source: driver/extracted/rTLToERTL.mli @ 3106

Last change on this file since 3106 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: 3.9 KB
Line 
1open Preamble
2
3open Order
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open ErrorMessages
12
13open PreIdentifiers
14
15open Errors
16
17open Extralib
18
19open Lists
20
21open Positive
22
23open Identifiers
24
25open Registers
26
27open Exp
28
29open Setoids
30
31open Monad
32
33open Option
34
35open Extranat
36
37open Vector
38
39open Div_and_mod
40
41open Russell
42
43open Types
44
45open List
46
47open Util
48
49open FoldStuff
50
51open BitVector
52
53open Arithmetic
54
55open Jmeq
56
57open Bool
58
59open Hints_declaration
60
61open Core_notation
62
63open Pts
64
65open Logic
66
67open Relations
68
69open Nat
70
71open I8051
72
73open RegisterSet
74
75open Extra_bool
76
77open Coqlib
78
79open Values
80
81open FrontEndVal
82
83open GenMem
84
85open FrontEndMem
86
87open Globalenvs
88
89open String
90
91open Sets
92
93open Listb
94
95open LabelledObjects
96
97open BitVectorTrie
98
99open Graphs
100
101open CostLabel
102
103open Hide
104
105open Integers
106
107open AST
108
109open Division
110
111open Z
112
113open BitVectorZ
114
115open Pointers
116
117open ByteValues
118
119open BackEndOps
120
121open Joint
122
123open RTL
124
125open ERTL
126
127open Deqsets_extra
128
129open State
130
131open Bind_new
132
133open BindLists
134
135open Blocks
136
137open TranslateUtils
138
139val save_hdws :
140  AST.ident List.list -> (Registers.register, I8051.register) Types.prod
141  List.list -> Joint.joint_seq List.list
142
143val restore_hdws :
144  AST.ident List.list -> (Joint.psd_argument, I8051.register) Types.prod
145  List.list -> Joint.joint_seq List.list
146
147val get_params_hdw :
148  AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
149  List.list
150
151val get_param_stack :
152  AST.ident List.list -> Registers.register -> Registers.register ->
153  Registers.register -> Joint.joint_seq List.list
154
155val get_params_stack :
156  AST.ident List.list -> Registers.register -> Registers.register ->
157  Registers.register -> Registers.register List.list -> Joint.joint_seq
158  List.list
159
160val get_params :
161  AST.ident List.list -> Registers.register -> Registers.register ->
162  Registers.register -> Registers.register List.list -> Joint.joint_seq
163  List.list
164
165val save_return :
166  AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
167  List.list
168
169val assign_result : AST.ident List.list -> Joint.joint_seq List.list
170
171val epilogue :
172  AST.ident List.list -> Registers.register List.list -> Registers.register
173  -> Registers.register -> (Registers.register, I8051.register) Types.prod
174  List.list -> Joint.joint_seq List.list Types.sig0
175
176val prologue :
177  AST.ident List.list -> Registers.register List.list -> Registers.register
178  -> Registers.register -> Registers.register -> Registers.register ->
179  Registers.register -> (Registers.register, I8051.register) Types.prod
180  List.list -> (Registers.register, Joint.joint_seq List.list)
181  Bind_new.bind_new
182
183val set_params_hdw :
184  AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
185  List.list
186
187val set_param_stack :
188  AST.ident List.list -> Registers.register -> Registers.register ->
189  Joint.psd_argument -> Joint.joint_seq List.list
190
191val set_params_stack :
192  AST.ident List.list -> Joint.psd_argument List.list -> (Registers.register,
193  Joint.joint_seq List.list) Bind_new.bind_new
194
195val set_params :
196  AST.ident List.list -> Joint.psd_argument List.list -> (Registers.register,
197  Joint.joint_seq List.list) Bind_new.bind_new Types.sig0
198
199val fetch_result :
200  AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
201  List.list Types.sig0
202
203val translate_step :
204  AST.ident List.list -> Graphs.label -> Joint.joint_step ->
205  Blocks.bind_step_block
206
207val translate_fin_step :
208  AST.ident List.list -> Registers.register List.list -> Registers.register
209  -> Registers.register -> (Registers.register, I8051.register) Types.prod
210  List.list -> Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block
211
212val allocate_regs :
213  ((Registers.register, I8051.register) Types.prod List.list ->
214  (Registers.register, 'a1) Bind_new.bind_new) -> (Registers.register, 'a1)
215  Bind_new.bind_new
216
217val translate_data :
218  AST.ident List.list -> Joint.joint_closed_internal_function ->
219  TranslateUtils.bound_b_graph_translate_data
220
221val rtl_to_ertl : RTL.rtl_program -> ERTL.ertl_program
222
Note: See TracBrowser for help on using the repository browser.