source: src/RTL/semantics.ma @ 1294

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

RTL semantics: porting to joint semantics started.

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