[WIP] Support for converting ILA program fragments to CHC problems

.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}}

.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

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)

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 <dir/for/smtswitch>
+source scripts/setup-smtswitch.sh <ilang/src/dir> <dir/for/smtswitch>
 ```
 
 
 ### 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=<dir/for/smtswitch>
 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=<dir/for/smtswitch>
 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).

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()

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,13 +20,15 @@
 #   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
 # XXX @smt-switch config time, set SMT_SWITCH_LIB_TYPE to STATIC
 
 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()
+

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 <unordered_map>
+#include <variant>
+#include <vector>
+#include <set>
+#include <sstream>
+
+#include <z3++.h>
+
+#include <ilang/ila/instr_lvl_abs.h>
+#include <ilang/ila-mngr/u_unroller.h>
+
+/// \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<Assert, Assume, Call, Update, While, Block>;
+
+    /// Converts to a string for pretty printing
+    std::string to_string(const Stmt& s);
+
+    struct Block : public std::vector<Stmt> {
+      using base=std::vector<Stmt>;
+      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>, "assert not copy constructible");
+    static_assert(std::is_copy_assignable_v<Assert>, "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>, "assume not copy constructible");
+    static_assert(std::is_copy_assignable_v<Assume>, "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>, "call not copy constructible");
+    static_assert(std::is_copy_assignable_v<Call>, "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>, "update not copy constructible");
+    static_assert(std::is_copy_assignable_v<Update>, "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>, "while not copy constructible");
+    static_assert(std::is_copy_assignable_v<While>, "while not copy assignable");
+
+    static_assert(std::is_copy_constructible_v<Stmt>, "stmt not copy constructible");
+    static_assert(std::is_copy_assignable_v<Stmt>, "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