Verilog: introduce the Verilog indexer

This adds a recusive decent parser for quicky indexing large quantities of
Verilog, tolerating parsing errors, for the purpose of creating overview
data very quickly.  A new executable, vlindex, is added to output it.

Author: kroening

regression/verilog/case/nested_case1.desc

@@ -0,0 +1,8 @@
+CORE
+nested_case1.v
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+^\[main.property.p1\] .* PROVED up to bound 0$
+--
+^warning: ignoring

regression/verilog/case/nested_case1.v

@@ -0,0 +1,17 @@
+module main(input x, input y);
+
+  reg result;
+
+  always @(x, y)
+    case(x)
+      0: result = 0;
+      1:
+        case(y)
+          1: result = 1;
+          0: result = 0;
+        endcase
+    endcase
+
+  always assert p1: result == (x && y);
+
+endmodule

src/Makefile

@@ -1,10 +1,10 @@
 DIRS = ebmc hw-cbmc temporal-logic trans-word-level trans-netlist \
-       verilog vhdl smvlang ic3 aiger
+       verilog vhdl smvlang ic3 aiger vlindex
 
 EBMC_DIR:=$(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
 CPROVER_DIR:=../lib/cbmc/src
 
-all: hw-cbmc.dir ebmc.dir
+all: hw-cbmc.dir ebmc.dir vlindex.dir
 
 .PHONY: $(patsubst %, %.dir, $(DIRS))
 $(patsubst %, %.dir, $(DIRS)):
@@ -21,6 +21,8 @@ ebmc.dir: trans-word-level.dir trans-netlist.dir verilog.dir vhdl.dir \
 hw-cbmc.dir: trans-word-level.dir trans-netlist.dir verilog.dir \
          vhdl.dir smvlang.dir cprover.dir temporal-logic.dir
 
+vlindex.dir: cprover.dir verilog.dir
+
 # building cbmc proper
 .PHONY: cprover.dir
 cprover.dir:

src/verilog/verilog_preprocessor.cpp

@@ -159,6 +159,8 @@ Function: verilog_preprocessort::preprocessor
 
 void verilog_preprocessort::preprocessor()
 {
+  bool error_found = false;
+
   try
   {
     // the first context is the input file
@@ -180,7 +182,18 @@ void verilog_preprocessort::preprocessor()
         // Read a token.
         auto token = tokenizer().next_token();
         if(token == '`')
-          directive();
+        {
+          try
+          {
+            directive();
+          }
+          catch(const verilog_preprocessor_errort &e)
+          {
+            error().source_location = context().make_source_location();
+            error() << e.what() << eom;
+            error_found = true;
+          }
+        }
         else if(condition)
         {
           auto a_it = context().define_arguments.find(token.text);
@@ -215,8 +228,11 @@ void verilog_preprocessort::preprocessor()
     if(!context_stack.empty())
       error().source_location = context().make_source_location();
     error() << e.what() << eom;
-    throw 0;
+    error_found = true;
   }
+
+  if(error_found)
+    throw 0;
 }
 
 /*******************************************************************\

src/vlindex/Makefile

@@ -0,0 +1,26 @@
+SRC = \
+      verilog_indexer.cpp \
+      vlindex_main.cpp \
+      vlindex_parse_options.cpp \
+      #empty line
+
+OBJ+= $(CPROVER_DIR)/util/util$(LIBEXT) \
+      $(CPROVER_DIR)/langapi/langapi$(LIBEXT) \
+      $(CPROVER_DIR)/big-int/big-int$(LIBEXT) \
+      ../verilog/verilog$(LIBEXT)
+
+include ../config.inc
+include ../common
+
+CLEANFILES = vlindex$(EXEEXT)
+
+all: vlindex$(EXEEXT)
+
+ifdef DEBUG
+CXXFLAGS += -DDEBUG
+endif
+
+###############################################################################
+
+vlindex$(EXEEXT): $(OBJ)
+	$(LINKBIN)