cprover
local_safe_pointers.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Local safe pointer analysis
4 
5 Author: Diffblue Ltd
6 
7 \*******************************************************************/
8 
11 
12 #include "local_safe_pointers.h"
13 
14 #include <util/base_type.h>
15 #include <util/expr_iterator.h>
16 #include <util/expr_util.h>
17 #include <util/format_expr.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 = normalized_expr.op0();
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(normalized_expr.op0());
60  const exprt &op1 = skip_typecast(normalized_expr.op1());
61 
62  if(op0.type().id() == ID_pointer &&
63  op0 == null_pointer_exprt(to_pointer_type(op0.type())))
64  {
65  return { { checked_when_taken, op1 } };
66  }
67 
68  if(op1.type().id() == ID_pointer &&
69  op1 == null_pointer_exprt(to_pointer_type(op1.type())))
70  {
71  return { { checked_when_taken, op0 } };
72  }
73  }
74 
75  return {};
76 }
77 
84 {
85  std::set<exprt, base_type_comparet> checked_expressions(
87 
88  for(const auto &instruction : goto_program.instructions)
89  {
90  // Handle control-flow convergence pessimistically:
91  if(instruction.incoming_edges.size() > 1)
92  checked_expressions.clear();
93  // Retrieve working set for forward GOTOs:
94  else if(instruction.is_target())
95  {
96  auto findit = non_null_expressions.find(instruction.location_number);
97  if(findit != non_null_expressions.end())
98  checked_expressions = findit->second;
99  else
100  {
101  checked_expressions =
102  std::set<exprt, base_type_comparet>(base_type_comparet{ns});
103  }
104  }
105 
106  // Save the working set at this program point:
107  if(!checked_expressions.empty())
108  {
109  non_null_expressions.emplace(
110  instruction.location_number, checked_expressions);
111  }
112 
113  switch(instruction.type)
114  {
115  // Instruction types that definitely don't write anything, and therefore
116  // can't store a null pointer:
117  case DECL:
118  case DEAD:
119  case ASSERT:
120  case SKIP:
121  case LOCATION:
122  case RETURN:
123  case THROW:
124  case CATCH:
125  break;
126 
127  // Possible checks:
128  case ASSUME:
129  if(auto assume_check = get_null_checked_expr(instruction.guard))
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 
142  auto target_emplace_result =
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(auto conditional_check = get_null_checked_expr(instruction.guard))
151  {
152  // Add the GOTO condition to either the target or current state,
153  // as appropriate:
154  if(conditional_check->checked_when_taken)
155  {
156  target_emplace_result.first->second.insert(
157  conditional_check->checked_expr);
158  }
159  else
160  checked_expressions.insert(conditional_check->checked_expr);
161  }
162  }
163  }
164 
165  break;
166 
167  default:
168  // Pessimistically assume all other instructions might overwrite any
169  // pointer with a possibly-null value.
170  checked_expressions.clear();
171  break;
172  }
173  }
174 }
175 
181  std::ostream &out, const goto_programt &goto_program)
182 {
183  forall_goto_program_instructions(i_it, goto_program)
184  {
185  out << "**** " << i_it->location_number << " "
186  << i_it->source_location << "\n";
187 
188  out << "Non-null expressions: ";
189 
190  auto findit = non_null_expressions.find(i_it->location_number);
191  if(findit == non_null_expressions.end())
192  out << "{}";
193  else
194  {
195  out << "{";
196  bool first = true;
197  for(const exprt &expr : findit->second)
198  {
199  if(!first)
200  out << ", ";
201  first = true;
202  format_rec(out, expr);
203  }
204  out << "}";
205  }
206 
207  out << '\n';
208  goto_program.output_instruction(ns, "", out, *i_it);
209  out << '\n';
210  }
211 }
212 
222  std::ostream &out, const goto_programt &goto_program)
223 {
224  forall_goto_program_instructions(i_it, goto_program)
225  {
226  out << "**** " << i_it->location_number << " "
227  << i_it->source_location << "\n";
228 
229  out << "Safe (known-not-null) dereferences: ";
230 
231  auto findit = non_null_expressions.find(i_it->location_number);
232  if(findit == non_null_expressions.end())
233  out << "{}";
234  else
235  {
236  out << "{";
237  bool first = true;
238  for(auto subexpr_it = i_it->code.depth_begin(),
239  subexpr_end = i_it->code.depth_end();
240  subexpr_it != subexpr_end;
241  ++subexpr_it)
242  {
243  if(subexpr_it->id() == ID_dereference)
244  {
245  if(!first)
246  out << ", ";
247  first = true;
248  format_rec(out, subexpr_it->op0());
249  }
250  }
251  out << "}";
252  }
253 
254  out << '\n';
255  goto_program.output_instruction(ns, "", out, *i_it);
256  out << '\n';
257  }
258 }
259 
264  const exprt &expr, goto_programt::const_targett program_point)
265 {
266  auto findit = non_null_expressions.find(program_point->location_number);
267  if(findit == non_null_expressions.end())
268  return false;
269  const exprt *tocheck = &expr;
270  while(tocheck->id() == ID_typecast)
271  tocheck = &tocheck->op0();
272  return findit->second.count(*tocheck) != 0;
273 }
274 
276  const exprt &e1, const exprt &e2) const
277 {
278  if(base_type_eq(e1, e2, ns))
279  return false;
280  else
281  return e1 < e2;
282 }
exprt checked_expr
Null-tested pointer expression.
void output_safe_dereferences(std::ostream &stream, const goto_programt &program)
Output safely dereferenced expressions per instruction in human-readable format.
exprt & op0()
Definition: expr.h:84
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
Deprecated expression utility functions.
The null pointer constant.
Definition: std_expr.h:4471
typet & type()
Return the type of the expression.
Definition: expr.h:68
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Forward depth-first search iterators These iterators' copy operations are expensive,...
static optionalt< goto_null_checkt > get_null_checked_expr(const exprt &expr)
Check if expr tests if a pointer is null.
void operator()(const goto_programt &goto_program)
Compute safe dereference expressions for a given GOTO program.
const irep_idt & id() const
Definition: irep.h:259
nonstd::optional< T > optionalt
Definition: optional.h:35
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
exprt & op1()
Definition: expr.h:87
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...
instructionst::const_iterator const_targett
Definition: goto_program.h:415
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:99
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:219
void output(std::ostream &stream, const goto_programt &program)
Output non-null expressions per instruction in human-readable format.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
Return structure for get_null_checked_expr and get_conditional_checked_expr
const namespacet & ns
Base class for all expressions.
Definition: expr.h:54
bool operator()(const exprt &e1, const exprt &e2) const
bool checked_when_taken
If true, the given GOTO/ASSUME tests that a pointer expression is non-null on the taken branch or pas...
Local safe pointer analysis.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
Base Type Computation.
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
Comparator that regards base_type_eq expressions as equal, and otherwise uses the natural (operator<)...
std::map< unsigned, std::set< exprt, base_type_comparet > > non_null_expressions