Merge pull request #514 from diffblue/verilog-standard-parse-tree

Verilog: standard version now tracked in parse tree

Author: kroening

src/verilog/scanner.l

@@ -71,34 +71,34 @@ static void preprocessor()
                              TOK_NON_TYPE_IDENTIFIER; \
   }
 #define KEYWORD(s, x) \
-  { if(PARSER.mode >= verilog_standardt::s) \
+  { if(PARSER.parse_tree.standard >= verilog_standardt::s) \
       return x; \
     else \
       IDENTIFIER(yytext); \
   }
 #define SYSTEM_VERILOG_OPERATOR(token, text) \
-  { if(PARSER.mode >= verilog_standardt::SV2005) \
+  { if(PARSER.parse_tree.standard >= verilog_standardt::SV2005) \
       return token; \
     else \
       yyverilogerror(text " is a System Verilog operator"); \
   }
 #define VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(x) \
-  { if(PARSER.mode >= verilog_standardt::SV2005 || \
-       PARSER.mode == verilog_standardt::V2005_SMV) \
+  { if(PARSER.parse_tree.standard >= verilog_standardt::SV2005 || \
+       PARSER.parse_tree.standard == verilog_standardt::V2005_SMV) \
       return x; \
     else \
       IDENTIFIER(yytext); \
   }
 #define VL2SMV_VERILOG_KEYWORD(x) \
-  { if(PARSER.mode == verilog_standardt::V2005_SMV) \
+  { if(PARSER.parse_tree.standard == verilog_standardt::V2005_SMV) \
       return x; \
     else \
       IDENTIFIER(yytext); \
   }
 #define VIS_OR_VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(x) \
-  { if(PARSER.mode >= verilog_standardt::SV2005 || \
-       PARSER.mode == verilog_standardt::V2005_SMV || \
-       PARSER.mode == verilog_standardt::V2005_VIS) \
+  { if(PARSER.parse_tree.standard >= verilog_standardt::SV2005 || \
+       PARSER.parse_tree.standard == verilog_standardt::V2005_SMV || \
+       PARSER.parse_tree.standard == verilog_standardt::V2005_VIS) \
       return x; \
     else \
       IDENTIFIER(yytext); \

src/verilog/verilog_language.cpp

@@ -55,23 +55,27 @@ bool verilog_languaget::parse(
   const std::string &path,
   message_handlert &message_handler)
 {
-  verilog_parsert verilog_parser;
-
   std::stringstream str;
 
   if(preprocess(instream, path, str, message_handler))
     return true;
 
+  verilog_standardt standard;
+
+  if(has_suffix(path, ".sv") || force_systemverilog)
+    standard = verilog_standardt::SV2023;
+  else if(vl2smv_extensions)
+    standard = verilog_standardt::V2005_SMV;
+  else
+    standard = verilog_standardt::V2005_SMV;
+
+  verilog_parsert verilog_parser(standard);
+
   verilog_parser.set_file(path);
   verilog_parser.in=&str;
   verilog_parser.log.set_message_handler(message_handler);
   verilog_parser.grammar=verilog_parsert::LANGUAGE;
 
-  if(has_suffix(path, ".sv") || force_systemverilog)
-    verilog_parser.mode = verilog_standardt::SV2023;
-  else if(vl2smv_extensions)
-    verilog_parser.mode = verilog_standardt::V2005_SMV;
-
   verilog_scanner_init();
 
   bool result=verilog_parser.parse();
@@ -182,7 +186,8 @@ bool verilog_languaget::typecheck(
   messaget message(message_handler);
   message.debug() << "Synthesis " << module << messaget::eom;
 
-  if(verilog_synthesis(symbol_table, module, message_handler, options))
+  if(verilog_synthesis(
+       symbol_table, module, parse_tree.standard, message_handler, options))
     return true;
 
   return false;
@@ -289,8 +294,10 @@ bool verilog_languaget::to_expr(
 
   std::istringstream i_preprocessed(code);
 
+  verilog_standardt standard = verilog_standardt::V2005;
+
   // parsing
-  verilog_parsert verilog_parser;
+  verilog_parsert verilog_parser(standard);
 
   verilog_parser.set_file("");
   verilog_parser.in=&i_preprocessed;
@@ -304,12 +311,12 @@ bool verilog_languaget::to_expr(
   expr.swap(verilog_parser.parse_tree.expr);
 
   // typecheck it
-  result = verilog_typecheck(expr, module, message_handler, ns);
+  result = verilog_typecheck(expr, module, standard, message_handler, ns);
   if(result)
     return true;
 
   // synthesize it
-  result = verilog_synthesis(expr, module, message_handler, ns);
+  result = verilog_synthesis(expr, module, standard, message_handler, ns);
   if(result)
     return true;
 

src/verilog/verilog_language.h

@@ -87,8 +87,8 @@ class verilog_languaget:public languaget
   }
 
   optionst options;
-  
-  verilog_languaget()
+
+  verilog_languaget() : parse_tree(verilog_standardt::NOT_SET)
   {
     options.set_option("flatten_hierarchy", true);
   }

src/verilog/verilog_parameterize_module.cpp

@@ -288,7 +288,8 @@ irep_idt verilog_typecheckt::parameterize_module(
 
   // recursive call
 
-  verilog_typecheckt verilog_typecheck(*new_symbol, symbol_table, get_message_handler());
+  verilog_typecheckt verilog_typecheck(
+    standard, *new_symbol, symbol_table, get_message_handler());
 
   if(verilog_typecheck.typecheck_main())
     throw 0;

src/verilog/verilog_parse_tree.h

@@ -9,16 +9,24 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_VERILOG_PARSE_TREE_H
 #define CPROVER_VERILOG_PARSE_TREE_H
 
-#include <list>
-#include <set>
-
 #include <util/string_hash.h>
 
 #include "verilog_module.h"
+#include "verilog_standard.h"
+
+#include <list>
+#include <set>
 
 class verilog_parse_treet
 {
 public:
+  explicit verilog_parse_treet(verilog_standardt _standard)
+    : standard(_standard)
+  {
+  }
+
+  verilog_standardt standard;
+
   class verilog_typedeft
   {
   public:
@@ -93,6 +101,7 @@ class verilog_parse_treet
     parse_tree.items.swap(items);
     parse_tree.expr.swap(expr);
     parse_tree.module_map.swap(module_map);
+    std::swap(parse_tree.standard, standard);
   }
 
   void modules_provided(

src/verilog/verilog_parser.cpp

@@ -29,12 +29,12 @@ verilog_parsert *verilog_parser_ptr = nullptr;
 
 \*******************************************************************/
 
-bool parse_verilog_file(const std::string &filename)
+bool parse_verilog_file(const std::string &filename, verilog_standardt standard)
 {
   std::ifstream in(widen_if_needed(filename));
   console_message_handlert console_message_handler;
 
-  verilog_parsert verilog_parser;
+  verilog_parsert verilog_parser(standard);
 
   verilog_parser.set_file(filename);
   verilog_parser.log.set_message_handler(console_message_handler);

src/verilog/verilog_parser.h

@@ -33,14 +33,12 @@ class verilog_parsert:public parsert
   typedef enum { LANGUAGE, EXPRESSION, TYPE } grammart;
   grammart grammar;
 
-  verilog_standardt mode;
-
   virtual bool parse()
   {
     return yyverilogparse()!=0;
   }
 
-  verilog_parsert() : mode(verilog_standardt::V2005_VIS)
+  explicit verilog_parsert(verilog_standardt standard) : parse_tree(standard)
   {
     PRECONDITION(verilog_parser_ptr == nullptr);
     verilog_parser_ptr = this;
@@ -131,7 +129,7 @@ class verilog_parsert:public parsert
   }
 };
 
-bool parse_verilog_file(const std::string &filename);
+bool parse_verilog_file(const std::string &filename, verilog_standardt);
 void verilog_scanner_init();
 
 #endif

src/verilog/verilog_standard.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, dkr@amazon.com
 // Verilog that the Cadence SMV model checker accepts.
 enum class verilog_standardt
 {
+  NOT_SET,
   V1995,
   V2001_NOCONFIG,
   V2001,

src/verilog/verilog_synthesis.cpp

@@ -334,7 +334,8 @@ exprt verilog_synthesist::expand_function_call(const function_call_exprt &call)
     else
     {
       // Attempt to constant fold.
-      verilog_typecheck_exprt verilog_typecheck_expr(ns, get_message_handler());
+      verilog_typecheck_exprt verilog_typecheck_expr(
+        standard, ns, get_message_handler());
       auto result =
         verilog_typecheck_expr.elaborate_constant_system_function_call(call);
       if(!result.is_constant())
@@ -1404,7 +1405,7 @@ void verilog_synthesist::synth_module_instance(
 
   // make sure the module is synthesized already
   verilog_synthesis(
-    symbol_table, module_identifier, get_message_handler(), options);
+    symbol_table, module_identifier, standard, get_message_handler(), options);
 
   for(auto &instance : statement.instances())
     expand_module_instance(module_symbol, instance, trans);
@@ -3496,12 +3497,13 @@ Function: verilog_synthesis
 bool verilog_synthesis(
   symbol_table_baset &symbol_table,
   const irep_idt &module,
+  verilog_standardt standard,
   message_handlert &message_handler,
   const optionst &options)
 {
   const namespacet ns(symbol_table);
   verilog_synthesist verilog_synthesis(
-    ns, symbol_table, module, options, message_handler);
+    standard, ns, symbol_table, module, options, message_handler);
   return verilog_synthesis.typecheck_main();
 }
 
@@ -3520,6 +3522,7 @@ Function: verilog_synthesis
 bool verilog_synthesis(
   exprt &expr,
   const irep_idt &module_identifier,
+  verilog_standardt standard,
   message_handlert &message_handler,
   const namespacet &ns)
 {
@@ -3530,7 +3533,7 @@ bool verilog_synthesis(
     message_handler.get_message_count(messaget::M_ERROR);
 
   verilog_synthesist verilog_synthesis(
-    ns, symbol_table, module_identifier, options, message_handler);
+    standard, ns, symbol_table, module_identifier, options, message_handler);
 
   try
   {

src/verilog/verilog_synthesis.h

@@ -13,15 +13,19 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/options.h>
 #include <util/symbol_table_base.h>
 
+#include "verilog_standard.h"
+
 bool verilog_synthesis(
   symbol_table_baset &,
   const irep_idt &module,
+  verilog_standardt,
   message_handlert &,
   const optionst &);
 
 bool verilog_synthesis(
   exprt &,
   const irep_idt &module_identifier,
+  verilog_standardt,
   message_handlert &,
   const namespacet &);