Verilog: extract verilog_synthesist::synthesis_constant

This extracts the conversion of expressions into synthesis-time constants
into a new method.

Author: kroening

src/verilog/verilog_synthesis.cpp

@@ -405,6 +405,35 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
 
 /*******************************************************************\
 
+Function: verilog_synthesist::synthesis_constant
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::optional<mp_integer>
+verilog_synthesist::synthesis_constant(const exprt &expr)
+{
+  exprt synthesised = synth_expr(expr, symbol_statet::CURRENT);
+
+  exprt simplified = simplify_expr(synthesised, ns);
+
+  if(!simplified.is_constant())
+    return {};
+
+  auto number = numeric_cast<mp_integer>(to_constant_expr(simplified));
+  if(!number.has_value())
+    DATA_INVARIANT(false, "synthesis_constant expects a numerical type");
+
+  return number.value();
+}
+
+/*******************************************************************\
+
 Function: verilog_synthesist::value_mapt::guarded_expr
 
   Inputs:
@@ -2950,19 +2979,19 @@ void verilog_synthesist::synth_for(const verilog_fort &statement)
   {  
     exprt tmp_guard=statement.condition();
     tmp_guard = typecast_exprt{tmp_guard, bool_typet{}};
-    tmp_guard = synth_expr(tmp_guard, symbol_statet::CURRENT);
-    simplify(tmp_guard, ns);
- 
-    if(!tmp_guard.is_constant())
+
+    auto guard_value_opt = synthesis_constant(tmp_guard);
+
+    if(!guard_value_opt.has_value())
     {
-      throw errort().with_location(
-        to_multi_ary_expr(statement).op1().source_location())
+      throw errort().with_location(statement.condition().source_location())
         << "synthesis failed to evaluate loop guard: `" << to_string(tmp_guard)
         << '\'';
     }
 
-    if(tmp_guard.is_false()) break;
-    
+    if(guard_value_opt.value() == 0)
+      break;
+
     // copy the body
     verilog_statementt tmp_body=statement.body();
     synth_statement(tmp_body);

src/verilog/verilog_synthesis_class.h

@@ -177,7 +177,10 @@ class verilog_synthesist:
 
     exprt guarded_expr(exprt) const;
   };
-   
+
+  // expressions
+  [[nodiscard]] std::optional<mp_integer> synthesis_constant(const exprt &);
+
   exprt current_value(
     const value_mapt::mapt &map,
     const symbolt &symbol,