Skip to content

Commit 66f913e

Browse files
kroeningkroening
authored
Merge pull request #7126 from esteffin/esteffin/log-smt-formula-to-file
Log SMT formula to file for new incremental backend.
2 parents e73fcbb + 1dc2e03 commit 66f913e

17 files changed

+309
-14
lines changed

Diff for: ‎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)

Diff for: ‎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.

Diff for: ‎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+
)

Diff for: ‎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

Diff for: ‎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()

Diff for: ‎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\)

Diff for: ‎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

Diff for: ‎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\)

Diff for: ‎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

Diff for: ‎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+
}

Diff for: ‎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\)

Diff for: ‎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

Diff for: ‎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\)

Diff for: ‎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

Diff for: ‎src/goto-checker/solver_factory.cpp

+45-13
Original file line numberDiff line numberDiff line change
@@ -329,12 +329,54 @@ solver_factoryt::get_string_refinement()
329329
std::move(decision_procedure), std::move(prop));
330330
}
331331

332+
std::unique_ptr<std::ofstream> open_outfile_and_check(
333+
const std::string &filename,
334+
message_handlert &message_handler)
335+
{
336+
if(filename.empty())
337+
return nullptr;
338+
339+
#ifdef _MSC_VER
340+
auto out = util_make_unique<std::ofstream>(widen(filename));
341+
#else
342+
auto out = util_make_unique<std::ofstream>(filename);
343+
#endif
344+
345+
if(!*out)
346+
{
347+
throw invalid_command_line_argument_exceptiont(
348+
"failed to open file: " + filename, "--outfile");
349+
}
350+
351+
messaget log(message_handler);
352+
log.status() << "Outputting SMTLib formula to file: " << filename
353+
<< messaget::eom;
354+
return out;
355+
}
356+
332357
std::unique_ptr<solver_factoryt::solvert>
333358
solver_factoryt::get_incremental_smt2(std::string solver_command)
334359
{
335360
no_beautification();
336-
auto solver_process = util_make_unique<smt_piped_solver_processt>(
337-
std::move(solver_command), message_handler);
361+
362+
const std::string outfile_arg = options.get_option("outfile");
363+
364+
std::unique_ptr<smt_base_solver_processt> solver_process = nullptr;
365+
366+
if(!outfile_arg.empty())
367+
{
368+
bool on_std_out = outfile_arg == "-";
369+
std::unique_ptr<std::ostream> outfile =
370+
on_std_out ? nullptr
371+
: open_outfile_and_check(outfile_arg, message_handler);
372+
solver_process = util_make_unique<smt_incremental_dry_run_solvert>(
373+
message_handler, on_std_out ? std::cout : *outfile, std::move(outfile));
374+
}
375+
else
376+
{
377+
solver_process = util_make_unique<smt_piped_solver_processt>(
378+
std::move(solver_command), message_handler);
379+
}
338380

339381
return util_make_unique<solvert>(
340382
util_make_unique<smt2_incremental_decision_proceduret>(
@@ -390,17 +432,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
390432
}
391433
else
392434
{
393-
#ifdef _MSC_VER
394-
auto out = util_make_unique<std::ofstream>(widen(filename));
395-
#else
396-
auto out = util_make_unique<std::ofstream>(filename);
397-
#endif
398-
399-
if(!*out)
400-
{
401-
throw invalid_command_line_argument_exceptiont(
402-
"failed to open file: " + filename, "--outfile");
403-
}
435+
auto out = open_outfile_and_check(filename, message_handler);
404436

405437
auto smt2_conv = util_make_unique<smt2_convt>(
406438
ns,

Diff for: ‎src/solvers/smt2_incremental/smt_solver_process.cpp

+30
Original file line numberDiff line numberDiff line change
@@ -68,3 +68,33 @@ smt_responset smt_piped_solver_processt::receive_response(
6868
handle_invalid_smt(*validation_errors, log);
6969
return *validation_result.get_if_valid();
7070
}
71+
72+
smt_incremental_dry_run_solvert::smt_incremental_dry_run_solvert(
73+
message_handlert &message_handler,
74+
std::ostream &out_stream,
75+
std::unique_ptr<std::ostream> file_stream)
76+
: file_stream(std::move(file_stream)),
77+
out_stream(out_stream),
78+
log(message_handler)
79+
{
80+
}
81+
82+
const std::string &smt_incremental_dry_run_solvert::description()
83+
{
84+
return desc;
85+
}
86+
87+
void smt_incremental_dry_run_solvert::send(const smt_commandt &smt_command)
88+
{
89+
out_stream << smt_to_smt2_string(smt_command) << '\n';
90+
}
91+
92+
smt_responset smt_incremental_dry_run_solvert::receive_response(
93+
const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
94+
{
95+
// Using `smt_unsat_responset` as response because the decision-procedure will
96+
// terminate anyway (stop-on-fail), it is not reported to the user as for
97+
// `unknown`, and does not trigger a subsequent invocation to get the model
98+
// (as a `smt_sat_responset` answer will trigger).
99+
return smt_check_sat_responset{smt_unsat_responset{}};
100+
}

Diff for: ‎src/solvers/smt2_incremental/smt_solver_process.h

+44-1
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,12 @@
55

66
class smt_commandt;
77

8-
#include <solvers/smt2_incremental/smt_responses.h>
98
#include <util/message.h>
109
#include <util/piped_process.h>
1110

11+
#include <solvers/smt2_incremental/smt_responses.h>
12+
13+
#include <memory>
1214
#include <sstream>
1315
#include <string>
1416

@@ -60,4 +62,45 @@ class smt_piped_solver_processt : public smt_base_solver_processt
6062
messaget log;
6163
};
6264

65+
/// Class for an incremental SMT solver used in combination with `--outfile`
66+
/// argument where the solver is never run.
67+
class smt_incremental_dry_run_solvert : public smt_base_solver_processt
68+
{
69+
public:
70+
/// \param message_handler:
71+
/// The messaging system to be used for logging purposes.
72+
/// \param out_stream:
73+
/// Reference to the stream to print the SMT formula.
74+
/// \param file_stream:
75+
/// Pointer to the file stream to print the SMT formula into. `nullptr` if
76+
/// output is to `std::cout`.
77+
smt_incremental_dry_run_solvert(
78+
message_handlert &message_handler,
79+
std::ostream &out_stream,
80+
std::unique_ptr<std::ostream> file_stream);
81+
82+
const std::string &description() override;
83+
84+
void send(const smt_commandt &smt_command) override;
85+
86+
/// \note This function returns always a valid unsat response.
87+
smt_responset receive_response(
88+
const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
89+
override;
90+
91+
~smt_incremental_dry_run_solvert() override = default;
92+
93+
protected:
94+
/// Pointer to the file stream to print the SMT formula. `nullptr` if output
95+
/// is to `std::cout`.
96+
std::unique_ptr<std::ostream> file_stream;
97+
/// The output stream reference to print the SMT formula to.
98+
std::ostream &out_stream;
99+
/// For debug printing.
100+
messaget log;
101+
102+
/// Description of the current solver
103+
const std::string desc = "SMT2 incremental dry-run";
104+
};
105+
63106
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H

0 commit comments

Comments
 (0)