CBMC
Loading...
Searching...
No Matches
counterexample_found.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Counterexample Found
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
13
14#include <util/cout_message.h>
15#include <util/simplify_expr.h>
16
18
19#include "axioms.h"
20#include "bv_pointers_wide.h"
21#include "simplify_state_expr.h"
22#include "state.h"
23
25{
26#if 0
27 for(auto &entry : solver.get_cache())
28 {
29 const auto &expr = entry.first;
30 if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_not)
31 continue;
32 auto value = solver.l_get(entry.second);
33# if 0
34 std::cout << "|| " << format(expr) << " --> " << value << "\n";
35# endif
36 }
37#endif
38
39#if 0
40 for(auto &entry : solver.get_map().get_mapping())
41 {
42 const auto &identifier = entry.first;
43 auto symbol = symbol_exprt(identifier, entry.second.type);
44 auto value = solver.get(symbol);
45 std::cout << "|| " << format(symbol) << " --> " << format(value) << "\n";
46 }
47#endif
48
49#if 0
50 for(auto &entry : solver.get_symbols())
51 {
52 const auto &identifier = entry.first;
53 auto value = solver.l_get(entry.second);
54 std::cout << "|| " << identifier << " --> " << value << "\n";
55 }
56#endif
57}
58
60 const std::unordered_map<exprt, exprt, irep_hash> &memory,
62 exprt src,
63 const namespacet &ns)
64{
65 if(src.id() == ID_evaluate)
66 {
67 const auto &evaluate_expr = to_evaluate_expr(src);
68
69 // recursively get the address
71 evaluator_rec(memory, solver, evaluate_expr.address(), ns);
72
75
76 auto m_it = memory.find(address_simplified);
77 if(m_it == memory.end())
78 return src;
79 else
80 return m_it->second;
81 }
82 else if(src.id() == ID_symbol)
83 {
84 // nondet -- ask the solver
85 return solver.get(src);
86 }
87 else
88 {
89 for(auto &op : src.operands())
90 op = evaluator_rec(memory, solver, op, ns);
91
92 return src;
93 }
94}
95
97 const std::unordered_map<exprt, exprt, irep_hash> &memory,
99 exprt src,
100 const namespacet &ns)
101{
102 auto tmp = evaluator_rec(memory, solver, src, ns);
103 return simplify_expr(simplify_state_expr(tmp, {}, ns), ns);
104}
105
106propertyt::tracet counterexample(
107 const std::vector<framet> &frames,
108 const workt &work,
110 const axiomst &axioms,
111 const namespacet &ns)
112{
113 propertyt::tracet trace;
114
115 // map from memory addresses to memory values
116 std::unordered_map<exprt, exprt, irep_hash> memory;
117
118 // heap object counter
119 std::size_t heap_object_counter = 0;
120
121 // work.path goes backwards, we want a forwards trace
122 for(auto r_it = work.path.rbegin(); r_it != work.path.rend(); ++r_it)
123 {
124 const auto &frame = frames[r_it->index];
126 state.frame = *r_it;
127
128 for(auto &implication : frame.implications)
129 {
130 if(implication.rhs.arguments().size() != 1)
131 continue;
132 auto &argument = implication.rhs.arguments().front();
133 if(argument.id() == ID_update_state)
134 {
136 auto address = evaluator(memory, solver, update_state.address(), ns);
137 auto value = evaluator(memory, solver, update_state.new_value(), ns);
138
139 if(value.id() == ID_allocate)
140 {
141 // replace by a numbered 'heap object'
143 auto object_type = to_pointer_type(value.type()).base_type();
144 auto identifier = "heap-" + std::to_string(heap_object_counter);
145 value = object_address_exprt(symbol_exprt(identifier, object_type));
146 }
147
148 state.updates.emplace_back(address, value);
149 memory[address] = value;
150 }
151 else if(argument.id() == ID_enter_scope_state)
152 {
153 // do we have a value?
155 auto address = enter_scope_state.address();
156 auto evaluate_expr = evaluate_exprt(enter_scope_state.state(), address);
157 auto translated = axioms.translate(evaluate_expr);
158 auto value = solver.get(translated);
159 if(value.is_not_nil() && value != evaluate_expr)
160 {
161 state.updates.emplace_back(address, value);
162 memory[address] = value;
163 }
164 }
165 }
166
167 trace.push_back(std::move(state));
168 }
169
170 return trace;
171}
172
173std::optional<propertyt::tracet> counterexample_found(
174 const std::vector<framet> &frames,
175 const workt &work,
176 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
177 bool verbose,
178 const namespacet &ns)
179{
180 auto &f = frames[work.frame.index];
181
182 for(const auto &implication : f.implications)
183 {
184 if(implication.lhs.id() == ID_initial_state)
185 {
186 cout_message_handlert message_handler;
187 message_handler.set_verbosity(verbose ? 10 : 1);
188 satcheckt satcheck(message_handler);
189 bv_pointers_widet solver(ns, satcheck, message_handler);
190 axiomst axioms(solver, address_taken, verbose, ns);
191
192 // These are initial states, i.e., initial_state(ς) ⇒ SInitial(ς).
193 // Ask the solver whether the invariant is 'true'.
194 axioms.set_to_false(work.invariant);
195 axioms.set_to_true(implication.lhs);
196 axioms.emit();
197
198 switch(solver())
199 {
201 if(verbose)
203 return counterexample(frames, work, solver, axioms, ns);
205 break;
207 throw "error reported by solver";
208 }
209 }
210 }
211
212 return {};
213}
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
Axioms.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
void emit()
Definition axioms.cpp:749
exprt translate(exprt) const
Definition axioms.cpp:350
void set_to_true(exprt)
Definition axioms.cpp:29
void set_to_false(exprt)
Definition axioms.cpp:34
An interface for a decision procedure for satisfiability problems.
Base class for all expressions.
Definition expr.h:56
operandst & operands()
Definition expr.h:94
std::size_t index
const irep_idt & id() const
Definition irep.h:388
void set_verbosity(unsigned _verbosity)
Definition message.h:52
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Operator to return the address of an object.
Expression to hold a symbol (variable)
Definition std_expr.h:131
static exprt evaluator_rec(const std::unordered_map< exprt, exprt, irep_hash > &memory, const decision_proceduret &solver, exprt src, const namespacet &ns)
static exprt evaluator(const std::unordered_map< exprt, exprt, irep_hash > &memory, const decision_proceduret &solver, exprt src, const namespacet &ns)
std::optional< propertyt::tracet > counterexample_found(const std::vector< framet > &frames, const workt &work, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, bool verbose, const namespacet &ns)
void show_assignment(const bv_pointers_widet &solver)
propertyt::tracet counterexample(const std::vector< framet > &frames, const workt &work, const bv_pointers_widet &solver, const axiomst &axioms, const namespacet &ns)
Counterexample Found.
static format_containert< T > format(const T &o)
Definition format.h:37
static exprt implication(exprt lhs, exprt rhs)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt simplify_state_expr(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
exprt simplify_expr(exprt src, const namespacet &ns)
Simplify State Expression.
void solver(std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &solver_options, const namespacet &ns, std::vector< propertyt > &properties, std::size_t property_index)
Definition solver.cpp:44
const enter_scope_state_exprt & to_enter_scope_state_expr(const exprt &expr)
Cast an exprt to a enter_scope_state_exprt.
Definition state.h:1042
const update_state_exprt & to_update_state_expr(const exprt &expr)
Cast an exprt to a update_state_exprt.
Definition state.h:200
const evaluate_exprt & to_evaluate_expr(const exprt &expr)
Cast an exprt to a evaluate_exprt.
Definition state.h:130
std::vector< trace_updatet > updates
exprt invariant
patht path
frame_reft frame