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 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
property_statust::FAIL
@ FAIL
The property was violated.
conjunction
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:51
ui_message_handlert
Definition: ui_message.h:20
property_statust::ERROR
@ ERROR
An error occurred during goto checking.
ui_message_handlert::uit::XML_UI
@ XML_UI
optionst
Definition: options.h:23
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
goto_symex_property_decidert::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: goto_symex_property_decider.h:70
goto_symex_property_decidert::solver
std::unique_ptr< solver_factoryt::solvert > solver
Definition: goto_symex_property_decider.h:72
threeval.h
decision_proceduret
Definition: decision_procedure.h:21
decision_proceduret::resultt::D_UNSATISFIABLE
@ D_UNSATISFIABLE
goto_symex_property_decider.h
Property Decider for Goto-Symex.
exprt
Base class for all expressions.
Definition: expr.h:53
goto_symex_property_decidert::solve
decision_proceduret::resultt solve()
Calls solve() on the solver instance.
Definition: goto_symex_property_decider.cpp:102
stack_decision_proceduret
Definition: stack_decision_procedure.h:58
solver_factoryt
Definition: solver_factory.h:27
goto_symex_property_decidert::get_equation
symex_target_equationt & get_equation() const
Return the equation associated with this instance.
Definition: goto_symex_property_decider.cpp:119
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:31
decision_proceduret::resultt::D_SATISFIABLE
@ D_SATISFIABLE
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
disjunction
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
goto_symex_property_decidert::goalt::as_expr
exprt as_expr() const
Definition: goto_symex_property_decider.cpp:34
goto_symex_property_decidert::equation
symex_target_equationt & equation
Definition: goto_symex_property_decider.h:71
goto_symex_property_decidert::goto_symex_property_decidert
goto_symex_property_decidert(const optionst &options, ui_message_handlert &ui_message_handler, symex_target_equationt &equation, const namespacet &ns)
Definition: goto_symex_property_decider.cpp:19
goto_symex_property_decidert::convert_goals
void convert_goals()
Convert the instances of a property into a goal variable.
Definition: goto_symex_property_decider.cpp:72
goto_symex_property_decidert::goal_map
std::map< irep_idt, goalt > goal_map
Maintains the relation between a property ID and the corresponding goal variable that encodes the neg...
Definition: goto_symex_property_decider.h:88
prop.h
is_property_to_check
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
Definition: properties.cpp:168
goto_symex_property_decidert::get_decision_procedure
decision_proceduret & get_decision_procedure() const
Returns the solver instance.
Definition: goto_symex_property_decider.cpp:108
goto_symex_property_decidert::get_stack_decision_procedure
stack_decision_proceduret & get_stack_decision_procedure() const
Returns the solver instance.
Definition: goto_symex_property_decider.cpp:114
decision_proceduret::resultt::D_ERROR
@ D_ERROR
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
dstringt::empty
bool empty() const
Definition: dstring.h:88
goto_symex_property_decidert::add_constraint_from_goals
void add_constraint_from_goals(std::function< bool(const irep_idt &property_id)> select_property)
Add disjunction of negated selected properties to the equation.
Definition: goto_symex_property_decider.cpp:83
decision_proceduret::resultt
resultt
Result of running the decision procedure.
Definition: decision_procedure.h:44
solver_factoryt::get_solver
virtual std::unique_ptr< solvert > get_solver()
Returns a solvert object.
Definition: solver_factory.cpp:131
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
property_statust::UNKNOWN
@ UNKNOWN
The checker was unable to determine the status of the property.
goto_symex_property_decidert::update_properties_goals_from_symex_target_equation
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...
Definition: goto_symex_property_decider.cpp:44
goto_symex_property_decidert::goalt::instances
std::vector< symex_target_equationt::SSA_stepst::iterator > instances
A property holds if all instances of it are true.
Definition: goto_symex_property_decider.h:77
goto_symex_property_decidert::update_properties_status_from_goals
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.
Definition: goto_symex_property_decider.cpp:124
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:257
property_statust::PASS
@ PASS
The property was not violated.
goto_symex_property_decidert::options
const optionst & options
Definition: goto_symex_property_decider.h:69
literal_expr.h
not_exprt
Boolean negation.
Definition: std_expr.h:2843