QoL improvements for regnant

.gitignore

@@ -15,3 +15,4 @@ auto/
 *~
 **/.merlin
 _build/
+.vscode/

.travis.yml

@@ -1,4 +1,7 @@
 language: c
+os:
+  - "linux"
+dist: "xenial"
 addons:
   apt:
     sources:
@@ -9,8 +12,9 @@ addons:
       - libstdc++6
       - libgomp1
       - libgmp-dev
-      - python
-sudo: false
+      - python3-pip
+      - python3-dev
+      - python3-setuptools
 cache:
   directories:
     - $HOME/.opam

src/regnant/.travis-ci.sh

@@ -11,4 +11,7 @@ if [[ ! -d $HOME/jdk8/jdk8u232-b09 ]]; then
         tar xf /tmp/jdk.tar.gz -C $HOME/jdk8;
 fi
 
-python $THIS_DIR/integration-test.py $HOME/jdk8/jdk8u232-b09
+pip3 install -U setuptools
+pip3 install wheel
+pip3 install PyYaml
+python3 $THIS_DIR/integration-test.py $HOME/jdk8/jdk8u232-b09

src/regnant/README.md

@@ -10,8 +10,7 @@ program.
 A compiler that supports Java 11, and a Java runtime that supports Java 11.
 The gradle build tool can be bootstrapped with the gradlew script (see below).
 
-To use the scripts distributed here, you will also need `python` versions 2 and 3 (porting
-the scripts to python 3 is a work in progress).
+To use the scripts distributed here, you will also need `python` version 3.
 
 To actually run the Regnant translation you will need a JDK 8 installation, which includes
 at least `rt.jar` (to give the definitions for the JCL classes).
@@ -37,7 +36,7 @@ whole program transformation and hooks into Soot's main method. To directly invo
 you will need to provide the (quite numerous) magical flags required to make Soot run.
 
 Instead, it is recommended you use the `regnant.py` script. If you want to know
-how to invoke regnant directly, you can pass the `--verbose` option which 
+how to invoke regnant directly, you can pass the `--verbose` option which
 causes the `regnant` script to print the flags it is using.
 
 The basic invocation is:
@@ -48,6 +47,56 @@ Any future argumens after the entry point are passed directly to the
 underlying consort tool (you will likely need to provide the `--`
 argument to avoid confusion from python).
 
+## Install Instructions for Mac
+
+> tested on ConSORT commit fe88545 on 2020-02-18
+
+First, the assumption is that you are in the SoftwareFoundationGroupAtKyotoU/consort repository.
+
+1. Install Java(s)
+1. Run the build scripts
+1. Run the command
+
+### Install the required Java JDKs
+
+First, we will install Java > 11
+
+```sh
+$ brew tap homebrew/cask-versions
+$ brew cask install java11
+```
+
+Next, install Java 8. [Oracle has stopped releasing Java 8](https://qiita.com/d_forest/items/290bb05bb929e5d74647).
+Therefore, we need to install OpenJDK or something similar.
+
+```sh
+$ brew cask install adoptopenjdk8
+```
+
+We can locate the jdk by using the following command
+
+```sh
+$ /usr/libexec/java_home
+# /Library/Java/JavaVirtualMachines/**jdk_version**/Contents/Home
+```
+
+### Running build scripts
+
+You can run the build scripts like it says at the top of this README.
+
+```sh
+$ pwd
+# ...SoftwareFoundationGroupAtKyotoU/consort/src/regnant
+$ ./gradlew installDist
+$ ./gradlew integrationJar
+```
+
+### Run the Command
+
+Now you can run `./regnant.py --src-dir ./src/integration/java /Library/Java/JavaVirtualMachines/adoptopenjdk-8.jdk/Contents/Home **ClassName**` to verify Java programs!
+
+---
+
 ## Code Walkthrough
 
 As mentioned above, Regnant is built upon Soot; you will need at least
@@ -89,16 +138,19 @@ The unit graph is first pre-processed by a series of rewriters, as defined in `R
 These rewriters perform the following functions:
 
 1. Translating the if statements generated by an `assert e` statement into `if(!e) fail` (`AssertionRewriter`).
-  * Technically we insert a new NOP statement which is given a tag interpreted by the translation pass such that it compiles to `fail`
+
+- Technically we insert a new NOP statement which is given a tag interpreted by the translation pass such that it compiles to `fail`
+
 2. Rewriting `random.nextInt()` into a call to `edu.kyoto.regnant.random.rand()` (this is later recognized and rewritten into a `_` form) (`RandomRewriter`)
 3. Automatically inserting aliasing annnotations (`AliasInsertion`):
-  * Aliasing annotations are handled with calls to (dummy) functions in the Regnant "runtime"
-  * This pass searches for variables that:
-     * are used and defined exactly once in the same block
-     * are defined with `x = y.f`
-     * after their last use, we have `mustAlias(x, y.f)`
-     * are not passed to to `Aliasing.noAutoReturn`
-  * For such variables, Regnant automatically inserts calls to the must aliasing calls
+
+- Aliasing annotations are handled with calls to (dummy) functions in the Regnant "runtime"
+- This pass searches for variables that:
+  - are used and defined exactly once in the same block
+  - are defined with `x = y.f`
+  - after their last use, we have `mustAlias(x, y.f)`
+  - are not passed to to `Aliasing.noAutoReturn`
+- For such variables, Regnant automatically inserts calls to the must aliasing calls
 
 The unit graph of the method is first translated into a BlockGraph, which gives the basic blocks
 of the method. The basic block construction is handled entirely by the `BasicBlockGraph` class.
@@ -116,8 +168,8 @@ following Java code:
 ```java
 lbl: {
    A;
-   if(e1) { 
-     B; 
+   if(e1) {
+     B;
      if(e2) { break lbl; }
    } else {
      C
@@ -131,8 +183,8 @@ under the condition `!e1 || !e2`. The above could be rewritten to:
 
 ```java
 A;
-if(e1) { 
-  B; 
+if(e1) {
+  B;
   if(!e2) { D }
 } else {
   C; D
@@ -152,8 +204,8 @@ example, we rewrite the program to:
 ```java
 A;
 flag = 0
-if(e1) { 
-  B; 
+if(e1) {
+  B;
   if(!e2) { flag = 1 }
 } else {
   C
@@ -191,8 +243,8 @@ is handled by `Translate`.
 
 ### Object Model
 
-As stated above, Regnant uses a large, monolithic tuple to represent objects. 
-More precisely, an object is represented with a tuple consisting n elements, 
+As stated above, Regnant uses a large, monolithic tuple to represent objects.
+More precisely, an object is represented with a tuple consisting n elements,
 the first element is an (immutable) integer representing the runtime tag of the object,
 and the remaining n - 1 fields representing the field values of the object or dummy values
 as required by the monolithic representation.
@@ -211,6 +263,6 @@ to a field into low-level IMPerial access paths, etc. The assumption about 1 is
 but in principle the flexibility of the `ObjectModel` interface implies other representation
 strategies are feasible.
 
-As a final note, the functional approach appear to scale better as it requires *significantly*
+As a final note, the functional approach appear to scale better as it requires _significantly_
 fewer ownership variables. Even in the relaxed ownership mode, the maximization constraint
 emited by ConSORT can grind Z3 to a halt if the number of ownership variables is too large.

src/regnant/integration-test.py

@@ -1,33 +1,36 @@
-#!/bin/python
+#!python
 
 import os
 import subprocess
 import sys
 import tempfile
 import yaml
+from yaml import FullLoader
 
 this_dir = os.path.realpath(os.path.dirname(sys.argv[0]))
 
-subprocess.check_call([os.path.join(this_dir, "gradlew"), "--console", "plain", "installDist", "integrationJar"], cwd = this_dir)
+subprocess.check_call([os.path.join(this_dir, "gradlew"), "--console",
+                       "plain", "installDist", "integrationJar"], cwd=this_dir)
 
 integration = os.path.join(this_dir, "build/libs/integration.jar")
 reg_script = os.path.join(this_dir, "regnant.py")
 
-with tempfile.NamedTemporaryFile(delete = True) as t:
+with tempfile.NamedTemporaryFile(delete=True) as t:
     subprocess.check_call([os.path.join(this_dir, "build/install/regnant/bin/generateWork"),
                            os.path.join(this_dir, "build/libs/integration.jar"), t.name])
-    worklist = yaml.load(t)
-
-for (k,v) in worklist.iteritems():
-    with open("/dev/null", "w") as out:
-        print "Testing",k
-        ret = subprocess.call([
-           reg_script, "--jar=" + integration,
-           "--skip-build",
-            sys.argv[1], k
-        ], stdout = out, stderr = subprocess.STDOUT)
-        if (ret != 0) != v:
-            print "Unexpected result for",k
-            sys.exit(1)
-
-print "DONE"
+    worklist = yaml.load(t, Loader=FullLoader)
+
+
+for (k, v) in worklist.items():
+    print("Testing", k)
+    ret = subprocess.call([
+        reg_script,
+        "--jar=" + integration,
+        "--skip-build",
+        sys.argv[1], k
+    ], stdout=subprocess.DEVNULL)
+    if (ret != 0) != v:
+        print("Unexpected result for", k)
+        sys.exit(1)
+
+print("DONE")

src/regnant/regnant.py

@@ -3,36 +3,43 @@
 import sys
 import subprocess
 import tempfile
-import atexit, shutil, os
+import atexit
+import shutil
+import os
 import argparse
 import time
 
+
 def log_command(args, cmd):
     if args.verbose:
         import pipes
-        print("executing:"," ".join([ pipes.quote(s) for s in cmd ]))
+        print("executing:", " ".join([pipes.quote(s) for s in cmd]))
+
 
 def run_silently(cmd, **kwargs):
     with open("/dev/null", "w") as out:
         s = time.time()
-        subprocess.check_call(cmd, stdout = out, stderr = subprocess.STDOUT, **kwargs)
+        subprocess.check_call(
+            cmd, stdout=out, stderr=subprocess.STDOUT, **kwargs)
         e = time.time()
         return e - s
 
+
 def print_done(args, e):
     if args.timing:
         print("done (in %.02f)" % e)
     else:
         print("done")
 
+
 def main(this_dir, args):
     parser = argparse.ArgumentParser()
     parser.add_argument("--work-dir")
     parser.add_argument("--verbose", action="store_true")
     parser.add_argument("--jar")
-    parser.add_argument("--skip-build", action="store_true", default = False)
-    parser.add_argument("--debug-trans", action="store_true", default = False)
-    parser.add_argument("--functional", action="store_true", default = False)
+    parser.add_argument("--skip-build", action="store_true", default=False)
+    parser.add_argument("--debug-trans", action="store_true", default=False)
+    parser.add_argument("--functional", action="store_true", default=False)
     parser.add_argument("--timing", action="store_true")
     parser.add_argument("--src-dir")
     parser.add_argument("--yaml")
@@ -49,7 +56,7 @@ def main(this_dir, args):
         args.verbose = True
 
     if not args.skip_build:
-        run_silently(["gradle", "installDist"], cwd = this_dir)
+        run_silently(["./gradlew", "installDist"], cwd=this_dir)
 
     if args.work_dir is None:
         work_dir = tempfile.mkdtemp()
@@ -65,7 +72,8 @@ def main(this_dir, args):
 
         source_file = cls.replace(".", "/") + ".java"
 
-        compile_command = ["javac", "-g:lines,vars", "-source", "8", "-target", "8", "-d", cls_dir, args.src_dir + "/" + source_file]
+        compile_command = ["javac", "-g:lines,vars", "-cp", args.src_dir, "-source",
+                           "8", "-target", "8", "-d", cls_dir, args.src_dir + "/" + source_file]
         log_command(args, compile_command)
         print("compiling source java...", end=' ')
         sys.stdout.flush()
@@ -88,14 +96,14 @@ def main(this_dir, args):
 
     regnant_command = [
         run_script,
-        "-f", "n", # no output
-        "-no-bodies-for-excluded", # don't load the JCL (for now)
-        "-w", # whole program mode
-        "-p", "cg.spark", "on", # run points to analysis
-#        "-p", "jb", "use-original-names:true", # try to make our names easier
-        "-soot-class-path", cls_dir + ":" + rt_path, # where to find the test file
+        "-f", "n",  # no output
+        "-no-bodies-for-excluded",  # don't load the JCL (for now)
+        "-w",  # whole program mode
+        "-p", "cg.spark", "on",  # run points to analysis
+        #        "-p", "jb", "use-original-names:true", # try to make our names easier
+        "-soot-class-path", cls_dir + ":" + rt_path,  # where to find the test file
         "-p", "wjtp.regnant", regnant_options,
-        cls # the class to run on
+        cls  # the class to run on
     ]
 
     log_command(args, regnant_command)
@@ -105,7 +113,7 @@ def main(this_dir, args):
     sys.stdout.flush()
     el = run_silently(regnant_command)
     print_done(args, el)
-    
+
     print("Generating control flags...", end=' ')
     sys.stdout.flush()
     intr_loc = os.path.join(work_dir, "java.intr")
@@ -120,8 +128,11 @@ def main(this_dir, args):
     log_command(args, intr_command)
     el = run_silently(intr_command)
     print_done(args, el)
-    
+
     print("Running ConSORT on translated program:")
+    if args.verbose:
+        with open(data, 'r') as file:
+            print(file.read())
     yaml_flg = ["-yaml"] if args.yaml is not None else []
     consort_cmd = [
         os.path.join(this_dir, "../_build/default/test.exe"),
@@ -132,7 +143,7 @@ def main(this_dir, args):
     ]
     log_command(args, consort_cmd)
     s = time.time()
-    ret = subprocess.run(consort_cmd, stdout = subprocess.PIPE)
+    ret = subprocess.run(consort_cmd, stdout=subprocess.PIPE)
     e = time.time()
     if args.yaml:
         with open(args.yaml, 'w') as out:
@@ -144,5 +155,7 @@ def main(this_dir, args):
         print("(ConSORT ran for %.02f seconds)" % (e - s))
     return ret.returncode
 
+
 if __name__ == "__main__":
-    sys.exit(main(os.path.realpath(os.path.dirname(sys.argv[0])), sys.argv[1:]))
+    sys.exit(main(os.path.realpath(
+        os.path.dirname(sys.argv[0])), sys.argv[1:]))