source: extracted/rTL.ml @ 2961

Last change on this file since 2961 was 2961, checked in by sacerdot, 5 years ago

Bug fixed (stupid typo in pre-main code made the compiler diverge on RTL
languages).

File size: 9.0 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
121type rtl_seq =
122| Rtl_stack_address of Registers.register * Registers.register
123
124(** val rtl_seq_rect_Type4 :
125    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
126let rec rtl_seq_rect_Type4 h_rtl_stack_address = function
127| Rtl_stack_address (x_7, x_6) -> h_rtl_stack_address x_7 x_6
128
129(** val rtl_seq_rect_Type5 :
130    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
131let rec rtl_seq_rect_Type5 h_rtl_stack_address = function
132| Rtl_stack_address (x_11, x_10) -> h_rtl_stack_address x_11 x_10
133
134(** val rtl_seq_rect_Type3 :
135    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
136let rec rtl_seq_rect_Type3 h_rtl_stack_address = function
137| Rtl_stack_address (x_15, x_14) -> h_rtl_stack_address x_15 x_14
138
139(** val rtl_seq_rect_Type2 :
140    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
141let rec rtl_seq_rect_Type2 h_rtl_stack_address = function
142| Rtl_stack_address (x_19, x_18) -> h_rtl_stack_address x_19 x_18
143
144(** val rtl_seq_rect_Type1 :
145    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
146let rec rtl_seq_rect_Type1 h_rtl_stack_address = function
147| Rtl_stack_address (x_23, x_22) -> h_rtl_stack_address x_23 x_22
148
149(** val rtl_seq_rect_Type0 :
150    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
151let rec rtl_seq_rect_Type0 h_rtl_stack_address = function
152| Rtl_stack_address (x_27, x_26) -> h_rtl_stack_address x_27 x_26
153
154(** val rtl_seq_inv_rect_Type4 :
155    rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
156let rtl_seq_inv_rect_Type4 hterm h1 =
157  let hcut = rtl_seq_rect_Type4 h1 hterm in hcut __
158
159(** val rtl_seq_inv_rect_Type3 :
160    rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
161let rtl_seq_inv_rect_Type3 hterm h1 =
162  let hcut = rtl_seq_rect_Type3 h1 hterm in hcut __
163
164(** val rtl_seq_inv_rect_Type2 :
165    rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
166let rtl_seq_inv_rect_Type2 hterm h1 =
167  let hcut = rtl_seq_rect_Type2 h1 hterm in hcut __
168
169(** val rtl_seq_inv_rect_Type1 :
170    rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
171let rtl_seq_inv_rect_Type1 hterm h1 =
172  let hcut = rtl_seq_rect_Type1 h1 hterm in hcut __
173
174(** val rtl_seq_inv_rect_Type0 :
175    rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
176let rtl_seq_inv_rect_Type0 hterm h1 =
177  let hcut = rtl_seq_rect_Type0 h1 hterm in hcut __
178
179(** val rtl_seq_discr : rtl_seq -> rtl_seq -> __ **)
180let rtl_seq_discr x y =
181  Logic.eq_rect_Type2 x
182    (let Rtl_stack_address (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __))
183    y
184
185(** val rtl_seq_jmdiscr : rtl_seq -> rtl_seq -> __ **)
186let rtl_seq_jmdiscr x y =
187  Logic.eq_rect_Type2 x
188    (let Rtl_stack_address (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __))
189    y
190
191(** val rTL_uns : Joint.unserialized_params **)
192let rTL_uns =
193  { Joint.ext_seq_labels = (fun x -> List.Nil); Joint.has_tailcalls =
194    Bool.False }
195
196(** val rTL_functs : Joint.get_pseudo_reg_functs **)
197let rTL_functs =
198  { Joint.acc_a_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
199    Joint.acc_b_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
200    Joint.acc_a_args = (fun a ->
201    match Obj.magic a with
202    | Joint.Reg r -> List.Cons (r, List.Nil)
203    | Joint.Imm x -> List.Nil); Joint.acc_b_args = (fun a ->
204    match Obj.magic a with
205    | Joint.Reg r -> List.Cons (r, List.Nil)
206    | Joint.Imm x -> List.Nil); Joint.dpl_regs = (fun r -> List.Cons
207    ((Obj.magic r), List.Nil)); Joint.dph_regs = (fun r -> List.Cons
208    ((Obj.magic r), List.Nil)); Joint.dpl_args = (fun a ->
209    match Obj.magic a with
210    | Joint.Reg r -> List.Cons (r, List.Nil)
211    | Joint.Imm x -> List.Nil); Joint.dph_args = (fun a ->
212    match Obj.magic a with
213    | Joint.Reg r -> List.Cons (r, List.Nil)
214    | Joint.Imm x -> List.Nil); Joint.snd_args = (fun a ->
215    match Obj.magic a with
216    | Joint.Reg r -> List.Cons (r, List.Nil)
217    | Joint.Imm x -> List.Nil); Joint.pair_move_regs = (fun x ->
218    List.append (List.Cons ((Obj.magic x).Types.fst, List.Nil))
219      (match (Obj.magic x).Types.snd with
220       | Joint.Reg r -> List.Cons (r, List.Nil)
221       | Joint.Imm x0 -> List.Nil)); Joint.f_call_args = (fun l ->
222    Util.foldl (fun l1 a ->
223      List.append l1
224        (match a with
225         | Joint.Reg r -> List.Cons (r, List.Nil)
226         | Joint.Imm x -> List.Nil)) List.Nil (Obj.magic l));
227    Joint.f_call_dest = (fun x -> Obj.magic x); Joint.ext_seq_regs =
228    (fun ext ->
229    let Rtl_stack_address (r1, r2) = Obj.magic ext in
230    List.Cons (r1, (List.Cons (r2, List.Nil)))); Joint.params_regs =
231    (fun x -> Obj.magic x) }
232
233(** val rTL : Joint.graph_params **)
234let rTL =
235  { Joint.u_pars = rTL_uns; Joint.functs = rTL_functs }
236
237type rtl_program = Joint.joint_program
238
239(** val dpi1__o__reg_to_rtl_snd_argument__o__inject :
240    (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
241let dpi1__o__reg_to_rtl_snd_argument__o__inject x2 =
242  Joint.psd_argument_from_reg x2.Types.dpi1
243
244(** val eject__o__reg_to_rtl_snd_argument__o__inject :
245    Registers.register Types.sig0 -> Joint.psd_argument Types.sig0 **)
246let eject__o__reg_to_rtl_snd_argument__o__inject x2 =
247  Joint.psd_argument_from_reg (Types.pi1 x2)
248
249(** val reg_to_rtl_snd_argument__o__inject :
250    Registers.register -> Joint.psd_argument Types.sig0 **)
251let reg_to_rtl_snd_argument__o__inject x1 =
252  Joint.psd_argument_from_reg x1
253
254(** val dpi1__o__reg_to_rtl_snd_argument :
255    (Registers.register, 'a1) Types.dPair -> Joint.psd_argument **)
256let dpi1__o__reg_to_rtl_snd_argument x1 =
257  Joint.psd_argument_from_reg x1.Types.dpi1
258
259(** val eject__o__reg_to_rtl_snd_argument :
260    Registers.register Types.sig0 -> Joint.psd_argument **)
261let eject__o__reg_to_rtl_snd_argument x1 =
262  Joint.psd_argument_from_reg (Types.pi1 x1)
263
264(** val dpi1__o__byte_to_rtl_snd_argument__o__inject :
265    (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
266let dpi1__o__byte_to_rtl_snd_argument__o__inject x2 =
267  Joint.psd_argument_from_byte x2.Types.dpi1
268
269(** val eject__o__byte_to_rtl_snd_argument__o__inject :
270    BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0 **)
271let eject__o__byte_to_rtl_snd_argument__o__inject x2 =
272  Joint.psd_argument_from_byte (Types.pi1 x2)
273
274(** val byte_to_rtl_snd_argument__o__inject :
275    BitVector.byte -> Joint.psd_argument Types.sig0 **)
276let byte_to_rtl_snd_argument__o__inject x1 =
277  Joint.psd_argument_from_byte x1
278
279(** val dpi1__o__byte_to_rtl_snd_argument :
280    (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument **)
281let dpi1__o__byte_to_rtl_snd_argument x1 =
282  Joint.psd_argument_from_byte x1.Types.dpi1
283
284(** val eject__o__byte_to_rtl_snd_argument :
285    BitVector.byte Types.sig0 -> Joint.psd_argument **)
286let eject__o__byte_to_rtl_snd_argument x1 =
287  Joint.psd_argument_from_byte (Types.pi1 x1)
288
289(** val rTL_premain : rtl_program -> Joint.joint_closed_internal_function **)
290let rTL_premain p =
291  let l1 = Positive.One in
292  let l2 = Positive.P0 Positive.One in
293  let l3 = Positive.P1 Positive.One in
294  let rs = List.Cons (Positive.One, (List.Cons ((Positive.P0 Positive.One),
295    (List.Cons ((Positive.P1 Positive.One), (List.Cons ((Positive.P0
296    (Positive.P0 Positive.One)), List.Nil)))))))
297  in
298  let res = { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0
299    Positive.One)); Joint.joint_if_runiverse = (Positive.P1 (Positive.P0
300    Positive.One)); Joint.joint_if_result = (Obj.magic List.Nil);
301    Joint.joint_if_params = (Obj.magic rs); Joint.joint_if_stacksize = Nat.O;
302    Joint.joint_if_local_stacksize = Nat.O; Joint.joint_if_code =
303    (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
304    Joint.joint_if_entry = (Obj.magic l1) }
305  in
306  let res0 =
307    Joint.add_graph rTL (AST.prog_var_names p.Joint.joint_prog) l1
308      (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
309      (Obj.magic l2))) res
310  in
311  let res1 =
312    Joint.add_graph rTL (AST.prog_var_names p.Joint.joint_prog) l2
313      (Joint.Sequential ((Joint.CALL ((Types.Inl
314      p.Joint.joint_prog.AST.prog_main), (Obj.magic List.Nil),
315      (Obj.magic rs))), (Obj.magic l3))) res0
316  in
317  let res2 =
318    Joint.add_graph rTL (AST.prog_var_names p.Joint.joint_prog) l3
319      (Joint.Final (Joint.GOTO l3)) res1
320  in
321  res2
322
Note: See TracBrowser for help on using the repository browser.