Fix parts with inconsistent convention

include/ilang/ila/ast/expr.h

@@ -16,7 +16,6 @@
 
 #include <ilang/ila/ast/ast.h>
 #include <ilang/ila/ast/sort.h>
-#include <ilang/ila/defines.h>
 
 /// \namespace ilang
 namespace ilang {
@@ -30,6 +29,11 @@ class Expr : public Ast, public std::enable_shared_from_this<Expr> {
   /// Type for storing a set of Expr.
   typedef std::vector<ExprPtr> ExprPtrVec;
 
+protected:
+  /// Vector type for z3 expression.
+  typedef std::vector<z3::expr> Z3ExprVec;
+
+public:
   // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
   /// Default constructor.
   Expr();

include/ilang/ila/ast/func.h

@@ -4,10 +4,14 @@
 #ifndef ILANG_ILA_AST_FUNC_H__
 #define ILANG_ILA_AST_FUNC_H__
 
-#include "z3++.h"
+#include <memory>
+#include <string>
+#include <vector>
+
+#include <z3++.h>
+
 #include <ilang/ila/ast/ast.h>
 #include <ilang/ila/ast/sort.h>
-#include <ilang/ila/defines.h>
 
 /// \namespace ilang
 namespace ilang {

include/ilang/ila/instr.h

@@ -5,6 +5,7 @@
 #define ILANG_ILA_INSTR_H__
 
 #include <memory>
+#include <set>
 #include <string>
 
 #include <ilang/ila/hash_ast.h>

include/ilang/ilang++.h

@@ -10,7 +10,7 @@
 #include <string>
 #include <vector>
 
-#include "z3++.h"
+#include <z3++.h>
 
 #include <ilang/config.h>
 
@@ -66,7 +66,7 @@ class SortRef {
   typedef std::shared_ptr<Sort> SortPtr;
   // ------------------------- MEMBERS -------------------------------------- //
   /// Wrapped Sort pointer.
-  SortPtr ptr_ = NULL;
+  SortPtr ptr_ = nullptr;
 
 public:
   // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
@@ -94,7 +94,7 @@ class ExprRef {
   typedef std::shared_ptr<Expr> ExprPtr;
   // ------------------------- MEMBERS -------------------------------------- //
   /// Wrapped Expr pointer.
-  ExprPtr ptr_ = NULL;
+  ExprPtr ptr_ = nullptr;
 
 public:
   // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
@@ -378,7 +378,7 @@ class FuncRef {
   typedef std::shared_ptr<Func> FuncPtr;
   // ------------------------- MEMBERS -------------------------------------- //
   /// Wrapped Func pointer.
-  FuncPtr ptr_ = NULL;
+  FuncPtr ptr_ = nullptr;
 
 public:
   // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
@@ -419,7 +419,7 @@ class InstrRef {
   typedef std::shared_ptr<Instr> InstrPtr;
   // ------------------------- MEMBERS -------------------------------------- //
   /// Wrapped Instr pointer.
-  InstrPtr ptr_ = NULL;
+  InstrPtr ptr_ = nullptr;
 
 public:
   // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
@@ -475,7 +475,7 @@ class Ila {
   typedef std::shared_ptr<InstrLvlAbs> IlaPtr;
   // ------------------------- MEMBERS -------------------------------------- //
   /// Wrapped InstrLvlAbs pointer.
-  IlaPtr ptr_ = NULL;
+  IlaPtr ptr_ = nullptr;
 
 public:
   // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
@@ -726,7 +726,7 @@ class IlaZ3Unroller {
   std::string extra_suff_;
 
   /// Pointer for calling universal functions.
-  std::shared_ptr<Unroller> univ_ = NULL;
+  std::shared_ptr<Unroller> univ_ = nullptr;
 
   // ------------------------- HELPERS -------------------------------------- //
   /// Initialize the unroller based on its dynamic type.

include/ilang/target-sc/ilator.h

@@ -41,14 +41,14 @@ class Ilator {
   class CxxFunc {
   public:
     CxxFunc(const std::string& in_name, const ExprPtr& in_ret,
-            const ExprPtr& in_target = NULL)
+            const ExprPtr& in_target = nullptr)
         : name(in_name), ret(in_ret), target(in_target) {}
     CxxFunc(const std::string& in_name, const SortPtr& in_ret_type)
         : name(in_name), ret_type(in_ret_type) {}
     const std::string name = "";
-    const ExprPtr ret = NULL;
-    const ExprPtr target = NULL;
-    const SortPtr ret_type = NULL;
+    const ExprPtr ret = nullptr;
+    const ExprPtr target = nullptr;
+    const SortPtr ret_type = nullptr;
     std::vector<SortPtr> args;
   };
 
@@ -113,7 +113,7 @@ class Ilator {
 
   /// Request a function with the specified name and return var.
   CxxFunc* RegisterFunction(const std::string& func_name,
-                            ExprPtr return_expr = NULL);
+                            ExprPtr return_expr = nullptr);
   /// Request a function simulating the uninterpreted function.
   CxxFunc* RegisterExternalFunc(const FuncPtr& func);
   /// Request a wrapping function for memory operation.

include/ilang/util/fs.h

@@ -50,10 +50,6 @@ std::string os_portable_join_dir(const std::vector<std::string>& dirs);
 /// C:\\a.txt -> C:\\a   or  /a/b/c.txt -> a/b/c
 std::string os_portable_remove_file_name_extension(const std::string& fname);
 
-/// Compare two file
-bool os_portable_compare_file(const std::string& file1,
-                              const std::string& file2);
-
 /// the result from executing
 struct execute_result {
   /// has timeout

src/ila-mngr/p_rewrite_conditional_store.cc

@@ -11,6 +11,8 @@ namespace ilang {
 
 namespace pass {
 
+#define DBG_TAG "PassRewrCondStore"
+
 class FuncObjRewrCondStore : public FuncObjRewrExpr {
 public:
   FuncObjRewrCondStore() : FuncObjRewrExpr({}) {}
@@ -41,7 +43,7 @@ class FuncObjRewrCondStore : public FuncObjRewrExpr {
     // pattern 0 - identical branch
     //  Ex. ITE(x, m, m)
     if (mem1 == mem2) {
-      ILA_DLOG("PassRewrCondStore") << "Identical branches - ITE(x, m, m)";
+      ILA_DLOG(DBG_TAG) << "Identical branches - ITE(x, m, m)";
       return mem1;
     }
 
@@ -50,8 +52,7 @@ class FuncObjRewrCondStore : public FuncObjRewrExpr {
     if (IsStore(mem1) && !mem2->is_op()) {
       if (mem1->arg(0) == mem2) {
 
-        ILA_DLOG("PassRewrCondStore")
-            << "Single STORE - ITE(x, m, ST(m, a, d))";
+        ILA_DLOG(DBG_TAG) << "Single STORE - ITE(x, m, ST(m, a, d))";
 
         auto mem1_addr = mem1->arg(1);
         auto mem1_data = mem1->arg(2);
@@ -64,8 +65,7 @@ class FuncObjRewrCondStore : public FuncObjRewrExpr {
     if (!mem1->is_op() && IsStore(mem2)) {
       if (mem2->arg(0) == mem1) {
 
-        ILA_DLOG("PassRewrCondStore")
-            << "Single STORE - ITE(x, ST(m, a, d), m)";
+        ILA_DLOG(DBG_TAG) << "Single STORE - ITE(x, ST(m, a, d), m)";
 
         auto mem2_addr = mem2->arg(1);
         auto mem2_data = mem2->arg(2);
@@ -80,7 +80,7 @@ class FuncObjRewrCondStore : public FuncObjRewrExpr {
     if (IsStore(mem1) && IsStore(mem2)) {
       if (mem1->arg(0) == mem2->arg(0)) {
 
-        ILA_DLOG("PassRewrCondStore")
+        ILA_DLOG(DBG_TAG)
             << "Identical STORE dest. - ITE(x, ST(m,a,b), ST(m,c,d))";
 
         auto new_addr = asthub::Ite(cond, mem1->arg(1), mem2->arg(1));
@@ -101,7 +101,7 @@ class FuncObjRewrCondStore : public FuncObjRewrExpr {
     //  Ex. ITE(x, STORE(STORE(v, a1, d1), a2, d2), STORE(v, a3, d3))
     // TODO extend the shorter one ... (any benefit?)
 
-    ILA_DLOG("PassRewrCondStore") << "Skip pattern " << mem1 << " " << mem2;
+    ILA_DLOG(DBG_TAG) << "Skip pattern " << mem1 << " " << mem2;
 
     return FuncObjRewrExpr::RewriteOp(e);
   }

src/ila-mngr/p_simplify_semantic.cc

@@ -35,7 +35,7 @@ class FuncObjEqSubtree {
   ExprMap rule_;
   ExprPtr target_;
   ExprPtr assump_;
-  ExprPtr candidate_ = NULL;
+  ExprPtr candidate_ = nullptr;
 
   ExprPtr Rewrite(const ExprPtr& e) {
 

src/ila-mngr/u_abs_knob.cc

@@ -3,8 +3,6 @@
 
 #include <ilang/ila-mngr/u_abs_knob.h>
 
-#include <functional>
-
 #include <ilang/ila-mngr/u_rewriter.h>
 #include <ilang/util/log.h>
 
@@ -343,7 +341,7 @@ ExprPtr DuplFetch(const InstrLvlAbsCnstPtr& src, const InstrLvlAbsPtr& dst,
   auto f_src = src->fetch();
   if (!f_src) {
     ILA_WARN << "Fetch not set for " << src;
-    return NULL;
+    return nullptr;
   }
   auto f_dst = Rewrite(f_src, expr_map);
   dst->SetFetch(f_dst);
@@ -355,7 +353,7 @@ ExprPtr DuplValid(const InstrLvlAbsCnstPtr& src, const InstrLvlAbsPtr& dst,
   auto v_src = src->valid();
   if (!v_src) {
     ILA_WARN << "Valid not set for " << src;
-    return NULL;
+    return nullptr;
   }
   auto v_dst = Rewrite(v_src, expr_map);
   dst->SetValid(v_dst);

src/ila-mngr/v_eq_check_bmc.cc

@@ -39,7 +39,7 @@ z3::check_result LegacyBmc::Check(InstrLvlAbsPtr m0, const int& k0,
   for (size_t i = 0; i != state_num_m0; i++) {
     auto state_m0 = m0->state(i);
     auto state_m1 = m1->find_state(state_m0->name());
-    ILA_ASSERT(state_m1 != NULL) << "State unmatched: " << state_m0;
+    ILA_NOT_NULL(state_m1);
 
     // equal initial condition
     auto state_m0_init = gen.GetExpr(state_m0, suffix_init);
@@ -59,7 +59,7 @@ z3::check_result LegacyBmc::Check(InstrLvlAbsPtr m0, const int& k0,
   for (size_t i = 0; i != input_num_m0; i++) {
     auto input_m0 = m0->input(i);
     auto input_m1 = m1->find_input(input_m0->name());
-    ILA_ASSERT(input_m1 != NULL) << "Input unmatched: " << input_m0;
+    ILA_NOT_NULL(input_m1);
 
     auto input_m0_init = gen.GetExpr(input_m0, suffix_init);
     auto input_m1_init = gen.GetExpr(input_m1, suffix_init);
@@ -131,7 +131,7 @@ z3::expr LegacyBmc::Instr(const InstrPtr& instr, const std::string& suffix_prev,
     auto state_n = ila->state(i);
     auto update_n = instr->update(state_n);
 
-    if (update_n != NULL) { // update function specified
+    if (update_n) { // update function specified
       auto next_val_e = gen_.GetExpr(update_n, suffix_prev);
       auto next_var_e = gen_.GetExpr(state_n, suffix_next);
       auto eq_cnst = (next_var_e == next_val_e);

src/ila-mngr/v_eq_check_crr.cc

@@ -233,7 +233,7 @@ RefPtr CommDiag::GetRefine(const UID& uid) {
     break;
   default:
     ILA_ASSERT(false) << "unknon uid " << uid;
-    return NULL;
+    return nullptr;
     break;
   }
 }

src/ila/hash_ast.cc

@@ -53,21 +53,21 @@ void ExprMngr::operator()(const ExprPtr& node) {
 }
 
 std::string ExprMngr::Hash(const ExprPtr& expr) {
-  static const char* template_var = "var::{sort}::{id}";
-  static const char* template_const = "const::{sort}::{value}";
-  static const char* template_op = "op::{sort}::{op}::{arg_list}::{param_list}";
-  static const char* template_sort = "{type}_{bit}_{addr}_{data}";
+  static const char* kTemplateVar = "var::{sort}::{id}";
+  static const char* kTemplateConst = "const::{sort}::{value}";
+  static const char* kTemplateOp = "op::{sort}::{op}::{arg_list}::{param_list}";
+  static const char* kTemplateSort = "{type}_{bit}_{addr}_{data}";
 
   auto GetSortHash = [](const SortPtr& sort) {
     return fmt::format(
-        template_sort, fmt::arg("type", sort->uid()),
+        kTemplateSort, fmt::arg("type", sort->uid()),
         fmt::arg("bit", sort->is_bv() ? sort->bit_width() : 0),
         fmt::arg("addr", sort->is_mem() ? sort->addr_width() : 0),
         fmt::arg("data", sort->is_mem() ? sort->data_width() : 0));
   };
 
   if (expr->is_var()) {
-    return fmt::format(template_var,
+    return fmt::format(kTemplateVar,
                        fmt::arg("sort", GetSortHash(expr->sort())),
                        fmt::arg("id", expr->name().id()));
 
@@ -82,7 +82,7 @@ std::string ExprMngr::Hash(const ExprPtr& expr) {
     }
     // skip sharing memory constants
 
-    return fmt::format(template_const,
+    return fmt::format(kTemplateConst,
                        fmt::arg("sort", GetSortHash(expr->sort())),
                        fmt::arg("value", value));
   } else {
@@ -101,7 +101,7 @@ std::string ExprMngr::Hash(const ExprPtr& expr) {
       param_list.push_back(expr->param(i));
     }
 
-    return fmt::format(template_op, fmt::arg("op", asthub::GetUidExprOp(expr)),
+    return fmt::format(kTemplateOp, fmt::arg("op", asthub::GetUidExprOp(expr)),
                        fmt::arg("sort", GetSortHash(expr->sort())),
                        fmt::arg("arg_list", fmt::join(arg_list, ",")),
                        fmt::arg("param_list", fmt::join(param_list, ",")));

src/target-itsy/abst_to_ila.cc

@@ -311,7 +311,7 @@ void SynthAbsConverter::PortInstructions(const ilasynth::Abstraction& abs,
     // next state functions are conjuncted when being exported
     auto name = var->name().str();
 
-    auto next_expr = ExprPtr(NULL);
+    ExprPtr next_expr = nullptr;
     try {
       auto next_node = abs.getNext(name)->node;
       next_expr = ConvertSynthNodeToIlangExpr(next_node, ila);
@@ -343,7 +343,7 @@ void SynthAbsConverter::DecomposeExpr(const ExprPtr& src) {
 
   auto Compare = [this](const ExprPtr& n) {
     // syntactically decompose at ITE nodes
-    const ExprOpIte* expr_ite = NULL;
+    const ExprOpIte* expr_ite = nullptr;
     if ((expr_ite = dynamic_cast<const ExprOpIte*>(n.get()))) {
       // check if the condition argument is one of the entries
       auto condition = n->arg(0);
@@ -426,7 +426,7 @@ void SynthAbsConverter::CnvtNodeToExpr(const ilasynth::Node* n) {
 
 void SynthAbsConverter::CnvtNodeToExprConst(const ilasynth::Node* n) {
   // place holder for the result
-  decltype(asthub::BoolConst(true)) expr = NULL;
+  decltype(asthub::BoolConst(true)) expr = nullptr;
 
   auto type = n->getType();
   switch (type.type) {
@@ -488,7 +488,7 @@ void SynthAbsConverter::CnvtNodeToExprBoolOp(const ilasynth::Node* n) {
   auto op_ptr = dynamic_cast<const ilasynth::BoolOp*>(n);
   ILA_CHECK(op_ptr) << "Fail casting " << n->getName() << " to Bool Op";
 
-  decltype(asthub::BoolConst(true)) expr = NULL;
+  decltype(asthub::BoolConst(true)) expr = nullptr;
 
   switch (op_ptr->getOp()) {
   case ilasynth::BoolOp::Op::NOT:
@@ -589,7 +589,7 @@ void SynthAbsConverter::CnvtNodeToExprBvOp(const ilasynth::Node* n) {
   auto op_ptr = dynamic_cast<const ilasynth::BitvectorOp*>(n);
   ILA_CHECK(op_ptr) << "Fail casting " << n->getName() << " to Bv Op";
 
-  decltype(asthub::BvConst(1, 1)) expr = NULL;
+  decltype(asthub::BvConst(1, 1)) expr = nullptr;
 
   switch (op_ptr->getOp()) {
   case ilasynth::BitvectorOp::Op::NEGATE:
@@ -737,7 +737,7 @@ void SynthAbsConverter::CnvtNodeToExprMemOp(const ilasynth::Node* n) {
   auto op_ptr = dynamic_cast<const ilasynth::MemOp*>(n);
   ILA_CHECK(op_ptr) << "Fail casting " << n->getName() << " to Mem Op";
 
-  decltype(asthub::MemConst(0, 8, 8)) expr = NULL;
+  decltype(asthub::MemConst(0, 8, 8)) expr = nullptr;
 
   switch (op_ptr->getOp()) {
   case ilasynth::MemOp::Op::STORE: