CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
30
36static std::optional<goto_null_checkt> get_null_checked_expr(const exprt &expr)
37{
39 // If true, then a null check is made when test `expr` passes; if false,
40 // one is made when it fails.
41 bool checked_when_taken = true;
42
43 // Reduce some roundabout ways of saying "x != null", e.g. "!(x == null)".
44 while(normalized_expr.id() == ID_not)
45 {
47 checked_when_taken = !checked_when_taken;
48 }
49
50 if(normalized_expr.id() == ID_equal)
51 {
53 checked_when_taken = !checked_when_taken;
54 }
55
57 {
60
61 if(op0.type().id() == ID_pointer &&
63 {
64 return { { checked_when_taken, op1 } };
65 }
66
67 if(op1.type().id() == ID_pointer &&
69 {
70 return { { checked_when_taken, op0 } };
71 }
72 }
73
74 return {};
75}
76
83{
84 std::set<exprt, type_comparet> checked_expressions(type_comparet{});
85
86 for(const auto &instruction : goto_program.instructions)
87 {
88 // Handle control-flow convergence pessimistically:
89 if(instruction.incoming_edges.size() > 1)
91 // Retrieve working set for forward GOTOs:
92 else if(instruction.is_target())
93 {
94 auto findit = non_null_expressions.find(instruction.location_number);
95 if(findit != non_null_expressions.end())
97 else
98 {
99 checked_expressions = std::set<exprt, type_comparet>(type_comparet{});
100 }
101 }
102
103 // Save the working set at this program point:
104 if(!checked_expressions.empty())
105 {
106 non_null_expressions.emplace(
107 instruction.location_number, checked_expressions);
108 }
109
110 switch(instruction.type())
111 {
112 // Instruction types that definitely don't write anything, and therefore
113 // can't store a null pointer:
114 case DECL:
115 case DEAD:
116 case ASSERT:
117 case SKIP:
118 case LOCATION:
119 case SET_RETURN_VALUE:
120 case THROW:
121 case CATCH:
122 case END_FUNCTION:
123 case ATOMIC_BEGIN:
124 case ATOMIC_END:
125 break;
126
127 // Possible checks:
128 case ASSUME:
129 if(auto assume_check = get_null_checked_expr(instruction.condition()))
130 {
131 if(assume_check->checked_when_taken)
132 checked_expressions.insert(assume_check->checked_expr);
133 }
134
135 break;
136
137 case GOTO:
138 if(!instruction.is_backwards_goto())
139 {
140 // Copy current state to GOTO target:
141
143 non_null_expressions.emplace(
144 instruction.get_target()->location_number, checked_expressions);
145
146 // If the target already has a state entry then it is a control-flow
147 // merge point and everything will be assumed maybe-null in any case.
148 if(target_emplace_result.second)
149 {
150 if(
151 auto conditional_check =
152 get_null_checked_expr(instruction.condition()))
153 {
154 // Add the GOTO condition to either the target or current state,
155 // as appropriate:
156 if(conditional_check->checked_when_taken)
157 {
158 target_emplace_result.first->second.insert(
159 conditional_check->checked_expr);
160 }
161 else
162 checked_expressions.insert(conditional_check->checked_expr);
163 }
164 }
165 }
166
167 break;
168
169 case ASSIGN:
170 case START_THREAD:
171 case END_THREAD:
172 case FUNCTION_CALL:
173 case OTHER:
174 case INCOMPLETE_GOTO:
176 // Pessimistically assume all other instructions might overwrite any
177 // pointer with a possibly-null value.
179 break;
180 }
181 }
182}
183
190 std::ostream &out,
191 const goto_programt &goto_program,
192 const namespacet &ns)
193{
194 for(const auto &instruction : goto_program.instructions)
195 {
196 out << "**** " << instruction.location_number << " "
197 << instruction.source_location() << "\n";
198
199 out << "Non-null expressions: ";
200
201 auto findit = non_null_expressions.find(instruction.location_number);
202 if(findit == non_null_expressions.end())
203 out << "{}";
204 else
205 {
206 out << "{";
207 bool first = true;
208 for(const exprt &expr : findit->second)
209 {
210 if(!first)
211 out << ", ";
212 first = true;
213 format_rec(out, expr);
214 }
215 out << "}";
216 }
217
218 out << '\n';
219 instruction.output(out);
220 out << '\n';
221 }
222}
223
234 std::ostream &out,
235 const goto_programt &goto_program,
236 const namespacet &ns)
237{
238 for(const auto &instruction : goto_program.instructions)
239 {
240 out << "**** " << instruction.location_number << " "
241 << instruction.source_location() << "\n";
242
243 out << "Safe (known-not-null) dereferences: ";
244
245 auto findit = non_null_expressions.find(instruction.location_number);
246 if(findit == non_null_expressions.end())
247 out << "{}";
248 else
249 {
250 out << "{";
251 bool first = true;
252 instruction.apply([&first, &out](const exprt &e) {
253 for(auto subexpr_it = e.depth_begin(), subexpr_end = e.depth_end();
255 ++subexpr_it)
256 {
257 if(subexpr_it->id() == ID_dereference)
258 {
259 if(!first)
260 out << ", ";
261 first = true;
262 format_rec(out, to_dereference_expr(*subexpr_it).pointer());
263 }
264 }
265 });
266 out << "}";
267 }
268
269 out << '\n';
270 instruction.output(out);
271 out << '\n';
272 }
273}
274
280{
281 auto findit = non_null_expressions.find(program_point->location_number);
282 if(findit == non_null_expressions.end())
283 return false;
284
285 return findit->second.count(skip_typecast(expr)) != 0;
286}
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
depth_iteratort depth_end()
Definition expr.cpp:249
depth_iteratort depth_begin()
Definition expr.cpp:247
typet & type()
Return the type of the expression.
Definition expr.h:84
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
const irep_idt & id() const
Definition irep.h:388
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.
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
static std::optional< 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:1450
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2479
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...