diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md new file mode 100644 index 00000000..d5e5e31c --- /dev/null +++ b/.github/ISSUE_TEMPLATE/bug_report.md @@ -0,0 +1,43 @@ +--- +name: Bug report +about: Create a report to help us improve +title: '' +labels: bug +assignees: '' + +--- + +**Describe the bug** +A clear and concise description of what the bug is. + +**To Reproduce** +Steps to reproduce the behavior: + +Exact command issued, with the input files attached, possibly minimized. + +**Expected behavior** +A clear and concise description of what you expected to happen. + +**Version (please complete the following information):** + - Version (branch, etc.) + - Theta version (if applicable) + +**Additional context** +Add any other context about the problem here. + +**Additional tips to pinpoint when the error was introduced:** + +Run with ... and check if the error persists: + + - `--no-optimize` + - `--memory=havoc --math=int` + - note that these might break soundness. Check if the CFA is correct! + - `--debug` flag to dump more data + +Intermediate state dumps: check these files to pinpoint the problem. + + - `clang -S -emit-llvm input.c` + - `gazer-cfa --run-pipeline ` + - This (and the next) creates one file (.function.dot) per loop and per function. + - `gazer-cfa ...` (this is for checking the backend only. Probably passing an optimized LLVM IR file is the best) + - When running gazer-theta, check the output file diff --git a/.travis.yml b/.travis.yml index 285dc7fb..987119fc 100644 --- a/.travis.yml +++ b/.travis.yml @@ -17,7 +17,7 @@ addons: - python3-setuptools - python3-psutil env: -- THETA_VERSION="v2.4.0" +- THETA_VERSION="v2.5.0" script: # fetch LLVM and other dependencies - wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add - diff --git a/CMakeLists.txt b/CMakeLists.txt index 73232bc5..ef46d6fb 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,6 +1,26 @@ cmake_minimum_required(VERSION 3.8) project(gazer) +# Set version information + +if(NOT DEFINED GAZER_VERSION_MAJOR) + set(GAZER_VERSION_MAJOR 1) +endif() +if(NOT DEFINED GAZER_VERSION_MINOR) + set(GAZER_VERSION_MINOR 0) +endif() +if(NOT DEFINED GAZER_VERSION_PATCH) + set(GAZER_VERSION_PATCH 0) +endif() +if(NOT DEFINED GAZER_VERSION_SUFFIX) + set(GAZER_VERSION_SUFFIX "") +endif() + +if (NOT PACKAGE_VERSION) + set(PACKAGE_VERSION + "${GAZER_VERSION_MAJOR}.${GAZER_VERSION_MINOR}.${GAZER_VERSION_PATCH}${GAZER_VERSION_SUFFIX}") +endif() + include(ExternalProject) list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_LIST_DIR}/cmake") @@ -53,7 +73,10 @@ include_directories(${Boost_INCLUDE_DIR}) add_definitions(-DBOOST_NO_RTTI -DBOOST_EXCEPTION_DISABLE -DBOOST_NO_EXCEPTIONS) # Project directories -include_directories(include) +set(GAZER_INCLUDE_DIR "${CMAKE_CURRENT_LIST_DIR}/include") +set(GAZER_MAIN_INCLUDE_DIR "${CMAKE_CURRENT_BINARY_DIR}/include") + +include_directories(${GAZER_INCLUDE_DIR} ${GAZER_MAIN_INCLUDE_DIR}) # Find out which solvers are enabled set(GAZER_ENABLE_SOLVERS "z3" CACHE STRING "Semicolon-separated list of solvers to build") @@ -61,6 +84,11 @@ set(GAZER_ENABLE_SOLVERS "z3" CACHE STRING "Semicolon-separated list of solvers add_subdirectory(src) add_subdirectory(tools) +# Generate the configuration file +configure_file( + ${GAZER_INCLUDE_DIR}/gazer/Config/gazer-config.h.cmake + ${GAZER_MAIN_INCLUDE_DIR}/gazer/Config/gazer-config.h) + option(GAZER_ENABLE_UNIT_TESTS "Enable unit tests" ON) if (GAZER_ENABLE_UNIT_TESTS) diff --git a/Dockerfile b/Dockerfile index 8aafa2df..2e0f92a3 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,6 +1,6 @@ FROM ubuntu:18.04 -ENV THETA_VERSION v2.4.0 +ENV THETA_VERSION v2.5.0 RUN apt-get update && \ apt-get install -y build-essential git cmake \ diff --git a/README.md b/README.md index a10e5901..9412cb84 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,7 @@ It provides a user-friendly end-to-end verification workflow, with support for m Currently we support two verification backends: * `gazer-theta` leverages the power of the [theta](https://github.com/ftsrg/theta) model checking framework. - * Currently, [v2.4.0](https://github.com/ftsrg/theta/releases/tag/v2.4.0) is tested, but newer releases might also work. + * Currently, [v2.5.0](https://github.com/ftsrg/theta/releases/tag/v2.5.0) is tested, but newer releases might also work. * `gazer-bmc` is gazer's built-in bounded model checking engine. # Usage diff --git a/doc/Contribution.md b/doc/Contribution.md index 302b7b95..0061edd5 100644 --- a/doc/Contribution.md +++ b/doc/Contribution.md @@ -1,5 +1,16 @@ # Contribution Guidelines +## General + +As the main repository is read-only, we suggest you to create your own [fork](https://help.github.com/articles/fork-a-repo/). +Within your fork, we also recommend to create new _branches_ for your development. +This enables us later on to easily integrate your work into the main repository by using [pull requests](https://help.github.com/articles/about-pull-requests/). + +As the framework is under development, we suggest you to [sync your fork](https://help.github.com/articles/syncing-a-fork/) often and merge the master branch into your development branch(es). + +Gazer uses [semantic versioning](https://semver.org/) in a `MAJOR.MINOR.PATCH` format, e.g., `1.2.3`. +The preferred development workflow is to bump the version number (see `CMakeLists.txt `) each time a PR gets merged. + ## Coding style and naming convention You can use `clang-format` with our provided style configuration file to reformat source code files to the appropriate coding style before commiting a patch. diff --git a/include/gazer/Config/gazer-config.h.cmake b/include/gazer/Config/gazer-config.h.cmake new file mode 100644 index 00000000..6d864434 --- /dev/null +++ b/include/gazer/Config/gazer-config.h.cmake @@ -0,0 +1,31 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2019 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +#ifndef GAZER_CONFIG_GAZER_CONFIG_H +#define GAZER_CONFIG_GAZER_CONFIG_H + +#define GAZER_VERSION_MAJOR ${GAZER_VERSION_MAJOR} + +#define GAZER_VERSION_MINOR ${GAZER_VERSION_MINOR} + +#define GAZER_VERSION_PATCH ${GAZER_VERSION_PATCH} + +#define GAZER_VERSION_SUFFIX ${GAZER_VERSION_SUFFIX} + +#define GAZER_VERSION_STRING "${PACKAGE_VERSION}" + +#endif \ No newline at end of file diff --git a/include/gazer/Core/Expr/ExprBuilder.h b/include/gazer/Core/Expr/ExprBuilder.h index e3ceab9c..857a5ee9 100644 --- a/include/gazer/Core/Expr/ExprBuilder.h +++ b/include/gazer/Core/Expr/ExprBuilder.h @@ -59,6 +59,16 @@ class ExprBuilder return IntLiteralExpr::Get(IntType::Get(mContext), value); } + ExprRef ArrayLit(ArrayType& arrTy, const ArrayLiteralExpr::MappingT& entries, const ExprRef& elze = nullptr) { + return ArrayLiteralExpr::Get(arrTy, entries, elze); + } + + ExprRef ArrayLit(const ArrayLiteralExpr::MappingT& entries, const ExprRef& elze = nullptr) { + assert(!entries.empty()); + const auto& [index, elem] = *entries.begin(); + return this->ArrayLit(ArrayType::Get(index->getType(), elem->getType()), entries, elze); + } + ExprRef BoolLit(bool value) { return value ? True() : False(); } ExprRef True() { return BoolLiteralExpr::True(BoolType::Get(mContext)); } ExprRef False() { return BoolLiteralExpr::False(BoolType::Get(mContext)); } diff --git a/include/gazer/LLVM/Instrumentation/Check.h b/include/gazer/LLVM/Instrumentation/Check.h index ec0123fa..cf3e7028 100644 --- a/include/gazer/LLVM/Instrumentation/Check.h +++ b/include/gazer/LLVM/Instrumentation/Check.h @@ -52,12 +52,21 @@ class Check : public llvm::ModulePass virtual bool mark(llvm::Function& function) = 0; protected: - /// Creates an error block with a gazer.error_code(i16 code) call and a terminating unreachable instruction. llvm::BasicBlock* createErrorBlock( llvm::Function& function, const llvm::Twine& name = "", llvm::Instruction* location = nullptr ); + /// Replaces all instructions matching the given predicate with an error call. + /// This function assumes that all instructions that follow a matching instruction within the + /// block are unreachable. + /// \return True if there were any matches; false otherwise. + bool replaceMatchingUnreachableWithError( + llvm::Function& function, + const llvm::Twine& errorBlockName, + std::function predicate + ); + CheckRegistry& getRegistry() const; private: diff --git a/include/gazer/LLVM/Instrumentation/Intrinsics.h b/include/gazer/LLVM/Instrumentation/Intrinsics.h index 084a6ee8..4ad3cfe0 100644 --- a/include/gazer/LLVM/Instrumentation/Intrinsics.h +++ b/include/gazer/LLVM/Instrumentation/Intrinsics.h @@ -50,7 +50,7 @@ class GazerIntrinsic enum class Overflow { - SAdd, UAdd, SSub, USub, SMul, UMul, SDiv, Shl + SAdd, UAdd, SSub, USub, SMul, UMul }; public: @@ -76,8 +76,6 @@ class GazerIntrinsic /// Returns a 'gazer.KIND.no_overflow.T(T left, T right)' intrinsic. static llvm::FunctionCallee GetOrInsertOverflowCheck(llvm::Module& module, Overflow kind, llvm::Type* type); - - static bool isPredicate(llvm::Function& function); }; } diff --git a/include/gazer/LLVM/Transform/Passes.h b/include/gazer/LLVM/Transform/Passes.h index 5d9800d8..bce13d39 100644 --- a/include/gazer/LLVM/Transform/Passes.h +++ b/include/gazer/LLVM/Transform/Passes.h @@ -39,6 +39,8 @@ llvm::Pass* createNormalizeVerifierCallsPass(); /// A simpler (and more restricted) inlining pass. llvm::Pass* createSimpleInlinerPass(llvm::Function& entry, InlineLevel level); +llvm::Pass* createCanonizeLoopExitsPass(); + } #endif diff --git a/src/Automaton/RecursiveToCyclicCfa.cpp b/src/Automaton/RecursiveToCyclicCfa.cpp index 8d7db1fc..c88ca288 100644 --- a/src/Automaton/RecursiveToCyclicCfa.cpp +++ b/src/Automaton/RecursiveToCyclicCfa.cpp @@ -42,15 +42,16 @@ class RecursiveToCyclicTransformer RecursiveToCyclicResult transform(); private: - void addUniqueErrorLocation(); void inlineCallIntoRoot(CallTransition* call, llvm::Twine suffix); + void createErrorTransition(Location* from, ExprPtr errorFieldExpr); + void createDummyErrorTransition(); private: Cfa* mRoot; CallGraph mCallGraph; llvm::SmallVector mTailRecursiveCalls; - Location* mError; - Variable* mErrorFieldVariable;; + Location* mError = nullptr; + Variable* mErrorFieldVariable = nullptr; llvm::DenseMap mInlinedLocations; llvm::DenseMap mInlinedVariables; std::unique_ptr mExprBuilder; @@ -61,8 +62,16 @@ class RecursiveToCyclicTransformer RecursiveToCyclicResult RecursiveToCyclicTransformer::transform() { - this->addUniqueErrorLocation(); + mError = mRoot->createErrorLocation(); + + // Connect error location + for (Location* loc : mRoot->nodes()) { + if (loc->isError() && loc != mError) { + this->createErrorTransition(loc, mRoot->getErrorFieldExpr(loc)); + } + } + // Collect tail-recursive calls for (Transition* edge : mRoot->edges()) { if (auto call = llvm::dyn_cast(edge)) { if (mCallGraph.isTailRecursive(call->getCalledAutomaton())) { @@ -78,6 +87,12 @@ RecursiveToCyclicResult RecursiveToCyclicTransformer::transform() this->inlineCallIntoRoot(call, "_inlined" + llvm::Twine(mInlineCnt++)); } + + if(mErrorFieldVariable == nullptr) { + // If there are no error locations, create one to use as goal + this->createDummyErrorTransition(); + } + mRoot->clearDisconnectedElements(); // Calculate the new call graph and remove unneeded automata. @@ -111,9 +126,10 @@ void RecursiveToCyclicTransformer::inlineCallIntoRoot(CallTransition* call, llvm rewrite[&local] = newLocal->getRefExpr(); } } - + // Clone input variables as well; we will insert an assign transition // with the initial values later. + std::vector inputTemporaries; for (Variable& input : callee->inputs()) { if (!callee->isOutput(&input)) { auto varname = (input.getName() + suffix).str(); @@ -122,6 +138,9 @@ void RecursiveToCyclicTransformer::inlineCallIntoRoot(CallTransition* call, llvm mInlinedVariables[newInput] = &input; //rewrite[input] = call->getInputArgument(i); rewrite[&input] = newInput->getRefExpr(); + + auto val = mRoot->createLocal(varname+"_", input.getType()); + inputTemporaries.emplace_back(val); } } @@ -141,9 +160,7 @@ void RecursiveToCyclicTransformer::inlineCallIntoRoot(CallTransition* call, llvm locToLocMap[&*origLoc] = newLoc; mInlinedLocations[newLoc] = origLoc; if (origLoc->isError()) { - mRoot->createAssignTransition(newLoc, mError, mExprBuilder->True(), { - { mErrorFieldVariable, callee->getErrorFieldExpr(origLoc) } - }); + this->createErrorTransition(newLoc, callee->getErrorFieldExpr(origLoc)); } } @@ -174,20 +191,36 @@ void RecursiveToCyclicTransformer::inlineCallIntoRoot(CallTransition* call, llvm // to the entry. std::vector recursiveInputArgs; for (size_t i = 0; i < callee->getNumInputs(); ++i) { - Variable* input = callee->getInput(i); + // result variable is different then original inputs #46 + // to simulate parallel assignments + Variable* input = inputTemporaries[i]; + Variable* realInput = callee->getInput(i); - auto variable = oldVarToNew[input]; - auto value = rewrite.walk(nestedCall->getInputArgument(*input)->getValue()); + auto variable = input; + auto value = rewrite.walk(nestedCall->getInputArgument(*realInput)->getValue()); if (variable->getRefExpr() != value) { // Do not add unneeded assignments (X := X). recursiveInputArgs.push_back({ - oldVarToNew[input], - value - }); + variable, + value + }); } } + for (size_t i = 0; i < callee->getNumInputs(); ++i) { + Variable* inputTemp = inputTemporaries[i]; + Variable* realInput = callee->getInput(i); + + auto variable = oldVarToNew[realInput]; + auto value = inputTemp->getRefExpr(); + + recursiveInputArgs.push_back({ + variable, + value + }); + } + // Create the assignment back-edge. mRoot->createAssignTransition( source, locToLocMap[callee->getEntry()], @@ -259,39 +292,33 @@ void RecursiveToCyclicTransformer::inlineCallIntoRoot(CallTransition* call, llvm mRoot->disconnectEdge(call); } -void RecursiveToCyclicTransformer::addUniqueErrorLocation() +void RecursiveToCyclicTransformer::createErrorTransition(Location *from, ExprPtr errorFieldExpr) { + assert(mError != nullptr); + assert(mErrorFieldVariable == nullptr || mErrorFieldVariable->getType() == errorFieldExpr->getType()); + + if(mErrorFieldVariable == nullptr) { + mErrorFieldVariable = mRoot->createLocal("__gazer_error_field", errorFieldExpr->getType()); + } + + mRoot->createAssignTransition(from, mError, BoolLiteralExpr::True(mRoot->getParent().getContext()), { + VariableAssignment { mErrorFieldVariable, errorFieldExpr } + }); +} + +void RecursiveToCyclicTransformer::createDummyErrorTransition() +{ + assert(mError != nullptr); + assert(mErrorFieldVariable == nullptr); + auto& intTy = IntType::Get(mRoot->getParent().getContext()); auto& ctx = mRoot->getParent().getContext(); - llvm::SmallVector errors; - for (Location* loc : mRoot->nodes()) { - if (loc->isError()) { - errors.push_back(loc); - } - } - - mError = mRoot->createErrorLocation(); + // A dummy error location will be used as a goal as there are no error locations in the automaton mErrorFieldVariable = mRoot->createLocal("__gazer_error_field", intTy); - - if (errors.empty()) { - // If there are no error locations in the main automaton, they might still exist in a called CFA. - // A dummy error location will be used as a goal. - mRoot->createAssignTransition(mRoot->getEntry(), mError, BoolLiteralExpr::False(ctx), { - VariableAssignment{ mErrorFieldVariable, IntLiteralExpr::Get(intTy, 0) } - }); - } else { - // The error location will be directly reachable from already existing error locations. - for (Location* err : errors) { - auto errorExpr = mRoot->getErrorFieldExpr(err); - - assert(errorExpr->getType().isIntType() && "Error expression must be arithmetic integers in the theta backend!"); - - mRoot->createAssignTransition(err, mError, BoolLiteralExpr::True(ctx), { - VariableAssignment { mErrorFieldVariable, errorExpr } - }); - } - } + mRoot->createAssignTransition(mRoot->getEntry(), mError, BoolLiteralExpr::False(ctx), { + VariableAssignment{ mErrorFieldVariable, IntLiteralExpr::Get(intTy, 0) } + }); } RecursiveToCyclicResult gazer::TransformRecursiveToCyclic(Cfa* cfa) diff --git a/src/LLVM/Automaton/InstToExpr.cpp b/src/LLVM/Automaton/InstToExpr.cpp index c623ba0d..c426f113 100644 --- a/src/LLVM/Automaton/InstToExpr.cpp +++ b/src/LLVM/Automaton/InstToExpr.cpp @@ -636,7 +636,6 @@ static GazerIntrinsic::Overflow getOverflowKind(llvm::StringRef name) HANDLE_PREFIX(GazerIntrinsic::SAddNoOverflowPrefix, SAdd) HANDLE_PREFIX(GazerIntrinsic::SSubNoOverflowPrefix, SSub) HANDLE_PREFIX(GazerIntrinsic::SMulNoOverflowPrefix, SMul) - HANDLE_PREFIX(GazerIntrinsic::SDivNoOverflowPrefix, SDiv) #undef HANDLE_PREFIX @@ -724,7 +723,6 @@ ExprPtr InstToExpr::handleOverflowPredicate(const llvm::CallInst& call) case GazerIntrinsic::Overflow::SAdd: result = mExprBuilder.Add(left, right); break; case GazerIntrinsic::Overflow::SSub: result = mExprBuilder.Sub(left, right); break; case GazerIntrinsic::Overflow::SMul: result = mExprBuilder.Mul(left, right); break; - case GazerIntrinsic::Overflow::SDiv: result = mExprBuilder.Div(left, right); break; default: llvm_unreachable("Unknown overflow kind!"); } @@ -754,7 +752,6 @@ ExprPtr InstToExpr::handleOverflowPredicate(const llvm::CallInst& call) case GazerIntrinsic::Overflow::SAdd: return handleSAddOverflow(left, right, mExprBuilder); case GazerIntrinsic::Overflow::SSub: return handleSSubOverflow(left, right, mExprBuilder); case GazerIntrinsic::Overflow::SMul: return handleSMulOverflow(left, right, mExprBuilder); - case GazerIntrinsic::Overflow::SDiv: return handleSDivOverflow(left, right, mExprBuilder); default: llvm_unreachable("Unknown overflow kind!"); } diff --git a/src/LLVM/Automaton/ModuleToAutomata.cpp b/src/LLVM/Automaton/ModuleToAutomata.cpp index 7aa65e92..18ad9062 100644 --- a/src/LLVM/Automaton/ModuleToAutomata.cpp +++ b/src/LLVM/Automaton/ModuleToAutomata.cpp @@ -326,6 +326,7 @@ void ModuleToCfa::createAutomata() // Create locations for the blocks for (BasicBlock* bb : loopOnlyBlocks) { + LLVM_DEBUG(llvm::dbgs() << "[LoopOnly] " << bb->getName() << "\n"); Location* entry = nested->createLocation(); Location* exit = isErrorBlock(bb) ? nested->createErrorLocation() : nested->createLocation(); @@ -382,12 +383,14 @@ void ModuleToCfa::createAutomata() // For the local variables, we only need to add the values not present in any of the loops. for (BasicBlock& bb : function) { + LLVM_DEBUG(llvm::dbgs() << "Translating function-level block " << bb.getName() << "\n"); for (Instruction& inst : bb) { + LLVM_DEBUG(llvm::dbgs().indent(2) << "Instruction " << inst.getName() << "\n"); if (auto loop = loopInfo->getLoopFor(&bb)) { // If the variable is an output of a loop, add it here as a local variable Variable* output = mGenCtx.getLoopCfa(loop).findOutput(&inst); if (output == nullptr && !hasUsesInBlockRange(&inst, functionBlocks)) { - LLVM_DEBUG(llvm::dbgs() << "Not adding " << inst << "\n"); + LLVM_DEBUG(llvm::dbgs().indent(4) << "Not adding (no uses in function) " << inst << "\n"); continue; } } diff --git a/src/LLVM/CMakeLists.txt b/src/LLVM/CMakeLists.txt index 8f6ccff2..a9911068 100644 --- a/src/LLVM/CMakeLists.txt +++ b/src/LLVM/CMakeLists.txt @@ -8,7 +8,6 @@ set(SOURCE_FILES Transform/TransformUtils.cpp Instrumentation/MarkFunctionEntries.cpp Instrumentation/Check.cpp - Instrumentation/DefaultChecks.cpp Instrumentation/Intrinsics.cpp Trace/TestHarnessGenerator.cpp Automaton/ModuleToAutomata.cpp @@ -32,7 +31,9 @@ set(SOURCE_FILES Automaton/ExtensionPoints.cpp Automaton/ValueOrMemoryObject.cpp Analysis/PDG.cpp -) + Instrumentation/Checks/AssertionFailCheck.cpp + Instrumentation/Checks/DivisionByZeroCheck.cpp + Instrumentation/Checks/SignedIntegerOverflowCheck.cpp Transform/LoopExitCanonizationPass.cpp) llvm_map_components_to_libnames(GAZER_LLVM_LIBS core irreader transformutils scalaropts ipo) message(STATUS "Using LLVM libraries: ${GAZER_LLVM_LIBS}") diff --git a/src/LLVM/ClangFrontend.cpp b/src/LLVM/ClangFrontend.cpp index 53f45fec..0405babe 100644 --- a/src/LLVM/ClangFrontend.cpp +++ b/src/LLVM/ClangFrontend.cpp @@ -240,6 +240,9 @@ void ClangOptions::addSanitizerFlag(llvm::StringRef flag) void ClangOptions::createArgumentList(std::vector& args) { if (!mSanitizerFlags.empty()) { - args.emplace_back("-fsanitize-trap=" + llvm::join(mSanitizerFlags, ",")); + auto sanitizerNames = llvm::join(mSanitizerFlags, ","); + + args.emplace_back("-fsanitize=" + sanitizerNames); + args.emplace_back("-fno-sanitize-recover=" + sanitizerNames); } } diff --git a/src/LLVM/FrontendConfig.cpp b/src/LLVM/FrontendConfig.cpp index de0ea3b2..1b2d17f4 100644 --- a/src/LLVM/FrontendConfig.cpp +++ b/src/LLVM/FrontendConfig.cpp @@ -18,6 +18,7 @@ #include "gazer/LLVM/LLVMFrontend.h" #include "gazer/LLVM/Instrumentation/DefaultChecks.h" #include "gazer/Support/Warnings.h" +#include "gazer/Config/gazer-config.h" #include #include @@ -82,7 +83,6 @@ void FrontendConfig::createChecks(std::vector>& checks) // Do the defaults fragments.push_back("assertion-fail"); fragments.push_back("div-by-zero"); - fragments.push_back("signed-overflow"); } else if (filter == AllChecksSetting) { // Add all registered checks for (auto& [name, factory] : mFactories) { @@ -108,6 +108,6 @@ void FrontendConfig::createChecks(std::vector>& checks) void FrontendConfigWrapper::PrintVersion(llvm::raw_ostream& os) { os << "gazer - a formal verification frontend\n"; - os << " version 0.1\n"; - os << " LLVM version 9.0\n"; + os.indent(2) << "version " << GAZER_VERSION_STRING << "\n"; + os.indent(2) << "LLVM version " << LLVM_VERSION_STRING << "\n"; } diff --git a/src/LLVM/Instrumentation/Check.cpp b/src/LLVM/Instrumentation/Check.cpp index 1555c825..3f09c06a 100644 --- a/src/LLVM/Instrumentation/Check.cpp +++ b/src/LLVM/Instrumentation/Check.cpp @@ -76,6 +76,47 @@ llvm::BasicBlock* Check::createErrorBlock( return errorBB; } +bool Check::replaceMatchingUnreachableWithError( + llvm::Function& function, + const llvm::Twine& errorBlockName, + std::function predicate) +{ + llvm::SmallVector errorCalls; + for (Instruction& inst : llvm::instructions(function)) { + if (predicate(inst)) { + errorCalls.emplace_back(&inst); + } + } + + if (errorCalls.empty()) { + return false; + } + + for (llvm::Instruction* inst : errorCalls) { + // Replace error calls with an unconditional jump to an error block + BasicBlock* errorBB = this->createErrorBlock( + function, + errorBlockName, + inst + ); + + // Remove all instructions from the error call to the terminator + auto it = inst->getIterator(); + auto terminator = inst->getParent()->getTerminator()->getIterator(); + while (it != terminator) { + auto instToDelete = it++; + instToDelete->eraseFromParent(); + } + + llvm::ReplaceInstWithInst( + &*terminator, + llvm::BranchInst::Create(errorBB) + ); + } + + return true; +} + CheckRegistry& Check::getRegistry() const { return *mRegistry; } void Check::setCheckRegistry(CheckRegistry& registry) diff --git a/src/LLVM/Instrumentation/Checks/AssertionFailCheck.cpp b/src/LLVM/Instrumentation/Checks/AssertionFailCheck.cpp new file mode 100644 index 00000000..cb2ed852 --- /dev/null +++ b/src/LLVM/Instrumentation/Checks/AssertionFailCheck.cpp @@ -0,0 +1,77 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2020 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +#include "gazer/LLVM/Instrumentation/DefaultChecks.h" + +#include +#include + +using namespace gazer; +using namespace llvm; + +namespace +{ + +/// This check ensures that no assertion failure instructions are reachable. +class AssertionFailCheck final : public Check +{ +public: + static char ID; + + AssertionFailCheck() + : Check(ID) + {} + + bool mark(llvm::Function& function) override; + + llvm::StringRef getErrorDescription() const override { return "Assertion failure"; } +}; + +} // namespace + +char AssertionFailCheck::ID; + +static bool isCallToErrorFunction(llvm::Instruction& inst) +{ + auto call = llvm::dyn_cast(&inst); + if (call == nullptr) { + return false; + } + + if (call->getCalledFunction() == nullptr) { + return false; + } + + auto name = call->getCalledFunction()->getName(); + + return name == "__VERIFIER_error" + || name == "__assert_fail" + || name == "__gazer_error" + || name == "reach_error"; +} + +bool AssertionFailCheck::mark(llvm::Function &function) +{ + return this->replaceMatchingUnreachableWithError( + function, "error.assert_fail", isCallToErrorFunction + ); +} + +std::unique_ptr gazer::checks::createAssertionFailCheck(ClangOptions& options) +{ + return std::make_unique(); +} diff --git a/src/LLVM/Instrumentation/Checks/DivisionByZeroCheck.cpp b/src/LLVM/Instrumentation/Checks/DivisionByZeroCheck.cpp new file mode 100644 index 00000000..e09d19f6 --- /dev/null +++ b/src/LLVM/Instrumentation/Checks/DivisionByZeroCheck.cpp @@ -0,0 +1,104 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2020 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +#include "gazer/LLVM/Instrumentation/DefaultChecks.h" + +#include +#include +#include + +using namespace gazer; +using namespace llvm; + +namespace +{ + +/// Checks for division by zero errors. +class DivisionByZeroCheck final : public Check +{ +public: + static char ID; + + DivisionByZeroCheck() + : Check(ID) + {} + + bool mark(llvm::Function& function) override; + + llvm::StringRef getErrorDescription() const override + { + return "Divison by zero"; + } +}; + +} // namespace + +char DivisionByZeroCheck::ID; + +static bool isDivisionInst(unsigned opcode) +{ + return opcode == Instruction::SDiv || opcode == Instruction::UDiv; +} + +bool DivisionByZeroCheck::mark(llvm::Function& function) +{ + auto& context = function.getContext(); + + std::vector divs; + for (llvm::Instruction& inst : instructions(function)) { + if (isDivisionInst(inst.getOpcode())) { + divs.push_back(&inst); + } + } + + if (divs.empty()) { + return false; + } + + IRBuilder<> builder(context); + for (llvm::Instruction* inst : divs) { + BasicBlock* errorBB = this->createErrorBlock( + function, + "error.divzero", + inst + ); + + BasicBlock* bb = inst->getParent(); + llvm::Value* rhs = inst->getOperand(1); + + builder.SetInsertPoint(inst); + auto icmp = builder.CreateICmpNE( + rhs, builder.getInt(llvm::APInt( + rhs->getType()->getIntegerBitWidth(), 0 + )) + ); + + BasicBlock* newBB = bb->splitBasicBlock(inst); + builder.ClearInsertionPoint(); + llvm::ReplaceInstWithInst( + bb->getTerminator(), + builder.CreateCondBr(icmp, newBB, errorBB) + ); + } + + return true; +} + +std::unique_ptr gazer::checks::createDivisionByZeroCheck(ClangOptions& options) +{ + return std::make_unique(); +} diff --git a/src/LLVM/Instrumentation/Checks/SignedIntegerOverflowCheck.cpp b/src/LLVM/Instrumentation/Checks/SignedIntegerOverflowCheck.cpp new file mode 100644 index 00000000..079988cb --- /dev/null +++ b/src/LLVM/Instrumentation/Checks/SignedIntegerOverflowCheck.cpp @@ -0,0 +1,202 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2020 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +#include "gazer/LLVM/Instrumentation/DefaultChecks.h" +#include "gazer/LLVM/Instrumentation/Intrinsics.h" +#include "gazer/Support/Warnings.h" + +#include +#include +#include +#include +#include + +using namespace gazer; +using namespace llvm; + +namespace +{ + +class SignedIntegerOverflowCheck final : public Check +{ + static constexpr char IntrinsicPattern[] = "^llvm\\.(u|s)(add|sub|mul)\\.with\\.overflow\\.i([0-9]+)$"; +public: + static char ID; + + SignedIntegerOverflowCheck() + : Check(ID), mIntrinsicRegex(IntrinsicPattern) + {} + + bool mark(llvm::Function& function) override; + + StringRef getErrorDescription() const override + { + return "Signed integer overflow"; + } +private: + bool isOverflowIntrinsic(llvm::Function* callee, GazerIntrinsic::Overflow* overflowKind); + +private: + llvm::Regex mIntrinsicRegex; +}; + +} // namespace + +char SignedIntegerOverflowCheck::ID; + +bool SignedIntegerOverflowCheck::isOverflowIntrinsic( + llvm::Function* callee, + GazerIntrinsic::Overflow* overflowKind) +{ + if (callee == nullptr) { + return false; + } + + // [ input, signedness, op, width ] + llvm::SmallVector groups; + if (!mIntrinsicRegex.match(callee->getName(), &groups)) { + return false; + } + + // Determine signedness + bool isSigned; + if (groups[1] == "s") { + isSigned = true; + } else if (groups[1] == "u") { + isSigned = false; + } else { + llvm_unreachable("Unknown overflow intrinsic signedness!"); + } + + llvm::StringRef op = groups[2]; + if (isSigned) { + *overflowKind = llvm::StringSwitch(op) + .Case("add", GazerIntrinsic::Overflow::SAdd) + .Case("sub", GazerIntrinsic::Overflow::SSub) + .Case("mul", GazerIntrinsic::Overflow::SMul); + } else { + *overflowKind = llvm::StringSwitch(op) + .Case("add", GazerIntrinsic::Overflow::UAdd) + .Case("sub", GazerIntrinsic::Overflow::USub) + .Case("mul", GazerIntrinsic::Overflow::UMul); + } + + return true; +} + +static bool isOverflowTrapCall(llvm::Instruction& inst) +{ + auto call = llvm::dyn_cast(&inst); + if (call == nullptr) { + return false; + } + + auto callee = call->getCalledFunction(); + if (callee == nullptr) { + return false; + } + + auto name = callee->getName(); + + return name == "__ubsan_handle_add_overflow_abort" + || name == "__ubsan_handle_sub_overflow_abort" + || name == "__ubsan_handle_mul_overflow_abort"; +} + +bool SignedIntegerOverflowCheck::mark(llvm::Function &function) +{ + bool modified = false; + + llvm::Module& module = *function.getParent(); + llvm::IRBuilder<> builder(module.getContext()); + + llvm::SmallVector, 16> targets; + llvm::SmallVector sanitizerCalls; + + for (Instruction& inst : instructions(function)) { + if (auto call = dyn_cast(&inst)) { + GazerIntrinsic::Overflow ovrKind; + if (this->isOverflowIntrinsic(call->getCalledFunction(), &ovrKind)) { + targets.emplace_back(call, ovrKind); + } + } + } + + // A call to `llvm.*.with.overflow.iN` returns a {iN, i1} pair where the + // second element is the flag which tells us whether an overflow has occured. + // As such, we will replace all uses of the second element with our own overflow + // check, and all uses of the first element with the actual operation. + for (auto& [call, ovrKind] : targets) { + llvm::Type* valTy = call->getType()->getStructElementType(0); + + auto lhs = call->getArgOperand(0); + auto rhs = call->getArgOperand(1); + + auto overflowCheckFn = GazerIntrinsic::GetOrInsertOverflowCheck(module, ovrKind, valTy); + + builder.SetInsertPoint(call); + auto check = builder.CreateCall(overflowCheckFn, { lhs, rhs }, "ovr_check"); + auto checkFail = builder.CreateNot(check); + + llvm::Value* binOp = nullptr; + switch (ovrKind) { + case GazerIntrinsic::Overflow::SAdd: binOp = builder.CreateAdd(lhs, rhs, "", /*HasNUW=*/false, /*HasNSW=*/true); break; + case GazerIntrinsic::Overflow::SSub: binOp = builder.CreateSub(lhs, rhs, "", /*HasNUW=*/false, /*HasNSW=*/true); break; + case GazerIntrinsic::Overflow::SMul: binOp = builder.CreateMul(lhs, rhs, "", /*HasNUW=*/false, /*HasNSW=*/true); break; + case GazerIntrinsic::Overflow::UAdd: binOp = builder.CreateAdd(lhs, rhs, "", /*HasNUW=*/true, /*HasNSW=*/false); break; + case GazerIntrinsic::Overflow::USub: binOp = builder.CreateSub(lhs, rhs, "", /*HasNUW=*/true, /*HasNSW=*/false); break; + case GazerIntrinsic::Overflow::UMul: binOp = builder.CreateMul(lhs, rhs, "", /*HasNUW=*/true, /*HasNSW=*/false); break; + } + + assert(binOp != nullptr && "Unknown overflow kind!"); + + // Check the uses of 'call' + for (auto ui = call->user_begin(), ue = call->user_end(); ui != ue;) { + auto current = ui++; + if (auto extract = llvm::dyn_cast(*current)) { + unsigned firstIdx = extract->getIndices()[0]; + if (firstIdx == 0) { + extract->replaceAllUsesWith(binOp); + } else if (firstIdx == 1) { + extract->replaceAllUsesWith(checkFail); + } else { + llvm_unreachable("Unknown overflow struct index!"); + } + + extract->dropAllReferences(); + extract->eraseFromParent(); + } + } + + call->dropAllReferences(); + call->eraseFromParent(); + + modified = true; + } + + // Find trap calls and replace them with our own error block + modified |= this->replaceMatchingUnreachableWithError(function, "error.signed_overflow", isOverflowTrapCall); + + return modified; +} + +std::unique_ptr gazer::checks::createSignedIntegerOverflowCheck(ClangOptions& options) +{ + options.addSanitizerFlag("signed-integer-overflow"); + return std::make_unique(); +} + diff --git a/src/LLVM/Instrumentation/DefaultChecks.cpp b/src/LLVM/Instrumentation/DefaultChecks.cpp deleted file mode 100644 index 14e73bc5..00000000 --- a/src/LLVM/Instrumentation/DefaultChecks.cpp +++ /dev/null @@ -1,323 +0,0 @@ -//==-------------------------------------------------------------*- C++ -*--==// -// -// Copyright 2019 Contributors to the Gazer project -// -// Licensed under the Apache License, Version 2.0 (the "License"); -// you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, -// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -// See the License for the specific language governing permissions and -// limitations under the License. -// -//===----------------------------------------------------------------------===// -#include "gazer/LLVM/Instrumentation/DefaultChecks.h" -#include "gazer/LLVM/Instrumentation/Intrinsics.h" - -#include -#include -#include -#include -#include - -using namespace gazer; -using namespace llvm; - -namespace -{ - -bool isCallToErrorFunction(llvm::Instruction& inst) { - auto call = llvm::dyn_cast(&inst); - if (call == nullptr) { - return false; - } - - if (call->getCalledFunction() == nullptr) { - return false; - } - - auto name = call->getCalledFunction()->getName(); - - return name == "__VERIFIER_error" - || name == "__assert_fail" - || name == "__gazer_error" - || name == "reach_error"; -} - -/// This check ensures that no assertion failure instructions are reachable. -class AssertionFailCheck final : public Check -{ -public: - static char ID; - - AssertionFailCheck() - : Check(ID) - {} - - bool mark(llvm::Function& function) override - { - llvm::SmallVector errorCalls; - for (Instruction& inst : llvm::instructions(function)) { - if (isCallToErrorFunction(inst)) { - errorCalls.emplace_back(&inst); - } - } - - for (llvm::Instruction* inst : errorCalls) { - // Replace error calls with an unconditional jump to an error block - BasicBlock* errorBB = this->createErrorBlock( - function, - "error.assert_fail", - inst - ); - - // Remove all instructions from the error call to the terminator - auto it = inst->getIterator(); - auto terminator = inst->getParent()->getTerminator()->getIterator(); - while (it != terminator) { - auto instToDelete = it++; - instToDelete->eraseFromParent(); - } - - llvm::ReplaceInstWithInst( - &*terminator, - llvm::BranchInst::Create(errorBB) - ); - } - - return true; - } - - llvm::StringRef getErrorDescription() const override { return "Assertion failure"; } -}; - -bool isDiv(unsigned opcode) { - return opcode == Instruction::SDiv || opcode == Instruction::UDiv; -} - -/// Checks for division by zero errors. -class DivisionByZeroCheck final : public Check -{ -public: - static char ID; - - DivisionByZeroCheck() - : Check(ID) - {} - - bool mark(llvm::Function& function) override - { - auto& context = function.getContext(); - - std::vector divs; - for (llvm::Instruction& inst : instructions(function)) { - if (isDiv(inst.getOpcode())) { - divs.push_back(&inst); - } - } - - if (divs.empty()) { - return false; - } - - unsigned divCnt = 0; - IRBuilder<> builder(context); - for (llvm::Instruction* inst : divs) { - BasicBlock* errorBB = this->createErrorBlock( - function, - "error.divzero" + llvm::Twine(divCnt++), - inst - ); - - BasicBlock* bb = inst->getParent(); - llvm::Value* rhs = inst->getOperand(1); - - builder.SetInsertPoint(inst); - auto icmp = builder.CreateICmpNE( - rhs, builder.getInt(llvm::APInt( - rhs->getType()->getIntegerBitWidth(), 0 - )) - ); - - BasicBlock* newBB = bb->splitBasicBlock(inst); - builder.ClearInsertionPoint(); - llvm::ReplaceInstWithInst( - bb->getTerminator(), - builder.CreateCondBr(icmp, newBB, errorBB) - ); - } - - return true; - } - - llvm::StringRef getErrorDescription() const override { return "Divison by zero"; } -}; - -/// Checks for over- and underflow in signed integer operations. -class SignedIntegerOverflowCheck : public Check -{ - static constexpr char IntrinsicPattern[] = "^llvm\\.(u|s)(add|sub|mul)\\.with\\.overflow\\.i([0-9]+)$"; -public: - static char ID; - - SignedIntegerOverflowCheck() - : Check(ID), mIntrinsicRegex(IntrinsicPattern) - {} - - bool mark(llvm::Function& function) override; - - llvm::StringRef getErrorDescription() const override { return "Signed integer overflow"; } -private: - bool isOverflowIntrinsic(llvm::Function* callee, GazerIntrinsic::Overflow* ovrKind); - bool isSanitizerCall(llvm::Function* callee); - -private: - llvm::Regex mIntrinsicRegex; -}; - -char DivisionByZeroCheck::ID; -char AssertionFailCheck::ID; -char SignedIntegerOverflowCheck::ID; - -} // end anonymous namespace - -bool SignedIntegerOverflowCheck::isOverflowIntrinsic(llvm::Function* callee, GazerIntrinsic::Overflow* ovrKind) -{ - if (callee == nullptr) { - return false; - } - - // [ input, signedness, op, width ] - llvm::SmallVector groups; - if (!mIntrinsicRegex.match(callee->getName(), &groups)) { - return false; - } - - // Determine signedness - bool isSigned; - if (groups[1] == "s") { - isSigned = true; - } else if (groups[1] == "u") { - isSigned = false; - } else { - llvm_unreachable("Unknown overflow intrinsic signedness!"); - } - - llvm::StringRef op = groups[2]; - if (op == "add") { - *ovrKind = isSigned ? GazerIntrinsic::Overflow::SAdd : GazerIntrinsic::Overflow::UAdd; - } else if (op == "sub") { - *ovrKind = isSigned ? GazerIntrinsic::Overflow::SSub : GazerIntrinsic::Overflow::USub; - } else if (op == "mul") { - *ovrKind = isSigned ? GazerIntrinsic::Overflow::SMul : GazerIntrinsic::Overflow::UMul; - } else { - llvm_unreachable("Unknown overflow intrinsic operation!"); - } - - return true; -} - -bool SignedIntegerOverflowCheck::mark(llvm::Function& function) -{ - llvm::Module& module = *function.getParent(); - llvm::IRBuilder<> builder(module.getContext()); - - llvm::SmallVector, 16> targets; - llvm::SmallVector sanitizerCalls; - - for (Instruction& inst : instructions(function)) { - if (auto call = dyn_cast(&inst)) { - GazerIntrinsic::Overflow ovrKind; - if (this->isOverflowIntrinsic(call->getCalledFunction(), &ovrKind)) { - targets.emplace_back(call, ovrKind); - } - } - } - - // A call to `llvm.*.with.overflow.iN` returns a {iN, i1} pair where the - // second element is the flag which tells us whether an overflow has occured. - // As such, we will replace all uses of the second element with our own overflow - // check, and all uses of the first element with the actual operation. - for (auto& [call, ovrKind] : targets) { - llvm::Type* valTy = call->getType()->getStructElementType(0); - - auto lhs = call->getArgOperand(0); - auto rhs = call->getArgOperand(1); - - auto fn = GazerIntrinsic::GetOrInsertOverflowCheck(module, ovrKind, valTy); - - builder.SetInsertPoint(call); - auto check = builder.CreateCall(fn, { lhs, rhs }, "ovr_check"); - auto ovrFail = builder.CreateNot(check); - - auto prev = builder.GetInsertPoint(); - - llvm::Value* binOp; - switch (ovrKind) { - case GazerIntrinsic::Overflow::SAdd: binOp = builder.CreateAdd(lhs, rhs, "", /*HasNUW=*/false, /*HasNSW=*/true); break; - case GazerIntrinsic::Overflow::SSub: binOp = builder.CreateSub(lhs, rhs, "", /*HasNUW=*/false, /*HasNSW=*/true); break; - case GazerIntrinsic::Overflow::SMul: binOp = builder.CreateMul(lhs, rhs, "", /*HasNUW=*/false, /*HasNSW=*/true); break; - case GazerIntrinsic::Overflow::UAdd: binOp = builder.CreateAdd(lhs, rhs, "", /*HasNUW=*/true, /*HasNSW=*/false); break; - case GazerIntrinsic::Overflow::USub: binOp = builder.CreateSub(lhs, rhs, "", /*HasNUW=*/true, /*HasNSW=*/false); break; - case GazerIntrinsic::Overflow::UMul: binOp = builder.CreateMul(lhs, rhs, "", /*HasNUW=*/true, /*HasNSW=*/false); break; - } - - assert(binOp != nullptr && "Unknown overflow kind!"); - - BasicBlock* bb = call->getParent(); - BasicBlock* errorBB = this->createErrorBlock(function, "error.ovr", call); - - BasicBlock* newBB = bb->splitBasicBlock(std::next(prev)); - builder.ClearInsertionPoint(); - llvm::ReplaceInstWithInst( - bb->getTerminator(), - builder.CreateCondBr(check, newBB, errorBB) - ); - - // Clean up the original sanitizer instrumentation - - auto ui = call->user_begin(); - auto ue = call->user_end(); - - while (ui != ue) { - auto curr = ui++; - if (auto extract = dyn_cast(*curr)) { - unsigned index = extract->getIndices()[0]; - if (index == 0) { - extract->replaceAllUsesWith(binOp); - } else if (index == 1) { - extract->replaceAllUsesWith(ovrFail); - } else { - llvm_unreachable("Unknown index for a { iN, i1 } struct!"); - } - extract->dropAllReferences(); - extract->eraseFromParent(); - } - } - - call->dropAllReferences(); - call->eraseFromParent(); - } - - return true; -} - -std::unique_ptr gazer::checks::createDivisionByZeroCheck(ClangOptions& options) -{ - return std::make_unique(); -} - -std::unique_ptr gazer::checks::createAssertionFailCheck(ClangOptions& options) -{ - return std::make_unique(); -} - -std::unique_ptr gazer::checks::createSignedIntegerOverflowCheck(ClangOptions& options) -{ - options.addSanitizerFlag("signed-integer-overflow"); - return std::make_unique(); -} diff --git a/src/LLVM/Instrumentation/Intrinsics.cpp b/src/LLVM/Instrumentation/Intrinsics.cpp index 9b05dbb9..b6d298e2 100644 --- a/src/LLVM/Instrumentation/Intrinsics.cpp +++ b/src/LLVM/Instrumentation/Intrinsics.cpp @@ -108,7 +108,6 @@ llvm::FunctionCallee GazerIntrinsic::GetOrInsertOverflowCheck(llvm::Module& modu case Overflow::USub: name = USubNoOverflowPrefix; break; case Overflow::SMul: name = SMulNoOverflowPrefix; break; case Overflow::UMul: name = UMulNoOverflowPrefix; break; - case Overflow::SDiv: name = SDivNoOverflowPrefix; break; default: llvm_unreachable("Unknown overflow kind!"); } diff --git a/src/LLVM/LLVMFrontend.cpp b/src/LLVM/LLVMFrontend.cpp index b3debc1f..b85059b4 100644 --- a/src/LLVM/LLVMFrontend.cpp +++ b/src/LLVM/LLVMFrontend.cpp @@ -373,6 +373,7 @@ void LLVMFrontend::registerLateOptimizations() // to work properly as it relies on loop preheaders being available. mPassManager.add(llvm::createCFGSimplificationPass()); mPassManager.add(llvm::createLoopSimplifyPass()); + mPassManager.add(gazer::createCanonizeLoopExitsPass()); } auto LLVMFrontend::FromInputFile( diff --git a/src/LLVM/LLVMTraceBuilder.cpp b/src/LLVM/LLVMTraceBuilder.cpp index 07d12f74..269586e7 100644 --- a/src/LLVM/LLVMTraceBuilder.cpp +++ b/src/LLVM/LLVMTraceBuilder.cpp @@ -273,6 +273,9 @@ auto LLVMTraceBuilder::build( undefs.insert(call); } else if (callee->getName().startswith("gazer.dummy")) { // These functions are the part of an "invisible" instrumentation and should be ignored. + } else if (callee->getName().startswith(GazerIntrinsic::NoOverflowPrefix)) { + // Do not show the intrinsic functions here + // TODO: We could add some information about the overflow (e.g. the unrepresentable value). } else if (callee->isDeclaration() && !call->getType()->isVoidTy()) { // This is a function call to a nondetermistic function. auto variable = mCfaToLlvmTrace.getVariableForValue(loc->getAutomaton(), call); diff --git a/src/LLVM/Transform/LoopExitCanonizationPass.cpp b/src/LLVM/Transform/LoopExitCanonizationPass.cpp new file mode 100644 index 00000000..59f17048 --- /dev/null +++ b/src/LLVM/Transform/LoopExitCanonizationPass.cpp @@ -0,0 +1,115 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2020 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +#include "gazer/LLVM/Transform/Passes.h" + +#include +#include +#include + +namespace +{ + +class LoopExitCanonizationPass : public llvm::FunctionPass +{ +public: + static char ID; + + LoopExitCanonizationPass() + : FunctionPass(ID) + {} + + void getAnalysisUsage(llvm::AnalysisUsage& au) const override + { + au.addRequired(); + } + + bool runOnFunction(llvm::Function& function) override; +}; + +} // namespace + +char LoopExitCanonizationPass::ID; + +static void adjustPhiNodes(llvm::BasicBlock* succ, llvm::BasicBlock* oldBB, llvm::BasicBlock* newBB) +{ + auto it = succ->begin(); + while (auto phi = llvm::dyn_cast(it)) { + phi->replaceIncomingBlockWith(oldBB, newBB); + ++it; + } +} + +static bool transformExitsInLoop(llvm::LoopInfo& loopInfo, llvm::Loop* loop) +{ + llvm::Loop* parent = loop->getParentLoop(); + if (parent == nullptr) { + // This is a top-level loop, all possibly descendants are outside + return false; + } + + llvm::SmallVector exitingBlocks; + loop->getExitingBlocks(exitingBlocks); + + if (exitingBlocks.empty()) { + return false; + } + + for (llvm::BasicBlock* bb : exitingBlocks) { + // TODO: Switch instruction terminator + auto br = llvm::dyn_cast(bb->getTerminator()); + if (br == nullptr) { + continue; + } + + for (unsigned i = 0; i < br->getNumSuccessors(); ++i) { + auto succ = br->getSuccessor(i); + + if (!loop->contains(succ) && !parent->contains(succ)) { + // We have a successor outside of the loop and parent loop. Create a new block + // for the parent loop which will serve as the destination for this jump. + auto newBB = llvm::BasicBlock::Create(bb->getContext(), "loop_exit", bb->getParent()); + llvm::BranchInst::Create(succ, newBB); + + br->setSuccessor(i, newBB); + adjustPhiNodes(succ, bb, newBB); + parent->addBasicBlockToLoop(newBB, loopInfo); + } + } + } + + return true; +} + +bool LoopExitCanonizationPass::runOnFunction(llvm::Function& function) +{ + llvm::LoopInfo& loopInfo = getAnalysis().getLoopInfo(); + + auto loopsInPostorder = loopInfo.getLoopsInPreorder(); + llvm::reverse(loopsInPostorder); + + bool changed = false; + for (llvm::Loop* loop : loopsInPostorder) { + changed |= transformExitsInLoop(loopInfo, loop); + } + + return changed; +} + +llvm::Pass* gazer::createCanonizeLoopExitsPass() { + return new LoopExitCanonizationPass(); +} \ No newline at end of file diff --git a/src/SolverZ3/CMakeLists.txt b/src/SolverZ3/CMakeLists.txt index 3406b682..aac20f66 100644 --- a/src/SolverZ3/CMakeLists.txt +++ b/src/SolverZ3/CMakeLists.txt @@ -4,20 +4,22 @@ set(SOURCE_FILES ) # Z3 + +set(Z3_INCLUDE_DIR "${CMAKE_CURRENT_BINARY_DIR}/vendor/src/z3_download/include") +set(Z3_LIBRARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/vendor/src/z3_download/bin") + ExternalProject_Add(z3_download PREFIX vendor # Download URL https://github.com/Z3Prover/z3/releases/download/z3-4.8.6/z3-4.8.6-x64-ubuntu-16.04.zip URL_HASH SHA1=1663a7825c45f24642045dfcc5e100d65c1b6b1e + BUILD_BYPRODUCTS "${Z3_LIBRARY_DIR}/libz3.so" CONFIGURE_COMMAND "" BUILD_COMMAND "" UPDATE_COMMAND "" INSTALL_COMMAND "" ) -set(Z3_INCLUDE_DIR "${CMAKE_CURRENT_BINARY_DIR}/vendor/src/z3_download/include") -set(Z3_LIBRARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/vendor/src/z3_download/bin") - message("Z3 includes are ${Z3_INCLUDE_DIR}") # Z3 diff --git a/src/SolverZ3/Z3Solver.cpp b/src/SolverZ3/Z3Solver.cpp index acd07c9f..1d061d5e 100644 --- a/src/SolverZ3/Z3Solver.cpp +++ b/src/SolverZ3/Z3Solver.cpp @@ -19,6 +19,8 @@ #include "gazer/Support/Float.h" +#include + #include #include #include @@ -381,9 +383,9 @@ Z3Handle Z3ExprTransformer::handleTupleType(TupleType& tupTy) Z3AstHandle Z3ExprTransformer::translateLiteral(const ExprRef& expr) { if (auto bvLit = llvm::dyn_cast(expr)) { - return createHandle(Z3_mk_unsigned_int64( - mZ3Context, bvLit->getValue().getZExtValue(), typeToSort(bvLit->getType()) - )); + llvm::SmallString<20> buffer; + bvLit->getValue().toStringUnsigned(buffer, 10); + return createHandle(Z3_mk_numeral(mZ3Context, buffer.c_str(), typeToSort(bvLit->getType()))); } if (auto bl = llvm::dyn_cast(expr)) { diff --git a/test/lit.cfg b/test/lit.cfg index 48212f31..65ddff8d 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -13,7 +13,7 @@ config.excludes = [ ] try: - gazer_tools_dir = os.environ['GAZER_TOOLS_DIR'] + gazer_tools_dir = os.path.abspath(os.environ['GAZER_TOOLS_DIR']) except KeyError: lit_config.fatal('Missing GAZER_TOOLS_DIR environment variable.') diff --git a/test/theta/cfa/counter.c b/test/theta/cfa/counter.c index 60e77f6e..2f26da35 100644 --- a/test/theta/cfa/counter.c +++ b/test/theta/cfa/counter.c @@ -1,4 +1,4 @@ -// RUN: %theta -model-only "%s" -o "%t" +// RUN: %theta -model-only -math-int "%s" -o "%t" // RUN: cat "%t" | /usr/bin/diff -B -Z "%p/Expected/counter.theta" - #include diff --git a/test/theta/verif/base/loops1.c b/test/theta/verif/base/loops1.c index f71e3fb3..07ff225f 100644 --- a/test/theta/verif/base/loops1.c +++ b/test/theta/verif/base/loops1.c @@ -1,4 +1,6 @@ -// RUN: %theta -memory=havoc "%s" | FileCheck "%s" +// RUN: %theta -memory=havoc -math-int "%s" | FileCheck "%s" +// RUN: %theta --domain EXPL --refinement UNSAT_CORE "%s" | FileCheck "%s" + // CHECK: Verification SUCCESSFUL extern int __VERIFIER_nondet_int(void); diff --git a/test/theta/verif/base/loops2_fail.c b/test/theta/verif/base/loops2_fail.c index a5b671ea..36e0804e 100644 --- a/test/theta/verif/base/loops2_fail.c +++ b/test/theta/verif/base/loops2_fail.c @@ -1,4 +1,5 @@ -// RUN: %theta -memory=havoc "%s" | FileCheck "%s" +// RUN: %theta -memory=havoc -math-int "%s" | FileCheck "%s" +// RUN: %theta --domain EXPL --refinement UNSAT_CORE "%s" | FileCheck "%s" // CHECK: Verification FAILED #include diff --git a/test/theta/verif/base/loops3_fail.c b/test/theta/verif/base/loops3_fail.c index b704f1a5..0951f34f 100644 --- a/test/theta/verif/base/loops3_fail.c +++ b/test/theta/verif/base/loops3_fail.c @@ -1,4 +1,5 @@ -// RUN: %theta -no-optimize -memory=havoc "%s" | FileCheck "%s" +// RUN: %theta -no-optimize -memory=havoc -math-int "%s" | FileCheck "%s" +// RUN: %theta --domain EXPL --refinement UNSAT_CORE "%s" | FileCheck "%s" // CHECK: Verification FAILED #include diff --git a/test/theta/verif/base/main_no_assert.c b/test/theta/verif/base/main_no_assert.c index 30201f2d..88ebd64a 100644 --- a/test/theta/verif/base/main_no_assert.c +++ b/test/theta/verif/base/main_no_assert.c @@ -1,4 +1,5 @@ -// RUN: %theta -memory=havoc "%s" | FileCheck "%s" +// RUN: %theta -memory=havoc "%s" -math-int | FileCheck "%s" +// RUN: %theta --domain EXPL --refinement UNSAT_CORE "%s" | FileCheck "%s" // CHECK: Verification SUCCESSFUL diff --git a/test/theta/verif/base/separate_assert.c b/test/theta/verif/base/separate_assert.c index dce49a26..cc0eaa79 100644 --- a/test/theta/verif/base/separate_assert.c +++ b/test/theta/verif/base/separate_assert.c @@ -1,4 +1,5 @@ -// RUN: %theta -memory=havoc "%s" | FileCheck "%s" +// RUN: %theta -memory=havoc "%s" -math-int | FileCheck "%s" +// RUN: %theta --domain EXPL --refinement UNSAT_CORE "%s" | FileCheck "%s" // CHECK: Verification SUCCESSFUL diff --git a/test/theta/verif/base/simple_fail.c b/test/theta/verif/base/simple_fail.c index dba370e5..36338c76 100644 --- a/test/theta/verif/base/simple_fail.c +++ b/test/theta/verif/base/simple_fail.c @@ -1,4 +1,5 @@ -// RUN: %theta -memory=havoc "%s" | FileCheck "%s" +// RUN: %theta -memory=havoc "%s" -math-int | FileCheck "%s" +// RUN: %theta --domain EXPL --refinement UNSAT_CORE "%s" | FileCheck "%s" // CHECK: Verification FAILED #include diff --git a/test/theta/verif/base/uninitialized_var_false.c b/test/theta/verif/base/uninitialized_var_false.c index c7731dd1..cbdc7748 100644 --- a/test/theta/verif/base/uninitialized_var_false.c +++ b/test/theta/verif/base/uninitialized_var_false.c @@ -1,5 +1,6 @@ -// RUN: %theta -no-optimize -memory=havoc "%s" | FileCheck "%s" -// RUN: %theta -memory=havoc "%s" | FileCheck "%s" +// RUN: %theta -no-optimize -memory=havoc "%s" -math-int | FileCheck "%s" +// RUN: %theta -memory=havoc "%s" -math-int | FileCheck "%s" +// RUN: %theta --domain EXPL --refinement UNSAT_CORE "%s" | FileCheck "%s" // CHECK: Verification FAILED diff --git a/test/theta/verif/memory/arrays1.c b/test/theta/verif/memory/arrays1.c deleted file mode 100644 index dae726e5..00000000 --- a/test/theta/verif/memory/arrays1.c +++ /dev/null @@ -1,21 +0,0 @@ -// REQUIRES: memory.burstall -// RUN: %theta "%s" | FileCheck "%s" - -// CHECK: Verification SUCCESSFUL -int __VERIFIER_nondet_int(void); -void __VERIFIER_error(void) __attribute__((__noreturn__)); - -int main(void) -{ - int x[5]; - - for (int i = 0; i < 5; ++i) { - x[i] = i + 1; - } - - if (x[0] == 0) { - __VERIFIER_error(); - } - - return 0; -} \ No newline at end of file diff --git a/test/theta/verif/memory/arrays2_fail.c b/test/theta/verif/memory/arrays2_fail.c index 0cbb2c0f..dad980af 100644 --- a/test/theta/verif/memory/arrays2_fail.c +++ b/test/theta/verif/memory/arrays2_fail.c @@ -1,5 +1,5 @@ // REQUIRES: memory.burstall -// RUN: %theta "%s" | FileCheck "%s" +// RUN: %theta --domain PRED_CART --refinement NWT_IT_WP "%s" | FileCheck "%s" // CHECK: Verification FAILED int __VERIFIER_nondet_int(void); @@ -13,7 +13,7 @@ int main(void) x[i] = i; } - if (x[0] != 0) { + if (x[0] == 0) { __VERIFIER_error(); } diff --git a/test/theta/verif/memory/globals1.c b/test/theta/verif/memory/globals1.c index 6579935e..1dbdcb8f 100644 --- a/test/theta/verif/memory/globals1.c +++ b/test/theta/verif/memory/globals1.c @@ -1,4 +1,4 @@ -// RUN: %theta "%s" | FileCheck "%s" +// RUN: %theta --domain PRED_CART --refinement NWT_IT_WP -no-inline-globals "%s" | FileCheck "%s" // CHECK: Verification SUCCESSFUL int __VERIFIER_nondet_int(void); diff --git a/test/theta/verif/memory/globals2.c b/test/theta/verif/memory/globals2.c index 8eb281f2..58dc1a71 100644 --- a/test/theta/verif/memory/globals2.c +++ b/test/theta/verif/memory/globals2.c @@ -1,4 +1,4 @@ -// RUN: %theta "%s" | FileCheck "%s" +// RUN: %theta --domain PRED_CART --refinement NWT_IT_WP -no-inline-globals "%s" | FileCheck "%s" // CHECK: Verification SUCCESSFUL #include diff --git a/test/theta/verif/memory/globals3.c b/test/theta/verif/memory/globals3.c index 10e3242e..484271d8 100644 --- a/test/theta/verif/memory/globals3.c +++ b/test/theta/verif/memory/globals3.c @@ -1,4 +1,4 @@ -// RUN: %theta "%s" | FileCheck "%s" +// RUN: %theta --domain PRED_CART --refinement NWT_IT_WP -no-inline-globals "%s" | FileCheck "%s" // CHECK: Verification SUCCESSFUL #include diff --git a/test/theta/verif/memory/globals4.c b/test/theta/verif/memory/globals4.c deleted file mode 100644 index 5975a3c8..00000000 --- a/test/theta/verif/memory/globals4.c +++ /dev/null @@ -1,28 +0,0 @@ -// RUN: %theta "%s" | FileCheck "%s" - -// CHECK: Verification SUCCESSFUL - -int __VERIFIER_nondet_int(void); -void __VERIFIER_error(void) __attribute__((__noreturn__)); - -int a = 1; -int b = 1; -int c = 3; - -int main(void) -{ - int input = 1; - while (input != 0) { - input = __VERIFIER_nondet_int(); - if (input == 1) { - a = a + 1; - } - } - - if (a < b) { - __VERIFIER_error(); - } - - return 0; -} - diff --git a/test/theta/verif/memory/lit.local.cfg b/test/theta/verif/memory/lit.local.cfg deleted file mode 100644 index 61864550..00000000 --- a/test/theta/verif/memory/lit.local.cfg +++ /dev/null @@ -1,7 +0,0 @@ -# -*- Python -*- - -import lit -import pathlib - -# Disable these tests until we will have a theta-compatible memory model -config.unsupported = True diff --git a/test/theta/verif/memory/local_passbyref1_fail.c b/test/theta/verif/memory/local_passbyref1_fail.c index c7b8808d..f41b4d40 100644 --- a/test/theta/verif/memory/local_passbyref1_fail.c +++ b/test/theta/verif/memory/local_passbyref1_fail.c @@ -1,5 +1,5 @@ // REQUIRES: memory.burstall -// RUN: %theta "%s" | FileCheck "%s" +// RUN: %theta --domain PRED_CART --refinement NWT_IT_WP "%s" | FileCheck "%s" // CHECK: Verification FAILED void __VERIFIER_error(void) __attribute__((__noreturn__)); diff --git a/test/theta/verif/memory/passbyref1_false.c b/test/theta/verif/memory/passbyref1_false.c index 50213622..ec18cab9 100644 --- a/test/theta/verif/memory/passbyref1_false.c +++ b/test/theta/verif/memory/passbyref1_false.c @@ -1,5 +1,5 @@ // REQUIRES: memory.burstall -// RUN: %theta "%s" | FileCheck "%s" +// RUN: %theta --domain PRED_CART --refinement NWT_IT_WP "%s" | FileCheck "%s" // CHECK: Verification FAILED diff --git a/test/theta/verif/memory/passbyref2.c b/test/theta/verif/memory/passbyref2.c index a4a054e0..950a73ae 100644 --- a/test/theta/verif/memory/passbyref2.c +++ b/test/theta/verif/memory/passbyref2.c @@ -1,5 +1,5 @@ // REQUIRES: memory.burstall -// RUN: %theta "%s" | FileCheck "%s" +// RUN: %theta --domain PRED_CART --refinement NWT_IT_WP "%s" | FileCheck "%s" // CHECK: Verification SUCCESSFUL diff --git a/test/theta/verif/memory/passbyref3_fail.c b/test/theta/verif/memory/passbyref3_fail.c index 0c44ad05..a10af409 100644 --- a/test/theta/verif/memory/passbyref3_fail.c +++ b/test/theta/verif/memory/passbyref3_fail.c @@ -1,5 +1,5 @@ // REQUIRES: memory.burstall -// RUN: %theta "%s" | FileCheck "%s" +// RUN: %theta --domain PRED_CART --refinement NWT_IT_WP "%s" | FileCheck "%s" // CHECK: Verification FAILED diff --git a/test/theta/verif/memory/passbyref4.c b/test/theta/verif/memory/passbyref4.c index 1465eaf5..36d4b3c4 100644 --- a/test/theta/verif/memory/passbyref4.c +++ b/test/theta/verif/memory/passbyref4.c @@ -1,5 +1,5 @@ // REQUIRES: memory.burstall -// RUN: %theta "%s" | FileCheck "%s" +// RUN: %theta --domain PRED_CART --refinement NWT_IT_WP "%s" | FileCheck "%s" // CHECK: Verification SUCCESSFUL diff --git a/test/theta/verif/memory/passbyref5.c b/test/theta/verif/memory/passbyref5.c deleted file mode 100644 index 8ac40ced..00000000 --- a/test/theta/verif/memory/passbyref5.c +++ /dev/null @@ -1,28 +0,0 @@ -// REQUIRES: memory.burstall -// RUN: %theta "%s" | FileCheck "%s" - -// CHECK: Verification SUCCESSFUL - -int __VERIFIER_nondet_int(void); -void __VERIFIER_error(void) __attribute__((__noreturn__)); - -void sumprod(int* a, int* b, int *sum, int *prod) -{ - *sum = *a + *b; - *prod = *a * *b; -} - -int main(void) -{ - int a = __VERIFIER_nondet_int(); - int b = a + 1; - - int sum, prod; - sumprod(&a, &b, &sum, &prod); - - if (a != 0 && b != 0 && prod == 0) { - __VERIFIER_error(); - } - - return 0; -} diff --git a/test/theta/verif/memory/passbyref6.c b/test/theta/verif/memory/passbyref6.c deleted file mode 100644 index ef4d7024..00000000 --- a/test/theta/verif/memory/passbyref6.c +++ /dev/null @@ -1,31 +0,0 @@ -// REQUIRES: memory.burstall -// RUN: %theta "%s" | FileCheck "%s" - -// CHECK: Verification SUCCESSFUL - -int __VERIFIER_nondet_int(void); -void __VERIFIER_error(void) __attribute__((__noreturn__)); - -void sumprod(int* a, int* b, int *sum, int *prod) -{ - *sum = *a + *b; - *prod = *a * *b; -} - -int main(void) -{ - int a = __VERIFIER_nondet_int(); - int b = a + 1; - int c = __VERIFIER_nondet_int(); - - int* p = a == 0 ? &c : &a; - - int sum, prod; - sumprod(p, &b, &sum, &prod); - - if (a != 0 && b != 0 && prod == 0) { - __VERIFIER_error(); - } - - return 0; -} diff --git a/test/theta/verif/memory/passbyref7_fail.c b/test/theta/verif/memory/passbyref7_fail.c index f46abffe..ef0a6b0a 100644 --- a/test/theta/verif/memory/passbyref7_fail.c +++ b/test/theta/verif/memory/passbyref7_fail.c @@ -1,5 +1,5 @@ // REQUIRES: memory.burstall -// RUN: %theta "%s" | FileCheck "%s" +// RUN: %theta --domain PRED_CART --refinement NWT_IT_WP "%s" | FileCheck "%s" // CHECK: Verification FAILED @@ -20,7 +20,7 @@ int main(void) int prod; sumprod(a, b, &prod, &prod); - if (prod != 25) { + if (prod == 25) { __VERIFIER_error(); } diff --git a/test/theta/verif/memory/pointers1.c b/test/theta/verif/memory/pointers1.c index f562d97d..85acf8ca 100644 --- a/test/theta/verif/memory/pointers1.c +++ b/test/theta/verif/memory/pointers1.c @@ -1,4 +1,4 @@ -// RUN: %theta "%s" | FileCheck "%s" +// RUN: %theta --domain PRED_CART --refinement NWT_IT_WP "%s" | FileCheck "%s" // CHECK: Verification SUCCESSFUL diff --git a/test/theta/verif/memory/structs1.c b/test/theta/verif/memory/structs1.c index 9debb018..c1d119a2 100644 --- a/test/theta/verif/memory/structs1.c +++ b/test/theta/verif/memory/structs1.c @@ -1,5 +1,5 @@ // REQUIRES: memory.structs -// RUN: %theta "%s" | FileCheck "%s" +// RUN: %theta --domain PRED_CART --refinement NWT_IT_WP "%s" | FileCheck "%s" // CHECK: Verification FAILED diff --git a/test/theta/verif/overflow/overflow_loops.c b/test/theta/verif/overflow/overflow_loops.c new file mode 100644 index 00000000..6a810221 --- /dev/null +++ b/test/theta/verif/overflow/overflow_loops.c @@ -0,0 +1,23 @@ +// RUN: %theta -checks=signed-overflow "%s" | FileCheck "%s" + +// CHECK: Verification FAILED +// CHECK: Signed integer overflow + +int __VERIFIER_nondet_int(); + +int main(void) +{ + int x = 1; + int y = 1; + + while (1) { + x = x * 2 * __VERIFIER_nondet_int(); + y = y * 3 * __VERIFIER_nondet_int(); + if (x == 0) { + goto EXIT; + } + } + +EXIT: + return 0; +} diff --git a/test/theta/verif/overflow/overflow_simple.c b/test/theta/verif/overflow/overflow_simple.c new file mode 100644 index 00000000..caa45927 --- /dev/null +++ b/test/theta/verif/overflow/overflow_simple.c @@ -0,0 +1,14 @@ +// RUN: %theta -checks=signed-overflow "%s" | FileCheck "%s" + +// CHECK: Verification FAILED + +int __VERIFIER_nondet_int(); + +int main(void) +{ + int x = __VERIFIER_nondet_int(); + int y = __VERIFIER_nondet_int(); + + // CHECK: Signed integer overflow in {{.*}}overflow_simple.c at line [[# @LINE + 1]] column 14 + return x + y; +} diff --git a/test/theta/verif/svcomp/locks/test_locks_13_true.c b/test/theta/verif/svcomp/locks/test_locks_13_true.c index 429ecf2a..92fae859 100644 --- a/test/theta/verif/svcomp/locks/test_locks_13_true.c +++ b/test/theta/verif/svcomp/locks/test_locks_13_true.c @@ -1,4 +1,5 @@ -// RUN: %theta -memory=havoc "%s" | FileCheck "%s" +// RUN: %theta -memory=havoc -math-int "%s" | FileCheck "%s" +// RUN: %theta --domain EXPL --refinement UNSAT_CORE "%s" | FileCheck "%s" // CHECK: Verification SUCCESSFUL extern void __VERIFIER_error() __attribute__ ((__noreturn__)); diff --git a/test/theta/verif/svcomp/locks/test_locks_14_false.c b/test/theta/verif/svcomp/locks/test_locks_14_false.c index 85b90907..9517a036 100644 --- a/test/theta/verif/svcomp/locks/test_locks_14_false.c +++ b/test/theta/verif/svcomp/locks/test_locks_14_false.c @@ -1,4 +1,5 @@ -// RUN: %theta -memory=havoc "%s" | FileCheck "%s" +// RUN: %theta -memory=havoc -math-int "%s" | FileCheck "%s" +// RUN: %theta --domain EXPL --refinement UNSAT_CORE "%s" | FileCheck "%s" // CHECK: Verification FAILED extern void __VERIFIER_error() __attribute__ ((__noreturn__)); diff --git a/test/theta/verif/svcomp/locks/test_locks_14_true.c b/test/theta/verif/svcomp/locks/test_locks_14_true.c index daebc4c0..5884fde9 100644 --- a/test/theta/verif/svcomp/locks/test_locks_14_true.c +++ b/test/theta/verif/svcomp/locks/test_locks_14_true.c @@ -1,4 +1,5 @@ -// RUN: %theta -memory=havoc "%s" | FileCheck "%s" +// RUN: %theta -memory=havoc -math-int "%s" | FileCheck "%s" +// RUN: %theta --domain EXPL --refinement UNSAT_CORE "%s" | FileCheck "%s" // CHECK: Verification SUCCESSFUL extern void __VERIFIER_error() __attribute__ ((__noreturn__)); diff --git a/test/theta/verif/svcomp/locks/test_locks_15_false.c b/test/theta/verif/svcomp/locks/test_locks_15_false.c index b7b83108..e8d61a9c 100644 --- a/test/theta/verif/svcomp/locks/test_locks_15_false.c +++ b/test/theta/verif/svcomp/locks/test_locks_15_false.c @@ -1,4 +1,5 @@ -// RUN: %theta -memory=havoc "%s" | FileCheck "%s" +// RUN: %theta -memory=havoc -math-int "%s" | FileCheck "%s" +// RUN: %theta --domain EXPL --refinement UNSAT_CORE "%s" | FileCheck "%s" // CHECK: Verification FAILED extern void __VERIFIER_error() __attribute__ ((__noreturn__)); diff --git a/test/theta/verif/svcomp/locks/test_locks_15_true.c b/test/theta/verif/svcomp/locks/test_locks_15_true.c index 4e2fc85b..aec8ffe1 100644 --- a/test/theta/verif/svcomp/locks/test_locks_15_true.c +++ b/test/theta/verif/svcomp/locks/test_locks_15_true.c @@ -1,4 +1,5 @@ -// RUN: %theta -memory=havoc "%s" | FileCheck "%s" +// RUN: %theta -memory=havoc -math-int "%s" | FileCheck "%s" +// RUN: %theta --domain EXPL --refinement UNSAT_CORE "%s" | FileCheck "%s" // CHECK: Verification SUCCESSFUL extern void __VERIFIER_error() __attribute__ ((__noreturn__)); diff --git a/test/verif/overflow/overflow_loops.c b/test/verif/overflow/overflow_loops.c new file mode 100644 index 00000000..41373a87 --- /dev/null +++ b/test/verif/overflow/overflow_loops.c @@ -0,0 +1,23 @@ +// RUN: %bmc -bound 1 -checks=signed-overflow "%s" | FileCheck "%s" + +// CHECK: Verification FAILED +// CHECK: Signed integer overflow + +int __VERIFIER_nondet_int(); + +int main(void) +{ + int x = 1; + int y = 1; + + while (1) { + x = x * 2 * __VERIFIER_nondet_int(); + y = y * 3 * __VERIFIER_nondet_int(); + if (x == 0) { + goto EXIT; + } + } + +EXIT: + return 0; +} diff --git a/test/verif/overflow/overflow_simple.c b/test/verif/overflow/overflow_simple.c new file mode 100644 index 00000000..1e648d72 --- /dev/null +++ b/test/verif/overflow/overflow_simple.c @@ -0,0 +1,15 @@ +// RUN: %bmc -bound 1 -checks=signed-overflow "%s" | FileCheck "%s" +// RUN: %bmc -bound 1 -checks=signed-overflow -math-int "%s" | FileCheck "%s" + +// CHECK: Verification FAILED + +int __VERIFIER_nondet_int(); + +int main(void) +{ + int x = __VERIFIER_nondet_int(); + int y = __VERIFIER_nondet_int(); + + // CHECK: Signed integer overflow in {{.*}}overflow_simple.c at line [[# @LINE + 1]] column 14 + return x + y; +} diff --git a/test/verif/regression/crash_on_long.c b/test/verif/regression/crash_on_long.c new file mode 100644 index 00000000..8e9029a0 --- /dev/null +++ b/test/verif/regression/crash_on_long.c @@ -0,0 +1,12 @@ +// RUN: %bmc -checks=signed-overflow "%s" | FileCheck "%s" + +// CHECK: Verification SUCCESSFUL + +void a() __attribute__((__noreturn__)); +int b() { + int c; + if (c - 4L) + ; + a(); +} +int main() { b(); } diff --git a/test/verif/svcomp/locks/test_locks_14_false.c b/test/verif/svcomp/locks/test_locks_14_false.c index 78bb82b4..2d89b2be 100644 --- a/test/verif/svcomp/locks/test_locks_14_false.c +++ b/test/verif/svcomp/locks/test_locks_14_false.c @@ -2,6 +2,8 @@ // RUN: %bmc -bound 10 -math-int "%s" | FileCheck "%s" // CHECK: Verification FAILED +// CHECK: Assertion failure in {{.*}}test_locks_14_false.c at line 223 column 10 + extern void __VERIFIER_error() __attribute__ ((__noreturn__)); extern int __VERIFIER_nondet_int(); diff --git a/tools/gazer-theta/CMakeLists.txt b/tools/gazer-theta/CMakeLists.txt index c88d2b04..13916695 100644 --- a/tools/gazer-theta/CMakeLists.txt +++ b/tools/gazer-theta/CMakeLists.txt @@ -1,5 +1,5 @@ set(LIB_SOURCE_FILES - lib/ThetaCfaGenerator.cpp + lib/ThetaCfaGenerator.cpp lib/ThetaExpr.cpp lib/ThetaVerifier.cpp lib/ThetaCfaWriterPass.cpp) diff --git a/tools/gazer-theta/gazer-theta.cpp b/tools/gazer-theta/gazer-theta.cpp index 0bcdfd26..7dffd3ba 100644 --- a/tools/gazer-theta/gazer-theta.cpp +++ b/tools/gazer-theta/gazer-theta.cpp @@ -120,7 +120,8 @@ int main(int argc, char* argv[]) } // Force -math-int - config.getSettings().ints = IntRepresentation::Integers; + // TODO: Find a way to make this behavior default + // config.getSettings().ints = IntRepresentation::Integers; // Create the frontend object auto frontend = config.buildFrontend(InputFilenames); diff --git a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp index 13a7ff07..0344ba45 100644 --- a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp +++ b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp @@ -16,18 +16,22 @@ // //===----------------------------------------------------------------------===// #include "ThetaCfaGenerator.h" -#include "gazer/Core/LiteralExpr.h" + +#include "ThetaType.h" + #include "gazer/Automaton/CfaTransforms.h" +#include "gazer/Core/LiteralExpr.h" -#include #include +#include +#include #include #include #include +#include #include -#include using namespace gazer; using namespace gazer::theta; @@ -43,7 +47,14 @@ constexpr std::array ThetaKeywords = { "return", "havoc", "bool", "int", "rat", "if", "then", "else", "iff", "imply", "forall", "exists", "or", "and", "not", - "mod", "rem", "true", "false" + "mod", "rem", "true", "false", + "bvadd", "bvsub", "bvpos", "bvneg", + "bvmul", "bvudiv", "bvsdiv", + "bvsmod", "bvurem", "bvsrem", + "bvshl", "bvashr", "bvlshr", "bvrol", "bvror", + "bvult", "bvule", "bvugt", "bvuge", + "bvslt", "bvsle", "bvsgt", "bvsge", + "bv_zero_extend", "bv_sign_extend" }; struct ThetaAst @@ -191,24 +202,6 @@ void ThetaEdgeDecl::print(llvm::raw_ostream& os) const os << "}\n"; } -static std::string typeName(Type& type) -{ - switch (type.getTypeID()) { - case Type::IntTypeID: - return "int"; - case Type::RealTypeID: - return "rat"; - case Type::BoolTypeID: - return "bool"; - case Type::ArrayTypeID: { - auto& arrTy = llvm::cast(type); - return "[" + typeName(arrTy.getIndexType()) + "] -> " + typeName(arrTy.getElementType()); - } - default: - llvm_unreachable("Types which are unsupported by theta should have been eliminated earlier!"); - } -} - void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace) { Cfa* main = mSystem.getMainAutomaton(); @@ -222,6 +215,7 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace llvm::DenseMap> locs; llvm::DenseMap> vars; std::vector> edges; + std::unordered_set uninitializedMemoryArrays; // Create a closure to test variable names auto isValidVarName = [&vars](const std::string& name) -> bool { @@ -234,7 +228,7 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace // Add variables for (auto& variable : main->locals()) { auto name = validName(variable.getName(), isValidVarName); - auto type = typeName(variable.getType()); + auto type = thetaType(variable.getType()); nameTrace.variables[name] = &variable; vars.try_emplace(&variable, std::make_unique(name, type)); @@ -242,7 +236,7 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace for (auto& variable : main->inputs()) { auto name = validName(variable.getName(), isValidVarName); - auto type = typeName(variable.getType()); + auto type = thetaType(variable.getType()); nameTrace.variables[name] = &variable; vars.try_emplace(&variable, std::make_unique(name, type)); @@ -274,6 +268,15 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace if (edge->getGuard() != BoolLiteralExpr::True(edge->getGuard()->getContext())) { stmts.push_back(ThetaStmt::Assume(edge->getGuard())); + + // Collect use of uninitialized memory + auto arrayLiterals = gazer::theta::collectArrayLiteralsThetaExpr(edge->getGuard()); + for (const auto& arrayLiteral : arrayLiterals) { + if (!arrayLiteral->hasDefault()) { + assert(arrayLiteral->getMap().empty()); + uninitializedMemoryArrays.insert(&ArrayType::Get(arrayLiteral->getType().getIndexType(), arrayLiteral->getType().getElementType())); + } + } } if (auto assignEdge = dyn_cast(edge)) { @@ -284,6 +287,15 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace stmts.push_back(ThetaStmt::Havoc(lhsName)); } else { stmts.push_back(ThetaStmt::Assign(lhsName, assignment.getValue())); + + // Collect use of uninitialized memory + auto arrayLiterals = gazer::theta::collectArrayLiteralsThetaExpr(assignment.getValue()); + for (const auto& arrayLiteral : arrayLiterals) { + if (!arrayLiteral->hasDefault()) { + assert(arrayLiteral->getMap().empty()); + uninitializedMemoryArrays.insert(&ArrayType::Get(arrayLiteral->getType().getIndexType(), arrayLiteral->getType().getElementType())); + } + } } } } else if (auto callEdge = dyn_cast(edge)) { @@ -293,6 +305,17 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace edges.emplace_back(std::make_unique(source, target, std::move(stmts))); } + // Add variables modeling uninitialized memory + for (const auto& memoryArrayType : uninitializedMemoryArrays) { + auto name = validName("__gazer_uninitialized_memory_" + gazer::theta::thetaEscapedType(*memoryArrayType), isValidVarName); + auto type = thetaType(*memoryArrayType); + + auto *variable = main->createLocal(name, *memoryArrayType); + + nameTrace.variables[name] = variable; + vars.try_emplace(variable, std::make_unique(name, type)); + } + auto INDENT = " "; auto INDENT2 = " "; @@ -334,11 +357,13 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace void operator()(const ExprPtr& expr) { mOS << "assume "; mOS << theta::printThetaExpr(expr, mCanonizeName); + assert(theta::collectArrayLiteralsThetaExpr(expr).size() >= 0); } void operator()(const std::pair& assign) { mOS << assign.first << " := "; mOS << theta::printThetaExpr(assign.second, mCanonizeName); + assert(theta::collectArrayLiteralsThetaExpr(assign.second).size() >= 0); } void operator()(const std::string& variable) { diff --git a/tools/gazer-theta/lib/ThetaCfaGenerator.h b/tools/gazer-theta/lib/ThetaCfaGenerator.h index 942d93d3..7663809c 100644 --- a/tools/gazer-theta/lib/ThetaCfaGenerator.h +++ b/tools/gazer-theta/lib/ThetaCfaGenerator.h @@ -18,11 +18,13 @@ #ifndef GAZER_TOOLS_GAZERTHETA_THETACFAGENERATOR_H #define GAZER_TOOLS_GAZERTHETA_THETACFAGENERATOR_H -#include "gazer/Automaton/Cfa.h" #include "gazer/Automaton/CallGraph.h" +#include "gazer/Automaton/Cfa.h" #include +#include + namespace llvm { class Pass; @@ -35,6 +37,8 @@ std::string printThetaExpr(const ExprPtr& expr); std::string printThetaExpr(const ExprPtr& expr, std::function variableNames); +llvm::SmallVector, 1> collectArrayLiteralsThetaExpr(const ExprPtr& expr); + /// \brief Perform pre-processing steps required by theta on the input CFA. /// /// This pass does the following transformations: diff --git a/tools/gazer-theta/lib/ThetaExpr.cpp b/tools/gazer-theta/lib/ThetaExpr.cpp index d12b4bcf..f0e93e6b 100644 --- a/tools/gazer-theta/lib/ThetaExpr.cpp +++ b/tools/gazer-theta/lib/ThetaExpr.cpp @@ -16,9 +16,11 @@ // //===----------------------------------------------------------------------===// #include "ThetaCfaGenerator.h" +#include "ThetaType.h" #include "gazer/Core/Expr/ExprWalker.h" #include "gazer/ADT/StringUtils.h" +#include #include #include @@ -26,6 +28,7 @@ #include using namespace gazer; +using namespace gazer::theta; class ThetaExprPrinter : public ExprWalker { @@ -49,20 +52,61 @@ class ThetaExprPrinter : public ExprWalker std::string visitLiteral(const ExprRef& expr) { - if (auto intLit = llvm::dyn_cast(expr)) { + if (auto *intLit = llvm::dyn_cast(expr)) { auto val = intLit->getValue(); return val < 0 ? "(" + std::to_string(val) + ")" : std::to_string(intLit->getValue()); } - if (auto boolLit = llvm::dyn_cast(expr)) { + if (auto *boolLit = llvm::dyn_cast(expr)) { return boolLit->getValue() ? "true" : "false"; } - if (auto realLit = llvm::dyn_cast(expr)) { + if (auto *realLit = llvm::dyn_cast(expr)) { auto val = realLit->getValue(); return std::to_string(val.numerator()) + "%" + std::to_string(val.denominator()); } + if (auto *bvLit = llvm::dyn_cast(expr)) { + llvm::SmallString<64> exactString; + llvm::SmallString<64> paddedString; + + bvLit->getValue().toStringUnsigned(exactString, 2); // The bitvector may be signed, but only the bits are relevant + + auto paddingLength = std::max((bvLit->getType().getWidth() - exactString.size()), 0ul); + paddedString.append(paddingLength, '0'); // Leading zeros + paddedString.append(exactString); // Append literal + + return std::to_string(bvLit->getType().getWidth()) + "'b" + std::string(paddedString.data(), paddedString.data() + paddedString.size()); + } + + if (auto *arrLit = llvm::dyn_cast(expr)) { + std::string arrLitStr; + + if (arrLit->hasDefault()) { + arrLitStr += "["; + + const auto& kvPairs = arrLit->getMap(); + if (!kvPairs.empty()) { + for (const auto& [index, elem] : kvPairs) { + arrLitStr += printThetaExpr(index, mReplacedNames) + " <- " + printThetaExpr(elem, mReplacedNames) + ", "; + } + arrLitStr += "default <- "; + } else { + arrLitStr += "<" + thetaType(arrLit->getType().getIndexType()) + ">default <- "; + } + + arrLitStr += printThetaExpr(arrLit->getDefault(), mReplacedNames); + + arrLitStr += "]"; + } else { + assert(arrLit->getMap().empty()); + arrLitStr += + "__gazer_uninitialized_memory_" + gazer::theta::thetaEscapedType(arrLit->getType()); + } + + return arrLitStr; + } + return visitExpr(expr); } @@ -75,29 +119,61 @@ class ThetaExprPrinter : public ExprWalker return expr->getVariable().getName(); } - std::string visitNot(const ExprRef& expr) { + std::string visitNot([[maybe_unused]] const ExprRef& expr) { return "(not " + getOperand(0) + ")"; } // Binary std::string visitAdd(const ExprRef& expr) { - return "(" + getOperand(0) + " + " + getOperand(1) + ")"; + if (expr->getType().isBvType()) { + return "(" + getOperand(0) + " bvadd " + getOperand(1) + ")"; + } else { + return "(" + getOperand(0) + " + " + getOperand(1) + ")"; + } } std::string visitSub(const ExprRef& expr) { - return "(" + getOperand(0) + " - " + getOperand(1) + ")"; + if (expr->getType().isBvType()) { + return "(" + getOperand(0) + " bvsub " + getOperand(1) + ")"; + } else { + return "(" + getOperand(0) + " - " + getOperand(1) + ")"; + } } std::string visitMul(const ExprRef& expr) { - return "(" + getOperand(0) + " * " + getOperand(1) + ")"; + if (expr->getType().isBvType()) { + return "(" + getOperand(0) + " bvmul " + getOperand(1) + ")"; + } else { + return "(" + getOperand(0) + " * " + getOperand(1) + ")"; + } } - std::string visitDiv(const ExprRef& expr) { + std::string visitDiv([[maybe_unused]] const ExprRef& expr) { return "(" + getOperand(0) + " / " + getOperand(1) + ")"; } + std::string visitBvUDiv([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvudiv " + getOperand(1) + ")"; + } + + std::string visitBvSDiv([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvsdiv " + getOperand(1) + ")"; + } + std::string visitMod(const ExprRef& expr) { - return "(" + getOperand(0) + " mod " + getOperand(1) + ")"; + if (expr->getType().isBvType()) { + return "(" + getOperand(0) + " bvsmod " + getOperand(1) + ")"; + } else { + return "(" + getOperand(0) + " mod " + getOperand(1) + ")"; + } + } + + std::string visitBvURem([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvurem " + getOperand(1) + ")"; + } + + std::string visitBvSRem([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvsrem " + getOperand(1) + ")"; } std::string visitAnd(const ExprRef& expr) @@ -133,43 +209,119 @@ class ThetaExprPrinter : public ExprWalker return rso.str(); } - std::string visitImply(const ExprRef& expr) { + std::string visitImply([[maybe_unused]] const ExprRef& expr) { return "(" + getOperand(0) + " imply " + getOperand(1) + ")"; } - std::string visitEq(const ExprRef& expr) { + std::string visitBvAnd([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvand " + getOperand(1) + ")"; + } + + std::string visitBvOr([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvor " + getOperand(1) + ")"; + } + + std::string visitBvXor([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvxor " + getOperand(1) + ")"; + } + + std::string visitShl([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvshl " + getOperand(1) + ")"; + } + + std::string visitAShr([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvashr " + getOperand(1) + ")"; + } + + std::string visitBvConcat([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " ++ " + getOperand(1) + ")"; + } + + std::string visitExtract(const ExprRef& expr) { + auto from = expr->getOffset(); + auto until = expr->getOffset() + expr->getWidth(); + return "(" + getOperand(0) + ")[" + std::to_string(until) + ":" + std::to_string(from) + "]"; + } + + std::string visitZExt(const ExprRef& expr) { + auto width = expr->getExtendedWidth(); + return "(" + getOperand(0) + " bv_zero_extend bv[" + std::to_string(width) + "])"; + } + + std::string visitSExt(const ExprRef& expr) { + auto width = expr->getExtendedWidth(); + return "(" + getOperand(0) + " bv_sign_extend bv[" + std::to_string(width) + "])"; + } + + std::string visitLShr([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvlshr " + getOperand(1) + ")"; + } + + std::string visitEq([[maybe_unused]] const ExprRef& expr) { return "(" + getOperand(0) + " = " + getOperand(1) + ")"; } - std::string visitNotEq(const ExprRef& expr) { + std::string visitNotEq([[maybe_unused]] const ExprRef& expr) { return "(" + getOperand(0) + " /= " + getOperand(1) + ")"; } - std::string visitLt(const ExprRef& expr) { + std::string visitLt([[maybe_unused]] const ExprRef& expr) { return "(" + getOperand(0) + " < " + getOperand(1) + ")"; } - std::string visitLtEq(const ExprRef& expr) { + std::string visitLtEq([[maybe_unused]] const ExprRef& expr) { return "(" + getOperand(0) + " <= " + getOperand(1) + ")"; } - std::string visitGt(const ExprRef& expr) { + std::string visitGt([[maybe_unused]] const ExprRef& expr) { return "(" + getOperand(0) + " > " + getOperand(1) + ")"; } - std::string visitGtEq(const ExprRef& expr) { + std::string visitGtEq([[maybe_unused]] const ExprRef& expr) { return "(" + getOperand(0) + " >= " + getOperand(1) + ")"; } - std::string visitSelect(const ExprRef& expr) { + std::string visitBvULt([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvult " + getOperand(1) + ")"; + } + + std::string visitBvULtEq([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvule " + getOperand(1) + ")"; + } + + std::string visitBvUGt([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvugt " + getOperand(1) + ")"; + } + + std::string visitBvUGtEq([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvuge " + getOperand(1) + ")"; + } + + std::string visitBvSLt([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvslt " + getOperand(1) + ")"; + } + + std::string visitBvSLtEq([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvsle " + getOperand(1) + ")"; + } + + std::string visitBvSGt([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvsgt " + getOperand(1) + ")"; + } + + std::string visitBvSGtEq([[maybe_unused]] const ExprRef& expr) { + return "(" + getOperand(0) + " bvsge " + getOperand(1) + ")"; + } + + std::string visitSelect([[maybe_unused]] const ExprRef& expr) { return "(if " + getOperand(0) + " then " + getOperand(1) + " else " + getOperand(2) + ")"; } - std::string visitArrayRead(const ExprRef& expr) { + std::string visitArrayRead([[maybe_unused]] const ExprRef& expr) { return "(" + getOperand(0) + ")[" + getOperand(1) + "]"; } - std::string visitArrayWrite(const ExprRef& expr) { + std::string visitArrayWrite([[maybe_unused]] const ExprRef& expr) { return "(" + getOperand(0) + ")[" + getOperand(1) + " <- " + getOperand(2) + "]"; } @@ -189,4 +341,36 @@ std::string gazer::theta::printThetaExpr(const ExprPtr& expr, std::function { +public: + llvm::SmallVector, 1> getArrayLiterals() const { + return mArrayLiterals; + } + +public: + void* visitExpr(const ExprPtr& expr) { + return nullptr; + } + + void* visitLiteral(const ExprRef& expr) + { + if (auto *arrLit = llvm::dyn_cast(expr)) { + mArrayLiterals.push_back(arrLit); + } + + return nullptr; + } + +private: + llvm::SmallVector, 1> mArrayLiterals; +}; + +llvm::SmallVector, 1> gazer::theta::collectArrayLiteralsThetaExpr(const ExprPtr& expr) +{ + ThetaExprArrayLiteralCollector collector; + collector.walk(expr); + return collector.getArrayLiterals(); +} diff --git a/tools/gazer-theta/lib/ThetaType.cpp b/tools/gazer-theta/lib/ThetaType.cpp new file mode 100644 index 00000000..75f8276c --- /dev/null +++ b/tools/gazer-theta/lib/ThetaType.cpp @@ -0,0 +1,66 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2019 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// + +#include "ThetaType.h" + +using namespace gazer; +using namespace gazer::theta; + +std::string gazer::theta::thetaType(Type &type) +{ + switch (type.getTypeID()) { + case Type::IntTypeID: + return "int"; + case Type::RealTypeID: + return "rat"; + case Type::BoolTypeID: + return "bool"; + case Type::ArrayTypeID: { + auto& arrTy = llvm::cast(type); + return "[" + thetaType(arrTy.getIndexType()) + "] -> " + thetaType(arrTy.getElementType()); + } + case Type::BvTypeID: { + auto& bvTy = llvm::cast(type); + return "bv[" + std::to_string(bvTy.getWidth()) + "]"; + } + default: + llvm_unreachable("Types which are unsupported by theta should have been eliminated earlier!"); + } +} + +std::string gazer::theta::defaultValueForType(Type &type) +{ + switch (type.getTypeID()) { + case Type::IntTypeID: + return "0"; + case Type::RealTypeID: + return "0%1"; + case Type::BoolTypeID: + return "false"; + case Type::ArrayTypeID: { + auto& arrTy = llvm::cast(type); + return "[<" + thetaType(arrTy.getIndexType()) + ">default <- " + defaultValueForType(arrTy.getElementType()) + "]"; + } + case Type::BvTypeID: { + auto& bvTy = llvm::cast(type); + return std::to_string(bvTy.getWidth()) + "'d0"; + } + default: + llvm_unreachable("Types which are unsupported by theta should have been eliminated earlier!"); + } +} diff --git a/tools/gazer-theta/lib/ThetaType.h b/tools/gazer-theta/lib/ThetaType.h new file mode 100644 index 00000000..f18da19b --- /dev/null +++ b/tools/gazer-theta/lib/ThetaType.h @@ -0,0 +1,96 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2019 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +#ifndef GAZER_TOOLS_GAZERTHETA_LIB_THETATYPE_H +#define GAZER_TOOLS_GAZERTHETA_LIB_THETATYPE_H + +#include "gazer/Core/Type.h" + +#include + +namespace gazer::theta +{ + +inline std::string thetaType(const Type &type) +{ + switch (type.getTypeID()) { + case Type::IntTypeID: + return "int"; + case Type::RealTypeID: + return "rat"; + case Type::BoolTypeID: + return "bool"; + case Type::ArrayTypeID: { + const auto& arrTy = llvm::cast(type); + return "[" + thetaType(arrTy.getIndexType()) + "] -> " + thetaType(arrTy.getElementType()); + } + case Type::BvTypeID: { + const auto& bvTy = llvm::cast(type); + return "bv[" + std::to_string(bvTy.getWidth()) + "]"; + } + default: + llvm_unreachable("Types which are unsupported by theta should have been eliminated earlier!"); + } +} + +inline std::string thetaEscapedType(const Type &type) +{ + switch (type.getTypeID()) { + case Type::IntTypeID: + return "int"; + case Type::RealTypeID: + return "rat"; + case Type::BoolTypeID: + return "bool"; + case Type::ArrayTypeID: { + const auto& arrTy = llvm::cast(type); + return "__" + thetaEscapedType(arrTy.getIndexType()) + "_" + thetaEscapedType(arrTy.getElementType()) + "__"; + } + case Type::BvTypeID: { + const auto& bvTy = llvm::cast(type); + return "bv_" + std::to_string(bvTy.getWidth()); + } + default: + llvm_unreachable("Types which are unsupported by theta should have been eliminated earlier!"); + } +} + +inline std::string defaultValueForType(const Type &type) +{ + switch (type.getTypeID()) { + case Type::IntTypeID: + return "0"; + case Type::RealTypeID: + return "0%1"; + case Type::BoolTypeID: + return "false"; + case Type::ArrayTypeID: { + const auto& arrTy = llvm::cast(type); + return "[<" + thetaType(arrTy.getIndexType()) + ">default <- " + defaultValueForType(arrTy.getElementType()) + "]"; + } + case Type::BvTypeID: { + const auto& bvTy = llvm::cast(type); + return std::to_string(bvTy.getWidth()) + "'d0"; + } + default: + llvm_unreachable("Types which are unsupported by theta should have been eliminated earlier!"); + } +} + +} // end namespace gazer::theta + +#endif // GAZER_TOOLS_GAZERTHETA_LIB_THETATYPE_H diff --git a/tools/gazer-theta/lib/ThetaVerifier.cpp b/tools/gazer-theta/lib/ThetaVerifier.cpp index 4424a8d0..63e31659 100644 --- a/tools/gazer-theta/lib/ThetaVerifier.cpp +++ b/tools/gazer-theta/lib/ThetaVerifier.cpp @@ -240,6 +240,117 @@ static void reportInvalidCex(llvm::StringRef message, llvm::StringRef cex, sexpr llvm::errs() << "Raw counterexample is: " << cex << "\n"; } +static auto parseLiteral(sexpr::Value* sexpr, Type& varTy) -> ExprRef; + +static auto parseBoolLiteral(sexpr::Value* sexpr, BoolType& varTy) -> ExprRef +{ + llvm::StringRef value = sexpr->asAtom(); + if (value.equals_lower("true")) { + return BoolLiteralExpr::True(varTy.getContext()); + } else if (value.equals_lower("false")) { + return BoolLiteralExpr::False(varTy.getContext()); + } else { + return nullptr; + } +} + +static auto parseIntLiteral(sexpr::Value* sexpr, IntType& varTy) -> ExprRef +{ + llvm::StringRef value = sexpr->asAtom(); + long long int intVal; + if (!value.getAsInteger(10, intVal)) { + return IntLiteralExpr::Get(varTy, intVal); + } + + return nullptr; +} + +static auto parseBvLiteral(sexpr::Value* sexpr, BvType& varTy) -> ExprRef +{ + llvm::StringRef value = sexpr->asAtom(); + llvm::APInt intVal; + + if (!value.getAsInteger(10, intVal)) { + // Check if we have decimal format + return BvLiteralExpr::Get(varTy, intVal.zextOrTrunc(varTy.getWidth())); + } + + if (const auto lit = value.split("'"); !std::get<1>(lit).empty()) { + // Check if we have Theta literal format + + llvm::StringRef bvSizeStr = std::get<0>(lit); + char bvLitForm = std::get<1>(lit)[0]; + llvm::StringRef bvLitValueStr = std::get<1>(lit).substr(1); + + unsigned bvSize; + + if (!bvSizeStr.getAsInteger(10, bvSize) && bvSize == varTy.getWidth()) { + // Check if we have valid bitvector size + + switch (std::tolower(bvLitForm)) { + // Check if we have valid bitvector literal type + + case 'b': + if (!bvLitValueStr.getAsInteger(2, intVal)) { + return BvLiteralExpr::Get(varTy, intVal.zextOrTrunc(varTy.getWidth())); + } + break; + case 'x': + if (!bvLitValueStr.getAsInteger(16, intVal)) { + return BvLiteralExpr::Get(varTy, intVal.zextOrTrunc(varTy.getWidth())); + } + break; + case 'd': + if (!bvLitValueStr.getAsInteger(10, intVal)) { + return BvLiteralExpr::Get(varTy, intVal.zextOrTrunc(varTy.getWidth())); + } + break; + } + } + } + + return nullptr; +} + +static auto parseArrayLiteral(sexpr::Value* sexpr, ArrayType& varTy) -> ExprRef +{ + auto arrLitImpl = sexpr->asList(); + // The string "array" at the beginning + arrLitImpl.erase(arrLitImpl.begin()); + + ArrayLiteralExpr::MappingT entries; + ExprRef def = nullptr; + + for (auto *arrEntryImpl : arrLitImpl) { + auto *keyImpl = arrEntryImpl->asList()[0]; + auto *valueImpl = arrEntryImpl->asList()[1]; + + if (keyImpl->isAtom() && keyImpl->asAtom() == "default") { + def = parseLiteral(valueImpl, varTy.getElementType()); + } else { + entries[parseLiteral(keyImpl, varTy.getIndexType())] = parseLiteral(valueImpl, varTy.getElementType()); + } + } + + return ArrayLiteralExpr::Get(varTy, entries, def); +} + +static auto parseLiteral(sexpr::Value* sexpr, Type& varTy) -> ExprRef +{ + switch (varTy.getTypeID()) { + case Type::BoolTypeID: + return parseBoolLiteral(sexpr, cast(varTy)); + case Type::IntTypeID: + return parseIntLiteral(sexpr, cast(varTy)); + case Type::BvTypeID: + return parseBvLiteral(sexpr, cast(varTy)); + case Type::ArrayTypeID: + return parseArrayLiteral(sexpr, cast(varTy)); + default: + return nullptr; + } +} + std::unique_ptr ThetaVerifierImpl::parseCex(llvm::StringRef cex, unsigned* errorCode) { // TODO: The whole parsing process is very fragile. We should introduce some proper error cheks. @@ -276,7 +387,6 @@ std::unique_ptr ThetaVerifierImpl::parseCex(llvm::StringRef cex, unsigned std::vector assigns; for (size_t j = 1; j < actionList.size(); ++j) { llvm::StringRef varName = actionList[j]->asList()[0]->asAtom(); - llvm::StringRef value = actionList[j]->asList()[1]->asAtom(); Variable* variable = mNameMapping.variables.lookup(varName); assert(variable != nullptr && "Each variable must be present in the theta name mapping!"); @@ -286,39 +396,9 @@ std::unique_ptr ThetaVerifierImpl::parseCex(llvm::StringRef cex, unsigned origVariable = variable; } - ExprPtr rhs; - Type& varTy = origVariable->getType(); - - switch (varTy.getTypeID()) { - case Type::IntTypeID: { - long long int intVal; - if (!value.getAsInteger(10, intVal)) { - rhs = IntLiteralExpr::Get(cast(varTy), intVal); - } - break; - } - case Type::BvTypeID: { - llvm::APInt intVal; - if (!value.getAsInteger(10, intVal)) { - auto& bvTy = cast(varTy); - rhs = BvLiteralExpr::Get(bvTy, intVal.zextOrTrunc(bvTy.getWidth())); - } - break; - } - case Type::BoolTypeID: { - if (value.equals_lower("true")) { - rhs = BoolLiteralExpr::True(varTy.getContext()); - } else if (value.equals_lower("false")) { - rhs = BoolLiteralExpr::False(varTy.getContext()); - } - break; - } - default: - break; - } - + auto rhs = parseLiteral(actionList[j]->asList()[1], origVariable->getType()); if (rhs == nullptr) { - reportInvalidCex("expected a valid integer or boolean value", cex, &*(actionList[j]->asList()[1])); + reportInvalidCex("expected a valid integer, bitvector, boolean or their array as value", cex, &*(actionList[j]->asList()[1])); return nullptr; } diff --git a/unittest/tools/gazer-theta/ThetaExprPrinterTest.cpp b/unittest/tools/gazer-theta/ThetaExprPrinterTest.cpp index f98234a5..0c178ecd 100644 --- a/unittest/tools/gazer-theta/ThetaExprPrinterTest.cpp +++ b/unittest/tools/gazer-theta/ThetaExprPrinterTest.cpp @@ -18,6 +18,7 @@ #include "../../../tools/gazer-theta/lib/ThetaCfaGenerator.h" #include "gazer/Core/Expr/ExprBuilder.h" +#include "gazer/Core/Type.h" #include @@ -59,7 +60,40 @@ ThetaExprPrinterTest::ThetaExprPrinterTest() b->Lt(b->IntLit(1), b->IntLit(2)), b->Gt(b->IntLit(2), b->IntLit(1)) }), "((1 = 1) and (1 < 2) and (2 > 1))" }, - { b->Select(b->Eq(b->IntLit(1), b->IntLit(2)), b->IntLit(3), b->IntLit(4)), "(if (1 = 2) then 3 else 4)" } + { b->Select(b->Eq(b->IntLit(1), b->IntLit(2)), b->IntLit(3), b->IntLit(4)), "(if (1 = 2) then 3 else 4)" }, + { b->Add(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvadd 8'b00000011)" }, + { b->Sub(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvsub 8'b00000011)" }, + { b->Mul(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvmul 8'b00000011)" }, + { b->BvUDiv(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvudiv 8'b00000011)" }, + { b->BvSDiv(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvsdiv 8'b00000011)" }, + { b->Mod(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvsmod 8'b00000011)" }, + { b->BvURem(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvurem 8'b00000011)" }, + { b->BvSRem(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvsrem 8'b00000011)" }, + { b->BvAnd(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvand 8'b00000011)" }, + { b->BvOr(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvor 8'b00000011)" }, + { b->BvXor(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvxor 8'b00000011)" }, + { b->Shl(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvshl 8'b00000011)" }, + { b->AShr(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvashr 8'b00000011)" }, + { b->LShr(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvlshr 8'b00000011)" }, + { b->BvConcat(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 ++ 8'b00000011)" }, + { b->Extract(b->BvLit(2, 8), 3, 3), "(8'b00000010)[6:3]" }, + { b->ZExt(b->BvLit(2, 8), BvType::Get(ctx, 16)), "(8'b00000010 bv_zero_extend bv[16])" }, + { b->SExt(b->BvLit(2, 8), BvType::Get(ctx, 16)), "(8'b00000010 bv_sign_extend bv[16])" }, + { b->BvULt(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvult 8'b00000011)" }, + { b->BvULtEq(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvule 8'b00000011)" }, + { b->BvUGt(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvugt 8'b00000011)" }, + { b->BvUGtEq(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvuge 8'b00000011)" }, + { b->BvSLt(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvslt 8'b00000011)" }, + { b->BvSLtEq(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvsle 8'b00000011)" }, + { b->BvSGt(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvsgt 8'b00000011)" }, + { b->BvSGtEq(b->BvLit(2, 8), b->BvLit(3, 8)), "(8'b00000010 bvsge 8'b00000011)" }, + { b->ArrayLit({ + { b->BvLit(2, 4), b->BvLit(3, 4) }, + { b->BvLit(1, 4), b->BvLit(0, 4) } + }, b->BvLit(0, 4)), "[4'b0010 <- 4'b0011, 4'b0001 <- 4'b0000, default <- 4'b0000]" + }, + { b->ArrayLit(ArrayType::Get(BvType::Get(ctx, 8), BvType::Get(ctx, 4)), {}, b->BvLit(0, 4)), "[default <- 4'b0000]" }, + { b->ArrayLit(ArrayType::Get(BvType::Get(ctx, 8), BvType::Get(ctx, 4)), {}), "__gazer_uninitialized_memory___bv_8_bv_4__" } }) {}