source: src/ERTL/ERTL_semantics.ma @ 2674

Last change on this file since 2674 was 2674, checked in by tranquil, 7 years ago
  • another change in block definition
  • RTLabs -> RTL and ERTL -> ERTLptr passes fixed, others stil broken
File size: 5.4 KB
Line 
1include "joint/semanticsUtils.ma".
2include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
3include alias "common/Identifiers.ma".
4
5definition ertl_reg_env ≝ register_env beval × hw_register_env.
6
7definition ps_reg_store: ? → ? → ? → res ? ≝
8 λr,v.λlocal_env : ertl_reg_env.
9  do res ← reg_store r v (\fst local_env) ;
10  OK … 〈res, \snd local_env〉.
11
12definition ps_reg_retrieve ≝
13 λlocal_env:ertl_reg_env. reg_retrieve … (\fst local_env).
14
15definition hw_reg_store ≝
16 λr,v.λlocal_env:ertl_reg_env.
17  OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.
18
19definition hw_reg_retrieve ≝
20 λlocal_env:ertl_reg_env.λreg.
21  OK … (hwreg_retrieve … (\snd local_env) reg).
22
23
24definition ps_arg_retrieve : ertl_reg_env → argument ? → res beval ≝
25  λlocal_env,a.
26  match a with
27  [ Reg r ⇒ ps_reg_retrieve local_env r
28  | Imm b ⇒ return BVByte b
29  ].
30
31definition get_hwsp : ertl_reg_env → res xpointer ≝
32 λst.hwreg_retrieve_sp (\snd st).
33
34definition set_hwsp : ertl_reg_env → xpointer → ertl_reg_env ≝
35 λst,sp.〈\fst st, hwreg_store_sp (\snd st) sp〉.
36
37definition ERTL_state : sem_state_params ≝
38  mk_sem_state_params
39 (* framesT ≝ *) (list (register_env beval × ident))
40 (* empty_framesT ≝ *) [ ]
41 (* regsT ≝ *) ertl_reg_env
42 (* empty_regsT ≝ *) (λsp.〈empty_map …,init_hw_register_env sp〉)
43 (*load_sp ≝ *) get_hwsp
44 (*save_sp ≝ *) set_hwsp.
45
46(* we ignore need_spilled_no as we never move framesize based values around in the
47   translation *)
48definition ertl_eval_move ≝ λenv,pr.
49      ! v ←
50        match \snd pr with
51        [ Reg src ⇒
52          match src with
53          [ PSD r ⇒ ps_reg_retrieve env r
54          | HDW r ⇒ hw_reg_retrieve env r
55          ]
56        | Imm b ⇒ return BVByte b ] ;
57      match \fst pr with
58      [ PSD r ⇒ ps_reg_store r v env
59      | HDW r ⇒ hw_reg_store r v env
60      ].
61
62definition ertl_allocate_local ≝
63  λreg.λlenv : ertl_reg_env.
64  〈 add … (\fst lenv) reg BVundef, \snd lenv〉.
65
66
67definition ertl_save_frame:
68 call_kind → unit → ident → state_pc ERTL_state → res (state … ERTL_state) ≝
69 λ_.λ_.λid.λst.
70  do st ← push_ra … st (pc … st) ;
71  OK …
72   (set_frms ERTL_state (〈\fst (regs ERTL_state st),id〉 :: (st_frms … st))
73    (set_regs ERTL_state 〈empty_map …,\snd (regs … st)〉 st)).
74
75(*CSC: XXXX, for external functions only*)
76axiom ertl_fetch_external_args: external_function → state ERTL_state → call_args ERTL → res (list val).
77axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
78(* I think there should be a list beval in place of list val here
79  λvals.λ_.λst.
80  (* set all RegisterRets to 0 *)
81  let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
82  let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
83  let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
84  let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
85  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
86
87axiom FunctionNotFound: errmsg.
88
89(*CSC: here we should use helper_def_store from Joint/semantics.ma,
90  but it is not visible *)
91definition ps_reg_store_status : register → beval → state ERTL_state →
92  res (state ERTL_state) ≝
93 λdst,v,st.
94  let env ≝ regs … st in
95  ! env' ← ps_reg_store dst v env ;
96  return set_regs ERTL_state env' st.
97
98definition eval_ertl_seq:
99 ∀F. ∀globals. genv_gen F globals →
100  ertl_seq → ident → state ERTL_state →
101   res (state ERTL_state) ≝
102 λF,globals,ge,stm,id,st.
103 ! framesize ← opt_to_res … FunctionNotFound  (stack_sizes … ge id);
104 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
105  match stm with
106   [ ertl_new_frame ⇒
107      ! sp ← sp … st ;
108      let newsp ≝ shift_pointer … sp framesize in
109      return set_sp … newsp st
110   | ertl_del_frame ⇒
111      ! sp ← sp … st ;
112      let newsp ≝ shift_pointer … sp framesize in
113      return set_sp … newsp st
114   | ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st
115   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 
116
117definition ERTL_sem_uns ≝ 
118λF. mk_sem_unserialized_params ERTL ?
119  (* st_pars            ≝ *) ERTL_state
120  (* acca_store_        ≝ *) ps_reg_store
121  (* acca_retrieve_     ≝ *) ps_reg_retrieve
122  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
123  (* accb_store_        ≝ *) ps_reg_store
124  (* accb_retrieve_     ≝ *) ps_reg_retrieve
125  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
126  (* dpl_store_         ≝ *) ps_reg_store
127  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
128  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
129  (* dph_store_         ≝ *) ps_reg_store
130  (* dph_retrieve_      ≝ *) ps_reg_retrieve
131  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
132  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
133  (* pair_reg_move_     ≝ *) ertl_eval_move
134  (* save_frame         ≝ *) ertl_save_frame
135  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
136  (* fetch_external_args≝ *) ertl_fetch_external_args
137  (* set_result         ≝ *) ertl_set_result
138  (* call_args_for_main ≝ *) 0
139  (* call_dest_for_main ≝ *) it
140  (* read_result        ≝ *) (λ_.λ_.λ_.
141     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
142  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertl_seq F gl ge stm id)
143  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …).
144
145definition ERTL_semantics ≝
146  mk_sem_graph_params ERTL ERTL_sem_uns.
Note: See TracBrowser for help on using the repository browser.