Source code

001package daikon.tools;
002
003import daikon.Daikon;
004import daikon.FileIO;
005import daikon.Global;
006import daikon.PptMap;
007import daikon.PptSlice;
008import daikon.PptSliceEquality;
009import daikon.PptTopLevel;
010import daikon.VarInfo;
011import daikon.inv.Invariant;
012import daikon.inv.binary.twoScalar.IntGreaterThan;
013import daikon.inv.binary.twoScalar.IntLessThan;
014import daikon.inv.unary.scalar.OneOfScalar;
015import gnu.getopt.*;
016import java.io.File;
017import java.io.IOException;
018import java.util.ArrayList;
019import java.util.HashSet;
020import java.util.Iterator;
021import java.util.LinkedHashMap;
022import java.util.List;
023import java.util.Map;
024import java.util.Set;
025import org.checkerframework.checker.nullness.qual.NonNull;
026import org.checkerframework.checker.nullness.qual.Nullable;
027import org.checkerframework.dataflow.qual.Pure;
028
029/**
030 * Functions that look for relationships between the invariants at different program points.
031 * Relationships between individual invariants are created with InvTranslate. Currently, only
032 * invariants of the same class can be related to one another.
033 */
034public class InvMatch {
035
036  /**
037   * Main program for testing purposes.
038   *
039   * @param args command-line arguments, ignored
040   */
041  @SuppressWarnings("nullness") // testing method, not worth type-checking
042  public static void main(String[] args) throws IOException {
043
044    // Read in the sample decls file
045    Set<File> decl_files = new HashSet<>(1);
046    decl_files.add(new File("daikon/test/SampleTester.decls"));
047    PptMap all_ppts = FileIO.read_declaration_files(decl_files);
048
049    // Setup everything to run
050    PptSliceEquality.dkconfig_set_per_var = true;
051    Daikon.setup_NISuppression();
052
053    // Get the exit ppts
054    PptTopLevel ppt35 = all_ppts.get("foo.f():::EXIT35");
055    PptTopLevel ppt40 = all_ppts.get("foo.g():::EXIT40");
056
057    // Get variables at both program points
058    VarInfo ppt35_x = ppt35.var_infos[0];
059    VarInfo ppt35_y = ppt35.var_infos[1];
060    VarInfo ppt35_z = ppt35.var_infos[2];
061    VarInfo ppt40_p = ppt40.var_infos[0];
062    VarInfo ppt40_q = ppt40.var_infos[1];
063    VarInfo ppt40_r = ppt40.var_infos[2];
064
065    // Build EXIT35 slices
066    PptSlice slice_xy_35 = ppt35.get_or_instantiate_slice(new VarInfo[] {ppt35_x, ppt35_y});
067    PptSlice slice_yz_35 = ppt35.get_or_instantiate_slice(new VarInfo[] {ppt35_y, ppt35_z});
068    PptSlice slice_x_35 = ppt35.get_or_instantiate_slice(new VarInfo[] {ppt35_x});
069
070    // Build EXIT40 slices
071    PptSlice slice_pq_40 = ppt40.get_or_instantiate_slice(new VarInfo[] {ppt40_p, ppt40_q});
072    PptSlice slice_qr_40 = ppt40.get_or_instantiate_slice(new VarInfo[] {ppt40_q, ppt40_r});
073    PptSlice slice_pr_40 = ppt40.get_or_instantiate_slice(new VarInfo[] {ppt40_p, ppt40_r});
074    PptSlice slice_p_40 = ppt40.get_or_instantiate_slice(new VarInfo[] {ppt40_p});
075
076    // Create invariants at EXIT35
077    Invariant inv_x_lt_y = IntLessThan.get_proto().instantiate(slice_xy_35);
078    slice_xy_35.addInvariant(inv_x_lt_y);
079    OneOfScalar inv_x_eq_5 = (OneOfScalar) OneOfScalar.get_proto().instantiate(slice_x_35);
080    inv_x_eq_5.add_modified(5, 1);
081    slice_x_35.addInvariant(inv_x_eq_5);
082    Invariant inv_y_gt_z = IntGreaterThan.get_proto().instantiate(slice_yz_35);
083    slice_yz_35.addInvariant(inv_y_gt_z);
084
085    // Create invariants at EXIT40
086    Invariant inv_p_lt_q = IntLessThan.get_proto().instantiate(slice_pq_40);
087    slice_pq_40.addInvariant(inv_p_lt_q);
088    OneOfScalar inv_p_eq_3 = (OneOfScalar) OneOfScalar.get_proto().instantiate(slice_p_40);
089    inv_p_eq_3.add_modified(3, 1);
090    slice_p_40.addInvariant(inv_p_eq_3);
091    Invariant inv_q_gt_r = IntGreaterThan.get_proto().instantiate(slice_qr_40);
092    slice_qr_40.addInvariant(inv_q_gt_r);
093    Invariant inv_p_gt_r = IntGreaterThan.get_proto().instantiate(slice_pr_40);
094    slice_pr_40.addInvariant(inv_p_gt_r);
095
096    // InvTranslate xlate = new InvTranslate(inv_x_lt_y, inv_p_lt_q);
097
098    // Try to matchup the program points
099    List<List<InvTranslate>> valid_translations = match_ppt(ppt35, ppt40);
100
101    // Dump all of the valid translations
102    System.out.println("Valid Translations:");
103    for (List<InvTranslate> current_translation : valid_translations) {
104      System.out.println("  Translation: ");
105      for (InvTranslate xlate : current_translation) {
106        System.out.printf("    %s%n", xlate);
107      }
108    }
109
110    List<InvTranslate> best_translation = best_translation(valid_translations);
111    System.out.println(Global.lineSep + "Best Translation");
112    for (InvTranslate xlate : best_translation) {
113      System.out.printf("  %s%n", xlate);
114    }
115  }
116
117  /**
118   * Compares the invariants between the two program points specified and returns a list of possible
119   * translations. A possible translation is a consistent set of translations (one for each
120   * invariant in ppt1) A set of translations is consistent if all of the variable mappings are
121   * consistent (i.e., no variable maps to more than one variable).
122   */
123  static List<List<InvTranslate>> match_ppt(PptTopLevel ppt1, PptTopLevel ppt2) {
124
125    List<List<InvTranslate>> xlate_list = new ArrayList<>();
126
127    for (Iterator<Invariant> i = ppt1.invariants_iterator(); i.hasNext(); ) {
128      Invariant inv1 = i.next();
129      List<InvTranslate> inv_xlate_list = new ArrayList<>();
130      xlate_list.add(inv_xlate_list);
131      for (Iterator<Invariant> j = ppt2.invariants_iterator(); j.hasNext(); ) {
132        Invariant inv2 = j.next();
133        InvTranslate xlate = new InvTranslate(inv1, inv2);
134        if (xlate.quality > 0) {
135          inv_xlate_list.add(xlate);
136        }
137      }
138      // What is the purpose of this?  Maybe it separates the translation
139      // results for different invariants.  How/where is it used/checked?
140      // I see places where a null is just skipped over, but not where it
141      // has an effect.
142      @SuppressWarnings(
143          "nullness") // can't figure out what this is for; maybe change the declaration
144      @NonNull InvTranslate dummy = null;
145      inv_xlate_list.add(dummy);
146    }
147
148    // Debug print all of the translations
149    if (true) {
150      Iterator<Invariant> invi = ppt1.invariants_iterator();
151      for (List<InvTranslate> inv_xlate_list : xlate_list) {
152        Invariant inv = invi.next();
153        System.out.printf("%s translations:%n", inv.format());
154        for (InvTranslate xlate : inv_xlate_list) {
155          System.out.printf("  %s%n", xlate);
156        }
157      }
158    }
159
160    List<List<InvTranslate>> valid_translations = new ArrayList<>();
161    List<InvTranslate> current_translation = new ArrayList<>();
162    consider_xlate(valid_translations, current_translation, xlate_list, 0);
163
164    return valid_translations;
165  }
166
167  /**
168   * Recursive routine that tries all possible combination of translations.
169   *
170   * @param valid_translations list of valid translations (updated)
171   * @param current_translation the current translation that is being built
172   * @param xlate_list the list of possible translations for each invariant
173   * @param index the current index in xlate_list
174   */
175  public static void consider_xlate(
176      List<List<InvTranslate>> valid_translations,
177      List<InvTranslate> current_translation,
178      List<List<InvTranslate>> xlate_list,
179      int index) {
180
181    List<InvTranslate> inv_xlate_list = xlate_list.get(index);
182    for (InvTranslate xlate : inv_xlate_list) {
183
184      List<InvTranslate> new_translation = new ArrayList<>();
185      new_translation.addAll(current_translation);
186      new_translation.add(xlate);
187      if (!is_good_translation(new_translation)) {
188        continue;
189      }
190
191      if ((index + 1) == xlate_list.size()) {
192        valid_translations.add(new_translation);
193      } else {
194        consider_xlate(valid_translations, new_translation, xlate_list, index + 1);
195      }
196    }
197  }
198
199  @Pure
200  public static boolean is_good_translation(List<InvTranslate> translation_list) {
201
202    Map<String, String> var_map = new LinkedHashMap<>();
203
204    for (InvTranslate xlate : translation_list) {
205      if (xlate == null) {
206        continue;
207      }
208      for (String key : xlate.var_map.keySet()) {
209        String val = xlate.var_map.get(key);
210        String cur_val = var_map.get(key);
211        if (cur_val == null) {
212          var_map.put(key, val);
213        } else if (!cur_val.equals(val)) {
214          return false;
215        }
216      }
217    }
218    return true;
219  }
220
221  public static @Nullable List<InvTranslate> best_translation(
222      List<List<InvTranslate>> valid_translations) {
223
224    // Determine the best translation and print it out.
225    List<InvTranslate> best_translation = null;
226    int best_quality = 0;
227    for (List<InvTranslate> current_translation : valid_translations) {
228      int quality = 0;
229      for (InvTranslate xlate : current_translation) {
230        if (xlate != null) {
231          quality += xlate.quality;
232        }
233      }
234      if (quality > best_quality) {
235        best_translation = current_translation;
236        best_quality = quality;
237      }
238    }
239    return best_translation;
240  }
241}