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 }
exprt & lhs()
Definition: std_code.h:310
Operator to dereference a pointer.
Definition: pointer_expr.h:628
Base class for all expressions.
Definition: expr.h:54
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:375
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
Definition: goto_program.h:198
instructionst::iterator targett
Definition: goto_program.h:646
instructionst::const_iterator const_targett
Definition: goto_program.h:647
The trinary if-then-else operator.
Definition: std_expr.h:2172
exprt & true_case()
Definition: std_expr.h:2199
exprt & false_case()
Definition: std_expr.h:2209
const irep_idt & id() const
Definition: irep.h:407
bool is_nil() const
Definition: irep.h:387
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
loop_instructionst::const_iterator const_iterator
Definition: loop_analysis.h:46
The plus expression Associativity is not specified.
Definition: std_expr.h:914
std::set< exprt > modifiest
Definition: havoc_utils.h:23
Field-insensitive, location-sensitive may-alias analysis.
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:68
goto_programt::targett get_loop_exit(const loopt &loop)
Definition: loop_utils.cpp:21
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
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:684
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237