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 
15 
17 
18 #include <util/pointer_expr.h>
19 #include <util/std_expr.h>
20 
22 {
23  assert(!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 
39 
41  const local_may_aliast &local_may_alias,
43  const exprt &lhs,
44  modifiest &modifies)
45 {
46  if(lhs.id() == ID_symbol || lhs.id() == ID_member || lhs.id() == ID_index)
47  modifies.insert(lhs);
48  else if(lhs.id()==ID_dereference)
49  {
50  const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
51  for(const auto &mod : local_may_alias.get(t, ptr.pointer))
52  {
53  if(ptr.offset.is_nil())
54  modifies.insert(dereference_exprt{mod});
55  else
56  modifies.insert(dereference_exprt{plus_exprt{mod, ptr.offset}});
57  }
58  }
59  else if(lhs.id()==ID_if)
60  {
61  const if_exprt &if_expr=to_if_expr(lhs);
62 
63  get_modifies_lhs(local_may_alias, t, if_expr.true_case(), modifies);
64  get_modifies_lhs(local_may_alias, t, if_expr.false_case(), modifies);
65  }
66 }
67 
69  const local_may_aliast &local_may_alias,
70  const loopt &loop,
71  modifiest &modifies)
72 {
74  i_it=loop.begin(); i_it!=loop.end(); i_it++)
75  {
76  const goto_programt::instructiont &instruction=**i_it;
77 
78  if(instruction.is_assign())
79  {
80  const exprt &lhs = instruction.get_assign().lhs();
81  get_modifies_lhs(local_may_alias, *i_it, lhs, modifies);
82  }
83  else if(instruction.is_function_call())
84  {
85  const exprt &lhs = instruction.call_lhs();
86  get_modifies_lhs(local_may_alias, *i_it, lhs, modifies);
87  }
88  }
89 }
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
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:2237
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:628
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2172
pointer_arithmetict::pointer
exprt pointer
Definition: pointer_arithmetic.h:17
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:914
loop_templatet::end
const_iterator end() const
Iterator over this loop's instructions.
Definition: loop_analysis.h:55
exprt
Base class for all expressions.
Definition: expr.h:54
pointer_arithmetict
Definition: pointer_arithmetic.h:16
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:198
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2209
modifiest
std::set< exprt > modifiest
Definition: havoc_utils.h:23
loop_templatet::begin
const_iterator begin() const
Iterator over this loop's instructions.
Definition: loop_analysis.h:49
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:21
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:40
pointer_expr.h
API to expression classes for Pointers.
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:310
loop_templatet
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
pointer_arithmetict::offset
exprt offset
Definition: pointer_arithmetic.h:17
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
goto_programt::instructiont::call_lhs
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:375
loop_utils.h
Helper functions for k-induction and loop invariants.
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2199
get_modifies
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:68
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:529
loop_templatet::empty
bool empty() const
Returns true if this loop contains no instructions.
Definition: loop_analysis.h:67
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:530
local_may_aliast::get
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
Definition: local_may_alias.cpp:115
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
std_expr.h
API to expression classes.
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:646