AGORA invariants, without introducing a new variable to check for "always empty"

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 \

doc/CHANGELOG.md

@@ -19,6 +19,35 @@ Further documentation can be found in:
    It is also available at http://plse.cs.washington.edu/daikon/download/api/ .
 
 
+Version 5.9.0 (??)
+=============================
+
+Daikon supports the following new invariants, over strings and sequences of
+strings; all of them are enabled by default:
+ * IsUrl
+ * FixedLengthString
+ * IsNumeric
+ * IsEmail
+ * IsDateYYYYMMDD
+ * IsDateDDMMYYYY
+ * IsDateMMDDYYYY
+ * IsTimeOfDay
+ * IsTimeOfDayWithSeconds
+ * IsTimeOfDayAMPM
+ * IsTimestampYYYYMMHHThhmmssmm
+ * SequenceFixedLengthString
+ * SequenceStringElementsAreUrl
+ * SequenceStringElementsAreNumeric
+ * SequenceStringElementsAreEmail
+ * SequenceStringElementsAreDateYYYYMMDD
+ * SequenceStringElementsAreDateDDMMYYYY
+ * SequenceStringElementsAreDateMMDDYYYY
+ * SequenceStringElementsAreTimeOfDay
+ * SequenceStringElementsAreTimeOfDayWithSeconds
+ * SequenceStringElementsAreTimeOfDayAMPM
+ * SequenceStringElementsAreTimestampYYYYMMHHThhmmssmm
+
+
 Version 5.8.20 (May 14, 2024)
 =============================
 

java/daikon/Daikon.java

@@ -150,11 +150,33 @@
 import daikon.inv.unary.sequence.SeqIndexIntLessThan;
 import daikon.inv.unary.sequence.SeqIndexIntNonEqual;
 import daikon.inv.unary.string.CompleteOneOfString;
+import daikon.inv.unary.string.FixedLengthString;
+import daikon.inv.unary.string.IsEmail;
+import daikon.inv.unary.string.IsNumeric;
+import daikon.inv.unary.string.IsUrl;
 import daikon.inv.unary.string.OneOfString;
 import daikon.inv.unary.string.PrintableString;
+import daikon.inv.unary.string.dates.IsDateDDMMYYYY;
+import daikon.inv.unary.string.dates.IsDateMMDDYYYY;
+import daikon.inv.unary.string.dates.IsDateYYYYMMDD;
+import daikon.inv.unary.string.dates.IsTimeOfDay;
+import daikon.inv.unary.string.dates.IsTimeOfDayAMPM;
+import daikon.inv.unary.string.dates.IsTimeOfDayWithSeconds;
+import daikon.inv.unary.string.dates.IsTimestampYYYYMMHHThhmmssmm;
 import daikon.inv.unary.stringsequence.CommonStringSequence;
 import daikon.inv.unary.stringsequence.EltOneOfString;
 import daikon.inv.unary.stringsequence.OneOfStringSequence;
+import daikon.inv.unary.stringsequence.SequenceFixedLengthString;
+import daikon.inv.unary.stringsequence.SequenceStringElementsAreEmail;
+import daikon.inv.unary.stringsequence.SequenceStringElementsAreNumeric;
+import daikon.inv.unary.stringsequence.SequenceStringElementsAreUrl;
+import daikon.inv.unary.stringsequence.dates.SequenceStringElementsAreDateDDMMYYYY;
+import daikon.inv.unary.stringsequence.dates.SequenceStringElementsAreDateMMDDYYYY;
+import daikon.inv.unary.stringsequence.dates.SequenceStringElementsAreDateYYYYMMDD;
+import daikon.inv.unary.stringsequence.dates.SequenceStringElementsAreTimeOfDay;
+import daikon.inv.unary.stringsequence.dates.SequenceStringElementsAreTimeOfDayAMPM;
+import daikon.inv.unary.stringsequence.dates.SequenceStringElementsAreTimeOfDayWithSeconds;
+import daikon.inv.unary.stringsequence.dates.SequenceStringElementsAreTimestampYYYYMMHHThhmmssmm;
 import daikon.simplify.LemmaStack;
 import daikon.split.ContextSplitterFactory;
 import daikon.split.PptSplitter;
@@ -1541,6 +1563,19 @@ public static void setup_proto_invs() {
       proto_invs.add(CompleteOneOfString.get_proto());
       proto_invs.add(CompleteOneOfScalar.get_proto());
 
+      // String formats
+      proto_invs.add(IsUrl.get_proto());
+      proto_invs.add(FixedLengthString.get_proto());
+      proto_invs.add(IsNumeric.get_proto());
+      proto_invs.add(IsEmail.get_proto());
+      proto_invs.add(IsDateYYYYMMDD.get_proto());
+      proto_invs.add(IsDateDDMMYYYY.get_proto());
+      proto_invs.add(IsDateMMDDYYYY.get_proto());
+      proto_invs.add(IsTimeOfDay.get_proto());
+      proto_invs.add(IsTimeOfDayWithSeconds.get_proto());
+      proto_invs.add(IsTimeOfDayAMPM.get_proto());
+      proto_invs.add(IsTimestampYYYYMMHHThhmmssmm.get_proto());
+
       // Positive (x > 0) (Postive.java).  Positive is a sample invariant
       // that is only included as an example.
       // proto_invs.add (Postive.get_proto());
@@ -1606,6 +1641,19 @@ public static void setup_proto_invs() {
 
       // CommonStringSequence (CommonStringSubsequence.java)
       proto_invs.add(CommonStringSequence.get_proto());
+
+      // String formats
+      proto_invs.add(SequenceFixedLengthString.get_proto());
+      proto_invs.add(SequenceStringElementsAreUrl.get_proto());
+      proto_invs.add(SequenceStringElementsAreNumeric.get_proto());
+      proto_invs.add(SequenceStringElementsAreEmail.get_proto());
+      proto_invs.add(SequenceStringElementsAreDateYYYYMMDD.get_proto());
+      proto_invs.add(SequenceStringElementsAreDateDDMMYYYY.get_proto());
+      proto_invs.add(SequenceStringElementsAreDateMMDDYYYY.get_proto());
+      proto_invs.add(SequenceStringElementsAreTimeOfDay.get_proto());
+      proto_invs.add(SequenceStringElementsAreTimeOfDayWithSeconds.get_proto());
+      proto_invs.add(SequenceStringElementsAreTimeOfDayAMPM.get_proto());
+      proto_invs.add(SequenceStringElementsAreTimestampYYYYMMHHThhmmssmm.get_proto());
     }
 
     // Binary scalar-scalar invariants
@@ -1808,9 +1856,16 @@ public static void createUpperPpts(PptMap all_ppts) {
     // Process each ppt that doesn't have a parent
     // (mergeInvs is called on a root, and recursively processes children)
     for (PptTopLevel ppt : all_ppts.pptIterable()) {
-      // System.out.printf("considering ppt %s parents: %s, children: %s%n",
-      //                     ppt.name, ppt.parents, ppt.children);
       if (ppt.parents.size() == 0) {
+        boolean debug =
+            ppt.name()
+                .startsWith(
+                    "com.rolemodelsoft.drawlet.basics.AbstractFigure.addPropertyChangeListener(java.beans.PropertyChangeListener)");
+        if (debug) {
+          System.out.printf(
+              "createUpperPpts: %s%n  parents: %s%n  children: %s%n",
+              ppt.name, ppt.parents, ppt.children);
+        }
         ppt.mergeInvs();
       }
     }

java/daikon/MergeInvariants.java

@@ -67,6 +67,8 @@ public static void main(final String[] args)
           OptionalDataException,
           IOException,
           ClassNotFoundException {
+    LogHelper.setLevel("daikon.MergeInvariants", FINE);
+    LogHelper.setLevel("daikon.MergeInvariants.progress", FINE);
     try {
       mainHelper(args);
     } catch (Daikon.DaikonTerminationException e) {
@@ -238,12 +240,21 @@ public static void mainHelper(String[] args)
         } else {
           PptMap pmap = FileIO.read_serialized_pptmap(file, true);
           for (PptTopLevel ppt : pmap.pptIterable()) {
+            boolean debug =
+                ppt.name()
+                    .startsWith(
+                        "com.rolemodelsoft.drawlet.basics.AbstractFigure.addPropertyChangeListener(java.beans.PropertyChangeListener)");
+
             if (merge_ppts.containsName(ppt.name())) {
-              // System.out.printf("Not adding ppt %s from %s%n", ppt, file);
+              if (debug) {
+                System.out.printf("Not adding ppt %s from %s%n", ppt, file);
+              }
               continue;
             }
+            if (debug) {
+              System.out.printf("Adding ppt %s from %s%n", ppt, file);
+            }
             merge_ppts.add(ppt);
-            // System.out.printf("Adding ppt %s from %s%n", ppt, file);
 
             // Make sure that the parents of this ppt are already in
             // the map.  This will be true if all possible children of
@@ -286,6 +297,14 @@ public static void mainHelper(String[] args)
     debugProgress.fine("Building hierarchy between leaves of the maps");
     for (PptTopLevel ppt : merge_ppts.pptIterable()) {
 
+      boolean debug =
+          ppt.name()
+              .startsWith(
+                  "com.rolemodelsoft.drawlet.basics.AbstractFigure.addPropertyChangeListener(java.beans.PropertyChangeListener)");
+      if (debug) {
+        System.out.printf("MergeInvariants processing ppt " + ppt);
+      }
+
       // Skip everything that is not a final exit point
       if (!ppt.ppt_name.isExitPoint()) {
         assert ppt.children.size() > 0 : ppt;
@@ -296,8 +315,9 @@ public static void mainHelper(String[] args)
         continue;
       }
 
-      // System.out.printf("Including ppt %s, %d children%n", ppt,
-      //                   ppt.children.size());
+      if (debug) {
+        System.out.printf("Including ppt %s, %d children%n", ppt, ppt.children.size());
+      }
 
       // Splitters should not have any children to begin with
       if (ppt.has_splitters()) {
@@ -313,7 +333,9 @@ public static void mainHelper(String[] args)
       for (int j = 0; j < pptmaps.size(); j++) {
         PptMap pmap = pptmaps.get(j);
         PptTopLevel child = pmap.get(ppt.name());
-        // System.out.printf("found child %s from pmap %d%n", child, j);
+        if (debug) {
+          System.out.printf("found child %s from pmap %d%n", child, j);
+        }
         if (child == null) {
           continue;
         }
@@ -351,10 +373,15 @@ public static void mainHelper(String[] args)
           assert ppt.splitters != null; // because ppt.has_splitters() = true
           setup_conditional_merge(ppt, child);
         } else {
+          // The returned value is ignored, but it is already stored in the parent and child.
           PptRelation.newMergeChildRel(ppt, child);
         }
       }
 
+      if (debug) {
+        System.out.println("children of " + ppt + " = " + ppt.children);
+      }
+
       // Make sure at least one child was found
       assert ppt.children.size() > 0 : ppt;
       if (ppt.has_splitters()) {
@@ -379,9 +406,25 @@ public static void mainHelper(String[] args)
         }
       }
     }
+    System.out.println("PPT Hierarchy");
+    for (PptTopLevel ppt : merge_ppts.pptIterable()) {
+      boolean debug =
+          ppt.name()
+              .startsWith(
+                  "com.rolemodelsoft.drawlet.basics.AbstractFigure.addPropertyChangeListener(java.beans.PropertyChangeListener)");
+
+      if (debug) {
+        if (ppt.parents.size() == 0) {
+          System.out.println("  TODO: " + ppt);
+          // TODO:
+          // ppt.debug_print_tree(debug, 0, null);
+        }
+      }
+    }
 
     // Merge the invariants
     debugProgress.fine("Merging invariants");
+    System.out.printf("Merging invariants; about to call Daikon.createUpperPpts");
     Daikon.createUpperPpts(merge_ppts);
 
     // Equality post processing

java/daikon/PptSlice.java.jpp

@@ -602,6 +602,10 @@ public final class PPTSLICE1 extends PptSlice {
    */
   public void merge_invariants() {
 
+    boolean debug = parent.name()
+                .startsWith(
+                    "com.rolemodelsoft.drawlet.basics.AbstractFigure.addPropertyChangeListener(java.beans.PropertyChangeListener)");
+
     if (debugMerge.isLoggable(Level.FINE)) {
       debugMerge.fine("entering merge_invariants for " + name());
     }
@@ -734,6 +738,10 @@ public final class PPTSLICE1 extends PptSlice {
       }
     }
 
+    if (debug) {
+      System.out.println("Found " + all_invs.size() + " invariants to merge");
+      System.out.println(all_invs);
+    }
     log("Found " + all_invs.size() + " invariants to merge");
     if (debugMerge.isLoggable(Level.FINE) && (valid_child_count == 0)) {
       debugMerge.fine("-- No valid children found");
@@ -759,6 +767,10 @@ public final class PPTSLICE1 extends PptSlice {
       invs.add(inv);
     }
 
+    if (debug) {
+      System.out.println("inv_map = " + inv_map);
+    }
+
     // Attempt to create a parent invariant for each invariant that
     // appeared at each valid child.  Note that some invariants will
     // not exist at the parent even if they exist at each child (eg,
@@ -783,19 +795,30 @@ public final class PPTSLICE1 extends PptSlice {
       }
       if (child_invs.size() == valid_child_count) {
         Invariant first = child_invs.get(0);
+        if (debug) {
+          System.out.printf("Attempting merge of %s invariants into ppt %s%n", child_invs.size(), name());
+        }
         if (Debug.logOn()) {
           first.log("Attempting merge of %s invariants into ppt %s", child_invs.size(), name());
         }
         Invariant parent_inv = first.merge(child_invs, this);
         if (parent_inv != null) {
           invs.add(parent_inv);
+          if (debug) {
+            System.out.printf("Merge successful of %s into %s%n", parent_inv.format(), name());
+          }
           if (Debug.logOn()) {
             parent_inv.log("Merge successful of %s into %s", parent_inv.format(), name());
           }
         }
       } else {
         if (Debug.logOn()) {
           Invariant inv = child_invs.get(0);
+          if (debug) {
+            System.out.printf(
+              "Not merging invariant into %s, Found %s child invariants in %s children%n",
+              name(), child_invs.size(), valid_child_count);
+          }
           inv.log(
               "Not merging invariant into %s, Found %s child invariants in %s children",
               name(), child_invs.size(), valid_child_count);

java/daikon/PptTopLevel.java

@@ -3650,8 +3650,14 @@ public void mergeInvs() {
     // Merge the ModBitTracker.
     // We'll reuse one dummy ValueTuple throughout, side-effecting its mods
     // array.
-    if (debugStdout) {
-      System.out.printf("in ppt %s%n", name());
+    boolean debugLocal =
+        debugStdout
+            && name()
+                .startsWith(
+                    "com.rolemodelsoft.drawlet.basics.AbstractFigure.addPropertyChangeListener(java.beans.PropertyChangeListener)");
+
+    if (debugLocal) {
+      System.out.printf("mergeInvs in ppt %s%n", name());
       System.out.printf("  num_tracevars = %d%n", num_tracevars);
       System.out.printf("  mbtracker.num_vars() = %d%n", mbtracker.num_vars());
       for (int ii = 0; ii < var_infos.length; ii++) {
@@ -3667,8 +3673,19 @@ public void mergeInvs() {
     for (PptRelation rel : children) {
       ModBitTracker child_mbtracker = rel.child.mbtracker;
       int child_mbsize = child_mbtracker.num_samples();
-      // System.out.println("mergeInvs child #" + children.indexOf(rel) + "=" + rel.child.name() + "
-      // has size " + child_mbsize + " for " + name());
+      if (debugLocal) {
+        System.out.println(
+            "mergeInvs child #"
+                + children.indexOf(rel)
+                + "/"
+                + children.size()
+                + "="
+                + rel.child.name()
+                + " has size "
+                + child_mbsize
+                + " for "
+                + name());
+      }
       for (int sampno = 0; sampno < child_mbsize; sampno++) {
         Arrays.fill(mods, ValueTuple.MISSING_FLOW);
         for (int j = 0; j < var_infos.length; j++) {
@@ -3858,11 +3875,17 @@ public void mergeInvs() {
   @RequiresNonNull("equality_view")
   public void merge_invs_multiple_children() {
 
+    boolean debugLocal =
+        debugStdout
+            && name()
+                .startsWith(
+                    "com.rolemodelsoft.drawlet.basics.AbstractFigure.addPropertyChangeListener(java.beans.PropertyChangeListener)");
+
     // Debug print ppt and children
-    if (debugStdout) {
+    if (debugLocal) {
       System.out.printf("Merging invariants for ppt %s%n", this);
       for (PptRelation rel : children) {
-        System.out.printf("child: %s%n", rel);
+        System.out.printf("  child: %s%n", rel);
       }
     }
 
@@ -3877,8 +3900,9 @@ public void merge_invs_multiple_children() {
         continue;
       }
       if (constants != null && constants.is_missing(l)) {
-        // System.out.printf("skipping leader %s in ppt %s, always missing%n",
-        //                   l, name());
+        if (debugLocal) {
+          System.out.printf("skipping leader %s in ppt %s, always missing%n", l, name());
+        }
         continue;
       }
       non_missing_leaders.add(l);
@@ -3900,6 +3924,9 @@ public void merge_invs_multiple_children() {
       }
       suppressed_invs.put(child, NIS.create_suppressed_invs(child));
     }
+    if (debugLocal) {
+      System.out.println("suppressed_invs = " + suppressed_invs);
+    }
 
     // Create unary views and related invariants
     List<PptSlice> unary_slices = new ArrayList<>();