source: driver/extracted/aSMCostsSplit.ml @ 3106

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

New extraction.

File size: 3.3 KB
Line 
1open Preamble
2
3open Fetch
4
5open Hide
6
7open Division
8
9open Z
10
11open BitVectorZ
12
13open Pointers
14
15open Coqlib
16
17open Values
18
19open Events
20
21open IOMonad
22
23open IO
24
25open Sets
26
27open Listb
28
29open StructuredTraces
30
31open AbstractStatus
32
33open BitVectorTrie
34
35open String
36
37open Exp
38
39open Arithmetic
40
41open Vector
42
43open FoldStuff
44
45open BitVector
46
47open Extranat
48
49open Integers
50
51open AST
52
53open LabelledObjects
54
55open Proper
56
57open PositiveMap
58
59open Deqsets
60
61open ErrorMessages
62
63open PreIdentifiers
64
65open Errors
66
67open Extralib
68
69open Setoids
70
71open Monad
72
73open Option
74
75open Div_and_mod
76
77open Util
78
79open List
80
81open Lists
82
83open Bool
84
85open Relations
86
87open Nat
88
89open Positive
90
91open Identifiers
92
93open CostLabel
94
95open ASM
96
97open Types
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Jmeq
108
109open Russell
110
111open Status
112
113open StatusProofs
114
115open Interpret
116
117open ASMCosts
118
119open UtilBranch
120
121(** val traverse_code_internal :
122    ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Nat.nat
123    Identifiers.identifier_map Types.sig0 **)
124let 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 **)
154let 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 **)
166let compute_costs =
167  traverse_code
168
169(** val aSM_cost_map :
170    ASM.labelled_object_code -> StructuredTraces.as_cost_map **)
171let 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
Note: See TracBrowser for help on using the repository browser.