source: src/RTL/semantics.ma @ 1376

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

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