Hello community, here is the log from the commit of package klee for openSUSE:Factory checked in at 2017-11-27 22:17:05 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/klee (Old) and /work/SRC/openSUSE:Factory/.klee.new (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "klee" Mon Nov 27 22:17:05 2017 rev:6 rq:545450 version:1.4.0+20171026 Changes: -------- --- /work/SRC/openSUSE:Factory/klee/klee.changes 2017-10-23 16:44:10.910265688 +0200 +++ /work/SRC/openSUSE:Factory/.klee.new/klee.changes 2017-11-27 22:17:07.501435544 +0100 @@ -1,0 +2,29 @@ +Fri Nov 17 17:01:38 UTC 2017 - [email protected] + +- Update to version 1.4.0+20171026: + * [cmake]Fix detection of non-standard path for tcmalloc + * fixing huge allocation size constant to be unsigned + * [travis] build metaSMT with C++11 + * [travis] add a workaround to keep Travis alive when running tests for metaSMT-CVC4 (which needs around 10m for one specific test case) + * [travis] update scripts to additionally test CVC4 and Yices2 + * [cmake] detect available metaSMT backends using a pre-defined flag and raise compile flags accordingly + * add support for CVC4 and Yices2 via metaSMT + * Fixed assert in BFSSearcher that does not hold as part of interleaved searcher + * Removed unnecessary and redundant variable +- removed + * 0001-errno-define-__errno_location.patch + * 0001-test-DirSeek-make-it-XFAIL-temporarily.patch +- added + * 0001-Fix-generation-of-expressions-from-constant-sequenti.patch + * 0002-Fix-getelementptr-for-array-or-vector-indices.patch + * 0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch + * 0004-Provide-errno-independent-of-CTYPE_EXTERNALS-being-d.patch + * 0005-Track-errno-correctly.patch + * 0006-Declare-klee_get_errno-and-remove-local-declarations.patch + * 0007-Add-support-for-modelling-errno_location.patch + * 0008-Cleanup-test-cases.patch + * 0009-test-fix-Feature-BFSSearcherAndDFSSearcherInterleave.patch + * 0012-llvm40-gep_type_iterator-has-no-operator.patch + * 0013-llvm38-test-change-some-tests.patch + +------------------------------------------------------------------- Old: ---- 0001-errno-define-__errno_location.patch 0001-test-DirSeek-make-it-XFAIL-temporarily.patch klee-1.4.0+20171009.tar.xz New: ---- 0001-Fix-generation-of-expressions-from-constant-sequenti.patch 0002-Fix-getelementptr-for-array-or-vector-indices.patch 0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch 0004-Provide-errno-independent-of-CTYPE_EXTERNALS-being-d.patch 0005-Track-errno-correctly.patch 0006-Declare-klee_get_errno-and-remove-local-declarations.patch 0007-Add-support-for-modelling-errno_location.patch 0008-Cleanup-test-cases.patch 0009-test-fix-Feature-BFSSearcherAndDFSSearcherInterleave.patch 0012-llvm40-gep_type_iterator-has-no-operator.patch 0013-llvm38-test-change-some-tests.patch klee-1.4.0+20171026.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ klee.spec ++++++ --- /var/tmp/diff_new_pack.lUapFu/_old 2017-11-27 22:17:08.685392570 +0100 +++ /var/tmp/diff_new_pack.lUapFu/_new 2017-11-27 22:17:08.689392425 +0100 @@ -19,7 +19,7 @@ %define llvm_version_minor 0 %define llvm_version %{llvm_version_major} -%define version_unconverted 1.4.0+20171009 +%define version_unconverted 1.4.0+20171026 %ifarch %{ix86} x86_64 %define with_uclibc 1 @@ -31,26 +31,36 @@ Summary: LLVM Execution Engine License: NCSA Group: Development/Languages/Other -Version: 1.4.0+20171009 +Version: 1.4.0+20171026 Release: 0 Url: http://klee.github.io/ Source0: %{name}-%{version}.tar.xz Source1: %{name}-rpmlintrc Source2: https://raw.githubusercontent.com/llvm-mirror/llvm/release_%{llvm_version_major}%{llvm_version_minor}/utils/not/not.cpp Source3: https://raw.githubusercontent.com/llvm-mirror/llvm/release_%{llvm_version_major}%{llvm_version_minor}/utils/FileCheck/FileCheck.cpp -Patch0: 0001-errno-define-__errno_location.patch -Patch1: 0001-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch -Patch2: 0002-llvm-make-KLEE-compile-against-LLVM-3.7.patch -Patch3: 0003-test-add-versions-of-some-tests-for-LLVM-3.7.patch -Patch4: 0004-llvm37-handle-getRegisteredOptions.patch -Patch5: 0005-llvm-make-KLEE-compile-against-LLVM-3.8.patch -Patch6: 0006-llvm-make-KLEE-compile-against-LLVM-3.9.patch -Patch7: 0007-llvm40-handle-different-header-names.patch -Patch8: 0008-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch -Patch9: 0009-llvm40-errorOr-and-similar.patch -Patch10: 0010-llvm-use-chrono-helpers-from-LLVM-4.0.patch -Patch11: 0011-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch -Patch14: 0001-test-DirSeek-make-it-XFAIL-temporarily.patch +Patch1: 0001-Fix-generation-of-expressions-from-constant-sequenti.patch +Patch2: 0002-Fix-getelementptr-for-array-or-vector-indices.patch +Patch3: 0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch +Patch4: 0004-Provide-errno-independent-of-CTYPE_EXTERNALS-being-d.patch +Patch5: 0005-Track-errno-correctly.patch +Patch6: 0006-Declare-klee_get_errno-and-remove-local-declarations.patch +Patch7: 0007-Add-support-for-modelling-errno_location.patch +Patch8: 0008-Cleanup-test-cases.patch +Patch9: 0009-test-fix-Feature-BFSSearcherAndDFSSearcherInterleave.patch +#--- +Patch10: 0001-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch +Patch11: 0002-llvm-make-KLEE-compile-against-LLVM-3.7.patch +Patch12: 0003-test-add-versions-of-some-tests-for-LLVM-3.7.patch +Patch13: 0004-llvm37-handle-getRegisteredOptions.patch +Patch14: 0005-llvm-make-KLEE-compile-against-LLVM-3.8.patch +Patch15: 0006-llvm-make-KLEE-compile-against-LLVM-3.9.patch +Patch16: 0007-llvm40-handle-different-header-names.patch +Patch17: 0008-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch +Patch18: 0009-llvm40-errorOr-and-similar.patch +Patch19: 0010-llvm-use-chrono-helpers-from-LLVM-4.0.patch +Patch20: 0011-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch +Patch21: 0012-llvm40-gep_type_iterator-has-no-operator.patch +Patch22: 0013-llvm38-test-change-some-tests.patch BuildRequires: clang%{llvm_version} BuildRequires: cmake @@ -76,7 +86,6 @@ %prep %setup -q -%patch0 -p1 %patch1 -p1 %patch2 -p1 %patch3 -p1 @@ -88,7 +97,17 @@ %patch9 -p1 %patch10 -p1 %patch11 -p1 +%patch12 -p1 +%patch13 -p1 %patch14 -p1 +%patch15 -p1 +%patch16 -p1 +%patch17 -p1 +%patch18 -p1 +%patch19 -p1 +%patch20 -p1 +%patch21 -p1 +%patch22 -p1 mkdir -p build/test/ cp %{SOURCE2} build/test/ cp %{SOURCE3} build/test/ ++++++ 0001-Fix-generation-of-expressions-from-constant-sequenti.patch ++++++ From: Martin Nowack <[email protected]> Date: Sun, 29 Oct 2017 22:02:32 +0100 Subject: Fix generation of expressions from constant sequential data Patch-mainline: no Signed-off-by: Jiri Slaby <[email protected]> --- lib/Core/ExecutorUtil.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 53f4c5b85754..4f51ecb6301b 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -58,9 +58,11 @@ namespace klee { return ConstantExpr::create(0, getWidthForLLVMType(c->getType())); } else if (const ConstantDataSequential *cds = dyn_cast<ConstantDataSequential>(c)) { + // Handle a vector or array: first element has the smallest address, + // the last element the highest std::vector<ref<Expr> > kids; - for (unsigned i = 0, e = cds->getNumElements(); i != e; ++i) { - ref<Expr> kid = evalConstant(cds->getElementAsConstant(i), ki); + for (unsigned i = cds->getNumElements(); i != 0; --i) { + ref<Expr> kid = evalConstant(cds->getElementAsConstant(i - 1), ki); kids.push_back(kid); } ref<Expr> res = ConcatExpr::createN(kids.size(), kids.data()); -- 2.15.0 ++++++ 0001-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch ++++++ --- /var/tmp/diff_new_pack.lUapFu/_old 2017-11-27 22:17:08.721391264 +0100 +++ /var/tmp/diff_new_pack.lUapFu/_new 2017-11-27 22:17:08.721391264 +0100 @@ -32,10 +32,10 @@ # define KLEE_LLVM_CL_VAL_END #else diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp -index 6c54d34b82bb..7d0707ddfab2 100644 +index 28546915b539..3558049d87cc 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp -@@ -319,6 +319,7 @@ Function *ExternalDispatcherImpl::createDispatcher(Function *target, +@@ -324,6 +324,7 @@ Function *ExternalDispatcherImpl::createDispatcher(Function *target, Type *argTy = (i < FTy->getNumParams() ? FTy->getParamType(i) : (*ai)->getType()); Instruction *argI64p = GetElementPtrInst::Create( @@ -68,5 +68,5 @@ } ii->removeFromParent(); -- -2.14.2 +2.15.0 ++++++ 0002-Fix-getelementptr-for-array-or-vector-indices.patch ++++++ From: Martin Nowack <[email protected]> Date: Sun, 29 Oct 2017 22:06:16 +0100 Subject: Fix getelementptr for array or vector indices Patch-mainline: no Rewrote code based on: llvm::GEPOperator::accumulateConstantOffset(): Handle signed offset correctly. Signed-off-by: Jiri Slaby <[email protected]> --- lib/Core/ExecutorUtil.cpp | 51 ++++++++++++++++++++++++----------------------- 1 file changed, 26 insertions(+), 25 deletions(-) diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 4f51ecb6301b..92dee5ac3906 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -19,18 +19,22 @@ #include "klee/Internal/Module/KModule.h" #include "klee/Internal/Support/ErrorHandling.h" -#include "klee/util/GetElementPtrTypeIterator.h" -#include "llvm/IR/Function.h" #include "llvm/IR/Constants.h" +#include "llvm/IR/DataLayout.h" +#include "llvm/IR/Function.h" #include "llvm/IR/Instructions.h" #include "llvm/IR/Module.h" -#include "llvm/IR/DataLayout.h" +#include "llvm/IR/Operator.h" +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 5) +#include "llvm/Support/GetElementPtrTypeIterator.h" +#else +#include "llvm/IR/GetElementPtrTypeIterator.h" +#endif #include "llvm/Support/raw_ostream.h" #include <cassert> -using namespace klee; using namespace llvm; namespace klee { @@ -188,34 +192,31 @@ namespace klee { case Instruction::GetElementPtr: { ref<ConstantExpr> base = op1->ZExt(Context::get().getPointerWidth()); - for (gep_type_iterator ii = gep_type_begin(ce), ie = gep_type_end(ce); ii != ie; ++ii) { - ref<ConstantExpr> addend = - ConstantExpr::alloc(0, Context::get().getPointerWidth()); - - if (StructType *st = dyn_cast<StructType>(*ii)) { - const StructLayout *sl = kmodule->targetData->getStructLayout(st); - const ConstantInt *ci = cast<ConstantInt>(ii.getOperand()); - - addend = ConstantExpr::alloc(sl->getElementOffset((unsigned) - ci->getZExtValue()), - Context::get().getPointerWidth()); - } else { - const SequentialType *set = cast<SequentialType>(*ii); - ref<ConstantExpr> index = + ref<ConstantExpr> indexOp = evalConstant(cast<Constant>(ii.getOperand()), ki); - unsigned elementSize = - kmodule->targetData->getTypeStoreSize(set->getElementType()); + if (indexOp->isZero()) + continue; - index = index->ZExt(Context::get().getPointerWidth()); - addend = index->Mul(ConstantExpr::alloc(elementSize, - Context::get().getPointerWidth())); + // Handle a struct index, which adds its field offset to the pointer. + if (StructType *STy = dyn_cast<StructType>(*ii)) { + unsigned ElementIdx = indexOp->getZExtValue(); + const StructLayout *SL = kmodule->targetData->getStructLayout(STy); + base = base->Add( + ConstantExpr::alloc(APInt(Context::get().getPointerWidth(), + SL->getElementOffset(ElementIdx)))); + continue; } - base = base->Add(addend); + // For array or vector indices, scale the index by the size of the type. + // Indices can be negative + base = base->Add(indexOp->SExt(Context::get().getPointerWidth()) + ->Mul(ConstantExpr::alloc( + APInt(Context::get().getPointerWidth(), + kmodule->targetData->getTypeAllocSize( + ii.getIndexedType()))))); } - return base; } -- 2.15.0 ++++++ 0002-llvm-make-KLEE-compile-against-LLVM-3.7.patch ++++++ --- /var/tmp/diff_new_pack.lUapFu/_old 2017-11-27 22:17:08.753390102 +0100 +++ /var/tmp/diff_new_pack.lUapFu/_new 2017-11-27 22:17:08.753390102 +0100 @@ -161,7 +161,7 @@ TLI = TM->getSubtargetImpl()->getTargetLowering(); #else diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp -index f1def38c90e5..5d1d0c22495c 100644 +index 4a820578bf16..f8706f9f74e5 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -35,6 +35,7 @@ @@ -173,5 +173,5 @@ #include "llvm/Support/TargetSelect.h" -- -2.14.2 +2.15.0 ++++++ 0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch ++++++ From: Martin Nowack <[email protected]> Date: Sun, 29 Oct 2017 22:12:30 +0100 Subject: Fix correct element order of InsertElement/ExtractElement Patch-mainline: no Signed-off-by: Jiri Slaby <[email protected]> --- lib/Core/Executor.cpp | 21 ++++++--------------- 1 file changed, 6 insertions(+), 15 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 0b7aa1a97f68..dcb8d30e0ffa 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2392,15 +2392,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { const unsigned elementCount = vt->getNumElements(); llvm::SmallVector<ref<Expr>, 8> elems; elems.reserve(elementCount); - for (unsigned i = 0; i < elementCount; ++i) { - // evalConstant() will use ConcatExpr to build vectors with the - // zero-th element leftmost (most significant bits), followed - // by the next element (second leftmost) and so on. This means - // that we have to adjust the index so we read left to right - // rather than right to left. - unsigned bitOffset = EltBits * (elementCount - i - 1); - elems.push_back(i == iIdx ? newElt - : ExtractExpr::create(vec, bitOffset, EltBits)); + for (unsigned i = elementCount; i != 0; --i) { + auto of = i - 1; + unsigned bitOffset = EltBits * of; + elems.push_back( + of == iIdx ? newElt : ExtractExpr::create(vec, bitOffset, EltBits)); } ref<Expr> Result = ConcatExpr::createN(elementCount, elems.data()); @@ -2430,12 +2426,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { return; } - // evalConstant() will use ConcatExpr to build vectors with the - // zero-th element left most (most significant bits), followed - // by the next element (second left most) and so on. This means - // that we have to adjust the index so we read left to right - // rather than right to left. - unsigned bitOffset = EltBits*(vt->getNumElements() - iIdx -1); + unsigned bitOffset = EltBits * iIdx; ref<Expr> Result = ExtractExpr::create(vec, bitOffset, EltBits); bindLocal(ki, state, Result); break; -- 2.15.0 ++++++ 0003-test-add-versions-of-some-tests-for-LLVM-3.7.patch ++++++ --- /var/tmp/diff_new_pack.lUapFu/_old 2017-11-27 22:17:08.769389521 +0100 +++ /var/tmp/diff_new_pack.lUapFu/_new 2017-11-27 22:17:08.777389231 +0100 @@ -1615,5 +1615,5 @@ + return 0; +} -- -2.14.2 +2.15.0 ++++++ 0004-Provide-errno-independent-of-CTYPE_EXTERNALS-being-d.patch ++++++ From: Martin Nowack <[email protected]> Date: Tue, 25 Jul 2017 18:04:06 +0200 Subject: Provide errno independent of CTYPE_EXTERNALS being defined Patch-mainline: no Add support for `errno()` for Darwin as well. Signed-off-by: Jiri Slaby <[email protected]> --- lib/Core/Executor.cpp | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index dcb8d30e0ffa..dd3af9836187 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -524,14 +524,20 @@ void Executor::initializeGlobals(ExecutionState &state) { globalAddresses.insert(std::make_pair(f, addr)); } - // Disabled, we don't want to promote use of live externals. -#ifdef HAVE_CTYPE_EXTERNALS #ifndef WINDOWS -#ifndef DARWIN +#ifndef __APPLE__ /* From /usr/include/errno.h: it [errno] is a per-thread variable. */ int *errno_addr = __errno_location(); +#else + int *errno_addr = __error(); +#endif addExternalObject(state, (void *)errno_addr, sizeof *errno_addr, false); +#endif + // Disabled, we don't want to promote use of live externals. +#ifdef HAVE_CTYPE_EXTERNALS +#ifndef WINDOWS +#ifndef DARWIN /* from /usr/include/ctype.h: These point into arrays of 384, so they can be indexed by any `unsigned char' value [0,255]; by EOF (-1); or by any `signed char' value -- 2.15.0 ++++++ 0004-llvm37-handle-getRegisteredOptions.patch ++++++ --- /var/tmp/diff_new_pack.lUapFu/_old 2017-11-27 22:17:08.797388505 +0100 +++ /var/tmp/diff_new_pack.lUapFu/_new 2017-11-27 22:17:08.801388360 +0100 @@ -12,7 +12,7 @@ 1 file changed, 4 insertions(+) diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp -index bffd3a4f7c00..ce09edde90ea 100644 +index aaba72f4b5b7..3c117db9fa7b 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -86,8 +86,12 @@ UseAssignmentValidatingSolver("debug-assignment-validating-solver", @@ -20,7 +20,7 @@ void KCommandLine::HideUnrelatedOptions(cl::OptionCategory &Category) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7) -+ StringMap<cl::Option*> &map = cl::getRegisteredOptions(); ++ StringMap<cl::Option *> &map = cl::getRegisteredOptions(); +#else StringMap<cl::Option *> map; cl::getRegisteredOptions(map); @@ -29,5 +29,5 @@ i++) { if (i->second->Category != &Category) { -- -2.14.2 +2.15.0 ++++++ 0005-Track-errno-correctly.patch ++++++ From: Martin Nowack <[email protected]> Date: Tue, 25 Jul 2017 22:38:41 +0200 Subject: Track errno correctly Patch-mainline: no Reduce the time of reading the value of errno and using it and writing it to the state space. Signed-off-by: Jiri Slaby <[email protected]> --- lib/Core/Executor.cpp | 26 +++++++++++++++++++++++++- lib/Core/ExternalDispatcher.cpp | 11 ++++++++++- lib/Core/ExternalDispatcher.h | 2 ++ lib/Core/Memory.h | 3 +++ 4 files changed, 40 insertions(+), 2 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index dd3af9836187..3492cd7e9b3c 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -531,7 +531,10 @@ void Executor::initializeGlobals(ExecutionState &state) { #else int *errno_addr = __error(); #endif - addExternalObject(state, (void *)errno_addr, sizeof *errno_addr, false); + MemoryObject *errnoObj = + addExternalObject(state, (void *)errno_addr, sizeof *errno_addr, false); + // Copy values from and to program space explicitly + errnoObj->isUserSpecified = true; #endif // Disabled, we don't want to promote use of live externals. @@ -2973,6 +2976,27 @@ void Executor::callExternalFunction(ExecutionState &state, return; } +#ifndef WINDOWS +#ifndef __APPLE__ + /* From /usr/include/errno.h: it [errno] is a per-thread variable. */ + int *errno_addr = __errno_location(); +#else + int *errno_addr = __error(); +#endif + // Update errno value explicitly + ObjectPair result; + bool resolved = state.addressSpace.resolveOne( + ConstantExpr::create((uint64_t)errno_addr, Expr::Int64), result); + if (!resolved) + klee_error("Could not resolve memory object for errno"); + int error = externalDispatcher->getLastErrno(); + if (memcmp(result.second->concreteStore, &error, result.first->size) != 0) { + ObjectState *wos = + state.addressSpace.getWriteable(result.first, result.second); + memcpy(wos->concreteStore, &error, result.first->size); + } +#endif + Type *resultType = target->inst->getType(); if (resultType != Type::getVoidTy(function->getContext())) { ref<Expr> e = ConstantExpr::fromMemory((void*) args, diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index 6c54d34b82bb..28546915b539 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -65,6 +65,7 @@ private: llvm::Module *singleDispatchModule; std::vector<std::string> moduleIDs; std::string &getFreshModuleID(); + int lastErrno; public: ExternalDispatcherImpl(llvm::LLVMContext &ctx); @@ -72,6 +73,7 @@ public: bool executeCall(llvm::Function *function, llvm::Instruction *i, uint64_t *args); void *resolveSymbol(const std::string &name); + int getLastErrno(); }; std::string &ExternalDispatcherImpl::getFreshModuleID() { @@ -114,7 +116,8 @@ void *ExternalDispatcherImpl::resolveSymbol(const std::string &name) { return addr; } -ExternalDispatcherImpl::ExternalDispatcherImpl(LLVMContext &ctx) : ctx(ctx) { +ExternalDispatcherImpl::ExternalDispatcherImpl(LLVMContext &ctx) + : ctx(ctx), lastErrno(0) { std::string error; singleDispatchModule = new Module(getFreshModuleID(), ctx); #if LLVM_VERSION_CODE < LLVM_VERSION(3, 6) @@ -253,6 +256,8 @@ bool ExternalDispatcherImpl::runProtectedCall(Function *f, uint64_t *args) { res = false; } else { executionEngine->runFunction(f, gvArgs); + // Explicitly acquire errno information + lastErrno = errno; res = true; } @@ -346,6 +351,8 @@ Function *ExternalDispatcherImpl::createDispatcher(Function *target, return dispatcher; } +int ExternalDispatcherImpl::getLastErrno() { return lastErrno; } + ExternalDispatcher::ExternalDispatcher(llvm::LLVMContext &ctx) : impl(new ExternalDispatcherImpl(ctx)) {} @@ -359,4 +366,6 @@ bool ExternalDispatcher::executeCall(llvm::Function *function, void *ExternalDispatcher::resolveSymbol(const std::string &name) { return impl->resolveSymbol(name); } + +int ExternalDispatcher::getLastErrno() { return impl->getLastErrno(); } } diff --git a/lib/Core/ExternalDispatcher.h b/lib/Core/ExternalDispatcher.h index c64dc7d81b93..e407355d6692 100644 --- a/lib/Core/ExternalDispatcher.h +++ b/lib/Core/ExternalDispatcher.h @@ -40,6 +40,8 @@ public: bool executeCall(llvm::Function *function, llvm::Instruction *i, uint64_t *args); void *resolveSymbol(const std::string &name); + + int getLastErrno(); }; } diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index 4e5c87346917..afb41390d071 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -153,7 +153,10 @@ private: const MemoryObject *object; +public: uint8_t *concreteStore; + +private: // XXX cleanup name of flushMask (its backwards or something) BitArray *concreteMask; -- 2.15.0 ++++++ 0005-llvm-make-KLEE-compile-against-LLVM-3.8.patch ++++++ --- /var/tmp/diff_new_pack.lUapFu/_old 2017-11-27 22:17:08.817387779 +0100 +++ /var/tmp/diff_new_pack.lUapFu/_new 2017-11-27 22:17:08.817387779 +0100 @@ -15,10 +15,10 @@ 7 files changed, 77 insertions(+), 9 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp -index 673476f61042..cb8862813133 100644 +index 3492cd7e9b3c..51531f8f46c8 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp -@@ -2127,8 +2127,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { +@@ -2136,8 +2136,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FRem operation"); llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); @@ -248,7 +248,7 @@ addPass(Passes, createLICMPass()); // Hoist loop invariants addPass(Passes, createGVNPass()); // Remove redundancies diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp -index 5d1d0c22495c..c48570799a7f 100644 +index f8706f9f74e5..dbc166ed158a 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -291,7 +291,12 @@ KleeHandler::KleeHandler(int argc, char **argv) @@ -266,5 +266,5 @@ // create directory and try to link klee-last if (mkdir(d.c_str(), 0775) == 0) { -- -2.14.2 +2.15.0 ++++++ 0006-Declare-klee_get_errno-and-remove-local-declarations.patch ++++++ From: Martin Nowack <[email protected]> Date: Thu, 12 Oct 2017 17:58:00 +0200 Subject: Declare klee_get_errno and remove local declarations Patch-mainline: no Signed-off-by: Jiri Slaby <[email protected]> --- include/klee/klee.h | 2 ++ runtime/POSIX/fd.c | 6 ------ 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/include/klee/klee.h b/include/klee/klee.h index bd3100b5007e..282670eebc91 100644 --- a/include/klee/klee.h +++ b/include/klee/klee.h @@ -152,6 +152,8 @@ extern "C" { /* Print range for given argument and tagged with name */ void klee_print_range(const char * name, int arg ); + /* Get errno value of the current state */ + int klee_get_errno(void); #ifdef __cplusplus } #endif diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c index 6f78c7475000..cf07d1380ef8 100644 --- a/runtime/POSIX/fd.c +++ b/runtime/POSIX/fd.c @@ -29,12 +29,6 @@ #include <sys/select.h> #include <klee/klee.h> -/* #define DEBUG */ - -void klee_warning(const char*); -void klee_warning_once(const char*); -int klee_get_errno(void); - /* Returns pointer to the symbolic file structure fs the pathname is symbolic */ static exe_disk_file_t *__get_sym_file(const char *pathname) { if (!pathname) -- 2.15.0 ++++++ 0006-llvm-make-KLEE-compile-against-LLVM-3.9.patch ++++++ --- /var/tmp/diff_new_pack.lUapFu/_old 2017-11-27 22:17:08.849386617 +0100 +++ /var/tmp/diff_new_pack.lUapFu/_new 2017-11-27 22:17:08.849386617 +0100 @@ -7,18 +7,18 @@ --- lib/Core/Executor.cpp | 16 ++++++++++++++++ lib/Core/MemoryManager.cpp | 5 ++++- - lib/Module/ModuleUtil.cpp | 33 ++++++++++++++++++++++++++++++--- + lib/Module/ModuleUtil.cpp | 36 +++++++++++++++++++++++++++++++++--- lib/Module/Optimize.cpp | 28 ++++++++++++++++++++++++++++ lib/Module/RaiseAsm.cpp | 10 +++++++++- tools/kleaver/main.cpp | 4 ++++ tools/klee/main.cpp | 4 ++++ - 7 files changed, 95 insertions(+), 5 deletions(-) + 7 files changed, 98 insertions(+), 5 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp -index cb8862813133..aee0974c7792 100644 +index 51531f8f46c8..cd36eeec13e1 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp -@@ -1299,10 +1299,18 @@ void Executor::executeCall(ExecutionState &state, +@@ -1308,10 +1308,18 @@ void Executor::executeCall(ExecutionState &state, // // Alignment requirements for scalar types is the same as their size if (argWidth > Expr::Int64) { @@ -37,7 +37,7 @@ } } -@@ -1335,10 +1343,18 @@ void Executor::executeCall(ExecutionState &state, +@@ -1344,10 +1352,18 @@ void Executor::executeCall(ExecutionState &state, Expr::Width argWidth = arguments[i]->getWidth(); if (argWidth > Expr::Int64) { @@ -75,7 +75,7 @@ // Handle the case of 0-sized allocations as 1-byte allocations. // This way, we make sure we have this allocation between its own red zones diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp -index e6d592b135b6..8acada93c2cd 100644 +index e6d592b135b6..ee4af254dae2 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -196,7 +196,11 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er @@ -91,7 +91,7 @@ for (object::Archive::child_iterator AI = archive->child_begin(), AE = archive->child_end(); AI != AE; ++AI) #else -@@ -236,7 +240,14 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er +@@ -236,7 +240,17 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er return false; } @@ -100,14 +100,17 @@ + Expected<std::unique_ptr<llvm::object::Binary> > child = + childErr->getAsBinary(); + if (!child) { -+ ec = errorToErrorCode(child.takeError()); ++ // I don't know why, but ++ // ec = errorToErrorCode(child.takeError()) ++ // does not work here, so: + consumeError(child.takeError()); ++ ec = std::make_error_code(std::errc::io_error); + } +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) ErrorOr<std::unique_ptr<llvm::object::Binary> > child = childErr->getAsBinary(); ec = child.getError(); -@@ -319,6 +330,13 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er +@@ -319,6 +333,13 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er } } @@ -121,7 +124,7 @@ KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loaded " << archiveModules.size() << " modules\n"); -@@ -490,7 +508,12 @@ Module *klee::linkWithLibrary(Module *module, +@@ -490,7 +511,12 @@ Module *klee::linkWithLibrary(Module *module, #endif } else if (magic == sys::fs::file_magic::archive) { @@ -135,7 +138,7 @@ ErrorOr<std::unique_ptr<object::Binary> > arch = object::createBinary(Buffer, &Context); ec = arch.getError(); -@@ -548,7 +571,11 @@ Function *klee::getDirectCallTarget(CallSite cs, bool moduleIsFullyLinked) { +@@ -548,7 +574,11 @@ Function *klee::getDirectCallTarget(CallSite cs, bool moduleIsFullyLinked) { if (Function *f = dyn_cast<Function>(v)) { return f; } else if (llvm::GlobalAlias *ga = dyn_cast<GlobalAlias>(v)) { @@ -269,10 +272,10 @@ llvm::cl::ParseCommandLineOptions(argc, argv); diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp -index c48570799a7f..d193d8341e93 100644 +index dbc166ed158a..3c78b480bb23 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp -@@ -1128,7 +1128,11 @@ int main(int argc, char **argv, char **envp) { +@@ -1130,7 +1130,11 @@ int main(int argc, char **argv, char **envp) { llvm::InitializeNativeTarget(); parseArguments(argc, argv); @@ -285,5 +288,5 @@ if (Watchdog) { if (MaxTime==0) { -- -2.14.2 +2.15.0 ++++++ 0007-Add-support-for-modelling-errno_location.patch ++++++ From: Martin Nowack <[email protected]> Date: Thu, 12 Oct 2017 21:57:03 +0200 Subject: Add support for modelling errno_location Patch-mainline: no Signed-off-by: Jiri Slaby <[email protected]> --- lib/Core/SpecialFunctionHandler.cpp | 46 ++++++++++++++++++++++++++++++++++--- lib/Core/SpecialFunctionHandler.h | 1 + tools/klee/main.cpp | 2 ++ 3 files changed, 46 insertions(+), 3 deletions(-) diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 88e0d1a034bd..a019a09486c1 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -89,6 +89,8 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = { add("klee_define_fixed_object", handleDefineFixedObject, false), add("klee_get_obj_size", handleGetObjSize, true), add("klee_get_errno", handleGetErrno, true), + add("__errno_location", handleErrnoLocation, true), + add("__error", handleErrnoLocation, true), add("klee_is_symbolic", handleIsSymbolic, true), add("klee_make_symbolic", handleMakeSymbolic, false), add("klee_mark_global", handleMarkGlobal, false), @@ -537,10 +539,48 @@ void SpecialFunctionHandler::handleGetErrno(ExecutionState &state, // XXX should type check args assert(arguments.size()==0 && "invalid number of arguments to klee_get_errno"); - executor.bindLocal(target, state, - ConstantExpr::create(errno, Expr::Int32)); +#ifndef WINDOWS +#ifndef __APPLE__ + int *errno_addr = __errno_location(); +#else + int *errno_addr = __error(); +#endif +#else + int *errno_addr = nullptr; +#endif + + // Retrieve the memory object of the errno variable + ObjectPair result; + bool resolved = state.addressSpace.resolveOne( + ConstantExpr::create((uint64_t)errno_addr, Expr::Int64), result); + if (!resolved) + executor.terminateStateOnError(state, "Could not resolve address for errno", + Executor::User); + executor.bindLocal(target, state, result.second->read(0, Expr::Int32)); +} + +void SpecialFunctionHandler::handleErrnoLocation( + ExecutionState &state, KInstruction *target, + std::vector<ref<Expr> > &arguments) { + // Returns the address of the errno variable + assert(arguments.size() == 0 && + "invalid number of arguments to __errno_location"); + +#ifndef WINDOWS +#ifndef __APPLE__ + int *errno_addr = __errno_location(); +#else + int *errno_addr = __error(); +#endif +#else + int *errno_addr = nullptr; +#endif + executor.bindLocal( + target, state, + ConstantExpr::create((uint64_t)errno_addr, + executor.kmodule->targetData->getTypeSizeInBits( + target->inst->getType()))); } - void SpecialFunctionHandler::handleCalloc(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h index 394b649aff72..5e58ede4f328 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -107,6 +107,7 @@ namespace klee { HANDLER(handleDelete); HANDLER(handleDeleteArray); HANDLER(handleExit); + HANDLER(handleErrnoLocation); HANDLER(handleAliasFunction); HANDLER(handleFree); HANDLER(handleGetErrno); diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index f1def38c90e5..4a820578bf16 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -698,6 +698,8 @@ static const char *modelledExternals[] = { "_assert", "__assert_fail", "__assert_rtn", + "__errno_location", + "__error", "calloc", "_exit", "exit", -- 2.15.0 ++++++ 0007-llvm40-handle-different-header-names.patch ++++++ --- /var/tmp/diff_new_pack.lUapFu/_old 2017-11-27 22:17:08.869385892 +0100 +++ /var/tmp/diff_new_pack.lUapFu/_new 2017-11-27 22:17:08.869385892 +0100 @@ -30,7 +30,7 @@ #include "llvm/IR/LLVMContext.h" #include "llvm/IR/Module.h" diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp -index 8acada93c2cd..63d3913a08f2 100644 +index ee4af254dae2..8aa070743048 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -26,7 +26,9 @@ @@ -59,7 +59,7 @@ #include "llvm/Support/raw_ostream.h" #include "llvm/Support/Path.h" diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp -index d193d8341e93..cd54d8aab5af 100644 +index 3c78b480bb23..d45fad22896f 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -31,7 +31,6 @@ @@ -84,5 +84,5 @@ #include <signal.h> #include <unistd.h> -- -2.14.2 +2.15.0 ++++++ 0008-Cleanup-test-cases.patch ++++++ From: Martin Nowack <[email protected]> Date: Thu, 12 Oct 2017 21:59:16 +0200 Subject: Cleanup test cases Patch-mainline: no * remove assert(!errno): errno being 0 cannot be assumed if no error occured * added missing header Signed-off-by: Jiri Slaby <[email protected]> --- test/Runtime/POSIX/DirSeek.c | 1 - test/Runtime/POSIX/Ioctl.c | 1 + 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Runtime/POSIX/DirSeek.c b/test/Runtime/POSIX/DirSeek.c index 3908b4e28879..155c80b92d1e 100644 --- a/test/Runtime/POSIX/DirSeek.c +++ b/test/Runtime/POSIX/DirSeek.c @@ -43,7 +43,6 @@ int main(int argc, char **argv) { // Go to end, then back to 2nd while (de) de = readdir(d); - assert(!errno); seekdir(d, pos); assert(telldir(d) == pos); de = readdir(d); diff --git a/test/Runtime/POSIX/Ioctl.c b/test/Runtime/POSIX/Ioctl.c index e8220276f8be..f1caaf77dea2 100644 --- a/test/Runtime/POSIX/Ioctl.c +++ b/test/Runtime/POSIX/Ioctl.c @@ -5,6 +5,7 @@ #include <assert.h> #include <fcntl.h> #include <sys/stat.h> +#include <sys/ioctl.h> #include <termios.h> #include <asm/ioctls.h> #include <errno.h> -- 2.15.0 ++++++ 0008-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch ++++++ --- /var/tmp/diff_new_pack.lUapFu/_old 2017-11-27 22:17:08.893385021 +0100 +++ /var/tmp/diff_new_pack.lUapFu/_new 2017-11-27 22:17:08.893385021 +0100 @@ -9,10 +9,10 @@ 1 file changed, 9 insertions(+) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp -index aee0974c7792..08474ae700ac 100644 +index cd36eeec13e1..af7f680fec3d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp -@@ -1442,12 +1442,21 @@ static bool isDebugIntrinsic(const Function *f, KModule *KM) { +@@ -1451,12 +1451,21 @@ static bool isDebugIntrinsic(const Function *f, KModule *KM) { static inline const llvm::fltSemantics * fpWidthToSemantics(unsigned width) { switch(width) { @@ -35,5 +35,5 @@ return 0; } -- -2.14.2 +2.15.0 ++++++ 0009-llvm40-errorOr-and-similar.patch ++++++ --- /var/tmp/diff_new_pack.lUapFu/_old 2017-11-27 22:17:08.909384440 +0100 +++ /var/tmp/diff_new_pack.lUapFu/_new 2017-11-27 22:17:08.909384440 +0100 @@ -9,7 +9,7 @@ 1 file changed, 41 insertions(+), 9 deletions(-) diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp -index 63d3913a08f2..e49896a06718 100644 +index 8aa070743048..ad847de0b368 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -204,7 +204,7 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er @@ -36,7 +36,7 @@ if (!ec) { memberName = memberNameErr.get(); #else -@@ -264,7 +270,10 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er +@@ -267,7 +273,10 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er #endif if (ec) { // If we can't open as a binary object file its hopefully a bitcode file @@ -48,7 +48,7 @@ ErrorOr<MemoryBufferRef> buff = childErr->getMemoryBufferRef(); ec = buff.getError(); #elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) -@@ -288,13 +297,20 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er +@@ -291,13 +300,20 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er Module *Result = 0; // FIXME: Maybe load bitcode file lazily? Then if we need to link, materialise the module #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) @@ -71,7 +71,7 @@ if (ec) errorMessage = ec.message(); else -@@ -471,7 +487,12 @@ Module *klee::linkWithLibrary(Module *module, +@@ -474,7 +490,12 @@ Module *klee::linkWithLibrary(Module *module, #if LLVM_VERSION_CODE < LLVM_VERSION(3, 8) Module *Result = 0; #endif @@ -85,7 +85,7 @@ #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7) ErrorOr<std::unique_ptr<Module> > ResultErr = #else -@@ -677,14 +698,22 @@ Module *klee::loadModule(LLVMContext &ctx, const std::string &path, std::string +@@ -680,14 +701,22 @@ Module *klee::loadModule(LLVMContext &ctx, const std::string &path, std::string return nullptr; } @@ -111,7 +111,7 @@ return nullptr; } // The module has taken ownership of the MemoryBuffer so release it -@@ -696,7 +725,10 @@ Module *klee::loadModule(LLVMContext &ctx, const std::string &path, std::string +@@ -699,7 +728,10 @@ Module *klee::loadModule(LLVMContext &ctx, const std::string &path, std::string auto module = *errorOrModule; #endif @@ -124,5 +124,5 @@ #else if (auto ec = module->materializeAllPermanently()) { -- -2.14.2 +2.15.0 ++++++ 0009-test-fix-Feature-BFSSearcherAndDFSSearcherInterleave.patch ++++++ From: =?UTF-8?q?Julian=20B=C3=BCning?= <[email protected]> Date: Mon, 30 Oct 2017 18:53:40 +0100 Subject: test: fix Feature/BFSSearcherAndDFSSearcherInterleaved.c Patch-mainline: no To use explicit enumeration of possible strings instead of CHECK-SAME (does not work as intended with LLVM >= 3.7). Signed-off-by: Jiri Slaby <[email protected]> --- test/Feature/BFSSearcherAndDFSSearcherInterleaved.c | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c b/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c index 9cc11b709bbe..3dd5b4d59fe4 100644 --- a/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c +++ b/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c @@ -38,12 +38,6 @@ int main() { } } - // exactly 4 characters - // CHECK: {{^[A-D]{4}$}} - - // for each of A, B, C and D: occurs exactly once - // CHECK-SAME: {{^[B-D]*A[B-D]*$}} - // CHECK-SAME: {{^[A,C-D]*B[A,C-D]*$}} - // CHECK-SAME: {{^[A-B,D]*C[A-B,D]*$}} - // CHECK-SAME: {{^[A-C]*D[A-C]*$}} + // exactly 4 characters, each of A, B, C and D occur exactly once + // CHECK: {{^(ABCD|ABDC|ACBD|ACDB|ADBC|ADCB|BACD|BADC|BCAD|BCDA|BDAC|BDCA|CABD|CADB|CBAD|CBDA|CDAB|CDBA|DABC|DACB|DBAC|DBCA|DCAB|DCBA)$}} } -- 2.15.0 ++++++ 0010-llvm-use-chrono-helpers-from-LLVM-4.0.patch ++++++ --- /var/tmp/diff_new_pack.lUapFu/_old 2017-11-27 22:17:08.929383714 +0100 +++ /var/tmp/diff_new_pack.lUapFu/_new 2017-11-27 22:17:08.929383714 +0100 @@ -195,5 +195,5 @@ + +#endif -- -2.14.2 +2.15.0 ++++++ 0011-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch ++++++ --- /var/tmp/diff_new_pack.lUapFu/_old 2017-11-27 22:17:08.941383279 +0100 +++ /var/tmp/diff_new_pack.lUapFu/_new 2017-11-27 22:17:08.945383133 +0100 @@ -9,8 +9,7 @@ --- include/klee/util/GetElementPtrTypeIterator.h | 4 ++++ lib/Core/Executor.cpp | 22 +++++++++++++++++++--- - lib/Core/ExecutorUtil.cpp | 17 ++++++++++++++--- - 3 files changed, 37 insertions(+), 6 deletions(-) + 2 files changed, 23 insertions(+), 3 deletions(-) diff --git a/include/klee/util/GetElementPtrTypeIterator.h b/include/klee/util/GetElementPtrTypeIterator.h index 5fb9f4ec5c2f..bf7cb6ff0bea 100644 @@ -28,7 +27,7 @@ CurTy = 0; } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp -index 08474ae700ac..5a88f1ae3180 100644 +index af7f680fec3d..f435f5389f64 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2520,8 +2520,7 @@ void Executor::computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie) { @@ -67,41 +66,6 @@ index++; } kgepi->offset = constantOffset->getZExtValue(); -diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp -index 53f4c5b85754..6d18e07425c5 100644 ---- a/lib/Core/ExecutorUtil.cpp -+++ b/lib/Core/ExecutorUtil.cpp -@@ -199,8 +199,7 @@ namespace klee { - addend = ConstantExpr::alloc(sl->getElementOffset((unsigned) - ci->getZExtValue()), - Context::get().getPointerWidth()); -- } else { -- const SequentialType *set = cast<SequentialType>(*ii); -+ } else if (const SequentialType *set = dyn_cast<SequentialType>(*ii)) { - ref<ConstantExpr> index = - evalConstant(cast<Constant>(ii.getOperand()), ki); - unsigned elementSize = -@@ -209,7 +208,19 @@ namespace klee { - index = index->ZExt(Context::get().getPointerWidth()); - addend = index->Mul(ConstantExpr::alloc(elementSize, - Context::get().getPointerWidth())); -- } -+#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0) -+ } else if (const PointerType *ptr = dyn_cast<PointerType>(*ii)) { -+ ref<ConstantExpr> index = -+ evalConstant(cast<Constant>(ii.getOperand())); -+ unsigned elementSize = -+ kmodule->targetData->getTypeStoreSize(ptr->getElementType()); -+ -+ index = index->ZExt(Context::get().getPointerWidth()); -+ addend = index->Mul(ConstantExpr::alloc(elementSize, -+ Context::get().getPointerWidth())); -+#endif -+ } else -+ assert("invalid type" && 0); - - base = base->Add(addend); - } -- -2.14.2 +2.15.0 ++++++ 0012-llvm40-gep_type_iterator-has-no-operator.patch ++++++ From: Jiri Slaby <[email protected]> Date: Fri, 17 Nov 2017 17:56:18 +0100 Subject: llvm40: gep_type_iterator has no operator* Patch-mainline: no Starting with LLVM 4.0, we have getStructTypeOrNull(), so use it. operator* in post-4 will have a different semantics. Signed-off-by: Jiri Slaby <[email protected]> --- lib/Core/ExecutorUtil.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 92dee5ac3906..c9308795804e 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -200,7 +200,11 @@ namespace klee { continue; // Handle a struct index, which adds its field offset to the pointer. +#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0) + if (StructType *STy = ii.getStructTypeOrNull()) { +#else if (StructType *STy = dyn_cast<StructType>(*ii)) { +#endif unsigned ElementIdx = indexOp->getZExtValue(); const StructLayout *SL = kmodule->targetData->getStructLayout(STy); base = base->Add( -- 2.15.0 ++++++ 0013-llvm38-test-change-some-tests.patch ++++++ From: Jiri Slaby <[email protected]> Date: Wed, 1 Nov 2017 09:25:47 +0100 Subject: llvm38: test, change some tests Patch-mainline: no alias in LLVM 3.8 has a new format, it adds a AliaseeTy parameter. So handle this in the tests. Signed-off-by: Jiri Slaby <[email protected]> --- test/Feature/BitcastAlias.llvm37.ll | 1 + test/Feature/BitcastAlias.llvm38.ll | 35 +++++++++++++++++++++++++++++++++ test/Feature/BitcastAliasMD2U.llvm37.ll | 1 + test/Feature/BitcastAliasMD2U.llvm38.ll | 35 +++++++++++++++++++++++++++++++++ 4 files changed, 72 insertions(+) create mode 100644 test/Feature/BitcastAlias.llvm38.ll create mode 100644 test/Feature/BitcastAliasMD2U.llvm38.ll diff --git a/test/Feature/BitcastAlias.llvm37.ll b/test/Feature/BitcastAlias.llvm37.ll index 0d6e72604d6b..3b702ba2a6b0 100644 --- a/test/Feature/BitcastAlias.llvm37.ll +++ b/test/Feature/BitcastAlias.llvm37.ll @@ -1,4 +1,5 @@ ; REQUIRES: geq-llvm-3.7 +; REQUIRES: lt-llvm-3.8 ; RUN: llvm-as %s -f -o %t1.bc ; RUN: rm -rf %t.klee-out ; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 diff --git a/test/Feature/BitcastAlias.llvm38.ll b/test/Feature/BitcastAlias.llvm38.ll new file mode 100644 index 000000000000..ff7009b7711b --- /dev/null +++ b/test/Feature/BitcastAlias.llvm38.ll @@ -0,0 +1,35 @@ +; REQUIRES: geq-llvm-3.8 +; RUN: llvm-as %s -f -o %t1.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 +; RUN: grep PASS %t2 + +target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64" +target triple = "x86_64-unknown-linux-gnu" + +@foo = alias i32 (i32), i32 (i32)* @__foo + +define i32 @__foo(i32 %i) nounwind { +entry: + ret i32 %i +} + +declare i32 @puts(i8*) + [email protected] = private constant [5 x i8] c"PASS\00", align 1 [email protected] = private constant [5 x i8] c"FAIL\00", align 1 + +define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone { +entry: + %call = call i32 (i64) bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52) + %r = icmp eq i32 %call, 52 + br i1 %r, label %bbtrue, label %bbfalse + +bbtrue: + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind + ret i32 0 + +bbfalse: + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind + ret i32 0 +} diff --git a/test/Feature/BitcastAliasMD2U.llvm37.ll b/test/Feature/BitcastAliasMD2U.llvm37.ll index 12abf09373f8..2332a1968dea 100644 --- a/test/Feature/BitcastAliasMD2U.llvm37.ll +++ b/test/Feature/BitcastAliasMD2U.llvm37.ll @@ -1,4 +1,5 @@ ; REQUIRES: geq-llvm-3.7 +; REQUIRES: lt-llvm-3.8 ; RUN: llvm-as %s -f -o %t1.bc ; RUN: rm -rf %t.klee-out ; RUN: %klee --output-dir=%t.klee-out -disable-opt -search=nurs:md2u %t1.bc > %t2 diff --git a/test/Feature/BitcastAliasMD2U.llvm38.ll b/test/Feature/BitcastAliasMD2U.llvm38.ll new file mode 100644 index 000000000000..f4e41293c347 --- /dev/null +++ b/test/Feature/BitcastAliasMD2U.llvm38.ll @@ -0,0 +1,35 @@ +; REQUIRES: geq-llvm-3.8 +; RUN: llvm-as %s -f -o %t1.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt -search=nurs:md2u %t1.bc > %t2 +; RUN: grep PASS %t2 + +target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64" +target triple = "x86_64-unknown-linux-gnu" + +@foo = alias i32 (i32), i32 (i32)* @__foo + +define i32 @__foo(i32 %i) nounwind { +entry: + ret i32 %i +} + +declare i32 @puts(i8*) + [email protected] = private constant [5 x i8] c"PASS\00", align 1 [email protected] = private constant [5 x i8] c"FAIL\00", align 1 + +define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone { +entry: + %call = call i32 (i64) bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52) + %r = icmp eq i32 %call, 52 + br i1 %r, label %bbtrue, label %bbfalse + +bbtrue: + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind + ret i32 0 + +bbfalse: + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind + ret i32 0 +} -- 2.15.0 ++++++ _servicedata ++++++ --- /var/tmp/diff_new_pack.lUapFu/_old 2017-11-27 22:17:09.013380665 +0100 +++ /var/tmp/diff_new_pack.lUapFu/_new 2017-11-27 22:17:09.013380665 +0100 @@ -1,4 +1,4 @@ <servicedata> <service name="tar_scm"> <param name="url">git://github.com/klee/klee.git</param> - <param name="changesrevision">9f11eababd767b012b623806b40fa0647affa47e</param></service></servicedata> \ No newline at end of file + <param name="changesrevision">9caaae0b1b6e52be3c7bb783f3a8be659a1a1869</param></service></servicedata> \ No newline at end of file ++++++ klee-1.4.0+20171009.tar.xz -> klee-1.4.0+20171026.tar.xz ++++++ diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/klee-1.4.0+20171009/.travis/klee.sh new/klee-1.4.0+20171026/.travis/klee.sh --- old/klee-1.4.0+20171009/.travis/klee.sh 2017-10-09 20:49:45.000000000 +0200 +++ new/klee-1.4.0+20171026/.travis/klee.sh 2017-10-26 16:50:55.000000000 +0200 @@ -147,9 +147,12 @@ # If metaSMT is the only solver, then rerun lit tests with non-default metaSMT backends if [ "X${SOLVERS}" == "XmetaSMT" ]; then metasmt_default=`echo "${METASMT_DEFAULT,,}"` # klee_opts and kleaver_opts use lowercase - available_metasmt_backends="btor stp z3" + available_metasmt_backends="btor stp z3 yices2 cvc4" for backend in $available_metasmt_backends; do if [ "X${metasmt_default}" != "X$backend" ]; then + if [ "$backend" == "cvc4" ]; then + for num in {1..5}; do sleep 120; echo 'Keep Travis alive'; done & + fi lit -v --param klee_opts=-metasmt-backend=$backend --param kleaver_opts=-metasmt-backend=$backend test/ fi done diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/klee-1.4.0+20171009/.travis/metaSMT.sh new/klee-1.4.0+20171026/.travis/metaSMT.sh --- old/klee-1.4.0+20171009/.travis/metaSMT.sh 2017-10-09 20:49:45.000000000 +0200 +++ new/klee-1.4.0+20171026/.travis/metaSMT.sh 2017-10-26 16:50:55.000000000 +0200 @@ -4,8 +4,8 @@ : ${METASMT_VERSION?"METASMT_VERSION not specified"} -# Get Z3, libgmp -sudo apt-get -y install libz3 libz3-dev libgmp-dev +# Get Z3, libgmp, gperf (required by yices2) +sudo apt-get -y install libz3 libz3-dev libgmp-dev gperf # Get Boost if [ "X${METASMT_BOOST_VERSION}" != "X" ]; then @@ -19,6 +19,11 @@ sudo apt-get -y install libboost1.55-dev fi +# Get CVC4 +wget http://www.informatik.uni-bremen.de/agra/systemc-verification/media/snapshots/cvc4-594301e.tar.gz +tar -xf cvc4-594301e.tar.gz +sudo mv cvc4 /usr + # Clone git clone -b ${METASMT_VERSION} --single-branch --depth 1 https://github.com/hoangmle/metaSMT.git cd metaSMT @@ -33,11 +38,12 @@ # Bootstrap export BOOST_ROOT=/usr sudo cp dependencies/Z3-2.19/Z3Config.cmake /usr # this is a hack -./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off -DmetaSMT_REQUIRE_CXX11=off --build stp-git-basic --build boolector-2.2.0 --build minisat-git --build lingeling-ayv-86bf266-140429 -DZ3_DIR=/usr +./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off --build stp-git-basic --build boolector-2.2.0 --build minisat-git --build lingeling-ayv-86bf266-140429 --build yices-2.5.1 -DZ3_DIR=/usr -DCVC4_DIR=/usr/cvc4 sudo cp deps/boolector-2.2.0/lib/* /usr/lib/ # sudo cp deps/lingeling-ayv-86bf266-140429/lib/* /usr/lib/ # sudo cp deps/minisat-git/lib/* /usr/lib/ # hack sudo cp -r deps/stp-git-basic/lib/lib* /usr/lib/ # +sudo cp deps/yices-2.5.1/lib/* /usr/lib/ # # Build make -C build install diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/klee-1.4.0+20171009/.travis.yml new/klee-1.4.0+20171026/.travis.yml --- old/klee-1.4.0+20171009/.travis.yml 2017-10-09 20:49:45.000000000 +0200 +++ new/klee-1.4.0+20171026/.travis.yml 2017-10-26 16:50:55.000000000 +0200 @@ -24,7 +24,7 @@ # SOLVERS : {Z3, STP, STP:Z3, metaSMT} # STP_VERSION : {2.1.2, master} # METASMT_VERSION : {v4.rc1} - # METASMT_DEFAULT : {BTOR, STP, Z3} + # METASMT_DEFAULT : {BTOR, CVC4, STP, YICES2, Z3} # METASMT_BOOST_VERSION : {x.y.z} // e.g. 1.60.0, libboost-dev will be used if unspecified # UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled # DISABLE_ASSERTIONS: {0, 1} diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/klee-1.4.0+20171009/CMakeLists.txt new/klee-1.4.0+20171026/CMakeLists.txt --- old/klee-1.4.0+20171009/CMakeLists.txt 2017-10-09 20:49:45.000000000 +0200 +++ new/klee-1.4.0+20171026/CMakeLists.txt 2017-10-26 16:50:55.000000000 +0200 @@ -370,6 +370,8 @@ if (ENABLE_TCMALLOC) message(STATUS "TCMalloc support enabled") set(TCMALLOC_HEADER "gperftools/malloc_extension.h") + find_path(TCMALLOC_INCLUDE_DIR "${TCMALLOC_HEADER}") + set(CMAKE_REQUIRED_INCLUDES "${TCMALLOC_INCLUDE_DIR}") check_include_file_cxx("${TCMALLOC_HEADER}" HAVE_GPERFTOOLS_MALLOC_EXTENSION_H) if (${HAVE_GPERFTOOLS_MALLOC_EXTENSION_H}) find_library(TCMALLOC_LIBRARIES diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/klee-1.4.0+20171009/cmake/find_metasmt.cmake new/klee-1.4.0+20171026/cmake/find_metasmt.cmake --- old/klee-1.4.0+20171009/cmake/find_metasmt.cmake 2017-10-09 20:49:45.000000000 +0200 +++ new/klee-1.4.0+20171026/cmake/find_metasmt.cmake 2017-10-26 16:50:55.000000000 +0200 @@ -62,7 +62,13 @@ klee_component_add_cxx_flag(${f} REQUIRED) endforeach() - set(available_metasmt_backends "BTOR" "STP" "Z3") + # Check if metaSMT provides an useable backend + if (NOT metaSMT_AVAILABLE_QF_ABV_SOLVERS) + message(FATAL_ERROR "metaSMT does not provide an useable backend.") + endif() + + message(STATUS "metaSMT has the following backend(s): ${metaSMT_AVAILABLE_QF_ABV_SOLVERS}.") + set(available_metasmt_backends ${metaSMT_AVAILABLE_QF_ABV_SOLVERS}) set(METASMT_DEFAULT_BACKEND "STP" CACHE STRING @@ -79,9 +85,12 @@ "Valid values are ${available_metasmt_backends}") endif() - # Set appropriate define + # Set appropriate defines list(APPEND KLEE_COMPONENT_CXX_DEFINES -DMETASMT_DEFAULT_BACKEND_IS_${METASMT_DEFAULT_BACKEND}) + foreach(backend ${available_metasmt_backends}) + list(APPEND KLEE_COMPONENT_CXX_DEFINES -DMETASMT_HAVE_${backend}) + endforeach() else() message(STATUS "metaSMT solver support disabled") set(ENABLE_METASMT 0) # For config.h diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/klee-1.4.0+20171009/include/klee/CommandLine.h new/klee-1.4.0+20171026/include/klee/CommandLine.h --- old/klee-1.4.0+20171009/include/klee/CommandLine.h 2017-10-09 20:49:45.000000000 +0200 +++ new/klee-1.4.0+20171026/include/klee/CommandLine.h 2017-10-26 16:50:55.000000000 +0200 @@ -61,7 +61,9 @@ { METASMT_BACKEND_STP, METASMT_BACKEND_Z3, - METASMT_BACKEND_BOOLECTOR + METASMT_BACKEND_BOOLECTOR, + METASMT_BACKEND_CVC4, + METASMT_BACKEND_YICES2 }; extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend; diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/klee-1.4.0+20171009/lib/Basic/CmdLineOptions.cpp new/klee-1.4.0+20171026/lib/Basic/CmdLineOptions.cpp --- old/klee-1.4.0+20171009/lib/Basic/CmdLineOptions.cpp 2017-10-09 20:49:45.000000000 +0200 +++ new/klee-1.4.0+20171026/lib/Basic/CmdLineOptions.cpp 2017-10-26 16:50:55.000000000 +0200 @@ -112,6 +112,12 @@ #elif METASMT_DEFAULT_BACKEND_IS_Z3 #define METASMT_DEFAULT_BACKEND_STR "(default = z3)." #define METASMT_DEFAULT_BACKEND METASMT_BACKEND_Z3 +#elif METASMT_DEFAULT_BACKEND_IS_CVC4 +#define METASMT_DEFAULT_BACKEND_STR "(default = cvc4)." +#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_CVC4 +#elif METASMT_DEFAULT_BACKEND_IS_YICES2 +#define METASMT_DEFAULT_BACKEND_STR "(default = yices2)." +#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_YICES2 #else #define METASMT_DEFAULT_BACKEND_STR "(default = stp)." #define METASMT_DEFAULT_BACKEND METASMT_BACKEND_STP @@ -123,7 +129,9 @@ cl::values(clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"), clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"), clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor", - "Use metaSMT with Boolector") + "Use metaSMT with Boolector"), + clEnumValN(METASMT_BACKEND_CVC4, "cvc4", "Use metaSMT with CVC4"), + clEnumValN(METASMT_BACKEND_YICES2, "yices2", "Use metaSMT with Yices2") KLEE_LLVM_CL_VAL_END), cl::init(METASMT_DEFAULT_BACKEND)); diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/klee-1.4.0+20171009/lib/Core/Executor.cpp new/klee-1.4.0+20171026/lib/Core/Executor.cpp --- old/klee-1.4.0+20171009/lib/Core/Executor.cpp 2017-10-09 20:49:45.000000000 +0200 +++ new/klee-1.4.0+20171026/lib/Core/Executor.cpp 2017-10-26 16:50:55.000000000 +0200 @@ -3114,7 +3114,7 @@ // malloc will fail for it, so lets fork and return 0. StatePair hugeSize = fork(*fixedSize.second, - UltExpr::create(ConstantExpr::alloc(1<<31, W), size), + UltExpr::create(ConstantExpr::alloc(1U<<31, W), size), true); if (hugeSize.first) { klee_message("NOTE: found huge malloc, returning 0"); @@ -3520,8 +3520,6 @@ void Executor::getConstraintLog(const ExecutionState &state, std::string &res, Interpreter::LogType logFormat) { - std::ostringstream info; - switch (logFormat) { case STP: { Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/klee-1.4.0+20171009/lib/Core/Searcher.cpp new/klee-1.4.0+20171026/lib/Core/Searcher.cpp --- old/klee-1.4.0+20171009/lib/Core/Searcher.cpp 2017-10-09 20:49:45.000000000 +0200 +++ new/klee-1.4.0+20171026/lib/Core/Searcher.cpp 2017-10-26 16:50:55.000000000 +0200 @@ -104,8 +104,9 @@ if (!addedStates.empty() && current && std::find(removedStates.begin(), removedStates.end(), current) == removedStates.end()) { - assert(states.front() == current); - states.pop_front(); + auto pos = std::find(states.begin(), states.end(), current); + assert(pos != states.end()); + states.erase(pos); states.push_back(current); } diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/klee-1.4.0+20171009/lib/Solver/MetaSMTSolver.cpp new/klee-1.4.0+20171026/lib/Solver/MetaSMTSolver.cpp --- old/klee-1.4.0+20171009/lib/Solver/MetaSMTSolver.cpp 2017-10-09 20:49:45.000000000 +0200 +++ new/klee-1.4.0+20171026/lib/Solver/MetaSMTSolver.cpp 2017-10-26 16:50:55.000000000 +0200 @@ -21,16 +21,34 @@ #include "llvm/Support/ErrorHandling.h" #include <metaSMT/DirectSolver_Context.hpp> + +#ifdef METASMT_HAVE_Z3 #include <metaSMT/backend/Z3_Backend.hpp> +#endif + +#ifdef METASMT_HAVE_BTOR #include <metaSMT/backend/Boolector.hpp> +#endif + +#ifdef METASMT_HAVE_CVC4 +#include <metaSMT/backend/CVC4.hpp> +#endif + +#ifdef METASMT_HAVE_YICES2 +#include <metaSMT/backend/Yices2.hpp> +#endif +#ifdef METASMT_HAVE_STP #define Expr VCExpr #define Type VCType #define STP STP_Backend +#define type_t STP_type_t #include <metaSMT/backend/STP.hpp> #undef Expr #undef Type #undef STP +#undef type_t +#endif #include <errno.h> #include <unistd.h> @@ -405,32 +423,47 @@ impl->setCoreSolverTimeout(timeout); } -template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Boolector> >; -template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Z3_Backend> >; -template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::STP_Backend> >; - Solver *createMetaSMTSolver() { - using metaSMT::DirectSolver_Context; - using namespace metaSMT::solver; + using namespace metaSMT; Solver *coreSolver = NULL; std::string backend; switch (MetaSMTBackend) { +#ifdef METASMT_HAVE_STP case METASMT_BACKEND_STP: backend = "STP"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<STP_Backend> >( + coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::STP_Backend> >( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; +#endif +#ifdef METASMT_HAVE_Z3 case METASMT_BACKEND_Z3: backend = "Z3"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<Z3_Backend> >( + coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Z3_Backend> >( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; +#endif +#ifdef METASMT_HAVE_BTOR case METASMT_BACKEND_BOOLECTOR: backend = "Boolector"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<Boolector> >( + coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Boolector> >( + UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; +#endif +#ifdef METASMT_HAVE_CVC4 + case METASMT_BACKEND_CVC4: + backend = "CVC4"; + coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::CVC4> >( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; +#endif +#ifdef METASMT_HAVE_YICES2 + case METASMT_BACKEND_YICES2: + backend = "Yices2"; + coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Yices2> >( + UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; +#endif default: llvm_unreachable("Unrecognised MetaSMT backend"); break; diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/klee-1.4.0+20171009/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c new/klee-1.4.0+20171026/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c --- old/klee-1.4.0+20171009/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c 1970-01-01 01:00:00.000000000 +0100 +++ new/klee-1.4.0+20171026/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c 2017-10-26 16:50:55.000000000 +0200 @@ -0,0 +1,49 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc +// RUN: rm -rf %t-bfs.klee-out +// RUN: rm -rf %t-dfs.klee-out +// RUN: rm -rf %t-bfs-dfs.klee-out +// RUN: rm -rf %t-dfs-bfs.klee-out +// RUN: %klee -output-dir=%t-bfs.klee-out -search=bfs %t.bc >%t-bfs.out +// RUN: %klee -output-dir=%t-dfs.klee-out -search=dfs %t.bc >%t-dfs.out +// RUN: %klee -output-dir=%t-bfs-dfs.klee-out -search=bfs -search=dfs %t.bc >%t-bfs-dfs.out +// RUN: %klee -output-dir=%t-dfs-bfs.klee-out -search=dfs -search=bfs %t.bc >%t-dfs-bfs.out +// RUN: FileCheck -input-file=%t-bfs.out %s +// RUN: FileCheck -input-file=%t-dfs.out %s +// RUN: FileCheck -input-file=%t-bfs-dfs.out %s +// RUN: FileCheck -input-file=%t-dfs-bfs.out %s + +#include "klee/klee.h" + +int main() { + int x, y, z; + klee_make_symbolic(&x, sizeof(x), "x"); + klee_make_symbolic(&y, sizeof(y), "y"); + klee_make_symbolic(&z, sizeof(z), "z"); + + if (x == 1) { + if (y == 1) { + if (z == 1) { + printf("A"); + } else { + printf("B"); + } + } + } else { + if (y == 1) { + if (z == 1) { + printf("C"); + } else { + printf("D"); + } + } + } + + // exactly 4 characters + // CHECK: {{^[A-D]{4}$}} + + // for each of A, B, C and D: occurs exactly once + // CHECK-SAME: {{^[B-D]*A[B-D]*$}} + // CHECK-SAME: {{^[A,C-D]*B[A,C-D]*$}} + // CHECK-SAME: {{^[A-B,D]*C[A-B,D]*$}} + // CHECK-SAME: {{^[A-C]*D[A-C]*$}} +}
