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
22{
27
30};
31
38{
39 exprt normalized_expr = expr;
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 {
47 normalized_expr = to_not_expr(normalized_expr).op();
48 checked_when_taken = !checked_when_taken;
49 }
50
51 if(normalized_expr.id() == ID_equal)
52 {
53 normalized_expr.id(ID_notequal);
54 checked_when_taken = !checked_when_taken;
55 }
56
57 if(normalized_expr.id() == ID_notequal)
58 {
59 const exprt &op0 = skip_typecast(to_notequal_expr(normalized_expr).op0());
60 const exprt &op1 = skip_typecast(to_notequal_expr(normalized_expr).op1());
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)
91 checked_expressions.clear();
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())
97 checked_expressions = findit->second;
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
143 auto target_emplace_result =
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.
179 checked_expressions.clear();
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();
255 subexpr_it != subexpr_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
280 const exprt &expr, goto_programt::const_targett program_point)
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}
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.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
instructionst::const_iterator const_targett
Definition: goto_program.h:593
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.
Definition: pointer_expr.h:723
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
Definition: expr_util.cpp:216
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.
Definition: format_expr.cpp:93
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ LOCATION
Definition: goto_program.h:41
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
@ ASSUME
Definition: goto_program.h:35
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.
nonstd::optional< T > optionalt
Definition: optional.h:35
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
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.