Merge pull request #97 from Bo-Yuan-Huang/dev

Dev.

.lgtm.yml

@@ -11,9 +11,8 @@ path_classifiers:
   script:
     - scripts
 
-  example:
+  application:
     - apps
-    - examples
 
 extraction:
   cpp:
@@ -30,7 +29,7 @@ extraction:
       command:
         - mkdir -p build
         - cd build
-        - cmake ..
+        - cmake .. -DILANG_STATIC=ON
 
     index:
       build_command:

CMakeLists.txt

@@ -20,6 +20,7 @@ project(ilang VERSION     0.9.0
 # OPTION
 # build configuration
 # ---------------------------------------------------------------------------- #
+option(ILANG_STATIC      "Build static libraries."                          OFF)
 option(ILANG_FETCH_DEPS  "Fetch source of dependencies at config time."      ON)
 option(ILANG_BUILD_DOCS  "Build documentations."                            OFF)
 option(ILANG_BUILD_SYNTH "Build the synthesis engine."                       ON)

LICENSE

@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2019
+Copyright (c) 2019 Princeton University ILA Team
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

include/ilang/ila/ast/expr_op.h

@@ -185,7 +185,15 @@ class ExprOpSub : public ExprOp {
 
 // TODO ExprOpMod
 
-// TODO ExprOpMul
+/// \brief The wrapper for unsigned multiplication.
+class ExprOpMul : public ExprOp {
+public:
+  /// Constructor for MUL operation.
+  ExprOpMul(const ExprPtr arg0, const ExprPtr arg1);
+  std::string op_name() const { return "MUL"; }
+  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
+                     const std::string& suffix = "") const;
+}; // class ExprOpMul
 
 /******************************************************************************/
 // Binary comparison

include/ilang/ila/ast_fuse.h

@@ -30,6 +30,7 @@ enum AST_UID_EXPR_OP {
   LSHR,
   ADD,
   SUB,
+  MUL,
   EQ,
   LT,
   GT,

include/ilang/ila/expr_fuse.h

@@ -101,6 +101,8 @@ ExprPtr Lshr(const ExprPtr l, const int& r);
 ExprPtr Add(const ExprPtr l, const int& r);
 /// Arithmetic subtraction with int.
 ExprPtr Sub(const ExprPtr l, const int& r);
+/// Arithmetic unsigned multiply with int (bv only).
+ExprPtr Mul(const ExprPtr l, const int& r);
 
 /******************************************************************************/
 // Comparison
@@ -163,6 +165,11 @@ ExprPtr Load(const ExprPtr mem, const int& addr);
 /// Memory store to constant address and data
 ExprPtr Store(const ExprPtr mem, const int& addr, const int& data);
 
+/// Set memory size.
+bool SetMemSize(const ExprPtr mem, const int& size = 0);
+/// Get memory size.
+int GetMemSize(const ExprPtr mem);
+
 /******************************************************************************/
 // Bit manipulation
 /******************************************************************************/

include/ilang/ilang++.h

@@ -137,6 +137,11 @@ class ExprRef {
   /// \brief Replace the original argument (must exist) with the new argument.
   void ReplaceArg(const ExprRef& org_arg, const ExprRef& new_arg);
 
+  /// \brief Set the entry number of the memory (size regardless of bit-width).
+  bool SetEntryNum(const int& num);
+  /// \brief GEt the entry number of the memory (size regardless of bit-width).
+  int GetEntryNum();
+
 }; // class ExprRef
 
 /******************************************************************************/
@@ -168,6 +173,8 @@ ExprRef Lshr(const ExprRef& a, const ExprRef& b);
 ExprRef operator+(const ExprRef& a, const ExprRef& b);
 /// Unsigned subtraction for bit-vectors.
 ExprRef operator-(const ExprRef& a, const ExprRef& b);
+/// Unsigned multiply for bit-vectors.
+ExprRef operator*(const ExprRef& a, const ExprRef& b);
 
 /// Logical AND with Boolean constant.
 ExprRef operator&(const ExprRef& a, const bool& b);
@@ -185,6 +192,8 @@ ExprRef Lshr(const ExprRef& a, const int& b);
 ExprRef operator+(const ExprRef& a, const int& b);
 /// Unsigned subtraction with int constant.
 ExprRef operator-(const ExprRef& a, const int& b);
+/// Unsigned multiply with int constant.
+ExprRef operator*(const ExprRef& a, const int& b);
 
 /******************************************************************************/
 // Binary comparison
@@ -485,7 +494,7 @@ class Ila {
 
   // ------------------------- GENERATORS --------------------------------- //
   /// \brief Export an ILA as Verilog
-  /// \param[in] filename the file name of the generated Verilog source
+  /// \param[in] fout the output stream of the generated Verilog source.
   void ExportToVerilog(std::ostream& fout) const;
 
   // ------------------------- ACCESSORS/MUTATORS --------------------------- //
@@ -542,6 +551,18 @@ std::ostream& operator<<(std::ostream& out, const InstrRef& instr);
 /// Print out the ILA.
 std::ostream& operator<<(std::ostream& out, const Ila& ila);
 
+/******************************************************************************/
+// Converters
+/******************************************************************************/
+/// \brief Export the ILA portable to file.
+/// \param[in] ila the source ILA model to export.
+/// \param[in] file_name the name of the exported ILA portable (JSON) file.
+bool ExportIlaPortable(const Ila& ila, const std::string& file_name);
+
+/// \brief Import the ILA portable from file.
+/// \param[in] file_name the name of the ILA portable (JSON) file to import.
+Ila ImportIlaPortable(const std::string& file_name);
+
 /******************************************************************************/
 // Verification.
 /******************************************************************************/

include/ilang/portable/ila_to_json_serializer.h

@@ -36,23 +36,31 @@ class I2JSer {
   json SerExpr(const ExprPtr& i_expr);
   /// \brief Serialize Instr to JSON.
   json SerInstr(const InstrPtr& i_instr);
-  /// \brief Serialize InstrLvlAbs to JSON.
+  /// \brief Serialize InstrLvlAbs, including its children, to JSON.
   json SerInstrLvlAbs(const InstrLvlAbsPtr& i_ila);
 
 private:
   // ------------------------- MEMBERS -------------------------------------- //
   /// A map from visited i_expr id to j_expr array index.
   std::unordered_map<size_t, size_t> id_idx_map_;
+  /// A map from visited i_func id to j_func array index.
+  std::unordered_map<size_t, size_t> func_id_idx_map_;
   /// The list of all serialized expressions (j_expr array).
   json j_expr_arr_;
+  /// The list of all serialized functions (j_func array).
+  json j_func_arr_;
 
   // ------------------------- METHODS -------------------------------------- //
   /// Serialize Sort to JSON.
   json SerSort(const SortPtr& i_sort) const;
+  /// Serialize Func to JSON.
+  json SerFunc(const FuncPtr& i_func);
   /// Serialize constant value to JSON.
   json SerConstVal(const ExprPtr& i_expr) const;
   /// Serialize one single Expr.
   json SerExprUnit(const ExprPtr& i_expr);
+  /// Serialize InstrLvlAbs and its children, excluding the AST list.
+  json SerInstrLvlAbsNoAst(const InstrLvlAbsPtr& i_ila);
 
 }; // class I2JSer
 

include/ilang/portable/interface.h

@@ -30,8 +30,10 @@ class IlaSerDesMngr {
   /// \brief Serialize the ILA model to the given file.
   /// \param[in] m the ILA model to serialize.
   /// \param[in] file_name the output file name.
+  /// \param[in] indent the number of space to indent.
   /// \return Return true if complete sucessfully.
-  static bool SerToFile(const InstrLvlAbsPtr& m, const std::string& file_name);
+  static bool SerToFile(const InstrLvlAbsPtr& m, const std::string& file_name,
+                        const int& indent = -1);
 
   /// \brief Deserialize the ILA model from the given file.
   /// \param[in] file_name the input file name.

include/ilang/portable/json_to_ila_deserializer.h

@@ -8,7 +8,6 @@
 #include <memory>
 #include <nlohmann/json.hpp>
 #include <unordered_map>
-#include <unordered_set>
 
 using json = nlohmann::json;
 
@@ -33,21 +32,25 @@ class J2IDes {
   static J2IDesPtr New();
 
   // ------------------------- METHODS -------------------------------------- //
+  /// Deserialize Sort from JSON.
+  SortPtr DesSort(const json& j_sort);
+  /// Deserialize Func from JSON.
+  FuncPtr DesFunc(const json& j_func);
   /// \brief Deserialize Expr from JSON.
-  ExprPtr DesExpr(const json& j_expr, const InstrLvlAbsPtr& i_host);
+  ExprPtr DesExpr(const json& j_expr);
   /// \brief Deserialize Instr from JSON.
   InstrPtr DesInstr(const json& j_instr, const InstrLvlAbsPtr& i_host) const;
   /// \brief Deserialize InstrLvlAbs from JSON.
-  InstrLvlAbsPtr DesInstrLvlAbs(const json& j_ila);
+  InstrLvlAbsPtr DesInstrLvlAbs(const json& j_global);
 
 private:
   // ------------------------- MEMBERS -------------------------------------- //
-  /// A mapping from id to expressions.
+  /// A mapping from id to expression.
   std::unordered_map<size_t, ExprPtr> id_expr_map_;
-  /// The set of state variables.
-  std::unordered_set<size_t> state_id_set_;
-  /// The set of input variables.
-  std::unordered_set<size_t> input_id_set_;
+  /// A mapping from id to function.
+  std::unordered_map<size_t, FuncPtr> id_func_map_;
+  /// The mapping from ila name to pointer.
+  std::unordered_map<std::string, const InstrLvlAbsPtr> ila_name_ptr_map_;
 
   // ------------------------- METHODS -------------------------------------- //
   /// Deserialize ExprVar into state from JSON.
@@ -61,6 +64,22 @@ class J2IDes {
   /// Deserialize ExprOp from JSON.
   ExprPtr DesExprOp(const unsigned& ast_expr_op_uid, const json& j_arg_arr,
                     const json& j_param_arr) const;
+  /// Deserialize ExprOpAppFunc from JSON.
+  ExprPtr DesExprOpAppFunc(const json& j_func_id, const json& j_arg_arr) const;
+
+  /// Deserialize state/input variables. Note: the ILA model will be
+  /// constructed on-the-fly.
+  void DesVarUnit(const json& j_ila, const json& j_ast_list,
+                  const InstrLvlAbsPtr& i_parent);
+  /// Deserialize state/input variables hierarchically. Note: ILA model will be
+  /// constructed on-the-fly.
+  void DesVarHier(const json& j_ila, const json& j_ast_list,
+                  const InstrLvlAbsPtr& i_parent);
+
+  /// Deserialize ILA info, e.g., fetch, valid, instructions, etc.
+  void DesIlaUnit(const json& j_ila);
+  /// Deserialize ILA info hierarchically.
+  void DesIlaHier(const json& j_ila);
 
 }; // class J2IDes
 

include/ilang/portable/serdes_config.h

@@ -13,6 +13,12 @@ namespace ilang {
 #define SERDES_SORT_ADDR_WIDTH "a"
 #define SERDES_SORT_DATA_WIDTH "d"
 
+// Func
+#define SERDES_FUNC_ID "i"
+#define SERDES_FUNC_NAME "n"
+#define SERDES_FUNC_OUT "o"
+#define SERDES_FUNC_ARGS "a"
+
 // Expr
 #define SERDES_EXPR_ID "i"
 #define SERDES_EXPR_UID "u"
@@ -22,6 +28,7 @@ namespace ilang {
 #define SERDES_EXPR_OP "o"
 #define SERDES_EXPR_ARGS "a"
 #define SERDES_EXPR_PARAMS "p"
+#define SERDES_EXPR_FUNC "f"
 
 // Instr
 #define SERDES_INSTR_NAME "n"
@@ -36,13 +43,18 @@ namespace ilang {
 #define SERDES_ILA_VALID "v"
 #define SERDES_ILA_INSTR "instr"
 #define SERDES_ILA_INIT "init"
-#define SERDES_ILA_AST "a"
+#define SERDES_ILA_CHILD "c"
 
 // ConstVal
 #define SERDES_CONST_VAL "v"
 #define SERDES_CONST_DEF "d"
 #define SERDES_CONST_MAP "m"
 
+// Global
+#define SERDES_GLOBAL_AST "a"
+#define SERDES_GLOBAL_FUNC "f"
+#define SERDES_GLOBAL_TOP "t"
+
 }; // namespace ilang
 
 #endif // ILANG_PORTABLE_SERDES_CONFIG_H__

include/ilang/target-c/ila_to_c.h

@@ -0,0 +1,54 @@
+/// \file
+/// ILA to C target generator..
+
+#ifndef ILANG_TARGET_I2C_H__
+#define ILANG_TARGET_I2C_H__
+
+#include <ilang/ila/instr_lvl_abs.h>
+#include <memory>
+#include <unordered_map>
+
+/// \namespace ilang
+namespace ilang {
+
+/// \brief The calss for converting an ILA model to a C target.
+class I2CMngr {
+public:
+  /// Pointer type for normal use of I2CMngr.
+  typedef std::shared_ptr<I2CMngr> I2CMngrPtr;
+
+  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
+  /// Default constructor.
+  I2CMngr();
+  /// Default destructor.
+  ~I2CMngr();
+
+  // ------------------------- HELPERS -------------------------------------- //
+  /// \brief Create a new I2CMngr. Used for hiding implementation specific type
+  /// details.
+  static I2CMngrPtr New();
+
+  // ------------------------- METHODS -------------------------------------- //
+  /// \brief Generate a C target of the given ILA model.
+  /// \param[in] ila The top-level ILA model to generate the C target for.
+  /// \param[out] C intermediate representation.
+  void GenerateCTarget(const InstrLvlAbsPtr& ila);
+
+private:
+  // ------------------------- MEMBERS -------------------------------------- //
+  /// A map from visited i_expr id to c_var array index.
+  std::unordered_map<size_t, size_t> id_var_map_;
+
+  // ------------------------- METHODS -------------------------------------- //
+  /// Convert constant node to c contant.
+  void ConvertConst(const ExprPtr& expr) const;
+
+}; // class I2CMngr
+
+/// Pointer type for normal use of I2CMngr.
+typedef I2CMngr::I2CMngrPtr I2CMngrPtr;
+
+}; // namespace ilang
+
+#endif // ILANG_TARGET_I2C_H__
+

src/CMakeLists.txt

@@ -2,20 +2,26 @@
 # TARGET
 # archive library 
 # ---------------------------------------------------------------------------- #
-add_library(${ILANG_LIB_NAME} ilang++.cc)
+if(${ILANG_STATIC})
+  add_library(${ILANG_LIB_NAME} STATIC ilang++.cc)
+else()
+  add_library(${ILANG_LIB_NAME} SHARED ilang++.cc)
+endif()
+
 add_library(${PROJECT_NAME}::${ILANG_LIB_NAME} ALIAS ${ILANG_LIB_NAME})
 
 ##
 ## source files
 ##
-add_subdirectory(util)
 add_subdirectory(ila)
+add_subdirectory(mcm)
+add_subdirectory(portable)
+add_subdirectory(target-c)
+add_subdirectory(util)
 add_subdirectory(verification)
 add_subdirectory(verilog-in)
 add_subdirectory(verilog-out)
 add_subdirectory(vtarget-out)
-add_subdirectory(mcm)
-add_subdirectory(portable)
 
 if(${ILANG_BUILD_SYNTH})
   add_subdirectory(synth-interface)

src/ila/ast/expr_op.cc

@@ -263,6 +263,19 @@ z3::expr ExprOpSub::GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
   return expr_vec[0] - expr_vec[1];
 }
 
+// ------------------------- Class ExprOpMul ------------------------------- //
+ExprOpMul::ExprOpMul(const ExprPtr arg0, const ExprPtr arg1)
+    : ExprOp(arg0, arg1) {
+  set_sort(GetSortBinaryOperation(arg0, arg1));
+}
+
+z3::expr ExprOpMul::GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
+                              const std::string& suffix) const {
+  ILA_ASSERT(expr_vec.size() == 2) << "Mul is binary operation.";
+  ILA_ASSERT(is_bv()) << "Mul can only be applied to bv.";
+  return expr_vec[0] * expr_vec[1];
+}
+
 // ------------------------- Class ExprOpEq --------------------------------- //
 ExprOpEq::ExprOpEq(const ExprPtr arg0, const ExprPtr arg1)
     : ExprOp(arg0, arg1) {