source: src/RTL/semantics.ma @ 1372

Last change on this file since 1372 was 1372, checked in by sacerdot, 8 years ago

save_frame now takes the stacksize to allow RTL to allocate the stack frame

File size: 15.9 KB
Line 
1include "joint/SemanticUtils.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 *)
10include alias "common/Identifiers.ma".
11include alias "ASM/Util.ma".
12
13record frame: Type[0] ≝
14 { fr_ret_regs: list register
15 ; fr_pc: address
16 ; fr_sp: pointer
17 ; fr_carry: beval
18 ; fr_regs: register_env beval
19 }.
20
21definition rtl_more_sem_params: more_sem_params rtl_params_ :=
22 mk_more_sem_params rtl_params_
23  (list frame) (register_env beval) graph_succ_p
24   reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
25    reg_store reg_retrieve reg_store reg_retrieve
26     (λlocals,dest_src.
27       do v ← reg_retrieve locals (\snd dest_src) ;
28       reg_store (\fst dest_src) v locals)
29     pointer_of_label.
30definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
31
32definition rtl_init_locals :
33 list register → register_env beval → register_env beval ≝
34 λlocals,env.
35  foldl ?? (λlenv,reg. add … lenv reg BVundef) env locals.
36
37(*CSC: could we use here a dependent type to avoid the Error case? *)
38axiom EmptyStack: String.
39axiom OutOfBounds: String.
40
41(*CSC: we could use a dependent type here: the list of return values should have
42  the same length of the list of return registers that store the values. This
43  saves the OutOfBounds exception *)
44definition rtl_pop_frame: list beval → state … rtl_sem_params → res (state … rtl_sem_params) ≝
45 λret_vals,st.
46  let frms ≝ st_frms ? st in
47  match frms with
48  [ nil ⇒ Error ? [MSG EmptyStack]
49  | cons hd tl ⇒
50     do st ←
51      mfold_left_i ??
52       (λi.λst.λreg.
53         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
54         greg_store rtl_sem_params reg v st)
55       (OK … st) (fr_ret_regs hd) ;
56     OK …
57      (set_frms rtl_sem_params tl
58       (set_regs rtl_sem_params (fr_regs hd)
59        (set_sp … (fr_sp hd)
60         (set_pc … (fr_pc hd)
61          (set_carry … (fr_carry hd) st))))) ].
62
63definition rtl_save_frame:
64 nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
65 λstacksize,formal_arg_regs,actual_arg_regs,retregs,st.
66  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
67  do new_regs ←
68   mfold_left2 …
69    (λlenv,dest,src.
70      do v ← greg_retrieve … st src ;
71      OK … (add … lenv dest v))
72    (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
73  OK …
74   (set_frms rtl_sem_params
75    (mk_frame retregs (pc … st) (sp … st) (carry … st) (regs … st) :: (st_frms … st))
76     (set_regs rtl_sem_params new_regs
77      (set_m … mem
78       (set_sp … (mk_pointer XData b ? (mk_offset 0)) st)))).
79cases daemon (*CSC: XXXX*)
80qed.
81
82(*+ USARE GLI ARGSNO CHE SONO IN VERITA' I VALORI DEI PARAMETRI COME IN RTLABS
83+ ALLOCARE LO STACK FRAME*)
84
85definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝
86 mk_more_sem_params1 ? rtl_params1 rtl_more_sem_params
87  rtl_init_locals rtl_pop_frame rtl_save_frame.
88
89(*CSC: XXXXX, for is_final only *)
90axiom rtl_fetch_result: state rtl_sem_params → res (list beval).
91(*  let ret_vals ≝ map … (λreg.greg_retrieve rtl_sem_params st reg) ret_val_regs in
92*)
93
94(*CSC: XXXX, for external functions only*)
95axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val).
96axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params).
97
98definition rtl_exec_extended:
99 ∀globals. genv globals (rtl_params globals) →
100  rtl_statement_extension → label → state rtl_sem_params →
101   IO io_out io_in (trace × (state rtl_sem_params)) ≝
102 λglobals,ge,stm,l,st.
103  match stm with
104   [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
105      let sp ≝ sp ? st in
106      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
107      ! st ← greg_store rtl_sem_params dreg1 dpl st ;
108      ! st ← greg_store rtl_sem_params dreg2 dph st ;
109       ret ? 〈E0, goto … l st〉
110   | rtl_st_ext_call_ptr _ _ _ _ ⇒ ?
111   | rtl_st_ext_tailcall_id id regs ⇒ ?
112   | rtl_st_ext_tailcall_ptr _ _ _ ⇒ ?
113   ].
114[1,2,3: cases not_implemented ] (*CSC: tailcalls and pointer calls not implemented ATM *)
115qed.
116
117definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
118 λglobals.
119  mk_more_sem_params2 … rtl_more_sem_params1
120   (graph_fetch_statement …) rtl_fetch_result rtl_fetch_external_args rtl_set_result
121    (rtl_exec_extended …).
122
123definition rtl_fullexec ≝
124 joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)).
125
126(*
127(* CSC: external functions never fail (??) and always return something of the
128   size of one register, both in the frontend and in the backend.
129   Is this reasonable??? In OCaml it always return a list, but in the frontend
130   only the head is kept (or Undef if the list is empty) ??? *)
131
132(* CSC: carries are values and booleans are not values; so we use integers.
133   But why using values at all? To have undef? *)
134(* CSC: ???????????? *)
135axiom smerge: val → val → res val.
136(* CSC: ???????????? In OCaml: IntValue.Int32.merge
137   Note also that the translation can fail; so it should be a res int! *)
138axiom smerge2: list val → int.
139(* CSC: I have a byte, I need a value, but it is complex to do so *)
140axiom val_of_Byte: Byte → val.
141axiom Byte_of_val: val → res Byte.
142(* Map from the front-end memory model to the back-end memory model *)
143axiom represent_block: block → val × val.
144(* CSC: fixed size chunk *)
145axiom chunk: memory_chunk.
146
147definition genv ≝ (genv_t Genv) (fundef rtl_internal_function).
148
149(* CSC: added carry *)
150record frame : Type[0] ≝
151{ func   : rtl_internal_function
152; locals : register_env val
153; next   : label
154; sp     : block
155; retdst : list register
156; carry  : val
157}.
158
159(* CSC: added carry *)
160definition adv : label → frame → frame ≝
161λl,f. mk_frame (func f) (locals f) l (sp f) (retdst f) (carry f).
162
163inductive state : Type[0] ≝
164| State :
165   ∀   f : frame.
166   ∀  fs : list frame.
167   ∀   m : mem.
168   state
169| Callstate :
170   ∀  fd : fundef rtl_internal_function.
171   ∀args : list val.
172   ∀ dst : list register. (* CSC: changed from option to list *)
173   ∀ stk : list frame.
174   ∀   m : mem.
175   state
176| Returnstate :
177   (* CSC: the two lists should have the same length, but this is
178      enforced only by the semantics *)
179   ∀ rtv : list val. (* CSC: changed from option to list *)
180   ∀ dst : list register. (* CSC: changed from option to list *)
181   ∀ stk : list frame.
182   ∀   m : mem.
183   state.
184
185definition mem_of_state : state → mem ≝
186λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
187
188definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
189
190(* CSC: modified to take in input a list of registers (untyped) *)
191definition init_locals : list register → register_env val ≝
192foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
193
194definition reg_store ≝
195λreg,v,locals.
196  update RegisterTag val locals reg v.
197
198axiom WrongNumberOfParameters : String.
199
200(* CSC: modified to take in input a list of registers (untyped) *)
201let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
202match rs with
203[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
204| cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
205  let locals' ≝ add RegisterTag val locals r v in
206  params_store rst vst locals'
207] ].
208
209axiom BadRegister : String.
210
211definition reg_retrieve : register_env ? → register → res val ≝
212λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
213
214axiom FailedOp : String.
215axiom MissingSymbol : String.
216
217axiom MissingStatement : String.
218axiom FailedConstant : String.
219axiom FailedLoad : String.
220axiom FailedStore : String.
221axiom BadFunction : String.
222axiom BadJumpTable : String.
223axiom BadJumpValue : String.
224axiom FinalState : String.
225axiom ReturnMismatch : String.
226
227definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
228λge,st.
229match st with
230[ State f fs m ⇒
231  ! s ← opt_to_io … [MSG MissingStatement; CTX ? (next f)] (lookup ?? (rtl_if_graph (func f)) (next f));
232  match s with
233  [ rtl_st_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
234  | rtl_st_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
235  | rtl_st_load addrl addrh dst l ⇒  (* CSC: pairs of regs vs reg *)
236      ! vaddrh ← reg_retrieve (locals f) addrh;
237      ! vaddrl ← reg_retrieve (locals f) addrl;
238      ! vaddr ← smerge vaddrl vaddrh;
239      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
240      ! locals ← reg_store dst v (locals f);
241      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
242  | rtl_st_store addrl addrh src l ⇒  (* CSC: pairs of regs vs reg *)
243      ! vaddrh ← reg_retrieve (locals f) addrh;
244      ! vaddrl ← reg_retrieve (locals f) addrl;
245      ! vaddr ← smerge vaddrl vaddrh;
246      ! v ← reg_retrieve (locals f) src;
247      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
248      ret ? 〈E0, build_state f fs m' l〉
249  | rtl_st_call_id id args dst l ⇒
250      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
251      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
252      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
253      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
254  | rtl_st_call_ptr lfrs hfrs args dst l ⇒ (* CSC: pairs of regs vs reg *)
255      ! hfv ← reg_retrieve (locals f) hfrs;
256      ! lfv ← reg_retrieve (locals f) lfrs;
257      ! fv  ← smerge lfv hfv;
258      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
259      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
260      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
261  | rtl_st_tailcall_id id args ⇒
262      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
263      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
264      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
265      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
266  | rtl_st_tailcall_ptr lfrs hfrs args ⇒ (* CSC: pairs of regs vs reg *)
267      ! hfv ← reg_retrieve (locals f) hfrs;
268      ! lfv ← reg_retrieve (locals f) lfrs;
269      ! fv  ← smerge lfv hfv;
270      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
271      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
272      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
273  | rtl_st_return ⇒
274      (* CSC: rtl_if_result/f_result; list vs option *)
275      let dest ≝ rtl_if_result (func f) in
276      ! v ←  mmap … (reg_retrieve (locals f)) dest;
277      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
278  | rtl_st_cond src ltrue lfalse ⇒
279      ! v ← reg_retrieve (locals f) src;
280      ! b ← eval_bool_of_val v;
281      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
282  (* CSC: mismatch between the memory models and failures for the next two opx *)
283  | rtl_st_op1 op dst src l ⇒
284     ! v ← reg_retrieve (locals f) src;
285     ! v ← Byte_of_val v;
286     let v' ≝ val_of_Byte (op1 eval op v) in
287     ! locals ← reg_store dst v' (locals f);
288     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
289  | rtl_st_op2 op dst src1 src2 l ⇒
290     ! v1 ← reg_retrieve (locals f) src1;
291     ! v1 ← Byte_of_val v1;
292     ! v2 ← reg_retrieve (locals f) src2;
293     ! v2 ← Byte_of_val v2;
294     ! carry ← eval_bool_of_val (carry f);
295     let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
296     let v' ≝ val_of_Byte v' in
297     let carry ≝ of_bool carry in
298     ! locals ← reg_store dst v' (locals f);
299     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) carry) fs m〉
300
301  (* CSC: Removed: St_jumptable *)
302  (* CSC: Added: *)
303 
304  (* CSC: St_const splitted into rtl_st_int, rtl_st_addr and rt_st_stack_addr; *)
305  | rtl_st_addr ldest hdest id l ⇒
306     ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
307     let 〈laddr,haddr〉 ≝ represent_block addr in
308     ! locals ← reg_store ldest laddr (locals f);
309     ! locals ← reg_store hdest haddr locals;
310     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
311  | rtl_st_stack_addr ldest hdest l ⇒
312     let 〈laddr,haddr〉 ≝ represent_block (sp f) in
313     ! locals ← reg_store ldest laddr (locals f);
314     ! locals ← reg_store hdest haddr locals;
315     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
316  | rtl_st_int dest v l ⇒
317     ! locals ← reg_store dest (val_of_Byte v) (locals f);
318     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
319
320  (* CSC: St_op1 splitted into rtl_st_op1 and rtl_st_move *)
321  | rtl_st_move dst src l ⇒
322     ! v ← reg_retrieve (locals f) src;
323     ! locals ← reg_store dst v (locals f);
324     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
325  (* CSC: St_op2 splitted into rtl_st_op2 and rtl_st_opaccs *) 
326  | rtl_st_opaccs op dacc dbacc sacc sbacc l ⇒
327     ! v1 ← reg_retrieve (locals f) sacc;
328     ! v1 ← Byte_of_val v1;
329     ! v2 ← reg_retrieve (locals f) sbacc;
330     ! v2 ← Byte_of_val v2;
331     let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
332     let v1' ≝ val_of_Byte v1' in
333     let v2' ≝ val_of_Byte v2' in
334     ! locals ← reg_store dacc v1' (locals f);
335     ! locals ← reg_store dbacc v2' locals;
336     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
337 
338  | rtl_st_clear_carry l ⇒
339    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vfalse) fs m〉
340  | rtl_st_set_carry l ⇒
341    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vtrue) fs m〉
342  ]
343| Callstate fd params dst fs m ⇒
344    match fd with
345    [ Internal fn ⇒
346        ! locals ← params_store (rtl_if_params fn) params (init_locals (rtl_if_locals fn));
347        let 〈m', sp〉 ≝ alloc m 0 (rtl_if_stacksize fn) Any in
348        (* CSC: added carry *)
349        ret ? 〈E0, State (mk_frame fn locals (rtl_if_entry fn) sp dst Vundef) fs m'〉
350    | External fn ⇒
351        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
352        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
353        (* CSC: return type changed from option to list *)
354        (* CSC: XXX bug here; I think I should split it into Byte-long
355           components; instead I am making a singleton out of it *)
356        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉
357    ]
358| Returnstate v dst fs m ⇒
359    match fs with
360    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
361    | cons f fs' ⇒
362       ! locals ←
363         mfold_left2 ???
364          (λlocals,dst,v. reg_store dst v locals) (OK ? (locals f)) dst v;
365        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f) (carry f)) fs' m〉
366    ]
367].
368
369axiom WrongReturnValueType: String.
370
371definition is_final : state → option ((*CSC: why not res*) int) ≝
372λs. match s with
373[ State _ _ _ ⇒ None ?
374| Callstate _ _ _ _ _ ⇒ None ?
375| Returnstate v _ fs _ ⇒
376    match fs with
377     [ nil ⇒ Some ? (smerge2 v)
378     | _ ⇒ None ? ]].
379(*
380definition RTL_exec : execstep io_out io_in ≝
381  mk_execstep … ? is_final mem_of_state eval_statement.
382*)
383(* CSC: XXX the program type does not fit with the globalenv and init_mem
384definition make_initial_state : rtl_program → res (genv × state) ≝
385λp.
386  do ge ← globalenv Genv ?? p;
387  do m ← init_mem Genv ?? p;
388  let main ≝ rtl_pr_main ?? p in
389  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
390  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
391  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
392
393definition RTL_fullexec : fullexec io_out io_in ≝
394  mk_fullexec … RTL_exec ? make_initial_state.
395*)
396*)
Note: See TracBrowser for help on using the repository browser.