Merge pull request #4374 from tautschnig/nondet-test

Additional unbounded-array test that should continue to pass

Author: tautschnig

jbmc/regression/jbmc/nondet_propagation1/BitSet.class

@@ -0,0 +1,10 @@
+CORE
+andNot_Pass.class
+--depth 1600 --java-unwind-enum-static --java-max-vla-length 48 --unwind 4 --max-nondet-string-length 100 --function andNot_Pass.main
+^\[java::andNot_Pass\.main:\(\[Ljava/lang/String;\)V.assertion\.3\] line 40 assertion at file andNot_Pass\.java line 40 function java::andNot_Pass.main:\(\[Ljava/lang/String;\)V bytecode-index 52: FAILURE$
+^\*\* 1 of \d+ failed
+VERIFICATION FAILED
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/nondet_propagation1/andNot_Pass.class

@@ -0,0 +1,42 @@
+class BitSet {
+  boolean bits[];
+  public BitSet()
+  {
+    int size = org.cprover.CProver.nondetInt();
+    org.cprover.CProver.assume(size >= 0);
+    bits = new boolean[size];
+  }
+  public void set(int i)
+  {
+    org.cprover.CProver.assume(i < bits.length);
+    bits[i] = true;
+  }
+  public boolean get(int i)
+  {
+    if(i < bits.length)
+      return bits[i];
+    return false;
+  }
+  public void andNot(BitSet other)
+  {
+    for (int i = 0; i < bits.length; i++) {
+      bits[i] = bits[i] && !other.get(i);
+    }
+  }
+}
+
+public class andNot_Pass {
+  public static void main(String args[]) {
+    BitSet b1 = new BitSet();
+    b1.set(1);
+    b1.set(2);
+    BitSet b2 = new BitSet();
+    b2.set(0);
+    b2.set(2);
+    b1.andNot(b2);
+
+    assert(!b1.get(0));
+    assert(b1.get(1));
+    assert(b1.get(2)); // expected to fail
+  }
+}

jbmc/regression/jbmc/nondet_propagation1/andNot_Pass.desc

@@ -43,24 +43,40 @@ bvt boolbvt::convert_index(const index_exprt &expr)
     {
       // use array decision procedure
 
-      // free variables
-
-      bv.resize(width);
-      for(std::size_t i=0; i<width; i++)
-        bv[i]=prop.new_variable();
-
       if(has_byte_operator(expr))
-        record_array_index(to_index_expr(lower_byte_operators(expr, ns)));
+      {
+        const index_exprt final_expr =
+          to_index_expr(lower_byte_operators(expr, ns));
+        CHECK_RETURN(final_expr != expr);
+        bv = convert_bv(final_expr);
+
+        // record type if array is a symbol
+        const exprt &final_array = final_expr.array();
+        if(
+          final_array.id() == ID_symbol || final_array.id() == ID_nondet_symbol)
+        {
+          map.get_map_entry(final_array.get(ID_identifier), array_type);
+        }
+
+        // make sure we have the index in the cache
+        convert_bv(final_expr.index());
+      }
       else
-        record_array_index(expr);
+      {
+        // free variables
+        bv.reserve(width);
+        for(std::size_t i = 0; i < width; i++)
+          bv.push_back(prop.new_variable());
 
-      // record type if array is a symbol
+        record_array_index(expr);
 
-      if(array.id() == ID_symbol || array.id() == ID_nondet_symbol)
-        map.get_map_entry(array.get(ID_identifier), array_type);
+        // record type if array is a symbol
+        if(array.id() == ID_symbol || array.id() == ID_nondet_symbol)
+          map.get_map_entry(array.get(ID_identifier), array_type);
 
-      // make sure we have the index in the cache
-      convert_bv(index);
+        // make sure we have the index in the cache
+        convert_bv(index);
+      }
 
       return bv;
     }