Skip to content

SMV: flatten hierarchy on parse tree #1425

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
merged 1 commit into from
Nov 25, 2025
+74 −177
Merged

SMV: flatten hierarchy on parse tree #1425

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
3 changes: 1 addition & 2 deletions regression/smv/modules/parameters2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,8 @@
KNOWNBUG
CORE
parameters2.smv

^EXIT=10$
^SIGNAL=0$
--
^warning: ignoring
--
This yields a type-checking error.
7 changes: 7 additions & 0 deletions regression/smv/modules/use_before_declaration1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE
use_before_declaration1.smv
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
--
10 changes: 10 additions & 0 deletions regression/smv/modules/use_before_declaration1.smv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
MODULE main

-- you can use modules before they are declared
SPEC sub.something = 123

VAR sub : my-module;

MODULE my-module

DEFINE something := 123;
2 changes: 1 addition & 1 deletion src/smvlang/smv_parse_tree.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ class smv_parse_treet
struct modulet
{
irep_idt name, base_name;
std::list<irep_idt> parameters;
std::vector<irep_idt> parameters;

struct elementt
{
Expand Down
229 changes: 55 additions & 174 deletions src/smvlang/smv_typecheck.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,7 @@ class smv_typecheckt:public typecheckt
} modet;

void convert(smv_parse_treet::modulet &);

void create_var_symbols(const smv_parse_treet::modulet::element_listt &);

void collect_define(const equal_exprt &);
Expand Down Expand Up @@ -104,16 +105,14 @@ class smv_typecheckt:public typecheckt
smv_parse_treet::modulet &,
const irep_idt &identifier,
const irep_idt &instance,
const exprt::operandst &operands,
const exprt::operandst &arguments,
const source_locationt &);

typet
type_union(const typet &type1, const typet &type2, const source_locationt &);

typedef std::map<irep_idt, exprt> rename_mapt;

void instantiate_rename(exprt &, const rename_mapt &rename_map);

void convert_ports(smv_parse_treet::modulet &, typet &dest);

// for defines
Expand Down Expand Up @@ -196,8 +195,14 @@ Function: smv_typecheckt::flatten_hierarchy

void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module)
{
for(auto &element : smv_module.elements)
// Not using ranged for since we will append to the list we are
// iterating over! This avoids recursion.
for(auto element_it = smv_module.elements.begin();
element_it != smv_module.elements.end();
++element_it)
{
auto &element = *element_it;

if(element.is_var() && element.expr.type().id() == ID_smv_submodule)
{
exprt &inst =
Expand Down Expand Up @@ -235,195 +240,66 @@ void smv_typecheckt::instantiate(
smv_parse_treet::modulet &smv_module,
const irep_idt &identifier,
const irep_idt &instance,
const exprt::operandst &operands,
const exprt::operandst &arguments,
const source_locationt &location)
{
symbol_table_baset::symbolst::const_iterator s_it =
symbol_table.symbols.find(identifier);
// Find the module
auto module_it = smv_parse_tree.module_map.find(identifier);

if(s_it==symbol_table.symbols.end())
if(module_it == smv_parse_tree.module_map.end())
{
throw errort().with_location(location)
<< "submodule `" << identifier << "' not found";
}

if(s_it->second.type.id()!=ID_module)
{
throw errort().with_location(location)
<< "submodule `" << identifier << "' not a module";
}

const irept::subt &ports=s_it->second.type.find(ID_ports).get_sub();

// do the arguments/ports
const auto &instantiated_module = *module_it->second;
const auto &parameters = instantiated_module.parameters;

if(ports.size()!=operands.size())
// map the arguments to parameters
if(parameters.size() != arguments.size())
{
throw errort().with_location(location)
<< "submodule `" << identifier << "' has wrong number of arguments";
}

std::set<irep_idt> port_identifiers;
rename_mapt rename_map;

for(std::size_t i = 0; i < ports.size(); i++)
{
const irep_idt &identifier=ports[i].get(ID_identifier);
rename_map.insert(std::pair<irep_idt, exprt>(identifier, operands[i]));
port_identifiers.insert(identifier);
}

// do the variables

std::string new_prefix=
id2string(smv_module.name)+"::var::"+id2string(instance)+".";

std::set<irep_idt> var_identifiers;

for(auto v_it=symbol_table.symbol_module_map.lower_bound(identifier);
v_it!=symbol_table.symbol_module_map.upper_bound(identifier);
v_it++)
{
symbol_table_baset::symbolst::const_iterator s_it2 =
symbol_table.symbols.find(v_it->second);

if(s_it2==symbol_table.symbols.end())
{
throw errort() << "symbol `" << v_it->second << "' not found";
}

if(port_identifiers.find(s_it2->first) != port_identifiers.end())
{
}
else if(s_it2->second.type.id() == ID_module)
{
}
else
{
symbolt symbol(s_it2->second);

symbol.name=new_prefix+id2string(symbol.base_name);
symbol.module=smv_module.name;

if(smv_module.name == "smv::main")
{
symbol.pretty_name =
id2string(instance) + '.' + id2string(symbol.base_name);
}
else
{
symbol.pretty_name = strip_smv_prefix(symbol.name);
}

rename_map.insert(
std::pair<irep_idt, exprt>(s_it2->first, symbol.symbol_expr()));

var_identifiers.insert(symbol.name);

symbol_table.add(symbol);
}
}

// fix values (macros)

for(const auto &v_id : var_identifiers)
{
auto s_it2 = symbol_table.get_writeable(v_id);

if(s_it2==nullptr)
{
throw errort() << "symbol `" << v_id << "' not found";
}

symbolt &symbol=*s_it2;

if(!symbol.value.is_nil())
{
instantiate_rename(symbol.value, rename_map);
typecheck(symbol.value, OTHER);
convert_expr_to(symbol.value, symbol.type);
}
}

// get the transition system

const transt &trans=to_trans_expr(s_it->second.value);
rename_mapt parameter_map;

std::string old_prefix=id2string(s_it->first)+"::var::";

// do the transition system

if(!trans.invar().is_true())
{
exprt tmp(trans.invar());
instantiate_rename(tmp, rename_map);
smv_module.add_invar(tmp);
}

if(!trans.init().is_true())
{
exprt tmp(trans.init());
instantiate_rename(tmp, rename_map);
smv_module.add_init(tmp);
}

if(!trans.trans().is_true())
for(std::size_t i = 0; i < parameters.size(); i++)
{
exprt tmp(trans.trans());
instantiate_rename(tmp, rename_map);
smv_module.add_trans(tmp);
parameter_map.emplace(parameters[i], arguments[i]);
}

}

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

Function: smv_typecheckt::instantiate_rename

Inputs:

Outputs:

Purpose:
const std::string prefix = id2string(instance) + '.';

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

void smv_typecheckt::instantiate_rename(
exprt &expr,
const rename_mapt &rename_map)
{
for(auto &op : expr.operands())
instantiate_rename(op, rename_map);

if(expr.id()==ID_symbol || expr.id()==ID_next_symbol)
// copy the parse tree elements
for(auto &src_element : instantiated_module.elements)
{
const irep_idt &old_identifier=expr.get(ID_identifier);
bool next=expr.id()==ID_next_symbol;

rename_mapt::const_iterator it=
rename_map.find(old_identifier);
auto copy = src_element;

if(it!=rename_map.end())
{
expr=it->second;

if(next)
// replace the parameter identifiers,
// and add the prefix to non-parameter identifiers
copy.expr.visit_post(
[&parameter_map, &prefix](exprt &expr)
{
if(expr.id()==ID_symbol)
{
expr=it->second;
expr.id(ID_next_symbol);
}
else
if(expr.id() == ID_smv_identifier)
{
throw errort().with_location(expr.find_source_location())
<< "expected symbol expression here, but got "
<< to_string(it->second);
auto identifier = to_smv_identifier_expr(expr).identifier();
auto parameter_it = parameter_map.find(identifier);
if(parameter_it != parameter_map.end())
{
expr = parameter_it->second;
}
else
{
// add the prefix
to_smv_identifier_expr(expr).identifier(
prefix + id2string(identifier));
}
}
}
else
expr=it->second;
}
});

// add to main parse tree
smv_module.elements.push_back(copy);
}
}

Expand Down Expand Up @@ -2497,10 +2373,10 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)

define_map.clear();

// check for re-use of variables/defines/parameter identifiers
variable_checks(smv_module);
// expand the module hierarchy
flatten_hierarchy(smv_module);

// variables/defines first, can be used before their declaration
// Now do variables/defines, which can be used before their declaration
create_var_symbols(smv_module.elements);

// transition relation
Expand All @@ -2524,8 +2400,6 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
if(!element.is_var() && !element.is_ivar())
convert(element);

flatten_hierarchy(smv_module);

// we first need to collect all the defines

for(auto &element : smv_module.elements)
Expand Down Expand Up @@ -2631,6 +2505,13 @@ Function: smv_typecheckt::typecheck

void smv_typecheckt::typecheck()
{
if(module != "smv::main")
return;

// check all modules for duplicate identifiers
for(auto &module : smv_parse_tree.module_list)
variable_checks(module);

auto it = smv_parse_tree.module_map.find(module);

if(it == smv_parse_tree.module_map.end())
Expand Down
Loading