Skip to content

Commit 0202f34

Browse files
kroeningkroening
committed
refactor pointer_validity_check using address_check
1 parent 4a24ad4 commit 0202f34

File tree

1 file changed

+60
-202
lines changed

1 file changed

+60
-202
lines changed

‎src/analyses/goto_check.cpp‎

Lines changed: 60 additions & 202 deletions
Original file line numberDiff line numberDiff line change
@@ -13,20 +13,21 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <algorithm>
1515

16-
#include <util/simplify_expr.h>
17-
#include <util/array_name.h>
18-
#include <util/ieee_float.h>
1916
#include <util/arith_tools.h>
17+
#include <util/array_name.h>
18+
#include <util/base_type.h>
19+
#include <util/cprover_prefix.h>
20+
#include <util/c_types.h>
2021
#include <util/expr_util.h>
2122
#include <util/find_symbols.h>
22-
#include <util/std_expr.h>
23-
#include <util/std_types.h>
2423
#include <util/guard.h>
25-
#include <util/base_type.h>
24+
#include <util/ieee_float.h>
25+
#include <util/options.h>
2626
#include <util/pointer_offset_size.h>
2727
#include <util/pointer_predicates.h>
28-
#include <util/cprover_prefix.h>
29-
#include <util/options.h>
28+
#include <util/simplify_expr.h>
29+
#include <util/std_expr.h>
30+
#include <util/std_types.h>
3031

3132
#include <langapi/language.h>
3233
#include <langapi/mode.h>
@@ -99,25 +100,21 @@ class goto_checkt
99100

100101
using conditionst = std::list<conditiont>;
101102

102-
void bounds_check(const index_exprt &expr, const guardt &guard);
103-
void div_by_zero_check(const div_exprt &expr, const guardt &guard);
104-
void mod_by_zero_check(const mod_exprt &expr, const guardt &guard);
105-
void undefined_shift_check(const shift_exprt &expr, const guardt &guard);
106-
void pointer_rel_check(const exprt &expr, const guardt &guard);
107-
void pointer_overflow_check(const exprt &expr, const guardt &guard);
108-
void pointer_validity_check(
109-
const dereference_exprt &expr,
110-
const guardt &guard,
111-
const exprt &access_lb,
112-
const exprt &access_ub);
103+
void bounds_check(const index_exprt &, const guardt &);
104+
void div_by_zero_check(const div_exprt &, const guardt &);
105+
void mod_by_zero_check(const mod_exprt &, const guardt &);
106+
void undefined_shift_check(const shift_exprt &, const guardt &);
107+
void pointer_rel_check(const exprt &, const guardt &);
108+
void pointer_overflow_check(const exprt &, const guardt &);
109+
void pointer_validity_check(const dereference_exprt &, const guardt &);
113110
conditionst address_check(const exprt &address, const exprt &size);
114-
void integer_overflow_check(const exprt &expr, const guardt &guard);
115-
void conversion_check(const exprt &expr, const guardt &guard);
116-
void float_overflow_check(const exprt &expr, const guardt &guard);
117-
void nan_check(const exprt &expr, const guardt &guard);
118-
void rw_ok_check(exprt &expr);
111+
void integer_overflow_check(const exprt &, const guardt &);
112+
void conversion_check(const exprt &, const guardt &);
113+
void float_overflow_check(const exprt &, const guardt &);
114+
void nan_check(const exprt &, const guardt &);
115+
void rw_ok_check(exprt &);
119116

120-
std::string array_name(const exprt &expr);
117+
std::string array_name(const exprt &);
121118

122119
void add_guarded_claim(
123120
const exprt &expr,
@@ -935,177 +932,25 @@ void goto_checkt::pointer_overflow_check(
935932

936933
void goto_checkt::pointer_validity_check(
937934
const dereference_exprt &expr,
938-
const guardt &guard,
939-
const exprt &access_lb,
940-
const exprt &access_ub)
935+
const guardt &guard)
941936
{
942937
if(!enable_pointer_check)
943938
return;
944939

945-
const exprt &pointer=expr.op0();
946-
const pointer_typet &pointer_type=
947-
to_pointer_type(ns.follow(pointer.type()));
948-
949-
assert(base_type_eq(pointer_type.subtype(), expr.type(), ns));
940+
const exprt &pointer=expr.pointer();
950941

951-
local_bitvector_analysist::flagst flags=
952-
local_bitvector_analysis->get(t, pointer);
953-
954-
// For Java, we only need to check for null
955-
if(mode==ID_java)
956-
{
957-
if(flags.is_unknown() || flags.is_null())
958-
{
959-
notequal_exprt not_eq_null(pointer, null_pointer_exprt(pointer_type));
942+
auto conditions =
943+
address_check(pointer, size_of_expr(expr.type(), ns));
960944

961-
add_guarded_claim(
962-
not_eq_null,
963-
"reference is null",
964-
"pointer dereference",
965-
expr.find_source_location(),
966-
expr,
967-
guard);
968-
}
969-
}
970-
else
945+
for(const auto &c : conditions)
971946
{
972-
exprt allocs=false_exprt();
973-
974-
if(!allocations.empty())
975-
{
976-
exprt::operandst disjuncts;
977-
978-
for(const auto &a : allocations)
979-
{
980-
typecast_exprt int_ptr(pointer, a.first.type());
981-
982-
exprt lb(int_ptr);
983-
if(access_lb.is_not_nil())
984-
{
985-
if(!base_type_eq(lb.type(), access_lb.type(), ns))
986-
lb=plus_exprt(lb, typecast_exprt(access_lb, lb.type()));
987-
else
988-
lb=plus_exprt(lb, access_lb);
989-
}
990-
991-
binary_relation_exprt lb_check(a.first, ID_le, lb);
992-
993-
exprt ub(int_ptr);
994-
if(access_ub.is_not_nil())
995-
{
996-
if(!base_type_eq(ub.type(), access_ub.type(), ns))
997-
ub=plus_exprt(ub, typecast_exprt(access_ub, ub.type()));
998-
else
999-
ub=plus_exprt(ub, access_ub);
1000-
}
1001-
1002-
binary_relation_exprt ub_check(
1003-
ub, ID_le, plus_exprt(a.first, a.second));
1004-
1005-
disjuncts.push_back(and_exprt(lb_check, ub_check));
1006-
}
1007-
1008-
allocs=disjunction(disjuncts);
1009-
}
1010-
1011-
if(flags.is_unknown() ||
1012-
flags.is_null())
1013-
{
1014-
add_guarded_claim(
1015-
or_exprt(allocs, not_exprt(null_pointer(pointer))),
1016-
"dereference failure: pointer NULL",
1017-
"pointer dereference",
1018-
expr.find_source_location(),
1019-
expr,
1020-
guard);
1021-
}
1022-
1023-
if(flags.is_unknown())
1024-
add_guarded_claim(
1025-
or_exprt(allocs, not_exprt(invalid_pointer(pointer))),
1026-
"dereference failure: pointer invalid",
1027-
"pointer dereference",
1028-
expr.find_source_location(),
1029-
expr,
1030-
guard);
1031-
1032-
if(flags.is_uninitialized())
1033-
add_guarded_claim(
1034-
or_exprt(allocs, not_exprt(invalid_pointer(pointer))),
1035-
"dereference failure: pointer uninitialized",
1036-
"pointer dereference",
1037-
expr.find_source_location(),
1038-
expr,
1039-
guard);
1040-
1041-
if(flags.is_unknown() ||
1042-
flags.is_dynamic_heap())
1043-
add_guarded_claim(
1044-
or_exprt(allocs, not_exprt(deallocated(pointer, ns))),
1045-
"dereference failure: deallocated dynamic object",
1046-
"pointer dereference",
1047-
expr.find_source_location(),
1048-
expr,
1049-
guard);
1050-
1051-
if(flags.is_unknown() ||
1052-
flags.is_dynamic_local())
1053-
add_guarded_claim(
1054-
or_exprt(allocs, not_exprt(dead_object(pointer, ns))),
1055-
"dereference failure: dead object",
1056-
"pointer dereference",
1057-
expr.find_source_location(),
1058-
expr,
1059-
guard);
1060-
1061-
if(flags.is_unknown() ||
1062-
flags.is_dynamic_heap())
1063-
{
1064-
const or_exprt dynamic_bounds(
1065-
dynamic_object_lower_bound(pointer, ns, access_lb),
1066-
dynamic_object_upper_bound(pointer, ns, access_ub));
1067-
1068-
add_guarded_claim(
1069-
or_exprt(
1070-
allocs,
1071-
implies_exprt(
1072-
malloc_object(pointer, ns),
1073-
not_exprt(dynamic_bounds))),
1074-
"dereference failure: pointer outside dynamic object bounds",
1075-
"pointer dereference",
1076-
expr.find_source_location(),
1077-
expr,
1078-
guard);
1079-
}
1080-
1081-
if(flags.is_unknown() ||
1082-
flags.is_dynamic_local() ||
1083-
flags.is_static_lifetime())
1084-
{
1085-
const or_exprt object_bounds(
1086-
object_lower_bound(pointer, ns, access_lb),
1087-
object_upper_bound(pointer, ns, access_ub));
1088-
1089-
add_guarded_claim(
1090-
or_exprt(allocs, dynamic_object(pointer), not_exprt(object_bounds)),
1091-
"dereference failure: pointer outside object bounds",
1092-
"pointer dereference",
1093-
expr.find_source_location(),
1094-
expr,
1095-
guard);
1096-
}
1097-
1098-
if(flags.is_unknown() ||
1099-
flags.is_integer_address())
1100-
{
1101-
add_guarded_claim(
1102-
implies_exprt(integer_address(pointer), allocs),
1103-
"dereference failure: invalid integer address",
1104-
"pointer dereference",
1105-
expr.find_source_location(),
1106-
expr,
1107-
guard);
1108-
}
947+
add_guarded_claim(
948+
c.assertion,
949+
"dereference failure: "+c.description,
950+
"pointer dereference",
951+
expr.find_source_location(),
952+
expr,
953+
guard);
1109954
}
1110955
}
1111956

@@ -1207,7 +1052,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
12071052

12081053
conditions.push_back(conditiont(
12091054
implies_exprt(not_exprt(dynamic_object(address)), not_exprt(object_bounds_violation)),
1210-
"dereference failure: pointer outside object bounds"));
1055+
"pointer outside object bounds"));
12111056
}
12121057

12131058
if(flags.is_unknown() || flags.is_integer_address())
@@ -1547,24 +1392,39 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
15471392
const dereference_exprt &deref=
15481393
to_dereference_expr(member.struct_op());
15491394

1550-
check_rec(deref.op0(), guard, false);
1395+
check_rec(deref.pointer(), guard, false);
15511396

15521397
// avoid building the following expressions when pointer_validity_check
15531398
// would return immediately anyway
15541399
if(!enable_pointer_check)
15551400
return;
15561401

1557-
exprt access_ub=nil_exprt();
1402+
// we rewrite s->member into *(s+member_offset)
1403+
// to avoid requiring memory safety of the entire struct
15581404

15591405
exprt member_offset=member_offset_expr(member, ns);
1560-
exprt size=size_of_expr(expr.type(), ns);
15611406

1562-
if(member_offset.is_not_nil() && size.is_not_nil())
1563-
access_ub=plus_exprt(member_offset, size);
1407+
if(member_offset.is_not_nil())
1408+
{
1409+
pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
1410+
new_pointer_type.subtype() = expr.type();
15641411

1565-
pointer_validity_check(deref, guard, member_offset, access_ub);
1412+
const exprt char_pointer =
1413+
typecast_exprt::conditional_cast(
1414+
deref.pointer(), pointer_type(char_type()));
15661415

1567-
return;
1416+
const exprt new_address = typecast_exprt(
1417+
plus_exprt(char_pointer, member_offset), char_pointer.type());
1418+
1419+
const exprt new_address_casted =
1420+
typecast_exprt::conditional_cast(new_address, new_pointer_type);
1421+
1422+
dereference_exprt new_deref(new_address_casted, expr.type());
1423+
new_deref.add_source_location() = deref.source_location();
1424+
pointer_validity_check(new_deref, guard);
1425+
1426+
return;
1427+
}
15681428
}
15691429

15701430
forall_operands(it, expr)
@@ -1626,11 +1486,9 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
16261486
expr.id()==ID_ge || expr.id()==ID_gt)
16271487
pointer_rel_check(expr, guard);
16281488
else if(expr.id()==ID_dereference)
1629-
pointer_validity_check(
1630-
to_dereference_expr(expr),
1631-
guard,
1632-
nil_exprt(),
1633-
size_of_expr(expr.type(), ns));
1489+
{
1490+
pointer_validity_check(to_dereference_expr(expr), guard);
1491+
}
16341492
}
16351493

16361494
void goto_checkt::check(const exprt &expr)

0 commit comments

Comments
 (0)