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,22 @@ class ai_baset
     finalize();
   }
 
+  /// Accessing individual domains at particular domains
+  /// (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.
+
   /// 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 +311,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