1 | |
---|
2 | include "common/Events.ma". |
---|
3 | include "common/Mem.ma". |
---|
4 | include "common/IO.ma". |
---|
5 | include "common/Globalenvs.ma". |
---|
6 | include "common/SmallstepExec.ma". |
---|
7 | |
---|
8 | include "Cminor/syntax.ma". |
---|
9 | |
---|
10 | definition env ≝ identifier_map SymbolTag val. |
---|
11 | definition genv ≝ (genv_t Genv) (fundef internal_function). |
---|
12 | |
---|
13 | inductive cont : Type[0] ≝ |
---|
14 | | Kstop : cont |
---|
15 | | Kseq : stmt → cont → cont |
---|
16 | | Kblock : cont → cont |
---|
17 | | Kcall : option ident → internal_function → block (* sp *) → env → cont → cont. |
---|
18 | |
---|
19 | inductive state : Type[0] ≝ |
---|
20 | | State: |
---|
21 | ∀ f: internal_function. |
---|
22 | ∀ s: stmt. |
---|
23 | ∀ en: env. |
---|
24 | ∀ m: mem. |
---|
25 | ∀ sp: block. |
---|
26 | ∀ k: cont. |
---|
27 | state |
---|
28 | | Callstate: |
---|
29 | ∀ fd: fundef internal_function. |
---|
30 | ∀ args: list val. |
---|
31 | ∀ m: mem. |
---|
32 | ∀ k: cont. |
---|
33 | state |
---|
34 | | Returnstate: |
---|
35 | ∀ v: option val. |
---|
36 | ∀ m: mem. |
---|
37 | ∀ k: cont. |
---|
38 | state. |
---|
39 | |
---|
40 | definition mem_of_state : state → mem ≝ |
---|
41 | λst. match st with |
---|
42 | [ State _ _ _ m _ _ ⇒ m |
---|
43 | | Callstate _ _ m _ ⇒ m |
---|
44 | | Returnstate _ m _ ⇒ m |
---|
45 | ]. |
---|
46 | |
---|
47 | axiom UnknownLocal : String. |
---|
48 | axiom FailedConstant : String. |
---|
49 | axiom FailedOp : String. |
---|
50 | axiom FailedLoad : String. |
---|
51 | |
---|
52 | let rec eval_expr (ge:genv) (e:expr) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝ |
---|
53 | match e with |
---|
54 | [ Id i ⇒ |
---|
55 | do r ← opt_to_res … [MSG UnknownLocal; CTX ? i] (lookup ?? en i); |
---|
56 | OK ? 〈E0, r〉 |
---|
57 | | Cst c ⇒ |
---|
58 | do r ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) sp c); |
---|
59 | OK ? 〈E0, r〉 |
---|
60 | | Op1 op e' ⇒ |
---|
61 | do 〈tr,v〉 ← eval_expr ge e' en sp m; |
---|
62 | do r ← opt_to_res … (msg FailedOp) (eval_unop op v); |
---|
63 | OK ? 〈tr, r〉 |
---|
64 | | Op2 op e1 e2 ⇒ |
---|
65 | do 〈tr1,v1〉 ← eval_expr ge e1 en sp m; |
---|
66 | do 〈tr2,v2〉 ← eval_expr ge e2 en sp m; |
---|
67 | do r ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2); |
---|
68 | OK ? 〈tr1 ⧺ tr2, r〉 |
---|
69 | | Mem chunk e ⇒ |
---|
70 | do 〈tr,v〉 ← eval_expr ge e en sp m; |
---|
71 | do r ← opt_to_res … (msg FailedLoad) (loadv chunk m v); |
---|
72 | OK ? 〈tr, r〉 |
---|
73 | | Cond e' e1 e2 ⇒ |
---|
74 | do 〈tr,v〉 ← eval_expr ge e' en sp m; |
---|
75 | do b ← eval_bool_of_val v; |
---|
76 | do 〈tr',r〉 ← eval_expr ge (if b then e1 else e2) en sp m; |
---|
77 | OK ? 〈tr ⧺ tr', r〉 |
---|
78 | | Ecost l e' ⇒ |
---|
79 | do 〈tr,r〉 ← eval_expr ge e' en sp m; |
---|
80 | OK ? 〈Echarge l ⧺ tr, r〉 |
---|
81 | ]. |
---|
82 | |
---|
83 | axiom BadState : String. |
---|
84 | |
---|
85 | let rec k_exit (n:nat) (k:cont) on k : res cont ≝ |
---|
86 | match k with |
---|
87 | [ Kstop ⇒ Error ? (msg BadState) |
---|
88 | | Kseq _ k' ⇒ k_exit n k' |
---|
89 | | Kblock k' ⇒ match n with [ O ⇒ OK ? k' | S m ⇒ k_exit m k' ] |
---|
90 | | Kcall _ _ _ _ _ ⇒ Error ? (msg BadState) |
---|
91 | ]. |
---|
92 | |
---|
93 | let rec find_case (A:Type[0]) (i:int) (cs:list (int × A)) (default:A) on cs : A ≝ |
---|
94 | match cs with |
---|
95 | [ nil ⇒ default |
---|
96 | | cons h t ⇒ |
---|
97 | let 〈hi,a〉 ≝ h in |
---|
98 | if eq i hi then a else find_case A i t default |
---|
99 | ]. |
---|
100 | |
---|
101 | let rec call_cont (k:cont) : cont ≝ |
---|
102 | match k with |
---|
103 | [ Kseq _ k' ⇒ call_cont k' |
---|
104 | | Kblock k' ⇒ call_cont k' |
---|
105 | | _ ⇒ k |
---|
106 | ]. |
---|
107 | |
---|
108 | let rec find_label (l:ident) (s:stmt) (k:cont) on s : option (stmt × cont) ≝ |
---|
109 | match s with |
---|
110 | [ St_seq s1 s2 ⇒ |
---|
111 | match find_label l s1 (Kseq s2 k) with |
---|
112 | [ None ⇒ find_label l s2 k |
---|
113 | | Some sk ⇒ Some ? sk |
---|
114 | ] |
---|
115 | | St_ifthenelse _ s1 s2 ⇒ |
---|
116 | match find_label l s1 k with |
---|
117 | [ None ⇒ find_label l s2 k |
---|
118 | | Some sk ⇒ Some ? sk |
---|
119 | ] |
---|
120 | | St_loop s' ⇒ find_label l s' (Kseq (St_loop s') k) |
---|
121 | | St_block s' ⇒ find_label l s' (Kblock k) |
---|
122 | | St_label l' s' ⇒ |
---|
123 | match ident_eq l l' with |
---|
124 | [ inl _ ⇒ Some ? 〈s',k〉 |
---|
125 | | inr _ ⇒ find_label l s' k |
---|
126 | ] |
---|
127 | | St_cost _ s' ⇒ find_label l s' k |
---|
128 | | _ ⇒ None ? |
---|
129 | ]. |
---|
130 | |
---|
131 | axiom WrongNumberOfParameters : String. |
---|
132 | |
---|
133 | let rec bind_params (vs:list val) (ids:list ident) : res env ≝ |
---|
134 | match vs with |
---|
135 | [ nil ⇒ match ids with [ nil ⇒ OK ? (empty_map ??) | _ ⇒ Error ? (msg WrongNumberOfParameters) ] |
---|
136 | | cons v vt ⇒ |
---|
137 | match ids with |
---|
138 | [ nil ⇒ Error ? (msg WrongNumberOfParameters) |
---|
139 | | cons id idt ⇒ |
---|
140 | do en ← bind_params vt idt; |
---|
141 | OK ? (add ?? en id v) |
---|
142 | ] |
---|
143 | ]. |
---|
144 | |
---|
145 | definition init_locals : env → list ident → env ≝ |
---|
146 | foldr ?? (λid,en. add ?? en id Vundef). |
---|
147 | |
---|
148 | axiom FailedStore : String. |
---|
149 | axiom BadFunctionValue : String. |
---|
150 | axiom BadSwitchValue : String. |
---|
151 | axiom UnknownLabel : String. |
---|
152 | axiom ReturnMismatch : String. |
---|
153 | |
---|
154 | definition eval_step : genv → state → IO io_out io_in (trace × state) ≝ |
---|
155 | λge,st. |
---|
156 | match st with |
---|
157 | [ State f s en m sp k ⇒ |
---|
158 | match s with |
---|
159 | [ St_skip ⇒ |
---|
160 | match k with |
---|
161 | [ Kstop ⇒ Wrong ??? (msg BadState) |
---|
162 | | Kseq s' k' ⇒ ret ? 〈E0, State f s' en m sp k'〉 |
---|
163 | | Kblock k' ⇒ ret ? 〈E0, State f s en m sp k'〉 |
---|
164 | (* cminor allows functions without an explicit return statement *) |
---|
165 | | Kcall _ _ _ _ _ ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) k〉 |
---|
166 | ] |
---|
167 | | St_assign id e ⇒ |
---|
168 | ! 〈tr,v〉 ← eval_expr ge e en sp m; |
---|
169 | ! en' ← update ?? en id v; |
---|
170 | ret ? 〈tr, State f St_skip en' m sp k〉 |
---|
171 | | St_store chunk edst e ⇒ |
---|
172 | ! 〈tr,vdst〉 ← eval_expr ge edst en sp m; |
---|
173 | ! 〈tr',v〉 ← eval_expr ge e en sp m; |
---|
174 | ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v); |
---|
175 | ret ? 〈tr ⧺ tr', State f St_skip en m' sp k〉 |
---|
176 | |
---|
177 | | St_call dst ef args ⇒ |
---|
178 | ! 〈tr,vf〉 ← eval_expr ge ef en sp m; |
---|
179 | ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf); |
---|
180 | ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args; |
---|
181 | ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉 |
---|
182 | | St_tailcall ef args ⇒ |
---|
183 | ! 〈tr,vf〉 ← eval_expr ge ef en sp m; |
---|
184 | ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf); |
---|
185 | ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args; |
---|
186 | ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) (call_cont k)〉 |
---|
187 | |
---|
188 | | St_seq s1 s2 ⇒ ret ? 〈E0, State f s1 en m sp (Kseq s2 k)〉 |
---|
189 | | St_ifthenelse e strue sfalse ⇒ |
---|
190 | ! 〈tr,v〉 ← eval_expr ge e en sp m; |
---|
191 | ! b ← eval_bool_of_val v; |
---|
192 | ret ? 〈tr, State f (if b then strue else sfalse) en m sp k〉 |
---|
193 | | St_loop s ⇒ ret ? 〈E0, State f s en m sp (Kseq (St_loop s) k)〉 |
---|
194 | | St_block s ⇒ ret ? 〈E0, State f s en m sp (Kblock k)〉 |
---|
195 | | St_exit n ⇒ |
---|
196 | ! k' ← k_exit n k; |
---|
197 | ret ? 〈E0, State f St_skip en m sp k'〉 |
---|
198 | | St_switch e cs default ⇒ |
---|
199 | ! 〈tr,v〉 ← eval_expr ge e en sp m; |
---|
200 | match v with |
---|
201 | [ Vint i ⇒ |
---|
202 | ! k' ← k_exit (find_case ? i cs default) k; |
---|
203 | ret ? 〈tr, State f St_skip en m sp k'〉 |
---|
204 | | _ ⇒ Wrong ??? (msg BadSwitchValue) |
---|
205 | ] |
---|
206 | | St_return eo ⇒ |
---|
207 | match eo with |
---|
208 | [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)〉 |
---|
209 | | Some e ⇒ |
---|
210 | ! 〈tr,v〉 ← eval_expr ge e en sp m; |
---|
211 | ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉 |
---|
212 | ] |
---|
213 | | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉 |
---|
214 | | St_goto l ⇒ |
---|
215 | ! 〈s', k'〉 ← opt_to_res … [MSG UnknownLabel; CTX ? l] (find_label l (f_body f) (call_cont k)); |
---|
216 | ret ? 〈E0, State f s' en m sp k'〉 |
---|
217 | | St_cost l s' ⇒ |
---|
218 | ret ? 〈Echarge l, State f s' en m sp k〉 |
---|
219 | ] |
---|
220 | | Callstate fd args m k ⇒ |
---|
221 | match fd with |
---|
222 | [ Internal f ⇒ |
---|
223 | let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in |
---|
224 | ! en ← bind_params args (f_params f); |
---|
225 | ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) m' sp k〉 |
---|
226 | | External fn ⇒ |
---|
227 | ! evargs ← check_eventval_list args (sig_args (ef_sig fn)); |
---|
228 | ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); |
---|
229 | let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in |
---|
230 | ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m k〉 |
---|
231 | ] |
---|
232 | | Returnstate res m k ⇒ |
---|
233 | match k with |
---|
234 | [ Kcall dst f sp en k' ⇒ |
---|
235 | ! en' ← match res with |
---|
236 | [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? (msg ReturnMismatch)] |
---|
237 | | Some v ⇒ match dst with [ None ⇒ Error ? (msg ReturnMismatch) |
---|
238 | | Some id ⇒ update ?? en id v ] |
---|
239 | ]; |
---|
240 | ret ? 〈E0, State f St_skip en' m sp k'〉 |
---|
241 | | _ ⇒ Wrong ??? (msg BadState) |
---|
242 | ] |
---|
243 | ]. |
---|
244 | |
---|
245 | definition is_final : state → option int ≝ |
---|
246 | λs. match s with |
---|
247 | [ Returnstate res m k ⇒ |
---|
248 | match k with |
---|
249 | [ Kstop ⇒ |
---|
250 | match res with |
---|
251 | [ None ⇒ None ? |
---|
252 | | Some v ⇒ |
---|
253 | match v with |
---|
254 | [ Vint i ⇒ Some ? i |
---|
255 | | _ ⇒ None ? |
---|
256 | ] |
---|
257 | ] |
---|
258 | | _ ⇒ None ? |
---|
259 | ] |
---|
260 | | _ ⇒ None ? |
---|
261 | ]. |
---|
262 | |
---|
263 | definition Cminor_exec : execstep io_out io_in ≝ |
---|
264 | mk_execstep … ? is_final mem_of_state eval_step. |
---|
265 | |
---|
266 | axiom MainMissing : String. |
---|
267 | |
---|
268 | definition make_initial_state : Cminor_program → res (genv × state) ≝ |
---|
269 | λp. |
---|
270 | do ge ← globalenv Genv ?? p; |
---|
271 | do m ← init_mem Genv ?? p; |
---|
272 | do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p)); |
---|
273 | do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b); |
---|
274 | OK ? 〈ge, Callstate f (nil ?) m Kstop〉. |
---|
275 | |
---|
276 | definition Cminor_fullexec : fullexec io_out io_in ≝ |
---|
277 | mk_fullexec … Cminor_exec ? make_initial_state. |
---|