source: extracted/rTL_semantics.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: 28.1 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 reg_sp = { reg_sp_env : ByteValues.beval Identifiers.identifier_map;
154                stackp : ByteValues.xpointer }
155
156(** val reg_sp_rect_Type4 :
157    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
158    'a1) -> reg_sp -> 'a1 **)
159let rec reg_sp_rect_Type4 h_mk_reg_sp x_6032 =
160  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6032 in
161  h_mk_reg_sp reg_sp_env0 stackp0
162
163(** val reg_sp_rect_Type5 :
164    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
165    'a1) -> reg_sp -> 'a1 **)
166let rec reg_sp_rect_Type5 h_mk_reg_sp x_6034 =
167  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6034 in
168  h_mk_reg_sp reg_sp_env0 stackp0
169
170(** val reg_sp_rect_Type3 :
171    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
172    'a1) -> reg_sp -> 'a1 **)
173let rec reg_sp_rect_Type3 h_mk_reg_sp x_6036 =
174  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6036 in
175  h_mk_reg_sp reg_sp_env0 stackp0
176
177(** val reg_sp_rect_Type2 :
178    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
179    'a1) -> reg_sp -> 'a1 **)
180let rec reg_sp_rect_Type2 h_mk_reg_sp x_6038 =
181  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6038 in
182  h_mk_reg_sp reg_sp_env0 stackp0
183
184(** val reg_sp_rect_Type1 :
185    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
186    'a1) -> reg_sp -> 'a1 **)
187let rec reg_sp_rect_Type1 h_mk_reg_sp x_6040 =
188  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6040 in
189  h_mk_reg_sp reg_sp_env0 stackp0
190
191(** val reg_sp_rect_Type0 :
192    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
193    'a1) -> reg_sp -> 'a1 **)
194let rec reg_sp_rect_Type0 h_mk_reg_sp x_6042 =
195  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6042 in
196  h_mk_reg_sp reg_sp_env0 stackp0
197
198(** val reg_sp_env :
199    reg_sp -> ByteValues.beval Identifiers.identifier_map **)
200let rec reg_sp_env xxx =
201  xxx.reg_sp_env
202
203(** val stackp : reg_sp -> ByteValues.xpointer **)
204let rec stackp xxx =
205  xxx.stackp
206
207(** val reg_sp_inv_rect_Type4 :
208    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
209    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
210let reg_sp_inv_rect_Type4 hterm h1 =
211  let hcut = reg_sp_rect_Type4 h1 hterm in hcut __
212
213(** val reg_sp_inv_rect_Type3 :
214    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
215    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
216let reg_sp_inv_rect_Type3 hterm h1 =
217  let hcut = reg_sp_rect_Type3 h1 hterm in hcut __
218
219(** val reg_sp_inv_rect_Type2 :
220    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
221    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
222let reg_sp_inv_rect_Type2 hterm h1 =
223  let hcut = reg_sp_rect_Type2 h1 hterm in hcut __
224
225(** val reg_sp_inv_rect_Type1 :
226    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
227    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
228let reg_sp_inv_rect_Type1 hterm h1 =
229  let hcut = reg_sp_rect_Type1 h1 hterm in hcut __
230
231(** val reg_sp_inv_rect_Type0 :
232    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
233    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
234let reg_sp_inv_rect_Type0 hterm h1 =
235  let hcut = reg_sp_rect_Type0 h1 hterm in hcut __
236
237(** val reg_sp_discr : reg_sp -> reg_sp -> __ **)
238let reg_sp_discr x y =
239  Logic.eq_rect_Type2 x
240    (let { reg_sp_env = a0; stackp = a1 } = x in
241    Obj.magic (fun _ dH -> dH __ __)) y
242
243(** val reg_sp_jmdiscr : reg_sp -> reg_sp -> __ **)
244let reg_sp_jmdiscr x y =
245  Logic.eq_rect_Type2 x
246    (let { reg_sp_env = a0; stackp = a1 } = x in
247    Obj.magic (fun _ dH -> dH __ __)) y
248
249(** val dpi1__o__reg_sp_env__o__inject :
250    (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
251    Types.sig0 **)
252let dpi1__o__reg_sp_env__o__inject x2 =
253  x2.Types.dpi1.reg_sp_env
254
255(** val eject__o__reg_sp_env__o__inject :
256    reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map
257    Types.sig0 **)
258let eject__o__reg_sp_env__o__inject x2 =
259  (Types.pi1 x2).reg_sp_env
260
261(** val reg_sp_env__o__inject :
262    reg_sp -> ByteValues.beval Identifiers.identifier_map Types.sig0 **)
263let reg_sp_env__o__inject x1 =
264  x1.reg_sp_env
265
266(** val dpi1__o__reg_sp_env :
267    (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map **)
268let dpi1__o__reg_sp_env x1 =
269  x1.Types.dpi1.reg_sp_env
270
271(** val eject__o__reg_sp_env :
272    reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map **)
273let eject__o__reg_sp_env x1 =
274  (Types.pi1 x1).reg_sp_env
275
276(** val reg_sp_store :
277    PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp **)
278let reg_sp_store reg v locals =
279  let locals' = SemanticsUtils.reg_store reg v locals.reg_sp_env in
280  { reg_sp_env = locals'; stackp = locals.stackp }
281
282(** val reg_sp_retrieve :
283    reg_sp -> Registers.register -> ByteValues.beval Errors.res **)
284let reg_sp_retrieve locals =
285  SemanticsUtils.reg_retrieve locals.reg_sp_env
286
287(** val reg_sp_empty : ByteValues.xpointer -> reg_sp **)
288let reg_sp_empty x =
289  { reg_sp_env = (Identifiers.empty_map PreIdentifiers.RegisterTag); stackp =
290    x }
291
292type frame = { fr_ret_regs : Registers.register List.list;
293               fr_pc : ByteValues.program_counter;
294               fr_carry : ByteValues.bebit; fr_regs : reg_sp }
295
296(** val frame_rect_Type4 :
297    (Registers.register List.list -> ByteValues.program_counter ->
298    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
299let rec frame_rect_Type4 h_mk_frame x_6058 =
300  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
301    fr_regs = fr_regs0 } = x_6058
302  in
303  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
304
305(** val frame_rect_Type5 :
306    (Registers.register List.list -> ByteValues.program_counter ->
307    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
308let rec frame_rect_Type5 h_mk_frame x_6060 =
309  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
310    fr_regs = fr_regs0 } = x_6060
311  in
312  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
313
314(** val frame_rect_Type3 :
315    (Registers.register List.list -> ByteValues.program_counter ->
316    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
317let rec frame_rect_Type3 h_mk_frame x_6062 =
318  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
319    fr_regs = fr_regs0 } = x_6062
320  in
321  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
322
323(** val frame_rect_Type2 :
324    (Registers.register List.list -> ByteValues.program_counter ->
325    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
326let rec frame_rect_Type2 h_mk_frame x_6064 =
327  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
328    fr_regs = fr_regs0 } = x_6064
329  in
330  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
331
332(** val frame_rect_Type1 :
333    (Registers.register List.list -> ByteValues.program_counter ->
334    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
335let rec frame_rect_Type1 h_mk_frame x_6066 =
336  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
337    fr_regs = fr_regs0 } = x_6066
338  in
339  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
340
341(** val frame_rect_Type0 :
342    (Registers.register List.list -> ByteValues.program_counter ->
343    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
344let rec frame_rect_Type0 h_mk_frame x_6068 =
345  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
346    fr_regs = fr_regs0 } = x_6068
347  in
348  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
349
350(** val fr_ret_regs : frame -> Registers.register List.list **)
351let rec fr_ret_regs xxx =
352  xxx.fr_ret_regs
353
354(** val fr_pc : frame -> ByteValues.program_counter **)
355let rec fr_pc xxx =
356  xxx.fr_pc
357
358(** val fr_carry : frame -> ByteValues.bebit **)
359let rec fr_carry xxx =
360  xxx.fr_carry
361
362(** val fr_regs : frame -> reg_sp **)
363let rec fr_regs xxx =
364  xxx.fr_regs
365
366(** val frame_inv_rect_Type4 :
367    frame -> (Registers.register List.list -> ByteValues.program_counter ->
368    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
369let frame_inv_rect_Type4 hterm h1 =
370  let hcut = frame_rect_Type4 h1 hterm in hcut __
371
372(** val frame_inv_rect_Type3 :
373    frame -> (Registers.register List.list -> ByteValues.program_counter ->
374    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
375let frame_inv_rect_Type3 hterm h1 =
376  let hcut = frame_rect_Type3 h1 hterm in hcut __
377
378(** val frame_inv_rect_Type2 :
379    frame -> (Registers.register List.list -> ByteValues.program_counter ->
380    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
381let frame_inv_rect_Type2 hterm h1 =
382  let hcut = frame_rect_Type2 h1 hterm in hcut __
383
384(** val frame_inv_rect_Type1 :
385    frame -> (Registers.register List.list -> ByteValues.program_counter ->
386    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
387let frame_inv_rect_Type1 hterm h1 =
388  let hcut = frame_rect_Type1 h1 hterm in hcut __
389
390(** val frame_inv_rect_Type0 :
391    frame -> (Registers.register List.list -> ByteValues.program_counter ->
392    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
393let frame_inv_rect_Type0 hterm h1 =
394  let hcut = frame_rect_Type0 h1 hterm in hcut __
395
396(** val frame_discr : frame -> frame -> __ **)
397let frame_discr x y =
398  Logic.eq_rect_Type2 x
399    (let { fr_ret_regs = a0; fr_pc = a1; fr_carry = a2; fr_regs = a3 } = x in
400    Obj.magic (fun _ dH -> dH __ __ __ __)) y
401
402(** val frame_jmdiscr : frame -> frame -> __ **)
403let frame_jmdiscr x y =
404  Logic.eq_rect_Type2 x
405    (let { fr_ret_regs = a0; fr_pc = a1; fr_carry = a2; fr_regs = a3 } = x in
406    Obj.magic (fun _ dH -> dH __ __ __ __)) y
407
408(** val rTL_state_params : Joint_semantics.sem_state_params **)
409let rTL_state_params =
410  { Joint_semantics.empty_framesT = (Obj.magic List.Nil);
411    Joint_semantics.empty_regsT = (Obj.magic reg_sp_empty);
412    Joint_semantics.load_sp = (fun env -> Errors.OK (Obj.magic env).stackp);
413    Joint_semantics.save_sp = (fun env ->
414    Obj.magic (fun x -> { reg_sp_env = (Obj.magic env).reg_sp_env; stackp =
415      x })) }
416
417type rTL_state = Joint_semantics.state
418
419(** val rtl_arg_retrieve :
420    reg_sp -> Joint.psd_argument -> ByteValues.beval Errors.res **)
421let rtl_arg_retrieve env = function
422| Joint.Reg r -> SemanticsUtils.reg_retrieve env.reg_sp_env r
423| Joint.Imm b -> Errors.OK (ByteValues.BVByte b)
424
425(** val rtl_fetch_ra :
426    rTL_state -> (rTL_state, ByteValues.program_counter) Types.prod
427    Errors.res **)
428let rtl_fetch_ra st =
429  Obj.magic
430    (Monad.m_bind0 (Monad.max_def Errors.res0)
431      (Obj.magic
432        (Errors.opt_to_res (List.Cons ((Errors.MSG
433          ErrorMessages.FrameErrorOnPop), List.Nil))
434          st.Joint_semantics.st_frms)) (fun frms ->
435      match frms with
436      | List.Nil ->
437        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
438          ErrorMessages.EmptyStack), List.Nil)))
439      | List.Cons (hd, tl) ->
440        Obj.magic (Errors.OK { Types.fst = st; Types.snd = hd.fr_pc })))
441
442(** val rtl_init_local : Registers.register -> reg_sp -> reg_sp **)
443let rtl_init_local local =
444  reg_sp_store local ByteValues.BVundef
445
446(** val rtl_setup_call_separate :
447    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
448    -> rTL_state -> rTL_state Errors.res **)
449let rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st =
450  (let { Types.fst = mem; Types.snd = b } =
451     GenMem.alloc st.Joint_semantics.m (Z.z_of_nat Nat.O)
452       (Z.z_of_nat stacksize)
453   in
454  (fun _ ->
455  let sp = { Pointers.pblock = b; Pointers.poff =
456    (BitVector.zero Pointers.offset_size) }
457  in
458  Obj.magic
459    (Monad.m_bind0 (Monad.max_def Errors.res0)
460      (Obj.magic
461        (Errors.mfold_left2 (fun lenv dest src ->
462          Obj.magic
463            (Monad.m_bind0 (Monad.max_def Errors.res0)
464              (Obj.magic
465                (rtl_arg_retrieve (Obj.magic st.Joint_semantics.regs) src))
466              (fun v -> Obj.magic (Errors.OK (reg_sp_store dest v lenv)))))
467          (Errors.OK (reg_sp_empty sp)) formal_arg_regs actual_arg_regs))
468      (fun new_regs ->
469      Obj.magic (Errors.OK
470        (Joint_semantics.set_regs rTL_state_params new_regs
471          (Joint_semantics.set_m rTL_state_params mem st))))))) __
472
473(** val stackOverflow : ErrorMessages.errorMessage **)
474let stackOverflow = ErrorMessages.MISSING
475
476(** val rtl_setup_call_separate_overflow :
477    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
478    -> rTL_state -> rTL_state Errors.res **)
479let rtl_setup_call_separate_overflow stacksize formal_arg_regs actual_arg_regs st =
480  match Nat.leb (Nat.S (Nat.plus stacksize st.Joint_semantics.stack_usage))
481          (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
482            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
483            (Nat.S (Nat.S Nat.O))))))))))))))))) with
484  | Bool.True ->
485    rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st
486  | Bool.False ->
487    Errors.Error (List.Cons ((Errors.MSG stackOverflow), List.Nil))
488
489(** val rtl_setup_call_unique :
490    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
491    -> rTL_state -> rTL_state Errors.res **)
492let rtl_setup_call_unique stacksize formal_arg_regs actual_arg_regs st =
493  Obj.magic
494    (Monad.m_bind0 (Monad.max_def Errors.res0)
495      (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
496      let newsp =
497        Pointers.neg_shift_pointer (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
498          (Nat.S (Nat.S Nat.O)))))))) (Types.pi1 sp)
499          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
500            (Nat.S (Nat.S (Nat.S Nat.O)))))))) stacksize)
501      in
502      Monad.m_bind0 (Monad.max_def Errors.res0)
503        (Obj.magic
504          (Errors.mfold_left2 (fun lenv dest src ->
505            Obj.magic
506              (Monad.m_bind0 (Monad.max_def Errors.res0)
507                (Obj.magic
508                  (rtl_arg_retrieve (Obj.magic st.Joint_semantics.regs) src))
509                (fun v -> Obj.magic (Errors.OK (reg_sp_store dest v lenv)))))
510            (Errors.OK (reg_sp_empty newsp)) formal_arg_regs actual_arg_regs))
511        (fun new_regs ->
512        Obj.magic (Errors.OK
513          (Joint_semantics.set_regs rTL_state_params new_regs st)))))
514
515type rTL_state_pc = Joint_semantics.state_pc
516
517(** val rtl_save_frame :
518    Registers.register List.list -> rTL_state_pc -> __ **)
519let rtl_save_frame retregs st =
520  Monad.m_bind0 (Monad.max_def Errors.res0)
521    (Obj.magic
522      (Errors.opt_to_res (List.Cons ((Errors.MSG
523        ErrorMessages.FrameErrorOnPush), List.Nil))
524        st.Joint_semantics.st_no_pc.Joint_semantics.st_frms)) (fun frms ->
525    let frame0 = List.Cons ({ fr_ret_regs = retregs; fr_pc =
526      st.Joint_semantics.pc; fr_carry =
527      st.Joint_semantics.st_no_pc.Joint_semantics.carry; fr_regs =
528      (Obj.magic st.Joint_semantics.st_no_pc.Joint_semantics.regs) }, frms)
529    in
530    Obj.magic (Errors.OK
531      (Joint_semantics.set_frms rTL_state_params (Obj.magic frame0)
532        st.Joint_semantics.st_no_pc)))
533
534(** val rtl_fetch_external_args :
535    AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
536    Values.val0 List.list Errors.res **)
537let rtl_fetch_external_args _ = assert false
538
539(** val rtl_set_result :
540    Values.val0 List.list -> Registers.register List.list -> rTL_state ->
541    rTL_state Errors.res **)
542let rtl_set_result _ = assert false
543
544(** val rtl_reg_store :
545    PreIdentifiers.identifier -> ByteValues.beval -> Joint_semantics.state ->
546    Joint_semantics.state **)
547let rtl_reg_store r v st =
548  let mem = reg_sp_store r v (Obj.magic st.Joint_semantics.regs) in
549  Joint_semantics.set_regs rTL_state_params (Obj.magic mem) st
550
551(** val rtl_reg_retrieve :
552    Joint_semantics.state -> Registers.register -> ByteValues.beval
553    Errors.res **)
554let rtl_reg_retrieve st l =
555  reg_sp_retrieve (Obj.magic st.Joint_semantics.regs) l
556
557(** val rtl_read_result :
558    Registers.register List.list -> rTL_state -> ByteValues.beval List.list
559    Errors.res **)
560let rtl_read_result rets st =
561  Obj.magic
562    (Monad.m_list_map (Monad.max_def Errors.res0)
563      (Obj.magic (rtl_reg_retrieve st)) rets)
564
565(** val rtl_pop_frame_separate :
566    Registers.register List.list -> rTL_state -> (rTL_state,
567    ByteValues.program_counter) Types.prod Errors.res **)
568let rtl_pop_frame_separate ret st =
569  Obj.magic
570    (Monad.m_bind0 (Monad.max_def Errors.res0)
571      (Obj.magic
572        (Errors.opt_to_res (List.Cons ((Errors.MSG
573          ErrorMessages.FrameErrorOnPop), List.Nil))
574          st.Joint_semantics.st_frms)) (fun frms ->
575      match frms with
576      | List.Nil ->
577        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
578          ErrorMessages.EmptyStack), List.Nil)))
579      | List.Cons (hd, tl) ->
580        Monad.m_bind0 (Monad.max_def Errors.res0)
581          (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
582          let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
583          Monad.m_bind0 (Monad.max_def Errors.res0)
584            (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
585            let st0 =
586              Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
587                (Joint_semantics.set_regs rTL_state_params
588                  (Obj.magic hd.fr_regs)
589                  (Joint_semantics.set_carry rTL_state_params hd.fr_carry
590                    (Joint_semantics.set_m rTL_state_params
591                      (GenMem.free st.Joint_semantics.m
592                        (Types.pi1 sp).Pointers.pblock) st)))
593            in
594            let pc = hd.fr_pc in
595            let st1 =
596              Util.foldl (fun st1 reg_val ->
597                rtl_reg_store reg_val.Types.fst reg_val.Types.snd st1) st0
598                reg_vals
599            in
600            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
601              Types.snd = pc }))))
602
603(** val rtl_pop_frame_unique :
604    Registers.register List.list -> rTL_state -> (rTL_state,
605    ByteValues.program_counter) Types.prod Errors.res **)
606let rtl_pop_frame_unique ret st =
607  Obj.magic
608    (Monad.m_bind0 (Monad.max_def Errors.res0)
609      (Obj.magic
610        (Errors.opt_to_res (List.Cons ((Errors.MSG
611          ErrorMessages.FrameErrorOnPop), List.Nil))
612          st.Joint_semantics.st_frms)) (fun frms ->
613      match frms with
614      | List.Nil ->
615        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
616          ErrorMessages.EmptyStack), List.Nil)))
617      | List.Cons (hd, tl) ->
618        Monad.m_bind0 (Monad.max_def Errors.res0)
619          (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
620          let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
621          Monad.m_bind0 (Monad.max_def Errors.res0)
622            (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
623            let st0 =
624              Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
625                (Joint_semantics.set_regs rTL_state_params
626                  (Obj.magic hd.fr_regs)
627                  (Joint_semantics.set_carry rTL_state_params hd.fr_carry st))
628            in
629            let pc = hd.fr_pc in
630            let st1 =
631              Util.foldl (fun st1 reg_val ->
632                rtl_reg_store reg_val.Types.fst reg_val.Types.snd st1) st0
633                reg_vals
634            in
635            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
636              Types.snd = pc }))))
637
638(** val block_of_register_pair :
639    Registers.register -> Registers.register -> rTL_state -> Pointers.block
640    Errors.res **)
641let block_of_register_pair r1 r2 st =
642  Obj.magic
643    (Monad.m_bind0 (Monad.max_def Errors.res0)
644      (Obj.magic (rtl_reg_retrieve st r1)) (fun v1 ->
645      Monad.m_bind0 (Monad.max_def Errors.res0)
646        (Obj.magic (rtl_reg_retrieve st r2)) (fun v2 ->
647        Monad.m_bind0 (Monad.max_def Errors.res0)
648          (Obj.magic
649            (BEMem.pointer_of_address { Types.fst = v1; Types.snd = v2 }))
650          (fun ptr -> Obj.magic (Errors.OK ptr.Pointers.pblock)))))
651
652(** val eval_rtl_seq :
653    RTL.rtl_seq -> AST.ident -> rTL_state -> rTL_state Errors.res **)
654let eval_rtl_seq stm curr_fn st =
655  let RTL.Rtl_stack_address (dreg1, dreg2) = stm in
656  Obj.magic
657    (Monad.m_bind0 (Monad.max_def Errors.res0)
658      (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
659      let { Types.fst = dpl; Types.snd = dph } =
660        ByteValues.beval_pair_of_pointer (Types.pi1 sp)
661      in
662      let st0 = rtl_reg_store dreg1 dpl st in
663      Monad.m_return0 (Monad.max_def Errors.res0)
664        (rtl_reg_store dreg2 dph st0)))
665
666(** val reg_res_store :
667    PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
668    Errors.res **)
669let reg_res_store r v s =
670  Errors.OK (reg_sp_store r v s)
671
672(** val rTL_semantics_separate : SemanticsUtils.sem_graph_params **)
673let rTL_semantics_separate =
674  { SemanticsUtils.sgp_pars =
675    (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
676    SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
677    rTL_state_params; Joint_semantics.acca_store_ =
678    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
679    (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
680    (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
681    (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
682    (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
683    (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
684    (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
685    (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
686    (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
687    (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
688    (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
689    (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
690    (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
691    (fun env p ->
692    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
693    Obj.magic
694      (Monad.m_bind0 (Monad.max_def Errors.res0)
695        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
696        Monad.m_return0 (Monad.max_def Errors.res0)
697          (reg_sp_store dest v (Obj.magic env)))));
698    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
699    Joint_semantics.setup_call = (Obj.magic rtl_setup_call_separate);
700    Joint_semantics.fetch_external_args =
701    (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
702    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
703    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
704    (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
705      Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
706      ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
707    Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
708    Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
709    Joint_semantics.pop_frame = (fun x x0 x1 ->
710    Obj.magic rtl_pop_frame_separate) });
711    SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }
712
713(** val rTL_semantics_separate_overflow : SemanticsUtils.sem_graph_params **)
714let rTL_semantics_separate_overflow =
715  { SemanticsUtils.sgp_pars =
716    (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
717    SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
718    rTL_state_params; Joint_semantics.acca_store_ =
719    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
720    (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
721    (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
722    (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
723    (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
724    (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
725    (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
726    (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
727    (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
728    (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
729    (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
730    (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
731    (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
732    (fun env p ->
733    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
734    Obj.magic
735      (Monad.m_bind0 (Monad.max_def Errors.res0)
736        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
737        Monad.m_return0 (Monad.max_def Errors.res0)
738          (reg_sp_store dest v (Obj.magic env)))));
739    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
740    Joint_semantics.setup_call =
741    (Obj.magic rtl_setup_call_separate_overflow);
742    Joint_semantics.fetch_external_args =
743    (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
744    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
745    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
746    (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
747      Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
748      ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
749    Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
750    Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
751    Joint_semantics.pop_frame = (fun x x0 x1 ->
752    Obj.magic rtl_pop_frame_separate) });
753    SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }
754
755(** val rTL_semantics_unique : SemanticsUtils.sem_graph_params **)
756let rTL_semantics_unique =
757  { SemanticsUtils.sgp_pars =
758    (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
759    SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
760    rTL_state_params; Joint_semantics.acca_store_ =
761    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
762    (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
763    (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
764    (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
765    (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
766    (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
767    (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
768    (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
769    (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
770    (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
771    (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
772    (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
773    (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
774    (fun env p ->
775    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
776    Obj.magic
777      (Monad.m_bind0 (Monad.max_def Errors.res0)
778        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
779        Monad.m_return0 (Monad.max_def Errors.res0)
780          (reg_sp_store dest v (Obj.magic env)))));
781    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
782    Joint_semantics.setup_call = (Obj.magic rtl_setup_call_unique);
783    Joint_semantics.fetch_external_args =
784    (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
785    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
786    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
787    (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
788      Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
789      ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
790    Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
791    Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
792    Joint_semantics.pop_frame = (fun x x0 x1 ->
793    Obj.magic rtl_pop_frame_unique) });
794    SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }
795
Note: See TracBrowser for help on using the repository browser.