From ac4908e81afceb684806387b6b0e577febf27210 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 17 Nov 2025 19:53:01 -0800 Subject: [PATCH 1/5] new transition system language API This adds an API for obtaining a transition system from a source modeling language, designed to suit Verilog, SMV and similar languages. --- src/ebmc/Makefile | 1 + src/ebmc/ebmc_language.cpp | 13 ++++++++++++ src/ebmc/ebmc_language.h | 43 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 57 insertions(+) create mode 100644 src/ebmc/ebmc_language.cpp create mode 100644 src/ebmc/ebmc_language.h diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile index aab061feb..793f05b53 100644 --- a/src/ebmc/Makefile +++ b/src/ebmc/Makefile @@ -13,6 +13,7 @@ SRC = \ diatest.cpp \ dimacs_writer.cpp \ ebmc_base.cpp \ + ebmc_language.cpp \ ebmc_language_file.cpp \ ebmc_languages.cpp \ ebmc_parse_options.cpp \ diff --git a/src/ebmc/ebmc_language.cpp b/src/ebmc/ebmc_language.cpp new file mode 100644 index 000000000..2eddf7e72 --- /dev/null +++ b/src/ebmc/ebmc_language.cpp @@ -0,0 +1,13 @@ +/*******************************************************************\ + +Module: Abstract interface to support a modeling language + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "ebmc_language.h" + +ebmc_languaget::~ebmc_languaget() +{ +} diff --git a/src/ebmc/ebmc_language.h b/src/ebmc/ebmc_language.h new file mode 100644 index 000000000..fe757af33 --- /dev/null +++ b/src/ebmc/ebmc_language.h @@ -0,0 +1,43 @@ +/*******************************************************************\ + +Module: Abstract interface to support a modeling language + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +/// \file +/// Abstract interface to support a modeling language + +#ifndef EBMC_LANGUAGE_H +#define EBMC_LANGUAGE_H + +#include + +class cmdlinet; +class message_handlert; +class transition_systemt; + +class ebmc_languaget +{ +public: + // constructor / destructor + ebmc_languaget(cmdlinet &_cmdline, message_handlert &_message_handler) + : cmdline(_cmdline), message_handler(_message_handler) + { + } + + virtual ~ebmc_languaget(); + + /// produce diagnostic output as specified on the command line + virtual void diagnostics() = 0; + + /// produce the transition system, and return it + virtual transition_systemt transition_system() = 0; + +protected: + cmdlinet &cmdline; + message_handlert &message_handler; +}; + +#endif // EBMC_LANGUAGE_H From 3a4a116175e6d98277f22a3af57c94de265251ab Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 18 Nov 2025 17:02:42 -0800 Subject: [PATCH 2/5] use ebmc_languaget API in ebmc_parse_optionst This replaces the direct call to get_transition_system(...) by a call to an implementation of ebmc_languaget, which wraps get_transition_system. --- .../preprocessor/unknown_directive.desc | 1 - src/ebmc/build_transition_system.cpp | 68 ++++++++++++------- src/ebmc/build_transition_system.h | 17 +++-- src/ebmc/ebmc_language.h | 9 ++- src/ebmc/ebmc_parse_options.cpp | 53 +++++++-------- src/ebmc/neural_liveness.cpp | 22 +++--- src/ebmc/neural_liveness.h | 10 ++- src/ebmc/random_traces.cpp | 17 +++-- src/ebmc/random_traces.h | 12 +++- src/ebmc/ranking_function.cpp | 6 +- src/ebmc/ranking_function.h | 5 +- 11 files changed, 124 insertions(+), 96 deletions(-) diff --git a/regression/verilog/preprocessor/unknown_directive.desc b/regression/verilog/preprocessor/unknown_directive.desc index 1f6ce9b32..e718de61f 100644 --- a/regression/verilog/preprocessor/unknown_directive.desc +++ b/regression/verilog/preprocessor/unknown_directive.desc @@ -2,7 +2,6 @@ CORE unknown_directive.v --preprocess ^file unknown_directive\.v line 1: unknown preprocessor directive "something"$ -^PREPROCESSING FAILED$ ^EXIT=1$ ^SIGNAL=0$ -- diff --git a/src/ebmc/build_transition_system.cpp b/src/ebmc/build_transition_system.cpp index dc9af380f..1471e2a1f 100644 --- a/src/ebmc/build_transition_system.cpp +++ b/src/ebmc/build_transition_system.cpp @@ -30,26 +30,20 @@ Author: Daniel Kroening, dkr@amazon.com #include #include -int preprocess(const cmdlinet &cmdline, message_handlert &message_handler) +void preprocess(const cmdlinet &cmdline, message_handlert &message_handler) { messaget message(message_handler); if(cmdline.args.size() != 1) - { - message.error() << "please give exactly one file to preprocess" - << messaget::eom; - return 1; - } + throw ebmc_errort{}.with_exit_code(1) + << "please give exactly one file to preprocess"; const auto &filename = cmdline.args.front(); std::ifstream infile(widen_if_needed(filename)); if(!infile) - { - message.error() << "failed to open input file `" << filename << "'" - << messaget::eom; - return 1; - } + throw ebmc_errort{}.with_exit_code(1) + << "failed to open input file `" << filename << "'"; auto language = get_language_from_filename(filename); @@ -57,9 +51,8 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler) { source_locationt location; location.set_file(filename); - message.error().source_location = location; - message.error() << "failed to figure out type of file" << messaget::eom; - return 1; + throw ebmc_errort{}.with_location(location).with_exit_code(1) + << "failed to figure out type of file"; } optionst options; @@ -77,12 +70,7 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler) language->set_language_options(options, message_handler); if(language->preprocess(infile, filename, std::cout, message_handler)) - { - message.error() << "PREPROCESSING FAILED" << messaget::eom; - return 1; - } - - return 0; + throw ebmc_errort{}.with_exit_code(1); } static bool parse( @@ -211,9 +199,6 @@ int get_transition_system( { messaget message(message_handler); - if(cmdline.isset("preprocess")) - return preprocess(cmdline, message_handler); - // // parsing // @@ -349,3 +334,40 @@ int show_symbol_table( return get_transition_system( cmdline, message_handler, dummy_transition_system); } + +std::optional ebmc_languagest::transition_system() +{ + if(cmdline.isset("preprocess")) + { + preprocess(cmdline, message_handler); + return {}; + } + + if(cmdline.isset("show-parse")) + { + show_parse(cmdline, message_handler); + return {}; + } + + if( + cmdline.isset("show-modules") || cmdline.isset("modules-xml") || + cmdline.isset("json-modules")) + { + show_modules(cmdline, message_handler); + return {}; + } + + if(cmdline.isset("show-module-hierarchy")) + { + show_module_hierarchy(cmdline, message_handler); + return {}; + } + + if(cmdline.isset("show-symbol-table")) + { + show_symbol_table(cmdline, message_handler); + return {}; + } + + return get_transition_system(cmdline, message_handler); +} diff --git a/src/ebmc/build_transition_system.h b/src/ebmc/build_transition_system.h index e75622385..35c345a2f 100644 --- a/src/ebmc/build_transition_system.h +++ b/src/ebmc/build_transition_system.h @@ -9,16 +9,25 @@ Author: Daniel Kroening, dkr@amazon.com #ifndef CPROVER_EBMC_BUILD_TRANSITION_SYSTEM_H #define CPROVER_EBMC_BUILD_TRANSITION_SYSTEM_H -class cmdlinet; -class message_handlert; -class transition_systemt; +#include "ebmc_language.h" transition_systemt get_transition_system(const cmdlinet &, message_handlert &); -int preprocess(const cmdlinet &, message_handlert &); +void preprocess(const cmdlinet &, message_handlert &); int show_parse(const cmdlinet &, message_handlert &); int show_modules(const cmdlinet &, message_handlert &); int show_module_hierarchy(const cmdlinet &, message_handlert &); int show_symbol_table(const cmdlinet &, message_handlert &); +class ebmc_languagest : public ebmc_languaget +{ +public: + ebmc_languagest(cmdlinet &_cmdline, message_handlert &_message_handler) + : ebmc_languaget{_cmdline, _message_handler} + { + } + + std::optional transition_system() override; +}; + #endif // CPROVER_EBMC_BUILD_TRANSITION_SYSTEM_H diff --git a/src/ebmc/ebmc_language.h b/src/ebmc/ebmc_language.h index fe757af33..d49f80917 100644 --- a/src/ebmc/ebmc_language.h +++ b/src/ebmc/ebmc_language.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, dkr@amazon.com #define EBMC_LANGUAGE_H #include +#include class cmdlinet; class message_handlert; @@ -29,11 +30,9 @@ class ebmc_languaget virtual ~ebmc_languaget(); - /// produce diagnostic output as specified on the command line - virtual void diagnostics() = 0; - - /// produce the transition system, and return it - virtual transition_systemt transition_system() = 0; + /// Produce the transition system, and return it; + /// returns {} when diagnostic output was produced instead. + virtual std::optional transition_system() = 0; protected: cmdlinet &cmdline; diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 3d9733130..478501507 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "diatest.h" #include "ebmc_base.h" #include "ebmc_error.h" +#include "ebmc_language.h" #include "ebmc_version.h" #include "format_hooks.h" #include "instrument_buechi.h" @@ -108,23 +109,6 @@ int ebmc_parse_optionst::doit() return 0; } - if(cmdline.isset("preprocess")) - return preprocess(cmdline, ui_message_handler); - - if(cmdline.isset("show-parse")) - return show_parse(cmdline, ui_message_handler); - - if( - cmdline.isset("show-modules") || cmdline.isset("modules-xml") || - cmdline.isset("json-modules")) - return show_modules(cmdline, ui_message_handler); - - if(cmdline.isset("show-module-hierarchy")) - return show_module_hierarchy(cmdline, ui_message_handler); - - if(cmdline.isset("show-symbol-table")) - return show_symbol_table(cmdline, ui_message_handler); - if(cmdline.isset("coverage")) { throw ebmc_errort() << "This option is currently disabled"; @@ -140,18 +124,6 @@ int ebmc_parse_optionst::doit() #endif } - if(cmdline.isset("random-traces")) - return random_traces(cmdline, ui_message_handler); - - if(cmdline.isset("random-trace") || cmdline.isset("random-waveform")) - return random_trace(cmdline, ui_message_handler); - - if(cmdline.isset("neural-liveness")) - return do_neural_liveness(cmdline, ui_message_handler); - - if(cmdline.isset("ranking-function")) - return do_ranking_function(cmdline, ui_message_handler); - if(cmdline.isset("interpolation-word")) { throw ebmc_errort() << "This option is currently disabled"; @@ -208,7 +180,28 @@ int ebmc_parse_optionst::doit() } // get the transition system - auto transition_system = get_transition_system(cmdline, ui_message_handler); + ebmc_languagest ebmc_languages{cmdline, ui_message_handler}; + + auto transition_system_opt = ebmc_languages.transition_system(); + + // Did we produce diagnostics instead? + if(!transition_system_opt.has_value()) + return 0; + + auto &transition_system = transition_system_opt.value(); + + if(cmdline.isset("random-traces")) + return random_traces(transition_system, cmdline, ui_message_handler); + + if(cmdline.isset("random-trace") || cmdline.isset("random-waveform")) + return random_trace(transition_system, cmdline, ui_message_handler); + + if(cmdline.isset("neural-liveness")) + return do_neural_liveness(transition_system, cmdline, ui_message_handler); + + if(cmdline.isset("ranking-function")) + return do_ranking_function( + transition_system, cmdline, ui_message_handler); // get the properties auto properties = ebmc_propertiest::from_command_line( diff --git a/src/ebmc/neural_liveness.cpp b/src/ebmc/neural_liveness.cpp index b55db6aff..5188f92cc 100644 --- a/src/ebmc/neural_liveness.cpp +++ b/src/ebmc/neural_liveness.cpp @@ -17,7 +17,6 @@ Author: Daniel Kroening, dkr@amazon.com #include #include -#include "build_transition_system.h" #include "ebmc_error.h" #include "ebmc_solver_factory.h" #include "live_signal.h" @@ -42,10 +41,14 @@ Author: Daniel Kroening, dkr@amazon.com class neural_livenesst { public: - neural_livenesst(const cmdlinet &_cmdline, message_handlert &_message_handler) + neural_livenesst( + transition_systemt &_transition_system, + const cmdlinet &_cmdline, + message_handlert &_message_handler) : cmdline(_cmdline), message(_message_handler), - solver_factory(ebmc_solver_factory(_cmdline)) + solver_factory(ebmc_solver_factory(_cmdline)), + transition_system(_transition_system) { } @@ -55,7 +58,7 @@ class neural_livenesst const cmdlinet &cmdline; messaget message; ebmc_solver_factoryt solver_factory; - transition_systemt transition_system; + transition_systemt &transition_system; ebmc_propertiest properties; int show_traces(); @@ -75,9 +78,6 @@ int neural_livenesst::operator()() if(!cmdline.isset("neural-engine")) throw ebmc_errort() << "give a neural engine"; - transition_system = - get_transition_system(cmdline, message.get_message_handler()); - // Get the properties properties = ebmc_propertiest::from_command_line( cmdline, transition_system, message.get_message_handler()); @@ -127,9 +127,6 @@ int neural_livenesst::operator()() int neural_livenesst::show_traces() { - transition_system = - get_transition_system(cmdline, message.get_message_handler()); - properties = ebmc_propertiest::from_command_line( cmdline, transition_system, message.get_message_handler()); @@ -317,8 +314,9 @@ tvt neural_livenesst::verify( } int do_neural_liveness( + transition_systemt &transition_system, const cmdlinet &cmdline, - ui_message_handlert &ui_message_handler) + message_handlert &message_handler) { - return neural_livenesst(cmdline, ui_message_handler)(); + return neural_livenesst{transition_system, cmdline, message_handler}(); } diff --git a/src/ebmc/neural_liveness.h b/src/ebmc/neural_liveness.h index 159f38208..ed47bb555 100644 --- a/src/ebmc/neural_liveness.h +++ b/src/ebmc/neural_liveness.h @@ -9,9 +9,13 @@ Author: Daniel Kroening, dkr@amazon.com #ifndef EBMC_NEURAL_LIVENESS_H #define EBMC_NEURAL_LIVENESS_H -#include -#include +class cmdlinet; +class message_handlert; +class transition_systemt; -int do_neural_liveness(const cmdlinet &, ui_message_handlert &); +int do_neural_liveness( + transition_systemt &, + const cmdlinet &, + message_handlert &); #endif // EBMC_NEURAL_LIVENESS_H diff --git a/src/ebmc/random_traces.cpp b/src/ebmc/random_traces.cpp index b761c6244..d9e102805 100644 --- a/src/ebmc/random_traces.cpp +++ b/src/ebmc/random_traces.cpp @@ -20,7 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "build_transition_system.h" #include "ebmc_base.h" #include "ebmc_error.h" #include "output_file.h" @@ -113,7 +112,10 @@ Function: random_traces \*******************************************************************/ -int random_traces(const cmdlinet &cmdline, message_handlert &message_handler) +int random_traces( + const transition_systemt &transition_system, + const cmdlinet &cmdline, + message_handlert &message_handler) { const auto number_of_traces = [&cmdline]() -> std::size_t { if(cmdline.isset("traces")) @@ -172,9 +174,6 @@ int random_traces(const cmdlinet &cmdline, message_handlert &message_handler) return {}; }(); - transition_systemt transition_system = - get_transition_system(cmdline, message_handler); - if(cmdline.isset("waveform") && cmdline.isset("vcd")) throw ebmc_errort() << "cannot do VCD and ASCII waveform simultaneously"; @@ -232,7 +231,10 @@ Function: random_trace \*******************************************************************/ -int random_trace(const cmdlinet &cmdline, message_handlert &message_handler) +int random_trace( + const transition_systemt &transition_system, + const cmdlinet &cmdline, + message_handlert &message_handler) { if(cmdline.isset("traces")) throw ebmc_errort() << "must not give number of traces"; @@ -276,9 +278,6 @@ int random_trace(const cmdlinet &cmdline, message_handlert &message_handler) return 10; // default }(); - transition_systemt transition_system = - get_transition_system(cmdline, message_handler); - auto consumer = [&](trans_tracet trace) -> void { namespacet ns(transition_system.symbol_table); if(cmdline.isset("random-waveform") || cmdline.isset("waveform")) diff --git a/src/ebmc/random_traces.h b/src/ebmc/random_traces.h index ccb03b584..92ba55645 100644 --- a/src/ebmc/random_traces.h +++ b/src/ebmc/random_traces.h @@ -16,14 +16,20 @@ Author: Daniel Kroening, kroening@kroening.com class cmdlinet; class message_handlert; +class transition_systemt; // many traces -int random_traces(const cmdlinet &, message_handlert &); +int random_traces( + const transition_systemt &, + const cmdlinet &, + message_handlert &); // just one trace -int random_trace(const cmdlinet &, message_handlert &); +int random_trace( + const transition_systemt &, + const cmdlinet &, + message_handlert &); -class transition_systemt; class trans_tracet; // many traces, VCD diff --git a/src/ebmc/ranking_function.cpp b/src/ebmc/ranking_function.cpp index 770939e6c..c35cc948a 100644 --- a/src/ebmc/ranking_function.cpp +++ b/src/ebmc/ranking_function.cpp @@ -21,7 +21,6 @@ Author: Daniel Kroening, dkr@amazon.com #include #include -#include "build_transition_system.h" #include "ebmc_base.h" #include "ebmc_error.h" #include "ebmc_solver_factory.h" @@ -87,13 +86,10 @@ ebmc_propertiest::propertyt &find_property(ebmc_propertiest &properties) } int do_ranking_function( + const transition_systemt &transition_system, const cmdlinet &cmdline, message_handlert &message_handler) { - // get the transition system - transition_systemt transition_system = - get_transition_system(cmdline, message_handler); - // parse the ranking function if(!cmdline.isset("ranking-function")) throw ebmc_errort() << "no candidate ranking function given"; diff --git a/src/ebmc/ranking_function.h b/src/ebmc/ranking_function.h index d705705a0..bcd360efe 100644 --- a/src/ebmc/ranking_function.h +++ b/src/ebmc/ranking_function.h @@ -20,7 +20,10 @@ class exprt; class transition_systemt; class trans_tracet; -int do_ranking_function(const cmdlinet &, message_handlert &); +int do_ranking_function( + const transition_systemt &, + const cmdlinet &, + message_handlert &); exprt parse_ranking_function( const std::string &, From f47fe86fcae9e2fd5013bb2796c27589fe62bd01 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 18 Nov 2025 10:08:50 -0800 Subject: [PATCH 3/5] ebmc language implementation for SMV This adds an implementation of the ebmc_languaget interface for SMV. --- src/smvlang/Makefile | 3 +- src/smvlang/smv_ebmc_language.cpp | 110 ++++++++++++++++++++++++++++++ src/smvlang/smv_ebmc_language.h | 34 +++++++++ 3 files changed, 146 insertions(+), 1 deletion(-) create mode 100644 src/smvlang/smv_ebmc_language.cpp create mode 100644 src/smvlang/smv_ebmc_language.h diff --git a/src/smvlang/Makefile b/src/smvlang/Makefile index 248dced76..30b6e6505 100644 --- a/src/smvlang/Makefile +++ b/src/smvlang/Makefile @@ -1,4 +1,5 @@ -SRC = smv_expr.cpp \ +SRC = smv_ebmc_language.cpp \ + smv_expr.cpp \ smv_language.cpp \ smv_parser.cpp \ smv_typecheck.cpp \ diff --git a/src/smvlang/smv_ebmc_language.cpp b/src/smvlang/smv_ebmc_language.cpp new file mode 100644 index 000000000..ba624f5b3 --- /dev/null +++ b/src/smvlang/smv_ebmc_language.cpp @@ -0,0 +1,110 @@ +/*******************************************************************\ + +Module: SMV Language Interface + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +/// \file +/// SMV Language Interface + +#include "smv_ebmc_language.h" + +#include +#include +#include + +#include +#include + +#include "smv_parser.h" +#include "smv_typecheck.h" + +#include +#include + +std::string smv_file_name(const cmdlinet &cmdline) +{ + if(cmdline.args.size() == 0) + throw ebmc_errort{} << "no file name given"; + + if(cmdline.args.size() >= 2) + throw ebmc_errort{}.with_exit_code(1) << "SMV only uses a single file"; + + return cmdline.args.front(); +} + +smv_parse_treet smv_ebmc_languaget::parse() +{ + smv_parsert smv_parser{message_handler}; + + auto file_name = smv_file_name(cmdline); + + std::ifstream infile{widen_if_needed(file_name)}; + + if(!infile) + throw ebmc_errort{}.with_exit_code(1) << "failed to open " << file_name; + + smv_parser.set_file(file_name); + smv_parser.in = &infile; + + if(smv_parser.parse()) + throw ebmc_errort{}.with_exit_code(1); + + return std::move(smv_parser.parse_tree); +} + +std::optional smv_ebmc_languaget::transition_system() +{ + if(cmdline.isset("preprocess")) + { + throw ebmc_errort{}.with_exit_code(1) << "SMV does not use preprocessing"; + } + + auto parse_tree = parse(); + + if(cmdline.isset("show-parse")) + { + parse_tree.show(std::cout); + return {}; + } + + if( + cmdline.isset("show-modules") || cmdline.isset("modules-xml") || + cmdline.isset("json-modules")) + { + //show_modules(cmdline, message_handler); + return {}; + } + + if(cmdline.isset("show-module-hierarchy")) + { + //show_module_hierarchy(cmdline, message_handler); + return {}; + } + + transition_systemt result; + + if(smv_typecheck( + parse_tree, result.symbol_table, "smv::main", message_handler)) + { + messaget message{message_handler}; + message.error() << "CONVERSION ERROR" << messaget::eom; + throw ebmc_errort{}.with_exit_code(2); + } + + if(cmdline.isset("show-symbol-table")) + { + std::cout << result.symbol_table; + return {}; + } + + result.main_symbol = + &get_module(result.symbol_table, "main", message_handler); + + result.trans_expr = + to_trans_expr(result.main_symbol->value); + + return result; +} diff --git a/src/smvlang/smv_ebmc_language.h b/src/smvlang/smv_ebmc_language.h new file mode 100644 index 000000000..72ab3ef35 --- /dev/null +++ b/src/smvlang/smv_ebmc_language.h @@ -0,0 +1,34 @@ +/*******************************************************************\ + +Module: SMV Language Interface + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +/// \file +/// SMV Language Interface + +#ifndef EBMC_SMV_LANGUAGE_H +#define EBMC_SMV_LANGUAGE_H + +#include + +class smv_parse_treet; + +class smv_ebmc_languaget : public ebmc_languaget +{ +public: + smv_ebmc_languaget(cmdlinet &_cmdline, message_handlert &_message_handler) + : ebmc_languaget(_cmdline, _message_handler) + { + } + + // produce the transition system, and return it + std::optional transition_system() override; + +protected: + smv_parse_treet parse(); +}; + +#endif // EBMC_SMV_LANGUAGE_H From ca68c2a33301d684dac29cd69275f4684c2f2b6d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 18 Nov 2025 10:19:24 -0800 Subject: [PATCH 4/5] ebmc language interface implementation for Verilog This adds an implementation of the ebmc_languaget interface for Verilog. --- src/verilog/verilog_ebmc_language.cpp | 64 +++++++++++++++++++++++++++ src/verilog/verilog_ebmc_language.h | 34 ++++++++++++++ 2 files changed, 98 insertions(+) create mode 100644 src/verilog/verilog_ebmc_language.cpp create mode 100644 src/verilog/verilog_ebmc_language.h diff --git a/src/verilog/verilog_ebmc_language.cpp b/src/verilog/verilog_ebmc_language.cpp new file mode 100644 index 000000000..c51ff5202 --- /dev/null +++ b/src/verilog/verilog_ebmc_language.cpp @@ -0,0 +1,64 @@ +/*******************************************************************\ + +Module: Verilog Language Interface + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +/// \file +/// Verilog Language Interface + +#include "verilog_ebmc_language.h" + +#include +#include +#include + +#include +#include + +#include "verilog_parser.h" +#include "verilog_typecheck.h" + +#include + +verilog_parse_treet verilog_ebmc_languaget::parse() +{ + verilog_standardt standard; + + verilog_parsert verilog_parser{standard, message_handler}; + + auto file_name = verilog_file_name(cmdline); + + std::ifstream infile{widen_if_needed(file_name)}; + + if(!infile) + throw ebmc_errort{} << "failed to open " << file_name; + + verilog_parser.set_file(file_name); + verilog_parser.in = &infile; + + if(verilog_parser.parse()) + throw ebmc_errort{} << "parsing has failed"; + + return std::move(verilog_parser.parse_tree); +} + +std::optional verilog_ebmc_languaget::transition_system() +{ + auto parse_tree = parse(); + + transition_systemt result; + + if(verilog_typecheck(parse_tree, result.symbol_table, "main", message_handler)) + throw ebmc_errort{} << "typechecking has failed"; + + result.main_symbol = + &get_module(result.symbol_table, "main", message_handler); + + result.trans_expr = + to_trans_expr(result.main_symbol->value); + + return result; +} diff --git a/src/verilog/verilog_ebmc_language.h b/src/verilog/verilog_ebmc_language.h new file mode 100644 index 000000000..d4fa52f27 --- /dev/null +++ b/src/verilog/verilog_ebmc_language.h @@ -0,0 +1,34 @@ +/*******************************************************************\ + +Module: Verilog Language Interface + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +/// \file +/// SMV Language Interface + +#ifndef EBMC_VERILOG_LANGUAGE_H +#define EBMC_VERILOG_LANGUAGE_H + +#include + +class verilog_parse_treet; + +class verilog_ebmc_languaget : public ebmc_languaget +{ +public: + verilog_ebmc_languaget(cmdlinet &_cmdline, message_handlert &_message_handler) + : ebmc_languaget(_cmdline, _message_handler) + { + } + + // produce the transition system, and return it + std::optional transition_system() override; + +protected: + verilog_parse_treet parse(); +}; + +#endif // EBMC_VERILOG_LANGUAGE_H From 7e2078f925289c02e95d6489e05f984118f08c0c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 18 Nov 2025 21:27:00 -0800 Subject: [PATCH 5/5] use SMV and Verilog langauge interfaces --- src/ebmc/build_transition_system.cpp | 84 ++++++++++++++++++++-------- 1 file changed, 61 insertions(+), 23 deletions(-) diff --git a/src/ebmc/build_transition_system.cpp b/src/ebmc/build_transition_system.cpp index 1471e2a1f..f14dc10b6 100644 --- a/src/ebmc/build_transition_system.cpp +++ b/src/ebmc/build_transition_system.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, dkr@amazon.com #include #include #include +#include #include #include @@ -335,39 +336,76 @@ int show_symbol_table( cmdline, message_handler, dummy_transition_system); } -std::optional ebmc_languagest::transition_system() +static std::set file_extensions(const cmdlinet::argst &args) { - if(cmdline.isset("preprocess")) - { - preprocess(cmdline, message_handler); - return {}; - } + std::set result; - if(cmdline.isset("show-parse")) + for(auto &arg : args) { - show_parse(cmdline, message_handler); - return {}; + std::size_t ext_pos = arg.rfind('.'); + + if(ext_pos != std::string::npos) + { + auto ext = std::string(arg, ext_pos + 1, std::string::npos); + result.insert(ext); + } } - if( - cmdline.isset("show-modules") || cmdline.isset("modules-xml") || - cmdline.isset("json-modules")) + return result; +} + +std::optional ebmc_languagest::transition_system() +{ + auto extensions = file_extensions(cmdline.args); + auto ext_used = [&extensions](const char *ext) + { return extensions.find(ext) != extensions.end(); }; + + bool have_smv = ext_used("smv"); + bool have_verilog = ext_used("v") || ext_used("sv"); + + if(have_smv && have_verilog) { - show_modules(cmdline, message_handler); - return {}; + throw ebmc_errort{} << "no support for mixed-language models"; } - if(cmdline.isset("show-module-hierarchy")) + if(have_smv) { - show_module_hierarchy(cmdline, message_handler); - return {}; + return smv_ebmc_languaget{cmdline, message_handler}.transition_system(); } - - if(cmdline.isset("show-symbol-table")) + else { - show_symbol_table(cmdline, message_handler); - return {}; + if(cmdline.isset("preprocess")) + { + preprocess(cmdline, message_handler); + return {}; + } + + if(cmdline.isset("show-parse")) + { + show_parse(cmdline, message_handler); + return {}; + } + + if( + cmdline.isset("show-modules") || cmdline.isset("modules-xml") || + cmdline.isset("json-modules")) + { + show_modules(cmdline, message_handler); + return {}; + } + + if(cmdline.isset("show-module-hierarchy")) + { + show_module_hierarchy(cmdline, message_handler); + return {}; + } + + if(cmdline.isset("show-symbol-table")) + { + show_symbol_table(cmdline, message_handler); + return {}; + } + + return get_transition_system(cmdline, message_handler); } - - return get_transition_system(cmdline, message_handler); }