cprover
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 assert(!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{
45 if(lhs.id() == ID_symbol || lhs.id() == ID_member || lhs.id() == ID_index)
46 assigns.insert(lhs);
47 else if(lhs.id()==ID_dereference)
48 {
49 const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
50 for(const auto &mod : local_may_alias.get(t, ptr.pointer))
51 {
52 const typecast_exprt typed_mod{mod, ptr.pointer.type()};
53 if(mod.id() == ID_unknown)
54 {
55 throw analysis_exceptiont("Alias analysis returned UNKNOWN!");
56 }
57 if(ptr.offset.is_nil())
58 assigns.insert(dereference_exprt{typed_mod});
59 else
60 assigns.insert(dereference_exprt{plus_exprt{typed_mod, ptr.offset}});
61 }
62 }
63 else if(lhs.id()==ID_if)
64 {
65 const if_exprt &if_expr=to_if_expr(lhs);
66
67 get_assigns_lhs(local_may_alias, t, if_expr.true_case(), assigns);
68 get_assigns_lhs(local_may_alias, t, if_expr.false_case(), assigns);
69 }
70}
71
73 const local_may_aliast &local_may_alias,
74 const loopt &loop,
75 assignst &assigns)
76{
78 i_it=loop.begin(); i_it!=loop.end(); i_it++)
79 {
80 const goto_programt::instructiont &instruction=**i_it;
81
82 if(instruction.is_assign())
83 {
84 const exprt &lhs = instruction.assign_lhs();
85 get_assigns_lhs(local_may_alias, *i_it, lhs, assigns);
86 }
87 else if(instruction.is_function_call())
88 {
89 const exprt &lhs = instruction.call_lhs();
90 get_assigns_lhs(local_may_alias, *i_it, lhs, assigns);
91 }
92 }
93}
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Operator to dereference a pointer.
Definition: pointer_expr.h:648
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:285
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:199
instructionst::iterator targett
Definition: goto_program.h:592
instructionst::const_iterator const_targett
Definition: goto_program.h:593
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
loop_instructionst::const_iterator const_iterator
Definition: loop_analysis.h:46
The plus expression Associativity is not specified.
Definition: std_expr.h:914
Semantic type conversion.
Definition: std_expr.h:1920
std::set< exprt > assignst
Definition: havoc_utils.h:23
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)
Definition: loop_utils.cpp:39
goto_programt::targett get_loop_exit(const loopt &loop)
Definition: loop_utils.cpp:21
void get_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
Definition: loop_utils.cpp:72
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.
Definition: pointer_expr.h:704
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291