diff --git a/doc/cprover-manual/goto-analyzer.md b/doc/cprover-manual/goto-analyzer.md index f5a84207e76..c3fadcb1ffd 100644 --- a/doc/cprover-manual/goto-analyzer.md +++ b/doc/cprover-manual/goto-analyzer.md @@ -49,16 +49,21 @@ goto-analyzer --verify --three-way-merge --vsd --vsd-values set-of-constants -- I want to discharge obvious conditions and remove unreachable code: ``` -goto-analyzer --simplify out.gb --three-way-merge --vsd +goto-analyzer --simplify out.gb --three-way-merge --vsd program.c ``` I want to build a dependency graph: ``` -goto-analyzer --show --dot depgraph.dot --dependence-graph-vs +goto-analyzer --show --dot depgraph.dot --dependence-graph-vs program.c ``` +I want to generate code contracts: +``` +goto-analyzer --instrument out.gb --instrument-targets requires,ensures,function_start,function_end,backwards_goto_target --vsd --verbosity 9 program.c +``` + ## Task @@ -106,6 +111,45 @@ domain which can result in a second (or more) runs giving simplification. Submitting bug reports for these is helpful but they may not be viable to fix. +`--instrument output_file.gb` +: Produces a new version of the GOTO binary in which +the abstract domains have been used to insert annotations, such as assertios +or assumptions. If everything is working correctly these should always +be true because they are implied by the program and are an overapproximation. +However they can be useful for a number of reasons. Assertions can be +used to test the results of goto-analyze against another tool. +Assumptions can be useful as auxilliary constraints to help other +tools or to provide better approximations of parts of the program. +The exact instrumentation depends on the domain. + +`--instrument-targets` +: A comma separated list of where in the program instrumentation should +be added and what kind of instrumentation should be inserted. +Available locations are `function_start`, `function_end`, `function_call` +(before function calls), `function_return` (after function calls), +`any_goto_target`, `backwards_goto_target`, `after_goto_not_taken`, +`requires` and `ensures`. If just the locations is used, assumptions +will be inserted apart from requires and assumes which add the +corresponding code contracts. If the location is given followed by +`=assume`, `=assert` or `=nothing` then assumptions, assertions or +nothing is inserted. A little care is necessary when using contracts +generated by `goto-analyzer`. The `requires` contract is an +over-approximations of the calling context in the analyzed program. +So if the function has flags (read, write, append, etc.) but only one +set is used in the program then the `requires` contract may well +include that specific set of flags. In that sense what is generated +is an over-approximation (i.e. a weakening or less restrictive +version) of the strongest pre-condition that would work for the +program you have analysed. In practice you may want to weaken it +further so your verification results are more general. Likewise the +`ensures` contract is an over-approximation of what the function does +in the analyzed program. If part of the functionality of the function +is not used then it may not be in the generated contract. In the +example of flags above, if the program only uses one set of flags, the +`ensures` contract may not include changes that are possible using +other sets of flags. Again, it may be desirable to weaken the +generated contract so it can be used more generally. + `--unreachable-instructions` : Lists which instructions have a domain which is bottom (i.e. unreachable). If `--function` has been used to set the program diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1 index bfa40f426f7..2b0c70c3193 100644 --- a/doc/man/goto-analyzer.1 +++ b/doc/man/goto-analyzer.1 @@ -103,6 +103,28 @@ may not be viable to fix. Do not remove instructions from which no property can be reached (use with \fB\-\-simplify\fR). .TP +\fB\-\-instrument\fR \fIfile_name\fR +Writes a new version of the input program to \fIfile_name\fR in which +the abstract domains have been used to insert annotations, such as assertios +or assumptions. If everything is working correctly these should always +be true because they are implied by the program and are an overapproximation. +However they can be useful for a number of reasons. Assertions can be +used to test the results of goto-analyze against another tool. +Assumptions can be useful as auxilliary constraints to help other +tools or to provide better approximations of parts of the program. +The exact instrumentation depends on the domain. +.TP +\fB\-\-instrument\-targets\fR +A comma separated list of where in the program instrumentation should +be added and what kind of instrumentation should be inserted. +Available locations are function_start, function_end, function_call +(before function calls), function_return (after function calls), +any_goto_target, backwards_goto_target, after_goto_not_taken, requires +and ensures. If just the locations is used, assumptions will be +inserted apart from requires and assumes which add the corresponding +code contracts. If the location is given followed by =assume, =assert or +=nothing then assumptions, assertions or nothing is inserted. +.TP \fB\-\-unreachable\-instructions\fR Lists which instructions have a domain which is bottom (i.e. unreachable). If \fB\-\-function\fR has been used to set the program diff --git a/regression/goto-analyzer/instrument-basic/after_goto_not_taken.desc b/regression/goto-analyzer/instrument-basic/after_goto_not_taken.desc new file mode 100644 index 00000000000..47a91d5c510 --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/after_goto_not_taken.desc @@ -0,0 +1,14 @@ +CORE +main.c +--instrument out.gb --instrument-targets after_goto_not_taken --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting example_function\nInstruction \d+ because after_goto_not_taken... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$ +-- +^warning: ignoring +-- +Testing instrumenting at after gotos that are not taken (i.e. the "other" branch that is not a goto_target) + + + diff --git a/regression/goto-analyzer/instrument-basic/any_goto_target.desc b/regression/goto-analyzer/instrument-basic/any_goto_target.desc new file mode 100644 index 00000000000..4764d6ff748 --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/any_goto_target.desc @@ -0,0 +1,13 @@ +CORE +main.c +--instrument out.gb --instrument-targets any_goto_target --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting example_function\nInstruction \d+ because any_goto_target... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption\nInstruction \d+ because any_goto_target... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1 ∧ \(10 ≤ example_function::1::1::i ∧ example_function::1::1::i ≤ max_value\)... added as assumption$ +-- +^warning: ignoring +-- +Testing instrumenting at goto targets + + diff --git a/regression/goto-analyzer/instrument-basic/assertions.desc b/regression/goto-analyzer/instrument-basic/assertions.desc new file mode 100644 index 00000000000..aceef5b2639 --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/assertions.desc @@ -0,0 +1,14 @@ +CORE +main.c +--instrument out.gb --instrument-targets function_call=assert,function_start=assume,function_end=assert,function_return=assume --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting main\nInstruction \d+ because function_return... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption\nInstruction \d+ because function_end... single history... condition is main#return_value = 0 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assertion\nInstruction \d+ because function_start... single history... condition is true_from_calling_context = 0 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption\nInstruction \d+ because function_call... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assertion$ +^Instrumenting example_function\nInstruction \d+ because function_end... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assertion\nInstruction \d+ because function_start... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$ +-- +^warning: ignoring +-- +Testing the addition of assertions in a way that mimics the use of contracts + + diff --git a/regression/goto-analyzer/instrument-basic/backwards_goto_target.desc b/regression/goto-analyzer/instrument-basic/backwards_goto_target.desc new file mode 100644 index 00000000000..fe8004ec2a5 --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/backwards_goto_target.desc @@ -0,0 +1,13 @@ +CORE +main.c +--instrument out.gb --instrument-targets backwards_goto_target --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting example_function\nInstruction \d+ because backwards_goto_target... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$ +-- +^warning: ignoring +-- +Testing instrumenting at backwards goto targets + + diff --git a/regression/goto-analyzer/instrument-basic/default.desc b/regression/goto-analyzer/instrument-basic/default.desc new file mode 100644 index 00000000000..425935f3aaa --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/default.desc @@ -0,0 +1,13 @@ +CORE +main.c +--instrument out.gb --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting main\nInstruction \d+ because function_start... single history... condition is true_from_calling_context = 0 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption\nInstruction \d+ because function_return... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$ +^Instrumenting example_function\nInstruction \d+ because function_start... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption\nInstruction \d+ because backwards_goto_target... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$ +-- +^warning: ignoring +-- +Testing the default options of instrumentation with goto-analyze + diff --git a/regression/goto-analyzer/instrument-basic/ensures.desc b/regression/goto-analyzer/instrument-basic/ensures.desc new file mode 100644 index 00000000000..a97588ecfc2 --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/ensures.desc @@ -0,0 +1,12 @@ +CORE +main.c +--instrument out.gb --instrument-targets ensures --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting example_function\nAdd ensures contract... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as contract$ +-- +^warning: ignoring +-- +Testing instrumenting add ensures contract + diff --git a/regression/goto-analyzer/instrument-basic/function_call.desc b/regression/goto-analyzer/instrument-basic/function_call.desc new file mode 100644 index 00000000000..a8e0b60c51e --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/function_call.desc @@ -0,0 +1,13 @@ +CORE +main.c +--instrument out.gb --instrument-targets function_call --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting main\nInstruction \d+ because function_call... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$ +-- +^warning: ignoring +-- +Testing instrumenting at function call + + diff --git a/regression/goto-analyzer/instrument-basic/function_end.desc b/regression/goto-analyzer/instrument-basic/function_end.desc new file mode 100644 index 00000000000..13c82059cbd --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/function_end.desc @@ -0,0 +1,14 @@ +CORE +main.c +--instrument out.gb --instrument-targets function_end --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting main\nInstruction \d+ because function_end... single history... condition is main#return_value = 0 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$ +^Instrumenting example_function\nInstruction \d+ because function_end... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$ +-- +^warning: ignoring +-- +Testing instrumenting at the function end + + diff --git a/regression/goto-analyzer/instrument-basic/function_return.desc b/regression/goto-analyzer/instrument-basic/function_return.desc new file mode 100644 index 00000000000..c82548fd455 --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/function_return.desc @@ -0,0 +1,13 @@ +CORE +main.c +--instrument out.gb --instrument-targets function_return --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting main\nInstruction \d+ because function_return... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$ +-- +^warning: ignoring +-- +Testing instrumenting at function return + + diff --git a/regression/goto-analyzer/instrument-basic/function_start.desc b/regression/goto-analyzer/instrument-basic/function_start.desc new file mode 100644 index 00000000000..3e7bacc4ffb --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/function_start.desc @@ -0,0 +1,14 @@ +CORE +main.c +--instrument out.gb --instrument-targets function_start --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting main\nInstruction \d+ because function_start... single history... condition is true_from_calling_context = 0 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$ +^Instrumenting example_function\nInstruction \d+ because function_start... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$ +-- +^warning: ignoring +-- +Testing instrumenting at the function start + + diff --git a/regression/goto-analyzer/instrument-basic/main.c b/regression/goto-analyzer/instrument-basic/main.c new file mode 100644 index 00000000000..b4a5655f29c --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/main.c @@ -0,0 +1,29 @@ +int true_from_calling_context = 0; + +int example_function(int argument) +{ + int local = argument + 1; + int location = 1; + + for(int i = 0; i < 10; ++i) + { + location = 2; + ++local; + } + + location = 3; + ++local; + + return location + local; +} + +int main(int argc, char **argv) +{ + true_from_calling_context = 1; + + int argument_input = 1; + + int ret = example_function(argument_input); + + return 0; +} diff --git a/regression/goto-analyzer/instrument-basic/requires.desc b/regression/goto-analyzer/instrument-basic/requires.desc new file mode 100644 index 00000000000..9af91e22a72 --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/requires.desc @@ -0,0 +1,14 @@ +CORE +main.c +--instrument out.gb --instrument-targets requires --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting example_function\nAdd requires contract... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as contract$ +-- +^warning: ignoring +-- +Testing instrumenting add requires contract + + + diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index f5bc1488934..5d172ec5269 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -5,6 +5,7 @@ SRC = goto_analyzer_languages.cpp \ taint_parser.cpp \ unreachable_instructions.cpp \ show_on_source.cpp \ + static_instrument.cpp \ static_show_domain.cpp \ static_simplifier.cpp \ static_verifier.cpp \ diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index b64119b6b9e..351070ca7d5 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -34,6 +34,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "build_analyzer.h" #include "show_on_source.h" +#include "static_instrument.h" #include "static_show_domain.h" #include "static_simplifier.h" #include "static_verifier.h" @@ -160,6 +161,18 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) "simplify-slicing", !(cmdline.isset("no-simplify-slicing"))); } + else if(cmdline.isset("instrument")) + { + if(cmdline.get_value("instrument") == "-") + throw invalid_command_line_argument_exceptiont( + "cannot output goto binary to stdout", "--instrument"); + + options.set_option("instrument", true); + options.set_option("outfile", cmdline.get_value("instrument")); + options.set_option("general-analysis", true); + options.set_option( + "instrument-targets", cmdline.get_value("instrument-targets")); + } else if(cmdline.isset("show-intervals")) { // For backwards compatibility @@ -623,6 +636,34 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) result = static_simplifier( goto_model, *analyzer, options, ui_message_handler, out); } + else if(options.get_bool_option("instrument")) + { + PRECONDITION(!outfile.empty() && outfile != "-"); + output_stream.close(); + output_stream.open(outfile, std::ios::binary); + if( + options.is_set("instrument-targets") && + options.get_option("instrument-targets") != "") + { + result = static_instrument( + goto_model, + *analyzer, + options.get_option("instrument-targets"), + ui_message_handler, + out); + } + else + { + // A reasonably sane set of defaults + result = static_instrument( + goto_model, + *analyzer, + "function_start=assume,function_return=assume,backwards_goto_target=" + "assume", + ui_message_handler, + out); + } + } else if(options.get_bool_option("unreachable-instructions")) { result = static_unreachable_instructions(goto_model, @@ -705,6 +746,8 @@ void goto_analyzer_parse_optionst::help() " program\n" " {y--no-simplify-slicing} \t do not remove instructions from which no" " property can be reached (use with {y--simplify})\n" + " {y--instrument} {ufile_name} \t use the abstract domains to generate annotations\n" + " {y--instrument-targets} {ulist} \t where to annotate and what annotations to use\n" " {y--unreachable-instructions} \t list dead code\n" " {y--unreachable-functions} \t list functions unreachable from the entry" " point\n" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index beda0d3a2d3..1b40ba1c21b 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -108,9 +108,14 @@ class optionst; #define GOTO_ANALYSER_OPTIONS_TASKS \ "(show)(verify)(simplify):" \ "(show-on-source)" \ + "(instrument):" \ "(unreachable-instructions)(unreachable-functions)" \ "(reachable-functions)" +#define GOTO_ANALYZER_OPTIONS_TASKS_CONFIG \ + "(no-simplify-slicing)" \ + "(instrument-targets):" \ + #define GOTO_ANALYSER_OPTIONS_AI \ "(recursive-interprocedural)" \ "(three-way-merge)" \ @@ -158,7 +163,7 @@ class optionst; OPT_TIMESTAMP \ OPT_VALIDATE \ GOTO_ANALYSER_OPTIONS_TASKS \ - "(no-simplify-slicing)" \ + GOTO_ANALYZER_OPTIONS_TASKS_CONFIG \ "(show-intervals)(show-non-null)" \ GOTO_ANALYSER_OPTIONS_AI \ "(location-sensitive)(concurrent)" \ diff --git a/src/goto-analyzer/static_instrument.cpp b/src/goto-analyzer/static_instrument.cpp new file mode 100644 index 00000000000..5c47a259904 --- /dev/null +++ b/src/goto-analyzer/static_instrument.cpp @@ -0,0 +1,461 @@ +/*******************************************************************\ + +Module: goto-analyzer + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#include "static_instrument.h" + +#include +#include +#include +#include +#include +#include +#include + +#include +#include +#include +#include + +#include + +#include + +static std::string s_function_start = "function_start"; +static std::string s_function_end = "function_end"; +static std::string s_function_call = "function_call"; +static std::string s_function_return = "function_return"; +static std::string s_any_goto_target = "any_goto_target"; +static std::string s_backwards_goto_target = "backwards_goto_target"; +static std::string s_after_goto_not_taken = "after_goto_not_taken"; + +// Build a configuration from user strings +instrument_configt::instrument_configt(const std::string &opts) +{ + // Initialise everything to the defaults + function_start = instrument_actiont::NOTHING; + function_end = instrument_actiont::NOTHING; + function_call = instrument_actiont::NOTHING; + function_return = instrument_actiont::NOTHING; + any_goto_target = instrument_actiont::NOTHING; + backwards_goto_target = instrument_actiont::NOTHING; + after_goto_not_taken = instrument_actiont::NOTHING; + requires = false; + ensures = false; + + if(opts == "") + { + return; + } + + // A helper struct + struct config_targett + { + const std::string &name; + instrument_actiont *target; + + config_targett(const std::string &n, instrument_actiont *t) + : name(n), target(t) + { + } + }; + + std::vector options; + options.push_back(config_targett(s_function_start, &(this->function_start))); + options.push_back(config_targett(s_function_end, &(this->function_end))); + options.push_back(config_targett(s_function_call, &(this->function_call))); + options.push_back( + config_targett(s_function_return, &(this->function_return))); + options.push_back( + config_targett(s_any_goto_target, &(this->any_goto_target))); + options.push_back( + config_targett(s_backwards_goto_target, &(this->backwards_goto_target))); + options.push_back( + config_targett(s_after_goto_not_taken, &(this->after_goto_not_taken))); + + auto const config_strings = split_string(opts, ','); + for(auto const &config_string : config_strings) + { + instrument_actiont *target = NULL; + std::string remainder = ""; + + for(auto const &option : options) + { + if(config_string.substr(0, option.name.length()) == option.name) + { + target = option.target; + remainder = config_string.substr(option.name.length()); + break; + } + } + + if(target == NULL) + { + if(config_string == "requires") + { + requires = true; + } + else if(config_string == "ensures") + { + ensures = true; + } + else + { + throw invalid_command_line_argument_exceptiont( + "Unrecognised instrument option: " + config_string, opts); + } + } + else + { + if((remainder == "") || (remainder == "=assume")) + *target = instrument_actiont::ASSUME; + else if(remainder == "=assert") + *target = instrument_actiont::ASSERT; + else if(remainder == "=nothing") + *target = instrument_actiont::NOTHING; + else + { + throw invalid_command_line_argument_exceptiont( + "Unrecognised instrument action: " + remainder, opts); + } + } + } +} + +typedef std::map< + goto_programt::targett, + std::pair, + goto_programt::target_less_than> + instrument_locationst; + +static instrument_locationst get_instrumentation_locations( + goto_programt &gp, + const instrument_configt &config) +{ + instrument_locationst targets; + + goto_programt::targett prev_it = gp.instructions.begin(); + Forall_goto_program_instructions(i_it, gp) + { + instrument_actiont action = instrument_actiont::NOTHING; + std::string *reason; + + if(i_it == gp.instructions.begin()) + { + action = config.function_start; + reason = &s_function_start; + } + else if(i_it->is_end_function()) + { + action = config.function_end; + reason = &s_function_end; + } + else if(i_it->is_function_call()) + { + action = config.function_call; + reason = &s_function_call; + } + else if(prev_it->is_function_call()) + { + action = config.function_return; + reason = &s_function_return; + } + else if(i_it->is_target()) + { + action = config.any_goto_target; + reason = &s_any_goto_target; + + // Choices for backwards_goto override any_goto if present + if(config.backwards_goto_target != instrument_actiont::NOTHING) + { + for(auto const incoming_it : i_it->incoming_edges) + { + if(incoming_it->is_backwards_goto()) + { + action = config.backwards_goto_target; + reason = &s_backwards_goto_target; + break; // inner! + } + } + } + } + else if(prev_it->is_goto() && !prev_it->condition().is_true()) + { + action = config.after_goto_not_taken; + reason = &s_after_goto_not_taken; + } + + if(action != instrument_actiont::NOTHING) + { + targets.emplace(i_it, std::make_pair(action, reason)); + } + + // This bit is vital! + prev_it = i_it; + } + + return targets; +} + +static exprt compute_instrumentation_expression( + goto_programt::targett i_it, + const ai_baset &ai, + const namespacet &ns, + const std::set &relevant_expressions, + messaget &m) +{ + // Multiple histories are handled as disjunctions + exprt::operandst inst; + + const auto trace_set_pointer = + ai.abstract_traces_before(i_it); // Keep a pointer so refcount > 0 + const auto &trace_set = *trace_set_pointer; + + if(trace_set.size() == 0) // i.e. unreachable + { + m.progress() << "unreachable... "; // No EOM yet + + inst.push_back(false_exprt{}); + } + else if(trace_set.size() == 1) + { + auto dp = ai.abstract_state_before(i_it); + + m.progress() << "single history... "; // No EOM yet + + inst.push_back(dp->to_predicate(relevant_expressions, ns)); + } + else + { + m.progress() << "multiple histories... "; // No EOM yet + + for(const auto &trace_ptr : trace_set) + { + auto dp = ai.abstract_state_before(trace_ptr); + inst.push_back(dp->to_predicate(relevant_expressions, ns)); + } + } + + return disjunction(inst); +} + +static void +get_globals(std::set &relevant_expressions, const namespacet &ns) +{ + system_library_symbolst lib; + std::set out; // Unused + + for(const auto &symbol_pair : ns.get_symbol_table().symbols) + { + const symbolt &symbol = symbol_pair.second; + auto name_string = id2string(symbol.name); + if( + symbol.is_lvalue && symbol.is_static_lifetime && + !lib.is_symbol_internal_symbol(symbol, out)) + { + relevant_expressions.insert(symbol_exprt(symbol.name, symbol.type)); + } + } + return; +} + +static void get_locals( + std::set &relevant_expressions, + const goto_programt &goto_program, + const namespacet &ns) +{ + goto_programt::decl_identifierst locals; + goto_program.get_decl_identifiers(locals); + for(const auto &identifier : locals) + { + const symbolt &symbol = ns.lookup(identifier); + relevant_expressions.insert(symbol_exprt(identifier, symbol.type)); + } + return; +} + +static void get_arguments( + std::set &relevant_expressions, + const irep_idt function_name, + const namespacet &ns) +{ + const symbolt &symbol = ns.lookup(function_name); + const code_typet &type = to_code_type(symbol.type); + + for(const auto ¶m : type.parameters()) + { + relevant_expressions.insert( + symbol_exprt(param.get_identifier(), param.type())); + } + return; +} + +static void static_instrument_goto_program( + const irep_idt function_name, + goto_programt &goto_program, + symbol_tablet &symbol_table, + const namespacet &ns, + const ai_baset &ai, + const instrument_configt &config, + message_handlert &message_handler) +{ + // Get the locations to instrument + auto targets = get_instrumentation_locations(goto_program, config); + + // The state may contain information about variables from other + // scopes, such as the caller which are true but putting them into + // instrumentation can cause problems. So gather the local + // variables. + std::set relevant_expressions; + get_globals(relevant_expressions, ns); + get_locals(relevant_expressions, goto_program, ns); + get_arguments(relevant_expressions, function_name, ns); + // TODO : for pointer variables p, add *p? + // TODO : rename whatever#return to __CPROVER_return_value + + // For each of them + for(const auto &t : targets) + { + goto_programt::targett i_it = t.first; + instrument_actiont action = t.second.first; + const std::string &reason = *(t.second.second); + + messaget m(message_handler); + m.status() << "Instruction " << i_it->location_number << " because " + << reason << "... "; // No EOM + + // Generate the expression + exprt instrument_expression = + compute_instrumentation_expression(i_it, ai, ns, relevant_expressions, m); + m.status() << "condition is " << format(instrument_expression) + << "... "; // No EOM + + // Insert it! + goto_programt::targett current = i_it; + goto_program.insert_before_swap(i_it); + + if(action == instrument_actiont::ASSUME) + { + *current = goto_programt::make_assumption(instrument_expression); + m.progress() << "added as assumption" << messaget::eom; + } + else if(action == instrument_actiont::ASSERT) + { + *current = goto_programt::make_assertion(instrument_expression); + m.progress() << "added as assertion" << messaget::eom; + } + else + { + UNREACHABLE; + } + current->source_location_nonconst() = i_it->source_location(); + } + + if(config.requires || config.ensures) + { + messaget m(message_handler); + + symbolt *symbol = symbol_table.get_writeable(function_name); + auto code = to_code_with_contract_type(symbol->type); + + if(config.requires) + { + m.status() << "Add requires contract... "; + exprt instrument_expression = compute_instrumentation_expression( + goto_program.instructions.begin(), ai, ns, relevant_expressions, m); + m.status() << "condition is " << format(instrument_expression) + << "... "; // No EOM + + code.c_requires().push_back(instrument_expression); + m.progress() << "added as contract" << messaget::eom; + } + if(config.ensures) + { + m.status() << "Add ensures contract... "; + auto i_it = goto_program.instructions.end(); + --i_it; + exprt instrument_expression = compute_instrumentation_expression( + i_it, ai, ns, relevant_expressions, m); + m.status() << "condition is " << format(instrument_expression) + << "... "; // No EOM + + code.c_requires().push_back(instrument_expression); + m.progress() << "added as contract" << messaget::eom; + } + + // Write back the annotated type + symbol->type = code; + } + + goto_program.update(); // Make sure the references are correct. + return; +} + +void static_instrument_goto_model( + goto_modelt &goto_model, + const ai_baset &ai, + const instrument_configt &config, + message_handlert &message_handler) +{ + messaget m(message_handler); + m.status() << "Instrumenting goto_model" << messaget::eom; + + const namespacet ns(goto_model.symbol_table); + + for(auto &gf_entry : goto_model.goto_functions.function_map) + { + if(!gf_entry.second.body_available()) + { + m.progress() << "Not instrumenting " << gf_entry.first + << " because it has no body" << messaget::eom; + } + else + { + m.progress() << "Instrumenting " << gf_entry.first << messaget::eom; + + static_instrument_goto_program( + gf_entry.first, + gf_entry.second.body, + goto_model.symbol_table, + ns, + ai, + config, + message_handler); + } + } + + return; +} + +/// Uses the domain to_predicate method to generate ASSUMEs or ASSERTs. +/// \param goto_model: the program analyzed +/// \param ai: the abstract interpreter after it has been run to fix point +/// \param options: the parsed user options +/// \param message_handler: the system message handler +/// \param out: output stream for the instrumented program +/// \return false on success with the instrumented program to out +bool static_instrument( + goto_modelt &goto_model, + const ai_baset &ai, + const std::string &configuration_string, + message_handlert &message_handler, + std::ostream &out) +{ + instrument_configt config(configuration_string); + + static_instrument_goto_model(goto_model, ai, config, message_handler); + + messaget m(message_handler); + m.status() << "Writing goto binary" << messaget::eom; + + restore_returns(goto_model); // restore return types before writing the binary + goto_model.goto_functions.update(); // Make sure the references are correct. + + namespacet ns(goto_model.symbol_table); + return write_goto_binary( + out, ns.get_symbol_table(), goto_model.goto_functions); +} diff --git a/src/goto-analyzer/static_instrument.h b/src/goto-analyzer/static_instrument.h new file mode 100644 index 00000000000..86a918ec754 --- /dev/null +++ b/src/goto-analyzer/static_instrument.h @@ -0,0 +1,73 @@ +/*******************************************************************\ + +Module: goto-analyzer + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_ANALYZER_STATIC_INSTRUMENT_H +#define CPROVER_GOTO_ANALYZER_STATIC_INSTRUMENT_H + +#include + +// What kind of instrumentation to add +enum class instrument_actiont +{ + NOTHING, + ASSERT, + ASSUME +}; + +// What kind of instrumentation to add at each location +struct instrument_configt +{ +public: + instrument_actiont function_start; + instrument_actiont function_end; + instrument_actiont function_call; + instrument_actiont function_return; + instrument_actiont any_goto_target; + instrument_actiont backwards_goto_target; + instrument_actiont after_goto_not_taken; + bool requires; + bool ensures; + + instrument_configt() + : function_start(instrument_actiont::NOTHING), + function_end(instrument_actiont::NOTHING), + function_call(instrument_actiont::NOTHING), + function_return(instrument_actiont::NOTHING), + any_goto_target(instrument_actiont::NOTHING), + backwards_goto_target(instrument_actiont::NOTHING), + after_goto_not_taken(instrument_actiont::NOTHING), + requires(false), + ensures(false) + { + } + + // Parse from an option string + explicit instrument_configt(const std::string &opts); +}; + +class ai_baset; +class goto_modelt; +class message_handlert; +class optionst; + +// For using this functionality in other tools +void static_instrument_goto_model( + goto_modelt &, + const ai_baset &, + const instrument_configt &, + message_handlert &); + +// As used in goto-analyze +bool static_instrument( + goto_modelt &, + const ai_baset &, + const std::string &configuration_string, + message_handlert &, + std::ostream &); + +#endif // CPROVER_GOTO_ANALYZER_STATIC_INSTRUMENT_H