cprover
utils.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Utility functions for code contracts.
4 
5 Author: Saswat Padhi, saspadhi@amazon.com
6 
7 Date: 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 
22 #include <langapi/language_util.h>
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,
182  goto_programt::targett &target,
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 
204 void simplify_gotos(goto_programt &goto_program, namespacet &ns)
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) +
275  ASSIGNS_CLAUSE_REPLACEMENT_TRACKING + id2string(function_id) + ")";
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
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
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
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_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