Skip to content
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

extract transition_systemt::inputs and ::state_variables #525

Merged
merged 1 commit into from
May 28, 2024
Merged

extract transition_systemt::inputs and ::state_variables #525

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
17 changes: 2 additions & 15 deletions src/ebmc/liveness_to_safety.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,23 +120,10 @@ void liveness_to_safetyt::operator()()
if(!properties.requires_lasso_constraints())
return; // no

irep_idt module_identifier = transition_system.main_symbol->name;

// gather the state variables
const namespacet ns(transition_system.symbol_table);
state_vars = transition_system.state_variables();

const auto &symbol_module_map =
transition_system.symbol_table.symbol_module_map;
auto lower = symbol_module_map.lower_bound(module_identifier);
auto upper = symbol_module_map.upper_bound(module_identifier);

for(auto it = lower; it != upper; it++)
{
const symbolt &symbol = ns.lookup(it->second);

if(symbol.is_state_var)
state_vars.push_back(symbol.symbol_expr());
}
const namespacet ns(transition_system.symbol_table);

// create 'loop' shadow symbols for the state variables
for(auto &symbol_expr : state_vars)
Expand Down
80 changes: 2 additions & 78 deletions src/ebmc/random_traces.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,8 +84,6 @@ class random_tracest

constant_exprt random_value(const typet &);

symbolst inputs() const;
symbolst state_variables() const;
symbolst remove_constrained(const symbolst &) const;

void
Expand Down Expand Up @@ -440,80 +438,6 @@ constant_exprt random_tracest::random_value(const typet &type)

/*******************************************************************\

Function: random_tracest::inputs

Inputs:

Outputs:

Purpose:

\*******************************************************************/

random_tracest::symbolst random_tracest::inputs() const
{
symbolst inputs;

const auto &module_symbol = *transition_system.main_symbol;

if(module_symbol.type.id() != ID_module)
throw ebmc_errort() << "expected a module but got "
<< module_symbol.type.id();

const auto &ports = module_symbol.type.find(ID_ports);

// filter out the inputs
for(auto &port : static_cast<const exprt &>(ports).operands())
{
DATA_INVARIANT(port.id() == ID_symbol, "port must be a symbol");
if(port.get_bool(ID_input) && !port.get_bool(ID_output))
{
symbol_exprt input_symbol(port.get(ID_identifier), port.type());
input_symbol.add_source_location() = port.source_location();
inputs.push_back(std::move(input_symbol));
}
}

return inputs;
}

/*******************************************************************\

Function: random_tracest::state_variables

Inputs:

Outputs:

Purpose:

\*******************************************************************/

random_tracest::symbolst random_tracest::state_variables() const
{
symbolst state_variables;

const auto &module_symbol = *transition_system.main_symbol;
const namespacet ns(transition_system.symbol_table);

const auto &symbol_module_map =
transition_system.symbol_table.symbol_module_map;
auto lower = symbol_module_map.lower_bound(module_symbol.name);
auto upper = symbol_module_map.upper_bound(module_symbol.name);

for(auto it = lower; it != upper; it++)
{
const symbolt &symbol = ns.lookup(it->second);

if(symbol.is_state_var)
state_variables.push_back(symbol.symbol_expr());
}

return state_variables;
}

/*******************************************************************\

Function: random_tracest::remove_constrained

Inputs:
Expand Down Expand Up @@ -665,12 +589,12 @@ void random_tracest::operator()(
ns,
true);

auto inputs = this->inputs();
auto inputs = transition_system.inputs();

if(inputs.empty())
throw ebmc_errort() << "module does not have inputs";

auto state_variables = this->state_variables();
auto state_variables = transition_system.state_variables();

message.statistics() << "Found " << inputs.size() << " input(s) and "
<< state_variables.size() << " state variable(s)"
Expand Down
50 changes: 50 additions & 0 deletions src/ebmc/transition_system.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -368,3 +368,53 @@ int show_symbol_table(
return get_transition_system(
cmdline, message_handler, dummy_transition_system);
}

std::vector<symbol_exprt> transition_systemt::state_variables() const
{
std::vector<symbol_exprt> state_variables;

const auto &module_symbol = *main_symbol;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How do we know this unconditional dereference is safe? Is the use of a pointer the right thing at all?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not easy to replace by a reference, but will try.

const namespacet ns(symbol_table);

const auto &symbol_module_map = symbol_table.symbol_module_map;
auto lower = symbol_module_map.lower_bound(module_symbol.name);
auto upper = symbol_module_map.upper_bound(module_symbol.name);

for(auto it = lower; it != upper; it++)
{
const symbolt &symbol = ns.lookup(it->second);

if(symbol.is_state_var)
state_variables.push_back(symbol.symbol_expr());
}

return state_variables;
}

std::vector<symbol_exprt> transition_systemt::inputs() const
{
std::vector<symbol_exprt> inputs;

const auto &module_symbol = *main_symbol;

DATA_INVARIANT(
module_symbol.type.id() == ID_module, "main_symbol must be module");

const auto &ports_irep = module_symbol.type.find(ID_ports);

// filter out the inputs
auto &ports = static_cast<const exprt &>(ports_irep).operands();
for(auto &port : ports)
{
DATA_INVARIANT(port.id() == ID_symbol, "port must be a symbol");
if(port.get_bool(ID_input) && !port.get_bool(ID_output))
{
symbol_exprt input_symbol(
to_symbol_expr(port).get_identifier(), port.type());
input_symbol.add_source_location() = port.source_location();
inputs.push_back(std::move(input_symbol));
}
}

return inputs;
}
3 changes: 3 additions & 0 deletions src/ebmc/transition_system.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,9 @@ class transition_systemt
transt trans_expr; // transition system expression

void output(std::ostream &) const;

std::vector<symbol_exprt> state_variables() const;
std::vector<symbol_exprt> inputs() const;
};

transition_systemt get_transition_system(const cmdlinet &, message_handlert &);
Expand Down