From 03744b0763a0f3de5f6b4309aed5ce13b73e7fd1 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Fri, 19 Jul 2024 09:06:16 -0700 Subject: [PATCH 1/6] SampleTester improvements --- ...t => SampleTester.commands_linear_ternary} | 20 +-- java/daikon/test/SampleTester.decls | 37 ++++-- java/daikon/test/SampleTester.java | 124 ++++++++++-------- 3 files changed, 109 insertions(+), 72 deletions(-) rename java/daikon/test/{SampleTester.test => SampleTester.commands_linear_ternary} (95%) diff --git a/java/daikon/test/SampleTester.test b/java/daikon/test/SampleTester.commands_linear_ternary similarity index 95% rename from java/daikon/test/SampleTester.test rename to java/daikon/test/SampleTester.commands_linear_ternary index 2f00461cb9..31bef925a7 100644 --- a/java/daikon/test/SampleTester.test +++ b/java/daikon/test/SampleTester.commands_linear_ternary @@ -50,11 +50,11 @@ ppt: foo.f():::EXIT35 assert: inv(daikon.inv.ternary.threeScalar.LinearTernary, x, x, z); data: 6 4 12 # should still be a line - assert: show_invs(x,x,z) +# assert: show_invs(x,x,z) assert: inv(daikon.inv.ternary.threeScalar.LinearTernary, x, x, z); data: 1 5 9 # should break the line and form a plane - assert: show_invs(x,y,z) +# assert: show_invs(x,y,z) ################### # the following does not work as planned because of zero coefficients ################### @@ -84,11 +84,11 @@ ppt: foo.f():::EXIT35 assert: inv(daikon.inv.ternary.threeScalar.LinearTernary, x, x, z); data: 6 6 12 # should still be a line -assert: show_invs(x,x,z) +# assert: show_invs(x,x,z) assert: inv(daikon.inv.ternary.threeScalar.LinearTernary, x, x, z); data: 1 5 100 # should break the line and form a plane -assert: show_invs(x,y,z) +# assert: show_invs(x,y,z) ################### # the following does not work as planned because of zero coefficients ################### @@ -130,11 +130,11 @@ ppt: foo.f():::EXIT35 assert: inv(daikon.inv.ternary.threeScalar.LinearTernary, x, x, z); data: 6 5 6 # should break the line and form a plane - assert: show_invs(x,y,z) +# assert: show_invs(x,y,z) assert: inv(daikon.inv.ternary.threeScalar.LinearTernary, x, y, z); data: 8 8 20 # should still be a plane - assert: show_invs(x,y,z) +# assert: show_invs(x,y,z) assert: inv(daikon.inv.ternary.threeScalar.LinearTernary, x, y, z); # should break the plane # data: 0 0 0 @@ -162,11 +162,11 @@ ppt: foo.f():::EXIT35 assert: inv(daikon.inv.ternary.threeScalar.LinearTernary, x, x, z); data: 3 8 10 # should break the line and form a plane - assert: show_invs(x,y,z) +# assert: show_invs(x,y,z) assert: inv(daikon.inv.ternary.threeScalar.LinearTernary, x, y, z); data: 8 16 20 # should still be a plane - assert: show_invs(x,y,z) +# assert: show_invs(x,y,z) assert: inv(daikon.inv.ternary.threeScalar.LinearTernary, x, y, z); # should break the plane data: 0 0 0 @@ -195,11 +195,11 @@ ppt: foo.f():::EXIT35 assert: inv(daikon.inv.ternary.threeScalar.LinearTernary, x, x, z); data: 2 3 1 # should break the line and form a plane - assert: show_invs(x,y,z) +# assert: show_invs(x,y,z) assert: inv(daikon.inv.ternary.threeScalar.LinearTernary, x, y, z); data: 15 15 15 # should still be a plane - assert: show_invs(x,y,z) +# assert: show_invs(x,y,z) assert: inv(daikon.inv.ternary.threeScalar.LinearTernary, x, y, z); # should break the plane data: 2 3 2 diff --git a/java/daikon/test/SampleTester.decls b/java/daikon/test/SampleTester.decls index 73d3000a55..fcf694092f 100644 --- a/java/daikon/test/SampleTester.decls +++ b/java/daikon/test/SampleTester.decls @@ -20,31 +20,31 @@ int 22 DECLARE -foo.g():::ENTER -p +foo.f():::EXIT35 +x int int 22 -q +y int int 22 -r +z int int 22 DECLARE -foo.f():::EXIT35 -x +foo.g():::ENTER +p int int 22 -y +q int int 22 -z +r int int 22 @@ -64,3 +64,24 @@ int int 22 +DECLARE +foo.strings():::ENTER +s +java.lang.String +java.lang.String +22 +a[] +java.lang.String[] +java.lang.String[] +22[22] + +DECLARE +foo.strings():::EXIT1 +s +java.lang.String +java.lang.String +22 +a[] +java.lang.String[] +java.lang.String[] +22[22] diff --git a/java/daikon/test/SampleTester.java b/java/daikon/test/SampleTester.java index 3e9a823f13..e455085cfa 100644 --- a/java/daikon/test/SampleTester.java +++ b/java/daikon/test/SampleTester.java @@ -133,17 +133,8 @@ public static void main(String[] args) throws IOException { daikon.LogHelper.setupLogs(Global.debugAll ? FINE : INFO); - try (InputStream commands = SampleTester.class.getResourceAsStream("SampleTester.commands")) { - if (commands == null) { - fail( - "Input file SampleTester.commands missing." - + " (Should be in daikon.test and it must be within the classpath)"); - } - - SampleTester ts = new SampleTester(); - ts.proc_sample_file(commands, "SampleTester.commands"); - System.out.println("Test Passes"); - } + new SampleTester().test_samples(); + System.out.println("Test Passes"); } private static @Nullable String find_file(String fname) { @@ -164,18 +155,29 @@ public static void main(String[] args) throws IOException { */ @Test public void test_samples() throws IOException { + test_samples("SampleTester.commands"); + test_samples("SampleTester.commands_linear_ternary"); + } + + /** + * This function is the actual function performed when this class is run through JUnit. + * + * @throws IOException if there in a problem with I/O + */ + public void test_samples(String commandFile) throws IOException { FileIO.new_decl_format = null; - try (InputStream commands = getClass().getResourceAsStream("SampleTester.commands")) { + try (InputStream commands = getClass().getResourceAsStream(commandFile)) { if (commands == null) { fail( - "Input file SampleTester.commands missing." + "Missing input file: " + + commandFile + " (Should be in daikon.test and it must be within the classpath)"); } SampleTester ts = new SampleTester(); - ts.proc_sample_file(commands, "SampleTester.commands"); + ts.proc_sample_file(commands, commandFile); } } @@ -303,6 +305,7 @@ private void proc_vars(String var_names) { private void proc_data(String data, LineNumberReader reader, String filename) { if (vars == null) parse_error("vars must be specified before data"); + // TODO: This does not work for arrays. String[] da = data.split(" *"); if (da.length != vars.length) parse_error("number of data elements doesn't match var elements"); debug_progress.fine("data: " + Debug.toString(da)); @@ -373,50 +376,62 @@ private void proc_assert(String assertion) throws IOException { assert_string = assert_string.substring(1); } - // Create a tokenizer over the assertion string - StreamTokenizer stok = new StreamTokenizer(new StringReader(assert_string)); - stok.commentChar('#'); - stok.quoteChar('"'); + boolean result = false; + + try { - int ttype; + // Create a tokenizer over the assertion string + StreamTokenizer stok = new StreamTokenizer(new StringReader(assert_string)); + stok.wordChars('_', '_'); + stok.commentChar('#'); + stok.quoteChar('"'); - // Get the assertion name - ttype = stok.nextToken(); - assertEquals(TT_WORD, ttype); - String name = stok.sval; - - // Get the arguments (enclosed in parens, separated by commas) - String delimiter = readString(stok); - assertEquals("(", delimiter); - - List args = new ArrayList<>(10); - do { - String arg = readString(stok); - args.add(arg); - delimiter = readString(stok); - } while (delimiter.equals(",")); - if (!delimiter.equals(")")) { - parse_error(String.format("%s found where ')' expected", delimiter)); - } + int ttype; - // process the specific assertion - boolean result = false; - if (name.equals("inv")) { - result = proc_inv_assert(args); - if (!result && !negate) { - daikon.LogHelper.setLevel(debug, FINE); - proc_inv_assert(args); + // Get the assertion name + ttype = stok.nextToken(); + assertEquals(TT_WORD, ttype); + String name = stok.sval; + + // Get the arguments (enclosed in parens, separated by commas) + String delimiter = readString(stok); + if (!"(".equals(delimiter)) { + throw new Error("Expected \"(\", got: " + delimiter); + } + + List args = new ArrayList<>(10); + do { + String arg = readString(stok); + args.add(arg); + delimiter = readString(stok); + } while (delimiter.equals(",")); + if (!delimiter.equals(")")) { + parse_error(String.format("%s found where ')' expected", delimiter)); } - } else if (name.equals("show_invs")) { - result = proc_show_invs_assert(args); - } else if (name.equals("constant")) { - result = proc_constant_assert(args); - } else { - parse_error("unknown assertion: " + name); - } - if (negate) { - result = !result; + // process the specific assertion + if (name.equals("inv")) { + result = proc_inv_assert(args); + if (!result && !negate) { + daikon.LogHelper.setLevel(debug, FINE); + proc_inv_assert(args); + } + } else if (name.equals("show_invs")) { + result = proc_show_invs_assert(args); + } else if (name.equals("constant")) { + result = proc_constant_assert(args); + } else { + parse_error("unknown assertion: " + name); + } + + if (negate) { + result = !result; + } + } catch (Throwable t) { + throw new Error( + String.format( + "Problem in file %s, line %d, assertion: " + assertion, fname, fp.getLineNumber()), + t); } if (!result) { @@ -504,8 +519,9 @@ private boolean proc_show_invs_assert(List args) { } // Look for a matching invariant in the slices invariant list + System.out.printf("SampleTester show_invs: %d invariants%n", slice.invs.size()); for (Invariant inv : slice.invs) { - System.out.printf("found %s: %s%n", inv.getClass(), inv.format()); + System.out.printf(" %s: %s%n", inv.getClass(), inv.format()); } return true; } From b6108f65b45a6639213dd9f43f3d1fc73386c236 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Fri, 19 Jul 2024 10:40:58 -0700 Subject: [PATCH 2/6] Permit array values in SampleTester --- java/daikon/test/SampleTester.java | 73 ++++++++++++++++++++++++++++-- 1 file changed, 68 insertions(+), 5 deletions(-) diff --git a/java/daikon/test/SampleTester.java b/java/daikon/test/SampleTester.java index e455085cfa..a19dea0160 100644 --- a/java/daikon/test/SampleTester.java +++ b/java/daikon/test/SampleTester.java @@ -34,10 +34,14 @@ import java.util.HashSet; import java.util.List; import java.util.Set; +import java.util.StringJoiner; import java.util.logging.Logger; +import java.util.regex.Matcher; +import java.util.regex.Pattern; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.checker.signature.qual.ClassGetName; import org.junit.Test; +import org.plumelib.util.IPair; import org.plumelib.util.StringsPlume; /** @@ -305,9 +309,9 @@ private void proc_vars(String var_names) { private void proc_data(String data, LineNumberReader reader, String filename) { if (vars == null) parse_error("vars must be specified before data"); - // TODO: This does not work for arrays. - String[] da = data.split(" *"); - if (da.length != vars.length) parse_error("number of data elements doesn't match var elements"); + List da = splitData(data); + if (da.size() != vars.length) + parse_error(String.format("%d vars but %d data elements: %s", vars.length, da.size(), data)); debug_progress.fine("data: " + Debug.toString(da)); VarInfo[] vis = ppt.var_infos; @@ -323,11 +327,12 @@ private void proc_data(String data, LineNumberReader reader, String filename) { // Parse and enter the specified variables, - indicates a missing value for (int i = 0; i < vars.length; i++) { - if (da[i].equals("-")) { + String val = da.get(i); + if (val.equals("-")) { continue; } VarInfo vi = vars[i]; - vals[vi.value_index] = vi.rep_type.parse_value(da[i], reader, filename); + vals[vi.value_index] = vi.rep_type.parse_value(val, reader, filename); mods[vi.value_index] = ValueTuple.parseModified("1"); } @@ -348,6 +353,64 @@ private void proc_data(String data, LineNumberReader reader, String filename) { ppt.add_bottom_up(vt, 1); } + /** + * Splits a "data:" line of a SampleTester input file. + * + * @return the components of a "data:" line of a SampleTester input file + */ + private List splitData(String s) { + s = s.trim(); + List result = new ArrayList<>(); + while (!s.isEmpty()) { + IPair p = readValueFromBeginning(s); + result.add(p.first); + s = p.second; + } + return result; + } + + /** + * Reads a value from the beginning of a string. + * + * @return the value and the remaining string + */ + private IPair readValueFromBeginning(String s) { + s = s.trim(); + if (s.isEmpty()) { + throw new Error("Cannot read a value from an empty string"); + } + switch (s.charAt(0)) { + case '"': + for (int i = 1; i < s.length(); i++) { + switch (s.charAt(i)) { + case '"': + return IPair.of(s.substring(0, i + i), s.substring(i).trim()); + case '\\': + i++; + break; + default: + break; + } + } + throw new Error("Unterminated string: " + s); + case '[': + StringJoiner sj = new StringJoiner(" ", "[", "]"); + s = s.substring(1); + while (!s.startsWith("]")) { + IPair p = readValueFromBeginning(s); + sj.add(p.first); + s = p.second; + } + return IPair.of(sj.toString(), s.substring(1).trim()); + default: + Matcher m = spaceOrCloseBracket.matcher(s); + int pos = m.find() ? m.start() : s.length(); + return IPair.of(s.substring(0, pos), s.substring(pos).trim()); + } + } + + Pattern spaceOrCloseBracket = Pattern.compile("[] ]"); + /** Requires that the StreamTokenizer has just read a word. Returns that word. */ private String readString(StreamTokenizer stok) { int ttype; From 788440b4a7c2264713eb3c733d85c882801bfd0e Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Fri, 19 Jul 2024 10:54:50 -0700 Subject: [PATCH 3/6] Add test --- java/daikon/test/SampleTester.java | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/java/daikon/test/SampleTester.java b/java/daikon/test/SampleTester.java index a19dea0160..e6f4a6b168 100644 --- a/java/daikon/test/SampleTester.java +++ b/java/daikon/test/SampleTester.java @@ -152,6 +152,16 @@ public static void main(String[] args) throws IOException { } } + @Test + public void test_splitData() { + assertEquals(2, splitData("\"foo@bar.com\" [\"foo@bar.com\"]").size()); + assertEquals(2, splitData("\"baz@a.b.edu\" [\"baz@a.b.edu\" \"baz@a.b.edu\"]").size()); + assertEquals(2, splitData("\"a@b.c.biz\" []").size()); + assertEquals(2, splitData("\"b@b.c.biz\" [\"a@b.c.biz\"]").size()); + assertEquals(2, splitData("\"c@b.c.biz\" [\"c@b.c.biz\" \"c@b.c.biz\" \"c@b.c.biz\"]").size()); + assertEquals(2, splitData("- []").size()); + } + /** * This function is the actual function performed when this class is run through JUnit. * @@ -384,7 +394,7 @@ private IPair readValueFromBeginning(String s) { for (int i = 1; i < s.length(); i++) { switch (s.charAt(i)) { case '"': - return IPair.of(s.substring(0, i + i), s.substring(i).trim()); + return IPair.of(s.substring(0, i + 1), s.substring(i + 1).trim()); case '\\': i++; break; From 2f94c36c768496980fb450a3e4bcf3ee616bbf1a Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Fri, 19 Jul 2024 11:13:04 -0700 Subject: [PATCH 4/6] More array support --- java/daikon/test/SampleTester.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/java/daikon/test/SampleTester.java b/java/daikon/test/SampleTester.java index e6f4a6b168..30dcf020d9 100644 --- a/java/daikon/test/SampleTester.java +++ b/java/daikon/test/SampleTester.java @@ -419,6 +419,7 @@ private IPair readValueFromBeginning(String s) { } } + /** A regular expression that matches a space or a close square bracket. */ Pattern spaceOrCloseBracket = Pattern.compile("[] ]"); /** Requires that the StreamTokenizer has just read a word. Returns that word. */ @@ -475,8 +476,12 @@ private void proc_assert(String assertion) throws IOException { List args = new ArrayList<>(10); do { String arg = readString(stok); - args.add(arg); delimiter = readString(stok); + while (delimiter.equals("[") || delimiter.equals("]")) { + arg += delimiter; + delimiter = readString(stok); + } + args.add(arg); } while (delimiter.equals(",")); if (!delimiter.equals(")")) { parse_error(String.format("%s found where ')' expected", delimiter)); From 81a667cf36de2752cde6da0fbf3f405198807c0f Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Fri, 19 Jul 2024 11:17:22 -0700 Subject: [PATCH 5/6] Adjust file name --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 56bd8abf51..e714a436e5 100644 --- a/Makefile +++ b/Makefile @@ -73,7 +73,7 @@ DAIKON_RESOURCE_FILES := daikon/config/example-settings.txt \ daikon/test/SampleTester.commands \ daikon/test/SampleTester.decls \ daikon/test/SampleTesterGlobal.decls \ - daikon/test/SampleTester.test \ + daikon/test/SampleTester.commands_linear_ternary \ daikon/test/varInfoNameTest.testEscForall \ daikon/test/varInfoNameTest.testEscForall.goal \ daikon/test/varInfoNameTest.testJML \ From 716719472b8e93d61c6601bd2ee1b7d4f3adacb6 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Fri, 19 Jul 2024 17:45:59 -0700 Subject: [PATCH 6/6] Add Javadoc --- java/daikon/test/SampleTester.java | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/java/daikon/test/SampleTester.java b/java/daikon/test/SampleTester.java index 30dcf020d9..c84015087b 100644 --- a/java/daikon/test/SampleTester.java +++ b/java/daikon/test/SampleTester.java @@ -152,6 +152,7 @@ public static void main(String[] args) throws IOException { } } + /** Test {@link #splitData}. */ @Test public void test_splitData() { assertEquals(2, splitData("\"foo@bar.com\" [\"foo@bar.com\"]").size()); @@ -176,6 +177,7 @@ public void test_samples() throws IOException { /** * This function is the actual function performed when this class is run through JUnit. * + * @param commandFile the file containing the commands * @throws IOException if there in a problem with I/O */ public void test_samples(String commandFile) throws IOException { @@ -366,6 +368,7 @@ private void proc_data(String data, LineNumberReader reader, String filename) { /** * Splits a "data:" line of a SampleTester input file. * + * @param s the "data:" line of a SampleTester input file * @return the components of a "data:" line of a SampleTester input file */ private List splitData(String s) { @@ -382,7 +385,8 @@ private List splitData(String s) { /** * Reads a value from the beginning of a string. * - * @return the value and the remaining string + * @param s a string containing a sequence of Daikon dtrace values, separated by spaces + * @return the first value and the remaining string */ private IPair readValueFromBeginning(String s) { s = s.trim(); @@ -422,7 +426,12 @@ private IPair readValueFromBeginning(String s) { /** A regular expression that matches a space or a close square bracket. */ Pattern spaceOrCloseBracket = Pattern.compile("[] ]"); - /** Requires that the StreamTokenizer has just read a word. Returns that word. */ + /** + * Requires that the StreamTokenizer has just read a word. Returns that word. + * + * @param stok a StreamTokenizer that has just read a word + * @return the word that the StreamTokenizer just read + */ private String readString(StreamTokenizer stok) { int ttype; try { @@ -508,7 +517,7 @@ private void proc_assert(String assertion) throws IOException { } catch (Throwable t) { throw new Error( String.format( - "Problem in file %s, line %d, assertion: " + assertion, fname, fp.getLineNumber()), + "Problem in file %s, line %d, assertion: %s", fname, fp.getLineNumber(), assertion), t); }