001package daikon.tools;
002
003import daikon.VarInfo;
004import daikon.inv.Invariant;
005import gnu.getopt.*;
006import java.util.ArrayList;
007import java.util.LinkedHashMap;
008import java.util.List;
009import java.util.Map;
010import org.checkerframework.checker.initialization.qual.UnknownInitialization;
011import org.checkerframework.checker.lock.qual.GuardSatisfied;
012import org.checkerframework.dataflow.qual.SideEffectFree;
013
014/**
015 * Provides a variable translation over an invariant at one program point (perhaps in a different
016 * program) to a similar invariant at a second program point. In general, on order for a translation
017 * to be possible, the invariants must be of the same class. For example, consider the invariants
018 * (x>y) at ppt1 and (p>q) at ppt2. Since the invariants are the same, the translation is (x
019 * → p) and (y → q).
020 *
021 * <p>The quality of the translation is also determined (approximately on a scale of 0 to 100). If
022 * the invariants are not of the same class, no translation is possible and the quality is zero. If
023 * the class and the formula are the same, the match is excellent (80). If the class is the same and
024 * the formula is different, the match is mediocre (40). The quality is increased for variables with
025 * exactly the same derivation and decreased for those with different derivations.
026 *
027 * <p>Other checks could be added to further specify the quality. For example, if one invariant is a
028 * precondition and the other is a postcondition, the quality should be reduced.
029 */
030public class InvTranslate {
031
032  /**
033   * The quality of the mapping. 0 indicates no mapping is possible. 100 indicates that there is a
034   * perfect translation.
035   */
036  int quality = 0;
037
038  /** Map of variables from inv to inv. */
039  Map<String, String> var_map = new LinkedHashMap<>();
040
041  /** source invariant */
042  Invariant inv1;
043
044  /** destination invariant */
045  Invariant inv2;
046
047  // /** an empty translation */
048  // private InvTranslate () {
049  //   inv1 = null;
050  //   inv2 = null;
051  //   quality = 0;
052  // }
053
054  /**
055   * Setup a translation from i1 to i2. The quality and the variable map is set accordingly.
056   *
057   * @param i1 the invariant to translate from
058   * @param i2 the invariant to translate to
059   */
060  public InvTranslate(Invariant i1, Invariant i2) {
061
062    inv1 = i1;
063    inv2 = i2;
064
065    // For now if the classes don't match, there is no translation
066    if (i1.getClass() != i2.getClass()) {
067      quality = 0;
068      return;
069    }
070
071    if (i1.isSameFormula(i2)) {
072      quality = 80;
073    } else {
074      quality = 40;
075    }
076
077    // Create the simple mapping and adjust for the quality of the variable
078    // mapping (variables of the same derivation are better than those of
079    // different derivations).
080    for (int i = 0; i < i1.ppt.var_infos.length; i++) {
081      VarInfo v1 = i1.ppt.var_infos[i];
082      VarInfo v2 = i2.ppt.var_infos[i];
083      add_variable_map(v1.name(), v2.name());
084      if ((v1.derived == null) && (v2.derived == null)) {
085        quality += 5;
086      } else if ((v1.derived != null)
087          && (v2.derived != null)
088          && (v1.derived.getClass() == v2.derived.getClass())) {
089        quality += 5;
090      } else {
091        /* variables have different derivations */ quality -= 5;
092      }
093    }
094  }
095
096  // private static InvTranslate no_translate = new InvTranslate();
097  // static InvTranslate no_translate() {
098  //   return no_translate;
099  // }
100
101  /** Add the specified variable names to the variable translation. */
102  private void add_variable_map(
103      @UnknownInitialization(daikon.tools.InvTranslate.class) InvTranslate this,
104      String v1_name,
105      String v2_name) {
106
107    assert !var_map.containsKey(v1_name);
108
109    var_map.put(v1_name, v2_name);
110  }
111
112  /** Returns a somewhat verbose description of the translation. */
113  @SideEffectFree
114  @Override
115  public String toString(@GuardSatisfied InvTranslate this) {
116    StringBuilder out = new StringBuilder();
117
118    List<String> mappings = new ArrayList<>();
119    for (String key : var_map.keySet()) {
120      String value = var_map.get(key);
121      mappings.add(key + "->" + value);
122    }
123    out.append(String.join(", ", mappings));
124
125    out.append(" [Quality=" + quality + "]");
126    if ((inv1 != null) && (inv2 != null)) {
127      out.append(" [" + inv1.format() + " -> " + inv2.format() + "]");
128    }
129
130    return out.toString();
131  }
132}