From 25b9b003178002360d666919f2e49e7f5f4a36e2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Feb 2012 19:14:14 +0000 Subject: Merge of the "volatile" branch: - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cexec.v | 2839 +++++++++++++++++++++++++++++------------------------ 1 file changed, 1529 insertions(+), 1310 deletions(-) (limited to 'cfrontend/Cexec.v') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 4bce535..b3c3f6b 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -13,6 +13,7 @@ (** Animating the CompCert C semantics *) Require Import Axioms. +Require Import Classical. Require Import Coqlib. Require Import Errors. Require Import Maps. @@ -28,28 +29,20 @@ Require Import Csyntax. Require Import Csem. Require Cstrategy. -Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2} -with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2} -with fieldlist_eq: forall (fld1 fld2: fieldlist), {fld1=fld2} + {fld1<>fld2}. -Proof. - assert (forall (x y: intsize), {x=y} + {x<>y}). decide equality. - assert (forall (x y: signedness), {x=y} + {x<>y}). decide equality. - assert (forall (x y: floatsize), {x=y} + {x<>y}). decide equality. - generalize ident_eq zeq. intros E1 E2. - decide equality. - decide equality. - generalize ident_eq. intros E1. - decide equality. -Defined. - -Opaque type_eq. - (** Error monad with options or lists *) Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end) (at level 200, X ident, A at level 100, B at level 200) : option_monad_scope. +Notation "'do' X , Y <- A ; B" := (match A with Some (X, Y) => B | None => None end) + (at level 200, X ident, Y ident, A at level 100, B at level 200) + : option_monad_scope. + +Notation "'do' X , Y , Z <- A ; B" := (match A with Some (X, Y, Z) => B | None => None end) + (at level 200, X ident, Y ident, Z ident, A at level 100, B at level 200) + : option_monad_scope. + Notation " 'check' A ; B" := (if A then B else None) (at level 200, A at level 100, B at level 200) : option_monad_scope. @@ -99,315 +92,1098 @@ Proof. destruct s; (left; congruence) || (right; congruence). Qed. -(** * Reduction of expressions *) +(** * Events, volatile memory accesses, and external functions. *) Section EXEC. Variable ge: genv. -Inductive reduction: Type := - | Lred (l': expr) (m': mem) - | Rred (r': expr) (m': mem) - | Callred (fd: fundef) (args: list val) (tyres: type) (m': mem). - -Section EXPRS. - -Variable e: env. - -Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) : option (list val) := - match vtl, tl with - | nil, Tnil => Some nil - | (v1,t1)::vtl, Tcons t1' tl => - do v <- sem_cast v1 t1 t1'; do vl <- sem_cast_arguments vtl tl; Some(v::vl) +Definition eventval_of_val (v: val) (t: typ) : option eventval := + match v, t with + | Vint i, AST.Tint => Some (EVint i) + | Vfloat f, AST.Tfloat => Some (EVfloat f) + | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol ge b; Some (EVptr_global id ofs) | _, _ => None end. -(** The result of stepping an expression can be -- [None] denoting that the expression is stuck; -- [Some nil] meaning that the expression is fully reduced - (it's [Eval] for a r-value and [Eloc] for a l-value); -- [Some ll] meaning that the expression can reduce to any of - the elements of [ll]. Each element is a pair of a context - and a reduction inside this context (see type [reduction] above). -*) - -Definition reducts (A: Type): Type := option (list ((expr -> A) * reduction)). - -Definition topred (r: reduction) : reducts expr := - Some (((fun (x: expr) => x), r) :: nil). - -Definition incontext {A B: Type} (ctx: A -> B) (r: reducts A) : reducts B := - match r with - | None => None - | Some l => Some (map (fun z => ((fun (x: expr) => ctx(fst z x)), snd z)) l) +Fixpoint list_eventval_of_val (vl: list val) (tl: list typ) : option (list eventval) := + match vl, tl with + | nil, nil => Some nil + | v1::vl, t1::tl => + do ev1 <- eventval_of_val v1 t1; + do evl <- list_eventval_of_val vl tl; + Some (ev1 :: evl) + | _, _ => None end. -Definition incontext2 {A1 A2 B: Type} - (ctx1: A1 -> B) (r1: reducts A1) - (ctx2: A2 -> B) (r2: reducts A2) : reducts B := - match r1, r2 with - | None, _ => None - | _, None => None - | Some l1, Some l2 => - Some (map (fun z => ((fun (x: expr) => ctx1(fst z x)), snd z)) l1 - ++ map (fun z => ((fun (x: expr) => ctx2(fst z x)), snd z)) l2) +Definition val_of_eventval (ev: eventval) (t: typ) : option val := + match ev, t with + | EVint i, AST.Tint => Some (Vint i) + | EVfloat f, AST.Tfloat => Some (Vfloat f) + | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol ge id; Some (Vptr b ofs) + | _, _ => None end. -Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := - match k, a with - | LV, Eloc b ofs ty => - Some nil - | LV, Evar x ty => - match e!x with - | Some(b, ty') => - check type_eq ty ty'; - topred (Lred (Eloc b Int.zero ty) m) - | None => - do b <- Genv.find_symbol ge x; - do ty' <- type_of_global ge b; - check type_eq ty ty'; - topred (Lred (Eloc b Int.zero ty) m) - end - | LV, Ederef r ty => - match is_val r with - | Some(Vptr b ofs, ty') => - topred (Lred (Eloc b ofs ty) m) - | Some _ => - None - | None => - incontext (fun x => Ederef x ty) (step_expr RV r m) - end - | LV, Efield l f ty => - match is_loc l with - | Some(b, ofs, ty') => - match ty' with - | Tstruct id fList => - match field_offset f fList with - | Error _ => None - | OK delta => topred (Lred (Eloc b (Int.add ofs (Int.repr delta)) ty) m) - end - | Tunion id fList => - topred (Lred (Eloc b ofs ty) m) - | _ => None - end - | None => - incontext (fun x => Efield x f ty) (step_expr LV l m) - end - | RV, Eval v ty => - Some nil - | RV, Evalof l ty => - match is_loc l with - | Some(b, ofs, ty') => - check type_eq ty ty'; - do v <- load_value_of_type ty m b ofs; - topred (Rred (Eval v ty) m) - | None => - incontext (fun x => Evalof x ty) (step_expr LV l m) - end - | RV, Eaddrof l ty => - match is_loc l with - | Some(b, ofs, ty') => topred (Rred (Eval (Vptr b ofs) ty) m) - | None => incontext (fun x => Eaddrof x ty) (step_expr LV l m) - end - | RV, Eunop op r1 ty => - match is_val r1 with - | Some(v1, ty1) => - do v <- sem_unary_operation op v1 ty1; - topred (Rred (Eval v ty) m) - | None => - incontext (fun x => Eunop op x ty) (step_expr RV r1 m) - end - | RV, Ebinop op r1 r2 ty => - match is_val r1, is_val r2 with - | Some(v1, ty1), Some(v2, ty2) => - do v <- sem_binary_operation op v1 ty1 v2 ty2 m; - topred (Rred (Eval v ty) m) - | _, _ => - incontext2 (fun x => Ebinop op x r2 ty) (step_expr RV r1 m) - (fun x => Ebinop op r1 x ty) (step_expr RV r2 m) - end - | RV, Ecast r1 ty => - match is_val r1 with - | Some(v1, ty1) => - do v <- sem_cast v1 ty1 ty; - topred (Rred (Eval v ty) m) - | None => - incontext (fun x => Ecast x ty) (step_expr RV r1 m) - end - | RV, Econdition r1 r2 r3 ty => - match is_val r1 with - | Some(v1, ty1) => - do b <- bool_val v1 ty1; - topred (Rred (Eparen (if b then r2 else r3) ty) m) - | None => - incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m) - end - | RV, Esizeof ty' ty => - topred (Rred (Eval (Vint (Int.repr (sizeof ty'))) ty) m) - | RV, Eassign l1 r2 ty => - match is_loc l1, is_val r2 with - | Some(b, ofs, ty1), Some(v2, ty2) => - check type_eq ty1 ty; - do v <- sem_cast v2 ty2 ty1; - do m' <- store_value_of_type ty1 m b ofs v; - topred (Rred (Eval v ty) m') - | _, _ => - incontext2 (fun x => Eassign x r2 ty) (step_expr LV l1 m) - (fun x => Eassign l1 x ty) (step_expr RV r2 m) - end - | RV, Eassignop op l1 r2 tyres ty => - match is_loc l1, is_val r2 with - | Some(b, ofs, ty1), Some(v2, ty2) => - check type_eq ty1 ty; - do v1 <- load_value_of_type ty1 m b ofs; - do v <- sem_binary_operation op v1 ty1 v2 ty2 m; - do v' <- sem_cast v tyres ty1; - do m' <- store_value_of_type ty1 m b ofs v'; - topred (Rred (Eval v' ty) m') - | _, _ => - incontext2 (fun x => Eassignop op x r2 tyres ty) (step_expr LV l1 m) - (fun x => Eassignop op l1 x tyres ty) (step_expr RV r2 m) - end - | RV, Epostincr id l ty => - match is_loc l with - | Some(b, ofs, ty1) => - check type_eq ty1 ty; - do v1 <- load_value_of_type ty m b ofs; - do v2 <- sem_incrdecr id v1 ty; - do v3 <- sem_cast v2 (typeconv ty) ty; - do m' <- store_value_of_type ty m b ofs v3; - topred (Rred (Eval v1 ty) m') - | None => - incontext (fun x => Epostincr id x ty) (step_expr LV l m) - end - | RV, Ecomma r1 r2 ty => - match is_val r1 with - | Some _ => - check type_eq (typeof r2) ty; - topred (Rred r2 m) - | None => - incontext (fun x => Ecomma x r2 ty) (step_expr RV r1 m) - end - | RV, Eparen r1 ty => - match is_val r1 with - | Some (v1, ty1) => - do v <- sem_cast v1 ty1 ty; - topred (Rred (Eval v ty) m) - | None => - incontext (fun x => Eparen x ty) (step_expr RV r1 m) - end - | RV, Ecall r1 rargs ty => - match is_val r1, is_val_list rargs with - | Some(vf, tyf), Some vtl => - match classify_fun tyf with - | fun_case_f tyargs tyres => - do fd <- Genv.find_funct ge vf; - do vargs <- sem_cast_arguments vtl tyargs; - check type_eq (type_of_fundef fd) (Tfunction tyargs tyres); - topred (Callred fd vargs ty m) - | _ => None - end - | _, _ => - incontext2 (fun x => Ecall x rargs ty) (step_expr RV r1 m) - (fun x => Ecall r1 x ty) (step_exprlist rargs m) - end - | _, _ => None - end +Lemma eventval_of_val_sound: + forall v t ev, eventval_of_val v t = Some ev -> eventval_match ge ev t v. +Proof. + intros. destruct v; destruct t; simpl in H; inv H. + constructor. + constructor. + destruct (Genv.invert_symbol ge b) as [id|]_eqn; inv H1. + constructor. apply Genv.invert_find_symbol; auto. +Qed. -with step_exprlist (rl: exprlist) (m: mem): reducts exprlist := - match rl with - | Enil => - Some nil - | Econs r1 rs => - incontext2 (fun x => Econs x rs) (step_expr RV r1 m) - (fun x => Econs r1 x) (step_exprlist rs m) - end. +Lemma eventval_of_val_complete: + forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev. +Proof. + induction 1; simpl; auto. + rewrite (Genv.find_invert_symbol _ _ H). auto. +Qed. -(** Soundness: if [step_expr] returns [Some ll], then every element - of [ll] is a reduct. *) +Lemma list_eventval_of_val_sound: + forall vl tl evl, list_eventval_of_val vl tl = Some evl -> eventval_list_match ge evl tl vl. +Proof with try discriminate. + induction vl; destruct tl; simpl; intros; inv H. + constructor. + destruct (eventval_of_val a t) as [ev1|]_eqn... + destruct (list_eventval_of_val vl tl) as [evl'|]_eqn... + inv H1. constructor. apply eventval_of_val_sound; auto. eauto. +Qed. -Lemma context_compose: - forall k2 k3 C2, context k2 k3 C2 -> - forall k1 C1, context k1 k2 C1 -> - context k1 k3 (fun x => C2(C1 x)) -with contextlist_compose: - forall k2 C2, contextlist k2 C2 -> - forall k1 C1, context k1 k2 C1 -> - contextlist k1 (fun x => C2(C1 x)). +Lemma list_eventval_of_val_complete: + forall evl tl vl, eventval_list_match ge evl tl vl -> list_eventval_of_val vl tl = Some evl. Proof. - induction 1; intros; try (constructor; eauto). - replace (fun x => C1 x) with C1. auto. apply extensionality; auto. - induction 1; intros; constructor; eauto. + induction 1; simpl. auto. + rewrite (eventval_of_val_complete _ _ _ H). rewrite IHeventval_list_match. auto. Qed. -Hint Constructors context contextlist. -Hint Resolve context_compose contextlist_compose. +Lemma val_of_eventval_sound: + forall ev t v, val_of_eventval ev t = Some v -> eventval_match ge ev t v. +Proof. + intros. destruct ev; destruct t; simpl in H; inv H. + constructor. + constructor. + destruct (Genv.find_symbol ge i) as [b|]_eqn; inv H1. + constructor. auto. +Qed. -Definition reduction_ok (a: expr) (m: mem) (rd: reduction) : Prop := - match rd with - | Lred l' m' => lred ge e a m l' m' - | Rred r' m' => rred a m r' m' - | Callred fd args tyres m' => callred ge a fd args tyres /\ m' = m - end. +Lemma val_of_eventval_complete: + forall ev t v, eventval_match ge ev t v -> val_of_eventval ev t = Some v. +Proof. + induction 1; simpl; auto. rewrite H; auto. +Qed. -Definition reduction_kind (rd: reduction): kind := - match rd with - | Lred l' m' => LV - | Rred r' m' => RV - | Callred fd args tyres m' => RV - end. +(** Volatile memory accesses. *) + +Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: int) + : option (world * trace * val) := + if block_is_volatile ge b then + do id <- Genv.invert_symbol ge b; + match nextworld_vload w chunk id ofs with + | None => None + | Some(res, w') => + do vres <- val_of_eventval res (type_of_chunk chunk); + Some(w', Event_vload chunk id ofs res :: nil, Val.load_result chunk vres) + end + else + do v <- Mem.load chunk m b (Int.unsigned ofs); + Some(w, E0, v). + +Definition do_volatile_store (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: int) (v: val) + : option (world * trace * mem) := + if block_is_volatile ge b then + do id <- Genv.invert_symbol ge b; + do ev <- eventval_of_val v (type_of_chunk chunk); + do w' <- nextworld_vstore w chunk id ofs ev; + Some(w', Event_vstore chunk id ofs ev :: nil, m) + else + do m' <- Mem.store chunk m b (Int.unsigned ofs) v; + Some(w, E0, m'). -Ltac monadInv := +Ltac mydestr := match goal with - | [ H: match ?x with Some _ => _ | None => None end = Some ?y |- _ ] => - destruct x as []_eqn; [monadInv|discriminate] - | [ H: match ?x with left _ => _ | right _ => None end = Some ?y |- _ ] => - destruct x; [monadInv|discriminate] + | [ |- None = Some _ -> _ ] => intro X; discriminate + | [ |- Some _ = Some _ -> _ ] => intro X; inv X + | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr + | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr + | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr | _ => idtac end. -Lemma sem_cast_arguments_sound: - forall rargs vtl tyargs vargs, - is_val_list rargs = Some vtl -> - sem_cast_arguments vtl tyargs = Some vargs -> - cast_arguments rargs tyargs vargs. +Lemma do_volatile_load_sound: + forall w chunk m b ofs w' t v, + do_volatile_load w chunk m b ofs = Some(w', t, v) -> + volatile_load ge chunk m b ofs t v /\ possible_trace w t w'. Proof. - induction rargs; simpl; intros. - inv H. destruct tyargs; simpl in H0; inv H0. constructor. - monadInv. inv H. simpl in H0. destruct p as [v1 t1]. destruct tyargs; try congruence. monadInv. - inv H0. rewrite (is_val_inv _ _ _ Heqo). constructor. auto. eauto. + intros until v. unfold do_volatile_load. mydestr. + destruct p as [ev w'']. mydestr. + split. constructor; auto. apply Genv.invert_find_symbol; auto. + apply val_of_eventval_sound; auto. + econstructor. constructor; eauto. constructor. + split. constructor; auto. constructor. Qed. -Definition reducts_ok (k: kind) (a: expr) (m: mem) (res: reducts expr) : Prop := - match res with - | None => True - | Some nil => match k with LV => is_loc a <> None | RV => is_val a <> None end - | Some ll => - forall C rd, - In (C, rd) ll -> - context (reduction_kind rd) k C /\ exists a', a = C a' /\ reduction_ok a' m rd - end. +Lemma do_volatile_load_complete: + forall w chunk m b ofs w' t v, + volatile_load ge chunk m b ofs t v -> possible_trace w t w' -> + do_volatile_load w chunk m b ofs = Some(w', t, v). +Proof. + unfold do_volatile_load; intros. inv H. + rewrite H1. rewrite (Genv.find_invert_symbol _ _ H2). inv H0. inv H8. inv H6. rewrite H9. + rewrite (val_of_eventval_complete _ _ _ H3). auto. + rewrite H1. rewrite H2. inv H0. auto. +Qed. -Definition list_reducts_ok (al: exprlist) (m: mem) (res: reducts exprlist) : Prop := - match res with - | None => True - | Some nil => is_val_list al <> None - | Some ll => - forall C rd, +Lemma do_volatile_store_sound: + forall w chunk m b ofs v w' t m', + do_volatile_store w chunk m b ofs v = Some(w', t, m') -> + volatile_store ge chunk m b ofs v t m' /\ possible_trace w t w'. +Proof. + intros until m'. unfold do_volatile_store. mydestr. + split. constructor; auto. apply Genv.invert_find_symbol; auto. + apply eventval_of_val_sound; auto. + econstructor. constructor; eauto. constructor. + split. constructor; auto. constructor. +Qed. + +Lemma do_volatile_store_complete: + forall w chunk m b ofs v w' t m', + volatile_store ge chunk m b ofs v t m' -> possible_trace w t w' -> + do_volatile_store w chunk m b ofs v = Some(w', t, m'). +Proof. + unfold do_volatile_store; intros. inv H. + rewrite H1. rewrite (Genv.find_invert_symbol _ _ H2). + rewrite (eventval_of_val_complete _ _ _ H3). + inv H0. inv H8. inv H6. rewrite H9. auto. + rewrite H1. rewrite H2. inv H0. auto. +Qed. + +(** Accessing locations *) + +Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) : option (world * trace * val) := + match access_mode ty with + | By_value chunk => + match type_is_volatile ty with + | false => do v <- Mem.loadv chunk m (Vptr b ofs); Some(w, E0, v) + | true => do_volatile_load w chunk m b ofs + end + | By_reference => Some(w, E0, Vptr b ofs) + | By_copy => Some(w, E0, Vptr b ofs) + | _ => None + end. + +Definition assign_copy_ok (ty: type) (b: block) (ofs: int) (b': block) (ofs': int) : Prop := + (alignof ty | Int.unsigned ofs') /\ (alignof ty | Int.unsigned ofs) /\ + (b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs + \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs + \/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs'). + +Remark check_assign_copy: + forall (ty: type) (b: block) (ofs: int) (b': block) (ofs': int), + { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }. +Proof with try (right; intuition omega). + intros. unfold assign_copy_ok. + assert (alignof ty > 0). apply alignof_pos; auto. + destruct (Zdivide_dec (alignof ty) (Int.unsigned ofs')); auto... + destruct (Zdivide_dec (alignof ty) (Int.unsigned ofs)); auto... + assert (Y: {b' <> b \/ + Int.unsigned ofs' = Int.unsigned ofs \/ + Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/ + Int.unsigned ofs + sizeof ty <= Int.unsigned ofs'} + + {~(b' <> b \/ + Int.unsigned ofs' = Int.unsigned ofs \/ + Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/ + Int.unsigned ofs + sizeof ty <= Int.unsigned ofs')}). + destruct (eq_block b' b); auto. + destruct (zeq (Int.unsigned ofs') (Int.unsigned ofs)); auto. + destruct (zle (Int.unsigned ofs' + sizeof ty) (Int.unsigned ofs)); auto. + destruct (zle (Int.unsigned ofs + sizeof ty) (Int.unsigned ofs')); auto. + right; intuition omega. + destruct Y... left; intuition omega. +Qed. + +Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) (v: val): option (world * trace * mem) := + match access_mode ty with + | By_value chunk => + match type_is_volatile ty with + | false => do m' <- Mem.storev chunk m (Vptr b ofs) v; Some(w, E0, m') + | true => do_volatile_store w chunk m b ofs v + end + | By_copy => + match v with + | Vptr b' ofs' => + if check_assign_copy ty b ofs b' ofs' then + do bytes <- Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ty); + do m' <- Mem.storebytes m b (Int.unsigned ofs) bytes; + Some(w, E0, m') + else None + | _ => None + end + | _ => None + end. + +Lemma do_deref_loc_sound: + forall w ty m b ofs w' t v, + do_deref_loc w ty m b ofs = Some(w', t, v) -> + deref_loc ge ty m b ofs t v /\ possible_trace w t w'. +Proof. + unfold do_deref_loc; intros until v. + destruct (access_mode ty) as []_eqn; mydestr. + intros. exploit do_volatile_load_sound; eauto. intuition. eapply deref_loc_volatile; eauto. + split. eapply deref_loc_value; eauto. constructor. + split. eapply deref_loc_reference; eauto. constructor. + split. eapply deref_loc_copy; eauto. constructor. +Qed. + +Lemma do_deref_loc_complete: + forall w ty m b ofs w' t v, + deref_loc ge ty m b ofs t v -> possible_trace w t w' -> + do_deref_loc w ty m b ofs = Some(w', t, v). +Proof. + unfold do_deref_loc; intros. inv H. + inv H0. rewrite H1; rewrite H2; rewrite H3; auto. + rewrite H1; rewrite H2. apply do_volatile_load_complete; auto. + inv H0. rewrite H1. auto. + inv H0. rewrite H1. auto. +Qed. + +Lemma do_assign_loc_sound: + forall w ty m b ofs v w' t m', + do_assign_loc w ty m b ofs v = Some(w', t, m') -> + assign_loc ge ty m b ofs v t m' /\ possible_trace w t w'. +Proof. + unfold do_assign_loc; intros until m'. + destruct (access_mode ty) as []_eqn; mydestr. + intros. exploit do_volatile_store_sound; eauto. intuition. eapply assign_loc_volatile; eauto. + split. eapply assign_loc_value; eauto. constructor. + destruct v; mydestr. destruct a as [P [Q R]]. + split. eapply assign_loc_copy; eauto. constructor. +Qed. + +Lemma do_assign_loc_complete: + forall w ty m b ofs v w' t m', + assign_loc ge ty m b ofs v t m' -> possible_trace w t w' -> + do_assign_loc w ty m b ofs v = Some(w', t, m'). +Proof. + unfold do_assign_loc; intros. inv H. + inv H0. rewrite H1; rewrite H2; rewrite H3; auto. + rewrite H1; rewrite H2. apply do_volatile_store_complete; auto. + rewrite H1. destruct (check_assign_copy ty b ofs b' ofs'). + inv H0. rewrite H5; rewrite H6; auto. + elim n. red; tauto. +Qed. + +(** System calls and library functions *) + +Definition do_ef_external (name: ident) (sg: signature) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + do args <- list_eventval_of_val vargs (sig_args sg); + match nextworld_io w name args with + | None => None + | Some(res, w') => + do vres <- val_of_eventval res (proj_sig_res sg); + Some(w', Event_syscall name args res :: E0, vres, m) + end. + +Definition do_ef_volatile_load (chunk: memory_chunk) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match vargs with + | Vptr b ofs :: nil => do w',t,v <- do_volatile_load w chunk m b ofs; Some(w',t,v,m) + | _ => None + end. + +Definition do_ef_volatile_store (chunk: memory_chunk) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match vargs with + | Vptr b ofs :: v :: nil => do w',t,m' <- do_volatile_store w chunk m b ofs v; Some(w',t,Vundef,m') + | _ => None + end. + +Definition do_ef_volatile_load_global (chunk: memory_chunk) (id: ident) (ofs: int) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + do b <- Genv.find_symbol ge id; do_ef_volatile_load chunk w (Vptr b ofs :: vargs) m. + +Definition do_ef_volatile_store_global (chunk: memory_chunk) (id: ident) (ofs: int) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + do b <- Genv.find_symbol ge id; do_ef_volatile_store chunk w (Vptr b ofs :: vargs) m. + +Definition do_ef_malloc + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match vargs with + | Vint n :: nil => + let (m', b) := Mem.alloc m (-4) (Int.unsigned n) in + do m'' <- Mem.store Mint32 m' b (-4) (Vint n); + Some(w, E0, Vptr b Int.zero, m'') + | _ => None + end. + +Definition do_ef_free + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match vargs with + | Vptr b lo :: nil => + do vsz <- Mem.load Mint32 m b (Int.unsigned lo - 4); + match vsz with + | Vint sz => + check (zlt 0 (Int.unsigned sz)); + do m' <- Mem.free m b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz); + Some(w, E0, Vundef, m') + | _ => None + end + | _ => None + end. + +Definition memcpy_args_ok + (sz al: Z) (bdst: block) (odst: Z) (bsrc: block) (osrc: Z) : Prop := + (al = 1 \/ al = 2 \/ al = 4) + /\ sz > 0 + /\ (al | sz) /\ (al | osrc) /\ (al | odst) + /\ (bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc). + +Remark memcpy_check_args: + forall sz al bdst odst bsrc osrc, + {memcpy_args_ok sz al bdst odst bsrc osrc} + {~memcpy_args_ok sz al bdst odst bsrc osrc}. +Proof with try (right; intuition omega). + intros. + assert (X: {al = 1 \/ al = 2 \/ al = 4} + {~(al = 1 \/ al = 2 \/ al = 4)}). + destruct (zeq al 1); auto. destruct (zeq al 2); auto. destruct (zeq al 4); auto... + unfold memcpy_args_ok. destruct X... + assert (al > 0) by (intuition omega). + destruct (zlt 0 sz)... + destruct (Zdivide_dec al sz); auto... + destruct (Zdivide_dec al osrc); auto... + destruct (Zdivide_dec al odst); auto... + assert (Y: {bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc} + +{~(bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc)}). + destruct (eq_block bsrc bdst); auto. + destruct (zeq osrc odst); auto. + destruct (zle (osrc + sz) odst); auto. + destruct (zle (odst + sz) osrc); auto. + right; intuition omega. + destruct Y... left; intuition omega. +Qed. + +Definition do_ef_memcpy (sz al: Z) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match vargs with + | Vptr bdst odst :: Vptr bsrc osrc :: nil => + if memcpy_check_args sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc) then + do bytes <- Mem.loadbytes m bsrc (Int.unsigned osrc) sz; + do m' <- Mem.storebytes m bdst (Int.unsigned odst) bytes; + Some(w, E0, Vundef, m') + else None + | _ => None + end. + +Definition do_ef_annot (text: ident) (targs: list typ) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + do args <- list_eventval_of_val vargs targs; + Some(w, Event_annot text args :: E0, Vundef, m). + +Definition do_ef_annot_val (text: ident) (targ: typ) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match vargs with + | varg :: nil => + do arg <- eventval_of_val varg targ; + Some(w, Event_annot text (arg :: nil) :: E0, varg, m) + | _ => None + end. + +Definition do_external (ef: external_function): + world -> list val -> mem -> option (world * trace * val * mem) := + match ef with + | EF_external name sg => do_ef_external name sg + | EF_builtin name sg => do_ef_external name sg + | EF_vload chunk => do_ef_volatile_load chunk + | EF_vstore chunk => do_ef_volatile_store chunk + | EF_vload_global chunk id ofs => do_ef_volatile_load_global chunk id ofs + | EF_vstore_global chunk id ofs => do_ef_volatile_store_global chunk id ofs + | EF_malloc => do_ef_malloc + | EF_free => do_ef_free + | EF_memcpy sz al => do_ef_memcpy sz al + | EF_annot text targs => do_ef_annot text targs + | EF_annot_val text targ => do_ef_annot_val text targ + end. + +Lemma do_ef_external_sound: + forall ef w vargs m w' t vres m', + do_external ef w vargs m = Some(w', t, vres, m') -> + external_call ef ge vargs m t vres m' /\ possible_trace w t w'. +Proof with try congruence. + intros until m'. + assert (IO: forall name sg, + do_ef_external name sg w vargs m = Some(w', t, vres, m') -> + extcall_io_sem name sg ge vargs m t vres m' /\ possible_trace w t w'). + intros until sg. unfold do_ef_external. mydestr. destruct p as [res w'']; mydestr. + split. econstructor. apply list_eventval_of_val_sound; auto. + apply val_of_eventval_sound; auto. + econstructor. constructor; eauto. constructor. + + assert (VLOAD: forall chunk vargs, + do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m') -> + volatile_load_sem chunk ge vargs m t vres m' /\ possible_trace w t w'). + intros chunk vargs'. + unfold do_ef_volatile_load. destruct vargs'... destruct v... destruct vargs'... + mydestr. destruct p as [[w'' t''] v]; mydestr. + exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto. + + assert (VSTORE: forall chunk vargs, + do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m') -> + volatile_store_sem chunk ge vargs m t vres m' /\ possible_trace w t w'). + intros chunk vargs'. + unfold do_ef_volatile_store. destruct vargs'... destruct v... destruct vargs'... destruct vargs'... + mydestr. destruct p as [[w'' t''] m'']. mydestr. + exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto. + + destruct ef; simpl. +(* EF_external *) + auto. +(* EF_builtin *) + auto. +(* EF_vload *) + auto. +(* EF_vstore *) + auto. +(* EF_vload_global *) + rewrite volatile_load_global_charact. + unfold do_ef_volatile_load_global. destruct (Genv.find_symbol ge)... + intros. exploit VLOAD; eauto. intros [A B]. split; auto. exists b; auto. +(* EF_vstore_global *) + rewrite volatile_store_global_charact. + unfold do_ef_volatile_store_global. destruct (Genv.find_symbol ge)... + intros. exploit VSTORE; eauto. intros [A B]. split; auto. exists b; auto. +(* EF_malloc *) + unfold do_ef_malloc. destruct vargs... destruct v... destruct vargs... + destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b]_eqn. mydestr. + split. econstructor; eauto. constructor. +(* EF_free *) + unfold do_ef_free. destruct vargs... destruct v... destruct vargs... + mydestr. destruct v... mydestr. + split. econstructor; eauto. omega. constructor. +(* EF_memcpy *) + unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... + destruct v... destruct vargs... mydestr. red in m0. + split. econstructor; eauto; tauto. constructor. +(* EF_annot *) + unfold do_ef_annot. mydestr. + split. constructor. apply list_eventval_of_val_sound; auto. + econstructor. constructor; eauto. constructor. +(* EF_annot_val *) + unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr. + split. constructor. apply eventval_of_val_sound; auto. + econstructor. constructor; eauto. constructor. +Qed. + +Lemma do_ef_external_complete: + forall ef w vargs m w' t vres m', + external_call ef ge vargs m t vres m' -> possible_trace w t w' -> + do_external ef w vargs m = Some(w', t, vres, m'). +Proof. + intros. + assert (IO: forall name sg, + extcall_io_sem name sg ge vargs m t vres m' -> + do_ef_external name sg w vargs m = Some (w', t, vres, m')). + intros. inv H1. inv H0. inv H8. inv H6. + unfold do_ef_external. rewrite (list_eventval_of_val_complete _ _ _ H2). rewrite H8. + rewrite (val_of_eventval_complete _ _ _ H3). auto. + + assert (VLOAD: forall chunk vargs, + volatile_load_sem chunk ge vargs m t vres m' -> + do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m')). + intros. inv H1; unfold do_ef_volatile_load. + exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto. + + assert (VSTORE: forall chunk vargs, + volatile_store_sem chunk ge vargs m t vres m' -> + do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m')). + intros. inv H1; unfold do_ef_volatile_store. + exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto. + + destruct ef; simpl in *. +(* EF_external *) + auto. +(* EF_builtin *) + auto. +(* EF_vload *) + auto. +(* EF_vstore *) + auto. +(* EF_vload_global *) + rewrite volatile_load_global_charact in H. destruct H as [b [P Q]]. + unfold do_ef_volatile_load_global. rewrite P. auto. +(* EF_vstore *) + rewrite volatile_store_global_charact in H. destruct H as [b [P Q]]. + unfold do_ef_volatile_store_global. rewrite P. auto. +(* EF_malloc *) + inv H; unfold do_ef_malloc. + inv H0. rewrite H1. rewrite H2. auto. +(* EF_free *) + inv H; unfold do_ef_free. + inv H0. rewrite H1. rewrite zlt_true. rewrite H3. auto. omega. +(* EF_memcpy *) + inv H; unfold do_ef_memcpy. + inv H0. rewrite pred_dec_true. rewrite H7; rewrite H8; auto. + red. tauto. +(* EF_annot *) + inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. + rewrite (list_eventval_of_val_complete _ _ _ H1). auto. +(* EF_annot_val *) + inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. + rewrite (eventval_of_val_complete _ _ _ H1). auto. +Qed. + +(** * Reduction of expressions *) + +Inductive reduction: Type := + | Lred (l': expr) (m': mem) + | Rred (r': expr) (m': mem) (t: trace) + | Callred (fd: fundef) (args: list val) (tyres: type) (m': mem) + | Stuckred. + +Section EXPRS. + +Variable e: env. +Variable w: world. + +Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) : option (list val) := + match vtl, tl with + | nil, Tnil => Some nil + | (v1,t1)::vtl, Tcons t1' tl => + do v <- sem_cast v1 t1 t1'; do vl <- sem_cast_arguments vtl tl; Some(v::vl) + | _, _ => None + end. + +(** The result of stepping an expression is a list [ll] of possible reducts. + Each element of [ll] is a pair of a context and the result of reducing + inside this context (see type [reduction] above). + The list [ll] is empty if the expression is fully reduced + (it's [Eval] for a r-value and [Eloc] for a l-value). +*) + +Definition reducts (A: Type): Type := list ((expr -> A) * reduction). + +Definition topred (r: reduction) : reducts expr := + ((fun (x: expr) => x), r) :: nil. + +Definition stuck : reducts expr := + ((fun (x: expr) => x), Stuckred) :: nil. + +Definition incontext {A B: Type} (ctx: A -> B) (ll: reducts A) : reducts B := + map (fun z => ((fun (x: expr) => ctx(fst z x)), snd z)) ll. + +Definition incontext2 {A1 A2 B: Type} + (ctx1: A1 -> B) (ll1: reducts A1) + (ctx2: A2 -> B) (ll2: reducts A2) : reducts B := + incontext ctx1 ll1 ++ incontext ctx2 ll2. + +Notation "'do' X <- A ; B" := (match A with Some X => B | None => stuck end) + (at level 200, X ident, A at level 100, B at level 200) + : reducts_monad_scope. + +Notation "'do' X , Y <- A ; B" := (match A with Some (X, Y) => B | None => stuck end) + (at level 200, X ident, Y ident, A at level 100, B at level 200) + : reducts_monad_scope. + +Notation "'do' X , Y , Z <- A ; B" := (match A with Some (X, Y, Z) => B | None => stuck end) + (at level 200, X ident, Y ident, Z ident, A at level 100, B at level 200) + : reducts_monad_scope. + +Notation " 'check' A ; B" := (if A then B else stuck) + (at level 200, A at level 100, B at level 200) + : reducts_monad_scope. + +Local Open Scope reducts_monad_scope. + +Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := + match k, a with + | LV, Eloc b ofs ty => + nil + | LV, Evar x ty => + match e!x with + | Some(b, ty') => + check type_eq ty ty'; + topred (Lred (Eloc b Int.zero ty) m) + | None => + do b <- Genv.find_symbol ge x; + do ty' <- type_of_global ge b; + check type_eq ty ty'; + topred (Lred (Eloc b Int.zero ty) m) + end + | LV, Ederef r ty => + match is_val r with + | Some(Vptr b ofs, ty') => + topred (Lred (Eloc b ofs ty) m) + | Some _ => + stuck + | None => + incontext (fun x => Ederef x ty) (step_expr RV r m) + end + | LV, Efield r f ty => + match is_val r with + | Some(Vptr b ofs, ty') => + match ty' with + | Tstruct id fList _ => + match field_offset f fList with + | Error _ => stuck + | OK delta => topred (Lred (Eloc b (Int.add ofs (Int.repr delta)) ty) m) + end + | Tunion id fList _ => + topred (Lred (Eloc b ofs ty) m) + | _ => stuck + end + | Some _ => + stuck + | None => + incontext (fun x => Efield x f ty) (step_expr RV r m) + end + | RV, Eval v ty => + nil + | RV, Evalof l ty => + match is_loc l with + | Some(b, ofs, ty') => + check type_eq ty ty'; + do w',t,v <- do_deref_loc w ty m b ofs; + topred (Rred (Eval v ty) m t) + | None => + incontext (fun x => Evalof x ty) (step_expr LV l m) + end + | RV, Eaddrof l ty => + match is_loc l with + | Some(b, ofs, ty') => topred (Rred (Eval (Vptr b ofs) ty) m E0) + | None => incontext (fun x => Eaddrof x ty) (step_expr LV l m) + end + | RV, Eunop op r1 ty => + match is_val r1 with + | Some(v1, ty1) => + do v <- sem_unary_operation op v1 ty1; + topred (Rred (Eval v ty) m E0) + | None => + incontext (fun x => Eunop op x ty) (step_expr RV r1 m) + end + | RV, Ebinop op r1 r2 ty => + match is_val r1, is_val r2 with + | Some(v1, ty1), Some(v2, ty2) => + do v <- sem_binary_operation op v1 ty1 v2 ty2 m; + topred (Rred (Eval v ty) m E0) + | _, _ => + incontext2 (fun x => Ebinop op x r2 ty) (step_expr RV r1 m) + (fun x => Ebinop op r1 x ty) (step_expr RV r2 m) + end + | RV, Ecast r1 ty => + match is_val r1 with + | Some(v1, ty1) => + do v <- sem_cast v1 ty1 ty; + topred (Rred (Eval v ty) m E0) + | None => + incontext (fun x => Ecast x ty) (step_expr RV r1 m) + end + | RV, Econdition r1 r2 r3 ty => + match is_val r1 with + | Some(v1, ty1) => + do b <- bool_val v1 ty1; + topred (Rred (Eparen (if b then r2 else r3) ty) m E0) + | None => + incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m) + end + | RV, Esizeof ty' ty => + topred (Rred (Eval (Vint (Int.repr (sizeof ty'))) ty) m E0) + | RV, Eassign l1 r2 ty => + match is_loc l1, is_val r2 with + | Some(b, ofs, ty1), Some(v2, ty2) => + check type_eq ty1 ty; + do v <- sem_cast v2 ty2 ty1; + do w',t,m' <- do_assign_loc w ty1 m b ofs v; + topred (Rred (Eval v ty) m' t) + | _, _ => + incontext2 (fun x => Eassign x r2 ty) (step_expr LV l1 m) + (fun x => Eassign l1 x ty) (step_expr RV r2 m) + end + | RV, Eassignop op l1 r2 tyres ty => + match is_loc l1, is_val r2 with + | Some(b, ofs, ty1), Some(v2, ty2) => + check type_eq ty1 ty; + do w',t,v1 <- do_deref_loc w ty1 m b ofs; + let r' := Eassign (Eloc b ofs ty1) + (Ebinop op (Eval v1 ty1) (Eval v2 ty2) tyres) ty1 in + topred (Rred r' m t) + | _, _ => + incontext2 (fun x => Eassignop op x r2 tyres ty) (step_expr LV l1 m) + (fun x => Eassignop op l1 x tyres ty) (step_expr RV r2 m) + end + | RV, Epostincr id l ty => + match is_loc l with + | Some(b, ofs, ty1) => + check type_eq ty1 ty; + do w',t, v1 <- do_deref_loc w ty m b ofs; + let op := match id with Incr => Oadd | Decr => Osub end in + let r' := + Ecomma (Eassign (Eloc b ofs ty) + (Ebinop op (Eval v1 ty) (Eval (Vint Int.one) type_int32s) (typeconv ty)) + ty) + (Eval v1 ty) ty in + topred (Rred r' m t) + | None => + incontext (fun x => Epostincr id x ty) (step_expr LV l m) + end + | RV, Ecomma r1 r2 ty => + match is_val r1 with + | Some _ => + check type_eq (typeof r2) ty; + topred (Rred r2 m E0) + | None => + incontext (fun x => Ecomma x r2 ty) (step_expr RV r1 m) + end + | RV, Eparen r1 ty => + match is_val r1 with + | Some (v1, ty1) => + do v <- sem_cast v1 ty1 ty; + topred (Rred (Eval v ty) m E0) + | None => + incontext (fun x => Eparen x ty) (step_expr RV r1 m) + end + | RV, Ecall r1 rargs ty => + match is_val r1, is_val_list rargs with + | Some(vf, tyf), Some vtl => + match classify_fun tyf with + | fun_case_f tyargs tyres => + do fd <- Genv.find_funct ge vf; + do vargs <- sem_cast_arguments vtl tyargs; + check type_eq (type_of_fundef fd) (Tfunction tyargs tyres); + topred (Callred fd vargs ty m) + | _ => stuck + end + | _, _ => + incontext2 (fun x => Ecall x rargs ty) (step_expr RV r1 m) + (fun x => Ecall r1 x ty) (step_exprlist rargs m) + end + | _, _ => stuck + end + +with step_exprlist (rl: exprlist) (m: mem): reducts exprlist := + match rl with + | Enil => + nil + | Econs r1 rs => + incontext2 (fun x => Econs x rs) (step_expr RV r1 m) + (fun x => Econs r1 x) (step_exprlist rs m) + end. + +(** Technical properties on safe expressions. *) + +Inductive imm_safe_t: kind -> expr -> mem -> Prop := + | imm_safe_t_val: forall v ty m, + imm_safe_t RV (Eval v ty) m + | imm_safe_t_loc: forall b ofs ty m, + imm_safe_t LV (Eloc b ofs ty) m + | imm_safe_t_lred: forall to C l m l' m', + lred ge e l m l' m' -> + context LV to C -> + imm_safe_t to (C l) m + | imm_safe_t_rred: forall to C r m t r' m' w', + rred ge r m t r' m' -> possible_trace w t w' -> + context RV to C -> + imm_safe_t to (C r) m + | imm_safe_t_callred: forall to C r m fd args ty, + callred ge r fd args ty -> + context RV to C -> + imm_safe_t to (C r) m. + +Remark imm_safe_t_imm_safe: + forall k a m, imm_safe_t k a m -> imm_safe ge e k a m. +Proof. + induction 1. + constructor. + constructor. + eapply imm_safe_lred; eauto. + eapply imm_safe_rred; eauto. + eapply imm_safe_callred; eauto. +Qed. + +(* +Definition not_stuck (a: expr) (m: mem) := + forall a' k C, context k RV C -> a = C a' -> imm_safe_t k a' m. + +Lemma safe_expr_kind: + forall k C a m, + context k RV C -> + not_stuck (C a) m -> + k = Cstrategy.expr_kind a. +Proof. + intros. + symmetry. eapply Cstrategy.imm_safe_kind. eapply imm_safe_t_imm_safe. eauto. +Qed. +*) + +Fixpoint exprlist_all_values (rl: exprlist) : Prop := + match rl with + | Enil => True + | Econs (Eval v ty) rl' => exprlist_all_values rl' + | Econs _ _ => False + end. + +Definition invert_expr_prop (a: expr) (m: mem) : Prop := + match a with + | Eloc b ofs ty => False + | Evar x ty => + exists b, + e!x = Some(b, ty) + \/ (e!x = None /\ Genv.find_symbol ge x = Some b /\ type_of_global ge b = Some ty) + | Ederef (Eval v ty1) ty => + exists b, exists ofs, v = Vptr b ofs + | Efield (Eval v ty1) f ty => + exists b, exists ofs, v = Vptr b ofs /\ + match ty1 with + | Tstruct _ fList _ => exists delta, field_offset f fList = Errors.OK delta + | Tunion _ _ _ => True + | _ => False + end + | Eval v ty => False + | Evalof (Eloc b ofs ty') ty => + ty' = ty /\ exists t, exists v, exists w', deref_loc ge ty m b ofs t v /\ possible_trace w t w' + | Eunop op (Eval v1 ty1) ty => + exists v, sem_unary_operation op v1 ty1 = Some v + | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => + exists v, sem_binary_operation op v1 ty1 v2 ty2 m = Some v + | Ecast (Eval v1 ty1) ty => + exists v, sem_cast v1 ty1 ty = Some v + | Econdition (Eval v1 ty1) r1 r2 ty => + exists b, bool_val v1 ty1 = Some b + | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty => + exists v, exists m', exists t, exists w', + ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m' /\ possible_trace w t w' + | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty => + exists t, exists v1, exists w', + ty = ty1 /\ deref_loc ge ty1 m b ofs t v1 /\ possible_trace w t w' + | Epostincr id (Eloc b ofs ty1) ty => + exists t, exists v1, exists w', + ty = ty1 /\ deref_loc ge ty m b ofs t v1 /\ possible_trace w t w' + | Ecomma (Eval v ty1) r2 ty => + typeof r2 = ty + | Eparen (Eval v1 ty1) ty => + exists v, sem_cast v1 ty1 ty = Some v + | Ecall (Eval vf tyf) rargs ty => + exprlist_all_values rargs -> + exists tyargs, exists tyres, exists fd, exists vl, + classify_fun tyf = fun_case_f tyargs tyres + /\ Genv.find_funct ge vf = Some fd + /\ cast_arguments rargs tyargs vl + /\ type_of_fundef fd = Tfunction tyargs tyres + | _ => True + end. + +Lemma lred_invert: + forall l m l' m', lred ge e l m l' m' -> invert_expr_prop l m. +Proof. + induction 1; red; auto. + exists b; auto. + exists b; auto. + exists b; exists ofs; auto. + exists b; exists ofs; split; auto. exists delta; auto. + exists b; exists ofs; auto. +Qed. + +Lemma rred_invert: + forall w' r m t r' m', rred ge r m t r' m' -> possible_trace w t w' -> invert_expr_prop r m. +Proof. + induction 1; intros; red; auto. + split; auto; exists t; exists v; exists w'; auto. + exists v; auto. + exists v; auto. + exists v; auto. + exists b; auto. + exists v; exists m'; exists t; exists w'; auto. + exists t; exists v1; exists w'; auto. + exists t; exists v1; exists w'; auto. + exists v; auto. +Qed. + +Lemma callred_invert: + forall r fd args ty m, + callred ge r fd args ty -> + invert_expr_prop r m. +Proof. + intros. inv H. simpl. + intros. exists tyargs; exists tyres; exists fd; exists args; auto. +Qed. + +Scheme context_ind2 := Minimality for context Sort Prop + with contextlist_ind2 := Minimality for contextlist Sort Prop. +Combined Scheme context_contextlist_ind from context_ind2, contextlist_ind2. + +Lemma invert_expr_context: + (forall from to C, context from to C -> + forall a m, + invert_expr_prop a m -> + invert_expr_prop (C a) m) +/\(forall from C, contextlist from C -> + forall a m, + invert_expr_prop a m -> + ~exprlist_all_values (C a)). +Proof. + apply context_contextlist_ind; intros; try (exploit H0; [eauto|intros]); simpl. + auto. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + auto. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct e1; auto; destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct e1; auto; destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct e1; auto; destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct e1; auto. intros. elim (H0 a m); auto. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + red; intros. destruct (C a); auto. + red; intros. destruct e1; auto. elim (H0 a m); auto. +Qed. + +Lemma imm_safe_t_inv: + forall k a m, + imm_safe_t k a m -> + match a with + | Eloc _ _ _ => True + | Eval _ _ => True + | _ => invert_expr_prop a m + end. +Proof. + destruct invert_expr_context as [A B]. + intros. inv H. + auto. + auto. + assert (invert_expr_prop (C l) m). + eapply A; eauto. eapply lred_invert; eauto. + red in H. destruct (C l); auto; contradiction. + assert (invert_expr_prop (C r) m). + eapply A; eauto. eapply rred_invert; eauto. + red in H. destruct (C r); auto; contradiction. + assert (invert_expr_prop (C r) m). + eapply A; eauto. eapply callred_invert; eauto. + red in H. destruct (C r); auto; contradiction. +Qed. + +(** Soundness: if [step_expr] returns [Some ll], then every element + of [ll] is a reduct. *) + +Lemma context_compose: + forall k2 k3 C2, context k2 k3 C2 -> + forall k1 C1, context k1 k2 C1 -> + context k1 k3 (fun x => C2(C1 x)) +with contextlist_compose: + forall k2 C2, contextlist k2 C2 -> + forall k1 C1, context k1 k2 C1 -> + contextlist k1 (fun x => C2(C1 x)). +Proof. + induction 1; intros; try (constructor; eauto). + replace (fun x => C1 x) with C1. auto. apply extensionality; auto. + induction 1; intros; constructor; eauto. +Qed. + +Hint Constructors context contextlist. +Hint Resolve context_compose contextlist_compose. + +Definition reduction_ok (k: kind) (a: expr) (m: mem) (rd: reduction) : Prop := + match k, rd with + | LV, Lred l' m' => lred ge e a m l' m' + | RV, Rred r' m' t => rred ge a m t r' m' /\ exists w', possible_trace w t w' + | RV, Callred fd args tyres m' => callred ge a fd args tyres /\ m' = m + | LV, Stuckred => ~imm_safe_t k a m + | RV, Stuckred => ~imm_safe_t k a m + | _, _ => False + end. + +Definition reducts_ok (k: kind) (a: expr) (m: mem) (ll: reducts expr) : Prop := + (forall C rd, + In (C, rd) ll -> + exists a', exists k', context k' k C /\ a = C a' /\ reduction_ok k' a' m rd) + /\ (ll = nil -> match k with LV => is_loc a <> None | RV => is_val a <> None end). + +Definition list_reducts_ok (al: exprlist) (m: mem) (ll: reducts exprlist) : Prop := + (forall C rd, In (C, rd) ll -> - contextlist (reduction_kind rd) C /\ exists a', al = C a' /\ reduction_ok a' m rd + exists a', exists k', contextlist k' C /\ al = C a' /\ reduction_ok k' a' m rd) + /\ (ll = nil -> is_val_list al <> None). + +Ltac monadInv := + match goal with + | [ H: match ?x with Some _ => _ | None => None end = Some ?y |- _ ] => + destruct x as []_eqn; [monadInv|discriminate] + | [ H: match ?x with left _ => _ | right _ => None end = Some ?y |- _ ] => + destruct x; [monadInv|discriminate] + | _ => idtac end. +Lemma sem_cast_arguments_sound: + forall rargs vtl tyargs vargs, + is_val_list rargs = Some vtl -> + sem_cast_arguments vtl tyargs = Some vargs -> + cast_arguments rargs tyargs vargs. +Proof. + induction rargs; simpl; intros. + inv H. destruct tyargs; simpl in H0; inv H0. constructor. + monadInv. inv H. simpl in H0. destruct p as [v1 t1]. destruct tyargs; try congruence. monadInv. + inv H0. rewrite (is_val_inv _ _ _ Heqo). constructor. auto. eauto. +Qed. + +Lemma sem_cast_arguments_complete: + forall al tyl vl, + cast_arguments al tyl vl -> + exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl = Some vl. +Proof. + induction 1. + exists (@nil (val * type)); auto. + destruct IHcast_arguments as [vtl [A B]]. + exists ((v, ty) :: vtl); simpl. rewrite A; rewrite B; rewrite H. auto. +Qed. + Lemma topred_ok: forall k a m rd, - reduction_ok a m rd -> - k = reduction_kind rd -> + reduction_ok k a m rd -> reducts_ok k a m (topred rd). Proof. - intros. unfold topred; red. simpl; intros. destruct H1; try contradiction. - inv H1. split. auto. exists a; auto. + intros. unfold topred; split; simpl; intros. + destruct H0; try contradiction. inv H0. exists a; exists k; auto. + congruence. +Qed. + +Lemma stuck_ok: + forall k a m, + ~imm_safe_t k a m -> + reducts_ok k a m stuck. +Proof. + intros. unfold stuck; split; simpl; intros. + destruct H0; try contradiction. inv H0. exists a; exists k; intuition. red. destruct k; auto. + congruence. +Qed. + +Lemma wrong_kind_ok: + forall k a m, + k <> Cstrategy.expr_kind a -> + reducts_ok k a m stuck. +Proof. + intros. apply stuck_ok. red; intros. exploit Cstrategy.imm_safe_kind; eauto. + eapply imm_safe_t_imm_safe; eauto. Qed. +Lemma not_invert_ok: + forall k a m, + match a with + | Eloc _ _ _ => False + | Eval _ _ => False + | _ => invert_expr_prop a m -> False + end -> + reducts_ok k a m stuck. +Proof. + intros. apply stuck_ok. red; intros. + exploit imm_safe_t_inv; eauto. destruct a; auto. +Qed. + Lemma incontext_ok: forall k a m C res k' a', reducts_ok k' a' m res -> @@ -416,48 +1192,11 @@ Lemma incontext_ok: match k' with LV => is_loc a' = None | RV => is_val a' = None end -> reducts_ok k a m (incontext C res). Proof. - unfold reducts_ok; intros. destruct res; simpl. destruct l. -(* res = Some nil *) - destruct k'; congruence. -(* res = Some nonempty-list *) - simpl map at 1. hnf. intros. + unfold reducts_ok, incontext; intros. destruct H. split; intros. exploit list_in_map_inv; eauto. intros [[C1 rd1] [P Q]]. inv P. - exploit H; eauto. intros [U [a'' [V W]]]. - split. eapply context_compose; eauto. exists a''; split; auto. congruence. -(* res = None *) - auto. -Qed. - -Remark incontext2_inv: - forall {A1 A2 B: Type} (C1: A1 -> B) res1 (C2: A2 -> B) res2, - match incontext2 C1 res1 C2 res2 with - | None => res1 = None \/ res2 = None - | Some nil => res1 = Some nil /\ res2 = Some nil - | Some ll => - exists ll1, exists ll2, - res1 = Some ll1 /\ res2 = Some ll2 /\ - forall C rd, In (C, rd) ll -> - (exists C', C = (fun x => C1(C' x)) /\ In (C', rd) ll1) - \/ (exists C', C = (fun x => C2(C' x)) /\ In (C', rd) ll2) - end. -Proof. - intros. unfold incontext2. destruct res1 as [ll1|]; auto. destruct res2 as [ll2|]; auto. - set (ll := map - (fun z : (expr -> A1) * reduction => - (fun x : expr => C1 (fst z x), snd z)) ll1 ++ - map - (fun z : (expr -> A2) * reduction => - (fun x : expr => C2 (fst z x), snd z)) ll2). - destruct ll as []_eqn. - destruct (app_eq_nil _ _ Heql). - split. destruct ll1; auto || discriminate. destruct ll2; auto || discriminate. - rewrite <- Heql. exists ll1; exists ll2. split. auto. split. auto. - unfold ll; intros. - rewrite in_app in H. destruct H. - exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P. - left; exists C'; auto. - exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P. - right; exists C'; auto. + exploit H; eauto. intros [a'' [k'' [U [V W]]]]. + exists a''; exists k''. split. eapply context_compose; eauto. rewrite V; auto. + destruct res; simpl in H4; try congruence. destruct k'; intuition congruence. Qed. Lemma incontext2_ok: @@ -470,17 +1209,16 @@ Lemma incontext2_ok: \/ match k2 with LV => is_loc a2 = None | RV => is_val a2 = None end -> reducts_ok k a m (incontext2 C1 res1 C2 res2). Proof. - unfold reducts_ok; intros. - generalize (incontext2_inv C1 res1 C2 res2). - destruct (incontext2 C1 res1 C2 res2) as [ll|]; auto. - destruct ll. - intros [EQ1 EQ2]. subst. destruct H5. destruct k1; congruence. destruct k2; congruence. - intros [ll1 [ll2 [EQ1 [EQ2 IN]]]]. subst. intros. - exploit IN; eauto. intros [[C' [P Q]] | [C' [P Q]]]; subst. - destruct ll1; try contradiction. exploit H; eauto. - intros [U [a' [V W]]]. split. eauto. exists a'; split. congruence. auto. - destruct ll2; try contradiction. exploit H0; eauto. - intros [U [a' [V W]]]. split. eauto. exists a'; split. congruence. auto. + unfold reducts_ok, incontext2, incontext; intros. destruct H; destruct H0; split; intros. + destruct (in_app_or _ _ _ H8). + exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P. + exploit H; eauto. intros [a'' [k'' [U [V W]]]]. + exists a''; exists k''. split. eapply context_compose; eauto. rewrite V; auto. + exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P. + exploit H0; eauto. intros [a'' [k'' [U [V W]]]]. + exists a''; exists k''. split. eapply context_compose; eauto. rewrite H2; rewrite V; auto. + destruct res1; simpl in H8; try congruence. destruct res2; simpl in H8; try congruence. + destruct H5. destruct k1; intuition congruence. destruct k2; intuition congruence. Qed. Lemma incontext2_list_ok: @@ -492,18 +1230,16 @@ Lemma incontext2_list_ok: (incontext2 (fun x => Ecall x a2 ty) res1 (fun x => Ecall a1 x ty) res2). Proof. - unfold reducts_ok, list_reducts_ok; intros. - set (C1 := fun x => Ecall x a2 ty). set (C2 := fun x => Ecall a1 x ty). - generalize (incontext2_inv C1 res1 C2 res2). - destruct (incontext2 C1 res1 C2 res2) as [ll|]; auto. - destruct ll. - intros [EQ1 EQ2]. subst. intuition congruence. - intros [ll1 [ll2 [EQ1 [EQ2 IN]]]]. subst. intros. - exploit IN; eauto. intros [[C' [P Q]] | [C' [P Q]]]; subst. - destruct ll1; try contradiction. exploit H; eauto. - intros [U [a' [V W]]]. split. unfold C1. auto. exists a'; split. unfold C1; congruence. auto. - destruct ll2; try contradiction. exploit H0; eauto. - intros [U [a' [V W]]]. split. unfold C2. auto. exists a'; split. unfold C2; congruence. auto. + unfold reducts_ok, incontext2, incontext; intros. destruct H; destruct H0; split; intros. + destruct (in_app_or _ _ _ H4). + exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P. + exploit H; eauto. intros [a'' [k'' [U [V W]]]]. + exists a''; exists k''. split. eauto. rewrite V; auto. + exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P. + exploit H0; eauto. intros [a'' [k'' [U [V W]]]]. + exists a''; exists k''. split. eauto. rewrite V; auto. + destruct res1; simpl in H4; try congruence. destruct res2; simpl in H4; try congruence. + tauto. Qed. Lemma incontext2_list_ok': @@ -514,1023 +1250,500 @@ Lemma incontext2_list_ok': (incontext2 (fun x => Econs x a2) res1 (fun x => Econs a1 x) res2). Proof. - unfold reducts_ok, list_reducts_ok; intros. - set (C1 := fun x => Econs x a2). set (C2 := fun x => Econs a1 x). - generalize (incontext2_inv C1 res1 C2 res2). - destruct (incontext2 C1 res1 C2 res2) as [ll|]; auto. - destruct ll. - intros [EQ1 EQ2]. subst. - simpl. destruct (is_val a1); try congruence. destruct (is_val_list a2); congruence. - intros [ll1 [ll2 [EQ1 [EQ2 IN]]]]. subst. intros. - exploit IN; eauto. intros [[C' [P Q]] | [C' [P Q]]]; subst. - destruct ll1; try contradiction. exploit H; eauto. - intros [U [a' [V W]]]. split. unfold C1. auto. exists a'; split. unfold C1; congruence. auto. - destruct ll2; try contradiction. exploit H0; eauto. - intros [U [a' [V W]]]. split. unfold C2. auto. exists a'; split. unfold C2; congruence. auto. -Qed. - -Ltac mysimpl := + unfold reducts_ok, list_reducts_ok, incontext2, incontext; intros. + destruct H; destruct H0. split; intros. + destruct (in_app_or _ _ _ H3). + exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P. + exploit H; eauto. intros [a'' [k'' [U [V W]]]]. + exists a''; exists k''. split. eauto. rewrite V; auto. + exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P. + exploit H0; eauto. intros [a'' [k'' [U [V W]]]]. + exists a''; exists k''. split. eauto. rewrite V; auto. + destruct res1; simpl in H3; try congruence. destruct res2; simpl in H3; try congruence. + simpl. destruct (is_val a1). destruct (is_val_list a2). congruence. intuition congruence. intuition congruence. +Qed. + +Lemma is_val_list_all_values: + forall al vtl, is_val_list al = Some vtl -> exprlist_all_values al. +Proof. + induction al; simpl; intros. auto. + destruct (is_val r1) as [[v ty]|]_eqn; try discriminate. + destruct (is_val_list al) as [vtl'|]_eqn; try discriminate. + rewrite (is_val_inv _ _ _ Heqo). eauto. +Qed. + +Ltac myinv := match goal with - | [ |- reducts_ok _ _ _ (match ?x with Some _ => _ | None => None end) ] => - destruct x as []_eqn; [mysimpl|exact I] - | [ |- reducts_ok _ _ _ (match ?x with left _ => _ | right _ => None end) ] => - destruct x as []_eqn; [subst;mysimpl|exact I] - | _ => - idtac + | [ H: False |- _ ] => destruct H + | [ H: _ /\ _ |- _ ] => destruct H; myinv + | [ H: exists _, _ |- _ ] => destruct H; myinv + | _ => idtac end. Theorem step_expr_sound: forall a k m, reducts_ok k a m (step_expr k a m) with step_exprlist_sound: forall al m, list_reducts_ok al m (step_exprlist al m). -Proof with try (exact I). - induction a; destruct k; intros; simpl... +Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; fail)). + induction a; intros; simpl; destruct k; try (apply wrong_kind_ok; simpl; congruence). (* Eval *) - congruence. + split; intros. tauto. simpl; congruence. (* Evar *) - destruct (e!x) as [[b ty'] | ]_eqn; mysimpl. - apply topred_ok; auto. apply red_var_local; auto. - apply topred_ok; auto. apply red_var_global; auto. + destruct (e!x) as [[b ty']|]_eqn. + destruct (type_eq ty ty')... + subst. apply topred_ok; auto. apply red_var_local; auto. + destruct (Genv.find_symbol ge x) as [b|]_eqn... + destruct (type_of_global ge b) as [ty'|]_eqn... + destruct (type_eq ty ty')... + subst. apply topred_ok; auto. apply red_var_global; auto. (* Efield *) - destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. + destruct (is_val a) as [[v ty'] | ]_eqn. + rewrite (is_val_inv _ _ _ Heqo). + destruct v... destruct ty'... (* top struct *) destruct (field_offset f f0) as [delta|]_eqn... - rewrite (is_loc_inv _ _ _ _ Heqo). apply topred_ok; auto. apply red_field_struct; auto. + apply topred_ok; auto. apply red_field_struct; auto. (* top union *) - rewrite (is_loc_inv _ _ _ _ Heqo). apply topred_ok; auto. apply red_field_union; auto. + apply topred_ok; auto. apply red_field_union; auto. (* in depth *) eapply incontext_ok; eauto. (* Evalof *) - destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. + destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. rewrite (is_loc_inv _ _ _ _ Heqo). (* top *) - mysimpl. apply topred_ok; auto. rewrite (is_loc_inv _ _ _ _ Heqo). apply red_rvalof; auto. + destruct (type_eq ty ty')... subst ty'. + destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ]_eqn. + exploit do_deref_loc_sound; eauto. intros [A B]. + apply topred_ok; auto. red. split. apply red_rvalof; auto. exists w'; auto. + apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. congruence. (* depth *) eapply incontext_ok; eauto. (* Ederef *) - destruct (is_val a) as [[v ty'] | ]_eqn. + destruct (is_val a) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct v... mysimpl. apply topred_ok; auto. rewrite (is_val_inv _ _ _ Heqo). apply red_deref; auto. + destruct v... apply topred_ok; auto. apply red_deref; auto. (* depth *) eapply incontext_ok; eauto. (* Eaddrof *) - destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. + destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. rewrite (is_loc_inv _ _ _ _ Heqo). (* top *) - apply topred_ok; auto. rewrite (is_loc_inv _ _ _ _ Heqo). apply red_addrof; auto. + apply topred_ok; auto. split. apply red_addrof; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. (* unop *) - destruct (is_val a) as [[v ty'] | ]_eqn. + destruct (is_val a) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). (* top *) - mysimpl. apply topred_ok; auto. rewrite (is_val_inv _ _ _ Heqo). apply red_unop; auto. + destruct (sem_unary_operation op v ty') as [v'|]_eqn... + apply topred_ok; auto. split. apply red_unop; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. (* binop *) - destruct (is_val a1) as [[v1 ty1] | ]_eqn. + destruct (is_val a1) as [[v1 ty1] | ]_eqn. destruct (is_val a2) as [[v2 ty2] | ]_eqn. + rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). (* top *) - mysimpl. apply topred_ok; auto. - rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). apply red_binop; auto. + destruct (sem_binary_operation op v1 ty1 v2 ty2 m) as [v|]_eqn... + apply topred_ok; auto. split. apply red_binop; auto. exists w; constructor. (* depth *) eapply incontext2_ok; eauto. eapply incontext2_ok; eauto. (* cast *) - destruct (is_val a) as [[v ty'] | ]_eqn. + destruct (is_val a) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). (* top *) - mysimpl. apply topred_ok; auto. - rewrite (is_val_inv _ _ _ Heqo). apply red_cast; auto. + destruct (sem_cast v ty' ty) as [v'|]_eqn... + apply topred_ok; auto. split. apply red_cast; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. (* condition *) - destruct (is_val a1) as [[v ty'] | ]_eqn. + destruct (is_val a1) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). (* top *) - mysimpl. apply topred_ok; auto. - rewrite (is_val_inv _ _ _ Heqo). eapply red_condition; eauto. + destruct (bool_val v ty') as [v'|]_eqn... + apply topred_ok; auto. split. eapply red_condition; eauto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. (* sizeof *) - apply topred_ok; auto. apply red_sizeof. + apply topred_ok; auto. split. apply red_sizeof. exists w; constructor. (* assign *) - destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn. - destruct (is_val a2) as [[v2 ty2] | ]_eqn. + destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn. + destruct (is_val a2) as [[v2 ty2] | ]_eqn. + rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). (* top *) - mysimpl. apply topred_ok; auto. - rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). apply red_assign; auto. + destruct (type_eq ty1 ty)... subst ty1. + destruct (sem_cast v2 ty2 ty) as [v|]_eqn... + destruct (do_assign_loc w ty m b ofs v) as [[[w' t] m']|]_eqn. + exploit do_assign_loc_sound; eauto. intros [P Q]. + apply topred_ok; auto. split. apply red_assign; auto. exists w'; auto. + apply not_invert_ok; simpl; intros; myinv. exploit do_assign_loc_complete; eauto. congruence. (* depth *) eapply incontext2_ok; eauto. eapply incontext2_ok; eauto. (* assignop *) - destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn. - destruct (is_val a2) as [[v2 ty2] | ]_eqn. + destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn. + destruct (is_val a2) as [[v2 ty2] | ]_eqn. + rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). (* top *) - mysimpl. apply topred_ok; auto. - rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). eapply red_assignop; eauto. + destruct (type_eq ty1 ty)... subst ty1. + destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ]_eqn. + exploit do_deref_loc_sound; eauto. intros [A B]. + apply topred_ok; auto. red. split. apply red_assignop; auto. exists w'; auto. + apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. congruence. (* depth *) eapply incontext2_ok; eauto. eapply incontext2_ok; eauto. (* postincr *) - destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. + destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. rewrite (is_loc_inv _ _ _ _ Heqo). (* top *) - mysimpl. apply topred_ok; auto. - rewrite (is_loc_inv _ _ _ _ Heqo). eapply red_postincr; eauto. + destruct (type_eq ty' ty)... subst ty'. + destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ]_eqn. + exploit do_deref_loc_sound; eauto. intros [A B]. + apply topred_ok; auto. red. split. apply red_postincr; auto. exists w'; auto. + apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. congruence. (* depth *) eapply incontext_ok; eauto. (* comma *) - destruct (is_val a1) as [[v ty'] | ]_eqn. - (* top *) - mysimpl. apply topred_ok; auto. - rewrite (is_val_inv _ _ _ Heqo). apply red_comma; auto. - (* depth *) - eapply incontext_ok; eauto. -(* call *) - destruct (is_val a) as [[vf tyf] | ]_eqn. - destruct (is_val_list rargs) as [vtl | ]_eqn. - (* top *) - destruct (classify_fun tyf) as [tyargs tyres|]_eqn... - mysimpl. apply topred_ok; auto. - rewrite (is_val_inv _ _ _ Heqo). red. split; auto. eapply red_Ecall; eauto. - eapply sem_cast_arguments_sound; eauto. - (* depth *) - eapply incontext2_list_ok; eauto. - eapply incontext2_list_ok; eauto. -(* loc *) - congruence. -(* paren *) - destruct (is_val a) as [[v ty'] | ]_eqn. + destruct (is_val a1) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). (* top *) - mysimpl. apply topred_ok; auto. - rewrite (is_val_inv _ _ _ Heqo). apply red_paren; auto. + destruct (type_eq (typeof a2) ty)... subst ty. + apply topred_ok; auto. split. apply red_comma; auto. exists w; constructor. + (* depth *) + eapply incontext_ok; eauto. +(* call *) + destruct (is_val a) as [[vf tyf] | ]_eqn. + destruct (is_val_list rargs) as [vtl | ]_eqn. + rewrite (is_val_inv _ _ _ Heqo). exploit is_val_list_all_values; eauto. intros ALLVAL. + (* top *) + destruct (classify_fun tyf) as [tyargs tyres|]_eqn... + destruct (Genv.find_funct ge vf) as [fd|]_eqn... + destruct (sem_cast_arguments vtl tyargs) as [vargs|]_eqn... + destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres))... + apply topred_ok; auto. red. split; auto. eapply red_Ecall; eauto. + eapply sem_cast_arguments_sound; eauto. + apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence. + apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. + exploit sem_cast_arguments_complete; eauto. intros [vtl' [P Q]]. congruence. + apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence. + apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence. + (* depth *) + eapply incontext2_list_ok; eauto. + eapply incontext2_list_ok; eauto. +(* loc *) + split; intros. tauto. simpl; congruence. +(* paren *) + destruct (is_val a) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). + (* top *) + destruct (sem_cast v ty' ty) as [v'|]_eqn... + apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. - induction al; simpl; intros. -(* nil *) - congruence. -(* cons *) - eapply incontext2_list_ok'; eauto. -Qed. - - -Lemma step_exprlist_val_list: - forall m al, is_val_list al <> None -> step_exprlist al m = Some nil. -Proof. - induction al; simpl; intros. - auto. - destruct (is_val r1) as [[v1 ty1]|]_eqn; try congruence. - destruct (is_val_list al) as []_eqn; try congruence. - rewrite (is_val_inv _ _ _ Heqo). - rewrite IHal. auto. congruence. -Qed. - -(** Completeness, part 1: if [step_expr] returns [Some ll], - then [ll] contains all possible reducts. *) - -Lemma lred_topred: - forall l1 m1 l2 m2, - lred ge e l1 m1 l2 m2 -> - step_expr LV l1 m1 = topred (Lred l2 m2). -Proof. - induction 1; simpl. -(* var local *) - rewrite H. rewrite dec_eq_true; auto. -(* var global *) - rewrite H; rewrite H0; rewrite H1. rewrite dec_eq_true; auto. -(* deref *) - auto. -(* field struct *) - rewrite H; auto. -(* field union *) - auto. -Qed. - -Lemma rred_topred: - forall r1 m1 r2 m2, - rred r1 m1 r2 m2 -> - step_expr RV r1 m1 = topred (Rred r2 m2). -Proof. - induction 1; simpl. -(* valof *) - rewrite dec_eq_true; auto. rewrite H; auto. -(* addrof *) - auto. -(* unop *) - rewrite H; auto. -(* binop *) - rewrite H; auto. -(* cast *) - rewrite H; auto. -(* condition *) - rewrite H; auto. -(* sizeof *) - auto. -(* assign *) - rewrite dec_eq_true; auto. rewrite H; rewrite H0; auto. -(* assignop *) - rewrite dec_eq_true; auto. rewrite H; rewrite H0; rewrite H1; rewrite H2; auto. -(* postincr *) - rewrite dec_eq_true; auto. rewrite H; rewrite H0; rewrite H1; rewrite H2; auto. -(* comma *) - rewrite H; rewrite dec_eq_true; auto. -(* paren *) - rewrite H; auto. -Qed. - -Lemma sem_cast_arguments_complete: - forall al tyl vl, - cast_arguments al tyl vl -> - exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl = Some vl. -Proof. - induction 1. - exists (@nil (val * type)); auto. - destruct IHcast_arguments as [vtl [A B]]. - exists ((v, ty) :: vtl); simpl. rewrite A; rewrite B; rewrite H. auto. -Qed. - -Lemma callred_topred: - forall a fd args ty m, - callred ge a fd args ty -> - step_expr RV a m = topred (Callred fd args ty m). -Proof. - induction 1; simpl. - rewrite H2. exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]]. - rewrite A; rewrite H; rewrite B; rewrite H1; rewrite dec_eq_true. auto. -Qed. - -Definition reducts_incl {A B: Type} (C: A -> B) (res1: reducts A) (res2: reducts B) : Prop := - match res1, res2 with - | Some ll1, Some ll2 => - forall C1 rd, In (C1, rd) ll1 -> In ((fun x => C(C1 x)), rd) ll2 - | None, Some ll2 => False - | _, None => True - end. - -Lemma reducts_incl_trans: - forall (A1 A2: Type) (C: A1 -> A2) res1 res2, reducts_incl C res1 res2 -> - forall (A3: Type) (C': A2 -> A3) res3, - reducts_incl C' res2 res3 -> - reducts_incl (fun x => C'(C x)) res1 res3. -Proof. - unfold reducts_incl; intros. destruct res1; destruct res2; destruct res3; auto. contradiction. -Qed. - -Lemma reducts_incl_nil: - forall (A B: Type) (C: A -> B) res, - reducts_incl C (Some nil) res. -Proof. - intros; red. destruct res; auto. intros; contradiction. -Qed. - -Lemma reducts_incl_val: - forall (A: Type) a m v ty (C: expr -> A) res, - is_val a = Some(v, ty) -> reducts_incl C (step_expr RV a m) res. -Proof. - intros. rewrite (is_val_inv _ _ _ H). apply reducts_incl_nil. -Qed. - -Lemma reducts_incl_loc: - forall (A: Type) a m b ofs ty (C: expr -> A) res, - is_loc a = Some(b, ofs, ty) -> reducts_incl C (step_expr LV a m) res. -Proof. - intros. rewrite (is_loc_inv _ _ _ _ H). apply reducts_incl_nil. -Qed. - -Lemma reducts_incl_listval: - forall (A: Type) a m vtl (C: exprlist -> A) res, - is_val_list a = Some vtl -> reducts_incl C (step_exprlist a m) res. -Proof. - intros. rewrite step_exprlist_val_list. apply reducts_incl_nil. congruence. -Qed. - -Lemma reducts_incl_incontext: - forall (A B: Type) (C: A -> B) res, - reducts_incl C res (incontext C res). -Proof. - intros; unfold reducts_incl. destruct res; simpl; auto. - intros. set (f := fun z : (expr -> A) * reduction => (fun x : expr => C (fst z x), snd z)). - change (In (f (C1, rd)) (map f l)). apply in_map. auto. -Qed. - -Lemma reducts_incl_incontext2_left: - forall (A1 A2 B: Type) (C1: A1 -> B) res1 (C2: A2 -> B) res2, - reducts_incl C1 res1 (incontext2 C1 res1 C2 res2). -Proof. - intros. destruct res1; simpl; auto. destruct res2; auto. - intros. rewrite in_app_iff. left. - set (f := fun z : (expr -> A1) * reduction => (fun x : expr => C1 (fst z x), snd z)). - change (In (f (C0, rd)) (map f l)). apply in_map; auto. -Qed. - -Lemma reducts_incl_incontext2_right: - forall (A1 A2 B: Type) (C1: A1 -> B) res1 (C2: A2 -> B) res2, - reducts_incl C2 res2 (incontext2 C1 res1 C2 res2). -Proof. - intros. destruct res1; destruct res2; simpl; auto. - intros. rewrite in_app_iff. right. - set (f := fun z : (expr -> A2) * reduction => (fun x : expr => C2 (fst z x), snd z)). - change (In (f (C0, rd)) (map f l0)). apply in_map; auto. -Qed. - -Hint Resolve reducts_incl_val reducts_incl_loc reducts_incl_listval - reducts_incl_incontext reducts_incl_incontext2_left reducts_incl_incontext2_right. - -Lemma step_expr_context: - forall from to C, context from to C -> - forall a m, reducts_incl C (step_expr from a m) (step_expr to (C a) m) -with step_exprlist_context: - forall from C, contextlist from C -> - forall a m, reducts_incl C (step_expr from a m) (step_exprlist (C a) m). -Proof. - induction 1; simpl; intros. -(* top *) - red. destruct (step_expr k a m); auto. intros. - replace (fun x => C1 x) with C1; auto. apply extensionality; auto. -(* deref *) - eapply reducts_incl_trans with (C' := fun x => Ederef x ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. -(* field *) - eapply reducts_incl_trans with (C' := fun x => Efield x f ty); eauto. - destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. -(* valof *) - eapply reducts_incl_trans with (C' := fun x => Evalof x ty); eauto. - destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. -(* addrof *) - eapply reducts_incl_trans with (C' := fun x => Eaddrof x ty); eauto. - destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. -(* unop *) - eapply reducts_incl_trans with (C' := fun x => Eunop op x ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. -(* binop left *) - eapply reducts_incl_trans with (C' := fun x => Ebinop op x e2 ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. -(* binop right *) - eapply reducts_incl_trans with (C' := fun x => Ebinop op e1 x ty); eauto. - destruct (is_val e1) as [[v1 ty1]|]_eqn; eauto. - destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto. -(* cast *) - eapply reducts_incl_trans with (C' := fun x => Ecast x ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. -(* condition *) - eapply reducts_incl_trans with (C' := fun x => Econdition x r2 r3 ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. -(* assign left *) - eapply reducts_incl_trans with (C' := fun x => Eassign x e2 ty); eauto. - destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. -(* assign right *) - eapply reducts_incl_trans with (C' := fun x => Eassign e1 x ty); eauto. - destruct (is_loc e1) as [[[b ofs] ty1]|]_eqn; eauto. - destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto. -(* assignop left *) - eapply reducts_incl_trans with (C' := fun x => Eassignop op x e2 tyres ty); eauto. - destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. -(* assignop right *) - eapply reducts_incl_trans with (C' := fun x => Eassignop op e1 x tyres ty); eauto. - destruct (is_loc e1) as [[[b ofs] ty1]|]_eqn; eauto. - destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto. -(* postincr *) - eapply reducts_incl_trans with (C' := fun x => Epostincr id x ty); eauto. - destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. -(* call left *) - eapply reducts_incl_trans with (C' := fun x => Ecall x el ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. -(* call right *) - eapply reducts_incl_trans with (C' := fun x => Ecall e1 x ty). apply step_exprlist_context. auto. - destruct (is_val e1) as [[v1 ty1]|]_eqn; eauto. - destruct (is_val_list (C a)) as [vl|]_eqn; eauto. -(* comma *) - eapply reducts_incl_trans with (C' := fun x => Ecomma x e2 ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. -(* paren *) - eapply reducts_incl_trans with (C' := fun x => Eparen x ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. - - induction 1; simpl; intros. -(* cons left *) - eapply reducts_incl_trans with (C' := fun x => Econs x el). - apply step_expr_context; eauto. eauto. -(* binop right *) - eapply reducts_incl_trans with (C' := fun x => Econs e1 x). - apply step_exprlist_context; eauto. eauto. -Qed. - -(** Completeness, part 2: given a safe expression, [step_expr] does not return [None]. *) - -Lemma topred_none: - forall rd, topred rd <> None. -Proof. - intros; unfold topred; congruence. -Qed. - -Lemma incontext_none: - forall (A B: Type) (C: A -> B) rds, - rds <> None -> incontext C rds <> None. -Proof. - unfold incontext; intros. destruct rds; congruence. -Qed. - -Lemma incontext2_none: - forall (A1 A2 B: Type) (C1: A1 -> B) rds1 (C2: A2 -> B) rds2, - rds1 <> None -> rds2 <> None -> incontext2 C1 rds1 C2 rds2 <> None. -Proof. - unfold incontext2; intros. destruct rds1; destruct rds2; congruence. + induction al; simpl; intros. +(* nil *) + split; intros. tauto. simpl; congruence. +(* cons *) + eapply incontext2_list_ok'; eauto. Qed. -Lemma safe_expr_kind: - forall k C a m, - context k RV C -> - not_stuck ge e (C a) m -> - k = Cstrategy.expr_kind a. +Lemma step_exprlist_val_list: + forall m al, is_val_list al <> None -> step_exprlist al m = nil. Proof. - intros. - symmetry. eapply Cstrategy.not_imm_stuck_kind; eauto. + induction al; simpl; intros. + auto. + destruct (is_val r1) as [[v1 ty1]|]_eqn; try congruence. + destruct (is_val_list al) as []_eqn; try congruence. + rewrite (is_val_inv _ _ _ Heqo). + rewrite IHal. auto. congruence. Qed. -Lemma safe_inversion: - forall k C a m, - context k RV C -> - not_stuck ge e (C a) m -> - match a with - | Eloc _ _ _ => True - | Eval _ _ => True - | _ => Cstrategy.invert_expr_prop ge e a m - end. -Proof. - intros. eapply Cstrategy.not_imm_stuck_inv; eauto. -Qed. +(** Completeness part 1: [step_expr] contains all possible non-error reducts. *) -Lemma is_val_list_all_values: - forall al vtl, is_val_list al = Some vtl -> Cstrategy.exprlist_all_values al. +Lemma lred_topred: + forall l1 m1 l2 m2, + lred ge e l1 m1 l2 m2 -> + step_expr LV l1 m1 = topred (Lred l2 m2). Proof. - induction al; simpl; intros. auto. - destruct (is_val r1) as [[v ty]|]_eqn; try discriminate. - destruct (is_val_list al) as [vtl'|]_eqn; try discriminate. - rewrite (is_val_inv _ _ _ Heqo). eauto. + induction 1; simpl. +(* var local *) + rewrite H. rewrite dec_eq_true; auto. +(* var global *) + rewrite H; rewrite H0; rewrite H1. rewrite dec_eq_true; auto. +(* deref *) + auto. +(* field struct *) + rewrite H; auto. +(* field union *) + auto. Qed. -Theorem step_expr_defined: - forall a k m C, - context k RV C -> - not_stuck ge e (C a) m -> - step_expr k a m <> None -with step_exprlist_defined: - forall al m C, - Cstrategy.contextlist' C -> - not_stuck ge e (C al) m -> - step_exprlist al m <> None. +Lemma rred_topred: + forall w' r1 m1 t r2 m2, + rred ge r1 m1 t r2 m2 -> possible_trace w t w' -> + step_expr RV r1 m1 = topred (Rred r2 m2 t). Proof. - induction a; intros k m C CTX NS; - rewrite (safe_expr_kind _ _ _ _ CTX NS); - rewrite (safe_expr_kind _ _ _ _ CTX NS) in CTX; - simpl in *; - generalize (safe_inversion _ _ _ _ CTX NS); intro INV. -(* val *) - congruence. -(* var *) - red in INV. destruct INV as [b [P | [P [Q R]]]]. - rewrite P; rewrite dec_eq_true. apply topred_none. - rewrite P; rewrite Q; rewrite R; rewrite dec_eq_true. apply topred_none. -(* field *) - destruct (is_loc a) as [[[b ofs] ty']|]_eqn. - rewrite (is_loc_inv _ _ _ _ Heqo) in INV. red in INV. - destruct ty'; try contradiction. destruct INV as [delta EQ]. rewrite EQ. apply topred_none. - apply topred_none. - apply incontext_none. apply IHa with (C := fun x => C(Efield x f ty)); eauto. + induction 1; simpl; intros. (* valof *) - destruct (is_loc a) as [[[b ofs] ty']|]_eqn. - rewrite (is_loc_inv _ _ _ _ Heqo) in INV. red in INV. destruct INV as [EQ [v LD]]. subst. - rewrite dec_eq_true; rewrite LD; apply topred_none. - apply incontext_none. apply IHa with (C := fun x => C(Evalof x ty)); eauto. -(* deref *) - destruct (is_val a) as [[v ty']|]_eqn. - rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [b [ofs EQ]]. subst. - apply topred_none. - apply incontext_none. apply IHa with (C := fun x => C(Ederef x ty)); eauto. -(* addrof *) - destruct (is_loc a) as [[[b ofs] ty']|]_eqn. - apply topred_none. - apply incontext_none. apply IHa with (C := fun x => C(Eaddrof x ty)); eauto. + rewrite dec_eq_true; auto. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). auto. +(* addrof *) + inv H. auto. (* unop *) - destruct (is_val a) as [[v1 ty1]|]_eqn. - rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ]. - rewrite EQ; apply topred_none. - apply incontext_none. apply IHa with (C := fun x => C(Eunop op x ty)); eauto. + inv H0. rewrite H; auto. (* binop *) - destruct (is_val a1) as [[v1 ty1]|]_eqn. - destruct (is_val a2) as [[v2 ty2]|]_eqn. - rewrite (is_val_inv _ _ _ Heqo) in INV. - rewrite (is_val_inv _ _ _ Heqo0) in INV. red in INV. destruct INV as [v EQ]. - rewrite EQ; apply topred_none. - apply incontext2_none. apply IHa1 with (C := fun x => C(Ebinop op x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Ebinop op a1 x ty)); eauto. - apply incontext2_none. apply IHa1 with (C := fun x => C(Ebinop op x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Ebinop op a1 x ty)); eauto. + inv H0. rewrite H; auto. (* cast *) - destruct (is_val a) as [[v1 ty1]|]_eqn. - rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ]. - rewrite EQ; apply topred_none. - apply incontext_none. apply IHa with (C := fun x => C(Ecast x ty)); eauto. + inv H0. rewrite H; auto. (* condition *) - destruct (is_val a1) as [[v1 ty1]|]_eqn. - rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ]. - rewrite EQ; apply topred_none. - apply incontext_none. apply IHa1 with (C := fun x => C(Econdition x a2 a3 ty)); eauto. + inv H0. rewrite H; auto. (* sizeof *) - apply topred_none. + inv H. auto. (* assign *) - destruct (is_loc a1) as [[[b ofs] ty1]|]_eqn. - destruct (is_val a2) as [[v2 ty2]|]_eqn. - rewrite (is_loc_inv _ _ _ _ Heqo) in INV. - rewrite (is_val_inv _ _ _ Heqo0) in INV. red in INV. - destruct INV as [v [m' [P [Q R]]]]. - subst. rewrite dec_eq_true; rewrite Q; rewrite R; apply topred_none. - apply incontext2_none. apply IHa1 with (C := fun x => C(Eassign x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Eassign a1 x ty)); eauto. - apply incontext2_none. apply IHa1 with (C := fun x => C(Eassign x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Eassign a1 x ty)); eauto. + rewrite dec_eq_true; auto. rewrite H. rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H1). auto. (* assignop *) - destruct (is_loc a1) as [[[b ofs] ty1]|]_eqn. - destruct (is_val a2) as [[v2 ty2]|]_eqn. - rewrite (is_loc_inv _ _ _ _ Heqo) in INV. - rewrite (is_val_inv _ _ _ Heqo0) in INV. red in INV. - destruct INV as [v1 [v [v' [m' [P [Q [R [S T]]]]]]]]. - subst. rewrite dec_eq_true; rewrite Q; rewrite R; rewrite S; rewrite T; apply topred_none. - apply incontext2_none. apply IHa1 with (C := fun x => C(Eassignop op x a2 tyres ty)); eauto. apply IHa2 with (C := fun x => C(Eassignop op a1 x tyres ty)); eauto. - apply incontext2_none. apply IHa1 with (C := fun x => C(Eassignop op x a2 tyres ty)); eauto. apply IHa2 with (C := fun x => C(Eassignop op a1 x tyres ty)); eauto. + rewrite dec_eq_true; auto. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). auto. (* postincr *) - destruct (is_loc a) as [[[b ofs] ty1]|]_eqn. - rewrite (is_loc_inv _ _ _ _ Heqo) in INV. red in INV. - destruct INV as [v1 [v2 [v3 [m' [P [Q [R [S T]]]]]]]]. - subst. rewrite dec_eq_true; rewrite Q; rewrite R; rewrite S; rewrite T; apply topred_none. - apply incontext_none. apply IHa with (C := fun x => C(Epostincr id x ty)); eauto. + rewrite dec_eq_true; auto. subst. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H1). auto. (* comma *) - destruct (is_val a1) as [[v1 ty1]|]_eqn. - rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. rewrite INV. - rewrite dec_eq_true; apply topred_none. - apply incontext_none. apply IHa1 with (C := fun x => C(Ecomma x a2 ty)); eauto. -(* call *) - destruct (is_val a) as [[vf tyf]|]_eqn. - destruct (is_val_list rargs) as [vtl|]_eqn. - rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. - destruct INV as [tyargs [tyres [fd [vl [P [Q [R S]]]]]]]. - eapply is_val_list_all_values; eauto. - rewrite P; rewrite Q. - exploit sem_cast_arguments_complete; eauto. intros [vtl' [U V]]. - assert (vtl' = vtl) by congruence. subst. rewrite V. rewrite S. rewrite dec_eq_true. - apply topred_none. - apply incontext2_none. apply IHa with (C := fun x => C(Ecall x rargs ty)); eauto. - apply step_exprlist_defined with (C := fun x => C(Ecall a x ty)); auto. - apply Cstrategy.contextlist'_intro with (rl0 := Enil). auto. - apply incontext2_none. apply IHa with (C := fun x => C(Ecall x rargs ty)); eauto. - apply step_exprlist_defined with (C := fun x => C(Ecall a x ty)); auto. - apply Cstrategy.contextlist'_intro with (rl0 := Enil). auto. -(* loc *) - congruence. + inv H0. rewrite dec_eq_true; auto. (* paren *) - destruct (is_val a) as [[v1 ty1]|]_eqn. - rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ]. - rewrite EQ; apply topred_none. - apply incontext_none. apply IHa with (C := fun x => C(Eparen x ty)); eauto. - - induction al; intros; simpl. -(* nil *) - congruence. -(* cons *) - apply incontext2_none. - apply step_expr_defined with (C := fun x => C(Econs x al)); eauto. - apply Cstrategy.contextlist'_head; auto. - apply IHal with (C := fun x => C(Econs r1 x)); auto. - apply Cstrategy.contextlist'_tail; auto. + inv H0. rewrite H; auto. Qed. -(** Connections between [not_stuck] and [step_expr]. *) - -Lemma step_expr_not_imm_stuck: - forall k a m, - step_expr k a m <> None -> - not_imm_stuck ge e k a m. +Lemma callred_topred: + forall a fd args ty m, + callred ge a fd args ty -> + step_expr RV a m = topred (Callred fd args ty m). Proof. - intros. generalize (step_expr_sound a k m). unfold reducts_ok. - destruct (step_expr k a m) as [ll|]. destruct ll. -(* value or location *) - destruct k; destruct a; simpl; intros; try congruence. - apply not_stuck_loc. - apply Csem.not_stuck_val. -(* reducible *) - intros R. destruct p as [C1 rd1]. destruct (R C1 rd1) as [P [a' [U V]]]; auto with coqlib. - subst a. red in V. destruct rd1. - eapply not_stuck_lred; eauto. - eapply not_stuck_rred; eauto. - destruct V. subst m'. eapply not_stuck_callred; eauto. -(* stuck *) - congruence. + induction 1; simpl. + rewrite H2. exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]]. + rewrite A; rewrite H; rewrite B; rewrite H1; rewrite dec_eq_true. auto. Qed. -Lemma step_expr_not_stuck: - forall a m, - step_expr RV a m <> None -> - not_stuck ge e a m. -Proof. - intros; red; intros. subst a. - apply step_expr_not_imm_stuck. - generalize (step_expr_context _ _ C H0 e' m). unfold reducts_incl. - destruct (step_expr k e' m). congruence. - destruct (step_expr RV (C e') m). tauto. congruence. -Qed. +Definition reducts_incl {A B: Type} (C: A -> B) (res1: reducts A) (res2: reducts B) : Prop := + forall C1 rd, In (C1, rd) res1 -> In ((fun x => C(C1 x)), rd) res2. -Lemma not_stuck_step_expr: - forall a m, - not_stuck ge e a m -> - step_expr RV a m <> None. +Lemma reducts_incl_trans: + forall (A1 A2: Type) (C: A1 -> A2) res1 res2, reducts_incl C res1 res2 -> + forall (A3: Type) (C': A2 -> A3) res3, + reducts_incl C' res2 res3 -> + reducts_incl (fun x => C'(C x)) res1 res3. Proof. - intros. apply step_expr_defined with (C := fun x => x); auto. + unfold reducts_incl; intros. auto. Qed. -End EXPRS. - -(** * External functions and events. *) - -Section EVENTS. - -Variable F V: Type. -Variable genv: Genv.t F V. - -Definition eventval_of_val (v: val) (t: typ) : option eventval := - match v, t with - | Vint i, AST.Tint => Some (EVint i) - | Vfloat f, AST.Tfloat => Some (EVfloat f) - | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol genv b; Some (EVptr_global id ofs) - | _, _ => None - end. - -Fixpoint list_eventval_of_val (vl: list val) (tl: list typ) : option (list eventval) := - match vl, tl with - | nil, nil => Some nil - | v1::vl, t1::tl => - do ev1 <- eventval_of_val v1 t1; - do evl <- list_eventval_of_val vl tl; - Some (ev1 :: evl) - | _, _ => None - end. - -Definition val_of_eventval (ev: eventval) (t: typ) : option val := - match ev, t with - | EVint i, AST.Tint => Some (Vint i) - | EVfloat f, AST.Tfloat => Some (Vfloat f) - | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol genv id; Some (Vptr b ofs) - | _, _ => None - end. - -Lemma eventval_of_val_sound: - forall v t ev, eventval_of_val v t = Some ev -> eventval_match genv ev t v. +Lemma reducts_incl_nil: + forall (A B: Type) (C: A -> B) res, + reducts_incl C nil res. Proof. - intros. destruct v; destruct t; simpl in H; inv H. - constructor. - constructor. - destruct (Genv.invert_symbol genv b) as [id|]_eqn; inv H1. - constructor. apply Genv.invert_find_symbol; auto. + intros; red. intros; contradiction. Qed. -Lemma eventval_of_val_complete: - forall ev t v, eventval_match genv ev t v -> eventval_of_val v t = Some ev. +Lemma reducts_incl_val: + forall (A: Type) a m v ty (C: expr -> A) res, + is_val a = Some(v, ty) -> reducts_incl C (step_expr RV a m) res. Proof. - induction 1; simpl; auto. - rewrite (Genv.find_invert_symbol _ _ H). auto. -Qed. - -Lemma list_eventval_of_val_sound: - forall vl tl evl, list_eventval_of_val vl tl = Some evl -> eventval_list_match genv evl tl vl. -Proof with try discriminate. - induction vl; destruct tl; simpl; intros; inv H. - constructor. - destruct (eventval_of_val a t) as [ev1|]_eqn... - destruct (list_eventval_of_val vl tl) as [evl'|]_eqn... - inv H1. constructor. apply eventval_of_val_sound; auto. eauto. + intros. rewrite (is_val_inv _ _ _ H). apply reducts_incl_nil. Qed. -Lemma list_eventval_of_val_complete: - forall evl tl vl, eventval_list_match genv evl tl vl -> list_eventval_of_val vl tl = Some evl. +Lemma reducts_incl_loc: + forall (A: Type) a m b ofs ty (C: expr -> A) res, + is_loc a = Some(b, ofs, ty) -> reducts_incl C (step_expr LV a m) res. Proof. - induction 1; simpl. auto. - rewrite (eventval_of_val_complete _ _ _ H). rewrite IHeventval_list_match. auto. + intros. rewrite (is_loc_inv _ _ _ _ H). apply reducts_incl_nil. Qed. -Lemma val_of_eventval_sound: - forall ev t v, val_of_eventval ev t = Some v -> eventval_match genv ev t v. +Lemma reducts_incl_listval: + forall (A: Type) a m vtl (C: exprlist -> A) res, + is_val_list a = Some vtl -> reducts_incl C (step_exprlist a m) res. Proof. - intros. destruct ev; destruct t; simpl in H; inv H. - constructor. - constructor. - destruct (Genv.find_symbol genv i) as [b|]_eqn; inv H1. - constructor. auto. + intros. rewrite step_exprlist_val_list. apply reducts_incl_nil. congruence. Qed. -Lemma val_of_eventval_complete: - forall ev t v, eventval_match genv ev t v -> val_of_eventval ev t = Some v. +Lemma reducts_incl_incontext: + forall (A B: Type) (C: A -> B) res, + reducts_incl C res (incontext C res). Proof. - induction 1; simpl; auto. rewrite H; auto. + unfold reducts_incl, incontext. intros. + set (f := fun z : (expr -> A) * reduction => (fun x : expr => C (fst z x), snd z)). + change (In (f (C1, rd)) (map f res)). apply in_map. auto. Qed. -(** System calls and library functions *) - -Definition do_ef_external (name: ident) (sg: signature) - (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - do args <- list_eventval_of_val vargs (sig_args sg); - match nextworld_io w name args with - | None => None - | Some(res, w') => - do vres <- val_of_eventval res (proj_sig_res sg); - Some(w', Event_syscall name args res :: E0, vres, m) - end. - -Definition do_ef_volatile_load (chunk: memory_chunk) - (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - match vargs with - | Vptr b ofs :: nil => - if block_is_volatile genv b then - do id <- Genv.invert_symbol genv b; - match nextworld_vload w chunk id ofs with - | None => None - | Some(res, w') => - do vres <- val_of_eventval res (type_of_chunk chunk); - Some(w', Event_vload chunk id ofs res :: nil, Val.load_result chunk vres, m) - end - else - do v <- Mem.load chunk m b (Int.unsigned ofs); - Some(w, E0, v, m) - | _ => None - end. - -Definition do_ef_volatile_store (chunk: memory_chunk) - (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - match vargs with - | Vptr b ofs :: v :: nil => - if block_is_volatile genv b then - do id <- Genv.invert_symbol genv b; - do ev <- eventval_of_val v (type_of_chunk chunk); - do w' <- nextworld_vstore w chunk id ofs ev; - Some(w', Event_vstore chunk id ofs ev :: nil, Vundef, m) - else - do m' <- Mem.store chunk m b (Int.unsigned ofs) v; - Some(w, E0, Vundef, m') - | _ => None - end. - -Definition do_ef_volatile_load_global (chunk: memory_chunk) (id: ident) (ofs: int) - (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - match Genv.find_symbol genv id with - | Some b => do_ef_volatile_load chunk w (Vptr b ofs :: vargs) m - | None => None - end. - -Definition do_ef_volatile_store_global (chunk: memory_chunk) (id: ident) (ofs: int) - (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - match Genv.find_symbol genv id with - | Some b => do_ef_volatile_store chunk w (Vptr b ofs :: vargs) m - | None => None - end. - -Definition do_ef_malloc - (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - match vargs with - | Vint n :: nil => - let (m', b) := Mem.alloc m (-4) (Int.unsigned n) in - do m'' <- Mem.store Mint32 m' b (-4) (Vint n); - Some(w, E0, Vptr b Int.zero, m'') - | _ => None - end. - -Definition do_ef_free - (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - match vargs with - | Vptr b lo :: nil => - do vsz <- Mem.load Mint32 m b (Int.unsigned lo - 4); - match vsz with - | Vint sz => - check (zlt 0 (Int.unsigned sz)); - do m' <- Mem.free m b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz); - Some(w, E0, Vundef, m') - | _ => None - end - | _ => None - end. - -Definition memcpy_args_ok - (sz al: Z) (bdst: block) (odst: Z) (bsrc: block) (osrc: Z) : Prop := - (al = 1 \/ al = 2 \/ al = 4) - /\ sz > 0 - /\ (al | sz) /\ (al | osrc) /\ (al | odst) - /\ (bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc). - -Remark memcpy_check_args: - forall sz al bdst odst bsrc osrc, - {memcpy_args_ok sz al bdst odst bsrc osrc} + {~memcpy_args_ok sz al bdst odst bsrc osrc}. -Proof with try (right; intuition omega). - intros. - assert (X: {al = 1 \/ al = 2 \/ al = 4} + {~(al = 1 \/ al = 2 \/ al = 4)}). - destruct (zeq al 1); auto. destruct (zeq al 2); auto. destruct (zeq al 4); auto... - unfold memcpy_args_ok. destruct X... - assert (al > 0) by (intuition omega). - destruct (zlt 0 sz)... - destruct (Zdivide_dec al sz); auto... - destruct (Zdivide_dec al osrc); auto... - destruct (Zdivide_dec al odst); auto... - assert (Y: {bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc} - +{~(bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc)}). - destruct (eq_block bsrc bdst); auto. - destruct (zeq osrc odst); auto. - destruct (zle (osrc + sz) odst); auto. - destruct (zle (odst + sz) osrc); auto. - right; intuition omega. - destruct Y... left; intuition omega. +Lemma reducts_incl_incontext2_left: + forall (A1 A2 B: Type) (C1: A1 -> B) res1 (C2: A2 -> B) res2, + reducts_incl C1 res1 (incontext2 C1 res1 C2 res2). +Proof. + unfold reducts_incl, incontext2, incontext. intros. + rewrite in_app_iff. left. + set (f := fun z : (expr -> A1) * reduction => (fun x : expr => C1 (fst z x), snd z)). + change (In (f (C0, rd)) (map f res1)). apply in_map; auto. Qed. -Definition do_ef_memcpy (sz al: Z) - (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - match vargs with - | Vptr bdst odst :: Vptr bsrc osrc :: nil => - if memcpy_check_args sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc) then - do bytes <- Mem.loadbytes m bsrc (Int.unsigned osrc) sz; - do m' <- Mem.storebytes m bdst (Int.unsigned odst) bytes; - Some(w, E0, Vundef, m') - else None - | _ => None - end. +Lemma reducts_incl_incontext2_right: + forall (A1 A2 B: Type) (C1: A1 -> B) res1 (C2: A2 -> B) res2, + reducts_incl C2 res2 (incontext2 C1 res1 C2 res2). +Proof. + unfold reducts_incl, incontext2, incontext. intros. + rewrite in_app_iff. right. + set (f := fun z : (expr -> A2) * reduction => (fun x : expr => C2 (fst z x), snd z)). + change (In (f (C0, rd)) (map f res2)). apply in_map; auto. +Qed. -Definition do_ef_annot (text: ident) (targs: list typ) - (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - do args <- list_eventval_of_val vargs targs; - Some(w, Event_annot text args :: E0, Vundef, m). +Hint Resolve reducts_incl_val reducts_incl_loc reducts_incl_listval + reducts_incl_incontext reducts_incl_incontext2_left reducts_incl_incontext2_right. -Definition do_ef_annot_val (text: ident) (targ: typ) - (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - match vargs with - | varg :: nil => - do arg <- eventval_of_val varg targ; - Some(w, Event_annot text (arg :: nil) :: E0, varg, m) - | _ => None - end. +Lemma step_expr_context: + forall from to C, context from to C -> + forall a m, reducts_incl C (step_expr from a m) (step_expr to (C a) m) +with step_exprlist_context: + forall from C, contextlist from C -> + forall a m, reducts_incl C (step_expr from a m) (step_exprlist (C a) m). +Proof. + induction 1; simpl; intros. +(* top *) + red. destruct (step_expr k a m); auto. intros. + replace (fun x => C1 x) with C1; auto. apply extensionality; auto. +(* deref *) + eapply reducts_incl_trans with (C' := fun x => Ederef x ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* field *) + eapply reducts_incl_trans with (C' := fun x => Efield x f ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* valof *) + eapply reducts_incl_trans with (C' := fun x => Evalof x ty); eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. +(* addrof *) + eapply reducts_incl_trans with (C' := fun x => Eaddrof x ty); eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. +(* unop *) + eapply reducts_incl_trans with (C' := fun x => Eunop op x ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* binop left *) + eapply reducts_incl_trans with (C' := fun x => Ebinop op x e2 ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* binop right *) + eapply reducts_incl_trans with (C' := fun x => Ebinop op e1 x ty); eauto. + destruct (is_val e1) as [[v1 ty1]|]_eqn; eauto. + destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto. +(* cast *) + eapply reducts_incl_trans with (C' := fun x => Ecast x ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* condition *) + eapply reducts_incl_trans with (C' := fun x => Econdition x r2 r3 ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* assign left *) + eapply reducts_incl_trans with (C' := fun x => Eassign x e2 ty); eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. +(* assign right *) + eapply reducts_incl_trans with (C' := fun x => Eassign e1 x ty); eauto. + destruct (is_loc e1) as [[[b ofs] ty1]|]_eqn; eauto. + destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto. +(* assignop left *) + eapply reducts_incl_trans with (C' := fun x => Eassignop op x e2 tyres ty); eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. +(* assignop right *) + eapply reducts_incl_trans with (C' := fun x => Eassignop op e1 x tyres ty); eauto. + destruct (is_loc e1) as [[[b ofs] ty1]|]_eqn; eauto. + destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto. +(* postincr *) + eapply reducts_incl_trans with (C' := fun x => Epostincr id x ty); eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. +(* call left *) + eapply reducts_incl_trans with (C' := fun x => Ecall x el ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* call right *) + eapply reducts_incl_trans with (C' := fun x => Ecall e1 x ty). apply step_exprlist_context. auto. + destruct (is_val e1) as [[v1 ty1]|]_eqn; eauto. + destruct (is_val_list (C a)) as [vl|]_eqn; eauto. +(* comma *) + eapply reducts_incl_trans with (C' := fun x => Ecomma x e2 ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* paren *) + eapply reducts_incl_trans with (C' := fun x => Eparen x ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. -Definition do_external (ef: external_function): - world -> list val -> mem -> option (world * trace * val * mem) := - match ef with - | EF_external name sg => do_ef_external name sg - | EF_builtin name sg => do_ef_external name sg - | EF_vload chunk => do_ef_volatile_load chunk - | EF_vstore chunk => do_ef_volatile_store chunk - | EF_vload_global chunk id ofs => do_ef_volatile_load_global chunk id ofs - | EF_vstore_global chunk id ofs => do_ef_volatile_store_global chunk id ofs - | EF_malloc => do_ef_malloc - | EF_free => do_ef_free - | EF_memcpy sz al => do_ef_memcpy sz al - | EF_annot text targs => do_ef_annot text targs - | EF_annot_val text targ => do_ef_annot_val text targ - end. + induction 1; simpl; intros. +(* cons left *) + eapply reducts_incl_trans with (C' := fun x => Econs x el). + apply step_expr_context; eauto. eauto. +(* binop right *) + eapply reducts_incl_trans with (C' := fun x => Econs e1 x). + apply step_exprlist_context; eauto. eauto. +Qed. -Ltac mydestr := - match goal with - | [ |- None = Some _ -> _ ] => intro X; discriminate - | [ |- Some _ = Some _ -> _ ] => intro X; inv X - | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr - | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr - | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr - | _ => idtac - end. +(** Completeness part 2: if we can reduce to [Stuckstate], [step_expr] + contains at least one [Stuckred] reduction. *) -Lemma do_ef_external_sound: - forall ef w vargs m w' t vres m', - do_external ef w vargs m = Some(w', t, vres, m') -> - external_call ef genv vargs m t vres m' /\ possible_trace w t w'. -Proof with try congruence. - intros until m'. - assert (IO: forall name sg, - do_ef_external name sg w vargs m = Some(w', t, vres, m') -> - extcall_io_sem name sg genv vargs m t vres m' /\ possible_trace w t w'). - intros until sg. unfold do_ef_external. mydestr. destruct p as [res w'']; mydestr. - split. econstructor. apply list_eventval_of_val_sound; auto. - apply val_of_eventval_sound; auto. - econstructor. constructor; eauto. constructor. +Lemma not_stuckred_imm_safe: + forall m a k, + (forall C, ~In (C, Stuckred) (step_expr k a m)) -> imm_safe_t k a m. +Proof. + intros. generalize (step_expr_sound a k m). intros [A B]. + destruct (step_expr k a m) as [|[C rd] res]_eqn. + specialize (B (refl_equal _)). destruct k. + destruct a; simpl in B; try congruence. constructor. + destruct a; simpl in B; try congruence. constructor. + assert (NOTSTUCK: rd <> Stuckred). + red; intros. elim (H C); subst rd; auto with coqlib. + exploit A. eauto with coqlib. intros [a' [k' [P [Q R]]]]. + destruct k'; destruct rd; simpl in R; intuition. + subst a. eapply imm_safe_t_lred; eauto. + subst a. destruct H1 as [w' PT]. eapply imm_safe_t_rred; eauto. + subst. eapply imm_safe_t_callred; eauto. +Qed. - assert (VLOAD: forall chunk vargs, - do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m') -> - volatile_load_sem chunk genv vargs m t vres m' /\ possible_trace w t w'). - intros chunk vargs'. - unfold do_ef_volatile_load. destruct vargs'... destruct v... destruct vargs'... - mydestr. destruct p as [res w'']; mydestr. - split. constructor. apply Genv.invert_find_symbol; auto. auto. - apply val_of_eventval_sound; auto. - econstructor. constructor; eauto. constructor. - split. constructor; auto. constructor. +Lemma not_imm_safe_stuck_red: + forall m a k C, + context k RV C -> + ~imm_safe_t k a m -> + exists C', In (C', Stuckred) (step_expr RV (C a) m). +Proof. + intros. + assert (exists C', In (C', Stuckred) (step_expr k a m)). + destruct (classic (exists C', In (C', Stuckred) (step_expr k a m))); auto. + elim H0. apply not_stuckred_imm_safe. apply not_ex_all_not. auto. + destruct H1 as [C' IN]. + specialize (step_expr_context _ _ _ H a m). unfold reducts_incl. + intro. + exists (fun x => (C (C' x))). apply H1; auto. +Qed. - assert (VSTORE: forall chunk vargs, - do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m') -> - volatile_store_sem chunk genv vargs m t vres m' /\ possible_trace w t w'). - intros chunk vargs'. - unfold do_ef_volatile_store. destruct vargs'... destruct v... destruct vargs'... destruct vargs'... - mydestr. - split. constructor. apply Genv.invert_find_symbol; auto. auto. - apply eventval_of_val_sound; auto. - econstructor. constructor; eauto. constructor. - split. constructor; auto. constructor. +(** Connections between [imm_safe_t] and [imm_safe] *) - destruct ef; simpl. -(* EF_external *) - auto. -(* EF_builtin *) - auto. -(* EF_vload *) - auto. -(* EF_vstore *) - auto. -(* EF_vload_global *) - rewrite volatile_load_global_charact. - unfold do_ef_volatile_load_global. destruct (Genv.find_symbol genv)... - intros. exploit VLOAD; eauto. intros [A B]. split; auto. exists b; auto. -(* EF_vstore_global *) - rewrite volatile_store_global_charact. - unfold do_ef_volatile_store_global. destruct (Genv.find_symbol genv)... - intros. exploit VSTORE; eauto. intros [A B]. split; auto. exists b; auto. -(* EF_malloc *) - unfold do_ef_malloc. destruct vargs... destruct v... destruct vargs... - destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b]_eqn. mydestr. - split. econstructor; eauto. constructor. -(* EF_free *) - unfold do_ef_free. destruct vargs... destruct v... destruct vargs... - mydestr. destruct v... mydestr. - split. econstructor; eauto. omega. constructor. -(* EF_memcpy *) - unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... - destruct v... destruct vargs... mydestr. red in m0. - split. econstructor; eauto; tauto. constructor. -(* EF_annot *) - unfold do_ef_annot. mydestr. - split. constructor. apply list_eventval_of_val_sound; auto. - econstructor. constructor; eauto. constructor. -(* EF_annot_val *) - unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr. - split. constructor. apply eventval_of_val_sound; auto. - econstructor. constructor; eauto. constructor. +Lemma imm_safe_imm_safe_t: + forall k a m, + imm_safe ge e k a m -> + imm_safe_t k a m \/ + exists C, exists a1, exists t, exists a1', exists m', + context RV k C /\ a = C a1 /\ rred ge a1 m t a1' m' /\ forall w', ~possible_trace w t w'. +Proof. + intros. inv H. + left. apply imm_safe_t_val. + left. apply imm_safe_t_loc. + left. eapply imm_safe_t_lred; eauto. + destruct (classic (exists w', possible_trace w t w')) as [[w' A] | A]. + left. eapply imm_safe_t_rred; eauto. + right. exists C; exists e0; exists t; exists e'; exists m'; intuition. apply A; exists w'; auto. + left. eapply imm_safe_t_callred; eauto. Qed. -Lemma do_ef_external_complete: - forall ef w vargs m w' t vres m', - external_call ef genv vargs m t vres m' -> possible_trace w t w' -> - do_external ef w vargs m = Some(w', t, vres, m'). -Proof. - intros. - assert (IO: forall name sg, - extcall_io_sem name sg genv vargs m t vres m' -> - do_ef_external name sg w vargs m = Some (w', t, vres, m')). - intros. inv H1. inv H0. inv H8. inv H6. - unfold do_ef_external. rewrite (list_eventval_of_val_complete _ _ _ H2). rewrite H8. - rewrite (val_of_eventval_complete _ _ _ H3). auto. - - assert (VLOAD: forall chunk vargs, - volatile_load_sem chunk genv vargs m t vres m' -> - do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m')). - intros. inv H1; unfold do_ef_volatile_load. - inv H0. inv H9. inv H7. - rewrite H3. rewrite (Genv.find_invert_symbol _ _ H2). rewrite H10. - rewrite (val_of_eventval_complete _ _ _ H4). auto. - inv H0. rewrite H2. rewrite H3. auto. +(** A state can "crash the world" if it can make an observable transition + whose trace is not accepted by the external world. *) - assert (VSTORE: forall chunk vargs, - volatile_store_sem chunk genv vargs m t vres m' -> - do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m')). - intros. inv H1; unfold do_ef_volatile_store. - inv H0. inv H9. inv H7. - rewrite H3. rewrite (Genv.find_invert_symbol _ _ H2). - rewrite (eventval_of_val_complete _ _ _ H4). rewrite H10. auto. - inv H0. rewrite H2. rewrite H3. auto. +Definition can_crash_world (w: world) (S: state) : Prop := + exists t, exists S', Csem.step ge S t S' /\ forall w', ~possible_trace w t w'. - destruct ef; simpl in *. -(* EF_external *) - auto. -(* EF_builtin *) - auto. -(* EF_vload *) - auto. -(* EF_vstore *) - auto. -(* EF_vload_global *) - rewrite volatile_load_global_charact in H. destruct H as [b [P Q]]. - unfold do_ef_volatile_load_global. rewrite P. auto. -(* EF_vstore *) - rewrite volatile_store_global_charact in H. destruct H as [b [P Q]]. - unfold do_ef_volatile_store_global. rewrite P. auto. -(* EF_malloc *) - inv H; unfold do_ef_malloc. - inv H0. rewrite H1. rewrite H2. auto. -(* EF_free *) - inv H; unfold do_ef_free. - inv H0. rewrite H1. rewrite zlt_true. rewrite H3. auto. omega. -(* EF_memcpy *) - inv H; unfold do_ef_memcpy. - inv H0. rewrite pred_dec_true. rewrite H7; rewrite H8; auto. - red. tauto. -(* EF_annot *) - inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. - rewrite (list_eventval_of_val_complete _ _ _ H1). auto. -(* EF_annot_val *) - inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. - rewrite (eventval_of_val_complete _ _ _ H1). auto. +Theorem not_imm_safe_t: + forall K C a m f k, + context K RV C -> + ~imm_safe_t K a m -> + Csem.step ge (ExprState f (C a) k e m) E0 Stuckstate \/ can_crash_world w (ExprState f (C a) k e m). +Proof. + intros. destruct (classic (imm_safe ge e K a m)). + exploit imm_safe_imm_safe_t; eauto. + intros [A | [C1 [a1 [t [a1' [m' [A [B [D E]]]]]]]]]. contradiction. + right. red. exists t; econstructor; split; auto. + left. rewrite B. eapply step_rred with (C := fun x => C(C1 x)). eauto. eauto. + left. left. eapply step_stuck; eauto. Qed. -End EVENTS. +End EXPRS. (** * Transitions over states. *) @@ -1560,7 +1773,7 @@ Proof. rewrite H; rewrite IHalloc_variables; auto. Qed. -Function sem_bind_parameters (e: env) (m: mem) (l: list (ident * type)) (lv: list val) +Function sem_bind_parameters (w: world) (e: env) (m: mem) (l: list (ident * type)) (lv: list val) {struct l} : option mem := match l, lv with | nil, nil => Some m @@ -1568,37 +1781,39 @@ Function sem_bind_parameters (e: env) (m: mem) (l: list (ident * type)) (lv: lis match PTree.get id e with | Some (b, ty') => check (type_eq ty ty'); - do m1 <- store_value_of_type ty m b Int.zero v1; - sem_bind_parameters e m1 params lv + do w', t, m1 <- do_assign_loc w ty m b Int.zero v1; + match t with nil => sem_bind_parameters w e m1 params lv | _ => None end | None => None end | _, _ => None end. -Lemma sem_bind_parameters_sound : forall e m l lv m', - sem_bind_parameters e m l lv = Some m' -> - bind_parameters e m l lv m'. +Lemma sem_bind_parameters_sound : forall w e m l lv m', + sem_bind_parameters w e m l lv = Some m' -> + bind_parameters ge e m l lv m'. Proof. - intros; functional induction (sem_bind_parameters e m l lv); try discriminate. - inversion H; constructor; auto. - econstructor; eauto. + intros; functional induction (sem_bind_parameters w e m l lv); try discriminate. + inversion H; constructor; auto. + exploit do_assign_loc_sound; eauto. intros [A B]. econstructor; eauto. Qed. -Lemma sem_bind_parameters_complete : forall e m l lv m', - bind_parameters e m l lv m' -> - sem_bind_parameters e m l lv = Some m'. +Lemma sem_bind_parameters_complete : forall w e m l lv m', + bind_parameters ge e m l lv m' -> + sem_bind_parameters w e m l lv = Some m'. Proof. induction 1; simpl; auto. - rewrite H. rewrite dec_eq_true. - destruct (store_value_of_type ty m b Int.zero v1); try discriminate. - inv H0; auto. + rewrite H. rewrite dec_eq_true. + assert (possible_trace w E0 w) by constructor. + rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H2). + simpl. auto. Qed. Definition expr_final_state (f: function) (k: cont) (e: env) (C_rd: (expr -> expr) * reduction) := match snd C_rd with | Lred a m => (E0, ExprState f (fst C_rd a) k e m) - | Rred a m => (E0, ExprState f (fst C_rd a) k e m) + | Rred a m t => (t, ExprState f (fst C_rd a) k e m) | Callred fd vargs ty m => (E0, Callstate fd vargs (Kcall f e (fst C_rd) ty k) m) + | Stuck => (E0, Stuckstate) end. Local Open Scope list_monad_scope. @@ -1637,10 +1852,7 @@ Definition do_step (w: world) (s: state) : list (trace * state) := end | None => - match step_expr e RV a m with - | None => nil - | Some ll => map (expr_final_state f k e) ll - end + map (expr_final_state f k e) (step_expr e w RV a m) end | State f (Sdo x) k e m => ret(ExprState f x (Kdo k) e m) @@ -1674,9 +1886,9 @@ Definition do_step (w: world) (s: state) : list (trace * state) := ret (Returnstate Vundef (call_cont k) m') | State f (Sreturn (Some x)) k e m => ret (ExprState f x (Kreturn k) e m) | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m => - check (type_eq f.(fn_return) Tvoid); - do m' <- Mem.free_list m (blocks_of_env e); - ret (Returnstate Vundef k m') + check type_eq (f.(fn_return)) Tvoid; + do m' <- Mem.free_list m (blocks_of_env e); + ret (Returnstate Vundef k m') | State f (Sswitch x sl) k e m => ret (ExprState f x (Kswitch1 sl k) e m) | State f (Sskip|Sbreak) (Kswitch2 k) e m => ret (State f Sskip k e m) @@ -1692,10 +1904,10 @@ Definition do_step (w: world) (s: state) : list (trace * state) := | Callstate (Internal f) vargs k m => check (list_norepet_dec ident_eq (var_names (fn_params f) ++ var_names (fn_vars f))); let (e,m1) := do_alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) in - do m2 <- sem_bind_parameters e m1 f.(fn_params) vargs; + do m2 <- sem_bind_parameters w e m1 f.(fn_params) vargs; ret (State f f.(fn_body) k e m2) | Callstate (External ef _ _) vargs k m => - match do_external _ _ ge ef w vargs m with + match do_external ef w vargs m with | None => nil | Some(w',t,v,m') => (t, Returnstate v k m') :: nil end @@ -1721,9 +1933,11 @@ Ltac myinv := Hint Extern 3 => exact I. -Lemma do_step_sound: - forall w S t S', In (t, S') (do_step w S) -> Csem.step ge S t S'. -Proof with try (right; econstructor; eauto; fail). +Theorem do_step_sound: + forall w S t S', + In (t, S') (do_step w S) -> + Csem.step ge S t S' \/ (t = E0 /\ S' = Stuckstate /\ can_crash_world w S). +Proof with try (left; right; econstructor; eauto; fail). intros until S'. destruct S; simpl. (* State *) destruct s; myinv... @@ -1742,82 +1956,87 @@ Proof with try (right; econstructor; eauto; fail). destruct k; myinv... destruct v; myinv... (* expression reduces *) - destruct (step_expr e RV r m) as [ll|]_eqn; try contradiction. intros. - exploit list_in_map_inv; eauto. intros [[C rd] [A B]]. - generalize (step_expr_sound e r RV m). unfold reducts_ok. rewrite Heqr0. - destruct ll; try contradiction. intros SOUND. - exploit SOUND; eauto. intros [CTX [a [EQ RD]]]. subst r. - unfold expr_final_state in A. simpl in A. left. - destruct rd; inv A; simpl in RD. - apply step_lred. auto. apply step_expr_not_stuck; congruence. auto. - apply step_rred. auto. apply step_expr_not_stuck; congruence. auto. - destruct RD; subst m'. apply Csem.step_call. auto. apply step_expr_not_stuck; congruence. auto. + intros. exploit list_in_map_inv; eauto. intros [[C rd] [A B]]. + generalize (step_expr_sound e w r RV m). unfold reducts_ok. intros [P Q]. + exploit P; eauto. intros [a' [k' [CTX [EQ RD]]]]. + unfold expr_final_state in A. simpl in A. + destruct k'; destruct rd; inv A; simpl in RD; try contradiction. + (* lred *) + left; left; apply step_lred; auto. + (* stuck lred *) + exploit not_imm_safe_t; eauto. intros [R | R]; eauto. + (* rred *) + destruct RD. left; left; apply step_rred; auto. + (* callred *) + destruct RD; subst m'. left; left; apply step_call; eauto. + (* stuck rred *) + exploit not_imm_safe_t; eauto. intros [R | R]; eauto. (* callstate *) destruct fd; myinv. (* internal *) destruct (do_alloc_variables empty_env m (fn_params f ++ fn_vars f)) as [e m1]_eqn. - myinv. right; apply step_internal_function with m1. auto. + myinv. left; right; apply step_internal_function with m1. auto. change e with (fst (e,m1)). change m1 with (snd (e,m1)) at 2. rewrite <- Heqp. - apply do_alloc_variables_sound. apply sem_bind_parameters_sound; auto. + apply do_alloc_variables_sound. eapply sem_bind_parameters_sound; eauto. (* external *) - destruct p as [[[w' tr] v] m']. myinv. right; constructor. + destruct p as [[[w' tr] v] m']. myinv. left; right; constructor. eapply do_ef_external_sound; eauto. (* returnstate *) destruct k; myinv... +(* stuckstate *) + contradiction. Qed. Remark estep_not_val: forall f a k e m t S, estep ge (ExprState f a k e m) t S -> is_val a = None. Proof. intros. - assert (forall b from to C, context from to C -> (C = fun x => x) \/ is_val (C b) = None). + assert (forall b from to C, context from to C -> (from = to /\ C = fun x => x) \/ is_val (C b) = None). induction 1; simpl; auto. inv H. - destruct (H0 a0 _ _ _ H10). subst. inv H8; auto. auto. - destruct (H0 a0 _ _ _ H10). subst. inv H8; auto. auto. - destruct (H0 a0 _ _ _ H10). subst. inv H8; auto. auto. + destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto. + destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto. + destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto. + destruct (H0 a0 _ _ _ H8) as [[A B] | A]. subst. destruct a0; auto. elim H9. constructor. auto. Qed. -Lemma do_step_complete: +Theorem do_step_complete: forall w S t S' w', possible_trace w t w' -> Csem.step ge S t S' -> In (t, S') (do_step w S). Proof with (unfold ret; auto with coqlib). - intros until w'; intro PT; intros. + intros until w'; intros PT H. destruct H. (* Expression step *) inversion H; subst; exploit estep_not_val; eauto; intro NOTVAL. (* lred *) unfold do_step; rewrite NOTVAL. - destruct (step_expr e RV (C a) m) as [ll|]_eqn. change (E0, ExprState f (C a') k e m') with (expr_final_state f k e (C, Lred a' m')). apply in_map. - generalize (step_expr_context e _ _ _ H2 a m). unfold reducts_incl. - rewrite Heqr. destruct (step_expr e LV a m) as [ll'|]_eqn; try tauto. - intro. replace C with (fun x => C x). apply H3. - rewrite (lred_topred _ _ _ _ _ H0) in Heqr0. inv Heqr0. auto with coqlib. + generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl. + intro. replace C with (fun x => C x). apply H2. + rewrite (lred_topred _ _ _ _ _ _ H0). unfold topred; auto with coqlib. apply extensionality; auto. - exploit not_stuck_step_expr; eauto. (* rred *) unfold do_step; rewrite NOTVAL. - destruct (step_expr e RV (C a) m) as [ll|]_eqn. - change (E0, ExprState f (C a') k e m') with (expr_final_state f k e (C, Rred a' m')). + change (t, ExprState f (C a') k e m') with (expr_final_state f k e (C, Rred a' m' t)). apply in_map. - generalize (step_expr_context e _ _ _ H2 a m). unfold reducts_incl. - rewrite Heqr. destruct (step_expr e RV a m) as [ll'|]_eqn; try tauto. - intro. replace C with (fun x => C x). apply H3. - rewrite (rred_topred _ _ _ _ _ H0) in Heqr0. inv Heqr0. auto with coqlib. + generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl. + intro. replace C with (fun x => C x). apply H2. + rewrite (rred_topred _ _ _ _ _ _ _ _ H0 PT). unfold topred; auto with coqlib. apply extensionality; auto. - exploit not_stuck_step_expr; eauto. (* callred *) unfold do_step; rewrite NOTVAL. - destruct (step_expr e RV (C a) m) as [ll|]_eqn. change (E0, Callstate fd vargs (Kcall f e C ty k) m) with (expr_final_state f k e (C, Callred fd vargs ty m)). apply in_map. - generalize (step_expr_context e _ _ _ H2 a m). unfold reducts_incl. - rewrite Heqr. destruct (step_expr e RV a m) as [ll'|]_eqn; try tauto. - intro. replace C with (fun x => C x). apply H3. - rewrite (callred_topred _ _ _ _ _ _ H0) in Heqr0. inv Heqr0. auto with coqlib. + generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl. + intro. replace C with (fun x => C x). apply H2. + rewrite (callred_topred _ _ _ _ _ _ _ H0). unfold topred; auto with coqlib. apply extensionality; auto. - exploit not_stuck_step_expr; eauto. +(* stuck *) + exploit not_imm_safe_stuck_red. eauto. red; intros; elim H1. eapply imm_safe_t_imm_safe. eauto. + instantiate (1 := w). intros [C' IN]. + simpl do_step. rewrite NOTVAL. + change (E0, Stuckstate) with (expr_final_state f k e (C', Stuckred)). + apply in_map. auto. (* Statement step *) inv H; simpl... @@ -1835,13 +2054,13 @@ Proof with (unfold ret; auto with coqlib). destruct H0; subst x... rewrite H0... rewrite H0; rewrite H1... - rewrite pred_dec_true; auto. rewrite H2. red in H0. destruct k; try contradiction... + rewrite H1. rewrite dec_eq_true. rewrite H2. red in H0. destruct k; try contradiction... destruct H0; subst x... rewrite H0... (* Call step *) rewrite pred_dec_true; auto. rewrite (do_alloc_variables_complete _ _ _ _ _ H1). - rewrite (sem_bind_parameters_complete _ _ _ _ _ H2)... + rewrite (sem_bind_parameters_complete _ _ _ _ _ _ H2)... exploit do_ef_external_complete; eauto. intro EQ; rewrite EQ. auto with coqlib. Qed. @@ -1854,7 +2073,7 @@ Definition do_initial_state (p: program): option (genv * state) := do m0 <- Genv.init_mem p; do b <- Genv.find_symbol ge p.(prog_main); do f <- Genv.find_funct_ptr ge b; - check (type_eq (type_of_fundef f) (Tfunction Tnil (Tint I32 Signed))); + check (type_eq (type_of_fundef f) (Tfunction Tnil type_int32s)); Some (ge, Callstate f nil Kstop m0). Definition at_final_state (S: state): option int := -- cgit v1.2.3