Merge pull request #251 from diffblue/verilog_synthesis_expr

synthesise command-line expressions

Author: tautschnig

regression/ebmc/ranking-function/counter_in_module1.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 counter_in_module1.sv
 --ranking-function instance.counter
 ^\[main\.property\.p0\] always \(eventually main.instance.counter == 0\): SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-We currently don't support hierarchical identifiers in the ranking function.

src/verilog/verilog_language.cpp

@@ -283,6 +283,13 @@ bool verilog_languaget::to_expr(
 
   // typecheck it
   result=verilog_typecheck(expr, module, get_message_handler(), ns);
+  if(result)
+    return true;
+
+  // synthesize it
+  result = verilog_synthesis(expr, module, get_message_handler(), ns);
+  if(result)
+    return true;
 
   // save some memory
   verilog_parser.clear();

src/verilog/verilog_synthesis.cpp

@@ -3110,3 +3110,65 @@ bool verilog_synthesis(
     ns, symbol_table, module, options, message_handler);
   return verilog_synthesis.typecheck_main();
 }
+
+/*******************************************************************\
+
+Function: verilog_synthesis
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool verilog_synthesis(
+  exprt &expr,
+  const irep_idt &module_identifier,
+  message_handlert &message_handler,
+  const namespacet &ns)
+{
+  optionst options;
+  symbol_tablet symbol_table;
+
+  const auto errors_before =
+    message_handler.get_message_count(messaget::M_ERROR);
+
+  verilog_synthesist verilog_synthesis(
+    ns, symbol_table, module_identifier, options, message_handler);
+
+  try
+  {
+    expr = verilog_synthesis.synth_expr(
+      expr, verilog_synthesist::symbol_statet::SYMBOL);
+  }
+
+  catch(int e)
+  {
+    verilog_synthesis.error();
+  }
+
+  catch(const char *e)
+  {
+    verilog_synthesis.error() << e << messaget::eom;
+  }
+
+  catch(const std::string &e)
+  {
+    verilog_synthesis.error() << e << messaget::eom;
+  }
+
+  catch(const verilog_typecheck_baset::errort &e)
+  {
+    if(e.what().empty())
+      verilog_synthesis.error();
+    else
+    {
+      verilog_synthesis.error().source_location = e.source_location();
+      verilog_synthesis.error() << e.what() << messaget::eom;
+    }
+  }
+
+  return message_handler.get_message_count(messaget::M_ERROR) != errors_before;
+}

src/verilog/verilog_synthesis.h

@@ -19,4 +19,10 @@ bool verilog_synthesis(
   message_handlert &,
   const optionst &);
 
+bool verilog_synthesis(
+  exprt &,
+  const irep_idt &module_identifier,
+  message_handlert &,
+  const namespacet &);
+
 #endif

src/verilog/verilog_synthesis_class.h

@@ -58,6 +58,16 @@ class verilog_synthesist:
 
   virtual void typecheck();
 
+  enum class symbol_statet
+  {
+    NONE,
+    SYMBOL,
+    CURRENT,
+    FINAL
+  };
+
+  [[nodiscard]] exprt synth_expr(exprt expr, symbol_statet symbol_state);
+
 protected:
   const optionst &options;
 
@@ -114,8 +124,12 @@ class verilog_synthesist:
   typedef std::list<exprt> invarst;
   invarst invars;
 
-  enum class constructt { INITIAL, ALWAYS, OTHER };
-  enum class symbol_statet { NONE, SYMBOL, CURRENT, FINAL };
+  enum class constructt
+  {
+    INITIAL,
+    ALWAYS,
+    OTHER
+  };
   constructt construct;
   event_guardt event_guard;
 
@@ -226,7 +240,6 @@ class verilog_synthesist:
   void synth_while(const verilog_whilet &);
   void synth_repeat(const verilog_repeatt &);
   void synth_function_call_or_task_enable(const verilog_function_callt &);
-  [[nodiscard]] exprt synth_expr(exprt expr, symbol_statet symbol_state);
   void synth_assign(const exprt &, bool blocking);
   void synth_assert(const verilog_assertt &);
   void synth_assume(const verilog_assumet &);