ftsrg · as3810t · Sep 7, 2020 · Sep 7, 2020 · Sep 7, 2020 · Sep 7, 2020
diff --git a/.github/ISSUE_TEMPLATE/bug_report.md 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 <args>`
+    - 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
@@ -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
@@ -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,14 +73,22 @@ 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")
 
 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
@@ -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
@@ -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
@@ -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
@@ -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
diff --git 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<ArrayLiteralExpr> ArrayLit(ArrayType& arrTy, const ArrayLiteralExpr::MappingT& entries, const ExprRef<LiteralExpr>& elze = nullptr) {
+        return ArrayLiteralExpr::Get(arrTy, entries, elze);
+    }
+
+    ExprRef<ArrayLiteralExpr> ArrayLit(const ArrayLiteralExpr::MappingT& entries, const ExprRef<LiteralExpr>& elze = nullptr) {
+        assert(!entries.empty());
+        const auto& [index, elem] = *entries.begin();
+        return this->ArrayLit(ArrayType::Get(index->getType(), elem->getType()), entries, elze);
+    }
+
     ExprRef<BoolLiteralExpr> BoolLit(bool value) { return value ? True() : False(); }
     ExprRef<BoolLiteralExpr> True()  { return BoolLiteralExpr::True(BoolType::Get(mContext)); }
     ExprRef<BoolLiteralExpr> False() { return BoolLiteralExpr::False(BoolType::Get(mContext)); }

diff --git 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<bool(llvm::Instruction&)> predicate
+    );
+
     CheckRegistry& getRegistry() const;
 
 private:

diff --git 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
@@ -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