Struct field accesses generate duplicate proof obligations for pointer validity

[brianhuffman]

Consider this C code that accesses fields from an array of structs:

#include <stdint.h>

typedef struct { uint32_t fst; uint32_t snd; } pair_t;
typedef struct { uint32_t head; pair_t tail; } triple_t;

void test(uint64_t i, triple_t *list) {
    list[i].tail.snd = 17;
}

Then we do a verification with crucible_llvm_verify, passing in an array of size 100:

crucible_llvm_verify bc "test" [] false
  do {
    i <- crucible_fresh_var "i" i64;
    crucible_precond {{ i < 100 }};
    let ty = llvm_array 100 (llvm_struct "struct.triple_t");
    list <- crucible_fresh_var "list" ty;
    list_ptr <- crucible_alloc ty;
    crucible_points_to list_ptr (crucible_term list);
    crucible_execute_func [crucible_term i, list_ptr];
  }
  do {
    print_goal;
    z3;
  };

Symbolic simulation of the address calculations then produces the following proof obligations (the memory write produces a couple more of its own, which are omitted):

• 0xf555555555555556 <=$ i /\ i <=$ 0x0aaaaaaaaaaaaaaa
• 12 * i <= 1200
• 12 * i <= 1200
• 4 + 12 * i <= 1200
• 4 + 12 * i <= 1200
• 8 + 12 * i <= 1200
  Notice that some of the obligations are exact duplicates of each other. Also note that the first proof obligation is to ensure that 12 * i does not cause signed overflow.

I figured out the reason for the duplication; the key is the getelementptr instructions in the LLVM:

  %7 = getelementptr inbounds %struct.triple_t, %struct.triple_t* %5, i64 %6, !dbg !57
  %8 = getelementptr inbounds %struct.triple_t, %struct.triple_t* %7, i32 0, i32 1, !dbg !59
  %9 = getelementptr inbounds %struct.pair_t, %struct.pair_t* %8, i32 0, i32 1, !dbg !60

The first one is for [i], the second is for .tail, and the third is for .snd. But note that the getelementptr instruction for a field access includes a first argument which is i32 0. This is actually treated as an array index, so what we're actually translating into Crucible is this:

    list[i][0].tail[0].snd = 17;

I think it is the extra array indexing at offset 0 that is producing the extra proof obligations. This problem only appears when combining symbolic array offsets with struct field accesses, because when the offsets are totally concrete, then the bounds checks can be evaluated statically, and they don't produce proof obligations at all.

To fix this, I think we just need to make a special case in the evaluation of getelementptr for arrays, to skip the case when the array index is a concrete 0.