Skip to content

SMV: move mechanism for next(...) #1359

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
Oct 24, 2025
Merged

SMV: move mechanism for next(...) #1359

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
60 changes: 26 additions & 34 deletions src/smvlang/smv_typecheck.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,7 @@ class smv_typecheckt:public typecheckt
INIT,
INVAR,
TRANS,
TRANS_NEXT,
OTHER,
LTL,
CTL
Expand All @@ -65,8 +66,7 @@ class smv_typecheckt:public typecheckt
void convert_defines(exprt::operandst &invar);
void convert_define(const irep_idt &identifier);

typedef enum { NORMAL, NEXT } expr_modet;
void convert(exprt &, expr_modet);
void convert(exprt &);

void typecheck(exprt &, modet);
void typecheck_op(exprt &, const typet &, modet);
Expand Down Expand Up @@ -201,7 +201,7 @@ void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module)
static_cast<exprt &>(static_cast<irept &>(item.expr.type()));

for(auto &op : inst.operands())
convert(op, NORMAL);
convert(op);

auto instance_base_name = to_symbol_expr(item.expr).get_identifier();

Expand Down Expand Up @@ -594,17 +594,27 @@ Function: smv_typecheckt::typecheck_expr_rec

void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
{
if(expr.id()==ID_symbol ||
expr.id()==ID_next_symbol)
if(expr.id() == ID_smv_next)
{
if(mode == TRANS_NEXT)
{
throw errort().with_location(expr.find_source_location())
<< "next(next(...)) encountered";
}

// next_symbol is only allowed in TRANS mode
if(expr.id() == ID_next_symbol && mode != TRANS && mode != OTHER)
if(mode != TRANS && mode != OTHER)
throw errort().with_location(expr.find_source_location())
<< "next(...) is not allowed here";

const irep_idt &identifier=expr.get(ID_identifier);
bool next=expr.id()==ID_next_symbol;

expr = to_unary_expr(expr).op();

typecheck_expr_rec(expr, TRANS_NEXT);
}
else if(expr.id() == ID_symbol || expr.id() == ID_next_symbol)
{
const irep_idt &identifier = expr.get(ID_identifier);

if(define_map.find(identifier)!=define_map.end())
convert_define(identifier);

Expand All @@ -616,12 +626,15 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
<< "variable `" << identifier << "' not found";
}

if(mode == TRANS_NEXT)
expr.id(ID_next_symbol);

symbolt &symbol=*s_it;

assert(symbol.type.is_not_nil());
expr.type()=symbol.type;

if(mode==INIT || (mode==TRANS && next))
if(mode == INIT || mode == TRANS_NEXT)
{
if(symbol.module==module)
{
Expand Down Expand Up @@ -1683,28 +1696,10 @@ Function: smv_typecheckt::convert

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

void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
void smv_typecheckt::convert(exprt &expr)
{
if(expr.id() == ID_smv_next)
{
if(expr_mode!=NORMAL)
{
throw errort().with_location(expr.find_source_location())
<< "next(next(...)) encountered";
}

assert(expr.operands().size()==1);

exprt tmp;
tmp.swap(to_unary_expr(expr).op());
expr.swap(tmp);

convert(expr, NEXT);
return;
}

for(auto &op : expr.operands())
convert(op, expr_mode);
convert(op);

if(expr.id()==ID_symbol)
{
Expand All @@ -1716,9 +1711,6 @@ void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
std::string id = module + "::var::" + identifier;

expr.set(ID_identifier, id);

if(expr_mode == NEXT)
expr.id(ID_next_symbol);
}
else if(expr.id()=="smv_nondet_choice" ||
expr.id()=="smv_union")
Expand Down Expand Up @@ -1898,7 +1890,7 @@ Function: smv_typecheckt::convert
void smv_typecheckt::convert(
smv_parse_treet::modulet::itemt &item)
{
convert(item.expr, NORMAL);
convert(item.expr);
}

/*******************************************************************\
Expand Down
Loading