CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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{
57
58 if(lhs.id() == ID_symbol || lhs.id() == ID_index)
59 {
60 // All variables `v` and their indexing expressions `v[idx]` are assigns.
61 new_assigns.insert(lhs);
62 }
63 else if(lhs.id() == ID_member)
64 {
65 auto op = to_member_expr(lhs).struct_op();
66 auto component_name = to_member_expr(lhs).get_component_name();
67
68 // Insert expressions of form `v.member`.
69 if(op.id() == ID_symbol)
70 {
71 new_assigns.insert(lhs);
72 }
73 // For expressions of form `v->member`, insert all targets `u->member`,
74 // where `u` and `v` alias.
75 else if(op.id() == ID_dereference)
76 {
77 const pointer_arithmetict ptr(to_dereference_expr(op).pointer());
78 for(const auto &mod : local_may_alias.get(t, ptr.pointer))
79 {
80 if(mod.id() == ID_unknown)
81 {
82 continue;
83 }
84 const exprt typed_mod =
87 if(ptr.offset.is_nil())
88 {
89 // u->member
91 dereference_exprt{typed_mod}, component_name, lhs.type());
92 }
93 else
94 {
95 // (u+offset)->member
98 component_name,
99 lhs.type());
100 }
101 new_assigns.insert(to_insert);
102 }
103 }
104 }
105 else if(lhs.id() == ID_dereference)
106 {
107 // All dereference `*v` and their alias `*u` are assigns.
108 const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
109 for(const auto &mod : local_may_alias.get(t, ptr.pointer))
110 {
111 if(mod.id() == ID_unknown)
112 {
113 continue;
114 }
115 const exprt typed_mod =
118 if(ptr.offset.is_nil())
120 else
122 new_assigns.insert(std::move(to_insert));
123 }
124 }
125 else if(lhs.id() == ID_if)
126 {
127 const if_exprt &if_expr = to_if_expr(lhs);
128
130 local_may_alias, t, if_expr.true_case(), assigns, predicate);
132 local_may_alias, t, if_expr.false_case(), assigns, predicate);
133 }
134
135 std::copy_if(
136 new_assigns.begin(),
137 new_assigns.end(),
138 std::inserter(assigns, assigns.begin()),
139 predicate);
140}
141
143 const local_may_aliast &local_may_alias,
144 const loopt &loop,
145 assignst &assigns)
146{
148 local_may_alias, loop, assigns, [](const exprt &e) { return true; });
149}
150
152 const local_may_aliast &local_may_alias,
153 const loopt &loop,
154 assignst &assigns,
155 std::function<bool(const exprt &)> predicate)
156{
157 for(loopt::const_iterator i_it = loop.begin(); i_it != loop.end(); i_it++)
158 {
159 const goto_programt::instructiont &instruction = **i_it;
160
161 if(instruction.is_assign())
162 {
163 const exprt &lhs = instruction.assign_lhs();
164 get_assigns_lhs(local_may_alias, *i_it, lhs, assigns, predicate);
165 }
166 else if(instruction.is_function_call())
167 {
168 const exprt &lhs = instruction.call_lhs();
169 get_assigns_lhs(local_may_alias, *i_it, lhs, assigns, predicate);
170 }
171 }
172}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:2497
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
Extract member of struct or union.
Definition std_expr.h:2971
The plus expression Associativity is not specified.
Definition std_expr.h:1002
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
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:2577
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063