Skip to content

Stop assertion size-of-expr for pointer-checks #4936

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 2 commits into from
Closed

Stop assertion size-of-expr for pointer-checks #4936

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
199b231
Stop assertion size-of-expr for pointer-checks
petr-bauch Jul 22, 2019
faf21d0
Implement converting void type
petr-bauch Jul 22, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions regression/cbmc/Void_Pointer_Init/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
#include <assert.h>

void foo(void *arg)
{
assert(*(unsigned *)(arg) == 5);
}
9 changes: 9 additions & 0 deletions regression/cbmc/Void_Pointer_Init/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
main.c
--function foo --pointer-check
^\[foo.assertion.1\] line \d+ assertion \*\(unsigned \*\)\(arg\) == 5: FAILURE$
^\[foo.pointer_dereference.4\] line \d+ dereference failure: dead object in \*\(\(unsigned int \*\)arg\): FAILURE$
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
3 changes: 2 additions & 1 deletion src/analyses/goto_check.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1113,7 +1113,8 @@ void goto_checkt::pointer_validity_check(
const exprt &pointer=expr.pointer();

auto size_of_expr_opt = size_of_expr(expr.type(), ns);
CHECK_RETURN(size_of_expr_opt.has_value());
if(!size_of_expr_opt.has_value())
return; // in the case of `void*`
Copy link
Contributor

@danpoe danpoe Jul 22, 2019 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't size_of_expr() also work for void pointers? In that case we should fix size_of_expr() if possible.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But even if we implement size-of for void the result will be 0, right? I'm not sure we should build the address-check in that case.

Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Jul 22, 2019 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

sizeof(void) is undefined in C, some compilers set it to 1 just because there's too much code out there that assumes that void* == char*. For example, gcc does this but warns against it with -Wpointer-arith (in the -Wpedantic group):

test.c:1:16: warning: invalid application of ‘sizeof’ to a void type [-Wpointer-arith]
 int x = sizeof(void);

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I see. It's surprising that we get a dereference expression of a void pointer here.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more. 

__CPROVER__start {
  char tmp;
  void *arg;
  if(NONDET(__CPROVER_bool))
    arg = NULL;

  else
  {
    arg = (void *)&tmp;
    *((void *)&tmp) = NONDET(void);
  }
  foo(arg);
}

This is what the entry-point looks like.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wouldn't address_check below with a zero-sized object still do some good?


auto conditions = address_check(pointer, size_of_expr_opt.value());

Expand Down
9 changes: 9 additions & 0 deletions src/solvers/smt2/smt2_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2214,6 +2214,10 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
convert_typecast(tmp);
}
}
else if(src_type.id() == ID_empty)
{
convert_expr(src);
}
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This might actually fix some of the broken-smt-backend tests - would you mind testing that?

else
{
std::ostringstream e_str;
Expand Down Expand Up @@ -4626,6 +4630,11 @@ void smt2_convt::convert_type(const typet &type)
{
convert_type(c_bit_field_replacement_type(to_c_bit_field_type(type), ns));
}
else if(type.id() == ID_empty)
{
// the NONDET(void) is in fact of type char
out << "(_ BitVec " << boolbv_width(char_type()) << " )";
}
else
{
UNEXPECTEDCASE("unsupported type: "+type.id_string());
Expand Down