<div dir="ltr">With the combination of your change and mine (<a href="https://reviews.llvm.org/D31677">https://reviews.llvm.org/D31677</a>), these tests are failing with this pickling error:<div><a href="http://lab.llvm.org:8011/builders/clang-cmake-armv7-a15-full/builds/5629/steps/ninja%20check%201/logs/stdio">http://lab.llvm.org:8011/builders/clang-cmake-armv7-a15-full/builds/5629/steps/ninja%20check%201/logs/stdio</a></div><div><div>cPickle.PicklingError: Can't pickle <class 'lit.TestingConfig.AnalyzerTest'>: attribute lookup lit.TestingConfig.AnalyzerTest failed<br></div></div><div><br></div><div>Any idea what's up? Why does AnalyzerTest multiply inherit from object? That seems unnecessary.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Apr 4, 2017 at 12:52 PM, Dominic Chen via cfe-commits <span dir="ltr"><<a href="mailto:cfe-commits@lists.llvm.org" target="_blank">cfe-commits@lists.llvm.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Author: ddcc<br>
Date: Tue Apr 4 14:52:25 2017<br>
New Revision: 299463<br>
<br>
URL: <a href="http://llvm.org/viewvc/llvm-project?rev=299463&view=rev" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-<wbr>project?rev=299463&view=rev</a><br>
Log:<br>
[analyzer] Add new Z3 constraint manager backend<br>
<br>
Summary: Implement new Z3 constraint manager backend.<br>
<br>
Reviewers: zaks.anna, dcoughlin, NoQ, xazax.hun<br>
<br>
Subscribers: mgorny, cfe-commits<br>
<br>
Differential Revision: <a href="https://reviews.llvm.org/D28952" rel="noreferrer" target="_blank">https://reviews.llvm.org/<wbr>D28952</a><br>
<br>
Added:<br>
cfe/trunk/cmake/modules/<wbr>FindZ3.cmake<br>
cfe/trunk/lib/StaticAnalyzer/<wbr>Core/Z3ConstraintManager.cpp<br>
cfe/trunk/test/Analysis/<wbr>unsupported-types.c<br>
Modified:<br>
cfe/trunk/CMakeLists.txt<br>
cfe/trunk/include/clang/<wbr>Config/config.h.cmake<br>
cfe/trunk/include/clang/<wbr>StaticAnalyzer/Core/Analyses.<wbr>def<br>
cfe/trunk/include/clang/<wbr>StaticAnalyzer/Core/<wbr>PathSensitive/<wbr>ConstraintManager.h<br>
cfe/trunk/lib/StaticAnalyzer/<wbr>Core/CMakeLists.txt<br>
cfe/trunk/test/Analysis/expr-<wbr>inspection.c<br>
cfe/trunk/test/Analysis/lit.<wbr>local.cfg<br>
cfe/trunk/test/lit.cfg<br>
cfe/trunk/test/<a href="http://lit.site.cfg.in" rel="noreferrer" target="_blank">lit.site.cfg.in</a><br>
<br>
Modified: cfe/trunk/CMakeLists.txt<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/CMakeLists.txt?rev=299463&r1=299462&r2=299463&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-<wbr>project/cfe/trunk/CMakeLists.<wbr>txt?rev=299463&r1=299462&r2=<wbr>299463&view=diff</a><br>
==============================<wbr>==============================<wbr>==================<br>
--- cfe/trunk/CMakeLists.txt (original)<br>
+++ cfe/trunk/CMakeLists.txt Tue Apr 4 14:52:25 2017<br>
@@ -186,6 +186,8 @@ if (LIBXML2_FOUND)<br>
set(CLANG_HAVE_LIBXML 1)<br>
endif()<br>
<br>
+find_package(Z3 4.5)<br>
+<br>
include(CheckIncludeFile)<br>
check_include_file(sys/<wbr>resource.h CLANG_HAVE_RLIMITS)<br>
<br>
@@ -330,10 +332,6 @@ if (APPLE)<br>
endif()<br>
endif()<br>
<br>
-configure_file(<br>
- ${CLANG_SOURCE_DIR}/include/<wbr>clang/Config/config.h.cmake<br>
- ${CLANG_BINARY_DIR}/include/<wbr>clang/Config/config.h)<br>
-<br>
include(CMakeParseArguments)<br>
include(AddClang)<br>
<br>
@@ -371,8 +369,19 @@ option(CLANG_BUILD_TOOLS<br>
option(CLANG_ENABLE_ARCMT "Build ARCMT." ON)<br>
option(CLANG_ENABLE_STATIC_<wbr>ANALYZER "Build static analyzer." ON)<br>
<br>
-if (NOT CLANG_ENABLE_STATIC_ANALYZER AND CLANG_ENABLE_ARCMT)<br>
- message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT")<br>
+option(CLANG_ANALYZER_BUILD_<wbr>Z3<br>
+ "Build the static analyzer with the Z3 constraint manager." OFF)<br>
+<br>
+if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR CLANG_ANALYZER_BUILD_Z3))<br>
+ message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3")<br>
+endif()<br>
+<br>
+if(CLANG_ANALYZER_BUILD_Z3)<br>
+ if(Z3_FOUND)<br>
+ set(CLANG_ANALYZER_WITH_Z3 1)<br>
+ else()<br>
+ message(FATAL_ERROR "Cannot find Z3 header file or shared library")<br>
+ endif()<br>
endif()<br>
<br>
if(CLANG_ENABLE_ARCMT)<br>
@@ -687,3 +696,7 @@ endif()<br>
if (LLVM_ADD_NATIVE_VISUALIZERS_<wbr>TO_SOLUTION)<br>
add_subdirectory(utils/<wbr>ClangVisualizers)<br>
endif()<br>
+<br>
+configure_file(<br>
+ ${CLANG_SOURCE_DIR}/include/<wbr>clang/Config/config.h.cmake<br>
+ ${CLANG_BINARY_DIR}/include/<wbr>clang/Config/config.h)<br>
<br>
Added: cfe/trunk/cmake/modules/<wbr>FindZ3.cmake<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/cmake/modules/FindZ3.cmake?rev=299463&view=auto" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-<wbr>project/cfe/trunk/cmake/<wbr>modules/FindZ3.cmake?rev=<wbr>299463&view=auto</a><br>
==============================<wbr>==============================<wbr>==================<br>
--- cfe/trunk/cmake/modules/<wbr>FindZ3.cmake (added)<br>
+++ cfe/trunk/cmake/modules/<wbr>FindZ3.cmake Tue Apr 4 14:52:25 2017<br>
@@ -0,0 +1,28 @@<br>
+find_path(Z3_INCLUDE_DIR NAMES z3.h<br>
+ PATH_SUFFIXES libz3<br>
+ )<br>
+<br>
+find_library(Z3_LIBRARIES NAMES z3 libz3<br>
+ )<br>
+<br>
+find_program(Z3_EXECUTABLE z3)<br>
+<br>
+if(Z3_INCLUDE_DIR AND Z3_EXECUTABLE)<br>
+ execute_process (COMMAND ${Z3_EXECUTABLE} -version<br>
+ OUTPUT_VARIABLE libz3_version_str<br>
+ ERROR_QUIET<br>
+ OUTPUT_STRIP_TRAILING_<wbr>WHITESPACE)<br>
+<br>
+ string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1"<br>
+ Z3_VERSION_STRING "${libz3_version_str}")<br>
+ unset(libz3_version_str)<br>
+endif()<br>
+<br>
+# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if<br>
+# all listed variables are TRUE<br>
+include(<wbr>FindPackageHandleStandardArgs)<br>
+FIND_PACKAGE_HANDLE_STANDARD_<wbr>ARGS(Z3<br>
+ REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR<br>
+ VERSION_VAR Z3_VERSION_STRING)<br>
+<br>
+mark_as_advanced(Z3_INCLUDE_<wbr>DIR Z3_LIBRARIES)<br>
<br>
Modified: cfe/trunk/include/clang/<wbr>Config/config.h.cmake<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/Config/config.h.cmake?rev=299463&r1=299462&r2=299463&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-<wbr>project/cfe/trunk/include/<wbr>clang/Config/config.h.cmake?<wbr>rev=299463&r1=299462&r2=<wbr>299463&view=diff</a><br>
==============================<wbr>==============================<wbr>==================<br>
--- cfe/trunk/include/clang/<wbr>Config/config.h.cmake (original)<br>
+++ cfe/trunk/include/clang/<wbr>Config/config.h.cmake Tue Apr 4 14:52:25 2017<br>
@@ -38,6 +38,9 @@<br>
/* Define if we have libxml2 */<br>
#cmakedefine CLANG_HAVE_LIBXML ${CLANG_HAVE_LIBXML}<br>
<br>
+/* Define if we have z3 and want to build it */<br>
+#cmakedefine CLANG_ANALYZER_WITH_Z3 ${CLANG_ANALYZER_WITH_Z3}<br>
+<br>
/* Define if we have sys/resource.h (rlimits) */<br>
#cmakedefine CLANG_HAVE_RLIMITS ${CLANG_HAVE_RLIMITS}<br>
<br>
<br>
Modified: cfe/trunk/include/clang/<wbr>StaticAnalyzer/Core/Analyses.<wbr>def<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/Analyses.def?rev=299463&r1=299462&r2=299463&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-<wbr>project/cfe/trunk/include/<wbr>clang/StaticAnalyzer/Core/<wbr>Analyses.def?rev=299463&r1=<wbr>299462&r2=299463&view=diff</a><br>
==============================<wbr>==============================<wbr>==================<br>
--- cfe/trunk/include/clang/<wbr>StaticAnalyzer/Core/Analyses.<wbr>def (original)<br>
+++ cfe/trunk/include/clang/<wbr>StaticAnalyzer/Core/Analyses.<wbr>def Tue Apr 4 14:52:25 2017<br>
@@ -22,6 +22,7 @@ ANALYSIS_STORE(RegionStore, "region", "U<br>
#endif<br>
<br>
ANALYSIS_CONSTRAINTS(<wbr>RangeConstraints, "range", "Use constraint tracking of concrete value ranges", CreateRangeConstraintManager)<br>
+ANALYSIS_CONSTRAINTS(<wbr>Z3Constraints, "z3", "Use Z3 contraint solver", CreateZ3ConstraintManager)<br>
<br>
#ifndef ANALYSIS_DIAGNOSTICS<br>
#define ANALYSIS_DIAGNOSTICS(NAME, CMDFLAG, DESC, CREATEFN)<br>
<br>
Modified: cfe/trunk/include/clang/<wbr>StaticAnalyzer/Core/<wbr>PathSensitive/<wbr>ConstraintManager.h<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h?rev=299463&r1=299462&r2=299463&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-<wbr>project/cfe/trunk/include/<wbr>clang/StaticAnalyzer/Core/<wbr>PathSensitive/<wbr>ConstraintManager.h?rev=<wbr>299463&r1=299462&r2=299463&<wbr>view=diff</a><br>
==============================<wbr>==============================<wbr>==================<br>
--- cfe/trunk/include/clang/<wbr>StaticAnalyzer/Core/<wbr>PathSensitive/<wbr>ConstraintManager.h (original)<br>
+++ cfe/trunk/include/clang/<wbr>StaticAnalyzer/Core/<wbr>PathSensitive/<wbr>ConstraintManager.h Tue Apr 4 14:52:25 2017<br>
@@ -184,6 +184,9 @@ std::unique_ptr<<wbr>ConstraintManager><br>
CreateRangeConstraintManager(<wbr>ProgramStateManager &statemgr,<br>
SubEngine *subengine);<br>
<br>
+std::unique_ptr<<wbr>ConstraintManager><br>
+CreateZ3ConstraintManager(<wbr>ProgramStateManager &statemgr, SubEngine *subengine);<br>
+<br>
} // end GR namespace<br>
<br>
} // end clang namespace<br>
<br>
Modified: cfe/trunk/lib/StaticAnalyzer/<wbr>Core/CMakeLists.txt<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt?rev=299463&r1=299462&r2=299463&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-<wbr>project/cfe/trunk/lib/<wbr>StaticAnalyzer/Core/<wbr>CMakeLists.txt?rev=299463&r1=<wbr>299462&r2=299463&view=diff</a><br>
==============================<wbr>==============================<wbr>==================<br>
--- cfe/trunk/lib/StaticAnalyzer/<wbr>Core/CMakeLists.txt (original)<br>
+++ cfe/trunk/lib/StaticAnalyzer/<wbr>Core/CMakeLists.txt Tue Apr 4 14:52:25 2017<br>
@@ -1,5 +1,12 @@<br>
set(LLVM_LINK_COMPONENTS support)<br>
<br>
+# Link Z3 if the user wants to build it.<br>
+if(CLANG_ANALYZER_WITH_Z3)<br>
+ set(Z3_LINK_FILES ${Z3_LIBRARIES})<br>
+else()<br>
+ set(Z3_LINK_FILES "")<br>
+endif()<br>
+<br>
add_clang_library(<wbr>clangStaticAnalyzerCore<br>
APSIntType.cpp<br>
AnalysisManager.cpp<br>
@@ -43,6 +50,7 @@ add_clang_library(<wbr>clangStaticAnalyzerCor<br>
Store.cpp<br>
SubEngine.cpp<br>
SymbolManager.cpp<br>
+ Z3ConstraintManager.cpp<br>
<br>
LINK_LIBS<br>
clangAST<br>
@@ -50,4 +58,12 @@ add_clang_library(<wbr>clangStaticAnalyzerCor<br>
clangBasic<br>
clangLex<br>
clangRewrite<br>
+ ${Z3_LINK_FILES}<br>
)<br>
+<br>
+if(CLANG_ANALYZER_WITH_Z3)<br>
+ target_include_directories(<wbr>clangStaticAnalyzerCore SYSTEM<br>
+ PRIVATE<br>
+ ${Z3_INCLUDE_DIR}<br>
+ )<br>
+endif()<br>
<br>
Added: cfe/trunk/lib/StaticAnalyzer/<wbr>Core/Z3ConstraintManager.cpp<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=299463&view=auto" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-<wbr>project/cfe/trunk/lib/<wbr>StaticAnalyzer/Core/<wbr>Z3ConstraintManager.cpp?rev=<wbr>299463&view=auto</a><br>
==============================<wbr>==============================<wbr>==================<br>
--- cfe/trunk/lib/StaticAnalyzer/<wbr>Core/Z3ConstraintManager.cpp (added)<br>
+++ cfe/trunk/lib/StaticAnalyzer/<wbr>Core/Z3ConstraintManager.cpp Tue Apr 4 14:52:25 2017<br>
@@ -0,0 +1,1618 @@<br>
+//== Z3ConstraintManager.cpp ------------------------------<wbr>--*- C++ -*--==//<br>
+//<br>
+// The LLVM Compiler Infrastructure<br>
+//<br>
+// This file is distributed under the University of Illinois Open Source<br>
+// License. See LICENSE.TXT for details.<br>
+//<br>
+//===------------------------<wbr>------------------------------<wbr>----------------===//<br>
+<br>
+#include "clang/Basic/TargetInfo.h"<br>
+#include "clang/StaticAnalyzer/Core/<wbr>PathSensitive/ExprEngine.h"<br>
+#include "clang/StaticAnalyzer/Core/<wbr>PathSensitive/ProgramState.h"<br>
+#include "clang/StaticAnalyzer/Core/<wbr>PathSensitive/<wbr>SimpleConstraintManager.h"<br>
+<br>
+#include "clang/Config/config.h"<br>
+<br>
+using namespace clang;<br>
+using namespace ento;<br>
+<br>
+#if CLANG_ANALYZER_WITH_Z3<br>
+<br>
+#include <z3.h><br>
+<br>
+// Forward declarations<br>
+namespace {<br>
+class Z3Expr;<br>
+class ConstraintZ3 {};<br>
+} // end anonymous namespace<br>
+<br>
+typedef llvm::ImmutableSet<std::pair<<wbr>SymbolRef, Z3Expr>> ConstraintZ3Ty;<br>
+<br>
+// Expansion of REGISTER_TRAIT_WITH_<wbr>PROGRAMSTATE(ConstraintZ3, Z3SetPair)<br>
+namespace clang {<br>
+namespace ento {<br>
+template <><br>
+struct ProgramStateTrait<<wbr>ConstraintZ3><br>
+ : public ProgramStatePartialTrait<<wbr>ConstraintZ3Ty> {<br>
+ static void *GDMIndex() {<br>
+ static int Index;<br>
+ return &Index;<br>
+ }<br>
+};<br>
+} // end namespace ento<br>
+} // end namespace clang<br>
+<br>
+namespace {<br>
+<br>
+class Z3Config {<br>
+ friend class Z3Context;<br>
+<br>
+ Z3_config Config;<br>
+<br>
+public:<br>
+ Z3Config() : Config(Z3_mk_config()) {<br>
+ // Enable model finding<br>
+ Z3_set_param_value(Config, "model", "true");<br>
+ // Disable proof generation<br>
+ Z3_set_param_value(Config, "proof", "false");<br>
+ // Set timeout to 15000ms = 15s<br>
+ Z3_set_param_value(Config, "timeout", "15000");<br>
+ }<br>
+<br>
+ ~Z3Config() { Z3_del_config(Config); }<br>
+}; // end class Z3Config<br>
+<br>
+class Z3Context {<br>
+ Z3_context ZC_P;<br>
+<br>
+public:<br>
+ static Z3_context ZC;<br>
+<br>
+ Z3Context() : ZC_P(Z3_mk_context_rc(<wbr>Z3Config().Config)) { ZC = ZC_P; }<br>
+<br>
+ ~Z3Context() {<br>
+ Z3_del_context(ZC);<br>
+ Z3_finalize_memory();<br>
+ ZC_P = nullptr;<br>
+ }<br>
+}; // end class Z3Context<br>
+<br>
+class Z3Sort {<br>
+ friend class Z3Expr;<br>
+<br>
+ Z3_sort Sort;<br>
+<br>
+ Z3Sort() : Sort(nullptr) {}<br>
+ Z3Sort(Z3_sort ZS) : Sort(ZS) {<br>
+ Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort)<wbr>);<br>
+ }<br>
+<br>
+public:<br>
+ /// Override implicit copy constructor for correct reference counting.<br>
+ Z3Sort(const Z3Sort &Copy) : Sort(Copy.Sort) {<br>
+ Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort)<wbr>);<br>
+ }<br>
+<br>
+ /// Provide move constructor<br>
+ Z3Sort(Z3Sort &&Move) : Sort(nullptr) { *this = std::move(Move); }<br>
+<br>
+ /// Provide move assignment constructor<br>
+ Z3Sort &operator=(Z3Sort &&Move) {<br>
+ if (this != &Move) {<br>
+ if (Sort)<br>
+ Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort)<wbr>);<br>
+ Sort = Move.Sort;<br>
+ Move.Sort = nullptr;<br>
+ }<br>
+ return *this;<br>
+ }<br>
+<br>
+ ~Z3Sort() {<br>
+ if (Sort)<br>
+ Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort)<wbr>);<br>
+ }<br>
+<br>
+ // Return a boolean sort.<br>
+ static Z3Sort getBoolSort() { return Z3Sort(Z3_mk_bool_sort(<wbr>Z3Context::ZC)); }<br>
+<br>
+ // Return an appropriate bitvector sort for the given bitwidth.<br>
+ static Z3Sort getBitvectorSort(unsigned BitWidth) {<br>
+ return Z3Sort(Z3_mk_bv_sort(<wbr>Z3Context::ZC, BitWidth));<br>
+ }<br>
+<br>
+ // Return an appropriate floating-point sort for the given bitwidth.<br>
+ static Z3Sort getFloatSort(unsigned BitWidth) {<br>
+ Z3_sort Sort;<br>
+<br>
+ switch (BitWidth) {<br>
+ default:<br>
+ llvm_unreachable("Unsupported floating-point bitwidth!");<br>
+ break;<br>
+ case 16:<br>
+ Sort = Z3_mk_fpa_sort_16(Z3Context::<wbr>ZC);<br>
+ break;<br>
+ case 32:<br>
+ Sort = Z3_mk_fpa_sort_32(Z3Context::<wbr>ZC);<br>
+ break;<br>
+ case 64:<br>
+ Sort = Z3_mk_fpa_sort_64(Z3Context::<wbr>ZC);<br>
+ break;<br>
+ case 128:<br>
+ Sort = Z3_mk_fpa_sort_128(Z3Context::<wbr>ZC);<br>
+ break;<br>
+ }<br>
+ return Z3Sort(Sort);<br>
+ }<br>
+<br>
+ // Return an appropriate sort for the given AST.<br>
+ static Z3Sort getSort(Z3_ast AST) {<br>
+ return Z3Sort(Z3_get_sort(Z3Context::<wbr>ZC, AST));<br>
+ }<br>
+<br>
+ Z3_sort_kind getSortKind() const {<br>
+ return Z3_get_sort_kind(Z3Context::<wbr>ZC, Sort);<br>
+ }<br>
+<br>
+ unsigned getBitvectorSortSize() const {<br>
+ assert(getSortKind() == Z3_BV_SORT && "Not a bitvector sort!");<br>
+ return Z3_get_bv_sort_size(Z3Context:<wbr>:ZC, Sort);<br>
+ }<br>
+<br>
+ unsigned getFloatSortSize() const {<br>
+ assert(getSortKind() == Z3_FLOATING_POINT_SORT &&<br>
+ "Not a floating-point sort!");<br>
+ return Z3_fpa_get_ebits(Z3Context::<wbr>ZC, Sort) +<br>
+ Z3_fpa_get_sbits(Z3Context::<wbr>ZC, Sort);<br>
+ }<br>
+<br>
+ bool operator==(const Z3Sort &Other) const {<br>
+ return Z3_is_eq_sort(Z3Context::ZC, Sort, Other.Sort);<br>
+ }<br>
+<br>
+ Z3Sort &operator=(const Z3Sort &Move) {<br>
+ Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Move.<wbr>Sort));<br>
+ Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort)<wbr>);<br>
+ Sort = Move.Sort;<br>
+ return *this;<br>
+ }<br>
+<br>
+ void print(raw_ostream &OS) const {<br>
+ OS << Z3_sort_to_string(Z3Context::<wbr>ZC, Sort);<br>
+ }<br>
+<br>
+ LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }<br>
+}; // end class Z3Sort<br>
+<br>
+class Z3Expr {<br>
+ friend class Z3Model;<br>
+ friend class Z3Solver;<br>
+<br>
+ Z3_ast AST;<br>
+<br>
+ Z3Expr(Z3_ast ZA) : AST(ZA) { Z3_inc_ref(Z3Context::ZC, AST); }<br>
+<br>
+ // Return an appropriate floating-point rounding mode.<br>
+ static Z3Expr getFloatRoundingMode() {<br>
+ // TODO: Don't assume nearest ties to even rounding mode<br>
+ return Z3Expr(Z3_mk_fpa_rne(<wbr>Z3Context::ZC));<br>
+ }<br>
+<br>
+ // Determine whether two float semantics are equivalent<br>
+ static bool areEquivalent(const llvm::fltSemantics &LHS,<br>
+ const llvm::fltSemantics &RHS) {<br>
+ return (llvm::APFloat::<wbr>semanticsPrecision(LHS) ==<br>
+ llvm::APFloat::<wbr>semanticsPrecision(RHS)) &&<br>
+ (llvm::APFloat::<wbr>semanticsMinExponent(LHS) ==<br>
+ llvm::APFloat::<wbr>semanticsMinExponent(RHS)) &&<br>
+ (llvm::APFloat::<wbr>semanticsMaxExponent(LHS) ==<br>
+ llvm::APFloat::<wbr>semanticsMaxExponent(RHS)) &&<br>
+ (llvm::APFloat::<wbr>semanticsSizeInBits(LHS) ==<br>
+ llvm::APFloat::<wbr>semanticsSizeInBits(RHS));<br>
+ }<br>
+<br>
+public:<br>
+ /// Override implicit copy constructor for correct reference counting.<br>
+ Z3Expr(const Z3Expr &Copy) : AST(Copy.AST) { Z3_inc_ref(Z3Context::ZC, AST); }<br>
+<br>
+ /// Provide move constructor<br>
+ Z3Expr(Z3Expr &&Move) : AST(nullptr) { *this = std::move(Move); }<br>
+<br>
+ /// Provide move assignment constructor<br>
+ Z3Expr &operator=(Z3Expr &&Move) {<br>
+ if (this != &Move) {<br>
+ if (AST)<br>
+ Z3_dec_ref(Z3Context::ZC, AST);<br>
+ AST = Move.AST;<br>
+ Move.AST = nullptr;<br>
+ }<br>
+ return *this;<br>
+ }<br>
+<br>
+ ~Z3Expr() {<br>
+ if (AST)<br>
+ Z3_dec_ref(Z3Context::ZC, AST);<br>
+ }<br>
+<br>
+ /// Get the corresponding IEEE floating-point type for a given bitwidth.<br>
+ static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {<br>
+ switch (BitWidth) {<br>
+ default:<br>
+ llvm_unreachable("Unsupported floating-point semantics!");<br>
+ break;<br>
+ case 16:<br>
+ return llvm::APFloat::IEEEhalf();<br>
+ case 32:<br>
+ return llvm::APFloat::IEEEsingle();<br>
+ case 64:<br>
+ return llvm::APFloat::IEEEdouble();<br>
+ case 128:<br>
+ return llvm::APFloat::IEEEquad();<br>
+ }<br>
+ }<br>
+<br>
+ /// Construct a Z3Expr from a unary operator, given a Z3_context.<br>
+ static Z3Expr fromUnOp(const UnaryOperator::Opcode Op, const Z3Expr &Exp) {<br>
+ Z3_ast AST;<br>
+<br>
+ switch (Op) {<br>
+ default:<br>
+ llvm_unreachable("<wbr>Unimplemented opcode");<br>
+ break;<br>
+<br>
+ case UO_Minus:<br>
+ AST = Z3_mk_bvneg(Z3Context::ZC, Exp.AST);<br>
+ break;<br>
+<br>
+ case UO_Not:<br>
+ AST = Z3_mk_bvnot(Z3Context::ZC, Exp.AST);<br>
+ break;<br>
+<br>
+ case UO_LNot:<br>
+ AST = Z3_mk_not(Z3Context::ZC, Exp.AST);<br>
+ break;<br>
+ }<br>
+<br>
+ return Z3Expr(AST);<br>
+ }<br>
+<br>
+ /// Construct a Z3Expr from a floating-point unary operator, given a<br>
+ /// Z3_context.<br>
+ static Z3Expr fromFloatUnOp(const UnaryOperator::Opcode Op,<br>
+ const Z3Expr &Exp) {<br>
+ Z3_ast AST;<br>
+<br>
+ switch (Op) {<br>
+ default:<br>
+ llvm_unreachable("<wbr>Unimplemented opcode");<br>
+ break;<br>
+<br>
+ case UO_Minus:<br>
+ AST = Z3_mk_fpa_neg(Z3Context::ZC, Exp.AST);<br>
+ break;<br>
+<br>
+ case UO_LNot:<br>
+ return Z3Expr::fromUnOp(Op, Exp);<br>
+ }<br>
+<br>
+ return Z3Expr(AST);<br>
+ }<br>
+<br>
+ /// Construct a Z3Expr from a n-ary binary operator.<br>
+ static Z3Expr fromNBinOp(const BinaryOperator::Opcode Op,<br>
+ const std::vector<Z3_ast> &ASTs) {<br>
+ Z3_ast AST;<br>
+<br>
+ switch (Op) {<br>
+ default:<br>
+ llvm_unreachable("<wbr>Unimplemented opcode");<br>
+ break;<br>
+<br>
+ case BO_LAnd:<br>
+ AST = Z3_mk_and(Z3Context::ZC, ASTs.size(), ASTs.data());<br>
+ break;<br>
+<br>
+ case BO_LOr:<br>
+ AST = Z3_mk_or(Z3Context::ZC, ASTs.size(), ASTs.data());<br>
+ break;<br>
+ }<br>
+<br>
+ return Z3Expr(AST);<br>
+ }<br>
+<br>
+ /// Construct a Z3Expr from a binary operator, given a Z3_context.<br>
+ static Z3Expr fromBinOp(const Z3Expr &LHS, const BinaryOperator::Opcode Op,<br>
+ const Z3Expr &RHS, bool isSigned) {<br>
+ Z3_ast AST;<br>
+<br>
+ assert(Z3Sort::getSort(LHS.<wbr>AST) == Z3Sort::getSort(RHS.AST) &&<br>
+ "AST's must have the same sort!");<br>
+<br>
+ switch (Op) {<br>
+ default:<br>
+ llvm_unreachable("<wbr>Unimplemented opcode");<br>
+ break;<br>
+<br>
+ // Multiplicative operators<br>
+ case BO_Mul:<br>
+ AST = Z3_mk_bvmul(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+ case BO_Div:<br>
+ AST = isSigned ? Z3_mk_bvsdiv(Z3Context::ZC, LHS.AST, RHS.AST)<br>
+ : Z3_mk_bvudiv(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+ case BO_Rem:<br>
+ AST = isSigned ? Z3_mk_bvsrem(Z3Context::ZC, LHS.AST, RHS.AST)<br>
+ : Z3_mk_bvurem(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+<br>
+ // Additive operators<br>
+ case BO_Add:<br>
+ AST = Z3_mk_bvadd(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+ case BO_Sub:<br>
+ AST = Z3_mk_bvsub(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+<br>
+ // Bitwise shift operators<br>
+ case BO_Shl:<br>
+ AST = Z3_mk_bvshl(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+ case BO_Shr:<br>
+ AST = isSigned ? Z3_mk_bvashr(Z3Context::ZC, LHS.AST, RHS.AST)<br>
+ : Z3_mk_bvlshr(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+<br>
+ // Relational operators<br>
+ case BO_LT:<br>
+ AST = isSigned ? Z3_mk_bvslt(Z3Context::ZC, LHS.AST, RHS.AST)<br>
+ : Z3_mk_bvult(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+ case BO_GT:<br>
+ AST = isSigned ? Z3_mk_bvsgt(Z3Context::ZC, LHS.AST, RHS.AST)<br>
+ : Z3_mk_bvugt(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+ case BO_LE:<br>
+ AST = isSigned ? Z3_mk_bvsle(Z3Context::ZC, LHS.AST, RHS.AST)<br>
+ : Z3_mk_bvule(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+ case BO_GE:<br>
+ AST = isSigned ? Z3_mk_bvsge(Z3Context::ZC, LHS.AST, RHS.AST)<br>
+ : Z3_mk_bvuge(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+<br>
+ // Equality operators<br>
+ case BO_EQ:<br>
+ AST = Z3_mk_eq(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+ case BO_NE:<br>
+ return Z3Expr::fromUnOp(UO_LNot,<br>
+ Z3Expr::fromBinOp(LHS, BO_EQ, RHS, isSigned));<br>
+ break;<br>
+<br>
+ // Bitwise operators<br>
+ case BO_And:<br>
+ AST = Z3_mk_bvand(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+ case BO_Xor:<br>
+ AST = Z3_mk_bvxor(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+ case BO_Or:<br>
+ AST = Z3_mk_bvor(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+<br>
+ // Logical operators<br>
+ case BO_LAnd:<br>
+ case BO_LOr: {<br>
+ std::vector<Z3_ast> Args = {LHS.AST, RHS.AST};<br>
+ return Z3Expr::fromNBinOp(Op, Args);<br>
+ }<br>
+ }<br>
+<br>
+ return Z3Expr(AST);<br>
+ }<br>
+<br>
+ /// Construct a Z3Expr from a special floating-point binary operator, given<br>
+ /// a Z3_context.<br>
+ static Z3Expr fromFloatSpecialBinOp(const Z3Expr &LHS,<br>
+ const BinaryOperator::Opcode Op,<br>
+ const llvm::APFloat::fltCategory &RHS) {<br>
+ Z3_ast AST;<br>
+<br>
+ switch (Op) {<br>
+ default:<br>
+ llvm_unreachable("<wbr>Unimplemented opcode");<br>
+ break;<br>
+<br>
+ // Equality operators<br>
+ case BO_EQ:<br>
+ switch (RHS) {<br>
+ case llvm::APFloat::fcInfinity:<br>
+ AST = Z3_mk_fpa_is_infinite(<wbr>Z3Context::ZC, LHS.AST);<br>
+ break;<br>
+ case llvm::APFloat::fcNaN:<br>
+ AST = Z3_mk_fpa_is_nan(Z3Context::<wbr>ZC, LHS.AST);<br>
+ break;<br>
+ case llvm::APFloat::fcNormal:<br>
+ AST = Z3_mk_fpa_is_normal(Z3Context:<wbr>:ZC, LHS.AST);<br>
+ break;<br>
+ case llvm::APFloat::fcZero:<br>
+ AST = Z3_mk_fpa_is_zero(Z3Context::<wbr>ZC, LHS.AST);<br>
+ break;<br>
+ }<br>
+ break;<br>
+ case BO_NE:<br>
+ return Z3Expr::fromFloatUnOp(<br>
+ UO_LNot, Z3Expr::fromFloatSpecialBinOp(<wbr>LHS, BO_EQ, RHS));<br>
+ break;<br>
+ }<br>
+<br>
+ return Z3Expr(AST);<br>
+ }<br>
+<br>
+ /// Construct a Z3Expr from a floating-point binary operator, given a<br>
+ /// Z3_context.<br>
+ static Z3Expr fromFloatBinOp(const Z3Expr &LHS,<br>
+ const BinaryOperator::Opcode Op,<br>
+ const Z3Expr &RHS) {<br>
+ Z3_ast AST;<br>
+<br>
+ assert(Z3Sort::getSort(LHS.<wbr>AST) == Z3Sort::getSort(RHS.AST) &&<br>
+ "AST's must have the same sort!");<br>
+<br>
+ switch (Op) {<br>
+ default:<br>
+ llvm_unreachable("<wbr>Unimplemented opcode");<br>
+ break;<br>
+<br>
+ // Multiplicative operators<br>
+ case BO_Mul: {<br>
+ Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode()<wbr>;<br>
+ AST = Z3_mk_fpa_mul(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);<br>
+ break;<br>
+ }<br>
+ case BO_Div: {<br>
+ Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode()<wbr>;<br>
+ AST = Z3_mk_fpa_div(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);<br>
+ break;<br>
+ }<br>
+ case BO_Rem:<br>
+ AST = Z3_mk_fpa_rem(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+<br>
+ // Additive operators<br>
+ case BO_Add: {<br>
+ Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode()<wbr>;<br>
+ AST = Z3_mk_fpa_add(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);<br>
+ break;<br>
+ }<br>
+ case BO_Sub: {<br>
+ Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode()<wbr>;<br>
+ AST = Z3_mk_fpa_sub(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);<br>
+ break;<br>
+ }<br>
+<br>
+ // Relational operators<br>
+ case BO_LT:<br>
+ AST = Z3_mk_fpa_lt(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+ case BO_GT:<br>
+ AST = Z3_mk_fpa_gt(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+ case BO_LE:<br>
+ AST = Z3_mk_fpa_leq(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+ case BO_GE:<br>
+ AST = Z3_mk_fpa_geq(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+<br>
+ // Equality operators<br>
+ case BO_EQ:<br>
+ AST = Z3_mk_fpa_eq(Z3Context::ZC, LHS.AST, RHS.AST);<br>
+ break;<br>
+ case BO_NE:<br>
+ return Z3Expr::fromFloatUnOp(UO_LNot,<br>
+ Z3Expr::fromFloatBinOp(LHS, BO_EQ, RHS));<br>
+ break;<br>
+<br>
+ // Logical operators<br>
+ case BO_LAnd:<br>
+ case BO_LOr:<br>
+ return Z3Expr::fromBinOp(LHS, Op, RHS, false);<br>
+ }<br>
+<br>
+ return Z3Expr(AST);<br>
+ }<br>
+<br>
+ /// Construct a Z3Expr from a SymbolData, given a Z3_context.<br>
+ static Z3Expr fromData(const SymbolID ID, bool isBool, bool isFloat,<br>
+ uint64_t BitWidth) {<br>
+ llvm::Twine Name = "$" + llvm::Twine(ID);<br>
+<br>
+ Z3Sort Sort;<br>
+ if (isBool)<br>
+ Sort = Z3Sort::getBoolSort();<br>
+ else if (isFloat)<br>
+ Sort = Z3Sort::getFloatSort(BitWidth)<wbr>;<br>
+ else<br>
+ Sort = Z3Sort::getBitvectorSort(<wbr>BitWidth);<br>
+<br>
+ Z3_symbol Symbol = Z3_mk_string_symbol(Z3Context:<wbr>:ZC, Name.str().c_str());<br>
+ Z3_ast AST = Z3_mk_const(Z3Context::ZC, Symbol, Sort.Sort);<br>
+ return Z3Expr(AST);<br>
+ }<br>
+<br>
+ /// Construct a Z3Expr from a SymbolCast, given a Z3_context.<br>
+ static Z3Expr fromCast(const Z3Expr &Exp, QualType ToTy, uint64_t ToBitWidth,<br>
+ QualType FromTy, uint64_t FromBitWidth) {<br>
+ Z3_ast AST;<br>
+<br>
+ if ((FromTy-><wbr>isIntegralOrEnumerationType() &&<br>
+ ToTy-><wbr>isIntegralOrEnumerationType()) ||<br>
+ (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||<br>
+ (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||<br>
+ (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {<br>
+ // Special case: Z3 boolean type is distinct from bitvector type, so<br>
+ // must use if-then-else expression instead of direct cast<br>
+ if (FromTy->isBooleanType()) {<br>
+ assert(ToBitWidth > 0 && "BitWidth must be positive!");<br>
+ Z3Expr Zero = Z3Expr::fromInt("0", ToBitWidth);<br>
+ Z3Expr One = Z3Expr::fromInt("1", ToBitWidth);<br>
+ AST = Z3_mk_ite(Z3Context::ZC, Exp.AST, One.AST, Zero.AST);<br>
+ } else if (ToBitWidth > FromBitWidth) {<br>
+ AST = FromTy-><wbr>isSignedIntegerOrEnumerationTy<wbr>pe()<br>
+ ? Z3_mk_sign_ext(Z3Context::ZC, ToBitWidth - FromBitWidth,<br>
+ Exp.AST)<br>
+ : Z3_mk_zero_ext(Z3Context::ZC, ToBitWidth - FromBitWidth,<br>
+ Exp.AST);<br>
+ } else if (ToBitWidth < FromBitWidth) {<br>
+ AST = Z3_mk_extract(Z3Context::ZC, ToBitWidth - 1, 0, Exp.AST);<br>
+ } else {<br>
+ // Both are bitvectors with the same width, ignore the type cast<br>
+ return Exp;<br>
+ }<br>
+ } else if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {<br>
+ if (ToBitWidth != FromBitWidth) {<br>
+ Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode()<wbr>;<br>
+ Z3Sort Sort = Z3Sort::getFloatSort(<wbr>ToBitWidth);<br>
+ AST = Z3_mk_fpa_to_fp_float(<wbr>Z3Context::ZC, RoundingMode.AST, Exp.AST,<br>
+ Sort.Sort);<br>
+ } else {<br>
+ return Exp;<br>
+ }<br>
+ } else if (FromTy-><wbr>isIntegralOrEnumerationType() &&<br>
+ ToTy->isRealFloatingType()) {<br>
+ Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode()<wbr>;<br>
+ Z3Sort Sort = Z3Sort::getFloatSort(<wbr>ToBitWidth);<br>
+ AST = FromTy-><wbr>isSignedIntegerOrEnumerationTy<wbr>pe()<br>
+ ? Z3_mk_fpa_to_fp_signed(<wbr>Z3Context::ZC, RoundingMode.AST,<br>
+ Exp.AST, Sort.Sort)<br>
+ : Z3_mk_fpa_to_fp_unsigned(<wbr>Z3Context::ZC, RoundingMode.AST,<br>
+ Exp.AST, Sort.Sort);<br>
+ } else if (FromTy->isRealFloatingType() &&<br>
+ ToTy-><wbr>isIntegralOrEnumerationType()) {<br>
+ Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode()<wbr>;<br>
+ AST = ToTy-><wbr>isSignedIntegerOrEnumerationTy<wbr>pe()<br>
+ ? Z3_mk_fpa_to_sbv(Z3Context::<wbr>ZC, RoundingMode.AST, Exp.AST,<br>
+ ToBitWidth)<br>
+ : Z3_mk_fpa_to_ubv(Z3Context::<wbr>ZC, RoundingMode.AST, Exp.AST,<br>
+ ToBitWidth);<br>
+ } else {<br>
+ llvm_unreachable("Unsupported explicit type cast!");<br>
+ }<br>
+<br>
+ return Z3Expr(AST);<br>
+ }<br>
+<br>
+ /// Construct a Z3Expr from a boolean, given a Z3_context.<br>
+ static Z3Expr fromBoolean(const bool Bool) {<br>
+ Z3_ast AST = Bool ? Z3_mk_true(Z3Context::ZC) : Z3_mk_false(Z3Context::ZC);<br>
+ return Z3Expr(AST);<br>
+ }<br>
+<br>
+ /// Construct a Z3Expr from a finite APFloat, given a Z3_context.<br>
+ static Z3Expr fromAPFloat(const llvm::APFloat &Float) {<br>
+ Z3_ast AST;<br>
+ Z3Sort Sort = Z3Sort::getFloatSort(<br>
+ llvm::APFloat::<wbr>semanticsSizeInBits(Float.<wbr>getSemantics()));<br>
+<br>
+ llvm::APSInt Int = llvm::APSInt(Float.<wbr>bitcastToAPInt(), true);<br>
+ Z3Expr Z3Int = Z3Expr::fromAPSInt(Int);<br>
+ AST = Z3_mk_fpa_to_fp_bv(Z3Context::<wbr>ZC, Z3Int.AST, Sort.Sort);<br>
+<br>
+ return Z3Expr(AST);<br>
+ }<br>
+<br>
+ /// Construct a Z3Expr from an APSInt, given a Z3_context.<br>
+ static Z3Expr fromAPSInt(const llvm::APSInt &Int) {<br>
+ Z3Sort Sort = Z3Sort::getBitvectorSort(Int.<wbr>getBitWidth());<br>
+ Z3_ast AST =<br>
+ Z3_mk_numeral(Z3Context::ZC, Int.toString(10).c_str(), Sort.Sort);<br>
+ return Z3Expr(AST);<br>
+ }<br>
+<br>
+ /// Construct a Z3Expr from an integer, given a Z3_context.<br>
+ static Z3Expr fromInt(const char *Int, uint64_t BitWidth) {<br>
+ Z3Sort Sort = Z3Sort::getBitvectorSort(<wbr>BitWidth);<br>
+ Z3_ast AST = Z3_mk_numeral(Z3Context::ZC, Int, Sort.Sort);<br>
+ return Z3Expr(AST);<br>
+ }<br>
+<br>
+ /// Construct an APFloat from a Z3Expr, given the AST representation<br>
+ static bool toAPFloat(const Z3Sort &Sort, const Z3_ast &AST,<br>
+ llvm::APFloat &Float, bool useSemantics = true) {<br>
+ assert(Sort.getSortKind() == Z3_FLOATING_POINT_SORT &&<br>
+ "Unsupported sort to floating-point!");<br>
+<br>
+ llvm::APSInt Int(Sort.getFloatSortSize(), true);<br>
+ const llvm::fltSemantics &Semantics =<br>
+ Z3Expr::getFloatSemantics(<wbr>Sort.getFloatSortSize());<br>
+ Z3Sort BVSort = Z3Sort::getBitvectorSort(Sort.<wbr>getFloatSortSize());<br>
+ if (!Z3Expr::toAPSInt(BVSort, AST, Int, true)) {<br>
+ return false;<br>
+ }<br>
+<br>
+ if (useSemantics &&<br>
+ !Z3Expr::areEquivalent(Float.<wbr>getSemantics(), Semantics)) {<br>
+ assert(false && "Floating-point types don't match!");<br>
+ return false;<br>
+ }<br>
+<br>
+ Float = llvm::APFloat(Semantics, Int);<br>
+ return true;<br>
+ }<br>
+<br>
+ /// Construct an APSInt from a Z3Expr, given the AST representation<br>
+ static bool toAPSInt(const Z3Sort &Sort, const Z3_ast &AST, llvm::APSInt &Int,<br>
+ bool useSemantics = true) {<br>
+ switch (Sort.getSortKind()) {<br>
+ default:<br>
+ llvm_unreachable("Unsupported sort to integer!");<br>
+ case Z3_BV_SORT: {<br>
+ if (useSemantics && Int.getBitWidth() != Sort.getBitvectorSortSize()) {<br>
+ assert(false && "Bitvector types don't match!");<br>
+ return false;<br>
+ }<br>
+<br>
+ uint64_t Value[2];<br>
+ // Force cast because Z3 defines __uint64 to be a unsigned long long<br>
+ // type, which isn't compatible with a unsigned long type, even if they<br>
+ // are the same size.<br>
+ Z3_get_numeral_uint64(<wbr>Z3Context::ZC, AST,<br>
+ reinterpret_cast<__uint64 *>(&Value[0]));<br>
+ if (Sort.getBitvectorSortSize() <= 64) {<br>
+ Int = llvm::APSInt(llvm::APInt(Int.<wbr>getBitWidth(), Value[0]), true);<br>
+ } else if (Sort.getBitvectorSortSize() == 128) {<br>
+ Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(<wbr>Z3Context::ZC, 127, 64, AST));<br>
+ Z3_get_numeral_uint64(<wbr>Z3Context::ZC, AST,<br>
+ reinterpret_cast<__uint64 *>(&Value[1]));<br>
+ Int = llvm::APSInt(llvm::APInt(Int.<wbr>getBitWidth(), Value), true);<br>
+ } else {<br>
+ assert(false && "Bitwidth not supported!");<br>
+ return false;<br>
+ }<br>
+ return true;<br>
+ }<br>
+ case Z3_BOOL_SORT:<br>
+ if (useSemantics && Int.getBitWidth() < 1) {<br>
+ assert(false && "Boolean type doesn't match!");<br>
+ return false;<br>
+ }<br>
+ Int = llvm::APSInt(<br>
+ llvm::APInt(Int.getBitWidth(),<br>
+ Z3_get_bool_value(Z3Context::<wbr>ZC, AST) == Z3_L_TRUE ? 1<br>
+ : 0),<br>
+ true);<br>
+ return true;<br>
+ }<br>
+ }<br>
+<br>
+ void Profile(llvm::FoldingSetNodeID &ID) const {<br>
+ ID.AddInteger(Z3_get_ast_hash(<wbr>Z3Context::ZC, AST));<br>
+ }<br>
+<br>
+ bool operator<(const Z3Expr &Other) const {<br>
+ llvm::FoldingSetNodeID ID1, ID2;<br>
+ Profile(ID1);<br>
+ Other.Profile(ID2);<br>
+ return ID1 < ID2;<br>
+ }<br>
+<br>
+ /// Comparison of AST equality, not model equivalence.<br>
+ bool operator==(const Z3Expr &Other) const {<br>
+ assert(Z3_is_eq_sort(<wbr>Z3Context::ZC, Z3_get_sort(Z3Context::ZC, AST),<br>
+ Z3_get_sort(Z3Context::ZC, Other.AST)) &&<br>
+ "AST's must have the same sort");<br>
+ return Z3_is_eq_ast(Z3Context::ZC, AST, Other.AST);<br>
+ }<br>
+<br>
+ /// Override implicit move constructor for correct reference counting.<br>
+ Z3Expr &operator=(const Z3Expr &Move) {<br>
+ Z3_inc_ref(Z3Context::ZC, Move.AST);<br>
+ Z3_dec_ref(Z3Context::ZC, AST);<br>
+ AST = Move.AST;<br>
+ return *this;<br>
+ }<br>
+<br>
+ void print(raw_ostream &OS) const {<br>
+ OS << Z3_ast_to_string(Z3Context::<wbr>ZC, AST);<br>
+ }<br>
+<br>
+ LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }<br>
+}; // end class Z3Expr<br>
+<br>
+class Z3Model {<br>
+ Z3_model Model;<br>
+<br>
+public:<br>
+ Z3Model(Z3_model ZM) : Model(ZM) { Z3_model_inc_ref(Z3Context::<wbr>ZC, Model); }<br>
+<br>
+ /// Override implicit copy constructor for correct reference counting.<br>
+ Z3Model(const Z3Model &Copy) : Model(Copy.Model) {<br>
+ Z3_model_inc_ref(Z3Context::<wbr>ZC, Model);<br>
+ }<br>
+<br>
+ /// Provide move constructor<br>
+ Z3Model(Z3Model &&Move) : Model(nullptr) { *this = std::move(Move); }<br>
+<br>
+ /// Provide move assignment constructor<br>
+ Z3Model &operator=(Z3Model &&Move) {<br>
+ if (this != &Move) {<br>
+ if (Model)<br>
+ Z3_model_dec_ref(Z3Context::<wbr>ZC, Model);<br>
+ Model = Move.Model;<br>
+ Move.Model = nullptr;<br>
+ }<br>
+ return *this;<br>
+ }<br>
+<br>
+ ~Z3Model() {<br>
+ if (Model)<br>
+ Z3_model_dec_ref(Z3Context::<wbr>ZC, Model);<br>
+ }<br>
+<br>
+ /// Given an expression, extract the value of this operand in the model.<br>
+ bool getInterpretation(const Z3Expr &Exp, llvm::APSInt &Int) const {<br>
+ Z3_func_decl Func =<br>
+ Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));<br>
+ if (Z3_model_has_interp(<wbr>Z3Context::ZC, Model, Func) != Z3_L_TRUE)<br>
+ return false;<br>
+<br>
+ Z3_ast Assign = Z3_model_get_const_interp(<wbr>Z3Context::ZC, Model, Func);<br>
+ Z3Sort Sort = Z3Sort::getSort(Assign);<br>
+ return Z3Expr::toAPSInt(Sort, Assign, Int, true);<br>
+ }<br>
+<br>
+ /// Given an expression, extract the value of this operand in the model.<br>
+ bool getInterpretation(const Z3Expr &Exp, llvm::APFloat &Float) const {<br>
+ Z3_func_decl Func =<br>
+ Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));<br>
+ if (Z3_model_has_interp(<wbr>Z3Context::ZC, Model, Func) != Z3_L_TRUE)<br>
+ return false;<br>
+<br>
+ Z3_ast Assign = Z3_model_get_const_interp(<wbr>Z3Context::ZC, Model, Func);<br>
+ Z3Sort Sort = Z3Sort::getSort(Assign);<br>
+ return Z3Expr::toAPFloat(Sort, Assign, Float, true);<br>
+ }<br>
+<br>
+ void print(raw_ostream &OS) const {<br>
+ OS << Z3_model_to_string(Z3Context::<wbr>ZC, Model);<br>
+ }<br>
+<br>
+ LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }<br>
+}; // end class Z3Model<br>
+<br>
+class Z3Solver {<br>
+ friend class Z3ConstraintManager;<br>
+<br>
+ Z3_solver Solver;<br>
+<br>
+ Z3Solver(Z3_solver ZS) : Solver(ZS) {<br>
+ Z3_solver_inc_ref(Z3Context::<wbr>ZC, Solver);<br>
+ }<br>
+<br>
+public:<br>
+ /// Override implicit copy constructor for correct reference counting.<br>
+ Z3Solver(const Z3Solver &Copy) : Solver(Copy.Solver) {<br>
+ Z3_solver_inc_ref(Z3Context::<wbr>ZC, Solver);<br>
+ }<br>
+<br>
+ /// Provide move constructor<br>
+ Z3Solver(Z3Solver &&Move) : Solver(nullptr) { *this = std::move(Move); }<br>
+<br>
+ /// Provide move assignment constructor<br>
+ Z3Solver &operator=(Z3Solver &&Move) {<br>
+ if (this != &Move) {<br>
+ if (Solver)<br>
+ Z3_solver_dec_ref(Z3Context::<wbr>ZC, Solver);<br>
+ Solver = Move.Solver;<br>
+ Move.Solver = nullptr;<br>
+ }<br>
+ return *this;<br>
+ }<br>
+<br>
+ ~Z3Solver() {<br>
+ if (Solver)<br>
+ Z3_solver_dec_ref(Z3Context::<wbr>ZC, Solver);<br>
+ }<br>
+<br>
+ /// Given a constraint, add it to the solver<br>
+ void addConstraint(const Z3Expr &Exp) {<br>
+ Z3_solver_assert(Z3Context::<wbr>ZC, Solver, Exp.AST);<br>
+ }<br>
+<br>
+ /// Given a program state, construct the logical conjunction and add it to<br>
+ /// the solver<br>
+ void addStateConstraints(<wbr>ProgramStateRef State) {<br>
+ // TODO: Don't add all the constraints, only the relevant ones<br>
+ ConstraintZ3Ty CZ = State->get<ConstraintZ3>();<br>
+ ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();<br>
+<br>
+ // Construct the logical AND of all the constraints<br>
+ if (I != IE) {<br>
+ std::vector<Z3_ast> ASTs;<br>
+<br>
+ while (I != IE)<br>
+ ASTs.push_back(I++->second.<wbr>AST);<br>
+<br>
+ Z3Expr Conj = Z3Expr::fromNBinOp(BO_LAnd, ASTs);<br>
+ addConstraint(Conj);<br>
+ }<br>
+ }<br>
+<br>
+ /// Check if the constraints are satisfiable<br>
+ Z3_lbool check() { return Z3_solver_check(Z3Context::ZC, Solver); }<br>
+<br>
+ /// Push the current solver state<br>
+ void push() { return Z3_solver_push(Z3Context::ZC, Solver); }<br>
+<br>
+ /// Pop the previous solver state<br>
+ void pop(unsigned NumStates = 1) {<br>
+ assert(Z3_solver_get_num_<wbr>scopes(Z3Context::ZC, Solver) >= NumStates);<br>
+ return Z3_solver_pop(Z3Context::ZC, Solver, NumStates);<br>
+ }<br>
+<br>
+ /// Get a model from the solver. Caller should check the model is<br>
+ /// satisfiable.<br>
+ Z3Model getModel() {<br>
+ return Z3Model(Z3_solver_get_model(<wbr>Z3Context::ZC, Solver));<br>
+ }<br>
+<br>
+ /// Reset the solver and remove all constraints.<br>
+ void reset() { Z3_solver_reset(Z3Context::ZC, Solver); }<br>
+}; // end class Z3Solver<br>
+<br>
+void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {<br>
+ llvm::report_fatal_error("Z3 error: " +<br>
+ llvm::Twine(Z3_get_error_msg_<wbr>ex(Context, Error)));<br>
+}<br>
+<br>
+class Z3ConstraintManager : public SimpleConstraintManager {<br>
+ Z3Context Context;<br>
+ mutable Z3Solver Solver;<br>
+<br>
+public:<br>
+ Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)<br>
+ : SimpleConstraintManager(SE, SB),<br>
+ Solver(Z3_mk_simple_solver(<wbr>Z3Context::ZC)) {<br>
+ Z3_set_error_handler(<wbr>Z3Context::ZC, Z3ErrorHandler);<br>
+ }<br>
+<br>
+ //===-------------------------<wbr>------------------------------<wbr>-----------===//<br>
+ // Implementation for interface from ConstraintManager.<br>
+ //===-------------------------<wbr>------------------------------<wbr>-----------===//<br>
+<br>
+ bool canReasonAbout(SVal X) const override;<br>
+<br>
+ ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;<br>
+<br>
+ const llvm::APSInt *getSymVal(ProgramStateRef State,<br>
+ SymbolRef Sym) const override;<br>
+<br>
+ ProgramStateRef removeDeadBindings(<wbr>ProgramStateRef St,<br>
+ SymbolReaper &SymReaper) override;<br>
+<br>
+ void print(ProgramStateRef St, raw_ostream &Out, const char *nl,<br>
+ const char *sep) override;<br>
+<br>
+ //===-------------------------<wbr>------------------------------<wbr>-----------===//<br>
+ // Implementation for interface from SimpleConstraintManager.<br>
+ //===-------------------------<wbr>------------------------------<wbr>-----------===//<br>
+<br>
+ ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,<br>
+ bool Assumption) override;<br>
+<br>
+ ProgramStateRef assumeSymInclusiveRange(<wbr>ProgramStateRef State, SymbolRef Sym,<br>
+ const llvm::APSInt &From,<br>
+ const llvm::APSInt &To,<br>
+ bool InRange) override;<br>
+<br>
+ ProgramStateRef assumeSymUnsupported(<wbr>ProgramStateRef State, SymbolRef Sym,<br>
+ bool Assumption) override;<br>
+<br>
+private:<br>
+ //===-------------------------<wbr>------------------------------<wbr>-----------===//<br>
+ // Internal implementation.<br>
+ //===-------------------------<wbr>------------------------------<wbr>-----------===//<br>
+<br>
+ // Check whether a new model is satisfiable, and update the program state.<br>
+ ProgramStateRef assumeZ3Expr(ProgramStateRef State, SymbolRef Sym,<br>
+ const Z3Expr &Exp);<br>
+<br>
+ // Generate and check a Z3 model, using the given constraint.<br>
+ Z3_lbool checkZ3Model(ProgramStateRef State, const Z3Expr &Exp) const;<br>
+<br>
+ // Generate a Z3Expr that represents the given symbolic expression.<br>
+ // Sets the hasComparison parameter if the expression has a comparison<br>
+ // operator.<br>
+ // Sets the RetTy parameter to the final return type after promotions and<br>
+ // casts.<br>
+ Z3Expr getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr,<br>
+ bool *hasComparison = nullptr) const;<br>
+<br>
+ // Generate a Z3Expr that takes the logical not of an expression.<br>
+ Z3Expr getZ3NotExpr(const Z3Expr &Exp) const;<br>
+<br>
+ // Generate a Z3Expr that compares the expression to zero.<br>
+ Z3Expr getZ3ZeroExpr(const Z3Expr &Exp, QualType RetTy,<br>
+ bool Assumption) const;<br>
+<br>
+ // Recursive implementation to unpack and generate symbolic expression.<br>
+ // Sets the hasComparison and RetTy parameters. See getZ3Expr().<br>
+ Z3Expr getZ3SymExpr(SymbolRef Sym, QualType *RetTy,<br>
+ bool *hasComparison) const;<br>
+<br>
+ // Wrapper to generate Z3Expr from SymbolData.<br>
+ Z3Expr getZ3DataExpr(const SymbolID ID, QualType Ty) const;<br>
+<br>
+ // Wrapper to generate Z3Expr from SymbolCast.<br>
+ Z3Expr getZ3CastExpr(const Z3Expr &Exp, QualType FromTy, QualType Ty) const;<br>
+<br>
+ // Wrapper to generate Z3Expr from BinarySymExpr.<br>
+ // Sets the hasComparison and RetTy parameters. See getZ3Expr().<br>
+ Z3Expr getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,<br>
+ QualType *RetTy) const;<br>
+<br>
+ // Wrapper to generate Z3Expr from unpacked binary symbolic expression.<br>
+ // Sets the RetTy parameter. See getZ3Expr().<br>
+ Z3Expr getZ3BinExpr(const Z3Expr &LHS, QualType LTy,<br>
+ BinaryOperator::Opcode Op, const Z3Expr &RHS,<br>
+ QualType RTy, QualType *RetTy) const;<br>
+<br>
+ //===-------------------------<wbr>------------------------------<wbr>-----------===//<br>
+ // Helper functions.<br>
+ //===-------------------------<wbr>------------------------------<wbr>-----------===//<br>
+<br>
+ // Recover the QualType of an APSInt.<br>
+ // TODO: Refactor to put elsewhere<br>
+ QualType getAPSIntType(const llvm::APSInt &Int) const;<br>
+<br>
+ // Perform implicit type conversion on binary symbolic expressions.<br>
+ // May modify all input parameters.<br>
+ // TODO: Refactor to use built-in conversion functions<br>
+ void doTypeConversion(Z3Expr &LHS, Z3Expr &RHS, QualType <y,<br>
+ QualType &RTy) const;<br>
+<br>
+ // Perform implicit integer type conversion.<br>
+ // May modify all input parameters.<br>
+ // TODO: Refactor to use Sema::handleIntegerConversion(<wbr>)<br>
+ template <typename T,<br>
+ T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)><br>
+ void doIntTypeConversion(T &LHS, QualType <y, T &RHS, QualType &RTy) const;<br>
+<br>
+ // Perform implicit floating-point type conversion.<br>
+ // May modify all input parameters.<br>
+ // TODO: Refactor to use Sema::handleFloatConversion()<br>
+ template <typename T,<br>
+ T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)><br>
+ void doFloatTypeConversion(T &LHS, QualType <y, T &RHS,<br>
+ QualType &RTy) const;<br>
+<br>
+ // Callback function for doCast parameter on APSInt type.<br>
+ static llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy,<br>
+ uint64_t ToWidth, QualType FromTy,<br>
+ uint64_t FromWidth);<br>
+}; // end class Z3ConstraintManager<br>
+<br>
+Z3_context Z3Context::ZC;<br>
+<br>
+} // end anonymous namespace<br>
+<br>
+ProgramStateRef Z3ConstraintManager::<wbr>assumeSym(ProgramStateRef State,<br>
+ SymbolRef Sym, bool Assumption) {<br>
+ QualType RetTy;<br>
+ bool hasComparison;<br>
+<br>
+ Z3Expr Exp = getZ3Expr(Sym, &RetTy, &hasComparison);<br>
+ // Create zero comparison for implicit boolean cast, with reversed assumption<br>
+ if (!hasComparison && !RetTy->isBooleanType())<br>
+ return assumeZ3Expr(State, Sym, getZ3ZeroExpr(Exp, RetTy, !Assumption));<br>
+<br>
+ return assumeZ3Expr(State, Sym, Assumption ? Exp : getZ3NotExpr(Exp));<br>
+}<br>
+<br>
+ProgramStateRef Z3ConstraintManager::<wbr>assumeSymInclusiveRange(<br>
+ ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,<br>
+ const llvm::APSInt &To, bool InRange) {<br>
+ QualType RetTy;<br>
+ // The expression may be casted, so we cannot call getZ3DataExpr() directly<br>
+ Z3Expr Exp = getZ3Expr(Sym, &RetTy);<br>
+<br>
+ assert((getAPSIntType(From) == getAPSIntType(To)) &&<br>
+ "Range values have different types!");<br>
+ QualType RTy = getAPSIntType(From);<br>
+ bool isSignedTy = RetTy-><wbr>isSignedIntegerOrEnumerationTy<wbr>pe();<br>
+ Z3Expr FromExp = Z3Expr::fromAPSInt(From);<br>
+ Z3Expr ToExp = Z3Expr::fromAPSInt(To);<br>
+<br>
+ // Construct single (in)equality<br>
+ if (From == To)<br>
+ return assumeZ3Expr(State, Sym,<br>
+ getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,<br>
+ FromExp, RTy, nullptr));<br>
+<br>
+ // Construct two (in)equalities, and a logical and/or<br>
+ Z3Expr LHS =<br>
+ getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy, nullptr);<br>
+ Z3Expr RHS =<br>
+ getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy, nullptr);<br>
+ return assumeZ3Expr(<br>
+ State, Sym,<br>
+ Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, isSignedTy));<br>
+}<br>
+<br>
+ProgramStateRef Z3ConstraintManager::<wbr>assumeSymUnsupported(<wbr>ProgramStateRef State,<br>
+ SymbolRef Sym,<br>
+ bool Assumption) {<br>
+ // Skip anything that is unsupported<br>
+ return State;<br>
+}<br>
+<br>
+bool Z3ConstraintManager::<wbr>canReasonAbout(SVal X) const {<br>
+ const TargetInfo &TI = getBasicVals().getContext().<wbr>getTargetInfo();<br>
+<br>
+ Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();<br>
+ if (!SymVal)<br>
+ return true;<br>
+<br>
+ const SymExpr *Sym = SymVal->getSymbol();<br>
+ do {<br>
+ QualType Ty = Sym->getType();<br>
+<br>
+ // Complex types are not modeled<br>
+ if (Ty->isComplexType() || Ty->isComplexIntegerType())<br>
+ return false;<br>
+<br>
+ // Non-IEEE 754 floating-point types are not modeled<br>
+ if ((Ty->isSpecificBuiltinType(<wbr>BuiltinType::LongDouble) &&<br>
+ (&TI.getLongDoubleFormat() == &llvm::APFloat::<wbr>x87DoubleExtended() ||<br>
+ &TI.getLongDoubleFormat() == &llvm::APFloat::<wbr>PPCDoubleDouble())))<br>
+ return false;<br>
+<br>
+ if (isa<SymbolData>(Sym)) {<br>
+ break;<br>
+ } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {<br>
+ Sym = SC->getOperand();<br>
+ } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {<br>
+ if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {<br>
+ Sym = SIE->getLHS();<br>
+ } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {<br>
+ Sym = ISE->getRHS();<br>
+ } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {<br>
+ return canReasonAbout(nonloc::<wbr>SymbolVal(SSM->getLHS())) &&<br>
+ canReasonAbout(nonloc::<wbr>SymbolVal(SSM->getRHS()));<br>
+ } else {<br>
+ llvm_unreachable("Unsupported binary expression to reason about!");<br>
+ }<br>
+ } else {<br>
+ llvm_unreachable("Unsupported expression to reason about!");<br>
+ }<br>
+ } while (Sym);<br>
+<br>
+ return true;<br>
+}<br>
+<br>
+ConditionTruthVal Z3ConstraintManager::<wbr>checkNull(ProgramStateRef State,<br>
+ SymbolRef Sym) {<br>
+ QualType RetTy;<br>
+ // The expression may be casted, so we cannot call getZ3DataExpr() directly<br>
+ Z3Expr VarExp = getZ3Expr(Sym, &RetTy);<br>
+ Z3Expr Exp = getZ3ZeroExpr(VarExp, RetTy, true);<br>
+ // Negate the constraint<br>
+ Z3Expr NotExp = getZ3ZeroExpr(VarExp, RetTy, false);<br>
+<br>
+ Solver.reset();<br>
+ Solver.addStateConstraints(<wbr>State);<br>
+<br>
+ Solver.push();<br>
+ Solver.addConstraint(Exp);<br>
+ Z3_lbool isSat = Solver.check();<br>
+<br>
+ Solver.pop();<br>
+ Solver.addConstraint(NotExp);<br>
+ Z3_lbool isNotSat = Solver.check();<br>
+<br>
+ // Zero is the only possible solution<br>
+ if (isSat == Z3_L_TRUE && isNotSat == Z3_L_FALSE)<br>
+ return true;<br>
+ // Zero is not a solution<br>
+ else if (isSat == Z3_L_FALSE && isNotSat == Z3_L_TRUE)<br>
+ return false;<br>
+<br>
+ // Zero may be a solution<br>
+ return ConditionTruthVal();<br>
+}<br>
+<br>
+const llvm::APSInt *Z3ConstraintManager::<wbr>getSymVal(ProgramStateRef State,<br>
+ SymbolRef Sym) const {<br>
+ BasicValueFactory &BV = getBasicVals();<br>
+ ASTContext &Ctx = BV.getContext();<br>
+<br>
+ if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {<br>
+ QualType Ty = Sym->getType();<br>
+ assert(!Ty-><wbr>isRealFloatingType());<br>
+ llvm::APSInt Value(Ctx.getTypeSize(Ty),<br>
+ !Ty-><wbr>isSignedIntegerOrEnumerationTy<wbr>pe());<br>
+<br>
+ Z3Expr Exp = getZ3DataExpr(SD->getSymbolID(<wbr>), Ty);<br>
+<br>
+ Solver.reset();<br>
+ Solver.addStateConstraints(<wbr>State);<br>
+<br>
+ // Constraints are unsatisfiable<br>
+ if (Solver.check() != Z3_L_TRUE)<br>
+ return nullptr;<br>
+<br>
+ Z3Model Model = Solver.getModel();<br>
+ // Model does not assign interpretation<br>
+ if (!Model.getInterpretation(Exp, Value))<br>
+ return nullptr;<br>
+<br>
+ // A value has been obtained, check if it is the only value<br>
+ Z3Expr NotExp = Z3Expr::fromBinOp(<br>
+ Exp, BO_NE,<br>
+ Ty->isBooleanType() ? Z3Expr::fromBoolean(Value.<wbr>getBoolValue())<br>
+ : Z3Expr::fromAPSInt(Value),<br>
+ false);<br>
+<br>
+ Solver.addConstraint(NotExp);<br>
+ if (Solver.check() == Z3_L_TRUE)<br>
+ return nullptr;<br>
+<br>
+ // This is the only solution, store it<br>
+ return &BV.getValue(Value);<br>
+ } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {<br>
+ SymbolRef CastSym = SC->getOperand();<br>
+ QualType CastTy = SC->getType();<br>
+ // Skip the void type<br>
+ if (CastTy->isVoidType())<br>
+ return nullptr;<br>
+<br>
+ const llvm::APSInt *Value;<br>
+ if (!(Value = getSymVal(State, CastSym)))<br>
+ return nullptr;<br>
+ return &BV.Convert(SC->getType(), *Value);<br>
+ } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {<br>
+ const llvm::APSInt *LHS, *RHS;<br>
+ if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {<br>
+ LHS = getSymVal(State, SIE->getLHS());<br>
+ RHS = &SIE->getRHS();<br>
+ } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {<br>
+ LHS = &ISE->getLHS();<br>
+ RHS = getSymVal(State, ISE->getRHS());<br>
+ } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {<br>
+ // Early termination to avoid expensive call<br>
+ LHS = getSymVal(State, SSM->getLHS());<br>
+ RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;<br>
+ } else {<br>
+ llvm_unreachable("Unsupported binary expression to get symbol value!");<br>
+ }<br>
+<br>
+ if (!LHS || !RHS)<br>
+ return nullptr;<br>
+<br>
+ llvm::APSInt ConvertedLHS = *LHS, ConvertedRHS = *RHS;<br>
+ QualType LTy = getAPSIntType(*LHS), RTy = getAPSIntType(*RHS);<br>
+ doIntTypeConversion<llvm::<wbr>APSInt, Z3ConstraintManager::<wbr>castAPSInt>(<br>
+ ConvertedLHS, LTy, ConvertedRHS, RTy);<br>
+ return BV.evalAPSInt(BSE->getOpcode()<wbr>, ConvertedLHS, ConvertedRHS);<br>
+ }<br>
+<br>
+ llvm_unreachable("Unsupported expression to get symbol value!");<br>
+}<br>
+<br>
+ProgramStateRef<br>
+Z3ConstraintManager::<wbr>removeDeadBindings(<wbr>ProgramStateRef State,<br>
+ SymbolReaper &SymReaper) {<br>
+ ConstraintZ3Ty CZ = State->get<ConstraintZ3>();<br>
+ ConstraintZ3Ty::Factory &CZFactory = State->get_context<<wbr>ConstraintZ3>();<br>
+<br>
+ for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {<br>
+ if (SymReaper.maybeDead(I->first)<wbr>)<br>
+ CZ = CZFactory.remove(CZ, *I);<br>
+ }<br>
+<br>
+ return State->set<ConstraintZ3>(CZ);<br>
+}<br>
+<br>
+//===------------------------<wbr>------------------------------<wbr>------------===//<br>
+// Internal implementation.<br>
+//===------------------------<wbr>------------------------------<wbr>------------===//<br>
+<br>
+ProgramStateRef Z3ConstraintManager::<wbr>assumeZ3Expr(ProgramStateRef State,<br>
+ SymbolRef Sym,<br>
+ const Z3Expr &Exp) {<br>
+ // Check the model, avoid simplifying AST to save time<br>
+ if (checkZ3Model(State, Exp) == Z3_L_TRUE)<br>
+ return State->add<ConstraintZ3>(std::<wbr>make_pair(Sym, Exp));<br>
+<br>
+ return nullptr;<br>
+}<br>
+<br>
+Z3_lbool Z3ConstraintManager::<wbr>checkZ3Model(ProgramStateRef State,<br>
+ const Z3Expr &Exp) const {<br>
+ Solver.reset();<br>
+ Solver.addConstraint(Exp);<br>
+ Solver.addStateConstraints(<wbr>State);<br>
+ return Solver.check();<br>
+}<br>
+<br>
+Z3Expr Z3ConstraintManager::<wbr>getZ3Expr(SymbolRef Sym, QualType *RetTy,<br>
+ bool *hasComparison) const {<br>
+ if (hasComparison) {<br>
+ *hasComparison = false;<br>
+ }<br>
+<br>
+ return getZ3SymExpr(Sym, RetTy, hasComparison);<br>
+}<br>
+<br>
+Z3Expr Z3ConstraintManager::<wbr>getZ3NotExpr(const Z3Expr &Exp) const {<br>
+ return Z3Expr::fromUnOp(UO_LNot, Exp);<br>
+}<br>
+<br>
+Z3Expr Z3ConstraintManager::<wbr>getZ3ZeroExpr(const Z3Expr &Exp, QualType Ty,<br>
+ bool Assumption) const {<br>
+ ASTContext &Ctx = getBasicVals().getContext();<br>
+ if (Ty->isRealFloatingType()) {<br>
+ llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.<wbr>getFloatTypeSemantics(Ty));<br>
+ return Z3Expr::fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE,<br>
+ Z3Expr::fromAPFloat(Zero));<br>
+ } else if (Ty-><wbr>isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||<br>
+ Ty->isBlockPointerType() || Ty->isReferenceType()) {<br>
+ bool isSigned = Ty-><wbr>isSignedIntegerOrEnumerationTy<wbr>pe();<br>
+ // Skip explicit comparison for boolean types<br>
+ if (Ty->isBooleanType())<br>
+ return Assumption ? getZ3NotExpr(Exp) : Exp;<br>
+ return Z3Expr::fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,<br>
+ Z3Expr::fromInt("0", Ctx.getTypeSize(Ty)),<br>
+ isSigned);<br>
+ }<br>
+<br>
+ llvm_unreachable("Unsupported type for zero value!");<br>
+}<br>
+<br>
+Z3Expr Z3ConstraintManager::<wbr>getZ3SymExpr(SymbolRef Sym, QualType *RetTy,<br>
+ bool *hasComparison) const {<br>
+ if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {<br>
+ if (RetTy)<br>
+ *RetTy = Sym->getType();<br>
+<br>
+ return getZ3DataExpr(SD->getSymbolID(<wbr>), Sym->getType());<br>
+ } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {<br>
+ if (RetTy)<br>
+ *RetTy = Sym->getType();<br>
+<br>
+ QualType FromTy;<br>
+ Z3Expr Exp = getZ3SymExpr(SC->getOperand(), &FromTy, hasComparison);<br>
+ // Casting an expression with a comparison invalidates it. Note that this<br>
+ // must occur after the recursive call above.<br>
+ // e.g. (signed char) (x > 0)<br>
+ if (hasComparison)<br>
+ *hasComparison = false;<br>
+ return getZ3CastExpr(Exp, FromTy, Sym->getType());<br>
+ } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {<br>
+ Z3Expr Exp = getZ3SymBinExpr(BSE, hasComparison, RetTy);<br>
+ // Set the hasComparison parameter, in post-order traversal order.<br>
+ if (hasComparison)<br>
+ *hasComparison = BinaryOperator::<wbr>isComparisonOp(BSE->getOpcode(<wbr>));<br>
+ return Exp;<br>
+ }<br>
+<br>
+ llvm_unreachable("Unsupported SymbolRef type!");<br>
+}<br>
+<br>
+Z3Expr Z3ConstraintManager::<wbr>getZ3DataExpr(const SymbolID ID,<br>
+ QualType Ty) const {<br>
+ ASTContext &Ctx = getBasicVals().getContext();<br>
+ return Z3Expr::fromData(ID, Ty->isBooleanType(), Ty->isRealFloatingType(),<br>
+ Ctx.getTypeSize(Ty));<br>
+}<br>
+<br>
+Z3Expr Z3ConstraintManager::<wbr>getZ3CastExpr(const Z3Expr &Exp, QualType FromTy,<br>
+ QualType ToTy) const {<br>
+ ASTContext &Ctx = getBasicVals().getContext();<br>
+ return Z3Expr::fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,<br>
+ Ctx.getTypeSize(FromTy));<br>
+}<br>
+<br>
+Z3Expr Z3ConstraintManager::<wbr>getZ3SymBinExpr(const BinarySymExpr *BSE,<br>
+ bool *hasComparison,<br>
+ QualType *RetTy) const {<br>
+ QualType LTy, RTy;<br>
+ BinaryOperator::Opcode Op = BSE->getOpcode();<br>
+<br>
+ if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {<br>
+ RTy = getAPSIntType(SIE->getRHS());<br>
+ Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), <y, hasComparison);<br>
+ Z3Expr RHS = Z3Expr::fromAPSInt(SIE-><wbr>getRHS());<br>
+ return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);<br>
+ } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {<br>
+ LTy = getAPSIntType(ISE->getLHS());<br>
+ Z3Expr LHS = Z3Expr::fromAPSInt(ISE-><wbr>getLHS());<br>
+ Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);<br>
+ return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);<br>
+ } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {<br>
+ Z3Expr LHS = getZ3SymExpr(SSM->getLHS(), <y, hasComparison);<br>
+ Z3Expr RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison);<br>
+ return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);<br>
+ } else {<br>
+ llvm_unreachable("Unsupported BinarySymExpr type!");<br>
+ }<br>
+}<br>
+<br>
+Z3Expr Z3ConstraintManager::<wbr>getZ3BinExpr(const Z3Expr &LHS, QualType LTy,<br>
+ BinaryOperator::Opcode Op,<br>
+ const Z3Expr &RHS, QualType RTy,<br>
+ QualType *RetTy) const {<br>
+ Z3Expr NewLHS = LHS;<br>
+ Z3Expr NewRHS = RHS;<br>
+ doTypeConversion(NewLHS, NewRHS, LTy, RTy);<br>
+ // Update the return type parameter if the output type has changed.<br>
+ if (RetTy) {<br>
+ // A boolean result can be represented as an integer type in C/C++, but at<br>
+ // this point we only care about the Z3 type. Set it as a boolean type to<br>
+ // avoid subsequent Z3 errors.<br>
+ if (BinaryOperator::<wbr>isComparisonOp(Op) || BinaryOperator::isLogicalOp(<wbr>Op)) {<br>
+ ASTContext &Ctx = getBasicVals().getContext();<br>
+ *RetTy = Ctx.BoolTy;<br>
+ } else {<br>
+ *RetTy = LTy;<br>
+ }<br>
+<br>
+ // If the two operands are pointers and the operation is a subtraction, the<br>
+ // result is of type ptrdiff_t, which is signed<br>
+ if (LTy->isAnyPointerType() && LTy == RTy && Op == BO_Sub) {<br>
+ ASTContext &Ctx = getBasicVals().getContext();<br>
+ *RetTy = Ctx.getIntTypeForBitwidth(Ctx.<wbr>getTypeSize(LTy), true);<br>
+ }<br>
+ }<br>
+<br>
+ return LTy->isRealFloatingType()<br>
+ ? Z3Expr::fromFloatBinOp(NewLHS, Op, NewRHS)<br>
+ : Z3Expr::fromBinOp(NewLHS, Op, NewRHS,<br>
+ LTy-><wbr>isSignedIntegerOrEnumerationTy<wbr>pe());<br>
+}<br>
+<br>
+//===------------------------<wbr>------------------------------<wbr>------------===//<br>
+// Helper functions.<br>
+//===------------------------<wbr>------------------------------<wbr>------------===//<br>
+<br>
+QualType Z3ConstraintManager::<wbr>getAPSIntType(const llvm::APSInt &Int) const {<br>
+ ASTContext &Ctx = getBasicVals().getContext();<br>
+ return Ctx.getIntTypeForBitwidth(Int.<wbr>getBitWidth(), Int.isSigned());<br>
+}<br>
+<br>
+void Z3ConstraintManager::<wbr>doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,<br>
+ QualType <y, QualType &RTy) const {<br>
+ ASTContext &Ctx = getBasicVals().getContext();<br>
+<br>
+ // Perform type conversion<br>
+ if (LTy-><wbr>isIntegralOrEnumerationType() &&<br>
+ RTy-><wbr>isIntegralOrEnumerationType()) {<br>
+ if (LTy->isArithmeticType() && RTy->isArithmeticType())<br>
+ return doIntTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);<br>
+ } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {<br>
+ return doFloatTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);<br>
+ } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||<br>
+ (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||<br>
+ (LTy->isReferenceType() || RTy->isReferenceType())) {<br>
+ // TODO: Refactor to Sema::<wbr>FindCompositePointerType(), and<br>
+ // Sema::CheckCompareOperands().<br>
+<br>
+ uint64_t LBitWidth = Ctx.getTypeSize(LTy);<br>
+ uint64_t RBitWidth = Ctx.getTypeSize(RTy);<br>
+<br>
+ // Cast the non-pointer type to the pointer type.<br>
+ // TODO: Be more strict about this.<br>
+ if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||<br>
+ (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||<br>
+ (LTy->isReferenceType() ^ RTy->isReferenceType())) {<br>
+ if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||<br>
+ LTy->isReferenceType()) {<br>
+ LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);<br>
+ LTy = RTy;<br>
+ } else {<br>
+ RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);<br>
+ RTy = LTy;<br>
+ }<br>
+ }<br>
+<br>
+ // Cast the void pointer type to the non-void pointer type.<br>
+ // For void types, this assumes that the casted value is equal to the value<br>
+ // of the original pointer, and does not account for alignment requirements.<br>
+ if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {<br>
+ assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&<br>
+ "Pointer types have different bitwidths!");<br>
+ if (RTy->isVoidPointerType())<br>
+ RTy = LTy;<br>
+ else<br>
+ LTy = RTy;<br>
+ }<br>
+<br>
+ if (LTy == RTy)<br>
+ return;<br>
+ }<br>
+<br>
+ // Fallback: for the solver, assume that these types don't really matter<br>
+ if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||<br>
+ (LTy->isObjCObjectPointerType(<wbr>) && RTy->isObjCObjectPointerType()<wbr>)) {<br>
+ LTy = RTy;<br>
+ return;<br>
+ }<br>
+<br>
+ // TODO: Refine behavior for invalid type casts<br>
+}<br>
+<br>
+template <typename T,<br>
+ T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)><br>
+void Z3ConstraintManager::<wbr>doIntTypeConversion(T &LHS, QualType <y, T &RHS,<br>
+ QualType &RTy) const {<br>
+ ASTContext &Ctx = getBasicVals().getContext();<br>
+<br>
+ uint64_t LBitWidth = Ctx.getTypeSize(LTy);<br>
+ uint64_t RBitWidth = Ctx.getTypeSize(RTy);<br>
+<br>
+ // Always perform integer promotion before checking type equality.<br>
+ // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion<br>
+ if (LTy->isPromotableIntegerType(<wbr>)) {<br>
+ QualType NewTy = Ctx.getPromotedIntegerType(<wbr>LTy);<br>
+ uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);<br>
+ LHS = (*doCast)(LHS, NewTy, NewBitWidth, LTy, LBitWidth);<br>
+ LTy = NewTy;<br>
+ LBitWidth = NewBitWidth;<br>
+ }<br>
+ if (RTy->isPromotableIntegerType(<wbr>)) {<br>
+ QualType NewTy = Ctx.getPromotedIntegerType(<wbr>RTy);<br>
+ uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);<br>
+ RHS = (*doCast)(RHS, NewTy, NewBitWidth, RTy, RBitWidth);<br>
+ RTy = NewTy;<br>
+ RBitWidth = NewBitWidth;<br>
+ }<br>
+<br>
+ if (LTy == RTy)<br>
+ return;<br>
+<br>
+ // Perform integer type conversion<br>
+ // Note: Safe to skip updating bitwidth because this must terminate<br>
+ bool isLSignedTy = LTy-><wbr>isSignedIntegerOrEnumerationTy<wbr>pe();<br>
+ bool isRSignedTy = RTy-><wbr>isSignedIntegerOrEnumerationTy<wbr>pe();<br>
+<br>
+ int order = Ctx.getIntegerTypeOrder(LTy, RTy);<br>
+ if (isLSignedTy == isRSignedTy) {<br>
+ // Same signedness; use the higher-ranked type<br>
+ if (order == 1) {<br>
+ RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);<br>
+ RTy = LTy;<br>
+ } else {<br>
+ LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);<br>
+ LTy = RTy;<br>
+ }<br>
+ } else if (order != (isLSignedTy ? 1 : -1)) {<br>
+ // The unsigned type has greater than or equal rank to the<br>
+ // signed type, so use the unsigned type<br>
+ if (isRSignedTy) {<br>
+ RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);<br>
+ RTy = LTy;<br>
+ } else {<br>
+ LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);<br>
+ LTy = RTy;<br>
+ }<br>
+ } else if (LBitWidth != RBitWidth) {<br>
+ // The two types are different widths; if we are here, that<br>
+ // means the signed type is larger than the unsigned type, so<br>
+ // use the signed type.<br>
+ if (isLSignedTy) {<br>
+ RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);<br>
+ RTy = LTy;<br>
+ } else {<br>
+ LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);<br>
+ LTy = RTy;<br>
+ }<br>
+ } else {<br>
+ // The signed type is higher-ranked than the unsigned type,<br>
+ // but isn't actually any bigger (like unsigned int and long<br>
+ // on most 32-bit systems). Use the unsigned type corresponding<br>
+ // to the signed type.<br>
+ QualType NewTy = Ctx.<wbr>getCorrespondingUnsignedType(<wbr>isLSignedTy ? LTy : RTy);<br>
+ RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);<br>
+ RTy = NewTy;<br>
+ LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);<br>
+ LTy = NewTy;<br>
+ }<br>
+}<br>
+<br>
+template <typename T,<br>
+ T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)><br>
+void Z3ConstraintManager::<wbr>doFloatTypeConversion(T &LHS, QualType <y, T &RHS,<br>
+ QualType &RTy) const {<br>
+ ASTContext &Ctx = getBasicVals().getContext();<br>
+<br>
+ uint64_t LBitWidth = Ctx.getTypeSize(LTy);<br>
+ uint64_t RBitWidth = Ctx.getTypeSize(RTy);<br>
+<br>
+ // Perform float-point type promotion<br>
+ if (!LTy->isRealFloatingType()) {<br>
+ LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);<br>
+ LTy = RTy;<br>
+ LBitWidth = RBitWidth;<br>
+ }<br>
+ if (!RTy->isRealFloatingType()) {<br>
+ RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);<br>
+ RTy = LTy;<br>
+ RBitWidth = LBitWidth;<br>
+ }<br>
+<br>
+ if (LTy == RTy)<br>
+ return;<br>
+<br>
+ // If we have two real floating types, convert the smaller operand to the<br>
+ // bigger result<br>
+ // Note: Safe to skip updating bitwidth because this must terminate<br>
+ int order = Ctx.getFloatingTypeOrder(LTy, RTy);<br>
+ if (order > 0) {<br>
+ RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);<br>
+ RTy = LTy;<br>
+ } else if (order == 0) {<br>
+ LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);<br>
+ LTy = RTy;<br>
+ } else {<br>
+ llvm_unreachable("Unsupported floating-point type cast!");<br>
+ }<br>
+}<br>
+<br>
+llvm::APSInt Z3ConstraintManager::<wbr>castAPSInt(const llvm::APSInt &V,<br>
+ QualType ToTy, uint64_t ToWidth,<br>
+ QualType FromTy,<br>
+ uint64_t FromWidth) {<br>
+ APSIntType TargetType(ToWidth, !ToTy-><wbr>isSignedIntegerOrEnumerationTy<wbr>pe());<br>
+ return TargetType.convert(V);<br>
+}<br>
+<br>
+//==-------------------------<wbr>------------------------------<wbr>-----------------==/<br>
+// Pretty-printing.<br>
+//==-------------------------<wbr>------------------------------<wbr>-----------------==/<br>
+<br>
+void Z3ConstraintManager::print(<wbr>ProgramStateRef St, raw_ostream &OS,<br>
+ const char *nl, const char *sep) {<br>
+<br>
+ ConstraintZ3Ty CZ = St->get<ConstraintZ3>();<br>
+<br>
+ OS << nl << sep << "Constraints:";<br>
+ for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {<br>
+ OS << nl << ' ' << I->first << " : ";<br>
+ I->second.print(OS);<br>
+ }<br>
+ OS << nl;<br>
+}<br>
+<br>
+#endif<br>
+<br>
+std::unique_ptr<<wbr>ConstraintManager><br>
+ento::<wbr>CreateZ3ConstraintManager(<wbr>ProgramStateManager &StMgr, SubEngine *Eng) {<br>
+#if CLANG_ANALYZER_WITH_Z3<br>
+ return llvm::make_unique<<wbr>Z3ConstraintManager>(Eng, StMgr.getSValBuilder());<br>
+#else<br>
+ llvm::report_fatal_error("<wbr>Clang was not compiled with Z3 support!", false);<br>
+ return nullptr;<br>
+#endif<br>
+}<br>
<br>
Modified: cfe/trunk/test/Analysis/expr-<wbr>inspection.c<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/expr-inspection.c?rev=299463&r1=299462&r2=299463&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-<wbr>project/cfe/trunk/test/<wbr>Analysis/expr-inspection.c?<wbr>rev=299463&r1=299462&r2=<wbr>299463&view=diff</a><br>
==============================<wbr>==============================<wbr>==================<br>
--- cfe/trunk/test/Analysis/expr-<wbr>inspection.c (original)<br>
+++ cfe/trunk/test/Analysis/expr-<wbr>inspection.c Tue Apr 4 14:52:25 2017<br>
@@ -19,4 +19,4 @@ void foo(int x) {<br>
<br>
// CHECK: Expressions:<br>
// CHECK-NEXT: clang_analyzer_printState : &code{clang_analyzer_<wbr>printState}<br>
-// CHECK-NEXT: Ranges are empty.<br>
+// CHECK-NEXT: {{(Ranges are empty.)|(Constraints:[[:space:<wbr>]]*$)}}<br>
<br>
Modified: cfe/trunk/test/Analysis/lit.<wbr>local.cfg<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/lit.local.cfg?rev=299463&r1=299462&r2=299463&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-<wbr>project/cfe/trunk/test/<wbr>Analysis/lit.local.cfg?rev=<wbr>299463&r1=299462&r2=299463&<wbr>view=diff</a><br>
==============================<wbr>==============================<wbr>==================<br>
--- cfe/trunk/test/Analysis/lit.<wbr>local.cfg (original)<br>
+++ cfe/trunk/test/Analysis/lit.<wbr>local.cfg Tue Apr 4 14:52:25 2017<br>
@@ -10,6 +10,10 @@ class AnalyzerTest(lit.formats.<wbr>ShTest, o<br>
if result.code == lit.Test.FAIL:<br>
return result<br>
<br>
+ # If z3 backend available, add an additional run line for it<br>
+ if test.config.clang_<wbr>staticanalyzer_z3 == '1':<br>
+ result = self.<wbr>executeWithAnalyzeSubstitution<wbr>(test, litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3')<br>
+<br>
return result<br>
<br>
def executeWithAnalyzeSubstitution<wbr>(self, test, litConfig, substitution):<br>
<br>
Added: cfe/trunk/test/Analysis/<wbr>unsupported-types.c<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/unsupported-types.c?rev=299463&view=auto" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-<wbr>project/cfe/trunk/test/<wbr>Analysis/unsupported-types.c?<wbr>rev=299463&view=auto</a><br>
==============================<wbr>==============================<wbr>==================<br>
--- cfe/trunk/test/Analysis/<wbr>unsupported-types.c (added)<br>
+++ cfe/trunk/test/Analysis/<wbr>unsupported-types.c Tue Apr 4 14:52:25 2017<br>
@@ -0,0 +1,31 @@<br>
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.<wbr>ExprInspection -verify %s<br>
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.<wbr>ExprInspection -triple x86_64-unknown-linux -verify %s<br>
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.<wbr>ExprInspection -triple powerpc64-linux-gnu -verify %s<br>
+<br>
+#define _Complex_I (__extension__ 1.0iF)<br>
+<br>
+void clang_analyzer_eval(int);<br>
+<br>
+void complex_float(double _Complex x, double _Complex y) {<br>
+ clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}<br>
+ if (x != 1.0 + 3.0 * _Complex_I && y != 1.0 - 4.0 * _Complex_I)<br>
+ return<br>
+ clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}<br>
+ clang_analyzer_eval(x + y == 2.0 - 1.0 * _Complex_I); // expected-warning{{UNKNOWN}}<br>
+}<br>
+<br>
+void complex_int(int _Complex x, int _Complex y) {<br>
+ clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}<br>
+ if (x != 1.0 + 3.0 * _Complex_I && y != 1.0 - 4.0 * _Complex_I)<br>
+ return<br>
+ clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}<br>
+ clang_analyzer_eval(x + y == 2.0 - 1.0 * _Complex_I); // expected-warning{{UNKNOWN}}<br>
+}<br>
+<br>
+void longdouble_float(long double x, long double y) {<br>
+ clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}<br>
+ if (x != 0.0L && y != 1.0L)<br>
+ return<br>
+ clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}<br>
+ clang_analyzer_eval(x + y == 1.0L); // expected-warning{{UNKNOWN}}<br>
+}<br>
<br>
Modified: cfe/trunk/test/lit.cfg<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/test/lit.cfg?rev=299463&r1=299462&r2=299463&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-<wbr>project/cfe/trunk/test/lit.<wbr>cfg?rev=299463&r1=299462&r2=<wbr>299463&view=diff</a><br>
==============================<wbr>==============================<wbr>==================<br>
--- cfe/trunk/test/lit.cfg (original)<br>
+++ cfe/trunk/test/lit.cfg Tue Apr 4 14:52:25 2017<br>
@@ -361,6 +361,9 @@ if config.clang_default_cxx_<wbr>stdlib != ''<br>
if config.clang_staticanalyzer:<br>
config.available_features.add(<wbr>"staticanalyzer")<br>
<br>
+ if config.clang_staticanalyzer_z3 == '1':<br>
+ config.available_features.add(<wbr>"z3")<br>
+<br>
# As of 2011.08, crash-recovery tests still do not pass on FreeBSD.<br>
if platform.system() not in ['FreeBSD']:<br>
config.available_features.add(<wbr>'crash-recovery')<br>
<br>
Modified: cfe/trunk/test/<a href="http://lit.site.cfg.in" rel="noreferrer" target="_blank">lit.site.cfg.in</a><br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/test/lit.site.cfg.in?rev=299463&r1=299462&r2=299463&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-<wbr>project/cfe/trunk/test/lit.<wbr>site.cfg.in?rev=299463&r1=<wbr>299462&r2=299463&view=diff</a><br>
==============================<wbr>==============================<wbr>==================<br>
--- cfe/trunk/test/<a href="http://lit.site.cfg.in" rel="noreferrer" target="_blank">lit.site.cfg.in</a> (original)<br>
+++ cfe/trunk/test/<a href="http://lit.site.cfg.in" rel="noreferrer" target="_blank">lit.site.cfg.in</a> Tue Apr 4 14:52:25 2017<br>
@@ -18,6 +18,7 @@ config.have_zlib = @HAVE_LIBZ@<br>
config.clang_arcmt = @CLANG_ENABLE_ARCMT@<br>
config.clang_default_cxx_<wbr>stdlib = "@CLANG_DEFAULT_CXX_STDLIB@"<br>
config.clang_staticanalyzer = @CLANG_ENABLE_STATIC_ANALYZER@<br>
+config.clang_staticanalyzer_<wbr>z3 = "@CLANG_ANALYZER_WITH_Z3@"<br>
config.clang_examples = @CLANG_BUILD_EXAMPLES@<br>
config.enable_shared = @ENABLE_SHARED@<br>
config.enable_backtrace = @ENABLE_BACKTRACES@<br>
<br>
<br>
______________________________<wbr>_________________<br>
cfe-commits mailing list<br>
<a href="mailto:cfe-commits@lists.llvm.org">cfe-commits@lists.llvm.org</a><br>
<a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits" rel="noreferrer" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/cfe-commits</a><br>
</blockquote></div><br></div>