Merge 3315da8 into cf82e07

.github/workflows/cmake.yml

@@ -13,7 +13,7 @@ jobs:
     - uses: actions/checkout@v2
 
     - name: Install Dependent Packages
-      run: sudo apt install bison flex z3 libz3-dev
+      run: sudo apt install bison flex z3 libz3-dev libfl-dev
 
     - name: Create Build Environment
       run: cmake -E make_directory ${{runner.workspace}}/build

.gitmodules

@@ -7,3 +7,6 @@
 [submodule "extern/smt-switch"]
 	path = extern/smt-switch
 	url = https://github.com/makaimann/smt-switch.git
+[submodule "extern/vexpparser"]
+	path = extern/vexpparser
+	url = https://github.com/zhanghongce/vexpparser.git

.travis.yml

@@ -57,6 +57,7 @@ jobs:
             - bison
             - z3
             - libz3-dev
+            - libfl-dev
             - g++-7
       before_install:
         - echo -n | openssl s_client -connect https://scan.coverity.com:443 | sed -ne '/-BEGIN CERTIFICATE-/,/-END CERTIFICATE-/p' | sudo tee -a /etc/ssl/certs/ca-
@@ -77,6 +78,7 @@ addons:
       - bison
       - z3
       - libz3-dev
+      - libfl-dev
       - g++-7
 
 notifications:

extern/CMakeLists.txt

@@ -126,6 +126,39 @@ if(NOT VERILOGPARSER_FOUND)
 endif() # VERILOGPARSER_FOUND
 
 
+# ---------------------------------------------------------------------------- #
+# Verilog Expression Parser
+# 
+#   TARGET vexpparser::vexpparser
+#   SOURCE https://github.com/zhanghongce/vexpparser.git
+#   PATH   extern/vexpparser
+# ---------------------------------------------------------------------------- #
+# find installed package
+find_package(vexpparser 1.1.0 QUIET)
+
+# embed to build tree if not installed
+if(NOT VEXP_PARSER_FOUND)
+
+  # fetch from git
+  if(${ILANG_FETCH_DEPS})
+
+    execute_process(
+      COMMAND ${GIT_EXECUTABLE} submodule update --init vexpparser
+      WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+      RESULT_VARIABLE GIT_SUBMOD_RESULT
+    )
+
+    if(NOT GIT_SUBMOD_RESULT EQUAL "0")
+      message(FATAL_ERROR "Submodule update failed with ${GIT_SUBMOD_RESULT}")
+    endif()
+
+  endif() # ILANG_FETCH_DEPS
+
+  # embedded build
+  add_subdirectory(vexpparser)
+
+endif() # VERILOGPARSER_FOUND
+
 # ---------------------------------------------------------------------------- #
 # Template-based ILA Synthesis
 #

include/ilang/rfmap-in/rfexpr_shortcut.h

@@ -0,0 +1,38 @@
+/// \file rfexpr_shortcut.h Refinement map expression
+/// construction
+/// Hongce Zhang (zhanghongce@126.com)
+
+#ifndef ILANG_RFEXPR_SHORTCUT_H__
+#define ILANG_RFEXPR_SHORTCUT_H__
+
+#include <ilang/rfmap-in/rfmap_typecheck.h>
+
+namespace ilang {
+
+rfmap::RfExpr rfmap_reduce_or(const rfmap::RfExpr& in);
+rfmap::RfExpr rfmap_imply(const rfmap::RfExpr& l, const rfmap::RfExpr& r);
+rfmap::RfExpr rfmap_and(const rfmap::RfExpr& l, const rfmap::RfExpr& r);
+rfmap::RfExpr rfmap_or(const rfmap::RfExpr& l, const rfmap::RfExpr& r);
+rfmap::RfExpr rfmap_and(const std::vector<rfmap::RfExpr>& v);
+rfmap::RfExpr rfmap_or(const std::vector<rfmap::RfExpr>& v);
+
+rfmap::RfExpr rfmap_ite(const rfmap::RfExpr& c, const rfmap::RfExpr& l,
+                        const rfmap::RfExpr& r);
+
+rfmap::RfExpr rfmap_eq(const rfmap::RfExpr& l, const rfmap::RfExpr& r);
+rfmap::RfExpr rfmap_le(const rfmap::RfExpr& l, const rfmap::RfExpr& r);
+
+rfmap::RfExpr rfmap_not(const rfmap::RfExpr& l);
+
+rfmap::RfExpr rfmap_true();
+rfmap::RfExpr rfmap_false();
+rfmap::RfExpr rfmap_const(unsigned b, unsigned w, unsigned v);
+/// if it is RTL. or ILA. then will use MakeVar
+/// otherwise will use MakeSpecial
+/// will not determine its type
+/// ReplExpr will determine the type
+rfmap::RfExpr rfmap_var(const std::string& v);
+
+} // namespace ilang
+
+#endif // ILANG_RFEXPR_SHORTCUT_H__

include/ilang/rfmap-in/rfexpr_to_smt.h

@@ -0,0 +1,58 @@
+/// \file rfexpr_to_smt.cc Refinement map to smt-lib2
+/// Hongce Zhang (hongcez@princeton.edu)
+
+#ifndef ILANG_RFEXPR_TO_SMT_H__
+#define ILANG_RFEXPR_TO_SMT_H__
+
+#include <ilang/rfmap-in/rfmap_typecheck.h>
+
+namespace ilang {
+namespace rfmap {
+
+struct SmtType : public RfMapVarType {
+  bool bool_or_bv;
+
+  SmtType() : RfMapVarType(1), bool_or_bv(true) {}
+  SmtType(unsigned w) : RfMapVarType(w), bool_or_bv(false) {}
+  SmtType(unsigned a, unsigned d) : RfMapVarType(a, d), bool_or_bv(false) {}
+  SmtType(const RfMapVarType& r, bool request_bool)
+      : RfMapVarType(r), bool_or_bv(request_bool) {}
+
+  bool is_bool() const { return bool_or_bv && (RfMapVarType::is_bv()); }
+  bool is_bv() const { return (!bool_or_bv) && (RfMapVarType::is_bv()); }
+  bool operator==(const SmtType& r) const {
+    if (bool_or_bv != r.bool_or_bv)
+      return false;
+    if (type != r.type)
+      return false;
+    if (type == TYPE::BV)
+      return width == r.width;
+    if (type == TYPE::MEM)
+      return data_width == r.data_width && addr_width == r.addr_width;
+    return false; // unknown type , unknown
+  }               // operator=
+
+  std::string type_to_smt2() const;
+
+}; // SmtType
+
+struct RfExpr2Smt {
+
+public:
+  static std::string to_smt2(const RfExpr& in, SmtType expected_type);
+
+protected:
+  // helper function
+  static std::string
+  to_smt2_const(const std::shared_ptr<verilog_expr::VExprAstConstant>& in,
+                SmtType expected_type);
+  static std::string
+  to_smt2_var(const std::shared_ptr<verilog_expr::VExprAstVar>& in,
+              SmtType expected_type);
+
+}; // struct RfExpr2Smt
+
+} // namespace rfmap
+} // namespace ilang
+
+#endif // ILANG_RFEXPR_TO_SMT_H__