Page MenuHomePhabricator

[analyzer] Enable support for symbolic extension/truncation
Needs ReviewPublic

Authored by ddcc on Jan 20 2017, 8:13 AM.

Details

Summary

Generate symbolic extension and truncation constraints where supported by the underlying constraint manager, currently limited to Z3. Also fix integer type bug with Z3ConstraintManager, and support comparison of APSInt with different types in SimpleConstraintManager.

Event Timeline

ddcc created this revision.Jan 20 2017, 8:13 AM
rgov added a subscriber: rgov.Jan 20 2017, 11:12 PM

Are all the changes here related to the extension/truncation support, for instance the changes to test/Analysis/malloc.c? Can you move misc. cleanup changes to another review?

ddcc added a comment.EditedJan 21 2017, 12:11 PM

When I was testing this patch, it was on top of both D28952 and D28953. For malloc.c, the change on line 1708 from int to size_t is necessary to prevent a false positive warning at line 1710. The other three type changes in that file don't affect the testcase output, but I probably made the changes at the same time. Do you want those other three pulled out separately?

In general, I think all the changes are related to the commit, or were other instances of a testcase related fix in the same file.

NoQ edited edge metadata.Jan 21 2017, 12:25 PM
In D28955#652443, @ddcc wrote:

When I was testing this patch, it was on top of both D28952 and D28953. For malloc.c, the change on line 1708 from int to size_t is necessary to prevent a false positive warning at line 1710.

We should have expected-warning on 64-bit targets (where size_t easily overflows int) and no-warning on 32-bit targets (where they are of the same size and the fix for the original issue https://llvm.org/bugs/show_bug.cgi?id=16558 applies). I think we should have two run-lines for this test, with two concrete targets specified; it'd be great to actually have other tests in this file undergo such trial.

ddcc added a comment.Jan 21 2017, 1:57 PM

We should have expected-warning on 64-bit targets (where size_t easily overflows int) and no-warning on 32-bit targets (where they are of the same size and the fix for the original issue https://llvm.org/bugs/show_bug.cgi?id=16558 applies). I think we should have two run-lines for this test, with two concrete targets specified; it'd be great to actually have other tests in this file undergo such trial.

To clarify, you're asking for something like the following, instead of changing from int to size_t?

diff --git a/test/Analysis/malloc.c b/test/Analysis/malloc.c
index 42deb9f..80e4184 100644
--- a/test/Analysis/malloc.c
+++ b/test/Analysis/malloc.c
@@ -1,4 +1,5 @@
-// RUN: %clang_cc1 %z3_cc1 -analyze -analyzer-checker=core,alpha.deadcode.UnreachableCode,alpha.core.CastSize,unix.Malloc,debug.ExprInspection -analyzer-store=region -verify %s
+// RUN: %clang_cc1 %z3_cc1 -triple i386-unknown-linux -analyze -analyzer-checker=core,alpha.deadcode.UnreachableCode,alpha.core.CastSize,unix.Malloc,debug.ExprInspection -analyzer-store=region -verify %s
+// RUN: %clang_cc1 %z3_cc1 -triple x86_64-unknown-linux -Dx86_64 -analyze -analyzer-checker=core,alpha.deadcode.UnreachableCode,alpha.core.CastSize,unix.Malloc,debug.ExprInspection -analyzer-store=region -verify %s

 #include "Inputs/system-header-simulator.h"

@@ -1705,9 +1706,13 @@ void *smallocNoWarn(size_t size) {
 }

 char *dupstrNoWarn(const char *s) {
-  const size_t len = strlen(s);
+  const int len = strlen(s);
   char *p = (char*) smallocNoWarn(len + 1);
-  strcpy(p, s); // no-warning
+#ifdef x86_64
+  strcpy(p, s); // expected-warning{{String copy function overflows destination buffer}}
+#else
+  strcpy(p, s); // no warning
+#endif
   return p;
 }
ddcc updated this revision to Diff 85316.Jan 22 2017, 8:24 PM

Rebase

dcoughlin edited edge metadata.Aug 31 2017, 3:27 PM

@ddcc : When I run this I get a bunch of assertion failures. Does this depend on https://reviews.llvm.org/D28953? (Which was reverted) Is it subsumed by https://reviews.llvm.org/D35450?

Is this blocking on a review of another patch on our end?

ddcc updated this revision to Diff 113619.Sep 1 2017, 3:54 PM

Rebase, factor out floating-point changes, fix Z3 type bug, support general APSInt comparison

ddcc added a comment.EditedSep 1 2017, 3:54 PM

@dcoughlin No, all three patches are separate. I have been testing them with each applied incrementally onto the previous, in the order trunk, D35450, D28954, then D28955 (this). But since these are a lot of dependencies, I've refactored this patch to apply directly on top of D35450, though the floating-point specific changes will need to be merged into D28954. Also, I think D28954 is waiting for review.

ddcc edited the summary of this revision. (Show Details)Sep 1 2017, 3:55 PM
ddcc added a comment.Sep 1 2017, 4:02 PM

@NoQ Does the proposal in https://reviews.llvm.org/D28955#652465 satisfy your concern?