diff --git a/src/main/java/java/util/regex/Matcher.java b/src/main/java/java/util/regex/Matcher.java index 3f529f9..03130fa 100644 --- a/src/main/java/java/util/regex/Matcher.java +++ b/src/main/java/java/util/regex/Matcher.java @@ -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. @@ -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; } /** @@ -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; } /** @@ -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; } /** @@ -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; } /** @@ -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()); } /** @@ -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(); } @@ -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(); } @@ -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); } /** @@ -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; } /** diff --git a/src/main/java/java/util/regex/Pattern.java b/src/main/java/java/util/regex/Pattern.java index ff12bfe..0f870ea 100644 --- a/src/main/java/java/util/regex/Pattern.java +++ b/src/main/java/java/util/regex/Pattern.java @@ -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 @@ -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); } /** @@ -1147,8 +1153,7 @@ public Matcher matcher(CharSequence input) { * @diffblue.noSupport */ public int flags() { - // return flags; - return CProver.nondetInt(); + return cproverFlags; } /** @@ -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 } - // 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(); } /** @@ -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;