Skip to content

Commit 8bc5452

Browse files
authored
Upgrade CBMC proof tools: starter kit and Litani 1.10.0 (#722)
* 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 * Change cbmc-batch.yaml to cbmc-proof.txt This makes the proof layout consistent with the starter kit, which will allow us to use a generic run script in a future commit. Putting this in commit by itself because the diff is huge and not worth reading (just moving some files and changing two lines in the runscript). * 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.
1 parent f3c8412 commit 8bc5452

File tree

212 files changed

+108
-729
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

212 files changed

+108
-729
lines changed

verification/cbmc/.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ proofs/**/logs
33
proofs/**/gotos
44
proofs/**/report
55
proofs/**/html
6+
proofs/output
67

78
# Emitted by CBMC Viewer
89
TAGS-*

verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_clean_up/cbmc-batch.yaml

Lines changed: 0 additions & 17 deletions
This file was deleted.
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
This file marks the directory as containing a CBMC proof

verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_size/cbmc-batch.yaml

Lines changed: 0 additions & 17 deletions
This file was deleted.
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
This file marks the directory as containing a CBMC proof

verification/cbmc/jobs_dontrun/aws_cryptosdk_hdr_write/cbmc-batch.yaml

Lines changed: 0 additions & 17 deletions
This file was deleted.
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
This file marks the directory as containing a CBMC proof

verification/cbmc/jobs_dontrun/hdr_zeroize/cbmc-batch.yaml

Lines changed: 0 additions & 17 deletions
This file was deleted.
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
This file marks the directory as containing a CBMC proof

verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/cbmc-batch.yaml

Lines changed: 0 additions & 4 deletions
This file was deleted.

0 commit comments

Comments
 (0)