cprover
havoc_utils.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Utilities for building havoc code for expressions.
4 
5 Author: Saswat Padhi, saspadhi@amazon.com
6 
7 Date: July 2021
8 
9 \*******************************************************************/
10 
13 
14 #include "havoc_utils.h"
15 
16 #include <util/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/pointer_expr.h>
19 
21  const source_locationt source_location,
22  const exprt &expr,
23  goto_programt &dest,
24  const std::function<void()> &havoc_code_impl)
25 {
26  goto_programt skip_program;
27  const auto skip_target =
28  skip_program.add(goto_programt::make_skip(source_location));
29 
30  // for deref expressions, check for validity of underlying pointer,
31  // and skip havocing if invalid (to avoid spurious pointer deref errors)
32  if(expr.id() == ID_dereference)
33  {
34  const auto condition = not_exprt(w_ok_exprt(
35  to_dereference_expr(expr).pointer(),
37  dest.add(goto_programt::make_goto(skip_target, condition, source_location));
38  }
39 
40  havoc_code_impl();
41 
42  // for deref expressions, add the final skip target
43  if(expr.id() == ID_dereference)
44  dest.destructive_append(skip_program);
45 }
46 
48  const source_locationt source_location,
49  const exprt &expr,
50  goto_programt &dest)
51 {
52  append_safe_havoc_code_for_expr(source_location, expr, dest, [&]() {
53  codet havoc(ID_havoc_object);
54  havoc.add_source_location() = source_location;
55  havoc.add_to_operands(expr);
56  dest.add(goto_programt::make_other(havoc, source_location));
57  });
58 }
59 
61  const source_locationt source_location,
62  const exprt &expr,
63  goto_programt &dest)
64 {
65  append_safe_havoc_code_for_expr(source_location, expr, dest, [&]() {
66  side_effect_expr_nondett rhs(expr.type(), source_location);
67  goto_programt::targett t = dest.add(
68  goto_programt::make_assignment(expr, std::move(rhs), source_location));
69  t->code_nonconst().add_source_location() = source_location;
70  });
71 }
72 
74  const source_locationt source_location,
75  const modifiest &modifies,
76  goto_programt &dest)
77 {
79  for(const auto &expr : modifies)
80  {
81  if(expr.id() == ID_index || expr.id() == ID_dereference)
82  {
83  address_of_exprt address_of_expr(expr);
84  if(!is_constant(address_of_expr))
85  {
87  source_location, address_of_expr, dest);
88  continue;
89  }
90  }
91 
92  append_scalar_havoc_code_for_expr(source_location, expr, dest);
93  }
94 }
arith_tools.h
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
havoc_utils_is_constantt
Definition: havoc_utils.h:26
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
exprt
Base class for all expressions.
Definition: expr.h:54
havoc_utils.h
Utilities for building havoc code for expressions.
append_safe_havoc_code_for_expr
void append_safe_havoc_code_for_expr(const source_locationt source_location, const exprt &expr, goto_programt &dest, const std::function< void()> &havoc_code_impl)
Definition: havoc_utils.cpp:20
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1082
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1056
modifiest
std::set< exprt > modifiest
Definition: havoc_utils.h:23
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
append_scalar_havoc_code_for_expr
void append_scalar_havoc_code_for_expr(const source_locationt source_location, const exprt &expr, goto_programt &dest)
Definition: havoc_utils.cpp:60
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:909
pointer_expr.h
API to expression classes for Pointers.
append_object_havoc_code_for_expr
void append_object_havoc_code_for_expr(const source_locationt source_location, const exprt &expr, goto_programt &dest)
Definition: havoc_utils.cpp:47
unsigned_int_type
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
irept::id
const irep_idt & id() const
Definition: irep.h:407
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:736
source_locationt
Definition: source_location.h:19
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
w_ok_exprt
A predicate that indicates that an address range is ok to write.
Definition: pointer_expr.h:761
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
goto_programt::make_other
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:971
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
append_havoc_code
void append_havoc_code(const source_locationt source_location, const modifiest &modifies, goto_programt &dest)
Definition: havoc_utils.cpp:73
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:235
is_constant
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
c_types.h
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:646
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
not_exprt
Boolean negation.
Definition: std_expr.h:2127