97 open Hints_declaration
119 (** val check_well_cost_fn : RTLabs_syntax.internal_function -> Bool.bool **)
120 let check_well_cost_fn f =
122 (Identifiers.idmap_all PreIdentifiers.LabelTag f.RTLabs_syntax.f_graph
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)))
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 **)
135 let rec check_label_bounded g checking checking_tail to_check term_check =
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' ->
141 let st = Identifiers.lookup_present PreIdentifiers.LabelTag g checking
143 let succs = CostSpec.successors st in
145 | List.Nil -> (fun _ -> stop_now)
146 | List.Cons (h, t) ->
151 Identifiers.lookup_present PreIdentifiers.LabelTag g h
153 (match CostSpec.is_cost_label st' with
154 | Bool.True -> stop_now
156 (match Identifiers.try_remove PreIdentifiers.LabelTag
162 (Identifiers.deq_identifier
163 PreIdentifiers.LabelTag) (Obj.magic h)
164 (Obj.magic checking))
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' ->
173 check_label_bounded g h (List.Cons (checking,
174 checking_tail)) to_check'.Types.snd term_check')) __))
175 | List.Cons (x, x0) -> (fun _ -> stop_now))) __)) __
177 (** val check_graph_bounded :
178 RTLabs_syntax.statement Graphs.graph -> Identifiers.identifier_set ->
179 Graphs.label -> Nat.nat -> Bool.bool **)
180 let rec check_graph_bounded g to_check start term_check =
181 (match term_check with
182 | Nat.O -> (fun _ -> assert false (* absurd case *))
183 | Nat.S term_check' ->
185 (match check_label_bounded g start List.Nil to_check
186 (Identifiers.id_map_size PreIdentifiers.LabelTag g) with
187 | Types.None -> (fun _ -> Bool.False)
188 | Types.Some to_check' ->
190 (match Identifiers.choose PreIdentifiers.LabelTag to_check' with
191 | Types.None -> (fun _ _ _ -> Bool.True)
192 | Types.Some l_to_check'' ->
194 check_graph_bounded g l_to_check''.Types.snd
195 l_to_check''.Types.fst.Types.fst term_check')) __ __ __))
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 ->
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))) __ __ __
212 (** val check_cost_program : RTLabs_syntax.rTLabs_program -> Bool.bool **)
213 let check_cost_program p =
215 match fn.Types.snd with
216 | AST.Internal fn0 ->
217 Bool.andb (check_well_cost_fn fn0) (check_sound_cost_fn fn0)
218 | AST.External x -> Bool.True) p.AST.prog_funct
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 __)
226 (fun _ -> Errors.Error (Errors.msg ErrorMessages.BadCostLabelling))) __