cprover
Loading...
Searching...
No Matches
dfcc_infer_loop_assigns.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7\*******************************************************************/
9
10#include <util/expr.h>
11#include <util/find_symbols.h>
12#include <util/message.h>
13#include <util/pointer_expr.h>
14#include <util/std_code.h>
15
17
18#include "dfcc_root_object.h"
19
21static exprt
23{
24 const symbolt &object_whole_sym = ns.lookup(CPROVER_PREFIX "object_whole");
25 const code_typet &object_whole_code_type =
26 to_code_type(object_whole_sym.type);
28 object_whole_sym.symbol_expr(),
29 {{expr}},
30 object_whole_code_type.return_type(),
31 expr.source_location());
32}
33
36static bool
37depends_on(const exprt &expr, std::unordered_set<irep_idt> identifiers)
38{
39 const std::unordered_set<irep_idt> ids = find_symbol_identifiers(expr);
40 for(const auto &id : ids)
41 {
42 if(identifiers.find(id) != identifiers.end())
43 return true;
44 }
45 return false;
46}
47
49 const local_may_aliast &local_may_alias,
50 const loopt &loop_instructions,
51 const source_locationt &loop_head_location,
52 const namespacet &ns)
53{
54 // infer
55 assignst assigns;
56 get_assigns(local_may_alias, loop_instructions, assigns);
57
58 // compute locals
59 std::unordered_set<irep_idt> loop_locals;
60 for(const auto &target : loop_instructions)
61 {
62 if(target->is_decl())
63 loop_locals.insert(target->decl_symbol().get_identifier());
64 }
65
66 // widen or drop targets that depend on loop-locals or are non-constant,
67 // ie. depend on other locations assigned by the loop.
68 // e.g: if the loop assigns {i, a[i]}, then a[i] is non-constant.
70 assignst result;
71 for(const auto &expr : assigns)
72 {
73 if(depends_on(expr, loop_locals))
74 {
75 // Target depends on loop locals, attempt widening to the root object
76 auto root_objects = dfcc_root_objects(expr);
77 for(const auto &root_object : root_objects)
78 {
79 if(!depends_on(root_object, loop_locals))
80 {
81 address_of_exprt address_of_root_object(root_object);
82 address_of_root_object.add_source_location() =
83 root_object.source_location();
84 result.emplace(
85 make_object_whole_call_expr(address_of_root_object, ns));
86 }
87 }
88 }
89 else
90 {
91 address_of_exprt address_of_expr(expr);
92 address_of_expr.add_source_location() = expr.source_location();
93 if(!is_constant(address_of_expr))
94 {
95 // Target address is not constant, widening to the whole object
96 result.emplace(make_object_whole_call_expr(address_of_expr, ns));
97 }
98 else
99 {
100 result.emplace(expr);
101 }
102 }
103 }
104
105 return result;
106}
Operator to return the address of an object.
Base type of functions.
Definition std_types.h:539
Base class for all expressions.
Definition expr.h:56
const source_locationt & source_location() const
Definition expr.h:223
source_locationt & add_source_location()
Definition expr.h:228
A class containing utility functions for havocing expressions.
Definition havoc_utils.h:28
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
Symbol table entry.
Definition symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
#define CPROVER_PREFIX
static const exprt::operandst & get_assigns(const goto_programt::const_targett &latch_target)
Extracts the assigns clause expression from the latch condition.
assignst dfcc_infer_loop_assigns(const local_may_aliast &local_may_alias, const loopt &loop_instructions, const source_locationt &loop_head_location, const namespacet &ns)
static exprt make_object_whole_call_expr(const exprt &expr, const namespacet &ns)
Builds a call expression object_whole(expr)
static bool depends_on(const exprt &expr, std::unordered_set< irep_idt > identifiers)
Returns true iff expr contains at least one identifier found in identifiers.
Infer a set of assigns clause targets for a natural loop.
std::unordered_set< exprt, irep_hash > dfcc_root_objects(const exprt &expr)
Computes a set of root object expressions from an lvalue or assigns clause target expression.
Utility functions that compute root object expressions for assigns clause targets and LHS expressions...
find_symbols_sett find_symbol_identifiers(const exprt &src)
Find identifiers of the sub expressions with id ID_symbol, considering both free and bound variables.
Utilities for building havoc code for expressions.
std::set< exprt > assignst
Definition havoc_utils.h:24
natural_loops_mutablet::natural_loopt loopt
Definition loop_utils.h:20
API to expression classes for Pointers.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition std_types.h:29