source: extracted/policyStep.ml @ 3043

Last change on this file since 3043 was 3043, checked in by sacerdot, 8 years ago

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

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