cprover
Loading...
Searching...
No Matches
local_safe_pointers.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Local safe pointer analysis
4
5Author: Diffblue Ltd
6
7\*******************************************************************/
8
11
12#include "local_safe_pointers.h"
13
14#include <util/expr_iterator.h>
15#include <util/expr_util.h>
16#include <util/format_expr.h>
17#include <util/symbol_table.h>
18
31
38{
40 // If true, then a null check is made when test `expr` passes; if false,
41 // one is made when it fails.
42 bool checked_when_taken = true;
43
44 // Reduce some roundabout ways of saying "x != null", e.g. "!(x == null)".
45 while(normalized_expr.id() == ID_not)
46 {
48 checked_when_taken = !checked_when_taken;
49 }
50
51 if(normalized_expr.id() == ID_equal)
52 {
54 checked_when_taken = !checked_when_taken;
55 }
56
58 {
61
62 if(op0.type().id() == ID_pointer &&
64 {
65 return { { checked_when_taken, op1 } };
66 }
67
68 if(op1.type().id() == ID_pointer &&
70 {
71 return { { checked_when_taken, op0 } };
72 }
73 }
74
75 return {};
76}
77
84{
85 std::set<exprt, type_comparet> checked_expressions(type_comparet{});
86
87 for(const auto &instruction : goto_program.instructions)
88 {
89 // Handle control-flow convergence pessimistically:
90 if(instruction.incoming_edges.size() > 1)
92 // Retrieve working set for forward GOTOs:
93 else if(instruction.is_target())
94 {
95 auto findit = non_null_expressions.find(instruction.location_number);
96 if(findit != non_null_expressions.end())
98 else
99 {
100 checked_expressions = std::set<exprt, type_comparet>(type_comparet{});
101 }
102 }
103
104 // Save the working set at this program point:
105 if(!checked_expressions.empty())
106 {
107 non_null_expressions.emplace(
108 instruction.location_number, checked_expressions);
109 }
110
111 switch(instruction.type())
112 {
113 // Instruction types that definitely don't write anything, and therefore
114 // can't store a null pointer:
115 case DECL:
116 case DEAD:
117 case ASSERT:
118 case SKIP:
119 case LOCATION:
120 case SET_RETURN_VALUE:
121 case THROW:
122 case CATCH:
123 case END_FUNCTION:
124 case ATOMIC_BEGIN:
125 case ATOMIC_END:
126 break;
127
128 // Possible checks:
129 case ASSUME:
130 if(auto assume_check = get_null_checked_expr(instruction.get_condition()))
131 {
132 if(assume_check->checked_when_taken)
133 checked_expressions.insert(assume_check->checked_expr);
134 }
135
136 break;
137
138 case GOTO:
139 if(!instruction.is_backwards_goto())
140 {
141 // Copy current state to GOTO target:
142
144 non_null_expressions.emplace(
145 instruction.get_target()->location_number, checked_expressions);
146
147 // If the target already has a state entry then it is a control-flow
148 // merge point and everything will be assumed maybe-null in any case.
149 if(target_emplace_result.second)
150 {
151 if(
152 auto conditional_check =
153 get_null_checked_expr(instruction.get_condition()))
154 {
155 // Add the GOTO condition to either the target or current state,
156 // as appropriate:
157 if(conditional_check->checked_when_taken)
158 {
159 target_emplace_result.first->second.insert(
160 conditional_check->checked_expr);
161 }
162 else
163 checked_expressions.insert(conditional_check->checked_expr);
164 }
165 }
166 }
167
168 break;
169
170 case ASSIGN:
171 case START_THREAD:
172 case END_THREAD:
173 case FUNCTION_CALL:
174 case OTHER:
175 case INCOMPLETE_GOTO:
177 // Pessimistically assume all other instructions might overwrite any
178 // pointer with a possibly-null value.
180 break;
181 }
182 }
183}
184
191 std::ostream &out,
192 const goto_programt &goto_program,
193 const namespacet &ns)
194{
195 for(const auto &instruction : goto_program.instructions)
196 {
197 out << "**** " << instruction.location_number << " "
198 << instruction.source_location() << "\n";
199
200 out << "Non-null expressions: ";
201
202 auto findit = non_null_expressions.find(instruction.location_number);
203 if(findit == non_null_expressions.end())
204 out << "{}";
205 else
206 {
207 out << "{";
208 bool first = true;
209 for(const exprt &expr : findit->second)
210 {
211 if(!first)
212 out << ", ";
213 first = true;
214 format_rec(out, expr);
215 }
216 out << "}";
217 }
218
219 out << '\n';
220 goto_program.output_instruction(ns, irep_idt(), out, instruction);
221 out << '\n';
222 }
223}
224
235 std::ostream &out,
236 const goto_programt &goto_program,
237 const namespacet &ns)
238{
239 for(const auto &instruction : goto_program.instructions)
240 {
241 out << "**** " << instruction.location_number << " "
242 << instruction.source_location() << "\n";
243
244 out << "Safe (known-not-null) dereferences: ";
245
246 auto findit = non_null_expressions.find(instruction.location_number);
247 if(findit == non_null_expressions.end())
248 out << "{}";
249 else
250 {
251 out << "{";
252 bool first = true;
253 instruction.apply([&first, &out](const exprt &e) {
254 for(auto subexpr_it = e.depth_begin(), subexpr_end = e.depth_end();
256 ++subexpr_it)
257 {
258 if(subexpr_it->id() == ID_dereference)
259 {
260 if(!first)
261 out << ", ";
262 first = true;
263 format_rec(out, to_dereference_expr(*subexpr_it).pointer());
264 }
265 }
266 });
267 out << "}";
268 }
269
270 out << '\n';
271 goto_program.output_instruction(ns, irep_idt(), out, instruction);
272 out << '\n';
273 }
274}
275
281{
282 auto findit = non_null_expressions.find(program_point->location_number);
283 if(findit == non_null_expressions.end())
284 return false;
285
286 return findit->second.count(skip_typecast(expr)) != 0;
287}
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Base class for all expressions.
Definition expr.h:54
depth_iteratort depth_end()
Definition expr.cpp:267
depth_iteratort depth_begin()
Definition expr.cpp:265
typet & type()
Return the type of the expression.
Definition expr.h:82
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
const irep_idt & id() const
Definition irep.h:396
void output_safe_dereferences(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output safely dereferenced expressions per instruction in human-readable format.
void operator()(const goto_programt &goto_program)
Compute safe dereference expressions for a given GOTO program.
bool is_non_null_at_program_point(const exprt &expr, goto_programt::const_targett program_point)
Return true if the local-safe-pointers analysis has determined expr cannot be null as of program_poin...
void output(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output non-null expressions per instruction in human-readable format.
std::map< unsigned, std::set< exprt, type_comparet > > non_null_expressions
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The null pointer constant.
const exprt & op() const
Definition std_expr.h:293
Forward depth-first search iterators These iterators' copy operations are expensive,...
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
static std::ostream & format_rec(std::ostream &os, const multi_ary_exprt &src)
This formats a multi-ary expression, adding parentheses where indicated by bracket_subexpression.
@ FUNCTION_CALL
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
dstringt irep_idt
Definition irep.h:37
static optionalt< goto_null_checkt > get_null_checked_expr(const exprt &expr)
Check if expr tests if a pointer is null.
Local safe pointer analysis.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition std_expr.h:1308
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2206
Return structure for get_null_checked_expr and get_conditional_checked_expr
bool checked_when_taken
If true, the given GOTO/ASSUME tests that a pointer expression is non-null on the taken branch or pas...
exprt checked_expr
Null-tested pointer expression.
Comparator that regards type-equal expressions as equal, and otherwise uses the natural (operator<) o...
Author: Diffblue Ltd.