From e409ce27733828731bc5ababd208565599d2c498 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@gmail.com>
Date: Mon, 5 Jul 2021 16:44:26 +0100
Subject: [PATCH] Include tests from reported issue cbmc#5952.

This is including two tests from https://github.com/diffblue/cbmc/issues/5952,
one of which succeeds demonstrating that the issue is now fixed,
and the other one is failing, marked so as `broken-smt-backend`, presumably
because of the `__CPROVER_r_ok` within an `assume` context.
---
 .../original_repro.c                          | 24 +++++++++++++++++++
 .../short.c                                   |  9 +++++++
 .../test_original.desc                        | 12 ++++++++++
 .../test_short.desc                           | 12 ++++++++++
 4 files changed, 57 insertions(+)
 create mode 100644 regression/cbmc/issue_5952_soundness_bug_smt_encoding/original_repro.c
 create mode 100644 regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c
 create mode 100644 regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_original.desc
 create mode 100644 regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc

diff --git a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/original_repro.c b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/original_repro.c
new file mode 100644
index 00000000000..f052e2a6ba4
--- /dev/null
+++ b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/original_repro.c
@@ -0,0 +1,24 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+bool validate(const char *data, unsigned allocated)
+{
+  // clang-format off
+  bool check_1 = (data == NULL ==> allocated == 0);
+  bool check_2 = (allocated != 0 ==> __CPROVER_r_ok(data, allocated));
+  // clang-format on
+  return check_1 && check_2;
+}
+
+void main()
+{
+  char *data;
+  unsigned allocated;
+
+  data = (allocated == 0) ? NULL : malloc(allocated);
+
+  __CPROVER_assume(validate(data, allocated));
+
+  assert(validate(data, allocated));
+}
diff --git a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c
new file mode 100644
index 00000000000..c92fed9cdad
--- /dev/null
+++ b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *data;
+  data = nondet() ? malloc(1) : malloc(2);
+  assert(__CPROVER_OBJECT_SIZE(data) <= 2);
+}
diff --git a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_original.desc b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_original.desc
new file mode 100644
index 00000000000..1f09f9e1000
--- /dev/null
+++ b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_original.desc
@@ -0,0 +1,12 @@
+KNOWNBUG broken-smt-backend
+original_repro.c
+--smt2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+\[main.assertion.\d\] line \d+ assertion validate\(data, allocated\): SUCCESS
+--
+\[main.assertion.\d\] line \d+ assertion validate\(data, allocated\): FAILURE
+--
+This is the original code that demonstrates the issue described in
+https://github.com/diffblue/cbmc/issues/5952
diff --git a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc
new file mode 100644
index 00000000000..eec1fc3fd4f
--- /dev/null
+++ b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc
@@ -0,0 +1,12 @@
+CORE
+short.c
+--smt2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+\[main.assertion.\d\] line \d assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: SUCCESS
+--
+\[main.assertion.\d\] line \d assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: FAILURE
+--
+This is the reduced version of the issue described in
+https://github.com/diffblue/cbmc/issues/5952