source: extracted/aSMCostsSplit.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.
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 Fetch
18
19open String
20
21open LabelledObjects
22
23open BitVectorTrie
24
25open Exp
26
27open Arithmetic
28
29open Integers
30
31open AST
32
33open CostLabel
34
35open Proper
36
37open PositiveMap
38
39open Deqsets
40
41open ErrorMessages
42
43open PreIdentifiers
44
45open Errors
46
47open Extralib
48
49open Setoids
50
51open Monad
52
53open Option
54
55open Lists
56
57open Positive
58
59open Identifiers
60
61open Extranat
62
63open Vector
64
65open Div_and_mod
66
67open Jmeq
68
69open Russell
70
71open Types
72
73open List
74
75open Util
76
77open FoldStuff
78
79open Bool
80
81open Hints_declaration
82
83open Core_notation
84
85open Pts
86
87open Logic
88
89open Relations
90
91open Nat
92
93open BitVector
94
95open ASM
96
97open ASMCosts
98
99open 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 **)
105let 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 **)
140let 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 **)
154let 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 **)
161let 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
Note: See TracBrowser for help on using the repository browser.