CBMC backend: missing multi-return support, and the unimplemented-feature error is silently swallowed

[PROgram52bc]

CBMC backend: missing multi-return support, and the unimplemented-feature error is silently swallowed

Summary

Two related problems in the CBMC GOTO backend (Strata/Backends/CBMC/GOTO/):

1. Missing feature. CoreToGOTO.transformToGoto cannot translate Strata Core procedures with more than one output parameter. It correctly recognizes this and throws Translation for multi-return value Strata Core procedures is unimplemented.
2. Silent-failure regression. That error (and several other intentional throws in transformToGoto) is swallowed by CoreToGOTO.getGotoJson. The error message is emitted via dbg_trace, the function returns an empty CProverGOTO.Json, and the downstream writeToGotoJson writes null to both output files. The StrataCoreToGoto binary exits with code 0. A script or CI job has no way to detect that translation failed.

The combined effect is that any program with a multi-output procedure produces JSON files that look superficially valid (they exist, they're written successfully), but contain null. CBMC consuming them either crashes or proceeds with no model — either way, no verification happens, but no failure signal propagates.

Reproduction

Tested on main at commit f6d195aa.

multi_out.core.st:

program Core;

procedure multi_out(out a : int, out b : int)
{
  a := 1;
  b := 2;
};

$ lake build StrataCoreToGoto
$ .lake/build/bin/StrataCoreToGoto --output-dir ./out ./multi_out.core.st
[Strata.Core] Type Checking Succeeded!
[transformToGoto] Translation for multi-return value Strata Core procedures is unimplemented.
Written ./out/multi_out.symtab.json and ./out/multi_out.goto.json
$ echo "exit=$?"
exit=0
$ cat ./out/multi_out.goto.json
null

The exit status is 0 and the output files exist on disk. The only signal of failure is an unattributed line on stderr, which any non-interactive consumer will discard.

Why missing multi-return support matters

Strata Core procedures naturally have multiple outputs in two scenarios:

• Explicit multi-output Boogie/Core procedures (procedure f(...) returns (a: int, b: int) in Boogie / out a, out b in Core). Common in proof obligations that pair a value with a status flag.
• BoogieToStrata's inout lowering of Boogie modifies. Each modified global becomes an inout parameter, which by Strata Core convention appears in BOTH Procedure.Header.inputs AND .outputs (see Strata/Languages/Core/StatementType.lean:25-30 and Strata/Languages/Core/DDMTransform/Translate.lean:1582-1585). A procedure that modifies two globals therefore has two outputs.

The downstream consequence: as soon as the CBMC backend is used on Boogie input that touches more than one global, it hits the outputs.length > 1 guard. Real-world Boogie code rarely touches only one global.

Why CBMC's GOTO can't represent multi-return directly

GOTO's calling convention has a single return-value channel: FUNCTION_CALL carries one lhsExpr and SET_RETURN_VALUE carries one value. C has the same restriction. To encode multiple outputs, the translation needs to use one of:

1. Pointer parameters. Each output past the first becomes a T* parameter; reads in the body become dereferences. C-idiomatic and aligns with CBMC's contract framework (DFCC).
2. Struct return. Synthesize a struct type per multi-output procedure, return it as a single value, unpack at each call site. Mechanically simple — no body-level type changes; CBMC handles structs natively.
3. Globals. Synthesize one global per output, callee writes there, caller reads after the call. Workable but loses re-entrancy.
4. Hybrid. First output via lhsExpr, rest as pointer parameters. Preserves single-output emission bit-for-bit; asymmetric body translation.
5. Procedure inlining at translation time. Replace each call to a multi-output procedure with its inlined body. Avoids the calling-convention question; pays code blowup; doesn't support recursion.
6. Modular contract abstraction. Replace the call with havoc(out1); havoc(out2); assume(postcondition);. Sound when the callee has a verified contract; appropriate for DFCC-style modular verification.

For unblocking near-term use, options (1) or (2) are the principled directions. Option (5) sidesteps the issue if the callee is non-recursive and code-size growth is acceptable.

Suggested fixes

Short-term (silent-failure fix)

Strata/Backends/CBMC/GOTO/CoreToCProverGOTO.lean:250-258:

def getGotoJson (programName : String) (env : Program) : IO CProverGOTO.Json := do
  let (program, errors) := TransM.run Inhabited.default (translateProgram env)
  if errors.isEmpty then
    (match (CoreToGOTO.transformToGoto program) with
      | .error e =>
        dbg_trace s!"{e}"           -- should be IO.eprintln + throw
        return {}                    -- swallows the error
      | .ok ctx =>
        IO.ofExcept (CProverGOTO.Context.toJson programName ctx))
  else
    throw (IO.userError s!"DDM Transform Error: {repr errors}")

The dbg_trace s!"{e}"; return {} arm should be replaced with throw (IO.userError s!"{e}") so the failure surfaces as a non-zero exit code from the binary and a propagating exception in any library consumer. The DDM-transform branch already does this correctly — the post-translation branch should match.

This is small, mechanical, and would have caught the missing-feature gap as a hard error in CI rather than as a silent null artifact.

Medium-term (feature)

Implement multi-return support in transformToGoto. Recommended: struct return (option 2 above). Since it is mechanical, requires no body-level type changes, and CBMC handles it natively.

If a Strata-level pre-pass is preferred (lower multi-output procedures to single-output before reaching the backend), that keeps the backend's contract simple and is reusable across other backends.

Other intentional throws currently swallowed by the same dbg_trace arm

The same swallowing path silences these transformToGoto errors as well — all of them produce null JSON files with exit=0:

• Translation for polymorphic Strata Core procedures is unimplemented. (line 202)
• We can process only Strata Core procedures at this time. (line 196)
• We can process Strata Core commands only, not statements! (line 207)
• We can transform only a single Strata Core procedure to GOTO at a time! (line 246)

Fixing the silent-failure path covers all of them at once.

Repro artifacts

out/multi_out.core.st (the 7-line program above) is sufficient to reproduce. Run on a clean checkout of main:

lake build StrataCoreToGoto
.lake/build/bin/StrataCoreToGoto --output-dir ./out ./multi_out.core.st
echo "exit=$?"        # → 0  (should be non-zero)
cat ./out/multi_out.goto.json   # → null  (should not have been written)