001package daikon.derive.binary; 002 003import daikon.Quantify; 004import daikon.VarInfo; 005import org.checkerframework.checker.lock.qual.GuardSatisfied; 006import org.checkerframework.dataflow.qual.SideEffectFree; 007 008/** Derivations of the form A[0..i] or A[i..<em>end</em>], derived from A and i. */ 009public abstract class SequenceSubsequence extends BinaryDerivation { 010 static final long serialVersionUID = 20020801L; 011 012 // Variables starting with dkconfig_ should only be set via the 013 // daikon.config.Configuration interface. 014 015 // base1 is the sequence 016 // base2 is the scalar 017 public VarInfo seqvar(@GuardSatisfied SequenceSubsequence this) { 018 return base1; 019 } 020 021 public VarInfo sclvar(@GuardSatisfied SequenceSubsequence this) { 022 return base2; 023 } 024 025 // Indicates whether the subscript is an index of valid data or a limit 026 // (one element beyond the data of interest). The first (or last) 027 // element of the derived variable is at index seqvar()+index_shift. 028 public final int index_shift; 029 030 // True for deriving from the start of the sequence to the scalar: B[0..I] 031 // False for deriving from the scalar to the end of the sequence: B[I..] 032 public final boolean from_start; 033 034 /** 035 * @param from_start true means the range goes 0..n; false means the range goes n..end. (n might 036 * be fudged through off_by_one.) 037 * @param off_by_one true means we should exclude the scalar from the range; false means we should 038 * include it 039 */ 040 protected SequenceSubsequence(VarInfo vi1, VarInfo vi2, boolean from_start, boolean off_by_one) { 041 super(vi1, vi2); 042 this.from_start = from_start; 043 if (off_by_one) { 044 index_shift = from_start ? -1 : +1; 045 } else { 046 index_shift = 0; 047 } 048 } 049 050 @Override 051 protected VarInfo makeVarInfo() { 052 VarInfo seqvar = seqvar(); 053 VarInfo sclvar = sclvar(); 054 055 VarInfo vi; 056 if (from_start) { 057 vi = VarInfo.make_subsequence(seqvar, null, 0, sclvar, index_shift); 058 } else { 059 vi = VarInfo.make_subsequence(seqvar, sclvar, index_shift, null, 0); 060 } 061 062 return vi; 063 } 064 065 @Override 066 public Quantify.Term get_lower_bound() { 067 if (from_start) { 068 return new Quantify.Constant(0); 069 } else { 070 return new Quantify.VarPlusOffset(sclvar(), index_shift); 071 } 072 } 073 074 @Override 075 public Quantify.Term get_upper_bound() { 076 if (from_start) { 077 return new Quantify.VarPlusOffset(sclvar(), index_shift); 078 } else { 079 return new Quantify.Length(seqvar(), -1); 080 } 081 } 082 083 @Override 084 public VarInfo get_array_var() { 085 return seqvar(); 086 } 087 088 @SideEffectFree 089 @Override 090 public String csharp_name(String index) { 091 // String lower = get_lower_bound().csharp_name(); 092 // String upper = get_upper_bound().csharp_name(); 093 // We do not need to check if seqvar().isPrestate() because it is redundant. 094 // return seqvar().csharp_name() + ".Slice(" + lower + ", " + upper + ")"; 095 return "\"SequenceSubsequence.java.jpp unimplemented\" != null"; // "interned" 096 } 097 098 @SideEffectFree 099 @Override 100 public String esc_name(String index) { 101 return String.format( 102 "%s[%s..%s]", 103 seqvar().esc_name(), get_lower_bound().esc_name(), get_upper_bound().esc_name()); 104 } 105 106 @Override 107 @SuppressWarnings("nullness") 108 public String jml_name(String index) { 109 110 // The slice routine needs the actual length as opposed to the 111 // highest legal index. 112 Quantify.Term upper = get_upper_bound(); 113 if (upper instanceof Quantify.Length) { 114 ((Quantify.Length) upper).set_offset(0); 115 } 116 117 if (seqvar().isPrestate()) { 118 return String.format( 119 "\\old(daikon.Quant.slice(%s, %s, %s))", 120 seqvar().enclosing_var.postState.jml_name(), 121 get_lower_bound().jml_name(true), 122 upper.jml_name(true)); 123 } else { 124 return String.format( 125 "daikon.Quant.slice(%s, %s, %s)", 126 seqvar().enclosing_var.jml_name(), get_lower_bound().jml_name(), upper.jml_name()); 127 } 128 } 129 130 /** Adds one to the default complexity if index_shift is not 0. */ 131 @Override 132 public int complexity() { 133 return super.complexity() + ((index_shift != 0) ? 1 : 0); 134 } 135}