Skip to content

Commit

Permalink
Merge pull request #516 from AbsInt/value-analysis-pointer-comparison
Browse files Browse the repository at this point in the history 
More conservative value analysis of pointer equality
  • Loading branch information
@xavierleroy
xavierleroy authored Jul 26, 2024
2 parents a15470e + 918df5a commit 62251c7
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 16 deletions.
16 changes: 1 addition & 15 deletions backend/ValueDomain.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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.

Expand Down
2 changes: 1 addition & 1 deletion test
Submodule test updated 4 files
+5 −0 export/.gitignore
+3 −1 export/Makefile
+2 −0 regression/Results/alias
+31 −1 regression/alias.c

4 comments on commit 62251c7

@monniaux
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@xavierleroy FYI We also ran into a interesting case of over-precise pointer value analysis on embedded code that, admittedly, relied on undefined behavior.

https://gricad-gitlab.univ-grenoble-alpes.fr/sixcy/CompCert/-/commit/7544c6b9a71459799984059bdfb2029ccf992b44

@xavierleroy
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The link requires registration.

@monniaux
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh sorry @xavierleroy the externally accessible link is
https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/Chamois-CompCert/-/commit/7544c6b9a71459799984059bdfb2029ccf992b44

@xavierleroy
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the link. As discussed over email: before the merge of #516, it is indeed possible to have loops whose stopping condition is a pointer comparison to be "optimized" into infinite loops. I believe this cannot occur now that #516 is merged.

Please sign in to comment.