Make trace generation opt-in for all user interfaces - #9150
Open
tautschnig wants to merge 1 commit into
Open
Conversation
The JSON and XML interfaces enabled counterexample-trace generation unconditionally, while the plain interface requires --trace. Consumers of the structured interfaces that only need property verdicts pay a very large cost for traces they discard: for a Kani-generated standard library harness with 611 properties, of which 63 are expected-failure reachability (cover-style) checks, CBMC with --json-ui spends 296 seconds wall-clock where the same invocation with the plain interface takes 34 seconds. 82% of total CPU time goes to BigInt::as_string via integer2binary, serialising ~2 MB of JSON trace - dominated by the "binary" fields of constant values - for each expected failure. Make trace generation opt-in uniformly across the plain, JSON and XML interfaces, for both cbmc and jbmc: traces are generated when requested explicitly (--trace, --compact-trace, --stack-trace) or when a mode whose purpose is trace output is active (--stop-on-fail, --graphml-witness, --validate-trace). This is a behavioural change for JSON/XML consumers that relied on implicit traces; they need to pass --trace (as the plain interface always required). The --cover mode already disabled the implicit trace default, so the previous behaviour was not even uniform within the structured interfaces. Regression tests that relied on implicit traces under --xml-ui now pass --trace explicitly (xml-trace, xml-trace2, Float24, function-return-no-body1); a new test checks both that --json-ui alone produces no trace elements and that --json-ui --trace does. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
requested review from
TGWDB,
kroening and
peterschrammel
as code owners
August 4, 2026 11:23
There was a problem hiding this comment.
Pull request overview
This PR changes CBMC/JBMC CLI option handling so counterexample trace generation becomes opt-in consistently across the plain, JSON, and XML UIs, addressing major performance overhead for structured-output consumers that only need verdicts.
Changes:
- Remove the previous implicit “JSON/XML UI implies traces” behavior; traces are now enabled only by explicit trace flags (or trace-focused modes such as
--stop-on-fail/--graphml-witness/--validate-tracewhere applicable). - Update existing XML regression tests to pass
--traceexplicitly. - Add new CBMC regression tests to assert
--json-uiproduces no"trace"output unless--traceis provided.
Reviewed changes
Copilot reviewed 9 out of 9 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| src/cbmc/cbmc_parse_options.cpp | Removes implicit trace enabling for non-plain UIs; keeps trace opt-in via explicit flags / trace-oriented modes. |
| jbmc/src/jbmc/jbmc_parse_options.cpp | Mirrors CBMC’s opt-in trace behavior for JBMC, including --validate-trace. |
| regression/cbmc/xml-trace2/test.desc | Adds --trace to reflect new opt-in trace behavior for XML UI. |
| regression/cbmc/xml-trace/test.desc | Adds --trace to reflect new opt-in trace behavior for XML UI. |
| regression/cbmc/function-return-no-body1/test.desc | Adds --trace to reflect new opt-in trace behavior for XML UI. |
| regression/cbmc/Float24/test.desc | Adds --trace to reflect new opt-in trace behavior for XML UI. |
| regression/cbmc/json-ui-trace-opt-in/main.c | New minimal failing program used to exercise JSON trace presence/absence. |
| regression/cbmc/json-ui-trace-opt-in/test.desc | New test asserting --json-ui output does not include trace data unless requested. |
| regression/cbmc/json-ui-trace-opt-in/trace.desc | New test asserting --json-ui --trace includes trace data. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
313
to
317
| if( | ||
| cmdline.isset("trace") || cmdline.isset("compact-trace") || | ||
| cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") || | ||
| (ui_message_handler.get_ui() != ui_message_handlert::uit::PLAIN && | ||
| !cmdline.isset("cover"))) | ||
| cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail")) | ||
| { | ||
| options.set_option("trace", true); |
Comment on lines
172
to
176
| if( | ||
| cmdline.isset("trace") || cmdline.isset("compact-trace") || | ||
| cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") || | ||
| (ui_message_handler.get_ui() != ui_message_handlert::uit::PLAIN && | ||
| !cmdline.isset("cover"))) | ||
| cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail")) | ||
| { | ||
| options.set_option("trace", true); |
Comment on lines
+1
to
+6
| int main() | ||
| { | ||
| int x; | ||
| __CPROVER_assert(x != 42, "should fail with a counterexample"); | ||
| return 0; | ||
| } |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #9150 +/- ##
========================================
Coverage 80.83% 80.84%
========================================
Files 1715 1715
Lines 189948 189985 +37
Branches 73 73
========================================
+ Hits 153540 153584 +44
+ Misses 36408 36401 -7 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Collaborator
|
This is very much a breaking change; let's consider it for CBMC 7. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The JSON and XML interfaces enabled counterexample-trace generation unconditionally, while the plain interface requires --trace. Consumers of the structured interfaces that only need property verdicts pay a very large cost for traces they discard: for a Kani-generated standard library harness with 611 properties, of which 63 are expected-failure reachability (cover-style) checks, CBMC with --json-ui spends 296 seconds wall-clock where the same invocation with the plain interface takes 34 seconds. 82% of total CPU time goes to BigInt::as_string via integer2binary, serialising ~2 MB of JSON trace - dominated by the "binary" fields of constant values - for each expected failure.
Make trace generation opt-in uniformly across the plain, JSON and XML interfaces, for both cbmc and jbmc: traces are generated when requested explicitly (--trace, --compact-trace, --stack-trace) or when a mode whose purpose is trace output is active (--stop-on-fail, --graphml-witness, --validate-trace). This is a behavioural change for JSON/XML consumers that relied on implicit traces; they need to pass --trace (as the plain interface always required). The --cover mode already disabled the implicit trace default, so the previous behaviour was not even uniform within the structured interfaces.
Regression tests that relied on implicit traces under --xml-ui now pass --trace explicitly (xml-trace, xml-trace2, Float24, function-return-no-body1); a new test checks both that --json-ui alone produces no trace elements and that --json-ui --trace does.