diff options
| -rw-r--r-- | include/klee/Expr.h | 3 | ||||
| -rw-r--r-- | lib/Core/Context.cpp | 6 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 6 | ||||
| -rw-r--r-- | test/Feature/GetElementPtr.ll | 28 |
4 files changed, 38 insertions, 5 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h index ccbd9163..3e296934 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -230,7 +230,8 @@ public: /* Kind utilities */ /* Utility creation functions */ - static ref<Expr> createCoerceToPointerType(ref<Expr> e); + static ref<Expr> createSExtToPointerWidth(ref<Expr> e); + static ref<Expr> createZExtToPointerWidth(ref<Expr> e); static ref<Expr> createImplies(ref<Expr> hyp, ref<Expr> conc); static ref<Expr> createIsZero(ref<Expr> e); diff --git a/lib/Core/Context.cpp b/lib/Core/Context.cpp index 45dbdca0..979970aa 100644 --- a/lib/Core/Context.cpp +++ b/lib/Core/Context.cpp @@ -35,7 +35,11 @@ const Context &Context::get() { // FIXME: This is a total hack, just to avoid a layering issue until this stuff // moves out of Expr. -ref<Expr> Expr::createCoerceToPointerType(ref<Expr> e) { +ref<Expr> Expr::createSExtToPointerWidth(ref<Expr> e) { + return SExtExpr::create(e, Context::get().getPointerWidth()); +} + +ref<Expr> Expr::createZExtToPointerWidth(ref<Expr> e) { return ZExtExpr::create(e, Context::get().getPointerWidth()); } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 48a8b57a..1a37498f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1863,7 +1863,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref<Expr> size = Expr::createPointer(elementSize); if (ai->isArrayAllocation()) { ref<Expr> count = eval(ki, 0, state).value; - count = Expr::createCoerceToPointerType(count); + count = Expr::createZExtToPointerWidth(count); size = MulExpr::create(size, count); } bool isLocal = i->getOpcode()==Instruction::Alloca; @@ -1899,7 +1899,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { uint64_t elementSize = it->second; ref<Expr> index = eval(ki, it->first, state).value; base = AddExpr::create(base, - MulExpr::create(Expr::createCoerceToPointerType(index), + MulExpr::create(Expr::createSExtToPointerWidth(index), Expr::createPointer(elementSize))); } if (kgepi->offset) @@ -2320,7 +2320,7 @@ void Executor::computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie) { Value *operand = ii.getOperand(); if (Constant *c = dyn_cast<Constant>(operand)) { ref<ConstantExpr> index = - evalConstant(c)->ZExt(Context::get().getPointerWidth()); + evalConstant(c)->SExt(Context::get().getPointerWidth()); ref<ConstantExpr> addend = index->Mul(ConstantExpr::alloc(elementSize, Context::get().getPointerWidth())); diff --git a/test/Feature/GetElementPtr.ll b/test/Feature/GetElementPtr.ll new file mode 100644 index 00000000..7f10c0a2 --- /dev/null +++ b/test/Feature/GetElementPtr.ll @@ -0,0 +1,28 @@ +; RUN: llvm-as %s -f -o %t1.bc +; RUN: %klee -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" + +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() { +entry: + %addr = alloca i8, align 4 + %addrp1 = getelementptr i8* %addr, i32 1 + %addrp1m1 = getelementptr i8* %addrp1, i32 -1 + %test = icmp eq i8* %addr, %addrp1m1 + br i1 %test, label %bbtrue, label %bbfalse + +bbtrue: + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + ret i32 0 + +bbfalse: + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + ret i32 0 +} |