source: extracted/eRTLToERTLptr.ml @ 2951

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 4.6 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
123open ERTLptr
124
125open Deqsets_extra
126
127open State
128
129open Bind_new
130
131open BindLists
132
133open Blocks
134
135open TranslateUtils
136
137(** val seq_embed :
138    AST.ident List.list -> Joint.joint_seq -> Joint.joint_seq **)
139let seq_embed globals = function
140| Joint.COMMENT s0 -> Joint.COMMENT s0
141| Joint.MOVE a -> Joint.MOVE a
142| Joint.POP a -> Joint.POP a
143| Joint.PUSH a -> Joint.PUSH a
144| Joint.ADDRESS (i, reg1, reg2) -> Joint.ADDRESS (i, reg1, reg2)
145| Joint.OPACCS (op, reg1, reg2, reg3, reg4) ->
146  Joint.OPACCS (op, reg1, reg2, reg3, reg4)
147| Joint.OP1 (op, reg1, reg2) -> Joint.OP1 (op, reg1, reg2)
148| Joint.OP2 (op, reg1, reg2, arg) -> Joint.OP2 (op, reg1, reg2, arg)
149| Joint.CLEAR_CARRY -> Joint.CLEAR_CARRY
150| Joint.SET_CARRY -> Joint.SET_CARRY
151| Joint.LOAD (reg1, reg2, reg3) -> Joint.LOAD (reg1, reg2, reg3)
152| Joint.STORE (arg1, arg2, reg) -> Joint.STORE (arg1, arg2, reg)
153| Joint.Extension_seq s0 ->
154  Joint.Extension_seq (Obj.magic (ERTLptr.Ertlptr_ertl (Obj.magic s0)))
155
156(** val translate_step :
157    AST.ident List.list -> Graphs.label -> Joint.joint_step ->
158    Blocks.bind_step_block **)
159let translate_step globals l = function
160| Joint.COST_LABEL c ->
161  Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
162    Joint.COST_LABEL c) }; Types.snd = List.Nil }
163| Joint.CALL (called, args, dest) ->
164  (match called with
165   | Types.Inl id ->
166     Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd =
167       (fun x -> Joint.CALL ((Types.Inl id), args, dest)) }; Types.snd =
168       List.Nil }
169   | Types.Inr dest1 ->
170     Bind_new.Bnew (fun reg -> Bind_new.Bret { Types.fst = { Types.fst =
171       (List.Cons ((fun l0 ->
172       let x =
173         ERTLptr.ertlptr_seq_joint globals
174           (Obj.magic (ERTLptr.LOW_ADDRESS (reg, (Obj.magic l0))))
175       in
176       x), (List.Cons ((fun x -> Joint.PUSH (Obj.magic (Joint.Reg reg))),
177       (List.Cons ((fun l0 ->
178       ERTLptr.ertlptr_seq_joint globals
179         (Obj.magic (ERTLptr.HIGH_ADDRESS (reg, (Obj.magic l0))))),
180       (List.Cons ((fun x -> Joint.PUSH (Obj.magic (Joint.Reg reg))),
181       List.Nil)))))))); Types.snd = (fun x -> Joint.CALL ((Types.Inr dest1),
182       args, dest)) }; Types.snd = List.Nil }))
183| Joint.COND (reg, l0) ->
184  Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
185    Joint.COND (reg, l0)) }; Types.snd = List.Nil }
186| Joint.Step_seq x ->
187  Bind_new.Bret
188    (Blocks.ensure_step_block (Joint.graph_params_to_params ERTLptr.eRTLptr)
189      globals (List.Cons ((seq_embed globals x), List.Nil)))
190
191(** val fin_step_embed : Joint.joint_fin_step -> Joint.joint_fin_step **)
192let fin_step_embed = function
193| Joint.GOTO l -> Joint.GOTO l
194| Joint.RETURN -> Joint.RETURN
195| Joint.TAILCALL (arg, arg') -> Joint.TAILCALL (arg, arg')
196
197(** val translate_fin_step :
198    AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
199    Blocks.bind_fin_block **)
200let translate_fin_step globals l s =
201  Bind_new.Bret { Types.fst = List.Nil; Types.snd = (fin_step_embed s) }
202
203(** val translate_data :
204    AST.ident List.list -> Joint.joint_closed_internal_function ->
205    (Registers.register, TranslateUtils.b_graph_translate_data)
206    Bind_new.bind_new **)
207let translate_data globals def =
208  Bind_new.Bret { TranslateUtils.init_ret =
209    (Types.pi1 def).Joint.joint_if_result; TranslateUtils.init_params =
210    (Types.pi1 def).Joint.joint_if_params; TranslateUtils.init_stack_size =
211    (Types.pi1 def).Joint.joint_if_stacksize; TranslateUtils.added_prologue =
212    List.Nil; TranslateUtils.new_regs = List.Nil; TranslateUtils.f_step =
213    (translate_step globals); TranslateUtils.f_fin =
214    (translate_fin_step globals) }
215
216(** val ertl_to_ertlptr : ERTL.ertl_program -> ERTLptr.ertlptr_program **)
217let ertl_to_ertlptr =
218  TranslateUtils.b_graph_transform_program ERTL.eRTL ERTLptr.eRTLptr
219    (fun globals h -> translate_data globals h)
220
Note: See TracBrowser for help on using the repository browser.