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 Feb 20, 2024
1 parent 1939544 commit 2ff2a46
Show file tree
Hide file tree
Showing 9 changed files with 61 additions and 39 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()));

// 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
6 changes: 5 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 ? ns.follow_tag(to_struct_tag_type(t))
: t.id() == ID_union_tag ? ns.follow_tag(to_union_tag_type(t))
: to_struct_union_type(t);

for(const auto &component : struct_type.components())
{
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));

for(const auto &comp : struct_type.components())
{
Expand Down
10 changes: 9 additions & 1 deletion src/analyses/variable-sensitivity/abstract_aggregate_object.h
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,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 @@ -225,8 +225,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
20 changes: 14 additions & 6 deletions src/analyses/variable-sensitivity/full_struct_abstract_object.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -6,15 +6,18 @@ Author: Thomas Kiley, [email protected]
\*******************************************************************/

#include <ostream>
#include "full_struct_abstract_object.h"

#include <analyses/variable-sensitivity/abstract_environment.h>
#include <util/c_types.h>
#include <util/std_expr.h>

#include "full_struct_abstract_object.h"
#include <analyses/variable-sensitivity/abstract_environment.h>

#include "location_update_visitor.h"
#include "map_visit.h"

#include <ostream>

// #define DEBUG

#ifdef DEBUG
Expand Down Expand Up @@ -43,9 +46,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 +209,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 ? ns.follow_tag(to_struct_tag_type(type()))
: type().id() == ID_union_tag ? ns.follow_tag(to_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 @@ -44,7 +44,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 @@ -149,52 +149,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 +208,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 2ff2a46

Please sign in to comment.