goto-symex: expand unknown points-to values to all objects

regression/cbmc/Pointer14/main.c

@@ -1,6 +1,4 @@
-typedef unsigned int size_t;
-
-void *malloc(size_t size);
+void *malloc(__CPROVER_size_t);
 
 enum blockstate
 {

regression/cbmc/String_Abstraction14/pass-in-implicit.c

@@ -1,4 +1,4 @@
-void *malloc(unsigned);
+void *malloc(__CPROVER_size_t);
 
 void use_str(char *s)
 {

regression/cbmc/String_Abstraction20/structs2.c

@@ -1,4 +1,4 @@
-void *malloc(unsigned);
+void *malloc(__CPROVER_size_t);
 
 typedef struct str_struct
 {

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc

@@ -2,7 +2,7 @@ CORE
 double_deref_with_pointer_arithmetic.c
 --show-vcc
 ^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
-^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\)
+^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : main::argc!0@1#1 = 1
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc

@@ -1,7 +1,7 @@
 CORE
 double_deref_with_pointer_arithmetic_single_alias.c
 --show-vcc
-\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object2\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)
+\{1\} main::argc!0@1#1 = 1
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc/nondet-pointer/nondet-pointer1.c

@@ -0,0 +1,13 @@
+int *nondet_pointer();
+
+int main()
+{
+  int x = 123;
+  int *p = &x;
+  int *q = nondet_pointer();
+
+  if(p == q)
+    __CPROVER_assert(*q == 123, "value of *q");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer1.desc

@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/nondet-pointer/nondet-pointer2.c

@@ -0,0 +1,14 @@
+int *nondet_pointer();
+
+int main()
+{
+  int x = 123, y = 456;
+  int *px = &x;
+  int *py = &y;
+  int *q = nondet_pointer();
+
+  if(q == px || q == py)
+    __CPROVER_assert(*q == 123 || *q == 456, "value of *q");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer2.desc

@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/nondet-pointer/nondet-pointer3.c

@@ -0,0 +1,18 @@
+int *nondet_pointer();
+
+int main()
+{
+  int some_array[10];
+  int *p = some_array;
+  int *q = nondet_pointer();
+  int index;
+
+  __CPROVER_assume(index >= 0 && index < 10);
+  __CPROVER_assume(q == p);
+
+  q[index] = 123;
+
+  __CPROVER_assert(some_array[index] == 123, "value of array[index]");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer3.desc

@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/nondet-pointer/nondet-pointer4.c

@@ -0,0 +1,18 @@
+int *nondet_pointer();
+
+int main()
+{
+  int some_array[10];
+  int *p = some_array;
+  int *q = nondet_pointer();
+  int index;
+
+  __CPROVER_assume(index >= 0 && index < 10);
+  __CPROVER_assume(q == p + index);
+
+  *q = 123;
+
+  __CPROVER_assert(some_array[index] == 123, "value of array[index]");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer4.desc

@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/nondet-pointer/nondet-pointer5.c

@@ -0,0 +1,19 @@
+int *nondet_pointer();
+
+int main()
+{
+  int some_array[10];
+  int *p = some_array;
+  int *q = nondet_pointer();
+  int index;
+
+  __CPROVER_assume(index >= 0 && index < 10);
+  __CPROVER_assume(__CPROVER_same_object(p, q));
+  __CPROVER_assume(__CPROVER_POINTER_OFFSET(q) == sizeof(int) * index);
+
+  *q = 123;
+
+  __CPROVER_assert(some_array[index] == 123, "value of array[index]");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer5.desc

@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/pointer-analysis/value_set.cpp

@@ -505,6 +505,23 @@ void value_sett::get_value_set_rec(
     else
       insert(dest, exprt(ID_unknown, original_type));
   }
+  else if(expr.id() == ID_nondet_symbol)
+  {
+    if(expr.type().id() == ID_pointer)
+    {
+      // we'll take the union of all objects we see, with unspecified offsets
+      values.iterate([this, &dest](const irep_idt &key, const entryt &value) {
+        for(const auto &object : value.object_map.read())
+          insert(dest, object.first, offsett());
+      });
+
+      // we'll add null, in case it's not there yet
+      insert(
+        dest,
+        exprt(ID_null_object, to_pointer_type(expr_type).subtype()),
+        offsett());
+    }
+  }
   else if(expr.id()==ID_if)
   {
     get_value_set_rec(
@@ -984,7 +1001,6 @@ void value_sett::get_value_set_rec(
   }
   else
   {
-    // for example: expr.id() == ID_nondet_symbol
     insert(dest, exprt(ID_unknown, original_type));
   }
 

src/solvers/flattening/boolbv_extractbits.cpp

@@ -31,18 +31,6 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
   auto upper_as_int = maybe_upper_as_int.value();
   auto lower_as_int = maybe_lower_as_int.value();
 
-  DATA_INVARIANT_WITH_DIAGNOSTICS(
-    upper_as_int >= 0 && upper_as_int < src_bv.size(),
-    "upper end of extracted bits must be within the bitvector",
-    expr.find_source_location(),
-    irep_pretty_diagnosticst{expr});
-
-  DATA_INVARIANT_WITH_DIAGNOSTICS(
-    lower_as_int >= 0 && lower_as_int < src_bv.size(),
-    "lower end of extracted bits must be within the bitvector",
-    expr.find_source_location(),
-    irep_pretty_diagnosticst{expr});
-
   DATA_INVARIANT(
     lower_as_int <= upper_as_int,
     "upper bound must be greater or equal to lower bound");
@@ -56,9 +44,40 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
     expr.find_source_location(),
     irep_pretty_diagnosticst{expr});
 
-  const std::size_t offset = numeric_cast_v<std::size_t>(lower_as_int);
+  bvt result_bv;
 
-  bvt result_bv(src_bv.begin() + offset, src_bv.begin() + offset + bv_width);
+  // add out-of-bounds bits (if any) at the lower end
+  if(lower_as_int < 0)
+  {
+    if(upper_as_int < 0)
+    {
+      lower_as_int -= upper_as_int + 1;
+      upper_as_int = 0;
+    }
+
+    const std::size_t lower_out_of_bounds =
+      numeric_cast_v<std::size_t>(-lower_as_int);
+    result_bv = prop.new_variables(lower_out_of_bounds);
+    lower_as_int = 0;
+  }
+
+  const std::size_t offset = numeric_cast_v<std::size_t>(lower_as_int);
+  const std::size_t upper_size_t = numeric_cast_v<std::size_t>(upper_as_int);
+
+  result_bv.reserve(bv_width);
+  result_bv.insert(
+    result_bv.end(),
+    src_bv.begin() + std::min(offset, src_bv.size()),
+    src_bv.begin() + std::min(src_bv.size(), upper_size_t + 1));
+
+  // add out-of-bounds bits (if any) at the upper end
+  if(upper_size_t >= src_bv.size())
+  {
+    bvt upper_oob_bits =
+      prop.new_variables(upper_size_t - std::max(offset, src_bv.size()) + 1);
+    result_bv.insert(
+      result_bv.end(), upper_oob_bits.begin(), upper_oob_bits.end());
+  }
 
   return result_bv;
 }