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/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 \
@@ -53,4 +54,5 @@ verilog_preprocessor_lex.yy.cpp: verilog_preprocessor_tokenizer.l
 # extra dependencies
 verilog_y.tab$(OBJEXT): verilog_y.tab.cpp verilog_y.tab.h
 verilog_lex.yy$(OBJEXT): verilog_y.tab.cpp verilog_lex.yy.cpp verilog_y.tab.h
+verilog_indexer.cpp: verilog_y.tab.h