cprover
Loading...
Searching...
No Matches
type_size_mapping.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#include "type_size_mapping.h"
4
5#include <util/arith_tools.h>
6#include <util/c_types.h>
7#include <util/invariant.h>
8#include <util/pointer_expr.h>
10
12
14 const exprt &expression,
15 const namespacet &ns,
16 type_size_mapt &type_size_map,
17 const smt_object_mapt &object_map,
19 const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object)
20{
21 expression.visit_pre([&](const exprt &sub_expression) {
22 if(
23 const auto &pointer_type =
25 {
26 const auto find_result = type_size_map.find(pointer_type->base_type());
27 if(find_result != type_size_map.cend())
28 return;
29 exprt pointer_size_expr;
30 // There's a special case for a pointer subtype here: the case where the
31 // pointer is `void *`. This means that we don't know the underlying base
32 // type, so we're just assigning a size expression value of 1 (given that
33 // this is going to be used in a multiplication and 1 is the identity
34 // value for multiplication)
36 {
37 pointer_size_expr = from_integer(1, size_type());
38 }
39 else
40 {
41 auto pointer_size_opt = size_of_expr(pointer_type->base_type(), ns);
42 PRECONDITION(pointer_size_opt.has_value());
43 pointer_size_expr = pointer_size_opt.value();
44 }
45 auto pointer_size_term = convert_expr_to_smt(
46 pointer_size_expr,
47 object_map,
48 type_size_map,
50 is_dynamic_object);
51 type_size_map.emplace_hint(
52 find_result, pointer_type->base_type(), pointer_size_term);
53 }
54 });
55}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
unsignedbv_typet size_type()
Definition c_types.cpp:50
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
Base class for all expressions.
Definition expr.h:56
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:227
typet & type()
Return the type of the expression.
Definition expr.h:84
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
Definition expr_cast.h:135
std::unordered_map< exprt, decision_procedure_objectt, irep_hash > smt_object_mapt
Mapping from an object's base expression to the set of information about it which we track.
API to expression classes for Pointers.
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt object_size(const exprt &pointer)
#define PRECONDITION(CONDITION)
Definition invariant.h:463
smt_function_application_termt::factoryt< smt_command_functiont > make_applicationt
Function which makes applications of the smt function.
smt_function_application_termt::factoryt< smt_command_functiont > make_applicationt
Function which makes applications of the smt function.
void associate_pointer_sizes(const exprt &expression, const namespacet &ns, type_size_mapt &type_size_map, const smt_object_mapt &object_map, const smt_object_sizet::make_applicationt &object_size, const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object)
This function populates the (pointer) type -> size map.
Utilities for making a map of types to associated sizes.
std::unordered_map< typet, smt_termt, irep_hash > type_size_mapt