Source code

001package daikon;
002
003import java.util.ArrayList;
004import java.util.EnumSet;
005import java.util.HashSet;
006import java.util.List;
007import java.util.Set;
008import java.util.StringJoiner;
009import org.checkerframework.checker.lock.qual.GuardSatisfied;
010import org.checkerframework.checker.nullness.qual.NonNull;
011import org.checkerframework.checker.nullness.qual.Nullable;
012import org.checkerframework.dataflow.qual.SideEffectFree;
013
014/** Helper classes for quantification for various output formats. */
015@SuppressWarnings("UnusedVariable") // messy code, need to investigate later
016public class Quantify {
017
018  /** Flags describing how quantifications are to be built. */
019  public enum QuantFlags {
020    /** two indices where they refer to corresponding positions. */
021    ELEMENT_WISE,
022    /** two indices where the second is one more than the first. */
023    ADJACENT,
024    /** two indices are different. */
025    DISTINCT,
026    /** Return the names of the index variables. */
027    INCLUDE_INDEX;
028
029    /** set with just ELEMENT_WISE turned on. */
030    public static EnumSet<QuantFlags> element_wise() {
031      return EnumSet.of(QuantFlags.ELEMENT_WISE);
032    }
033
034    /** set with just ADJACENT turned on. */
035    public static EnumSet<QuantFlags> adjacent() {
036      return EnumSet.of(QuantFlags.ADJACENT);
037    }
038
039    /** set with just DISTINCT turned on. */
040    public static EnumSet<QuantFlags> distinct() {
041      return EnumSet.of(QuantFlags.DISTINCT);
042    }
043
044    /** set with just INCLUDE_INDEX turned on. */
045    public static EnumSet<QuantFlags> include_index() {
046      return EnumSet.of(QuantFlags.INCLUDE_INDEX);
047    }
048  }
049
050  /** Returns a set with ELEMENT_WISE turned on if specified. */
051  public static EnumSet<QuantFlags> get_flags(boolean elementwise) {
052    if (elementwise) {
053      return EnumSet.of(QuantFlags.ELEMENT_WISE);
054    } else {
055      return EnumSet.noneOf(QuantFlags.class);
056    }
057  }
058
059  /**
060   * Class the represents terms that can be used in variable expressions. These include constants
061   * (such as 0 and 1), free variables used for quantification (i, j, etc), and normal Daikon
062   * variables.
063   */
064  public abstract static class Term {
065    @SideEffectFree
066    public abstract String name(@GuardSatisfied Term this);
067
068    @SideEffectFree
069    public String esc_name() {
070      return name();
071    }
072
073    @SideEffectFree
074    public String jml_name() {
075      return esc_name();
076    }
077
078    @SideEffectFree
079    public String jml_name(boolean in_prestate) {
080      return jml_name();
081    }
082
083    @SideEffectFree
084    public String simplify_name() {
085      return name();
086    }
087
088    @SideEffectFree
089    public String csharp_name() {
090      return name();
091    }
092
093    @SideEffectFree
094    protected static String name_with_offset(String name, int offset) {
095      if (offset == 0) {
096        return name;
097      } else {
098        return String.format("%s%+d", name, offset);
099      }
100    }
101  }
102
103  /** Free variable normally used for quantification. */
104  public static class FreeVar extends Term {
105    String name;
106
107    public FreeVar(String name) {
108      this.name = name;
109    }
110
111    @SideEffectFree
112    @Override
113    public String name(@GuardSatisfied FreeVar this) {
114      return name;
115    }
116
117    @SideEffectFree
118    @Override
119    public String simplify_name() {
120      return "|" + name + "|";
121    }
122  }
123
124  /** Represents a constant integer. */
125  public static class Constant extends Term {
126    int val;
127
128    public Constant(int val) {
129      this.val = val;
130    }
131
132    @SideEffectFree
133    @Override
134    public String name(@GuardSatisfied Constant this) {
135      return "" + val;
136    }
137
138    public int get_value() {
139      return val;
140    }
141  }
142
143  /** Represents the length of a sequence and an optional offset. */
144  public static class Length extends Term {
145    VarInfo sequence;
146    int offset;
147
148    public Length(VarInfo sequence, int offset) {
149      this.sequence = sequence;
150      this.offset = offset;
151    }
152
153    @SideEffectFree
154    @Override
155    public String toString(@GuardSatisfied Length this) {
156      return name();
157    }
158
159    @SideEffectFree
160    @Override
161    public String name(@GuardSatisfied Length this) {
162      return name_with_offset("size(" + sequence.name() + ")", offset);
163    }
164
165    @SideEffectFree
166    @Override
167    public String esc_name() {
168      VarInfo arr_var = get_check_array_var("ESC");
169      if (arr_var.isPrestate()) {
170        assert arr_var.postState != null; // because isPrestate() = true
171        return String.format(
172            "\\old(%s)", name_with_offset(arr_var.postState.esc_name() + ".length", offset));
173      } else { // array is not orig
174        return name_with_offset(arr_var.esc_name() + ".length", offset);
175      }
176    }
177
178    @SideEffectFree
179    @Override
180    public String jml_name() {
181      VarInfo arr_var = get_check_array_var("JML");
182      if (arr_var.isPrestate()) {
183        assert arr_var.postState != null; // because isPrestate() = true
184        String name = String.format("daikon.Quant.size(%s)", arr_var.postState.jml_name());
185        return name_with_offset(String.format("\\old(%s)", name), offset);
186        // return String.format ("\\old(%s)", name_with_offset (name, offset));
187      } else {
188        String name = String.format("daikon.Quant.size(%s)", arr_var.jml_name());
189        return name_with_offset(name, offset);
190      }
191    }
192
193    @SideEffectFree
194    @Override
195    public String jml_name(boolean in_prestate) {
196      if (!in_prestate) {
197        return jml_name();
198      }
199
200      VarInfo arr_var = get_check_array_var("JML");
201      if (arr_var.isPrestate()) {
202        assert arr_var.postState != null; // because isPrestate() = true
203        String name = String.format("daikon.Quant.size(%s)", arr_var.postState.jml_name());
204        return name_with_offset(name, offset);
205      } else {
206        String name = String.format("daikon.Quant.size(\\new(%s))", arr_var.jml_name());
207        return name_with_offset(name, offset);
208      }
209    }
210
211    @SideEffectFree
212    @Override
213    public String simplify_name() {
214      VarInfo arr_var = get_check_array_var("Simplify");
215      String length = String.format("(arrayLength %s)", arr_var.simplify_name());
216      if (offset < 0) {
217        return String.format("(- %s %d)", length, -offset);
218      } else if (offset > 0) {
219        return String.format("(+ %s %d)", length, offset);
220      } else {
221        return length;
222      }
223    }
224
225    @SideEffectFree
226    @Override
227    public String csharp_name() {
228      VarInfo arr_var = get_check_array_var("CHARPCONTRACT");
229      return name_with_offset(arr_var.csharp_name() + ".Count()", offset);
230    }
231
232    public void set_offset(int offset) {
233      this.offset = offset;
234    }
235
236    /**
237     * Looks up the array variable which is the base of this array. Throws an exception if one does
238     * not exist.
239     */
240    @SuppressWarnings("all:sideeffectfree") // throws exception in case of error
241    @SideEffectFree
242    private VarInfo get_check_array_var(String output_format) {
243      VarInfo arr_var = sequence.get_base_array_hashcode();
244      if (arr_var != null) {
245        return arr_var;
246      }
247
248      throw new Daikon.UserError(
249          String.format(
250              "Error: Can't create %s expression for the size of an array: "
251                  + "No base array (hashcode) variable declared for array '%s'"
252                  + " in program point %s",
253              output_format, sequence.name(), sequence.ppt.name()));
254    }
255  }
256
257  /**
258   * Represents a Daikon variable with an optional integer offset. Usually used for the bounds of a
259   * slice.
260   */
261  public static class VarPlusOffset extends Term {
262    VarInfo var;
263    int offset;
264
265    public VarPlusOffset(VarInfo var) {
266      this(var, 0);
267    }
268
269    public VarPlusOffset(VarInfo var, int offset) {
270      this.var = var;
271      this.offset = offset;
272    }
273
274    @SideEffectFree
275    @Override
276    public String name(@GuardSatisfied VarPlusOffset this) {
277      return name_with_offset(var.name(), offset);
278    }
279
280    @SideEffectFree
281    @Override
282    public String esc_name() {
283      return name_with_offset(var.esc_name(), offset);
284    }
285
286    @SideEffectFree
287    @Override
288    public String jml_name() {
289      return name_with_offset(var.jml_name(), offset);
290    }
291
292    @SideEffectFree
293    @Override
294    public String jml_name(boolean in_prestate) {
295      if (!in_prestate) {
296        return jml_name();
297      }
298
299      if (var.isPrestate()) {
300        assert var.postState != null; // because isPrestate() = true
301        return name_with_offset(var.postState.jml_name(), offset);
302      } else {
303        return name_with_offset(String.format("\\new(%s)", var.jml_name()), offset);
304      }
305    }
306
307    @SideEffectFree
308    @Override
309    public String simplify_name() {
310      if (offset < 0) {
311        return String.format("(- %s %d)", var.simplify_name(), -offset);
312      } else if (offset > 0) {
313        return String.format("(+ %s %d)", var.simplify_name(), offset);
314      } else {
315        return var.simplify_name();
316      }
317    }
318  }
319
320  public static class QuantifyReturn {
321    /** Variable being quantified. */
322    public VarInfo var;
323
324    /** Index into the variable. If null, variable is not a sequence. */
325    public @Nullable Term index;
326
327    public QuantifyReturn(VarInfo var) {
328      this.var = var;
329    }
330  }
331
332  /**
333   * Given a list of sequences, determines a free variable that can be used as a subscript for each
334   * sequence. If any of the vars are not sequences, no index is calculated for them.
335   */
336  public static QuantifyReturn[] quantify(VarInfo[] vars) {
337    assert vars != null;
338
339    // create empty result
340    QuantifyReturn[] result = new QuantifyReturn[vars.length];
341    for (int ii = 0; ii < vars.length; ii++) {
342      result[ii] = new QuantifyReturn(vars[ii]);
343    }
344
345    // Determine all of the simple identifiers used by the given variables (vars)
346    Set<String> simples = new HashSet<>();
347    for (VarInfo vi : vars) {
348      for (String name : vi.get_all_simple_names()) {
349        simples.add(name);
350      }
351    }
352    // System.out.printf("simple names = %s%n", simples);
353
354    // Loop through each of the variables, choosing an index for each
355    char tmp = 'i';
356    for (int ii = 0; ii < vars.length; ii++) {
357      VarInfo vi = vars[ii];
358
359      // If this variable is not an array, there is not much to do
360      if (!vi.file_rep_type.isArray()) {
361        continue;
362      }
363
364      // Get a unique free variable name
365      String idx_name;
366      do {
367        idx_name = String.valueOf(tmp++);
368      } while (simples.contains(idx_name));
369      assert tmp <= 'z' : "Ran out of letters in quantification";
370      result[ii].index = new FreeVar(idx_name);
371    }
372    return result;
373  }
374
375  /** Class that represents an ESC quantification over one or two variables. */
376  public static class ESCQuantification {
377
378    private EnumSet<QuantFlags> flags;
379    // private VarInfo[] vars;
380    private VarInfo[] arr_vars;
381    private String[] arr_vars_indexed;
382    private String[] quants;
383    private String quant;
384    private Term[] indices;
385
386    public ESCQuantification(EnumSet<QuantFlags> flags, VarInfo... vars) {
387      this.flags = flags.clone();
388
389      assert vars != null;
390      assert (vars.length == 1) || (vars.length == 2) : vars.length;
391      assert vars[0].file_rep_type.isArray();
392
393      // quantification for first var
394      Term index1 = new FreeVar("i");
395      String quant1 = bld_quant(vars[0], index1);
396      VarInfo arr_var1 = vars[0].get_array_var();
397      String arr_var1_index = arr_var1.esc_name(index1.esc_name());
398
399      // If there is a second array variable, get quant for it
400      if ((vars.length > 1) && vars[1].file_rep_type.isArray()) {
401        Term index2 = new FreeVar("j");
402        String quant2 = bld_quant(vars[1], index2);
403        indices = new Term[] {index1, index2};
404        quants = new String[] {quant1, quant2};
405        if (flags.contains(QuantFlags.ELEMENT_WISE)) {
406          quant =
407              String.format(
408                  "(\\forall int %s, %s; (%s && %s && %s == %s)",
409                  index1.esc_name(),
410                  index2.esc_name(),
411                  quant1,
412                  quant2,
413                  index1.esc_name(),
414                  index2.esc_name());
415        } else {
416          quant =
417              String.format(
418                  "(\\forall int %s, %s; (%s && %s)",
419                  index1.esc_name(), index2.esc_name(), quant1, quant2);
420        }
421
422        VarInfo arr_var2 = vars[1].get_array_var();
423        arr_vars = new VarInfo[] {arr_var1, arr_var2};
424        String arr_var2_index = arr_var2.esc_name(index2.esc_name());
425        arr_vars_indexed = new String[] {arr_var1_index, arr_var2_index};
426      } else { // only one array variable
427        indices = new Term[] {index1};
428        quants = new String[] {quant1};
429        quant = String.format("(\\forall int %s; (%s)", index1.esc_name(), quant1);
430        arr_vars = new VarInfo[] {arr_var1};
431        arr_vars_indexed = new String[] {arr_var1_index};
432      }
433    }
434
435    /**
436     * Returns a string quantification expression for the array variable var using index. The
437     * expression is of the form
438     *
439     * <pre>{@code lower_bound <= index && index <= upper_bound}</pre>
440     */
441    private static String bld_quant(VarInfo var, Term index) {
442      return String.format(
443          "%s <= %s && %s <= %s",
444          var.get_lower_bound().esc_name(),
445          index.esc_name(),
446          index.esc_name(),
447          var.get_upper_bound().esc_name());
448    }
449
450    /**
451     * Returns the quantification string. For example, if there is one array variable (a[]) that is
452     * not a slice, it will return
453     *
454     * <pre>{@code
455     * '(\forall int i; (0 <= i <= size(a[]) ==> '
456     * }</pre>
457     */
458    public String get_quantification() {
459      return quant + " ==> ";
460    }
461
462    /**
463     * Returns the specified array variable indexed by its index. For example, if the array variable
464     * is 'a.b[]' and the index is 'i', returns a.b[i].
465     */
466    public String get_arr_vars_indexed(int num) {
467      return arr_vars_indexed[num];
468    }
469  }
470
471  /** Class that represents an Simplify quantification over one or two variables. */
472  public static class SimplifyQuantification {
473
474    EnumSet<QuantFlags> flags;
475    String quantification;
476    String[] arr_vars_indexed;
477    @Nullable String[] indices;
478
479    public SimplifyQuantification(EnumSet<QuantFlags> flags, VarInfo... vars) {
480      this.flags = flags.clone();
481
482      assert vars != null;
483      assert (vars.length == 1) || (vars.length == 2) : vars.length;
484      assert vars[0].file_rep_type.isArray();
485
486      if (flags.contains(QuantFlags.ADJACENT) || flags.contains(QuantFlags.DISTINCT)) {
487        assert vars.length == 2;
488      }
489
490      QuantifyReturn[] qrets = quantify(vars);
491
492      // build the forall predicate
493      StringJoiner int_list, conditions;
494      {
495        // "i j ..."
496        int_list = new StringJoiner(" ");
497        // "(AND (<= ai i) (<= i bi) (<= aj j) (<= j bj) ...)"
498        // if elementwise, also insert "(EQ (- i ai) (- j aj)) ..."
499        conditions = new StringJoiner(" ");
500        for (int i = 0; i < qrets.length; i++) {
501          Term idx = qrets[i].index;
502          if (idx == null) {
503            continue;
504          }
505          VarInfo vi = qrets[i].var;
506          Term low = vi.get_lower_bound();
507          Term high = vi.get_upper_bound();
508          int_list.add(idx.simplify_name());
509          conditions.add("(<= " + low.simplify_name() + " " + idx.simplify_name() + ")");
510          conditions.add("(<= " + idx.simplify_name() + " " + high.simplify_name() + ")");
511          if (flags.contains(QuantFlags.ELEMENT_WISE) && (i >= 1)) {
512            // Term[] _boundv = qret.bound_vars.get(i-1);
513            // Term _idx = _boundv[0], _low = _boundv[1];
514            @SuppressWarnings(
515                "nullness") // if variable is a sequence (is it?), then index is non-null
516            @NonNull Term _idx = qrets[i - 1].index;
517            Term _low = qrets[i - 1].var.get_lower_bound();
518            if (_low.simplify_name().equals(low.simplify_name())) {
519              conditions.add("(EQ " + _idx.simplify_name() + " " + idx.simplify_name() + ")");
520            } else {
521              conditions.add("(EQ (- " + _idx.simplify_name() + " " + _low.simplify_name() + ")");
522              conditions.add("(- " + idx.simplify_name() + " " + low.simplify_name() + "))");
523            }
524          }
525          if (i == 1
526              && (flags.contains(QuantFlags.ADJACENT) || flags.contains(QuantFlags.DISTINCT))) {
527            // Term[] _boundv = qret.bound_vars.get(i-1);
528            // Term prev_idx = _boundv[0];
529            @SuppressWarnings(
530                "nullness") // if variable is a sequence (is it?), then index is non-null
531            @NonNull Term prev_idx = qrets[i - 1].index;
532            if (flags.contains(QuantFlags.ADJACENT)) {
533              conditions.add(
534                  "(EQ (+ " + prev_idx.simplify_name() + " 1) " + idx.simplify_name() + ")");
535            }
536            if (flags.contains(QuantFlags.DISTINCT)) {
537              conditions.add("(NEQ " + prev_idx.simplify_name() + " " + idx.simplify_name() + ")");
538            }
539          }
540        }
541      }
542      quantification = "(FORALL (" + int_list + ") (IMPLIES (AND " + conditions + ") ";
543
544      // stringify the terms
545      List<String> avi_list = new ArrayList<>(vars.length);
546      for (QuantifyReturn qret : qrets) {
547        String arr_var_indexed;
548        if (qret.index != null) {
549          Term index = qret.index;
550          VarInfo arr_var = qret.var.get_array_var();
551          arr_var_indexed = arr_var.simplify_name(index.simplify_name());
552          // System.out.printf("vi = %s, arr_var = %s%n", vi, arr_var);
553        } else {
554          arr_var_indexed = qret.var.simplify_name();
555        }
556        avi_list.add(arr_var_indexed);
557        // result[i + 1] = qret.root_primes[i].simplify_name();
558      }
559      arr_vars_indexed = avi_list.toArray(new String[0]);
560
561      // stringify the indices,
562      // note that the index should be relative to the slice, not relative
563      // to the original array (we used to get this wrong)
564      indices = new @Nullable String[vars.length];
565      for (int i = 0; i < qrets.length; i++) {
566        // Term[] boundv = qret.bound_vars.get(i);
567        // Term idx_var = boundv[0];
568        QuantifyReturn qret = qrets[i];
569        if (qret.index == null) {
570          continue;
571        }
572        String idx_var_name = qret.index.simplify_name();
573        String lower_bound = qret.var.get_lower_bound().simplify_name();
574        String idx_expr = "(- " + idx_var_name + " " + lower_bound + ")";
575        indices[i] = idx_expr;
576      }
577    }
578
579    /** Returns the quantification string that quantifies over each of the free variables. */
580    public String get_quantification() {
581      return quantification;
582    }
583
584    /**
585     * Returns the specified array variable indexed by its index. For example, if the array variable
586     * is 'a[]' and the index is 'i', returns 'select i a'.
587     */
588    public String get_arr_vars_indexed(int num) {
589      return arr_vars_indexed[num];
590    }
591
592    /**
593     * Returns the term at the specified index.
594     *
595     * @param num the term's index
596     * @return the term at the specified index
597     */
598    @SuppressWarnings("nullness:return") // possible application invariant?
599    public String get_index(int num) {
600      assert indices[num] != null; // will this assertion fail?
601      return indices[num];
602    }
603
604    /** Returns the string to be appended to the end of the quantification. */
605    public String get_closer() {
606      return "))"; // close IMPLIES, FORALL
607    }
608  }
609}