source: src/RTLabs/semantics.ma @ 1882

Last change on this file since 1882 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 14.9 KB
Line 
1
2(* XXX NB: I haven't checked all of these semantics against the prototype
3           compilers yet! *)
4
5include "basics/lists/list.ma".
6
7include "common/Errors.ma".
8include "common/Globalenvs.ma".
9include "common/IO.ma".
10include "common/SmallstepExec.ma".
11
12include "RTLabs/syntax.ma".
13
14definition genv ≝ (genv_t Genv) (fundef internal_function).
15
16record frame : Type[0] ≝
17{ func   : internal_function
18; locals : register_env val
19; next   : label
20; next_ok: present ?? (f_graph func) next
21; sp     : block
22; retdst : option register
23}.
24
25definition adv : ∀l:label. ∀f:frame. present ?? (f_graph (func f)) l → frame ≝
26λl,f,p. mk_frame (func f) (locals f) l p (sp f) (retdst f).
27
28inductive state : Type[0] ≝
29| State :
30   ∀   f : frame.
31   ∀  fs : list frame.
32   ∀   m : mem.
33   state
34| Callstate :
35   ∀  fd : fundef internal_function.
36   ∀args : list val.
37   ∀ dst : option register.
38   ∀ stk : list frame.
39   ∀   m : mem.
40   state
41| Returnstate :
42   ∀ rtv : option val.
43   ∀ dst : option register.
44   ∀ stk : list frame.
45   ∀   m : mem.
46   state
47| Finalstate :
48   ∀   r : int.
49   state
50.
51
52definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m.
53
54definition init_locals : list (register × typ) → register_env val ≝
55foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??).
56
57definition reg_store ≝
58λreg,v,locals.
59  update RegisterTag val locals reg v.
60
61axiom WrongNumberOfParameters : String.
62
63let rec params_store (rs:list (register × typ)) (vs:list val) (locals : register_env val) : res (register_env val) ≝
64match rs with
65[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
66| cons rt rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
67  let 〈r,ty〉 ≝ rt in
68  let locals' ≝ add RegisterTag val locals r v in
69  params_store rst vst locals'
70] ].
71
72axiom BadRegister : String.
73
74definition reg_retrieve : register_env ? → register → res val ≝
75λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
76
77axiom FailedOp : String.
78axiom MissingSymbol : String.
79
80axiom MissingStatement : String.
81axiom FailedConstant : String.
82axiom FailedLoad : String.
83axiom FailedStore : String.
84axiom BadFunction : String.
85axiom BadJumpTable : String.
86axiom BadJumpValue : String.
87axiom FinalState : String.
88axiom ReturnMismatch : String.
89
90definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
91λge,st.
92match st return λ_. IO ??? with
93[ State f fs m ⇒
94  let s ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
95  match s return λs. labels_present ? s → IO ??? with
96  [ St_skip l ⇒ λH. return 〈E0, build_state f fs m l ?〉
97  | St_cost cl l ⇒ λH. return 〈Echarge cl, build_state f fs m l ?〉
98  | St_const _ r cst l ⇒ λH.
99      ! v ← opt_to_res … (msg FailedConstant) (eval_constant ? (find_symbol … ge) (sp f) cst);
100      ! locals ← reg_store r v (locals f);
101      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
102  | St_op1 _ _ op dst src l ⇒ λH.
103      ! v ← reg_retrieve (locals f) src;
104      ! v' ← opt_to_res … (msg FailedOp) (eval_unop ?? op v);
105      ! locals ← reg_store dst v' (locals f);
106      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
107  | St_op2 _ _ _  op dst src1 src2 l ⇒ λH.
108      ! v1 ← reg_retrieve (locals f) src1;
109      ! v2 ← reg_retrieve (locals f) src2;
110      ! v' ← opt_to_res … (msg FailedOp) (eval_binop ??? op v1 v2);
111      ! locals ← reg_store dst v' (locals f);
112      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
113  | St_load chunk addr dst l ⇒ λH.
114      ! vaddr ← reg_retrieve (locals f) addr;
115      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
116      ! locals ← reg_store dst v (locals f);
117      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
118  | St_store chunk addr src l ⇒ λH.
119      ! vaddr ← reg_retrieve (locals f) addr;
120      ! v ← reg_retrieve (locals f) src;
121      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
122      return 〈E0, build_state f fs m' l ?〉
123  | St_call_id id args dst l ⇒ λH.
124      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
125      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
126      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
127      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
128  | St_call_ptr frs args dst l ⇒ λH.
129      ! fv ← reg_retrieve (locals f) frs;
130      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
131      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
132      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
133(*
134  | St_tailcall_id id args ⇒ λH.
135      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
136      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
137      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
138      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
139  | St_tailcall_ptr frs args ⇒ λH.
140      ! fv ← reg_retrieve (locals f) frs;
141      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
142      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
143      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
144*)
145  | St_cond src ltrue lfalse ⇒ λH.
146      ! v ← reg_retrieve (locals f) src;
147      ! b ← eval_bool_of_val v;
148      return 〈E0, build_state f fs m (if b then ltrue else lfalse) ?〉
149
150  | St_jumptable r ls ⇒ λH.
151      ! v ← reg_retrieve (locals f) r;
152      match v with
153      [ Vint _ i ⇒
154          match nth_opt ? (nat_of_bitvector ? i) ls return λx. nth_opt ??? = x → ? with
155          [ None ⇒ λ_. Error ? (msg BadJumpTable)
156          | Some l ⇒ λE. return 〈E0, build_state f fs m l ?〉
157          ] (refl ??)
158      | _ ⇒ Error ? (msg BadJumpValue)
159      ]
160
161  | St_return ⇒ λH.
162      ! v ← match f_result (func f) with
163            [ None ⇒ return (None ?)
164            | Some rt ⇒
165                let 〈r,ty〉 ≝ rt in
166                ! v ← reg_retrieve (locals f) r;
167                return (Some ? v)
168            ];
169      return 〈E0, Returnstate v (retdst f) fs (free ? m (sp f))〉
170  ] (f_closed (func f) (next f) s ?)
171| Callstate fd params dst fs m ⇒
172    match fd return λ_. IO ??? with
173    [ Internal fn ⇒
174        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
175        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
176           here *)
177        let 〈m', sp〉 ≝ alloc ? m 0 (f_stacksize fn) Any in
178        return 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉
179    | External fn ⇒
180        ! evargs ← err_to_io … (check_eventval_list params (sig_args (ef_sig fn)));
181        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
182        return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
183    ]
184| Returnstate v dst fs m ⇒
185    match fs with
186    [ nil ⇒
187        match v with
188        [ Some v' ⇒
189          match v' with
190          [ Vint sz r ⇒ match sz return λsz. bvint sz → monad Res ? with
191                        [ I32 ⇒ λr. return 〈E0, Finalstate r〉
192                        | _ ⇒ λ_. Error ? (msg ReturnMismatch)
193                        ] r
194          | _ ⇒ Error ? (msg ReturnMismatch)
195          ]
196        | _ ⇒ Error ? (msg ReturnMismatch)
197        ]
198    | cons f fs' ⇒
199        ! locals ← match dst with
200                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
201                                         | _ ⇒ Error ? (msg ReturnMismatch) ]
202                   | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch)
203                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
204        return 〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉
205    ]
206| Finalstate r ⇒ Error ? (msg FinalState) (* Already in final state *)
207]. try @(next_ok f) try @lookup_lookup_present try @H
208[ cases b [ @(proj1 ?? H) | @(proj2 ?? H) ]
209| whd in H; @(All_nth … H ? E)
210| cases (f_entry fn) //
211] qed.
212
213definition RTLabs_is_final : state → option int ≝
214λs. match s with
215[ Finalstate r ⇒ Some ? r
216| _ ⇒ None ?
217].
218
219definition RTLabs_exec : trans_system io_out io_in ≝
220  mk_trans_system … ? (λ_.RTLabs_is_final) eval_statement.
221
222definition make_global : RTLabs_program → genv ≝
223λp. globalenv Genv ?? (λx.[Init_space x]) p.
224
225definition make_initial_state : RTLabs_program → res state ≝
226λp.
227  let ge ≝ make_global p in
228  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
229  let main ≝ prog_main ?? p in
230  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
231  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
232  OK ? (Callstate f (nil ?) (None ?) (nil ?) m).
233
234definition RTLabs_fullexec : fullexec io_out io_in ≝
235  mk_fullexec … RTLabs_exec make_global make_initial_state.
236
237
238(* Some lemmas about the semantics. *)
239
240(* Note parts of frames and states that are preserved. *)
241
242inductive frame_rel : frame → frame → Prop ≝
243| mk_frame_rel :
244  ∀func,locals,next,next_ok,sp,retdst,locals',next',next_ok'. frame_rel
245   (mk_frame func locals next next_ok sp retdst)
246   (mk_frame func locals' next' next_ok' sp retdst)
247.
248
249inductive state_rel : genv → state → state → Prop ≝
250| normal : ∀ge,f,f',fs,m,m'. frame_rel f f' → state_rel ge (State f fs m) (State f' fs m')
251| to_call : ∀ge,f,fs,m,fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst (f'::fs) m)
252(*
253| tail_call : ∀ge,f,fs,m,fd,args,dst,m'. ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst fs m')
254*)
255| from_call : ∀ge,fn,locals,next,nok,sp,fs,m,args,dst,m'. state_rel ge (Callstate (Internal ? fn) args dst fs m) (State (mk_frame fn locals next nok sp dst) fs m')
256| to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m')
257| from_ret : ∀ge,f,fs,rtv,dst,f',m. frame_rel f f' → state_rel ge (Returnstate rtv dst (f::fs) m) (State f' fs m)
258| finish : ∀ge,r,dst,m. state_rel ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) (Finalstate r)
259.
260
261lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Prop.
262  (∀a. e = OK A a → f a = OK ? v → P v) →
263  (match e with [ OK v ⇒ f v | Error m ⇒ Error ? m ] = OK ? v → P v).
264#A #B *
265[ #a #f #v #P #H #E whd in E:(??%?); @(H a) //
266| #m #f #v #P #H #E whd in E:(??%?); destruct
267] qed.
268
269lemma bind_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
270  (∀a. e = OK A a → f a = OK B v → P v) →
271  (match e »= f with [ OK v ⇒ Value … v | Error m ⇒ Wrong … m ] = Value O I B v → P v).
272#O #I #A #B *
273[ #a #f #v #P #H #E @H [ @a | @refl | normalize in E; cases (f a) in E ⊢ %;
274  [ #v' #E normalize in E; destruct @refl | #m #E normalize in E; destruct ] ]
275| #m #f #v #P #H #E whd in E:(??%?); destruct
276] qed.
277
278lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
279  (∀a. e = Value ??? a → f a = Value ??? v → P v) →
280  (bindIO O I A B e f = Value ??? v → P v).
281#O #I #A #B *
282[ #o #k #f #v #P #H #E whd in E:(??%?); destruct
283| #a #f #v #P #H #E @H [ @a | @refl | @E ]
284| #m #f #v #P #H #E whd in E:(??%?); destruct
285] qed.
286
287lemma eval_perserves : ∀ge,s,tr,s'.
288  eval_statement ge s = Value ??? 〈tr,s'〉 →
289  state_rel ge s s'.
290#ge *
291[ * #func #locals #next #next_ok #sp #retdst #fs #m
292  #tr #s'
293  whd in ⊢ (??%? → ?);
294  generalize in ⊢ (??(?%)? → ?);
295  cases (lookup_present LabelTag statement (f_graph func) next next_ok)
296  [ #l #LP whd in ⊢ (??%? → ?); #E destruct % %
297  | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % %
298  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct % %
299  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
300  | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
301  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
302  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
303  | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ????) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
304  | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
305(*
306  | #id #rs #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
307  | #r #rs #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
308*)
309  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
310  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: #vl #E whd in E:(??%?); destruct ]
311  | #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %4
312  ]
313| * #fn #args #retdst #stk #m #tr #s'
314  whd in ⊢ (??%? → ?);
315  [ @bind_value #loc #Eloc cases (alloc ? m O ??) #m' #b whd in ⊢ (??%? → ?);
316    #E destruct %3
317  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
318  ]
319| #v #r * [2: #f #fs ] #m #tr #s'
320  whd in ⊢ (??%? → ?);
321  [ @bind_value #loc #Eloc #E whd in E:(??%?); destruct
322    %5 cases f #func #locals #next #next_ok #sp #retdst %
323  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct // | *: normalize #a try #b destruct ] ]
324  ]
325| #r #tr #s' normalize #E destruct
326] qed.
327
328
329lemma initial_state_is_not_final : ∀p,s.
330  make_initial_state p = OK ? s →
331  RTLabs_is_final s = None ?.
332#p #s whd in ⊢ (??%? → ?);
333@bind_ok #m #Em
334@bind_ok #b #Eb
335@bind_ok #f #Ef
336#E destruct
337@refl
338qed.
Note: See TracBrowser for help on using the repository browser.