001// ***** This file is automatically generated from SequenceSubscript.java.jpp 002 003package daikon.derive.binary; 004 005import org.checkerframework.checker.interning.qual.Interned; 006import org.checkerframework.checker.lock.qual.GuardSatisfied; 007import org.checkerframework.dataflow.qual.Pure; 008import org.checkerframework.dataflow.qual.SideEffectFree; 009import java.util.logging.Logger; 010import daikon.*; 011import daikon.derive.*; 012import org.plumelib.util.Intern; 013import org.plumelib.util.UtilPlume; 014 015public final class SequenceScalarSubscript extends BinaryDerivation { 016 static final long serialVersionUID = 20020122L; 017 018 // Variables starting with dkconfig_ should only be set via the 019 // daikon.config.Configuration interface. 020 /** Boolean. True iff SequenceScalarSubscript derived variables should be generated. */ 021 public static boolean dkconfig_enabled = true; 022 023 /** General debug tracer. */ 024 public static final Logger debug = Logger.getLogger("daikon.derive.binary.SequenceScalarSubscript"); 025 026 // base1 is the sequence 027 // base2 is the scalar 028 public VarInfo seqvar(@GuardSatisfied SequenceScalarSubscript this) { 029 return base1; 030 } 031 032 public VarInfo sclvar(@GuardSatisfied SequenceScalarSubscript this) { 033 return base2; 034 } 035 036 public VarInfo seq_enclosing_var() { 037 VarInfo result = seqvar().enclosing_var; 038 // When using old dtrace file format, this can fail. 039 assert result != null : "@AssumeAssertion(nullness): foo[] has enclosing_var foo"; 040 return result; 041 } 042 043 // Indicates whether the subscript is an index of valid data or a limit 044 // (one element beyond the data of interest). 045 // Value is -1 or 0. 046 public final int index_shift; 047 048 SequenceScalarSubscript(VarInfo vi1, VarInfo vi2, boolean less1) { 049 super(vi1, vi2); 050 if (less1) { 051 index_shift = -1; 052 } else { 053 index_shift = 0; 054 } 055 debug.fine("SequenceScalarSubscript(" + vi1 + ", " + vi2 + ", " + less1 + ") => " + this); 056 } 057 058 @SideEffectFree 059 @Override 060 public String toString(@GuardSatisfied SequenceScalarSubscript this) { 061 String shift = ""; 062 if (index_shift < 0) { 063 shift = "" + index_shift; 064 } else if (index_shift > 0) { 065 shift = "+" + index_shift; 066 } 067 return seqvar().name().replace("[]", "") + "[" + sclvar().name() + shift + "]"; 068 } 069 070 @Override 071 public ValueAndModified computeValueAndModifiedImpl(ValueTuple full_vt) { 072 int mod1 = base1.getModified(full_vt); 073 if (mod1 == ValueTuple.MISSING_NONSENSICAL) { 074 return ValueAndModified.MISSING_NONSENSICAL; 075 } 076 int mod2 = base2.getModified(full_vt); 077 if (mod2 == ValueTuple.MISSING_NONSENSICAL) { 078 return ValueAndModified.MISSING_NONSENSICAL; 079 } 080 Object val1 = base1.getValue(full_vt); 081 if (val1 == null) { 082 return ValueAndModified.MISSING_NONSENSICAL; 083 } 084 long[] val1_array = (long[]) val1; 085 int val2 = base2.getIndexValue(full_vt) + index_shift; 086 if ((val2 < 0) || (val2 >= val1_array.length)) { 087 // if (!missing_array_bounds) 088 // System.out.println ("out of bounds" + base1.name() + " " 089 // + base2.name() + " @" + base1.ppt.name()); 090 missing_array_bounds = true; 091 return ValueAndModified.MISSING_NONSENSICAL; 092 } 093 long val = val1_array[val2]; 094 int mod = 095 (((mod1 == ValueTuple.UNMODIFIED) && (mod2 == ValueTuple.UNMODIFIED)) 096 ? ValueTuple.UNMODIFIED 097 : ValueTuple.MODIFIED); 098 return new ValueAndModified(Intern.internedLong(val), mod); 099 } 100 101 @Override 102 protected VarInfo makeVarInfo() { 103 return VarInfo.make_subscript(seqvar(), sclvar(), index_shift); 104 } 105 106 @Pure 107 @Override 108 public boolean isSameFormula(Derivation other) { 109 return (other instanceof SequenceScalarSubscript) 110 && (((SequenceScalarSubscript) other).index_shift == this.index_shift); 111 } 112 113 @SuppressWarnings("nullness") 114 @SideEffectFree 115 @Override 116 public String esc_name(String index) { 117 if (seqvar().isPrestate()) { 118 return String.format( 119 "\\old(%s[%s])", 120 seqvar().enclosing_var.postState.esc_name(), 121 inside_esc_name(sclvar(), true, index_shift)); 122 } else { 123 return String.format( 124 "%s[%s%s]", 125 seqvar().enclosing_var.esc_name(), sclvar().esc_name(), shift_str(index_shift)); 126 } 127 } 128 129 @SuppressWarnings("nullness") 130 @Override 131 public String jml_name(String index) { 132 String get_element = "daikon.Quant.getElement_int"; 133 if (seqvar().file_rep_type.baseIsHashcode()) { 134 get_element = "daikon.Quant.getElement_Object"; 135 } else if (seqvar().file_rep_type.baseIsBoolean()) { 136 get_element = "daikon.Quant.getElement_boolean"; 137 } 138 if (seqvar().isPrestate()) { 139 return String.format( 140 "\\old(%s(%s, %s))", 141 get_element, 142 seqvar().enclosing_var.postState.jml_name(), 143 inside_jml_name(sclvar(), true, index_shift)); 144 } else { 145 return String.format( 146 "%s(%s, %s%s)", 147 get_element, 148 seqvar().enclosing_var.jml_name(), 149 sclvar().jml_name(), 150 shift_str(index_shift)); 151 } 152 } 153 154 @SuppressWarnings("nullness") 155 @SideEffectFree 156 @Override 157 public String csharp_name(String index) { 158 String[] split = seqvar().csharp_array_split(); 159 if (seqvar().isPrestate()) { 160 return String.format( 161 "Contract.OldValue(%s[%s]%s)", 162 seqvar().enclosing_var.postState.csharp_name(), 163 inside_csharp_name(sclvar(), true, index_shift), 164 split[1]); 165 } else { 166 return String.format( 167 "%s[%s%s]%s", split[0], sclvar().csharp_name(), shift_str(index_shift), split[1]); 168 } 169 } 170 171 @SuppressWarnings("nullness") 172 @SideEffectFree 173 @Override 174 public String simplify_name() { 175 String subscript = sclvar().simplify_name(); 176 if (index_shift < 0) { 177 subscript = String.format("(- %s %d)", subscript, -index_shift); 178 } else if (index_shift > 0) { 179 subscript = String.format("(+ %s %d)", subscript, index_shift); 180 } 181 182 return String.format( 183 "(select (select elems %s) %s)", seqvar().enclosing_var.simplify_name(), subscript); 184 } 185 186 /** Adds one to the default complexity if index_shift is not 0. */ 187 @Override 188 public int complexity() { 189 return super.complexity() + ((index_shift != 0) ? 1 : 0); 190 } 191}