Refactor the methods that access "the abstract domain at a location".

This allows us to be a lot more flexible about the relationship
between location and domain rather than assuming it is a 1-to-1 map.

Author: martin

src/analyses/ai.cpp

@@ -50,7 +50,7 @@ void ai_baset::output(
     out << "**** " << i_it->location_number << " "
         << i_it->source_location << "\n";
 
-    find_state(i_it).output(out, *this, ns);
+    abstract_state_before(i_it)->output(out, *this, ns);
     out << "\n";
     #if 1
     goto_program.output_instruction(ns, identifier, out, *i_it);
@@ -101,7 +101,8 @@ jsont ai_baset::output_json(
       json_numbert(std::to_string(i_it->location_number));
     location["sourceLocation"]=
       json_stringt(i_it->source_location.as_string());
-    location["abstractState"]=find_state(i_it).output_json(*this, ns);
+    location["abstractState"] =
+      abstract_state_before(i_it)->output_json(*this, ns);
 
     // Ideally we need output_instruction_json
     std::ostringstream out;
@@ -162,7 +163,7 @@ xmlt ai_baset::output_xml(
       "source_location",
       i_it->source_location.as_string());
 
-    location.new_element(find_state(i_it).output_xml(*this, ns));
+    location.new_element(abstract_state_before(i_it)->output_xml(*this, ns));
 
     // Ideally we need output_instruction_xml
     std::ostringstream out;

src/analyses/ai.h

@@ -82,15 +82,23 @@ class ai_baset
     finalize();
   }
 
+  /// Accessing individual domains at particular locations
+  /// (without needing to know what kind of domain or history is used)
+  /// A pointer to a copy as the method should be const and
+  /// there are some non-trivial cases including merging domains, etc.
+  /// Intended for users of the abstract interpreter; don't use internally.
+
   /// Returns the abstract state before the given instruction
-  virtual const ai_domain_baset & abstract_state_before(
-    goto_programt::const_targett t) const = 0;
+  /// PRECONDITION(l is dereferenceable)
+  virtual std::unique_ptr<statet> abstract_state_before(locationt l) const = 0;
 
   /// Returns the abstract state after the given instruction
-  virtual const ai_domain_baset & abstract_state_after(
-    goto_programt::const_targett t) const
+  virtual std::unique_ptr<statet> abstract_state_after(locationt l) const
   {
-    return abstract_state_before(std::next(t));
+    /// PRECONDITION(l is dereferenceable && std::next(l) is dereferenceable)
+    /// Check relies on a DATA_INVARIANT of goto_programs
+    INVARIANT(!l->is_end_function(), "No state after the last instruction");
+    return abstract_state_before(std::next(l));
   }
 
   virtual void clear()
@@ -304,10 +312,17 @@ class ait:public ai_baset
     return it->second;
   }
 
-  const ai_domain_baset & abstract_state_before(
-    goto_programt::const_targett t) const override
+  std::unique_ptr<statet> abstract_state_before(locationt t) const override
   {
-    return (*this)[t];
+    typename state_mapt::const_iterator it = state_map.find(t);
+    if(it == state_map.end())
+    {
+      std::unique_ptr<statet> d = util_make_unique<domainT>();
+      CHECK_RETURN(d->is_bottom());
+      return d;
+    }
+
+    return util_make_unique<domainT>(it->second);
   }
 
   void clear() override

src/goto-analyzer/static_simplifier.cpp

@@ -65,8 +65,8 @@ bool static_simplifier(
 
       if(i_it->is_assert())
       {
-        bool unchanged=
-          ai.abstract_state_before(i_it).ai_simplify(i_it->guard, ns);
+        bool unchanged =
+          ai.abstract_state_before(i_it)->ai_simplify(i_it->guard, ns);
 
         if(unchanged)
           unmodified.asserts++;
@@ -75,8 +75,8 @@ bool static_simplifier(
       }
       else if(i_it->is_assume())
       {
-        bool unchanged=
-          ai.abstract_state_before(i_it).ai_simplify(i_it->guard, ns);
+        bool unchanged =
+          ai.abstract_state_before(i_it)->ai_simplify(i_it->guard, ns);
 
         if(unchanged)
           unmodified.assumes++;
@@ -85,8 +85,8 @@ bool static_simplifier(
       }
       else if(i_it->is_goto())
       {
-        bool unchanged=
-          ai.abstract_state_before(i_it).ai_simplify(i_it->guard, ns);
+        bool unchanged =
+          ai.abstract_state_before(i_it)->ai_simplify(i_it->guard, ns);
 
         if(unchanged)
           unmodified.gotos++;
@@ -102,11 +102,11 @@ bool static_simplifier(
         // <i=0, j=1>  i=j
         // should simplify to i=1, not to 0=1.
 
-        bool unchanged_lhs=
-          ai.abstract_state_before(i_it).ai_simplify_lhs(assign.lhs(), ns);
+        bool unchanged_lhs =
+          ai.abstract_state_before(i_it)->ai_simplify_lhs(assign.lhs(), ns);
 
-        bool unchanged_rhs=
-          ai.abstract_state_before(i_it).ai_simplify(assign.rhs(), ns);
+        bool unchanged_rhs =
+          ai.abstract_state_before(i_it)->ai_simplify(assign.rhs(), ns);
 
         if(unchanged_lhs && unchanged_rhs)
           unmodified.assigns++;
@@ -117,13 +117,13 @@ bool static_simplifier(
       {
         code_function_callt &fcall=to_code_function_call(i_it->code);
 
-        bool unchanged=
-          ai.abstract_state_before(i_it).ai_simplify(fcall.function(), ns);
+        bool unchanged =
+          ai.abstract_state_before(i_it)->ai_simplify(fcall.function(), ns);
 
         exprt::operandst &args=fcall.arguments();
 
         for(auto &o : args)
-          unchanged&=ai.abstract_state_before(i_it).ai_simplify(o, ns);
+          unchanged &= ai.abstract_state_before(i_it)->ai_simplify(o, ns);
 
         if(unchanged)
           unmodified.function_calls++;

src/goto-analyzer/static_verifier.cpp

@@ -55,7 +55,8 @@ bool static_verifier(
           continue;
 
         exprt e(i_it->guard);
-        const ai_domain_baset &domain(ai.abstract_state_before(i_it));
+        auto dp = ai.abstract_state_before(i_it);
+        const ai_domain_baset &domain(*dp);
         domain.ai_simplify(e, ns);
 
         json_objectt &j=json_result.push_back().make_object();
@@ -104,7 +105,8 @@ bool static_verifier(
           continue;
 
         exprt e(i_it->guard);
-        const ai_domain_baset &domain(ai.abstract_state_before(i_it));
+        auto dp = ai.abstract_state_before(i_it);
+        const ai_domain_baset &domain(*dp);
         domain.ai_simplify(e, ns);
 
         xmlt &x=xml_result.new_element("result");
@@ -160,7 +162,8 @@ bool static_verifier(
           continue;
 
         exprt e(i_it->guard);
-        const ai_domain_baset &domain(ai.abstract_state_before(i_it));
+        auto dp = ai.abstract_state_before(i_it);
+        const ai_domain_baset &domain(*dp);
         domain.ai_simplify(e, ns);
 
         out << '[' << i_it->source_location.get_property_id()

src/goto-analyzer/unreachable_instructions.cpp

@@ -59,7 +59,7 @@ static void build_dead_map_from_ai(
   dead_mapt &dest)
 {
   forall_goto_program_instructions(it, goto_program)
-    if(ai.abstract_state_before(it).is_bottom())
+    if(ai.abstract_state_before(it)->is_bottom())
       dest.insert(std::make_pair(it->location_number, it));
 }
 
@@ -418,7 +418,7 @@ std::unordered_set<irep_idt> compute_called_functions_from_ai(
 
     const goto_programt &p = f_it->second.body;
 
-    if(!ai.abstract_state_before(p.instructions.begin()).is_bottom())
+    if(!ai.abstract_state_before(p.instructions.begin())->is_bottom())
       called.insert(f_it->first);
   }