Use java to detect standard JAR/JIMAGE paths

[RyanGlScott]

Currently, using SAW to verify Java code requires manually specifying the path to where your JDK installation's rt.jar file lives with the -j flag. This is rather cumbersome, and this will likely be even more cumbersome after #861 is fixed, since that will require knowing about even more standard paths:

1. The path to your JDK installation's modules file (a JIMAGE file), and
2. The path to your JDK installation's bin directory, which contains utilities such as jimage.

However, having to specify all of these paths is a bit redundant. If we specify the path to your JDK installation's bin directory, that gives SAW access to java, and java is well equipped to tell you where the other paths are. For example, here is java 11 can tell you:

$ java -XshowSettings:properties -version
Property settings:
    awt.toolkit = sun.awt.X11.XToolkit
    file.encoding = UTF-8
    file.separator = /
    java.awt.graphicsenv = sun.awt.X11GraphicsEnvironment
    java.awt.printerjob = sun.print.PSPrinterJob
    java.class.path = 
    java.class.version = 55.0
    java.home = /usr/lib/jvm/java-11-openjdk-amd64
    java.io.tmpdir = /tmp
    java.library.path = /usr/java/packages/lib
        /usr/lib/x86_64-linux-gnu/jni
        /lib/x86_64-linux-gnu
        /usr/lib/x86_64-linux-gnu
        /usr/lib/jni
        /lib
        /usr/lib
    java.runtime.name = OpenJDK Runtime Environment
    java.runtime.version = 11.0.9.1+1-Ubuntu-0ubuntu1.20.04
    java.specification.name = Java Platform API Specification
    java.specification.vendor = Oracle Corporation
    java.specification.version = 11
    java.vendor = Ubuntu
    java.vendor.url = https://ubuntu.com/
    java.vendor.url.bug = https://bugs.launchpad.net/ubuntu/+source/openjdk-lts
    java.version = 11.0.9.1
    java.version.date = 2020-11-04
    java.vm.compressedOopsMode = Zero based
    java.vm.info = mixed mode, sharing
    java.vm.name = OpenJDK 64-Bit Server VM
    java.vm.specification.name = Java Virtual Machine Specification
    java.vm.specification.vendor = Oracle Corporation
    java.vm.specification.version = 11
    java.vm.vendor = Ubuntu
    java.vm.version = 11.0.9.1+1-Ubuntu-0ubuntu1.20.04
    jdk.debug = release
    line.separator = \n 
    os.arch = amd64
    os.name = Linux
    os.version = 5.4.0-62-generic
    path.separator = :
    sun.arch.data.model = 64
    sun.boot.library.path = /usr/lib/jvm/java-11-openjdk-amd64/lib
    sun.cpu.endian = little
    sun.cpu.isalist = 
    sun.io.unicode.encoding = UnicodeLittle
    sun.java.launcher = SUN_STANDARD
    sun.jnu.encoding = UTF-8
    sun.management.compiler = HotSpot 64-Bit Tiered Compilers
    sun.os.patch.level = unknown
    user.country = US
    user.dir = /home/rscott
    user.home = /home/rscott
    user.language = en
    user.name = rscott
    user.timezone = 

openjdk version "11.0.9.1" 2020-11-04
OpenJDK Runtime Environment (build 11.0.9.1+1-Ubuntu-0ubuntu1.20.04)
OpenJDK 64-Bit Server VM (build 11.0.9.1+1-Ubuntu-0ubuntu1.20.04, mixed mode, sharing)

In particular, this line:

    java.home = /usr/lib/jvm/java-11-openjdk-amd64

Is the key piece of information needed to find everything else. Utilities like jimage, for instance, will be located at <java.home>/bin/jimage. If using Java 9 or later, the standard modules file is located at <java.home>/lib/modules, so SAW can automatically add this to the module path. If using Java 8 or earlier, the standard rt.jar file is located at <java.home>/jre/lib/rt.jar, so SAW can automatically add this to the class path.

In fact, we can go one step further. The path to your JDK installation's bin directory is, in many cases, also on your PATH. We could take advantage of this in SAW by first consulting the PATH to see if java is found there. This would allow using SAW to verify Java code without having to manually specify any special paths, which would be a huge usability win.

[brianhuffman]

This would be very nice. It means I could get rid of my sawj script, which simply runs saw with the command line option for rt.jar prepended to any other arguments.

It might also be useful to have a way to make saw print out what directories and .jar files it's actually using, maybe based on the verbosity level. This might help with debugging problems that might arise if, for example, some proof script breaks after you've upgraded your system java installation.