source: src/Cminor/semantics.ma @ 886

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

Put types into parameter and variable lists in Cminor.
Temporarily breaks translation to RTLabs.

File size: 9.4 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
133(* TODO: perhaps should do a little type checking? *)
134let rec bind_params (vs:list val) (ids:list (ident×typ)) : res env ≝
135match vs with
136[ nil ⇒ match ids with [ nil ⇒ OK ? (empty_map ??) | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
137| cons v vt ⇒
138    match ids with
139    [ nil ⇒ Error ? (msg WrongNumberOfParameters)
140    | cons idh idt ⇒
141        let 〈id,ty〉 ≝ idh in
142        do en ← bind_params vt idt;
143        OK ? (add ?? en id v)
144    ]
145].
146
147(* TODO: perhaps should do a little type checking? *)
148definition init_locals : env → list (ident×typ) → env ≝
149foldr ?? (λidty,en. add ?? en (\fst idty) Vundef).
150
151axiom FailedStore : String.
152axiom BadFunctionValue : String.
153axiom BadSwitchValue : String.
154axiom UnknownLabel : String.
155axiom ReturnMismatch : String.
156
157definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
158λge,st.
159match st with
160[ State f s en m sp k ⇒
161    match s with
162    [ St_skip ⇒
163        match k with
164        [ Kstop ⇒ Wrong ??? (msg BadState)
165        | Kseq s' k' ⇒ ret ? 〈E0, State f s' en m sp k'〉
166        | Kblock k' ⇒ ret ? 〈E0, State f s en m sp k'〉
167          (* cminor allows functions without an explicit return statement *)
168        | Kcall _ _ _ _ _ ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) k〉
169        ]
170    | St_assign _ id e ⇒
171        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
172        ! en' ← update ?? en id v;
173        ret ? 〈tr, State f St_skip en' m sp k〉
174    | St_store _ _ chunk edst e ⇒
175        ! 〈tr,vdst〉 ← eval_expr ge ? edst en sp m;
176        ! 〈tr',v〉 ← eval_expr ge ? e en sp m;
177        ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v);
178        ret ? 〈tr ⧺ tr', State f St_skip en m' sp k〉
179
180    | St_call dst ef args ⇒
181        ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m;
182        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
183        ! 〈tr',vargs〉 ← trace_map … (λe. match e with [ dp ty e ⇒ eval_expr ge ? e en sp m ]) args;
184        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉
185    | St_tailcall ef args ⇒
186        ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m;
187        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
188        ! 〈tr',vargs〉 ← trace_map … (λe. match e with [ dp ty e ⇒ eval_expr ge ? e en sp m ]) args;
189        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) (call_cont k)〉
190       
191    | St_seq s1 s2 ⇒ ret ? 〈E0, State f s1 en m sp (Kseq s2 k)〉
192    | St_ifthenelse _ _ e strue sfalse ⇒
193        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
194        ! b ← eval_bool_of_val v;
195        ret ? 〈tr, State f (if b then strue else sfalse) en m sp k〉
196    | St_loop s ⇒ ret ? 〈E0, State f s en m sp (Kseq (St_loop s) k)〉
197    | St_block s ⇒ ret ? 〈E0, State f s en m sp (Kblock k)〉
198    | St_exit n ⇒
199        ! k' ← k_exit n k;
200        ret ? 〈E0, State f St_skip en m sp k'〉
201    | St_switch _ _ e cs default ⇒
202        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
203        match v with
204        [ Vint i ⇒
205            ! k' ← k_exit (find_case ? i cs default) k;
206            ret ? 〈tr, State f St_skip en m sp k'〉
207        | _ ⇒ Wrong ??? (msg BadSwitchValue)
208        ]
209    | St_return eo ⇒
210        match eo with
211        [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)〉
212        | Some e ⇒
213            match e with [ dp ty e ⇒
214              ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
215              ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉
216            ]
217        ]
218    | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉
219    | St_goto l ⇒
220        ! 〈s', k'〉 ← opt_to_res … [MSG UnknownLabel; CTX ? l] (find_label l (f_body f) (call_cont k));
221        ret ? 〈E0, State f s' en m sp k'〉
222    | St_cost l s' ⇒
223        ret ? 〈Echarge l, State f s' en m sp k〉
224    ]
225| Callstate fd args m k ⇒
226    match fd with
227    [ Internal f ⇒
228        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
229        ! en ← bind_params args (f_params f);
230        ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) m' sp k〉
231    | External fn ⇒
232        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
233        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
234        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
235        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m k〉
236    ]
237| Returnstate res m k ⇒
238    match k with
239    [ Kcall dst f sp en k' ⇒
240        ! en' ← match res with
241                [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? (msg ReturnMismatch)]
242                | Some v ⇒ match dst with [ None ⇒ Error ? (msg ReturnMismatch)
243                                          | Some id ⇒ update ?? en id v ]
244                ];
245        ret ? 〈E0, State f St_skip en' m sp k'〉
246    | _ ⇒ Wrong ??? (msg BadState)
247    ]
248].
249
250definition is_final : state → option int ≝
251λs. match s with
252[ Returnstate res m k ⇒
253    match k with
254    [ Kstop ⇒
255        match res with
256        [ None ⇒ None ?
257        | Some v ⇒
258            match v with
259            [ Vint i ⇒ Some ? i
260            | _ ⇒ None ?
261            ]
262        ]
263    | _ ⇒ None ?
264    ]
265| _ ⇒ None ?
266].
267
268definition Cminor_exec : execstep io_out io_in ≝
269  mk_execstep … ? is_final mem_of_state eval_step.
270
271axiom MainMissing : String.
272
273definition make_initial_state : Cminor_program → res (genv × state) ≝
274λp.
275  do ge ← globalenv Genv ?? p;
276  do m ← init_mem Genv ?? p;
277  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
278  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
279  OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
280
281definition Cminor_fullexec : fullexec io_out io_in ≝
282  mk_fullexec … Cminor_exec ? make_initial_state.
Note: See TracBrowser for help on using the repository browser.