Add regression tests for simplification of singleton intervals

Author: NlightNFotis

regression/cbmc/simplify_singleton_interval_7690/negative_test.desc

@@ -0,0 +1,18 @@
+CORE 
+--trace
+singleton_interval_simp_neg.c
+^VERIFICATION FAILED$
+^\[main\.assertion\.1\] line \d expected failure: paths where x is unbounded explored: FAILURE$
+^\[main\.assertion\.2\] line \d+ expected failure: paths where 0 \<= x \<= 15 explored: FAILURE$
+^\[main\.assertion\.3\] line \d+ expected success: paths where x \<= 15 explored: SUCCESS$
+y=-6 \(11111111 11111111 11111111 11111010\)
+x=14 \(00000000 00000000 00000000 00001110\)
+y=34 \(00000000 00000000 00000000 00100010\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This tests the negative case of the simplification of the singleton interval
+(i.e when the presented interval *is* the *not* the singleton interval - 
+the set of possible values that the bounded variable can take has cardinality
+> 1).

regression/cbmc/simplify_singleton_interval_7690/positive_test.desc

@@ -0,0 +1,13 @@
+CORE 
+--trace
+singleton_interval_simp.c
+^VERIFICATION FAILED$
+^\[main\.assertion\.1\] line \d+ expected failure: only paths where x == 15 explored: FAILURE$
+^\[main\.assertion\.2\] line \d+ expected failure: only paths where x == 15 explored: FAILURE$
+x=15 \(00000000 00000000 00000000 00001111\)
+y=35 \(00000000 00000000 00000000 00100011\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This tests the positive and 

regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c

@@ -0,0 +1,89 @@
+// Code presented in https://github.com/diffblue/cbmc/issues/7690
+
+// clang-format off
+
+#include <stdlib.h>
+#include <stdint.h>
+
+extern size_t __CPROVER_max_malloc_size;
+int __builtin_clzll(unsigned long long);
+
+#define __nof_symex_objects                                                    \
+  ((size_t)(1ULL << __builtin_clzll(__CPROVER_max_malloc_size)))
+
+typedef struct {
+  size_t k;
+  void **ptrs;
+} smap_t;
+
+void smap_init(smap_t *smap, size_t k) {
+  *smap = (smap_t){
+      .k = k, .ptrs = __CPROVER_allocate(__nof_symex_objects * sizeof(void *), 1)};
+}
+
+void *smap_get(smap_t *smap, void *ptr) {
+  size_t id = __CPROVER_POINTER_OBJECT(ptr);
+  void *sptr = smap->ptrs[id];
+  if (!sptr) {
+    sptr = __CPROVER_allocate(smap->k * __CPROVER_OBJECT_SIZE(ptr), 1);
+    smap->ptrs[id] = sptr;
+  }
+  return sptr + smap->k * __CPROVER_POINTER_OFFSET(ptr);
+}
+
+typedef struct {
+  uint8_t key;
+  uint8_t value;
+} stk_elem_t;
+
+typedef struct {
+  int8_t top;
+  stk_elem_t *elems;
+} stk_t;
+
+size_t nondet_size_t();
+
+// Creates a fresh borrow stack
+stk_t *stk_new() {
+  stk_t *stk = __CPROVER_allocate(sizeof(stk_t), 1);
+  size_t stk_size = nondet_size_t();
+  __CPROVER_assume(UINT8_MAX <= stk_size && stk_size <= UINT8_MAX);
+  // works with
+  // __CPROVER_assume(stk_size == UINT8_MAX);
+  *stk = (stk_t){
+      .top = 0,
+      .elems = __CPROVER_allocate(sizeof(stk_elem_t) * stk_size, 1)};
+  return stk;
+}
+
+void stk_push(stk_t *stk, uint8_t key, uint8_t value) {
+  assert(stk->top < UINT8_MAX);
+  stk->elems[stk->top] = (stk_elem_t){.key = key, .value = value};
+  stk->top++;
+}
+
+stk_t *get_stk(smap_t *smap, void *ptr) {
+  stk_t **stk_ptr = (stk_t **) smap_get(smap, ptr);
+  if (!(*stk_ptr)) {
+    *stk_ptr = stk_new();
+  }
+  return *stk_ptr;
+}
+
+typedef struct {
+  int a;
+  int b;
+} my_struct_t;
+
+int main() {
+  smap_t smap;
+  smap_init(&smap, sizeof(stk_t*));
+  my_struct_t my_struct;
+  stk_t *stk_a = get_stk(&smap, &(my_struct.a));
+  stk_push(stk_a, 1, 1);
+  stk_t *stk_b = get_stk(&smap, &(my_struct.b));
+  assert(stk_b);
+  stk_push(stk_b, 1, 1);
+}
+
+// clang-format on

regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp.c

@@ -0,0 +1,14 @@
+// Positive test for singleton interval simplification.
+// Notice that the sequence of the inequalities in this
+// expression is different to the one in
+// `singleton_interval_in_assume_7690.c`.
+
+int main() {
+    int x;
+    __CPROVER_assume(x >= 15 && x <= 15);
+    int y = x + 20;
+
+    __CPROVER_assert(y != 35, "expected failure: only paths where x == 15 explored");
+    __CPROVER_assert(y == 34, "expected failure: only paths where x == 15 explored");
+    return 0;
+}

regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp_neg.c

@@ -0,0 +1,15 @@
+// Negative test for singleton interval simplification.
+
+int main() {
+    int x;
+    int y = x + 20;
+
+    __CPROVER_assert(y != -6, "expected failure: paths where x is unbounded explored");
+    
+    __CPROVER_assume(x >= 0 && x <= 15);
+    __CPROVER_assert(y != 34, "expected failure: paths where 0 <= x <= 15 explored");
+    
+    int z = x + 20;
+    __CPROVER_assert(z != 36, "expected success: paths where x <= 15 explored");    
+    return 0;
+}

regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc

@@ -0,0 +1,14 @@
+CORE smt-backend new-smt-backend
+singleton_interval_in_assume_7690.c
+--pointer-check
+^\[stk_push\.pointer_dereference\.17] line \d+ dereference failure: pointer outside object bounds in stk-\>elems\[\(signed long int\)stk-\>top\]: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Without the singleton interval simplification implemented in
+https://github.com/diffblue/cbmc/pull/7761 this would fail in
+the (old) SMT backend in /src/solvers/smt2, because some constraints
+would not be propagated correctly, leaving the value of `stk_size`
+in `stk_new` as nondet.