cprover
counterexample_beautification.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Counterexample Beautification using Incremental SAT
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/arith_tools.h>
15 #include <util/std_expr.h>
16 #include <util/symbol.h>
17 #include <util/threeval.h>
18 
20 
23  : log(message_handler)
24 {
25 }
26 
28  prop_convt &prop_conv,
29  const symex_target_equationt &equation,
30  minimization_listt &minimization_list)
31 {
32  // ignore the ones that are assigned under false guards
33 
34  for(symex_target_equationt::SSA_stepst::const_iterator it =
35  equation.SSA_steps.begin();
36  it != equation.SSA_steps.end();
37  it++)
38  {
39  if(
40  it->is_assignment() &&
41  it->assignment_type == symex_targett::assignment_typet::STATE)
42  {
43  if(!prop_conv.get(it->guard_handle).is_false())
44  {
45  const typet &type = it->ssa_lhs.type();
46 
47  if(type != bool_typet())
48  {
49  // we minimize the absolute value, if applicable
50  if(
51  type.id() == ID_signedbv || type.id() == ID_fixedbv ||
52  type.id() == ID_floatbv)
53  {
54  abs_exprt abs_expr(it->ssa_lhs);
55  minimization_list.insert(abs_expr);
56  }
57  else
58  minimization_list.insert(it->ssa_lhs);
59  }
60  }
61  }
62 
63  // reached failed assertion?
64  if(it == failed)
65  break;
66  }
67 }
68 
69 symex_target_equationt::SSA_stepst::const_iterator
71  const prop_convt &prop_conv,
72  const symex_target_equationt &equation)
73 {
74  // find failed property
75 
76  for(symex_target_equationt::SSA_stepst::const_iterator it =
77  equation.SSA_steps.begin();
78  it != equation.SSA_steps.end();
79  it++)
80  {
81  if(
82  it->is_assert() && prop_conv.get(it->guard_handle).is_true() &&
83  prop_conv.get(it->cond_handle).is_false())
84  {
85  return it;
86  }
87  }
88 
90  return equation.SSA_steps.end();
91 }
92 
94 operator()(boolbvt &boolbv, const symex_target_equationt &equation)
95 {
96  // find failed property
97 
98  failed = get_failed_property(boolbv, equation);
99 
100  // lock the failed assertion
101  boolbv.set_to(failed->cond_handle, false);
102 
103  {
104  log.status() << "Beautifying counterexample (guards)" << messaget::eom;
105 
106  // compute weights for guards
107  typedef std::map<literalt, unsigned> guard_countt;
108  guard_countt guard_count;
109 
110  for(symex_target_equationt::SSA_stepst::const_iterator it =
111  equation.SSA_steps.begin();
112  it != equation.SSA_steps.end();
113  it++)
114  {
115  if(
116  it->is_assignment() &&
117  it->assignment_type != symex_targett::assignment_typet::HIDDEN)
118  {
119  literalt l = boolbv.convert(it->guard_handle);
120  if(!l.is_constant())
121  guard_count[l]++;
122  }
123 
124  // reached failed assertion?
125  if(it == failed)
126  break;
127  }
128 
129  // give to propositional minimizer
130  prop_minimizet prop_minimize{boolbv, log.get_message_handler()};
131 
132  for(const auto &g : guard_count)
133  prop_minimize.objective(g.first, g.second);
134 
135  // minimize
136  prop_minimize();
137  }
138 
139  {
140  log.status() << "Beautifying counterexample (values)" << messaget::eom;
141 
142  // get symbols we care about
143  minimization_listt minimization_list;
144 
145  get_minimization_list(boolbv, equation, minimization_list);
146 
147  // minimize
148  bv_minimizet bv_minimize(boolbv, log.get_message_handler());
149  bv_minimize(minimization_list);
150  }
151 }
decision_proceduret::get
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
counterexample_beautificationt::get_failed_property
symex_target_equationt::SSA_stepst::const_iterator get_failed_property(const prop_convt &prop_conv, const symex_target_equationt &equation)
Definition: counterexample_beautification.cpp:70
minimization_listt
std::set< exprt > minimization_listt
Definition: bv_minimize.h:23
arith_tools.h
prop_minimizet
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT.
Definition: prop_minimize.h:25
typet
The type of an expression, extends irept.
Definition: type.h:29
prop_convt
Definition: prop_conv.h:22
threeval.h
messaget::status
mstreamt & status() const
Definition: message.h:414
boolbvt::set_to
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
Definition: boolbv.cpp:601
counterexample_beautificationt::counterexample_beautificationt
counterexample_beautificationt(message_handlert &message_handler)
Definition: counterexample_beautification.cpp:21
bool_typet
The Boolean type.
Definition: std_types.h:37
messaget::eom
static eomt eom
Definition: message.h:297
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
symex_targett::assignment_typet::STATE
@ STATE
counterexample_beautificationt::failed
symex_target_equationt::SSA_stepst::const_iterator failed
Definition: counterexample_beautification.h:42
prop_minimize.h
SAT Minimizer.
counterexample_beautificationt::log
messaget log
Definition: counterexample_beautification.h:44
bv_minimizet
Definition: bv_minimize.h:26
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
abs_exprt
Absolute value.
Definition: std_expr.h:334
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:168
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
counterexample_beautificationt::get_minimization_list
void get_minimization_list(prop_convt &prop_conv, const symex_target_equationt &equation, minimization_listt &minimization_list)
Definition: counterexample_beautification.cpp:27
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:257
literalt
Definition: literal.h:26
counterexample_beautificationt::operator()
void operator()(boolbvt &boolbv, const symex_target_equationt &equation)
Definition: counterexample_beautification.cpp:94
boolbvt
Definition: boolbv.h:35
counterexample_beautification.h
Counterexample Beautification.
literalt::is_constant
bool is_constant() const
Definition: literal.h:166
symex_targett::assignment_typet::HIDDEN
@ HIDDEN
std_expr.h
API to expression classes.
ui_message_handlert::message_handler
message_handlert * message_handler
Definition: ui_message.h:47