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 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 */