From 2dbb123654a81238da59ba44e899b3c1223b4409 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 5 Mar 2024 08:23:45 -0800 Subject: [PATCH] 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. --- .github/workflows/pull-request-checks.yaml | 8 + regression/verilog/case/nested_case1.desc | 8 + regression/verilog/case/nested_case1.v | 17 + regression/vlindex/Makefile | 6 + regression/vlindex/hierarchy1/hierarchy1.desc | 8 + regression/vlindex/hierarchy1/hierarchy1.v | 11 + regression/vlindex/modules1/modules1.desc | 9 + regression/vlindex/modules1/modules1.v | 7 + src/Makefile | 6 +- src/verilog/verilog_preprocessor.cpp | 20 +- src/vlindex/Makefile | 26 + src/vlindex/verilog_indexer.cpp | 1478 +++++++++++++++++ src/vlindex/verilog_indexer.h | 111 ++ src/vlindex/vlindex_main.cpp | 27 + src/vlindex/vlindex_parse_options.cpp | 120 ++ src/vlindex/vlindex_parse_options.h | 46 + 16 files changed, 1904 insertions(+), 4 deletions(-) create mode 100644 regression/verilog/case/nested_case1.desc create mode 100644 regression/verilog/case/nested_case1.v create mode 100644 regression/vlindex/Makefile create mode 100644 regression/vlindex/hierarchy1/hierarchy1.desc create mode 100644 regression/vlindex/hierarchy1/hierarchy1.v create mode 100644 regression/vlindex/modules1/modules1.desc create mode 100644 regression/vlindex/modules1/modules1.v create mode 100644 src/vlindex/Makefile create mode 100644 src/vlindex/verilog_indexer.cpp create mode 100644 src/vlindex/verilog_indexer.h create mode 100644 src/vlindex/vlindex_main.cpp create mode 100644 src/vlindex/vlindex_parse_options.cpp create mode 100644 src/vlindex/vlindex_parse_options.h diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index ec2e94bf6..f4680468b 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -51,6 +51,8 @@ jobs: run: make -C regression/verilog test - name: Run the verilog tests with Z3 run: make -C regression/verilog test-z3 + - name: Run the vlindex tests + run: make -C regression/vlindex test - name: Print ccache stats run: ccache -s @@ -103,6 +105,8 @@ jobs: run: make -C regression/verilog test - name: Run the verilog tests with Z3 run: make -C regression/verilog test-z3 + - name: Run the vlindex tests + run: make -C regression/vlindex test - name: Print ccache stats run: ccache -s - name: Upload the ebmc binary @@ -181,6 +185,8 @@ jobs: make -C regression/ebmc test - name: Run the verilog tests run: make -C regression/verilog test + - name: Run the vlindex tests + run: make -C regression/vlindex test - name: Print ccache stats run: ccache -s @@ -222,6 +228,8 @@ jobs: run: make -C regression/verilog test - name: Run the verilog tests with Z3 run: make -C regression/verilog test-z3 + - name: Run the vlindex tests + run: make -C regression/vlindex test - name: Print ccache stats run: ccache -s diff --git a/regression/verilog/case/nested_case1.desc b/regression/verilog/case/nested_case1.desc new file mode 100644 index 000000000..63cc96523 --- /dev/null +++ b/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 diff --git a/regression/verilog/case/nested_case1.v b/regression/verilog/case/nested_case1.v new file mode 100644 index 000000000..137140aec --- /dev/null +++ b/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 diff --git a/regression/vlindex/Makefile b/regression/vlindex/Makefile new file mode 100644 index 000000000..13c7f5719 --- /dev/null +++ b/regression/vlindex/Makefile @@ -0,0 +1,6 @@ +default: test + +TEST_PL = ../../lib/cbmc/regression/test.pl + +test: + @$(TEST_PL) -e -p -c ../../../src/vlindex/vlindex diff --git a/regression/vlindex/hierarchy1/hierarchy1.desc b/regression/vlindex/hierarchy1/hierarchy1.desc new file mode 100644 index 000000000..f63e4bbbf --- /dev/null +++ b/regression/vlindex/hierarchy1/hierarchy1.desc @@ -0,0 +1,8 @@ +CORE + +--hierarchy +^sub$ +^subsub$ +^top$ +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/vlindex/hierarchy1/hierarchy1.v b/regression/vlindex/hierarchy1/hierarchy1.v new file mode 100644 index 000000000..34b6769b0 --- /dev/null +++ b/regression/vlindex/hierarchy1/hierarchy1.v @@ -0,0 +1,11 @@ +module top; + sub instance1(); + sub instance2(); +endmodule + +module sub; + subsub instance3(); +endmodule + +module subsub; +endmodule diff --git a/regression/vlindex/modules1/modules1.desc b/regression/vlindex/modules1/modules1.desc new file mode 100644 index 000000000..1f8261381 --- /dev/null +++ b/regression/vlindex/modules1/modules1.desc @@ -0,0 +1,9 @@ +CORE + +--modules +^nested modules1.v line 5$ +^sub modules1.v line 4$ +^top modules1.v line 1$ +^EXIT=0$ +^SIGNAL=0$ + diff --git a/regression/vlindex/modules1/modules1.v b/regression/vlindex/modules1/modules1.v new file mode 100644 index 000000000..38d62cc8c --- /dev/null +++ b/regression/vlindex/modules1/modules1.v @@ -0,0 +1,7 @@ +module top; +endmodule + +module sub; + module nested; + endmodule +endmodule diff --git a/src/Makefile b/src/Makefile index 4d9700260..ab50be8dd 100644 --- a/src/Makefile +++ b/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)): @@ -25,6 +25,8 @@ endif 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: diff --git a/src/verilog/verilog_preprocessor.cpp b/src/verilog/verilog_preprocessor.cpp index d8ff5e843..5c7913755 100644 --- a/src/verilog/verilog_preprocessor.cpp +++ b/src/verilog/verilog_preprocessor.cpp @@ -182,6 +182,8 @@ Function: verilog_preprocessort::preprocessor void verilog_preprocessort::preprocessor() { + bool error_found = false; + try { // set up the initial defines @@ -221,7 +223,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); @@ -256,8 +269,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; } /*******************************************************************\ diff --git a/src/vlindex/Makefile b/src/vlindex/Makefile new file mode 100644 index 000000000..9ed4fac4f --- /dev/null +++ b/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) diff --git a/src/vlindex/verilog_indexer.cpp b/src/vlindex/verilog_indexer.cpp new file mode 100644 index 000000000..e5b2c341a --- /dev/null +++ b/src/vlindex/verilog_indexer.cpp @@ -0,0 +1,1478 @@ +/*******************************************************************\ + +Module: Verilog Indexer + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "verilog_indexer.h" + +#include +#include +#include +#include + +#include +#include +#include + +#include +#include +#include +#include +#include + +std::size_t verilog_indexert::total_number_of_files() const +{ + return file_map.size(); +} + +std::size_t verilog_indexert::total_number_of_symlinked_files() const +{ + std::size_t result = 0; + for(auto &[path, _] : file_map) + { + if(std::filesystem::is_symlink(id2string(path))) + result++; + } + return result; +} + +std::map +verilog_indexert::total_number_of() const +{ + std::map result; + for(auto &[_, file] : file_map) + for(auto &id : file.ids) + result[id.kind]++; + return result; +} + +std::size_t verilog_indexert::total_number_of_lines() const +{ + std::size_t sum = 0; + for(auto &[_, file] : file_map) + sum += file.number_of_lines; + return sum; +} + +class verilog_indexer_parsert +{ +public: + explicit verilog_indexer_parsert( + std::istream &in, + verilog_indexert &__indexer, + verilog_standardt standard, + message_handlert &message_handler) + : indexer(__indexer), verilog_parser(standard, message_handler) + { + verilog_parser.in = ∈ + verilog_parser.grammar = verilog_parsert::LANGUAGE; + } + + // grammar rules + void rDescription(); + +protected: + using idt = verilog_indexert::idt; + verilog_indexert &indexer; + irep_idt current_module; + + // modules, classes, primitives, packages, interfaces, configurations + void rModule(verilog_indexert::idt::kindt, int end_token); + void rImport(); + void rExtends(); + void rPorts(); + void rItem(); + void rBind(); + + void rCell(); + void rDesign(); + void rInterconnect(); + void rModport(); + void rConstruct(); // always, initial, ... + void rStatement(); + void rBegin(); + void rFor(); + void rForEach(); + void rForEver(); + void rFork(); + void rRepeat(); + void rWait(); + void rWhile(); + void rDisable(); + void rForce(); + void rRelease(); + void rReturn(); + void rIf(); + void rCase(); + void rCaseLabel(); + void rUniquePriority(); + void rParenExpression(); // (expression) + void rDeclaration(); // var, reg, wire, input, typedef, defparam ... + void rType(); + void rTypeOpt(); + void rStructUnion(); + void rEnum(); + void rDeclarators(); + void rTaskFunction(); // task ... endtask + void rConstraint(); // constraint ID { ... } + void rContinuousAssign(); // assign + void rGenerate(); // generate ... endgenerate + void rGenerateFor(); + void rGenerateIf(); + void rGenerateBegin(); + void rModuleInstance(); + void rLabeledItem(); + void rAssertAssumeCover(); + void rClocking(); + void rCoverGroup(); + void rProperty(); + void rSequence(); + void rSpecify(); + void skip_until(int token); + + struct tokent + { + int kind; + std::string text; + bool is_eof() const + { + return kind == 0; // EOF, flex magic number + } + bool is_identifier() const + { + return kind == TOK_NON_TYPE_IDENTIFIER || kind == TOK_TYPE_IDENTIFIER; + } + bool is_system_identifier() const + { + return kind == TOK_SYSIDENT; + } + bool operator==(int other) const + { + return kind == other; + } + bool operator!=(int other) const + { + return kind != other; + } + }; + + static bool may_be_type(const tokent &); + + const tokent &peek() + { + return peek1(); + } + + const tokent &next_token(); + const tokent &peek1(); + const tokent &peek2(); + + tokent peeked_token, extra_token; + bool have_peeked_token = false, have_extra_token = false; + + static tokent fetch_token(); + +public: + // used as scanner interface + verilog_parsert verilog_parser; +}; + +void verilog_indexert::operator()( + const irep_idt &file_name, + enum verilog_standardt standard) +{ + // run the preprocessor + const auto preprocessed_string = preprocess(id2string(file_name)); + std::istringstream preprocessed(preprocessed_string); + + // set up the tokenizer + console_message_handlert message_handler; + verilog_indexer_parsert parser( + preprocessed, *this, standard, message_handler); + verilog_scanner_init(); + + // now parse + parser.rDescription(); + file_map[file_name].number_of_lines = parser.verilog_parser.get_line_no(); +} + +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(); + } + + console_message_handlert message_handler; + verilog_preprocessort preprocessor( + in_stream, preprocessed, message_handler, file_name, {}); + + try + { + preprocessor.preprocessor(); + } + catch(...) + { + } + + return preprocessed.str(); +} + +const verilog_indexer_parsert::tokent &verilog_indexer_parsert::next_token() +{ + peek(); + have_peeked_token = false; + return peeked_token; +} + +// scanner interface +int yyveriloglex(); +extern char *yyverilogtext; +extern int yyverilogleng; + +verilog_indexer_parsert::tokent verilog_indexer_parsert::fetch_token() +{ + tokent result; + result.kind = yyveriloglex(); + result.text = std::string(yyverilogtext, yyverilogleng); + return result; +} + +const verilog_indexer_parsert::tokent &verilog_indexer_parsert::peek1() +{ + if(!have_peeked_token) + { + if(have_extra_token) + { + peeked_token = std::move(extra_token); + have_extra_token = false; + have_peeked_token = true; + } + else + { + // no token available + peeked_token = fetch_token(); + have_peeked_token = true; + } + } + + return peeked_token; +} + +const verilog_indexer_parsert::tokent &verilog_indexer_parsert::peek2() +{ + peek1(); + + if(!have_extra_token) + { + // Only one token available, but we want two. + extra_token = fetch_token(); + have_extra_token = true; + } + + return extra_token; +} + +void verilog_indexer_parsert::rDescription() +{ + if(peek().is_eof()) + return; // empty file + + if(next_token().kind != TOK_PARSE_LANGUAGE) + DATA_INVARIANT(false, "expected TOK_PARSE_LANGUAGE"); + + while(!peek().is_eof()) + { + rItem(); + } +} + +/// Covers the various 'definition-like' constructs in SystemVerilog, i.e., +/// modules, interfaces, classes, primitives, packages, configurations +void verilog_indexer_parsert::rModule( + verilog_indexert::idt::kindt kind, + int end_token) +{ + auto keyword = next_token(); // module, ... + + auto name = next_token(); + if(!name.is_identifier()) + return; // give up + + current_module = name.text; + + idt id; + id.kind = kind; + id.name = current_module; + id.module = current_module; + id.file_name = verilog_parser.get_file(); + id.line_number = verilog_parser.get_line_no(); + indexer.add(std::move(id)); + + if(peek() == TOK_IMPORT) + rImport(); + + if(peek() == TOK_EXTENDS) + rExtends(); + + rPorts(); + + // now look for the 'endmodule', given as end_token + while(!peek().is_eof()) + { + if(peek() == end_token) + { + next_token(); + break; // done with the module + } + else + rItem(); + } + + // optional : name + if(peek() == TOK_COLON) + { + next_token(); // : + next_token(); // identifier + } + + current_module = irep_idt(); +} + +void verilog_indexer_parsert::rItem() +{ + auto &token = peek(); + + if(token == TOK_MODULE) + rModule(verilog_indexert::idt::MODULE, TOK_ENDMODULE); + else if(token == TOK_CLASS) + rModule(verilog_indexert::idt::CLASS, TOK_ENDCLASS); + else if(token == TOK_PRIMITIVE) + rModule(verilog_indexert::idt::UDP, TOK_ENDPRIMITIVE); + else if(token == TOK_INTERFACE) + rModule(verilog_indexert::idt::INTERFACE, TOK_ENDINTERFACE); + else if(token == TOK_PACKAGE) + rModule(verilog_indexert::idt::PACKAGE, TOK_ENDPACKAGE); + else if(token == TOK_CONFIG) + rModule(verilog_indexert::idt::CONFIG, TOK_CONFIG); + else if(token == TOK_PROPERTY) + rProperty(); + else if(token == TOK_SEQUENCE) + rSequence(); + else if(token == TOK_SPECIFY) + rSpecify(); + else if(token == TOK_MODPORT) + rModport(); + else if(token == TOK_BIND) + rBind(); + else if(token == TOK_CELL) + rCell(); + else if(token == TOK_DESIGN) + rDesign(); + else if(token == TOK_INTERCONNECT) + rInterconnect(); + else if( + token == TOK_ALWAYS || token == TOK_ALWAYS_FF || token == TOK_ALWAYS_COMB || + token == TOK_ALWAYS_LATCH || token == TOK_FINAL || token == TOK_INITIAL) + { + rConstruct(); + } + else if(token == TOK_DEFAULT) + { + if(peek2() == TOK_CLOCKING) + rClocking(); + else if(peek2() == TOK_DISABLE) + rDisable(); + else + next_token(); + } + else if(token == TOK_CLOCKING) + { + rClocking(); + } + else if(token == TOK_COVERGROUP) + { + rCoverGroup(); + } + else if(may_be_type(token)) + { + rDeclaration(); + } + else if( + token == TOK_VAR || token == TOK_WIRE || token == TOK_TRI0 || + token == TOK_TRI1 || token == TOK_INPUT || token == TOK_INOUT || + token == TOK_OUTPUT || token == TOK_GENVAR || token == TOK_TYPEDEF || + token == TOK_PARAMETER || token == TOK_LOCALPARAM || + token == TOK_DEFPARAM || token == TOK_SUPPLY0 || token == TOK_SUPPLY1 || + token == TOK_LET || token == TOK_ALIAS || token == TOK_RAND || + token == TOK_RANDC || token == TOK_LOCAL || token == TOK_PROTECTED || + token == TOK_AUTOMATIC || token == TOK_CONST) + { + rDeclaration(); + } + else if(token == TOK_STATIC) + { + if(peek2() == TOK_CONSTRAINT) + rConstraint(); + else + rDeclaration(); + } + else if(token == TOK_EXPORT) + { + if(peek2() == TOK_FUNCTION) + rTaskFunction(); + else + { + skip_until(';'); + } + } + else if( + token == TOK_FUNCTION || token == TOK_TASK || token == TOK_VIRTUAL || + token == TOK_EXTERN) + { + rTaskFunction(); + } + else if(token == TOK_CONSTRAINT) + rConstraint(); + else if(token == TOK_ASSIGN) + rContinuousAssign(); + else if(token == TOK_FORK) + rFork(); + else if(token == TOK_WAIT || token == TOK_WAIT_ORDER) + rWait(); + else if(token == TOK_IF) + rGenerateIf(); + else if(token == TOK_BEGIN) + rGenerateBegin(); + else if(token == TOK_FOR) + rGenerateFor(); + else if(token == TOK_GENERATE) + rGenerate(); + else if(token == TOK_ASSERT || token == TOK_ASSUME || token == TOK_COVER) + rAssertAssumeCover(); + else if( + token == TOK_BUF || token == TOK_OR || token == TOK_NOR || + token == TOK_XOR || token == TOK_XNOR || token == TOK_AND || + token == TOK_NAND || token == TOK_NOT || token == TOK_BUFIF0 || + token == TOK_BUFIF1 || token == TOK_TRAN || token == TOK_TRANIF0 || + token == TOK_TRANIF1 || token == TOK_RTRAN || token == TOK_RTRANIF0 || + token == TOK_RTRANIF1 || token == TOK_PULLUP || token == TOK_PULLDOWN) + { + rModuleInstance(); + } + else if(token.is_identifier()) + { + // Type identifier (for declaration), label, module instance. + // We look one further token ahead to disambiguate. + auto &second_token = peek2(); + if(second_token == '#' || second_token == '(') + rModuleInstance(); + else if(second_token == TOK_COLON) + rLabeledItem(); + else + { + // Might be one of + // type identifier; + // module instance(...); + rDeclaration(); + } + } + else if(token == TOK_TIMEUNIT) + { + skip_until(';'); + } + else if(token == TOK_TIMEPRECISION) + { + skip_until(';'); + } + else if(token == ';') + { + // the empty item + next_token(); + } + else if(token.is_system_identifier()) + { + // $error... + skip_until(';'); + } + else if(token == TOK_IMPORT) + { + skip_until(';'); + } + else if(token == '(') + { + // possibly a macro that wasn't found + std::cout << "LPAREN: " << verilog_parser.get_file() << ':' + << verilog_parser.get_line_no() << ' ' << token.text << "\n"; + rParenExpression(); + } + else + { + // something else + std::cout << "ELSE: " << verilog_parser.get_file() << ':' + << verilog_parser.get_line_no() << ' ' << token.text << "\n"; + next_token(); + } +} + +void verilog_indexer_parsert::rImport() +{ + next_token(); // import + skip_until(';'); +} + +void verilog_indexer_parsert::rExtends() +{ + next_token(); // extends + next_token(); // identifier +} + +void verilog_indexer_parsert::rPorts() +{ + skip_until(';'); +} + +void verilog_indexer_parsert::rConstruct() +{ + auto keyword = next_token(); // initial, final, always, always_comb, ... + rStatement(); +} + +void verilog_indexer_parsert::rClocking() +{ + if(peek() == TOK_DEFAULT) + next_token(); // default + + if(next_token() != TOK_CLOCKING) + return; + + skip_until(TOK_ENDCLOCKING); + + if(peek() == TOK_COLON) + { + // optional label + next_token(); // : + next_token(); // identifier + } +} + +void verilog_indexer_parsert::rCoverGroup() +{ + next_token(); // covergroup + skip_until(TOK_ENDGROUP); + + if(peek() == TOK_COLON) + { + // optional label + next_token(); // : + next_token(); // identifier + } +} + +void verilog_indexer_parsert::rStatement() +{ + auto first = peek(); + if(first == TOK_ASSERT || first == TOK_ASSUME || first == TOK_COVER) + rAssertAssumeCover(); + else if(first == TOK_BEGIN) + rBegin(); + else if(first == TOK_CASE || first == TOK_CASEX || first == TOK_CASEZ) + rCase(); + else if(first == TOK_UNIQUE || first == TOK_UNIQUE0 || first == TOK_PRIORITY) + rUniquePriority(); + else if(first == TOK_FOR) + rFor(); + else if(first == TOK_FOREACH) + rForEach(); + else if(first == TOK_FOREVER) + rForEver(); + else if(first == TOK_REPEAT) + rRepeat(); + else if(first == TOK_WHILE) + rWhile(); + else if(first == TOK_IF) + rIf(); + else if(first == TOK_DISABLE) + rDisable(); + else if(first == TOK_FORCE) + rForce(); + else if(first == TOK_RELEASE) + rRelease(); + else if(first == TOK_RETURN) + rReturn(); + else if(first == '@') + { + next_token(); // @ + if(peek() == '(') + rParenExpression(); + else if(peek() == TOK_PARENASTERIC) // (* + { + next_token(); + if(peek() == ')') + next_token(); + } + else + next_token(); + + rStatement(); + } + else if(first == '#') + { + // delay + next_token(); // # + next_token(); // delay value + rStatement(); + } + else if(first == ';') + { + // skip + next_token(); + } + else + { + // Label? + if(first.is_identifier() && peek2() == TOK_COLON) + { + next_token(); // identifier + next_token(); // : + rStatement(); + } + else + { + // e.g., declarations, assignments, ... + skip_until(';'); + } + } +} + +void verilog_indexer_parsert::rAssertAssumeCover() +{ + next_token(); // assert, assume, ... + rParenExpression(); + if(peek() == TOK_ELSE) + { + next_token(); // else + rStatement(); + } + else + skip_until(';'); +} + +void verilog_indexer_parsert::rBegin() +{ + next_token(); // begin + + if(peek() == TOK_COLON) + { + // optional block label + next_token(); // : + next_token(); // identifier + } + + while(true) + { + if(peek().is_eof()) + return; + + if(peek() == TOK_END) + { + next_token(); // end + break; + } + + rStatement(); + } + + if(peek() == TOK_COLON) + { + // optional block label + next_token(); // : + next_token(); // identifier + } +} + +void verilog_indexer_parsert::rFork() +{ + next_token(); // fork + + if(peek() == TOK_COLON) + { + // optional block label + next_token(); // : + next_token(); // identifier + } + + while(!peek().is_eof()) + { + if(peek() == TOK_JOIN || peek() == TOK_JOIN_ANY || peek() == TOK_JOIN_NONE) + { + next_token(); + break; + } + + rItem(); + } + + if(peek() == TOK_COLON) + { + // optional block label + next_token(); // : + next_token(); // identifier + } +} + +void verilog_indexer_parsert::rWait() +{ + next_token(); // wait, wait_order + + if(peek() == '(') + { + rParenExpression(); + rStatement(); + } + else if(peek() == TOK_FORK) + { + next_token(); // fork + if(next_token() != ';') + return; // error + } + else + return; // error +} + +void verilog_indexer_parsert::rFor() +{ + next_token(); // for + rParenExpression(); + rStatement(); +} + +void verilog_indexer_parsert::rForEach() +{ + next_token(); // foreach + rParenExpression(); + rStatement(); +} + +void verilog_indexer_parsert::rForEver() +{ + next_token(); // forever + rStatement(); +} + +void verilog_indexer_parsert::rRepeat() +{ + next_token(); // repeat + rParenExpression(); + rStatement(); +} + +void verilog_indexer_parsert::rWhile() +{ + next_token(); // while + rParenExpression(); + rStatement(); +} + +void verilog_indexer_parsert::rDisable() +{ + if(peek() == TOK_DEFAULT) + next_token(); // default + + next_token(); // disable + skip_until(';'); +} + +void verilog_indexer_parsert::rReturn() +{ + next_token(); // return + skip_until(';'); +} + +void verilog_indexer_parsert::rBind() +{ + next_token(); // bind + skip_until(';'); +} + +void verilog_indexer_parsert::rForce() +{ + next_token(); // force + skip_until(';'); +} + +void verilog_indexer_parsert::rRelease() +{ + next_token(); // release + skip_until(';'); +} + +void verilog_indexer_parsert::rModport() +{ + next_token(); // modport + skip_until(';'); +} + +void verilog_indexer_parsert::rCell() +{ + next_token(); // cell + skip_until(';'); +} + +void verilog_indexer_parsert::rDesign() +{ + next_token(); // design + skip_until(';'); +} + +void verilog_indexer_parsert::rInterconnect() +{ + next_token(); // interconnect + skip_until(';'); +} + +void verilog_indexer_parsert::rIf() +{ + next_token(); // if + rParenExpression(); + rStatement(); + if(peek() == TOK_ELSE) + { + next_token(); + rStatement(); + } +} + +void verilog_indexer_parsert::rCase() +{ + next_token(); // case, casex, ... + rParenExpression(); + while(true) + { + if(peek().is_eof()) + return; + if(peek() == TOK_ENDCASE) + { + next_token(); + return; + } + rCaseLabel(); + rStatement(); + } +} + +void verilog_indexer_parsert::rCaseLabel() +{ + skip_until(TOK_COLON); +} + +void verilog_indexer_parsert::rUniquePriority() +{ + // unique case/if ... + // unique0 case/if ... + // priority case/if ... + auto first = next_token(); // unique, unique0, priority + if(peek() == TOK_IF) + rIf(); + else if(peek() == TOK_CASE || peek() == TOK_CASEZ || peek() == TOK_CASEX) + rCase(); + else + { + // error + } +} + +void verilog_indexer_parsert::rParenExpression() +{ + auto first = next_token(); + if(first != '(') + return; + std::size_t count = 1; + + while(true) + { + auto token = next_token(); + if(token.is_eof()) + return; + else if(token == '(') + count++; + else if(token == ')') + { + if(count == 1) + return; + count--; + } + } +} + +void verilog_indexer_parsert::rDeclaration() +{ + if(peek() == TOK_PROTECTED) + { + next_token(); // protected + } + + if(peek() == TOK_AUTOMATIC) + { + next_token(); // automatic + } + + if(peek() == TOK_CONST) + { + next_token(); // const + } + + auto &token = peek(); + + if(token == TOK_TYPEDEF) + { + next_token(); // typedef + rType(); + } + else if(token == TOK_RAND || token == TOK_RANDC) + { + next_token(); // rand + rType(); + } + else if(token == TOK_LOCAL) + { + next_token(); // local + rType(); + } + else if(token == TOK_LET) + { + next_token(); // let + rTypeOpt(); + } + else if(token == TOK_ALIAS) + { + next_token(); // alias + rTypeOpt(); + } + else if(token == TOK_PARAMETER || token == TOK_LOCALPARAM) + { + next_token(); + rTypeOpt(); + } + else if( + token == TOK_VAR || token == TOK_INPUT || token == TOK_OUTPUT || + token == TOK_INOUT || token == TOK_WIRE || token == TOK_TRI0 || + token == TOK_TRI1) + { + next_token(); + rTypeOpt(); + } + else + { + rType(); + } + + rDeclarators(); +} + +void verilog_indexer_parsert::rType() +{ + auto &token = peek(); + if(token == TOK_STRUCT || token == TOK_UNION) + { + rStructUnion(); + } + else if(token == TOK_ENUM) + { + rEnum(); + } + else + { + next_token(); + } +} + +bool verilog_indexer_parsert::may_be_type(const tokent &token) +{ + return token == TOK_REG || token == TOK_GENVAR || token == TOK_ENUM || + token == TOK_INTEGER || token == TOK_REALTIME || token == TOK_REAL || + token == TOK_TIME || token == TOK_SIGNED || token == TOK_UNSIGNED || + token == TOK_SHORTREAL || token == TOK_BYTE || token == TOK_SHORTINT || + token == TOK_LONGINT || token == TOK_LOGIC || token == TOK_BIT || + token == TOK_INT || token == TOK_STRUCT || token == TOK_UNION || + token == TOK_STRING || token == TOK_VOID || token == TOK_EVENT || + token == TOK_CHANDLE; +} + +void verilog_indexer_parsert::rTypeOpt() +{ + auto &token = peek(); + if(may_be_type(token)) + rType(); +} + +void verilog_indexer_parsert::rEnum() +{ + next_token(); + skip_until('{'); + skip_until('}'); +} + +void verilog_indexer_parsert::rStructUnion() +{ + next_token(); // struct or union + skip_until('{'); + while(!peek().is_eof() && peek() != '}') + { + rType(); + rDeclarators(); + } + skip_until('}'); +} + +void verilog_indexer_parsert::rDeclarators() +{ + skip_until(';'); +} + +void verilog_indexer_parsert::rTaskFunction() +{ + if(peek() == TOK_VIRTUAL) + next_token(); // virtual + + if(peek() == TOK_EXTERN) + next_token(); // extern + + if(peek() == TOK_EXPORT) + { + next_token(); // export + next_token(); // string literal + } + + auto tf_keyword = next_token(); // function or task + + if(peek() == TOK_AUTOMATIC) + next_token(); // automatic + + // optional return type + rTypeOpt(); + + auto name = next_token(); // name or new + + { + idt id; + + if(tf_keyword == TOK_FUNCTION) + id.kind = idt::FUNCTION; + else + id.kind = idt::TASK; + + id.name = name.text; + id.module = current_module; + id.file_name = verilog_parser.get_file(); + id.line_number = verilog_parser.get_line_no(); + indexer.add(std::move(id)); + } + + if(tf_keyword == TOK_FUNCTION) + skip_until(TOK_ENDFUNCTION); + else + skip_until(TOK_ENDTASK); + + // optional label + if(peek() == TOK_COLON) + { + next_token(); // : + next_token(); // identifier + } +} + +void verilog_indexer_parsert::rConstraint() +{ + if(peek() == TOK_STATIC) + { + next_token(); // static + } + + next_token(); // constraint + + next_token(); // identifier + + if(next_token() != '{') // onstraint_block + return; // error + + skip_until('}'); +} + +void verilog_indexer_parsert::rContinuousAssign() +{ + skip_until(';'); +} + +void verilog_indexer_parsert::rGenerate() +{ + skip_until(TOK_ENDGENERATE); +} + +void verilog_indexer_parsert::rGenerateFor() +{ + next_token(); // for + rParenExpression(); + rItem(); +} + +void verilog_indexer_parsert::rGenerateIf() +{ + next_token(); // if + rParenExpression(); + rItem(); + if(peek() == TOK_ELSE) + { + next_token(); + rItem(); + } +} + +void verilog_indexer_parsert::rGenerateBegin() +{ + next_token(); // begin + + if(peek() == TOK_COLON) + { + // optional block label + next_token(); // : + next_token(); // identifier + } + + while(true) + { + if(peek().is_eof()) + return; + + if(peek() == TOK_END) + { + next_token(); // end + return; + } + + rItem(); + } +} + +void verilog_indexer_parsert::rProperty() +{ + skip_until(TOK_ENDPROPERTY); +} + +void verilog_indexer_parsert::rSequence() +{ + skip_until(TOK_ENDSEQUENCE); +} + +void verilog_indexer_parsert::rSpecify() +{ + skip_until(TOK_ENDSPECIFY); +} + +void verilog_indexer_parsert::skip_until(int token) +{ + while(true) + { + if(peek().is_eof()) + return; + if(next_token() == token) + return; + } +} + +void verilog_indexer_parsert::rModuleInstance() +{ + auto first = next_token(); // module, class or primitive name + + if(peek() == '#') + { + // Module instance with parameters. + next_token(); // # + if(peek() == '(') + { + // parameter values + rParenExpression(); + } + else + { + next_token(); // parameter value + } + } + + // the instance name is optional + if(peek() != '[' && peek() != '(') + { + auto second = next_token(); // instance name + + idt id; + id.kind = verilog_indexert::idt::INSTANCE; + id.name = second.text; + id.module = current_module; + id.file_name = verilog_parser.get_file(); + id.line_number = verilog_parser.get_line_no(); + id.instantiated_module = first.text; + indexer.add(std::move(id)); + } + + if(peek() == '[') // instance range + skip_until(']'); + + if(peek() == '(') // connections + { + next_token(); // ( + } + else if(peek() == '=') // initialization for classes + { + next_token(); // = + } + else + return; // error + + skip_until(';'); +} + +void verilog_indexer_parsert::rLabeledItem() +{ + // label followed by assert/assume/cover + next_token(); // label + if(next_token() != TOK_COLON) // : + return; + skip_until(';'); +} + +std::vector verilog_files() +{ + std::vector result; + + auto current = std::filesystem::current_path(); + + for(auto &entry : std::filesystem::recursive_directory_iterator(current)) + if(!is_directory(entry.path())) + if( +#ifdef _WIN32 + has_suffix(narrow(entry.path()), ".v") || + has_suffix(narrow(entry.path()), ".sv")) +#else + has_suffix(entry.path(), ".v") || has_suffix(entry.path(), ".sv")) +#endif + { + result.push_back(std::filesystem::relative(entry.path())); + } + + return result; +} + +void show_module_hierarchy_rec( + const irep_idt &module, + std::size_t indent, + const verilog_indexert::instancest &instances) +{ + auto m_it = instances.find(module); + if(m_it != instances.end()) + { + // We output in the order found in the file, + // but show the sub-instances of any module only once. + std::unordered_set done; + for(auto &instance : m_it->second) + { + std::cout << std::string(indent * 2, ' ') << instance.instantiated_module + << ' ' << instance.name << '\n'; + if(done.insert(instance.instantiated_module).second) + show_module_hierarchy_rec( + instance.instantiated_module, indent + 1, instances); + } + } +} + +void sort_alphabetically(std::vector &ids) +{ + using idt = verilog_indexert::idt; + std::sort( + ids.begin(), + ids.end(), + [](const idt &a, const idt &b) { return a.name.compare(b.name) < 0; }); +} + +void show_module_hierarchy(const verilog_indexert &indexer) +{ + std::unordered_set instantiated_modules; + // module -> list of instances + verilog_indexert::instancest instances; + + for(const auto &[_, file] : indexer.file_map) + for(const auto &id : file.ids) + if(id.is_instance()) + { + instantiated_modules.insert(id.instantiated_module); + instances[id.module].push_back(id); + } + + // identify root modules + std::vector root_modules; + for(auto &[_, file] : indexer.file_map) + for(const auto &id : file.ids) + if( + id.is_module() && + instantiated_modules.find(id.name) == instantiated_modules.end()) + { + root_modules.push_back(id.name); + } + + // sort those alphabetically + std::sort( + root_modules.begin(), + root_modules.end(), + [](const irep_idt &a, const irep_idt &b) { return a.compare(b) < 0; }); + + for(auto &root : root_modules) + { + std::cout << root << '\n'; + show_module_hierarchy_rec(root, 1, instances); + } +} + +void show_kind( + verilog_indexert::idt::kindt kind, + const verilog_indexert &indexer) +{ + std::vector ids; + + for(const auto &[_, file] : indexer.file_map) + for(const auto &id : file.ids) + if(id.kind == kind) + ids.push_back(id); + + sort_alphabetically(ids); + + for(const auto &id : ids) + { + std::cout << id.name << ' ' << id.file_name << " line " << id.line_number + << '\n'; + } +} + +int verilog_index(const cmdlinet &cmdline) +{ + // First find all .v and .sv files + auto files = verilog_files(); + + // Now index them. + verilog_indexert indexer; + + verilog_standardt standard = [&cmdline]() + { + if(cmdline.isset("1800-2017")) + return verilog_standardt::SV2017; + else if(cmdline.isset("1800-2012")) + return verilog_standardt::SV2012; + else if(cmdline.isset("1800-2009")) + return verilog_standardt::SV2009; + else if(cmdline.isset("1800-2005")) + return verilog_standardt::SV2005; + else if(cmdline.isset("1364-2005")) + return verilog_standardt::V2005; + else if(cmdline.isset("1364-2001")) + return verilog_standardt::V2001; + else if(cmdline.isset("1364-2001-noconfig")) + return verilog_standardt::V2001_NOCONFIG; + else if(cmdline.isset("1364-1995")) + return verilog_standardt::V1995; + else // default + return verilog_standardt::SV2017; + }(); + + for(const auto &file : files) + { +#ifdef _WIN32 + indexer(narrow(file), standard); +#else + indexer(std::string(file), standard); +#endif + } + + if(cmdline.isset("hierarchy")) + { + show_module_hierarchy(indexer); + } + else if(cmdline.isset("modules")) + { + // Show the modules. + show_kind(verilog_indexert::idt::kindt::MODULE, indexer); + } + else if(cmdline.isset("packages")) + { + // Show the packages. + show_kind(verilog_indexert::idt::kindt::PACKAGE, indexer); + } + else if(cmdline.isset("interfaces")) + { + // Show the interfaces. + show_kind(verilog_indexert::idt::kindt::INTERFACE, indexer); + } + else if(cmdline.isset("classes")) + { + // Show the interfaces. + show_kind(verilog_indexert::idt::kindt::CLASS, indexer); + } + else if(cmdline.isset("udps")) + { + // Show the interfaces. + show_kind(verilog_indexert::idt::kindt::UDP, indexer); + } + else if(cmdline.isset("instances")) + { + // Show the module instances. + show_kind(verilog_indexert::idt::kindt::INSTANCE, indexer); + } + else if(cmdline.isset("functions")) + { + // Show the functions. + show_kind(verilog_indexert::idt::kindt::FUNCTION, indexer); + } + else if(cmdline.isset("tasks")) + { + // Show the module instances. + show_kind(verilog_indexert::idt::kindt::TASK, indexer); + } + else + { + auto total_number_of = indexer.total_number_of(); + using idt = verilog_indexert::idt; + std::cout << "Number of files...........: " + << indexer.total_number_of_files() << '\n'; + std::cout << "Number of symlinked files.: " + << indexer.total_number_of_symlinked_files() << '\n'; + std::cout << "Number of lines...........: " + << indexer.total_number_of_lines() << '\n'; + std::cout << "Number of modules.........: " << total_number_of[idt::MODULE] + << '\n'; + std::cout << "Number of UDPs............: " << total_number_of[idt::UDP] + << '\n'; + std::cout << "Number of classes.........: " << total_number_of[idt::CLASS] + << '\n'; + std::cout << "Number of packages........: " << total_number_of[idt::PACKAGE] + << '\n'; + std::cout << "Number of interfaces......: " + << total_number_of[idt::INTERFACE] << '\n'; + std::cout << "Number of functions.......: " + << total_number_of[idt::FUNCTION] << '\n'; + std::cout << "Number of tasks...........: " << total_number_of[idt::TASK] + << '\n'; + std::cout << "Number of module instances: " + << total_number_of[idt::INSTANCE] << '\n'; + std::cout << "Number of configurations..: " << total_number_of[idt::CONFIG] + << '\n'; + } + + return 0; +} diff --git a/src/vlindex/verilog_indexer.h b/src/vlindex/verilog_indexer.h new file mode 100644 index 000000000..6f32fa32a --- /dev/null +++ b/src/vlindex/verilog_indexer.h @@ -0,0 +1,111 @@ +/*******************************************************************\ + +Module: Verilog Indexer + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef VERILOG_INDEXER_H +#define VERILOG_INDEXER_H + +#include + +#include + +#include +#include + +/// This is a catalogue of Verilog identifiers by file. +/// See 1800-2017 Sec 3.13 Name spaces for an overview of +/// the name spaces. +class verilog_indexert +{ +public: + struct idt + { + using kindt = enum { + UNKNOWN, + PACKAGE, + MODULE, + UDP, + INTERFACE, + CLASS, + CONFIG, + TYPEDEF, + FUNCTION, + TASK, + INSTANCE, + BLOCK, + NET, + VARIABLE, + PARAMETER, + PORT + }; + kindt kind = UNKNOWN; + // identifier or identifier.identifier + irep_idt name; + irep_idt file_name; + irep_idt module; + std::size_t line_number; + irep_idt instantiated_module; // for INSTANCE + bool is_module() const + { + return kind == MODULE; + } + bool is_package() const + { + return kind == PACKAGE; + } + bool is_class() const + { + return kind == CLASS; + } + bool is_udp() const + { + return kind == UDP; + } + bool is_instance() const + { + return kind == INSTANCE; + } + }; + + struct filet + { + std::size_t number_of_lines = 0; + std::vector ids; + }; + + // The keys are the file names. + using file_mapt = std::map; + file_mapt file_map; + + /// add an idt + void add(idt id) + { + auto file_name = id.file_name; + file_map[file_name].ids.push_back(std::move(id)); + } + + /// index the given file + void operator()(const irep_idt &file_name, verilog_standardt); + + using instancest = + std::unordered_map, irep_id_hash>; + + // statistics + std::map total_number_of() const; + std::size_t total_number_of_files() const; + std::size_t total_number_of_symlinked_files() const; + std::size_t total_number_of_lines() const; + +protected: + std::string preprocess(const std::string &file_name); +}; + +class cmdlinet; + +int verilog_index(const cmdlinet &); + +#endif // VERILOG_INDEXER_H diff --git a/src/vlindex/vlindex_main.cpp b/src/vlindex/vlindex_main.cpp new file mode 100644 index 000000000..8df104409 --- /dev/null +++ b/src/vlindex/vlindex_main.cpp @@ -0,0 +1,27 @@ +/*******************************************************************\ + +Module: vlindex Main Module + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "vlindex_parse_options.h" + +/*******************************************************************\ + +Function: main + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +int main(int argc, const char **argv) +{ + vlindex_parse_optionst vlindex_parse_options(argc, argv); + return vlindex_parse_options.main(); +} diff --git a/src/vlindex/vlindex_parse_options.cpp b/src/vlindex/vlindex_parse_options.cpp new file mode 100644 index 000000000..b72556823 --- /dev/null +++ b/src/vlindex/vlindex_parse_options.cpp @@ -0,0 +1,120 @@ +/*******************************************************************\ + +Module: vlindex Main Module + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "vlindex_parse_options.h" + +#include +#include +#include + +#include + +#include "verilog_indexer.h" + +#include + +/*******************************************************************\ + +Function: vlindex_parse_optionst::doit + + Inputs: + + Outputs: + + Purpose: invoke main modules + +\*******************************************************************/ + +int vlindex_parse_optionst::doit() +{ + if(cmdline.isset("verbosity")) + ui_message_handler.set_verbosity( + unsafe_string2unsigned(cmdline.get_value("verbosity"))); + else + ui_message_handler.set_verbosity(messaget::M_STATUS); // default + + if(cmdline.isset("version")) + { + std::cout << EBMC_VERSION << '\n'; + return 0; + } + + try + { + return verilog_index(cmdline); + } + catch(const ebmc_errort &ebmc_error) + { + if(!ebmc_error.what().empty()) + { + messaget message(ui_message_handler); + if(ebmc_error.location().is_not_nil()) + message.error().source_location = ebmc_error.location(); + + message.error() << "error: " << messaget::red << ebmc_error.what() + << messaget::reset << messaget::eom; + } + return ebmc_error.exit_code().value_or(CPROVER_EXIT_EXCEPTION); + } +} + +/*******************************************************************\ + +Function: vlindex_parse_optionst::help + + Inputs: + + Outputs: + + Purpose: display command line help + +\*******************************************************************/ + +void vlindex_parse_optionst::help() +{ + std::cout + << "\n" + "* * VLINDEX - Copyright (C) 2024 * *\n" + "* * Version " EBMC_VERSION + " * *\n" + "* * dkr@amazon.com * *\n" + "\n"; + + std::cout << help_formatter( + // clang-format off + "Usage:\tPurpose:\n" + "\n" + " {bvlindex} [{y-?}] [{y-h}] [{y--help}] \t show help\n" + " {bvlindex} {ufile} {u...} \t source file names\n" + "\n" + "Additonal options:\n" + " {y--top} {umodule} \t set top module\n" + " {y-I} {upath} \t set include path\n" + " {y--1800-2017} \t recognize 1800-2017 SystemVerilog (default)\n" + " {y--1800-2012} \t recognize 1800-2012 SystemVerilog\n" + " {y--1800-2009} \t recognize 1800-2009 SystemVerilog\n" + " {y--1800-2005} \t recognize 1800-2005 SystemVerilog\n" + " {y--1364-2005} \t recognize 1364-2005 Verilog\n" + " {y--1364-2001} \t recognize 1364-2001 Verilog\n" + " {y--1364-2001-noconfig} \t recognize 1364-2001-noconfig Verilog\n" + " {y--1364-1995} \t recognize 1364-1995 Verilog\n" + "\n" + "Actions:\n" + " {y--preprocess} \t output the preprocessed source file\n" + " {y--modules} \t show a list of the modules\n" + " {y--instances} \t show a list of the module instances\n" + " {y--classes} \t show a list of the module classes\n" + " {y--packages} \t show a list of the module packages\n" + " {y--udps} \t show a list of the UPDs\n" + " {y--tasks} \t show a list of the tasks\n" + " {y--functions} \t show a list of the functions\n" + " {y--hierarchy} \t show the hierarchy of module instantiations\n" + " {y--verbosity} {u#} \t verbosity level, from 0 (silent) to 10 (everything)\n" + // clang-format on + "\n"); +} diff --git a/src/vlindex/vlindex_parse_options.h b/src/vlindex/vlindex_parse_options.h new file mode 100644 index 000000000..9613c7a00 --- /dev/null +++ b/src/vlindex/vlindex_parse_options.h @@ -0,0 +1,46 @@ +/*******************************************************************\ + +Module: Command Line Parsing + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef VLINDEX_PARSEOPTIONS_H +#define VLINDEX_PARSEOPTIONS_H + +#include +#include + +#include + +class vlindex_parse_optionst : public parse_options_baset +{ +public: + int doit() override; + void help() override; + + vlindex_parse_optionst(int argc, const char **argv) + : parse_options_baset( + "(top)" + "(hierarchy)" + "(modules)" + "(packages)(classes)(interfaces)(udps)(instances)(tasks)(functions)" + "(symlinks)(files)" + "(1800-2017)(1800-2012)(1800-2009)(1800-2005)" + "(1364-2005)(1364-2001)(1364-2001-noconfig)(1364-1995)" + "I:(preprocess)", + argc, + argv, + std::string("EBMC ") + EBMC_VERSION), + ui_message_handler(cmdline, "EBMC " EBMC_VERSION) + { + } + + virtual ~vlindex_parse_optionst() = default; + +protected: + ui_message_handlert ui_message_handler; +}; + +#endif