[Patch 2/3]: Rebasing Ryan Govostes' STP patch for Clang SA

[bshastry]

Summary

• Use of std::unique_ptr to return ConstraintManager instance
• Minor changes to CMakeLists.txt to get code to build with mainline code

[rgov]

Adding Anna and Devin as reviewers.

[zaks.anna]

What was the last outstanding issue with this patch (I believe it was related to either make or cmake changes)?
Has it been addressed?

[bshastry]

In D15611#320699, @zaks.anna wrote:

What was the last outstanding issue with this patch (I believe it was related to either make or cmake changes)?
Has it been addressed?

I have tested on a Linux machine and can confirm that it works as documented in the README. The cmake bit of the patch is actually in the third and final sequence of patches for this issue [1].

Caveats:

• stp APIs that the plugin uses need to be statically linked
  • I have only known stp being used by an executable (KLEE) where dynamic linking is a possibility
  • For something that is itself a shared object library (this plugin), static linking is the work-around that I chose

[1]: http://reviews.llvm.org/D15612

include/clang/StaticAnalyzer/Core/Analyses.def

 #endif
 
 ANALYSIS_CONSTRAINTS(RangeConstraints, "range", "Use constraint tracking of concrete value ranges", CreateRangeConstraintManager)
+ANALYSIS_CONSTRAINTS(SMTConstraints, "smt", "Use an SMT solver for constraint tracking", StubCreateSMTConstraintManager)
 
 #ifndef ANALYSIS_DIAGNOSTICS
 #define ANALYSIS_DIAGNOSTICS(NAME, CMDFLAG, DESC, CREATEFN)

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

 CreateRangeConstraintManager(ProgramStateManager &statemgr,
                              SubEngine *subengine);
 
+std::unique_ptr<ConstraintManager>
+StubCreateSMTConstraintManager(ProgramStateManager& statemgr,
+                               SubEngine *subengine);
+
 } // end GR namespace
 
 } // end clang namespace

lib/StaticAnalyzer/Core/CMakeLists.txt

   SimpleConstraintManager.cpp
   SimpleSValBuilder.cpp
   Store.cpp
+  StubSMTConstraintManager.cpp
   SubEngine.cpp
   SymbolManager.cpp
 

lib/StaticAnalyzer/Core/SValBuilder.cpp

                                    BinaryOperator::Opcode Op,
                                    NonLoc LHS, NonLoc RHS,
                                    QualType ResultTy) {
-  if (!State->isTainted(RHS) && !State->isTainted(LHS))
-    return UnknownVal();
+  // TODO: Ask the ConstraintManager if it can handle this SymExpr
+  //if (!State->isTainted(RHS) && !State->isTainted(LHS))
+  //  return UnknownVal();
     
   const SymExpr *symLHS = LHS.getAsSymExpr();
   const SymExpr *symRHS = RHS.getAsSymExpr();

lib/StaticAnalyzer/Core/StubSMTConstraintManager.cpp

+//== StubSMTConstraintManager.cpp -------------------------------*- 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 implements a stub for CreateSMTConstraintManager() that
+//  simply errors if it is invoked without the plug-in enabled.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+
+#include "llvm/Support/DynamicLibrary.h"
+#include "llvm/Support/ErrorHandling.h"
+
+
+using llvm::sys::DynamicLibrary;
+
+
+namespace clang {
+
+namespace ento {
+
+std::unique_ptr<ConstraintManager>
+StubCreateSMTConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
+  static ConstraintManagerCreator CMCreator = NULL;
+  
+  // Attempt to look up the real CreateSMTConstraintManager implementation;
+  // cache the result for the future. 
+  if (!CMCreator) {
+    CMCreator = (ConstraintManagerCreator)(intptr_t)
+      DynamicLibrary::SearchForAddressOfSymbol("CreateSMTConstraintManager");
+  }
+  
+  if (CMCreator)
+    return CMCreator(StMgr, Eng);
+  
+  llvm::report_fatal_error("The SMT constraint manager plug-in is not loaded.");
+  return NULL;
+}
+
+} // end of namespace ento
+
+} // end of namespace clang

tools/CMakeLists.txt

 if(CLANG_ENABLE_STATIC_ANALYZER)
   add_subdirectory(clang-check)
 endif()
+add_subdirectory(smt-constraint-manager)
 
 # We support checking out the clang-tools-extra repository into the 'extra'
 # subdirectory. It contains tools developed as part of the Clang/LLVM project

tools/Makefile

   OPTIONAL_PARALLEL_DIRS :=
 endif
 
+# Build the SMT constraint manager plug-in if STPPREFIX is set.
+ifdef STPPREFIX
+  DIRS += smt-constraint-manager
+endif
+
 include $(CLANG_LEVEL)/Makefile

tools/smt-constraint-manager/CMakeLists.txt

+set(MODULE TRUE)
+
+set( LLVM_LINK_COMPONENTS support mc)
+
+add_library(SMTConstraintManagerPlugin SHARED
+ SMTConstraintManager.cpp)
+
+# add_dependencies(SMTConstraintManagerPlugin
+#   ClangAttrClasses
+#   ClangAttrList
+#   ClangCommentNodes
+#   ClangDeclNodes
+#   ClangDiagnosticCommon
+#   ClangStmtNodes
+#   )
+
+target_link_libraries(SMTConstraintManagerPlugin
+  clangStaticAnalyzerCore
+  )
+
+set_target_properties(SMTConstraintManagerPlugin
+  PROPERTIES
+  LINKER_LANGUAGE CXX
+  PREFIX "")
+
+set (CMAKE_CXX_FLAGS "-std=c++11 -fPIC -pedantic -fno-common -Wcast-qual -fno-strict-aliasing -Wno-long-long -Wall -Wno-unused-parameter -Wwrite-strings -fno-rtti")
+
+set (CMAKE_SHARED_LINKER_FLAGS "-L/usr/local/lib -lstp")

tools/smt-constraint-manager/Makefile

+##===- examples/smt-constraint-manager/Makefile ------------*- Makefile -*-===##
+# 
+#                     The LLVM Compiler Infrastructure
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+# 
+##===----------------------------------------------------------------------===##
+
+CLANG_LEVEL := ../..
+LIBRARYNAME = SMTConstraintManagerPlugin
+
+LINK_LIBS_IN_SHARED = 0
+LOADABLE_MODULE = 1
+
+include $(CLANG_LEVEL)/Makefile
+
+ifeq ($(OS),Darwin)
+  LDFLAGS=-Wl,-undefined,dynamic_lookup
+endif
+
+CXXFLAGS+=-I$(STPPREFIX)/include
+LDFLAGS+=-L$(STPPREFIX)/lib -lstp

tools/smt-constraint-manager/README

+This plug-in implements a constraint manager for the Clang Static Analyzer
+backed by the STP constraint solver:
+
+https://sites.google.com/site/stpfastprover/STP-Fast-Prover
+
+
+## Building
+
+Please build and install STP first.
+
+To build this plug-in, pass the path to the STP installation prefix to make(1):
+
+    make ... STPPREFIX=/usr/local
+
+Please note that CMake is not supported at this time.
+
+
+## Usage
+
+Use the plug-in like so (TODO: easier invocation):
+
+   clang -Xclang -load -Xclang path/to/SMTConstraintManagerPlugin.dylib \
+         -Xanalyzer -analyzer-constraints=smt \
+         --analyze ...
+
+
+## Future
+
+This is an incomplete list.
+
+### Changes to Clang
+
+- Refactor the ConstraintManager base class to eliminate
+    VerySimpleConstraintManager
+- Remove StubSMTConstraintManager with plugin support for constraint managers
+- Make SymIntExpr, IntSymExpr, SymSymExpr subclasses of a BinarySymExpr class,
+    to simplify a number of redundancies
+- Implement a UnarySymExpr for bitwise not (~) and unary minus (-) 
+- Generate implicit SymbolCasts
+
+### Changes to SMTConstraintManager
+
+- Abstract away STP to allow other SMT solvers
+- Verify the memory management of STPExprs
+- Avoid constructing a SymExpr in VerySimpleConstraintManager::assumeSymExpr();
+    it's nice, but the temporary SymExpr is never disposed of
+- Reconsider use of container types; replace with LLVM's efficient containers
+    where possible
+- Improve readability with typedefs for complex types
+- Replace ProgramStateTrait code with REGISTER_TRAIT_WITH_PROGRAMSTATE macro
+- Stop using 'Axiom' and 'Constraint' interchangeably
 No newline at end of file