Skip to content

Commit 4b896ba

Browse files
peterschrammelpeterschrammel
committed
Factor out goto_symex_property_decider
Provides functionality close to solvers/prop/cover_goals but without callbacks. It allows us to iteratively get all counterexamples for a set of properties on a fixed equation. This is used as a component by multi-path and single-path symex checkers.
1 parent 06e364a commit 4b896ba

5 files changed

+282
-181
lines changed

‎src/goto-checker/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ SRC = bmc_util.cpp \
22
counterexample_beautification.cpp \
33
cover_goals_report_util.cpp \
44
incremental_goto_checker.cpp \
5+
goto_symex_property_decider.cpp \
56
goto_trace_storage.cpp \
67
goto_verifier.cpp \
78
multi_path_symex_checker.cpp \

‎src/goto-checker/goto_symex_property_decider.cpp

Lines changed: 162 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,162 @@
1+
/*******************************************************************\
2+
3+
Module: Property Decider for Goto-Symex
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Property Decider for Goto-Symex
11+
12+
#include "goto_symex_property_decider.h"
13+
14+
goto_symex_property_decidert::goto_symex_property_decidert(
15+
const optionst &options,
16+
ui_message_handlert &ui_message_handler,
17+
symex_target_equationt &equation,
18+
const namespacet &ns)
19+
: options(options), ui_message_handler(ui_message_handler), equation(equation)
20+
{
21+
solver_factoryt solvers(
22+
options,
23+
ns,
24+
ui_message_handler,
25+
ui_message_handler.get_ui() == ui_message_handlert::uit::XML_UI);
26+
solver = solvers.get_solver();
27+
solver->prop_conv().set_message_handler(ui_message_handler);
28+
}
29+
30+
exprt goto_symex_property_decidert::goalt::as_expr() const
31+
{
32+
std::vector<exprt> tmp;
33+
tmp.reserve(instances.size());
34+
for(const auto &inst : instances)
35+
tmp.push_back(literal_exprt(inst->cond_literal));
36+
return conjunction(tmp);
37+
}
38+
39+
void goto_symex_property_decidert::
40+
update_properties_goals_from_symex_target_equation(propertiest &properties)
41+
{
42+
for(symex_target_equationt::SSA_stepst::iterator it =
43+
equation.SSA_steps.begin();
44+
it != equation.SSA_steps.end();
45+
++it)
46+
{
47+
if(it->is_assert())
48+
{
49+
irep_idt property_id = it->get_property_id();
50+
CHECK_RETURN(!property_id.empty());
51+
52+
// consider goal instance if it is in the given properties
53+
auto property_pair_it = properties.find(property_id);
54+
if(
55+
property_pair_it != properties.end() &&
56+
is_property_to_check(property_pair_it->second.status))
57+
{
58+
// it's going to be checked, but we don't know the status yet
59+
property_pair_it->second.status |= property_statust::UNKNOWN;
60+
goal_map[property_id].instances.push_back(it);
61+
}
62+
}
63+
}
64+
}
65+
66+
void goto_symex_property_decidert::convert_goals()
67+
{
68+
for(auto &goal_pair : goal_map)
69+
{
70+
// Our goal is to falsify a property, i.e., we will
71+
// add the negation of the property as goal.
72+
goal_pair.second.condition =
73+
!solver->prop_conv().convert(goal_pair.second.as_expr());
74+
}
75+
}
76+
77+
void goto_symex_property_decidert::freeze_goal_variables()
78+
{
79+
for(const auto &goal_pair : goal_map)
80+
{
81+
if(!goal_pair.second.condition.is_constant())
82+
solver->prop_conv().set_frozen(goal_pair.second.condition);
83+
}
84+
}
85+
86+
void goto_symex_property_decidert::add_constraint_from_goals(
87+
std::function<bool(const irep_idt &)> select_property)
88+
{
89+
exprt::operandst disjuncts;
90+
91+
for(const auto &goal_pair : goal_map)
92+
{
93+
if(
94+
select_property(goal_pair.first) &&
95+
!goal_pair.second.condition.is_false())
96+
{
97+
disjuncts.push_back(literal_exprt(goal_pair.second.condition));
98+
}
99+
}
100+
101+
// this is 'false' if there are no disjuncts
102+
solver->prop_conv().set_to_true(disjunction(disjuncts));
103+
}
104+
105+
decision_proceduret::resultt goto_symex_property_decidert::solve()
106+
{
107+
return solver->prop_conv().dec_solve();
108+
}
109+
110+
prop_convt &goto_symex_property_decidert::get_solver() const
111+
{
112+
return solver->prop_conv();
113+
}
114+
115+
symex_target_equationt &goto_symex_property_decidert::get_equation() const
116+
{
117+
return equation;
118+
}
119+
120+
void goto_symex_property_decidert::update_properties_status_from_goals(
121+
propertiest &properties,
122+
std::unordered_set<irep_idt> &updated_properties,
123+
decision_proceduret::resultt dec_result,
124+
bool set_pass) const
125+
{
126+
switch(dec_result)
127+
{
128+
case decision_proceduret::resultt::D_SATISFIABLE:
129+
for(auto &goal_pair : goal_map)
130+
{
131+
if(solver->prop_conv().l_get(goal_pair.second.condition).is_true())
132+
{
133+
properties.at(goal_pair.first).status |= property_statust::FAIL;
134+
updated_properties.insert(goal_pair.first);
135+
}
136+
}
137+
break;
138+
case decision_proceduret::resultt::D_UNSATISFIABLE:
139+
if(!set_pass)
140+
break;
141+
142+
for(auto &property_pair : properties)
143+
{
144+
if(property_pair.second.status == property_statust::UNKNOWN)
145+
{
146+
property_pair.second.status |= property_statust::PASS;
147+
updated_properties.insert(property_pair.first);
148+
}
149+
}
150+
break;
151+
case decision_proceduret::resultt::D_ERROR:
152+
for(auto &property_pair : properties)
153+
{
154+
if(property_pair.second.status == property_statust::UNKNOWN)
155+
{
156+
property_pair.second.status |= property_statust::ERROR;
157+
updated_properties.insert(property_pair.first);
158+
}
159+
}
160+
break;
161+
}
162+
}

‎src/goto-checker/goto_symex_property_decider.h

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
/*******************************************************************\
2+
3+
Module: Property Decider for Goto-Symex
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Property Decider for Goto-Symex
11+
12+
#ifndef CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H
13+
#define CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H
14+
15+
#include <util/ui_message.h>
16+
17+
#include <goto-symex/symex_target_equation.h>
18+
19+
#include "properties.h"
20+
#include "solver_factory.h"
21+
22+
/// Provides management of goal variables that encode properties
23+
class goto_symex_property_decidert
24+
{
25+
public:
26+
goto_symex_property_decidert(
27+
const optionst &options,
28+
ui_message_handlert &ui_message_handler,
29+
symex_target_equationt &equation,
30+
const namespacet &ns);
31+
32+
/// Get the conditions for the properties from the equation
33+
/// and collect all 'instances' of the properties in the `goal_map`
34+
void
35+
update_properties_goals_from_symex_target_equation(propertiest &properties);
36+
37+
/// Convert the instances of a property into a goal variable
38+
void convert_goals();
39+
40+
/// Prevent the solver to optimize-away the goal variables
41+
/// (necessary for incremental solving)
42+
void freeze_goal_variables();
43+
44+
/// Add disjunction of negated selected properties to the equation
45+
void add_constraint_from_goals(
46+
std::function<bool(const irep_idt &property_id)> select_property);
47+
48+
/// Calls solve() on the solver instance
49+
decision_proceduret::resultt solve();
50+
51+
/// Returns the solver instance
52+
prop_convt &get_solver() const;
53+
54+
/// Return the equation associated with this instance
55+
symex_target_equationt &get_equation() const;
56+
57+
/// Update the property status from the truth value of the goal variable
58+
/// \param [inout] properties: The status is updated in this data structure
59+
/// \param [inout] updated_properties: The set of property IDs of
60+
/// updated properties
61+
/// \param dec_result: The result returned by the solver
62+
/// \param set_pass: If true then update UNKNOWN properties to PASS
63+
/// if the solver returns UNSATISFIABLE
64+
void update_properties_status_from_goals(
65+
propertiest &properties,
66+
std::unordered_set<irep_idt> &updated_properties,
67+
decision_proceduret::resultt dec_result,
68+
bool set_pass = true) const;
69+
70+
protected:
71+
const optionst &options;
72+
ui_message_handlert &ui_message_handler;
73+
symex_target_equationt &equation;
74+
std::unique_ptr<solver_factoryt::solvert> solver;
75+
76+
struct goalt
77+
{
78+
/// A property holds if all instances of it are true
79+
std::vector<symex_target_equationt::SSA_stepst::iterator> instances;
80+
81+
/// The goal variable
82+
literalt condition;
83+
84+
exprt as_expr() const;
85+
};
86+
87+
/// Maintains the relation between a property ID and
88+
/// the corresponding goal variable that encodes
89+
/// the negation of the conjunction of the instances of the property
90+
std::map<irep_idt, goalt> goal_map;
91+
};
92+
93+
#endif // CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H

0 commit comments

Comments
 (0)