cprover
goto_symex_property_decider.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Property Decider for Goto-Symex
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
13 
15 #include <solvers/prop/prop.h>
16 
17 #include <util/threeval.h>
18 
20  const optionst &options,
21  ui_message_handlert &ui_message_handler,
22  symex_target_equationt &equation,
23  const namespacet &ns)
24  : options(options), ui_message_handler(ui_message_handler), equation(equation)
25 {
26  solver_factoryt solvers(
27  options,
28  ns,
31  solver = solvers.get_solver();
32 }
33 
35 {
36  exprt::operandst conjuncts;
37  conjuncts.reserve(instances.size());
38  for(const auto &inst : instances)
39  conjuncts.push_back(inst->cond_handle);
40  return conjunction(conjuncts);
41 }
42 
45 {
46  goal_map.clear();
47 
48  for(symex_target_equationt::SSA_stepst::iterator it =
49  equation.SSA_steps.begin();
50  it != equation.SSA_steps.end();
51  ++it)
52  {
53  if(it->is_assert())
54  {
55  irep_idt property_id = it->get_property_id();
56  CHECK_RETURN(!property_id.empty());
57 
58  // consider goal instance if it is in the given properties
59  auto property_pair_it = properties.find(property_id);
60  if(
61  property_pair_it != properties.end() &&
62  is_property_to_check(property_pair_it->second.status))
63  {
64  // it's going to be checked, but we don't know the status yet
65  property_pair_it->second.status |= property_statust::UNKNOWN;
66  goal_map[property_id].instances.push_back(it);
67  }
68  }
69  }
70 }
71 
73 {
74  for(auto &goal_pair : goal_map)
75  {
76  // Our goal is to falsify a property, i.e., we will
77  // add the negation of the property as goal.
78  goal_pair.second.condition = solver->decision_procedure().handle(
79  not_exprt(goal_pair.second.as_expr()));
80  }
81 }
82 
84  std::function<bool(const irep_idt &)> select_property)
85 {
86  exprt::operandst disjuncts;
87 
88  for(const auto &goal_pair : goal_map)
89  {
90  if(
91  select_property(goal_pair.first) &&
92  !goal_pair.second.condition.is_false())
93  {
94  disjuncts.push_back(goal_pair.second.condition);
95  }
96  }
97 
98  // this is 'false' if there are no disjuncts
99  solver->decision_procedure().set_to_true(disjunction(disjuncts));
100 }
101 
103 {
104  return solver->decision_procedure()();
105 }
106 
109 {
110  return solver->decision_procedure();
111 }
112 
115 {
116  return solver->stack_decision_procedure();
117 }
118 
120 {
121  return equation;
122 }
123 
125  propertiest &properties,
126  std::unordered_set<irep_idt> &updated_properties,
127  decision_proceduret::resultt dec_result,
128  bool set_pass) const
129 {
130  switch(dec_result)
131  {
133  for(auto &goal_pair : goal_map)
134  {
135  auto &status = properties.at(goal_pair.first).status;
136  if(
137  solver->decision_procedure()
138  .get(goal_pair.second.condition)
139  .is_true() &&
140  status != property_statust::FAIL)
141  {
142  status |= property_statust::FAIL;
143  updated_properties.insert(goal_pair.first);
144  }
145  }
146  break;
148  if(!set_pass)
149  break;
150 
151  for(auto &property_pair : properties)
152  {
153  if(property_pair.second.status == property_statust::UNKNOWN)
154  {
155  property_pair.second.status |= property_statust::PASS;
156  updated_properties.insert(property_pair.first);
157  }
158  }
159  break;
161  for(auto &property_pair : properties)
162  {
163  if(property_pair.second.status == property_statust::UNKNOWN)
164  {
165  property_pair.second.status |= property_statust::ERROR;
166  updated_properties.insert(property_pair.first);
167  }
168  }
169  break;
170  }
171 }
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:92
Boolean negation.
Definition: std_expr.h:2042
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:31
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:168
@ 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::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
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:41
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:29
std::vector< symex_target_equationt::SSA_stepst::iterator > instances
A property holds if all instances of it are true.