38template <
typename index_fn>
46 auto evaluated_index = environment.
eval(index_expr.
index(), ns);
47 auto index_range = (std::dynamic_pointer_cast<const abstract_value_objectt>(
48 evaluated_index->unwrap_context()))
52 for(
const auto &index : index_range)
88 if(expr.
id() == ID_array)
94 map_put(index.value, environment.
eval(entry, ns), index.overrun);
122 std::dynamic_pointer_cast<const full_array_abstract_objectt>(other);
134 return std::make_shared<full_array_abstract_objectt>(*other);
137 std::dynamic_pointer_cast<full_array_abstract_objectt>(
mutable_clone());
143 return shared_from_this();
147 INVARIANT(!result->is_top(),
"Merge of maps will not generate top");
148 INVARIANT(!result->is_bottom(),
"Merge of maps will not generate bottom");
149 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
168 out <<
"[" << entry.first <<
"] = ";
169 entry.second->output(out, ai, ns);
184 auto read_element_fn =
185 [
this, &environment, &ns](
const index_exprt &index_expr) {
191 return (result !=
nullptr) ? result :
get_top_entry(environment, ns);
197 const std::stack<exprt> &stack,
200 bool merging_write)
const
202 auto write_element_fn =
203 [
this, &environment, &ns, &stack, &value, &merging_write](
206 environment, ns, stack, index_expr, value, merging_write);
211 return (result !=
nullptr) ? result :
make_top();
245 const std::stack<exprt> &stack,
248 bool merging_write)
const
253 environment, ns, stack, expr, value, merging_write);
258 environment, ns, stack, expr, value, merging_write);
266 const std::stack<exprt> &stack,
269 bool merging_write)
const
272 std::dynamic_pointer_cast<full_array_abstract_objectt>(
mutable_clone());
274 auto index =
eval_index(expr, environment, ns);
280 auto const existing_value =
map_find_or_top(index.value, environment, ns);
283 environment.
write(existing_value, value, stack, ns, merging_write),
285 result->set_not_top();
286 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
296 starting_value.first,
297 environment.
write(starting_value.second, value, stack, ns,
true));
299 result->set_not_top();
302 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
312 bool merging_write)
const
315 std::dynamic_pointer_cast<full_array_abstract_objectt>(
mutable_clone());
317 auto index =
eval_index(expr, environment, ns);
326 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
330 INVARIANT(!result->map.empty(),
"If not top, map cannot be empty");
332 auto old_value = result->map.find(index.value);
333 if(old_value.has_value())
341 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
346 result->map_put(index.value, value, index.overrun);
347 result->set_not_top();
349 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
357 environment, ns, std::stack<exprt>(), expr, value, merging_write);
365 auto old_value =
map.
find(index_value);
367 if(!old_value.has_value())
372 auto replacement_value =
387 auto value =
map.
find(index_value);
388 if(value.has_value())
389 return value.value();
416 std::dynamic_pointer_cast<full_array_abstract_objectt>(
mutable_clone());
418 bool is_modified =
visit_map(result->map, visitor);
420 return is_modified ? result : shared_from_this();
424 const exprt &name)
const
432 auto field_expr = field.second->to_predicate(index);
434 if(!field_expr.is_true())
435 all_predicates.push_back(field_expr);
438 if(all_predicates.empty())
440 if(all_predicates.size() == 1)
441 return all_predicates.front();
453 if(visited.find(
object.second) == visited.end())
455 object.second->get_statistics(
statistics, visited, env, ns);
467 auto index_abstract_object = env.
eval(index_expr.index(), ns);
468 auto value = index_abstract_object->to_constant();
470 if(!value.is_constant())
487 bool overrun = (index >= max_array_index);
489 return {
true, overrun ? max_array_index : index, overrun};
An abstract version of a program environment.
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Common behaviour for abstract objects modelling values - constants, intervals, etc.
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, const widen_modet &widen_mode)
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
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
const vsd_configt & configuration() const
Exposes the environment configuration.
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.
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.
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual internal_abstract_object_pointert mutable_clone() const
goto_programt::const_targett locationt
abstract_object_pointert make_top() const
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const override
Tries to do an array/array merge if merging with a constant array If it can't, falls back to parent m...
void map_put(mp_integer index, const abstract_object_pointert &value, bool overrun)
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
the current known value about this object.
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 map_find_or_top(mp_integer index, const abstract_environmentt &env, const namespacet &ns) const
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
bool verify() const override
To validate that the struct object is in a valid state.
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.
abstract_object_pointert merge_location_context(const locationt &location) const override
Update the merge location context for an abstract object.
void set_top_internal() override
Perform any additional structural modifications when setting this object to TOP.
abstract_object_pointert full_array_merge(const full_array_pointert &other, const widen_modet &widen_mode) const
Merges an array into this array.
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.
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.
abstract_object_pointert read_element(const abstract_environmentt &env, const exprt &expr, const namespacet &ns) const
abstract_object_pointert write_leaf_element(abstract_environmentt &environment, const namespacet &ns, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const
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
abstract_object_pointert write_location_context(const locationt &location) const override
Update the location context for an abstract object.
void statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
full_array_abstract_objectt(typet type)
sharing_ptrt< full_array_abstract_objectt > const full_array_pointert
Unbounded, signed integers (mathematical integers, not bitvectors)
const irep_idt & id() const
static memory_sizet from_bytes(std::size_t bytes)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
void replace(const key_type &k, valueU &&m)
Replace element, element must exist in map.
bool empty() const
Check if map is empty.
sorted_viewt get_sorted_view() const
Convenience function to get a sorted view of the map elements.
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
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...
The Boolean constant true.
The type of an expression, extends irept.
abstract_object_pointert apply_to_index_range(const abstract_environmentt &environment, const exprt &expr, const namespacet &ns, index_fn &fn)
static eval_index_resultt eval_index(const exprt &expr, const abstract_environmentt &env, const namespacet &ns)
An abstraction of an array value.
bool visit_map(mapt &map, const visitort &visitor)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
abstract_object_pointert object
size_t maximum_array_index
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...