From d5eae6f0c7dfc446937fe0c270044185cbfb1b6a Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 27 Jul 2019 15:40:19 -0700 Subject: [PATCH 01/94] Use static_cast for known-typed casting (#141). --- src/target-itsy/abst_to_ila.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/target-itsy/abst_to_ila.cc b/src/target-itsy/abst_to_ila.cc index 7322f02ea..bb141920d 100644 --- a/src/target-itsy/abst_to_ila.cc +++ b/src/target-itsy/abst_to_ila.cc @@ -434,20 +434,20 @@ void SynthAbsConverter::CnvtNodeToExprConst(const ilasynth::Node* n) { auto type = n->getType(); switch (type.type) { case ilasynth::NodeType::Type::BOOL: { - auto bool_const = dynamic_cast(n); + auto bool_const = static_cast(n); expr = ExprFuse::BoolConst(bool_const->val()); break; } case ilasynth::NodeType::Type::BITVECTOR: { - auto bv_const = dynamic_cast(n); + auto bv_const = static_cast(n); auto val = static_cast(bv_const->val()); expr = ExprFuse::BvConst(val, type.bitWidth); break; } case ilasynth::NodeType::Type::MEM: { - auto mem_const = dynamic_cast(n); + auto mem_const = static_cast(n); auto def_value = static_cast(mem_const->memvalues.def_value); auto mem_value = MemVal(def_value); From fae386c5359e4bc1619643fb8d95ce8c797f5559 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 27 Jul 2019 16:06:10 -0700 Subject: [PATCH 02/94] Double check directory creation result (#141). --- src/util/fs.cc | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/util/fs.cc b/src/util/fs.cc index 0c04f32ce..ee1eea1de 100644 --- a/src/util/fs.cc +++ b/src/util/fs.cc @@ -46,7 +46,13 @@ bool os_portable_mkdir(const std::string& dir) { return true; } } - return mkdir(dir.c_str(), S_IRWXU | S_IRWXG | S_IROTH | S_IXOTH) != -1; + // return mkdir(dir.c_str(), S_IRWXU | S_IRWXG | S_IROTH | S_IXOTH) != -1; + mkdir(dir.c_str(), S_IRWXU | S_IRWXG | S_IROTH | S_IXOTH); + + if (stat(dir.c_str(), &statbuff) != -1) { + return S_ISDIR(statbuff.st_mode); + } + return false; #endif } From 31ff030bdbcab4dc6eed95a15e956cee764ed545 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 27 Jul 2019 16:06:49 -0700 Subject: [PATCH 03/94] Explicitly specifiy return value for the last case before default (#141). --- src/verilog-in/verilog_analysis.cc | 1 + 1 file changed, 1 insertion(+) diff --git a/src/verilog-in/verilog_analysis.cc b/src/verilog-in/verilog_analysis.cc index d40fdaefc..eee445a0d 100644 --- a/src/verilog-in/verilog_analysis.cc +++ b/src/verilog-in/verilog_analysis.cc @@ -657,6 +657,7 @@ SignalInfoBase VerilogAnalyzer::get_signal(const std::string& net_name) const { return SignalInfoReg((ast_reg_declaration*)ast_ptr, net_name, tp_, this); case MODULE: ILA_ERROR << "Module instance:" << net_name << " is not a signal."; + return bad_signal; default: ILA_ERROR << "Does not know how to handle:" << net_name << ", which is not a signal."; From e0620f52d83232f1a5591466dd5f7ce83bbe69ff Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 27 Jul 2019 16:26:20 -0700 Subject: [PATCH 04/94] Remove logically dead code (#141). --- include/ilang/vtarget-out/vtarget_gen_impl.h | 11 +++++---- src/vtarget-out/vtarget_gen_impl.cc | 25 ++++++++------------ 2 files changed, 16 insertions(+), 20 deletions(-) diff --git a/include/ilang/vtarget-out/vtarget_gen_impl.h b/include/ilang/vtarget-out/vtarget_gen_impl.h index 84034a13b..afbe25546 100644 --- a/include/ilang/vtarget-out/vtarget_gen_impl.h +++ b/include/ilang/vtarget-out/vtarget_gen_impl.h @@ -14,20 +14,21 @@ #ifndef VTARGET_GEN_IMPL_H__ #define VTARGET_GEN_IMPL_H__ -#include - -#include "nlohmann/json.hpp" -#include -#include #include #include #include #include + #include #include #include #include +#include "nlohmann/json.hpp" +#include +#include +#include + namespace ilang { /// \brief Generating a target (just the invairant or for an instruction) diff --git a/src/vtarget-out/vtarget_gen_impl.cc b/src/vtarget-out/vtarget_gen_impl.cc index 55b4924ba..bfb953265 100644 --- a/src/vtarget-out/vtarget_gen_impl.cc +++ b/src/vtarget-out/vtarget_gen_impl.cc @@ -2,22 +2,22 @@ /// // --- Hongce Zhang +#include + +#include +#include + #include #include #include #include #include #include -#include #include -#include -#include - namespace ilang { -// ------------------------------ VlgVerifTgtGen -// --------------------------------- // +// ------------------------------ VlgVerifTgtGen ---------------------------- // VlgVerifTgtGen::VlgVerifTgtGen( const std::vector& implementation_include_path, @@ -240,7 +240,7 @@ bool VlgVerifTgtGen::bad_state_return(void) { // return npos if no comments in static size_t find_comments(const std::string& line) { - enum state_t { PLAIN, STR, LEFT } state, next_state; + enum state_t { PLAIN, LEFT } state, next_state; state = PLAIN; size_t ret = 0; for (const auto& c : line) { @@ -249,19 +249,14 @@ static size_t find_comments(const std::string& line) { next_state = LEFT; else next_state = PLAIN; - } else if (state == STR) { - if (c == '"') - next_state = PLAIN; - else - next_state = STR; - } else if (state == LEFT) { + } else { + ILA_ASSERT(state == LEFT) << "Unknwon state " << state; if (c == '/') { ILA_ASSERT(ret > 0); return ret - 1; } else next_state = PLAIN; - } else - ILA_ASSERT(false); + } state = next_state; ++ret; } From 717856fb4335ba6e7246a3248434b73d19a3b7f5 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 27 Jul 2019 16:34:21 -0700 Subject: [PATCH 05/94] Remove redundant test source files --- test/t_vtarget_gen_config.cc | 0 test/t_vtarget_gen_error.cc | 0 2 files changed, 0 insertions(+), 0 deletions(-) delete mode 100644 test/t_vtarget_gen_config.cc delete mode 100644 test/t_vtarget_gen_error.cc diff --git a/test/t_vtarget_gen_config.cc b/test/t_vtarget_gen_config.cc deleted file mode 100644 index e69de29bb..000000000 diff --git a/test/t_vtarget_gen_error.cc b/test/t_vtarget_gen_error.cc deleted file mode 100644 index e69de29bb..000000000 From 9daf0db9608e4fae500263a96544308639b66d45 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 27 Jul 2019 16:34:52 -0700 Subject: [PATCH 06/94] Initialize scalar fields of Verilog target generator (#141). --- include/ilang/vtarget-out/vtarget_gen_impl.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/include/ilang/vtarget-out/vtarget_gen_impl.h b/include/ilang/vtarget-out/vtarget_gen_impl.h index afbe25546..e4ca7d5d2 100644 --- a/include/ilang/vtarget-out/vtarget_gen_impl.h +++ b/include/ilang/vtarget-out/vtarget_gen_impl.h @@ -33,9 +33,8 @@ namespace ilang { /// \brief Generating a target (just the invairant or for an instruction) class VlgSglTgtGen { - - // --------------------- TYPE DEFINITION ------------------------ // public: + // --------------------- TYPE DEFINITION ------------------------ // /// Type of the target typedef enum { INVARIANTS, INSTRUCTIONS } target_type_t; /// Type of the ready condition @@ -133,9 +132,9 @@ class VlgSglTgtGen { /// func apply counter func_app_cnt_t func_cnt; /// max bound , default 127 - unsigned max_bound; + unsigned max_bound = 127; /// the width of the counter - unsigned cnt_width; + unsigned cnt_width = 1; private: /// Counter of mapping @@ -155,6 +154,7 @@ class VlgSglTgtGen { const ExprPtr IlaGetInput(const std::string& sname) const; /// Get (a,d) width of a memory, if not existing, (0,0) std::pair + GetMemInfo(const std::string& ila_mem_name) const; /// Test if a string represents an ila state name bool TryFindIlaState(const std::string& sname); From 1cfeb2d415cd861109438616833c89831466c390 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 27 Jul 2019 23:36:12 -0700 Subject: [PATCH 07/94] Remove warning and add check at the end instead --- src/util/fs.cc | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/util/fs.cc b/src/util/fs.cc index ee1eea1de..1abf4cd3b 100644 --- a/src/util/fs.cc +++ b/src/util/fs.cc @@ -39,16 +39,9 @@ bool os_portable_mkdir(const std::string& dir) { return _mkdir(dir.c_str()) == 0; #else // on *nix - struct stat statbuff; - if (stat(dir.c_str(), &statbuff) != -1) { - if (S_ISDIR(statbuff.st_mode)) { - ILA_WARN << "Directory " << dir << " already exists."; - return true; - } - } - // return mkdir(dir.c_str(), S_IRWXU | S_IRWXG | S_IROTH | S_IXOTH) != -1; mkdir(dir.c_str(), S_IRWXU | S_IRWXG | S_IROTH | S_IXOTH); + struct stat statbuff; if (stat(dir.c_str(), &statbuff) != -1) { return S_ISDIR(statbuff.st_mode); } From 0456c8e450beddc62bc725cc30c0c7cc64fae840 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 27 Jul 2019 23:41:15 -0700 Subject: [PATCH 08/94] Initialize scalar fields in IlaSim. (#141, #142). --- include/ilang/target-sc/ila_sim.h | 72 +++++++++++++++++++------------ 1 file changed, 45 insertions(+), 27 deletions(-) diff --git a/include/ilang/target-sc/ila_sim.h b/include/ilang/target-sc/ila_sim.h index 359ee04bf..b3e76ffe3 100644 --- a/include/ilang/target-sc/ila_sim.h +++ b/include/ilang/target-sc/ila_sim.h @@ -6,9 +6,9 @@ #include #include +#include #include #include -#include #include @@ -26,21 +26,28 @@ namespace ilang { /// - ila_sim.sim_gen("./"); class IlaSim { public: + /// TODO typedef struct { std::string mem_str; std::string addr_str; std::string dest_str; } ld_info; + /// TODO typedef struct { std::string mem_str; std::string mem_map; } st_info; + /// TODO IlaSim(); + /// TODO IlaSim(const InstrLvlAbsPtr& model_ptr); + /// TODO void set_instr_lvl_abs(const InstrLvlAbsPtr& model_ptr); + /// TODO void set_systemc_path(std::string systemc_path); + /// TODO void sim_gen(std::string export_dir, bool external_mem = false, bool readable = false, bool qemu_device = false); @@ -76,27 +83,29 @@ class IlaSim { void init_check_valid(std::stringstream& init_function, std::string& indent, const ExprPtr& valid_expr, const InstrLvlAbsPtr& ila); void init_return(std::stringstream& init_function, std::string& indent); - void init_export(std::stringstream& init_function, std::string& init_func_name); + void init_export(std::stringstream& init_function, + std::string& init_func_name); void init_mk_file(std::string& init_func_name); void create_decode(const InstrPtr& instr_expr); void decode_decl(std::stringstream& decode_function, std::string& indent, std::string& decode_func_name); - void decode_check_valid(std::stringstream& decode_function, std::string& indent, - const ExprPtr& valid_expr, + void decode_check_valid(std::stringstream& decode_function, + std::string& indent, const ExprPtr& valid_expr, const InstrPtr& instr_expr); void decode_return(std::stringstream& decode_function, std::string& indent, const ExprPtr& decode_expr, const InstrPtr& instr_expr); - void decode_export(std::stringstream& decode_function, std::string& decode_func_name); + void decode_export(std::stringstream& decode_function, + std::string& decode_func_name); void decode_mk_file(std::string& decode_func_name); void create_state_update(const InstrPtr& instr_expr); - void state_update_decl(std::stringstream& state_update_function, std::string& indent, - const ExprPtr& updated_state, + void state_update_decl(std::stringstream& state_update_function, + std::string& indent, const ExprPtr& updated_state, const ExprPtr& update_expr, std::string& state_update_func_name); - void state_update_return(std::stringstream& state_update_function, std::string& indent, - const ExprPtr& updated_state, + void state_update_return(std::stringstream& state_update_function, + std::string& indent, const ExprPtr& updated_state, const ExprPtr& update_expr); void state_update_export(std::stringstream& state_update_function, std::string& state_update_func_name); @@ -107,32 +116,39 @@ class IlaSim { void execute_init(std::stringstream& execute_kernel, std::string& indent); void execute_parent_instructions(std::stringstream& execute_kernel, std::string& indent); - void execute_child_instructions(std::stringstream& execute_kernel, std::string& indent); - void execute_instruction(std::stringstream& execute_kernel, std::string& indent, - const InstrPtr& instr_expr, bool child = false); + void execute_child_instructions(std::stringstream& execute_kernel, + std::string& indent); + void execute_instruction(std::stringstream& execute_kernel, + std::string& indent, const InstrPtr& instr_expr, + bool child = false); void execute_decode(std::stringstream& execute_kernel, std::string& indent, const InstrPtr& instr_expr); - void execute_state_update_func(std::stringstream& execute_kernel, std::string& indent, + void execute_state_update_func(std::stringstream& execute_kernel, + std::string& indent, const InstrPtr& instr_expr, const ExprPtr& updated_state); - void execute_update_state(std::stringstream& execute_kernel, std::string& indent, - const InstrPtr& instr_expr, + void execute_update_state(std::stringstream& execute_kernel, + std::string& indent, const InstrPtr& instr_expr, const ExprPtr& updated_state); void execute_external_mem_load_begin(std::stringstream& execute_kernel, std::string& indent, const InstrPtr& instr_expr); void execute_external_mem_load_end(std::stringstream& execute_kernel, std::string& indent); - void execute_read_external_mem(std::stringstream& execute_kernel, std::string& indent); - void execute_write_external_mem(std::stringstream& execute_kernel, std::string& indent); + void execute_read_external_mem(std::stringstream& execute_kernel, + std::string& indent); + void execute_write_external_mem(std::stringstream& execute_kernel, + std::string& indent); void execute_external_mem_before_input(std::stringstream& execute_kernel, std::string& indent); void execute_external_mem_after_output(std::stringstream& execute_kernel, std::string& indent); void execute_external_mem_return(std::stringstream& execute_kernel, std::string& indent); - void execute_read_input(std::stringstream& execute_kernel, std::string& indent); - void execute_write_output(std::stringstream& execute_kernel, std::string& indent); + void execute_read_input(std::stringstream& execute_kernel, + std::string& indent); + void execute_write_output(std::stringstream& execute_kernel, + std::string& indent); void execute_kernel_export(std::stringstream& execute_kernel); void execute_kernel_mk_file(); void execute_kernel_header(); @@ -149,11 +165,11 @@ class IlaSim { void dfs_unary_op(std::stringstream& dfs_simulator, std::string& indent, const ExprPtr& expr); void dfs_unary_op_check(const ExprPtr& expr); - void dfs_binary_op_bool_out(std::stringstream& dfs_simulator, std::string& indent, - const ExprPtr& expr); + void dfs_binary_op_bool_out(std::stringstream& dfs_simulator, + std::string& indent, const ExprPtr& expr); void dfs_binary_op_bool_out_check(const ExprPtr& expr); - void dfs_binary_op_non_mem(std::stringstream& dfs_simulator, std::string& indent, - const ExprPtr& expr); + void dfs_binary_op_non_mem(std::stringstream& dfs_simulator, + std::string& indent, const ExprPtr& expr); void dfs_binary_op_non_mem_check(const ExprPtr& expr); void dfs_binary_op_mem(std::stringstream& dfs_simulator, std::string& indent, const ExprPtr& expr); @@ -172,7 +188,8 @@ class IlaSim { void decrease_indent(std::string& indent); int get_update_state_num(const InstrPtr& instr_expr); bool load_from_store_analysis(const ExprPtr& expr); - void declare_variable_with_id(size_t id, std::string v_type, std::string v_name); + void declare_variable_with_id(size_t id, std::string v_type, + std::string v_name); void int_var_width_scan(); std::string export_dir_; @@ -193,15 +210,16 @@ class IlaSim { std::set dfs_ld_search_set_; std::vector external_ld_set_; std::vector external_st_set_; - int ld_st_counter_; - bool EXTERNAL_MEM_; + int ld_st_counter_ = 0; + bool EXTERNAL_MEM_ = false; const int MEM_MAP_ARRAY_DIV = 16; std::set int_var_width_set_; + // Readable_ is used to control whether the generated function name is // huname-readable. When being set true, function will be named based on the // instruction name and the updated state name. However, there is a potential // same-name bug if setting true. - bool readable_; + bool readable_ = true; bool qemu_device_; InstrLvlAbsPtr model_ptr_; From cc9bcd928db5b42dc18de94fb8c807ba12ee51f1 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 27 Jul 2019 23:41:15 -0700 Subject: [PATCH 09/94] Initialize scalar fields in IlaSim. (#141, #143). --- include/ilang/target-sc/ila_sim.h | 72 +++++++++++++++++++------------ 1 file changed, 45 insertions(+), 27 deletions(-) diff --git a/include/ilang/target-sc/ila_sim.h b/include/ilang/target-sc/ila_sim.h index 359ee04bf..b3e76ffe3 100644 --- a/include/ilang/target-sc/ila_sim.h +++ b/include/ilang/target-sc/ila_sim.h @@ -6,9 +6,9 @@ #include #include +#include #include #include -#include #include @@ -26,21 +26,28 @@ namespace ilang { /// - ila_sim.sim_gen("./"); class IlaSim { public: + /// TODO typedef struct { std::string mem_str; std::string addr_str; std::string dest_str; } ld_info; + /// TODO typedef struct { std::string mem_str; std::string mem_map; } st_info; + /// TODO IlaSim(); + /// TODO IlaSim(const InstrLvlAbsPtr& model_ptr); + /// TODO void set_instr_lvl_abs(const InstrLvlAbsPtr& model_ptr); + /// TODO void set_systemc_path(std::string systemc_path); + /// TODO void sim_gen(std::string export_dir, bool external_mem = false, bool readable = false, bool qemu_device = false); @@ -76,27 +83,29 @@ class IlaSim { void init_check_valid(std::stringstream& init_function, std::string& indent, const ExprPtr& valid_expr, const InstrLvlAbsPtr& ila); void init_return(std::stringstream& init_function, std::string& indent); - void init_export(std::stringstream& init_function, std::string& init_func_name); + void init_export(std::stringstream& init_function, + std::string& init_func_name); void init_mk_file(std::string& init_func_name); void create_decode(const InstrPtr& instr_expr); void decode_decl(std::stringstream& decode_function, std::string& indent, std::string& decode_func_name); - void decode_check_valid(std::stringstream& decode_function, std::string& indent, - const ExprPtr& valid_expr, + void decode_check_valid(std::stringstream& decode_function, + std::string& indent, const ExprPtr& valid_expr, const InstrPtr& instr_expr); void decode_return(std::stringstream& decode_function, std::string& indent, const ExprPtr& decode_expr, const InstrPtr& instr_expr); - void decode_export(std::stringstream& decode_function, std::string& decode_func_name); + void decode_export(std::stringstream& decode_function, + std::string& decode_func_name); void decode_mk_file(std::string& decode_func_name); void create_state_update(const InstrPtr& instr_expr); - void state_update_decl(std::stringstream& state_update_function, std::string& indent, - const ExprPtr& updated_state, + void state_update_decl(std::stringstream& state_update_function, + std::string& indent, const ExprPtr& updated_state, const ExprPtr& update_expr, std::string& state_update_func_name); - void state_update_return(std::stringstream& state_update_function, std::string& indent, - const ExprPtr& updated_state, + void state_update_return(std::stringstream& state_update_function, + std::string& indent, const ExprPtr& updated_state, const ExprPtr& update_expr); void state_update_export(std::stringstream& state_update_function, std::string& state_update_func_name); @@ -107,32 +116,39 @@ class IlaSim { void execute_init(std::stringstream& execute_kernel, std::string& indent); void execute_parent_instructions(std::stringstream& execute_kernel, std::string& indent); - void execute_child_instructions(std::stringstream& execute_kernel, std::string& indent); - void execute_instruction(std::stringstream& execute_kernel, std::string& indent, - const InstrPtr& instr_expr, bool child = false); + void execute_child_instructions(std::stringstream& execute_kernel, + std::string& indent); + void execute_instruction(std::stringstream& execute_kernel, + std::string& indent, const InstrPtr& instr_expr, + bool child = false); void execute_decode(std::stringstream& execute_kernel, std::string& indent, const InstrPtr& instr_expr); - void execute_state_update_func(std::stringstream& execute_kernel, std::string& indent, + void execute_state_update_func(std::stringstream& execute_kernel, + std::string& indent, const InstrPtr& instr_expr, const ExprPtr& updated_state); - void execute_update_state(std::stringstream& execute_kernel, std::string& indent, - const InstrPtr& instr_expr, + void execute_update_state(std::stringstream& execute_kernel, + std::string& indent, const InstrPtr& instr_expr, const ExprPtr& updated_state); void execute_external_mem_load_begin(std::stringstream& execute_kernel, std::string& indent, const InstrPtr& instr_expr); void execute_external_mem_load_end(std::stringstream& execute_kernel, std::string& indent); - void execute_read_external_mem(std::stringstream& execute_kernel, std::string& indent); - void execute_write_external_mem(std::stringstream& execute_kernel, std::string& indent); + void execute_read_external_mem(std::stringstream& execute_kernel, + std::string& indent); + void execute_write_external_mem(std::stringstream& execute_kernel, + std::string& indent); void execute_external_mem_before_input(std::stringstream& execute_kernel, std::string& indent); void execute_external_mem_after_output(std::stringstream& execute_kernel, std::string& indent); void execute_external_mem_return(std::stringstream& execute_kernel, std::string& indent); - void execute_read_input(std::stringstream& execute_kernel, std::string& indent); - void execute_write_output(std::stringstream& execute_kernel, std::string& indent); + void execute_read_input(std::stringstream& execute_kernel, + std::string& indent); + void execute_write_output(std::stringstream& execute_kernel, + std::string& indent); void execute_kernel_export(std::stringstream& execute_kernel); void execute_kernel_mk_file(); void execute_kernel_header(); @@ -149,11 +165,11 @@ class IlaSim { void dfs_unary_op(std::stringstream& dfs_simulator, std::string& indent, const ExprPtr& expr); void dfs_unary_op_check(const ExprPtr& expr); - void dfs_binary_op_bool_out(std::stringstream& dfs_simulator, std::string& indent, - const ExprPtr& expr); + void dfs_binary_op_bool_out(std::stringstream& dfs_simulator, + std::string& indent, const ExprPtr& expr); void dfs_binary_op_bool_out_check(const ExprPtr& expr); - void dfs_binary_op_non_mem(std::stringstream& dfs_simulator, std::string& indent, - const ExprPtr& expr); + void dfs_binary_op_non_mem(std::stringstream& dfs_simulator, + std::string& indent, const ExprPtr& expr); void dfs_binary_op_non_mem_check(const ExprPtr& expr); void dfs_binary_op_mem(std::stringstream& dfs_simulator, std::string& indent, const ExprPtr& expr); @@ -172,7 +188,8 @@ class IlaSim { void decrease_indent(std::string& indent); int get_update_state_num(const InstrPtr& instr_expr); bool load_from_store_analysis(const ExprPtr& expr); - void declare_variable_with_id(size_t id, std::string v_type, std::string v_name); + void declare_variable_with_id(size_t id, std::string v_type, + std::string v_name); void int_var_width_scan(); std::string export_dir_; @@ -193,15 +210,16 @@ class IlaSim { std::set dfs_ld_search_set_; std::vector external_ld_set_; std::vector external_st_set_; - int ld_st_counter_; - bool EXTERNAL_MEM_; + int ld_st_counter_ = 0; + bool EXTERNAL_MEM_ = false; const int MEM_MAP_ARRAY_DIV = 16; std::set int_var_width_set_; + // Readable_ is used to control whether the generated function name is // huname-readable. When being set true, function will be named based on the // instruction name and the updated state name. However, there is a potential // same-name bug if setting true. - bool readable_; + bool readable_ = true; bool qemu_device_; InstrLvlAbsPtr model_ptr_; From 9b44b5ea1b67052653be933932b9a0038f4c791b Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 01:19:04 -0700 Subject: [PATCH 10/94] Setup Coverity submit branch --- .travis.yml | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 54788852d..b76707fd8 100644 --- a/.travis.yml +++ b/.travis.yml @@ -2,7 +2,7 @@ branches: only: - master - travis - - pre-release + - coverity_scan git: depth: 1 @@ -12,6 +12,11 @@ sudo: required language: cpp +env: + global: + - secure: "RwHto3MzZ2KTsGK2LiCKCxdN/xzuWiCTO+2+zhfPjVujGMx84QdMHC5fRu94VoJ5PdZ5QHwoWy3jqQ0f2PJE7oRQe28w/ENY32yDl/ziRjY1U6k4p2pcfgYQtsyyof60mL+yG6Yzz4hlJ74uQ+arhdvyAYYvliyvUiHkLgp4XvJhmsqpogkL89pERAeZ32Xg22ajzXZD5tcWQ7CbCDVKOE0KrwktU3UG08VxMmgfjKG+rU1MKj5R8rXtwZrMzqEAzosTEK0miZYJcgO0pVStCeAC2UAZllEpWXaR2EW5plb/hXRmFjRSlWflasGzJ7VB6mZ95w4xm2DICKYgcrwPWgiMnwoEByrJBh0M7xBzU1MTFmbiqB5wSSsWfVA7zv+SLmD4mCww4HKxAkE2cDJ3MOAvK8bp1vCULBCMMmbVFNGQgBprZKoxUlpQLNn+y9C6pQoaCej9/KVdkyiSQ8SM2vXDoS4/CGnoeaOAoNpu5mkPmDk7RRjIPjdS7by9xycYXAoUVVty/EZideCrYswe1KvH87GK6Fd91XITHuhuc/Aw4Jg0zXjxx6dcHbjZKuYN5MgNMx4IWK+lNiKPyLGO1/AnFG1UP+CpOC6QE8XZNhcnvn3q4r6c+v/QbeoEE7O/XOXqJDSEumJ5b2psBuoktl52azKgUqMtDzuTWjv6BvY=" + + cache: directories: - $HOME/_cache @@ -30,6 +35,15 @@ matrix: after_success: - source $TRAVIS_BUILD_DIR/scripts/travis/submit-coverage.sh $TRAVIS_BUILD_DIR/build + - name: "coverity" + os: linux + dist: xenial + compiler: gcc + 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- + before_script: + - mkdir -p $TRAVIS_BUILD_DIR/build + - name: "linux-clang" os: linux dist: xenial @@ -81,6 +95,14 @@ addons: - boost - boost-python - z3 + coverity_scan: + project: + name: "Bo-Yuan-Huang/ILAng" + description: "A modeling and verification platform for SoCs" + notification_email: byhuang1992@gmail.com + build_command_prepend: "cd $TRAVIS_BUILD_DIR && mkdir -p build && cd build && cmake .." + build_command: "make" + branch_pattern: coverity_scan script: - cd $TRAVIS_BUILD_DIR From 71f28c0e12c60c7484401f2780e61060501a64a4 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 01:45:15 -0700 Subject: [PATCH 11/94] Clean analysis for coveriy using Travis --- .travis.yml | 37 +++++++++++++++++++++++++++---------- 1 file changed, 27 insertions(+), 10 deletions(-) diff --git a/.travis.yml b/.travis.yml index b76707fd8..f6a624b85 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,5 +1,3 @@ -branches: - only: - master - travis - coverity_scan @@ -7,7 +5,6 @@ branches: git: depth: 1 submodules: false - sudo: required language: cpp @@ -40,9 +37,30 @@ matrix: dist: xenial compiler: gcc 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- + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then 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-; fi before_script: - - mkdir -p $TRAVIS_BUILD_DIR/build + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then git submodule update --init --recursive; fi + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then mkdir -p ${TRAVIS_BUILD_DIR}/build; fi + # glog + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then mkdir -p ${TRAVIS_BUILD_DIR}/extern/glog/build; fi + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cd ${TRAVIS_BUILD_DIR}/extern/glog/build; fi + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cmake ..; fi + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then sudo cmake --build . --target install; fi + # json + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then mkdir -p ${TRAVIS_BUILD_DIR}/extern/json/build; fi + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cd ${TRAVIS_BUILD_DIR}/extern/json/build; fi + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cmake ..; fi + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then sudo cmake --build . --target install; fi + # vlog-parser + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then mkdir -p ${TRAVIS_BUILD_DIR}/extern/vlog-parser/build; fi + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cd ${TRAVIS_BUILD_DIR}/extern/vlog-parser/build; fi + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cmake ..; fi + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then sudo cmake --build . --target install; fi + # tmpl-synth + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then mkdir -p ${TRAVIS_BUILD_DIR}/extern/tmpl-synth/build; fi + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cd ${TRAVIS_BUILD_DIR}/extern/tmpl-synth/build; fi + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cmake ..; fi + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then sudo cmake --build . --target install; fi - name: "linux-clang" os: linux @@ -100,7 +118,7 @@ addons: name: "Bo-Yuan-Huang/ILAng" description: "A modeling and verification platform for SoCs" notification_email: byhuang1992@gmail.com - build_command_prepend: "cd $TRAVIS_BUILD_DIR && mkdir -p build && cd build && cmake .." + build_command_prepend: "cd $TRAVIS_BUILD_DIR && mkdir -p build && cd build && cmake .. -DILANG_BUILD_TEST=OFF" build_command: "make" branch_pattern: coverity_scan @@ -109,10 +127,9 @@ script: - mkdir -p build - cd build - cmake .. -DILANG_BUILD_COV=ON -DCMAKE_BUILD_TYPE=Debug - - make -j$(nproc) - - sudo make install - - make run_test - - ctest -R ExampleCMakeBuild + - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then make -j$(nproc); fi + - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then sudo make install; fi + - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then make test; fi notifications: email: false From 93f4c00dadc5428f8642ec0c84873483a7d0e871 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 09:45:46 -0700 Subject: [PATCH 12/94] Add back accidentally removed lines --- .travis.yml | 36 ++++++------------------------- scripts/travis/build.sh | 12 +++++++++++ scripts/travis/install-externs.sh | 31 ++++++++++++++++++++++++++ 3 files changed, 49 insertions(+), 30 deletions(-) create mode 100644 scripts/travis/build.sh create mode 100644 scripts/travis/install-externs.sh diff --git a/.travis.yml b/.travis.yml index f6a624b85..2252bdb0d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,3 +1,5 @@ +branches: + only: - master - travis - coverity_scan @@ -5,6 +7,7 @@ git: depth: 1 submodules: false + sudo: required language: cpp @@ -37,30 +40,9 @@ matrix: dist: xenial compiler: gcc before_install: - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then 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-; fi + - 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- before_script: - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then git submodule update --init --recursive; fi - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then mkdir -p ${TRAVIS_BUILD_DIR}/build; fi - # glog - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then mkdir -p ${TRAVIS_BUILD_DIR}/extern/glog/build; fi - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cd ${TRAVIS_BUILD_DIR}/extern/glog/build; fi - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cmake ..; fi - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then sudo cmake --build . --target install; fi - # json - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then mkdir -p ${TRAVIS_BUILD_DIR}/extern/json/build; fi - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cd ${TRAVIS_BUILD_DIR}/extern/json/build; fi - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cmake ..; fi - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then sudo cmake --build . --target install; fi - # vlog-parser - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then mkdir -p ${TRAVIS_BUILD_DIR}/extern/vlog-parser/build; fi - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cd ${TRAVIS_BUILD_DIR}/extern/vlog-parser/build; fi - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cmake ..; fi - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then sudo cmake --build . --target install; fi - # tmpl-synth - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then mkdir -p ${TRAVIS_BUILD_DIR}/extern/tmpl-synth/build; fi - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cd ${TRAVIS_BUILD_DIR}/extern/tmpl-synth/build; fi - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then cmake ..; fi - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then sudo cmake --build . --target install; fi + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR; fi - name: "linux-clang" os: linux @@ -123,13 +105,7 @@ addons: branch_pattern: coverity_scan script: - - cd $TRAVIS_BUILD_DIR - - mkdir -p build - - cd build - - cmake .. -DILANG_BUILD_COV=ON -DCMAKE_BUILD_TYPE=Debug - - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then make -j$(nproc); fi - - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then sudo make install; fi - - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then make test; fi + - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR; fi notifications: email: false diff --git a/scripts/travis/build.sh b/scripts/travis/build.sh new file mode 100644 index 000000000..2019fcffa --- /dev/null +++ b/scripts/travis/build.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +CI_BUILD_DIR=$1 + +cd $CI_BUILD_DIR +mkdir -p build +cd build +cmake .. -DILANG_BUILD_COV=ON -DCMAKE_BUILD_TYPE=Debug +make -j$(nproc) +sudo make install +make test + diff --git a/scripts/travis/install-externs.sh b/scripts/travis/install-externs.sh new file mode 100644 index 000000000..ec662fb37 --- /dev/null +++ b/scripts/travis/install-externs.sh @@ -0,0 +1,31 @@ +#!/bin/bash + +CI_BUILD_DIR=$1 + +git submodule update --init --recursive +mkdir -p $CI_BUILD_DIR/build + +# glog +mkdir -p $CI_BUILD_DIR/extern/glog/build +cd $CI_BUILD_DIR/extern/glog/build +cmake .. +sudo cmake --build . --target install + +# json +mkdir -p $CI_BUILD_DIR/extern/json/build +cd $CI_BUILD_DIR/extern/json/build +cmake .. +sudo cmake --build . --target install + +# vlog-parser +mkdir -p $CI_BUILD_DIR/extern/vlog-parser/build +cd $CI_BUILD_DIR/extern/vlog-parser/build +cmake .. +sudo cmake --build . --target install + +# tmpl-synth +mkdir -p $CI_BUILD_DIR/extern/tmpl-synth/build +cd $CI_BUILD_DIR/extern/tmpl-synth/build +cmake .. +sudo cmake --build . --target install + From 260c29966db8f4e9df802869258eb4955ef7e507 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 10:02:48 -0700 Subject: [PATCH 13/94] Only enable coverity in one matrix --- .travis.yml | 39 ++++++++++++++++++++------------------- 1 file changed, 20 insertions(+), 19 deletions(-) diff --git a/.travis.yml b/.travis.yml index 2252bdb0d..ef81fd891 100644 --- a/.travis.yml +++ b/.travis.yml @@ -31,18 +31,9 @@ matrix: - gem install coveralls-lcov before_script: - mkdir -p $TRAVIS_BUILD_DIR/build - - source $TRAVIS_BUILD_DIR/scripts/travis/clean-coverage.sh $TRAVIS_BUILD_DIR/build + - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/clean-coverage.sh $TRAVIS_BUILD_DIR/build; fi after_success: - - source $TRAVIS_BUILD_DIR/scripts/travis/submit-coverage.sh $TRAVIS_BUILD_DIR/build - - - name: "coverity" - os: linux - dist: xenial - compiler: gcc - 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- - before_script: - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR; fi + - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/submit-coverage.sh $TRAVIS_BUILD_DIR/build; fi - name: "linux-clang" os: linux @@ -77,6 +68,24 @@ matrix: - export PATH="/usr/local/opt/bison/bin:$PATH" - export LDFLAGS="-L/usr/local/opt/bison/lib" + - name: "coverity" + os: linux + dist: xenial + compiler: gcc + addons: + coverity_scan: + project: + name: "Bo-Yuan-Huang/ILAng" + description: "A modeling and verification platform for SoCs" + notification_email: byhuang1992@gmail.com + build_command_prepend: "cd $TRAVIS_BUILD_DIR && mkdir -p build && cd build && cmake .. -DILANG_BUILD_TEST=OFF" + build_command: "make" + branch_pattern: coverity_scan + 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- + before_script: + - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR; fi + addons: apt: update: true @@ -95,14 +104,6 @@ addons: - boost - boost-python - z3 - coverity_scan: - project: - name: "Bo-Yuan-Huang/ILAng" - description: "A modeling and verification platform for SoCs" - notification_email: byhuang1992@gmail.com - build_command_prepend: "cd $TRAVIS_BUILD_DIR && mkdir -p build && cd build && cmake .. -DILANG_BUILD_TEST=OFF" - build_command: "make" - branch_pattern: coverity_scan script: - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR; fi From f9aa431a5ada4f5775289525cfbd9d44f292132b Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 10:13:10 -0700 Subject: [PATCH 14/94] Change the if condition to use the var directory --- .travis.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index ef81fd891..3b920b84c 100644 --- a/.travis.yml +++ b/.travis.yml @@ -82,9 +82,9 @@ matrix: build_command: "make" branch_pattern: coverity_scan 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- + - if [ ${COVERITY_SCAN_BRANCH} ]; then 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- ; fi before_script: - - if [ ${COVERITY_SCAN_BRANCH} == 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR; fi + - if [ ${COVERITY_SCAN_BRANCH} ]; then source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR; fi addons: apt: From 34dcea1265a6176866378f44d23539edf0430f34 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 21:28:51 -0700 Subject: [PATCH 15/94] Use single = for comparison --- .travis.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index 3b920b84c..38628cbcc 100644 --- a/.travis.yml +++ b/.travis.yml @@ -82,9 +82,9 @@ matrix: build_command: "make" branch_pattern: coverity_scan before_install: - - if [ ${COVERITY_SCAN_BRANCH} ]; then 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- ; fi + - if [ ${COVERITY_SCAN_BRANCH} = 1 ]; then 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- ; fi before_script: - - if [ ${COVERITY_SCAN_BRANCH} ]; then source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR; fi + - if [ ${COVERITY_SCAN_BRANCH} = 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR; fi addons: apt: From c7002b0e29acbc5d0f6594e30c8fcf918c4bbc3e Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 21:34:35 -0700 Subject: [PATCH 16/94] Allow installing external packages for not only coverity branch --- .travis.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index 38628cbcc..cb9e3e2c5 100644 --- a/.travis.yml +++ b/.travis.yml @@ -82,9 +82,9 @@ matrix: build_command: "make" branch_pattern: coverity_scan before_install: - - if [ ${COVERITY_SCAN_BRANCH} = 1 ]; then 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- ; fi + - 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- before_script: - - if [ ${COVERITY_SCAN_BRANCH} = 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR; fi + - source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR addons: apt: From f4c99f91b9a76b9af3cd0a2010a4d88ad7c159a6 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 21:46:06 -0700 Subject: [PATCH 17/94] Fix missing apt packages in coverity matrix --- .travis.yml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/.travis.yml b/.travis.yml index cb9e3e2c5..69a15433e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -81,6 +81,14 @@ matrix: build_command_prepend: "cd $TRAVIS_BUILD_DIR && mkdir -p build && cd build && cmake .. -DILANG_BUILD_TEST=OFF" build_command: "make" branch_pattern: coverity_scan + apt: + update: true + packages: + - flex + - bison + - libboost-all-dev + - z3 + - libz3-dev 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- before_script: From 71679eee8bb29448bb4de26ba8b0c720ef4251c4 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 21:51:54 -0700 Subject: [PATCH 18/94] Specifiy external package versions --- extern/CMakeLists.txt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/extern/CMakeLists.txt b/extern/CMakeLists.txt index 0a5afcb4d..a2ae410cc 100644 --- a/extern/CMakeLists.txt +++ b/extern/CMakeLists.txt @@ -6,7 +6,7 @@ # PATH extern/glog # ---------------------------------------------------------------------------- # # find installed package -find_package(glog QUIET) +find_package(glog 0.4.0 QUIET) # build from embeded subtree (in-source) if(NOT GLOG_FOUND) @@ -25,7 +25,7 @@ endif() # GLOG_FOUND # PATH extern/json # ---------------------------------------------------------------------------- # # find installed package -find_package(nlohmann_json QUIET) +find_package(nlohmann_json 3.6.1 QUIET) # build from embeded subtree (in-source) if(NOT NLOHMANN_JSON_FOUND) @@ -44,7 +44,7 @@ endif() # NLOHMANN_JSON_FOUND # PATH extern/vlog-parser # ---------------------------------------------------------------------------- # # find installed package -find_package(verilogparser QUIET) +find_package(verilogparser 1.1.0 QUIET) # embed to build tree if not installed if(NOT VERILOGPARSER_FOUND) @@ -80,7 +80,7 @@ endif() # VERILOGPARSER_FOUND if(${ILANG_BUILD_SYNTH}) # find installed package - find_package(ilasynth QUIET) + find_package(ilasynth 1.0 QUIET) # embed to build tree if not installed if(NOT ILASYNTH_FOUND) From ab8def81f7f335437b5d4f813eb4a3193516923f Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 21:52:48 -0700 Subject: [PATCH 19/94] Update Verilog parser to v1.1.0 --- extern/vlog-parser | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/extern/vlog-parser b/extern/vlog-parser index 544c00436..40c8b8af4 160000 --- a/extern/vlog-parser +++ b/extern/vlog-parser @@ -1 +1 @@ -Subproject commit 544c004363556a3c29c67305dc63e5aa21afa4c5 +Subproject commit 40c8b8af4a02b227410ead23497f29942432601b From 94d7bc3b6f0b2be0189e92964bdf73874a50781a Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 21:56:22 -0700 Subject: [PATCH 20/94] Uplift to sudo for installing --- .travis.yml | 2 +- scripts/travis/install-externs.sh | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/.travis.yml b/.travis.yml index 69a15433e..ab803e31d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -92,7 +92,7 @@ matrix: 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- before_script: - - source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR + - sudo source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR addons: apt: diff --git a/scripts/travis/install-externs.sh b/scripts/travis/install-externs.sh index ec662fb37..97f8088bc 100644 --- a/scripts/travis/install-externs.sh +++ b/scripts/travis/install-externs.sh @@ -9,23 +9,23 @@ mkdir -p $CI_BUILD_DIR/build mkdir -p $CI_BUILD_DIR/extern/glog/build cd $CI_BUILD_DIR/extern/glog/build cmake .. -sudo cmake --build . --target install +cmake --build . --target install # json mkdir -p $CI_BUILD_DIR/extern/json/build cd $CI_BUILD_DIR/extern/json/build cmake .. -sudo cmake --build . --target install +cmake --build . --target install # vlog-parser mkdir -p $CI_BUILD_DIR/extern/vlog-parser/build cd $CI_BUILD_DIR/extern/vlog-parser/build cmake .. -sudo cmake --build . --target install +cmake --build . --target install # tmpl-synth mkdir -p $CI_BUILD_DIR/extern/tmpl-synth/build cd $CI_BUILD_DIR/extern/tmpl-synth/build cmake .. -sudo cmake --build . --target install +cmake --build . --target install From 7bb4e3e92822f584dbed60cc9a5330d29d6dfdd9 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 22:05:44 -0700 Subject: [PATCH 21/94] Specify sudo runnign shell --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index ab803e31d..e49bf93f5 100644 --- a/.travis.yml +++ b/.travis.yml @@ -92,7 +92,7 @@ matrix: 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- before_script: - - sudo source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR + - sudo -s source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR addons: apt: From ee9c8a34c558db82d8c79f892b556aab0142480c Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 22:14:00 -0700 Subject: [PATCH 22/94] Avoid using sudo... --- .travis.yml | 4 ++-- scripts/travis/install-externs.sh | 11 +++++------ 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/.travis.yml b/.travis.yml index e49bf93f5..53543dd26 100644 --- a/.travis.yml +++ b/.travis.yml @@ -78,7 +78,7 @@ matrix: name: "Bo-Yuan-Huang/ILAng" description: "A modeling and verification platform for SoCs" notification_email: byhuang1992@gmail.com - build_command_prepend: "cd $TRAVIS_BUILD_DIR && mkdir -p build && cd build && cmake .. -DILANG_BUILD_TEST=OFF" + build_command_prepend: "cd $TRAVIS_BUILD_DIR && mkdir -p build && cd build && cmake .. -DILANG_BUILD_TEST=OFF -DCMAKE_PREFIX_PATH=$TRAVIS_BUILD_DIR/local" build_command: "make" branch_pattern: coverity_scan apt: @@ -92,7 +92,7 @@ matrix: 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- before_script: - - sudo -s source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR + - source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR addons: apt: diff --git a/scripts/travis/install-externs.sh b/scripts/travis/install-externs.sh index 97f8088bc..642a8c23a 100644 --- a/scripts/travis/install-externs.sh +++ b/scripts/travis/install-externs.sh @@ -3,29 +3,28 @@ CI_BUILD_DIR=$1 git submodule update --init --recursive -mkdir -p $CI_BUILD_DIR/build +mkdir -p $CI_BUILD_DIR/local # glog mkdir -p $CI_BUILD_DIR/extern/glog/build cd $CI_BUILD_DIR/extern/glog/build -cmake .. +cmake .. -DCMAKE_INSTALL_PREFIX=$CI_BUILD_DIR/local cmake --build . --target install # json mkdir -p $CI_BUILD_DIR/extern/json/build cd $CI_BUILD_DIR/extern/json/build -cmake .. +cmake .. -DCMAKE_INSTALL_PREFIX=$CI_BUILD_DIR/local cmake --build . --target install # vlog-parser mkdir -p $CI_BUILD_DIR/extern/vlog-parser/build cd $CI_BUILD_DIR/extern/vlog-parser/build -cmake .. +cmake .. -DCMAKE_INSTALL_PREFIX=$CI_BUILD_DIR/local cmake --build . --target install # tmpl-synth mkdir -p $CI_BUILD_DIR/extern/tmpl-synth/build cd $CI_BUILD_DIR/extern/tmpl-synth/build -cmake .. +cmake .. -DCMAKE_INSTALL_PREFIX=$CI_BUILD_DIR/local cmake --build . --target install - From b24b69db2817f87d6d02fc5d0f222b7135caead8 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 22:30:13 -0700 Subject: [PATCH 23/94] Cleanup headers - ila --- include/ilang/ila/ast/ast.h | 12 +++++------- include/ilang/ila/ast/expr.h | 17 +++++++++-------- include/ilang/ila/ast/expr_const.h | 6 +++--- include/ilang/ila/ast/expr_op.h | 6 +++--- include/ilang/ila/ast/expr_var.h | 9 +++++---- include/ilang/ila/ast/func.h | 6 +++--- include/ilang/ila/ast/sort.h | 11 ++++++----- include/ilang/ila/ast/sort_value.h | 6 +++--- include/ilang/ila/comp_ref_rel.h | 6 +++--- include/ilang/ila/defines.h | 11 ++++++----- include/ilang/ila/expr_fuse.h | 9 +++++---- include/ilang/ila/hash_ast.h | 9 +++++---- include/ilang/ila/instr.h | 11 ++++++----- include/ilang/ila/instr_lvl_abs.h | 17 +++++++++-------- include/ilang/ila/object.h | 9 +++++---- include/ilang/ila/symbol.h | 8 +++----- include/ilang/ila/transition.h | 6 +++--- include/ilang/ila/validate_model.h | 6 ++++-- include/ilang/ila/z3_expr_adapter.h | 9 +++++---- 19 files changed, 91 insertions(+), 83 deletions(-) diff --git a/include/ilang/ila/ast/ast.h b/include/ilang/ila/ast/ast.h index d947b98ea..b3abac80d 100644 --- a/include/ilang/ila/ast/ast.h +++ b/include/ilang/ila/ast/ast.h @@ -1,14 +1,14 @@ /// \file /// Header for the class Ast. -#ifndef AST_H__ -#define AST_H__ +#ifndef ILANG_ILA_AST_AST_H__ +#define ILANG_ILA_AST_AST_H__ -#include "z3++.h" -#include #include #include +#include + /// \namespace ilang namespace ilang { @@ -54,10 +54,8 @@ class Ast : public Object { /// Pointer to the host ILA. InstrLvlAbsPtr host_ = NULL; - // ------------------------- HELPERS -------------------------------------- // - }; // class Ast } // namespace ilang -#endif // AST_H__ +#endif // ILANG_ILA_AST_AST_H__ diff --git a/include/ilang/ila/ast/expr.h b/include/ilang/ila/ast/expr.h index 4a0008743..165fbbbd1 100644 --- a/include/ilang/ila/ast/expr.h +++ b/include/ilang/ila/ast/expr.h @@ -1,14 +1,9 @@ /// \file /// Header for the class Expr -#ifndef EXPR_H__ -#define EXPR_H__ +#ifndef ILANG_ILA_AST_EXPR_H__ +#define ILANG_ILA_AST_EXPR_H__ -#include "z3++.h" -#include "z3_api.h" -#include -#include -#include #include #include #include @@ -16,6 +11,12 @@ #include #include +#include "z3++.h" +#include "z3_api.h" +#include +#include +#include + /// \namespace ilang namespace ilang { @@ -148,4 +149,4 @@ typedef std::unordered_set ExprSet; } // namespace ilang -#endif // EXPR_H__ +#endif // ILANG_ILA_AST_EXPR_H__ diff --git a/include/ilang/ila/ast/expr_const.h b/include/ilang/ila/ast/expr_const.h index 5acb28f4d..82826c233 100644 --- a/include/ilang/ila/ast/expr_const.h +++ b/include/ilang/ila/ast/expr_const.h @@ -1,8 +1,8 @@ /// \file /// Header for constant expression -#ifndef EXPR_CONST_H__ -#define EXPR_CONST_H__ +#ifndef ILANG_ILA_AST_EXPR_CONST_H__ +#define ILANG_ILA_AST_EXPR_CONST_H__ #include #include @@ -53,4 +53,4 @@ class ExprConst : public Expr { } // namespace ilang -#endif // EXPR_CONST_H__ +#endif // ILANG_ILA_AST_EXPR_CONST_H__ diff --git a/include/ilang/ila/ast/expr_op.h b/include/ilang/ila/ast/expr_op.h index 264b0709a..d604bf4d5 100644 --- a/include/ilang/ila/ast/expr_op.h +++ b/include/ilang/ila/ast/expr_op.h @@ -1,8 +1,8 @@ /// \file /// Header for the class ExprOp -#ifndef EXPR_OP_H__ -#define EXPR_OP_H__ +#ifndef ILANG_ILA_AST_EXPR_OP_H__ +#define ILANG_ILA_AST_EXPR_OP_H__ #include @@ -432,4 +432,4 @@ class ExprOpIte : public ExprOp { } // namespace ilang -#endif // EXPR_OP_H__ +#endif // ILANG_ILA_AST_EXPR_OP_H__ diff --git a/include/ilang/ila/ast/expr_var.h b/include/ilang/ila/ast/expr_var.h index 6521a1e8c..38e4331cc 100644 --- a/include/ilang/ila/ast/expr_var.h +++ b/include/ilang/ila/ast/expr_var.h @@ -1,12 +1,13 @@ /// \file /// Header for the class ExprVar -#ifndef EXPR_VAR_H__ -#define EXPR_VAR_H__ +#ifndef ILANG_ILA_AST_EXPR_VAR_H__ +#define ILANG_ILA_AST_EXPR_VAR_H__ -#include #include +#include + /// \namespace ilang namespace ilang { @@ -54,4 +55,4 @@ class ExprVar : public Expr { } // namespace ilang -#endif // EXPR_VAR_H__ +#endif // ILANG_ILA_AST_EXPR_VAR_H__ diff --git a/include/ilang/ila/ast/func.h b/include/ilang/ila/ast/func.h index 534136f03..0ab2eb367 100644 --- a/include/ilang/ila/ast/func.h +++ b/include/ilang/ila/ast/func.h @@ -1,8 +1,8 @@ /// \file /// Header for the class Func (uninterpreted function). -#ifndef FUNC_H__ -#define FUNC_H__ +#ifndef ILANG_ILA_AST_FUNC_H__ +#define ILANG_ILA_AST_FUNC_H__ #include "z3++.h" #include @@ -80,4 +80,4 @@ typedef Func::FuncPtr FuncPtr; } // namespace ilang -#endif // FUNC_H__ +#endif // ILANG_ILA_AST_FUNC_H__ diff --git a/include/ilang/ila/ast/sort.h b/include/ilang/ila/ast/sort.h index 0ab27bbd1..422207930 100644 --- a/include/ilang/ila/ast/sort.h +++ b/include/ilang/ila/ast/sort.h @@ -1,14 +1,15 @@ /// \file /// Header for the class Sort -#ifndef SORT_H__ -#define SORT_H__ +#ifndef ILANG_ILA_AST_SORT_H__ +#define ILANG_ILA_AST_SORT_H__ -#include "z3++.h" -#include #include #include +#include "z3++.h" +#include + /// \namespace ilang namespace ilang { @@ -166,4 +167,4 @@ class SortMem : public Sort { } // namespace ilang -#endif // SORT_H__ +#endif // ILANG_ILA_AST_SORT_H__ diff --git a/include/ilang/ila/ast/sort_value.h b/include/ilang/ila/ast/sort_value.h index 82cff3dde..696ea8f44 100644 --- a/include/ilang/ila/ast/sort_value.h +++ b/include/ilang/ila/ast/sort_value.h @@ -1,8 +1,8 @@ /// \file /// Header for the class BoolVal, BvVal, and MemVal -#ifndef SORT_VALUE_H__ -#define SORT_VALUE_H__ +#ifndef ILANG_ILA_AST_SORT_VALUE_H__ +#define ILANG_ILA_AST_SORT_VALUE_H__ #include #include @@ -152,4 +152,4 @@ typedef MemVal::MemValMap MemValMap; } // namespace ilang -#endif // SORT_VALUE_H__ +#endif // ILANG_ILA_AST_SORT_VALUE_H__ diff --git a/include/ilang/ila/comp_ref_rel.h b/include/ilang/ila/comp_ref_rel.h index 3ef42bb39..94974a2e2 100644 --- a/include/ilang/ila/comp_ref_rel.h +++ b/include/ilang/ila/comp_ref_rel.h @@ -1,8 +1,8 @@ /// \file /// Header for the refinement relation -#ifndef COMP_REF_REL_H__ -#define COMP_REF_REL_H__ +#ifndef ILANG_ILA_COMP_REF_REL_H__ +#define ILANG_ILA_COMP_REF_REL_H__ #include @@ -174,4 +174,4 @@ typedef CompRefRel::CrrPtr CrrPtr; } // namespace ilang -#endif // COMP_REF_REL_H__ +#endif // ILANG_ILA_COMP_REF_REL_H__ diff --git a/include/ilang/ila/defines.h b/include/ilang/ila/defines.h index 10ed87a0d..dd22cff8f 100644 --- a/include/ilang/ila/defines.h +++ b/include/ilang/ila/defines.h @@ -1,14 +1,15 @@ /// \file /// Headers for macros, type definitions, etc. -#ifndef DEFINES_H__ -#define DEFINES_H__ +#ifndef ILANG_ILA_DEFINES_H__ +#define ILANG_ILA_DEFINES_H__ + +#include +#include #include "z3++.h" #include #include -#include -#include /// \namespace ilang namespace ilang { @@ -24,4 +25,4 @@ typedef std::shared_ptr Z3ExprMapPtr; } // namespace ilang -#endif // DEFINES_H__ +#endif // ILANG_ILA_DEFINES_H__ diff --git a/include/ilang/ila/expr_fuse.h b/include/ilang/ila/expr_fuse.h index 462f01c5b..f6ec4bc54 100644 --- a/include/ilang/ila/expr_fuse.h +++ b/include/ilang/ila/expr_fuse.h @@ -1,15 +1,16 @@ /// \file /// Header of the wrapping Expr usage -#ifndef EXPR_FUSE_H__ -#define EXPR_FUSE_H__ +#ifndef ILANG_ILA_EXPR_FUSE_H__ +#define ILANG_ILA_EXPR_FUSE_H__ + +#include #include #include #include #include #include -#include /// \namespace ilang namespace ilang { @@ -221,4 +222,4 @@ bool TopEq(const ExprPtr a, const ExprPtr b); } // namespace ilang -#endif // EXPR_FUSE_H__ +#endif // ILANG_ILA_EXPR_FUSE_H__ diff --git a/include/ilang/ila/hash_ast.h b/include/ilang/ila/hash_ast.h index 7796ecc62..b562ddf22 100644 --- a/include/ilang/ila/hash_ast.h +++ b/include/ilang/ila/hash_ast.h @@ -1,12 +1,13 @@ /// \file /// Header for the class ExprMngr and the corresponding hash -#ifndef AST_HASH_H__ -#define AST_HASH_H__ +#ifndef ILANG_ILA_HASH_AST_H__ +#define ILANG_ILA_HASH_AST_H__ -#include #include +#include + /// \namespace ilang namespace ilang { @@ -55,4 +56,4 @@ typedef ExprMngr::ExprMngrPtr ExprMngrPtr; } // namespace ilang -#endif // HASH_AST_H__ +#endif // ILANG_ILA_HASH_AST_H__ diff --git a/include/ilang/ila/instr.h b/include/ilang/ila/instr.h index 98f0c6583..976f543dc 100644 --- a/include/ilang/ila/instr.h +++ b/include/ilang/ila/instr.h @@ -1,14 +1,15 @@ /// \file /// The header for the class Instr. -#ifndef INSTR_H__ -#define INSTR_H__ +#ifndef ILANG_ILA_INSTR_H__ +#define ILANG_ILA_INSTR_H__ + +#include +#include #include #include #include -#include -#include /// \namespace ilang namespace ilang { @@ -138,4 +139,4 @@ typedef std::vector InstrVec; } // namespace ilang -#endif // INSTR_H__ +#endif // ILNAG_ILA_INSTR_H__ diff --git a/include/ilang/ila/instr_lvl_abs.h b/include/ilang/ila/instr_lvl_abs.h index 42ac2aeef..4f1cfd3ab 100644 --- a/include/ilang/ila/instr_lvl_abs.h +++ b/include/ilang/ila/instr_lvl_abs.h @@ -1,8 +1,14 @@ /// \file /// The header for the class InstrLvlAbs. -#ifndef INSTR_LVL_ABS_H__ -#define INSTR_LVL_ABS_H__ +#ifndef ILANG_ILA_INSTR_LVL_ABS_H__ +#define ILANG_ILA_INSTR_LVL_ABS_H__ + +#include +#include +#include +#include +#include #include #include @@ -11,11 +17,6 @@ #include #include #include -#include -#include -#include -#include -#include /// \namespace ilang namespace ilang { @@ -330,4 +331,4 @@ typedef std::map CnstIlaMap; } // namespace ilang -#endif // INSTR_LVL_ABS_H__ +#endif // ILANG_ILA_INSTR_LVL_ABS_H__ diff --git a/include/ilang/ila/object.h b/include/ilang/ila/object.h index 0d19426e0..f7c2f8c66 100644 --- a/include/ilang/ila/object.h +++ b/include/ilang/ila/object.h @@ -1,13 +1,14 @@ /// \file /// The header for the class Object. -#ifndef OBJECT_H__ -#define OBJECT_H__ +#ifndef ILANG_ILA_OBJECT_H__ +#define ILANG_ILA_OBJECT_H__ -#include #include #include +#include + /// \namespace ilang namespace ilang { @@ -55,4 +56,4 @@ typedef Object::ObjPtr ObjPtr; } // namespace ilang -#endif // OBJECT_H__ +#endif // ILANG_ILA_OBJECT_H__ diff --git a/include/ilang/ila/symbol.h b/include/ilang/ila/symbol.h index f886b57b0..b8aa3ca04 100644 --- a/include/ilang/ila/symbol.h +++ b/include/ilang/ila/symbol.h @@ -1,8 +1,8 @@ /// \file /// The header for the class Symbol. -#ifndef SYMBOL_H__ -#define SYMBOL_H__ +#ifndef ILANG_ILA_SYMBOL_H__ +#define ILANG_ILA_SYMBOL_H__ #include #include @@ -65,10 +65,8 @@ class Symbol { /// Static counter for symbols IDs. static size_t counter_; - // ------------------------- HELPERS -------------------------------------- // - }; // class Symbol } // namespace ilang -#endif // SYMBOL_H__ +#endif // ILANG_ILA_SYMBOL_H__ diff --git a/include/ilang/ila/transition.h b/include/ilang/ila/transition.h index f47309ae5..a3ec00335 100644 --- a/include/ilang/ila/transition.h +++ b/include/ilang/ila/transition.h @@ -1,8 +1,8 @@ /// \file /// Header for the class InstrTran, InstrTranGraph, and InstrSeq -#ifndef INSTR_TRAN_H__ -#define INSTR_TRAN_H__ +#ifndef ILANG_ILA_TRANSITION_H__ +#define ILANG_ILA_TRANSITION_H__ #include #include @@ -148,4 +148,4 @@ typedef InstrSeq::InstrSeqPtr InstrSeqPtr; } // namespace ilang -#endif // INSTR_TRAN_H__ +#endif // ILANG_ILA_TRANSITION_H__ diff --git a/include/ilang/ila/validate_model.h b/include/ilang/ila/validate_model.h index b2bcdfa40..b9b68eb24 100644 --- a/include/ilang/ila/validate_model.h +++ b/include/ilang/ila/validate_model.h @@ -17,13 +17,15 @@ enum DEFAULT_UPDATE_METHOD { OLD_VALUE = 0, NONDET_VALUE = 1 }; /// Check whether the model (pointed by model_ptr_) is deterministic. /// Determinism means no more than one instruction can be decoded truth. bool CheckDeterminism(const InstrLvlAbsPtr& model_ptr_); + /// Check whether the model (pointed by model_ptr_) is complete. /// Completeness means every assignment to input and state corresponds an /// instruction. bool CheckCompleteness(const InstrLvlAbsPtr& model_ptr_); + /// Use a default update method to complete model. -void CompleteModel(const InstrLvlAbsPtr& model_ptr_, - DEFAULT_UPDATE_METHOD dum); +void CompleteModel(const InstrLvlAbsPtr& model_ptr_, DEFAULT_UPDATE_METHOD dum); + } // namespace ilang #endif // ILANG_ILA_VALIDATE_MODEL_H__ diff --git a/include/ilang/ila/z3_expr_adapter.h b/include/ilang/ila/z3_expr_adapter.h index 219e4de43..f25d831b2 100644 --- a/include/ilang/ila/z3_expr_adapter.h +++ b/include/ilang/ila/z3_expr_adapter.h @@ -1,12 +1,13 @@ /// \file /// Header for the class Z3ExprAdapter -#ifndef Z3_EXPR_ADAPTER_H__ -#define Z3_EXPR_ADAPTER_H__ +#ifndef ILANG_ILA_Z3_EXPR_ADAPTER_H__ +#define ILANG_ILA_Z3_EXPR_ADAPTER_H__ + +#include #include "z3++.h" #include -#include /// \namespace ilang namespace ilang { @@ -50,4 +51,4 @@ class Z3ExprAdapter { } // namespace ilang -#endif // Z3_EXPR_ADAPTER_H__ +#endif // ILANG_ILA_Z3_EXPR_ADAPTER_H__ From 9349c015a0deaee498b8994135e361866bd0daa0 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 22:35:01 -0700 Subject: [PATCH 24/94] Remove legacy code for Python API --- include/ilang/python-api/ila_py_api.h | 24 -------------- include/ilang/python-api/wrap_expr.h | 45 --------------------------- include/ilang/python-api/wrap_ila.h | 38 ---------------------- include/ilang/python-api/wrap_log.h | 19 ----------- 4 files changed, 126 deletions(-) delete mode 100644 include/ilang/python-api/ila_py_api.h delete mode 100644 include/ilang/python-api/wrap_expr.h delete mode 100644 include/ilang/python-api/wrap_ila.h delete mode 100644 include/ilang/python-api/wrap_log.h diff --git a/include/ilang/python-api/ila_py_api.h b/include/ilang/python-api/ila_py_api.h deleted file mode 100644 index 7c7b51c77..000000000 --- a/include/ilang/python-api/ila_py_api.h +++ /dev/null @@ -1,24 +0,0 @@ -/// \file -/// Header for Python API -- top level for all tools - -#ifndef ILA_PY_API_H__ -#define ILA_PY_API_H__ - -#include - -namespace ilang { -namespace pyapi { -using namespace boost::python; - -void export_log(); - -void export_expr(); - -void export_instr(); - -void export_instr_lvl_abs(); - -} // namespace pyapi -} // namespace ilang - -#endif // ILA_PY_API_H__ diff --git a/include/ilang/python-api/wrap_expr.h b/include/ilang/python-api/wrap_expr.h deleted file mode 100644 index 477ab6771..000000000 --- a/include/ilang/python-api/wrap_expr.h +++ /dev/null @@ -1,45 +0,0 @@ -/// \file -/// Header for wrapping Expr. - -#ifndef WRAP_EXPR_H__ -#define WRAP_EXPR_H__ - -#include - -namespace ilang { -namespace pyapi { - -/// \brief The Expr wrapper for Boost.Python API. -class ExprWrap { - // ------------------------- MEMBERS -------------------------------------- // - /// Wrapped data. - ExprPtr ptr_; - -public: - // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // - /// Default constructor for Boost.Python wrapper. - ExprWrap() : ptr_(NULL) {} - /// Constructor for copying from C++ API. - ExprWrap(const ExprPtr e) : ptr_(e) {} - - // ------------------------- ACCESSORS/MUTATORS --------------------------- // - const ExprPtr get() const; - - // ------------------------- METHODS -------------------------------------- // - std::string Name() const; - - ExprWrap* Complement() const; - - ExprWrap* Negate() const; - - ExprWrap* And(ExprWrap* rhs) const; - - // ------------------------- STATIC METHODS ------------------------------- // - static ExprWrap* Load(ExprWrap* mem, ExprWrap* addr); - -}; // class ExprWrap - -} // namespace pyapi -} // namespace ilang - -#endif // WRAP_EXPR_H__ diff --git a/include/ilang/python-api/wrap_ila.h b/include/ilang/python-api/wrap_ila.h deleted file mode 100644 index 9047f282f..000000000 --- a/include/ilang/python-api/wrap_ila.h +++ /dev/null @@ -1,38 +0,0 @@ -/// \file -/// Header for wrapping the ila. - -#ifndef WRAP_INSTR_LVL_ABS_H__ -#define WRAP_INSTR_LVL_ABS_H__ - -#include -#include - -namespace ilang { -namespace pyapi { - -/// \brief The wrapper class for InstrLvlAbs -class InstrLvlAbsWrap { - // ------------------------- MEMBERS -------------------------------------- // - /// Wrapped data. - InstrLvlAbsPtr ptr_; - -public: - // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // - /// Constructor for Boost.Python API. - InstrLvlAbsWrap(const std::string& name) : ptr_(InstrLvlAbs::New(name)) {} - - // ------------------------- ACCESSORS/MUTATORS --------------------------- // - - // ------------------------- METHODS -------------------------------------- // - /// Create new bitvector input. - ExprWrap* NewBvInput(const std::string& name, const int& bit_width); - /// Get the input with name. - ExprWrap* input(const std::string& name); - /// TODO - -}; // class InstrLvlAbsWrap - -} // namespace pyapi -} // namespace ilang - -#endif // WRAP_INSTR_LVL_ABS_H__ diff --git a/include/ilang/python-api/wrap_log.h b/include/ilang/python-api/wrap_log.h deleted file mode 100644 index 07e74e42a..000000000 --- a/include/ilang/python-api/wrap_log.h +++ /dev/null @@ -1,19 +0,0 @@ -/// \file -/// Header for wrapping the logging system. - -#ifndef WRAP_LOG_H__ -#define WRAP_LOG_H__ - -namespace ilang { -namespace pyapi { - -void EnableLog(const std::string& tag); - -void DisableLog(const std::string& tag); - -void ClearLogs(); - -} // namespace pyapi -} // namespace ilang - -#endif // WRAP_LOG_H__ From db05da3a979a9c5675fc9ddd05e346859b11e175 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 22:38:35 -0700 Subject: [PATCH 25/94] Cleanup headers - util --- include/ilang/util/container.h | 6 +++--- include/ilang/util/container_shortcut.h | 6 +++--- include/ilang/util/fs.h | 6 +++--- include/ilang/util/str_util.h | 15 +++------------ 4 files changed, 12 insertions(+), 21 deletions(-) diff --git a/include/ilang/util/container.h b/include/ilang/util/container.h index 4930b95e0..fe432f0a6 100644 --- a/include/ilang/util/container.h +++ b/include/ilang/util/container.h @@ -1,8 +1,8 @@ /// \file /// Header for containers, e.g. KeyVec. -#ifndef CONTAINER_H__ -#define CONTAINER_H__ +#ifndef ILANG_UTIL_CONTAINER_H__ +#define ILANG_UTIL_CONTAINER_H__ #include #include @@ -155,4 +155,4 @@ template class MapSet { } // namespace ilang -#endif // CONTAINER_H__ +#endif // ILANG_UTIL_CONTAINER_H__ diff --git a/include/ilang/util/container_shortcut.h b/include/ilang/util/container_shortcut.h index 221ebabf4..f45b4f979 100644 --- a/include/ilang/util/container_shortcut.h +++ b/include/ilang/util/container_shortcut.h @@ -1,8 +1,8 @@ /// \file /// Some short cut for set operations -#ifndef CONTAINER_SHORTCUT_H__ -#define CONTAINER_SHORTCUT_H__ +#ifndef ILANG_UTIL_CONTAINER_SHORTCUT_H__ +#define ILANG_UTIL_CONTAINER_SHORTCUT_H__ #include #include @@ -26,4 +26,4 @@ #define S_IN(sub, s) (s.find(sub) != s.npos) -#endif // CONTAINER_SHORTCUT_H__ +#endif // ILANG_UTIL_CONTAINER_SHORTCUT_H__ diff --git a/include/ilang/util/fs.h b/include/ilang/util/fs.h index c53da7437..33778d7d5 100644 --- a/include/ilang/util/fs.h +++ b/include/ilang/util/fs.h @@ -5,8 +5,8 @@ /// experimental/filesystem, but we don't rely on it // --- Hongce Zhang -#ifndef FS_H__ -#define FS_H__ +#ifndef ILANG_UTIL_FS_H__ +#define ILANG_UTIL_FS_H__ #include @@ -33,4 +33,4 @@ std::string os_portable_file_name_from_path(const std::string& path); }; // namespace ilang -#endif // FS_H__ +#endif // ILANG_UTIL_FS_H__ diff --git a/include/ilang/util/str_util.h b/include/ilang/util/str_util.h index 68e18320f..2f7310b64 100644 --- a/include/ilang/util/str_util.h +++ b/include/ilang/util/str_util.h @@ -1,8 +1,8 @@ /// \file /// Header for some utily functions for string formating. -#ifndef STR_UTIL_H__ -#define STR_UTIL_H__ +#ifndef ILANG_UTIL_STR_UTIL_H__ +#define ILANG_UTIL_STR_UTIL_H__ #include #include @@ -50,15 +50,6 @@ std::vector ReFindAndDo(const std::string& s, bool IsRExprUsable(); -#if 0 -/// Concatenate two string with "_". -std::string StrConcat(const std::string& l, const std::string& r); - -/// Concatenate three string with "_". -std::string StrConcat(const std::string& l, const std::string& m, - const std::string& r); -#endif - } // namespace ilang -#endif // STR_UTIL_H__ +#endif // ILANG_UTIL_STR_UTIL_H__ From 9b0c47157ceb28366fafffac5ac50f1630dcae15 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 28 Jul 2019 23:51:13 -0700 Subject: [PATCH 26/94] Cleanup headers - mcm --- include/ilang/mcm/ast_helper.h | 82 +++++++++++++++----------- include/ilang/mcm/axiom_helper.h | 6 +- include/ilang/mcm/inter_ila_unroller.h | 15 ++--- include/ilang/mcm/sc_manual.h | 6 +- include/ilang/mcm/set_op.h | 6 +- include/ilang/mcm/tso_manual.h | 6 +- 6 files changed, 66 insertions(+), 55 deletions(-) diff --git a/include/ilang/mcm/ast_helper.h b/include/ilang/mcm/ast_helper.h index 52fe17b98..d37301ba4 100644 --- a/include/ilang/mcm/ast_helper.h +++ b/include/ilang/mcm/ast_helper.h @@ -1,16 +1,16 @@ /// \file /// Header for AST helpers (some helper classes to handle AST) -#ifndef AST_HELPER_H__ -#define AST_HELPER_H__ - -#include "ilang/ila/instr_lvl_abs.h" +#ifndef ILANG_MCM_AST_HELPER_H__ +#define ILANG_MCM_AST_HELPER_H__ #include #include #include #include +#include "ilang/ila/instr_lvl_abs.h" + /// \namespace ilang namespace ilang { @@ -87,78 +87,88 @@ class FunctionApplicationFinder { const std::set> GetReferredFunc() const; }; // class FunctionApplicationFinder -/* +#if 0 /// \brief Class of traversing to detect nested store class PureNestedStoreDetector { /// Type of vector of (address, data) pair - typedef std::vector > AddrDataVec; // (addr,data) -list + typedef std::vector> + AddrDataVec; // (addr,data) list + /// Type of map, from points of expression to the pair collected so far for -the sub tree typedef std::unordered_map HashTable; // here -we do use the raw pointer public: + /// the sub tree + typedef std::unordered_map + HashTable; // here we do use the raw pointer public: + // ------------------------- METHODS -------------------------------------- // /// \brief To decide if a expr contains nested store or not - bool isNestedStore(const ExprPtr &); + bool isNestedStore(const ExprPtr&); /// \brief Get the address/data pair of a given expr ptr - const AddrDataVec & getStoreAddrDataVec(const ExprPtr &); + const AddrDataVec& getStoreAddrDataVec(const ExprPtr&); + private: // ------------------------- MEMBERS -------------------------------------- // // a map HashTable map_; } -*/ +#endif -/* +#if 0 struct MRF_HASH_FUNC { - std::size_t operator() (const std::pair & p) const { + std::size_t operator()(const std::pair& p) const { return std::hash()(p.first) ^ std::hash()(p.second); } }; -*/ +#endif -/* +#if 0 /// \brief class MemReadFinder(MRF) to find (only find) the address and data -part that exists in a trace step? class MemReadFinder { public: +part that exists in a trace step ? class MemReadFinder { +public: // Type of (addr,data) pair list - typedef std::vector > AddrDataVec; + typedef std::vector> AddrDataVec; + private: /// Type of the Hash Key - typedef Instr * MRFHashKey; // typedef std::pair< TraceStep *, Expr * > -MRFHashKey; + typedef Instr* + MRFHashKey; // typedef std::pair< TraceStep *, Expr * > MRFHashKey; /// Type of the dictionary value - typedef std::unordered_map MRFVal; // statename -> -(addr,data) list + typedef std::unordered_map + MRFVal; // statename -> (addr,data) list /// Type for caching the result of the search: Instr * -> (statename -> -(addr,data) list ), for a instruction, for a given state, what are the addr/data -that is read typedef std::unordered_map MRFHashTable; + /// (addr,data) list ), for a instruction, for a given state, what are the + /// addr/data that is read + typedef std::unordered_map MRFHashTable; + private: // ------------------------- MEMBERS -------------------------------------- // /// A wrapper of calling DepthFirstVisit with a function object - void FindAddrDataPairVecInExpr(const ExprPtr &node, MRFVal & nad_map_); + void FindAddrDataPairVecInExpr(const ExprPtr& node, MRFVal& nad_map_); /// a private function to be called to handle a node. The traversal is -original in the Expr (template member function: DepthFirstVisit) void -VisitNode(const ExprPtr &node, MRFVal & nad_map_); public: + /// original in the Expr (template member function: DepthFirstVisit) + void VisitNode(const ExprPtr& node, MRFVal& nad_map_); + +public: /// for an instruction, for a state, return the reference to the (addr,data) -pair list - /// it has no way to check if sname is memvar or not, so it needs to be -guaranteed that it is a memver's name const AddrDataVec & -FindAddrDataPairVecInInst(const InstrPtr &instr, const std::string &sname); + /// pair list it has no way to check if sname is memvar or not, so it needs to + /// be guaranteed that it is a memver's name + const AddrDataVec& FindAddrDataPairVecInInst(const InstrPtr& instr, + const std::string& sname); // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // /// Constructor, it needs a NestedMemAddrDataAvoider reference (so we can -share among different MemReadFinder) MemReadFinder(NestedMemAddrDataAvoider & n) -: nested_finder_(n) {} + /// share among different MemReadFinder) + MemReadFinder(NestedMemAddrDataAvoider& n) : nested_finder_(n) {} private: // ------------------------- MEMBERS -------------------------------------- // /// The table to cache the results MRFHashTable map_; /// reference to the shared nested avoider - NestedMemAddrDataAvoider & nested_finder_; + NestedMemAddrDataAvoider& nested_finder_; }; // class MemReadFinder -*/ +#endif } // namespace ilang -#endif // AST_HELPER_H__ +#endif // ILANG_MCM_AST_HELPER_H__ diff --git a/include/ilang/mcm/axiom_helper.h b/include/ilang/mcm/axiom_helper.h index 26ce97b46..1773075d0 100644 --- a/include/ilang/mcm/axiom_helper.h +++ b/include/ilang/mcm/axiom_helper.h @@ -1,8 +1,8 @@ /// \file /// Header for Axiom helpers (some helper classes to used in writing Axioms) -#ifndef AXIOM_HELPER_H__ -#define AXIOM_HELPER_H__ +#ifndef ILANG_MCM_AXIOM_HELPER_H__ +#define ILANG_MCM_AXIOM_HELPER_H__ /// \namespace ilang namespace ilang { @@ -23,4 +23,4 @@ z3::expr Z3And(const z3::expr& a, const z3::expr& b); } // namespace ilang -#endif // AXIOM_HELPER_H__ +#endif // ILANG_MCM_AXIOM_HELPER_H__ diff --git a/include/ilang/mcm/inter_ila_unroller.h b/include/ilang/mcm/inter_ila_unroller.h index 44f18dd74..88553a362 100644 --- a/include/ilang/mcm/inter_ila_unroller.h +++ b/include/ilang/mcm/inter_ila_unroller.h @@ -1,19 +1,20 @@ /// \file /// Header for multi-ILA unroller -#ifndef INTER_ILA_UNROLLER_H__ -#define INTER_ILA_UNROLLER_H__ +#ifndef ILANG_MCM_INTER_ILA_UNROLLER_H__ +#define ILANG_MCM_INTER_ILA_UNROLLER_H__ -#include "ilang/ila/instr_lvl_abs.h" -#include "ilang/ila/z3_expr_adapter.h" -#include "ilang/mcm/memory_model.h" -#include "z3++.h" #include #include #include #include #include +#include "ilang/ila/instr_lvl_abs.h" +#include "ilang/ila/z3_expr_adapter.h" +#include "ilang/mcm/memory_model.h" +#include "z3++.h" + /// \namespace ilang namespace ilang { @@ -218,4 +219,4 @@ class HostRemoveRestore { } // namespace ilang -#endif // INTER_ILA_UNROLLER_H__ +#endif // ILANG_MCM_INTER_ILA_UNROLLER_H__ diff --git a/include/ilang/mcm/sc_manual.h b/include/ilang/mcm/sc_manual.h index a8438a857..049d8b8f0 100644 --- a/include/ilang/mcm/sc_manual.h +++ b/include/ilang/mcm/sc_manual.h @@ -2,8 +2,8 @@ /// Header for SC memory model (constructed manually, rather than fully /// automaticated generation) -#ifndef SC_MANUAL_H__ -#define SC_MANUAL_H__ +#ifndef ILANG_MCM_SC_MANUAL_H__ +#define ILANG_MCM_SC_MANUAL_H__ #include #include @@ -67,4 +67,4 @@ class Sc : public MemoryModel { } // namespace ilang -#endif // SC_MANUAL_H__ +#endif // ILANG_MCM_SC_MANUAL_H__ diff --git a/include/ilang/mcm/set_op.h b/include/ilang/mcm/set_op.h index 024ed84af..95344d947 100644 --- a/include/ilang/mcm/set_op.h +++ b/include/ilang/mcm/set_op.h @@ -1,8 +1,8 @@ /// \file /// Some short cut for set operations -#ifndef MCM_SET_OP_H__ -#define MCM_SET_OP_H__ +#ifndef ILANG_MCM_SET_OP_H__ +#define ILANG_MCM_SET_OP_H__ #include #include @@ -24,4 +24,4 @@ #define IN(e, s) ((s).find(e) != (s).end()) #define IN_p(e, s) ((s)->find(e) != (s)->end()) -#endif // MCM_SET_OP_H__ +#endif // ILANG_MCM_SET_OP_H__ diff --git a/include/ilang/mcm/tso_manual.h b/include/ilang/mcm/tso_manual.h index 3639d3572..f71bc9a13 100644 --- a/include/ilang/mcm/tso_manual.h +++ b/include/ilang/mcm/tso_manual.h @@ -1,8 +1,8 @@ /// \file /// Header for TSO memory model -#ifndef TSO_MANUAL_H__ -#define TSO_MANUAL_H__ +#ifndef ILANG_MCM_TSO_MANUAL_H__ +#define ILANG_MCM_TSO_MANUAL_H__ #include "ilang/mcm/memory_model.h" @@ -76,4 +76,4 @@ class Tso : public MemoryModel { } // namespace ilang -#endif // TSO_MANUAL_H__ +#endif // ILANG_MCM_TSO_MANUAL_H__ From 59902174c3d73cbfe633848d8f8aa85fc21f36c6 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 29 Jul 2019 00:19:59 -0700 Subject: [PATCH 27/94] Turn on test build on Windows --- azure-pipelines.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index b1b3ea865..a44469469 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -126,7 +126,7 @@ jobs: - script: | md build cd build - cmake .. -DILANG_BUILD_SYNTH=OFF -DILANG_BUILD_TEST=OFF -DBUILD_SHARED_LIBS=OFF -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe + cmake .. -DILANG_BUILD_SYNTH=OFF -DBUILD_SHARED_LIBS=OFF -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe cmake --build . cmake --build . --target install displayName: 'build' From ab53822c43bc8390bc8bdca2e1ce00d27fa55d25 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 29 Jul 2019 01:17:05 -0700 Subject: [PATCH 28/94] Install gtest independently --- azure-pipelines.yml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index a44469469..74369bec4 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -105,6 +105,15 @@ jobs: cmake --build . --target install displayName: 'glog' + - script: | + cd extern + cd googletest + md build + cd build + cmake .. + cmake --build . --target install + displayName: 'gtest' + - script: | cd extern cd json From 841e20e0c095a68c034aca1026fc7eb0d82c7dcd Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 29 Jul 2019 21:35:41 -0700 Subject: [PATCH 29/94] Build archive libs for gtest --- azure-pipelines.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 74369bec4..869222ece 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -110,7 +110,7 @@ jobs: cd googletest md build cd build - cmake .. + cmake .. -DBUILD_SHARED_LIBS=OFF cmake --build . --target install displayName: 'gtest' From f7c57f6a7b4d7ce1571676acabd0e6ff6fc32dd3 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 29 Jul 2019 21:52:16 -0700 Subject: [PATCH 30/94] Pass the BUILD_SHARED_LIBS var to gtest --- azure-pipelines.yml | 9 --------- test/CMakeLists.txt | 2 +- 2 files changed, 1 insertion(+), 10 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 869222ece..a44469469 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -105,15 +105,6 @@ jobs: cmake --build . --target install displayName: 'glog' - - script: | - cd extern - cd googletest - md build - cd build - cmake .. -DBUILD_SHARED_LIBS=OFF - cmake --build . --target install - displayName: 'gtest' - - script: | cd extern cd json diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 3f8054e87..1b3108d84 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -9,7 +9,7 @@ add_subdirectory("${PROJECT_SOURCE_DIR}/extern/googletest" "extern/googletest" ## To keep cache clean ## mark_as_advanced( - BUILD_GMOCK BUILD_GTEST BUILD_SHARED_LIBS + BUILD_GMOCK BUILD_GTEST # BUILD_SHARED_LIBS gmock_build_tests gtest_build_samples gtest_build_tests gtest_disable_pthreads gtest_force_shared_crt gtest_hide_internal_symbols ) From d42bf0f59a4939d5606e15a66a10e25ef406064e Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 29 Jul 2019 22:27:54 -0700 Subject: [PATCH 31/94] Let the var be in the cache --- test/CMakeLists.txt | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 1b3108d84..c8cbeaf8d 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -8,11 +8,11 @@ add_subdirectory("${PROJECT_SOURCE_DIR}/extern/googletest" "extern/googletest" ## ## To keep cache clean ## -mark_as_advanced( - BUILD_GMOCK BUILD_GTEST # BUILD_SHARED_LIBS - gmock_build_tests gtest_build_samples gtest_build_tests - gtest_disable_pthreads gtest_force_shared_crt gtest_hide_internal_symbols -) +# mark_as_advanced( +# BUILD_GMOCK BUILD_GTEST BUILD_SHARED_LIBS +# gmock_build_tests gtest_build_samples gtest_build_tests +# gtest_disable_pthreads gtest_force_shared_crt gtest_hide_internal_symbols +# ) ## ## Keep IDEs that support folders clean From 1a96d815804b1870938a9e9e8a6df43129a1378f Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 29 Jul 2019 23:21:51 -0700 Subject: [PATCH 32/94] Disable pthreads in gtest --- azure-pipelines.yml | 3 ++- test/CMakeLists.txt | 10 +++++----- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index a44469469..80285e672 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -126,7 +126,8 @@ jobs: - script: | md build cd build - cmake .. -DILANG_BUILD_SYNTH=OFF -DBUILD_SHARED_LIBS=OFF -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe + # For building the test, we need CMAKE_MSVC_RUNTIME_LIBRARY (which will be supported in CMake 3.15+) + cmake .. -DILANG_BUILD_SYNTH=OFF -DILANG_BUILD_TEST=OFF -DBUILD_SHARED_LIBS=OFF -Dgtest_disable_pthreads=ON -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe cmake --build . cmake --build . --target install displayName: 'build' diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index c8cbeaf8d..3f8054e87 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -8,11 +8,11 @@ add_subdirectory("${PROJECT_SOURCE_DIR}/extern/googletest" "extern/googletest" ## ## To keep cache clean ## -# mark_as_advanced( -# BUILD_GMOCK BUILD_GTEST BUILD_SHARED_LIBS -# gmock_build_tests gtest_build_samples gtest_build_tests -# gtest_disable_pthreads gtest_force_shared_crt gtest_hide_internal_symbols -# ) +mark_as_advanced( + BUILD_GMOCK BUILD_GTEST BUILD_SHARED_LIBS + gmock_build_tests gtest_build_samples gtest_build_tests + gtest_disable_pthreads gtest_force_shared_crt gtest_hide_internal_symbols +) ## ## Keep IDEs that support folders clean From 64d7b153d535380f524cb904be70fc9171abea51 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 29 Jul 2019 23:30:20 -0700 Subject: [PATCH 33/94] Turn on build test to test the effect of disabling pthreads --- azure-pipelines.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 80285e672..da1b4574c 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -127,7 +127,7 @@ jobs: md build cd build # For building the test, we need CMAKE_MSVC_RUNTIME_LIBRARY (which will be supported in CMake 3.15+) - cmake .. -DILANG_BUILD_SYNTH=OFF -DILANG_BUILD_TEST=OFF -DBUILD_SHARED_LIBS=OFF -Dgtest_disable_pthreads=ON -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe + cmake .. -DILANG_BUILD_SYNTH=OFF -DBUILD_SHARED_LIBS=OFF -Dgtest_disable_pthreads=ON -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe cmake --build . cmake --build . --target install displayName: 'build' From 9c4fa7a201dd56c247d5dde82f8395f2959035ba Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 29 Jul 2019 23:45:51 -0700 Subject: [PATCH 34/94] TODO: set MSVC runtime for gtest --- azure-pipelines.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index da1b4574c..fc896be37 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -127,7 +127,7 @@ jobs: md build cd build # For building the test, we need CMAKE_MSVC_RUNTIME_LIBRARY (which will be supported in CMake 3.15+) - cmake .. -DILANG_BUILD_SYNTH=OFF -DBUILD_SHARED_LIBS=OFF -Dgtest_disable_pthreads=ON -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe + cmake .. -DILANG_BUILD_SYNTH=OFF -DILANG_BUILD_TEST=OFF -DBUILD_SHARED_LIBS=OFF -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe cmake --build . cmake --build . --target install displayName: 'build' From 1d2c689561cde06233cb8320f816dce88991a44b Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 30 Jul 2019 00:55:18 -0700 Subject: [PATCH 35/94] Initialize qemu_target (#141). --- include/ilang/target-sc/ila_sim.h | 2 +- src/target-sc/ila_sim.cc | 13 ++----------- 2 files changed, 3 insertions(+), 12 deletions(-) diff --git a/include/ilang/target-sc/ila_sim.h b/include/ilang/target-sc/ila_sim.h index b3e76ffe3..7e33d8d36 100644 --- a/include/ilang/target-sc/ila_sim.h +++ b/include/ilang/target-sc/ila_sim.h @@ -220,7 +220,7 @@ class IlaSim { // instruction name and the updated state name. However, there is a potential // same-name bug if setting true. bool readable_ = true; - bool qemu_device_; + bool qemu_device_ = false; InstrLvlAbsPtr model_ptr_; }; diff --git a/src/target-sc/ila_sim.cc b/src/target-sc/ila_sim.cc index 04bc40362..04f1e8af4 100644 --- a/src/target-sc/ila_sim.cc +++ b/src/target-sc/ila_sim.cc @@ -6,18 +6,9 @@ namespace ilang { -IlaSim::IlaSim() { - ld_st_counter_ = 0; - EXTERNAL_MEM_ = false; - readable_ = true; -} +IlaSim::IlaSim() {} -IlaSim::IlaSim(const InstrLvlAbsPtr& model_ptr) { - model_ptr_ = model_ptr; - ld_st_counter_ = 0; - EXTERNAL_MEM_ = false; - readable_ = true; -} +IlaSim::IlaSim(const InstrLvlAbsPtr& model_ptr) { model_ptr_ = model_ptr; } void IlaSim::set_instr_lvl_abs(const InstrLvlAbsPtr& model_ptr) { model_ptr_ = model_ptr; From f53606cb28ee92eda6ef70e40e8945502c45ecb4 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 30 Jul 2019 00:55:37 -0700 Subject: [PATCH 36/94] Check mkdir result (#141) --- src/util/fs.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/fs.cc b/src/util/fs.cc index 1abf4cd3b..327ba0da5 100644 --- a/src/util/fs.cc +++ b/src/util/fs.cc @@ -39,11 +39,11 @@ bool os_portable_mkdir(const std::string& dir) { return _mkdir(dir.c_str()) == 0; #else // on *nix - mkdir(dir.c_str(), S_IRWXU | S_IRWXG | S_IROTH | S_IXOTH); + auto res = mkdir(dir.c_str(), S_IRWXU | S_IRWXG | S_IROTH | S_IXOTH) != -1; struct stat statbuff; if (stat(dir.c_str(), &statbuff) != -1) { - return S_ISDIR(statbuff.st_mode); + return res || S_ISDIR(statbuff.st_mode); } return false; #endif From 414b5a4ff7bdf3c2502a3842d1a30b98953b0f88 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 30 Jul 2019 23:09:59 -0700 Subject: [PATCH 37/94] Cleanup headers - verilog in --- include/ilang/verilog-in/verilog_analysis.h | 12 +++++------- include/ilang/verilog-in/verilog_analysis_wrapper.h | 7 +++---- include/ilang/verilog-in/verilog_parse.h | 9 ++++----- 3 files changed, 12 insertions(+), 16 deletions(-) diff --git a/include/ilang/verilog-in/verilog_analysis.h b/include/ilang/verilog-in/verilog_analysis.h index d160de32c..1562033fb 100644 --- a/include/ilang/verilog-in/verilog_analysis.h +++ b/include/ilang/verilog-in/verilog_analysis.h @@ -1,4 +1,4 @@ -///\file Header for Verilog Analyzer +/// \file Header for Verilog Analyzer /// /// This is to use the info generated by the parser /// to gather the following informations @@ -14,11 +14,10 @@ /// // ---Hongce Zhang -#ifndef VERILOG_ANALYSIS_H__ -#define VERILOG_ANALYSIS_H__ +#ifndef ILANG_VERILOG_IN_VERILOG_ANALYSIS_H__ +#define ILANG_VERILOG_IN_VERILOG_ANALYSIS_H__ #include -#include // I have to put this include here, because it needs to know the class // VerilogAnalyzerBase @@ -202,8 +201,7 @@ class VerilogAnalyzer : public VerilogAnalyzerBase { static vlg_loc_t Meta2Loc(const ast_metadata& md) { return vlg_loc_t(md.file, md.line); } - // --------------------- FOR verilog const parser ---------------------------- - // // + // --------------------- FOR verilog const parser ----------- // /// Get the hierarchy information needed by constant parser /// returns true if succeed bool get_hierarchy_from_full_name( @@ -235,4 +233,4 @@ class VerilogAnalyzer : public VerilogAnalyzerBase { }; // namespace ilang -#endif // VERILOG_ANALYSIS_H__ +#endif // ILANG_VERILOG_IN_VERILOG_ANALYSIS_H__ diff --git a/include/ilang/verilog-in/verilog_analysis_wrapper.h b/include/ilang/verilog-in/verilog_analysis_wrapper.h index 3d710311e..9a56d058b 100644 --- a/include/ilang/verilog-in/verilog_analysis_wrapper.h +++ b/include/ilang/verilog-in/verilog_analysis_wrapper.h @@ -7,12 +7,11 @@ /// /// --- Hongce Zhang -#ifndef VERILOG_ANALYSIS_WRAPPER_H__ -#define VERILOG_ANALYSIS_WRAPPER_H__ +#ifndef ILANG_VERILOG_IN_VERILOG_ANALYSIS_WRAPPER_H__ +#define ILANG_VERILOG_IN_VERILOG_ANALYSIS_WRAPPER_H__ #include #include -#include #include #include @@ -249,4 +248,4 @@ std::ostream& operator<<(std::ostream& os, }; // namespace ilang -#endif // VERILOG_ANALYSIS_WRAPPER_H__ +#endif // ILANG_VERILOG_IN_VERILOG_ANALYSIS_WRAPPER_H__ diff --git a/include/ilang/verilog-in/verilog_parse.h b/include/ilang/verilog-in/verilog_parse.h index 98151eb81..20b9be8f5 100644 --- a/include/ilang/verilog-in/verilog_parse.h +++ b/include/ilang/verilog-in/verilog_parse.h @@ -1,11 +1,10 @@ /// \file /// Header for testing Verilog files -#ifndef VERILOG_PARSE_H__ -#define VERILOG_PARSE_H__ +#ifndef ILANG_VERILOG_IN_VERILOG_PARSE_H__ +#define ILANG_VERILOG_IN_VERILOG_PARSE_H__ -#include -#include +#include /// \namespace ilang namespace ilang { @@ -15,4 +14,4 @@ int TestParseVerilogFrom(const std::string& fn); }; // namespace ilang -#endif // VERILOG_PARSE_H__ +#endif // ILANG_VERILOG_IN_VERILOG_PARSE_H__ From b030f7fa875e344a8af4350044ffcb2ad49d5758 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 30 Jul 2019 23:14:19 -0700 Subject: [PATCH 38/94] Cleanup headers - verilog out --- include/ilang/verilog-out/verilog_gen.h | 1 - 1 file changed, 1 deletion(-) diff --git a/include/ilang/verilog-out/verilog_gen.h b/include/ilang/verilog-out/verilog_gen.h index f6959ab3d..aa180b90e 100644 --- a/include/ilang/verilog-out/verilog_gen.h +++ b/include/ilang/verilog-out/verilog_gen.h @@ -17,7 +17,6 @@ #include #include -#include /// \namespace ilang namespace ilang { From 6359c9d5694d77c36ac628d2bdd0411bfe168c6e Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 30 Jul 2019 23:23:18 -0700 Subject: [PATCH 39/94] Cleanup headers - vtarget out --- include/ilang/vtarget-out/absmem.h | 11 ++++++----- include/ilang/vtarget-out/directive.h | 13 +++++++------ include/ilang/vtarget-out/var_extract.h | 6 +++--- include/ilang/vtarget-out/vlg_mod.h | 12 ++++++------ include/ilang/vtarget-out/vtarget_gen.h | 7 +++---- include/ilang/vtarget-out/vtarget_gen_cosa.h | 13 +++++++------ include/ilang/vtarget-out/vtarget_gen_impl.h | 15 +++++++-------- include/ilang/vtarget-out/vtarget_gen_jasper.h | 6 +++--- 8 files changed, 42 insertions(+), 41 deletions(-) diff --git a/include/ilang/vtarget-out/absmem.h b/include/ilang/vtarget-out/absmem.h index c9808a77c..c97ca12b1 100644 --- a/include/ilang/vtarget-out/absmem.h +++ b/include/ilang/vtarget-out/absmem.h @@ -1,17 +1,18 @@ /// \file Header for generating abstract memory // --- Hongce Zhang -#ifndef ABS_MEM_H__ -#define ABS_MEM_H__ +#ifndef ILANG_VTARGET_OUT_ABS_MEM_H__ +#define ILANG_VTARGET_OUT_ABS_MEM_H__ -#include -#include #include #include #include #include #include +#include +#include + namespace ilang { /// \brief a struct to store abstract memory @@ -81,4 +82,4 @@ struct VlgAbsMem { }; // namespace ilang -#endif // ABS_MEM_H__ \ No newline at end of file +#endif // ILANG_VTARGET_OUT_ABS_MEM_H__ diff --git a/include/ilang/vtarget-out/directive.h b/include/ilang/vtarget-out/directive.h index 5334fe0e6..993857997 100644 --- a/include/ilang/vtarget-out/directive.h +++ b/include/ilang/vtarget-out/directive.h @@ -2,17 +2,18 @@ /// Verification Target Generation Some I/O has special meanings, and special /// usage The wrapper has to be able to handle it // --- Hongce Zhang -#ifndef DIRECTIVE_H__ -#define DIRECTIVE_H__ +#ifndef ILANG_VTARGET_OUT_DIRECTIVE_H__ +#define ILANG_VTARGET_OUT_DIRECTIVE_H__ #include -#include -#include -#include #include #include #include +#include +#include +#include + namespace ilang { /// \brief Used in Verilog Verification Target Generation @@ -154,4 +155,4 @@ class StateMappingDirectiveRecorder { }; // namespace ilang -#endif // DIRECTIVE_H__ +#endif // ILANG_VTARGET_OUT_DIRECTIVE_H__ diff --git a/include/ilang/vtarget-out/var_extract.h b/include/ilang/vtarget-out/var_extract.h index bae95f5e4..b8e4ec89c 100644 --- a/include/ilang/vtarget-out/var_extract.h +++ b/include/ilang/vtarget-out/var_extract.h @@ -4,8 +4,8 @@ /// and change their name if needed and generate a string // --- Hongce Zhang -#ifndef VAR_EXTRACT_H__ -#define VAR_EXTRACT_H__ +#ifndef ILANG_VTARGET_OUT_VAR_EXTRACT_H__ +#define ILANG_VTARGET_OUT_VAR_EXTRACT_H__ #include #include @@ -65,4 +65,4 @@ class VarExtractor { }; // namespace ilang -#endif // VAR_EXTRACT_H__ \ No newline at end of file +#endif // ILANG_VTARGET_OUT_VAR_EXTRACT_H__ diff --git a/include/ilang/vtarget-out/vlg_mod.h b/include/ilang/vtarget-out/vlg_mod.h index 3d770e106..fb0d75bd4 100644 --- a/include/ilang/vtarget-out/vlg_mod.h +++ b/include/ilang/vtarget-out/vlg_mod.h @@ -7,15 +7,15 @@ /// 2c. wire and assign // ---Hongce Zhang (hongcez@princeton.edu) -#ifndef VLG_MOD_H__ -#define VLG_MOD_H__ - -#include +#ifndef ILANG_VTARGET_OUT_VLG_MOD_H__ +#define ILANG_VTARGET_OUT_VLG_MOD_H__ #include #include #include +#include + namespace ilang { /// \brief the class for modification to verilog @@ -126,8 +126,8 @@ class VerilogModifier { std::string& line_out, const std::string& vname, unsigned width); -}; // class v +}; // class VerilogModifier }; // namespace ilang -#endif // VLG_MOD_H__ +#endif // ILANG_VTARGET_OUT_VLG_MOD_H__ diff --git a/include/ilang/vtarget-out/vtarget_gen.h b/include/ilang/vtarget-out/vtarget_gen.h index 814f21d19..21882deee 100644 --- a/include/ilang/vtarget-out/vtarget_gen.h +++ b/include/ilang/vtarget-out/vtarget_gen.h @@ -2,11 +2,10 @@ /// This is used to avoid include json explicitly // --- Hongce Zhang -#ifndef VTARGET_GEN_H__ -#define VTARGET_GEN_H__ +#ifndef ILANG_VTARGET_OUT_VTARGET_GEN_H__ +#define ILANG_VTARGET_OUT_VTARGET_GEN_H__ #include - #include #include @@ -127,4 +126,4 @@ class VerilogVerificationTargetGenerator { }; // namespace ilang -#endif // VTARGET_GEN_H__ \ No newline at end of file +#endif // ILANG_VTARGET_OUT_VTARGET_GEN_H__ diff --git a/include/ilang/vtarget-out/vtarget_gen_cosa.h b/include/ilang/vtarget-out/vtarget_gen_cosa.h index 8abf99740..8523bc881 100644 --- a/include/ilang/vtarget-out/vtarget_gen_cosa.h +++ b/include/ilang/vtarget-out/vtarget_gen_cosa.h @@ -3,18 +3,19 @@ /// Internally, we use the // ---Hongce Zhang -#ifndef VTARGET_GEN_COSA_H__ -#define VTARGET_GEN_COSA_H__ +#ifndef ILANG_VTARGET_OUT_VTARGET_GEN_COSA_H__ +#define ILANG_VTARGET_OUT_VTARGET_GEN_COSA_H__ -#include - -#include #include #include + #include #include #include +#include +#include + namespace ilang { class VlgSglTgtGen_Cosa; @@ -135,4 +136,4 @@ class VlgSglTgtGen_Cosa : public VlgSglTgtGen { }; // namespace ilang -#endif // VTARGET_GEN_COSA_H__ +#endif // ILANG_VTARGET_OUT_VTARGET_GEN_COSA_H__ diff --git a/include/ilang/vtarget-out/vtarget_gen_impl.h b/include/ilang/vtarget-out/vtarget_gen_impl.h index e4ca7d5d2..c95be9315 100644 --- a/include/ilang/vtarget-out/vtarget_gen_impl.h +++ b/include/ilang/vtarget-out/vtarget_gen_impl.h @@ -11,13 +11,8 @@ /// although it might be easier /// we need to copy some of the vlg-out's functionality -#ifndef VTARGET_GEN_IMPL_H__ -#define VTARGET_GEN_IMPL_H__ - -#include -#include -#include -#include +#ifndef ILANG_VTARGET_OUT_VTARGET_GEN_IMPL_H__ +#define ILANG_VTARGET_OUT_VTARGET_GEN_IMPL_H__ #include #include @@ -28,6 +23,10 @@ #include #include #include +#include +#include +#include +#include namespace ilang { @@ -418,4 +417,4 @@ class VlgVerifTgtGen : public VlgVerifTgtGenBase { }; // namespace ilang -#endif // VTARGET_GEN_IMPL_H__ +#endif // ILANG_VTARGET_OUT_VTARGET_GEN_IMPL_H__ diff --git a/include/ilang/vtarget-out/vtarget_gen_jasper.h b/include/ilang/vtarget-out/vtarget_gen_jasper.h index b6b6259d3..5d1f49028 100644 --- a/include/ilang/vtarget-out/vtarget_gen_jasper.h +++ b/include/ilang/vtarget-out/vtarget_gen_jasper.h @@ -1,8 +1,8 @@ /// \file Verilog Verification Target Generator -- for JasperGold // ---Hongce Zhang -#ifndef VTARGET_GEN_JASPER_H__ -#define VTARGET_GEN_JASPER_H__ +#ifndef ILANG_VTARGET_OUT_VTARGET_GEN_JASPER_H__ +#define ILANG_VTARGET_OUT_VTARGET_GEN_JASPER_H__ #include @@ -114,4 +114,4 @@ class VlgSglTgtGen_Jasper : public VlgSglTgtGen { }; // namespace ilang -#endif // VTARGET_GEN_JASPER_H__ \ No newline at end of file +#endif // ILANG_VTARGET_OUT_VTARGET_GEN_JASPER_H__ From 0fe267013dfc92bbade907da92390421f9802229 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 31 Jul 2019 02:23:12 -0700 Subject: [PATCH 40/94] Update README.md Fix #77 --- README.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 3145733e9..0d509529b 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,15 @@ [![ILAng](https://raw.githubusercontent.com/Bo-Yuan-Huang/ILAng/master/docs/pics/ilang-logo.png)](https://bo-yuan-huang.gitbook.io/ilang/) +[![Build Status](https://dev.azure.com/byhuang/ILAng/_apis/build/status/Bo-Yuan-Huang.ILAng?branchName=master)](https://dev.azure.com/byhuang/ILAng/_build/latest?definitionId=1&branchName=master) [![Build Status](https://travis-ci.org/Bo-Yuan-Huang/ILAng.svg?branch=master)](https://travis-ci.org/Bo-Yuan-Huang/ILAng) [![Build Status](https://semaphoreci.com/api/v1/bo-yuan-huang/ilang/branches/master/shields_badge.svg)](https://semaphoreci.com/bo-yuan-huang/ilang) [![Build status](https://ci.appveyor.com/api/projects/status/cwhlq09513art6hw/branch/master?svg=true)](https://ci.appveyor.com/project/Bo-Yuan-Huang/ilang/branch/master) -[![Build Status](https://dev.azure.com/byhuang/ILAng/_apis/build/status/Bo-Yuan-Huang.ILAng?branchName=master)](https://dev.azure.com/byhuang/ILAng/_build/latest?definitionId=1&branchName=master) + +[![Coverity Scan Build Status](https://scan.coverity.com/projects/bo-yuan-huang-ilang)](https://scan.coverity.com/projects/17719/badge.svg) [![Coverage Status](https://coveralls.io/repos/github/Bo-Yuan-Huang/ILAng/badge.svg?branch=master)](https://coveralls.io/github/Bo-Yuan-Huang/ILAng?branch=master) -[![Codacy Badge](https://api.codacy.com/project/badge/Grade/b120e2527cc04d4aacd1dc11581e2f30)](https://www.codacy.com/app/Bo-Yuan-Huang/ILAng?utm_source=github.com&utm_medium=referral&utm_content=Bo-Yuan-Huang/ILAng&utm_campaign=Badge_Grade) [![Language grade: C/C++](https://img.shields.io/lgtm/grade/cpp/g/Bo-Yuan-Huang/ILAng.svg?logo=lgtm&logoWidth=18)](https://lgtm.com/projects/g/Bo-Yuan-Huang/ILAng/context:cpp) +[![Codacy Badge](https://api.codacy.com/project/badge/Grade/b120e2527cc04d4aacd1dc11581e2f30)](https://www.codacy.com/app/Bo-Yuan-Huang/ILAng?utm_source=github.com&utm_medium=referral&utm_content=Bo-Yuan-Huang/ILAng&utm_campaign=Badge_Grade) + [![license](https://img.shields.io/github/license/bo-yuan-huang/ilang.svg?style=flat)](https://github.com/Bo-Yuan-Huang/ILA-Tools/blob/master/LICENSE) [![Documentation](https://img.shields.io/badge/docs-manual-blue.svg)](https://bo-yuan-huang.gitbook.io/ilang/) [![Documentation](https://img.shields.io/badge/docs-doxygen-blue.svg)](https://bo-yuan-huang.github.io/ILAng-Doc/doxygen-output-html/namespaceilang.html) From 7a52f6a9b3919644524fcda054f95e8755da1ac8 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 31 Jul 2019 02:24:33 -0700 Subject: [PATCH 41/94] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 0d509529b..2799fffbb 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,7 @@ [![Build Status](https://semaphoreci.com/api/v1/bo-yuan-huang/ilang/branches/master/shields_badge.svg)](https://semaphoreci.com/bo-yuan-huang/ilang) [![Build status](https://ci.appveyor.com/api/projects/status/cwhlq09513art6hw/branch/master?svg=true)](https://ci.appveyor.com/project/Bo-Yuan-Huang/ilang/branch/master) -[![Coverity Scan Build Status](https://scan.coverity.com/projects/bo-yuan-huang-ilang)](https://scan.coverity.com/projects/17719/badge.svg) +[![Coverity Scan Build Status](https://scan.coverity.com/projects/17719/badge.svg)](https://scan.coverity.com/projects/bo-yuan-huang-ilang) [![Coverage Status](https://coveralls.io/repos/github/Bo-Yuan-Huang/ILAng/badge.svg?branch=master)](https://coveralls.io/github/Bo-Yuan-Huang/ILAng?branch=master) [![Language grade: C/C++](https://img.shields.io/lgtm/grade/cpp/g/Bo-Yuan-Huang/ILAng.svg?logo=lgtm&logoWidth=18)](https://lgtm.com/projects/g/Bo-Yuan-Huang/ILAng/context:cpp) [![Codacy Badge](https://api.codacy.com/project/badge/Grade/b120e2527cc04d4aacd1dc11581e2f30)](https://www.codacy.com/app/Bo-Yuan-Huang/ILAng?utm_source=github.com&utm_medium=referral&utm_content=Bo-Yuan-Huang/ILAng&utm_campaign=Badge_Grade) From 8a0a89a282f2f29e44ae090b1601ba9c37618f69 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 31 Jul 2019 02:26:06 -0700 Subject: [PATCH 42/94] Update README.md --- README.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/README.md b/README.md index 2799fffbb..4c4747b7d 100644 --- a/README.md +++ b/README.md @@ -4,12 +4,10 @@ [![Build Status](https://travis-ci.org/Bo-Yuan-Huang/ILAng.svg?branch=master)](https://travis-ci.org/Bo-Yuan-Huang/ILAng) [![Build Status](https://semaphoreci.com/api/v1/bo-yuan-huang/ilang/branches/master/shields_badge.svg)](https://semaphoreci.com/bo-yuan-huang/ilang) [![Build status](https://ci.appveyor.com/api/projects/status/cwhlq09513art6hw/branch/master?svg=true)](https://ci.appveyor.com/project/Bo-Yuan-Huang/ilang/branch/master) - [![Coverity Scan Build Status](https://scan.coverity.com/projects/17719/badge.svg)](https://scan.coverity.com/projects/bo-yuan-huang-ilang) [![Coverage Status](https://coveralls.io/repos/github/Bo-Yuan-Huang/ILAng/badge.svg?branch=master)](https://coveralls.io/github/Bo-Yuan-Huang/ILAng?branch=master) [![Language grade: C/C++](https://img.shields.io/lgtm/grade/cpp/g/Bo-Yuan-Huang/ILAng.svg?logo=lgtm&logoWidth=18)](https://lgtm.com/projects/g/Bo-Yuan-Huang/ILAng/context:cpp) [![Codacy Badge](https://api.codacy.com/project/badge/Grade/b120e2527cc04d4aacd1dc11581e2f30)](https://www.codacy.com/app/Bo-Yuan-Huang/ILAng?utm_source=github.com&utm_medium=referral&utm_content=Bo-Yuan-Huang/ILAng&utm_campaign=Badge_Grade) - [![license](https://img.shields.io/github/license/bo-yuan-huang/ilang.svg?style=flat)](https://github.com/Bo-Yuan-Huang/ILA-Tools/blob/master/LICENSE) [![Documentation](https://img.shields.io/badge/docs-manual-blue.svg)](https://bo-yuan-huang.gitbook.io/ilang/) [![Documentation](https://img.shields.io/badge/docs-doxygen-blue.svg)](https://bo-yuan-huang.github.io/ILAng-Doc/doxygen-output-html/namespaceilang.html) From 795507f023bc64dbd144484370bbb17c21c937b8 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Thu, 1 Aug 2019 02:04:53 -0700 Subject: [PATCH 43/94] Cleanup source - ila --- src/ila/ast/expr.cc | 3 +-- src/ila/ast/expr_const.cc | 22 ++++++++++------------ src/ila/ast/expr_op.cc | 7 ++++--- src/ila/ast/expr_var.cc | 4 +--- src/ila/ast/func.cc | 1 + src/ila/ast/sort.cc | 1 + src/ila/ast/sort_value.cc | 1 + src/ila/ast_fuse.cc | 4 ++-- src/ila/comp_ref_rel.cc | 1 + src/ila/expr_fuse.cc | 1 + src/ila/hash_ast.cc | 4 +++- src/ila/instr.cc | 1 + src/ila/instr_lvl_abs.cc | 17 +---------------- src/ila/symbol.cc | 1 + src/ila/transition.cc | 6 +++--- src/ila/validate_model.cc | 4 ++++ src/ila/z3_expr_adapter.cc | 2 +- 17 files changed, 37 insertions(+), 43 deletions(-) diff --git a/src/ila/ast/expr.cc b/src/ila/ast/expr.cc index 0123e6e9b..b5f46e695 100644 --- a/src/ila/ast/expr.cc +++ b/src/ila/ast/expr.cc @@ -2,12 +2,11 @@ /// Source for the class Expr #include + #include namespace ilang { -// typedef Expr::InstrLvlAbsPtr InstrLvlAbsPtr; - Expr::Expr() {} Expr::Expr(const std::string& name) : Ast(name) {} diff --git a/src/ila/ast/expr_const.cc b/src/ila/ast/expr_const.cc index b63eeb3db..eb091457e 100644 --- a/src/ila/ast/expr_const.cc +++ b/src/ila/ast/expr_const.cc @@ -2,27 +2,25 @@ /// Source for the class ExprConst #include + #include /// \namespace ilang namespace ilang { ExprConst::ExprConst(const BoolVal& bool_val) { - // set_sort(Sort()); set_sort(Sort::MakeBoolSort()); val_ = std::make_shared(bool_val); } ExprConst::ExprConst(const BvVal& bv_val, const int& bit_width) { set_sort(Sort::MakeBvSort(bit_width)); - // set_sort(Sort(bit_width)); val_ = std::make_shared(bv_val); } ExprConst::ExprConst(const MemVal& mem_val, const int& addr_width, const int& data_width) { set_sort(Sort::MakeMemSort(addr_width, data_width)); - // set_sort(Sort(addr_width, data_width)); val_ = std::make_shared(mem_val); } @@ -30,7 +28,7 @@ ExprConst::~ExprConst() {} z3::expr ExprConst::GetZ3Expr(z3::context& ctx, const Z3ExprVec& z3expr_vec, const std::string& suffix) const { - ILA_ASSERT(z3expr_vec.empty()) << "Constant should be terminating nodes.\n"; + ILA_ASSERT(z3expr_vec.empty()) << "Constant should be terminating nodes."; if (is_bool()) { auto bool_ptr = val_bool(); @@ -39,7 +37,7 @@ z3::expr ExprConst::GetZ3Expr(z3::context& ctx, const Z3ExprVec& z3expr_vec, auto bv_ptr = val_bv(); return ctx.bv_val(bv_ptr->val(), sort()->bit_width()); } else { - ILA_ASSERT(is_mem()) << "Neither bool, bv, nor mem.\n"; + ILA_ASSERT(is_mem()) << "Neither bool, bv, nor mem."; auto addr_sort = ctx.bv_sort(sort()->addr_width()); auto data_sort = ctx.bv_sort(sort()->data_width()); @@ -69,30 +67,30 @@ std::ostream& ExprConst::Print(std::ostream& out) const { auto bv_ptr = val_bv(); return bv_ptr->Print(out); } else { - ILA_ASSERT(is_mem()) << "Print neither bool, bv, nor mem.\n"; + ILA_ASSERT(is_mem()) << "Print neither bool, bv, nor mem."; auto mem_ptr = val_mem(); return mem_ptr->Print(out); } } BoolValPtr ExprConst::val_bool() const { - ILA_ASSERT(is_bool()) << "Not boolean constant\n"; + ILA_ASSERT(is_bool()) << "Not boolean constant"; auto ptr = std::dynamic_pointer_cast(val_); - ILA_ASSERT(ptr) << "Fail casting to BoolVal\n"; + ILA_ASSERT(ptr) << "Fail casting to BoolVal"; return ptr; } BvValPtr ExprConst::val_bv() const { - ILA_ASSERT(is_bv()) << "Not bitvector constant\n"; + ILA_ASSERT(is_bv()) << "Not bitvector constant"; auto ptr = std::dynamic_pointer_cast(val_); - ILA_ASSERT(ptr) << "Fail casting to BvVal\n"; + ILA_ASSERT(ptr) << "Fail casting to BvVal"; return ptr; } MemValPtr ExprConst::val_mem() const { - ILA_ASSERT(is_mem()) << "Not memory constatnc\n"; + ILA_ASSERT(is_mem()) << "Not memory constatnc"; auto ptr = std::dynamic_pointer_cast(val_); - ILA_ASSERT(ptr) << "Fail casting to MemVal\n"; + ILA_ASSERT(ptr) << "Fail casting to MemVal"; return ptr; } diff --git a/src/ila/ast/expr_op.cc b/src/ila/ast/expr_op.cc index ebd5aff5f..fe033fd0f 100644 --- a/src/ila/ast/expr_op.cc +++ b/src/ila/ast/expr_op.cc @@ -2,6 +2,7 @@ /// Source for the op expression #include + #include #include #include @@ -491,7 +492,7 @@ z3::expr ExprOpSExt::GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec, ILA_ASSERT(expr_vec.size() == 1) << "Extend take 1 argument."; ILA_ASSERT(param_num() == 1) << "Extend need one parameter."; auto bv = expr_vec[0]; - auto org_wid = arg(0)->sort()->bit_width(); + auto org_wid = arg(0)->sort()->bit_width(); unsigned wid = static_cast(param(0) - org_wid); return Z3SExt(ctx, bv, wid); } @@ -504,7 +505,7 @@ ExprOpLRotate::ExprOpLRotate(const ExprPtr bv, const int& immediate) set_sort(bv->sort()); } -z3::expr ExprOpLRotate::GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec, +z3::expr ExprOpLRotate::GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec, const std::string& suffix) const { ILA_ASSERT(expr_vec.size() == 1) << "Rotate takes 1 argument."; ILA_ASSERT(param_num() == 1) << "Rotate takes 1 parameter."; @@ -521,7 +522,7 @@ ExprOpRRotate::ExprOpRRotate(const ExprPtr bv, const int& immediate) set_sort(bv->sort()); } -z3::expr ExprOpRRotate::GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec, +z3::expr ExprOpRRotate::GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec, const std::string& suffix) const { ILA_ASSERT(expr_vec.size() == 1) << "Rotate takes 1 argument."; ILA_ASSERT(param_num() == 1) << "Rotate takes 1 parameter."; diff --git a/src/ila/ast/expr_var.cc b/src/ila/ast/expr_var.cc index c02a4b637..24c407a9e 100644 --- a/src/ila/ast/expr_var.cc +++ b/src/ila/ast/expr_var.cc @@ -2,6 +2,7 @@ /// Source for the var expression #include + #include #include @@ -42,17 +43,14 @@ std::ostream& ExprVar::Print(std::ostream& out) const { } std::ostream& ExprVar::PrintBool(std::ostream& out) const { - // return out << name().format_str("Bool", ""); return out << name(); } std::ostream& ExprVar::PrintBv(std::ostream& out) const { - // return out << name().format_str("Bv", std::to_string(sort()->bit_width())); return out << name().str() + "(" + std::to_string(sort()->bit_width()) + ")"; } std::ostream& ExprVar::PrintMem(std::ostream& out) const { - // return out << name().format_str("Mem", ""); return out << name().str() + "(" + std::to_string(sort()->addr_width()) + ", " + std::to_string(sort()->data_width()) + ")"; } diff --git a/src/ila/ast/func.cc b/src/ila/ast/func.cc index 89b886cb5..5fa806386 100644 --- a/src/ila/ast/func.cc +++ b/src/ila/ast/func.cc @@ -2,6 +2,7 @@ /// Source for the class Func #include + #include #include #include diff --git a/src/ila/ast/sort.cc b/src/ila/ast/sort.cc index ae078adaf..c5b425ed1 100644 --- a/src/ila/ast/sort.cc +++ b/src/ila/ast/sort.cc @@ -2,6 +2,7 @@ /// Source for the class Sort #include + #include namespace ilang { diff --git a/src/ila/ast/sort_value.cc b/src/ila/ast/sort_value.cc index f0cd3f8c8..cbc090fc4 100644 --- a/src/ila/ast/sort_value.cc +++ b/src/ila/ast/sort_value.cc @@ -2,6 +2,7 @@ /// Source for the class BoolVal, BvVal, and MemVal #include + #include #include diff --git a/src/ila/ast_fuse.cc b/src/ila/ast_fuse.cc index fa8fb58d4..8bf1482f7 100644 --- a/src/ila/ast_fuse.cc +++ b/src/ila/ast_fuse.cc @@ -67,7 +67,7 @@ AST_UID_EXPR_OP GetUidExprOp(const ExprPtr& expr) { } else if (std::dynamic_pointer_cast(expr_op)) { return AST_UID_EXPR_OP::SREM; } else if (std::dynamic_pointer_cast(expr_op)) { - return AST_UID_EXPR_OP::UREM; + return AST_UID_EXPR_OP::UREM; } else if (std::dynamic_pointer_cast(expr_op)) { return AST_UID_EXPR_OP::MUL; } else if (std::dynamic_pointer_cast(expr_op)) { @@ -95,7 +95,7 @@ AST_UID_EXPR_OP GetUidExprOp(const ExprPtr& expr) { } else if (std::dynamic_pointer_cast(expr_op)) { return AST_UID_EXPR_OP::LROTATE; } else if (std::dynamic_pointer_cast(expr_op)) { - return AST_UID_EXPR_OP::RROTATE; + return AST_UID_EXPR_OP::RROTATE; } else if (std::dynamic_pointer_cast(expr_op)) { return AST_UID_EXPR_OP::APP_FUNC; } else if (std::dynamic_pointer_cast(expr_op)) { diff --git a/src/ila/comp_ref_rel.cc b/src/ila/comp_ref_rel.cc index e177ca7a1..65109ea90 100644 --- a/src/ila/comp_ref_rel.cc +++ b/src/ila/comp_ref_rel.cc @@ -2,6 +2,7 @@ /// Source for the refinement relation #include + #include #include diff --git a/src/ila/expr_fuse.cc b/src/ila/expr_fuse.cc index 24dab5ff5..339efdc7d 100644 --- a/src/ila/expr_fuse.cc +++ b/src/ila/expr_fuse.cc @@ -2,6 +2,7 @@ /// Source of ExprFuse #include + #include #include #include diff --git a/src/ila/hash_ast.cc b/src/ila/hash_ast.cc index ab8ea3834..191bf8347 100644 --- a/src/ila/hash_ast.cc +++ b/src/ila/hash_ast.cc @@ -3,8 +3,10 @@ // XXX Current replacing is not efficient. -#include #include + +#include + #include namespace ilang { diff --git a/src/ila/instr.cc b/src/ila/instr.cc index 3bc8230d7..71f87ae30 100644 --- a/src/ila/instr.cc +++ b/src/ila/instr.cc @@ -2,6 +2,7 @@ /// The source for the class Instr. #include + #include #include diff --git a/src/ila/instr_lvl_abs.cc b/src/ila/instr_lvl_abs.cc index e219daf73..97b273fbe 100644 --- a/src/ila/instr_lvl_abs.cc +++ b/src/ila/instr_lvl_abs.cc @@ -2,6 +2,7 @@ /// The source for the class InstrLvlAbs. #include + #include // Do the simplification by hashing AST sub-trees. @@ -96,22 +97,6 @@ void InstrLvlAbs::AddState(const ExprPtr state_var) { states_.push_back(name, var); } -#if 0 -void InstrLvlAbs::AddFreeVar(const ExprPtr free_var) { - // sanity check - ILA_NOT_NULL(free_var); - ILA_ASSERT(free_var->is_var()) << "Register non-var to free_vars_."; - // should be the first - auto name = free_var->name(); - auto poss = states_.find(name); - auto posi = inputs_.find(name); - ILA_ASSERT(poss == states_.end() && posi == inputs_.end()) - << "Free variable " << free_var << "has been declared."; - // register to free_vars_ - free_vars_.push_back(name, free_var); -} -#endif - void InstrLvlAbs::AddInit(const ExprPtr cntr_expr) { // sanity check ILA_NOT_NULL(cntr_expr); diff --git a/src/ila/symbol.cc b/src/ila/symbol.cc index a09cb1cc8..7201825aa 100644 --- a/src/ila/symbol.cc +++ b/src/ila/symbol.cc @@ -2,6 +2,7 @@ /// Source for the class Symbol. #include + #include #include diff --git a/src/ila/transition.cc b/src/ila/transition.cc index 88d1d2f0b..0463c642e 100644 --- a/src/ila/transition.cc +++ b/src/ila/transition.cc @@ -2,6 +2,7 @@ /// Source of instruction sequencing #include + #include namespace ilang { @@ -41,12 +42,12 @@ size_t InstrTranNode::next_num() const { return next_.size(); } size_t InstrTranNode::prev_num() const { return prev_.size(); } const ItNodePtr InstrTranNode::next(const size_t& i) const { - ILA_ASSERT(i < next_.size()) << "Access overflow for out-going nodes.\n"; + ILA_ASSERT(i < next_.size()) << "Access overflow for out-going nodes."; return next_.at(i); } const ItNodePtr InstrTranNode::prev(const size_t& i) const { - ILA_ASSERT(i < prev_.size()) << "Access overflow for in-comming nodes.\n"; + ILA_ASSERT(i < prev_.size()) << "Access overflow for in-comming nodes."; return prev_.at(i); } @@ -106,7 +107,6 @@ bool InstrSeq::CheckTransition() const { } InstrIdxKeyVecPtr InstrSeq::Sort() { - // ILA_ASSERT(sorted_->empty()); // TODO return sorted_; } diff --git a/src/ila/validate_model.cc b/src/ila/validate_model.cc index d495334de..1e7a3e5ba 100644 --- a/src/ila/validate_model.cc +++ b/src/ila/validate_model.cc @@ -1,3 +1,6 @@ +/// \file +/// The source for validating ILA. + #include #include "z3++.h" @@ -95,4 +98,5 @@ void CompleteModel(const InstrLvlAbsPtr& model_ptr, DEFAULT_UPDATE_METHOD dum) { } } } + } // namespace ilang diff --git a/src/ila/z3_expr_adapter.cc b/src/ila/z3_expr_adapter.cc index 2c46b772c..177ac627c 100644 --- a/src/ila/z3_expr_adapter.cc +++ b/src/ila/z3_expr_adapter.cc @@ -2,6 +2,7 @@ /// Source for the class Z3EXprAdapter #include + #include namespace ilang { @@ -16,7 +17,6 @@ z3::expr Z3ExprAdapter::GetExpr(const ExprPtr expr, const std::string& suffix) { expr->DepthFirstVisit(*this); - // auto pos = expr_map_.find(expr.get()); auto pos = expr_map_.find(expr); ILA_ASSERT(pos != expr_map_.end()) << "z3 expr cannot be generated."; From 2b0d1a292e93de1578d53d0781e62ae0323938f9 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Fri, 2 Aug 2019 01:35:47 -0700 Subject: [PATCH 44/94] Remove redundant legacy code --- src/python-api/CMakeLists.txt | 15 --------------- src/python-api/api_expr.cc | 27 --------------------------- src/python-api/api_ila.cc | 22 ---------------------- src/python-api/api_log.cc | 28 ---------------------------- src/python-api/ila_py_api.cc | 17 ----------------- src/python-api/wrap_expr.cc | 30 ------------------------------ src/python-api/wrap_ila.cc | 19 ------------------- src/python-api/wrap_log.cc | 17 ----------------- 8 files changed, 175 deletions(-) delete mode 100644 src/python-api/CMakeLists.txt delete mode 100644 src/python-api/api_expr.cc delete mode 100644 src/python-api/api_ila.cc delete mode 100644 src/python-api/api_log.cc delete mode 100644 src/python-api/ila_py_api.cc delete mode 100644 src/python-api/wrap_expr.cc delete mode 100644 src/python-api/wrap_ila.cc delete mode 100644 src/python-api/wrap_log.cc diff --git a/src/python-api/CMakeLists.txt b/src/python-api/CMakeLists.txt deleted file mode 100644 index e9f1a9fc1..000000000 --- a/src/python-api/CMakeLists.txt +++ /dev/null @@ -1,15 +0,0 @@ -# path = root/src/python-api - -file(GLOB ILAPY_SOURCES "${CMAKE_CURRENT_SOURCE_DIR}/*.cc") - -#set(ILA_TOOLS ila++) -#set(EXT_LIBRARIES ${Z3_LIBRARY} ${ILA_TOOLS}) - - -#add_library (ilapy "${ILAPY_SOURCES}") # Compile sources into a library. -#add_dependencies(ilapy ${ILA_TOOLS}) -#target_link_libraries (ilapy ${EXT_LIBRARIES} ${Boost_LIBRARIES}) - -add_library (ilapy ${ILAPY_SOURCES}) -target_link_libraries(ilapy ${ILANG_LIB_NAME}) - diff --git a/src/python-api/api_expr.cc b/src/python-api/api_expr.cc deleted file mode 100644 index c459ce3fb..000000000 --- a/src/python-api/api_expr.cc +++ /dev/null @@ -1,27 +0,0 @@ -/// \file -/// Source for Python API -- Expr - -#include -#include - -namespace ilang { -namespace pyapi { - -void export_expr() { - class_("Expr", init<>()) - .add_property("name", &ExprWrap::Name) - // unary operators - .def("__invert__", &ExprWrap::Complement, - return_value_policy()) - .def("__neg__", &ExprWrap::Negate, - return_value_policy()) - .def("__and__", &ExprWrap::And, return_value_policy()) - // TODO operator override - ; - - def("load", &ExprWrap::Load, return_value_policy()); - // TODO static functions -} - -} // namespace pyapi -} // namespace ilang diff --git a/src/python-api/api_ila.cc b/src/python-api/api_ila.cc deleted file mode 100644 index df12893b9..000000000 --- a/src/python-api/api_ila.cc +++ /dev/null @@ -1,22 +0,0 @@ -/// \file -/// Source for Python API -- ILA - -#include -#include - -namespace ilang { -namespace pyapi { - -void export_instr_lvl_abs() { - // Expose ILA wrapper to Boost.Python - class_("Abstraction", init()) - .def("inp", &InstrLvlAbsWrap::NewBvInput, - return_value_policy()) - .def("getinp", &InstrLvlAbsWrap::input, - return_value_policy()) - // TODO - ; -} - -} // namespace pyapi -} // namespace ilang diff --git a/src/python-api/api_log.cc b/src/python-api/api_log.cc deleted file mode 100644 index c45749db3..000000000 --- a/src/python-api/api_log.cc +++ /dev/null @@ -1,28 +0,0 @@ -/// \file -/// Source for Python API -- logging system - -#include -#include - -namespace ilang { -namespace pyapi { - -void export_log() { - // Initialize logging - - /// Set log level to the given value. - def("setLogLevel", SetLogLevel); - /// Set the path for log files. - def("setLogPath", SetLogPath); - /// Output all log to std err. - def("setToStdErr", SetToStdErr); - /// Turn on the debug log tag. - def("enablelog", EnableLog); - /// Turn off the debug log tag. - def("disablelog", DisableLog); - /// Turn off all the debug logs. - def("clearlogs", ClearLogs); -} - -} // namespace pyapi -} // namespace ilang diff --git a/src/python-api/ila_py_api.cc b/src/python-api/ila_py_api.cc deleted file mode 100644 index 763e088ea..000000000 --- a/src/python-api/ila_py_api.cc +++ /dev/null @@ -1,17 +0,0 @@ -/// \file -/// Source for Python API -- top level for all tools - -#include - -namespace ilang { -namespace pyapi { - -BOOST_PYTHON_MODULE(ila) { - export_log(); - export_expr(); - // export_instr(); - export_instr_lvl_abs(); -} - -} // namespace pyapi -} // namespace ilang diff --git a/src/python-api/wrap_expr.cc b/src/python-api/wrap_expr.cc deleted file mode 100644 index b2dd28400..000000000 --- a/src/python-api/wrap_expr.cc +++ /dev/null @@ -1,30 +0,0 @@ -/// \file -/// Source for wrapping Expr. - -#include - -namespace ilang { -namespace pyapi { - -const ExprPtr ExprWrap::get() const { return ptr_; } - -std::string ExprWrap::Name() const { return ptr_->name().str(); } - -ExprWrap* ExprWrap::Complement() const { - return new ExprWrap(ExprFuse::Complement(ptr_)); -} - -ExprWrap* ExprWrap::Negate() const { - return new ExprWrap(ExprFuse::Negate(ptr_)); -} - -ExprWrap* ExprWrap::And(ExprWrap* rhs) const { - return new ExprWrap(ExprFuse::And(ptr_, rhs->get())); -} - -ExprWrap* ExprWrap::Load(ExprWrap* mem, ExprWrap* addr) { - return new ExprWrap(ExprFuse::Load(mem->get(), addr->get())); -} - -} // namespace pyapi -} // namespace ilang diff --git a/src/python-api/wrap_ila.cc b/src/python-api/wrap_ila.cc deleted file mode 100644 index 28459fea9..000000000 --- a/src/python-api/wrap_ila.cc +++ /dev/null @@ -1,19 +0,0 @@ -/// \file -/// Source for wrapping ILA - -#include - -namespace ilang { -namespace pyapi { - -ExprWrap* InstrLvlAbsWrap::NewBvInput(const std::string& name, - const int& bit_width) { - return new ExprWrap(ptr_->NewBvInput(name, bit_width)); -} - -ExprWrap* InstrLvlAbsWrap::input(const std::string& name) { - return new ExprWrap(ptr_->input(name)); -} - -} // namespace pyapi -} // namespace ilang diff --git a/src/python-api/wrap_log.cc b/src/python-api/wrap_log.cc deleted file mode 100644 index 0011d5cbb..000000000 --- a/src/python-api/wrap_log.cc +++ /dev/null @@ -1,17 +0,0 @@ -/// \file -/// Source for wrapping logging system - -#include -#include - -namespace ilang { -namespace pyapi { - -void EnableLog(const std::string& tag) { DebugLog::Enable(tag); } - -void DisableLog(const std::string& tag) { DebugLog::Disable(tag); } - -void ClearLogs() { DebugLog::Clear(); } - -} // namespace pyapi -} // namespace ilang From 01d404537ba2052bbfa5cbc3db8a4470f5217a5f Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Fri, 2 Aug 2019 01:37:03 -0700 Subject: [PATCH 45/94] cleanup source - itsy --- src/target-itsy/interface.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/target-itsy/interface.cc b/src/target-itsy/interface.cc index fac0b1954..b65cdcb95 100644 --- a/src/target-itsy/interface.cc +++ b/src/target-itsy/interface.cc @@ -1,11 +1,11 @@ /// \file /// The implementation of the elevated synthesis engine interface. -#include #include #include +#include #include namespace ilang { From ace259fa53f2c80be52359767645e39b5299a1f4 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Fri, 2 Aug 2019 01:42:09 -0700 Subject: [PATCH 46/94] cleanup source - json --- src/target-json/ila_to_json_serializer.cc | 2 +- src/target-json/interface.cc | 3 ++- src/target-json/json_to_ila_deserializer.cc | 8 ++++---- 3 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/target-json/ila_to_json_serializer.cc b/src/target-json/ila_to_json_serializer.cc index 1e1948409..8a3f0e22e 100644 --- a/src/target-json/ila_to_json_serializer.cc +++ b/src/target-json/ila_to_json_serializer.cc @@ -2,9 +2,9 @@ /// The implementation of the ILA to JSON serializer. #include -#include #include +#include #include namespace ilang { diff --git a/src/target-json/interface.cc b/src/target-json/interface.cc index 4ca188c21..d8f779daf 100644 --- a/src/target-json/interface.cc +++ b/src/target-json/interface.cc @@ -1,10 +1,11 @@ /// \file /// The source for the ILA portable interface. +#include + #include #include -#include #include namespace ilang { diff --git a/src/target-json/json_to_ila_deserializer.cc b/src/target-json/json_to_ila_deserializer.cc index d9536881a..a4a586851 100644 --- a/src/target-json/json_to_ila_deserializer.cc +++ b/src/target-json/json_to_ila_deserializer.cc @@ -2,7 +2,6 @@ /// The implementation of the JSON to ILA deserializer. #include -#include #include #include @@ -10,6 +9,7 @@ #include #include +#include #include namespace ilang { @@ -327,7 +327,7 @@ ExprPtr J2IDes::DesExprOp(const unsigned& ast_expr_op_uid, } case AST_UID_EXPR_OP::SMOD: { return ExprFuse::SMod(args.at(0), args.at(1)); - } + } case AST_UID_EXPR_OP::MUL: { return ExprFuse::Mul(args.at(0), args.at(1)); } @@ -494,7 +494,7 @@ void J2IDes::DesIlaUnit(const json& j_ila) { ILA_WARN_IF(fetch_it == id_expr_map_.end()) << "Fetch not found"; m->SetFetch(fetch_it->second); } catch (...) { - ILA_WARN << "Fetch not defined"; + ILA_WARN << "Fetch not defined in " << m; } // valid @@ -505,7 +505,7 @@ void J2IDes::DesIlaUnit(const json& j_ila) { ILA_WARN_IF(valid_it == id_expr_map_.end()) << "Valid not found"; m->SetValid(valid_it->second); } catch (...) { - ILA_WARN << "Valid not defined"; + ILA_WARN << "Valid not defined in " << m; } // instructions From 7d07ca5bc3e6064195e7b799d856eff7f1f0ebb5 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Fri, 2 Aug 2019 21:29:36 -0700 Subject: [PATCH 47/94] Cleanup source - util --- src/util/fs.cc | 4 ++++ src/util/str_util.cc | 24 +++--------------------- 2 files changed, 7 insertions(+), 21 deletions(-) diff --git a/src/util/fs.cc b/src/util/fs.cc index 327ba0da5..4dae6c850 100644 --- a/src/util/fs.cc +++ b/src/util/fs.cc @@ -9,12 +9,16 @@ #include #if defined(_WIN32) || defined(_WIN64) + // windows #include + #else + // *nix #include #include + #endif #include diff --git a/src/util/str_util.cc b/src/util/str_util.cc index 3c34b1d95..2e224c532 100644 --- a/src/util/str_util.cc +++ b/src/util/str_util.cc @@ -1,11 +1,13 @@ /// \file /// Source for some utility functions for string formating. -#include #include + #include #include +#include + namespace ilang { std::string StrToUpper(const std::string& str) { @@ -14,14 +16,6 @@ std::string StrToUpper(const std::string& str) { return res; } -#if 0 -std::string StrToLower(const std::string& str) { - std::string res = str; - std::transform(res.begin(), res.end(), res.begin(), tolower); - return res; -} -#endif - bool StrToBool(const std::string& str) { std::string up = StrToUpper(str); ILA_ASSERT((up == "TRUE") || (up == "FALSE")) @@ -38,7 +32,6 @@ int StrToInt(const std::string& str, int base) { } } - std::vector Split(const std::string& str, const std::string& delim) { std::vector tokens; @@ -168,15 +161,4 @@ ReFindAndDo(const std::string& s, const std::string& re, bool IsRExprUsable() { return false; } #endif -#if 0 -std::string StrConcat(const std::string& l, const std::string& r) { - return (l + "_" + r); -} - -std::string StrConcat(const std::string& l, const std::string& m, - const std::string& r) { - return (l + "_" + m + "_" + r); -} -#endif - } // namespace ilang From 0e82a0f6fd8561f5a0c587eb1e63f58bd5d4a730 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Fri, 2 Aug 2019 21:41:32 -0700 Subject: [PATCH 48/94] Cleanup verif --- include/ilang/verification/abs_knob.h | 6 +-- include/ilang/verification/eq_check_crr.h | 6 +-- include/ilang/verification/legacy_bmc.h | 9 ++-- include/ilang/verification/rewrite_expr.h | 7 +-- include/ilang/verification/rewrite_ila.h | 6 +-- include/ilang/verification/unroller.h | 11 +++-- src/verification/abs_knob.cc | 4 +- src/verification/eq_check_crr.cc | 57 ++--------------------- src/verification/legacy_bmc.cc | 6 +-- src/verification/rewrite_expr.cc | 3 +- src/verification/rewrite_ila.cc | 3 +- src/verification/unroller.cc | 6 ++- 12 files changed, 42 insertions(+), 82 deletions(-) diff --git a/include/ilang/verification/abs_knob.h b/include/ilang/verification/abs_knob.h index 88cee3f12..5f2c50773 100644 --- a/include/ilang/verification/abs_knob.h +++ b/include/ilang/verification/abs_knob.h @@ -1,8 +1,8 @@ /// \file /// Header for a collection of ILA helpers. -#ifndef ABS_KNOB_H__ -#define ABS_KNOB_H__ +#ifndef ILANG_VERIFICATION_ABS_KNOB_H__ +#define ILANG_VERIFICATION_ABS_KNOB_H__ #include @@ -123,4 +123,4 @@ class AbsKnob { } // namespace ilang -#endif // ABS_KNOB_H__ +#endif // ILANG_VERIFICATION_ABS_KNOB_H__ diff --git a/include/ilang/verification/eq_check_crr.h b/include/ilang/verification/eq_check_crr.h index 5272f9868..40264651d 100644 --- a/include/ilang/verification/eq_check_crr.h +++ b/include/ilang/verification/eq_check_crr.h @@ -1,8 +1,8 @@ /// \file /// Header for generating verification condition for equivalence checking. -#ifndef EQ_CHECK_CRR_H__ -#define EQ_CHECK_CRR_H__ +#ifndef ILANG_VERIFICATION_EQ_CHECK_CRR_H__ +#define ILANG_VERIFICATION_EQ_CHECK_CRR_H__ #include "z3++.h" #include @@ -124,4 +124,4 @@ class CommDiag { } // namespace ilang -#endif // EQ_CHECK_CRR_H__ +#endif // ILANG_VERIFICATION_EQ_CHECK_CRR_H__ diff --git a/include/ilang/verification/legacy_bmc.h b/include/ilang/verification/legacy_bmc.h index 2c454e6b8..0690099c5 100644 --- a/include/ilang/verification/legacy_bmc.h +++ b/include/ilang/verification/legacy_bmc.h @@ -1,14 +1,15 @@ /// \file /// Header for bounded model checking -#ifndef LEGACY_BMC_H__ -#define LEGACY_BMC_H__ +#ifndef ILANG_VERIFICATION_LEGACY_BMC_H__ +#define ILANG_VERIFICATION_LEGACY_BMC_H__ + +#include #include "z3++.h" #include #include #include -#include /// \namespace ilang namespace ilang { @@ -78,4 +79,4 @@ class LegacyBmc { } // namespace ilang -#endif // LEGACY_BMC_H__ +#endif // ILANG_VERIFICATION_LEGACY_BMC_H__ diff --git a/include/ilang/verification/rewrite_expr.h b/include/ilang/verification/rewrite_expr.h index 668bc15db..bc65d879b 100644 --- a/include/ilang/verification/rewrite_expr.h +++ b/include/ilang/verification/rewrite_expr.h @@ -1,10 +1,11 @@ /// \file /// Header for function object for rewriting Expr. -#ifndef REWRITE_EXPR_H__ -#define REWRITE_EXPR_H__ +#ifndef ILANG_VERIFICATION_REWRITE_EXPR_H__ +#define ILANG_VERIFICATION_REWRITE_EXPR_H__ #include +#include namespace ilang { @@ -39,4 +40,4 @@ class FuncObjRewrExpr { } // namespace ilang -#endif // REWRITE_EXPR_H__ +#endif // ILANG_VERIFICATION_REWRITE_EXPR_H__ diff --git a/include/ilang/verification/rewrite_ila.h b/include/ilang/verification/rewrite_ila.h index f23b98a77..1307bc157 100644 --- a/include/ilang/verification/rewrite_ila.h +++ b/include/ilang/verification/rewrite_ila.h @@ -1,8 +1,8 @@ /// \file /// Header for function object for rewriting ILA. -#ifndef REWRITE_ILA_H__ -#define REWRITE_ILA_H__ +#ifndef ILANG_VERIFICATION_REWRITE_ILA_H__ +#define ILANG_VERIFICATION_REWRITE_ILA_H__ #include @@ -72,4 +72,4 @@ class FuncObjFlatIla { } // namespace ilang -#endif // REWRITE_ILA_H__ +#endif // ILANG_VERIFICATION_REWRITE_ILA_H__ diff --git a/include/ilang/verification/unroller.h b/include/ilang/verification/unroller.h index 8fd6e59dc..95a8f0ddd 100644 --- a/include/ilang/verification/unroller.h +++ b/include/ilang/verification/unroller.h @@ -1,14 +1,15 @@ /// \file /// Header for unrolling ILA execution. -#ifndef UNROLLER_H__ -#define UNROLLER_H__ +#ifndef ILANG_VERIFICATION_UNROLLER_H__ +#define ILANG_VERIFICATION_UNROLLER_H__ + +#include +#include #include "z3++.h" #include #include -#include -#include /// \namespace ilang namespace ilang { @@ -285,4 +286,4 @@ class MonoUnroll : public Unroller { } // namespace ilang -#endif // UNROLLER_H__ +#endif // ILANG_VERIFICATION_UNROLLER_H__ diff --git a/src/verification/abs_knob.cc b/src/verification/abs_knob.cc index 8a8a83368..bc8d69a22 100644 --- a/src/verification/abs_knob.cc +++ b/src/verification/abs_knob.cc @@ -1,9 +1,11 @@ /// \file /// Source for a collection of ILA helpers. +#include + #include + #include -#include #include #include diff --git a/src/verification/eq_check_crr.cc b/src/verification/eq_check_crr.cc index 805f7fd27..5b9ae7890 100644 --- a/src/verification/eq_check_crr.cc +++ b/src/verification/eq_check_crr.cc @@ -1,12 +1,14 @@ /// \file /// Source for generating verification condition for equivalecne checking. +#include + +#include + #include #include #include -#include #include -#include namespace ilang { @@ -368,37 +370,21 @@ bool CommDiag::IncEqCheck(const int& min, const int& max, const int& step) { auto tran = GetZ3IncUnrl(inc_unrl_old_a, crr_->refine_a(), i, step, stts_a); s.add(tran); - // auto tran = inc_unrl_old_a.MonoIncr(ma, step /*length*/, i /*base*/); - // auto mark = GetZ3IncUnrl(inc_unrl_old_a, crr_->refine_a(), i, - // stts_a); - // s.add(tran && mark); } if (num_new_a == i) { // need to unroll new step auto tran = GetZ3IncUnrl(inc_unrl_new_a, crr_->refine_a(), i, step, stts_a); s.add(tran); - // auto tran = inc_unrl_new_a.MonoIncr(ma, step /*length*/, i /*base*/); - // auto mark = GetZ3IncUnrl(inc_unrl_new_a, crr_->refine_a(), i, - // stts_a); - // s.add(tran && mark); } if (num_old_b == i) { // need to unroll new step auto tran = GetZ3IncUnrl(inc_unrl_old_b, crr_->refine_b(), i, step, stts_b); s.add(tran); - // auto tran = inc_unrl_old_b.MonoIncr(mb, step /*length*/, i /*base*/); - // auto mark = GetZ3IncUnrl(inc_unrl_old_b, crr_->refine_b(), i, - // stts_b); - // s.add(tran && mark); } if (num_new_b == i) { // need to unroll new step auto tran = GetZ3IncUnrl(inc_unrl_new_b, crr_->refine_b(), i, step, stts_b); s.add(tran); - // auto tran = inc_unrl_new_b.MonoIncr(mb, step /*length*/, i /*base*/); - // auto mark = GetZ3IncUnrl(inc_unrl_new_b, crr_->refine_b(), i, - // stts_b); - // s.add(tran && mark); } s.push(); // recording the current transition relation @@ -469,42 +455,18 @@ bool CommDiag::IncEqCheck(const int& min, const int& max, const int& step) { if (num_old_a == i) { // new step auto sufficient = CheckCmpl(s, cmpl_old_a); num_old_a = sufficient ? num_old_a : num_old_a + step; -#if 0 - if (sufficient) { - s.add(cmpl_old_a); - s.push(); - } -#endif } if (num_new_a == i) { // new step auto sufficient = CheckCmpl(s, cmpl_new_a); num_new_a = sufficient ? num_new_a : num_new_a + step; -#if 0 - if (sufficient) { - s.add(cmpl_new_a); - s.push(); - } -#endif } if (num_old_b == i) { // new step auto sufficient = CheckCmpl(s, cmpl_old_b); num_old_b = sufficient ? num_old_b : num_old_b + step; -#if 0 - if (sufficient) { - s.add(cmpl_old_b); - s.push(); - } -#endif } if (num_new_b == i) { // new step auto sufficient = CheckCmpl(s, cmpl_new_b); num_new_b = sufficient ? num_new_b : num_new_b + step; -#if 0 - if (sufficient) { - s.add(cmpl_new_b); - s.push(); - } -#endif } } @@ -809,19 +771,11 @@ z3::expr CommDiag::GetZ3IncUnrl(MonoUnroll& un, const RefPtr ref, } bool CommDiag::CheckCmpl(z3::solver& s, z3::expr& cmpl_expr) const { -#if 0 - s.push(); - s.add(cmpl_expr); - auto can_cmpl = (s.check() == z3::sat); - s.pop(); - -#endif s.push(); s.add(!cmpl_expr); auto must_cmpl = (s.check() == z3::unsat); s.pop(); - // return can_cmpl && must_cmpl; - //#if 0 + if (must_cmpl) { s.add(cmpl_expr); // added s.push(); // added @@ -829,7 +783,6 @@ bool CommDiag::CheckCmpl(z3::solver& s, z3::expr& cmpl_expr) const { } else { return false; } - //#endif } z3::expr CommDiag::GenAssm() { diff --git a/src/verification/legacy_bmc.cc b/src/verification/legacy_bmc.cc index c6f0ec07c..d7eab2278 100644 --- a/src/verification/legacy_bmc.cc +++ b/src/verification/legacy_bmc.cc @@ -1,9 +1,10 @@ /// \file /// Source for bounded model checking +#include + #include #include -#include namespace ilang { @@ -69,8 +70,6 @@ z3::check_result LegacyBmc::Check(InstrLvlAbsPtr m0, const int& k0, // initial condition for (size_t i = 0; i != inits_.size(); i++) { auto init_i = inits_[i]; - // ILA_ASSERT(init_i->host()) << "Legacy BMC can only have single-ILA - // init."; auto init_e = gen.GetExpr(init_i, suffix_init); solver.add(init_e); } @@ -78,7 +77,6 @@ z3::check_result LegacyBmc::Check(InstrLvlAbsPtr m0, const int& k0, // invariants for (size_t i = 0; i != invs_.size(); i++) { auto inv_i = invs_[i]; - // ILA_ASSERT(inv_i->host()) << "Legacy BMC can only have single-ILA inv."; // XXX Only apply invariants on initial states. auto inv_e = gen.GetExpr(inv_i, suffix_init); solver.add(inv_e); diff --git a/src/verification/rewrite_expr.cc b/src/verification/rewrite_expr.cc index 64bed8900..3616224bb 100644 --- a/src/verification/rewrite_expr.cc +++ b/src/verification/rewrite_expr.cc @@ -1,9 +1,10 @@ /// \file /// Source for function object for rewriting Expr. -#include #include +#include + namespace ilang { using namespace ExprFuse; diff --git a/src/verification/rewrite_ila.cc b/src/verification/rewrite_ila.cc index fe47e0609..5ccee4d92 100644 --- a/src/verification/rewrite_ila.cc +++ b/src/verification/rewrite_ila.cc @@ -1,9 +1,10 @@ /// \file /// Source for function object for rewriting ILA. +#include + #include #include -#include namespace ilang { diff --git a/src/verification/unroller.cc b/src/verification/unroller.cc index 86c53def6..5886bbf61 100644 --- a/src/verification/unroller.cc +++ b/src/verification/unroller.cc @@ -1,12 +1,14 @@ /// \file /// Source for unrolling ILA execution. -#include -#include #include + #include #include +#include +#include + namespace ilang { using namespace ExprFuse; From fa24074588a89a495d1bbd1b36c3d36c49df3d51 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Fri, 2 Aug 2019 21:48:29 -0700 Subject: [PATCH 49/94] Cleanup vlog related code --- src/verilog-in/verilog_analysis_wrapper.cc | 6 ++++-- src/vtarget-out/absmem.cc | 6 ++++-- src/vtarget-out/gen_util.cc | 19 +++++++------------ src/vtarget-out/single_target.cc | 11 ++++++----- src/vtarget-out/var_extract.cc | 6 ++++-- src/vtarget-out/vtarget_gen.cc | 3 ++- src/vtarget-out/vtarget_gen_cosa.cc | 8 +++++--- src/vtarget-out/vtarget_gen_jasper.cc | 8 +++++--- 8 files changed, 37 insertions(+), 30 deletions(-) diff --git a/src/verilog-in/verilog_analysis_wrapper.cc b/src/verilog-in/verilog_analysis_wrapper.cc index 90f0676fe..ddbe8c505 100644 --- a/src/verilog-in/verilog_analysis_wrapper.cc +++ b/src/verilog-in/verilog_analysis_wrapper.cc @@ -1,7 +1,9 @@ /// \file Verilog Wrapper Class -#include + #include +#include + namespace ilang { VerilogInfo::VerilogInfo(const path_vec_t& include_path, const path_vec_t& srcs, @@ -89,4 +91,4 @@ std::ostream& operator<<(std::ostream& os, return VerilogAnalyzerBase::PrintLoc(os, obj); } -}; // namespace ilang \ No newline at end of file +}; // namespace ilang diff --git a/src/vtarget-out/absmem.cc b/src/vtarget-out/absmem.cc index c0b2f80f1..76e3dcca1 100644 --- a/src/vtarget-out/absmem.cc +++ b/src/vtarget-out/absmem.cc @@ -1,11 +1,13 @@ /// \file Source for generating abstract memory // --- Hongce Zhang +#include + #include +#include + #include #include -#include -#include namespace ilang { diff --git a/src/vtarget-out/gen_util.cc b/src/vtarget-out/gen_util.cc index 861804210..3698e5c19 100644 --- a/src/vtarget-out/gen_util.cc +++ b/src/vtarget-out/gen_util.cc @@ -4,12 +4,14 @@ /// go in the same file and make it that long. // --- Hongce Zhang +#include + #include + #include #include #include #include -#include namespace ilang { @@ -112,16 +114,9 @@ bool VlgSglTgtGen::TryFindVlgState(const std::string& sname) { /// it is normal that you cannot find /// them in the verilog std::set wrapper_signals = { - "__START__", - "__IEND__", - "__ISSUE__", - "__STARTED__", - "__RESETED__", - "__ENDED__", - "__ENDFLUSH__", - "__FLUSHENDED__", - "__CYCLE_CNT__" -}; + "__START__", "__IEND__", "__ISSUE__", + "__STARTED__", "__RESETED__", "__ENDED__", + "__ENDFLUSH__", "__FLUSHENDED__", "__CYCLE_CNT__"}; // for ila state: add __ILA_SO_ // for verilog signal: keep as it is should be fine @@ -133,7 +128,7 @@ VlgSglTgtGen::ModifyCondExprAndRecordVlgName(const VarExtractor::token& t) { const auto& sname = t.second; if (token_tp == VarExtractor::token_type::UNKN_S) { - ILA_WARN_IF(!IN(sname,wrapper_signals)) + ILA_WARN_IF(!IN(sname, wrapper_signals)) << "In refinement relations: unknown reference to name:" << sname << " keep unchanged."; return sname; diff --git a/src/vtarget-out/single_target.cc b/src/vtarget-out/single_target.cc index db47e2620..e7096571c 100644 --- a/src/vtarget-out/single_target.cc +++ b/src/vtarget-out/single_target.cc @@ -2,17 +2,18 @@ /// // --- Hongce Zhang +#include + +#include +#include +#include + #include #include #include #include #include #include -#include - -#include -#include -#include namespace ilang { diff --git a/src/vtarget-out/var_extract.cc b/src/vtarget-out/var_extract.cc index f5aa8e029..222a1a663 100644 --- a/src/vtarget-out/var_extract.cc +++ b/src/vtarget-out/var_extract.cc @@ -4,10 +4,12 @@ /// and change their name if needed and generate a string // --- Hongce Zhang +#include + #include + #include #include -#include namespace ilang { @@ -168,4 +170,4 @@ void VarExtractor::ForEachTokenReplace(str_r replacer) { // Find the strings like this : -}; // namespace ilang \ No newline at end of file +}; // namespace ilang diff --git a/src/vtarget-out/vtarget_gen.cc b/src/vtarget-out/vtarget_gen.cc index 275f0b1a2..f45a4009b 100644 --- a/src/vtarget-out/vtarget_gen.cc +++ b/src/vtarget-out/vtarget_gen.cc @@ -2,10 +2,11 @@ /// This is used to avoid include json explicitly // --- Hongce Zhang -#include #include #include +#include + namespace ilang { VerilogVerificationTargetGenerator::VerilogVerificationTargetGenerator( diff --git a/src/vtarget-out/vtarget_gen_cosa.cc b/src/vtarget-out/vtarget_gen_cosa.cc index ff9fc2060..e9d009632 100644 --- a/src/vtarget-out/vtarget_gen_cosa.cc +++ b/src/vtarget-out/vtarget_gen_cosa.cc @@ -1,15 +1,17 @@ /// \file Source of generating CoSA accepted problem, vlg, mem, script // --- Hongce Zhang +#include + #include #include +#include + #include #include #include #include #include -#include -#include namespace ilang { @@ -316,4 +318,4 @@ void VlgSglTgtGen_Cosa::Export_modify_verilog() { } // Export_modify_verilog -}; // namespace ilang \ No newline at end of file +}; // namespace ilang diff --git a/src/vtarget-out/vtarget_gen_jasper.cc b/src/vtarget-out/vtarget_gen_jasper.cc index a71c51eb2..793275569 100644 --- a/src/vtarget-out/vtarget_gen_jasper.cc +++ b/src/vtarget-out/vtarget_gen_jasper.cc @@ -1,14 +1,16 @@ /// \file Source of generating Jasper accepted problem, vlg, mem, script // --- Hongce Zhang +#include + #include #include +#include + #include #include #include #include -#include -#include namespace ilang { @@ -167,4 +169,4 @@ void VlgSglTgtGen_Jasper::Export_modify_verilog() { } } -} // namespace ilang \ No newline at end of file +} // namespace ilang From 373d4cf8099ca82847f4d7cf6d3b4e8dafe2b02a Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Fri, 2 Aug 2019 21:51:17 -0700 Subject: [PATCH 50/94] Clean starter --- starter/CMakeLists.txt | 2 +- starter/app/main.cc | 5 +++-- starter/cmake/FindZ3.cmake | 11 ++++++----- starter/src/lib.cc | 6 ++++-- 4 files changed, 14 insertions(+), 10 deletions(-) diff --git a/starter/CMakeLists.txt b/starter/CMakeLists.txt index ff1d5a319..fc9a6b37e 100644 --- a/starter/CMakeLists.txt +++ b/starter/CMakeLists.txt @@ -1,4 +1,4 @@ -cmake_minimum_required(VERSION 3.8) +cmake_minimum_required(VERSION 3.9.6) # ---------------------------------------------------------------------------- # # PROJECT diff --git a/starter/app/main.cc b/starter/app/main.cc index 2cb8c6d62..a34edbd93 100644 --- a/starter/app/main.cc +++ b/starter/app/main.cc @@ -1,11 +1,12 @@ // main.cc // Synopsis: Entry point for the executable -#include #include +#include + int main() { - std::cout << "Hello World from executable main." << std::endl; + std::cout << "Hello World!!" << std::endl; Foo(); diff --git a/starter/cmake/FindZ3.cmake b/starter/cmake/FindZ3.cmake index f21c9ebaf..8182dbd2f 100644 --- a/starter/cmake/FindZ3.cmake +++ b/starter/cmake/FindZ3.cmake @@ -4,8 +4,8 @@ # This will define the following variables # # Z3_FOUND -# Z3_INCLUDE_DIRS -# Z3_LIBRARIES +# Z3_INCLUDE_DIR +# Z3_LIBRARY # Z3_VERSION # # and the following imported targets @@ -19,23 +19,24 @@ pkg_check_modules(PC_Z3 QUIET Z3) find_path(Z3_INCLUDE_DIR NAMES z3++.h HINTS ${PC_Z3_INCLUDEDIR} ${PC_Z3_INCLUDE_DIRS} - PATH_SUFFIXES z3 + PATH_SUFFIXES z3 Z3 ) find_library(Z3_LIBRARY NAMES z3 libz3 HINTS ${PC_Z3_LIBDIR} ${PC_Z3_LIBRARY_DIRS} - PATH_SUFFIXES z3 + PATH_SUFFIXES z3 Z3 ) find_program(Z3_EXEC NAMES z3 - PATH_SUFFIXES z3 + PATH_SUFFIXES z3 Z3 ) mark_as_advanced(Z3_FOUND Z3_INCLUDE_DIR Z3_LIBRARY Z3_EXEC) include(FindPackageHandleStandardArgs) + find_package_handle_standard_args(Z3 DEFAULT_MSG Z3_INCLUDE_DIR Z3_LIBRARY diff --git a/starter/src/lib.cc b/starter/src/lib.cc index 01d32fb95..c44b74ad3 100644 --- a/starter/src/lib.cc +++ b/starter/src/lib.cc @@ -1,10 +1,12 @@ // lib.cc // Synopsis: implementation of the library -#include -#include #include +#include + +#include + void Foo() { auto m = ilang::Ila("bar"); From 7abad8a5cb78acee3ba7192ef637b0f4e3361719 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 4 Aug 2019 16:44:03 -0700 Subject: [PATCH 51/94] Use ast uid for expr rewriting --- src/verification/rewrite_expr.cc | 108 ++++++++++++++++++++++++------- 1 file changed, 83 insertions(+), 25 deletions(-) diff --git a/src/verification/rewrite_expr.cc b/src/verification/rewrite_expr.cc index 3616224bb..2e6e7ed2c 100644 --- a/src/verification/rewrite_expr.cc +++ b/src/verification/rewrite_expr.cc @@ -3,6 +3,7 @@ #include +#include #include namespace ilang { @@ -33,103 +34,155 @@ ExprPtr FuncObjRewrExpr::Rewrite(const ExprPtr e) const { ExprPtr FuncObjRewrExpr::RewriteOp(const ExprPtr e) const { // check each type of op - if (std::dynamic_pointer_cast(e)) { // Negate + auto expr_op_uid = GetUidExprOp(e); + + switch (expr_op_uid) { + case AST_UID_EXPR_OP::NEG: { auto a = get(e->arg(0)); return Negate(a); - } else if (std::dynamic_pointer_cast(e)) { // Not + } + case AST_UID_EXPR_OP::NOT: { auto a = get(e->arg(0)); return Not(a); - } else if (std::dynamic_pointer_cast(e)) { // Complement + } + case AST_UID_EXPR_OP::COMPL: { auto a = get(e->arg(0)); return Complement(a); - } else if (std::dynamic_pointer_cast(e)) { // And + } + case AST_UID_EXPR_OP::AND: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return And(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Or + } + case AST_UID_EXPR_OP::OR: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Or(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Xor + } + case AST_UID_EXPR_OP::XOR: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Xor(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Shl + } + case AST_UID_EXPR_OP::SHL: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Shl(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Ashl + } + case AST_UID_EXPR_OP::ASHR: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Ashr(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Lshl + } + case AST_UID_EXPR_OP::LSHR: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Lshr(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Add + } + case AST_UID_EXPR_OP::ADD: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Add(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Sub + } + case AST_UID_EXPR_OP::SUB: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Sub(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Eq + } +#if 0 + case AST_UID_EXPR_OP::DIV: { + // TODO + } + case AST_UID_EXPR_OP::SREM: { + // TODO + } + case AST_UID_EXPR_OP::UREM: { + // TODO + } + case AST_UID_EXPR_OP::SMOD: { + // TODO + } + case AST_UID_EXPR_OP::MUL: { + // TODO + } +#endif + case AST_UID_EXPR_OP::EQ: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Eq(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Lt + } + case AST_UID_EXPR_OP::LT: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Lt(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Gt + } + case AST_UID_EXPR_OP::GT: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Gt(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Ult + } + case AST_UID_EXPR_OP::ULT: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Ult(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Ugt + } + case AST_UID_EXPR_OP::UGT: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Ugt(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Load + } + case AST_UID_EXPR_OP::LOAD: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Load(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Store + } + case AST_UID_EXPR_OP::STORE: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); auto a2 = get(e->arg(2)); return Store(a0, a1, a2); - } else if (std::dynamic_pointer_cast(e)) { // Concat + } + case AST_UID_EXPR_OP::CONCAT: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Concat(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Extract + } + case AST_UID_EXPR_OP::EXTRACT: { auto a0 = get(e->arg(0)); auto p0 = e->param(0); auto p1 = e->param(1); return Extract(a0, p0, p1); - } else if (std::dynamic_pointer_cast(e)) { // ZExt + } + case AST_UID_EXPR_OP::ZEXT: { auto a0 = get(e->arg(0)); auto p0 = e->param(0); return ZExt(a0, p0); - } else if (std::dynamic_pointer_cast(e)) { // SExt + } + case AST_UID_EXPR_OP::SEXT: { auto a0 = get(e->arg(0)); auto p0 = e->param(0); return SExt(a0, p0); - } else if (std::dynamic_pointer_cast(e)) { // Imply + } +#if 0 + case AST_UID_EXPR_OP::LROTATE: { + // TODO + } + case AST_UID_EXPR_OP::RROTATE: { + // TODO + } +#endif + case AST_UID_EXPR_OP::IMPLY: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); return Imply(a0, a1); - } else if (std::dynamic_pointer_cast(e)) { // Ite + } + case AST_UID_EXPR_OP::ITE: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); auto a2 = get(e->arg(2)); return Ite(a0, a1, a2); - } else { // AppFunc + } + case AST_UID_EXPR_OP::APP_FUNC: { auto e_derive = std::dynamic_pointer_cast(e); ILA_ASSERT(e_derive) << "Fail copying " << e; @@ -140,6 +193,11 @@ ExprPtr FuncObjRewrExpr::RewriteOp(const ExprPtr e) const { } return AppFunc(f, args); } + default: { + ILA_ERROR << "Rewriting " << expr_op_uid << " not implemented"; + return NULL; + } + }; } } // namespace ilang From 4032cac6c2bd0270529ca5d09dd7f27ab7a0cd4c Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 4 Aug 2019 16:44:47 -0700 Subject: [PATCH 52/94] Disable support for mem typed input --- src/target-itsy/abst_to_ila.cc | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/target-itsy/abst_to_ila.cc b/src/target-itsy/abst_to_ila.cc index bb141920d..d0107bbe7 100644 --- a/src/target-itsy/abst_to_ila.cc +++ b/src/target-itsy/abst_to_ila.cc @@ -112,9 +112,6 @@ void SynthAbsConverter::PortInputs(const ilasynth::Abstraction& abs, case ilasynth::NodeType::Type::BITVECTOR: ila->NewBvInput(name, type.bitWidth); break; - case ilasynth::NodeType::Type::MEM: - ila->NewMemInput(name, type.addrWidth, type.dataWidth); - break; default: ILA_ERROR << "Input of type " << type.type << " not supported."; break; From 8ced3f27e3223a52c1ccc0ce5186f3492cd6bb73 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 4 Aug 2019 16:57:10 -0700 Subject: [PATCH 53/94] Replace dynamic cast to static cast if the type is pre-defined --- src/ila/ast/expr_const.cc | 12 +++--------- src/ila/hash_ast.cc | 6 ++---- src/target-json/ila_to_json_serializer.cc | 4 ++-- src/verification/rewrite_expr.cc | 4 ++-- 4 files changed, 9 insertions(+), 17 deletions(-) diff --git a/src/ila/ast/expr_const.cc b/src/ila/ast/expr_const.cc index eb091457e..f06467472 100644 --- a/src/ila/ast/expr_const.cc +++ b/src/ila/ast/expr_const.cc @@ -75,23 +75,17 @@ std::ostream& ExprConst::Print(std::ostream& out) const { BoolValPtr ExprConst::val_bool() const { ILA_ASSERT(is_bool()) << "Not boolean constant"; - auto ptr = std::dynamic_pointer_cast(val_); - ILA_ASSERT(ptr) << "Fail casting to BoolVal"; - return ptr; + return std::static_pointer_cast(val_); } BvValPtr ExprConst::val_bv() const { ILA_ASSERT(is_bv()) << "Not bitvector constant"; - auto ptr = std::dynamic_pointer_cast(val_); - ILA_ASSERT(ptr) << "Fail casting to BvVal"; - return ptr; + return std::static_pointer_cast(val_); } MemValPtr ExprConst::val_mem() const { ILA_ASSERT(is_mem()) << "Not memory constatnc"; - auto ptr = std::dynamic_pointer_cast(val_); - ILA_ASSERT(ptr) << "Fail casting to MemVal"; - return ptr; + return std::static_pointer_cast(val_); } } // namespace ilang diff --git a/src/ila/hash_ast.cc b/src/ila/hash_ast.cc index 191bf8347..93598f239 100644 --- a/src/ila/hash_ast.cc +++ b/src/ila/hash_ast.cc @@ -59,8 +59,7 @@ static std::hash int_hash_fn; size_t ExprMngr::Hash(const ExprPtr n) const { if (n->is_op()) { // ExprOp - auto n_op = std::dynamic_pointer_cast(n); - ILA_ASSERT(n_op) << "Dynamic cast fail for ExprOp " << n; + auto n_op = std::static_pointer_cast(n); std::string op_name_str = n_op->op_name(); auto hash = str_hash_fn(op_name_str); @@ -76,8 +75,7 @@ size_t ExprMngr::Hash(const ExprPtr n) const { return n->name().id(); } else { // ExprConst ILA_ASSERT(n->is_const()) << "Unrecognized expr type"; - auto n_const = std::dynamic_pointer_cast(n); - ILA_ASSERT(n_const) << "Dynamic cast fail for ExprConst " << n; + auto n_const = std::static_pointer_cast(n); if (n_const->is_bool()) { return str_hash_fn(n_const->val_bool()->str()); diff --git a/src/target-json/ila_to_json_serializer.cc b/src/target-json/ila_to_json_serializer.cc index 8a3f0e22e..7e6a8852b 100644 --- a/src/target-json/ila_to_json_serializer.cc +++ b/src/target-json/ila_to_json_serializer.cc @@ -146,7 +146,7 @@ json I2JSer::SerFunc(const FuncPtr& i_func) { } json I2JSer::SerConstVal(const ExprPtr& i_expr) const { - auto i_expr_const = std::dynamic_pointer_cast(i_expr); + auto i_expr_const = std::static_pointer_cast(i_expr); ILA_NOT_NULL(i_expr_const); // create a new JSON object @@ -225,7 +225,7 @@ json I2JSer::SerExprUnit(const ExprPtr& i_expr) { // only for apply function if (expr_op_uid == AST_UID_EXPR_OP::APP_FUNC) { - auto i_expr_op_appfunc = std::dynamic_pointer_cast(i_expr); + auto i_expr_op_appfunc = std::static_pointer_cast(i_expr); ILA_NOT_NULL(i_expr_op_appfunc); auto j_func = SerFunc(i_expr_op_appfunc->func()); j_expr.emplace(SERDES_EXPR_FUNC, j_func.at(SERDES_FUNC_ID).get()); diff --git a/src/verification/rewrite_expr.cc b/src/verification/rewrite_expr.cc index 2e6e7ed2c..4f38d7498 100644 --- a/src/verification/rewrite_expr.cc +++ b/src/verification/rewrite_expr.cc @@ -183,8 +183,8 @@ ExprPtr FuncObjRewrExpr::RewriteOp(const ExprPtr e) const { return Ite(a0, a1, a2); } case AST_UID_EXPR_OP::APP_FUNC: { - auto e_derive = std::dynamic_pointer_cast(e); - ILA_ASSERT(e_derive) << "Fail copying " << e; + auto e_derive = std::static_pointer_cast(e); + ILA_NOT_NULL(e_derive); auto f = e_derive->func(); ExprPtrVec args; From 292f8bd37c94fa71da6852931311a277f46747ce Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 4 Aug 2019 17:20:27 -0700 Subject: [PATCH 54/94] Auto set fetch and valid if not found --- src/target-json/json_to_ila_deserializer.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/target-json/json_to_ila_deserializer.cc b/src/target-json/json_to_ila_deserializer.cc index a4a586851..7eec9035e 100644 --- a/src/target-json/json_to_ila_deserializer.cc +++ b/src/target-json/json_to_ila_deserializer.cc @@ -494,7 +494,7 @@ void J2IDes::DesIlaUnit(const json& j_ila) { ILA_WARN_IF(fetch_it == id_expr_map_.end()) << "Fetch not found"; m->SetFetch(fetch_it->second); } catch (...) { - ILA_WARN << "Fetch not defined in " << m; + m->SetFetch(ExprFuse::BvConst(1, 1)); } // valid @@ -505,7 +505,7 @@ void J2IDes::DesIlaUnit(const json& j_ila) { ILA_WARN_IF(valid_it == id_expr_map_.end()) << "Valid not found"; m->SetValid(valid_it->second); } catch (...) { - ILA_WARN << "Valid not defined in " << m; + m->SetValid(ExprFuse::BoolConst(true)); } // instructions From ca6aac99d3a4cc89aedb65e8bdc591a687a4dcb0 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 4 Aug 2019 17:20:54 -0700 Subject: [PATCH 55/94] Test validate model on GB-low, RBM, and OC8051 --- test/t_validate_model.cc | 45 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/test/t_validate_model.cc b/test/t_validate_model.cc index a9e2380fd..8005c9b82 100644 --- a/test/t_validate_model.cc +++ b/test/t_validate_model.cc @@ -86,4 +86,49 @@ TEST_F(TestValidateModel, complete_model_with_nondet_value) { EXPECT_TRUE(msg.empty()); } +TEST_F(TestValidateModel, case_gb) { + auto gb_dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, "gb"); + auto gb_file = os_portable_append_dir(gb_dir, "gb_low.json"); + auto gb = ImportIlaPortable(gb_file); + auto res = true; + + GET_STDERR_MSG(res = CheckCompleteness(gb.get()), msg); + EXPECT_FALSE(res); + EXPECT_FALSE(msg.empty()); + + CompleteModel(gb.get(), DEFAULT_UPDATE_METHOD::OLD_VALUE); + + GET_STDERR_MSG(res = CheckCompleteness(gb.get()), msg); + EXPECT_TRUE(res); + EXPECT_TRUE(msg.empty()); +} + +TEST_F(TestValidateModel, case_rbm) { + auto rbm_dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, "rbm"); + auto rbm_file = os_portable_append_dir(rbm_dir, "rbm.json"); + auto rbm = ImportIlaPortable(rbm_file); + auto res = true; + + GET_STDERR_MSG(res = CheckCompleteness(rbm.get()), msg); + EXPECT_FALSE(res); + EXPECT_FALSE(msg.empty()); + + CompleteModel(rbm.get(), DEFAULT_UPDATE_METHOD::OLD_VALUE); + + GET_STDERR_MSG(res = CheckCompleteness(rbm.get()), msg); + EXPECT_TRUE(res); + EXPECT_TRUE(msg.empty()); +} + +TEST_F(TestValidateModel, case_oc) { + auto oc_dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, "oc"); + auto oc_file = os_portable_append_dir(oc_dir, "oc.json"); + auto oc = ImportIlaPortable(oc_file); + auto res = true; + + GET_STDERR_MSG(res = CheckCompleteness(oc.get()), msg); + EXPECT_TRUE(res); + EXPECT_TRUE(msg.empty()); +} + } // namespace ilang From 9d2fd1ab5f784e1b89a05646fc8487dd55e96571 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 4 Aug 2019 18:40:05 -0700 Subject: [PATCH 56/94] add test for verilog generator on AES V/C, RBM, and OC8051 --- test/t_verilog_gen.cc | 116 ++++++++++++++++++++++++++++++++---------- 1 file changed, 90 insertions(+), 26 deletions(-) diff --git a/test/t_verilog_gen.cc b/test/t_verilog_gen.cc index 040a00b14..08bfc7dac 100644 --- a/test/t_verilog_gen.cc +++ b/test/t_verilog_gen.cc @@ -4,6 +4,9 @@ #include #include +#include +#include +#include #include #include #include @@ -29,7 +32,47 @@ void parseable(const std::string& fname, VerilogGenerator& vgen) { ILA_INFO << "ParseErrorFileName = " << fname; } +void ParseIla(const InstrLvlAbsPtr& ila) { + // test 1 gen all : internal mem + { + auto vgen = VerilogGenerator(); + vgen.ExportIla(ila); + + char tmp_file_template[] = "/tmp/vlog_XXXXXX"; + auto tmp_file_name = GetRandomFileName(tmp_file_template); + parseable(tmp_file_name, vgen); + } + // test 2 gen all : external mem + { + auto config = VerilogGenerator::VlgGenConfig( + true, VerilogGenerator::VlgGenConfig::funcOption::Internal); + auto vgen = VerilogGenerator(config); + vgen.ExportIla(ila); + + char tmp_file_template[] = "/tmp/vlog_ext_XXXXXX"; + auto tmp_file_name = GetRandomFileName(tmp_file_template); + parseable(tmp_file_name, vgen); + } +} + +void FlattenIla(const InstrLvlAbsPtr& ila) { + + for (auto i = 0; i < ila->instr_num(); i++) { + auto dep_ila = AbsKnob::ExtrDeptModl(ila->instr(i), "Flatten"); + AbsKnob::FlattenIla(dep_ila); + + auto vgen = VerilogGenerator(); + vgen.ExportIla(dep_ila); + + char tmp_file_template[] = "/tmp/vlog_flat_XXXXXX"; + auto tmp_file_name = GetRandomFileName(tmp_file_template); + ILA_INFO << tmp_file_name; + parseable(tmp_file_name, vgen); + } +} + TEST(TestVerilogGen, Init) { VerilogGenerator(); } + TEST(TestVerilogGen, ParseInst) { auto ila_ptr_ = SimpleCpu("proc"); // test 1 gen Add : internal mem @@ -87,37 +130,58 @@ TEST(TestVerilogGen, ParseInst) { } } // TEST (ParseInst) -TEST(TestVerilogGen, ParseIla) { - auto ila_ptr_ = SimpleCpu("proc"); - // test 1 gen all : internal mem - { - auto vgen = VerilogGenerator(); - vgen.ExportIla(ila_ptr_); - parseable(std::string(ILANG_TEST_BIN_ROOT) + "/t_proc_all.v", vgen); - } - // test 2 gen all : external mem - { - auto config = VerilogGenerator::VlgGenConfig( - true, VerilogGenerator::VlgGenConfig::funcOption::Internal); - auto vgen = VerilogGenerator(config); - vgen.ExportIla(ila_ptr_); - parseable(std::string(ILANG_TEST_BIN_ROOT) + "/t_proc_all_extmem.v", vgen); - } -} // TEST: ParseILA -TEST(TestVerilogGen, FlattenIla) { +TEST(TestVerilogGen, CpReg) { EqIlaGen ila_gen; - auto ila_ptr = ila_gen.GetIlaHier1("CpReg"); + auto ila = ila_gen.GetIlaHier1("CpReg"); + ParseIla(ila); + FlattenIla(ila); +} + +TEST(TestVerilogGen, SimpleProc) { + auto ila = SimpleCpu("proc"); + ParseIla(ila); + FlattenIla(ila); +} + +TEST(TestVerilogGen, AES_V) { + auto dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, "aes"); + auto file = os_portable_append_dir(dir, "aes_v.json"); + auto ila = ImportIlaPortable(file); + ParseIla(ila.get()); + FlattenIla(ila.get()); +} - auto dep_ila_ptr = - AbsKnob::ExtrDeptModl(ila_ptr->instr("instr1"), "FlattenCpReg"); - AbsKnob::FlattenIla(dep_ila_ptr); +TEST(TestVerilogGen, AES_C) { + auto dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, "aes"); + auto file = os_portable_append_dir(dir, "aes_c.json"); + auto ila = ImportIlaPortable(file); + ParseIla(ila.get()); + FlattenIla(ila.get()); +} - auto vgen = VerilogGenerator(); - vgen.ExportIla(dep_ila_ptr); +TEST(TestVerilogGen, GB_Low) { + auto dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, "gb"); + auto file = os_portable_append_dir(dir, "gb_low.json"); + auto ila = ImportIlaPortable(file); + ParseIla(ila.get()); + FlattenIla(ila.get()); +} - parseable(std::string(ILANG_TEST_BIN_ROOT) + "/t_proc_flatten.v", vgen); +TEST(TestVerilogGen, RBM) { + auto dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, "rbm"); + auto file = os_portable_append_dir(dir, "rbm.json"); + auto ila = ImportIlaPortable(file); + ParseIla(ila.get()); + FlattenIla(ila.get()); +} -} // TEST: FlattenILA +TEST(TestVerilogGen, OC) { + auto dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, "oc"); + auto file = os_portable_append_dir(dir, "oc.json"); + auto ila = ImportIlaPortable(file); + ParseIla(ila.get()); + FlattenIla(ila.get()); +} class T1 { friend class TestVerilogExport; From edd3724f8ae69def69bda02847ea60754d3c7776 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 4 Aug 2019 22:51:14 -0700 Subject: [PATCH 57/94] Intermediate commit for supporting Verilog export on OC8051 --- src/verilog-out/verilog_gen.cc | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/verilog-out/verilog_gen.cc b/src/verilog-out/verilog_gen.cc index 3c914a56d..d118a09e1 100644 --- a/src/verilog-out/verilog_gen.cc +++ b/src/verilog-out/verilog_gen.cc @@ -605,6 +605,25 @@ VerilogGenerator::translateBvOp(const std::shared_ptr& e) { else result_stmt = vlg_stmt_t(" { {") + toStr(outw - inw) + "{" + arg0 + "[" + toStr(inw - 1) + "] } }, " + arg0 + "} "; + } else if (op_name == "RIGHT_ROTATE") { + // {x[i-1:0], x[w-1:i]} + int rotw = e->param(0); + int inw = get_width(e->arg(0)); + if (rotw == 1) { + result_stmt = vlg_stmt_t(" { { ") + arg0 + "[0] }, { " + arg0 + "[ " + + toStr(inw - 1) + " : 1] } }"; + } else { + result_stmt = vlg_stmt_t(" { { ") + arg0 + "[ " + toStr(rotw - 1) + + " : 0 ] }, {" + arg0 + "[ " + toStr(inw - 1) + " : " + + toStr(rotw) + " ] } } "; + } + } else if (op_name == "LEFT_ROTATE") { + // {x[w-1-i:0], x[w-1:w-1-i]} + int rotw = e->param(0); + int inw = get_width(e->arg(0)); + result_stmt = vlg_stmt_t(" { { ") + arg0 + "[ " + toStr(inw - 1 - rotw) + + " : 0 ] }, { " + arg0 + "[ " + toStr(inw - 1) + " : " + + toStr(inw - 1 - rotw) + " ] } } "; } else ILA_ASSERT(false) << op_name << " is not supported by VerilogGenerator"; } // else if(arg_num == 1) @@ -630,6 +649,10 @@ VerilogGenerator::translateBvOp(const std::shared_ptr& e) { result_stmt = vlg_stmt_t(" ( ") + arg1 + " ) - ( " + arg2 + " ) "; else if (op_name == "MUL") result_stmt = vlg_stmt_t(" ( ") + arg1 + " ) * ( " + arg2 + " ) "; + else if (op_name == "DIV") + result_stmt = vlg_stmt_t(" ( ") + arg1 + " ) / ( " + arg2 + " ) "; + else if (op_name == "UREM") + result_stmt = vlg_stmt_t(" ( ") + arg1 + " ) % ( " + arg2 + " ) "; else if (op_name == "CONCAT") result_stmt = vlg_stmt_t(" { ( ") + arg1 + " ) , ( " + arg2 + " ) } "; else if (op_name == "LOAD") { From 8d36c5eb33efee39ae54f27681bcbf7ced6352e7 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 5 Aug 2019 00:26:17 -0700 Subject: [PATCH 58/94] Add more op in expr rewrite to support OC8051 --- src/verification/rewrite_expr.cc | 28 +++++++++++++++++++--------- 1 file changed, 19 insertions(+), 9 deletions(-) diff --git a/src/verification/rewrite_expr.cc b/src/verification/rewrite_expr.cc index 4f38d7498..59f012512 100644 --- a/src/verification/rewrite_expr.cc +++ b/src/verification/rewrite_expr.cc @@ -89,23 +89,31 @@ ExprPtr FuncObjRewrExpr::RewriteOp(const ExprPtr e) const { auto a1 = get(e->arg(1)); return Sub(a0, a1); } -#if 0 case AST_UID_EXPR_OP::DIV: { - // TODO + auto a0 = get(e->arg(0)); + auto a1 = get(e->arg(1)); + return Div(a0, a1); } +#if 0 case AST_UID_EXPR_OP::SREM: { // TODO } +#endif case AST_UID_EXPR_OP::UREM: { - // TODO + auto a0 = get(e->arg(0)); + auto a1 = get(e->arg(1)); + return URem(a0, a1); } +#if 0 case AST_UID_EXPR_OP::SMOD: { // TODO } +#endif case AST_UID_EXPR_OP::MUL: { - // TODO + auto a0 = get(e->arg(0)); + auto a1 = get(e->arg(1)); + return Mul(a0, a1); } -#endif case AST_UID_EXPR_OP::EQ: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); @@ -163,14 +171,16 @@ ExprPtr FuncObjRewrExpr::RewriteOp(const ExprPtr e) const { auto p0 = e->param(0); return SExt(a0, p0); } -#if 0 case AST_UID_EXPR_OP::LROTATE: { - // TODO + auto a0 = get(e->arg(0)); + auto p0 = e->param(0); + return LRotate(a0, p0); } case AST_UID_EXPR_OP::RROTATE: { - // TODO + auto a0 = get(e->arg(0)); + auto p0 = e->param(0); + return RRotate(a0, p0); } -#endif case AST_UID_EXPR_OP::IMPLY: { auto a0 = get(e->arg(0)); auto a1 = get(e->arg(1)); From 2cfade9e11396fa69ec4a88854ee38e19bbffef1 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 5 Aug 2019 22:40:39 -0700 Subject: [PATCH 59/94] Check in for updating vlog parser --- src/verilog-out/verilog_gen.cc | 27 +++++++++++++++------------ test/t_verilog_gen.cc | 4 +++- 2 files changed, 18 insertions(+), 13 deletions(-) diff --git a/src/verilog-out/verilog_gen.cc b/src/verilog-out/verilog_gen.cc index d118a09e1..09eb6625b 100644 --- a/src/verilog-out/verilog_gen.cc +++ b/src/verilog-out/verilog_gen.cc @@ -609,21 +609,24 @@ VerilogGenerator::translateBvOp(const std::shared_ptr& e) { // {x[i-1:0], x[w-1:i]} int rotw = e->param(0); int inw = get_width(e->arg(0)); - if (rotw == 1) { - result_stmt = vlg_stmt_t(" { { ") + arg0 + "[0] }, { " + arg0 + "[ " + - toStr(inw - 1) + " : 1] } }"; - } else { - result_stmt = vlg_stmt_t(" { { ") + arg0 + "[ " + toStr(rotw - 1) + - " : 0 ] }, {" + arg0 + "[ " + toStr(inw - 1) + " : " + - toStr(rotw) + " ] } } "; - } +#if 0 + result_stmt = vlg_stmt_t(" { ( ") + arg0 + "[" + toStr(rotw - 1) + + ":0] ), ( " + arg0 + "[" + toStr(inw - 1) + ":" + + toStr(rotw) + "] ) } "; +#endif + result_stmt = arg0; + ILA_INFO << result_stmt; } else if (op_name == "LEFT_ROTATE") { - // {x[w-1-i:0], x[w-1:w-1-i]} + // {x[w-1-i:0], x[w-1:w-i]} int rotw = e->param(0); int inw = get_width(e->arg(0)); - result_stmt = vlg_stmt_t(" { { ") + arg0 + "[ " + toStr(inw - 1 - rotw) + - " : 0 ] }, { " + arg0 + "[ " + toStr(inw - 1) + " : " + - toStr(inw - 1 - rotw) + " ] } } "; +#if 0 + result_stmt = vlg_stmt_t(" { ( ") + arg0 + "[" + toStr(inw - 1 - rotw) + + ":0] ), ( " + arg0 + "[" + toStr(inw - 1) + ":" + + toStr(inw - rotw) + "] ) } "; +#endif + result_stmt = arg0; + ILA_INFO << result_stmt; } else ILA_ASSERT(false) << op_name << " is not supported by VerilogGenerator"; } // else if(arg_num == 1) diff --git a/test/t_verilog_gen.cc b/test/t_verilog_gen.cc index 08bfc7dac..94530e361 100644 --- a/test/t_verilog_gen.cc +++ b/test/t_verilog_gen.cc @@ -35,6 +35,7 @@ void parseable(const std::string& fname, VerilogGenerator& vgen) { void ParseIla(const InstrLvlAbsPtr& ila) { // test 1 gen all : internal mem { + // SetToStdErr(true); auto vgen = VerilogGenerator(); vgen.ExportIla(ila); @@ -43,6 +44,7 @@ void ParseIla(const InstrLvlAbsPtr& ila) { parseable(tmp_file_name, vgen); } // test 2 gen all : external mem +#if 1 { auto config = VerilogGenerator::VlgGenConfig( true, VerilogGenerator::VlgGenConfig::funcOption::Internal); @@ -53,6 +55,7 @@ void ParseIla(const InstrLvlAbsPtr& ila) { auto tmp_file_name = GetRandomFileName(tmp_file_template); parseable(tmp_file_name, vgen); } +#endif } void FlattenIla(const InstrLvlAbsPtr& ila) { @@ -66,7 +69,6 @@ void FlattenIla(const InstrLvlAbsPtr& ila) { char tmp_file_template[] = "/tmp/vlog_flat_XXXXXX"; auto tmp_file_name = GetRandomFileName(tmp_file_template); - ILA_INFO << tmp_file_name; parseable(tmp_file_name, vgen); } } From f7978562e7578734f8810a719cd73c0d76619b77 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 5 Aug 2019 22:42:48 -0700 Subject: [PATCH 60/94] Update vlog parser --- extern/vlog-parser | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/extern/vlog-parser b/extern/vlog-parser index 40c8b8af4..544c00436 160000 --- a/extern/vlog-parser +++ b/extern/vlog-parser @@ -1 +1 @@ -Subproject commit 40c8b8af4a02b227410ead23497f29942432601b +Subproject commit 544c004363556a3c29c67305dc63e5aa21afa4c5 From f4e2e74ccc64584f1e9e4bc7cd7ea6b10dafde71 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 7 Aug 2019 00:37:25 -0700 Subject: [PATCH 61/94] Fix extend bug when extending constants --- src/verilog-out/verilog_gen.cc | 18 ++++++------------ test/t_verilog_gen.cc | 4 +--- 2 files changed, 7 insertions(+), 15 deletions(-) diff --git a/src/verilog-out/verilog_gen.cc b/src/verilog-out/verilog_gen.cc index 09eb6625b..bf2cebdd8 100644 --- a/src/verilog-out/verilog_gen.cc +++ b/src/verilog-out/verilog_gen.cc @@ -602,31 +602,26 @@ VerilogGenerator::translateBvOp(const std::shared_ptr& e) { int inw = get_width(e->arg(0)); if (outw == inw) result_stmt = arg0; - else + else if (e->arg(0)->is_const() && inw == 1) { + result_stmt = vlg_stmt_t(" { {") + toStr(outw - inw) + "{" + arg0 + + "} }, " + arg0 + "} "; + } else result_stmt = vlg_stmt_t(" { {") + toStr(outw - inw) + "{" + arg0 + - "[" + toStr(inw - 1) + "] } }, " + arg0 + "} "; + "[" + toStr(inw - 1) + "]} }, " + arg0 + "} "; } else if (op_name == "RIGHT_ROTATE") { // {x[i-1:0], x[w-1:i]} int rotw = e->param(0); int inw = get_width(e->arg(0)); -#if 0 result_stmt = vlg_stmt_t(" { ( ") + arg0 + "[" + toStr(rotw - 1) + ":0] ), ( " + arg0 + "[" + toStr(inw - 1) + ":" + toStr(rotw) + "] ) } "; -#endif - result_stmt = arg0; - ILA_INFO << result_stmt; } else if (op_name == "LEFT_ROTATE") { // {x[w-1-i:0], x[w-1:w-i]} int rotw = e->param(0); int inw = get_width(e->arg(0)); -#if 0 result_stmt = vlg_stmt_t(" { ( ") + arg0 + "[" + toStr(inw - 1 - rotw) + ":0] ), ( " + arg0 + "[" + toStr(inw - 1) + ":" + toStr(inw - rotw) + "] ) } "; -#endif - result_stmt = arg0; - ILA_INFO << result_stmt; } else ILA_ASSERT(false) << op_name << " is not supported by VerilogGenerator"; } // else if(arg_num == 1) @@ -690,8 +685,7 @@ VerilogGenerator::translateBvOp(const std::shared_ptr& e) { result_stmt = data_name; } // if( pos != mems_external.end() ) else { - result_stmt = - vlg_stmt_t(" ( ") + mem_var_name + " [ " + arg2 + " ] ) "; + result_stmt = vlg_stmt_t(" ( ") + mem_var_name + "[" + arg2 + "] ) "; ILA_DLOG("VerilogGen.translateBvOp") << "Not found."; } diff --git a/test/t_verilog_gen.cc b/test/t_verilog_gen.cc index 94530e361..729c92a0b 100644 --- a/test/t_verilog_gen.cc +++ b/test/t_verilog_gen.cc @@ -35,7 +35,7 @@ void parseable(const std::string& fname, VerilogGenerator& vgen) { void ParseIla(const InstrLvlAbsPtr& ila) { // test 1 gen all : internal mem { - // SetToStdErr(true); + SetLogLevel(2); auto vgen = VerilogGenerator(); vgen.ExportIla(ila); @@ -44,7 +44,6 @@ void ParseIla(const InstrLvlAbsPtr& ila) { parseable(tmp_file_name, vgen); } // test 2 gen all : external mem -#if 1 { auto config = VerilogGenerator::VlgGenConfig( true, VerilogGenerator::VlgGenConfig::funcOption::Internal); @@ -55,7 +54,6 @@ void ParseIla(const InstrLvlAbsPtr& ila) { auto tmp_file_name = GetRandomFileName(tmp_file_template); parseable(tmp_file_name, vgen); } -#endif } void FlattenIla(const InstrLvlAbsPtr& ila) { From d5f4d8bcfb7355568aa1dc60c0cd6b95523bc1b8 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 7 Aug 2019 01:04:43 -0700 Subject: [PATCH 62/94] Add test for copying ILA trees --- test/CMakeLists.txt | 1 + test/t_copy.cc | 47 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 48 insertions(+) create mode 100644 test/t_copy.cc diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 3f8054e87..76a79b741 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -49,6 +49,7 @@ package_add_test(${ILANG_TEST_MAIN} unit-src/util.cc t_api.cc t_case_aes_eq.cc + t_copy.cc t_crr.cc t_eq_check.cc t_expr.cc diff --git a/test/t_copy.cc b/test/t_copy.cc new file mode 100644 index 000000000..d11f258d1 --- /dev/null +++ b/test/t_copy.cc @@ -0,0 +1,47 @@ +/// \file +/// Unit tests for exporting and importing ILA portables. + +#include + +#include "unit-include/config.h" +#include "unit-include/util.h" +#include +#include +#include + +namespace ilang { + +void Check(InstrLvlAbsPtr& a, InstrLvlAbsPtr& b) { CheckIlaEqLegacy(a, b); } + +void Copy(const std::string& dir, const std::string& file, bool check = true) { + SetLogLevel(2); + auto file_dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, dir); + auto ila_file = os_portable_append_dir(file_dir, file); + auto ila = ImportIlaPortable(ila_file).get(); + + auto copy = AbsKnob::CopyIlaTree(ila, "copied"); + + if (check) { + Check(ila, copy); + } +} + +TEST(TestCopyTree, AES_V_TOP) { Copy("aes", "aes_v_top.json"); } + +TEST(TestCopyTree, AES_V_CHILD) { Copy("aes", "aes_v_child.json"); } + +TEST(TestCopyTree, AES_V) { Copy("aes", "aes_v.json"); } + +TEST(TestCopyTree, AES_C_TOP) { Copy("aes", "aes_c_top.json"); } + +TEST(TestCopyTree, AES_C_CHILD) { Copy("aes", "aes_c_child.json"); } + +TEST(TestCopyTree, AES_C) { Copy("aes", "aes_c.json"); } + +TEST(TestCopyTree, GB_LOW) { Copy("gb", "gb_low.json"); } + +TEST(TestCopyTree, RBM) { Copy("rbm", "rbm.json"); } + +TEST(TestCopyTree, OC8051) { Copy("oc", "oc.json", false); } + +} // namespace ilang From fee94f0747af9282904d3ba7b84d835b469edfe7 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 7 Aug 2019 01:05:02 -0700 Subject: [PATCH 63/94] fix typo --- test/t_portable.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/t_portable.cc b/test/t_portable.cc index 7994f81d2..44fd4fed0 100644 --- a/test/t_portable.cc +++ b/test/t_portable.cc @@ -16,8 +16,8 @@ void Check(Ila& a, Ila& b) { CheckIlaEqLegacy(a.get(), b.get()); } void SerDes(const std::string& dir, const std::string& file, bool check = true) { auto file_dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, dir); - auto aes_file = os_portable_append_dir(file_dir, file); - auto ila = ImportIlaPortable(aes_file); + auto ila_file = os_portable_append_dir(file_dir, file); + auto ila = ImportIlaPortable(ila_file); char tmp_file_template[] = "/tmp/ila_XXXXXX"; auto tmp_file_name = GetRandomFileName(tmp_file_template); From de5652530e9393a307f524f28aa1836fbfb5977c Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Fri, 9 Aug 2019 23:06:44 -0700 Subject: [PATCH 64/94] Fix typo --- src/verification/abs_knob.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/verification/abs_knob.cc b/src/verification/abs_knob.cc index bc8d69a22..117552630 100644 --- a/src/verification/abs_knob.cc +++ b/src/verification/abs_knob.cc @@ -276,7 +276,7 @@ InstrLvlAbsPtr AbsKnob::ExtrDeptModl(const InstrPtr instr, InstrLvlAbsPtr AbsKnob::CopyIlaTree(const InstrLvlAbsCnstPtr src, const std::string& dst_name) { ILA_NOT_NULL(src); - ILA_WARN_IF(!src->parent()) << "Copying non-root ILA " << src; + ILA_WARN_IF(src->parent()) << "Copying non-root ILA " << src; auto dst = InstrLvlAbs::New(dst_name); dst->set_spec(src->is_spec()); From 79b3f256381f9d36dea8c12b05ed28bcd5574c32 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 10 Aug 2019 14:34:52 -0700 Subject: [PATCH 65/94] Add out stream support for ptr of constant instr --- include/ilang/ila/instr.h | 6 +++++- src/ila/instr.cc | 4 ++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/include/ilang/ila/instr.h b/include/ilang/ila/instr.h index 976f543dc..9c19db9c3 100644 --- a/include/ilang/ila/instr.h +++ b/include/ilang/ila/instr.h @@ -25,6 +25,8 @@ class Instr : public Object { public: /// Pointer type for normal use of Instr. typedef std::shared_ptr InstrPtr; + /// Pointer type for read-only use of Instr. + typedef std::shared_ptr InstrCnstPtr; /// Type for a set of state names typedef std::set StateNameSet; /// Type for storing a set of Expr. @@ -107,6 +109,8 @@ class Instr : public Object { /// Overload output stream operator. friend std::ostream& operator<<(std::ostream& out, InstrPtr i); + /// Overload output stream operator for const object. + friend std::ostream& operator<<(std::ostream& out, InstrCnstPtr i); private: // ------------------------- MEMBERS -------------------------------------- // @@ -133,7 +137,7 @@ class Instr : public Object { /// Pointer type for normal use of Instr. typedef Instr::InstrPtr InstrPtr; /// Pointer type for read-only use of Instr. -typedef std::shared_ptr InstrCnstPtr; +typedef Instr::InstrCnstPtr InstrCnstPtr; /// Type for storing a set of Instr. typedef std::vector InstrVec; diff --git a/src/ila/instr.cc b/src/ila/instr.cc index 71f87ae30..58f283fd4 100644 --- a/src/ila/instr.cc +++ b/src/ila/instr.cc @@ -96,6 +96,10 @@ std::ostream& operator<<(std::ostream& out, InstrPtr i) { return i->Print(out); } +std::ostream& operator<<(std::ostream& out, InstrCnstPtr i) { + return i->Print(out); +} + ExprPtr Instr::Unify(const ExprPtr e) { return host_ ? host_->Unify(e) : e; } } // namespace ilang From d883d6486f9ffe1c05a06d4125a7d2da309cabf2 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 10 Aug 2019 14:35:24 -0700 Subject: [PATCH 66/94] Bug fix for rewriting/copying ILAs with multiple (>1) children --- src/verification/abs_knob.cc | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/src/verification/abs_knob.cc b/src/verification/abs_knob.cc index 117552630..a4ca243bc 100644 --- a/src/verification/abs_knob.cc +++ b/src/verification/abs_knob.cc @@ -190,15 +190,12 @@ void AbsKnob::RewriteInstr(const InstrCnstPtr src, const InstrPtr dst, dst->set_decode(d_dst); // update - for (auto it = expr_map.begin(); it != expr_map.end(); it++) { - // state - auto s_src = it->first; - auto s_dst = it->second; - // update function - auto u_src = src->update(s_src); - if (u_src) { - auto u_dst = AbsKnob::Rewrite(u_src, expr_map); - dst->set_update(s_dst, u_dst); + auto updated_states = src->updated_states(); + for (auto& state_name : updated_states) { + auto update_src = src->update(state_name); + if (update_src) { + auto update_dst = AbsKnob::Rewrite(update_src, expr_map); + dst->set_update(state_name, update_dst); } } } @@ -378,7 +375,7 @@ InstrPtr AbsKnob::DuplInstr(const InstrCnstPtr i_src, const InstrLvlAbsPtr dst, void AbsKnob::DuplInstrSeq(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst) { - ILA_WARN << "DuplInstrSeq not implemented yet."; + // ILA_WARN << "DuplInstrSeq not implemented yet."; // TODO } From b8ad7bdf7eaa4481f572b5e8bf364fd030858aa1 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 10 Aug 2019 14:45:41 -0700 Subject: [PATCH 67/94] Remove redundant file --- test/t_vtarget_gen_rf.cc | 0 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 test/t_vtarget_gen_rf.cc diff --git a/test/t_vtarget_gen_rf.cc b/test/t_vtarget_gen_rf.cc deleted file mode 100644 index e69de29bb..000000000 From 00a1bdaa6f24440f36724c79d89ac23b938d4295 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 11 Aug 2019 01:25:20 -0700 Subject: [PATCH 68/94] Warn for all cases --- test/unit-src/util.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/unit-src/util.cc b/test/unit-src/util.cc index 2d20f4702..b0c1aa71d 100644 --- a/test/unit-src/util.cc +++ b/test/unit-src/util.cc @@ -46,7 +46,7 @@ void CheckIlaEqLegacy(const InstrLvlAbsPtr& a, const InstrLvlAbsPtr& b) { state_mapping = ExprFuse::And(state_mapping, ExprFuse::Eq(var_org, var_des)); } catch (...) { - ILA_DLOG("Portable") << "Fail automatically matcing state vars"; + ILA_WARN << "Fail automatically matcing state vars"; } } From 02d58a54d03857d835d4427597f03e99a1ad8e63 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 12 Aug 2019 23:55:02 -0700 Subject: [PATCH 69/94] Start adding (auto) eq check helpers --- include/ilang/ila-handler/eq_check.h | 28 +++++++++++++++++ src/CMakeLists.txt | 1 + src/ila-handler/CMakeLists.txt | 7 +++++ src/ila-handler/eq_check.cc | 46 ++++++++++++++++++++++++++++ 4 files changed, 82 insertions(+) create mode 100644 include/ilang/ila-handler/eq_check.h create mode 100644 src/ila-handler/CMakeLists.txt create mode 100644 src/ila-handler/eq_check.cc diff --git a/include/ilang/ila-handler/eq_check.h b/include/ilang/ila-handler/eq_check.h new file mode 100644 index 000000000..8e240dcde --- /dev/null +++ b/include/ilang/ila-handler/eq_check.h @@ -0,0 +1,28 @@ +/// \file +/// The header for checking the equivalence of two ILAs. + +#ifndef ILANG_ILA_HANDLER_EQ_CHECK_H__ +#define ILANG_ILA_HANDLER_EQ_CHECK_H__ + +#include + +/// \namespace ilang +namespace ilang { + +/// \brief Check if two ILAs have an exact same architecture, i.e., at the +/// highest level of hierarchy. +/// \param[in] a first ILA. +/// \param[in] b second ILA. +/// \param[in] update check update if true. +bool CheckEqSameArch(const Ila& a, const Ila& b, bool update = true); + +/// \brief Check if two ILAs have an exact same micro-architecture. That is, +/// they have a same architecture at every level in the hierarchy. +/// \param[in] a first ILA. +/// \param[in] b second ILA. +/// \param[in] update check update if true. +bool CheckEqSameMicroArch(const Ila& a, const Ila& b, bool update = true); + +}; // namespace ilang + +#endif // ILANG_ILA_HANDLER_EQ_CHECK_H__ diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 24208531f..593f8d4ee 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -9,6 +9,7 @@ add_library(${PROJECT_NAME}::${ILANG_LIB_NAME} ALIAS ${ILANG_LIB_NAME}) ## source files ## add_subdirectory(ila) +add_subdirectory(ila-handler) add_subdirectory(mcm) add_subdirectory(target-json) add_subdirectory(target-sc) diff --git a/src/ila-handler/CMakeLists.txt b/src/ila-handler/CMakeLists.txt new file mode 100644 index 000000000..ab17907fe --- /dev/null +++ b/src/ila-handler/CMakeLists.txt @@ -0,0 +1,7 @@ +# ---------------------------------------------------------------------------- # +# source +# ---------------------------------------------------------------------------- # +target_sources(${ILANG_LIB_NAME} PRIVATE + ${CMAKE_CURRENT_SOURCE_DIR}/eq_check.cc +) + diff --git a/src/ila-handler/eq_check.cc b/src/ila-handler/eq_check.cc new file mode 100644 index 000000000..4657c7710 --- /dev/null +++ b/src/ila-handler/eq_check.cc @@ -0,0 +1,46 @@ +/// \file +/// The implementation for checking the equivalence of two ILAs. + +#include + +#include +#include + +namespace ilang { + +bool CheckEqSameMicroArch(const Ila& a, const Ila& b, bool update) { + auto ma = a.get(); + auto mb = b.get(); + + ILA_NOT_NULL(ma); + ILA_NOT_NULL(mb); + + if (ma->state_num() != mb->state_num()) { + ILA_INFO << "#state mismatch"; + return false; + } + + for (decltype(ma->state_num()) i = 0; i != ma->state_num(); i++) { + // for (auto i = 0; i != ma->state_num(); i++) { + // + } + + if (ma->input_num() != mb->input_num()) { + ILA_INFO << "#input mismatch"; + return false; + } + + if (ma->instr_num() != mb->instr_num()) { + ILA_INFO << "#instruction mismatch"; + return false; + } + + if (ma->child_num() != mb->child_num()) { + return false; + } + + return true; +} + +}; // namespace ilang + From 4c8a905fd609d198997a89594d2dd76c475dc231 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 14 Aug 2019 01:13:28 -0700 Subject: [PATCH 70/94] Add test for dev --- test/t_copy.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/test/t_copy.cc b/test/t_copy.cc index d11f258d1..ce67fb6d7 100644 --- a/test/t_copy.cc +++ b/test/t_copy.cc @@ -5,6 +5,7 @@ #include "unit-include/config.h" #include "unit-include/util.h" +#include #include #include #include @@ -14,7 +15,7 @@ namespace ilang { void Check(InstrLvlAbsPtr& a, InstrLvlAbsPtr& b) { CheckIlaEqLegacy(a, b); } void Copy(const std::string& dir, const std::string& file, bool check = true) { - SetLogLevel(2); + SetLogLevel(0); auto file_dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, dir); auto ila_file = os_portable_append_dir(file_dir, file); auto ila = ImportIlaPortable(ila_file).get(); @@ -24,6 +25,8 @@ void Copy(const std::string& dir, const std::string& file, bool check = true) { if (check) { Check(ila, copy); } + + EXPECT_TRUE(CheckEqSameMicroArch(ila, copy, check)); } TEST(TestCopyTree, AES_V_TOP) { Copy("aes", "aes_v_top.json"); } From 9f2b653a645f83ee5aaf2bf9bc9cc72169f0e6bb Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Fri, 13 Sep 2019 10:42:40 -0400 Subject: [PATCH 71/94] Wrap the string buffer allocation with basic string --- include/ilang/verilog-in/vlog_parser_util.h | 23 +++++++++++ src/verilog-in/CMakeLists.txt | 1 + src/verilog-in/verilog_analysis.cc | 44 ++++++++++----------- src/verilog-in/vlog_parser_util.cc | 21 ++++++++++ 4 files changed, 67 insertions(+), 22 deletions(-) create mode 100644 include/ilang/verilog-in/vlog_parser_util.h create mode 100644 src/verilog-in/vlog_parser_util.cc diff --git a/include/ilang/verilog-in/vlog_parser_util.h b/include/ilang/verilog-in/vlog_parser_util.h new file mode 100644 index 000000000..30f395b9e --- /dev/null +++ b/include/ilang/verilog-in/vlog_parser_util.h @@ -0,0 +1,23 @@ +/// \file Header of Verilog parser utils +/// +/// To provide utils and wrappers for the external Verilog parser. +/// - resource-leak-free string translation of ast id + +#ifndef ILANG_VERILOG_IN_VLOG_PARSER_UTIL_H__ +#define ILANG_VERILOG_IN_VLOG_PARSER_UTIL_H__ + +extern "C" { +#include +} + +#include + +/// \namespace ilang +namespace ilang { + +/// A wrapper of the ast_identifier_tostring method with basic string type. +std::string _ast_identifier_tostring(ast_identifier id); + +}; // namespace ilang + +#endif // ILANG_VERILOG_IN_VLOG_PARSER_UTIL_H__ diff --git a/src/verilog-in/CMakeLists.txt b/src/verilog-in/CMakeLists.txt index 104803aa1..9280e50e1 100644 --- a/src/verilog-in/CMakeLists.txt +++ b/src/verilog-in/CMakeLists.txt @@ -6,5 +6,6 @@ target_sources(${ILANG_LIB_NAME} PRIVATE ${CMAKE_CURRENT_SOURCE_DIR}/verilog_analysis.cc ${CMAKE_CURRENT_SOURCE_DIR}/verilog_const_parser.cc ${CMAKE_CURRENT_SOURCE_DIR}/verilog_analysis_wrapper.cc + ${CMAKE_CURRENT_SOURCE_DIR}/vlog_parser_util.cc ) diff --git a/src/verilog-in/verilog_analysis.cc b/src/verilog-in/verilog_analysis.cc index db4d57009..d82a1077b 100644 --- a/src/verilog-in/verilog_analysis.cc +++ b/src/verilog-in/verilog_analysis.cc @@ -10,6 +10,7 @@ #include #include #include +#include // extern int yy_flex_debug; extern int yydebug; @@ -70,7 +71,7 @@ VerilogAnalyzer::VerilogAnalyzer(const path_vec_t& include_path, const std::string& optional_top_module) : vlg_include_path(include_path), vlg_src_files(srcs), top_inst_name(top_module_inst_name), _bad_state(false) { -//yydebug = 1; + // yydebug = 1; instance_count++; if (instance_count != 1) { _bad_state = true; @@ -147,7 +148,7 @@ void VerilogAnalyzer::check_resolve_modules(verilog_source_tree* source) { ILA_NOT_NULL(module->identifier); // otherwise it is the parser bug - std::string mod_name(ast_identifier_tostring(module->identifier)); + auto mod_name = _ast_identifier_tostring(module->identifier); if (IN(mod_name, name_module_map)) { // the module has been encountered, redefinition std::stringstream outinfo; @@ -173,7 +174,7 @@ void VerilogAnalyzer::check_resolve_modules(verilog_source_tree* source) { if (submod->resolved) { // Do Nothing } else ILA_WARN << "Verilog module " - << ast_identifier_tostring(submod->module_identifer) + << _ast_identifier_tostring(submod->module_identifer) << "'s definition is not found."; } } @@ -198,10 +199,10 @@ void VerilogAnalyzer::create_module_submodule_map(verilog_source_tree* source) { (ast_module_instantiation*)ast_list_get_not_null( module_ast_ptr->module_instantiations, sm); - std::string submod_name( + auto submod_name = submod->resolved - ? ast_identifier_tostring(submod->declaration->identifier) - : ast_identifier_tostring(submod->module_identifer)); + ? _ast_identifier_tostring(submod->declaration->identifier) + : _ast_identifier_tostring(submod->module_identifer); // get the instance names for (unsigned int si = 0; si < submod->module_instances->items; si++) { @@ -209,8 +210,8 @@ void VerilogAnalyzer::create_module_submodule_map(verilog_source_tree* source) { (ast_module_instance*)ast_list_get_not_null( submod->module_instances, si); ILA_NOT_NULL(submod_inst); - std::string submod_name_inst( - ast_identifier_tostring(submod_inst->instance_identifier)); + auto submod_name_inst = + _ast_identifier_tostring(submod_inst->instance_identifier); modules_to_submodules_map[name].insert({submod_name_inst, submod_name}); modules_to_submodule_inst_ast_map[name].insert( {submod_name_inst, submod}); @@ -235,10 +236,10 @@ void VerilogAnalyzer::find_top_module(verilog_source_tree* source, (ast_module_instantiation*)ast_list_get_not_null( module_ast_ptr->module_instantiations, sm); - std::string submod_name( + auto submod_name = submod->resolved - ? ast_identifier_tostring(submod->declaration->identifier) - : ast_identifier_tostring(submod->module_identifer)); + ? _ast_identifier_tostring(submod->declaration->identifier) + : _ast_identifier_tostring(submod->module_identifer); module_to_whereuses_map[submod_name].push_back(name); } @@ -369,7 +370,7 @@ VerilogAnalyzer::_check_hierarchical_name_type( // if (port_id_ptr->) ILA_NOT_NULL(port_id_ptr); ILA_NOT_NULL(port_id_ptr->identifier); - std::string port_name(ast_identifier_tostring(port_id_ptr)); + auto port_name = _ast_identifier_tostring(port_id_ptr); ILA_ASSERT(port_name != "") << "Get an empty port name from the verilog parser"; if (port_name == last_level_name) { @@ -400,7 +401,7 @@ VerilogAnalyzer::_check_hierarchical_name_type( ast_reg_declaration* reg_decl_ptr = (ast_reg_declaration*)ast_list_get_not_null( mod_ast_ptr->reg_declarations, reg_decl_idx); - if (ast_identifier_tostring(reg_decl_ptr->identifier) == last_level_name) { + if (_ast_identifier_tostring(reg_decl_ptr->identifier) == last_level_name) { // now we know it is reg! if (internalDef) { std::stringstream outbuf; @@ -421,7 +422,7 @@ VerilogAnalyzer::_check_hierarchical_name_type( ast_net_declaration* net_decl_ptr = (ast_net_declaration*)ast_list_get_not_null( mod_ast_ptr->net_declarations, net_decl_idx); - if (ast_identifier_tostring(net_decl_ptr->identifier) == last_level_name) { + if (_ast_identifier_tostring(net_decl_ptr->identifier) == last_level_name) { // now we know it is net! if (internalDef) { if (isReg) { @@ -544,8 +545,8 @@ VerilogAnalyzer::get_module_inst_loc(const std::string& inst_name) const { if (level_names.size() == 1) { // already matched (so, we don't compare again) o.w. return above name_decl_buffer[inst_name] = GetMap(name_module_map, top_module_name); - ILA_ERROR - << "Top module has no instance! Use the declaration location instead."; + ILA_ERROR << "Top module has no instance! Use the declaration location " + "instead."; return name2loc(inst_name); } @@ -587,8 +588,8 @@ VerilogAnalyzer::get_module_inst_loc(const std::string& inst_name) const { ast_module_instance* submod_inst = (ast_module_instance*)ast_list_get_not_null(submod->module_instances, smi); - std::string submod_name_inst( - ast_identifier_tostring(submod_inst->instance_identifier)); + auto submod_name_inst = + _ast_identifier_tostring(submod_inst->instance_identifier); if (submod_name_inst == last_level_name) return Meta2Loc(submod_inst->instance_identifier->meta); } // for each instance in the instantiation @@ -693,8 +694,8 @@ VerilogAnalyzer::module_io_vec_t VerilogAnalyzer::get_top_module_io() const { void* ptr_from_list_ = ast_list_get_not_null(port_ptr->port_names, name_idx); ast_identifier port_id_ptr; - if (! port_ptr - ->is_list_id) { // in this case, it is not a list of ast_identifier + if (!port_ptr->is_list_id) { // in this case, it is not a list of + // ast_identifier // but a list of ast_single_assignment(ast_new_lvalue_id) ast_single_assignment* asm_ptr = (ast_single_assignment*)ptr_from_list_; ILA_ASSERT(asm_ptr->lval->type == ast_lvalue_type_e::NET_IDENTIFIER || @@ -703,8 +704,7 @@ VerilogAnalyzer::module_io_vec_t VerilogAnalyzer::get_top_module_io() const { } else port_id_ptr = (ast_identifier)ptr_from_list_; - std::string short_name = - std::string(ast_identifier_tostring(port_id_ptr)); + auto short_name = _ast_identifier_tostring(port_id_ptr); std::string port_name = top_inst_name + "." + short_name; auto tp_ = check_hierarchical_name_type(port_name); diff --git a/src/verilog-in/vlog_parser_util.cc b/src/verilog-in/vlog_parser_util.cc new file mode 100644 index 000000000..5f7ae86fe --- /dev/null +++ b/src/verilog-in/vlog_parser_util.cc @@ -0,0 +1,21 @@ +/// \file Source of Verilog parser utils +/// + +#include + +namespace ilang { + +std::string _ast_identifier_tostring(ast_identifier id) { + std::string tr_str(ast_strdup(id->identifier)); + + ast_identifier walker = id; + + while (walker->next != NULL) { + walker = walker->next; + tr_str += walker->identifier; + } + + return tr_str; +} + +}; // namespace ilang From 491565b4cd1d12b1676fa348ef352d23bcd0da09 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Fri, 13 Sep 2019 08:15:38 -0700 Subject: [PATCH 72/94] Intermediate commit before merging with the upstream --- src/ila-handler/eq_check.cc | 53 +++++++++++++++++++++++++++++++++---- 1 file changed, 48 insertions(+), 5 deletions(-) diff --git a/src/ila-handler/eq_check.cc b/src/ila-handler/eq_check.cc index 4657c7710..1126c4e85 100644 --- a/src/ila-handler/eq_check.cc +++ b/src/ila-handler/eq_check.cc @@ -3,8 +3,10 @@ #include +#include #include #include +#include namespace ilang { @@ -20,11 +22,6 @@ bool CheckEqSameMicroArch(const Ila& a, const Ila& b, bool update) { return false; } - for (decltype(ma->state_num()) i = 0; i != ma->state_num(); i++) { - // for (auto i = 0; i != ma->state_num(); i++) { - // - } - if (ma->input_num() != mb->input_num()) { ILA_INFO << "#input mismatch"; return false; @@ -35,6 +32,52 @@ bool CheckEqSameMicroArch(const Ila& a, const Ila& b, bool update) { return false; } + auto relation = RelationMap::New(); + + for (decltype(ma->input_num()) i = 0; i != ma->input_num(); i++) { + auto inp_a = ma->input(i); + auto inp_b = mb->input(inp_a->name().str()); + if (inp_b && (inp_a->sort() == inp_b->sort())) { + relation->add(ExprFuse::Eq(inp_a, inp_b)); + } else { + ILA_INFO << "No corresponding input " << inp_a << " found"; + return false; + } + } + + for (decltype(ma->state_num()) i = 0; i != ma->state_num(); i++) { + auto var_a = ma->state(i); + auto var_b = mb->state(var_a->name().str()); + if (var_b && (var_a->sort() == var_b->sort())) { + relation->add(ExprFuse::Eq(var_a, var_b)); + } else { + ILA_INFO << "No corresponding state var " << var_a << " found"; + return false; + } + } + + auto refinement_a = NULL; + auto refinement_b = NULL; + + auto GetFlatRefinement = [=](InstrLvlAbsPtr m, InstrPtr instr) { + // target + auto ref = RefinementMap::New(); + ref->set_tgt(instr); + + // apply + ref->set_appl(instr->decode()); + + // flush + auto has_instr = ExprFuse::BoolConst(false); + for (auto i = 0; i < m->instr_num(); i++) { + has_instr = ExprFuse::Or(has_instr, m->instr(i)->decode()); + } + ref->set_flush(ExprFuse::Not(has_instr)); + + // ready + // fix bound 1? + }; + if (ma->child_num() != mb->child_num()) { return false; } From 90436cdaadea0ccd85a81bd1e3001ab23e04cc63 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Fri, 13 Sep 2019 12:45:18 -0700 Subject: [PATCH 73/94] Add a placeholder for static analysis model to avoid resource leak false positive --- .travis.yml | 2 +- CMakeLists.txt | 1 + include/ilang/verilog-in/vlog_parser_util.h | 2 +- src/CMakeLists.txt | 8 ++++++++ src/config.h.in | 2 ++ src/verilog-in/vlog_parser_util.cc | 20 ++++++++++++-------- 6 files changed, 25 insertions(+), 10 deletions(-) diff --git a/.travis.yml b/.travis.yml index 53543dd26..558be1984 100644 --- a/.travis.yml +++ b/.travis.yml @@ -78,7 +78,7 @@ matrix: name: "Bo-Yuan-Huang/ILAng" description: "A modeling and verification platform for SoCs" notification_email: byhuang1992@gmail.com - build_command_prepend: "cd $TRAVIS_BUILD_DIR && mkdir -p build && cd build && cmake .. -DILANG_BUILD_TEST=OFF -DCMAKE_PREFIX_PATH=$TRAVIS_BUILD_DIR/local" + build_command_prepend: "cd $TRAVIS_BUILD_DIR && mkdir -p build && cd build && cmake .. -DILANG_BUILD_TEST=OFF -DCMAKE_PREFIX_PATH=$TRAVIS_BUILD_DIR/local -DILANG_STATIC_ANALYSIS=ON" build_command: "make" branch_pattern: coverity_scan apt: diff --git a/CMakeLists.txt b/CMakeLists.txt index 072fb8922..e774142a6 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -25,6 +25,7 @@ option(ILANG_BUILD_DOCS "Build documentations." OFF) option(ILANG_BUILD_SYNTH "Build the synthesis engine." ON) option(ILANG_INSTALL_DEV "Install dev features." OFF) option(ILANG_EXPORT_PACKAGE "Export CMake package if enabled." OFF) +option(ILANG_STATIC_ANALYSIS "Build for static analysis." OFF) option(BUILD_SHARED_LIBS "Build shared libraries." ON) include(CMakeDependentOption) diff --git a/include/ilang/verilog-in/vlog_parser_util.h b/include/ilang/verilog-in/vlog_parser_util.h index 30f395b9e..0b55c2002 100644 --- a/include/ilang/verilog-in/vlog_parser_util.h +++ b/include/ilang/verilog-in/vlog_parser_util.h @@ -1,7 +1,7 @@ /// \file Header of Verilog parser utils /// /// To provide utils and wrappers for the external Verilog parser. -/// - resource-leak-free string translation of ast id +/// - placeholder for static analysis model (resource leak false positive) #ifndef ILANG_VERILOG_IN_VLOG_PARSER_UTIL_H__ #define ILANG_VERILOG_IN_VLOG_PARSER_UTIL_H__ diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 593f8d4ee..ddafa8b8f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -139,6 +139,14 @@ else() set(SYNTH_INTERFACE FALSE) endif() +## +## static analysis only +## +if(${ILANG_STATIC_ANALYSIS}) + set(STATIC_ANALYSIS TRUE) +else() + set(STATIC_ANALYSIS FALSE) +endif() # ---------------------------------------------------------------------------- # # INSTALL diff --git a/src/config.h.in b/src/config.h.in index 50fb55031..31ba312b1 100644 --- a/src/config.h.in +++ b/src/config.h.in @@ -10,5 +10,7 @@ #cmakedefine SYNTH_INTERFACE +#cmakedefine STATIC_ANALYSIS + #endif // CONFIG_CMAKE_DEFINE_H__ diff --git a/src/verilog-in/vlog_parser_util.cc b/src/verilog-in/vlog_parser_util.cc index 5f7ae86fe..7326bfbda 100644 --- a/src/verilog-in/vlog_parser_util.cc +++ b/src/verilog-in/vlog_parser_util.cc @@ -3,19 +3,23 @@ #include +#include + namespace ilang { -std::string _ast_identifier_tostring(ast_identifier id) { - std::string tr_str(ast_strdup(id->identifier)); +#ifdef STATIC_ANALYSIS +extern void _static_analysis_only_free(char* x); +#endif - ast_identifier walker = id; +std::string _ast_identifier_tostring(ast_identifier id) { + auto id_cptr = ast_identifier_tostring(id); + auto id_bstr = static_cast(id_cptr); - while (walker->next != NULL) { - walker = walker->next; - tr_str += walker->identifier; - } +#ifdef STATIC_ANALYSIS + _static_analysis_only_free(id_cptr); +#endif - return tr_str; + return id_bstr; } }; // namespace ilang From cab4a46aee6c6a42478ddb1f69e0fe2d4804e4c8 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 14 Sep 2019 13:13:16 -0700 Subject: [PATCH 74/94] Rename coverity flag and FP reducing workaround --- .travis.yml | 2 +- CMakeLists.txt | 2 +- src/CMakeLists.txt | 6 +++--- src/config.h.in | 2 +- src/verilog-in/vlog_parser_util.cc | 9 +++------ 5 files changed, 9 insertions(+), 12 deletions(-) diff --git a/.travis.yml b/.travis.yml index 558be1984..f85d19e53 100644 --- a/.travis.yml +++ b/.travis.yml @@ -78,7 +78,7 @@ matrix: name: "Bo-Yuan-Huang/ILAng" description: "A modeling and verification platform for SoCs" notification_email: byhuang1992@gmail.com - build_command_prepend: "cd $TRAVIS_BUILD_DIR && mkdir -p build && cd build && cmake .. -DILANG_BUILD_TEST=OFF -DCMAKE_PREFIX_PATH=$TRAVIS_BUILD_DIR/local -DILANG_STATIC_ANALYSIS=ON" + build_command_prepend: "cd $TRAVIS_BUILD_DIR && mkdir -p build && cd build && cmake .. -DILANG_BUILD_TEST=OFF -DCMAKE_PREFIX_PATH=$TRAVIS_BUILD_DIR/local -DILANG_COVERITY=ON" build_command: "make" branch_pattern: coverity_scan apt: diff --git a/CMakeLists.txt b/CMakeLists.txt index e774142a6..a25c63595 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -25,7 +25,7 @@ option(ILANG_BUILD_DOCS "Build documentations." OFF) option(ILANG_BUILD_SYNTH "Build the synthesis engine." ON) option(ILANG_INSTALL_DEV "Install dev features." OFF) option(ILANG_EXPORT_PACKAGE "Export CMake package if enabled." OFF) -option(ILANG_STATIC_ANALYSIS "Build for static analysis." OFF) +option(ILANG_COVERITY "Build for Coverity static analysis." OFF) option(BUILD_SHARED_LIBS "Build shared libraries." ON) include(CMakeDependentOption) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ddafa8b8f..e89e81fed 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -142,10 +142,10 @@ endif() ## ## static analysis only ## -if(${ILANG_STATIC_ANALYSIS}) - set(STATIC_ANALYSIS TRUE) +if(${ILANG_COVERITY}) + set(COVERITY TRUE) else() - set(STATIC_ANALYSIS FALSE) + set(COVERITY FALSE) endif() # ---------------------------------------------------------------------------- # diff --git a/src/config.h.in b/src/config.h.in index 31ba312b1..9cc7091c8 100644 --- a/src/config.h.in +++ b/src/config.h.in @@ -10,7 +10,7 @@ #cmakedefine SYNTH_INTERFACE -#cmakedefine STATIC_ANALYSIS +#cmakedefine COVERITY #endif // CONFIG_CMAKE_DEFINE_H__ diff --git a/src/verilog-in/vlog_parser_util.cc b/src/verilog-in/vlog_parser_util.cc index 7326bfbda..152abec45 100644 --- a/src/verilog-in/vlog_parser_util.cc +++ b/src/verilog-in/vlog_parser_util.cc @@ -7,16 +7,13 @@ namespace ilang { -#ifdef STATIC_ANALYSIS -extern void _static_analysis_only_free(char* x); -#endif - std::string _ast_identifier_tostring(ast_identifier id) { auto id_cptr = ast_identifier_tostring(id); auto id_bstr = static_cast(id_cptr); -#ifdef STATIC_ANALYSIS - _static_analysis_only_free(id_cptr); +#ifdef COVERITY + // Used only for static analysis for it cannot identify the free phase + free(id_cptr); #endif return id_bstr; From d7ead590c41f4ffaba2120675301ca13b0873f37 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 14 Sep 2019 19:46:05 -0700 Subject: [PATCH 75/94] Remove branch-specific CI script - run all as the baseline --- .travis.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.travis.yml b/.travis.yml index f85d19e53..103cd17b0 100644 --- a/.travis.yml +++ b/.travis.yml @@ -31,9 +31,9 @@ matrix: - gem install coveralls-lcov before_script: - mkdir -p $TRAVIS_BUILD_DIR/build - - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/clean-coverage.sh $TRAVIS_BUILD_DIR/build; fi + - source $TRAVIS_BUILD_DIR/scripts/travis/clean-coverage.sh $TRAVIS_BUILD_DIR/build after_success: - - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/submit-coverage.sh $TRAVIS_BUILD_DIR/build; fi + - source $TRAVIS_BUILD_DIR/scripts/travis/submit-coverage.sh $TRAVIS_BUILD_DIR/build - name: "linux-clang" os: linux @@ -114,7 +114,7 @@ addons: - z3 script: - - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR; fi + - source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR notifications: email: false From 6b8529c8821448488d9796793a4755602b90e4b5 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 15 Sep 2019 11:05:39 -0400 Subject: [PATCH 76/94] Close file description to avoid out-of-limit opend files --- src/verilog-in/verilog_parse.cc | 2 +- test/unit-src/util.cc | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/verilog-in/verilog_parse.cc b/src/verilog-in/verilog_parse.cc index 8fb1a9e65..5bf37f021 100644 --- a/src/verilog-in/verilog_parse.cc +++ b/src/verilog-in/verilog_parse.cc @@ -17,6 +17,7 @@ static void* VlgParserAllocCstr(const std::string& str) { } void TestParseVerilog() { verilog_parser_init(); } + int TestParseVerilogFrom(const std::string& fn) { std::FILE* fp = std::fopen(fn.c_str(), "r"); if (fp == NULL) @@ -25,7 +26,6 @@ int TestParseVerilogFrom(const std::string& fn) { verilog_preprocessor_set_file(yy_preproc, (char*)VlgParserAllocCstr(fn)); auto ret = verilog_parse_file(fp); - ; std::fclose(fp); return ret; diff --git a/test/unit-src/util.cc b/test/unit-src/util.cc index b0c1aa71d..25ba98d2d 100644 --- a/test/unit-src/util.cc +++ b/test/unit-src/util.cc @@ -15,11 +15,13 @@ std::string GetRandomFileName(char* file_name_template) { #ifdef __unix__ auto res = mkstemp(file_name_template); ILA_CHECK(res != -1) << "Fail creating file"; + close(res); // avoid resource exhaustion - not thread safe return static_cast(file_name_template); #elif __APPLE__ auto res = mkstemp(file_name_template); ILA_CHECK(res != -1) << "Fail creating file"; + close(res); // avoid resource exhaustion - not thread safe return static_cast(file_name_template); #else From 97aed5c09ffdf4c051756505c1082da9d91b428e Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 15 Sep 2019 11:06:09 -0400 Subject: [PATCH 77/94] Avoid normal build in static analysis CI instance --- .travis.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.travis.yml b/.travis.yml index 103cd17b0..f85d19e53 100644 --- a/.travis.yml +++ b/.travis.yml @@ -31,9 +31,9 @@ matrix: - gem install coveralls-lcov before_script: - mkdir -p $TRAVIS_BUILD_DIR/build - - source $TRAVIS_BUILD_DIR/scripts/travis/clean-coverage.sh $TRAVIS_BUILD_DIR/build + - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/clean-coverage.sh $TRAVIS_BUILD_DIR/build; fi after_success: - - source $TRAVIS_BUILD_DIR/scripts/travis/submit-coverage.sh $TRAVIS_BUILD_DIR/build + - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/submit-coverage.sh $TRAVIS_BUILD_DIR/build; fi - name: "linux-clang" os: linux @@ -114,7 +114,7 @@ addons: - z3 script: - - source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR + - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR; fi notifications: email: false From 14cc20d690a00fa97185fe81fb0a77c9e81a7546 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 15 Sep 2019 23:42:12 -0400 Subject: [PATCH 78/94] Update CMake recipe and CI scripts for Boost::python 1.71.0 --- .travis.yml | 13 ++++++++++--- CMakeLists.txt | 2 +- azure-pipelines.yml | 6 +++--- extern/tmpl-synth | 2 +- scripts/travis/build-osx.sh | 11 +++++++++++ scripts/travis/build.sh | 3 +-- 6 files changed, 27 insertions(+), 10 deletions(-) create mode 100644 scripts/travis/build-osx.sh diff --git a/.travis.yml b/.travis.yml index f85d19e53..224a33b6a 100644 --- a/.travis.yml +++ b/.travis.yml @@ -32,6 +32,8 @@ matrix: before_script: - mkdir -p $TRAVIS_BUILD_DIR/build - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/clean-coverage.sh $TRAVIS_BUILD_DIR/build; fi + script: + - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR; fi after_success: - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/submit-coverage.sh $TRAVIS_BUILD_DIR/build; fi @@ -41,6 +43,8 @@ matrix: compiler: clang before_install: - export LD_LIBRARY_PATH=/usr/local/clang/lib:$LD_LIBRARY_PATH + script: + - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR; fi - name: "gcc49" os: linux @@ -60,6 +64,8 @@ matrix: - MATRIX_EVAL="CC=gcc-4.9 && CXX=g++-4.9" before_install: - eval "${MATRIX_EVAL}" + script: + - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR; fi - name: "osx" os: osx @@ -67,6 +73,8 @@ matrix: - brew install bison - export PATH="/usr/local/opt/bison/bin:$PATH" - export LDFLAGS="-L/usr/local/opt/bison/lib" + script: + - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build-osx.sh $TRAVIS_BUILD_DIR; fi - name: "coverity" os: linux @@ -93,6 +101,8 @@ matrix: - 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- before_script: - source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR + script: + - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR; fi addons: apt: @@ -113,8 +123,5 @@ addons: - boost-python - z3 -script: - - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR; fi - notifications: email: false diff --git a/CMakeLists.txt b/CMakeLists.txt index a25c63595..1939d6088 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -11,7 +11,7 @@ endif() # PROJECT # name version language # ---------------------------------------------------------------------------- # -project(ilang VERSION 0.9.3 +project(ilang VERSION 0.9.4 LANGUAGES CXX ) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index fc896be37..9413708db 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -27,7 +27,7 @@ jobs: export LDFLAGS="-L/usr/local/opt/bison/lib" mkdir -p build cd build - cmake .. + cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON cmake --build . cmake --build . --target install cmake --build . --target test @@ -53,7 +53,7 @@ jobs: export LDFLAGS="-L/usr/local/opt/bison/lib" mkdir -p build cd build - cmake .. + cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON cmake --build . cmake --build . --target install cmake --build . --target test @@ -74,7 +74,7 @@ jobs: - script: | mkdir -p build cd build - cmake .. + cmake .. -DCMAKE_BUILD_TYPE=Release cmake --build . sudo cmake --build . --target install cmake --build . --target test diff --git a/extern/tmpl-synth b/extern/tmpl-synth index af2bf67b0..1abbbb141 160000 --- a/extern/tmpl-synth +++ b/extern/tmpl-synth @@ -1 +1 @@ -Subproject commit af2bf67b070b556f22a1fcf7ff8c4dbad17adc31 +Subproject commit 1abbbb141aa6c5eff59e8c545e8efaec4aac008b diff --git a/scripts/travis/build-osx.sh b/scripts/travis/build-osx.sh new file mode 100644 index 000000000..b14b2005a --- /dev/null +++ b/scripts/travis/build-osx.sh @@ -0,0 +1,11 @@ +#!/bin/bash + +CI_BUILD_DIR=$1 + +cd $CI_BUILD_DIR +mkdir -p build +cd build +cmake .. -DCMAKE_BUILD_TYPE=Debug -DBoost_NO_BOOST_CMAKE=ON +make -j$(nproc) +sudo make install +make test diff --git a/scripts/travis/build.sh b/scripts/travis/build.sh index 2019fcffa..155209b28 100644 --- a/scripts/travis/build.sh +++ b/scripts/travis/build.sh @@ -5,8 +5,7 @@ CI_BUILD_DIR=$1 cd $CI_BUILD_DIR mkdir -p build cd build -cmake .. -DILANG_BUILD_COV=ON -DCMAKE_BUILD_TYPE=Debug +cmake .. -DCMAKE_BUILD_TYPE=Debug -DILANG_BUILD_COV=ON make -j$(nproc) sudo make install make test - From 87c5bdf33861348da0e2a0cfc0fa2618b6cf90ba Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 16 Sep 2019 09:50:05 -0400 Subject: [PATCH 79/94] Verbose testing for debuging --- .travis.yml | 14 +++++++------- scripts/travis/build.sh | 3 ++- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/.travis.yml b/.travis.yml index 224a33b6a..a59108acd 100644 --- a/.travis.yml +++ b/.travis.yml @@ -31,11 +31,11 @@ matrix: - gem install coveralls-lcov before_script: - mkdir -p $TRAVIS_BUILD_DIR/build - - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/clean-coverage.sh $TRAVIS_BUILD_DIR/build; fi + - source $TRAVIS_BUILD_DIR/scripts/travis/clean-coverage.sh $TRAVIS_BUILD_DIR/build script: - - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR; fi + - source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR after_success: - - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/submit-coverage.sh $TRAVIS_BUILD_DIR/build; fi + - source $TRAVIS_BUILD_DIR/scripts/travis/submit-coverage.sh $TRAVIS_BUILD_DIR/build - name: "linux-clang" os: linux @@ -44,7 +44,7 @@ matrix: before_install: - export LD_LIBRARY_PATH=/usr/local/clang/lib:$LD_LIBRARY_PATH script: - - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR; fi + - source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR - name: "gcc49" os: linux @@ -65,7 +65,7 @@ matrix: before_install: - eval "${MATRIX_EVAL}" script: - - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR; fi + - source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR - name: "osx" os: osx @@ -74,7 +74,7 @@ matrix: - export PATH="/usr/local/opt/bison/bin:$PATH" - export LDFLAGS="-L/usr/local/opt/bison/lib" script: - - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build-osx.sh $TRAVIS_BUILD_DIR; fi + - source $TRAVIS_BUILD_DIR/scripts/travis/build-osx.sh $TRAVIS_BUILD_DIR - name: "coverity" os: linux @@ -102,7 +102,7 @@ matrix: before_script: - source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR script: - - if [ ${COVERITY_SCAN_BRANCH} != 1 ]; then source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR; fi + - echo ${COVERITY_SCAN_BRANCH} addons: apt: diff --git a/scripts/travis/build.sh b/scripts/travis/build.sh index 155209b28..ab94bdf6c 100644 --- a/scripts/travis/build.sh +++ b/scripts/travis/build.sh @@ -8,4 +8,5 @@ cd build cmake .. -DCMAKE_BUILD_TYPE=Debug -DILANG_BUILD_COV=ON make -j$(nproc) sudo make install -make test +make run_test +ctest -R ExampleCMakeBuild From 914790ee79284f6325c541c87851062d6496866f Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 16 Sep 2019 11:30:49 -0700 Subject: [PATCH 80/94] Fix unit test check under Release mode --- test/t_validate_model.cc | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/test/t_validate_model.cc b/test/t_validate_model.cc index 8005c9b82..48a8e4013 100644 --- a/test/t_validate_model.cc +++ b/test/t_validate_model.cc @@ -39,7 +39,12 @@ TEST_F(TestValidateModel, nondeterministic_check) { bool res = true; GET_STDERR_MSG(res = CheckDeterminism(aes_nondet.get()), msg); EXPECT_FALSE(res); + +#ifndef NDEBUG EXPECT_FALSE(msg.empty()); +#else + EXPECT_TRUE(msg.empty()); +#endif } TEST_F(TestValidateModel, completeness) { @@ -49,7 +54,12 @@ TEST_F(TestValidateModel, completeness) { bool res = true; GET_STDERR_MSG(res = CheckCompleteness(aes_v.get()), msg); EXPECT_FALSE(res); + +#ifndef NDEBUG EXPECT_FALSE(msg.empty()); +#else + EXPECT_TRUE(msg.empty()); +#endif } TEST_F(TestValidateModel, complete_model_with_old_value) { @@ -60,7 +70,12 @@ TEST_F(TestValidateModel, complete_model_with_old_value) { GET_STDERR_MSG(res = CheckCompleteness(aes_v.get()), msg); EXPECT_FALSE(res); + +#ifndef NDEBUG EXPECT_FALSE(msg.empty()); +#else + EXPECT_TRUE(msg.empty()); +#endif CompleteModel(aes_v.get(), DEFAULT_UPDATE_METHOD::OLD_VALUE); @@ -77,7 +92,12 @@ TEST_F(TestValidateModel, complete_model_with_nondet_value) { GET_STDERR_MSG(res = CheckCompleteness(aes_v.get()), msg); EXPECT_FALSE(res); + +#ifndef NDEBUG EXPECT_FALSE(msg.empty()); +#else + EXPECT_TRUE(msg.empty()); +#endif CompleteModel(aes_v.get(), DEFAULT_UPDATE_METHOD::NONDET_VALUE); @@ -94,7 +114,12 @@ TEST_F(TestValidateModel, case_gb) { GET_STDERR_MSG(res = CheckCompleteness(gb.get()), msg); EXPECT_FALSE(res); + +#ifndef NDEBUG EXPECT_FALSE(msg.empty()); +#else + EXPECT_TRUE(msg.empty()); +#endif CompleteModel(gb.get(), DEFAULT_UPDATE_METHOD::OLD_VALUE); @@ -111,7 +136,12 @@ TEST_F(TestValidateModel, case_rbm) { GET_STDERR_MSG(res = CheckCompleteness(rbm.get()), msg); EXPECT_FALSE(res); + +#ifndef NDEBUG EXPECT_FALSE(msg.empty()); +#else + EXPECT_TRUE(msg.empty()); +#endif CompleteModel(rbm.get(), DEFAULT_UPDATE_METHOD::OLD_VALUE); From 0134931b5e1bca100f24b194cfd585dee77b8284 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 16 Sep 2019 19:06:44 -0700 Subject: [PATCH 81/94] Guard the death check under debug flag --- test/t_verilog_gen.cc | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/test/t_verilog_gen.cc b/test/t_verilog_gen.cc index 729c92a0b..03daab1b0 100644 --- a/test/t_verilog_gen.cc +++ b/test/t_verilog_gen.cc @@ -266,15 +266,21 @@ class TestVerilogExport : public ::testing::Test { auto vgen = VerilogGenerator(); vgen.add_input("x", 1); vgen.add_input("x", 1); +#ifndef NDEBUG EXPECT_DEATH(vgen.add_input("x", 2), ".*"); +#endif vgen.add_output("y", 1); vgen.add_output("y", 1); +#ifndef NDEBUG EXPECT_DEATH(vgen.add_output("y", 2), ".*"); +#endif vgen.add_wire("z", 1); vgen.add_wire("z", 1); +#ifndef NDEBUG EXPECT_DEATH(vgen.add_wire("z", 2), ".*"); +#endif } void death() { @@ -282,7 +288,9 @@ class TestVerilogExport : public ::testing::Test { auto mi = i2->NewMemInput("mi", 8, 8); auto vgen = VerilogGenerator(); +#ifndef NDEBUG EXPECT_DEATH(vgen.insertInput(mi), ".*"); +#endif } void internal_func() { From 0983c71075edf9c82b5f69f4333b787e55bdafbc Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 16 Sep 2019 20:37:31 -0700 Subject: [PATCH 82/94] Test if the CI error is due to unhandeled exception --- test/t_verilog_gen.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/t_verilog_gen.cc b/test/t_verilog_gen.cc index 03daab1b0..a661e986e 100644 --- a/test/t_verilog_gen.cc +++ b/test/t_verilog_gen.cc @@ -267,19 +267,19 @@ class TestVerilogExport : public ::testing::Test { vgen.add_input("x", 1); vgen.add_input("x", 1); #ifndef NDEBUG - EXPECT_DEATH(vgen.add_input("x", 2), ".*"); + // EXPECT_DEATH(vgen.add_input("x", 2), ".*"); #endif vgen.add_output("y", 1); vgen.add_output("y", 1); #ifndef NDEBUG - EXPECT_DEATH(vgen.add_output("y", 2), ".*"); + // EXPECT_DEATH(vgen.add_output("y", 2), ".*"); #endif vgen.add_wire("z", 1); vgen.add_wire("z", 1); #ifndef NDEBUG - EXPECT_DEATH(vgen.add_wire("z", 2), ".*"); + // EXPECT_DEATH(vgen.add_wire("z", 2), ".*"); #endif } From 7efa3fac3d7facd48c6fa29805f9b6120678cdc6 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 17 Sep 2019 06:50:52 -0700 Subject: [PATCH 83/94] Try if test class cause the uncaught crash --- test/t_verilog_gen.cc | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/test/t_verilog_gen.cc b/test/t_verilog_gen.cc index a661e986e..dce899490 100644 --- a/test/t_verilog_gen.cc +++ b/test/t_verilog_gen.cc @@ -266,9 +266,8 @@ class TestVerilogExport : public ::testing::Test { auto vgen = VerilogGenerator(); vgen.add_input("x", 1); vgen.add_input("x", 1); -#ifndef NDEBUG + // ILA_CHECK cannot be catched // EXPECT_DEATH(vgen.add_input("x", 2), ".*"); -#endif vgen.add_output("y", 1); vgen.add_output("y", 1); @@ -320,8 +319,23 @@ TEST_F(TestVerilogExport, get_width) { get_width(); } // pass node name, refset TEST_F(TestVerilogExport, new_id) { new_id(); } -// -TEST_F(TestVerilogExport, dup) { dup(); } + +// TEST_F(TestVerilogExport, dup) { dup(); } + +TEST(TestVerilogGen, dup) { + auto vgen = VerilogGenerator(); + vgen.add_input("x", 1); + vgen.add_input("x", 1); + EXPECT_DEATH(vgen.add_input("x", 2), ".*"); + + vgen.add_output("y", 1); + vgen.add_output("y", 1); + EXPECT_DEATH(vgen.add_output("y", 2), ".*"); + + vgen.add_wire("z", 1); + vgen.add_wire("z", 1); + EXPECT_DEATH(vgen.add_wire("z", 2), ".*"); +} TEST_F(TestVerilogExport, death) { death(); } From da7d90c772a4db6f7f3b3a9a2781de8de6255971 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 17 Sep 2019 06:51:29 -0700 Subject: [PATCH 84/94] Hardcode Boost flag in build test --- test/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 76a79b741..15e25c1ef 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -118,7 +118,7 @@ add_test( "${CMAKE_CTEST_COMMAND}" --build-and-test "${PROJECT_SOURCE_DIR}/starter" "${CMAKE_CURRENT_BINARY_DIR}/simple" - --build-generator "${CMAKE_GENERATOR}" + --build-generator "${CMAKE_GENERATOR} -DBoost_NO_BOOST_CMAKE=ON" --test-command "${CMAKE_CTEST_COMMAND}" ) From df917327b18df1d26a3bf2ac9d5621bfa70ff1e3 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 17 Sep 2019 07:57:37 -0700 Subject: [PATCH 85/94] Remove ill-formed build test command --- test/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 15e25c1ef..76a79b741 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -118,7 +118,7 @@ add_test( "${CMAKE_CTEST_COMMAND}" --build-and-test "${PROJECT_SOURCE_DIR}/starter" "${CMAKE_CURRENT_BINARY_DIR}/simple" - --build-generator "${CMAKE_GENERATOR} -DBoost_NO_BOOST_CMAKE=ON" + --build-generator "${CMAKE_GENERATOR}" --test-command "${CMAKE_CTEST_COMMAND}" ) From b9e55ed1a8976848a3f868d1fe1aa9649c0fe42b Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 17 Sep 2019 07:57:52 -0700 Subject: [PATCH 86/94] rename death test per suggestied convention --- test/t_verilog_gen.cc | 30 ++++++++++-------------------- 1 file changed, 10 insertions(+), 20 deletions(-) diff --git a/test/t_verilog_gen.cc b/test/t_verilog_gen.cc index dce899490..be7b636e1 100644 --- a/test/t_verilog_gen.cc +++ b/test/t_verilog_gen.cc @@ -266,19 +266,20 @@ class TestVerilogExport : public ::testing::Test { auto vgen = VerilogGenerator(); vgen.add_input("x", 1); vgen.add_input("x", 1); - // ILA_CHECK cannot be catched - // EXPECT_DEATH(vgen.add_input("x", 2), ".*"); +#ifndef NDEBUG + EXPECT_DEATH(vgen.add_input("x", 2), ".*"); +#endif vgen.add_output("y", 1); vgen.add_output("y", 1); #ifndef NDEBUG - // EXPECT_DEATH(vgen.add_output("y", 2), ".*"); + EXPECT_DEATH(vgen.add_output("y", 2), ".*"); #endif vgen.add_wire("z", 1); vgen.add_wire("z", 1); #ifndef NDEBUG - // EXPECT_DEATH(vgen.add_wire("z", 2), ".*"); + EXPECT_DEATH(vgen.add_wire("z", 2), ".*"); #endif } @@ -320,24 +321,13 @@ TEST_F(TestVerilogExport, get_width) { get_width(); } // pass node name, refset TEST_F(TestVerilogExport, new_id) { new_id(); } -// TEST_F(TestVerilogExport, dup) { dup(); } - -TEST(TestVerilogGen, dup) { - auto vgen = VerilogGenerator(); - vgen.add_input("x", 1); - vgen.add_input("x", 1); - EXPECT_DEATH(vgen.add_input("x", 2), ".*"); +using TestVerilogExportDeathTest = TestVerilogExport; - vgen.add_output("y", 1); - vgen.add_output("y", 1); - EXPECT_DEATH(vgen.add_output("y", 2), ".*"); - - vgen.add_wire("z", 1); - vgen.add_wire("z", 1); - EXPECT_DEATH(vgen.add_wire("z", 2), ".*"); -} +// TEST_F(TestVerilogExport, dup) { dup(); } +TEST_F(TestVerilogExportDeathTest, dup) { dup(); } -TEST_F(TestVerilogExport, death) { death(); } +// TEST_F(TestVerilogExport, death) { death(); } +TEST_F(TestVerilogExportDeathTest, death) { death(); } // ?? func -- death TEST_F(TestVerilogExport, internalfunc) { internal_func(); } From fe8cdc069ec2b28fd9c82e77d3c4ba0249bb63cf Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 17 Sep 2019 12:47:01 -0400 Subject: [PATCH 87/94] Update ItSy for boost --- extern/tmpl-synth | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/extern/tmpl-synth b/extern/tmpl-synth index 1abbbb141..06bab9a5b 160000 --- a/extern/tmpl-synth +++ b/extern/tmpl-synth @@ -1 +1 @@ -Subproject commit 1abbbb141aa6c5eff59e8c545e8efaec4aac008b +Subproject commit 06bab9a5bbb49f70d013aabc678433c9c0f22a91 From 3f5bceeaaea9af63090e960f83cd62a44196c9d2 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 17 Sep 2019 14:47:33 -0400 Subject: [PATCH 88/94] Rename death test with extra suffix to avoid thread errors --- test/t_verilog_gen.cc | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/test/t_verilog_gen.cc b/test/t_verilog_gen.cc index be7b636e1..0a9440c4f 100644 --- a/test/t_verilog_gen.cc +++ b/test/t_verilog_gen.cc @@ -266,21 +266,15 @@ class TestVerilogExport : public ::testing::Test { auto vgen = VerilogGenerator(); vgen.add_input("x", 1); vgen.add_input("x", 1); -#ifndef NDEBUG EXPECT_DEATH(vgen.add_input("x", 2), ".*"); -#endif vgen.add_output("y", 1); vgen.add_output("y", 1); -#ifndef NDEBUG EXPECT_DEATH(vgen.add_output("y", 2), ".*"); -#endif vgen.add_wire("z", 1); vgen.add_wire("z", 1); -#ifndef NDEBUG EXPECT_DEATH(vgen.add_wire("z", 2), ".*"); -#endif } void death() { @@ -288,9 +282,7 @@ class TestVerilogExport : public ::testing::Test { auto mi = i2->NewMemInput("mi", 8, 8); auto vgen = VerilogGenerator(); -#ifndef NDEBUG EXPECT_DEATH(vgen.insertInput(mi), ".*"); -#endif } void internal_func() { @@ -323,10 +315,8 @@ TEST_F(TestVerilogExport, new_id) { new_id(); } using TestVerilogExportDeathTest = TestVerilogExport; -// TEST_F(TestVerilogExport, dup) { dup(); } TEST_F(TestVerilogExportDeathTest, dup) { dup(); } -// TEST_F(TestVerilogExport, death) { death(); } TEST_F(TestVerilogExportDeathTest, death) { death(); } // ?? func -- death From a3772d4cfea0f6ea8614f4c0e67f951d93d8dc62 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 17 Sep 2019 14:47:58 -0400 Subject: [PATCH 89/94] Debugging unknown error messages --- test/t_vtarget_gen.cc | 44 ++++++++++++++++++++++--------------------- 1 file changed, 23 insertions(+), 21 deletions(-) diff --git a/test/t_vtarget_gen.cc b/test/t_vtarget_gen.cc index b7b867f76..74a751924 100644 --- a/test/t_vtarget_gen.cc +++ b/test/t_vtarget_gen.cc @@ -49,14 +49,19 @@ TEST(TestVlgTargetGen, AesIlaInfo) { TEST(TestVlgTargetGen, PipeExample) { auto ila_model = SimplePipe::BuildModel(); - auto dirName = std::string(ILANG_TEST_SRC_ROOT) + "/unit-data/vpipe/"; + auto dirName = os_portable_append_dir(ILANG_TEST_DATA_DIR, "vpipe"); + auto rfDir = os_portable_append_dir(dirName, "rfmap"); + VerilogVerificationTargetGenerator vg( - {}, // no include - {dirName + "simple_pipe.v"}, // - "pipeline_v", // top_module_name - dirName + "rfmap/vmap.json", // variable mapping - dirName + "rfmap/cond.json", dirName + "verify/", ila_model.get(), - VerilogVerificationTargetGenerator::backend_selector::COSA); + {}, // no include + {os_portable_append_dir(dirName, "simple_pipe.v")}, // vlog files + "pipeline_v", // top_module_name + os_portable_append_dir(rfDir, "vmap.json"), // variable mapping + os_portable_append_dir(rfDir, "cond.json"), // instruction mapping + os_portable_append_dir(dirName, "verify"), // verification dir + ila_model.get(), // ILA model + VerilogVerificationTargetGenerator::backend_selector::COSA // engine + ); EXPECT_FALSE(vg.in_bad_state()); @@ -100,7 +105,6 @@ TEST(TestVlgTargetGen, PipeExampleNotEqu) { vg.GenerateTargets(); } - TEST(TestVlgTargetGen, Memory) { auto ila_model = MemorySwap::BuildModel(); @@ -123,41 +127,39 @@ TEST(TestVlgTargetGen, Memory) { TEST(TestVlgTargetGen, MemoryInternal) { // test the expansion of memory auto ila_model = MemorySwap::BuildSimpleSwapModel(); - VerilogVerificationTargetGenerator::vtg_config_t vtg_cfg; // default configuration + VerilogVerificationTargetGenerator::vtg_config_t + vtg_cfg; // default configuration VerilogGeneratorBase::VlgGenConfig vlg_cfg; vlg_cfg.extMem = false; auto dirName = std::string(ILANG_TEST_SRC_ROOT) + "/unit-data/vpipe/vmem/"; VerilogVerificationTargetGenerator vg( - {}, // no include - {dirName + "swap_im.v"}, // vlog files - "swap", // top_module_name + {}, // no include + {dirName + "swap_im.v"}, // vlog files + "swap", // top_module_name dirName + "vmap-expand.json", // variable mapping dirName + "cond-expand.json", // cond path - dirName, // output path + dirName, // output path ila_model.get(), - VerilogVerificationTargetGenerator::backend_selector::COSA, - vtg_cfg, - vlg_cfg - ); + VerilogVerificationTargetGenerator::backend_selector::COSA, vtg_cfg, + vlg_cfg); EXPECT_FALSE(vg.in_bad_state()); vg.GenerateTargets(); } - TEST(TestVlgTargetGen, MemoryInternalExternal) { auto ila_model = MemorySwap::BuildRfAsMemModel(); auto dirName = std::string(ILANG_TEST_SRC_ROOT) + "/unit-data/vpipe/vmem/"; VerilogVerificationTargetGenerator vg( - {}, // no include + {}, // no include {dirName + "rf_as_mem.v"}, // vlog files - "proc", // top_module_name + "proc", // top_module_name dirName + "vmap-rfarray.json", // variable mapping dirName + "cond-rfarray.json", // cond path - dirName, // output path + dirName, // output path ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA); From 548488221a93c073b4750ee235ab8274a1ca7029 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 17 Sep 2019 14:50:34 -0400 Subject: [PATCH 90/94] Fix typo --- test/unit-src/util.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/unit-src/util.cc b/test/unit-src/util.cc index 25ba98d2d..f331ee94a 100644 --- a/test/unit-src/util.cc +++ b/test/unit-src/util.cc @@ -48,7 +48,7 @@ void CheckIlaEqLegacy(const InstrLvlAbsPtr& a, const InstrLvlAbsPtr& b) { state_mapping = ExprFuse::And(state_mapping, ExprFuse::Eq(var_org, var_des)); } catch (...) { - ILA_WARN << "Fail automatically matcing state vars"; + ILA_WARN << "Fail automatically matching state vars"; } } From 51db4b75590d15d9648048ecb378494f4dce2854 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 17 Sep 2019 15:56:43 -0400 Subject: [PATCH 91/94] Update regression package versions --- README.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 4c4747b7d..72d03a675 100644 --- a/README.md +++ b/README.md @@ -56,12 +56,12 @@ brew install bison flex boost boost-python z3 | Ubuntu 14.04 (Trusty) | gcc 4.8.4 | 3.8.0 | 4.8.5 | 1.54 | 3.0.4 | 2.5.25 | Release | | Ubuntu 16.04 (Xenial) | gcc 5.4.0 | 3.12.4 | 4.4.1 | 1.58 | 3.0.4 | 2.6.0 | Debug | | Ubuntu 16.04 (Xenial) | clang 7.0.0 | 3.12.4 | 4.4.1 | 1.58 | 3.0.4 | 2.6.0 | Debug | -| Ubuntu 16.04 (Xenial) | gcc 5.4.0 | 3.12.4 | 4.4.1 | 1.69 | 3.0.4 | 2.6.0 | Default | -| Ubuntu 18.04 (Bionic) | gcc 7.4.0 | 3.14.4 | 4.4.1 | 1.65 | 3.0.4 | 2.6.4 | Default | -| OSX 10.13.3 (High Sierra) | Xcode 9.4.1 | 3.11.3 | 4.8.5 | 1.70 | 3.4.1 | 2.5.35 | Debug | -| OSX 10.13.6 (High Sierra) | Xcode 10.1.0 | 3.14.5 | 4.8.5 | 1.70 | 3.4.1 | 2.5.35 | Default | -| OSX 10.14.5 (Mojave) | Xcode 10.2.1 | 3.14.5 | 4.8.5 | 1.70 | 3.4.1 | 2.5.35 | Default | -| Windows Server 2016 | VS 2017 | 3.14.5 | 4.8.5 | - | 3.3.2 | 2.6.4 | Default | +| Ubuntu 16.04 (Xenial) | gcc 5.4.0 | 3.12.4 | 4.4.1 | 1.69 | 3.0.4 | 2.6.0 | Release | +| Ubuntu 18.04 (Bionic) | gcc 7.4.0 | 3.15.2 | 4.8.6 | 1.65 | 3.0.4 | 2.6.4 | Release | +| OSX 10.13.3 (High Sierra) | Xcode 9.4.1 | 3.11.3 | 4.8.5 | 1.71 | 3.4.2 | 2.5.35 | Debug | +| OSX 10.13.6 (High Sierra) | Xcode 10.1.0 | 3.14.5 | 4.8.5 | 1.71 | 3.4.2 | 2.5.35 | Release | +| OSX 10.14.5 (Mojave) | Xcode 10.2.1 | 3.14.5 | 4.8.5 | 1.71 | 3.4.2 | 2.5.35 | Release | +| Windows Server 2016 | VS 2017 | 3.14.5 | 4.8.5 | - | 3.3.2 | 2.6.4 | Release | ### Default Build From bf3bbb3bb83c20309fa40f86fb507dc6e4ac437f Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 17 Sep 2019 16:22:01 -0400 Subject: [PATCH 92/94] Prepare for Coverity static analysis --- .travis.yml | 2 +- CMakeLists.txt | 2 +- scripts/travis/build-static.sh | 9 +++++++++ 3 files changed, 11 insertions(+), 2 deletions(-) create mode 100644 scripts/travis/build-static.sh diff --git a/.travis.yml b/.travis.yml index a59108acd..b758af42b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -102,7 +102,7 @@ matrix: before_script: - source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR script: - - echo ${COVERITY_SCAN_BRANCH} + - source $TRAVIS_BUILD_DIR/scripts/travis/build-static.sh $TRAVIS_BUILD_DIR addons: apt: diff --git a/CMakeLists.txt b/CMakeLists.txt index 1939d6088..8ac9873c0 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -11,7 +11,7 @@ endif() # PROJECT # name version language # ---------------------------------------------------------------------------- # -project(ilang VERSION 0.9.4 +project(ilang VERSION 0.9.5 LANGUAGES CXX ) diff --git a/scripts/travis/build-static.sh b/scripts/travis/build-static.sh new file mode 100644 index 000000000..7b54504dd --- /dev/null +++ b/scripts/travis/build-static.sh @@ -0,0 +1,9 @@ +#!/bin/bash + +CI_BUILD_DIR=$1 + +cd $CI_BUILD_DIR +mkdir -p build +cd build +cmake .. -DCMAKE_BUILD_TYPE=Debug -DILANG_COVERITY=ON -DILANG_BUILD_TEST=OFF +make -j$(nproc) From 30d9f3a27e6fafe4826bc26d46bf085835637005 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 17 Sep 2019 17:50:20 -0400 Subject: [PATCH 93/94] Add static analysis annotation --- src/verilog-in/verilog_const_parser.cc | 54 +++++++++++++------------- 1 file changed, 28 insertions(+), 26 deletions(-) diff --git a/src/verilog-in/verilog_const_parser.cc b/src/verilog-in/verilog_const_parser.cc index eda472a95..1fd799d07 100644 --- a/src/verilog-in/verilog_const_parser.cc +++ b/src/verilog-in/verilog_const_parser.cc @@ -7,6 +7,7 @@ #include #include #include +#include namespace ilang { @@ -69,41 +70,44 @@ VerilogConstantExprEval::_eval(ast_expression* e, } // to explicitly free it return ret; - } else if (e->primary->value_type == ast_primary_value_type::PRIMARY_MINMAX_EXP) { - if ( e->primary->value.minmax->left != NULL || e->primary->value.minmax->right != NULL - || e->primary->value.minmax->aux == NULL) { - error_str = ast_expression_tostring(e); - ILA_ERROR << "Unable to parse " << error_str; - eval_error = true; - return 0; - } + } else if (e->primary->value_type == + ast_primary_value_type::PRIMARY_MINMAX_EXP) { + if (e->primary->value.minmax->left != NULL || + e->primary->value.minmax->right != NULL || + e->primary->value.minmax->aux == NULL) { + error_str = ast_expression_tostring(e); + ILA_ERROR << "Unable to parse " << error_str; + eval_error = true; + return 0; + } return _eval(e->primary->value.minmax->aux, param_defs); - } else if (e->primary->value_type == ast_primary_value_type::PRIMARY_CONCATENATION) { - ast_concatenation * cc = e->primary->value.concatenation; - unsigned repeat = cc->repeat? _eval(cc->repeat, param_defs ) : 1; + } else if (e->primary->value_type == + ast_primary_value_type::PRIMARY_CONCATENATION) { + ast_concatenation* cc = e->primary->value.concatenation; + unsigned repeat = cc->repeat ? _eval(cc->repeat, param_defs) : 1; unsigned total_width = 0; long long ret = 0; for (size_t idx = 0; idx < cc->items->items; ++idx) { - ast_expression * it = (ast_expression *)ast_list_get_not_null(cc->items, idx); + ast_expression* it = + (ast_expression*)ast_list_get_not_null(cc->items, idx); unsigned v = _eval(it, param_defs); unsigned width = it->primary->value.number->width; if (width == 0) { error_str = ast_expression_tostring(e); eval_error = true; return 0; - } + } ret = ret << width; - ret = ret | v; + ret = ret | v; total_width += width; } unsigned origin = ret; - for (unsigned idx = 1; idx < repeat; ++ idx) { + for (unsigned idx = 1; idx < repeat; ++idx) { ret = ret << total_width; ret = ret | origin; } return ret; - } - else { // parser error: unable to handle + } else { // parser error: unable to handle error_str = ast_expression_tostring(e); eval_error = true; return 0; @@ -138,10 +142,10 @@ VerilogConstantExprEval::_eval(ast_expression* e, error_str = ast_expression_tostring(e); return 0; } else if (e->type == ast_expression_type::CONDITIONAL_EXPRESSION) { - double left = _eval(e->left, param_defs); + double left = _eval(e->left, param_defs); double right = _eval(e->right, param_defs); double cond = _eval(e->aux, param_defs); - return cond?left:right; + return cond ? left : right; } eval_error = true; @@ -164,7 +168,6 @@ double VerilogConstantExprEval::Eval(ast_expression* _s) { return val; } - /// parse only the current module's parameter definitions, will update /// param_defs void VerilogConstantExprEval::ParseCurrentModuleParameters( @@ -183,7 +186,7 @@ void VerilogConstantExprEval::ParseCurrentModuleParameters( return; ILA_DLOG("vlg_cnst_parser") << "For each param in ParseCurrentModuleParameters " - << ast_identifier_tostring(m->identifier) << std::endl; + << _ast_identifier_tostring(m->identifier) << std::endl; for (unsigned pi = 0; pi < params->items; ++pi) { ILA_DLOG("vlg_cnst_parser") << " For param " << pi << std::endl; @@ -204,8 +207,7 @@ void VerilogConstantExprEval::ParseCurrentModuleParameters( ILA_DLOG("vlg_cnst_parser") << " for assignment #" << assignidx << std::endl; - std::string param_name = - ast_identifier_tostring(asn->lval->data.identifier); + auto param_name = _ast_identifier_tostring(asn->lval->data.identifier); double val; if (pi < ordered_parameter_override.size()) @@ -216,7 +218,8 @@ void VerilogConstantExprEval::ParseCurrentModuleParameters( val = _eval(asn->expression, output_parameter_dict); if (eval_error) { eval_error = false; - ILA_WARN <<"ParseCurrentModuleParameters has error for : " << error_str << std::endl; + ILA_WARN << "ParseCurrentModuleParameters has error for : " << error_str + << std::endl; continue; // if we encounter error, just skip it } @@ -284,8 +287,7 @@ void VerilogConstantExprEval::PopulateParameterDefByHierarchy( instance_ptr->module_parameters->module_parameter, param_ov_idx); ILA_NOT_NULL(name_val_pair->port_name); - std::string param_name = - ast_identifier_tostring(name_val_pair->port_name); + auto param_name = _ast_identifier_tostring(name_val_pair->port_name); double val = _eval(name_val_pair->expression, current_module_param_defs); if (eval_error) From 1ac29c8fa11d607827f3f501c1372549b7a8523d Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Tue, 17 Sep 2019 22:37:42 -0400 Subject: [PATCH 94/94] Release v1.0.0 --- CMakeLists.txt | 2 +- appveyor.yml | 28 ---------------------------- 2 files changed, 1 insertion(+), 29 deletions(-) delete mode 100644 appveyor.yml diff --git a/CMakeLists.txt b/CMakeLists.txt index 8ac9873c0..08d0641a4 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -11,7 +11,7 @@ endif() # PROJECT # name version language # ---------------------------------------------------------------------------- # -project(ilang VERSION 0.9.5 +project(ilang VERSION 1.0.0 LANGUAGES CXX ) diff --git a/appveyor.yml b/appveyor.yml deleted file mode 100644 index 8ec750f43..000000000 --- a/appveyor.yml +++ /dev/null @@ -1,28 +0,0 @@ -version: 1.0.{build} -image: -- Ubuntu1804 -clone_depth: 1 -build_script: -- sh: >- - sudo apt update - - sudo DEBIAN_FRONTEND=noninteractive apt install --yes bison libboost-all-dev z3 libz3-dev - - sudo apt install --yes flex - - # ILAng - - cd $APPVEYOR_BUILD_FOLDER - - mkdir -p build - - cd build - - cmake .. - - make -j$(nproc) - - sudo make install - - make test -