cprover
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 <map>
15 
16 #include <util/c_types.h>
17 #include <util/format_expr.h>
18 #include <util/format_type.h>
19 #include <util/message.h>
20 #include <util/pointer_expr.h>
23 #include <util/std_code.h>
24 
25 #include <ansi-c/c_expr.h>
26 #include <langapi/language_util.h>
27 
29 #include "utils.h"
30 
32 {
33  // snapshotting instructions and well-definedness checks
34  goto_programt snapshot_program;
35 
36  // add spec targets
37  for(const auto &target : targets)
38  track_spec_target(target, snapshot_program);
39 
40  // add static locals called touched by the replaced function
41  track_static_locals(snapshot_program);
42 
43  // generate havocking instructions for all tracked CARs
44  goto_programt havoc_program;
45  for(const auto &pair : from_spec_assigns)
46  havoc_if_valid(pair.second, havoc_program);
47 
48  for(const auto &pair : from_stack_alloc)
49  havoc_if_valid(pair.second, havoc_program);
50 
51  for(const auto &pair : from_heap_alloc)
52  havoc_if_valid(pair.second, havoc_program);
53 
54  // append to dest
55  dest.destructive_append(snapshot_program);
56  dest.destructive_append(havoc_program);
57 }
58 
60  car_exprt car,
61  goto_programt &dest)
62 {
63  const irep_idt &tracking_comment =
65  car.target(), function_id, ns);
66 
67  source_locationt source_location_no_checks(source_location);
68  add_pragma_disable_pointer_checks(source_location_no_checks);
69 
70  goto_programt skip_program;
71  const auto skip_target =
72  skip_program.add(goto_programt::make_skip(source_location_no_checks));
73 
75  skip_target, not_exprt{car.valid_var()}, source_location_no_checks));
76 
77  if(car.target().id() == ID_pointer_object)
78  {
79  // OTHER __CPROVER_havoc_object(target_snapshot_var)
80  codet code(ID_havoc_object, {car.lower_bound_var()});
81  const auto &inst =
83  inst->source_location_nonconst().set_comment(tracking_comment);
84  }
85  else
86  {
87  // ASSIGN *(target.type() *)__car_lb = nondet(car.target().type())
88  const auto &target_type = car.target().type();
89  side_effect_expr_nondett nondet(target_type, source_location);
90  const auto &inst = dest.add(goto_programt::make_assignment(
92  car.lower_bound_var(), pointer_type(target_type))},
93  nondet,
95  inst->source_location_nonconst().set_comment(tracking_comment);
96  }
97 
98  dest.destructive_append(skip_program);
99 
100  dest.add(
101  goto_programt::make_dead(car.valid_var(), source_location_no_checks));
102 
103  dest.add(
104  goto_programt::make_dead(car.lower_bound_var(), source_location_no_checks));
105 
106  dest.add(
107  goto_programt::make_dead(car.upper_bound_var(), source_location_no_checks));
108 }
API to expression classes that are internal to the C frontend.
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
Class that represents a normalized conditional address range, with:
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.
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:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typet & type()
Return the type of the expression.
Definition: expr.h:82
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:956
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:698
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:880
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:942
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 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 to from DECL symbols to corresponding conditional address ranges.
cond_target_exprt_to_car_mapt from_spec_assigns
Map to from conditional target expressions of assigns clauses to corresponding conditional address ra...
exprt_to_car_mapt from_heap_alloc
Map to from malloc'd symbols to corresponding conditional address ranges.
void track_static_locals(goto_programt &dest)
Search the call graph reachable from the instrumented function to identify local static variables use...
const namespacet ns
Program namespace.
const irep_idt & function_id
Name of the instrumented function.
const irep_idt & id() const
Definition: irep.h:396
Boolean negation.
Definition: std_expr.h:2181
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
Havoc function assigns clauses.
Specify write set in function contracts.
API to expression classes for Pointers.
Pointer Logic.
Various predicates over pointers in programs.
void add_pragma_disable_pointer_checks(source_locationt &location)
Adds a pragma on a source location disable all pointer checks.
Definition: utils.cpp:79
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:269