From 5b06ed4d5c6772f8a3356c850bd6297b46ef73c3 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 8 Jul 2020 11:37:32 -0400 Subject: [PATCH 01/30] Make single-used DfsExpr as lambda func --- include/ilang/target-sc/ilator.h | 2 -- src/target-sc/ilator.cc | 19 +++++++++++++++---- src/target-sc/ilator_dfs.cc | 15 --------------- 3 files changed, 15 insertions(+), 21 deletions(-) diff --git a/include/ilang/target-sc/ilator.h b/include/ilang/target-sc/ilator.h index 2ff338b28..40f831e6c 100644 --- a/include/ilang/target-sc/ilator.h +++ b/include/ilang/target-sc/ilator.h @@ -91,8 +91,6 @@ class Ilator { /// Translate expression node to SystemC statements. bool RenderExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut); - /// Translation routine entry point. - void DfsExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut); /// Translation routine for variable. void DfsVar(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) const; /// Translation routine for constant. diff --git a/src/target-sc/ilator.cc b/src/target-sc/ilator.cc index a636c0877..56d3068bc 100644 --- a/src/target-sc/ilator.cc +++ b/src/target-sc/ilator.cc @@ -531,11 +531,22 @@ bool Ilator::GenerateBuildSupport(const std::string& dir) { } bool Ilator::RenderExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { + auto ExprDfsVisiter = [this, &buff, &lut](const ExprPtr& e) { + if (auto pos = lut.find(e); pos == lut.end()) { + if (e->is_var()) { + DfsVar(e, buff, lut); + } else if (e->is_const()) { + DfsConst(e, buff, lut); + } else { + ILA_ASSERT(e->is_op()); + DfsOp(e, buff, lut); + } + } + ILA_ASSERT((e->is_mem() && e->is_op()) || (lut.find(e) != lut.end())); + }; + try { - auto visiter = [this, &buff, &lut](const ExprPtr& e) { - DfsExpr(e, buff, lut); - }; - expr->DepthFirstVisit(visiter); + expr->DepthFirstVisit(ExprDfsVisiter); } catch (std::exception& err) { ILA_ERROR << err.what(); return false; diff --git a/src/target-sc/ilator_dfs.cc b/src/target-sc/ilator_dfs.cc index 697a1d694..cf07d972d 100644 --- a/src/target-sc/ilator_dfs.cc +++ b/src/target-sc/ilator_dfs.cc @@ -10,21 +10,6 @@ namespace ilang { -void Ilator::DfsExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { - if (auto pos = lut.find(expr); pos == lut.end()) { - if (expr->is_var()) { - DfsVar(expr, buff, lut); - } else if (expr->is_const()) { - DfsConst(expr, buff, lut); - } else { - ILA_ASSERT(expr->is_op()); - DfsOp(expr, buff, lut); - } - } - ILA_ASSERT((expr->is_mem() && expr->is_op()) || - (lut.find(expr) != lut.end())); -} - void Ilator::DfsVar(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) const { auto [it, status] = lut.insert({expr, GetCxxName(expr)}); ILA_ASSERT(status); From db07fde0f9b6a18954d8365ec987373ed1ff0a5a Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 8 Jul 2020 12:22:38 -0400 Subject: [PATCH 02/30] Reorder variable space look-up-table --- src/target-sc/ilator.cc | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/target-sc/ilator.cc b/src/target-sc/ilator.cc index 56d3068bc..7b652b05a 100644 --- a/src/target-sc/ilator.cc +++ b/src/target-sc/ilator.cc @@ -258,12 +258,11 @@ bool Ilator::GenerateMemoryUpdate(const std::string& dir) { status &= RenderExpr(mem, buff, lut); } else { // ite status &= RenderExpr(mem->arg(0), buff, lut); - auto lut_copy = lut; - fmt::format_to(buff, "if ({}) {{\n", LookUp(mem->arg(0), lut_copy)); - status &= RenderExpr(mem->arg(1), buff, lut); - lut_copy.clear(); + fmt::format_to(buff, "if ({}) {{\n", LookUp(mem->arg(0), lut)); + auto lut_local_0 = lut; + status &= RenderExpr(mem->arg(1), buff, lut_local_0); fmt::format_to(buff, "}} else {{\n"); - status &= RenderExpr(mem->arg(2), buff, lut_copy); + status &= RenderExpr(mem->arg(2), buff, lut); // reuse lut fmt::format_to(buff, "}}\n"); } @@ -273,10 +272,12 @@ bool Ilator::GenerateMemoryUpdate(const std::string& dir) { CommitSource(GetMemUpdateFile(), dir, buff); StartNewFile(); } + if (!status) { + return status; + } } CommitSource(GetMemUpdateFile(), dir, buff); - // CommitSource("memory_update_functions.cc", dir, buff); return status; } From f190a10fde27442bad674ef7fe102f62ccc9a3d5 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 8 Jul 2020 12:23:11 -0400 Subject: [PATCH 03/30] Remove redundant configuration --- .travis.yml | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) diff --git a/.travis.yml b/.travis.yml index 4d1233cc1..8dd10733e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -48,20 +48,10 @@ jobs: build_command_prepend: "cd $TRAVIS_BUILD_DIR && mkdir -p build && cd build && cmake .. -DILANG_BUILD_TEST=OFF -DCMAKE_PREFIX_PATH=$TRAVIS_BUILD_DIR/local -DILANG_COVERITY=ON" build_command: "make" branch_pattern: coverity_scan - apt: - update: true - sources: - - ubuntu-toolchain-r-test - packages: - - flex - - bison - - z3 - - libz3-dev - - g++-7 before_install: - echo -n | openssl s_client -connect https://scan.coverity.com:443 | sed -ne '/-BEGIN CERTIFICATE-/,/-END CERTIFICATE-/p' | sudo tee -a /etc/ssl/certs/ca- - before_script: - eval "${MATRIX_EVAL}" + before_script: - source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR script: - source $TRAVIS_BUILD_DIR/scripts/travis/build-static.sh $TRAVIS_BUILD_DIR @@ -75,7 +65,6 @@ addons: - lcov - flex - bison - - libboost-all-dev - z3 - libz3-dev - g++-7 From 37dd3685a9cd766e3944441656c49ca7027bc9d2 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 8 Jul 2020 15:05:22 -0400 Subject: [PATCH 04/30] Update CI environment setting and info --- .semaphore/semaphore.yml | 8 ++++---- README.md | 10 ++++------ appveyor.yml | 2 +- azure-pipelines.yml | 2 +- 4 files changed, 10 insertions(+), 12 deletions(-) diff --git a/.semaphore/semaphore.yml b/.semaphore/semaphore.yml index 1e1c1c1fe..91c4d4c66 100644 --- a/.semaphore/semaphore.yml +++ b/.semaphore/semaphore.yml @@ -14,12 +14,12 @@ blocks: - name: build_install_test commands: - sudo apt-get update - - sudo apt-get install -y bison flex libboost-all-dev z3 libz3-dev - - export CC=gcc-7 - - export CXX=g++-7 + - sudo apt-get install -y bison flex z3 libz3-dev + - export CC=gcc-8 + - export CXX=g++-8 - mkdir build - cd build - - cmake .. -DCMAKE_BUILD_TYPE=Debug -DILANG_BUILD_SYNTH=ON + - cmake .. -DCMAKE_BUILD_TYPE=Debug - make -j$(nproc) - sudo make install - make run_test diff --git a/README.md b/README.md index 3e95329c7..ff9d6356b 100644 --- a/README.md +++ b/README.md @@ -59,13 +59,11 @@ brew install bison flex z3 | OS | Compiler | CMake | z3 | Bison | Flex | Build | | ------------------------- | ------------ | ------ | ----- | ----- | ------ | ------- | -| Ubuntu 16.04 (Xenial) | clang 7.0.0 | 3.12.4 | 4.4.1 | 3.0.4 | 2.6.0 | Debug | | Ubuntu 16.04 (Xenial) | gcc 7.5.0 | 3.12.4 | 4.4.1 | 3.0.4 | 2.6.0 | Debug | -| Ubuntu 16.04 (Xenial) | gcc 7.5.0 | 3.17.0 | 4.4.1 | 3.0.4 | 2.6.0 | Release | -| Ubuntu 18.04 (Bionic) | clang 6.0.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4 | Debug | -| Ubuntu 18.04 (Bionic) | gcc 7.5.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4 | Debug | -| Ubuntu 18.04 (Bionic) | gcc 7.5.0 | 3.17.0 | 4.4.1 | 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 | +| Ubuntu 16.04 (Xenial) | gcc 7.5.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.0 | Release | +| Ubuntu 18.04 (Bionic) | gcc 8.4.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4 | Debug | +| Ubuntu 18.04 (Bionic) | gcc 8.4.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4 | Release | +| Ubuntu 20.04 (Focal Fosa) | gcc 9.3.0 | 3.17.0 | 4.4.1 | 3.0.4 | 2.6.4 | 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 | diff --git a/appveyor.yml b/appveyor.yml index ccb6613be..d27d347c8 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -10,7 +10,7 @@ build_script: - cd $APPVEYOR_BUILD_FOLDER - mkdir -p build - cd build -- cmake .. -DCMAKE_BUILD_TYPE=Release +- cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_COMPILER=g++-9 - make -j$(nproc) - sudo make install - make test diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 1c03a137e..32fd209fe 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -91,7 +91,7 @@ jobs: - script: | mkdir -p build cd build - cmake .. -DCMAKE_BUILD_TYPE=Release + cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_COMPILER=g++-8 cmake --build . sudo cmake --build . --target install cmake --build . --target test From 2149b5d5d160212e952737330f5648314fa66d15 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 8 Jul 2020 15:38:18 -0400 Subject: [PATCH 05/30] Fixing travis coverity hook --- .travis.yml | 10 ++++++++++ scripts/travis/install-externs.sh | 6 ------ 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/.travis.yml b/.travis.yml index 8dd10733e..6d39ff479 100644 --- a/.travis.yml +++ b/.travis.yml @@ -48,6 +48,16 @@ jobs: build_command_prepend: "cd $TRAVIS_BUILD_DIR && mkdir -p build && cd build && cmake .. -DILANG_BUILD_TEST=OFF -DCMAKE_PREFIX_PATH=$TRAVIS_BUILD_DIR/local -DILANG_COVERITY=ON" build_command: "make" branch_pattern: coverity_scan + apt: + update: true + sources: + - ubuntu-toolchain-r-test + packages: + - flex + - bison + - z3 + - libz3-dev + - g++-7 before_install: - echo -n | openssl s_client -connect https://scan.coverity.com:443 | sed -ne '/-BEGIN CERTIFICATE-/,/-END CERTIFICATE-/p' | sudo tee -a /etc/ssl/certs/ca- - eval "${MATRIX_EVAL}" diff --git a/scripts/travis/install-externs.sh b/scripts/travis/install-externs.sh index 6922f7c21..028776c4e 100644 --- a/scripts/travis/install-externs.sh +++ b/scripts/travis/install-externs.sh @@ -47,12 +47,6 @@ cd $CI_BUILD_DIR/extern/vlog-parser/build cmake .. -DCMAKE_INSTALL_PREFIX=$CI_BUILD_DIR/local cmake --build . --target install -# tmpl-synth -mkdir -p $CI_BUILD_DIR/extern/tmpl-synth/build -cd $CI_BUILD_DIR/extern/tmpl-synth/build -cmake .. -DCMAKE_INSTALL_PREFIX=$CI_BUILD_DIR/local -cmake --build . --target install - # smt-switch with Boolector cd $CI_BUILD_DIR/extern/smt-switch source contrib/setup-btor.sh From d78ec52a7f44ec1f6c0340616e61612d45ac62d2 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 8 Jul 2020 22:19:22 -0400 Subject: [PATCH 06/30] Fix #198 --- src/target-sc/ilator.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/target-sc/ilator.cc b/src/target-sc/ilator.cc index 7b652b05a..8f03b2f72 100644 --- a/src/target-sc/ilator.cc +++ b/src/target-sc/ilator.cc @@ -182,6 +182,9 @@ bool Ilator::GenerateInstrContent(const InstrPtr& instr, if (!RenderExpr(update_expr, buff, lut)) { return false; } + fmt::format_to(buff, "auto {next_holder} = {next_internal};\n", + fmt::arg("next_holder", GetCxxName(update_expr)), + fmt::arg("next_internal", LookUp(update_expr, lut))); } else { // memory (one copy for performance, need special handling) if (HasLoadFromStore(update_expr)) { return false; @@ -211,7 +214,7 @@ bool Ilator::GenerateInstrContent(const InstrPtr& instr, if (!curr->is_mem()) { fmt::format_to(buff, "{current} = {next_value};\n", fmt::arg("current", GetCxxName(curr)), - fmt::arg("next_value", LookUp(next, lut))); + fmt::arg("next_value", GetCxxName(next))); } else { fmt::format_to(buff, "for (auto& it : {next_value}) {{\n" From 5083ea566f3ca1913778eec9b171419b54b9d516 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 8 Jul 2020 22:32:11 -0400 Subject: [PATCH 07/30] Fix typo --- src/target-sc/ilator.cc | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/target-sc/ilator.cc b/src/target-sc/ilator.cc index 8f03b2f72..e06da9d35 100644 --- a/src/target-sc/ilator.cc +++ b/src/target-sc/ilator.cc @@ -182,9 +182,8 @@ bool Ilator::GenerateInstrContent(const InstrPtr& instr, if (!RenderExpr(update_expr, buff, lut)) { return false; } - fmt::format_to(buff, "auto {next_holder} = {next_internal};\n", - fmt::arg("next_holder", GetCxxName(update_expr)), - fmt::arg("next_internal", LookUp(update_expr, lut))); + fmt::format_to(buff, "auto {local_var}_nxt_holder = {local_var};\n", + fmt::arg("local_var", LookUp(update_expr, lut))); } else { // memory (one copy for performance, need special handling) if (HasLoadFromStore(update_expr)) { return false; @@ -212,9 +211,9 @@ bool Ilator::GenerateInstrContent(const InstrPtr& instr, auto curr = instr->host()->state(s); auto next = instr->update(s); if (!curr->is_mem()) { - fmt::format_to(buff, "{current} = {next_value};\n", + fmt::format_to(buff, "{current} = {next_value}_nxt_holder;\n", fmt::arg("current", GetCxxName(curr)), - fmt::arg("next_value", GetCxxName(next))); + fmt::arg("next_value", LookUp(next, lut))); } else { fmt::format_to(buff, "for (auto& it : {next_value}) {{\n" From d5855c3d189d60f2f3762bf14e6c1c0f88860940 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 8 Jul 2020 23:30:02 -0400 Subject: [PATCH 08/30] Use initializer for switch statements --- include/ilang/ila-mngr/u_smt_switch.h | 2 - src/ila-mngr/u_smt_switch.cc | 65 +++++++++++---------------- 2 files changed, 25 insertions(+), 42 deletions(-) diff --git a/include/ilang/ila-mngr/u_smt_switch.h b/include/ilang/ila-mngr/u_smt_switch.h index e8b80ec7c..edf9e2d48 100644 --- a/include/ilang/ila-mngr/u_smt_switch.h +++ b/include/ilang/ila-mngr/u_smt_switch.h @@ -55,8 +55,6 @@ class SmtSwitchItf { // ------------------------- HELPERS -------------------------------------- // /// Insert the SMT Term of the given node into the map. void PopulateExprMap(const ExprPtr expr); - /// Make Term of expr based on its argument terms. - smt::Term Expr2Term(const ExprPtr expr, const smt::TermVec& arg_terms); /// Make Term of expr variable. smt::Term ExprVar2Term(const ExprPtr expr); /// Make Term of expr constant. diff --git a/src/ila-mngr/u_smt_switch.cc b/src/ila-mngr/u_smt_switch.cc index 9d35c3f0d..52fc464af 100644 --- a/src/ila-mngr/u_smt_switch.cc +++ b/src/ila-mngr/u_smt_switch.cc @@ -72,33 +72,27 @@ void SmtSwitchItf::PopulateExprMap(const ExprPtr expr) { } // get the Term based on its ast node type + auto Expr2Term = [this](const ExprPtr& e, const smt::TermVec& args) { + switch (auto uid = GetUidExpr(e); uid) { + case AST_UID_EXPR::VAR: { + return ExprVar2Term(e); + } + case AST_UID_EXPR::CONST: { + return ExprConst2Term(e); + } + default: { + ILA_ASSERT(uid == AST_UID_EXPR::OP); + return ExprOp2Term(e, args); + } + }; // switch uid + }; + auto res = Expr2Term(expr, arg_terms); // update the Term cache expr_map_.insert({expr, res}); } -smt::Term SmtSwitchItf::Expr2Term(const ExprPtr expr, - const smt::TermVec& arg_terms) { - auto expr_uid = GetUidExpr(expr); - - switch (expr_uid) { - case AST_UID_EXPR::VAR: { - return ExprVar2Term(expr); - } - case AST_UID_EXPR::CONST: { - return ExprConst2Term(expr); - } - case AST_UID_EXPR::OP: { - return ExprOp2Term(expr, arg_terms); - } - default: { - ILA_CHECK(false) << fmt::format("Unknown type {} for ", expr_uid) << expr; - return solver_->make_term(true); - } - }; // switch expr_uid -} - smt::Term SmtSwitchItf::ExprVar2Term(const ExprPtr expr) { // for z3 compatibility auto prefix = (expr->host()) ? expr->host()->GetRootName() : ""; @@ -110,9 +104,8 @@ smt::Term SmtSwitchItf::ExprVar2Term(const ExprPtr expr) { smt::Term SmtSwitchItf::ExprConst2Term(const ExprPtr expr) { auto expr_const = std::static_pointer_cast(expr); - auto sort_uid = GetUidSort(expr->sort()); - switch (sort_uid) { + switch (auto sort_uid = GetUidSort(expr->sort()); sort_uid) { case AST_UID_SORT::BOOL: { return solver_->make_term(expr_const->val_bool()->val()); } @@ -121,7 +114,8 @@ smt::Term SmtSwitchItf::ExprConst2Term(const ExprPtr expr) { return solver_->make_term(expr_const->val_bv()->val(), solver_->make_sort(smt::BV, bw)); } - case AST_UID_SORT::MEM: { + default: { + ILA_ASSERT(sort_uid == AST_UID_SORT::MEM); auto addr_sort = solver_->make_sort(smt::BV, expr->sort()->addr_width()); auto data_sort = solver_->make_sort(smt::BV, expr->sort()->data_width()); auto mem_sort = solver_->make_sort(smt::ARRAY, addr_sort, data_sort); @@ -143,10 +137,6 @@ smt::Term SmtSwitchItf::ExprConst2Term(const ExprPtr expr) { return const_memory; } - default: { - ILA_CHECK(false) << fmt::format("Unknown sort {} for ", sort_uid) << expr; - return solver_->make_term(true); - } }; // switch sort_uid } @@ -156,9 +146,8 @@ smt::Term SmtSwitchItf::ExprOp2Term(const ExprPtr expr, // XXX Boolector (maybe also others) doesn't accept INT sort for param. // auto param_sort = solver_->make_sort(smt::INT); auto param_sort = solver_->make_sort(smt::BV, PARAM_BIT_WIDTH); - auto expr_op_uid = GetUidExprOp(expr); - switch (expr_op_uid) { + switch (auto expr_op_uid = GetUidExprOp(expr); expr_op_uid) { case AST_UID_EXPR_OP::NEG: { ILA_WARN << "Negate not fully supported in smt-switch."; return solver_->make_term(smt::PrimOp::Negate, arg_terms.at(0)); @@ -327,8 +316,8 @@ smt::Term SmtSwitchItf::ExprOp2Term(const ExprPtr expr, } // apply func - for (size_t i = 0; i != arg_terms.size(); i++) { - func_arg_terms.push_back(arg_terms.at(i)); + for (auto arg_i : arg_terms) { + func_arg_terms.push_back(arg_i); } return solver_->make_term(smt::PrimOp::Apply, func_arg_terms); } @@ -340,24 +329,20 @@ smt::Term SmtSwitchItf::ExprOp2Term(const ExprPtr expr, } smt::Sort SmtSwitchItf::IlaSort2SmtSort(const SortPtr s) { - auto sort_uid = GetUidSort(s); - switch (sort_uid) { + switch (auto sort_uid = GetUidSort(s); sort_uid) { case AST_UID_SORT::BOOL: { return solver_->make_sort(smt::BOOL); } case AST_UID_SORT::BV: { return solver_->make_sort(smt::BV, s->bit_width()); } - case AST_UID_SORT::MEM: { + default: { + ILA_ASSERT(sort_uid == AST_UID_SORT::MEM); return solver_->make_sort(smt::ARRAY, solver_->make_sort(smt::BV, s->addr_width()), solver_->make_sort(smt::BV, s->data_width())); } - default: { - ILA_CHECK(false) << "Unknown sort " << sort_uid; - return solver_->make_sort(smt::BOOL); - } - }; // switch sort uid @ lambda Sort2Term + }; // switch sort uid } }; // namespace ilang From babb74ab73dc6da79da9cab442e601b122e82f58 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Thu, 9 Jul 2020 00:01:04 -0400 Subject: [PATCH 09/30] Upgrade container implementation for better performance --- include/ilang/util/container.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/include/ilang/util/container.h b/include/ilang/util/container.h index fe432f0a6..c4e33fcf1 100644 --- a/include/ilang/util/container.h +++ b/include/ilang/util/container.h @@ -64,11 +64,11 @@ template class KeyVec { /// Push back a data member. The name MUST NOT be registerd before. bool push_back(const Key& key, const T& data) { auto idx = vec_.size(); - auto res = map_.emplace(key, idx); - if (res.second) { + auto [it, status] = map_.try_emplace(key, idx); + if (status) { vec_.push_back(data); } - return res.second; + return status; } /// Get the data by index. From 0ee299416543eafd23fb10331030a46798673663 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Thu, 9 Jul 2020 13:55:04 -0400 Subject: [PATCH 10/30] Use try_emplace for look-up table update --- src/target-sc/ilator.cc | 25 +++++++++++++++---------- src/target-sc/ilator_dfs.cc | 10 +++++----- 2 files changed, 20 insertions(+), 15 deletions(-) diff --git a/src/target-sc/ilator.cc b/src/target-sc/ilator.cc index e06da9d35..b898e2df4 100644 --- a/src/target-sc/ilator.cc +++ b/src/target-sc/ilator.cc @@ -5,6 +5,7 @@ #include +#include #include #include #include @@ -136,19 +137,23 @@ bool Ilator::SanityCheck() const { bool Ilator::Bootstrap(const std::string& root) { Reset(); + auto status = true; + + // light-weight preprocessing + // status &= PassRewriteConditionalStore(m_); // create/structure project directory - auto res_mkdir = os_portable_mkdir(root); - res_mkdir &= os_portable_mkdir(os_portable_append_dir(root, dir_app)); - res_mkdir &= os_portable_mkdir(os_portable_append_dir(root, dir_extern)); - res_mkdir &= os_portable_mkdir(os_portable_append_dir(root, dir_include)); - res_mkdir &= os_portable_mkdir(os_portable_append_dir(root, dir_src)); - if (!res_mkdir) { + status &= os_portable_mkdir(root); + status &= os_portable_mkdir(os_portable_append_dir(root, dir_app)); + status &= os_portable_mkdir(os_portable_append_dir(root, dir_extern)); + status &= os_portable_mkdir(os_portable_append_dir(root, dir_include)); + status &= os_portable_mkdir(os_portable_append_dir(root, dir_src)); + if (!status) { os_portable_remove_directory(root); - ILA_ERROR << "Fail structuring simulator direcory at " << root; - return false; } - return true; + + ILA_ERROR_IF(!status) << "Fail bootstraping"; + return status; } bool Ilator::GenerateInstrContent(const InstrPtr& instr, @@ -189,7 +194,7 @@ bool Ilator::GenerateInstrContent(const InstrPtr& instr, return false; } auto placeholder = GetLocalVar(lut); - auto [it, status] = lut.insert({update_expr, placeholder}); + auto [it, status] = lut.try_emplace(update_expr, placeholder); ILA_ASSERT(status); auto mem_update_func = RegisterMemoryUpdate(update_expr); fmt::format_to(buff, diff --git a/src/target-sc/ilator_dfs.cc b/src/target-sc/ilator_dfs.cc index cf07d972d..3db47f43b 100644 --- a/src/target-sc/ilator_dfs.cc +++ b/src/target-sc/ilator_dfs.cc @@ -11,14 +11,14 @@ namespace ilang { void Ilator::DfsVar(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) const { - auto [it, status] = lut.insert({expr, GetCxxName(expr)}); + auto [it, status] = lut.try_emplace(expr, GetCxxName(expr)); ILA_ASSERT(status); // no need to define new variable } void Ilator::DfsConst(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { auto local_var = GetLocalVar(lut); - auto [it, status] = lut.insert({expr, local_var}); + auto [it, status] = lut.try_emplace(expr, local_var); ILA_ASSERT(status); // alias for constant memory @@ -107,7 +107,7 @@ void Ilator::DfsOpAppFunc(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { ILA_CHECK(!expr->is_mem()) << "Func returning memory not supported yet"; auto local_var = GetLocalVar(lut); - auto [it, status] = lut.insert({expr, local_var}); + auto [it, status] = lut.try_emplace(expr, local_var); ILA_ASSERT(status); // apply uninterpreted function @@ -130,7 +130,7 @@ void Ilator::DfsOpAppFunc(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { void Ilator::DfsOpSpecial(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { auto local_var = GetLocalVar(lut); - auto [it, status] = lut.insert({expr, local_var}); + auto [it, status] = lut.try_emplace(expr, local_var); ILA_ASSERT(status); switch (auto uid = GetUidExprOp(expr); uid) { @@ -243,7 +243,7 @@ static const std::unordered_map k_op_symbols = { void Ilator::DfsOpRegular(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) const { auto local_var = GetLocalVar(lut); - auto [it, status] = lut.insert({expr, local_var}); + auto [it, status] = lut.try_emplace(expr, local_var); ILA_ASSERT(status); // get the corresponding operator symbol From 9f00fe1a6980c906b5cdf2620272d5c242aef5d6 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Thu, 9 Jul 2020 13:55:46 -0400 Subject: [PATCH 11/30] Apply light-wight rewriting pass for preprocessing --- src/target-sc/ilator.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/target-sc/ilator.cc b/src/target-sc/ilator.cc index b898e2df4..1c81813b0 100644 --- a/src/target-sc/ilator.cc +++ b/src/target-sc/ilator.cc @@ -140,7 +140,7 @@ bool Ilator::Bootstrap(const std::string& root) { auto status = true; // light-weight preprocessing - // status &= PassRewriteConditionalStore(m_); + status &= PassRewriteConditionalStore(m_); // create/structure project directory status &= os_portable_mkdir(root); From 48a37219d04c3f597458a67d48d355f8e50fa542 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Fri, 10 Jul 2020 16:01:43 -0400 Subject: [PATCH 12/30] Allow unroller to get z3::func_decl for uninterpreted funcs --- CMakeLists.txt | 2 +- include/ilang/ila-mngr/u_unroller.h | 2 ++ include/ilang/ilang++.h | 9 +++---- src/ila-mngr/u_abs_knob.cc | 38 ++++++++++++----------------- src/ila-mngr/u_unroller.cc | 8 ++++-- src/ila/symbol.cc | 10 +++++--- src/ilang++.cc | 4 +++ 7 files changed, 38 insertions(+), 35 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 397749c2a..d0255502b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -11,7 +11,7 @@ endif() # PROJECT # name version language # ---------------------------------------------------------------------------- # -project(ilang VERSION 1.1.0 +project(ilang VERSION 1.1.1 LANGUAGES CXX ) diff --git a/include/ilang/ila-mngr/u_unroller.h b/include/ilang/ila-mngr/u_unroller.h index ae5f4be21..1ea75747b 100644 --- a/include/ilang/ila-mngr/u_unroller.h +++ b/include/ilang/ila-mngr/u_unroller.h @@ -57,6 +57,8 @@ class Unroller { ZExpr GetZ3Expr(const ExprPtr e); /// Return the z3::expr representing a and b are equal at their time. ZExpr Equal(const ExprPtr va, const int& ta, const ExprPtr vb, const int& tb); + /// Return the z3::func_decl representing f. + z3::func_decl GetZ3FuncDecl(const FuncPtr& f) const; protected: // ------------------------- MEMBERS -------------------------------------- // diff --git a/include/ilang/ilang++.h b/include/ilang/ilang++.h index 92ce5615d..e84d068da 100644 --- a/include/ilang/ilang++.h +++ b/include/ilang/ilang++.h @@ -398,6 +398,8 @@ class FuncRef { // ------------------------- ACCESSORS/MUTATORS --------------------------- // /// Return the function name as std::string. std::string name() const; + /// Return the wrapped Func pointer. + inline FuncPtr get() const { return ptr_; } // ------------------------- METHODS -------------------------------------- // /// Apply the function with no argument. @@ -409,11 +411,6 @@ class FuncRef { /// Apply the function with multiple arguments. ExprRef operator()(const std::vector& argvec) const; -private: - // ------------------------- ACCESSORS/MUTATORS --------------------------- // - /// Return the wrapped Func pointer. - inline FuncPtr get() const { return ptr_; } - }; // class FuncRef /// \brief The wrapper of Instr (instruction). @@ -692,6 +689,8 @@ class IlaZ3Unroller { /// Return the z3::expr representing a and b are equal at their time. z3::expr Equal(const ExprRef& va, const int& ta, const ExprRef& vb, const int& tb); + /// Return the z3::func_decl representing f. + z3::func_decl GetZ3FuncDecl(const FuncRef& f) const; private: // ------------------------- MEMBERS -------------------------------------- // diff --git a/src/ila-mngr/u_abs_knob.cc b/src/ila-mngr/u_abs_knob.cc index 432f4b0eb..8db777163 100644 --- a/src/ila-mngr/u_abs_knob.cc +++ b/src/ila-mngr/u_abs_knob.cc @@ -230,23 +230,23 @@ void RewriteInstr(const InstrCnstPtr src, const InstrPtr dst, // this function will change the input ! You can copy it first. void FlattenIla(const InstrLvlAbsPtr ila_ptr_) { ILA_NOT_NULL(ila_ptr_); + ILA_INFO << "Flatten " << ila_ptr_; // let's first record all the child's input/states auto expr_map = ExprMap(); CnstIlaMap ila_map_; - std::function recordInpStates = - [&](const InstrLvlAbsCnstPtr& a) { - ILA_INFO << "Traverse:" << (a->name().str()); - if (a == ila_ptr_) - return; // will not change the top - DuplInp(a, ila_ptr_, expr_map); - DuplStt(a, ila_ptr_, expr_map); - DuplInit(a, ila_ptr_, expr_map); + auto recordInpStates = [&](const InstrLvlAbsCnstPtr& a) { + if (a == ila_ptr_) + return; // will not change the top - ila_map_.insert({a, ila_ptr_}); - // remember to change the decode !!! to factor in the valid state - }; + DuplInp(a, ila_ptr_, expr_map); + DuplStt(a, ila_ptr_, expr_map); + DuplInit(a, ila_ptr_, expr_map); + + ila_map_.insert({a, ila_ptr_}); + // remember to change the decode !!! to factor in the valid state + }; ila_ptr_->DepthFirstVisit(recordInpStates); @@ -316,34 +316,26 @@ InstrLvlAbsPtr CopyIlaTree(const InstrLvlAbsCnstPtr src, /******************************************************************************/ void DuplInp(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst, ExprMap& expr_map) { - auto inps = GetInp(src); - for (auto it = inps.begin(); it != inps.end(); it++) { + for (const auto& inp_src : GetInp(src)) { // declare new input if not exist (not parent states) - auto inp_src = *it; auto inp_dst = dst->find_input(inp_src->name()); if (!inp_dst) { // not exist --> child-input --> create inp_dst = DuplInp(dst, inp_src); } // update rewrite rule - if (expr_map.find(inp_src) == expr_map.end()) { - expr_map.insert({inp_src, inp_dst}); - } + expr_map.try_emplace(inp_src, inp_dst); } } void DuplStt(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst, ExprMap& expr_map) { - auto stts = GetStt(src); - for (auto it = stts.begin(); it != stts.end(); it++) { - auto stt_src = *it; + for (const auto& stt_src : GetStt(src)) { auto stt_dst = dst->find_state(stt_src->name()); if (!stt_dst) { // not exist --> child-state --> create stt_dst = DuplStt(dst, stt_src); } // update rewrite rule - if (expr_map.find(stt_src) == expr_map.end()) { - expr_map.insert({stt_src, stt_dst}); - } + expr_map.try_emplace(stt_src, stt_dst); } } diff --git a/src/ila-mngr/u_unroller.cc b/src/ila-mngr/u_unroller.cc index f21fdb478..a85e401fa 100644 --- a/src/ila-mngr/u_unroller.cc +++ b/src/ila-mngr/u_unroller.cc @@ -72,6 +72,10 @@ ZExpr Unroller::Equal(const ExprPtr a, const int& ta, const ExprPtr b, return a_expr == b_expr; } +z3::func_decl Unroller::GetZ3FuncDecl(const FuncPtr& f) const { + return f->GetZ3FuncDecl(ctx_); +} + ZExpr Unroller::UnrollSubs(const size_t& len, const int& pos) { // bootstrap basic information BootStrap(pos); @@ -300,8 +304,8 @@ void Unroller::CopyZExprVec(const ZExprVec& src, ZExprVec& dst) { ZExpr Unroller::ConjPred(const ZExprVec& vec) const { auto conj = ctx().bool_val(true); - for (size_t i = 0; i != vec.size(); i++) { - conj = (conj && vec[i]); + for (const auto& p : vec) { + conj = (conj && p); } conj = conj.simplify(); return conj; diff --git a/src/ila/symbol.cc b/src/ila/symbol.cc index 7201825aa..f78b8b2d7 100644 --- a/src/ila/symbol.cc +++ b/src/ila/symbol.cc @@ -31,10 +31,12 @@ const char* Symbol::c_str() const { return name_.c_str(); } const std::string Symbol::format_str(const std::string& prefix, const std::string& suffix) const { std::string res = name_; - if (prefix != "") - res = prefix + "_" + res; - if (suffix != "") - res = res + "_" + suffix; + if (!prefix.empty()) { + res = prefix + "_sEp_" + res; + } + if (!suffix.empty()) { + res = res + "_sEp_" + suffix; + } return res; } diff --git a/src/ilang++.cc b/src/ilang++.cc index c17895757..77e112a8e 100644 --- a/src/ilang++.cc +++ b/src/ilang++.cc @@ -828,6 +828,10 @@ z3::expr IlaZ3Unroller::Equal(const ExprRef& va, const int& ta, return univ_->Equal(va.get(), ta, vb.get(), tb); } +z3::func_decl IlaZ3Unroller::GetZ3FuncDecl(const FuncRef& f) const { + return univ_->GetZ3FuncDecl(f.get()); +} + void LogLevel(const int& lvl) { SetLogLevel(lvl); } void LogPath(const std::string& path) { SetLogPath(path); } From 10fa797f072d7843e4ab25f9531382b4e25daf15 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Fri, 10 Jul 2020 16:27:13 -0400 Subject: [PATCH 13/30] Regular cleanup --- src/ila-mngr/u_rewrite_expr.cc | 5 +---- src/ila/ast/expr_var.cc | 8 +++++--- 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/ila-mngr/u_rewrite_expr.cc b/src/ila-mngr/u_rewrite_expr.cc index f9e19626e..14ace19e6 100644 --- a/src/ila-mngr/u_rewrite_expr.cc +++ b/src/ila-mngr/u_rewrite_expr.cc @@ -40,10 +40,7 @@ ExprPtr FuncObjRewrExpr::Rewrite(const ExprPtr e) const { } ExprPtr FuncObjRewrExpr::RewriteOp(const ExprPtr e) const { - // check each type of op - auto expr_op_uid = GetUidExprOp(e); - - switch (expr_op_uid) { + switch (auto expr_op_uid = GetUidExprOp(e); expr_op_uid) { case AST_UID_EXPR_OP::NEG: { auto a = get(e->arg(0)); return Negate(a); diff --git a/src/ila/ast/expr_var.cc b/src/ila/ast/expr_var.cc index 24c407a9e..c53d93e44 100644 --- a/src/ila/ast/expr_var.cc +++ b/src/ila/ast/expr_var.cc @@ -3,6 +3,8 @@ #include +#include + #include #include @@ -47,12 +49,12 @@ std::ostream& ExprVar::PrintBool(std::ostream& out) const { } std::ostream& ExprVar::PrintBv(std::ostream& out) const { - return out << name().str() + "(" + std::to_string(sort()->bit_width()) + ")"; + return out << fmt::format("{}({})", name().str(), sort()->bit_width()); } std::ostream& ExprVar::PrintMem(std::ostream& out) const { - return out << name().str() + "(" + std::to_string(sort()->addr_width()) + - ", " + std::to_string(sort()->data_width()) + ")"; + return out << fmt::format("{}({}, {})", name().str(), sort()->addr_width(), + sort()->data_width()); } } // namespace ilang From c1ae3621523df0e1c7a09050c92cfa7d7c7d24ff Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 11 Jul 2020 00:26:22 -0400 Subject: [PATCH 14/30] Update README --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index ff9d6356b..857790309 100644 --- a/README.md +++ b/README.md @@ -63,7 +63,7 @@ brew install bison flex z3 | Ubuntu 16.04 (Xenial) | gcc 7.5.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.0 | Release | | Ubuntu 18.04 (Bionic) | gcc 8.4.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4 | Debug | | Ubuntu 18.04 (Bionic) | gcc 8.4.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4 | Release | -| Ubuntu 20.04 (Focal Fosa) | gcc 9.3.0 | 3.17.0 | 4.4.1 | 3.0.4 | 2.6.4 | Release | +| Ubuntu 20.04 (Focal Fosa) | gcc 9.3.0 | 3.17.0 | 4.8.7 | 3.0.4 | 2.6.4 | 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 | From 9b429b14fc658b7b1d225866c62ea4a8b97a2a0c Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 11 Jul 2020 00:26:44 -0400 Subject: [PATCH 15/30] Fix ITE mem sim-gen --- include/ilang/target-sc/ilator.h | 2 + src/target-sc/ilator.cc | 122 ++++++++++++++++++------------- src/target-sc/ilator_dfs.cc | 14 ++++ 3 files changed, 89 insertions(+), 49 deletions(-) diff --git a/include/ilang/target-sc/ilator.h b/include/ilang/target-sc/ilator.h index 40f831e6c..56db5b3f1 100644 --- a/include/ilang/target-sc/ilator.h +++ b/include/ilang/target-sc/ilator.h @@ -91,6 +91,8 @@ class Ilator { /// Translate expression node to SystemC statements. bool RenderExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut); + /// Translation routine for entrypoint. + void DfsExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut); /// Translation routine for variable. void DfsVar(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) const; /// Translation routine for constant. diff --git a/src/target-sc/ilator.cc b/src/target-sc/ilator.cc index 1c81813b0..f638649e2 100644 --- a/src/target-sc/ilator.cc +++ b/src/target-sc/ilator.cc @@ -189,7 +189,7 @@ bool Ilator::GenerateInstrContent(const InstrPtr& instr, } fmt::format_to(buff, "auto {local_var}_nxt_holder = {local_var};\n", fmt::arg("local_var", LookUp(update_expr, lut))); - } else { // memory (one copy for performance, need special handling) + } else { // memory (one copy for performance, require special handling) if (HasLoadFromStore(update_expr)) { return false; } @@ -236,22 +236,53 @@ bool Ilator::GenerateInstrContent(const InstrPtr& instr, } bool Ilator::GenerateMemoryUpdate(const std::string& dir) { - fmt::memory_buffer buff; - ExprVarMap lut; + // helper for traversing memory updates + class MemUpdateVisiter { + public: + MemUpdateVisiter(Ilator* h, fmt::memory_buffer& b, ExprVarMap& l) + : host(h), buff_ref(b), lut_ref(l) {} + + bool pre(const ExprPtr& expr) { + // stop traversing when reaching memory ITE (stand-alone func) + if (expr->is_mem() && expr->is_op() && + GetUidExprOp(expr) == AST_UID_EXPR_OP::ITE) { + host->DfsExpr(expr, buff_ref, lut_ref); + return true; + } else { + return false; + } + } + + void post(const ExprPtr& expr) { host->DfsExpr(expr, buff_ref, lut_ref); } + + Ilator* host; + fmt::memory_buffer& buff_ref; + ExprVarMap lut_ref; + }; + + auto RenderMemUpdate = [this](const ExprPtr e, fmt::memory_buffer& b, + ExprVarMap& l) { + auto mem_visiter = MemUpdateVisiter(this, b, l); + e->DepthFirstVisitPrePost(mem_visiter); + }; + + // helpers for managing files int file_cnt = 0; auto GetMemUpdateFile = [&file_cnt]() { return fmt::format("memory_update_functions_{}.cc", file_cnt++); }; + fmt::memory_buffer buff; auto StartNewFile = [this, &buff]() { buff.clear(); fmt::format_to(buff, "#include <{}.h>\n", GetProjectName()); }; + // start generating StartNewFile(); + ExprVarMap lut; - auto status = true; for (auto mem_update_func_it : memory_updates_) { auto& mem_update_func = mem_update_func_it.second; ILA_NOT_NULL(mem_update_func); @@ -262,30 +293,29 @@ bool Ilator::GenerateMemoryUpdate(const std::string& dir) { BeginFuncDef(mem_update_func, buff); if (auto uid = GetUidExprOp(mem); uid == AST_UID_EXPR_OP::STORE) { - status &= RenderExpr(mem, buff, lut); + RenderMemUpdate(mem, buff, lut); } else { // ite - status &= RenderExpr(mem->arg(0), buff, lut); + RenderExpr(mem->arg(0), buff, lut); + auto lut_local_true = lut; + auto& lut_local_false = lut; // reuse + fmt::format_to(buff, "if ({}) {{\n", LookUp(mem->arg(0), lut)); - auto lut_local_0 = lut; - status &= RenderExpr(mem->arg(1), buff, lut_local_0); + RenderMemUpdate(mem->arg(1), buff, lut_local_true); fmt::format_to(buff, "}} else {{\n"); - status &= RenderExpr(mem->arg(2), buff, lut); // reuse lut + RenderMemUpdate(mem->arg(2), buff, lut_local_false); fmt::format_to(buff, "}}\n"); } EndFuncDef(mem_update_func, buff); - if (buff.size() > 100000) { + if (buff.size() > 50000) { CommitSource(GetMemUpdateFile(), dir, buff); StartNewFile(); } - if (!status) { - return status; - } } CommitSource(GetMemUpdateFile(), dir, buff); - return status; + return true; } bool Ilator::GenerateConstantMemory(const std::string& dir) { @@ -471,17 +501,8 @@ bool Ilator::GenerateGlobalHeader(const std::string& dir) { } bool Ilator::GenerateBuildSupport(const std::string& dir) { - fmt::memory_buffer buff; - // CMakeLists.txt - std::vector src_files; - for (auto& f : source_files_) { - src_files.push_back( - fmt::format(" ${{CMAKE_CURRENT_SOURCE_DIR}}/{dir}/{file}", - fmt::arg("dir", dir_src), fmt::arg("file", f))); - } - fmt::format_to( - buff, + static const char* cmake_recipe_template = "# CMakeLists.txt for {project}\n" "cmake_minimum_required(VERSION 3.14.0)\n" "project({project} LANGUAGES CXX)\n" @@ -513,26 +534,39 @@ bool Ilator::GenerateBuildSupport(const std::string& dir) { " )\n" " FetchContent_MakeAvailable(json)\n" " target_link_libraries({project} nlohmann_json::nlohmann_json)\n" - "endif()\n" - // - , - fmt::arg("project", GetProjectName()), fmt::arg("dir_app", dir_app), - fmt::arg("source_files", fmt::join(src_files, "\n")), - fmt::arg("dir_include", dir_include)); + "endif()\n"; + + std::vector src_files; + for (auto& f : source_files_) { + src_files.push_back( + fmt::format(" ${{CMAKE_CURRENT_SOURCE_DIR}}/{dir}/{file}", + fmt::arg("dir", dir_src), fmt::arg("file", f))); + } + + fmt::memory_buffer buff; + fmt::format_to(buff, cmake_recipe_template, + fmt::arg("project", GetProjectName()), + fmt::arg("dir_app", dir_app), + fmt::arg("source_files", fmt::join(src_files, "\n")), + fmt::arg("dir_include", dir_include)); + WriteFile(os_portable_append_dir(dir, "CMakeLists.txt"), buff); // dummy main function if not exist - auto app_template = + static const char* sim_entry_template = + "#include <{project}.h>\n\n" + "int sc_main(int argc, char* argv[]) {{\n" + " return 0; \n" + "}}\n"; + + auto entry_path = os_portable_append_dir(os_portable_append_dir(dir, dir_app), "main.cc"); - if (!os_portable_exist(app_template)) { + + if (!os_portable_exist(entry_path)) { buff.clear(); - fmt::format_to(buff, - "#include <{project}.h>\n\n" - "int sc_main(int argc, char* argv[]) {{\n" - " return 0; \n" - "}}\n", + fmt::format_to(buff, sim_entry_template, fmt::arg("project", GetProjectName())); - WriteFile(app_template, buff); + WriteFile(entry_path, buff); } return true; @@ -540,17 +574,7 @@ bool Ilator::GenerateBuildSupport(const std::string& dir) { bool Ilator::RenderExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { auto ExprDfsVisiter = [this, &buff, &lut](const ExprPtr& e) { - if (auto pos = lut.find(e); pos == lut.end()) { - if (e->is_var()) { - DfsVar(e, buff, lut); - } else if (e->is_const()) { - DfsConst(e, buff, lut); - } else { - ILA_ASSERT(e->is_op()); - DfsOp(e, buff, lut); - } - } - ILA_ASSERT((e->is_mem() && e->is_op()) || (lut.find(e) != lut.end())); + DfsExpr(e, buff, lut); }; try { diff --git a/src/target-sc/ilator_dfs.cc b/src/target-sc/ilator_dfs.cc index 3db47f43b..3b2cf7db6 100644 --- a/src/target-sc/ilator_dfs.cc +++ b/src/target-sc/ilator_dfs.cc @@ -10,6 +10,20 @@ namespace ilang { +void Ilator::DfsExpr(const ExprPtr& e, StrBuff& buff, ExprVarMap& lut) { + if (auto pos = lut.find(e); pos == lut.end()) { + if (e->is_var()) { + DfsVar(e, buff, lut); + } else if (e->is_const()) { + DfsConst(e, buff, lut); + } else { + ILA_ASSERT(e->is_op()); + DfsOp(e, buff, lut); + } + } + ILA_ASSERT((e->is_mem() && e->is_op()) || (lut.find(e) != lut.end())); +} + void Ilator::DfsVar(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) const { auto [it, status] = lut.try_emplace(expr, GetCxxName(expr)); ILA_ASSERT(status); From 865827b73430ce014ea2411921fba2eb40826918 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 11 Jul 2020 00:34:51 -0400 Subject: [PATCH 16/30] Roll back for compatibility --- src/ila-mngr/u_unroller.cc | 4 ++-- test/t_symbol.cc | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/ila-mngr/u_unroller.cc b/src/ila-mngr/u_unroller.cc index a85e401fa..1a6a5f108 100644 --- a/src/ila-mngr/u_unroller.cc +++ b/src/ila-mngr/u_unroller.cc @@ -304,8 +304,8 @@ void Unroller::CopyZExprVec(const ZExprVec& src, ZExprVec& dst) { ZExpr Unroller::ConjPred(const ZExprVec& vec) const { auto conj = ctx().bool_val(true); - for (const auto& p : vec) { - conj = (conj && p); + for (size_t i = 0; i != vec.size(); i++) { + conj = (conj && vec[i]); } conj = conj.simplify(); return conj; diff --git a/test/t_symbol.cc b/test/t_symbol.cc index fd897061c..97d8d60df 100644 --- a/test/t_symbol.cc +++ b/test/t_symbol.cc @@ -64,9 +64,9 @@ TEST(TestSymbol, Copy) { TEST(TestSymbol, Format) { Symbol sym("name"); - EXPECT_EQ("name_suf", sym.format_str("", "suf")); - EXPECT_EQ("pre_name", sym.format_str("pre", "")); - EXPECT_EQ("p_name_s", sym.format_str("p", "s")); + EXPECT_EQ("name_sEp_suf", sym.format_str("", "suf")); + EXPECT_EQ("pre_sEp_name", sym.format_str("pre", "")); + EXPECT_EQ("p_sEp_name_sEp_s", sym.format_str("p", "s")); } TEST(TestSymbol, Compare) { From 676a1068a4065921ed4b8cd00c63c789c9f3741f Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 11 Jul 2020 22:02:24 -0400 Subject: [PATCH 17/30] Remove redundant dependency --- azure-pipelines.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 32fd209fe..e87518651 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -63,7 +63,6 @@ jobs: sudo apt-get update sudo apt-get install bison sudo apt-get install flex - sudo apt-get install libboost-all-dev sudo apt-get install z3 sudo apt-get install libz3-dev displayName: 'package' @@ -84,7 +83,6 @@ jobs: sudo apt-get update sudo apt-get install bison sudo apt-get install flex - sudo apt-get install libboost-all-dev sudo apt-get install z3 sudo apt-get install libz3-dev displayName: 'package' From 24469bb9cb9fff1754fd59d7b88679faadfa89c2 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 11 Jul 2020 22:57:40 -0400 Subject: [PATCH 18/30] Setup initial condition via z3 solving --- include/ilang/target-sc/ilator.h | 2 + src/target-sc/ilator.cc | 67 ++++++++++++++++++++++++++++++-- test/t_ilator.cc | 5 ++- 3 files changed, 69 insertions(+), 5 deletions(-) diff --git a/include/ilang/target-sc/ilator.h b/include/ilang/target-sc/ilator.h index 56db5b3f1..78c79ee32 100644 --- a/include/ilang/target-sc/ilator.h +++ b/include/ilang/target-sc/ilator.h @@ -82,6 +82,8 @@ class Ilator { bool GenerateMemoryUpdate(const std::string& dir); /// Special handle for constant memory. bool GenerateConstantMemory(const std::string& dir); + /// Generate setup function for initial condition. + bool GenerateInitialSetup(const std::string& dir); /// Generate the instruction scheduler and driver. bool GenerateExecuteKernel(const std::string& dir); /// Generate the shared header files. diff --git a/src/target-sc/ilator.cc b/src/target-sc/ilator.cc index f638649e2..f867b1940 100644 --- a/src/target-sc/ilator.cc +++ b/src/target-sc/ilator.cc @@ -4,10 +4,13 @@ #include #include +#include #include #include #include +#include +#include #include #include @@ -85,6 +88,9 @@ void Ilator::Generate(const std::string& dst) { // constant memory status &= GenerateConstantMemory(os_portable_append_dir(dst, dir_src)); + // initial condition setup + status &= GenerateInitialSetup(os_portable_append_dir(dst, dir_src)); + // execution kernel status &= GenerateExecuteKernel(os_portable_append_dir(dst, dir_src)); @@ -346,8 +352,56 @@ bool Ilator::GenerateConstantMemory(const std::string& dir) { return true; } +bool Ilator::GenerateInitialSetup(const std::string& dir) { + // conjunct all initial condition + auto init = ExprFuse::BoolConst(true); + auto ConjInit = [&init](const InstrLvlAbsCnstPtr& m) { + for (size_t i = 0; i < m->init_num(); i++) { + init = ExprFuse::And(init, m->init(i)); + } + }; + m_->DepthFirstVisit(ConjInit); + + // get value for referred vars + z3::context ctx; + z3::solver solver(ctx); + Z3ExprAdapter gen(ctx); + solver.add(gen.GetExpr(init)); + auto res = solver.check(); + if (res != z3::sat) { + ILA_ERROR << "Fail finding assignment satisfying initial condition"; + return false; + } + + std::map init_values; + auto model = solver.get_model(); + auto refer_vars = AbsKnob::GetVar(init); + for (const auto& var : refer_vars) { + auto var_value = model.eval(gen.GetExpr(var)); + try { + init_values.emplace(var, var_value.get_numeral_uint64()); + } catch (...) { + ILA_ERROR << "Fail getting " << var_value; + return false; + } + } + + // gen file + auto init_func = RegisterFunction("setup_initial_condition"); + fmt::memory_buffer buff; + fmt::format_to(buff, "#include <{}.h>\n", GetProjectName()); + BeginFuncDef(init_func, buff); + for (auto pair : init_values) { + fmt::format_to(buff, "{var_name} = {var_value};\n", + fmt::arg("var_name", GetCxxName(pair.first)), + fmt::arg("var_value", pair.second)); + } + EndFuncDef(init_func, buff); + CommitSource("setup_initial_condition.cc", dir, buff); + return true; +} + bool Ilator::GenerateExecuteKernel(const std::string& dir) { - auto kernel_func = RegisterFunction("compute"); fmt::memory_buffer buff; fmt::format_to( // headers @@ -366,16 +420,23 @@ bool Ilator::GenerateExecuteKernel(const std::string& dir) { "}}\n", fmt::arg("project", GetProjectName())); + fmt::format_to(buff, "static bool g_initialized = false;\n"); + + auto kernel_func = RegisterFunction("compute"); BeginFuncDef(kernel_func, buff); + // setup initial condition + fmt::format_to(buff, "if (!g_initialized) {{\n" + " setup_initial_condition();\n" + " g_initialized = true;\n" + "}}\n"); + // read in input value for (size_t i = 0; i < m_->input_num(); i++) { fmt::format_to(buff, "{input_name} = {input_name}_in.read();\n", fmt::arg("input_name", GetCxxName(m_->input(i)))); } - // init TODO - // instruction execution auto ExecInstr = [this, &buff](const InstrPtr& instr, bool child) { fmt::format_to( diff --git a/test/t_ilator.cc b/test/t_ilator.cc index ff96ff537..e58f32b1f 100644 --- a/test/t_ilator.cc +++ b/test/t_ilator.cc @@ -18,13 +18,14 @@ class TestIlator : public ::testing::Test { ~TestIlator() {} void SetUp() { - out_dir = GetRandomFileName(fs::temp_directory_path()); + // out_dir = GetRandomFileName(fs::temp_directory_path()); + out_dir = GetRandomFileName(fs::current_path()); os_portable_mkdir(out_dir); } void TearDown() { // for CI tests, may be needed for out-of-scope build tests - os_portable_remove_directory(out_dir); + // os_portable_remove_directory(out_dir); } fs::path out_dir; From 0ceb579b0b7e35566a2399523b35d2985b49b870 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 11 Jul 2020 23:00:06 -0400 Subject: [PATCH 19/30] Revert mistakenly commited modification --- test/t_ilator.cc | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/test/t_ilator.cc b/test/t_ilator.cc index e58f32b1f..ff96ff537 100644 --- a/test/t_ilator.cc +++ b/test/t_ilator.cc @@ -18,14 +18,13 @@ class TestIlator : public ::testing::Test { ~TestIlator() {} void SetUp() { - // out_dir = GetRandomFileName(fs::temp_directory_path()); - out_dir = GetRandomFileName(fs::current_path()); + out_dir = GetRandomFileName(fs::temp_directory_path()); os_portable_mkdir(out_dir); } void TearDown() { // for CI tests, may be needed for out-of-scope build tests - // os_portable_remove_directory(out_dir); + os_portable_remove_directory(out_dir); } fs::path out_dir; From 8b9dbf75f029eb4eb5c2d95053261ebcc374b9f2 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sat, 11 Jul 2020 23:35:39 -0400 Subject: [PATCH 20/30] Support legacy z3 API for backward compatibility --- src/target-sc/ilator.cc | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/target-sc/ilator.cc b/src/target-sc/ilator.cc index f867b1940..deefce3cf 100644 --- a/src/target-sc/ilator.cc +++ b/src/target-sc/ilator.cc @@ -6,6 +6,7 @@ #include #include +#include #include #include #include @@ -379,7 +380,13 @@ bool Ilator::GenerateInitialSetup(const std::string& dir) { for (const auto& var : refer_vars) { auto var_value = model.eval(gen.GetExpr(var)); try { - init_values.emplace(var, var_value.get_numeral_uint64()); +#ifndef Z3_LEGACY_API + auto value_holder = var_value.get_numeral_uint64(); +#else + __uint64 value_holder; + Z3_get_numeral_uint64(ctx, var_value, &value_holder); +#endif + init_values.emplace(var, value_holder); } catch (...) { ILA_ERROR << "Fail getting " << var_value; return false; From 75906d7fab520b917f10a4b30bb68f33f0db3c75 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 12 Jul 2020 18:40:34 -0400 Subject: [PATCH 21/30] Fix #158. Rely on standard library hash function for string --- include/ilang/ila/hash_ast.h | 16 ++++----- src/ila/hash_ast.cc | 70 +++++++++++++++++++----------------- 2 files changed, 44 insertions(+), 42 deletions(-) diff --git a/include/ilang/ila/hash_ast.h b/include/ilang/ila/hash_ast.h index b562ddf22..9ed2ec154 100644 --- a/include/ilang/ila/hash_ast.h +++ b/include/ilang/ila/hash_ast.h @@ -14,17 +14,15 @@ namespace ilang { /// \brief Simplifier for AST trees by sharing nodes based on the hash value. class ExprMngr { public: + /// Pointer type for passing shared ast simplifier. + typedef std::shared_ptr ExprMngrPtr; + // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // /// Default constructor. ExprMngr(); /// Default destructor. ~ExprMngr(); - /// Pointer type for passing shared ast simplifier. - typedef std::shared_ptr ExprMngrPtr; - /// Type for cacheing the AST node hashing. - typedef std::unordered_map HashTable; - // ------------------------- HELPERS -------------------------------------- // /// \brief Create an object and return the pointer. Used for hiding /// implementation specific types. @@ -36,18 +34,18 @@ class ExprMngr { // ------------------------- METHODS -------------------------------------- // /// Return the AST node representative. - ExprPtr GetRep(const ExprPtr node); + ExprPtr GetRep(const ExprPtr& node); /// Function object for sharing ast nodes. - void operator()(const ExprPtr node); + void operator()(const ExprPtr& node); private: // ------------------------- MEMBERS -------------------------------------- // /// The map for AST nodes. - HashTable map_; + std::unordered_map map_; // ------------------------- HELPER FUNCTIONS ----------------------------- // /// Hash function. - size_t Hash(const ExprPtr node) const; + static std::string Hash(const ExprPtr& node); }; // class ExprMngr diff --git a/src/ila/hash_ast.cc b/src/ila/hash_ast.cc index 93598f239..3121d91e0 100644 --- a/src/ila/hash_ast.cc +++ b/src/ila/hash_ast.cc @@ -1,12 +1,12 @@ /// \file /// Source for the class ExprMngr and the corresponding hash -// XXX Current replacing is not efficient. - #include +#include #include +#include #include namespace ilang { @@ -19,7 +19,7 @@ ExprMngrPtr ExprMngr::New() { return std::make_shared(); } void ExprMngr::clear() { map_.clear(); } -ExprPtr ExprMngr::GetRep(const ExprPtr node) { +ExprPtr ExprMngr::GetRep(const ExprPtr& node) { node->DepthFirstVisit(*this); auto pos = map_.find(Hash(node)); @@ -30,7 +30,7 @@ ExprPtr ExprMngr::GetRep(const ExprPtr node) { return pos->second; } -void ExprMngr::operator()(const ExprPtr node) { +void ExprMngr::operator()(const ExprPtr& node) { ExprPtrVec reps; // replace child (must exist) for (size_t i = 0; i != node->arg_num(); i++) { @@ -49,44 +49,48 @@ void ExprMngr::operator()(const ExprPtr node) { auto pos = map_.find(hash); // new node if (pos == map_.end()) { - map_.insert({hash, node}); + map_.emplace(hash, node); } } -static std::hash ptr_hash_fn; -static std::hash str_hash_fn; -static std::hash int_hash_fn; +std::string ExprMngr::Hash(const ExprPtr& expr) { + static const char* template_var = "var::{id}"; + static const char* template_const = "const::{sort}::{value}"; + static const char* template_op = "op::{op}::{arg_list}::{param_list}"; + + if (expr->is_var()) { + return fmt::format(template_var, fmt::arg("id", expr->name().id())); -size_t ExprMngr::Hash(const ExprPtr n) const { - if (n->is_op()) { // ExprOp - auto n_op = std::static_pointer_cast(n); + } else if (expr->is_const()) { + auto const_expr = std::static_pointer_cast(expr); - std::string op_name_str = n_op->op_name(); - auto hash = str_hash_fn(op_name_str); - for (size_t i = 0; i != n->arg_num(); i++) { - hash ^= (ptr_hash_fn(n->arg(i)) << (i * 8)); + std::string value = std::to_string(expr->name().id()); + if (expr->is_bool()) { + value = const_expr->val_bool()->str(); + } else if (expr->is_bv()) { + value = fmt::format("{}_{}", const_expr->val_bv()->val(), + expr->sort()->bit_width()); } - for (size_t i = 0; i != n->param_num(); i++) { - hash ^= (int_hash_fn(n->param(i)) << (i * 8)); + // skip sharing memory constants + + return fmt::format(template_const, + fmt::arg("sort", GetUidSort(expr->sort())), + fmt::arg("value", value)); + } else { + ILA_ASSERT(expr->is_op()); + std::vector arg_list; + for (size_t i = 0; i < expr->arg_num(); i++) { + arg_list.push_back(expr->arg(i)->name().id()); } - return hash; - } else if (n->is_var()) { // ExprVar - return n->name().id(); - } else { // ExprConst - ILA_ASSERT(n->is_const()) << "Unrecognized expr type"; - auto n_const = std::static_pointer_cast(n); - - if (n_const->is_bool()) { - return str_hash_fn(n_const->val_bool()->str()); - } else if (n_const->is_bv()) { - auto bv_str = n_const->val_bv()->str() + "_" + - std::to_string(n_const->sort()->bit_width()); - return str_hash_fn(bv_str); - } else { - ILA_ASSERT(n_const->is_mem()) << "Unrecognized constant type"; - return str_hash_fn(n_const->name().str()); + std::vector param_list; + for (size_t i = 0; i < expr->param_num(); i++) { + param_list.push_back(expr->param(i)); } + + return fmt::format(template_op, fmt::arg("op", GetUidExprOp(expr)), + fmt::arg("arg_list", fmt::join(arg_list, ",")), + fmt::arg("param_list", fmt::join(param_list, ","))); } } From bcaa390a106e8bf2abb6c83903b8080fbdd21f77 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 12 Jul 2020 19:42:48 -0400 Subject: [PATCH 22/30] New pass - simplify instruction syntactically --- include/ilang/ila-mngr/pass.h | 10 +++++++ src/ila-mngr/CMakeLists.txt | 1 + src/ila-mngr/p_simplify_syntactic.cc | 42 ++++++++++++++++++++++++++++ src/ila/hash_ast.cc | 23 +++++++++++---- test/t_pass.cc | 1 + 5 files changed, 71 insertions(+), 6 deletions(-) create mode 100644 src/ila-mngr/p_simplify_syntactic.cc diff --git a/include/ilang/ila-mngr/pass.h b/include/ilang/ila-mngr/pass.h index e2b3e989e..16cd289c6 100644 --- a/include/ilang/ila-mngr/pass.h +++ b/include/ilang/ila-mngr/pass.h @@ -34,6 +34,16 @@ bool PassRewriteGeneric(const InstrLvlAbsPtr& m, /// \param[in] timeout Max time (ms) for each SMT query. (-1 for default) bool PassSimplifyInstrUpdate(const InstrLvlAbsPtr& m, const int& timeout = -1); +/// \namespace pass +namespace pass { + +/// \brief Simplify instructions (across the hierarchy) syntactically. +/// (Light-weight simplification, no SMT query.) +/// \param[in] m The top-level ILA. +bool SimplifySyntactic(const InstrLvlAbsCnstPtr& m); + +} // namespace pass + }; // namespace ilang #endif // ILANG_ILA_MNGR_PASS_H__ diff --git a/src/ila-mngr/CMakeLists.txt b/src/ila-mngr/CMakeLists.txt index 013bd7ba6..8ab9fc347 100644 --- a/src/ila-mngr/CMakeLists.txt +++ b/src/ila-mngr/CMakeLists.txt @@ -8,6 +8,7 @@ target_sources(${ILANG_LIB_NAME} PRIVATE ${CMAKE_CURRENT_SOURCE_DIR}/p_rewrite_generic.cc ${CMAKE_CURRENT_SOURCE_DIR}/p_rewrite_store_load.cc ${CMAKE_CURRENT_SOURCE_DIR}/p_simplify_instr_update.cc + ${CMAKE_CURRENT_SOURCE_DIR}/p_simplify_syntactic.cc ${CMAKE_CURRENT_SOURCE_DIR}/u_abs_knob.cc ${CMAKE_CURRENT_SOURCE_DIR}/u_rewrite_expr.cc ${CMAKE_CURRENT_SOURCE_DIR}/u_rewrite_ila.cc diff --git a/src/ila-mngr/p_simplify_syntactic.cc b/src/ila-mngr/p_simplify_syntactic.cc new file mode 100644 index 000000000..a452b36e4 --- /dev/null +++ b/src/ila-mngr/p_simplify_syntactic.cc @@ -0,0 +1,42 @@ +/// \file +/// Simplify Expr node syntactically (structurally). + +#include + +#include +#include + +namespace ilang { + +namespace pass { + +bool SimplifySyntactic(const InstrLvlAbsCnstPtr& m) { + ILA_NOT_NULL(m); + + auto mngr = ExprMngr::New(); + auto visiter = [&mngr](const InstrLvlAbsCnstPtr& current) { + try { + // only simplify instructions + for (size_t i = 0; i < current->instr_num(); i++) { + auto instr = current->instr(i); + // decode + ILA_NOT_NULL(instr->decode()); + instr->ForceSetDecode(mngr->GetRep(instr->decode())); + // state updates + auto updated_states = instr->updated_states(); + for (const auto& state : updated_states) { + instr->ForceAddUpdate(state, mngr->GetRep(instr->update(state))); + } + } + } catch (...) { + ILA_ERROR << "Fail simplify " << current; + } + }; + + m->DepthFirstVisit(visiter); + return true; +} + +} // namespace pass + +} // namespace ilang diff --git a/src/ila/hash_ast.cc b/src/ila/hash_ast.cc index 3121d91e0..b7797811b 100644 --- a/src/ila/hash_ast.cc +++ b/src/ila/hash_ast.cc @@ -54,12 +54,23 @@ void ExprMngr::operator()(const ExprPtr& node) { } std::string ExprMngr::Hash(const ExprPtr& expr) { - static const char* template_var = "var::{id}"; + static const char* template_var = "var::{sort}::{id}"; static const char* template_const = "const::{sort}::{value}"; - static const char* template_op = "op::{op}::{arg_list}::{param_list}"; + static const char* template_op = "op::{sort}::{op}::{arg_list}::{param_list}"; + static const char* template_sort = "{type}_{bit}_{addr}_{data}"; + + auto GetSortHash = [](const SortPtr& sort) { + return fmt::format( + template_sort, fmt::arg("type", GetUidSort(sort)), + fmt::arg("bit", sort->is_bv() ? sort->bit_width() : 0), + fmt::arg("addr", sort->is_mem() ? sort->addr_width() : 0), + fmt::arg("data", sort->is_mem() ? sort->data_width() : 0)); + }; if (expr->is_var()) { - return fmt::format(template_var, fmt::arg("id", expr->name().id())); + return fmt::format(template_var, + fmt::arg("sort", GetSortHash(expr->sort())), + fmt::arg("id", expr->name().id())); } else if (expr->is_const()) { auto const_expr = std::static_pointer_cast(expr); @@ -68,13 +79,12 @@ std::string ExprMngr::Hash(const ExprPtr& expr) { if (expr->is_bool()) { value = const_expr->val_bool()->str(); } else if (expr->is_bv()) { - value = fmt::format("{}_{}", const_expr->val_bv()->val(), - expr->sort()->bit_width()); + value = const_expr->val_bv()->str(); } // skip sharing memory constants return fmt::format(template_const, - fmt::arg("sort", GetUidSort(expr->sort())), + fmt::arg("sort", GetSortHash(expr->sort())), fmt::arg("value", value)); } else { ILA_ASSERT(expr->is_op()); @@ -89,6 +99,7 @@ std::string ExprMngr::Hash(const ExprPtr& expr) { } return fmt::format(template_op, fmt::arg("op", GetUidExprOp(expr)), + fmt::arg("sort", GetSortHash(expr->sort())), fmt::arg("arg_list", fmt::join(arg_list, ",")), fmt::arg("param_list", fmt::join(param_list, ","))); } diff --git a/test/t_pass.cc b/test/t_pass.cc index e569a4344..2e8020800 100644 --- a/test/t_pass.cc +++ b/test/t_pass.cc @@ -24,6 +24,7 @@ void ApplyPass(const std::string& dir, const std::string& file, auto ila_file = os_portable_append_dir(file_dir, file); auto ila = ImportIlaPortable(ila_file).get(); + pass::SimplifySyntactic(ila); PassSimplifyInstrUpdate(ila); PassRewriteConditionalStore(ila); From 9c927253e9c4a244c74685864e0eb400d1d48ac0 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 12 Jul 2020 23:49:05 -0400 Subject: [PATCH 23/30] Clean up pass and bug fix --- include/ilang/ila-mngr/pass.h | 26 ++++---- include/ilang/ila-mngr/u_rewriter.h | 30 +++++---- include/ilang/ilang++.h | 6 +- include/ilang/target-sc/ilator.h | 5 +- src/ila-mngr/CMakeLists.txt | 2 +- src/ila-mngr/p_infer_child_prog_cfg.cc | 11 +++- src/ila-mngr/p_map_child_prog_entry.cc | 9 ++- src/ila-mngr/p_rewrite_conditional_store.cc | 11 +++- src/ila-mngr/p_rewrite_generic.cc | 35 +++++------ src/ila-mngr/p_rewrite_store_load.cc | 35 +++-------- ...instr_update.cc => p_simplify_semantic.cc} | 60 +++++++++--------- src/ila-mngr/p_simplify_syntactic.cc | 30 +++------ src/ila-mngr/u_abs_knob.cc | 11 ++-- src/ila-mngr/u_rewrite_expr.cc | 12 ++-- src/ila-mngr/u_rewrite_ila.cc | 10 +-- src/ila/hash_ast.cc | 4 ++ src/ilang++.cc | 4 +- src/target-sc/ilator.cc | 62 +++++++++++++------ test/t_ilator.cc | 7 ++- test/t_pass.cc | 12 ++-- 20 files changed, 199 insertions(+), 183 deletions(-) rename src/ila-mngr/{p_simplify_instr_update.cc => p_simplify_semantic.cc} (69%) diff --git a/include/ilang/ila-mngr/pass.h b/include/ilang/ila-mngr/pass.h index 16cd289c6..949b414e4 100644 --- a/include/ilang/ila-mngr/pass.h +++ b/include/ilang/ila-mngr/pass.h @@ -11,36 +11,36 @@ /// \namespace ilang namespace ilang { +/// \namespace pass +namespace pass { + /// Infer the control flow graph among the child-instructions (instr. seq.) -bool PassInferChildProgCFG(const InstrLvlAbsPtr& m); +bool InferChildProgCFG(const InstrLvlAbsPtr& m); /// Map the child program (and its entry point) to the parent instruction -bool PassMapChildProgEntryPoint(const InstrLvlAbsPtr& m); +bool MapChildProgEntryPoint(const InstrLvlAbsPtr& m); /// Rewrite the conditional STORE in the AST. -bool PassRewriteConditionalStore(const InstrLvlAbsPtr& m); +bool RewriteConditionalStore(const InstrLvlAbsPtr& m); /// Rewrite the STORE-LOAD pattern in the AST. -bool PassRewriteStoreLoad(const InstrLvlAbsPtr& m); +bool RewriteStoreLoad(const InstrLvlAbsPtr& m); /// A pass template for rewriting AST in an ILA. /// \param[in] m The target ILA. /// \param[in] Rewr The pass-specific rewriting function. -bool PassRewriteGeneric(const InstrLvlAbsPtr& m, - std::function Rewr); +bool RewriteGeneric(const InstrLvlAbsPtr& m, + std::function Rewr); -/// Simplify instruction state updates. -/// \param[in] m The target ILA. +/// \brief Simplify instructions (across the hierarchy) semantically (z3). +/// \param[in] m The top-level ILA. /// \param[in] timeout Max time (ms) for each SMT query. (-1 for default) -bool PassSimplifyInstrUpdate(const InstrLvlAbsPtr& m, const int& timeout = -1); - -/// \namespace pass -namespace pass { +bool SimplifySemantic(const InstrLvlAbsCnstPtr& m, const int& timeout = -1); /// \brief Simplify instructions (across the hierarchy) syntactically. /// (Light-weight simplification, no SMT query.) /// \param[in] m The top-level ILA. -bool SimplifySyntactic(const InstrLvlAbsCnstPtr& m); +bool SimplifySyntactic(const InstrLvlAbsPtr& m); } // namespace pass diff --git a/include/ilang/ila-mngr/u_rewriter.h b/include/ilang/ila-mngr/u_rewriter.h index a698c9e1a..8e141db11 100644 --- a/include/ilang/ila-mngr/u_rewriter.h +++ b/include/ilang/ila-mngr/u_rewriter.h @@ -15,41 +15,42 @@ class FuncObjRewrExpr { FuncObjRewrExpr(const ExprMap& rule) : rule_(rule) {} /// Return the rewritten result. - ExprPtr get(const ExprPtr e) const; + ExprPtr get(const ExprPtr& e) const; /// Pre-process: return true (break) if the node has been visited. - bool pre(const ExprPtr e) const; + bool pre(const ExprPtr& e) const; /// Post-process: update the rewriting rule map. - void post(const ExprPtr e); + void post(const ExprPtr& e); protected: /// Internal rewriting table. ExprMap rule_; /// Rewrite all sorts of Expr. - virtual ExprPtr Rewrite(const ExprPtr e) const; + virtual ExprPtr Rewrite(const ExprPtr& e) const; /// Rewrite Operation sorted Expr. - virtual ExprPtr RewriteOp(const ExprPtr e) const; + virtual ExprPtr RewriteOp(const ExprPtr& e) const; }; // class FuncObjRewrExpr /// \brief Function object for rewriting ILA tree. class FuncObjRewrIla { -public: +private: /// Type for storing ILA to ILA mapping. typedef CnstIlaMap IlaMap; +public: /// Constructor. FuncObjRewrIla(const IlaMap& ila_map, const ExprMap& expr_map) : ila_map_(ila_map), expr_map_(expr_map) {} /// Return the mapped ILA. - InstrLvlAbsPtr get(const InstrLvlAbsCnstPtr m) const; + InstrLvlAbsPtr get(const InstrLvlAbsCnstPtr& m) const; /// Pre-processing: create new ILA based on the given source. - bool pre(const InstrLvlAbsCnstPtr src); + bool pre(const InstrLvlAbsCnstPtr& src); /// Nothing. - void post(const InstrLvlAbsCnstPtr src) const; + void post(const InstrLvlAbsCnstPtr& src) const; private: /// ILA mapping. @@ -71,21 +72,24 @@ class FuncObjFlatIla { - Hongce */ -public: +private: /// Type for storing ILA to ILA mapping. typedef CnstIlaMap IlaMap; - typedef std::stack ValidCondStack; +public: /// Constructor. FuncObjFlatIla(const InstrLvlAbsCnstPtr& top_, const IlaMap& ila_map, const ExprMap& expr_map); /// Pre-processing: create new ILA based on the given source. - bool pre(const InstrLvlAbsCnstPtr src); + bool pre(const InstrLvlAbsCnstPtr& src); /// Nothing. - void post(const InstrLvlAbsCnstPtr src); + void post(const InstrLvlAbsCnstPtr& src); private: + /// Type for holding valid condition stack across the hierarchy. + typedef std::stack ValidCondStack; + /// ILA mapping. IlaMap ila_map_; /// Expr mapping. diff --git a/include/ilang/ilang++.h b/include/ilang/ilang++.h index e84d068da..7e9db9a4d 100644 --- a/include/ilang/ilang++.h +++ b/include/ilang/ilang++.h @@ -619,7 +619,11 @@ void ImportChildSynthAbstraction(const std::string& file_name, Ila& parent, const std::string& ila_name); /// \brief Generate the SystemC simulator. -void ExportSysCSim(const Ila& ila, const std::string& dir_path); +/// \param [in] ila the top-level ILA to generate. +/// \param [in] dir_path directory path of the generated simulator. +/// \param [in] optimize set true to enable optimization. +void ExportSysCSim(const Ila& ila, const std::string& dir_path, + bool optimize = false); /******************************************************************************/ // Verification. diff --git a/include/ilang/target-sc/ilator.h b/include/ilang/target-sc/ilator.h index 78c79ee32..2eae3ee9b 100644 --- a/include/ilang/target-sc/ilator.h +++ b/include/ilang/target-sc/ilator.h @@ -29,7 +29,8 @@ class Ilator { // ------------------------- METHODS -------------------------------------- // /// \brief Generate the SystemC simulator. /// \param[in] dst the directory path for the generated simulator. - void Generate(const std::string& dst); + /// \param[in] opt set true to enable optimization. + void Generate(const std::string& dst, bool opt); private: /// Internal type of the string buffer. @@ -74,7 +75,7 @@ class Ilator { /// Check if the ILA model contains unsupported patterns. bool SanityCheck() const; /// Generation bootstrap, e.g., creating directories. - bool Bootstrap(const std::string& root); + bool Bootstrap(const std::string& root, bool opt); /// Interpret instruction semantics (decode and state updates). bool GenerateInstrContent(const InstrPtr& instr, const std::string& dir); diff --git a/src/ila-mngr/CMakeLists.txt b/src/ila-mngr/CMakeLists.txt index 8ab9fc347..957ffae4e 100644 --- a/src/ila-mngr/CMakeLists.txt +++ b/src/ila-mngr/CMakeLists.txt @@ -7,7 +7,7 @@ target_sources(${ILANG_LIB_NAME} PRIVATE ${CMAKE_CURRENT_SOURCE_DIR}/p_rewrite_conditional_store.cc ${CMAKE_CURRENT_SOURCE_DIR}/p_rewrite_generic.cc ${CMAKE_CURRENT_SOURCE_DIR}/p_rewrite_store_load.cc - ${CMAKE_CURRENT_SOURCE_DIR}/p_simplify_instr_update.cc + ${CMAKE_CURRENT_SOURCE_DIR}/p_simplify_semantic.cc ${CMAKE_CURRENT_SOURCE_DIR}/p_simplify_syntactic.cc ${CMAKE_CURRENT_SOURCE_DIR}/u_abs_knob.cc ${CMAKE_CURRENT_SOURCE_DIR}/u_rewrite_expr.cc diff --git a/src/ila-mngr/p_infer_child_prog_cfg.cc b/src/ila-mngr/p_infer_child_prog_cfg.cc index 556bbc326..caab1c596 100644 --- a/src/ila-mngr/p_infer_child_prog_cfg.cc +++ b/src/ila-mngr/p_infer_child_prog_cfg.cc @@ -8,8 +8,11 @@ namespace ilang { -bool PassInferChildProgCFG(const InstrLvlAbsPtr& m) { +namespace pass { + +bool InferChildProgCFG(const InstrLvlAbsPtr& m) { ILA_NOT_NULL(m); + ILA_INFO << "Start pass: infer child program control-flow"; // iterate through child-ILAs for (size_t i = 0; i < m->child_num(); i++) { @@ -51,10 +54,12 @@ bool PassInferChildProgCFG(const InstrLvlAbsPtr& m) { ILA_WARN_IF(!child->instr_seq()) << "Fail to infer CFG for " << child; // traverse the hierarchy - PassInferChildProgCFG(child); + InferChildProgCFG(child); } return true; } -}; // namespace ilang +} // namespace pass + +} // namespace ilang diff --git a/src/ila-mngr/p_map_child_prog_entry.cc b/src/ila-mngr/p_map_child_prog_entry.cc index c4b47e87b..6a6640a28 100644 --- a/src/ila-mngr/p_map_child_prog_entry.cc +++ b/src/ila-mngr/p_map_child_prog_entry.cc @@ -8,8 +8,11 @@ namespace ilang { -bool PassMapChildProgEntryPoint(const InstrLvlAbsPtr& m) { +namespace pass { + +bool MapChildProgEntryPoint(const InstrLvlAbsPtr& m) { ILA_NOT_NULL(m); + ILA_INFO << "Start pass: mapping child program entry"; // check if a can trigger b auto CheckCausality = [=](InstrPtr a, InstrPtr b) { @@ -93,4 +96,6 @@ bool PassMapChildProgEntryPoint(const InstrLvlAbsPtr& m) { return true; } -}; // namespace ilang +} // namespace pass + +} // namespace ilang diff --git a/src/ila-mngr/p_rewrite_conditional_store.cc b/src/ila-mngr/p_rewrite_conditional_store.cc index 118341923..e6101597a 100644 --- a/src/ila-mngr/p_rewrite_conditional_store.cc +++ b/src/ila-mngr/p_rewrite_conditional_store.cc @@ -10,6 +10,8 @@ namespace ilang { +namespace pass { + class FuncObjRewrCondStore : public FuncObjRewrExpr { public: FuncObjRewrCondStore() : FuncObjRewrExpr({}) {} @@ -107,8 +109,9 @@ class FuncObjRewrCondStore : public FuncObjRewrExpr { }; // class FuncObjRewrCondStore -bool PassRewriteConditionalStore(const InstrLvlAbsPtr& m) { +bool RewriteConditionalStore(const InstrLvlAbsPtr& m) { ILA_NOT_NULL(m); + ILA_INFO << "Start pass: rewrite conditional store"; auto func = FuncObjRewrCondStore(); auto Rewr = [=, &func](const ExprPtr e) { @@ -119,7 +122,9 @@ bool PassRewriteConditionalStore(const InstrLvlAbsPtr& m) { return e; }; - return PassRewriteGeneric(m, Rewr); + return RewriteGeneric(m, Rewr); } -}; // namespace ilang +} // namespace pass + +} // namespace ilang diff --git a/src/ila-mngr/p_rewrite_generic.cc b/src/ila-mngr/p_rewrite_generic.cc index f7495c4a2..056887c9a 100644 --- a/src/ila-mngr/p_rewrite_generic.cc +++ b/src/ila-mngr/p_rewrite_generic.cc @@ -7,20 +7,20 @@ namespace ilang { -bool PassRewriteGeneric(const InstrLvlAbsPtr& m, - std::function Rewr) { +namespace pass { + +bool RewriteGeneric(const InstrLvlAbsPtr& m, + std::function Rewr) { ILA_NOT_NULL(m); // rewrite valid - auto new_valid = Rewr(m->valid()); - if (new_valid) { - m->ForceSetValid(new_valid); + if (m->valid()) { + m->ForceSetValid(Rewr(m->valid())); } // rewrite fetch - auto new_fetch = Rewr(m->fetch()); - if (new_fetch) { - m->ForceSetFetch(new_fetch); + if (m->fetch()) { + m->ForceSetFetch(Rewr(m->fetch())); } // TODO rewrite init @@ -30,26 +30,23 @@ bool PassRewriteGeneric(const InstrLvlAbsPtr& m, auto instr = m->instr(i); // rewrite decode - auto new_decode = Rewr(instr->decode()); - if (new_decode) { - instr->ForceSetDecode(new_decode); - } + ILA_NOT_NULL(instr->decode()); + instr->ForceSetDecode(Rewr(instr->decode())); // rewrite updates - for (size_t s = 0; s < m->state_num(); s++) { - auto new_update = Rewr(instr->update(m->state(s))); - if (new_update) { - instr->ForceAddUpdate(m->state(s)->name().str(), new_update); - } + for (const auto& state : instr->updated_states()) { + instr->ForceAddUpdate(state, Rewr(instr->update(state))); } } // traverse the ILA hierarchy for (size_t c = 0; c < m->child_num(); c++) { - PassRewriteGeneric(m->child(c), Rewr); + RewriteGeneric(m->child(c), Rewr); } return true; } -}; // namespace ilang +} // namespace pass + +} // namespace ilang diff --git a/src/ila-mngr/p_rewrite_store_load.cc b/src/ila-mngr/p_rewrite_store_load.cc index 6609a82ab..d5865557f 100644 --- a/src/ila-mngr/p_rewrite_store_load.cc +++ b/src/ila-mngr/p_rewrite_store_load.cc @@ -9,31 +9,7 @@ namespace ilang { -#if 0 -class FuncObjStoreStore { -public: - inline const ExprPtrVec& addr() const { return addr_; } - inline const ExprPtrVec& data() const { return data_; } - - bool pre(const ExprPtr e) { - // ILA_ASSERT(GetUidExprOp(e) == AST_UID_EXPR_OP::LOAD); - // can be load from store/var/const/ite - - addr_.push_back(e->arg(1)); - data_.push_back(e->arg(2)); - - // return true if is store to store - return e->arg(0)->is_op(); - } - - void post(const ExprPtr e) {} - -private: - ExprPtrVec addr_; - ExprPtrVec data_; - -}; // class FuncObjStoreStore -#endif +namespace pass { class FuncObjRewrStoreLoad : public FuncObjRewrExpr { public: @@ -97,8 +73,9 @@ class FuncObjRewrStoreLoad : public FuncObjRewrExpr { }; // class FuncObjRewrStoreLoad -bool PassRewriteStoreLoad(const InstrLvlAbsPtr& m) { +bool RewriteStoreLoad(const InstrLvlAbsPtr& m) { ILA_NOT_NULL(m); + ILA_INFO << "Start pass: rewrite store-load pattern"; auto func = FuncObjRewrStoreLoad(); auto Rewr = [=, &func](const ExprPtr e) { @@ -109,7 +86,9 @@ bool PassRewriteStoreLoad(const InstrLvlAbsPtr& m) { return e; }; - return PassRewriteGeneric(m, Rewr); + return RewriteGeneric(m, Rewr); } -}; // namespace ilang +} // namespace pass + +} // namespace ilang diff --git a/src/ila-mngr/p_simplify_instr_update.cc b/src/ila-mngr/p_simplify_semantic.cc similarity index 69% rename from src/ila-mngr/p_simplify_instr_update.cc rename to src/ila-mngr/p_simplify_semantic.cc index e0f1504cd..7f07a5715 100644 --- a/src/ila-mngr/p_simplify_instr_update.cc +++ b/src/ila-mngr/p_simplify_semantic.cc @@ -8,29 +8,7 @@ namespace ilang { -bool SimplifyInstrUpdateTemplate( - const InstrLvlAbsPtr& m, - std::function Simp) { - ILA_NOT_NULL(m); - - // for each instruction - for (size_t i = 0; i < m->instr_num(); i++) { - // for each state - for (size_t s = 0; s < m->state_num(); s++) { - auto state_var = m->state(s); - auto new_update = Simp(m->instr(i)->update(state_var), m->instr(i)); - if (new_update) { - m->instr(i)->ForceAddUpdate(state_var->name().str(), new_update); - } - } - } - - for (size_t c = 0; c < m->child_num(); c++) { - SimplifyInstrUpdateTemplate(m->child(c), Simp); - } - - return true; -} +namespace pass { class FuncObjEqSubtree { public: @@ -50,7 +28,7 @@ class FuncObjEqSubtree { void post(const ExprPtr e) { auto dst = Rewrite(e); - rule_.insert({e, dst}).second; + rule_.insert({e, dst}); } private: @@ -92,8 +70,9 @@ class FuncObjEqSubtree { }; // class FuncObjSimpInstrUpdateRedundant -bool PassSimplifyInstrUpdate(const InstrLvlAbsPtr& m, const int& timeout) { +bool SimplifySemantic(const InstrLvlAbsCnstPtr& m, const int& timeout) { ILA_NOT_NULL(m); + ILA_INFO << "Start pass: semantic simplification"; // pattern - equivalent sub-tree modulo valid and decode auto SimpEqSubtree = [=](const ExprPtr e, const InstrPtr i) { @@ -111,7 +90,7 @@ bool PassSimplifyInstrUpdate(const InstrLvlAbsPtr& m, const int& timeout) { auto new_update = func.get(e); if (new_update != e) { - ILA_DLOG("PassSimpInstrUpdate") << "Equivalent sub-tree of " << i; + ILA_DLOG("PassSimpSemantic") << "Equivalent sub-tree of " << i; } return new_update; }; @@ -119,10 +98,33 @@ bool PassSimplifyInstrUpdate(const InstrLvlAbsPtr& m, const int& timeout) { if (timeout > 0) { z3::set_param("timeout", timeout); } - auto res = SimplifyInstrUpdateTemplate(m, SimpEqSubtree); + + auto visiter = [&SimpEqSubtree](const InstrLvlAbsCnstPtr& current) { + try { + // only simplify instructions + for (size_t i = 0; i < current->instr_num(); i++) { + auto instr = current->instr(i); + // decode + ILA_NOT_NULL(instr->decode()); + instr->ForceSetDecode(SimpEqSubtree(instr->decode(), instr)); + // state updates + for (const auto& state : instr->updated_states()) { + instr->ForceAddUpdate(state, + SimpEqSubtree(instr->update(state), instr)); + } + } + } catch (...) { + ILA_ERROR << "Fail simplify " << current; + } + }; + + m->DepthFirstVisit(visiter); + z3::reset_params(); - return res; + return true; } -}; // namespace ilang +} // namespace pass + +} // namespace ilang diff --git a/src/ila-mngr/p_simplify_syntactic.cc b/src/ila-mngr/p_simplify_syntactic.cc index a452b36e4..b4f8d5ea5 100644 --- a/src/ila-mngr/p_simplify_syntactic.cc +++ b/src/ila-mngr/p_simplify_syntactic.cc @@ -10,31 +10,17 @@ namespace ilang { namespace pass { -bool SimplifySyntactic(const InstrLvlAbsCnstPtr& m) { +bool SimplifySyntactic(const InstrLvlAbsPtr& m) { ILA_NOT_NULL(m); + ILA_INFO << "Start pass: syntactic simplification"; auto mngr = ExprMngr::New(); - auto visiter = [&mngr](const InstrLvlAbsCnstPtr& current) { - try { - // only simplify instructions - for (size_t i = 0; i < current->instr_num(); i++) { - auto instr = current->instr(i); - // decode - ILA_NOT_NULL(instr->decode()); - instr->ForceSetDecode(mngr->GetRep(instr->decode())); - // state updates - auto updated_states = instr->updated_states(); - for (const auto& state : updated_states) { - instr->ForceAddUpdate(state, mngr->GetRep(instr->update(state))); - } - } - } catch (...) { - ILA_ERROR << "Fail simplify " << current; - } - }; - - m->DepthFirstVisit(visiter); - return true; + auto Rewr = [&mngr](const ExprPtr& expr) { return mngr->GetRep(expr); }; + try { + return RewriteGeneric(m, Rewr); + } catch (...) { + return false; + } } } // namespace pass diff --git a/src/ila-mngr/u_abs_knob.cc b/src/ila-mngr/u_abs_knob.cc index 8db777163..d64cbaabb 100644 --- a/src/ila-mngr/u_abs_knob.cc +++ b/src/ila-mngr/u_abs_knob.cc @@ -217,13 +217,10 @@ void RewriteInstr(const InstrCnstPtr src, const InstrPtr dst, dst->set_decode(d_dst); // update - auto updated_states = src->updated_states(); - for (auto& state_name : updated_states) { - auto update_src = src->update(state_name); - if (update_src) { - auto update_dst = Rewrite(update_src, expr_map); - dst->set_update(state_name, update_dst); - } + for (const auto& state : src->updated_states()) { + auto update_src = src->update(state); + auto update_dst = Rewrite(update_src, expr_map); + dst->set_update(state, update_dst); } } diff --git a/src/ila-mngr/u_rewrite_expr.cc b/src/ila-mngr/u_rewrite_expr.cc index 14ace19e6..bdfcb34d5 100644 --- a/src/ila-mngr/u_rewrite_expr.cc +++ b/src/ila-mngr/u_rewrite_expr.cc @@ -11,26 +11,26 @@ namespace ilang { using namespace ExprFuse; -ExprPtr FuncObjRewrExpr::get(const ExprPtr e) const { +ExprPtr FuncObjRewrExpr::get(const ExprPtr& e) const { auto pos = rule_.find(e); ILA_CHECK(pos != rule_.end()) << e << " not found"; return pos->second; } -bool FuncObjRewrExpr::pre(const ExprPtr e) const { +bool FuncObjRewrExpr::pre(const ExprPtr& e) const { // check rewriting rule to see if defined/visited auto pos = rule_.find(e); return pos != rule_.end(); // if found --> break } -void FuncObjRewrExpr::post(const ExprPtr e) { +void FuncObjRewrExpr::post(const ExprPtr& e) { auto dst = Rewrite(e); - auto ok = rule_.insert({e, dst}).second; + auto [it, ok] = rule_.emplace(e, dst); // must not be defined, otherwise, there is a cycle. ILA_ASSERT(ok) << "Rewriting rule redefined (exist cycle in the AST)"; } -ExprPtr FuncObjRewrExpr::Rewrite(const ExprPtr e) const { +ExprPtr FuncObjRewrExpr::Rewrite(const ExprPtr& e) const { if (e->is_var() || e->is_const()) { return e; } else { @@ -39,7 +39,7 @@ ExprPtr FuncObjRewrExpr::Rewrite(const ExprPtr e) const { } } -ExprPtr FuncObjRewrExpr::RewriteOp(const ExprPtr e) const { +ExprPtr FuncObjRewrExpr::RewriteOp(const ExprPtr& e) const { switch (auto expr_op_uid = GetUidExprOp(e); expr_op_uid) { case AST_UID_EXPR_OP::NEG: { auto a = get(e->arg(0)); diff --git a/src/ila-mngr/u_rewrite_ila.cc b/src/ila-mngr/u_rewrite_ila.cc index 82587d77e..6afbb9352 100644 --- a/src/ila-mngr/u_rewrite_ila.cc +++ b/src/ila-mngr/u_rewrite_ila.cc @@ -12,13 +12,13 @@ namespace ilang { -InstrLvlAbsPtr FuncObjRewrIla::get(const InstrLvlAbsCnstPtr m) const { +InstrLvlAbsPtr FuncObjRewrIla::get(const InstrLvlAbsCnstPtr& m) const { auto pos = ila_map_.find(m); ILA_CHECK(pos != ila_map_.end()) << m << " not found"; return pos->second; } -bool FuncObjRewrIla::pre(const InstrLvlAbsCnstPtr src) { +bool FuncObjRewrIla::pre(const InstrLvlAbsCnstPtr& src) { auto pos = ila_map_.find(src); ILA_ASSERT(pos != ila_map_.end()) << "ILA dst for " << src << " not found."; auto dst = pos->second; @@ -58,7 +58,7 @@ bool FuncObjRewrIla::pre(const InstrLvlAbsCnstPtr src) { return false; } -void FuncObjRewrIla::post(const InstrLvlAbsCnstPtr src) const { +void FuncObjRewrIla::post(const InstrLvlAbsCnstPtr& src) const { // nothing } @@ -71,7 +71,7 @@ FuncObjFlatIla::FuncObjFlatIla(const InstrLvlAbsCnstPtr& top_, #endif // VALID_STACK } -bool FuncObjFlatIla::pre(const InstrLvlAbsCnstPtr src) { +bool FuncObjFlatIla::pre(const InstrLvlAbsCnstPtr& src) { if (src == top_ila_) return false; // skip the top level ila, do nothing auto pos = ila_map_.find(src); @@ -105,7 +105,7 @@ bool FuncObjFlatIla::pre(const InstrLvlAbsCnstPtr src) { return false; } -void FuncObjFlatIla::post(const InstrLvlAbsCnstPtr src) { +void FuncObjFlatIla::post(const InstrLvlAbsCnstPtr& src) { // pop the stack #ifdef VALID_STACK valid_cond_stack_.pop(); diff --git a/src/ila/hash_ast.cc b/src/ila/hash_ast.cc index b7797811b..00933f4fe 100644 --- a/src/ila/hash_ast.cc +++ b/src/ila/hash_ast.cc @@ -88,10 +88,14 @@ std::string ExprMngr::Hash(const ExprPtr& expr) { fmt::arg("value", value)); } else { ILA_ASSERT(expr->is_op()); + std::vector arg_list; for (size_t i = 0; i < expr->arg_num(); i++) { arg_list.push_back(expr->arg(i)->name().id()); } + if (auto app_func = std::dynamic_pointer_cast(expr)) { + arg_list.push_back(app_func->func()->name().id()); + } std::vector param_list; for (size_t i = 0; i < expr->param_num(); i++) { diff --git a/src/ilang++.cc b/src/ilang++.cc index 77e112a8e..a9978adf3 100644 --- a/src/ilang++.cc +++ b/src/ilang++.cc @@ -740,9 +740,9 @@ void ImportChildSynthAbstraction(const std::string& file_name, Ila& parent, #endif } -void ExportSysCSim(const Ila& ila, const std::string& dir_path) { +void ExportSysCSim(const Ila& ila, const std::string& dir_path, bool opt) { auto ilator = Ilator(ila.get()); - ilator.Generate(dir_path); + ilator.Generate(dir_path, opt); } IlaZ3Unroller::IlaZ3Unroller(z3::context& ctx, const std::string& suff) diff --git a/src/target-sc/ilator.cc b/src/target-sc/ilator.cc index deefce3cf..b691f8444 100644 --- a/src/target-sc/ilator.cc +++ b/src/target-sc/ilator.cc @@ -69,9 +69,9 @@ Ilator::Ilator(const InstrLvlAbsPtr& m) : m_(m) {} Ilator::~Ilator() { Reset(); } -void Ilator::Generate(const std::string& dst) { +void Ilator::Generate(const std::string& dst, bool opt) { // sanity checks and initialize - if (!SanityCheck() || !Bootstrap(dst)) { + if (!SanityCheck() || !Bootstrap(dst, opt)) { return; } @@ -142,12 +142,15 @@ bool Ilator::SanityCheck() const { return true; } -bool Ilator::Bootstrap(const std::string& root) { +bool Ilator::Bootstrap(const std::string& root, bool opt) { Reset(); auto status = true; // light-weight preprocessing - status &= PassRewriteConditionalStore(m_); + if (opt) { + status &= pass::SimplifySyntactic(m_); + status &= pass::RewriteConditionalStore(m_); + } // create/structure project directory status &= os_portable_mkdir(root); @@ -165,7 +168,7 @@ bool Ilator::Bootstrap(const std::string& root) { bool Ilator::GenerateInstrContent(const InstrPtr& instr, const std::string& dir) { - fmt::memory_buffer buff; + StrBuff buff; ExprVarMap lut; // include headers @@ -188,8 +191,18 @@ bool Ilator::GenerateInstrContent(const InstrPtr& instr, auto update_func = RegisterFunction(GetUpdateFuncName(instr)); BeginFuncDef(update_func, buff); lut.clear(); + std::set visited; auto updated_states = instr->updated_states(); - for (auto& s : updated_states) { + for (const auto& s : updated_states) { + // check if visited + auto update_expr = instr->update(s); + if (auto pos = visited.find(update_expr); pos == visited.end()) { + visited.insert(update_expr); + } else { + continue; + } + + // create placeholder if (auto update_expr = instr->update(s); !update_expr->is_mem()) { if (!RenderExpr(update_expr, buff, lut)) { return false; @@ -211,7 +224,7 @@ bool Ilator::GenerateInstrContent(const InstrPtr& instr, fmt::arg("mem_update_func", mem_update_func->name), fmt::arg("placeholder", placeholder)); // dummy traverse collect related memory operation - fmt::memory_buffer dummy_buff; + StrBuff dummy_buff; ExprVarMap dummy_lut; if (!RenderExpr(update_expr, dummy_buff, dummy_lut)) { return false; @@ -247,7 +260,7 @@ bool Ilator::GenerateMemoryUpdate(const std::string& dir) { // helper for traversing memory updates class MemUpdateVisiter { public: - MemUpdateVisiter(Ilator* h, fmt::memory_buffer& b, ExprVarMap& l) + MemUpdateVisiter(Ilator* h, StrBuff& b, ExprVarMap& l) : host(h), buff_ref(b), lut_ref(l) {} bool pre(const ExprPtr& expr) { @@ -264,12 +277,11 @@ bool Ilator::GenerateMemoryUpdate(const std::string& dir) { void post(const ExprPtr& expr) { host->DfsExpr(expr, buff_ref, lut_ref); } Ilator* host; - fmt::memory_buffer& buff_ref; + StrBuff& buff_ref; ExprVarMap lut_ref; }; - auto RenderMemUpdate = [this](const ExprPtr e, fmt::memory_buffer& b, - ExprVarMap& l) { + auto RenderMemUpdate = [this](const ExprPtr e, StrBuff& b, ExprVarMap& l) { auto mem_visiter = MemUpdateVisiter(this, b, l); e->DepthFirstVisitPrePost(mem_visiter); }; @@ -280,7 +292,7 @@ bool Ilator::GenerateMemoryUpdate(const std::string& dir) { return fmt::format("memory_update_functions_{}.cc", file_cnt++); }; - fmt::memory_buffer buff; + StrBuff buff; auto StartNewFile = [this, &buff]() { buff.clear(); fmt::format_to(buff, "#include <{}.h>\n", GetProjectName()); @@ -326,7 +338,7 @@ bool Ilator::GenerateMemoryUpdate(const std::string& dir) { } bool Ilator::GenerateConstantMemory(const std::string& dir) { - fmt::memory_buffer buff; + StrBuff buff; fmt::format_to(buff, "#include <{}.h>\n", GetProjectName()); for (auto& mem : const_mems_) { @@ -395,7 +407,7 @@ bool Ilator::GenerateInitialSetup(const std::string& dir) { // gen file auto init_func = RegisterFunction("setup_initial_condition"); - fmt::memory_buffer buff; + StrBuff buff; fmt::format_to(buff, "#include <{}.h>\n", GetProjectName()); BeginFuncDef(init_func, buff); for (auto pair : init_values) { @@ -409,7 +421,7 @@ bool Ilator::GenerateInitialSetup(const std::string& dir) { } bool Ilator::GenerateExecuteKernel(const std::string& dir) { - fmt::memory_buffer buff; + StrBuff buff; fmt::format_to( // headers buff, @@ -491,7 +503,7 @@ bool Ilator::GenerateExecuteKernel(const std::string& dir) { } bool Ilator::GenerateGlobalHeader(const std::string& dir) { - fmt::memory_buffer buff; + StrBuff buff; fmt::format_to(buff, "#include \n" @@ -611,7 +623,7 @@ bool Ilator::GenerateBuildSupport(const std::string& dir) { fmt::arg("dir", dir_src), fmt::arg("file", f))); } - fmt::memory_buffer buff; + StrBuff buff; fmt::format_to(buff, cmake_recipe_template, fmt::arg("project", GetProjectName()), fmt::arg("dir_app", dir_app), @@ -641,12 +653,22 @@ bool Ilator::GenerateBuildSupport(const std::string& dir) { } bool Ilator::RenderExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { - auto ExprDfsVisiter = [this, &buff, &lut](const ExprPtr& e) { - DfsExpr(e, buff, lut); + + class ExprDfsVisiter { + public: + ExprDfsVisiter(Ilator* hi, StrBuff& bi, ExprVarMap& li) + : host(hi), b(bi), l(li) {} + bool pre(const ExprPtr& e) { return l.find(e) != l.end(); } + void post(const ExprPtr& e) { host->DfsExpr(e, b, l); } + + Ilator* host; + StrBuff& b; + ExprVarMap& l; }; try { - expr->DepthFirstVisit(ExprDfsVisiter); + auto visiter = ExprDfsVisiter(this, buff, lut); + expr->DepthFirstVisitPrePost(visiter); } catch (std::exception& err) { ILA_ERROR << err.what(); return false; diff --git a/test/t_ilator.cc b/test/t_ilator.cc index ff96ff537..ee5f72b1d 100644 --- a/test/t_ilator.cc +++ b/test/t_ilator.cc @@ -31,9 +31,14 @@ class TestIlator : public ::testing::Test { }; // TestIlator -TEST_F(TestIlator, IlaSimTest) { +TEST_F(TestIlator, Default) { IlaSimTest m; ExportSysCSim(m.model, out_dir); } +TEST_F(TestIlator, Optimize) { + IlaSimTest m; + ExportSysCSim(m.model, out_dir, true); +} + } // namespace ilang diff --git a/test/t_pass.cc b/test/t_pass.cc index 2e8020800..2ab4d48c7 100644 --- a/test/t_pass.cc +++ b/test/t_pass.cc @@ -14,7 +14,7 @@ void ApplyPass(const std::string& dir, const std::string& file, bool simplify = true) { // SetToStdErr(true); - EnableDebug("PassSimpInstrUpdate"); + EnableDebug("PassSimpSemantic"); EnableDebug("PassRewrCondStore"); EnableDebug("PassRewrStoreLoad"); EnableDebug("PassInferChildProgCFG"); @@ -25,13 +25,13 @@ void ApplyPass(const std::string& dir, const std::string& file, auto ila = ImportIlaPortable(ila_file).get(); pass::SimplifySyntactic(ila); - PassSimplifyInstrUpdate(ila); + pass::SimplifySemantic(ila); - PassRewriteConditionalStore(ila); - PassRewriteStoreLoad(ila); + pass::RewriteConditionalStore(ila); + pass::RewriteStoreLoad(ila); - PassInferChildProgCFG(ila); - PassMapChildProgEntryPoint(ila); + pass::InferChildProgCFG(ila); + pass::MapChildProgEntryPoint(ila); auto out_file = "opt_" + file; ExportIlaPortable(Ila(ila), out_file); From a6cfc7d867d85aae288620594f900901271f073c Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 13 Jul 2020 16:48:12 -0400 Subject: [PATCH 24/30] New top-level API for executing passes --- include/ilang/ilang++.h | 12 ++++++++++++ src/ilang++.cc | 26 ++++++++++++++++++++++++++ test/t_pass.cc | 26 +++++++++++++++----------- test/unit-include/util.h | 2 +- test/unit-src/util.cc | 9 ++++++--- 5 files changed, 60 insertions(+), 15 deletions(-) diff --git a/include/ilang/ilang++.h b/include/ilang/ilang++.h index 7e9db9a4d..377822e3a 100644 --- a/include/ilang/ilang++.h +++ b/include/ilang/ilang++.h @@ -580,6 +580,18 @@ class Ila { /// top-level parent instructions. void FlattenHierarchy(); + /// \brief Supported pass ID. + typedef enum PassID { + SIMPLIFY_SYNTACTIC = 0, + SIMPLIFY_SEMANTIC, + REWRITE_CONDITIONAL_STORE, + REWRITE_LOAD_FROM_STORE + } PassID; + + /// \brief Execute the specified passes in order. + /// \param[in] passes the list of passes to execute. + bool ExecutePass(const std::vector& passes) const; + }; // class Ila /******************************************************************************/ diff --git a/src/ilang++.cc b/src/ilang++.cc index a9978adf3..367c73115 100644 --- a/src/ilang++.cc +++ b/src/ilang++.cc @@ -4,6 +4,7 @@ #include #include +#include #include #include #include @@ -694,6 +695,31 @@ void Ila::ExportToVerilog(std::ostream& fout) const { void Ila::FlattenHierarchy() { AbsKnob::FlattenIla(ptr_); } +bool Ila::ExecutePass(const std::vector& passes) const { + auto status = true; + for (const auto& id : passes) { + switch (id) { + case PassID::SIMPLIFY_SYNTACTIC: { + status &= pass::SimplifySyntactic(ptr_); + break; + } + case PassID::SIMPLIFY_SEMANTIC: { + status &= pass::SimplifySemantic(ptr_); + break; + } + case PassID::REWRITE_CONDITIONAL_STORE: { + status &= pass::RewriteConditionalStore(ptr_); + break; + } + case PassID::REWRITE_LOAD_FROM_STORE: { + status &= pass::RewriteStoreLoad(ptr_); + break; + } + }; + } + return status; +} + std::ostream& operator<<(std::ostream& out, const ExprRef& expr) { return out << expr.get(); } diff --git a/test/t_pass.cc b/test/t_pass.cc index 2ab4d48c7..63b9f84ef 100644 --- a/test/t_pass.cc +++ b/test/t_pass.cc @@ -12,8 +12,6 @@ namespace ilang { void ApplyPass(const std::string& dir, const std::string& file, bool simplify = true) { - // SetToStdErr(true); - EnableDebug("PassSimpSemantic"); EnableDebug("PassRewrCondStore"); EnableDebug("PassRewrStoreLoad"); @@ -22,19 +20,25 @@ void ApplyPass(const std::string& dir, const std::string& file, auto file_dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, dir); auto ila_file = os_portable_append_dir(file_dir, file); - auto ila = ImportIlaPortable(ila_file).get(); + auto ila = ImportIlaPortable(ila_file); - pass::SimplifySyntactic(ila); - pass::SimplifySemantic(ila); + ila.ExecutePass({Ila::PassID::SIMPLIFY_SYNTACTIC, + Ila::PassID::SIMPLIFY_SEMANTIC, + Ila::PassID::REWRITE_CONDITIONAL_STORE, + Ila::PassID::REWRITE_LOAD_FROM_STORE}); - pass::RewriteConditionalStore(ila); - pass::RewriteStoreLoad(ila); + pass::InferChildProgCFG(ila.get()); + pass::MapChildProgEntryPoint(ila.get()); - pass::InferChildProgCFG(ila); - pass::MapChildProgEntryPoint(ila); + auto out_file = GetRandomFileName(); + ExportIlaPortable(ila, out_file); + os_portable_remove_file(out_file); - auto out_file = "opt_" + file; - ExportIlaPortable(Ila(ila), out_file); + DisableDebug("PassSimpSemantic"); + DisableDebug("PassRewrCondStore"); + DisableDebug("PassRewrStoreLoad"); + DisableDebug("PassInferChildProgCFG"); + DisableDebug("PassMapChildProgEntry"); } TEST(TestPass, AES) { ApplyPass("aes", "aes.json"); } diff --git a/test/unit-include/util.h b/test/unit-include/util.h index 4b9ef7047..442211a7b 100644 --- a/test/unit-include/util.h +++ b/test/unit-include/util.h @@ -46,7 +46,7 @@ void EndRecordLog(); cmd; \ msg = ::testing::internal::GetCapturedStderr(); -std::string GetRandomFileName(const std::string& dir); +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 543d4a111..0d8c1a05f 100644 --- a/test/unit-src/util.cc +++ b/test/unit-src/util.cc @@ -28,13 +28,16 @@ std::string random_string(std::size_t length) { } std::string GetRandomFileName(const std::string& dir) { - ILA_ASSERT(fs::is_directory(dir)) << dir << " doesn't exist"; + auto root = fs::path(dir); + if (dir.empty() || !fs::is_directory(dir)) { + root = fs::temp_directory_path(); + } auto file_name = fs::path(random_string(6)); - while (fs::exists(fs::path(dir) / file_name)) { + while (fs::exists(root / file_name)) { file_name = fs::path(random_string(6)); } - return (dir / file_name).string(); + return (root / file_name).string(); } void CheckIlaEqLegacy(const InstrLvlAbsPtr& a, const InstrLvlAbsPtr& b) { From 02e32cb4d2dd3a6b5ca52a91817a4efd88e2b722 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 13 Jul 2020 17:53:08 -0400 Subject: [PATCH 25/30] Test untested functions and clean up --- include/ilang/ilang++.h | 2 + src/ilang++.cc | 26 +----------- src/vtarget-out/vtarget_gen_yosys.cc | 46 +++++++++++----------- test/t_api.cc | 59 +++++++++++++++++++++++++++- test/t_unroll_seq.cc | 4 +- test/t_vtarget_gen.cc | 33 ---------------- 6 files changed, 87 insertions(+), 83 deletions(-) diff --git a/include/ilang/ilang++.h b/include/ilang/ilang++.h index 377822e3a..3554657cd 100644 --- a/include/ilang/ilang++.h +++ b/include/ilang/ilang++.h @@ -616,6 +616,7 @@ bool ExportIlaPortable(const Ila& ila, const std::string& file_name); /// \param[in] file_name the name of the ILA portable (JSON) file to import. Ila ImportIlaPortable(const std::string& file_name); +#ifdef SYNTH_INTERFACE /// \brief Import the synthesized abstraction from file. /// \param[in] file_name the name of the synthesized abstraction (.ila) file. /// \param[in] ila_name the name of the generated ILA. @@ -629,6 +630,7 @@ Ila ImportSynthAbstraction(const std::string& file_name, /// \param[in] ila_name the name pf the generated child-ILA. void ImportChildSynthAbstraction(const std::string& file_name, Ila& parent, const std::string& ila_name); +#endif // SYNTH_INTERFACE /// \brief Generate the SystemC simulator. /// \param [in] ila the top-level ILA to generate. diff --git a/src/ilang++.cc b/src/ilang++.cc index 367c73115..8aa5dc03f 100644 --- a/src/ilang++.cc +++ b/src/ilang++.cc @@ -741,30 +741,20 @@ Ila ImportIlaPortable(const std::string& file_name) { return Ila(m); } +#ifdef SYNTH_INTERFACE Ila ImportSynthAbstraction(const std::string& file_name, const std::string& ila_name) { -#ifdef SYNTH_INTERFACE auto m = ImportSynthAbsFromFile(file_name, ila_name); return Ila(m); -#else // SYNTH_INTERFACE - auto m = Ila(ila_name); - ILA_ERROR << "Synthesis interface not built."; - ILA_ERROR << "Empty ILA " << ila_name << " is returned."; - return m; -#endif // SYNTH_INTERFACE } void ImportChildSynthAbstraction(const std::string& file_name, Ila& parent, const std::string& ila_name) { -#ifdef SYNTH_INTERFACE auto m = ImportSynthAbsFromFileHier(file_name, parent.get(), ila_name); ILA_NOT_NULL(m); return; -#else - ILA_ERROR << "Synthesis interface not built."; - ILA_ERROR << "Empty ILA " << ila_name << " is returned."; -#endif } +#endif // SYNTH_INTERFACE void ExportSysCSim(const Ila& ila, const std::string& dir_path, bool opt) { auto ilator = Ilator(ila.get()); @@ -778,18 +768,6 @@ IlaZ3Unroller::IlaZ3Unroller(z3::context& ctx, const std::string& suff) IlaZ3Unroller::~IlaZ3Unroller() {} -#if 0 -void IlaZ3Unroller::SetExtraSuffix(const std::string& suff) { - extra_suff_ = suff; - univ_->SetExtraSuffix(suff); -} - -void IlaZ3Unroller::ResetExtraSuffix() { - extra_suff_ = ""; - univ_->ResetExtraSuffix(); -} -#endif - z3::expr IlaZ3Unroller::UnrollMonoConn(const Ila& top, const int& k, const int& init) { auto u = std::make_shared(ctx_, extra_suff_); diff --git a/src/vtarget-out/vtarget_gen_yosys.cc b/src/vtarget-out/vtarget_gen_yosys.cc index 5a6d74b6a..0426fce00 100644 --- a/src/vtarget-out/vtarget_gen_yosys.cc +++ b/src/vtarget-out/vtarget_gen_yosys.cc @@ -2,15 +2,17 @@ /// the inv-syn related HC generation is located in inv_syn.cc // --- Hongce Zhang +#include + #include #include +#include + #include #include #include #include #include -#include -#include namespace ilang { @@ -242,51 +244,51 @@ VlgSglTgtGen_Yosys::VlgSglTgtGen_Yosys( ILA_CHECK(chc_target == _chc_target_t::GENERAL_PROPERTY); ILA_CHECK(target_tp == target_type_t::INVARIANTS || - target_tp == target_type_t::INSTRUCTIONS) + target_tp == target_type_t::INSTRUCTIONS) << "Unknown target type: " << target_tp; ILA_CHECK((vbackend & backend_selector::YOSYS) == backend_selector::YOSYS) << "Must use Yosys as vbackend"; ILA_CHECK(s_backend == synthesis_backend_selector::ABC || - s_backend == synthesis_backend_selector::Z3 || - s_backend == synthesis_backend_selector::GRAIN || - s_backend == synthesis_backend_selector::ELDERICA || - s_backend == synthesis_backend_selector::NOSYN); + s_backend == synthesis_backend_selector::Z3 || + s_backend == synthesis_backend_selector::GRAIN || + s_backend == synthesis_backend_selector::ELDERICA || + s_backend == synthesis_backend_selector::NOSYN); ILA_CHECK(IMPLY(s_backend == synthesis_backend_selector::GRAIN, - vtg_config.YosysSmtFlattenDatatype && - vtg_config.YosysSmtFlattenHierarchy)) + vtg_config.YosysSmtFlattenDatatype && + vtg_config.YosysSmtFlattenHierarchy)) << "Grain requires not to flatten hierarchy/datatype"; ILA_CHECK(IMPLY(s_backend == synthesis_backend_selector::ABC, - _vtg_config.AbcUseAiger)) + _vtg_config.AbcUseAiger)) << "Currently only support using AIGER"; ILA_CHECK(IMPLY(s_backend == synthesis_backend_selector::ABC, - vtg_config.YosysSmtFlattenHierarchy)) + vtg_config.YosysSmtFlattenHierarchy)) << "ABC requires to flatten hierarchy"; // This is hard-coded in the Yosys script // if not flattened, abc will be unhappy ILA_CHECK(IMPLY(s_backend == synthesis_backend_selector::ABC, - vbackend == backend_selector::ABCPDR)); + vbackend == backend_selector::ABCPDR)); ILA_CHECK(IMPLY(s_backend == synthesis_backend_selector::GRAIN, - vbackend == backend_selector::GRAIN_SYGUS && - _vtg_config.YosysSmtStateSort == _vtg_config.Datatypes)); + vbackend == backend_selector::GRAIN_SYGUS && + _vtg_config.YosysSmtStateSort == _vtg_config.Datatypes)); ILA_CHECK(IMPLY(s_backend == synthesis_backend_selector::Z3, - vbackend == backend_selector::Z3PDR)); + vbackend == backend_selector::Z3PDR)); ILA_CHECK(IMPLY(vbackend == backend_selector::BTOR_GENERIC, - s_backend == synthesis_backend_selector::NOSYN)); + s_backend == synthesis_backend_selector::NOSYN)); ILA_CHECK(s_backend != synthesis_backend_selector::ELDERICA) << "Bug : not implemented yet!"; ILA_CHECK(!(_vtg_config.YosysSmtFlattenDatatype && - _vtg_config.YosysSmtStateSort != _vtg_config.Datatypes)) + _vtg_config.YosysSmtStateSort != _vtg_config.Datatypes)) << "Must use Datatypes to encode state in order to flatten"; } // VlgSglTgtGen_Yosys @@ -571,10 +573,10 @@ void VlgSglTgtGen_Yosys::Export_script(const std::string& script_name) { ILA_CHECK(false) << "Not implemented."; } else if (s_backend == synthesis_backend_selector::NOSYN) { if (!_vtg_config.BtorGenericCmdline.empty()) { - runnable = ReplaceAll(_vtg_config.BtorGenericCmdline, "%btorfile%", prob_fname); + runnable = + ReplaceAll(_vtg_config.BtorGenericCmdline, "%btorfile%", prob_fname); options = ""; - } - else{ + } else { runnable = "echo"; options = " \"btor file is available as: " + prob_fname + "\""; } @@ -595,7 +597,7 @@ void VlgSglTgtGen_Yosys::Export_script(const std::string& script_name) { std::shared_ptr VlgSglTgtGen_Yosys::GetDesignSmtInfo() const { ILA_CHECK((_backend & backend_selector::CHC) == backend_selector::CHC && - _vtg_config.YosysSmtStateSort == _vtg_config.Datatypes) + _vtg_config.YosysSmtStateSort == _vtg_config.Datatypes) << "Only CHC target with datatypes will generate suitable smt-lib2."; ILA_CHECK(design_smt_info != nullptr); return design_smt_info; @@ -738,7 +740,7 @@ void VlgSglTgtGen_Yosys::design_only_gen_smt( write_smt2_options += "-stbv "; else ILA_CHECK(false) << "Unsupported smt state sort encoding:" - << _vtg_config.YosysSmtStateSort; + << _vtg_config.YosysSmtStateSort; ys_script_fout << "read_verilog -sv " << os_portable_append_dir(_output_path, top_file_name) diff --git a/test/t_api.cc b/test/t_api.cc index 5b8aa43b5..056c19b78 100644 --- a/test/t_api.cc +++ b/test/t_api.cc @@ -1,12 +1,15 @@ /// \file /// Unit test for c++ API +#include + +#include +#include + #include "unit-include/config.h" #include "unit-include/eq_ilas.h" #include "unit-include/simple_cpu.h" #include "unit-include/util.h" -#include -#include #define REG_NUM 16 #define REG_SIZE 8 @@ -325,6 +328,58 @@ TEST(TestApi, EntryNum) { #endif } +TEST(TestApi, OutStream) { + auto m = SimpleCpuRef("m"); + std::string msg = ""; + + // ila + GET_STDOUT_MSG((std::cout << m), msg); + EXPECT_TRUE(msg.find(m.name()) != std::string::npos); + + // state + for (size_t i = 0; i < m.state_num(); i++) { + auto state = m.state(i); + GET_STDOUT_MSG((std::cout << state), msg); + EXPECT_TRUE(msg.find(state.name()) != std::string::npos); + } + + // instr + for (size_t i = 0; i < m.instr_num(); i++) { + auto instr = m.instr(i); + GET_STDOUT_MSG((std::cout << instr), msg); + EXPECT_TRUE(msg.find(instr.name()) != std::string::npos); + } +} + +TEST(TestApi, VerilogGen) { + auto tmp_dir = GetRandomFileName(); + os_portable_mkdir(tmp_dir); + + // ila + auto m = SimpleCpuRef("m"); + auto tmp_file_ila = GetRandomFileName(tmp_dir); + std::ofstream fout(tmp_file_ila); + m.ExportToVerilog(fout); + fout.close(); + + // instr + for (size_t i = 0; i < m.instr_num(); i++) { + auto instr = m.instr(i); + + auto tmp_file_instr = GetRandomFileName(tmp_dir); + fout.open(tmp_file_instr); + instr.ExportToVerilog(fout); + fout.close(); + + auto tmp_file_instr_child = GetRandomFileName(tmp_dir); + fout.open(tmp_file_instr_child); + instr.ExportToVerilogWithChild(fout); + fout.close(); + } + + os_portable_remove_directory(tmp_dir); +} + TEST(TestApi, Unroll) { z3::context c; auto unroller = IlaZ3Unroller(c); diff --git a/test/t_unroll_seq.cc b/test/t_unroll_seq.cc index aa2173a2f..030cdc0ed 100644 --- a/test/t_unroll_seq.cc +++ b/test/t_unroll_seq.cc @@ -36,7 +36,7 @@ class TestUnroll : public ::testing::Test { }; // class TestUnroll -TEST_F(TestUnroll, InsteSeqFlatSubs) { +TEST_F(TestUnroll, InstrSeqFlatSubs) { auto m = ila_gen_.GetIlaFlat1(); std::vector seq; @@ -48,7 +48,7 @@ TEST_F(TestUnroll, InsteSeqFlatSubs) { auto cstr = unroller->PathSubs(seq); } -TEST_F(TestUnroll, InsteSeqFlatAssn) { +TEST_F(TestUnroll, InstrSeqFlatAssn) { auto m = ila_gen_.GetIlaFlat1(); std::vector seq; diff --git a/test/t_vtarget_gen.cc b/test/t_vtarget_gen.cc index 7ea3cb1fa..a0ed39d58 100644 --- a/test/t_vtarget_gen.cc +++ b/test/t_vtarget_gen.cc @@ -15,39 +15,6 @@ namespace ilang { typedef std::vector P; -TEST(TestVlgTargetGen, AesIlaInfo) { - auto aes_dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, "aes"); - auto aesFile = os_portable_append_dir(aes_dir, "aes_v_top.abst"); - auto aesuFile = os_portable_append_dir(aes_dir, "aes_v_child.abst"); - auto aes = ImportSynthAbstraction(aesFile, "AES").get(); - auto aesu = ImportSynthAbstraction(aesuFile, "AES_U").get(); - - // aes->AddChild(aesu); - - ILA_DLOG("TestVlgTargetGen.IlaInfo") << "No. instr:" << aes->instr_num(); - for (unsigned i = 0; i < aes->instr_num(); ++i) { - ILA_DLOG("TestVlgTargetGen.IlaInfo") << "\t" << aes->instr(i)->name().str() - << "\t" << aes->instr(i)->decode(); - } - ILA_DLOG("TestVlgTargetGen.IlaInfo") << "No. state:" << aes->state_num(); - for (unsigned i = 0; i < aes->state_num(); ++i) { - ILA_DLOG("TestVlgTargetGen.IlaInfo") << "\t" << aes->state(i)->name().str(); - } - ILA_DLOG("TestVlgTargetGen.IlaInfo") << std::endl; - - ILA_DLOG("TestVlgTargetGen.IlaInfo") << "No. instr:" << aesu->instr_num(); - for (unsigned i = 0; i < aes->instr_num(); ++i) { - ILA_DLOG("TestVlgTargetGen.IlaInfo") << "\t" << aesu->instr(i)->name().str() - << "\t" << aesu->instr(i)->decode(); - } - ILA_DLOG("TestVlgTargetGen.IlaInfo") << "No. state:" << aesu->state_num(); - for (unsigned i = 0; i < aesu->state_num(); ++i) { - ILA_DLOG("TestVlgTargetGen.IlaInfo") - << "\t" << aesu->state(i)->name().str(); - } - ILA_DLOG("TestVlgTargetGen.IlaInfo") << std::endl; -} - TEST(TestVlgTargetGen, PipeExample) { auto ila_model = SimplePipe::BuildModel(); From 994340ae441f3b45b59ace932eb457147778da3b Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 13 Jul 2020 17:57:43 -0400 Subject: [PATCH 26/30] Check pass correctness semantically --- test/t_pass.cc | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/test/t_pass.cc b/test/t_pass.cc index 63b9f84ef..4ef7c147a 100644 --- a/test/t_pass.cc +++ b/test/t_pass.cc @@ -30,9 +30,8 @@ void ApplyPass(const std::string& dir, const std::string& file, pass::InferChildProgCFG(ila.get()); pass::MapChildProgEntryPoint(ila.get()); - auto out_file = GetRandomFileName(); - ExportIlaPortable(ila, out_file); - os_portable_remove_file(out_file); + auto org = ImportIlaPortable(ila_file); + CheckIlaEqLegacy(org.get(), ila.get()); DisableDebug("PassSimpSemantic"); DisableDebug("PassRewrCondStore"); From 0e2a30646741070aa015ffb59d3c79a765c1a1fe Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 13 Jul 2020 18:00:23 -0400 Subject: [PATCH 27/30] Test top-level instr decode access --- test/t_api.cc | 3 +++ 1 file changed, 3 insertions(+) diff --git a/test/t_api.cc b/test/t_api.cc index 056c19b78..76c2d9f88 100644 --- a/test/t_api.cc +++ b/test/t_api.cc @@ -348,6 +348,9 @@ TEST(TestApi, OutStream) { auto instr = m.instr(i); GET_STDOUT_MSG((std::cout << instr), msg); EXPECT_TRUE(msg.find(instr.name()) != std::string::npos); + + GET_STDOUT_MSG((std::cout << instr.GetDecode()), msg); + EXPECT_FALSE(msg.empty()); } } From dc527225a1195c9f62f39d5f4fe642cd462d702e Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 13 Jul 2020 22:36:48 -0400 Subject: [PATCH 28/30] Test free unroller, uninterpreted function definition, and instr update access --- test/t_api.cc | 67 ++++++++++++++++++++++++++++++++ test/unit-include/ila_sim_test.h | 8 ++-- test/unit-src/ila_sim_test.cc | 20 ++++++---- 3 files changed, 83 insertions(+), 12 deletions(-) diff --git a/test/t_api.cc b/test/t_api.cc index 76c2d9f88..e2da6facf 100644 --- a/test/t_api.cc +++ b/test/t_api.cc @@ -8,6 +8,7 @@ #include "unit-include/config.h" #include "unit-include/eq_ilas.h" +#include "unit-include/ila_sim_test.h" #include "unit-include/simple_cpu.h" #include "unit-include/util.h" @@ -343,6 +344,8 @@ TEST(TestApi, OutStream) { EXPECT_TRUE(msg.find(state.name()) != std::string::npos); } + auto pc = m.state("pc"); + // instr for (size_t i = 0; i < m.instr_num(); i++) { auto instr = m.instr(i); @@ -351,6 +354,10 @@ TEST(TestApi, OutStream) { GET_STDOUT_MSG((std::cout << instr.GetDecode()), msg); EXPECT_FALSE(msg.empty()); + + auto next_pc = instr.GetUpdate(pc); + GET_STDOUT_MSG((std::cout << next_pc), msg); // not NULL + EXPECT_FALSE(msg.empty()); } } @@ -515,6 +522,66 @@ TEST(TestApi, Log) { #endif } +TEST(TestApi, UnrollPathFreeWithFunc) { + z3::context ctx; + z3::solver solver(ctx); + + auto unroller = IlaZ3Unroller(ctx); + auto m0 = IlaSimTest("m0").model; + auto m1 = IlaSimTest("m1").model; + + // start from saem state + auto same_state = BoolConst(true); + for (size_t i = 0; i < m0.state_num(); i++) { + auto state_0 = m0.state(i); + auto state_1 = m1.state(state_0.name()); + same_state = same_state & (state_0 == state_1); + } + unroller.AddInitPred(same_state); + + // always share same input + auto same_input = BoolConst(true); + for (size_t i = 0; i < m0.input_num(); i++) { + auto input_0 = m0.input(i); + auto input_1 = m1.input(input_0.name()); + same_input = same_input & (input_0 == input_1); + } + unroller.AddGlobPred(same_input); + + // unroll instr sequence + auto seq0 = {m0.instr("WRITE_ADDRESS"), m0.instr("START_ENCRYPT")}; + auto seq1 = {m1.instr("WRITE_ADDRESS"), m1.instr("START_ENCRYPT")}; + auto path0 = unroller.UnrollPathConn(seq0); + auto path1 = unroller.UnrollPathFree(seq1); + + auto connect = ctx.bool_val(true); + for (size_t i = 0; i < m1.state_num(); i++) { + auto state = m1.state(i); + connect = connect && + (unroller.NextState(state, 0) == unroller.CurrState(state, 1)) && + (unroller.NextState(state, 1) == unroller.CurrState(state, 2)); + } + + // func + auto farg = SortRef::BV(128); + auto func = unroller.GetZ3FuncDecl(FuncRef("process128", farg, farg, farg)); + auto x = ctx.bv_const("x", 128); + auto y = ctx.bv_const("y", 128); + auto fdef = z3::forall(x, y, func(x, y) == (x + y)); // dummy + + // check length + auto to_check = unroller.Equal(m0.state("length"), 2, m1.state("length"), 2); + + // SMT query + solver.add(path0); + solver.add(path1); + solver.add(fdef); + solver.add(!to_check); + EXPECT_EQ(solver.check(), z3::sat); + solver.add(connect); + EXPECT_EQ(solver.check(), z3::unsat); +} + TEST(TestApi, Portable) { // SetToStdErr(1); EnableDebug("Portable"); diff --git a/test/unit-include/ila_sim_test.h b/test/unit-include/ila_sim_test.h index a9e9153e6..c291bc7cb 100644 --- a/test/unit-include/ila_sim_test.h +++ b/test/unit-include/ila_sim_test.h @@ -25,16 +25,16 @@ using namespace ilang; class IlaSimTest { public: - IlaSimTest(); + IlaSimTest(const std::string& name = "TEST"); Ila model; protected: - static ExprRef slice_read(const ExprRef ®, const ExprRef &idx, + static ExprRef slice_read(const ExprRef& reg, const ExprRef& idx, unsigned long base_addr, unsigned no_slice, unsigned slice_width); - static ExprRef slice_update(const ExprRef ®, const ExprRef &idx, - const ExprRef &input_slice, + static ExprRef slice_update(const ExprRef& reg, const ExprRef& idx, + const ExprRef& input_slice, unsigned long base_addr, unsigned no_slice, unsigned slice_width); diff --git a/test/unit-src/ila_sim_test.cc b/test/unit-src/ila_sim_test.cc index 45db4591e..445add31e 100644 --- a/test/unit-src/ila_sim_test.cc +++ b/test/unit-src/ila_sim_test.cc @@ -1,8 +1,11 @@ -#include "../unit-include/ila_sim_test.h" -#include #include -IlaSimTest::IlaSimTest() - : model("TEST"), cmd(model.NewBvInput("cmd", 2)), + +#include + +#include "../unit-include/ila_sim_test.h" + +IlaSimTest::IlaSimTest(const std::string& name) + : model(name), cmd(model.NewBvInput("cmd", 2)), cmdaddr(model.NewBvInput("cmdaddr", 16)), cmddata(model.NewBvInput("cmddata", 8)), cmdflag(model.NewBoolInput("cmdflag")), flag(model.NewBoolState("flag")), @@ -29,10 +32,11 @@ IlaSimTest::IlaSimTest() (cmdaddr < ADDR + 2)); instr.SetUpdate( - address, Ite(is_status_idle, - Concat(Ite(cmdaddr == ADDR + 1, cmddata/cmddata, address(15, 8)), - Ite(cmdaddr == ADDR, cmddata * cmddata, address(7, 0))), - address)); + address, + Ite(is_status_idle, + Concat(Ite(cmdaddr == ADDR + 1, cmddata / cmddata, address(15, 8)), + Ite(cmdaddr == ADDR, cmddata * cmddata, address(7, 0))), + address)); instr.SetUpdate(flag, Ite(is_status_idle, flag_true, flag_false)); From 4e6af7e4411ea79cc2c4e480e0688fd0f7e770a1 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 13 Jul 2020 22:46:56 -0400 Subject: [PATCH 29/30] Remove legacy headers --- include/ilang/verification/abs_knob.h | 126 ---------- include/ilang/verification/eq_check_crr.h | 127 ---------- include/ilang/verification/legacy_bmc.h | 82 ------ include/ilang/verification/rewrite_expr.h | 43 ---- include/ilang/verification/rewrite_ila.h | 75 ------ include/ilang/verification/unroller.h | 289 ---------------------- 6 files changed, 742 deletions(-) delete mode 100644 include/ilang/verification/abs_knob.h delete mode 100644 include/ilang/verification/eq_check_crr.h delete mode 100644 include/ilang/verification/legacy_bmc.h delete mode 100644 include/ilang/verification/rewrite_expr.h delete mode 100644 include/ilang/verification/rewrite_ila.h delete mode 100644 include/ilang/verification/unroller.h diff --git a/include/ilang/verification/abs_knob.h b/include/ilang/verification/abs_knob.h deleted file mode 100644 index 5f2c50773..000000000 --- a/include/ilang/verification/abs_knob.h +++ /dev/null @@ -1,126 +0,0 @@ -/// \file -/// Header for a collection of ILA helpers. - -#ifndef ILANG_VERIFICATION_ABS_KNOB_H__ -#define ILANG_VERIFICATION_ABS_KNOB_H__ - -#include - -namespace ilang { - -class AbsKnob { -public: - /****************************************************************************/ - /// Add all dependent vars of the expr to the set. - static void InsertVar(const ExprPtr e, ExprSet& vars); - /// Get the set of all dependent vars of the expr. - static ExprSet GetVar(const ExprPtr e); - - /****************************************************************************/ - /// Add all state vars of the host (excluding child) to the set. - static void InsertStt(const InstrCnstPtr instrs, ExprSet& stts); - /// Add all state vars of the host (including child) to the set. - static void InsertSttTree(const InstrCnstPtr instrs, ExprSet& stts); - - /****************************************************************************/ - /// Add all vars of the ILA (excluding child) to the set. - static void InsertVar(const InstrLvlAbsCnstPtr m, ExprSet& vars); - /// Add all state vars of the ILA (excluding child) to the set. - static void InsertStt(const InstrLvlAbsCnstPtr m, ExprSet& stts); - /// Add all input vars of the ILA (excluding child) to the set. - static void InsertInp(const InstrLvlAbsCnstPtr m, ExprSet& inps); - /// Add all vars of the ILA (including child) to the set. - static void InsertVarTree(const InstrLvlAbsCnstPtr top, ExprSet& vars); - /// Add all state vars of the ILA (including child) to the set. - static void InsertSttTree(const InstrLvlAbsCnstPtr top, ExprSet& stts); - /// Add all input vars of the ILA (including child) to the set. - static void InsertInpTree(const InstrLvlAbsCnstPtr top, ExprSet& inps); - - /// Get the set of all vars of the ILA (excluding child). - static ExprSet GetVar(const InstrLvlAbsCnstPtr m); - /// Get the set of all state vars of the ILA (excluding child). - static ExprSet GetStt(const InstrLvlAbsCnstPtr m); - /// Get the set of all input vars of the ILA (excluding child). - static ExprSet GetInp(const InstrLvlAbsCnstPtr m); - /// Get the set of all vars of the ILA (including child). - static ExprSet GetVarTree(const InstrLvlAbsCnstPtr top); - /// Get the set of all state vars of the ILA (including child). - static ExprSet GetSttTree(const InstrLvlAbsCnstPtr top); - /// Get the set of all input vars of the ILA (including child). - static ExprSet GetInpTree(const InstrLvlAbsCnstPtr top); - - static void DuplInp(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst); - static void DuplStt(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst); - - /// Add all instructions of the ILA (excluding child) to the set. - static void InsertInstr(const InstrLvlAbsCnstPtr m, InstrVec& instrs); - /// Add all instructions of the ILA (including child) to the set. - static void InsertInstrTree(const InstrLvlAbsCnstPtr top, InstrVec& instrs); - - /// Get the set of instructions of the ILA (excluding child). - static InstrVec GetInstr(const InstrLvlAbsCnstPtr m); - /// Get the set of instructions of the ILA (including child). - static InstrVec GetInstrTree(const InstrLvlAbsCnstPtr top); - - /****************************************************************************/ - /// \brief Rewrite an expression by replacing based on the rule. - /// - If leaves contain non-var nodes, will replace with no further traverse. - static ExprPtr Rewrite(const ExprPtr e, const ExprMap& rule); - - /// \brief Rewrite an instruction by replacing based on the rule. - static void RewriteInstr(const InstrCnstPtr instr_src, - const InstrPtr instr_dst, const ExprMap& expr_map); - - /// \brief Flatten the given ILA, the initial conditions will be added to the - /// top the child instructions will also be added to the top, but their - /// (hierarchical) valid conditions will be added to their decode condition - /// Some usage hint: this function is intended to generate an ILA for Verilog - /// generator or other verification model generator. You can first use - /// ExtrDeptModl to extract the dependent model and use this to flatten the - /// that model and send to the generator - static void FlattenIla(const InstrLvlAbsPtr ila_ptr_); - - /// \brief Return a new ILA that contains the dependant instructions and - /// child-ILAs of an instruction (defined by sub-programs). - static InstrLvlAbsPtr ExtrDeptModl(const InstrPtr instr, - const std::string& name); - - /// Copy and ILA (including child). - static InstrLvlAbsPtr CopyIlaTree(const InstrLvlAbsCnstPtr src, - const std::string& dst_name); - - /****************************************************************************/ - /// Duplicate input vars from src to dst while updating the mapping. - static void DuplInp(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst, - ExprMap& expr_map); - /// Duplicate state vars from src to dst while updating the mapping. - static void DuplStt(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst, - ExprMap& expr_map); - /// Duplicate fetch from src to dst if defined (rewritten w.r.t. mapping). - static ExprPtr DuplFetch(const InstrLvlAbsCnstPtr src, - const InstrLvlAbsPtr dst, const ExprMap& expr_map); - /// Duplicate valid from src to dst if defined (rewritten w.r.t. mapping). - static ExprPtr DuplValid(const InstrLvlAbsCnstPtr src, - const InstrLvlAbsPtr dst, const ExprMap& expr_map); - /// Duplicate initial conditions from src to dst (rewritten w.r.t. mapping). - static void DuplInit(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst, - const ExprMap& expr_map); - /// Duplicate an instruction to dst (rewritten w.r.t. mapping). - static InstrPtr DuplInstr(const InstrCnstPtr instr_src, - const InstrLvlAbsPtr dst, const ExprMap& expr_map, - const CnstIlaMap& ila_map); - /// Duplicate instruction sequence to dst. NOT IMPLEMENTED YET. - static void DuplInstrSeq(const InstrLvlAbsCnstPtr src, - const InstrLvlAbsPtr dst); - -private: - /// Duplicate/create the input var in m. - static ExprPtr DuplInp(const InstrLvlAbsPtr m, const ExprPtr inp); - /// Duplicate/create the state var in m. - static ExprPtr DuplStt(const InstrLvlAbsPtr m, const ExprPtr stt); - -}; // class AbsKnob - -} // namespace ilang - -#endif // ILANG_VERIFICATION_ABS_KNOB_H__ diff --git a/include/ilang/verification/eq_check_crr.h b/include/ilang/verification/eq_check_crr.h deleted file mode 100644 index 40264651d..000000000 --- a/include/ilang/verification/eq_check_crr.h +++ /dev/null @@ -1,127 +0,0 @@ -/// \file -/// Header for generating verification condition for equivalence checking. - -#ifndef ILANG_VERIFICATION_EQ_CHECK_CRR_H__ -#define ILANG_VERIFICATION_EQ_CHECK_CRR_H__ - -#include "z3++.h" -#include -#include -#include - -/// \namespace ilang -namespace ilang { - -/// \brief Generator for commutating diagram-based equivalence checking. -class CommDiag { -public: - // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // - /// Default constructor. - CommDiag(z3::context& ctx, const CrrPtr crr); - /// Default destructor. - ~CommDiag(); - - // ------------------------- METHODS -------------------------------------- // - /// \brief Check equivalence between two models based on the refinement - /// relation up to the given unrolling bound. - /// \param[in] max unrolling bound. - bool EqCheck(const int& max = 10); - - /// \brief Incrementally checking equivalence between two models based on - /// the refinement relation up to the given unrolling bound. - /// \param[in] min #step of unrolling. - /// \param[in] max #step of unrolling. - bool IncEqCheck(const int& min = 0, const int& max = 10, const int& step = 1); - - bool IncCheck(const int& min = 0, const int& max = 10, const int& step = 1); - - typedef MonoUnroll Unroll; - -private: - // ------------------------- MEMBERS -------------------------------------- // - /// The underlying z3 context. - z3::context& ctx_; - /// The refinement relation. - CrrPtr crr_; - - // ------------------------- IncCheck ------------------------------------- // - - void Init(); - - enum UID { A_OLD, A_NEW, B_OLD, B_NEW }; - - struct UnrlUnit { - int lo = 0; - int hi = 0; - } uu_a_old_, uu_a_new_, uu_b_old_, uu_b_new_; - - Unroll unrl_a_old_ = Unroll(ctx_, k_suff_old_); - Unroll unrl_a_new_ = Unroll(ctx_, k_suff_new_); - Unroll unrl_b_old_ = Unroll(ctx_, k_suff_old_); - Unroll unrl_b_new_ = Unroll(ctx_, k_suff_new_); - - ExprSet stts_a_; - ExprSet stts_b_; - - Unroll& GetUnrl(const UID& uid); - Unroll& GetUnrlOld(); - Unroll& GetUnrlNew(); - Unroll& GetUnrlApl(); - - RefPtr GetRefine(const UID& uid); - UnrlUnit& GetUnrlUnit(const UID& uid); - const ExprSet& GetStts(const UID& uid); - - z3::expr GetZ3IncFlsh(const UID& uid); - z3::expr GetZ3IncCmpl(const UID& uid); - - // ------------------------- IncEqCheck ----------------------------------- // - static const std::string k_suff_old_; - static const std::string k_suff_new_; - static const std::string k_suff_apl_; - MonoUnroll unrl_old_ = MonoUnroll(ctx_, k_suff_old_); - MonoUnroll unrl_new_ = MonoUnroll(ctx_, k_suff_new_); - MonoUnroll unrl_apl_ = MonoUnroll(ctx_, k_suff_apl_); - - z3::expr GetZ3ApplInstr(const ExprSet& stts, const RefPtr ref); - z3::expr GetZ3Assm(); - z3::expr GetZ3Prop(); - z3::expr GetZ3Cmpl(const ExprPtr cmpl, MonoUnroll& un, const int& begin, - const int& end) const; - z3::expr GetZ3IncUnrl(MonoUnroll& un, const RefPtr ref, const int& begin, - const int& length, const ExprSet& stts) const; - bool CheckCmpl(z3::solver& s, z3::expr& cmpl_expr) const; - - // ------------------------- MonoCheck ------------------------------------ // - static const std::string k_suff_orig_; - static const std::string k_suff_appl_; - MonoUnroll unroll_appl_ = MonoUnroll(ctx_, k_suff_appl_); - MonoUnroll unroll_orig_ = MonoUnroll(ctx_, k_suff_orig_); - - bool SanityCheck(); - bool SanityCheckRefinement(const RefPtr ref); - bool SanityCheckRelation(const RelPtr rel, const InstrLvlAbsPtr ma, - const InstrLvlAbsPtr mb) const; - - int DetStepOrig(const RefPtr ref, const int& max); - int DetStepAppl(const RefPtr ref, const int& max); - bool CheckStepOrig(const RefPtr ref, const int& k); - bool CheckStepAppl(const RefPtr ref, const int& k); - - z3::expr GenInit(const RefPtr ref); - z3::expr GenTranRel(const RefPtr ref, const int& k_orig, const int& k_appl); - z3::expr GenAssm(); - z3::expr GenProp(); - - z3::expr AtLeastOnce(MonoUnroll& unroller, const ExprPtr cmpl, - const int& start, const int& end) const; - z3::expr AtMostOnce(MonoUnroll& unroller, const ExprPtr cmpl, - const int& start, const int& end) const; - z3::expr UnrollFlush(MonoUnroll& unroller, const RefPtr ref, const int& base, - const int& length, const int& start); - -}; // class CommDiag - -} // namespace ilang - -#endif // ILANG_VERIFICATION_EQ_CHECK_CRR_H__ diff --git a/include/ilang/verification/legacy_bmc.h b/include/ilang/verification/legacy_bmc.h deleted file mode 100644 index 0690099c5..000000000 --- a/include/ilang/verification/legacy_bmc.h +++ /dev/null @@ -1,82 +0,0 @@ -/// \file -/// Header for bounded model checking - -#ifndef ILANG_VERIFICATION_LEGACY_BMC_H__ -#define ILANG_VERIFICATION_LEGACY_BMC_H__ - -#include - -#include "z3++.h" -#include -#include -#include - -/// \namespace ilang -namespace ilang { - -/// \brief Simplified bounded model checking engine for ILAs. -class LegacyBmc { -public: - // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // - /// Default constructor. - LegacyBmc(); - /// Default destructor. - ~LegacyBmc(); - - // ------------------------- METHODS -------------------------------------- // - /// \brief Add initial condition to the solver. - void AddInit(ExprPtr init); - - /// \brief Add invariant to the solver. - void AddInvariant(ExprPtr inv); - - /// \brief Add property of one ILA. - void AddProperty(ExprPtr prop); - - /// \brief Legacy BMC where two ILAs are unrolled and compared monolithically. - z3::check_result Check(InstrLvlAbsPtr m0, const int& k0, InstrLvlAbsPtr m1, - const int& k1); - -private: - // ------------------------- MEMBERS -------------------------------------- // - /// z3 context. - z3::context ctx_; - /// Z3 expr generator. - Z3ExprAdapter gen_ = Z3ExprAdapter(ctx_); - - /// The set of invariants. - ExprPtrVec invs_; - /// The set of initial condition. - // - ExprPtrVec inits_; - - /// Automatically add default transition (unchanged) for un-specified states - /// if set to true. - bool def_tran_ = false; - - // ------------------------- HELPERS -------------------------------------- // - /// Unroll an ILA for k steps - /// \param[in] m pointer to the ILA to unroll. - /// \param[in] k number of steps to unroll. - /// \param[in] pos starting frame number (default 0). - /// \return the z3 expression representing the constraints. - z3::expr UnrollCmplIla(InstrLvlAbsPtr m, const int& k, const int& pos = 0); - - /// \brief Get the set of z3 expression (constraints) for the instruction. - /// - States with no update functions are encoded as unchanged. - z3::expr Instr(const InstrPtr instr, const std::string& suffix_prev, - const std::string& suffix_next, bool complete); - - /// \brief Get the set of z3 expression (constraints) for the ILA. - /// - Assume no child-ILAs (not considered). - /// - States with no update functions are encoded as unchanged. - /// - Assume one-hot encoding of all instructions. - z3::expr IlaOneHotFlat(const InstrLvlAbsPtr ila, - const std::string& suffix_prev, - const std::string& suffix_next); - -}; // class LegacyBmc - -} // namespace ilang - -#endif // ILANG_VERIFICATION_LEGACY_BMC_H__ diff --git a/include/ilang/verification/rewrite_expr.h b/include/ilang/verification/rewrite_expr.h deleted file mode 100644 index bc65d879b..000000000 --- a/include/ilang/verification/rewrite_expr.h +++ /dev/null @@ -1,43 +0,0 @@ -/// \file -/// Header for function object for rewriting Expr. - -#ifndef ILANG_VERIFICATION_REWRITE_EXPR_H__ -#define ILANG_VERIFICATION_REWRITE_EXPR_H__ - -#include -#include - -namespace ilang { - -/// \brief Function object for rewriting Expr. -class FuncObjRewrExpr { -public: - /// Constructor, initialize rewriting rule. - FuncObjRewrExpr(const ExprMap& rule) : rule_(rule) {} - - /// Return the rewritten result. - inline ExprPtr get(const ExprPtr e) const { - auto pos = rule_.find(e); - ILA_ASSERT(pos != rule_.end()) << e << " not found"; - return pos->second; - } - - /// Pre-process: return true (break) if the node has been visited. - bool pre(const ExprPtr e) const; - /// Post-process: update the rewriting rule map. - void post(const ExprPtr e); - -private: - /// Internal rewriting table. - ExprMap rule_; - - /// Rewrite all sorts of Expr. - ExprPtr Rewrite(const ExprPtr e) const; - /// Rewrite Operation sorted Expr. - ExprPtr RewriteOp(const ExprPtr e) const; - -}; // class FuncObjRewrExpr - -} // namespace ilang - -#endif // ILANG_VERIFICATION_REWRITE_EXPR_H__ diff --git a/include/ilang/verification/rewrite_ila.h b/include/ilang/verification/rewrite_ila.h deleted file mode 100644 index 1307bc157..000000000 --- a/include/ilang/verification/rewrite_ila.h +++ /dev/null @@ -1,75 +0,0 @@ -/// \file -/// Header for function object for rewriting ILA. - -#ifndef ILANG_VERIFICATION_REWRITE_ILA_H__ -#define ILANG_VERIFICATION_REWRITE_ILA_H__ - -#include - -namespace ilang { - -/// \brief Function object for rewriting ILA tree. -class FuncObjRewrIla { -public: - /// Type for storing ILA to ILA mapping. - typedef CnstIlaMap IlaMap; - - /// Constructor. - FuncObjRewrIla(const IlaMap& ila_map, const ExprMap& expr_map) - : ila_map_(ila_map), expr_map_(expr_map) {} - - /// Return the mapped ILA. - InstrLvlAbsPtr get(const InstrLvlAbsCnstPtr m) const; - - /// Pre-processing: create new ILA based on the given source. - bool pre(const InstrLvlAbsCnstPtr src); - /// Nothing. - void post(const InstrLvlAbsCnstPtr src) const; - -private: - /// ILA mapping. - IlaMap ila_map_; - /// Expr mapping. - ExprMap expr_map_; - -}; // FuncObjRewrIla - -/// \brief Function object for flatten ILA tree. -/// There is currently a problem: -/// this func obj calls duplInst -/// which in turn uses rewriteExpr -/// and rewriteExpr does not change the host of -/// of state variables, so the flatten expression -/// still has the host pointed to their original -/// ILA. This is fine for Verilog Gen, which only -/// depends on variable names to generate variables -/// but may not be good enough for other purpose. -class FuncObjFlatIla { -public: - /// Type for storing ILA to ILA mapping. - typedef CnstIlaMap IlaMap; - typedef std::stack ValidCondStack; - - /// Constructor. - FuncObjFlatIla(const InstrLvlAbsCnstPtr& top_, const IlaMap& ila_map, - const ExprMap& expr_map); - - /// Pre-processing: create new ILA based on the given source. - bool pre(const InstrLvlAbsCnstPtr src); - /// Nothing. - void post(const InstrLvlAbsCnstPtr src); - -private: - /// ILA mapping. - IlaMap ila_map_; - /// Expr mapping. - ExprMap expr_map_; - /// A stack to keep track of the hierarchical valid condition - ValidCondStack valid_cond_stack_; - /// Record which ila is the top level one - InstrLvlAbsCnstPtr top_ila_; -}; // FuncObjRewrIla - -} // namespace ilang - -#endif // ILANG_VERIFICATION_REWRITE_ILA_H__ diff --git a/include/ilang/verification/unroller.h b/include/ilang/verification/unroller.h deleted file mode 100644 index 95a8f0ddd..000000000 --- a/include/ilang/verification/unroller.h +++ /dev/null @@ -1,289 +0,0 @@ -/// \file -/// Header for unrolling ILA execution. - -#ifndef ILANG_VERIFICATION_UNROLLER_H__ -#define ILANG_VERIFICATION_UNROLLER_H__ - -#include -#include - -#include "z3++.h" -#include -#include - -/// \namespace ilang -namespace ilang { - -/// \brief Base class for unrolling ILA execution in different settings. -class Unroller { -public: - /// Type alias for z3::expr. - typedef z3::expr ZExpr; - /// Type for containing a set of z3::expr. - typedef z3::expr_vector ZExprVec; - /// Type alias for a set of ExprPtr. - typedef ExprPtrVec IExprVec; - - // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // - /// Default constructor - Unroller(z3::context& ctx, const std::string& suffix); - /// Default virtual destructor. - virtual ~Unroller(); - - // ------------------------- METHODS -------------------------------------- // - /// Add a predicate that should be asserted globally. - void AddGlobPred(const ExprPtr p); - /// Add a predicate that should be asserted in the initial condition. - void AddInitPred(const ExprPtr p); - /// Add a predicate that should be asserted at the k-th step. - void AddStepPred(const ExprPtr p, const int& k); - /// Clear the global predicates. - void ClearGlobPred(); - /// Clear the initial predicates. - void ClearInitPred(); - /// Clear the step-specific predicates. - void ClearStepPred(); - /// Clear all predicates. - void ClearPred(); - - // ------------------------- HELPERS -------------------------------------- // - /// Return the z3::expr representing the current state at the time. - ZExpr CurrState(const ExprPtr v, const int& t); - /// Return the z3::expr representing the next state at the time. - ZExpr NextState(const ExprPtr v, const int& t); - /// Return the z3::expr representing the current-based Expr at the time. - ZExpr GetZ3Expr(const ExprPtr e, const int& t); - /// Return the z3::expr representing a unique Expr (regardless of time). - ZExpr GetZ3Expr(const ExprPtr e); - /// Return the z3::expr representing a and b are equal at their time. - ZExpr Equal(const ExprPtr va, const int& ta, const ExprPtr vb, const int& tb); - -protected: - // ------------------------- MEMBERS -------------------------------------- // - /// The set of dependant state variables. - IExprVec vars_; - /// The set of predicates to be asserted of each step. - IExprVec k_pred_; - /// The set of state update functions of each step. - IExprVec k_next_; - - // ------------------------- METHODS -------------------------------------- // - /// \brief [Application-specific] Define dependant state variables. - /// - "vars_" should be assigned with the state vars uniquely. - /// - "vars_" will be cleared before caling this function. - /// = The var order stored in "vars_" will be the globally agree-upon order. - virtual void DefineDepVar() = 0; - - /// \brief [Application-specific] Define next state update functions. - /// - "k_next_" should be assigned with the next state expression. - /// - "k_next_" follows the global order as stored in "vars_". - /// - "k_next_" will NOT be cleared before calling (is the only modifier). - /// - "k_pred_" can be used to store step-specific predicates, e.g. decode. - /// - "k_pred_" will NOT be cleared before calling (is the only modifier). - virtual void Transition(const int& idx) = 0; - - /// Unroll while substituting internal expression. - ZExpr UnrollSubs(const size_t& len, const int& pos); - /// Unroll without substituting internal expression. - ZExpr UnrollAssn(const size_t& len, const int& pos, bool cache = false); - /// Unroll without asserting state equality between each step. - ZExpr UnrollNone(const size_t& len, const int& pos); - - // ------------------------- HELPERS -------------------------------------- // - /// Return the state update function (unchanged if not defined). - static ExprPtr StateUpdCmpl(const InstrPtr instr, const ExprPtr var); - /// Return the decode function (true if not defined). - static ExprPtr DecodeCmpl(const InstrPtr instr); - - /// Create a new free variable (with same sort) under the same host. - static ExprPtr NewFreeVar(const ExprPtr var, const std::string& name); - -private: - // ------------------------- MEMBERS -------------------------------------- // - /// z3::context of the unroller. - z3::context& ctx_; - /// z3 expression generator. - Z3ExprAdapter gen_; - - /// Extra suffix for customized applications. - std::string extra_suff_ = ""; - - /// The set of global predicates. - IExprVec g_pred_; - /// The set of initial predicates. - IExprVec i_pred_; - /// The mapping of (external) step-specific predicates. - std::map s_pred_; - - /// The set of z3::expr representing the latest states of previous steps. - ZExprVec k_prev_z3_; - /// The set of z3::expr representing the current states. - ZExprVec k_curr_z3_; - /// The set of z3::expr representing the next states. - ZExprVec k_next_z3_; - - /// The set of constraints that should be asserted. - ZExprVec cstr_; - - // ------------------------- ACCESSORS/MUTATORS --------------------------- // - /// Return the underlying z3::context. - inline z3::context& ctx() const { return ctx_; } - /// Return the z3::expr generator. - inline Z3ExprAdapter& gen() { return gen_; } - - // ------------------------- HELPERS -------------------------------------- // - /// \brief Boot-strapping information needed for unrolling. - /// - collect dependant state variables - /// - prepare rewriting table - void BootStrap(const int& pos, bool cache = false); - - /// Assert equal between the z3::expr and the Expr w.r.t the suffix. - void AssertEqual(const ZExprVec& z, const IExprVec& e, - const std::string& suffix); - - /// Clear the z3::epxr container. - inline void Clear(ZExprVec& z3_vec); - - /// Generate and append the z3::expr for the set of Expr w.r.t. the suffix. - void IExprToZExpr(const IExprVec& i_expr_src, const std::string& suffix, - ZExprVec& z_expr_dst); - /// \brief Generate and append the z3::expr for the set of Expr w.r.t. the - /// suffix while substituting internal expressions. - void IExprToZExpr(const IExprVec& i_expr_src, const std::string& suffix, - ZExprVec& z_expr_dst, const ZExprVec& subs_src, - const ZExprVec& subs_dst); - - /// Wrapper for assigning (copying) z3::expr_vector from src to dst. - void CopyZExprVec(const ZExprVec& src, ZExprVec& dst); - - /// Conjunct (AND) all the predicates in the set. - ZExpr ConjPred(const ZExprVec& vec) const; - - /// Suffix generator for current state expressions of each step. - inline std::string SuffCurr(const int& t) const { - return std::to_string(t) + "_" + extra_suff_; - } - /// Suffix generator for next state symbol of each step. - inline std::string SuffNext(const int& t) const { - return std::to_string(t) + "_" + extra_suff_ + ".nxt"; - } - -}; // class Unroller - -/// \brief Application class for unrolling a path of instruction sequence. -class PathUnroll : public Unroller { -public: - /// Type of a list of instruction sequence. - typedef std::vector InstrVec; - - // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // - /// Default constructor. - PathUnroll(z3::context& ctx, const std::string& suff = ""); - /// Default destructor. - ~PathUnroll(); - - // ------------------------- METHODS -------------------------------------- // - /// \brief Unroll a sequence of instructions with internal states substituted. - /// \param[in] seq the sequence of instructions. - /// \param[in] pos the starting time frame. - ZExpr PathSubs(const std::vector& seq, const int& pos = 0); - - /// \brief Unroll a sequence of instructions while asserting states are equal - /// between each step. - /// \param[in] seq the sequence of instructions. - /// \param[in] pos the starting time frame. - ZExpr PathAssn(const std::vector& seq, const int& pos = 0); - - /// \brief Unroll a sequence of instructions without asserting states - /// relations between steps. "N(var_i) == var_i.nxt_suff" - /// \param[in] seq the sequence of instructions. - /// \param[in] pos the starting time frame. - ZExpr PathNone(const std::vector& seq, const int& pos = 0); - -protected: - // ------------------------- METHODS -------------------------------------- // - /// \brief [Application-specific] Define dependant state variables. - /// - "vars_" should be assigned with the state vars uniquely. - /// - "vars_" will be cleared before caling this function. - /// = The var order stored in "vars_" will be the globally agree-upon order. - void DefineDepVar(); - - /// \brief [Application-specific] Define next state update functions. - /// - "k_next_" should be assigned with the next state expression. - /// - "k_next_" follows the global order as stored in "vars_". - /// - "k_next_" will NOT be cleared before calling (is the only modifier). - /// - "k_pred_" can be used to store step-specific predicates, e.g. decode. - /// - "k_pred_" will NOT be cleared before calling (is the only modifier). - void Transition(const int& idx); - -private: - // ------------------------- MEMBERS -------------------------------------- // - /// The sequence of instructions. - InstrVec seq_; -}; // class PathUnroll - -/// \brief Application class for unrolling the ILA as a monolithic transition -/// system. -class MonoUnroll : public Unroller { -public: - // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // - /// Default constructor. - MonoUnroll(z3::context& ctx, const std::string& suff = ""); - /// Default destructor. - ~MonoUnroll(); - - // ------------------------- METHODS -------------------------------------- // - /// \brief Unroll the ILA with internal states substituted. - /// \param[in] top the top-level ILA. - /// \param[in] length number of steps to unroll. - /// \param[in] pos the starting time frame. - ZExpr MonoSubs(const InstrLvlAbsPtr top, const int& length, - const int& pos = 0); - - /// \brief Unroll the ILA while asserting states are equal between each step. - /// \param[in] top the top-level ILA. - /// \param[in] length number of steps to unroll. - /// \param[in] pos the starting time frame. - ZExpr MonoAssn(const InstrLvlAbsPtr top, const int& length, - const int& pos = 0); - - /// \brief Unroll the ILA without asserting states relations between steps. - /// \param[in] top the top-level ILA. - /// \param[in] length number of steps to unroll. - /// \param[in] pos the starting time frame. - ZExpr MonoNone(const InstrLvlAbsPtr top, const int& length, - const int& pos = 0); - - /// \brief Incrementally unrolling the ILA using MonoAssn (with transition - /// relation being cached). - /// \param[in] top the top-level ILA. - /// \param[in] length number of steps to unroll. - /// \param[in] pos the starting time frame. - ZExpr MonoIncr(const InstrLvlAbsPtr top, const int& length, const int& pos); - -protected: - // ------------------------- METHODS -------------------------------------- // - /// \brief [Application-specific] Define dependant state variables. - /// - "vars_" should be assigned with the state vars uniquely. - /// - "vars_" will be cleared before caling this function. - /// - The var order stored in "vars_" will be the globally agree-upon order. - void DefineDepVar(); - - /// \brief [Application-specific] Define next state update functions. - /// - "k_next_" should be assigned with the next state expression. - /// - "k_next_" follows the global order as stored in "vars_". - /// - "k_next_" will NOT be cleared before calling (is the only modifier). - /// - "k_pred_" can be used to store step-specific predicates, e.g. decode. - /// - "k_pred_" will NOT be cleared before calling (is the only modifier). - void Transition(const int& idx); - -private: - // ------------------------- MEMBERS -------------------------------------- // - /// The sequence of instructions. - InstrLvlAbsPtr top_; - -}; // class MonoUnroll - -} // namespace ilang - -#endif // ILANG_VERIFICATION_UNROLLER_H__ From 81418cc9efc5246ac93113d9936680f96b605e0f Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 13 Jul 2020 23:14:58 -0400 Subject: [PATCH 30/30] format --- test/t_unroll_seq.cc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/test/t_unroll_seq.cc b/test/t_unroll_seq.cc index 030cdc0ed..7e85b7218 100644 --- a/test/t_unroll_seq.cc +++ b/test/t_unroll_seq.cc @@ -1,11 +1,13 @@ /// \file /// Unit test for unrolling a sequence of instruction. +#include + +#include + #include "unit-include/eq_ilas.h" #include "unit-include/simple_cpu.h" #include "unit-include/util.h" -#include -#include namespace ilang {