open Preamble open Fetch open Hide open Division open Z open BitVectorZ open Pointers open Coqlib open Values open Events open IOMonad open IO open Sets open Listb open StructuredTraces open AbstractStatus open BitVectorTrie open String open Exp open Arithmetic open Vector open FoldStuff open BitVector open Extranat open Integers open AST open LabelledObjects open Proper open PositiveMap open Deqsets open ErrorMessages open PreIdentifiers open Errors open Extralib open Setoids open Monad open Option open Div_and_mod open Util open List open Lists open Bool open Relations open Nat open Positive open Identifiers open CostLabel open ASM open Types open Hints_declaration open Core_notation open Pts open Logic open Jmeq open Russell open Status open StatusProofs open Interpret open ASMCosts open UtilBranch (** val traverse_code_internal : ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Nat.nat Identifiers.identifier_map Types.sig0 **) let rec traverse_code_internal prog program_counter program_size = (match program_size with | Nat.O -> (fun _ -> Identifiers.empty_map PreIdentifiers.CostTag) | Nat.S program_size' -> (fun _ -> let new_program_counter' = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)) program_counter in let cost_mapping = traverse_code_internal prog new_program_counter' program_size' in (match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter prog.ASM.costlabels with | Types.None -> (fun _ -> Types.pi1 cost_mapping) | Types.Some lbl -> (fun _ -> let cost = ASMCosts.block_cost prog program_counter in Identifiers.add PreIdentifiers.CostTag (Types.pi1 cost_mapping) lbl (Types.pi1 cost))) __)) __ (** val traverse_code : ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0 **) let traverse_code prog = Types.pi1 (traverse_code_internal prog (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))) (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) (** val compute_costs : ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0 **) let compute_costs = traverse_code (** val aSM_cost_map : ASM.labelled_object_code -> StructuredTraces.as_cost_map **) let aSM_cost_map p = let cost_map = compute_costs p in (fun l_sig -> Identifiers.lookup_present PreIdentifiers.CostTag (Types.pi1 cost_map) (StructuredTraces.as_cost_get_label (ASMCosts.oC_abstract_status p) l_sig))