cprover
Loading...
Searching...
No Matches
loop_utils.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Helper functions for k-induction and loop invariants
4
5Author: 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 PRECONDITION(!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
40 const local_may_aliast &local_may_alias,
42 const exprt &lhs,
43 assignst &assigns)
44{
46 local_may_alias, t, lhs, assigns, [](const exprt &e) { return true; });
47}
48
50 const local_may_aliast &local_may_alias,
52 const exprt &lhs,
53 assignst &assigns,
54 std::function<bool(const exprt &)> predicate)
55{
56 if(
57 (lhs.id() == ID_symbol || lhs.id() == ID_member || lhs.id() == ID_index) &&
58 predicate(lhs))
59 {
60 assigns.insert(lhs);
61 }
62 else if(lhs.id() == ID_dereference)
63 {
64 const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
65 for(const auto &mod : local_may_alias.get(t, ptr.pointer))
66 {
67 const typecast_exprt typed_mod{mod, ptr.pointer.type()};
68 if(mod.id() == ID_unknown)
69 {
70 continue;
71 }
72 exprt to_insert;
73 if(ptr.offset.is_nil())
74 to_insert = dereference_exprt{typed_mod};
75 else
76 to_insert = dereference_exprt{plus_exprt{typed_mod, ptr.offset}};
77 if(predicate(to_insert))
78 assigns.insert(std::move(to_insert));
79 }
80 }
81 else if(lhs.id() == ID_if)
82 {
83 const if_exprt &if_expr = to_if_expr(lhs);
84
85 get_assigns_lhs(local_may_alias, t, if_expr.true_case(), assigns);
86 get_assigns_lhs(local_may_alias, t, if_expr.false_case(), assigns);
87 }
88}
89
91 const local_may_aliast &local_may_alias,
92 const loopt &loop,
93 assignst &assigns)
94{
96 local_may_alias, loop, assigns, [](const exprt &e) { return true; });
97}
98
100 const local_may_aliast &local_may_alias,
101 const loopt &loop,
102 assignst &assigns,
103 std::function<bool(const exprt &)> predicate)
104{
105 for(loopt::const_iterator i_it = loop.begin(); i_it != loop.end(); i_it++)
106 {
107 const goto_programt::instructiont &instruction = **i_it;
108
109 if(instruction.is_assign())
110 {
111 const exprt &lhs = instruction.assign_lhs();
112 get_assigns_lhs(local_may_alias, *i_it, lhs, assigns, predicate);
113 }
114 else if(instruction.is_function_call())
115 {
116 const exprt &lhs = instruction.call_lhs();
117 get_assigns_lhs(local_may_alias, *i_it, lhs, assigns, predicate);
118 }
119 }
120}
Operator to dereference a pointer.
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
This class represents an instruction in the GOTO intermediate representation.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
instructionst::iterator targett
instructionst::const_iterator const_targett
The trinary if-then-else operator.
Definition std_expr.h:2370
exprt & false_case()
Definition std_expr.h:2407
exprt & true_case()
Definition std_expr.h:2397
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
The plus expression Associativity is not specified.
Definition std_expr.h:1002
Semantic type conversion.
Definition std_expr.h:2068
std::set< exprt > assignst
Definition havoc_utils.h:24
Field-insensitive, location-sensitive may-alias analysis.
void get_assigns_lhs(const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, assignst &assigns)
goto_programt::targett get_loop_exit(const loopt &loop)
void get_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
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.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2450