Basic CHC Encoding

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\)\)\)\)\)$
+--

regression/goto-instrument-chc/chain.sh

@@ -0,0 +1,23 @@
+#!/bin/bash
+
+set -e
+
+goto_cc=$1
+goto_instrument=$2
+
+sources=${*:$#}
+args=${*:3:$#-3}
+
+set -- $sources
+target=${*:$#}
+target=${target%.c}
+
+if [[ `basename "${goto_cc}"` == "goto-cl" || `basename "${goto_cc}"` == "goto-cl.exe" ]]; then
+  $goto_cc ${sources} "/Fe${target}.gb"
+else
+  $goto_cc -o ${target}.gb ${sources}
+fi
+
+echo DOING: $goto_instrument ${args} "${target}.gb"
+
+$goto_instrument ${args} "${target}.gb"

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -848,7 +848,7 @@ int goto_instrument_parse_optionst::doit()
       remove_skip(goto_model);
     }
 
-    if(cmdline.isset("horn-encoding"))
+    if(cmdline.isset("horn"))
     {
       log.status() << "Horn-clause encoding" << messaget::eom;
       namespacet ns(goto_model.symbol_table);