From 677be21ca4098915735c54cdac421118cffecd8b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 31 May 2022 07:55:13 +0000 Subject: [PATCH 1/4] Move namespace declaration close to (single) use There is no need to declare in a parent scope what is only used in a single branch. --- src/goto-instrument/goto_instrument_parse_options.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 09f13c5fe08..c9f53af5df7 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1059,8 +1059,6 @@ void goto_instrument_parse_optionst::instrument_goto_program() throw 0; } - namespacet ns(goto_model.symbol_table); - // initialize argv with valid pointers if(cmdline.isset("model-argc-argv")) { @@ -1420,6 +1418,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() do_indirect_call_and_rtti_removal(); log.status() << "Pointer Analysis" << messaget::eom; + const namespacet ns(goto_model.symbol_table); value_set_analysist value_set_analysis(ns); value_set_analysis(goto_model.goto_functions); From 56944c25fa0d26bcf9e03d84b0ed75936a10b2bf Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 31 May 2022 08:00:42 +0000 Subject: [PATCH 2/4] Remove "unwind" option parsing that is no longer required The unwinding done by goto-instrument is configured elsewhere and makes no use of this option parsing. It used to be used by weak-memory instrumentation, but this is no longer the case. --- src/goto-instrument/goto_instrument_parse_options.cpp | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index c9f53af5df7..e0893839758 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1029,13 +1029,6 @@ void goto_instrument_parse_optionst::instrument_goto_program() // all checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); - // unwind loops - if(cmdline.isset("unwind")) - { - log.status() << "Unwinding loops" << messaget::eom; - options.set_option("unwind", cmdline.get_value("unwind")); - } - { parse_function_pointer_restriction_options_from_cmdline(cmdline, options); From 7e56e96a146d00ea8ee695636ae625a59d7e6fd1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 31 May 2022 08:01:52 +0000 Subject: [PATCH 3/4] Goto-instrument: Remove inline ASM before adding library functions Just like CBMC, we need to make sure that library functions called via inline assembly are resolved. --- src/goto-instrument/goto_instrument_parse_options.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index e0893839758..c397296e689 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1087,6 +1087,10 @@ void goto_instrument_parse_optionst::instrument_goto_program() std::string(CPROVER_PREFIX) + "CUSTOM_BITVECTOR_ANALYSIS"); } + // remove inline assembler as that may yield further library function calls + // that need to be resolved + remove_asm(goto_model); + // add the library log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << messaget::eom; From 5c9827218670f3f050d6cbb97bc8d16495dcbef6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 31 May 2022 08:02:40 +0000 Subject: [PATCH 4/4] Goto-instrument: Include the library in function pointer restrictions and loop skipping Adding additional code should be the first order of business, and all transformations can only be applied thereafter to make sure they equally apply to library code. --- .../goto_instrument_parse_options.cpp | 48 ++++++++++--------- 1 file changed, 25 insertions(+), 23 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index c397296e689..df91f7be78c 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1029,29 +1029,6 @@ void goto_instrument_parse_optionst::instrument_goto_program() // all checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); - { - parse_function_pointer_restriction_options_from_cmdline(cmdline, options); - - if( - options.is_set(RESTRICT_FUNCTION_POINTER_OPT) || - options.is_set(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT) || - options.is_set(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT)) - { - label_function_pointer_call_sites(goto_model); - - restrict_function_pointers(ui_message_handler, goto_model, options); - } - } - - // skip over selected loops - if(cmdline.isset("skip-loops")) - { - log.status() << "Adding gotos to skip loops" << messaget::eom; - if(skip_loops( - goto_model, cmdline.get_value("skip-loops"), ui_message_handler)) - throw 0; - } - // initialize argv with valid pointers if(cmdline.isset("model-argc-argv")) { @@ -1099,6 +1076,31 @@ void goto_instrument_parse_optionst::instrument_goto_program() link_to_library(goto_model, ui_message_handler, cprover_c_library_factory); } + { + parse_function_pointer_restriction_options_from_cmdline(cmdline, options); + + if( + options.is_set(RESTRICT_FUNCTION_POINTER_OPT) || + options.is_set(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT) || + options.is_set(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT)) + { + label_function_pointer_call_sites(goto_model); + + restrict_function_pointers(ui_message_handler, goto_model, options); + } + } + + // skip over selected loops + if(cmdline.isset("skip-loops")) + { + log.status() << "Adding gotos to skip loops" << messaget::eom; + if(skip_loops( + goto_model, cmdline.get_value("skip-loops"), ui_message_handler)) + { + throw 0; + } + } + // now do full inlining, if requested if(cmdline.isset("inline")) {