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}