Verilog: set defines on command line

This allows setting SystemVerilog preprocessor defines on the command line
with -D.

Author: kroening

regression/verilog/preprocessor/cmdline_define1.desc

@@ -0,0 +1,10 @@
+CORE
+cmdline_define1.v
+--preprocess -D SOMETHING -D ELSE=foo
+^A$
+^foo$
+^EXIT=0$
+^SIGNAL=0$
+--
+^B$
+^PREPROCESSING FAILED$

regression/verilog/preprocessor/cmdline_define1.v

@@ -0,0 +1,7 @@
+`ifdef SOMETHING
+A
+`endif
+`ifdef OTHER
+B
+`endif
+`ELSE

src/ebmc/ebmc_parse_options.h

@@ -47,7 +47,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(random-traces)(trace-steps):(random-seed):(traces):"
         "(random-trace)(random-waveform)"
         "(liveness-to-safety)"
-        "I:(preprocess)(systemverilog)(vl2smv-extensions)",
+        "I:D:(preprocess)(systemverilog)(vl2smv-extensions)",
         argc,
         argv,
         std::string("EBMC ") + EBMC_VERSION),

src/ebmc/transition_system.cpp

@@ -113,6 +113,10 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
   options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
   options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions"));
 
+  // do -D
+  if(cmdline.isset('D'))
+    options.set_option("defines", cmdline.get_values('D'));
+
   language->set_language_options(options, message_handler);
 
   if(language->preprocess(infile, filename, std::cout, message_handler))
@@ -160,6 +164,10 @@ static bool parse(
   options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
   options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions"));
 
+  // do -D
+  if(cmdline.isset('D'))
+    options.set_option("defines", cmdline.get_values('D'));
+
   language.set_language_options(options, message_handler);
 
   message.status() << "Parsing " << filename << messaget::eom;

src/verilog/verilog_language.cpp

@@ -36,6 +36,7 @@ void verilog_languaget::set_language_options(
 {
   force_systemverilog = options.get_bool_option("force-systemverilog");
   vl2smv_extensions = options.get_bool_option("vl2smv-extensions");
+  initial_defines = options.get_list_option("defines");
 }
 
 /*******************************************************************\
@@ -103,7 +104,7 @@ bool verilog_languaget::preprocess(
   message_handlert &message_handler)
 {
   verilog_preprocessort preprocessor(
-    instream, outstream, message_handler, path);
+    instream, outstream, message_handler, path, initial_defines);
 
   try { preprocessor.preprocessor(); }
   catch(int e) { return true; }
@@ -186,7 +187,7 @@ bool verilog_languaget::typecheck(
   message.debug() << "Synthesis " << module << messaget::eom;
 
   if(verilog_synthesis(
-       symbol_table, module, parse_tree.standard, message_handler, options))
+       symbol_table, module, parse_tree.standard, message_handler, optionst{}))
     return true;
 
   return false;

src/verilog/verilog_language.h

@@ -85,17 +85,15 @@ class verilog_languaget:public languaget
   {
     return parse_tree;
   }
-  
-  optionst options;
 
   verilog_languaget() : parse_tree(verilog_standardt::NOT_SET)
   {
-    options.set_option("flatten_hierarchy", true);
   }
 
 protected:
   bool force_systemverilog = false;
   bool vl2smv_extensions = false;
+  std::list<std::string> initial_defines;
   verilog_parse_treet parse_tree;
 };
 

src/verilog/verilog_preprocessor.cpp

@@ -184,6 +184,24 @@ void verilog_preprocessort::preprocessor()
 {
   try
   {
+    // set up the initial defines
+    for(auto &define : initial_defines)
+    {
+      std::size_t equal_pos = define.find('=');
+      if(equal_pos == std::string::npos)
+      {
+        defines.insert(std::pair<std::string, definet>(define, definet{}));
+      }
+      else
+      {
+        std::string key = define.substr(0, equal_pos);
+        std::string value = define.substr(equal_pos + 1, std::string::npos);
+        auto tokens = verilog_preprocessor_tokenize(value);
+        defines.insert(
+          std::pair<std::string, definet>(key, definet{std::move(tokens)}));
+      }
+    }
+
     // the first context is the input file
     context_stack.emplace_back(false, &in, widen_if_needed(filename));
 

src/verilog/verilog_preprocessor.h

@@ -21,22 +21,31 @@ class verilog_preprocessort:public preprocessort
     std::istream &_in,
     std::ostream &_out,
     message_handlert &_message_handler,
-    const std::string &_filename):
-    preprocessort(_in, _out, _message_handler, _filename)
+    const std::string &_filename,
+    const std::list<std::string> &_initial_defines)
+    : preprocessort(_in, _out, _message_handler, _filename),
+      initial_defines(_initial_defines)
   {
     condition=true;
   }
 
   virtual ~verilog_preprocessort() { }
 
 protected:
+  // from the command line
+  const std::list<std::string> &initial_defines;
+
   using tokent = verilog_preprocessor_token_sourcet::tokent;
 
   struct definet
   {
     using parameterst = std::vector<std::string>;
     parameterst parameters;
     std::vector<tokent> tokens;
+    definet() = default;
+    explicit definet(std::vector<tokent> _tokens) : tokens(std::move(_tokens))
+    {
+    }
   };
 
   static std::string as_string(const std::vector<tokent> &);

src/verilog/verilog_preprocessor_tokenizer.cpp

@@ -114,3 +114,14 @@ void verilog_preprocessor_tokenizert::get_token_from_stream()
   token.kind = static_cast<verilog_preprocessor_tokenizert::tokent::kindt>(
     yyverilog_preprocessorlex());
 }
+
+std::vector<verilog_preprocessor_token_sourcet::tokent>
+verilog_preprocessor_tokenize(const std::string &text)
+{
+  std::istringstream instream(text);
+  verilog_preprocessor_tokenizert tokenizer(instream);
+  std::vector<verilog_preprocessor_token_sourcet::tokent> result;
+  while(!tokenizer.eof())
+    result.push_back(tokenizer.next_token());
+  return result;
+}

src/verilog/verilog_preprocessor_tokenizer.h

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "verilog_preprocessor_error.h"
 
+#include <vector>
+
 /// Note that the set of tokens recognised by the Verilog preprocessor
 /// differs from the set of tokens used by the main parser.
 
@@ -105,4 +107,8 @@ class verilog_preprocessor_tokenizert
   void get_token_from_stream() override;
 };
 
+// tokenize a given string
+std::vector<verilog_preprocessor_token_sourcet::tokent>
+verilog_preprocessor_tokenize(const std::string &);
+
 #endif // VERILOG_PREPROCESSOR_TOKENIZER_H