From 179a8930253e7e81dda77fda1db11a6d11b22f14 Mon Sep 17 00:00:00 2001
From: Peter Collingbourne <peter@pcc.me.uk>
Date: Fri, 29 Jul 2011 17:49:56 +0000
Subject: Sign extend, rather than zero extend, narrow gep indices

For example, clang creates these for ++ and -- operations on pointers
on 64-bit platforms.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136474 91177308-0d34-0410-b5e6-96231b3b80d8
---
 include/klee/Expr.h           |  3 ++-
 lib/Core/Context.cpp          |  6 +++++-
 lib/Core/Executor.cpp         |  6 +++---
 test/Feature/GetElementPtr.ll | 28 ++++++++++++++++++++++++++++
 4 files changed, 38 insertions(+), 5 deletions(-)
 create mode 100644 test/Feature/GetElementPtr.ll

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
+}
-- 
cgit 1.4.1