cbmc invariant violation in rewrite_with_to_field_symbols

[andreast271]

CBMC version: 5.12 (cbmc-5.12-d8598f8-557-g1edf4d91f)
Operating system: CentOS Linux 7
Exact command line resulting in the issue: cbmc struct_array.c
What behaviour did you expect: no invariant violation
What happened instead: invariant violation

cbmc symbolic simulation fails with an invariant violation in function rewrite_with_to_field_symbols when it tries to simulate the following c code:

typedef struct _MyStruct {
    int m_a;
} MyStruct;

typedef struct _MyArrayStruct {
    MyStruct m_ar[2];
} MyArrayStruct;

int main()
{
  MyArrayStruct mas;
  int a, i;
  i = 1;
  (mas.m_ar + i)->m_a = a;
  //(mas.m_ar + 1)->m_a = a;
  //mas.m_ar[i].m_a = a;
  return 0;
}

The failure is caused in expr_skeletont::clear_innermost_member_expr when deepest_not_nil returns a byte_extract expression and the code expects it to return a member expression.
Either of the two lines that are commented out in the code above do not lead to an invariant failure.

[smowton]

#4917 would fix this by virtue of deleting the offending code entirely -- @tautschnig @romainbrenguier @kroening would you mind reviewing?

[smowton]

(confirmed the given test program works fine with #4917)

[andreast271]

#4917 works on the test program, but introduces a different problem on another test case, where the constant offset of a byte extract operation exceeds the width of the first operand. I am trying to get a self-contained test case for this problem.

[smowton]

@andreast271 I haven't been able to reproduce that with some fiddling around with byte-extract ops, any luck on that test-case? If you have a non-reduced test-case I'm also happy to have a go at minimising it myself.

[andreast271]

The problem with offset exceeding the operand width is probably not a bug after all. It occurs in C code that has been automatically translated from C++. Which such code, function pointers cannot always be resolved statically or by constant propagation, so symex has to guess. Symex will then occasionally execute a method of a derived class on an object of the base class. This can easily lead to offset overflows, for example if the code accesses a member of the derived class that is not present in the base class. However, these execution paths are infeasible, so the out-of-range access does no harm.

[tautschnig]

Closing as #4917 has been merged.