Merge pull request #1060 from GaloisInc/remove-jvm-verifier

Remove dependency on jvm-verifier repository
GaloisInc · Feb 4, 2021 · f8449a1 · f8449a1
2 parents 1467987 + 8afdf33
commit f8449a1
Show file tree

Hide file tree

Showing 69 changed files with 41 additions and 446 deletions.
diff --git a/.github/ci.sh b/.github/ci.sh
@@ -41,15 +41,13 @@ setup_dist_bins() {
   if $IS_WIN; then
     is_exe "dist/bin" "saw" && is_exe "dist/bin" "saw-remote-api" && return
   else
-    is_exe "dist/bin" "saw" && is_exe "dist/bin" "saw-remote-api" && is_exe "dist/bin" "jss" && return
-    extract_exe "jss" "dist/bin"
+    is_exe "dist/bin" "saw" && is_exe "dist/bin" "saw-remote-api" && return
   fi
   extract_exe "saw" "dist/bin"
   extract_exe "saw-remote-api" "dist/bin"
   export PATH=$PWD/dist/bin:$PATH
   echo "$PWD/dist/bin" >> "$GITHUB_PATH"
   strip dist/bin/saw* || echo "Strip failed: Ignoring harmless error"
-  strip dist/bin/jss* || echo "Strip failed: Ignoring harmless error"
 }
 
 install_z3() {
@@ -126,9 +124,7 @@ build() {
   pkgs=(saw saw-remote-api)
   if $IS_WIN; then
     echo "flags: -builtin-abc" >> cabal.project.local
-    echo "constraints: jvm-verifier -builtin-abc, cryptol-saw-core -build-css" >> cabal.project.local
-  else
-    pkgs+=(jss)
+    echo "constraints: cryptol-saw-core -build-css" >> cabal.project.local
   fi
   echo "allow-newer: all" >> cabal.project.local
   tee -a cabal.project > /dev/null < cabal.project.ci
@@ -195,7 +191,7 @@ bundle_files() {
   cp doc/tutorial/sawScriptTutorial.pdf dist/doc/tutorial.pdf
   cp doc/manual/manual.pdf dist/doc/manual.pdf
   cp -r doc/tutorial/code dist/doc
-  cp deps/jvm-verifier/support/galois.jar dist/lib
+  cp intTests/jars/galois.jar dist/lib
   cp -r deps/cryptol/lib/* dist/lib
   cp -r examples/* dist/examples
 }

diff --git a/.gitmodules b/.gitmodules
@@ -13,9 +13,6 @@
 [submodule "deps/jvm-parser"]
 	path = deps/jvm-parser
 	url = https://github.com/GaloisInc/jvm-parser.git
-[submodule "deps/jvm-verifier"]
-	path = deps/jvm-verifier
-	url = https://github.com/GaloisInc/jvm-verifier.git
 [submodule "deps/llvm-pretty"]
 	path = deps/llvm-pretty
 	url = https://github.com/elliottt/llvm-pretty.git

diff --git a/README.md b/README.md
@@ -87,7 +87,6 @@ downloaded dependencies include:
 * `deps/abcBridge/`:        [Haskell bindings for ABC](https://github.com/GaloisInc/abcBridge)
 * `deps/crucible/`:         [Crucible symbolic execution engine](https://github.com/GaloisInc/crucible)
 * `deps/cryptol/`:          [Cryptol](https://github.com/GaloisInc/cryptol)
-* `deps/jvm-verifier/`:     [Java Symbolic Simulator (JSS)](https://github.com/GaloisInc/jvm-verifier)
 * `deps/saw-core/`:         [SAWCore intermediate language](https://github.com/GaloisInc/saw-core), used by CSS, JSS, and SAWScript
 
 ## For SAW developers

diff --git a/build.sh b/build.sh
@@ -6,11 +6,10 @@ function install() {
   cp $(find dist-newstyle -type f -name $1 | sort -g | tail -1) bin/
 }
 
-cabal build exe:cryptol exe:jss exe:saw exe:saw-remote-api
+cabal build exe:cryptol exe:saw exe:saw-remote-api
 
 rm -rf bin && mkdir bin
 install cryptol
-install jss
 install saw
 install saw-remote-api
 

diff --git a/cabal.GHC-8.10.2.config b/cabal.GHC-8.10.2.config
@@ -183,7 +183,6 @@ constraints: any.Cabal ==3.2.0.0,
              any.js-chart ==2.9.4.1,
              any.json ==0.10,
              json +generic -mapdict +parsec +pretty +split-base,
-             jvm-verifier +build-benchmarks -build-examples +build-jss -build-jvmgraph +build-library +builtin-abc,
              any.kan-extensions ==5.2.1,
              any.language-c ==0.8.3,
              language-c -allwarnings +iecfpextension +separatesyb +usebytestrings,

diff --git a/cabal.GHC-8.6.5.config b/cabal.GHC-8.6.5.config
@@ -147,7 +147,6 @@ constraints: any.Cabal ==2.4.0.1,
              any.js-jquery ==3.3.1,
              any.json ==0.10,
              json +generic -mapdict +parsec +pretty +split-base,
-             jvm-verifier +build-benchmarks -build-examples +build-jss -build-jvmgraph +build-library,
              any.kan-extensions ==5.2,
              any.language-c ==0.8.3,
              language-c -allwarnings +iecfpextension +separatesyb +usebytestrings,

diff --git a/cabal.GHC-8.8.3.config b/cabal.GHC-8.8.3.config
@@ -149,7 +149,6 @@ constraints: any.Cabal ==3.0.1.0,
              any.js-jquery ==3.3.1,
              any.json ==0.10,
              json +generic -mapdict +parsec +pretty +split-base,
-             jvm-verifier +build-benchmarks -build-examples +build-jss -build-jvmgraph +build-library,
              any.kan-extensions ==5.2,
              any.language-c ==0.8.3,
              language-c -allwarnings +iecfpextension +separatesyb +usebytestrings,

diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config
@@ -143,7 +143,6 @@ constraints: any.Cabal ==3.0.1.0,
              any.js-jquery ==3.3.1,
              any.json ==0.10,
              json +generic -mapdict +parsec +pretty +split-base,
-             jvm-verifier +build-benchmarks -build-examples +build-jss -build-jvmgraph +build-library,
              any.kan-extensions ==5.2,
              any.language-c ==0.8.3,
              language-c -allwarnings +iecfpextension +separatesyb +usebytestrings,

diff --git a/cabal.project b/cabal.project
@@ -14,7 +14,6 @@ packages:
     deps/saw-core/saw-core-sbv
     deps/saw-core/saw-core-what4
     deps/saw-core/saw-core-coq
-    deps/jvm-verifier
     deps/what4/what4
     deps/crucible/crucible
     deps/crucible/crucible-jvm

diff --git a/coverage.sh b/coverage.sh
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-cabal build --enable-coverage exe:jss exe:saw
+cabal build --enable-coverage exe:saw
 
 # This conflicts with GitRev.mix in `saw-script`. Yuck.
 rm -f ./dist-newstyle/build/*/ghc-*/cryptol-*/**/GitRev.mix

diff --git a/deps/jvm-verifier b/deps/jvm-verifier
diff --git a/intTests/README b/intTests/README
@@ -42,7 +42,7 @@ works.
 
 Tests generally consist of a SAW script that is expected to succeed
 together with the artifacts that are needed. The "runtests.sh" script
-defines environment variables "JAVA", "SAW", and "JSS", pointing to the
+defines environment variables "JAVA" and "SAW", pointing to the
 corresponding executables, and with appropriate Java classpaths
 included. It's a good idea to include a README in each test directory.
 

diff --git a/intTests/jars/README b/intTests/jars/README
@@ -5,3 +5,11 @@ DIMACS format SAT solver from http://www.sat4j.org. Released under
 open source license LICENSE.sat4j, copied from
 http://www.eclipse.org/legal/epl-v10.html. See usage in ../sat.sh for
 usage info.
+
+
+bcprov-jdk16-145.jar
+--------------------
+
+Crypto library from https://www.bouncycastle.org. Released under open
+source license LICENSE.bcprov, copied from
+https://www.bouncycastle.org/licence.html.
diff --git a/intTests/jars/bcprov-jdk16-145.jar b/intTests/jars/bcprov-jdk16-145.jar
diff --git a/intTests/jars/galois.jar b/intTests/jars/galois.jar
diff --git a/intTests/runtests.sh b/intTests/runtests.sh
@@ -26,8 +26,6 @@ if [ -z "$TESTBASE" ]; then
   export TESTBASE
 fi
 
-JSS_BASE=$TESTBASE/../deps/jvm-verifier
-
 if [ "${OS}" == "Windows_NT" ]; then
   export CPSEP=";"
   export DIRSEP="\\"
@@ -41,10 +39,10 @@ fi
 #
 # Locate rt.jar. This is already a Windows path on windows, so no need
 # to 'cygpath' it.
-JDK=$("$JSS_BASE"/find-java-rt-jar.sh)
+JDK=$(support/find-java-rt-jar.sh)
 CP="$JDK"
 # Add our bundled .jars to the class path.
-for i in "$TESTBASE"/jars/*.jar "$JSS_BASE"/jars/*.jar; do
+for i in "$TESTBASE"/jars/*.jar; do
   if [ "$OS" == "Windows_NT" ]; then
     i=$(cygpath -w "$i")
   fi
@@ -55,7 +53,6 @@ export CP
 # We need the 'eval's here to interpret the single quotes protecting
 # the spaces and semi-colons in the Windows class path.
 export SAW="eval cabal run ${CABAL_FLAGS} saw -- -j '$CP'"
-export JSS="eval cabal run ${CABAL_FLAGS} jss -- -j '$CP' -c ."
 
 # Figure out what tests to run
 if [[ -z "$*" ]]; then

diff --git a/intTests/support/Makefile b/intTests/support/Makefile
@@ -1,4 +1,4 @@
-CP=.:../../deps/jvm-verifier/support/galois.jar
+CP=.:../jars/galois.jar
 
 %.ll: %.c
 	clang -S -emit-llvm $< -o $(shell basename $< .c).ll

diff --git a/intTests/support/find-java-rt-jar.sh b/intTests/support/find-java-rt-jar.sh
@@ -0,0 +1,17 @@
+#! /bin/bash
+
+# Find the Java core classes JAR, 'rt.jar' (called 'classes.jar' on OS
+# X for JDKs prior to 1.7).
+
+if [ -z "$RT_JAR" ]; then
+  JDK=$(java -verbose 2>&1 | sed -n -e '1 s/\[Opened \(.*\)\]/\1/p')
+else
+  JDK="$RT_JAR"
+fi
+if [ -z "$JDK" ]; then
+    echo "Failed to locate Java core classes (rt.jar / classes.jar)!" >&2
+    echo "The trick used by this script is only known to work with" >&2
+    echo "Sun-based JDKs." >&2
+    exit 1
+fi
+echo -n $JDK
diff --git a/intTests/test0001/Makefile b/intTests/test0001/Makefile
@@ -1,2 +1,2 @@
 JavaMD5.class: JavaMD5.java
-	javac -g -cp ../../deps/jvm-verifier/jars/bcprov-jdk16-145.jar:../../deps/jvm-verifier/jars/galois.jar JavaMD5.java
+	javac -g -cp ../jars/bcprov-jdk16-145.jar:../jars/galois.jar JavaMD5.java
diff --git a/intTests/test0008_jss_cnf/Makefile b/intTests/test0008_jss_cnf/Makefile
diff --git a/intTests/test0008_jss_cnf/README b/intTests/test0008_jss_cnf/README
diff --git a/intTests/test0008_jss_cnf/Test.class b/intTests/test0008_jss_cnf/Test.class
diff --git a/intTests/test0008_jss_cnf/Test.java b/intTests/test0008_jss_cnf/Test.java
diff --git a/intTests/test0008_jss_cnf/test.sh b/intTests/test0008_jss_cnf/test.sh
diff --git a/intTests/test0010_jss_cnf_exp/Makefile b/intTests/test0010_jss_cnf_exp/Makefile
diff --git a/intTests/test0010_jss_cnf_exp/README b/intTests/test0010_jss_cnf_exp/README
diff --git a/intTests/test0010_jss_cnf_exp/Test.class b/intTests/test0010_jss_cnf_exp/Test.class
diff --git a/intTests/test0010_jss_cnf_exp/Test.java b/intTests/test0010_jss_cnf_exp/Test.java
diff --git a/intTests/test0010_jss_cnf_exp/test.sh b/intTests/test0010_jss_cnf_exp/test.sh
diff --git a/intTests/test0012_jss_aig/Makefile b/intTests/test0012_jss_aig/Makefile
diff --git a/intTests/test0012_jss_aig/README b/intTests/test0012_jss_aig/README
diff --git a/intTests/test0012_jss_aig/Test.class b/intTests/test0012_jss_aig/Test.class
diff --git a/intTests/test0012_jss_aig/Test.java b/intTests/test0012_jss_aig/Test.java