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/pointer_expr.h>
15 #include <util/std_expr.h>
16 
17 #include <analyses/natural_loops.h>
19 
21 {
22  assert(!loop.empty());
23 
24  // find the last instruction in the loop
25  std::map<unsigned, goto_programt::targett> loop_map;
26 
27  for(loopt::const_iterator l_it=loop.begin();
28  l_it!=loop.end();
29  l_it++)
30  loop_map[(*l_it)->location_number]=*l_it;
31 
32  // get the one with the highest number
33  goto_programt::targett last=(--loop_map.end())->second;
34 
35  return ++last;
36 }
37 
39  const goto_programt::targett loop_head,
40  const modifiest &modifies,
41  goto_programt &dest)
42 {
43  for(modifiest::const_iterator
44  m_it=modifies.begin();
45  m_it!=modifies.end();
46  m_it++)
47  {
48  exprt lhs=*m_it;
49  side_effect_expr_nondett rhs(lhs.type(), loop_head->source_location);
50 
52  code_assignt(std::move(lhs), std::move(rhs)),
53  loop_head->source_location));
54  t->code.add_source_location()=loop_head->source_location;
55  }
56 }
57 
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 {
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 }
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2087
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:657
exprt
Base class for all expressions.
Definition: expr.h:54
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::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:995
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2124
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:20
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:183
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:58
pointer_expr.h
API to expression classes for Pointers.
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
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
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2114
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
get_modifies
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:88
natural_loops.h
Compute natural loops in a goto_function.
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:431
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:551
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
build_havoc_code
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: loop_utils.cpp:38
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:432
local_may_aliast::get
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
Definition: local_may_alias.cpp:116
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:234
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:550