Skip to content

type symbols now use ID_symbol_type #2205

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 3 commits into from
Aug 14, 2018
Merged

type symbols now use ID_symbol_type #2205

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
f93deec
type symbols now use ID_symbol_type
May 18, 2018
6178908
bump goto binary version
Jul 30, 2018
355fbd2
avoid assert()
Jul 30, 2018
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
6 changes: 3 additions & 3 deletions jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ void ci_lazy_methods_neededt::gather_field_types(
{
// If class_type is not a symbol this may be a reference array,
// but we can't tell what type.
if(class_type.id() == ID_symbol)
if(class_type.id() == ID_symbol_type)
Copy link
Contributor

Choose a reason for hiding this comment

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

To avoid this pain in the future, in the TG bump I am going to use can_cast_type<symbol_typet>(class_type) rather than directly accessing the ID - you might like to do something similar with this PR while the TG bump is being prepared 😊

Copy link
Member Author

Choose a reason for hiding this comment

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

This should be one-off -- we should simply stick to the convention that the id() matches the name of the class type.

Copy link
Contributor

@thk123 thk123 Jul 24, 2018 •
edited
Loading

Choose a reason for hiding this comment

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

should be considered to rename it all to typedef_type

Seems like it could change at least one more time.

In any case, this pattern, were it to be used more widely, would hide more of the internal ireps and make changes like this less painful in future.

It also allows for at a later date adding more rigorous type checking (e.g. a symbol_typet should always have one named sub, ID_identifier etc).

{
const typet &element_type =
java_array_element_type(to_symbol_type(class_type));
Expand All @@ -127,11 +127,11 @@ void ci_lazy_methods_neededt::gather_field_types(
{
for(const auto &field : underlying_type.components())
{
if(field.type().id() == ID_struct || field.type().id() == ID_symbol)
if(field.type().id() == ID_struct || field.type().id() == ID_symbol_type)
gather_field_types(field.type(), ns);
else if(field.type().id() == ID_pointer)
{
if(field.type().subtype().id() == ID_symbol)
if(field.type().subtype().id() == ID_symbol_type)
{
add_all_needed_classes(to_pointer_type(field.type()));
}
Expand Down
8 changes: 4 additions & 4 deletions jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1633,7 +1633,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
const typecast_exprt pointer(op[0], java_array_type(statement[0]));

dereference_exprt array(pointer, pointer.type().subtype());
assert(pointer.type().subtype().id()==ID_symbol);
PRECONDITION(pointer.type().subtype().id() == ID_symbol_type);
array.set(ID_java_member_access, true);

const member_exprt length(array, "length", java_int_type());
Expand Down Expand Up @@ -2562,7 +2562,7 @@ codet java_bytecode_convert_methodt::convert_putstatic(
const exprt::operandst &op,
const symbol_exprt &symbol_expr)
{
if(needed_lazy_methods && arg0.type().id() == ID_symbol)
if(needed_lazy_methods && arg0.type().id() == ID_symbol_type)
{
needed_lazy_methods->add_needed_class(
to_symbol_type(arg0.type()).get_identifier());
Expand Down Expand Up @@ -2612,15 +2612,15 @@ void java_bytecode_convert_methodt::convert_getstatic(
{
if(needed_lazy_methods)
{
if(arg0.type().id() == ID_symbol)
if(arg0.type().id() == ID_symbol_type)
{
needed_lazy_methods->add_needed_class(
to_symbol_type(arg0.type()).get_identifier());
}
else if(arg0.type().id() == ID_pointer)
{
const auto &pointer_type = to_pointer_type(arg0.type());
if(pointer_type.subtype().id() == ID_symbol)
if(pointer_type.subtype().id() == ID_symbol_type)
{
needed_lazy_methods->add_needed_class(
to_symbol_type(pointer_type.subtype()).get_identifier());
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ java_bytecode_parse_treet::find_annotation(
if(annotation.type.id() != ID_pointer)
return false;
const typet &type = annotation.type.subtype();
return type.id() == ID_symbol &&
return type.id() == ID_symbol_type &&
to_symbol_type(type).get_identifier() == annotation_type_name;
});
if(annotation_it == annotations.end())
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_bytecode_parser.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -616,7 +616,7 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src)
for(const auto &p : ct.parameters())
get_class_refs_rec(p.type());
}
else if(src.id()==ID_symbol)
else if(src.id()==ID_symbol_type)
{
irep_idt name=src.get(ID_C_base_name);
if(has_prefix(id2string(name), "array["))
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]

void java_bytecode_typecheckt::typecheck_type(typet &type)
{
if(type.id()==ID_symbol)
if(type.id() == ID_symbol_type)
{
irep_idt identifier=to_symbol_type(type).get_identifier();

Expand Down
4 changes: 2 additions & 2 deletions jbmc/src/java_bytecode/java_object_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1179,7 +1179,7 @@ void java_object_factoryt::gen_nondet_init(
if(is_sub)
{
const typet &symbol = override_ ? override_type : expr.type();
PRECONDITION(symbol.id() == ID_symbol);
PRECONDITION(symbol.id() == ID_symbol_type);
generic_parameter_specialization_map_keys.insert_pairs_for_symbol(
to_symbol_type(symbol), struct_type);
}
Expand Down Expand Up @@ -1286,7 +1286,7 @@ void java_object_factoryt::gen_nondet_array_init(
const source_locationt &location)
{
PRECONDITION(expr.type().id()==ID_pointer);
PRECONDITION(expr.type().subtype().id()==ID_symbol);
PRECONDITION(expr.type().subtype().id() == ID_symbol_type);
PRECONDITION(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE);

const typet &type=ns.follow(expr.type().subtype());
Expand Down
16 changes: 8 additions & 8 deletions jbmc/src/java_bytecode/java_string_library_preprocess.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ Date: April 2017
irep_idt get_tag(const typet &type)
{
/// \todo Use follow instead of assuming tag to symbol relationship.
if(type.id() == ID_symbol)
if(type.id() == ID_symbol_type)
return to_symbol_type(type).get_identifier();
else if(type.id() == ID_struct)
return irep_idt("java::" + id2string(to_struct_type(type).get_tag()));
Expand Down Expand Up @@ -394,11 +394,11 @@ java_string_library_preprocesst::process_equals_function_operands(
/// \return type of the "data" component
static typet get_data_type(const typet &type, const symbol_tablet &symbol_table)
{
PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol);
if(type.id()==ID_symbol)
PRECONDITION(type.id() == ID_struct || type.id() == ID_symbol_type);
if(type.id() == ID_symbol_type)
{
symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier());
CHECK_RETURN(sym.type.id()!=ID_symbol);
CHECK_RETURN(sym.type.id() != ID_symbol_type);
return get_data_type(sym.type, symbol_table);
}
// else type id is ID_struct
Expand All @@ -413,11 +413,11 @@ static typet get_data_type(const typet &type, const symbol_tablet &symbol_table)
static typet
get_length_type(const typet &type, const symbol_tablet &symbol_table)
{
PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol);
if(type.id()==ID_symbol)
PRECONDITION(type.id() == ID_struct || type.id() == ID_symbol_type);
if(type.id() == ID_symbol_type)
{
symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier());
CHECK_RETURN(sym.type.id()!=ID_symbol);
CHECK_RETURN(sym.type.id() != ID_symbol_type);
return get_length_type(sym.type, symbol_table);
}
// else type id is ID_struct
Expand Down Expand Up @@ -892,7 +892,7 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
PRECONDITION(implements_java_char_sequence_pointer(rhs.type()));

typet deref_type;
if(rhs.type().subtype().id()==ID_symbol)
if(rhs.type().subtype().id() == ID_symbol_type)
deref_type=symbol_table.lookup_ref(
to_symbol_type(rhs.type().subtype()).get_identifier()).type;
else
Expand Down
7 changes: 4 additions & 3 deletions jbmc/src/java_bytecode/java_types.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -777,7 +777,8 @@ bool equal_java_types(const typet &type1, const typet &type2)
bool arrays_with_same_element_type = true;
if(
type1.id() == ID_pointer && type2.id() == ID_pointer &&
type1.subtype().id() == ID_symbol && type2.subtype().id() == ID_symbol)
type1.subtype().id() == ID_symbol_type &&
type2.subtype().id() == ID_symbol_type)
{
const symbol_typet &subtype_symbol1 = to_symbol_type(type1.subtype());
const symbol_typet &subtype_symbol2 = to_symbol_type(type2.subtype());
Expand Down Expand Up @@ -824,7 +825,7 @@ void get_dependencies_from_generic_parameters_rec(
}

// symbol type
else if(t.id() == ID_symbol)
else if(t.id() == ID_symbol_type)
{
const symbol_typet &symbol_type = to_symbol_type(t);
const irep_idt class_name(symbol_type.get_identifier());
Expand Down Expand Up @@ -958,7 +959,7 @@ std::string pretty_java_type(const typet &type)
return "byte";
else if(is_reference(type))
{
if(type.subtype().id() == ID_symbol)
if(type.subtype().id() == ID_symbol_type)
{
const auto &symbol_type = to_symbol_type(type.subtype());
const irep_idt &id = symbol_type.get_identifier();
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/remove_instanceof.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ bool remove_instanceoft::lower_instanceof(

// Find all types we know about that satisfy the given requirement:
INVARIANT(
target_type.id()==ID_symbol,
target_type.id() == ID_symbol_type,
"instanceof second operand should have a simple type");
const irep_idt &target_name=
to_symbol_type(target_type).get_identifier();
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/select_pointer_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ pointer_typet select_pointer_typet::specialize_generics(
visited_nodes.erase(parameter_name);
return returned_type;
}
else if(pointer_type.subtype().id() == ID_symbol)
else if(pointer_type.subtype().id() == ID_symbol_type)
{
// if the pointer is an array, recursively specialize its element type
const symbol_typet &array_subtype = to_symbol_type(pointer_type.subtype());
Expand Down
2 changes: 1 addition & 1 deletion jbmc/unit/java-testing-utils/require_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -427,7 +427,7 @@ require_type::require_complete_java_non_generic_class(const typet &class_type)
const symbol_typet &
require_type::require_symbol(const typet &type, const irep_idt &identifier)
{
REQUIRE(type.id() == ID_symbol);
REQUIRE(type.id() == ID_symbol_type);
const symbol_typet &result = to_symbol_type(type);
if(identifier != "")
{
Expand Down
4 changes: 2 additions & 2 deletions jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ SCENARIO(
next.type(),
{{require_type::type_argument_kindt::Var, "java::KeyValue::K"},
{require_type::type_argument_kindt::Var, "java::KeyValue::V"}});
REQUIRE(next_type.subtype().id() == ID_symbol);
REQUIRE(next_type.subtype().id() == ID_symbol_type);
const symbol_typet &next_symbol = to_symbol_type(next_type.subtype());
REQUIRE(
symbol_table.lookup_ref(next_symbol.get_identifier()).name ==
Expand All @@ -75,7 +75,7 @@ SCENARIO(
reverse.type(),
{{require_type::type_argument_kindt::Var, "java::KeyValue::V"},
{require_type::type_argument_kindt::Var, "java::KeyValue::K"}});
REQUIRE(next_type.subtype().id() == ID_symbol);
REQUIRE(next_type.subtype().id() == ID_symbol_type);
const symbol_typet &reverse_symbol = to_symbol_type(reverse_type.subtype());
REQUIRE(
symbol_table.lookup_ref(next_symbol.get_identifier()).name ==
Expand Down
Binary file modified regression/ansi-c/arch_flags_mcpu_bad/object.intel
View file
Open in desktop
Binary file not shown.
Binary file modified regression/ansi-c/arch_flags_mcpu_good/object.arm
View file
Open in desktop
Binary file not shown.
Binary file modified regression/ansi-c/arch_flags_mthumb_good/object.arm
View file
Open in desktop
Binary file not shown.
Binary file modified regression/goto-diff/syntactic-diff1/a.gb
View file
Open in desktop
Binary file not shown.
Binary file modified regression/goto-diff/syntactic-diff1/b.gb
View file
Open in desktop
Binary file not shown.
2 changes: 1 addition & 1 deletion src/analyses/invariant_propagation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -189,7 +189,7 @@ bool invariant_propagationt::check_type(const typet &type) const
return false;
else if(type.id()==ID_array)
return false;
else if(type.id()==ID_symbol)
else if(type.id() == ID_symbol_type)
return check_type(ns.follow(type));
else if(type.id()==ID_unsignedbv ||
type.id()==ID_signedbv)
Expand Down
7 changes: 3 additions & 4 deletions src/analyses/uncaught_exceptions_analysis.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,11 +19,10 @@ irep_idt uncaught_exceptions_domaint::get_exception_type(const typet &type)
{
PRECONDITION(type.id()==ID_pointer);

if(type.subtype().id()==ID_symbol)
{
if(type.subtype().id() == ID_symbol_type)
return to_symbol_type(type.subtype()).get_identifier();
}
return ID_empty;
else
Copy link
Contributor

Choose a reason for hiding this comment

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

Nit: Unrelated change should either not be done or go in its own commit

return ID_empty;
}

/// Returns the symbol corresponding to an exception
Expand Down
8 changes: 5 additions & 3 deletions src/ansi-c/c_typecast.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -253,7 +253,8 @@ bool check_c_implicit_typecast(
typet c_typecastt::follow_with_qualifiers(const typet &src_type)
{
if(
src_type.id() != ID_symbol && src_type.id() != ID_struct_tag &&
src_type.id() != ID_symbol_type &&
src_type.id() != ID_struct_tag &&
src_type.id() != ID_union_tag)
{
return src_type;
Expand All @@ -264,7 +265,8 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)
// collect qualifiers
c_qualifierst qualifiers(src_type);

while(result_type.id() == ID_symbol || result_type.id() == ID_struct_tag ||
while(result_type.id() == ID_symbol_type ||
result_type.id() == ID_struct_tag ||
result_type.id() == ID_union_tag)
{
const typet &followed_type = ns.follow(result_type);
Expand Down Expand Up @@ -348,7 +350,7 @@ c_typecastt::c_typet c_typecastt::get_c_type(
{
return INT;
}
else if(type.id()==ID_symbol)
else if(type.id() == ID_symbol_type)
return get_c_type(ns.follow(type));
else if(type.id()==ID_rational)
return RATIONAL;
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_base.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -406,7 +406,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
final_old.subtype()==final_new.subtype())
{
// we don't do symbol types for arrays anymore
PRECONDITION(old_symbol.type.id()!=ID_symbol);
PRECONDITION(old_symbol.type.id() != ID_symbol_type);
old_symbol.type=new_symbol.type;
}
else if((final_old.id()==ID_incomplete_c_enum ||
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_code.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -383,7 +383,7 @@ bool c_typecheck_baset::is_complete_type(const typet &type) const
}
else if(type.id()==ID_vector)
return is_complete_type(type.subtype());
else if(type.id()==ID_symbol)
else if(type.id() == ID_symbol_type)
return is_complete_type(follow(type));

return true;
Expand Down
8 changes: 4 additions & 4 deletions src/ansi-c/c_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,9 +91,9 @@ bool c_typecheck_baset::gcc_types_compatible_p(
// read
// http://gcc.gnu.org/onlinedocs/gcc-3.3.6/gcc/Other-Builtins.html

if(type1.id()==ID_symbol)
if(type1.id() == ID_symbol_type)
return gcc_types_compatible_p(follow(type1), type2);
else if(type2.id()==ID_symbol)
else if(type2.id() == ID_symbol_type)
return gcc_types_compatible_p(type1, follow(type2));

// check qualifiers first
Expand Down Expand Up @@ -3067,8 +3067,8 @@ void c_typecheck_baset::typecheck_arithmetic_pointer(const exprt &expr)

typet subtype=type.subtype();

if(subtype.id()==ID_symbol)
subtype=follow(subtype);
if(subtype.id() == ID_symbol_type)
subtype = follow(to_symbol_type(subtype));

if(subtype.id()==ID_incomplete_struct)
{
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_initializer.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -492,7 +492,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(

const typet &type=designator.back().subtype;
const typet &full_type=follow(type);
assert(full_type.id()!=ID_symbol);
CHECK_RETURN(full_type.id() != ID_symbol_type);

// do we initialize a scalar?
if(full_type.id()!=ID_struct &&
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ void c_typecheck_baset::typecheck_type(typet &type)
typecheck_c_bit_field_type(to_c_bit_field_type(type));
else if(type.id()==ID_typeof)
typecheck_typeof_type(type);
else if(type.id()==ID_symbol)
else if(type.id() == ID_symbol_type)
typecheck_symbol_type(to_symbol_type(type));
else if(type.id() == ID_typedef_type)
typecheck_typedef_type(type);
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/expr2c.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -457,7 +457,7 @@ std::string expr2ct::convert_rec(
return convert_rec(
src.subtype(), qualifiers, declarator+"[]");
}
else if(src.id()==ID_symbol)
else if(src.id() == ID_symbol_type)
{
symbol_typet symbolic_type=to_symbol_type(src);
const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef);
Expand Down
4 changes: 2 additions & 2 deletions src/ansi-c/padding.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,8 +86,8 @@ mp_integer alignment(const typet &type, const namespacet &ns)
result = alignment(ns.follow_tag(to_struct_tag_type(type)), ns);
else if(type.id() == ID_union_tag)
result = alignment(ns.follow_tag(to_union_tag_type(type)), ns);
else if(type.id()==ID_symbol)
result=alignment(ns.follow(type), ns);
else if(type.id() == ID_symbol_type)
result = alignment(ns.follow(to_symbol_type(type)), ns);
else if(type.id()==ID_c_bit_field)
{
// we align these according to the 'underlying type'
Expand Down
7 changes: 3 additions & 4 deletions src/ansi-c/type2name.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -187,10 +187,9 @@ static std::string type2name(
else
result+="ARR"+integer2string(size);
}
else if(type.id()==ID_symbol ||
type.id()==ID_c_enum_tag ||
type.id()==ID_struct_tag ||
type.id()==ID_union_tag)
else if(
type.id() == ID_symbol_type || type.id() == ID_c_enum_tag ||
type.id() == ID_struct_tag || type.id() == ID_union_tag)
{
parent_is_sym_check=true;
result+=type2name_symbol(type, ns, symbol_number);
Expand Down
20 changes: 7 additions & 13 deletions src/cpp/cpp_convert_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -588,19 +588,13 @@ void cpp_convert_typet::write(typet &type)

void cpp_convert_plain_type(typet &type)
{
if(type.id()==ID_cpp_name ||
type.id()==ID_struct ||
type.id()==ID_union ||
type.id()==ID_array ||
type.id()==ID_code ||
type.id()==ID_unsignedbv ||
type.id()==ID_signedbv ||
type.id()==ID_bool ||
type.id()==ID_floatbv ||
type.id()==ID_empty ||
type.id()==ID_symbol ||
type.id()==ID_constructor ||
type.id()==ID_destructor)
if(
type.id() == ID_cpp_name || type.id() == ID_struct ||
type.id() == ID_union || type.id() == ID_array || type.id() == ID_code ||
type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
type.id() == ID_bool || type.id() == ID_floatbv || type.id() == ID_empty ||
type.id() == ID_symbol_type || type.id() == ID_constructor ||
type.id() == ID_destructor)
{
}
else if(type.id()==ID_c_enum)
Expand Down
Loading