Extended support for assembler raising

Improved support for assembler handling.
Providing additional triple information
to raise assembler for supported architectures
only.

Implemented support for raising full assembly
memory fence.

Added initial support for memory fences in Executor.

3 files changed, 47 insertions, 9 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index d755403f..8b885527 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2543,9 +2543,15 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     bindLocal(ki, state, result);
     break;
   }
- 
-    // Other instructions...
-    // Unhandled
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+  case Instruction::Fence: {
+    // Ignore for now
+    break;
+  }
+#endif
+
+  // Other instructions...
+  // Unhandled
   case Instruction::ExtractElement:
   case Instruction::InsertElement:
   case Instruction::ShuffleVector:
diff --git a/lib/Module/Passes.h b/lib/Module/Passes.h
index accb64d0..4f1a1453 100644
--- a/lib/Module/Passes.h
+++ b/lib/Module/Passes.h
@@ -21,8 +21,9 @@
 #include "llvm/Instructions.h"
 #include "llvm/Module.h"
 #endif
-#include "llvm/Pass.h"
+#include "llvm/ADT/Triple.h"
 #include "llvm/CodeGen/IntrinsicLowering.h"
+#include "llvm/Pass.h"
 
 namespace llvm {
   class Function;
@@ -46,6 +47,8 @@ class RaiseAsmPass : public llvm::ModulePass {
 
   const llvm::TargetLowering *TLI;
 
+  llvm::Triple triple;
+
   llvm::Function *getIntrinsic(llvm::Module &M,
                                unsigned IID,
                                LLVM_TYPE_Q llvm::Type **Tys,
diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp
index 12e5479b..7c0e6ccf 100644
--- a/lib/Module/RaiseAsm.cpp
+++ b/lib/Module/RaiseAsm.cpp
@@ -9,12 +9,16 @@
 
 #include "Passes.h"
 #include "klee/Config/Version.h"
+#include "klee/Internal/Support/ErrorHandling.h"
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/IRBuilder.h"
 #include "llvm/IR/InlineAsm.h"
 #include "llvm/IR/LLVMContext.h"
+#include "llvm/IR/Instructions.h"
 #else
 #include "llvm/InlineAsm.h"
 #include "llvm/LLVMContext.h"
+#include "llvm/Support/IRBuilder.h"
 #endif
 
 #include "llvm/Support/raw_ostream.h"
@@ -46,10 +50,32 @@ Function *RaiseAsmPass::getIntrinsic(llvm::Module &M,
 // FIXME: This should just be implemented as a patch to
 // X86TargetAsmInfo.cpp, then everyone will benefit.
 bool RaiseAsmPass::runOnInstruction(Module &M, Instruction *I) {
-  if (CallInst *ci = dyn_cast<CallInst>(I)) {
-    if (InlineAsm *ia = dyn_cast<InlineAsm>(ci->getCalledValue())) {
-      (void) ia;
-      return TLI && TLI->ExpandInlineAsm(ci);
+  // We can just raise inline assembler using calls
+  CallInst *ci = dyn_cast<CallInst>(I);
+  if (!ci)
+    return false;
+
+  InlineAsm *ia = dyn_cast<InlineAsm>(ci->getCalledValue());
+  if (!ia)
+    return false;
+
+  // Try to use existing infrastructure
+  if (!TLI)
+    return false;
+
+  if (TLI->ExpandInlineAsm(ci))
+    return true;
+
+  if (triple.getArch() == llvm::Triple::x86_64 &&
+      triple.getOS() == llvm::Triple::Linux) {
+
+    if (ia->getAsmString() == "" && ia->hasSideEffects()) {
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+      IRBuilder<> Builder(I);
+      Builder.CreateFence(llvm::SequentiallyConsistent);
+#endif
+      I->eraseFromParent();
+      return true;
     }
   }
 
@@ -66,9 +92,10 @@ bool RaiseAsmPass::runOnModule(Module &M) {
   std::string HostTriple = llvm::sys::getHostTriple();
 #endif
   const Target *NativeTarget = TargetRegistry::lookupTarget(HostTriple, Err);
+
   TargetMachine * TM = 0;
   if (NativeTarget == 0) {
-    llvm::errs() << "Warning: unable to select native target: " << Err << "\n";
+    klee_warning("Warning: unable to select native target: %s", Err.c_str());
     TLI = 0;
   } else {
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
@@ -80,6 +107,8 @@ bool RaiseAsmPass::runOnModule(Module &M) {
     TM = NativeTarget->createTargetMachine(HostTriple, "");
 #endif
     TLI = TM->getTargetLowering();
+
+    triple = llvm::Triple(HostTriple);
   }
   
   for (Module::iterator fi = M.begin(), fe = M.end(); fi != fe; ++fi) {