This is an archive of the discontinued LLVM Phabricator instance.

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

Authored by mikhail.ramalho 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?

@mikhail.ramalho brought this up in pr41809 so let's revisit this.

Like, the patch looks great, the idea looks great, but i'd like to make super duper sure that the behavior without Z3 remains the same, because we are in no position to give up on the no-Z3 mode yet.

test/Analysis/PR3991.m
63 ↗(On Diff #113619)

This looks like a regression to me. Even though BoolAssignment is an alpha checker, it's definitely one of the good ones, which i want to enable by default sooner rather than later, so can we try not to regress it too much?

test/Analysis/std-c-library-functions.c
149

Why did this have to change? I don't remember all the details of how these functions work, but as far as i remember the only character that is printable but not graphical is the space character (32) which converts between int and char just fine.

ddcc added a comment.Jan 17 2020, 7:41 AM

I don't have the time to rebase and retest this currently, so it might be better for someone else to take over this patch. Unfortunately, it's been long enough that I don't remember the details of these changes.

I can give some help here, but my time is quite limited as well :/

Let me at least rebase against master.

mikhail.ramalho commandeered this revision.Jan 20 2020, 11:39 AM
mikhail.ramalho added a reviewer: ddcc.

Two changes:

  • Moved the BoolAssignmentChecker changes to separate revision (D73062).
  • Rebased on top of master.

There are a few cases failing, some because clang is trying to match some strings printed by the ranged constraint manager and there is at least 1 segfault.

Herald added a project: Restricted Project. · View Herald TranscriptJan 20 2020, 11:42 AM
NoQ added a comment.Jan 21 2020, 7:03 AM

Thanks for picking this up!~

Hmm, why did the change in MallocChecker tests disappear?

clang is trying to match some strings printed by the ranged constraint manager

Are these state dump tests / exploded-graph-rewriter tests? We'll need to ignore/silence them in Z3 mode.