Skip to content

Commit

Permalink
Merge pull request #528 from diffblue/sequence1
Browse files Browse the repository at this point in the history 
property instantiation now returns largest timeframe used
  • Loading branch information
@tautschnig
tautschnig authored Jun 3, 2024
2 parents f05060e + 22418ab commit 5ce1ec8
Show file tree
Hide file tree
Showing 4 changed files with 79 additions and 120 deletions.
7 changes: 5 additions & 2 deletions regression/verilog/SVA/sequence1.desc
View file
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
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
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
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

0 comments on commit 5ce1ec8

Please sign in to comment.