Field sensitivity is not applied for pointer to struct member

[andreast271]

CBMC version: 5.12 (cbmc-5.12.2-3-g9b5f761d5)
Operating system: Linux x86_64
Exact command line resulting in the issue: cbmc --program-only access.c
What behaviour did you expect: field sensitivity is applied for the assignment to s.n[i]
What happened instead: field sensitivity is not applied

Test case:
access.c.txt

I have encountered an example where field sensitivity is not applied, although as far as I can see it could be applied. I have attached the full test case above. The relevant code is as follows:

Good case:

  struct st s;
  s.n[i] = k;

Here field sensitivity works as expected and the assignment to s.n[i] becomes the equation

(37) s!0@1#1..n == { s!0@1#1..n[[0]], s!0@1#1..n[[1]], s!0@1#1..n[[2]], s!0@1#1..n[[3]] } WITH [(signed long int)i!0@1#2:=k!0@1#1]

However, with an intermediate pointer field sensitivity is no longer applied:

  struct st s;
  int *p = s.n;
  p[i] = k;

Now the assignment updates the whole struct:

(37) s!0@1#1 == byte_update_little_endian({ .c=s!0@1#1..c, .$pad1=s!0@1#1..$pad1, .n={ s!0@1#1..n[[0]], s!0@1#1..n[[1]], s!0@1#1..n[[2]], s!0@1#1..n[[3]] } }, 4l * (signed long int)i!0@1#2 + 4l, k!0@1#1, signed int)

There is also the dual case of reading from an index of the array s.n. The situation is similar in that field sensitivity is applied if the access happens directly ( s.n[i] ), but not if an intermediate pointer is inserted ( p = s.n, p[i] ). In this case a simplification rule can get the same effect as field sensitivity, but having a solution involving field sensitivity would be preferable.

[martin-cs]

I suspect this is happening because the pointer analysis is not field sensitive and so says that p can point to s. If I am right then this won't be fixed without a major change to the internals of the symbolic execution engine. VSD might give a way of doing field sensitive pointer analysis that could be used. Alternatively I know @tautschnig did have plans at one point to improve symex's handling of pointers so that the preliminary pointer analysis was not needed.

[smowton]

Looked into this tonight, got some of the way to an answer. The critical moment looks to come during symex_dereference, which applies constant propagation to *(p + i) and resolves p to cast(cast(address_of(main::1::s!0@1), signedbv[8]*) + 4, signedbv[32]*), or cleaning up the notation ((char*)&s) + 4, which is of course &s.n[0].

Taking addresses of fields is of course hazardous when there are individual field symbols floating around in the constant propagator and the LHS of the value-set, so I suspect that's why it's represented that way.

Whether we can preserve the information that this offset aligns with a field when writing to the constant propagator, or recover it when reading, in this case it shouldn't be too difficult to establish we're talking about s.n[i].

Side-note: it's in fact unsound to make that transformation, since s.n[100] for example might write to a subsequent struct field. We're probably right to exclude that case and apply field sensitivity anyhow, though.

[smowton]

Looks like p gets that value because int *p = s.n's rhs is &s.n[0], which symex_clean_expr turns into (int*)((char*)&s) + 4. That form appears to be a very deliberate invariant of address_arithmetic, so in the context p[i] = *(p + i) we would need to recover the array form when trying to apply field sensitivity to the LHS.

[smowton]

Eventual conclusion: the problem was value-set-dereference losing sight of the underlying object (s and specifically s.n), so producing a byte-extract against the whole object not an index against s.n, and so failing to trigger the (in this case, unsound) application of field-sensitivity (unsound in that it assumes the references is in-bounds, which should probably be optional).

@andreast271 here's a draft that fixes your particular case: #5418

I'm unlikely to have a lot of time to test that thoroughly enough to get it into develop -- are you in a position to test that draft and if it's useful perhaps shepherd it from here? If not @hannes-steffenhagen-diffblue @tautschnig is an improvement along these lines interesting to you?

[hannes-steffenhagen-diffblue]

@smowton In principle interesting thing to do, we’re considering possible performance improvements (and it seems like we might have to make some changes to field sensitivity regardless for that). We don’t have a ton of time to schedule this right now but I’ll definitely take a look.

[andreast271]

@smowton Thank you very much and I will definitely test your fix on a number of industrial examples for both correctness and performance impact. I'll have to backport the change set to our version of cbmc, but the code in value_set_dereference.{cpp,h} has not changed and I did not see any changes to field sensitivity either, so the impact of the change set should be the same on the latest version and on our version.

[smowton]

@andreast271 looking at that Travis report I've definitely broken type-preservation with this one -- I've probably thrown a cast away somewhere. I'll try for a version of this that passes tests tonight...

[smowton]

@andreast271 it was just a missing integer typecast, I'm expecting the version I just pushed to pass tests

[smowton]

@chrisr-diffblue I have forwarded you an email from @andreast271 about working further on this, let me know if you don't see it

[chrisr-diffblue]

Thanks @smowton - email received ;-)