Merge pull request #53 from ftsrg/float-cast

Add support for bitcast instructions between bitvectors and float types

CMakeLists.txt

@@ -7,10 +7,10 @@ if(NOT DEFINED GAZER_VERSION_MAJOR)
   set(GAZER_VERSION_MAJOR 1)
 endif()
 if(NOT DEFINED GAZER_VERSION_MINOR)
-  set(GAZER_VERSION_MINOR 1)
+  set(GAZER_VERSION_MINOR 2)
 endif()
 if(NOT DEFINED GAZER_VERSION_PATCH)
-  set(GAZER_VERSION_PATCH 5)
+  set(GAZER_VERSION_PATCH 0)
 endif()
 if(NOT DEFINED GAZER_VERSION_SUFFIX)
   set(GAZER_VERSION_SUFFIX "")

include/gazer/Core/Expr.h

@@ -37,7 +37,7 @@
 
 namespace llvm {
     class raw_ostream;
-}
+} // namespace llvm
 
 namespace gazer
 {
@@ -100,7 +100,7 @@ class Expr
     static constexpr int LastFp = FLtEq;
 
     static constexpr int FirstFpUnary = FIsNan;
-    static constexpr int LastFpUnary = FpToUnsigned;
+    static constexpr int LastFpUnary = FpToBv;
     static constexpr int FirstFpArithmetic = FAdd;
     static constexpr int LastFpArithmetic = FDiv;
     static constexpr int FirstFpCompare = FEq;
@@ -170,7 +170,6 @@ class Expr
     virtual void print(llvm::raw_ostream& os) const = 0;
     virtual ~Expr() = default;
 
-public:
     static llvm::StringRef getKindName(ExprKind kind);
 
 private:

include/gazer/Core/Expr/ExprBuilder.h

@@ -246,6 +246,13 @@ class ExprBuilder
         return FpToUnsignedExpr::Create(op, type, rm);
     }
 
+    virtual ExprPtr FpToBv(const ExprPtr& op, BvType& type) {
+        return FpToBvExpr::Create(op, type);
+    }
+    virtual ExprPtr BvToFp(const ExprPtr& op, FloatType& type) {
+        return BvToFpExpr::Create(op, type);
+    }
+
     virtual ExprPtr FAdd(const ExprPtr& left, const ExprPtr& right, llvm::APFloat::roundingMode rm) {
         return FAddExpr::Create(left, right, rm);
     }

include/gazer/Core/Expr/ExprKind.def

@@ -89,6 +89,8 @@ GAZER_EXPR_KIND(SignedToFp)
 GAZER_EXPR_KIND(UnsignedToFp)
 GAZER_EXPR_KIND(FpToSigned)
 GAZER_EXPR_KIND(FpToUnsigned)
+GAZER_EXPR_KIND(FpToBv) // Bit-cast a floating-point value to a bit-vector
+GAZER_EXPR_KIND(BvToFp) // Bit-cast a bit-vector into a floating-point value
 
 // Floating point binary
 GAZER_EXPR_KIND(FAdd)

include/gazer/Core/Expr/ExprWalker.h

@@ -403,6 +403,13 @@ class ExprWalker
         return static_cast<DerivedT*>(this)->visitNonNullary(expr);
     }
 
+    ReturnT visitFpToBv(const ExprRef<FpToBvExpr>& expr) {
+        return static_cast<DerivedT*>(this)->visitNonNullary(expr);
+    }
+    ReturnT visitBvToFp(const ExprRef<BvToFpExpr>& expr) {
+        return static_cast<DerivedT*>(this)->visitNonNullary(expr);
+    }
+
     // Floating-point arithmetic
     ReturnT visitFAdd(const ExprRef<FAddExpr>& expr) {
         return static_cast<DerivedT*>(this)->visitNonNullary(expr);

include/gazer/Core/ExprTypes.h

@@ -300,8 +300,6 @@ class BvFpCastExpr final : public UnaryExpr, public detail::FpExprWithRoundingMo
         : UnaryExpr(kind, type, begin, end), FpExprWithRoundingMode(rm)
     {}
 
-protected:
-
 public:
     static ExprRef<BvFpCastExpr<Kind>> Create(const ExprPtr& operand, Type& type, const llvm::APFloat::roundingMode& rm);
 
@@ -315,6 +313,27 @@ using UnsignedToFpExpr = BvFpCastExpr<Expr::UnsignedToFp>;
 using FpToSignedExpr   = BvFpCastExpr<Expr::FpToSigned>;
 using FpToUnsignedExpr = BvFpCastExpr<Expr::FpToUnsigned>;
 
+template<Expr::ExprKind Kind>
+class BitCastExpr final : public UnaryExpr
+{
+    static_assert(Kind >= Expr::FpToBv && Kind <= Expr::BvToFp, "BitCast expressions can only be FpToBv or BvToFp!");
+    friend class ExprStorage;
+private:
+    template<class InputIterator>
+    BitCastExpr(Expr::ExprKind kind, Type& type, InputIterator begin, InputIterator end)
+        : UnaryExpr(kind, type, begin, end)
+    {}
+
+public:
+    static ExprRef<BitCastExpr<Kind>> Create(const ExprPtr& operand, Type& type);
+
+    static bool classof(const Expr* expr) { return expr->getKind() == Kind; }
+    static bool classof(const Expr& expr) { return expr.getKind() == Kind; }
+};
+
+using FpToBvExpr = BitCastExpr<Expr::FpToBv>;
+using BvToFpExpr = BitCastExpr<Expr::BvToFp>;
+
 template<Expr::ExprKind Kind>
 class FpArithmeticExpr final : public BinaryExpr, public detail::FpExprWithRoundingMode
 {

include/gazer/LLVM/Automaton/InstToExpr.h

@@ -83,6 +83,7 @@ class InstToExpr
     ExprPtr asInt(const ExprPtr& operand);
 
     ExprPtr integerCast(const llvm::CastInst& cast, const ExprPtr& castOperand, Type& expectedType);
+    ExprPtr bitCast(const ExprPtr& castOperand, Type& expectedType);
     ExprPtr castResult(const ExprPtr& expr, const Type& type);
     ExprPtr boolToIntCast(const llvm::CastInst& cast, const ExprPtr& operand, Type& expectedType);
 

include/gazer/LLVM/LLVMFrontend.h

@@ -150,6 +150,7 @@ class LLVMFrontend
     void registerEarlyOptimizations();
     void registerLateOptimizations();
     void registerInlining();
+    void registerVerificationStep();
 
 private:
     GazerContext& mContext;

src/Core/Expr.cpp

@@ -34,7 +34,8 @@ std::size_t gazer::expr_kind_prime(Expr::ExprKind kind)
         290623u, 241291u, 579499u, 384287u, 125287u, 920273u, 485833u, 326449u,
         972683u, 485167u, 882599u, 535727u, 383651u, 159833u, 796001u, 218479u,
         163993u, 622561u, 938881u, 692467u, 851971u, 478427u, 653969u, 650329u,
-        645187u, 830827u, 431729u, 497663u, 392351u, 715237u
+        645187u, 830827u, 431729u, 497663u, 392351u, 715237u,  111323u,
+        359641u
     };
 
     static_assert(
@@ -251,6 +252,24 @@ auto BvFpCastExpr<Kind>::Create(const ExprPtr& operand, Type& type, const llvm::
     return context.pImpl->Exprs.create<BvFpCastExpr<Kind>>(type, { operand }, rm);
 }
 
+template<Expr::ExprKind Kind>
+auto BitCastExpr<Kind>::Create(const ExprPtr& operand, Type& type) -> ExprRef<BitCastExpr<Kind>>
+{
+    assert(operand->getType() != type && "Cast source and target operands must differ!");
+
+    if constexpr (Kind == Expr::FpToBv) { // NOLINT
+        assert(operand->getType().isFloatType() && "Can only do FpToBv cast on float inputs!");
+        assert(type.isBvType() && "Can only do FpToBv cast to bit-vector targets!");
+    } else if constexpr (Kind == Expr::BvToFp) { // NOLINT
+        assert(operand->getType().isBvType() && "Can only do BvToFp on bit-vector inputs!");
+        assert(type.isFloatType() && "Can only do BvToFp cast to floating-point targets!");
+    }
+
+    auto& context = operand->getContext();
+
+    return context.pImpl->Exprs.create<BitCastExpr<Kind>>(type, { operand });
+}
+
 template<Expr::ExprKind Kind>
 auto FpArithmeticExpr<Kind>::Create(const ExprPtr& left, const ExprPtr& right, const llvm::APFloat::roundingMode& rm) -> ExprRef<FpArithmeticExpr<Kind>>
 {
@@ -370,6 +389,9 @@ template class BvFpCastExpr<Expr::UnsignedToFp>;
 template class BvFpCastExpr<Expr::FpToSigned>;
 template class BvFpCastExpr<Expr::FpToUnsigned>;
 
+template class BitCastExpr<Expr::FpToBv>;
+template class BitCastExpr<Expr::BvToFp>;
+
 template class FpArithmeticExpr<Expr::FAdd>;
 template class FpArithmeticExpr<Expr::FSub>;
 template class FpArithmeticExpr<Expr::FMul>;

src/Core/Expr/ExprRewrite.cpp

@@ -105,6 +105,8 @@ ExprPtr ExprRewriteBase::rewriteNonNullary(const ExprRef<NonNullaryExpr>& expr,
                 casted->getRoundingMode()
             );
         }
+        case Expr::FpToBv: return mExprBuilder.FpToBv(ops[0], llvm::cast<BvType>(expr->getType()));
+        case Expr::BvToFp: return mExprBuilder.BvToFp(ops[0], llvm::cast<FloatType>(expr->getType()));
         case Expr::FAdd: return mExprBuilder.FAdd(ops[0], ops[1], llvm::cast<FAddExpr>(expr)->getRoundingMode());
         case Expr::FSub: return mExprBuilder.FSub(ops[0], ops[1], llvm::cast<FSubExpr>(expr)->getRoundingMode());
         case Expr::FMul: return mExprBuilder.FMul(ops[0], ops[1], llvm::cast<FMulExpr>(expr)->getRoundingMode());

src/LLVM/Automaton/InstToExpr.cpp

@@ -432,15 +432,15 @@ ExprPtr InstToExpr::visitCastInst(const llvm::CastInst& cast, Type& expectedType
         return asBool(castOp);
     }
 
-    if (castOp->getType().isBvType() || castOp->getType().isIntType()) {
-        return integerCast(cast, castOp, expectedType);
+    if (cast.getOpcode() == Instruction::BitCast) {
+        return this->bitCast(castOp, expectedType);
     }
 
-
-    if (cast.getOpcode() == Instruction::BitCast) {
-        // TODO...
+    if (castOp->getType().isBvType() || castOp->getType().isIntType()) {
+        return integerCast(cast, castOp, expectedType);
     }
 
+    llvm::errs() << cast << " " << expectedType << "\n";
     llvm_unreachable("Unsupported cast operation");
 }
 
@@ -580,6 +580,7 @@ ExprPtr InstToExpr::integerCast(const llvm::CastInst& cast, const ExprPtr& castO
         return mExprBuilder.Undef(castOperand->getType());
     }
 
+    llvm::errs() << cast << "\n";
     llvm_unreachable("Invalid integer type!");
 }
 
@@ -628,6 +629,28 @@ ExprPtr InstToExpr::boolToIntCast(const llvm::CastInst& cast, const ExprPtr& ope
     llvm_unreachable("Invalid integer cast type!");
 }
 
+ExprPtr InstToExpr::bitCast(const ExprPtr &castOperand, Type &expectedType)
+{
+    Type& srcType = castOperand->getType();
+
+    if (auto floatTy = llvm::dyn_cast<FloatType>(&srcType)) {
+        if (auto bvTy = llvm::dyn_cast<BvType>(&expectedType)) {
+            assert(floatTy->getWidth() == bvTy->getWidth() && "Can only perform bit-cast between types of equal width!");
+            return mExprBuilder.FpToBv(castOperand, *bvTy);
+        }
+    }
+
+    if (auto bvTy = llvm::dyn_cast<BvType>(&srcType)) {
+        if (auto floatTy = llvm::dyn_cast<FloatType>(&expectedType)) {
+            assert(floatTy->getWidth() == bvTy->getWidth() && "Can only perform bit-cast between types of equal width!");
+            return mExprBuilder.BvToFp(castOperand, *floatTy);
+        }
+    }
+
+    llvm::errs() << "Unhandled bitcast between " << srcType << " and " << expectedType << "\n";
+    llvm_unreachable("Unknown bit-cast instruction!");
+}
+
 static GazerIntrinsic::Overflow getOverflowKind(llvm::StringRef name)
 {
     #define HANDLE_PREFIX(PREFIX, KIND)                                           \

src/LLVM/LLVMFrontend.cpp

@@ -68,6 +68,9 @@ namespace
     cl::opt<bool> StructurizeCFG(
         "structurize", cl::desc("Try to remove irreducible controlf flow"), cl::cat(LLVMFrontendCategory)
     );
+    cl::opt<bool> SkipPipeline(
+        "skip-pipeline", cl::desc("Do not execute the verification pipeline; translate and verify the input LLVM module directly")
+    );
 
     class RunVerificationBackendPass : public llvm::ModulePass
     {
@@ -117,10 +120,7 @@ LLVMFrontend::LLVMFrontend(
 
     // Force settings to be consistent
     if (mSettings.ints == IntRepresentation::Integers) {
-        llvm::errs().changeColor(llvm::raw_ostream::YELLOW, true);
-        llvm::errs() << "warning: ";
-        llvm::errs().resetColor();
-        llvm::errs() << "-math-int mode forces havoc memory model, analysis may be unsound\n";
+        emit_warning("-math-int mode forces havoc memory model, analysis may be unsound\n");
         mSettings.memoryModel = MemoryModelSetting::Havoc;
     }
 
@@ -137,6 +137,12 @@ LLVMFrontend::LLVMFrontend(
 
 void LLVMFrontend::registerVerificationPipeline()
 {
+    if (SkipPipeline) {
+        mPassManager.add(new llvm::DominatorTreeWrapperPass());
+        this->registerVerificationStep();
+        return;
+    }
+
     // Do basic preprocessing: get rid of alloca's and turn undef's
     //  into nondet function calls.
     mPassManager.add(llvm::createPromoteMemoryToRegisterPass());
@@ -175,19 +181,25 @@ void LLVMFrontend::registerVerificationPipeline()
     // Do an instruction namer pass.
     mPassManager.add(llvm::createInstructionNamerPass());
 
-    if (!PrintFinalModule.empty() && mModuleOutput != nullptr) {
-        mPassManager.add(llvm::createPrintModulePass(mModuleOutput->os()));
-        mModuleOutput->keep();
-    }
-
     // Unify exit nodes again
     mPassManager.add(llvm::createUnifyFunctionExitNodesPass());
+    mPassManager.add(llvm::createInstructionCombiningPass(false));
 
     // Display the final LLVM CFG now.
     if (ShowFinalCFG) {
         mPassManager.add(llvm::createCFGPrinterLegacyPassPass());
     }
 
+    if (mModuleOutput != nullptr) {
+        mPassManager.add(llvm::createPrintModulePass(mModuleOutput->os()));
+        mModuleOutput->keep();
+    }
+
+    this->registerVerificationStep();
+}
+
+void LLVMFrontend::registerVerificationStep()
+{
     // Perform module-to-automata translation.
     mPassManager.add(new gazer::MemoryModelWrapperPass(mContext, mSettings));
     mPassManager.add(new gazer::ModuleToAutomataPass(mContext, mSettings));
@@ -404,33 +416,3 @@ void LLVMFrontend::registerLateOptimizations()
     mPassManager.add(gazer::createCanonizeLoopExitsPass());
 }
 
-auto LLVMFrontend::FromInputFile(
-    llvm::StringRef input,
-    GazerContext& context,
-    llvm::LLVMContext& llvmContext,
-    LLVMFrontendSettings& settings
-) -> std::unique_ptr<LLVMFrontend>
-{
-    llvm::SMDiagnostic err;
-
-    std::unique_ptr<llvm::Module> module = nullptr;
-
-    if (input.endswith(".bc")) {
-        module = llvm::parseIRFile(input, err, llvmContext);
-    } else if (input.endswith(".ll")) {
-        module = llvm::parseAssemblyFile(input, err, llvmContext);
-    } else {
-        err = SMDiagnostic(
-            input,
-            SourceMgr::DK_Error,
-            "Input file must be in LLVM bitcode (.bc) or LLVM assembly (.ll) format."
-        );
-    }
-
-    if (module == nullptr) {
-        err.print(nullptr, llvm::errs());
-        return nullptr;
-    }
-
-    return std::make_unique<LLVMFrontend>(std::move(module), context, settings);
-}

src/LLVM/Memory/FlatMemoryModel.cpp

@@ -18,10 +18,10 @@
 #include "gazer/LLVM/Memory/MemoryModel.h"
 #include "gazer/LLVM/Memory/MemoryInstructionHandler.h"
 #include "gazer/LLVM/Memory/MemorySSA.h"
-#include "gazer/LLVM/Memory/MemoryUtils.h"
 
 #include "gazer/Core/LiteralExpr.h"
 #include "gazer/Core/Expr/ExprBuilder.h"
+#include "gazer/Support/Warnings.h"
 
 #include <llvm/IR/InstIterator.h>
 #include <llvm/IR/GetElementPtrTypeIterator.h>
@@ -529,6 +529,16 @@ ExprPtr FlatMemoryModelInstTranslator::handleConstantDataArray(
                 boolLit->getValue() ? mExprBuilder.BvLit8(1) : mExprBuilder.BvLit8(0)
             );
             currentOffset += 1;
+        } else if (auto floatLit = llvm::dyn_cast<FloatLiteralExpr>(lit)) {
+            llvm::APInt floatAsIeeeBv = floatLit->getValue().bitcastToAPInt();
+            for (unsigned j = 0; j < size; ++j) {
+                auto byteValue = mExprBuilder.BvLit(floatAsIeeeBv.extractBits(8, j * 8));
+                builder.addValue(
+                    mMemoryModel.ptrConstant(currentOffset),
+                    byteValue
+                );
+                currentOffset += j;
+            }
         } else {
             llvm_unreachable("Unsupported array type!");
         }
@@ -723,12 +733,18 @@ auto FlatMemoryModelInstTranslator::buildMemoryRead(
             return result;
         }
         case Type::FloatTypeID: {
-            // TODO: We will need a bitcast from bitvectors to floats.
-            return mExprBuilder.Undef(targetTy);
+            ExprPtr result = mExprBuilder.Read(array, pointer);
+            for (unsigned i = 1; i < size; ++i) {
+                // TODO: Little/big endian
+                result = mExprBuilder.BvConcat(
+                    mExprBuilder.Read(array, this->pointerOffset(pointer, i)), result);
+            }
+
+            return mExprBuilder.BvToFp(result, llvm::cast<FloatType>(targetTy));
         }
         default:
             // If it is not a convertible type, just undef it.
-            // TODO: We should emit a warning here.
+            emit_warning("Cannot represent result type %s of memory load", targetTy.getName().c_str());
             return mExprBuilder.Undef(targetTy);
     }
 

src/LLVM/Memory/MemoryModel.cpp

@@ -33,7 +33,6 @@ void MemoryModelWrapperPass::getAnalysisUsage(llvm::AnalysisUsage& au) const
 {
     switch (mSettings.memoryModel) {
         case MemoryModelSetting::Flat:
-            au.addRequired<llvm::UnifyFunctionExitNodes>();
             au.addRequired<llvm::DominatorTreeWrapperPass>();
         case MemoryModelSetting::Havoc:
             break;