source: src/RTL/semantics.ma @ 1371

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

save_frame changed to accept also the formal/actual argument pairs, required
in the RTL semantics. The function returns now a res, but this could be fixed
with a dependent type for function call to disallow calling a function with the
wrong arguments.

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