diff --git a/.github/workflows/cmake.yml b/.github/workflows/cmake.yml
index 9e7372839..be7d0f804 100644
--- a/.github/workflows/cmake.yml
+++ b/.github/workflows/cmake.yml
@@ -1,34 +1,57 @@
name: CMake
-on: [push]
+on:
+ push:
+
+ pull_request:
+ branches:
+ - main
+
+ schedule:
+ - cron: '0 9 * * *'
env:
BUILD_TYPE: Release
jobs:
build:
- runs-on: ubuntu-latest
+ runs-on: self-hosted
+ # OS: CentOs 8
+ # Packages: bison flex gmp-devel
steps:
- uses: actions/checkout@v2
- - name: Install Dependent Packages
- run: sudo apt install bison flex z3 libz3-dev
-
- name: Create Build Environment
- run: cmake -E make_directory ${{runner.workspace}}/build
+ run: |
+ cmake -E make_directory ${{github.workspace}}/deps-src
+ cmake -E make_directory ${{github.workspace}}/deps-bin
+ cmake -E make_directory ${{github.workspace}}/build
+
+ - name: Build and Install Dependency
+ shell: bash
+ run: source ${{github.workspace}}/scripts/setup-smtswitch.sh ${{github.workspace}}/deps-src ${{github.workspace}}/deps-bin
- name: Configure CMake
shell: bash
- working-directory: ${{runner.workspace}}/build
- run: cmake $GITHUB_WORKSPACE -DCMAKE_BUILD_TYPE=$BUILD_TYPE
+ working-directory: ${{github.workspace}}/build
+ run: cmake ${{github.workspace}} -DCMAKE_BUILD_TYPE=$BUILD_TYPE -DCMAKE_PREFIX_PATH=${{github.workspace}}/deps-bin
- name: Build
- working-directory: ${{runner.workspace}}/build
shell: bash
- run: cmake --build . --config $BUILD_TYPE
+ working-directory: ${{github.workspace}}/build
+ run: make -j$(nproc)
- name: Test
- working-directory: ${{runner.workspace}}/build
shell: bash
+ working-directory: ${{github.workspace}}/build
run: make run_test
+
+ clean:
+ needs: build
+ runs-on: self-hosted
+
+ steps:
+ - name: Remove Workspace
+ shell: bash
+ run: rm -rf ${{github.workspace}}
diff --git a/.gitmodules b/.gitmodules
index f2f3e286e..aeb856b19 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -6,4 +6,4 @@
url = https://github.com/PrincetonUniversity/ILA-Synthesis-Python.git
[submodule "extern/smt-switch"]
path = extern/smt-switch
- url = https://github.com/makaimann/smt-switch.git
+ url = https://github.com/stanford-centaur/smt-switch
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 1498562aa..55e0123d1 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -28,7 +28,7 @@ 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)
option(ILANG_BUILD_INVSYN "Build invariant synthesis feature." ON)
-option(ILANG_BUILD_SWITCH "Build smt-switch interface." OFF)
+option(ILANG_BUILD_SWITCH "Build smt-switch interface." ON)
option(ILANG_BUILD_COSIM "Build QEMU-based co-simulation support." OFF)
include(CMakeDependentOption)
diff --git a/README.md b/README.md
index dd536e1b9..757f8b96b 100644
--- a/README.md
+++ b/README.md
@@ -33,40 +33,43 @@
### Prerequisites
ILAng requires CMake (3.9.6 or above) and compilers with C++17 support.
-To install dependencies on Debian-based Linux:
+To install dependent packages:
```bash
-apt-get install bison flex z3 libz3-dev
-```
-
-To install dependencies (besides [z3](https://github.com/Z3Prover/z3)) on Fedora-based Linux:
+# Debian-based
+apt-get install bison flex
-```bash
+# Fedora-based
yum install bison flex
+
+# OSX
+brew install bison flex
```
-To install dependencies on OSX:
+To build smt-switch and SMT solvers:
-```bash
-brew install bison flex z3
+``` bash
+mkdir -p
+source scripts/setup-smtswitch.sh
```
### Default Build
-To build ILAng with default configuration, create a build directory and make:
+To build ILAng with default configuration:
```bash
mkdir -p build && cd build
-cmake ..
+cmake .. -DCMAKE_PREFIX_PATH=
make
```
If you are using git older than `1.8.4`, init the submodule from root and disable config-time submodule fetching:
+
```bash
git submodule update --init --recursive
mkdir -p build && cd build
-cmake .. -DILANG_FETCH_DEPS=OFF
+cmake .. -DILANG_FETCH_DEPS=OFF -DCMAKE_PREFIX_PATH=
make
```
@@ -83,7 +86,6 @@ sudo make install
- Use `-DILANG_BUILD_TEST=OFF` to disalbe building the unit tests.
- Use `-DILANG_BUILD_SYNTH=ON` to enable building the synthesis engine (required [Boost](https://www.boost.org)).
- Use `-DILANG_BUILD_INVSYN=OFF` to disable building invariant synthesis feature.
-- Use `-DILANG_BUILD_SWITCH=ON` to enable building [smt-switch](https://github.com/makaimann/smt-switch.git) interface support.
- Use `-DILANG_BUILD_COSIM=ON` to enable building [Xilinx cosimulation](https://www.linuxsecrets.com/xilinx/QEMU%20SystemC%20and%20TLM%20CoSimulation.html) support.
- Use `-DILANG_INSTALL_DEV=ON` to install working features.
@@ -233,7 +235,7 @@ Copyright (c) 2018 Ben Marshall.
ILAng uses the [SMT parser](https://es-static.fbk.eu/people/griggio/misc/smtlib2parser.html), which is licensed under the [MIT License](https://es-static.fbk.eu/people/griggio/misc/smtlib2parser.html).
Copyright (c) 2010 Alberto Griggio.
-ILAng uses the [smt-switch](https://github.com/makaimann/smt-switch.git), which is licensed under the [BSD 3-Clause License](https://github.com/makaimann/smt-switch/blob/master/LICENSE).
+ILAng uses the [smt-switch](https://github.com/stanford-centaur/smt-switch), which is licensed under the [BSD 3-Clause License](https://github.com/stanford-centaur/smt-switch/blob/master/LICENSE).
Copyright (c) 2019-2020 the authors.
ILAng uses [ItSy](https://github.com/PrincetonUniversity/ItSy), which is licensed under the [MIT License](https://github.com/PrincetonUniversity/ItSy/blob/master/LICENSE).
diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake
new file mode 100644
index 000000000..797973064
--- /dev/null
+++ b/cmake/FindGMP.cmake
@@ -0,0 +1,19 @@
+# Find GMP
+# GMP_FOUND - system has GMP lib
+# GMP_INCLUDE_DIR - the GMP include directory
+# GMP_LIBRARIES - Libraries needed to use GMP
+
+find_path(GMP_INCLUDE_DIR NAMES gmp.h gmpxx.h)
+find_library(GMP_LIBRARIES NAMES gmp)
+find_library(GMPXX_LIBRARIES NAMES gmpxx)
+
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES)
+
+mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARIES)
+if(GMP_LIBRARIES)
+ message(STATUS "Found GMP libs: ${GMP_LIBRARIES}")
+endif()
+if (GMPXX_LIBRARIES)
+ message(STATUS "Found GMPXX libs: ${GMPXX_LIBRARIES}")
+endif()
diff --git a/cmake/Findsmtswitch.cmake b/cmake/Findsmtswitch.cmake
index 68f352368..db911ae21 100644
--- a/cmake/Findsmtswitch.cmake
+++ b/cmake/Findsmtswitch.cmake
@@ -11,6 +11,7 @@
# SMTSWITCH_CVC4_FOUND
# SMTSWITCH_MSAT_FOUND
# SMTSWITCH_YICES2_FOUND
+# SMTSWITCH_Z3_FOUND
#
# and the following imported targets
#
@@ -19,6 +20,7 @@
# smt-switch::smt-switch-cvc4
# smt-switch::smt-switch-msat
# smt-switch::smt-switch-yices2
+# smt-switch::smt-switch-z3
#
# XXX smt-switch needs to be built with static type
@@ -26,6 +28,7 @@
find_package(PkgConfig)
pkg_check_modules(PC_SMTSWITCH QUIET SMTSWITCH)
+find_package(GMP REQUIRED)
##
## core smt-switch
@@ -119,6 +122,22 @@ endif()
set(SMTSWITCH_YICES2_LIBRARY ${SMTSWITCH_YICES_LIBRARY} ${SMTSWITCH_LIBRARY})
mark_as_advanced(SMTSWITCH_YICES2_FOUND)
+# z3
+find_library(SMTSWITCH_Z3_LIBRARY
+ NAMES smt-switch-z3
+ HINTS ${PC_SMTSWITCH_LIBDIR} ${PC_SMTSWITCH_LIBRARY_DIRS}
+ PATH_SUFFIXES smt-switch
+)
+
+if(SMTSWITCH_Z3_LIBRARY)
+ set(SMTSWITCH_Z3_FOUND TRUE)
+else()
+ set(SMTSWITCH_Z3_FOUND FALSE)
+endif()
+
+set(SMTSWITCH_Z3_LIBRARY ${SMTSWITCH_Z3_LIBRARY} ${SMTSWITCH_LIBRARY})
+mark_as_advanced(SMTSWITCH_Z3_FOUND)
+
# create imported target smt-switch::smt-switch
if(SMTSWITCH_FOUND AND NOT TARGET smt-switch::smt-switch)
add_library(smt-switch::smt-switch INTERFACE IMPORTED)
@@ -184,3 +203,16 @@ if(SMTSWITCH_YICES2_FOUND AND NOT TARGET smt-switch::smt-switch-yices2)
)
endif()
+# create imported target smt-switch::smt-switch-z3
+if(SMTSWITCH_Z3_FOUND AND NOT TARGET smt-switch::smt-switch-z3)
+ add_library(smt-switch::smt-switch-z3 INTERFACE IMPORTED)
+ set_property(
+ TARGET smt-switch::smt-switch-z3
+ PROPERTY INTERFACE_INCLUDE_DIRECTORIES ${SMTSWITCH_INCLUDE_DIR}
+ )
+ set_property(
+ TARGET smt-switch::smt-switch-z3
+ PROPERTY INTERFACE_LINK_LIBRARIES ${SMTSWITCH_Z3_LIBRARY}
+ )
+endif()
+
diff --git a/extern/smt-switch b/extern/smt-switch
index 68dad97f7..768ed5d05 160000
--- a/extern/smt-switch
+++ b/extern/smt-switch
@@ -1 +1 @@
-Subproject commit 68dad97f77282f77d3f5ae93ffc5e521d88e3992
+Subproject commit 768ed5d05315d0b652a915adcfbbc7f3e7a4896a
diff --git a/include/ilang/ila-mngr/u_progfrag.h b/include/ilang/ila-mngr/u_progfrag.h
new file mode 100644
index 000000000..d4397ce23
--- /dev/null
+++ b/include/ilang/ila-mngr/u_progfrag.h
@@ -0,0 +1,149 @@
+/// \file
+/// Defines the program fragment AST
+
+#ifndef ILANG_ILA_MNGR_U_PROGFRAG_H__
+#define ILANG_ILA_MNGR_U_PROGFRAG_H__
+
+#include
+#include
+#include
+#include
+#include
+
+#include
+
+#include
+#include
+
+/// \namespace ilang
+namespace ilang {
+
+ /// \namespace pfast
+ /// Defines the program-fragment AST
+ namespace pfast {
+
+ using Constraint = ExprPtr;
+
+ struct Assert;
+ struct Assume;
+ struct Call;
+ struct Update;
+ struct While;
+ struct Block;
+
+ using Stmt = std::variant;
+
+ /// Converts to a string for pretty printing
+ std::string to_string(const Stmt& s);
+
+ struct Block : public std::vector {
+ using base=std::vector;
+ using base::base;
+ using base::operator=;
+ };
+
+ struct ProgramFragment {
+ ExprSet params;
+ Block body;
+ };
+
+ /// Checks structural equality
+ bool operator==(const ProgramFragment& a, const ProgramFragment& b);
+
+ /// Converts to a string for pretty printing
+ std::string to_string(const ProgramFragment& pf);
+ std::ostream& operator<<(std::ostream& out, const ProgramFragment& pf);
+
+ struct Assert {
+ Constraint assertion;
+ /// Checks structural equality
+ bool operator==(const Assert& b) const {
+ return asthub::TopEq(assertion, b.assertion);
+ }
+ };
+
+ static_assert(std::is_copy_constructible_v, "assert not copy constructible");
+ static_assert(std::is_copy_assignable_v, "assert not copy assignable");
+
+ struct Assume {
+ Constraint assumption;
+ /// Checks structural equality
+ bool operator==(const Assume& b) const {
+ return asthub::TopEq(assumption, b.assumption);
+ }
+ };
+
+ static_assert(std::is_copy_constructible_v, "assume not copy constructible");
+ static_assert(std::is_copy_assignable_v, "assume not copy assignable");
+
+ struct Call {
+ InstrPtr instr;
+ Constraint input_constraint;
+
+ /// Checks structural equality
+ bool operator==(const Call& b) const {
+ return (instr == b.instr)
+ && (bool(input_constraint) == bool(b.input_constraint))
+ && (!bool(input_constraint)
+ || asthub::TopEq(input_constraint, b.input_constraint));
+ }
+ };
+
+ static_assert(std::is_copy_constructible_v, "call not copy constructible");
+ static_assert(std::is_copy_assignable_v, "call not copy assignable");
+
+ struct Update: public ExprMap {
+ using base=ExprMap;
+ using base::base;
+ using base::operator=;
+ };
+
+ static_assert(std::is_copy_constructible_v, "update not copy constructible");
+ static_assert(std::is_copy_assignable_v, "update not copy assignable");
+
+ struct While {
+ Constraint loop_condition;
+ Block body;
+
+ /// Checks structural equality
+ bool operator==(const While& w) const {
+ return (asthub::TopEq(loop_condition, w.loop_condition)
+ && body == w.body);
+ }
+ };
+
+ static_assert(std::is_copy_constructible_v, "while not copy constructible");
+ static_assert(std::is_copy_assignable_v, "while not copy assignable");
+
+ static_assert(std::is_copy_constructible_v, "stmt not copy constructible");
+ static_assert(std::is_copy_assignable_v, "stmt not copy constructible");
+
+
+ /// \class PrettyPrinter
+ /// A visitor for pretty-printing program-fragment AST elements
+ class PrettyPrinter {
+ public:
+ PrettyPrinter(): buf_ {} {}
+ ~PrettyPrinter()=default;
+ void operator()(const ProgramFragment& pf);
+ void operator()(const Block& b);
+
+ void operator()(const Assert& a);
+ void operator()(const Assume& a);
+ void operator()(const Call& c);
+ void operator()(const Update& u);
+ void operator()(const While& w);
+
+ std::string str() { return buf_.str(); }
+ private:
+ std::ostringstream buf_;
+ int indent_;
+
+ std::string reserved_word(const std::string& word);
+ std::string indent_str();
+ };
+
+ }
+}
+
+#endif
\ No newline at end of file
diff --git a/include/ilang/ila-mngr/u_unroller_smt.h b/include/ilang/ila-mngr/u_unroller_smt.h
index 446b71a9c..a9b8d05a0 100644
--- a/include/ilang/ila-mngr/u_unroller_smt.h
+++ b/include/ilang/ila-mngr/u_unroller_smt.h
@@ -59,6 +59,11 @@ template class UnrollerSmt {
return smt_gen_.GetShimFunc(func);
}
+ /// Return the deciding variables used for the previous unrolling.
+ inline const ExprPtrVec& GetLastDecidingVars() {
+ return deciding_vars_;
+ }
+
private:
// ------------------------- MEMBERS -------------------------------------- //
/// The underlying (templated) SMT generator.
diff --git a/include/ilang/ila-mngr/v_eq_check_progfrag.h b/include/ilang/ila-mngr/v_eq_check_progfrag.h
new file mode 100644
index 000000000..d298788dc
--- /dev/null
+++ b/include/ilang/ila-mngr/v_eq_check_progfrag.h
@@ -0,0 +1,119 @@
+/// \file
+/// Program-fragment-based ILA equivalence checking using
+/// constrained horn clauses.
+
+#ifndef ILANG_ILA_MNGR_V_EQ_CHECK_PROGFRAG_H__
+#define ILANG_ILA_MNGR_V_EQ_CHECK_PROGFRAG_H__
+
+#include
+#include
+#include
+#include
+
+#include
+
+#include
+
+#include
+#include
+
+/// \namespace ilang
+namespace ilang {
+
+ /// \namespace pgraph
+ /// Expresses program fragments using cut-point graphs
+ namespace pgraph {
+
+ using Location = std::string;
+ constexpr char LOC_BEGIN[] = "begin";
+ constexpr char LOC_ERROR[] = "fail";
+ constexpr char LOC_END[] = "end";
+
+ using BasicStmt = std::variant;
+ using StmtSeq = std::vector;
+
+ using Edge = StmtSeq;
+
+ struct EdgeTo {
+ Edge edge;
+ Location to;
+ };
+
+ using Edges = std::vector;
+
+ using CutpointGraph = std::unordered_map;
+
+ CutpointGraph program_graph(const pfast::ProgramFragment& pf);
+
+ }
+
+ // TODO: Use an unroller to convert sequences of
+ // instructions to predicates
+ // Should I create a program fragment unroller?
+ // Decision: use PathUnroller.Unroll, PathUnroller.GetSMTCurrent
+ class PFToCHCEncoder {
+
+ using Predicate = ExprPtr;
+
+ public:
+
+ PFToCHCEncoder(
+ z3::context& ctx, z3::fixedpoint& ctxfp,
+ const InstrLvlAbsPtr& ila, const pfast::ProgramFragment& pf);
+ ~PFToCHCEncoder()=default;
+
+ std::string to_string();
+
+ z3::check_result check_assertions() {
+ // z3::expr q = get_error_query();
+ z3::func_decl_vector q = get_error_queries();
+ return ctxfp_.query(q);
+ }
+
+ ExprSet scope() { return total_scope_; }
+
+ private:
+ const InstrLvlAbsPtr ila_;
+ const pgraph::CutpointGraph pg_;
+ const ExprSet params_;
+ ExprPtrVec pred_scope_;
+ ExprSet total_scope_;
+
+ z3::context& ctx_;
+ z3::fixedpoint& ctxfp_;
+
+ std::unordered_map loc_predicates_;
+ int max_step_count_ {0};
+
+ constexpr static char PRED_END_SUFFIX[] = "end";
+
+ // internal constructor
+ PFToCHCEncoder(
+ z3::context& ctx, z3::fixedpoint& ctxfp,
+ const InstrLvlAbsPtr& ila, const pgraph::CutpointGraph& pg, const ExprSet& params);
+
+ void encode();
+
+ void encode_transition(
+ const pgraph::Location& start,
+ const pgraph::StmtSeq& transition,
+ const pgraph::Location& end);
+
+ void record_scopes(const pgraph::CutpointGraph& pg, const ExprSet& params);
+ void add_unique_vars(
+ const pgraph::BasicStmt& s, ExprSet& pred_scope, ExprSet& total_scope);
+
+ ExprPtrVec get_scope(const pgraph::Location& l) {
+ return pred_scope_; // for now, same scope for the whole graph
+ }
+
+ Predicate get_or_make_loc_predicate(const std::string& name);
+ Predicate new_predicate(const std::string& name, const ExprPtrVec& args);
+
+ z3::func_decl_vector get_error_queries();
+
+ };
+
+}
+
+#endif
\ No newline at end of file
diff --git a/include/ilang/ila/ast/expr.h b/include/ilang/ila/ast/expr.h
index 1bf4be153..e4fa7b304 100644
--- a/include/ilang/ila/ast/expr.h
+++ b/include/ilang/ila/ast/expr.h
@@ -90,6 +90,9 @@ class Expr : public Ast, public std::enable_shared_from_this {
/// Output to stream.
virtual std::ostream& Print(std::ostream& out) const = 0;
+ /// Pretty output function
+ virtual std::ostream& PrintPretty(std::ostream& out) const = 0;
+
/// Overload output stream operator for pointer.
friend std::ostream& operator<<(std::ostream& out, const ExprPtr& expr) {
return expr->Print(out);
diff --git a/include/ilang/ila/ast/expr_const.h b/include/ilang/ila/ast/expr_const.h
index 82826c233..9ec5bc4cf 100644
--- a/include/ilang/ila/ast/expr_const.h
+++ b/include/ilang/ila/ast/expr_const.h
@@ -37,6 +37,9 @@ class ExprConst : public Expr {
/// Output to stream.
std::ostream& Print(std::ostream& out) const;
+ /// Pretty output function
+ std::ostream& PrintPretty(std::ostream& out) const;
+
/// Return the Boolean value.
BoolValPtr val_bool() const;
/// Return the Bitvector value.
diff --git a/include/ilang/ila/ast/expr_op.h b/include/ilang/ila/ast/expr_op.h
index 7de15549a..972a76344 100644
--- a/include/ilang/ila/ast/expr_op.h
+++ b/include/ilang/ila/ast/expr_op.h
@@ -89,6 +89,9 @@ class ExprOp : public Expr {
/// Output to stream.
std::ostream& Print(std::ostream& out) const;
+ /// Pretty output function
+ std::ostream& PrintPretty(std::ostream& out) const;
+
protected:
// ------------------------- HELPERS -------------------------------------- //
/// Derived the sort for binary operations.
diff --git a/include/ilang/ila/ast/expr_var.h b/include/ilang/ila/ast/expr_var.h
index 38e4331cc..288abbe57 100644
--- a/include/ilang/ila/ast/expr_var.h
+++ b/include/ilang/ila/ast/expr_var.h
@@ -40,6 +40,9 @@ class ExprVar : public Expr {
/// Output to stream.
std::ostream& Print(std::ostream& out) const;
+ /// Pretty output function
+ std::ostream& PrintPretty(std::ostream& out) const;
+
private:
// ------------------------- MEMBERS -------------------------------------- //
diff --git a/include/ilang/ilang++.h b/include/ilang/ilang++.h
index 09f7d6616..b3be28742 100644
--- a/include/ilang/ilang++.h
+++ b/include/ilang/ilang++.h
@@ -9,6 +9,7 @@
#include
#include
#include
+#include
#include
#ifdef SMTSWITCH_INTERFACE
@@ -56,6 +57,8 @@ class Expr;
class Instr;
class InstrLvlAbs;
class Unroller;
+namespace pfast { class ProgramFragment; }
+class PFToCHCEncoder;
// forward declaration
class Ila;
@@ -747,15 +750,232 @@ class IlaZ3Unroller {
#ifdef SMTSWITCH_INTERFACE
-/// \brief Reset the solver and generate the SMT Term (for smt-switch).
+/// \brief Generate the SMT Term (for smt-switch).
/// \param[in] solver The SMT solver in smt-switch.
/// \param[in] expr The target ILA expression.
/// \param[in] suffix The suffix to add on SMT symbols' name.
-smt::Term ResetAndGetSmtTerm(smt::SmtSolver& solver, const ExprRef& expr,
- const std::string& suffix = "");
+smt::Term GetSmtTerm(smt::SmtSolver& solver, const ExprRef& expr,
+ const std::string& suffix = "");
#endif // SMTSWITCH_INTERFACE
+namespace programfragment {
+
+ /// \brief The type of a constraint in the program fragment language.
+ using Constraint = ExprRef;
+
+ /// \brief Wrapper for a bitvector that allows it to be automatically
+ /// zero/sign extended as part of an Update statement.
+ struct ExtendableBv {
+ ExprRef expr;
+ enum ExtMode {EXT_ZERO, EXT_SIGNED} ext_mode;
+
+ /// \brief Constructs an ExtendableBv from a bitvector expr.
+ /// \param[in] expr The ILA expression to extend as needed.
+ explicit ExtendableBv(const ExprRef& expr): ExtendableBv{expr, EXT_ZERO} {}
+
+ /// \brief Constructs an ExtendableBv from a bitvector expr.
+ /// \param[in] expr The ILA expression to extend as needed.
+ /// \param[in] ext_mode How the expression should be extended.
+ explicit ExtendableBv(const ExprRef& expr, ExtMode ext_mode)
+ : expr{expr}, ext_mode{ext_mode} {}
+
+ /// Default destructor.
+ ~ExtendableBv()=default;
+
+ /// \brief Extends the wrapped bitvector expression to match the given expr.
+ /// \param[in] other The ILA expression whose bitwidth to match.
+ ExprRef extend_to(const ExprRef& other) const;
+ };
+
+ /// \brief Valid types for the RHS of an update.
+ using AssignmentExpr = std::variant;
+
+ /// \brief A list of variables and what they should be updated to.
+ using VarMap = std::vector>;
+
+ /// forward declarations
+ struct Assert;
+ struct Assume;
+ struct Call;
+ struct Update;
+ struct While;
+ struct Block;
+
+ /// \brief A statement within a program fragment.
+ using Stmt = std::variant;
+
+ /// \brief A sequence of statements.
+ struct Block : public std::vector {
+ using base=std::vector;
+ using base::base;
+ using base::operator=;
+ };
+
+ /// \brief An assertion that a given constraint holds at a given
+ /// location of a program fragment.
+ /// Will be checked once encoded for and sent to a solver.
+ struct Assert {
+ Constraint assertion; // The constraint that must hold.
+ };
+
+ /// \brief An assumption that a given constraint holds at a given
+ /// location of a program fragment.
+ struct Assume {
+ Constraint assumption; // The constraint assumed to hold.
+ };
+
+ /// \brief "Calls" the given instruction with the given inputs.
+ /// Assumes the decode of the given instruction holds.
+ struct Call {
+ InstrRef instr; // The instruction to call.
+ VarMap inputs {}; // Assignments to the inputs of instr's ILA.
+ };
+
+ /// \brief Updates the given variables using the expressions they
+ /// are mapped to.
+ struct Update: public VarMap {
+ using base=VarMap;
+ using base::base;
+ using base::operator=;
+ };
+
+ /// \brief A while loop. Repeatedly executes the body while the
+ /// given loop condition holds.
+ struct While {
+ Constraint loop_condition; // The loop condition
+ /// An invariant on the loop provided to help verification.
+ /// The invariant is asserted before the loop and at the end
+ /// of the loop body, and assumed at the start of the loop
+ /// body and after the loop ends.
+ Constraint invariant;
+ Block body; // The body of the loop
+
+ /// \brief Constructs a While loop given a loop condition and body.
+ /// \param[in] loop_condition The loop condition.
+ /// \param[in] body The loop body.
+ While(const Constraint& loop_condition, const Block& body);
+ /// \brief Constructs a While loop given a loop condition and body.
+ /// \param[in] loop_condition The loop condition.
+ /// \param[in] invariant An invariant on the loop provided
+ /// to help verification.
+ /// The invariant is asserted before the loop and at the end
+ /// of the loop body, and assumed at the start of the loop
+ /// body and after the loop ends.
+ /// \param[in] body The loop body.
+ While(const Constraint& loop_condition,
+ const Constraint& invariant, const Block& body);
+ };
+
+ /// \brief A program using an ILA.
+ class ProgramFragment {
+
+ friend bool operator==(const ProgramFragment& a, const ProgramFragment& b);
+ friend std::ostream& operator<<(std::ostream& out, const ProgramFragment& pf);
+
+ public:
+ /// Pointer to the internal representation of a program fragment.
+ using PfragPtr = std::shared_ptr;
+ /// Pointer to the internal representation of a program fragment.
+ using PfragConstPtr = std::shared_ptr;
+
+ /// Constructs an empty program fragment.
+ ProgramFragment();
+
+ /// Constructs a program fragment consisting of the given block.
+ ProgramFragment(const Block& b);
+
+ /// Destroys a program fragment
+ ~ProgramFragment()=default;
+
+ /// TODO: these aren't parameters, they are helper variables
+
+ /// Creates a new boolean variable and registers it as a parameter
+ ExprRef NewBoolVar(const std::string& name);
+
+ /// Creates a new bitvector variable and registers it as a parameter
+ ExprRef NewBvVar(const std::string& name, const int& bitwidth);
+
+ /// Creates a new bitvector variable and registers it as a parameter
+ ExprRef NewMemVar(const std::string& name,
+ const int& addrwidth, const int& datawidth);
+
+ /// Returns the number of parameters registered
+ size_t num_params();
+
+ /// Returns the nth registered parameter
+ ExprRef param(size_t n);
+
+ /// Returns registered parameter with the given name
+ ExprRef param(const std::string& name);
+
+ /// Returns the body of the program fragment
+ Block body();
+
+ /// Registers the given parameter in this program fragment
+ void RegisterParam(const ExprRef& p);
+
+ /// Adds the given statement to the program fragment
+ void AddStatement(const Stmt& s);
+
+ /// Adds the given block of statements to the program fragment
+ void AddStatements(const Block& b);
+
+ /// Returns the internal representation of the program fragment
+ PfragConstPtr get() const;
+
+ private:
+ PfragPtr pf_;
+ Block body_;
+ };
+
+ /// Checks structural equality
+ bool operator==(const ProgramFragment& a, const ProgramFragment& b);
+
+ /// Prints a program fragment
+ std::ostream& operator<<(std::ostream& out, const ProgramFragment& pf);
+
+} // namespace programfragment
+
+
+/// An enum representing the result of verifying the system of CHCs
+enum class ChcResult: char {
+ valid=z3::unsat,
+ invalid=z3::sat,
+ unknown=z3::unknown
+};
+
+std::ostream& operator<<(std::ostream& out, const ChcResult& r);
+
+/// Encodes a program fragment on an ILA into a CHC
+class IlaToChcEncoder {
+ public:
+ // TODO: move parameter registration in program fragments to
+ // internal representation, rename IlaToChcEncoder to PfToChcIncoder,
+ // and remove the Ila argument.
+
+ /// Constructs an IlaToChcEncoder
+ IlaToChcEncoder(
+ z3::context& ctx, z3::fixedpoint& ctxfp,
+ const Ila& ila, const programfragment::ProgramFragment& pf);
+
+ /// Destructor
+ ~IlaToChcEncoder()=default;
+
+ /// Returns the set of variables read or written by a program fragment
+ std::vector scope() const;
+
+ /// Gives the system of CHCs as a string
+ std::string to_string();
+
+ /// Checks the assertion of the system of CHCs
+ ChcResult check_assertions();
+
+ private:
+ std::shared_ptr impl_;
+};
+
+
} // namespace ilang
#endif // ILANG_ILANG_CPP_H__
diff --git a/include/ilang/target-smt/lia_cvtr.h b/include/ilang/target-smt/lia_cvtr.h
new file mode 100644
index 000000000..913a92f63
--- /dev/null
+++ b/include/ilang/target-smt/lia_cvtr.h
@@ -0,0 +1,63 @@
+/// \file
+/// Class LiaCvtr - the converter for linear integer arithmetic SMT expressions.
+
+#ifndef ILANG_TARGET_SMT_LIA_CVTR_H__
+#define ILANG_TARGET_SMT_LIA_CVTR_H__
+
+#ifdef SMTSWITCH_INTERFACE
+
+#include
+#include
+
+#include
+
+#include
+#include
+
+/// \namepsace ilang
+namespace ilang {
+
+class LiaCvtr : public SmtSwitchItf {
+public:
+ // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
+ /// Default constructor.
+ LiaCvtr(smt::SmtSolver& solver);
+ /// Default destructor.
+ ~LiaCvtr();
+
+private:
+ /// Type for cacheing the generated expressions.
+ typedef std::unordered_map ExprTermMap;
+ /// Type for cacheing the generated functions.
+ typedef std::unordered_map FuncTermMap;
+
+ // ------------------------- MEMBERS -------------------------------------- //
+ /// The underlying SMT solver.
+ smt::SmtSolver& solver_;
+ /// Container for cacheing expression Terms.
+ ExprTermMap expr_map_;
+ /// Container for cacheing function Terms.
+ FuncTermMap func_map_;
+ /// Name suffix for each expression generation (e.g., time step).
+ std::string suffix_ = "";
+
+ // ------------------------- HELPERS -------------------------------------- //
+ /// Make Term of expr variable.
+ smt::Term ExprVar2Term(const ExprPtr& expr);
+ /// Make Term of expr constant.
+ smt::Term ExprConst2Term(const ExprPtr& expr);
+ /// Make Term of expr operator.
+ smt::Term ExprOp2Term(const ExprPtr& expr, const smt::TermVec& arg_terms);
+ /// Make Term of func.
+ smt::Term Func2Term(const FuncPtr& func);
+ /// Make smt::Sort of ilang::SortPtr.
+ smt::Sort IlaSort2LiaSort(const SortPtr& s);
+
+}; // class LiaCvtr
+
+} // namespace ilang
+
+#endif // SMTSWITCH_INTERFACE
+
+#endif // ILANG_TARGET_SMT_LIA_CVTR_H__
+
diff --git a/include/ilang/target-smt/smt_switch_itf.h b/include/ilang/target-smt/smt_switch_itf.h
index e7e317b69..8ceee1670 100644
--- a/include/ilang/target-smt/smt_switch_itf.h
+++ b/include/ilang/target-smt/smt_switch_itf.h
@@ -1,8 +1,8 @@
/// \file
/// Class SmtSwitchItf - the interface to external library smt-switch.
-#ifndef ILANG_ILA_MNGR_U_SMT_SWITCH_H__
-#define ILANG_ILA_MNGR_U_SMT_SWITCH_H__
+#ifndef ILANG_TARGET_SMT_SMT_SWITCH_H__
+#define ILANG_TARGET_SMT_SMT_SWITCH_H__
#ifdef SMTSWITCH_INTERFACE
@@ -74,15 +74,16 @@ class SmtSwitchItf {
/// Insert the SMT Term of the given node into the map.
void PopulateExprMap(const ExprPtr& expr);
/// Make Term of expr variable.
- smt::Term ExprVar2Term(const ExprPtr& expr);
+ virtual smt::Term ExprVar2Term(const ExprPtr& expr);
/// Make Term of expr constant.
- smt::Term ExprConst2Term(const ExprPtr& expr);
+ virtual smt::Term ExprConst2Term(const ExprPtr& expr);
/// Make Term of expr operator.
- smt::Term ExprOp2Term(const ExprPtr& expr, const smt::TermVec& arg_terms);
+ virtual smt::Term ExprOp2Term(const ExprPtr& expr,
+ const smt::TermVec& arg_terms);
/// Make Term of func.
- smt::Term Func2Term(const FuncPtr& func);
+ virtual smt::Term Func2Term(const FuncPtr& func);
/// Make smt::Sort of ilang::SortPtr.
- smt::Sort IlaSort2SmtSort(const SortPtr& s);
+ virtual smt::Sort IlaSort2SmtSort(const SortPtr& s);
}; // class SmtSwitchItf
@@ -90,5 +91,5 @@ class SmtSwitchItf {
#endif // SMTSWITCH_INTERFACE
-#endif // ILANG_ILA_MNGR_U_SMT_SWITCH_H__
+#endif // ILANG_TARGET_SMT_SMT_SWITCH_H__
diff --git a/scripts/setup-smtswitch.sh b/scripts/setup-smtswitch.sh
new file mode 100644
index 000000000..d14dcd361
--- /dev/null
+++ b/scripts/setup-smtswitch.sh
@@ -0,0 +1,68 @@
+#!/bin/sh
+
+# ==============================================================================
+# MIT License
+#
+# Copyright (c) 2019 Princeton University
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+# ==============================================================================
+
+SRC_DIR=$1
+DEP_DIR=$2
+SMTSWITCH_VERSION=768ed5d05315d0b652a915adcfbbc7f3e7a4896a
+Z3_VERSION=tags/z3-4.8.12
+BTOR_VERSION=tags/3.2.2
+
+# fetch smt-switch
+cd $SRC_DIR
+git clone https://github.com/stanford-centaur/smt-switch.git
+cd smt-switch
+git checkout $SMTSWITCH_VERSION
+mkdir -p deps
+
+# fetch/build/install z3
+cd $SRC_DIR/smt-switch/deps
+git clone https://github.com/Z3Prover/z3.git
+cd z3
+git checkout $Z3_VERSION
+python3 scripts/mk_make.py --staticlib --single-threaded --prefix=$DEP_DIR
+cd build
+make -j$(nproc)
+make install
+
+#fetch/build boolector
+cd $SRC_DIR/smt-switch/deps
+git clone https://github.com/Boolector/boolector.git
+cd boolector
+git checkout $BTOR_VERSION
+./contrib/setup-btor2tools.sh
+./contrib/setup-cadical.sh
+mkdir -p build
+cd build
+cmake .. -DONLY_CADICAL=ON -DCMAKE_POSITION_INDEPENDENT_CODE=ON
+make -j$(nproc)
+
+#build/install smt-switch
+cd $SRC_DIR/smt-switch
+mkdir -p build
+./configure.sh --static --btor --z3 --prefix=$DEP_DIR
+cd build
+make -j$(nproc)
+make install
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index b80acf95a..fac02aa63 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -206,6 +206,10 @@ if(${ILANG_BUILD_SWITCH})
target_link_libraries(${ILANG_LIB_NAME} PUBLIC smt-switch::smt-switch)
target_compile_definitions(${ILANG_LIB_NAME} PUBLIC SMTSWITCH_INTERFACE)
+ find_package(Threads REQUIRED)
+ target_link_libraries(${ILANG_LIB_NAME} PUBLIC gmp)
+ target_link_libraries(${ILANG_LIB_NAME} PUBLIC Threads::Threads)
+
if(${SMTSWITCH_BTOR_FOUND})
target_link_libraries(${ILANG_LIB_NAME} PUBLIC smt-switch::smt-switch-btor)
endif()
@@ -222,6 +226,11 @@ if(${ILANG_BUILD_SWITCH})
target_link_libraries(${ILANG_LIB_NAME} PUBLIC smt-switch::smt-switch-yices2)
endif()
+ if(${SMTSWITCH_Z3_FOUND})
+ target_link_libraries(${ILANG_LIB_NAME} PUBLIC smt-switch::smt-switch-z3)
+ target_link_libraries(smt-switch::smt-switch-z3 INTERFACE gmp)
+ endif()
+
endif()
##
diff --git a/src/ila-mngr/CMakeLists.txt b/src/ila-mngr/CMakeLists.txt
index 8c8cd824c..47aa1716a 100644
--- a/src/ila-mngr/CMakeLists.txt
+++ b/src/ila-mngr/CMakeLists.txt
@@ -11,11 +11,13 @@ target_sources(${ILANG_LIB_NAME} PRIVATE
${CMAKE_CURRENT_SOURCE_DIR}/p_simplify_semantic.cc
${CMAKE_CURRENT_SOURCE_DIR}/p_simplify_syntactic.cc
${CMAKE_CURRENT_SOURCE_DIR}/u_abs_knob.cc
+ ${CMAKE_CURRENT_SOURCE_DIR}/u_progfrag.cc
${CMAKE_CURRENT_SOURCE_DIR}/u_rewrite_expr.cc
${CMAKE_CURRENT_SOURCE_DIR}/u_rewrite_ila.cc
${CMAKE_CURRENT_SOURCE_DIR}/u_unroller.cc
${CMAKE_CURRENT_SOURCE_DIR}/u_unroller_smt.cc
- ${CMAKE_CURRENT_SOURCE_DIR}/v_eq_check_crr.cc
${CMAKE_CURRENT_SOURCE_DIR}/v_eq_check_bmc.cc
+ ${CMAKE_CURRENT_SOURCE_DIR}/v_eq_check_crr.cc
+ ${CMAKE_CURRENT_SOURCE_DIR}/v_eq_check_pfrag.cc
${CMAKE_CURRENT_SOURCE_DIR}/v_refinement.cc
)
diff --git a/src/ila-mngr/u_progfrag.cc b/src/ila-mngr/u_progfrag.cc
new file mode 100644
index 000000000..6abf7f40a
--- /dev/null
+++ b/src/ila-mngr/u_progfrag.cc
@@ -0,0 +1,115 @@
+/// \file
+/// Utilities for handling program fragments
+
+#include
+
+#include
+
+#include
+
+namespace ilang {
+
+namespace pfast {
+
+ bool operator==(const ProgramFragment& a, const ProgramFragment& b) {
+ // [TODO] check == operator on unordered sets
+ return (a.params == b.params) && (a.body == b.body);
+ }
+
+ std::string to_string(const Stmt& s) {
+ PrettyPrinter pp {};
+ std::visit(pp, s);
+ return pp.str();
+ }
+
+ std::string to_string(const ProgramFragment& pf) {
+ PrettyPrinter pp {};
+ pp(pf);
+ return pp.str();
+ }
+
+ std::ostream& operator<<(std::ostream& out, const ProgramFragment& pf) {
+ return (out << to_string(pf));
+ }
+
+ // std::string to_string(const Block& b) {
+ // PrettyPrinter pp {};
+ // pp(b);
+ // return pp.str();
+ // }
+
+ void PrettyPrinter::operator()(const ProgramFragment& pf) {
+ buf_ << reserved_word("main") << "(";
+ bool first = true;
+ for (const auto& param : pf.params) {
+ if (first) first = false;
+ else buf_ << ", ";
+ buf_ << param;
+ }
+ buf_ << ") ";
+
+ this->indent_ = 0;
+ (*this)(pf.body);
+
+ buf_ << "\n";
+ }
+
+ void PrettyPrinter::operator()(const Block& b) {
+ buf_ << "{\n";
+ this->indent_ += 2;
+ for (int i = 0; i != b.size(); ++i) {
+ buf_ << indent_str();
+ std::visit(*this, b[i]);
+ buf_ << "\n";
+ }
+ this->indent_ -= 2;
+ buf_ << indent_str() << "}";
+ }
+
+ void PrettyPrinter::operator()(const Assert& a) {
+ buf_ << reserved_word("assert") << " ";
+ a.assertion->PrintPretty(buf_);
+ }
+
+ void PrettyPrinter::operator()(const Assume& a) {
+ buf_ << reserved_word("assume") << " ";
+ a.assumption->PrintPretty(buf_);
+ }
+
+ void PrettyPrinter::operator()(const Call& c) {
+ buf_ << reserved_word("call") << " " << c.instr->name().str();
+ if (c.input_constraint) {
+ buf_ << " where ";
+ c.input_constraint->PrintPretty(buf_);
+ }
+ }
+
+ void PrettyPrinter::operator()(const Update& u) {
+ buf_ << reserved_word("update");
+ bool first = true;
+ for (const auto& [x, v] : u) {
+ buf_ << (first ? " " : ", ")
+ << x << " = ";
+ v->PrintPretty(buf_);
+ first = false;
+ }
+ }
+
+ void PrettyPrinter::operator()(const While& w) {
+ buf_ << reserved_word("while") << " ";
+ w.loop_condition->PrintPretty(buf_);
+ buf_ << " ";
+ (*this)(w.body);
+ }
+
+ std::string PrettyPrinter::reserved_word(const std::string& word) {
+ std::string res = word;
+ for (auto & c: res) c = toupper(c);
+ return res;
+ }
+
+ std::string PrettyPrinter::indent_str() { return std::string(this->indent_, ' '); }
+
+}
+
+}
\ No newline at end of file
diff --git a/src/ila-mngr/v_eq_check_pfrag.cc b/src/ila-mngr/v_eq_check_pfrag.cc
new file mode 100644
index 000000000..95a311012
--- /dev/null
+++ b/src/ila-mngr/v_eq_check_pfrag.cc
@@ -0,0 +1,310 @@
+/// \file
+/// Program fragment-based verification checking driver.
+
+#include
+
+#include
+
+#include
+#include
+
+namespace ilang {
+
+template struct dependent_false : std::false_type {};
+
+namespace pgraph {
+
+ using namespace pfast;
+
+ struct PGraphBuilder {
+
+ CutpointGraph get_pg() { return pg_; }
+
+ void operator()(const ProgramFragment& pf) {
+ (*this)(pf.body);
+ running_seq_to_newloc(pgraph::LOC_END);
+ }
+
+ void operator()(const Block& b) {
+ for (const Stmt& s : b) std::visit(*this, s);
+ }
+
+ void operator()(const Call& c) {
+ running_seq_.emplace_back(c);
+ }
+
+ void operator()(const Assume& a) {
+ running_seq_.emplace_back(a);
+ }
+
+ void operator()(const Assert& a) {
+ running_seq_.emplace_back(pfast::Assume{asthub::Not(a.assertion)});
+ add_edge_from_curloc(running_seq_, LOC_ERROR);
+ running_seq_.pop_back();
+ running_seq_.emplace_back(Assume{a.assertion});
+ }
+
+ void operator()(const Update& u) {
+ running_seq_.emplace_back(u);
+ }
+
+ void operator()(const While& w) {
+ running_seq_to_newloc("while");
+ Location loop_start = curloc();
+ running_seq_.emplace_back(Assume{w.loop_condition});
+ (*this)(w.body); // visit loop body
+ running_seq_to_loc(loop_start); // connect loop body to loop start
+ // continue after loop
+ running_seq_.emplace_back(Assume{asthub::Not(w.loop_condition)});
+ }
+
+ private:
+
+ CutpointGraph pg_ {};
+ StmtSeq running_seq_ {};
+ int loc_ctr_ {0};
+ Location curloc_ {LOC_BEGIN};
+
+ void running_seq_to_loc(const Location& next) {
+ add_edge_from_curloc(running_seq_, next);
+ set_curloc(next);
+ running_seq_.clear();
+ }
+
+ void running_seq_to_newloc(const std::string& loc_ident) {
+ running_seq_to_loc(newloc(loc_ident));
+ }
+
+ void add_edge_from_curloc(const Edge& edge, const Location& loc) {
+ Location cur = curloc();
+ pg_.try_emplace(cur); // creates an Edges object at pg[cur] if none exists
+ EdgeTo new_edge {edge, loc};
+ pg_[cur].push_back(new_edge);
+ }
+
+ Location curloc() { return curloc_; }
+ void set_curloc(const Location& loc) { curloc_ = loc; }
+
+ Location newloc(const std::string& loc_ident) {
+ return "loc" + std::to_string(loc_ctr_++) + "_" + loc_ident;
+ }
+
+ };
+
+ CutpointGraph program_graph(const pfast::ProgramFragment& pf) {
+ PGraphBuilder builder {};
+ builder(pf);
+ return builder.get_pg();
+ }
+
+}
+
+template
+class PathUnrollerCustomDecidingVars: public PathUnroller {
+
+public:
+ PathUnrollerCustomDecidingVars(
+ SmtShim& smt_shim, const ExprPtrVec& deciding_vars,
+ const std::string& suffix = ""):
+ PathUnroller(smt_shim, suffix), custom_deciding_vars_ {deciding_vars} {}
+
+ ~PathUnrollerCustomDecidingVars()=default;
+
+protected:
+ void SetDecidingVars() { this->deciding_vars_ = custom_deciding_vars_; }
+
+private:
+ const ExprPtrVec custom_deciding_vars_;
+};
+
+
+PFToCHCEncoder::PFToCHCEncoder(
+ z3::context& ctx, z3::fixedpoint& ctxfp,
+ const InstrLvlAbsPtr& ila, const pfast::ProgramFragment& pf
+ ): PFToCHCEncoder(ctx, ctxfp, ila, pgraph::program_graph(pf), pf.params) {}
+
+PFToCHCEncoder::PFToCHCEncoder(
+ z3::context& ctx, z3::fixedpoint& ctxfp,
+ const InstrLvlAbsPtr& ila, const pgraph::CutpointGraph& pg, const ExprSet& params
+ ): ctx_{ctx}, ctxfp_{ctxfp}, ila_ {ila}, pg_ {pg}, params_ {params} {
+
+ // z3::params p {ctx_};
+ // p.set("engine", "spacer");
+ // ctxfp_.set(p);
+
+ total_scope_ = params_; // initialize total_scope_, will add more in record_scopes
+ record_scopes(pg_, params_);
+ encode();
+}
+
+
+std::string PFToCHCEncoder::to_string() {
+ z3::func_decl_vector queries = get_error_queries();
+ std::stringstream encoding;
+ encoding << ctxfp_.to_string();
+ for (const z3::func_decl& f : queries) {
+ encoding << "(query " << f.name() << ")\n";
+ }
+ return encoding.str();
+}
+
+
+void PFToCHCEncoder::encode() {
+ Z3ExprAdapter z3_adapter {ctx_};
+
+ for (const auto& [loc, edges] : pg_) {
+ for (const auto& [edge, next] : edges) {
+ encode_transition(loc, edge, next);
+ }
+ }
+}
+
+void PFToCHCEncoder::encode_transition(
+ const pgraph::Location& start,
+ const pgraph::StmtSeq& transition,
+ const pgraph::Location& end) {
+
+ Z3ExprAdapter z3_adapter {ctx_};
+ SmtShim smt_solver {z3_adapter};
+ PathUnrollerCustomDecidingVars unroller {smt_solver, pred_scope_};
+
+ InstrVec seq {};
+ int step_ctr = 0;
+
+ if (start != pgraph::LOC_BEGIN) {
+ unroller.AssertStep(get_or_make_loc_predicate(start), 0);
+ }
+
+ for (auto& stmt : transition) {
+ std::visit([&unroller, &seq, &step_ctr](const auto& s) {
+ using T = std::decay_t;
+
+ if constexpr (std::is_same_v) {
+ unroller.AssertStep(s.assumption, step_ctr);
+
+ } else if constexpr (std::is_same_v) {
+ seq.push_back(s.instr);
+ if (s.input_constraint) unroller.AssertStep(s.input_constraint, step_ctr);
+ ++step_ctr;
+
+ } else if constexpr (std::is_same_v) {
+ // [HACK] convert the update into an instruction
+ auto instr = Instr::New("update_at_" + std::to_string(step_ctr));
+ instr->set_decode(asthub::BoolConst(true));
+ for (const auto& [x, v] : s) {
+ instr->set_update(x, v);
+ }
+ seq.push_back(instr);
+ ++step_ctr;
+ } else {
+ // raise compile-time error
+ static_assert(
+ dependent_false::value,
+ "encode_transition not implemented for given type of BasicStmt."
+ );
+ }
+ }, stmt);
+ }
+
+ z3::expr_vector forall_args {ctx_};
+ for (int i = 0; i != step_ctr + 1; ++i) {
+ for (const auto& v : total_scope_) {
+ forall_args.push_back(unroller.GetSmtCurrent(v, i));
+ }
+ }
+
+ z3::expr_vector body {ctx_};
+
+ body.push_back(unroller.Unroll(seq));
+ auto dvs = unroller.GetLastDecidingVars();
+ ExprSet deciding_vars {dvs.begin(), dvs.end()};
+
+ for (const auto& v : get_scope(end)) {
+ auto end_pred_v = smt_solver.GetShimExpr(v, PRED_END_SUFFIX);
+
+ forall_args.push_back(end_pred_v);
+
+ int last_v_step = (deciding_vars.find(v) == deciding_vars.end()) ? 0 : step_ctr;
+ auto last_v_update = unroller.GetSmtCurrent(v, last_v_step);
+ body.push_back(smt_solver.Equal(last_v_update, end_pred_v));
+ }
+
+ ExprPtr end_pred = get_or_make_loc_predicate(end);
+
+ z3::expr rule = z3::forall(forall_args, z3::implies(
+ z3::mk_and(body), smt_solver.GetShimExpr(end_pred, PRED_END_SUFFIX)
+ ));
+
+ ctxfp_.add_rule(rule, ctx_.str_symbol((start + "_to_" + end).c_str()));
+}
+
+void PFToCHCEncoder::record_scopes(const pgraph::CutpointGraph& pg, const ExprSet& params) {
+ ExprSet uvars {params};
+ for (const auto& [loc, edges] : pg) {
+ for (const auto& edgeTo : edges) {
+ for (const auto& stmt : edgeTo.edge) {
+ add_unique_vars(stmt, uvars, total_scope_);
+ }
+ }
+ }
+
+ pred_scope_ = {uvars.begin(), uvars.end()};
+}
+
+void PFToCHCEncoder::add_unique_vars(
+ const pgraph::BasicStmt& s, ExprSet& pred_scope, ExprSet& total_scope
+) {
+ std::visit([&pred_scope, &total_scope](const auto& s) {
+ using T = std::decay_t;
+ if constexpr (std::is_same_v) {
+ // Assume should only use known variables.
+ // OLD: absknob::InsertVar(s.assumption, scope);
+ } else if constexpr (std::is_same_v) {
+ // add ILA state variables to the scope
+ absknob::InsertStt(s.instr->host(), pred_scope);
+ absknob::InsertVar(s.instr->host(), total_scope);
+ // we do not include the state of children unless an instruction
+ // of the child is called.
+ // Also, the constraint should not use any new variables.
+ } else if constexpr (std::is_same_v) {
+ // Update should only use known variables.
+ } else {
+ // compile-time error
+ static_assert(
+ dependent_false::value,
+ "record_scopes not implemented for given type of BasicStmt."
+ );
+ }
+ }, s);
+}
+
+ExprPtr PFToCHCEncoder::get_or_make_loc_predicate(const pgraph::Location& loc) {
+ auto res = loc_predicates_.find(loc);
+ if (res != loc_predicates_.end()) return res->second;
+ loc_predicates_[loc] = new_predicate(loc, get_scope(loc));
+ return loc_predicates_[loc];
+}
+
+ExprPtr PFToCHCEncoder::new_predicate(const std::string& name, const ExprPtrVec& args) {
+ std::vector arg_sorts;
+ for (const auto& e : args) {
+ arg_sorts.push_back(e->sort());
+ }
+ FuncPtr f = Func::New(name, Sort::MakeBoolSort(), arg_sorts);
+ z3::func_decl fd = f->GetZ3FuncDecl(ctx_);
+ ctxfp_.register_relation(fd);
+ return asthub::AppFunc(f, args);
+}
+
+z3::func_decl_vector PFToCHCEncoder::get_error_queries() {
+ z3::func_decl_vector queries {ctx_};
+
+ ExprPtr p = get_or_make_loc_predicate(pgraph::LOC_ERROR);
+ queries.push_back(
+ std::dynamic_pointer_cast(p)
+ ->func()->GetZ3FuncDecl(ctx_));
+
+ return queries;
+}
+
+}
\ No newline at end of file
diff --git a/src/ila/ast/expr_const.cc b/src/ila/ast/expr_const.cc
index 5885276e8..9a23ae397 100644
--- a/src/ila/ast/expr_const.cc
+++ b/src/ila/ast/expr_const.cc
@@ -86,6 +86,10 @@ std::ostream& ExprConst::Print(std::ostream& out) const {
}
}
+std::ostream& ExprConst::PrintPretty(std::ostream& out) const {
+ return Print(out);
+}
+
BoolValPtr ExprConst::val_bool() const {
ILA_ASSERT(is_bool()) << "Not boolean constant";
return std::static_pointer_cast(val_);
diff --git a/src/ila/ast/expr_op.cc b/src/ila/ast/expr_op.cc
index 927a4c3a7..2d6e9f04e 100644
--- a/src/ila/ast/expr_op.cc
+++ b/src/ila/ast/expr_op.cc
@@ -112,6 +112,15 @@ std::ostream& ExprOp::Print(std::ostream& out) const {
return out << name().format_str(op_name(), "");
}
+std::ostream& ExprOp::PrintPretty(std::ostream& out) const {
+ out << "(" << op_name();
+ for (size_t i = 0; i != arg_num(); ++i) {
+ out << " ";
+ arg(i)->PrintPretty(out);
+ }
+ return out << ")";
+}
+
SortPtr ExprOp::GetSortBinaryOperation(const ExprPtr& e0, const ExprPtr& e1) {
auto s0 = e0->sort();
auto s1 = e1->sort();
diff --git a/src/ila/ast/expr_var.cc b/src/ila/ast/expr_var.cc
index c53d93e44..7863362d2 100644
--- a/src/ila/ast/expr_var.cc
+++ b/src/ila/ast/expr_var.cc
@@ -44,6 +44,10 @@ std::ostream& ExprVar::Print(std::ostream& out) const {
}
}
+std::ostream& ExprVar::PrintPretty(std::ostream& out) const {
+ return Print(out);
+}
+
std::ostream& ExprVar::PrintBool(std::ostream& out) const {
return out << name();
}
diff --git a/src/ilang++.cc b/src/ilang++.cc
index 6091c964e..6297d026f 100644
--- a/src/ilang++.cc
+++ b/src/ilang++.cc
@@ -7,6 +7,8 @@
#include
#include
#include
+#include
+#include
#include
#include
#include
@@ -840,6 +842,209 @@ z3::func_decl IlaZ3Unroller::GetZ3FuncDecl(const FuncRef& f) const {
return univ_->GetZ3FuncDecl(f.get());
}
+namespace programfragment {
+
+ template struct dependent_false : std::false_type {};
+
+ ExprRef ExtendableBv::extend_to(const ExprRef& other) const {
+ int diff = expr.bit_width() - other.bit_width();
+ if (diff == 0) return expr;
+ switch (ext_mode) {
+ case EXT_ZERO: return ZExt(expr, other.bit_width());
+ case EXT_SIGNED: return SExt(expr, other.bit_width());
+ }
+ return expr;
+ }
+
+ ExprRef try_ext(const AssignmentExpr& expr, const ExprRef& target) {
+ return std::visit([&target](const auto& to_ext) {
+ using T = std::decay_t;
+ if constexpr (std::is_same_v) return to_ext;
+ else if constexpr (std::is_same_v) {
+ return BvConst(to_ext, target.bit_width());
+ } else if constexpr (std::is_same_v) {
+ return to_ext.extend_to(target);
+ } else {
+ // raise compile-time error
+ static_assert(
+ dependent_false::value,
+ "try_ext not implemented for given variant of AssignmentExpr"
+ );
+ }
+ }, expr);
+ }
+
+ pfast::Stmt convert_stmt(const Stmt& s);
+
+ pfast::Block convert_block(const Block& b) {
+ pfast::Block converted;
+ for (const auto& s : b) {
+ converted.push_back(convert_stmt(s));
+ }
+ return converted;
+ }
+
+ pfast::Stmt convert_stmt(const Stmt& s) {
+ return std::visit([](const auto& s) -> pfast::Stmt {
+ using T = std::decay_t;
+
+ if constexpr (std::is_same_v) {
+ return pfast::Assert{s.assertion.get()};
+
+ } else if constexpr (std::is_same_v) {
+ return pfast::Assume{s.assumption.get()};
+
+ } else if constexpr (std::is_same_v) {
+ ExprRef c = asthub::BoolConst(true);
+ for (const auto& [input, assignment] : s.inputs) {
+ c = c & (input == try_ext(assignment, input));
+ }
+ return pfast::Call{s.instr.get(), c.get()};
+
+ } else if constexpr (std::is_same_v) {
+ pfast::Update u {};
+ for (const auto& [param, update] : s) {
+ u.emplace(param.get(), try_ext(update, param).get());
+ }
+ return u;
+
+ } else if constexpr (std::is_same_v) {
+ pfast::Constraint inv = s.invariant.get();
+ pfast::Block body = convert_block(s.body);
+ if (!bool(inv)) {
+ return pfast::While{s.loop_condition.get(), body};
+ }
+ return pfast::Block{
+ pfast::Assert{inv},
+ pfast::While{s.loop_condition.get(), pfast::Block{
+ pfast::Assume{inv},
+ body,
+ pfast::Assert{inv}
+ }},
+ pfast::Assume{inv}
+ };
+
+ } else if constexpr (std::is_same_v) {
+ return convert_block(s);
+
+ } else {
+ // raise compile-time error
+ static_assert(
+ dependent_false::value,
+ "convert_stmt not implemented for given type of Stmt."
+ );
+ }
+
+ }, s);
+ }
+
+ While::While(const Constraint& loop_condition, const Block& body):
+ While(loop_condition, {nullptr}, body) {}
+
+ While::While(
+ const Constraint& loop_condition, const Constraint& invariant,
+ const Block& body
+ ): loop_condition {loop_condition}, invariant {invariant}, body {body} {}
+
+ ProgramFragment::ProgramFragment(): ProgramFragment(Block{}) {}
+
+ ProgramFragment::ProgramFragment(const Block& b)
+ : pf_ {new pfast::ProgramFragment{{}, convert_block(b)}} {}
+
+ ExprRef ProgramFragment::NewBoolVar(const std::string& name) {
+ ExprRef v {asthub::NewBoolVar(name)};
+ RegisterParam(v);
+ return v;
+ }
+
+ ExprRef ProgramFragment::NewBvVar(const std::string& name, const int& bitwidth) {
+ ExprRef v {asthub::NewBvVar(name, bitwidth)};
+ RegisterParam(v);
+ return v;
+ }
+
+ ExprRef ProgramFragment::NewMemVar(
+ const std::string& name, const int& addrwidth, const int& datawidth) {
+ ExprRef v {asthub::NewMemVar(name, addrwidth, datawidth)};
+ RegisterParam(v);
+ return v;
+ }
+
+ size_t ProgramFragment::num_params() { return pf_->params.size(); }
+
+ ExprRef ProgramFragment::param(size_t n) {
+ return {*std::next(pf_->params.begin(), n)};
+ }
+
+ ExprRef ProgramFragment::param(const std::string& name) {
+ for (const ExprPtr& p : pf_->params) {
+ if (p->name() == name) return {p};
+ }
+ return {nullptr};
+ }
+
+ Block ProgramFragment::body() {
+ return {body_};
+ }
+
+ void ProgramFragment::RegisterParam(const ExprRef& p) {
+ pf_->params.insert(p.get());
+ }
+
+ void ProgramFragment::AddStatement(const Stmt& s) {
+ body_.push_back(s);
+ pf_->body.push_back(convert_stmt(s));
+ }
+
+ void ProgramFragment::AddStatements(const Block& b) {
+ for (auto& s : b) {
+ body_.push_back(s);
+ pf_->body.push_back(convert_stmt(s));
+ }
+ }
+
+ ProgramFragment::PfragConstPtr ProgramFragment::get() const {
+ return pf_;
+ }
+
+ bool operator==(const ProgramFragment& a, const ProgramFragment& b) {
+ return *(a.pf_) == *(b.pf_);
+ }
+
+ std::ostream& operator<<(std::ostream& out, const ProgramFragment& pf) {
+ return (out << *(pf.pf_));
+ }
+
+} // namespace programfragment
+
+std::ostream& operator<<(std::ostream& out, const ChcResult& r) {
+ switch (r) {
+ case ChcResult::valid: return out << "valid";
+ case ChcResult::invalid: return out << "invalid";
+ case ChcResult::unknown: return out << "unknown";
+ }
+ return out;
+}
+
+IlaToChcEncoder::IlaToChcEncoder(
+ z3::context& ctx, z3::fixedpoint& ctxfp,
+ const Ila& ila, const programfragment::ProgramFragment& pf
+): impl_ {std::make_shared(
+ ctx, ctxfp, ila.get(), *(pf.get())
+ )} {}
+
+std::vector IlaToChcEncoder::scope() const {
+ std::vector vars;
+ for (const auto& v : impl_->scope()) vars.emplace_back(v);
+ return vars;
+}
+
+std::string IlaToChcEncoder::to_string() { return impl_->to_string(); }
+
+ChcResult IlaToChcEncoder::check_assertions() {
+ return static_cast(impl_->check_assertions());
+}
+
void LogLevel(const int& lvl) { SetLogLevel(lvl); }
void LogPath(const std::string& path) { SetLogPath(path); }
@@ -860,12 +1065,13 @@ void EnableDebug(const std::string& tag) { DebugLog::Enable(tag); }
void DisableDebug(const std::string& tag) { DebugLog::Disable(tag); }
#ifdef SMTSWITCH_INTERFACE
-smt::Term ResetAndGetSmtTerm(smt::SmtSolver& solver, const ExprRef& expr,
- const std::string& suffix) {
- solver->reset();
+
+smt::Term GetSmtTerm(smt::SmtSolver& solver, const ExprRef& expr,
+ const std::string& suffix) {
auto itf = SmtSwitchItf(solver);
return itf.GetSmtTerm(expr.get(), suffix);
}
+
#endif // SMTSWITCH_INTERFACE
} // namespace ilang
diff --git a/src/target-smt/CMakeLists.txt b/src/target-smt/CMakeLists.txt
index b9781559d..d908b3b0b 100644
--- a/src/target-smt/CMakeLists.txt
+++ b/src/target-smt/CMakeLists.txt
@@ -2,6 +2,7 @@
# source
# ---------------------------------------------------------------------------- #
target_sources(${ILANG_LIB_NAME} PRIVATE
+ ${CMAKE_CURRENT_SOURCE_DIR}/lia_cvtr.cc
${CMAKE_CURRENT_SOURCE_DIR}/smt_switch_itf.cc
${CMAKE_CURRENT_SOURCE_DIR}/z3_expr_adapter.cc
)
diff --git a/src/target-smt/lia_cvtr.cc b/src/target-smt/lia_cvtr.cc
new file mode 100644
index 000000000..e5fa8bba5
--- /dev/null
+++ b/src/target-smt/lia_cvtr.cc
@@ -0,0 +1,270 @@
+/// \file
+/// Source for the LIA converter.
+
+#ifdef SMTSWITCH_INTERFACE
+
+#include
+
+#include
+
+#include
+#include
+#include
+
+namespace ilang {
+
+LiaCvtr::LiaCvtr(smt::SmtSolver& solver)
+ : SmtSwitchItf(solver), solver_(solver) {}
+
+LiaCvtr::~LiaCvtr() {}
+
+smt::Term LiaCvtr::ExprVar2Term(const ExprPtr& expr) {
+ auto prefix = (expr->host()) ? expr->host()->GetRootName() : "";
+ auto e_name = expr->name().format_str(prefix, suffix_);
+
+ auto smt_sort = IlaSort2LiaSort(expr->sort());
+ return solver_->make_symbol(e_name, smt_sort);
+}
+
+smt::Term LiaCvtr::ExprConst2Term(const ExprPtr& expr) {
+ auto expr_const = std::static_pointer_cast(expr);
+
+ switch (auto sort_uid = asthub::GetUidSort(expr); sort_uid) {
+ case AstUidSort::kBool: {
+ return solver_->make_term(expr_const->val_bool()->val());
+ }
+ case AstUidSort::kBv: {
+ return solver_->make_term(expr_const->val_bv()->val(),
+ solver_->make_sort(smt::INT));
+ }
+ default: {
+ ILA_ASSERT(sort_uid == AstUidSort::kMem);
+ auto int_sort = solver_->make_sort(smt::INT);
+ auto mem_sort = solver_->make_sort(smt::ARRAY, int_sort, int_sort);
+
+ // create const memory with default value
+ auto memory_value = expr_const->val_mem();
+ auto def_val_term = solver_->make_term(memory_value->def_val(), int_sort);
+ auto const_memory = solver_->make_term(def_val_term, mem_sort);
+
+ // write in non-default addr-data pairs
+ auto& value_map = memory_value->val_map();
+ for (const auto& p : value_map) {
+ auto addr_term = solver_->make_term(p.first, int_sort);
+ auto data_term = solver_->make_term(p.second, int_sort);
+ auto memory_wr = solver_->make_term(smt::PrimOp::Store, const_memory,
+ addr_term, data_term);
+ const_memory = memory_wr;
+ }
+
+ return const_memory;
+ }
+ }; // switch sort_uid
+}
+
+smt::Term LiaCvtr::ExprOp2Term(const ExprPtr& expr,
+ const smt::TermVec& arg_terms) {
+ // construct based on the operator
+ switch (auto expr_op_uid = asthub::GetUidExprOp(expr); expr_op_uid) {
+ case AstUidExprOp::kNegate: {
+ return solver_->make_term(smt::PrimOp::Negate, arg_terms.at(0));
+ }
+ case AstUidExprOp::kNot: {
+ return solver_->make_term(smt::PrimOp::Not, arg_terms.at(0));
+ }
+#if 0
+ case AstUidExprOp::kComplement: {
+ return solver_->make_term(smt::PrimOp::BVNot, arg_terms.at(0));
+ }
+#endif
+ case AstUidExprOp::kAnd: {
+ ILA_CHECK(expr->is_bool()) << "BVAnd not supported for LIA";
+ return solver_->make_term(smt::PrimOp::And, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kOr: {
+ ILA_CHECK(expr->is_bool()) << "BVOr not supported for LIA";
+ return solver_->make_term(smt::PrimOp::Or, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kXor: {
+ ILA_CHECK(expr->is_bool()) << "BVXor not supported for LIA";
+ return solver_->make_term(smt::PrimOp::Xor, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+#if 0
+ case AstUidExprOp::kShiftLeft: {
+ return solver_->make_term(smt::PrimOp::BVShl, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kArithShiftRight: {
+ return solver_->make_term(smt::PrimOp::BVAshr, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kLogicShiftRight: {
+ return solver_->make_term(smt::PrimOp::BVLshr, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+#endif
+ case AstUidExprOp::kAdd: {
+ return solver_->make_term(smt::PrimOp::Plus, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kSubtract: {
+ return solver_->make_term(smt::PrimOp::Minus, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kDivide: {
+ return solver_->make_term(smt::PrimOp::IntDiv, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+#if 0
+ case AstUidExprOp::kSignedRemainder: {
+ return solver_->make_term(smt::PrimOp::BVSrem, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kUnsignedRemainder: {
+ return solver_->make_term(smt::PrimOp::BVUrem, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+#endif
+ case AstUidExprOp::kSignedModular: {
+ return solver_->make_term(smt::PrimOp::Mod, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kMultiply: {
+ return solver_->make_term(smt::PrimOp::Mult, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kEqual: {
+ return solver_->make_term(smt::PrimOp::Equal, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kLessThan: {
+ return solver_->make_term(smt::PrimOp::Lt, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kGreaterThan: {
+ return solver_->make_term(smt::PrimOp::Gt, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kUnsignedLessThan: {
+ return solver_->make_term(smt::PrimOp::Lt, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kUnsignedGreaterThan: {
+ return solver_->make_term(smt::PrimOp::Gt, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kLoad: {
+ return solver_->make_term(smt::PrimOp::Select, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kStore: {
+ return solver_->make_term(smt::PrimOp::Store, arg_terms.at(0),
+ arg_terms.at(1), arg_terms.at(2));
+ }
+ case AstUidExprOp::kConcatenate: {
+ auto w_exp_v = 1 << expr->arg(1)->sort()->bit_width();
+ auto w_exp_t = solver_->make_term(w_exp_v, solver_->make_sort(smt::INT));
+ auto a0_lsh_w =
+ solver_->make_term(smt::PrimOp::Mult, arg_terms.at(0), w_exp_t);
+ return solver_->make_term(smt::PrimOp::Plus, a0_lsh_w, arg_terms.at(1));
+ }
+#if 0
+ case AstUidExprOp::kExtract: {
+ auto op = smt::Op(smt::PrimOp::Extract, expr->param(0), expr->param(1));
+ return solver_->make_term(op, arg_terms.at(0));
+ }
+#endif
+ case AstUidExprOp::kZeroExtend: {
+ return arg_terms.at(0);
+ }
+ case AstUidExprOp::kSignedExtend: {
+ return arg_terms.at(0);
+ }
+#if 0
+ case AstUidExprOp::kRotateLeft: {
+ auto op = smt::Op(smt::PrimOp::Rotate_Left, expr->param(0));
+ return solver_->make_term(op, arg_terms.at(0));
+ }
+ case AstUidExprOp::kRotateRight: {
+ auto op = smt::Op(smt::PrimOp::Rotate_Right, expr->param(0));
+ return solver_->make_term(op, arg_terms.at(0));
+ }
+#endif
+ case AstUidExprOp::kImply: {
+ return solver_->make_term(smt::PrimOp::Implies, arg_terms.at(0),
+ arg_terms.at(1));
+ }
+ case AstUidExprOp::kIfThenElse: {
+ return solver_->make_term(smt::PrimOp::Ite, arg_terms.at(0),
+ arg_terms.at(1), arg_terms.at(2));
+ }
+ case AstUidExprOp::kApplyFunc: {
+ auto expr_appfunc = std::static_pointer_cast(expr);
+ auto func = expr_appfunc->func();
+
+ // term placeholder for the solver
+ smt::TermVec func_arg_terms;
+
+ // check if the func has been visited
+ auto pos = func_map_.find(func);
+ if (pos != func_map_.end()) {
+ func_arg_terms.push_back(pos->second);
+ } else { // fist visit - create new term
+ auto func_term = Func2Term(func);
+ func_arg_terms.push_back(func_term);
+ func_map_[func] = func_term;
+ }
+
+ // apply func
+ for (auto arg_i : arg_terms) {
+ func_arg_terms.push_back(arg_i);
+ }
+ return solver_->make_term(smt::PrimOp::Apply, func_arg_terms);
+ }
+ default: {
+ ILA_CHECK(false) << "Op " << expr_op_uid << " not supported for LIA (yet)";
+ return solver_->make_term(true);
+ }
+ }; // switch expr_op_uid
+}
+
+smt::Term LiaCvtr::Func2Term(const FuncPtr& func) {
+ // func name (for z3 compatibility)
+ auto prefix = (func->host()) ? func->host()->GetRootName() : "";
+ auto f_name = func->name().format_str(prefix, suffix_);
+
+ // func sort
+ auto arg_sorts = smt::SortVec();
+ for (size_t i = 0; i != func->arg_num(); i++) {
+ arg_sorts.push_back(IlaSort2LiaSort(func->arg(i)));
+ }
+ arg_sorts.push_back(IlaSort2LiaSort(func->out())); // return is the last
+ auto func_sort = solver_->make_sort(smt::FUNCTION, arg_sorts);
+
+ // func term
+ auto func_term = solver_->make_symbol(f_name, func_sort);
+ return func_term;
+}
+
+smt::Sort LiaCvtr::IlaSort2LiaSort(const SortPtr& s) {
+ switch (auto sort_uid = s->uid(); sort_uid) {
+ case AstUidSort::kBool: {
+ return solver_->make_sort(smt::BOOL);
+ }
+ case AstUidSort::kBv: {
+ return solver_->make_sort(smt::INT);
+ }
+ default: {
+ ILA_ASSERT(sort_uid == AstUidSort::kMem);
+ return solver_->make_sort(smt::ARRAY, solver_->make_sort(smt::INT),
+ solver_->make_sort(smt::INT));
+ }
+ }; // switch sort uid
+}
+
+} // namespace ilang
+
+#endif // SMTSWITCH_INTERFACE
diff --git a/src/target-smt/smt_switch_itf.cc b/src/target-smt/smt_switch_itf.cc
index 14be39119..4ae8d8476 100644
--- a/src/target-smt/smt_switch_itf.cc
+++ b/src/target-smt/smt_switch_itf.cc
@@ -331,4 +331,4 @@ smt::Sort SmtSwitchItf::IlaSort2SmtSort(const SortPtr& s) {
} // namespace ilang
-#endif // SMT_SWITCH_INTERFACE
+#endif // SMTSWITCH_INTERFACE
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index b4cad2fff..fe61a9ebf 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -71,10 +71,10 @@ package_add_test(${ILANG_TEST_MAIN}
t_mcm.cc
t_mngr_absknob.cc
t_pass.cc
+ t_pfrag.cc
t_portable.cc
t_smt_in.cc
t_smt_shim.cc
- t_smt_switch_itf.cc
t_smt_trans.cc
t_sort.cc
t_symbol.cc
@@ -108,7 +108,19 @@ endif()
if(${ILANG_BUILD_SWITCH})
find_package(smtswitch REQUIRED)
+ find_package(Threads REQUIRED)
+ target_link_libraries(${ILANG_TEST_MAIN} gmp)
+ target_link_libraries(${ILANG_TEST_MAIN} Threads::Threads)
+
+ if(${SMTSWITCH_Z3_FOUND})
+ target_compile_definitions(${ILANG_TEST_MAIN} PRIVATE SMTSWITCH_Z3)
+ endif()
+
if(${SMTSWITCH_BTOR_FOUND})
+ target_compile_definitions(${ILANG_TEST_MAIN} PRIVATE SMTSWITCH_BTOR)
+ endif()
+
+ if(${SMTSWITCH_Z3_FOUND} OR ${SMTSWITCH_BTOR_FOUND})
target_compile_definitions(${ILANG_TEST_MAIN} PRIVATE SMTSWITCH_TEST)
endif()
endif()
diff --git a/test/t_api.cc b/test/t_api.cc
index e2da6facf..f0621ffb9 100644
--- a/test/t_api.cc
+++ b/test/t_api.cc
@@ -3,6 +3,18 @@
#include
+#ifdef SMTSWITCH_TEST
+#include
+#endif // SMTSWITCH_TEST
+
+#ifdef SMTSWITCH_Z3
+#include
+#endif // SMTSWITCH_Z3
+
+#ifdef SMTSWITCH_BTOR
+#include
+#endif // SMTSWITCH_BTOR
+
#include
#include
@@ -582,6 +594,29 @@ TEST(TestApi, UnrollPathFreeWithFunc) {
EXPECT_EQ(solver.check(), z3::unsat);
}
+TEST(TestApi, GetSmtTerm) {
+ auto m = Ila("M");
+ auto v = m.NewBvState("var", 8);
+ auto p = ((v + 1) - 1) != v;
+
+ auto CheckViaSolver = [&p](smt::SmtSolver& s) {
+ auto term = GetSmtTerm(s, p);
+ s->assert_formula(term);
+ auto res = s->check_sat();
+ EXPECT_TRUE(res.is_unsat());
+ };
+
+#ifdef SMTSWITCH_BTOR
+ auto s_btor = smt::BoolectorSolverFactory::create(false);
+ CheckViaSolver(s_btor);
+#endif // SMTSWITCH_BTOR
+
+#ifdef SMTSWITCH_Z3
+ auto s_z3 = smt::Z3SolverFactory::create(false);
+ CheckViaSolver(s_z3);
+#endif // SMTSWITCH_Z3
+}
+
TEST(TestApi, Portable) {
// SetToStdErr(1);
EnableDebug("Portable");
@@ -599,4 +634,89 @@ TEST(TestApi, Portable) {
DisableDebug("Portable");
}
+TEST(TestApi, Ila2Chc) {
+
+ using namespace programfragment;
+
+ Ila m {"Counter"};
+
+ auto ctr_w = 8;
+
+ auto ctr = m.NewBvState("ctr", ctr_w);
+ auto op = m.NewBvInput("op", 2);
+
+ // increment
+ auto inst_inc = m.NewInstr("inc");
+ inst_inc.SetDecode(op == 0);
+ inst_inc.SetUpdate(ctr, ctr + 1);
+
+ // decrement
+ auto inst_dec = m.NewInstr("dec");
+ inst_dec.SetDecode(op == 1);
+ inst_dec.SetUpdate(ctr, Ite(ctr == 0, BvConst(0, 8), ctr - 1));
+
+ // program fragment
+ ProgramFragment pf {};
+
+ auto x = pf.NewBvVar("x", ctr_w); // asthub::BvConst(3, ctr_w);
+ auto y = pf.NewBvVar("y", ctr_w); // asthub::BvConst(4, ctr_w);
+ auto i = pf.NewBvVar("i", ctr_w);
+ auto j = pf.NewBvVar("j", ctr_w);
+
+ auto inv1 = ((ctr == i * y) & (i <= x));
+ auto inv2 = ((ctr == (i * y + j)) & (j <= y));
+
+ pf.AddStatements({
+ Assume {ctr == 0},
+ Assume {x > 0},
+ Assume {y > 0},
+ Assume {x < 3}, // keeps runtime short
+ Assume {y < 4}, // keeps runtime short
+
+ Update { {i, 0} },
+ Assert { inv1 },
+ While { i < x, {
+ Assume { inv1 },
+ Update { {j, ExtendableBv(BvConst(0, 2))} },
+ Assert { inv2 },
+ While { j < y, {
+ Assume { inv2 },
+ Call { inst_inc },
+ Update { {j, j + 1} },
+ Assert { inv2 }
+ }},
+ Assume { inv2 },
+ Update { {i, i + 1} },
+ Assert { inv1 },
+ }},
+ Assume { inv1 },
+ Assert { ctr == x * y }
+ });
+
+ z3::context ctx;
+ z3::fixedpoint ctxfp {ctx};
+
+ // use spacer instead of datalog
+ z3::params p {ctx};
+ p.set("engine", "spacer");
+ ctxfp.set(p);
+
+ IlaToChcEncoder encoder {ctx, ctxfp, m, pf};
+
+ // std::cout << "\nEncoded successfully!\n" << std::endl;
+
+ // std::cout << encoder.to_string() << std::endl;
+
+ EXPECT_NO_THROW(encoder.to_string());
+
+ ChcResult res = ChcResult::invalid;
+ try {
+ res = encoder.check_assertions();
+ } catch (const z3::exception& e) {
+ std::cout << "Error: " << e << std::endl;
+ }
+
+ EXPECT_EQ(res, ChcResult::valid);
+}
+
} // namespace ilang
diff --git a/test/t_pfrag.cc b/test/t_pfrag.cc
new file mode 100644
index 000000000..c43a5b08a
--- /dev/null
+++ b/test/t_pfrag.cc
@@ -0,0 +1,671 @@
+/// \file
+/// Unit tests for program fragment checker
+
+#include
+#include
+#include
+
+#include "unit-include/config.h"
+#include "unit-include/simple_cpu.h"
+#include "unit-include/util.h"
+
+#define COUNTER_INSTR_INC "INC"
+#define COUNTER_INSTR_DEC "DEC"
+
+#define COUNTER_OP_INC 1
+#define COUNTER_OP_DEC 2
+
+#define COUNTER_STATE_CTR "ctr"
+#define COUNTER_INPUT_OP "op"
+
+namespace ilang {
+
+namespace pf2graph {
+
+ using namespace pfast;
+
+ InstrLvlAbsPtr simple_counter_ila(std::string suffix="") {
+ Ila m {"Counter" + suffix};
+
+ auto ctr = m.NewBvState(COUNTER_STATE_CTR + suffix, 8);
+ auto op = m.NewBvInput(COUNTER_INPUT_OP + suffix, 2);
+
+ { // increment
+ auto instr = m.NewInstr(COUNTER_INSTR_INC + suffix);
+ instr.SetDecode(op == COUNTER_OP_INC);
+ instr.SetUpdate(ctr, ctr + 1);
+ }
+
+ { // decrement
+ auto instr = m.NewInstr(COUNTER_INSTR_DEC + suffix);
+ instr.SetDecode(op == COUNTER_OP_DEC);
+ instr.SetUpdate(ctr, Ite(ctr == 0, BvConst(0, 8), ctr - 1));
+ }
+
+ return m.get();
+ }
+
+ TEST(ProgFrag, StructuralEquality) {
+
+ auto file_dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, "aes");
+ auto ila_file = os_portable_append_dir(file_dir, "aes.json");
+ InstrLvlAbsPtr ila = ImportIlaPortable(ila_file).get();
+
+ ProgramFragment pf {
+ {ila->state("aes_address")},
+ Block{
+ Assume{asthub::Gt(ila->state("aes_key"), 0)},
+ Assume{asthub::Gt(ila->state("aes_key"), 0)},
+ Call{ila->instr("WRITE_ADDRESS")},
+ Call{ila->instr("START_ENCRYPT")},
+ Assert{asthub::Gt(ila->state("aes_key"), 0)},
+ Call{ila->instr("START_ENCRYPT")},
+ Assert{asthub::Gt(ila->state("aes_key"), 0)}
+ }
+ };
+
+ bool cmp_same_fragment = (pf == ProgramFragment{
+ {ila->state("aes_address")},
+ Block{
+ Assume{asthub::Gt(ila->state("aes_key"), 0)},
+ Assume{asthub::Gt(ila->state("aes_key"), 0)},
+ Call{ila->instr("WRITE_ADDRESS")},
+ Call{ila->instr("START_ENCRYPT")},
+ Assert{asthub::Gt(ila->state("aes_key"), 0)},
+ Call{ila->instr("START_ENCRYPT")},
+ Assert{asthub::Gt(ila->state("aes_key"), 0)}
+ }
+ });
+ EXPECT_TRUE(cmp_same_fragment);
+
+ bool cmp_diff_fragment = (pf == ProgramFragment{
+ {ila->state("aes_address")},
+ Block{
+ Assume{asthub::Gt(ila->state("aes_key"), 0)},
+ Call{ila->instr("WRITE_ADDRESS")},
+ Assert{asthub::Gt(ila->state("aes_key"), 0)}
+ }
+ }
+ );
+ EXPECT_FALSE(cmp_diff_fragment);
+ }
+
+ TEST(Pf2chc, Counter) {
+
+ InstrLvlAbsPtr m = simple_counter_ila();
+ auto inst_inc = m->instr(COUNTER_INSTR_INC);
+ auto inst_dec = m->instr(COUNTER_INSTR_DEC);
+
+ auto ctr = m->state(COUNTER_STATE_CTR);
+ auto op = m->input(COUNTER_INPUT_OP);
+
+ auto ctr_w = ctr->sort()->bit_width();
+ auto lowbound = m->NewBvFreeVar("lowbound", ctr_w);
+
+ // program fragment
+ ProgramFragment pf {{ lowbound }, {
+ Assume {asthub::Eq(ctr, 0)},
+ Assume {asthub::Eq(lowbound, 0)},
+ Call {inst_inc},
+ Update {{lowbound, asthub::Add(lowbound, asthub::BvConst(1, ctr_w))}},
+ Assert {asthub::Eq(ctr, 1)},
+ Call {inst_dec},
+ Update {{lowbound, asthub::Sub(lowbound, asthub::BvConst(1, ctr_w))}},
+ Call {inst_dec},
+ Update {{lowbound, asthub::Sub(lowbound, asthub::BvConst(1, ctr_w))}},
+ Assert {asthub::Eq(ctr, 0)}, // dec should not go less than 0
+ Block{
+ Call {inst_inc},
+ Call {inst_inc},
+ Call {inst_dec},
+ Call {inst_inc},
+ Update {{lowbound, asthub::Add(lowbound, asthub::BvConst(3, ctr_w))}},
+ Assert {asthub::Eq(ctr, 2)},
+ },
+ Assert {asthub::Le(lowbound, ctr)}
+ }};
+
+ z3::context ctx;
+ z3::fixedpoint ctxfp {ctx};
+ PFToCHCEncoder encoder {ctx, ctxfp, m, pf};
+
+ // std::cout << "\nEncoded successfully!\n" << std::endl;
+
+ // std::cout << encoder.to_string() << std::endl;
+
+ EXPECT_NO_THROW(encoder.to_string());
+
+ z3::check_result res = z3::sat;
+ try {
+ res = encoder.check_assertions();
+ } catch (const z3::exception& e) {
+ std::cout << "Error: " << e << std::endl;
+ }
+
+ EXPECT_EQ(res, z3::unsat);
+ }
+
+ TEST(Pf2chc, CounterFail) {
+
+ // create ILA
+
+ InstrLvlAbsPtr m = simple_counter_ila();
+ auto inst_inc = m->instr(COUNTER_INSTR_INC);
+ auto inst_dec = m->instr(COUNTER_INSTR_DEC);
+
+ auto ctr = m->state(COUNTER_STATE_CTR);
+ auto op = m->input(COUNTER_INPUT_OP);
+
+ // program fragment
+ ProgramFragment pf {{ /* no params */ }, {
+ Assume {asthub::Eq(ctr, 0)},
+ Call {inst_inc},
+ Assert {asthub::Eq(ctr, 1)},
+ Call {inst_dec},
+ Call {inst_dec},
+ Assert {asthub::Eq(ctr, 3)}, // assertion should fail
+ Call {inst_inc},
+ Call {inst_inc},
+ Call {inst_dec},
+ Call {inst_inc},
+ Assert {asthub::Eq(ctr, 2)}
+ }};
+
+ z3::context ctx;
+ z3::fixedpoint ctxfp {ctx};
+ PFToCHCEncoder encoder {ctx, ctxfp, m, pf};
+
+ // std::cout << "\nEncoded successfully!\n" << std::endl;
+
+ // std::cout << encoder.to_string() << std::endl;
+
+ z3::check_result res = encoder.check_assertions();
+ EXPECT_EQ(res, z3::sat);
+ }
+
+ TEST(Pf2chc, UnrollerSMTTest) {
+
+ using namespace pfast;
+ using namespace asthub;
+
+ auto m = SimpleCpu("m");
+
+ Block b;
+
+ // initial conditions of CPU
+ for (size_t i = 0; i != m->init_num(); i++) {
+ b.push_back(Assume{m->init(i)});
+ }
+
+ MemVal init_mem_val(0);
+ init_mem_val.set_data(0, GenLoad(0, 0));
+ init_mem_val.set_data(1, GenLoad(1, 1));
+ init_mem_val.set_data(2, GenAdd(2, 0, 1));
+ init_mem_val.set_data(3, GenStore(2, 2));
+
+ { // instruction memory
+ auto ir = m->state("ir");
+ b.push_back(Assume{Eq(ir, MemConst(init_mem_val, 8, 8))});
+ }
+
+ // concretize data
+ b.insert(b.end(), {
+ Assume{Eq(m->state("r0"), 7)},
+ Assume{Eq(m->state("r1"), 7)},
+ Assume{Eq(Load(m->state("mem"), 0), 3)},
+ Assume{Eq(Load(m->state("mem"), 1), 3)}
+ });
+
+ // program
+ b.insert(b.end(), {
+ Call{m->instr("Load")},
+ Call{m->instr("Load")},
+ Call{m->instr("Add")},
+ Call{m->instr("Store")}
+ });
+
+ // check stored result
+ b.push_back(Assert{Eq(Load(m->state("mem"), 2), 6)});
+
+ ProgramFragment pf {{ }, b}; /* no params */
+
+ z3::context ctx;
+ z3::fixedpoint ctxfp {ctx};
+
+ // use spacer instead of datalog engine
+ z3::params p {ctx};
+ p.set("engine", "spacer");
+ ctxfp.set(p);
+
+ PFToCHCEncoder encoder {ctx, ctxfp, m, pf};
+
+ // std::cout << "\nEncoded successfully!\n" << std::endl;
+
+ // std::cout << encoder.to_string() << std::endl;
+
+ z3::check_result res = encoder.check_assertions();
+ EXPECT_EQ(res, z3::unsat);
+
+ }
+
+ TEST(Pf2chc, UnrollerSMTTestWithParams) {
+
+ using namespace pfast;
+ using namespace asthub;
+
+ auto m = SimpleCpu("m");
+
+ // params
+ ExprPtr x = m->NewBvFreeVar("x", 8);
+ ExprPtr y = m->NewBvFreeVar("y", 8);
+ ExprPtr unused = m->NewBvFreeVar("unused", 8);
+
+ // fragment body
+ Block b;
+
+ // initial conditions of CPU
+ for (size_t i = 0; i != m->init_num(); i++) {
+ b.push_back(Assume{m->init(i)});
+ }
+
+ MemVal init_mem_val(0);
+ init_mem_val.set_data(0, GenLoad(0, 0));
+ init_mem_val.set_data(1, GenLoad(1, 1));
+ init_mem_val.set_data(2, GenAdd(2, 0, 1));
+ init_mem_val.set_data(3, GenStore(2, 2));
+
+ { // instruction memory
+ auto ir = m->state("ir");
+ b.push_back(Assume{Eq(ir, MemConst(init_mem_val, 8, 8))});
+ }
+
+ // link params and model
+ b.insert(b.end(), {
+ Assume{Eq(Load(m->state("mem"), 0), x)},
+ Assume{Eq(Load(m->state("mem"), 1), y)}
+ });
+
+ // program
+ b.insert(b.end(), {
+ Call{m->instr("Load")},
+ Call{m->instr("Load")},
+ Call{m->instr("Add")},
+ Call{m->instr("Store")}
+ });
+
+ // check stored result
+ b.push_back(Assert{Eq(Load(m->state("mem"), 2), asthub::Add(x, y))});
+
+ ProgramFragment pf {{x, y, unused}, b};
+
+ z3::context ctx;
+ z3::fixedpoint ctxfp {ctx};
+
+ // use spacer instead of datalog
+ z3::params p {ctx};
+ p.set("engine", "spacer");
+ ctxfp.set(p);
+
+ PFToCHCEncoder encoder {ctx, ctxfp, m, pf};
+
+ // std::cout << "\nEncoded successfully!\n" << std::endl;
+
+ // std::cout << encoder.to_string() << std::endl;
+
+ z3::check_result res = encoder.check_assertions();
+
+ EXPECT_EQ(res, z3::unsat);
+
+ }
+
+ TEST(Pf2chc, CounterLoop) {
+
+ InstrLvlAbsPtr m = simple_counter_ila();
+ auto inst_inc = m->instr(COUNTER_INSTR_INC);
+ auto inst_dec = m->instr(COUNTER_INSTR_DEC);
+
+ auto ctr = m->state(COUNTER_STATE_CTR);
+ auto op = m->input(COUNTER_INPUT_OP);
+
+ auto ctr_w = ctr->sort()->bit_width();
+ auto x = m->NewBvFreeVar("x", ctr_w);
+ auto y = m->NewBvFreeVar("y", ctr_w);
+ auto i = m->NewBvFreeVar("i", ctr_w);
+
+ auto inv1 = asthub::And(asthub::Eq(ctr, i), asthub::Le(i, x));
+
+ auto inv2 = asthub::And(
+ asthub::Ge(ctr, asthub::BvConst(0, ctr_w)),
+ asthub::Or(asthub::Eq(ctr, asthub::Sub(x, i)),
+ asthub::Eq(ctr, asthub::BvConst(0, ctr_w)))
+ );
+
+ // program fragment
+ ProgramFragment pf {{ x, y, i }, {
+ Assume {asthub::Eq(ctr, 0)},
+ Assume {asthub::Gt(x, 0)},
+ Assume {asthub::Gt(y, x)},
+ Assume {asthub::Lt(y, 15)}, // keeps runtime short
+
+ Update { {i, asthub::BvConst(0, ctr_w)} },
+ Assert { inv1 },
+ While { asthub::Lt(i, x), {
+ Assume { inv1 },
+ Call { inst_inc, asthub::BoolConst(true) },
+ Update { {i, asthub::Add(i, asthub::BvConst(1, ctr_w))} },
+ Assert { inv1 },
+ }},
+ Assume { inv1 },
+
+ Update { {i, asthub::BvConst(0, ctr_w)} },
+ Assert { inv2 },
+ While { asthub::Lt(i, y), {
+ Assume { inv2 },
+ Call { inst_dec, asthub::BoolConst(true) },
+ Update { {i, asthub::Add(i, asthub::BvConst(1, ctr_w))} },
+ Assert { inv2 },
+ }},
+ Assume { inv2 },
+ Assert { asthub::Eq(ctr, 0) }
+ }};
+
+ z3::context ctx;
+ z3::fixedpoint ctxfp {ctx};
+
+ // use spacer instead of datalog
+ z3::params p {ctx};
+ p.set("engine", "spacer");
+ ctxfp.set(p);
+
+ PFToCHCEncoder encoder {ctx, ctxfp, m, pf};
+
+ // std::cout << "\nEncoded successfully!\n" << std::endl;
+
+ // std::cout << encoder.to_string() << std::endl;
+
+ EXPECT_NO_THROW(encoder.to_string());
+
+ z3::check_result res = z3::sat;
+ try {
+ res = encoder.check_assertions();
+ } catch (const z3::exception& e) {
+ std::cout << "Error: " << e << std::endl;
+ }
+
+ EXPECT_EQ(res, z3::unsat);
+ }
+
+ TEST(Pf2chc, CounterLoop2) {
+
+ InstrLvlAbsPtr m1 = simple_counter_ila("1");
+ InstrLvlAbsPtr m2 = simple_counter_ila("2");
+ auto inst_inc1 = m1->instr(COUNTER_INSTR_INC "1"); // implicit concat of str literals
+ auto inst_inc2 = m2->instr(COUNTER_INSTR_INC "2"); // implicit concat of str literals
+
+ auto ctr1 = m1->state(COUNTER_STATE_CTR "1"); // implicit concat of str literals
+ auto ctr2 = m2->state(COUNTER_STATE_CTR "2"); // implicit concat of str literals
+
+ auto ctr_w = ctr1->sort()->bit_width();
+ auto n = m1->NewBvFreeVar("n", ctr_w);
+ auto i = m1->NewBvFreeVar("i", ctr_w);
+
+ auto inv1 = asthub::And(asthub::Eq(ctr1, i), asthub::Le(i, n));
+ auto inv2 = asthub::And(asthub::Eq(ctr2, i), asthub::Le(i, n));
+
+ // program fragment
+ ProgramFragment pf {{ n, i }, {
+ Assume {asthub::Eq(ctr1, 0)},
+ Assume {asthub::Eq(ctr2, 0)},
+ Assume {asthub::Gt(n, 0)},
+ Assume {asthub::Lt(n, 15)}, // keeps runtime short
+
+ Update { {i, asthub::BvConst(0, ctr_w)} },
+ Assert { inv1 },
+ While { asthub::Lt(i, n), {
+ Assume { inv1 },
+ Call { inst_inc1, asthub::BoolConst(true) },
+ Update { {i, asthub::Add(i, asthub::BvConst(1, ctr_w))} },
+ Assert { inv1 },
+ }},
+ Assume { inv1 },
+
+ Update { {i, asthub::BvConst(0, ctr_w)} },
+ Assert { inv2 },
+ While { asthub::Lt(i, n), {
+ Assume { inv2 },
+ Call { inst_inc2, asthub::BoolConst(true) },
+ Update { {i, asthub::Add(i, asthub::BvConst(1, ctr_w))} },
+ Assert { inv2 },
+ }},
+ Assume { inv2 },
+ Assert { asthub::And(
+ asthub::Eq(ctr1, n), asthub::Eq(ctr1, ctr2)) }
+ }};
+
+ z3::context ctx;
+ z3::fixedpoint ctxfp {ctx};
+
+ // use spacer instead of datalog
+ z3::params p {ctx};
+ p.set("engine", "spacer");
+ ctxfp.set(p);
+
+ PFToCHCEncoder encoder {ctx, ctxfp, m1, pf};
+
+ // std::cout << "\nEncoded successfully!\n" << std::endl;
+
+ // std::cout << encoder.to_string() << std::endl;
+
+ EXPECT_NO_THROW(encoder.to_string());
+
+ z3::check_result res = z3::sat;
+ try {
+ res = encoder.check_assertions();
+ } catch (const z3::exception& e) {
+ std::cout << "Error: " << e << std::endl;
+ }
+
+ EXPECT_EQ(res, z3::unsat);
+ }
+
+ TEST(Pf2chc, Hierarchy) {
+ Ila m {"Broadcast"};
+
+ constexpr int msg_bits = 8;
+ constexpr int port_bits = 4;
+
+ auto next_msg = m.NewBvInput("next_msg", msg_bits);
+ auto msg = m.NewBvState("msg", msg_bits);
+
+ auto n_ports = m.NewBvState("nports", port_bits);
+ auto ports = m.NewMemState("ports", port_bits, msg_bits);
+
+ auto cur_port = m.NewBvState("cur_port", port_bits);
+
+ m.SetValid((n_ports > 0) & (msg == 0 | next_msg == 0));
+
+ auto child = m.NewChild("broadcaster");
+ child.SetValid((n_ports > 0) & (msg != 0));
+ auto bcast_step = child.NewInstr("bcast_step");
+ {
+ bcast_step.SetDecode((msg != 0) & (cur_port < n_ports));
+ bcast_step.SetUpdate(ports, Store(ports, cur_port, msg));
+ bcast_step.SetUpdate(cur_port, cur_port + 1);
+ bcast_step.SetUpdate(msg,
+ Ite(cur_port + 1 == n_ports, BvConst(0, msg_bits), msg));
+ }
+
+ auto broadcast = m.NewInstr("bcast");
+ {
+ broadcast.SetDecode((msg == 0) & (next_msg != 0));
+ broadcast.SetUpdate(msg, next_msg);
+ broadcast.SetUpdate(cur_port, BvConst(0, port_bits));
+ broadcast.SetProgram(child);
+ }
+
+ auto num = m.get()->NewBvFreeVar("num", msg_bits);
+ auto k = m.get()->NewBvFreeVar("k", port_bits);
+ auto i = m.get()->NewBvFreeVar("i", port_bits);
+
+ auto inv = asthub::And(
+ asthub::Le(i, n_ports.get()),
+ asthub::Or(
+ asthub::Le(i, k),
+ asthub::Eq(asthub::Load(ports.get(), k), num)
+ )
+ );
+
+ /* Program fragment:
+ FORALL num, k, i {
+ ASSUME 0 < k < n_ports;
+ CALL broadcast WHERE next_msg = num;
+ UPDATE i = 0;
+ ASSERT inv: (i <= n) && (i <= k || ports[k] == num);
+ WHILE i < n_ports DO {
+ ASSUME inv;
+ CALL bcast_step;
+ UPDATE i = i + 1;
+ ASSERT inv;
+ } END;
+ ASSUME inv;
+ ASSERT ports[k] == num;
+ }
+ */
+
+ ProgramFragment pf {{num, k, i}, {
+ // ASSUME 0 < k < n_ports
+ Assume { asthub::Gt(k, asthub::BvConst(0, port_bits)) },
+ Assume { asthub::Gt(n_ports.get(), k) },
+ // CALL broadcast WHERE next_msg = num
+ Call { broadcast.get(), asthub::Eq(next_msg.get(), num) },
+ // UPDATE i = 0
+ Update { {i, asthub::BvConst(0, port_bits)} },
+ // ASSERT inv: (i <= n) && (i <= k || ports[k] == num)
+ Assert { inv },
+ // WHILE i < n_ports DO
+ While { asthub::Lt(i, n_ports.get()), {
+ // ASSUME inv
+ Assume { inv },
+ // CALL bcast_step
+ Call { bcast_step.get() },
+ // UPDATE i = i + 1
+ Update { {i, asthub::Add(i, asthub::BvConst(1, port_bits))} },
+ // ASSERT inv
+ Assert { inv }
+ } }, // END
+ // ASSUME inv
+ Assume { inv },
+ // ASSERT ports[k] = num
+ Assert { asthub::Eq(asthub::Load(ports.get(), k), num) }
+ }};
+
+ z3::context ctx;
+ z3::fixedpoint ctxfp {ctx};
+
+ // use spacer instead of datalog
+ // z3::params p {ctx};
+ // p.set("engine", "spacer");
+ // ctxfp.set(p);
+
+ PFToCHCEncoder encoder {ctx, ctxfp, m.get(), pf};
+
+ // std::cout << "\nEncoded successfully!\n" << std::endl;
+
+ // std::cout << encoder.to_string() << std::endl;
+
+ EXPECT_NO_THROW(encoder.to_string());
+
+ z3::check_result res = z3::sat;
+
+ try {
+ res = encoder.check_assertions();
+ } catch (const z3::exception& e) {
+ std::cout << "Error: " << e << std::endl;
+ }
+
+ EXPECT_EQ(res, z3::unsat);
+
+ }
+
+ TEST(Pf2chc, CounterLoopNested) {
+
+ InstrLvlAbsPtr m = simple_counter_ila();
+ auto inst_inc = m->instr(COUNTER_INSTR_INC);
+ auto inst_dec = m->instr(COUNTER_INSTR_DEC);
+
+ auto ctr = m->state(COUNTER_STATE_CTR);
+ auto op = m->input(COUNTER_INPUT_OP);
+
+ auto ctr_w = ctr->sort()->bit_width();
+ auto x = asthub::NewBvVar("x", ctr_w); // asthub::BvConst(3, ctr_w);
+ auto y = asthub::NewBvVar("y", ctr_w); // asthub::BvConst(4, ctr_w);
+ auto i = asthub::NewBvVar("i", ctr_w);
+ auto j = asthub::NewBvVar("j", ctr_w);
+
+ auto inv1 = asthub::And(
+ asthub::Eq(ctr, asthub::Mul(i, y)),
+ asthub::Le(i, x)
+ );
+
+ auto inv2 = asthub::And(
+ asthub::Eq(ctr, asthub::Add(asthub::Mul(i, y), j)),
+ asthub::Le(j, y)
+ );
+
+ // program fragment
+ ProgramFragment pf {{ x, y, i, j }, {
+ Assume {asthub::Eq(ctr, 0)},
+ Assume {asthub::Gt(x, 0)},
+ Assume {asthub::Gt(y, 0)},
+ Assume {asthub::Lt(x, 3)}, // keeps runtime short
+ Assume {asthub::Lt(y, 4)}, // keeps runtime short
+
+ Update { {i, asthub::BvConst(0, ctr_w)} },
+ Assert { inv1 },
+ While { asthub::Lt(i, x), {
+ Assume { inv1 },
+ Update { {j, asthub::BvConst(0, ctr_w)} },
+ Assert { inv2 },
+ While { asthub::Lt(j, y), {
+ Assume { inv2 },
+ Call { inst_inc },
+ Update { {j, asthub::Add(j, asthub::BvConst(1, ctr_w))} },
+ Assert { inv2 }
+ }},
+ Assume { inv2 },
+ Update { {i, asthub::Add(i, asthub::BvConst(1, ctr_w))} },
+ Assert { inv1 },
+ }},
+ Assume { inv1 },
+ Assert { asthub::Eq(ctr, asthub::Mul(x, y)) }
+ }};
+
+ z3::context ctx;
+ z3::fixedpoint ctxfp {ctx};
+
+ // use spacer instead of datalog
+ z3::params p {ctx};
+ p.set("engine", "spacer");
+ ctxfp.set(p);
+
+ PFToCHCEncoder encoder {ctx, ctxfp, m, pf};
+
+ // std::cout << "\nEncoded successfully!\n" << std::endl;
+
+ // std::cout << encoder.to_string() << std::endl;
+
+ EXPECT_NO_THROW(encoder.to_string());
+
+ z3::check_result res = z3::sat;
+ try {
+ res = encoder.check_assertions();
+ } catch (const z3::exception& e) {
+ std::cout << "Error: " << e << std::endl;
+ }
+
+ EXPECT_EQ(res, z3::unsat);
+ }
+
+}
+
+}
diff --git a/test/t_smt_shim.cc b/test/t_smt_shim.cc
index 2d158582d..5a217b690 100644
--- a/test/t_smt_shim.cc
+++ b/test/t_smt_shim.cc
@@ -2,11 +2,20 @@
/// Unit tests for SmtShim
#ifdef SMTSWITCH_TEST
-#include
#include
#endif // SMTSWITCH_TEST
+#ifdef SMTSWITCH_BTOR
+#include
+#endif // SMTSWITCH_BTOR
+
+#ifdef SMTSWITCH_Z3
+#include
+#include
+#endif // SMTSWITCH_Z3
+
#include
+#include
#include
#include
#include
@@ -44,7 +53,7 @@ class TestSmtShim : public ::testing::Test {
}
void CheckUnsatSwitch(const ExprRef& e) {
-#ifdef SMTSWITCH_TEST
+#ifdef SMTSWITCH_BTOR
auto solver = smt::BoolectorSolverFactory::create(false);
auto switch_itf = SmtSwitchItf(solver);
auto shim = SmtShim(switch_itf);
@@ -53,7 +62,20 @@ class TestSmtShim : public ::testing::Test {
solver->assert_formula(switch_term);
auto res = solver->check_sat();
EXPECT_TRUE(res.is_unsat());
-#endif // SMTSWITCH_TEST
+#endif // SMTSWITCH_BTOR
+ }
+
+ void CheckUnsatLia(const ExprRef& e) {
+#ifdef SMTSWITCH_Z3
+ auto solver = smt::Z3SolverFactory::create(false);
+ auto lia_cvtr = LiaCvtr(solver);
+ auto shim = SmtShim(lia_cvtr);
+
+ auto lia_term = shim.GetShimExpr(e.get());
+ solver->assert_formula(lia_term);
+ auto res = solver->check_sat();
+ EXPECT_TRUE(res.is_unsat());
+#endif // SMTSWITCH_Z3
}
Ila m = Ila("host");
@@ -71,6 +93,7 @@ TEST_F(TestSmtShim, OpBoolNot) {
auto prop = not_not_a != var_bool_a;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvNeg) {
@@ -79,6 +102,7 @@ TEST_F(TestSmtShim, OpBvNeg) {
auto prop = neg_neg_a != var_bv_a;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvComplement) {
@@ -87,12 +111,14 @@ TEST_F(TestSmtShim, OpBvComplement) {
auto prop = com_com_a != var_bv_a;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ EXPECT_DEATH(CheckUnsatLia(prop), ".*");
}
TEST_F(TestSmtShim, OpBoolAnd) {
auto a_and_not_a = var_bool_a & !var_bool_a;
CheckUnsatZ3(a_and_not_a);
CheckUnsatSwitch(a_and_not_a);
+ CheckUnsatLia(a_and_not_a);
}
TEST_F(TestSmtShim, OpBvAnd) {
@@ -100,6 +126,7 @@ TEST_F(TestSmtShim, OpBvAnd) {
auto prop = a_and_all1 != var_bv_a;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ EXPECT_DEATH(CheckUnsatLia(prop), ".*");
}
TEST_F(TestSmtShim, OpBoolOr) {
@@ -107,6 +134,7 @@ TEST_F(TestSmtShim, OpBoolOr) {
auto prop = !a_or_not_a;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvOr) {
@@ -114,6 +142,7 @@ TEST_F(TestSmtShim, OpBvOr) {
auto prop = a_or_0 != var_bv_a;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ EXPECT_DEATH(CheckUnsatLia(prop), ".*");
}
TEST_F(TestSmtShim, OpBoolXor) {
@@ -122,6 +151,7 @@ TEST_F(TestSmtShim, OpBoolXor) {
auto prop = a_xor_b & a_eq_b;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvXor) {
@@ -130,6 +160,7 @@ TEST_F(TestSmtShim, OpBvXor) {
auto prop = a_eq_b & (a_xor_b == BvConst((1 << BV_SIZE) - 1, BV_SIZE));
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ EXPECT_DEATH(CheckUnsatLia(prop), ".*");
}
TEST_F(TestSmtShim, OpBvShl) {
@@ -137,6 +168,7 @@ TEST_F(TestSmtShim, OpBvShl) {
auto prop = a_shl_all != BvConst(0, BV_SIZE);
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ EXPECT_DEATH(CheckUnsatLia(prop), ".*");
}
TEST_F(TestSmtShim, OpBvAshr) {
@@ -146,6 +178,7 @@ TEST_F(TestSmtShim, OpBvAshr) {
auto prop = !(is_pos | is_neg);
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ EXPECT_DEATH(CheckUnsatLia(prop), ".*");
}
TEST_F(TestSmtShim, OpBvLshr) {
@@ -153,6 +186,7 @@ TEST_F(TestSmtShim, OpBvLshr) {
auto prop = a_ashr_all != BvConst(0, BV_SIZE);
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ EXPECT_DEATH(CheckUnsatLia(prop), ".*");
}
TEST_F(TestSmtShim, OpBvAdd) {
@@ -160,6 +194,7 @@ TEST_F(TestSmtShim, OpBvAdd) {
auto prop = a_plus_0 != var_bv_a;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvSub) {
@@ -167,6 +202,7 @@ TEST_F(TestSmtShim, OpBvSub) {
auto prop = a_minus_0 != var_bv_a;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvAddSub) {
@@ -175,6 +211,7 @@ TEST_F(TestSmtShim, OpBvAddSub) {
auto prop = a_plus_b_minus_b != var_bv_a;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvMul) {
@@ -182,6 +219,7 @@ TEST_F(TestSmtShim, OpBvMul) {
auto prop = a_times_0 != BvConst(0, BV_SIZE);
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvDiv) {
@@ -189,6 +227,7 @@ TEST_F(TestSmtShim, OpBvDiv) {
auto prop = a_div_1 != var_bv_a;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvSrem) {
@@ -197,6 +236,7 @@ TEST_F(TestSmtShim, OpBvSrem) {
auto prop = !(Slt(a_srem_3, div));
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ EXPECT_DEATH(CheckUnsatLia(prop), ".*");
}
TEST_F(TestSmtShim, OpBvUrem) {
@@ -205,6 +245,7 @@ TEST_F(TestSmtShim, OpBvUrem) {
auto prop = !(Ult(a_urem_3, div));
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ EXPECT_DEATH(CheckUnsatLia(prop), ".*");
}
TEST_F(TestSmtShim, OpBvSmod) {
@@ -213,6 +254,7 @@ TEST_F(TestSmtShim, OpBvSmod) {
auto prop = !(Slt(a_smod_3, div));
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ // LIA
}
TEST_F(TestSmtShim, OpBvSltSge) {
@@ -221,6 +263,7 @@ TEST_F(TestSmtShim, OpBvSltSge) {
auto prop = a_slt_b & a_sge_b;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvSleSgt) {
@@ -229,6 +272,7 @@ TEST_F(TestSmtShim, OpBvSleSgt) {
auto prop = a_sle_b & a_sgt_b;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvSltSgteq) {
@@ -238,6 +282,7 @@ TEST_F(TestSmtShim, OpBvSltSgteq) {
auto prop = !(a_slt_b | a_sgt_b | a_eq_b);
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvUltUge) {
@@ -246,6 +291,7 @@ TEST_F(TestSmtShim, OpBvUltUge) {
auto prop = a_ult_b & a_uge_b;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvUleUgt) {
@@ -254,6 +300,7 @@ TEST_F(TestSmtShim, OpBvUleUgt) {
auto prop = a_ule_b & a_ugt_b;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvUltUgteq) {
@@ -263,6 +310,7 @@ TEST_F(TestSmtShim, OpBvUltUgteq) {
auto prop = !(a_ult_b | a_ugt_b | a_eq_b);
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpMemLoad) {
@@ -271,6 +319,7 @@ TEST_F(TestSmtShim, OpMemLoad) {
auto prop = (var_bv_a == var_bv_b) & (data_a != data_b);
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpMemStore) {
@@ -279,6 +328,7 @@ TEST_F(TestSmtShim, OpMemStore) {
auto prop = data != var_bv_b;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvConcat) {
@@ -287,6 +337,7 @@ TEST_F(TestSmtShim, OpBvConcat) {
auto prop = (var_bv_a == var_bv_b) & (a_con_b != b_con_a);
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvExtract) {
@@ -295,6 +346,7 @@ TEST_F(TestSmtShim, OpBvExtract) {
auto prop = extract_a_con_b != var_bv_b;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ EXPECT_DEATH(CheckUnsatLia(prop), ".*");
}
TEST_F(TestSmtShim, OpBvZext) {
@@ -303,6 +355,7 @@ TEST_F(TestSmtShim, OpBvZext) {
auto prop = zext_a != zero_con_a;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvSext) {
@@ -312,6 +365,7 @@ TEST_F(TestSmtShim, OpBvSext) {
auto prop = sext_a != zero_con_a;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ EXPECT_DEATH(CheckUnsatLia(prop), ".*");
}
TEST_F(TestSmtShim, OpBvRotate) {
@@ -320,6 +374,7 @@ TEST_F(TestSmtShim, OpBvRotate) {
auto prop = right_rotate_back != var_bv_a;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ EXPECT_DEATH(CheckUnsatLia(prop), ".*");
}
TEST_F(TestSmtShim, OpBoolImply) {
@@ -327,6 +382,7 @@ TEST_F(TestSmtShim, OpBoolImply) {
auto prop = a_imply_b & var_bool_a & !var_bool_b;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBoolIte) {
@@ -334,6 +390,7 @@ TEST_F(TestSmtShim, OpBoolIte) {
auto prop = ite_a_0_a;
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpBvIte) {
@@ -341,6 +398,7 @@ TEST_F(TestSmtShim, OpBvIte) {
auto prop = (var_bv_a == var_bv_b) & (ite_c_a_b != var_bv_a);
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, OpApplyFunc) {
@@ -350,6 +408,7 @@ TEST_F(TestSmtShim, OpApplyFunc) {
auto prop = (var_bv_a == var_bv_b) & (out1 != out2);
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, ConstBool) {
@@ -358,6 +417,7 @@ TEST_F(TestSmtShim, ConstBool) {
auto prop = a_is_0 & b_is_1 & (var_bool_a == var_bool_b);
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, ConstBv) {
@@ -366,6 +426,7 @@ TEST_F(TestSmtShim, ConstBv) {
auto prop = a_is_0 & b_is_1 & (var_bv_a == var_bv_b);
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, ConstMem) {
@@ -380,6 +441,7 @@ TEST_F(TestSmtShim, ConstMem) {
auto prop = !Imply(save_addr, is_linear);
CheckUnsatZ3(prop);
CheckUnsatSwitch(prop);
+ CheckUnsatLia(prop);
}
TEST_F(TestSmtShim, DiscreteUsage) {
@@ -401,7 +463,7 @@ TEST_F(TestSmtShim, DiscreteUsage) {
EXPECT_TRUE(res == z3::unsat);
}
-#ifdef SMTSWITCH_TEST
+#ifdef SMTSWITCH_BTOR
{ // switch
auto solver = smt::BoolectorSolverFactory::create(false);
auto itf = SmtSwitchItf(solver);
@@ -414,7 +476,26 @@ TEST_F(TestSmtShim, DiscreteUsage) {
auto res = solver->check_sat();
EXPECT_TRUE(res.is_unsat());
}
-#endif // SMTSWITCH_TEST
+#endif // SMTSWITCH_BTOR
+
+#ifdef SMTSWITCH_Z3
+ { // LiaCvtr
+ auto solver = smt::Z3SolverFactory::create(false);
+ auto lia = LiaCvtr(solver);
+ auto shim = SmtShim(lia);
+
+ // Use SmtShim to gen/add formulas
+ solver->assert_formula(shim.GetShimExpr(a_ult_b.get()));
+ solver->assert_formula(shim.GetShimExpr(a_ugt_b.get()));
+ solver->assert_formula(shim.GetShimExpr(a_eq_b.get()));
+
+ // Use z3's command for checking
+ auto raw = std::static_pointer_cast(solver);
+ auto slv = raw->get_z3_solver(); // get_z3_context() also available
+ auto res = slv->check();
+ EXPECT_TRUE(res == z3::unsat);
+ }
+#endif // SMTSWITCH_Z3
}
} // namespace ilang
diff --git a/test/t_smt_switch_itf.cc b/test/t_smt_switch_itf.cc
deleted file mode 100644
index 7965d30d5..000000000
--- a/test/t_smt_switch_itf.cc
+++ /dev/null
@@ -1,367 +0,0 @@
-/// \file
-/// Unit tests for smt-switch interface (with Boolector)
-
-#ifdef SMTSWITCH_TEST
-
-#include
-#include
-
-#include
-#include
-
-#include "unit-include/util.h"
-
-#define BV_SIZE 4
-
-namespace ilang {
-
-class TestSmtSwitch : public ::testing::Test {
-public:
- TestSmtSwitch()
- : var_bool_a(m.NewBoolState("var_bool_a")),
- var_bool_b(m.NewBoolState("var_bool_b")),
- var_bv_a(m.NewBvState("var_bv_a", BV_SIZE)),
- var_bv_b(m.NewBvState("var_bv_b", BV_SIZE)),
- var_mem_a(m.NewMemState("var_mem_a", BV_SIZE, BV_SIZE)),
- var_mem_b(m.NewMemState("var_mem_b", BV_SIZE, BV_SIZE)) {
- // use boolector for the unit tests
- s = smt::BoolectorSolverFactory::create(false);
- }
-
- ~TestSmtSwitch() {}
-
- void SetUp() {}
-
- void TearDown() {
- // reset all created terms etc.
- s->reset();
- }
-
- void CheckUnsat(const ExprRef& e) {
- auto term = ResetAndGetSmtTerm(s, e);
- s->assert_formula(term);
- auto res = s->check_sat();
- EXPECT_TRUE(res.is_unsat());
- }
-
- smt::SmtSolver s;
-
- Ila m = Ila("host");
- ExprRef var_bool_a;
- ExprRef var_bool_b;
- ExprRef var_bv_a;
- ExprRef var_bv_b;
- ExprRef var_mem_a;
- ExprRef var_mem_b;
-
-}; // class TestSmtSwitch
-
-TEST_F(TestSmtSwitch, OpBvNeg) {
- auto neg_a = -var_bv_a;
- auto neg_neg_a = -neg_a;
- auto prop = neg_neg_a != var_bv_a;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBoolNot) {
- auto not_a = !var_bool_a;
- auto not_not_a = !not_a;
- auto prop = not_not_a != var_bool_a;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvComplement) {
- auto com_a = ~var_bv_a;
- auto com_com_a = ~com_a;
- auto prop = com_com_a != var_bv_a;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBoolAnd) {
- auto a_and_not_a = var_bool_a & !var_bool_a;
- CheckUnsat(a_and_not_a);
-}
-
-TEST_F(TestSmtSwitch, OpBvAnd) {
- auto a_and_all1 = var_bv_a & BvConst((1 << BV_SIZE) - 1, BV_SIZE);
- auto prop = a_and_all1 != var_bv_a;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBoolOr) {
- auto a_or_not_a = var_bool_a | !var_bool_a;
- auto prop = !a_or_not_a;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvOr) {
- auto a_or_0 = var_bv_a | BvConst(0, BV_SIZE);
- auto prop = a_or_0 != var_bv_a;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBoolXor) {
- auto a_xor_b = var_bool_a ^ var_bool_b;
- auto a_eq_b = var_bool_a == var_bool_b;
- auto prop = a_xor_b & a_eq_b;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvXor) {
- auto a_xor_b = var_bv_a ^ var_bv_b;
- auto a_eq_b = var_bv_a == var_bv_b;
- auto prop = a_eq_b & (a_xor_b == BvConst((1 << BV_SIZE) - 1, BV_SIZE));
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvShl) {
- auto a_shl_all = var_bv_a << BV_SIZE;
- auto prop = a_shl_all != BvConst(0, BV_SIZE);
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvAshr) {
- auto a_ashr_all = var_bv_a >> BV_SIZE;
- auto is_pos = a_ashr_all == BvConst(0, BV_SIZE);
- auto is_neg = a_ashr_all == BvConst((1 << BV_SIZE) - 1, BV_SIZE);
- auto prop = !(is_pos | is_neg);
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvLshr) {
- auto a_ashr_all = Lshr(var_bv_a, BvConst(BV_SIZE, BV_SIZE));
- auto prop = a_ashr_all != BvConst(0, BV_SIZE);
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvAdd) {
- auto a_plus_0 = var_bv_a + BvConst(0, BV_SIZE);
- auto prop = a_plus_0 != var_bv_a;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvSub) {
- auto a_minus_0 = var_bv_a - BvConst(0, BV_SIZE);
- auto prop = a_minus_0 != var_bv_a;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvAddSub) {
- auto a_plus_b = var_bv_a + var_bv_b;
- auto a_plus_b_minus_b = a_plus_b - var_bv_b;
- auto prop = a_plus_b_minus_b != var_bv_a;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvMul) {
- auto a_times_0 = var_bv_a * BvConst(0, BV_SIZE);
- auto prop = a_times_0 != BvConst(0, BV_SIZE);
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvDiv) {
- auto a_div_1 = var_bv_a / BvConst(1, BV_SIZE);
- auto prop = a_div_1 != var_bv_a;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvSrem) {
- auto div = BvConst(3, BV_SIZE);
- auto a_srem_3 = SRem(var_bv_a, div);
- auto prop = !(Slt(a_srem_3, div));
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvUrem) {
- auto div = BvConst(3, BV_SIZE);
- auto a_urem_3 = URem(var_bv_a, div);
- auto prop = !(Ult(a_urem_3, div));
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvSmod) {
- auto div = BvConst(3, BV_SIZE);
- auto a_smod_3 = SMod(var_bv_a, div);
- auto prop = !(Slt(a_smod_3, div));
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvSltSge) {
- auto a_slt_b = var_bv_a < var_bv_b;
- auto a_sge_b = var_bv_a >= var_bv_b;
- auto prop = a_slt_b & a_sge_b;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvSleSgt) {
- auto a_sle_b = var_bv_a <= var_bv_b;
- auto a_sgt_b = var_bv_a > var_bv_b;
- auto prop = a_sle_b & a_sgt_b;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvSltSgteq) {
- auto a_slt_b = var_bv_a < var_bv_b;
- auto a_sgt_b = var_bv_a > var_bv_b;
- auto a_eq_b = var_bv_a == var_bv_b;
- auto prop = !(a_slt_b | a_sgt_b | a_eq_b);
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvUltUge) {
- auto a_ult_b = Ult(var_bv_a, var_bv_b);
- auto a_uge_b = Uge(var_bv_a, var_bv_b);
- auto prop = a_ult_b & a_uge_b;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvUleUgt) {
- auto a_ule_b = Ule(var_bv_a, var_bv_b);
- auto a_ugt_b = Ugt(var_bv_a, var_bv_b);
- auto prop = a_ule_b & a_ugt_b;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvUltUgteq) {
- auto a_ult_b = Ult(var_bv_a, var_bv_b);
- auto a_ugt_b = Ugt(var_bv_a, var_bv_b);
- auto a_eq_b = var_bv_a == var_bv_b;
- auto prop = !(a_ult_b | a_ugt_b | a_eq_b);
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpMemLoad) {
- auto data_a = Load(var_mem_a, var_bv_a);
- auto data_b = Load(var_mem_a, var_bv_b);
- auto prop = (var_bv_a == var_bv_b) & (data_a != data_b);
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpMemStore) {
- auto new_mem = Store(var_mem_a, var_bv_a, var_bv_b);
- auto data = Load(new_mem, var_bv_a);
- auto prop = data != var_bv_b;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvConcat) {
- auto a_con_b = Concat(var_bv_a, var_bv_b);
- auto b_con_a = Concat(var_bv_b, var_bv_a);
- auto prop = (var_bv_a == var_bv_b) & (a_con_b != b_con_a);
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvExtract) {
- auto a_con_b = Concat(var_bv_a, var_bv_b);
- auto extract_a_con_b = Extract(a_con_b, BV_SIZE - 1, 0);
- auto prop = extract_a_con_b != var_bv_b;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvZext) {
- auto zext_a = ZExt(var_bv_a, 2 * BV_SIZE);
- auto zero_con_a = Concat(BvConst(0, BV_SIZE), var_bv_a);
- auto prop = zext_a != zero_con_a;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvSext) {
- auto pos_a = Lshr(var_bv_a, 1);
- auto sext_a = SExt(pos_a, 2 * BV_SIZE);
- auto zero_con_a = Concat(BvConst(0, BV_SIZE), pos_a);
- auto prop = sext_a != zero_con_a;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvRotate) {
- auto left_rotate_1 = LRotate(var_bv_a, 1);
- auto right_rotate_back = RRotate(left_rotate_1, 1);
- auto prop = right_rotate_back != var_bv_a;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBoolImply) {
- auto a_imply_b = Imply(var_bool_a, var_bool_b);
- auto prop = a_imply_b & var_bool_a & !var_bool_b;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBoolIte) {
- auto ite_a_0_a = Ite(var_bool_a, BoolConst(false), var_bool_a);
- auto prop = ite_a_0_a;
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpBvIte) {
- auto ite_c_a_b = Ite(var_bool_a, var_bv_a, var_bv_b);
- auto prop = (var_bv_a == var_bv_b) & (ite_c_a_b != var_bv_a);
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, OpApplyFunc) {
- auto func = FuncRef("func", SortRef::BOOL(), SortRef::BV(BV_SIZE));
- auto out1 = func(var_bv_a);
- auto out2 = func(var_bv_b);
- auto prop = (var_bv_a == var_bv_b) & (out1 != out2);
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, ConstBool) {
- auto a_is_0 = var_bool_a == BoolConst(false);
- auto b_is_1 = var_bool_b == BoolConst(true);
- auto prop = a_is_0 & b_is_1 & (var_bool_a == var_bool_b);
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, ConstBv) {
- auto a_is_0 = var_bv_a == BvConst(0, BV_SIZE);
- auto b_is_1 = var_bv_b == BvConst(1, BV_SIZE);
- auto prop = a_is_0 & b_is_1 & (var_bv_a == var_bv_b);
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, ConstMem) {
- std::map data_pair;
- data_pair[0] = 0;
- data_pair[1] = 1;
- data_pair[2] = 2;
- data_pair[3] = 3;
- auto const_mem = MemConst(0, data_pair, BV_SIZE, BV_SIZE);
- auto save_addr = (var_bv_a <= 3) & (var_bv_a >= 0);
- auto is_linear = Load(const_mem, var_bv_a) == var_bv_a;
- auto prop = !Imply(save_addr, is_linear);
- CheckUnsat(prop);
-}
-
-TEST_F(TestSmtSwitch, DiscreteUsage) {
- auto a_ult_b = Ult(var_bv_a, var_bv_b);
- auto a_ugt_b = Ugt(var_bv_a, var_bv_b);
- auto a_eq_b = var_bv_a == var_bv_b;
-
- auto itf = SmtSwitchItf(s);
- s->assert_formula(itf.GetSmtTerm(a_ult_b.get()));
- s->assert_formula(itf.GetSmtTerm(a_ugt_b.get()));
- s->assert_formula(itf.GetSmtTerm(a_eq_b.get()));
-
- auto res = s->check_sat();
- EXPECT_TRUE(res.is_unsat());
-}
-
-TEST_F(TestSmtSwitch, DISABLED_MultiIssue) {
- auto itf = SmtSwitchItf(s);
-
- auto a_and_not_a = var_bool_a & !var_bool_a;
- s->assert_formula(itf.GetSmtTerm(a_and_not_a.get()));
- auto res = s->check_sat();
- EXPECT_TRUE(res.is_unsat());
-
- itf.Reset(); // XXX solver not properly reseted
-
- auto a_or_b = var_bool_a | var_bool_b;
- s->assert_formula(itf.GetSmtTerm(a_or_b.get()));
- EXPECT_TRUE(res.is_sat());
-}
-
-}; // namespace ilang
-
-#endif // SMTSWITCH_TEST
diff --git a/test/t_unroller_smt.cc b/test/t_unroller_smt.cc
index 86c986dd4..a9ed61cc3 100644
--- a/test/t_unroller_smt.cc
+++ b/test/t_unroller_smt.cc
@@ -2,10 +2,17 @@
/// Unit tests for Unroller using SmtShim
#ifdef SMTSWITCH_TEST
-#include
#include
#endif // SMTSWITCH_TEST
+#ifdef SMTSWITCH_BTOR
+#include
+#endif // SMTSWITCH_BTOR
+
+#ifdef SMTSWITCH_Z3
+#include
+#endif // SMTSWITCH_Z3
+
#include
#include
#include
@@ -98,17 +105,28 @@ TEST_F(TestUnrollerSmt, z3) {
#ifdef SMTSWITCH_TEST
TEST_F(TestUnrollerSmt, btor) {
- auto solver = smt::BoolectorSolverFactory::create(false);
- auto switch_itf = SmtSwitchItf(solver);
- auto shim = SmtShim(switch_itf);
- auto p = UnrollTestSequence(shim);
+ auto UnrollAndCheck = [this](smt::SmtSolver& solver) {
+ auto switch_itf = SmtSwitchItf(solver);
+ auto shim = SmtShim(switch_itf);
- solver->assert_formula(p);
- auto res = solver->check_sat();
- EXPECT_TRUE(res.is_unsat());
-}
+ auto p = UnrollTestSequence(shim);
+
+ solver->assert_formula(p);
+ auto res = solver->check_sat();
+ EXPECT_TRUE(res.is_unsat());
+ };
+#ifdef SMTSWITCH_BTOR
+ auto s_btor = smt::BoolectorSolverFactory::create(false);
+ UnrollAndCheck(s_btor);
+#endif // SMTSWITCH_BTOR
+
+#ifdef SMTSWITCH_Z3
+ auto s_z3 = smt::Z3SolverFactory::create(false);
+ UnrollAndCheck(s_z3);
+#endif // SMTSWITCH_Z3
+}
#endif // SMTSWITCH_TEST
} // namespace ilang