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 --- 1 file changed, 3 deletions(-) (limited to 'cfrontend/Cop.v') 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 => -- 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/Cop.v | 68 ++++++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 50 insertions(+), 18 deletions(-) (limited to 'cfrontend/Cop.v') 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 *) -- cgit