source: driver/extracted/policyStep.ml @ 3106

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

New extraction.

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