extracted/aSMCostsSplit.ml

   1 open Preamble
   2
   3 open Fetch
   4
   5 open Hide
   6
   7 open Division
   8
   9 open Z
  10
  11 open BitVectorZ
  12
  13 open Pointers
  14
  15 open Coqlib
  16
  17 open Values
  18
  19 open Events
  20
  21 open IOMonad
  22
  23 open IO
  24
  25 open Sets
  26
  27 open Listb
  28
  29 open StructuredTraces
  30
  31 open AbstractStatus
  32
  33 open BitVectorTrie
  34
  35 open String
  36
  37 open Exp
  38
  39 open Arithmetic
  40
  41 open Vector
  42
  43 open FoldStuff
  44
  45 open BitVector
  46
  47 open Extranat
  48
  49 open Integers
  50
  51 open AST
  52
  53 open LabelledObjects
  54
  55 open Proper
  56
  57 open PositiveMap
  58
  59 open Deqsets
  60
  61 open ErrorMessages
  62
  63 open PreIdentifiers
  64
  65 open Errors
  66
  67 open Extralib
  68
  69 open Setoids
  70
  71 open Monad
  72
  73 open Option
  74
  75 open Div_and_mod
  76
  77 open Util
  78
  79 open List
  80
  81 open Lists
  82
  83 open Bool
  84
  85 open Relations
  86
  87 open Nat
  88
  89 open Positive
  90
  91 open Identifiers
  92
  93 open CostLabel
  94
  95 open ASM
  96
  97 open Types
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 106
 107 open Jmeq
 108
 109 open Russell
 110
 111 open Status
 112
 113 open StatusProofs
 114
 115 open Interpret
 116
 117 open ASMCosts
 118
 119 open UtilBranch
 120
 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' ->
 128      (fun _ ->
 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))
 136            program_counter
 137        in
 138        let cost_mapping =
 139          traverse_code_internal prog new_program_counter' program_size'
 140        in
 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)
 146         | Types.Some lbl ->
 147           (fun _ ->
 148             let cost = ASMCosts.block_cost prog program_counter in
 149             Identifiers.add PreIdentifiers.CostTag (Types.pi1 cost_mapping)
 150               lbl (Types.pi1 cost))) __)) __
 151
 152 (** val traverse_code :
 153     ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0 **)
 154 let traverse_code prog =
 155   Types.pi1
 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))))))))))))))))))
 163
 164 (** val compute_costs :
 165     ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0 **)
 166 let compute_costs =
 167   traverse_code
 168
 169 (** val aSM_cost_map :
 170     ASM.labelled_object_code -> StructuredTraces.as_cost_map **)
 171 let aSM_cost_map p =
 172   let cost_map = compute_costs p in
 173   (fun l_sig ->
 174   Identifiers.lookup_present PreIdentifiers.CostTag (Types.pi1 cost_map)
 175     (StructuredTraces.as_cost_get_label (ASMCosts.oC_abstract_status p)
 176       l_sig))
 177