Sort definitions topologically before doing typecheck for SMV

src/smvlang/smv_typecheck.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/typecheck.h>
 #include <util/arith_tools.h>
 #include <util/std_expr.h>
+#include <util/graph.h>
 
 #include "smv_typecheck.h"
 #include "expr2smv.h"
@@ -1297,13 +1298,13 @@ void smv_typecheckt::convert_define(const irep_idt &identifier)
   definet &d=define_map[identifier];
 
   if(d.typechecked) return;
-  
+
   if(d.in_progress)
   {
     error() << "definition of `" << identifier << "' is cyclic" << eom;
     throw 0;
   }
-  
+
   symbol_tablet::symbolst::iterator it=symbol_table.symbols.find(identifier);
 
   if(it==symbol_table.symbols.end())
@@ -1326,6 +1327,22 @@ void smv_typecheckt::convert_define(const irep_idt &identifier)
     symbol.type=d.value.type();
 }
 
+class symbol_collectort:public const_expr_visitort
+{
+public:
+  virtual void operator()(const exprt &expr)
+  {
+    if(expr.id()==ID_symbol)
+    {
+      const symbol_exprt &symbol_expr=to_symbol_expr(expr);
+      const irep_idt id=symbol_expr.get_identifier();
+      symbols.insert(id);
+    }
+  }
+
+  std::unordered_set<irep_idt, irep_id_hash> symbols;
+};
+
 /*******************************************************************\
 
 Function: smv_typecheckt::convert_defines
@@ -1340,18 +1357,75 @@ Function: smv_typecheckt::convert_defines
 
 void smv_typecheckt::convert_defines(exprt::operandst &invar)
 {
-  for(define_mapt::iterator it=define_map.begin();
-      it!=define_map.end();
-      it++)
+  // create graph of definition dependencies
+  typedef size_t node_indext;
+  std::map<irep_idt, node_indext> id_node_index;
+  std::map<node_indext, irep_idt> index_node_id;
+  grapht<graph_nodet<empty_edget> > definition_graph;
+
+  for(const auto &p : define_map)
   {
-    convert_define(it->first);
-
-    // generate constraint
-    equal_exprt equality;
-    equality.lhs()=exprt(ID_symbol, it->second.value.type());
-    equality.lhs().set(ID_identifier, it->first);
-    equality.rhs()=it->second.value;
-    invar.push_back(equality);
+    // for each defined symbol, collect all symbols it depends on
+    symbol_collectort visitor;
+    p.second.value.visit(visitor);
+    if(id_node_index.find(p.first)==id_node_index.end())
+    {
+      id_node_index[p.first]=definition_graph.add_node();
+      index_node_id[id_node_index[p.first]]=p.first;
+    }
+    node_indext t=id_node_index[p.first];
+
+    // for each node t add (t, dep) for each definition dep it depends on
+    for(const auto &id : visitor.symbols)
+    {
+      if(id_node_index.find(id)==id_node_index.end())
+      {
+        id_node_index[id]=definition_graph.add_node();
+        index_node_id[id_node_index[id]]=id;
+      }
+      node_indext s=id_node_index[id];
+      definition_graph.add_edge(s, t);
+    }
+  }
+
+  // sort the graph topologically to reduce call depth of `convert_define` and
+  // `typecheck`
+  std::list<node_indext> top_order=definition_graph.topsort();
+  if(top_order.empty())
+  {
+    // in case no topological order exists, fall back on starting with any
+    // defined symbol
+    warning() << "definiton graph is not a DAG";
+    for(define_mapt::iterator it=define_map.begin();
+        it!=define_map.end();
+        it++)
+    {
+      convert_define(it->first);
+
+      // generate constraint
+      equal_exprt equality;
+      equality.lhs()=exprt(ID_symbol, it->second.value.type());
+      equality.lhs().set(ID_identifier, it->first);
+      equality.rhs()=it->second.value;
+    }
+  }
+  else
+  {
+    for(const auto idx : top_order)
+    {
+      const irep_idt &id=index_node_id[idx];
+      // skip independent defines
+      if(define_map.find(id)==define_map.end())
+        continue;
+      convert_define(id);
+
+      // generate constraint
+      equal_exprt equality;
+      equality.lhs()=exprt(ID_symbol, define_map[id].value.type());
+      equality.lhs().set(ID_identifier, id);
+      equality.rhs()=define_map[id].value;
+      invar.push_back(equality);
+    }
   }
 }