source: src/RTLabs/semantics.ma @ 1680

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

Comment out unused tailcalls in Cminor and RTLabs.
(They would be a little tricky to deal with in RTLabs/Traces.ma, and we
don't currently generate them.)

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