From f166bfbd37b5fcdde586e9eeea03d0441c96cb94 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Sun, 3 Dec 2023 17:08:42 +0100 Subject: [PATCH 1/4] Apply topological sort to SMV definitions --- src/smvlang/smv_typecheck.cpp | 87 ++++++++++++++++++++++++++++++++--- 1 file changed, 80 insertions(+), 7 deletions(-) diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 0bec5d149..ad5f37cb6 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -1712,6 +1713,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 symbols; +}; + /*******************************************************************\ Function: smv_typecheckt::convert_defines @@ -1726,15 +1743,71 @@ Function: smv_typecheckt::convert_defines void smv_typecheckt::convert_defines(exprt::operandst &invar) { - for(auto &define_it : define_map) + // create graph of definition dependencies + typedef size_t node_indext; + std::map id_node_index; + std::map index_node_id; + grapht> definition_graph; + + for(const auto &p : define_map) { + // 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 top_order=definition_graph.topsort(); + if(top_order.empty()) { - convert_define(define_it.first); + // 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{ - symbol_exprt{define_it.first, define_it.second.value.type()}, - define_it.second.value}; - invar.push_back(equality); + // generate constraint + equal_exprt equality{symbol_exprt{it->first, it->second.value.type()}, + it->second.value}; + invar.push_back(equality); + } + } + 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{symbol_exprt{id, define_map[id].value.type()}, + define_map[id].value}; + invar.push_back(equality); + } } } From a3770f357addce33f6bd5d851bf51decacb360d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Sun, 3 Dec 2023 16:45:33 +0100 Subject: [PATCH 2/4] Increase YYMAXDEPTH --- src/smvlang/parser.y | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index a5e2bd76b..752a13474 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -14,7 +14,7 @@ #include "smv_y.tab.h" -#define YYMAXDEPTH 200000 +#define YYMAXDEPTH 2000000 #define YYSTYPE_IS_TRIVIAL 1 /*------------------------------------------------------------------------*/ From f9a799bc9acf14f06cc8dc0182e80cc954b667a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Sun, 3 Dec 2023 19:17:04 +0100 Subject: [PATCH 3/4] Apply `clang-format` patch --- src/smvlang/smv_typecheck.cpp | 44 +++++++++++++++++------------------ 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index ad5f37cb6..9a317f17b 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -1713,15 +1713,15 @@ void smv_typecheckt::convert_define(const irep_idt &identifier) symbol.type=d.value.type(); } -class symbol_collectort:public const_expr_visitort +class symbol_collectort : public const_expr_visitort { public: virtual void operator()(const exprt &expr) { - if(expr.id()==ID_symbol) + if(expr.id() == ID_symbol) { - const symbol_exprt &symbol_expr=to_symbol_expr(expr); - const irep_idt id=symbol_expr.get_identifier(); + const symbol_exprt &symbol_expr = to_symbol_expr(expr); + const irep_idt id = symbol_expr.get_identifier(); symbols.insert(id); } } @@ -1749,47 +1749,47 @@ void smv_typecheckt::convert_defines(exprt::operandst &invar) std::map index_node_id; grapht> definition_graph; - for(const auto &p : define_map) { + for(const auto &p : define_map) + { // 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()) + 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; + 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]; + 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()) + 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; + id_node_index[id] = definition_graph.add_node(); + index_node_id[id_node_index[id]] = id; } - node_indext s=id_node_index[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 top_order=definition_graph.topsort(); + std::list 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(); + for(define_mapt::iterator it = define_map.begin(); it != define_map.end(); it++) { convert_define(it->first); // generate constraint - equal_exprt equality{symbol_exprt{it->first, it->second.value.type()}, - it->second.value}; + equal_exprt equality{ + symbol_exprt{it->first, it->second.value.type()}, it->second.value}; invar.push_back(equality); } } @@ -1797,15 +1797,15 @@ void smv_typecheckt::convert_defines(exprt::operandst &invar) { for(const auto &idx : top_order) { - const irep_idt &id=index_node_id[idx]; + const irep_idt &id = index_node_id[idx]; // skip independent defines - if(define_map.find(id)==define_map.end()) + if(define_map.find(id) == define_map.end()) continue; convert_define(id); // generate constraint - equal_exprt equality{symbol_exprt{id, define_map[id].value.type()}, - define_map[id].value}; + equal_exprt equality{ + symbol_exprt{id, define_map[id].value.type()}, define_map[id].value}; invar.push_back(equality); } } From 79a97154c4d5a139230c11f8c322ab896d9dd011 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Fri, 28 Mar 2025 08:05:49 +0100 Subject: [PATCH 4/4] Warning about graph not being a DAG only if non-empty --- src/smvlang/smv_typecheck.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 9a317f17b..693066f69 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -1781,7 +1781,11 @@ void smv_typecheckt::convert_defines(exprt::operandst &invar) { // in case no topological order exists, fall back on starting with any // defined symbol - warning() << "definiton graph is not a DAG"; + + // warn if non-empty graph is not a DAG + if(!definition_graph.empty()) + warning() << "definiton graph is not a DAG"; + for(define_mapt::iterator it = define_map.begin(); it != define_map.end(); it++) {