Skip to content

CBMC: Allow specification of timeouts #733

@hanno-becker

Description

@hanno-becker

When CBMC proofs blow up in CI, it is very tedious to find out which function(s) are actually the problematic ones. One needs to crawl through the log and reverse engineer from the presence of successful steps which functions have not completed.

Task:

  • Modify run-cbmc-proofs.py so one can pass a per-proof timeout
  • Set the proof timeout in CI to 30min (for now) and report "TIMEOUT" in the result table upon timeout, so one can always inspect the table in the CI results to see which functions were problematic.

30min is larger than what we'd want in CI, but it is still useful to know whether a proof works in principle, but is just slow. It is also good enough to prevent the CI from running for hours and wasting money on a failing / inacceptably long proof.

Acceptance Criteria:

  • run-cbmc-proofs.py has an additional `--per-proof-timeout argument which defaults to 1800s (30min) and bounds the amount of time spent on a fixed proof.
  • When a proof times out, the corresponding entry in the summary table is "TIMEOUT" rather then "XXX s" upon success.
  • If at least one proof times out, the return value of run-cbmc-proofs.py is non-zero.
  • tests cbmc has an additional --per-proof-timeout argument which is passed on to run-cbmc-proofs.py
  • CI is adjusted to CBMC proofs run with timeout of 30min; this should be spelled out explicitly even though it's also the implicit default.
  • A local test of tests cbmc --per-proof-timeout=15 has been run to confirm that the mechanism works, and that the return value upon any timeout is non-zero.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions