diff options
| -rw-r--r-- | cfrontend/Cexec.v | 32 | ||||
| -rw-r--r-- | cfrontend/Clight.v | 4 | ||||
| -rw-r--r-- | cfrontend/ClightBigstep.v | 4 | ||||
| -rw-r--r-- | cfrontend/Cop.v | 68 | ||||
| -rw-r--r-- | cfrontend/Csem.v | 26 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 13 | ||||
| -rw-r--r-- | cfrontend/Cstrategy.v | 68 | ||||
| -rw-r--r-- | cfrontend/Ctyping.v | 5 | ||||
| -rw-r--r-- | cfrontend/Initializers.v | 8 | ||||
| -rw-r--r-- | cfrontend/Initializersproof.v | 47 | ||||
| -rw-r--r-- | cfrontend/SimplExpr.v | 3 | ||||
| -rw-r--r-- | cfrontend/SimplExprproof.v | 24 |
12 files changed, 182 insertions, 120 deletions
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index ed67286f..52e9eaac 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -785,7 +785,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Eunop op r1 ty => match is_val r1 with | Some(v1, ty1) => - do v <- sem_unary_operation op v1 ty1; + do v <- sem_unary_operation op v1 ty1 m; topred (Rred "red_unop" (Eval v ty) m E0) | None => incontext (fun x => Eunop op x ty) (step_expr RV r1 m) @@ -810,7 +810,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Eseqand r1 r2 ty => match is_val r1 with | Some(v1, ty1) => - do b <- bool_val v1 ty1; + do b <- bool_val v1 ty1 m; if b then topred (Rred "red_seqand_true" (Eparen r2 type_bool ty) m E0) else topred (Rred "red_seqand_false" (Eval (Vint Int.zero) ty) m E0) | None => @@ -819,7 +819,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Eseqor r1 r2 ty => match is_val r1 with | Some(v1, ty1) => - do b <- bool_val v1 ty1; + do b <- bool_val v1 ty1 m; if b then topred (Rred "red_seqor_true" (Eval (Vint Int.one) ty) m E0) else topred (Rred "red_seqor_false" (Eparen r2 type_bool ty) m E0) | None => @@ -828,7 +828,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Econdition r1 r2 r3 ty => match is_val r1 with | Some(v1, ty1) => - do b <- bool_val v1 ty1; + do b <- bool_val v1 ty1 m; topred (Rred "red_condition" (Eparen (if b then r2 else r3) ty ty) m E0) | None => incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m) @@ -987,17 +987,17 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | 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 + exists v, sem_unary_operation op v1 ty1 m = Some v | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v | Ecast (Eval v1 ty1) ty => exists v, sem_cast v1 ty1 ty = Some v | Eseqand (Eval v1 ty1) r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Eseqor (Eval v1 ty1) r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Econdition (Eval v1 ty1) r1 r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = 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' @@ -1409,7 +1409,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* unop *) destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (sem_unary_operation op v ty') as [v'|] eqn:?... + destruct (sem_unary_operation op v ty' m) as [v'|] eqn:?... apply topred_ok; auto. split. apply red_unop; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. @@ -1433,7 +1433,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* seqand *) destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (bool_val v ty') as [v'|] eqn:?... destruct v'. + destruct (bool_val v ty' m) as [v'|] eqn:?... destruct v'. apply topred_ok; auto. split. eapply red_seqand_true; eauto. exists w; constructor. apply topred_ok; auto. split. eapply red_seqand_false; eauto. exists w; constructor. (* depth *) @@ -1441,7 +1441,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* seqor *) destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (bool_val v ty') as [v'|] eqn:?... destruct v'. + destruct (bool_val v ty' m) as [v'|] eqn:?... destruct v'. apply topred_ok; auto. split. eapply red_seqor_true; eauto. exists w; constructor. apply topred_ok; auto. split. eapply red_seqor_false; eauto. exists w; constructor. (* depth *) @@ -1449,7 +1449,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* condition *) destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (bool_val v ty') as [v'|] eqn:?... + destruct (bool_val v ty' m) as [v'|] eqn:?... apply topred_ok; auto. split. eapply red_condition; eauto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. @@ -1973,20 +1973,20 @@ Definition do_step (w: world) (s: state) : list transition := match k with | Kdo k => ret "step_do_2" (State f Sskip k e m ) | Kifthenelse s1 s2 k => - do b <- bool_val v ty; + do b <- bool_val v ty m; ret "step_ifthenelse_2" (State f (if b then s1 else s2) k e m) | Kwhile1 x s k => - do b <- bool_val v ty; + do b <- bool_val v ty m; if b then ret "step_while_true" (State f s (Kwhile2 x s k) e m) else ret "step_while_false" (State f Sskip k e m) | Kdowhile2 x s k => - do b <- bool_val v ty; + do b <- bool_val v ty m; if b then ret "step_dowhile_true" (State f (Sdowhile x s) k e m) else ret "step_dowhile_false" (State f Sskip k e m) | Kfor2 a2 a3 s k => - do b <- bool_val v ty; + do b <- bool_val v ty m; if b then ret "step_for_true" (State f s (Kfor3 a2 a3 s k) e m) else ret "step_for_false" (State f Sskip k e m) diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 7a45b453..77511b2c 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -403,7 +403,7 @@ Inductive eval_expr: expr -> val -> Prop := eval_expr (Eaddrof a ty) (Vptr loc ofs) | eval_Eunop: forall op a ty v1 v, eval_expr a v1 -> - sem_unary_operation op v1 (typeof a) = Some v -> + sem_unary_operation op v1 (typeof a) m = Some v -> eval_expr (Eunop op a ty) v | eval_Ebinop: forall op a1 a2 ty v1 v2 v, eval_expr a1 v1 -> @@ -620,7 +620,7 @@ Inductive step: state -> trace -> state -> Prop := | step_ifthenelse: forall f a s1 s2 k e le m v1 b, eval_expr e le m a v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m = Some b -> step (State f (Sifthenelse a s1 s2) k e le m) E0 (State f (if b then s1 else s2) k e le m) diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v index 5b092db7..ac8931e5 100644 --- a/cfrontend/ClightBigstep.v +++ b/cfrontend/ClightBigstep.v @@ -115,7 +115,7 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> t1 le1 m1 out | exec_Sifthenelse: forall e le m a s1 s2 v1 b t le' m' out, eval_expr ge e le m a v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m = Some b -> exec_stmt e le m (if b then s1 else s2) t le' m' out -> exec_stmt e le m (Sifthenelse a s1 s2) t le' m' out @@ -204,7 +204,7 @@ CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Pro execinf_stmt e le m (Ssequence s1 s2) (t1 *** t2) | execinf_Sifthenelse: forall e le m a s1 s2 v1 b t, eval_expr ge e le m a v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m = Some b -> execinf_stmt e le m (if b then s1 else s2) t -> execinf_stmt e le m (Sifthenelse a s1 s2) t | execinf_Sloop_body1: forall e le m s1 s2 t, diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index b6b75abe..2a5d17bc 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -370,7 +370,7 @@ Definition classify_bool (ty: type) : classify_bool_cases := considered as true. The integer zero (which also represents the null pointer) and the float 0.0 are false. *) -Definition bool_val (v: val) (t: type) : option bool := +Definition bool_val (v: val) (t: type) (m: mem) : option bool := match classify_bool t with | bool_case_i => match v with @@ -390,6 +390,7 @@ Definition bool_val (v: val) (t: type) : option bool := | bool_case_p => match v with | Vint n => Some (negb (Int.eq n Int.zero)) + | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some true else None | _ => None end | bool_case_l => @@ -404,7 +405,7 @@ Definition bool_val (v: val) (t: type) : option bool := (** *** Boolean negation *) -Definition sem_notbool (v: val) (ty: type) : option val := +Definition sem_notbool (v: val) (ty: type) (m: mem): option val := match classify_bool ty with | bool_case_i => match v with @@ -424,6 +425,7 @@ Definition sem_notbool (v: val) (ty: type) : option val := | bool_case_p => match v with | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) + | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some Vfalse else None | _ => None end | bool_case_l => @@ -970,9 +972,9 @@ Definition sem_switch_arg (v: val) (ty: type): option Z := (** * Combined semantics of unary and binary operators *) Definition sem_unary_operation - (op: unary_operation) (v: val) (ty: type): option val := + (op: unary_operation) (v: val) (ty: type) (m: mem): option val := match op with - | Onotbool => sem_notbool v ty + | Onotbool => sem_notbool v ty m | Onotint => sem_notint v ty | Oneg => sem_neg v ty | Oabsfloat => sem_absfloat v ty @@ -1088,15 +1090,17 @@ Proof. - econstructor; eauto. Qed. -Lemma sem_unary_operation_inject: +Lemma sem_unary_operation_inj: forall op v1 ty v tv1, - sem_unary_operation op v1 ty = Some v -> + sem_unary_operation op v1 ty m = Some v -> val_inject f v1 tv1 -> - exists tv, sem_unary_operation op tv1 ty = Some tv /\ val_inject f v tv. + exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ val_inject f v tv. Proof. unfold sem_unary_operation; intros. destruct op. (* notbool *) unfold sem_notbool in *; destruct (classify_bool ty); inv H0; inv H; TrivialInject. + destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VP; inv H2. + erewrite weak_valid_pointer_inj by eauto. TrivialInject. (* notint *) unfold sem_notint in *; destruct (classify_notint ty); inv H0; inv H; TrivialInject. (* neg *) @@ -1262,18 +1266,31 @@ Proof. - eapply sem_cmp_inj; eauto. Qed. -Lemma bool_val_inject: +Lemma bool_val_inj: forall v ty b tv, - bool_val v ty = Some b -> + bool_val v ty m = Some b -> val_inject f v tv -> - bool_val tv ty = Some b. + bool_val tv ty m' = Some b. Proof. unfold bool_val; intros. - destruct (classify_bool ty); inv H0; congruence. + destruct (classify_bool ty); inv H0; try congruence. + destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VP; inv H. + erewrite weak_valid_pointer_inj by eauto. auto. Qed. End GENERIC_INJECTION. +Lemma sem_unary_operation_inject: + forall f m m' op v1 ty1 v tv1, + sem_unary_operation op v1 ty1 m = Some v -> + val_inject f v1 tv1 -> + Mem.inject f m m' -> + exists tv, sem_unary_operation op tv1 ty1 m' = Some tv /\ val_inject f v tv. +Proof. + intros. eapply sem_unary_operation_inj; eauto. + intros; eapply Mem.weak_valid_pointer_inject_val; eauto. +Qed. + Lemma sem_binary_operation_inject: forall f m m' cenv op v1 ty1 v2 ty2 v tv1 tv2, sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v -> @@ -1288,6 +1305,17 @@ Proof. intros; eapply Mem.different_pointers_inject; eauto. Qed. +Lemma bool_val_inject: + forall f m m' v ty b tv, + bool_val v ty m = Some b -> + val_inject f v tv -> + Mem.inject f m m' -> + bool_val tv ty m' = Some b. +Proof. + intros. eapply bool_val_inj; eauto. + intros; eapply Mem.weak_valid_pointer_inject_val; eauto. +Qed. + (** * Some properties of operator semantics *) (** This section collects some common-sense properties about the type @@ -1298,9 +1326,12 @@ Qed. (** Relation between Boolean value and casting to [_Bool] type. *) Lemma cast_bool_bool_val: - forall v t, - sem_cast v t (Tint IBool Signed noattr) = - match bool_val v t with None => None | Some b => Some(Val.of_bool b) end. + forall v t m, + match sem_cast v t (Tint IBool Signed noattr), bool_val v t m with + | Some v', Some b => v' = Val.of_bool b + | Some v', None => False + | None, _ => True + end. Proof. intros. assert (A: classify_bool t = @@ -1334,12 +1365,13 @@ Qed. (** Relation between Boolean value and Boolean negation. *) Lemma notbool_bool_val: - forall v t, - sem_notbool v t = - match bool_val v t with None => None | Some b => Some(Val.of_bool (negb b)) end. + forall v t m, + sem_notbool v t m = + match bool_val v t m with None => None | Some b => Some(Val.of_bool (negb b)) end. Proof. intros. unfold sem_notbool, bool_val. - destruct (classify_bool t); auto; destruct v; auto; rewrite negb_involutive; auto. + destruct (classify_bool t); auto; destruct v; auto; rewrite ? negb_involutive; auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. Qed. (** Relation with the arithmetic conversions of ISO C99, section 6.3.1 *) diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index fafbf29f..3e9017c9 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -241,7 +241,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := rred (Eaddrof (Eloc b ofs ty1) ty) m E0 (Eval (Vptr b ofs) ty) m | red_unop: forall op v1 ty1 ty m v, - sem_unary_operation op v1 ty1 = Some v -> + sem_unary_operation op v1 ty1 m = Some v -> rred (Eunop op (Eval v1 ty1) ty) m E0 (Eval v ty) m | red_binop: forall op v1 ty1 v2 ty2 ty m v, @@ -253,23 +253,23 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := rred (Ecast (Eval v1 ty1) ty) m E0 (Eval v ty) m | red_seqand_true: forall v1 ty1 r2 ty m, - bool_val v1 ty1 = Some true -> + bool_val v1 ty1 m = Some true -> rred (Eseqand (Eval v1 ty1) r2 ty) m E0 (Eparen r2 type_bool ty) m | red_seqand_false: forall v1 ty1 r2 ty m, - bool_val v1 ty1 = Some false -> + bool_val v1 ty1 m = Some false -> rred (Eseqand (Eval v1 ty1) r2 ty) m E0 (Eval (Vint Int.zero) ty) m | red_seqor_true: forall v1 ty1 r2 ty m, - bool_val v1 ty1 = Some true -> + bool_val v1 ty1 m = Some true -> rred (Eseqor (Eval v1 ty1) r2 ty) m E0 (Eval (Vint Int.one) ty) m | red_seqor_false: forall v1 ty1 r2 ty m, - bool_val v1 ty1 = Some false -> + bool_val v1 ty1 m = Some false -> rred (Eseqor (Eval v1 ty1) r2 ty) m E0 (Eparen r2 type_bool ty) m | red_condition: forall v1 ty1 r1 r2 ty b m, - bool_val v1 ty1 = Some b -> + bool_val v1 ty1 m = Some b -> rred (Econdition (Eval v1 ty1) r1 r2 ty) m E0 (Eparen (if b then r1 else r2) ty ty) m | red_sizeof: forall ty1 ty m, @@ -633,7 +633,7 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (State f (Sifthenelse a s1 s2) k e m) E0 (ExprState f a (Kifthenelse s1 s2 k) e m) | step_ifthenelse_2: forall f v ty s1 s2 k e m b, - bool_val v ty = Some b -> + bool_val v ty m = Some b -> sstep (ExprState f (Eval v ty) (Kifthenelse s1 s2 k) e m) E0 (State f (if b then s1 else s2) k e m) @@ -641,11 +641,11 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (State f (Swhile x s) k e m) E0 (ExprState f x (Kwhile1 x s k) e m) | step_while_false: forall f v ty x s k e m, - bool_val v ty = Some false -> + bool_val v ty m = Some false -> sstep (ExprState f (Eval v ty) (Kwhile1 x s k) e m) E0 (State f Sskip k e m) | step_while_true: forall f v ty x s k e m , - bool_val v ty = Some true -> + bool_val v ty m = Some true -> sstep (ExprState f (Eval v ty) (Kwhile1 x s k) e m) E0 (State f s (Kwhile2 x s k) e m) | step_skip_or_continue_while: forall f s0 x s k e m, @@ -664,11 +664,11 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (State f s0 (Kdowhile1 x s k) e m) E0 (ExprState f x (Kdowhile2 x s k) e m) | step_dowhile_false: forall f v ty x s k e m, - bool_val v ty = Some false -> + bool_val v ty m = Some false -> sstep (ExprState f (Eval v ty) (Kdowhile2 x s k) e m) E0 (State f Sskip k e m) | step_dowhile_true: forall f v ty x s k e m, - bool_val v ty = Some true -> + bool_val v ty m = Some true -> sstep (ExprState f (Eval v ty) (Kdowhile2 x s k) e m) E0 (State f (Sdowhile x s) k e m) | step_break_dowhile: forall f a s k e m, @@ -683,11 +683,11 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (State f (Sfor Sskip a2 a3 s) k e m) E0 (ExprState f a2 (Kfor2 a2 a3 s k) e m) | step_for_false: forall f v ty a2 a3 s k e m, - bool_val v ty = Some false -> + bool_val v ty m = Some false -> sstep (ExprState f (Eval v ty) (Kfor2 a2 a3 s k) e m) E0 (State f Sskip k e m) | step_for_true: forall f v ty a2 a3 s k e m, - bool_val v ty = Some true -> + bool_val v ty m = Some true -> sstep (ExprState f (Eval v ty) (Kfor2 a2 a3 s k) e m) E0 (State f s (Kfor3 a2 a3 s k) e m) | step_skip_or_continue_for3: forall f x a2 a3 s k e m, diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 847e4856..025d7b66 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -311,7 +311,7 @@ Qed. Lemma make_boolean_correct: forall e le m a v ty b, eval_expr ge e le m a v -> - bool_val v ty = Some b -> + bool_val v ty m = Some b -> exists vb, eval_expr ge e le m (make_boolean a ty) vb /\ Val.bool_of_val vb b. @@ -333,6 +333,10 @@ Proof. econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpu, Val.cmpu_bool. simpl. destruct (Int.eq i Int.zero); simpl; constructor. + econstructor; split. econstructor; eauto with cshm. simpl. eauto. + destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i)) eqn:V; inv H2. + unfold Val.cmpu, Val.cmpu_bool. simpl. + unfold Mem.weak_valid_pointer in V; rewrite V. constructor. (* long *) econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. destruct (Int64.eq i Int64.zero); simpl; constructor. @@ -365,13 +369,16 @@ Qed. Lemma make_notbool_correct: forall a tya c va v e le m, - sem_notbool va tya = Some v -> + sem_notbool va tya m = Some v -> make_notbool a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. unfold sem_notbool, make_notbool; intros until m; intros SEM MAKE EV1; destruct (classify_bool tya); inv MAKE; destruct va; inv SEM; eauto with cshm. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:V; inv H0. + econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. + unfold Mem.weak_valid_pointer in V; rewrite V. auto. Qed. Lemma make_notint_correct: @@ -632,7 +639,7 @@ Qed. Lemma transl_unop_correct: forall op a tya c va v e le m, transl_unop op a tya = OK c -> - sem_unary_operation op va tya = Some v -> + sem_unary_operation op va tya m = Some v -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 3b0eb84f..b082ea56 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -122,7 +122,7 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs) | esr_unop: forall op r1 ty v1 v, eval_simple_rvalue r1 v1 -> - sem_unary_operation op v1 (typeof r1) = Some v -> + sem_unary_operation op v1 (typeof r1) m = Some v -> eval_simple_rvalue (Eunop op r1 ty) v | esr_binop: forall op r1 r2 ty v1 v2 v, eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 -> @@ -249,33 +249,33 @@ Inductive estep: state -> trace -> state -> Prop := | step_seqand_true: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some true -> + bool_val v (typeof r1) m = Some true -> estep (ExprState f (C (Eseqand r1 r2 ty)) k e m) E0 (ExprState f (C (Eparen r2 type_bool ty)) k e m) | step_seqand_false: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some false -> + bool_val v (typeof r1) m = Some false -> estep (ExprState f (C (Eseqand r1 r2 ty)) k e m) E0 (ExprState f (C (Eval (Vint Int.zero) ty)) k e m) | step_seqor_true: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some true -> + bool_val v (typeof r1) m = Some true -> estep (ExprState f (C (Eseqor r1 r2 ty)) k e m) E0 (ExprState f (C (Eval (Vint Int.one) ty)) k e m) | step_seqor_false: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some false -> + bool_val v (typeof r1) m = Some false -> estep (ExprState f (C (Eseqor r1 r2 ty)) k e m) E0 (ExprState f (C (Eparen r2 type_bool ty)) k e m) | step_condition: forall f C r1 r2 r3 ty k e m v b, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some b -> + bool_val v (typeof r1) m = Some b -> estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m) E0 (ExprState f (C (Eparen (if b then r2 else r3) ty ty)) k e m) @@ -536,17 +536,17 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Evalof (Eloc b ofs ty') ty => ty' = ty /\ exists t, exists v, deref_loc ge ty m b ofs t v | Eunop op (Eval v1 ty1) ty => - exists v, sem_unary_operation op v1 ty1 = Some v + exists v, sem_unary_operation op v1 ty1 m = Some v | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v | Ecast (Eval v1 ty1) ty => exists v, sem_cast v1 ty1 ty = Some v | Eseqand (Eval v1 ty1) r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Eseqor (Eval v1 ty1) r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Econdition (Eval v1 ty1) r1 r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty => exists v, exists m', exists t, ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m' @@ -1695,27 +1695,27 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m RV (Ecast a ty) t m' (Ecast a' ty) | eval_seqand_true: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some true -> + bool_val v1 (typeof a1) m' = Some true -> eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 -> sem_cast v2 (typeof a2) type_bool = Some v -> eval_expr e m RV (Eseqand a1 a2 ty) (t1**t2) m'' (Eval v ty) | eval_seqand_false: forall e m a1 a2 ty t1 m' a1' v1, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some false -> + bool_val v1 (typeof a1) m' = Some false -> eval_expr e m RV (Eseqand a1 a2 ty) t1 m' (Eval (Vint Int.zero) ty) | eval_seqor_false: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some false -> + bool_val v1 (typeof a1) m' = Some false -> eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 -> sem_cast v2 (typeof a2) type_bool = Some v -> eval_expr e m RV (Eseqor a1 a2 ty) (t1**t2) m'' (Eval v ty) | eval_seqor_true: forall e m a1 a2 ty t1 m' a1' v1, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some true -> + bool_val v1 (typeof a1) m' = Some true -> eval_expr e m RV (Eseqor a1 a2 ty) t1 m' (Eval (Vint Int.one) ty) | eval_condition: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 m'' a' v' b v, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some b -> + bool_val v1 (typeof a1) m' = Some b -> eval_expr e m' RV (if b then a2 else a3) t2 m'' a' -> eval_simple_rvalue ge e m'' a' v' -> sem_cast v' (typeof (if b then a2 else a3)) ty = Some v -> eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty) @@ -1801,7 +1801,7 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := t1 m1 out | exec_Sifthenelse: forall e m a s1 s2 t1 m1 v1 t2 m2 b out, eval_expression e m a t1 m1 v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m1 = Some b -> exec_stmt e m1 (if b then s1 else s2) t2 m2 out -> exec_stmt e m (Sifthenelse a s1 s2) (t1**t2) m2 out @@ -1820,19 +1820,19 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := E0 m Out_continue | exec_Swhile_false: forall e m a s t m' v, eval_expression e m a t m' v -> - bool_val v (typeof a) = Some false -> + bool_val v (typeof a) m' = Some false -> exec_stmt e m (Swhile a s) t m' Out_normal | exec_Swhile_stop: forall e m a s t1 m1 v t2 m2 out' out, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> exec_stmt e m1 s t2 m2 out' -> out_break_or_return out' out -> exec_stmt e m (Swhile a s) (t1**t2) m2 out | exec_Swhile_loop: forall e m a s t1 m1 v t2 m2 out1 t3 m3 out, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 (Swhile a s) t3 m3 out -> @@ -1842,7 +1842,7 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - bool_val v (typeof a) = Some false -> + bool_val v (typeof a) m2 = Some false -> exec_stmt e m (Sdowhile a s) (t1 ** t2) m2 Out_normal | exec_Sdowhile_stop: forall e m s a t m1 out1 out, @@ -1854,7 +1854,7 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m2 = Some true -> exec_stmt e m2 (Sdowhile a s) t3 m3 out -> exec_stmt e m (Sdowhile a s) (t1 ** t2 ** t3) m3 out @@ -1865,19 +1865,19 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := (t1 ** t2) m2 out | exec_Sfor_false: forall e m s a2 a3 t m' v, eval_expression e m a2 t m' v -> - bool_val v (typeof a2) = Some false -> + bool_val v (typeof a2) m' = Some false -> exec_stmt e m (Sfor Sskip a2 a3 s) t m' Out_normal | exec_Sfor_stop: forall e m s a2 a3 t1 m1 v t2 m2 out1 out, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_break_or_return out1 out -> exec_stmt e m (Sfor Sskip a2 a3 s) (t1 ** t2) m2 out | exec_Sfor_loop: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3 m3 t4 m4 out, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 a3 t3 m3 Out_normal -> @@ -1952,7 +1952,7 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_expr e m RV (Eseqand a1 a2 ty) t1 | evalinf_seqand_2: forall e m a1 a2 ty t1 m' a1' v1 t2, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some true -> + bool_val v1 (typeof a1) m' = Some true -> evalinf_expr e m' RV a2 t2 -> evalinf_expr e m RV (Eseqand a1 a2 ty) (t1***t2) | evalinf_seqor: forall e m a1 a2 ty t1, @@ -1960,7 +1960,7 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_expr e m RV (Eseqor a1 a2 ty) t1 | evalinf_seqor_2: forall e m a1 a2 ty t1 m' a1' v1 t2, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some false -> + bool_val v1 (typeof a1) m' = Some false -> evalinf_expr e m' RV a2 t2 -> evalinf_expr e m RV (Eseqor a1 a2 ty) (t1***t2) | evalinf_condition: forall e m a1 a2 a3 ty t1, @@ -1968,7 +1968,7 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_expr e m RV (Econdition a1 a2 a3 ty) t1 | evalinf_condition_2: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 b, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some b -> + bool_val v1 (typeof a1) m' = Some b -> evalinf_expr e m' RV (if b then a2 else a3) t2 -> evalinf_expr e m RV (Econdition a1 a2 a3 ty) (t1***t2) | evalinf_assign_left: forall e m a1 t1 a2 ty, @@ -2039,7 +2039,7 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Sifthenelse a s1 s2) t1 | execinf_Sifthenelse: forall e m a s1 s2 t1 m1 v1 t2 b, eval_expression e m a t1 m1 v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m1 = Some b -> execinf_stmt e m1 (if b then s1 else s2) t2 -> execinf_stmt e m (Sifthenelse a s1 s2) (t1***t2) | execinf_Sreturn_some: forall e m a t, @@ -2050,12 +2050,12 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Swhile a s) t1 | execinf_Swhile_body: forall e m a s t1 m1 v t2, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> execinf_stmt e m1 s t2 -> execinf_stmt e m (Swhile a s) (t1***t2) | execinf_Swhile_loop: forall e m a s t1 m1 v t2 m2 out1 t3, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> execinf_stmt e m2 (Swhile a s) t3 -> @@ -2072,7 +2072,7 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m2 = Some true -> execinf_stmt e m2 (Sdowhile a s) t3 -> execinf_stmt e m (Sdowhile a s) (t1***t2***t3) | execinf_Sfor_start_1: forall e m s a1 a2 a3 t1, @@ -2087,19 +2087,19 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Sfor Sskip a2 a3 s) t | execinf_Sfor_body: forall e m s a2 a3 t1 m1 v t2, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> execinf_stmt e m1 s t2 -> execinf_stmt e m (Sfor Sskip a2 a3 s) (t1***t2) | execinf_Sfor_next: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> execinf_stmt e m2 a3 t3 -> execinf_stmt e m (Sfor Sskip a2 a3 s) (t1***t2***t3) | execinf_Sfor_loop: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3 m3 t4, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 a3 t3 m3 Out_normal -> diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index bdeeff2a..2582fff8 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -1376,9 +1376,9 @@ Proof. Qed. Lemma pres_sem_unop: - forall op ty1 ty v1 v, + forall op ty1 ty v1 m v, type_unop op ty1 = OK ty -> - sem_unary_operation op v1 ty1 = Some v -> + sem_unary_operation op v1 ty1 m = Some v -> wt_val v1 ty1 -> wt_val v ty. Proof. @@ -1390,6 +1390,7 @@ Proof. destruct (Float.cmp Ceq f Float.zero); constructor; auto with ty. destruct (Float32.cmp Ceq f Float32.zero); constructor; auto with ty. destruct (Int.eq i Int.zero); constructor; auto with ty. + constructor. constructor. destruct (Int64.eq i Int64.zero); constructor; auto with ty. - (* notint *) unfold sem_notint in SEM; DestructCases; auto with ty. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 025960d7..7af4792a 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -74,7 +74,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := constval ce l | Eunop op r1 ty => do v1 <- constval ce r1; - match sem_unary_operation op v1 (typeof r1) with + match sem_unary_operation op v1 (typeof r1) Mem.empty with | Some v => OK v | None => Error(msg "undefined unary operation") end @@ -94,7 +94,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := | Eseqand r1 r2 ty => do v1 <- constval ce r1; do v2 <- constval ce r2; - match bool_val v1 (typeof r1) with + match bool_val v1 (typeof r1) Mem.empty with | Some true => do_cast v2 (typeof r2) type_bool | Some false => OK (Vint Int.zero) | None => Error(msg "undefined && operation") @@ -102,7 +102,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := | Eseqor r1 r2 ty => do v1 <- constval ce r1; do v2 <- constval ce r2; - match bool_val v1 (typeof r1) with + match bool_val v1 (typeof r1) Mem.empty with | Some false => do_cast v2 (typeof r2) type_bool | Some true => OK (Vint Int.one) | None => Error(msg "undefined || operation") @@ -111,7 +111,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := do v1 <- constval ce r1; do v2 <- constval ce r2; do v3 <- constval ce r3; - match bool_val v1 (typeof r1) with + match bool_val v1 (typeof r1) Mem.empty with | Some true => do_cast v2 (typeof r2) ty | Some false => do_cast v3 (typeof r3) ty | None => Error(msg "condition is undefined") diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 02a453cf..e0fcb210 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -112,7 +112,7 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs) | esr_unop: forall op r1 ty v1 v, eval_simple_rvalue r1 v1 -> - sem_unary_operation op v1 (typeof r1) = Some v -> + sem_unary_operation op v1 (typeof r1) m = Some v -> eval_simple_rvalue (Eunop op r1 ty) v | esr_binop: forall op r1 r2 ty v1 v2 v, eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 -> @@ -127,23 +127,23 @@ with eval_simple_rvalue: expr -> val -> Prop := | esr_alignof: forall ty1 ty, eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))) | esr_seqand_true: forall r1 r2 ty v1 v2 v3, - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some true -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true -> eval_simple_rvalue r2 v2 -> sem_cast v2 (typeof r2) type_bool = Some v3 -> eval_simple_rvalue (Eseqand r1 r2 ty) v3 | esr_seqand_false: forall r1 r2 ty v1, - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some false -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false -> eval_simple_rvalue (Eseqand r1 r2 ty) (Vint Int.zero) | esr_seqor_false: forall r1 r2 ty v1 v2 v3, - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some false -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false -> eval_simple_rvalue r2 v2 -> sem_cast v2 (typeof r2) type_bool = Some v3 -> eval_simple_rvalue (Eseqor r1 r2 ty) v3 | esr_seqor_true: forall r1 r2 ty v1, - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some true -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true -> eval_simple_rvalue (Eseqor r1 r2 ty) (Vint Int.one) | esr_condition: forall r1 r2 r3 ty v v1 b v', - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some b -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some b -> eval_simple_rvalue (if b then r2 else r3) v' -> sem_cast v' (typeof (if b then r2 else r3)) ty = Some v -> eval_simple_rvalue (Econdition r1 r2 r3 ty) v @@ -366,6 +366,15 @@ Proof. intros [v' [A B]]. congruence. Qed. +Lemma bool_val_match: + forall v ty b v' m, + bool_val v ty Mem.empty = Some b -> + val_inject inj v v' -> + bool_val v' ty m = Some b. +Proof. + intros. eapply bool_val_inj; eauto. intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate. +Qed. + (** Soundness of [constval] with respect to the big-step semantics *) Lemma constval_rvalue: @@ -390,8 +399,10 @@ Proof. (* addrof *) eauto. (* unop *) - destruct (sem_unary_operation op x (typeof r1)) as [v1'|] eqn:E; inv EQ0. - exploit sem_unary_operation_inject. eexact E. eauto. + destruct (sem_unary_operation op x (typeof r1) Mem.empty) as [v1'|] eqn:E; inv EQ0. + exploit (sem_unary_operation_inj inj Mem.empty m). + intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate. + eexact E. eauto. intros [v' [A B]]. congruence. (* binop *) destruct (sem_binary_operation ge op x (typeof r1) x0 (typeof r2) Mem.empty) as [v1'|] eqn:E; inv EQ2. @@ -409,24 +420,24 @@ Proof. (* alignof *) constructor. (* seqand *) - destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = true) by congruence. subst b. eapply sem_cast_match; eauto. - destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = false) by congruence. subst b. inv H2. auto. (* seqor *) - destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = false) by congruence. subst b. eapply sem_cast_match; eauto. - destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = true) by congruence. subst b. inv H2. auto. (* conditional *) - destruct (bool_val x (typeof r1)) as [b'|] eqn:E; inv EQ3. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b'|] eqn:E; inv EQ3. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b' = b) by congruence. subst b'. destruct b; eapply sem_cast_match; eauto. (* comma *) diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 36fe07ae..097dc589 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -18,6 +18,7 @@ Require Import Errors. Require Import Integers. Require Import Floats. Require Import Values. +Require Import Memory. Require Import AST. Require Import Ctypes. Require Import Cop. @@ -129,7 +130,7 @@ Function eval_simpl_expr (a: expr) : option val := Function makeif (a: expr) (s1 s2: statement) : statement := match eval_simpl_expr a with | Some v => - match bool_val v (typeof a) with + match bool_val v (typeof a) Mem.empty with | Some b => if b then s1 else s2 | None => Sifthenelse a s1 s2 end diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 74019061..7ef1cbe2 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -761,20 +761,30 @@ Proof. inv H; simpl; auto. Qed. +Lemma static_bool_val_sound: + forall v t m b, bool_val v t Mem.empty = Some b -> bool_val v t m = Some b. +Proof. + intros until b; unfold bool_val. destruct (classify_bool t); destruct v; auto. + intros E. unfold Mem.weak_valid_pointer, Mem.valid_pointer, proj_sumbool in E. + rewrite ! pred_dec_false in E by (apply Mem.perm_empty). discriminate. +Qed. + Lemma step_makeif: forall f a s1 s2 k e le m v1 b, eval_expr tge e le m a v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m = Some b -> star step1 tge (State f (makeif a s1 s2) k e le m) E0 (State f (if b then s1 else s2) k e le m). Proof. intros. functional induction (makeif a s1 s2). - exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v. - rewrite e1 in H0. inv H0. constructor. - exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v. - rewrite e1 in H0. inv H0. constructor. - apply star_one. eapply step_ifthenelse; eauto. - apply star_one. eapply step_ifthenelse; eauto. +- exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v. + assert (bool_val v1 (typeof a) m = Some true) by (apply static_bool_val_sound; auto). + replace b with true by congruence. constructor. +- exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v. + assert (bool_val v1 (typeof a) m = Some false) by (apply static_bool_val_sound; auto). + replace b with false by congruence. constructor. +- apply star_one. eapply step_ifthenelse; eauto. +- apply star_one. eapply step_ifthenelse; eauto. Qed. Lemma step_make_set: |