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}