r340532 - [analyzer] Delete SMTContext. NFC.

2018-08-23 Thread Mikhail R. Gadelha via cfe-commits
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

2018-05-23 Thread Mikhail R. Gadelha via cfe-commits
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.

2018-05-24 Thread Mikhail R. Gadelha via cfe-commits
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.

2018-05-28 Thread Mikhail R. Gadelha via cfe-commits
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.

2018-08-23 Thread Mikhail R. Gadelha via cfe-commits
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.

2018-08-23 Thread Mikhail R. Gadelha via cfe-commits
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

2018-08-23 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-19 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-25 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-25 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-25 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-25 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-25 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-25 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-25 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-25 Thread Mikhail R. Gadelha via cfe-commits
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, QualType isPromotableIntegerType()) {
-  QualType NewTy = Ctx.getPromotedInteg

r337922 - [analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and replace by proper calls to SMTSolver

2018-07-25 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-25 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-25 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-25 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-26 Thread Mikhail R. Gadelha via cfe-commits
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

2018-05-30 Thread Mikhail R. Gadelha via cfe-commits
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

2018-06-04 Thread Mikhail R. Gadelha via cfe-commits
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

2018-06-04 Thread Mikhail R. Gadelha via cfe-commits
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

2018-06-04 Thread Mikhail R. Gadelha via cfe-commits
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

2018-06-16 Thread Mikhail R. Gadelha via cfe-commits
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

2018-06-20 Thread Mikhail R. Gadelha via cfe-commits
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

2018-10-25 Thread Mikhail R. Gadelha via cfe-commits
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

2018-10-25 Thread Mikhail R. Gadelha via cfe-commits
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

2018-11-28 Thread Mikhail R. Gadelha via cfe-commits
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.

2019-03-25 Thread Mikhail R. Gadelha via cfe-commits
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

2018-10-02 Thread Mikhail R. Gadelha via cfe-commits
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

2019-02-06 Thread Mikhail R. Gadelha via cfe-commits
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

2019-02-06 Thread Mikhail R. Gadelha via cfe-commits
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.

2019-02-06 Thread Mikhail R. Gadelha via cfe-commits
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

2019-02-06 Thread Mikhail R. Gadelha via cfe-commits
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.

2019-02-08 Thread Mikhail R. Gadelha via cfe-commits
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.

2018-06-27 Thread Mikhail R. Gadelha via cfe-commits
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

2018-06-27 Thread Mikhail R. Gadelha via cfe-commits
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."

2018-06-27 Thread Mikhail R. Gadelha via cfe-commits
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

2018-06-28 Thread Mikhail R. Gadelha via cfe-commits
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

2018-06-28 Thread Mikhail R. Gadelha via cfe-commits
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

2018-06-28 Thread Mikhail R. Gadelha via cfe-commits
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

2018-06-29 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-10 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-16 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-16 Thread Mikhail R. Gadelha via cfe-commits
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

2018-07-17 Thread Mikhail R. Gadelha via cfe-commits
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

2023-03-24 Thread Mikhail R. Gadelha via cfe-commits

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)

2024-05-01 Thread Mikhail R. Gadelha via cfe-commits

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)

2024-05-01 Thread Mikhail R. Gadelha via cfe-commits

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)

2024-05-02 Thread Mikhail R. Gadelha via cfe-commits

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)

2024-05-02 Thread Mikhail R. Gadelha via cfe-commits

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)

2024-05-04 Thread Mikhail R. Gadelha via cfe-commits

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)

2024-05-04 Thread Mikhail R. Gadelha via cfe-commits

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)

2024-05-04 Thread Mikhail R. Gadelha via cfe-commits

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)

2024-05-04 Thread Mikhail R. Gadelha via cfe-commits

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)

2024-05-09 Thread Mikhail R. Gadelha via cfe-commits

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)

2024-05-09 Thread Mikhail R. Gadelha via cfe-commits

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