Adt chc

CMakeLists.txt

@@ -1,18 +1,16 @@
 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 (ADTIND)
+set (ADTIND_VERSION_MAJOR 0)
+set (ADTIND_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}")
+    "${ADTIND_VERSION_MAJOR}.${ADTIND_VERSION_MINOR}.${ADTIND_VERSION_PATCH}")
+  if (DEFINED ADTIND_VERSION_TWEAK)
+    set (PACKAGE_VERSION "${PACKAGE_VERSION}-${ADTIND_VERSION_TWEAK}")
   endif()
-  set (SeaHorn_VERSION_INFO ${PACKAGE_VERSION})
+  set (ADTIND_VERSION_INFO ${PACKAGE_VERSION})
 endif()
 
 
@@ -29,7 +27,7 @@ list (APPEND CMAKE_MODULE_PATH
   "${CMAKE_CURRENT_SOURCE_DIR}/cmake")
 
 
-option (SEAHORN_STATIC_EXE "Static executable." OFF)
+option (ADTIND_STATIC_EXE "Static executable." OFF)
 
 set (CUSTOM_BOOST_ROOT "" CACHE PATH "Path to custom boost installation.")
 if (CUSTOM_BOOST_ROOT)
@@ -46,16 +44,16 @@ 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.10" 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()
@@ -76,11 +74,12 @@ ExternalProject_Add(z3
   LOG_INSTALL 1
   LOG_BUILD 1)
 
-find_package(Z3 4.3.2)
+find_package(Z3 4.8.1)
 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,78 +88,20 @@ 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/ADTIND
+  RENAME ADTIND_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
+    DESTINATION share/doc/ADTIND
     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)
-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?
@@ -182,7 +123,10 @@ 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()
 
 install(DIRECTORY include/
   DESTINATION include
@@ -207,6 +151,7 @@ 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 ()

README.md

@@ -1,13 +1,27 @@
-#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/`
-
+About
+=====
+
+Skolemizer for AE-formulas in LIA/LRA based on the Expression library of <a href="http://seahorn.github.io/">SeaHorn</a> 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
+============
+
+Compiles with gcc-5 (on Linux) and clang-700 (on Mac). Assumes preinstalled Gmp and Boost v1.67 packages.
+
+* `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/`.
+
+Benchmarks
+==========
+
+Each benchmark is split into two files (for the universal and the existential parts of the formula). AE-VAL either returns `Valid` (with a skolem) or `Invalid`. Collection of the formulas can be found at `bench/tasks/` and the expected skolems at `bench/skolems/`.
+
+For example, if AE-VAL is run with the following input:
+
+`./build/tools/aeval/aeval bench/tasks/fast_1_e8_747_extend_s_part.smt2 bench/tasks/fast_1_e8_747_extend_t_part.smt2 `
+
+Then, the output is `Valid` and the synthesized skolem should be close enough to the formula in `bench/skolems/fast_1_e8_747_extend_skolem.smt2`.

bench/run-bench.sh

@@ -0,0 +1,49 @@
+#!/bin/bash
+echo "This is the script for running regression tests"
+echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')"
+echo " - host name $(hostname -f)"
+echo " - script path: $(readlink -f $0)"
+
+adtchc=../adtchc
+if [[ ! $# -eq 0 ]] ; then
+    #echo 'Setting path to' $1
+    adtchc=$1
+fi
+
+# run the interpolating version of OpenSMT
+adtchc=${adtchc}' -i'
+
+picky=./utils/picky.smt2
+lookahead=./utils/lookahead.smt2
+
+tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S')
+mkdir ${tmpfolder}
+
+export outmod=false
+export errmod=false
+export rtmod=false
+export err=false
+
+for file in $(find . -name '*.smt2' |sort); do
+    name=$(basename $file)
+    dir=$(dirname $file)
+
+    sh -c "ulimit -St 60; ${adtchc} $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null
+    grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err
+
+    if [ -s "$tmpfolder/$name.err" ]; then
+        echo "stderr not empty for benchmark $file";
+        err=true;
+    fi
+
+
+done
+#echo "Stdout differs: ${outmod}, stderr differs: ${errmod}"
+
+if [[ ${err} == true ]]; then
+    echo "There were anomalies: check logs in ${tmpfolder}"
+    exit 1
+else
+    rm -rf ${tmpfolder}
+fi
+

bench/skolems/PRODUCER_CONSUMER_2_base_skolem.smt2

@@ -0,0 +1,22 @@
+(declare-fun $V74_X$2 () Bool)
+(declare-fun $V87_First$2 () Int)
+(declare-fun $V79_Sofar$2 () Bool)
+(declare-fun $etat1$0 () Bool)
+(declare-fun $V31_env$2 () Bool)
+(declare-fun $a_init$0 () Int)
+(declare-fun $OK$2 () Bool)
+(declare-fun $V26_i$2 () Int)
+(declare-fun $etat3$0 () Bool)
+(declare-fun $etat2$0 () Bool)
+
+(assert (let ((a!1 (and (not $etat1$0) (not (and $etat2$0 $etat3$0)) (> $a_init$0 0))))
+(let ((a!2 (and (= $OK$2 (or (not a!1) (>= 0 0)))
+                (= $V31_env$2 a!1)
+                (= $V26_i$2 0)
+                (= $V79_Sofar$2 (not (and $etat2$0 $etat3$0)))
+                (= $V87_First$2 $a_init$0)
+                (= $V74_X$2 (not (and $etat2$0 $etat3$0))))))
+  (ite (and $etat2$0 $etat3$0)
+       a!2
+       (ite (or (not $etat2$0) (not $etat3$0)) a!2 true)))))
+(check-sat)

bench/skolems/PRODUCER_CONSUMER_2_extend_skolem.smt2

@@ -0,0 +1,52 @@
+(declare-fun $V87_First$2 () Int)
+(declare-fun $V74_X$2 () Bool)
+(declare-fun $etat1$0 () Bool)
+(declare-fun $V26_i$2 () Int)
+(declare-fun %init () Bool)
+(declare-fun $V31_env$2 () Bool)
+(declare-fun $V79_Sofar$~1 () Bool)
+(declare-fun $V79_Sofar$2 () Bool)
+(declare-fun $OK$2 () Bool)
+(declare-fun $V87_First$~1 () Int)
+(declare-fun $a_init$0 () Int)
+(declare-fun $etat3$0 () Bool)
+(declare-fun $etat2$0 () Bool)
+
+(assert (let ((a!1 (and %init (= (+ (* (- 1) $a_init$0) $V87_First$~1) 0)))
+      (a!2 (ite %init
+                (not (and $etat2$0 $etat3$0))
+                (and (not (and $etat2$0 $etat3$0)) $V79_Sofar$~1)))
+      (a!6 (and (not %init) (= (+ (* (- 1) $V87_First$~1) $a_init$0) 0))))
+(let ((a!3 (and (and (ite %init (not $etat1$0) true) a!2) (> $V87_First$~1 0)))
+      (a!5 (and (or (not $etat2$0) (not $etat3$0))
+                (or %init (and (not %init) $V79_Sofar$~1))
+                (or a!1 (not %init))))
+      (a!7 (and (and (ite %init (not $etat1$0) true) a!2) (> $a_init$0 0)))
+      (a!9 (and (or (not $etat2$0) (not $etat3$0))
+                (or %init (and (not %init) $V79_Sofar$~1))
+                (or %init a!6))))
+(let ((a!4 (and (= $OK$2 (or (not a!3) (>= 0 0)))
+                (= $V31_env$2 a!3)
+                (= $V26_i$2 0)
+                (= $V79_Sofar$2 a!2)
+                (= $V87_First$2 $V87_First$~1)
+                (= $V74_X$2 (not (and $etat2$0 $etat3$0)))))
+      (a!8 (and (= $OK$2 (or (>= 0 0) (not a!7)))
+                (= $V31_env$2 a!7)
+                (= $V26_i$2 0)
+                (= $V79_Sofar$2 a!2)
+                (= $V87_First$2 $a_init$0)
+                (= $V74_X$2 (not (and $etat2$0 $etat3$0))))))
+(let ((a!10 (ite a!5
+                 a!4
+                 (ite (and $etat2$0 $etat3$0 (or %init a!6))
+                      a!8
+                      (ite a!9 a!8 true)))))
+(let ((a!11 (ite (and (or (not $etat2$0) (not $etat3$0))
+                      (not %init)
+                      (not $V79_Sofar$~1)
+                      (or a!1 (not %init)))
+                 a!4
+                 a!10)))
+  (ite (and $etat2$0 $etat3$0 (or a!1 (not %init))) a!4 a!11)))))))
+(check-sat)

bench/skolems/SYNAPSE_2_e8_1118_e7_1043_base_skolem.smt2

@@ -0,0 +1,21 @@
+(declare-fun $V83_X$2 () Bool)
+(declare-fun $V28_valid_s$2 () Int)
+(declare-fun $V27_invalid_s$2 () Int)
+(declare-fun $init_invalid_s$0 () Int)
+(declare-fun $e_s2$0 () Bool)
+(declare-fun $e_s3$0 () Bool)
+(declare-fun $e_s1$0 () Bool)
+(declare-fun $V29_dirty_s$2 () Int)
+(declare-fun $V31_env$2 () Bool)
+(declare-fun $OK$2 () Bool)
+
+(assert (let ((a!1 (and (not (or (and $e_s1$0 $e_s2$0 $e_s1$0 $e_s3$0)
+                         (and $e_s2$0 $e_s3$0)))
+                (>= $init_invalid_s$0 0))))
+  (and (= $OK$2 true)
+       (= $V31_env$2 a!1)
+       (= $V27_invalid_s$2 0)
+       (= $V28_valid_s$2 0)
+       (= $V29_dirty_s$2 0)
+       (= $V83_X$2 a!1))))
+(check-sat)