add blockaddress and indirectbr instructions

4 files changed, 146 insertions, 28 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 794b5980..81b9ec3c 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1526,6 +1526,79 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     }
     break;
   }
+  case Instruction::IndirectBr: {
+    // implements indirect branch to a label within the current function
+    const auto bi = cast<IndirectBrInst>(i);
+    auto address = eval(ki, 0, state).value;
+    address = toUnique(state, address);
+
+    // concrete address
+    if (const auto CE = dyn_cast<ConstantExpr>(address.get())) {
+      const auto bb_address = (BasicBlock *) CE->getZExtValue(Context::get().getPointerWidth());
+      transferToBasicBlock(bb_address, bi->getParent(), state);
+      break;
+    }
+
+    // symbolic address
+    const auto numDestinations = bi->getNumDestinations();
+    std::vector<BasicBlock *> targets;
+    targets.reserve(numDestinations);
+    std::vector<ref<Expr>> expressions;
+    expressions.reserve(numDestinations);
+
+    ref<Expr> errorCase = ConstantExpr::alloc(1, Expr::Bool);
+    SmallPtrSet<BasicBlock *, 5> destinations;
+    // collect and check destinations from label list
+    for (unsigned k = 0; k < numDestinations; ++k) {
+      // filter duplicates
+      const auto d = bi->getDestination(k);
+      if (destinations.count(d)) continue;
+      destinations.insert(d);
+
+      // create address expression
+      const auto PE = Expr::createPointer((uint64_t) (unsigned long) (void *) d);
+      ref<Expr> e = EqExpr::create(address, PE);
+
+      // exclude address from errorCase
+      errorCase = AndExpr::create(errorCase, Expr::createIsZero(e));
+
+      // check feasibility
+      bool result;
+      bool success __attribute__ ((unused)) = solver->mayBeTrue(state, e, result);
+      assert(success && "FIXME: Unhandled solver failure");
+      if (result) {
+        targets.push_back(d);
+        expressions.push_back(e);
+      }
+    }
+    // check errorCase feasibility
+    bool result;
+    bool success __attribute__ ((unused)) = solver->mayBeTrue(state, errorCase, result);
+    assert(success && "FIXME: Unhandled solver failure");
+    if (result) {
+      expressions.push_back(errorCase);
+    }
+
+    // fork states
+    std::vector<ExecutionState *> branches;
+    branch(state, expressions, branches);
+
+    // terminate error state
+    if (result) {
+      terminateStateOnExecError(*branches.back(), "indirectbr: illegal label address");
+      branches.pop_back();
+    }
+
+    // branch states to resp. target blocks
+    assert(targets.size() == branches.size());
+    for (std::vector<ExecutionState *>::size_type k = 0; k < branches.size(); ++k) {
+      if (branches[k]) {
+        transferToBasicBlock(targets[k], bi->getParent(), *branches[k]);
+      }
+    }
+
+    break;
+  }
   case Instruction::Switch: {
     SwitchInst *si = cast<SwitchInst>(i);
     ref<Expr> cond = eval(ki, 0, state).value;
@@ -1641,7 +1714,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       }
     }
     break;
- }
+  }
   case Instruction::Unreachable:
     // Note that this is not necessarily an internal bug, llvm will
     // generate unreachable instructions in cases where it knows the
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 62d65c31..a0f4de3d 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -119,6 +119,11 @@ namespace klee {
         assert(isa<ConstantExpr>(res) &&
                "result of constant vector built is not a constant");
         return cast<ConstantExpr>(res);
+      } else if (const BlockAddress * ba = dyn_cast<BlockAddress>(c)) {
+        // return the address of the specified basic block in the specified function
+        const auto arg_bb = (BasicBlock *) ba->getOperand(1);
+        const auto res = Expr::createPointer((uint64_t) (unsigned long) (void *) arg_bb);
+        return cast<ConstantExpr>(res);
       } else {
         std::string msg("Cannot handle constant ");
         llvm::raw_string_ostream os(msg);
diff --git a/test/Feature/AddressOfLabels.c b/test/Feature/AddressOfLabels.c
index 84493fd8..6d807dbb 100644
--- a/test/Feature/AddressOfLabels.c
+++ b/test/Feature/AddressOfLabels.c
@@ -1,36 +1,38 @@
 // RUN: %llvmgcc -emit-llvm -g -c %s -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: not %klee --output-dir=%t.klee-out %t.bc 2> %t.log
-// RUN: FileCheck --input-file %t.log %s
+// RUN: %klee --output-dir=%t.klee-out %t.bc > %t.log
+// RUN: FileCheck --input-file=%t.log %s
 
-/* 
-   This currently tests that KLEE clearly reports that it doesn't
-   support taking the address of the labels, in particular
-   blockaddress constants.
+#include <stdio.h>
 
-   The test would need to be changes once support for this feature is
-   added. 
-*/
+int main(int argc, char * argv[]) {
+	// prevent CFGSimplificationPass optimisation
+	void * dummy = &&one;
+	switch(argc) {
+		case 1: break;
+		case 2:
+			dummy = &&three;
+			goto *dummy;
+		default:
+			goto *dummy;
+	}
 
-#include <stdio.h>
+	// the real test
+	void * lptr = &&two;
+	goto *lptr;
 
-int main (int argc, char** argv)
-{
-  int i = 1;
-  // CHECK: Cannot handle constant 'i8* blockaddress 
-  // CHECK: AddressOfLabels.c:[[@LINE+1]]
-  void * lptr = &&one;
+one:
+	puts("Label one");
+// CHECK-NOT: Label one
+	return 1;
 
-  if (argc > 1)
-    lptr = &&two;
-  
-  goto *lptr;
+two:
+	puts("Label two");
+// CHECK: Label two
+	return 0;
 
- one:
-  printf("argc is 1\n");
-  return 0;
-  
- two:
-  printf("argc is >1\n");
-  return 0;
+three:
+	puts("Label three");
+// CHECK-NOT: Label three
+	return 1;
 }
diff --git a/test/Feature/AddressOfLabelsSymbolic.c b/test/Feature/AddressOfLabelsSymbolic.c
new file mode 100644
index 00000000..2c7e39c7
--- /dev/null
+++ b/test/Feature/AddressOfLabelsSymbolic.c
@@ -0,0 +1,38 @@
+// RUN: %llvmgcc -emit-llvm -g -c %s -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out %t.bc > %t.log 2> %t.stderr.log
+// RUN: FileCheck %s -check-prefix=CHECK-MSG --input-file=%t.log
+// RUN: FileCheck %s -check-prefix=CHECK-ERR --input-file=%t.stderr.log
+
+#include <stdio.h>
+
+int main(void) {
+	void * lptr = &&one;
+	lptr = &&two;
+	lptr = &&three;
+
+	klee_make_symbolic(&lptr, sizeof(lptr), "lptr");
+// CHECK-ERR: KLEE: ERROR: {{.*}} indirectbr: illegal label address
+	goto *lptr;
+
+one:
+	puts("Label one");
+// CHECK-MSG-DAG: Label one
+	return 0;
+
+two:
+	puts("Label two");
+// CHECK-MSG-DAG: Label two
+	return 0;
+
+three:
+	puts("Label three");
+// CHECK-MSG-DAG: Label three
+	return 0;
+
+// LLVM should infer only {one, two, three} as valid targets
+four:
+	puts("Label four");
+// CHECK-MSG-NOT: Label four
+	return 0;
+}