From 487dabac369ee25ed709c65c458cf68b891ae8d5 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 3 Jun 2020 00:04:42 -0400 Subject: [PATCH 01/21] Start adopting c++17 --- CMakeLists.txt | 2 +- README.md | 3 ++- src/CMakeLists.txt | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index fc12ca295..46face01e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -11,7 +11,7 @@ endif() # PROJECT # name version language # ---------------------------------------------------------------------------- # -project(ilang VERSION 1.0.3 +project(ilang VERSION 1.0.4 LANGUAGES CXX ) diff --git a/README.md b/README.md index f857e5663..1351c03fe 100644 --- a/README.md +++ b/README.md @@ -33,7 +33,7 @@ ### Prerequisites -ILAng requires CMake (3.9.6 or above) and compilers with CXX11 support. +ILAng requires CMake (3.9.6 or above) and compilers with C++17 support. To install dependencies on Debian-based Linux: ```bash @@ -62,6 +62,7 @@ brew install bison flex boost boost-python z3 | 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.58 | 3.0.4 | 2.6.0 | Debug | | Ubuntu 16.04 (Xenial) | gcc 5.4.0 | 3.17.0 | 4.4.1 | 1.58 | 3.0.4 | 2.6.0 | Release | +| Ubuntu 18.04 (Bionic) | clang 6.0.0 | 3.10.2 | 4.4.1 | 1.65 | 3.0.4 | 2.6.4 | Debug | | Ubuntu 18.04 (Bionic) | gcc 7.5.0 | 3.10.2 | 4.4.1 | 1.65 | 3.0.4 | 2.6.4 | Debug | | Ubuntu 18.04 (Bionic) | gcc 7.5.0 | 3.17.0 | 4.4.1 | 1.65 | 3.0.4 | 2.6.4 | Release | | Ubuntu 20.04 (Focal Fosa) | gcc 7.4.0 | 3.17.0 | 4.4.1 | 1.65 | 3.0.4 | 2.6.4 | Release | diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 8b93b20f0..0dab6802d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -26,7 +26,7 @@ endif() ## ## compile features/options ## -target_compile_features(${ILANG_LIB_NAME} PUBLIC cxx_std_11) +target_compile_features(${ILANG_LIB_NAME} PUBLIC cxx_std_17) set_property( TARGET ${ILANG_LIB_NAME} From b837366280d038f8b666e545cd4c877bf8c8600b Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 3 Jun 2020 01:25:08 -0400 Subject: [PATCH 02/21] Remove redundant legacy code --- include/ilang/ila/instr_lvl_abs.h | 10 ---------- src/ila/instr_lvl_abs.cc | 28 ---------------------------- test/t_ila.cc | 17 ----------------- 3 files changed, 55 deletions(-) diff --git a/include/ilang/ila/instr_lvl_abs.h b/include/ilang/ila/instr_lvl_abs.h index 297f0733a..3b12dbb0b 100644 --- a/include/ilang/ila/instr_lvl_abs.h +++ b/include/ilang/ila/instr_lvl_abs.h @@ -235,16 +235,6 @@ class InstrLvlAbs : public Object, /// \param[in] valid_expr pointer to the valid function (as an expression). void ForceSetValid(const ExprPtr valid_expr); - /// \brief Sanity check for the ILA (e.g. sort marching). - /// \return True if check pass. - bool Check() const; - - /// \brief Merge child-ILAs, including variables, simplifier, etc. - void MergeChild(); - - /// \brief Sort instructions based on the sequencing, if any. - void SortInstr(); - /// \brief Define instruction sequencing by adding a transition edge. /// \param[in] src source instruction /// \param[in] dst target instruction (destination) diff --git a/src/ila/instr_lvl_abs.cc b/src/ila/instr_lvl_abs.cc index 76d6c673f..3945e8f3b 100644 --- a/src/ila/instr_lvl_abs.cc +++ b/src/ila/instr_lvl_abs.cc @@ -261,34 +261,6 @@ void InstrLvlAbs::ForceSetValid(const ExprPtr valid_expr) { valid_ = valid; } -bool InstrLvlAbs::Check() const { - ILA_WARN << "Check in InstrLvlAbs not implemented."; - // TODO - // check input - // check state - // check init - // check fetch - // check valid - // check instr - // check child-ILA? - // check sequencing - return true; -} - -void InstrLvlAbs::MergeChild() { - ILA_WARN << "MergeChild in InstrLvlAbs not implemented."; - // TODO - // merge shared states - // merge simplifier -} - -void InstrLvlAbs::SortInstr() { - ILA_WARN << "SortInstr in InstrLvlAbs not implemented."; - // TODO - // check this is a micro-ILA and has sequencing - // sort instructions based on the sequencing -} - void InstrLvlAbs::AddSeqTran(const InstrPtr src, const InstrPtr dst, const ExprPtr cnd) { // XXX src, dst should already registered. diff --git a/test/t_ila.cc b/test/t_ila.cc index 004d15b37..ef63f0ab9 100644 --- a/test/t_ila.cc +++ b/test/t_ila.cc @@ -273,23 +273,6 @@ TEST(TestInstrLvlAbs, Child) { EXPECT_ANY_THROW(ila->child(3)); } -TEST(TestInstrLvlAbs, CheckAll) { - auto ila = InstrLvlAbs::New("ila"); - EXPECT_TRUE(ila->Check()); -} - -TEST(TestInstrLvlAbs, MergeAll) { - auto ila = InstrLvlAbs::New("ila"); - ila->MergeChild(); - // TODO -} - -TEST(TestInstrLvlAbs, SortInstr) { - auto ila = InstrLvlAbs::New("ila"); - ila->SortInstr(); - // TODO -} - TEST(TestInstrLvlAbs, SeqTran) { auto ila = InstrLvlAbs::New("ila"); From 5d75abc9db9197a1cdbb73f82fbb14c0502c0117 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 3 Jun 2020 01:25:51 -0400 Subject: [PATCH 03/21] Replace os_portable implementation with std::filesystem if possible --- src/CMakeLists.txt | 5 +++++ src/util/fs.cc | 47 +++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 51 insertions(+), 1 deletion(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0dab6802d..a040a0f46 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -61,6 +61,11 @@ target_include_directories(${ILANG_LIB_NAME} # LINK LIBRARIES # external dependencies # ---------------------------------------------------------------------------- # +## +## std::filesystem +## +target_link_libraries(${ILANG_LIB_NAME} PRIVATE stdc++fs) + ## ## gcov ## diff --git a/src/util/fs.cc b/src/util/fs.cc index a5e830e28..d6a6a1176 100644 --- a/src/util/fs.cc +++ b/src/util/fs.cc @@ -8,6 +8,7 @@ #include #include +#include #include #include @@ -37,6 +38,8 @@ namespace ilang { /// Create a dir, true -> suceeded , ow false bool os_portable_mkdir(const std::string& dir) { + return std::filesystem::create_directory(dir); +#if 0 #if defined(_WIN32) || defined(_WIN64) // on windows return _mkdir(dir.c_str()) == 0; @@ -50,11 +53,14 @@ bool os_portable_mkdir(const std::string& dir) { } return false; #endif +#endif } /// Append two path (you have to decide whether it is / or \) std::string os_portable_append_dir(const std::string& dir1, const std::string& dir2) { + return std::filesystem::path(dir1) / std::filesystem::path(dir2); +#if 0 std::string sep; #if defined(_WIN32) || defined(_WIN64) // on windows @@ -72,16 +78,24 @@ std::string os_portable_append_dir(const std::string& dir1, str2 = dir2.substr(1); } return str1 + str2; +#endif } /// Append two path (you have to decide whether it is / or \) std::string os_portable_append_dir(const std::string& dir1, const std::vector& dirs) { + auto ret = std::filesystem::path(dir1); + for (auto&& d : dirs) { + ret /= d; + } + return ret; +#if 0 std::string ret = dir1; for (auto&& d : dirs) { ret = os_portable_append_dir(ret, d); } return ret; +#endif } /// Append two path (you have to decide whether it is / or \) @@ -98,6 +112,8 @@ std::string os_portable_join_dir(const std::vector& dirs) { /// C:\a\b\c.txt -> c.txt /// d/e/ghi -> ghi std::string os_portable_file_name_from_path(const std::string& path) { + return std::filesystem::path(path).filename(); +#if 0 std::string sep; #if defined(_WIN32) || defined(_WIN64) // on windows @@ -110,10 +126,15 @@ std::string os_portable_file_name_from_path(const std::string& path) { ILA_ERROR_IF(path.back() == sep[0]) << "Extracting file name from path:" << path << " that ends with:" << sep; return Split(path, sep).back(); +#endif } /// Copy all file from a source dir to the destination dir bool os_portable_copy_dir(const std::string& src, const std::string& dst) { + auto ret = std::filesystem::exists(src) && std::filesystem::exists(dst); + std::filesystem::copy(src, dst); + return ret; +#if 0 int ret; #if defined(_WIN32) || defined(_WIN64) // on windows @@ -125,11 +146,16 @@ bool os_portable_copy_dir(const std::string& src, const std::string& dst) { ("cp " + os_portable_append_dir(src, "*") + " " + dst).c_str()); #endif return ret == 0; +#endif } /// Copy the source file to the destination dir bool os_portable_copy_file_to_dir(const std::string& src, const std::string& dst) { + auto ret = std::filesystem::exists(src) && std::filesystem::exists(dst); + std::filesystem::copy(src, dst); + return ret; +#if 0 int ret; #if defined(_WIN32) || defined(_WIN64) // on windows @@ -139,10 +165,15 @@ bool os_portable_copy_file_to_dir(const std::string& src, ret = std::system(("cp " + src + " " + dst).c_str()); #endif return ret == 0; +#endif } bool os_portable_move_file_to_dir(const std::string& src, const std::string& dst) { + auto ret = std::filesystem::exists(src) && std::filesystem::exists(dst); + std::filesystem::rename(src, dst); + return ret; +#if 0 #if defined(_WIN32) || defined(_WIN64) // on windows // XXX need test @@ -153,9 +184,12 @@ bool os_portable_move_file_to_dir(const std::string& src, #endif int ret = std::system(cmd.c_str()); return ret == 0; +#endif } bool os_portable_remove_file(const std::string& file) { + return std::filesystem::remove(file); +#if 0 #if defined(_WIN32) || defined(_WIN64) // on windows // XXX need test @@ -166,6 +200,7 @@ bool os_portable_remove_file(const std::string& file) { #endif int ret = std::system(cmd.c_str()); return ret == 0; +#endif } /// Extract path from path @@ -173,7 +208,8 @@ bool os_portable_remove_file(const std::string& file) { /// C:\a\b\c -> C:\a\b /// d/e/ghi -> d/e/ std::string os_portable_path_from_path(const std::string& path) { - + return std::filesystem::path(path).parent_path(); +#if 0 std::string sep; #if defined(_WIN32) || defined(_WIN64) // on windows @@ -187,10 +223,15 @@ std::string os_portable_path_from_path(const std::string& path) { auto pos = path.rfind(sep); ILA_ASSERT(pos != path.npos); return path.substr(0, pos + 1); // include sep +#endif } /// C:\\a.txt -> C:\\a or /a/b/c.txt -> a/b/c std::string os_portable_remove_file_name_extension(const std::string& fname) { + auto ret = std::filesystem::path(fname); + ret.replace_extension(); + return ret; +#if 0 std::string sep; #if defined(_WIN32) || defined(_WIN64) // on windows @@ -214,6 +255,7 @@ std::string os_portable_remove_file_name_extension(const std::string& fname) { // /.asdfaf.d -> /.asdfaf | /.a -> /. return fname.substr(0, dot_pos); +#endif } bool os_portable_compare_file(const std::string& file1, @@ -622,6 +664,8 @@ bool os_portable_chdir(const std::string& dirname) { /// Get the current directory std::string os_portable_getcwd() { + return std::filesystem::current_path(); +#if 0 #if defined(_WIN32) || defined(_WIN64) // windows size_t len = GetCurrentDirectory(0, NULL); @@ -647,6 +691,7 @@ std::string os_portable_getcwd() { delete[] buffer; return ret; #endif +#endif } // os_portable_getcwd #if (defined(__unix__) || defined(unix) || defined(__APPLE__) || \ From f72ecf2b3476ce3ccd0ba9b9019612fabb6f14dd Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Thu, 4 Jun 2020 16:46:17 -0400 Subject: [PATCH 04/21] Use c++17 filesystem for util/fs implementation --- src/util/fs.cc | 267 +++++++---------------- test/t_portable.cc | 15 +- test/t_util.cc | 94 ++++---- test/t_verilog_gen.cc | 127 +++++------ test/t_verilog_mod.cc | 19 +- test/unit-data/verilog_sample/.gitignore | 1 - test/unit-include/util.h | 2 +- test/unit-src/util.cc | 42 ++-- 8 files changed, 235 insertions(+), 332 deletions(-) delete mode 100644 test/unit-data/verilog_sample/.gitignore diff --git a/src/util/fs.cc b/src/util/fs.cc index d6a6a1176..2038aaf2f 100644 --- a/src/util/fs.cc +++ b/src/util/fs.cc @@ -1,8 +1,9 @@ /// \file Utility to deal with filesystem /// This could be possible OS dependent so we want to provide a portable layer -/// C++17 and after should support something like experimental/filesystem, but -/// we don't rely on it +// C++17 and after should support something like experimental/filesystem, but +// we don't rely on it // --- Hongce Zhang +// Now that ILAng require C++17, we can utilize some of the supports. #include @@ -13,7 +14,6 @@ #include #if defined(_WIN32) || defined(_WIN64) - // windows #include #include @@ -36,66 +36,36 @@ namespace ilang { +namespace fs = std::filesystem; + /// Create a dir, true -> suceeded , ow false bool os_portable_mkdir(const std::string& dir) { - return std::filesystem::create_directory(dir); -#if 0 -#if defined(_WIN32) || defined(_WIN64) - // on windows - return _mkdir(dir.c_str()) == 0; -#else - // on *nix - auto res = mkdir(dir.c_str(), S_IRWXU | S_IRWXG | S_IROTH | S_IXOTH) != -1; + if (fs::is_directory(dir)) { + return true; + } - struct stat statbuff; - if (stat(dir.c_str(), &statbuff) != -1) { - return res || S_ISDIR(statbuff.st_mode); + try { + return fs::create_directory(dir); + } catch (fs::filesystem_error& e) { + ILA_ERROR << e.what(); + return false; } - return false; -#endif -#endif } /// Append two path (you have to decide whether it is / or \) std::string os_portable_append_dir(const std::string& dir1, const std::string& dir2) { - return std::filesystem::path(dir1) / std::filesystem::path(dir2); -#if 0 - std::string sep; -#if defined(_WIN32) || defined(_WIN64) - // on windows - sep = "\\"; -#else - // on *nix - sep = "/"; -#endif - auto str1 = dir1; - auto str2 = dir2; - if (!StrEndsWith(str1, sep)) - str1 += sep; - if (StrStartsWith(dir2, sep)) { - ILA_ERROR << "appending root path:" << dir2 << " to " << dir1; - str2 = dir2.substr(1); - } - return str1 + str2; -#endif + return (fs::path(dir1) / fs::path(dir2)).string(); } /// Append two path (you have to decide whether it is / or \) std::string os_portable_append_dir(const std::string& dir1, const std::vector& dirs) { - auto ret = std::filesystem::path(dir1); - for (auto&& d : dirs) { - ret /= d; - } - return ret; -#if 0 - std::string ret = dir1; + auto acc = fs::path(dir1); for (auto&& d : dirs) { - ret = os_portable_append_dir(ret, d); + acc /= fs::path(d); } - return ret; -#endif + return acc.string(); } /// Append two path (you have to decide whether it is / or \) @@ -112,95 +82,65 @@ std::string os_portable_join_dir(const std::vector& dirs) { /// C:\a\b\c.txt -> c.txt /// d/e/ghi -> ghi std::string os_portable_file_name_from_path(const std::string& path) { - return std::filesystem::path(path).filename(); -#if 0 - std::string sep; -#if defined(_WIN32) || defined(_WIN64) - // on windows - sep = "\\"; -#else - // on *nix - sep = "/"; -#endif - - ILA_ERROR_IF(path.back() == sep[0]) - << "Extracting file name from path:" << path << " that ends with:" << sep; - return Split(path, sep).back(); -#endif + return fs::path(path).filename(); } /// Copy all file from a source dir to the destination dir bool os_portable_copy_dir(const std::string& src, const std::string& dst) { - auto ret = std::filesystem::exists(src) && std::filesystem::exists(dst); - std::filesystem::copy(src, dst); - return ret; -#if 0 - int ret; -#if defined(_WIN32) || defined(_WIN64) - // on windows - ret = std::system( - ("xcopy " + os_portable_append_dir(src, "*") + " " + dst).c_str()); -#else - // on *nix - ret = std::system( - ("cp " + os_portable_append_dir(src, "*") + " " + dst).c_str()); -#endif - return ret == 0; -#endif + ILA_ASSERT(fs::is_directory(src) && fs::is_directory(dst)); + // fs::copy can only have one copy_options, + // either recursive or overwrite_existing + // therefore, we explicitly iterate through the hierarchy + for (auto& p : fs::recursive_directory_iterator(src)) { + if (fs::is_regular_file(p.path())) { + auto dst_p = fs::path(dst) / p.path().filename(); + try { + fs::copy_file(p.path(), dst_p, fs::copy_options::overwrite_existing); + } catch (fs::filesystem_error& e) { + ILA_ERROR << fmt::format("Fail copying file {} to {}", + p.path().string(), dst_p.string(), e.what()); + return false; + } + } + } + return true; } /// Copy the source file to the destination dir bool os_portable_copy_file_to_dir(const std::string& src, const std::string& dst) { - auto ret = std::filesystem::exists(src) && std::filesystem::exists(dst); - std::filesystem::copy(src, dst); - return ret; -#if 0 - int ret; -#if defined(_WIN32) || defined(_WIN64) - // on windows - ret = std::system(("xcopy " + src + " " + dst).c_str()); -#else - // on *nix - ret = std::system(("cp " + src + " " + dst).c_str()); -#endif - return ret == 0; -#endif + ILA_ASSERT(fs::is_regular_file(src) && fs::is_directory(dst)); + + try { + fs::copy(src, dst, fs::copy_options::overwrite_existing); + } catch (fs::filesystem_error& e) { + ILA_ERROR << e.what(); + return false; + } + + return true; } bool os_portable_move_file_to_dir(const std::string& src, const std::string& dst) { - auto ret = std::filesystem::exists(src) && std::filesystem::exists(dst); - std::filesystem::rename(src, dst); - return ret; -#if 0 -#if defined(_WIN32) || defined(_WIN64) - // on windows - // XXX need test - auto cmd = fmt::format("move /y {} {}", src, dst); -#else - // on *nix - auto cmd = fmt::format("mv {} {}", src, dst); -#endif - int ret = std::system(cmd.c_str()); - return ret == 0; -#endif + ILA_ASSERT(fs::is_regular_file(src) && fs::is_directory(dst)); + try { + fs::rename(src, dst); + } catch (fs::filesystem_error& e) { + ILA_ERROR << e.what(); + return false; + } + return true; } bool os_portable_remove_file(const std::string& file) { - return std::filesystem::remove(file); -#if 0 -#if defined(_WIN32) || defined(_WIN64) - // on windows - // XXX need test - auto cmd = fmt::format("del /q {}", file); -#else - // on *nix - auto cmd = fmt::format("rm {}", file); -#endif - int ret = std::system(cmd.c_str()); - return ret == 0; -#endif + ILA_ASSERT(fs::exists(file)); + try { + return fs::remove(file); + } catch (fs::filesystem_error& e) { + ILA_ERROR << e.what(); + return false; + } } /// Extract path from path @@ -208,61 +148,31 @@ bool os_portable_remove_file(const std::string& file) { /// C:\a\b\c -> C:\a\b /// d/e/ghi -> d/e/ std::string os_portable_path_from_path(const std::string& path) { - return std::filesystem::path(path).parent_path(); -#if 0 - std::string sep; -#if defined(_WIN32) || defined(_WIN64) - // on windows - sep = "\\"; -#else - // on *nix - sep = "/"; -#endif - if (path.find(sep) == path.npos) - return "." + sep; - auto pos = path.rfind(sep); - ILA_ASSERT(pos != path.npos); - return path.substr(0, pos + 1); // include sep + auto p = fs::path(path).parent_path().string(); + + // for backward compatibility + if (p.empty()) { +#if defined(_WIN32) || defined(_WIN64) // on windows + return ".\\"; +#else // on *nix + return "./"; #endif + } + + return p; } /// C:\\a.txt -> C:\\a or /a/b/c.txt -> a/b/c std::string os_portable_remove_file_name_extension(const std::string& fname) { - auto ret = std::filesystem::path(fname); - ret.replace_extension(); - return ret; -#if 0 - std::string sep; -#if defined(_WIN32) || defined(_WIN64) - // on windows - sep = "\\"; -#else - // on *nix - sep = "/"; -#endif - auto dot_pos = fname.rfind('.'); - if (dot_pos == std::string::npos) - return fname; // no dot - - auto sep_pos = fname.rfind(sep); - - if (sep_pos == std::string::npos) // no sep and only dot - return fname.substr(0, dot_pos); // remove after dot - - // no change ./../a -> ./../a - if (dot_pos < sep_pos) - return fname; - - // /.asdfaf.d -> /.asdfaf | /.a -> /. - return fname.substr(0, dot_pos); -#endif + auto name = fs::path(fname); + name.replace_extension(); + return name.string(); } bool os_portable_compare_file(const std::string& file1, const std::string& file2) { #if defined(_WIN32) || defined(_WIN64) // on windows - // XXX need test auto cmd = fmt::format("fc /a {} {}", file1, file2); #else // on *nix @@ -664,34 +574,7 @@ bool os_portable_chdir(const std::string& dirname) { /// Get the current directory std::string os_portable_getcwd() { - return std::filesystem::current_path(); -#if 0 -#if defined(_WIN32) || defined(_WIN64) - // windows - size_t len = GetCurrentDirectory(0, NULL); - char* buffer = new char[len + 1]; - if (GetCurrentDirectory(len, buffer) == 0) { - ILA_ERROR << "Unable to get the current working directory."; - delete[] buffer; - return ""; - } - std::string ret(buffer); - delete[] buffer; - return ret; -#else - // *nix - size_t buff_size = 128; - char* buffer = new char[buff_size]; - while (getcwd(buffer, buff_size) == NULL) { - delete[] buffer; - buff_size *= 2; - buffer = new char[buff_size]; // resize - } - std::string ret(buffer); - delete[] buffer; - return ret; -#endif -#endif + return fs::current_path().string(); } // os_portable_getcwd #if (defined(__unix__) || defined(unix) || defined(__APPLE__) || \ diff --git a/test/t_portable.cc b/test/t_portable.cc index 44fd4fed0..63f613db9 100644 --- a/test/t_portable.cc +++ b/test/t_portable.cc @@ -1,13 +1,15 @@ /// \file /// Unit tests for exporting and importing ILA portables. +#include + #include #include #include +#include #include "unit-include/config.h" #include "unit-include/util.h" -#include namespace ilang { @@ -19,15 +21,18 @@ void SerDes(const std::string& dir, const std::string& 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); + // char tmp_file_template[] = "/tmp/ila_XXXXXX"; + // auto tmp_file_name = GetRandomFileName(tmp_file_template); + auto tmp_file = GetRandomFileName(std::filesystem::temp_directory_path()); - ExportIlaPortable(ila, tmp_file_name); - auto des = ImportIlaPortable(tmp_file_name); + ExportIlaPortable(ila, tmp_file); + auto des = ImportIlaPortable(tmp_file); if (check) { Check(ila, des); } + + os_portable_remove_file(tmp_file); } TEST(TestPortable, AES_V_TOP) { SerDes("aes", "aes_v_top.json"); } diff --git a/test/t_util.cc b/test/t_util.cc index 8a6c89877..f69035fe7 100644 --- a/test/t_util.cc +++ b/test/t_util.cc @@ -1,14 +1,16 @@ /// \file /// Unit test for utility functions -#include "unit-include/config.h" -#include "unit-include/util.h" +#include +#include + #include #include -#include -namespace ilang { +#include "unit-include/config.h" +#include "unit-include/util.h" +namespace ilang { void RecordLog() { // precondition for log test @@ -36,7 +38,6 @@ void EndRecordLog() { EndRecordLog(); \ } while (0); - #if defined(_WIN32) || defined(_WIN64) TEST(TestUtil, DirAppend) { @@ -52,8 +53,7 @@ TEST(TestUtil, DirAppend) { EXPECT_ERROR(os_portable_append_dir("\\a\\", "\\b")); EXPECT_ERROR(os_portable_append_dir("\\a", "\\b")); - - EXPECT_EQ(os_portable_append_dir("a", {"b","c"}), "a\\b\\c"); + EXPECT_EQ(os_portable_append_dir("a", {"b", "c"}), "a\\b\\c"); } #else TEST(TestUtil, DirAppend) { @@ -70,25 +70,29 @@ TEST(TestUtil, DirAppend) { EXPECT_ERROR(os_portable_append_dir("/a/", "/b")); EXPECT_ERROR(os_portable_append_dir("/a", "/b")); - EXPECT_EQ(os_portable_append_dir("/a", std::vector({"b","c"})), "/a/b/c"); + EXPECT_EQ(os_portable_append_dir("/a", std::vector({"b", "c"})), + "/a/b/c"); } #endif - TEST(TestUtil, CopyDir) { - auto src_dir = - os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), - {"unit-data", "fs", "cpsrc"}); - auto dst_dir = - os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), - {"unit-data", "fs", "cpdst/"}); + auto src_dir = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "fs", "cpsrc"}); + auto dst_dir = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "fs", "cpdst"}); + auto dummy_path = os_portable_append_dir(dst_dir, "dummy"); + EXPECT_TRUE(os_portable_mkdir(dst_dir)); + EXPECT_TRUE(os_portable_copy_dir(src_dir, dst_dir)); - EXPECT_FALSE(os_portable_mkdir(os_portable_append_dir(dst_dir,"dummy"))); + EXPECT_TRUE(std::filesystem::exists(dummy_path)); + EXPECT_FALSE(std::filesystem::is_directory(dummy_path)); + EXPECT_FALSE(os_portable_mkdir(dummy_path)); + EXPECT_TRUE(std::filesystem::exists(dummy_path)); + EXPECT_FALSE(std::filesystem::is_directory(dummy_path)); } - #if defined(_WIN32) || defined(_WIN64) TEST(TestUtil, FileNameFromDir) { @@ -121,14 +125,15 @@ TEST(TestUtil, FileNameFromDir) { } #endif -#if defined(__unix__) || defined(unix) || defined(__APPLE__) || defined(__MACH__) || defined(__linux__) || defined(__FreeBSD__) +#if defined(__unix__) || defined(unix) || defined(__APPLE__) || \ + defined(__MACH__) || defined(__linux__) || defined(__FreeBSD__) TEST(TestUtil, ExecShell) { typedef std::vector P; - auto scriptName = - os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), - P({"unit-data", "shell_ex", "shell.sh"})); + auto scriptName = + os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + P({"unit-data", "shell_ex", "shell.sh"})); std::vector cmd; cmd.push_back("bash"); @@ -145,36 +150,35 @@ TEST(TestUtil, ExecShellOSPath) { EXPECT_EQ(res.failure, execute_result::NONE); } - TEST(TestUtil, ExecShellRedirect) { auto redirect_file = - os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), - {"unit-data", "shell_ex", "date_out.txt"}); + os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "shell_ex", "date_out.txt"}); auto pid_file = - os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), - {"unit-data", "shell_ex", "pid_out.txt"}); + os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "shell_ex", "pid_out.txt"}); auto scriptName = "date"; std::vector cmd; cmd.push_back(scriptName); execute_result res; - res = os_portable_execute_shell(cmd,redirect_file, BOTH,0,pid_file); + res = os_portable_execute_shell(cmd, redirect_file, BOTH, 0, pid_file); EXPECT_EQ(res.failure, execute_result::NONE); - + std::ifstream d1(redirect_file); std::string l1; EXPECT_TRUE(d1.is_open()); if (d1.is_open()) { - std::getline(d1,l1); + std::getline(d1, l1); d1.close(); } - + sleep(2); // wait for at ~ 2 seconds - res = os_portable_execute_shell(cmd,redirect_file, BOTH,0, pid_file); + res = os_portable_execute_shell(cmd, redirect_file, BOTH, 0, pid_file); EXPECT_EQ(res.failure, execute_result::NONE); std::ifstream d2(redirect_file); @@ -182,38 +186,34 @@ TEST(TestUtil, ExecShellRedirect) { EXPECT_TRUE(d2.is_open()); if (d2.is_open()) { - std::getline(d2,l2); + std::getline(d2, l2); d2.close(); } EXPECT_TRUE(l1 != l2); } - TEST(TestUtil, ExecShellRedirectTimeOut) { - auto redirect_file = - os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), - {"unit-data", "shell_ex", "sleep_out.txt"}); + auto redirect_file = + os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "shell_ex", "sleep_out.txt"}); std::vector s1cmd({"sleep", "1"}); std::vector s10cmd({"sleep", "10"}); execute_result res; - res = os_portable_execute_shell(s1cmd,redirect_file, BOTH, 5); + res = os_portable_execute_shell(s1cmd, redirect_file, BOTH, 5); EXPECT_TRUE(res.failure == execute_result::NONE); EXPECT_EQ(res.timeout, false); EXPECT_EQ(res.ret, 0); - res = os_portable_execute_shell(s10cmd,redirect_file, BOTH, 2); + res = os_portable_execute_shell(s10cmd, redirect_file, BOTH, 2); EXPECT_EQ(res.failure, execute_result::NONE); EXPECT_EQ(res.timeout, true); // EXPECT_EQ(res.ret, 0); if timeout return value not usable - } #endif - - TEST(TestUtil, RegularExpr) { if (IsRExprUsable()) { auto l = ReFindList("s1 == 2", "[A-Za-z0-9]+"); @@ -335,11 +335,12 @@ TEST(TestUtil, Int2Str) { } } -#define TestTrim(fa, in, out) { \ -std::string a = in; \ -fa (a); \ -EXPECT_EQ(a, out); \ -} +#define TestTrim(fa, in, out) \ + { \ + std::string a = in; \ + fa(a); \ + EXPECT_EQ(a, out); \ + } TEST(TestUtil, StrTrim) { TestTrim(StrLeftTrim, " dfs a b ", "dfs a b "); @@ -356,5 +357,4 @@ TEST(TestUtil, StrTrim) { TestTrim(StrTrim, " dfs a b ", "dfs a b"); } - } // namespace ilang diff --git a/test/t_verilog_gen.cc b/test/t_verilog_gen.cc index 4a1f07668..486aa6853 100644 --- a/test/t_verilog_gen.cc +++ b/test/t_verilog_gen.cc @@ -2,6 +2,7 @@ /// Unit test for Verilog parser. #include #include +#include #include #include @@ -18,62 +19,67 @@ namespace ilang { -void parseable(const std::string& fname, VerilogGenerator& vgen) { - std::ofstream fout(fname); - if (fout.is_open()) { - vgen.DumpToFile(fout); - fout.close(); - } else - ILA_WARN << "Cannot write tmpfile:" << fname << " for vlog-gen test."; - - int result = TestParseVerilogFrom(fname); - EXPECT_EQ(result, 0); - if (result != 0) - ILA_INFO << "ParseErrorFileName = " << fname; -} +class TestVerilogGen : public ::testing::Test { +public: + TestVerilogGen() { working_dir = std::filesystem::temp_directory_path(); } + ~TestVerilogGen() {} -void ParseIla(const InstrLvlAbsPtr& ila) { - // test 1 gen all : internal mem - { - SetLogLevel(2); - auto vgen = VerilogGenerator(); - vgen.ExportIla(ila); + void SetUp() {} - 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); + void TearDown() {} - char tmp_file_template[] = "/tmp/vlog_ext_XXXXXX"; - auto tmp_file_name = GetRandomFileName(tmp_file_template); - parseable(tmp_file_name, vgen); - } -} + std::filesystem::path working_dir; -void FlattenIla(const InstrLvlAbsPtr& ila) { + void Parseable(VerilogGenerator& vgen) { + auto fname = GetRandomFileName(working_dir); + std::ofstream fout(fname); + if (fout.is_open()) { + vgen.DumpToFile(fout); + fout.close(); + } else { + ILA_ERROR << "Fail writing file:" << fname; + } - for (auto i = 0; i < ila->instr_num(); i++) { - auto dep_ila = AbsKnob::ExtrDeptModl(ila->instr(i), "Flatten"); - AbsKnob::FlattenIla(dep_ila); + int result = TestParseVerilogFrom(fname); + EXPECT_EQ(result, 0); - auto vgen = VerilogGenerator(); - vgen.ExportIla(dep_ila); + os_portable_remove_file(fname); + } - char tmp_file_template[] = "/tmp/vlog_flat_XXXXXX"; - auto tmp_file_name = GetRandomFileName(tmp_file_template); - parseable(tmp_file_name, vgen); + void ParseIla(const InstrLvlAbsPtr& ila) { + // test 1 gen all : internal mem + { + SetLogLevel(2); + auto vgen = VerilogGenerator(); + vgen.ExportIla(ila); + Parseable(vgen); + } + // test 2 gen all : external mem + { + auto config = VerilogGenerator::VlgGenConfig( + true, VerilogGenerator::VlgGenConfig::funcOption::Internal); + auto vgen = VerilogGenerator(config); + vgen.ExportIla(ila); + Parseable(vgen); + } } -} -TEST(TestVerilogGen, Init) { VerilogGenerator(); } + 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); + Parseable(vgen); + } + } + +}; // TestVerilogGen + +TEST_F(TestVerilogGen, Init) { VerilogGenerator(); } -TEST(TestVerilogGen, VlgCnst) { +TEST_F(TestVerilogGen, VlgCnst) { EXPECT_EQ(VerilogGeneratorBase::ToVlgNum(1, 8), "8'h1"); EXPECT_EQ(VerilogGeneratorBase::ToVlgNum(255, 8), "8'hff"); EXPECT_EQ(VerilogGeneratorBase::ToVlgNum(0, 8), "8'h0"); @@ -112,7 +118,7 @@ TEST(TestVerilogGen, VlgCnst) { #endif } -TEST(TestVerilogGen, ParseInst) { +TEST_F(TestVerilogGen, ParseInst) { auto ila_ptr_ = SimpleCpu("proc"); // test 1 gen Add : internal mem { @@ -121,7 +127,7 @@ TEST(TestVerilogGen, ParseInst) { // DebugLog::Enable("VerilogGen.ParseNonMemUpdateExpr"); vgen.ExportTopLevelInstr(ila_ptr_->instr("Add")); - parseable(std::string(ILANG_TEST_BIN_ROOT) + "/t_proc_Add.v", vgen); + Parseable(vgen); } // test 2 gen Add : external mem { @@ -132,21 +138,21 @@ TEST(TestVerilogGen, ParseInst) { // DebugLog::Enable("VerilogGen.ParseNonMemUpdateExpr"); vgen.ExportTopLevelInstr(ila_ptr_->instr("Add")); - parseable(std::string(ILANG_TEST_BIN_ROOT) + "/t_proc_Add_extmem.v", vgen); + Parseable(vgen); } // test 3 gen Load : internal mem { auto vgen = VerilogGenerator(); // DebugLog::Enable("VerilogGen.ParseNonMemUpdateExpr"); vgen.ExportTopLevelInstr(ila_ptr_->instr("Load")); - parseable(std::string(ILANG_TEST_BIN_ROOT) + "/t_proc_Load.v", vgen); + Parseable(vgen); } // test 4 gen Store : internal mem { auto vgen = VerilogGenerator(); // DebugLog::Enable("VerilogGen.ParseNonMemUpdateExpr"); vgen.ExportTopLevelInstr(ila_ptr_->instr("Store")); - parseable(std::string(ILANG_TEST_BIN_ROOT) + "/t_proc_Store.v", vgen); + Parseable(vgen); } // test 5 gen Load : external mem { @@ -155,7 +161,7 @@ TEST(TestVerilogGen, ParseInst) { auto vgen = VerilogGenerator(config); // DebugLog::Enable("VerilogGen.ParseNonMemUpdateExpr"); vgen.ExportTopLevelInstr(ila_ptr_->instr("Load")); - parseable(std::string(ILANG_TEST_BIN_ROOT) + "/t_proc_Load_extmem.v", vgen); + Parseable(vgen); } // test 6 gen Store : external mem { @@ -164,25 +170,24 @@ TEST(TestVerilogGen, ParseInst) { auto vgen = VerilogGenerator(config); // DebugLog::Enable("VerilogGen.ParseNonMemUpdateExpr"); vgen.ExportTopLevelInstr(ila_ptr_->instr("Store")); - parseable(std::string(ILANG_TEST_BIN_ROOT) + "/t_proc_Store_extmem.v", - vgen); + Parseable(vgen); } } // TEST (ParseInst) -TEST(TestVerilogGen, CpReg) { +TEST_F(TestVerilogGen, CpReg) { EqIlaGen ila_gen; auto ila = ila_gen.GetIlaHier1("CpReg"); ParseIla(ila); FlattenIla(ila); } -TEST(TestVerilogGen, SimpleProc) { +TEST_F(TestVerilogGen, SimpleProc) { auto ila = SimpleCpu("proc"); ParseIla(ila); FlattenIla(ila); } -TEST(TestVerilogGen, AES_V) { +TEST_F(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); @@ -190,7 +195,7 @@ TEST(TestVerilogGen, AES_V) { FlattenIla(ila.get()); } -TEST(TestVerilogGen, AES_C) { +TEST_F(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); @@ -198,7 +203,7 @@ TEST(TestVerilogGen, AES_C) { FlattenIla(ila.get()); } -TEST(TestVerilogGen, GB_Low) { +TEST_F(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); @@ -206,7 +211,7 @@ TEST(TestVerilogGen, GB_Low) { FlattenIla(ila.get()); } -TEST(TestVerilogGen, RBM) { +TEST_F(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); @@ -214,7 +219,7 @@ TEST(TestVerilogGen, RBM) { FlattenIla(ila.get()); } -TEST(TestVerilogGen, OC) { +TEST_F(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); diff --git a/test/t_verilog_mod.cc b/test/t_verilog_mod.cc index 35872ad66..38bfd1b8e 100644 --- a/test/t_verilog_mod.cc +++ b/test/t_verilog_mod.cc @@ -2,12 +2,13 @@ /// Unit test for Verilog analyzer. #include #include +#include #include #include #include -#include #include +#include #include #include #include @@ -17,7 +18,6 @@ namespace ilang { - TEST(TestVerilogMod, Modify) { /* @@ -31,10 +31,9 @@ TEST(TestVerilogMod, Modify) { } */ - std::string fn = - os_portable_join_dir({ILANG_TEST_SRC_ROOT, "unit-data", "verilog_sample", "t_ana_insta.v"}); - std::string ofn = - os_portable_join_dir({ILANG_TEST_SRC_ROOT, "unit-data", "verilog_sample", "t_ana_insta_mod.v"}); + std::string fn = os_portable_join_dir( + {ILANG_TEST_SRC_ROOT, "unit-data", "verilog_sample", "t_ana_insta.v"}); + auto ofn = GetRandomFileName(std::filesystem::temp_directory_path()); VerilogInfo va(VerilogInfo::path_vec_t(), VerilogInfo::path_vec_t({fn}), "m1"); @@ -47,7 +46,7 @@ TEST(TestVerilogMod, Modify) { vm.RecordConnectSigName("m1.subm4.b"); vm.RecordConnectSigName("m1.n27"); vm.RecordConnectSigName("m1.ir"); - vm.RecordAdditionalVlgModuleStmt("wire abcd; assign abcd = 1'b1;","m1"); + vm.RecordAdditionalVlgModuleStmt("wire abcd; assign abcd = 1'b1;", "m1"); vm.FinishRecording(); std::ifstream fin(fn); @@ -64,6 +63,10 @@ TEST(TestVerilogMod, Modify) { } vm.ReadModifyWrite(fn, fin, fout); + + fin.close(); + fout.close(); + os_portable_remove_file(ofn); } -}; // namespace ilang +}; // namespace ilang diff --git a/test/unit-data/verilog_sample/.gitignore b/test/unit-data/verilog_sample/.gitignore deleted file mode 100644 index 47d6485d8..000000000 --- a/test/unit-data/verilog_sample/.gitignore +++ /dev/null @@ -1 +0,0 @@ -t_ana_insta_mod.v diff --git a/test/unit-include/util.h b/test/unit-include/util.h index 5be60e591..1c7e374c1 100644 --- a/test/unit-include/util.h +++ b/test/unit-include/util.h @@ -34,7 +34,7 @@ void EndRecordLog(); cmd; \ msg = ::testing::internal::GetCapturedStderr(); -std::string GetRandomFileName(char* file_name_template); +std::string GetRandomFileName(const std::string& dir); void CheckIlaEqLegacy(const InstrLvlAbsPtr& a, const InstrLvlAbsPtr& b); diff --git a/test/unit-src/util.cc b/test/unit-src/util.cc index 260445f2c..4b7a8a261 100644 --- a/test/unit-src/util.cc +++ b/test/unit-src/util.cc @@ -4,32 +4,40 @@ #include "../unit-include/util.h" #include +#include +#include #include namespace ilang { -std::string GetRandomFileName(char* file_name_template) { - ILA_NOT_NULL(file_name_template); +namespace fs = std::filesystem; -#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); +static const std::string CHARACTERS = + "0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz"; -#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); +std::string random_string(std::size_t length) { + std::random_device random_device; + std::mt19937 generator(random_device()); + std::uniform_int_distribution<> distribution(0, CHARACTERS.size() - 1); -#else - ILA_WARN << "tmpnam may be deprecated -- find alternatives"; - auto fn = std::tmpnam(NULL); - return static_cast(fn); + std::string random_string; -#endif + for (std::size_t i = 0; i < length; ++i) { + random_string += CHARACTERS[distribution(generator)]; + } + + return random_string; +} + +std::string GetRandomFileName(const std::string& dir) { + ILA_ASSERT(fs::is_directory(dir)) << dir << " doesn't exist"; + + auto file_name = fs::path(random_string(6)); + while (fs::exists(fs::path(dir) / file_name)) { + file_name = fs::path(random_string(6)); + } + return (dir / file_name).string(); } void CheckIlaEqLegacy(const InstrLvlAbsPtr& a, const InstrLvlAbsPtr& b) { From f509a74066fcd5e18997bc9a3c214370b2934666 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 8 Jun 2020 17:30:06 -0400 Subject: [PATCH 05/21] Cleanup unit tests --- test/CMakeLists.txt | 1 - test/t_case_aes_eq.cc | 6 +++--- test/t_eq_check.cc | 19 ------------------- test/t_expr_const.cc | 2 +- test/t_expr_op.cc | 4 ++-- test/t_hash_ast.cc | 4 ++-- test/t_instr.cc | 18 ------------------ test/t_legacy_bmc.cc | 4 ++-- test/t_op_sanity.cc | 40 ---------------------------------------- test/t_pass.cc | 2 +- test/t_portable.cc | 2 -- test/t_unroll_seq.cc | 8 ++++---- test/t_util.cc | 10 +++++++--- test/t_validate_model.cc | 4 +++- test/t_z3adapter.cc | 4 ---- 15 files changed, 25 insertions(+), 103 deletions(-) delete mode 100644 test/t_op_sanity.cc diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index fdc8653c7..fcc979a87 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -69,7 +69,6 @@ package_add_test(${ILANG_TEST_MAIN} t_main.cc t_mapset.cc t_mcm.cc - t_op_sanity.cc t_pass.cc t_portable.cc t_sort.cc diff --git a/test/t_case_aes_eq.cc b/test/t_case_aes_eq.cc index 3d8b4495a..9d9f5c214 100644 --- a/test/t_case_aes_eq.cc +++ b/test/t_case_aes_eq.cc @@ -13,9 +13,11 @@ namespace ilang { TEST(TestCase, AES_V_C_EQ) { SetToStdErr(0); +#if 0 DebugLog::Enable("CaseAesEq"); DebugLog::Enable("EqCheck"); DebugLog::Enable("Verbose-CrrEqCheck"); +#endif // get the ILA model auto aes_dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, "aes"); @@ -110,8 +112,6 @@ TEST(TestCase, AES_V_C_EQ) { auto refinement_v = DefaultRefinement(m_v, start_v); auto refinement_c = DefaultRefinement(m_c, start_c); - // invariant TODO - // check auto crr = CompRefRel::New(refinement_v, refinement_c, relation); z3::context ctx; @@ -119,7 +119,7 @@ TEST(TestCase, AES_V_C_EQ) { cd.IncCheck(10, 50, 50); - SetToStdErr(0); + // SetToStdErr(0); DebugLog::Disable("CaseAesEq"); DebugLog::Disable("EqCheck"); DebugLog::Disable("Verbose-CrrEqCheck"); diff --git a/test/t_eq_check.cc b/test/t_eq_check.cc index 339a0d585..92ecece74 100644 --- a/test/t_eq_check.cc +++ b/test/t_eq_check.cc @@ -23,7 +23,6 @@ class TestEqCheck : public ::testing::Test { DebugLog::Enable("Verbose-CrrEqCheck"); } void TearDown() { - SetToStdErr(0); DebugLog::Disable("EqCheck"); DebugLog::Disable("Verbose-CrrEqCheck"); } @@ -36,7 +35,6 @@ class TestEqCheck : public ::testing::Test { InstrLvlAbsPtr f1 = ila_gen.GetIlaFlat1("f1"); InstrLvlAbsPtr f2 = ila_gen.GetIlaFlat2("f2"); InstrLvlAbsPtr h1 = ila_gen.GetIlaHier1("h1"); - // InstrLvlAbsPtr h2 = ila_gen.GetIlaHier2("h2"); RefPtr GetRefine(const InstrLvlAbsPtr top, const int& instr_idx, bool comp, bool flat); @@ -48,7 +46,6 @@ class TestEqCheck : public ::testing::Test { }; TEST_F(TestEqCheck, FF_Mono) { - SetToStdErr(0); for (auto instr_idx : {0, 1, 2, 3}) { // refinement auto ref1 = GetRefine(f1, instr_idx, false, true); @@ -68,7 +65,6 @@ TEST_F(TestEqCheck, FF_Mono) { } TEST_F(TestEqCheck, CommDiag_HF) { - SetToStdErr(0); // DebugLog::Disable("Verbose-CrrEqCheck"); for (auto instr_idx : {0}) { // refinement @@ -84,12 +80,10 @@ TEST_F(TestEqCheck, CommDiag_HF) { CustH1(ref2); EXPECT_TRUE(cd.EqCheck(100)); - // EXPECT_TRUE(cd.EqCheck(20)); } } TEST_F(TestEqCheck, IncCommDiag_HF) { - SetToStdErr(0); // DebugLog::Disable("Verbose-CrrEqCheck"); for (auto instr_idx : {0}) { // refinement @@ -104,13 +98,11 @@ TEST_F(TestEqCheck, IncCommDiag_HF) { CustF1(ref1); CustH1(ref2); - // EXPECT_TRUE(cd.IncEqCheck(0, 20)); EXPECT_TRUE(cd.IncEqCheck(0, 90, 10)); } } TEST_F(TestEqCheck, NewIncCommDiag_HF) { - SetToStdErr(0); // DebugLog::Disable("Verbose-CrrEqCheck"); for (auto instr_idx : {0}) { // refinement @@ -130,17 +122,6 @@ TEST_F(TestEqCheck, NewIncCommDiag_HF) { } } -TEST_F(TestEqCheck, CommDiag_HH) { - // TODO - // with and without completion -} - -TEST_F(TestEqCheck, CommDiag_Pipeline) { - ExmpStrmBuff sb; - auto m = sb.GetStrmBuffSpecRaw("spec"); - // TODO -} - RefPtr TestEqCheck::GetRefine(const InstrLvlAbsPtr top, const int& instr_idx, bool comp, bool flat) { auto ref = RefinementMap::New(); diff --git a/test/t_expr_const.cc b/test/t_expr_const.cc index ba4647760..2899c4aef 100644 --- a/test/t_expr_const.cc +++ b/test/t_expr_const.cc @@ -168,7 +168,7 @@ TEST(TestExprConst, BvConstBitwidth) { } TEST(TestExprConst, BvConstNumeric) { - SetToStdErr(1); + // SetToStdErr(1); // 8-bit EXPECT_EQ(BVCONST(0, 8)->val_bv()->val(), 0); diff --git a/test/t_expr_op.cc b/test/t_expr_op.cc index a1952a8e0..2b3a0fa8b 100644 --- a/test/t_expr_op.cc +++ b/test/t_expr_op.cc @@ -14,12 +14,12 @@ class TestExprOp : public ::testing::Test { void SetUp() { s.reset(); - SetToStdErr(1); + // SetToStdErr(1); DebugLog::Enable("TestExprOp"); } void TearDown() { - SetToStdErr(0); + // SetToStdErr(0); DebugLog::Disable("TestExprOp"); } diff --git a/test/t_hash_ast.cc b/test/t_hash_ast.cc index 83e79b1ab..9b3beed54 100644 --- a/test/t_hash_ast.cc +++ b/test/t_hash_ast.cc @@ -27,12 +27,12 @@ class TestHashApi : public ::testing::Test { void SetUp() { DebugLog::Enable("HashApi"); - SetToStdErr(1); + // SetToStdErr(1); } void TearDown() { DebugLog::Disable("HashApi"); - SetToStdErr(0); + // SetToStdErr(0); } InstrLvlAbsPtr ila = NULL; diff --git a/test/t_instr.cc b/test/t_instr.cc index 9e8630e04..f3f21ac08 100644 --- a/test/t_instr.cc +++ b/test/t_instr.cc @@ -37,24 +37,6 @@ TEST_F(TestInstr, Construct) { EXPECT_FALSE(eptr->is_ast()); EXPECT_FALSE(eptr->has_view()); - -#if 0 - InstrPtr nptr = std::make_shared(); - - EXPECT_TRUE(nptr->is_instr()); - EXPECT_FALSE(nptr->is_instr_lvl_abs()); - EXPECT_FALSE(nptr->is_ast()); - - EXPECT_FALSE(nptr->has_view()); - - InstrPtr hptr = Instr::New(); - - EXPECT_TRUE(hptr->is_instr()); - EXPECT_FALSE(hptr->is_instr_lvl_abs()); - EXPECT_FALSE(hptr->is_ast()); - - EXPECT_FALSE(hptr->has_view()); -#endif } TEST_F(TestInstr, View) { diff --git a/test/t_legacy_bmc.cc b/test/t_legacy_bmc.cc index e539080c5..8d6474626 100644 --- a/test/t_legacy_bmc.cc +++ b/test/t_legacy_bmc.cc @@ -11,7 +11,7 @@ namespace ilang { TEST(TestLegacyBmc, FF) { - SetToStdErr(0); + // SetToStdErr(0); DebugLog::Enable("Bmc.Legacy"); DebugLog::Enable("ModelGen.IlaOneHotFlat"); @@ -52,7 +52,7 @@ TEST(TestLegacyBmc, FF) { DebugLog::Disable("ModelGen.IlaOneHotFlat"); DebugLog::Disable("ModelGen.Instr"); - SetToStdErr(0); + // SetToStdErr(0); } } // namespace ilang diff --git a/test/t_op_sanity.cc b/test/t_op_sanity.cc deleted file mode 100644 index 79288ffa6..000000000 --- a/test/t_op_sanity.cc +++ /dev/null @@ -1,40 +0,0 @@ -/// \file -/// Unit test for operation construction, z3 formula, hash, print, etc. - -#include "unit-include/util.h" -#include - -namespace ilang { - -class TestOpSanity : public ::testing::Test { -public: - TestOpSanity() { - m = new Ila("host"); - // TODO - } - - ~TestOpSanity() { - if (m) - delete m; - } - - void SetUp() { - DebugLog::Enable("OpSanity"); - SetToStdErr(1); - } - - void TearDown() { - DebugLog::Disable("OpSanity"); - SetToStdErr(0); - } - - Ila* m = NULL; - -}; // class TestOpSanity - -TEST_F(TestOpSanity, AndBool) { - // TODO - // Need to have a API for node equivalence (semantically). -} - -} // namespace ilang diff --git a/test/t_pass.cc b/test/t_pass.cc index 6962f134c..e569a4344 100644 --- a/test/t_pass.cc +++ b/test/t_pass.cc @@ -12,7 +12,7 @@ namespace ilang { void ApplyPass(const std::string& dir, const std::string& file, bool simplify = true) { - SetToStdErr(true); + // SetToStdErr(true); EnableDebug("PassSimpInstrUpdate"); EnableDebug("PassRewrCondStore"); diff --git a/test/t_portable.cc b/test/t_portable.cc index 63f613db9..1ef11197d 100644 --- a/test/t_portable.cc +++ b/test/t_portable.cc @@ -21,8 +21,6 @@ void SerDes(const std::string& dir, const std::string& 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); auto tmp_file = GetRandomFileName(std::filesystem::temp_directory_path()); ExportIlaPortable(ila, tmp_file); diff --git a/test/t_unroll_seq.cc b/test/t_unroll_seq.cc index 18c5329c6..aa2173a2f 100644 --- a/test/t_unroll_seq.cc +++ b/test/t_unroll_seq.cc @@ -26,7 +26,7 @@ class TestUnroll : public ::testing::Test { init_mem = MemConst(init_mem_val, 8, 8); } void TearDown() { - SetToStdErr(0); + // SetToStdErr(0); DebugLog::Disable("Unroller"); } @@ -72,7 +72,7 @@ TEST_F(TestUnroll, InstrSeqFlatNone) { } TEST_F(TestUnroll, InstrSeqSolve) { - SetToStdErr(1); + // SetToStdErr(1); auto m0 = SimpleCpu("m0"); auto m1 = SimpleCpu("m1"); @@ -170,7 +170,7 @@ TEST_F(TestUnroll, MonoFlatNone) { } TEST_F(TestUnroll, MonoSolve) { - SetToStdErr(1); + // SetToStdErr(1); auto m0 = SimpleCpu("m0"); auto m1 = SimpleCpu("m1"); @@ -245,7 +245,7 @@ TEST_F(TestUnroll, MonoSolve) { } TEST_F(TestUnroll, PathMonoSolve) { - SetToStdErr(1); + // SetToStdErr(1); auto m0 = SimpleCpu("m0"); auto m1 = SimpleCpu("m1"); diff --git a/test/t_util.cc b/test/t_util.cc index f69035fe7..d1ea374c6 100644 --- a/test/t_util.cc +++ b/test/t_util.cc @@ -14,20 +14,24 @@ namespace ilang { void RecordLog() { // precondition for log test +#if 0 SetLogLevel(0); // log all SetLogPath(""); // log to /tmp SetToStdErr(1); // log to stderr for easy catching +#endif } void EndRecordLog() { - // reset to default condition +// reset to default condition +#if 0 SetLogLevel(0); // log all SetLogPath(""); // log to /tmp #ifndef NDEBUG SetToStdErr(0); // still log to stderr -#else // NDEBUG +#else // NDEBUG SetToStdErr(0); // not log to stderr -#endif // NDEBUG +#endif // NDEBUG +#endif } #define EXPECT_ERROR(m) \ diff --git a/test/t_validate_model.cc b/test/t_validate_model.cc index 48a8e4013..7cb33e24c 100644 --- a/test/t_validate_model.cc +++ b/test/t_validate_model.cc @@ -15,7 +15,9 @@ class TestValidateModel : public ::testing::Test { TestValidateModel() {} ~TestValidateModel() {} - void SetUp() { SetToStdErr(1); } + void SetUp() { + // SetToStdErr(1); + } void TearDown() {} diff --git a/test/t_z3adapter.cc b/test/t_z3adapter.cc index a018cc344..0974804cc 100644 --- a/test/t_z3adapter.cc +++ b/test/t_z3adapter.cc @@ -76,8 +76,4 @@ TEST(TestZ3Adapter, Suffix) { DebugLog::Disable("z3_adapter"); } -// TODO simplify -// TODO change context -// TODO Clear - } // namespace ilang From ffb20d404f294d5eda032e514abe0f3daea54f98 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 10 Jun 2020 10:52:33 -0400 Subject: [PATCH 06/21] Set ILANG_BUILD_SYNTH to default off --- .semaphore/semaphore.yml | 2 +- .travis.yml | 3 --- CMakeLists.txt | 2 +- README.md | 10 +++++----- appveyor.yml | 17 +++++++++++++++++ azure-pipelines.yml | 14 +++++--------- scripts/travis/build-osx.sh | 2 +- scripts/travis/build.sh | 2 +- 8 files changed, 31 insertions(+), 21 deletions(-) create mode 100644 appveyor.yml diff --git a/.semaphore/semaphore.yml b/.semaphore/semaphore.yml index 2e6ebd8ff..1e1c1c1fe 100644 --- a/.semaphore/semaphore.yml +++ b/.semaphore/semaphore.yml @@ -19,7 +19,7 @@ blocks: - export CXX=g++-7 - mkdir build - cd build - - cmake .. -DCMAKE_BUILD_TYPE=Debug + - cmake .. -DCMAKE_BUILD_TYPE=Debug -DILANG_BUILD_SYNTH=ON - make -j$(nproc) - sudo make install - make run_test diff --git a/.travis.yml b/.travis.yml index 030894222..3d5922570 100644 --- a/.travis.yml +++ b/.travis.yml @@ -73,7 +73,6 @@ matrix: packages: - flex - bison - - libboost-all-dev - z3 - libz3-dev before_install: @@ -98,8 +97,6 @@ addons: packages: - flex - python - - boost - - boost-python - z3 notifications: diff --git a/CMakeLists.txt b/CMakeLists.txt index 46face01e..deea64e6e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -22,7 +22,7 @@ project(ilang VERSION 1.0.4 # ---------------------------------------------------------------------------- # option(ILANG_FETCH_DEPS "Fetch source of dependencies at config time." ON) option(ILANG_BUILD_DOCS "Build documentations." OFF) -option(ILANG_BUILD_SYNTH "Build the synthesis engine." ON) +option(ILANG_BUILD_SYNTH "Build the synthesis engine." OFF) option(ILANG_INSTALL_DEV "Install dev features." OFF) option(ILANG_EXPORT_PACKAGE "Export CMake package if enabled." OFF) option(ILANG_COVERITY "Build for Coverity static analysis." OFF) diff --git a/README.md b/README.md index 1351c03fe..88bccec97 100644 --- a/README.md +++ b/README.md @@ -65,10 +65,10 @@ brew install bison flex boost boost-python z3 | Ubuntu 18.04 (Bionic) | clang 6.0.0 | 3.10.2 | 4.4.1 | 1.65 | 3.0.4 | 2.6.4 | Debug | | Ubuntu 18.04 (Bionic) | gcc 7.5.0 | 3.10.2 | 4.4.1 | 1.65 | 3.0.4 | 2.6.4 | Debug | | Ubuntu 18.04 (Bionic) | gcc 7.5.0 | 3.17.0 | 4.4.1 | 1.65 | 3.0.4 | 2.6.4 | Release | -| Ubuntu 20.04 (Focal Fosa) | gcc 7.4.0 | 3.17.0 | 4.4.1 | 1.65 | 3.0.4 | 2.6.4 | Release | -| OSX 10.13.6 (High Sierra) | Xcode 9.4.1 | 3.15.5 | 4.8.8 | 1.72 | 3.6.2 | 2.5.35 | Release | -| OSX 10.14.6 (Mojave) | Xcode 11.3.1 | 3.17.2 | 4.8.8 | 1.72 | 3.6.2 | 2.5.35 | Release | -| OSX 10.15.4 (Catalina) | Xcode 11.4.1 | 3.17.2 | 4.8.8 | 1.72 | 3.6.2 | 2.5.35 | Release | +| Ubuntu 20.04 (Focal Fosa) | gcc 7.4.0 | 3.17.0 | 4.4.1 | - | 3.0.4 | 2.6.4 | Release | +| OSX 10.13.6 (High Sierra) | Xcode 9.4.1 | 3.15.5 | 4.8.8 | - | 3.6.2 | 2.5.35 | Release | +| OSX 10.14.6 (Mojave) | Xcode 11.3.1 | 3.17.2 | 4.8.8 | - | 3.6.2 | 2.5.35 | Release | +| OSX 10.15.4 (Catalina) | Xcode 11.4.1 | 3.17.2 | 4.8.8 | - | 3.6.2 | 2.5.35 | Release | | Windows Server 2016 | VS 2017 | 3.17.2 | 4.8.8 | - | 3.3.2 | 2.6.4 | Release | ### Default Build @@ -100,7 +100,7 @@ sudo make install - Use `-DILANG_FETCH_DEPS=OFF` to disable config-time updating submodules for in-source dependencies. - Use `-DILANG_BUILD_TEST=OFF` to disalbe building the unit tests. -- Use `-DILANG_BUILD_SYNTH=OFF` to disable building the synthesis engine. +- Use `-DILANG_BUILD_SYNTH=ON` to enable building the synthesis engine. - Use `-DILANG_BUILD_INVSYN=ON` to enable building invariant synthesis feature. - Use `-DILANG_BUILD_SWITCH=ON` to enable building [smt-switch](https://github.com/makaimann/smt-switch.git) interface support. - Use `-DILANG_INSTALL_DEV=ON` to install working features. diff --git a/appveyor.yml b/appveyor.yml new file mode 100644 index 000000000..055abebc9 --- /dev/null +++ b/appveyor.yml @@ -0,0 +1,17 @@ +version: 1.0.{build} +image: Ubuntu2004 +clone_depth: 1 + +install: +- sudo apt update --yes +- sudo apt install --yes z3 libz3-dev bison flex + +build_script: +- cd $APPVEYOR_BUILD_FOLDER +- mkdir -p build +- cd build +- cmake .. -DCMAKE_BUILD_TYPE=Release +- make -j$(nproc) +- sudo make install +- make test +- cmake --version diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 8956515fb..3f8bb2b4b 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -14,8 +14,6 @@ jobs: - script: | brew update brew install bison - brew install boost - brew install boost-python brew install z3 displayName: 'package' - script: | @@ -27,7 +25,7 @@ jobs: export LDFLAGS="-L/usr/local/opt/bison/lib" mkdir -p build cd build - cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON -DILANG_BUILD_INVSYN=OFF + cmake .. -DCMAKE_BUILD_TYPE=Release cmake --build . cmake --build . --target install cmake --build . --target test @@ -40,8 +38,6 @@ jobs: - script: | brew update brew install bison - brew install boost - brew install boost-python brew install z3 displayName: 'package' - script: | @@ -53,7 +49,7 @@ jobs: export LDFLAGS="-L/usr/local/opt/bison/lib" mkdir -p build cd build - cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON -DILANG_BUILD_INVSYN=OFF + cmake .. -DCMAKE_BUILD_TYPE=Release cmake --build . cmake --build . --target install cmake --build . --target test @@ -74,7 +70,7 @@ jobs: - script: | mkdir -p build cd build - cmake .. -DCMAKE_BUILD_TYPE=Release + cmake .. -DCMAKE_BUILD_TYPE=Release -DILANG_BUILD_SYNTH=ON cmake --build . sudo cmake --build . --target install cmake --build . --target test @@ -95,7 +91,7 @@ jobs: - script: | mkdir -p build cd build - cmake .. -DCMAKE_BUILD_TYPE=Release + cmake .. -DCMAKE_BUILD_TYPE=Release -DILANG_BUILD_SYNTH=ON cmake --build . sudo cmake --build . --target install cmake --build . --target test @@ -148,7 +144,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 -DILANG_BUILD_INVSYN=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_TEST=OFF -DBUILD_SHARED_LIBS=OFF -DILANG_BUILD_INVSYN=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' diff --git a/scripts/travis/build-osx.sh b/scripts/travis/build-osx.sh index b65547871..c04964a37 100644 --- a/scripts/travis/build-osx.sh +++ b/scripts/travis/build-osx.sh @@ -29,7 +29,7 @@ CI_BUILD_DIR=$1 cd $CI_BUILD_DIR mkdir -p build cd build -cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON +cmake .. -DCMAKE_BUILD_TYPE=Release make -j$(nproc) sudo make install make run_test diff --git a/scripts/travis/build.sh b/scripts/travis/build.sh index 05def505d..3d4f23e38 100644 --- a/scripts/travis/build.sh +++ b/scripts/travis/build.sh @@ -38,7 +38,7 @@ sudo make install cd $CI_BUILD_DIR mkdir -p build cd build -cmake .. -DCMAKE_BUILD_TYPE=Debug -DILANG_BUILD_COV=ON -DILANG_BUILD_SWITCH=ON +cmake .. -DCMAKE_BUILD_TYPE=Debug -DILANG_BUILD_COV=ON -DILANG_BUILD_SWITCH=ON -DILANG_BUILD_SYNTH=ON make -j$(nproc) sudo make install make run_test From 642a85af8316cab711511690fccdf485d0adf154 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 10 Jun 2020 11:21:42 -0400 Subject: [PATCH 07/21] Add experimental suffix to support GCC < 8 --- src/util/fs.cc | 4 ++-- test/t_portable.cc | 6 ++++-- test/t_util.cc | 12 +++++++----- test/t_verilog_gen.cc | 8 +++++--- test/t_verilog_mod.cc | 6 ++++-- test/unit-src/util.cc | 4 ++-- 6 files changed, 24 insertions(+), 16 deletions(-) diff --git a/src/util/fs.cc b/src/util/fs.cc index 2038aaf2f..e975f5af4 100644 --- a/src/util/fs.cc +++ b/src/util/fs.cc @@ -9,7 +9,7 @@ #include #include -#include +#include #include #include @@ -36,7 +36,7 @@ namespace ilang { -namespace fs = std::filesystem; +namespace fs = std::experimental::filesystem; /// Create a dir, true -> suceeded , ow false bool os_portable_mkdir(const std::string& dir) { diff --git a/test/t_portable.cc b/test/t_portable.cc index 1ef11197d..51283017f 100644 --- a/test/t_portable.cc +++ b/test/t_portable.cc @@ -1,7 +1,7 @@ /// \file /// Unit tests for exporting and importing ILA portables. -#include +#include #include #include @@ -13,6 +13,8 @@ namespace ilang { +namespace fs = std::experimental::filesystem; + void Check(Ila& a, Ila& b) { CheckIlaEqLegacy(a.get(), b.get()); } void SerDes(const std::string& dir, const std::string& file, @@ -21,7 +23,7 @@ void SerDes(const std::string& dir, const std::string& file, auto ila_file = os_portable_append_dir(file_dir, file); auto ila = ImportIlaPortable(ila_file); - auto tmp_file = GetRandomFileName(std::filesystem::temp_directory_path()); + auto tmp_file = GetRandomFileName(fs::temp_directory_path()); ExportIlaPortable(ila, tmp_file); auto des = ImportIlaPortable(tmp_file); diff --git a/test/t_util.cc b/test/t_util.cc index d1ea374c6..38ca63a60 100644 --- a/test/t_util.cc +++ b/test/t_util.cc @@ -1,7 +1,7 @@ /// \file /// Unit test for utility functions -#include +#include #include #include @@ -12,6 +12,8 @@ namespace ilang { +namespace fs = std::experimental::filesystem; + void RecordLog() { // precondition for log test #if 0 @@ -89,12 +91,12 @@ TEST(TestUtil, CopyDir) { EXPECT_TRUE(os_portable_mkdir(dst_dir)); EXPECT_TRUE(os_portable_copy_dir(src_dir, dst_dir)); - EXPECT_TRUE(std::filesystem::exists(dummy_path)); - EXPECT_FALSE(std::filesystem::is_directory(dummy_path)); + EXPECT_TRUE(fs::exists(dummy_path)); + EXPECT_FALSE(fs::is_directory(dummy_path)); EXPECT_FALSE(os_portable_mkdir(dummy_path)); - EXPECT_TRUE(std::filesystem::exists(dummy_path)); - EXPECT_FALSE(std::filesystem::is_directory(dummy_path)); + EXPECT_TRUE(fs::exists(dummy_path)); + EXPECT_FALSE(fs::is_directory(dummy_path)); } #if defined(_WIN32) || defined(_WIN64) diff --git a/test/t_verilog_gen.cc b/test/t_verilog_gen.cc index 486aa6853..00d41b0cf 100644 --- a/test/t_verilog_gen.cc +++ b/test/t_verilog_gen.cc @@ -2,7 +2,7 @@ /// Unit test for Verilog parser. #include #include -#include +#include #include #include @@ -19,16 +19,18 @@ namespace ilang { +namespace fs = std::experimental::filesystem; + class TestVerilogGen : public ::testing::Test { public: - TestVerilogGen() { working_dir = std::filesystem::temp_directory_path(); } + TestVerilogGen() { working_dir = fs::temp_directory_path(); } ~TestVerilogGen() {} void SetUp() {} void TearDown() {} - std::filesystem::path working_dir; + fs::path working_dir; void Parseable(VerilogGenerator& vgen) { auto fname = GetRandomFileName(working_dir); diff --git a/test/t_verilog_mod.cc b/test/t_verilog_mod.cc index 38bfd1b8e..50dc42132 100644 --- a/test/t_verilog_mod.cc +++ b/test/t_verilog_mod.cc @@ -2,7 +2,7 @@ /// Unit test for Verilog analyzer. #include #include -#include +#include #include #include @@ -18,6 +18,8 @@ namespace ilang { +namespace fs = std::experimental::filesystem; + TEST(TestVerilogMod, Modify) { /* @@ -33,7 +35,7 @@ TEST(TestVerilogMod, Modify) { std::string fn = os_portable_join_dir( {ILANG_TEST_SRC_ROOT, "unit-data", "verilog_sample", "t_ana_insta.v"}); - auto ofn = GetRandomFileName(std::filesystem::temp_directory_path()); + auto ofn = GetRandomFileName(fs::temp_directory_path()); VerilogInfo va(VerilogInfo::path_vec_t(), VerilogInfo::path_vec_t({fn}), "m1"); diff --git a/test/unit-src/util.cc b/test/unit-src/util.cc index 4b7a8a261..c22d31c99 100644 --- a/test/unit-src/util.cc +++ b/test/unit-src/util.cc @@ -4,14 +4,14 @@ #include "../unit-include/util.h" #include -#include +#include #include #include namespace ilang { -namespace fs = std::filesystem; +namespace fs = std::experimental::filesystem; static const std::string CHARACTERS = "0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz"; From c253c703d3478b4751141f76e23cbe444b62a3e7 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 10 Jun 2020 15:11:50 -0400 Subject: [PATCH 08/21] Fix missing config --- test/t_expr_const.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/t_expr_const.cc b/test/t_expr_const.cc index 2899c4aef..ba4647760 100644 --- a/test/t_expr_const.cc +++ b/test/t_expr_const.cc @@ -168,7 +168,7 @@ TEST(TestExprConst, BvConstBitwidth) { } TEST(TestExprConst, BvConstNumeric) { - // SetToStdErr(1); + SetToStdErr(1); // 8-bit EXPECT_EQ(BVCONST(0, 8)->val_bv()->val(), 0); From 405654f576372d7167abd5a706bc1f229ed88434 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 10 Jun 2020 22:02:26 -0400 Subject: [PATCH 09/21] Clean up log setup in tests --- test/t_log.cc | 4 ---- test/t_util.cc | 10 +--------- 2 files changed, 1 insertion(+), 13 deletions(-) diff --git a/test/t_log.cc b/test/t_log.cc index 3e3aaa0ea..03fc6b5b8 100644 --- a/test/t_log.cc +++ b/test/t_log.cc @@ -22,11 +22,7 @@ class TestLog : public ::testing::Test { // reset to default condition SetLogLevel(0); // log all SetLogPath(""); // log to /tmp -#ifndef NDEBUG - SetToStdErr(0); // still log to stderr -#else // NDEBUG SetToStdErr(0); // not log to stderr -#endif // NDEBUG } }; // Log test fixture diff --git a/test/t_util.cc b/test/t_util.cc index 38ca63a60..4b492a1ce 100644 --- a/test/t_util.cc +++ b/test/t_util.cc @@ -16,24 +16,16 @@ namespace fs = std::experimental::filesystem; void RecordLog() { // precondition for log test -#if 0 SetLogLevel(0); // log all SetLogPath(""); // log to /tmp SetToStdErr(1); // log to stderr for easy catching -#endif } void EndRecordLog() { -// reset to default condition -#if 0 + // reset to default condition SetLogLevel(0); // log all SetLogPath(""); // log to /tmp -#ifndef NDEBUG - SetToStdErr(0); // still log to stderr -#else // NDEBUG SetToStdErr(0); // not log to stderr -#endif // NDEBUG -#endif } #define EXPECT_ERROR(m) \ From d481faf7d00f74576a361699e3ca0761e7e380e3 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 10 Jun 2020 22:24:54 -0400 Subject: [PATCH 10/21] Distinguish c++17 support at build config time --- src/CMakeLists.txt | 5 +++++ src/config.h.in | 2 ++ src/util/fs.cc | 12 +++++++++++- test/t_portable.cc | 4 ---- test/t_util.cc | 3 --- test/t_verilog_gen.cc | 3 --- test/t_verilog_mod.cc | 3 --- test/unit-include/util.h | 12 ++++++++++++ test/unit-src/util.cc | 3 --- 9 files changed, 30 insertions(+), 17 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index a040a0f46..6a8d44f05 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -57,6 +57,9 @@ target_include_directories(${ILANG_LIB_NAME} $ ) +# check if c++17 filesystem is available +CHECK_INCLUDE_FILE_CXX(filesystem FS_INCLUDE) + # ---------------------------------------------------------------------------- # # LINK LIBRARIES # external dependencies @@ -64,7 +67,9 @@ target_include_directories(${ILANG_LIB_NAME} ## ## std::filesystem ## +if(NOT APPLE) target_link_libraries(${ILANG_LIB_NAME} PRIVATE stdc++fs) +endif() ## ## gcov diff --git a/src/config.h.in b/src/config.h.in index 83b191766..73dee04ab 100644 --- a/src/config.h.in +++ b/src/config.h.in @@ -24,5 +24,7 @@ #cmakedefine SMTSWITCH_YICES2_FOUND +#cmakedefine FS_INCLUDE + #endif // CONFIG_CMAKE_DEFINE_H__ diff --git a/src/util/fs.cc b/src/util/fs.cc index e975f5af4..c753544c0 100644 --- a/src/util/fs.cc +++ b/src/util/fs.cc @@ -9,10 +9,16 @@ #include #include -#include #include #include +#include +#ifdef FS_INCLUDE +#include +#else // FS_INCLUDE +#include +#endif // FS_INCLUDE + #if defined(_WIN32) || defined(_WIN64) // windows #include @@ -36,7 +42,11 @@ namespace ilang { +#ifdef FS_INCLUDE +namespace fs = std::filesystem; +#else // FS_INCLUDE namespace fs = std::experimental::filesystem; +#endif // FS_INCLUDE /// Create a dir, true -> suceeded , ow false bool os_portable_mkdir(const std::string& dir) { diff --git a/test/t_portable.cc b/test/t_portable.cc index 51283017f..65f564fc0 100644 --- a/test/t_portable.cc +++ b/test/t_portable.cc @@ -1,8 +1,6 @@ /// \file /// Unit tests for exporting and importing ILA portables. -#include - #include #include #include @@ -13,8 +11,6 @@ namespace ilang { -namespace fs = std::experimental::filesystem; - void Check(Ila& a, Ila& b) { CheckIlaEqLegacy(a.get(), b.get()); } void SerDes(const std::string& dir, const std::string& file, diff --git a/test/t_util.cc b/test/t_util.cc index 4b492a1ce..a17933126 100644 --- a/test/t_util.cc +++ b/test/t_util.cc @@ -1,7 +1,6 @@ /// \file /// Unit test for utility functions -#include #include #include @@ -12,8 +11,6 @@ namespace ilang { -namespace fs = std::experimental::filesystem; - void RecordLog() { // precondition for log test SetLogLevel(0); // log all diff --git a/test/t_verilog_gen.cc b/test/t_verilog_gen.cc index 00d41b0cf..fdff28cbf 100644 --- a/test/t_verilog_gen.cc +++ b/test/t_verilog_gen.cc @@ -2,7 +2,6 @@ /// Unit test for Verilog parser. #include #include -#include #include #include @@ -19,8 +18,6 @@ namespace ilang { -namespace fs = std::experimental::filesystem; - class TestVerilogGen : public ::testing::Test { public: TestVerilogGen() { working_dir = fs::temp_directory_path(); } diff --git a/test/t_verilog_mod.cc b/test/t_verilog_mod.cc index 50dc42132..633dd3731 100644 --- a/test/t_verilog_mod.cc +++ b/test/t_verilog_mod.cc @@ -2,7 +2,6 @@ /// Unit test for Verilog analyzer. #include #include -#include #include #include @@ -18,8 +17,6 @@ namespace ilang { -namespace fs = std::experimental::filesystem; - TEST(TestVerilogMod, Modify) { /* diff --git a/test/unit-include/util.h b/test/unit-include/util.h index 1c7e374c1..4b9ef7047 100644 --- a/test/unit-include/util.h +++ b/test/unit-include/util.h @@ -11,12 +11,24 @@ #include #include +#ifdef FS_INCLUDE +#include +#else // FS_INCLUDE +#include +#endif // FS_INCLUDE + #include #include #include namespace ilang { +#ifdef FS_INCLUDE +namespace fs = std::filesystem; +#else // FS_INCLUDE +namespace fs = std::experimental::filesystem; +#endif // FS_INCLUDE + /// \def Start to capture the log to stderr void RecordLog(); /// \def Stop to capture the log to stderr diff --git a/test/unit-src/util.cc b/test/unit-src/util.cc index c22d31c99..543d4a111 100644 --- a/test/unit-src/util.cc +++ b/test/unit-src/util.cc @@ -4,15 +4,12 @@ #include "../unit-include/util.h" #include -#include #include #include namespace ilang { -namespace fs = std::experimental::filesystem; - static const std::string CHARACTERS = "0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz"; From 501184f07f7f259e52e9c4ccee8ae3b7bd01fc1a Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 10 Jun 2020 22:25:13 -0400 Subject: [PATCH 11/21] Update Travis CI OSX version for c++17 support --- .travis.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.travis.yml b/.travis.yml index 3d5922570..450a5cf18 100644 --- a/.travis.yml +++ b/.travis.yml @@ -48,6 +48,7 @@ matrix: - name: "osx" os: osx + osx_image: xcode11.5 before_install: - brew install bison - export PATH="/usr/local/opt/bison/bin:$PATH" From aeba661051e8bd1bcf912086f6bfc1c4037aeeac Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 10 Jun 2020 22:32:03 -0400 Subject: [PATCH 12/21] Fix type cast error in return --- src/util/fs.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/fs.cc b/src/util/fs.cc index c753544c0..7473d6f23 100644 --- a/src/util/fs.cc +++ b/src/util/fs.cc @@ -92,7 +92,7 @@ std::string os_portable_join_dir(const std::vector& dirs) { /// C:\a\b\c.txt -> c.txt /// d/e/ghi -> ghi std::string os_portable_file_name_from_path(const std::string& path) { - return fs::path(path).filename(); + return fs::path(path).filename().string(); } /// Copy all file from a source dir to the destination dir From 97b9e1a32bc0ff15a72432b365127c129405d398 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 10 Jun 2020 23:13:42 -0400 Subject: [PATCH 13/21] Remove clang from the CI/CD list --- .travis.yml | 25 ------------------------- appveyor.yml | 2 +- azure-pipelines.yml | 8 ++++---- scripts/travis/build-osx.sh | 36 ------------------------------------ 4 files changed, 5 insertions(+), 66 deletions(-) delete mode 100644 scripts/travis/build-osx.sh diff --git a/.travis.yml b/.travis.yml index 450a5cf18..0feb85480 100644 --- a/.travis.yml +++ b/.travis.yml @@ -37,25 +37,6 @@ matrix: after_success: - source $TRAVIS_BUILD_DIR/scripts/travis/submit-coverage.sh $TRAVIS_BUILD_DIR/build - - name: "linux-clang" - os: linux - dist: xenial - compiler: clang - before_install: - - export LD_LIBRARY_PATH=/usr/local/clang/lib:$LD_LIBRARY_PATH - script: - - source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR - - - name: "osx" - os: osx - osx_image: xcode11.5 - before_install: - - brew install bison - - export PATH="/usr/local/opt/bison/bin:$PATH" - - export LDFLAGS="-L/usr/local/opt/bison/lib" - script: - - source $TRAVIS_BUILD_DIR/scripts/travis/build-osx.sh $TRAVIS_BUILD_DIR - - name: "coverity" os: linux dist: xenial @@ -93,12 +74,6 @@ addons: - libboost-all-dev - z3 - libz3-dev - homebrew: - update: true - packages: - - flex - - python - - z3 notifications: email: false diff --git a/appveyor.yml b/appveyor.yml index 055abebc9..ccb6613be 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -4,7 +4,7 @@ clone_depth: 1 install: - sudo apt update --yes -- sudo apt install --yes z3 libz3-dev bison flex +- sudo apt install --yes z3 libz3-dev bison flex gcc g++ build_script: - cd $APPVEYOR_BUILD_FOLDER diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 3f8bb2b4b..878023921 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -7,9 +7,9 @@ pr: - master jobs: -- job: macOS_Mojave +- job: macOS_Catalina_Debug pool: - vmImage: 'macOS-10.14' + vmImage: 'macOS-10.15' steps: - script: | brew update @@ -25,13 +25,13 @@ jobs: export LDFLAGS="-L/usr/local/opt/bison/lib" mkdir -p build cd build - cmake .. -DCMAKE_BUILD_TYPE=Release + cmake .. -DCMAKE_BUILD_TYPE=Debug cmake --build . cmake --build . --target install cmake --build . --target test displayName: 'build' -- job: macOS_Catalina +- job: macOS_Catalina_Release pool: vmImage: 'macOS-10.15' steps: diff --git a/scripts/travis/build-osx.sh b/scripts/travis/build-osx.sh deleted file mode 100644 index c04964a37..000000000 --- a/scripts/travis/build-osx.sh +++ /dev/null @@ -1,36 +0,0 @@ -#!/bin/sh - -# ============================================================================== -# MIT License -# -# Copyright (c) 2019 Princeton University -# -# Permission is hereby granted, free of charge, to any person obtaining a copy -# of this software and associated documentation files (the "Software"), to deal -# in the Software without restriction, including without limitation the rights -# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell -# copies of the Software, and to permit persons to whom the Software is -# furnished to do so, subject to the following conditions: -# -# The above copyright notice and this permission notice shall be included in all -# copies or substantial portions of the Software. -# -# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR -# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, -# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE -# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER -# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, -# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE -# SOFTWARE. -# ============================================================================== - -CI_BUILD_DIR=$1 - -cd $CI_BUILD_DIR -mkdir -p build -cd build -cmake .. -DCMAKE_BUILD_TYPE=Release -make -j$(nproc) -sudo make install -make run_test -ctest -R ExampleCMakeBuild From 3dcaa02779a3ba120fd42d9213555fa27a91f441 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Thu, 11 Jun 2020 02:01:40 -0400 Subject: [PATCH 14/21] Verbose unit tests for AzurePipelines for debug --- azure-pipelines.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 878023921..b9fce2f20 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -52,7 +52,7 @@ jobs: cmake .. -DCMAKE_BUILD_TYPE=Release cmake --build . cmake --build . --target install - cmake --build . --target test + ./test/unit_tests displayName: 'build' - job: Ubuntu_1604_LTS From 97b19adca0104b901c0314702fb2e3820a5c724e Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Thu, 11 Jun 2020 11:26:36 -0400 Subject: [PATCH 15/21] Explicitly closing opened files and categorized debug logs --- test/t_inv_extract.cc | 376 ++++++++++++++++------------------ test/t_inv_obj.cc | 61 +++--- test/t_smt_in.cc | 66 +++--- test/t_smt_trans.cc | 24 ++- test/unit-data/cex/.gitignore | 3 - test/unit-data/smt/.gitignore | 4 - 6 files changed, 252 insertions(+), 282 deletions(-) delete mode 100644 test/unit-data/cex/.gitignore delete mode 100644 test/unit-data/smt/.gitignore diff --git a/test/t_inv_extract.cc b/test/t_inv_extract.cc index 25f44d255..1a5fb57d1 100644 --- a/test/t_inv_extract.cc +++ b/test/t_inv_extract.cc @@ -1,150 +1,141 @@ /// \file /// Unit test for invariant extract -#include #include #include #include -#include +#include +#include #include +#include #include "unit-include/config.h" -#include "unit-include/pipe_ila.h" #include "unit-include/memswap.h" +#include "unit-include/pipe_ila.h" #include "unit-include/util.h" - namespace ilang { +class TestInvExtract : public ::testing::Test { +public: + TestInvExtract() {} + ~TestInvExtract() {} + + void SetUp() { + // EnableDebug("InvExtract"); + } + void TearDown() { DisableDebug("InvExtract"); } + +}; // class TestInvExtract + #ifdef ILANG_BUILD_INVSYN -TEST(TestInvExtract, Abc) { +TEST_F(TestInvExtract, Abc) { - auto dirName = - os_portable_append_dir(ILANG_TEST_SRC_ROOT, {"unit-data", "inv_extract", "abc"}); + auto dirName = os_portable_append_dir(ILANG_TEST_SRC_ROOT, + {"unit-data", "inv_extract", "abc"}); InvariantObject inv_obj; InvariantInCnf inv_cnf; inv_obj.set_dut_inst_name("m1"); inv_obj.AddInvariantFromAbcResultFile( - os_portable_append_dir( dirName , "wrapper.blif"), - os_portable_append_dir( dirName , "ffmap.info"), - true, - false, - "",/*,dirName + "glamap.info"*/ - false, // use aiger, if false, the following has no use - "", - inv_cnf, - InvariantInCnf()); - - EXPECT_EQ(inv_obj.GetVlgConstraints().size() , 1); - std::cout << inv_obj.GetVlgConstraints().at(0) << std::endl; + os_portable_append_dir(dirName, "wrapper.blif"), + os_portable_append_dir(dirName, "ffmap.info"), true, false, + "", /*,dirName + "glamap.info"*/ + false, // use aiger, if false, the following has no use + "", inv_cnf, InvariantInCnf()); + + EXPECT_EQ(inv_obj.GetVlgConstraints().size(), 1); + ILA_DLOG("InvExtract") << inv_obj.GetVlgConstraints().at(0); } +TEST_F(TestInvExtract, PipeBlifGla) { -TEST(TestInvExtract, PipeBlifGla) { - - auto dirName = - os_portable_append_dir(ILANG_TEST_SRC_ROOT, {"unit-data", "inv_extract", "pipe", "blif-gla"}); + auto dirName = os_portable_append_dir( + ILANG_TEST_SRC_ROOT, {"unit-data", "inv_extract", "pipe", "blif-gla"}); InvariantObject inv_obj; InvariantInCnf inv_cnf; inv_obj.set_dut_inst_name("m1"); inv_obj.AddInvariantFromAbcResultFile( - os_portable_append_dir( dirName , "wrapper.blif"), - os_portable_append_dir( dirName , "ffmap.info"), - true, - false, - os_portable_append_dir( dirName , "glamap.info"), /*,dirName + "glamap.info"*/ - false, // use aiger, if false, the following has no use - "", - inv_cnf, - InvariantInCnf()); - - EXPECT_EQ(inv_obj.GetVlgConstraints().size() , 1); - std::cout << inv_obj.GetVlgConstraints().at(0) << std::endl; + os_portable_append_dir(dirName, "wrapper.blif"), + os_portable_append_dir(dirName, "ffmap.info"), true, false, + os_portable_append_dir(dirName, "glamap.info"), + false, // use aiger, if false, the following has no use + "", inv_cnf, InvariantInCnf()); + + EXPECT_EQ(inv_obj.GetVlgConstraints().size(), 1); + ILA_DLOG("InvExtract") << inv_obj.GetVlgConstraints().at(0); } - - -TEST(TestInvExtract, AbcAiger) { - auto dirName = - os_portable_append_dir(ILANG_TEST_SRC_ROOT, {"unit-data", "inv_extract", "abc-aig"}); +TEST_F(TestInvExtract, AbcAiger) { + auto dirName = os_portable_append_dir( + ILANG_TEST_SRC_ROOT, {"unit-data", "inv_extract", "abc-aig"}); InvariantObject inv_obj; InvariantInCnf inv_cnf; inv_obj.set_dut_inst_name("m1"); inv_obj.AddInvariantFromAbcResultFile( - os_portable_append_dir( dirName , "__aiger_prepare.blif"), - os_portable_append_dir( dirName , "ffmap.info"), - true, - false, - "",/*,dirName + "glamap.info"*/ - true, // use aiger, if false, the following has no use - os_portable_append_dir( dirName , "wrapper.aig.map"), - inv_cnf, - InvariantInCnf()); - - EXPECT_EQ(inv_obj.GetVlgConstraints().size() , 1); - std::cout << inv_obj.GetVlgConstraints().at(0) << std::endl; + os_portable_append_dir(dirName, "__aiger_prepare.blif"), + os_portable_append_dir(dirName, "ffmap.info"), true, false, + "", /*,dirName + "glamap.info"*/ + true, // use aiger, if false, the following has no use + os_portable_append_dir(dirName, "wrapper.aig.map"), inv_cnf, + InvariantInCnf()); + + EXPECT_EQ(inv_obj.GetVlgConstraints().size(), 1); + ILA_DLOG("InvExtract") << inv_obj.GetVlgConstraints().at(0); } - -TEST(TestInvExtract, AbcAigerGLA) { - auto dirName = - os_portable_append_dir(ILANG_TEST_SRC_ROOT, {"unit-data", "inv_extract", "abc-aig-gla"}); +TEST_F(TestInvExtract, AbcAigerGLA) { + auto dirName = os_portable_append_dir( + ILANG_TEST_SRC_ROOT, {"unit-data", "inv_extract", "abc-aig-gla"}); InvariantObject inv_obj; InvariantInCnf inv_cnf; inv_obj.set_dut_inst_name("m1"); inv_obj.AddInvariantFromAbcResultFile( - os_portable_append_dir( dirName , "__aiger_prepare.blif"), - os_portable_append_dir( dirName , "ffmap.info"), - true, - false, - os_portable_append_dir( dirName , "glamap.info"), /*,dirName + "glamap.info"*/ - true, // use aiger, if false, the following has no use - os_portable_append_dir( dirName , "wrapper.aig.map"), - inv_cnf, - InvariantInCnf()); - - EXPECT_EQ(inv_obj.GetVlgConstraints().size() , 1); - std::cout << inv_obj.GetVlgConstraints().at(0) << std::endl; + os_portable_append_dir(dirName, "__aiger_prepare.blif"), + os_portable_append_dir(dirName, "ffmap.info"), true, false, + os_portable_append_dir(dirName, "glamap.info"), + true, // use aiger, if false, the following has no use + os_portable_append_dir(dirName, "wrapper.aig.map"), inv_cnf, + InvariantInCnf()); + + EXPECT_EQ(inv_obj.GetVlgConstraints().size(), 1); + ILA_DLOG("InvExtract") << inv_obj.GetVlgConstraints().at(0); } - -TEST(TestInvExtract, PipeAigerGLA) { - auto dirName = - os_portable_append_dir(ILANG_TEST_SRC_ROOT, {"unit-data", "inv_extract", "pipe", "aiger-gla"}); +TEST_F(TestInvExtract, PipeAigerGLA) { + auto dirName = os_portable_append_dir( + ILANG_TEST_SRC_ROOT, {"unit-data", "inv_extract", "pipe", "aiger-gla"}); InvariantObject inv_obj; InvariantInCnf inv_cnf; inv_obj.set_dut_inst_name("m1"); inv_obj.AddInvariantFromAbcResultFile( - os_portable_append_dir( dirName , "__aiger_prepare.blif"), - os_portable_append_dir( dirName , "ffmap.info"), - true, - false, - os_portable_append_dir( dirName , "glamap.info"), /*,dirName + "glamap.info"*/ - true, // use aiger, if false, the following has no use - os_portable_append_dir( dirName , "wrapper.aig.map"), - inv_cnf, - InvariantInCnf()); - - EXPECT_EQ(inv_obj.GetVlgConstraints().size() , 1); - std::cout << inv_obj.GetVlgConstraints().at(0) << std::endl; + os_portable_append_dir(dirName, "__aiger_prepare.blif"), + os_portable_append_dir(dirName, "ffmap.info"), true, false, + os_portable_append_dir(dirName, + "glamap.info"), /*,dirName + "glamap.info"*/ + true, // use aiger, if false, the following has no use + os_portable_append_dir(dirName, "wrapper.aig.map"), inv_cnf, + InvariantInCnf()); + + EXPECT_EQ(inv_obj.GetVlgConstraints().size(), 1); + ILA_DLOG("InvExtract") << inv_obj.GetVlgConstraints().at(0); } -TEST(TestInvExtract, GrainInvExtract) { - auto dirName = - os_portable_append_dir(ILANG_TEST_SRC_ROOT, {"unit-data", "inv_extract", "grain"}); +TEST_F(TestInvExtract, GrainInvExtract) { + auto dirName = os_portable_append_dir(ILANG_TEST_SRC_ROOT, + {"unit-data", "inv_extract", "grain"}); auto smt_file = os_portable_append_dir(dirName, "__design_smt.smt2"); - + bool flatten_datatype = true; bool flatten_hierarchy = true; @@ -154,23 +145,24 @@ TEST(TestInvExtract, GrainInvExtract) { std::ifstream fin(smt_file); std::stringstream buffer; buffer << fin.rdbuf(); + fin.close(); { smt::YosysSmtParser design_info(buffer.str()); auto inv_file = os_portable_append_dir(dirName, "smt-op-okay.result"); - inv_obj.AddInvariantFromGrainResultFile( - design_info, // smt - "" , // tag - inv_file // result file - ); - - EXPECT_EQ(inv_obj.GetVlgConstraints().size() , 1); - std::cout << inv_obj.GetVlgConstraints().at(0) << std::endl; + inv_obj.AddInvariantFromGrainResultFile(design_info, // smt + "", // tag + inv_file // result file + ); + + EXPECT_EQ(inv_obj.GetVlgConstraints().size(), 1); + ILA_DLOG("InvExtract") << inv_obj.GetVlgConstraints().at(0); EXPECT_TRUE(inv_obj.GetExtraFreeVarDefs().empty()); - EXPECT_EQ(inv_obj.GetExtraVarDefs().size() , 1); - for (auto && vdef: inv_obj.GetExtraVarDefs()) { - std::cout << std::get<0>(vdef) << std::endl << std::get<1>(vdef) << std::endl - << std::get<2>(vdef) << std::endl; + EXPECT_EQ(inv_obj.GetExtraVarDefs().size(), 1); + for (auto&& vdef : inv_obj.GetExtraVarDefs()) { + ILA_DLOG("InvExtract") << std::get<0>(vdef) << std::endl + << std::get<1>(vdef) << std::endl + << std::get<2>(vdef) << std::endl; } } @@ -178,89 +170,90 @@ TEST(TestInvExtract, GrainInvExtract) { smt::YosysSmtParser design_info(buffer.str()); auto inv_file = os_portable_append_dir(dirName, "bvsrem.result"); - EXPECT_DEATH(inv_obj.AddInvariantFromGrainResultFile( - design_info, // smt - "" , // tag - inv_file // result file - ), ".*"); + EXPECT_DEATH(inv_obj.AddInvariantFromGrainResultFile(design_info, // smt + "", // tag + inv_file // result file + ), + ".*"); } { smt::YosysSmtParser design_info(buffer.str()); auto inv_file = os_portable_append_dir(dirName, "repeat.result"); - EXPECT_DEATH(inv_obj.AddInvariantFromGrainResultFile( - design_info, // smt - "" , // tag - inv_file // result file - ), ".*"); + EXPECT_DEATH(inv_obj.AddInvariantFromGrainResultFile(design_info, // smt + "", // tag + inv_file // result file + ), + ".*"); } { smt::YosysSmtParser design_info(buffer.str()); auto inv_file = os_portable_append_dir(dirName, "rotate_left.result"); - EXPECT_DEATH(inv_obj.AddInvariantFromGrainResultFile( - design_info, // smt - "" , // tag - inv_file // result file - ), ".*"); + EXPECT_DEATH(inv_obj.AddInvariantFromGrainResultFile(design_info, // smt + "", // tag + inv_file // result file + ), + ".*"); } { smt::YosysSmtParser design_info(buffer.str()); auto inv_file = os_portable_append_dir(dirName, "rotate_right.result"); - EXPECT_DEATH(inv_obj.AddInvariantFromGrainResultFile( - design_info, // smt - "" , // tag - inv_file // result file - ), ".*"); + EXPECT_DEATH(inv_obj.AddInvariantFromGrainResultFile(design_info, // smt + "", // tag + inv_file // result file + ), + ".*"); } { smt::YosysSmtParser design_info(buffer.str()); auto inv_file = os_portable_append_dir(dirName, "sign_extend.result"); - EXPECT_DEATH(inv_obj.AddInvariantFromGrainResultFile( - design_info, // smt - "" , // tag - inv_file // result file - ), ".*"); + EXPECT_DEATH(inv_obj.AddInvariantFromGrainResultFile(design_info, // smt + "", // tag + inv_file // result file + ), + ".*"); } { smt::YosysSmtParser design_info(buffer.str()); auto inv_file = os_portable_append_dir(dirName, "zero_extend.result"); - EXPECT_DEATH(inv_obj.AddInvariantFromGrainResultFile( - design_info, // smt - "" , // tag - inv_file // result file - ), ".*"); + EXPECT_DEATH(inv_obj.AddInvariantFromGrainResultFile(design_info, // smt + "", // tag + inv_file // result file + ), + ".*"); } { smt::YosysSmtParser design_info(buffer.str()); auto inv_file = os_portable_append_dir(dirName, "outside_var.result"); - inv_obj.AddInvariantFromGrainResultFile( - design_info, // smt - "" , // tag - inv_file // result file - ), ".*"; + inv_obj.AddInvariantFromGrainResultFile(design_info, // smt + "", // tag + inv_file // result file + ), + ".*"; } } // Current implementation does not support extract invariants // from un-flattened hierarchy -TEST(TestInvExtract, Z3InvExtract) { +TEST_F(TestInvExtract, Z3InvExtract) { // prepare for ... - auto dirName = std::string(ILANG_TEST_SRC_ROOT) + "/unit-data/inv_extract/z3/"; + auto dirName = + std::string(ILANG_TEST_SRC_ROOT) + "/unit-data/inv_extract/z3/"; auto smt_file = os_portable_append_dir(dirName, "__design_smt.smt2"); InvariantInCnf inv_cnf; - + bool flatten_datatype = false; bool flatten_hierarchy = true; @@ -270,33 +263,31 @@ TEST(TestInvExtract, Z3InvExtract) { std::ifstream fin(smt_file); std::stringstream buffer; buffer << fin.rdbuf(); + fin.close(); { smt::YosysSmtParser design_info(buffer.str()); auto inv_file = os_portable_append_dir(dirName, "__synthesis_result.txt"); - inv_obj.AddInvariantFromChcResultFile( - design_info, // smt - "" , // tag - inv_file, // result file - flatten_datatype, - flatten_hierarchy - ); - - EXPECT_EQ(inv_obj.GetVlgConstraints().size() , 1); - std::cout << inv_obj.GetVlgConstraints().at(0) << std::endl; + inv_obj.AddInvariantFromChcResultFile(design_info, // smt + "", // tag + inv_file, // result file + flatten_datatype, flatten_hierarchy); + + EXPECT_EQ(inv_obj.GetVlgConstraints().size(), 1); + ILA_DLOG("InvExtract") << inv_obj.GetVlgConstraints().at(0); EXPECT_TRUE(inv_obj.GetExtraFreeVarDefs().empty()); EXPECT_TRUE(inv_obj.GetExtraVarDefs().empty()); } } - -TEST(TestInvExtract, Z3InvExtractPipe) { +TEST_F(TestInvExtract, Z3InvExtractPipe) { // prepare for ... - auto dirName = std::string(ILANG_TEST_SRC_ROOT) + "/unit-data/inv_extract/pipe/z3/"; + auto dirName = + std::string(ILANG_TEST_SRC_ROOT) + "/unit-data/inv_extract/pipe/z3/"; auto smt_file = os_portable_append_dir(dirName, "__design_smt.smt2"); InvariantInCnf inv_cnf; - + bool flatten_datatype = false; bool flatten_hierarchy = true; @@ -306,37 +297,37 @@ TEST(TestInvExtract, Z3InvExtractPipe) { std::ifstream fin(smt_file); std::stringstream buffer; buffer << fin.rdbuf(); + fin.close(); { smt::YosysSmtParser design_info(buffer.str()); auto inv_file = os_portable_append_dir(dirName, "__synthesis_result.txt"); - inv_obj.AddInvariantFromChcResultFile( - design_info, // smt - "" , // tag - inv_file, // result file - flatten_datatype, - flatten_hierarchy - ); - - EXPECT_EQ(inv_obj.GetVlgConstraints().size() , 1); - std::cout << inv_obj.GetVlgConstraints().at(0) << std::endl; + inv_obj.AddInvariantFromChcResultFile(design_info, // smt + "", // tag + inv_file, // result file + flatten_datatype, flatten_hierarchy); + + EXPECT_EQ(inv_obj.GetVlgConstraints().size(), 1); + ILA_DLOG("InvExtract") << inv_obj.GetVlgConstraints().at(0); EXPECT_TRUE(inv_obj.GetExtraFreeVarDefs().empty()); EXPECT_TRUE(inv_obj.GetExtraVarDefs().empty()); } } // Test whether it is able to handle [][] in the description -TEST(TestInvExtract, Z3InvExtractRangeSpec) { +TEST_F(TestInvExtract, Z3InvExtractRangeSpec) { // prepare for ... - auto dirName = std::string(ILANG_TEST_SRC_ROOT) + "/unit-data/inv_extract/z3-range/"; + auto dirName = + std::string(ILANG_TEST_SRC_ROOT) + "/unit-data/inv_extract/z3-range/"; auto smt_file = os_portable_append_dir(dirName, "__design_smt.smt2"); - + bool flatten_datatype = false; bool flatten_hierarchy = true; std::ifstream fin(smt_file); std::stringstream buffer; buffer << fin.rdbuf(); + fin.close(); { smt::YosysSmtParser design_info(buffer.str()); @@ -344,21 +335,19 @@ TEST(TestInvExtract, Z3InvExtractRangeSpec) { InvariantObject inv_obj; inv_obj.set_dut_inst_name("m1"); - inv_obj.AddInvariantFromChcResultFile( - design_info, // smt - "" , // tag - inv_file, // result file - flatten_datatype, - flatten_hierarchy - ); - - EXPECT_EQ(inv_obj.GetVlgConstraints().size() , 1); - std::cout << inv_obj.GetVlgConstraints().at(0) << std::endl; + inv_obj.AddInvariantFromChcResultFile(design_info, // smt + "", // tag + inv_file, // result file + flatten_datatype, flatten_hierarchy); + + EXPECT_EQ(inv_obj.GetVlgConstraints().size(), 1); + ILA_DLOG("InvExtract") << inv_obj.GetVlgConstraints().at(0); EXPECT_TRUE(inv_obj.GetExtraFreeVarDefs().empty()); EXPECT_FALSE(inv_obj.GetExtraVarDefs().empty()); - for (auto && var_expr_width : inv_obj.GetExtraVarDefs()) { - std::cout << "DEF: " << std::get<0>(var_expr_width) << " (width=" << std::get<2>(var_expr_width) - <<") := " << std::get<1>(var_expr_width) << std::endl; + for (auto&& var_expr_width : inv_obj.GetExtraVarDefs()) { + ILA_DLOG("InvExtract") << "DEF: " << std::get<0>(var_expr_width) + << " (width=" << std::get<2>(var_expr_width) + << ") := " << std::get<1>(var_expr_width); } EXPECT_TRUE(smt::SmtlibInvariantParserBase::get_local_ctr() >= 2); inv_obj.ExportToFile(os_portable_append_dir(dirName, "inv.txt")); @@ -375,29 +364,26 @@ TEST(TestInvExtract, Z3InvExtractRangeSpec) { auto inv_file = os_portable_append_dir(dirName, "__synthesis_result.txt"); - inv_obj2.AddInvariantFromChcResultFile( - design_info, // smt - "" , // tag - inv_file, // result file - flatten_datatype, - flatten_hierarchy - ); - - EXPECT_EQ(inv_obj2.GetVlgConstraints().size() , 2); - std::cout << inv_obj2.GetVlgConstraints().at(0) << std::endl; - std::cout << inv_obj2.GetVlgConstraints().at(1) << std::endl; + inv_obj2.AddInvariantFromChcResultFile(design_info, // smt + "", // tag + inv_file, // result file + flatten_datatype, flatten_hierarchy); + + EXPECT_EQ(inv_obj2.GetVlgConstraints().size(), 2); + ILA_DLOG("InvExtract") << inv_obj2.GetVlgConstraints().at(0); + ILA_DLOG("InvExtract") << inv_obj2.GetVlgConstraints().at(1); EXPECT_TRUE(inv_obj2.GetExtraFreeVarDefs().empty()); EXPECT_FALSE(inv_obj2.GetExtraVarDefs().empty()); - for (auto && var_expr_width : inv_obj2.GetExtraVarDefs()) { - std::cout << "DEF: " << std::get<0>(var_expr_width) << " (width=" << std::get<2>(var_expr_width) - <<") := " << std::get<1>(var_expr_width) << std::endl; + for (auto&& var_expr_width : inv_obj2.GetExtraVarDefs()) { + ILA_DLOG("InvExtract") << "DEF: " << std::get<0>(var_expr_width) + << " (width=" << std::get<2>(var_expr_width) + << ") := " << std::get<1>(var_expr_width); } EXPECT_TRUE(smt::SmtlibInvariantParserBase::get_local_ctr() >= 4); inv_obj2.ExportToFile(os_portable_append_dir(dirName, "inv.txt")); } } // Z3InvExtractRangeSpec - // Parsing back chc invariant is not ready yet // You may want to partially flatten. Done in // Yosys scripts, and then when parse back the @@ -405,7 +391,7 @@ TEST(TestInvExtract, Z3InvExtractRangeSpec) { // of hierarchy. #if 0 // Test whether it is able to handle [][] in the description -TEST(TestInvExtract, Z3RelChcExtract) { +TEST_F(TestInvExtract, Z3RelChcExtract) { // prepare for ... auto dirName = std::string(ILANG_TEST_SRC_ROOT) + "/unit-data/inv_extract/relchc"; @@ -441,4 +427,4 @@ TEST(TestInvExtract, Z3RelChcExtract) { #endif -}; // namespace ilang \ No newline at end of file +}; // namespace ilang diff --git a/test/t_inv_obj.cc b/test/t_inv_obj.cc index 43ee16214..7f8013205 100644 --- a/test/t_inv_obj.cc +++ b/test/t_inv_obj.cc @@ -1,62 +1,55 @@ /// \file /// Unit test for invariant object/cnf/cex/... -#include -#include #include #include -#include +#include +#include #include +#include #include "unit-include/config.h" -#include "unit-include/pipe_ila.h" #include "unit-include/memswap.h" +#include "unit-include/pipe_ila.h" #include "unit-include/util.h" - namespace ilang { #ifdef ILANG_BUILD_INVSYN TEST(InvSynSupportAuxClass, CexObj) { - auto dirName = - os_portable_append_dir(ILANG_TEST_SRC_ROOT, std::vector({"unit-data", "cex"})); - auto vcdfile = - os_portable_append_dir(dirName, "cex.vcd"); - auto cexfile = - os_portable_append_dir(dirName, "cex.txt"); + auto dirName = os_portable_append_dir( + ILANG_TEST_SRC_ROOT, std::vector({"unit-data", "cex"})); + auto vcdfile = os_portable_append_dir(dirName, "cex.vcd"); + auto cexfile = os_portable_append_dir(dirName, "cex.txt"); CexExtractor cex( - vcdfile, - "m1", - [](const std::string &) {return true;}, - true - ); + vcdfile, "m1", [](const std::string&) { return true; }, true); cex.DropStates({"m1.m1__DOT__out[3:0]"}); cex.StoreCexToFile(cexfile); { CexExtractor cex(cexfile); - EXPECT_TRUE( !IN("m1.m1__DOT__out[3:0]", cex.GetCex())); + EXPECT_TRUE(!IN("m1.m1__DOT__out[3:0]", cex.GetCex())); } - + os_portable_remove_file(cexfile); } - TEST(InvSynSupportAuxClass, InvCnf) { - auto dirName = - os_portable_append_dir(ILANG_TEST_SRC_ROOT, std::vector({"unit-data", "cex"})); - auto cnffile = - os_portable_append_dir(dirName, "cnf.txt"); - + auto dirName = os_portable_append_dir( + ILANG_TEST_SRC_ROOT, std::vector({"unit-data", "cex"})); + auto cnffile = os_portable_append_dir(dirName, "cnf.txt"); + InvariantInCnf cnf; { std::ifstream fin(cnffile); EXPECT_TRUE(fin.is_open()); cnf.ImportFromFile(fin); - InvariantInCnf::clause cl({ std::make_tuple(true, "m1.imp" , 1U), std::make_tuple(true, "m1.v", 1U) }); + InvariantInCnf::clause cl({std::make_tuple(true, "m1.imp", 1U), + std::make_tuple(true, "m1.v", 1U)}); cnf.InsertClauseNoReorder(cl); EXPECT_EQ(cnf.GetCnfs().size(), 2); + fin.close(); } { InvariantInCnf cnf2; @@ -67,26 +60,24 @@ TEST(InvSynSupportAuxClass, InvCnf) { EXPECT_EQ(cnf.GetCnfs().size(), 2); cnf2.Clear(); EXPECT_EQ(cnf2.GetCnfs().size(), 0); + fin.close(); } { - auto cocifile = - os_portable_append_dir(dirName, "coci.txt"); + auto cocifile = os_portable_append_dir(dirName, "coci.txt"); std::ofstream fout(cocifile); cnf.ExportInCociFormat(fout); + fout.close(); + os_portable_remove_file(cocifile); } { - auto cnfout = - os_portable_append_dir(dirName, "cnfout.txt"); + auto cnfout = os_portable_append_dir(dirName, "cnfout.txt"); std::ofstream fout(cnfout); cnf.ExportInCnfFormat(fout); + fout.close(); + os_portable_remove_file(cnfout); } - -} - - -TEST(InvSynSupportAuxClass, InvObj) { } #endif -}; // namespace ilang \ No newline at end of file +}; // namespace ilang diff --git a/test/t_smt_in.cc b/test/t_smt_in.cc index b8fef9f91..b634e4c32 100644 --- a/test/t_smt_in.cc +++ b/test/t_smt_in.cc @@ -1,11 +1,11 @@ /// \file /// Unit test SMT parser +#include +#include +#include #include #include -#include -#include -#include #include "unit-include/config.h" #include "unit-include/util.h" @@ -13,30 +13,31 @@ namespace ilang { TEST(TestSmtParse, Type) { - smt::var_type t1,t2; + smt::var_type t1, t2; t1._type = smt::var_type::tp::Bool; t2._type = smt::var_type::tp::BV; - EXPECT_FALSE(smt::var_type::eqtype(t1,t2)); + EXPECT_FALSE(smt::var_type::eqtype(t1, t2)); t1._type = smt::var_type::tp::Datatype; t1.module_name = "m1"; - EXPECT_FALSE(smt::var_type::eqtype(t1,t2)); - EXPECT_EQ(t1.toString(),"|m1_s|"); + EXPECT_FALSE(smt::var_type::eqtype(t1, t2)); + EXPECT_EQ(t1.toString(), "|m1_s|"); - EXPECT_EQ(smt::convert_to_binary(5,4), "#b0101"); - EXPECT_EQ(smt::convert_to_binary("0011",2,4), "#b0011"); - EXPECT_EQ(smt::convert_to_binary("0011",2,5), "#b00011"); - EXPECT_EQ(smt::convert_to_binary("0011",2,3), "#b011"); + EXPECT_EQ(smt::convert_to_binary(5, 4), "#b0101"); + EXPECT_EQ(smt::convert_to_binary("0011", 2, 4), "#b0011"); + EXPECT_EQ(smt::convert_to_binary("0011", 2, 5), "#b00011"); + EXPECT_EQ(smt::convert_to_binary("0011", 2, 3), "#b011"); } TEST(TestSmtParse, Parse) { - auto fn = - os_portable_append_dir(ILANG_TEST_SRC_ROOT, {"unit-data", "smt", "pipeline_design.smt2"}); - auto fo = - os_portable_append_dir(ILANG_TEST_SRC_ROOT, {"unit-data","smt","smt-out.smt2"}); - + auto fn = os_portable_append_dir( + ILANG_TEST_SRC_ROOT, {"unit-data", "smt", "pipeline_design.smt2"}); + auto fo = os_portable_append_dir(ILANG_TEST_SRC_ROOT, + {"unit-data", "smt", "smt-out.smt2"}); + std::ifstream fin(fn); std::stringstream buffer; buffer << fin.rdbuf(); + fin.close(); smt::smt_file smtinfo; smt::str_iterator smt_string_iterator(buffer.str()); @@ -44,8 +45,10 @@ TEST(TestSmtParse, Parse) { { std::ofstream fout(fo); - ILA_ERROR_IF(! fout.is_open()) << "Error writing to: " << fo; + ILA_ERROR_IF(!fout.is_open()) << "Error writing to: " << fo; fout << smtinfo.toString(); + fout.close(); + os_portable_remove_file(fo); } // Expect no error... } @@ -53,24 +56,23 @@ TEST(TestSmtParse, Parse) { #ifdef ILANG_BUILD_INVSYN TEST(TestSmtParse, ChcParse) { - auto fn = - os_portable_append_dir(ILANG_TEST_SRC_ROOT, {"unit-data", "smt", "aes.smt2"}); - auto chc_fn = - os_portable_append_dir(ILANG_TEST_SRC_ROOT, {"unit-data","smt","aes-chc.chc"}); + auto fn = os_portable_append_dir(ILANG_TEST_SRC_ROOT, + {"unit-data", "smt", "aes.smt2"}); + auto chc_fn = os_portable_append_dir(ILANG_TEST_SRC_ROOT, + {"unit-data", "smt", "aes-chc.chc"}); bool flatten_datatype = false; bool flatten_hierarchy = true; - + std::ifstream fin(fn); std::stringstream buffer; buffer << fin.rdbuf(); + fin.close(); { smt::YosysSmtParser design_info(buffer.str()); smt::SmtlibInvariantParserInstance chc_parser( - &design_info,flatten_datatype,flatten_hierarchy,{"INV"}, - "m1"); + &design_info, flatten_datatype, flatten_hierarchy, {"INV"}, "m1"); chc_parser.ParseInvResultFromFile(chc_fn); - std::cout - << chc_parser.GetFinalTranslateResult() << std::endl; + ILA_INFO << chc_parser.GetFinalTranslateResult(); } { std::string test_inv(R"##( @@ -162,15 +164,11 @@ TEST(TestSmtParse, ChcParse) { smt::YosysSmtParser design_info(buffer.str()); smt::SmtlibInvariantParserInstance chc_parser( - &design_info,flatten_datatype,flatten_hierarchy,{"INV"}, - "m1"); - - chc_parser.ParseSmtResultFromString( - "(assert " + test_inv + ")"); - std::cout - << chc_parser.GetFinalTranslateResult() << std::endl; - } + &design_info, flatten_datatype, flatten_hierarchy, {"INV"}, "m1"); + chc_parser.ParseSmtResultFromString("(assert " + test_inv + ")"); + ILA_INFO << chc_parser.GetFinalTranslateResult(); + } } #endif // ILANG_BUILD_INVSYN diff --git a/test/t_smt_trans.cc b/test/t_smt_trans.cc index aabba428f..0031d5f7f 100644 --- a/test/t_smt_trans.cc +++ b/test/t_smt_trans.cc @@ -1,31 +1,32 @@ /// \file /// Unit test SMT translator +#include +#include #include #include -#include -#include #include "unit-include/config.h" #include "unit-include/util.h" namespace ilang { -TEST(TestSmtTrans,ReplaceAndAddKeep) { +TEST(TestSmtTrans, ReplaceAndAddKeep) { + + auto fn = os_portable_append_dir( + ILANG_TEST_SRC_ROOT, {"unit-data", "smt", "pipeline_design.smt2"}); + auto fo = os_portable_append_dir(ILANG_TEST_SRC_ROOT, + {"unit-data", "smt", "smt-out-trans.smt2"}); - auto fn = - os_portable_append_dir(ILANG_TEST_SRC_ROOT, {"unit-data", "smt", "pipeline_design.smt2"}); - auto fo = - os_portable_append_dir(ILANG_TEST_SRC_ROOT, {"unit-data", "smt", "smt-out-trans.smt2"}); - std::ifstream fin(fn); EXPECT_TRUE(fin.is_open()); - if (! fin.is_open()) { + if (!fin.is_open()) { ILA_ERROR << "Unable to read from " << fn; return; } std::stringstream buffer; buffer << fin.rdbuf(); + fin.close(); smt::YosysSmtParser smt_in(buffer.str()); smt_in.BreakDatatypes(); @@ -33,10 +34,11 @@ TEST(TestSmtTrans,ReplaceAndAddKeep) { { std::ofstream fout(fo); - ILA_ERROR_IF(! fout.is_open()) << "Error writing to: " << fo; + ILA_ERROR_IF(!fout.is_open()) << "Error writing to: " << fo; fout << smt_in.Export(); + fout.close(); + os_portable_remove_file(fo); } - } }; // namespace ilang diff --git a/test/unit-data/cex/.gitignore b/test/unit-data/cex/.gitignore deleted file mode 100644 index 688e9b9a3..000000000 --- a/test/unit-data/cex/.gitignore +++ /dev/null @@ -1,3 +0,0 @@ -cex.txt -coci.txt -cnfout.txt diff --git a/test/unit-data/smt/.gitignore b/test/unit-data/smt/.gitignore deleted file mode 100644 index a57a5de20..000000000 --- a/test/unit-data/smt/.gitignore +++ /dev/null @@ -1,4 +0,0 @@ -smt-out.smt2 -smt-out-trans.smt2 -smt_bv_chc.smt2 - From e9d7a02d84296a0ee9022a747939bbcd47d4b855 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Thu, 11 Jun 2020 22:55:48 -0400 Subject: [PATCH 16/21] Fix copy directory when there are recursive sub-dirs --- src/util/fs.cc | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/util/fs.cc b/src/util/fs.cc index 7473d6f23..5066bb5b3 100644 --- a/src/util/fs.cc +++ b/src/util/fs.cc @@ -101,9 +101,9 @@ bool os_portable_copy_dir(const std::string& src, const std::string& dst) { // fs::copy can only have one copy_options, // either recursive or overwrite_existing // therefore, we explicitly iterate through the hierarchy - for (auto& p : fs::recursive_directory_iterator(src)) { - if (fs::is_regular_file(p.path())) { - auto dst_p = fs::path(dst) / p.path().filename(); + for (auto& p : fs::directory_iterator(src)) { + auto dst_p = fs::path(dst) / p.path().filename(); + if (p.is_regular_file()) { try { fs::copy_file(p.path(), dst_p, fs::copy_options::overwrite_existing); } catch (fs::filesystem_error& e) { @@ -111,6 +111,9 @@ bool os_portable_copy_dir(const std::string& src, const std::string& dst) { p.path().string(), dst_p.string(), e.what()); return false; } + } else if (p.is_directory()) { + fs::create_directory(dst_p); + os_portable_copy_dir(p.path().string(), dst_p.string()); } } return true; From dd8b7c4b317bb40bb01786a6dbe23f7a2a62397f Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Thu, 11 Jun 2020 22:56:50 -0400 Subject: [PATCH 17/21] Explicitly handle file closing and categoriz debug logs in TestVlgVerifInvSyn --- test/t_inv_syn.cc | 547 ++++++++++++++++++++++++---------------------- 1 file changed, 286 insertions(+), 261 deletions(-) diff --git a/test/t_inv_syn.cc b/test/t_inv_syn.cc index ed5c2c0fa..a23ae107c 100644 --- a/test/t_inv_syn.cc +++ b/test/t_inv_syn.cc @@ -1,31 +1,52 @@ /// \file /// Unit test for invariant synthesis -#include #include #include -#include +#include #include +#include #include "unit-include/config.h" -#include "unit-include/pipe_ila.h" #include "unit-include/memswap.h" +#include "unit-include/pipe_ila.h" #include "unit-include/util.h" namespace ilang { #ifdef ILANG_BUILD_INVSYN -typedef std::vector P; +#define DBG_TAG "VlgVerifInvSyn" + +class TestVlgVerifInvSyn : public ::testing::Test { +public: + TestVlgVerifInvSyn() {} + ~TestVlgVerifInvSyn() {} + + void SetUp() { + // EnableDebug(DBG_TAG); + outDir = GetRandomFileName(fs::temp_directory_path()); + os_portable_mkdir(outDir); + } + + void TearDown() { + DisableDebug(DBG_TAG); + fs::remove_all(outDir); + } + + typedef std::vector P; + fs::path outDir; + +}; // class TestVlgVerifInvSyn + // Z3, ABC, FREQHORN // ABC w. different configurations // FREQHORN w. different configurations // SMT IN? // smt-target-gen - // will not execute any external tools -TEST(TestVlgVerifInvSyn, SimpleCntCegar) { +TEST_F(TestVlgVerifInvSyn, SimpleCntCegar) { auto ila_model = CntTest::BuildModel(); VerilogVerificationTargetGenerator::vtg_config_t cfg; @@ -41,25 +62,25 @@ TEST(TestVlgVerifInvSyn, SimpleCntCegar) { cfg.Z3Path = "N/A"; cfg.GrainPath = "N/A"; - auto dirName = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT) , - P({ "unit-data","inv_syn","cnt2"}) ); - auto outDir = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT) , - P({"unit-data","inv_syn","cnt2-cex"}) ); + auto dirName = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + P({"unit-data", "inv_syn", "cnt2"})); + auto refDir = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + P({"unit-data", "inv_syn", "cnt2-cex"})); + os_portable_copy_dir(refDir, outDir); InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir(dirName , P({"verilog", "opposite.v" }))} , // - "opposite", // top_module_name - os_portable_append_dir(dirName , P({ "rfmap","vmap.json" })), // variable mapping - os_portable_append_dir(dirName , P({ "rfmap","cond-noinv.json" })), - outDir, ila_model.get(), + {}, // no include + {os_portable_append_dir(dirName, P({"verilog", "opposite.v"}))}, // + "opposite", // top_module_name + os_portable_append_dir(dirName, + P({"rfmap", "vmap.json"})), // variable mapping + os_portable_append_dir(dirName, P({"rfmap", "cond-noinv.json"})), outDir, + ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, - VerilogVerificationTargetGenerator::synthesis_backend_selector::Z3, - cfg); + VerilogVerificationTargetGenerator::synthesis_backend_selector::Z3, cfg); EXPECT_FALSE(vg.in_bad_state()); - vg.GenerateVerificationTarget({"1==1"}); EXPECT_FALSE(vg.RunVerifAuto("INC", "", true)); vg.ExtractVerificationResult(); @@ -71,7 +92,7 @@ TEST(TestVlgVerifInvSyn, SimpleCntCegar) { vg.GenerateInvariantVerificationTarget(); auto design_stat = vg.GetDesignStatistics(); design_stat.StoreToFile(os_portable_append_dir(outDir, "design_stat.txt")); - ILA_INFO << "========== Design Info ==========" ; + ILA_INFO << "========== Design Info =========="; ILA_INFO << "#bits= " << design_stat.NumOfDesignStateBits; ILA_INFO << "#vars=" << design_stat.NumOfDesignStateVars; ILA_INFO << "#extra_bits= " << design_stat.NumOfExtraStateBits; @@ -86,29 +107,31 @@ TEST(TestVlgVerifInvSyn, SimpleCntCegar) { // test save invariants / load invariants vg.GetInvariants().ExportToFile(os_portable_append_dir(outDir, "inv.txt")); vg.LoadCandidateInvariantsFromFile(os_portable_append_dir(outDir, "inv.txt")); - EXPECT_EQ(vg.GetCandidateInvariants().NumInvariant(), vg.GetInvariants().NumInvariant()); + EXPECT_EQ(vg.GetCandidateInvariants().NumInvariant(), + vg.GetInvariants().NumInvariant()); vg.RemoveInvariantsByIdx(0); - EXPECT_EQ(vg.GetInvariants().NumInvariant(),1); + EXPECT_EQ(vg.GetInvariants().NumInvariant(), 1); { InvariantInCnf cnf1; - vg.ExtractInvariantVarForEnhance(0, cnf1,true, {}); + vg.ExtractInvariantVarForEnhance(0, cnf1, true, {}); std::ofstream fout(os_portable_append_dir(outDir, "cnf1.txt")); cnf1.ExportInCnfFormat(fout); + fout.close(); } { InvariantInCnf cnf2; - vg.ExtractInvariantVarForEnhance(0, cnf2,false, {}); + vg.ExtractInvariantVarForEnhance(0, cnf2, false, {}); std::ofstream fout(os_portable_append_dir(outDir, "cnf2.txt")); cnf2.ExportInCnfFormat(fout); + fout.close(); } - InvariantObject inv_obj; inv_obj.InsertFromAnotherInvObj(vg.GetInvariants()); vg.LoadInvariantsFromFile(os_portable_append_dir(outDir, "inv.txt")); - EXPECT_EQ(vg.GetInvariants().NumInvariant(),3); + EXPECT_EQ(vg.GetInvariants().NumInvariant(), 3); vg.GenerateInvariantVerificationTarget(); inv_obj.ClearAllInvariants(); @@ -116,12 +139,13 @@ TEST(TestVlgVerifInvSyn, SimpleCntCegar) { vg.AcceptAllCandidateInvariant(); EXPECT_FALSE(vg.GetRunnableTargetScriptName().empty()); vg.CexGeneralizeRemoveStates({}); - vg.LoadDesignSmtInfo(os_portable_join_dir({outDir, "inv-syn", "__design_smt.smt2"})); -} // CegarPipelineExample + vg.LoadDesignSmtInfo( + os_portable_join_dir({outDir, "inv-syn", "__design_smt.smt2"})); +} // CegarPipelineExample // will not execute any external tools -TEST(TestVlgVerifInvSyn, SimpleCntCegarWithAssumptions) { +TEST_F(TestVlgVerifInvSyn, SimpleCntCegarWithAssumptions) { auto ila_model = CntTest::BuildModel(); VerilogVerificationTargetGenerator::vtg_config_t cfg; @@ -137,21 +161,22 @@ TEST(TestVlgVerifInvSyn, SimpleCntCegarWithAssumptions) { cfg.Z3Path = "N/A"; cfg.GrainPath = "N/A"; - auto dirName = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT) , - P({ "unit-data","inv_syn","cnt2"}) ); - auto outDir = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT) , - P({"unit-data","inv_syn","cnt2-cex"}) ); + auto dirName = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + P({"unit-data", "inv_syn", "cnt2"})); + auto refDir = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + P({"unit-data", "inv_syn", "cnt2-cex"})); + os_portable_copy_dir(refDir, outDir); InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir(dirName , P({"verilog", "opposite.v" }))} , // - "opposite", // top_module_name - os_portable_append_dir(dirName , P({ "rfmap","vmap.json" })), // variable mapping - os_portable_append_dir(dirName , P({ "rfmap","cond-noinv.json" })), - outDir, ila_model.get(), + {}, // no include + {os_portable_append_dir(dirName, P({"verilog", "opposite.v"}))}, // + "opposite", // top_module_name + os_portable_append_dir(dirName, + P({"rfmap", "vmap.json"})), // variable mapping + os_portable_append_dir(dirName, P({"rfmap", "cond-noinv.json"})), outDir, + ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, - VerilogVerificationTargetGenerator::synthesis_backend_selector::Z3, - cfg); + VerilogVerificationTargetGenerator::synthesis_backend_selector::Z3, cfg); EXPECT_FALSE(vg.in_bad_state()); @@ -165,7 +190,7 @@ TEST(TestVlgVerifInvSyn, SimpleCntCegarWithAssumptions) { } // will not execute any external tools -TEST(TestVlgVerifInvSyn, LoadInvFromBeginning) { +TEST_F(TestVlgVerifInvSyn, LoadInvFromBeginning) { auto ila_model = CntTest::BuildModel(); VerilogVerificationTargetGenerator::vtg_config_t cfg; @@ -182,17 +207,20 @@ TEST(TestVlgVerifInvSyn, LoadInvFromBeginning) { cfg.Z3Path = "N/A"; cfg.GrainPath = "N/A"; - auto dirName = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT) , - P({ "unit-data","inv_syn","cnt2"}) ); - auto outDir = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT) , - P({"unit-data","inv_syn","cnt2-cex"}) ); + auto dirName = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + P({"unit-data", "inv_syn", "cnt2"})); + auto refDir = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + P({"unit-data", "inv_syn", "cnt2-cex"})); + os_portable_copy_dir(refDir, outDir); + { InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir(dirName , P({"verilog", "opposite.v" }))} , // - "opposite", // top_module_name - os_portable_append_dir(dirName , P({ "rfmap","vmap.json" })), // variable mapping - os_portable_append_dir(dirName , P({ "rfmap","cond-noinv.json" })), + {}, // no include + {os_portable_append_dir(dirName, P({"verilog", "opposite.v"}))}, // + "opposite", // top_module_name + os_portable_append_dir(dirName, + P({"rfmap", "vmap.json"})), // variable mapping + os_portable_append_dir(dirName, P({"rfmap", "cond-noinv.json"})), outDir, ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, VerilogVerificationTargetGenerator::synthesis_backend_selector::Z3, @@ -200,18 +228,20 @@ TEST(TestVlgVerifInvSyn, LoadInvFromBeginning) { EXPECT_FALSE(vg.in_bad_state()); - vg.LoadCandidateInvariantsFromFile(os_portable_append_dir(outDir, "inv2.txt")); + vg.LoadCandidateInvariantsFromFile( + os_portable_append_dir(outDir, "inv2.txt")); vg.LoadInvariantsFromFile(os_portable_append_dir(outDir, "inv2.txt")); vg.GenerateInvariantVerificationTarget(); } cfg.ValidateSynthesizedInvariant = cfg.CONFIRMED; { InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir(dirName , P({"verilog", "opposite.v" }))} , // - "opposite", // top_module_name - os_portable_append_dir(dirName , P({ "rfmap","vmap.json" })), // variable mapping - os_portable_append_dir(dirName , P({ "rfmap","cond-noinv.json" })), + {}, // no include + {os_portable_append_dir(dirName, P({"verilog", "opposite.v"}))}, // + "opposite", // top_module_name + os_portable_append_dir(dirName, + P({"rfmap", "vmap.json"})), // variable mapping + os_portable_append_dir(dirName, P({"rfmap", "cond-noinv.json"})), outDir, ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, VerilogVerificationTargetGenerator::synthesis_backend_selector::Z3, @@ -219,18 +249,20 @@ TEST(TestVlgVerifInvSyn, LoadInvFromBeginning) { EXPECT_FALSE(vg.in_bad_state()); - vg.LoadCandidateInvariantsFromFile(os_portable_append_dir(outDir, "inv2.txt")); + vg.LoadCandidateInvariantsFromFile( + os_portable_append_dir(outDir, "inv2.txt")); vg.LoadInvariantsFromFile(os_portable_append_dir(outDir, "inv2.txt")); vg.GenerateInvariantVerificationTarget(); } cfg.ValidateSynthesizedInvariant = cfg.NOINV; { InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir(dirName , P({"verilog", "opposite.v" }))} , // - "opposite", // top_module_name - os_portable_append_dir(dirName , P({ "rfmap","vmap.json" })), // variable mapping - os_portable_append_dir(dirName , P({ "rfmap","cond-noinv.json" })), + {}, // no include + {os_portable_append_dir(dirName, P({"verilog", "opposite.v"}))}, // + "opposite", // top_module_name + os_portable_append_dir(dirName, + P({"rfmap", "vmap.json"})), // variable mapping + os_portable_append_dir(dirName, P({"rfmap", "cond-noinv.json"})), outDir, ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, VerilogVerificationTargetGenerator::synthesis_backend_selector::Z3, @@ -238,7 +270,8 @@ TEST(TestVlgVerifInvSyn, LoadInvFromBeginning) { EXPECT_FALSE(vg.in_bad_state()); - vg.LoadCandidateInvariantsFromFile(os_portable_append_dir(outDir, "inv2.txt")); + vg.LoadCandidateInvariantsFromFile( + os_portable_append_dir(outDir, "inv2.txt")); vg.LoadInvariantsFromFile(os_portable_append_dir(outDir, "inv2.txt")); vg.GenerateInvariantVerificationTarget(); vg.GenerateVerificationTarget(); @@ -246,18 +279,19 @@ TEST(TestVlgVerifInvSyn, LoadInvFromBeginning) { vg.ExtractVerificationResult(); vg.GenerateSynthesisTarget(); // you will need fp engine EXPECT_FALSE(vg.RunSynAuto(true)); - vg.ExtractSynthesisResult(); + vg.ExtractSynthesisResult(); EXPECT_FALSE(vg.in_bad_state()); } cfg.InvariantSynthesisReachableCheckKeepOldInvariant = true; { InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir(dirName , P({"verilog", "opposite.v" }))} , // - "opposite", // top_module_name - os_portable_append_dir(dirName , P({ "rfmap","vmap.json" })), // variable mapping - os_portable_append_dir(dirName , P({ "rfmap","cond-noinv.json" })), + {}, // no include + {os_portable_append_dir(dirName, P({"verilog", "opposite.v"}))}, // + "opposite", // top_module_name + os_portable_append_dir(dirName, + P({"rfmap", "vmap.json"})), // variable mapping + os_portable_append_dir(dirName, P({"rfmap", "cond-noinv.json"})), outDir, ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, VerilogVerificationTargetGenerator::synthesis_backend_selector::Z3, @@ -265,7 +299,8 @@ TEST(TestVlgVerifInvSyn, LoadInvFromBeginning) { EXPECT_FALSE(vg.in_bad_state()); - vg.LoadCandidateInvariantsFromFile(os_portable_append_dir(outDir, "inv2.txt")); + vg.LoadCandidateInvariantsFromFile( + os_portable_append_dir(outDir, "inv2.txt")); vg.LoadInvariantsFromFile(os_portable_append_dir(outDir, "inv2.txt")); vg.GenerateInvariantVerificationTarget(); vg.GenerateVerificationTarget(); @@ -276,10 +311,10 @@ TEST(TestVlgVerifInvSyn, LoadInvFromBeginning) { vg.ExtractSynthesisResult(); EXPECT_FALSE(vg.in_bad_state()); } -} // CegarPipelineExample +} // CegarPipelineExample -TEST(TestVlgVerifInvSyn, SimpleCntCegarPassed) { +TEST_F(TestVlgVerifInvSyn, SimpleCntCegarPassed) { auto ila_model = CntTest::BuildModel(); VerilogVerificationTargetGenerator::vtg_config_t cfg; @@ -295,31 +330,33 @@ TEST(TestVlgVerifInvSyn, SimpleCntCegarPassed) { cfg.Z3Path = "N/A"; cfg.GrainPath = "N/A"; - auto dirName = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT) , - P({ "unit-data","inv_syn","cnt2"}) ); - auto outDir = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT) , - P({"unit-data","inv_syn","cnt2-pass"}) ); + auto dirName = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + P({"unit-data", "inv_syn", "cnt2"})); + auto refDir = + os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + P({"unit-data", "inv_syn", "cnt2-pass"})); + os_portable_copy_dir(refDir, outDir); InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir(dirName , P({"verilog", "opposite.v" }))} , // - "opposite", // top_module_name - os_portable_append_dir(dirName , P({ "rfmap","vmap.json" })), // variable mapping - os_portable_append_dir(dirName , P({ "rfmap","cond-noinv.json" })), - outDir, ila_model.get(), + {}, // no include + {os_portable_append_dir(dirName, P({"verilog", "opposite.v"}))}, // + "opposite", // top_module_name + os_portable_append_dir(dirName, + P({"rfmap", "vmap.json"})), // variable mapping + os_portable_append_dir(dirName, P({"rfmap", "cond-noinv.json"})), outDir, + ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, - VerilogVerificationTargetGenerator::synthesis_backend_selector::Z3, - cfg); + VerilogVerificationTargetGenerator::synthesis_backend_selector::Z3, cfg); EXPECT_FALSE(vg.in_bad_state()); vg.GenerateVerificationTarget(); EXPECT_TRUE(vg.RunVerifAuto("INC", "", true)); EXPECT_TRUE(vg.GetCandidateInvariants().GetSmtFormulae().empty()); -} // SimpleCntCegarPassed +} // SimpleCntCegarPassed -TEST(TestVlgVerifInvSyn, CegarCntAbc) { +TEST_F(TestVlgVerifInvSyn, CegarCntAbc) { auto ila_model = CntTest::BuildModel(); VerilogVerificationTargetGenerator::vtg_config_t cfg; @@ -338,21 +375,22 @@ TEST(TestVlgVerifInvSyn, CegarCntAbc) { cfg.Z3Path = "N/A"; cfg.GrainPath = "N/A"; - auto dirName = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT), - {"unit-data","inv_syn","cnt2"}); - auto outDir = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT), - {"unit-data","inv_syn","cnt2-abc"}); + auto dirName = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "inv_syn", "cnt2"}); + auto refDir = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "inv_syn", "cnt2-abc"}); + os_portable_copy_dir(refDir, outDir); InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir(dirName, P({"verilog","opposite.v"}))}, - "opposite", // top_module_name - os_portable_append_dir(dirName , P({ "rfmap","vmap.json" })), // variable mapping - os_portable_append_dir(dirName , P({ "rfmap","cond-noinv.json" })), - outDir, ila_model.get(), + {}, // no include + {os_portable_append_dir(dirName, P({"verilog", "opposite.v"}))}, + "opposite", // top_module_name + os_portable_append_dir(dirName, + P({"rfmap", "vmap.json"})), // variable mapping + os_portable_append_dir(dirName, P({"rfmap", "cond-noinv.json"})), outDir, + ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, - VerilogVerificationTargetGenerator::synthesis_backend_selector::ABC, - cfg); + VerilogVerificationTargetGenerator::synthesis_backend_selector::ABC, cfg); EXPECT_FALSE(vg.in_bad_state()); @@ -370,9 +408,7 @@ TEST(TestVlgVerifInvSyn, CegarCntAbc) { } // CegarCntAbc - - -TEST(TestVlgVerifInvSyn, CegarCntAbcBlif) { +TEST_F(TestVlgVerifInvSyn, CegarCntAbcBlif) { auto ila_model = CntTest::BuildModel(); VerilogVerificationTargetGenerator::vtg_config_t cfg; @@ -392,21 +428,23 @@ TEST(TestVlgVerifInvSyn, CegarCntAbcBlif) { cfg.Z3Path = "N/A"; cfg.GrainPath = "N/A"; - auto dirName = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT), - {"unit-data","inv_syn","cnt2"}); - auto outDir = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT), - {"unit-data","inv_syn","cnt2-abc-blif"}); + auto dirName = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "inv_syn", "cnt2"}); + auto refDir = + os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "inv_syn", "cnt2-abc-blif"}); + os_portable_copy_dir(refDir, outDir); InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir(dirName, P({"verilog","opposite.v"}))}, - "opposite", // top_module_name - os_portable_append_dir(dirName , P({ "rfmap","vmap.json" })), // variable mapping - os_portable_append_dir(dirName , P({ "rfmap","cond-noinv.json" })), - outDir, ila_model.get(), + {}, // no include + {os_portable_append_dir(dirName, P({"verilog", "opposite.v"}))}, + "opposite", // top_module_name + os_portable_append_dir(dirName, + P({"rfmap", "vmap.json"})), // variable mapping + os_portable_append_dir(dirName, P({"rfmap", "cond-noinv.json"})), outDir, + ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, - VerilogVerificationTargetGenerator::synthesis_backend_selector::ABC, - cfg); + VerilogVerificationTargetGenerator::synthesis_backend_selector::ABC, cfg); EXPECT_FALSE(vg.in_bad_state()); @@ -423,8 +461,7 @@ TEST(TestVlgVerifInvSyn, CegarCntAbcBlif) { } // CegarCntAbc - -TEST(TestVlgVerifInvSyn, CegarCntAbcWithAssumption) { +TEST_F(TestVlgVerifInvSyn, CegarCntAbcWithAssumption) { auto ila_model = CntTest::BuildModel(); VerilogVerificationTargetGenerator::vtg_config_t cfg; @@ -443,21 +480,22 @@ TEST(TestVlgVerifInvSyn, CegarCntAbcWithAssumption) { cfg.Z3Path = "N/A"; cfg.GrainPath = "N/A"; - auto dirName = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT), - {"unit-data","inv_syn","cnt2"}); - auto outDir = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT), - {"unit-data","inv_syn","cnt2-abc"}); + auto dirName = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "inv_syn", "cnt2"}); + auto refDir = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "inv_syn", "cnt2-abc"}); + os_portable_copy_dir(refDir, outDir); InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir(dirName, P({"verilog","opposite.v"}))}, - "opposite", // top_module_name - os_portable_append_dir(dirName , P({ "rfmap","vmap.json" })), // variable mapping - os_portable_append_dir(dirName , P({ "rfmap","cond-noinv.json" })), - outDir, ila_model.get(), + {}, // no include + {os_portable_append_dir(dirName, P({"verilog", "opposite.v"}))}, + "opposite", // top_module_name + os_portable_append_dir(dirName, + P({"rfmap", "vmap.json"})), // variable mapping + os_portable_append_dir(dirName, P({"rfmap", "cond-noinv.json"})), outDir, + ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, - VerilogVerificationTargetGenerator::synthesis_backend_selector::ABC, - cfg); + VerilogVerificationTargetGenerator::synthesis_backend_selector::ABC, cfg); EXPECT_FALSE(vg.in_bad_state()); vg.SupplyCandidateInvariant("1'b1 == 1'b1"); @@ -469,7 +507,7 @@ TEST(TestVlgVerifInvSyn, CegarCntAbcWithAssumption) { } // CegarCntAbc -TEST(TestVlgVerifInvSyn, CegarCntAbcInvStart) { +TEST_F(TestVlgVerifInvSyn, CegarCntAbcInvStart) { auto ila_model = CntTest::BuildModel(); VerilogVerificationTargetGenerator::vtg_config_t cfg; @@ -488,20 +526,23 @@ TEST(TestVlgVerifInvSyn, CegarCntAbcInvStart) { cfg.Z3Path = "N/A"; cfg.GrainPath = "N/A"; - auto dirName = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT), - {"unit-data","inv_syn","cnt2"}); - auto outDir = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT), - {"unit-data","inv_syn","cnt2-abc"}); + auto dirName = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "inv_syn", "cnt2"}); + auto refDir = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "inv_syn", "cnt2-abc"}); + os_portable_copy_dir(refDir, outDir); { - auto inv_in = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT), - {"unit-data","inv_syn","inv_test", "inv.txt"}); + auto inv_in = + os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "inv_syn", "inv_test", "inv.txt"}); InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir(dirName, P({"verilog","opposite.v"}))}, - "opposite", // top_module_name - os_portable_append_dir(dirName , P({ "rfmap","vmap.json" })), // variable mapping - os_portable_append_dir(dirName , P({ "rfmap","cond-noinv.json" })), + {}, // no include + {os_portable_append_dir(dirName, P({"verilog", "opposite.v"}))}, + "opposite", // top_module_name + os_portable_append_dir(dirName, + P({"rfmap", "vmap.json"})), // variable mapping + os_portable_append_dir(dirName, P({"rfmap", "cond-noinv.json"})), outDir, ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, VerilogVerificationTargetGenerator::synthesis_backend_selector::ABC, @@ -509,10 +550,10 @@ TEST(TestVlgVerifInvSyn, CegarCntAbcInvStart) { EXPECT_FALSE(vg.in_bad_state()); vg.LoadInvariantsFromFile(inv_in); - std::cout << "--- LOADED ---" << std::endl; - for (auto && v : vg.GetInvariants().GetVlgConstraints()) - std::cout << "[" << v << "]" << std::endl; - std::cout << "--- END ---" << std::endl; + ILA_DLOG(DBG_TAG) << "--- LOADED ---"; + for (auto&& v : vg.GetInvariants().GetVlgConstraints()) + ILA_DLOG(DBG_TAG) << "[" << v << "]"; + ILA_DLOG(DBG_TAG) << "--- END ---"; vg.GenerateVerificationTarget(); EXPECT_FALSE(vg.RunVerifAuto("INC", "", true)); @@ -525,18 +566,19 @@ TEST(TestVlgVerifInvSyn, CegarCntAbcInvStart) { EXPECT_EQ(vg.GetCandidateInvariants().NumInvariant(), 0); vg.GetInvariants().ExportToFile(os_portable_append_dir(outDir, "inv.txt")); EXPECT_EQ(vg.GetInvariants().NumInvariant(), 1); - } { - auto inv_in = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT), - {"unit-data","inv_syn","inv_test", "inv2.txt"}); + auto inv_in = os_portable_append_dir( + std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "inv_syn", "inv_test", "inv2.txt"}); InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir(dirName, P({"verilog","opposite.v"}))}, - "opposite", // top_module_name - os_portable_append_dir(dirName , P({ "rfmap","vmap.json" })), // variable mapping - os_portable_append_dir(dirName , P({ "rfmap","cond-noinv.json" })), + {}, // no include + {os_portable_append_dir(dirName, P({"verilog", "opposite.v"}))}, + "opposite", // top_module_name + os_portable_append_dir(dirName, + P({"rfmap", "vmap.json"})), // variable mapping + os_portable_append_dir(dirName, P({"rfmap", "cond-noinv.json"})), outDir, ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, VerilogVerificationTargetGenerator::synthesis_backend_selector::ABC, @@ -556,13 +598,11 @@ TEST(TestVlgVerifInvSyn, CegarCntAbcInvStart) { EXPECT_EQ(vg.GetCandidateInvariants().NumInvariant(), 0); vg.GetInvariants().ExportToFile(os_portable_append_dir(outDir, "inv.txt")); EXPECT_EQ(vg.GetInvariants().NumInvariant(), 2); - } } // CegarCntAbc - -TEST(TestVlgVerifInvSyn, CegarCntGrain) { +TEST_F(TestVlgVerifInvSyn, CegarCntGrain) { auto ila_model = CntTest::BuildModel(); VerilogVerificationTargetGenerator::vtg_config_t cfg; @@ -580,52 +620,49 @@ TEST(TestVlgVerifInvSyn, CegarCntGrain) { cfg.GrainPath = "N/A"; cfg.GrainHintsUseCnfStyle = true; - cfg.GrainOptions = { - "--skip-cnf --skip-const-check --skip-stat-collect --ante-size 1 --conseq-size 1 --cnf cnt-no-group.cnf --use-arith-bvnot --no-const-enum-vars-on m1.v,m1.imp"}; - - auto dirName = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT), - {"unit-data","inv_syn","cnt2"}); - auto outDir = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT), - {"unit-data","inv_syn","cnt2-grain"}); - + cfg.GrainOptions = {"--skip-cnf --skip-const-check --skip-stat-collect " + "--ante-size 1 --conseq-size 1 --cnf cnt-no-group.cnf " + "--use-arith-bvnot --no-const-enum-vars-on m1.v,m1.imp"}; + + auto dirName = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "inv_syn", "cnt2"}); + auto refDir = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "inv_syn", "cnt2-grain"}); + os_portable_copy_dir(refDir, outDir); + InvariantInCnf var_in_cnf; { // save grammar file - os_portable_mkdir( - os_portable_append_dir(outDir, "inv-syn")); + os_portable_mkdir(os_portable_append_dir(outDir, "inv-syn")); InvariantInCnf::clause cl; - InvariantInCnf::VarsToClause( { - "m1.imp", "m1.v" - } , cl); + InvariantInCnf::VarsToClause({"m1.imp", "m1.v"}, cl); var_in_cnf.InsertClause(cl); std::ofstream fout( - os_portable_append_dir(outDir ,P({"inv-syn","cnt-no-group.cnf"}))); + os_portable_append_dir(outDir, P({"inv-syn", "cnt-no-group.cnf"}))); if (fout.is_open()) var_in_cnf.ExportInCnfFormat(fout); else EXPECT_TRUE(false); + fout.close(); } // save grammar file - + InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir(dirName, P({"verilog","opposite.v"}))}, - "opposite", // top_module_name - os_portable_append_dir(dirName , P({ "rfmap","vmap.json" })), // variable mapping - os_portable_append_dir(dirName , P({ "rfmap","cond-noinv.json" })), - outDir, ila_model.get(), + {}, // no include + {os_portable_append_dir(dirName, P({"verilog", "opposite.v"}))}, + "opposite", // top_module_name + os_portable_append_dir(dirName, + P({"rfmap", "vmap.json"})), // variable mapping + os_portable_append_dir(dirName, P({"rfmap", "cond-noinv.json"})), outDir, + ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, VerilogVerificationTargetGenerator::synthesis_backend_selector::GRAIN, cfg); EXPECT_FALSE(vg.in_bad_state()); - vg.ChangeGrainSyntax({ - "--skip-cnf", - "--skip-const-check", - "--skip-stat-collect", - "--ante-size 1", "--conseq-size 1", - "--cnf cnt-no-group.cnf", - "--use-arith-bvnot", - "--no-const-enum-vars-on m1.v,m1.imp"}); + vg.ChangeGrainSyntax( + {"--skip-cnf", "--skip-const-check", "--skip-stat-collect", + "--ante-size 1", "--conseq-size 1", "--cnf cnt-no-group.cnf", + "--use-arith-bvnot", "--no-const-enum-vars-on m1.v,m1.imp"}); vg.GenerateVerificationTarget(); EXPECT_FALSE(vg.RunVerifAuto("INC", "", true)); @@ -637,8 +674,7 @@ TEST(TestVlgVerifInvSyn, CegarCntGrain) { } // CegarCntGrain - -TEST(TestVlgVerifInvSyn, CegarCntGrainBackVars) { +TEST_F(TestVlgVerifInvSyn, CegarCntGrainBackVars) { auto ila_model = CntTest::BuildModel(); VerilogVerificationTargetGenerator::vtg_config_t cfg; @@ -656,52 +692,50 @@ TEST(TestVlgVerifInvSyn, CegarCntGrainBackVars) { cfg.GrainPath = "N/A"; cfg.GrainHintsUseCnfStyle = true; - cfg.GrainOptions = { - "--skip-cnf --skip-const-check --skip-stat-collect --ante-size 1 --conseq-size 1 --cnf cnt-no-group.cnf --use-arith-bvnot --no-const-enum-vars-on m1.v,m1.imp"}; - - auto dirName = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT), - {"unit-data","inv_syn","cnt2"}); - auto outDir = os_portable_append_dir( std::string(ILANG_TEST_SRC_ROOT), - {"unit-data","inv_syn","cnt2-grain-back"}); - + cfg.GrainOptions = {"--skip-cnf --skip-const-check --skip-stat-collect " + "--ante-size 1 --conseq-size 1 --cnf cnt-no-group.cnf " + "--use-arith-bvnot --no-const-enum-vars-on m1.v,m1.imp"}; + + auto dirName = os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "inv_syn", "cnt2"}); + auto refDir = + os_portable_append_dir(std::string(ILANG_TEST_SRC_ROOT), + {"unit-data", "inv_syn", "cnt2-grain-back"}); + os_portable_copy_dir(refDir, outDir); + InvariantInCnf var_in_cnf; { // save grammar file - os_portable_mkdir( - os_portable_append_dir(outDir, "inv-syn")); + os_portable_mkdir(os_portable_append_dir(outDir, "inv-syn")); InvariantInCnf::clause cl; - InvariantInCnf::VarsToClause( { - "m1.imp", "m1.v" - } , cl); + InvariantInCnf::VarsToClause({"m1.imp", "m1.v"}, cl); var_in_cnf.InsertClause(cl); std::ofstream fout( - os_portable_append_dir(outDir ,P({"inv-syn","cnt-no-group.cnf"}))); + os_portable_append_dir(outDir, P({"inv-syn", "cnt-no-group.cnf"}))); if (fout.is_open()) var_in_cnf.ExportInCnfFormat(fout); else EXPECT_TRUE(false); + fout.close(); } // save grammar file - + InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir(dirName, P({"verilog","opposite.v"}))}, - "opposite", // top_module_name - os_portable_append_dir(dirName , P({ "rfmap","vmap.json" })), // variable mapping - os_portable_append_dir(dirName , P({ "rfmap","cond-noinv.json" })), - outDir, ila_model.get(), + {}, // no include + {os_portable_append_dir(dirName, P({"verilog", "opposite.v"}))}, + "opposite", // top_module_name + os_portable_append_dir(dirName, + P({"rfmap", "vmap.json"})), // variable mapping + os_portable_append_dir(dirName, P({"rfmap", "cond-noinv.json"})), outDir, + ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, VerilogVerificationTargetGenerator::synthesis_backend_selector::GRAIN, cfg); EXPECT_FALSE(vg.in_bad_state()); - vg.ChangeGrainSyntax({ - "--skip-cnf", - "--skip-const-check", - "--skip-stat-collect", - "--ante-size 1", "--conseq-size 1", - "--cnf cnt-no-group.cnf", - "--use-arith-bvnot", - "--no-const-enum-vars-on m1.v,m1.imp"}); + vg.ChangeGrainSyntax( + {"--skip-cnf", "--skip-const-check", "--skip-stat-collect", + "--ante-size 1", "--conseq-size 1", "--cnf cnt-no-group.cnf", + "--use-arith-bvnot", "--no-const-enum-vars-on m1.v,m1.imp"}); vg.GenerateVerificationTarget(); EXPECT_FALSE(vg.RunVerifAuto("INC", "", true)); @@ -715,8 +749,7 @@ TEST(TestVlgVerifInvSyn, CegarCntGrainBackVars) { } // CegarCntGrain - -TEST(TestVlgVerifInvSyn, CegarPipelineAbcAigEnhance) { +TEST_F(TestVlgVerifInvSyn, CegarPipelineAbcAigEnhance) { auto ila_model = SimplePipe::BuildModel(); VerilogVerificationTargetGenerator::vtg_config_t cfg; @@ -736,24 +769,24 @@ TEST(TestVlgVerifInvSyn, CegarPipelineAbcAigEnhance) { cfg.AbcUseCorr = false; cfg.CosaSolver = "btor"; - cfg.GrainOptions = {"--ante-size", "1", "--conseq-size", "1" , "--gen-spec-only"}; + cfg.GrainOptions = {"--ante-size", "1", "--conseq-size", "1", + "--gen-spec-only"}; - auto dirName = - os_portable_join_dir({ILANG_TEST_SRC_ROOT, "unit-data", "vpipe"}); - auto outDir = - os_portable_join_dir({ILANG_TEST_SRC_ROOT, "unit-data", "inv_syn", "vpipe-out-abc-aig-enhance"}); + auto dirName = + os_portable_join_dir({ILANG_TEST_SRC_ROOT, "unit-data", "vpipe"}); + auto refDir = os_portable_join_dir({ILANG_TEST_SRC_ROOT, "unit-data", + "inv_syn", "vpipe-out-abc-aig-enhance"}); + os_portable_copy_dir(refDir, outDir); InvariantSynthesizerCegar vg( - {}, // no include - {os_portable_append_dir( dirName, "simple_pipe.v")}, // - "pipeline_v", // top_module_name + {}, // no include + {os_portable_append_dir(dirName, "simple_pipe.v")}, // + "pipeline_v", // top_module_name os_portable_join_dir({dirName, "rfmap", "vmap.json"}), // variable mapping - os_portable_join_dir({dirName, "rfmap", "cond-noinv.json"}), - outDir, + os_portable_join_dir({dirName, "rfmap", "cond-noinv.json"}), outDir, ila_model.get(), VerilogVerificationTargetGenerator::backend_selector::COSA, - VerilogVerificationTargetGenerator::synthesis_backend_selector::ABC, - cfg); + VerilogVerificationTargetGenerator::synthesis_backend_selector::ABC, cfg); EXPECT_FALSE(vg.in_bad_state()); @@ -765,29 +798,30 @@ TEST(TestVlgVerifInvSyn, CegarPipelineAbcAigEnhance) { vg.ExtractVerificationResult(); vg.GenerateSynthesisTarget(); EXPECT_FALSE(vg.RunSynAuto(true)); - + vg.ExtractAbcSynthesisResultForEnhancement(incremental_cnf); { // what inv to enhance - const auto & inv_to_enhance = - vg.GetCandidateInvariants(); + const auto& inv_to_enhance = vg.GetCandidateInvariants(); EXPECT_EQ(inv_to_enhance.NumInvariant(), 1); if (inv_to_enhance.NumInvariant() >= 1) - std::cout << "INV to enhance:" << inv_to_enhance.GetVlgConstraints()[0] << std::endl; + ILA_DLOG(DBG_TAG) << "INV to enhance:" + << inv_to_enhance.GetVlgConstraints()[0]; } - + // This is the function we need to write - EXPECT_TRUE(vg.WordLevelEnhancement(incremental_cnf, true) ); + EXPECT_TRUE(vg.WordLevelEnhancement(incremental_cnf, true)); vg.MergeCnf(incremental_cnf); incremental_cnf.Clear(); - vg.ClearAllCandidateInvariants(); // already included (you can also accept but unnecessary) - - vg.GetInvariants().ExportToFile(os_portable_append_dir( outDir, "inv.txt")); - + vg.ClearAllCandidateInvariants(); // already included (you can also accept but + // unnecessary) + + vg.GetInvariants().ExportToFile(os_portable_append_dir(outDir, "inv.txt")); + EXPECT_FALSE(vg.in_bad_state()); vg.GenerateInvariantVerificationTarget(); auto design_stat = vg.GetDesignStatistics(); - ILA_INFO << "========== Design Info ==========" ; + ILA_INFO << "========== Design Info =========="; ILA_INFO << "#bits= " << design_stat.NumOfDesignStateBits; ILA_INFO << "#vars=" << design_stat.NumOfDesignStateVars; ILA_INFO << "#extra_bits= " << design_stat.NumOfExtraStateBits; @@ -796,12 +830,9 @@ TEST(TestVlgVerifInvSyn, CegarPipelineAbcAigEnhance) { ILA_INFO << "t(syn)=" << design_stat.TimeOfInvSyn; ILA_INFO << "t(proof)= " << design_stat.TimeOfInvProof; ILA_INFO << "t(validate)=" << design_stat.TimeOfInvValidate; - } - - -TEST(TestVlgVerifInvSyn, SimpleCntRelChc) { +TEST_F(TestVlgVerifInvSyn, SimpleCntRelChc) { auto ila_model = CntTest::BuildModel(); VerilogVerificationTargetGenerator::vtg_config_t cfg; @@ -810,23 +841,19 @@ TEST(TestVlgVerifInvSyn, SimpleCntRelChc) { auto dirName = std::string(ILANG_TEST_SRC_ROOT) + "/unit-data/inv_syn/cnt2/"; VerilogVerificationTargetGenerator vg( - {}, // no include + {}, // no include {dirName + "verilog/opposite.v"}, // - "opposite", // top_module_name - dirName + "rfmap/vmap.json", // variable mapping + "opposite", // top_module_name + dirName + "rfmap/vmap.json", // variable mapping dirName + "rfmap/cond-relchc.json", dirName + "out/", ila_model.get(), - VerilogVerificationTargetGenerator::backend_selector::RELCHC, - cfg); + VerilogVerificationTargetGenerator::backend_selector::RELCHC, cfg); EXPECT_FALSE(vg.in_bad_state()); vg.GenerateTargets(); - } - - -TEST(TestVlgVerifInvSyn, SimpleCntRelChcNoStart) { +TEST_F(TestVlgVerifInvSyn, SimpleCntRelChcNoStart) { auto ila_model = CntTest::BuildModel(); VerilogVerificationTargetGenerator::vtg_config_t cfg; @@ -836,21 +863,19 @@ TEST(TestVlgVerifInvSyn, SimpleCntRelChcNoStart) { auto dirName = std::string(ILANG_TEST_SRC_ROOT) + "/unit-data/inv_syn/cnt2/"; VerilogVerificationTargetGenerator vg( - {}, // no include + {}, // no include {dirName + "verilog/opposite.v"}, // - "opposite", // top_module_name - dirName + "rfmap/vmap.json", // variable mapping - dirName + "rfmap/cond-relchc.json", dirName + "out-no-start/", ila_model.get(), - VerilogVerificationTargetGenerator::backend_selector::RELCHC, - cfg); + "opposite", // top_module_name + dirName + "rfmap/vmap.json", // variable mapping + dirName + "rfmap/cond-relchc.json", dirName + "out-no-start/", + ila_model.get(), + VerilogVerificationTargetGenerator::backend_selector::RELCHC, cfg); EXPECT_FALSE(vg.in_bad_state()); vg.GenerateTargets(); - } - #endif // ILANG_BUILD_INVSYN }; // namespace ilang From c1ec8b0b69a42104c7cf94b8eea7dc83ee841947 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Thu, 11 Jun 2020 23:12:40 -0400 Subject: [PATCH 18/21] Row back to legacy API for experimental versions --- src/util/fs.cc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/util/fs.cc b/src/util/fs.cc index 5066bb5b3..7fbc9082c 100644 --- a/src/util/fs.cc +++ b/src/util/fs.cc @@ -103,7 +103,8 @@ bool os_portable_copy_dir(const std::string& src, const std::string& dst) { // therefore, we explicitly iterate through the hierarchy for (auto& p : fs::directory_iterator(src)) { auto dst_p = fs::path(dst) / p.path().filename(); - if (p.is_regular_file()) { + // directory_entry::is_regular_file not supported in experimental + if (fs::is_regular_file(p.path())) { try { fs::copy_file(p.path(), dst_p, fs::copy_options::overwrite_existing); } catch (fs::filesystem_error& e) { @@ -111,7 +112,7 @@ bool os_portable_copy_dir(const std::string& src, const std::string& dst) { p.path().string(), dst_p.string(), e.what()); return false; } - } else if (p.is_directory()) { + } else if (fs::is_directory(p.path())) { fs::create_directory(dst_p); os_portable_copy_dir(p.path().string(), dst_p.string()); } From 518d231366803464dbb43ce17a6068b9fd6bbe3b Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Fri, 12 Jun 2020 02:33:36 -0400 Subject: [PATCH 19/21] New fs util - remove directory --- include/ilang/util/fs.h | 3 +++ src/util/fs.cc | 19 +++++++++++++++++-- test/t_inv_syn.cc | 2 +- 3 files changed, 21 insertions(+), 3 deletions(-) diff --git a/include/ilang/util/fs.h b/include/ilang/util/fs.h index 5d993de82..9613cf241 100644 --- a/include/ilang/util/fs.h +++ b/include/ilang/util/fs.h @@ -30,6 +30,9 @@ bool os_portable_move_file_to_dir(const std::string& src, /// Remove one file bool os_portable_remove_file(const std::string& file); +/// Remove one directory +bool os_portable_remove_directory(const std::string& dir); + /// Append two paths std::string os_portable_append_dir(const std::string& dir1, const std::string& dir2); diff --git a/src/util/fs.cc b/src/util/fs.cc index 7fbc9082c..423481a3a 100644 --- a/src/util/fs.cc +++ b/src/util/fs.cc @@ -109,7 +109,8 @@ bool os_portable_copy_dir(const std::string& src, const std::string& dst) { fs::copy_file(p.path(), dst_p, fs::copy_options::overwrite_existing); } catch (fs::filesystem_error& e) { ILA_ERROR << fmt::format("Fail copying file {} to {}", - p.path().string(), dst_p.string(), e.what()); + p.path().string(), dst_p.string()) + << e.what(); return false; } } else if (fs::is_directory(p.path())) { @@ -148,7 +149,7 @@ bool os_portable_move_file_to_dir(const std::string& src, } bool os_portable_remove_file(const std::string& file) { - ILA_ASSERT(fs::exists(file)); + ILA_ASSERT(fs::is_regular_file(file)); try { return fs::remove(file); } catch (fs::filesystem_error& e) { @@ -157,6 +158,20 @@ bool os_portable_remove_file(const std::string& file) { } } +bool os_portable_remove_directory(const std::string& dir) { + ILA_ASSERT(fs::is_directory(dir)); + // A bug in g++5 will throw exception: + // - cannot remove all: Directory not empty + // - https://gcc.gnu.org/bugzilla/show_bug.cgi?id=71313 + try { + fs::remove_all(fs::path(dir)); + } catch (fs::filesystem_error& e) { + ILA_ERROR << e.what(); + return false; + } + return true; +} + /// Extract path from path /// C:\a\b\c.txt -> "C:\a\b\" /// C:\a\b\c -> C:\a\b diff --git a/test/t_inv_syn.cc b/test/t_inv_syn.cc index a23ae107c..ac5860a1e 100644 --- a/test/t_inv_syn.cc +++ b/test/t_inv_syn.cc @@ -31,7 +31,7 @@ class TestVlgVerifInvSyn : public ::testing::Test { void TearDown() { DisableDebug(DBG_TAG); - fs::remove_all(outDir); + os_portable_remove_directory(outDir); } typedef std::vector P; From 5bb19f9054682c8b649c9c40917974586ec3168e Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 17 Jun 2020 13:58:08 -0400 Subject: [PATCH 20/21] Temporarily disable smt-parser usage in OSX Release build --- azure-pipelines.yml | 2 +- src/util/fs.cc | 10 ++++++---- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index b9fce2f20..3a4bfe3e3 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -49,7 +49,7 @@ jobs: export LDFLAGS="-L/usr/local/opt/bison/lib" mkdir -p build cd build - cmake .. -DCMAKE_BUILD_TYPE=Release + cmake .. -DCMAKE_BUILD_TYPE=Release -DILANG_BUILD_INVSYN=OFF cmake --build . cmake --build . --target install ./test/unit_tests diff --git a/src/util/fs.cc b/src/util/fs.cc index 423481a3a..0141c23b3 100644 --- a/src/util/fs.cc +++ b/src/util/fs.cc @@ -108,13 +108,15 @@ bool os_portable_copy_dir(const std::string& src, const std::string& dst) { try { fs::copy_file(p.path(), dst_p, fs::copy_options::overwrite_existing); } catch (fs::filesystem_error& e) { - ILA_ERROR << fmt::format("Fail copying file {} to {}", - p.path().string(), dst_p.string()) - << e.what(); + ILA_ERROR << e.what(); return false; } } else if (fs::is_directory(p.path())) { - fs::create_directory(dst_p); + try { + fs::create_directory(dst_p); + } catch (fs::filesystem_error& e) { + ILA_ERROR << e.what(); + } os_portable_copy_dir(p.path().string(), dst_p.string()); } } From 01724243fe0ef4857faba086ec2929caaf6bf605 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 17 Jun 2020 14:28:27 -0400 Subject: [PATCH 21/21] Update README for v1.0.4 (C++17 upgrade) --- README.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 88bccec97..369ea5574 100644 --- a/README.md +++ b/README.md @@ -53,7 +53,7 @@ brew install bison flex boost boost-python z3 ``` - The [z3](https://github.com/Z3Prover/z3) SMT solver (over 4.4.0) is required. Detailed instruction for building latest z3 can be found [here](https://github.com/Z3prover/z3#building-z3-using-make-and-gccclang). -- The [Boost](https://www.boost.org) package is required only if you want to build the synthesis engine. +- The [Boost](https://www.boost.org) package is required only if you want to build the synthesis engine (default `OFF`). #### Regression Environments @@ -66,8 +66,7 @@ brew install bison flex boost boost-python z3 | Ubuntu 18.04 (Bionic) | gcc 7.5.0 | 3.10.2 | 4.4.1 | 1.65 | 3.0.4 | 2.6.4 | Debug | | Ubuntu 18.04 (Bionic) | gcc 7.5.0 | 3.17.0 | 4.4.1 | 1.65 | 3.0.4 | 2.6.4 | Release | | Ubuntu 20.04 (Focal Fosa) | gcc 7.4.0 | 3.17.0 | 4.4.1 | - | 3.0.4 | 2.6.4 | Release | -| OSX 10.13.6 (High Sierra) | Xcode 9.4.1 | 3.15.5 | 4.8.8 | - | 3.6.2 | 2.5.35 | Release | -| OSX 10.14.6 (Mojave) | Xcode 11.3.1 | 3.17.2 | 4.8.8 | - | 3.6.2 | 2.5.35 | Release | +| OSX 10.15.4 (Catalina) | Xcode 11.4.1 | 3.17.2 | 4.8.8 | - | 3.6.2 | 2.5.35 | Debug | | OSX 10.15.4 (Catalina) | Xcode 11.4.1 | 3.17.2 | 4.8.8 | - | 3.6.2 | 2.5.35 | Release | | Windows Server 2016 | VS 2017 | 3.17.2 | 4.8.8 | - | 3.3.2 | 2.6.4 | Release | @@ -101,7 +100,7 @@ sudo make install - Use `-DILANG_FETCH_DEPS=OFF` to disable config-time updating submodules for in-source dependencies. - Use `-DILANG_BUILD_TEST=OFF` to disalbe building the unit tests. - Use `-DILANG_BUILD_SYNTH=ON` to enable building the synthesis engine. -- Use `-DILANG_BUILD_INVSYN=ON` to enable building invariant synthesis feature. +- Use `-DILANG_BUILD_INVSYN=OFF` to disable building invariant synthesis feature. - Use `-DILANG_BUILD_SWITCH=ON` to enable building [smt-switch](https://github.com/makaimann/smt-switch.git) interface support. - Use `-DILANG_INSTALL_DEV=ON` to install working features.