-
Notifications
You must be signed in to change notification settings - Fork 262
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add goto-bmc
, a new tool to run only the verifier
#7762
Changes from 14 commits
50d87da
727f434
d032cae
edea1bc
090b7be
94d66bd
b81ca84
4322d61
192142b
92d4e38
002eb9e
74cdc37
5a667fd
2fcc60b
4f5a3b0
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
add_test_pl_tests( | ||
"$<TARGET_FILE:goto-bmc>" | ||
) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
CORE | ||
|
||
--help | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
goto-bmc \d\.\d+\.\d+ | ||
Usage\: | ||
Purpose\: | ||
show help | ||
show version and exit | ||
-- | ||
-- | ||
Test that help is output when help argument is specified. |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
CORE | ||
|
||
|
||
^EXIT=6$ | ||
^SIGNAL=0$ | ||
Please give exactly one binary file | ||
-- | ||
-- | ||
Test that an appropriate error message is produced when no input goto binary is | ||
specified. |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
CORE | ||
|
||
--version | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^\d\.\d+\.\d+ | ||
-- | ||
-- | ||
Test that version is output when version argument is specified. |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows") | ||
set(is_windows true) | ||
else() | ||
set(is_windows false) | ||
endif() | ||
|
||
# Second suite of tests is running `goto-cc` to produce "normal" goto-binaries, | ||
# which we expect `goto-bmc` to reject in some capacity. For now, it just fails | ||
# non-gracefully, with invariant violations. This behaviour is important enough | ||
# that we want to test for it, but we expect the software to become better behaved | ||
# in the future (by checking that the input binary *is* in symex-ready-goto form | ||
# and if not produce appropriate error reporting for the user). | ||
add_test_pl_tests( | ||
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-bmc> ${is_windows}" | ||
) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
#!/usr/bin/env bash | ||
|
||
set -e | ||
|
||
goto_cc=$1 | ||
goto_bmc=$2 | ||
is_windows=$3 | ||
|
||
options=${*:4:$#-4} | ||
name=${*:$#} | ||
base_name=${name%.c} | ||
base_name=${base_name%.cpp} | ||
|
||
if [[ "${is_windows}" == "true" ]]; then | ||
"${goto_cc}" "${name}" "/Fe${base_name}.gb" | ||
else | ||
"${goto_cc}" "${name}" -o "${base_name}.gb" | ||
fi | ||
|
||
"${goto_bmc}" "${base_name}.gb" ${options} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
int main(int argc, char *argv[]) | ||
{ | ||
int a[] = {0, 1, 2, 3, 4}; | ||
__CPROVER_assert(a[0] != 0, "expected fail: 0 == 0"); | ||
return 0; | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
CORE | ||
main.c | ||
|
||
^EXIT=(127|134)$ | ||
^SIGNAL=0$ | ||
^Invariant check failed$ | ||
^Reason: Check return value$ | ||
-- | ||
^warning: ignoring | ||
-- | ||
This is the same file as in positive1/ but we want to make sure | ||
that we fail in some way, signalling that we don't support non | ||
symex-ready goto binaries as input. | ||
|
||
We expect the semantics of the test to remain the same as the | ||
program evolves, but some of the regexes above may fail as the | ||
program is enhanced with better capacity to detect non symex-ready | ||
goto binaries and report to the user appropriately. |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
# `goto-bmc` is supposed to operate only on symex-ready goto binary files, so | ||
# we follow two different paths to make sure that it's behaviour is correct: | ||
|
||
# First suite of tests is supposed to be tests against symex-ready goto. For these, | ||
# goto-bmc is capable of handling those, and so we produce them using | ||
# `cbmc --export-symex-ready-goto <file>`. | ||
add_test_pl_tests( | ||
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:cbmc> $<TARGET_FILE:goto-bmc>" | ||
) | ||
|
||
# Second suite of tests is in folder `regression/goto-bmc-non-symex-ready-goto/` |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
#!/usr/bin/env bash | ||
|
||
set -e | ||
|
||
cbmc=$1 | ||
goto_bmc=$2 | ||
|
||
options=${*:3:$#-3} | ||
name=${*:$#} | ||
base_name=${name%.c} | ||
|
||
"${cbmc}" --export-symex-ready-goto "${base_name}.goto.symex_ready" "${name}" | ||
"${goto_bmc}" "${base_name}.goto.symex_ready" ${options} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
int main(int argc, char *argv[]) | ||
{ | ||
int a[] = {0, 1, 2, 3, 4}; | ||
__CPROVER_assert(a[0] != 0, "expected fail: 0 == 0"); | ||
return 0; | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
CORE | ||
main.c | ||
|
||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
\[main\.assertion\.1\] line \d expected fail: 0 == 0: FAILURE | ||
^VERIFICATION FAILED$ | ||
-- | ||
^warning: ignoring | ||
-- |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
CORE | ||
main.c | ||
main.goto.symex_ready | ||
^EXIT=6$ | ||
^SIGNAL=0$ | ||
Please give exactly one binary file | ||
-- | ||
-- | ||
Test that an appropriate error message is produced when too many input goto | ||
binaries are specified. A copy of the `main.goto.symex_ready` argument will | ||
be generated by the `chain.sh` script from the specified `main.c`. This yields | ||
2 copies of this argument including the one in this file. |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
CORE | ||
not-goto-no-header.goto | ||
|
||
^EXIT=6$ | ||
^SIGNAL=0$ | ||
Please give exactly one binary file | ||
-- | ||
not a goto binary | ||
Unable to read goto-binary from file not-goto-no-header\.goto | ||
-- | ||
This test confirms that an appropriate error message is displayed in the case | ||
where a single input file is specified which does not pass the header check. |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
This is not a goto binary. A header would be required to pass the | ||
`is_goto_binary` check. |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
CORE | ||
not-goto-with-header.goto | ||
|
||
^EXIT=2$ | ||
^SIGNAL=0$ | ||
Unable to read goto-binary from file not-goto-with-header\.goto | ||
-- | ||
Please give exactly one binary file | ||
not a goto binary | ||
-- | ||
This test confirms that an appropriate error message is displayed in the case | ||
where an input file is specified which passed the header check used to | ||
determine if the file is a goto binary or not, but which is not followed by | ||
data of a valid goto binary file. Note that the `is_goto_binary` check works | ||
based on checking if the first four bytes of the file are the byte 7F followed | ||
by the characters "GBF". |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
GBF | ||
This is not a valid goto binary. It does have a header which should pass the | ||
`is_goto_binary` check though. |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
file(GLOB_RECURSE sources "*.cpp" "*.h") | ||
add_executable(goto-bmc ${sources}) | ||
|
||
generic_includes(goto-bmc) | ||
|
||
target_link_libraries(goto-bmc cprover-api-cpp) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
// Author: Enrico Steffinlongo for Diffblue Ltd. | ||
|
||
#include "goto_bmc_parse_options.h" | ||
|
||
#include <iostream> | ||
#include <vector> | ||
|
||
int main(int argc, const char **argv) | ||
{ | ||
return goto_bmc_parse_optionst{argc, argv}.main(); | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,98 @@ | ||
// Author: Fotis Koutoulakis for Diffblue Ltd. | ||
|
||
#include "goto_bmc_parse_options.h" | ||
|
||
#include <util/exit_codes.h> | ||
#include <util/message.h> | ||
#include <util/version.h> | ||
|
||
#include <libcprover-cpp/api_options.h> | ||
#include <libcprover-cpp/verification_result.h> | ||
|
||
#include "api.h" | ||
|
||
goto_bmc_parse_optionst::goto_bmc_parse_optionst(int argc, const char **argv) | ||
: parse_options_baset( | ||
GOTO_BMC_OPTIONS, | ||
argc, | ||
argv, | ||
std::string("goto-bmc") + CBMC_VERSION) | ||
{ | ||
} | ||
|
||
int goto_bmc_parse_optionst::doit() | ||
{ | ||
auto api_options = api_optionst::create(); | ||
|
||
if(cmdline.isset("version")) | ||
{ | ||
log.status() << CBMC_VERSION << messaget::eom; | ||
return CPROVER_EXIT_SUCCESS; | ||
} | ||
|
||
api_sessiont api{api_options}; | ||
|
||
if(cmdline.args.size() != 1 || !api.is_goto_binary(cmdline.args[0])) | ||
{ | ||
log.error() << "Please give exactly one binary file" << messaget::eom; | ||
return CPROVER_EXIT_INCORRECT_TASK; | ||
} | ||
|
||
std::string filename = cmdline.args[0]; | ||
|
||
if(cmdline.isset("validate-goto-model")) | ||
{ | ||
api_options.validate_goto_model(true); | ||
} | ||
|
||
log.status() << "goto-bmc version " << *api.get_api_version() | ||
<< messaget::eom; | ||
|
||
// The API works with a callback for querying state - we for now just print | ||
// collected messages from the message buffer to stdout. | ||
struct call_back_contextt | ||
{ | ||
std::reference_wrapper<messaget> log; | ||
bool error_seen; | ||
} call_back_context{log}; | ||
const auto callback = []( | ||
const api_messaget &message, | ||
api_call_back_contextt api_call_back_context) { | ||
auto context = static_cast<call_back_contextt *>(api_call_back_context); | ||
const bool is_error_message = api_message_is_error(message); | ||
context->error_seen |= is_error_message; | ||
(is_error_message ? context->log.get().error() | ||
: context->log.get().status()) | ||
<< api_message_get_string(message) << messaget::eom; | ||
}; | ||
|
||
api.set_message_callback(callback, &call_back_context); | ||
|
||
// Finally, we read the goto-binary the user supplied... | ||
api.read_goto_binary(filename); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 🚫 Missing error handling. I am thinking about handling of basic issues like the specified file not existing. We should not just violate an INVARIANT and dump a stack on bad input from the user. This could be resolved via the message_call back interface via the following steps -
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Error handling is still missing here. In the case where |
||
if(call_back_context.error_seen) | ||
return CPROVER_EXIT_PARSE_ERROR; | ||
|
||
// ... and run analysis on it. | ||
auto result = api.run_verifier(); | ||
|
||
return verifier_result_to_exit_code(result->final_result()); | ||
} | ||
|
||
void goto_bmc_parse_optionst::help() | ||
{ | ||
// clang-format off | ||
log.status() << '\n' << banner_string("goto-bmc", CBMC_VERSION) << '\n' | ||
<< align_center_with_border("Copyright (C) 2023") << '\n' | ||
<< align_center_with_border("Diffblue Ltd.") << '\n' // NOLINT(*) | ||
<< | ||
"\n" | ||
"Usage: Purpose:\n" | ||
"\n" | ||
"goto-bmc [-?] [-h] [--help] show help\n" | ||
"goto-bmc --version show version and exit\n" | ||
// NOLINTNEXTLINE(*) | ||
"goto-bmc [options] file.c ... perform bounded model checking on symex-ready goto-binary\n"; | ||
// clang-format on | ||
log.status() << messaget::eom; | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,29 @@ | ||
// Author: Fotis Koutoulakis for Diffblue Ltd. | ||
|
||
#ifndef CPROVER_GOTO_BMC_GOTO_BMC_PARSE_OPTIONS_H | ||
#define CPROVER_GOTO_BMC_GOTO_BMC_PARSE_OPTIONS_H | ||
|
||
#include <util/parse_options.h> | ||
|
||
#include <libcprover-cpp/api_options.h> | ||
|
||
#include <memory> | ||
#include <string> | ||
#include <vector> | ||
|
||
// clang-format off | ||
#define GOTO_BMC_OPTIONS \ | ||
"(version)" | ||
// clang-format on | ||
|
||
class goto_bmc_parse_optionst : public parse_options_baset | ||
{ | ||
public: | ||
goto_bmc_parse_optionst(int argc, const char **argv); | ||
|
||
void help() override; | ||
|
||
int doit() override; | ||
}; | ||
|
||
#endif // CPROVER_GOTO_BMC_GOTO_BMC_PARSE_OPTIONS_H |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
util | ||
libcprover-cpp |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
ℹ️ A capture-less lambda can be converted to a function pointer (without using
std::function
). This technique could be used in order to keep the definition of the function next-to/in-line-with the setting of the message callback. This would restrict the scope of the function and might dodge such reader questions as "what is this function for?"