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

@@ -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
 

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.

regression/goto-analyzer/example-01/main.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+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;
+}

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.
+

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 \

src/analyses/example_domain.cpp

@@ -0,0 +1,193 @@
+/*******************************************************************\
+
+Module: Abstract Interpretation
+
+Author: Martin Brain
+
+\*******************************************************************/
+
+#include "example_domain.h"
+
+#include <iostream>
+
+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;
+}

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

src/goto-analyzer/build_analyzer.cpp

@@ -12,6 +12,7 @@ Author: Martin Brain, [email protected]
 #include <analyses/call_stack_history.h>
 #include <analyses/constant_propagator.h>
 #include <analyses/dependence_graph.h>
+#include <analyses/example_domain.h>
 #include <analyses/interval_domain.h>
 #include <analyses/local_control_flow_history.h>
 #include <analyses/variable-sensitivity/three_way_merge_abstract_interpreter.h>
@@ -68,6 +69,16 @@ std::unique_ptr<ai_baset> build_analyzer(
       df = util_make_unique<
         ai_domain_factory_default_constructort<constant_propagator_domaint>>();
     }
+    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<example_domaint>
+      // and implements the ai_domain_factory_baset::make method
+      df = util_make_unique<
+        ai_domain_factory_default_constructort<example_domaint>>();
+    }
     else if(options.get_bool_option("intervals"))
     {
       df = util_make_unique<
@@ -121,6 +132,13 @@ std::unique_ptr<ai_baset> build_analyzer(
       return util_make_unique<constant_propagator_ait>(
         goto_model.goto_functions);
     }
+    else if(options.get_bool_option("example"))
+    {
+      auto df = util_make_unique<
+        ai_domain_factory_default_constructort<example_domaint>>();
+      return util_make_unique<ait<variable_sensitivity_domaint>>(std::move(df));
+    }
+
     else if(options.get_bool_option("dependence-graph"))
     {
       return util_make_unique<dependence_grapht>(ns);

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"

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)" \