Value set dereferencing: do not treat struct prefixes as equal

[tautschnig]

Two distinct struct types cannot be cast between, even when one is a
prefix of the other. Value set dereferencing taking this approach just
resulted in propositional encoding producing a warning about invalid
type casts.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a 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).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Attention: Patch coverage is 0% with 10 lines in your changes are missing coverage. Please review.

Project coverage is 78.36%. Comparing base (ae7d311) to head (b450a9e).
Report is 2 commits behind head on develop.

Files	Patch %	Lines
src/cprover/may_alias.cpp	0.00%	10 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #5876      +/-   ##
===========================================
+ Coverage    77.81%   78.36%   +0.55%     
===========================================
  Files         1721     1721              
  Lines       189460   188104    -1356     
  Branches     18401    18456      +55     
===========================================
- Hits        147432   147414      -18     
+ Misses       42028    40690    -1338     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[martin-cs]

I had to go back and check my copy of ISO 9899 because I thought there was a rule about this but ... I can't find it. I wrote the following...

#include <assert.h>

struct a { int x; };
struct b { struct a p; int y; };

int f00 (struct a *ptr) {
  return ptr->x;
}

int main() {
  struct b z = { {1}, 2 };
  
  assert(&z == &(z.p));
  assert(&z == &(z.p.x));

  assert(f00(&z) == z.p.x);
  
  return 0;
}

This compiles but I don't think it is actually standard C:

$ gcc  struct-pointer.c -o struct-pointer 
In file included from struct-pointer.c:1:
struct-pointer.c: In function ‘main’:
struct-pointer.c:13:13: warning: comparison of distinct pointer types lacks a cast
   assert(&z == &(z.p));
             ^~
struct-pointer.c:13:13: warning: comparison of distinct pointer types lacks a cast
   assert(&z == &(z.p));
             ^~
struct-pointer.c:14:13: warning: comparison of distinct pointer types lacks a cast
   assert(&z == &(z.p.x));
             ^~
struct-pointer.c:14:13: warning: comparison of distinct pointer types lacks a cast
   assert(&z == &(z.p.x));
             ^~
struct-pointer.c:16:14: warning: passing argument 1 of ‘f00’ from incompatible pointer type [-Wincompatible-pointer-types]
   assert(f00(&z) == z.p.x);
              ^~
struct-pointer.c:6:20: note: expected ‘struct a *’ but argument is of type ‘struct b *’
 int f00 (struct a *ptr) {
          ~~~~~~~~~~^~~
In file included from struct-pointer.c:1:
struct-pointer.c:16:14: warning: passing argument 1 of ‘f00’ from incompatible pointer type [-Wincompatible-pointer-types]
   assert(f00(&z) == z.p.x);
              ^~
struct-pointer.c:6:20: note: expected ‘struct a *’ but argument is of type ‘struct b *’
 int f00 (struct a *ptr) {
          ~~~~~~~~~~^~~

which we can handle:

$ cbmc struct-pointer.c
CBMC version 5.24.0 (cbmc-5.24.0-81-g19fca2ebfc) 64-bit x86_64 linux
Parsing struct-pointer.c
Converting
Type-checking struct-pointer
file struct-pointer.c line 16 function main: warning: conversion from 'struct b *' to 'struct a *': incompatible pointer types
file struct-pointer.c line 16 function main: warning: conversion from 'struct b *' to 'struct a *': incompatible pointer types
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00476498s
size of program expression: 54 steps
simple slicing removed 0 assignments
Generated 3 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 3.4174e-05s

** Results:
struct-pointer.c function main
[main.assertion.1] line 13 assertion &z == &(z.p): SUCCESS
[main.assertion.2] line 14 assertion &z == &(z.p.x): SUCCESS
[main.assertion.3] line 16 assertion f00(&z) == z.p.x: SUCCESS

** 0 of 3 failed (1 iterations)
VERIFICATION SUCCESSFUL

and correctly put in the casts:

#include <assert.h>

struct a { int x; };
struct b { struct a p; int y; };

int f00 (struct a *ptr) {
  return ptr->x;
}

int main() {
  struct b z = { {1}, 2 };
  
  assert(&z == &(z.p));
  assert(&z == &(z.p.x));

  assert(f00(&z) == z.p.x);
  
  return 0;
}

[martin-cs]

Seems correct but removing things like this makes me nervous. Please could you check whether it is covered by any of the tests-- it should be dead right? The code seems to be almost exactly a decade old but that might well be the date of the move from CVS to Subversion and the "start" of history.

[martin-cs]

If we are removing the .desc file, should we remove the Java file as well or is it used for other things?

[tautschnig]

There are other tests in this directory that are still using this Java code and that do pass as expected.

[tautschnig]

I had to go back and check my copy of ISO 9899 because I thought there was a rule about this but ... I can't find it. I wrote the following...

[...]

Thanks, I included your proposed test as a further regression test.

Also, it may be that some of the tests actually used this code, but they will now fall back to the code path that actually does the right thing and creates a byte extract.

[kroening]

Structs can't be casted, but pointers to structs can be casted to pointers to structs that are prefixes -- this is what this piece of code was meant to cover.

[tautschnig]

Structs can't be casted, but pointers to structs can be casted to pointers to structs that are prefixes -- this is what this piece of code was meant to cover.

But then value_set_dereferencet::dereference_type_compare would have to do a test of is_prefix_of on object_unwrapped and dereference_unwrapped with the additional check that they are not the same as object_type (and dereference_type). Is that the change we should be making?