From fd48dc8680286ab91ad79c1c8b1ca9ec2f516e64 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 4 Sep 2024 18:59:48 +0200 Subject: [PATCH] Return `Btop` for undefined pointer comparisons in non-strict mode Comparing pointers from different blocks with `< <= > >=` is undefined behavior in CompCert and in ISO C. So, it is sound to analyze such comparisons as `Bnone`. However, these comparisons occur in real code, and produce statically-unpredictable Boolean results, so it is safer and more consistent with other parts of the value analysis to return `Btop` in non-strict mode. Currently, this should make no difference to the generated code, since CompCert does not optimize based on the absence of undefined comparisons. --- backend/ValueDomain.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 1ebf09772..f505c4e88 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -373,19 +373,19 @@ Definition cmp_different_blocks (c: comparison) : abool := match c with | Ceq => Maybe false | Cne => Maybe true - | _ => Bnone + | _ => if va_strict tt then Bnone else Btop end. Lemma cmp_different_blocks_none: forall c, cmatch None (cmp_different_blocks c). Proof. - intros; destruct c; constructor. + unfold cmp_different_blocks. destruct c, (va_strict tt); constructor. Qed. Lemma cmp_different_blocks_sound: forall c, cmatch (Val.cmp_different_blocks c) (cmp_different_blocks c). Proof. - intros; destruct c; constructor. + unfold cmp_different_blocks. destruct c, (va_strict tt); constructor. Qed. Definition pcmp (c: comparison) (p1 p2: aptr) : abool :=