Make casts of pointers to _Bool semantically well defined (again).

In compCert 2.5 the semantics of pointer comparisons against the NULL pointer was made more accurate by making it undefined if the pointer is invalid (outside bounds).  Technical difficulties prevented this change from being propagated to the semantics of casts from pointer types to the _Bool type, which involves an implicit pointer comparison against NULL.  Hence, this kind of casts was temporarily given undefined semantics.

This commit makes pointer-to-_Bool casts semantically defined (again), provided the pointer is valid.  This reinstates the equivalence between casts to _Bool and comparisons != 0.  The technical difficulties mentioned above came from the translation of assignments in a value context in the SimplExpr pass.  The pass was lightly modified to work around the issue.

1 files changed, 40 insertions, 40 deletions

diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index b3cbacca..2650e0a8 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -130,7 +130,7 @@ with eval_simple_rvalue: expr -> val -> Prop :=
       eval_simple_rvalue (Ebinop op r1 r2 ty) v
   | esr_cast: forall ty r1 v1 v,
       eval_simple_rvalue r1 v1 ->
-      sem_cast v1 (typeof r1) ty = Some v ->
+      sem_cast v1 (typeof r1) ty m = Some v ->
       eval_simple_rvalue (Ecast r1 ty) v
   | esr_sizeof: forall ty1 ty,
       eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1)))
@@ -141,7 +141,7 @@ Inductive eval_simple_list: exprlist -> typelist -> list val -> Prop :=
   | esrl_nil:
       eval_simple_list Enil Tnil nil
   | esrl_cons: forall r rl ty tyl v vl v',
-      eval_simple_rvalue r v' -> sem_cast v' (typeof r) ty = Some v ->
+      eval_simple_rvalue r v' -> sem_cast v' (typeof r) ty m = Some v ->
       eval_simple_list rl tyl vl ->
       eval_simple_list (Econs r rl) (Tcons ty tyl) (v :: vl).
 
@@ -283,7 +283,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       leftcontext RV RV C ->
       eval_simple_lvalue e m l b ofs ->
       eval_simple_rvalue e m r v ->
-      sem_cast v (typeof r) (typeof l) = Some v' ->
+      sem_cast v (typeof r) (typeof l) m = Some v' ->
       assign_loc ge (typeof l) m b ofs v' t m' ->
       ty = typeof l ->
       estep (ExprState f (C (Eassign l r ty)) k e m)
@@ -295,7 +295,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       deref_loc ge (typeof l) m b ofs t1 v1 ->
       eval_simple_rvalue e m r v2 ->
       sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m = Some v3 ->
-      sem_cast v3 tyres (typeof l) = Some v4 ->
+      sem_cast v3 tyres (typeof l) m = Some v4 ->
       assign_loc ge (typeof l) m b ofs v4 t2 m' ->
       ty = typeof l ->
       t = t1 ** t2 ->
@@ -310,7 +310,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       match sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m with
       | None => True
       | Some v3 =>
-          match sem_cast v3 tyres (typeof l) with
+          match sem_cast v3 tyres (typeof l) m with
           | None => True
           | Some v4 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v4 t2 m')
           end
@@ -323,8 +323,8 @@ Inductive estep: state -> trace -> state -> Prop :=
       leftcontext RV RV C ->
       eval_simple_lvalue e m l b ofs ->
       deref_loc ge ty m b ofs t1 v1 ->
-      sem_incrdecr ge id v1 ty = Some v2 ->
-      sem_cast v2 (incrdecr_type ty) ty = Some v3 ->
+      sem_incrdecr ge id v1 ty m = Some v2 ->
+      sem_cast v2 (incrdecr_type ty) ty m = Some v3 ->
       assign_loc ge ty m b ofs v3 t2 m' ->
       ty = typeof l ->
       t = t1 ** t2 ->
@@ -335,10 +335,10 @@ Inductive estep: state -> trace -> state -> Prop :=
       leftcontext RV RV C ->
       eval_simple_lvalue e m l b ofs ->
       deref_loc ge ty m b ofs t v1 ->
-      match sem_incrdecr ge id v1 ty with
+      match sem_incrdecr ge id v1 ty m with
       | None => True
       | Some v2 =>
-          match sem_cast v2 (incrdecr_type ty) ty with
+          match sem_cast v2 (incrdecr_type ty) ty m with
           | None => True
           | Some v3 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v3 t2 m')
           end
@@ -357,7 +357,7 @@ Inductive estep: state -> trace -> state -> Prop :=
   | step_paren: forall f C r tycast ty k e m v1 v,
       leftcontext RV RV C ->
       eval_simple_rvalue e m r v1 ->
-      sem_cast v1 (typeof r) tycast = Some v ->
+      sem_cast v1 (typeof r) tycast m = Some v ->
       estep (ExprState f (C (Eparen r tycast ty)) k e m)
          E0 (ExprState f (C (Eval v ty)) k e m)
 
@@ -472,7 +472,7 @@ Proof.
 Qed.
 
 Lemma callred_kind:
-  forall a fd args ty, callred ge a fd args ty -> expr_kind a = RV.
+  forall a m fd args ty, callred ge a m fd args ty -> expr_kind a = RV.
 Proof.
   induction 1; auto.
 Qed.
@@ -540,7 +540,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | 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
+      exists v, sem_cast v1 ty1 ty m = Some v
   | Eseqand (Eval v1 ty1) r2 ty =>
       exists b, bool_val v1 ty1 m = Some b
   | Eseqor (Eval v1 ty1) r2 ty =>
@@ -549,7 +549,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
       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'
+      ty = ty1 /\ sem_cast v2 ty2 ty1 m = Some v /\ assign_loc ge ty1 m b ofs v t m'
   | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty =>
       exists t, exists v1,
       ty = ty1
@@ -561,18 +561,18 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Ecomma (Eval v ty1) r2 ty =>
       typeof r2 = ty
   | Eparen (Eval v1 ty1) ty2 ty =>
-      exists v, sem_cast v1 ty1 ty2 = Some v
+      exists v, sem_cast v1 ty1 ty2 m = Some v
   | Ecall (Eval vf tyf) rargs ty =>
       exprlist_all_values rargs ->
       exists tyargs tyres cconv fd vl,
          classify_fun tyf = fun_case_f tyargs tyres cconv
       /\ Genv.find_funct ge vf = Some fd
-      /\ cast_arguments rargs tyargs vl
+      /\ cast_arguments m rargs tyargs vl
       /\ type_of_fundef fd = Tfunction tyargs tyres cconv
   | Ebuiltin ef tyargs rargs ty =>
       exprlist_all_values rargs ->
       exists vargs, exists t, exists vres, exists m',
-         cast_arguments rargs tyargs vargs
+         cast_arguments m rargs tyargs vargs
       /\ external_call ef ge vargs m t vres m'
   | _ => True
   end.
@@ -608,7 +608,7 @@ Qed.
 
 Lemma callred_invert:
   forall r fd args ty m,
-  callred ge r fd args ty ->
+  callred ge r m fd args ty ->
   invert_expr_prop r m.
 Proof.
   intros. inv H. simpl.
@@ -893,7 +893,7 @@ Inductive eval_simple_list': exprlist -> list val -> Prop :=
 Lemma eval_simple_list_implies:
   forall rl tyl vl,
   eval_simple_list e m rl tyl vl ->
-  exists vl', cast_arguments (rval_list vl' rl) tyl vl /\ eval_simple_list' rl vl'.
+  exists vl', cast_arguments m (rval_list vl' rl) tyl vl /\ eval_simple_list' rl vl'.
 Proof.
   induction 1.
   exists (@nil val); split. constructor. constructor.
@@ -905,7 +905,7 @@ Lemma can_eval_simple_list:
   forall rl vl,
   eval_simple_list' rl vl ->
   forall tyl vl',
-  cast_arguments (rval_list vl rl) tyl vl' ->
+  cast_arguments m (rval_list vl rl) tyl vl' ->
   eval_simple_list e m rl tyl vl'.
 Proof.
   induction 1; simpl; intros.
@@ -1234,9 +1234,9 @@ Proof.
   left; apply step_rred; auto. econstructor; eauto.
   set (op := match id with Incr => Oadd | Decr => Osub end).
   assert (SEM: sem_binary_operation ge op v1 (typeof l) (Vint Int.one) type_int32s m =
-              sem_incrdecr ge id v1 (typeof l)).
+              sem_incrdecr ge id v1 (typeof l) m).
     destruct id; auto.
-  destruct (sem_incrdecr ge id v1 (typeof l)) as [v2|].
+  destruct (sem_incrdecr ge id v1 (typeof l) m) as [v2|].
   eapply star_left.
   left; apply step_rred with (C := fun x => C (Ecomma (Eassign (Eloc b ofs (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto.
   econstructor; eauto.
@@ -1329,7 +1329,7 @@ Proof.
   intros [v [E2 S2]].
   exploit safe_inv. eexact S2. eauto. simpl. intros [t1 [v1 [A B]]].
   destruct (sem_binary_operation ge op v1 (typeof b1) v (typeof b2) m) as [v3|] eqn:?.
-  destruct (sem_cast v3 tyres (typeof b1)) as [v4|] eqn:?.
+  destruct (sem_cast v3 tyres (typeof b1) m) as [v4|] eqn:?.
   destruct (classic (exists t2, exists m', assign_loc ge (typeof b1) m b ofs v4 t2 m')).
   destruct H2 as [t2 [m' D]].
   econstructor; econstructor; eapply step_assignop; eauto.
@@ -1343,8 +1343,8 @@ Proof.
   exploit (simple_can_eval_lval f k e m b (fun x => C(Epostincr id x ty))); eauto.
   intros [b1 [ofs [E1 S1]]].
   exploit safe_inv. eexact S1. eauto. simpl. intros [t [v1 [A B]]].
-  destruct (sem_incrdecr ge id v1 ty) as [v2|] eqn:?.
-  destruct (sem_cast v2 (incrdecr_type ty) ty) as [v3|] eqn:?.
+  destruct (sem_incrdecr ge id v1 ty m) as [v2|] eqn:?.
+  destruct (sem_cast v2 (incrdecr_type ty) ty m) as [v3|] eqn:?.
   destruct (classic (exists t2, exists m', assign_loc ge ty m b1 ofs v3 t2 m')).
   destruct H0 as [t2 [m' D]].
   econstructor; econstructor; eapply step_postincr; eauto.
@@ -1498,7 +1498,7 @@ Proof.
   econstructor; econstructor; eauto.
   inv H10. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
   destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?.
-  destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?.
+  destruct (sem_cast v3' tyres (typeof l) m) as [v4'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v4' t2' m'')).
   destruct H1 as [t2' [m'' P]].
   econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity.
@@ -1511,7 +1511,7 @@ Proof.
   (* assignop stuck *)
   exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
   destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?.
-  destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?.
+  destruct (sem_cast v3' tyres (typeof l) m) as [v4'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v4' t2' m'')).
   destruct H1 as [t2' [m'' P]].
   econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity.
@@ -1526,8 +1526,8 @@ Proof.
   subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H.
   econstructor; econstructor; eauto.
   inv H9. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
-  destruct (sem_incrdecr ge id v1' (typeof l)) as [v2'|] eqn:?.
-  destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l)) as [v3'|] eqn:?.
+  destruct (sem_incrdecr ge id v1' (typeof l) m) as [v2'|] eqn:?.
+  destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l) m) as [v3'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v3' t2' m'')).
   destruct H1 as [t2' [m'' P]].
   econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity.
@@ -1539,8 +1539,8 @@ Proof.
   rewrite Heqo; auto.
   (* postincr stuck *)
   exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
-  destruct (sem_incrdecr ge id v1' (typeof l)) as [v2'|] eqn:?.
-  destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l)) as [v3'|] eqn:?.
+  destruct (sem_incrdecr ge id v1' (typeof l) m) as [v2'|] eqn:?.
+  destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l) m) as [v3'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v3' t2' m'')).
   destruct H1 as [t2' [m'' P]].
   econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity.
@@ -1641,11 +1641,11 @@ Definition outcome_switch (out: outcome) : outcome :=
   | o => o
   end.
 
-Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop :=
+Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem) : Prop :=
   match out, t with
   | Out_normal, Tvoid => v = Vundef
   | Out_return None, Tvoid => v = Vundef
-  | Out_return (Some (v', ty')), ty => ty <> Tvoid /\ sem_cast v' ty' ty = Some v
+  | Out_return (Some (v', ty')), ty => ty <> Tvoid /\ sem_cast v' ty' ty m = Some v
   | _, _ => False
   end.
 
@@ -1697,7 +1697,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
       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 ->
+      sem_cast v2 (typeof a2) type_bool m'' = 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 ->
@@ -1707,7 +1707,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
       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 ->
+      sem_cast v2 (typeof a2) type_bool m'' = 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 ->
@@ -1717,7 +1717,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
       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 ->
+      sem_cast v' (typeof (if b then a2 else a3)) ty m'' = Some v ->
       eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty)
   | eval_sizeof: forall e m ty' ty,
       eval_expr e m RV (Esizeof ty' ty) E0 m (Esizeof ty' ty)
@@ -1727,7 +1727,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m LV l t1 m1 l' -> eval_expr e m1 RV r t2 m2 r' ->
       eval_simple_lvalue ge e m2 l' b ofs ->
       eval_simple_rvalue ge e m2 r' v ->
-      sem_cast v (typeof r) (typeof l) = Some v' ->
+      sem_cast v (typeof r) (typeof l) m2 = Some v' ->
       assign_loc ge (typeof l) m2 b ofs v' t3 m3 ->
       ty = typeof l ->
       eval_expr e m RV (Eassign l r ty) (t1**t2**t3) m3 (Eval v' ty)
@@ -1738,7 +1738,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       deref_loc ge (typeof l) m2 b ofs t3 v1 ->
       eval_simple_rvalue ge e m2 r' v2 ->
       sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m2 = Some v3 ->
-      sem_cast v3 tyres (typeof l) = Some v4 ->
+      sem_cast v3 tyres (typeof l) m2 = Some v4 ->
       assign_loc ge (typeof l) m2 b ofs v4 t4 m3 ->
       ty = typeof l ->
       eval_expr e m RV (Eassignop op l r tyres ty) (t1**t2**t3**t4) m3 (Eval v4 ty)
@@ -1746,8 +1746,8 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m LV l t1 m1 l' ->
       eval_simple_lvalue ge e m1 l' b ofs ->
       deref_loc ge ty m1 b ofs t2 v1 ->
-      sem_incrdecr ge id v1 ty = Some v2 ->
-      sem_cast v2 (incrdecr_type ty) ty = Some v3 ->
+      sem_incrdecr ge id v1 ty m1 = Some v2 ->
+      sem_cast v2 (incrdecr_type ty) ty m1 = Some v3 ->
       assign_loc ge ty m1 b ofs v3 t3 m2 ->
       ty = typeof l ->
       eval_expr e m RV (Epostincr id l ty) (t1**t2**t3) m2 (Eval v1 ty)
@@ -1901,7 +1901,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
       alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
       bind_parameters ge e m1 f.(fn_params) vargs m2 ->
       exec_stmt e m2 f.(fn_body) t m3 out ->
-      outcome_result_value out f.(fn_return) vres ->
+      outcome_result_value out f.(fn_return) vres m3 ->
       Mem.free_list m3 (blocks_of_env ge e) = Some m4 ->
       eval_funcall m (Internal f) vargs t m4 vres
   | eval_funcall_external: forall m ef targs tres cconv vargs t vres m',