Skip to content

Commit

Permalink
Update proof tools (+disable submodule cloning by default) (#20)
Browse files Browse the repository at this point in the history
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
  • Loading branch information
sukhmanm authored Jul 20, 2021
1 parent 1b7a37a commit 2e4bd59
Show file tree
Hide file tree
Showing 4 changed files with 6 additions and 2 deletions.
3 changes: 3 additions & 0 deletions .gitmodules
Original file line number Diff line number Diff line change
@@ -1,9 +1,12 @@
[submodule "test/unit-test/CMock"]
path = test/unit-test/CMock
url = https://github.com/ThrowTheSwitch/CMock.git
update = none
[submodule "test/cbmc/aws-templates-for-cbmc-proofs"]
path = test/cbmc/aws-templates-for-cbmc-proofs
url = https://github.com/awslabs/aws-templates-for-cbmc-proofs.git
update = none
[submodule "test/cbmc/litani"]
path = test/cbmc/litani
url = https://github.com/awslabs/aws-build-accumulator
update = none
1 change: 1 addition & 0 deletions test/cbmc/.gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ proofs/**/logs
proofs/**/gotos
proofs/**/report
proofs/**/html
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

0 comments on commit 2e4bd59

Please sign in to comment.