CBMC
havoc_assigns_clause_targets.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Havoc multiple and possibly dependent targets simultaneously
4 
5 Author: Remi Delmas, delmasrd@amazon.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/c_types.h>
15 #include <util/message.h>
16 #include <util/pointer_expr.h>
17 #include <util/std_code.h>
18 
20 #include "utils.h"
21 
23 {
24  // snapshotting instructions and well-definedness checks
25  goto_programt snapshot_program;
26 
27  // add static locals called touched by the replaced function
28  track_static_locals(snapshot_program);
29 
30  // add spec targets
31  for(const auto &target : targets)
32  track_spec_target(target, snapshot_program);
33 
34  // generate havocking instructions for all tracked CARs
35  goto_programt havoc_program;
36  for(const auto &pair : from_spec_assigns)
37  havoc_if_valid(pair.second, havoc_program);
38 
39  for(const auto &pair : from_stack_alloc)
40  havoc_if_valid(pair.second, havoc_program);
41 
42  for(const auto &car : from_heap_alloc)
43  havoc_if_valid(car, havoc_program);
44 
45  for(const auto &pair : from_static_local)
46  {
47  havoc_static_local(pair.second, havoc_program);
48  }
49 
50  // append to dest
51  dest.destructive_append(snapshot_program);
52  dest.destructive_append(havoc_program);
53 }
54 
56  car_exprt car,
57  goto_programt &dest)
58 {
59  const irep_idt &tracking_comment =
61  car.target(), function_id, ns);
62 
63  source_locationt source_location_no_checks(source_location);
64  add_pragma_disable_pointer_checks(source_location_no_checks);
65 
66  goto_programt skip_program;
67  const auto skip_target =
68  skip_program.add(goto_programt::make_skip(source_location_no_checks));
69 
71  skip_target, boolean_negate(car.valid_var()), source_location_no_checks));
72 
74  {
75  // OTHER __CPROVER_havoc_object(target_snapshot_var)
76  codet code(ID_havoc_object, {car.lower_bound_var()});
77  source_locationt annotated_location = source_location;
78  annotated_location.set_comment(tracking_comment);
79  dest.add(goto_programt::make_other(code, annotated_location));
80  }
82  {
83  // This is a slice target. We use goto convert's do_havoc_slice()
84  // code generation, provided by cleanert.
85  cleanert cleaner(st, log.get_message_handler());
86  const auto &mode = st.lookup_ref(function_id).mode;
87  const auto &funcall = to_side_effect_expr_function_call(car.target());
88  const auto &function = to_symbol_expr(funcall.function());
89  exprt::operandst arguments;
90  arguments.push_back(car.lower_bound_var());
91  arguments.push_back(car.target_size());
92  cleaner.do_havoc_slice(function, arguments, dest, mode);
93  }
95  {
96  // a target where the size is derived from the type of the target
97  // ASSIGN *(target.type() *)__car_lb = nondet(car.target().type())
98  const auto &target_type = car.target().type();
99  side_effect_expr_nondett nondet(target_type, source_location);
100  source_locationt annotated_location = source_location;
101  annotated_location.set_comment(tracking_comment);
104  car.lower_bound_var(), pointer_type(target_type))},
105  nondet,
106  annotated_location));
107  }
108  else
109  {
110  UNREACHABLE;
111  }
112 
113  dest.destructive_append(skip_program);
114 
115  dest.add(
116  goto_programt::make_dead(car.valid_var(), source_location_no_checks));
117 
118  dest.add(
119  goto_programt::make_dead(car.lower_bound_var(), source_location_no_checks));
120 
121  dest.add(
122  goto_programt::make_dead(car.upper_bound_var(), source_location_no_checks));
123 }
124 
126  car_exprt car,
127  goto_programt &dest)
128 {
129  // We havoc the target expression directly for local statics
130  // instead of the __car_lb pointer because we know statics never die
131  // and cannot be involved in in dependencies
132  // since we cannot talk about them in contracts.
133  const irep_idt &tracking_comment =
135  car.target(), function_id, ns);
136 
137  source_locationt source_location_no_checks(source_location);
138  add_pragma_disable_pointer_checks(source_location_no_checks);
139 
140  goto_programt skip_program;
141  const auto skip_target =
142  skip_program.add(goto_programt::make_skip(source_location_no_checks));
143 
145  skip_target, boolean_negate(car.valid_var()), source_location_no_checks));
146 
147  const auto &target_type = car.target().type();
148  side_effect_expr_nondett nondet(target_type, source_location);
149  source_locationt annotated_location = source_location;
150  annotated_location.set_comment(tracking_comment);
151  add_propagate_static_local_pragma(annotated_location);
152  dest.add(
153  goto_programt::make_assignment(car.target(), nondet, annotated_location));
154 
155  dest.destructive_append(skip_program);
156 
157  dest.add(
158  goto_programt::make_dead(car.valid_var(), source_location_no_checks));
159 
160  dest.add(
161  goto_programt::make_dead(car.lower_bound_var(), source_location_no_checks));
162 
163  dest.add(
164  goto_programt::make_dead(car.upper_bound_var(), source_location_no_checks));
165 }
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
Class that represents a normalized conditional address range, with:
const car_havoc_methodt havoc_method
Method to use to havod the target.
const exprt & target_size() const
Size of the target in bytes.
const symbol_exprt & upper_bound_var() const
Identifier of the upper address bound snapshot variable.
const symbol_exprt & valid_var() const
Identifier of the validity snapshot variable.
const exprt & target() const
The target expression.
const symbol_exprt & lower_bound_var() const
Identifier of the lower address bound snapshot variable.
Class that allows to clean expressions of side effects and to generate havoc_slice expressions.
Definition: utils.h:37
void do_havoc_slice(const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
Definition: utils.h:54
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
Operator to dereference a pointer.
Definition: pointer_expr.h:834
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
std::vector< exprt > operandst
Definition: expr.h:58
typet & type()
Return the type of the expression.
Definition: expr.h:84
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:971
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:722
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:891
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:957
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
const std::vector< exprt > & targets
void havoc_if_valid(car_exprt car, goto_programt &dest)
Generates instructions to conditionally havoc the given conditional address range expression car,...
void get_instructions(goto_programt &dest)
Generates the assigns clause replacement instructions in dest.
void havoc_static_local(car_exprt car, goto_programt &dest)
Havoc a static local expression.
void track_spec_target(const exprt &expr, goto_programt &dest)
Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in ...
symbol_exprt_to_car_mapt from_stack_alloc
Map from DECL symbols to corresponding conditional address ranges.
cond_target_exprt_to_car_mapt from_spec_assigns
Map from conditional target expressions of assigns clauses to corresponding conditional address range...
symbol_table_baset & st
Program symbol table.
symbol_exprt_to_car_mapt from_static_local
Map to from detected or propagated static local symbols to corresponding conditional address ranges.
const irep_idt & mode
Language mode.
void track_static_locals(goto_programt &dest)
Searches the goto instructions reachable from the start to the end of the instrumented function's ins...
const namespacet ns
Program namespace.
const irep_idt & function_id
Name of the instrumented function.
message_handlert & get_message_handler()
Definition: message.h:183
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
void set_comment(const irep_idt &comment)
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
irep_idt mode
Language mode.
Definition: symbol.h:49
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2081
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:103
Havoc function assigns clauses.
void add_pragma_disable_pointer_checks(source_locationt &location)
Adds a pragma on a source location disable all pointer checks.
void add_propagate_static_local_pragma(source_locationt &source_location)
Sets a pragma to mark assignments to static local variables that need to be propagated upwards in the...
Specify write set in function contracts.
API to expression classes for Pointers.
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1739
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
irep_idt make_assigns_clause_replacement_tracking_comment(const exprt &target, const irep_idt &function_id, const namespacet &ns)
Returns an irep_idt that essentially says that target was assigned by the contract of function_id.
Definition: utils.cpp:329