source: src/Cminor/semantics.ma @ 751

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

Initial version of the Cminor syntax and semantics.

File size: 8.2 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 eval_step : genv → state → IO io_out io_in (trace × state) ≝
137λge,st.
138match st with
139[ State f s en m sp k ⇒
140    match s with
141    [ St_skip ⇒
142        match k with
143        [ Kstop ⇒ Wrong ???
144        | Kseq s' k' ⇒ ret ? 〈E0, State f s' en m sp k'〉
145        | Kblock k' ⇒ ret ? 〈E0, State f s en m sp k'〉
146          (* cminor allows functions without an explicit return statement *)
147        | Kcall _ _ _ _ _ ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) k〉
148        ]
149    | St_assign id e ⇒
150        ! 〈tr,v〉 ← eval_expr ge e en sp m;
151        ret ? 〈tr, State f St_skip (add ?? en id v) m sp k〉
152    | St_store chunk edst e ⇒
153        ! 〈tr,vdst〉 ← eval_expr ge edst en sp m;
154        ! 〈tr',v〉 ← eval_expr ge e en sp m;
155        ! m' ← opt_to_res … (storev chunk m vdst v);
156        ret ? 〈tr ⧺ tr', State f St_skip en m' sp k〉
157
158    | St_call dst ef args sig ⇒ (* XXX sig unused? *)
159        ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
160        ! fd ← opt_to_res … (find_funct ?? ge vf);
161        ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
162        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉
163    | St_tailcall ef args sig ⇒
164        ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
165        ! fd ← opt_to_res … (find_funct ?? ge vf);
166        ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
167        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) k〉
168       
169    | St_seq s1 s2 ⇒ ret ? 〈E0, State f s1 en m sp (Kseq s2 k)〉
170    | St_ifthenelse e strue sfalse ⇒
171        ! 〈tr,v〉 ← eval_expr ge e en sp m;
172        ! b ← eval_bool_of_val v;
173        ret ? 〈tr, State f (if b then strue else sfalse) en m sp k〉
174    | St_loop s ⇒ ret ? 〈E0, State f s en m sp (Kseq (St_loop s) k)〉
175    | St_block s ⇒ ret ? 〈E0, State f s en m sp (Kblock k)〉
176    | St_exit n ⇒
177        ! k' ← k_exit n k;
178        ret ? 〈E0, State f St_skip en m sp k'〉
179    | St_switch e cs default ⇒
180        ! 〈tr,v〉 ← eval_expr ge e en sp m;
181        match v with
182        [ Vint i ⇒
183            ! k' ← k_exit (find_case ? i cs default) k;
184            ret ? 〈tr, State f St_skip en m sp k'〉
185        | _ ⇒ Wrong ???
186        ]
187    | St_return eo ⇒
188        match eo with
189        [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)〉
190        | Some e ⇒
191            ! 〈tr,v〉 ← eval_expr ge e en sp m;
192            ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉
193        ]
194    | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉
195    | St_goto l ⇒
196        ! 〈s', k'〉 ← opt_to_res … (find_label l (f_body f) (call_cont k));
197        ret ? 〈E0, State f s' en m sp k'〉
198    | St_cost l s' ⇒
199        ret ? 〈Echarge l, State f s' en m sp k〉
200    ]
201| Callstate fd args m k ⇒
202    match fd with
203    [ Internal f ⇒
204        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
205        ! en ← bind_params args (f_params f);
206        ret ? 〈E0, State f (f_body f) en m' sp k〉
207    | External fn ⇒
208        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
209        ! evres ← do_io (ef_id fn) evargs (match (sig_res (ef_sig fn)) with [ None ⇒ ASTint | Some t ⇒ t ]);  (* XXX hack, should allow none *)
210        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
211        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m k〉
212    ]
213| Returnstate res m k ⇒
214    match k with
215    [ Kcall dst f sp en k' ⇒
216        ! en' ← match res with
217                [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? ]
218                | Some v ⇒ match dst with [ None ⇒ Error ?
219                                          | Some id ⇒ OK ? (add ?? en id v) ]
220                ];
221        ret ? 〈E0, State f St_skip en' m sp k'〉
222    | _ ⇒ Wrong ???
223    ]
224].
225
226definition is_final : state → option int ≝
227λs. match s with
228[ Returnstate res m k ⇒
229    match k with
230    [ Kstop ⇒
231        match res with
232        [ None ⇒ None ?
233        | Some v ⇒
234            match v with
235            [ Vint i ⇒ Some ? i
236            | _ ⇒ None ?
237            ]
238        ]
239    | _ ⇒ None ?
240    ]
241| _ ⇒ None ?
242].
243
244definition Cminor_exec : execstep io_out io_in ≝
245  mk_execstep … ? is_final mem_of_state eval_step.
246
247definition make_initial_state : Cminor_program → res (genv × state) ≝
248λp.
249  do ge ← globalenv Genv ?? p;
250  do m ← init_mem Genv ?? p;
251  do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
252  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
253  OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
254
255definition Cminor_fullexec : fullexec io_out io_in ≝
256  mk_fullexec … Cminor_exec ? make_initial_state.
Note: See TracBrowser for help on using the repository browser.