CBMC
c_safety_checks.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Checks for Errors in C/C++ Programs
4 
5 Author: Daniel Kroening, dkr@amazon.com
6 
7 \*******************************************************************/
8 
11 
12 #include "c_safety_checks.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/pointer_expr.h>
19 
21 
22 #include <ansi-c/expr2c.h>
23 
25 {
26  if(type.id() == ID_array)
27  return to_array_type(type).size();
28  else if(type.id() == ID_vector)
29  return to_vector_type(type).size();
30  else
31  PRECONDITION(false);
32 }
33 
34 enum class access_typet
35 {
36  R,
37  W
38 };
39 
41  goto_functionst::function_mapt::value_type &,
42  const exprt::operandst &guards,
43  const exprt &,
45  const namespacet &,
46  goto_programt &);
47 
49  goto_functionst::function_mapt::value_type &f,
50  const exprt::operandst &guards,
51  const exprt &expr,
52  const namespacet &ns,
53  goto_programt &dest)
54 {
55  if(expr.id() == ID_index)
56  {
57  const auto &index_expr = to_index_expr(expr);
58  c_safety_checks_address_rec(f, guards, index_expr.array(), ns, dest);
60  f, guards, index_expr.index(), access_typet::R, ns, dest);
61  }
62  else if(expr.id() == ID_member)
63  {
65  f, guards, to_member_expr(expr).struct_op(), ns, dest);
66  }
67 }
68 
69 static exprt guard(const exprt::operandst &guards, exprt cond)
70 {
71  if(guards.empty())
72  return cond;
73  else
74  return implies_exprt(conjunction(guards), std::move(cond));
75 }
76 
78  goto_functionst::function_mapt::value_type &f,
79  const exprt::operandst &guards,
80  const exprt &expr,
81  access_typet access_type,
82  const namespacet &ns,
83  goto_programt &dest)
84 {
85  if(expr.id() == ID_address_of)
86  {
88  f, guards, to_address_of_expr(expr).object(), ns, dest);
89  return;
90  }
91  else if(expr.id() == ID_and)
92  {
93  auto new_guards = guards;
94  for(auto &op : expr.operands())
95  {
97  f, new_guards, op, access_type, ns, dest); // rec. call
98  new_guards.push_back(op);
99  }
100  return;
101  }
102  else if(expr.id() == ID_or)
103  {
104  auto new_guards = guards;
105  for(auto &op : expr.operands())
106  {
108  f, new_guards, op, access_type, ns, dest); // rec. call
109  new_guards.push_back(not_exprt(op));
110  }
111  return;
112  }
113  else if(expr.id() == ID_if)
114  {
115  const auto &if_expr = to_if_expr(expr);
117  f, guards, if_expr.cond(), access_typet::R, ns, dest); // rec. call
118  auto new_guards = guards;
119  new_guards.push_back(if_expr.cond());
121  f, new_guards, if_expr.true_case(), access_type, ns, dest); // rec. call
122  new_guards.pop_back();
123  new_guards.push_back(not_exprt(if_expr.cond()));
125  f, new_guards, if_expr.false_case(), access_type, ns, dest); // rec. call
126  return;
127  }
128  else if(expr.id() == ID_forall || expr.id() == ID_exists)
129  {
130  return;
131  }
132 
133  // now do operands
134  for(auto &op : expr.operands())
135  c_safety_checks_rec(f, guards, op, access_type, ns, dest); // rec. call
136 
137  if(expr.id() == ID_dereference)
138  {
139  if(expr.type().id() == ID_code)
140  {
141  // dealt with elsewhere
142  }
143  else
144  {
145  auto size_opt = pointer_offset_size(expr.type(), ns);
146  if(size_opt.has_value())
147  {
148  auto size = from_integer(*size_opt, size_type());
149  auto pointer = to_dereference_expr(expr).pointer();
150  auto condition = r_or_w_ok_exprt(
151  access_type == access_typet::W ? ID_w_ok : ID_r_ok, pointer, size);
152  condition.add_source_location() = expr.source_location();
153  auto assertion_source_location = expr.source_location();
154  assertion_source_location.set_property_class("pointer");
155  auto pointer_text = expr2c(pointer, ns);
156  assertion_source_location.set_comment(
157  "pointer " + pointer_text + " safe");
159  guard(guards, condition), assertion_source_location));
160  }
161  }
162  }
163  else if(expr.id() == ID_div)
164  {
165  const auto &div_expr = to_div_expr(expr);
166  if(
167  div_expr.divisor().is_constant() &&
168  !to_constant_expr(div_expr.divisor()).is_zero())
169  {
170  }
171  else
172  {
173  auto zero = from_integer(0, div_expr.type());
174  auto condition = implies_exprt(
175  conjunction(guards), notequal_exprt(div_expr.divisor(), zero));
176  auto source_location = expr.source_location();
177  condition.add_source_location() = expr.source_location();
178  source_location.set_property_class("division-by-zero");
179  source_location.set_comment("division by zero in " + expr2c(expr, ns));
181  guard(guards, condition), source_location));
182  }
183  }
184  else if(expr.id() == ID_mod)
185  {
186  const auto &mod_expr = to_mod_expr(expr);
187  if(
188  mod_expr.divisor().is_constant() &&
189  !to_constant_expr(mod_expr.divisor()).is_zero())
190  {
191  }
192  else
193  {
194  auto zero = from_integer(0, mod_expr.type());
195  auto condition = notequal_exprt(mod_expr.divisor(), zero);
196  auto source_location = expr.source_location();
197  condition.add_source_location() = expr.source_location();
198  source_location.set_property_class("division-by-zero");
199  source_location.set_comment("division by zero in " + expr2c(expr, ns));
201  guard(guards, condition), source_location));
202  }
203  }
204  else if(expr.id() == ID_index)
205  {
206  const auto &index_expr = to_index_expr(expr);
207  auto zero = from_integer(0, index_expr.index().type());
209  index_array_size(index_expr.array().type()), index_expr.index().type());
210  auto condition = and_exprt(
211  binary_relation_exprt(zero, ID_le, index_expr.index()),
212  binary_relation_exprt(size, ID_gt, index_expr.index()));
213  // 'index' may not have a source location, e.g., when implicitly
214  // taking the address of an array.
215  auto source_location = expr.find_source_location();
216  condition.add_source_location() = expr.source_location();
217  source_location.set_property_class("array bounds");
218  source_location.set_comment("array bounds in " + expr2c(expr, ns));
219  dest.add(
220  goto_programt::make_assertion(guard(guards, condition), source_location));
221  }
222 }
223 
225  goto_functionst::function_mapt::value_type &f,
226  const exprt &expr,
227  access_typet access_type,
228  const namespacet &ns,
229  goto_programt &dest)
230 {
231  c_safety_checks_rec(f, {}, expr, access_type, ns, dest);
232 }
233 
234 static exprt offset_is_zero(const exprt &pointer)
235 {
236  auto offset = pointer_offset(pointer);
237  auto zero = from_integer(0, offset.type());
238  return equal_exprt(std::move(offset), std::move(zero));
239 }
240 
242  goto_functionst::function_mapt::value_type &f,
243  const namespacet &ns)
244 {
245  auto &body = f.second.body;
246  goto_programt dest;
247 
248  for(auto it = body.instructions.begin(); it != body.instructions.end(); it++)
249  {
250  if(it->is_assign())
251  {
252  c_safety_checks(f, it->assign_lhs(), access_typet::W, ns, dest);
253  c_safety_checks(f, it->assign_rhs(), access_typet::R, ns, dest);
254  }
255  else if(it->is_function_call())
256  {
257  c_safety_checks(f, it->call_lhs(), access_typet::W, ns, dest);
258  c_safety_checks(f, it->call_function(), access_typet::R, ns, dest);
259  for(const auto &argument : it->call_arguments())
260  c_safety_checks(f, argument, access_typet::R, ns, dest);
261  }
262  else
263  {
264  it->apply([&f, &ns, &dest](const exprt &expr) {
265  c_safety_checks(f, expr, access_typet::R, ns, dest);
266  });
267  }
268 
269  if(it->is_function_call())
270  {
271  const auto &function = it->call_function();
272  if(function.id() == ID_symbol)
273  {
274  const auto &identifier = to_symbol_expr(function).get_identifier();
275  if(identifier == "free")
276  {
277  if(
278  it->call_arguments().size() == 1 &&
279  it->call_arguments()[0].type().id() == ID_pointer)
280  {
281  // Must be 1) dynamically allocated, 2) still alive,
282  // 3) have offset zero, or, alternatively, NULL.
283  const auto &pointer = it->call_arguments()[0];
284  auto condition = or_exprt(
285  equal_exprt(
286  pointer, null_pointer_exprt(to_pointer_type(pointer.type()))),
287  and_exprt(
288  live_object_exprt(pointer),
289  is_dynamic_object_exprt(pointer),
290  offset_is_zero(pointer)));
291  auto source_location = it->source_location();
292  source_location.set_property_class("free");
293  source_location.set_comment(
294  "free argument must be valid dynamic object");
295  dest.add(goto_programt::make_assertion(condition, source_location));
296  }
297  }
298  else if(identifier == "realloc")
299  {
300  if(
301  it->call_arguments().size() == 2 &&
302  it->call_arguments()[0].type().id() == ID_pointer)
303  {
304  // Must be 1) dynamically allocated, 2) still alive,
305  // 3) have offset zero, or, alternatively, NULL.
306  const auto &pointer = it->call_arguments()[0];
307  auto condition = or_exprt(
308  equal_exprt(
309  pointer, null_pointer_exprt(to_pointer_type(pointer.type()))),
310  and_exprt(
311  live_object_exprt(pointer),
312  is_dynamic_object_exprt(pointer),
313  offset_is_zero(pointer)));
314  auto source_location = it->source_location();
315  source_location.set_property_class("realloc");
316  source_location.set_comment(
317  "realloc argument must be valid dynamic object");
318  dest.add(goto_programt::make_assertion(condition, source_location));
319  }
320  }
321  else if(identifier == "memcmp")
322  {
323  if(
324  it->call_arguments().size() == 3 &&
325  it->call_arguments()[0].type().id() == ID_pointer &&
326  it->call_arguments()[1].type().id() == ID_pointer &&
327  it->call_arguments()[2].type().id() == ID_unsignedbv)
328  {
329  // int memcmp(const void *s1, const void *s2, size_t n);
330  const auto &p1 = it->call_arguments()[0];
331  const auto &p2 = it->call_arguments()[1];
332  const auto &size = it->call_arguments()[2];
333  auto condition =
334  and_exprt(r_ok_exprt(p1, size), r_ok_exprt(p2, size));
335  auto source_location = it->source_location();
336  source_location.set_property_class("memcmp");
337  source_location.set_comment("memcmp regions must be valid");
338  dest.add(goto_programt::make_assertion(condition, source_location));
339  }
340  }
341  else if(identifier == "memchr")
342  {
343  if(
344  it->call_arguments().size() == 3 &&
345  it->call_arguments()[0].type().id() == ID_pointer &&
346  it->call_arguments()[2].type().id() == ID_unsignedbv)
347  {
348  // void *memchr(const void *, int, size_t);
349  const auto &p = it->call_arguments()[0];
350  const auto &size = it->call_arguments()[2];
351  auto condition = r_ok_exprt(p, size);
352  auto source_location = it->source_location();
353  source_location.set_property_class("memchr");
354  source_location.set_comment("memchr source must be valid");
355  dest.add(goto_programt::make_assertion(condition, source_location));
356  }
357  }
358  else if(identifier == "memset")
359  {
360  if(
361  it->call_arguments().size() == 3 &&
362  it->call_arguments()[0].type().id() == ID_pointer &&
363  it->call_arguments()[2].type().id() == ID_unsignedbv)
364  {
365  // void *memset(void *b, int c, size_t len);
366  const auto &pointer = it->call_arguments()[0];
367  const auto &size = it->call_arguments()[2];
368  auto condition = w_ok_exprt(pointer, size);
369  auto source_location = it->source_location();
370  source_location.set_property_class("memset");
371  source_location.set_comment("memset destination must be valid");
372  dest.add(goto_programt::make_assertion(condition, source_location));
373  }
374  }
375  else if(identifier == "strlen")
376  {
377  if(
378  it->call_arguments().size() == 1 &&
379  it->call_arguments()[0].type().id() == ID_pointer)
380  {
381  const auto &address = it->call_arguments()[0];
382  auto condition = is_cstring_exprt(address);
383  auto source_location = it->source_location();
384  source_location.set_property_class("strlen");
385  source_location.set_comment("strlen argument must be C string");
386  dest.add(goto_programt::make_assertion(condition, source_location));
387  }
388  }
389  else if(identifier == "__builtin___memset_chk") // clang variant
390  {
391  if(
392  it->call_arguments().size() == 4 &&
393  it->call_arguments()[0].type().id() == ID_pointer &&
394  it->call_arguments()[2].type().id() == ID_unsignedbv)
395  {
396  const auto &pointer = it->call_arguments()[0];
397  const auto &size = it->call_arguments()[2];
398  auto condition = w_ok_exprt(pointer, size);
399  auto source_location = it->source_location();
400  source_location.set_property_class("memset");
401  source_location.set_comment("memset destination must be valid");
402  dest.add(goto_programt::make_assertion(condition, source_location));
403  }
404  }
405  }
406  }
407 
408  std::size_t n = dest.instructions.size();
409  if(n != 0)
410  {
411  body.insert_before_swap(it, dest);
412  dest.clear();
413  it = std::next(it, n);
414  }
415  }
416 }
417 
418 void c_safety_checks(goto_modelt &goto_model)
419 {
420  const namespacet ns(goto_model.symbol_table);
421 
422  for(auto &f : goto_model.goto_functions.function_map)
423  c_safety_checks(f, ns);
424 
425  // update the numbering
427 }
428 
429 void no_assertions(goto_functionst::function_mapt::value_type &f)
430 {
431  auto &body = f.second.body;
432 
433  for(auto it = body.instructions.begin(); it != body.instructions.end(); it++)
434  {
435  if(
436  it->is_assert() &&
437  it->source_location().get_property_class() == ID_assertion)
438  {
439  it->turn_into_skip();
440  }
441  }
442 }
443 
444 void no_assertions(goto_modelt &goto_model)
445 {
446  for(auto &f : goto_model.goto_functions.function_map)
447  no_assertions(f);
448 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static exprt guard(const exprt::operandst &guards, exprt cond)
access_typet
void c_safety_checks_address_rec(goto_functionst::function_mapt::value_type &f, const exprt::operandst &guards, const exprt &expr, const namespacet &ns, goto_programt &dest)
exprt index_array_size(const typet &type)
void c_safety_checks(goto_functionst::function_mapt::value_type &f, const exprt &expr, access_typet access_type, const namespacet &ns, goto_programt &dest)
void no_assertions(goto_functionst::function_mapt::value_type &f)
static exprt offset_is_zero(const exprt &pointer)
void c_safety_checks_rec(goto_functionst::function_mapt::value_type &, const exprt::operandst &guards, const exprt &, access_typet, const namespacet &, goto_programt &)
Checks for Errors in C/C++ Programs.
Boolean AND.
Definition: std_expr.h:2120
const exprt & size() const
Definition: std_types.h:840
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
Equality.
Definition: std_expr.h:1361
Base class for all expressions.
Definition: expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:147
std::vector< exprt > operandst
Definition: expr.h:58
const source_locationt & source_location() const
Definition: expr.h:231
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:47
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
function_mapt function_map
void compute_location_numbers()
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
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:622
void clear()
Clear the goto program.
Definition: goto_program.h:820
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
Boolean implication.
Definition: std_expr.h:2183
const irep_idt & id() const
Definition: irep.h:388
A predicate that indicates that a zero-terminated string starts at the given address.
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: pointer_expr.h:335
A predicate that indicates that the object pointed to is live.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Boolean negation.
Definition: std_expr.h:2327
Disequality.
Definition: std_expr.h:1420
The null pointer constant.
Definition: pointer_expr.h:909
Boolean OR.
Definition: std_expr.h:2228
A predicate that indicates that an address range is ok to read.
Definition: pointer_expr.h:960
A base class for a predicate that indicates that an address range is ok to read or write or both.
Definition: pointer_expr.h:920
void set_property_class(const irep_idt &property_class)
const irep_idt & get_identifier() const
Definition: std_expr.h:160
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2076
The type of an expression, extends irept.
Definition: type.h:29
const constant_exprt & size() const
Definition: std_types.cpp:286
A predicate that indicates that an address range is ok to write.
Definition: pointer_expr.h:989
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4155
Symbol Table + CFG.
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:890
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
Various predicates over pointers in programs.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:83
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2450
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3045
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1272
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1201
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2936
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1113
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
#define size_type
Definition: unistd.c:347