source: src/RTL/semantics.ma @ 1298

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