class interface for flex

src/verilog/Makefile

@@ -1,6 +1,7 @@
 SRC = aval_bval_encoding.cpp \
       convert_literals.cpp \
       expr2verilog.cpp \
+      flex_interface.cpp \
       sva_expr.cpp \
       typename.cpp \
       verilog_bits.cpp \

src/verilog/flex_interface.cpp

@@ -0,0 +1,34 @@
+/*******************************************************************\
+
+Module: Flex Interface
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "flex_interface.h"
+
+#include <util/invariant.h>
+
+#include <istream>
+
+std::size_t flex_interfacet::yy_input(char *buffer, std::size_t max_size)
+{
+  PRECONDITION(in != nullptr);
+
+  std::size_t result = 0;
+  while(result < max_size)
+  {
+    char ch;
+    if(!in->get(ch))
+      break; // eof
+    buffer[result++] = ch;
+    if(ch == '\n')
+    {
+      // We need to abort prematurely to enable
+      // switching input streams, e.g., for include files.
+      break;
+    }
+  }
+  return result;
+}

src/verilog/flex_interface.h

@@ -0,0 +1,54 @@
+/*******************************************************************\
+
+Module: Flex Interface
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_FLEX_INTERFACE_H
+#define CPROVER_FLEX_INTERFACE_H
+
+#include <cstddef>
+#include <iosfwd>
+#include <utility>
+
+// This is a C++ interface for a flex-generated tokenizer.
+// Defining our own avoids the issue with the different versions
+// of the FlexLexer.h, which needs to match the version of the
+// flex binary.
+
+class flex_interfacet
+{
+public:
+  virtual ~flex_interfacet()
+  {
+    destroy();
+  }
+
+  // the return type is hard-wired by flex
+  virtual int lex() = 0;
+
+  // for calling yylex_init
+  virtual void init()
+  {
+  }
+
+  // for calling yylex_destroy
+  virtual void destroy()
+  {
+  }
+
+  // to be called by the YY_INPUT macro, as follows
+  // #define YY_INPUT(buf, result, max_size)
+  // { result = flex_interface.yy_input(buf, max_size); }
+  std::size_t yy_input(char *buffer, std::size_t max_size);
+
+  // yytext and yyleng
+  using text_and_lengt = std::pair<char *, std::size_t>;
+  virtual text_and_lengt text_and_leng() = 0;
+
+  std::istream *in = nullptr;
+};
+
+#endif // CPROVER_FLEX_INTERFACE_H

src/verilog/verilog_preprocessor_tokenizer.cpp

@@ -81,38 +81,20 @@ auto verilog_preprocessor_token_sourcet::next_token() -> const tokent &
 
 verilog_preprocessor_tokenizert::verilog_preprocessor_tokenizert(
   std::istream &_in)
-  : in(_in)
 {
+  flex.in = &_in;
+  flex.init();
 }
 
-std::size_t
-verilog_preprocessor_tokenizert::yy_input(char *buffer, std::size_t max_size)
-{
-  std::size_t result = 0;
-  while(result < max_size)
-  {
-    char ch;
-    if(!in.get(ch))
-      break; // eof
-    buffer[result++] = ch;
-    if(ch == '\n')
-    {
-      // We need to abort prematurely to enable
-      // switching input streams on `include.
-      break;
-    }
-  }
-  return result;
-}
-
-int yyverilog_preprocessorlex();
-verilog_preprocessor_tokenizert *verilog_preprocessor_tokenizer;
+verilog_preprocessor_flext *verilog_preprocessor_flex;
 
 void verilog_preprocessor_tokenizert::get_token_from_stream()
 {
-  verilog_preprocessor_tokenizer = this;
-  token.kind = static_cast<verilog_preprocessor_tokenizert::tokent::kindt>(
-    yyverilog_preprocessorlex());
+  verilog_preprocessor_flex = &flex;
+  token.kind =
+    static_cast<verilog_preprocessor_tokenizert::tokent::kindt>(flex.lex());
+  auto [text, leng] = flex.text_and_leng();
+  token.text = std::string(text, leng);
 }
 
 std::vector<verilog_preprocessor_token_sourcet::tokent>

src/verilog/verilog_preprocessor_tokenizer.h

@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef VERILOG_PREPROCESSOR_TOKENIZER_H
 #define VERILOG_PREPROCESSOR_TOKENIZER_H
 
+#include "flex_interface.h"
 #include "verilog_preprocessor_error.h"
 
 #include <vector>
@@ -84,26 +85,23 @@ class verilog_preprocessor_token_sourcet
   virtual void get_token_from_stream() = 0;
 };
 
+class verilog_preprocessor_flext : public flex_interfacet
+{
+public:
+  int lex() override;
+  void init() override;
+  text_and_lengt text_and_leng() override;
+};
+
 class verilog_preprocessor_tokenizert
   : public verilog_preprocessor_token_sourcet
 {
 public:
-  explicit verilog_preprocessor_tokenizert(std::istream &_in);
+  explicit verilog_preprocessor_tokenizert(std::istream &);
 
-  // for flex
-  std::size_t yy_input(char *buffer, std::size_t max_size);
-  void text(const char *buffer, std::size_t len)
-  {
-    token.text = std::string(buffer, len);
-  }
-
-  void text(char ch)
-  {
-    token.text = std::string(1, ch);
-  }
+  verilog_preprocessor_flext flex;
 
 protected:
-  std::istream &in;
   void get_token_from_stream() override;
 };
 

src/verilog/verilog_preprocessor_tokenizer.l

@@ -13,13 +13,11 @@ static int isatty(int) { return 0; }
 
 #include "verilog_preprocessor_tokenizer.h"
 
-extern verilog_preprocessor_tokenizert *verilog_preprocessor_tokenizer;
+extern flex_interfacet *verilog_preprocessor_flex;
 using tokent = verilog_preprocessor_tokenizert::tokent;
 
-#define TOKENIZER (*verilog_preprocessor_tokenizer)
-
 #define YY_INPUT(buf, result, max_size) \
-  { result = TOKENIZER.yy_input(buf, max_size); }
+  { result = verilog_preprocessor_flex->yy_input(buf, max_size); }
 %}
 
 %s SLCOMMENT
@@ -33,13 +31,13 @@ String		\"(\\.|[^"\\])*\"
 
 <INITIAL>"//"		{ BEGIN SLCOMMENT; /* single-line comment */ }
 <INITIAL>"/*"           { BEGIN MLCOMMENT; /* multi-line comment */ }
-<INITIAL>{String}	{ TOKENIZER.text(yytext, yyleng); return tokent::STRING_LITERAL; }
-<INITIAL>{Identifier}	{ TOKENIZER.text(yytext, yyleng); return tokent::IDENTIFIER; }
-<INITIAL>.|\n		{ TOKENIZER.text(yytext[0]); return yytext[0]; /* anything else */ }
-<SLCOMMENT>\n		{ BEGIN INITIAL; TOKENIZER.text('\n'); return '\n'; }
+<INITIAL>{String}	{ return tokent::STRING_LITERAL; }
+<INITIAL>{Identifier}	{ return tokent::IDENTIFIER; }
+<INITIAL>.|\n		{ return yytext[0]; /* anything else */ }
+<SLCOMMENT>\n		{ BEGIN INITIAL; return '\n'; }
 <SLCOMMENT>.		{ /* just eat up */ }
 <SLCOMMENT><<EOF>>      { /* we allow that */ BEGIN INITIAL; }
-<MLCOMMENT>\n		{ TOKENIZER.text('\n'); return '\n'; }
+<MLCOMMENT>\n		{ return '\n'; }
 <MLCOMMENT>"*/"         { BEGIN INITIAL; /* comment done */ }
 <MLCOMMENT>.		{ /* just eat up */ }
 <MLCOMMENT><<EOF>>      { throw verilog_preprocessor_errort() << "EOF inside a comment"; }
@@ -48,8 +46,19 @@ String		\"(\\.|[^"\\])*\"
 
 int yywrap() { return 1; }
 
-void verilog_preprocessor_tokenizer_init()
+void verilog_preprocessor_flext::init()
 {
   YY_FLUSH_BUFFER;
   BEGIN INITIAL;
 }
+
+int verilog_preprocessor_flext::lex()
+{
+  return yylex();
+}
+
+verilog_preprocessor_flext::text_and_lengt
+verilog_preprocessor_flext::text_and_leng()
+{
+  return {yytext, yyleng};
+}