source: src/RTL/semantics.ma @ 1295

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

More progress.

File size: 14.0 KB
Line 
1include "joint/semantics.ma".
2(*
3include "utilities/lists.ma".
4include "common/Errors.ma".
5include "common/Globalenvs.ma".
6include "common/IO.ma".
7include "common/SmallstepExec.ma".
8*)
9include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
10
11(*CSC: XXXX; we need to create a brand new chunk per label, so that
12  pointer operations on labels are not semantically valid!! *)
13axiom rtl_pointer_of_label: label → Σp:pointer. ptype p = Code.
14
15(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
16  Maybe there is a better way to organize the code!!! *)
17definition rtl_succ_p: label → address → address.
18 #l #_ generalize in match (refl … (beval_pair_of_pointer (rtl_pointer_of_label l)))
19 cases (beval_pair_of_pointer (rtl_pointer_of_label l)) in ⊢ (???% → ?)
20  [ #res #_ @res
21  | #msg cases (rtl_pointer_of_label l) * * #q #com #off #E1 #E2 destruct ]
22qed.
23
24axiom rtl_pop_frame: unit → res unit.
25axiom rtl_save_frame: unit → register_env beval → unit.
26
27
28axiom BadRegister : String.
29definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
30definition reg_retrieve : register_env beval → register → res beval ≝
31 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
32
33definition rtl_more_sem_params: more_sem_params rtl_params_ :=
34 mk_more_sem_params rtl_params_
35  unit(*framesT*) (register_env beval) rtl_succ_p rtl_pop_frame rtl_save_frame
36   reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
37    reg_store reg_retrieve reg_store reg_retrieve
38     (λlocals,dest_src.
39       do v ← reg_retrieve locals (\snd dest_src) ;
40       reg_store (\fst dest_src) v locals)
41     rtl_pointer_of_label.
42definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
43
44(*CSC: XXXXX *)
45axiom rtl_init_locals : list register → register_env beval.
46axiom rtl_fetch_statement: ∀globals. state rtl_sem_params → res (rtl_statement globals).
47
48axiom rtl_fetch_result: state rtl_sem_params → nat → res val.
49
50(*CSC: XXXX, for external functions only*)
51axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val).
52axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params).
53
54axiom rtl_exec_extended: ∀globals. genv globals (rtl_params globals) → rtl_statement_extension → state rtl_sem_params → IO io_out io_in (trace × (state rtl_sem_params)).
55
56definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) :=
57 λglobals.
58  mk_more_sem_params2 … rtl_more_sem_params rtl_init_locals
59   (rtl_fetch_statement …) rtl_fetch_result rtl_fetch_external_args rtl_set_result
60    (rtl_exec_extended …).
61
62definition rtl_fullexec ≝
63 joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)).
64
65(*
66(* CSC: external functions never fail (??) and always return something of the
67   size of one register, both in the frontend and in the backend.
68   Is this reasonable??? In OCaml it always return a list, but in the frontend
69   only the head is kept (or Undef if the list is empty) ??? *)
70
71(* CSC: carries are values and booleans are not values; so we use integers.
72   But why using values at all? To have undef? *)
73(* CSC: ???????????? *)
74axiom smerge: val → val → res val.
75(* CSC: ???????????? In OCaml: IntValue.Int32.merge
76   Note also that the translation can fail; so it should be a res int! *)
77axiom smerge2: list val → int.
78(* CSC: I have a byte, I need a value, but it is complex to do so *)
79axiom val_of_Byte: Byte → val.
80axiom Byte_of_val: val → res Byte.
81(* Map from the front-end memory model to the back-end memory model *)
82axiom represent_block: block → val × val.
83(* CSC: fixed size chunk *)
84axiom chunk: memory_chunk.
85
86definition genv ≝ (genv_t Genv) (fundef rtl_internal_function).
87
88(* CSC: added carry *)
89record frame : Type[0] ≝
90{ func   : rtl_internal_function
91; locals : register_env val
92; next   : label
93; sp     : block
94; retdst : list register
95; carry  : val
96}.
97
98(* CSC: added carry *)
99definition adv : label → frame → frame ≝
100λl,f. mk_frame (func f) (locals f) l (sp f) (retdst f) (carry f).
101
102inductive state : Type[0] ≝
103| State :
104   ∀   f : frame.
105   ∀  fs : list frame.
106   ∀   m : mem.
107   state
108| Callstate :
109   ∀  fd : fundef rtl_internal_function.
110   ∀args : list val.
111   ∀ dst : list register. (* CSC: changed from option to list *)
112   ∀ stk : list frame.
113   ∀   m : mem.
114   state
115| Returnstate :
116   (* CSC: the two lists should have the same length, but this is
117      enforced only by the semantics *)
118   ∀ rtv : list val. (* CSC: changed from option to list *)
119   ∀ dst : list register. (* CSC: changed from option to list *)
120   ∀ stk : list frame.
121   ∀   m : mem.
122   state.
123
124definition mem_of_state : state → mem ≝
125λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
126
127definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
128
129(* CSC: modified to take in input a list of registers (untyped) *)
130definition init_locals : list register → register_env val ≝
131foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
132
133definition reg_store ≝
134λreg,v,locals.
135  update RegisterTag val locals reg v.
136
137axiom WrongNumberOfParameters : String.
138
139(* CSC: modified to take in input a list of registers (untyped) *)
140let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
141match rs with
142[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
143| cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
144  let locals' ≝ add RegisterTag val locals r v in
145  params_store rst vst locals'
146] ].
147
148axiom BadRegister : String.
149
150definition reg_retrieve : register_env ? → register → res val ≝
151λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
152
153axiom FailedOp : String.
154axiom MissingSymbol : String.
155
156axiom MissingStatement : String.
157axiom FailedConstant : String.
158axiom FailedLoad : String.
159axiom FailedStore : String.
160axiom BadFunction : String.
161axiom BadJumpTable : String.
162axiom BadJumpValue : String.
163axiom FinalState : String.
164axiom ReturnMismatch : String.
165
166definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
167λge,st.
168match st with
169[ State f fs m ⇒
170  ! s ← opt_to_io … [MSG MissingStatement; CTX ? (next f)] (lookup ?? (rtl_if_graph (func f)) (next f));
171  match s with
172  [ rtl_st_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
173  | rtl_st_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
174  | rtl_st_load addrl addrh dst l ⇒  (* CSC: pairs of regs vs reg *)
175      ! vaddrh ← reg_retrieve (locals f) addrh;
176      ! vaddrl ← reg_retrieve (locals f) addrl;
177      ! vaddr ← smerge vaddrl vaddrh;
178      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
179      ! locals ← reg_store dst v (locals f);
180      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
181  | rtl_st_store addrl addrh src l ⇒  (* CSC: pairs of regs vs reg *)
182      ! vaddrh ← reg_retrieve (locals f) addrh;
183      ! vaddrl ← reg_retrieve (locals f) addrl;
184      ! vaddr ← smerge vaddrl vaddrh;
185      ! v ← reg_retrieve (locals f) src;
186      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
187      ret ? 〈E0, build_state f fs m' l〉
188  | rtl_st_call_id id args dst l ⇒
189      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
190      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
191      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
192      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
193  | rtl_st_call_ptr lfrs hfrs args dst l ⇒ (* CSC: pairs of regs vs reg *)
194      ! hfv ← reg_retrieve (locals f) hfrs;
195      ! lfv ← reg_retrieve (locals f) lfrs;
196      ! fv  ← smerge lfv hfv;
197      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
198      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
199      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
200  | rtl_st_tailcall_id id args ⇒
201      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
202      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
203      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
204      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
205  | rtl_st_tailcall_ptr lfrs hfrs args ⇒ (* CSC: pairs of regs vs reg *)
206      ! hfv ← reg_retrieve (locals f) hfrs;
207      ! lfv ← reg_retrieve (locals f) lfrs;
208      ! fv  ← smerge lfv hfv;
209      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
210      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
211      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
212  | rtl_st_return ⇒
213      (* CSC: rtl_if_result/f_result; list vs option *)
214      let dest ≝ rtl_if_result (func f) in
215      ! v ←  mmap … (reg_retrieve (locals f)) dest;
216      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
217  | rtl_st_cond src ltrue lfalse ⇒
218      ! v ← reg_retrieve (locals f) src;
219      ! b ← eval_bool_of_val v;
220      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
221  (* CSC: mismatch between the memory models and failures for the next two opx *)
222  | rtl_st_op1 op dst src l ⇒
223     ! v ← reg_retrieve (locals f) src;
224     ! v ← Byte_of_val v;
225     let v' ≝ val_of_Byte (op1 eval op v) in
226     ! locals ← reg_store dst v' (locals f);
227     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
228  | rtl_st_op2 op dst src1 src2 l ⇒
229     ! v1 ← reg_retrieve (locals f) src1;
230     ! v1 ← Byte_of_val v1;
231     ! v2 ← reg_retrieve (locals f) src2;
232     ! v2 ← Byte_of_val v2;
233     ! carry ← eval_bool_of_val (carry f);
234     let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
235     let v' ≝ val_of_Byte v' in
236     let carry ≝ of_bool carry in
237     ! locals ← reg_store dst v' (locals f);
238     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) carry) fs m〉
239
240  (* CSC: Removed: St_jumptable *)
241  (* CSC: Added: *)
242 
243  (* CSC: St_const splitted into rtl_st_int, rtl_st_addr and rt_st_stack_addr; *)
244  | rtl_st_addr ldest hdest id l ⇒
245     ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
246     let 〈laddr,haddr〉 ≝ represent_block addr in
247     ! locals ← reg_store ldest laddr (locals f);
248     ! locals ← reg_store hdest haddr locals;
249     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
250  | rtl_st_stack_addr ldest hdest l ⇒
251     let 〈laddr,haddr〉 ≝ represent_block (sp f) in
252     ! locals ← reg_store ldest laddr (locals f);
253     ! locals ← reg_store hdest haddr locals;
254     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
255  | rtl_st_int dest v l ⇒
256     ! locals ← reg_store dest (val_of_Byte v) (locals f);
257     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
258
259  (* CSC: St_op1 splitted into rtl_st_op1 and rtl_st_move *)
260  | rtl_st_move dst src l ⇒
261     ! v ← reg_retrieve (locals f) src;
262     ! locals ← reg_store dst v (locals f);
263     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
264  (* CSC: St_op2 splitted into rtl_st_op2 and rtl_st_opaccs *) 
265  | rtl_st_opaccs op dacc dbacc sacc sbacc l ⇒
266     ! v1 ← reg_retrieve (locals f) sacc;
267     ! v1 ← Byte_of_val v1;
268     ! v2 ← reg_retrieve (locals f) sbacc;
269     ! v2 ← Byte_of_val v2;
270     let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
271     let v1' ≝ val_of_Byte v1' in
272     let v2' ≝ val_of_Byte v2' in
273     ! locals ← reg_store dacc v1' (locals f);
274     ! locals ← reg_store dbacc v2' locals;
275     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
276 
277  | rtl_st_clear_carry l ⇒
278    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vfalse) fs m〉
279  | rtl_st_set_carry l ⇒
280    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vtrue) fs m〉
281  ]
282| Callstate fd params dst fs m ⇒
283    match fd with
284    [ Internal fn ⇒
285        ! locals ← params_store (rtl_if_params fn) params (init_locals (rtl_if_locals fn));
286        let 〈m', sp〉 ≝ alloc m 0 (rtl_if_stacksize fn) Any in
287        (* CSC: added carry *)
288        ret ? 〈E0, State (mk_frame fn locals (rtl_if_entry fn) sp dst Vundef) fs m'〉
289    | External fn ⇒
290        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
291        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
292        (* CSC: return type changed from option to list *)
293        (* CSC: XXX bug here; I think I should split it into Byte-long
294           components; instead I am making a singleton out of it *)
295        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉
296    ]
297| Returnstate v dst fs m ⇒
298    match fs with
299    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
300    | cons f fs' ⇒
301       ! locals ←
302         mfold_left2 ???
303          (λlocals,dst,v. reg_store dst v locals) (OK ? (locals f)) dst v;
304        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f) (carry f)) fs' m〉
305    ]
306].
307
308axiom WrongReturnValueType: String.
309
310definition is_final : state → option ((*CSC: why not res*) int) ≝
311λs. match s with
312[ State _ _ _ ⇒ None ?
313| Callstate _ _ _ _ _ ⇒ None ?
314| Returnstate v _ fs _ ⇒
315    match fs with
316     [ nil ⇒ Some ? (smerge2 v)
317     | _ ⇒ None ? ]].
318(*
319definition RTL_exec : execstep io_out io_in ≝
320  mk_execstep … ? is_final mem_of_state eval_statement.
321*)
322(* CSC: XXX the program type does not fit with the globalenv and init_mem
323definition make_initial_state : rtl_program → res (genv × state) ≝
324λp.
325  do ge ← globalenv Genv ?? p;
326  do m ← init_mem Genv ?? p;
327  let main ≝ rtl_pr_main ?? p in
328  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
329  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
330  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
331
332definition RTL_fullexec : fullexec io_out io_in ≝
333  mk_fullexec … RTL_exec ? make_initial_state.
334*)
335*)
Note: See TracBrowser for help on using the repository browser.