source: src/RTL/semantics.ma @ 1118

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

All derivatives of St_const implemented (up to axioms to match the two
memory models).

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