source: src/ERTL/semantics.ma @ 1130

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

File in progress (copied from RTL).
All instructions considered up to function call/return.

File size: 11.6 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
76definition goto: label → state → state ≝
77 λl,st. set_pc (address_of_label (m st) l) st.
78
79(*CSC: To be implemented *)
80axiom fetch_statement: state → res ertl_statement.
81
82(*
83definition mem_of_state : state → mem ≝
84λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
85
86definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
87
88(* CSC: modified to take in input a list of registers (untyped) *)
89definition init_locals : list register → register_env val ≝
90foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
91*)
92
93definition reg_store ≝
94λreg,v,locals. update RegisterTag val locals reg v.
95
96(*
97axiom WrongNumberOfParameters : String.
98
99(* CSC: modified to take in input a list of registers (untyped) *)
100let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
101match rs with
102[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
103| cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
104  let locals' ≝ add RegisterTag val locals r v in
105  params_store rst vst locals'
106] ].
107*)
108
109axiom BadRegister : String.
110
111definition reg_retrieve : register_env val → register → res val ≝
112λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
113
114(*
115axiom FailedOp : String.
116axiom MissingSymbol : String.
117
118axiom MissingStatement : String.
119axiom FailedConstant : String. *)
120axiom FailedLoad : String.
121axiom FailedStore : String.
122(*axiom BadFunction : String.
123axiom BadJumpTable : String.
124axiom BadJumpValue : String.
125axiom FinalState : String.
126axiom ReturnMismatch : String.
127*)
128
129definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
130λge,st.
131  ! s ← fetch_statement st;
132  match s with
133  [ ertl_st_skip l ⇒ ret ? 〈E0, goto l st〉
134  | ertl_st_cost cl l ⇒ ret ? 〈Echarge cl, goto l st〉
135  | ertl_st_int dest v l ⇒
136     ! locals ← reg_store dest (val_of_Byte v) (locals st);
137     ret ? 〈E0, goto l (set_locals locals st)〉
138  | ertl_st_load addrl addrh dst l ⇒
139      ! vaddrh ← reg_retrieve (locals st) addrh;
140      ! vaddrl ← reg_retrieve (locals st) addrl;
141      ! vaddr ← smerge vaddrl vaddrh;
142      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
143      ! locals ← reg_store dst v (locals st);
144      ret ? 〈E0, goto l (set_locals locals st)〉
145  | ertl_st_store addrl addrh src l ⇒
146      ! vaddrh ← reg_retrieve (locals st) addrh;
147      ! vaddrl ← reg_retrieve (locals st) addrl;
148      ! vaddr ← smerge vaddrl vaddrh;
149      ! v ← reg_retrieve (locals st) src;
150      ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
151      ret ? 〈E0, goto l (set_m m' st)〉
152  | ertl_st_cond src ltrue lfalse ⇒
153      ! v ← reg_retrieve (locals st) src;
154      ! b ← eval_bool_of_val v;
155      ret ? 〈E0, goto (if b then ltrue else lfalse) st〉
156(*  | ertl_st_addr ldest hdest id l ⇒
157     ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
158     let 〈laddr,haddr〉 ≝ represent_block addr in
159     ! locals ← reg_store ldest laddr (locals st);
160     ! locals ← reg_store hdest haddr locals;
161     ret ? 〈E0, goto l (set_locals locals st)〉
162*)  | ertl_st_op1 op dst src l ⇒
163     ! v ← reg_retrieve (locals st) src;
164     ! v ← Byte_of_val v;
165     let v' ≝ val_of_Byte (op1 eval op v) in
166     ! locals ← reg_store dst v' (locals st);
167     ret ? 〈E0, goto l (set_locals locals st)〉
168  | ertl_st_op2 op dst src1 src2 l ⇒
169     ! v1 ← reg_retrieve (locals st) src1;
170     ! v1 ← Byte_of_val v1;
171     ! v2 ← reg_retrieve (locals st) src2;
172     ! v2 ← Byte_of_val v2;
173     ! carry ← eval_bool_of_val (carry st);
174     let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
175     let v' ≝ val_of_Byte v' in
176     let carry ≝ of_bool carry in
177     ! locals ← reg_store dst v' (locals st);
178     ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
179(*  | ertl_st_opaccs op dacc dbacc sacc sbacc l ⇒
180     ! v1 ← reg_retrieve (locals st) sacc;
181     ! v1 ← Byte_of_val v1;
182     ! v2 ← reg_retrieve (locals st) sbacc;
183     ! v2 ← Byte_of_val v2;
184     let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
185     let v1' ≝ val_of_Byte v1' in
186     let v2' ≝ val_of_Byte v2' in
187     ! locals ← reg_store dacc v1' (locals st);
188     ! locals ← reg_store dbacc v2' locals;
189     ret ? 〈E0, goto l (set_locals locals st)〉 *)
190  | ertl_st_clear_carry l ⇒
191    ret ? 〈E0, goto l (set_carry Vfalse st)〉
192  | ertl_st_set_carry l ⇒
193    ret ? 〈E0, goto l (set_carry Vtrue st)〉
194
195     
196  (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,
197         ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would
198         be more than enough... *)
199  | ertl_st_move dst src l ⇒
200     ! v ← reg_retrieve (locals st) src;
201     ! locals ← reg_store dst v (locals st);
202     ret ? 〈E0, goto l (set_locals locals st)〉
203  | ertl_st_hdw_to_hdw dst src l ⇒
204     ! v ← hwreg_retrieve (regs st) src;
205     ! regs ← hwreg_store dst v (regs st);
206     ret ? 〈E0, goto l (set_regs regs st)〉
207  | ertl_st_get_hdw dst src l ⇒
208     ! v ← hwreg_retrieve (regs st) src;
209     ! locals ← reg_store dst v (locals st);
210     ret ? 〈E0, goto l (set_locals locals st)〉
211  | ertl_st_set_hdw dst src l ⇒
212     ! v ← reg_retrieve (locals st) src;
213     ! regs ← hwreg_store dst v (regs st);
214     ret ? 〈E0, goto l (set_regs regs st)〉
215
216  (* CSC: Dropped: rtl_st_stackaddr (becomes two get_hdw) *)
217
218  | _ ⇒ ? ]
219(*
220  | rtl_st_call_id id args dst l ⇒
221      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
222      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
223      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
224      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
225  | rtl_st_call_ptr lfrs hfrs args dst l ⇒ (* CSC: pairs of regs vs reg *)
226      ! hfv ← reg_retrieve (locals f) hfrs;
227      ! lfv ← reg_retrieve (locals f) lfrs;
228      ! fv  ← smerge lfv hfv;
229      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
230      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
231      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
232  | rtl_st_tailcall_id id args ⇒
233      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
234      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
235      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
236      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
237  | rtl_st_tailcall_ptr lfrs hfrs args ⇒ (* CSC: pairs of regs vs reg *)
238      ! hfv ← reg_retrieve (locals f) hfrs;
239      ! lfv ← reg_retrieve (locals f) lfrs;
240      ! fv  ← smerge lfv hfv;
241      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
242      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
243      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
244  | rtl_st_return ⇒
245      (* CSC: rtl_if_result/f_result; list vs option *)
246      let dest ≝ rtl_if_result (func f) in
247      ! v ←  mmap … (reg_retrieve (locals f)) dest;
248      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
249  ]
250| Callstate fd params dst fs m ⇒
251    match fd with
252    [ Internal fn ⇒
253        ! locals ← params_store (rtl_if_params fn) params (init_locals (rtl_if_locals fn));
254        let 〈m', sp〉 ≝ alloc m 0 (rtl_if_stacksize fn) Any in
255        (* CSC: added carry *)
256        ret ? 〈E0, State (mk_frame fn locals (rtl_if_entry fn) sp dst Vundef) fs m'〉
257    | External fn ⇒
258        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
259        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
260        (* CSC: return type changed from option to list *)
261        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉
262    ]
263| Returnstate v dst fs m ⇒
264    match fs with
265    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
266    | cons f fs' ⇒
267       ! locals ←
268         mfold_left2 ???
269          (λlocals,dst,v. reg_store dst v locals) (OK ? (locals f)) dst v;
270        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f) (carry f)) fs' m〉
271    ]
272]*).
273
274axiom WrongReturnValueType: String.
275
276definition is_final : state → option ((*CSC: why not res*) int) ≝
277λs. match s with
278[ State _ _ _ ⇒ None ?
279| Callstate _ _ _ _ _ ⇒ None ?
280| Returnstate v _ fs _ ⇒
281    match fs with
282     [ nil ⇒ Some ? (smerge2 v)
283     | _ ⇒ None ? ]].
284
285definition RTL_exec : execstep io_out io_in ≝
286  mk_execstep … ? is_final mem_of_state eval_statement.
287
288(* CSC: XXX the program type does not fit with the globalenv and init_mem
289definition make_initial_state : rtl_program → res (genv × state) ≝
290λp.
291  do ge ← globalenv Genv ?? p;
292  do m ← init_mem Genv ?? p;
293  let main ≝ rtl_pr_main ?? p in
294  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
295  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
296  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
297
298definition RTL_fullexec : fullexec io_out io_in ≝
299  mk_fullexec … RTL_exec ? make_initial_state.
300*)
Note: See TracBrowser for help on using the repository browser.