cprover
Loading...
Searching...
No Matches
havoc_assigns_clause_targets.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Havoc multiple and possibly dependent targets simultaneously
4
5Author: 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>
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