[2601] | 1 | open Preamble |
---|
| 2 | |
---|
[2773] | 3 | open Fetch |
---|
[2601] | 4 | |
---|
[2773] | 5 | open Hide |
---|
[2601] | 6 | |
---|
[2773] | 7 | open Division |
---|
[2601] | 8 | |
---|
[2773] | 9 | open Z |
---|
[2601] | 10 | |
---|
[2773] | 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 | |
---|
[2601] | 25 | open Sets |
---|
| 26 | |
---|
| 27 | open Listb |
---|
| 28 | |
---|
[2773] | 29 | open StructuredTraces |
---|
[2601] | 30 | |
---|
[2773] | 31 | open AbstractStatus |
---|
[2601] | 32 | |
---|
[2773] | 33 | open BitVectorTrie |
---|
| 34 | |
---|
[2649] | 35 | open String |
---|
| 36 | |
---|
[2717] | 37 | open Exp |
---|
| 38 | |
---|
[2601] | 39 | open Arithmetic |
---|
| 40 | |
---|
[2773] | 41 | open Vector |
---|
| 42 | |
---|
| 43 | open FoldStuff |
---|
| 44 | |
---|
| 45 | open BitVector |
---|
| 46 | |
---|
| 47 | open Extranat |
---|
| 48 | |
---|
[2601] | 49 | open Integers |
---|
| 50 | |
---|
| 51 | open AST |
---|
| 52 | |
---|
[2773] | 53 | open LabelledObjects |
---|
[2601] | 54 | |
---|
| 55 | open Proper |
---|
| 56 | |
---|
| 57 | open PositiveMap |
---|
| 58 | |
---|
| 59 | open Deqsets |
---|
| 60 | |
---|
[2649] | 61 | open ErrorMessages |
---|
| 62 | |
---|
[2601] | 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 Jmeq |
---|
| 78 | |
---|
| 79 | open Russell |
---|
| 80 | |
---|
[2773] | 81 | open Util |
---|
[2601] | 82 | |
---|
| 83 | open List |
---|
| 84 | |
---|
[2773] | 85 | open Lists |
---|
[2601] | 86 | |
---|
| 87 | open Bool |
---|
| 88 | |
---|
[2773] | 89 | open Relations |
---|
| 90 | |
---|
| 91 | open Nat |
---|
| 92 | |
---|
| 93 | open Positive |
---|
| 94 | |
---|
[2601] | 95 | open Hints_declaration |
---|
| 96 | |
---|
| 97 | open Core_notation |
---|
| 98 | |
---|
| 99 | open Pts |
---|
| 100 | |
---|
| 101 | open Logic |
---|
| 102 | |
---|
[2773] | 103 | open Types |
---|
[2601] | 104 | |
---|
[2773] | 105 | open Identifiers |
---|
[2601] | 106 | |
---|
[2773] | 107 | open CostLabel |
---|
[2601] | 108 | |
---|
| 109 | open ASM |
---|
| 110 | |
---|
[2773] | 111 | open Status |
---|
| 112 | |
---|
| 113 | open StatusProofs |
---|
| 114 | |
---|
| 115 | open Interpret |
---|
| 116 | |
---|
[2601] | 117 | open ASMCosts |
---|
| 118 | |
---|
| 119 | open UtilBranch |
---|
| 120 | |
---|
| 121 | (** val traverse_code_internal : |
---|
[2909] | 122 | ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Nat.nat |
---|
[2601] | 123 | Identifiers.identifier_map Types.sig0 **) |
---|
[2909] | 124 | let rec traverse_code_internal prog program_counter program_size = |
---|
[2601] | 125 | (match program_size with |
---|
[2997] | 126 | | Nat.O -> (fun _ -> Identifiers.empty_map PreIdentifiers.CostTag) |
---|
| 127 | | Nat.S program_size' -> |
---|
[2601] | 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)) |
---|
[2773] | 136 | program_counter |
---|
[2601] | 137 | in |
---|
| 138 | let cost_mapping = |
---|
[2909] | 139 | traverse_code_internal prog new_program_counter' program_size' |
---|
[2601] | 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 |
---|
[2773] | 143 | (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter |
---|
[2909] | 144 | prog.ASM.costlabels with |
---|
[2601] | 145 | | Types.None -> (fun _ -> Types.pi1 cost_mapping) |
---|
| 146 | | Types.Some lbl -> |
---|
| 147 | (fun _ -> |
---|
[2909] | 148 | let cost = ASMCosts.block_cost prog program_counter in |
---|
[2649] | 149 | Identifiers.add PreIdentifiers.CostTag (Types.pi1 cost_mapping) |
---|
| 150 | lbl (Types.pi1 cost))) __)) __ |
---|
[2601] | 151 | |
---|
| 152 | (** val traverse_code : |
---|
[2909] | 153 | ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0 **) |
---|
| 154 | let traverse_code prog = |
---|
[2601] | 155 | Types.pi1 |
---|
[2909] | 156 | (traverse_code_internal prog |
---|
[2601] | 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))))))))))))))))) |
---|
[2997] | 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)))))))))))))))))) |
---|
[2601] | 163 | |
---|
| 164 | (** val compute_costs : |
---|
[2909] | 165 | ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0 **) |
---|
| 166 | let compute_costs = |
---|
| 167 | traverse_code |
---|
[2601] | 168 | |
---|
| 169 | (** val aSM_cost_map : |
---|
[2773] | 170 | ASM.labelled_object_code -> StructuredTraces.as_cost_map **) |
---|
[2601] | 171 | let aSM_cost_map p = |
---|
[2909] | 172 | let cost_map = compute_costs p in |
---|
[2601] | 173 | (fun l_sig -> |
---|
[2649] | 174 | Identifiers.lookup_present PreIdentifiers.CostTag (Types.pi1 cost_map) |
---|
[2909] | 175 | (StructuredTraces.as_cost_get_label (ASMCosts.oC_abstract_status p) |
---|
| 176 | l_sig)) |
---|
[2601] | 177 | |
---|