source: src/RTL/semantics.ma @ 1324

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

The semantics of extended statements must also consider the label since
the program counter is not automatically incremented
(because of cond instructions :-(

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