Go to the documentation of this file.
23 template <
typename index_fn>
31 auto evaluated_index = environment.
eval(index_expr.
index(), ns);
32 auto index_range = (std::dynamic_pointer_cast<const abstract_value_objectt>(
33 evaluated_index->unwrap_context()))
36 if(!index_range->advance_to_next())
44 result = (result ==
nullptr) ? at_index
46 }
while(!result->
is_top() && index_range->advance_to_next());
71 if(expr.
id() == ID_array)
103 std::dynamic_pointer_cast<const full_array_abstract_objectt>(other);
120 return std::make_shared<full_array_abstract_objectt>(*other);
125 std::dynamic_pointer_cast<full_array_abstract_objectt>(
mutable_clone());
131 return shared_from_this();
135 INVARIANT(!result->is_top(),
"Merge of maps will not generate top");
136 INVARIANT(!result->is_bottom(),
"Merge of maps will not generate bottom");
137 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
157 out <<
"[" << entry.first <<
"] = ";
158 entry.second->output(out, ai, ns);
173 auto read_element_fn =
174 [
this, &environment, &ns](
const index_exprt &index_expr) {
180 return (result !=
nullptr) ? result :
get_top_entry(environment, ns);
186 const std::stack<exprt> &stack,
189 bool merging_write)
const
191 auto write_element_fn =
192 [
this, &environment, &ns, &stack, &value, &merging_write](
195 environment, ns, stack, index_expr, value, merging_write);
200 return (result !=
nullptr) ? result :
make_top();
213 auto const value =
map.
find(index_value);
214 if(value.has_value())
215 return value.value();
240 const std::stack<exprt> &stack,
243 bool merging_write)
const
248 environment, ns, stack, expr, value, merging_write);
253 environment, ns, stack, expr, value, merging_write);
261 const std::stack<exprt> &stack,
264 bool merging_write)
const
267 std::dynamic_pointer_cast<full_array_abstract_objectt>(
mutable_clone());
270 bool good_index =
eval_index(expr, environment, ns, index_value);
276 auto const old_value =
map.
find(index_value);
278 if(old_value.has_value())
282 environment.
write(old_value.value(), value, stack, ns, merging_write));
289 get_top_entry(environment, ns), value, stack, ns, merging_write));
292 result->set_not_top();
293 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
303 starting_value.first,
304 environment.
write(starting_value.second, value, stack, ns,
true));
306 result->set_not_top();
309 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
319 bool merging_write)
const
322 std::dynamic_pointer_cast<full_array_abstract_objectt>(
mutable_clone());
325 bool good_index =
eval_index(expr, environment, ns, index_value);
334 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
338 INVARIANT(!result->map.empty(),
"If not top, map cannot be empty");
340 auto old_value = result->map.find(index_value);
341 if(old_value.has_value())
347 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
352 auto old_value = result->map.find(index_value);
354 if(old_value.has_value())
355 result->map.replace(index_value, value);
357 result->map.insert(index_value, value);
359 result->set_not_top();
360 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
368 environment, ns, std::stack<exprt>(), expr, value, merging_write);
382 std::dynamic_pointer_cast<full_array_abstract_objectt>(
mutable_clone());
384 bool modified =
false;
385 for(
auto &item : result->map.get_view())
387 auto newval = visitor.
visit(item.second);
388 if(newval != item.second)
390 result->map.replace(item.first, std::move(newval));
401 return shared_from_this();
413 if(visited.find(
object.second) == visited.end())
415 object.second->get_statistics(
statistics, visited, env, ns);
429 exprt value = index_abstract_object->to_constant();
435 bool result =
to_integer(constant_index, out_index);
abstract_object_pointert write_sub_element(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual bool is_top() const
Find out if the abstract object is top.
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
sharing_ptrt< full_array_abstract_objectt > const full_array_pointert
abstract_object_pointert full_array_merge(const full_array_pointert other) const
Merges an array into this array.
virtual abstract_object_pointert write(const abstract_object_pointert &lhs, const abstract_object_pointert &rhs, std::stack< exprt > remaining_stack, const namespacet &ns, bool merge_write)
Used within assign to do the actual dispatch.
abstract_object_pointert apply_to_index_range(const abstract_environmentt &environment, const exprt &expr, const namespacet &ns, index_fn &fn)
The type of an expression, extends irept.
void get_view(V &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
abstract_object_pointert write_leaf_element(abstract_environmentt &environment, const namespacet &ns, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const
sorted_viewt get_sorted_view() const
Convenience function to get a sorted view of the map elements.
abstract_object_pointert read_element(const abstract_environmentt &env, const exprt &expr, const namespacet &ns) const
Base class for all expressions.
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
abstract_object_pointert write_component(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a index of an array.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
the current known value about this object.
abstract_object_pointert write_element(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
abstract_object_pointert visit_sub_elements(const abstract_object_visitort &visitor) const override
Apply a visitor operation to all sub elements of this abstract_object.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
static bool merge_shared_maps(const sharing_mapt< keyt, abstract_object_pointert, false, hash > &map1, const sharing_mapt< keyt, abstract_object_pointert, false, hash > &map2, sharing_mapt< keyt, abstract_object_pointert, false, hash > &out_map)
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
#define PRECONDITION(CONDITION)
bool eval_index(const exprt &index, const abstract_environmentt &env, const namespacet &ns, mp_integer &out_index)
An abstract version of a program environment.
bool empty() const
Check if map is empty.
abstract_object_pointert make_top() const
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
const irep_idt & id() const
full_array_abstract_objectt(typet type)
std::set< abstract_object_pointert > abstract_object_visitedt
An abstraction of an array value.
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
virtual abstract_object_pointert write_component(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const
bool is_constant() const
Return whether the expression is a constant.
This is the basic interface of the abstract interpreter with default implementations of the core func...
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
void statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
A constant literal expression.
abstract_object_pointert get_top_entry(const abstract_environmentt &env, const namespacet &ns) const
Short hand method for creating a top element of the array.
abstract_object_pointert merge(abstract_object_pointert other) const override
Tries to do an array/array merge if merging with a constant array If it can't, falls back to parent m...
API to expression classes.
virtual abstract_object_pointert visit(const abstract_object_pointert element) const =0
static memory_sizet from_bytes(std::size_t bytes)
bool verify() const override
To validate that the struct object is in a valid state.
virtual internal_abstract_object_pointert mutable_clone() const
CLONE abstract_object_pointert read_component(const abstract_environmentt &env, const exprt &expr, const namespacet &ns) const override
A helper function to read elements from an array.
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
void set_top_internal() override
Perform any additional structural modifications when setting this object to TOP.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.