1 | open Preamble |
---|
2 | |
---|
3 | open StructuredTraces |
---|
4 | |
---|
5 | open AbstractStatus |
---|
6 | |
---|
7 | open Status |
---|
8 | |
---|
9 | open StatusProofs |
---|
10 | |
---|
11 | open Sets |
---|
12 | |
---|
13 | open Listb |
---|
14 | |
---|
15 | open Interpret |
---|
16 | |
---|
17 | open Fetch |
---|
18 | |
---|
19 | open String |
---|
20 | |
---|
21 | open LabelledObjects |
---|
22 | |
---|
23 | open BitVectorTrie |
---|
24 | |
---|
25 | open Exp |
---|
26 | |
---|
27 | open Arithmetic |
---|
28 | |
---|
29 | open Integers |
---|
30 | |
---|
31 | open AST |
---|
32 | |
---|
33 | open CostLabel |
---|
34 | |
---|
35 | open Proper |
---|
36 | |
---|
37 | open PositiveMap |
---|
38 | |
---|
39 | open Deqsets |
---|
40 | |
---|
41 | open ErrorMessages |
---|
42 | |
---|
43 | open PreIdentifiers |
---|
44 | |
---|
45 | open Errors |
---|
46 | |
---|
47 | open Extralib |
---|
48 | |
---|
49 | open Setoids |
---|
50 | |
---|
51 | open Monad |
---|
52 | |
---|
53 | open Option |
---|
54 | |
---|
55 | open Lists |
---|
56 | |
---|
57 | open Positive |
---|
58 | |
---|
59 | open Identifiers |
---|
60 | |
---|
61 | open Extranat |
---|
62 | |
---|
63 | open Vector |
---|
64 | |
---|
65 | open Div_and_mod |
---|
66 | |
---|
67 | open Jmeq |
---|
68 | |
---|
69 | open Russell |
---|
70 | |
---|
71 | open Types |
---|
72 | |
---|
73 | open List |
---|
74 | |
---|
75 | open Util |
---|
76 | |
---|
77 | open FoldStuff |
---|
78 | |
---|
79 | open Bool |
---|
80 | |
---|
81 | open Hints_declaration |
---|
82 | |
---|
83 | open Core_notation |
---|
84 | |
---|
85 | open Pts |
---|
86 | |
---|
87 | open Logic |
---|
88 | |
---|
89 | open Relations |
---|
90 | |
---|
91 | open Nat |
---|
92 | |
---|
93 | open BitVector |
---|
94 | |
---|
95 | open ASM |
---|
96 | |
---|
97 | open ASMCosts |
---|
98 | |
---|
99 | open UtilBranch |
---|
100 | |
---|
101 | (** val traverse_code_internal : |
---|
102 | BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel |
---|
103 | BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat -> Nat.nat |
---|
104 | Identifiers.identifier_map Types.sig0 **) |
---|
105 | let rec traverse_code_internal code_memory cost_labels program_counter0 program_size = |
---|
106 | (match program_size with |
---|
107 | | Nat.O -> (fun _ -> Identifiers.empty_map PreIdentifiers.CostTag) |
---|
108 | | Nat.S program_size' -> |
---|
109 | (fun _ -> |
---|
110 | let new_program_counter' = |
---|
111 | Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
112 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
113 | Nat.O)))))))))))))))) |
---|
114 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
115 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
116 | (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)) |
---|
117 | program_counter0 |
---|
118 | in |
---|
119 | let cost_mapping = |
---|
120 | traverse_code_internal code_memory cost_labels new_program_counter' |
---|
121 | program_size' |
---|
122 | in |
---|
123 | (match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
124 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
125 | (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter0 |
---|
126 | cost_labels with |
---|
127 | | Types.None -> (fun _ -> Types.pi1 cost_mapping) |
---|
128 | | Types.Some lbl -> |
---|
129 | (fun _ -> |
---|
130 | let cost = |
---|
131 | ASMCosts.block_cost code_memory program_counter0 cost_labels |
---|
132 | in |
---|
133 | Identifiers.add PreIdentifiers.CostTag (Types.pi1 cost_mapping) |
---|
134 | lbl (Types.pi1 cost))) __)) __ |
---|
135 | |
---|
136 | (** val traverse_code : |
---|
137 | BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel |
---|
138 | BitVectorTrie.bitVectorTrie -> Nat.nat Identifiers.identifier_map |
---|
139 | Types.sig0 **) |
---|
140 | let traverse_code code_memory cost_labels = |
---|
141 | Types.pi1 |
---|
142 | (traverse_code_internal code_memory cost_labels |
---|
143 | (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
144 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
145 | Nat.O))))))))))))))))) |
---|
146 | (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
147 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
148 | (Nat.S Nat.O)))))))))))))))))) |
---|
149 | |
---|
150 | (** val compute_costs : |
---|
151 | BitVector.byte List.list -> CostLabel.costlabel |
---|
152 | BitVectorTrie.bitVectorTrie -> Nat.nat Identifiers.identifier_map |
---|
153 | Types.sig0 **) |
---|
154 | let compute_costs program0 cost_labels = |
---|
155 | let code_memory = Fetch.load_code_memory program0 in |
---|
156 | traverse_code code_memory cost_labels |
---|
157 | |
---|
158 | (** val aSM_cost_map : |
---|
159 | (BitVector.byte List.list, CostLabel.costlabel |
---|
160 | BitVectorTrie.bitVectorTrie) Types.prod -> StructuredTraces.as_cost_map **) |
---|
161 | let aSM_cost_map p = |
---|
162 | let cost_map = compute_costs p.Types.fst p.Types.snd in |
---|
163 | (fun l_sig -> |
---|
164 | Identifiers.lookup_present PreIdentifiers.CostTag (Types.pi1 cost_map) |
---|
165 | (StructuredTraces.as_cost_get_label |
---|
166 | (ASMCosts.aSM_abstract_status (Fetch.load_code_memory p.Types.fst) |
---|
167 | p.Types.snd) l_sig)) |
---|
168 | |
---|