Add AGORA invariants

java/daikon/Daikon.java

@@ -149,12 +149,10 @@
 import daikon.inv.unary.sequence.SeqIndexIntLessEqual;
 import daikon.inv.unary.sequence.SeqIndexIntLessThan;
 import daikon.inv.unary.sequence.SeqIndexIntNonEqual;
-import daikon.inv.unary.string.CompleteOneOfString;
-import daikon.inv.unary.string.OneOfString;
-import daikon.inv.unary.string.PrintableString;
-import daikon.inv.unary.stringsequence.CommonStringSequence;
-import daikon.inv.unary.stringsequence.EltOneOfString;
-import daikon.inv.unary.stringsequence.OneOfStringSequence;
+import daikon.inv.unary.string.*;
+import daikon.inv.unary.string.dates.*;
+import daikon.inv.unary.stringsequence.*;
+import daikon.inv.unary.stringsequence.dates.*;
 import daikon.simplify.LemmaStack;
 import daikon.split.ContextSplitterFactory;
 import daikon.split.PptSplitter;
@@ -1538,6 +1536,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(IsHour.get_proto());
+      proto_invs.add(IsHourWithSeconds.get_proto());
+      proto_invs.add(IsHourAMPM.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());
@@ -1603,6 +1614,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(SequenceStringElementsAreHour.get_proto());
+      proto_invs.add(SequenceStringElementsAreHourWithSeconds.get_proto());
+      proto_invs.add(SequenceStringElementsAreHourAMPM.get_proto());
+      proto_invs.add(SequenceStringElementsAreTimestampYYYYMMHHThhmmssmm.get_proto());
     }
 
     // Binary scalar-scalar invariants

java/daikon/inv/binary/Member.java.jpp

@@ -378,7 +378,10 @@ public final class CLASSNAME extends SEQUENCESCALAR {
 
   @Override
   protected double computeConfidence() {
-    return Invariant.CONFIDENCE_JUSTIFIED;
+      if (ppt.num_samples() == 0) {
+        return CONFIDENCE_UNJUSTIFIED;
+      }
+  return CONFIDENCE_JUSTIFIED;
   }
 
   @Pure

java/daikon/inv/binary/twoSequence/Reverse.java.jpp

@@ -227,7 +227,10 @@ public class CLASSNAME extends SUPERCLASS {
 
   @Override
   protected double computeConfidence() {
-    return Invariant.CONFIDENCE_JUSTIFIED;
+      if (ppt.num_samples() == 0) {
+        return CONFIDENCE_UNJUSTIFIED;
+      }
+  return CONFIDENCE_JUSTIFIED;
   }
 
   @Pure

java/daikon/inv/binary/twoSequence/SubSequence.java.jpp

@@ -313,7 +313,10 @@ public class CLASSNAME extends SUPERCLASS {
 
   @Override
   protected double computeConfidence() {
-    return Invariant.CONFIDENCE_JUSTIFIED;
+      if (ppt.num_samples() == 0) {
+        return CONFIDENCE_UNJUSTIFIED;
+      }
+  return CONFIDENCE_JUSTIFIED;
   }
 
   /** Returns a DiscardInfo, or null if the Invariant is not an obvious subsequence.

java/daikon/inv/binary/twoSequence/SubSet.java.jpp

@@ -309,7 +309,10 @@ public class SUBSET extends TWOSEQUENCE {
 
   @Override
   protected double computeConfidence() {
-    return Invariant.CONFIDENCE_JUSTIFIED;
+      if (ppt.num_samples() == 0) {
+        return CONFIDENCE_UNJUSTIFIED;
+      }
+  return CONFIDENCE_JUSTIFIED;
   }
 
   // Convenience name to make this easier to find.

java/daikon/inv/unary/scalar/Range.java.jpp

@@ -192,7 +192,10 @@ public abstract class RANGE extends SUPERCLASS {
 
   @Override
   protected double computeConfidence() {
-    return CONFIDENCE_JUSTIFIED;
+      if (ppt.num_samples() == 0) {
+        return CONFIDENCE_UNJUSTIFIED;
+      }
+  return CONFIDENCE_JUSTIFIED;
   }
 
   @Pure

java/daikon/inv/unary/string/FixedLengthString.java

@@ -0,0 +1,138 @@
+package daikon.inv.unary.string;
+
+import daikon.PptSlice;
+import daikon.inv.Invariant;
+import daikon.inv.InvariantStatus;
+import daikon.inv.OutputFormat;
+import daikon.inv.unary.string.dates.IsDateDDMMYYYY;
+import daikon.inv.unary.string.dates.IsDateMMDDYYYY;
+import daikon.inv.unary.string.dates.IsDateYYYYMMDD;
+import daikon.suppress.NISuppressee;
+import daikon.suppress.NISuppression;
+import daikon.suppress.NISuppressionSet;
+import daikon.suppress.NISuppressor;
+import org.checkerframework.checker.interning.qual.Interned;
+import org.checkerframework.checker.lock.qual.GuardSatisfied;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.dataflow.qual.Pure;
+import org.checkerframework.dataflow.qual.SideEffectFree;
+import org.checkerframework.framework.qual.Unused;
+import typequals.prototype.qual.Prototype;
+
+/**
+ * Indicates that the value of a string variable always has a fixed length n. Prints as {@code
+ * LENGTH(x)==n}.
+ */
+public class FixedLengthString extends SingleString {
+
+  // We are Serializable, so we specify a version to allow changes to
+  // method signatures without breaking serialization.  If you add or
+  // remove fields, you should change this number to the current date.
+  static final long serialVersionUID = 20230704L;
+
+  // Variables starting with dkconfig_ should only be set via the
+  // daikon.config.Configuration interface.
+  /** Boolean. True iff Positive invariants should be considered. */
+  public static boolean dkconfig_enabled = false;
+
+  @Unused(when = Prototype.class)
+  private @Nullable Integer length = null;
+
+  ///
+  /// Required methods
+  ///
+  private FixedLengthString(PptSlice ppt) {
+    super(ppt);
+  }
+
+  private @Prototype FixedLengthString() {
+    super();
+  }
+
+  private static @Prototype FixedLengthString proto = new @Prototype FixedLengthString();
+
+  // Returns the prototype invariant
+  public static @Prototype FixedLengthString get_proto() {
+    return proto;
+  }
+
+  @Override
+  public boolean enabled() {
+    return dkconfig_enabled;
+  }
+
+  @Override
+  public FixedLengthString instantiate_dyn(@Prototype FixedLengthString this, PptSlice slice) {
+    return new FixedLengthString(slice);
+  }
+
+  @SideEffectFree
+  @Override
+  public String format_using(@GuardSatisfied FixedLengthString this, OutputFormat format) {
+    return "LENGTH(" + var().name() + ")==" + length;
+  }
+
+  @Override
+  public InvariantStatus add_modified(@Interned String a, int count) {
+    return check_modified(a, count);
+  }
+
+  @Override
+  public InvariantStatus check_modified(@Interned String v, int count) {
+    // Initialize the length the first time
+    if (length == null) {
+      length = v.length();
+    }
+
+    if (v.length() == length) {
+      return InvariantStatus.NO_CHANGE;
+    }
+    return InvariantStatus.FALSIFIED;
+  }
+
+  @Override
+  protected double computeConfidence() {
+    return 1 - Math.pow(.1, ppt.num_samples());
+  }
+
+  @Pure
+  @Override
+  public boolean isSameFormula(Invariant other) {
+    // Check type and length value
+    assert other instanceof FixedLengthString;
+
+    FixedLengthString o = (FixedLengthString) other;
+    if (!o.length.equals(length)) {
+      return false;
+    }
+
+    return true;
+  }
+
+  /** NI suppressions, initialized in get_ni_suppressions() */
+  private static @Nullable NISuppressionSet suppressions = null;
+
+  /** returns the ni-suppressions for SeqIndexFloatGreaterEqual */
+  @Pure
+  @Override
+  public NISuppressionSet get_ni_suppressions() {
+    if (suppressions == null) {
+
+      NISuppressee suppressee = new NISuppressee(FixedLengthString.class, 1);
+
+      // suppressor definitions (used in suppressions below)
+      NISuppressor isDateMMDDYYYY = new NISuppressor(0, IsDateMMDDYYYY.class);
+      NISuppressor isDateDDMMYYYY = new NISuppressor(0, IsDateDDMMYYYY.class);
+      NISuppressor isDateYYYYMMDD = new NISuppressor(0, IsDateYYYYMMDD.class);
+
+      suppressions =
+          new NISuppressionSet(
+              new NISuppression[] {
+                new NISuppression(isDateMMDDYYYY, suppressee),
+                new NISuppression(isDateDDMMYYYY, suppressee),
+                new NISuppression(isDateYYYYMMDD, suppressee),
+              });
+    }
+    return suppressions;
+  }
+}

java/daikon/inv/unary/string/IsEmail.java

@@ -0,0 +1,95 @@
+package daikon.inv.unary.string;
+
+import daikon.PptSlice;
+import daikon.inv.Invariant;
+import daikon.inv.InvariantStatus;
+import daikon.inv.OutputFormat;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+import org.checkerframework.checker.lock.qual.GuardSatisfied;
+import org.checkerframework.dataflow.qual.Pure;
+import org.checkerframework.dataflow.qual.SideEffectFree;
+import typequals.prototype.qual.Prototype;
+
+/**
+ * Indicates that the value of a string type variable is always an email. Represented as {@code x is
+ * Email}.
+ */
+public class IsEmail extends SingleString {
+  // We are Serializable, so we specify a version to allow changes to
+  // method signatures without breaking serialization.  If you add or
+  // remove fields, you should change this number to the current date.
+  static final long serialVersionUID = 20230704L;
+
+  // Variables starting with dkconfig_ should only be set via the
+  // daikon.config.Configuration interface.
+  /** Boolean. True iff Positive invariants should be considered. */
+  public static boolean dkconfig_enabled = false;
+
+  ///
+  /// Required methods
+  ///
+  private IsEmail(PptSlice ppt) {
+    super(ppt);
+  }
+
+  private @Prototype IsEmail() {
+    super();
+  }
+
+  private static @Prototype IsEmail proto = new @Prototype IsEmail();
+
+  // Returns the prototype invariant
+  public static @Prototype IsEmail get_proto() {
+    return proto;
+  }
+
+  @Override
+  public boolean enabled() {
+    return dkconfig_enabled;
+  }
+
+  @Override
+  public IsEmail instantiate_dyn(@Prototype IsEmail this, PptSlice slice) {
+    return new IsEmail(slice);
+  }
+
+  // A printed representation for user output
+  @SideEffectFree
+  @Override
+  public String format_using(@GuardSatisfied IsEmail this, OutputFormat format) {
+    return var().name() + " is Email";
+  }
+
+  @Override
+  public InvariantStatus check_modified(String v, int count) {
+
+    Pattern pattern =
+        Pattern.compile(
+            "^(?:[a-z0-9!#$%&'*+/=?^_`{|}~-]+(?:\\.[a-z0-9!#$%&'*+/=?^_`{|}~-]+)*|\"(?:[\\x01-\\x08\\x0b\\x0c\\x0e-\\x1f\\x21\\x23-\\x5b\\x5d-\\x7f]|\\\\[\\x01-\\x09\\x0b\\x0c\\x0e-\\x7f])*\")@(?:(?:[a-z0-9](?:[a-z0-9-]*[a-z0-9])?\\.)+[a-z0-9](?:[a-z0-9-]*[a-z0-9])?|\\[(?:(?:25[0-5]|2[0-4][0-9]|[01]?[0-9][0-9]?)\\.){3}(?:25[0-5]|2[0-4][0-9]|[01]?[0-9]^[0-9]?|[a-z0-9-]*[a-z0-9]:(?:[\\x01-\\x08\\x0b\\x0c\\x0e-\\x1f\\x21-\\x5a\\x53-\\x7f]|\\\\[\\x01-\\x09\\x0b\\x0c\\x0e-\\x7f])+)\\])$");
+
+    Matcher matcher = pattern.matcher(v);
+
+    if (matcher.matches()) {
+      return InvariantStatus.NO_CHANGE;
+    }
+    return InvariantStatus.FALSIFIED;
+  }
+
+  @Override
+  public InvariantStatus add_modified(String v, int count) {
+    return check_modified(v, count);
+  }
+
+  @Override
+  protected double computeConfidence() {
+    return 1 - Math.pow(.1, ppt.num_samples());
+  }
+
+  @Pure
+  @Override
+  public boolean isSameFormula(Invariant other) {
+    assert other instanceof IsEmail;
+    return true;
+  }
+}