source: src/RTL/semantics.ma @ 1299

Last change on this file since 1299 was 1299, checked in by sacerdot, 8 years ago

Functions from RTL/semantics.ma generalized to work on every graph language
and moved into joint/SemanticUtils.ma.

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