Merge pull request #204 from Bo-Yuan-Huang/unroller

Unroll instruction sequence using templated SMT formula generator

CMakeLists.txt

@@ -11,7 +11,7 @@ endif()
 # PROJECT
 # name version language
 # ---------------------------------------------------------------------------- #
-project(ilang VERSION     1.1.2
+project(ilang VERSION     1.1.3
               LANGUAGES   CXX
 )
 

README.md

@@ -63,30 +63,31 @@ brew install bison flex z3
 | Ubuntu 16.04 (Xenial)     | gcc 7.5.0    | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.0  | Release |
 | Ubuntu 18.04 (Bionic)     | gcc 8.4.0    | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4  | Debug   |
 | Ubuntu 18.04 (Bionic)     | gcc 8.4.0    | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4  | Release |
+| Ubuntu 20.04 (Focal Fosa) | gcc 9.3.0    | 3.17.0 | 4.8.7 | 3.0.4 | 2.6.4  | Debug   |
 | Ubuntu 20.04 (Focal Fosa) | gcc 9.3.0    | 3.17.0 | 4.8.7 | 3.0.4 | 2.6.4  | Release |
 | OSX 10.15.4 (Catalina)    | Xcode 11.4.1 | 3.17.2 | 4.8.8 | 3.6.2 | 2.5.35 | Debug   |
 | OSX 10.15.4 (Catalina)    | Xcode 11.4.1 | 3.17.2 | 4.8.8 | 3.6.2 | 2.5.35 | Release |
 | Windows Server 2016       | VS 2017      | 3.17.2 | 4.8.8 | 3.3.2 | 2.6.4  | Release |
 
 ### Default Build
 
-To build ILAng with default configuration, create a build directory and execute:
+To build ILAng with default configuration, create a build directory and make:
 
 ```bash
 mkdir -p build && cd build
 cmake .. 
 make
 ```
 
-If you are using git older than `1.8.4`, init the submodule from root and disable config-time submodule update:
+If you are using git older than `1.8.4`, init the submodule from root and disable config-time submodule fetching:
 ```bash
 git submodule update --init --recursive
 mkdir -p build && cd build
 cmake .. -DILANG_FETCH_DEPS=OFF
 make
 ```
 
-After the build complete, run unit tests and install the library. 
+After the build complete, run unit tests (optional) and install the library. 
 
 ```bash
 make run_test
@@ -95,11 +96,12 @@ sudo make install
 
 ### Options
 
--   Use `-DILANG_FETCH_DEPS=OFF` to disable config-time updating submodules for in-source dependencies.
+-   Use `-DILANG_FETCH_DEPS=OFF` to disable config-time fetching submodules for in-source dependencies.
 -   Use `-DILANG_BUILD_TEST=OFF` to disalbe building the unit tests.
 -   Use `-DILANG_BUILD_SYNTH=ON` to enable building the synthesis engine. 
 -   Use `-DILANG_BUILD_INVSYN=OFF` to disable building invariant synthesis feature.
 -   Use `-DILANG_BUILD_SWITCH=ON` to enable building [smt-switch](https://github.com/makaimann/smt-switch.git) interface support. 
+-   Use `-DILANG_BUILD_COSIM=ON` to enable building [Xilinx cosimulation](https://www.linuxsecrets.com/xilinx/QEMU%20SystemC%20and%20TLM%20CoSimulation.html) support.
 -   Use `-DILANG_INSTALL_DEV=ON` to install working features. 
 
 ## CMake Integration

appveyor.yml

@@ -2,6 +2,10 @@ version: 1.0.{build}
 image: Ubuntu2004
 clone_depth: 1
 
+configuration:
+- Debug
+- Release
+
 install:
 - sudo apt update --yes
 - sudo apt install --yes z3 libz3-dev bison flex gcc g++
@@ -10,7 +14,7 @@ build_script:
 - cd $APPVEYOR_BUILD_FOLDER
 - mkdir -p build
 - cd build
-- cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_COMPILER=g++-9
+- cmake .. -DCMAKE_CXX_COMPILER=g++-9
 - make -j$(nproc)
 - sudo make install
 - make test

include/ilang/ila-mngr/u_unroller_smt.h

@@ -0,0 +1,190 @@
+/// \file
+/// Class UnrollerSmt, PathUnroller, and MonoUnroller - a collection of
+/// ILA unrollers with SmtShim support.
+
+#ifndef ILANG_ILA_MNGR_U_UNROLLER_SMT_H__
+#define ILANG_ILA_MNGR_U_UNROLLER_SMT_H__
+
+#include <map>
+#include <string>
+#include <vector>
+
+#include <ilang/ila/instr_lvl_abs.h>
+#include <ilang/target-smt/smt_shim.h>
+#include <ilang/util/log.h>
+
+/// \namespace ilang
+namespace ilang {
+
+/// \brief Base class for unrolling ILA execution in different settings.
+template <class Generator> class UnrollerSmt {
+public:
+  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
+  /// Constructor.
+  UnrollerSmt(SmtShim<Generator>& smt_shim, const std::string& suffix)
+      : smt_gen_(smt_shim), unroller_suffix_(suffix) {}
+
+  // ------------------------- METHODS -------------------------------------- //
+  //
+  // Control property/predicate beyond the transition.
+  //
+  /// Add the predicate p to be asserted globally.
+  inline void AssertGlobal(const ExprPtr& p) { global_pred_.insert(p); }
+  /// Add the predicate p to be asserted at the first step (initial condition).
+  inline void AssertInitial(const ExprPtr& p) { initial_pred_.insert(p); }
+  /// Add the predicate p to be asserted at the k-th step.
+  inline void AssertStep(const ExprPtr& p, const int& k) {
+    step_pred_[k].insert(p);
+  }
+  /// Clear all the global assertions.
+  inline void ClearGlobalAssertion() { global_pred_.clear(); }
+  /// Clear all the initial assertions.
+  inline void ClearInitialAssertion() { initial_pred_.clear(); }
+  /// Clear all the step-specific assertions.
+  inline void ClearStepAssertion() { step_pred_.clear(); }
+
+  //
+  // Access SMT formula in the unrolled execution.
+  //
+  /// Return the SMT formula of expr at the beginning k-th step.
+  inline auto GetSmtCurrent(const ExprPtr& expr, const size_t& k) const {
+    return smt_gen_.GetShimExpr(expr, SuffixCurrent(k));
+  }
+  /// Return the SMT formula of expr at the end of k-th step.
+  inline auto GetSmtNext(const ExprPtr& expr, const size_t& k) const {
+    return smt_gen_.GetShimExpr(expr, SuffixNext(k));
+  }
+  /// Return the SMT function declaration of uninterpreted function func.
+  inline auto GetSmtFuncDecl(const FuncPtr& func) const {
+    return smt_gen_.GetShimFunc(func);
+  }
+
+private:
+  // ------------------------- MEMBERS -------------------------------------- //
+  /// The underlying (templated) SMT generator.
+  SmtShim<Generator>& smt_gen_;
+  /// Unroller specific suffix.
+  const std::string unroller_suffix_;
+
+  /// Predicates to be asserted globally.
+  ExprSet global_pred_;
+  /// Predicates to be asserted initially.
+  ExprSet initial_pred_;
+  /// Predicates to be asserted at each step.
+  std::map<size_t, ExprSet> step_pred_;
+
+  // ------------------------- HELPERS -------------------------------------- //
+  /// Return suffix for current state.
+  inline std::string SuffixCurrent(const size_t& t) const {
+    return std::to_string(t) + "_" + unroller_suffix_;
+  }
+  /// Return suffix for next state.
+  inline std::string SuffixNext(const size_t& t) const {
+    return std::to_string(t) + "_" + unroller_suffix_ + ".nxt";
+  }
+
+protected:
+  // ------------------------- TYPES ---------------------------------------- //
+  typedef decltype(smt_gen_.GetShimExpr(nullptr, "")) SmtExpr;
+  typedef decltype(smt_gen_.GetShimFunc(nullptr)) SmtFunc;
+  typedef std::vector<ExprPtr> IlaExprVec;
+  typedef std::vector<SmtExpr> SmtExprVec;
+
+  // ------------------------- MEMBERS -------------------------------------- //
+  /// Variables on which the instruction sequence depends
+  IlaExprVec deciding_vars_;
+  /// State update functions of the deciding variables
+  IlaExprVec update_holder_;
+  /// Non-execution semantics (state update) properties
+  IlaExprVec assert_holder_;
+
+  // ------------------------- METHODS -------------------------------------- //
+  /// Setup the deciding variabels
+  virtual void SetDecidingVars() = 0;
+
+  /// Make one transition (step) and setup the update_holder_ and assert_holder_
+  /// accordingly
+  virtual void MakeOneTransition(const size_t& idx) = 0;
+
+  /// Unroll the whole sequence
+  SmtExpr Unroll_(const size_t& len, const size_t& begin);
+
+  /// Unroll the whole sequence without connecting the steps
+  SmtExpr UnrollWithStepsUnconnected_(const size_t& len, const size_t& begin);
+
+private:
+  // ------------------------- HELPERS -------------------------------------- //
+  inline void InterpIlaExprAndAppend(const IlaExprVec& ila_expr_src,
+                                     const std::string& suffix,
+                                     SmtExprVec& smt_expr_dst) {
+    for (const auto& e : ila_expr_src) {
+      smt_expr_dst.push_back(smt_gen_.GetShimExpr(e, suffix));
+    }
+  }
+
+  inline void InterpIlaExprAndAppend(const ExprSet& ila_expr_src,
+                                     const std::string& suffix,
+                                     SmtExprVec& smt_expr_dst) {
+    for (const auto& e : ila_expr_src) {
+      smt_expr_dst.push_back(smt_gen_.GetShimExpr(e, suffix));
+    }
+  }
+
+  inline void ElementWiseEqualAndAppend(const SmtExprVec& a,
+                                        const SmtExprVec& b,
+                                        SmtExprVec& smt_expr_dst) {
+    ILA_ASSERT(a.size() == b.size());
+    for (size_t i = 0; i < a.size(); i++) {
+      smt_expr_dst.push_back(smt_gen_.Equal(a.at(i), b.at(i)));
+    }
+  }
+
+  inline SmtExpr ConjunctAll(const SmtExprVec& vec) const {
+    auto conjunct_holder = smt_gen_.GetShimExpr(asthub::BoolConst(true));
+    for (const auto& e : vec) {
+      conjunct_holder = smt_gen_.BoolAnd(conjunct_holder, e);
+    }
+    return conjunct_holder;
+  }
+
+}; // class UnrollerSmt
+
+/// \brief Application class for unrolling a sequence of instructions.
+template <class Generator> class PathUnroller : public UnrollerSmt<Generator> {
+public:
+  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
+  /// Constructor.
+  PathUnroller(SmtShim<Generator>& smt_shim, const std::string& suffix = "")
+      : UnrollerSmt<Generator>(smt_shim, suffix) {}
+
+  // ------------------------- METHODS -------------------------------------- //
+  /// Unroll the sequence
+  auto Unroll(const InstrVec& seq, const size_t& begin = 0) {
+    seq_ = seq;
+    return this->Unroll_(seq.size(), begin);
+  }
+
+  /// Unroll the sequence without connecting the steps
+  auto UnrollWithStepsUnconnected(const InstrVec& seq, const size_t& begin) {
+    seq_ = seq;
+    return this->UnrollWithStepsUnconnected_(seq.size(), begin);
+  }
+
+protected:
+  // ------------------------- METHODS -------------------------------------- //
+  /// Setup the deciding variables
+  void SetDecidingVars();
+
+  /// Make one transition and setup holders accordingly
+  void MakeOneTransition(const size_t& idx);
+
+private:
+  // ------------------------- MEMBERS -------------------------------------- //
+  /// The sequence of instructions.
+  InstrVec seq_;
+
+}; // class PathUnroller
+
+} // namespace ilang
+
+#endif // ILANG_ILA_MNGR_U_UNROLLER_SMT_H__

include/ilang/ilang++.h

@@ -11,13 +11,12 @@
 #include <vector>
 
 #include <z3++.h>
-
-#include <ilang/config.h>
-
 #ifdef SMTSWITCH_INTERFACE
 #include <smt-switch/smt.h>
 #endif // SMTSWITCH_INTERFACE
 
+#include <ilang/config.h>
+
 /// \namespace ilang
 /// Defines the core data structure and APIs for constructing and storing ILA.
 namespace ilang {
@@ -57,6 +56,7 @@ class Expr;
 class Instr;
 class InstrLvlAbs;
 class Unroller;
+
 // forward declaration
 class Ila;
 

include/ilang/target-smt/smt_shim.h

@@ -20,6 +20,8 @@ template <class Generator> class SmtShim {
 private:
   /// Reference to the underlying SMT formula generator.
   Generator& gen_;
+  /// Type alias for expression.
+  typedef decltype(gen_.GetShimExpr(nullptr, "")) ShimExprType;
 
 public:
   /// Unified interface to get expression.
@@ -30,6 +32,16 @@ template <class Generator> class SmtShim {
   inline auto GetShimFunc(const FuncPtr& func) {
     return gen_.GetShimFunc(func);
   }
+  /// Unified interface to AND two boolean expressions.
+  inline auto BoolAnd(const ShimExprType& a, const ShimExprType& b) {
+    return gen_.BoolAnd(a, b);
+  }
+  /// Unified interface to Equal two expressions.
+  inline auto Equal(const ShimExprType& a, const ShimExprType& b) {
+    return gen_.Equal(a, b);
+  }
+  /// Return the underlying generator.
+  inline Generator& get() const { return gen_; }
 
 }; // class SmtShim
 

include/ilang/target-smt/smt_switch_itf.h

@@ -30,6 +30,8 @@ class SmtSwitchItf {
   smt::Term GetSmtTerm(const ExprPtr& expr, const std::string& suffix = "");
   /// Reset the solver and the interface.
   void Reset();
+  /// Return the underlying SMT solver;
+  inline smt::SmtSolver& solver() const { return solver_; }
 
   /// Check if Term is generated.
   bool pre(const ExprPtr& expr);
@@ -43,6 +45,14 @@ class SmtSwitchItf {
   }
   /// Unified SmtShim interface to get smt::Func.
   inline auto GetShimFunc(const FuncPtr& func) { return Func2Term(func); }
+  /// Unified SmtShim interface to AND two boolean smt::Term.
+  inline auto BoolAnd(const smt::Term& a, const smt::Term& b) {
+    return solver_->make_term(smt::PrimOp::And, a, b);
+  }
+  /// Unified SmtShim interface to EQUAL two smt::Term.
+  inline auto Equal(const smt::Term& a, const smt::Term& b) {
+    return solver_->make_term(smt::PrimOp::Equal, a, b);
+  }
 
 private:
   /// Type for cacheing the generated expressions.

include/ilang/target-smt/z3_expr_adapter.h

@@ -32,6 +32,9 @@ class Z3ExprAdapter {
   /// Function object for getting z3 expression.
   void operator()(const ExprPtr& expr);
 
+  /// Return the underlying z3 context.
+  inline z3::context& context() const { return ctx_; }
+
   // ------------------------- SHIM INTERFACE ------------------------------- //
   /// Unified SmtShim interface to get z3::expr.
   inline auto GetShimExpr(const ExprPtr& expr, const std::string& suffix) {
@@ -41,6 +44,10 @@ class Z3ExprAdapter {
   inline auto GetShimFunc(const FuncPtr& func) {
     return func->GetZ3FuncDecl(ctx_);
   }
+  /// Unified SmtShim interface to AND two boolean z3::expr.
+  inline auto BoolAnd(const z3::expr& a, const z3::expr& b) { return a && b; }
+  /// Unified SmtShim interface to EQUAL two z3::expr.
+  inline auto Equal(const z3::expr& a, const z3::expr& b) { return a == b; }
 
 private:
   /// Type for caching the generated expressions.

src/ila-mngr/CMakeLists.txt

@@ -14,6 +14,7 @@ target_sources(${ILANG_LIB_NAME} PRIVATE
   ${CMAKE_CURRENT_SOURCE_DIR}/u_rewrite_expr.cc
   ${CMAKE_CURRENT_SOURCE_DIR}/u_rewrite_ila.cc
   ${CMAKE_CURRENT_SOURCE_DIR}/u_unroller.cc
+  ${CMAKE_CURRENT_SOURCE_DIR}/u_unroller_smt.cc
   ${CMAKE_CURRENT_SOURCE_DIR}/v_eq_check_crr.cc
   ${CMAKE_CURRENT_SOURCE_DIR}/v_eq_check_bmc.cc
   ${CMAKE_CURRENT_SOURCE_DIR}/v_refinement.cc