Skip to content

Commit c36170a

Browse files
kroeningkroening
committed
basic CHC encoding
This adds a basic encoding from goto programs into constrained Horn clause systems. It relies on inlining function calls, and does not support pointers.
1 parent 4ba287d commit c36170a

16 files changed

+1319
-5
lines changed

‎regression/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ add_subdirectory(cbmc-incr-smt2)
3636
add_subdirectory(cbmc-incr)
3737
add_subdirectory(cbmc-with-incr)
3838
add_subdirectory(array-refinement-with-incr)
39+
add_subdirectory(goto-instrument-chc)
3940
add_subdirectory(goto-instrument-json)
4041
add_subdirectory(goto-instrument-wmm-core)
4142
add_subdirectory(goto-instrument-typedef)

‎regression/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ DIRS = cbmc \
1515
cbmc-incr \
1616
cbmc-with-incr \
1717
array-refinement-with-incr \
18+
goto-instrument-chc \
1819
goto-instrument-json \
1920
goto-instrument-wmm-core \
2021
goto-instrument-typedef \

‎regression/goto-instrument-chc/CMakeLists.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
add_test_pl_tests(
2+
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument>"
3+
)

‎regression/goto-instrument-chc/Makefile

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
default: tests.log
2+
3+
include ../../src/config.inc
4+
include ../../src/common
5+
6+
ifeq ($(BUILD_ENV_),MSVC)
7+
exe=../../../src/goto-cc/goto-cl
8+
is_windows=true
9+
else
10+
exe=../../../src/goto-cc/goto-cc
11+
is_windows=false
12+
endif
13+
14+
test:
15+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument'
16+
17+
tests.log:
18+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument'
19+
20+
clean:
21+
@for dir in *; do \
22+
$(RM) tests.log; \
23+
if [ -d "$$dir" ]; then \
24+
cd "$$dir"; \
25+
$(RM) *.out *.gb; \
26+
cd ..; \
27+
fi \
28+
done

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
int main()
2+
{
3+
int x;
4+
__CPROVER_bool c1 = (x >= 10);
5+
__CPROVER_bool c2 = (x >= 5);
6+
// clang-format off
7+
__CPROVER_assert(c1 ==> c2, "property 1"); // passes
8+
__CPROVER_assert(c2 ==> c1, "property 2"); // fails
9+
return 0;
10+
}

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
basic5.c
3+
--horn
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\(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|\)\)\)\)$
7+
^\(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|\)\)\)\)$
8+
^\(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|\)\)\)\)$
9+
--

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
int x;
2+
3+
int main()
4+
{
5+
x = 1;
6+
x++;
7+
x++;
8+
x++;
9+
x++;
10+
__CPROVER_assert(x == 5, "property 1");
11+
return 0;
12+
}

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
basic6.c
3+
--horn
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\(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\)\)\)\)\)$
7+
^\(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\)\)\)\)\)\)$
8+
--

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
int nondet_int();
2+
3+
int main()
4+
{
5+
int x, y;
6+
7+
x = nondet_int();
8+
__CPROVER_assert(x == 20, "property 1"); // fails
9+
10+
y = nondet_int();
11+
__CPROVER_assert(x == y, "property 2"); // fails
12+
13+
return 0;
14+
}

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
nondet1.c
3+
--horn
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\(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|\)\)\)\)$
7+
^\(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\)\)\)\)\)$
8+
--

‎regression/goto-instrument-chc/chain.sh

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
#!/bin/bash
2+
3+
set -e
4+
5+
goto_cc=$1
6+
goto_instrument=$2
7+
8+
sources=${*:$#}
9+
args=${*:3:$#-3}
10+
11+
set -- $sources
12+
target=${*:$#}
13+
target=${target%.c}
14+
15+
if [[ `basename "${goto_cc}"` == "goto-cl" ]]; then
16+
$goto_cc ${sources} "/Fe${target}.gb"
17+
else
18+
$goto_cc -o ${target}.gb ${sources}
19+
fi
20+
21+
echo DOING: $goto_instrument ${args} "${target}.gb"
22+
23+
$goto_instrument ${args} "${target}.gb"

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -848,7 +848,7 @@ int goto_instrument_parse_optionst::doit()
848848
remove_skip(goto_model);
849849
}
850850

851-
if(cmdline.isset("horn-encoding"))
851+
if(cmdline.isset("horn"))
852852
{
853853
log.status() << "Horn-clause encoding" << messaget::eom;
854854
namespacet ns(goto_model.symbol_table);

0 commit comments

Comments
 (0)