source: extracted/eRTLptr.ml @ 2960

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

New extraction, it diverges in RTL execution now.

File size: 11.9 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open GenMem
12
13open FrontEndMem
14
15open Globalenvs
16
17open String
18
19open Sets
20
21open Listb
22
23open LabelledObjects
24
25open BitVectorTrie
26
27open Graphs
28
29open I8051
30
31open Order
32
33open Registers
34
35open CostLabel
36
37open Hide
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Exp
64
65open Arithmetic
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open Div_and_mod
78
79open Jmeq
80
81open Russell
82
83open List
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Types
92
93open Bool
94
95open Relations
96
97open Nat
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Positive
108
109open Z
110
111open BitVectorZ
112
113open Pointers
114
115open ByteValues
116
117open BackEndOps
118
119open Joint
120
121open ERTL
122
123type ertlptr_seq =
124| Ertlptr_ertl of ERTL.ertl_seq
125| LOW_ADDRESS of Registers.register * Graphs.label
126| HIGH_ADDRESS of Registers.register * Graphs.label
127
128(** val ertlptr_seq_rect_Type4 :
129    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
130    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
131let rec ertlptr_seq_rect_Type4 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
132| Ertlptr_ertl x_141 -> h_ertlptr_ertl x_141
133| LOW_ADDRESS (x_143, x_142) -> h_LOW_ADDRESS x_143 x_142
134| HIGH_ADDRESS (x_145, x_144) -> h_HIGH_ADDRESS x_145 x_144
135
136(** val ertlptr_seq_rect_Type5 :
137    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
138    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
139let rec ertlptr_seq_rect_Type5 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
140| Ertlptr_ertl x_150 -> h_ertlptr_ertl x_150
141| LOW_ADDRESS (x_152, x_151) -> h_LOW_ADDRESS x_152 x_151
142| HIGH_ADDRESS (x_154, x_153) -> h_HIGH_ADDRESS x_154 x_153
143
144(** val ertlptr_seq_rect_Type3 :
145    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
146    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
147let rec ertlptr_seq_rect_Type3 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
148| Ertlptr_ertl x_159 -> h_ertlptr_ertl x_159
149| LOW_ADDRESS (x_161, x_160) -> h_LOW_ADDRESS x_161 x_160
150| HIGH_ADDRESS (x_163, x_162) -> h_HIGH_ADDRESS x_163 x_162
151
152(** val ertlptr_seq_rect_Type2 :
153    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
154    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
155let rec ertlptr_seq_rect_Type2 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
156| Ertlptr_ertl x_168 -> h_ertlptr_ertl x_168
157| LOW_ADDRESS (x_170, x_169) -> h_LOW_ADDRESS x_170 x_169
158| HIGH_ADDRESS (x_172, x_171) -> h_HIGH_ADDRESS x_172 x_171
159
160(** val ertlptr_seq_rect_Type1 :
161    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
162    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
163let rec ertlptr_seq_rect_Type1 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
164| Ertlptr_ertl x_177 -> h_ertlptr_ertl x_177
165| LOW_ADDRESS (x_179, x_178) -> h_LOW_ADDRESS x_179 x_178
166| HIGH_ADDRESS (x_181, x_180) -> h_HIGH_ADDRESS x_181 x_180
167
168(** val ertlptr_seq_rect_Type0 :
169    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
170    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
171let rec ertlptr_seq_rect_Type0 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
172| Ertlptr_ertl x_186 -> h_ertlptr_ertl x_186
173| LOW_ADDRESS (x_188, x_187) -> h_LOW_ADDRESS x_188 x_187
174| HIGH_ADDRESS (x_190, x_189) -> h_HIGH_ADDRESS x_190 x_189
175
176(** val ertlptr_seq_inv_rect_Type4 :
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_Type4 hterm h1 h2 h3 =
181  let hcut = ertlptr_seq_rect_Type4 h1 h2 h3 hterm in hcut __
182
183(** val ertlptr_seq_inv_rect_Type3 :
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_Type3 hterm h1 h2 h3 =
188  let hcut = ertlptr_seq_rect_Type3 h1 h2 h3 hterm in hcut __
189
190(** val ertlptr_seq_inv_rect_Type2 :
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_Type2 hterm h1 h2 h3 =
195  let hcut = ertlptr_seq_rect_Type2 h1 h2 h3 hterm in hcut __
196
197(** val ertlptr_seq_inv_rect_Type1 :
198    ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
199    Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __
200    -> 'a1) -> 'a1 **)
201let ertlptr_seq_inv_rect_Type1 hterm h1 h2 h3 =
202  let hcut = ertlptr_seq_rect_Type1 h1 h2 h3 hterm in hcut __
203
204(** val ertlptr_seq_inv_rect_Type0 :
205    ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
206    Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __
207    -> 'a1) -> 'a1 **)
208let ertlptr_seq_inv_rect_Type0 hterm h1 h2 h3 =
209  let hcut = ertlptr_seq_rect_Type0 h1 h2 h3 hterm in hcut __
210
211(** val ertlptr_seq_discr : ertlptr_seq -> ertlptr_seq -> __ **)
212let ertlptr_seq_discr x y =
213  Logic.eq_rect_Type2 x
214    (match x with
215     | Ertlptr_ertl a0 -> Obj.magic (fun _ dH -> dH __)
216     | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
217     | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
218
219(** val ertlptr_seq_jmdiscr : ertlptr_seq -> ertlptr_seq -> __ **)
220let ertlptr_seq_jmdiscr x y =
221  Logic.eq_rect_Type2 x
222    (match x with
223     | Ertlptr_ertl a0 -> Obj.magic (fun _ dH -> dH __)
224     | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
225     | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
226
227(** val eRTLptr_uns : Joint.unserialized_params **)
228let eRTLptr_uns =
229  { Joint.ext_seq_labels = (fun s ->
230    match Obj.magic s with
231    | Ertlptr_ertl x -> List.Nil
232    | LOW_ADDRESS (x, l) -> List.Cons (l, List.Nil)
233    | HIGH_ADDRESS (x, l) -> List.Cons (l, List.Nil)); Joint.has_tailcalls =
234    Bool.False }
235
236(** val eRTLptr_functs : Joint.get_pseudo_reg_functs **)
237let eRTLptr_functs =
238  { Joint.acc_a_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
239    Joint.acc_b_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
240    Joint.acc_a_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.acc_b_args = (fun arg ->
244    match Obj.magic arg with
245    | Joint.Reg r -> List.Cons (r, List.Nil)
246    | Joint.Imm x -> List.Nil); Joint.dpl_regs = (fun r -> List.Cons
247    ((Obj.magic r), List.Nil)); Joint.dph_regs = (fun r -> List.Cons
248    ((Obj.magic r), List.Nil)); Joint.dpl_args = (fun arg ->
249    match Obj.magic arg with
250    | Joint.Reg r -> List.Cons (r, List.Nil)
251    | Joint.Imm x -> List.Nil); Joint.dph_args = (fun arg ->
252    match Obj.magic arg with
253    | Joint.Reg r -> List.Cons (r, List.Nil)
254    | Joint.Imm x -> List.Nil); Joint.snd_args = (fun arg ->
255    match Obj.magic arg with
256    | Joint.Reg r -> List.Cons (r, List.Nil)
257    | Joint.Imm x -> List.Nil); Joint.pair_move_regs = (fun x ->
258    List.append (ERTL.regs_from_move_dst (Obj.magic x).Types.fst)
259      (ERTL.regs_from_move_src (Obj.magic x).Types.snd)); Joint.f_call_args =
260    (fun x -> List.Nil); Joint.f_call_dest = (fun x -> List.Nil);
261    Joint.ext_seq_regs = (fun s ->
262    match Obj.magic s with
263    | Ertlptr_ertl s' -> ERTL.ertl_ext_seq_regs s'
264    | LOW_ADDRESS (r, x) -> List.Cons (r, List.Nil)
265    | HIGH_ADDRESS (r, x) -> List.Cons (r, List.Nil)); Joint.params_regs =
266    (fun x -> List.Nil) }
267
268(** val eRTLptr : Joint.graph_params **)
269let eRTLptr =
270  { Joint.u_pars = eRTLptr_uns; Joint.functs = eRTLptr_functs }
271
272type ertlptr_program = Joint.joint_program
273
274(** val ertlptr_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq **)
275let ertlptr_seq_joint =
276  Obj.magic (fun _ x -> Joint.Extension_seq x)
277
278(** val dpi1__o__ertlptr_seq_to_joint_seq__o__inject :
279    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
280    Types.sig0 **)
281let dpi1__o__ertlptr_seq_to_joint_seq__o__inject x1 x2 =
282  ertlptr_seq_joint x1 x2.Types.dpi1
283
284(** val dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
285    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
286    Types.sig0 **)
287let dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
288  Joint.seq_to_step__o__inject
289    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTLptr) x1
290    (ertlptr_seq_joint x1 x2.Types.dpi1)
291
292(** val dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step :
293    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step **)
294let dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step x1 x2 =
295  Joint.Step_seq (ertlptr_seq_joint x1 x2.Types.dpi1)
296
297(** val eject__o__ertlptr_seq_to_joint_seq__o__inject :
298    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0 **)
299let eject__o__ertlptr_seq_to_joint_seq__o__inject x1 x2 =
300  ertlptr_seq_joint x1 (Types.pi1 x2)
301
302(** val eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
303    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0 **)
304let eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
305  Joint.seq_to_step__o__inject
306    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTLptr) x1
307    (ertlptr_seq_joint x1 (Types.pi1 x2))
308
309(** val eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step :
310    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step **)
311let eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step x1 x2 =
312  Joint.Step_seq (ertlptr_seq_joint x1 (Types.pi1 x2))
313
314(** val ertlptr_seq_to_joint_seq__o__seq_to_step :
315    AST.ident List.list -> __ -> Joint.joint_step **)
316let ertlptr_seq_to_joint_seq__o__seq_to_step x0 x1 =
317  Joint.Step_seq (ertlptr_seq_joint x0 x1)
318
319(** val ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
320    AST.ident List.list -> __ -> Joint.joint_step Types.sig0 **)
321let ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x0 x1 =
322  Joint.seq_to_step__o__inject
323    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTLptr) x0
324    (ertlptr_seq_joint x0 x1)
325
326(** val ertlptr_seq_to_joint_seq__o__inject :
327    AST.ident List.list -> __ -> Joint.joint_seq Types.sig0 **)
328let ertlptr_seq_to_joint_seq__o__inject x0 x1 =
329  ertlptr_seq_joint x0 x1
330
331(** val dpi1__o__ertlptr_seq_to_joint_seq :
332    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq **)
333let dpi1__o__ertlptr_seq_to_joint_seq x1 x2 =
334  ertlptr_seq_joint x1 x2.Types.dpi1
335
336(** val eject__o__ertlptr_seq_to_joint_seq :
337    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq **)
338let eject__o__ertlptr_seq_to_joint_seq x1 x2 =
339  ertlptr_seq_joint x1 (Types.pi1 x2)
340
341(** val eRTLptr_premain :
342    ertlptr_program -> Joint.joint_closed_internal_function **)
343let eRTLptr_premain p =
344  let l1 = Positive.One in
345  let l2 = Positive.P0 Positive.One in
346  let l3 = Positive.P1 Positive.One in
347  let res = { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0
348    Positive.One)); Joint.joint_if_runiverse = Positive.One;
349    Joint.joint_if_result = (Obj.magic Types.It); Joint.joint_if_params =
350    (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))));
351    Joint.joint_if_stacksize = Nat.O; Joint.joint_if_local_stacksize = Nat.O;
352    Joint.joint_if_code =
353    (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
354    Joint.joint_if_entry = (Obj.magic l1) }
355  in
356  let res0 =
357    Joint.add_graph eRTLptr (AST.prog_var_names p.Joint.joint_prog) l1
358      (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
359      (Obj.magic l2))) res
360  in
361  let res1 =
362    Joint.add_graph eRTLptr (AST.prog_var_names p.Joint.joint_prog) l2
363      (Joint.Sequential ((Joint.CALL ((Types.Inl
364      p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
365      (Obj.magic Types.It))), (Obj.magic l3))) res0
366  in
367  let res2 =
368    Joint.add_graph eRTLptr (AST.prog_var_names p.Joint.joint_prog) l3
369      (Joint.Final (Joint.GOTO l3)) res1
370  in
371  res2
372
Note: See TracBrowser for help on using the repository browser.