From 1509f47716a1fa7b879f545f5a67e5d79645005f Mon Sep 17 00:00:00 2001
From: Brett Boston <bboston7@users.noreply.github.com>
Date: Fri, 14 Jan 2022 10:27:52 -0800
Subject: [PATCH] Publish html-summary script output to Github pages (#71)
* fix paths
* use method names in summary
* change "loc" to "description" in html summary
* add memory-safety html summary
* use dependency "names" instead of numbers
* add functional_proofs.html (as example html output)
* Publish html-summary output on github pages
* Remove example files
* Cleanup HTML dependencies file name
* Temporarily ignore Yices TLS certificate expiration
* Always return 0 on *_dependencies.html copy in CI
* Configure ghpages not to clobber existing files on docs update
* Revert "Temporarily ignore Yices TLS certificate expiration"
This reverts commit 26052801ab62d64eb842a09002b66c53fd76425c.
Co-authored-by: Giuliano Losa <giuliano@galois.com>
---
.github/workflows/ci.yml | 2 ++
scripts/html_summary.py | 18 +++++++++++-------
scripts/prove.sh | 3 ++-
3 files changed, 15 insertions(+), 8 deletions(-)
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 8508b37d..4874d45b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -33,10 +33,12 @@ jobs:
- run: |
sudo chown -R $USER:$(id -gn $USER) build
jq -r '.[]' < <(cat build/*_output.json) | jq -s '.' | jq '. |= unique' > docs/output.json
+ cp build/*_dependencies.html docs || true
- uses: peaceiris/actions-gh-pages@v3
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
publish_dir: ./docs
+ keep_files: true
# - name: "Post Summary on PR"
# uses: actions/github-script@v3
# if: github.event_name == 'pull_request'
diff --git a/scripts/html_summary.py b/scripts/html_summary.py
index 2eecda5d..618e996e 100755
--- a/scripts/html_summary.py
+++ b/scripts/html_summary.py
@@ -9,6 +9,7 @@
import json
import sys
+import re
class DiGraph():
'''Barely-functional version.'''
@@ -179,17 +180,19 @@ def show_assumptions(f):
# goes to https://github.com/GaloisInc/BLST-Verification/blob/main/proof/foo.saw#Lnnn
def pathname_to_uri(p):
- a = p.split('/')[-1]
- b = a.split(':')
- if len(b) < 2:
+ a = p.split(':')
+ b = re.findall(r'proof/(.*)', a[0])
+ if len(a) < 2:
# raise Exception('Too few colons in %s => %s'%(p,a))
return None
- return 'https://github.com/GaloisInc/BLST-Verification/blob/main/proof/%s#L%s'%(b[0], b[1])
+ if len(b) == 0:
+ return None
+ return 'https://github.com/GaloisInc/BLST-Verification/blob/main/proof/%s#L%s'%(b[0], a[1])
def show_method_summaries_html_1(s, f = sys.stdout):
'''Shows which assumptions are used (even if via some intermediary)'''
print ('<html><body><table>', file=f)
- print ('<tr> <th> loc </th> <th> assumptions used</th></tr>', file=f)
+ print ('<tr> <th> description </th> <th> assumptions used</th></tr>', file=f)
uris = [pathname_to_uri(e['loc']) for e in s]
G = summary_event_digraph(s).transitive_closure()
for i, e in enumerate(s):
@@ -209,6 +212,7 @@ def show_method_summaries_html(s, f = sys.stdout, deps_per_row=10, only_items =
print ('<html><head><style> table, th, td {border: 1px solid black;}</style><body><table>', file=f)
print ('<tr> <th> loc </th> <th> assumptions used</th></tr>', file=f)
uris = [pathname_to_uri(e['loc']) for e in s]
+ descriptions = [(e['method'] if e['type']=='method' else e['type']+"-"+str(i)) for i, e in enumerate(s)]
G = summary_event_digraph(s).transitive_closure()
for i, e in enumerate(s):
# if only_items is None and (e['type'] != 'method' or G.indegree(i) > 0): continue
@@ -220,7 +224,7 @@ def show_method_summaries_html(s, f = sys.stdout, deps_per_row=10, only_items =
dep_p.append(d)
dep_p.sort()
nrows = (len(dep_p) + deps_per_row - 1)//deps_per_row
- print('<tr><td rowspan=%d> <a href="%s"> %d </a> </td>'% (nrows, uris[i], i), file=f)
+ print('<tr><td rowspan=%d> <a href="%s"> %s </a> </td>'% (nrows, uris[i], descriptions[i]), file=f)
n = 0
first_row = True
for d in dep_p:
@@ -230,7 +234,7 @@ def show_method_summaries_html(s, f = sys.stdout, deps_per_row=10, only_items =
first_row=False
else:
print('<tr><td>', file=f)
- print (', ' if n > 0 else '', '<a href="', uris[d], '">', d, '</a>', file=f)
+ print (', ' if n > 0 else '', '<a href="', uris[d], '">', descriptions[d], '</a>', file=f)
n = (n+1)%deps_per_row
if n==0: print('</td></tr>', file=f)
if n>0:
diff --git a/scripts/prove.sh b/scripts/prove.sh
index 7ad53261..7b8de2aa 100755
--- a/scripts/prove.sh
+++ b/scripts/prove.sh
@@ -18,7 +18,8 @@ for f in $files; do
patch -f -p1 -t < patches/blst_bulk_addition_saw_cryptol/changes.patch
fi
saw "$f" -s "$summary_file" -f json
- python3 scripts/html_summary.py "$summary_file" -o "build/$(basename $f)_dependencies.html"
+ dependencies_html=$(printf '%s' "build/${f}_dependencies.html" | sed -e 's/\.saw//' -e 's!/proof/!/!')
+ python3 scripts/html_summary.py "$summary_file" -o "$dependencies_html"
done
echo "All functions under verification were verified successfully"