99 open Hints_declaration
121 (** val traverse_code_internal :
122 ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Nat.nat
123 Identifiers.identifier_map Types.sig0 **)
124 let rec traverse_code_internal prog program_counter program_size =
125 (match program_size with
126 | Nat.O -> (fun _ -> Identifiers.empty_map PreIdentifiers.CostTag)
127 | Nat.S program_size' ->
129 let new_program_counter' =
130 Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
131 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
132 Nat.O))))))))))))))))
133 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
134 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
135 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O))
139 traverse_code_internal prog new_program_counter' program_size'
141 (match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
142 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
143 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter
144 prog.ASM.costlabels with
145 | Types.None -> (fun _ -> Types.pi1 cost_mapping)
148 let cost = ASMCosts.block_cost prog program_counter in
149 Identifiers.add PreIdentifiers.CostTag (Types.pi1 cost_mapping)
150 lbl (Types.pi1 cost))) __)) __
152 (** val traverse_code :
153 ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0 **)
154 let traverse_code prog =
156 (traverse_code_internal prog
157 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
158 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
159 Nat.O)))))))))))))))))
160 (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
161 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
162 (Nat.S Nat.O))))))))))))))))))
164 (** val compute_costs :
165 ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0 **)
169 (** val aSM_cost_map :
170 ASM.labelled_object_code -> StructuredTraces.as_cost_map **)
172 let cost_map = compute_costs p in
174 Identifiers.lookup_present PreIdentifiers.CostTag (Types.pi1 cost_map)
175 (StructuredTraces.as_cost_get_label (ASMCosts.oC_abstract_status p)