From 0db58223d9c3e33888fa3d08f5595c2f0d91e42a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 23 Jul 2024 16:57:37 +0200 Subject: [PATCH 1/2] More conservative analysis of pointer equality and difference A pointer "one past" a global "x" and a pointer to the beginning of a global "y" can be equal. This is undefined behavior in CompCert C, but defined behavior in ISO C. Thus, the value analysis should not infer that a pointer based at "x" and a pointer based at "y" cannot be equal. The only inference we keep is that a pointer based in the current stack block and a pointer based in a global variable cannot be equal. --- backend/ValueDomain.v | 16 +--------------- 1 file changed, 1 insertion(+), 15 deletions(-) diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 9b98d4bef7..98d6736b85 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -391,15 +391,7 @@ Qed. Definition pcmp (c: comparison) (p1 p2: aptr) : abool := match p1, p2 with | Pbot, _ | _, Pbot => Bnone - | Gl id1 ofs1, Gl id2 ofs2 => - if peq id1 id2 then Maybe (Ptrofs.cmpu c ofs1 ofs2) - else cmp_different_blocks c - | Gl id1 ofs1, Glo id2 => - if peq id1 id2 then Btop else cmp_different_blocks c - | Glo id1, Gl id2 ofs2 => - if peq id1 id2 then Btop else cmp_different_blocks c - | Glo id1, Glo id2 => - if peq id1 id2 then Btop else cmp_different_blocks c + | Gl id1 ofs1, Gl id2 ofs2 => if peq id1 id2 then Maybe (Ptrofs.cmpu c ofs1 ofs2) else Btop | Stk ofs1, Stk ofs2 => Maybe (Ptrofs.cmpu c ofs1 ofs2) | (Gl _ _ | Glo _ | Glob | Nonstack), (Stk _ | Stack) => cmp_different_blocks c | (Stk _ | Stack), (Gl _ _ | Glo _ | Glob | Nonstack) => cmp_different_blocks c @@ -438,9 +430,6 @@ Proof. unfold pcmp; inv H; inv H0; (apply cmatch_top || (apply DIFF; congruence) || idtac). - destruct (peq id id0). subst id0. apply SAME. eapply bc_glob; eauto. auto with va. - - destruct (peq id id0); auto with va. - - destruct (peq id id0); auto with va. - - destruct (peq id id0); auto with va. - apply SAME. eapply bc_stack; eauto. Qed. @@ -476,9 +465,6 @@ Proof. unfold pcmp; inv H; inv H0; (apply cmatch_top || (apply DIFF; congruence) || idtac). - destruct (peq id id0). subst id0. apply SAME. eapply bc_glob; eauto. auto with va. - - destruct (peq id id0); auto with va. - - destruct (peq id id0); auto with va. - - destruct (peq id id0); auto with va. - apply SAME. eapply bc_stack; eauto. Qed. From 918df5a9d7679decaab281245c4234be9966b38a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 23 Jul 2024 17:02:42 +0200 Subject: [PATCH 2/2] Update test suite --- test | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test b/test index 4a25324208..02fc1f7521 160000 --- a/test +++ b/test @@ -1 +1 @@ -Subproject commit 4a253242086d1ce78365d1b5cac3201193fa3814 +Subproject commit 02fc1f752101db18e8ac0b103a0e1222a7f94702