source: src/Cminor/semantics.ma @ 1224

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

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

File size: 10.1 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 ?? (λx.x) p;
277  do m ← init_mem Genv ?? (λx.x) 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.
284
285definition make_initial_noinit_state : Cminor_noinit_program → res (genv × state) ≝
286λp.
287  do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
288  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
289  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
290  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
291  OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
292
293definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
294  mk_fullexec … Cminor_exec ? make_initial_noinit_state.
Note: See TracBrowser for help on using the repository browser.