source: src/Cminor/semantics.ma @ 882

Last change on this file since 882 was 881, checked in by campbell, 10 years ago

Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.

File size: 9.3 KB
Line 
1
2include "common/Events.ma".
3include "common/Mem.ma".
4include "common/IO.ma".
5include "common/Globalenvs.ma".
6include "common/SmallstepExec.ma".
7
8include "Cminor/syntax.ma".
9
10definition env ≝ identifier_map SymbolTag val.
11definition genv ≝ (genv_t Genv) (fundef internal_function).
12
13inductive 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
19inductive 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
40definition mem_of_state : state → mem ≝
41λst. match st with
42[ State _ _ _ m _ _ ⇒ m
43| Callstate _ _ m _ ⇒ m
44| Returnstate _ m _ ⇒ m
45].
46
47axiom UnknownLocal : String.
48axiom FailedConstant : String.
49axiom FailedOp : String.
50axiom FailedLoad : String.
51
52let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝
53match 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 ty ty' 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 ty1 ty2 ty' 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 rg ty 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 sz sg ty 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 ty l e' ⇒
79    do 〈tr,r〉 ← eval_expr ge ty e' en sp m;
80    OK ? 〈Echarge l ⧺ tr, r〉
81].
82
83axiom BadState : String.
84
85let rec k_exit (n:nat) (k:cont) on k : res cont ≝
86match 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
93let rec find_case (A:Type[0]) (i:int) (cs:list (int × A)) (default:A) on cs : A ≝
94match 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
101let rec call_cont (k:cont) : cont ≝
102match k with
103[ Kseq _ k' ⇒ call_cont k'
104| Kblock k' ⇒ call_cont k'
105| _ ⇒ k
106].
107
108let rec find_label (l:ident) (s:stmt) (k:cont) on s : option (stmt × cont) ≝
109match 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
131axiom WrongNumberOfParameters : String.
132
133let rec bind_params (vs:list val) (ids:list ident) : res env ≝
134match 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
145definition init_locals : env → list ident → env ≝
146foldr ?? (λid,en. add ?? en id Vundef).
147
148axiom FailedStore : String.
149axiom BadFunctionValue : String.
150axiom BadSwitchValue : String.
151axiom UnknownLabel : String.
152axiom ReturnMismatch : String.
153
154definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
155λge,st.
156match 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. match e with [ dp ty 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. match e with [ dp ty 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            match e with [ dp ty e ⇒
211              ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
212              ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉
213            ]
214        ]
215    | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉
216    | St_goto l ⇒
217        ! 〈s', k'〉 ← opt_to_res … [MSG UnknownLabel; CTX ? l] (find_label l (f_body f) (call_cont k));
218        ret ? 〈E0, State f s' en m sp k'〉
219    | St_cost l s' ⇒
220        ret ? 〈Echarge l, State f s' en m sp k〉
221    ]
222| Callstate fd args m k ⇒
223    match fd with
224    [ Internal f ⇒
225        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
226        ! en ← bind_params args (f_params f);
227        ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) m' sp k〉
228    | External fn ⇒
229        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
230        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
231        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
232        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m k〉
233    ]
234| Returnstate res m k ⇒
235    match k with
236    [ Kcall dst f sp en k' ⇒
237        ! en' ← match res with
238                [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? (msg ReturnMismatch)]
239                | Some v ⇒ match dst with [ None ⇒ Error ? (msg ReturnMismatch)
240                                          | Some id ⇒ update ?? en id v ]
241                ];
242        ret ? 〈E0, State f St_skip en' m sp k'〉
243    | _ ⇒ Wrong ??? (msg BadState)
244    ]
245].
246
247definition is_final : state → option int ≝
248λs. match s with
249[ Returnstate res m k ⇒
250    match k with
251    [ Kstop ⇒
252        match res with
253        [ None ⇒ None ?
254        | Some v ⇒
255            match v with
256            [ Vint i ⇒ Some ? i
257            | _ ⇒ None ?
258            ]
259        ]
260    | _ ⇒ None ?
261    ]
262| _ ⇒ None ?
263].
264
265definition Cminor_exec : execstep io_out io_in ≝
266  mk_execstep … ? is_final mem_of_state eval_step.
267
268axiom MainMissing : String.
269
270definition make_initial_state : Cminor_program → res (genv × state) ≝
271λp.
272  do ge ← globalenv Genv ?? p;
273  do m ← init_mem Genv ?? p;
274  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
275  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
276  OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
277
278definition Cminor_fullexec : fullexec io_out io_in ≝
279  mk_fullexec … Cminor_exec ? make_initial_state.
Note: See TracBrowser for help on using the repository browser.