Skip to content

Commit 35cc503

Browse files
tautschnigtautschnig
committed
Remove void* pointer arithmetic support from back-ends
The semantics thereof are set by GCC, so we should fix this up in the front-end. This also avoids repeating the same code in multiple places in the back-ends.
1 parent d158216 commit 35cc503

File tree

7 files changed

+72
-123
lines changed

7 files changed

+72
-123
lines changed

‎regression/cbmc/ptr_arithmetic_on_null/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
CORE gcc-only
22
main.c
33

4-
^\[main.assertion.1\] line .* assertion \(void \*\)0 != \(void \*\)0 \+ \(.*\)1: SUCCESS$
5-
^\[main.assertion.2\] line .* assertion \(void \*\)0 != \(void \*\)0 - \(.*\)1: SUCCESS$
6-
^\[main.assertion.3\] line .* assertion \(void \*\)0 != \(void \*\)0 \+ \(.*\)offset: SUCCESS$
7-
^\[main.assertion.4\] line .* assertion \(void \*\)0 - \(void \*\)0 == \(.*\)0: SUCCESS$
4+
^\[main.assertion.1\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 \+ \(.*\)1: SUCCESS$
5+
^\[main.assertion.2\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 - \(.*\)1: SUCCESS$
6+
^\[main.assertion.3\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 \+ \(.*\)offset: SUCCESS$
7+
^\[main.assertion.4\] line .* assertion \(char \*\)\(void \*\)0 - \(char \*\)\(void \*\)0 == \(.*\)0: SUCCESS$
88
^\[main.assertion.5\] line .* assertion ptr - \(signed int \*\)\(void \*\)0 == \(.*\)0: FAILURE$
99
^\[main.assertion.6\] line .* assertion \(ptr - \(.*\)1\) \+ \(.*\)1 == \(\(.* \*\)NULL\): SUCCESS$
1010
^\[main.assertion.7\] line .* assertion \(ptr - \(.*\)1\) \+ \(.*\)1 == \(\(.* \*\)NULL\): FAILURE$

‎src/ansi-c/c_typecheck_base.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -196,7 +196,7 @@ class c_typecheck_baset:
196196
virtual void typecheck_expr_binary_arithmetic(exprt &expr);
197197
virtual void typecheck_expr_shifts(shift_exprt &expr);
198198
virtual void typecheck_expr_pointer_arithmetic(exprt &expr);
199-
virtual void typecheck_arithmetic_pointer(const exprt &expr);
199+
virtual void typecheck_arithmetic_pointer(exprt &expr);
200200
virtual void typecheck_expr_binary_boolean(exprt &expr);
201201
virtual void typecheck_expr_trinary(if_exprt &expr);
202202
virtual void typecheck_expr_address_of(exprt &expr);

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1893,8 +1893,8 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr)
18931893
}
18941894
else if(type0.id() == ID_pointer)
18951895
{
1896-
expr.type()=type0;
1897-
typecheck_arithmetic_pointer(op0);
1896+
typecheck_arithmetic_pointer(to_unary_expr(expr).op());
1897+
expr.type() = to_unary_expr(expr).op().type();
18981898
}
18991899
else
19001900
{
@@ -4123,7 +4123,7 @@ void c_typecheck_baset::typecheck_expr_shifts(shift_exprt &expr)
41234123
throw 0;
41244124
}
41254125

4126-
void c_typecheck_baset::typecheck_arithmetic_pointer(const exprt &expr)
4126+
void c_typecheck_baset::typecheck_arithmetic_pointer(exprt &expr)
41274127
{
41284128
const typet &type=expr.type();
41294129
PRECONDITION(type.id() == ID_pointer);
@@ -4154,6 +4154,13 @@ void c_typecheck_baset::typecheck_arithmetic_pointer(const exprt &expr)
41544154
error() << "pointer arithmetic with unknown object size" << eom;
41554155
throw 0;
41564156
}
4157+
else if(base_type.id() == ID_empty)
4158+
{
4159+
// This is a gcc extension.
4160+
// https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
4161+
typecast_exprt tc{expr, pointer_type(char_type())};
4162+
expr.swap(tc);
4163+
}
41574164
}
41584165

41594166
void c_typecheck_baset::typecheck_expr_pointer_arithmetic(exprt &expr)
@@ -4192,7 +4199,7 @@ void c_typecheck_baset::typecheck_expr_pointer_arithmetic(exprt &expr)
41924199
{
41934200
typecheck_arithmetic_pointer(op0);
41944201
make_index_type(op1);
4195-
expr.type()=type0;
4202+
expr.type() = op0.type();
41964203
return;
41974204
}
41984205
}

‎src/cprover/bv_pointers_wide.cpp

Lines changed: 22 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -414,19 +414,12 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
414414
CHECK_RETURN(bv.size() == bits);
415415

416416
typet pointer_base_type = to_pointer_type(op.type()).base_type();
417-
418-
if(pointer_base_type.id() == ID_empty)
419-
{
420-
// This is a gcc extension.
421-
// https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
422-
size = 1;
423-
}
424-
else
425-
{
426-
auto size_opt = pointer_offset_size(pointer_base_type, ns);
427-
CHECK_RETURN(size_opt.has_value() && *size_opt >= 0);
428-
size = *size_opt;
429-
}
417+
DATA_INVARIANT(
418+
pointer_base_type.id() != ID_empty,
419+
"no pointer arithmetic over void pointers");
420+
auto size_opt = pointer_offset_size(pointer_base_type, ns);
421+
CHECK_RETURN(size_opt.has_value() && *size_opt >= 0);
422+
size = *size_opt;
430423
}
431424
}
432425

@@ -484,22 +477,12 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
484477

485478
typet pointer_base_type =
486479
to_pointer_type(minus_expr.lhs().type()).base_type();
487-
mp_integer element_size;
488-
489-
if(pointer_base_type.id() == ID_empty)
490-
{
491-
// This is a gcc extension.
492-
// https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
493-
element_size = 1;
494-
}
495-
else
496-
{
497-
auto element_size_opt = pointer_offset_size(pointer_base_type, ns);
498-
CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
499-
element_size = *element_size_opt;
500-
}
501-
502-
return offset_arithmetic(type, bv, element_size, neg_op1);
480+
DATA_INVARIANT(
481+
pointer_base_type.id() != ID_empty,
482+
"no pointer arithmetic over void pointers");
483+
auto element_size_opt = pointer_offset_size(pointer_base_type, ns);
484+
CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
485+
return offset_arithmetic(type, bv, *element_size_opt, neg_op1);
503486
}
504487
else if(
505488
expr.id() == ID_byte_extract_little_endian ||
@@ -631,21 +614,17 @@ bvt bv_pointers_widet::convert_bitvector(const exprt &expr)
631614

632615
bvt difference = bv_utils.sub(lhs_offset, rhs_offset);
633616

634-
// Support for void* is a gcc extension, with the size treated as 1 byte
635-
// (no division required below).
636-
// https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
637-
if(lhs_pt.base_type().id() != ID_empty)
638-
{
639-
auto element_size_opt = pointer_offset_size(lhs_pt.base_type(), ns);
640-
CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
617+
DATA_INVARIANT(
618+
lhs_pt.base_type().id() != ID_empty,
619+
"no pointer arithmetic over void pointers");
620+
auto element_size_opt = pointer_offset_size(lhs_pt.base_type(), ns);
621+
CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
641622

642-
if(*element_size_opt != 1)
643-
{
644-
bvt element_size_bv =
645-
bv_utils.build_constant(*element_size_opt, width);
646-
difference = bv_utils.divider(
647-
difference, element_size_bv, bv_utilst::representationt::SIGNED);
648-
}
623+
if(*element_size_opt != 1)
624+
{
625+
bvt element_size_bv = bv_utils.build_constant(*element_size_opt, width);
626+
difference = bv_utils.divider(
627+
difference, element_size_bv, bv_utilst::representationt::SIGNED);
649628
}
650629

651630
prop.l_set_to_true(prop.limplies(

‎src/solvers/flattening/bv_pointers.cpp

Lines changed: 22 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -447,19 +447,12 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
447447
CHECK_RETURN(bv.size()==bits);
448448

449449
typet pointer_base_type = to_pointer_type(op.type()).base_type();
450-
451-
if(pointer_base_type.id() == ID_empty)
452-
{
453-
// This is a gcc extension.
454-
// https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
455-
size = 1;
456-
}
457-
else
458-
{
459-
auto size_opt = pointer_offset_size(pointer_base_type, ns);
460-
CHECK_RETURN(size_opt.has_value() && *size_opt >= 0);
461-
size = *size_opt;
462-
}
450+
DATA_INVARIANT(
451+
pointer_base_type.id() != ID_empty,
452+
"no pointer arithmetic over void pointers");
453+
auto size_opt = pointer_offset_size(pointer_base_type, ns);
454+
CHECK_RETURN(size_opt.has_value() && *size_opt >= 0);
455+
size = *size_opt;
463456
}
464457
}
465458

@@ -519,22 +512,12 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
519512

520513
typet pointer_base_type =
521514
to_pointer_type(minus_expr.lhs().type()).base_type();
522-
mp_integer element_size;
523-
524-
if(pointer_base_type.id() == ID_empty)
525-
{
526-
// This is a gcc extension.
527-
// https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
528-
element_size = 1;
529-
}
530-
else
531-
{
532-
auto element_size_opt = pointer_offset_size(pointer_base_type, ns);
533-
CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
534-
element_size = *element_size_opt;
535-
}
536-
537-
return offset_arithmetic(type, bv, element_size, neg_op1);
515+
DATA_INVARIANT(
516+
pointer_base_type.id() != ID_empty,
517+
"no pointer arithmetic over void pointers");
518+
auto element_size_opt = pointer_offset_size(pointer_base_type, ns);
519+
CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
520+
return offset_arithmetic(type, bv, *element_size_opt, neg_op1);
538521
}
539522
else if(expr.id()==ID_byte_extract_little_endian ||
540523
expr.id()==ID_byte_extract_big_endian)
@@ -641,21 +624,17 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
641624

642625
bvt difference = bv_utils.sub(lhs_offset, rhs_offset);
643626

644-
// Support for void* is a gcc extension, with the size treated as 1 byte
645-
// (no division required below).
646-
// https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
647-
if(lhs_pt.base_type().id() != ID_empty)
648-
{
649-
auto element_size_opt = pointer_offset_size(lhs_pt.base_type(), ns);
650-
CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
627+
DATA_INVARIANT(
628+
lhs_pt.base_type().id() != ID_empty,
629+
"no pointer arithmetic over void pointers");
630+
auto element_size_opt = pointer_offset_size(lhs_pt.base_type(), ns);
631+
CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
651632

652-
if(*element_size_opt != 1)
653-
{
654-
bvt element_size_bv =
655-
bv_utils.build_constant(*element_size_opt, width);
656-
difference = bv_utils.divider(
657-
difference, element_size_bv, bv_utilst::representationt::SIGNED);
658-
}
633+
if(*element_size_opt != 1)
634+
{
635+
bvt element_size_bv = bv_utils.build_constant(*element_size_opt, width);
636+
difference = bv_utils.divider(
637+
difference, element_size_bv, bv_utilst::representationt::SIGNED);
659638
}
660639

661640
// test for null object (integer constants)

‎src/solvers/flattening/pointer_logic.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,8 @@ exprt pointer_logict::pointer_expr(
9595
objects[numeric_cast_v<std::size_t>(pointer.object)];
9696

9797
typet subtype = type.base_type();
98-
// This is a gcc extension.
98+
// In a counterexample we may up with void pointers with an offset; handle
99+
// this just like GCC does and treat them as char pointers:
99100
// https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
100101
if(subtype.id() == ID_empty)
101102
subtype = char_type();

‎src/solvers/smt2/smt2_conv.cpp

Lines changed: 10 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -3701,20 +3701,12 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
37013701
"one of the operands should have pointer type");
37023702

37033703
const auto &base_type = to_pointer_type(expr.type()).base_type();
3704+
DATA_INVARIANT(
3705+
base_type.id() != ID_empty, "no pointer arithmetic over void pointers");
37043706

3705-
mp_integer element_size;
3706-
if(base_type.id() == ID_empty)
3707-
{
3708-
// This is a gcc extension.
3709-
// https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
3710-
element_size = 1;
3711-
}
3712-
else
3713-
{
3714-
auto element_size_opt = pointer_offset_size(base_type, ns);
3715-
CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 0);
3716-
element_size = *element_size_opt;
3717-
}
3707+
auto element_size_opt = pointer_offset_size(base_type, ns);
3708+
CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 0);
3709+
mp_integer element_size = *element_size_opt;
37183710

37193711
// First convert the pointer operand
37203712
out << "(let ((?pointerop ";
@@ -3911,20 +3903,11 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
39113903
{
39123904
// Pointer difference
39133905
const auto &base_type = to_pointer_type(expr.op0().type()).base_type();
3914-
mp_integer element_size;
3915-
3916-
if(base_type.id() == ID_empty)
3917-
{
3918-
// Pointer arithmetic on void is a gcc extension.
3919-
// https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
3920-
element_size = 1;
3921-
}
3922-
else
3923-
{
3924-
auto element_size_opt = pointer_offset_size(base_type, ns);
3925-
CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
3926-
element_size = *element_size_opt;
3927-
}
3906+
DATA_INVARIANT(
3907+
base_type.id() != ID_empty, "no pointer arithmetic over void pointers");
3908+
auto element_size_opt = pointer_offset_size(base_type, ns);
3909+
CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
3910+
mp_integer element_size = *element_size_opt;
39283911

39293912
if(element_size >= 2)
39303913
out << "(bvsdiv ";

0 commit comments

Comments
 (0)