Skip to content

Commit

Permalink
Upgrade proof tool submodules (#102)
Browse files Browse the repository at this point in the history
* Upgrade proof tool submodules

This commit advances Litani to release 1.10.0, and the starter kit to
the tip-of-tree. This brings the following improvements:

- Profiling
    - Litani measures the memory usage of the CBMC safety checking and
      coverage checking jobs
    - The dashboard includes box-and-whisker diagrams for memory use per
      proof
    - The dashboard includes a graph of how many parallel jobs are
      running over the whole run, making it easy to choose a CI machine
      with enough parallelism
    - It is now possible to designate particular proofs as "EXPENSIVE";
      Litani runs expensive proofs serially, ensuring that they do not
      over-consume resources like RAM.

- UI improvements
    - Each pipeline page includes a table of contents
    - Each pipeline page includes a dependency graph of the pipeline
    - Each job on the pipeline page has a hyperlink to that job
    - The terminal output is now less noisy

* Symlink run-cbmc-proofs.py to starter kit

The run script is now a symbolic link into the starter kit submodule,
meaning that it will be updated whenever the starter kit is. This is
done iso that E-SDK doesn't carry custom modifications to the run script
unless necessary; previous commits have made the E-SDK proofs consistent
with the generic starter kit conventions.

Co-authored-by: Paul Bartell <[email protected]>
  • Loading branch information
karkhaz and paulbartell authored Jul 16, 2021
1 parent 53194dc commit 9066f2c
Show file tree
Hide file tree
Showing 4 changed files with 4 additions and 260 deletions.
1 change: 1 addition & 0 deletions test/cbmc/.gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ proofs/**/gotos
proofs/**/report
proofs/**/html
proofs/**/core_json.c
proofs/output

# Emitted by CBMC Viewer
TAGS-*
Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/aws-templates-for-cbmc-proofs
2 changes: 1 addition & 1 deletion test/cbmc/litani
Submodule litani updated 55 files
+9 −4 .gitignore
+91 −0 CHANGELOG
+9 −4 README.md
+20 −3 bin/validate-run
+78 −0 doc/bin/build-html-doc
+30 −0 doc/bin/uniquify-header-ids
+143 −0 doc/configure
+0 −4 doc/foot.html
+0 −124 doc/head.html
+0 −393 doc/index.md
+0 −12 doc/litani-flow.dot
+158 −0 doc/src/man/litani-add-job.scdoc
+77 −0 doc/src/man/litani-init.scdoc
+49 −0 doc/src/man/litani-run-build.scdoc
+396 −0 doc/templates/index.jinja.html
+8 −1 lib/capabilities.py
+112 −20 lib/graph.py
+235 −0 lib/job_outcome.py
+5 −1 lib/litani.py
+306 −80 lib/litani_report.py
+194 −0 lib/ninja.py
+306 −0 lib/process.py
+152 −0 lib/validation.py
+191 −200 litani
+0 −62 litani-progress
+29 −12 templates/dashboard.jinja.html
+38 −0 templates/memory-peak-box.jinja.gnu
+40 −0 templates/memory-trace.jinja.gnu
+223 −0 templates/outcome_table.jinja.html
+450 −14 templates/pipeline.jinja.html
+38 −0 templates/run-parallelism.jinja.gnu
+1 −2 templates/runtime-box.jinja.gnu
+6 −0 test/README
+0 −0 test/__init__.py
+71 −0 test/e2e/README
+145 −0 test/e2e/run
+0 −0 test/e2e/tests/__init__.py
+42 −0 test/e2e/tests/cwd.py
+63 −0 test/e2e/tests/no_pool_serialize.py
+53 −0 test/e2e/tests/no_pool_serialize_graph.py
+40 −0 test/e2e/tests/no_timed_out.py
+48 −0 test/e2e/tests/no_timed_out_timeout_ignored.py
+48 −0 test/e2e/tests/no_timed_out_timeout_ok.py
+76 −0 test/e2e/tests/pool_serialize.py
+57 −0 test/e2e/tests/pool_serialize_graph.py
+39 −0 test/e2e/tests/single_pool.py
+40 −0 test/e2e/tests/timed_out.py
+49 −0 test/e2e/tests/timed_out_timeout_ignored.py
+48 −0 test/e2e/tests/timed_out_timeout_ok.py
+22 −8 test/e2e/tests/zero_pool.py
+169 −0 test/run
+0 −0 test/unit/__init__.py
+0 −0 test/unit/lockable_directory.py
+263 −0 test/unit/outcome_table_decider.py
+43 −0 test/unit/status_parser.py
258 changes: 0 additions & 258 deletions test/cbmc/proofs/run-cbmc-proofs.py

This file was deleted.

1 change: 1 addition & 0 deletions test/cbmc/proofs/run-cbmc-proofs.py

0 comments on commit 9066f2c

Please sign in to comment.