source: extracted/policyStep.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: 7.0 KB
Line 
1open Preamble
2
3open Assembly
4
5open Status
6
7open Fetch
8
9open String
10
11open LabelledObjects
12
13open BitVectorTrie
14
15open Exp
16
17open Arithmetic
18
19open Integers
20
21open AST
22
23open CostLabel
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Setoids
40
41open Monad
42
43open Option
44
45open Lists
46
47open Positive
48
49open Identifiers
50
51open Extranat
52
53open Vector
54
55open Div_and_mod
56
57open Jmeq
58
59open Russell
60
61open Types
62
63open List
64
65open Util
66
67open FoldStuff
68
69open Bool
70
71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
79open Relations
80
81open Nat
82
83open BitVector
84
85open ASM
86
87open PolicyFront
88
89(** val jump_expansion_step :
90    ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map
91    Types.sig0 -> PolicyFront.ppc_pc_map Types.sig0 -> (Bool.bool,
92    PolicyFront.ppc_pc_map Types.option) Types.prod Types.sig0 **)
93let jump_expansion_step program0 labels old_sigma =
94  (let { Types.fst = final_added; Types.snd = final_policy } =
95     Types.pi1
96       (FoldStuff.foldl_strong (Types.pi1 program0)
97         (fun prefix0 x tl _ acc ->
98         (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } =
99            Types.pi1 acc
100          in
101         (fun _ ->
102         (let { Types.fst = label; Types.snd = instr } = x in
103         (fun _ ->
104         let add_instr =
105           match instr with
106           | ASM.Instruction i ->
107             PolicyFront.jump_expansion_step_instruction (Types.pi1 labels)
108               (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix0) i
109           | ASM.Comment x0 -> Types.None
110           | ASM.Cost x0 -> Types.None
111           | ASM.Jmp j ->
112             Types.Some
113               (PolicyFront.select_jump_length (Types.pi1 labels)
114                 (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix0) j)
115           | ASM.Jnz (x0, x1, x2) -> Types.None
116           | ASM.MovSuccessor (x0, x1, x2) -> Types.None
117           | ASM.Call c ->
118             Types.Some
119               (PolicyFront.select_call_length (Types.pi1 labels)
120                 (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix0) c)
121           | ASM.Mov (x0, x1) -> Types.None
122         in
123         let { Types.fst = inc_pc; Types.snd = inc_sigma } = inc_pc_sigma in
124         let old_length =
125           (BitVectorTrie.lookup (Nat.S (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 (Nat.S
127             (Nat.S Nat.O))))))))))))))))
128             (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
129               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
130               (Nat.S (Nat.S Nat.O)))))))))))))))) (List.length prefix0))
131             (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
132             Assembly.Short_jump }).Types.snd
133         in
134         let old_size = PolicyFront.instruction_size_jmplen old_length instr
135         in
136         let { Types.fst = new_length; Types.snd = isize } =
137           match add_instr with
138           | Types.None ->
139             { Types.fst = Assembly.Short_jump; Types.snd =
140               (PolicyFront.instruction_size_jmplen Assembly.Short_jump
141                 instr) }
142           | Types.Some pl ->
143             { Types.fst = (PolicyFront.max_length old_length pl);
144               Types.snd =
145               (PolicyFront.instruction_size_jmplen
146                 (PolicyFront.max_length old_length pl) instr) }
147         in
148         let new_added =
149           match add_instr with
150           | Types.None -> inc_added
151           | Types.Some x0 -> Nat.plus inc_added (Nat.minus isize old_size)
152         in
153         let old_Slength =
154           (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
155             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
156             (Nat.S Nat.O))))))))))))))))
157             (Arithmetic.bitvector_of_nat (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 (Nat.S
159               (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S
160               (List.length prefix0))) (Types.pi1 old_sigma).Types.snd
161             { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.snd
162         in
163         let updated_sigma =
164           BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
165             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
166             (Nat.S Nat.O))))))))))))))))
167             (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
168               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
169               (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S
170               (List.length prefix0))) { Types.fst = (Nat.plus inc_pc isize);
171             Types.snd = old_Slength }
172             (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
173               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
174               (Nat.S Nat.O))))))))))))))))
175               (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
176                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
177                 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
178                 (List.length prefix0)) { Types.fst = inc_pc; Types.snd =
179               new_length } inc_sigma)
180         in
181         { Types.fst = new_added; Types.snd = { Types.fst =
182         (Nat.plus inc_pc isize); Types.snd = updated_sigma } })) __)) __)
183         { Types.fst = Nat.O; Types.snd = { Types.fst = Nat.O; Types.snd =
184         (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
185           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
186           (Nat.S Nat.O))))))))))))))))
187           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
188             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
189             (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O) { Types.fst = Nat.O;
190           Types.snd =
191           (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
192             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
193             (Nat.S Nat.O))))))))))))))))
194             (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
195               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
196               (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O)
197             (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
198             Assembly.Short_jump }).Types.snd } (BitVectorTrie.Stub (Nat.S
199           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
200           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } })
201   in
202  (fun _ ->
203  (match Util.gtb final_policy.Types.fst
204           (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
205             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
206             (Nat.S (Nat.S Nat.O))))))))))))))))) with
207   | Bool.True ->
208     (fun _ -> { Types.fst = (Nat.eqb final_added Nat.O); Types.snd =
209       Types.None })
210   | Bool.False ->
211     (fun _ -> { Types.fst = (Nat.eqb final_added Nat.O); Types.snd =
212       (Types.Some final_policy) })) __)) __
213
Note: See TracBrowser for help on using the repository browser.