Features/fix match global

Analyser/src/Models/Helpers.js

@@ -79,15 +79,6 @@ export default function(state, ctx) {
 		return symbol;
 	}
 
-	//Hook for regex methods, will only hook if regex is enabled
-	function symbolicHookRe(f, condition, hook) {
-		return symbolicHook(f, condition, function() {
-			//Intercept the hook to do regex stats
-			state.stats.seen("Regex Function Model");
-			return hook.apply(this, arguments);
-		}, true, !Config.regexEnabled);
-	}
-
 	function NoOp(f) {
 		return function(base, args) {
 			Log.logMid(`NoOp ${f.name} with base ${ObjectHelper.asString(base)} and ${ObjectHelper.asString(args)}`);
@@ -153,10 +144,10 @@ export default function(state, ctx) {
 	}
 
 	return {
+		runMethod: runMethod,
 		symbolicHook: symbolicHook,
 		ConcretizeIfNative: ConcretizeIfNative,
 		coerceToString: coerceToString,
-		symbolicHookRe: symbolicHookRe,
 		NoOp: NoOp,
 		substring: substringHelper
 	};

Analyser/src/Models/RegexModels.js

@@ -7,9 +7,20 @@ let isMatchCount = 0;
 
 export default function(state, ctx, model, helpers) {
 
-	const symbolicHookRe = helpers.symbolicHookRe;
 	const coerceToString = helpers.coerceToString;
 
+	//Hook for regex methods, will only hook if regex is enabled
+	function symbolicHookRe(f, condition, hook) {
+		const runMethod = helpers.runMethod;
+		return function(base, args) {
+			if (condition(base, args)) {
+				return hook(base, args);
+			} else {
+				return runMethod(f, base, args);
+			}
+		}
+	}
+
 	function DoesntMatch(l, r) {
 		if (l == undefined) {
 			const is_match = (r == "") || (r == undefined);
@@ -50,6 +61,9 @@ export default function(state, ctx, model, helpers) {
 
 	function BuildRefinements(regex, real, string_s, is_match_s) {
 
+		//The refinements operate on the remainder of the string so we no longer care about the sticky / global rules
+		real = new RegExp(real.source, real.flags.replace(/y|g/g, ""));
+
 		if (!(Config.capturesEnabled && Config.refinementsEnabled)) {
 			Log.log("Refinements disabled - potential accuracy loss");
 			return [];
@@ -120,7 +134,7 @@ export default function(state, ctx, model, helpers) {
 			let real_match = real.exec(model.eval(string_s).asConstant(model));
 
 			if (!real_match) {
-				Log.log(`WARN: Broken regex detected ${regex.ast.toString()} vs ${real}`);
+				Log.log(`WARN: Broken regex detected ${regex.ast.toString()} vs ${real} in ${model.eval(string_s).asConstant(model)}`);
 				return [];
 			}
 
@@ -144,29 +158,52 @@ export default function(state, ctx, model, helpers) {
 	/** As an optimization we implement test differently, this allows us to not generated extra paths when not needed on usage **/
 	function RegexpBuiltinTest(regex, string) {
 
+		let currentLastIndex = regex.lastIndex;
+		regex.lastIndex = state.getConcrete(regex.lastIndex);
+
 		const is_match_c = regex.test(state.getConcrete(string));
 
 		if (regex.sticky || regex.global) {
-			stats.seen('Sticky (RegexBuiltinExec)');
 			//Cut at regex.lastIndex
-			string = models.get(String.prototype.substring)(string, [regex.lastIndex]);
+			state.stats.seen('Sticky (RegexBuiltinExec)');
+			string = model.get(String.prototype.substring).call(string, currentLastIndex);
+			if (!regex.source[0] != '^') {
+				Log.log("In Sticky Mode We Insert ^");
+				regex = new RegExp('^' + regex.source, regex.flags);
+			}
 		}
 
 		const regexEncoded = Z3.Regex(ctx, regex);
-
 		const is_match_s = ctx.mkSeqInRe(state.asSymbolic(string), regexEncoded.ast);
 
 		EnableCaptures(regexEncoded, regex, state.asSymbolic(string));
 		is_match_s.checks = BuildRefinements(regexEncoded, regex, state.asSymbolic(string), is_match_s);
 
+		if (Config.capturesEnabled && (regex.sticky || regex.global)) {
+			Log.log('Captures enabled - symbolic lastIndex enabled');
+			regex.lastIndex = new ConcolicValue(
+				regex.lastIndex,
+				ctx.mkIte(
+					is_match_s,
+					ctx.mkAdd(state.asSymbolic(currentLastIndex), regexEncoded.captures[0].getLength()),
+					ctx.mkIntVal(0)
+				)
+			);
+		}
+
 		return {
 			result: new ConcolicValue(is_match_c, is_match_s),
 			encodedRegex: regexEncoded,
 		}
 	}
 
 	function RegexpBuiltinExec(regex, string) {
+
+		//Preserve the lastIndex property
+		let lastIndex = regex.lastIndex;
 		const test = RegexpBuiltinTest(regex, string);
+		regex.lastIndex = lastIndex;
+
 		state.conditional(test.result); //Fork on the str.in.re operation
 
 		let result_c = regex.exec(state.getConcrete(string));
@@ -201,15 +238,17 @@ export default function(state, ctx, model, helpers) {
 		if (regex.global) {
 
 			//Remove g and y from regex
-			const rewrittenRe = new RegExp(regex.source, regex.flags.replace(/"g|y"/g, "") + "y");
+			const rewrittenRe = new RegExp(regex.source, regex.flags.replace(/g|y/g, "") + "y");
 
 			let results = [];
 
 			while (true) {
 				const next = RegexpBuiltinExec(rewrittenRe, string);
+
 				if (!next.result) {
 					break;
 				}
+
 				results.push(next.result[0]);
 			}
 
@@ -243,40 +282,44 @@ export default function(state, ctx, model, helpers) {
 
 	}
 
+	function shouldBeSymbolic(regex, string) {
+		return regex instanceof RegExp && (state.isSymbolic(regex.lastIndex) || state.isSymbolic(string)); 
+	}
+
 	model.add(String.prototype.search, symbolicHookRe(
 		String.prototype.search,
-		(base, args) => state.isSymbolic(base) && args[0] instanceof RegExp,
-		(base, args, _result) => RegexpBuiltinSearch(args[0], coerceToString(base)).result
+		(base, args) => shouldBeSymbolic(args[0], base),
+		(base, args) => RegexpBuiltinSearch(args[0], coerceToString(base)).result
 	));
 
 	model.add(String.prototype.match, symbolicHookRe(
 		String.prototype.match,
-		(base, args) => state.isSymbolic(base) && args[0] instanceof RegExp,
-		(base, args, _result) => RegexpBuiltinMatch(args[0], coerceToString(base)).result
+		(base, args) => shouldBeSymbolic(args[0], base),
+		(base, args) => RegexpBuiltinMatch(args[0], coerceToString(base)).result
 	));
 
 	model.add(RegExp.prototype.exec, symbolicHookRe(
 		RegExp.prototype.exec,
-		(base, args) => base instanceof RegExp && state.isSymbolic(args[0]),
-		(base, args, _result) => RegexpBuiltinExec(base, coerceToString(args[0])).result
+		(base, args) => shouldBeSymbolic(base, args[0]),
+		(base, args) => RegexpBuiltinExec(base, coerceToString(args[0])).result
 	));
 
 	model.add(RegExp.prototype.test, symbolicHookRe(
 		RegExp.prototype.test,
-		(base, args) => base instanceof RegExp && state.isSymbolic(args[0]),
-		(base, args, _result) => RegexpBuiltinTest(base, coerceToString(args[0])).result
+		(base, args) => shouldBeSymbolic(base, args[0]),
+		(base, args) => RegexpBuiltinTest(base, coerceToString(args[0])).result
 	));
 
 	//Replace model for replace regex by string. Does not model replace with callback.
 	model.add(String.prototype.replace, symbolicHookRe(
 		String.prototype.replace,
 		(base, args) => state.isSymbolic(base) && args[0] instanceof RegExp && typeof args[1] === "string",
-		(base, args, _result) => state.getConcrete(base).secret_replace.apply(base, args)
+		(base, args) => state.getConcrete(base).secret_replace.apply(base, args)
 	));
 
 	model.add(String.prototype.split, symbolicHookRe(
 		String.prototype.split,
 		(base, args) => state.isSymbolic(base) && args[0] instanceof RegExp,
-		(base, args, _result) => state.getConcrete(base).secret_split.apply(base, args)
+		(base, args) => state.getConcrete(base).secret_split.apply(base, args)
 	));
 }

Analyser/src/SymbolicExecution.js

@@ -35,7 +35,7 @@ class SymbolicExecution {
 
 		} else { 
 			const process = External.load("process");
-            
+
 			//Bind any uncaught exceptions to the uncaught exception handler
 			process.on("uncaughtException", this._uncaughtException.bind(this));
 

lib/S$/src/symbols.js

@@ -24,8 +24,9 @@ function secret_replace_once(str, regex, w) {
 
 String.prototype.secret_replace = function (regex, w) {
     console.log('TODO: Replace prototype is new and needs better modeling ' + regex + ' and w ' + w);
+		console.log('Regex ' + regex);
 
-    regex = new RegExp(regex.source, regex.flags.replace(/g/, ''));
+    regex = new RegExp(regex.source, regex.flags);
 
     let result = this;
     let next_start = 0;
@@ -48,7 +49,7 @@ String.prototype.secret_replace = function (regex, w) {
 String.prototype.secret_split = function (regex) {
     console.log('TODO: Split prototype is new and needs better modeling ' + regex);
 
-    regex = new RegExp(regex.source, regex.flags.replace(/g/, ''));
+    regex = new RegExp(regex.source, regex.flags);
 
     let result = [];
     let remaining = this;

tests/regex/match/global/test1.js

@@ -1,8 +1,20 @@
 var S$ = require('S$');
 var a = S$.symbol('A', '');
 
-S$.assume(a.length == 'iPhoneAndroid'.length);
+S$.assume(a.length <= 20);
 
-if (a == 'iPhoneAndroid') {
-   throw 'iPhone Android'; 
+var res = a.match(/Testi/g);
+
+//Test that other string constraints will still get generated after a match
+if (a == "HotDog") {
+	throw 'Reachable';
+} 
+
+//Test that we can find this enumeration-required case in a match operation
+if (res) {
+	for (var i = 0; i < res.length; i++) {
+		if (i == 3) {
+			throw 'Reachable';
+		}
+	}
 }

tests/regex/replace/single/replace_2.js

@@ -2,6 +2,7 @@
 
 //Tests a replace on a non global regex
 
+var S$ = require('S$');
 var x = S$.symbol("X", 'a');
 var b = /^(a|b)$/;
 

tests/regex/replace/single/replace_3.js

@@ -2,6 +2,7 @@
 
 //Tests a replace on a non global regex
 
+var S$ = require('S$');
 var x = S$.symbol("X", 'a');
 var b = /^...$/;
 

tests/regex/replace/single/single_replace.js

@@ -2,6 +2,7 @@
 
 //Tests a replace on a non global regex
 
+var S$ = require('S$');
 var x = S$.symbol("X", '');
 var b = /(a|b)/;
 

tests/regex/search/alt.js

@@ -2,6 +2,7 @@
 
 //Tests a simple string search
 
+var S$ = require('S$');
 var x = S$.symbol("X", '');
 var b = /^(a|b)$/;
 var nl = x.search(b);

tests/regex/search/ambiguous3.js

@@ -2,6 +2,7 @@
 
 //Tests a simple string search
 
+var S$ = require('S$');
 var x = S$.symbol("X", '');
 
 S$.assume(x.length < 7);

tests/regex/search/ambiguous4.js

@@ -2,6 +2,7 @@
 
 //Tests a simple string search
 
+var S$ = require('S$');
 var x = S$.symbol("X", '');
 var b = /[a-z]*/;
 var nl = x.search(b);

tests/regex/search/not_at_start.js

@@ -1,5 +1,6 @@
 /* Copyright (c) Royal Holloway, University of London | Contact Blake Loring (blake@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 */
 
+var S$ = require('S$');
 var x = S$.symbol("X", '');
 var b = /(a|b)$/;
 var nl = x.search(b);

tests/regex/search/test_at_start.js

@@ -1,5 +1,6 @@
 /* Copyright (c) Royal Holloway, University of London | Contact Blake Loring (blake@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 */
 
+var S$ = require('S$');
 var x = S$.symbol("X", '');
 var b = /(a|b)$/;
 var nl = x.search(b);

tests/regex/split/split_1.js

@@ -2,6 +2,7 @@
 
 //Tests replace on a global regex
 
+var S$ = require('S$');
 var x = S$.symbol("X", '');
 var b = /(a)/;
 

tests/regex/split/split_2.js

@@ -2,6 +2,7 @@
 
 //Tests replace on a global regex
 
+var S$ = require('S$');
 var x = S$.symbol("X", '');
 var b = /(a)/;
 

tests/regex/split/split_3.js

@@ -2,6 +2,7 @@
 
 //Tests replace on a global regex
 
+var S$ = require('S$');
 var x = S$.symbol("X", '');
 var b = /(a)/;
 

tests/regex/split/split_4.js

@@ -2,6 +2,7 @@
 
 //Tests replace on a global regex
 
+var S$ = require('S$');
 var x = S$.symbol("X", '');
 var b = /(a)/;
 

tests/regex/split/split_5.js

@@ -2,6 +2,7 @@
 
 //Tests replace on a global regex
 
+var S$ = require('S$');
 var x = S$.symbol("X", '');
 var b = /.../;
 

tests/regex/split/split_hard.js

@@ -2,6 +2,7 @@
 
 //Tests replace on a global regex
 
+var S$ = require('S$');
 var x = S$.symbol("X", '');
 var b = /(a)/;
 

tests/regex/test/flags/sticky.js

@@ -1,6 +1,8 @@
 /* Copyright (c) Royal Holloway, University of London | Contact Blake Loring (blake@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 */
 
 //Test that multiline changes ^ into (\n or ^) and $ into (\n or $)
+var S$ = require('S$');
+
 var x = S$.symbol("X", '');
 var re = /abc/y;
 

tests/regex/test/flags/sticky2.js

@@ -1,17 +1,18 @@
 /* Copyright (c) Royal Holloway, University of London | Contact Blake Loring (blake@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 */
 
 //Test that multiline changes ^ into (\n or ^) and $ into (\n or $)
+var S$ = require('S$');
 var x = S$.symbol("X", '');
-var re = /abc/y;
+var re = /Hello/y;
 
-S$.assume(x.length < 8);
+S$.assume(x.length < 13);
 
 if (re.test(x)) {
 
 	if (re.test(x)) {
 		//Length < 4, sticky is set, lastIndex should be 3, cant match again
-		throw 'Unreachable';
+		throw 'Reachable 2';
 	}
 
-	throw 'Reachable';
+	throw 'Reachable 1';
 }