001package daikon.inv.filter;
002
003import daikon.PrintInvariants;
004import daikon.VarInfo;
005import daikon.VarInfo.VarFlags;
006import daikon.inv.EqualityComparison;
007import daikon.inv.Invariant;
008import java.util.logging.Level;
009
010/**
011 * Suppress invariants that refer to the prestate value of a field marked with {@link
012 * daikon.VarInfo.VarFlags#IS_READONLY}.
013 */
014public class ReadonlyPrestateFilter extends InvariantFilter {
015  @Override
016  public String getDescription() {
017    return "Suppress invariants indicate that a readonly variable was unmodified";
018  }
019
020  /** Boolean. If true, ReadonlyPrestateFilter is initially turned on. */
021  public static boolean dkconfig_enabled = true;
022
023  public ReadonlyPrestateFilter() {
024    isOn = dkconfig_enabled;
025  }
026
027  @Override
028  boolean shouldDiscardInvariant(Invariant invariant) {
029    if (PrintInvariants.debugFiltering.isLoggable(Level.FINE)) {
030      PrintInvariants.debugFiltering.fine("\tEntering UnmodRPF.shouldDiscard");
031    }
032
033    if (!invariant.isEqualityComparison()) {
034      if (PrintInvariants.debugFiltering.isLoggable(Level.FINE)) {
035        PrintInvariants.debugFiltering.fine("\tUnmodRPF thinks this isn't an equality comparison");
036      }
037      return false;
038    }
039
040    EqualityComparison comp = (EqualityComparison) invariant;
041    VarInfo var1 = comp.var1();
042    VarInfo var2 = comp.var2();
043
044    if (PrintInvariants.debugFiltering.isLoggable(Level.FINE)) {
045      PrintInvariants.debugFiltering.fine(
046          "compared " + var1.prestate_name() + " to " + var2.name());
047    }
048
049    if (var1.is_prestate_version(var2) && var1.var_flags.contains(VarFlags.IS_READONLY)) {
050      return true;
051    } else if (var2.is_prestate_version(var1) && var2.var_flags.contains(VarFlags.IS_READONLY)) {
052      return true;
053    }
054    return false;
055  }
056}