Skip to content

Commit 5036706

Browse files
tautschnigtautschnig
authored
Merge pull request #3763 from tautschnig/no-follow-pointer-analyses
Remove unnecessary use of ns.follow in pointer-analysis/
2 parents b03eb7a + 8cb0481 commit 5036706

File tree

6 files changed

+36
-42
lines changed

6 files changed

+36
-42
lines changed

‎src/pointer-analysis/value_set.cpp

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ bool value_sett::field_sensitive(
4848
return true;
4949

5050
// otherwise it has to be a struct
51-
return ns.follow(type).id()==ID_struct;
51+
return type.id() == ID_struct || type.id() == ID_struct_tag;
5252
}
5353

5454
const value_sett::entryt *value_sett::find_entry(const value_sett::idt &id)
@@ -397,7 +397,7 @@ void value_sett::get_value_set_rec(
397397
{
398398
assert(expr.operands().size()==2);
399399

400-
const typet &type=ns.follow(expr.op0().type());
400+
const typet &type = expr.op0().type();
401401

402402
DATA_INVARIANT(
403403
type.id() == ID_array, "operand 0 of index expression must be an array");
@@ -548,7 +548,7 @@ void value_sett::get_value_set_rec(
548548

549549
// let's see what gets converted to what
550550

551-
const typet &op_type=ns.follow(expr.op0().type());
551+
const typet &op_type = expr.op0().type();
552552

553553
if(op_type.id()==ID_pointer)
554554
{
@@ -1033,7 +1033,7 @@ void value_sett::get_reference_set_rec(
10331033
const index_exprt &index_expr=to_index_expr(expr);
10341034
const exprt &array=index_expr.array();
10351035
const exprt &offset=index_expr.index();
1036-
const typet &array_type=ns.follow(array.type());
1036+
const typet &array_type = array.type();
10371037

10381038
DATA_INVARIANT(
10391039
array_type.id() == ID_array, "index takes array-typed operand");
@@ -1340,7 +1340,7 @@ void value_sett::assign_rec(
13401340
if(lhs.operands().size()!=2)
13411341
throw "index expected to have two operands";
13421342

1343-
const typet &type=ns.follow(lhs.op0().type());
1343+
const typet &type = lhs.op0().type();
13441344

13451345
DATA_INVARIANT(
13461346
type.id() == ID_array, "operand 0 of index expression must be an array");
@@ -1493,11 +1493,11 @@ void value_sett::apply_code_rec(
14931493
if(lhs.id()!=ID_symbol)
14941494
throw "decl expected to have symbol on lhs";
14951495

1496-
const typet &lhs_type=ns.follow(lhs.type());
1496+
const typet &lhs_type = lhs.type();
14971497

1498-
if(lhs_type.id()==ID_pointer ||
1499-
(lhs_type.id()==ID_array &&
1500-
ns.follow(lhs_type.subtype()).id()==ID_pointer))
1498+
if(
1499+
lhs_type.id() == ID_pointer ||
1500+
(lhs_type.id() == ID_array && lhs_type.subtype().id() == ID_pointer))
15011501
{
15021502
// assign the address of the failed object
15031503
exprt failed=get_failed_symbol(to_symbol_expr(lhs), ns);

‎src/pointer-analysis/value_set_dereference.cpp

Lines changed: 9 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -272,8 +272,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
272272
const exprt &what,
273273
const exprt &pointer_expr)
274274
{
275-
const typet &dereference_type=
276-
ns.follow(pointer_expr.type()).subtype();
275+
const typet &dereference_type = pointer_expr.type().subtype();
277276

278277
if(what.id()==ID_unknown ||
279278
what.id()==ID_invalid)
@@ -334,28 +333,25 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
334333
const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory");
335334
const symbol_exprt symbol_expr(memory_symbol.name, memory_symbol.type);
336335

337-
if(base_type_eq(
338-
ns.follow(memory_symbol.type).subtype(),
339-
dereference_type, ns))
336+
if(base_type_eq(memory_symbol.type.subtype(), dereference_type, ns))
340337
{
341338
// Types match already, what a coincidence!
342339
// We can use an index expression.
343340

344341
const index_exprt index_expr(
345342
symbol_expr,
346343
pointer_offset(pointer_expr),
347-
ns.follow(memory_symbol.type).subtype());
344+
memory_symbol.type.subtype());
348345

349346
result.value=index_expr;
350347
}
351348
else if(dereference_type_compare(
352-
ns.follow(memory_symbol.type).subtype(),
353-
dereference_type))
349+
memory_symbol.type.subtype(), dereference_type))
354350
{
355351
const index_exprt index_expr(
356352
symbol_expr,
357353
pointer_offset(pointer_expr),
358-
ns.follow(memory_symbol.type).subtype());
354+
memory_symbol.type.subtype());
359355
result.value=typecast_exprt(index_expr, dereference_type);
360356
}
361357
else
@@ -592,10 +588,10 @@ bool value_set_dereferencet::memory_model_bytes(
592588
auto to_type_size = pointer_offset_size(to_type, ns);
593589

594590
if(
595-
ns.follow(from_type).id() == ID_array &&
596-
from_type_subtype_size.has_value() && *from_type_subtype_size == 1 &&
597-
to_type_size.has_value() && *to_type_size == 1 &&
598-
is_a_bv_type(ns.follow(from_type).subtype()) && is_a_bv_type(to_type))
591+
from_type.id() == ID_array && from_type_subtype_size.has_value() &&
592+
*from_type_subtype_size == 1 && to_type_size.has_value() &&
593+
*to_type_size == 1 && is_a_bv_type(ns.follow(from_type).subtype()) &&
594+
is_a_bv_type(to_type))
599595
{
600596
// yes, can use 'index'
601597
result=index_exprt(value, offset, ns.follow(from_type).subtype());

‎src/pointer-analysis/value_set_fi.cpp

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -407,7 +407,7 @@ void value_set_fit::get_value_set_rec(
407407
{
408408
assert(expr.operands().size()==2);
409409

410-
const typet &type=ns.follow(expr.op0().type());
410+
const typet &type = expr.op0().type();
411411

412412
DATA_INVARIANT(type.id()==ID_array ||
413413
type.id()=="#REF#",
@@ -852,7 +852,7 @@ void value_set_fit::get_reference_set_sharing_rec(
852852

853853
const exprt &array=expr.op0();
854854
const exprt &offset=expr.op1();
855-
const typet &array_type=ns.follow(array.type());
855+
const typet &array_type = array.type();
856856

857857
DATA_INVARIANT(
858858
array_type.id() == ID_array, "index takes array-typed operand");
@@ -874,8 +874,7 @@ void value_set_fit::get_reference_set_sharing_rec(
874874
object, from_integer(0, index_type()), expr.type());
875875

876876
// adjust type?
877-
if(object.type().id()!="#REF#" &&
878-
ns.follow(object.type())!=array_type)
877+
if(object.type().id() != "#REF#" && object.type() != array_type)
879878
index_expr.make_typecast(array.type());
880879

881880
offsett o = a_it->second;
@@ -1197,7 +1196,7 @@ void value_set_fit::assign_rec(
11971196
if(lhs.operands().size()!=2)
11981197
throw "index expected to have two operands";
11991198

1200-
const typet &type=ns.follow(lhs.op0().type());
1199+
const typet &type = lhs.op0().type();
12011200

12021201
DATA_INVARIANT(type.id()==ID_array ||
12031202
type.id()=="#REF#",

‎src/pointer-analysis/value_set_fivr.cpp

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -519,7 +519,7 @@ void value_set_fivrt::get_value_set_rec(
519519
{
520520
assert(expr.operands().size()==2);
521521

522-
const typet &type=ns.follow(expr.op0().type());
522+
const typet &type = expr.op0().type();
523523

524524
DATA_INVARIANT(type.id()==ID_array ||
525525
type.id()=="#REF#",
@@ -963,7 +963,7 @@ void value_set_fivrt::get_reference_set_sharing_rec(
963963

964964
const exprt &array=expr.op0();
965965
const exprt &offset=expr.op1();
966-
const typet &array_type=ns.follow(array.type());
966+
const typet &array_type = array.type();
967967

968968
DATA_INVARIANT(
969969
array_type.id() == ID_array, "index takes array-typed operand");
@@ -985,8 +985,7 @@ void value_set_fivrt::get_reference_set_sharing_rec(
985985
object, from_integer(0, index_type()), expr.type());
986986

987987
// adjust type?
988-
if(object.type().id()!="#REF#" &&
989-
ns.follow(object.type())!=array_type)
988+
if(object.type().id() != "#REF#" && object.type() != array_type)
990989
index_expr.make_typecast(array.type());
991990

992991
offsett o = a_it->second;
@@ -1328,7 +1327,7 @@ void value_set_fivrt::assign_rec(
13281327
if(lhs.operands().size()!=2)
13291328
throw "index expected to have two operands";
13301329

1331-
const typet &type=ns.follow(lhs.op0().type());
1330+
const typet &type = lhs.op0().type();
13321331

13331332
DATA_INVARIANT(type.id()==ID_array ||
13341333
type.id()=="#REF#",

‎src/pointer-analysis/value_set_fivrns.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -314,7 +314,7 @@ void value_set_fivrnst::get_value_set_rec(
314314
{
315315
assert(expr.operands().size()==2);
316316

317-
const typet &type=ns.follow(expr.op0().type());
317+
const typet &type = expr.op0().type();
318318

319319
DATA_INVARIANT(
320320
type.id() == ID_array, "operand 0 of index expression must be an array");
@@ -656,7 +656,7 @@ void value_set_fivrnst::get_reference_set_rec(
656656

657657
const exprt &array=expr.op0();
658658
const exprt &offset=expr.op1();
659-
const typet &array_type=ns.follow(array.type());
659+
const typet &array_type = array.type();
660660

661661
DATA_INVARIANT(
662662
array_type.id() == ID_array, "index takes array-typed operand");
@@ -678,7 +678,7 @@ void value_set_fivrnst::get_reference_set_rec(
678678
object, from_integer(0, index_type()), expr.type());
679679

680680
// adjust type?
681-
if(ns.follow(object.type())!=array_type)
681+
if(object.type() != array_type)
682682
index_expr.make_typecast(array.type());
683683

684684
offsett o = a_it->second;
@@ -990,7 +990,7 @@ void value_set_fivrnst::assign_rec(
990990
if(lhs.operands().size()!=2)
991991
throw "index expected to have two operands";
992992

993-
const typet &type=ns.follow(lhs.op0().type());
993+
const typet &type = lhs.op0().type();
994994

995995
DATA_INVARIANT(
996996
type.id() == ID_array, "operand 0 of index expression must be an array");

‎unit/pointer-analysis/value_set.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -62,12 +62,12 @@ SCENARIO(
6262
A_x.set_name("x");
6363
A_x.set_base_name("x");
6464
A_x.set_pretty_name("x");
65-
A_x.type() = pointer_typet(symbol_typet(A_symbol.name), 64);
65+
A_x.type() = pointer_typet(struct_tag_typet(A_symbol.name), 64);
6666

6767
A_y.set_name("y");
6868
A_y.set_base_name("y");
6969
A_y.set_pretty_name("y");
70-
A_y.type() = pointer_typet(symbol_typet(A_symbol.name), 64);
70+
A_y.type() = pointer_typet(struct_tag_typet(A_symbol.name), 64);
7171

7272
A_symbol.type = struct_A;
7373
symbol_table.add(A_symbol);
@@ -78,23 +78,23 @@ SCENARIO(
7878
a1_symbol.name = "a1";
7979
a1_symbol.base_name = "a1";
8080
a1_symbol.pretty_name = "a1";
81-
a1_symbol.type = symbol_typet(A_symbol.name);
81+
a1_symbol.type = struct_tag_typet(A_symbol.name);
8282
a1_symbol.is_static_lifetime = true;
8383
symbol_table.add(a1_symbol);
8484

8585
symbolt a2_symbol;
8686
a2_symbol.name = "a2";
8787
a2_symbol.base_name = "a2";
8888
a2_symbol.pretty_name = "a2";
89-
a2_symbol.type = symbol_typet(A_symbol.name);
89+
a2_symbol.type = struct_tag_typet(A_symbol.name);
9090
a2_symbol.is_static_lifetime = true;
9191
symbol_table.add(a2_symbol);
9292

9393
symbolt a3_symbol;
9494
a3_symbol.name = "a3";
9595
a3_symbol.base_name = "a3";
9696
a3_symbol.pretty_name = "a3";
97-
a3_symbol.type = symbol_typet(A_symbol.name);
97+
a3_symbol.type = struct_tag_typet(A_symbol.name);
9898
a3_symbol.is_static_lifetime = true;
9999
symbol_table.add(a3_symbol);
100100

@@ -211,7 +211,7 @@ SCENARIO(
211211

212212
WHEN("We query what '{ .x = &a2, .y = &a3 }.x' points to")
213213
{
214-
struct_exprt struct_constant(symbol_typet(A_symbol.name));
214+
struct_exprt struct_constant(struct_tag_typet(A_symbol.name));
215215
struct_constant.copy_to_operands(
216216
address_of_exprt(a2_symbol.symbol_expr()));
217217
struct_constant.copy_to_operands(

0 commit comments

Comments
 (0)