source: src/ERTL/semantics.ma @ 1140

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

More instructions implemented.

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