Skip to content

Commit

Permalink
Simplify tests of is-null that use integer types
Browse files Browse the repository at this point in the history
Injecting casts to integer types should not hamper our ability to
simplify tests for null-ness. Such expressions emerge from Rust code,
see model-checking/kani#2191.
  • Loading branch information
tautschnig committed Feb 23, 2023
1 parent d7099ae commit 5d87cf0
Show file tree
Hide file tree
Showing 3 changed files with 58 additions and 0 deletions.
12 changes: 12 additions & 0 deletions regression/cbmc/null8/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
union U
{
void *ptr;
__CPROVER_size_t n;
};

int main()
{
int *p = __CPROVER_allocate(sizeof(int), 0);
union U u = {.ptr = p};
__CPROVER_assert(u.n != 0, "is not null");
}
9 changes: 9 additions & 0 deletions regression/cbmc/null8/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE new-smt-backend
main.c

Generated 1 VCC\(s\), 0 remaining after simplification
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
37 changes: 37 additions & 0 deletions src/util/simplify_expr_int.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1897,6 +1897,43 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
}
}
}

if(config.ansi_c.NULL_is_zero)
{
const exprt &maybe_tc_op = skip_typecast(expr.op0());
if(maybe_tc_op.type().id() == ID_pointer)
{
// make sure none of the type casts lose information
const pointer_typet &p_type = to_pointer_type(maybe_tc_op.type());
bool bitwidth_unchanged = true;
const exprt *ep = &(expr.op0());
while(bitwidth_unchanged && ep->id() == ID_typecast)
{
if(auto t = type_try_dynamic_cast<bitvector_typet>(ep->type()))
{
bitwidth_unchanged = t->get_width() == p_type.get_width();
}
else
bitwidth_unchanged = false;

ep = &to_typecast_expr(*ep).op();
}

if(bitwidth_unchanged)
{
if(expr.id() == ID_equal || expr.id() == ID_ge || expr.id() == ID_le)
{
return changed(simplify_rec(
equal_exprt{maybe_tc_op, null_pointer_exprt{p_type}}));
}
else
{
return changed(simplify_rec(
notequal_exprt{maybe_tc_op, null_pointer_exprt{p_type}}));
}
}
}
}
}

// are we comparing with a typecast from bool?
Expand Down

0 comments on commit 5d87cf0

Please sign in to comment.