Integrate experimental Go frontend with symbolic semantic expectations

[CaelmBleidd]

The original Go prototype only checked execution and instruction coverage. This integration adapts it to current main and tests input-dependent Go results, panics and mutations through the shared TestRunner. The reproduced failures are fixed, with selected results independently checked by native Go. The frontend remains experimental.

The prototype comes from buraindo/go-jacodb at 717bd41613fbc4bb8d8a0af43f3900bab824dcb8. Its Go-specific JacoDB API is separately pinned to 816194b963; other frontends retain their dependency. The branch is rebased onto main at 70a88e3d6a0156c4e7b40d912e9c1d31e9530a12.

Implementation

• Adapt the frontend to modern USVM, including frontend-local pointer targets and slice backing/offset/length/capacity metadata, cloning and merge guards.
• Fix integer width, signedness, unary/named numeric values, finite representable numeric conversions and float-literal precision.
• Preserve nil maps, absent-key zero values, comma-ok, deletion and range; assignment to a nil map still panics.
• Constrain valid input representations and retain symbolic input-memory expressions when resolving snapshots. Refine oversized witnesses within their original path constraints; report unsupported when no model fits the 10,000-element materialization limit.
• Copy arrays and structs on stores, calls, interface boxing, map insertion/lookup, copy and append, including nested values. Composite slice copies read a source snapshot one element per machine step, preserving overlapping ranges and symbolic lengths under the normal budgets. Pointer fields inside copied structs keep their shared pointee; scalar-pointer conversions preserve nil and round-trip equality.
• Capture deferred-call arguments at registration and keep a separate defer stack for each invocation, including recursion.
• Produce type-specific zero values for missing map entries and failed comma-ok assertions; panic for failed non-comma assertions. Use the implementation direction for interface assertions and export separate value/pointer method sets. Dispatch interface methods across admissible concrete receivers, including typed nil pointer panics. Values do not inherit pointer-receiver methods, and pointers to interfaces do not inherit interface methods.
• Compare named nilable values through their payload. Reject negative narrow signed indices before widening, and panic on stores through symbolic nil pointers.
• Check slice bounds directly, avoiding overflow in limit + 1.
• Generate SSA fixtures, native oracles and replay executables under build/generated/go using pinned Go 1.22.3; add bounded ci-go validation.

Tests and local validation

All 103 original examples have explicitly registered semantic tests in thematic packages for arithmetic, arrays, maps, slices, strings, control flow, calls, exceptions, globals, objects, pointers, types and algorithms. Catalog checks require one registration per sample and a native oracle for every constant regression.

checkDiscoveredProperties requires a witness for each expected property and checks that every collected execution satisfies an expectation. checkMatches additionally requires a one-to-one match. Mutation checks inspect snapshots before and after the call.

• 237 default tests and 5 manual tests pass, with no skipped tests.
• 108 constant scalar/panic cases compare with native Go.
• Generated-input replay checks execute 19 inputs for branch, slice-alias, named-number/interface and symbolic composite-copy/append samples, plus six original array/slice/pointer/object/map examples. They compare return values, panic occurrence and argument snapshots after execution. The latest manual map replay checks 100 generated inputs against the original mapLoopLen.
• Add 36 review regressions in the thematic defer/interface/map/slice/pointer packages: 28 native scalar/panic comparisons and 8 symbolic/helper checks.
• Detekt on main/test Go sources reports zero findings; gofmt, validateProjectList and git diff --check pass. Native replay process handling is shared, and non-obvious Kotlin literals use named arguments.
• The 4 primitive-map core tests pass again. Shared core map additions also retain the earlier local validation with 11 object-map tests.

The mapLoopLen expectation now follows the source's zero-initialized keys instead of assuming max-minus-min with an added zero. Native replay checks this behavior independently. assertCreatureFailNoComma allows partial instruction coverage because its guaranteed assertion panic makes the following return unreachable; every execution must still panic. Existing bounded manual/unreachable-loop exceptions retain their semantic checks.

./gradlew :usvm-go:check :usvm-go:detektMain :usvm-go:detektTest validateProjectList --configure-on-demand
./gradlew :usvm-go:manualTest --configure-on-demand

These are bounded local observations: exploration uses finite timeouts and a 100-state limit. CI for the updated commit is tracked separately.

Review focus and boundaries

Review input-shape constraints and model refinement, value copying, pointer conversion metadata, interface dispatch, primitive-map invariants and the separately pinned Go JacoDB dependency.

Channels/goroutines/select, unsafe and several conversions remain unsupported. Full rune/UTF-8 iteration and preservation of invalid UTF-8 in resolved text are incomplete. Float-to-integer validation covers finite representable values. Collection sizes use a nonnegative BV32 domain and input slice capacity equals length. External calls and function inputs retain prototype mocks; resolved snapshots and JSON replay do not preserve arbitrary alias graphs. General pointer/interface identity, reference map keys, standard-library integration and arbitrary-project workflows need broader validation. Map-zero regressions cover selected structs, arrays and named scalars; nil-map regressions currently cover integer keys/values. See usvm-go/README.md.