Skip to content

Commit 46c0b0a

Browse files
kroeningkroening
authored
Merge pull request #7263 from diffblue/chc_inductiveness
CHC solver: extract inductiveness check
2 parents 22c547a + e34cb8a commit 46c0b0a

File tree

6 files changed

+494
-344
lines changed

6 files changed

+494
-344
lines changed

‎src/cprover/Makefile

+2
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ SRC = address_taken.cpp \
1313
format_hooks.cpp \
1414
free_symbols.cpp \
1515
help_formatter.cpp \
16+
inductiveness.cpp \
1617
instrument_contracts.cpp \
1718
instrument_given_invariants.cpp \
1819
may_alias.cpp \
@@ -27,6 +28,7 @@ SRC = address_taken.cpp \
2728
state_encoding_targets.cpp \
2829
solver.cpp \
2930
solver_progress.cpp \
31+
solver_types.cpp \
3032
variable_encoding.cpp \
3133
wcwidth.c \
3234
# Empty last line

‎src/cprover/inductiveness.cpp

+233
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,233 @@
1+
/*******************************************************************\
2+
3+
Module: Inductiveness
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Inductiveness
11+
12+
#include "inductiveness.h"
13+
14+
#include <util/arith_tools.h>
15+
#include <util/cout_message.h>
16+
#include <util/format_expr.h>
17+
#include <util/simplify_expr.h>
18+
19+
#include <solvers/sat/satcheck.h>
20+
21+
#include "axioms.h"
22+
#include "bv_pointers_wide.h"
23+
#include "console.h"
24+
#include "counterexample_found.h"
25+
#include "propagate.h"
26+
#include "solver.h"
27+
28+
#include <iomanip>
29+
#include <iostream>
30+
31+
bool is_subsumed(
32+
const std::unordered_set<exprt, irep_hash> &a1,
33+
const std::unordered_set<exprt, irep_hash> &a2,
34+
const exprt &b,
35+
const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
36+
bool verbose,
37+
const namespacet &ns)
38+
{
39+
if(b.is_true())
40+
return true; // anything subsumes 'true'
41+
42+
if(a1.find(false_exprt()) != a1.end())
43+
return true; // 'false' subsumes anything
44+
45+
if(a1.find(b) != a1.end())
46+
return true; // b is subsumed by a conjunct in a
47+
48+
cout_message_handlert message_handler;
49+
#if 0
50+
message_handler.set_verbosity(verbose ? 10 : 1);
51+
#else
52+
message_handler.set_verbosity(1);
53+
#endif
54+
satcheckt satcheck(message_handler);
55+
bv_pointers_widet solver(ns, satcheck, message_handler);
56+
axiomst axioms(solver, address_taken, verbose, ns);
57+
58+
// check if a => b is valid,
59+
// or (!a || b) is valid,
60+
// or (a && !b) is unsat
61+
for(auto &a_conjunct : a1)
62+
axioms << a_conjunct;
63+
64+
for(auto &a_conjunct : a2)
65+
axioms << a_conjunct;
66+
67+
axioms.set_to_false(b);
68+
69+
// instantiate our axioms
70+
axioms.emit();
71+
72+
// now run solver
73+
switch(solver())
74+
{
75+
case decision_proceduret::resultt::D_SATISFIABLE:
76+
if(verbose)
77+
show_assignment(solver);
78+
return false;
79+
case decision_proceduret::resultt::D_UNSATISFIABLE:
80+
return true;
81+
case decision_proceduret::resultt::D_ERROR:
82+
throw "error reported by solver";
83+
}
84+
85+
UNREACHABLE; // to silence a warning
86+
}
87+
88+
std::size_t count_frame(const workt::patht &path, frame_reft f)
89+
{
90+
return std::count_if(path.begin(), path.end(), [f](const frame_reft &frame) {
91+
return f == frame;
92+
});
93+
}
94+
95+
inductiveness_resultt inductiveness_check(
96+
std::vector<framet> &frames,
97+
const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
98+
const solver_optionst &solver_options,
99+
const namespacet &ns,
100+
std::vector<propertyt> &properties,
101+
std::size_t property_index)
102+
{
103+
const auto frame_map = build_frame_map(frames);
104+
auto &property = properties[property_index];
105+
106+
// add properties proven so far as auxiliaries
107+
for(std::size_t i = 0; i < property_index; i++)
108+
{
109+
const auto &p = properties[i];
110+
if(p.status == propertyt::PASS)
111+
frames[p.frame.index].add_auxiliary(p.condition);
112+
}
113+
114+
std::vector<workt> queue;
115+
std::vector<workt> dropped;
116+
117+
auto propagator =
118+
[&frames,
119+
&frame_map,
120+
&queue,
121+
&dropped,
122+
&address_taken,
123+
&solver_options,
124+
&ns](
125+
const symbol_exprt &symbol, exprt invariant, const workt::patht &path) {
126+
auto frame_ref = find_frame(frame_map, symbol);
127+
auto &f = frames[frame_ref.index];
128+
129+
#if 0
130+
if(solver_options.verbose)
131+
{
132+
std::cout << "F: " << format(symbol) << " <- " << format(invariant)
133+
<< '\n';
134+
}
135+
#endif
136+
137+
if(solver_options.verbose)
138+
{
139+
// print the current invariants in the frame
140+
for(const auto &invariant : f.invariants)
141+
{
142+
std::cout << consolet::faint << consolet::blue;
143+
std::cout << 'I' << std::setw(2) << frame_ref.index << ' ';
144+
std::cout << format(invariant);
145+
std::cout << consolet::reset << '\n';
146+
}
147+
}
148+
149+
if(solver_options.verbose)
150+
std::cout << "\u2192" << consolet::faint << std::setw(2)
151+
<< frame_ref.index << consolet::reset << ' ';
152+
153+
// trivially true?
154+
if(invariant.is_true())
155+
{
156+
if(solver_options.verbose)
157+
std::cout << "trivial\n";
158+
}
159+
else if(is_subsumed(
160+
f.invariants_set,
161+
f.auxiliaries_set,
162+
invariant,
163+
address_taken,
164+
solver_options.verbose,
165+
ns))
166+
{
167+
if(solver_options.verbose)
168+
std::cout << "subsumed " << format(invariant) << '\n';
169+
}
170+
else if(count_frame(path, frame_ref) > solver_options.loop_limit)
171+
{
172+
// loop limit exceeded, drop it
173+
if(solver_options.verbose)
174+
std::cout << consolet::red << "dropped" << consolet::reset << ' '
175+
<< format(invariant) << '\n';
176+
dropped.emplace_back(frame_ref, invariant, path);
177+
}
178+
else
179+
{
180+
// propagate
181+
if(solver_options.verbose)
182+
std::cout << format(invariant) << '\n';
183+
184+
// store in frame
185+
frames[frame_ref.index].add_invariant(invariant);
186+
187+
// add to queue
188+
auto new_path = path;
189+
new_path.push_back(frame_ref);
190+
queue.emplace_back(f.ref, std::move(invariant), std::move(new_path));
191+
}
192+
};
193+
194+
// stick non-true frames into the queue
195+
for(std::size_t frame_index = 0; frame_index < frames.size(); frame_index++)
196+
{
197+
frame_reft frame_ref(frame_index);
198+
for(auto &cond : frames[frame_index].invariants)
199+
queue.emplace_back(frame_ref, cond, workt::patht{frame_ref});
200+
}
201+
202+
while(!queue.empty())
203+
{
204+
auto work = queue.back();
205+
queue.pop_back();
206+
207+
#if 0
208+
if(solver_options.verbose)
209+
{
210+
dump(frames, property, true, true);
211+
std::cout << '\n';
212+
}
213+
#endif
214+
215+
auto counterexample_found = ::counterexample_found(
216+
frames, work, address_taken, solver_options.verbose, ns);
217+
218+
if(counterexample_found)
219+
{
220+
property.trace = counterexample_found.value();
221+
return inductiveness_resultt::BASE_CASE_FAIL;
222+
}
223+
224+
propagate(
225+
frames, work, address_taken, solver_options.verbose, ns, propagator);
226+
}
227+
228+
// did we drop anything?
229+
if(dropped.empty())
230+
return inductiveness_resultt::INDUCTIVE;
231+
else
232+
return inductiveness_resultt::STEP_CASE_FAIL;
233+
}

‎src/cprover/inductiveness.h

+34
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
/*******************************************************************\
2+
3+
Module: Inductiveness
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Inductiveness
11+
12+
#ifndef CPROVER_CPROVER_INDUCTIVENESS_H
13+
#define CPROVER_CPROVER_INDUCTIVENESS_H
14+
15+
#include "solver_types.h"
16+
17+
class solver_optionst;
18+
19+
enum inductiveness_resultt
20+
{
21+
INDUCTIVE,
22+
BASE_CASE_FAIL,
23+
STEP_CASE_FAIL
24+
};
25+
26+
inductiveness_resultt inductiveness_check(
27+
std::vector<framet> &frames,
28+
const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
29+
const solver_optionst &,
30+
const namespacet &,
31+
std::vector<propertyt> &properties,
32+
std::size_t property_index);
33+
34+
#endif // CPROVER_CPROVER_INDUCTIVENESS_H

0 commit comments

Comments
 (0)