Skip to content

Commit

Permalink
analyses: Replace uses of namespacet::follow
Browse files Browse the repository at this point in the history
This is deprecated. Use suitable variants of `follow_tag` instead.
  • Loading branch information
tautschnig committed Mar 22, 2024
1 parent e7b0557 commit 5c0fd9b
Show file tree
Hide file tree
Showing 9 changed files with 67 additions and 43 deletions.
6 changes: 4 additions & 2 deletions src/analyses/custom_bitvector_analysis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -233,8 +233,10 @@ void custom_bitvector_domaint::assign_struct_rec(
{
if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag)
{
const struct_typet &struct_type=
to_struct_type(ns.follow(lhs.type()));
const struct_typet &struct_type =
lhs.type().id() == ID_struct
? to_struct_type(lhs.type())
: ns.follow_tag(to_struct_tag_type(lhs.type()));

Check warning on line 239 in src/analyses/custom_bitvector_analysis.cpp

View check run for this annotation

Codecov / codecov/patch

src/analyses/custom_bitvector_analysis.cpp#L236-L239

Added lines #L236 - L239 were not covered by tests

// assign member-by-member
for(const auto &c : struct_type.components())
Expand Down
10 changes: 7 additions & 3 deletions src/analyses/goto_rw.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -250,7 +250,9 @@ void rw_range_sett::get_objects_member(
return;
}

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

auto offset_bits =
member_offset_bits(struct_type, expr.get_component_name(), ns);
Expand Down Expand Up @@ -367,8 +369,10 @@ void rw_range_sett::get_objects_struct(
const range_spect &range_start,
const range_spect &size)
{
const struct_typet &struct_type=
to_struct_type(ns.follow(expr.type()));
const struct_typet &struct_type =
expr.type().id() == ID_struct
? to_struct_type(expr.type())
: ns.follow_tag(to_struct_tag_type(expr.type()));

auto struct_bits = pointer_offset_bits(struct_type, ns);

Expand Down
8 changes: 7 additions & 1 deletion src/analyses/invariant_propagation.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]

#include "invariant_propagation.h"

#include <util/c_types.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>

Expand Down Expand Up @@ -131,7 +132,10 @@ void invariant_propagationt::get_objects_rec(
t.id() == ID_struct || t.id() == ID_union || t.id() == ID_struct_tag ||
t.id() == ID_union_tag)
{
const struct_union_typet &struct_type = to_struct_union_type(ns.follow(t));
const struct_union_typet &struct_type =
(t.id() == ID_struct_tag || t.id() == ID_union_tag)
? ns.follow_struct_or_union_tag(to_struct_or_union_tag_type(t))
: to_struct_union_type(t);

Check warning on line 138 in src/analyses/invariant_propagation.cpp

View check run for this annotation

Codecov / codecov/patch

src/analyses/invariant_propagation.cpp#L135-L138

Added lines #L135 - L138 were not covered by tests

for(const auto &component : struct_type.components())
{
Expand Down Expand Up @@ -223,7 +227,9 @@ bool invariant_propagationt::check_type(const typet &type) const
else if(
type.id() == ID_struct || type.id() == ID_union ||
type.id() == ID_struct_tag || type.id() == ID_union_tag)
{
return false;
}
else if(type.id()==ID_array)
return false;
else if(type.id()==ID_unsignedbv ||
Expand Down
4 changes: 3 additions & 1 deletion src/analyses/invariant_set.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -474,7 +474,9 @@ void invariant_sett::strengthen_rec(const exprt &expr)

if(op_type.id() == ID_struct || op_type.id() == ID_struct_tag)
{
const struct_typet &struct_type = to_struct_type(ns.follow(op_type));
const struct_typet &struct_type =
op_type.id() == ID_struct ? to_struct_type(op_type)
: ns.follow_tag(to_struct_tag_type(op_type));

Check warning on line 479 in src/analyses/invariant_set.cpp

View check run for this annotation

Codecov / codecov/patch

src/analyses/invariant_set.cpp#L477-L479

Added lines #L477 - L479 were not covered by tests

for(const auto &comp : struct_type.components())
{
Expand Down
18 changes: 16 additions & 2 deletions src/analyses/variable-sensitivity/abstract_aggregate_object.h
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,13 @@ class abstract_aggregate_objectt : public abstract_objectt,
abstract_aggregate_objectt(const typet &type, bool tp, bool bttm)
: abstract_objectt(type, tp, bttm)
{
PRECONDITION(type.id() == aggregate_traitst::TYPE_ID());
PRECONDITION(
type.id() != ID_struct_tag || ID_struct == aggregate_traitst::TYPE_ID());
PRECONDITION(
type.id() != ID_union_tag || ID_union == aggregate_traitst::TYPE_ID());
PRECONDITION(
type.id() == ID_struct_tag || type.id() == ID_union_tag ||
type.id() == aggregate_traitst::TYPE_ID());
}

abstract_aggregate_objectt(
Expand All @@ -42,7 +48,15 @@ class abstract_aggregate_objectt : public abstract_objectt,
const namespacet &ns)
: abstract_objectt(expr, environment, ns)
{
PRECONDITION(ns.follow(expr.type()).id() == aggregate_traitst::TYPE_ID());
PRECONDITION(
expr.type().id() != ID_struct_tag ||
ID_struct == aggregate_traitst::TYPE_ID());
PRECONDITION(
expr.type().id() != ID_union_tag ||
ID_union == aggregate_traitst::TYPE_ID());
PRECONDITION(
expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag ||
expr.type().id() == aggregate_traitst::TYPE_ID());
}

abstract_object_pointert expression_transform(
Expand Down
9 changes: 3 additions & 6 deletions src/analyses/variable-sensitivity/abstract_environment.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -209,19 +209,16 @@ bool abstract_environmentt::assign(
final_value = value;
}

const typet &lhs_type = ns.follow(lhs_value->type());
const typet &rhs_type = ns.follow(final_value->type());

// Write the value for the root symbol back into the map
INVARIANT(
lhs_type == rhs_type,
lhs_value->type() == final_value->type(),
"Assignment types must match"
"\n"
"lhs_type :" +
lhs_type.pretty() +
lhs_value->type().pretty() +
"\n"
"rhs_type :" +
rhs_type.pretty());
final_value->type().pretty());

// If LHS was directly the symbol
if(s.id() == ID_symbol)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@

#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/std_expr.h>

Expand Down Expand Up @@ -225,8 +224,7 @@ abstract_object_pointert constant_pointer_abstract_objectt::write_dereference(
if(stack.empty())
{
// We should not be changing the type of an abstract object
PRECONDITION(
new_value->type() == ns.follow(to_pointer_type(type()).base_type()));
PRECONDITION(new_value->type() == to_pointer_type(type()).base_type());

// Get an expression that we can assign to
exprt value = to_address_of_expr(value_stack.to_expression()).object();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ full_struct_abstract_objectt::full_struct_abstract_objectt(
bool bottom)
: abstract_aggregate_baset(t, top, bottom)
{
PRECONDITION(t.id() == ID_struct);
PRECONDITION(t.id() == ID_struct || t.id() == ID_struct_tag);
DATA_INVARIANT(verify(), "Structural invariants maintained");
}

Expand All @@ -43,9 +43,11 @@ full_struct_abstract_objectt::full_struct_abstract_objectt(
const namespacet &ns)
: abstract_aggregate_baset(e, environment, ns)
{
PRECONDITION(ns.follow(e.type()).id() == ID_struct);
PRECONDITION(e.type().id() == ID_struct || e.type().id() == ID_struct_tag);

const struct_typet struct_type_def = to_struct_type(ns.follow(e.type()));
const struct_typet &struct_type_def =
e.type().id() == ID_struct ? to_struct_type(e.type())
: ns.follow_tag(to_struct_tag_type(e.type()));

bool did_initialize_values = false;
auto struct_type_it = struct_type_def.components().begin();
Expand Down Expand Up @@ -204,7 +206,10 @@ void full_struct_abstract_objectt::output(
// To ensure that a consistent ordering of fields is output, use
// the underlying type declaration for this struct to determine
// the ordering
struct_union_typet type_decl = to_struct_union_type(ns.follow(type()));
struct_union_typet type_decl =
(type().id() == ID_struct_tag || type().id() == ID_union_tag)
? ns.follow_struct_or_union_tag(to_struct_or_union_tag_type(type()))
: to_struct_union_type(type());

bool first = true;

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,6 @@

#include "variable_sensitivity_object_factory.h"

#include <util/namespace.h>

#include "constant_abstract_value.h"
#include "constant_pointer_abstract_object.h"
#include "data_dependency_context.h"
Expand Down Expand Up @@ -44,7 +42,7 @@ abstract_object_pointert create_abstract_object(
if(top || bottom)
return std::make_shared<abstract_object_classt>(type, top, bottom);

PRECONDITION(type == ns.follow(e.type()));
PRECONDITION(type == e.type());
return std::make_shared<abstract_object_classt>(e, environment, ns);
}

Expand Down Expand Up @@ -124,11 +122,11 @@ variable_sensitivity_object_factoryt::get_abstract_object_type(
{
return configuration.pointer_abstract_type;
}
else if(type.id() == ID_struct)
else if(type.id() == ID_struct || type.id() == ID_struct_tag)
{
return configuration.struct_abstract_type;
}
else if(type.id() == ID_union)
else if(type.id() == ID_union || type.id() == ID_union_tag)
{
return configuration.union_abstract_type;
}
Expand All @@ -149,52 +147,50 @@ variable_sensitivity_object_factoryt::get_abstract_object(
const abstract_environmentt &environment,
const namespacet &ns) const
{
const typet &followed_type = ns.follow(type);
ABSTRACT_OBJECT_TYPET abstract_object_type =
get_abstract_object_type(followed_type);
ABSTRACT_OBJECT_TYPET abstract_object_type = get_abstract_object_type(type);

switch(abstract_object_type)
{
case TWO_VALUE:
return initialize_abstract_object<abstract_objectt>(
followed_type, top, bottom, e, environment, ns, configuration);
type, top, bottom, e, environment, ns, configuration);
case CONSTANT:
return initialize_abstract_object<constant_abstract_valuet>(
followed_type, top, bottom, e, environment, ns, configuration);
type, top, bottom, e, environment, ns, configuration);
case INTERVAL:
return initialize_abstract_object<interval_abstract_valuet>(
followed_type, top, bottom, e, environment, ns, configuration);
type, top, bottom, e, environment, ns, configuration);
case VALUE_SET:
return initialize_abstract_object<value_set_abstract_objectt>(
followed_type, top, bottom, e, environment, ns, configuration);
type, top, bottom, e, environment, ns, configuration);

case ARRAY_INSENSITIVE:
return initialize_abstract_object<two_value_array_abstract_objectt>(
followed_type, top, bottom, e, environment, ns, configuration);
type, top, bottom, e, environment, ns, configuration);
case ARRAY_SENSITIVE:
return initialize_abstract_object<full_array_abstract_objectt>(
followed_type, top, bottom, e, environment, ns, configuration);
type, top, bottom, e, environment, ns, configuration);

case POINTER_INSENSITIVE:
return initialize_abstract_object<two_value_pointer_abstract_objectt>(
followed_type, top, bottom, e, environment, ns, configuration);
type, top, bottom, e, environment, ns, configuration);
case POINTER_SENSITIVE:
return initialize_abstract_object<constant_pointer_abstract_objectt>(
followed_type, top, bottom, e, environment, ns, configuration);
type, top, bottom, e, environment, ns, configuration);
case VALUE_SET_OF_POINTERS:
return initialize_abstract_object<value_set_pointer_abstract_objectt>(
followed_type, top, bottom, e, environment, ns, configuration);
type, top, bottom, e, environment, ns, configuration);

case STRUCT_INSENSITIVE:
return initialize_abstract_object<two_value_struct_abstract_objectt>(
followed_type, top, bottom, e, environment, ns, configuration);
type, top, bottom, e, environment, ns, configuration);
case STRUCT_SENSITIVE:
return initialize_abstract_object<full_struct_abstract_objectt>(
followed_type, top, bottom, e, environment, ns, configuration);
type, top, bottom, e, environment, ns, configuration);

case UNION_INSENSITIVE:
return initialize_abstract_object<two_value_union_abstract_objectt>(
followed_type, top, bottom, e, environment, ns, configuration);
type, top, bottom, e, environment, ns, configuration);

case HEAP_ALLOCATION:
{
Expand All @@ -210,7 +206,7 @@ variable_sensitivity_object_factoryt::get_abstract_object(
default:
UNREACHABLE;
return initialize_abstract_object<abstract_objectt>(
followed_type, top, bottom, e, environment, ns, configuration);
type, top, bottom, e, environment, ns, configuration);
}
}

Expand Down

0 comments on commit 5c0fd9b

Please sign in to comment.