From 4ad3eab1e132aa027ba4d8ac07c975c9a7f80617 Mon Sep 17 00:00:00 2001 From: polgreen Date: Mon, 23 Oct 2017 17:09:57 +0200 Subject: [PATCH 1/2] make-function-assume-false command line option Blocks all paths through a function by replacing the function calls with assume_false. This is similar to --undefined-function-is-assume-false, but gives the flexibility to havoc undefined functions and block specific functions without needing multiple calls to goto-instrument. Needed for aggressive slicer work --- src/goto-instrument/Makefile | 1 + .../goto_instrument_parse_options.cpp | 11 +++ .../goto_instrument_parse_options.h | 1 + .../make_function_assume_false.cpp | 99 +++++++++++++++++++ .../make_function_assume_false.h | 32 ++++++ 5 files changed, 144 insertions(+) create mode 100644 src/goto-instrument/make_function_assume_false.cpp create mode 100644 src/goto-instrument/make_function_assume_false.h diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index da86474e7f1..87bf036786d 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -34,6 +34,7 @@ SRC = accelerate/accelerate.cpp \ interrupt.cpp \ k_induction.cpp \ loop_utils.cpp \ + make_function_assume_false.cpp \ mmio.cpp \ model_argc_argv.cpp \ nondet_static.cpp \ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 2218fd68235..f3823615de9 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -97,6 +97,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "model_argc_argv.h" #include "undefined_functions.h" #include "remove_function.h" +#include "make_function_assume_false.h" #include "splice_call.h" void goto_instrument_parse_optionst::eval_verbosity() @@ -939,6 +940,14 @@ void goto_instrument_parse_optionst::instrument_goto_program() get_message_handler()); } + if(cmdline.isset("make-function-assume-false")) + { + make_functions_assume_false( + goto_model, + cmdline.get_values("make-function-assume-false"), + get_message_handler()); + } + // we add the library in some cases, as some analyses benefit if(cmdline.isset("add-library") || @@ -1521,6 +1530,8 @@ void goto_instrument_parse_optionst::help() " --model-argc-argv model up to command line arguments\n" // NOLINTNEXTLINE(whitespace/line_length) " --remove-function-body remove the implementation of function (may be repeated)\n" + " --make-function-assume-false \n" + " replace calls to function with assume(false) (may be repeated)\n" // NOLINT(*) "\n" "Other options:\n" " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 04b3a8f7b2b..99387e57f2c 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -78,6 +78,7 @@ Author: Daniel Kroening, kroening@kroening.com "(show-threaded)(list-calls-args)(print-path-lengths)" \ "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ + "(make-function-assume-false):"\ "(splice-call):" \ diff --git a/src/goto-instrument/make_function_assume_false.cpp b/src/goto-instrument/make_function_assume_false.cpp new file mode 100644 index 00000000000..28360ca4133 --- /dev/null +++ b/src/goto-instrument/make_function_assume_false.cpp @@ -0,0 +1,99 @@ +/*******************************************************************\ + +Module: Make function assume false + +Author: Elizabeth Polgreen + +Date: November 2017 + +\*******************************************************************/ + +/// \file +/// Make function assume false + +#include "make_function_assume_false.h" + +#include + +#include + +/// \brief Replace calls to the function with assume(false). +/// This effectively blocks any paths through the function +/// or depending on return values from the function. +/// \param goto_model input program to be modifier +/// \param identifier name of function to block +/// \param message_handler Error/status output +void make_function_assume_false( + goto_modelt &goto_model, + const irep_idt &identifier, + message_handlert &message_handler) +{ + messaget message(message_handler); + + goto_functionst::function_mapt::iterator entry = + goto_model.goto_functions.function_map.find(identifier); + + if(entry==goto_model.goto_functions.function_map.end()) + { + message.error() << "No function " << identifier + << " in goto program" << messaget::eom; + return; + } + else if(entry->second.is_inlined()) + { + message.warning() << "Function " << identifier << " is inlined, " + << "instantiations will not be blocked" + << messaget::eom; + } + else + { + message.status() << "Blocking all calls to " << identifier << messaget::eom; + + Forall_goto_functions(it, goto_model.goto_functions) + { + Forall_goto_program_instructions(iit, it->second.body) + { + goto_programt::instructiont &ins = *iit; + + if(!ins.is_function_call()) + continue; + + const code_function_callt &call = to_code_function_call(ins.code); + + if(call.function().id() != ID_symbol) + continue; + + if(to_symbol_expr(call.function()).get_identifier() == identifier) + { + ins.make_assumption(false_exprt()); + ins.source_location.set_comment( + "`"+id2string(identifier)+"'" + " is marked unusable by --make-function-assume-false"); + } + } + } + } +} + +/// \brief Replace calls to any functions in the list +/// "functions" with assume(false). +/// This effectively blocks any paths through the function +/// or depending on return values from the function. +/// \param functions list of function names to block +/// \param goto_model input program to be modifier +/// \param message_handler Error/status output +void make_functions_assume_false( + goto_modelt &goto_model, + const std::list &functions, + message_handlert &message_handler) +{ + messaget message(message_handler); + for(const auto &func : functions) + { + make_function_assume_false(goto_model, func, message_handler); + } +} + + + + diff --git a/src/goto-instrument/make_function_assume_false.h b/src/goto-instrument/make_function_assume_false.h new file mode 100644 index 00000000000..a7f81029b84 --- /dev/null +++ b/src/goto-instrument/make_function_assume_false.h @@ -0,0 +1,32 @@ +/*******************************************************************\ + +Module: Make function assume false + +Author: Elizabeth Polgreen + +Date: November 2017 + +\*******************************************************************/ + +/// \file +/// Make function assume false + +#ifndef CPROVER_GOTO_INSTRUMENT_MAKE_FUNCTION_ASSUME_FALSE_H +#define CPROVER_GOTO_INSTRUMENT_MAKE_FUNCTION_ASSUME_FALSE_H + +#include +#include + +#include + +class goto_modelt; +class message_handlert; + +void make_functions_assume_false( + goto_modelt &, + const std::list &names, + message_handlert &); + + + +#endif /* CPROVER_GOTO_INSTRUMENT_MAKE_FUNCTION_ASSUME_FALSE_H */ From 7d80a525a622c5ceee758e87772adb659dc1b2bb Mon Sep 17 00:00:00 2001 From: polgreen Date: Tue, 21 Nov 2017 11:26:48 +0000 Subject: [PATCH 2/2] Regression tests for make-function-assume-false --- .../make_function_assume_false1/main.c | 10 ++++++++++ .../make_function_assume_false1/test.desc | 8 ++++++++ .../make_function_assume_false2/main.c | 13 +++++++++++++ .../make_function_assume_false2/test.desc | 8 ++++++++ .../make_function_assume_false3/main.c | 13 +++++++++++++ .../make_function_assume_false3/test.desc | 8 ++++++++ 6 files changed, 60 insertions(+) create mode 100644 regression/goto-instrument/make_function_assume_false1/main.c create mode 100644 regression/goto-instrument/make_function_assume_false1/test.desc create mode 100644 regression/goto-instrument/make_function_assume_false2/main.c create mode 100644 regression/goto-instrument/make_function_assume_false2/test.desc create mode 100644 regression/goto-instrument/make_function_assume_false3/main.c create mode 100644 regression/goto-instrument/make_function_assume_false3/test.desc diff --git a/regression/goto-instrument/make_function_assume_false1/main.c b/regression/goto-instrument/make_function_assume_false1/main.c new file mode 100644 index 00000000000..76fcdaca5e2 --- /dev/null +++ b/regression/goto-instrument/make_function_assume_false1/main.c @@ -0,0 +1,10 @@ +void function_a() +{ + __CPROVER_assert(0,""); +} + +int main() +{ + function_a(); + return 0; +} diff --git a/regression/goto-instrument/make_function_assume_false1/test.desc b/regression/goto-instrument/make_function_assume_false1/test.desc new file mode 100644 index 00000000000..7937fc40e63 --- /dev/null +++ b/regression/goto-instrument/make_function_assume_false1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--make-function-assume-false function_a +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring \ No newline at end of file diff --git a/regression/goto-instrument/make_function_assume_false2/main.c b/regression/goto-instrument/make_function_assume_false2/main.c new file mode 100644 index 00000000000..b47c72f687f --- /dev/null +++ b/regression/goto-instrument/make_function_assume_false2/main.c @@ -0,0 +1,13 @@ +void function_a(int *num) +{ + *num = *num+1; +} + +int main() +{ + int b=0; + int c; + if(c) + function_a(&b); + __CPROVER_assert(b==0, ""); +} \ No newline at end of file diff --git a/regression/goto-instrument/make_function_assume_false2/test.desc b/regression/goto-instrument/make_function_assume_false2/test.desc new file mode 100644 index 00000000000..bd3ffe687ee --- /dev/null +++ b/regression/goto-instrument/make_function_assume_false2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--make-function-assume-false function_a +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/make_function_assume_false3/main.c b/regression/goto-instrument/make_function_assume_false3/main.c new file mode 100644 index 00000000000..431372ab0b9 --- /dev/null +++ b/regression/goto-instrument/make_function_assume_false3/main.c @@ -0,0 +1,13 @@ +void function_a(int *num) +{ + *num = *num+1; +} + +int main() +{ + int b=0; + int c; + if(c) + function_a(&b); + __CPROVER_assert(b!=0, ""); +} \ No newline at end of file diff --git a/regression/goto-instrument/make_function_assume_false3/test.desc b/regression/goto-instrument/make_function_assume_false3/test.desc new file mode 100644 index 00000000000..b5f4b1d667b --- /dev/null +++ b/regression/goto-instrument/make_function_assume_false3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--make-function-assume-false function_a +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring