Verilog: introduce the Verilog indexer

src/ebmc/ebmc_parse_options.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/help_formatter.h>
 #include <util/string2int.h>
 
+#include <verilog/verilog_indexer.h>
+
 #include "bdd_engine.h"
 #include "diatest.h"
 #include "ebmc_base.h"
@@ -232,6 +234,9 @@ int ebmc_parse_optionst::doit()
     if(cmdline.isset("verilog-netlist"))
       return show_trans_verilog_netlist(cmdline, ui_message_handler);
 
+    if(cmdline.isset("verilog-index"))
+      return verilog_index();
+
     // get the transition system
     auto transition_system = get_transition_system(cmdline, ui_message_handler);
 

src/ebmc/ebmc_parse_options.h

@@ -36,6 +36,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(neural-liveness)(neural-engine):"
         "(reset):"
         "(version)(verilog-rtl)(verilog-netlist)"
+        "(verilog-index)"
         "(compute-interpolant)(interpolation)(interpolation-vmcai)"
         "(ic3)(property):(constr)(h)(new-mode)(aiger)"
         "(interpolation-word)(interpolator):(bdd)"

src/verilog/Makefile

@@ -3,6 +3,7 @@ SRC = expr2verilog.cpp \
       verilog_elaborate.cpp \
       verilog_expr.cpp \
       verilog_generate.cpp \
+      verilog_indexer.cpp \
       verilog_interfaces.cpp \
       verilog_interpreter.cpp \
       verilog_language.cpp \

src/verilog/verilog_indexer.cpp

@@ -0,0 +1,204 @@
+/*******************************************************************\
+
+Module: Verilog Indexer
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "verilog_indexer.h"
+
+#include <util/suffix.h>
+#include <util/unicode.h>
+
+#include "verilog_parser.h"
+#include "verilog_preprocessor.h"
+#include "verilog_y.tab.h"
+
+#include <algorithm>
+#include <fstream>
+#include <iosfwd>
+#include <iostream>
+#include <unordered_map>
+
+class verilog_indexert
+{
+public:
+  struct idt
+  {
+    using kindt = enum { MODULE, PACKAGE, CLASS, TYPEDEF, INSTANCE };
+    kindt kind;
+    irep_idt file_name;
+    bool is_module() const
+    {
+      return kind == MODULE;
+    }
+  };
+
+  // The keys are Verilog hierarchical identifiers
+  // without Verilog:: prefix, as this is Verilog only.
+  using id_mapt = std::unordered_map<irep_idt, idt>;
+  id_mapt id_map;
+
+  // a lookup helper
+  std::optional<const idt &> operator[](const irep_idt &) const;
+
+  /// index the given file
+  void operator()(const irep_idt &file_name);
+
+protected:
+  struct parsert
+  {
+    // grammar rules
+    void rDescription();
+    void rModule();
+
+    struct tokent
+    {
+      int kind;
+      std::string text;
+      bool is_eof() const
+      {
+        return kind == YYEOF;
+      }
+      bool is_identifier() const
+      {
+        return kind == TOK_NON_TYPE_IDENTIFIER;
+      }
+    };
+
+    const tokent &next_token()
+    {
+      peek();
+      peeked = false;
+      return peeked_token;
+    }
+
+    const tokent &peek();
+
+    bool peeked = false;
+    tokent peeked_token;
+  };
+
+  std::string preprocess(const std::string &file_name);
+};
+
+void verilog_indexert::operator()(const irep_idt &file_name)
+{
+  // run the preprocessor
+  const auto preprocessed_string = preprocess(id2string(file_name));
+  std::istringstream preprocessed(preprocessed_string);
+
+  // set up the tokenizer
+  verilog_parser.in=&preprocessed;
+  verilog_scanner_init();
+
+  // now parse
+  parsert parser;
+  parser.rDescription();
+}
+
+std::string verilog_indexert::preprocess(const std::string &file_name)
+{
+  std::stringstream preprocessed;
+
+  auto in_stream = std::ifstream(widen_if_needed(file_name));
+
+  if(!in_stream)
+  {
+    // We deliberately fail silently.
+    // Errors on invalid file names are expected to be raised
+    // later.
+    return std::string();
+  }
+
+  null_message_handlert message_handler;
+  verilog_preprocessort preprocessor(
+    in_stream, preprocessed, message_handler, file_name);
+
+  preprocessor.preprocessor();
+
+  return preprocessed.str();
+}
+
+// scanner interface
+int yyveriloglex();
+extern char *yyverilogtext;
+extern int yyverilogleng;
+
+const verilog_indexert::parsert::tokent &verilog_indexert::parsert::peek()
+{
+  if(!peeked)
+  {
+    peeked_token.kind = yyveriloglex();
+    peeked_token.text = std::string(yyverilogtext, yyverilogleng);
+    peeked = true;
+  }
+
+  return peeked_token;
+}
+
+void verilog_indexert::parsert::rDescription()
+{
+  if(next_token().kind != TOK_PARSE_LANGUAGE)
+    DATA_INVARIANT(false, "expected TOK_PARSE_LANGUAGE");
+
+  while(true)
+  {
+    auto &token = next_token();
+    if(token.is_eof())
+      break;
+    if(token.text == "module")
+      rModule();
+  }
+}
+
+void verilog_indexert::parsert::rModule()
+{
+  auto name = next_token();
+  if(name.is_identifier())
+    std::cout << "MODULE: " << name.text << '\n';
+}
+
+std::vector<std::filesystem::path> verilog_files()
+{
+  std::vector<std::filesystem::path> result;
+
+  for(auto &entry : std::filesystem::recursive_directory_iterator("."))
+    if(!is_directory(entry.path()))
+      if(has_suffix(entry.path(), ".v") || has_suffix(entry.path(), ".sv"))
+        result.push_back(entry.path());
+
+  return result;
+}
+
+int verilog_index()
+{
+  // First find all .v and .sv files
+  auto files = verilog_files();
+
+  // Now index them.
+  verilog_indexert indexer;
+
+  for(const auto &file : files)
+  {
+    indexer(std::string(file));
+  }
+
+  // Show the modules.
+  std::vector<irep_idt> modules;
+
+  for(auto &id : indexer.id_map)
+    if(id.second.is_module())
+      modules.push_back(id.first);
+
+  std::sort(
+    modules.begin(),
+    modules.end(),
+    [](const irep_idt &a, const irep_idt &b) { return a.compare(b) < 0; });
+
+  for(auto m : modules)
+    std::cout << "MODULE: " << m << '\n';
+
+  return 0;
+}

src/verilog/verilog_indexer.h

@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module: Verilog Indexer
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef VERILOG_INDEXER_H
+#define VERILOG_INDEXER_H
+
+/// Verilog allows modules, classes, packages, interfaces,
+/// tasks, functions, wires to be used before they are declared,
+/// which makes typing identifier tokens difficult.
+/// This maps identifiers to their kind and file,
+/// for the benefit of parsing/typechecking.
+
+int verilog_index();
+
+#endif // VERILOG_INDEXER_H