Accepting request 545450 from devel:tools:statica
Automatic submission by obs-autosubmit OBS-URL: https://build.opensuse.org/request/show/545450 OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/klee?expand=0&rev=6
This commit is contained in:
commit
7729329c3d
@ -0,0 +1,31 @@
|
|||||||
|
From: Martin Nowack <martin_nowack@tu-dresden.de>
|
||||||
|
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 <jirislaby@gmail.com>
|
||||||
|
---
|
||||||
|
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
|
||||||
|
|
@ -1,42 +0,0 @@
|
|||||||
From: Jiri Slaby <jirislaby@gmail.com>
|
|
||||||
Date: Fri, 17 Mar 2017 13:15:18 +0100
|
|
||||||
Subject: errno: define __errno_location
|
|
||||||
Patch-mainline: no
|
|
||||||
|
|
||||||
POSIX runtime library is built on my system with a reference to
|
|
||||||
__errno_location(). And then it is undefined when klee is run
|
|
||||||
--with-posix:
|
|
||||||
KLEE: NOTE: Using model: lib/libkleeRuntimePOSIX.bca
|
|
||||||
KLEE: output directory is "test/Runtime/POSIX/Output/Read1.c.tmp.klee-out"
|
|
||||||
KLEE: Using STP solver backend
|
|
||||||
KLEE: WARNING: undefined reference to function: __errno_location
|
|
||||||
KLEE: WARNING ONCE: calling external: __errno_location()
|
|
||||||
KLEE: ERROR: (location information missing) ASSERTION FAIL: x == -1 && errno == EFAULT
|
|
||||||
KLEE: NOTE: now ignoring this error at this location
|
|
||||||
EXITING ON ERROR:
|
|
||||||
Error: ASSERTION FAIL: x == -1 && errno == EFAULT
|
|
||||||
Stack:
|
|
||||||
#000000170 in main (argc=4, argv=24928704)
|
|
||||||
|
|
||||||
Therefore, the tests fail.
|
|
||||||
|
|
||||||
Define __errno_location as a weak symbol to return the actual int errno.
|
|
||||||
|
|
||||||
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
||||||
---
|
|
||||||
runtime/POSIX/errno_location.c | 9 +++++++++
|
|
||||||
1 file changed, 9 insertions(+)
|
|
||||||
create mode 100644 runtime/POSIX/errno_location.c
|
|
||||||
|
|
||||||
--- /dev/null
|
|
||||||
+++ b/runtime/POSIX/errno_location.c
|
|
||||||
@@ -0,0 +1,9 @@
|
|
||||||
+#include <errno.h>
|
|
||||||
+
|
|
||||||
+#undef errno
|
|
||||||
+int errno __attribute__((weak));
|
|
||||||
+
|
|
||||||
+int __attribute__((weak)) *__errno_location(void)
|
|
||||||
+{
|
|
||||||
+ return &errno;
|
|
||||||
+}
|
|
@ -32,10 +32,10 @@ index ccf54ae13092..532051602fe3 100644
|
|||||||
# define KLEE_LLVM_CL_VAL_END
|
# define KLEE_LLVM_CL_VAL_END
|
||||||
#else
|
#else
|
||||||
diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
|
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
|
--- a/lib/Core/ExternalDispatcher.cpp
|
||||||
+++ b/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 =
|
Type *argTy =
|
||||||
(i < FTy->getNumParams() ? FTy->getParamType(i) : (*ai)->getType());
|
(i < FTy->getNumParams() ? FTy->getParamType(i) : (*ai)->getType());
|
||||||
Instruction *argI64p = GetElementPtrInst::Create(
|
Instruction *argI64p = GetElementPtrInst::Create(
|
||||||
@ -68,5 +68,5 @@ index b02605208bbb..54bda16013b6 100644
|
|||||||
}
|
}
|
||||||
ii->removeFromParent();
|
ii->removeFromParent();
|
||||||
--
|
--
|
||||||
2.14.2
|
2.15.0
|
||||||
|
|
||||||
|
@ -1,51 +0,0 @@
|
|||||||
From: Jiri Slaby <jirislaby@gmail.com>
|
|
||||||
Date: Fri, 17 Mar 2017 13:40:30 +0100
|
|
||||||
Subject: test: disable some tests temporarily
|
|
||||||
Patch-mainline: no
|
|
||||||
|
|
||||||
They fail for some reason I cannot debug ATM, I will fix it later.
|
|
||||||
|
|
||||||
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
||||||
---
|
|
||||||
test/Feature/BitcastAlias.llvm37.ll | 1 +
|
|
||||||
test/Feature/BitcastAliasMD2U.llvm37.ll | 1 +
|
|
||||||
test/Runtime/POSIX/DirSeek.c | 1 +
|
|
||||||
test/Runtime/POSIX/Ioctl.c | 1 +
|
|
||||||
4 files changed, 4 insertions(+)
|
|
||||||
|
|
||||||
--- a/test/Feature/BitcastAlias.llvm37.ll
|
|
||||||
+++ b/test/Feature/BitcastAlias.llvm37.ll
|
|
||||||
@@ -1,4 +1,5 @@
|
|
||||||
; REQUIRES: geq-llvm-3.7
|
|
||||||
+; REQUIRES: lt-llvm-4.0
|
|
||||||
; 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
|
|
||||||
--- a/test/Feature/BitcastAliasMD2U.llvm37.ll
|
|
||||||
+++ b/test/Feature/BitcastAliasMD2U.llvm37.ll
|
|
||||||
@@ -1,4 +1,5 @@
|
|
||||||
; REQUIRES: geq-llvm-3.7
|
|
||||||
+; REQUIRES: lt-llvm-4.0
|
|
||||||
; 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
|
|
||||||
--- a/test/Runtime/POSIX/DirSeek.c
|
|
||||||
+++ b/test/Runtime/POSIX/DirSeek.c
|
|
||||||
@@ -8,6 +8,7 @@
|
|
||||||
// RUN: rm -rf %t.klee-out %t.klee-out-tmp
|
|
||||||
// RUN: %gentmp %t.klee-out-tmp
|
|
||||||
// RUN: %klee --output-dir=%t.klee-out --run-in=%t.klee-out-tmp --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 0 2
|
|
||||||
+// XFAIL: *
|
|
||||||
|
|
||||||
// For this test really to work as intended it needs to be run in a
|
|
||||||
// directory large enough to cause uclibc to do multiple getdents
|
|
||||||
--- a/test/Runtime/POSIX/Ioctl.c
|
|
||||||
+++ b/test/Runtime/POSIX/Ioctl.c
|
|
||||||
@@ -1,6 +1,7 @@
|
|
||||||
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
|
|
||||||
// RUN: rm -rf %t.klee-out
|
|
||||||
// RUN: %klee --output-dir=%t.klee-out --posix-runtime --exit-on-error %t.bc --sym-files 0 4
|
|
||||||
+// REQUIRES: undefined-symbol
|
|
||||||
|
|
||||||
#include <assert.h>
|
|
||||||
#include <fcntl.h>
|
|
100
0002-Fix-getelementptr-for-array-or-vector-indices.patch
Normal file
100
0002-Fix-getelementptr-for-array-or-vector-indices.patch
Normal file
@ -0,0 +1,100 @@
|
|||||||
|
From: Martin Nowack <martin_nowack@tu-dresden.de>
|
||||||
|
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 <jirislaby@gmail.com>
|
||||||
|
---
|
||||||
|
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
|
||||||
|
|
@ -161,7 +161,7 @@ index 13e4f7d47e58..c597fa2a7b82 100644
|
|||||||
TLI = TM->getSubtargetImpl()->getTargetLowering();
|
TLI = TM->getSubtargetImpl()->getTargetLowering();
|
||||||
#else
|
#else
|
||||||
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
|
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
|
--- a/tools/klee/main.cpp
|
||||||
+++ b/tools/klee/main.cpp
|
+++ b/tools/klee/main.cpp
|
||||||
@@ -35,6 +35,7 @@
|
@@ -35,6 +35,7 @@
|
||||||
@ -173,5 +173,5 @@ index f1def38c90e5..5d1d0c22495c 100644
|
|||||||
|
|
||||||
#include "llvm/Support/TargetSelect.h"
|
#include "llvm/Support/TargetSelect.h"
|
||||||
--
|
--
|
||||||
2.14.2
|
2.15.0
|
||||||
|
|
||||||
|
@ -0,0 +1,52 @@
|
|||||||
|
From: Martin Nowack <martin_nowack@tu-dresden.de>
|
||||||
|
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 <jirislaby@gmail.com>
|
||||||
|
---
|
||||||
|
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
|
||||||
|
|
@ -1615,5 +1615,5 @@ index 000000000000..aa6b42ed6b9f
|
|||||||
+ return 0;
|
+ return 0;
|
||||||
+}
|
+}
|
||||||
--
|
--
|
||||||
2.14.2
|
2.15.0
|
||||||
|
|
||||||
|
@ -0,0 +1,43 @@
|
|||||||
|
From: Martin Nowack <martin@se.inf.tu-dresden.de>
|
||||||
|
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 <jirislaby@gmail.com>
|
||||||
|
---
|
||||||
|
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
|
||||||
|
|
@ -12,7 +12,7 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|||||||
1 file changed, 4 insertions(+)
|
1 file changed, 4 insertions(+)
|
||||||
|
|
||||||
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
|
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
|
--- a/lib/Basic/CmdLineOptions.cpp
|
||||||
+++ b/lib/Basic/CmdLineOptions.cpp
|
+++ b/lib/Basic/CmdLineOptions.cpp
|
||||||
@@ -86,8 +86,12 @@ UseAssignmentValidatingSolver("debug-assignment-validating-solver",
|
@@ -86,8 +86,12 @@ UseAssignmentValidatingSolver("debug-assignment-validating-solver",
|
||||||
@ -20,7 +20,7 @@ index bffd3a4f7c00..ce09edde90ea 100644
|
|||||||
|
|
||||||
void KCommandLine::HideUnrelatedOptions(cl::OptionCategory &Category) {
|
void KCommandLine::HideUnrelatedOptions(cl::OptionCategory &Category) {
|
||||||
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7)
|
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7)
|
||||||
+ StringMap<cl::Option*> &map = cl::getRegisteredOptions();
|
+ StringMap<cl::Option *> &map = cl::getRegisteredOptions();
|
||||||
+#else
|
+#else
|
||||||
StringMap<cl::Option *> map;
|
StringMap<cl::Option *> map;
|
||||||
cl::getRegisteredOptions(map);
|
cl::getRegisteredOptions(map);
|
||||||
@ -29,5 +29,5 @@ index bffd3a4f7c00..ce09edde90ea 100644
|
|||||||
i++) {
|
i++) {
|
||||||
if (i->second->Category != &Category) {
|
if (i->second->Category != &Category) {
|
||||||
--
|
--
|
||||||
2.14.2
|
2.15.0
|
||||||
|
|
||||||
|
146
0005-Track-errno-correctly.patch
Normal file
146
0005-Track-errno-correctly.patch
Normal file
@ -0,0 +1,146 @@
|
|||||||
|
From: Martin Nowack <martin@se.inf.tu-dresden.de>
|
||||||
|
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 <jirislaby@gmail.com>
|
||||||
|
---
|
||||||
|
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
|
||||||
|
|
@ -15,10 +15,10 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|||||||
7 files changed, 77 insertions(+), 9 deletions(-)
|
7 files changed, 77 insertions(+), 9 deletions(-)
|
||||||
|
|
||||||
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
|
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
|
--- a/lib/Core/Executor.cpp
|
||||||
+++ b/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()))
|
!fpWidthToSemantics(right->getWidth()))
|
||||||
return terminateStateOnExecError(state, "Unsupported FRem operation");
|
return terminateStateOnExecError(state, "Unsupported FRem operation");
|
||||||
llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
|
llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
|
||||||
@ -248,7 +248,7 @@ index 64e4863f70b3..944f51ef336d 100644
|
|||||||
addPass(Passes, createLICMPass()); // Hoist loop invariants
|
addPass(Passes, createLICMPass()); // Hoist loop invariants
|
||||||
addPass(Passes, createGVNPass()); // Remove redundancies
|
addPass(Passes, createGVNPass()); // Remove redundancies
|
||||||
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
|
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
|
--- a/tools/klee/main.cpp
|
||||||
+++ b/tools/klee/main.cpp
|
+++ b/tools/klee/main.cpp
|
||||||
@@ -291,7 +291,12 @@ KleeHandler::KleeHandler(int argc, char **argv)
|
@@ -291,7 +291,12 @@ KleeHandler::KleeHandler(int argc, char **argv)
|
||||||
@ -266,5 +266,5 @@ index 5d1d0c22495c..c48570799a7f 100644
|
|||||||
// create directory and try to link klee-last
|
// create directory and try to link klee-last
|
||||||
if (mkdir(d.c_str(), 0775) == 0) {
|
if (mkdir(d.c_str(), 0775) == 0) {
|
||||||
--
|
--
|
||||||
2.14.2
|
2.15.0
|
||||||
|
|
||||||
|
@ -0,0 +1,44 @@
|
|||||||
|
From: Martin Nowack <martin_nowack@tu-dresden.de>
|
||||||
|
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 <jirislaby@gmail.com>
|
||||||
|
---
|
||||||
|
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
|
||||||
|
|
@ -7,18 +7,18 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|||||||
---
|
---
|
||||||
lib/Core/Executor.cpp | 16 ++++++++++++++++
|
lib/Core/Executor.cpp | 16 ++++++++++++++++
|
||||||
lib/Core/MemoryManager.cpp | 5 ++++-
|
lib/Core/MemoryManager.cpp | 5 ++++-
|
||||||
lib/Module/ModuleUtil.cpp | 33 ++++++++++++++++++++++++++++++---
|
lib/Module/ModuleUtil.cpp | 36 +++++++++++++++++++++++++++++++++---
|
||||||
lib/Module/Optimize.cpp | 28 ++++++++++++++++++++++++++++
|
lib/Module/Optimize.cpp | 28 ++++++++++++++++++++++++++++
|
||||||
lib/Module/RaiseAsm.cpp | 10 +++++++++-
|
lib/Module/RaiseAsm.cpp | 10 +++++++++-
|
||||||
tools/kleaver/main.cpp | 4 ++++
|
tools/kleaver/main.cpp | 4 ++++
|
||||||
tools/klee/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
|
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
|
--- a/lib/Core/Executor.cpp
|
||||||
+++ b/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
|
// Alignment requirements for scalar types is the same as their size
|
||||||
if (argWidth > Expr::Int64) {
|
if (argWidth > Expr::Int64) {
|
||||||
@ -37,7 +37,7 @@ index cb8862813133..aee0974c7792 100644
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -1335,10 +1343,18 @@ void Executor::executeCall(ExecutionState &state,
|
@@ -1344,10 +1352,18 @@ void Executor::executeCall(ExecutionState &state,
|
||||||
|
|
||||||
Expr::Width argWidth = arguments[i]->getWidth();
|
Expr::Width argWidth = arguments[i]->getWidth();
|
||||||
if (argWidth > Expr::Int64) {
|
if (argWidth > Expr::Int64) {
|
||||||
@ -75,7 +75,7 @@ index 24e2ed97581f..f40e8bc9deb8 100644
|
|||||||
// Handle the case of 0-sized allocations as 1-byte allocations.
|
// 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
|
// 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
|
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
|
--- a/lib/Module/ModuleUtil.cpp
|
||||||
+++ b/lib/Module/ModuleUtil.cpp
|
+++ b/lib/Module/ModuleUtil.cpp
|
||||||
@@ -196,7 +196,11 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er
|
@@ -196,7 +196,11 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er
|
||||||
@ -91,7 +91,7 @@ index e6d592b135b6..8acada93c2cd 100644
|
|||||||
for (object::Archive::child_iterator AI = archive->child_begin(),
|
for (object::Archive::child_iterator AI = archive->child_begin(),
|
||||||
AE = archive->child_end(); AI != AE; ++AI)
|
AE = archive->child_end(); AI != AE; ++AI)
|
||||||
#else
|
#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;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -100,14 +100,17 @@ index e6d592b135b6..8acada93c2cd 100644
|
|||||||
+ Expected<std::unique_ptr<llvm::object::Binary> > child =
|
+ Expected<std::unique_ptr<llvm::object::Binary> > child =
|
||||||
+ childErr->getAsBinary();
|
+ childErr->getAsBinary();
|
||||||
+ if (!child) {
|
+ if (!child) {
|
||||||
+ ec = errorToErrorCode(child.takeError());
|
+ // I don't know why, but
|
||||||
|
+ // ec = errorToErrorCode(child.takeError())
|
||||||
|
+ // does not work here, so:
|
||||||
+ consumeError(child.takeError());
|
+ consumeError(child.takeError());
|
||||||
|
+ ec = std::make_error_code(std::errc::io_error);
|
||||||
+ }
|
+ }
|
||||||
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
|
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
|
||||||
ErrorOr<std::unique_ptr<llvm::object::Binary> > child =
|
ErrorOr<std::unique_ptr<llvm::object::Binary> > child =
|
||||||
childErr->getAsBinary();
|
childErr->getAsBinary();
|
||||||
ec = child.getError();
|
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 @@ index e6d592b135b6..8acada93c2cd 100644
|
|||||||
|
|
||||||
KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loaded " << archiveModules.size() << " modules\n");
|
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
|
#endif
|
||||||
|
|
||||||
} else if (magic == sys::fs::file_magic::archive) {
|
} else if (magic == sys::fs::file_magic::archive) {
|
||||||
@ -135,7 +138,7 @@ index e6d592b135b6..8acada93c2cd 100644
|
|||||||
ErrorOr<std::unique_ptr<object::Binary> > arch =
|
ErrorOr<std::unique_ptr<object::Binary> > arch =
|
||||||
object::createBinary(Buffer, &Context);
|
object::createBinary(Buffer, &Context);
|
||||||
ec = arch.getError();
|
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)) {
|
if (Function *f = dyn_cast<Function>(v)) {
|
||||||
return f;
|
return f;
|
||||||
} else if (llvm::GlobalAlias *ga = dyn_cast<GlobalAlias>(v)) {
|
} else if (llvm::GlobalAlias *ga = dyn_cast<GlobalAlias>(v)) {
|
||||||
@ -269,10 +272,10 @@ index b8b32e31264a..800cece95e9c 100644
|
|||||||
llvm::cl::ParseCommandLineOptions(argc, argv);
|
llvm::cl::ParseCommandLineOptions(argc, argv);
|
||||||
|
|
||||||
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
|
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
|
--- a/tools/klee/main.cpp
|
||||||
+++ b/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();
|
llvm::InitializeNativeTarget();
|
||||||
|
|
||||||
parseArguments(argc, argv);
|
parseArguments(argc, argv);
|
||||||
@ -285,5 +288,5 @@ index c48570799a7f..d193d8341e93 100644
|
|||||||
if (Watchdog) {
|
if (Watchdog) {
|
||||||
if (MaxTime==0) {
|
if (MaxTime==0) {
|
||||||
--
|
--
|
||||||
2.14.2
|
2.15.0
|
||||||
|
|
||||||
|
105
0007-Add-support-for-modelling-errno_location.patch
Normal file
105
0007-Add-support-for-modelling-errno_location.patch
Normal file
@ -0,0 +1,105 @@
|
|||||||
|
From: Martin Nowack <martin_nowack@tu-dresden.de>
|
||||||
|
Date: Thu, 12 Oct 2017 21:57:03 +0200
|
||||||
|
Subject: Add support for modelling errno_location
|
||||||
|
Patch-mainline: no
|
||||||
|
|
||||||
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
||||||
|
---
|
||||||
|
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
|
||||||
|
|
@ -30,7 +30,7 @@ index 0439431b3bc8..ff76cd53c895 100644
|
|||||||
#include "llvm/IR/LLVMContext.h"
|
#include "llvm/IR/LLVMContext.h"
|
||||||
#include "llvm/IR/Module.h"
|
#include "llvm/IR/Module.h"
|
||||||
diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
|
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
|
--- a/lib/Module/ModuleUtil.cpp
|
||||||
+++ b/lib/Module/ModuleUtil.cpp
|
+++ b/lib/Module/ModuleUtil.cpp
|
||||||
@@ -26,7 +26,9 @@
|
@@ -26,7 +26,9 @@
|
||||||
@ -59,7 +59,7 @@ index 8acada93c2cd..63d3913a08f2 100644
|
|||||||
#include "llvm/Support/raw_ostream.h"
|
#include "llvm/Support/raw_ostream.h"
|
||||||
#include "llvm/Support/Path.h"
|
#include "llvm/Support/Path.h"
|
||||||
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
|
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
|
--- a/tools/klee/main.cpp
|
||||||
+++ b/tools/klee/main.cpp
|
+++ b/tools/klee/main.cpp
|
||||||
@@ -31,7 +31,6 @@
|
@@ -31,7 +31,6 @@
|
||||||
@ -84,5 +84,5 @@ index d193d8341e93..cd54d8aab5af 100644
|
|||||||
#include <signal.h>
|
#include <signal.h>
|
||||||
#include <unistd.h>
|
#include <unistd.h>
|
||||||
--
|
--
|
||||||
2.14.2
|
2.15.0
|
||||||
|
|
||||||
|
42
0008-Cleanup-test-cases.patch
Normal file
42
0008-Cleanup-test-cases.patch
Normal file
@ -0,0 +1,42 @@
|
|||||||
|
From: Martin Nowack <martin_nowack@tu-dresden.de>
|
||||||
|
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 <jirislaby@gmail.com>
|
||||||
|
---
|
||||||
|
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
|
||||||
|
|
@ -9,10 +9,10 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|||||||
1 file changed, 9 insertions(+)
|
1 file changed, 9 insertions(+)
|
||||||
|
|
||||||
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
|
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
|
--- a/lib/Core/Executor.cpp
|
||||||
+++ b/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) {
|
static inline const llvm::fltSemantics * fpWidthToSemantics(unsigned width) {
|
||||||
switch(width) {
|
switch(width) {
|
||||||
@ -35,5 +35,5 @@ index aee0974c7792..08474ae700ac 100644
|
|||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
--
|
--
|
||||||
2.14.2
|
2.15.0
|
||||||
|
|
||||||
|
@ -9,7 +9,7 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|||||||
1 file changed, 41 insertions(+), 9 deletions(-)
|
1 file changed, 41 insertions(+), 9 deletions(-)
|
||||||
|
|
||||||
diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
|
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
|
--- a/lib/Module/ModuleUtil.cpp
|
||||||
+++ b/lib/Module/ModuleUtil.cpp
|
+++ b/lib/Module/ModuleUtil.cpp
|
||||||
@@ -204,7 +204,7 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er
|
@@ -204,7 +204,7 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er
|
||||||
@ -36,7 +36,7 @@ index 63d3913a08f2..e49896a06718 100644
|
|||||||
if (!ec) {
|
if (!ec) {
|
||||||
memberName = memberNameErr.get();
|
memberName = memberNameErr.get();
|
||||||
#else
|
#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
|
#endif
|
||||||
if (ec) {
|
if (ec) {
|
||||||
// If we can't open as a binary object file its hopefully a bitcode file
|
// If we can't open as a binary object file its hopefully a bitcode file
|
||||||
@ -48,7 +48,7 @@ index 63d3913a08f2..e49896a06718 100644
|
|||||||
ErrorOr<MemoryBufferRef> buff = childErr->getMemoryBufferRef();
|
ErrorOr<MemoryBufferRef> buff = childErr->getMemoryBufferRef();
|
||||||
ec = buff.getError();
|
ec = buff.getError();
|
||||||
#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
|
#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;
|
Module *Result = 0;
|
||||||
// FIXME: Maybe load bitcode file lazily? Then if we need to link, materialise the module
|
// FIXME: Maybe load bitcode file lazily? Then if we need to link, materialise the module
|
||||||
#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
|
#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
|
||||||
@ -71,7 +71,7 @@ index 63d3913a08f2..e49896a06718 100644
|
|||||||
if (ec)
|
if (ec)
|
||||||
errorMessage = ec.message();
|
errorMessage = ec.message();
|
||||||
else
|
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)
|
#if LLVM_VERSION_CODE < LLVM_VERSION(3, 8)
|
||||||
Module *Result = 0;
|
Module *Result = 0;
|
||||||
#endif
|
#endif
|
||||||
@ -85,7 +85,7 @@ index 63d3913a08f2..e49896a06718 100644
|
|||||||
#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7)
|
#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7)
|
||||||
ErrorOr<std::unique_ptr<Module> > ResultErr =
|
ErrorOr<std::unique_ptr<Module> > ResultErr =
|
||||||
#else
|
#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;
|
return nullptr;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -111,7 +111,7 @@ index 63d3913a08f2..e49896a06718 100644
|
|||||||
return nullptr;
|
return nullptr;
|
||||||
}
|
}
|
||||||
// The module has taken ownership of the MemoryBuffer so release it
|
// 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;
|
auto module = *errorOrModule;
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
@ -124,5 +124,5 @@ index 63d3913a08f2..e49896a06718 100644
|
|||||||
#else
|
#else
|
||||||
if (auto ec = module->materializeAllPermanently()) {
|
if (auto ec = module->materializeAllPermanently()) {
|
||||||
--
|
--
|
||||||
2.14.2
|
2.15.0
|
||||||
|
|
||||||
|
@ -0,0 +1,35 @@
|
|||||||
|
From: =?UTF-8?q?Julian=20B=C3=BCning?= <julian.buening@rwth-aachen.de>
|
||||||
|
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 <jirislaby@gmail.com>
|
||||||
|
---
|
||||||
|
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
|
||||||
|
|
@ -195,5 +195,5 @@ index da96981079ae..a223b39ada57 100644
|
|||||||
+
|
+
|
||||||
+#endif
|
+#endif
|
||||||
--
|
--
|
||||||
2.14.2
|
2.15.0
|
||||||
|
|
||||||
|
@ -9,8 +9,7 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|||||||
---
|
---
|
||||||
include/klee/util/GetElementPtrTypeIterator.h | 4 ++++
|
include/klee/util/GetElementPtrTypeIterator.h | 4 ++++
|
||||||
lib/Core/Executor.cpp | 22 +++++++++++++++++++---
|
lib/Core/Executor.cpp | 22 +++++++++++++++++++---
|
||||||
lib/Core/ExecutorUtil.cpp | 17 ++++++++++++++---
|
2 files changed, 23 insertions(+), 3 deletions(-)
|
||||||
3 files changed, 37 insertions(+), 6 deletions(-)
|
|
||||||
|
|
||||||
diff --git a/include/klee/util/GetElementPtrTypeIterator.h b/include/klee/util/GetElementPtrTypeIterator.h
|
diff --git a/include/klee/util/GetElementPtrTypeIterator.h b/include/klee/util/GetElementPtrTypeIterator.h
|
||||||
index 5fb9f4ec5c2f..bf7cb6ff0bea 100644
|
index 5fb9f4ec5c2f..bf7cb6ff0bea 100644
|
||||||
@ -28,7 +27,7 @@ index 5fb9f4ec5c2f..bf7cb6ff0bea 100644
|
|||||||
CurTy = 0;
|
CurTy = 0;
|
||||||
}
|
}
|
||||||
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
|
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
|
--- a/lib/Core/Executor.cpp
|
||||||
+++ b/lib/Core/Executor.cpp
|
+++ b/lib/Core/Executor.cpp
|
||||||
@@ -2520,8 +2520,7 @@ void Executor::computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie) {
|
@@ -2520,8 +2520,7 @@ void Executor::computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie) {
|
||||||
@ -67,41 +66,6 @@ index 08474ae700ac..5a88f1ae3180 100644
|
|||||||
index++;
|
index++;
|
||||||
}
|
}
|
||||||
kgepi->offset = constantOffset->getZExtValue();
|
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
|
||||||
|
|
||||||
|
32
0012-llvm40-gep_type_iterator-has-no-operator.patch
Normal file
32
0012-llvm40-gep_type_iterator-has-no-operator.patch
Normal file
@ -0,0 +1,32 @@
|
|||||||
|
From: Jiri Slaby <jirislaby@gmail.com>
|
||||||
|
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 <jirislaby@gmail.com>
|
||||||
|
---
|
||||||
|
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
|
||||||
|
|
123
0013-llvm38-test-change-some-tests.patch
Normal file
123
0013-llvm38-test-change-some-tests.patch
Normal file
@ -0,0 +1,123 @@
|
|||||||
|
From: Jiri Slaby <jirislaby@gmail.com>
|
||||||
|
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 <jirislaby@gmail.com>
|
||||||
|
---
|
||||||
|
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*)
|
||||||
|
+
|
||||||
|
+@.passstr = private constant [5 x i8] c"PASS\00", align 1
|
||||||
|
+@.failstr = 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*)
|
||||||
|
+
|
||||||
|
+@.passstr = private constant [5 x i8] c"PASS\00", align 1
|
||||||
|
+@.failstr = 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
|
||||||
|
|
@ -1,4 +1,4 @@
|
|||||||
<servicedata>
|
<servicedata>
|
||||||
<service name="tar_scm">
|
<service name="tar_scm">
|
||||||
<param name="url">git://github.com/klee/klee.git</param>
|
<param name="url">git://github.com/klee/klee.git</param>
|
||||||
<param name="changesrevision">9f11eababd767b012b623806b40fa0647affa47e</param></service></servicedata>
|
<param name="changesrevision">9caaae0b1b6e52be3c7bb783f3a8be659a1a1869</param></service></servicedata>
|
@ -1,3 +0,0 @@
|
|||||||
version https://git-lfs.github.com/spec/v1
|
|
||||||
oid sha256:ad3ed763f431f001921a8b6bdab69e38de3f0f1e0746af6468b71a478a1dffee
|
|
||||||
size 580524
|
|
3
klee-1.4.0+20171026.tar.xz
Normal file
3
klee-1.4.0+20171026.tar.xz
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
version https://git-lfs.github.com/spec/v1
|
||||||
|
oid sha256:a4a0830328c4cbac4f059a7fa016994df5101b5b9a30105fdf9cc42e5c14169e
|
||||||
|
size 582380
|
29
klee.changes
29
klee.changes
@ -1,3 +1,32 @@
|
|||||||
|
-------------------------------------------------------------------
|
||||||
|
Fri Nov 17 17:01:38 UTC 2017 - jslaby@suse.com
|
||||||
|
|
||||||
|
- 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
|
||||||
|
|
||||||
-------------------------------------------------------------------
|
-------------------------------------------------------------------
|
||||||
Tue Oct 10 12:45:08 UTC 2017 - jslaby@suse.com
|
Tue Oct 10 12:45:08 UTC 2017 - jslaby@suse.com
|
||||||
|
|
||||||
|
51
klee.spec
51
klee.spec
@ -19,7 +19,7 @@
|
|||||||
%define llvm_version_minor 0
|
%define llvm_version_minor 0
|
||||||
%define llvm_version %{llvm_version_major}
|
%define llvm_version %{llvm_version_major}
|
||||||
|
|
||||||
%define version_unconverted 1.4.0+20171009
|
%define version_unconverted 1.4.0+20171026
|
||||||
|
|
||||||
%ifarch %{ix86} x86_64
|
%ifarch %{ix86} x86_64
|
||||||
%define with_uclibc 1
|
%define with_uclibc 1
|
||||||
@ -31,26 +31,36 @@ Name: klee
|
|||||||
Summary: LLVM Execution Engine
|
Summary: LLVM Execution Engine
|
||||||
License: NCSA
|
License: NCSA
|
||||||
Group: Development/Languages/Other
|
Group: Development/Languages/Other
|
||||||
Version: 1.4.0+20171009
|
Version: 1.4.0+20171026
|
||||||
Release: 0
|
Release: 0
|
||||||
Url: http://klee.github.io/
|
Url: http://klee.github.io/
|
||||||
Source0: %{name}-%{version}.tar.xz
|
Source0: %{name}-%{version}.tar.xz
|
||||||
Source1: %{name}-rpmlintrc
|
Source1: %{name}-rpmlintrc
|
||||||
Source2: https://raw.githubusercontent.com/llvm-mirror/llvm/release_%{llvm_version_major}%{llvm_version_minor}/utils/not/not.cpp
|
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
|
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-Fix-generation-of-expressions-from-constant-sequenti.patch
|
||||||
Patch1: 0001-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch
|
Patch2: 0002-Fix-getelementptr-for-array-or-vector-indices.patch
|
||||||
Patch2: 0002-llvm-make-KLEE-compile-against-LLVM-3.7.patch
|
Patch3: 0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch
|
||||||
Patch3: 0003-test-add-versions-of-some-tests-for-LLVM-3.7.patch
|
Patch4: 0004-Provide-errno-independent-of-CTYPE_EXTERNALS-being-d.patch
|
||||||
Patch4: 0004-llvm37-handle-getRegisteredOptions.patch
|
Patch5: 0005-Track-errno-correctly.patch
|
||||||
Patch5: 0005-llvm-make-KLEE-compile-against-LLVM-3.8.patch
|
Patch6: 0006-Declare-klee_get_errno-and-remove-local-declarations.patch
|
||||||
Patch6: 0006-llvm-make-KLEE-compile-against-LLVM-3.9.patch
|
Patch7: 0007-Add-support-for-modelling-errno_location.patch
|
||||||
Patch7: 0007-llvm40-handle-different-header-names.patch
|
Patch8: 0008-Cleanup-test-cases.patch
|
||||||
Patch8: 0008-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch
|
Patch9: 0009-test-fix-Feature-BFSSearcherAndDFSSearcherInterleave.patch
|
||||||
Patch9: 0009-llvm40-errorOr-and-similar.patch
|
#---
|
||||||
Patch10: 0010-llvm-use-chrono-helpers-from-LLVM-4.0.patch
|
Patch10: 0001-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch
|
||||||
Patch11: 0011-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch
|
Patch11: 0002-llvm-make-KLEE-compile-against-LLVM-3.7.patch
|
||||||
Patch14: 0001-test-DirSeek-make-it-XFAIL-temporarily.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: clang%{llvm_version}
|
||||||
BuildRequires: cmake
|
BuildRequires: cmake
|
||||||
@ -76,7 +86,6 @@ information on what KLEE is and what it can do, see the OSDI 2008 paper.
|
|||||||
|
|
||||||
%prep
|
%prep
|
||||||
%setup -q
|
%setup -q
|
||||||
%patch0 -p1
|
|
||||||
%patch1 -p1
|
%patch1 -p1
|
||||||
%patch2 -p1
|
%patch2 -p1
|
||||||
%patch3 -p1
|
%patch3 -p1
|
||||||
@ -88,7 +97,17 @@ information on what KLEE is and what it can do, see the OSDI 2008 paper.
|
|||||||
%patch9 -p1
|
%patch9 -p1
|
||||||
%patch10 -p1
|
%patch10 -p1
|
||||||
%patch11 -p1
|
%patch11 -p1
|
||||||
|
%patch12 -p1
|
||||||
|
%patch13 -p1
|
||||||
%patch14 -p1
|
%patch14 -p1
|
||||||
|
%patch15 -p1
|
||||||
|
%patch16 -p1
|
||||||
|
%patch17 -p1
|
||||||
|
%patch18 -p1
|
||||||
|
%patch19 -p1
|
||||||
|
%patch20 -p1
|
||||||
|
%patch21 -p1
|
||||||
|
%patch22 -p1
|
||||||
mkdir -p build/test/
|
mkdir -p build/test/
|
||||||
cp %{SOURCE2} build/test/
|
cp %{SOURCE2} build/test/
|
||||||
cp %{SOURCE3} build/test/
|
cp %{SOURCE3} build/test/
|
||||||
|
Loading…
x
Reference in New Issue
Block a user