source: extracted/rTL_semantics.ml @ 2829

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

Semantics files committed.

File size: 20.2 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
157(** val frame_rect_Type4 :
158    (Registers.register List.list -> ByteValues.program_counter ->
159    ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
160let rec frame_rect_Type4 h_mk_frame x_3 =
161  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
162    fr_regs = fr_regs0 } = x_3
163  in
164  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
165
166(** val frame_rect_Type5 :
167    (Registers.register List.list -> ByteValues.program_counter ->
168    ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
169let rec frame_rect_Type5 h_mk_frame x_5 =
170  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
171    fr_regs = fr_regs0 } = x_5
172  in
173  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
174
175(** val frame_rect_Type3 :
176    (Registers.register List.list -> ByteValues.program_counter ->
177    ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
178let rec frame_rect_Type3 h_mk_frame x_7 =
179  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
180    fr_regs = fr_regs0 } = x_7
181  in
182  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
183
184(** val frame_rect_Type2 :
185    (Registers.register List.list -> ByteValues.program_counter ->
186    ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
187let rec frame_rect_Type2 h_mk_frame x_9 =
188  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
189    fr_regs = fr_regs0 } = x_9
190  in
191  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
192
193(** val frame_rect_Type1 :
194    (Registers.register List.list -> ByteValues.program_counter ->
195    ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
196let rec frame_rect_Type1 h_mk_frame x_11 =
197  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
198    fr_regs = fr_regs0 } = x_11
199  in
200  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
201
202(** val frame_rect_Type0 :
203    (Registers.register List.list -> ByteValues.program_counter ->
204    ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
205let rec frame_rect_Type0 h_mk_frame x_13 =
206  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
207    fr_regs = fr_regs0 } = x_13
208  in
209  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
210
211(** val fr_ret_regs : frame -> Registers.register List.list **)
212let rec fr_ret_regs xxx =
213  xxx.fr_ret_regs
214
215(** val fr_pc : frame -> ByteValues.program_counter **)
216let rec fr_pc xxx =
217  xxx.fr_pc
218
219(** val fr_carry : frame -> ByteValues.bebit **)
220let rec fr_carry xxx =
221  xxx.fr_carry
222
223(** val fr_regs : frame -> SemanticsUtils.reg_sp **)
224let rec fr_regs xxx =
225  xxx.fr_regs
226
227(** val frame_inv_rect_Type4 :
228    frame -> (Registers.register List.list -> ByteValues.program_counter ->
229    ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1 **)
230let frame_inv_rect_Type4 hterm h1 =
231  let hcut = frame_rect_Type4 h1 hterm in hcut __
232
233(** val frame_inv_rect_Type3 :
234    frame -> (Registers.register List.list -> ByteValues.program_counter ->
235    ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1 **)
236let frame_inv_rect_Type3 hterm h1 =
237  let hcut = frame_rect_Type3 h1 hterm in hcut __
238
239(** val frame_inv_rect_Type2 :
240    frame -> (Registers.register List.list -> ByteValues.program_counter ->
241    ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1 **)
242let frame_inv_rect_Type2 hterm h1 =
243  let hcut = frame_rect_Type2 h1 hterm in hcut __
244
245(** val frame_inv_rect_Type1 :
246    frame -> (Registers.register List.list -> ByteValues.program_counter ->
247    ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1 **)
248let frame_inv_rect_Type1 hterm h1 =
249  let hcut = frame_rect_Type1 h1 hterm in hcut __
250
251(** val frame_inv_rect_Type0 :
252    frame -> (Registers.register List.list -> ByteValues.program_counter ->
253    ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1 **)
254let frame_inv_rect_Type0 hterm h1 =
255  let hcut = frame_rect_Type0 h1 hterm in hcut __
256
257(** val frame_discr : frame -> frame -> __ **)
258let frame_discr x y =
259  Logic.eq_rect_Type2 x
260    (let { fr_ret_regs = a0; fr_pc = a1; fr_carry = a2; fr_regs = a3 } = x in
261    Obj.magic (fun _ dH -> dH __ __ __ __)) y
262
263(** val frame_jmdiscr : frame -> frame -> __ **)
264let frame_jmdiscr x y =
265  Logic.eq_rect_Type2 x
266    (let { fr_ret_regs = a0; fr_pc = a1; fr_carry = a2; fr_regs = a3 } = x in
267    Obj.magic (fun _ dH -> dH __ __ __ __)) y
268
269(** val rTL_state_params : Joint_semantics.sem_state_params **)
270let rTL_state_params =
271  { Joint_semantics.empty_framesT = (Obj.magic List.Nil);
272    Joint_semantics.empty_regsT = (Obj.magic SemanticsUtils.reg_sp_init);
273    Joint_semantics.load_sp = (fun env -> Errors.OK
274    (Obj.magic env).SemanticsUtils.stackp); Joint_semantics.save_sp =
275    (fun env ->
276    Obj.magic (fun x -> { SemanticsUtils.reg_sp_env =
277      (Obj.magic env).SemanticsUtils.reg_sp_env; SemanticsUtils.stackp = x })) }
278
279type rTL_state = Joint_semantics.state
280
281(** val rtl_arg_retrieve :
282    SemanticsUtils.reg_sp -> Joint.psd_argument -> ByteValues.beval
283    Errors.res **)
284let rtl_arg_retrieve env = function
285| Joint.Reg r -> SemanticsUtils.reg_retrieve env.SemanticsUtils.reg_sp_env r
286| Joint.Imm b -> Errors.OK (ByteValues.BVByte b)
287
288(** val rtl_fetch_ra :
289    rTL_state -> (rTL_state, ByteValues.program_counter) Types.prod
290    Errors.res **)
291let rtl_fetch_ra st =
292  Obj.magic
293    (Monad.m_bind0 (Monad.max_def Errors.res0)
294      (Obj.magic
295        (Errors.opt_to_res (List.Cons ((Errors.MSG
296          ErrorMessages.FrameErrorOnPop), List.Nil))
297          st.Joint_semantics.st_frms)) (fun frms ->
298      match frms with
299      | List.Nil ->
300        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
301          ErrorMessages.EmptyStack), List.Nil)))
302      | List.Cons (hd, tl) ->
303        Obj.magic (Errors.OK { Types.fst = st; Types.snd = hd.fr_pc })))
304
305(** val rtl_init_local :
306    Registers.register -> SemanticsUtils.reg_sp -> SemanticsUtils.reg_sp **)
307let rtl_init_local local =
308  SemanticsUtils.reg_sp_store local ByteValues.BVundef
309
310(** val rtl_setup_call_separate :
311    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
312    -> rTL_state -> rTL_state Errors.res **)
313let rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st =
314  (let { Types.fst = mem; Types.snd = b } =
315     GenMem.alloc st.Joint_semantics.m (Z.z_of_nat Nat.O)
316       (Z.z_of_nat stacksize)
317   in
318  (fun _ ->
319  let sp = { Pointers.pblock = b; Pointers.poff =
320    (BitVector.zero Pointers.offset_size) }
321  in
322  Obj.magic
323    (Monad.m_bind0 (Monad.max_def Errors.res0)
324      (Obj.magic
325        (Errors.mfold_left2 (fun lenv dest src ->
326          Obj.magic
327            (Monad.m_bind0 (Monad.max_def Errors.res0)
328              (Obj.magic
329                (rtl_arg_retrieve (Obj.magic st.Joint_semantics.regs) src))
330              (fun v ->
331              Obj.magic (Errors.OK (SemanticsUtils.reg_sp_store dest v lenv)))))
332          (Errors.OK (SemanticsUtils.reg_sp_init sp)) formal_arg_regs
333          actual_arg_regs)) (fun new_regs ->
334      Obj.magic (Errors.OK
335        (Joint_semantics.set_regs rTL_state_params new_regs
336          (Joint_semantics.set_m rTL_state_params mem st))))))) __
337
338(** val rtl_setup_call_unique :
339    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
340    -> rTL_state -> rTL_state Errors.res **)
341let rtl_setup_call_unique stacksize formal_arg_regs actual_arg_regs st =
342  Obj.magic
343    (Monad.m_bind0 (Monad.max_def Errors.res0)
344      (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
345      let newsp =
346        Pointers.neg_shift_pointer (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
347          (Nat.S (Nat.S Nat.O)))))))) (Types.pi1 sp)
348          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
349            (Nat.S (Nat.S (Nat.S Nat.O)))))))) stacksize)
350      in
351      Monad.m_bind0 (Monad.max_def Errors.res0)
352        (Obj.magic
353          (Errors.mfold_left2 (fun lenv dest src ->
354            Obj.magic
355              (Monad.m_bind0 (Monad.max_def Errors.res0)
356                (Obj.magic
357                  (rtl_arg_retrieve (Obj.magic st.Joint_semantics.regs) src))
358                (fun v ->
359                Obj.magic (Errors.OK
360                  (SemanticsUtils.reg_sp_store dest v lenv))))) (Errors.OK
361            (SemanticsUtils.reg_sp_init newsp)) formal_arg_regs
362            actual_arg_regs)) (fun new_regs ->
363        Obj.magic (Errors.OK
364          (Joint_semantics.set_regs rTL_state_params new_regs st)))))
365
366type rTL_state_pc = Joint_semantics.state_pc
367
368(** val rtl_save_frame :
369    Registers.register List.list -> rTL_state_pc -> __ **)
370let rtl_save_frame retregs st =
371  Monad.m_bind0 (Monad.max_def Errors.res0)
372    (Obj.magic
373      (Errors.opt_to_res (List.Cons ((Errors.MSG
374        ErrorMessages.FrameErrorOnPush), List.Nil))
375        st.Joint_semantics.st_no_pc.Joint_semantics.st_frms)) (fun frms ->
376    let frame0 = List.Cons ({ fr_ret_regs = retregs; fr_pc =
377      st.Joint_semantics.pc; fr_carry =
378      st.Joint_semantics.st_no_pc.Joint_semantics.carry; fr_regs =
379      (Obj.magic st.Joint_semantics.st_no_pc.Joint_semantics.regs) }, frms)
380    in
381    Obj.magic (Errors.OK
382      (Joint_semantics.set_frms rTL_state_params (Obj.magic frame0)
383        st.Joint_semantics.st_no_pc)))
384
385(** val rtl_fetch_external_args :
386    AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
387    Values.val0 List.list Errors.res **)
388let rtl_fetch_external_args _ =
389  failwith "AXIOM TO BE REALIZED"
390
391(** val rtl_set_result :
392    Values.val0 List.list -> Registers.register List.list -> rTL_state ->
393    rTL_state Errors.res **)
394let rtl_set_result _ =
395  failwith "AXIOM TO BE REALIZED"
396
397(** val rtl_reg_store :
398    PreIdentifiers.identifier -> ByteValues.beval -> Joint_semantics.state ->
399    Joint_semantics.state **)
400let rtl_reg_store r v st =
401  let mem =
402    SemanticsUtils.reg_sp_store r v (Obj.magic st.Joint_semantics.regs)
403  in
404  Joint_semantics.set_regs rTL_state_params (Obj.magic mem) st
405
406(** val rtl_reg_retrieve :
407    Joint_semantics.state -> Registers.register -> ByteValues.beval
408    Errors.res **)
409let rtl_reg_retrieve st l =
410  SemanticsUtils.reg_sp_retrieve (Obj.magic st.Joint_semantics.regs) l
411
412(** val rtl_read_result :
413    Registers.register List.list -> rTL_state -> ByteValues.beval List.list
414    Errors.res **)
415let rtl_read_result rets st =
416  Obj.magic
417    (Monad.m_list_map (Monad.max_def Errors.res0)
418      (Obj.magic (rtl_reg_retrieve st)) rets)
419
420(** val rtl_pop_frame_separate :
421    Registers.register List.list -> rTL_state -> (rTL_state,
422    ByteValues.program_counter) Types.prod Errors.res **)
423let rtl_pop_frame_separate ret st =
424  Obj.magic
425    (Monad.m_bind0 (Monad.max_def Errors.res0)
426      (Obj.magic
427        (Errors.opt_to_res (List.Cons ((Errors.MSG
428          ErrorMessages.FrameErrorOnPop), List.Nil))
429          st.Joint_semantics.st_frms)) (fun frms ->
430      match frms with
431      | List.Nil ->
432        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
433          ErrorMessages.EmptyStack), List.Nil)))
434      | List.Cons (hd, tl) ->
435        Monad.m_bind0 (Monad.max_def Errors.res0)
436          (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
437          let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
438          let st0 =
439            Util.foldl (fun st0 reg_val ->
440              rtl_reg_store reg_val.Types.fst reg_val.Types.snd st0) st
441              reg_vals
442          in
443          Monad.m_bind0 (Monad.max_def Errors.res0)
444            (Obj.magic (Joint_semantics.sp rTL_state_params st0)) (fun sp ->
445            let st1 =
446              Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
447                (Joint_semantics.set_regs rTL_state_params
448                  (Obj.magic hd.fr_regs)
449                  (Joint_semantics.set_carry rTL_state_params hd.fr_carry
450                    (Joint_semantics.set_m rTL_state_params
451                      (GenMem.free st0.Joint_semantics.m
452                        (Types.pi1 sp).Pointers.pblock) st0)))
453            in
454            let pc = hd.fr_pc in
455            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
456              Types.snd = pc }))))
457
458(** val rtl_pop_frame_unique :
459    Registers.register List.list -> rTL_state -> (rTL_state,
460    ByteValues.program_counter) Types.prod Errors.res **)
461let rtl_pop_frame_unique ret st =
462  Obj.magic
463    (Monad.m_bind0 (Monad.max_def Errors.res0)
464      (Obj.magic
465        (Errors.opt_to_res (List.Cons ((Errors.MSG
466          ErrorMessages.FrameErrorOnPop), List.Nil))
467          st.Joint_semantics.st_frms)) (fun frms ->
468      match frms with
469      | List.Nil ->
470        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
471          ErrorMessages.EmptyStack), List.Nil)))
472      | List.Cons (hd, tl) ->
473        Monad.m_bind0 (Monad.max_def Errors.res0)
474          (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
475          let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
476          let st0 =
477            Util.foldl (fun st0 reg_val ->
478              rtl_reg_store reg_val.Types.fst reg_val.Types.snd st0) st
479              reg_vals
480          in
481          Monad.m_bind0 (Monad.max_def Errors.res0)
482            (Obj.magic (Joint_semantics.sp rTL_state_params st0)) (fun sp ->
483            let st1 =
484              Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
485                (Joint_semantics.set_regs rTL_state_params
486                  (Obj.magic hd.fr_regs)
487                  (Joint_semantics.set_carry rTL_state_params hd.fr_carry
488                    st0))
489            in
490            let pc = hd.fr_pc in
491            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
492              Types.snd = pc }))))
493
494(** val block_of_register_pair :
495    Registers.register -> Registers.register -> rTL_state -> Pointers.block
496    Errors.res **)
497let block_of_register_pair r1 r2 st =
498  Obj.magic
499    (Monad.m_bind0 (Monad.max_def Errors.res0)
500      (Obj.magic (rtl_reg_retrieve st r1)) (fun v1 ->
501      Monad.m_bind0 (Monad.max_def Errors.res0)
502        (Obj.magic (rtl_reg_retrieve st r2)) (fun v2 ->
503        Monad.m_bind0 (Monad.max_def Errors.res0)
504          (Obj.magic
505            (BEMem.pointer_of_address { Types.fst = v1; Types.snd = v2 }))
506          (fun ptr -> Obj.magic (Errors.OK ptr.Pointers.pblock)))))
507
508(** val eval_rtl_seq :
509    RTL.rtl_seq -> AST.ident -> rTL_state -> rTL_state Errors.res **)
510let eval_rtl_seq stm curr_fn st =
511  let RTL.Rtl_stack_address (dreg1, dreg2) = stm in
512  Obj.magic
513    (Monad.m_bind0 (Monad.max_def Errors.res0)
514      (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
515      let { Types.fst = dpl; Types.snd = dph } =
516        ByteValues.beval_pair_of_pointer (Types.pi1 sp)
517      in
518      let st0 = rtl_reg_store dreg1 dpl st in
519      Monad.m_return0 (Monad.max_def Errors.res0)
520        (rtl_reg_store dreg2 dph st0)))
521
522(** val reg_res_store :
523    PreIdentifiers.identifier -> ByteValues.beval -> SemanticsUtils.reg_sp ->
524    SemanticsUtils.reg_sp Errors.res **)
525let reg_res_store r v s =
526  Errors.OK (SemanticsUtils.reg_sp_store r v s)
527
528(** val rTL_semantics_separate : SemanticsUtils.sem_graph_params **)
529let rTL_semantics_separate =
530  { SemanticsUtils.sgp_pars =
531    (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
532    SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
533    rTL_state_params; Joint_semantics.acca_store_ =
534    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
535    (Obj.magic SemanticsUtils.reg_sp_retrieve);
536    Joint_semantics.acca_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
537    Joint_semantics.accb_store_ = (Obj.magic reg_res_store);
538    Joint_semantics.accb_retrieve_ =
539    (Obj.magic SemanticsUtils.reg_sp_retrieve);
540    Joint_semantics.accb_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
541    Joint_semantics.dpl_store_ = (Obj.magic reg_res_store);
542    Joint_semantics.dpl_retrieve_ =
543    (Obj.magic SemanticsUtils.reg_sp_retrieve);
544    Joint_semantics.dpl_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
545    Joint_semantics.dph_store_ = (Obj.magic reg_res_store);
546    Joint_semantics.dph_retrieve_ =
547    (Obj.magic SemanticsUtils.reg_sp_retrieve);
548    Joint_semantics.dph_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
549    Joint_semantics.snd_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
550    Joint_semantics.pair_reg_move_ = (fun env p ->
551    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
552    Obj.magic
553      (Monad.m_bind0 (Monad.max_def Errors.res0)
554        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
555        Monad.m_return0 (Monad.max_def Errors.res0)
556          (SemanticsUtils.reg_sp_store dest v (Obj.magic env)))));
557    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
558    Joint_semantics.setup_call = (Obj.magic rtl_setup_call_separate);
559    Joint_semantics.fetch_external_args =
560    (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
561    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
562    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
563    (Obj.magic List.Nil); Joint_semantics.read_result = (fun x x0 ->
564    Obj.magic rtl_read_result); Joint_semantics.eval_ext_seq = (fun x x0 ->
565    Obj.magic eval_rtl_seq); Joint_semantics.pop_frame = (fun x x0 x1 ->
566    Obj.magic rtl_pop_frame_separate) }) }
567
568(** val rTL_semantics_unique : SemanticsUtils.sem_graph_params **)
569let rTL_semantics_unique =
570  { SemanticsUtils.sgp_pars =
571    (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
572    SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
573    rTL_state_params; Joint_semantics.acca_store_ =
574    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
575    (Obj.magic SemanticsUtils.reg_sp_retrieve);
576    Joint_semantics.acca_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
577    Joint_semantics.accb_store_ = (Obj.magic reg_res_store);
578    Joint_semantics.accb_retrieve_ =
579    (Obj.magic SemanticsUtils.reg_sp_retrieve);
580    Joint_semantics.accb_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
581    Joint_semantics.dpl_store_ = (Obj.magic reg_res_store);
582    Joint_semantics.dpl_retrieve_ =
583    (Obj.magic SemanticsUtils.reg_sp_retrieve);
584    Joint_semantics.dpl_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
585    Joint_semantics.dph_store_ = (Obj.magic reg_res_store);
586    Joint_semantics.dph_retrieve_ =
587    (Obj.magic SemanticsUtils.reg_sp_retrieve);
588    Joint_semantics.dph_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
589    Joint_semantics.snd_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
590    Joint_semantics.pair_reg_move_ = (fun env p ->
591    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
592    Obj.magic
593      (Monad.m_bind0 (Monad.max_def Errors.res0)
594        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
595        Monad.m_return0 (Monad.max_def Errors.res0)
596          (SemanticsUtils.reg_sp_store dest v (Obj.magic env)))));
597    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
598    Joint_semantics.setup_call = (Obj.magic rtl_setup_call_unique);
599    Joint_semantics.fetch_external_args =
600    (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
601    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
602    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
603    (Obj.magic List.Nil); Joint_semantics.read_result = (fun x x0 ->
604    Obj.magic rtl_read_result); Joint_semantics.eval_ext_seq = (fun x x0 ->
605    Obj.magic eval_rtl_seq); Joint_semantics.pop_frame = (fun x x0 x1 ->
606    Obj.magic rtl_pop_frame_unique) }) }
607
Note: See TracBrowser for help on using the repository browser.