source: extracted/aSMCostsSplit.ml @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 7 years ago

...

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