diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-03-15 17:07:36 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-03-15 17:07:36 +0100 |
| commit | 57d3627c69a812a037d2d4161941ce25d15082d1 (patch) | |
| tree | 02f375b130eb6cdab00796fc3580d56684f95a70 /backend | |
| parent | b3294fbaf50539f254ff3bb7145e848b3f902f73 (diff) | |
| download | compcert-57d3627c69a812a037d2d4161941ce25d15082d1.tar.gz compcert-57d3627c69a812a037d2d4161941ce25d15082d1.zip | |
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.
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Selectionproof.v | 2 | ||||
| -rw-r--r-- | backend/ValueDomain.v | 6 |
2 files changed, 5 insertions, 3 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index bb9bd592..20b6cf93 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -135,7 +135,7 @@ Proof. inv H. econstructor; eauto. (* default *) econstructor. constructor. eauto. constructor. - simpl. inv H0. auto. auto. + simpl. inv H0. auto. Qed. Lemma eval_load: diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 92004a2f..ff3ccfa1 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2121,12 +2121,14 @@ Proof. assert (IP: forall i b ofs, cmatch (Val.cmpu_bool valid c (Vint i) (Vptr b ofs)) (cmp_different_blocks c)). { - intros. simpl. destruct (Int.eq i Int.zero). apply cmp_different_blocks_sound. apply cmp_different_blocks_none. + intros. simpl. destruct (Int.eq i Int.zero && (valid b (Int.unsigned ofs) || valid b (Int.unsigned ofs - 1))). + apply cmp_different_blocks_sound. apply cmp_different_blocks_none. } assert (PI: forall i b ofs, cmatch (Val.cmpu_bool valid c (Vptr b ofs) (Vint i)) (cmp_different_blocks c)). { - intros. simpl. destruct (Int.eq i Int.zero). apply cmp_different_blocks_sound. apply cmp_different_blocks_none. + intros. simpl. destruct (Int.eq i Int.zero && (valid b (Int.unsigned ofs) || valid b (Int.unsigned ofs - 1))). + apply cmp_different_blocks_sound. apply cmp_different_blocks_none. } unfold cmpu_bool; inversion H; subst; inversion H0; subst; auto using cmatch_top, cmp_different_blocks_none, pcmp_none, |