38 #ifdef DEBUG_SHADOW_MEMORY
39 log.conditional_output(
41 mstream <<
"Shadow memory: set_field: " << id2string(field_name)
42 <<
" for " << format(expr) <<
" to " << format(value)
54 #ifdef DEBUG_SHADOW_MEMORY
55 log.conditional_output(
57 mstream <<
"Shadow memory: get_field: " << id2string(field_name)
58 <<
" for " << format(expr) << messaget::eom;
66 const std::vector<exprt> &value_set)
68 #ifdef DEBUG_SHADOW_MEMORY
69 log.conditional_output(
71 for(const auto &e : value_set)
73 mstream <<
"Shadow memory: value_set: " << format(e) << messaget::eom;
86 #ifdef DEBUG_SHADOW_MEMORY
87 log.conditional_output(
89 mstream <<
"Shadow memory: value_set_match: " << format(address)
90 <<
" <-- " << format(expr) << messaget::eom;
101 #ifdef DEBUG_SHADOW_MEMORY
102 log.conditional_output(
104 mstream <<
"Shadow memory: " << text <<
": " << format(expr)
117 const exprt &matched_base_address,
122 #ifdef DEBUG_SHADOW_MEMORY
123 log.conditional_output(
129 matched_base_address,
131 mstream <<
"Shadow memory: value_set_match: " << messaget::eom;
132 mstream <<
"Shadow memory: base: " << format(shadowed_address.address)
133 <<
" <-- " << format(matched_base_address) << messaget::eom;
134 mstream <<
"Shadow memory: cell: " << format(dereference.pointer)
135 <<
" <-- " << format(expr) << messaget::eom;
136 mstream <<
"Shadow memory: shadow_ptr: "
137 << format(shadow_dereference.pointer) << messaget::eom;
138 mstream <<
"Shadow memory: shadow_val: "
139 << format(shadow_dereference.value) << messaget::eom;
150 #ifdef DEBUG_SHADOW_MEMORY
151 log.conditional_output(
153 mstream <<
"Shadow memory: trying shadowed address: "
154 << format(shadowed_address.address) << messaget::eom;
162 #ifdef DEBUG_SHADOW_MEMORY
173 #ifdef DEBUG_SHADOW_MEMORY
174 log.debug() <<
"Shadow memory: incompatible types "
185 const exprt &null_pointer)
187 #ifdef DEBUG_SHADOW_MEMORY
188 log.conditional_output(
190 mstream <<
"Shadow memory: value set match: " << format(null_pointer)
191 <<
" <-- " << format(expr) << messaget::eom;
192 mstream <<
"Shadow memory: ignoring set field on NULL object"
204 #ifdef DEBUG_SHADOW_MEMORY
205 log.debug() <<
"Shadow memory: incompatible types "
222 return string_expr.
get(ID_value);
264 if(expr.
id() == ID_string_constant)
283 expr.
id() == ID_symbol && expr.
type().
id() == ID_pointer &&
304 return field_type_it->second;
308 return field_type_it->second;
315 return field_init_expr.
type();
319 const std::vector<exprt> &value_set,
320 const exprt &address)
324 for(
const auto &e : value_set)
326 if(e.id() != ID_object_descriptor)
330 if(expr.
id() == ID_null_object)
336 for(
const auto &e : value_set)
338 if(e.id() == ID_unknown || e.id() == ID_object_descriptor)
349 if(value.
type().
id() != ID_floatbv)
369 const typet &field_type,
374 "Cannot combine with *or* elements of a non-bitvector type.");
378 for(
size_t i = 1; i < size; ++i)
397 const typet &field_type,
404 if(element.
type().
id() == ID_unsignedbv || element.
type().
id() == ID_signedbv)
406 exprt value = element;
432 if(values.size() == 1)
441 const typet &field_type,
449 "Can aggregate bytes with *or* only if the shadow memory type is _Bool.");
452 expr.
type().
id() == ID_struct || expr.
type().
id() == ID_union ||
453 expr.
type().
id() == ID_struct_tag || expr.
type().
id() == ID_union_tag)
455 const auto &components =
456 (expr.
type().
id() == ID_struct_tag || expr.
type().
id() == ID_union_tag)
471 else if(expr.
type().
id() == ID_array)
479 for(
mp_integer index = 0; index < size; ++index)
494 <<
"Shadow memory: cannot compute or over variable-size array "
524 const std::vector<exprt>::const_iterator &expr_iterator,
525 const std::vector<exprt>::const_iterator &end)
528 INVARIANT(expr_iterator != end,
"Cannot compute max of an empty collection");
529 const exprt ¤t_expr = *expr_iterator;
533 std::vector<exprt>::const_iterator expr_to_compare_to =
534 std::next(expr_iterator);
535 if(expr_to_compare_to == end)
540 std::vector<exprt> comparisons;
541 for(; expr_to_compare_to != end; ++expr_to_compare_to)
544 comparisons.emplace_back(
548 return {
and_exprt(comparisons), current_expr};
557 const std::vector<std::pair<exprt, exprt>> &conditions_and_values)
561 conditions_and_values.size() > 0,
562 "Cannot compute max of an empty collection");
566 auto reverse_ite = conditions_and_values.rbegin();
571 "Last element of condition-value list must have nil_exprt condition.");
573 exprt res = std::move(reverse_ite->second);
575 for(++reverse_ite; reverse_ite != conditions_and_values.rend(); ++reverse_ite)
577 res =
if_exprt(reverse_ite->first, reverse_ite->second, res);
588 std::vector<std::pair<exprt, exprt>> rows;
589 rows.reserve(values.size());
590 for(
auto byte_it = values.begin(); byte_it != values.end(); ++byte_it)
602 const typet &field_type,
612 std::vector<exprt> extracted_bytes;
613 extracted_bytes.reserve(byte_count);
614 for(std::size_t i = 0; i < byte_count; ++i)
624 max_expr.
type() == field_type,
625 "Aggregated max value type must be the same as shadow memory field's "
632 const std::vector<std::pair<exprt, exprt>> &conds_values)
635 !conds_values.empty(),
"build_if_else_expr requires non-empty argument");
637 for(
const auto &cond_value : conds_values)
641 result = cond_value.second;
645 result =
if_exprt(cond_value.first, cond_value.second, result);
660 if(expr_type.
id() != ID_pointer || shadow_type.
id() != ID_pointer)
669 expr_subtype.
id() == ID_pointer &&
671 shadow_subtype.
id() == ID_array &&
672 to_array_type(shadow_subtype).element_type().
id() != ID_pointer)
677 shadow_subtype.
id() == ID_pointer &&
679 expr_subtype.
id() != ID_pointer)
691 const auto *index_expr = expr_try_dynamic_cast<index_exprt>(expr);
693 index_expr && index_expr->index().is_zero() &&
696 expr = index_expr->array();
706 auto *
pointer_type = type_try_dynamic_cast<pointer_typet>(type);
712 const auto *array_type =
730 const exprt &shadowed_address,
731 const exprt &matched_base_address,
735 typet shadowed_address_type = shadowed_address.
type();
740 matched_base_address, shadowed_address_type);
743 base_cond.
id() == ID_equal &&
748 if(base_cond.
id() == ID_equal)
751 const bool equality_types_match =
754 equality_types_match,
755 "types of expressions on each side of equality should match",
769 const exprt &dereference_pointer,
782 expr_cond.
id() == ID_equal &&
787 if(expr_cond.
id() == ID_equal)
790 const bool equality_types_match =
793 equality_types_match,
794 "types of expressions on each side of equality should match",
819 shadowed_object.
object() = shadow;
822 #ifdef DEBUG_SHADOW_MEMORY
823 log.debug() <<
"Shadow memory: shadow-deref: "
826 return shadow_dereference;
853 const exprt &matched_object,
854 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
855 const typet &field_type,
857 const typet &lhs_type,
860 std::vector<std::pair<exprt, exprt>> result;
862 for(
const auto &shadowed_address : addresses)
872 exprt matched_base_address =
877 if(matched_base_descriptor.
object().
id() == ID_null_object)
889 s <<
"Shadow memory: cannot get shadow memory via type void* for "
891 <<
". Insert a cast to the type that you want to access.";
899 shadowed_address.shadow, matched_base_descriptor, expr, ns,
log);
904 matched_base_address,
909 const bool is_union = matched_base_descriptor.
type().
id() == ID_union ||
910 matched_base_descriptor.
type().
id() == ID_union_tag;
914 if(field_type.
id() == ID_c_bool || field_type.
id() == ID_bool)
919 shadow_dereference.
value, field_type, ns,
log, is_union),
929 shadowed_address.address, matched_base_address, ns,
log);
936 const exprt expr_cond =
945 #ifdef DEBUG_SHADOW_MEMORY
950 result.emplace_back(base_cond, value);
958 #ifdef DEBUG_SHADOW_MEMORY
962 result.emplace_back(expr_cond, value);
967 #ifdef DEBUG_SHADOW_MEMORY
970 result.emplace_back(
and_exprt(base_cond, expr_cond), value);
984 if(expr.
offset().
id() == ID_unknown)
996 if(
object.
id() == ID_index)
1003 object = index_expr.
array();
1005 else if(
object.
id() == ID_member)
1008 const auto &struct_op = member_expr.
struct_op();
1010 struct_op.type().
id() == ID_struct_tag
1022 result.
object() = object;
1030 const std::vector<exprt> &value_set,
1035 "Cannot check if value_set contains only NULL as `expr` type is not a "
1047 static std::vector<std::pair<exprt, exprt>>
1050 const exprt &matched_object,
1051 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
1056 std::vector<std::pair<exprt, exprt>> result;
1057 for(
const auto &shadowed_address : addresses)
1072 matched_base_descriptor, expr, ns);
1074 exprt matched_base_address =
1079 if(matched_base_descriptor.
object().
id() == ID_null_object)
1085 shadowed_address.shadow, matched_base_descriptor, expr, ns,
log);
1090 matched_base_address,
1093 shadow_dereference);
1096 shadowed_address.address, matched_base_address, ns,
log);
1103 const exprt expr_cond =
1116 result.push_back({base_cond, shadow_dereference.
pointer});
1127 result.emplace_back(expr_cond, shadow_dereference.
pointer);
1133 result.emplace_back(
1142 const std::vector<exprt> &value_set,
1143 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
1148 std::vector<std::pair<exprt, exprt>> conds_values;
1149 for(
const auto &matched_object : value_set)
1151 if(matched_object.id() != ID_object_descriptor)
1153 log.warning() <<
"Shadow memory: value set contains unknown for "
1161 log.warning() <<
"Shadow memory: value set contains integer_address for "
1165 if(matched_object.type().get_bool(ID_C_is_failed_symbol))
1167 log.warning() <<
"Shadow memory: value set contains failed symbol for "
1172 bool exact_match =
false;
1174 expr, matched_object, addresses, ns,
log, exact_match);
1176 if(!per_value_set_conds_values.empty())
1180 conds_values.clear();
1182 conds_values.insert(
1183 conds_values.begin(),
1184 per_value_set_conds_values.begin(),
1185 per_value_set_conds_values.end());
1186 mux_size += conds_values.size() - 1;
1193 if(!conds_values.empty())
API to expression classes for bitvectors.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
unsignedbv_typet unsigned_int_type()
unsignedbv_typet unsigned_long_int_type()
pointer_typet pointer_type(const typet &subtype)
bitvector_typet char_type()
bool can_cast_type< c_bool_typet >(const typet &type)
Check whether a reference to a typet is a c_bool_typet.
Operator to return the address of an object.
typet index_type() const
The type of the index expressions into any instance of this type.
const exprt & size() const
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
std::size_t get_width() const
struct configt::ansi_ct ansi_c
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
Central data structure: state.
shadow_memory_statet shadow_memory
The trinary if-then-else operator.
bool get_bool(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
Extract member of struct or union.
const exprt & struct_op() const
irep_idt get_component_name() const
Class that provides messages with a built-in verbosity 'level'.
A base class for multi-ary expressions Associativity is not specified.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
Split an expression into a base object and a (byte) offset.
const typet & base_type() const
The type of the data what we point to.
field_definitiont global_fields
Field definitions for global-scope fields.
field_definitiont local_fields
Field definitions for local-scope fields.
shadow_memory_field_definitionst fields
The available shadow memory field definitions.
Expression providing an SSA-renamed symbol of expressions.
void set_expression(exprt expr)
Replace the underlying, original expression by expr while maintaining SSA indices.
const exprt & get_original_expr() const
Structure type, corresponds to C style structs.
const componentst & components() const
The Boolean constant true.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Fixed-width bit-vector with unsigned binary interpretation.
Return value for build_reference_to; see that method for documentation.
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
#define Forall_operands(it, expr)
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets, message_handlert &message_handler)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
const std::string & id2string(const irep_idt &d)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
bool can_cast_expr< dereference_exprt >(const exprt &base)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
bool can_cast_expr< address_of_exprt >(const exprt &base)
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
exprt build_if_else_expr(const std::vector< std::pair< exprt, exprt >> &conds_values)
Build an if-then-else chain from a vector containing pairs of expressions.
void replace_invalid_object_by_null(exprt &expr)
Replace an invalid object by a null pointer.
static object_descriptor_exprt normalize(const object_descriptor_exprt &expr, const namespacet &ns)
void shadow_memory_log_value_set_match(const namespacet &ns, const messaget &log, const exprt &address, const exprt &expr)
Logs a successful match between an address and a value within the value set.
static void clean_string_constant(exprt &expr)
Simplify &string_constant[0] to &string_constant to facilitate expression equality for exact matching...
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
bool contains_null_or_invalid(const std::vector< exprt > &value_set, const exprt &address)
Given a pointer expression check to see if it can be a null pointer or an invalid object within value...
static exprt or_values(const exprt::operandst &values, const typet &field_type)
Translate a list of values into an or expression.
exprt compute_or_over_bytes(const exprt &expr, const typet &field_type, const namespacet &ns, const messaget &log, const bool is_union)
Performs aggregation of the shadow memory field value over multiple bytes for fields whose type is _B...
static bool are_types_compatible(const typet &expr_type, const typet &shadow_type)
Checks given types (object type and shadow memory field type) for equality.
static std::vector< std::pair< exprt, exprt > > get_shadow_memory_for_matched_object(const exprt &expr, const exprt &matched_object, const std::vector< shadow_memory_statet::shadowed_addresst > &addresses, const namespacet &ns, const messaget &log, bool &exact_match)
Used for set_field and shadow memory copy.
static void extract_bytes_of_expr(exprt element, const typet &field_type, const namespacet &ns, const messaget &log, const bool is_union, exprt::operandst &values)
Extract the components from the input expression value and places them into the array values.
static void adjust_array_types(typet &type)
Flattens type of the form pointer_type(array_type(element_type)) to pointer_type(element_type) and po...
bool check_value_set_contains_only_null_ptr(const namespacet &ns, const messaget &log, const std::vector< exprt > &value_set, const exprt &expr)
Checks if value_set contains only a NULL pointer expression of the same type of expr.
static void log_value_set_match(const namespacet &ns, const messaget &log, const shadow_memory_statet::shadowed_addresst &shadowed_address, const exprt &matched_base_address, const value_set_dereferencet::valuet &dereference, const exprt &expr, const value_set_dereferencet::valuet &shadow_dereference)
Log a match between an address and the value set.
void shadow_memory_log_set_field(const namespacet &ns, const messaget &log, const irep_idt &field_name, const exprt &expr, const exprt &value)
Logs setting a value to a given shadow field.
const typet & get_field_init_type(const irep_idt &field_name, const goto_symex_statet &state)
Retrieves the type of the shadow memory by returning the type of the shadow memory initializer value.
const exprt & get_field_init_expr(const irep_idt &field_name, const goto_symex_statet &state)
Retrieve the expression that a field was initialised with within a given symex state.
std::pair< exprt, exprt > compare_to_collection(const std::vector< exprt >::const_iterator &expr_iterator, const std::vector< exprt >::const_iterator &end)
Create an expression comparing the element at expr_iterator with the following elements of the collec...
void clean_pointer_expr(exprt &expr)
Clean the given pointer expression so that it has the right shape for being used for identifying shad...
std::vector< std::pair< exprt, exprt > > get_shadow_dereference_candidates(const namespacet &ns, const messaget &log, const exprt &matched_object, const std::vector< shadow_memory_statet::shadowed_addresst > &addresses, const typet &field_type, const exprt &expr, const typet &lhs_type, bool &exact_match)
Get a list of (condition, value) pairs for a certain pointer from the shadow memory,...
static exprt get_matched_expr_cond(const exprt &dereference_pointer, const exprt &expr, const namespacet &ns, const messaget &log)
Function that compares the two arguments dereference_pointer and expr, simplifies the comparison expr...
static void log_try_shadow_address(const namespacet &ns, const messaget &log, const shadow_memory_statet::shadowed_addresst &shadowed_address)
Log trying out a match between an object and a (target) shadow address.
static void log_value_set_contains_only_null(const messaget &log, const namespacet &ns, const exprt &expr, const exprt &null_pointer)
static void log_are_types_incompatible(const namespacet &ns, const exprt &expr, const shadow_memory_statet::shadowed_addresst &shadowed_address, const messaget &log)
exprt compute_max_over_bytes(const exprt &expr, const typet &field_type, const namespacet &ns)
Performs aggregation of the shadow memory field value over multiple cells for fields whose type is a ...
static void log_shadow_memory_incompatible_types(const messaget &log, const namespacet &ns, const exprt &expr, const shadow_memory_statet::shadowed_addresst &shadowed_address)
static void log_shadow_memory_message(const messaget &log, const char *text)
Generic logging function to log a text if DEBUG_SHADOW_MEMORY is defined.
void shadow_memory_log_get_field(const namespacet &ns, const messaget &log, const irep_idt &field_name, const exprt &expr)
Logs getting a value corresponding to a shadow memory field.
irep_idt extract_field_name(const exprt &string_expr)
Extracts the field name identifier from a string expression, e.g.
static exprt create_max_expr(const std::vector< exprt > &values)
Create an expression encoding the max operation over the collection values
static void remove_array_type_l2(typet &type)
If the given type is an array type, then remove the L2 level renaming from its size.
void shadow_memory_log_value_set(const namespacet &ns, const messaget &log, const std::vector< exprt > &value_set)
Logs the retrieval of the value associated with a given shadow memory field.
void shadow_memory_log_text_and_expr(const namespacet &ns, const messaget &log, const char *text, const exprt &expr)
Generic logging function that will log depending on the configured verbosity.
static exprt combine_condition_and_max_values(const std::vector< std::pair< exprt, exprt >> &conditions_and_values)
Combine each (condition, value) element in the input collection into a if-then-else expression such a...
static value_set_dereferencet::valuet get_shadow_dereference(const exprt &shadow, const object_descriptor_exprt &matched_base_descriptor, const exprt &expr, const namespacet &ns, const messaget &log)
Retrieve the shadow value a pointer expression may point to.
std::optional< exprt > get_shadow_memory(const exprt &expr, const std::vector< exprt > &value_set, const std::vector< shadow_memory_statet::shadowed_addresst > &addresses, const namespacet &ns, const messaget &log, size_t &mux_size)
Get shadow memory values for a given expression within a specified value set.
static exprt conditional_cast_floatbv_to_unsignedbv(const exprt &value)
Casts a given (float) bitvector expression to an unsigned bitvector.
static void extract_bytes_of_bv(const exprt &value, const typet &type, const typet &field_type, exprt::operandst &values)
Extract byte-sized elements from the input bitvector-typed expression value and places them into the ...
static exprt get_matched_base_cond(const exprt &shadowed_address, const exprt &matched_base_address, const namespacet &ns, const messaget &log)
Function that compares the two arguments shadowed_address and matched_base_address,...
Symex Shadow Memory Instrumentation Utilities.
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
#define POSTCONDITION(CONDITION)
#define UNREACHABLE_BECAUSE(REASON)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
bool can_cast_expr< typecast_exprt >(const exprt &base)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bool can_cast_expr< index_exprt >(const exprt &base)
bool can_cast_expr< symbol_exprt >(const exprt &base)
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
bool can_cast_type< bool_typet >(const typet &base)
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
bool can_cast_expr< string_constantt >(const exprt &base)