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:
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.
crux-llvm
will choke on this C code which, as far as I can tell, is perfectly valid:The
Load from invalid memory at type i24
part of the error message hints at what is going on. Whenstruct s
is compiled to LLVM, it puts 24 bits of padding between fieldx
and fieldy
so that astruct s
value occupies exactly 64 bits. We can see this if we look at the LLVM bitcode:Note that
get_ss
returns ani64
instead of a%struct.s
, which reflects SystemV ABI requirements. This is all well and good, except for these lines:Here, we cast a
%struct.s
pointer to ani64
pointer and load ani64
value from the pointer.crucible-llvm
's memory model does not like the fact that 24 bits of thisi64
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 thestore
instruction may be relevant:I wonder if we should do something similar.