source: src/RTL/semantics.ma @ 1122

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

Internal function call implemented too.

File size: 11.5 KB
Line 
1
2(* XXX NB: I haven't checked all of these semantics against the prototype
3           compilers yet! *)
4
5include "utilities/lists.ma".
6
7include "common/Errors.ma".
8include "common/Globalenvs.ma".
9include "common/IO.ma".
10include "common/SmallstepExec.ma".
11
12include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
13
14(* CSC: external functions never fail (??) and always return something of the
15   size of one register, both in the frontend and in the backend.
16   Is this reasonable??? In OCaml it always return a list, but in the frontend
17   only the head is kept (or Undef if the list is empty) ??? *)
18
19(* CSC: carries are values and booleans are not values; so we use integers.
20   But why using values at all? To have undef? *)
21(* CSC: ???????????? *)
22axiom smerge: val → val → res val.
23(* CSC: I have a byte, I need a value, but it is complex to do so *)
24axiom val_of_Byte: Byte → val.
25axiom Byte_of_val: val → res Byte.
26(* Map from the front-end memory model to the back-end memory model *)
27axiom represent_block: block → val × val.
28(* CSC: fixed size chunk *)
29axiom chunk: memory_chunk.
30
31definition genv ≝ (genv_t Genv) (fundef rtl_internal_function).
32
33(* CSC: added carry *)
34record frame : Type[0] ≝
35{ func   : rtl_internal_function
36; locals : register_env val
37; next   : label
38; sp     : block
39; retdst : list register
40; carry  : val
41}.
42
43(* CSC: added carry *)
44definition adv : label → frame → frame ≝
45λl,f. mk_frame (func f) (locals f) l (sp f) (retdst f) (carry f).
46
47inductive state : Type[0] ≝
48| State :
49   ∀   f : frame.
50   ∀  fs : list frame.
51   ∀   m : mem.
52   state
53| Callstate :
54   ∀  fd : fundef rtl_internal_function.
55   ∀args : list val.
56   ∀ dst : list register. (* CSC: changed from option to list *)
57   ∀ stk : list frame.
58   ∀   m : mem.
59   state
60| Returnstate :
61   ∀ rtv : list val. (* CSC: changed from option to list *)
62   ∀ dst : list register. (* CSC: changed from option to list *)
63   ∀ stk : list frame.
64   ∀   m : mem.
65   state.
66
67definition mem_of_state : state → mem ≝
68λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
69
70definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
71
72(* CSC: modified to take in input a list of registers (untyped) *)
73definition init_locals : list register → register_env val ≝
74foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
75
76definition reg_store ≝
77λreg,v,locals.
78  update RegisterTag val locals reg v.
79
80axiom WrongNumberOfParameters : String.
81
82(* CSC: modified to take in input a list of registers (untyped) *)
83let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
84match rs with
85[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
86| cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
87  let locals' ≝ add RegisterTag val locals r v in
88  params_store rst vst locals'
89] ].
90
91axiom BadRegister : String.
92
93definition reg_retrieve : register_env ? → register → res val ≝
94λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
95
96axiom FailedOp : String.
97axiom MissingSymbol : String.
98
99axiom MissingStatement : String.
100axiom FailedConstant : String.
101axiom FailedLoad : String.
102axiom FailedStore : String.
103axiom BadFunction : String.
104axiom BadJumpTable : String.
105axiom BadJumpValue : String.
106axiom FinalState : String.
107axiom ReturnMismatch : String.
108
109definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
110λge,st.
111match st with
112[ State f fs m ⇒
113  ! s ← opt_to_io … [MSG MissingStatement; CTX ? (next f)] (lookup ?? (rtl_if_graph (func f)) (next f));
114  match s with
115  [ rtl_st_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
116  | rtl_st_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
117  | rtl_st_load addrl addrh dst l ⇒  (* CSC: pairs of regs vs reg *)
118      ! vaddrh ← reg_retrieve (locals f) addrh;
119      ! vaddrl ← reg_retrieve (locals f) addrl;
120      ! vaddr ← smerge vaddrl vaddrh;
121      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
122      ! locals ← reg_store dst v (locals f);
123      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
124  | rtl_st_store addrl addrh src l ⇒  (* CSC: pairs of regs vs reg *)
125      ! vaddrh ← reg_retrieve (locals f) addrh;
126      ! vaddrl ← reg_retrieve (locals f) addrl;
127      ! vaddr ← smerge vaddrl vaddrh;
128      ! v ← reg_retrieve (locals f) src;
129      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
130      ret ? 〈E0, build_state f fs m' l〉
131  | rtl_st_call_id id args dst l ⇒
132      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
133      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
134      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
135      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
136  | rtl_st_call_ptr lfrs hfrs args dst l ⇒ (* CSC: pairs of regs vs reg *)
137      ! hfv ← reg_retrieve (locals f) hfrs;
138      ! lfv ← reg_retrieve (locals f) lfrs;
139      ! fv  ← smerge lfv hfv;
140      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
141      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
142      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
143  | rtl_st_tailcall_id id args ⇒
144      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
145      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
146      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
147      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
148  | rtl_st_tailcall_ptr lfrs hfrs args ⇒ (* CSC: pairs of regs vs reg *)
149      ! hfv ← reg_retrieve (locals f) hfrs;
150      ! lfv ← reg_retrieve (locals f) lfrs;
151      ! fv  ← smerge lfv hfv;
152      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
153      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
154      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
155  | rtl_st_return ⇒
156      (* CSC: rtl_if_result/f_result; list vs option *)
157      let dest ≝ rtl_if_result (func f) in
158      ! v ←  mmap … (reg_retrieve (locals f)) dest;
159      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
160  | rtl_st_cond src ltrue lfalse ⇒
161      ! v ← reg_retrieve (locals f) src;
162      ! b ← eval_bool_of_val v;
163      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
164  (* CSC: mismatch between the memory models and failures for the next two opx *)
165  | rtl_st_op1 op dst src l ⇒
166     ! v ← reg_retrieve (locals f) src;
167     ! v ← Byte_of_val v;
168     let v' ≝ val_of_Byte (op1 eval op v) in
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_op2 op dst src1 src2 l ⇒
172     ! v1 ← reg_retrieve (locals f) src1;
173     ! v1 ← Byte_of_val v1;
174     ! v2 ← reg_retrieve (locals f) src2;
175     ! v2 ← Byte_of_val v2;
176     ! carry ← eval_bool_of_val (carry f);
177     let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
178     let v' ≝ val_of_Byte v' in
179     let carry ≝ of_bool carry in
180     ! locals ← reg_store dst v' (locals f);
181     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) carry) fs m〉
182
183  (* CSC: Removed: St_jumptable *)
184  (* CSC: Added: *)
185 
186  (* CSC: St_const splitted into rtl_st_int, rtl_st_addr and rt_st_stack_addr; *)
187  | rtl_st_addr ldest hdest id l ⇒
188     ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
189     let 〈laddr,haddr〉 ≝ represent_block addr in
190     ! locals ← reg_store ldest laddr (locals f);
191     ! locals ← reg_store hdest haddr locals;
192     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
193  | rtl_st_stack_addr ldest hdest l ⇒
194     let 〈laddr,haddr〉 ≝ represent_block (sp f) in
195     ! locals ← reg_store ldest laddr (locals f);
196     ! locals ← reg_store hdest haddr locals;
197     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
198  | rtl_st_int dest v l ⇒
199     ! locals ← reg_store dest (val_of_Byte v) (locals f);
200     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
201
202  (* CSC: St_op1 splitted into rtl_st_op1 and rtl_st_move *)
203  | rtl_st_move dst src l ⇒
204     ! v ← reg_retrieve (locals f) src;
205     ! locals ← reg_store dst v (locals f);
206     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
207  (* CSC: St_op2 splitted into rtl_st_op2 and rtl_st_opaccs *) 
208  | rtl_st_opaccs op dacc dbacc sacc sbacc l ⇒
209     ! v1 ← reg_retrieve (locals f) sacc;
210     ! v1 ← Byte_of_val v1;
211     ! v2 ← reg_retrieve (locals f) sbacc;
212     ! v2 ← Byte_of_val v2;
213     let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
214     let v1' ≝ val_of_Byte v1' in
215     let v2' ≝ val_of_Byte v2' in
216     ! locals ← reg_store dacc v1' (locals f);
217     ! locals ← reg_store dbacc v2' locals;
218     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
219 
220  | rtl_st_clear_carry l ⇒
221    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vfalse) fs m〉
222  | rtl_st_set_carry l ⇒
223    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vtrue) fs m〉
224  ]
225| Callstate fd params dst fs m ⇒
226    match fd with
227    [ Internal fn ⇒
228        ! locals ← params_store (rtl_if_params fn) params (init_locals (rtl_if_locals fn));
229        let 〈m', sp〉 ≝ alloc m 0 (rtl_if_stacksize fn) Any in
230        (* CSC: added carry *)
231        ret ? 〈E0, State (mk_frame fn locals (rtl_if_entry fn) sp dst Vundef) fs m'〉
232    | External fn ⇒
233        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
234        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
235        (* CSC: return type changed from option to list *)
236        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉
237    ]
238| Returnstate v dst fs m ⇒ ? (* CSC: XXXXXXXXXXXXXXXXXX
239    match fs with
240    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
241    | cons f fs' ⇒
242        ! locals ← match dst with
243                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
244                                         | _ ⇒ Error ? (msg ReturnMismatch) ]
245                   | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch)
246                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
247        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
248    ] *)
249].
250
251definition is_final : state → option int ≝
252λs. match s with
253[ State _ _ _ ⇒ None ?
254| Callstate _ _ _ _ _ ⇒ None ?
255| Returnstate v _ fs _ ⇒
256    match fs with [ nil ⇒
257      match v with [ Some v' ⇒
258        match v' with
259        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
260        | _ ⇒ None ? ]
261      | None ⇒ None ? ]
262    | cons _ _ ⇒ None ? ]
263].
264
265definition RTLabs_exec : execstep io_out io_in ≝
266  mk_execstep … ? is_final mem_of_state eval_statement.
267
268definition make_initial_state : RTLabs_program → res (genv × state) ≝
269λp.
270  do ge ← globalenv Genv ?? p;
271  do m ← init_mem Genv ?? p;
272  let main ≝ prog_main ?? p in
273  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
274  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
275  OK ? 〈ge,Callstate f (nil ?) (None ?) (nil ?) m〉.
276
277definition RTLabs_fullexec : fullexec io_out io_in ≝
278  mk_fullexec … RTLabs_exec ? make_initial_state.
279
Note: See TracBrowser for help on using the repository browser.