cprover
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 
14 #include <util/expr_util.h>
15 #include <util/pointer_expr.h>
16 #include <util/std_expr.h>
17 
19 
20 #include <analyses/natural_loops.h>
22 
24 {
25 public:
26  explicit loop_utils_is_constantt(const modifiest &mod) : modifies(mod)
27  {
28  }
29  bool is_constant(const exprt &expr) const override
30  {
31  // Besides the "usual" constants (checked in is_constantt::is_constant),
32  // we also treat unmodified symbols as constants
33  if(expr.id() == ID_symbol && modifies.find(expr) == modifies.end())
34  return true;
35 
36  return is_constantt::is_constant(expr);
37  }
38 
39 protected:
41 };
42 
44 {
45  assert(!loop.empty());
46 
47  // find the last instruction in the loop
48  std::map<unsigned, goto_programt::targett> loop_map;
49 
50  for(loopt::const_iterator l_it=loop.begin();
51  l_it!=loop.end();
52  l_it++)
53  loop_map[(*l_it)->location_number]=*l_it;
54 
55  // get the one with the highest number
56  goto_programt::targett last=(--loop_map.end())->second;
57 
58  return ++last;
59 }
60 
62  const goto_programt::targett loop_head,
63  const exprt &lhs,
64  goto_programt &dest)
65 {
66  side_effect_expr_nondett rhs(lhs.type(), loop_head->source_location);
67 
69  lhs, std::move(rhs), loop_head->source_location));
70  t->code_nonconst().add_source_location() = loop_head->source_location;
71 }
72 
74  const goto_programt::targett loop_head,
75  const exprt &lhs,
76  goto_programt &dest)
77 {
78  codet havoc(ID_havoc_object);
79  havoc.add_source_location() = loop_head->source_location;
80  havoc.add_to_operands(lhs);
81 
82  dest.add(goto_programt::make_other(havoc, loop_head->source_location));
83 }
84 
86  const goto_programt::targett loop_head,
87  const modifiest &modifies,
88  goto_programt &dest)
89 {
91  for(const auto &lhs : modifies)
92  {
93  if(lhs.id() == ID_index || lhs.id() == ID_dereference)
94  {
95  address_of_exprt address_of_lhs(lhs);
96  if(!is_constant(address_of_lhs))
97  {
98  build_havoc_code_for_object(loop_head, address_of_lhs, dest);
99  continue;
100  }
101  }
102 
103  build_havoc_code_for_scalar(loop_head, lhs, dest);
104  }
105 }
106 
108  const local_may_aliast &local_may_alias,
110  const exprt &lhs,
111  modifiest &modifies)
112 {
113  if(lhs.id() == ID_symbol || lhs.id() == ID_member || lhs.id() == ID_index)
114  modifies.insert(lhs);
115  else if(lhs.id()==ID_dereference)
116  {
117  const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
118  for(const auto &mod : local_may_alias.get(t, ptr.pointer))
119  {
120  if(ptr.offset.is_nil())
121  modifies.insert(dereference_exprt{mod});
122  else
123  modifies.insert(dereference_exprt{plus_exprt{mod, ptr.offset}});
124  }
125  }
126  else if(lhs.id()==ID_if)
127  {
128  const if_exprt &if_expr=to_if_expr(lhs);
129 
130  get_modifies_lhs(local_may_alias, t, if_expr.true_case(), modifies);
131  get_modifies_lhs(local_may_alias, t, if_expr.false_case(), modifies);
132  }
133 }
134 
136  const local_may_aliast &local_may_alias,
137  const loopt &loop,
138  modifiest &modifies)
139 {
141  i_it=loop.begin(); i_it!=loop.end(); i_it++)
142  {
143  const goto_programt::instructiont &instruction=**i_it;
144 
145  if(instruction.is_assign())
146  {
147  const exprt &lhs = instruction.get_assign().lhs();
148  get_modifies_lhs(local_may_alias, *i_it, lhs, modifies);
149  }
150  else if(instruction.is_function_call())
151  {
152  const exprt &lhs = instruction.get_function_call().lhs();
153  get_modifies_lhs(local_may_alias, *i_it, lhs, modifies);
154  }
155  }
156 }
is_constantt
Determine whether an expression is constant.
Definition: expr_util.h:87
loop_utils_is_constantt
Definition: loop_utils.cpp:24
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:442
pointer_arithmetic.h
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2151
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:386
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
build_havoc_code_for_object
void build_havoc_code_for_object(const goto_programt::targett loop_head, const exprt &lhs, goto_programt &dest)
Definition: loop_utils.cpp:73
pointer_arithmetict::pointer
exprt pointer
Definition: pointer_arithmetic.h:17
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:670
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
exprt
Base class for all expressions.
Definition: expr.h:54
pointer_arithmetict
Definition: pointer_arithmetic.h:16
loop_utils_is_constantt::is_constant
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
Definition: loop_utils.cpp:29
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1240
loopt
natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
local_may_aliast
Definition: local_may_alias.h:26
goto_programt::instructiont::get_assign
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
Definition: goto_program.h:199
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1008
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2123
is_constantt::is_constant
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:229
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
modifiest
std::set< exprt > modifiest
Definition: loop_utils.h:17
loop_templatet::const_iterator
loop_instructionst::const_iterator const_iterator
Definition: loop_analysis.h:46
local_may_alias.h
Field-insensitive, location-sensitive may-alias analysis.
get_loop_exit
goto_programt::targett get_loop_exit(const loopt &loop)
Definition: loop_utils.cpp:43
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
get_modifies_lhs
void get_modifies_lhs(const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, modifiest &modifies)
Definition: loop_utils.cpp:107
pointer_expr.h
API to expression classes for Pointers.
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
goto_programt::instructiont::get_function_call
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
Definition: goto_program.h:319
pointer_arithmetict::offset
exprt offset
Definition: pointer_arithmetic.h:17
build_havoc_code_for_scalar
void build_havoc_code_for_scalar(const goto_programt::targett loop_head, const exprt &lhs, goto_programt &dest)
Definition: loop_utils.cpp:61
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
loop_utils.h
Helper functions for k-induction and loop invariants.
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
loop_utils_is_constantt::loop_utils_is_constantt
loop_utils_is_constantt(const modifiest &mod)
Definition: loop_utils.cpp:26
expr_util.h
Deprecated expression utility functions.
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2113
get_modifies
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:135
natural_loops.h
Compute natural loops in a goto_function.
goto_programt::make_other
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:897
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:444
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:144
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:564
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:243
build_havoc_code
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: loop_utils.cpp:85
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:445
local_may_aliast::get
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
Definition: local_may_alias.cpp:116
is_constant
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
loop_utils_is_constantt::modifies
const modifiest & modifies
Definition: loop_utils.cpp:40