source: extracted/aSMCostsSplit.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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 LabelledObjects
22
23open Coqlib
24
25open Floats
26
27open Arithmetic
28
29open Integers
30
31open AST
32
33open CostLabel
34
35open Proper
36
37open PositiveMap
38
39open Deqsets
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 Char
60
61open String
62
63open Extranat
64
65open Vector
66
67open Div_and_mod
68
69open Jmeq
70
71open Russell
72
73open Types
74
75open List
76
77open Util
78
79open FoldStuff
80
81open Bool
82
83open Hints_declaration
84
85open Core_notation
86
87open Pts
88
89open Logic
90
91open Relations
92
93open Nat
94
95open BitVector
96
97open ASM
98
99open ASMCosts
100
101open UtilBranch
102
103(** val traverse_code_internal :
104    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
105    BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat -> Nat.nat
106    Identifiers.identifier_map Types.sig0 **)
107let rec traverse_code_internal code_memory cost_labels program_counter0 program_size =
108  (match program_size with
109   | Nat.O -> (fun _ -> Identifiers.empty_map CostLabel.costTag)
110   | Nat.S program_size' ->
111     (fun _ ->
112       let new_program_counter' =
113         Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
114           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
115           Nat.O))))))))))))))))
116           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
117             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
118             (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O))
119           program_counter0
120       in
121       let cost_mapping =
122         traverse_code_internal code_memory cost_labels new_program_counter'
123           program_size'
124       in
125       (match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
126                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
127                (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter0
128                cost_labels with
129        | Types.None -> (fun _ -> Types.pi1 cost_mapping)
130        | Types.Some lbl ->
131          (fun _ ->
132            let cost =
133              ASMCosts.block_cost code_memory program_counter0 cost_labels
134            in
135            Identifiers.add CostLabel.costTag (Types.pi1 cost_mapping) lbl
136              (Types.pi1 cost))) __)) __
137
138(** val traverse_code :
139    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
140    BitVectorTrie.bitVectorTrie -> Nat.nat Identifiers.identifier_map
141    Types.sig0 **)
142let traverse_code code_memory cost_labels =
143  Types.pi1
144    (traverse_code_internal code_memory cost_labels
145      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
146        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
147        Nat.O)))))))))))))))))
148      (Util.exponential (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
149        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
150        (Nat.S (Nat.S Nat.O))))))))))))))))))
151
152(** val compute_costs :
153    BitVector.byte List.list -> CostLabel.costlabel
154    BitVectorTrie.bitVectorTrie -> Nat.nat Identifiers.identifier_map
155    Types.sig0 **)
156let compute_costs program0 cost_labels =
157  let code_memory = Fetch.load_code_memory program0 in
158  traverse_code code_memory cost_labels
159
160(** val aSM_cost_map :
161    (BitVector.byte List.list, CostLabel.costlabel
162    BitVectorTrie.bitVectorTrie) Types.prod -> StructuredTraces.as_cost_map **)
163let aSM_cost_map p =
164  let cost_map = compute_costs p.Types.fst p.Types.snd in
165  (fun l_sig ->
166  Identifiers.lookup_present CostLabel.costTag (Types.pi1 cost_map)
167    (StructuredTraces.as_cost_get_label
168      (ASMCosts.aSM_abstract_status (Fetch.load_code_memory p.Types.fst)
169        p.Types.snd) l_sig))
170
Note: See TracBrowser for help on using the repository browser.