source: extracted/joint_LTL_LIN.ml @ 2817

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

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File size: 13.4 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open BitVectorTrie
12
13open Graphs
14
15open I8051
16
17open Order
18
19open Registers
20
21open CostLabel
22
23open Hide
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Lists
40
41open Identifiers
42
43open Integers
44
45open AST
46
47open Division
48
49open Exp
50
51open Arithmetic
52
53open Setoids
54
55open Monad
56
57open Option
58
59open Extranat
60
61open Vector
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open List
70
71open Util
72
73open FoldStuff
74
75open BitVector
76
77open Types
78
79open Bool
80
81open Relations
82
83open Nat
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107type registers_move =
108| From_acc of I8051.register * Types.unit0
109| To_acc of Types.unit0 * I8051.register
110| Int_to_reg of I8051.register * BitVector.byte
111| Int_to_acc of Types.unit0 * BitVector.byte
112
113(** val registers_move_rect_Type4 :
114    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
115    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
116    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
117let rec registers_move_rect_Type4 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
118| From_acc (x_21377, x_21376) -> h_from_acc x_21377 x_21376
119| To_acc (x_21379, x_21378) -> h_to_acc x_21379 x_21378
120| Int_to_reg (x_21381, x_21380) -> h_int_to_reg x_21381 x_21380
121| Int_to_acc (x_21383, x_21382) -> h_int_to_acc x_21383 x_21382
122
123(** val registers_move_rect_Type5 :
124    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
125    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
126    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
127let rec registers_move_rect_Type5 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
128| From_acc (x_21390, x_21389) -> h_from_acc x_21390 x_21389
129| To_acc (x_21392, x_21391) -> h_to_acc x_21392 x_21391
130| Int_to_reg (x_21394, x_21393) -> h_int_to_reg x_21394 x_21393
131| Int_to_acc (x_21396, x_21395) -> h_int_to_acc x_21396 x_21395
132
133(** val registers_move_rect_Type3 :
134    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
135    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
136    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
137let rec registers_move_rect_Type3 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
138| From_acc (x_21403, x_21402) -> h_from_acc x_21403 x_21402
139| To_acc (x_21405, x_21404) -> h_to_acc x_21405 x_21404
140| Int_to_reg (x_21407, x_21406) -> h_int_to_reg x_21407 x_21406
141| Int_to_acc (x_21409, x_21408) -> h_int_to_acc x_21409 x_21408
142
143(** val registers_move_rect_Type2 :
144    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
145    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
146    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
147let rec registers_move_rect_Type2 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
148| From_acc (x_21416, x_21415) -> h_from_acc x_21416 x_21415
149| To_acc (x_21418, x_21417) -> h_to_acc x_21418 x_21417
150| Int_to_reg (x_21420, x_21419) -> h_int_to_reg x_21420 x_21419
151| Int_to_acc (x_21422, x_21421) -> h_int_to_acc x_21422 x_21421
152
153(** val registers_move_rect_Type1 :
154    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
155    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
156    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
157let rec registers_move_rect_Type1 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
158| From_acc (x_21429, x_21428) -> h_from_acc x_21429 x_21428
159| To_acc (x_21431, x_21430) -> h_to_acc x_21431 x_21430
160| Int_to_reg (x_21433, x_21432) -> h_int_to_reg x_21433 x_21432
161| Int_to_acc (x_21435, x_21434) -> h_int_to_acc x_21435 x_21434
162
163(** val registers_move_rect_Type0 :
164    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
165    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
166    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
167let rec registers_move_rect_Type0 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
168| From_acc (x_21442, x_21441) -> h_from_acc x_21442 x_21441
169| To_acc (x_21444, x_21443) -> h_to_acc x_21444 x_21443
170| Int_to_reg (x_21446, x_21445) -> h_int_to_reg x_21446 x_21445
171| Int_to_acc (x_21448, x_21447) -> h_int_to_acc x_21448 x_21447
172
173(** val registers_move_inv_rect_Type4 :
174    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
175    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
176    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
177    'a1) -> 'a1 **)
178let registers_move_inv_rect_Type4 hterm h1 h2 h3 h4 =
179  let hcut = registers_move_rect_Type4 h1 h2 h3 h4 hterm in hcut __
180
181(** val registers_move_inv_rect_Type3 :
182    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
183    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
184    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
185    'a1) -> 'a1 **)
186let registers_move_inv_rect_Type3 hterm h1 h2 h3 h4 =
187  let hcut = registers_move_rect_Type3 h1 h2 h3 h4 hterm in hcut __
188
189(** val registers_move_inv_rect_Type2 :
190    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
191    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
192    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
193    'a1) -> 'a1 **)
194let registers_move_inv_rect_Type2 hterm h1 h2 h3 h4 =
195  let hcut = registers_move_rect_Type2 h1 h2 h3 h4 hterm in hcut __
196
197(** val registers_move_inv_rect_Type1 :
198    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
199    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
200    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
201    'a1) -> 'a1 **)
202let registers_move_inv_rect_Type1 hterm h1 h2 h3 h4 =
203  let hcut = registers_move_rect_Type1 h1 h2 h3 h4 hterm in hcut __
204
205(** val registers_move_inv_rect_Type0 :
206    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
207    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
208    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
209    'a1) -> 'a1 **)
210let registers_move_inv_rect_Type0 hterm h1 h2 h3 h4 =
211  let hcut = registers_move_rect_Type0 h1 h2 h3 h4 hterm in hcut __
212
213(** val registers_move_discr : registers_move -> registers_move -> __ **)
214let registers_move_discr x y =
215  Logic.eq_rect_Type2 x
216    (match x with
217     | From_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
218     | To_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
219     | Int_to_reg (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
220     | Int_to_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
221
222(** val registers_move_jmdiscr : registers_move -> registers_move -> __ **)
223let registers_move_jmdiscr x y =
224  Logic.eq_rect_Type2 x
225    (match x with
226     | From_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
227     | To_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
228     | Int_to_reg (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
229     | Int_to_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
230
231type ltl_lin_seq =
232| SAVE_CARRY
233| RESTORE_CARRY
234| LOW_ADDRESS of I8051.register * Graphs.label
235| HIGH_ADDRESS of I8051.register * Graphs.label
236
237(** val ltl_lin_seq_rect_Type4 :
238    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
239    -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
240let rec ltl_lin_seq_rect_Type4 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
241| SAVE_CARRY -> h_SAVE_CARRY
242| RESTORE_CARRY -> h_RESTORE_CARRY
243| LOW_ADDRESS (x_21542, x_21541) -> h_LOW_ADDRESS x_21542 x_21541
244| HIGH_ADDRESS (x_21544, x_21543) -> h_HIGH_ADDRESS x_21544 x_21543
245
246(** val ltl_lin_seq_rect_Type5 :
247    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
248    -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
249let rec ltl_lin_seq_rect_Type5 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
250| SAVE_CARRY -> h_SAVE_CARRY
251| RESTORE_CARRY -> h_RESTORE_CARRY
252| LOW_ADDRESS (x_21551, x_21550) -> h_LOW_ADDRESS x_21551 x_21550
253| HIGH_ADDRESS (x_21553, x_21552) -> h_HIGH_ADDRESS x_21553 x_21552
254
255(** val ltl_lin_seq_rect_Type3 :
256    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
257    -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
258let rec ltl_lin_seq_rect_Type3 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
259| SAVE_CARRY -> h_SAVE_CARRY
260| RESTORE_CARRY -> h_RESTORE_CARRY
261| LOW_ADDRESS (x_21560, x_21559) -> h_LOW_ADDRESS x_21560 x_21559
262| HIGH_ADDRESS (x_21562, x_21561) -> h_HIGH_ADDRESS x_21562 x_21561
263
264(** val ltl_lin_seq_rect_Type2 :
265    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
266    -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
267let rec ltl_lin_seq_rect_Type2 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
268| SAVE_CARRY -> h_SAVE_CARRY
269| RESTORE_CARRY -> h_RESTORE_CARRY
270| LOW_ADDRESS (x_21569, x_21568) -> h_LOW_ADDRESS x_21569 x_21568
271| HIGH_ADDRESS (x_21571, x_21570) -> h_HIGH_ADDRESS x_21571 x_21570
272
273(** val ltl_lin_seq_rect_Type1 :
274    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
275    -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
276let rec ltl_lin_seq_rect_Type1 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
277| SAVE_CARRY -> h_SAVE_CARRY
278| RESTORE_CARRY -> h_RESTORE_CARRY
279| LOW_ADDRESS (x_21578, x_21577) -> h_LOW_ADDRESS x_21578 x_21577
280| HIGH_ADDRESS (x_21580, x_21579) -> h_HIGH_ADDRESS x_21580 x_21579
281
282(** val ltl_lin_seq_rect_Type0 :
283    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
284    -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
285let rec ltl_lin_seq_rect_Type0 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
286| SAVE_CARRY -> h_SAVE_CARRY
287| RESTORE_CARRY -> h_RESTORE_CARRY
288| LOW_ADDRESS (x_21587, x_21586) -> h_LOW_ADDRESS x_21587 x_21586
289| HIGH_ADDRESS (x_21589, x_21588) -> h_HIGH_ADDRESS x_21589 x_21588
290
291(** val ltl_lin_seq_inv_rect_Type4 :
292    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
293    Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
294    'a1) -> 'a1 **)
295let ltl_lin_seq_inv_rect_Type4 hterm h1 h2 h3 h4 =
296  let hcut = ltl_lin_seq_rect_Type4 h1 h2 h3 h4 hterm in hcut __
297
298(** val ltl_lin_seq_inv_rect_Type3 :
299    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
300    Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
301    'a1) -> 'a1 **)
302let ltl_lin_seq_inv_rect_Type3 hterm h1 h2 h3 h4 =
303  let hcut = ltl_lin_seq_rect_Type3 h1 h2 h3 h4 hterm in hcut __
304
305(** val ltl_lin_seq_inv_rect_Type2 :
306    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
307    Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
308    'a1) -> 'a1 **)
309let ltl_lin_seq_inv_rect_Type2 hterm h1 h2 h3 h4 =
310  let hcut = ltl_lin_seq_rect_Type2 h1 h2 h3 h4 hterm in hcut __
311
312(** val ltl_lin_seq_inv_rect_Type1 :
313    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
314    Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
315    'a1) -> 'a1 **)
316let ltl_lin_seq_inv_rect_Type1 hterm h1 h2 h3 h4 =
317  let hcut = ltl_lin_seq_rect_Type1 h1 h2 h3 h4 hterm in hcut __
318
319(** val ltl_lin_seq_inv_rect_Type0 :
320    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
321    Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
322    'a1) -> 'a1 **)
323let ltl_lin_seq_inv_rect_Type0 hterm h1 h2 h3 h4 =
324  let hcut = ltl_lin_seq_rect_Type0 h1 h2 h3 h4 hterm in hcut __
325
326(** val ltl_lin_seq_discr : ltl_lin_seq -> ltl_lin_seq -> __ **)
327let ltl_lin_seq_discr x y =
328  Logic.eq_rect_Type2 x
329    (match x with
330     | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
331     | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
332     | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
333     | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
334
335(** val ltl_lin_seq_jmdiscr : ltl_lin_seq -> ltl_lin_seq -> __ **)
336let ltl_lin_seq_jmdiscr x y =
337  Logic.eq_rect_Type2 x
338    (match x with
339     | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
340     | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
341     | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
342     | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
343
344(** val ltl_lin_seq_labels : ltl_lin_seq -> Graphs.label List.list **)
345let ltl_lin_seq_labels = function
346| SAVE_CARRY -> List.Nil
347| RESTORE_CARRY -> List.Nil
348| LOW_ADDRESS (x, lbl) -> List.Cons (lbl, List.Nil)
349| HIGH_ADDRESS (x, lbl) -> List.Cons (lbl, List.Nil)
350
351(** val lTL_LIN_uns : Joint.unserialized_params **)
352let lTL_LIN_uns =
353  { Joint.ext_seq_labels = (Obj.magic ltl_lin_seq_labels);
354    Joint.has_tailcalls = Bool.False }
355
356(** val lTL_LIN_functs : Joint.get_pseudo_reg_functs **)
357let lTL_LIN_functs =
358  { Joint.acc_a_regs = (fun x -> List.Nil); Joint.acc_b_regs = (fun x ->
359    List.Nil); Joint.acc_a_args = (fun x -> List.Nil); Joint.acc_b_args =
360    (fun x -> List.Nil); Joint.dpl_regs = (fun x -> List.Nil);
361    Joint.dph_regs = (fun x -> List.Nil); Joint.dpl_args = (fun x ->
362    List.Nil); Joint.dph_args = (fun x -> List.Nil); Joint.snd_args =
363    (fun x -> List.Nil); Joint.pair_move_regs = (fun x -> List.Nil);
364    Joint.f_call_args = (fun x -> List.Nil); Joint.f_call_dest = (fun x ->
365    List.Nil); Joint.ext_seq_regs = (fun x -> List.Nil); Joint.params_regs =
366    (fun x -> List.Nil) }
367
368(** val lTL_LIN : Joint.uns_params **)
369let lTL_LIN =
370  { Joint.u_pars = lTL_LIN_uns; Joint.functs = lTL_LIN_functs }
371
Note: See TracBrowser for help on using the repository browser.