From 57d3627c69a812a037d2d4161941ce25d15082d1 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 15 Mar 2015 17:07:36 +0100 Subject: Revised semantics of comparisons between a pointer and 0. It used to be that a pointer value (Vptr) always compare unequal to the null pointer (Vint Int.zero). However, this may not be true in the final machine code when pointer addition overflows and wraps around to the bit pattern 0. This patch checks the validity of the pointer being compared with 0, and makes the comparison undefined if the pointer is out of bounds. Note: only the IA32 back-end was updated, ARM and PowerPC need updating. --- cfrontend/Cop.v | 3 --- cfrontend/Cshmgenproof.v | 1 - cfrontend/Ctyping.v | 1 - cfrontend/SimplLocalsproof.v | 3 --- 4 files changed, 8 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 4e572277..b6b75abe 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -273,7 +273,6 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := | cast_case_p2bool => match v with | Vint i => Some (Vint (cast_int_int IBool Signed i)) - | Vptr _ _ => Some (Vint Int.one) | _ => None end | cast_case_l2l => @@ -391,7 +390,6 @@ 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 => Some true | _ => None end | bool_case_l => @@ -426,7 +424,6 @@ 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 _ _ => Some Vfalse | _ => None end | bool_case_l => diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 7f61c657..847e4856 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -333,7 +333,6 @@ Proof. econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpu, Val.cmpu_bool. simpl. destruct (Int.eq i Int.zero); simpl; constructor. - exists Vtrue; split. econstructor; eauto with cshm. constructor. (* long *) econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. destruct (Int64.eq i Int64.zero); simpl; constructor. diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 43d34007..bdeeff2a 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -1390,7 +1390,6 @@ 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; auto with ty. destruct (Int64.eq i Int64.zero); constructor; auto with ty. - (* notint *) unfold sem_notint in SEM; DestructCases; auto with ty. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 5cf59d94..3364ec6a 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -267,11 +267,8 @@ Proof. constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto. constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. (* long *) destruct ty; try (destruct f); try discriminate. destruct v; inv H. constructor. -- cgit From daccc2928e6410c4e8c886ea7d019fd9a071b931 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 29 Mar 2015 19:57:16 +0200 Subject: Omission: forgot to treat pointer values in bool_of_val and sem_notbool. --- cfrontend/Cexec.v | 32 ++++++++++---------- cfrontend/Clight.v | 4 +-- cfrontend/ClightBigstep.v | 4 +-- cfrontend/Cop.v | 68 +++++++++++++++++++++++++++++++------------ cfrontend/Csem.v | 26 ++++++++--------- cfrontend/Cshmgenproof.v | 13 +++++++-- cfrontend/Cstrategy.v | 68 +++++++++++++++++++++---------------------- cfrontend/Ctyping.v | 5 ++-- cfrontend/Initializers.v | 8 ++--- cfrontend/Initializersproof.v | 47 ++++++++++++++++++------------ cfrontend/SimplExpr.v | 3 +- cfrontend/SimplExprproof.v | 24 ++++++++++----- 12 files changed, 182 insertions(+), 120 deletions(-) (limited to 'cfrontend') 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: -- cgit