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 2605280. Co-authored-by: Giuliano Losa <giuliano@galois.com>
GaloisInc · Jan 14, 2022 · 1509f47 · 1509f47
1 parent 519c2ed
commit 1509f47
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 8 deletions.
diff --git 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
@@ -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
@@ -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"