[2730] | 1 | open Preamble |
---|
| 2 | |
---|
[2773] | 3 | open BitVectorTrie |
---|
| 4 | |
---|
[2730] | 5 | open Graphs |
---|
| 6 | |
---|
| 7 | open Order |
---|
| 8 | |
---|
| 9 | open Registers |
---|
| 10 | |
---|
| 11 | open FrontEndVal |
---|
| 12 | |
---|
| 13 | open Hide |
---|
| 14 | |
---|
| 15 | open ByteValues |
---|
| 16 | |
---|
| 17 | open GenMem |
---|
| 18 | |
---|
| 19 | open FrontEndMem |
---|
| 20 | |
---|
| 21 | open Division |
---|
| 22 | |
---|
| 23 | open Z |
---|
| 24 | |
---|
| 25 | open BitVectorZ |
---|
| 26 | |
---|
| 27 | open Pointers |
---|
| 28 | |
---|
| 29 | open Coqlib |
---|
| 30 | |
---|
| 31 | open Values |
---|
| 32 | |
---|
| 33 | open FrontEndOps |
---|
| 34 | |
---|
| 35 | open CostLabel |
---|
| 36 | |
---|
| 37 | open Proper |
---|
| 38 | |
---|
| 39 | open PositiveMap |
---|
| 40 | |
---|
| 41 | open Deqsets |
---|
| 42 | |
---|
| 43 | open ErrorMessages |
---|
| 44 | |
---|
| 45 | open PreIdentifiers |
---|
| 46 | |
---|
| 47 | open Errors |
---|
| 48 | |
---|
| 49 | open Extralib |
---|
| 50 | |
---|
| 51 | open Lists |
---|
| 52 | |
---|
| 53 | open Positive |
---|
| 54 | |
---|
| 55 | open Identifiers |
---|
| 56 | |
---|
| 57 | open Exp |
---|
| 58 | |
---|
| 59 | open Arithmetic |
---|
| 60 | |
---|
| 61 | open Vector |
---|
| 62 | |
---|
| 63 | open Div_and_mod |
---|
| 64 | |
---|
[2773] | 65 | open Util |
---|
| 66 | |
---|
| 67 | open FoldStuff |
---|
| 68 | |
---|
| 69 | open BitVector |
---|
| 70 | |
---|
[2730] | 71 | open Jmeq |
---|
| 72 | |
---|
| 73 | open Russell |
---|
| 74 | |
---|
| 75 | open List |
---|
| 76 | |
---|
[2773] | 77 | open Setoids |
---|
[2730] | 78 | |
---|
[2773] | 79 | open Monad |
---|
[2730] | 80 | |
---|
[2773] | 81 | open Option |
---|
[2730] | 82 | |
---|
| 83 | open Extranat |
---|
| 84 | |
---|
| 85 | open Bool |
---|
| 86 | |
---|
| 87 | open Relations |
---|
| 88 | |
---|
| 89 | open Nat |
---|
| 90 | |
---|
| 91 | open Integers |
---|
| 92 | |
---|
| 93 | open Types |
---|
| 94 | |
---|
| 95 | open AST |
---|
| 96 | |
---|
| 97 | open Hints_declaration |
---|
| 98 | |
---|
| 99 | open Core_notation |
---|
| 100 | |
---|
| 101 | open Pts |
---|
| 102 | |
---|
| 103 | open Logic |
---|
| 104 | |
---|
| 105 | open RTLabs_syntax |
---|
| 106 | |
---|
| 107 | open CostSpec |
---|
| 108 | |
---|
| 109 | open Extra_bool |
---|
| 110 | |
---|
| 111 | open Sets |
---|
| 112 | |
---|
| 113 | open Listb |
---|
| 114 | |
---|
[2743] | 115 | open Listb_extra |
---|
[2730] | 116 | |
---|
| 117 | open CostMisc |
---|
| 118 | |
---|
| 119 | (** val check_well_cost_fn : RTLabs_syntax.internal_function -> Bool.bool **) |
---|
| 120 | let check_well_cost_fn f = |
---|
| 121 | Bool.andb |
---|
| 122 | (Identifiers.idmap_all PreIdentifiers.LabelTag f.RTLabs_syntax.f_graph |
---|
| 123 | (fun l s _ -> |
---|
| 124 | CostSpec.well_cost_labelled_statement f.RTLabs_syntax.f_graph s)) |
---|
| 125 | (CostSpec.is_cost_label |
---|
| 126 | (Identifiers.lookup_present PreIdentifiers.LabelTag |
---|
| 127 | f.RTLabs_syntax.f_graph (Types.pi1 f.RTLabs_syntax.f_entry))) |
---|
| 128 | |
---|
| 129 | open Deqsets_extra |
---|
| 130 | |
---|
| 131 | (** val check_label_bounded : |
---|
| 132 | RTLabs_syntax.statement Graphs.graph -> Graphs.label -> Graphs.label |
---|
| 133 | List.list -> Identifiers.identifier_set -> Nat.nat -> |
---|
| 134 | Identifiers.identifier_set Types.option **) |
---|
[2773] | 135 | let rec check_label_bounded g checking checking_tail to_check term_check = |
---|
[2730] | 136 | let stop_now = Types.Some to_check in |
---|
| 137 | (match term_check with |
---|
| 138 | | Nat.O -> (fun _ -> assert false (* absurd case *)) |
---|
| 139 | | Nat.S term_check' -> |
---|
| 140 | (fun _ -> |
---|
[2773] | 141 | let st = Identifiers.lookup_present PreIdentifiers.LabelTag g checking |
---|
[2730] | 142 | in |
---|
| 143 | let succs = CostSpec.successors st in |
---|
| 144 | (match succs with |
---|
| 145 | | List.Nil -> (fun _ -> stop_now) |
---|
| 146 | | List.Cons (h, t) -> |
---|
| 147 | (match t with |
---|
| 148 | | List.Nil -> |
---|
| 149 | (fun _ -> |
---|
| 150 | let st' = |
---|
[2773] | 151 | Identifiers.lookup_present PreIdentifiers.LabelTag g h |
---|
[2730] | 152 | in |
---|
| 153 | (match CostSpec.is_cost_label st' with |
---|
| 154 | | Bool.True -> stop_now |
---|
| 155 | | Bool.False -> |
---|
| 156 | (match Identifiers.try_remove PreIdentifiers.LabelTag |
---|
| 157 | to_check h with |
---|
| 158 | | Types.None -> |
---|
| 159 | (fun _ -> |
---|
| 160 | match Bool.orb |
---|
| 161 | (Deqsets.eqb |
---|
| 162 | (Identifiers.deq_identifier |
---|
| 163 | PreIdentifiers.LabelTag) (Obj.magic h) |
---|
| 164 | (Obj.magic checking)) |
---|
| 165 | (Listb.memb |
---|
| 166 | (Identifiers.deq_identifier |
---|
| 167 | PreIdentifiers.LabelTag) (Obj.magic h) |
---|
| 168 | (Obj.magic checking_tail)) with |
---|
| 169 | | Bool.True -> Types.None |
---|
| 170 | | Bool.False -> stop_now) |
---|
| 171 | | Types.Some to_check' -> |
---|
| 172 | (fun _ -> |
---|
[2773] | 173 | check_label_bounded g h (List.Cons (checking, |
---|
[2730] | 174 | checking_tail)) to_check'.Types.snd term_check')) __)) |
---|
| 175 | | List.Cons (x, x0) -> (fun _ -> stop_now))) __)) __ |
---|
| 176 | |
---|
| 177 | (** val check_graph_bounded : |
---|
| 178 | RTLabs_syntax.statement Graphs.graph -> Identifiers.identifier_set -> |
---|
| 179 | Graphs.label -> Nat.nat -> Bool.bool **) |
---|
[2773] | 180 | let rec check_graph_bounded g to_check start term_check = |
---|
[2730] | 181 | (match term_check with |
---|
| 182 | | Nat.O -> (fun _ -> assert false (* absurd case *)) |
---|
| 183 | | Nat.S term_check' -> |
---|
| 184 | (fun _ -> |
---|
[2773] | 185 | (match check_label_bounded g start List.Nil to_check |
---|
| 186 | (Identifiers.id_map_size PreIdentifiers.LabelTag g) with |
---|
[2730] | 187 | | Types.None -> (fun _ -> Bool.False) |
---|
| 188 | | Types.Some to_check' -> |
---|
| 189 | (fun _ -> |
---|
| 190 | (match Identifiers.choose PreIdentifiers.LabelTag to_check' with |
---|
| 191 | | Types.None -> (fun _ _ _ -> Bool.True) |
---|
| 192 | | Types.Some l_to_check'' -> |
---|
| 193 | (fun _ _ _ -> |
---|
[2773] | 194 | check_graph_bounded g l_to_check''.Types.snd |
---|
[2730] | 195 | l_to_check''.Types.fst.Types.fst term_check')) __ __ __)) |
---|
| 196 | __)) __ |
---|
| 197 | |
---|
| 198 | (** val check_sound_cost_fn : |
---|
| 199 | RTLabs_syntax.internal_function -> Bool.bool **) |
---|
| 200 | let check_sound_cost_fn fn = |
---|
| 201 | (match Identifiers.try_remove PreIdentifiers.LabelTag |
---|
| 202 | (Identifiers.id_set_of_map PreIdentifiers.LabelTag |
---|
| 203 | fn.RTLabs_syntax.f_graph) (Types.pi1 fn.RTLabs_syntax.f_entry) with |
---|
| 204 | | Types.None -> (fun _ -> assert false (* absurd case *)) |
---|
| 205 | | Types.Some to_check -> |
---|
| 206 | (fun _ _ _ -> |
---|
| 207 | check_graph_bounded fn.RTLabs_syntax.f_graph to_check.Types.snd |
---|
| 208 | (Types.pi1 fn.RTLabs_syntax.f_entry) |
---|
| 209 | (Identifiers.id_map_size PreIdentifiers.LabelTag |
---|
| 210 | fn.RTLabs_syntax.f_graph))) __ __ __ |
---|
| 211 | |
---|
| 212 | (** val check_cost_program : RTLabs_syntax.rTLabs_program -> Bool.bool **) |
---|
| 213 | let check_cost_program p = |
---|
[2773] | 214 | Lists.all (fun fn -> |
---|
[2730] | 215 | match fn.Types.snd with |
---|
| 216 | | AST.Internal fn0 -> |
---|
| 217 | Bool.andb (check_well_cost_fn fn0) (check_sound_cost_fn fn0) |
---|
[3043] | 218 | | AST.External x -> Bool.True) p.AST.prog_funct |
---|
[2730] | 219 | |
---|
[3043] | 220 | (** val check_cost_program_prf : |
---|
| 221 | RTLabs_syntax.rTLabs_program -> __ Errors.res **) |
---|
| 222 | let check_cost_program_prf p = |
---|
| 223 | (match check_cost_program p with |
---|
| 224 | | Bool.True -> (fun _ -> Errors.OK __) |
---|
| 225 | | Bool.False -> |
---|
| 226 | (fun _ -> Errors.Error (Errors.msg ErrorMessages.BadCostLabelling))) __ |
---|
| 227 | |
---|