From 96306e49376948cb716dc3b17832e1586a4c258c Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 22 Nov 2021 21:56:43 +0000 Subject: [PATCH 01/14] --all is not implemented, not clear that it has a sensible implementation --- src/goto-instrument/goto_instrument_parse_options.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 5b12310641a..1362a20ebb7 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -39,7 +39,6 @@ Author: Daniel Kroening, kroening@kroening.com // clang-format off #define GOTO_INSTRUMENT_OPTIONS \ - "(all)" \ "(document-claims-latex)(document-claims-html)" \ "(document-properties-latex)(document-properties-html)" \ "(dump-c-type-header):" \ From 27d4ab6c68fd79a80cd5da0beb55b94adc4e29a6 Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 22 Nov 2021 22:11:03 +0000 Subject: [PATCH 02/14] OPT_ and HELP_ macros for the document properties flags --- src/goto-instrument/document_properties.h | 11 +++++++++++ src/goto-instrument/goto_instrument_parse_options.cpp | 4 +--- src/goto-instrument/goto_instrument_parse_options.h | 4 ++-- 3 files changed, 14 insertions(+), 5 deletions(-) diff --git a/src/goto-instrument/document_properties.h b/src/goto-instrument/document_properties.h index 45f1b147ca7..f48f9440f00 100644 --- a/src/goto-instrument/document_properties.h +++ b/src/goto-instrument/document_properties.h @@ -24,4 +24,15 @@ void document_properties_html( const goto_modelt &, std::ostream &out); +#define OPT_DOCUMENT_PROPERTIES \ + "(document-claims-latex)(document-claims-html)" \ + "(document-properties-latex)(document-properties-html)" + +// clang-format off +#define HELP_DOCUMENT_PROPERTIES \ + " --document-properties-html generate HTML property documentation\n" \ + " --document-properties-latex generate Latex property documentation\n" + +// clang-format on + #endif // CPROVER_GOTO_INSTRUMENT_DOCUMENT_PROPERTIES_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 8bc4ff2b7a7..fd84c2374ee 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -85,7 +85,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "branch.h" #include "call_sequences.h" #include "concurrency.h" -#include "document_properties.h" #include "dot.h" #include "dump_c.h" #include "full_slicer.h" @@ -1722,8 +1721,7 @@ void goto_instrument_parse_optionst::help() " goto-instrument in out perform instrumentation\n" "\n" "Main options:\n" - " --document-properties-html generate HTML property documentation\n" - " --document-properties-latex generate Latex property documentation\n" + HELP_DOCUMENT_PROPERTIES " --dump-c generate C source\n" " --dump-c-type-header m generate a C header for types local in m\n" " --dump-cpp generate C++ source\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 1362a20ebb7..e0100f352e3 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -30,6 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "aggressive_slicer.h" #include "contracts/contracts.h" +#include "document_properties.h" #include "generate_function_bodies.h" #include "insert_final_assert_false.h" #include "nondet_volatile.h" @@ -39,8 +40,7 @@ Author: Daniel Kroening, kroening@kroening.com // clang-format off #define GOTO_INSTRUMENT_OPTIONS \ - "(document-claims-latex)(document-claims-html)" \ - "(document-properties-latex)(document-properties-html)" \ + OPT_DOCUMENT_PROPERTIES \ "(dump-c-type-header):" \ "(dump-c)(dump-cpp)(no-system-headers)(use-all-headers)(dot)(xml)" \ "(harness)" \ From f8364660ba77d5d0470a3cc3e7d642d530935bf5 Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 22 Nov 2021 22:45:54 +0000 Subject: [PATCH 03/14] Add basic "does it run" tests for the --document options --- .../document-properties-basic/html.desc | 10 ++++++++++ .../document-properties-basic/latex.desc | 10 ++++++++++ .../goto-instrument/document-properties-basic/main.c | 8 ++++++++ 3 files changed, 28 insertions(+) create mode 100644 regression/goto-instrument/document-properties-basic/html.desc create mode 100644 regression/goto-instrument/document-properties-basic/latex.desc create mode 100644 regression/goto-instrument/document-properties-basic/main.c diff --git a/regression/goto-instrument/document-properties-basic/html.desc b/regression/goto-instrument/document-properties-basic/html.desc new file mode 100644 index 00000000000..b73e500ba57 --- /dev/null +++ b/regression/goto-instrument/document-properties-basic/html.desc @@ -0,0 +1,10 @@ +CORE +main.c +--document-properties-html +^EXIT=0$ +^SIGNAL=0$ +^ assert\(1 == 1\);<\/em>$ +-- +^warning: ignoring +-- +Tests whether this option works at all. diff --git a/regression/goto-instrument/document-properties-basic/latex.desc b/regression/goto-instrument/document-properties-basic/latex.desc new file mode 100644 index 00000000000..6d9c44ce59b --- /dev/null +++ b/regression/goto-instrument/document-properties-basic/latex.desc @@ -0,0 +1,10 @@ +CORE +main.c +--document-properties-latex +^EXIT=0$ +^SIGNAL=0$ +^\\claim\{assertion 1 == 1\}$ +-- +^warning: ignoring +-- +Tests whether this option works at all. diff --git a/regression/goto-instrument/document-properties-basic/main.c b/regression/goto-instrument/document-properties-basic/main.c new file mode 100644 index 00000000000..802bae87713 --- /dev/null +++ b/regression/goto-instrument/document-properties-basic/main.c @@ -0,0 +1,8 @@ +#include + +int main(int argc, char **argv) +{ + assert(1 == 1); + + return 0; +} From 6a18cb1c891cee2a49bee5b509ade12760297ee0 Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 22 Nov 2021 23:05:19 +0000 Subject: [PATCH 04/14] OPT_ and HELP_ macros for the dump-c flags --- src/goto-instrument/dump_c.h | 16 ++++++++++++++++ .../goto_instrument_parse_options.cpp | 10 +++------- .../goto_instrument_parse_options.h | 6 +++--- 3 files changed, 22 insertions(+), 10 deletions(-) diff --git a/src/goto-instrument/dump_c.h b/src/goto-instrument/dump_c.h index 3fb56ea2712..69820a33d3f 100644 --- a/src/goto-instrument/dump_c.h +++ b/src/goto-instrument/dump_c.h @@ -43,4 +43,20 @@ void dump_cpp( const namespacet &ns, std::ostream &out); +#define OPT_DUMP_C \ + "(dump-c)(dump-cpp)" \ + "(dump-c-type-header):" \ + "(no-system-headers)(use-all-headers)(harness)" + +// clang-format off +#define HELP_DUMP_C \ + " --dump-c generate C source\n" \ + " --dump-c-type-header m generate a C header for types local in m\n" \ + " --dump-cpp generate C++ source\n" \ + " --no-system-headers generate C source expanding libc includes\n"\ + " --use-all-headers generate C source with all includes\n" \ + " --harness include input generator in output\n" + +// clang-format on + #endif // CPROVER_GOTO_INSTRUMENT_DUMP_C_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index fd84c2374ee..e82006393e9 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -86,7 +86,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "call_sequences.h" #include "concurrency.h" #include "dot.h" -#include "dump_c.h" #include "full_slicer.h" #include "function.h" #include "havoc_loops.h" @@ -1722,12 +1721,12 @@ void goto_instrument_parse_optionst::help() "\n" "Main options:\n" HELP_DOCUMENT_PROPERTIES - " --dump-c generate C source\n" - " --dump-c-type-header m generate a C header for types local in m\n" - " --dump-cpp generate C++ source\n" " --dot generate CFG graph in DOT format\n" " --interpreter do concrete execution\n" "\n" + "Dump Source:\n" + HELP_DUMP_C + "\n" "Diagnosis:\n" " --show-loops show the loops in the program\n" HELP_SHOW_PROPERTIES @@ -1851,9 +1850,6 @@ void goto_instrument_parse_optionst::help() HELP_ENFORCE_CONTRACT "\n" "Other options:\n" - " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*) - " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*) - " --harness with --dump-c/--dump-cpp: include input generator in output\n" // NOLINT(*) " --version show version and exit\n" HELP_FLUSH " --xml-ui use XML-formatted output\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index e0100f352e3..c168314b636 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -31,6 +31,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "aggressive_slicer.h" #include "contracts/contracts.h" #include "document_properties.h" +#include "dump_c.h" #include "generate_function_bodies.h" #include "insert_final_assert_false.h" #include "nondet_volatile.h" @@ -41,9 +42,8 @@ Author: Daniel Kroening, kroening@kroening.com // clang-format off #define GOTO_INSTRUMENT_OPTIONS \ OPT_DOCUMENT_PROPERTIES \ - "(dump-c-type-header):" \ - "(dump-c)(dump-cpp)(no-system-headers)(use-all-headers)(dot)(xml)" \ - "(harness)" \ + OPT_DUMP_C \ + "(dot)(xml)" \ OPT_GOTO_CHECK \ /* no-X-check are deprecated and ignored */ \ "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \ From 033506bc3eb03539ae65627155062005944beea5 Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 23 Nov 2021 07:28:17 +0000 Subject: [PATCH 05/14] Remove --no-pointer-check from CBMC KNOWNBUG tests This option has long been deprecated and then removed from cbmc. I guess it only stayed in these tests as they have also long been marked as KNOWNBUG. --- regression/cbmc-cpp/Overloading_Operators16/test.desc | 2 +- regression/cbmc-cpp/virtual11/test.desc | 2 +- regression/cbmc-cpp/virtual12/test.desc | 2 +- regression/cbmc-cpp/virtual3/test.desc | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/regression/cbmc-cpp/Overloading_Operators16/test.desc b/regression/cbmc-cpp/Overloading_Operators16/test.desc index 1eb75202b41..6666d172f47 100644 --- a/regression/cbmc-cpp/Overloading_Operators16/test.desc +++ b/regression/cbmc-cpp/Overloading_Operators16/test.desc @@ -1,6 +1,6 @@ KNOWNBUG main.cpp ---no-pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-cpp/virtual11/test.desc b/regression/cbmc-cpp/virtual11/test.desc index 419c45813dd..f23a03ce789 100644 --- a/regression/cbmc-cpp/virtual11/test.desc +++ b/regression/cbmc-cpp/virtual11/test.desc @@ -1,6 +1,6 @@ KNOWNBUG main.cpp ---unwind 1 --no-pointer-check +--unwind 1 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-cpp/virtual12/test.desc b/regression/cbmc-cpp/virtual12/test.desc index 419c45813dd..f23a03ce789 100644 --- a/regression/cbmc-cpp/virtual12/test.desc +++ b/regression/cbmc-cpp/virtual12/test.desc @@ -1,6 +1,6 @@ KNOWNBUG main.cpp ---unwind 1 --no-pointer-check +--unwind 1 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-cpp/virtual3/test.desc b/regression/cbmc-cpp/virtual3/test.desc index 1eb75202b41..6666d172f47 100644 --- a/regression/cbmc-cpp/virtual3/test.desc +++ b/regression/cbmc-cpp/virtual3/test.desc @@ -1,6 +1,6 @@ KNOWNBUG main.cpp ---no-pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ From 49f44f86c1dcd9a2ad7323f93dbf14d6520296e1 Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 23 Nov 2021 07:32:00 +0000 Subject: [PATCH 06/14] Remove the --no-*-check options from goto-instrument These are not implemented, not used by any test, removed from other tools and marked deprecated almost 5 years ago. --- src/goto-instrument/goto_instrument_parse_options.h | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index c168314b636..2d511abc3b6 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -45,9 +45,6 @@ Author: Daniel Kroening, kroening@kroening.com OPT_DUMP_C \ "(dot)(xml)" \ OPT_GOTO_CHECK \ - /* no-X-check are deprecated and ignored */ \ - "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \ - "(no-nan-check)" \ "(remove-pointers)" \ "(no-simplify)" \ "(uninitialized-check)" \ From 62c30622c8026ac907e30f19ece3560fb8a1d89a Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 23 Nov 2021 07:44:23 +0000 Subject: [PATCH 07/14] OPT_ and HELP_ macros for the remove options flag --- src/goto-instrument/goto_instrument_parse_options.cpp | 3 +-- src/goto-instrument/goto_instrument_parse_options.h | 4 +++- src/pointer-analysis/goto_program_dereference.h | 8 ++++++++ 3 files changed, 12 insertions(+), 3 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index e82006393e9..9fba5ffd296 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -52,7 +52,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -1777,7 +1776,7 @@ void goto_instrument_parse_optionst::help() " --nondet-static-exclude e same as nondet-static except for the variable e\n" //NOLINT(*) " (use multiple times if required)\n" " --check-invariant function instruments invariant checking function\n" - " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*) + HELP_REMOVE_POINTERS " --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*) " --undefined-function-is-assume-false\n" // NOLINTNEXTLINE(whitespace/line_length) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 2d511abc3b6..9e411a039b3 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -28,6 +28,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + #include "aggressive_slicer.h" #include "contracts/contracts.h" #include "document_properties.h" @@ -45,7 +47,7 @@ Author: Daniel Kroening, kroening@kroening.com OPT_DUMP_C \ "(dot)(xml)" \ OPT_GOTO_CHECK \ - "(remove-pointers)" \ + OPT_REMOVE_POINTERS \ "(no-simplify)" \ "(uninitialized-check)" \ "(race-check)(scc)(one-event-per-cycle)" \ diff --git a/src/pointer-analysis/goto_program_dereference.h b/src/pointer-analysis/goto_program_dereference.h index e0a81ccf903..ec4cf0ae26c 100644 --- a/src/pointer-analysis/goto_program_dereference.h +++ b/src/pointer-analysis/goto_program_dereference.h @@ -107,4 +107,12 @@ void remove_pointers( goto_modelt &, value_setst &); +#define OPT_REMOVE_POINTERS "(remove-pointers)" + +// clang-format off +#define HELP_REMOVE_POINTERS \ + " --remove-pointers converts pointer arithmetic to base+offset expressions\n" /* NOLINT(whitespace/line_length) */ + +// clang-format on + #endif // CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H From 75873b57d33ba716b43d11597ba83307960df2cb Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 23 Nov 2021 21:57:53 +0000 Subject: [PATCH 08/14] Document the XML output option Note that this is different to --xml-ui which shift the tool's general output into XML; --xml only affects a few options that produce analysis results. --- src/goto-instrument/goto_instrument_parse_options.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 9fba5ffd296..f5a1d89725e 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1851,6 +1851,7 @@ void goto_instrument_parse_optionst::help() "Other options:\n" " --version show version and exit\n" HELP_FLUSH + " --xml output files in XML where supported\n" " --xml-ui use XML-formatted output\n" " --json-ui use JSON-formatted output\n" HELP_TIMESTAMP From 8c47a4fb5b4597bc9d942391d11bee268284daa3 Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 23 Nov 2021 22:06:33 +0000 Subject: [PATCH 09/14] OPT_ and HELP_ macros for the uninitialized local variable check flag --- src/goto-instrument/goto_instrument_parse_options.cpp | 3 +-- src/goto-instrument/goto_instrument_parse_options.h | 3 ++- src/goto-instrument/uninitialized.h | 6 ++++++ 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index f5a1d89725e..872ebfb16ab 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -107,7 +107,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "stack_depth.h" #include "thread_instrumentation.h" #include "undefined_functions.h" -#include "uninitialized.h" #include "unwind.h" #include "unwindset.h" #include "value_set_fi_fp_removal.h" @@ -1758,7 +1757,7 @@ void goto_instrument_parse_optionst::help() "Safety checks:\n" " --no-assertions ignore user assertions\n" HELP_GOTO_CHECK - " --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*) + HELP_UNINITIALIZED_CHECK " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*) " --race-check add floating-point data race checks\n" "\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 9e411a039b3..dc8c6a4f162 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -38,6 +38,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "insert_final_assert_false.h" #include "nondet_volatile.h" #include "replace_calls.h" +#include "uninitialized.h" #include "count_eloc.h" @@ -49,7 +50,7 @@ Author: Daniel Kroening, kroening@kroening.com OPT_GOTO_CHECK \ OPT_REMOVE_POINTERS \ "(no-simplify)" \ - "(uninitialized-check)" \ + OPT_UNINITIALIZED_CHECK \ "(race-check)(scc)(one-event-per-cycle)" \ "(minimum-interference)" \ "(mm):(my-events)" \ diff --git a/src/goto-instrument/uninitialized.h b/src/goto-instrument/uninitialized.h index ff2b85b9d22..7e421233f77 100644 --- a/src/goto-instrument/uninitialized.h +++ b/src/goto-instrument/uninitialized.h @@ -24,4 +24,10 @@ void show_uninitialized( const goto_modelt &, std::ostream &out); +#define OPT_UNINITIALIZED_CHECK "(uninitialized-check)" + +#define HELP_UNINITIALIZED_CHECK \ + " --uninitialized-check add checks for uninitialized locals " \ + "(experimental)\n" // NOLINT(whitespace/line_length) + #endif // CPROVER_GOTO_INSTRUMENT_UNINITIALIZED_H From 8a6ff179feb6f8f0071bb39d3e993e382bf10476 Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 23 Nov 2021 22:30:49 +0000 Subject: [PATCH 10/14] Improve the error messages given by the uninitialized checks --- src/goto-instrument/uninitialized.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-instrument/uninitialized.cpp index d22f8a400ed..a80099b6d39 100644 --- a/src/goto-instrument/uninitialized.cpp +++ b/src/goto-instrument/uninitialized.cpp @@ -158,7 +158,7 @@ void uninitializedt::add_assertions( symbol_exprt(new_identifier, bool_typet()), instruction.source_location()); assertion.source_location_nonconst().set_comment( - "use of uninitialized local variable"); + "use of uninitialized local variable " + id2string(identifier)); assertion.source_location_nonconst().set_property_class( "uninitialized local"); From 44a1fc94e45ac4eaea54ef9dfe9c65293b9bc908 Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 23 Nov 2021 22:43:29 +0000 Subject: [PATCH 11/14] Add a test for the uninitialized local variable check --- .../uninitialized-check/main.c | 29 +++++++++++++++++++ .../uninitialized-check/test.desc | 16 ++++++++++ 2 files changed, 45 insertions(+) create mode 100644 regression/goto-instrument/uninitialized-check/main.c create mode 100644 regression/goto-instrument/uninitialized-check/test.desc diff --git a/regression/goto-instrument/uninitialized-check/main.c b/regression/goto-instrument/uninitialized-check/main.c new file mode 100644 index 00000000000..fe472b1bc7d --- /dev/null +++ b/regression/goto-instrument/uninitialized-check/main.c @@ -0,0 +1,29 @@ +#include + +int globals_are_actually_initialized; // See ISO-9899! + +int main(int argc, char **argv) +{ + int definitely_uninitialized; + int maybe_uninitialized; + int actually_initialized; + + if(argc > 1) + { + maybe_uninitialized = 1; + } + + if(argc <= 3) + { + actually_initialized = 0; + } + if(argc >= 4) + { + actually_initialized = 1; + } + + int *heap_variables_uninitialized = malloc(sizeof(int)); + + return definitely_uninitialized + maybe_uninitialized + actually_initialized + + globals_are_actually_initialized + *heap_variables_uninitialized; +} diff --git a/regression/goto-instrument/uninitialized-check/test.desc b/regression/goto-instrument/uninitialized-check/test.desc new file mode 100644 index 00000000000..cd0985c3076 --- /dev/null +++ b/regression/goto-instrument/uninitialized-check/test.desc @@ -0,0 +1,16 @@ +CORE +main.c +--uninitialized-check +^\[main.uninitialized_local.1\] line \d+ use of uninitialized local variable main::1::definitely_uninitialized: FAILURE$ +^\[main.uninitialized_local.2\] line \d+ use of uninitialized local variable main::1::maybe_uninitialized: FAILURE$ +^\[main.uninitialized_local.3\] line \d+ use of uninitialized local variable main::1::actually_initialized: SUCCESS$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +A basic test of the uninitialized variable check. +In an ideal world there would be a check for heap_variables_uninitialized +that would fail however this is beyond the current scope of the analysis. + From 6fb3bffb274032adee29db511d9e8eb83b2d6213 Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 23 Nov 2021 22:56:08 +0000 Subject: [PATCH 12/14] Fix up the include order of local headers --- src/goto-instrument/goto_instrument_parse_options.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index dc8c6a4f162..5b92f852ed9 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -32,6 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "aggressive_slicer.h" #include "contracts/contracts.h" +#include "count_eloc.h" #include "document_properties.h" #include "dump_c.h" #include "generate_function_bodies.h" @@ -40,8 +41,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "replace_calls.h" #include "uninitialized.h" -#include "count_eloc.h" - // clang-format off #define GOTO_INSTRUMENT_OPTIONS \ OPT_DOCUMENT_PROPERTIES \ From b1c61dc7dd31113250965c5e644ab7c5963ebfd9 Mon Sep 17 00:00:00 2001 From: martin Date: Wed, 24 Nov 2021 15:32:39 +0000 Subject: [PATCH 13/14] OPT_ and HELP_ macros for the weak memory model flags This also adds: --read-first --write-first --no-loop-duplication --hide-internals which are handled by goto-instrument but were not options so couldn't be used. --- .../goto_instrument_parse_options.cpp | 13 +---- .../goto_instrument_parse_options.h | 10 ++-- src/goto-instrument/wmm/weak_memory.h | 51 +++++++++++++++++++ 3 files changed, 55 insertions(+), 19 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 872ebfb16ab..858a24da0c7 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -110,7 +110,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "unwind.h" #include "unwindset.h" #include "value_set_fi_fp_removal.h" -#include "wmm/weak_memory.h" /// invoke main modules int goto_instrument_parse_optionst::doit() @@ -1793,17 +1792,7 @@ void goto_instrument_parse_optionst::help() " --skip-loops add gotos to skip selected loops during execution\n" // NOLINT(*) "\n" "Memory model instrumentations:\n" - " --mm instruments a weak memory model\n" - " --scc detects critical cycles per SCC (one thread per SCC)\n" // NOLINT(*) - " --one-event-per-cycle only instruments one event per cycle\n" - " --minimum-interference instruments an optimal number of events\n" - " --my-events only instruments events whose ids appear in inst.evt\n" // NOLINT(*) - " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" // NOLINT(*) - " --no-dependencies no dependency analysis\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --no-po-rendering no representation of the threads in the dot\n" - " --render-cluster-file clusterises the dot by files\n" - " --render-cluster-function clusterises the dot by functions\n" + HELP_WMM_FULL "\n" "Slicing:\n" HELP_REACHABILITY_SLICER diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 5b92f852ed9..f209dc14116 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -40,6 +40,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "nondet_volatile.h" #include "replace_calls.h" #include "uninitialized.h" +#include "wmm/weak_memory.h" // clang-format off #define GOTO_INSTRUMENT_OPTIONS \ @@ -50,18 +51,14 @@ Author: Daniel Kroening, kroening@kroening.com OPT_REMOVE_POINTERS \ "(no-simplify)" \ OPT_UNINITIALIZED_CHECK \ - "(race-check)(scc)(one-event-per-cycle)" \ - "(minimum-interference)" \ - "(mm):(my-events)" \ + OPT_WMM \ + "(race-check)" \ "(unwind):(unwindset):(unwindset-file):" \ "(unwinding-assertions)(partial-loops)(continue-as-loops)" \ "(log):" \ - "(max-var):(max-po-trans):(ignore-arrays)" \ - "(cfg-kill)(no-dependencies)(force-loop-duplication)" \ "(call-graph)(reachable-call-graph)" \ OPT_INSERT_FINAL_ASSERT_FALSE \ OPT_SHOW_CLASS_HIERARCHY \ - "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \ "(isr):" \ "(stack-depth):(nondet-static)" \ "(nondet-static-exclude):" \ @@ -85,7 +82,6 @@ Author: Daniel Kroening, kroening@kroening.com "(remove-function-pointers)" \ "(show-claims)(property):" \ "(show-symbol-table)(show-points-to)(show-rw-set)" \ - "(cav11)" \ OPT_TIMESTAMP \ "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \ "(string-abstraction)" \ diff --git a/src/goto-instrument/wmm/weak_memory.h b/src/goto-instrument/wmm/weak_memory.h index a8764f7877b..bbb7bb596ad 100644 --- a/src/goto-instrument/wmm/weak_memory.h +++ b/src/goto-instrument/wmm/weak_memory.h @@ -54,4 +54,55 @@ void introduce_temporaries( #endif messaget &message); +// clang-format off +#define OPT_WMM_MEMORY_MODEL "(mm):" + +#define OPT_WMM_INSTRUMENTATION_STRATEGIES \ + "(one-event-per-cycle)" \ + "(minimum-interference)" \ + "(read-first)" \ + "(write-first)" \ + "(my-events)" \ + +#define OPT_WMM_LIMITS \ + "(max-var):" \ + "(max-po-trans):" \ + +#define OPT_WMM_LOOPS \ + "(force-loop-duplication)" \ + "(no-loop-duplication)" \ + +#define OPT_WMM_MISC \ + "(scc)" \ + "(cfg-kill)" \ + "(no-dependencies)" \ + "(no-po-rendering)" \ + "(render-cluster-file)" \ + "(render-cluster-function)" \ + "(cav11)" \ + "(hide-internals)" \ + "(ignore-arrays)" \ + +#define OPT_WMM \ + OPT_WMM_MEMORY_MODEL \ + OPT_WMM_INSTRUMENTATION_STRATEGIES \ + OPT_WMM_LIMITS \ + OPT_WMM_LOOPS \ + OPT_WMM_MISC \ + + +#define HELP_WMM_FULL \ + " --mm instruments a weak memory model\n" \ + " --scc detects critical cycles per SCC (one thread per SCC)\n" /* NOLINT(whitespace/line_length) */ \ + " --one-event-per-cycle only instruments one event per cycle\n" \ + " --minimum-interference instruments an optimal number of events\n" \ + " --my-events only instruments events whose ids appear in inst.evt\n" /* NOLINT(whitespace/line_length) */ \ + " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" /* NOLINT(whitespace/line_length) */ \ + " --no-dependencies no dependency analysis\n" \ + " --no-po-rendering no representation of the threads in the dot\n"\ + " --render-cluster-file clusterises the dot by files\n" \ + " --render-cluster-function clusterises the dot by functions\n" + +// clang-format on + #endif // CPROVER_GOTO_INSTRUMENT_WMM_WEAK_MEMORY_H From b71a83009aca91198e67c0a24c5714331df03a10 Mon Sep 17 00:00:00 2001 From: martin Date: Wed, 24 Nov 2021 15:34:44 +0000 Subject: [PATCH 14/14] Remove the --mm option from goto-diff This was tested for but does not appear as an option in goto_diff_parse_options.h as a valid option so this code can never be used. Worse, goto-diff doesn't include any of the code that uses it, nor can I think what the memory model might have to do with diffing goto-programs. --- src/goto-diff/goto_diff_parse_options.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 5e108b9541a..4e6a2798322 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -70,9 +70,6 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("cover")) parse_cover_options(cmdline, options); - if(cmdline.isset("mm")) - options.set_option("mm", cmdline.get_value("mm")); - // all checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options);