Add tests for let-expression introduction on double-deref

Author: smowton

regression/cbmc/double_deref/README

@@ -0,0 +1,27 @@
+This is a batch of tests checking cbmc's behaviour against expressions with more than one deref
+operator, such as **p, *(int*)*p, p->field1->field2, etc. At present a directly nested dereference
+(**p) is handled by pushing the second deref inside the result of the first. Example:
+
+**p ==>
+*(p == &o1 ? o1 : o2) ==>
+(p == &o1 ? *o1 : *o2) ==>
+(p == &o1 ? (o1 == &o3 ? o3 : o4) : (o2 == &o5 ? o5 : o6))
+
+This deref operator push-in is performed (implicitly) by value_set_dereferencet::dereference, which special-cases
+the ternary conditional expression.
+More complicated expressions are handled using a let-expression. Example:
+
+p->field1->field2 ==>
+((p == &o1 ? o1 : o2).field1)->field2 ==>
+let derefd_pointer = ((p == &o1 ? o1 : o2).field1) in (derefd_pointer == &o3 ? o3 : derefd_pointer == &o4 ? o4 : derefd_pointer == &o5 ? o5 : o6)
+
+Symex executes this let-expression as an auxiliary assignment, such as
+derefd_pointer = ((p == &o1 ? o1 : o2).field1)
+result = (derefd_pointer == &o3 ? o3 : derefd_pointer == &o4 ? o4 : derefd_pointer == &o5 ? o5 : o6)
+
+The tests in this directory check that auxiliary let-expressions like this are only used when appropriate by inspecting formula VCCs:
+double_deref.desc -- a directly nested double-dereference, should not use a let-expression
+double_deref_with_cast.desc -- a double-deref with an intervening cast (*(int*)*p for example), should use a let-expression
+double_deref_with_member.desc -- a double-deref with an intervening member expression (p->field1->field2), should use a let-expression
+double_deref_with_pointer_arithmetic.desc -- a double-deref with intervening pointer arithmetic (p[idx1][idx2]), should use a let-expression
+*_single_alias.desc -- variants of the above where the first dereference points to a single possible object, so no let-expression is necessary

regression/cbmc/double_deref/double_deref.c

@@ -0,0 +1,16 @@
+
+#include <assert.h>
+#include <stdlib.h>
+
+int main(int argc, char **argv)
+{
+  int **pptr;
+  int *ptr1 = (int *)malloc(sizeof(int));
+  *ptr1 = 1;
+  int *ptr2 = (int *)malloc(sizeof(int));
+  *ptr2 = 2;
+
+  pptr = (argc == 5 ? &ptr1 : &ptr2);
+
+  assert(**pptr == argc);
+}

regression/cbmc/double_deref/double_deref.desc

@@ -0,0 +1,10 @@
+CORE
+double_deref.c
+--show-vcc
+\{1\} \(main::1::pptr!0@1#2 = address_of\(main::1::ptr[12]!0@1\) \? main::argc!0@1#1 = [12] : main::argc!0@1#1 = [12]\)
+^EXIT=0$
+^SIGNAL=0$
+--
+derefd_pointer::derefd_pointer
+--
+See README for details about these tests

regression/cbmc/double_deref/double_deref_single_alias.c

@@ -0,0 +1,14 @@
+
+#include <assert.h>
+#include <stdlib.h>
+
+int main(int argc, char **argv)
+{
+  int **pptr;
+  int *ptr1 = (int *)malloc(sizeof(int));
+  *ptr1 = 1;
+
+  pptr = &ptr1;
+
+  assert(**pptr == argc);
+}

regression/cbmc/double_deref/double_deref_single_alias.desc

@@ -0,0 +1,10 @@
+CORE
+double_deref_single_alias.c
+--show-vcc
+\{1\} main::argc!0@1#1 = 1
+^EXIT=0$
+^SIGNAL=0$
+--
+derefd_pointer::derefd_pointer
+--
+See README for details about these tests

regression/cbmc/double_deref/double_deref_with_cast.c

@@ -0,0 +1,16 @@
+
+#include <assert.h>
+#include <stdlib.h>
+
+int main(int argc, char **argv)
+{
+  void **pptr;
+  int *ptr1 = (int *)malloc(sizeof(int));
+  *ptr1 = 1;
+  int *ptr2 = (int *)malloc(sizeof(int));
+  *ptr2 = 2;
+
+  pptr = (argc == 1 ? &ptr1 : &ptr2);
+
+  assert(*(int *)*pptr == argc);
+}

regression/cbmc/double_deref/double_deref_with_cast.desc

@@ -0,0 +1,10 @@
+CORE
+double_deref_with_cast.c
+--show-vcc
+^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 =
+^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[1-9]+\) \? main::argc!0@1#1 = [12] : main::argc!0@1#1 = [12]
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+See README for details about these tests

regression/cbmc/double_deref/double_deref_with_cast_single_alias.c

@@ -0,0 +1,14 @@
+
+#include <assert.h>
+#include <stdlib.h>
+
+int main(int argc, char **argv)
+{
+  void **pptr;
+  int *ptr1 = (int *)malloc(sizeof(int));
+  *ptr1 = 1;
+
+  pptr = &ptr1;
+
+  assert(*(int *)*pptr == argc);
+}

regression/cbmc/double_deref/double_deref_with_cast_single_alias.desc

@@ -0,0 +1,10 @@
+CORE
+double_deref_with_cast_single_alias.c
+--show-vcc
+\{1\} main::argc!0@1#1 = 1
+^EXIT=0$
+^SIGNAL=0$
+--
+derefd_pointer::derefd_pointer
+--
+See README for details about these tests

regression/cbmc/double_deref/double_deref_with_member.c

@@ -0,0 +1,22 @@
+
+#include <assert.h>
+#include <stdlib.h>
+
+struct container
+{
+  int *iptr;
+};
+
+int main(int argc, char **argv)
+{
+  struct container *cptr;
+  struct container container1, container2;
+  container1.iptr = (int *)malloc(sizeof(int));
+  *container1.iptr = 1;
+  container2.iptr = (int *)malloc(sizeof(int));
+  *container2.iptr = 2;
+
+  cptr = (argc == 1 ? &container1 : &container2);
+
+  assert(*(cptr->iptr) == argc);
+}

regression/cbmc/double_deref/double_deref_with_member.desc

@@ -0,0 +1,10 @@
+CORE
+double_deref_with_member.c
+--show-vcc
+^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \(main::1::cptr!0@1#2 = address_of\(main::1::container[12]!0@1\) \? address_of\(symex_dynamic::dynamic_object[12]\) : address_of\(symex_dynamic::dynamic_object[12]\)\)
+^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[12]\) \? main::argc!0@1#1 = 2 : main::argc!0@1#1 = 1\)
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+See README for details about these tests

regression/cbmc/double_deref/double_deref_with_member_single_alias.c

@@ -0,0 +1,20 @@
+
+#include <assert.h>
+#include <stdlib.h>
+
+struct container
+{
+  int *iptr;
+};
+
+int main(int argc, char **argv)
+{
+  struct container *cptr;
+  struct container container1;
+  container1.iptr = (int *)malloc(sizeof(int));
+  *container1.iptr = 1;
+
+  cptr = &container1;
+
+  assert(*(cptr->iptr) == argc);
+}

regression/cbmc/double_deref/double_deref_with_member_single_alias.desc

@@ -0,0 +1,10 @@
+CORE
+double_deref_with_member_single_alias.c
+--show-vcc
+\{1\} main::argc!0@1#1 = 1
+^EXIT=0$
+^SIGNAL=0$
+--
+derefd_pointer::derefd_pointer
+--
+See README for details about these tests

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.c

@@ -0,0 +1,22 @@
+
+#include <assert.h>
+#include <stdlib.h>
+
+struct container
+{
+  int *iptr;
+};
+
+int main(int argc, char **argv)
+{
+  int **new_ptrs = malloc(2 * sizeof(int *));
+  int *iptr1 = (int *)malloc(sizeof(int));
+  *iptr1 = 1;
+  int *iptr2 = (int *)malloc(sizeof(int));
+  *iptr2 = 2;
+
+  new_ptrs[argc % 2] = iptr1;
+  new_ptrs[1 - (argc % 2)] = iptr2;
+
+  assert(*(new_ptrs[argc % 2]) == argc);
+}

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc

@@ -0,0 +1,10 @@
+CORE
+double_deref_with_pointer_arithmetic.c
+--show-vcc
+^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = symex_dynamic::dynamic_object1#3\[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 : main::argc!0@1#1 = 1\)
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+See README for details about these tests

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.c

@@ -0,0 +1,19 @@
+
+#include <assert.h>
+#include <stdlib.h>
+
+struct container
+{
+  int *iptr;
+};
+
+int main(int argc, char **argv)
+{
+  int **new_ptrs = malloc(2 * sizeof(int *));
+  int *iptr1 = (int *)malloc(sizeof(int));
+  *iptr1 = 1;
+
+  new_ptrs[argc % 2] = iptr1;
+
+  assert(*(new_ptrs[argc % 2]) == argc);
+}

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc

@@ -0,0 +1,10 @@
+CORE
+double_deref_with_pointer_arithmetic_single_alias.c
+--show-vcc
+\{1\} main::argc!0@1#1 = 1
+^EXIT=0$
+^SIGNAL=0$
+--
+derefd_pointer::derefd_pointer
+--
+See README for details about these tests