source: extracted/eRTLptr.ml @ 2797

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

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File size: 10.6 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open BitVectorTrie
12
13open Graphs
14
15open I8051
16
17open Order
18
19open Registers
20
21open CostLabel
22
23open Hide
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Lists
40
41open Identifiers
42
43open Integers
44
45open AST
46
47open Division
48
49open Exp
50
51open Arithmetic
52
53open Setoids
54
55open Monad
56
57open Option
58
59open Extranat
60
61open Vector
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open List
70
71open Util
72
73open FoldStuff
74
75open BitVector
76
77open Types
78
79open Bool
80
81open Relations
82
83open Nat
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107open ERTL
108
109type ertlptr_seq =
110| Ertlptr_ertl of ERTL.ertl_seq
111| LOW_ADDRESS of Registers.register * Graphs.label
112| HIGH_ADDRESS of Registers.register * Graphs.label
113
114(** val ertlptr_seq_rect_Type4 :
115    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
116    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
117let rec ertlptr_seq_rect_Type4 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
118| Ertlptr_ertl x_21255 -> h_ertlptr_ertl x_21255
119| LOW_ADDRESS (x_21257, x_21256) -> h_LOW_ADDRESS x_21257 x_21256
120| HIGH_ADDRESS (x_21259, x_21258) -> h_HIGH_ADDRESS x_21259 x_21258
121
122(** val ertlptr_seq_rect_Type5 :
123    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
124    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
125let rec ertlptr_seq_rect_Type5 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
126| Ertlptr_ertl x_21264 -> h_ertlptr_ertl x_21264
127| LOW_ADDRESS (x_21266, x_21265) -> h_LOW_ADDRESS x_21266 x_21265
128| HIGH_ADDRESS (x_21268, x_21267) -> h_HIGH_ADDRESS x_21268 x_21267
129
130(** val ertlptr_seq_rect_Type3 :
131    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
132    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
133let rec ertlptr_seq_rect_Type3 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
134| Ertlptr_ertl x_21273 -> h_ertlptr_ertl x_21273
135| LOW_ADDRESS (x_21275, x_21274) -> h_LOW_ADDRESS x_21275 x_21274
136| HIGH_ADDRESS (x_21277, x_21276) -> h_HIGH_ADDRESS x_21277 x_21276
137
138(** val ertlptr_seq_rect_Type2 :
139    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
140    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
141let rec ertlptr_seq_rect_Type2 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
142| Ertlptr_ertl x_21282 -> h_ertlptr_ertl x_21282
143| LOW_ADDRESS (x_21284, x_21283) -> h_LOW_ADDRESS x_21284 x_21283
144| HIGH_ADDRESS (x_21286, x_21285) -> h_HIGH_ADDRESS x_21286 x_21285
145
146(** val ertlptr_seq_rect_Type1 :
147    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
148    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
149let rec ertlptr_seq_rect_Type1 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
150| Ertlptr_ertl x_21291 -> h_ertlptr_ertl x_21291
151| LOW_ADDRESS (x_21293, x_21292) -> h_LOW_ADDRESS x_21293 x_21292
152| HIGH_ADDRESS (x_21295, x_21294) -> h_HIGH_ADDRESS x_21295 x_21294
153
154(** val ertlptr_seq_rect_Type0 :
155    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
156    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
157let rec ertlptr_seq_rect_Type0 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
158| Ertlptr_ertl x_21300 -> h_ertlptr_ertl x_21300
159| LOW_ADDRESS (x_21302, x_21301) -> h_LOW_ADDRESS x_21302 x_21301
160| HIGH_ADDRESS (x_21304, x_21303) -> h_HIGH_ADDRESS x_21304 x_21303
161
162(** val ertlptr_seq_inv_rect_Type4 :
163    ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
164    Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __
165    -> 'a1) -> 'a1 **)
166let ertlptr_seq_inv_rect_Type4 hterm h1 h2 h3 =
167  let hcut = ertlptr_seq_rect_Type4 h1 h2 h3 hterm in hcut __
168
169(** val ertlptr_seq_inv_rect_Type3 :
170    ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
171    Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __
172    -> 'a1) -> 'a1 **)
173let ertlptr_seq_inv_rect_Type3 hterm h1 h2 h3 =
174  let hcut = ertlptr_seq_rect_Type3 h1 h2 h3 hterm in hcut __
175
176(** val ertlptr_seq_inv_rect_Type2 :
177    ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
178    Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __
179    -> 'a1) -> 'a1 **)
180let ertlptr_seq_inv_rect_Type2 hterm h1 h2 h3 =
181  let hcut = ertlptr_seq_rect_Type2 h1 h2 h3 hterm in hcut __
182
183(** val ertlptr_seq_inv_rect_Type1 :
184    ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
185    Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __
186    -> 'a1) -> 'a1 **)
187let ertlptr_seq_inv_rect_Type1 hterm h1 h2 h3 =
188  let hcut = ertlptr_seq_rect_Type1 h1 h2 h3 hterm in hcut __
189
190(** val ertlptr_seq_inv_rect_Type0 :
191    ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
192    Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __
193    -> 'a1) -> 'a1 **)
194let ertlptr_seq_inv_rect_Type0 hterm h1 h2 h3 =
195  let hcut = ertlptr_seq_rect_Type0 h1 h2 h3 hterm in hcut __
196
197(** val ertlptr_seq_discr : ertlptr_seq -> ertlptr_seq -> __ **)
198let ertlptr_seq_discr x y =
199  Logic.eq_rect_Type2 x
200    (match x with
201     | Ertlptr_ertl a0 -> Obj.magic (fun _ dH -> dH __)
202     | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
203     | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
204
205(** val ertlptr_seq_jmdiscr : ertlptr_seq -> ertlptr_seq -> __ **)
206let ertlptr_seq_jmdiscr x y =
207  Logic.eq_rect_Type2 x
208    (match x with
209     | Ertlptr_ertl a0 -> Obj.magic (fun _ dH -> dH __)
210     | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
211     | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
212
213(** val eRTLptr_uns : Joint.unserialized_params **)
214let eRTLptr_uns =
215  { Joint.ext_seq_labels = (fun s ->
216    match Obj.magic s with
217    | Ertlptr_ertl x -> List.Nil
218    | LOW_ADDRESS (x, l) -> List.Cons (l, List.Nil)
219    | HIGH_ADDRESS (x, l) -> List.Cons (l, List.Nil)); Joint.has_tailcalls =
220    Bool.False }
221
222(** val eRTLptr_functs : Joint.get_pseudo_reg_functs **)
223let eRTLptr_functs =
224  { Joint.acc_a_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
225    Joint.acc_b_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
226    Joint.acc_a_args = (fun arg ->
227    match Obj.magic arg with
228    | Joint.Reg r -> List.Cons (r, List.Nil)
229    | Joint.Imm x -> List.Nil); Joint.acc_b_args = (fun arg ->
230    match Obj.magic arg with
231    | Joint.Reg r -> List.Cons (r, List.Nil)
232    | Joint.Imm x -> List.Nil); Joint.dpl_regs = (fun r -> List.Cons
233    ((Obj.magic r), List.Nil)); Joint.dph_regs = (fun r -> List.Cons
234    ((Obj.magic r), List.Nil)); Joint.dpl_args = (fun arg ->
235    match Obj.magic arg with
236    | Joint.Reg r -> List.Cons (r, List.Nil)
237    | Joint.Imm x -> List.Nil); Joint.dph_args = (fun arg ->
238    match Obj.magic arg with
239    | Joint.Reg r -> List.Cons (r, List.Nil)
240    | Joint.Imm x -> List.Nil); Joint.snd_args = (fun arg ->
241    match Obj.magic arg with
242    | Joint.Reg r -> List.Cons (r, List.Nil)
243    | Joint.Imm x -> List.Nil); Joint.pair_move_regs = (fun x ->
244    List.append (ERTL.regs_from_move_dst (Obj.magic x).Types.fst)
245      (ERTL.regs_from_move_src (Obj.magic x).Types.snd)); Joint.f_call_args =
246    (fun x -> List.Nil); Joint.f_call_dest = (fun x -> List.Nil);
247    Joint.ext_seq_regs = (fun s ->
248    match Obj.magic s with
249    | Ertlptr_ertl s' -> ERTL.ertl_ext_seq_regs s'
250    | LOW_ADDRESS (r, x) -> List.Cons (r, List.Nil)
251    | HIGH_ADDRESS (r, x) -> List.Cons (r, List.Nil)); Joint.params_regs =
252    (fun x -> List.Nil) }
253
254(** val eRTLptr : Joint.graph_params **)
255let eRTLptr =
256  { Joint.u_pars = eRTLptr_uns; Joint.functs = eRTLptr_functs }
257
258type ertlptr_program = Joint.joint_program
259
260(** val ertlptr_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq **)
261let ertlptr_seq_joint =
262  Obj.magic (fun _ x -> Joint.Extension_seq x)
263
264(** val dpi1__o__ertlptr_seq_to_joint_seq__o__inject :
265    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
266    Types.sig0 **)
267let dpi1__o__ertlptr_seq_to_joint_seq__o__inject x1 x2 =
268  ertlptr_seq_joint x1 x2.Types.dpi1
269
270(** val dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
271    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
272    Types.sig0 **)
273let dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
274  Joint.seq_to_step__o__inject
275    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTLptr) x1
276    (ertlptr_seq_joint x1 x2.Types.dpi1)
277
278(** val dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step :
279    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step **)
280let dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step x1 x2 =
281  Joint.Step_seq (ertlptr_seq_joint x1 x2.Types.dpi1)
282
283(** val eject__o__ertlptr_seq_to_joint_seq__o__inject :
284    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0 **)
285let eject__o__ertlptr_seq_to_joint_seq__o__inject x1 x2 =
286  ertlptr_seq_joint x1 (Types.pi1 x2)
287
288(** val eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
289    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0 **)
290let eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
291  Joint.seq_to_step__o__inject
292    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTLptr) x1
293    (ertlptr_seq_joint x1 (Types.pi1 x2))
294
295(** val eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step :
296    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step **)
297let eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step x1 x2 =
298  Joint.Step_seq (ertlptr_seq_joint x1 (Types.pi1 x2))
299
300(** val ertlptr_seq_to_joint_seq__o__seq_to_step :
301    AST.ident List.list -> __ -> Joint.joint_step **)
302let ertlptr_seq_to_joint_seq__o__seq_to_step x0 x1 =
303  Joint.Step_seq (ertlptr_seq_joint x0 x1)
304
305(** val ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
306    AST.ident List.list -> __ -> Joint.joint_step Types.sig0 **)
307let ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x0 x1 =
308  Joint.seq_to_step__o__inject
309    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTLptr) x0
310    (ertlptr_seq_joint x0 x1)
311
312(** val ertlptr_seq_to_joint_seq__o__inject :
313    AST.ident List.list -> __ -> Joint.joint_seq Types.sig0 **)
314let ertlptr_seq_to_joint_seq__o__inject x0 x1 =
315  ertlptr_seq_joint x0 x1
316
317(** val dpi1__o__ertlptr_seq_to_joint_seq :
318    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq **)
319let dpi1__o__ertlptr_seq_to_joint_seq x1 x2 =
320  ertlptr_seq_joint x1 x2.Types.dpi1
321
322(** val eject__o__ertlptr_seq_to_joint_seq :
323    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq **)
324let eject__o__ertlptr_seq_to_joint_seq x1 x2 =
325  ertlptr_seq_joint x1 (Types.pi1 x2)
326
Note: See TracBrowser for help on using the repository browser.