Skip to content

Commit 1dc2e03

Browse files
author
Enrico Steffinlongo
committed
Add regression tests for --outfile argument
1 parent 21d4907 commit 1dc2e03

14 files changed

+190
-0
lines changed

‎regression/CMakeLists.txt

+1
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ add_subdirectory(cbmc-cover)
3434
add_subdirectory(cbmc-incr-oneloop)
3535
add_subdirectory(cbmc-incr-smt2)
3636
add_subdirectory(cbmc-incr)
37+
add_subdirectory(cbmc-output-file)
3738
add_subdirectory(cbmc-with-incr)
3839
add_subdirectory(array-refinement-with-incr)
3940
add_subdirectory(goto-instrument-chc)

‎regression/cbmc-incr-smt2/nondeterministic-int-assert/stdout-match.desc

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
test.c
3+
--outfile -
4+
Starting Bounded Model Checking
5+
^\(set-option :produce-models true\)$
6+
^\(set-logic ALL\)$
7+
^\(declare-fun size_of_object \(\(_ BitVec 8\)\) \(_ BitVec 64\)\)$
8+
^Passing problem to incremental SMT2 solving via SMT2 incremental dry-run$
9+
^\(define-fun B0 \(\) Bool true\)$
10+
^\(define-fun B2 \(\) Bool \(not false\)\)$
11+
^\(assert B2\)$
12+
^\(assert \(= \(size_of_object \(_ bv1 8\)\) \(_ bv0 64\)\)\)$
13+
^\(assert \(= \(size_of_object \(_ bv0 8\)\) \(_ bv0 64\)\)\)$
14+
^\(check-sat\)$
15+
^EXIT=0$
16+
^SIGNAL=0$
17+
--
18+
Test to check that the `--outfile -` argument is used correctly.

‎regression/cbmc-output-file/CMakeLists.txt

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
add_test_pl_tests(
2+
"${CMAKE_CURRENT_SOURCE_DIR}/chain.py $<TARGET_FILE:cbmc>" "-f"
3+
)

‎regression/cbmc-output-file/Makefile

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
default: tests.log
2+
3+
include ../../src/config.inc
4+
include ../../src/common
5+
6+
test:
7+
@../test.pl -f -e -p -c '../chain.py ../../../src/cbmc/cbmc'
8+
9+
tests.log:
10+
@../test.pl -f -e -p -c '../chain.py ../../../src/cbmc/cbmc'
11+
12+
clean:
13+
@for dir in *; do \
14+
$(RM) tests.log; \
15+
if [ -d "$$dir" ]; then \
16+
cd "$$dir"; \
17+
$(RM) *.out *.gb; \
18+
cd ..; \
19+
fi \
20+
done

‎regression/cbmc-output-file/chain.py

+71
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
#!/usr/bin/env python3
2+
3+
import subprocess
4+
import sys
5+
import re
6+
7+
8+
class Options:
9+
def __init__(self):
10+
self.cmd_binary = sys.argv[1]
11+
self.test_name = sys.argv[2]
12+
self.cmd_options = sys.argv[3:]
13+
self.outfile = self.test_name + "-out-file.out"
14+
self.outfile_rules = self.test_name + "-out-file-rules.txt"
15+
16+
def __str__(self):
17+
return """
18+
cmd_binary: {},
19+
test_name: {},
20+
cmd_options: {},
21+
outfile: {},
22+
outfile_rules: {},
23+
""".format(self.cmd_binary,
24+
self.test_name,
25+
self.cmd_options,
26+
self.outfile,
27+
self.outfile_rules)
28+
29+
30+
def try_compile_regex(regex_content):
31+
try:
32+
return re.compile(regex_content)
33+
except re.error:
34+
print("Bad regex: {}".format(regex_content))
35+
raise
36+
37+
38+
def check_outfile(options):
39+
with open(options.outfile) as outfile_f:
40+
with open(options.outfile_rules) as outfile_rules_f:
41+
unprocessed_outfile = outfile_f.readlines()
42+
outfile_rules = [try_compile_regex(c) for c in outfile_rules_f.readlines()]
43+
for rule in outfile_rules:
44+
found = False
45+
while not found:
46+
if len(unprocessed_outfile) == 0:
47+
return False
48+
match = rule.match(unprocessed_outfile[0])
49+
found = match is not None
50+
unprocessed_outfile = unprocessed_outfile[1:]
51+
return True
52+
53+
54+
def main():
55+
options = Options()
56+
cmd_options = [options.outfile if item == '%out-file-name%' else item for item in
57+
options.cmd_options]
58+
cmd_line = [options.cmd_binary] + cmd_options
59+
print("Running: ", cmd_line)
60+
subprocess.run(cmd_line)
61+
print("\n--- Checking outfiles ---")
62+
if check_outfile(options):
63+
print("Output file matches.")
64+
sys.exit(0)
65+
else:
66+
print("Output file does not match.")
67+
sys.exit(1)
68+
69+
70+
if __name__ == "__main__":
71+
main()

‎regression/cbmc-output-file/outfile/cvc5-match-out-file-rules.txt

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
\(set-option :produce-models true\)
2+
\(set-logic ALL\)
3+
\(define-fun B0 \(\) Bool true\)
4+
\(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
5+
\(define-fun B1 \(\) Bool \(= |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
6+
\(assert \(not \(not \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
7+
\(define-fun B2 \(\) Bool \(not false\)\)
8+
\(assert B2\)
9+
\(check-sat\)

‎regression/cbmc-output-file/outfile/cvc5-match.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.c
3+
--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --slice-formula --outfile %out-file-name%
4+
Passing problem to incremental SMT2 solving via SMT2 incremental dry-run
5+
Output file matches.
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
Test to check that the --outfile argument is used correctly and that the output file matches the
10+
rules defined in test-outfile-rules.txt

‎regression/cbmc-output-file/outfile/cvc5-no-match-out-file-rules.txt

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
\(set-option :produce-models true\)
2+
\(set-logic ALL\)
3+
\(define-fun B0 \(\) Bool true\)
4+
\(define-fun B2 \(\) Bool \(not false\)\)
5+
\(check-sat\)
6+
\(assert B2\)

‎regression/cbmc-output-file/outfile/cvc5-no-match.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.c
3+
--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --slice-formula --outfile %out-file-name%
4+
Passing problem to incremental SMT2 solving via SMT2 incremental dry-run
5+
Output file does not match.
6+
^EXIT=1$
7+
^SIGNAL=0$
8+
--
9+
Test to check that the --outfile argument is used correctly and that the output file matches the
10+
rules defined in test-outfile-rules.txt

‎regression/cbmc-output-file/outfile/test.c

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
2+
int main()
3+
{
4+
int x;
5+
__CPROVER_assert(x, "Nondeterministic int assert.");
6+
return 0;
7+
}

‎regression/cbmc-output-file/outfile/z3-match-out-file-rules.txt

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
\(set-option :produce-models true\)
2+
\(set-logic ALL\)
3+
\(define-fun B0 \(\) Bool true\)
4+
\(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
5+
\(define-fun B1 \(\) Bool \(= |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
6+
\(assert \(not \(not \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
7+
\(define-fun B2 \(\) Bool \(not false\)\)
8+
\(assert B2\)
9+
\(check-sat\)

‎regression/cbmc-output-file/outfile/z3-match.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.c
3+
--incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --outfile %out-file-name%
4+
Passing problem to incremental SMT2 solving via SMT2 incremental dry-run
5+
Output file matches.
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
Test to check that the --outfile argument is used correctly and that the output file matches the
10+
rules defined in test-outfile-rules.txt

‎regression/cbmc-output-file/outfile/z3-no-match-out-file-rules.txt

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
\(set-option :produce-models true\)
2+
\(set-logic ALL\)
3+
\(define-fun B0 \(\) Bool true\)
4+
\(define-fun B2 \(\) Bool \(not false\)\)
5+
\(check-sat\)
6+
\(assert B2\)

‎regression/cbmc-output-file/outfile/z3-no-match.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.c
3+
--incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --outfile %out-file-name%
4+
Passing problem to incremental SMT2 solving via SMT2 incremental dry-run
5+
Output file does not match.
6+
^EXIT=1$
7+
^SIGNAL=0$
8+
--
9+
Test to check that the --outfile argument is used correctly and that the output file matches the
10+
rules defined in test-outfile-rules.txt

0 commit comments

Comments
 (0)