Heapster: remove generated coq files

.github/workflows/ci.yml

@@ -173,7 +173,7 @@ jobs:
           name: "saw-${{ runner.os }}-${{ matrix.ghc }}"
           path: "dist/bin/saw"
 
-  ocaml-tests:
+  heapster-tests:
     needs: [build]
     strategy:
       fail-fast: false
@@ -193,6 +193,12 @@ jobs:
           name: "${{ runner.os }}-bins"
           path: dist/bin
 
+      - name: Update PATH to include SAW
+        shell: bash
+        run: |
+          chmod +x dist/bin/*
+          echo $GITHUB_WORKSPACE/dist/bin >> $GITHUB_PATH
+
       - uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: 4.09.x  # coq-bits claims to support < 4.10 only
@@ -201,11 +207,16 @@ jobs:
 
       - run: opam install --unlock-base -y coq=8.12.2 coq-bits=1.0.0
 
+      # FIXME: the following builds the Coq libraries for the SAW core
+      # to Coq translator; if we do other Coq tests, this should become
+      # its own build artifact, to avoid downloading it twice
       - working-directory: saw-core-coq/coq
-        run: PATH="$PWD/dist/bin:$PATH" opam exec -- make -j
+        shell: bash
+        run: opam exec -- make -j
 
       - working-directory: heapster-saw/examples
-        run: PATH="$PWD/dist/bin:$PATH" opam exec -- make -j
+        shell: bash
+        run: opam exec -- make -j
 
   saw-remote-api-tests:
     runs-on: ${{ matrix.os }}
@@ -496,7 +507,7 @@ jobs:
     runs-on: ubuntu-latest
     needs:
       - build
-      - ocaml-tests
+      - heapster-tests
       - saw-remote-api-tests
       - cabal-test
       - build-push-image

heapster-saw/examples/.gitignore

@@ -1,2 +1,3 @@
 Makefile.coq*
 .Makefile.coq*
+*_gen.v

heapster-saw/examples/Makefile

@@ -5,56 +5,28 @@ Makefile.coq: _CoqProject
 
 include Makefile.coq
 
-# If the saw executable is available, use it, otherwise fall back on cabal run saw
-SAW=$(shell which saw || echo cabal run saw)
+# If running in CI, always set $SAW=`which saw`. Otherwise, if saw is not in the
+# current path, fall back on cabal run saw
+SAW=$(shell which saw)
+ifeq ($(SAW),)
+  ifeq ($(CI),)
+	    SAW=cabal run saw
+  else
+    $(error Could not find SAW executable; PATH = $(PATH))
+  endif
+endif
 
 %.bc: %.c
 	clang -emit-llvm -g -c $<
 
-linked_list.v: linked_list.bc linked_list.saw linked_list.sawcore
-	$(SAW) linked_list.saw
-
-xor_swap.v: xor_swap.bc xor_swap.saw
-	$(SAW) xor_swap.saw
+%_gen.v: %.saw %.bc
+	$(SAW) $<
 
 xor_swap_rust.bc: xor_swap_rust.rs
 	rustc --crate-type=lib --emit=llvm-bc xor_swap_rust.rs
 
-xor_swap_rust.v: xor_swap_rust.bc xor_swap_rust.saw
-	$(SAW) xor_swap_rust.saw
-
-string_set.v: string_set.bc string_set.saw string_set.sawcore
-	$(SAW) string_set.saw
-
-loops.v: loops.bc loops.saw loops.sawcore
-	$(SAW) loops.saw
-
-arrays.v: arrays.bc arrays.saw arrays.sawcore
-	$(SAW) arrays.saw
-
-iter_linked_list.v: iter_linked_list.bc iter_linked_list.saw iter_linked_list.sawcore
-	$(SAW) iter_linked_list.saw
-
-iso_recursive.v: iso_recursive.bc iso_recursive.saw iso_recursive.sawcore
-	$(SAW) iso_recursive.saw
-
-memcpy.v: memcpy.bc memcpy.saw memcpy.sawcore
-	$(SAW) memcpy.saw
-
 rust_data.bc: rust_data.rs
 	rustc --crate-type=lib --emit=llvm-bc rust_data.rs
 
-rust_data.v: rust_data.bc rust_data.saw
-	$(SAW) rust_data.saw
-
 rust_lifetimes.bc: rust_lifetimes.rs
 	rustc --crate-type=lib --emit=llvm-bc rust_lifetimes.rs
-
-rust_lifetimes.v: rust_lifetimes.bc rust_lifetimes.saw
-	$(SAW) rust_lifetimes.saw
-
-clearbufs.v: clearbufs.bc clearbufs.saw clearbufs.sawcore
-	$(SAW) clearbufs.saw
-
-mbox.v: mbox.bc mbox.saw
-	$(SAW) mbox.saw

heapster-saw/examples/_CoqProject

@@ -2,28 +2,28 @@
 -Q ../../saw-core-coq/coq/handwritten/CryptolToCoq   CryptolToCoq
 -Q . Examples
 
-linked_list.v
+linked_list_gen.v
 linked_list_proofs.v
-xor_swap.v
+xor_swap_gen.v
 xor_swap_proofs.v
-xor_swap_rust.v
+xor_swap_rust_gen.v
 xor_swap_rust_proofs.v
-string_set.v
+string_set_gen.v
 string_set_proofs.v
-loops.v
+loops_gen.v
 loops_proofs.v
-iter_linked_list.v
+iter_linked_list_gen.v
 iter_linked_list_proofs.v
-iso_recursive.v
+iso_recursive_gen.v
 iso_recursive_proofs.v
-memcpy.v
+memcpy_gen.v
 memcpy_proofs.v
-rust_data.v
+rust_data_gen.v
 rust_data_proofs.v
-rust_lifetimes.v
+rust_lifetimes_gen.v
 rust_lifetimes_proofs.v
-arrays.v
-clearbufs.v
+arrays_gen.v
+clearbufs_gen.v
 clearbufs_proofs.v
-mbox.v
+mbox_gen.v
 mbox_proofs.v

heapster-saw/examples/arrays.saw

@@ -26,4 +26,4 @@ heapster_typecheck_fun env "filter_and_sum_pos" "(len:bv 64).arg0:array(0,<len,*
 heapster_gen_block_perms_hint env "sum_2d" [];
 heapster_typecheck_fun env "sum_2d" "(l1:bv 64,l2:bv 64).arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:eq(llvmword(l1)), arg2:eq(llvmword(l2)) -o arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:true, arg2:true, ret:exists x:bv 64.eq(llvmword(x))";
 
-heapster_export_coq env "arrays.v";
+heapster_export_coq env "arrays_gen.v";

heapster-saw/examples/arrays_proofs.v

@@ -11,7 +11,7 @@ From CryptolToCoq Require Import CompMExtra.
 
 Import SAWCorePrelude.
 
-Require Import Examples.arrays.
+Require Import Examples.arrays_gen.
 Import arrays.
 
 Import VectorNotations.

heapster-saw/examples/clearbufs.saw

@@ -10,4 +10,4 @@ heapster_block_entry_hint env "clearbufs" 3 "top1:llvmptr 64" "frm:llvmframe 64,
 
 heapster_typecheck_fun env "clearbufs" "().arg0:Bufs<llvmword(0)> -o arg0:Bufs<llvmword(0)>";
 
-heapster_export_coq env "clearbufs.v";
+heapster_export_coq env "clearbufs_gen.v";

heapster-saw/examples/clearbufs_proofs.v

@@ -8,7 +8,7 @@ From CryptolToCoq Require Import SAWCoreBitvectors.
 From CryptolToCoq Require Import SAWCorePrelude.
 From CryptolToCoq Require Import CompMExtra.
 
-Require Import Examples.clearbufs.
+Require Import Examples.clearbufs_gen.
 Import clearbufs.
 
 (* Eval cbn in clearbufs__tuple_fun. *)

heapster-saw/examples/iso_recursive.saw

@@ -7,4 +7,4 @@ heapster_define_irt_recursive_shape env "ListS" 64 "X:llvmshape 64" "(fieldsh(eq
 
 heapster_typecheck_fun env "is_elem" "(x:bv 64).arg0:eq(llvmword(x)), arg1:List<(exists y:(bv 64).eq(llvmword(y))),always,R> -o arg0:true, arg1:true, ret:exists z:(bv 64).eq(llvmword(z))";
 
-heapster_export_coq env "iso_recursive.v";
+heapster_export_coq env "iso_recursive_gen.v";