cprover
goto_symex_property_decider.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Property Decider for Goto-Symex
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
13
14#include <util/ui_message.h>
15
16#include <solvers/prop/prop.h>
17
19 const optionst &options,
20 ui_message_handlert &ui_message_handler,
21 symex_target_equationt &equation,
22 const namespacet &ns)
23 : options(options), ui_message_handler(ui_message_handler), equation(equation)
24{
25 solver_factoryt solvers(
26 options,
27 ns,
30 solver = solvers.get_solver();
31}
32
34{
35 exprt::operandst conjuncts;
36 conjuncts.reserve(instances.size());
37 for(const auto &inst : instances)
38 conjuncts.push_back(inst->cond_handle);
39 return conjunction(conjuncts);
40}
41
44{
45 goal_map.clear();
46
47 for(symex_target_equationt::SSA_stepst::iterator it =
48 equation.SSA_steps.begin();
49 it != equation.SSA_steps.end();
50 ++it)
51 {
52 if(it->is_assert())
53 {
54 irep_idt property_id = it->get_property_id();
55 CHECK_RETURN(!property_id.empty());
56
57 // consider goal instance if it is in the given properties
58 auto property_pair_it = properties.find(property_id);
59 if(
60 property_pair_it != properties.end() &&
61 is_property_to_check(property_pair_it->second.status))
62 {
63 // it's going to be checked, but we don't know the status yet
64 property_pair_it->second.status |= property_statust::UNKNOWN;
65 goal_map[property_id].instances.push_back(it);
66 }
67 }
68 }
69}
70
72{
73 for(auto &goal_pair : goal_map)
74 {
75 // Our goal is to falsify a property, i.e., we will
76 // add the negation of the property as goal.
77 goal_pair.second.condition = solver->decision_procedure().handle(
78 not_exprt(goal_pair.second.as_expr()));
79 }
80}
81
83 std::function<bool(const irep_idt &)> select_property)
84{
85 exprt::operandst disjuncts;
86
87 for(const auto &goal_pair : goal_map)
88 {
89 if(
90 select_property(goal_pair.first) &&
91 !goal_pair.second.condition.is_false())
92 {
93 disjuncts.push_back(goal_pair.second.condition);
94 }
95 }
96
97 // this is 'false' if there are no disjuncts
98 solver->decision_procedure().set_to_true(disjunction(disjuncts));
99}
100
102{
103 return solver->decision_procedure()();
104}
105
108{
109 return solver->decision_procedure();
110}
111
114{
115 return solver->stack_decision_procedure();
116}
117
119{
120 return equation;
121}
122
124 propertiest &properties,
125 std::unordered_set<irep_idt> &updated_properties,
127 bool set_pass) const
128{
129 switch(dec_result)
130 {
132 for(auto &goal_pair : goal_map)
133 {
134 auto &status = properties.at(goal_pair.first).status;
135 if(
136 solver->decision_procedure()
137 .get(goal_pair.second.condition)
138 .is_true() &&
139 status != property_statust::FAIL)
140 {
141 status |= property_statust::FAIL;
142 updated_properties.insert(goal_pair.first);
143 }
144 }
145 break;
147 if(!set_pass)
148 break;
149
150 for(auto &property_pair : properties)
151 {
152 if(property_pair.second.status == property_statust::UNKNOWN)
153 {
154 property_pair.second.status |= property_statust::PASS;
155 updated_properties.insert(property_pair.first);
156 }
157 }
158 break;
160 for(auto &property_pair : properties)
161 {
162 if(property_pair.second.status == property_statust::UNKNOWN)
163 {
164 property_pair.second.status |= property_statust::ERROR;
165 updated_properties.insert(property_pair.first);
166 }
167 }
168 break;
169 }
170}
resultt
Result of running the decision procedure.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
symex_target_equationt & get_equation() const
Return the equation associated with this instance.
goto_symex_property_decidert(const optionst &options, ui_message_handlert &ui_message_handler, symex_target_equationt &equation, const namespacet &ns)
decision_proceduret & get_decision_procedure() const
Returns the solver instance.
decision_proceduret::resultt solve()
Calls solve() on the solver instance.
std::unique_ptr< solver_factoryt::solvert > solver
void update_properties_goals_from_symex_target_equation(propertiest &properties)
Get the conditions for the properties from the equation and collect all 'instances' of the properties...
void update_properties_status_from_goals(propertiest &properties, std::unordered_set< irep_idt > &updated_properties, decision_proceduret::resultt dec_result, bool set_pass=true) const
Update the property status from the truth value of the goal variable.
void add_constraint_from_goals(std::function< bool(const irep_idt &property_id)> select_property)
Add disjunction of negated selected properties to the equation.
void convert_goals()
Convert the instances of a property into a goal variable.
std::map< irep_idt, goalt > goal_map
Maintains the relation between a property ID and the corresponding goal variable that encodes the neg...
stack_decision_proceduret & get_stack_decision_procedure() const
Returns the solver instance.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Boolean negation.
Definition: std_expr.h:2181
virtual std::unique_ptr< solvert > get_solver()
Returns a solvert object.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual uit get_ui() const
Definition: ui_message.h:33
Property Decider for Goto-Symex.
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
Definition: properties.cpp:171
@ UNKNOWN
The checker was unable to determine the status of the property.
@ PASS
The property was not violated.
@ ERROR
An error occurred during goto checking.
@ FAIL
The property was violated.
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:76
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:34
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:22
std::vector< symex_target_equationt::SSA_stepst::iterator > instances
A property holds if all instances of it are true.