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