source: extracted/aSMCostsSplit.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 3.8 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 Jmeq
78
79open Russell
80
81open Util
82
83open List
84
85open Lists
86
87open Bool
88
89open Relations
90
91open Nat
92
93open Positive
94
95open Hints_declaration
96
97open Core_notation
98
99open Pts
100
101open Logic
102
103open Types
104
105open Identifiers
106
107open CostLabel
108
109open ASM
110
111open Status
112
113open StatusProofs
114
115open Interpret
116
117open ASMCosts
118
119open UtilBranch
120
121(** val traverse_code_internal :
122    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
123    BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat -> Nat.nat
124    Identifiers.identifier_map Types.sig0 **)
125let rec traverse_code_internal code_memory cost_labels program_counter program_size =
126  (match program_size with
127   | Nat.O -> (fun _ -> Identifiers.empty_map PreIdentifiers.CostTag)
128   | Nat.S program_size' ->
129     (fun _ ->
130       let new_program_counter' =
131         Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
132           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
133           Nat.O))))))))))))))))
134           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
135             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
136             (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O))
137           program_counter
138       in
139       let cost_mapping =
140         traverse_code_internal code_memory cost_labels new_program_counter'
141           program_size'
142       in
143       (match BitVectorTrie.lookup_opt (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.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter
146                cost_labels with
147        | Types.None -> (fun _ -> Types.pi1 cost_mapping)
148        | Types.Some lbl ->
149          (fun _ ->
150            let cost =
151              ASMCosts.block_cost code_memory program_counter cost_labels
152            in
153            Identifiers.add PreIdentifiers.CostTag (Types.pi1 cost_mapping)
154              lbl (Types.pi1 cost))) __)) __
155
156(** val traverse_code :
157    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
158    BitVectorTrie.bitVectorTrie -> Nat.nat Identifiers.identifier_map
159    Types.sig0 **)
160let traverse_code code_memory cost_labels =
161  Types.pi1
162    (traverse_code_internal code_memory cost_labels
163      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
164        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
165        Nat.O)))))))))))))))))
166      (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
167        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
168        (Nat.S Nat.O))))))))))))))))))
169
170(** val compute_costs :
171    ASM.object_code -> CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
172    Nat.nat Identifiers.identifier_map Types.sig0 **)
173let compute_costs program cost_labels =
174  let code_memory = Fetch.load_code_memory program in
175  traverse_code code_memory cost_labels
176
177(** val aSM_cost_map :
178    ASM.labelled_object_code -> StructuredTraces.as_cost_map **)
179let aSM_cost_map p =
180  let cost_map = compute_costs p.ASM.oc p.ASM.costlabels in
181  (fun l_sig ->
182  Identifiers.lookup_present PreIdentifiers.CostTag (Types.pi1 cost_map)
183    (StructuredTraces.as_cost_get_label
184      (ASMCosts.aSM_abstract_status (Fetch.load_code_memory p.ASM.oc)
185        p.ASM.costlabels) l_sig))
186
Note: See TracBrowser for help on using the repository browser.