source: Deliverables/D3.3/Cminor-experiment/semantics.ma @ 796

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

Update experimental version of Cminor semantics.

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