CBMC
loop_utils.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Helper functions for k-induction and loop invariants
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "loop_utils.h"
13 
15 
17 
18 #include <util/pointer_expr.h>
19 #include <util/std_expr.h>
20 
22 {
23  PRECONDITION(!loop.empty());
24 
25  // find the last instruction in the loop
26  std::map<unsigned, goto_programt::targett> loop_map;
27 
28  for(loopt::const_iterator l_it=loop.begin();
29  l_it!=loop.end();
30  l_it++)
31  loop_map[(*l_it)->location_number]=*l_it;
32 
33  // get the one with the highest number
34  goto_programt::targett last=(--loop_map.end())->second;
35 
36  return ++last;
37 }
38 
40  const local_may_aliast &local_may_alias,
42  const exprt &lhs,
43  assignst &assigns)
44 {
46  local_may_alias, t, lhs, assigns, [](const exprt &e) { return true; });
47 }
48 
50  const local_may_aliast &local_may_alias,
52  const exprt &lhs,
53  assignst &assigns,
54  std::function<bool(const exprt &)> predicate)
55 {
56  if(
57  (lhs.id() == ID_symbol || lhs.id() == ID_member || lhs.id() == ID_index) &&
58  predicate(lhs))
59  {
60  assigns.insert(lhs);
61  }
62  else if(lhs.id() == ID_dereference)
63  {
64  const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
65  for(const auto &mod : local_may_alias.get(t, ptr.pointer))
66  {
67  const typecast_exprt typed_mod{mod, ptr.pointer.type()};
68  if(mod.id() == ID_unknown)
69  {
70  continue;
71  }
72  exprt to_insert;
73  if(ptr.offset.is_nil())
74  to_insert = dereference_exprt{typed_mod};
75  else
76  to_insert = dereference_exprt{plus_exprt{typed_mod, ptr.offset}};
77  if(predicate(to_insert))
78  assigns.insert(std::move(to_insert));
79  }
80  }
81  else if(lhs.id() == ID_if)
82  {
83  const if_exprt &if_expr = to_if_expr(lhs);
84 
85  get_assigns_lhs(local_may_alias, t, if_expr.true_case(), assigns);
86  get_assigns_lhs(local_may_alias, t, if_expr.false_case(), assigns);
87  }
88 }
89 
91  const local_may_aliast &local_may_alias,
92  const loopt &loop,
93  assignst &assigns)
94 {
96  local_may_alias, loop, assigns, [](const exprt &e) { return true; });
97 }
98 
100  const local_may_aliast &local_may_alias,
101  const loopt &loop,
102  assignst &assigns,
103  std::function<bool(const exprt &)> predicate)
104 {
105  for(loopt::const_iterator i_it = loop.begin(); i_it != loop.end(); i_it++)
106  {
107  const goto_programt::instructiont &instruction = **i_it;
108 
109  if(instruction.is_assign())
110  {
111  const exprt &lhs = instruction.assign_lhs();
112  get_assigns_lhs(local_may_alias, *i_it, lhs, assigns, predicate);
113  }
114  else if(instruction.is_function_call())
115  {
116  const exprt &lhs = instruction.call_lhs();
117  get_assigns_lhs(local_may_alias, *i_it, lhs, assigns, predicate);
118  }
119  }
120 }
Operator to dereference a pointer.
Definition: pointer_expr.h:834
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:286
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:200
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
The trinary if-then-else operator.
Definition: std_expr.h:2370
exprt & true_case()
Definition: std_expr.h:2397
exprt & false_case()
Definition: std_expr.h:2407
const irep_idt & id() const
Definition: irep.h:388
bool is_nil() const
Definition: irep.h:368
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
Semantic type conversion.
Definition: std_expr.h:2068
std::set< exprt > assignst
Definition: havoc_utils.h:22
Field-insensitive, location-sensitive may-alias analysis.
void get_assigns_lhs(const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, assignst &assigns)
Definition: loop_utils.cpp:39
goto_programt::targett get_loop_exit(const loopt &loop)
Definition: loop_utils.cpp:21
void get_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
Definition: loop_utils.cpp:90
Helper functions for k-induction and loop invariants.
natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
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:890
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2450