Skip to content

regex: model Pattern/Matcher for JBMC's intercepted regex machinery #40

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
tautschnig wants to merge 1 commit into
base: master
Choose a base branch
from
Open

regex: model Pattern/Matcher for JBMC's intercepted regex machinery #40

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
135 changes: 100 additions & 35 deletions src/main/java/java/util/regex/Matcher.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -236,22 +236,36 @@ public final class Matcher implements MatchResult {
// Matcher() {
// }

// DIFFBLUE MODEL LIBRARY The pattern and input this matcher was
// created with, plus two staleness flags (JLS state semantics):
// - cproverImprecise: the REGION no longer covers the whole input
// (region(start, end)); matches()/lookingAt()/find() are all anchored
// to the region, so every query degrades to a sound nondet.
// - cproverFindConsumed: a find() already advanced the (unmodelled)
// match POSITION; only find() depends on it, so only find() degrades.
// matches()/lookingAt() are position-independent per the JLS.
private Pattern cproverPattern;
private String cproverText;
private boolean cproverImprecise;
private boolean cproverFindConsumed;

/**
* All matchers have the state used by Pattern during a match.
*/
// DIFFBLUE MODEL LIBRARY - not used in model
// Matcher(Pattern parent, CharSequence text) {
// this.parentPattern = parent;
// this.text = text;

// // Allocate state storage
// int parentGroupCount = Math.max(parent.capturingGroupCount, 10);
// groups = new int[parentGroupCount * 2];
// locals = new int[parent.localCount];

// // Put fields into initial states
// reset();
// }
Matcher(Pattern parent, CharSequence text) {
// DIFFBLUE MODEL LIBRARY Store the pattern and the input converted
// to a String (String/StringBuilder toString() are intercepted; an
// unknown CharSequence yields a nondet String, keeping queries
// sound). Callers validate arguments (Pattern.matcher throws
// NullPointerException on a null input, per the JDK); the null
// tolerance HERE is defence for nondet-generated Matcher objects
// from the object factory, whose fields may legitimately be null --
// the query methods degrade those to a sound nondet result.
cproverPattern = parent;
cproverText = text == null ? null : text.toString();
cproverImprecise = false;
cproverFindConsumed = false;
}

/**
* Returns the pattern that is interpreted by this matcher.
Expand All @@ -262,9 +276,8 @@ public final class Matcher implements MatchResult {
* @diffblue.noSupport
*/
public Pattern pattern() {
// return parentPattern;
CProver.notModelled();
return CProver.nondetWithoutNullForNotModelled();
// DIFFBLUE MODEL LIBRARY
return cproverPattern;
}

/**
Expand Down Expand Up @@ -321,8 +334,17 @@ public Matcher usePattern(Pattern newPattern) {
// for (int i = 0; i < locals.length; i++)
// locals[i] = -1;
// return this;
CProver.notModelled();
return CProver.nondetWithoutNullForNotModelled();
// DIFFBLUE MODEL LIBRARY Method contract: a null pattern throws
// IllegalArgumentException (see the commented-out original above).
if (newPattern == null) {
throw new IllegalArgumentException("Pattern cannot be null");
}
// JDK: changes the pattern; the region is unchanged and the match
// POSITION is retained (unmodelled), so find() degrades but
// matches()/lookingAt() stay precise.
cproverPattern = newPattern;
cproverFindConsumed = true;
return this;
}

/**
Expand All @@ -349,9 +371,12 @@ public Matcher reset() {
// lastAppendPosition = 0;
// from = 0;
// to = getTextLength();
// return this;
CProver.notModelled();
return CProver.nondetWithoutNullForNotModelled();
// DIFFBLUE MODEL LIBRARY JLS: returns the matcher to its initial
// state (full region, no match state) -- exactly the state the
// model's fields describe, so precision is restored.
cproverImprecise = false;
cproverFindConsumed = false;
return this;
}

/**
Expand All @@ -372,10 +397,16 @@ public Matcher reset() {
* @diffblue.noSupport
*/
public Matcher reset(CharSequence input) {
// text = input;
// return reset();
CProver.notModelled();
return CProver.nondetWithoutNullForNotModelled();
// DIFFBLUE MODEL LIBRARY JDK behaviour: resetting with a null input
// throws NullPointerException (the real reset dereferences the
// text); otherwise resets to the initial state with the new input.
if (input == null) {
throw new NullPointerException();
}
cproverText = input.toString();
cproverImprecise = false;
cproverFindConsumed = false;
return this;
}

/**
Expand Down Expand Up @@ -703,9 +734,14 @@ public int groupCount() {
* @diffblue.noSupport
*/
public boolean matches() {
// return match(from, ENDANCHOR);
CProver.notModelled();
return CProver.nondetBoolean();
// DIFFBLUE MODEL LIBRARY JLS: attempts to match the ENTIRE region
// against the pattern. Delegates to the intercepted String.matches;
// nondet when the pattern/flags/state are outside the model.
if (cproverImprecise || cproverPattern == null || cproverText == null
|| cproverPattern.flags() != 0) {
return CProver.nondetBoolean();
}
return cproverText.matches(cproverPattern.pattern());
}

/**
Expand Down Expand Up @@ -742,7 +778,29 @@ public boolean find() {
// return false;
// }
// return search(nextSearchIndex);
CProver.notModelled();

// DIFFBLUE MODEL LIBRARY JLS: successive find() calls advance
// through the input. The FIRST find() on a fresh (or freshly reset)
// matcher is decided exactly ("does any subsequence match");
// subsequent calls depend on the previous match position, which is
// not modelled, so the matcher degrades to nondet afterwards.
if (cproverImprecise || cproverFindConsumed || cproverPattern == null
|| cproverText == null || cproverPattern.flags() != 0) {
cproverFindConsumed = true;
return CProver.nondetBoolean();
}
cproverFindConsumed = true;
return cproverFind(cproverPattern.pattern(), cproverText);
}

// DIFFBLUE MODEL LIBRARY Intercepted by JBMC (lowered to the SMT regex
// machinery / the concrete matcher); the bodies are the sound fallback.
private static boolean cproverFind(String pattern, String text) {
return CProver.nondetBoolean();
}

// DIFFBLUE MODEL LIBRARY Intercepted by JBMC.
private static boolean cproverLookingAt(String pattern, String text) {
return CProver.nondetBoolean();
}

Expand Down Expand Up @@ -774,7 +832,9 @@ public boolean find(int start) {
// throw new IndexOutOfBoundsException("Illegal start index");
// reset();
// return search(start);
CProver.notModelled();
// DIFFBLUE MODEL LIBRARY offset search is not modelled; the match
// POSITION is consumed (JLS: resets, then searches from `start`).
cproverFindConsumed = true;
return CProver.nondetBoolean();
}

Expand All @@ -796,9 +856,13 @@ public boolean find(int start) {
* @diffblue.noSupport
*/
public boolean lookingAt() {
// return match(from, NOANCHOR);
CProver.notModelled();
return CProver.nondetBoolean();
// DIFFBLUE MODEL LIBRARY JLS: matches the input against the pattern
// anchored at the start only. Intercepted via cproverLookingAt.
if (cproverImprecise || cproverPattern == null || cproverText == null
|| cproverPattern.flags() != 0) {
return CProver.nondetBoolean();
}
return cproverLookingAt(cproverPattern.pattern(), cproverText);
}

/**
Expand Down Expand Up @@ -1189,8 +1253,9 @@ public Matcher region(int start, int end) {
// from = start;
// to = end;
// return this;
CProver.notModelled();
return CProver.nondetWithoutNullForNotModelled();
// DIFFBLUE MODEL LIBRARY region bounds are not modelled.
cproverImprecise = true;
return this;
}

/**
Expand Down
53 changes: 26 additions & 27 deletions src/main/java/java/util/regex/Pattern.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -945,8 +945,9 @@ public final class Pattern
*
* @serial
*/
// DIFFBLUE MODEL LIBRARY - not used in model
// private int flags;
// DIFFBLUE MODEL LIBRARY Stored so flags() returns the compile flags
// (JLS) and the Matcher model can fall back to nondet for flags != 0.
private int cproverFlags;

/**
* Boolean indicating this Pattern is compiled; this is necessary in order
Expand Down Expand Up @@ -1132,10 +1133,15 @@ public Matcher matcher(CharSequence input) {
// compile();
// }
// }
// Matcher m = new Matcher(this, input);
// return m;
CProver.notModelled();
return CProver.nondetWithoutNullForNotModelled();
// DIFFBLUE MODEL LIBRARY A real Matcher carrying this pattern and
// the input, so Matcher.matches()/lookingAt()/find() can decide
// exactly (see the Matcher model). JDK behaviour: a null input
// throws NullPointerException (the real Matcher constructor
// dereferences the text).
if (input == null) {
throw new NullPointerException();
}
return new Matcher(this, input);
}

/**
Expand All @@ -1147,8 +1153,7 @@ public Matcher matcher(CharSequence input) {
* @diffblue.noSupport
*/
public int flags() {
// return flags;
return CProver.nondetInt();
return cproverFlags;
}

/**
Expand Down Expand Up @@ -1207,25 +1212,15 @@ private static void cproverAssumeIsPlainString(String regex)
* If the expression's syntax is invalid
*
* @diffblue.untested
* @diffblue.limitedSupport Regex can only be a plain string.
* @diffblue.fullSupport (via the intercepted regex machinery)
*/
public static boolean matches(String regex, CharSequence input) {
// Pattern p = Pattern.compile(regex);
// Matcher m = p.matcher(input);
// return m.matches();

//
// DIFFBLUE MODEL LIBRARY Delegates to the intercepted matching
// machinery (JLS semantics; no plain-string restriction).
if (input == null) {
throw new NullPointerException(); // JDK throws NPE when the 2nd param is null
Comment thread
tautschnig marked this conversation as resolved.
}
// DIFFBLUE MODEL LIBRARY
// We disallow special characters so that we can do matching using equals.
if (cproverIsPlainString(regex)) {
return regex.equals(input);
} else {
CProver.notModelled();
return CProver.nondetBoolean();
}
return compile(regex).matcher(input).matches();
}

/**
Expand Down Expand Up @@ -1444,15 +1439,19 @@ public static String quote(String s) {
* a Pattern. An empty pattern string results in an object tree with
* only a Start node and a LastNode node.
*/
// DIFFBLUE MODEL LIBRARY - argument `f` is ignored for now but kept
// to stay closer to the original implementation
private Pattern(String p, int f) {
// DIFFBLUE MODEL LIBRARY
// We disallow special characters so that we can use equals for matching.
if (!cproverIsPlainString(p)) {
CProver.notModelled();
// JDK behaviour: compiling a null pattern throws
// NullPointerException (the real constructor dereferences it).
if (p == null) {
throw new NullPointerException();
}
// Store the pattern and flags; matching is delegated to
// String.matches / the Matcher model, which JBMC intercepts (the
// regex is translated to the SMT string theory or evaluated
// concretely; unsupported patterns yield a sound nondet result).
pattern = p;
cproverFlags = f;
// pattern = p;
// flags = f;

Expand Down
Loading