source: src/ERTL/semantics.ma @ 1138

Last change on this file since 1138 was 1137, checked in by sacerdot, 9 years ago

More progress.

File size: 11.0 KB
Line 
1
2(* XXX NB: I haven't checked all of these semantics against the prototype
3           compilers yet! *)
4
5include "utilities/lists.ma".
6
7include "common/Errors.ma".
8include "common/Globalenvs.ma".
9include "common/IO.ma".
10include "common/SmallstepExec.ma".
11
12include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
13
14(* CSC: external functions never fail (??) and always return something of the
15   size of one register, both in the frontend and in the backend.
16   Is this reasonable??? In OCaml it always return a list, but in the frontend
17   only the head is kept (or Undef if the list is empty) ??? *)
18
19(* CSC: carries are values and booleans are not values; so we use integers.
20   But why using values at all? To have undef? *)
21(* CSC: ???????????? *)
22axiom smerge: val → val → res val.
23(*
24(* CSC: ???????????? In OCaml: IntValue.Int32.merge
25   Note also that the translation can fail; so it should be a res int! *)
26axiom smerge2: list val → int.
27*)
28(* CSC: I have a byte, I need a value, but it is complex to do so *)
29axiom val_of_Byte: Byte → val.
30axiom Byte_of_val: val → res Byte.
31(*
32(* Map from the front-end memory model to the back-end memory model *)
33axiom represent_block: block → val × val.
34*)
35(* CSC: fixed size chunk *)
36axiom chunk: memory_chunk.
37
38axiom address: Type[0].
39(* CSC: ??? *)
40axiom address_of_label: mem → label → address.
41axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
42axiom hwreg_retrieve : mRegisterMap → Register → res val.
43axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
44
45definition genv ≝ (genv_t Genv) (fundef ertl_internal_function).
46
47(* CSC: frame reduced to this *)
48definition frame: Type[0] ≝ register_env val.
49
50record state : Type[0] ≝
51 { st_frms: list frame
52 ; pc: address
53 ; sp: address
54(* ; exit: address *)
55 ; locals: register_env val
56 ; carry: val
57 ; regs: mRegisterMap
58 ; m: mem
59 }.
60
61definition set_m: mem → state → state ≝
62 λm,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) m.
63
64definition set_locals: register_env val → state → state ≝
65 λlocals,st. mk_state (st_frms st) (pc st) (sp st) locals (carry st) (regs st) (m st).
66
67definition set_regs: mRegisterMap → state → state ≝
68 λregs,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) regs (m st).
69
70definition set_carry: val → state → state ≝
71 λcarry,st. mk_state (st_frms st) (pc st) (sp st) (locals st) carry (regs st) (m st).
72
73definition set_pc: address → state → state ≝
74 λpc,st. mk_state (st_frms st) pc (sp st) (locals st) (carry st) (regs st) (m st).
75
76(* CSC: was build_state in RTL *)
77definition goto: label → state → state ≝
78 λl,st. set_pc (address_of_label (m st) l) st.
79
80(* pushes the locals (i.e. the current frame) on top of the frames list *)
81definition save_frame: state → state ≝
82 λst. mk_state (locals st::st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) (m st).
83
84definition push: state → Byte → state ≝
85 λst,v.
86
87definition pop: state → state × Byte ≝
88 λst.
89
90definition save_ra : state → ? → state ≝
91 λst,l.
92  let 〈addrl,addrh〉 ≝ ? l in
93  let st ≝ push st addrl in
94  let st ≝ push st addrh in
95   st.
96
97definition fetch_ra : state → state × ? ≝
98 λst.
99  let 〈st,addrh〉 ≝ pop st in
100  let 〈st,addrl〉 ≝ pop st in
101   〈st, ? addrl addrh〉.
102
103(*CSC: To be implemented *)
104axiom fetch_statement: state → res ertl_statement.
105
106definition init_locals : list register → register_env val ≝
107foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
108
109definition reg_store ≝
110λreg,v,locals. update RegisterTag val locals reg v.
111
112(*
113axiom WrongNumberOfParameters : String.
114
115(* CSC: modified to take in input a list of registers (untyped) *)
116let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
117match rs with
118[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
119| cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
120  let locals' ≝ add RegisterTag val locals r v in
121  params_store rst vst locals'
122] ].
123*)
124
125axiom BadRegister : String.
126
127definition reg_retrieve : register_env val → register → res val ≝
128λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
129
130(*
131axiom FailedOp : String.
132*)
133axiom MissingSymbol : String.
134(*
135axiom MissingStatement : String.
136axiom FailedConstant : String. *)
137axiom FailedLoad : String.
138axiom FailedStore : String.
139axiom BadFunction : String.
140(*axiom BadJumpTable : String.
141axiom BadJumpValue : String.
142axiom FinalState : String.
143axiom ReturnMismatch : String.
144*)
145
146definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
147λge,st.
148  ! s ← fetch_statement st;
149  match s with
150  [ ertl_st_skip l ⇒ ret ? 〈E0, goto l st〉
151  | ertl_st_cost cl l ⇒ ret ? 〈Echarge cl, goto l st〉
152  | ertl_st_int dest v l ⇒
153     ! locals ← reg_store dest (val_of_Byte v) (locals st);
154     ret ? 〈E0, goto l (set_locals locals st)〉
155  | ertl_st_load addrl addrh dst l ⇒
156      ! vaddrh ← reg_retrieve (locals st) addrh;
157      ! vaddrl ← reg_retrieve (locals st) addrl;
158      ! vaddr ← smerge vaddrl vaddrh;
159      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
160      ! locals ← reg_store dst v (locals st);
161      ret ? 〈E0, goto l (set_locals locals st)〉
162  | ertl_st_store addrl addrh src l ⇒
163      ! vaddrh ← reg_retrieve (locals st) addrh;
164      ! vaddrl ← reg_retrieve (locals st) addrl;
165      ! vaddr ← smerge vaddrl vaddrh;
166      ! v ← reg_retrieve (locals st) src;
167      ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
168      ret ? 〈E0, goto l (set_m m' st)〉
169  | ertl_st_cond src ltrue lfalse ⇒
170      ! v ← reg_retrieve (locals st) src;
171      ! b ← eval_bool_of_val v;
172      ret ? 〈E0, goto (if b then ltrue else lfalse) st〉
173(*  | ertl_st_addr ldest hdest id l ⇒
174     ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
175     let 〈laddr,haddr〉 ≝ represent_block addr in
176     ! locals ← reg_store ldest laddr (locals st);
177     ! locals ← reg_store hdest haddr locals;
178     ret ? 〈E0, goto l (set_locals locals st)〉
179*)  | ertl_st_op1 op dst src l ⇒
180     ! v ← reg_retrieve (locals st) src;
181     ! v ← Byte_of_val v;
182     let v' ≝ val_of_Byte (op1 eval op v) in
183     ! locals ← reg_store dst v' (locals st);
184     ret ? 〈E0, goto l (set_locals locals st)〉
185  | ertl_st_op2 op dst src1 src2 l ⇒
186     ! v1 ← reg_retrieve (locals st) src1;
187     ! v1 ← Byte_of_val v1;
188     ! v2 ← reg_retrieve (locals st) src2;
189     ! v2 ← Byte_of_val v2;
190     ! carry ← eval_bool_of_val (carry st);
191     let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
192     let v' ≝ val_of_Byte v' in
193     let carry ≝ of_bool carry in
194     ! locals ← reg_store dst v' (locals st);
195     ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
196(*  | ertl_st_opaccs op dacc dbacc sacc sbacc l ⇒
197     ! v1 ← reg_retrieve (locals st) sacc;
198     ! v1 ← Byte_of_val v1;
199     ! v2 ← reg_retrieve (locals st) sbacc;
200     ! v2 ← Byte_of_val v2;
201     let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
202     let v1' ≝ val_of_Byte v1' in
203     let v2' ≝ val_of_Byte v2' in
204     ! locals ← reg_store dacc v1' (locals st);
205     ! locals ← reg_store dbacc v2' locals;
206     ret ? 〈E0, goto l (set_locals locals st)〉 *)
207  | ertl_st_clear_carry l ⇒
208    ret ? 〈E0, goto l (set_carry Vfalse st)〉
209  | ertl_st_set_carry l ⇒
210    ret ? 〈E0, goto l (set_carry Vtrue st)〉
211     
212  (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,
213         ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would
214         be more than enough... *)
215  | ertl_st_move dst src l ⇒
216     ! v ← reg_retrieve (locals st) src;
217     ! locals ← reg_store dst v (locals st);
218     ret ? 〈E0, goto l (set_locals locals st)〉
219  | ertl_st_hdw_to_hdw dst src l ⇒
220     ! v ← hwreg_retrieve (regs st) src;
221     ! regs ← hwreg_store dst v (regs st);
222     ret ? 〈E0, goto l (set_regs regs st)〉
223  | ertl_st_get_hdw dst src l ⇒
224     ! v ← hwreg_retrieve (regs st) src;
225     ! locals ← reg_store dst v (locals st);
226     ret ? 〈E0, goto l (set_locals locals st)〉
227  | ertl_st_set_hdw dst src l ⇒
228     ! v ← reg_retrieve (locals st) src;
229     ! regs ← hwreg_store dst v (regs st);
230     ret ? 〈E0, goto l (set_regs regs st)〉
231
232  (* CSC: Dropped:
233      - rtl_st_stackaddr (becomes two get_hdw)
234      - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM)
235      - rtl_st_call_ptr (unimplemented ATM) *)
236     
237  (* CSC: changed, where the meat is *)
238  | ertl_st_call_id id argsno l ⇒ (* CSC: only the number of args kept, no return reg *)
239      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
240      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
241      match fd with
242      [ Internal fn ⇒
243        let st ≝ save_ra st l in
244        let st ≝ save_frame st in
245        let locals ≝ init_locals (ertl_if_locals fn) in
246        let pc ≝ ertl_if_entry fn in
247         goto pc (set_locals locals st)
248      | External fn ⇒ ? (*
249        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
250        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
251        (* CSC: return type changed from option to list *)
252        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉 *)
253      ]
254(*     
255     
256      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
257      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
258*)   
259
260  | _ ⇒ ? ]
261(*
262  | rtl_st_return ⇒
263      let dest ≝ rtl_if_result (func f) in
264      ! v ←  mmap … (reg_retrieve (locals f)) dest;
265      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
266  ]
267| Returnstate v dst fs m ⇒
268    match fs with
269    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
270    | cons f fs' ⇒
271       ! locals ←
272         mfold_left2 ???
273          (λlocals,dst,v. reg_store dst v locals) (OK ? (locals f)) dst v;
274        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f) (carry f)) fs' m〉
275    ]
276]*).
277
278axiom WrongReturnValueType: String.
279
280definition is_final : state → option ((*CSC: why not res*) int) ≝
281λs. match s with
282[ State _ _ _ ⇒ None ?
283| Callstate _ _ _ _ _ ⇒ None ?
284| Returnstate v _ fs _ ⇒
285    match fs with
286     [ nil ⇒ Some ? (smerge2 v)
287     | _ ⇒ None ? ]].
288
289definition RTL_exec : execstep io_out io_in ≝
290  mk_execstep … ? is_final mem_of_state eval_statement.
291
292(* CSC: XXX the program type does not fit with the globalenv and init_mem
293definition make_initial_state : rtl_program → res (genv × state) ≝
294λp.
295  do ge ← globalenv Genv ?? p;
296  do m ← init_mem Genv ?? p;
297  let main ≝ rtl_pr_main ?? p in
298  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
299  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
300  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
301
302definition RTL_fullexec : fullexec io_out io_in ≝
303  mk_fullexec … RTL_exec ? make_initial_state.
304*)
Note: See TracBrowser for help on using the repository browser.