Bounds checking on nested structs when passed as pointer

[bg1729]

When a C struct encapsulates another struct, it seems CBMC does not identify out of bounds accesses to an inner struct under the following conditions:-

1. The access is inside the "outer" struct's bounds.
2. The outer struct is accessed via a pointer.

I have enabled both bounds-check and pointer-check so I think this should be picked up?

I've included an example below.

BR
Gareth

#include <stdint.h>

struct bar
{
    uint8_t baz[8];
};

struct foo
{
    struct bar bars[2];
};

#ifdef PROBLEMMAYBE
int test(struct foo* f)
{
    f->bars[0].baz[9] = 0;
}
#endif

int main(int argc, char* argv[])
{
    struct foo f;
#ifdef PROBLEMMAYBE
    test(&f);
#else
    f.bars[0].baz[9] = 0;
#endif
}

gareth@snares:~$ cbmc foo.c --bounds-check --pointer-check -DPROBLEMMAYBE | tail -n 5
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
file <command-line> line 0: <built-in>: note: this is the location of the previous definition
Solving with MiniSAT 2.2.0 with simplifier
502 variables, 328 clauses
SAT checker inconsistent: negated claim is UNSATISFIABLE, i.e., holds
Runtime decision procedure: 0.001s
VERIFICATION SUCCESSFUL

gareth@snares:~$ cbmc foo.c --bounds-check --pointer-check | tail -n 5
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
file <command-line> line 0: <built-in>: note: this is the location of the previous definition
  file foo.c line 27 function main
  array `f'.bars[].baz upper bound in f.bars[(signed long int)0].baz[(signed long int)9]
  FALSE

VERIFICATION FAILED
gareth@snares:~$ 

[smowton]

So goto_check.cpp applies a different check depending on whether its argument starts with a dereference operator or not. If it does, it creates an array upper-bounds check against the dynamic object's size. If not, it checks against the static type. Thus it would catch both of the following:

char x[4]; x[5]='a'; // Static type abuse
struct y { char x[4] }; struct y a; struct y* a2=(struct y*)((char*)a)+3; a2->x[3]='a'; // Acceptable according to static types, but outside the bounds of the underlying object

But it would miss anything that's out of bounds statically but not dynamically, like the example given above, or more simply
struct z { char arr[4]; int more_fields; }; struct z a3; (&a3)->arr[5]='a' // Overwrites part of more_fields, which is part of the same allocation

However I see no reason why we can't have both checks when a pointer-typed argument is used. Posting a PR with a fix that enables this check even in this circumstance, but this isn't tested except with the given example.

[smowton]

Recreated PR, to try to get this unstalled and because the cbmc/cbmc-testgen move had left this orphaned.

[smowton]

Waiting on #339