Skip to content

Commit f334106

Browse files
kroeningkroening
authored
Merge pull request #923 from diffblue/k-induction6-fix
Engine heuristic: fix for assumptions unsupported by k-induction
2 parents 4f09a7e + 600f348 commit f334106

18 files changed

+227
-26
lines changed

‎regression/ebmc/engine-heuristic/basic1.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
basic1.sv
3+
4+
^\[main\.a0\] always not s_eventually !main\.x: ASSUMED$
5+
^\[main\.p0\] always main\.x: PROVED up to bound 5$
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--

‎regression/ebmc/engine-heuristic/basic1.sv

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
module main(input clk, input x);
2+
3+
// not supported by k-induction
4+
a0: assume property (not s_eventually !x);
5+
6+
p0: assert property (x);
7+
8+
endmodule

‎regression/ebmc/engine-heuristic/basic2.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
basic2.sv
3+
4+
^\[main\.a0\] always not s_eventually !main\.y: UNSUPPORTED: unsupported by k-induction$
5+
^\[main\.a1\] always !main\.x: ASSUMED$
6+
^\[main\.p0\] always !main\.z: PROVED$
7+
^EXIT=0$
8+
^SIGNAL=0$
9+
--
10+
^warning: ignoring
11+
--

‎regression/ebmc/engine-heuristic/basic2.sv

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
module main(input clk, input x, input y);
2+
3+
reg z = 0;
4+
always_ff @(posedge clk) z <= z || x;
5+
6+
// unsupported assumption
7+
a0: assume property (not s_eventually !y);
8+
9+
// supported assumption
10+
a1: assume property (!x);
11+
12+
// inductive property
13+
p0: assert property (!z);
14+
15+
endmodule

‎regression/ebmc/engine-heuristic/basic3.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
basic3.sv
3+
4+
^\[main\.a0\] always not s_eventually !main\.x: ASSUMED$
5+
^\[main\.p0\] always 0: REFUTED$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--

‎regression/ebmc/engine-heuristic/basic3.sv

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
module main(input clk, input x);
2+
3+
// unsupported
4+
a0: assume property (not s_eventually !x);
5+
6+
// should fail
7+
p0: assert property (0);
8+
9+
endmodule

‎regression/ebmc/k-induction/k-induction-unsupported2.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ k-induction-unsupported2.sv
33
--module main --k-induction
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main\.p0\] always s_eventually main\.x == 10: FAILURE: property unsupported by k-induction$
6+
^\[main\.p0\] always s_eventually main\.x == 10: UNSUPPORTED: unsupported by k-induction$
77
^\[main\.p1\] always main\.x <= 10: PROVED$
88
--
99
^warning: ignoring

‎regression/ebmc/k-induction/k-induction6.desc

+4-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
1-
KNOWNBUG
1+
CORE
22
k-induction6.sv
3-
3+
--k-induction
4+
^\[main\.a0\] always not s_eventually !main\.x: UNSUPPORTED: unsupported by k-induction$
5+
^\[main\.p0\] always main\.x: INCONCLUSIVE$
46
^EXIT=10$
57
^SIGNAL=0$
68
--
79
^warning: ignoring
810
--
9-
The property should hold, but is reported as refuted.

‎regression/ebmc/k-induction/k-induction7.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
k-induction7.sv
3+
--k-induction
4+
^\[main\.a0\] always not s_eventually !main\.y: UNSUPPORTED: unsupported by k-induction$
5+
^\[main\.a1\] always !main\.x: ASSUMED$
6+
^\[main\.p0\] always !main\.z: PROVED$
7+
^EXIT=0$
8+
^SIGNAL=0$
9+
--
10+
^warning: ignoring
11+
--

‎regression/ebmc/k-induction/k-induction7.sv

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
module main(input clk, input x, input y);
2+
3+
reg z = 0;
4+
always_ff @(posedge clk) z <= z || x;
5+
6+
// unsupported assumption
7+
a0: assume property (not s_eventually !y);
8+
9+
// supported assumption
10+
a1: assume property (!x);
11+
12+
// inductive property
13+
p0: assert property (!z);
14+
15+
endmodule

‎src/ebmc/bdd_engine.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -180,7 +180,7 @@ property_checker_resultt bdd_enginet::operator()()
180180
try
181181
{
182182
// any properties left?
183-
if(!properties.has_unknown_property())
183+
if(!properties.has_unfinished_property())
184184
return property_checker_resultt{properties};
185185

186186
// possibly apply liveness-to-safety

‎src/ebmc/ebmc_properties.cpp

+10-7
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
1818

1919
std::string ebmc_propertiest::propertyt::status_as_string() const
2020
{
21+
auto suffix = failure_reason.has_value() ? ": " + failure_reason.value() : "";
22+
2123
switch(status)
2224
{
2325
case statust::ASSUMED:
@@ -31,14 +33,15 @@ std::string ebmc_propertiest::propertyt::status_as_string() const
3133
case statust::REFUTED_WITH_BOUND:
3234
return "REFUTED up to bound " + std::to_string(bound);
3335
case statust::UNKNOWN:
34-
return "UNKNOWN";
36+
return "UNKNOWN" + suffix;
37+
case statust::UNSUPPORTED:
38+
return "UNSUPPORTED" + suffix;
3539
case statust::INCONCLUSIVE:
36-
return "INCONCLUSIVE";
40+
return "INCONCLUSIVE" + suffix;
3741
case statust::FAILURE:
38-
return failure_reason.has_value() ? "FAILURE: " + failure_reason.value()
39-
: "FAILURE";
42+
return "FAILURE" + suffix;
4043
case statust::DROPPED:
41-
return "DROPPED";
44+
return "DROPPED" + suffix;
4245
case statust::DISABLED:
4346
default:
4447
UNREACHABLE;
@@ -78,9 +81,9 @@ ebmc_propertiest ebmc_propertiest::from_transition_system(
7881
id2string(symbol.location.get_comment());
7982

8083
// Don't try to prove assumption properties.
81-
if(symbol.value.id() == ID_sva_assume)
84+
if(properties.properties.back().is_assumption())
8285
{
83-
properties.properties.back().status = propertyt::statust::ASSUMED;
86+
properties.properties.back().assumed();
8487
properties.properties.back().normalized_expr =
8588
normalize_property(to_sva_assume_expr(symbol.value).op());
8689
}

‎src/ebmc/ebmc_properties.h

+70-3
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ class ebmc_propertiest
4040
UNKNOWN, // no work done yet
4141
DISABLED, // turned off by user
4242
ASSUMED, // property is assumed to be true, unbounded
43+
UNSUPPORTED, // property is unsupported
4344
PROVED, // property is true, unbounded
4445
PROVED_WITH_BOUND, // property is true, with bound
4546
REFUTED, // property is false, possibly counterexample
@@ -98,24 +99,38 @@ class ebmc_propertiest
9899
return status == statust::FAILURE;
99100
}
100101

102+
bool is_unsupported() const
103+
{
104+
return status == statust::UNSUPPORTED;
105+
}
106+
101107
bool is_inconclusive() const
102108
{
103109
return status == statust::INCONCLUSIVE;
104110
}
105111

112+
void assumed()
113+
{
114+
status = statust::ASSUMED;
115+
failure_reason = {};
116+
}
117+
106118
void unknown()
107119
{
108120
status = statust::UNKNOWN;
121+
failure_reason = {};
109122
}
110123

111124
void disable()
112125
{
113126
status = statust::DISABLED;
127+
failure_reason = {};
114128
}
115129

116130
void proved()
117131
{
118132
status = statust::PROVED;
133+
failure_reason = {};
119134
}
120135

121136
void proved_with_bound(std::size_t _bound)
@@ -127,17 +142,20 @@ class ebmc_propertiest
127142
void refuted()
128143
{
129144
status = statust::REFUTED;
145+
failure_reason = {};
130146
}
131147

132148
void refuted_with_bound(std::size_t _bound)
133149
{
134150
status = statust::REFUTED_WITH_BOUND;
135151
bound = _bound;
152+
failure_reason = {};
136153
}
137154

138155
void drop()
139156
{
140157
status = statust::DROPPED;
158+
failure_reason = {};
141159
}
142160

143161
void failure(const std::optional<std::string> &reason = {})
@@ -146,9 +164,16 @@ class ebmc_propertiest
146164
failure_reason = reason;
147165
}
148166

167+
void unsupported(const std::optional<std::string> &reason = {})
168+
{
169+
status = statust::UNSUPPORTED;
170+
failure_reason = reason;
171+
}
172+
149173
void inconclusive()
150174
{
151175
status = statust::INCONCLUSIVE;
176+
failure_reason = {};
152177
}
153178

154179
std::string status_as_string() const;
@@ -164,16 +189,30 @@ class ebmc_propertiest
164189
{
165190
return ::is_exists_path(original_expr);
166191
}
192+
193+
bool is_assumption() const
194+
{
195+
return original_expr.id() == ID_sva_assume;
196+
}
167197
};
168198

169199
typedef std::list<propertyt> propertiest;
170200
propertiest properties;
171201

172-
bool has_unknown_property() const
202+
bool has_unfinished_property() const
173203
{
174204
for(const auto &p : properties)
175-
if(p.is_unknown())
205+
{
206+
if(p.is_assumption())
207+
{
208+
}
209+
else if(
210+
p.is_unknown() || p.is_unsupported() || p.is_failure() ||
211+
p.is_inconclusive())
212+
{
176213
return true;
214+
}
215+
}
177216

178217
return false;
179218
}
@@ -209,12 +248,40 @@ class ebmc_propertiest
209248
return result;
210249
}
211250

212-
void reset_failure_to_unknown()
251+
/// Resets properties/assumptions in FAILURE state to
252+
/// ASSUMED/UNKNOWN respectively.
253+
void reset_failure()
213254
{
214255
for(auto &p : properties)
215256
if(p.is_failure())
257+
{
258+
if(p.is_assumption())
259+
p.assumed();
260+
else
261+
p.unknown();
262+
}
263+
}
264+
265+
/// Resets properties in INCONCLUSIVE state to UNKNOWN.
266+
void reset_inconclusive()
267+
{
268+
for(auto &p : properties)
269+
if(p.is_inconclusive())
216270
p.unknown();
217271
}
272+
273+
/// Resets properties in UNSUPPORTED state to UNKNOWN/ASSUMED.
274+
void reset_unsupported()
275+
{
276+
for(auto &p : properties)
277+
if(p.is_unsupported())
278+
{
279+
if(p.is_assumption())
280+
p.assumed();
281+
else
282+
p.unknown();
283+
}
284+
}
218285
};
219286

220287
#endif // CPROVER_EBMC_PROPERTIES_H

‎src/ebmc/k_induction.cpp

+33-3
Original file line numberDiff line numberDiff line change
@@ -170,18 +170,44 @@ Function: k_inductiont::operator()
170170

171171
void k_inductiont::operator()()
172172
{
173+
// Unsupported assumption? Mark as such.
174+
bool assumption_unsupported = false;
175+
for(auto &property : properties.properties)
176+
{
177+
if(!supported(property) && property.is_assumed())
178+
{
179+
assumption_unsupported = true;
180+
property.unsupported("unsupported by k-induction");
181+
}
182+
}
183+
173184
// Fail unsupported properties
174185
for(auto &property : properties.properties)
175186
{
176-
if(!supported(property))
177-
property.failure("property unsupported by k-induction");
187+
if(
188+
!supported(property) && !property.is_assumed() && !property.is_disabled())
189+
{
190+
property.unsupported("unsupported by k-induction");
191+
}
178192
}
179193

180194
// do induction base
181195
induction_base();
182196

183197
// do induction step
184198
induction_step();
199+
200+
// Any refuted properties are really inconclusive if there are
201+
// unsupported assumptions, as the assumption might have
202+
// proven the property.
203+
if(assumption_unsupported)
204+
{
205+
for(auto &property : properties.properties)
206+
{
207+
if(property.is_refuted())
208+
property.inconclusive();
209+
}
210+
}
185211
}
186212

187213
/*******************************************************************\
@@ -231,8 +257,12 @@ void k_inductiont::induction_step()
231257

232258
for(auto &p_it : properties.properties)
233259
{
234-
if(p_it.is_disabled() || p_it.is_failure() || p_it.is_assumed())
260+
if(
261+
p_it.is_disabled() || p_it.is_failure() || p_it.is_assumed() ||
262+
p_it.is_unsupported())
263+
{
235264
continue;
265+
}
236266

237267
// If it's not failed, then it's supported.
238268
DATA_INVARIANT(supported(p_it), "property must be supported");

0 commit comments

Comments
 (0)