source: extracted/rTL_semantics.mli @ 2829

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

Semantics files committed.

File size: 5.4 KB
Line 
1open Preamble
2
3open ExtraMonads
4
5open Deqsets_extra
6
7open State
8
9open Bind_new
10
11open BindLists
12
13open Blocks
14
15open TranslateUtils
16
17open ExtraGlobalenvs
18
19open I8051bis
20
21open String
22
23open Sets
24
25open Listb
26
27open LabelledObjects
28
29open BitVectorTrie
30
31open Graphs
32
33open I8051
34
35open Order
36
37open Registers
38
39open BackEndOps
40
41open Joint
42
43open BEMem
44
45open CostLabel
46
47open Events
48
49open IOMonad
50
51open IO
52
53open Extra_bool
54
55open Coqlib
56
57open Values
58
59open FrontEndVal
60
61open Hide
62
63open ByteValues
64
65open Division
66
67open Z
68
69open BitVectorZ
70
71open Pointers
72
73open GenMem
74
75open FrontEndMem
76
77open Proper
78
79open PositiveMap
80
81open Deqsets
82
83open Extralib
84
85open Lists
86
87open Identifiers
88
89open Exp
90
91open Arithmetic
92
93open Vector
94
95open Div_and_mod
96
97open Util
98
99open FoldStuff
100
101open BitVector
102
103open Extranat
104
105open Integers
106
107open AST
108
109open ErrorMessages
110
111open Option
112
113open Setoids
114
115open Monad
116
117open Jmeq
118
119open Russell
120
121open Positive
122
123open PreIdentifiers
124
125open Bool
126
127open Relations
128
129open Nat
130
131open List
132
133open Hints_declaration
134
135open Core_notation
136
137open Pts
138
139open Logic
140
141open Types
142
143open Errors
144
145open Globalenvs
146
147open Joint_semantics
148
149open SemanticsUtils
150
151open RTL
152
153type frame = { fr_ret_regs : Registers.register List.list;
154               fr_pc : ByteValues.program_counter;
155               fr_carry : ByteValues.bebit; fr_regs : SemanticsUtils.reg_sp }
156
157val frame_rect_Type4 :
158  (Registers.register List.list -> ByteValues.program_counter ->
159  ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1
160
161val frame_rect_Type5 :
162  (Registers.register List.list -> ByteValues.program_counter ->
163  ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1
164
165val frame_rect_Type3 :
166  (Registers.register List.list -> ByteValues.program_counter ->
167  ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1
168
169val frame_rect_Type2 :
170  (Registers.register List.list -> ByteValues.program_counter ->
171  ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1
172
173val frame_rect_Type1 :
174  (Registers.register List.list -> ByteValues.program_counter ->
175  ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1
176
177val frame_rect_Type0 :
178  (Registers.register List.list -> ByteValues.program_counter ->
179  ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1
180
181val fr_ret_regs : frame -> Registers.register List.list
182
183val fr_pc : frame -> ByteValues.program_counter
184
185val fr_carry : frame -> ByteValues.bebit
186
187val fr_regs : frame -> SemanticsUtils.reg_sp
188
189val frame_inv_rect_Type4 :
190  frame -> (Registers.register List.list -> ByteValues.program_counter ->
191  ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1
192
193val frame_inv_rect_Type3 :
194  frame -> (Registers.register List.list -> ByteValues.program_counter ->
195  ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1
196
197val frame_inv_rect_Type2 :
198  frame -> (Registers.register List.list -> ByteValues.program_counter ->
199  ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1
200
201val frame_inv_rect_Type1 :
202  frame -> (Registers.register List.list -> ByteValues.program_counter ->
203  ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1
204
205val frame_inv_rect_Type0 :
206  frame -> (Registers.register List.list -> ByteValues.program_counter ->
207  ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1
208
209val frame_discr : frame -> frame -> __
210
211val frame_jmdiscr : frame -> frame -> __
212
213val rTL_state_params : Joint_semantics.sem_state_params
214
215type rTL_state = Joint_semantics.state
216
217val rtl_arg_retrieve :
218  SemanticsUtils.reg_sp -> Joint.psd_argument -> ByteValues.beval Errors.res
219
220val rtl_fetch_ra :
221  rTL_state -> (rTL_state, ByteValues.program_counter) Types.prod Errors.res
222
223val rtl_init_local :
224  Registers.register -> SemanticsUtils.reg_sp -> SemanticsUtils.reg_sp
225
226val rtl_setup_call_separate :
227  Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
228  rTL_state -> rTL_state Errors.res
229
230val rtl_setup_call_unique :
231  Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
232  rTL_state -> rTL_state Errors.res
233
234type rTL_state_pc = Joint_semantics.state_pc
235
236val rtl_save_frame : Registers.register List.list -> rTL_state_pc -> __
237
238val rtl_fetch_external_args :
239  AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
240  Values.val0 List.list Errors.res
241
242val rtl_set_result :
243  Values.val0 List.list -> Registers.register List.list -> rTL_state ->
244  rTL_state Errors.res
245
246val rtl_reg_store :
247  PreIdentifiers.identifier -> ByteValues.beval -> Joint_semantics.state ->
248  Joint_semantics.state
249
250val rtl_reg_retrieve :
251  Joint_semantics.state -> Registers.register -> ByteValues.beval Errors.res
252
253val rtl_read_result :
254  Registers.register List.list -> rTL_state -> ByteValues.beval List.list
255  Errors.res
256
257val rtl_pop_frame_separate :
258  Registers.register List.list -> rTL_state -> (rTL_state,
259  ByteValues.program_counter) Types.prod Errors.res
260
261val rtl_pop_frame_unique :
262  Registers.register List.list -> rTL_state -> (rTL_state,
263  ByteValues.program_counter) Types.prod Errors.res
264
265val block_of_register_pair :
266  Registers.register -> Registers.register -> rTL_state -> Pointers.block
267  Errors.res
268
269val eval_rtl_seq :
270  RTL.rtl_seq -> AST.ident -> rTL_state -> rTL_state Errors.res
271
272val reg_res_store :
273  PreIdentifiers.identifier -> ByteValues.beval -> SemanticsUtils.reg_sp ->
274  SemanticsUtils.reg_sp Errors.res
275
276val rTL_semantics_separate : SemanticsUtils.sem_graph_params
277
278val rTL_semantics_unique : SemanticsUtils.sem_graph_params
279
Note: See TracBrowser for help on using the repository browser.