Skip to content

ebmc language interface implementation for Verilog #1454

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
kroening merged 2 commits into from
Dec 23, 2025
Merged

ebmc language interface implementation for Verilog #1454

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
bd06494
cmdlinet in ebmc_languaget can be const
kroening Dec 23, 2025
916ff1f
ebmc language interface implementation for Verilog
kroening Nov 18, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
365 changes: 7 additions & 358 deletions src/ebmc/build_transition_system.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,339 +9,16 @@ Author: Daniel Kroening, [email protected]
#include "build_transition_system.h"

#include <util/cmdline.h>
#include <util/get_module.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/options.h>
#include <util/unicode.h>

#include <langapi/language.h>
#include <langapi/language_util.h>
#include <langapi/mode.h>
#include <smvlang/smv_ebmc_language.h>
#include <trans-word-level/show_module_hierarchy.h>
#include <verilog/verilog_ebmc_language.h>

#include "ebmc_error.h"
#include "ebmc_language_file.h"
#include "ebmc_version.h"
#include "output_file.h"
#include "show_modules.h"
#include "transition_system.h"

#include <fstream>
#include <iostream>

void preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
{
messaget message(message_handler);

if(cmdline.args.size() != 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)
throw ebmc_errort{}.with_exit_code(1)
<< "failed to open input file `" << filename << "'";

auto language = get_language_from_filename(filename);

if(language == nullptr)
{
source_locationt location;
location.set_file(filename);
throw ebmc_errort{}.with_location(location).with_exit_code(1)
<< "failed to figure out type of file";
}

optionst options;

// do -I
if(cmdline.isset('I'))
options.set_option("I", cmdline.get_values('I'));

options.set_option("force-systemverilog", cmdline.isset("systemverilog"));

// do -D
if(cmdline.isset('D'))
options.set_option("defines", cmdline.get_values('D'));

language->set_language_options(options, message_handler);

if(language->preprocess(infile, filename, std::cout, message_handler))
throw ebmc_errort{}.with_exit_code(1);
}

static bool parse(
const cmdlinet &cmdline,
const std::string &filename,
ebmc_language_filest &language_files,
message_handlert &message_handler)
{
messaget message(message_handler);

std::ifstream infile(widen_if_needed(filename));

if(!infile)
{
message.error() << "failed to open input file `" << filename << "'"
<< messaget::eom;
return true;
}

auto &lf = language_files.add_file(filename);
lf.filename = filename;
lf.language = get_language_from_filename(filename);

if(lf.language == nullptr)
{
source_locationt location;
location.set_file(filename);
message.error().source_location = location;
message.error() << "failed to figure out type of file" << messaget::eom;
return true;
}

languaget &language = *lf.language;

optionst options;

// do -I
if(cmdline.isset('I'))
options.set_option("I", cmdline.get_values('I'));

options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions"));
options.set_option("warn-implicit-nets", cmdline.isset("warn-implicit-nets"));

// do -D
if(cmdline.isset('D'))
options.set_option("defines", cmdline.get_values('D'));

// do --ignore-initial
if(cmdline.isset("ignore-initial"))
options.set_option("ignore-initial", true);

// do --initial-zero
if(cmdline.isset("initial-zero"))
options.set_option("initial-zero", true);

language.set_language_options(options, message_handler);

message.status() << "Parsing " << filename << messaget::eom;

if(language.parse(infile, filename, message_handler))
{
message.error() << "PARSING ERROR\n";
return true;
}

lf.get_modules();

return false;
}

bool parse(
const cmdlinet &cmdline,
ebmc_language_filest &language_files,
message_handlert &message_handler)
{
for(unsigned i = 0; i < cmdline.args.size(); i++)
{
if(parse(cmdline, cmdline.args[i], language_files, message_handler))
return true;
}
return false;
}

bool get_main(
const cmdlinet &cmdline,
message_handlert &message_handler,
transition_systemt &transition_system)
{
std::string top_module;

if(cmdline.isset("module"))
top_module = cmdline.get_value("module");
else if(cmdline.isset("top"))
top_module = cmdline.get_value("top");

try
{
transition_system.main_symbol =
&get_module(transition_system.symbol_table, top_module, message_handler);
transition_system.trans_expr =
to_trans_expr(transition_system.main_symbol->value);
}

catch(int e)
{
return true;
}

return false;
}

void make_next_state(exprt &expr)
{
for(auto &sub_expression : expr.operands())
make_next_state(sub_expression);

if(expr.id() == ID_symbol)
expr.id(ID_next_symbol);
}

int get_transition_system(
const cmdlinet &cmdline,
message_handlert &message_handler,
transition_systemt &transition_system)
{
messaget message(message_handler);

//
// parsing
//
ebmc_language_filest language_files;

if(parse(cmdline, language_files, message_handler))
return 1;

if(cmdline.isset("show-parse"))
{
language_files.show_parse(std::cout, message_handler);
return 0;
}

//
// type checking
//

message.status() << "Converting" << messaget::eom;

if(language_files.typecheck(transition_system.symbol_table, message_handler))
{
message.error() << "CONVERSION ERROR" << messaget::eom;
return 2;
}

if(cmdline.isset("show-modules"))
{
show_modulest::from_symbol_table(transition_system.symbol_table)
.plain_text(std::cout);
return 0;
}

if(cmdline.isset("modules-xml"))
{
auto filename = cmdline.get_value("modules-xml");
auto out_file = output_filet{filename};
show_modulest::from_symbol_table(transition_system.symbol_table)
.xml(out_file.stream());
return 0;
}

if(cmdline.isset("json-modules"))
{
auto out_file = output_filet{cmdline.get_value("json-modules")};
show_modulest::from_symbol_table(transition_system.symbol_table)
.json(out_file.stream());
return 0;
}

if(cmdline.isset("show-symbol-table"))
{
std::cout << transition_system.symbol_table;
return 0;
}

// get module name

if(get_main(cmdline, message_handler, transition_system))
return 1;

if(cmdline.isset("show-module-hierarchy"))
{
DATA_INVARIANT(
transition_system.main_symbol != nullptr, "must have main_symbol");
show_module_hierarchy(
transition_system.symbol_table,
*transition_system.main_symbol,
std::cout);
return 0;
}

// --reset given?
if(cmdline.isset("reset"))
{
namespacet ns(transition_system.symbol_table);
exprt reset_constraint = to_expr(
ns, transition_system.main_symbol->name, cmdline.get_value("reset"));

// we want the constraint to be boolean
reset_constraint =
typecast_exprt::conditional_cast(reset_constraint, bool_typet{});

// true in initial state
transt new_trans_expr = transition_system.trans_expr;
new_trans_expr.init() = and_exprt(new_trans_expr.init(), reset_constraint);

// and not anymore afterwards
exprt reset_next_state = reset_constraint;
make_next_state(reset_next_state);

new_trans_expr.trans() =
and_exprt(new_trans_expr.trans(), not_exprt(reset_next_state));
transition_system.trans_expr = new_trans_expr;
}

return -1; // done with the transition system
}

transition_systemt get_transition_system(
const cmdlinet &cmdline,
message_handlert &message_handler)
{
transition_systemt transition_system;
auto exit_code =
get_transition_system(cmdline, message_handler, transition_system);
if(exit_code != -1)
throw ebmc_errort().with_exit_code(exit_code);
return transition_system;
}

int show_parse(const cmdlinet &cmdline, message_handlert &message_handler)
{
transition_systemt dummy_transition_system;
return get_transition_system(
cmdline, message_handler, dummy_transition_system);
}

int show_modules(const cmdlinet &cmdline, message_handlert &message_handler)
{
transition_systemt dummy_transition_system;
return get_transition_system(
cmdline, message_handler, dummy_transition_system);
}

int show_module_hierarchy(
const cmdlinet &cmdline,
message_handlert &message_handler)
{
transition_systemt dummy_transition_system;
return get_transition_system(
cmdline, message_handler, dummy_transition_system);
}

int show_symbol_table(
const cmdlinet &cmdline,
message_handlert &message_handler)
{
transition_systemt dummy_transition_system;
return get_transition_system(
cmdline, message_handler, dummy_transition_system);
}
#include <set>

static std::set<std::string> file_extensions(const cmdlinet::argst &args)
{
Expand Down Expand Up @@ -379,40 +56,12 @@ std::optional<transition_systemt> ebmc_languagest::transition_system()
{
return smv_ebmc_languaget{cmdline, message_handler}.transition_system();
}
else if(have_verilog)
{
return verilog_ebmc_languaget{cmdline, message_handler}.transition_system();
}
else
{
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);
throw ebmc_errort{} << "no support for given input file extensions";
}
}
Loading
Loading