r340532 - [analyzer] Delete SMTContext. NFC.
Author: mramalho Date: Thu Aug 23 06:20:18 2018 New Revision: 340532 URL: http://llvm.org/viewvc/llvm-project?rev=340532&view=rev Log: [analyzer] Delete SMTContext. NFC. Summary: There is no reason to have a base class for a context anymore as each SMT object carries a reference to the specific solver context. Reviewers: NoQ, george.karpenkov, hiraditya Reviewed By: hiraditya Subscribers: hiraditya, xazax.hun, szepet, a.sidorin, Szelethus Differential Revision: https://reviews.llvm.org/D50768 Removed: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Removed: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h?rev=340531&view=auto == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h (removed) @@ -1,31 +0,0 @@ -//== SMTContext.h ---*- C++ -*--==// -// -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===--===// -// -// This file defines a SMT generic Context API, which will be the base class -// for every SMT solver context specific class. -// -//===--===// - -#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONTEXT_H -#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONTEXT_H - -namespace clang { -namespace ento { - -/// Generic base class for SMT contexts -class SMTContext { -public: - SMTContext() = default; - virtual ~SMTContext() = default; -}; - -} // namespace ento -} // namespace clang - -#endif Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=340532&r1=340531&r2=340532&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Thu Aug 23 06:20:18 2018 @@ -11,7 +11,6 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h" @@ -53,11 +52,11 @@ void Z3ErrorHandler(Z3_context Context, } /// Wrapper for Z3 context -class Z3Context : public SMTContext { +class Z3Context { public: Z3_context Context; - Z3Context() : SMTContext() { + Z3Context() { Context = Z3_mk_context_rc(Z3Config().Config); // The error function is set here because the context is the first object // created by the backend ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r333094 - Test Commit. Fix namespace comment
Author: mramalho Date: Wed May 23 08:49:12 2018 New Revision: 333094 URL: http://llvm.org/viewvc/llvm-project?rev=333094&view=rev Log: Test Commit. Fix namespace comment Signed-off-by: Mikhail Ramalho Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h?rev=333094&r1=333093&r2=333094&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h Wed May 23 08:49:12 2018 @@ -85,8 +85,8 @@ private: bool Assumption); }; -} // end GR namespace +} // end namespace ento -} // end clang namespace +} // end namespace clang #endif ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r333179 - [analyzer] Move RangeSet related declarations into the RangedConstraintManager header.
Author: mramalho Date: Thu May 24 05:16:35 2018 New Revision: 333179 URL: http://llvm.org/viewvc/llvm-project?rev=333179&view=rev Log: [analyzer] Move RangeSet related declarations into the RangedConstraintManager header. Summary: I could also move `RangedConstraintManager.h` under `include/` if you agree as it seems slightly out of place under `lib/`. Patch by Réka Kovács Reviewers: NoQ, george.karpenkov, dcoughlin, rnkovacs Reviewed By: NoQ Subscribers: mikhail.ramalho, whisperity, xazax.hun, baloghadamsoftware, szepet, a.sidorin, dkrupp, cfe-commits Differential Revision: https://reviews.llvm.org/D45920 Modified: cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.h Modified: cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp?rev=333179&r1=333178&r2=333179&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp Thu May 24 05:16:35 2018 @@ -23,263 +23,171 @@ using namespace clang; using namespace ento; -/// A Range represents the closed range [from, to]. The caller must -/// guarantee that from <= to. Note that Range is immutable, so as not -/// to subvert RangeSet's immutability. -namespace { -class Range : public std::pair { -public: - Range(const llvm::APSInt &from, const llvm::APSInt &to) - : std::pair(&from, &to) { -assert(from <= to); - } - bool Includes(const llvm::APSInt &v) const { -return *first <= v && v <= *second; - } - const llvm::APSInt &From() const { return *first; } - const llvm::APSInt &To() const { return *second; } - const llvm::APSInt *getConcreteValue() const { -return &From() == &To() ? &From() : nullptr; - } - - void Profile(llvm::FoldingSetNodeID &ID) const { -ID.AddPointer(&From()); -ID.AddPointer(&To()); - } -}; - -class RangeTrait : public llvm::ImutContainerInfo { -public: - // When comparing if one Range is less than another, we should compare - // the actual APSInt values instead of their pointers. This keeps the order - // consistent (instead of comparing by pointer values) and can potentially - // be used to speed up some of the operations in RangeSet. - static inline bool isLess(key_type_ref lhs, key_type_ref rhs) { -return *lhs.first < *rhs.first || - (!(*rhs.first < *lhs.first) && *lhs.second < *rhs.second); - } -}; - -/// RangeSet contains a set of ranges. If the set is empty, then -/// there the value of a symbol is overly constrained and there are no -/// possible values for that symbol. -class RangeSet { - typedef llvm::ImmutableSet PrimRangeSet; - PrimRangeSet ranges; // no need to make const, since it is an - // ImmutableSet - this allows default operator= - // to work. -public: - typedef PrimRangeSet::Factory Factory; - typedef PrimRangeSet::iterator iterator; - - RangeSet(PrimRangeSet RS) : ranges(RS) {} - - /// Create a new set with all ranges of this set and RS. - /// Possible intersections are not checked here. - RangeSet addRange(Factory &F, const RangeSet &RS) { -PrimRangeSet Ranges(RS.ranges); -for (const auto &range : ranges) - Ranges = F.add(Ranges, range); -return RangeSet(Ranges); - } - - iterator begin() const { return ranges.begin(); } - iterator end() const { return ranges.end(); } - - bool isEmpty() const { return ranges.isEmpty(); } - - /// Construct a new RangeSet representing '{ [from, to] }'. - RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to) - : ranges(F.add(F.getEmptySet(), Range(from, to))) {} - - /// Profile - Generates a hash profile of this RangeSet for use - /// by FoldingSet. - void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); } - - /// getConcreteValue - If a symbol is contrained to equal a specific integer - /// constant then this method returns that value. Otherwise, it returns - /// NULL. - const llvm::APSInt *getConcreteValue() const { -return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : nullptr; - } +void RangeSet::IntersectInRange(BasicValueFactory &BV, Factory &F, + const llvm::APSInt &Lower, const llvm::APSInt &Upper, + PrimRangeSet &newRanges, PrimRangeSet::iterator &i, + PrimRangeSet::iterator &e) const { + // There are six cases for each range R in the set: + // 1. R is entirely before the intersection range. + // 2. R is entirely after the intersection range. + // 3. R contains the entire intersection range. + // 4. R starts before the intersection range and ends in the middle. + // 5. R starts in the middle of the intersection range and ends after it. + // 6. R
r333375 - Introduces --stats-only option to only show changes in statistics.
Author: mramalho Date: Mon May 28 08:40:39 2018 New Revision: 75 URL: http://llvm.org/viewvc/llvm-project?rev=75&view=rev Log: Introduces --stats-only option to only show changes in statistics. Modified: cfe/trunk/utils/analyzer/CmpRuns.py Modified: cfe/trunk/utils/analyzer/CmpRuns.py URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/utils/analyzer/CmpRuns.py?rev=75&r1=74&r2=75&view=diff == --- cfe/trunk/utils/analyzer/CmpRuns.py (original) +++ cfe/trunk/utils/analyzer/CmpRuns.py Mon May 28 08:40:39 2018 @@ -26,12 +26,25 @@ Usage: """ -import sys -import os -import plistlib +from collections import defaultdict + from math import log from optparse import OptionParser +import json +import os +import plistlib +import re +import sys + +STATS_REGEXP = re.compile(r"Statistics: (\{.+\})", re.MULTILINE | re.DOTALL) +class Colors: +""" +Color for terminal highlight. +""" +RED = '\x1b[2;30;41m' +GREEN = '\x1b[6;30;42m' +CLEAR = '\x1b[0m' # Information about analysis run: # path - the analysis output directory @@ -120,12 +133,16 @@ class AnalysisRun: # Cumulative list of all diagnostics from all the reports. self.diagnostics = [] self.clang_version = None +self.stats = [] def getClangVersion(self): return self.clang_version def readSingleFile(self, p, deleteEmpty): data = plistlib.readPlist(p) +if 'statistics' in data: +self.stats.append(json.loads(data['statistics'])) +data.pop('statistics') # We want to retrieve the clang version even if there are no # reports. Assume that all reports were created using the same @@ -264,12 +281,53 @@ def compareResults(A, B, opts): return res +def deriveStats(results): +# Assume all keys are the same in each statistics bucket. +combined_data = defaultdict(list) +for stat in results.stats: +for key, value in stat.iteritems(): +combined_data[key].append(value) +combined_stats = {} +for key, values in combined_data.iteritems(): +combined_stats[str(key)] = { +"max": max(values), +"min": min(values), +"mean": sum(values) / len(values), +"median": sorted(values)[len(values) / 2], +"total": sum(values) +} +return combined_stats + + +def compareStats(resultsA, resultsB): +statsA = deriveStats(resultsA) +statsB = deriveStats(resultsB) +keys = sorted(statsA.keys()) +for key in keys: +print key +for kkey in statsA[key]: +valA = float(statsA[key][kkey]) +valB = float(statsB[key][kkey]) +report = "%.3f -> %.3f" % (valA, valB) +# Only apply highlighting when writing to TTY and it's not Windows +if sys.stdout.isatty() and os.name != 'nt': +if valA != 0: + ratio = (valB - valA) / valB + if ratio < -0.2: + report = Colors.GREEN + report + Colors.CLEAR + elif ratio > 0.2: + report = Colors.RED + report + Colors.CLEAR +print "\t %s %s" % (kkey, report) def dumpScanBuildResultsDiff(dirA, dirB, opts, deleteEmpty=True, Stdout=sys.stdout): # Load the run results. resultsA = loadResults(dirA, opts, opts.rootA, deleteEmpty) resultsB = loadResults(dirB, opts, opts.rootB, deleteEmpty) +if resultsA.stats: +compareStats(resultsA, resultsB) +if opts.stats_only: +return # Open the verbose log, if given. if opts.verboseLog: @@ -339,6 +397,8 @@ def generate_option_parser(): default=False, help="Show histogram of absolute paths differences. \ Requires matplotlib") +parser.add_option("--stats-only", action="store_true", dest="stats_only", + default=False, help="Only show statistics on reports") return parser ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r340533 - [analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations. NFC.
Author: mramalho Date: Thu Aug 23 06:21:00 2018 New Revision: 340533 URL: http://llvm.org/viewvc/llvm-project?rev=340533&view=rev Log: [analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations. NFC. Summary: By making SMTConstraintManager a template and passing the SMT constraint type and expr, we can further move code from the Z3ConstraintManager class to the generic SMT constraint Manager. Now, each SMT specific constraint manager only needs to implement the method `bool canReasonAbout(SVal X) const`. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: mgorny, xazax.hun, szepet, a.sidorin, Szelethus Differential Revision: https://reviews.llvm.org/D50770 Removed: cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=340533&r1=340532&r2=340533&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Thu Aug 23 06:21:00 2018 @@ -21,6 +21,7 @@ namespace clang { namespace ento { +template class SMTConstraintManager : public clang::ento::SimpleConstraintManager { SMTSolverRef &Solver; @@ -34,25 +35,191 @@ public: // Implementation for interface from SimpleConstraintManager. //===--===// - ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym, -bool Assumption) override; + ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, +bool Assumption) override { +ASTContext &Ctx = getBasicVals().getContext(); + +QualType RetTy; +bool hasComparison; + +SMTExprRef Exp = Solver->getExpr(Ctx, Sym, &RetTy, &hasComparison); + +// Create zero comparison for implicit boolean cast, with reversed +// assumption +if (!hasComparison && !RetTy->isBooleanType()) + return assumeExpr(State, Sym, +Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption)); + +return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp)); + } ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, - bool InRange) override; + bool InRange) override { +ASTContext &Ctx = getBasicVals().getContext(); +return assumeExpr(State, Sym, + Solver->getRangeExpr(Ctx, Sym, From, To, InRange)); + } ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, - bool Assumption) override; + bool Assumption) override { +// Skip anything that is unsupported +return State; + } //===--===// // Implementation for interface from ConstraintManager. //===--===// - ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override; + ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override { +ASTContext &Ctx = getBasicVals().getContext(); + +QualType RetTy; +// The expression may be casted, so we cannot call getZ3DataExpr() directly +SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy); +SMTExprRef Exp = +Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/true); + +// Negate the constraint +SMTExprRef NotExp = +Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/false); + +Solver->reset(); +addStateConstraints(State); + +Solver->push(); +Solver->addConstraint(Exp); +ConditionTruthVal isSat = Solver->check(); + +Solver->pop(); +Solver->addConstraint(NotExp); +ConditionTruthVal isNotSat = Solver->check(); + +// Zero is the only possible solution +if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse()) + return true; + +// Zero is not a solution +if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue()) + return false; + +// Zero may be a solution +return ConditionTruthVal(); + } const llvm::APSInt *getSymVal(ProgramStateRef State, -
r340534 - [analyzer] Moved all CSA code from the SMT API to a new header, `SMTConv.h`. NFC.
Author: mramalho Date: Thu Aug 23 06:21:31 2018 New Revision: 340534 URL: http://llvm.org/viewvc/llvm-project?rev=340534&view=rev Log: [analyzer] Moved all CSA code from the SMT API to a new header, `SMTConv.h`. NFC. Summary: With this patch, the SMT backend is almost completely detached from the CSA. Unfortunate consequence is that we missed the `ConditionTruthVal` from the CSA and had to use `Optional`. The Z3 solver implementation is still in the same file as the `Z3ConstraintManager`, in `lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp` though, but except for that, the SMT API can be moved to anywhere in the codebase. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin, Szelethus Differential Revision: https://reviews.llvm.org/D50772 Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=340534&r1=340533&r2=340534&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Thu Aug 23 06:21:31 2018 @@ -16,7 +16,7 @@ #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h" namespace clang { namespace ento { @@ -42,13 +42,14 @@ public: QualType RetTy; bool hasComparison; -SMTExprRef Exp = Solver->getExpr(Ctx, Sym, &RetTy, &hasComparison); +SMTExprRef Exp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison); // Create zero comparison for implicit boolean cast, with reversed // assumption if (!hasComparison && !RetTy->isBooleanType()) - return assumeExpr(State, Sym, -Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption)); + return assumeExpr( + State, Sym, + SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption)); return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp)); } @@ -58,8 +59,8 @@ public: const llvm::APSInt &To, bool InRange) override { ASTContext &Ctx = getBasicVals().getContext(); -return assumeExpr(State, Sym, - Solver->getRangeExpr(Ctx, Sym, From, To, InRange)); +return assumeExpr( +State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange)); } ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, @@ -77,31 +78,37 @@ public: QualType RetTy; // The expression may be casted, so we cannot call getZ3DataExpr() directly -SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy); +SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); SMTExprRef Exp = -Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/true); +SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true); // Negate the constraint SMTExprRef NotExp = -Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/false); +SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false); Solver->reset(); addStateConstraints(State); Solver->push(); Solver->addConstraint(Exp); -ConditionTruthVal isSat = Solver->check(); + +Optional isSat = Solver->check(); +if (!isSat.hasValue()) + return ConditionTruthVal(); Solver->pop(); Solver->addConstraint(NotExp); -ConditionTruthVal isNotSat = Solver->check(); + +Optional isNotSat = Solver->check(); +if (!isNotSat.hasValue()) + return ConditionTruthVal(); // Zero is the only possible solution -if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse()) +if (isSat.getValue() && !isNotSat.getValue()) return true; // Zero is not a solution -if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue()) +if (!isSat.getValue() && isNotSat.getValue()) return false; // Zero may be a solution @@ -120,14 +127,14 @@ public: !Ty->isSignedIntegerOrEnumerationType()); SMTExprRef Exp = - Solver->fromData(SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
r340535 - [analyzer] added cache for SMT queries in the SMTConstraintManager
Author: mramalho Date: Thu Aug 23 06:21:35 2018 New Revision: 340535 URL: http://llvm.org/viewvc/llvm-project?rev=340535&view=rev Log: [analyzer] added cache for SMT queries in the SMTConstraintManager Summary: This patch implements a new cache for the result of SMT queries; with this patch the regression tests are 25% faster. It's implemented as a `llvm::DenseMap` where the key is the hash of the set of the constraints in a state. There is still one method that does not use the cache, `getSymVal`, because it needs to get a symbol interpretation from the SMT, which is not cached yet. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin, Szelethus Differential Revision: https://reviews.llvm.org/D50773 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=340535&r1=340534&r2=340535&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Thu Aug 23 06:21:35 2018 @@ -86,29 +86,15 @@ public: SMTExprRef NotExp = SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false); -Solver->reset(); -addStateConstraints(State); - -Solver->push(); -Solver->addConstraint(Exp); - -Optional isSat = Solver->check(); -if (!isSat.hasValue()) - return ConditionTruthVal(); - -Solver->pop(); -Solver->addConstraint(NotExp); - -Optional isNotSat = Solver->check(); -if (!isNotSat.hasValue()) - return ConditionTruthVal(); +ConditionTruthVal isSat = checkModel(State, Sym, Exp); +ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp); // Zero is the only possible solution -if (isSat.getValue() && !isNotSat.getValue()) +if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse()) return true; // Zero is not a solution -if (!isSat.getValue() && isNotSat.getValue()) +if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue()) return false; // Zero may be a solution @@ -126,6 +112,10 @@ public: llvm::APSInt Value(Ctx.getTypeSize(Ty), !Ty->isSignedIntegerOrEnumerationType()); + // TODO: this should call checkModel so we can use the cache, however, + // this method tries to get the interpretation (the actual value) from + // the solver, which is currently not cached. + SMTExprRef Exp = SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty)); @@ -236,7 +226,7 @@ protected: virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym, const SMTExprRef &Exp) { // Check the model, avoid simplifying AST to save time -if (checkModel(State, Exp).isConstrainedTrue()) +if (checkModel(State, Sym, Exp).isConstrainedTrue()) return State->add( std::make_pair(Sym, static_cast(*Exp))); @@ -264,18 +254,34 @@ protected: } // Generate and check a Z3 model, using the given constraint. - ConditionTruthVal checkModel(ProgramStateRef State, + ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym, const SMTExprRef &Exp) const { +ProgramStateRef NewState = State->add( +std::make_pair(Sym, static_cast(*Exp))); + +llvm::FoldingSetNodeID ID; +NewState->get().Profile(ID); + +unsigned hash = ID.ComputeHash(); +auto I = Cached.find(hash); +if (I != Cached.end()) + return I->second; + Solver->reset(); -Solver->addConstraint(Exp); -addStateConstraints(State); +addStateConstraints(NewState); Optional res = Solver->check(); if (!res.hasValue()) - return ConditionTruthVal(); + Cached[hash] = ConditionTruthVal(); +else + Cached[hash] = ConditionTruthVal(res.getValue()); -return ConditionTruthVal(res.getValue()); +return Cached[hash]; } + + // Cache the result of an SMT query (true, false, unknown). The key is the + // hash of the constraints in a state + mutable llvm::DenseMap Cached; }; // end class SMTConstraintManager } // namespace ento ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r337472 - [analyzer] Memoize complexity of SymExpr
Author: mramalho Date: Thu Jul 19 10:03:12 2018 New Revision: 337472 URL: http://llvm.org/viewvc/llvm-project?rev=337472&view=rev Log: [analyzer] Memoize complexity of SymExpr Summary: This patch introduces a new member to SymExpr, which stores the symbol complexity, avoiding recalculating it every time computeComplexity() is called. Also, increase the complexity of conjured Symbols by one, so it's clear that it has a greater complexity than its underlying symbols. Reviewers: NoQ, george.karpenkov Reviewed By: NoQ, george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49232 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp cfe/trunk/lib/StaticAnalyzer/Core/SymbolManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h?rev=337472&r1=337471&r2=337472&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h Thu Jul 19 10:03:12 2018 @@ -49,6 +49,8 @@ protected: return !T.isNull() && !T->isVoidType(); } + mutable unsigned Complexity = 0; + public: virtual ~SymExpr() = default; @@ -85,7 +87,7 @@ public: symbol_iterator symbol_begin() const { return symbol_iterator(this); } static symbol_iterator symbol_end() { return symbol_iterator(); } - unsigned computeComplexity() const; + virtual unsigned computeComplexity() const = 0; /// Find the region from which this symbol originates. /// @@ -127,6 +129,10 @@ public: SymbolID getSymbolID() const { return Sym; } + unsigned computeComplexity() const override { +return 1; + }; + // Implement isa support. static inline bool classof(const SymExpr *SE) { Kind k = SE->getKind(); Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h?rev=337472&r1=337471&r2=337472&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h Thu Jul 19 10:03:12 2018 @@ -270,6 +270,12 @@ public: // Otherwise, 'To' should also be a valid type. } + unsigned computeComplexity() const override { +if (Complexity == 0) + Complexity = 1 + Operand->computeComplexity(); +return Complexity; + } + QualType getType() const override { return ToTy; } const SymExpr *getOperand() const { return Operand; } @@ -337,6 +343,12 @@ public: const SymExpr *getLHS() const { return LHS; } const llvm::APSInt &getRHS() const { return RHS; } + unsigned computeComplexity() const override { +if (Complexity == 0) + Complexity = 1 + LHS->computeComplexity(); +return Complexity; + } + static void Profile(llvm::FoldingSetNodeID& ID, const SymExpr *lhs, BinaryOperator::Opcode op, const llvm::APSInt& rhs, QualType t) { @@ -374,6 +386,12 @@ public: const SymExpr *getRHS() const { return RHS; } const llvm::APSInt &getLHS() const { return LHS; } + unsigned computeComplexity() const override { +if (Complexity == 0) + Complexity = 1 + RHS->computeComplexity(); +return Complexity; + } + static void Profile(llvm::FoldingSetNodeID& ID, const llvm::APSInt& lhs, BinaryOperator::Opcode op, const SymExpr *rhs, QualType t) { @@ -412,6 +430,12 @@ public: void dumpToStream(raw_ostream &os) const override; + unsigned computeComplexity() const override { +if (Complexity == 0) + Complexity = RHS->computeComplexity() + LHS->computeComplexity(); +return Complexity; + } + static void Profile(llvm::FoldingSetNodeID& ID, const SymExpr *lhs, BinaryOperator::Opcode op, const SymExpr *rhs, QualType t) { ID.AddInteger((unsigned) SymSymExprKind); Modified: cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp?rev=337472&r1=337471&r2=337472&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp Thu Jul 19 10:03:12 2018 @@ -390,7 +390,7 @@ unsigned AnalyzerOptions::getGraphTrimIn unsigned AnalyzerOptions::getMaxSymbolComplexit
r337915 - [analyzer] Moved static Context to class member
Author: mramalho Date: Wed Jul 25 05:49:11 2018 New Revision: 337915 URL: http://llvm.org/viewvc/llvm-project?rev=337915&view=rev Log: [analyzer] Moved static Context to class member Summary: Although it is a big patch, the changes are simple: 1. There is one `Z3_Context` now, member of the `SMTConstraintManager` class. 2. `Z3Expr`, `Z3Sort`, `Z3Model` and `Z3Solver` are constructed with a reference to the `Z3_Context` in `SMTConstraintManager`. 3. All static functions are now members of `Z3Solver`, e.g, the `SMTConstraintManager` now calls `Solver.fromBoolean(false)` instead of `Z3Expr::fromBoolean(false)`. Most of the patch only move stuff around except: 1. New method `Z3Sort MkSort(const QualType &Ty, unsigned BitWidth)`, that creates a sort based on the `QualType` and its width. Used to simplify the `fromData` method. Unfortunate consequence of this patch: 1. `getInterpretation` was moved from `Z3Model` class to `Z3Solver`, because it needs to create a `Z3Sort` before returning the interpretation. This can be fixed by changing both `toAPFloat` and `toAPSInt` by removing the dependency of `Z3Sort` (it's only used to check which Sort was created and to retrieve the type width). Reviewers: NoQ, george.karpenkov, ddcc Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49236 Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337915&r1=337914&r2=337915&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jul 25 05:49:11 2018 @@ -64,48 +64,55 @@ public: ~Z3Config() { Z3_del_config(Config); } }; // end class Z3Config +void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) { + llvm::report_fatal_error("Z3 error: " + + llvm::Twine(Z3_get_error_msg_ex(Context, Error))); +} + class Z3Context : public SMTContext { public: - static Z3_context ZC; + Z3_context Context; Z3Context() : SMTContext() { Context = Z3_mk_context_rc(Z3Config().Config); -ZC = Context; +Z3_set_error_handler(Context, Z3ErrorHandler); } - ~Z3Context() { -Z3_del_context(ZC); + virtual ~Z3Context() { +Z3_del_context(Context); Context = nullptr; } - -protected: - Z3_context Context; }; // end class Z3Context class Z3Sort { friend class Z3Expr; + friend class Z3Solver; + + Z3Context &Context; Z3_sort Sort; - Z3Sort() : Sort(nullptr) {} - Z3Sort(Z3_sort ZS) : Sort(ZS) { -Z3_inc_ref(Z3Context::ZC, reinterpret_cast(Sort)); + Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) { +assert(C.Context != nullptr); +Z3_inc_ref(Context.Context, reinterpret_cast(Sort)); } public: /// Override implicit copy constructor for correct reference counting. - Z3Sort(const Z3Sort &Copy) : Sort(Copy.Sort) { -Z3_inc_ref(Z3Context::ZC, reinterpret_cast(Sort)); + Z3Sort(const Z3Sort &Copy) : Context(Copy.Context), Sort(Copy.Sort) { +Z3_inc_ref(Context.Context, reinterpret_cast(Sort)); } /// Provide move constructor - Z3Sort(Z3Sort &&Move) : Sort(nullptr) { *this = std::move(Move); } + Z3Sort(Z3Sort &&Move) : Context(Move.Context), Sort(nullptr) { +*this = std::move(Move); + } /// Provide move assignment constructor Z3Sort &operator=(Z3Sort &&Move) { if (this != &Move) { if (Sort) -Z3_dec_ref(Z3Context::ZC, reinterpret_cast(Sort)); +Z3_dec_ref(Context.Context, reinterpret_cast(Sort)); Sort = Move.Sort; Move.Sort = nullptr; } @@ -114,75 +121,38 @@ public: ~Z3Sort() { if (Sort) - Z3_dec_ref(Z3Context::ZC, reinterpret_cast(Sort)); - } - - // Return a boolean sort. - static Z3Sort getBoolSort() { return Z3Sort(Z3_mk_bool_sort(Z3Context::ZC)); } - - // Return an appropriate bitvector sort for the given bitwidth. - static Z3Sort getBitvectorSort(unsigned BitWidth) { -return Z3Sort(Z3_mk_bv_sort(Z3Context::ZC, BitWidth)); - } - - // Return an appropriate floating-point sort for the given bitwidth. - static Z3Sort getFloatSort(unsigned BitWidth) { -Z3_sort Sort; - -switch (BitWidth) { -default: - llvm_unreachable("Unsupported floating-point bitwidth!"); - break; -case 16: - Sort = Z3_mk_fpa_sort_16(Z3Context::ZC); - break; -case 32: - Sort = Z3_mk_fpa_sort_32(Z3Context::ZC); - break; -case 64: - Sort = Z3_mk_fpa_sort_64(Z3Context::ZC); - break; -case 128: - Sort = Z3_mk_fpa_sort_128(Z3Context::ZC); - break; -} -return Z3Sort(Sort); - } - - // Return an appropriate sort for the given AST. - static Z3Sort getSort(Z3_
r337917 - [analyzer] Create generic SMT Expr class
Author: mramalho Date: Wed Jul 25 05:49:19 2018 New Revision: 337917 URL: http://llvm.org/viewvc/llvm-project?rev=337917&view=rev Log: [analyzer] Create generic SMT Expr class Summary: New base class for all future SMT Exprs. No major changes except moving `areEquivalent` and `getFloatSemantics` outside of `Z3Expr` to keep the class minimal. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49551 Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h?rev=337917&view=auto == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h (added) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h Wed Jul 25 05:49:19 2018 @@ -0,0 +1,57 @@ +//== SMTExpr.h --*- C++ -*--==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===--===// +// +// This file defines a SMT generic Expr API, which will be the base class +// for every SMT solver expr specific class. +// +//===--===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H + +#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h" + +namespace clang { +namespace ento { + +class SMTExpr { +public: + SMTExpr() = default; + virtual ~SMTExpr() = default; + + bool operator<(const SMTExpr &Other) const { +llvm::FoldingSetNodeID ID1, ID2; +Profile(ID1); +Other.Profile(ID2); +return ID1 < ID2; + } + + virtual void Profile(llvm::FoldingSetNodeID &ID) const { +static int Tag = 0; +ID.AddPointer(&Tag); + } + + friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) { +return LHS.equal_to(RHS); + } + + virtual void print(raw_ostream &OS) const = 0; + + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } + +protected: + virtual bool equal_to(SMTExpr const &other) const = 0; +}; + +using SMTExprRef = std::shared_ptr; + +} // namespace ento +} // namespace clang + +#endif Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337917&r1=337916&r2=337917&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jul 25 05:49:19 2018 @@ -12,6 +12,7 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h" #include "clang/Config/config.h" @@ -162,40 +163,25 @@ public: } }; // end class Z3Sort -class Z3Expr { - friend class Z3Model; +class Z3Expr : public SMTExpr { friend class Z3Solver; Z3Context &Context; Z3_ast AST; - Z3Expr(Z3Context &C, Z3_ast ZA) : Context(C), AST(ZA) { -assert(C.Context != nullptr); + Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) { Z3_inc_ref(Context.Context, AST); } - // Determine whether two float semantics are equivalent - static bool areEquivalent(const llvm::fltSemantics &LHS, -const llvm::fltSemantics &RHS) { -return (llvm::APFloat::semanticsPrecision(LHS) == -llvm::APFloat::semanticsPrecision(RHS)) && - (llvm::APFloat::semanticsMinExponent(LHS) == -llvm::APFloat::semanticsMinExponent(RHS)) && - (llvm::APFloat::semanticsMaxExponent(LHS) == -llvm::APFloat::semanticsMaxExponent(RHS)) && - (llvm::APFloat::semanticsSizeInBits(LHS) == -llvm::APFloat::semanticsSizeInBits(RHS)); - } - public: /// Override implicit copy constructor for correct reference counting. - Z3Expr(const Z3Expr &Copy) : Context(Copy.Context), AST(Copy.AST) { + Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) { Z3_inc_ref(Context.Context, AST); } /// Provide move constructor - Z3Expr(Z3Expr &&Move) : Context(Move.Context), AST(nullptr) { + Z3Expr(Z3Expr &&Mov
r337916 - [analyzer] Create generic SMT Sort Class
Author: mramalho Date: Wed Jul 25 05:49:15 2018 New Revision: 337916 URL: http://llvm.org/viewvc/llvm-project?rev=337916&view=rev Log: [analyzer] Create generic SMT Sort Class Summary: New base class for all future SMT sorts. The only change is that the class implements methods `isBooleanSort()`, `isBitvectorSort()` and `isFloatSort()` so it doesn't rely on `Z3`'s enum. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49550 Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h?rev=337916&view=auto == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h (added) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h Wed Jul 25 05:49:15 2018 @@ -0,0 +1,71 @@ +//== SMTSort.h --*- C++ -*--==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===--===// +// +// This file defines a SMT generic Sort API, which will be the base class +// for every SMT solver sort specific class. +// +//===--===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H + +namespace clang { +namespace ento { + +class SMTSort { +public: + SMTSort() = default; + virtual ~SMTSort() = default; + + virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); } + virtual bool isFloatSort() const { return isFloatSortImpl(); } + virtual bool isBooleanSort() const { return isBooleanSortImpl(); } + + virtual unsigned getBitvectorSortSize() const { +assert(isBitvectorSort() && "Not a bitvector sort!"); +unsigned Size = getBitvectorSortSizeImpl(); +assert(Size && "Size is zero!"); +return Size; + }; + + virtual unsigned getFloatSortSize() const { +assert(isFloatSort() && "Not a floating-point sort!"); +unsigned Size = getFloatSortSizeImpl(); +assert(Size && "Size is zero!"); +return Size; + }; + + friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) { +return LHS.equal_to(RHS); + } + + virtual void print(raw_ostream &OS) const = 0; + + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } + +protected: + virtual bool equal_to(SMTSort const &other) const = 0; + + virtual bool isBitvectorSortImpl() const = 0; + + virtual bool isFloatSortImpl() const = 0; + + virtual bool isBooleanSortImpl() const = 0; + + virtual unsigned getBitvectorSortSizeImpl() const = 0; + + virtual unsigned getFloatSortSizeImpl() const = 0; +}; + +using SMTSortRef = std::shared_ptr; + +} // namespace ento +} // namespace clang + +#endif Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337916&r1=337915&r2=337916&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jul 25 05:49:15 2018 @@ -12,6 +12,7 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h" #include "clang/Config/config.h" @@ -84,27 +85,26 @@ public: } }; // end class Z3Context -class Z3Sort { - friend class Z3Expr; +class Z3Sort : public SMTSort { friend class Z3Solver; Z3Context &Context; Z3_sort Sort; - Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) { -assert(C.Context != nullptr); + Z3Sort(Z3Context &C, Z3_sort ZS) : SMTSort(), Context(C), Sort(ZS) { Z3_inc_ref(Context.Context, reinterpret_cast(Sort)); } public: /// Override implicit copy constructor for correct reference counting. - Z3Sort(const Z3Sort &Copy) : Context(Copy.Context), Sort(Copy.Sort) { + Z3Sort(const Z3Sort &Copy) + : SMTSort(), Context(Copy.Context), Sort(Copy.Sort) { Z3_inc_ref(Context.Context, reinterpret_cast(Sort)); } /// Provide move constructor - Z3Sort(Z3Sort &&Move) : Context(Move.Context), Sort(nullptr) { + Z3Sort(Z3Sort &&Move) : SMTSort(), Context(Move.Context), Sort(nullptr) {
r337918 - [analyzer] Implemented SMT generic API
Author: mramalho Date: Wed Jul 25 05:49:23 2018 New Revision: 337918 URL: http://llvm.org/viewvc/llvm-project?rev=337918&view=rev Log: [analyzer] Implemented SMT generic API Summary: Created new SMT generic API. Small changes to `Z3ConstraintManager` because of the new generic objects (`SMTSort` and `SMTExpr`) returned by `SMTSolver`. Reviewers: george.karpenkov, NoQ Reviewed By: george.karpenkov Subscribers: mgorny, xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49495 Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=337918&view=auto == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (added) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Wed Jul 25 05:49:23 2018 @@ -0,0 +1,546 @@ +//== SMTSolver.h *- C++ -*--==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===--===// +// +// This file defines a SMT generic Solver API, which will be the base class +// for every SMT solver specific class. +// +//===--===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H + +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h" + +namespace clang { +namespace ento { + +class SMTSolver { +public: + SMTSolver() = default; + virtual ~SMTSolver() = default; + + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } + + // Return an appropriate floating-point sort for the given bitwidth. + SMTSortRef getFloatSort(unsigned BitWidth) { +switch (BitWidth) { +case 16: + return getFloat16Sort(); +case 32: + return getFloat32Sort(); +case 64: + return getFloat64Sort(); +case 128: + return getFloat128Sort(); +default:; +} +llvm_unreachable("Unsupported floating-point bitwidth!"); + } + + // Return an appropriate sort, given a QualType + SMTSortRef mkSort(const QualType &Ty, unsigned BitWidth) { +if (Ty->isBooleanType()) + return getBoolSort(); + +if (Ty->isRealFloatingType()) + return getFloatSort(BitWidth); + +return getBitvectorSort(BitWidth); + } + + /// Construct a Z3Expr from a unary operator, given a Z3_context. + SMTExprRef fromUnOp(const UnaryOperator::Opcode Op, const SMTExprRef &Exp) { +switch (Op) { +case UO_Minus: + return mkBVNeg(Exp); + +case UO_Not: + return mkBVNot(Exp); + +case UO_LNot: + return mkNot(Exp); + +default:; +} +llvm_unreachable("Unimplemented opcode"); + } + + /// Construct a Z3Expr from a floating-point unary operator, given a + /// Z3_context. + SMTExprRef fromFloatUnOp(const UnaryOperator::Opcode Op, + const SMTExprRef &Exp) { +switch (Op) { +case UO_Minus: + return mkFPNeg(Exp); + +case UO_LNot: + return fromUnOp(Op, Exp); + +default:; +} +llvm_unreachable("Unimplemented opcode"); + } + + /// Construct a Z3Expr from a n-ary binary operator. + SMTExprRef fromNBinOp(const BinaryOperator::Opcode Op, +const std::vector &ASTs) { +assert(!ASTs.empty()); + +if (Op != BO_LAnd && Op != BO_LOr) + llvm_unreachable("Unimplemented opcode"); + +SMTExprRef res = ASTs.front(); +for (std::size_t i = 1; i < ASTs.size(); ++i) + res = (Op == BO_LAnd) ? mkAnd(res, ASTs[i]) : mkOr(res, ASTs[i]); +return res; + } + + /// Construct a Z3Expr from a binary operator, given a Z3_context. + SMTExprRef fromBinOp(const SMTExprRef &LHS, const BinaryOperator::Opcode Op, + const SMTExprRef &RHS, bool isSigned) { +assert(*getSort(LHS) == *getSort(RHS) && "AST's must have the same sort!"); + +switch (Op) { +// Multiplicative operators +case BO_Mul: + return mkBVMul(LHS, RHS); + +case BO_Div: + return isSigned ? mkBVSDiv(LHS, RHS) : mkBVUDiv(LHS, RHS); + +case BO_Rem: + return isSigned ? mkBVSRem(LHS, RHS) : mkBVURem(LHS, RHS); + + // Additive operators +case BO_Add: + return mkBVAdd(LHS, RHS); + +case BO_Sub: + return mkBVSub(LHS, RHS); + + // Bitwise shift operators +case BO_Shl: + return mkBVShl(LHS, RHS); + +case BO_Shr: + return isSigned ? mkB
r337914 - [analyzer] Create generic SMT Context class
Author: mramalho Date: Wed Jul 25 05:49:07 2018 New Revision: 337914 URL: http://llvm.org/viewvc/llvm-project?rev=337914&view=rev Log: [analyzer] Create generic SMT Context class Summary: This patch creates `SMTContext` which will wrap a specific SMT context, through `SMTSolverContext`. The templated `SMTSolverContext` class it's a simple wrapper around a SMT specific context (currently only used in the Z3 backend), while `Z3Context` inherits `SMTSolverContext` and implements solver specific operations like initialization and destruction of the context. This separation was done because: 1. We might want to keep one single context, shared across different `SMTConstraintManager`s. It can be achieved by constructing a `SMTContext`, through a function like `CreateSMTContext(Z3)`, `CreateSMTContext(BOOLECTOR)`, etc. The rest of the CSA only need to know about `SMTContext`, so maybe it's a good idea moving `SMTSolverContext` to a separate header in the future. 2. Any generic SMT operation will only require one `SMTSolverContext`object, which can access the specific context by calling `getContext()`. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49233 Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h?rev=337914&view=auto == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h (added) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h Wed Jul 25 05:49:07 2018 @@ -0,0 +1,30 @@ +//== SMTContext.h ---*- C++ -*--==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===--===// +// +// This file defines a SMT generic Context API, which will be the base class +// for every SMT solver context specific class. +// +//===--===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONTEXT_H +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONTEXT_H + +namespace clang { +namespace ento { + +class SMTContext { +public: + SMTContext() = default; + virtual ~SMTContext() = default; +}; + +} // namespace ento +} // namespace clang + +#endif Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337914&r1=337913&r2=337914&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jul 25 05:49:07 2018 @@ -11,6 +11,7 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h" #include "clang/Config/config.h" @@ -63,19 +64,22 @@ public: ~Z3Config() { Z3_del_config(Config); } }; // end class Z3Config -class Z3Context { - Z3_context ZC_P; - +class Z3Context : public SMTContext { public: static Z3_context ZC; - Z3Context() : ZC_P(Z3_mk_context_rc(Z3Config().Config)) { ZC = ZC_P; } + Z3Context() : SMTContext() { +Context = Z3_mk_context_rc(Z3Config().Config); +ZC = Context; + } ~Z3Context() { Z3_del_context(ZC); -Z3_finalize_memory(); -ZC_P = nullptr; +Context = nullptr; } + +protected: + Z3_context Context; }; // end class Z3Context class Z3Sort { ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r337919 - [analyzer] Moved non solver specific code from Z3ConstraintManager to SMTConstraintManager
Author: mramalho Date: Wed Jul 25 05:49:29 2018 New Revision: 337919 URL: http://llvm.org/viewvc/llvm-project?rev=337919&view=rev Log: [analyzer] Moved non solver specific code from Z3ConstraintManager to SMTConstraintManager Summary: This patch moves a lot of code from `Z3ConstraintManager` to `SMTConstraintManager`, leaving only the necessary: * `canReasonAbout` which returns if a Solver can handle a given `SVal` (should be moved to `SMTSolver` in the future). * `removeDeadBindings`, `assumeExpr` and `print`: methods that need to use `ConstraintZ3Ty`, can probably be moved to `SMTConstraintManager` in the future. The patch creates a new file, `SMTConstraintManager.cpp` with the moved code. Conceptually, this is move in the right direction and needs further improvements: `SMTConstraintManager` still does a lot of things that are not required by a `ConstraintManager`. We ought to move the unrelated to `SMTSolver` and remove everything that's not related to a `ConstraintManager`. In particular, we could remove `addRangeConstraints` and `isModelFeasible`, and make the refutation manager create an Z3Solver directly. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: mgorny, xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49668 Added: cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=337919&r1=337918&r2=337919&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Wed Jul 25 05:49:29 2018 @@ -16,27 +16,254 @@ #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h" namespace clang { namespace ento { class SMTConstraintManager : public clang::ento::SimpleConstraintManager { + SMTSolverRef &Solver; public: - SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB) - : SimpleConstraintManager(SE, SB) {} + SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB, + SMTSolverRef &S) + : SimpleConstraintManager(SE, SB), Solver(S) {} virtual ~SMTConstraintManager() = default; + //===--===// + // Implementation for interface from SimpleConstraintManager. + //===--===// + + ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym, +bool Assumption) override; + + ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, + const llvm::APSInt &From, + const llvm::APSInt &To, + bool InRange) override; + + ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, + bool Assumption) override; + + //===--===// + // Implementation for interface from ConstraintManager. + //===--===// + + ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override; + + const llvm::APSInt *getSymVal(ProgramStateRef State, +SymbolRef Sym) const override; + /// Converts the ranged constraints of a set of symbols to SMT /// /// \param CR The set of constraints. - virtual void addRangeConstraints(clang::ento::ConstraintRangeTy CR) = 0; + void addRangeConstraints(clang::ento::ConstraintRangeTy CR); /// Checks if the added constraints are satisfiable - virtual clang::ento::ConditionTruthVal isModelFeasible() = 0; + clang::ento::ConditionTruthVal isModelFeasible(); /// Dumps SMT formula - LLVM_DUMP_METHOD virtual void dump() const = 0; + LLVM_DUMP_METHOD void dump() const { Solver->dump(); } + +protected: + //===--===// + // Internal implementation. + //===--===// + + // Check whether a new model is satisfiable, and update the program state. + virtual ProgramStateRef assumeExpr(ProgramS
r337920 - [analyzer] Try to minimize the number of equivalent bug reports evaluated by the refutation manager
Author: mramalho Date: Wed Jul 25 05:49:32 2018 New Revision: 337920 URL: http://llvm.org/viewvc/llvm-project?rev=337920&view=rev Log: [analyzer] Try to minimize the number of equivalent bug reports evaluated by the refutation manager Summary: This patch changes how the SMT bug refutation runs in an equivalent bug report class. Now, all other visitor are executed until they find a valid bug or mark all bugs as invalid. When the one valid bug is found (and crosscheck is enabled), the SMT refutation checks the satisfiability of this single bug. If the bug is still valid after checking with Z3, it is returned and a bug report is created. If the bug is found to be invalid, the next bug report in the equivalent class goes through the same process, until we find a valid bug or all bugs are marked as invalid. Massive speedups when verifying redis/src/rax.c, from 1500s to 10s. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49693 Modified: cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp Modified: cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp?rev=337920&r1=337919&r2=337920&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp Wed Jul 25 05:49:32 2018 @@ -2605,8 +2605,6 @@ std::pairaddVisitor(llvm::make_unique()); -if (Opts.shouldCrosscheckWithZ3()) - R->addVisitor(llvm::make_unique()); // Register additional node visitors. R->addVisitor(llvm::make_unique()); @@ -2619,9 +2617,24 @@ std::pair visitorNotes = generateVisitorsDiagnostics(R, ErrorNode, BRC); -if (R->isValid()) - return std::make_pair(R, std::move(visitorNotes)); +if (R->isValid()) { + if (Opts.shouldCrosscheckWithZ3()) { +// If crosscheck is enabled, remove all visitors, add the refutation +// visitor and check again +R->clearVisitors(); +R->addVisitor(llvm::make_unique()); + +// We don't overrite the notes inserted by other visitors because the +// refutation manager does not add any new note to the path +generateVisitorsDiagnostics(R, ErrorGraph.ErrorNode, BRC); + } + + // Check if the bug is still valid + if (R->isValid()) +return std::make_pair(R, std::move(visitorNotes)); +} } + return std::make_pair(nullptr, llvm::make_unique()); } ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r337921 - [analyzer] Moved code from SMTConstraintManager to SMTSolver
Author: mramalho Date: Wed Jul 25 05:49:37 2018 New Revision: 337921 URL: http://llvm.org/viewvc/llvm-project?rev=337921&view=rev Log: [analyzer] Moved code from SMTConstraintManager to SMTSolver Summary: This is the second part of D49668, and moves all the code that's not specific to a ConstraintManager to SMTSolver. No functional change intended. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49767 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=337921&r1=337920&r2=337921&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Wed Jul 25 05:49:37 2018 @@ -81,189 +81,6 @@ protected: // Generate and check a Z3 model, using the given constraint. ConditionTruthVal checkModel(ProgramStateRef State, const SMTExprRef &Exp) const; - - // Generate a Z3Expr that represents the given symbolic expression. - // Sets the hasComparison parameter if the expression has a comparison - // operator. - // Sets the RetTy parameter to the final return type after promotions and - // casts. - SMTExprRef getExpr(SymbolRef Sym, QualType *RetTy = nullptr, - bool *hasComparison = nullptr) const; - - // Generate a Z3Expr that takes the logical not of an expression. - SMTExprRef getNotExpr(const SMTExprRef &Exp) const; - - // Generate a Z3Expr that compares the expression to zero. - SMTExprRef getZeroExpr(const SMTExprRef &Exp, QualType RetTy, - bool Assumption) const; - - // Recursive implementation to unpack and generate symbolic expression. - // Sets the hasComparison and RetTy parameters. See getZ3Expr(). - SMTExprRef getSymExpr(SymbolRef Sym, QualType *RetTy, -bool *hasComparison) const; - - // Wrapper to generate Z3Expr from SymbolData. - SMTExprRef getDataExpr(const SymbolID ID, QualType Ty) const; - - // Wrapper to generate Z3Expr from SymbolCast. - SMTExprRef getCastExpr(const SMTExprRef &Exp, QualType FromTy, - QualType Ty) const; - - // Wrapper to generate Z3Expr from BinarySymExpr. - // Sets the hasComparison and RetTy parameters. See getZ3Expr(). - SMTExprRef getSymBinExpr(const BinarySymExpr *BSE, bool *hasComparison, - QualType *RetTy) const; - - // Wrapper to generate Z3Expr from unpacked binary symbolic expression. - // Sets the RetTy parameter. See getZ3Expr(). - SMTExprRef getBinExpr(const SMTExprRef &LHS, QualType LTy, -BinaryOperator::Opcode Op, const SMTExprRef &RHS, -QualType RTy, QualType *RetTy) const; - - // Wrapper to generate Z3Expr from a range. If From == To, an equality will - // be created instead. - SMTExprRef getRangeExpr(SymbolRef Sym, const llvm::APSInt &From, - const llvm::APSInt &To, bool InRange); - - //===--===// - // Helper functions. - //===--===// - - // Recover the QualType of an APSInt. - // TODO: Refactor to put elsewhere - QualType getAPSIntType(const llvm::APSInt &Int) const; - - // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1. - std::pair fixAPSInt(const llvm::APSInt &Int) const; - - // Perform implicit type conversion on binary symbolic expressions. - // May modify all input parameters. - // TODO: Refactor to use built-in conversion functions - void doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS, QualTypeisPromotableIntegerType()) { - QualType NewTy = Ctx.getPromotedInteg
r337922 - [analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and replace by proper calls to SMTSolver
Author: mramalho Date: Wed Jul 25 05:49:43 2018 New Revision: 337922 URL: http://llvm.org/viewvc/llvm-project?rev=337922&view=rev Log: [analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and replace by proper calls to SMTSolver Summary: Third patch in the refactoring series, to decouple the SMT Solver from the Refutation Manager (1st: D49668, 2nd: D49767). The refutation API in the `SMTConstraintManager` was a hack to allow us to create an SMT solver and verify the constraints; it was conceptually wrong from the start. Now, we don't actually need to use the `SMTConstraintManager` and can create an SMT object directly, add the constraints and check them. While updating the Falsification visitor, I inlined the two functions that were used to collect the constraints and add them to the solver. As a result of this patch, we could move the SMT API elsewhere and as it's not really dependent on the CSA anymore. Maybe we can create a new dir (utils/smt) for Z3 and future solvers? Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49768 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=337922&r1=337921&r2=337922&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Wed Jul 25 05:49:43 2018 @@ -54,14 +54,6 @@ public: const llvm::APSInt *getSymVal(ProgramStateRef State, SymbolRef Sym) const override; - /// Converts the ranged constraints of a set of symbols to SMT - /// - /// \param CR The set of constraints. - void addRangeConstraints(clang::ento::ConstraintRangeTy CR); - - /// Checks if the added constraints are satisfiable - clang::ento::ConditionTruthVal isModelFeasible(); - /// Dumps SMT formula LLVM_DUMP_METHOD void dump() const { Solver->dump(); } Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=337922&r1=337921&r2=337922&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Wed Jul 25 05:49:43 2018 @@ -954,6 +954,8 @@ public: using SMTSolverRef = std::shared_ptr; +std::unique_ptr CreateZ3Solver(); + } // namespace ento } // namespace clang Modified: cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp?rev=337922&r1=337921&r2=337922&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp Wed Jul 25 05:49:43 2018 @@ -2370,34 +2370,6 @@ TaintBugVisitor::VisitNode(const Explode return std::make_shared(L, "Taint originated here"); } -static bool areConstraintsUnfeasible(BugReporterContext &BRC, - const ConstraintRangeTy &Cs) { - // Create a refutation manager - std::unique_ptr RefutationMgr = CreateZ3ConstraintManager( - BRC.getStateManager(), BRC.getStateManager().getOwningEngine()); - - SMTConstraintManager *SMTRefutationMgr = - static_cast(RefutationMgr.get()); - - // Add constraints to the solver - SMTRefutationMgr->addRangeConstraints(Cs); - - // And check for satisfiability - return SMTRefutationMgr->isModelFeasible().isConstrainedFalse(); -} - -static void addNewConstraints(ConstraintRangeTy &Cs, - const ConstraintRangeTy &NewCs, - ConstraintRangeTy::Factory &CF) { - // Add constraints if we don't have them yet - for (auto const &C : NewCs) { -const SymbolRef &Sym = C.first; -if (!Cs.contains(Sym)) { - Cs = CF.add(Cs, Sym, C.second); -} - } -} - FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor() : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {} @@ -2406,8 +2378,26 @@ void FalsePositiveRefut
r337923 - [analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 backend
Author: mramalho Date: Wed Jul 25 05:49:47 2018 New Revision: 337923 URL: http://llvm.org/viewvc/llvm-project?rev=337923&view=rev Log: [analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 backend Summary: The macro was manually expanded in the Z3 backend and this patch adds it back. Adding the expanded code is dangerous as the macro may change in the future and the expanded code might be left outdated. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49769 Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337923&r1=337922&r2=337923&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jul 25 05:49:47 2018 @@ -25,28 +25,6 @@ using namespace ento; #include -// Forward declarations -namespace { -class Z3Expr; -class ConstraintZ3 {}; -} // end anonymous namespace - -typedef llvm::ImmutableSet> ConstraintZ3Ty; - -// Expansion of REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, Z3SetPair) -namespace clang { -namespace ento { -template <> -struct ProgramStateTrait -: public ProgramStatePartialTrait { - static void *GDMIndex() { -static int Index; -return &Index; - } -}; -} // end namespace ento -} // end namespace clang - namespace { class Z3Config { @@ -313,6 +291,13 @@ static bool areEquivalent(const llvm::fl llvm::APFloat::semanticsSizeInBits(RHS)); } +} // end anonymous namespace + +typedef llvm::ImmutableSet> ConstraintZ3Ty; +REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, ConstraintZ3Ty) + +namespace { + class Z3Solver : public SMTSolver { friend class Z3ConstraintManager; ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r337948 - [analyzer] Fix compilation when LLVM_ENABLE_MODULES=ON
Author: mramalho Date: Wed Jul 25 11:26:50 2018 New Revision: 337948 URL: http://llvm.org/viewvc/llvm-project?rev=337948&view=rev Log: [analyzer] Fix compilation when LLVM_ENABLE_MODULES=ON Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h?rev=337948&r1=337947&r2=337948&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h Wed Jul 25 11:26:50 2018 @@ -15,7 +15,8 @@ #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H -#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h" +#include "clang/Basic/TargetInfo.h" +#include "llvm/ADT/FoldingSet.h" namespace clang { namespace ento { Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=337948&r1=337947&r2=337948&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Wed Jul 25 11:26:50 2018 @@ -15,8 +15,12 @@ #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H +#include "clang/AST/Expr.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h" namespace clang { namespace ento { Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h?rev=337948&r1=337947&r2=337948&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h Wed Jul 25 11:26:50 2018 @@ -15,6 +15,8 @@ #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H +#include "clang/Basic/TargetInfo.h" + namespace clang { namespace ento { ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r337954 - [analyzer] Update SMT API documentation and methods
Author: mramalho Date: Wed Jul 25 12:34:48 2018 New Revision: 337954 URL: http://llvm.org/viewvc/llvm-project?rev=337954&view=rev Log: [analyzer] Update SMT API documentation and methods Summary: Update the documentation of all the classes introduced with the new generic SMT API, most of them were referencing Z3 and how previous operations were being done (like including the context as parameter in a few methods). Renamed the following methods, so it's clear that the operate on bitvectors: *`mkSignExt` -> `mkBVSignExt` *`mkZeroExt` -> `mkBVZeroExt` *`mkExtract` -> `mkBVExtract` *`mkConcat` -> `mkBVConcat` Removed the unecessary methods: * `getDataExpr`: it was an one line method that called `fromData` * `mkBitvector(const llvm::APSInt Int)`: it was not being used anywhere Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49799 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=337954&r1=337953&r2=337954&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Wed Jul 25 12:34:48 2018 @@ -58,10 +58,6 @@ public: LLVM_DUMP_METHOD void dump() const { Solver->dump(); } protected: - //===--===// - // Internal implementation. - //===--===// - // Check whether a new model is satisfiable, and update the program state. virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym, const SMTExprRef &Exp) = 0; Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h?rev=337954&r1=337953&r2=337954&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h Wed Jul 25 12:34:48 2018 @@ -18,6 +18,7 @@ namespace clang { namespace ento { +/// Generic base class for SMT contexts class SMTContext { public: SMTContext() = default; Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h?rev=337954&r1=337953&r2=337954&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h Wed Jul 25 12:34:48 2018 @@ -21,6 +21,7 @@ namespace clang { namespace ento { +/// Generic base class for SMT exprs class SMTExpr { public: SMTExpr() = default; @@ -47,9 +48,12 @@ public: LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } protected: + /// Query the SMT solver and returns true if two sorts are equal (same kind + /// and bit width). This does not check if the two sorts are the same objects. virtual bool equal_to(SMTExpr const &other) const = 0; }; +/// Shared pointer for SMTExprs, used by SMTSolver API. using SMTExprRef = std::shared_ptr; } // namespace ento Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=337954&r1=337953&r2=337954&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Wed Jul 25 12:34:48 2018 @@ -25,6 +25,11 @@ namespace clang { namespace ento { +/// Generic base class for SMT Solvers +/// +/// This class is responsible for wrapping all sorts and expression generation, +/// through the mk* methods. It also provides met
r338020 - [analyzer] Fixed method to get APSInt model
Author: mramalho Date: Thu Jul 26 04:17:13 2018 New Revision: 338020 URL: http://llvm.org/viewvc/llvm-project?rev=338020&view=rev Log: [analyzer] Fixed method to get APSInt model Summary: This patch replaces the current method of getting an `APSInt` from Z3's model by calling generic API method `getBitvector` instead of `Z3_get_numeral_uint64`. By calling `getBitvector`, there's no need to handle bitvectors with bit width == 128 separately. And, as a bonus, clang now compiles correctly with Z3 4.7.1. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49818 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=338020&r1=338019&r2=338020&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Thu Jul 26 04:17:13 2018 @@ -931,7 +931,8 @@ public: virtual SMTExprRef getFloatRoundingMode() = 0; // If the a model is available, returns the value of a given bitvector symbol - virtual const llvm::APSInt getBitvector(const SMTExprRef &Exp) = 0; + virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, +bool isUnsigned) = 0; // If the a model is available, returns the value of a given boolean symbol virtual bool getBoolean(const SMTExprRef &Exp) = 0; Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=338020&r1=338019&r2=338020&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Thu Jul 26 04:17:13 2018 @@ -734,10 +734,11 @@ public: toZ3Sort(*Sort).Sort))); } - const llvm::APSInt getBitvector(const SMTExprRef &Exp) override { -// FIXME: this returns a string and the bitWidth is overridden -return llvm::APSInt( -Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST)); + llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, +bool isUnsigned) override { +return llvm::APSInt(llvm::APInt( +BitWidth, Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST), +10)); } bool getBoolean(const SMTExprRef &Exp) override { @@ -814,26 +815,20 @@ public: return false; } - uint64_t Value[2]; - // Force cast because Z3 defines __uint64 to be a unsigned long long - // type, which isn't compatible with a unsigned long type, even if they - // are the same size. - Z3_get_numeral_uint64(Context.Context, toZ3Expr(*AST).AST, -reinterpret_cast<__uint64 *>(&Value[0])); - if (Sort->getBitvectorSortSize() <= 64) { -Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), - Int.isUnsigned()); - } else if (Sort->getBitvectorSortSize() == 128) { -SMTExprRef ASTHigh = mkBVExtract(127, 64, AST); -Z3_get_numeral_uint64(Context.Context, toZ3Expr(*AST).AST, - reinterpret_cast<__uint64 *>(&Value[1])); -Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), - Int.isUnsigned()); - } else { -assert(false && "Bitwidth not supported!"); -return false; + // FIXME: This function is also used to retrieve floating-point values, + // which can be 16, 32, 64 or 128 bits long. Bitvectors can be anything + // between 1 and 64 bits long, which is the reason we have this weird + // guard. In the future, we need proper calls in the backend to retrieve + // floating-points and its special values (NaN, +/-infinity, +/-zero), + // then we can drop this weird condition. + if (Sort->getBitvectorSortSize() <= 64 || + Sort->getBitvectorSortSize() == 128) { +Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned()); +return true; } - return true; + + assert(false && "Bitwidth not supported!"); + return false; } if (Sort->isBooleanSort()) { ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r333529 - Fix a (possible) division by zero check in the CmpRuns script
Author: mramalho Date: Wed May 30 04:17:55 2018 New Revision: 333529 URL: http://llvm.org/viewvc/llvm-project?rev=333529&view=rev Log: Fix a (possible) division by zero check in the CmpRuns script I missed updating the check in r75 Modified: cfe/trunk/utils/analyzer/CmpRuns.py Modified: cfe/trunk/utils/analyzer/CmpRuns.py URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/utils/analyzer/CmpRuns.py?rev=333529&r1=333528&r2=333529&view=diff == --- cfe/trunk/utils/analyzer/CmpRuns.py (original) +++ cfe/trunk/utils/analyzer/CmpRuns.py Wed May 30 04:17:55 2018 @@ -311,7 +311,7 @@ def compareStats(resultsA, resultsB): report = "%.3f -> %.3f" % (valA, valB) # Only apply highlighting when writing to TTY and it's not Windows if sys.stdout.isatty() and os.name != 'nt': -if valA != 0: +if valB != 0: ratio = (valB - valA) / valB if ratio < -0.2: report = Colors.GREEN + report + Colors.CLEAR ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r333862 - Moved RangedConstraintManager header to the StaticAnalyser include dir
Author: mramalho Date: Sun Jun 3 17:23:01 2018 New Revision: 333862 URL: http://llvm.org/viewvc/llvm-project?rev=333862&view=rev Log: Moved RangedConstraintManager header to the StaticAnalyser include dir Summary: Moved `RangedConstraintManager` header from `lib/StaticAnalyzer/Core/` to `clang/StaticAnalyzer/Core/PathSensitive/`. No changes to the code. Reviewers: NoQ, george.karpenkov, dcoughlin Reviewed By: george.karpenkov Subscribers: NoQ, george.karpenkov, dcoughlin, ddcc Differential Revision: https://reviews.llvm.org/D47640 Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h - copied, changed from r333858, cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.h Removed: cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.h Modified: cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp Copied: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h (from r333858, cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.h) URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h?p2=cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h&p1=cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.h&r1=333858&r2=333862&rev=333862&view=diff == (empty) Modified: cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp?rev=333862&r1=333861&r2=333862&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp Sun Jun 3 17:23:01 2018 @@ -12,10 +12,10 @@ // //===--===// -#include "RangedConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" #include "llvm/ADT/FoldingSet.h" #include "llvm/ADT/ImmutableSet.h" #include "llvm/Support/raw_ostream.h" Modified: cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp?rev=333862&r1=333861&r2=333862&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp Sun Jun 3 17:23:01 2018 @@ -12,8 +12,8 @@ // //===--===// -#include "RangedConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" namespace clang { Removed: cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.h?rev=333861&view=auto == --- cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.h (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.h (removed) @@ -1,214 +0,0 @@ -//== RangedConstraintManager.h --*- C++ -*--==// -// -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===--===// -// -// Ranged constraint manager, built on SimpleConstraintManager. -// -//===--===// - -#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H -#define LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H - -#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h" - -namespace clang { - -namespace ento { - -/// A Range represents the closed range [from, to]. The caller must -/// guarantee that from <= to. Note that Range is immutable, so as not -/// to subvert RangeSet's immutability. -class Range : public std::pair { -public: - Range(const llvm::APSInt &from, const llvm::APSInt &to) - : std::pair(&from, &to) { -assert(from
r333903 - [analyzer] False positive refutation with Z3
Author: mramalho Date: Mon Jun 4 07:40:44 2018 New Revision: 333903 URL: http://llvm.org/viewvc/llvm-project?rev=333903&view=rev Log: [analyzer] False positive refutation with Z3 Summary: This is a prototype of a bug reporter visitor that invalidates bug reports by re-checking constraints of certain states on the bug path using the Z3 constraint manager backend. The functionality is available under the `crosscheck-with-z3` analyzer config flag. Reviewers: george.karpenkov, NoQ, dcoughlin, rnkovacs Reviewed By: george.karpenkov Subscribers: rnkovacs, NoQ, george.karpenkov, dcoughlin, xbolva00, ddcc, mikhail.ramalho, MTC, fhahn, whisperity, baloghadamsoftware, szepet, a.sidorin, gsd, dkrupp, xazax.hun, cfe-commits Differential Revision: https://reviews.llvm.org/D45517 Added: cfe/trunk/test/Analysis/z3-crosscheck.c Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h?rev=333903&r1=333902&r2=333903&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h Mon Jun 4 07:40:44 2018 @@ -280,6 +280,9 @@ private: /// \sa shouldSuppressFromCXXStandardLibrary Optional SuppressFromCXXStandardLibrary; + /// \sa shouldCrosscheckWithZ3 + Optional CrosscheckWithZ3; + /// \sa reportIssuesInMainSourceFile Optional ReportIssuesInMainSourceFile; @@ -575,6 +578,13 @@ public: /// which accepts the values "true" and "false". bool shouldSuppressFromCXXStandardLibrary(); + /// Returns whether bug reports should be crosschecked with the Z3 + /// constraint manager backend. + /// + /// This is controlled by the 'crosscheck-with-z3' config option, + /// which accepts the values "true" and "false". + bool shouldCrosscheckWithZ3(); + /// Returns whether or not the diagnostic report should be always reported /// in the main source file and not the headers. /// Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h?rev=333903&r1=333902&r2=333903&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h Mon Jun 4 07:40:44 2018 @@ -16,6 +16,7 @@ #define LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_BUGREPORTERVISITORS_H #include "clang/Basic/LLVM.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" #include "llvm/ADT/FoldingSet.h" #include "llvm/ADT/STLExtras.h" @@ -355,6 +356,27 @@ public: std::shared_ptr VisitNode(const ExplodedNode *N, const ExplodedNode *PrevN, + BugReporterContext &BRC, + BugReport &BR) override; +}; + +/// The bug visitor will walk all the nodes in a path and collect all the +/// constraints. When it reaches the root node, will create a refutation +/// manager and check if the constraints are satisfiable +class FalsePositiveRefutationBRVisitor final +: public BugReporterVisitorImpl { +private: + /// Holds the constraints in a given path + // TODO: should we use a set? + llvm::SmallVector Constraints; + +public: + FalsePositiveRefutationBRVisitor() = default; + + void Profile(llvm::FoldingSetNodeID &ID) const override; + + std::shared_ptr VisitNode(const ExplodedNode *N, + const ExplodedNode *PrevN, BugReporterContext &BRC, BugReport &BR) override; }; Modified: cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp?rev=333903&r1=333902&r2=333903&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp Mon Jun 4 07:40:44 2018 @@ -296,6 +296,12 @@ bool AnalyzerOptions::shouldSuppressFrom /* Default = */ true); }
r333899 - Created a tiny SMT interface and make Z3ConstraintManager implement it
Author: mramalho Date: Mon Jun 4 07:25:58 2018 New Revision: 333899 URL: http://llvm.org/viewvc/llvm-project?rev=333899&view=rev Log: Created a tiny SMT interface and make Z3ConstraintManager implement it Summary: This patch implements a simple SMTConstraintManager API, and requires the implementation of two methods for now: `addRangeConstraints` and `isModelFeasible`. Update Z3ConstraintManager to inherit it and implement required methods. I also moved the method to dump the SMT formula from D45517 to this patch. This patch was created based on the reviews from D47640. Reviewers: george.karpenkov, NoQ, ddcc, dcoughlin Reviewed By: george.karpenkov Differential Revision: https://reviews.llvm.org/D47689 Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=333899&view=auto == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (added) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Mon Jun 4 07:25:58 2018 @@ -0,0 +1,43 @@ +//== SMTConstraintManager.h -*- C++ -*--==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===--===// +// +// This file defines a SMT generic API, which will be the base class for +// every SMT solver specific class. +// +//===--===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H + +#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" + +namespace clang { +namespace ento { + +class SMTConstraintManager : public clang::ento::SimpleConstraintManager { + +public: + SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB) + : SimpleConstraintManager(SE, SB) {} + virtual ~SMTConstraintManager() = default; + + /// Converts the ranged constraints of a set of symbols to SMT + /// + /// \param CR The set of constraints. + virtual void addRangeConstraints(clang::ento::ConstraintRangeTy CR) = 0; + + /// Checks if the added constraints are satisfiable + virtual clang::ento::ConditionTruthVal isModelFeasible() = 0; + +}; // end class SMTConstraintManager + +} // namespace ento +} // namespace clang + +#endif Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=333899&r1=333898&r2=333899&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Mon Jun 4 07:25:58 2018 @@ -10,7 +10,7 @@ #include "clang/Basic/TargetInfo.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" #include "clang/Config/config.h" @@ -880,6 +880,12 @@ public: /// Reset the solver and remove all constraints. void reset() { Z3_solver_reset(Z3Context::ZC, Solver); } + + void print(raw_ostream &OS) const { +OS << Z3_solver_to_string(Z3Context::ZC, Solver); + } + + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } }; // end class Z3Solver void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) { @@ -887,16 +893,23 @@ void Z3ErrorHandler(Z3_context Context, llvm::Twine(Z3_get_error_msg_ex(Context, Error))); } -class Z3ConstraintManager : public SimpleConstraintManager { +class Z3ConstraintManager : public SMTConstraintManager { Z3Context Context; mutable Z3Solver Solver; public: Z3ConstraintManager(SubEngine *SE, SValBuilder &SB) - : SimpleConstraintManager(SE, SB), + : SMTConstraintManager(SE, SB), Solver(Z3_mk_simple_solver(Z3Context::ZC)) { Z3_set_error_handler(Z3Context::ZC, Z3ErrorHandler); } + //===--===// + // Implementation for Refutation. + //===--===// + + void addRangeConstraints(clang::ento::ConstraintRangeTy CR) o
r334891 - [analyzer] Add method to the generic SMT API to dump the SMT formula
Author: mramalho Date: Sat Jun 16 07:36:17 2018 New Revision: 334891 URL: http://llvm.org/viewvc/llvm-project?rev=334891&view=rev Log: [analyzer] Add method to the generic SMT API to dump the SMT formula Summary: New method dump the SMT formula and the Z3 implementation. There is no test because I only used it for debugging. However, if requested, I can add an option to the static analyzer to dump the formula (whole program? per path?), maybe something like the trimmed graph but for SMT formulas. Reviewers: NoQ, george.karpenkov, ddcc Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D48221 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=334891&r1=334890&r2=334891&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Sat Jun 16 07:36:17 2018 @@ -35,6 +35,8 @@ public: /// Checks if the added constraints are satisfiable virtual clang::ento::ConditionTruthVal isModelFeasible() = 0; + /// Dumps SMT formula + LLVM_DUMP_METHOD virtual void dump() const = 0; }; // end class SMTConstraintManager } // namespace ento Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=334891&r1=334890&r2=334891&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Sat Jun 16 07:36:17 2018 @@ -911,6 +911,8 @@ public: ConditionTruthVal isModelFeasible() override; + LLVM_DUMP_METHOD void dump() const override; + //===--===// // Implementation for interface from ConstraintManager. //===--===// @@ -1299,6 +1301,11 @@ clang::ento::ConditionTruthVal Z3Constra return ConditionTruthVal(); } +LLVM_DUMP_METHOD void Z3ConstraintManager::dump() const +{ + Solver.dump(); +} + //===--===// // Internal implementation. //===--===// ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r335116 - [analyzer] Optimize constraint generation when the range is a concrete value
Author: mramalho Date: Wed Jun 20 04:42:12 2018 New Revision: 335116 URL: http://llvm.org/viewvc/llvm-project?rev=335116&view=rev Log: [analyzer] Optimize constraint generation when the range is a concrete value Summary: If a constraint is something like: ``` $0 = [1,1] ``` it'll now be created as: ``` assert($0 == 1) ``` instead of: ``` assert($0 >= 1 && $0 <= 1) ``` In general, ~3% speedup when solving per query in my machine. Biggest improvement was when verifying sqlite3, total time went down from 3000s to 2200s. I couldn't create a test for this as there is no way to dump the formula yet. D48221 adds a method to dump the formula but there is no way to do it from the command line. Also, a test that prints the formula will most likely fail in the future, as different solvers print the formula in different formats. Reviewers: NoQ, george.karpenkov, ddcc Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D48227 Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=335116&r1=335115&r2=335116&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jun 20 04:42:12 2018 @@ -994,6 +994,11 @@ private: BinaryOperator::Opcode Op, const Z3Expr &RHS, QualType RTy, QualType *RetTy) const; + // Wrapper to generate Z3Expr from a range. If From == To, an equality will + // be created instead. + Z3Expr getZ3RangeExpr(SymbolRef Sym, const llvm::APSInt &From, +const llvm::APSInt &To, bool InRange); + //===--===// // Helper functions. //===--===// @@ -1052,35 +1057,7 @@ ProgramStateRef Z3ConstraintManager::ass ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange( ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) { - QualType RetTy; - // The expression may be casted, so we cannot call getZ3DataExpr() directly - Z3Expr Exp = getZ3Expr(Sym, &RetTy); - - QualType FromTy; - llvm::APSInt NewFromInt; - std::tie(NewFromInt, FromTy) = fixAPSInt(From); - Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt); - - // Construct single (in)equality - if (From == To) -return assumeZ3Expr(State, Sym, -getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE, - FromExp, FromTy, nullptr)); - - QualType ToTy; - llvm::APSInt NewToInt; - std::tie(NewToInt, ToTy) = fixAPSInt(To); - Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt); - assert(FromTy == ToTy && "Range values have different types!"); - // Construct two (in)equalities, and a logical and/or - Z3Expr LHS = getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, -FromTy, nullptr); - Z3Expr RHS = - getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, ToTy, nullptr); - return assumeZ3Expr( - State, Sym, - Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, -RetTy->isSignedIntegerOrEnumerationType())); + return assumeZ3Expr(State, Sym, getZ3RangeExpr(Sym, From, To, InRange)); } ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State, @@ -1264,31 +1241,14 @@ void Z3ConstraintManager::addRangeConstr SymbolRef Sym = I.first; Z3Expr Constraints = Z3Expr::fromBoolean(false); - for (const auto &Range : I.second) { - const llvm::APSInt &From = Range.From(); - const llvm::APSInt &To = Range.To(); + Z3Expr SymRange = + getZ3RangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true); - QualType FromTy; - llvm::APSInt NewFromInt; - std::tie(NewFromInt, FromTy) = fixAPSInt(From); - Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt); - QualType SymTy; - Z3Expr Exp = getZ3Expr(Sym, &SymTy); - bool IsSignedTy = SymTy->isSignedIntegerOrEnumerationType(); - QualType ToTy; - llvm::APSInt NewToInt; - std::tie(NewToInt, ToTy) = fixAPSInt(To); - Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt); - assert(FromTy == ToTy && "Range values have different types!"); - - Z3Expr LHS = - getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, FromTy, /*RetTy=*/nullptr); - Z3Expr RHS = - getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, FromTy, /*RetTy=*/nullptr); - Z3Expr SymRange = Z3Expr::fromBinOp(LHS, BO_LAnd, RHS, IsSignedTy); + // FIXME: the last argument (isSigned) is not used when generating the + // or expression, as
r345284 - [analyzer] Move canReasonAbout from Z3ConstraintManager to SMTConstraintManager
Author: mramalho Date: Thu Oct 25 10:27:42 2018 New Revision: 345284 URL: http://llvm.org/viewvc/llvm-project?rev=345284&view=rev Log: [analyzer] Move canReasonAbout from Z3ConstraintManager to SMTConstraintManager Summary: This patch moves the last method in `Z3ConstraintManager` to `SMTConstraintManager`: `canReasonAbout()`. The `canReasonAbout()` method checks if a given `SVal` can be encoded in SMT. I've added a new method to the SMT API to return true if a solver can encode floating-point arithmetics and it was enough to make `canReasonAbout()` solver independent. As an annoying side-effect, `Z3ConstraintManager` is pretty empty now and only (1) creates the Z3 solver object by calling `CreateZ3Solver()` and (2) instantiates `SMTConstraintManager`. Maybe we can get rid of this class altogether in the future: a `CreateSMTConstraintManager()` method that does (1) and (2) and returns the constraint manager object? Reviewers: george.karpenkov, NoQ Reviewed By: george.karpenkov Subscribers: mehdi_amini, xazax.hun, szepet, a.sidorin, dexonsmith, Szelethus, donat.nagy, dkrupp Differential Revision: https://reviews.llvm.org/D53694 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=345284&r1=345283&r2=345284&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Thu Oct 25 10:27:42 2018 @@ -218,6 +218,52 @@ public: OS << nl; } + bool canReasonAbout(SVal X) const override { +const TargetInfo &TI = getBasicVals().getContext().getTargetInfo(); + +Optional SymVal = X.getAs(); +if (!SymVal) + return true; + +const SymExpr *Sym = SymVal->getSymbol(); +QualType Ty = Sym->getType(); + +// Complex types are not modeled +if (Ty->isComplexType() || Ty->isComplexIntegerType()) + return false; + +// Non-IEEE 754 floating-point types are not modeled +if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) && + (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() || + &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble( + return false; + +if (Ty->isRealFloatingType()) + return Solver->isFPSupported(); + +if (isa(Sym)) + return true; + +SValBuilder &SVB = getSValBuilder(); + +if (const SymbolCast *SC = dyn_cast(Sym)) + return canReasonAbout(SVB.makeSymbolVal(SC->getOperand())); + +if (const BinarySymExpr *BSE = dyn_cast(Sym)) { + if (const SymIntExpr *SIE = dyn_cast(BSE)) +return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS())); + + if (const IntSymExpr *ISE = dyn_cast(BSE)) +return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS())); + + if (const SymSymExpr *SSE = dyn_cast(BSE)) +return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) && + canReasonAbout(SVB.makeSymbolVal(SSE->getRHS())); +} + +llvm_unreachable("Unsupported expression to reason about!"); + } + /// Dumps SMT formula LLVM_DUMP_METHOD void dump() const { Solver->dump(); } Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=345284&r1=345283&r2=345284&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Thu Oct 25 10:27:42 2018 @@ -285,6 +285,9 @@ public: /// Reset the solver and remove all constraints. virtual void reset() = 0; + /// Checks if the solver supports floating-points. + virtual bool isFPSupported() = 0; + virtual void print(raw_ostream &OS) const = 0; }; Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=345284&r1=345283&r2=345284&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Thu Oct 25 10:27:42 2018 @@ -860,6 +860,8 @@ public: return Z3Model(Context, Z3_solver_get_model(Context.Context, Solver)); } + bool isFPSupported() override { return true; } + /// Reset th
r345283 - [analyzer] Fixed bitvector from model always being unsigned
Author: mramalho Date: Thu Oct 25 10:27:36 2018 New Revision: 345283 URL: http://llvm.org/viewvc/llvm-project?rev=345283&view=rev Log: [analyzer] Fixed bitvector from model always being unsigned Summary: Getting an `APSInt` from the model always returned an unsigned integer because of the unused parameter. This was not breaking any test case because no code relies on the actual value of the integer returned here, but rather it is only used to check if a symbol has more than one solution in `getSymVal`. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin, Szelethus, donat.nagy, dkrupp Differential Revision: https://reviews.llvm.org/D53637 Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=345283&r1=345282&r2=345283&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Thu Oct 25 10:27:36 2018 @@ -733,9 +733,11 @@ public: llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, bool isUnsigned) override { -return llvm::APSInt(llvm::APInt( -BitWidth, Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST), -10)); +return llvm::APSInt( +llvm::APInt(BitWidth, +Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST), +10), +isUnsigned); } bool getBoolean(const SMTExprRef &Exp) override { ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r347777 - [analyzer] Cleanup constructors in the Z3 backend
Author: mramalho Date: Wed Nov 28 09:22:49 2018 New Revision: 34 URL: http://llvm.org/viewvc/llvm-project?rev=34&view=rev Log: [analyzer] Cleanup constructors in the Z3 backend Summary: Left only the constructors that are actually required, and marked the move constructors as deleted. They are not used anymore and we were never sure they've actually worked correctly. Reviewers: george.karpenkov, NoQ Reviewed By: george.karpenkov Subscribers: xazax.hun, baloghadamsoftware, szepet, a.sidorin, Szelethus, donat.nagy, dkrupp Differential Revision: https://reviews.llvm.org/D54974 Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=34&r1=347776&r2=34&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Nov 28 09:22:49 2018 @@ -77,32 +77,27 @@ class Z3Sort : public SMTSort { public: /// Default constructor, mainly used by make_shared - Z3Sort(Z3Context &C, Z3_sort ZS) : SMTSort(), Context(C), Sort(ZS) { + Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) { Z3_inc_ref(Context.Context, reinterpret_cast(Sort)); } /// Override implicit copy constructor for correct reference counting. - Z3Sort(const Z3Sort &Copy) - : SMTSort(), Context(Copy.Context), Sort(Copy.Sort) { + Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) { Z3_inc_ref(Context.Context, reinterpret_cast(Sort)); } - /// Provide move constructor - Z3Sort(Z3Sort &&Move) : SMTSort(), Context(Move.Context), Sort(nullptr) { -*this = std::move(Move); - } - - /// Provide move assignment constructor - Z3Sort &operator=(Z3Sort &&Move) { -if (this != &Move) { - if (Sort) -Z3_dec_ref(Context.Context, reinterpret_cast(Sort)); - Sort = Move.Sort; - Move.Sort = nullptr; -} + /// Override implicit copy assignment constructor for correct reference + /// counting. + Z3Sort &operator=(const Z3Sort &Other) { +Z3_inc_ref(Context.Context, reinterpret_cast(Other.Sort)); +Z3_dec_ref(Context.Context, reinterpret_cast(Sort)); +Sort = Other.Sort; return *this; } + Z3Sort(Z3Sort &&Other) = delete; + Z3Sort &operator=(Z3Sort &&Other) = delete; + ~Z3Sort() { if (Sort) Z3_dec_ref(Context.Context, reinterpret_cast(Sort)); @@ -134,13 +129,6 @@ public: static_cast(Other).Sort); } - Z3Sort &operator=(const Z3Sort &Move) { -Z3_inc_ref(Context.Context, reinterpret_cast(Move.Sort)); -Z3_dec_ref(Context.Context, reinterpret_cast(Sort)); -Sort = Move.Sort; -return *this; - } - void print(raw_ostream &OS) const override { OS << Z3_sort_to_string(Context.Context, Sort); } @@ -167,22 +155,18 @@ public: Z3_inc_ref(Context.Context, AST); } - /// Provide move constructor - Z3Expr(Z3Expr &&Move) : SMTExpr(), Context(Move.Context), AST(nullptr) { -*this = std::move(Move); - } - - /// Provide move assignment constructor - Z3Expr &operator=(Z3Expr &&Move) { -if (this != &Move) { - if (AST) -Z3_dec_ref(Context.Context, AST); - AST = Move.AST; - Move.AST = nullptr; -} + /// Override implicit copy assignment constructor for correct reference + /// counting. + Z3Expr &operator=(const Z3Expr &Other) { +Z3_inc_ref(Context.Context, Other.AST); +Z3_dec_ref(Context.Context, AST); +AST = Other.AST; return *this; } + Z3Expr(Z3Expr &&Other) = delete; + Z3Expr &operator=(Z3Expr &&Other) = delete; + ~Z3Expr() { if (AST) Z3_dec_ref(Context.Context, AST); @@ -202,14 +186,6 @@ public: static_cast(Other).AST); } - /// Override implicit move constructor for correct reference counting. - Z3Expr &operator=(const Z3Expr &Move) { -Z3_inc_ref(Context.Context, Move.AST); -Z3_dec_ref(Context.Context, AST); -AST = Move.AST; -return *this; - } - void print(raw_ostream &OS) const override { OS << Z3_ast_to_string(Context.Context, AST); } @@ -228,30 +204,13 @@ class Z3Model { public: Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) { -assert(C.Context != nullptr); -Z3_model_inc_ref(Context.Context, Model); - } - - /// Override implicit copy constructor for correct reference counting. - Z3Model(const Z3Model &Copy) : Context(Copy.Context), Model(Copy.Model) { Z3_model_inc_ref(Context.Context, Model); } - /// Provide move constructor - Z3Model(Z3Model &&Move) : Context(Move.Context), Model(nullptr) { -*this = std::move(Move); - } - - /// Provide move assignment constructor - Z3Model &operator=(Z3Model &&Move) { -if (this != &Move) { - if (Model
r356929 - Moved everything SMT-related to LLVM and updated the cmake scripts.
Author: mramalho Date: Mon Mar 25 10:47:45 2019 New Revision: 356929 URL: http://llvm.org/viewvc/llvm-project?rev=356929&view=rev Log: Moved everything SMT-related to LLVM and updated the cmake scripts. Differential Revision: https://reviews.llvm.org/D54978 Added: cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp Removed: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/CMakeLists.txt cfe/trunk/cmake/modules/FindZ3.cmake cfe/trunk/include/clang/Config/config.h.cmake cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt cfe/trunk/test/CMakeLists.txt cfe/trunk/test/lit.site.cfg.py.in Modified: cfe/trunk/CMakeLists.txt URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/CMakeLists.txt?rev=356929&r1=356928&r2=356929&view=diff == --- cfe/trunk/CMakeLists.txt (original) +++ cfe/trunk/CMakeLists.txt Mon Mar 25 10:47:45 2019 @@ -447,34 +447,9 @@ option(CLANG_BUILD_TOOLS option(CLANG_ENABLE_ARCMT "Build ARCMT." ON) option(CLANG_ENABLE_STATIC_ANALYZER "Build static analyzer." ON) -set(CLANG_ANALYZER_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.") - -find_package(Z3 4.7.1) - -if (CLANG_ANALYZER_Z3_INSTALL_DIR) - if (NOT Z3_FOUND) -message(FATAL_ERROR "Z3 4.7.1 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR: ${CLANG_ANALYZER_Z3_INSTALL_DIR}.") - endif() -endif() - -set(CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}") - -option(CLANG_ANALYZER_ENABLE_Z3_SOLVER - "Enable Support for the Z3 constraint solver in the Clang Static Analyzer." - ${CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT} -) - -if (CLANG_ANALYZER_ENABLE_Z3_SOLVER) - if (NOT Z3_FOUND) -message(FATAL_ERROR "CLANG_ANALYZER_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.") - endif() - - set(CLANG_ANALYZER_WITH_Z3 1) -endif() - option(CLANG_ENABLE_PROTO_FUZZER "Build Clang protobuf fuzzer." OFF) -if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR CLANG_ANALYZER_ENABLE_Z3_SOLVER)) +if(NOT CLANG_ENABLE_STATIC_ANALYZER AND CLANG_ENABLE_ARCMT) message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3") endif() Modified: cfe/trunk/cmake/modules/FindZ3.cmake URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/cmake/modules/FindZ3.cmake?rev=356929&r1=356928&r2=356929&view=diff == --- cfe/trunk/cmake/modules/FindZ3.cmake (original) +++ cfe/trunk/cmake/modules/FindZ3.cmake Mon Mar 25 10:47:45 2019 @@ -1,51 +0,0 @@ -# Looking for Z3 in CLANG_ANALYZER_Z3_INSTALL_DIR -find_path(Z3_INCLUDE_DIR NAMES z3.h - NO_DEFAULT_PATH - PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}/include - PATH_SUFFIXES libz3 z3 - ) - -find_library(Z3_LIBRARIES NAMES z3 libz3 - NO_DEFAULT_PATH - PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR} - PATH_SUFFIXES lib bin - ) - -find_program(Z3_EXECUTABLE z3 - NO_DEFAULT_PATH - PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR} - PATH_SUFFIXES bin - ) - -# If Z3 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR look in the default directories -find_path(Z3_INCLUDE_DIR NAMES z3.h - PATH_SUFFIXES libz3 z3 - ) - -find_library(Z3_LIBRARIES NAMES z3 libz3 - PATH_SUFFIXES lib bin - ) - -find_program(Z3_EXECUTABLE z3 - PATH_SUFFIXES bin - ) - -if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE) -execute_process (COMMAND ${Z3_EXECUTABLE} -version - OUTPUT_VARIABLE libz3_version_str - ERROR_QUIET - OUTPUT_STRIP_TRAILING_WHITESPACE) - -string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1" - Z3_VERSION_STRING "${libz3_version_str}") -unset(libz3_version_str) -endif() - -# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if -# all listed variables are TRUE -include(FindPackageHandleStandardArgs) -FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3 - REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR - VERSION_VAR Z3_VERSION_STRING) - -mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES) Modified: cfe/trunk/include/clang/Config/config.h.cmake URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/Config/config.h.cmake?rev=356929&r1=356928&r2=356929&view=diff == --- cfe/trunk/include/clang/Config/config.h.cmake (original) +++ cfe/trunk/include/clang/Config/config.h.cmake Mon Mar 25 10:47:45 2019 @@ -57,9 +57,6 @@ /* Define if we have libxml2 */ #cmakedefine CLANG_HAVE_LIBXML ${CLANG_HAVE_LIBXML} -/* Define if we have z3 and want to build it */ -#cmakedefine CLANG_ANALYZER_WI
r343581 - [analyzer] Improvements to the SMT API
Author: mramalho Date: Tue Oct 2 05:55:48 2018 New Revision: 343581 URL: http://llvm.org/viewvc/llvm-project?rev=343581&view=rev Log: [analyzer] Improvements to the SMT API Summary: Several improvements in preparation for the new backends. Refactoring: - Removed duplicated methods `fromBoolean`, `fromAPSInt`, `fromInt` and `fromAPFloat`. The methods `mkBoolean`, `mkBitvector` and `mkFloat` are now used instead. - The names of the functions that convert BVs to FPs were swapped (`mkSBVtoFP`, `mkUBVtoFP`, `mkFPtoSBV`, `mkFPtoUBV`). - Added a couple of comments in function calls. Crosscheck encoding: - Changed how constraints are encoded in the refutation manager so it doesn't start with (false OR ...). This change introduces one duplicated line (see file `BugReporterVisitors.cpp`, the `SMTConv::getRangeExpr is called twice, so I can remove this change if the duplication is a problem. Reviewers: george.karpenkov, NoQ Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin, Szelethus Differential Revision: https://reviews.llvm.org/D52365 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=343581&r1=343580&r2=343581&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Tue Oct 2 05:55:48 2018 @@ -134,9 +134,9 @@ public: // A value has been obtained, check if it is the only value SMTExprRef NotExp = SMTConv::fromBinOp( Solver, Exp, BO_NE, - Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue()) - : Solver->fromAPSInt(Value), - false); + Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue()) + : Solver->mkBitvector(Value, Value.getBitWidth()), + /*isSigned=*/false); Solver->addConstraint(NotExp); Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h?rev=343581&r1=343580&r2=343581&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h Tue Oct 2 05:55:48 2018 @@ -246,7 +246,7 @@ public: // Logical operators case BO_LAnd: case BO_LOr: - return fromBinOp(Solver, LHS, Op, RHS, false); + return fromBinOp(Solver, LHS, Op, RHS, /*isSigned=*/false); default:; } @@ -294,14 +294,14 @@ public: if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) { SMTSortRef Sort = Solver->getFloatSort(ToBitWidth); return FromTy->isSignedIntegerOrEnumerationType() - ? Solver->mkFPtoSBV(Exp, Sort) - : Solver->mkFPtoUBV(Exp, Sort); + ? Solver->mkSBVtoFP(Exp, Sort) + : Solver->mkUBVtoFP(Exp, Sort); } if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType()) return ToTy->isSignedIntegerOrEnumerationType() - ? Solver->mkSBVtoFP(Exp, ToBitWidth) - : Solver->mkUBVtoFP(Exp, ToBitWidth); + ? Solver->mkFPtoSBV(Exp, ToBitWidth) + : Solver->mkFPtoUBV(Exp, ToBitWidth); llvm_unreachable("Unsupported explicit type cast!"); } @@ -379,14 +379,14 @@ public: getSymExpr(Solver, Ctx, SIE->getLHS(),getRHS()); - SMTExprRef RHS = Solver->fromAPSInt(NewRInt); + SMTExprRef RHS = Solver->mkBitvector(NewRInt, NewRInt.getBitWidth()); return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); } if (const IntSymExpr *ISE = dyn_cast(BSE)) { llvm::APSInt NewLInt; std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS()); - SMTExprRef LHS = Solver->fromAPSInt(NewLInt); + SMTExprRef LHS = Solver->mkBitvector(NewLInt, NewLInt.getBitWidth()); SMTExprRef RHS = getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison); return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); @@ -466,7 +466,7 @@ public
r353370 - Generalised the SMT state constraints
Author: mramalho Date: Wed Feb 6 19:17:36 2019 New Revision: 353370 URL: http://llvm.org/viewvc/llvm-project?rev=353370&view=rev Log: Generalised the SMT state constraints This patch moves the ConstraintSMT definition to the SMTConstraintManager header to make it easier to move the Z3 backend around. We achieve this by not using shared_ptr anymore, as llvm::ImmutableSet doesn't seem to like it. The solver specific exprs and sorts are cached in the Z3Solver object now and we move pointers to those objects around. As a nice side-effect, SMTConstraintManager doesn't have to be a template anymore. Yay! Differential Revision: https://reviews.llvm.org/D54975 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=353370&r1=353369&r2=353370&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Wed Feb 6 19:17:36 2019 @@ -17,10 +17,14 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h" +typedef llvm::ImmutableSet< +std::pair> +ConstraintSMTTy; +REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTTy) + namespace clang { namespace ento { -template class SMTConstraintManager : public clang::ento::SimpleConstraintManager { SMTSolverRef &Solver; @@ -212,7 +216,7 @@ public: OS << nl << sep << "Constraints:"; for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) { OS << nl << ' ' << I->first << " : "; - I->second.print(OS); + I->second->print(OS); } OS << nl; } @@ -272,8 +276,7 @@ protected: const SMTExprRef &Exp) { // Check the model, avoid simplifying AST to save time if (checkModel(State, Sym, Exp).isConstrainedTrue()) - return State->add( - std::make_pair(Sym, static_cast(*Exp))); + return State->add(std::make_pair(Sym, Exp)); return nullptr; } @@ -289,9 +292,9 @@ protected: if (I != IE) { std::vector ASTs; - SMTExprRef Constraint = Solver->newExprRef(I++->second); + SMTExprRef Constraint = I++->second; while (I != IE) { -Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second)); +Constraint = Solver->mkAnd(Constraint, I++->second); } Solver->addConstraint(Constraint); @@ -301,8 +304,8 @@ protected: // Generate and check a Z3 model, using the given constraint. ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym, const SMTExprRef &Exp) const { -ProgramStateRef NewState = State->add( -std::make_pair(Sym, static_cast(*Exp))); +ProgramStateRef NewState = +State->add(std::make_pair(Sym, Exp)); llvm::FoldingSetNodeID ID; NewState->get().Profile(ID); Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h?rev=353370&r1=353369&r2=353370&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h Wed Feb 6 19:17:36 2019 @@ -33,10 +33,7 @@ public: return ID1 < ID2; } - virtual void Profile(llvm::FoldingSetNodeID &ID) const { -static int Tag = 0; -ID.AddPointer(&Tag); - } + virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0; friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) { return LHS.equal_to(RHS); @@ -53,7 +50,7 @@ protected: }; /// Shared pointer for SMTExprs, used by SMTSolver API. -using SMTExprRef = std::shared_ptr; +using SMTExprRef = const SMTExpr *; } // namespace ento } // namespace clang Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=353370&r1=353369&r2=353370&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original) +++ cfe/t
r353371 - Got rid of the `Z3ConstraintManager` class
Author: mramalho Date: Wed Feb 6 19:18:10 2019 New Revision: 353371 URL: http://llvm.org/viewvc/llvm-project?rev=353371&view=rev Log: Got rid of the `Z3ConstraintManager` class Now, instead of passing the reference to a shared_ptr, we pass the shared_ptr instead. I've also removed the check if Z3 is present in CreateZ3ConstraintManager as this function already calls CreateZ3Solver that performs the exactly same check. Differential Revision: https://reviews.llvm.org/D54976 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=353371&r1=353370&r2=353371&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Wed Feb 6 19:18:10 2019 @@ -26,12 +26,11 @@ namespace clang { namespace ento { class SMTConstraintManager : public clang::ento::SimpleConstraintManager { - SMTSolverRef &Solver; + mutable SMTSolverRef Solver = CreateZ3Solver(); public: - SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB, - SMTSolverRef &S) - : SimpleConstraintManager(SE, SB), Solver(S) {} + SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB) + : SimpleConstraintManager(SE, SB) {} virtual ~SMTConstraintManager() = default; //===--===// Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=353371&r1=353370&r2=353371&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Feb 6 19:18:10 2019 @@ -814,14 +814,6 @@ public: } }; // end class Z3Solver -class Z3ConstraintManager : public SMTConstraintManager { - SMTSolverRef Solver = CreateZ3Solver(); - -public: - Z3ConstraintManager(SubEngine *SE, SValBuilder &SB) - : SMTConstraintManager(SE, SB, Solver) {} -}; // end class Z3ConstraintManager - } // end anonymous namespace #endif @@ -839,12 +831,5 @@ SMTSolverRef clang::ento::CreateZ3Solver std::unique_ptr ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) { -#if CLANG_ANALYZER_WITH_Z3 - return llvm::make_unique(Eng, StMgr.getSValBuilder()); -#else - llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild " - "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON", - false); - return nullptr; -#endif + return llvm::make_unique(Eng, StMgr.getSValBuilder()); } ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r353372 - Moved the whole SMT API to a single file. NFC.
Author: mramalho Date: Wed Feb 6 19:18:21 2019 New Revision: 353372 URL: http://llvm.org/viewvc/llvm-project?rev=353372&view=rev Log: Moved the whole SMT API to a single file. NFC. There is no advantage in having them in separate files, I doubt some will ever use them separately. This also makes it easier to move the API to LLVM. Differential Revision: https://reviews.llvm.org/D54977 Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h Removed: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h?rev=353372&view=auto == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h (added) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h Wed Feb 6 19:18:21 2019 @@ -0,0 +1,404 @@ +//== SMTSolver.h *- C++ -*--==// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===--===// +// +// This file defines a SMT generic Solver API, which will be the base class +// for every SMT solver specific class. +// +//===--===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H + +#include "clang/Basic/TargetInfo.h" +#include "llvm/ADT/APSInt.h" + +namespace clang { +namespace ento { + +/// Generic base class for SMT sorts +class SMTSort { +public: + SMTSort() = default; + virtual ~SMTSort() = default; + + /// Returns true if the sort is a bitvector, calls isBitvectorSortImpl(). + virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); } + + /// Returns true if the sort is a floating-point, calls isFloatSortImpl(). + virtual bool isFloatSort() const { return isFloatSortImpl(); } + + /// Returns true if the sort is a boolean, calls isBooleanSortImpl(). + virtual bool isBooleanSort() const { return isBooleanSortImpl(); } + + /// Returns the bitvector size, fails if the sort is not a bitvector + /// Calls getBitvectorSortSizeImpl(). + virtual unsigned getBitvectorSortSize() const { +assert(isBitvectorSort() && "Not a bitvector sort!"); +unsigned Size = getBitvectorSortSizeImpl(); +assert(Size && "Size is zero!"); +return Size; + }; + + /// Returns the floating-point size, fails if the sort is not a floating-point + /// Calls getFloatSortSizeImpl(). + virtual unsigned getFloatSortSize() const { +assert(isFloatSort() && "Not a floating-point sort!"); +unsigned Size = getFloatSortSizeImpl(); +assert(Size && "Size is zero!"); +return Size; + }; + + virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0; + + bool operator<(const SMTSort &Other) const { +llvm::FoldingSetNodeID ID1, ID2; +Profile(ID1); +Other.Profile(ID2); +return ID1 < ID2; + } + + friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) { +return LHS.equal_to(RHS); + } + + virtual void print(raw_ostream &OS) const = 0; + + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } + +protected: + /// Query the SMT solver and returns true if two sorts are equal (same kind + /// and bit width). This does not check if the two sorts are the same objects. + virtual bool equal_to(SMTSort const &other) const = 0; + + /// Query the SMT solver and checks if a sort is bitvector. + virtual bool isBitvectorSortImpl() const = 0; + + /// Query the SMT solver and checks if a sort is floating-point. + virtual bool isFloatSortImpl() const = 0; + + /// Query the SMT solver and checks if a sort is boolean. + virtual bool isBooleanSortImpl() const = 0; + + /// Query the SMT solver and returns the sort bit width. + virtual unsigned getBitvectorSortSizeImpl() const = 0; + + /// Query the SMT solver and returns the sort bit width. + virtual unsigned getFloatSortSizeImpl() const = 0; +}; + +/// Shared pointer for SMTSorts, used by SMTSolver API. +using SMTSortRef = const SMTSort *; + +/// Generic base class for SMT exprs +class SMTExpr { +public: + SMTExpr() = default; + virtual ~SMTExpr() = default; + + bool operator<(const SMTExpr &Other) const { +llvm::FoldingSetNodeID ID1, ID2; +Profile(ID1); +Other.Profile(ID2); +return ID1 < ID2; + } + + virtual void Profile(llvm:
r353373 - Move the SMT API to LLVM
Author: mramalho Date: Wed Feb 6 19:19:45 2019 New Revision: 353373 URL: http://llvm.org/viewvc/llvm-project?rev=353373&view=rev Log: Move the SMT API to LLVM Moved everything SMT-related to LLVM and updated the cmake scripts. Differential Revision: https://reviews.llvm.org/D54978 Added: cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp Removed: cfe/trunk/cmake/modules/FindZ3.cmake cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/CMakeLists.txt cfe/trunk/include/clang/Config/config.h.cmake cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt cfe/trunk/test/CMakeLists.txt cfe/trunk/test/lit.site.cfg.py.in Modified: cfe/trunk/CMakeLists.txt URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/CMakeLists.txt?rev=353373&r1=353372&r2=353373&view=diff == --- cfe/trunk/CMakeLists.txt (original) +++ cfe/trunk/CMakeLists.txt Wed Feb 6 19:19:45 2019 @@ -411,34 +411,9 @@ option(CLANG_BUILD_TOOLS option(CLANG_ENABLE_ARCMT "Build ARCMT." ON) option(CLANG_ENABLE_STATIC_ANALYZER "Build static analyzer." ON) -set(CLANG_ANALYZER_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.") - -find_package(Z3 4.7.1) - -if (CLANG_ANALYZER_Z3_INSTALL_DIR) - if (NOT Z3_FOUND) -message(FATAL_ERROR "Z3 4.7.1 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR: ${CLANG_ANALYZER_Z3_INSTALL_DIR}.") - endif() -endif() - -set(CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}") - -option(CLANG_ANALYZER_ENABLE_Z3_SOLVER - "Enable Support for the Z3 constraint solver in the Clang Static Analyzer." - ${CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT} -) - -if (CLANG_ANALYZER_ENABLE_Z3_SOLVER) - if (NOT Z3_FOUND) -message(FATAL_ERROR "CLANG_ANALYZER_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.") - endif() - - set(CLANG_ANALYZER_WITH_Z3 1) -endif() - option(CLANG_ENABLE_PROTO_FUZZER "Build Clang protobuf fuzzer." OFF) -if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR CLANG_ANALYZER_ENABLE_Z3_SOLVER)) +if(NOT CLANG_ENABLE_STATIC_ANALYZER AND CLANG_ENABLE_ARCMT) message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3") endif() Removed: cfe/trunk/cmake/modules/FindZ3.cmake URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/cmake/modules/FindZ3.cmake?rev=353372&view=auto == --- cfe/trunk/cmake/modules/FindZ3.cmake (original) +++ cfe/trunk/cmake/modules/FindZ3.cmake (removed) @@ -1,51 +0,0 @@ -# Looking for Z3 in CLANG_ANALYZER_Z3_INSTALL_DIR -find_path(Z3_INCLUDE_DIR NAMES z3.h - NO_DEFAULT_PATH - PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}/include - PATH_SUFFIXES libz3 z3 - ) - -find_library(Z3_LIBRARIES NAMES z3 libz3 - NO_DEFAULT_PATH - PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR} - PATH_SUFFIXES lib bin - ) - -find_program(Z3_EXECUTABLE z3 - NO_DEFAULT_PATH - PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR} - PATH_SUFFIXES bin - ) - -# If Z3 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR look in the default directories -find_path(Z3_INCLUDE_DIR NAMES z3.h - PATH_SUFFIXES libz3 z3 - ) - -find_library(Z3_LIBRARIES NAMES z3 libz3 - PATH_SUFFIXES lib bin - ) - -find_program(Z3_EXECUTABLE z3 - PATH_SUFFIXES bin - ) - -if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE) -execute_process (COMMAND ${Z3_EXECUTABLE} -version - OUTPUT_VARIABLE libz3_version_str - ERROR_QUIET - OUTPUT_STRIP_TRAILING_WHITESPACE) - -string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1" - Z3_VERSION_STRING "${libz3_version_str}") -unset(libz3_version_str) -endif() - -# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if -# all listed variables are TRUE -include(FindPackageHandleStandardArgs) -FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3 - REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR - VERSION_VAR Z3_VERSION_STRING) - -mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES) Modified: cfe/trunk/include/clang/Config/config.h.cmake URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/Config/config.h.cmake?rev=353373&r1=353372&r2=353373&view=diff == --- cfe/trunk/include/clang/Config/config.h.cmake (original) +++ cfe/trunk/include/clang/Config/config.h.cmake Wed Feb 6 19:19:45 2019 @@ -54,9 +54,6 @@ /* Define if we have libxml2 */ #cmakedefine CLANG_HAVE_LIBXML ${CLANG_HAVE_LIBXML} -/* Define if we have z3 and want to build it */ -#cmakedefine CLANG_ANALYZER_WITH_Z3 ${CL
r353590 - This reverts commit 1440a848a635849b97f7a5cfa0ecc40d37451f5b.
Author: mramalho Date: Fri Feb 8 16:46:12 2019 New Revision: 353590 URL: http://llvm.org/viewvc/llvm-project?rev=353590&view=rev Log: This reverts commit 1440a848a635849b97f7a5cfa0ecc40d37451f5b. and commit a1853e834c65751f92521f7481b15cf0365e796b. They broke arm and aarch64 Added: cfe/trunk/cmake/modules/FindZ3.cmake cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Removed: cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp Modified: cfe/trunk/CMakeLists.txt cfe/trunk/include/clang/Config/config.h.cmake cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt cfe/trunk/test/CMakeLists.txt cfe/trunk/test/lit.site.cfg.py.in Modified: cfe/trunk/CMakeLists.txt URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/CMakeLists.txt?rev=353590&r1=353589&r2=353590&view=diff == --- cfe/trunk/CMakeLists.txt (original) +++ cfe/trunk/CMakeLists.txt Fri Feb 8 16:46:12 2019 @@ -411,9 +411,34 @@ option(CLANG_BUILD_TOOLS option(CLANG_ENABLE_ARCMT "Build ARCMT." ON) option(CLANG_ENABLE_STATIC_ANALYZER "Build static analyzer." ON) +set(CLANG_ANALYZER_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.") + +find_package(Z3 4.7.1) + +if (CLANG_ANALYZER_Z3_INSTALL_DIR) + if (NOT Z3_FOUND) +message(FATAL_ERROR "Z3 4.7.1 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR: ${CLANG_ANALYZER_Z3_INSTALL_DIR}.") + endif() +endif() + +set(CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}") + +option(CLANG_ANALYZER_ENABLE_Z3_SOLVER + "Enable Support for the Z3 constraint solver in the Clang Static Analyzer." + ${CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT} +) + +if (CLANG_ANALYZER_ENABLE_Z3_SOLVER) + if (NOT Z3_FOUND) +message(FATAL_ERROR "CLANG_ANALYZER_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.") + endif() + + set(CLANG_ANALYZER_WITH_Z3 1) +endif() + option(CLANG_ENABLE_PROTO_FUZZER "Build Clang protobuf fuzzer." OFF) -if(NOT CLANG_ENABLE_STATIC_ANALYZER AND CLANG_ENABLE_ARCMT) +if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR CLANG_ANALYZER_ENABLE_Z3_SOLVER)) message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3") endif() Added: cfe/trunk/cmake/modules/FindZ3.cmake URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/cmake/modules/FindZ3.cmake?rev=353590&view=auto == --- cfe/trunk/cmake/modules/FindZ3.cmake (added) +++ cfe/trunk/cmake/modules/FindZ3.cmake Fri Feb 8 16:46:12 2019 @@ -0,0 +1,51 @@ +# Looking for Z3 in CLANG_ANALYZER_Z3_INSTALL_DIR +find_path(Z3_INCLUDE_DIR NAMES z3.h + NO_DEFAULT_PATH + PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}/include + PATH_SUFFIXES libz3 z3 + ) + +find_library(Z3_LIBRARIES NAMES z3 libz3 + NO_DEFAULT_PATH + PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR} + PATH_SUFFIXES lib bin + ) + +find_program(Z3_EXECUTABLE z3 + NO_DEFAULT_PATH + PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR} + PATH_SUFFIXES bin + ) + +# If Z3 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR look in the default directories +find_path(Z3_INCLUDE_DIR NAMES z3.h + PATH_SUFFIXES libz3 z3 + ) + +find_library(Z3_LIBRARIES NAMES z3 libz3 + PATH_SUFFIXES lib bin + ) + +find_program(Z3_EXECUTABLE z3 + PATH_SUFFIXES bin + ) + +if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE) +execute_process (COMMAND ${Z3_EXECUTABLE} -version + OUTPUT_VARIABLE libz3_version_str + ERROR_QUIET + OUTPUT_STRIP_TRAILING_WHITESPACE) + +string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1" + Z3_VERSION_STRING "${libz3_version_str}") +unset(libz3_version_str) +endif() + +# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if +# all listed variables are TRUE +include(FindPackageHandleStandardArgs) +FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3 + REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR + VERSION_VAR Z3_VERSION_STRING) + +mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES) Modified: cfe/trunk/include/clang/Config/config.h.cmake URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/Config/config.h.cmake?rev=353590&r1=353589&r2=353590&view=diff == --- cfe/trunk/include/clang/Config/config.h.cmake (original) +++ cfe/trunk/include/clang/Config/config.h.cmake Fri Feb 8 16:46:12 2019 @@ -54,6 +54,9 @@ /* Define if we have libxml2 */ #cmakedefine CLANG_HAVE_LIBXML ${CLANG_HAVE_LIBXML} +/* Define if we have z3 and want to build it */ +#cmakedefine CLANG_ANALYZER_WITH_Z3 $
r335726 - [Analyzer] Moved RangeConstraintManager to header. NFC.
Author: mramalho Date: Wed Jun 27 05:42:48 2018 New Revision: 335726 URL: http://llvm.org/viewvc/llvm-project?rev=335726&view=rev Log: [Analyzer] Moved RangeConstraintManager to header. NFC. Summary: While at it, added a dump method to RangeSet. Reviewers: george.karpenkov, NoQ Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D48561 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h?rev=335726&r1=335725&r2=335726&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h Wed Jun 27 05:42:48 2018 @@ -117,6 +117,8 @@ public: void print(raw_ostream &os) const; + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } + bool operator==(const RangeSet &other) const { return ranges == other.ranges; } @@ -207,8 +209,90 @@ private: static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment); }; -} // end GR namespace +class RangeConstraintManager : public RangedConstraintManager { +public: + RangeConstraintManager(SubEngine *SE, SValBuilder &SVB) + : RangedConstraintManager(SE, SVB) {} + + //===--===// + // Implementation for interface from ConstraintManager. + //===--===// + + bool canReasonAbout(SVal X) const override; + + ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override; + + const llvm::APSInt *getSymVal(ProgramStateRef State, +SymbolRef Sym) const override; + + ProgramStateRef removeDeadBindings(ProgramStateRef State, + SymbolReaper &SymReaper) override; + + void print(ProgramStateRef State, raw_ostream &Out, const char *nl, + const char *sep) override; + + //===--===// + // Implementation for interface from RangedConstraintManager. + //===--===// + + ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym, + const llvm::APSInt &V, + const llvm::APSInt &Adjustment) override; + + ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym, + const llvm::APSInt &V, + const llvm::APSInt &Adjustment) override; + + ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym, + const llvm::APSInt &V, + const llvm::APSInt &Adjustment) override; + + ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym, + const llvm::APSInt &V, + const llvm::APSInt &Adjustment) override; + + ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym, + const llvm::APSInt &V, + const llvm::APSInt &Adjustment) override; + + ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym, + const llvm::APSInt &V, + const llvm::APSInt &Adjustment) override; + + ProgramStateRef assumeSymWithinInclusiveRange( + ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, + const llvm::APSInt &To, const llvm::APSInt &Adjustment) override; + + ProgramStateRef assumeSymOutsideInclusiveRange( + ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, + const llvm::APSInt &To, const llvm::APSInt &Adjustment) override; + + RangeSet::Factory &getRangeSetFactory() { return F; } + +private: + RangeSet::Factory F; + + RangeSet getRange(ProgramStateRef State, SymbolRef Sym); + + RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym, + const llvm::APSInt &Int, + const llvm::APSInt &Adjustment); + RangeSet getSymGTRange(ProgramStateRef St, SymbolRef Sym, + const llvm::APSInt &Int, + const llvm::APSInt &Adjustment); + RangeSet getSymLERange(ProgramStateRef St, SymbolRef Sym, + const llvm::APSInt &Int, + const llvm::APSInt &Adjustment); + RangeSet getSymLERange(llvm::function_ref RS, + const llvm::APSInt &Int, +
r335739 - [analyzer] Fix string not being formatted with extra arguments
Author: mramalho Date: Wed Jun 27 07:39:41 2018 New Revision: 335739 URL: http://llvm.org/viewvc/llvm-project?rev=335739&view=rev Log: [analyzer] Fix string not being formatted with extra arguments Signed-off-by: Mikhail Ramalho Modified: cfe/trunk/utils/analyzer/SATestBuild.py Modified: cfe/trunk/utils/analyzer/SATestBuild.py URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/utils/analyzer/SATestBuild.py?rev=335739&r1=335738&r2=335739&view=diff == --- cfe/trunk/utils/analyzer/SATestBuild.py (original) +++ cfe/trunk/utils/analyzer/SATestBuild.py Wed Jun 27 07:39:41 2018 @@ -280,7 +280,8 @@ def runScanBuild(Dir, SBOutputDir, PBuil } SBOptions += "-analyzer-config '%s' " % ( -",".join("%s=%s" for key, value in AnalyzerConfig.iteritems())) +",".join("%s=%s" % (key, value) for key, value in AnalyzerConfig.iteritems())) + # Always use ccc-analyze to ensure that we can locate the failures # directory. SBOptions += "--override-compiler " ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r335752 - Revert "[Analyzer] Moved RangeConstraintManager to header. NFC."
Author: mramalho Date: Wed Jun 27 09:45:58 2018 New Revision: 335752 URL: http://llvm.org/viewvc/llvm-project?rev=335752&view=rev Log: Revert "[Analyzer] Moved RangeConstraintManager to header. NFC." This broke a number of bots. This reverts commit 5e1a89912d37a21c3b49ccf30600d7f498dffa9c. Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h?rev=335752&r1=335751&r2=335752&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h Wed Jun 27 09:45:58 2018 @@ -117,8 +117,6 @@ public: void print(raw_ostream &os) const; - LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } - bool operator==(const RangeSet &other) const { return ranges == other.ranges; } @@ -209,90 +207,8 @@ private: static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment); }; -class RangeConstraintManager : public RangedConstraintManager { -public: - RangeConstraintManager(SubEngine *SE, SValBuilder &SVB) - : RangedConstraintManager(SE, SVB) {} - - //===--===// - // Implementation for interface from ConstraintManager. - //===--===// - - bool canReasonAbout(SVal X) const override; - - ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override; - - const llvm::APSInt *getSymVal(ProgramStateRef State, -SymbolRef Sym) const override; - - ProgramStateRef removeDeadBindings(ProgramStateRef State, - SymbolReaper &SymReaper) override; - - void print(ProgramStateRef State, raw_ostream &Out, const char *nl, - const char *sep) override; - - //===--===// - // Implementation for interface from RangedConstraintManager. - //===--===// - - ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &V, - const llvm::APSInt &Adjustment) override; - - ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &V, - const llvm::APSInt &Adjustment) override; - - ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &V, - const llvm::APSInt &Adjustment) override; - - ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &V, - const llvm::APSInt &Adjustment) override; - - ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &V, - const llvm::APSInt &Adjustment) override; - - ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &V, - const llvm::APSInt &Adjustment) override; - - ProgramStateRef assumeSymWithinInclusiveRange( - ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, - const llvm::APSInt &To, const llvm::APSInt &Adjustment) override; - - ProgramStateRef assumeSymOutsideInclusiveRange( - ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, - const llvm::APSInt &To, const llvm::APSInt &Adjustment) override; - - RangeSet::Factory &getRangeSetFactory() { return F; } - -private: - RangeSet::Factory F; - - RangeSet getRange(ProgramStateRef State, SymbolRef Sym); - - RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym, - const llvm::APSInt &Int, - const llvm::APSInt &Adjustment); - RangeSet getSymGTRange(ProgramStateRef St, SymbolRef Sym, - const llvm::APSInt &Int, - const llvm::APSInt &Adjustment); - RangeSet getSymLERange(ProgramStateRef St, SymbolRef Sym, - const llvm::APSInt &Int, - const llvm::APSInt &Adjustment); - RangeSet getSymLERange(llvm::function_ref RS, - const llvm::APSInt &Int, - const llvm::APSInt &Adjustment); - RangeSet getSymGERange(ProgramStateRef St, SymbolRef Sym, - const llvm::APSIn
r335926 - [analyzer] Fix wrong comparison generation of the ranges generated by the refutation manager
Author: mramalho Date: Thu Jun 28 14:26:52 2018 New Revision: 335926 URL: http://llvm.org/viewvc/llvm-project?rev=335926&view=rev Log: [analyzer] Fix wrong comparison generation of the ranges generated by the refutation manager The refutation manager is removing a true bug from the test in this patch. The problem is that the following constraint: ``` (conj_$1{struct o *}) - (reg_$3): [-9223372036854775808, 0] ``` is encoded as: ``` (and (bvuge (bvsub $1 $3) #x8000) (bvule (bvsub $1 $3) #x)) ``` The issue is that unsigned comparisons (bvuge and bvule) are being generated instead of signed comparisons (bvsge and bvsle). When generating the expressions: ``` (conj_$1{p *}) - (reg_$3) >= -9223372036854775808 ``` and ``` (conj_$1{p *}) - (reg_$3) <= 0 ``` both -9223372036854775808 and 0 are casted to pointer type and `LTy->isSignedIntegerOrEnumerationType()` in `Z3ConstraintManager::getZ3BinExpr` only checks if the type is signed, not if it's a pointer. Reviewers: NoQ, george.karpenkov, ddcc Subscribers: rnkovacs, NoQ, george.karpenkov, ddcc, xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D48324 Added: cfe/trunk/test/PR37855.c Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=335926&r1=335925&r2=335926&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Thu Jun 28 14:26:52 2018 @@ -1414,9 +1414,8 @@ Z3Expr Z3ConstraintManager::getZ3BinExpr // If the two operands are pointers and the operation is a subtraction, the // result is of type ptrdiff_t, which is signed -if (LTy->isAnyPointerType() && LTy == RTy && Op == BO_Sub) { - ASTContext &Ctx = getBasicVals().getContext(); - *RetTy = Ctx.getIntTypeForBitwidth(Ctx.getTypeSize(LTy), true); +if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) { + *RetTy = getBasicVals().getContext().getPointerDiffType(); } } Added: cfe/trunk/test/PR37855.c URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/PR37855.c?rev=335926&view=auto == --- cfe/trunk/test/PR37855.c (added) +++ cfe/trunk/test/PR37855.c Thu Jun 28 14:26:52 2018 @@ -0,0 +1,24 @@ +// RUN: %clang_cc1 -analyze -analyzer-eagerly-assume -analyzer-checker=core -w -DNO_CROSSCHECK -verify %s +// RUN: %clang_cc1 -analyze -analyzer-eagerly-assume -analyzer-checker=core -w -analyzer-config crosscheck-with-z3=true -verify %s +// REQUIRES: z3 + +typedef struct o p; +struct o { + struct { + } s; +}; + +void q(*r, p2) { r < p2; } + +void k(l, node) { + struct { +p *node; + } * n, *nodep, path[sizeof(void)]; + path->node = l; + for (n = path; node != l;) { +q(node, n->node); +nodep = n; + } + if (nodep) // expected-warning {{Branch condition evaluates to a garbage value}} +n[1].node->s; // expected-warning {{Dereference of undefined pointer value}} +} ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r335929 - [analyzer] Move test to the correct directory
Author: mramalho Date: Thu Jun 28 14:39:41 2018 New Revision: 335929 URL: http://llvm.org/viewvc/llvm-project?rev=335929&view=rev Log: [analyzer] Move test to the correct directory It was accidentaly pushed in r335926 Added: cfe/trunk/test/Analysis/PR37855.c - copied, changed from r335927, cfe/trunk/test/PR37855.c Removed: cfe/trunk/test/PR37855.c Copied: cfe/trunk/test/Analysis/PR37855.c (from r335927, cfe/trunk/test/PR37855.c) URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/PR37855.c?p2=cfe/trunk/test/Analysis/PR37855.c&p1=cfe/trunk/test/PR37855.c&r1=335927&r2=335929&rev=335929&view=diff == (empty) Removed: cfe/trunk/test/PR37855.c URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/PR37855.c?rev=335928&view=auto == --- cfe/trunk/test/PR37855.c (original) +++ cfe/trunk/test/PR37855.c (removed) @@ -1,24 +0,0 @@ -// RUN: %clang_cc1 -analyze -analyzer-eagerly-assume -analyzer-checker=core -w -DNO_CROSSCHECK -verify %s -// RUN: %clang_cc1 -analyze -analyzer-eagerly-assume -analyzer-checker=core -w -analyzer-config crosscheck-with-z3=true -verify %s -// REQUIRES: z3 - -typedef struct o p; -struct o { - struct { - } s; -}; - -void q(*r, p2) { r < p2; } - -void k(l, node) { - struct { -p *node; - } * n, *nodep, path[sizeof(void)]; - path->node = l; - for (n = path; node != l;) { -q(node, n->node); -nodep = n; - } - if (nodep) // expected-warning {{Branch condition evaluates to a garbage value}} -n[1].node->s; // expected-warning {{Dereference of undefined pointer value}} -} ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r335932 - [analyzer] fix test case expected warning
Author: mramalho Date: Thu Jun 28 15:08:44 2018 New Revision: 335932 URL: http://llvm.org/viewvc/llvm-project?rev=335932&view=rev Log: [analyzer] fix test case expected warning After r335814, the constraint manager is no longer generating a false bug report about the division by zero in the test case. This patch removes the expected false bug report. Modified: cfe/trunk/test/Analysis/z3-crosscheck.c Modified: cfe/trunk/test/Analysis/z3-crosscheck.c URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/z3-crosscheck.c?rev=335932&r1=335931&r2=335932&view=diff == --- cfe/trunk/test/Analysis/z3-crosscheck.c (original) +++ cfe/trunk/test/Analysis/z3-crosscheck.c Thu Jun 28 15:08:44 2018 @@ -21,22 +21,14 @@ void f(int *a, int *b) { if ((a - b) == 0) c = 0; if (a != b) -#ifdef NO_CROSSCHECK -g(3 / c); // expected-warning {{Division by zero}} -#else g(3 / c); // no-warning -#endif } _Bool nondet_bool(); void h(int d) { int x, y, k, z = 1; -#ifdef NO_CROSSCHECK while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}} -#else - while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}} -#endif z = 2 * z; } } ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r336002 - [analyzer] Replace the vector of ConstraintSets by a single ConstraintSet and a function to merge ConstraintSets
Author: mramalho Date: Fri Jun 29 11:11:43 2018 New Revision: 336002 URL: http://llvm.org/viewvc/llvm-project?rev=336002&view=rev Log: [analyzer] Replace the vector of ConstraintSets by a single ConstraintSet and a function to merge ConstraintSets Now, instead of adding the constraints when they are removed, this patch adds them when they first appear and, since we walk the bug report backward, it should be the last set of ranges generated by the CSA for a given symbol. These are the number before and after the patch: ``` Project| current | patch | tmux | 283.222 | 123.052 | redis | 614.858 | 400.347 | openssl| 308.292 | 307.149 | twin | 274.478 | 245.411 | git| 547.687 | 477.335 | postgresql | 2927.495 | 2002.526 | sqlite3| 3264.305 | 1028.416 | ``` Major speedups in tmux and sqlite (less than half of the time), redis and postgresql were about 25% faster while the rest are basically the same. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: rnkovacs, xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D48565 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h?rev=336002&r1=336001&r2=336002&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h Fri Jun 29 11:11:43 2018 @@ -336,11 +336,10 @@ public: class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor { private: /// Holds the constraints in a given path - // TODO: should we use a set? - llvm::SmallVector Constraints; + ConstraintRangeTy Constraints; public: - FalsePositiveRefutationBRVisitor() = default; + FalsePositiveRefutationBRVisitor(); void Profile(llvm::FoldingSetNodeID &ID) const override; @@ -348,6 +347,9 @@ public: const ExplodedNode *PrevN, BugReporterContext &BRC, BugReport &BR) override; + + void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode, + BugReport &BR) override; }; namespace bugreporter { Modified: cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp?rev=336002&r1=336001&r2=336002&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp Fri Jun 29 11:11:43 2018 @@ -2349,9 +2349,8 @@ TaintBugVisitor::VisitNode(const Explode return std::make_shared(L, "Taint originated here"); } -static bool -areConstraintsUnfeasible(BugReporterContext &BRC, - const llvm::SmallVector &Cs) { +static bool areConstraintsUnfeasible(BugReporterContext &BRC, + const ConstraintRangeTy &Cs) { // Create a refutation manager std::unique_ptr RefutationMgr = CreateZ3ConstraintManager( BRC.getStateManager(), BRC.getStateManager().getOwningEngine()); @@ -2360,28 +2359,45 @@ areConstraintsUnfeasible(BugReporterCont static_cast(RefutationMgr.get()); // Add constraints to the solver - for (const auto &C : Cs) -SMTRefutationMgr->addRangeConstraints(C); + SMTRefutationMgr->addRangeConstraints(Cs); // And check for satisfiability return SMTRefutationMgr->isModelFeasible().isConstrainedFalse(); } +static void addNewConstraints(ConstraintRangeTy &Cs, + const ConstraintRangeTy &NewCs, + ConstraintRangeTy::Factory &CF) { + // Add constraints if we don't have them yet + for (auto const &C : NewCs) { +const SymbolRef &Sym = C.first; +if (!Cs.contains(Sym)) { + Cs = CF.add(Cs, Sym, C.second); +} + } +} + +FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor() +: Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {} + +void FalsePositiveRefutationBRVisitor::finalizeVisitor( +BugReporterContext &BRC, const ExplodedNode *EndPathNode, BugReport &BR) { + // Collect new constraints + VisitNode(EndPathNode, nullptr, BRC, BR); + + // Create a new refutation manager and check feasibility + if (areConstraintsUnfeasible(BRC, Constraints)) +BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext()); +} + std::shared_ptr
r336671 - [analyzer] Add option to set maximum symbol complexity threshold
Author: mramalho Date: Tue Jul 10 06:46:05 2018 New Revision: 336671 URL: http://llvm.org/viewvc/llvm-project?rev=336671&view=rev Log: [analyzer] Add option to set maximum symbol complexity threshold Summary: This adds an option, max-symbol-complexity, so an user can set the maximum symbol complexity threshold. Note that the current behaviour is equivalent to max complexity = 0, when taint analysis is not enabled and tests show that in a number of tests, having complexity = 25 yields the same results as complexity = 1. This patch was extracted and modified from Dominic Chen's patch, D35450. Reviewers: george.karpenkov, NoQ, ddcc Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49093 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp cfe/trunk/lib/StaticAnalyzer/Core/SValBuilder.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h?rev=336671&r1=336670&r2=336671&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h Tue Jul 10 06:46:05 2018 @@ -294,6 +294,9 @@ private: /// \sa getGraphTrimInterval Optional GraphTrimInterval; + /// \sa getMaxSymbolComplexity + Optional MaxSymbolComplexity; + /// \sa getMaxTimesInlineLarge Optional MaxTimesInlineLarge; @@ -643,6 +646,11 @@ public: /// node reclamation, set the option to "0". unsigned getGraphTrimInterval(); + /// Returns the maximum complexity of symbolic constraint (50 by default). + /// + /// This is controlled by "-analyzer-config max-symbol-complexity" option. + unsigned getMaxSymbolComplexity(); + /// Returns the maximum times a large function could be inlined. /// /// This is controlled by the 'max-times-inline-large' config option. Modified: cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp?rev=336671&r1=336670&r2=336671&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp Tue Jul 10 06:46:05 2018 @@ -388,6 +388,12 @@ unsigned AnalyzerOptions::getGraphTrimIn return GraphTrimInterval.getValue(); } +unsigned AnalyzerOptions::getMaxSymbolComplexity() { + if (!MaxSymbolComplexity.hasValue()) +MaxSymbolComplexity = getOptionAsInteger("max-symbol-complexity", 1); + return MaxSymbolComplexity.getValue(); +} + unsigned AnalyzerOptions::getMaxTimesInlineLarge() { if (!MaxTimesInlineLarge.hasValue()) MaxTimesInlineLarge = getOptionAsInteger("max-times-inline-large", 32); Modified: cfe/trunk/lib/StaticAnalyzer/Core/SValBuilder.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SValBuilder.cpp?rev=336671&r1=336670&r2=336671&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/SValBuilder.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/SValBuilder.cpp Tue Jul 10 06:46:05 2018 @@ -22,6 +22,7 @@ #include "clang/AST/Type.h" #include "clang/Basic/LLVM.h" #include "clang/Analysis/AnalysisDeclContext.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" #include "clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h" #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h" @@ -29,6 +30,7 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" #include "clang/StaticAnalyzer/Core/PathSensitive/Store.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h" #include "llvm/ADT/APSInt.h" @@ -384,7 +386,9 @@ SVal SValBuilder::makeSymExprValNN(Progr const SymExpr *symRHS = RHS.getAsSymExpr(); // TODO: When the Max Complexity is reached, we should conjure a symbol // instead of generating an Unknown value and propagate the taint info to it. - const unsigned MaxComp = 1; // 10 28X + const unsigned MaxComp = StateMgr.getOwningEngine() + ->getAnalysisManager() + .options.getMaxSymbolComplexity(); if (symLHS && symRHS && (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp) ___ cfe-commits mailing list cfe-commits@li
r337167 - [analyzer] Fix constraint being dropped when analyzing a program without taint tracking enabled
Author: mramalho Date: Mon Jul 16 06:14:46 2018 New Revision: 337167 URL: http://llvm.org/viewvc/llvm-project?rev=337167&view=rev Log: [analyzer] Fix constraint being dropped when analyzing a program without taint tracking enabled Summary: This patch removes the constraint dropping when taint tracking is disabled. It also voids the crash reported in D28953 by treating a SymSymExpr with non pointer symbols as an opaque expression. Updated the regressions and verifying the big projects now; I'll update here when they're done. Based on the discussion on the mailing list and the patches by @ddcc. Reviewers: george.karpenkov, NoQ, ddcc, baloghadamsoftware Reviewed By: george.karpenkov Subscribers: delcypher, llvm-commits, rnkovacs, xazax.hun, szepet, a.sidorin, ddcc Differential Revision: https://reviews.llvm.org/D48650 Modified: cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp cfe/trunk/lib/StaticAnalyzer/Core/SValBuilder.cpp cfe/trunk/test/Analysis/PR37855.c cfe/trunk/test/Analysis/bitwise-ops.c cfe/trunk/test/Analysis/std-c-library-functions.c cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c Modified: cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp?rev=337167&r1=337166&r2=337167&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp Mon Jul 16 06:14:46 2018 @@ -390,7 +390,7 @@ unsigned AnalyzerOptions::getGraphTrimIn unsigned AnalyzerOptions::getMaxSymbolComplexity() { if (!MaxSymbolComplexity.hasValue()) -MaxSymbolComplexity = getOptionAsInteger("max-symbol-complexity", 1); +MaxSymbolComplexity = getOptionAsInteger("max-symbol-complexity", 25); return MaxSymbolComplexity.getValue(); } Modified: cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp?rev=337167&r1=337166&r2=337167&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp Mon Jul 16 06:14:46 2018 @@ -52,17 +52,18 @@ ProgramStateRef RangedConstraintManager: assert(BinaryOperator::isComparisonOp(Op)); // For now, we only support comparing pointers. -assert(Loc::isLocType(SSE->getLHS()->getType())); -assert(Loc::isLocType(SSE->getRHS()->getType())); -QualType DiffTy = SymMgr.getContext().getPointerDiffType(); -SymbolRef Subtraction = -SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy); +if (Loc::isLocType(SSE->getLHS()->getType()) && +Loc::isLocType(SSE->getRHS()->getType())) { + QualType DiffTy = SymMgr.getContext().getPointerDiffType(); + SymbolRef Subtraction = + SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy); -const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy); -Op = BinaryOperator::reverseComparisonOp(Op); -if (!Assumption) - Op = BinaryOperator::negateComparisonOp(Op); -return assumeSymRel(State, Subtraction, Op, Zero); + const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy); + Op = BinaryOperator::reverseComparisonOp(Op); + if (!Assumption) +Op = BinaryOperator::negateComparisonOp(Op); + return assumeSymRel(State, Subtraction, Op, Zero); +} } // If we get here, there's nothing else we can do but treat the symbol as Modified: cfe/trunk/lib/StaticAnalyzer/Core/SValBuilder.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SValBuilder.cpp?rev=337167&r1=337166&r2=337167&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/SValBuilder.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/SValBuilder.cpp Mon Jul 16 06:14:46 2018 @@ -379,11 +379,9 @@ SVal SValBuilder::makeSymExprValNN(Progr BinaryOperator::Opcode Op, NonLoc LHS, NonLoc RHS, QualType ResultTy) { - if (!State->isTainted(RHS) && !State->isTainted(LHS)) -return UnknownVal(); - const SymExpr *symLHS = LHS.getAsSymExpr(); const SymExpr *symRHS = RHS.getAsSymExpr(); + // TODO: When the Max Complexity is reached, we should conjure a symbol // instead of generating an Unknown value and propagate the taint info to it. const unsigned MaxComp = StateMgr.getOwningEngine() Modified: cfe/trunk/test/Analysis/PR37855.c URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/PR37855.c?rev=337167&
r337169 - [analyzer] Fix the Z3 backend always generating unsigned APSInt
Author: mramalho Date: Mon Jul 16 06:32:22 2018 New Revision: 337169 URL: http://llvm.org/viewvc/llvm-project?rev=337169&view=rev Log: [analyzer] Fix the Z3 backend always generating unsigned APSInt Summary: In `toAPSInt`, the Z3 backend was not checking the variable `Int`'s type and was always generating unsigned `APSInt`s. This was found by accident when I removed: ``` llvm::APSInt ConvertedLHS, ConvertedRHS; QualType LTy, RTy; std::tie(ConvertedLHS, LTy) = fixAPSInt(*LHS); std::tie(ConvertedRHS, RTy) = fixAPSInt(*RHS); -doIntTypePromotion( -ConvertedLHS, LTy, ConvertedRHS, RTy); return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS); ``` And the `BasicValueFactory` started to complain about different `signedness`. Reviewers: george.karpenkov, NoQ, ddcc Reviewed By: ddcc Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49305 Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337169&r1=337168&r2=337169&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Mon Jul 16 06:32:22 2018 @@ -681,12 +681,14 @@ public: Z3_get_numeral_uint64(Z3Context::ZC, AST, reinterpret_cast<__uint64 *>(&Value[0])); if (Sort.getBitvectorSortSize() <= 64) { -Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), true); +Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), + Int.isUnsigned()); } else if (Sort.getBitvectorSortSize() == 128) { Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64, AST)); Z3_get_numeral_uint64(Z3Context::ZC, AST, reinterpret_cast<__uint64 *>(&Value[1])); -Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), true); +Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), + Int.isUnsigned()); } else { assert(false && "Bitwidth not supported!"); return false; @@ -702,7 +704,7 @@ public: llvm::APInt(Int.getBitWidth(), Z3_get_bool_value(Z3Context::ZC, AST) == Z3_L_TRUE ? 1 : 0), - true); + Int.isUnsigned()); return true; } } ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
r337304 - [analyzer] Fix Z3 backend after D48205
Author: mramalho Date: Tue Jul 17 10:40:34 2018 New Revision: 337304 URL: http://llvm.org/viewvc/llvm-project?rev=337304&view=rev Log: [analyzer] Fix Z3 backend after D48205 Summary: An assertion was added in D48205 to catch places where a `nonloc::SymbolVal` was wrapping a `loc` object. This patch fixes that in the Z3 backend by making the `SValBuilder` object accessible from inherited instances of `SimpleConstraintManager` and calling `SVB.makeSymbolVal(foo)` instead of `nonloc::SymbolVal(foo)`. Reviewers: NoQ, george.karpenkov Reviewed By: NoQ Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49430 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h?rev=337304&r1=337303&r2=337304&view=diff == --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h Tue Jul 17 10:40:34 2018 @@ -75,6 +75,7 @@ protected: // Internal implementation. //===--===// + SValBuilder &getSValBuilder() const { return SVB; } BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); } SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); } Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337304&r1=337303&r2=337304&view=diff == --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Tue Jul 17 10:40:34 2018 @@ -1077,40 +1077,39 @@ bool Z3ConstraintManager::canReasonAbout return true; const SymExpr *Sym = SymVal->getSymbol(); - do { -QualType Ty = Sym->getType(); + QualType Ty = Sym->getType(); -// Complex types are not modeled -if (Ty->isComplexType() || Ty->isComplexIntegerType()) - return false; - -// Non-IEEE 754 floating-point types are not modeled -if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) && - (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() || - &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble( - return false; - -if (isa(Sym)) { - break; -} else if (const SymbolCast *SC = dyn_cast(Sym)) { - Sym = SC->getOperand(); -} else if (const BinarySymExpr *BSE = dyn_cast(Sym)) { - if (const SymIntExpr *SIE = dyn_cast(BSE)) { -Sym = SIE->getLHS(); - } else if (const IntSymExpr *ISE = dyn_cast(BSE)) { -Sym = ISE->getRHS(); - } else if (const SymSymExpr *SSM = dyn_cast(BSE)) { -return canReasonAbout(nonloc::SymbolVal(SSM->getLHS())) && - canReasonAbout(nonloc::SymbolVal(SSM->getRHS())); - } else { -llvm_unreachable("Unsupported binary expression to reason about!"); - } -} else { - llvm_unreachable("Unsupported expression to reason about!"); -} - } while (Sym); + // Complex types are not modeled + if (Ty->isComplexType() || Ty->isComplexIntegerType()) +return false; + + // Non-IEEE 754 floating-point types are not modeled + if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) && + (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() || +&TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble( +return false; - return true; + if (isa(Sym)) +return true; + + SValBuilder &SVB = getSValBuilder(); + + if (const SymbolCast *SC = dyn_cast(Sym)) +return canReasonAbout(SVB.makeSymbolVal(SC->getOperand())); + + if (const BinarySymExpr *BSE = dyn_cast(Sym)) { +if (const SymIntExpr *SIE = dyn_cast(BSE)) + return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS())); + +if (const IntSymExpr *ISE = dyn_cast(BSE)) + return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS())); + +if (const SymSymExpr *SSE = dyn_cast(BSE)) + return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) && + canReasonAbout(SVB.makeSymbolVal(SSE->getRHS())); + } + + llvm_unreachable("Unsupported expression to reason about!"); } ConditionTruthVal Z3ConstraintManager::checkNull(ProgramStateRef State, ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] 0f6fd1b - [libc] Add support for setjmp and longjmp in riscv
Author: Mikhail R. Gadelha Date: 2023-03-24T16:16:31-03:00 New Revision: 0f6fd1b704c014089f94271e08417a8179ee2b1c URL: https://github.com/llvm/llvm-project/commit/0f6fd1b704c014089f94271e08417a8179ee2b1c DIFF: https://github.com/llvm/llvm-project/commit/0f6fd1b704c014089f94271e08417a8179ee2b1c.diff LOG: [libc] Add support for setjmp and longjmp in riscv This patch implements setjmp and longjmp in riscv using inline asm. The following changes were required: * Omit frame pointer: otherwise gcc won't allow us to use s0 * Use __attribute__((naked)): otherwise both gcc and clang will generate function prologue and epilogue in both functions. This doesn't happen in x86_64, so we guard it to only riscv Furthermore, using __attribute__((naked)) causes two problems: we can't use `return 0` (both gcc and clang) and the function arguments in the function body (clang only), so we had to use a0 and a1 directly. Reviewed By: sivachandra Differential Revision: https://reviews.llvm.org/D145584 Added: libc/src/setjmp/riscv64/CMakeLists.txt libc/src/setjmp/riscv64/longjmp.cpp libc/src/setjmp/riscv64/setjmp.cpp libc/src/setjmp/x86_64/CMakeLists.txt libc/src/setjmp/x86_64/longjmp.cpp libc/src/setjmp/x86_64/setjmp.cpp Modified: clang/docs/tools/clang-formatted-files.txt libc/config/linux/riscv64/entrypoints.txt libc/config/linux/riscv64/headers.txt libc/include/llvm-libc-types/jmp_buf.h libc/src/setjmp/CMakeLists.txt Removed: libc/src/setjmp/longjmp.cpp libc/src/setjmp/setjmp.cpp diff --git a/clang/docs/tools/clang-formatted-files.txt b/clang/docs/tools/clang-formatted-files.txt index 31d1dd7f365a2..4b70e78cb1131 100644 --- a/clang/docs/tools/clang-formatted-files.txt +++ b/clang/docs/tools/clang-formatted-files.txt @@ -2594,6 +2594,7 @@ libc/include/llvm-libc-types/fexcept_t.h libc/include/llvm-libc-types/FILE.h libc/include/llvm-libc-types/float_t.h libc/include/llvm-libc-types/imaxdiv_t.h +libc/include/llvm-libc-types/jmp_buf.h libc/include/llvm-libc-types/ldiv_t.h libc/include/llvm-libc-types/lldiv_t.h libc/include/llvm-libc-types/mode_t.h diff --git a/libc/config/linux/riscv64/entrypoints.txt b/libc/config/linux/riscv64/entrypoints.txt index 95e3c1e5bf509..b502df6d1ecf6 100644 --- a/libc/config/linux/riscv64/entrypoints.txt +++ b/libc/config/linux/riscv64/entrypoints.txt @@ -371,6 +371,10 @@ if(LLVM_LIBC_FULL_BUILD) # sched.h entrypoints libc.src.sched.__sched_getcpucount +# setjmp.h entrypoints +libc.src.setjmp.longjmp +libc.src.setjmp.setjmp + # stdio.h entrypoints libc.src.stdio.clearerr libc.src.stdio.clearerr_unlocked diff --git a/libc/config/linux/riscv64/headers.txt b/libc/config/linux/riscv64/headers.txt index 6d7e53790ec12..223b9ea506892 100644 --- a/libc/config/linux/riscv64/headers.txt +++ b/libc/config/linux/riscv64/headers.txt @@ -10,6 +10,7 @@ set(TARGET_PUBLIC_HEADERS libc.include.sched libc.include.signal libc.include.spawn +libc.include.setjmp libc.include.stdio libc.include.stdlib libc.include.string diff --git a/libc/include/llvm-libc-types/jmp_buf.h b/libc/include/llvm-libc-types/jmp_buf.h index e948a7f42248a..6af4e8ebad92c 100644 --- a/libc/include/llvm-libc-types/jmp_buf.h +++ b/libc/include/llvm-libc-types/jmp_buf.h @@ -19,6 +19,19 @@ typedef struct { __UINT64_TYPE__ r15; __UINTPTR_TYPE__ rsp; __UINTPTR_TYPE__ rip; +#elif defined(__riscv) + /* Program counter. */ + long int __pc; + /* Callee-saved registers. */ + long int __regs[12]; + /* Stack pointer. */ + long int __sp; + /* Callee-saved floating point registers. */ +#if __riscv_float_abi_double + double __fpregs[12]; +#elif defined(__riscv_float_abi_single) +#error "__jmp_buf not available for your target architecture." +#endif #else #error "__jmp_buf not available for your target architecture." #endif diff --git a/libc/src/setjmp/CMakeLists.txt b/libc/src/setjmp/CMakeLists.txt index 5b79155cb4f05..d85c532e8636c 100644 --- a/libc/src/setjmp/CMakeLists.txt +++ b/libc/src/setjmp/CMakeLists.txt @@ -1,24 +1,17 @@ +if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${LIBC_TARGET_ARCHITECTURE}) + add_subdirectory(${CMAKE_CURRENT_SOURCE_DIR}/${LIBC_TARGET_ARCHITECTURE}) +endif() + add_entrypoint_object( setjmp - SRCS -setjmp.cpp - HDRS -setjmp_impl.h - COMPILE_OPTIONS --O3 # We do not want any local variables in setjmp --fno-omit-frame-pointer # The implementation assumes frame pointer on to the stack + ALIAS DEPENDS -libc.include.setjmp +.${LIBC_TARGET_ARCHITECTURE}.setjmp ) add_entrypoint_object( longjmp - SRCS -longjmp.cpp - HDRS -longjmp.h - COMPILE_OPTIONS --O3 # We do not want any local variables in longjmp + ALIAS DEPENDS -libc.include.setjmp +.${LIBC_TARGET_ARCHITECTURE}.longjmp ) diff --git a/libc/src/setjmp/riscv64/CMake
[clang] [alpha.webkit.UncountedLocalVarsChecker] Don't warning on inlined functions (PR #90733)
https://github.com/mikhailramalho created https://github.com/llvm/llvm-project/pull/90733 As per the guidelines, trivial inline functions shouldn't be changed to adopt smart pointers. >From a8c7e012a576fd01d6a6bdcb23a43e6669b005e8 Mon Sep 17 00:00:00 2001 From: "Mikhail R. Gadelha" Date: Wed, 1 May 2024 11:23:11 -0300 Subject: [PATCH] [alpha.webkit.UncountedLocalVarsChecker] Don't warning on inlined functions As per the guidelines, trivial inline functions shouldn't be changed to adopt smart pointers --- .../Checkers/WebKit/UncountedLocalVarsChecker.cpp| 5 + 1 file changed, 5 insertions(+) diff --git a/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp index 6036ad58cf253c..f64e29089f0b78 100644 --- a/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp +++ b/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp @@ -178,6 +178,11 @@ class UncountedLocalVarsChecker if (shouldSkipVarDecl(V)) return; +if (auto *FD = dyn_cast(V->getDeclContext())) { + if (FD->isInlined()) +return; +} + const auto *ArgType = V->getType().getTypePtr(); if (!ArgType) return; ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [alpha.webkit.UncountedLocalVarsChecker] Don't warning on inlined functions (PR #90733)
mikhailramalho wrote: @rniwa we noticed quite a drop in the warnings when using this patch, but we understand that there is another approach to handle inline functions: to add the `SUPPRESS_UNCOUNTED_LOCAL` to local variables inside these functions, like it was done here: https://github.com/WebKit/WebKit/pull/27870/files#diff-33ee084014f64a3d61fecb03211318d0d48dfa8f5b4ef6f4364fc2ab0364f9ebL137 Please let me know what you think of these approaches. If you prefer the macro one, I can close this PR and open another one. https://github.com/llvm/llvm-project/pull/90733 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [alpha.webkit.UncountedLocalVarsChecker] Don't warning on inlined functions (PR #90733)
https://github.com/mikhailramalho closed https://github.com/llvm/llvm-project/pull/90733 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [alpha.webkit.UncountedLocalVarsChecker] Don't warning on inlined functions (PR #90733)
mikhailramalho wrote: Thanks for the feedback folks. I'll close the PR. https://github.com/llvm/llvm-project/pull/90733 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [alpha.webkit.UncountedLocalVarsChecker] Ignore local vars of JSC::VM& type (PR #91068)
https://github.com/mikhailramalho created https://github.com/llvm/llvm-project/pull/91068 This patch also updates safeGetName to get names from operators without hitting an assertion >From 7f59654193385e78e1635c9bb2a627522f888b8d Mon Sep 17 00:00:00 2001 From: "Mikhail R. Gadelha" Date: Sat, 4 May 2024 13:08:32 -0300 Subject: [PATCH] [alpha.webkit.UncountedLocalVarsChecker] Ignore local vars of JSC::VM& type This patch also updates safeGetName to get names from operators without hitting an assertion --- .../StaticAnalyzer/Checkers/WebKit/ASTUtils.h | 11 + .../WebKit/UncountedLocalVarsChecker.cpp | 23 +++ 2 files changed, 29 insertions(+), 5 deletions(-) diff --git a/clang/lib/StaticAnalyzer/Checkers/WebKit/ASTUtils.h b/clang/lib/StaticAnalyzer/Checkers/WebKit/ASTUtils.h index e35ea4ef05dd17..d9049fea897be1 100644 --- a/clang/lib/StaticAnalyzer/Checkers/WebKit/ASTUtils.h +++ b/clang/lib/StaticAnalyzer/Checkers/WebKit/ASTUtils.h @@ -67,12 +67,13 @@ template std::string safeGetName(const T *ASTNode) { if (!ND) return ""; - // In case F is for example "operator|" the getName() method below would - // assert. - if (!ND->getDeclName().isIdentifier()) -return ""; + if (const auto *Identifier = ND->getIdentifier()) +return Identifier->getName().str(); - return ND->getName().str(); + std::string Name; + llvm::raw_string_ostream OS(Name); + ND->printName(OS); + return OS.str().empty() ? "" : OS.str(); } } // namespace clang diff --git a/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp index 6036ad58cf253c..2d33e63f66ad7c 100644 --- a/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp +++ b/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp @@ -225,11 +225,34 @@ class UncountedLocalVarsChecker } } + bool isVarIsAVMRefType(const VarDecl *V) const { +auto* type = V->getType()->getAs(); +if(!type) + return false; + +auto ClassDecl = type->getPointeeType()->getUnqualifiedDesugaredType()->getAsCXXRecordDecl(); +if (!ClassDecl) + return false; + +auto *NsDecl = ClassDecl->getParent(); +if (!NsDecl || !isa(NsDecl)) + return false; + +auto ClsNameStr = safeGetName(ClassDecl); +auto NamespaceName = safeGetName(NsDecl); + +// FIXME: These should be implemented via attributes. +return NamespaceName == "JSC" && ClsNameStr == "VM"; + } + bool shouldSkipVarDecl(const VarDecl *V) const { assert(V); if (!V->isLocalVarDecl()) return true; +if (isVarIsAVMRefType(V)) + return true; + return false; } ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [alpha.webkit.UncountedLocalVarsChecker] Ignore local vars of JSC::VM& type (PR #91068)
mikhailramalho wrote: Hey @rniwa, if you want I can send the `safeGetName` changes in a separate patch. I was planning to unify this with `isMethodOnWTFContainerType` so there is some duplicated code here. I'll update the PR next week with some tests. https://github.com/llvm/llvm-project/pull/91068 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [alpha.webkit.UncountedLocalVarsChecker] Ignore local vars of JSC::VM& type (PR #91068)
https://github.com/mikhailramalho updated https://github.com/llvm/llvm-project/pull/91068 >From dde31272c1599a699c49117c1612ae72d0491384 Mon Sep 17 00:00:00 2001 From: "Mikhail R. Gadelha" Date: Sat, 4 May 2024 13:08:32 -0300 Subject: [PATCH] [alpha.webkit.UncountedLocalVarsChecker] Ignore local vars of JSC::VM& type This patch also updates safeGetName to get names from operators without hitting an assertion --- .../StaticAnalyzer/Checkers/WebKit/ASTUtils.h | 11 + .../WebKit/UncountedLocalVarsChecker.cpp | 23 +++ 2 files changed, 29 insertions(+), 5 deletions(-) diff --git a/clang/lib/StaticAnalyzer/Checkers/WebKit/ASTUtils.h b/clang/lib/StaticAnalyzer/Checkers/WebKit/ASTUtils.h index e35ea4ef05dd17..d9049fea897be1 100644 --- a/clang/lib/StaticAnalyzer/Checkers/WebKit/ASTUtils.h +++ b/clang/lib/StaticAnalyzer/Checkers/WebKit/ASTUtils.h @@ -67,12 +67,13 @@ template std::string safeGetName(const T *ASTNode) { if (!ND) return ""; - // In case F is for example "operator|" the getName() method below would - // assert. - if (!ND->getDeclName().isIdentifier()) -return ""; + if (const auto *Identifier = ND->getIdentifier()) +return Identifier->getName().str(); - return ND->getName().str(); + std::string Name; + llvm::raw_string_ostream OS(Name); + ND->printName(OS); + return OS.str().empty() ? "" : OS.str(); } } // namespace clang diff --git a/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp index 6036ad58cf253c..2d33e63f66ad7c 100644 --- a/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp +++ b/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp @@ -225,11 +225,34 @@ class UncountedLocalVarsChecker } } + bool isVarIsAVMRefType(const VarDecl *V) const { +auto* type = V->getType()->getAs(); +if(!type) + return false; + +auto ClassDecl = type->getPointeeType()->getUnqualifiedDesugaredType()->getAsCXXRecordDecl(); +if (!ClassDecl) + return false; + +auto *NsDecl = ClassDecl->getParent(); +if (!NsDecl || !isa(NsDecl)) + return false; + +auto ClsNameStr = safeGetName(ClassDecl); +auto NamespaceName = safeGetName(NsDecl); + +// FIXME: These should be implemented via attributes. +return NamespaceName == "JSC" && ClsNameStr == "VM"; + } + bool shouldSkipVarDecl(const VarDecl *V) const { assert(V); if (!V->isLocalVarDecl()) return true; +if (isVarIsAVMRefType(V)) + return true; + return false; } ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [alpha.webkit.UncountedLocalVarsChecker] Ignore local vars of JSC::VM& type (PR #91068)
https://github.com/mikhailramalho updated https://github.com/llvm/llvm-project/pull/91068 >From a770060da101720ffddc033fd37db790eaa17710 Mon Sep 17 00:00:00 2001 From: "Mikhail R. Gadelha" Date: Sat, 4 May 2024 13:08:32 -0300 Subject: [PATCH] [alpha.webkit.UncountedLocalVarsChecker] Ignore local vars of JSC::VM& type This patch also updates safeGetName to get names from operators without hitting an assertion --- .../StaticAnalyzer/Checkers/WebKit/ASTUtils.h | 11 .../WebKit/UncountedLocalVarsChecker.cpp | 25 +++ 2 files changed, 31 insertions(+), 5 deletions(-) diff --git a/clang/lib/StaticAnalyzer/Checkers/WebKit/ASTUtils.h b/clang/lib/StaticAnalyzer/Checkers/WebKit/ASTUtils.h index e35ea4ef05dd17..d9049fea897be1 100644 --- a/clang/lib/StaticAnalyzer/Checkers/WebKit/ASTUtils.h +++ b/clang/lib/StaticAnalyzer/Checkers/WebKit/ASTUtils.h @@ -67,12 +67,13 @@ template std::string safeGetName(const T *ASTNode) { if (!ND) return ""; - // In case F is for example "operator|" the getName() method below would - // assert. - if (!ND->getDeclName().isIdentifier()) -return ""; + if (const auto *Identifier = ND->getIdentifier()) +return Identifier->getName().str(); - return ND->getName().str(); + std::string Name; + llvm::raw_string_ostream OS(Name); + ND->printName(OS); + return OS.str().empty() ? "" : OS.str(); } } // namespace clang diff --git a/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp index 6036ad58cf253c..2f5e8e139709f6 100644 --- a/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp +++ b/clang/lib/StaticAnalyzer/Checkers/WebKit/UncountedLocalVarsChecker.cpp @@ -225,11 +225,36 @@ class UncountedLocalVarsChecker } } + bool isVarIsAVMRefType(const VarDecl *V) const { +auto *type = V->getType()->getAs(); +if (!type) + return false; + +auto ClassDecl = type->getPointeeType() + ->getUnqualifiedDesugaredType() + ->getAsCXXRecordDecl(); +if (!ClassDecl) + return false; + +auto *NsDecl = ClassDecl->getParent(); +if (!NsDecl || !isa(NsDecl)) + return false; + +auto ClsNameStr = safeGetName(ClassDecl); +auto NamespaceName = safeGetName(NsDecl); + +// FIXME: These should be implemented via attributes. +return NamespaceName == "JSC" && ClsNameStr == "VM"; + } + bool shouldSkipVarDecl(const VarDecl *V) const { assert(V); if (!V->isLocalVarDecl()) return true; +if (isVarIsAVMRefType(V)) + return true; + return false; } ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [alpha.webkit.UncountedLocalVarsChecker] Ignore local vars of JSC::VM& type (PR #91068)
https://github.com/mikhailramalho closed https://github.com/llvm/llvm-project/pull/91068 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [alpha.webkit.UncountedLocalVarsChecker] Ignore local vars of JSC::VM& type (PR #91068)
mikhailramalho wrote: I opened this PR before we spoke offline, I'm closing it now https://github.com/llvm/llvm-project/pull/91068 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits