Initial Commit (Release)

.gitignore

@@ -0,0 +1,28 @@
+bin/
+node_modules/
+temp_build/
+obj/
+obj-test/
+*_jalangi_*.js*
+*.d
+*.o
+*.dylib
+*.a
+*configure
+*config.log
+*config.status
+*autom4te.cache
+*Makefile
+*lib.srcs
+*shell.srcs
+*npm-debug.log
+DS_Store
+*paper.synctex.gz
+*.aux
+*.log
+*.pdf
+z3.emscripten.js.mem
+libz3*
+.babelrc
+Dashboard/tmp/*
+tmp/

Analyser/README.md

@@ -0,0 +1,12 @@
+#Analyser
+
+The core of the symbolic analyser, executes a test script symbolically and reports any errors
+
+#Program Output
+The final output of the program will be the number of script errors that have occured (through fail()) or the error code magic number
+If the result of the run is 0xDEADBAD this indicates an internal error has occured.
+
+#Expected Paths
+The analyser can take an optional integer as the expected path count, if PC != this integer then the program will exit with an additional error (errorCount + 1) to indicate this.
+
+To run it with an expected PC execute ./expoSE FILENAME --expected pathcount

Analyser/package.json

@@ -0,0 +1,24 @@
+{
+  "name": "ExpoSE",
+  "version": "0.0.2",
+  "description": "Symbolic Execution for JavaScript",
+  "author": "Blake Loring <blake_l@parsed.uk>, Johannes Kinder <johannes.kinder@rhul.ac.uk>",
+  "readme": "README.md",
+  "dependencies": {
+    "browserify": "^14.1.0",
+    "jalangi": "git+https://github.com/Samsung/jalangi2.git",
+    "z3javascript": "git+https://github.com/ExpoSEJS/z3javascript.git"
+  },
+  "scripts": {
+    "postinstall": "./postinstall"
+  },
+  "license": "Apache",
+  "main": "src/SymbolicExecution.js",
+  "devDependencies": {
+    "babel-cli": "^6.18.0",
+    "babel-plugin-strip-function-call": "^1.0.2",
+    "babel-preset-babili": "0.0.9",
+    "babel-preset-es2015": "^6.3.13",
+    "babel-preset-stage-0": "^6.3.13"
+  }
+}

Analyser/postinstall

@@ -0,0 +1,2 @@
+#!/bin/bash -e
+exit 0

Analyser/src/Analyser.js

@@ -0,0 +1,80 @@
+/* Copyright (c) Royal Holloway, University of London | Contact Blake Loring (blake_l@parsed.uk), Duncan Mitchell (Duncan.Mitchell.2015@rhul.ac.uk), or Johannes Kinder (johannes.kinder@rhul.ac.uk) for details or support | LICENSE.md for license details */
+
+"use strict";
+
+// do not remove the following comment
+// JALANGI DO NOT INSTRUMENT
+//
+// Symbolic execution analyser entry point
+
+import SymbolicExecution from './SymbolicExecution';
+import ObjectHelper from './Utilities/ObjectHelper';
+import {ConcolicValue, WrappedValue} from './Values/WrappedValue';
+import NotAnErrorException from './NotAnErrorException';
+import Log from './Utilities/Log';
+import Z3 from 'z3javascript';
+import fs from 'fs';
+
+/**
+ * Set up the methods and classes which ObjectHelper considers safe to string
+ */
+
+ObjectHelper.safe(Z3.Expr.prototype);
+ObjectHelper.safe(Z3.Model.prototype);
+ObjectHelper.safe(Z3.Context.prototype);
+ObjectHelper.safe(WrappedValue.prototype);
+ObjectHelper.safe(ConcolicValue.prototype)
+ObjectHelper.safe(NotAnErrorException.prototype);
+
+/**
+ * End the SafeToString table
+ */
+
+const OUT_PATH = 'EXPOSE_OUT_PATH';
+const COVERAGE_PATH = 'EXPOSE_COVERAGE_PATH';
+
+function Default(i, d) {
+	return process.env[i] || d;
+}
+
+let outFilePath = Default(OUT_PATH, undefined);
+let outCoveragePath = Default(COVERAGE_PATH, undefined);
+
+let input = process.argv[process.argv.length - 1];
+
+Log.logHigh('Built with VERY logging enabled');
+Log.logMid('Built with FINE logging enabled');
+Log.log('Built with BASE logging enabled');
+Log.log('Intial Input' + input);
+
+process.title = 'ExpoSE Play ' + input;
+
+process.on('disconnect', function() {
+  Log.log('Premature termination - Parent exit')
+  process.exit();
+});
+
+J$.analysis = new SymbolicExecution(J$, JSON.parse(input), (state, coverage) => {
+    Log.log("Finished play with PC " + state.pathCondition.map(x => x.ast));
+
+    let finalOut = {
+        pc: state.finalPC(),
+        input: state.finalInput(),
+        errors: state.errors,
+        alternatives: state.alternatives()
+    };
+
+    if (outCoveragePath) {
+		fs.writeFileSync(outCoveragePath, JSON.stringify(coverage.end()));
+		Log.log('Wrote final coverage to ' + outCoveragePath);
+    } else {
+    	Log.log('No final coverage path supplied');
+	}
+
+	if (outFilePath) {
+		fs.writeFileSync(outFilePath, JSON.stringify(finalOut));
+        Log.log('Wrote final output to ' + outFilePath);
+	} else {
+    	Log.log('No final output path supplied');
+	}
+});

Analyser/src/Coverage.js

@@ -0,0 +1,58 @@
+/* Copyright (c) Royal Holloway, University of London | Contact Blake Loring (blake_l@parsed.uk), Duncan Mitchell (Duncan.Mitchell.2015@rhul.ac.uk), or Johannes Kinder (johannes.kinder@rhul.ac.uk) for details or support | LICENSE.md for license details */
+
+"use strict";
+
+class Coverage {
+
+    constructor(sandbox) {
+        this._sandbox = sandbox;
+        this._branches = [];
+        this._branchFilenameMap = [];
+    }
+
+    end() {
+        let ret = {};
+        for (let i = 0; i < this._branches.length; i++) {
+            if (this._branches[i] !== undefined) {
+
+                //Deep copy the smap
+            	let map = JSON.parse(JSON.stringify(this._sandbox.smap[i+1]));
+
+                //Strip away any non SID related entities
+                //Also replace all source index arrays to a single value to reduce stdout
+            	for (let j in map) {
+            		if (isNaN(parseInt(j))) {
+            			delete map[j];
+            		} else {
+                        map[j] = 1;
+                    }
+            	}
+
+                ret[this._branchFilenameMap[i]] = {
+                	smap: map,
+                    branches: this._branches[i]
+                };
+            }
+        }
+
+        return ret;
+    }
+
+    getBranchInfo() {
+        let branchInfo = this._branches[this._sandbox.sid - 1];
+
+        if (!branchInfo) {
+            branchInfo = {};
+            this._branches[this._sandbox.sid - 1] = branchInfo;
+            this._branchFilenameMap[this._sandbox.sid - 1] = this._sandbox.smap[this._sandbox.sid].originalCodeFileName;
+        }
+
+        return branchInfo;
+    }
+
+    touch(iid) {
+    	this.getBranchInfo()[iid] = 1;
+    }
+}
+
+export default Coverage;

Analyser/src/External.js

@@ -0,0 +1,22 @@
+/* Copyright (c) Royal Holloway, University of London | Contact Blake Loring (blake_l@parsed.uk), Duncan Mitchell (Duncan.Mitchell.2015@rhul.ac.uk), or Johannes Kinder (johannes.kinder@rhul.ac.uk) for details or support | LICENSE.md for license details */
+
+"use strict";
+
+/**
+ * This is a function that detects whether we are using Electron and 
+ * if so does a remote call through IPC rather than a direct require.
+ */
+
+ const ELECTRON_PATH_MAGIC = '/electron/';
+
+export default function (library) {
+	let lrequire = require;
+
+	if (process && process.execPath && process.execPath.indexOf(ELECTRON_PATH_MAGIC) != -1) {
+		lrequire = require('electron').remote.require;
+	}
+
+	const result = lrequire(library);
+
+	return result.default ? result.default : result;
+}