Merge pull request #6807 from diffblue/variable_encoding

Basic CHC Encoding

Author: tautschnig

regression/CMakeLists.txt

@@ -36,6 +36,7 @@ add_subdirectory(cbmc-incr-smt2)
 add_subdirectory(cbmc-incr)
 add_subdirectory(cbmc-with-incr)
 add_subdirectory(array-refinement-with-incr)
+add_subdirectory(goto-instrument-chc)
 add_subdirectory(goto-instrument-json)
 add_subdirectory(goto-instrument-wmm-core)
 add_subdirectory(goto-instrument-typedef)

regression/Makefile

@@ -15,6 +15,7 @@ DIRS = cbmc \
        cbmc-incr \
        cbmc-with-incr \
        array-refinement-with-incr \
+       goto-instrument-chc \
        goto-instrument-json \
        goto-instrument-wmm-core \
        goto-instrument-typedef \

regression/goto-instrument-chc/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument>"
+)

regression/goto-instrument-chc/Makefile

@@ -0,0 +1,28 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
+
+test:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument'
+
+tests.log:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument'
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/goto-instrument-chc/basic/basic5.c

@@ -0,0 +1,10 @@
+int main()
+{
+  int x;
+  __CPROVER_bool c1 = (x >= 10);
+  __CPROVER_bool c2 = (x >= 5);
+  // clang-format off
+  __CPROVER_assert(c1 ==> c2, "property 1"); // passes
+  __CPROVER_assert(c2 ==> c1, "property 2"); // fails
+  return 0;
+}

regression/goto-instrument-chc/basic/basic5.desc

@@ -0,0 +1,9 @@
+CORE
+basic5.c
+--horn
+^EXIT=0$
+^SIGNAL=0$
+^\(assert \(forall \( \(|__CPROVER_rounding_mode| \(_ BitVec 32\)\) \(|main::1::c1| Bool\) \(|main::1::c2| Bool\) \(|main::1::x| \(_ BitVec 32\)\) \(|return_value| \(_ BitVec 32\)\) \) \(=> \(|S31.24| |__CPROVER_rounding_mode| |main::1::c1| |main::1::c2| |main::1::x| |return_value|\) \(|S32Entry| |__CPROVER_rounding_mode| |main::1::c1| |main::1::c2| |main::1::x| |return_value|\)\)\)\)$
+^\(assert \(forall \( \(|__CPROVER_rounding_mode| \(_ BitVec 32\)\) \(|main::1::c1| Bool\) \(|main::1::c2| Bool\) \(|main::1::x| \(_ BitVec 32\)\) \(|return_value| \(_ BitVec 32\)\) \) \(=> \(|S32Entry| |__CPROVER_rounding_mode| |main::1::c1| |main::1::c2| |main::1::x| |return_value|\) \(|S32.2| |__CPROVER_rounding_mode| \(bvsge |main::1::x| \(_ bv10 32\)\) |main::1::c2| |main::1::x| |return_value|\)\)\)\)$
+^\(assert \(forall \( \(|__CPROVER_rounding_mode| \(_ BitVec 32\)\) \(|main::1::c1| Bool\) \(|main::1::c2| Bool\) \(|main::1::x| \(_ BitVec 32\)\) \(|return_value| \(_ BitVec 32\)\) \) \(=> \(|S32.2| |__CPROVER_rounding_mode| |main::1::c1| |main::1::c2| |main::1::x| |return_value|\) \(|S32.4| |__CPROVER_rounding_mode| |main::1::c1| \(bvsge |main::1::x| \(_ bv5 32\)\) |main::1::x| |return_value|\)\)\)\)$
+--

regression/goto-instrument-chc/basic/basic6.c

@@ -0,0 +1,12 @@
+int x;
+
+int main()
+{
+  x = 1;
+  x++;
+  x++;
+  x++;
+  x++;
+  __CPROVER_assert(x == 5, "property 1");
+  return 0;
+}

regression/goto-instrument-chc/basic/basic6.desc

@@ -0,0 +1,8 @@
+CORE
+basic6.c
+--horn
+^EXIT=0$
+^SIGNAL=0$
+^\(assert \(forall \( \(|__CPROVER_rounding_mode| \(_ BitVec 32\)\) \(|return_value| \(_ BitVec 32\)\) \(|x| \(_ BitVec 32\)\) \) \(=> \(|S11Entry| |__CPROVER_rounding_mode| |return_value| |x|\) \(|S11\.0| |__CPROVER_rounding_mode| |return_value| \(_ bv1 32\)\)\)\)\)$
+^\(assert \(forall \( \(|__CPROVER_rounding_mode| \(_ BitVec 32\)\) \(|return_value| \(_ BitVec 32\)\) \(|x| \(_ BitVec 32\)\) \) \(=> \(|S11\.0| |__CPROVER_rounding_mode| |return_value| |x|\) \(|S11\.1| |__CPROVER_rounding_mode| |return_value| \(bvadd |x| \(_ bv1 32\)\)\)\)\)\)$
+--

regression/goto-instrument-chc/basic/nondet1.c

@@ -0,0 +1,14 @@
+int nondet_int();
+
+int main()
+{
+  int x, y;
+
+  x = nondet_int();
+  __CPROVER_assert(x == 20, "property 1"); // fails
+
+  y = nondet_int();
+  __CPROVER_assert(x == y, "property 2"); // fails
+
+  return 0;
+}

regression/goto-instrument-chc/basic/nondet1.desc

@@ -0,0 +1,8 @@
+CORE
+nondet1.c
+--horn
+^EXIT=0$
+^SIGNAL=0$
+^\(assert \(forall \( \(|__CPROVER_rounding_mode| \(_ BitVec 32\)\) \(|main::1::x| \(_ BitVec 32\)\) \(|main::1::y| \(_ BitVec 32\)\) \(|return_value| \(_ BitVec 32\)\) \) \(=> \(|S30Entry| |__CPROVER_rounding_mode| |main::1::x| |main::1::y| |return_value|\) \(|S30\.2| |__CPROVER_rounding_mode| |nondet::S30\.2| |main::1::y| |return_value|\)\)\)\)$
+^\(assert \(forall \( \(|__CPROVER_rounding_mode| \(_ BitVec 32\)\) \(|main::1::x| \(_ BitVec 32\)\) \(|main::1::y| \(_ BitVec 32\)\) \(|return_value| \(_ BitVec 32\)\) \) \(=> \(|S30\.2| |__CPROVER_rounding_mode| |main::1::x| |main::1::y| |return_value|\) \(= |main::1::x| \(_ bv20 32\)\)\)\)\)$
+--