From 12f7b21e6e1bafe895680108e75311c678a22ac1 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 24 Nov 2017 10:03:11 +0100 Subject: Issue #208: make value analysis of comparisons more conservative w.r.t. pointers (#209) Comparisons such as "(uintptr_t) &global == 0x1234" are undefined behavior in CompCert but their status in ISO C is unclear and they may occur in real-world code. Make sure they are statically analyzed as Btop. --- Changelog | 3 +++ backend/ValueDomain.v | 20 ++++++++++++-------- 2 files changed, 15 insertions(+), 8 deletions(-) diff --git a/Changelog b/Changelog index 4c5632ee..7b230e41 100644 --- a/Changelog +++ b/Changelog @@ -1,5 +1,8 @@ Code generation and optimization: - ARM in Thumb mode: simpler instruction sequence for branch through jump table. +- Issue #208: make value analysis of comparisons more conservative for + dubious comparisons such as "(uintptr_t) &global == 0x1234" which are + undefined behavior in CompCert. Usability: - Resurrected support for the Cygwin x86-32 port, which got lost at release 3.0. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 7cf947ba..e7e44e29 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2634,11 +2634,9 @@ Qed. Definition cmpu_bool (c: comparison) (v w: aval) : abool := match v, w with | I i1, I i2 => Just (Int.cmpu c i1 i2) - | Ptr _, I _ => cmp_different_blocks c - | I _, Ptr _ => cmp_different_blocks c + | Ptr _, I i => if Int.eq i Int.zero then cmp_different_blocks c else Btop + | I i, Ptr _ => if Int.eq i Int.zero then cmp_different_blocks c else Btop | Ptr p1, Ptr p2 => pcmp c p1 p2 - | Ptr p1, (Ifptr p2 | Uns p2 _ | Sgn p2 _) => club (pcmp c p1 p2) (cmp_different_blocks c) - | (Ifptr p1 | Uns p1 _ | Sgn p1 _), Ptr p2 => club (pcmp c p1 p2) (cmp_different_blocks c) | _, I i => club (cmp_intv c (uintv v) (Int.unsigned i)) (cmp_different_blocks c) | I i, _ => club (cmp_intv (swap_comparison c) (uintv w) (Int.unsigned i)) (cmp_different_blocks c) | _, _ => Btop @@ -2669,6 +2667,10 @@ Proof. cmatch_lub_l, cmatch_lub_r, pcmp_sound, cmpu_intv_sound, cmpu_intv_sound_2, cmp_intv_None. - constructor. +- destruct (Int.eq i Int.zero); auto using cmatch_top. +- simpl; destruct (Int.eq i Int.zero); auto using cmatch_top, cmp_different_blocks_none. +- destruct (Int.eq i Int.zero); auto using cmatch_top. +- simpl; destruct (Int.eq i Int.zero); auto using cmatch_top, cmp_different_blocks_none. Qed. Definition cmp_bool (c: comparison) (v w: aval) : abool := @@ -2691,11 +2693,9 @@ Qed. Definition cmplu_bool (c: comparison) (v w: aval) : abool := match v, w with | L i1, L i2 => Just (Int64.cmpu c i1 i2) - | Ptr _, L _ => cmp_different_blocks c - | L _, Ptr _ => cmp_different_blocks c + | Ptr _, L i => if Int64.eq i Int64.zero then cmp_different_blocks c else Btop + | L i, Ptr _ => if Int64.eq i Int64.zero then cmp_different_blocks c else Btop | Ptr p1, Ptr p2 => pcmp c p1 p2 - | Ptr p1, Ifptr p2 => club (pcmp c p1 p2) (cmp_different_blocks c) - | Ifptr p1, Ptr p2 => club (pcmp c p1 p2) (cmp_different_blocks c) | _, _ => Btop end. @@ -2723,6 +2723,10 @@ Proof. auto using cmatch_top, cmp_different_blocks_none, pcmp_none, cmatch_lub_l, cmatch_lub_r, pcmp_sound_64. - constructor. +- destruct (Int64.eq i Int64.zero); auto using cmatch_top. +- simpl; destruct (Int64.eq i Int64.zero); auto using cmatch_top, cmp_different_blocks_none. +- destruct (Int64.eq i Int64.zero); auto using cmatch_top. +- simpl; destruct (Int64.eq i Int64.zero); auto using cmatch_top, cmp_different_blocks_none. Qed. Definition cmpl_bool (c: comparison) (v w: aval) : abool := -- cgit