pool/klee
SHA256
4
0
Fork 1
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

up to 1.4.0+20180518

Browse Source 
OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/klee?expand=0&rev=42
This commit is contained in:
Jiri Slaby 2018-05-21 09:40:31 +00:00 committed by Git OBS Bridge
parent 9596527f6a
commit c5fd26f59f
36 changed files with 396 additions and 839 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
0001-Fix-generation-of-expressions-from-constant-sequenti.patch
View File

@ -1,31 +0,0 @@
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.1

36
0001-MergeHandler-remove-unused-closedStateCount.patch
View File

@ -1,36 +0,0 @@
From: Jiri Slaby <jirislaby@gmail.com>
Date: Mon, 15 Jan 2018 09:20:32 +0100
Subject: MergeHandler: remove unused closedStateCount
Patch-mainline: no
clang 5 reports:
In file included from ../lib/Core/MergeHandler.cpp:10:
../include/klee/MergeHandler.h:81:12: warning: private field 'closedStateCount' is not used [-Wunused-private-field]
unsigned closedStateCount;
^
So fix it by removing the member.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
---
include/klee/MergeHandler.h | 4 ----
1 file changed, 4 deletions(-)
diff --git a/include/klee/MergeHandler.h b/include/klee/MergeHandler.h
index d374e1684036..0c596825e867 100644
--- a/include/klee/MergeHandler.h
+++ b/include/klee/MergeHandler.h
@@ -76,10 +76,6 @@ class MergeHandler {
private:
Executor *executor;
- /// @brief Number of states that are tracked by this MergeHandler, that ran
- /// into a relevant klee_close_merge
- unsigned closedStateCount;
-
/// @brief Mapping the different 'klee_close_merge' calls to the states that ran into
/// them
std::map<llvm::Instruction *, std::vector<ExecutionState *> >
--
2.15.1

8
0001-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch
View File

@ -32,10 +32,10 @@ index ccf54ae13092..532051602fe3 100644
# define KLEE_LLVM_CL_VAL_END
#else
diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
index 28546915b539..3558049d87cc 100644
index 70c14050e8e7..72b866cf6395 100644
--- a/lib/Core/ExternalDispatcher.cpp
+++ b/lib/Core/ExternalDispatcher.cpp
@@ -324,6 +324,7 @@ Function *ExternalDispatcherImpl::createDispatcher(Function *target,
@@ -326,6 +326,7 @@ Function *ExternalDispatcherImpl::createDispatcher(Function *target,
Type *argTy =
(i < FTy->getNumParams() ? FTy->getParamType(i) : (*ai)->getType());
Instruction *argI64p = GetElementPtrInst::Create(
@ -44,7 +44,7 @@ index 28546915b539..3558049d87cc 100644
Instruction *argp =
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index b02605208bbb..54bda16013b6 100644
index 10b5df0864f0..4846b4ce72b3 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -82,11 +82,15 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
@ -68,5 +68,5 @@ index b02605208bbb..54bda16013b6 100644
}
ii->removeFromParent();
--
2.15.1
2.16.3

100
0002-Fix-getelementptr-for-array-or-vector-indices.patch
View File

@ -1,100 +0,0 @@
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.1

4
0002-llvm-make-KLEE-compile-against-LLVM-3.7.patch
View File

@ -161,7 +161,7 @@ index 13e4f7d47e58..c597fa2a7b82 100644
TLI = TM->getSubtargetImpl()->getTargetLowering();
#else
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 9bdf06f600ce..ea24d89c5aaf 100644
index 44bc5407e9c8..ab9dfe286ffb 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -35,6 +35,7 @@
@ -173,5 +173,5 @@ index 9bdf06f600ce..ea24d89c5aaf 100644
#include "llvm/Support/TargetSelect.h"
--
2.15.1
2.16.3

44
0002-llvm50-use-auto-variable-instead-of-SwitchInst-CaseI.patch
View File

@ -1,44 +0,0 @@
From: Jiri Slaby <jirislaby@gmail.com>
Date: Mon, 15 Jan 2018 10:24:48 +0100
Subject: llvm50: use auto variable instead of SwitchInst::CaseIt
Patch-mainline: no
llvm50 changed the semantics of SwitchInst::CaseIt and started using
"auto" variable type. So use it here too for all versions.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
---
lib/Core/Executor.cpp | 3 +--
lib/Module/LowerSwitch.cpp | 2 +-
2 files changed, 2 insertions(+), 3 deletions(-)
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index be92b16a459d..d836598927ce 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1553,8 +1553,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
std::map<ref<Expr>, BasicBlock *> expressionOrder;
// Iterate through all non-default cases and order them by expressions
- for (SwitchInst::CaseIt i = si->case_begin(), e = si->case_end(); i != e;
- ++i) {
+ for (auto i : si->cases()) {
ref<Expr> value = evalConstant(i.getCaseValue());
BasicBlock *caseSuccessor = i.getCaseSuccessor();
diff --git a/lib/Module/LowerSwitch.cpp b/lib/Module/LowerSwitch.cpp
index 1a194245a09a..02f00a3ae94e 100644
--- a/lib/Module/LowerSwitch.cpp
+++ b/lib/Module/LowerSwitch.cpp
@@ -115,7 +115,7 @@ void LowerSwitchPass::processSwitchInst(SwitchInst *SI) {
CaseVector cases;
- for (SwitchInst::CaseIt i = SI->case_begin(), e = SI->case_end(); i != e; ++i)
+ for (auto i : SI->cases())
cases.push_back(SwitchCase(i.getCaseValue(),
i.getCaseSuccessor()));
--
2.15.1

52
0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch
View File

@ -1,52 +0,0 @@
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 d836598927ce..fd1da6478fb2 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2391,15 +2391,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());
@@ -2429,12 +2425,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.1

303
0003-test-add-versions-of-some-tests-for-LLVM-3.7.patch
View File

@ -9,46 +9,54 @@ Clone some tests to have their 3.7 version. 'call's, 'load's and
@andreamattavelli: Fixed test cases: BitCastAlias test cases included
modification to alias specifications that require LLVM 3.8
[v2] added comments what was changed and why
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
---
test/Concrete/BoolReadWrite.ll | 1 +
test/Concrete/BoolReadWrite.llvm37.ll | 16 +
test/Concrete/BoolReadWrite.llvm37.ll | 17 +
test/Concrete/ConstantExpr.ll | 1 +
test/Concrete/ConstantExpr.llvm37.ll | 165 +++++
test/Concrete/ConstantExpr.llvm37.ll | 167 +++++
test/Concrete/ConstantInit.ll | 1 +
test/Concrete/ConstantInit.llvm37.ll | 62 ++
test/Concrete/FloatingPointOps.ll | 1 +
test/Concrete/FloatingPointOps.llvm37.ll | 680 +++++++++++++++++++++
test/Concrete/FloatingPointOps.llvm37.ll | 681 +++++++++++++++++++++
test/Concrete/GlobalInitializers.ll | 1 +
test/Concrete/GlobalInitializers.llvm37.ll | 48 ++
test/Concrete/GlobalInitializers.llvm37.ll | 50 ++
test/Concrete/SimpleStoreAndLoad.ll | 1 +
test/Concrete/SimpleStoreAndLoad.llvm37.ll | 20 +
test/Concrete/SimpleStoreAndLoad.llvm37.ll | 22 +
test/Feature/BitcastAlias.ll | 1 +
test/Feature/BitcastAlias.llvm37.ll | 35 ++
test/Feature/BitcastAlias.llvm37.ll | 37 ++
test/Feature/BitcastAliasMD2U.ll | 1 +
test/Feature/BitcastAliasMD2U.llvm37.ll | 35 ++
test/Feature/BitcastAliasMD2U.llvm37.ll | 37 ++
test/Feature/ConstantArray.ll | 3 +-
test/Feature/ConstantArray.llvm37.ll | 55 ++
test/Feature/ConstantStruct.ll | 1 +
test/Feature/ConstantStruct.llvm37.ll | 34 ++
test/Feature/ConstantStruct.llvm37.ll | 35 ++
test/Feature/GetElementPtr.ll | 1 +
test/Feature/GetElementPtr.llvm37.ll | 30 +
test/Feature/GetElementPtr.llvm37.ll | 31 +
test/Feature/InsertExtractValue.ll | 1 +
test/Feature/InsertExtractValue.llvm37.ll | 34 ++
test/Feature/InsertExtractValue.llvm37.ll | 35 ++
test/Feature/Overflow.ll | 1 +
test/Feature/Overflow.llvm37.ll | 45 ++
test/Feature/Overflow.llvm37.ll | 46 ++
test/Feature/OverflowMul.ll | 1 +
test/Feature/OverflowMul.llvm37.ll | 45 ++
test/Feature/_utils.llvm37._ll | 71 +++
test/Feature/OverflowMul.llvm37.ll | 46 ++
test/Feature/_utils.llvm37._ll | 74 +++
test/Intrinsics/objectsize.ll | 1 +
test/Intrinsics/objectsize.llvm37.ll | 36 ++
test/Intrinsics/objectsize.llvm37.ll | 37 ++
test/lit.cfg | 2 +-
.../regression/2007-08-16-invalid-constant-value.c | 1 +
.../2007-08-16-invalid-constant-value.llvm37.c | 33 +
30 files changed, 1342 insertions(+), 1 deletion(-)
34 files changed, 1483 insertions(+), 2 deletions(-)
create mode 100644 test/Concrete/BoolReadWrite.llvm37.ll
create mode 100644 test/Concrete/ConstantExpr.llvm37.ll
create mode 100644 test/Concrete/ConstantInit.llvm37.ll
create mode 100644 test/Concrete/FloatingPointOps.llvm37.ll
create mode 100755 test/Concrete/GlobalInitializers.llvm37.ll
create mode 100644 test/Concrete/SimpleStoreAndLoad.llvm37.ll
create mode 100644 test/Feature/BitcastAlias.llvm37.ll
create mode 100644 test/Feature/BitcastAliasMD2U.llvm37.ll
create mode 100644 test/Feature/ConstantArray.llvm37.ll
create mode 100644 test/Feature/ConstantStruct.llvm37.ll
create mode 100644 test/Feature/GetElementPtr.llvm37.ll
create mode 100644 test/Feature/InsertExtractValue.llvm37.ll
@ -69,10 +77,11 @@ index f818ecafacd5..34a50447db99 100644
declare void @print_i1(i1)
diff --git a/test/Concrete/BoolReadWrite.llvm37.ll b/test/Concrete/BoolReadWrite.llvm37.ll
new file mode 100644
index 000000000000..9141987e97a0
index 000000000000..4dfb49e01d0b
--- /dev/null
+++ b/test/Concrete/BoolReadWrite.llvm37.ll
@@ -0,0 +1,16 @@
@@ -0,0 +1,17 @@
+; LLVM 3.7 requires a type as the first argument to 'load'
+; REQUIRES: geq-llvm-3.7
+; RUN: %S/ConcreteTest.py --klee='%klee' --lli=%lli %s
+
@ -100,10 +109,11 @@ index d00c59a637e9..2d8e5bc65721 100644
; Most of the test below use the *address* of gInt as part of their computation,
diff --git a/test/Concrete/ConstantExpr.llvm37.ll b/test/Concrete/ConstantExpr.llvm37.ll
new file mode 100644
index 000000000000..fa634c497a4b
index 000000000000..38577f7056ef
--- /dev/null
+++ b/test/Concrete/ConstantExpr.llvm37.ll
@@ -0,0 +1,165 @@
@@ -0,0 +1,167 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; REQUIRES: geq-llvm-3.7
+; RUN: %S/ConcreteTest.py --klee='%klee' --lli=%lli %s
+
@ -152,13 +162,14 @@ index 000000000000..fa634c497a4b
+ call void @print_i32(i32 %t1)
+ call void @print_i32(i32 %t2)
+ call void @print_i32(i32 %t3)
+
+ ; or the address with 1 to ensure the addresses will differ in 'ne' below
+ %t4 = shl i64 lshr(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8
+ %t5 = shl i64 ashr(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8
+ %t6 = lshr i64 shl(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8
+
+ %t4 = shl i32 lshr(i32 ptrtoint(i32* @gInt to i32), i32 8), 8
+ %t5 = shl i32 ashr(i32 ptrtoint(i32* @gInt to i32), i32 8), 8
+ %t6 = lshr i32 shl(i32 ptrtoint(i32* @gInt to i32), i32 8), 8
+
+ %t7 = icmp eq i32 %t4, %t5
+ %t8 = icmp ne i32 %t4, %t6
+ %t7 = icmp eq i64 %t4, %t5
+ %t8 = icmp ne i64 %t4, %t6
+
+ %t9 = zext i1 %t7 to i8
+ %t10 = zext i1 %t8 to i8
@ -269,6 +280,83 @@ index 000000000000..fa634c497a4b
+declare void @print_i16(i16)
+declare void @print_i32(i32)
+declare void @print_i64(i64)
diff --git a/test/Concrete/ConstantInit.ll b/test/Concrete/ConstantInit.ll
index 2127d27bce7a..44f852120f35 100644
--- a/test/Concrete/ConstantInit.ll
+++ b/test/Concrete/ConstantInit.ll
@@ -1,3 +1,4 @@
+; REQUIRES: lt-llvm-3.7
; RUN: %S/ConcreteTest.py --klee='%klee' --lli=%lli %s
%struct.dirent = type { i64, i64, i16, i8 }
diff --git a/test/Concrete/ConstantInit.llvm37.ll b/test/Concrete/ConstantInit.llvm37.ll
new file mode 100644
index 000000000000..c30b7f093301
--- /dev/null
+++ b/test/Concrete/ConstantInit.llvm37.ll
@@ -0,0 +1,62 @@
+; LLVM 3.7 requires a type as the first argument to 'load'
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; REQUIRES: geq-llvm-3.7
+; RUN: %S/ConcreteTest.py --klee='%klee' --lli=%lli %s
+
+%struct.dirent = type { i64, i64, i16, i8 }
+declare void @print_i64(i64)
+
+define void @test_constant_vector_simple() {
+ entry:
+ %a = alloca %struct.dirent
+ %tmp1 = getelementptr %struct.dirent, %struct.dirent* %a, i32 0
+ %tmp2 = bitcast %struct.dirent* %tmp1 to <2 x i64>*
+ ; Initialize with constant vector parsed as ConstantDataSequential
+ store <2 x i64> <i64 0, i64 4096>, <2 x i64>* %tmp2, align 8
+
+ br label %exit
+exit:
+ ; Print first initialized element
+ %idx = getelementptr %struct.dirent, %struct.dirent* %a, i32 0, i32 0
+ %val = load i64, i64* %idx
+ call void @print_i64(i64 %val)
+
+ ; Print second initialized element
+ %idx2 = getelementptr %struct.dirent, %struct.dirent* %a, i32 0, i32 1
+ %val2 = load i64, i64* %idx2
+ call void @print_i64(i64 %val2)
+ ret void
+}
+
+define void @test_constant_vector_complex() {
+entry:
+ ; Create a vector using an uncommon type: i1024: Force usage of constant vector
+ %a = alloca <2 x i1024>
+ store <2 x i1024> <i1024 5, i1024 1024>, <2 x i1024>* %a, align 8
+
+ br label %exit
+exit:
+ ; Print first initialized element
+ %idx = getelementptr <2 x i1024>, <2 x i1024>* %a, i32 0, i32 0
+ %narrow = bitcast i1024* %idx to i64*
+ %val = load i64, i64* %narrow
+ call void @print_i64(i64 %val)
+
+ ; Print second initialized element
+ %idx2 = getelementptr <2 x i1024>, <2 x i1024>* %a, i32 0, i32 1
+ %narrow2 = bitcast i1024* %idx2 to i64*
+ %val2 = load i64, i64* %narrow2
+ call void @print_i64(i64 %val2)
+
+ ret void
+}
+
+define i32 @main() {
+entry:
+ call void @test_constant_vector_simple()
+ call void @test_constant_vector_complex()
+
+ br label %exit
+exit:
+ ret i32 0
+}
diff --git a/test/Concrete/FloatingPointOps.ll b/test/Concrete/FloatingPointOps.ll
index 00d4e877b562..b81a3b8df1f4 100644
--- a/test/Concrete/FloatingPointOps.ll
@ -280,10 +368,13 @@ index 00d4e877b562..b81a3b8df1f4 100644
; casting error messages
diff --git a/test/Concrete/FloatingPointOps.llvm37.ll b/test/Concrete/FloatingPointOps.llvm37.ll
new file mode 100644
index 000000000000..3e21f0f12408
index 000000000000..4c96e3363eb0
--- /dev/null
+++ b/test/Concrete/FloatingPointOps.llvm37.ll
@@ -0,0 +1,680 @@
@@ -0,0 +1,681 @@
+; LLVM 3.7 requires a type as the first argument to 'load'
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; LLVM 3.7 no longer accepts '*' with a 'call'
+; REQUIRES: geq-llvm-3.7
+; RUN: %S/ConcreteTest.py --klee='%klee' --lli=%lli %s
+
@ -929,18 +1020,16 @@ index 000000000000..3e21f0f12408
+ %nan1 = load double, double* %nan
+ %nan2 = load double, double* %nan
+
+ ; Warning: NaN comparisons with normal operators is BROKEN in LLVM JIT v2.0. Fixed in v2.1.
+ ; FIXME: Just check against 2.9 and the Unordered checks work, but the ordered ones do not. Should be investigated.
+ ; NaNs do different things depending on ordered vs unordered
+; call void @testFCmpBothOrdered( double %nan1, double 0.000000e+00, i1 0, i1 0, i1 0, i1 0, i1 0, i1 0, i1 0 )
+; call void @testFCmpBothOrdered( double %nan1, double %nan2, i1 0, i1 0, i1 0, i1 0, i1 0, i1 0, i1 0 )
+; call void @testFCmpBothUnordered( double %nan1, double 0.000000e+00, i1 1, i1 1, i1 1, i1 1, i1 1, i1 1, i1 1 )
+; call void @testFCmpBothUnordered( double %nan1, double %nan2, i1 1, i1 1, i1 1, i1 1, i1 1, i1 1, i1 1 )
+ call void @testFCmpBothOrdered( double %nan1, double 0.000000e+00, i1 0, i1 0, i1 0, i1 0, i1 0, i1 0, i1 0 )
+ call void @testFCmpBothOrdered( double %nan1, double %nan2, i1 0, i1 0, i1 0, i1 0, i1 0, i1 0, i1 0 )
+ call void @testFCmpBothUnordered( double %nan1, double 0.000000e+00, i1 1, i1 1, i1 1, i1 1, i1 1, i1 1, i1 1 )
+ call void @testFCmpBothUnordered( double %nan1, double %nan2, i1 1, i1 1, i1 1, i1 1, i1 1, i1 1, i1 1 )
+
+ ret void
+}
+
+; tes all floating point instructions
+; test all floating point instructions
+define i32 @main() {
+entry:
+ call void @testFPTrunc( )
@ -975,10 +1064,12 @@ index e3657dad19e5..ba7e53eb7cd7 100755
declare void @print_i32(i32)
diff --git a/test/Concrete/GlobalInitializers.llvm37.ll b/test/Concrete/GlobalInitializers.llvm37.ll
new file mode 100755
index 000000000000..2303a6974712
index 000000000000..57e702dcdca9
--- /dev/null
+++ b/test/Concrete/GlobalInitializers.llvm37.ll
@@ -0,0 +1,48 @@
@@ -0,0 +1,50 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; LLVM 3.7 requires a type as the first argument to 'load'
+; REQUIRES: geq-llvm-3.7
+; RUN: %S/ConcreteTest.py --klee='%klee' --lli=%lli %s
+
@ -1038,10 +1129,12 @@ index 1edad0386916..7bb65ea7dfc9 100644
declare void @print_i32(i32)
diff --git a/test/Concrete/SimpleStoreAndLoad.llvm37.ll b/test/Concrete/SimpleStoreAndLoad.llvm37.ll
new file mode 100644
index 000000000000..bd081a4a2bcc
index 000000000000..951a474ee297
--- /dev/null
+++ b/test/Concrete/SimpleStoreAndLoad.llvm37.ll
@@ -0,0 +1,20 @@
@@ -0,0 +1,22 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; LLVM 3.7 requires a type as the first argument to 'load'
+; REQUIRES: geq-llvm-3.7
+; RUN: %S/ConcreteTest.py --klee='%klee' --lli=%lli %s
+
@ -1073,10 +1166,12 @@ index e0e3653feebc..d203e52c4bcb 100644
; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
diff --git a/test/Feature/BitcastAlias.llvm37.ll b/test/Feature/BitcastAlias.llvm37.ll
new file mode 100644
index 000000000000..0d6e72604d6b
index 000000000000..5bd301936e13
--- /dev/null
+++ b/test/Feature/BitcastAlias.llvm37.ll
@@ -0,0 +1,35 @@
@@ -0,0 +1,37 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; LLVM 3.7 no longer accepts '*' with a 'call'
+; REQUIRES: geq-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
@ -1123,10 +1218,12 @@ index 24eabaa57c8c..cef8ac5459ca 100644
; RUN: %klee --output-dir=%t.klee-out -disable-opt -search=nurs:md2u %t1.bc > %t2
diff --git a/test/Feature/BitcastAliasMD2U.llvm37.ll b/test/Feature/BitcastAliasMD2U.llvm37.ll
new file mode 100644
index 000000000000..12abf09373f8
index 000000000000..7eddd3d6a01c
--- /dev/null
+++ b/test/Feature/BitcastAliasMD2U.llvm37.ll
@@ -0,0 +1,35 @@
@@ -0,0 +1,37 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; LLVM 3.7 no longer accepts '*' with a 'call'
+; REQUIRES: geq-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
@ -1162,6 +1259,83 @@ index 000000000000..12abf09373f8
+ %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/ConstantArray.ll b/test/Feature/ConstantArray.ll
index 161b2a167610..a4986ff4bc7f 100644
--- a/test/Feature/ConstantArray.ll
+++ b/test/Feature/ConstantArray.ll
@@ -1,3 +1,4 @@
+; REQUIRES: lt-llvm-3.7
; 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 2>&1 | FileCheck %s
@@ -48,4 +49,4 @@ exit:
; CHECK: 1:9
ret i32 0
-}
\ No newline at end of file
+}
diff --git a/test/Feature/ConstantArray.llvm37.ll b/test/Feature/ConstantArray.llvm37.ll
new file mode 100644
index 000000000000..195b4cb014e4
--- /dev/null
+++ b/test/Feature/ConstantArray.llvm37.ll
@@ -0,0 +1,55 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; LLVM 3.7 requires a type as the first argument to 'load'
+; LLVM 3.7 no longer accepts '*' with a 'call'
+; REQUIRES: geq-llvm-3.7
+; 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 2>&1 | FileCheck %s
+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-S128"
+target triple = "x86_64-unknown-linux-gnu"
+
+@.str = private unnamed_addr constant [2 x i8] c"0\00", align 1
+@.str2 = private unnamed_addr constant [2 x i8] c"1\00", align 1
+
+%struct.dirent = type { i32, i32, i16, i8 }
+declare void @klee_print_expr(i8*, ...)
+
+define i32 @main() {
+entry:
+ %a = alloca %struct.dirent
+ %tmp1 = getelementptr %struct.dirent, %struct.dirent* %a, i32 0
+ %tmp2 = bitcast %struct.dirent* %tmp1 to <2 x i32>*
+ ; Initialize with constant vector
+ store <2 x i32> <i32 42, i32 4096>, <2 x i32>* %tmp2
+ br label %exit
+exit:
+ ; Print first initialized element
+ %idx = getelementptr %struct.dirent, %struct.dirent* %a, i32 0, i32 0
+ %val = load i32, i32* %idx
+ call void(i8*, ...) @klee_print_expr(i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str, i32 0, i32 0), i32 %val)
+ ; CHECK: 0:42
+
+ ; Print second initialized element
+ %idx2 = getelementptr %struct.dirent, %struct.dirent* %a, i32 0, i32 1
+ %val2 = load i32, i32* %idx2
+ call void(i8*, ...) @klee_print_expr(i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str2, i32 0, i32 0), i32 %val2)
+ ; CHECK: 1:4096
+
+ ; Initialize with constant array
+ %array = alloca [2 x i32];
+ store [2 x i32][i32 7, i32 9], [2 x i32]* %array
+
+ ; Print first initialized element
+ %idx3 = getelementptr [2 x i32], [2 x i32]* %array, i32 0, i32 0
+ %val3 = load i32, i32* %idx3
+ call void(i8*, ...) @klee_print_expr(i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str, i32 0, i32 0), i32 %val3)
+ ; CHECK: 0:7
+
+ ; Print second initialized element
+ %idx4 = getelementptr [2 x i32], [2 x i32]* %array, i32 0, i32 1
+ %val4 = load i32, i32* %idx4
+ call void(i8*, ...) @klee_print_expr(i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str2, i32 0, i32 0), i32 %val4)
+ ; CHECK: 1:9
+
+ ret i32 0
+}
diff --git a/test/Feature/ConstantStruct.ll b/test/Feature/ConstantStruct.ll
index 4fe6b5d0e041..073544d38d2f 100644
--- a/test/Feature/ConstantStruct.ll
@ -1173,10 +1347,11 @@ index 4fe6b5d0e041..073544d38d2f 100644
; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
diff --git a/test/Feature/ConstantStruct.llvm37.ll b/test/Feature/ConstantStruct.llvm37.ll
new file mode 100644
index 000000000000..802dfbf74f6e
index 000000000000..e4b3d07bdc08
--- /dev/null
+++ b/test/Feature/ConstantStruct.llvm37.ll
@@ -0,0 +1,34 @@
@@ -0,0 +1,35 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; REQUIRES: geq-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
@ -1222,10 +1397,11 @@ index da94441c685e..43f33e27aaf1 100644
; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
diff --git a/test/Feature/GetElementPtr.llvm37.ll b/test/Feature/GetElementPtr.llvm37.ll
new file mode 100644
index 000000000000..b4c3ea445729
index 000000000000..f7f8aada8dc5
--- /dev/null
+++ b/test/Feature/GetElementPtr.llvm37.ll
@@ -0,0 +1,30 @@
@@ -0,0 +1,31 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; REQUIRES: geq-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
@ -1267,10 +1443,11 @@ index 83e8f851ccea..431e14c4225a 100644
; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
diff --git a/test/Feature/InsertExtractValue.llvm37.ll b/test/Feature/InsertExtractValue.llvm37.ll
new file mode 100644
index 000000000000..16dcfd9d0002
index 000000000000..fff6da7cd07a
--- /dev/null
+++ b/test/Feature/InsertExtractValue.llvm37.ll
@@ -0,0 +1,34 @@
@@ -0,0 +1,35 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; REQUIRES: geq-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
@ -1316,10 +1493,11 @@ index 35dfbd10fe02..2ab047727817 100644
; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
diff --git a/test/Feature/Overflow.llvm37.ll b/test/Feature/Overflow.llvm37.ll
new file mode 100644
index 000000000000..80313a777149
index 000000000000..1dbe12168ed2
--- /dev/null
+++ b/test/Feature/Overflow.llvm37.ll
@@ -0,0 +1,45 @@
@@ -0,0 +1,46 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; REQUIRES: geq-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
@ -1376,10 +1554,11 @@ index 7026aa74bfbe..1b14d3806cf6 100644
; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
diff --git a/test/Feature/OverflowMul.llvm37.ll b/test/Feature/OverflowMul.llvm37.ll
new file mode 100644
index 000000000000..8dd93778728a
index 000000000000..3173e43c271c
--- /dev/null
+++ b/test/Feature/OverflowMul.llvm37.ll
@@ -0,0 +1,45 @@
@@ -0,0 +1,46 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; REQUIRES: geq-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
@ -1427,10 +1606,13 @@ index 000000000000..8dd93778728a
+}
diff --git a/test/Feature/_utils.llvm37._ll b/test/Feature/_utils.llvm37._ll
new file mode 100644
index 000000000000..7114daabb6c2
index 000000000000..d825df3a7bcf
--- /dev/null
+++ b/test/Feature/_utils.llvm37._ll
@@ -0,0 +1,71 @@
@@ -0,0 +1,74 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; LLVM 3.7 requires a type as the first argument to 'load'
+
+define i32 @util_make_and_i1(i32 %a, i32 %b) {
+ %a_i1 = icmp ne i32 %a, 0
+ %b_i1 = icmp ne i32 %b, 0
@ -1513,13 +1695,14 @@ index 4bb59596ad2f..7ad4b6fc4fad 100644
; RUN: %klee -exit-on-error --output-dir=%t.klee-out -disable-opt %t.bc
diff --git a/test/Intrinsics/objectsize.llvm37.ll b/test/Intrinsics/objectsize.llvm37.ll
new file mode 100644
index 000000000000..ba3e706a301a
index 000000000000..3a111f99c619
--- /dev/null
+++ b/test/Intrinsics/objectsize.llvm37.ll
@@ -0,0 +1,36 @@
@@ -0,0 +1,37 @@
+; Unfortunately LLVM 2.9 has a different suffix for the ``llvm.objectsize`` instrinsic
+; so this LLVM IR fails to verify for that version.
+;
+; LLVM 3.7 requires a type as the first argument to 'load'
+; REQUIRES: geq-llvm-3.7
+; RUN: %llvmas %s -o=%t.bc
+; RUN: rm -rf %t.klee-out
@ -1567,7 +1750,7 @@ index 00b429b697a5..e570f9b227e3 100644
config.llvm_version_minor)
config.available_features.add("llvm-" + current_llvm_version)
diff --git a/test/regression/2007-08-16-invalid-constant-value.c b/test/regression/2007-08-16-invalid-constant-value.c
index e0b304f40b01..73fe8689d53c 100644
index 5b17e68b5412..53014f97827c 100644
--- a/test/regression/2007-08-16-invalid-constant-value.c
+++ b/test/regression/2007-08-16-invalid-constant-value.c
@@ -1,3 +1,4 @@
@ -1577,7 +1760,7 @@ index e0b304f40b01..73fe8689d53c 100644
// RUN: llvm-as -f %p/../Feature/_utils._ll -o %t2.bc
diff --git a/test/regression/2007-08-16-invalid-constant-value.llvm37.c b/test/regression/2007-08-16-invalid-constant-value.llvm37.c
new file mode 100644
index 000000000000..aa6b42ed6b9f
index 000000000000..f2c1f9c4bb2c
--- /dev/null
+++ b/test/regression/2007-08-16-invalid-constant-value.llvm37.c
@@ -0,0 +1,33 @@
@ -1596,7 +1779,7 @@ index 000000000000..aa6b42ed6b9f
+int main() {
+ unsigned char a;
+
+ klee_make_symbolic(&a, sizeof a);
+ klee_make_symbolic(&a, sizeof a, "a");
+
+ // demand was firing here because an invalid constant
+ // value was being created when implied value did not
@ -1615,5 +1798,5 @@ index 000000000000..aa6b42ed6b9f
+ return 0;
+}
--
2.15.1
2.16.3

43
0004-Provide-errno-independent-of-CTYPE_EXTERNALS-being-d.patch
View File

@ -1,43 +0,0 @@
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 fd1da6478fb2..efc59008e542 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.1

2
0004-llvm37-handle-getRegisteredOptions.patch
View File

@ -29,5 +29,5 @@ index aaba72f4b5b7..3c117db9fa7b 100644
i++) {
if (i->second->Category != &Category) {
--
2.15.1
2.16.3

146
0005-Track-errno-correctly.patch
View File

@ -1,146 +0,0 @@
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 efc59008e542..045e353ba932 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.
@@ -2999,6 +3002,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.1

16
0005-llvm-make-KLEE-compile-against-LLVM-3.8.patch
View File

@ -15,10 +15,10 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
7 files changed, 77 insertions(+), 9 deletions(-)
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 045e353ba932..96d85f503d4f 100644
index f7c71e8d2dfc..a7d2eaac2a18 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2135,8 +2135,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
@@ -2212,8 +2212,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());
@ -33,10 +33,10 @@ index 045e353ba932..96d85f503d4f 100644
break;
}
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 6dc13df86440..e931dcef8b2e 100644
index d9ec35aa3405..76f079a81cfd 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -629,7 +629,11 @@ static std::vector<Instruction*> getSuccs(Instruction *i) {
@@ -637,7 +637,11 @@ static std::vector<Instruction*> getSuccs(Instruction *i) {
for (succ_iterator it = succ_begin(bb), ie = succ_end(bb); it != ie; ++it)
res.push_back(&*(it->begin()));
} else {
@ -49,7 +49,7 @@ index 6dc13df86440..e931dcef8b2e 100644
return res;
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index 54bda16013b6..2b93319f2615 100644
index 4846b4ce72b3..6b08ef40e09e 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -52,6 +52,10 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
@ -78,7 +78,7 @@ index 54bda16013b6..2b93319f2615 100644
Value *op2 = ii->getArgOperand(1);
diff --git a/lib/Module/LowerSwitch.cpp b/lib/Module/LowerSwitch.cpp
index 02f00a3ae94e..7fe9d9768d72 100644
index 0f4e8b1eb72b..056885219e85 100644
--- a/lib/Module/LowerSwitch.cpp
+++ b/lib/Module/LowerSwitch.cpp
@@ -64,7 +64,11 @@ void LowerSwitchPass::switchConvert(CaseItr begin, CaseItr end,
@ -248,7 +248,7 @@ index 64e4863f70b3..944f51ef336d 100644
addPass(Passes, createLICMPass()); // Hoist loop invariants
addPass(Passes, createGVNPass()); // Remove redundancies
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index ea24d89c5aaf..14afce0edf7c 100644
index ab9dfe286ffb..3d73ae07fcb5 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 @@ index ea24d89c5aaf..14afce0edf7c 100644
// create directory and try to link klee-last
if (mkdir(d.c_str(), 0775) == 0) {
--
2.15.1
2.16.3

45
0006-Declare-klee_get_errno-and-remove-local-declarations.patch
View File

@ -1,45 +0,0 @@
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 | 3 +++
runtime/POSIX/fd.c | 6 ------
2 files changed, 3 insertions(+), 6 deletions(-)
diff --git a/include/klee/klee.h b/include/klee/klee.h
index 644c498e94ab..8b9cd2e266d3 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -157,6 +157,9 @@ extern "C" {
/* Merge all paths of the state that went through klee_open_merge */
void klee_close_merge();
+
+ /* 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.1

10
0006-llvm-make-KLEE-compile-against-LLVM-3.9.patch
View File

@ -15,10 +15,10 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
7 files changed, 98 insertions(+), 5 deletions(-)
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 96d85f503d4f..d7c3194d9de4 100644
index a7d2eaac2a18..3d54af877844 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1308,10 +1308,18 @@ void Executor::executeCall(ExecutionState &state,
@@ -1307,10 +1307,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 @@ index 96d85f503d4f..d7c3194d9de4 100644
}
}
@@ -1344,10 +1352,18 @@ void Executor::executeCall(ExecutionState &state,
@@ -1343,10 +1351,18 @@ void Executor::executeCall(ExecutionState &state,
Expr::Width argWidth = arguments[i]->getWidth();
if (argWidth > Expr::Int64) {
@ -272,7 +272,7 @@ index b8b32e31264a..800cece95e9c 100644
llvm::cl::ParseCommandLineOptions(argc, argv);
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 14afce0edf7c..436651f438d4 100644
index 3d73ae07fcb5..c0ea4fa54551 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -1132,7 +1132,11 @@ int main(int argc, char **argv, char **envp) {
@ -288,5 +288,5 @@ index 14afce0edf7c..436651f438d4 100644
if (Watchdog) {
if (MaxTime==0) {
--
2.15.1
2.16.3

104
0007-Add-support-for-modelling-errno_location.patch
View File

@ -1,104 +0,0 @@
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 | 44 +++++++++++++++++++++++++++++++++++--
lib/Core/SpecialFunctionHandler.h | 1 +
tools/klee/main.cpp | 2 ++
3 files changed, 45 insertions(+), 2 deletions(-)
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index a8d6edecdd91..267a262fc133 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -91,6 +91,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),
@@ -578,10 +580,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 7e58018f8366..b11a49749ccb 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 2b2fe3eb06c8..9bdf06f600ce 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.1

36
0007-llvm38-test-change-some-tests.patch
View File

@ -6,21 +6,25 @@ Patch-mainline: no
alias in LLVM 3.8 has a new format, it adds a AliaseeTy parameter. So
handle this in the tests.
[v2] add comments about what was changed and why
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
---
test/Feature/BitcastAlias.llvm37.ll | 1 +
test/Feature/BitcastAlias.llvm38.ll | 35 +++++++++++++++++++++++++++++++++
test/Feature/BitcastAlias.llvm38.ll | 38 +++++++++++++++++++++++++++++++++
test/Feature/BitcastAliasMD2U.llvm37.ll | 1 +
test/Feature/BitcastAliasMD2U.llvm38.ll | 35 +++++++++++++++++++++++++++++++++
4 files changed, 72 insertions(+)
test/Feature/BitcastAliasMD2U.llvm38.ll | 38 +++++++++++++++++++++++++++++++++
4 files changed, 78 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
index 5bd301936e13..e860acb24594 100644
--- a/test/Feature/BitcastAlias.llvm37.ll
+++ b/test/Feature/BitcastAlias.llvm37.ll
@@ -1,4 +1,5 @@
@@ -1,6 +1,7 @@
; LLVM 3.7 requires a type as the first argument to 'getelementptr'
; LLVM 3.7 no longer accepts '*' with a 'call'
; REQUIRES: geq-llvm-3.7
+; REQUIRES: lt-llvm-3.8
; RUN: llvm-as %s -f -o %t1.bc
@ -28,10 +32,13 @@ index 0d6e72604d6b..3b702ba2a6b0 100644
; 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
index 000000000000..5111f18e53aa
--- /dev/null
+++ b/test/Feature/BitcastAlias.llvm38.ll
@@ -0,0 +1,35 @@
@@ -0,0 +1,38 @@
+; LLVM 3.8 requires a type as the first argument to 'alias'
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; LLVM 3.7 no longer accepts '*' with a 'call'
+; REQUIRES: geq-llvm-3.8
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
@ -68,10 +75,12 @@ index 000000000000..ff7009b7711b
+ ret i32 0
+}
diff --git a/test/Feature/BitcastAliasMD2U.llvm37.ll b/test/Feature/BitcastAliasMD2U.llvm37.ll
index 12abf09373f8..2332a1968dea 100644
index 7eddd3d6a01c..c29ec8a62243 100644
--- a/test/Feature/BitcastAliasMD2U.llvm37.ll
+++ b/test/Feature/BitcastAliasMD2U.llvm37.ll
@@ -1,4 +1,5 @@
@@ -1,6 +1,7 @@
; LLVM 3.7 requires a type as the first argument to 'getelementptr'
; LLVM 3.7 no longer accepts '*' with a 'call'
; REQUIRES: geq-llvm-3.7
+; REQUIRES: lt-llvm-3.8
; RUN: llvm-as %s -f -o %t1.bc
@ -79,10 +88,13 @@ index 12abf09373f8..2332a1968dea 100644
; 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
index 000000000000..7ef74a8da43c
--- /dev/null
+++ b/test/Feature/BitcastAliasMD2U.llvm38.ll
@@ -0,0 +1,35 @@
@@ -0,0 +1,38 @@
+; LLVM 3.8 requires a type as the first argument to 'alias'
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; LLVM 3.7 no longer accepts '*' with a 'call'
+; REQUIRES: geq-llvm-3.8
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
@ -119,5 +131,5 @@ index 000000000000..f4e41293c347
+ ret i32 0
+}
--
2.15.1
2.16.3

42
0008-Cleanup-test-cases.patch
View File

@ -1,42 +0,0 @@
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.1

6
0008-llvm40-handle-different-header-names.patch
View File

@ -14,7 +14,7 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
3 files changed, 18 insertions(+), 2 deletions(-)
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 0439431b3bc8..ff76cd53c895 100644
index 75e71c0a557f..232cd88fd621 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -21,7 +21,11 @@
@ -59,7 +59,7 @@ index ee4af254dae2..8aa070743048 100644
#include "llvm/Support/raw_ostream.h"
#include "llvm/Support/Path.h"
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 436651f438d4..07f302a4641f 100644
index c0ea4fa54551..154a76feb361 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -31,7 +31,6 @@
@ -84,5 +84,5 @@ index 436651f438d4..07f302a4641f 100644
#include <signal.h>
#include <unistd.h>
--
2.15.1
2.16.3

6
0009-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch
View File

@ -9,10 +9,10 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
1 file changed, 9 insertions(+)
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index d7c3194d9de4..19499e1be37d 100644
index 3d54af877844..dca1fe3a6b93 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1451,12 +1451,21 @@ static bool isDebugIntrinsic(const Function *f, KModule *KM) {
@@ -1450,12 +1450,21 @@ static bool isDebugIntrinsic(const Function *f, KModule *KM) {
static inline const llvm::fltSemantics * fpWidthToSemantics(unsigned width) {
switch(width) {
@ -35,5 +35,5 @@ index d7c3194d9de4..19499e1be37d 100644
return 0;
}
--
2.15.1
2.16.3

35
0009-test-fix-Feature-BFSSearcherAndDFSSearcherInterleave.patch
View File

@ -1,35 +0,0 @@
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.1

2
0010-llvm40-errorOr-and-similar.patch
View File

@ -124,5 +124,5 @@ index 8aa070743048..ad847de0b368 100644
#else
if (auto ec = module->materializeAllPermanently()) {
--
2.15.1
2.16.3

14
0011-llvm-use-chrono-helpers-from-LLVM-4.0.patch
View File

@ -38,7 +38,7 @@ index a422abd027f3..d80ccb31f647 100644
public:
WallTimer();
diff --git a/include/klee/Internal/System/Time.h b/include/klee/Internal/System/Time.h
index 14d235364401..feeeed8affa2 100644
index 220e260c975e..12522c866439 100644
--- a/include/klee/Internal/System/Time.h
+++ b/include/klee/Internal/System/Time.h
@@ -10,7 +10,13 @@
@ -48,9 +48,9 @@ index 14d235364401..feeeed8affa2 100644
+#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
+#include <chrono>
+
+#include <llvm/Support/Chrono.h>
+#include "llvm/Support/Chrono.h"
+#else
#include <llvm/Support/TimeValue.h>
#include "llvm/Support/TimeValue.h"
+#endif
namespace klee {
@ -69,10 +69,10 @@ index 14d235364401..feeeed8affa2 100644
}
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index e931dcef8b2e..c39c7d5bd7ba 100644
index 76f079a81cfd..246c106cc9f4 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -282,6 +282,29 @@ void StatsTracker::done() {
@@ -286,6 +286,29 @@ void StatsTracker::done() {
void StatsTracker::stepInstruction(ExecutionState &es) {
if (OutputIStats) {
if (TrackInstructionTime) {
@ -102,7 +102,7 @@ index e931dcef8b2e..c39c7d5bd7ba 100644
static sys::TimeValue lastNowTime(0,0),lastUserTime(0,0);
if (lastUserTime.seconds()==0 && lastUserTime.nanoseconds()==0) {
@@ -297,6 +320,7 @@ void StatsTracker::stepInstruction(ExecutionState &es) {
@@ -301,6 +324,7 @@ void StatsTracker::stepInstruction(ExecutionState &es) {
lastUserTime = user;
lastNowTime = now;
}
@ -195,5 +195,5 @@ index da96981079ae..a223b39ada57 100644
+
+#endif
--
2.15.1
2.16.3

8
0012-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch
View File

@ -27,10 +27,10 @@ index 5fb9f4ec5c2f..bf7cb6ff0bea 100644
CurTy = 0;
}
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 19499e1be37d..093be697c7da 100644
index dca1fe3a6b93..50a6345e8767 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2522,8 +2522,7 @@ void Executor::computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie) {
@@ -2600,8 +2600,7 @@ void Executor::computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie) {
uint64_t addend = sl->getElementOffset((unsigned) ci->getZExtValue());
constantOffset = constantOffset->Add(ConstantExpr::alloc(addend,
Context::get().getPointerWidth()));
@ -40,7 +40,7 @@ index 19499e1be37d..093be697c7da 100644
uint64_t elementSize =
kmodule->targetData->getTypeStoreSize(set->getElementType());
Value *operand = ii.getOperand();
@@ -2537,7 +2536,24 @@ void Executor::computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie) {
@@ -2615,7 +2614,24 @@ void Executor::computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie) {
} else {
kgepi->indices.push_back(std::make_pair(index, elementSize));
}
@ -67,5 +67,5 @@ index 19499e1be37d..093be697c7da 100644
}
kgepi->offset = constantOffset->getZExtValue();
--
2.15.1
2.16.3

6
0013-llvm40-gep_type_iterator-has-no-operator.patch
View File

@ -12,10 +12,10 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
1 file changed, 4 insertions(+)
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 92dee5ac3906..c9308795804e 100644
index a0f4de3dc43a..6397443647ec 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -200,7 +200,11 @@ namespace klee {
@@ -213,7 +213,11 @@ namespace klee {
continue;
// Handle a struct index, which adds its field offset to the pointer.
@ -28,5 +28,5 @@ index 92dee5ac3906..c9308795804e 100644
const StructLayout *SL = kmodule->targetData->getStructLayout(STy);
base = base->Add(
--
2.15.1
2.16.3

4
0014-llvm50-avoid-on-function-arg_begin.patch
View File

@ -18,7 +18,7 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
1 file changed, 8 insertions(+)
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 07f302a4641f..aeed018631ea 100644
index 154a76feb361..def83b584167 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -658,7 +658,11 @@ static int initEnv(Module *mainModule) {
@ -46,5 +46,5 @@ index 07f302a4641f..aeed018631ea 100644
args.push_back(Constant::getNullValue(ft->getParamType(4))); // app_fini
args.push_back(Constant::getNullValue(ft->getParamType(5))); // rtld_fini
--
2.15.1
2.16.3

2
0015-llvm50-integerPartWidth-is-from-llvm-APFloatBase.patch
View File

@ -28,5 +28,5 @@ index f73d1614c250..5433d9211ead 100644
}
}
--
2.15.1
2.16.3

6
0016-llvm50-handle-getOrInsertFunction-terminator.patch
View File

@ -58,7 +58,7 @@ index aac63e1d9854..406b3045e527 100644
}
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index 2b93319f2615..c00c77699e18 100644
index 6b08ef40e09e..c9e909272b33 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -208,7 +208,7 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
@ -71,7 +71,7 @@ index 2b93319f2615..c00c77699e18 100644
F->setDoesNotThrow();
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index aeed018631ea..02748fbc0ee5 100644
index def83b584167..ff87d210b863 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -678,8 +678,8 @@ static int initEnv(Module *mainModule) {
@ -115,5 +115,5 @@ index aeed018631ea..02748fbc0ee5 100644
f = mainModule->getFunction("__ctype_get_mb_cur_max");
--
2.15.1
2.16.3

6
0017-llvm50-SwitchInst-case-functions-now-return-pointers.patch
View File

@ -15,10 +15,10 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
1 file changed, 4 insertions(+)
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 093be697c7da..5fe5bf9c1346 100644
index 50a6345e8767..5411efe36402 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1571,7 +1571,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
@@ -1643,7 +1643,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
// switch to an internal rep.
llvm::IntegerType *Ty = cast<IntegerType>(si->getCondition()->getType());
ConstantInt *ci = ConstantInt::get(Ty, CE->getZExtValue());
@ -31,5 +31,5 @@ index 093be697c7da..5fe5bf9c1346 100644
} else {
// Handle possible different branch targets
--
2.15.1
2.16.3

2
0018-llvm50-handle-new-file_magic-s-location.patch
View File

@ -65,5 +65,5 @@ index ad847de0b368..5f967410568c 100644
Expected<std::unique_ptr<object::Binary> > arch =
object::createBinary(Buffer, &Context);
--
2.15.1
2.16.3

8
0019-llvm50-use-MutableArrayRef-for-APFloat-convertToInte.patch
View File

@ -13,10 +13,10 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
1 file changed, 12 insertions(+), 2 deletions(-)
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 5fe5bf9c1346..44293f885136 100644
index 5411efe36402..5353f581ab36 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2219,7 +2219,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
@@ -2296,7 +2296,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
uint64_t value = 0;
bool isExact = true;
@ -30,7 +30,7 @@ index 5fe5bf9c1346..44293f885136 100644
llvm::APFloat::rmTowardZero, &isExact);
bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
break;
@@ -2236,7 +2241,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
@@ -2313,7 +2318,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
uint64_t value = 0;
bool isExact = true;
@ -45,5 +45,5 @@ index 5fe5bf9c1346..44293f885136 100644
bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
break;
--
2.15.1
2.16.3

4
0020-llvm50-AllocaInst-takes-address-space.patch
View File

@ -12,7 +12,7 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
1 file changed, 8 insertions(+)
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 02748fbc0ee5..30100b19af3b 100644
index ff87d210b863..c85fee861f03 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -664,10 +664,18 @@ static int initEnv(Module *mainModule) {
@ -35,5 +35,5 @@ index 02748fbc0ee5..30100b19af3b 100644
/* Insert void klee_init_env(int* argc, char*** argv) */
std::vector<const Type*> params;
--
2.15.1
2.16.3

2
_servicedata
View File

@ -1,4 +1,4 @@
<servicedata>
<service name="tar_scm">
<param name="url">git://github.com/klee/klee.git</param>
<param name="changesrevision">37f554d5cf587ec9f6befa359a0e3aa60e9ce73f</param></service></servicedata>
<param name="changesrevision">33964e5d935f903b2850f6576f93ce229fb00918</param></service></servicedata>

3
klee-1.4.0+20180108.tar.xz
View File

@ -1,3 +0,0 @@
version https://git-lfs.github.com/spec/v1
oid sha256:a419c2131fb65b0d4ac8e83d88c1444adfc6cbe02916c1405f435492ff2c4bc4
size 584980

3
klee-1.4.0+20180518.tar.xz Normal file
View File

@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:2ac616443c0b3dd6fd8a24fc4d95dc35ff27bd1bca116c92556434640e0e5338
size 591008

65
klee.changes
View File

@ -1,3 +1,68 @@
-------------------------------------------------------------------
Mon May 21 09:30:16 UTC 2018 - opensuse-packaging@opensuse.org
- Update to version 1.4.0+20180518:
* tests: use names in klee_make_symbolic
* Delete coverageServer.py
* Abort execution if --only-output-states-covering-new is enabled but its dependency --output-istats is not
* Add support for concretizing symbolic objects passed to external functions
* Improve error messages for ReadStringAtAddress
* Improved code quality
* Implemented incomplete merging
* remove QueryLog.h
* Update clang-format standard for KLEE codebase to C++11
* Fix test case to check for correct call string
* Improve handling of constant array in Z3
* Remove the option for truncating lines in assembly.ll
* Remove workaround for bug in older LLVM version (< 3)
* Fix include files
* remove unused file: tools/klee/Debug.cpp
* Fixed test case to exercise modification to utimes()
* Fixed utimes() behavior for symbolic files when the second argument is NULL
* Moved regression test to proper location. Fixes #705
* Fix handling of errno if external functions are invoked
* Factor out method to update state memory with process state
* Ensured program reliably has 3 paths to be explored, and removed unnecessary options. Make klee_abort() call abort() in replay, and removed trivial test which cannot be easily integrated into the test suite.
* Implement klee_prefer_cex() and klee_abort() in Runtest and added corresponding tests
* add blockaddress and indirectbr instructions
* fix compilation warning
* exitOnError no output buf fix
* Change llvm apt repository to enable llvm 3.7+
* Fix python2 linking
* doDumpStates: incorrectly increments stats
* [CMake] Add option to set GTest include dir
* fix test/Feature/BFSSearcherAndDFSSearcherInterleaved.c to use explicit enumeration of possible strings instead of CHECK-SAME (does not work as intended with LLVM >= 3.7)
* Store CexCache stats and then update klee-stats to use them
* Add missing endian information to avoid selecction of big endian systems
* Fail for aggegrations with big endian ordering
* Fixed handling of constant vectors with complex data
* Test complex constant data vectors as well
* Make print function of ObjectState public and const
* Add testcase for constant array handling
* Add test case for constant vector init
* Fix correct element order of InsertElement/ExtractElement
* Fix getelementptr for array or vector indices
* Fix generation of expressions from constant sequential data
* Added comment for getPointerWidth
* llvm50: use auto variable instead of SwitchInst::CaseIt
* Enable caching for travis-ci
* Fix coverage generation
* MergeHandler: remove unused closedStateCount
* add wllvm to the python packages to be installed
* [Travis-CI] Added codecov.io support
- Dropped patches (they are in upstream already):
* 0001-MergeHandler-remove-unused-closedStateCount.patch
* 0002-llvm50-use-auto-variable-instead-of-SwitchInst-CaseI.patch
* 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
-------------------------------------------------------------------
Wed Jan 24 07:59:06 UTC 2018 - jslaby@suse.com

31
klee.spec
View File

@ -19,7 +19,7 @@
%define llvm_version_minor 0
%define llvm_version %{llvm_version_major}
%define version_unconverted 1.4.0+20180108
%define version_unconverted 1.4.0+20180518
%ifarch %{ix86} x86_64
%define with_uclibc 1
@ -31,7 +31,7 @@ Name: klee
Summary: LLVM Execution Engine
License: NCSA
Group: Development/Languages/Other
Version: 1.4.0+20180108
Version: 1.4.0+20180518
Release: 0
Url: http://klee.github.io/
Source0: %{name}-%{version}.tar.xz
@ -39,19 +39,6 @@ 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
Patch1: 0001-MergeHandler-remove-unused-closedStateCount.patch
Patch2: 0002-llvm50-use-auto-variable-instead-of-SwitchInst-CaseI.patch
Patch101: 0001-Fix-generation-of-expressions-from-constant-sequenti.patch
Patch102: 0002-Fix-getelementptr-for-array-or-vector-indices.patch
Patch103: 0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch
Patch104: 0004-Provide-errno-independent-of-CTYPE_EXTERNALS-being-d.patch
Patch105: 0005-Track-errno-correctly.patch
Patch106: 0006-Declare-klee_get_errno-and-remove-local-declarations.patch
Patch107: 0007-Add-support-for-modelling-errno_location.patch
Patch108: 0008-Cleanup-test-cases.patch
Patch109: 0009-test-fix-Feature-BFSSearcherAndDFSSearcherInterleave.patch
Patch201: 0001-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch
Patch202: 0002-llvm-make-KLEE-compile-against-LLVM-3.7.patch
Patch203: 0003-test-add-versions-of-some-tests-for-LLVM-3.7.patch
@ -100,18 +87,6 @@ information on what KLEE is and what it can do, see the OSDI 2008 paper.
%prep
%setup -q
%patch1 -p1
%patch2 -p1
%patch101 -p1
%patch102 -p1
%patch103 -p1
%patch104 -p1
%patch105 -p1
%patch106 -p1
%patch107 -p1
%patch108 -p1
%patch109 -p1
%patch201 -p1
%patch202 -p1
@ -134,7 +109,7 @@ information on what KLEE is and what it can do, see the OSDI 2008 paper.
%patch219 -p1
%patch220 -p1
%patch300 -p1
#%%patch300 -p1
mkdir -p build/test/
cp %{SOURCE2} build/test/