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;
49 
51  t->function=loop_head->function;
52  t->source_location=loop_head->source_location;
53  t->code=code_assignt(lhs, rhs);
54  t->code.add_source_location()=loop_head->source_location;
55  }
56 }
57 
58 static void get_modifies_lhs(
59  const local_may_aliast &local_may_alias,
61  const exprt &lhs,
62  modifiest &modifies)
63 {
64  if(lhs.id()==ID_symbol)
65  modifies.insert(lhs);
66  else if(lhs.id()==ID_dereference)
67  {
68  modifiest m=local_may_alias.get(t, to_dereference_expr(lhs).pointer());
69  for(modifiest::const_iterator m_it=m.begin();
70  m_it!=m.end(); m_it++)
71  get_modifies_lhs(local_may_alias, t, *m_it, modifies);
72  }
73  else if(lhs.id()==ID_member)
74  {
75  }
76  else if(lhs.id()==ID_index)
77  {
78  }
79  else if(lhs.id()==ID_if)
80  {
81  const if_exprt &if_expr=to_if_expr(lhs);
82 
83  get_modifies_lhs(local_may_alias, t, if_expr.true_case(), modifies);
84  get_modifies_lhs(local_may_alias, t, if_expr.false_case(), modifies);
85  }
86 }
87 
89  const local_may_aliast &local_may_alias,
90  const loopt &loop,
91  modifiest &modifies)
92 {
93  for(loopt::const_iterator
94  i_it=loop.begin(); i_it!=loop.end(); i_it++)
95  {
96  const goto_programt::instructiont &instruction=**i_it;
97 
98  if(instruction.is_assign())
99  {
100  const exprt &lhs=to_code_assign(instruction.code).lhs();
101  get_modifies_lhs(local_may_alias, *i_it, lhs, modifies);
102  }
103  else if(instruction.is_function_call())
104  {
105  const exprt &lhs=to_code_function_call(instruction.code).lhs();
106  get_modifies_lhs(local_may_alias, *i_it, lhs, modifies);
107  }
108  }
109 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
exprt & true_case()
Definition: std_expr.h:3395
const natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
The trinary if-then-else operator.
Definition: std_expr.h:3361
typet & type()
Definition: expr.h:56
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3328
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
instructionst::iterator targett
Definition: goto_program.h:397
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:398
std::set< exprt > modifiest
Definition: loop_utils.h:17
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
Helper functions for k-induction and loop invariants.
exprt & false_case()
Definition: std_expr.h:3405
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:88
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
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:58
Assignment.
Definition: std_code.h:195
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:879