Merge pull request #1790 from martin-cs/fix/correct-domain-interface

Fix/correct domain interface

src/analyses/ai.cpp

@@ -365,8 +365,7 @@ bool ai_baset::visit(
       // initialize state, if necessary
       get_state(to_l);
 
-      new_values.transform(
-        l, to_l, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL);
+      new_values.transform(l, to_l, *this, ns);
 
       if(merge(new_values, l, to_l))
         have_new_values=true;
@@ -399,8 +398,7 @@ bool ai_baset::do_function_call(
   {
     // if we don't have a body, we just do an edige call -> return
     std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
-    tmp_state->transform(
-      l_call, l_return, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL);
+    tmp_state->transform(l_call, l_return, *this, ns);
 
     return merge(*tmp_state, l_call, l_return);
   }
@@ -417,8 +415,7 @@ bool ai_baset::do_function_call(
 
     // do the edge from the call site to the beginning of the function
     std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
-    tmp_state->transform(
-      l_call, l_begin, *this, ns, ai_domain_baset::edge_typet::CALL);
+    tmp_state->transform(l_call, l_begin, *this, ns);
 
     bool new_data=false;
 
@@ -445,8 +442,7 @@ bool ai_baset::do_function_call(
       return false; // function exit point not reachable
 
     std::unique_ptr<statet> tmp_state(make_temporary_state(end_state));
-    tmp_state->transform(
-      l_end, l_return, *this, ns, ai_domain_baset::edge_typet::RETURN);
+    tmp_state->transform(l_end, l_return, *this, ns);
 
     // Propagate those
     return merge(*tmp_state, l_end, l_return);

src/analyses/ai.h

@@ -31,13 +31,6 @@ class ai_baset;
 class ai_domain_baset
 {
 public:
-  enum class edge_typet
-  {
-    FUNCTION_LOCAL,
-    CALL,
-    RETURN,
-  };
-
   // The constructor is expected to produce 'false'
   // or 'bottom'
   ai_domain_baset()
@@ -55,13 +48,21 @@ class ai_domain_baset
   // b) there is an edge from the last instruction (END_FUNCTION)
   //    of the function to the instruction _following_ the call site
   //    (this also needs to set the LHS, if applicable)
+  //
+  // "this" is the domain before the instruction "from"
+  // "from" is the instruction to be interpretted
+  // "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
+  //
+  // PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
+  // PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
+  // PRECONDITION(are_comparable(from,to) ||
+  //              (from->is_function_call() || from->is_end_function())
 
   virtual void transform(
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns,
-    edge_typet edge_type) = 0;
+    const namespacet &ns) = 0;
 
   virtual void output(
     std::ostream &out,
@@ -98,6 +99,11 @@ class ai_domain_baset
   //
   // This computes the join between "this" and "b".
   // Return true if "this" has changed.
+  // In the usual case, "b" is the updated state after "from"
+  // and "this" is the state before "to".
+  //
+  // PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
+  // PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
 
   // This method allows an expression to be simplified / evaluated using the
   // current state.  It is used to evaluate assertions and in program

src/analyses/constant_propagator.cpp

@@ -45,8 +45,7 @@ void constant_propagator_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet edge_type)
+  const namespacet &ns)
 {
 #ifdef DEBUG
   std::cout << "Transform from/to:\n";
@@ -94,6 +93,8 @@ void constant_propagator_domaint::transform(
   {
     exprt g;
 
+    // Comparing iterators is safe as the target must be within the same list
+    // of instructions because this is a GOTO.
     if(from->get_target()==to)
       g=simplify_expr(from->guard, ns);
     else
@@ -122,15 +123,14 @@ void constant_propagator_domaint::transform(
     const code_function_callt &function_call=to_code_function_call(from->code);
     const exprt &function=function_call.function();
 
-    const locationt& next=std::next(from);
-
     if(function.id()==ID_symbol)
     {
       // called function identifier
       const symbol_exprt &symbol_expr=to_symbol_expr(function);
       const irep_idt id=symbol_expr.get_identifier();
 
-      if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL)
+      // Functions with no body
+      if(from->function == to->function)
       {
         if(id==CPROVER_PREFIX "set_must" ||
            id==CPROVER_PREFIX "get_must" ||
@@ -178,7 +178,9 @@ void constant_propagator_domaint::transform(
     else
     {
       // unresolved call
-      INVARIANT(to==next, "Unresolved call can only be approximated if a skip");
+      INVARIANT(
+        from->function == to->function,
+        "Unresolved call can only be approximated if a skip");
 
       if(have_dirty)
         values.set_dirty_to_top(cp->dirty, ns);

src/analyses/constant_propagator.h

@@ -25,8 +25,7 @@ class constant_propagator_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai_base,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+    const namespacet &ns) final override;
 
   virtual void output(
     std::ostream &out,

src/analyses/custom_bitvector_analysis.cpp

@@ -269,8 +269,7 @@ void custom_bitvector_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet edge_type)
+  const namespacet &ns)
 {
   // upcast of ai
   custom_bitvector_analysist &cba=
@@ -397,7 +396,7 @@ void custom_bitvector_domaint::transform(
         else
         {
           // only if there is an actual call, i.e., we have a body
-          if(edge_type != ai_domain_baset::edge_typet::FUNCTION_LOCAL)
+          if(from->function != to->function)
           {
             const code_typet &code_type=
               to_code_type(ns.lookup(identifier).type);
@@ -520,6 +519,8 @@ void custom_bitvector_domaint::transform(
     {
       exprt guard=instruction.guard;
 
+      // Comparing iterators is safe as the target must be within the same list
+      // of instructions because this is a GOTO.
       if(to!=from->get_target())
         guard.make_not();
 

src/analyses/custom_bitvector_analysis.h

@@ -23,12 +23,9 @@ class custom_bitvector_analysist;
 class custom_bitvector_domaint:public ai_domain_baset
 {
 public:
-  void transform(
-    locationt from,
-    locationt to,
-    ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+  void
+  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
+    final override;
 
   void output(
     std::ostream &out,

src/analyses/dependence_graph.cpp

@@ -187,24 +187,22 @@ void dep_graph_domaint::transform(
   goto_programt::const_targett from,
   goto_programt::const_targett to,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet edge_type)
+  const namespacet &ns)
 {
   dependence_grapht *dep_graph=dynamic_cast<dependence_grapht*>(&ai);
   assert(dep_graph!=nullptr);
 
   // propagate control dependencies across function calls
   if(from->is_function_call())
   {
-    const goto_programt::const_targett next = std::next(from);
-
-    if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL)
+    if(from->function == to->function)
     {
       control_dependencies(from, to, *dep_graph);
     }
     else
     {
       // edge to function entry point
+      const goto_programt::const_targett next = std::next(from);
 
       dep_graph_domaint *s=
         dynamic_cast<dep_graph_domaint*>(&(dep_graph->get_state(next)));

src/analyses/dependence_graph.h

@@ -83,8 +83,7 @@ class dep_graph_domaint:public ai_domain_baset
     goto_programt::const_targett from,
     goto_programt::const_targett to,
     ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,

src/analyses/escape_analysis.cpp

@@ -165,8 +165,7 @@ void escape_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet /*edge_type*/)
+  const namespacet &ns)
 {
   if(has_values.is_false())
     return;

src/analyses/escape_analysis.h

@@ -28,12 +28,9 @@ class escape_domaint:public ai_domain_baset
   {
   }
 
-  void transform(
-    locationt from,
-    locationt to,
-    ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+  void
+  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
+    final override;
 
   void output(
     std::ostream &out,

src/analyses/global_may_alias.cpp

@@ -79,8 +79,7 @@ void global_may_alias_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet /*edge_type*/)
+  const namespacet &ns)
 {
   if(has_values.is_false())
     return;

src/analyses/global_may_alias.h

@@ -28,12 +28,9 @@ class global_may_alias_domaint:public ai_domain_baset
   {
   }
 
-  void transform(
-    locationt from,
-    locationt to,
-    ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+  void
+  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
+    final override;
 
   void output(
     std::ostream &out,

src/analyses/interval_domain.cpp

@@ -59,8 +59,7 @@ void interval_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet /*edge_type*/)
+  const namespacet &ns)
 {
   const goto_programt::instructiont &instruction=*from;
   switch(instruction.type)
@@ -79,12 +78,17 @@ void interval_domaint::transform(
 
   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;
       next++;
-      if(next==to)
-        assume(not_exprt(instruction.guard), ns);
-      else
-        assume(instruction.guard, ns);
+      if(from->get_target() != next) // If equal then a skip
+      {
+        if(next == to)
+          assume(not_exprt(instruction.guard), ns);
+        else
+          assume(instruction.guard, ns);
+      }
     }
     break;
 

src/analyses/interval_domain.h

@@ -32,12 +32,9 @@ class interval_domaint:public ai_domain_baset
   {
   }
 
-  void transform(
-    locationt from,
-    locationt to,
-    ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+  void
+  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
+    final override;
 
   void output(
     std::ostream &out,

src/analyses/invariant_set_domain.cpp

@@ -17,13 +17,14 @@ void invariant_set_domaint::transform(
   locationt from_l,
   locationt to_l,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet /*edge_type*/)
+  const namespacet &ns)
 {
   switch(from_l->type)
   {
   case GOTO:
     {
+      // Comparing iterators is safe as the target must be within the same list
+      // of instructions because this is a GOTO.
       exprt tmp(from_l->guard);
 
       goto_programt::const_targett next=from_l;

src/analyses/invariant_set_domain.h

@@ -56,8 +56,7 @@ class invariant_set_domaint:public ai_domain_baset
     locationt from_l,
     locationt to_l,
     ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+    const namespacet &ns) final override;
 
   void make_top() final override
   {

src/analyses/is_threaded.cpp

@@ -48,12 +48,9 @@ class is_threaded_domaint:public ai_domain_baset
            old_is_threaded!=is_threaded;
   }
 
-  void transform(
-    locationt from,
-    locationt to,
-    ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet /*edge_type*/) final override
+  void
+  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
+    final override
   {
     // assert(reachable);