source: src/Cminor/semantics.ma @ 761

Last change on this file since 761 was 761, checked in by campbell, 9 years ago

Enforce the use of declared identifiers/registers in Cminor/RTLabs.

File size: 8.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
47let rec eval_expr (ge:genv) (e:expr) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝
48match e with
49[ Id i ⇒
50    do r ← opt_to_res … (lookup ?? en i);
51    OK ? 〈E0, r〉
52| Cst c ⇒
53    do r ← opt_to_res … (eval_constant (find_symbol … ge) sp c);
54    OK ? 〈E0, r〉
55| Op1 op e' ⇒
56    do 〈tr,v〉 ← eval_expr ge e' en sp m;
57    do r ← opt_to_res … (eval_unop op v);
58    OK ? 〈tr, r〉
59| Op2 op e1 e2 ⇒
60    do 〈tr1,v1〉 ← eval_expr ge e1 en sp m;
61    do 〈tr2,v2〉 ← eval_expr ge e2 en sp m;
62    do r ← opt_to_res … (eval_binop op v1 v2);
63    OK ? 〈tr1 ⧺ tr2, r〉
64| Mem chunk e ⇒
65    do 〈tr,v〉 ← eval_expr ge e en sp m;
66    do r ← opt_to_res … (loadv chunk m v);
67    OK ? 〈tr, r〉
68| Cond e' e1 e2 ⇒
69    do 〈tr,v〉 ← eval_expr ge e' en sp m;
70    do b ← eval_bool_of_val v;
71    do 〈tr',r〉 ← eval_expr ge (if b then e1 else e2) en sp m;
72    OK ? 〈tr ⧺ tr', r〉
73| Ecost l e' ⇒
74    do 〈tr,r〉 ← eval_expr ge e' en sp m;
75    OK ? 〈Echarge l ⧺ tr, r〉
76].
77
78let rec k_exit (n:nat) (k:cont) on k : res cont ≝
79match k with
80[ Kstop ⇒ Error ?
81| Kseq _ k' ⇒ k_exit n k'
82| Kblock k' ⇒ match n with [ O ⇒ OK ? k' | S m ⇒ k_exit m k' ]
83| Kcall _ _ _ _ _ ⇒ Error ?
84].
85
86let rec find_case (A:Type[0]) (i:int) (cs:list (int × A)) (default:A) on cs : A ≝
87match cs with
88[ nil ⇒ default
89| cons h t ⇒
90    let 〈hi,a〉 ≝ h in
91    if eq i hi then a else find_case A i t default
92].
93
94let rec call_cont (k:cont) : cont ≝
95match k with
96[ Kseq _ k' ⇒ call_cont k'
97| Kblock k' ⇒ call_cont k'
98| _ ⇒ k
99].
100
101let rec find_label (l:ident) (s:stmt) (k:cont) on s : option (stmt × cont) ≝
102match s with
103[ St_seq s1 s2 ⇒
104    match find_label l s1 (Kseq s2 k) with
105    [ None ⇒ find_label l s2 k
106    | Some sk ⇒ Some ? sk
107    ]
108| St_ifthenelse _ s1 s2 ⇒
109    match find_label l s1 k with
110    [ None ⇒ find_label l s2 k
111    | Some sk ⇒ Some ? sk
112    ]
113| St_loop s' ⇒ find_label l s' (Kseq (St_loop s') k)
114| St_block s' ⇒ find_label l s' (Kblock k)
115| St_label l' s' ⇒
116    match ident_eq l l' with
117    [ inl _ ⇒ Some ? 〈s',k〉
118    | inr _ ⇒ find_label l s' k
119    ]
120| St_cost _ s' ⇒ find_label l s' k
121| _ ⇒ None ?
122].
123
124let rec bind_params (vs:list val) (ids:list ident) : res env ≝
125match vs with
126[ nil ⇒ match ids with [ nil ⇒ OK ? (empty_map ??) | _ ⇒ Error ? ]
127| cons v vt ⇒
128    match ids with
129    [ nil ⇒ Error ?
130    | cons id idt ⇒
131        do en ← bind_params vt idt;
132        OK ? (add ?? en id v)
133    ]
134].
135
136definition init_locals : env → list ident → env ≝
137foldr ?? (λid,en. add ?? en id Vundef).
138
139definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
140λge,st.
141match st with
142[ State f s en m sp k ⇒
143    match s with
144    [ St_skip ⇒
145        match k with
146        [ Kstop ⇒ Wrong ???
147        | Kseq s' k' ⇒ ret ? 〈E0, State f s' en m sp k'〉
148        | Kblock k' ⇒ ret ? 〈E0, State f s en m sp k'〉
149          (* cminor allows functions without an explicit return statement *)
150        | Kcall _ _ _ _ _ ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) k〉
151        ]
152    | St_assign id e ⇒
153        ! 〈tr,v〉 ← eval_expr ge e en sp m;
154        ! en' ← update ?? en id v;
155        ret ? 〈tr, State f St_skip en' m sp k〉
156    | St_store chunk edst e ⇒
157        ! 〈tr,vdst〉 ← eval_expr ge edst en sp m;
158        ! 〈tr',v〉 ← eval_expr ge e en sp m;
159        ! m' ← opt_to_res … (storev chunk m vdst v);
160        ret ? 〈tr ⧺ tr', State f St_skip en m' sp k〉
161
162    | St_call dst ef args sig ⇒ (* XXX sig unused? *)
163        ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
164        ! fd ← opt_to_res … (find_funct ?? ge vf);
165        ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
166        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉
167    | St_tailcall ef args sig ⇒
168        ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
169        ! fd ← opt_to_res … (find_funct ?? ge vf);
170        ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
171        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) (call_cont k)〉
172       
173    | St_seq s1 s2 ⇒ ret ? 〈E0, State f s1 en m sp (Kseq s2 k)〉
174    | St_ifthenelse e strue sfalse ⇒
175        ! 〈tr,v〉 ← eval_expr ge e en sp m;
176        ! b ← eval_bool_of_val v;
177        ret ? 〈tr, State f (if b then strue else sfalse) en m sp k〉
178    | St_loop s ⇒ ret ? 〈E0, State f s en m sp (Kseq (St_loop s) k)〉
179    | St_block s ⇒ ret ? 〈E0, State f s en m sp (Kblock k)〉
180    | St_exit n ⇒
181        ! k' ← k_exit n k;
182        ret ? 〈E0, State f St_skip en m sp k'〉
183    | St_switch e cs default ⇒
184        ! 〈tr,v〉 ← eval_expr ge e en sp m;
185        match v with
186        [ Vint i ⇒
187            ! k' ← k_exit (find_case ? i cs default) k;
188            ret ? 〈tr, State f St_skip en m sp k'〉
189        | _ ⇒ Wrong ???
190        ]
191    | St_return eo ⇒
192        match eo with
193        [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)〉
194        | Some e ⇒
195            ! 〈tr,v〉 ← eval_expr ge e en sp m;
196            ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉
197        ]
198    | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉
199    | St_goto l ⇒
200        ! 〈s', k'〉 ← opt_to_res … (find_label l (f_body f) (call_cont k));
201        ret ? 〈E0, State f s' en m sp k'〉
202    | St_cost l s' ⇒
203        ret ? 〈Echarge l, State f s' en m sp k〉
204    ]
205| Callstate fd args m k ⇒
206    match fd with
207    [ Internal f ⇒
208        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
209        ! en ← bind_params args (f_params f);
210        ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) m' sp k〉
211    | External fn ⇒
212        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
213        ! evres ← do_io (ef_id fn) evargs (match (sig_res (ef_sig fn)) with [ None ⇒ ASTint | Some t ⇒ t ]);  (* XXX hack, should allow none *)
214        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
215        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m k〉
216    ]
217| Returnstate res m k ⇒
218    match k with
219    [ Kcall dst f sp en k' ⇒
220        ! en' ← match res with
221                [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? ]
222                | Some v ⇒ match dst with [ None ⇒ Error ?
223                                          | Some id ⇒ update ?? en id v ]
224                ];
225        ret ? 〈E0, State f St_skip en' m sp k'〉
226    | _ ⇒ Wrong ???
227    ]
228].
229
230definition is_final : state → option int ≝
231λs. match s with
232[ Returnstate res m k ⇒
233    match k with
234    [ Kstop ⇒
235        match res with
236        [ None ⇒ None ?
237        | Some v ⇒
238            match v with
239            [ Vint i ⇒ Some ? i
240            | _ ⇒ None ?
241            ]
242        ]
243    | _ ⇒ None ?
244    ]
245| _ ⇒ None ?
246].
247
248definition Cminor_exec : execstep io_out io_in ≝
249  mk_execstep … ? is_final mem_of_state eval_step.
250
251definition make_initial_state : Cminor_program → res (genv × state) ≝
252λp.
253  do ge ← globalenv Genv ?? p;
254  do m ← init_mem Genv ?? p;
255  do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
256  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
257  OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
258
259definition Cminor_fullexec : fullexec io_out io_in ≝
260  mk_fullexec … Cminor_exec ? make_initial_state.
Note: See TracBrowser for help on using the repository browser.