Skip to content

Commit b4c2ff1

Browse files
committed
Simplification of nested pointer arithmetic: do not assume same type
Pointer arithmetic is permitted with both signed and unsigned numeric operands. Nested expressions could possibly mix this when the front-end does not strictly use the same type for pointer arithmetic as for index types. Observed in model-checking/kani#708. Introducing type casts (as needed) exposed a further issue in this code: it previously did not make sure that it was really the numeric operands that ended up being grouped together. This became apparent on test Pointer_Arithmetic15, which specifically constructs such expressions.
1 parent 7214340 commit b4c2ff1

File tree

2 files changed

+10
-2
lines changed

2 files changed

+10
-2
lines changed

regression/cbmc/Pointer_Arithmetic15/main.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,5 +15,9 @@ int main()
1515

1616
a = p - q;
1717

18+
// mixing types: the C front-end will insert casts
19+
unsigned long long u;
20+
p = (p + a) + u;
21+
1822
assert(0);
1923
}

src/util/simplify_expr_int.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -440,17 +440,21 @@ simplify_exprt::resultt<> simplify_exprt::simplify_plus(const plus_exprt &expr)
440440
expr.op0().operands().size() == 2)
441441
{
442442
plus_exprt result = to_plus_expr(expr.op0());
443+
if(as_const(result).op0().type().id() != ID_pointer)
444+
result.op0().swap(result.op1());
443445
const exprt &op1 = as_const(result).op1();
444446

445447
if(op1.id() == ID_plus)
446448
{
447449
plus_exprt new_op1 = to_plus_expr(op1);
448-
new_op1.add_to_operands(expr.op1());
450+
new_op1.add_to_operands(
451+
typecast_exprt::conditional_cast(expr.op1(), new_op1.op0().type()));
449452
result.op1() = simplify_plus(new_op1);
450453
}
451454
else
452455
{
453-
plus_exprt new_op1{op1, expr.op1()};
456+
plus_exprt new_op1{
457+
op1, typecast_exprt::conditional_cast(expr.op1(), op1.type())};
454458
result.op1() = simplify_plus(new_op1);
455459
}
456460

0 commit comments

Comments
 (0)