From e14e33d63e4a2dbdb9986e255803bcdf4cc2142a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 8 Mar 2022 22:01:51 +0000 Subject: [PATCH 1/2] Replace the goto_check indirection by direct use of goto_check_c All existing calls necessarily end up calling goto_check_c. --- .../accelerate/acceleration_utils.cpp | 2 +- .../goto_instrument_parse_options.cpp | 2 +- src/goto-programs/goto_check.cpp | 40 +------------------ src/goto-programs/goto_check.h | 20 +--------- src/goto-programs/process_goto_program.cpp | 4 +- 5 files changed, 8 insertions(+), 60 deletions(-) diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index 660e0c16188..2e525a8fa2b 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -475,7 +475,7 @@ void acceleration_utilst::ensure_no_overflows(scratch_programt &program) // goto_functionst::goto_functiont fn; // fn.body.instructions.swap(program.instructions); - // goto_check(ns, checker_options, fn); + // goto_check_c(ns, checker_options, fn); // fn.body.instructions.swap(program.instructions); #ifdef DEBUG diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index efea60220bd..ed029d6212b 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1328,7 +1328,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() } // add generic checks, if needed - goto_check(options, goto_model, ui_message_handler); + goto_check_c(options, goto_model, ui_message_handler); transform_assertions_assumptions(options, goto_model); // check for uninitalized local variables diff --git a/src/goto-programs/goto_check.cpp b/src/goto-programs/goto_check.cpp index c3f5e28576a..e105d98553b 100644 --- a/src/goto-programs/goto_check.cpp +++ b/src/goto-programs/goto_check.cpp @@ -12,45 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_check.h" #include -#include -#include -#include - -#include - -void goto_check( - const irep_idt &function_identifier, - goto_functionst::goto_functiont &goto_function, - const namespacet &ns, - const optionst &options, - message_handlert &message_handler) -{ - const auto &function_symbol = ns.lookup(function_identifier); - - if(function_symbol.mode == ID_C) - { - goto_check_c( - function_identifier, goto_function, ns, options, message_handler); - } -} - -void goto_check( - const namespacet &ns, - const optionst &options, - goto_functionst &goto_functions, - message_handlert &message_handler) -{ - goto_check_c(ns, options, goto_functions, message_handler); -} - -void goto_check( - const optionst &options, - goto_modelt &goto_model, - message_handlert &message_handler) -{ - goto_check_c(options, goto_model, message_handler); -} +#include "goto_model.h" +#include "remove_skip.h" static void transform_assertions_assumptions( goto_programt &goto_program, diff --git a/src/goto-programs/goto_check.h b/src/goto-programs/goto_check.h index b95e38afd94..91bbaedf264 100644 --- a/src/goto-programs/goto_check.h +++ b/src/goto-programs/goto_check.h @@ -12,27 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H #define CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H -#include "goto_functions.h" - class goto_modelt; -class namespacet; +class goto_programt; class optionst; -class message_handlert; - -void goto_check( - const namespacet &, - const optionst &, - goto_functionst &, - message_handlert &); - -void goto_check( - const irep_idt &function_identifier, - goto_functionst::goto_functiont &, - const namespacet &, - const optionst &, - message_handlert &); - -void goto_check(const optionst &, goto_modelt &, message_handlert &); /// Handle the options "assertions", "built-in-assertions", "assumptions" to /// remove assertions and assumptions in \p goto_model when these are set to diff --git a/src/goto-programs/process_goto_program.cpp b/src/goto-programs/process_goto_program.cpp index 17a8bbf923a..bcde95f76f6 100644 --- a/src/goto-programs/process_goto_program.cpp +++ b/src/goto-programs/process_goto_program.cpp @@ -27,6 +27,8 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include #include +#include + #include "goto_check.h" bool process_goto_program( @@ -73,7 +75,7 @@ bool process_goto_program( // add generic checks log.status() << "Generic Property Instrumentation" << messaget::eom; - goto_check(options, goto_model, log.get_message_handler()); + goto_check_c(options, goto_model, log.get_message_handler()); transform_assertions_assumptions(options, goto_model); // checks don't know about adjusted float expressions From dd7cd37767a1961f2f8ff1bdf2e2b9046dce62dc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Feb 2022 23:24:36 +0000 Subject: [PATCH 2/2] Filter generated assertions according to command-line settings Turn into skip C/C++ goto checks that were previously generated, but are no longer expected as configured via the command line. --- .../goto_instrument_parse_options.cpp | 1 + src/goto-programs/goto_check.cpp | 160 ++++++++++++++++++ src/goto-programs/goto_check.h | 2 + src/goto-programs/process_goto_program.cpp | 1 + 4 files changed, 164 insertions(+) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index ed029d6212b..8de4afb8dce 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1329,6 +1329,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() // add generic checks, if needed goto_check_c(options, goto_model, ui_message_handler); + remove_disabled_checks(options, goto_model); transform_assertions_assumptions(options, goto_model); // check for uninitalized local variables diff --git a/src/goto-programs/goto_check.cpp b/src/goto-programs/goto_check.cpp index e105d98553b..b149f2fb9eb 100644 --- a/src/goto-programs/goto_check.cpp +++ b/src/goto-programs/goto_check.cpp @@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_check.h" #include +#include +#include #include "goto_model.h" #include "remove_skip.h" @@ -96,3 +98,161 @@ void transform_assertions_assumptions( enable_built_in_assertions, enable_assumptions); } + +void remove_disabled_checks(const optionst &options, goto_modelt &goto_model) +{ + // properties to keep + const bool enable_bounds_check = options.get_bool_option("bounds-check"); + const bool enable_conversion_check = + options.get_bool_option("conversion-check"); + const bool enable_div_by_zero_check = + options.get_bool_option("div-by-zero-check"); + const bool enable_enum_range_check = + options.get_bool_option("enum-range-check"); + const bool enable_float_overflow_check = + options.get_bool_option("float-overflow-check"); + const bool enable_memory_leak_check = + options.get_bool_option("memory-leak-check"); + const bool enable_nan_check = options.get_bool_option("nan-check"); + const bool enable_pointer_check = options.get_bool_option("pointer-check"); + const bool enable_pointer_overflow_check = + options.get_bool_option("pointer-overflow-check"); + const bool enable_pointer_primitive_check = + options.get_bool_option("pointer-primitive-check"); + const bool enable_signed_overflow_check = + options.get_bool_option("signed-overflow-check"); + const bool enable_undefined_shift_check = + options.get_bool_option("undefined-shift-check"); + const bool enable_unsigned_overflow_check = + options.get_bool_option("unsigned-overflow-check"); + const auto error_labels = options.get_list_option("error-label"); + + // transformations retained on properties + // const bool enable_simplify = options.get_bool_option("simplify"); + const bool enable_assert_to_assume = + options.get_bool_option("assert-to-assume"); + // const bool retain_trivial = options.get_bool_option("retain-trivial-checks"); + + const std::unordered_map should_skip = { + {"NaN", !enable_nan_check}, + {"array bounds", !enable_bounds_check}, + {"bit count", !enable_bounds_check}, + {"division-by-zero", !enable_div_by_zero_check}, + {"enum-range-check", !enable_enum_range_check}, + {"error label", error_labels.empty()}, // further evaluation is necessary + {"memory-leak", !enable_memory_leak_check}, + {"overflow", false}, // further evaluation is necessary + {"pointer arithmetic", + !enable_pointer_check && !enable_pointer_overflow_check}, + {"pointer dereference", !enable_pointer_check}, + {"pointer primitives", !enable_pointer_primitive_check}, + {"pointer", !enable_pointer_check}, + {"undefined-shift", !enable_undefined_shift_check}}; + + const namespacet ns(goto_model.symbol_table); + + for(auto &entry : goto_model.goto_functions.function_map) + { + bool added_skip = false; + + for(auto &instruction : entry.second.body.instructions) + { + // TODO: we may have other code using __CPROVER_dead_object and therefore + // cannot easily remove these assignments +#if 0 + if( + instruction.is_assign() && !enable_pointer_check && + !enable_pointer_primitive_check && + instruction.assign_lhs().id() == ID_symbol && + to_symbol_expr(instruction.assign_lhs()).get_identifier() == + CPROVER_PREFIX "dead_object") + { + instruction.turn_into_skip(); + added_skip = true; + continue; + } + else +#endif + if(!instruction.is_assert()) + continue; + + const irep_idt &property_class = + instruction.source_location().get_property_class(); + auto entry_it = should_skip.find(property_class); + bool skip = entry_it != should_skip.end() && entry_it->second; + + if(!skip && property_class == "error label") + { + const std::string comment = + id2string(instruction.source_location().get_comment()); + skip = true; + for(const auto &l : error_labels) + { + if(comment == std::string("error label " + l)) + { + skip = false; + break; + } + } + } + else if(!skip && property_class == "overflow") + { + const std::string comment = + id2string(instruction.source_location().get_comment()); + if(has_prefix(comment, "result of signed mod is not representable")) + skip = !enable_signed_overflow_check; + else if(has_prefix(comment, "arithmetic overflow on ")) + { + const std::string op = comment.substr(23); + if(has_prefix(op, "floating-point ")) + skip = !enable_float_overflow_check; + else if( + has_prefix(op, "signed type ") || has_prefix(op, "float to ") || + has_prefix(op, "signed to ") || has_prefix(op, "unsigned to ")) + { + skip = !enable_conversion_check; + } + else if(has_prefix(op, "signed ")) + { + // TODO: some of these checks may also have been generated via + // enable_pointer_overflow_check + skip = !enable_signed_overflow_check; + } + else if(has_prefix(op, "unsigned ")) + { + // TODO: some of these checks may also have been generated via + // enable_pointer_overflow_check + skip = !enable_unsigned_overflow_check; + } + } + } + + if(skip) + { + instruction.turn_into_skip(); + added_skip = true; + } + else + { + if(enable_assert_to_assume) + instruction.turn_into_assume(); + + // TODO: the following would also simplify assertions not generated by + // goto_check_c +#if 0 + if(enable_simplify) + simplify(instruction.guard, ns); + + if(!retain_trivial && instruction.guard.is_true()) + { + instruction.turn_into_skip(); + added_skip = true; + } +#endif + } + } + + if(added_skip) + remove_skip(entry.second.body); + } +} diff --git a/src/goto-programs/goto_check.h b/src/goto-programs/goto_check.h index 91bbaedf264..4644d92bed6 100644 --- a/src/goto-programs/goto_check.h +++ b/src/goto-programs/goto_check.h @@ -30,4 +30,6 @@ void transform_assertions_assumptions( const optionst &options, goto_programt &goto_program); +void remove_disabled_checks(const optionst &, goto_modelt &); + #endif // CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H diff --git a/src/goto-programs/process_goto_program.cpp b/src/goto-programs/process_goto_program.cpp index bcde95f76f6..a2f8028634b 100644 --- a/src/goto-programs/process_goto_program.cpp +++ b/src/goto-programs/process_goto_program.cpp @@ -76,6 +76,7 @@ bool process_goto_program( // add generic checks log.status() << "Generic Property Instrumentation" << messaget::eom; goto_check_c(options, goto_model, log.get_message_handler()); + remove_disabled_checks(options, goto_model); transform_assertions_assumptions(options, goto_model); // checks don't know about adjusted float expressions