Skip to content

Commit 584bb2b

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 8f7ffc4 commit 584bb2b

5 files changed

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

‎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)