Add package.json and fix README.md

.gitignore

@@ -7,3 +7,4 @@ solver_commands.smt2
 data.dzn
 model.fzn
 model.mzn
+node_modules

README.md

@@ -1,28 +1,32 @@
-# Concolic analysis for Jalangi 2
+# Aratha
 
-This is a prototype concolic analysis tool for Jalangi 2. To run it, you require
-a working copy of either the [CVC4](http://cvc4.cs.stanford.edu/) or the
-[Z3](https://github.com/Z3Prover/z3) SMT solver and Node.js v7 or up, as well as
-a working setup of Jalangi 2.
+Aratha is a prototype dynamic symbolic execution tool for JavaScript built on
+[Jalangi 2](https://github.com/Samsung/jalangi2). To run it, you require
+a working copy of the [G-Strings](https://bitbucket.org/robama/g-strings.git) CP
+solver, or one of the SMT solvers [CVC4](http://cvc4.cs.stanford.edu/) or
+[Z3](https://github.com/Z3Prover/z3), as well as Node v7 or higher.
 
-## How to run the analysis
-
-The default solver is CVC4, and the environment variable `CVC4_PATH` must be set
-to the path to CVC4, if it is not in your `PATH`.
-
-Alternatively, you can set `SMT_SOLVER=z3`to use Z3 instead. In this case,
-`Z3_PATH` must point to Z3 (or `z3` must be in your `PATH`).
-
-To analyze a script, run
+## Running the analysis
 
+First, install the dependencies by running
 ```
-node ../src/js/commands/jalangi.js --analysis ./ <path to script>
+$ npm install
+```
+from this directory. To analyze a script, run
+```
+$ npm run analyze -- <path to script>
 ```
-
 from this directory.
 
-## Running tests
+### Options
+
+The default solver is CVC4, and the environment variable `CVC4_PATH` must be set
+to the path to CVC4 if `cvc4` is not in your `PATH`.
+
+Alternatively, you can set `SOLVER=z3`to use Z3 instead. In this case,
+`Z3_PATH` must point to Z3 (or `z3` must be in your `PATH`).
+
+## Tests
 
 The tests are written with [Mocha](https://mochajs.org/). To run them, run
-`mocha` from this directory, or `../node_modules/.bin/mocha` if you've installed
-Jalangi 2's dependencies.
+`npm test` from this directory.

lib/analysis.js

@@ -21,7 +21,7 @@
         'abort': false,
         'verifyModel': false
     }
-    
+
     const path = require("path");
     const process = require("process");
     const fs = require("fs");
@@ -126,8 +126,8 @@
                 break;
             default:
                 throw new Error(`invalid solver ${SOLVER}`);
-        }        
-        
+        }
+
         if (solver.isCPSolver()) {
             if (process.env.INCREMENTAL === "0")
                 console.error("Warning: incremental option disabled for CP solvers.");
@@ -172,7 +172,7 @@
 
             const dseOptions = {
                 unsatCores: process.env.UNSAT_CORES === "1",
-                incremental: !(process.env.SOLVER === "G-Strings") && 
+                incremental: !(process.env.SOLVER === "G-Strings") &&
                              !(process.env.INCREMENTAL === "0"),
             };
 
@@ -200,7 +200,7 @@
                 const value = this.conditional(null, cond);
                 return value ? value.result : cond;
             };
-            
+
             sandbox.assert = (cond) => {
                 if(!sandbox.check(cond)) {
                     throw new ProcessExitException("J$.assert(): failed");
@@ -234,19 +234,21 @@
                 let first = true;
                 try {
                     fs.writeSync(inputLog, "[\n");
-                    const searcher = new DSE(solver, (newInput) => {                    
+                    const searcher = new DSE(solver, (newInput) => {
                         if (!first) {
                             fs.writeSync(inputLog, ",\n");
                         }
                         first = false;
-                        var isCircular = require('is-circular');
-                        if (isCircular(newInput)) {
-                            console.log("Warning! Circular object detected. Ignored input")
-                        } 
-                        else {
-                            fs.writeSync(inputLog, JSON.stringify(newInput));
+                        let serializedInput = null;
+                        try {
+                            serializedInput = JSON.stringify(newInput);
+                        } catch(e) {
+                            console.warn("Circular object detected; omitting from output log");
+                        }
+                        if (serializedInput !== null) {
+                            fs.writeSync(inputLog, serializedInput);
                             fs.fsyncSync(inputLog);
-                        }                    
+                        }
                         this.inputs = newInput;
                         this.path = new ExecutionPath();
                         resetNameCounter();