Merge pull request #884 from nmanthey/ipasir-no-ci

kroening · web-flow · commit 5196e40cf722 · 2017-10-30T06:40:41.000Z
ipasir modification without CI integration
diff --git a/COMPILING.md b/COMPILING.md
@@ -46,6 +46,19 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    make
    ```
 
+4. Linking against an IPASIR SAT solver
+
+   Get an IPASIR package and build picosat by default
+   ```
+   make -C src ipasir-build
+   ```
+
+   Build CBMC with IPASIR and link against the ipasir solver library
+   Note: the LIBSOLVER variable could be pointed towards other solvers
+   ```
+   make -C src IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a
+   ```
+
 # COMPILATION ON SOLARIS 11
 
 1. As root, get the necessary development tools:
diff --git a/regression/cbmc-concurrency/pthread_join1/test.desc b/regression/cbmc-concurrency/pthread_join1/test.desc
@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] assertion i==1: FAILURE$
 ^\[main\.assertion\.2\] assertion i==2: SUCCESS$
-^\*\* 1 of 2 failed \(2 iterations\)$
+^\*\* 1 of 2 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc1/test.desc b/regression/cbmc-cover/mcdc1/test.desc
@@ -10,6 +10,5 @@ main.c
 ^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$
 ^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 10 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc11/test.desc b/regression/cbmc-cover/mcdc11/test.desc
@@ -10,6 +10,5 @@ main.c
 ^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE.*: SATISFIED$
 ^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 6 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc12/test.desc b/regression/cbmc-cover/mcdc12/test.desc
@@ -13,6 +13,5 @@ main.c
 ^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && F != FALSE.*: SATISFIED$
 ^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && !\(F != FALSE\).*: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 10 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc14/test.desc b/regression/cbmc-cover/mcdc14/test.desc
@@ -6,6 +6,5 @@ main.c
 ^\[main.coverage.1\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
 ^\[main.coverage.2\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 2 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc3/test.desc b/regression/cbmc-cover/mcdc3/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && !\(x > \(unsigned int\)3\).*: SATISFIED$
 ^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && x > \(unsigned int\)3.*: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 4 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc4/test.desc b/regression/cbmc-cover/mcdc4/test.desc
@@ -9,6 +9,5 @@ main.c
 ^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
 ^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 9 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc6/test.desc b/regression/cbmc-cover/mcdc6/test.desc
@@ -6,6 +6,5 @@ main.c
 ^\[main.coverage.1\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* false: SATISFIED$
 ^\[main.coverage.2\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* true: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 2 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc7/test.desc b/regression/cbmc-cover/mcdc7/test.desc
@@ -8,6 +8,5 @@ main.c
 ^\[main.coverage.3\] file main.c line 8 function main decision/condition `x \* 123 < 0.* false: SATISFIED$
 ^\[main.coverage.4\] file main.c line 8 function main decision/condition `x \* 123 < 0.* true: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 2 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc8/test.desc b/regression/cbmc-cover/mcdc8/test.desc
@@ -8,6 +8,5 @@ main.c
 ^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !\(a != FALSE\) && !\(b != FALSE\).* SATISFIED$
 ^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(c != FALSE\) && a != FALSE && !\(b != FALSE\).* SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 6 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc9/test.desc b/regression/cbmc-cover/mcdc9/test.desc
@@ -9,6 +9,5 @@ main.c
 ^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && C != FALSE && !\(D != FALSE\).* SATISFIED$
 ^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 8 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/exceptions1/test.desc b/regression/cbmc-java/exceptions1/test.desc
@@ -4,7 +4,7 @@ test.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file test.java line 26 function.*: FAILURE$
-\*\* 1 of [0-9]* failed \(2 iterations\)$
+\*\* 1 of [0-9]* failed 
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/exceptions2/test.desc b/regression/cbmc-java/exceptions2/test.desc
@@ -4,7 +4,7 @@ test.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file test.java line 15 function.*: FAILURE$
-^\*\* 1 of [0-9]* failed \(2 iterations\)$
+^\*\* 1 of [0-9]* failed 
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc b/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc
@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] assertion matriz\[\(signed long int\)j\]\[\(signed long int\)k\] <= maior: OK$
 ^\[main\.assertion\.2\] assertion matriz\[\(signed long int\)0\]\[\(signed long int\)0\] < maior: FAILED$
-^\*\* 1 of 2 failed \(2 iterations\)$
+^\*\* 1 of 2 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.2\] .*: FAILED$
-^\*\* 1 of 2 failed \(2 iterations\)$
+^\*\* 1 of 2 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.array_bounds\.5\] array.List upper bound in .*: FAILED$
-^\*\* 1 of 9 failed \(2 iterations\)$
+^\*\* 1 of 9 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.array_bounds\.5\] array.List upper bound: FAILED$
-^\*\* 1 of 9 failed \(2 iterations\)$
+^\*\* 1 of 9 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/pipe1/test.desc b/regression/cbmc-with-incr/pipe1/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.4\] assertion data\[1\]==31: FAILED$
-^\*\* 1 of 5 failed \(2 iterations\)$
+^\*\* 1 of 5 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc
@@ -7,6 +7,6 @@ pointer outside dynamic object bounds in \*p: FAILURE
 pointer outside dynamic object bounds in \*p: FAILURE
 pointer outside dynamic object bounds in p2\[.*1\]: FAILURE
 pointer outside dynamic object bounds in p2\[.*0\]: FAILURE
-\*\* 4 of 36 failed \(3 iterations\)
+\*\* 4 of 36 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Multi_Dimensional_Array6/test.desc b/regression/cbmc/Multi_Dimensional_Array6/test.desc
@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] : SUCCESS$
 ^\[main\.assertion\.2\] : FAILURE$
-^\*\* 1 of 2 failed \(2 iterations\)$
+^\*\* 1 of 2 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Pointer_byte_extract2/test.desc b/regression/cbmc/Pointer_byte_extract2/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.2\] .*: FAILURE$
-^\*\* 1 of 2 failed \(2 iterations\)$
+^\*\* 1 of 2 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 array\.List dynamic object upper bound in p->List\[2\]: FAILURE
-\*\* 1 of 11 failed \(2 iterations\)
+\*\* 1 of 11 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Pointer_byte_extract8/test.desc b/regression/cbmc/Pointer_byte_extract8/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.array_bounds\.5\] array.List upper bound: FAILED$
-^\*\* 1 of 9 failed \(2 iterations\)$
+^\*\* 1 of 9 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc
@@ -8,5 +8,5 @@ main.c
 ^\[main.assertion.4\] NotExists-Forall: failed: FAILURE$
 ^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$
 ^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
-^\*\* 2 of 6 failed \(2 iterations\)$
+^\*\* 2 of 6 failed 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc
@@ -6,5 +6,5 @@ main.c
 ^\[main.assertion.2\] assertion y: FAILURE$
 ^\[main.assertion.3\] assertion z1: SUCCESS$
 ^\[main.assertion.4\] assertion z2: SUCCESS$
-^\*\* 1 of 4 failed \(2 iterations\)$
+^\*\* 1 of 4 failed 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc
@@ -7,5 +7,5 @@ main.c
 ^\[main.assertion.3\] success 1: SUCCESS$
 ^\[main.assertion.4\] failure 3: FAILURE$
 ^\[main.assertion.5\] success 2: SUCCESS$
-^\*\* 3 of 5 failed \(2 iterations\)$
+^\*\* 3 of 5 failed 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc
@@ -7,5 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion a\[.*\] > a\[.*\]: FAILURE$
 ^\[main.assertion.4\] forall c\[\]: SUCCESS$
 ^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$
-^\*\* 1 of 5 failed \(2 iterations\)$
+^\*\* 1 of 5 failed 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc
@@ -7,5 +7,5 @@ main.c
 ^\[main.assertion.3\] failure 1: FAILURE$
 ^\[main.assertion.4\] success 3: SUCCESS$
 ^\[main.assertion.5\] failure 2: FAILURE$
-^\*\* 2 of 5 failed \(2 iterations\)$
+^\*\* 2 of 5 failed 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc
@@ -4,5 +4,5 @@ main.c
 ^\*\* Results:$
 ^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$
 ^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
-^\*\* 1 of 2 failed \(2 iterations\)$
+^\*\* 1 of 2 failed 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/fgets1/test.desc b/regression/cbmc/fgets1/test.desc
@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[main.assertion.3\] assertion p\[1\]=='b': FAILURE
-\*\* 1 of \d+ failed \(2 iterations\)
+\*\* 1 of \d+ failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc
@@ -7,6 +7,6 @@ main.c
 \[main.assertion.1\] assertion \*p==42: SUCCESS
 \[main.pointer_dereference.14\] dereference failure: pointer invalid in p\[.*1\]: FAILURE
 \[main.assertion.2\] assertion \*\(p\+1\)==42: SUCCESS
-\*\* 12 of 26 failed \(2 iterations\)
+\*\* 12 of 26 failed
 --
 ^warning: ignoring
diff --git a/regression/cbmc/memset1/test.desc b/regression/cbmc/memset1/test.desc
@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[main.assertion.7\] assertion A\[1\]==0x01010111: FAILURE
-\*\* 1 of 12 failed \(2 iterations\)
+\*\* 1 of 12 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/pipe1/test.desc b/regression/cbmc/pipe1/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.4\] assertion data\[1\]==31: FAILURE$
-^\*\* 1 of 5 failed \(2 iterations\)$
+^\*\* 1 of 5 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/pointer-function-parameters-2/test.desc b/regression/cbmc/pointer-function-parameters-2/test.desc
@@ -2,7 +2,6 @@ CORE
 main.c
 --function fun --cover branch
 ^\*\* 7 of 7 covered \(100.0%\)$
-^\*\* Used 4 iterations$
 ^Test suite:$
 ^a=\(\(signed int \*\*\)NULL\), tmp\$\d+=[^,]*, tmp\$\d+=[^,]*$
 ^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
diff --git a/regression/cbmc/pointer-function-parameters/test.desc b/regression/cbmc/pointer-function-parameters/test.desc
@@ -2,7 +2,6 @@ CORE
 main.c
 --function fun --cover branch
 ^\*\* 5 of 5 covered \(100\.0%\)$
-^\*\* Used 3 iterations$
 ^Test suite:$
 ^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
 ^a=&tmp\$\d+!0, tmp\$\d+=4$
diff --git a/regression/strings/test_pass1/test.desc b/regression/strings/test_pass1/test.desc
@@ -5,4 +5,4 @@ test.c
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): SUCCESS
 ^\[main.assertion.2\] assertion !__CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): FAILURE$
-^\*\* 1 of 2 failed \(2 iterations\)$
+^\*\* 1 of 2 failed 
diff --git a/src/Makefile b/src/Makefile
@@ -93,4 +93,17 @@ cprover-jar-build:
 	cd target; jar cf org.cprover.jar `find . -name "*.class"`; \
 	mv org.cprover.jar ../../../)
 
-.PHONY: minisat2-download glucose-download cprover-jar-build
+ipasir-download:
+	# get the 2016 version of the ipasir package, which contains a few solvers
+	@echo "Download ipasir 2016 package"
+	@(lwp-download http://baldur.iti.kit.edu/sat-competition-2016/downloads/ipasir.zip ../ipasir.zip)
+	@(cd ..; unzip -u ipasir.zip)
+
+ipasir-build: ipasir-download
+	# build libpicosat, and create a libipasir.a in ipasir directory
+	# make sure that the ipasir.h file is located there as well (ships with 2016 package)
+	@echo "Build Picosat 961 from ipasir 2016 package"
+	$(MAKE) -C ../ipasir/sat/picosat961 libipasirpicosat961.a
+	@(cd ../ipasir; ln -sf sat/picosat961/libipasirpicosat961.a libipasir.a)
+
+.PHONY: ipasir-build minisat2-download glucose-download cprover-jar-build
diff --git a/src/common b/src/common
@@ -155,6 +155,48 @@ else
   $(error Invalid setting for BUILD_ENV: $(BUILD_ENV_))
 endif
 
+# select default solver to be minisat2 if no other is specified
+ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(PRECOSAT),)
+  MINISAT2 = ../../minisat-2.2.1
+endif
+
+ifneq ($(IPASIR),)
+  CP_CXXFLAGS += -DHAVE_IPASIR
+endif
+
+ifneq ($(PRECOSAT),)
+  CP_CXXFLAGS += -DHAVE_PRECOSAT
+endif
+
+ifneq ($(PICOSAT),)
+  CP_CXXFLAGS += -DHAVE_PICOSAT
+endif
+
+ifneq ($(LINGELING),)
+  CP_CXXFLAGS += -DHAVE_LINGELING
+endif
+
+ifneq ($(CHAFF),)
+  CP_CXXFLAGS += -DHAVE_CHAFF
+endif
+
+ifneq ($(BOOLEFORCE),)
+  CP_CXXFLAGS += -DHAVE_BOOLEFORCE
+endif
+
+ifneq ($(MINISAT),)
+  CP_CXXFLAGS += -DHAVE_MINISAT
+endif
+
+ifneq ($(MINISAT2),)
+  CP_CXXFLAGS += -DHAVE_MINISAT2
+endif
+
+ifneq ($(GLUCOSE),)
+  CP_CXXFLAGS += -DHAVE_GLUCOSE
+endif
+
+
 
 first_target: all
 
diff --git a/src/config.inc b/src/config.inc
@@ -22,10 +22,15 @@ endif
 #CHAFF = ../../zChaff
 #BOOLEFORCE = ../../booleforce-0.4
 #MINISAT = ../../MiniSat-p_v1.14
-MINISAT2 = ../../minisat-2.2.1
+#MINISAT2 = ../../minisat-2.2.1
+#IPASIR = ../../ipasir
 #GLUCOSE = ../../glucose-syrup
 #SMVSAT =
 
+# Extra library for SAT solver. This should link to the archive file to be used
+# when linking against an IPASIR solver.
+LIBSOLVER =
+
 ifneq ($(PRECOSAT),)
   CP_CXXFLAGS += -DSATCHECK_PRECOSAT
 endif
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
diff --git a/src/solvers/prop/literal.h b/src/solvers/prop/literal.h
diff --git a/src/solvers/sat/satcheck.h b/src/solvers/sat/satcheck.h
diff --git a/src/solvers/sat/satcheck_ipasir.cpp b/src/solvers/sat/satcheck_ipasir.cpp
diff --git a/src/solvers/sat/satcheck_ipasir.h b/src/solvers/sat/satcheck_ipasir.h
