[TheaPredicate2]

Addresses the second half of #171: SymCC crashes when symbolic values flow through vector-typed instructions (e.g. <4 x i32> arithmetic, extractelement, insertelement, shufflevector).

Note: This PR builds on top of #189 (bool arithmetic fix). The first commit here is identical to the single commit in #189. Once #189 lands, this branch will be rebased so it carries only the vector delta.

Approach

Represent vector values as flat bit-vectors (one lane after another in little-endian order), then add visitors for each new instruction and decompose per-lane where the semantics do not cross lanes.

Changes

• createValueExpression learns VectorType: concatenates per-element expressions into a single flat bit-vector, mirroring the existing StructType path.
• visitBinaryOperator handles vector operands:
  • Bitwise And/Or/Xor stay on the fast path (one call on the full-width expression — bits don't interact across lanes).
  • Arithmetic ops (Add/Sub/Mul/…) are decomposed lane by lane so inter-lane carries/borrows don't leak.
• visitCmpInst handles vector operands by comparing each lane and converting the Bool result to a 1-bit bit-vector before concatenation.
• visitExtractElementInst: constant index → byte-aligned _sym_build_extract on the flat expression; variable index → ITE chain over the possible lanes so the solver can reason jointly about index selection and lane contents.
• visitInsertElementInst: mirrors visitInsertValueInst over the flat bit-vector representation.
• visitShuffleVectorInst: walks the mask, extracts the chosen lane from the appropriate source (or a zero byte for undef), concatenates to form the result.
• Runtime gains buildIte → _sym_build_ite, used by extractelement with a symbolic index.
• test/vectors.c covers construction, extract/insert (constant and variable index), binary ops (both paths), compare, and shufflevector.

Out of scope

The following produce a warning and fall through to concretization — reasonable follow-ups:

• Scalable vectors (will crash — not handled).
• Float-element vector binary ops.
• Float-element vector comparisons.

Testing

Tested with LLVM 17 and 21 on Linux x86_64. Full test suite passes (modulo the pre-existing file_input.c unresolved test, which is unrelated to this PR).

[aurelf]

🤖 This review was written by Claude (Anthropic's AI assistant) at aurelf's request. Claude built this PR in the project's LLVM 15 Docker image and ran hand-written LLVM IR probes against it with the simple and QSYM backends. The findings below come from those runs unless marked "from reading the code".

Thanks for working on vector support. The overall approach is sound: a fast path for bitwise ops, per-lane decomposition otherwise, and an ITE chain for a symbolic index (_sym_build_ite already exists in the runtime, so the new import links fine). However, there is one blocking correctness problem, plus a few smaller ones.

1. Vector layout is inconsistent on little-endian targets (blocking)

isLittleEndian() returns true for vector types (LLVM doesn't consider vectors aggregates). So visitLoadInst/visitStoreInst treat a <4 x i32> like an i128: lane 0 is in the low bits. That is also what bitcast <4 x i32> to i128 means. The new code instead mirrors the struct path (createValueExpression, _sym_build_extract/_sym_build_insert with byte offsets, lane-by-lane concat): lane 0 in the high bits and each lane byte-swapped. The two layouts don't agree, so the solver reasons about the wrong lane or about byte-swapped lane values and generates wrong inputs:

IR pattern	Branch condition	Solver output (simple backend)	Correct input
vector load → extractelement lane 0	== 0x11223344	stdin12..15 = 11 22 33 44 (lane 3, reversed)	stdin0..3 = 44 33 22 11
vector load → add v, v → store → load i32	== 256	stdin2 = 0x80 (2 × 0x00800000 ≠ 256)	stdin0 = 0x80
insertelement lane 0 → vector store → load i32	== 0x11223344	no query at all: the symbolic lane ends up in bytes 12–15	stdin0..3 = 44 33 22 11
vector icmp → extractelement (with or without sext)	lane 0 == 7	constrains lane 3	lane 0

The add case shows the lane arithmetic running on byte-reversed values (bvmul 2 (concat stdin0 stdin1 stdin2 stdin3)), so the result is wrong as soon as a carry crosses a byte.

On big-endian targets, isLittleEndian() is false for vectors too, loads keep memory order, and the struct-style layout happens to be consistent (for byte-sized elements). So this only bites on little-endian targets, which in practice means x86-64, AArch64 and RISC-V.

Suggested fix: use one layout everywhere: the bit pattern of bitcast to an integer of the same width, which is what loads and stores already produce on both endiannesses. Lane i of an N-lane vector with K-bit elements is at bit offset i*K (little-endian) or (N-1-i)*K (big-endian) from the least significant end. Extract lanes at the bit level without bswap, and build vectors (createValueExpression, binary ops, compares, shuffles) by concatenating lanes from the most significant end. This also gives cheaper expressions and fixes <N x i1> (item 2).

Regression test: test/vector_endianness.ll (one commit on top of this branch). It covers vector load + extractelement, lane-wise add with a carry across bytes + store, and insertelement + store. It checks the exact solutions with the simple backend and checks generated inputs through a test-case handler with QSYM. It fails on the current head with both backends, and its expected inputs were verified by running the program natively. Feel free to cherry-pick it.

2. <N x i1> vectors have three different sizes (from reading the code)

A vector icmp builds an N-bit expression. createValueExpression of an undef vector gives getTypeStoreSize() bytes, and shuffle's undef lanes use buildZeroBytes(elementSize). Extract, insert and shuffle use byte offsets with elementSize = 1 for i1. _sym_build_extract asserts totalBits % 8 == 0, which is compiled out in release builds. Bool vectors need bit-level lane access, which the layout in item 1 gives for free.

3. Existing visitors now see symbolic vectors (from reading the code; outside this diff)

Before this PR vectors never had expressions; now they do, and they reach visitors that assume scalars:

• visitCastInst (sext/zext) and visitTruncInst call getIntegerBitWidth() on the operand and result types. For vector types that asserts in debug builds and gives a meaningless width in release builds. Note that C vec == (v4si){...} lowers to exactly icmp + sext <4 x i1> to <4 x i32>.
• visitBitCastInst asserts on vector↔integer bitcasts, which are common in SIMD code (e.g. <16 x i8> ↔ <2 x i64>, <4 x i1> → i4).

These should either handle vectors (lane-wise sext/zext/trunc; a no-op for same-width bitcasts with the layout above) or explicitly skip them, so the value is treated as concrete.

4. The test doesn't exercise most of the new code

At -O1, clang scalarizes test/vectors.c. The only vector instructions left are the insertelement chain and one variable-index extractelement, so the add, mul, xor, shuffle and compare cases never reach the new visitors. The CHECK lines also only require Found diverging input, not a correct input. I'd suggest hand-written .ll tests (like load_store.ll/symbolic_structs.ll) that check the actual solution, e.g. SIMPLE-DAG: stdin0 -> #x80.

5. Minor

• Scalable vectors crash on cast<FixedVectorType>. A dyn_cast plus a warning would treat them as concrete, as the description intends.
• A constant extractelement/insertelement index past the last lane (which yields poison) produces an out-of-range offset.
• coding_style CI fails: please run git clang-format --style LLVM.
• The branch carries #189's commit and two merge commits; a rebase once #189 lands will make it easier to review.
• The pre-existing file_input.c UNRESOLVED failure is unrelated: recent lit releases (23.x on PyPI) removed the %T substitution; using %t.input instead of %T/%basename_t.input fixes it.

[aurelf]

🤖 (Claude) This builds vectors like structs: each lane byte-swapped, lane 0 in the most significant bits. Vectors loaded from memory use the opposite layout on little-endian targets (isLittleEndian() is true for vector types, so _sym_read_memory puts byte 0 in the least significant bits, like bitcast to i128). Suggest building the vector as that integer instead: no per-lane bswap, and concatenate from lane N-1 down to lane 0 on little-endian. See item 1 of the review summary.

[aurelf]

🤖 (Claude) _sym_build_extract with byte offsets assumes the struct layout (offset 0 = most significant byte). For a vector that came from a load, offset 0 is lane N-1, byte-swapped. Probe: load <4 x i32> → extractelement 0 → == 0x11223344 makes the solver constrain stdin12..15 instead of stdin0..3. Also, a constant index ≥ the number of lanes (poison) gives an out-of-range offset here.

[aurelf]

🤖 (Claude) The per-lane decomposition is the right idea, but lanes are extracted with the struct layout. On a loaded vector the scalar op therefore runs on byte-reversed lane values. Probe: load → add v, v → store → load i32 → == 256 produces stdin2 = 0x80 (wrong: the carry goes the wrong way). The bitwise fast path is fine as long as both operands use the same layout.

[aurelf]

🤖 (Claude) This produces an N-bit result for <N x i1>, but extract/insert/shuffle on <N x i1> use byte offsets with elementSize = 1 (store size of i1), and the undef case gives getTypeStoreSize() bytes. Those sizes don't agree, and _sym_build_extract's totalBits % 8 == 0 assert is compiled out in release builds. Also, sext <N x i1> (what C vec == ... produces) goes to visitCastInst, which calls getIntegerBitWidth() on the vector type.

[aurelf]

🤖 (Claude) cast<FixedVectorType> crashes on scalable vectors. A dyn_cast returning early (with the usual warning) would treat the value as concrete instead. The same applies at the other cast<FixedVectorType> sites.

[aurelf]

🤖 (Claude) Nit: copied from the struct case. This comment should say vectors.

[aurelf]

🤖 (Claude) At -O1 clang scalarizes almost all of this. In the emitted IR, the only vector instructions left are the insertelement chain and the variable-index extractelement, so the add/mul/xor/shuffle/compare paths aren't exercised. The CHECK lines also only require Found diverging input, not a correct solution. Hand-written .ll tests that check the solved bytes would catch the layout issue (see test/vector_endianness.ll).

[aurelf]

Thanks for the PR!
See above for the heavily Claude assisted review. I spent a bit of time to look a those, and they seem legit to me. Also, there is a bit code test I'm doing a PR to your branch as it seems I cannot commit to it directly.
Would be nice if you also fix the minor coding style issue.