source: src/ERTL/ERTL_semantics.ma @ 2946

Last change on this file since 2946 was 2946, checked in by tranquil, 7 years ago

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File size: 6.0 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  let res ≝ reg_store r v (\fst local_env) in
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 × (Σb:block.block_region b=Code)))
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
66definition ertl_save_frame:
67 call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
68 λ_.λ_.λst.
69  ! st' ← push_ra … st (pc … st) ;
70  ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st');
71  return
72  (set_frms ERTL_state
73  (〈\fst (regs ERTL_state st'),(pc_block (pc ? st))〉 :: frms)
74    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
75
76definition ertl_pop_frame:
77 state ERTL_state →
78   res (state ERTL_state × program_counter) ≝
79 λst.
80 ! frms ← opt_to_res ? [MSG FrameErrorOnPop] (st_frms … st);
81 match frms with
82 [ nil ⇒ Error ? [MSG FramesEmptyOnPop]
83 | cons hd tl ⇒
84   let 〈local_mem, bl〉 ≝ hd in
85   let st' ≝ set_regs ERTL_state 〈local_mem, \snd (regs … st)〉
86      (set_frms ERTL_state tl st) in
87   ! 〈st'', pc〉 ← pop_ra … st' ;
88   if eq_block bl (pc_block pc) then
89     OK … 〈st'', pc〉
90   else Error ? [MSG BlockInFramesCorrupted]
91 ].
92
93(*CSC: XXXX, for external functions only*)
94axiom ertl_fetch_external_args: external_function → state ERTL_state → call_args ERTL → res (list val).
95axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
96(* I think there should be a list beval in place of list val here
97  λvals.λ_.λst.
98  (* set all RegisterRets to 0 *)
99  let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
100  let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
101  let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
102  let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
103  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
104
105(*CSC: here we should use helper_def_store from Joint/semantics.ma,
106  but it is not visible *)
107definition ps_reg_store_status : register → beval → state ERTL_state →
108  res (state ERTL_state) ≝
109 λdst,v,st.
110  let env ≝ regs … st in
111  ! env' ← ps_reg_store dst v env ;
112  return set_regs ERTL_state env' st.
113
114definition eval_ertl_seq:
115 ∀F. ∀globals. genv_gen F globals →
116  ertl_seq → ident → state ERTL_state →
117   res (state ERTL_state) ≝
118 λF,globals,ge,stm,id,st.
119 ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
120 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
121  match stm with
122   [ ertl_new_frame ⇒
123      ! sp ← sp … st ;
124      let newsp ≝ neg_shift_pointer … sp framesize in
125      return set_sp … newsp st
126   | ertl_del_frame ⇒
127      ! sp ← sp … st ;
128      let newsp ≝ shift_pointer … sp framesize in
129      return set_sp … newsp st
130   | ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st
131   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 
132
133definition ERTL_sem_uns ≝ 
134λF. mk_sem_unserialized_params ERTL ?
135  (* st_pars            ≝ *) ERTL_state
136  (* acca_store_        ≝ *) ps_reg_store
137  (* acca_retrieve_     ≝ *) ps_reg_retrieve
138  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
139  (* accb_store_        ≝ *) ps_reg_store
140  (* accb_retrieve_     ≝ *) ps_reg_retrieve
141  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
142  (* dpl_store_         ≝ *) ps_reg_store
143  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
144  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
145  (* dph_store_         ≝ *) ps_reg_store
146  (* dph_retrieve_      ≝ *) ps_reg_retrieve
147  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
148  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
149  (* pair_reg_move_     ≝ *) ertl_eval_move
150  (* save_frame         ≝ *) ertl_save_frame
151  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
152  (* fetch_external_args≝ *) ertl_fetch_external_args
153  (* set_result         ≝ *) ertl_set_result
154  (* call_args_for_main ≝ *) 0
155  (* call_dest_for_main ≝ *) it
156  (* read_result        ≝ *) (λ_.λ_.λ_.
157     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
158  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertl_seq F gl ge stm id)
159  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.ertl_pop_frame).
160
161definition ERTL_semantics ≝
162  mk_sem_graph_params ERTL ERTL_sem_uns ERTL_premain.
Note: See TracBrowser for help on using the repository browser.