crucible-llvm rejects memory load of a struct with padding

[RyanGlScott]

crux-llvm will choke on this C code which, as far as I can tell, is perfectly valid:

#include <stdint.h>

struct s {
  uint8_t  x;
  uint32_t y;
};

static struct s ss = { 0 };

static struct s get_ss() {
    return ss;
}

int main(void) {
    struct s local_ss = get_ss();
    return 0;
}

$ ~/Software/crux-llvm-0.8/bin/crux-llvm -O0 test.c
[Crux] Using pointer width: 64 for file crux-build/crux~test.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] *** debug executable: results/test/debug-11
[Crux] *** break on line: 11
[Crux] Found counterexample for verification goal
[Crux]   test.c:11:5: error: in get_ss
[Crux]   Error during memory load
[Crux]     Load from invalid memory at type i24
[Crux]     Performing overall load at type: i64
[Crux]       Via pointer: (8, 0x0:[64])
[Crux]     In memory state:
[Crux]       Stack frame get_ss
[Crux]         Allocations:
[Crux]           StackAlloc 8 0x8:[64] Mutable 4-byte-aligned test.c:11:12
[Crux]         Writes:
[Crux]           memcopy (8, 0x0:[64]) (5, 0x0:[64]) 0x8:[64]
[Crux]       Stack frame main
[Crux]         Allocations:
[Crux]           StackAlloc 7 0x8:[64] Mutable 4-byte-aligned test.c:15:14
[Crux]           StackAlloc 6 0x4:[64] Mutable 4-byte-aligned internal
[Crux]         Writes:
[Crux]           Indexed chunk:
[Crux]             6 |->   memset (6, 0x0:[64]) 0x0:[8] 0x4:[64]
[Crux]       Base memory
[Crux]         Allocations:
[Crux]           GlobalAlloc 5 0x8:[64] Mutable 4-byte-aligned [global variable  ] ss
[Crux]           GlobalAlloc 4 0x0:[64] Immutable 1-byte-aligned [defined function ] get_ss
[Crux]           GlobalAlloc 3 0x0:[64] Immutable 1-byte-aligned [defined function ] main
[Crux]           GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned [external function] llvm.memcpy.p0i8.p0i8.i64
[Crux]           GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned [external function] llvm.dbg.declare
[Crux]         Writes:
[Crux]           Indexed chunk:
[Crux]             5 |->   *(5, 0x0:[64]) := 0
[Crux]     in context:
[Crux]       get_ss
[Crux]       main
[Crux] Goal status:
[Crux]   Total: 1
[Crux]   Proved: 0
[Crux]   Disproved: 1
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.

The Load from invalid memory at type i24 part of the error message hints at what is going on. When struct s is compiled to LLVM, it puts 24 bits of padding between field x and field y so that a struct s value occupies exactly 64 bits. We can see this if we look at the LLVM bitcode:

%struct.s = type { i8, i32 }

@ss = internal global %struct.s zeroinitializer, align 4, !dbg !0

; Function Attrs: noinline nounwind optnone uwtable
define dso_local i32 @main() #0 !dbg !25 {
  %1 = alloca i32, align 4
  %2 = alloca %struct.s, align 4
  store i32 0, i32* %1, align 4
  call void @llvm.dbg.declare(metadata %struct.s* %2, metadata !30, metadata !DIExpression()), !dbg !31
  %3 = call i64 @get_ss(), !dbg !32
  %4 = bitcast %struct.s* %2 to i64*, !dbg !32
  store i64 %3, i64* %4, align 4, !dbg !32
  ret i32 0, !dbg !33
}

; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
declare void @llvm.dbg.declare(metadata, metadata, metadata) #1

; Function Attrs: noinline nounwind optnone uwtable
define internal i64 @get_ss() #0 !dbg !34 {
  %1 = alloca %struct.s, align 4
  %2 = bitcast %struct.s* %1 to i8*, !dbg !37
  call void @llvm.memcpy.p0i8.p0i8.i64(i8* align 4 %2, i8* align 4 getelementptr inbounds (%struct.s, %struct.s* @ss, i32 0, i32 0), i64 8, i1 false), !dbg !37
  %3 = bitcast %struct.s* %1 to i64*, !dbg !38
  %4 = load i64, i64* %3, align 4, !dbg !38
  ret i64 %4, !dbg !38
}

Note that get_ss returns an i64 instead of a %struct.s, which reflects SystemV ABI requirements. This is all well and good, except for these lines:

  %3 = bitcast %struct.s* %1 to i64*, !dbg !38
  %4 = load i64, i64* %3, align 4, !dbg !38

Here, we cast a %struct.s pointer to an i64 pointer and load an i64 value from the pointer. crucible-llvm's memory model does not like the fact that 24 bits of this i64 are padding and throws the error above.

In order to fix this, we will likely need to relax this check in crucible-llvm's memory model. The following note in the LLVM language reference about the store instruction may be relevant:

If <value> is of aggregate type, padding is filled with undef.

I wonder if we should do something similar.

[sauclovian-g]

Seems reasonable. In principle (though only on DS9000) you can have padding bits in signed integers too :-)