[PSym] resolve rare failure due to nested any types with null values …

…and map value summaries

Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/MapVS.java

@@ -185,28 +185,23 @@ public PrimitiveVS<Boolean> symbolicEquals(MapVS<K, T, V> cmp, Guard pc) {
       return BooleanVS.trueUnderGuard(Guard.constFalse());
     }
 
-    Guard guard = BooleanVS.getTrueGuard(this.keys.symbolicEquals(cmp.keys, pc));
-    ListVS<T> thisSet = this.restrict(guard).getKeys();
-    ListVS<T> cmpSet = cmp.restrict(guard).getKeys();
-
-    if (thisSet.isEmpty() && cmpSet.isEmpty())
-      return BooleanVS.trueUnderGuard(guard).restrict(getUniverse().and(cmp.getUniverse()));
-
-    Guard equalCond = guard;
-    while (!thisSet.isEmpty()) {
-      T thisVal = thisSet.get(new PrimitiveVS<>(0, guard));
-      for (GuardedValue<?> key : ValueSummary.getGuardedValues(thisVal)) {
-        PrimitiveVS<Boolean> compareVals =
-            entries
-                .get(key.getValue())
-                .restrict(key.getGuard())
-                .symbolicEquals(
-                    cmp.entries.get(key.getValue()).restrict(key.getGuard()), equalCond);
-        equalCond = equalCond.and(BooleanVS.getTrueGuard(compareVals));
+    Guard keyGuard = BooleanVS.getTrueGuard(this.keys.symbolicEquals(cmp.keys, pc));
+
+    Guard notEqual = Guard.constFalse();
+    for (Object key: this.restrict(keyGuard).getKeys().getItems()) {
+      ValueSummary thisVal = this.entries.get(key);
+      ValueSummary cmpVal = cmp.entries.get(key);
+      if (thisVal == null && cmpVal == null) {
+          continue;
+      } else if (thisVal == null) {
+        notEqual = notEqual.or(cmpVal.symbolicEquals(null, Guard.constTrue()).getGuardFor(false));
+      } else if (cmpVal == null) {
+        notEqual = notEqual.or(thisVal.symbolicEquals(null, Guard.constTrue()).getGuardFor(false));
+      } else {
+        notEqual = notEqual.or(thisVal.symbolicEquals(cmpVal, Guard.constTrue()).getGuardFor(false));
       }
-      thisSet = thisSet.removeAt(new PrimitiveVS<>(0, thisVal.getUniverse()));
     }
-
+    Guard equalCond = keyGuard.and(notEqual.not());
     return BooleanVS.trueUnderGuard(equalCond).restrict(getUniverse().and(cmp.getUniverse()));
   }
 
@@ -227,7 +222,7 @@ public MapVS<K, T, V> put(T keySummary, V valSummary) {
     final Map<K, V> newEntries = new HashMap<>(entries);
     for (GuardedValue<?> guardedKey : ValueSummary.getGuardedValues(keySummary)) {
       V oldVal = entries.get(guardedKey.getValue());
-      if (oldVal == null) {
+      if (oldVal == null || oldVal.isEmptyVS()) {
         newEntries.put((K) guardedKey.getValue(), valSummary);
       } else {
         newEntries.put(

Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/PrimitiveVS.java

@@ -312,18 +312,34 @@ public PrimitiveVS<T> updateUnderGuard(Guard guard, PrimitiveVS<T> updateVal) {
   public PrimitiveVS<T> merge(Iterable<PrimitiveVS<T>> summaries) {
     final Map<T, Guard> result = new HashMap<>();
 
+    Guard nullUniverse = Guard.constFalse();
+    Guard coveredUniverse = Guard.constFalse();
+    Guard totalUniverse = getUniverse();
     for (Map.Entry<T, Guard> entry : guardedValues.entrySet()) {
       if (entry.getKey() == null) {
+        nullUniverse = nullUniverse.or(entry.getValue());
         continue;
       }
+      coveredUniverse = coveredUniverse.or(entry.getValue());
       result.merge(entry.getKey(), entry.getValue(), Guard::or);
     }
 
     for (PrimitiveVS<T> summary : summaries) {
+      totalUniverse = totalUniverse.or(summary.getUniverse());
       for (Map.Entry<T, Guard> entry : summary.guardedValues.entrySet()) {
+        if (entry.getKey() == null) {
+          nullUniverse = nullUniverse.or(entry.getValue());
+          continue;
+        }
+        coveredUniverse = coveredUniverse.or(entry.getValue());
         result.merge(entry.getKey(), entry.getValue(), Guard::or);
       }
     }
+    Guard remainingUniverse = totalUniverse.and(coveredUniverse.not());
+    if (!remainingUniverse.isFalse()) {
+      assert (remainingUniverse.implies(nullUniverse).isTrue());
+      result.put(null, remainingUniverse);
+    }
 
     return new PrimitiveVS<>(result);
   }

Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/TupleVS.java

@@ -1,5 +1,6 @@
 package psym.valuesummary;
 
+import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.Collections;
 import java.util.List;
@@ -24,13 +25,15 @@ public class TupleVS implements ValueSummary<TupleVS> {
   /**
    * Copy-constructor for TupleVS
    *
-   * @param fields Fields of the tuple
-   * @param classes Types of the fields of the tuple
+   * @param inpFields Fields of the tuple
+   * @param inpClasses Types of the fields of the tuple
    */
-  public TupleVS(ValueSummary[] fields, Class[] classes) {
-    this.fields = fields;
-    this.classes = classes;
+  public TupleVS(ValueSummary[] inpFields, Class[] inpClasses) {
+    this.fields = Arrays.copyOf(inpFields, inpFields.length);
+    this.classes = Arrays.copyOf(inpClasses, inpClasses.length);
     this.concreteHash = computeConcreteHash();
+    assert (IntStream.range(0, this.fields.length).allMatch(x -> this.fields[x].getUniverse().equals(this.fields[0].getUniverse()))) :
+            "Error in tuple field guards";
   }
 
   /**
@@ -39,9 +42,7 @@ public TupleVS(ValueSummary[] fields, Class[] classes) {
    * @param old The TupleVS to copy
    */
   public TupleVS(TupleVS old) {
-    this(
-        Arrays.copyOf(old.fields, old.fields.length),
-        Arrays.copyOf(old.classes, old.classes.length));
+    this(old.fields, old.classes);
   }
 
   /** Make a new TupleVS from the provided items */
@@ -62,6 +63,8 @@ public TupleVS(ValueSummary<?>... items) {
             .collect(Collectors.toList())
             .toArray(new Class[items.length]);
     this.concreteHash = computeConcreteHash();
+    assert (IntStream.range(0, this.fields.length).allMatch(x -> this.fields[x].getUniverse().equals(this.fields[0].getUniverse()))) :
+            "Error in tuple field guards";
   }
 
   /**
@@ -83,7 +86,7 @@ public TupleVS getCopy() {
   public TupleVS swap(Machine m1, Machine m2) {
     return new TupleVS(
         Arrays.stream(this.fields).map(x -> x.swap(m1, m2)).toArray(size -> new ValueSummary[size]),
-        Arrays.copyOf(this.classes, this.classes.length));
+        this.classes);
   }
 
   /**
@@ -152,8 +155,6 @@ public boolean isEmptyVS() {
 
   @Override
   public TupleVS restrict(Guard guard) {
-    if (guard.equals(getUniverse())) return new TupleVS(this);
-
     ValueSummary<?>[] resultFields = new ValueSummary[fields.length];
     for (int i = 0; i < fields.length; i++) {
       resultFields[i] = fields[i].restrict(guard);
@@ -163,7 +164,7 @@ public TupleVS restrict(Guard guard) {
 
   @Override
   public TupleVS merge(Iterable<TupleVS> summaries) {
-    List<ValueSummary> resultList = Arrays.asList(fields);
+    List<ValueSummary> resultList = Arrays.asList(Arrays.copyOf(fields, fields.length));
     for (TupleVS summary : summaries) {
       for (int i = 0; i < summary.fields.length; i++) {
         if (i < resultList.size()) {
@@ -218,8 +219,6 @@ public Guard getUniverse() {
     // Optimization: Tuples should always be nonempty,
     // and all fields should exist under the same conditions
     Guard result = fields[0].getUniverse();
-    assert IntStream.range(0, fields.length).allMatch(i -> fields[i].getUniverse().equals(result)):
-          "Error: all tuple fields should have same universe";
     return result;
   }
 

Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/UnionVS.java

@@ -36,7 +36,7 @@ public UnionVS() {
     UnionVStype type = UnionVStype.getUnionVStype(PrimitiveVS.class, null);
     this.type = new PrimitiveVS<>(type);
     this.value = new HashMap<>();
-    this.value.put(type, null);
+    this.value.put(type, new PrimitiveVS(null, Guard.constTrue()));
     this.concreteHash = computeConcreteHash();
   }
 
@@ -191,7 +191,10 @@ public UnionVS merge(Iterable<UnionVS> summaries) {
       List<ValueSummary> value = entry.getValue();
       ValueSummary newValue = null;
       if (value.size() > 0) {
-        newValue = value.get(0).merge(value.subList(1, entry.getValue().size()));
+        newValue = value.get(0);
+        if (value.size() > 1) {
+          newValue = newValue.merge(value.subList(1, entry.getValue().size()));
+        }
       }
       mergedValue.put(type, newValue);
     }