source: src/ERTL/ERTL_semantics.ma @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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_semantics ≝
118  make_sem_graph_params ERTL
119  (λF. mk_sem_unserialized_params ??
120  (* st_pars            ≝ *) ERTL_state
121  (* acca_store_        ≝ *) ps_reg_store
122  (* acca_retrieve_     ≝ *) ps_reg_retrieve
123  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
124  (* accb_store_        ≝ *) ps_reg_store
125  (* accb_retrieve_     ≝ *) ps_reg_retrieve
126  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
127  (* dpl_store_         ≝ *) ps_reg_store
128  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
129  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
130  (* dph_store_         ≝ *) ps_reg_store
131  (* dph_retrieve_      ≝ *) ps_reg_retrieve
132  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
133  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
134  (* pair_reg_move_     ≝ *) ertl_eval_move
135  (* allocate_local     ≝ *) ertl_allocate_local
136  (* save_frame         ≝ *) ertl_save_frame
137  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
138  (* fetch_external_args≝ *) ertl_fetch_external_args
139  (* set_result         ≝ *) ertl_set_result
140  (* call_args_for_main ≝ *) 0
141  (* call_dest_for_main ≝ *) it
142  (* read_result        ≝ *) (λ_.λ_.λ_.
143     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
144  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertl_seq F gl ge stm id)
145  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …)).
Note: See TracBrowser for help on using the repository browser.