source: src/Cminor/semantics.ma @ 961

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

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File size: 9.6 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]) (sz:intsize) (i:bvint sz) (cs:list (bvint sz × 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_bv ? i hi then a else find_case A sz 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 sz _ e cs default ⇒
202        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
203        match v with
204        [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λ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        | _ ⇒ Wrong ??? (msg BadSwitchValue)
209        ]
210    | St_return eo ⇒
211        match eo with
212        [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)〉
213        | Some e ⇒
214            match e with [ dp ty e ⇒
215              ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
216              ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉
217            ]
218        ]
219    | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉
220    | St_goto l ⇒
221        ! 〈s', k'〉 ← opt_to_res … [MSG UnknownLabel; CTX ? l] (find_label l (f_body f) (call_cont k));
222        ret ? 〈E0, State f s' en m sp k'〉
223    | St_cost l s' ⇒
224        ret ? 〈Echarge l, State f s' en m sp k〉
225    ]
226| Callstate fd args m k ⇒
227    match fd with
228    [ Internal f ⇒
229        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
230        ! en ← bind_params args (f_params f);
231        ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) m' sp k〉
232    | External fn ⇒
233        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
234        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
235        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
236        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m k〉
237    ]
238| Returnstate res m k ⇒
239    match k with
240    [ Kcall dst f sp en k' ⇒
241        ! en' ← match res with
242                [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? (msg ReturnMismatch)]
243                | Some v ⇒ match dst with [ None ⇒ Error ? (msg ReturnMismatch)
244                                          | Some id ⇒ update ?? en id v ]
245                ];
246        ret ? 〈E0, State f St_skip en' m sp k'〉
247    | _ ⇒ Wrong ??? (msg BadState)
248    ]
249].
250
251definition is_final : state → option int ≝
252λs. match s with
253[ Returnstate res m k ⇒
254    match k with
255    [ Kstop ⇒
256        match res with
257        [ None ⇒ None ?
258        | Some v ⇒
259            match v with
260            [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
261            | _ ⇒ None ?
262            ]
263        ]
264    | _ ⇒ None ?
265    ]
266| _ ⇒ None ?
267].
268
269definition Cminor_exec : execstep io_out io_in ≝
270  mk_execstep … ? is_final mem_of_state eval_step.
271
272axiom MainMissing : String.
273
274definition make_initial_state : Cminor_program → res (genv × state) ≝
275λp.
276  do ge ← globalenv Genv ?? p;
277  do m ← init_mem Genv ?? p;
278  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
279  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
280  OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
281
282definition Cminor_fullexec : fullexec io_out io_in ≝
283  mk_fullexec … Cminor_exec ? make_initial_state.
Note: See TracBrowser for help on using the repository browser.