Skip to content

property instantiation now returns largest timeframe used #528

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
tautschnig merged 1 commit into from
Jun 3, 2024
Merged

property instantiation now returns largest timeframe used #528

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
7 changes: 5 additions & 2 deletions regression/verilog/SVA/sequence1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,12 @@
KNOWNBUG
CORE
sequence1.sv
--bound 20 --numbered-trace
^\[main\.property\.1\] ##\[0:9\] main\.x == 100: REFUTED$
^Counterexample with 10 states:$
^main\.x@0 = 0$
^main\.x@9 = 9$
^EXIT=10$
^SIGNAL=0$
--
^warning: ignoring
--
The trace shown only has one state, but 10 are expected.
104 changes: 65 additions & 39 deletions src/trans-word-level/instantiate_word_level.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,8 @@ class wl_instantiatet
}

/// Instantiate the given expression for timeframe t
[[nodiscard]] exprt operator()(exprt expr, const mp_integer &t) const
[[nodiscard]] std::pair<mp_integer, exprt>
operator()(exprt expr, const mp_integer &t) const
{
return instantiate_rec(std::move(expr), t);
}
Expand All @@ -86,7 +87,8 @@ class wl_instantiatet
const mp_integer &no_timeframes;
const namespacet &ns;

[[nodiscard]] exprt instantiate_rec(exprt, const mp_integer &t) const;
[[nodiscard]] std::pair<mp_integer, exprt>
instantiate_rec(exprt, const mp_integer &t) const;
[[nodiscard]] typet instantiate_rec(typet, const mp_integer &t) const;
};

Expand Down Expand Up @@ -123,18 +125,20 @@ Function: wl_instantiatet::instantiate_rec

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

exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
std::pair<mp_integer, exprt>
wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
{
expr.type() = instantiate_rec(expr.type(), t);

if(expr.id() == ID_next_symbol)
{
expr.id(ID_symbol);
return timeframe_symbol(t + 1, to_symbol_expr(std::move(expr)));
auto u = t + 1;
return {u, timeframe_symbol(u, to_symbol_expr(std::move(expr)))};
}
else if(expr.id() == ID_symbol)
{
return timeframe_symbol(t, to_symbol_expr(std::move(expr)));
return {t, timeframe_symbol(t, to_symbol_expr(std::move(expr)))};
}
else if(expr.id()==ID_sva_cycle_delay) // ##[1:2] something
{
Expand All @@ -150,7 +154,7 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const

// Do we exceed the bound? Make it 'true'
if(u >= no_timeframes)
return true_exprt();
return {no_timeframes - 1, true_exprt()};
else
return instantiate_rec(sva_cycle_delay_expr.op(), u);
}
Expand All @@ -168,35 +172,29 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
else if(to_integer_non_constant(sva_cycle_delay_expr.to(), to))
throw "failed to convert sva_cycle_delay offsets";

// This is an 'or', and we let it fail if the bound is too small.
auto lower = t + from;
auto upper = t + to;

// Do we exceed the bound? Make it 'true'
if(upper >= no_timeframes)
return {no_timeframes - 1, true_exprt()};

exprt::operandst disjuncts;

for(mp_integer offset = from; offset < to; ++offset)
for(mp_integer u = lower; u <= upper; ++u)
{
auto u = t + offset;

if(u >= no_timeframes)
{
}
else
{
disjuncts.push_back(instantiate_rec(sva_cycle_delay_expr.op(), u));
}
disjuncts.push_back(
instantiate_rec(sva_cycle_delay_expr.op(), u).second);
}

return disjunction(disjuncts);
return {upper, disjunction(disjuncts)};
}
}
else if(expr.id()==ID_sva_sequence_concatenation)
{
// much like regular 'and'
expr.id(ID_and);

for(auto &op : expr.operands())
op = instantiate_rec(op, t);

return expr;
return instantiate_rec(expr, t);
}
else if(expr.id()==ID_sva_always)
{
Expand All @@ -206,10 +204,10 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const

for(auto u = t; u < no_timeframes; ++u)
{
conjuncts.push_back(instantiate_rec(op, u));
conjuncts.push_back(instantiate_rec(op, u).second);
}

return conjunction(conjuncts);
return {no_timeframes - 1, conjunction(conjuncts)};
}
else if(expr.id() == ID_X)
{
Expand All @@ -220,7 +218,7 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
return instantiate_rec(to_X_expr(expr).op(), next);
}
else
return true_exprt(); // works on NNF only
return {no_timeframes - 1, true_exprt()}; // works on NNF only
}
else if(expr.id() == ID_sva_eventually)
{
Expand All @@ -238,14 +236,14 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
// This is weak, and passes if any of the timeframes
// does not exist.
if(t + lower >= no_timeframes || t + upper >= no_timeframes)
return true_exprt();
return {no_timeframes - 1, true_exprt()};

exprt::operandst disjuncts = {};

for(mp_integer u = t + lower; u <= t + upper; ++u)
disjuncts.push_back(instantiate_rec(op, u));
disjuncts.push_back(instantiate_rec(op, u).second);

return disjunction(disjuncts);
return {no_timeframes - 1, disjunction(disjuncts)};
}
else if(
expr.id() == ID_sva_s_eventually || expr.id() == ID_F || expr.id() == ID_AF)
Expand Down Expand Up @@ -273,13 +271,13 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const

for(mp_integer j = k; j <= i; ++j)
{
disjuncts.push_back(instantiate_rec(p, j));
disjuncts.push_back(instantiate_rec(p, j).second);
}

conjuncts.push_back(disjunction(disjuncts));
}

return conjunction(conjuncts);
return {no_timeframes - 1, conjunction(conjuncts)};
}
else if(expr.id()==ID_sva_until ||
expr.id()==ID_sva_s_until)
Expand All @@ -292,19 +290,19 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const

// we expand: p U q <=> q || (p && X(p U q))
exprt tmp_q = to_binary_expr(expr).op1();
tmp_q = instantiate_rec(tmp_q, t);
tmp_q = instantiate_rec(tmp_q, t).second;

exprt expansion = to_binary_expr(expr).op0();
expansion = instantiate_rec(expansion, t);
expansion = instantiate_rec(expansion, t).second;

const auto next = t + 1;

if(next < no_timeframes)
{
expansion = and_exprt(expansion, instantiate_rec(expr, next));
expansion = and_exprt(expansion, instantiate_rec(expr, next).second);
}

return or_exprt(tmp_q, expansion);
return {no_timeframes - 1, or_exprt(tmp_q, expansion)};
}
else if(expr.id()==ID_sva_until_with ||
expr.id()==ID_sva_s_until_with)
Expand Down Expand Up @@ -335,7 +333,7 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
if(ticks > t)
{
// return the 'default value' for the type
return default_value(verilog_past.type());
return {t, default_value(verilog_past.type())};
}
else
{
Expand All @@ -344,9 +342,15 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
}
else
{
mp_integer max = t;
for(auto &op : expr.operands())
op = instantiate_rec(op, t);
return expr;
{
auto tmp = instantiate_rec(op, t);
op = tmp.second;
max = std::max(max, tmp.first);
}

return {max, expr};
}
}

Expand Down Expand Up @@ -386,5 +390,27 @@ exprt instantiate(
const namespacet &ns)
{
wl_instantiatet wl_instantiate(no_timeframes, ns);
return wl_instantiate(expr, t);
return wl_instantiate(expr, t).second;
}

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

Function: instantiate_property

Inputs:

Outputs:

Purpose:

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

std::pair<mp_integer, exprt> instantiate_property(
const exprt &expr,
const mp_integer &current,
const mp_integer &no_timeframes,
const namespacet &ns)
{
wl_instantiatet wl_instantiate(no_timeframes, ns);
return wl_instantiate(expr, current);
}
6 changes: 6 additions & 0 deletions src/trans-word-level/instantiate_word_level.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,12 @@ exprt instantiate(
const mp_integer &no_timeframes,
const namespacet &);

std::pair<mp_integer, exprt> instantiate_property(
const exprt &,
const mp_integer &current,
const mp_integer &no_timeframes,
const namespacet &);

std::string
timeframe_identifier(const mp_integer &timeframe, const irep_idt &identifier);

Expand Down
82 changes: 3 additions & 79 deletions src/trans-word-level/property.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,54 +78,6 @@ bool bmc_supports_property(const exprt &expr)

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

Function: max_property_obligation

Inputs:

Outputs:

Purpose:

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

static void property_obligations_rec(
const exprt &property_expr,
decision_proceduret &,
const mp_integer &current,
const mp_integer &no_timeframes,
const namespacet &,
std::map<mp_integer, exprt::operandst> &obligations);

static std::pair<mp_integer, exprt> max_property_obligation(
const exprt &property_expr,
decision_proceduret &solver,
const mp_integer &current,
const mp_integer &no_timeframes,
const namespacet &ns)
{
// Generate one obligation, equivalent to the conjunction
// for the maximum timeframe.

std::map<mp_integer, exprt::operandst> obligations;

property_obligations_rec(
property_expr, solver, current, no_timeframes, ns, obligations);

exprt::operandst conjuncts;
mp_integer max_timeframe = 0;

for(auto &[timeframe, exprs] : obligations)
{
max_timeframe = std::max(max_timeframe, timeframe);
for(auto &conjunct : exprs)
conjuncts.push_back(conjunct);
}

return std::pair<mp_integer, exprt>{max_timeframe, conjunction(conjuncts)};
}

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

Function: property_obligations_rec

Inputs:
Expand All @@ -146,17 +98,7 @@ static void property_obligations_rec(
{
PRECONDITION(current >= 0 && current < no_timeframes);

if(property_expr.id() == ID_X)
{
auto next = current + 1;
if(next < no_timeframes)
{
auto &op = to_X_expr(property_expr).op();
property_obligations_rec(
op, solver, next, no_timeframes, ns, obligations);
}
}
else if(
if(
property_expr.id() == ID_AG || property_expr.id() == ID_G ||
property_expr.id() == ID_sva_always)
{
Expand Down Expand Up @@ -254,28 +196,10 @@ static void property_obligations_rec(
property_obligations_rec(
op, solver, current, no_timeframes, ns, obligations);
}
else if(property_expr.id() == ID_or)
{
// generate one obligation, equivalent to the disjunction,
// for the maximum timeframe
mp_integer max_timeframe = 0;
exprt::operandst disjuncts;

for(auto &op : to_or_expr(property_expr).operands())
{
auto obligation =
max_property_obligation(op, solver, current, no_timeframes, ns);
max_timeframe = std::max(max_timeframe, obligation.first);
disjuncts.push_back(obligation.second);
}

obligations[max_timeframe].push_back(disjunction(disjuncts));
}
else
{
// current state property
exprt tmp = instantiate(property_expr, current, no_timeframes, ns);
obligations[current].push_back(tmp);
auto tmp = instantiate_property(property_expr, current, no_timeframes, ns);
obligations[tmp.first].push_back(tmp.second);
}
}

Expand Down