source: src/Cminor/semantics.ma @ 879

Last change on this file since 879 was 879, checked in by campbell, 8 years ago

Refine "AST" types to include size/signedness information.

File size: 9.0 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) (e:expr) (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 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
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. 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
245definition 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
263definition Cminor_exec : execstep io_out io_in ≝
264  mk_execstep … ? is_final mem_of_state eval_step.
265
266axiom MainMissing : String.
267
268definition 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
276definition Cminor_fullexec : fullexec io_out io_in ≝
277  mk_fullexec … Cminor_exec ? make_initial_state.
Note: See TracBrowser for help on using the repository browser.