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

xbauch · 2019-07-22T09:26:26Z

Since these can be void-pointers. In this case we simply skip introducing the
address-check altogether. See #4930.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

danpoe · 2019-07-22T09:42:03Z

src/analyses/goto_check.cpp

@@ -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*`


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

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.

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);

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

__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.

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

Since these can be void-pointers. In this case we simply skip introducing the address-check altogether.

kroening · 2019-07-22T11:03:25Z

What is the semantics of a valid void * pointer? Would that be true for a zero-sized object?

xbauch · 2019-07-22T11:09:58Z

What is the semantics of a valid void * pointer? Would that be true for a zero-sized object?

Well if anything it should be legal to allocate memory, cast it to void*, pass to a function, which can then cast back, and access all the elements (within the allocation). That is probably not what we should allow for zero-sized objects.

for the SMT2 queries.

codecov-io · 2019-07-22T15:15:13Z

Codecov Report

Merging #4936 into develop will increase coverage by <.01%.
The diff coverage is 100%.

@@             Coverage Diff             @@
##           develop    #4936      +/-   ##
===========================================
+ Coverage    69.26%   69.26%   +<.01%     
===========================================
  Files         1307     1307              
  Lines       108087   108091       +4     
===========================================
+ Hits         74866    74872       +6     
+ Misses       33221    33219       -2

Impacted Files	Coverage Δ
src/analyses/goto_check.cpp	`78.96% <100%> (ø)`	⬆️
src/solvers/smt2/smt2_conv.cpp	`60.1% <100%> (+0.07%)`	⬆️
src/solvers/flattening/boolbv_typecast.cpp	`44.26% <0%> (+0.4%)`	⬆️
src/util/allocate_objects.cpp	`92.15% <0%> (+1.96%)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 1edf4d9...faf21d0. Read the comment docs.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: faf21d0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120033995
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

hannes-steffenhagen-diffblue · 2019-07-23T11:31:05Z

The problem is that there's no "valid" semantics for what a void* points to per se - if it's "valid" it should point to a memory location we're allowed to access, but since there's no such thing as a "void object" in C we can't really tell what's supposed to be there... Now we could do some sort of abstract interpretation thingy or some such to figure out what the pointer is supposed to be dereferenced as by looking at where it's being dereferenced, the problem of course being that void* are often used for closures like this

typedef struct event event;
void register_event_handler(void *closure, void (*handler)(const event*));

so in that case, what the void* is supposed to be pointing to depends on what we set the handler to... There are lots of similar cases where we have instances of several parameters have nontrivial dependencies between each other, that was (for me) a big part of the motivation for goto-harness.

kroening · 2019-07-25T13:02:25Z

What is the semantics of a valid void * pointer? Would that be true for a zero-sized object?

Well if anything it should be legal to allocate memory, cast it to void*, pass to a function, which can then cast back, and access all the elements (within the allocation). That is probably not what we should allow for zero-sized objects.

Note that it is valid to allocate zero bytes; so to make the first part of your statement work, the would need to make this pass for the case of a zero-sized object.

kroening · 2019-07-25T13:04:36Z

I.e., my proposal is to treat the case of void * as "zero size", but otherwise do the same checks as they are done now. In particular, something like valid_pointer((void *)null) should fail.

tautschnig · 2019-08-05T10:17:29Z

src/analyses/goto_check.cpp

@@ -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*`


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

tautschnig · 2019-08-05T10:18:20Z

src/solvers/smt2/smt2_conv.cpp

+    else if(src_type.id() == ID_empty)
+    {
+      convert_expr(src);
+    }


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

tautschnig · 2021-04-16T20:17:19Z

Closing as superseded by #5427.

xbauch requested review from chrisr-diffblue, danpoe, martin-cs, owen-mc-diffblue, peterschrammel, smowton and thk123 as code owners July 22, 2019 09:26

danpoe reviewed Jul 22, 2019

View reviewed changes

Stop assertion size-of-expr for pointer-checks

199b231

Since these can be void-pointers. In this case we simply skip introducing the address-check altogether.

xbauch force-pushed the fix/void-pointer-check branch from 5ce002d to 199b231 Compare July 22, 2019 09:51

Implement converting void type

faf21d0

for the SMT2 queries.

xbauch requested review from allredj, kroening, romainbrenguier and tautschnig as code owners July 22, 2019 14:19

allredj reviewed Jul 22, 2019

View reviewed changes

tautschnig reviewed Aug 5, 2019

View reviewed changes

tautschnig assigned xbauch Aug 5, 2019

romainbrenguier approved these changes Oct 8, 2019

View reviewed changes

tautschnig closed this Apr 16, 2021

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

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

Uh oh!

Conversation

xbauch commented Jul 22, 2019

Uh oh!

danpoe Jul 22, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

xbauch Jul 22, 2019

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Jul 22, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

danpoe Jul 22, 2019

Choose a reason for hiding this comment

Uh oh!

xbauch Jul 22, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

kroening commented Jul 22, 2019

Uh oh!

xbauch commented Jul 22, 2019

Uh oh!

codecov-io commented Jul 22, 2019

Codecov Report

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue commented Jul 23, 2019

Uh oh!

kroening commented Jul 25, 2019

Uh oh!

kroening commented Jul 25, 2019

Uh oh!

tautschnig Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Apr 16, 2021

Uh oh!

Uh oh!

danpoe Jul 22, 2019 •

edited

Loading

hannes-steffenhagen-diffblue Jul 22, 2019 •

edited

Loading