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/std_expr.h>
15 
16 #include <analyses/natural_loops.h>
18 
20 {
21  assert(!loop.empty());
22 
23  // find the last instruction in the loop
24  std::map<unsigned, goto_programt::targett> loop_map;
25 
26  for(loopt::const_iterator l_it=loop.begin();
27  l_it!=loop.end();
28  l_it++)
29  loop_map[(*l_it)->location_number]=*l_it;
30 
31  // get the one with the highest number
32  goto_programt::targett last=(--loop_map.end())->second;
33 
34  return ++last;
35 }
36 
38  const goto_programt::targett loop_head,
39  const modifiest &modifies,
40  goto_programt &dest)
41 {
42  for(modifiest::const_iterator
43  m_it=modifies.begin();
44  m_it!=modifies.end();
45  m_it++)
46  {
47  exprt lhs=*m_it;
48  exprt rhs =
50 
52  t->function=loop_head->function;
53  t->source_location=loop_head->source_location;
54  t->code=code_assignt(lhs, rhs);
55  t->code.add_source_location()=loop_head->source_location;
56  }
57 }
58 
59 static void get_modifies_lhs(
60  const local_may_aliast &local_may_alias,
62  const exprt &lhs,
63  modifiest &modifies)
64 {
65  if(lhs.id()==ID_symbol)
66  modifies.insert(lhs);
67  else if(lhs.id()==ID_dereference)
68  {
69  modifiest m=local_may_alias.get(t, to_dereference_expr(lhs).pointer());
70  for(modifiest::const_iterator m_it=m.begin();
71  m_it!=m.end(); m_it++)
72  get_modifies_lhs(local_may_alias, t, *m_it, modifies);
73  }
74  else if(lhs.id()==ID_member)
75  {
76  }
77  else if(lhs.id()==ID_index)
78  {
79  }
80  else if(lhs.id()==ID_if)
81  {
82  const if_exprt &if_expr=to_if_expr(lhs);
83 
84  get_modifies_lhs(local_may_alias, t, if_expr.true_case(), modifies);
85  get_modifies_lhs(local_may_alias, t, if_expr.false_case(), modifies);
86  }
87 }
88 
90  const local_may_aliast &local_may_alias,
91  const loopt &loop,
92  modifiest &modifies)
93 {
94  for(loopt::const_iterator
95  i_it=loop.begin(); i_it!=loop.end(); i_it++)
96  {
97  const goto_programt::instructiont &instruction=**i_it;
98 
99  if(instruction.is_assign())
100  {
101  const exprt &lhs=to_code_assign(instruction.code).lhs();
102  get_modifies_lhs(local_may_alias, *i_it, lhs, modifies);
103  }
104  else if(instruction.is_function_call())
105  {
106  const exprt &lhs=to_code_function_call(instruction.code).lhs();
107  get_modifies_lhs(local_may_alias, *i_it, lhs, modifies);
108  }
109  }
110 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
exprt & true_case()
Definition: std_expr.h:3455
const natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
The trinary if-then-else operator.
Definition: std_expr.h:3427
typet & type()
Return the type of the expression.
Definition: expr.h:68
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3397
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:269
instructionst::iterator targett
Definition: goto_program.h:414
API to expression classes.
goto_programt::targett get_loop_exit(const loopt &loop)
Definition: loop_utils.cpp:19
instructionst::const_iterator const_targett
Definition: goto_program.h:415
std::set< exprt > modifiest
Definition: loop_utils.h:17
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
Helper functions for k-induction and loop invariants.
exprt & false_case()
Definition: std_expr.h:3465
const source_locationt & source_location() const
Definition: type.h:62
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:89
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
Base class for all expressions.
Definition: expr.h:54
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: loop_utils.cpp:37
Compute natural loops in a goto_function.
static 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:59
A codet representing an assignment in the program.
Definition: std_code.h:256
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
Field-insensitive, location-sensitive may-alias analysis.
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173