From 77240922212ea161b783687ee081105df35642bf Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 19 Apr 2023 11:51:44 +0300 Subject: [PATCH] Adding initial version of `goto-inspect`. This allows to inspect a goto-binary (this means showing the goto-functions, for now at least). The reason this binary is helpful is that different tools (CBMC, goto-instrument, etc) perform instrumentation before showing the goto-functions, and there's a need to be able to inspect certain properties of a goto-binary without doing instrumentation. --- CMakeLists.txt | 2 + CODEOWNERS | 1 + doc/man/goto-inspect.1 | 33 ++++++ regression/CMakeLists.txt | 1 + regression/goto-inspect/CMakeLists.txt | 11 ++ regression/goto-inspect/chain.sh | 31 ++++++ .../goto-inspect/show-goto-functions/main.c | 5 + .../show-goto-functions/negative.desc | 22 ++++ .../show-goto-functions/positive.desc | 14 +++ src/CMakeLists.txt | 1 + src/Makefile | 8 +- src/goto-inspect/CMakeLists.txt | 22 ++++ src/goto-inspect/Makefile | 31 ++++++ src/goto-inspect/goto_inspect_main.cpp | 20 ++++ .../goto_inspect_parse_options.cpp | 100 ++++++++++++++++++ src/goto-inspect/goto_inspect_parse_options.h | 24 +++++ src/goto-inspect/module_dependencies.txt | 2 + src/goto-inspect/readme.md | 10 ++ 18 files changed, 336 insertions(+), 2 deletions(-) create mode 100644 doc/man/goto-inspect.1 create mode 100644 regression/goto-inspect/CMakeLists.txt create mode 100755 regression/goto-inspect/chain.sh create mode 100644 regression/goto-inspect/show-goto-functions/main.c create mode 100644 regression/goto-inspect/show-goto-functions/negative.desc create mode 100644 regression/goto-inspect/show-goto-functions/positive.desc create mode 100644 src/goto-inspect/CMakeLists.txt create mode 100644 src/goto-inspect/Makefile create mode 100644 src/goto-inspect/goto_inspect_main.cpp create mode 100644 src/goto-inspect/goto_inspect_parse_options.cpp create mode 100644 src/goto-inspect/goto_inspect_parse_options.h create mode 100644 src/goto-inspect/module_dependencies.txt create mode 100644 src/goto-inspect/readme.md diff --git a/CMakeLists.txt b/CMakeLists.txt index d77266f176f..5c56ddc3e9f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -158,6 +158,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR "$" "$" "$" + "$" "$" "$" "$" @@ -230,6 +231,7 @@ cprover_default_properties( goto-checker goto-diff goto-diff-lib + goto-inspect goto-harness goto-instrument goto-instrument-lib diff --git a/CODEOWNERS b/CODEOWNERS index 87736894f38..4f1cf7c0f9e 100644 --- a/CODEOWNERS +++ b/CODEOWNERS @@ -53,6 +53,7 @@ /src/goto-harness/ @martin-cs @chris-ryder @peterschrammel /src/goto-instrument/ @martin-cs @chris-ryder @peterschrammel @tautschnig @kroening /src/goto-instrument/contracts/ @tautschnig @feliperodri @remi-delmas-3000 +/src/goto-inspect/ @diffblue/diffblue-opensource /src/goto-synthesizer/ @qinheping @tautschnig @feliperodri @remi-delmas-3000 /src/goto-diff/ @tautschnig @peterschrammel /src/jsil/ @kroening @tautschnig diff --git a/doc/man/goto-inspect.1 b/doc/man/goto-inspect.1 new file mode 100644 index 00000000000..c51643d08b6 --- /dev/null +++ b/doc/man/goto-inspect.1 @@ -0,0 +1,33 @@ +.TH GOTO-INSPECT "2" "May 2023" "goto-inspect-5.81.0" "User Commands" +.SH NAME +goto\-inspect \- Inspect goto-binaries. +.SH SYNOPSIS +.TP +.B goto\-inspect [\-?] [\-h] [\-\-help] +show help +.TP +.B goto\-inspect \-\-version +show version and exit +.TP +.B goto\-inspect [options] \fIin\fR +Inspect (show properties, goto-functions, etc of) given goto-binary. +.SH DESCRIPTION +\fBgoto-inspect\fR reads a GOTO binary, and shows goto-functions, properties, +and other attributes associated with the goto-program. +.SH OPTIONS +.SS "User-interface options:" +.TP +\fB\-\-show\-goto\-functions\fR +print the goto-program instructions for the functions contained by the binary. +.SH ENVIRONMENT +All tools honor the TMPDIR environment variable when generating temporary +files and directories. +.SH BUGS +If you encounter a problem please create an issue at +.B https://github.com/diffblue/cbmc/issues +.SH SEE ALSO +.BR cbmc (1), +.BR goto-cc (1) +.BR goto-instrument (1) +.SH COPYRIGHT +2023, Diffblue Ltd. diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index 21a262a5ae5..823fd386414 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -46,6 +46,7 @@ add_subdirectory(goto-instrument-chc) add_subdirectory(goto-instrument-json) add_subdirectory(goto-instrument-wmm-core) add_subdirectory(goto-instrument-typedef) +add_subdirectory(goto-inspect) add_subdirectory(smt2_solver) add_subdirectory(smt2_strings) add_subdirectory(strings) diff --git a/regression/goto-inspect/CMakeLists.txt b/regression/goto-inspect/CMakeLists.txt new file mode 100644 index 00000000000..d6fbe4092e3 --- /dev/null +++ b/regression/goto-inspect/CMakeLists.txt @@ -0,0 +1,11 @@ +if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows") + set(is_windows true) + set(exclude_win_broken_tests -X winbug) +else() + set(is_windows false) + set(exclude_win_broken_tests "") +endif() + +add_test_pl_tests( + "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $ ${is_windows}" ${exclude_win_broken_tests} +) diff --git a/regression/goto-inspect/chain.sh b/regression/goto-inspect/chain.sh new file mode 100755 index 00000000000..5c546d46dbf --- /dev/null +++ b/regression/goto-inspect/chain.sh @@ -0,0 +1,31 @@ +#!/bin/bash + +set -e + +# A test instruction passed to this `chain.sh` file looks like this: +# +# build/bin/goto-cc build/bin/goto-inspect --show-goto-functions main.c +# +# This allows us to safely assume for now (as long as we're operating +# goto-inspect with one binary and one inspection option, which seems +# to be the case for now) that the option is going to be at $4. +# If this is no longer the case in the future, this script will need +# to be made significantly more sophisticated in terms of handling +# a variable number of options for the goto-inspect binary. + +goto_cc_exe=$1 +goto_inspect_exe=$2 +is_windows=$3 + +name=${*:$#} +name=${name%.c} + +# We need to dispatch to the appropriate platform executable because +# they accept different options. +if [[ "${is_windows}" == "true" ]]; then + $goto_cc_exe "${name}.c" "/Fe${name}.gb" +else + $goto_cc_exe -o "${name}.gb" "${name}.c" +fi + +$goto_inspect_exe $4 "${name}.gb" diff --git a/regression/goto-inspect/show-goto-functions/main.c b/regression/goto-inspect/show-goto-functions/main.c new file mode 100644 index 00000000000..b08ca61b9cf --- /dev/null +++ b/regression/goto-inspect/show-goto-functions/main.c @@ -0,0 +1,5 @@ +int main(int argc, char *argv[]) +{ + int arr[] = {0, 1, 2, 3, 4}; + __CPROVER_assert(arr[0] != 0, "Expected failure: 0 == 0"); +} diff --git a/regression/goto-inspect/show-goto-functions/negative.desc b/regression/goto-inspect/show-goto-functions/negative.desc new file mode 100644 index 00000000000..f6762c1c344 --- /dev/null +++ b/regression/goto-inspect/show-goto-functions/negative.desc @@ -0,0 +1,22 @@ +CORE winbug +main.c +" " +^EXIT=6$ +^SIGNAL=0$ +-- +DECL main::1::arr : signedbv\[32\]\[5\] +ASSIGN main::1::arr := \{ 0, 1, 2, 3, 4 \} +ASSERT main::1::arr\[cast\(0, signedbv\[64\]\)\] ≠ 0 // Expected failure: 0 == 0 +DEAD main::1::arr +SET RETURN VALUE side_effect statement="nondet" is_nondet_nullable="1" +END_FUNCTION +-- +This is testing the behaviour of the goto-inspect binary in case a binary +is present, but no inspection option is present. + +This is labelled `winbug` to avoid running on windows because of issues with +the empty string in line 3 (simulating the lack of an option) not working as +it should (it is contrary to the behaviour of unix systems). The behaviour +has been verified manually on a machine as working as expected, but getting +the test to run automatically is a lot more involved, so we're opting to +skipping this on that platform for now. diff --git a/regression/goto-inspect/show-goto-functions/positive.desc b/regression/goto-inspect/show-goto-functions/positive.desc new file mode 100644 index 00000000000..7d2149d8274 --- /dev/null +++ b/regression/goto-inspect/show-goto-functions/positive.desc @@ -0,0 +1,14 @@ +CORE +main.c +--show-goto-functions +^EXIT=0$ +^SIGNAL=0$ +main +DECL main::1::arr : signedbv\[32\]\[5\] +ASSIGN main::1::arr := \{ 0, 1, 2, 3, 4 \} +ASSERT main::1::arr\[cast\(0, signedbv\[64\]\)\] ≠ 0 // Expected failure: 0 == 0 +DEAD main::1::arr +SET RETURN VALUE side_effect statement="nondet" is_nondet_nullable="1" +END_FUNCTION +-- +-- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6bda1f9d709..51bfee0e30a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -98,6 +98,7 @@ add_subdirectory(xmllang) add_subdirectory(goto-checker) add_subdirectory(goto-programs) add_subdirectory(goto-symex) +add_subdirectory(goto-inspect) add_subdirectory(jsil) add_subdirectory(json) add_subdirectory(json-symtab-language) diff --git a/src/Makefile b/src/Makefile index 640b600e94f..6c230a7256c 100644 --- a/src/Makefile +++ b/src/Makefile @@ -10,6 +10,7 @@ DIRS = analyses \ goto-cc \ goto-checker \ goto-diff \ + goto-inspect \ goto-instrument \ goto-harness \ goto-programs \ @@ -36,6 +37,7 @@ all: cbmc.dir \ goto-cc.dir \ goto-diff.dir \ goto-instrument.dir \ + goto-inspect.dir \ goto-harness.dir \ goto-synthesizer.dir \ symtab2gb.dir \ @@ -82,6 +84,8 @@ goto-harness.dir: util.dir goto-programs.dir langapi.dir linking.dir \ goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \ goto-symex.dir linking.dir analyses.dir solvers.dir +goto-inspect.dir: util.dir goto-programs.dir languages linking.dir + goto-checker.dir: solvers.dir goto-symex.dir goto-programs.dir cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \ @@ -190,8 +194,8 @@ doc : install: all for b in \ cbmc crangler \ - goto-analyzer goto-cc goto-diff goto-instrument goto-harness goto-synthesizer \ - symtab2gb ; do \ + goto-analyzer goto-cc goto-diff goto-instrument goto-inspect goto-harness \ + goto-synthesizer symtab2gb ; do \ cp $$b/$$b $(PREFIX)/bin/ ; \ cp ../doc/man/$$b.1 $(PREFIX)/doc/man/man1/ ; \ done diff --git a/src/goto-inspect/CMakeLists.txt b/src/goto-inspect/CMakeLists.txt new file mode 100644 index 00000000000..846ee4b3cf5 --- /dev/null +++ b/src/goto-inspect/CMakeLists.txt @@ -0,0 +1,22 @@ +# For goto-inspect, we are not building a library - only a binary. + +file(GLOB_RECURSE sources "*.cpp" "*.h") + +add_executable(goto-inspect ${sources}) + +generic_includes(goto-inspect) + +target_link_libraries(goto-inspect + util + goto-programs +) + +install(TARGETS goto-inspect DESTINATION ${CMAKE_INSTALL_BINDIR}) + +# Man page +if(NOT WIN32) + install( + DIRECTORY ${CMAKE_SOURCE_DIR}/doc/man/ + DESTINATION ${CMAKE_INSTALL_MANDIR}/man1 + FILES_MATCHING PATTERN "goto-harness*") +endif() diff --git a/src/goto-inspect/Makefile b/src/goto-inspect/Makefile new file mode 100644 index 00000000000..4aa85c7b8a3 --- /dev/null +++ b/src/goto-inspect/Makefile @@ -0,0 +1,31 @@ +SRC = goto_inspect_main.cpp \ + goto_inspect_parse_options.cpp \ + # Empty last line + +OBJ += ../big-int/big-int$(LIBEXT) \ + ../linking/linking$(LIBEXT) \ + ../langapi/langapi$(LIBEXT) \ + ../goto-programs/goto-programs$(LIBEXT) \ + ../util/util$(LIBEXT) \ + # Empty last line + +INCLUDES= -I .. + +LIBS = + +CLEANFILES = goto-inspect$(EXEEXT) goto-inspect$(LIBEXT) + +include ../config.inc +include ../common + +all: goto-inspect$(EXEEXT) + +############################################################################### + +goto-inspect$(EXEEXT): $(OBJ) + $(LINKBIN) + +.PHONY: goto-inspect-mac-signed + +goto-inspect-mac-signed: goto-inspect$(EXEEXT) + codesign -v -s $(OSX_IDENTITY) goto-inspect$(EXEEXT) diff --git a/src/goto-inspect/goto_inspect_main.cpp b/src/goto-inspect/goto_inspect_main.cpp new file mode 100644 index 00000000000..7dd106f3dd1 --- /dev/null +++ b/src/goto-inspect/goto_inspect_main.cpp @@ -0,0 +1,20 @@ +// Author: Fotis Koutoulakis for Diffblue Ltd. + +#ifdef _MSC_VER +# include +#endif + +#include "goto_inspect_parse_options.h" + +#ifdef _MSC_VER +int wmain(int argc, const wchar_t **argv_wide) +{ + auto vec = narrow_argv(argc, argv_wide); + auto narrow = to_c_str_array(std::begin(vec), std::end(vec)); + auto argv = narrow.data(); +#else +int main(int argc, const char **argv) +{ +#endif + return goto_inspect_parse_optionst{argc, argv}.main(); +} diff --git a/src/goto-inspect/goto_inspect_parse_options.cpp b/src/goto-inspect/goto_inspect_parse_options.cpp new file mode 100644 index 00000000000..441fcc268cc --- /dev/null +++ b/src/goto-inspect/goto_inspect_parse_options.cpp @@ -0,0 +1,100 @@ +// Author: Fotis Koutoulakis for Diffblue Ltd. + +#include "goto_inspect_parse_options.h" + +#include +#include +#include +#include + +#include +#include +#include + +#include + +int goto_inspect_parse_optionst::doit() +{ + if(cmdline.isset("version")) + { + std::cout << CBMC_VERSION << '\n'; + return CPROVER_EXIT_SUCCESS; + } + + // Before we do anything else, ensure that a file argument has been given. + if(cmdline.args.size() != 1) + { + help(); + throw invalid_command_line_argument_exceptiont{ + "failed to supply a goto-binary name or an option for inspection", + " "}; + } + + // This just sets up the defaults (and would interpret options such as --32). + config.set(cmdline); + + // Normally we would register language front-ends here but as goto-inspect + // only works on goto binaries, we don't need to + + auto binary_filename = cmdline.args[0]; + + // Read goto binary into goto-model + auto read_goto_binary_result = + read_goto_binary(binary_filename, ui_message_handler); + if(!read_goto_binary_result.has_value()) + { + throw deserialization_exceptiont{ + "failed to read goto program from file '" + binary_filename + "'"}; + } + auto goto_model = std::move(read_goto_binary_result.value()); + + // This has to be called after the defaults are set up (as per the + // config.set(cmdline) above) otherwise, e.g. the architecture specification + // will be unknown. + config.set_from_symbol_table(goto_model.symbol_table); + + if(cmdline.isset("show-goto-functions")) + { + show_goto_functions( + goto_model, ui_message_handler, cmdline.isset("list-goto-functions")); + return CPROVER_EXIT_SUCCESS; + } + + // If an option + binary was provided, the program will have exited + // gracefully through a different branch. If we hit the code below, it + // means that something has gone wrong - it's also possible to fall through + // this case if no optional inspection flag is present in the argument + // vector. This will ensure that the return value in that case is + // semantically meaningful, and provide a return value that also satisfies + // the compiler's requirements based on the signature of `doit()`. + return CPROVER_EXIT_INCORRECT_TASK; +} + +void goto_inspect_parse_optionst::help() +{ + std::cout << '\n' + << banner_string("Goto-Inspect", CBMC_VERSION) << '\n' + << align_center_with_border("Copyright (C) 2023") << '\n' + << align_center_with_border("Diffblue Ltd.") << '\n' + << align_center_with_border("info@diffblue.com") << '\n' + << '\n' + << "Usage: Purpose:\n" + << '\n' + << " goto-inspect [-?] [-h] [--help] show help\n" + << " goto-inspect --version show version\n" + << " goto-inspect --show-goto-functions show code for " + "goto-functions present in goto-binary\n" + << "\n" + << " goto binary to read from\n"; +} + +goto_inspect_parse_optionst::goto_inspect_parse_optionst( + int argc, + const char *argv[]) + : parse_options_baset{ + GOTO_INSPECT_OPTIONS, + argc, + argv, + std::string("GOTO-INSPECT ") + CBMC_VERSION} +{ +} diff --git a/src/goto-inspect/goto_inspect_parse_options.h b/src/goto-inspect/goto_inspect_parse_options.h new file mode 100644 index 00000000000..ae2b711c194 --- /dev/null +++ b/src/goto-inspect/goto_inspect_parse_options.h @@ -0,0 +1,24 @@ +// Author: Fotis Koutoulakis for Diffblue Ltd. + +#ifndef CPROVER_GOTO_INSPECT_GOTO_INSPECT_PARSE_OPTIONS_H +#define CPROVER_GOTO_INSPECT_GOTO_INSPECT_PARSE_OPTIONS_H + +#include + +// clang-format off +#define GOTO_INSPECT_OPTIONS \ + "(version)" \ + "(show-goto-functions)" \ +// end GOTO_INSPECT_OPTIONS + +// clang-format on + +struct goto_inspect_parse_optionst : public parse_options_baset +{ + int doit() override; + void help() override; + + goto_inspect_parse_optionst(int argc, const char *argv[]); +}; + +#endif // CPROVER_GOTO_INSPECT_GOTO_INSPECT_PARSE_OPTIONS_H diff --git a/src/goto-inspect/module_dependencies.txt b/src/goto-inspect/module_dependencies.txt new file mode 100644 index 00000000000..a7a95a1321a --- /dev/null +++ b/src/goto-inspect/module_dependencies.txt @@ -0,0 +1,2 @@ +goto-programs +util diff --git a/src/goto-inspect/readme.md b/src/goto-inspect/readme.md new file mode 100644 index 00000000000..98ccfb3106d --- /dev/null +++ b/src/goto-inspect/readme.md @@ -0,0 +1,10 @@ +\ingroup module_hidden +\defgroup goto-inspect goto-inspect + +# Folder goto-inspect + +\author Fotis Koutoulakis + +The `goto-inspect/` contains the code for the binary `goto-inspect`, intended +to provide an all-purpose tool for inspection of goto-binaries (properties, +goto-functions, etc).