Merge pull request #200 from Bo-Yuan-Huang/smt

Unified SMT interface

CMakeLists.txt

@@ -11,7 +11,7 @@ endif()
 # PROJECT
 # name version language
 # ---------------------------------------------------------------------------- #
-project(ilang VERSION     1.1.1
+project(ilang VERSION     1.1.2
               LANGUAGES   CXX
 )
 
@@ -29,6 +29,7 @@ option(ILANG_COVERITY    "Build for Coverity static analysis."              OFF)
 option(BUILD_SHARED_LIBS "Build shared libraries."                           ON)
 option(ILANG_BUILD_INVSYN "Build invariant synthesis feature."               ON)
 option(ILANG_BUILD_SWITCH "Build smt-switch interface."                     OFF)
+option(ILANG_BUILD_COSIM "Build QEMU-based co-simulation support."          OFF)
 
 include(CMakeDependentOption)
 

include/ilang/ila-mngr/pass.h

@@ -42,6 +42,11 @@ bool SimplifySemantic(const InstrLvlAbsCnstPtr& m, const int& timeout = -1);
 /// \param[in] m The top-level ILA.
 bool SimplifySyntactic(const InstrLvlAbsPtr& m);
 
+/// \brief Sanity check instruction completness and determinism and fix if
+/// possible.
+/// \param[in] m The top-level ILA.
+bool SanityCheckAndFix(const InstrLvlAbsPtr& m);
+
 } // namespace pass
 
 }; // namespace ilang

include/ilang/ila-mngr/u_abs_knob.h

@@ -13,9 +13,9 @@ namespace ilang {
 namespace AbsKnob {
 /****************************************************************************/
 /// Add all dependent vars of the expr to the set.
-void InsertVar(const ExprPtr e, ExprSet& vars);
+void InsertVar(const ExprPtr& e, ExprSet& vars);
 /// Get the set of all dependent vars of the expr.
-ExprSet GetVar(const ExprPtr e);
+ExprSet GetVar(const ExprPtr& e);
 
 /****************************************************************************/
 /// Add all state vars of the host (excluding child) to the set.
@@ -25,48 +25,48 @@ void InsertSttTree(const InstrCnstPtr instrs, ExprSet& stts);
 
 /****************************************************************************/
 /// Add all vars of the ILA (excluding child) to the set.
-void InsertVar(const InstrLvlAbsCnstPtr m, ExprSet& vars);
+void InsertVar(const InstrLvlAbsCnstPtr& m, ExprSet& vars);
 /// Add all state vars of the ILA (excluding child) to the set.
-void InsertStt(const InstrLvlAbsCnstPtr m, ExprSet& stts);
+void InsertStt(const InstrLvlAbsCnstPtr& m, ExprSet& stts);
 /// Add all input vars of the ILA (excluding child) to the set.
-void InsertInp(const InstrLvlAbsCnstPtr m, ExprSet& inps);
+void InsertInp(const InstrLvlAbsCnstPtr& m, ExprSet& inps);
 /// Add all vars of the ILA (including child) to the set.
-void InsertVarTree(const InstrLvlAbsCnstPtr top, ExprSet& vars);
+void InsertVarTree(const InstrLvlAbsCnstPtr& top, ExprSet& vars);
 /// Add all state vars of the ILA (including child) to the set.
-void InsertSttTree(const InstrLvlAbsCnstPtr top, ExprSet& stts);
+void InsertSttTree(const InstrLvlAbsCnstPtr& top, ExprSet& stts);
 /// Add all input vars of the ILA (including child) to the set.
-void InsertInpTree(const InstrLvlAbsCnstPtr top, ExprSet& inps);
+void InsertInpTree(const InstrLvlAbsCnstPtr& top, ExprSet& inps);
 
 /// Get the set of all vars of the ILA (excluding child).
-ExprSet GetVar(const InstrLvlAbsCnstPtr m);
+ExprSet GetVar(const InstrLvlAbsCnstPtr& m);
 /// Get the set of all state vars of the ILA (excluding child).
-ExprSet GetStt(const InstrLvlAbsCnstPtr m);
+ExprSet GetStt(const InstrLvlAbsCnstPtr& m);
 /// Get the set of all input vars of the ILA (excluding child).
-ExprSet GetInp(const InstrLvlAbsCnstPtr m);
+ExprSet GetInp(const InstrLvlAbsCnstPtr& m);
 /// Get the set of all vars of the ILA (including child).
-ExprSet GetVarTree(const InstrLvlAbsCnstPtr top);
+ExprSet GetVarTree(const InstrLvlAbsCnstPtr& top);
 /// Get the set of all state vars of the ILA (including child).
-ExprSet GetSttTree(const InstrLvlAbsCnstPtr top);
+ExprSet GetSttTree(const InstrLvlAbsCnstPtr& top);
 /// Get the set of all input vars of the ILA (including child).
-ExprSet GetInpTree(const InstrLvlAbsCnstPtr top);
+ExprSet GetInpTree(const InstrLvlAbsCnstPtr& top);
 
 /// Add all instructions of the ILA (excluding child) to the set.
-void InsertInstr(const InstrLvlAbsCnstPtr m, InstrVec& instrs);
+void InsertInstr(const InstrLvlAbsCnstPtr& m, InstrVec& instrs);
 /// Add all instructions of the ILA (including child) to the set.
-void InsertInstrTree(const InstrLvlAbsCnstPtr top, InstrVec& instrs);
+void InsertInstrTree(const InstrLvlAbsCnstPtr& top, InstrVec& instrs);
 
 /// Get the set of instructions of the ILA (excluding child).
-InstrVec GetInstr(const InstrLvlAbsCnstPtr m);
+InstrVec GetInstr(const InstrLvlAbsCnstPtr& m);
 /// Get the set of instructions of the ILA (including child).
-InstrVec GetInstrTree(const InstrLvlAbsCnstPtr top);
+InstrVec GetInstrTree(const InstrLvlAbsCnstPtr& top);
 
 /****************************************************************************/
 /// \brief Rewrite an expression by replacing based on the rule.
 /// - If leaves contain non-var nodes, will replace with no further traverse.
-ExprPtr Rewrite(const ExprPtr e, const ExprMap& rule);
+ExprPtr Rewrite(const ExprPtr& e, const ExprMap& rule);
 
 /// \brief Rewrite an instruction by replacing based on the rule.
-void RewriteInstr(const InstrCnstPtr instr_src, const InstrPtr instr_dst,
+void RewriteInstr(const InstrCnstPtr instr_src, const InstrPtr& instr_dst,
                   const ExprMap& expr_map);
 
 /// \brief Flatten the given ILA, the initial conditions will be added to the
@@ -76,37 +76,37 @@ void RewriteInstr(const InstrCnstPtr instr_src, const InstrPtr instr_dst,
 /// generator or other verification model generator. You can first use
 /// ExtrDeptModl to extract the dependent model and use this to flatten the
 /// that model and send to the generator
-void FlattenIla(const InstrLvlAbsPtr ila_ptr_);
+void FlattenIla(const InstrLvlAbsPtr& ila_ptr_);
 
 /// \brief Return a new ILA that contains the dependant instructions and
 /// child-ILAs of an instruction (defined by sub-programs).
-InstrLvlAbsPtr ExtrDeptModl(const InstrPtr instr, const std::string& name);
+InstrLvlAbsPtr ExtrDeptModl(const InstrPtr& instr, const std::string& name);
 
 /// Copy and ILA (including child).
-InstrLvlAbsPtr CopyIlaTree(const InstrLvlAbsCnstPtr src,
+InstrLvlAbsPtr CopyIlaTree(const InstrLvlAbsCnstPtr& src,
                            const std::string& dst_name);
 
 /****************************************************************************/
 /// Duplicate input vars from src to dst while updating the mapping.
-void DuplInp(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst,
+void DuplInp(const InstrLvlAbsCnstPtr& src, const InstrLvlAbsPtr& dst,
              ExprMap& expr_map);
 /// Duplicate state vars from src to dst while updating the mapping.
-void DuplStt(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst,
+void DuplStt(const InstrLvlAbsCnstPtr& src, const InstrLvlAbsPtr& dst,
              ExprMap& expr_map);
 /// Duplicate fetch from src to dst if defined (rewritten w.r.t. mapping).
-ExprPtr DuplFetch(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst,
+ExprPtr DuplFetch(const InstrLvlAbsCnstPtr& src, const InstrLvlAbsPtr& dst,
                   const ExprMap& expr_map);
 /// Duplicate valid from src to dst if defined (rewritten w.r.t. mapping).
-ExprPtr DuplValid(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst,
+ExprPtr DuplValid(const InstrLvlAbsCnstPtr& src, const InstrLvlAbsPtr& dst,
                   const ExprMap& expr_map);
 /// Duplicate initial conditions from src to dst (rewritten w.r.t. mapping).
-void DuplInit(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst,
+void DuplInit(const InstrLvlAbsCnstPtr& src, const InstrLvlAbsPtr& dst,
               const ExprMap& expr_map);
 /// Duplicate an instruction to dst (rewritten w.r.t. mapping).
-InstrPtr DuplInstr(const InstrCnstPtr instr_src, const InstrLvlAbsPtr dst,
+InstrPtr DuplInstr(const InstrCnstPtr instr_src, const InstrLvlAbsPtr& dst,
                    const ExprMap& expr_map, const CnstIlaMap& ila_map);
 /// Duplicate instruction sequence to dst. NOT IMPLEMENTED YET.
-void DuplInstrSeq(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst);
+void DuplInstrSeq(const InstrLvlAbsCnstPtr& src, const InstrLvlAbsPtr& dst);
 
 }; // namespace AbsKnob
 

include/ilang/ila-mngr/u_unroller.h

@@ -4,26 +4,28 @@
 #ifndef ILANG_ILA_MNGR_U_UNROLLER_H__
 #define ILANG_ILA_MNGR_U_UNROLLER_H__
 
-#include <set>
+#include <map>
 #include <vector>
 
-#include "z3++.h"
+#include <z3++.h>
+
 #include <ilang/ila/instr_lvl_abs.h>
-#include <ilang/ila/z3_expr_adapter.h>
+#include <ilang/target-smt/z3_expr_adapter.h>
 
 /// \namespace ilang
 namespace ilang {
 
 /// \brief Base class for unrolling ILA execution in different settings.
 class Unroller {
-public:
+protected:
   /// Type alias for z3::expr.
   typedef z3::expr ZExpr;
   /// Type for containing a set of z3::expr.
   typedef z3::expr_vector ZExprVec;
   /// Type alias for a set of ExprPtr.
   typedef ExprPtrVec IExprVec;
 
+public:
   // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
   /// Default constructor
   Unroller(z3::context& ctx, const std::string& suffix);
@@ -32,11 +34,11 @@ class Unroller {
 
   // ------------------------- METHODS -------------------------------------- //
   /// Add a predicate that should be asserted globally.
-  void AddGlobPred(const ExprPtr p);
+  void AddGlobPred(const ExprPtr& p);
   /// Add a predicate that should be asserted in the initial condition.
-  void AddInitPred(const ExprPtr p);
+  void AddInitPred(const ExprPtr& p);
   /// Add a predicate that should be asserted at the k-th step.
-  void AddStepPred(const ExprPtr p, const int& k);
+  void AddStepPred(const ExprPtr& p, const int& k);
   /// Clear the global predicates.
   void ClearGlobPred();
   /// Clear the initial predicates.
@@ -48,15 +50,16 @@ class Unroller {
 
   // ------------------------- HELPERS -------------------------------------- //
   /// Return the z3::expr representing the current state at the time.
-  ZExpr CurrState(const ExprPtr v, const int& t);
+  ZExpr CurrState(const ExprPtr& v, const int& t);
   /// Return the z3::expr representing the next state at the time.
-  ZExpr NextState(const ExprPtr v, const int& t);
+  ZExpr NextState(const ExprPtr& v, const int& t);
   /// Return the z3::expr representing the current-based Expr at the time.
-  ZExpr GetZ3Expr(const ExprPtr e, const int& t);
+  ZExpr GetZ3Expr(const ExprPtr& e, const int& t);
   /// Return the z3::expr representing a unique Expr (regardless of time).
-  ZExpr GetZ3Expr(const ExprPtr e);
+  ZExpr GetZ3Expr(const ExprPtr& e);
   /// Return the z3::expr representing a and b are equal at their time.
-  ZExpr Equal(const ExprPtr va, const int& ta, const ExprPtr vb, const int& tb);
+  ZExpr Equal(const ExprPtr& va, const int& ta, const ExprPtr& vb,
+              const int& tb);
   /// Return the z3::func_decl representing f.
   z3::func_decl GetZ3FuncDecl(const FuncPtr& f) const;
 
@@ -93,12 +96,12 @@ class Unroller {
 
   // ------------------------- HELPERS -------------------------------------- //
   /// Return the state update function (unchanged if not defined).
-  static ExprPtr StateUpdCmpl(const InstrPtr instr, const ExprPtr var);
+  static ExprPtr StateUpdCmpl(const InstrPtr& instr, const ExprPtr& var);
   /// Return the decode function (true if not defined).
-  static ExprPtr DecodeCmpl(const InstrPtr instr);
+  static ExprPtr DecodeCmpl(const InstrPtr& instr);
 
   /// Create a new free variable (with same sort) under the same host.
-  static ExprPtr NewFreeVar(const ExprPtr var, const std::string& name);
+  static ExprPtr NewFreeVar(const ExprPtr& var, const std::string& name);
 
 private:
   // ------------------------- MEMBERS -------------------------------------- //
@@ -144,7 +147,7 @@ class Unroller {
                    const std::string& suffix);
 
   /// Clear the z3::epxr container.
-  inline void Clear(ZExprVec& z3_vec);
+  void Clear(ZExprVec& z3_vec);
 
   /// Generate and append the z3::expr for the set of Expr w.r.t. the suffix.
   void IExprToZExpr(const IExprVec& i_expr_src, const std::string& suffix,
@@ -239,29 +242,29 @@ class MonoUnroll : public Unroller {
   /// \param[in] top the top-level ILA.
   /// \param[in] length number of steps to unroll.
   /// \param[in] pos the starting time frame.
-  ZExpr MonoSubs(const InstrLvlAbsPtr top, const int& length,
+  ZExpr MonoSubs(const InstrLvlAbsPtr& top, const int& length,
                  const int& pos = 0);
 
   /// \brief Unroll the ILA while asserting states are equal between each step.
   /// \param[in] top the top-level ILA.
   /// \param[in] length number of steps to unroll.
   /// \param[in] pos the starting time frame.
-  ZExpr MonoAssn(const InstrLvlAbsPtr top, const int& length,
+  ZExpr MonoAssn(const InstrLvlAbsPtr& top, const int& length,
                  const int& pos = 0);
 
   /// \brief Unroll the ILA without asserting states relations between steps.
   /// \param[in] top the top-level ILA.
   /// \param[in] length number of steps to unroll.
   /// \param[in] pos the starting time frame.
-  ZExpr MonoNone(const InstrLvlAbsPtr top, const int& length,
+  ZExpr MonoNone(const InstrLvlAbsPtr& top, const int& length,
                  const int& pos = 0);
 
   /// \brief Incrementally unrolling the ILA using MonoAssn (with transition
   /// relation being cached).
   /// \param[in] top the top-level ILA.
   /// \param[in] length number of steps to unroll.
   /// \param[in] pos the starting time frame.
-  ZExpr MonoIncr(const InstrLvlAbsPtr top, const int& length, const int& pos);
+  ZExpr MonoIncr(const InstrLvlAbsPtr& top, const int& length, const int& pos);
 
 protected:
   // ------------------------- METHODS -------------------------------------- //

include/ilang/ila-mngr/v_eq_check_legacy_bmc.h

@@ -6,9 +6,10 @@
 
 #include <map>
 
-#include "z3++.h"
+#include <z3++.h>
+
 #include <ilang/ila/instr_lvl_abs.h>
-#include <ilang/ila/z3_expr_adapter.h>
+#include <ilang/target-smt/z3_expr_adapter.h>
 #include <ilang/util/container.h>
 
 /// \namespace ilang
@@ -64,14 +65,14 @@ class LegacyBmc {
 
   /// \brief Get the set of z3 expression (constraints) for the instruction.
   /// - States with no update functions are encoded as unchanged.
-  z3::expr Instr(const InstrPtr instr, const std::string& suffix_prev,
+  z3::expr Instr(const InstrPtr& instr, const std::string& suffix_prev,
                  const std::string& suffix_next, bool complete);
 
   /// \brief Get the set of z3 expression (constraints) for the ILA.
   /// - Assume no child-ILAs (not considered).
   /// - States with no update functions are encoded as unchanged.
   /// - Assume one-hot encoding of all instructions.
-  z3::expr IlaOneHotFlat(const InstrLvlAbsPtr ila,
+  z3::expr IlaOneHotFlat(const InstrLvlAbsPtr& ila,
                          const std::string& suffix_prev,
                          const std::string& suffix_next);