Skip to content

do not access typet::subtype() without cast #3087

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Oct 7, 2018
Merged

do not access typet::subtype() without cast #3087

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions src/analyses/goto_rw.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -616,8 +616,9 @@ void rw_range_sett::get_objects_rec(const typet &type)
// TODO should recurse into various composite types
if(type.id()==ID_array)
{
get_objects_rec(type.subtype());
get_objects_rec(get_modet::READ, to_array_type(type).size());
const auto &array_type = to_array_type(type);
get_objects_rec(array_type.subtype());
get_objects_rec(get_modet::READ, array_type.size());
}
}

Expand Down
4 changes: 3 additions & 1 deletion src/goto-instrument/thread_instrumentation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,5 +140,7 @@ void mutex_init_instrumentation(goto_modelt &goto_model)

Forall_goto_functions(f_it, goto_model.goto_functions)
mutex_init_instrumentation(
goto_model.symbol_table, f_it->second.body, lock_type.subtype());
goto_model.symbol_table,
f_it->second.body,
to_pointer_type(lock_type).subtype());
}
4 changes: 2 additions & 2 deletions src/goto-symex/auto_objects.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ void goto_symext::initialize_auto_object(
else if(type.id()==ID_pointer)
{
const pointer_typet &pointer_type=to_pointer_type(type);
const typet &subtype=ns.follow(type.subtype());
const typet &subtype = ns.follow(pointer_type.subtype());

// we don't like function pointers and
// we don't like void *
Expand All @@ -67,7 +67,7 @@ void goto_symext::initialize_auto_object(
// could be NULL nondeterministically

address_of_exprt address_of_expr(
make_auto_object(type.subtype(), state), pointer_type);
make_auto_object(pointer_type.subtype(), state), pointer_type);

if_exprt rhs(
side_effect_expr_nondett(bool_typet(), expr.source_location()),
Expand Down
20 changes: 11 additions & 9 deletions src/goto-symex/goto_symex_state.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -211,7 +211,7 @@ static bool check_renaming(const typet &type)
return true;
}
else if(type.has_subtype())
return check_renaming(type.subtype());
return check_renaming(to_type_with_subtype(type).subtype());

return false;
}
Expand Down Expand Up @@ -489,7 +489,7 @@ void goto_symex_statet::rename(
{
auto &address_of_expr = to_address_of_expr(expr);
rename_address(address_of_expr.object(), ns, level);
expr.type().subtype() = address_of_expr.object().type();
to_pointer_type(expr.type()).subtype() = address_of_expr.object().type();
}
else
{
Expand Down Expand Up @@ -725,7 +725,7 @@ void goto_symex_statet::rename_address(

rename_address(index_expr.array(), ns, level);
PRECONDITION(index_expr.array().type().id() == ID_array);
expr.type()=index_expr.array().type().subtype();
expr.type() = to_array_type(index_expr.array().type()).subtype();

// the index is not an address
rename(index_expr.index(), ns, level);
Expand Down Expand Up @@ -810,8 +810,9 @@ void goto_symex_statet::rename(

if(type.id()==ID_array)
{
rename(type.subtype(), irep_idt(), ns, level);
rename(to_array_type(type).size(), ns, level);
auto &array_type = to_array_type(type);
rename(array_type.subtype(), irep_idt(), ns, level);
rename(array_type.size(), ns, level);
}
else if(type.id()==ID_struct ||
type.id()==ID_union ||
Expand All @@ -832,7 +833,7 @@ void goto_symex_statet::rename(
}
else if(type.id()==ID_pointer)
{
rename(type.subtype(), irep_idt(), ns, level);
rename(to_pointer_type(type).subtype(), irep_idt(), ns, level);
}
else if(type.id() == ID_symbol_type)
{
Expand Down Expand Up @@ -876,8 +877,9 @@ void goto_symex_statet::get_original_name(typet &type) const

if(type.id()==ID_array)
{
get_original_name(type.subtype());
get_original_name(to_array_type(type).size());
auto &array_type = to_array_type(type);
get_original_name(array_type.subtype());
get_original_name(array_type.size());
}
else if(type.id()==ID_struct ||
type.id()==ID_union ||
Expand All @@ -894,7 +896,7 @@ void goto_symex_statet::get_original_name(typet &type) const
}
else if(type.id()==ID_pointer)
{
get_original_name(type.subtype());
get_original_name(to_pointer_type(type).subtype());
}
}

Expand Down
21 changes: 12 additions & 9 deletions src/goto-symex/symex_builtin_functions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,9 +60,11 @@ void goto_symext::symex_allocate(
const irep_idt &mode = function_symbol->mode;

// is the type given?
if(code.type().id()==ID_pointer && code.type().subtype().id()!=ID_empty)
if(
code.type().id() == ID_pointer &&
to_pointer_type(code.type()).subtype().id() != ID_empty)
{
object_type=code.type().subtype();
object_type = to_pointer_type(code.type()).subtype();
}
else
{
Expand Down Expand Up @@ -190,11 +192,11 @@ void goto_symext::symex_allocate(

if(object_type.id()==ID_array)
{
index_exprt index_expr(value_symbol.type.subtype());
const auto &array_type = to_array_type(object_type);
index_exprt index_expr(array_type.subtype());
index_expr.array()=value_symbol.symbol_expr();
index_expr.index()=from_integer(0, index_type());
rhs=address_of_exprt(
index_expr, pointer_type(value_symbol.type.subtype()));
rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype()));
}
else
{
Expand Down Expand Up @@ -391,6 +393,8 @@ void goto_symext::symex_cpp_new(

PRECONDITION(code.type().id() == ID_pointer);

const auto &pointer_type = to_pointer_type(code.type());

do_array =
(code.get(ID_statement) == ID_cpp_new_array ||
code.get(ID_statement) == ID_java_new_array_data);
Expand Down Expand Up @@ -418,19 +422,18 @@ void goto_symext::symex_cpp_new(
{
exprt size_arg = static_cast<const exprt &>(code.find(ID_size));
clean_expr(size_arg, state, false);
symbol.type = array_typet(code.type().subtype(), size_arg);
symbol.type = array_typet(pointer_type.subtype(), size_arg);
}
else
symbol.type=code.type().subtype();
symbol.type = pointer_type.subtype();

symbol.type.set(ID_C_dynamic, true);

state.symbol_table.add(symbol);

// make symbol expression

exprt rhs(ID_address_of, code.type());
rhs.type().subtype()=code.type().subtype();
exprt rhs(ID_address_of, pointer_type);

if(do_array)
{
Expand Down
7 changes: 5 additions & 2 deletions src/goto-symex/symex_dereference.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -321,8 +321,11 @@ void goto_symext::dereference_rec(
exprt &object=address_of_expr.object();

const typet &expr_type=ns.follow(expr.type());
expr=address_arithmetic(object, state, guard,
expr_type.subtype().id()==ID_array);
expr = address_arithmetic(
object,
state,
guard,
to_pointer_type(expr_type).subtype().id() == ID_array);
}
else if(expr.id()==ID_typecast)
{
Expand Down
2 changes: 1 addition & 1 deletion src/util/arith_tools.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
}
else if(type_id==ID_c_bit_field)
{
const typet &subtype=type.subtype();
const typet &subtype = to_c_bit_field_type(type).subtype();
if(subtype.id()==ID_signedbv)
{
int_value=binary2integer(id2string(value), true);
Expand Down
3 changes: 2 additions & 1 deletion src/util/expr_initializer.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,8 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
result = side_effect_expr_nondett(type, source_location);
else
{
exprt sub_zero = expr_initializer_rec(type.subtype(), source_location);
exprt sub_zero =
expr_initializer_rec(to_complex_type(type).subtype(), source_location);
result = complex_exprt(sub_zero, sub_zero, to_complex_type(type));
}

Expand Down
2 changes: 1 addition & 1 deletion src/util/find_symbols.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
src.id()!=ID_pointer)
{
if(src.has_subtype())
find_symbols(kind, src.subtype(), dest);
find_symbols(kind, to_type_with_subtype(src).subtype(), dest);

forall_subtypes(it, src)
find_symbols(kind, *it, dest);
Expand Down
6 changes: 3 additions & 3 deletions src/util/format_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,14 +60,14 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
const auto &id = type.id();

if(id == ID_pointer)
return os << '*' << format(type.subtype());
return os << '*' << format(to_pointer_type(type).subtype());
else if(id == ID_array)
{
const auto &t = to_array_type(type);
if(t.is_complete())
return os << format(type.subtype()) << '[' << format(t.size()) << ']';
return os << format(t.subtype()) << '[' << format(t.size()) << ']';
else
return os << format(type.subtype()) << "[]";
return os << format(t.subtype()) << "[]";
}
else if(id == ID_struct)
return format_rec(os, to_struct_type(type));
Expand Down
19 changes: 11 additions & 8 deletions src/util/json_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -154,7 +154,10 @@ json_objectt json(
else if(type.id()==ID_c_enum_tag)
{
// we return the base type
return json(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns, mode);
return json(
to_c_enum_type(ns.follow_tag(to_c_enum_tag_type(type))).subtype(),
ns,
mode);
}
else if(type.id()==ID_fixedbv)
{
Expand All @@ -165,7 +168,7 @@ json_objectt json(
else if(type.id()==ID_pointer)
{
result["name"]=json_stringt("pointer");
result["subtype"]=json(type.subtype(), ns, mode);
result["subtype"] = json(to_pointer_type(type).subtype(), ns, mode);
}
else if(type.id()==ID_bool)
{
Expand All @@ -174,12 +177,12 @@ json_objectt json(
else if(type.id()==ID_array)
{
result["name"]=json_stringt("array");
result["subtype"]=json(type.subtype(), ns, mode);
result["subtype"] = json(to_array_type(type).subtype(), ns, mode);
}
else if(type.id()==ID_vector)
{
result["name"]=json_stringt("vector");
result["subtype"]=json(type.subtype(), ns, mode);
result["subtype"] = json(to_vector_type(type).subtype(), ns, mode);
result["size"]=json(to_vector_type(type).size(), ns, mode);
}
else if(type.id()==ID_struct)
Expand Down Expand Up @@ -242,9 +245,8 @@ json_objectt json(
lang=std::unique_ptr<languaget>(get_default_language());
}

const typet &underlying_type=
type.id()==ID_c_bit_field?type.subtype():
type;
const typet &underlying_type =
type.id() == ID_c_bit_field ? to_c_bit_field_type(type).subtype() : type;

std::string type_string;
bool error=lang->from_type(underlying_type, type_string, ns);
Expand All @@ -270,7 +272,8 @@ json_objectt json(
{
result["name"]=json_stringt("integer");
result["binary"] = json_stringt(constant_expr.get_value());
result["width"]=json_numbert(type.subtype().get_string(ID_width));
result["width"] =
json_numbert(to_c_enum_type(type).subtype().get_string(ID_width));
result["type"]=json_stringt("enum");
result["data"]=json_stringt(value_string);
}
Expand Down
28 changes: 16 additions & 12 deletions src/util/pointer_offset_size.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
{
if(type.id()==ID_array)
{
auto sub = pointer_offset_bits(type.subtype(), ns);
auto sub = pointer_offset_bits(to_array_type(type).subtype(), ns);
if(!sub.has_value())
return {};

Expand All @@ -137,7 +137,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
}
else if(type.id()==ID_vector)
{
auto sub = pointer_offset_bits(type.subtype(), ns);
auto sub = pointer_offset_bits(to_vector_type(type).subtype(), ns);
if(!sub.has_value())
return {};

Expand All @@ -154,7 +154,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
}
else if(type.id()==ID_complex)
{
auto sub = pointer_offset_bits(type.subtype(), ns);
auto sub = pointer_offset_bits(to_complex_type(type).subtype(), ns);

if(sub.has_value())
return (*sub) * 2;
Expand Down Expand Up @@ -212,7 +212,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
}
else if(type.id()==ID_c_enum)
{
return mp_integer(to_bitvector_type(type.subtype()).get_width());
return mp_integer(to_bitvector_type(to_c_enum_type(type).subtype()).get_width());
}
else if(type.id()==ID_c_enum_tag)
{
Expand Down Expand Up @@ -313,12 +313,14 @@ exprt size_of_expr(
{
if(type.id()==ID_array)
{
exprt sub=size_of_expr(type.subtype(), ns);
const auto &array_type = to_array_type(type);

exprt sub = size_of_expr(array_type.subtype(), ns);
if(sub.is_nil())
return nil_exprt();

// get size
exprt size=to_array_type(type).size();
exprt size = array_type.size();

if(size.is_nil())
return nil_exprt();
Expand All @@ -333,7 +335,7 @@ exprt size_of_expr(
}
else if(type.id()==ID_vector)
{
exprt sub=size_of_expr(type.subtype(), ns);
exprt sub = size_of_expr(to_vector_type(type).subtype(), ns);
if(sub.is_nil())
return nil_exprt();

Expand All @@ -353,7 +355,7 @@ exprt size_of_expr(
}
else if(type.id()==ID_complex)
{
exprt sub=size_of_expr(type.subtype(), ns);
exprt sub = size_of_expr(to_complex_type(type).subtype(), ns);
if(sub.is_nil())
return nil_exprt();

Expand Down Expand Up @@ -465,7 +467,8 @@ exprt size_of_expr(
}
else if(type.id()==ID_c_enum)
{
std::size_t width=to_bitvector_type(type.subtype()).get_width();
std::size_t width =
to_bitvector_type(to_c_enum_type(type).subtype()).get_width();
std::size_t bytes=width/8;
if(bytes*8!=width)
bytes++;
Expand Down Expand Up @@ -529,15 +532,16 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns)
else if(expr.id()==ID_index)
{
const index_exprt &index_expr=to_index_expr(expr);
const typet &array_type=ns.follow(index_expr.array().type());
DATA_INVARIANT(
array_type.id()==ID_array,
"index into array expected, found "+array_type.id_string());
index_expr.array().type().id() == ID_array,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

? Are you sure about removing the ns.follow, couldn't the array have symbol type here?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, we don't use symbol types for arrays (anymore - I think many many years ago we might).

"index into array expected, found " +
index_expr.array().type().id_string());

auto o = compute_pointer_offset(index_expr.array(), ns);

if(o.has_value())
{
const auto &array_type = to_array_type(index_expr.array().type());
auto sub_size = pointer_offset_size(array_type.subtype(), ns);

mp_integer i;
Expand Down
Loading