source: src/RTL/RTL_semantics.ma @ 2796

Last change on this file since 2796 was 2796, checked in by tranquil, 8 years ago
  • added global notation for existence in Type[1] (\exists[1] x.P)
  • in Arithmetic, reimplemented efficient nat_to_bitvector, but still commented out
  • in joint_semantics, moved out and around some parameters in primitive semantics functions
  • fixed all back end semantics
  • added skeleton files for single passes correctness proofs
File size: 5.4 KB
Line 
1include "joint/semanticsUtils.ma".
2include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
3include alias "common/Identifiers.ma".
4include alias "ASM/Util.ma".
5
6record frame: Type[0] ≝
7 { fr_ret_regs: list register
8 ; fr_pc: program_counter
9 ; fr_carry: bebit
10 ; fr_regs: reg_sp
11 }.
12
13definition RTL_state_params : sem_state_params ≝
14  mk_sem_state_params
15    (list frame)
16    [ ]
17    reg_sp
18    reg_sp_init
19    (λenv.OK … (stackp env))
20    (λenv.mk_reg_sp env (* coercion*)).
21
22definition RTL_state ≝ state RTL_state_params.
23
24unification hint 0 ≔ X ⊢ register_env X ≡ identifier_map RegisterTag X.
25
26definition rtl_arg_retrieve : reg_sp → psd_argument → res beval ≝
27  λenv.λa : psd_argument.
28  match a with
29  [ Reg r ⇒ reg_retrieve env r
30  | Imm b ⇒ OK … (BVByte b)
31  ].
32
33(*CSC: could we use here a dependent type to avoid the Error case? *)
34definition rtl_fetch_ra:
35 RTL_state → res (RTL_state × program_counter) ≝
36 λst.
37 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
38   match frms with
39  [ nil ⇒ Error ? [MSG EmptyStack]
40  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉
41  ].
42
43definition rtl_init_local :
44 register → reg_sp → reg_sp ≝
45 λlocal.reg_sp_store … local BVundef.
46
47definition rtl_setup_call:
48 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
49  λstacksize,formal_arg_regs,actual_arg_regs,st.
50  (* paolo: this will need to be changed: we want a unified stack in the whole backend *)
51  let 〈mem,b〉 as E ≝ alloc … (m … st) 0 stacksize in
52  let sp ≝ mk_pointer b (mk_offset (bv_zero …)) in
53  do new_regs ←
54   mfold_left2 …
55    (λlenv,dest,src.
56      do v ← rtl_arg_retrieve … (regs ? st) src ;
57      OK … (reg_sp_store dest v lenv))
58    (OK … (reg_sp_init sp)) formal_arg_regs actual_arg_regs ;
59  OK …
60   (set_regs RTL_state_params new_regs
61    (set_m … mem st)).
62cases daemon (* will probably change anyway *)
63qed.
64
65definition RTL_state_pc ≝ state_pc RTL_state_params.
66
67unification hint 0 ≔ ⊢ RTL_state ≡ state RTL_state_params.
68unification hint 0 ≔ ⊢ RTL_state_pc ≡ state_pc RTL_state_params.
69
70definition rtl_save_frame ≝ λretregs.λst : RTL_state_pc.
71 ! frms ← opt_to_res … [MSG … FrameErrorOnPush] (st_frms … st) ;
72 let frame ≝ mk_frame retregs (pc ? st) (carry ? st) (regs ? st) :: frms in
73  OK … (set_frms RTL_state_params frame st).
74
75(*CSC: XXXX, for external functions only*)
76axiom rtl_fetch_external_args: external_function → RTL_state → list psd_argument → res (list val).
77axiom rtl_set_result: list val → list register → RTL_state → res RTL_state.
78
79definition rtl_reg_store ≝ λr,v,st.
80  let mem ≝ reg_sp_store r v (regs RTL_state_params st) in
81  set_regs RTL_state_params mem st.
82
83definition rtl_reg_retrieve ≝ λst,l.reg_sp_retrieve (regs RTL_state_params st) l.
84
85definition rtl_read_result :
86 list register → RTL_state → res (list beval) ≝
87 λrets,st.
88 m_list_map … (rtl_reg_retrieve st) rets.
89
90(*CSC: we could use a dependent type here: the list of return values should have
91  the same length of the list of return registers that store the values. This
92  saves the OutOfBounds exception *)
93definition rtl_pop_frame:
94 list register → RTL_state →
95  res (RTL_state × program_counter) ≝
96 λret,st.
97 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
98 match frms with
99  [ nil ⇒ Error ? [MSG EmptyStack]
100  | cons hd tl ⇒
101    ! ret_vals ← rtl_read_result … ret st ;
102    (* Paolo: no more OutOfBounds exception, but is it right? should be for
103       compiled programs *)
104    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
105    let st ≝ foldl …
106      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
107      st reg_vals in
108    ! sp ← sp … st ;  (* always succeeds in RTL *)
109    let st ≝ set_frms RTL_state_params tl
110        (set_regs RTL_state_params (fr_regs hd)
111          (set_carry RTL_state_params (fr_carry hd)
112            (set_m … (free … (m … st) (pblock sp)) st))) in
113    let pc ≝ fr_pc hd in
114    return 〈st, pc〉
115  ].
116
117definition block_of_register_pair: register → register → RTL_state → res block ≝
118 λr1,r2,st.
119 do v1 ← rtl_reg_retrieve st r1 ;
120 do v2 ← rtl_reg_retrieve st r2 ;
121 do ptr ← pointer_of_address 〈v1,v2〉 ;
122 OK … (pblock ptr). 
123
124definition eval_rtl_seq:
125  rtl_seq → ident → RTL_state →
126   res RTL_state ≝
127 λstm,curr_fn,st.
128  match stm with
129   [ rtl_stack_address dreg1 dreg2  ⇒
130      ! sp ← sp ? st ; (* always succeeds in RTL *)
131      let 〈dpl,dph〉 ≝ beval_pair_of_pointer sp in
132      let st ≝ rtl_reg_store dreg1 dpl st in
133      return rtl_reg_store dreg2 dph st
134   ].
135
136(* for a store living in res *)
137definition reg_res_store ≝ λr,v,s.OK ? (reg_sp_store r v s).
138
139definition RTL_semantics ≝
140  mk_sem_graph_params RTL
141    (λF.mk_sem_unserialized_params RTL F
142      RTL_state_params
143      reg_res_store reg_sp_retrieve rtl_arg_retrieve
144      reg_res_store reg_sp_retrieve rtl_arg_retrieve
145      reg_res_store reg_sp_retrieve rtl_arg_retrieve
146      reg_res_store reg_sp_retrieve rtl_arg_retrieve
147      rtl_arg_retrieve
148      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
149        ! v ← rtl_arg_retrieve env src ;
150        return reg_sp_store dest v env)
151      (λ_.rtl_save_frame)
152      rtl_setup_call
153      rtl_fetch_external_args
154      rtl_set_result
155      [ ] [ ]
156      (λ_.λ_.rtl_read_result) 
157      (λ_.λ_.eval_rtl_seq)
158      (λ_.λ_.λ_.rtl_pop_frame)).
Note: See TracBrowser for help on using the repository browser.