Skip to content

Commit a7b7f1d

Browse files
kroeningkroening
committed
BMC without assumptions
1 parent a7b8510 commit a7b7f1d

File tree

5 files changed

+194
-64
lines changed

5 files changed

+194
-64
lines changed

‎src/ebmc/bmc.cpp‎

Lines changed: 187 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,181 @@ Author: Daniel Kroening, [email protected]
1717
#include <chrono>
1818
#include <fstream>
1919

20+
void bmc_with_assumptions(
21+
std::size_t bound,
22+
const transition_systemt &transition_system,
23+
ebmc_propertiest &properties,
24+
decision_proceduret &solver,
25+
message_handlert &message_handler)
26+
{
27+
messaget message(message_handler);
28+
const namespacet ns(transition_system.symbol_table);
29+
30+
// Use assumptions to check the properties separately
31+
32+
for(auto &property : properties.properties)
33+
{
34+
if(property.is_disabled() || property.is_failure() || property.is_assumed())
35+
{
36+
continue;
37+
}
38+
39+
message.status() << "Checking " << property.name << messaget::eom;
40+
41+
auto assumption = not_exprt{conjunction(property.timeframe_handles)};
42+
43+
decision_proceduret::resultt dec_result = solver(assumption);
44+
45+
switch(dec_result)
46+
{
47+
case decision_proceduret::resultt::D_SATISFIABLE:
48+
if(property.is_exists_path())
49+
{
50+
property.proved();
51+
message.result() << "SAT: path found" << messaget::eom;
52+
}
53+
else // universal path property
54+
{
55+
property.refuted();
56+
message.result() << "SAT: counterexample found" << messaget::eom;
57+
}
58+
59+
property.witness_trace = compute_trans_trace(
60+
property.timeframe_handles,
61+
solver,
62+
bound + 1,
63+
ns,
64+
transition_system.main_symbol->name);
65+
break;
66+
67+
case decision_proceduret::resultt::D_UNSATISFIABLE:
68+
if(property.is_exists_path())
69+
{
70+
message.result() << "UNSAT: No path found within bound"
71+
<< messaget::eom;
72+
property.refuted_with_bound(bound);
73+
}
74+
else // universal path property
75+
{
76+
message.result() << "UNSAT: No counterexample found within bound"
77+
<< messaget::eom;
78+
property.proved_with_bound(bound);
79+
}
80+
break;
81+
82+
case decision_proceduret::resultt::D_ERROR:
83+
message.error() << "Error from decision procedure" << messaget::eom;
84+
property.failure();
85+
break;
86+
87+
default:
88+
property.failure();
89+
throw ebmc_errort() << "Unexpected result from decision procedure";
90+
}
91+
}
92+
}
93+
94+
void bmc_without_assumptions(
95+
std::size_t bound,
96+
const transition_systemt &transition_system,
97+
ebmc_propertiest &properties,
98+
decision_proceduret &solver,
99+
message_handlert &message_handler)
100+
{
101+
messaget message(message_handler);
102+
const namespacet ns(transition_system.symbol_table);
103+
104+
auto trace_found = [&solver](const ebmc_propertiest::propertyt &property)
105+
{
106+
for(auto &h : property.timeframe_handles)
107+
if(solver.get(h).is_false())
108+
return true;
109+
return false;
110+
};
111+
112+
while(true)
113+
{
114+
// At least one of the remaining properties
115+
// should be falsified.
116+
exprt::operandst disjuncts;
117+
118+
for(auto &property : properties.properties)
119+
{
120+
if(property.is_unknown())
121+
{
122+
for(auto &h : property.timeframe_handles)
123+
disjuncts.push_back(not_exprt{h});
124+
}
125+
}
126+
127+
solver.set_to_true(disjunction(disjuncts));
128+
129+
decision_proceduret::resultt dec_result = solver();
130+
131+
switch(dec_result)
132+
{
133+
case decision_proceduret::resultt::D_SATISFIABLE:
134+
// Found a trace for at least one further property with unknown state
135+
message.result() << "SAT: path found" << messaget::eom;
136+
137+
for(auto &property : properties.properties)
138+
{
139+
if(property.is_unknown() && trace_found(property))
140+
{
141+
if(property.is_exists_path())
142+
property.proved();
143+
else // universal path property
144+
property.refuted();
145+
146+
property.witness_trace = compute_trans_trace(
147+
property.timeframe_handles,
148+
solver,
149+
bound + 1,
150+
ns,
151+
transition_system.main_symbol->name);
152+
}
153+
}
154+
break; // next iteration of while loop
155+
156+
case decision_proceduret::resultt::D_UNSATISFIABLE:
157+
message.result() << "UNSAT: No path found within bound" << messaget::eom;
158+
159+
for(auto &property : properties.properties)
160+
{
161+
if(property.is_unknown())
162+
{
163+
if(property.is_exists_path())
164+
property.refuted_with_bound(bound);
165+
else // universal path property
166+
property.proved_with_bound(bound);
167+
}
168+
}
169+
return;
170+
171+
case decision_proceduret::resultt::D_ERROR:
172+
for(auto &property : properties.properties)
173+
{
174+
if(property.is_unknown())
175+
property.failure();
176+
}
177+
message.error() << "Error from decision procedure" << messaget::eom;
178+
return;
179+
180+
default:
181+
for(auto &property : properties.properties)
182+
{
183+
if(property.is_unknown())
184+
property.failure();
185+
}
186+
throw ebmc_errort() << "Unexpected result from decision procedure";
187+
}
188+
}
189+
}
190+
20191
void bmc(
21192
std::size_t bound,
22193
bool convert_only,
194+
bool bmc_with_assumptions,
23195
const transition_systemt &transition_system,
24196
ebmc_propertiest &properties,
25197
const ebmc_solver_factoryt &solver_factory,
@@ -78,8 +250,14 @@ void bmc(
78250
{
79251
for(const auto &property : properties.properties)
80252
{
81-
if(!property.is_disabled())
253+
if(property.is_assumed())
254+
{
255+
solver.set_to_true(conjunction(property.timeframe_handles));
256+
}
257+
else if(!property.is_disabled())
258+
{
82259
solver.set_to_false(conjunction(property.timeframe_handles));
260+
}
83261
}
84262

85263
// Call decision_proceduret::dec_solve to finish the conversion
@@ -93,69 +271,15 @@ void bmc(
93271

94272
auto sat_start_time = std::chrono::steady_clock::now();
95273

96-
// Use assumptions to check the properties separately
97-
98-
for(auto &property : properties.properties)
274+
if(bmc_with_assumptions)
99275
{
100-
if(
101-
property.is_disabled() || property.is_failure() ||
102-
property.is_assumed())
103-
{
104-
continue;
105-
}
106-
107-
message.status() << "Checking " << property.name << messaget::eom;
108-
109-
auto assumption = not_exprt{conjunction(property.timeframe_handles)};
110-
111-
decision_proceduret::resultt dec_result = solver(assumption);
112-
113-
switch(dec_result)
114-
{
115-
case decision_proceduret::resultt::D_SATISFIABLE:
116-
if(property.is_exists_path())
117-
{
118-
property.proved();
119-
message.result() << "SAT: path found" << messaget::eom;
120-
}
121-
else // universal path property
122-
{
123-
property.refuted();
124-
message.result() << "SAT: counterexample found" << messaget::eom;
125-
}
126-
127-
property.witness_trace = compute_trans_trace(
128-
property.timeframe_handles,
129-
solver,
130-
bound + 1,
131-
ns,
132-
transition_system.main_symbol->name);
133-
break;
134-
135-
case decision_proceduret::resultt::D_UNSATISFIABLE:
136-
if(property.is_exists_path())
137-
{
138-
message.result() << "UNSAT: No path found within bound"
139-
<< messaget::eom;
140-
property.refuted_with_bound(bound);
141-
}
142-
else // universal path property
143-
{
144-
message.result() << "UNSAT: No counterexample found within bound"
145-
<< messaget::eom;
146-
property.proved_with_bound(bound);
147-
}
148-
break;
149-
150-
case decision_proceduret::resultt::D_ERROR:
151-
message.error() << "Error from decision procedure" << messaget::eom;
152-
property.failure();
153-
break;
154-
155-
default:
156-
property.failure();
157-
throw ebmc_errort() << "Unexpected result from decision procedure";
158-
}
276+
::bmc_with_assumptions(
277+
bound, transition_system, properties, solver, message_handler);
278+
}
279+
else
280+
{
281+
::bmc_without_assumptions(
282+
bound, transition_system, properties, solver, message_handler);
159283
}
160284

161285
auto sat_stop_time = std::chrono::steady_clock::now();

‎src/ebmc/bmc.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ class transition_systemt;
2222
void bmc(
2323
std::size_t bound,
2424
bool convert_only,
25+
bool bmc_with_assumptions,
2526
const transition_systemt &,
2627
ebmc_propertiest &,
2728
const ebmc_solver_factoryt &,

‎src/ebmc/ebmc_parse_options.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ class ebmc_parse_optionst:public parse_options_baset
4646
"(compute-ct)(dot-netlist)(smv-netlist)(vcd):"
4747
"(random-traces)(trace-steps):(random-seed):(traces):"
4848
"(random-trace)(random-waveform)"
49+
"(bmc-with-assumptions)"
4950
"(liveness-to-safety)"
5051
"I:D:(preprocess)(systemverilog)(vl2smv-extensions)"
5152
"(warn-implicit-nets)",

‎src/ebmc/k_induction.cpp‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -202,7 +202,8 @@ void k_inductiont::induction_base()
202202

203203
bmc(
204204
k,
205-
false,
205+
false, // convert_only
206+
false, // bmc_with_assumptions
206207
transition_system,
207208
properties,
208209
solver_factory,

‎src/ebmc/property_checker.cpp‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -80,9 +80,12 @@ property_checker_resultt word_level_bmc(
8080
if(properties.properties.empty())
8181
throw "no properties";
8282

83+
bool bmc_with_assumptions = cmdline.isset("bmc-with-assumptions");
84+
8385
bmc(
8486
bound,
8587
convert_only,
88+
bmc_with_assumptions,
8689
transition_system,
8790
properties,
8891
solver_factory,

0 commit comments

Comments
 (0)