Get lhs_object from byte_extract for goto trace

[peterschrammel]

Otherwise fields are missing from the XML output, which breaks downstream integration of a commercial CBMC user.

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

[tautschnig]

Great to see this improving - I don't think you'd even need to add a new test, existing tests like regression/cbmc/array_constraints1 also have this problem.

[tautschnig]

Remind me, do we actually consider the offset? What you propose is consistent with what's done for index and member expressions, but I'm still wondering whether the overall result is meaningful.

[peterschrammel]

No, it was not considered. The meaningfulness is questionable, but that probably goes beyond this fix.
It might be good to actually specify what these fields are supposed to mean precisely.

[tautschnig]

Here's an example to validate:

#include <assert.h>

int main()
{
  int x;
  char *p = (char *)&x + 2;
  *p = 1;
  assert(x == 0);
}

The trace currently includes byte_extract_little_endian(x, 2l, char)=1 (00000001) - which might not be downstream-consumable, but at least is accurate. If after this PR the result is x=1 then there's a problem I'm afraid.

[kroening]

goto_trace_steps offer two bits of information:

1. The thing returned by get_lhs_object() -- that is the object as defined in the C standard, and x is the right answer.
2. The full_lhs, which is documented to be "after dereferencing". It is supposed to be exactly what gets assigned. The byte_extract expression above is the best answer for that, in my view.

The trace given to the user should show the latter. We may wish to print byte_extract expressions there as a pointer typecast plus dereferencing.

[tautschnig]

Thank you for clarifying! +1 for printing byte_extract as some C expression, which will be important for SV-COMP as well. But I accept that this might be outside the scope of this PR.

[tautschnig]

Please also add --little-endian to the command line to make sure this test is portable.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 60b5328).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107058275