source: extracted/rTL_semantics.ml @ 2933

Last change on this file since 2933 was 2933, checked in by sacerdot, 6 years ago

New extraction, several bug fixed. RTL_semantics fixed by hand, will be fixed
automatically when Paolo commits.

File size: 20.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
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_26392 =
161  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
162    fr_regs = fr_regs0 } = x_26392
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_26394 =
170  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
171    fr_regs = fr_regs0 } = x_26394
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_26396 =
179  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
180    fr_regs = fr_regs0 } = x_26396
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_26398 =
188  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
189    fr_regs = fr_regs0 } = x_26398
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_26400 =
197  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
198    fr_regs = fr_regs0 } = x_26400
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_26402 =
206  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
207    fr_regs = fr_regs0 } = x_26402
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          Monad.m_bind0 (Monad.max_def Errors.res0)
439            (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
440            let st1 =
441              Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
442                (Joint_semantics.set_regs rTL_state_params
443                  (Obj.magic hd.fr_regs)
444                  (Joint_semantics.set_carry rTL_state_params hd.fr_carry
445                    (Joint_semantics.set_m rTL_state_params
446                      (GenMem.free st.Joint_semantics.m
447                        (Types.pi1 sp).Pointers.pblock) st)))
448            in
449            let pc = hd.fr_pc in
450          let st1 =
451            Util.foldl (fun st0 reg_val ->
452prerr_endline ("SALVO IL REGISTRO: r_" ^ string_of_int (Glue.int_of_matitapos reg_val.Types.fst));
453              rtl_reg_store reg_val.Types.fst reg_val.Types.snd st0) st1
454              reg_vals
455          in
456            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
457              Types.snd = pc }))))
458
459(** val rtl_pop_frame_unique :
460    Registers.register List.list -> rTL_state -> (rTL_state,
461    ByteValues.program_counter) Types.prod Errors.res **)
462let rtl_pop_frame_unique ret st =
463  Obj.magic
464    (Monad.m_bind0 (Monad.max_def Errors.res0)
465      (Obj.magic
466        (Errors.opt_to_res (List.Cons ((Errors.MSG
467          ErrorMessages.FrameErrorOnPop), List.Nil))
468          st.Joint_semantics.st_frms)) (fun frms ->
469      match frms with
470      | List.Nil ->
471        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
472          ErrorMessages.EmptyStack), List.Nil)))
473      | List.Cons (hd, tl) ->
474        Monad.m_bind0 (Monad.max_def Errors.res0)
475          (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
476          let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
477          let st0 =
478            Util.foldl (fun st0 reg_val ->
479              rtl_reg_store reg_val.Types.fst reg_val.Types.snd st0) st
480              reg_vals
481          in
482          Monad.m_bind0 (Monad.max_def Errors.res0)
483            (Obj.magic (Joint_semantics.sp rTL_state_params st0)) (fun sp ->
484            let st1 =
485              Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
486                (Joint_semantics.set_regs rTL_state_params
487                  (Obj.magic hd.fr_regs)
488                  (Joint_semantics.set_carry rTL_state_params hd.fr_carry
489                    st0))
490            in
491            let pc = hd.fr_pc in
492            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
493              Types.snd = pc }))))
494
495(** val block_of_register_pair :
496    Registers.register -> Registers.register -> rTL_state -> Pointers.block
497    Errors.res **)
498let block_of_register_pair r1 r2 st =
499  Obj.magic
500    (Monad.m_bind0 (Monad.max_def Errors.res0)
501      (Obj.magic (rtl_reg_retrieve st r1)) (fun v1 ->
502      Monad.m_bind0 (Monad.max_def Errors.res0)
503        (Obj.magic (rtl_reg_retrieve st r2)) (fun v2 ->
504        Monad.m_bind0 (Monad.max_def Errors.res0)
505          (Obj.magic
506            (BEMem.pointer_of_address { Types.fst = v1; Types.snd = v2 }))
507          (fun ptr -> Obj.magic (Errors.OK ptr.Pointers.pblock)))))
508
509(** val eval_rtl_seq :
510    RTL.rtl_seq -> AST.ident -> rTL_state -> rTL_state Errors.res **)
511let eval_rtl_seq stm curr_fn st =
512  let RTL.Rtl_stack_address (dreg1, dreg2) = stm in
513  Obj.magic
514    (Monad.m_bind0 (Monad.max_def Errors.res0)
515      (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
516      let { Types.fst = dpl; Types.snd = dph } =
517        ByteValues.beval_pair_of_pointer (Types.pi1 sp)
518      in
519      let st0 = rtl_reg_store dreg1 dpl st in
520      Monad.m_return0 (Monad.max_def Errors.res0)
521        (rtl_reg_store dreg2 dph st0)))
522
523(** val reg_res_store :
524    PreIdentifiers.identifier -> ByteValues.beval -> SemanticsUtils.reg_sp ->
525    SemanticsUtils.reg_sp Errors.res **)
526let reg_res_store r v s =
527  Errors.OK (SemanticsUtils.reg_sp_store r v s)
528
529(** val rTL_semantics_separate : SemanticsUtils.sem_graph_params **)
530let rTL_semantics_separate =
531  { SemanticsUtils.sgp_pars =
532    (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
533    SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
534    rTL_state_params; Joint_semantics.acca_store_ =
535    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
536    (Obj.magic SemanticsUtils.reg_sp_retrieve);
537    Joint_semantics.acca_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
538    Joint_semantics.accb_store_ = (Obj.magic reg_res_store);
539    Joint_semantics.accb_retrieve_ =
540    (Obj.magic SemanticsUtils.reg_sp_retrieve);
541    Joint_semantics.accb_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
542    Joint_semantics.dpl_store_ = (Obj.magic reg_res_store);
543    Joint_semantics.dpl_retrieve_ =
544    (Obj.magic SemanticsUtils.reg_sp_retrieve);
545    Joint_semantics.dpl_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
546    Joint_semantics.dph_store_ = (Obj.magic reg_res_store);
547    Joint_semantics.dph_retrieve_ =
548    (Obj.magic SemanticsUtils.reg_sp_retrieve);
549    Joint_semantics.dph_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
550    Joint_semantics.snd_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
551    Joint_semantics.pair_reg_move_ = (fun env p ->
552    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
553    Obj.magic
554      (Monad.m_bind0 (Monad.max_def Errors.res0)
555        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
556        Monad.m_return0 (Monad.max_def Errors.res0)
557          (SemanticsUtils.reg_sp_store dest v (Obj.magic env)))));
558    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
559    Joint_semantics.setup_call = (Obj.magic rtl_setup_call_separate);
560    Joint_semantics.fetch_external_args =
561    (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
562    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
563    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
564    (Obj.magic List.Nil); Joint_semantics.read_result = (fun x x0 ->
565    Obj.magic rtl_read_result); Joint_semantics.eval_ext_seq = (fun x x0 ->
566    Obj.magic eval_rtl_seq); Joint_semantics.pop_frame = (fun x x0 x1 ->
567    Obj.magic rtl_pop_frame_separate) }) }
568
569(** val rTL_semantics_unique : SemanticsUtils.sem_graph_params **)
570let rTL_semantics_unique =
571  { SemanticsUtils.sgp_pars =
572    (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
573    SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
574    rTL_state_params; Joint_semantics.acca_store_ =
575    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
576    (Obj.magic SemanticsUtils.reg_sp_retrieve);
577    Joint_semantics.acca_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
578    Joint_semantics.accb_store_ = (Obj.magic reg_res_store);
579    Joint_semantics.accb_retrieve_ =
580    (Obj.magic SemanticsUtils.reg_sp_retrieve);
581    Joint_semantics.accb_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
582    Joint_semantics.dpl_store_ = (Obj.magic reg_res_store);
583    Joint_semantics.dpl_retrieve_ =
584    (Obj.magic SemanticsUtils.reg_sp_retrieve);
585    Joint_semantics.dpl_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
586    Joint_semantics.dph_store_ = (Obj.magic reg_res_store);
587    Joint_semantics.dph_retrieve_ =
588    (Obj.magic SemanticsUtils.reg_sp_retrieve);
589    Joint_semantics.dph_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
590    Joint_semantics.snd_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
591    Joint_semantics.pair_reg_move_ = (fun env p ->
592    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
593    Obj.magic
594      (Monad.m_bind0 (Monad.max_def Errors.res0)
595        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
596        Monad.m_return0 (Monad.max_def Errors.res0)
597          (SemanticsUtils.reg_sp_store dest v (Obj.magic env)))));
598    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
599    Joint_semantics.setup_call = (Obj.magic rtl_setup_call_unique);
600    Joint_semantics.fetch_external_args =
601    (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
602    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
603    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
604    (Obj.magic List.Nil); Joint_semantics.read_result = (fun x x0 ->
605    Obj.magic rtl_read_result); Joint_semantics.eval_ext_seq = (fun x x0 ->
606    Obj.magic eval_rtl_seq); Joint_semantics.pop_frame = (fun x x0 x1 ->
607    Obj.magic rtl_pop_frame_unique) }) }
608
Note: See TracBrowser for help on using the repository browser.