[analyzer] Generalised the SMT state constraints

[mikhail.ramalho]

Summary

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!

[george.karpenkov]

TBH this seems overly complicated. Z3 already hash-conses all objects; I don't think there is benefit of doing it again on the LLVM side.

What is the benefit from this patch, apart from being able to use ImmutableSet?

[mikhail.ramalho]

In D54975#1310619, @george.karpenkov wrote:

TBH this seems overly complicated. Z3 already hash-conses all objects; I don't think there is benefit of doing it again on the LLVM side.

What is the benefit from this patch, apart from being able to use ImmutableSet?

The cache is only used to hold the exprs and sorts in the Solver class.

The idea here is to make it similar to the SymbolManager class in the CSA and store all the exprs and sorts in the solver specific class, so we don't have to manage their lifetime.

[NoQ]

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

21–24

Why is this a path-sensitive data?

Wouldn't we always automatically map the same symbol to the same SMT expression? If we would, then this should be a global. If we wouldn't, then the path-sensitive trait is already useless, because the SMT expression would probably change between nodes on the same path as well.

[mikhail.ramalho]

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

21–24

By "this should be global" do you mean moving it to RangedConstraintManager.h along with ConstraintRangeTy?

The only reason I didn't do it was because I was trying to keep everything SMT-related together.

[NoQ]

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

21–24

Wait, i guess i misunderstood. Yes, this should be state-specific, never mind.

314–317

Mmm, would this sometimes cause non-deterministic collisions? I think that NewState->get<ConstraintSMT>().getRootWithoutRetain() should be used as hash directly, as it does actually uniquely identify the set. ID also uniquely identifies the set (being the same thing), but ID.ComputeHash() doesn't (being a shorter integer).

[mikhail.ramalho]

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

314–317

Oh, I didn't know that! I'll update it.

[michaelplatings]

cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

22 ↗

(On Diff #185695)

This does not compile with Visual Studio 2015:

1>  SMTConstraintManager.cpp
1>StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h(23): error C2872: 'ConstraintSMTTy': ambiguous symbol
1>  StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h(22): note: could be 'llvm::ImmutableSet<std::pair<clang::ento::SymbolRef,const llvm::SMTExpr *>,llvm::ImutContainerInfo<ValT>> ConstraintSMTTy'
1>    with
1>    [
1>        ValT=std::pair<clang::ento::SymbolRef,const llvm::SMTExpr *>
1>    ]
1>  StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h(23): note: or       '`anonymous-namespace'::ConstraintSMTTy'

It could be fixed by changing ConstraintSMTTy to e.g. ConstraintSMTType

[mikhail.ramalho]

@michaelplatings, thanks for the report.

That's weird, did you try to run the tests? You can do it with ninja check-clang-analyzer-z3

[michaelplatings]

In D54975#1391441, @mikhail.ramalho wrote:

@michaelplatings, thanks for the report.

That's weird, did you try to run the tests? You can do it with ninja check-clang-analyzer-z3

If you look at the lines referenced by the error you may find it less weird - the patch adds a typedef that has the same name as a using statement added by the REGISTER_TRAIT_WITH_PROGRAMSTATE macro.

To be clear, this patch breaks compilation with Visual Studio 2015. Running tests requires that the code can be built, so no I didn't run the tests.

[mikhail.ramalho]

To be clear, this patch breaks compilation with Visual Studio 2015. Running tests requires that the code can be built, so no I didn't run the tests.

Maybe I didn't express myself very clearly: if you change it to ConstraintSMTType, do the tests pass?

If so, I don't see why not pushing the fix. Unfortunately, I don't have Windows to test it.

[dyung]

In D54975#1393783, @mikhail.ramalho wrote:

To be clear, this patch breaks compilation with Visual Studio 2015. Running tests requires that the code can be built, so no I didn't run the tests.

Maybe I didn't express myself very clearly: if you change it to ConstraintSMTType, do the tests pass?

If so, I don't see why not pushing the fix. Unfortunately, I don't have Windows to test it.

I can give it a try. But just to be clear, the fix is to change ConstraintSMTTy on line 22 to ConstraintSMTType? Would line 23 require a similar change, or is it fine as it currently is?

[dyung]

In D54975#1394002, @dyung wrote:

In D54975#1393783, @mikhail.ramalho wrote:

To be clear, this patch breaks compilation with Visual Studio 2015. Running tests requires that the code can be built, so no I didn't run the tests.

Maybe I didn't express myself very clearly: if you change it to ConstraintSMTType, do the tests pass?

If so, I don't see why not pushing the fix. Unfortunately, I don't have Windows to test it.

I can give it a try. But just to be clear, the fix is to change ConstraintSMTTy on line 22 to ConstraintSMTType? Would line 23 require a similar change, or is it fine as it currently is?

I can answer my own question, both seem to need updating. I am building/testing now.

[dyung]

In D54975#1394044, @dyung wrote:

In D54975#1394002, @dyung wrote:

In D54975#1393783, @mikhail.ramalho wrote:

To be clear, this patch breaks compilation with Visual Studio 2015. Running tests requires that the code can be built, so no I didn't run the tests.

Maybe I didn't express myself very clearly: if you change it to ConstraintSMTType, do the tests pass?

If so, I don't see why not pushing the fix. Unfortunately, I don't have Windows to test it.

I can give it a try. But just to be clear, the fix is to change ConstraintSMTTy on line 22 to ConstraintSMTType? Would line 23 require a similar change, or is it fine as it currently is?

I can answer my own question, both seem to need updating. I am building/testing now.

Build and test passed for me with Visual Studio 2015 and on Linux. Should I submit the fix?

[dyung]

In D54975#1394068, @dyung wrote:

Build and test passed for me with Visual Studio 2015 and on Linux. Should I submit the fix?

I committed the change in r353791. Hopefully this fixes the problem.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
 
 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
 
+typedef llvm::ImmutableSet<
+    std::pair<clang::ento::SymbolRef, const clang::ento::SMTExpr *>>
+    ConstraintSMTTy;
+REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTTy)
+
 namespace clang {
 namespace ento {
 
-template <typename ConstraintSMT, typename SMTExprTy>
 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
   SMTSolverRef &Solver;
 
 public:
   SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB,
                        SMTSolverRef &S)
       : SimpleConstraintManager(SE, SB), Solver(S) {}
   virtual ~SMTConstraintManager() = default;
public:
   void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
              const char *sep) override {
 
     auto CZ = St->get<ConstraintSMT>();
 
     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;
   }
 
   bool canReasonAbout(SVal X) const override {
     const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
 
     Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
public:
   LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
 
 protected:
   // Check whether a new model is satisfiable, and update the program state.
   virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
                                      const SMTExprRef &Exp) {
     // Check the model, avoid simplifying AST to save time
     if (checkModel(State, Sym, Exp).isConstrainedTrue())
-      return State->add<ConstraintSMT>(
-          std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp)));
+      return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
 
     return nullptr;
   }
 
   /// Given a program state, construct the logical conjunction and add it to
   /// the solver
   virtual void addStateConstraints(ProgramStateRef State) const {
     // TODO: Don't add all the constraints, only the relevant ones
     auto CZ = State->get<ConstraintSMT>();
     auto I = CZ.begin(), IE = CZ.end();
 
     // Construct the logical AND of all the constraints
     if (I != IE) {
       std::vector<SMTExprRef> 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);
     }
   }
 
   // Generate and check a Z3 model, using the given constraint.
   ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,
                                const SMTExprRef &Exp) const {
-    ProgramStateRef NewState = State->add<ConstraintSMT>(
-        std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp)));
+    ProgramStateRef NewState =
+        State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
 
     llvm::FoldingSetNodeID ID;
     NewState->get<ConstraintSMT>().Profile(ID);
 
     unsigned hash = ID.ComputeHash();
     auto I = Cached.find(hash);
     if (I != Cached.end())
       return I->second;
 
     Solver->reset();
     addStateConstraints(NewState);
 
     Optional<bool> res = Solver->check();
     if (!res.hasValue())
       Cached[hash] = ConditionTruthVal();
     else

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h

public:
 
   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);
-  }
+  virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
 
   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:
   /// 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<SMTExpr>;
+using SMTExprRef = const SMTExpr *;
 
 } // namespace ento
 } // namespace clang
 
 #endif

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h

public:
   virtual SMTSortRef getFloat64Sort() = 0;
 
   // Returns a floating-point sort of width 128
   virtual SMTSortRef getFloat128Sort() = 0;
 
   // Returns an appropriate sort for the given AST.
   virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
 
-  // Returns a new SMTExprRef from an SMTExpr
-  virtual SMTExprRef newExprRef(const SMTExpr &E) const = 0;
-
   /// Given a constraint, adds it to the solver
   virtual void addConstraint(const SMTExprRef &Exp) const = 0;
 
   /// Creates a bitvector addition operation
   virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
   /// Creates a bitvector subtraction operation
   virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h

public:
   /// 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 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 = std::shared_ptr<SMTSort>;
+using SMTSortRef = const SMTSort *;
 
 } // namespace ento
 } // namespace clang
 
 #endif

clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

public:
   Z3Sort(Z3Sort &&Other) = delete;
   Z3Sort &operator=(Z3Sort &&Other) = delete;
 
   ~Z3Sort() {
     if (Sort)
       Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
   }
 
+  void Profile(llvm::FoldingSetNodeID &ID) const {
+    ID.AddInteger(
+        Z3_get_ast_id(Context.Context, reinterpret_cast<Z3_ast>(Sort)));
+  }
+
   bool isBitvectorSortImpl() const override {
     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);
   }
 
   bool isFloatSortImpl() const override {
     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT);
   }
 
public:
   Z3Expr &operator=(Z3Expr &&Other) = delete;
 
   ~Z3Expr() {
     if (AST)
       Z3_dec_ref(Context.Context, AST);
   }
 
   void Profile(llvm::FoldingSetNodeID &ID) const override {
-    ID.AddInteger(Z3_get_ast_hash(Context.Context, AST));
+    ID.AddInteger(Z3_get_ast_id(Context.Context, AST));
   }
 
   /// Comparison of AST equality, not model equivalence.
   bool equal_to(SMTExpr const &Other) const override {
     assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
                          Z3_get_sort(Context.Context,
                                      static_cast<const Z3Expr &>(Other).AST)) &&
            "AST's must have the same sort");
return (llvm::APFloat::semanticsPrecision(LHS) ==
          (llvm::APFloat::semanticsMinExponent(LHS) ==
           llvm::APFloat::semanticsMinExponent(RHS)) &&
          (llvm::APFloat::semanticsMaxExponent(LHS) ==
           llvm::APFloat::semanticsMaxExponent(RHS)) &&
          (llvm::APFloat::semanticsSizeInBits(LHS) ==
           llvm::APFloat::semanticsSizeInBits(RHS));
 }
 
-} // end anonymous namespace
-
-typedef llvm::ImmutableSet<std::pair<SymbolRef, Z3Expr>> ConstraintZ3Ty;
-REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, ConstraintZ3Ty)
-
-namespace {
-
 class Z3Solver : public SMTSolver {
   friend class Z3ConstraintManager;
 
   Z3Context Context;
 
   Z3_solver Solver;
 
+  // Cache Sorts
+  std::set<Z3Sort> CachedSorts;
+
+  // Cache Exprs
+  std::set<Z3Expr> CachedExprs;
+
 public:
   Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {
     Z3_solver_inc_ref(Context.Context, Solver);
   }
 
   Z3Solver(const Z3Solver &Other) = delete;
   Z3Solver(Z3Solver &&Other) = delete;
   Z3Solver &operator=(Z3Solver &Other) = delete;
   Z3Solver &operator=(Z3Solver &&Other) = delete;
 
   ~Z3Solver() {
     if (Solver)
       Z3_solver_dec_ref(Context.Context, Solver);
   }
 
   void addConstraint(const SMTExprRef &Exp) const override {
     Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
   }
 
+  // Given an SMTSort, adds/retrives it from the cache and returns
+  // an SMTSortRef to the SMTSort in the cache
+  SMTSortRef newSortRef(const SMTSort &Sort) {
+    auto It = CachedSorts.insert(toZ3Sort(Sort));
+    return &(*It.first);
+  }
+
+  // Given an SMTExpr, adds/retrives it from the cache and returns
+  // an SMTExprRef to the SMTExpr in the cache
+  SMTExprRef newExprRef(const SMTExpr &Exp) {
+    auto It = CachedExprs.insert(toZ3Expr(Exp));
+    return &(*It.first);
+  }
+
   SMTSortRef getBoolSort() override {
-    return std::make_shared<Z3Sort>(Context, Z3_mk_bool_sort(Context.Context));
+    return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(Context.Context)));
   }
 
   SMTSortRef getBitvectorSort(unsigned BitWidth) override {
-    return std::make_shared<Z3Sort>(Context,
-                                    Z3_mk_bv_sort(Context.Context, BitWidth));
+    return newSortRef(
+        Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth)));
   }
 
   SMTSortRef getSort(const SMTExprRef &Exp) override {
-    return std::make_shared<Z3Sort>(
-        Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST));
+    return newSortRef(
+        Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));
   }
 
   SMTSortRef getFloat16Sort() override {
-    return std::make_shared<Z3Sort>(Context,
-                                    Z3_mk_fpa_sort_16(Context.Context));
+    return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(Context.Context)));
   }
 
   SMTSortRef getFloat32Sort() override {
-    return std::make_shared<Z3Sort>(Context,
-                                    Z3_mk_fpa_sort_32(Context.Context));
+    return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(Context.Context)));
   }
 
   SMTSortRef getFloat64Sort() override {
-    return std::make_shared<Z3Sort>(Context,
-                                    Z3_mk_fpa_sort_64(Context.Context));
+    return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(Context.Context)));
   }
 
   SMTSortRef getFloat128Sort() override {
-    return std::make_shared<Z3Sort>(Context,
-                                    Z3_mk_fpa_sort_128(Context.Context));
-  }
-
-  SMTExprRef newExprRef(const SMTExpr &E) const override {
-    return std::make_shared<Z3Expr>(toZ3Expr(E));
+    return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context)));
   }
 
   SMTExprRef mkBVNeg(const SMTExprRef &Exp) override {
     return newExprRef(
         Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));
   }
 
   SMTExprRef mkBVNot(const SMTExprRef &Exp) override {
public:
   /// Reset the solver and remove all constraints.
   void reset() override { Z3_solver_reset(Context.Context, Solver); }
 
   void print(raw_ostream &OS) const override {
     OS << Z3_solver_to_string(Context.Context, Solver);
   }
 }; // end class Z3Solver
 
-class Z3ConstraintManager : public SMTConstraintManager<ConstraintZ3, Z3Expr> {
+class Z3ConstraintManager : public SMTConstraintManager {
   SMTSolverRef Solver = CreateZ3Solver();
 
 public:
   Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
       : SMTConstraintManager(SE, SB, Solver) {}
 }; // end class Z3ConstraintManager
 
 } // end anonymous namespace