source: extracted/rTL_semantics.ml @ 2960

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

New extraction, it diverges in RTL execution now.

File size: 28.0 KB
RevLine 
[2829]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
[2951]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 **)
[2960]159let rec reg_sp_rect_Type4 h_mk_reg_sp x_3 =
160  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_3 in
[2951]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 **)
[2960]166let rec reg_sp_rect_Type5 h_mk_reg_sp x_5 =
167  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_5 in
[2951]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 **)
[2960]173let rec reg_sp_rect_Type3 h_mk_reg_sp x_7 =
174  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_7 in
[2951]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 **)
[2960]180let rec reg_sp_rect_Type2 h_mk_reg_sp x_9 =
181  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_9 in
[2951]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 **)
[2960]187let rec reg_sp_rect_Type1 h_mk_reg_sp x_11 =
188  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_11 in
[2951]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 **)
[2960]194let rec reg_sp_rect_Type0 h_mk_reg_sp x_13 =
195  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_13 in
[2951]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
[2829]292type frame = { fr_ret_regs : Registers.register List.list;
293               fr_pc : ByteValues.program_counter;
[2951]294               fr_carry : ByteValues.bebit; fr_regs : reg_sp }
[2829]295
296(** val frame_rect_Type4 :
297    (Registers.register List.list -> ByteValues.program_counter ->
[2951]298    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
[2960]299let rec frame_rect_Type4 h_mk_frame x_29 =
[2829]300  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
[2960]301    fr_regs = fr_regs0 } = x_29
[2829]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 ->
[2951]307    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
[2960]308let rec frame_rect_Type5 h_mk_frame x_31 =
[2829]309  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
[2960]310    fr_regs = fr_regs0 } = x_31
[2829]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 ->
[2951]316    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
[2960]317let rec frame_rect_Type3 h_mk_frame x_33 =
[2829]318  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
[2960]319    fr_regs = fr_regs0 } = x_33
[2829]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 ->
[2951]325    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
[2960]326let rec frame_rect_Type2 h_mk_frame x_35 =
[2829]327  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
[2960]328    fr_regs = fr_regs0 } = x_35
[2829]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 ->
[2951]334    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
[2960]335let rec frame_rect_Type1 h_mk_frame x_37 =
[2829]336  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
[2960]337    fr_regs = fr_regs0 } = x_37
[2829]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 ->
[2951]343    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
[2960]344let rec frame_rect_Type0 h_mk_frame x_39 =
[2829]345  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
[2960]346    fr_regs = fr_regs0 } = x_39
[2829]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
[2951]362(** val fr_regs : frame -> reg_sp **)
[2829]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 ->
[2951]368    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
[2829]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 ->
[2951]374    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
[2829]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 ->
[2951]380    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
[2829]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 ->
[2951]386    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
[2829]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 ->
[2951]392    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
[2829]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);
[2951]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 })) }
[2829]416
417type rTL_state = Joint_semantics.state
418
419(** val rtl_arg_retrieve :
[2951]420    reg_sp -> Joint.psd_argument -> ByteValues.beval Errors.res **)
[2829]421let rtl_arg_retrieve env = function
[2951]422| Joint.Reg r -> SemanticsUtils.reg_retrieve env.reg_sp_env r
[2829]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
[2951]442(** val rtl_init_local : Registers.register -> reg_sp -> reg_sp **)
[2829]443let rtl_init_local local =
[2951]444  reg_sp_store local ByteValues.BVundef
[2829]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))
[2951]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 ->
[2829]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
[2951]473(** val rtl_setup_call_separate_overflow :
474    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
475    -> rTL_state -> rTL_state Errors.res **)
476let rtl_setup_call_separate_overflow stacksize formal_arg_regs actual_arg_regs st =
477  match Nat.leb (Nat.S (Nat.plus stacksize st.Joint_semantics.stack_usage))
478          (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
479            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
480            (Nat.S (Nat.S Nat.O))))))))))))))))) with
481  | Bool.True ->
482    rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st
483  | Bool.False ->
[2960]484    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.StackOverflow), List.Nil))
[2951]485
[2829]486(** val rtl_setup_call_unique :
487    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
488    -> rTL_state -> rTL_state Errors.res **)
489let rtl_setup_call_unique stacksize formal_arg_regs actual_arg_regs st =
490  Obj.magic
491    (Monad.m_bind0 (Monad.max_def Errors.res0)
492      (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
493      let newsp =
494        Pointers.neg_shift_pointer (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
495          (Nat.S (Nat.S Nat.O)))))))) (Types.pi1 sp)
496          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
497            (Nat.S (Nat.S (Nat.S Nat.O)))))))) stacksize)
498      in
499      Monad.m_bind0 (Monad.max_def Errors.res0)
500        (Obj.magic
501          (Errors.mfold_left2 (fun lenv dest src ->
502            Obj.magic
503              (Monad.m_bind0 (Monad.max_def Errors.res0)
504                (Obj.magic
505                  (rtl_arg_retrieve (Obj.magic st.Joint_semantics.regs) src))
[2951]506                (fun v -> Obj.magic (Errors.OK (reg_sp_store dest v lenv)))))
507            (Errors.OK (reg_sp_empty newsp)) formal_arg_regs actual_arg_regs))
508        (fun new_regs ->
[2829]509        Obj.magic (Errors.OK
510          (Joint_semantics.set_regs rTL_state_params new_regs st)))))
511
512type rTL_state_pc = Joint_semantics.state_pc
513
514(** val rtl_save_frame :
515    Registers.register List.list -> rTL_state_pc -> __ **)
516let rtl_save_frame retregs st =
517  Monad.m_bind0 (Monad.max_def Errors.res0)
518    (Obj.magic
519      (Errors.opt_to_res (List.Cons ((Errors.MSG
520        ErrorMessages.FrameErrorOnPush), List.Nil))
521        st.Joint_semantics.st_no_pc.Joint_semantics.st_frms)) (fun frms ->
522    let frame0 = List.Cons ({ fr_ret_regs = retregs; fr_pc =
523      st.Joint_semantics.pc; fr_carry =
524      st.Joint_semantics.st_no_pc.Joint_semantics.carry; fr_regs =
525      (Obj.magic st.Joint_semantics.st_no_pc.Joint_semantics.regs) }, frms)
526    in
527    Obj.magic (Errors.OK
528      (Joint_semantics.set_frms rTL_state_params (Obj.magic frame0)
529        st.Joint_semantics.st_no_pc)))
530
531(** val rtl_fetch_external_args :
532    AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
533    Values.val0 List.list Errors.res **)
[2960]534let rtl_fetch_external_args _ =
535  failwith "AXIOM TO BE REALIZED"
[2829]536
537(** val rtl_set_result :
538    Values.val0 List.list -> Registers.register List.list -> rTL_state ->
539    rTL_state Errors.res **)
[2960]540let rtl_set_result _ =
541  failwith "AXIOM TO BE REALIZED"
[2829]542
543(** val rtl_reg_store :
544    PreIdentifiers.identifier -> ByteValues.beval -> Joint_semantics.state ->
545    Joint_semantics.state **)
546let rtl_reg_store r v st =
[2951]547  let mem = reg_sp_store r v (Obj.magic st.Joint_semantics.regs) in
[2829]548  Joint_semantics.set_regs rTL_state_params (Obj.magic mem) st
549
550(** val rtl_reg_retrieve :
551    Joint_semantics.state -> Registers.register -> ByteValues.beval
552    Errors.res **)
553let rtl_reg_retrieve st l =
[2951]554  reg_sp_retrieve (Obj.magic st.Joint_semantics.regs) l
[2829]555
556(** val rtl_read_result :
557    Registers.register List.list -> rTL_state -> ByteValues.beval List.list
558    Errors.res **)
559let rtl_read_result rets st =
560  Obj.magic
561    (Monad.m_list_map (Monad.max_def Errors.res0)
562      (Obj.magic (rtl_reg_retrieve st)) rets)
563
564(** val rtl_pop_frame_separate :
565    Registers.register List.list -> rTL_state -> (rTL_state,
566    ByteValues.program_counter) Types.prod Errors.res **)
567let rtl_pop_frame_separate ret st =
568  Obj.magic
569    (Monad.m_bind0 (Monad.max_def Errors.res0)
570      (Obj.magic
571        (Errors.opt_to_res (List.Cons ((Errors.MSG
572          ErrorMessages.FrameErrorOnPop), List.Nil))
573          st.Joint_semantics.st_frms)) (fun frms ->
574      match frms with
575      | List.Nil ->
576        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
577          ErrorMessages.EmptyStack), List.Nil)))
578      | List.Cons (hd, tl) ->
579        Monad.m_bind0 (Monad.max_def Errors.res0)
580          (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
581          let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
582          Monad.m_bind0 (Monad.max_def Errors.res0)
[2933]583            (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
[2951]584            let st0 =
[2829]585              Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
586                (Joint_semantics.set_regs rTL_state_params
587                  (Obj.magic hd.fr_regs)
588                  (Joint_semantics.set_carry rTL_state_params hd.fr_carry
589                    (Joint_semantics.set_m rTL_state_params
[2933]590                      (GenMem.free st.Joint_semantics.m
591                        (Types.pi1 sp).Pointers.pblock) st)))
[2829]592            in
593            let pc = hd.fr_pc in
[2951]594            let st1 =
595              Util.foldl (fun st1 reg_val ->
596                rtl_reg_store reg_val.Types.fst reg_val.Types.snd st1) st0
597                reg_vals
598            in
[2829]599            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
600              Types.snd = pc }))))
601
602(** val rtl_pop_frame_unique :
603    Registers.register List.list -> rTL_state -> (rTL_state,
604    ByteValues.program_counter) Types.prod Errors.res **)
605let rtl_pop_frame_unique ret st =
606  Obj.magic
607    (Monad.m_bind0 (Monad.max_def Errors.res0)
608      (Obj.magic
609        (Errors.opt_to_res (List.Cons ((Errors.MSG
610          ErrorMessages.FrameErrorOnPop), List.Nil))
611          st.Joint_semantics.st_frms)) (fun frms ->
612      match frms with
613      | List.Nil ->
614        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
615          ErrorMessages.EmptyStack), List.Nil)))
616      | List.Cons (hd, tl) ->
617        Monad.m_bind0 (Monad.max_def Errors.res0)
618          (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
619          let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
620          Monad.m_bind0 (Monad.max_def Errors.res0)
[2951]621            (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
622            let st0 =
[2829]623              Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
624                (Joint_semantics.set_regs rTL_state_params
625                  (Obj.magic hd.fr_regs)
[2951]626                  (Joint_semantics.set_carry rTL_state_params hd.fr_carry st))
[2829]627            in
628            let pc = hd.fr_pc in
[2951]629            let st1 =
630              Util.foldl (fun st1 reg_val ->
631                rtl_reg_store reg_val.Types.fst reg_val.Types.snd st1) st0
632                reg_vals
633            in
[2829]634            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
635              Types.snd = pc }))))
636
637(** val block_of_register_pair :
638    Registers.register -> Registers.register -> rTL_state -> Pointers.block
639    Errors.res **)
640let block_of_register_pair r1 r2 st =
641  Obj.magic
642    (Monad.m_bind0 (Monad.max_def Errors.res0)
643      (Obj.magic (rtl_reg_retrieve st r1)) (fun v1 ->
644      Monad.m_bind0 (Monad.max_def Errors.res0)
645        (Obj.magic (rtl_reg_retrieve st r2)) (fun v2 ->
646        Monad.m_bind0 (Monad.max_def Errors.res0)
647          (Obj.magic
648            (BEMem.pointer_of_address { Types.fst = v1; Types.snd = v2 }))
649          (fun ptr -> Obj.magic (Errors.OK ptr.Pointers.pblock)))))
650
651(** val eval_rtl_seq :
652    RTL.rtl_seq -> AST.ident -> rTL_state -> rTL_state Errors.res **)
653let eval_rtl_seq stm curr_fn st =
654  let RTL.Rtl_stack_address (dreg1, dreg2) = stm in
655  Obj.magic
656    (Monad.m_bind0 (Monad.max_def Errors.res0)
657      (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
658      let { Types.fst = dpl; Types.snd = dph } =
659        ByteValues.beval_pair_of_pointer (Types.pi1 sp)
660      in
661      let st0 = rtl_reg_store dreg1 dpl st in
662      Monad.m_return0 (Monad.max_def Errors.res0)
663        (rtl_reg_store dreg2 dph st0)))
664
665(** val reg_res_store :
[2951]666    PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
667    Errors.res **)
[2829]668let reg_res_store r v s =
[2951]669  Errors.OK (reg_sp_store r v s)
[2829]670
671(** val rTL_semantics_separate : SemanticsUtils.sem_graph_params **)
672let rTL_semantics_separate =
673  { SemanticsUtils.sgp_pars =
674    (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
675    SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
676    rTL_state_params; Joint_semantics.acca_store_ =
677    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
[2951]678    (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
679    (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
680    (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
681    (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
682    (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
683    (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
684    (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
685    (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
686    (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
687    (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
688    (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
689    (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
690    (fun env p ->
[2829]691    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
692    Obj.magic
693      (Monad.m_bind0 (Monad.max_def Errors.res0)
694        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
695        Monad.m_return0 (Monad.max_def Errors.res0)
[2951]696          (reg_sp_store dest v (Obj.magic env)))));
[2829]697    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
698    Joint_semantics.setup_call = (Obj.magic rtl_setup_call_separate);
699    Joint_semantics.fetch_external_args =
700    (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
701    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
702    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
[2951]703    (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
704      Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
705      ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
706    Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
707    Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
708    Joint_semantics.pop_frame = (fun x x0 x1 ->
709    Obj.magic rtl_pop_frame_separate) });
710    SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }
[2829]711
[2951]712(** val rTL_semantics_separate_overflow : SemanticsUtils.sem_graph_params **)
713let rTL_semantics_separate_overflow =
714  { SemanticsUtils.sgp_pars =
715    (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
716    SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
717    rTL_state_params; Joint_semantics.acca_store_ =
718    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
719    (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
720    (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
721    (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
722    (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
723    (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
724    (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
725    (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
726    (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
727    (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
728    (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
729    (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
730    (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
731    (fun env p ->
732    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
733    Obj.magic
734      (Monad.m_bind0 (Monad.max_def Errors.res0)
735        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
736        Monad.m_return0 (Monad.max_def Errors.res0)
737          (reg_sp_store dest v (Obj.magic env)))));
738    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
739    Joint_semantics.setup_call =
740    (Obj.magic rtl_setup_call_separate_overflow);
741    Joint_semantics.fetch_external_args =
742    (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
743    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
744    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
745    (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
746      Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
747      ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
748    Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
749    Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
750    Joint_semantics.pop_frame = (fun x x0 x1 ->
751    Obj.magic rtl_pop_frame_separate) });
752    SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }
753
[2829]754(** val rTL_semantics_unique : SemanticsUtils.sem_graph_params **)
755let rTL_semantics_unique =
756  { SemanticsUtils.sgp_pars =
757    (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
758    SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
759    rTL_state_params; Joint_semantics.acca_store_ =
760    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
[2951]761    (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
762    (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
763    (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
764    (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
765    (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
766    (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
767    (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
768    (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
769    (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
770    (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
771    (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
772    (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
773    (fun env p ->
[2829]774    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
775    Obj.magic
776      (Monad.m_bind0 (Monad.max_def Errors.res0)
777        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
778        Monad.m_return0 (Monad.max_def Errors.res0)
[2951]779          (reg_sp_store dest v (Obj.magic env)))));
[2829]780    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
781    Joint_semantics.setup_call = (Obj.magic rtl_setup_call_unique);
782    Joint_semantics.fetch_external_args =
783    (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
784    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
785    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
[2951]786    (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
787      Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
788      ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
789    Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
790    Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
791    Joint_semantics.pop_frame = (fun x x0 x1 ->
792    Obj.magic rtl_pop_frame_unique) });
793    SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }
[2829]794
Note: See TracBrowser for help on using the repository browser.