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 
182  std::ostream &out, const goto_programt &goto_program)
183 {
185  {
186  out << "**** " << i_it->location_number << " "
187  << i_it->source_location << "\n";
188 
189  out << "Non-null expressions: ";
190 
191  auto findit = non_null_expressions.find(i_it->location_number);
192  if(findit == non_null_expressions.end())
193  out << "{}";
194  else
195  {
196  out << "{";
197  bool first = true;
198  for(const exprt &expr : findit->second)
199  {
200  if(!first)
201  out << ", ";
202  first = true;
203  format_rec(out, expr);
204  }
205  out << "}";
206  }
207 
208  out << '\n';
209  goto_program.output_instruction(ns, "", out, *i_it);
210  out << '\n';
211  }
212 }
213 
224  std::ostream &out, const goto_programt &goto_program)
225 {
227  {
228  out << "**** " << i_it->location_number << " "
229  << i_it->source_location << "\n";
230 
231  out << "Safe (known-not-null) dereferences: ";
232 
233  auto findit = non_null_expressions.find(i_it->location_number);
234  if(findit == non_null_expressions.end())
235  out << "{}";
236  else
237  {
238  out << "{";
239  bool first = true;
240  for(auto subexpr_it = i_it->code.depth_begin(),
241  subexpr_end = i_it->code.depth_end();
242  subexpr_it != subexpr_end;
243  ++subexpr_it)
244  {
245  if(subexpr_it->id() == ID_dereference)
246  {
247  if(!first)
248  out << ", ";
249  first = true;
250  format_rec(out, subexpr_it->op0());
251  }
252  }
253  out << "}";
254  }
255 
256  out << '\n';
257  goto_program.output_instruction(ns, "", out, *i_it);
258  out << '\n';
259  }
260 }
261 
266  const exprt &expr, goto_programt::const_targett program_point)
267 {
268  auto findit = non_null_expressions.find(program_point->location_number);
269  if(findit == non_null_expressions.end())
270  return false;
271  const exprt *tocheck = &expr;
272  while(tocheck->id() == ID_typecast)
273  tocheck = &tocheck->op0();
274  return findit->second.count(*tocheck) != 0;
275 }
276 
278  const exprt &e1, const exprt &e2) const
279 {
280  if(base_type_eq(e1, e2, ns))
281  return false;
282  else
283  return e1 < e2;
284 }
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:72
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
Deprecated expression utility functions.
The null pointer constant.
Definition: std_expr.h:4518
typet & type()
Definition: expr.h:56
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:403
exprt & op1()
Definition: expr.h:75
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:398
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:61
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:218
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:70
Return structure for get_null_checked_expr and get_conditional_checked_expr
const namespacet & ns
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
Base class for all expressions.
Definition: expr.h:42
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.
goto_programt & goto_program
Definition: cover.cpp:63
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1459
Base Type Computation.
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
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