From 2e129381e6dc2a3adf696cec696faf83010a9bce Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 29 Oct 2025 16:20:59 -0700
Subject: [PATCH] netlist conversion: replace recursion by explicit stack

---
 src/trans-netlist/trans_to_netlist.cpp | 63 +++++++++++++++++++-------
 1 file changed, 46 insertions(+), 17 deletions(-)

diff --git a/src/trans-netlist/trans_to_netlist.cpp b/src/trans-netlist/trans_to_netlist.cpp
index 7e485b4d3..b3a4e3422 100644
--- a/src/trans-netlist/trans_to_netlist.cpp
+++ b/src/trans-netlist/trans_to_netlist.cpp
@@ -141,9 +141,15 @@ class convert_trans_to_netlistt:public messaget
 
   literalt convert_rhs(const rhst &);
 
-  void finalize_lhs(lhs_mapt::iterator);
-
-  void convert_lhs_rec(const exprt &expr, std::size_t from, std::size_t to);
+  // The bv_varidts of the definitions that are yet to be processed.
+  using lhs_stackt = std::stack<lhs_mapt::iterator>;
+  void add_to_stack(
+    const exprt &expr,
+    std::size_t from,
+    std::size_t to,
+    lhs_stackt &);
+  void lhs_loop(lhs_stackt &);
+  void finalize_definition(lhs_mapt::iterator);
 
   void convert_constraints();
 
@@ -335,13 +341,17 @@ void convert_trans_to_netlistt::operator()(
   add_constraint(trans.invar());
   add_constraint(trans.trans());
 
-  // do recursive conversion for LHSs
-  for(lhs_mapt::iterator
-      it=lhs_map.begin();
-      it!=lhs_map.end();
-      it++)
   {
-    finalize_lhs(it);
+    // ensure all LHSs will be processed
+    lhs_stackt lhs_stack;
+
+    for(lhs_mapt::iterator
+        it=lhs_map.begin();
+        it!=lhs_map.end();
+        it++)
+    {
+      lhs_stack.push(it);
+    }
   }
 
   // finish the var_map
@@ -568,7 +578,23 @@ void convert_trans_to_netlistt::finalize_lhs(lhs_mapt::iterator lhs_it)
 
 /*******************************************************************\
 
-Function: convert_trans_to_netlistt::convert_lhs_rec
+Function: convert_trans_to_netlistt::lhs_loop
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void convert_trans_to_netlistt::lhs_loop(lhs_stackt &lhs_stack)
+{
+}
+
+/*******************************************************************\
+
+Function: convert_trans_to_netlistt::add_to_stack
 
   Inputs:
 
@@ -578,10 +604,11 @@ Function: convert_trans_to_netlistt::convert_lhs_rec
 
 \*******************************************************************/
 
-void convert_trans_to_netlistt::convert_lhs_rec(
+void convert_trans_to_netlistt::add_to_stack(
   const exprt &expr,
   std::size_t from,
-  std::size_t to)
+  std::size_t to,
+  lhs_stackt &lhs_stack)
 {
   PRECONDITION(from <= to);
 
@@ -604,7 +631,9 @@ void convert_trans_to_netlistt::convert_lhs_rec(
       // we only need to do wires
       if(!it->second.var->is_wire()) return;
 
-      finalize_lhs(it);
+      // only push if not already done
+      if(!it->second.converted)     
+        lhs_stack.push(it);
     }
 
     return;
@@ -616,7 +645,7 @@ void convert_trans_to_netlistt::convert_lhs_rec(
          to_extractbit_expr(expr).index(), i)) // constant?
     {
       from = i.to_ulong();
-      convert_lhs_rec(to_extractbit_expr(expr).src(), from, from);
+      add_to_stack(to_extractbit_expr(expr).src(), from, from, lhs_stack);
       return;
     }
   }
@@ -635,7 +664,7 @@ void convert_trans_to_netlistt::convert_lhs_rec(
       from = new_from.to_ulong();
       to = new_to.to_ulong();
 
-      convert_lhs_rec(to_extractbits_expr(expr).src(), from, to);
+      add_to_stack(to_extractbits_expr(expr).src(), from, to, lhs_stack);
       return;
     }
   }
@@ -655,7 +684,7 @@ void convert_trans_to_netlistt::convert_lhs_rec(
     if(width==0)
       continue;
 
-    convert_lhs_rec(*it, 0, width - 1);
+    add_to_stack(*it, 0, width - 1, lhs_stack);
   }
 }
 
@@ -679,7 +708,7 @@ literalt convert_trans_to_netlistt::convert_rhs(const rhst &rhs)
   if(!rhs_entry.converted)
   {
     // get all lhs symbols this depends on
-    convert_lhs_rec(rhs_entry.expr, 0, rhs_entry.width - 1);
+    add_to_stack(rhs_entry.expr, 0, rhs_entry.width - 1, lhs_stack);
 
     rhs_entry.converted=true;