Skip to content
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

goto-programs: Replace uses of namespacet::follow #8230

Merged
merged 2 commits into from
Apr 18, 2024
Merged

goto-programs: Replace uses of namespacet::follow #8230

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d26743a
Use conditional_cast instead of make_type
tautschnig Mar 6, 2024
60dc466
goto-programs: Replace uses of namespacet::follow
tautschnig Mar 6, 2024
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
7 changes: 4 additions & 3 deletions src/goto-programs/class_identifier.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,8 @@ static exprt build_class_identifier(

while(1)
{
const typet &type=ns.follow(e.type());
const struct_typet &struct_type=to_struct_type(type);
const struct_typet &struct_type =
ns.follow_tag(to_struct_tag_type(e.type()));
const struct_typet::componentst &components=struct_type.components();
INVARIANT(!components.empty(), "class structs cannot be empty");

Expand Down Expand Up @@ -85,7 +85,8 @@ void set_class_identifier(
const namespacet &ns,
const struct_tag_typet &class_type)
{
const struct_typet &struct_type=to_struct_type(ns.follow(expr.type()));
const struct_typet &struct_type =
ns.follow_tag(to_struct_tag_type(expr.type()));
const struct_typet::componentst &components=struct_type.components();

if(components.empty())
Expand Down
8 changes: 6 additions & 2 deletions src/goto-programs/destructor.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,9 +38,13 @@
{
const typet &arg_type=code_type.parameters().front().type();

if(arg_type.id() != ID_pointer)
continue;

Check warning on line 42 in src/goto-programs/destructor.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/destructor.cpp#L42 

Added line #L42 was not covered by tests

const typet &base_type = to_pointer_type(arg_type).base_type();
if(
arg_type.id() == ID_pointer &&
ns.follow(to_pointer_type(arg_type).base_type()) == type)
base_type.id() == ID_struct_tag &&
ns.follow_tag(to_struct_tag_type(base_type)) == type)
{
const symbol_exprt symbol_expr(op.get(ID_name), op.type());
return code_function_callt(symbol_expr);
Expand Down
9 changes: 5 additions & 4 deletions src/goto-programs/graphml_witness.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -132,10 +132,11 @@
return convert_assign_rec(identifier, tmp);
}

const struct_union_typet &type=
to_struct_union_type(ns.follow(assign.lhs().type()));
const struct_union_typet::componentst &components=
type.components();
const typet &lhs_type = assign.lhs().type();
const struct_union_typet::componentst &components =
(lhs_type.id() == ID_struct_tag || lhs_type.id() == ID_union_tag)
? ns.follow_tag(to_struct_or_union_tag_type(lhs_type)).components()
: to_struct_union_type(lhs_type).components();

Check warning on line 139 in src/goto-programs/graphml_witness.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/graphml_witness.cpp#L135-L139 

Added lines #L135 - L139 were not covered by tests

exprt::operandst::const_iterator it=
assign.rhs().operands().begin();
Expand Down
44 changes: 21 additions & 23 deletions src/goto-programs/interpreter.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -424,11 +424,11 @@
struct_typet::componentt
interpretert::get_component(const typet &object_type, const mp_integer &offset)
{
const typet real_type = ns.follow(object_type);
if(real_type.id()!=ID_struct)
if(object_type.id() != ID_struct_tag)

Check warning on line 427 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L427 

Added line #L427 was not covered by tests
throw "request for member of non-struct";

const struct_typet &struct_type=to_struct_type(real_type);
const struct_typet &struct_type =
ns.follow_tag(to_struct_tag_type(object_type));

Check warning on line 431 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L430-L431 

Added lines #L430 - L431 were not covered by tests
const struct_typet::componentst &components=struct_type.components();

mp_integer tmp_offset=offset;
Expand Down Expand Up @@ -460,11 +460,10 @@
const mp_integer &offset,
bool use_non_det)
{
const typet real_type=ns.follow(type);
if(real_type.id()==ID_struct)
if(type.id() == ID_struct_tag)

Check warning on line 463 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L463 

Added line #L463 was not covered by tests
{
struct_exprt result({}, real_type);
const struct_typet &struct_type=to_struct_type(real_type);
struct_exprt result({}, type);
const struct_typet &struct_type = ns.follow_tag(to_struct_tag_type(type));

Check warning on line 466 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L465-L466 

Added lines #L465 - L466 were not covered by tests
const struct_typet::componentst &components=struct_type.components();

// Retrieve the values for the individual members
Expand All @@ -482,10 +481,10 @@

return std::move(result);
}
else if(real_type.id()==ID_array)
else if(type.id() == ID_array)

Check warning on line 484 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L484 

Added line #L484 was not covered by tests
{
// Get size of array
array_exprt result({}, to_array_type(real_type));
array_exprt result({}, to_array_type(type));

Check warning on line 487 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L487 

Added line #L487 was not covered by tests
const exprt &size_expr = to_array_type(type).size();
mp_integer subtype_size = get_size(to_array_type(type).element_type());
mp_integer count;
Expand Down Expand Up @@ -526,13 +525,12 @@
mp_vectort &rhs,
const mp_integer &offset)
{
const typet real_type=ns.follow(type);
PRECONDITION(!rhs.empty());

if(real_type.id()==ID_struct)
if(type.id() == ID_struct_tag)
{
struct_exprt result({}, real_type);
const struct_typet &struct_type=to_struct_type(real_type);
struct_exprt result({}, type);
const struct_typet &struct_type = ns.follow_tag(to_struct_tag_type(type));

Check warning on line 533 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L532-L533 

Added lines #L532 - L533 were not covered by tests
const struct_typet::componentst &components=struct_type.components();

// Retrieve the values for the individual members
Expand All @@ -548,10 +546,10 @@
}
return std::move(result);
}
else if(real_type.id()==ID_array)
else if(type.id() == ID_array)
{
array_exprt result({}, to_array_type(real_type));
const exprt &size_expr = to_array_type(real_type).size();
array_exprt result({}, to_array_type(type));
const exprt &size_expr = to_array_type(type).size();

Check warning on line 552 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L551-L552 

Added lines #L551 - L552 were not covered by tests

// Get size of array
mp_integer subtype_size = get_size(to_array_type(type).element_type());
Expand All @@ -576,34 +574,34 @@
}
return std::move(result);
}
else if(real_type.id()==ID_floatbv)
else if(type.id() == ID_floatbv)
{
ieee_floatt f(to_floatbv_type(type));
f.unpack(rhs[numeric_cast_v<std::size_t>(offset)]);
return f.to_expr();
}
else if(real_type.id()==ID_fixedbv)
else if(type.id() == ID_fixedbv)
{
fixedbvt f;
f.from_integer(rhs[numeric_cast_v<std::size_t>(offset)]);
return f.to_expr();
}
else if(real_type.id()==ID_bool)
else if(type.id() == ID_bool)
{
if(rhs[numeric_cast_v<std::size_t>(offset)] != 0)
return true_exprt();
else
false_exprt();
}
else if(real_type.id()==ID_c_bool)
else if(type.id() == ID_c_bool)
{
return from_integer(
rhs[numeric_cast_v<std::size_t>(offset)] != 0 ? 1 : 0, type);
}
else if(real_type.id() == ID_pointer)
else if(type.id() == ID_pointer)
{
if(rhs[numeric_cast_v<std::size_t>(offset)] == 0)
return null_pointer_exprt(to_pointer_type(real_type)); // NULL pointer
return null_pointer_exprt(to_pointer_type(type)); // NULL pointer

if(rhs[numeric_cast_v<std::size_t>(offset)] < memory.size())
{
Expand Down Expand Up @@ -634,7 +632,7 @@

throw "interpreter: reading from invalid pointer";
}
else if(real_type.id()==ID_string)
else if(type.id() == ID_string)
{
// Strings are currently encoded by their irep_idt ID.
return constant_exprt(
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/interpreter_evaluate.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1042,7 +1042,7 @@
else if(expr.id()==ID_member)
{
const struct_typet &struct_type =
to_struct_type(ns.follow(to_member_expr(expr).compound().type()));
ns.follow_tag(to_struct_tag_type(to_member_expr(expr).compound().type()));

Check warning on line 1045 in src/goto-programs/interpreter_evaluate.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter_evaluate.cpp#L1045 

Added line #L1045 was not covered by tests

const irep_idt &component_name=
to_member_expr(expr).get_component_name();
Expand Down
30 changes: 14 additions & 16 deletions src/goto-programs/json_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -361,24 +361,22 @@
{
result["name"] = json_stringt("struct");

const typet &type = ns.follow(expr.type());
const struct_typet &struct_type =
expr.type().id() == ID_struct_tag
? ns.follow_tag(to_struct_tag_type(expr.type()))
: to_struct_type(expr.type());

Check warning on line 367 in src/goto-programs/json_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/json_expr.cpp#L367 

Added line #L367 was not covered by tests
const struct_typet::componentst &components = struct_type.components();
DATA_INVARIANT(
components.size() == expr.operands().size(),
"number of struct components should match with its type");

// these are expected to have a struct type
if(type.id() == ID_struct)
json_arrayt &members = result["members"].make_array();
for(std::size_t m = 0; m < expr.operands().size(); m++)
{
const struct_typet &struct_type = to_struct_type(type);
const struct_typet::componentst &components = struct_type.components();
DATA_INVARIANT(
components.size() == expr.operands().size(),
"number of struct components should match with its type");

json_arrayt &members = result["members"].make_array();
for(std::size_t m = 0; m < expr.operands().size(); m++)
{
json_objectt e{{"value", json(expr.operands()[m], ns, mode)},
{"name", json_stringt(components[m].get_name())}};
members.push_back(std::move(e));
}
json_objectt e{
{"value", json(expr.operands()[m], ns, mode)},
{"name", json_stringt(components[m].get_name())}};
members.push_back(std::move(e));
}
}
else if(expr.id() == ID_union)
Expand Down
3 changes: 2 additions & 1 deletion src/goto-programs/remove_const_function_pointers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -800,7 +800,8 @@ bool remove_const_function_pointerst::is_const_type(const typet &type) const
exprt remove_const_function_pointerst::get_component_value(
const struct_exprt &struct_expr, const member_exprt &member_expr)
{
const struct_typet &struct_type=to_struct_type(ns.follow(struct_expr.type()));
const struct_typet &struct_type =
ns.follow_tag(to_struct_tag_type(struct_expr.type()));
size_t component_number=
struct_type.component_number(member_expr.get_component_name());

Expand Down
5 changes: 4 additions & 1 deletion src/goto-programs/rewrite_union.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,10 @@ static bool restore_union_rec(exprt &expr, const namespacet &ns)
byte_extract_exprt &be = to_byte_extract_expr(expr);
if(be.op().type().id() == ID_union || be.op().type().id() == ID_union_tag)
{
const union_typet &union_type = to_union_type(ns.follow(be.op().type()));
const union_typet &union_type =
be.op().type().id() == ID_union_tag
? ns.follow_tag(to_union_tag_type(be.op().type()))
: to_union_type(be.op().type());

for(const auto &comp : union_type.components())
{
Expand Down
44 changes: 20 additions & 24 deletions src/goto-programs/string_abstraction.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -353,14 +353,10 @@ exprt string_abstractiont::make_val_or_dummy_rec(goto_programt &dest,
symbol.type.id() == ID_union_tag ||
(symbol.type.id() == ID_struct_tag && symbol.type != string_struct))
{
const struct_union_typet &su_source =
to_struct_union_type(ns.follow(source_type));
const struct_union_typet::componentst &s_components=
su_source.components();
const struct_union_typet &struct_union_type =
to_struct_union_type(ns.follow(symbol.type));
const struct_union_typet::componentst &components=
struct_union_type.components();
const struct_union_typet::componentst &s_components =
ns.follow_tag(to_struct_or_union_tag_type(source_type)).components();
const struct_union_typet::componentst &components =
ns.follow_tag(to_struct_or_union_tag_type(symbol.type)).components();
unsigned seen=0;

struct_union_typet::componentst::const_iterator it2=components.begin();
Expand Down Expand Up @@ -442,10 +438,9 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value(
build_unknown(whatt::LENGTH, false),
to_array_type(source_type).size().id() == ID_infinity
? build_unknown(whatt::SIZE, false)
: to_array_type(source_type).size()},
: typecast_exprt::conditional_cast(
to_array_type(source_type).size(), build_type(whatt::SIZE))},
string_struct);

make_type(to_struct_expr(new_symbol.value).op2(), build_type(whatt::SIZE));
}
else
new_symbol.value=
Expand Down Expand Up @@ -733,7 +728,10 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
{
const struct_union_typet &struct_union_type =
to_struct_union_type(ns.follow(type));
type.id() == ID_struct_tag ? static_cast<const struct_union_typet &>(
ns.follow_tag(to_struct_tag_type(type)))
: static_cast<const struct_union_typet &>(
ns.follow_tag(to_union_tag_type(type)));

struct_union_typet::componentst new_comp;
for(const auto &comp : struct_union_type.components())
Expand Down Expand Up @@ -1212,8 +1210,8 @@ goto_programt::targett string_abstractiont::abstract_char_assign(
i2.is_not_nil(),
"failed to create length-component for the left-hand-side");

exprt new_length=i_lhs.index();
make_type(new_length, i2.type());
exprt new_length =
typecast_exprt::conditional_cast(i_lhs.index(), i2.type());

if_exprt min_expr(binary_relation_exprt(new_length, ID_lt, i2),
new_length, i2);
Expand All @@ -1232,16 +1230,14 @@ goto_programt::targett string_abstractiont::abstract_char_assign(
i2.is_not_nil(),
"failed to create length-component for the left-hand-side");

make_type(ptr.offset, build_type(whatt::LENGTH));
return
char_assign(
dest,
target,
new_lhs,
i2,
ptr.offset.is_nil()?
from_integer(0, build_type(whatt::LENGTH)):
ptr.offset);
return char_assign(
dest,
target,
new_lhs,
i2,
ptr.offset.is_nil() ? from_integer(0, build_type(whatt::LENGTH))
: typecast_exprt::conditional_cast(
ptr.offset, build_type(whatt::LENGTH)));
}
}

Expand Down
7 changes: 0 additions & 7 deletions src/goto-programs/string_abstraction.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,13 +73,6 @@ class string_abstractiont

bool is_ptr_string_struct(const typet &type) const;

void make_type(exprt &dest, const typet &type)
{
if(dest.is_not_nil() &&
ns.follow(dest.type())!=ns.follow(type))
dest = typecast_exprt(dest, type);
}

goto_programt::targett abstract(
goto_programt &dest, goto_programt::targett it);
goto_programt::targett abstract_assign(
Expand Down
9 changes: 1 addition & 8 deletions src/goto-programs/string_instrumentation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,12 +64,6 @@ class string_instrumentationt
symbol_table_baset &symbol_table;
namespacet ns;

void make_type(exprt &dest, const typet &type)
{
if(ns.follow(dest.type())!=ns.follow(type))
dest = typecast_exprt(dest, type);
}

void instrument(goto_programt &dest, goto_programt::targett it);
void do_function_call(goto_programt &dest, goto_programt::targett target);

Expand Down Expand Up @@ -785,8 +779,7 @@ void string_instrumentationt::do_strerror(

// assign address
{
exprt rhs=ptr;
make_type(rhs, lhs.type());
exprt rhs = typecast_exprt::conditional_cast(ptr, lhs.type());
tmp.add(goto_programt::make_assignment(
code_assignt(lhs, rhs), it->source_location()));
}
Expand Down
23 changes: 10 additions & 13 deletions src/goto-programs/xml_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -253,21 +253,18 @@
{
result.name = "struct";

const typet &type = ns.follow(expr.type());
const struct_typet &struct_type =
expr.type().id() == ID_struct_tag
? ns.follow_tag(to_struct_tag_type(expr.type()))
: to_struct_type(expr.type());

Check warning on line 259 in src/goto-programs/xml_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/xml_expr.cpp#L259 

Added line #L259 was not covered by tests
const struct_typet::componentst &components = struct_type.components();
PRECONDITION(components.size() == expr.operands().size());

// these are expected to have a struct type
if(type.id() == ID_struct)
for(unsigned m = 0; m < expr.operands().size(); m++)
{
const struct_typet &struct_type = to_struct_type(type);
const struct_typet::componentst &components = struct_type.components();
PRECONDITION(components.size() == expr.operands().size());

for(unsigned m = 0; m < expr.operands().size(); m++)
{
xmlt &e = result.new_element("member");
e.new_element() = xml(expr.operands()[m], ns);
e.set_attribute("name", id2string(components[m].get_name()));
}
xmlt &e = result.new_element("member");
e.new_element() = xml(expr.operands()[m], ns);
e.set_attribute("name", id2string(components[m].get_name()));
}
}
else if(expr.id() == ID_union)
Expand Down
Loading