SQL fault injection in the equivalence harness (#4173); LINK COMMAREA bounded to the caller's record (#4181)

[squid-protocol]

Fixes #4173, Fixes #4181

SQL fault injection (#4173)

• Key. Each EXEC SQL statement is keyed PROGRAM:LINE: its line in the file it is written in, which for an INCLUDEd member is the member's own line. The precompiler writes the key into the statement table, and every det-port DetSql call carries the same one.

• Injection, both sides. A fault plan (PROGRAM LINE NTH SQLCODE SQLSTATE) makes that execution skip Db2, with the planned SQLCODE and SQLSTATE: tests/equivalence/db2/ggsql.c ($GGSQL_FAULTS) on the COBOL side, DetSql.withFaults / gitgalaxy.sqlfaults.plan on the Java side. Both log what fired, and a run proves only if the same faults fired on both sides.

• Enumeration. equivalence.py run --sql-faults auto|declared|none, default auto. Auto adds one task (CICS) or run (batch) per statement the case actually executed, its first execution failing:

  Statement	Injected SQLCODE
  INSERT	-803
  SELECT INTO	+100
  UPDATE, DELETE, OPEN, FETCH	-913
  COMMIT, CLOSE, SET :H = VALUES	none

  A scenario may also declare its own sql_faults, by line or by table + verb.

• Not judged, rather than faked:

  • A fault task that LINKs to a program the case doesn't run (GenApp's LGSTSQ, X6) is judged up to and including that LINK, with the COMMAREA bytes compared byte for byte; its end state is not compared.
  • A task that reaches a det port's named hole (COTRTLIC's dynamic CALL) is recorded "not judged" and left out of both the proof and the coverage figure.
  • So is a fault task on a port without DetSql (a model port). Its base scenarios still prove.

#4181, and what the faults found

• A LINK whose area is shorter than the target's contract DTO read past the caller's record (GenApp's 71-byte ERROR-MSG, LINKed as the 99-byte CA-ERROR-MSG). Cobol.commarea / commareaBack now give the target the caller's bytes up to the end of its record, and LOW-VALUES past it (register X10).
• The first fault runs then found a second bug. The contract DTO, typed from another caller's record, dropped the bytes it doesn't name: ERROR-MSG's date, which falls under CA-ERROR-MSG's FILLER. A det caller now passes the area's bytes themselves (CicsTask.link(..., area)), and a det target overlays them on DFHCOMMAREA and writes back. The LGSTSQ COMMAREA now matches byte for byte.
• Register X11 (new). GenApp's ASKTIME writes ABSTIME into an S9(8) COMP field, so both sides date the error message 01011900. They agree, so no verdict changes, but z/OS would not give that date.

Coverage before → after (det sweep, --faults all)

Case	Branches before	Branches after
genapp-lgacdb01	6/14	8/14 (4/4 paragraphs)
genapp-lgupdb01	17/38	26/38
genapp-lgapdb01	13/31	17/31
genapp-lgucdb01	2/10	4/10
genapp-lgipdb01	46/74	48/74
genapp-lgacdb02 / lgdpdb01	4/10, 5/12	5/10, 6/12
cbsa-delacc	10/14	13/14
cbsa-dbcrfun	22/35	25/35
cbsa-inqacc	13/25	15/25
cbsa-updacc	5/6	6/6
cbsa-xfrfun	44/81	46/81
carddemo-cobtupdt (batch)	14/20	16/20
carddemo-cotrtupc	124/166	126/166
carddemo-cotrtlic	165/230	165/230 (9 fault tasks not judged: dynamic-CALL hole)
cbsa-custctrl, genapp-lgicdb01	unchanged	unchanged

Verification

• Det sweep: proof_sweep.py --det-only --jobs 4: "as expected", 48/50 (the same two KNOWN_UNPROVEN). Run on the final commit.
• Model sweep: 23/23 proven, "as expected".
• Model port with faults: [needs Joe's review] Model ports beyond CardDemo: CBSA UPDACC, GenApp LGICDB01, LGAPVS01 #4187's UPDACC port proves its base scenarios; its two fault tasks are "not judged (no SQL fault hook)".
• Tests: tests/cobol_mainframe, tests/cics_crucible and tests/test_source_reads.py: 1304 passed. The new test_sql_faults.py passes (6 tests). ruff_audit --ci is clean.

Register (oracle_assumptions.md)

• M2 now says MATCHED, with the SQLCA assumed. A fault leaves reset's SQLCA: SQLERRMC empty, SQLERRD zero. -913 rolls back the statement only.
• X6: the judged-to-the-LINK rule.
• X10 and X11: new.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ

[github-actions]

🐦‍⬛ Muninn Security Scan

✅ No security issues found.

🐦‍⬛ Powered by Muninn · Skald Lab