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  side_effect_expr_nondett rhs(lhs.type(), loop_head->source_location);
49 
51  code_assignt(std::move(lhs), std::move(rhs)),
52  loop_head->source_location));
53  t->code.add_source_location()=loop_head->source_location;
54  }
55 }
56 
58  const local_may_aliast &local_may_alias,
60  const exprt &lhs,
61  modifiest &modifies)
62 {
63  if(lhs.id()==ID_symbol)
64  modifies.insert(lhs);
65  else if(lhs.id()==ID_dereference)
66  {
67  modifiest m=local_may_alias.get(t, to_dereference_expr(lhs).pointer());
68  for(modifiest::const_iterator m_it=m.begin();
69  m_it!=m.end(); m_it++)
70  get_modifies_lhs(local_may_alias, t, *m_it, modifies);
71  }
72  else if(lhs.id()==ID_member)
73  {
74  }
75  else if(lhs.id()==ID_index)
76  {
77  }
78  else if(lhs.id()==ID_if)
79  {
80  const if_exprt &if_expr=to_if_expr(lhs);
81 
82  get_modifies_lhs(local_may_alias, t, if_expr.true_case(), modifies);
83  get_modifies_lhs(local_may_alias, t, if_expr.false_case(), modifies);
84  }
85 }
86 
88  const local_may_aliast &local_may_alias,
89  const loopt &loop,
90  modifiest &modifies)
91 {
93  i_it=loop.begin(); i_it!=loop.end(); i_it++)
94  {
95  const goto_programt::instructiont &instruction=**i_it;
96 
97  if(instruction.is_assign())
98  {
99  const exprt &lhs=to_code_assign(instruction.code).lhs();
100  get_modifies_lhs(local_may_alias, *i_it, lhs, modifies);
101  }
102  else if(instruction.is_function_call())
103  {
104  const exprt &lhs=to_code_function_call(instruction.code).lhs();
105  get_modifies_lhs(local_may_alias, *i_it, lhs, modifies);
106  }
107  }
108 }
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
exprt
Base class for all expressions.
Definition: expr.h:53
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
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:1024
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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:19
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
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:57
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
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:1945
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
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:87
natural_loops.h
Compute natural loops in a goto_function.
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:460
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
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:37
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:461
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:179
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579