[aurelf]

This PR was prepared by Claude (Anthropic's AI assistant) at aurelf's request, as a follow-up to the review on eurecom-s3#191.

Adds test/vector_endianness.ll, a regression test for the vector layout issue described in item 1 of the review on #191.

On little-endian targets, loads and stores treat a vector like an integer of the same width: lane 0 is in the least significant bits, as with bitcast <4 x i32> to i128. The extract/insert/concat code in eurecom-s3#191 assumes the struct layout instead (lane 0 first, lanes byte-swapped). So the solver reasons about the wrong lane, or about byte-swapped lane values.

The test treats 16 symbolic bytes as a <4 x i32> and covers three patterns, each on its own lane so every correct solution is unique:

#	Pattern	Condition	Expected input
1	vector load → extractelement lane 1	== 0x11223344	bytes 4..7 = 44 33 22 11
2	vector load → add 1 (carry crosses a byte) → vector store → scalar load of lane 2	== 0x100	bytes 8..11 = ff 00 00 00
3	insertelement into lane 3 → vector store → scalar load of lane 3	== 0x55667788	bytes 12..15 = 88 77 66 55

• Simple backend: the test checks the exact solutions the solver prints.
• QSYM backend: a test-case handler prints sN solved only if a generated input actually satisfies scenario N.

Status: this test fails on the current branch by design. It should pass once vectors use the same layout as loads, stores and bitcasts.

• Simple backend, scenario 1: the solver produces stdin8..11 = 11 22 33 44 (lane 2, reversed) instead of stdin4..7 = 44 33 22 11.
• QSYM backend: no input is generated for any of the vector scenarios. A control variant using a scalar load for scenario 1 does report s1 solved, which shows the handler logic works.
• Built natively with a stub runtime, the expected inputs take all three branches.

Tested with LLVM 15 (the project's Docker builder image).

🤖 Generated with Claude Code