Tg nonlin

.gitignore

@@ -13,3 +13,29 @@
 /llvm-seahorn/
 /seahorn-llvm/
 /gtags.files
+
+.mypy_cache
+.vscode
+.sync
+.tags
+.tags1
+.ipynb_checkpoints
+terraform.tfstate
+terraform.tfstate.backup*
+tools/deep_bench/windows/files/ice.zip
+tools/deep_bench/windows/files/mcmc.zip
+tools/deep_bench/**/.terraform
+tools/deep_bench/**/playbook.retry
+tools/deep_bench/**/playbook.retry
+tools/deep_bench/windows/clusterjobs.log
+tools/deep_bench/windows/out-*.tar.gz
+
+# Benchmarks
+
+bench/
+bench_adt/
+bench_horn_adt/
+bench_sim/
+
+# .idea files
+cmake-build-debug/

CMakeLists.txt

@@ -1,35 +1,33 @@
 cmake_minimum_required(VERSION 2.8.11)
 
-project (SeaHorn)
-set (SeaHorn_VERSION_MAJOR 0)
-set (SeaHorn_VERSION_MINOR 1)
-set (SeaHorn_VERSION_PATCH 0)
-set (SeaHorn_VERSION_TWEAK "rc3")
+project (FreqHorn)
+set (FreqHorn_VERSION_MAJOR 0)
+set (FreqHorn_VERSION_MINOR 5)
 
 if (NOT PACKAGE_VERSION)
   set(PACKAGE_VERSION
-    "${SeaHorn_VERSION_MAJOR}.${SeaHorn_VERSION_MINOR}.${SeaHorn_VERSION_PATCH}")
-  if (DEFINED SeaHorn_VERSION_TWEAK)
-    set (PACKAGE_VERSION "${PACKAGE_VERSION}-${SeaHorn_VERSION_TWEAK}")
+          "${FreqHorn_VERSION_MAJOR}.${FreqHorn_VERSION_MINOR}.${FreqHorn_VERSION_PATCH}")
+  if (DEFINED FreqHorn_VERSION_TWEAK)
+    set (PACKAGE_VERSION "${PACKAGE_VERSION}-${FreqHorn_VERSION_TWEAK}")
   endif()
-  set (SeaHorn_VERSION_INFO ${PACKAGE_VERSION})
+  set (FreqHorn_VERSION_INFO ${PACKAGE_VERSION})
 endif()
 
 
 if (CMAKE_SOURCE_DIR STREQUAL CMAKE_BINARY_DIR )
   message (FATAL_ERROR
-    "In-source builds are not allowed. Please clean your source tree and try again.")
+          "In-source builds are not allowed. Please clean your source tree and try again.")
 endif()
 
 enable_testing()
 include (CTest)
 
 # Add path for custom modules
 list (APPEND CMAKE_MODULE_PATH
-  "${CMAKE_CURRENT_SOURCE_DIR}/cmake")
+        "${CMAKE_CURRENT_SOURCE_DIR}/cmake")
 
 
-option (SEAHORN_STATIC_EXE "Static executable." OFF)
+option (FreqHorn_STATIC_EXE "Static executable." OFF)
 
 set (CUSTOM_BOOST_ROOT "" CACHE PATH "Path to custom boost installation.")
 if (CUSTOM_BOOST_ROOT)
@@ -46,41 +44,42 @@ set (BOOST_COMPONENTS system)
 if (UNIT_TESTS)
   set (BOOST_COMPONENTS ${BOOST_COMPONENTS} unit_test_framework)
 endif()
-  find_package (Boost 1.55 REQUIRED COMPONENTS ${BOOST_COMPONENTS})
+find_package (Boost 1.71 REQUIRED COMPONENTS ${BOOST_COMPONENTS})
 if (Boost_FOUND)
   include_directories (${Boost_INCLUDE_DIRS})
 endif ()
 
 include(ExternalProject)
 set_property(DIRECTORY PROPERTY EP_STEP_TARGETS configure build test)
 
-set (Z3_TAG "origin/spacer3" CACHE STRING "Z3 git tag to use")
-set (Z3_REPO "https://bitbucket.org/spacer/code.git" CACHE STRING "Z3 repo")
+set (Z3_TAG "z3-4.8.17" CACHE STRING "Z3 git tag to use")
+set (Z3_REPO "https://github.com/Z3Prover/z3.git" CACHE STRING "Z3 repo")
 if (CMAKE_BUILD_TYPE STREQUAL "Debug")
   set (Z3_DEBUG "-d")
 else()
   set (Z3_DEBUG "")
 endif()
 
 ExternalProject_Add(z3
-  GIT_REPOSITORY  ${Z3_REPO}
-  GIT_TAG ${Z3_TAG}
-  BUILD_IN_SOURCE 1
-  INSTALL_DIR ${CMAKE_BINARY_DIR}/run
-  CONFIGURE_COMMAND env CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER}
-  ./configure -p <INSTALL_DIR> -b build --staticlib ${Z3_DEBUG}
-  BUILD_COMMAND make -j3 -C build
-  INSTALL_COMMAND make -C build install
-  COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_LIST_FILE}
-  LOG_CONFIGURE 1
-  LOG_INSTALL 1
-  LOG_BUILD 1)
-
-find_package(Z3 4.3.2)
+        GIT_REPOSITORY  ${Z3_REPO}
+        GIT_TAG ${Z3_TAG}
+        BUILD_IN_SOURCE 1
+        INSTALL_DIR ${CMAKE_BINARY_DIR}/run
+        CONFIGURE_COMMAND env CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER}
+        ./configure -p <INSTALL_DIR> -b build --staticlib ${Z3_DEBUG}
+        BUILD_COMMAND make -j3 -C build
+        INSTALL_COMMAND make -C build install
+        COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_LIST_FILE}
+        LOG_CONFIGURE 1
+        LOG_INSTALL 1
+        LOG_BUILD 1)
+
+find_package(Z3 4.8.17)
 if (NOT Z3_FOUND)
   ExternalProject_Get_Property (z3 INSTALL_DIR)
   set(Z3_ROOT ${INSTALL_DIR} CACHE PATH "Forced location of Z3" FORCE)
   message(WARNING "No Z3 found. Run \n\tcmake --build . && cmake ${CMAKE_SOURCE_DIR}")
+  return()
 else()
   set_target_properties(z3 PROPERTIES EXCLUDE_FROM_ALL ON)
   include_directories(${Z3_INCLUDE_DIR})
@@ -89,86 +88,28 @@ else()
   install (PROGRAMS ${Z3_EXECUTABLE} DESTINATION bin)
 endif()
 
-ExternalProject_Add (llvm
-  SVN_REPOSITORY http://llvm.org/svn/llvm-project/llvm/tags/RELEASE_360/final/
-  SOURCE_DIR ${CMAKE_SOURCE_DIR}/ext/llvm
-  INSTALL_DIR ${CMAKE_BINARY_DIR}/run
-  CMAKE_ARGS
-  -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}
-  -DCMAKE_BUILD_TYPE:STRING=${CMAKE_BUILD_TYPE}
-  -DCMAKE_INSTALL_PREFIX:PATH=<INSTALL_DIR>
-  -DLLVM_TARGETS_TO_BUILD:STRING=X86 -DWITH_POLY:BOOL=OFF
-  -DLLVM_ENABLE_PEDANTIC=OFF
-  -DLLVM_ENABLE_PIC=ON -DLLVM_REQUIRES_RTTI:BOOL=TRUE
-  TEST_AFTER_INSTALL 1
-  TEST_COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_LIST_FILE}
-  LOG_CONFIGURE 1
-  LOG_BUILD 1
-  LOG_INSTALL 1)
-
-find_package (LLVM 3.6.0 CONFIG NO_DEFAULT_PATH)
-if (NOT LLVM_FOUND)
-  ExternalProject_Get_Property (llvm INSTALL_DIR)
-  set (LLVM_ROOT ${INSTALL_DIR})
-  set (LLVM_DIR ${LLVM_ROOT}/share/llvm/cmake CACHE PATH
-    "Forced location of LLVM cmake config" FORCE)
-  message (WARNING "No llvm found. Run \n\tcmake --build . && cmake ${CMAKE_SOURCE_DIR}")
-  return()
-else()
-  set_target_properties(llvm PROPERTIES EXCLUDE_FROM_ALL ON)
-
-  message(STATUS "Found LLVM ${LLVM_PACKAGE_VERSION}")
-  message(STATUS "Using LLVMConfig.cmake in: ${LLVM_DIR}")
-
-  # We incorporate the CMake features provided by LLVM:
-  list(APPEND CMAKE_MODULE_PATH "${LLVM_CMAKE_DIR}")
-  include(AddLLVM)
-  include(HandleLLVMOptions)
-  set(LLVM_RUNTIME_OUTPUT_INTDIR ${CMAKE_BINARY_DIR}/${CMAKE_CFG_INTDIR}/bin)
-  set(LLVM_LIBRARY_OUTPUT_INTDIR ${CMAKE_BINARY_DIR}/${CMAKE_CFG_INTDIR}/lib)
-
-  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${LLVM_CXXFLAGS}")
-  set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LLVM_LDFLAGS}")
-
-  set(LLVM_REQUIRES_RTTI TRUE)
-  set(LLVM_REQUIRES_EH TRUE)
-
-  include_directories(${LLVM_INCLUDE_DIRS})
-  link_directories(${LLVM_LIBRARY_DIRS})
-  add_definitions(${LLVM_DEFINITIONS})
-
-endif()
-
-
 install (FILES ${CMAKE_CURRENT_SOURCE_DIR}/README.md DESTINATION .)
 # install all the licenses
 install (FILES  ${CMAKE_CURRENT_SOURCE_DIR}/license.txt
-  DESTINATION share/doc/seahorn
-  RENAME seahorn_license.txt)
+        DESTINATION share/doc/FreqHorn
+        RENAME FreqHorn_license.txt)
 
 if (EXISTS z3-prefix/src/z3/LICENSE.txt)
   install (
-    FILES
-    ${CMAKE_CURRENT_BINARY_DIR}/z3-prefix/src/z3/LICENSE.txt
-    DESTINATION share/doc/seahorn
-    RENAME z3_license.txt)
-endif()
-
-if (EXISTS ${CMAKE_CURRENT_BINARY_DIR}/llvm-prefix/src/llvm-build/bin/clang-3.6)
-  install (
-    PROGRAMS
-    ${CMAKE_CURRENT_BINARY_DIR}/llvm-prefix/src/llvm-build/bin/clang-3.6
-    DESTINATION bin)
+          FILES
+          ${CMAKE_CURRENT_BINARY_DIR}/z3-prefix/src/z3/LICENSE.txt
+          DESTINATION share/doc/FreqHorn
+          RENAME z3_license.txt)
 endif()
 
 if (EXISTS ${CMAKE_CURRENT_BINARY_DIR}/z3-prefix/src/z3/build)
   file(GLOB z3py
-    ${CMAKE_CURRENT_BINARY_DIR}/z3-prefix/src/z3/build/*.py?
-    ${CMAKE_CURRENT_BINARY_DIR}/z3-prefix/src/z3/build/*.py?
-    ${CMAKE_CURRENT_BINARY_DIR}/z3-prefix/src/z3/build/*.so
-    ${CMAKE_CURRENT_BINARY_DIR}/z3-prefix/src/z3/build/*.dylib
-    ${CMAKE_CURRENT_BINARY_DIR}/z3-prefix/src/z3/build/*.dll
-    )
+          ${CMAKE_CURRENT_BINARY_DIR}/z3-prefix/src/z3/build/*.py?
+          ${CMAKE_CURRENT_BINARY_DIR}/z3-prefix/src/z3/build/*.py?
+          ${CMAKE_CURRENT_BINARY_DIR}/z3-prefix/src/z3/build/*.so
+          ${CMAKE_CURRENT_BINARY_DIR}/z3-prefix/src/z3/build/*.dylib
+          ${CMAKE_CURRENT_BINARY_DIR}/z3-prefix/src/z3/build/*.dll
+          )
   install(FILES ${z3py} DESTINATION lib/z3py)
 endif()
 
@@ -182,31 +123,41 @@ else()
 endif()
 
 find_package(OpenMP)
-set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${OpenMP_CXX_FLAGS}")
+if (OPENMP_FOUND)
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${OpenMP_CXX_FLAGS}")
+  #set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fopenmp")
+endif()
+
+find_package(Armadillo)
+if (ARMADILLO_FOUND)
+  add_definitions(-DHAVE_ARMADILLO)
+  include_directories(${ARMADILLO_INCLUDE_DIR})
+endif()
 
 install(DIRECTORY include/
-  DESTINATION include
-  FILES_MATCHING
-  PATTERN "*.hpp"
-  PATTERN "*.hh"
-  PATTERN "*.h"
-  PATTERN ".svn" EXCLUDE
-  )
+        DESTINATION include
+        FILES_MATCHING
+        PATTERN "*.hpp"
+        PATTERN "*.hh"
+        PATTERN "*.h"
+        PATTERN ".svn" EXCLUDE
+        )
 
 install(DIRECTORY ${CMAKE_BINARY_DIR}/include/
-  DESTINATION include
-  FILES_MATCHING
-  PATTERN "*.hpp"
-  PATTERN "*.hh"
-  PATTERN "*.h"
-  PATTERN "CMakeFiles" EXCLUDE
-  PATTERN ".svn" EXCLUDE
-  )
+        DESTINATION include
+        FILES_MATCHING
+        PATTERN "*.hpp"
+        PATTERN "*.hh"
+        PATTERN "*.h"
+        PATTERN "CMakeFiles" EXCLUDE
+        PATTERN ".svn" EXCLUDE
+        )
 
 set(CMAKE_CXX_EXTENSIONS ON)
 add_definitions(-Wno-redeclared-class-member -Wno-sometimes-uninitialized)
 add_definitions(-Wno-covered-switch-default)
 add_definitions(-Wno-inconsistent-missing-override)
+set(CMAKE_CXX_STANDARD 11)
 if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")
   add_definitions( -Wno-unused-local-typedefs)
 endif ()
@@ -217,7 +168,7 @@ include_directories(BEFORE ${CMAKE_CURRENT_BINARY_DIR}/include)
 ### add our include directories to the front, overriding directories
 ### specified by external packages.
 include_directories(BEFORE
-  ${CMAKE_CURRENT_SOURCE_DIR}/include
-  ${CMAKE_CURRENT_BINARY_DIR}/include)
+        ${CMAKE_CURRENT_SOURCE_DIR}/include
+        ${CMAKE_CURRENT_BINARY_DIR}/include)
 
 add_subdirectory(tools)

README.md

@@ -1,13 +1,34 @@
-#About#
-
-Skolemizer for AE-formulas in LIA/LRA based on the <a href="http://seahorn.github.io/">SeaHorn</a> verification framework and the <a href="https://github.com/Z3Prover/z3">Z3</a> SMT solver. This is the main computational engine used in the Incremental Model Checking (<a href="http://www.inf.usi.ch/phd/fedyukovich/simabs_paper.pdf">LPAR'15</a>, <a href="http://www.inf.usi.ch/phd/fedyukovich/pde_paper.pdf">CAV'16</a>) and in the Program Synthesis from Assume-Guarantee contracts (<a href="https://arxiv.org/abs/1610.05867">preprint</a>).
-
-#Installation#
-
-* `cd aeval ; mkdir build ; cd build`
-* `cmake ../`
-* `make` to build dependencies (Z3 and LLVM)
-* `make` to build AE-VAL
-
-The binary of AE-VAL can be found in `build/tools/aeval/`
-
+TG-nonlin
+========
+
+Maximizing Branch Coverage with Constrained Horn Clauses
+for Solidity Language 
+
+Installation
+============
+
+Assumes preinstalled Boost (e.g., 1.75.0) and Gmp (e.g. 10.4.0) packages. 
+
+* `git clone https://github.com/izlatkin/aeval`
+* `cd aeval`
+* `git checkout tg-nonlin`
+* `mkdir build ; cd build`
+* `cmake ../`
+* `cmake --build .  && cmake {PATH_TO_REPO}/aeval`
+* `make` (again) to build TG
+
+The binary of TG-nonlin can be found at `build/tools/nonlin/tgnonlin`.
+Note that TG-nonlin comes with its own version of Z3
+
+HowTo
+==========
+`./tools/nonlin/tgnonlin <options> file.smt2`
+generated raw tests dumped to `testgen.txt` file 
+
+Benchmarks
+==========
+
+Collection of the Solidity files
+https://github.com/leonardoalt/cav_2022_artifact/tree/main/regression
+sol files should be encoded to smt2 format (see: https://github.com/izlatkin/solidity_testgen)
+