cprover
Loading...
Searching...
No Matches
utils.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Utility functions for code contracts.
4
5Author: Saswat Padhi, saspadhi@amazon.com
6
7Date: September 2021
8
9\*******************************************************************/
10
11#include "utils.h"
12
13#include <goto-programs/cfg.h>
14
15#include <util/fresh_symbol.h>
16#include <util/graph.h>
17#include <util/message.h>
18#include <util/pointer_expr.h>
20#include <util/simplify_expr.h>
21
23
25 const source_locationt location,
26 const namespacet &ns,
27 const exprt &expr,
28 goto_programt &dest,
29 const std::function<void()> &havoc_code_impl)
30{
31 goto_programt skip_program;
32 const auto skip_target = skip_program.add(goto_programt::make_skip(location));
33
34 // skip havocing only if all pointer derefs in the expression are valid
35 // (to avoid spurious pointer deref errors)
37 skip_target, not_exprt{all_dereferences_are_valid(expr, ns)}, location));
38
39 havoc_code_impl();
40
41 // add the final skip target
42 dest.destructive_append(skip_program);
43}
44
46 const source_locationt location,
47 const exprt &expr,
48 goto_programt &dest) const
49{
50 append_safe_havoc_code_for_expr(location, ns, expr, dest, [&]() {
52 });
53}
54
56 const source_locationt location,
57 const exprt &expr,
58 goto_programt &dest) const
59{
60 append_safe_havoc_code_for_expr(location, ns, expr, dest, [&]() {
62 });
63}
64
66 const source_locationt location,
67 const exprt &expr,
68 goto_programt &dest) const
69{
70 if(expr.id() == ID_pointer_object)
71 {
72 append_object_havoc_code_for_expr(location, expr.operands().front(), dest);
73 return;
74 }
75
76 havoc_utilst::append_havoc_code_for_expr(location, expr, dest);
77}
78
80{
81 location.add_pragma("disable:pointer-check");
82 location.add_pragma("disable:pointer-primitive-check");
83 location.add_pragma("disable:pointer-overflow-check");
84 location.add_pragma("disable:signed-overflow-check");
85 location.add_pragma("disable:unsigned-overflow-check");
86 location.add_pragma("disable:conversion-check");
87}
88
91{
93 return instr;
94}
95
97{
100 return prog;
101}
102
104{
106}
107
110{
112 return instr;
113}
114
116{
119 return prog;
120}
121
123{
124 exprt::operandst validity_checks;
125
126 if(expr.id() == ID_dereference)
127 validity_checks.push_back(
128 good_pointer_def(to_dereference_expr(expr).pointer(), ns));
129
130 for(const auto &op : expr.operands())
131 validity_checks.push_back(all_dereferences_are_valid(op, ns));
132
133 return conjunction(validity_checks);
134}
135
137 const std::vector<symbol_exprt> &lhs,
138 const std::vector<symbol_exprt> &rhs)
139{
140 PRECONDITION(lhs.size() == rhs.size());
141
142 if(lhs.empty())
143 {
144 return false_exprt();
145 }
146
147 // Store conjunctions of equalities.
148 // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
149 // l2, l3>.
150 // Then this vector stores <s1 == l1, s1 == l1 && s2 == l2,
151 // s1 == l1 && s2 == l2 && s3 == l3>.
152 // In fact, the last element is unnecessary, so we do not create it.
153 exprt::operandst equality_conjunctions(lhs.size());
154 equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]);
155 for(size_t i = 1; i < equality_conjunctions.size() - 1; i++)
156 {
157 binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]};
158 equality_conjunctions[i] =
159 and_exprt(equality_conjunctions[i - 1], component_i_equality);
160 }
161
162 // Store inequalities between the i-th components of the input vectors
163 // (i.e. lhs and rhs).
164 // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
165 // l2, l3>.
166 // Then this vector stores <s1 < l1, s1 == l1 && s2 < l2, s1 == l1 &&
167 // s2 == l2 && s3 < l3>.
168 exprt::operandst lexicographic_individual_comparisons(lhs.size());
169 lexicographic_individual_comparisons[0] =
170 binary_relation_exprt(lhs[0], ID_lt, rhs[0]);
171 for(size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
172 {
173 binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]};
174 lexicographic_individual_comparisons[i] =
175 and_exprt(equality_conjunctions[i - 1], component_i_less_than);
176 }
177 return disjunction(lexicographic_individual_comparisons);
178}
179
181 goto_programt &destination,
183 goto_programt &payload)
184{
185 const auto offset = payload.instructions.size();
186 destination.insert_before_swap(target, payload);
187 std::advance(target, offset);
188}
189
191 const typet &type,
192 const source_locationt &location,
193 const irep_idt &mode,
194 symbol_table_baset &symtab,
195 std::string suffix,
196 bool is_auxiliary)
197{
198 symbolt &new_symbol = get_fresh_aux_symbol(
199 type, id2string(location.get_function()), suffix, location, mode, symtab);
200 new_symbol.is_auxiliary = is_auxiliary;
201 return new_symbol;
202}
203
205{
206 for(auto &instruction : goto_program.instructions)
207 {
208 if(
209 instruction.is_goto() &&
210 simplify_expr(instruction.get_condition(), ns).is_false())
211 instruction.turn_into_skip();
212 }
213}
214
216 const goto_programt &goto_program,
217 namespacet &ns,
218 messaget &log)
219{
220 // create cfg from instruction list
222 cfg(goto_program);
223
224 // check that all nodes are there
225 INVARIANT(
226 goto_program.instructions.size() == cfg.size(),
227 "Instruction list vs CFG size mismatch.");
228
229 // compute SCCs
231 std::vector<idxt> node_to_scc(cfg.size(), -1);
232 auto nof_sccs = cfg.SCCs(node_to_scc);
233
234 // compute size of each SCC
235 std::vector<int> scc_size(nof_sccs, 0);
236 for(auto scc : node_to_scc)
237 {
238 INVARIANT(
239 0 <= scc && scc < nof_sccs, "Could not determine SCC for instruction");
240 scc_size[scc]++;
241 }
242
243 // check they are all of size 1
244 for(size_t scc_id = 0; scc_id < nof_sccs; scc_id++)
245 {
246 auto size = scc_size[scc_id];
247 if(size > 1)
248 {
249 log.error() << "Found CFG SCC with size " << size << messaget::eom;
250 for(const auto &node_id : node_to_scc)
251 {
252 if(node_to_scc[node_id] == scc_id)
253 {
254 const auto &pc = cfg[node_id].PC;
255 goto_program.output_instruction(ns, "", log.error(), *pc);
256 log.error() << messaget::eom;
257 }
258 }
259 return false;
260 }
261 }
262 return true;
263}
264
267 " (assigned by the contract of ";
268
270 const exprt &target,
271 const irep_idt &function_id,
272 const namespacet &ns)
273{
274 return from_expr(ns, target.id(), target) +
276}
277
279{
281 std::string::npos;
282}
Control Flow Graph.
Boolean AND.
Definition: std_expr.h:1974
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO pr...
Definition: cfg.h:87
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2865
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
source_locationt & source_location_nonconst()
Definition: goto_program.h:337
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:598
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
instructionst::iterator targett
Definition: goto_program.h:592
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:698
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single 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())
std::size_t node_indext
Definition: graph.h:37
std::size_t SCCs(std::vector< node_indext > &subgraph_nr) const
Computes strongly-connected components of a graph and yields a vector expressing a mapping from nodes...
Definition: graph.h:832
std::size_t size() const
Definition: graph.h:212
void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc a single expression expr
Definition: utils.cpp:65
void append_object_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc the underlying object of expr
Definition: utils.cpp:45
const namespacet & ns
Definition: utils.h:51
void append_scalar_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc the value of expr
Definition: utils.cpp:55
virtual void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc a single expression expr
Definition: havoc_utils.cpp:29
virtual void append_object_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the underlying object of expr
Definition: havoc_utils.cpp:46
virtual void append_scalar_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the value of expr
Definition: havoc_utils.cpp:57
const irep_idt & id() const
Definition: irep.h:396
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Boolean negation.
Definition: std_expr.h:2181
const irep_idt & get_function() const
void add_pragma(const irep_idt &pragma)
The symbol table base class interface.
Symbol table entry.
Definition: symbol.h:28
bool is_auxiliary
Definition: symbol.h:67
The type of an expression, extends irept.
Definition: type.h:29
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
#define Forall_goto_program_instructions(it, program)
A Template Class for Graphs.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
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:704
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
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:34
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:22
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
static void append_safe_havoc_code_for_expr(const source_locationt location, const namespacet &ns, const exprt &expr, goto_programt &dest, const std::function< void()> &havoc_code_impl)
Definition: utils.cpp:24
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symtab, std::string suffix, bool is_auxiliary)
Adds a fresh and uniquely named symbol to the symbol table.
Definition: utils.cpp:190
bool is_loop_free(const goto_programt &goto_program, namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
Definition: utils.cpp:215
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
Generate a validity check over all dereferences in an expression.
Definition: utils.cpp:122
bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)
Returns true if the given comment matches the type of comments created by make_assigns_clause_replace...
Definition: utils.cpp:278
void insert_before_swap_and_advance(goto_programt &destination, goto_programt::targett &target, goto_programt &payload)
Insert a goto program before a target instruction iterator and advance the iterator.
Definition: utils.cpp:180
void simplify_gotos(goto_programt &goto_program, namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
Definition: utils.cpp:204
static const char ASSIGNS_CLAUSE_REPLACEMENT_TRACKING[]
Prefix for comments added to track assigns clause replacement.
Definition: utils.cpp:266
void add_pragma_disable_assigns_check(source_locationt &location)
Adds a pragma on a source_locationt to disable inclusion checking.
Definition: utils.cpp:103
exprt generate_lexicographic_less_than_check(const std::vector< symbol_exprt > &lhs, const std::vector< symbol_exprt > &rhs)
Generate a lexicographic less-than comparison over ordered tuples.
Definition: utils.cpp:136
#define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK
Definition: utils.h:27