[PATCH] D45517: [analyzer] False positive refutation with Z3

This revision was automatically updated to reflect the committed changes. Closed by commit rC333903: [analyzer] False positive refutation with Z3 (authored by mramalho, committed by ). Changed prior to commit: https://reviews.llvm.org/D45517?vs=149664&id=149764#toc Repository: rC Clang http

Re: [PATCH] D45517: [analyzer] False positive refutation with Z3

> > > Awesome! Does it mean that the optimization for adding less constraints > was in fact buggy? > > I pretty sure it was not related to the optimizations, I removed them days ago (in the previous version of this patch) and the bug was still there. > > 2. Could it be something unrelated to your

[PATCH] D45517: [analyzer] False positive refutation with Z3

mikhail.ramalho updated this revision to Diff 149664. mikhail.ramalho edited the summary of this revision. mikhail.ramalho added a comment. Fix naming issue. https://reviews.llvm.org/D45517 Files: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h include/clang/StaticAnalyzer/Core/BugRepor

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added a comment. > I pretty sure it was not related to the optimizations, I removed them days ago (in the previous version of this patch) and the bug was still there. OK so any idea what the change could have been? Clearly the bug was there but not now. Anyway, should be OK to

[PATCH] D45517: [analyzer] False positive refutation with Z3

mikhail.ramalho added a subscriber: rnkovacs. mikhail.ramalho added a comment. > Awesome! Does it mean that the optimization for adding less constraints > was in fact buggy? I pretty sure it was not related to the optimizations, I removed them days ago (in the previous version of this patch) and

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov requested changes to this revision. george.karpenkov added a comment. This revision now requires changes to proceed. > I updated the test case as the cross check is not marking the true bug as > invalid anymore. Awesome! Does it mean that the optimization for adding less constra

[PATCH] D45517: [analyzer] False positive refutation with Z3

mikhail.ramalho added inline comments. Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2366 + + SMTConstraintManager *SMTRefutationMgr = + static_cast(RefutationMgr.get()); I'm not happy about this cast. Suggestions are welcome. https://review

[PATCH] D45517: [analyzer] False positive refutation with Z3

mikhail.ramalho updated this revision to Diff 149653. mikhail.ramalho added a comment. Update patch based on https://reviews.llvm.org/D47640 and https://reviews.llvm.org/D47689. I updated the test case as the cross check is not marking the true bug as invalid anymore. My `make clang-test` is s

[PATCH] D45517: [analyzer] False positive refutation with Z3

mikhail.ramalho updated this revision to Diff 149524. mikhail.ramalho added a comment. - Simplified the API even further by constructing a Z3ConstraintManager object directly. - Update isModelFeasible to return a isModelFeasible - Update code with the fix for 1-bit long integer https://reviews.

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added a comment. @mikhail.ramalho I assume you know it, but just in case, you can mark dependencies in phabricator by adding "parent" revisions. https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.or

Re: [PATCH] D45517: [analyzer] False positive refutation with Z3

Hi, > Just a bit of context and to have some expectation management regarding > this patch. The main purpose of this implementation was to back a thesis. > It was made under a very serious time pressure and the main goal was to be > able to measure on real world projects as soon as possible and i

[PATCH] D45517: [analyzer] False positive refutation with Z3

mikhail.ramalho added inline comments. Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:183 + virtual void reset() {} + virtual bool isModelFeasible() { return true; } + virtual void addRangeConstraints(ConstraintRangeTy) {} geo

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added inline comments. Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:183 + virtual void reset() {} + virtual bool isModelFeasible() { return true; } + virtual void addRangeConstraints(ConstraintRangeTy) {} mi

[PATCH] D45517: [analyzer] False positive refutation with Z3

mikhail.ramalho added inline comments. Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:183 + virtual void reset() {} + virtual bool isModelFeasible() { return true; } + virtual void addRangeConstraints(ConstraintRangeTy) {} geo

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added inline comments. Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:925 + void reset() override { Solver.reset(); } + mikhail.ramalho wrote: > george.karpenkov wrote: > > We don't need `reset` anymore. > We don't need it but the

[PATCH] D45517: [analyzer] False positive refutation with Z3

mikhail.ramalho added inline comments. Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2391 +if (!RefutationMgr->isModelFeasible()) + BR.markInvalid("Infeasible constraints", N->getLocationContext()); + } george.karpenkov wrote: > That would

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added inline comments. Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:928 + bool isModelFeasible() override { +return Solver.check() != Z3_L_FALSE; + } george.karpenkov wrote: > The semantics of this method is incorrect. It sho

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov requested changes to this revision. george.karpenkov added a comment. This revision now requires changes to proceed. Thanks, this is going in the right direction! Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:182 + virtual

[PATCH] D45517: [analyzer] False positive refutation with Z3

rnkovacs added a comment. In https://reviews.llvm.org/D45517#1117898, @mikhail.ramalho wrote: > Just want to comment here and give thanks again for the first version of > the refutation code. It's being really helpful to develop the approach this > code as a base; things would definitely be slo

[PATCH] D45517: [analyzer] False positive refutation with Z3

mikhail.ramalho added subscribers: dcoughlin, george.karpenkov, NoQ. mikhail.ramalho added a comment. Hi, > Just a bit of context and to have some expectation management regarding > this patch. The main purpose of this implementation was to back a thesis. > It was made under a very serious time

[PATCH] D45517: [analyzer] False positive refutation with Z3

mikhail.ramalho updated this revision to Diff 149317. mikhail.ramalho marked 6 inline comments as not done. mikhail.ramalho added a comment. - Simplified refutation process: it now collects all the constraints in a given path and, only when it reaches the root node, the refutation manager is crea

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added a comment. @xazax.hun > So strictly speaking it is not a deduplication on the constraint level but on > the symbol level. Right, apologies, I was initially mistaken then. That's not even deduplication, I would call it using the interval solver to guide the constraint sel

[PATCH] D45517: [analyzer] False positive refutation with Z3

xazax.hun added a comment. In https://reviews.llvm.org/D45517#1116770, @george.karpenkov wrote: > > I am not not sure that I got the idea what are you suggesting here. If we > > have the constraint of for example a symbol s > 10 and later on a path we > > discover s > 20, will we also deduplica

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added a comment. > I am not not sure that I got the idea what are you suggesting here. If we > have the constraint of for example a symbol s > 10 and later on a path we > discover s > 20, will we also deduplicate this that way? No. But I thought in your optimization atoms insid

[PATCH] D45517: [analyzer] False positive refutation with Z3

xazax.hun added a comment. In https://reviews.llvm.org/D45517#1116734, @george.karpenkov wrote: > @xazax.hun (I'll reply here to avoid scattering the conversation across many > subtrees) > > I was thinking about the optimization for not adding redundant constraints > some more, and I've decided

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added a comment. @xazax.hun (I'll reply here to avoid scattering the conversation across many subtrees) I was thinking about the optimization for not adding redundant constraints some more, and I've decided I'm still against it --- we are creating a higher potential for bugs, a

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added inline comments. Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2382 +// Reset the solver +RefutationMgr.reset(); + } xazax.hun wrote: > george.karpenkov wrote: > > xazax.hun wrote: > > > george.karpenkov wrote: > > >

[PATCH] D45517: [analyzer] False positive refutation with Z3

xazax.hun added inline comments. Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2382 +// Reset the solver +RefutationMgr.reset(); + } george.karpenkov wrote: > xazax.hun wrote: > > george.karpenkov wrote: > > > george.karpenkov wrote: > > >

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added inline comments. Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2382 +// Reset the solver +RefutationMgr.reset(); + } xazax.hun wrote: > george.karpenkov wrote: > > george.karpenkov wrote: > > > (apologies in advance f

[PATCH] D45517: [analyzer] False positive refutation with Z3

xazax.hun added inline comments. Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2382 +// Reset the solver +RefutationMgr.reset(); + } george.karpenkov wrote: > george.karpenkov wrote: > > (apologies in advance for nitpicking not on your code

[PATCH] D45517: [analyzer] False positive refutation with Z3

rnkovacs added inline comments. Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1249 +bool Z3ConstraintManager::isModelFeasible() { + return Solver.check() != Z3_L_FALSE; +} george.karpenkov wrote: > solver can also return "unknown", what happens the

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added inline comments. Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1267 + +Z3Expr Constraints = Z3Expr::fromBoolean(false); + george.karpenkov wrote: > almost certainly a bug, we shouldn't default to unfeasible when the list o

[PATCH] D45517: [analyzer] False positive refutation with Z3

NoQ added inline comments. Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1292 + Constraints = + Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy); +} george.karpenkov wrote: > I'm very confused as to why are we doing dis

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added inline comments. Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:496 std::unique_ptr ConstraintMgr; + std::unique_ptr RefutationMgr; See the comment below, I think we should not have this manager here. J

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added inline comments. Comment at: lib/StaticAnalyzer/Core/BugReporter.cpp:3153 +if (getAnalyzerOptions().shouldCrosscheckWithZ3()) + R->addVisitor(llvm::make_unique()); + Unless I'm mistaken, visitors are run in the order they are being

[PATCH] D45517: [analyzer] False positive refutation with Z3

mikhail.ramalho updated this revision to Diff 148969. mikhail.ramalho marked 6 inline comments as done. mikhail.ramalho added a comment. 1. Moved FalsePositiveRefutationBRVisitor::Profile definition to BugReporterVisitor.cpp 2. Update test cases two run twice, with and without the crosscheck 3. R

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added inline comments. Comment at: test/Analysis/z3-crosscheck.c:2 +// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s +// REQUIRES: z3 +// expected-no-diagnostics

[PATCH] D45517: [analyzer] False positive refutation with Z3

george.karpenkov added a comment. Please resubmit with -U999 diff flag (or using arc) Comment at: include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h:362 +class FalsePositiveRefutationBRVisitor final +: public BugReporterVisitorImpl { Can

[PATCH] D45517: [analyzer] False positive refutation with Z3

mikhail.ramalho updated this revision to Diff 148828. mikhail.ramalho retitled this revision from "[analyzer] WIP: False positive refutation with Z3" to "[analyzer] False positive refutation with Z3". mikhail.ramalho added a comment. Added test cases and updated the analyzer-config tests with the