From 3a500c7024826d6f44d3d5db27b86d9e208c02a2 Mon Sep 17 00:00:00 2001 From: martin Date: Thu, 27 Aug 2020 23:36:42 +0100 Subject: [PATCH] Create an example abstract domain and use in goto-analyzer The domain simply prints out what calls are made to the key interfaces and nothing else. It is intended as a skeleton for people to experiment. --- doc/cprover-manual/goto-analyzer.md | 2 + doc/man/goto-analyzer.1 | 3 + regression/goto-analyzer/example-01/main.c | 20 ++ regression/goto-analyzer/example-01/test.desc | 13 ++ src/analyses/Makefile | 1 + src/analyses/example_domain.cpp | 193 ++++++++++++++++++ src/analyses/example_domain.h | 70 +++++++ src/goto-analyzer/build_analyzer.cpp | 18 ++ .../goto_analyzer_parse_options.cpp | 10 + .../goto_analyzer_parse_options.h | 1 + 10 files changed, 331 insertions(+) create mode 100644 regression/goto-analyzer/example-01/main.c create mode 100644 regression/goto-analyzer/example-01/test.desc create mode 100644 src/analyses/example_domain.cpp create mode 100644 src/analyses/example_domain.h diff --git a/doc/cprover-manual/goto-analyzer.md b/doc/cprover-manual/goto-analyzer.md index f5a84207e76..81e2b2a13b6 100644 --- a/doc/cprover-manual/goto-analyzer.md +++ b/doc/cprover-manual/goto-analyzer.md @@ -236,6 +236,8 @@ the foundational pointer and reaching definitions analysis. This means it can be configured using the VSD options and give more precise analysis (for example, field aware) of the dependencies. +`--example` +: Documentation of the domain goes here. ### Configuration of the Variable Sensitivity Domain diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1 index bfa40f426f7..d1ab6c6653f 100644 --- a/doc/man/goto-analyzer.1 +++ b/doc/man/goto-analyzer.1 @@ -254,6 +254,9 @@ the foundational pointer and reaching definitions analysis. This means it can be configured using the VSD options and give more precise analysis (for example, field aware) of the dependencies. .TP +\fB\-\-exampleR +Documentation of the domain goes here. +.TP \fB\-\-constants\fR The default option, this stores one constant value per variable. This means it is fast but will only find things that can be resolved by constant propagation. diff --git a/regression/goto-analyzer/example-01/main.c b/regression/goto-analyzer/example-01/main.c new file mode 100644 index 00000000000..64e37ae74e9 --- /dev/null +++ b/regression/goto-analyzer/example-01/main.c @@ -0,0 +1,20 @@ +#include + +int nondet_int(void); + +int main(int argc, char **argv) +{ + int x = nondet_int(); + int y = nondet_int(); + int z = nondet_int(); + + if(0) + { + __CPROVER_assert(0, "Should be unreachable"); + } + + __CPROVER_assert(1, "Always true"); + __CPROVER_assert(x < y, "Sometimes true, sometimes false"); + + return 0; +} diff --git a/regression/goto-analyzer/example-01/test.desc b/regression/goto-analyzer/example-01/test.desc new file mode 100644 index 00000000000..55e2081b25d --- /dev/null +++ b/regression/goto-analyzer/example-01/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--verify --example +^\[main.assertion.1\] line (\d)+ Should be unreachable: UNKNOWN$ +^\[main.assertion.2\] line (\d)+ Always true: UNKNOWN$ +^\[main.assertion.3\] line (\d)+ Sometimes true, sometimes false: UNKNOWN$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This is an example of a test case for basic domain functionality. + diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 798ee0c6704..52d3e7c36ec 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -10,6 +10,7 @@ SRC = ai.cpp \ dirty.cpp \ does_remove_const.cpp \ escape_analysis.cpp \ + example_domain.cpp \ flow_insensitive_analysis.cpp \ global_may_alias.cpp \ goto_rw.cpp \ diff --git a/src/analyses/example_domain.cpp b/src/analyses/example_domain.cpp new file mode 100644 index 00000000000..4f31dc3a34f --- /dev/null +++ b/src/analyses/example_domain.cpp @@ -0,0 +1,193 @@ +/*******************************************************************\ + +Module: Abstract Interpretation + +Author: Martin Brain + +\*******************************************************************/ + +#include "example_domain.h" + +#include + +example_domaint::example_domaint() +{ + // This must set the domain to bottom i.e. "no possible values" + make_bottom(); +} + +example_domaint::~example_domaint() +{ + // You probably don't need anything here +} + +// Transform updates the domain with the effect of the instruction "from" +void example_domaint::transform( + const irep_idt &function_from, + trace_ptrt from, + const irep_idt &function_to, + trace_ptrt to, + ai_baset &ai, + const namespacet &ns) +{ + std::cerr << "Example domain @ 0x" << this << " transform using instruction " + << from->current_location()->location_number << '\n'; + + // If e is an exprt (an expression) then + // std::cerr << e.pretty() + // prints it out + + // Normally how the state of the domain is updated would depend on + // what the instruction was (see below). However the state we are + // storing is so simple that we can just... + this->may_reach = true; + + const goto_programt::instructiont &instruction = *(from->current_location()); + switch(instruction.type()) + { + /** These are the instructions you actually need to implement **/ + case DECL: + // Creates a new variable to_code_decl(instruction.code).symbol() + break; + + case DEAD: + // Says that to_code_dead(instruction.code).symbol() is no longer needed + break; + + case ASSIGN: + // Set to_code_assign(instruction.code).lhs() to + // to_code_assign(instruction.code).rhs() + break; + + case GOTO: + { + // Comparing iterators is safe as the target must be within the same list + // of instructions because this is a GOTO. + locationt next = from->current_location(); + next++; + if( + from->current_location()->get_target() != + next) // If equal then effectively a SKIP + { + if(next == to->current_location()) + { + // Branch is not taken + } + else + { + // Branch is taken + } + } + break; + } + + case FUNCTION_CALL: + { + // Function calls are a bit of a fiddle... + // const code_function_callt &code_function_call = + // to_code_function_call(instruction.code); + break; + } + /* Removed from more recent versions + case RETURN: // Are transformed away into SET_RETURN_VALUE + // and then GOTO the end of the function + DATA_INVARIANT(false, "Returns must be removed before analysis"); + break; + */ + case SET_RETURN_VALUE: + { + // Handle setting the return value + break; + } + + case ASSUME: + // It is safe to over-approximate these by ... ignoring them! + break; + + /** These are instructions you really can ignore **/ + case ASSERT: // An assert is a check; they don't alter execution + // If goto-analyzer is run with --verify they will be checked after fixpoint + // by using the ai_simplify() method given below. + break; + + // Mostly markers + case LOCATION: // No action required + case SKIP: // No action required + case END_FUNCTION: // No action required + break; + + case CATCH: + case THROW: + DATA_INVARIANT(false, "Exceptions must be removed before analysis"); + break; + + case ATOMIC_BEGIN: // Ignoring is a valid over-approximation + case ATOMIC_END: // Ignoring is a valid over-approximation + case START_THREAD: // Require a concurrent analysis at higher level + case END_THREAD: // Require a concurrent analysis at higher level + break; + + case OTHER: +#if 0 + DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER"); +#endif + break; + + case INCOMPLETE_GOTO: + case NO_INSTRUCTION_TYPE: + DATA_INVARIANT(false, "Only complete instructions can be analyzed"); + break; + } + + return; +} + +// Merges the contents of b into this +bool example_domaint::merge(const example_domaint &b, trace_ptrt, trace_ptrt) +{ + std::cerr << "Example domain @ 0x" << this << " merge in example domain @ 0x" + << &b << '\n'; + + bool old = this->may_reach; + this->may_reach |= b.may_reach; + + // Returning true here has consequences! + // If merge is true then the domain will be requeued and transformed again. + // Fixpoint is reached when all domains return false when merged. + return (old != this->may_reach); +} + +void example_domaint::make_bottom() +{ + this->may_reach = false; +} + +void example_domaint::make_top() +{ + this->may_reach = true; +} + +void example_domaint::make_entry() +{ + // This is fine for almost everyone + make_top(); +} + +bool example_domaint::is_bottom() const +{ + return may_reach == false; +} + +bool example_domaint::is_top() const +{ + return may_reach == true; +} + +void example_domaint::output( + std::ostream &out, + const ai_baset &ai, + const namespacet &ns) const +{ + out << "Example domain (" << may_reach << ") @ 0x" << this; + return; +} diff --git a/src/analyses/example_domain.h b/src/analyses/example_domain.h new file mode 100644 index 00000000000..dd88757fc82 --- /dev/null +++ b/src/analyses/example_domain.h @@ -0,0 +1,70 @@ +/*******************************************************************\ + +Module: Abstract Interpretation + +Author: Martin Brain + +\*******************************************************************/ + +/// \file +/// This is a skeleton implementation of an abstract interpretation +/// domain. It is intended to be a start-point for writing your own +/// domain! + +#ifndef CPROVER_ANALYSES_EXAMPLE_DOMAIN_H +#define CPROVER_ANALYSES_EXAMPLE_DOMAIN_H + +#include "ai_domain.h" + +class example_domaint : public ai_domain_baset +{ +public: + /// Constructors + example_domaint(); + + /// Destructor + virtual ~example_domaint(); + + /// Transform updates the domain with the effect of the instruction + /// given by "from". + /// As GOTO has multiple next instructions, the abstract trace "to" + /// is passed so you can tell whether it is the branch taken or not. + virtual void transform( + const irep_idt &function_from, + trace_ptrt from, + const irep_idt &function_to, + trace_ptrt to, + ai_baset &ai, + const namespacet &ns) override; + + /// Merges two domains together + /// \return true if and only if *this has been modified / extended + /// If it is true then it will requeue this domain for analysis + bool merge(const example_domaint &b, trace_ptrt, trace_ptrt); + + /// Set the domain to be empty, i.e. representing nothing + void make_bottom() override; + + /// Set the domain to allow all possibilities + void make_top() override; + + /// Set up the domain for the start of the program + void make_entry() override; + + /// Is the domain bottom or not + bool is_bottom() const override; + + /// Is the domain top or not + bool is_top() const override; + + /// Output the domain as a string + void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) + const override; + +protected: + // Domain state goes here + // For now we will track which states may (an overapproximation) be reachable. + bool may_reach; +}; + +#endif // CPROVER_ANALYSES_EXAMPLE_DOMAIN_H diff --git a/src/goto-analyzer/build_analyzer.cpp b/src/goto-analyzer/build_analyzer.cpp index 9d9e44e318a..aa582ade34e 100644 --- a/src/goto-analyzer/build_analyzer.cpp +++ b/src/goto-analyzer/build_analyzer.cpp @@ -12,6 +12,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include #include #include +#include #include #include #include @@ -68,6 +69,16 @@ std::unique_ptr build_analyzer( df = util_make_unique< ai_domain_factory_default_constructort>(); } + else if(options.get_bool_option("example")) + { + // If you want to pass command line options to domains, you will + // need to replace ai_domain_factory_default_constructort with + // your own factory which inherits from + // ai_domain_factoryt + // and implements the ai_domain_factory_baset::make method + df = util_make_unique< + ai_domain_factory_default_constructort>(); + } else if(options.get_bool_option("intervals")) { df = util_make_unique< @@ -121,6 +132,13 @@ std::unique_ptr build_analyzer( return util_make_unique( goto_model.goto_functions); } + else if(options.get_bool_option("example")) + { + auto df = util_make_unique< + ai_domain_factory_default_constructort>(); + return util_make_unique>(std::move(df)); + } + else if(options.get_bool_option("dependence-graph")) { return util_make_unique(ns); diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 840621d0baf..68b2f3d6e45 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -307,6 +307,15 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) PARSE_OPTIONS_VSD(cmdline, options); options.set_option("data-dependencies", true); // Always set } + else if(cmdline.isset("example")) + { + options.set_option("example", true); + options.set_option("domain set", true); + // Any other options you want should be: + // 1. located in cmdline + // 2. checked and errors reported + // 3. put into the options object when sanitised + } // Reachability questions, when given with a domain swap from specific // to general tasks so that they can use the domain & parameterisations. @@ -735,6 +744,7 @@ void goto_analyzer_parse_optionst::help() " {y--constants} \t a constant for each variable if possible\n" " {y--intervals} \t an interval for each variable\n" " {y--non-null} \t tracks which pointers are non-null\n" + " {y--example} \t whatever you implement in the example\n" " {y--dependence-graph} \t data and control dependencies between" " instructions\n" " {y--vsd}, {y--variable-sensitivity} \t a configurable non-relational" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index beda0d3a2d3..be0c4cc2478 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -131,6 +131,7 @@ class optionst; "(dependence-graph)" \ "(vsd)(variable-sensitivity)" \ "(dependence-graph-vs)" \ + "(example)" \ #define GOTO_ANALYSER_OPTIONS_STORAGE \ "(one-domain-per-history)" \