WIP

src/analyses/history_automaton.cpp

@@ -0,0 +1,81 @@
+/*******************************************************************\
+
+Module: Abstract Interpretation
+
+Author: Martin Brain, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Abstract Interpretation history automaton
+
+#include "history_automaton.h"
+
+history_automatont::history_automatont(const ai_history_baset::trace_sett &end_states,
+                                       const ai_baset &ai,
+                                       const call_grapht &call_graph)
+{
+  using ai_history_baset::trace_ptrt;
+  using ai_history_baset::trace_sett;
+
+  // TODO : add to the actual graph
+  trace_sett working_set(end_states);
+  trace_sett processed;
+
+  while (!working_set.empty())
+  {
+    // Move current from the working set to processed so it will be
+    // processed at most once.
+    auto first = working_set.begin();
+    trace_ptrt current = *first;
+    working_set.erase(first);
+    processed.insert(current);
+
+    // We assume that the only locations with no predecessors are
+    // function start
+    if (current->current_location().incoming_edges.empty())
+    {
+      // TODO : out to caller context
+    }
+    else
+    {
+      const auto current_location(current->current_location());
+      const auto current_traces_ptr(ai.abstract_traces_before());
+      CHECK_RETURN(current_traces_ptr != nullptr);
+
+      const auto &current_trace_set(current_traces_ptr);
+      DATA_INVARIANT(current_trace_set.find(current) != current_trace_set.end(),
+                     "The current history must be in the set of histories at its location");
+
+      // For each predecessor location
+      for(const auto &predecessor : current_location->incoming_edges)
+      {
+        // TODO : if predecessor is call function have to reverse step
+        // into the called thing :-\
+
+        const auto predecessor_history_ptr(ai.abstract_traces_before(predecessor));
+        CHECK_RETURN(predecessor_history_ptr != nullptr);
+
+        // Try each history at that location
+        for(const auto &prehistory : *predecessor_history_ptr)
+        {
+          const auto step_result(prehistory.step(current_location, current_trace_set, no_caller_history));
+          // ai should have been run to fixed point
+          PRECONDITION(step_result.first != step_statust::NEW);
+
+          if (result.first == step_statust::MERGED && result.second == current)
+          {
+            // prehistory is a predecessor history!
+            // But have we seen it before?
+            if (processed.find(prehistory) != processed.end()) {
+              // Add it to the TODO list!
+              working_set.insert(prehistory);
+              // TODO : add to the actual graph
+            }
+          }
+        }
+      }
+    }
+  }
+}
+

src/analyses/history_automaton.h

@@ -0,0 +1,52 @@
+/*******************************************************************\
+
+Module: Abstract Interpretation
+
+Author: Martin Brain, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Abstract Interpretation history automaton
+///
+/// ai_history_baset subclasses are used to track the execution of the
+/// abstract interpreter.  They are effectively program counters with
+/// extra context / state (for example, a call stack).  So they
+/// describe a point in the (abstract) computation.  This class is an
+/// automaton showing how they connect together, describing the whole
+/// computation.  This allows you to find the abstract state(s) that
+/// lead to a given history.  For example, you could find what the
+/// state at function start that is sufficient to show a condition is
+/// true.  Or you could trace back something marked "false if
+/// reachable" and see if it really is reachable.
+
+#ifndef CPROVER_ANALYSES_HISTORY_AUTOMATON_H
+#define CPROVER_ANALYSES_HISTORY_AUTOMATON_H
+
+#include <analyses/ai_history.h>
+
+#include <util/graph.h>
+#include <util/json.h>
+#include <util/xml.h>
+
+/// Each node contains a single (pointer to) a history
+class history_automaton_nodet : public graph_nodet {
+ public:
+  using ai_history_baset::trace_ptrt;
+
+  trace_ptrt history;
+
+  explicit history_automaton_nodet(trace_ptrt h) : history(h) {}
+}
+
+
+/// Implement an automaton as a graph
+class history_automatont : public grapht<history_automaton_nodet> {
+ public : 
+  history_automatont(const ai_history_baset::trace_sett &end_states,
+                     const ai_baset &ai,
+                     const call_grapht &call_graph);
+
+}
+
+#endif // CPROVER_ANALYSES_HISTORY_AUTOMATON_H