Skip to content

Add initializer list constructor to struct/union typet and cleanup API use [blocks: #3597] #3623

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.

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
Jan 21, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
4 changes: 1 addition & 3 deletions jbmc/src/java_bytecode/java_root_class.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -25,10 +25,8 @@ void java_root_class(symbolt &class_symbol)

{
// the class identifier is used for stuff such as 'instanceof'
struct_typet::componentt component;
component.set_name("@class_identifier");
struct_typet::componentt component("@class_identifier", string_typet());
component.set_pretty_name("@class_identifier");
component.type()=string_typet();

// add at the beginning
components.insert(components.begin(), component);
Expand Down
23 changes: 11 additions & 12 deletions jbmc/src/java_bytecode/java_string_library_preprocess.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1254,9 +1254,9 @@ java_string_library_preprocesst::get_primitive_value_of_object(
const auto maybe_symbol =
symbol_table.lookup(object_type->get_identifier()))
{
struct_typet struct_type=to_struct_type(maybe_symbol->type);
const struct_typet &struct_type = to_struct_type(maybe_symbol->type);
// Check that the type has a value field
const struct_union_typet::componentt value_comp=
const struct_union_typet::componentt &value_comp =
struct_type.get_component("value");
if(!value_comp.is_nil())
{
Expand Down Expand Up @@ -1454,17 +1454,16 @@ code_blockt java_string_library_preprocesst::make_string_format_code(
// The argument can be:
// a string, an integer, a floating point, a character, a boolean,
// an object of which we take the hash code, or a date/time
struct_typet structured_type;
struct_typet structured_type({{"string_expr", refined_string_type},
{ID_int, java_int_type()},
{ID_float, java_float_type()},
{ID_char, java_char_type()},
{ID_boolean, java_boolean_type()},
// TODO: hash_code not implemented for now
{"hashcode", java_int_type()},
// TODO: date_time type not implemented for now
{"date_time", java_int_type()}});
structured_type.set_tag(CPROVER_PREFIX "string_formatter_variant");
structured_type.components().emplace_back("string_expr", refined_string_type);
structured_type.components().emplace_back(ID_int, java_int_type());
structured_type.components().emplace_back(ID_float, java_float_type());
structured_type.components().emplace_back(ID_char, java_char_type());
structured_type.components().emplace_back(ID_boolean, java_boolean_type());
// TODO: hash_code not implemented for now
structured_type.components().emplace_back("hashcode", java_int_type());
// TODO: date_time type not implemented for now
structured_type.components().emplace_back("date_time", java_int_type());

// We will process arguments so that each is converted to a `struct_exprt`
// containing each possible type used in format specifiers.
Expand Down
7 changes: 2 additions & 5 deletions jbmc/src/java_bytecode/java_utils.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -239,11 +239,8 @@ void java_add_components_to_class(
PRECONDITION(class_symbol.type.id()==ID_struct);
struct_typet &struct_type=to_struct_type(class_symbol.type);
struct_typet::componentst &components=struct_type.components();

for(const struct_union_typet::componentt &component : components_to_add)
{
components.push_back(component);
}
components.insert(
components.end(), components_to_add.begin(), components_to_add.end());
}

/// Declare a function with the given name and type.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -30,14 +30,13 @@ typet length_type()
/// Make a struct with a pointer content and an integer length
struct_exprt make_string_argument(std::string name)
{
struct_typet type;
const array_typet char_array(char_type(), infinity_exprt(length_type()));
type.components().emplace_back("length", length_type());
type.components().emplace_back("content", pointer_type(char_array));
struct_typet type(
{{"length", length_type()}, {"content", pointer_type(char_array)}});

const symbol_exprt length(name + "_length", length_type());
const symbol_exprt content(name + "_content", pointer_type(java_char_type()));
return struct_exprt({length, content}, type);
symbol_exprt length(name + "_length", length_type());
symbol_exprt content(name + "_content", pointer_type(java_char_type()));
return struct_exprt({std::move(length), std::move(content)}, std::move(type));
}

SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -36,9 +36,8 @@ SCENARIO("string_identifiers_resolution_from_equations",
constant_exprt e("e", string_typet());
constant_exprt f("f", string_typet());

struct_typet struct_type;
struct_type.components().emplace_back("str1", string_typet());
struct_type.components().emplace_back("str2", string_typet());
struct_typet struct_type(
{{"str1", string_typet()}, {"str2", string_typet()}});
struct_exprt struct_expr({a, f}, struct_type);
symbol_exprt symbol_struct("sym_struct", struct_type);

Expand Down
9 changes: 3 additions & 6 deletions jbmc/unit/util/has_subtype.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -37,9 +37,8 @@ SCENARIO("has_subtype", "[core][utils][has_subtype]")

GIVEN("a struct with char and int fields")
{
struct_typet struct_type;
struct_type.components().emplace_back("char_field", char_type);
struct_type.components().emplace_back("int_field", int_type);
struct_typet struct_type(
{{"char_field", char_type}, {"int_field", int_type}});
THEN("char and int are subtypes")
{
REQUIRE(has_subtype(struct_type, is_type(char_type), ns));
Expand Down Expand Up @@ -67,9 +66,7 @@ SCENARIO("has_subtype", "[core][utils][has_subtype]")
GIVEN("a recursive struct definition")
{
struct_tag_typet struct_tag("A-struct");
struct_typet::componentt comp("ptr", pointer_type(struct_tag));
struct_typet struct_type;
struct_type.components().push_back(comp);
struct_typet struct_type({{"ptr", pointer_type(struct_tag)}});

symbolt s;
s.type = struct_type;
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1538,7 +1538,7 @@ void c_typecheck_baset::typecheck_expr_member(exprt &expr)
expr.get(ID_component_name);

// first try to find directly
struct_union_typet::componentt component=
const struct_union_typet::componentt &component =
struct_union_type.get_component(component_name);

Copy link
Member

Choose a reason for hiding this comment

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

Seems unrelated?

// if that fails, search the anonymous members
Expand Down
6 changes: 2 additions & 4 deletions src/ansi-c/expr2c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1573,8 +1573,7 @@ std::string expr2ct::convert_member(

if(component_name!="")
{
const exprt comp_expr=
struct_union_type.get_component(component_name);
const exprt &comp_expr = struct_union_type.get_component(component_name);

if(comp_expr.is_nil())
return convert_norep(src, precedence);
Expand All @@ -1592,8 +1591,7 @@ std::string expr2ct::convert_member(
if(n>=struct_union_type.components().size())
return convert_norep(src, precedence);

const exprt comp_expr=
struct_union_type.components()[n];
const exprt &comp_expr = struct_union_type.components()[n];

dest+=comp_expr.get_string(ID_pretty_name);

Expand Down
13 changes: 7 additions & 6 deletions src/cpp/cpp_typecheck_compound_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1699,14 +1699,15 @@ void cpp_typecheckt::make_ptr_typecast(
assert(src_type.id()== ID_pointer);
assert(dest_type.id()== ID_pointer);

struct_typet src_struct =
to_struct_type(static_cast<const typet&>(follow(src_type.subtype())));
const struct_typet &src_struct =
to_struct_type(static_cast<const typet &>(follow(src_type.subtype())));

struct_typet dest_struct =
to_struct_type(static_cast<const typet&>(follow(dest_type.subtype())));
const struct_typet &dest_struct =
to_struct_type(static_cast<const typet &>(follow(dest_type.subtype())));

assert(subtype_typecast(src_struct, dest_struct) ||
subtype_typecast(dest_struct, src_struct));
PRECONDITION(
subtype_typecast(src_struct, dest_struct) ||
subtype_typecast(dest_struct, src_struct));

expr.make_typecast(dest_type);
}
18 changes: 9 additions & 9 deletions src/cpp/cpp_typecheck_conversions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -619,10 +619,10 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member(
return true;
}

struct_typet from_struct = to_struct_type(
const struct_typet &from_struct = to_struct_type(
follow(static_cast<const typet &>(expr.type().find(ID_to_member))));

struct_typet to_struct =
const struct_typet &to_struct =
to_struct_type(follow(static_cast<const typet &>(type.find(ID_to_member))));

if(subtype_typecast(to_struct, from_struct))
Expand Down Expand Up @@ -1891,8 +1891,8 @@ bool cpp_typecheckt::static_typecast(
if(!qual_to.is_subset_of(qual_from))
return false;

struct_typet from_struct=to_struct_type(from);
struct_typet subto_struct=to_struct_type(subto);
const struct_typet &from_struct = to_struct_type(from);
const struct_typet &subto_struct = to_struct_type(subto);

if(subtype_typecast(subto_struct, from_struct))
{
Expand Down Expand Up @@ -1975,8 +1975,8 @@ bool cpp_typecheckt::static_typecast(
return false;
}

struct_typet from_struct=to_struct_type(from);
struct_typet to_struct=to_struct_type(to);
const struct_typet &from_struct = to_struct_type(from);
const struct_typet &to_struct = to_struct_type(to);
if(subtype_typecast(to_struct, from_struct))
{
make_ptr_typecast(e, type);
Expand All @@ -1994,10 +1994,10 @@ bool cpp_typecheckt::static_typecast(
if(type.subtype()!=e.type().subtype())
return false;

struct_typet from_struct = to_struct_type(
const struct_typet &from_struct = to_struct_type(
follow(static_cast<const typet &>(e.type().find(ID_to_member))));

struct_typet to_struct = to_struct_type(
const struct_typet &to_struct = to_struct_type(
follow(static_cast<const typet &>(type.find(ID_to_member))));

if(subtype_typecast(from_struct, to_struct))
Expand All @@ -2014,7 +2014,7 @@ bool cpp_typecheckt::static_typecast(
if(type.subtype() != e.type().subtype())
return false;

struct_typet from_struct = to_struct_type(
const struct_typet &from_struct = to_struct_type(
follow(static_cast<const typet &>(e.type().find(ID_to_member))));

new_expr = e;
Expand Down
2 changes: 1 addition & 1 deletion src/cpp/cpp_typecheck_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1175,7 +1175,7 @@ void cpp_typecheckt::typecheck_expr_member(
else
{
// it must be a static component
const struct_typet::componentt pcomp=
const struct_typet::componentt &pcomp =
type.get_component(to_symbol_expr(symbol_expr).get_identifier());
Copy link
Member

Choose a reason for hiding this comment

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

Seems unrelated to PR?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I may have overstretched the "cleanup API use."


if(pcomp.is_nil())
Expand Down
2 changes: 1 addition & 1 deletion src/cpp/cpp_typecheck_resolve.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,7 @@ exprt cpp_typecheck_resolvet::convert_identifier(
const struct_union_typet &struct_union_type=
to_struct_union_type(compound_symbol.type);

const exprt component=
const exprt &component =
struct_union_type.get_component(identifier.identifier);

const typet &type=component.type();
Expand Down
10 changes: 3 additions & 7 deletions src/goto-programs/remove_complex.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -257,15 +257,11 @@ static void remove_complex(typet &type)

// Replace by a struct with two members.
// The real part goes first.
struct_typet struct_type;
struct_typet struct_type(
{{ID_real, type.subtype()}, {ID_imag, type.subtype()}});
struct_type.add_source_location()=type.source_location();
struct_type.components().resize(2);
struct_type.components()[0].type()=type.subtype();
struct_type.components()[0].set_name(ID_real);
struct_type.components()[1].type()=type.subtype();
struct_type.components()[1].set_name(ID_imag);

type=struct_type;
type = std::move(struct_type);
}
}

Expand Down
17 changes: 4 additions & 13 deletions src/goto-programs/string_abstraction.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -101,23 +101,14 @@ string_abstractiont::string_abstractiont(
ns(_symbol_table),
temporary_counter(0)
{
struct_typet s;

s.components().resize(3);

s.components()[0].set_name("is_zero");
struct_typet s({{"is_zero", build_type(whatt::IS_ZERO)},
{"length", build_type(whatt::LENGTH)},
{"size", build_type(whatt::SIZE)}});
s.components()[0].set_pretty_name("is_zero");
s.components()[0].type()=build_type(whatt::IS_ZERO);

s.components()[1].set_name("length");
s.components()[1].set_pretty_name("length");
s.components()[1].type()=build_type(whatt::LENGTH);

s.components()[2].set_name("size");
s.components()[2].set_pretty_name("size");
s.components()[2].type()=build_type(whatt::SIZE);

string_struct=s;
string_struct = std::move(s);
}

typet string_abstractiont::build_type(whatt what)
Expand Down
3 changes: 1 addition & 2 deletions src/util/refined_string_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,7 @@ Author: Romain Brenguier, [email protected]
refined_string_typet::refined_string_typet(
const typet &index_type,
const pointer_typet &content_type)
: struct_typet({{"length", index_type}, {"content", content_type}})
{
components().emplace_back("length", index_type);
components().emplace_back("content", content_type);
set_tag(CPROVER_PREFIX"refined_string_type");
}
16 changes: 16 additions & 0 deletions src/util/std_types.h
Original file line number Diff line number Diff line change
Expand Up @@ -202,6 +202,12 @@ class struct_union_typet:public typet

typedef std::vector<componentt> componentst;

struct_union_typet(const irep_idt &_id, componentst &&_components)
: typet(_id)
{
components() = std::move(_components);
}

const componentst &components() const
{
return (const componentst &)(find(ID_components).get_sub());
Expand Down Expand Up @@ -292,6 +298,11 @@ class struct_typet:public struct_union_typet
{
}

explicit struct_typet(componentst &&_components)
: struct_union_typet(ID_struct, std::move(_components))
{
}

bool is_prefix_of(const struct_typet &other) const;

/// A struct may be a class, where members may have access restrictions.
Expand Down Expand Up @@ -440,6 +451,11 @@ class union_typet:public struct_union_typet
union_typet():struct_union_typet(ID_union)
{
}

explicit union_typet(componentst &&_components)
: struct_union_typet(ID_union, std::move(_components))
{
}
};

/// Check whether a reference to a typet is a \ref union_typet.
Expand Down
19 changes: 7 additions & 12 deletions unit/pointer-analysis/value_set.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -47,29 +47,24 @@ SCENARIO(
{
// Create struct A { A *x; A *y }

struct_typet struct_A;
struct_typet struct_A({{"x", pointer_typet(struct_tag_typet("A"), 64)},
{"y", pointer_typet(struct_tag_typet("A"), 64)}});
struct_A.set_tag("A");
Copy link
Member

Choose a reason for hiding this comment

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

These should now actually be struct_tag types!

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

If that's a strict requirement in goto programs then we need a validation pass that says so?! Otherwise that unit test would seem ok to me?

struct_A.components().resize(2);

type_symbolt A_symbol(struct_A);
A_symbol.name = "A";
A_symbol.base_name = "A";
A_symbol.pretty_name = "A";

auto &A_x = struct_A.components()[0];
auto &A_y = struct_A.components()[1];

A_x.set_name("x");
A_x.set_base_name("x");
A_x.set_pretty_name("x");
A_x.type() = pointer_typet(struct_tag_typet(A_symbol.name), 64);

A_y.set_name("y");
A_y.set_base_name("y");
A_y.set_pretty_name("y");
A_y.type() = pointer_typet(struct_tag_typet(A_symbol.name), 64);

A_symbol.type = struct_A;
type_symbolt A_symbol(struct_A);
A_symbol.name = "A";
A_symbol.base_name = "A";
A_symbol.pretty_name = "A";

symbol_table.add(A_symbol);

// Create global symbols struct A a1, a2, a3;
Expand Down
4 changes: 1 addition & 3 deletions unit/util/pointer_offset_size.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -79,9 +79,7 @@ TEST_CASE("Build subexpression to access element at offset into struct")

const signedbv_typet t(32);

struct_typet st;
st.components().emplace_back("foo", t);
st.components().emplace_back("bar", t);
struct_typet st({{"foo", t}, {"bar", t}});

symbol_exprt s("struct", st);

Expand Down