source: src/RTL/semantics.ma @ 1120

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

All operations implemented.

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