<commit_before>import Z3 from "z3javascript";
import { ConcolicValue } from "../Values/WrappedValue";
import Config from "../Config";
import Log from "../Utilities/Log";

export default function(state, ctx, model, helpers) {

	const symbolicHookRe = helpers.symbolicHookRe;
	const coerceToString = helpers.coerceToString;

	function DoesntMatch(l, r) {
		if (l == undefined) {
			const is_match = (r == "") || (r == undefined);
			return !is_match;
		} else {
			return l == r;
		} 
	}

	function Exists(array1, array2, pred) {

		for (let i = 0; i < array1.length; i++) {
			if (pred(array1[i], array2[i])) {
				return true;
			}
		}

		return false;
	}

	function EnableCaptures(regex, real, string_s) {

		if (!Config.capturesEnabled) {
			Log.log("Captures disabled - potential loss of precision");
		}

		Log.logMid("Captures Enabled - Adding Implications");

		const implies = ctx.mkImplies(ctx.mkSeqInRe(string_s, regex.ast),
				ctx.mkEq(string_s, regex.implier));

		//Mock the symbolic conditional if (regex.test(/.../) then regex.match => true)
		regex.assertions.forEach(binder => state.pushCondition(binder, true));
		state.pushCondition(implies, true);
	}

	function BuildRefinements(regex, real, string_s) {

		if (!(Config.capturesEnabled && Config.refinementsEnabled)) {
			Log.log("Refinements disabled - potential accuracy loss");
			return {
trueCheck: [],
					 falseCheck: []
			};
		}

		Log.log("Refinements Enabled - Adding checks");

		state.stats.seen("Regex Which May Need Checks");

		function CheckCorrect(model) {
			const real_match = real.exec(model.eval(string_s).asConstant(model));
			const sym_match = regex.captures.map(cap => model.eval(cap).asConstant(model));

			Log.logMid(`Regex sanity check ${JSON.stringify(real_match)} vs ${JSON.stringify(sym_match)}`);

			const is_correct = real_match && !Exists(real_match, sym_match, DoesntMatch);

			state.stats.seen("Regex Checks");	

			if (!is_correct) {
				state.stats.seen("Failed Regex Checks");
			}

			return is_correct;
		}

		function CheckFailed(model) {
			const is_failed = !real.test(model.eval(string_s).asConstant(model));
			state.stats.seen("Regex Checks");
			if (!is_failed) {
				state.stats.seen("Failed Regex Checks"); 
			}

			return is_failed;
		}

		const NotMatch = Z3.Check(CheckCorrect, (query, model) => {

				const not = ctx.mkNot(
						ctx.mkEq(string_s, ctx.mkString(model.eval(string_s).asConstant(model)))
						);

				return [new Z3.Query(query.exprs.slice(0).concat([not]), [CheckFixed, NotMatch])];
				});

		/**
		 * Generate a fixed string refinement (c_0, c_n, ...) == (e_0, e_n, ...)
		 */
		const CheckFixed = Z3.Check(CheckCorrect, (query, model) => {
				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}`);
				return [];
				}

				real_match = real_match.map(match => match || "");

				const query_list = regex.captures.map(
						(cap, idx) => ctx.mkEq(ctx.mkString(real_match[idx]), cap)
						);

				return [new Z3.Query(query.exprs.slice(0).concat(query_list), [])];
				});

		const CheckNotIn = Z3.Check(CheckFailed, (query, model) => {
				const existing_queries = query.expr.slice(0);
				const not_eq = ctx.mkNot(ctx.mkEq(string_s, model.eval(string_s)));
				return [new Z3.Query(existing_queries.concat([not_eq]))];
				});

		return {
trueCheck: [NotMatch, CheckFixed],
					 falseCheck: [CheckNotIn]
		};
	}
<commit_msg>Tweaks to RegexModels before the rebuild<commit_after>import Z3 from "z3javascript";
import { ConcolicValue } from "../Values/WrappedValue";
import Config from "../Config";
import Log from "../Utilities/Log";

export default function(state, ctx, model, helpers) {

	const symbolicHookRe = helpers.symbolicHookRe;
	const coerceToString = helpers.coerceToString;

	function DoesntMatch(l, r) {
		if (l == undefined) {
			const is_match = (r == "") || (r == undefined);
			return !is_match;
		} else {
			return l == r;
		} 
	}

	function Exists(array1, array2, pred) {

		for (let i = 0; i < array1.length; i++) {
			if (pred(array1[i], array2[i])) {
				return true;
			}
		}

		return false;
	}

	function EnableCaptures(regex, real, string_s) {

		if (!Config.capturesEnabled) {
			Log.log("Captures disabled - potential loss of precision");
		}

		Log.logMid("Captures Enabled - Adding Implications");

		const implies = ctx.mkImplies(ctx.mkSeqInRe(string_s, regex.ast),
				ctx.mkEq(string_s, regex.implier));

		//Mock the symbolic conditional if (regex.test(/.../) then regex.match => true)
		regex.assertions.forEach(binder => state.pushCondition(binder, true));
		state.pushCondition(implies, true);
	}

	function BuildRefinements(regex, real, string_s) {

		if (!(Config.capturesEnabled && Config.refinementsEnabled)) {
			Log.log("Refinements disabled - potential accuracy loss");
			return {
trueCheck: [],
					 falseCheck: []
			};
		}

		Log.log("Refinements Enabled - Adding checks");

		state.stats.seen("Regex Which May Need Checks");

		function CheckCorrect(model) {
			const real_match = real.exec(model.eval(string_s).asConstant(model));
			const sym_match = regex.captures.map(cap => model.eval(cap).asConstant(model));

			Log.logMid(`Regex sanity check ${JSON.stringify(real_match)} vs ${JSON.stringify(sym_match)}`);

			const is_correct = real_match && !Exists(real_match, sym_match, DoesntMatch);

			state.stats.seen("Regex Checks");	

			if (!is_correct) {
				state.stats.seen("Failed Regex Checks");
			}

			return is_correct;
		}

		function CheckFailed(model) {
			const is_failed = !real.test(model.eval(string_s).asConstant(model));
			state.stats.seen("Regex Checks");
			if (!is_failed) {
				state.stats.seen("Failed Regex Checks"); 
			}

			return is_failed;
		}

		const NotMatch = Z3.Check(CheckCorrect, (query, model) => {

				const not = ctx.mkNot(
						ctx.mkEq(string_s, ctx.mkString(model.eval(string_s).asConstant(model)))
						);

				return [new Z3.Query(query.exprs.slice(0).concat([not]), [CheckFixed, NotMatch])];
				});

		/**
		 * Generate a fixed string refinement (c_0, c_n, ...) == (e_0, e_n, ...)
		 */
		const CheckFixed = Z3.Check(CheckCorrect, (query, model) => {
				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}`);
				return [];
				}

				real_match = real_match.map(match => match || "");

				const query_list = regex.captures.map(
						(cap, idx) => ctx.mkEq(ctx.mkString(real_match[idx]), cap)
						);

				return [new Z3.Query(query.exprs.slice(0).concat(query_list), [])];
				});

		const CheckNotIn = Z3.Check(CheckFailed, (query, model) => {
			const existing_queries = query.expr.slice(0);
			const not_eq = ctx.mkNot(ctx.mkEq(string_s, model.eval(string_s)));
			return [new Z3.Query(existing_queries.concat([not_eq]))];
		});

		return {
			trueCheck: [NotMatch, CheckFixed],
			//falseCheck: [CheckNotIn]
		};
	}

{'fraction_non_alphanumeric': 0.15877993158494869, 'fraction_numerical': 0.005416191562143672, 'mean_word_length': 3.7637474541751526, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 19, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1666651', 'n_tokens_mistral': 2780, 'n_tokens_neox': 2358, 'n_words': 491}