From 445527d308c9bdbdd114466e848b5d2d4c25b59b Mon Sep 17 00:00:00 2001
From: Remi Delmas <delmasrd@amazon.com>
Date: Wed, 3 May 2023 16:03:25 +0000
Subject: [PATCH] CONTRACTS: re-enable side effect checking in assigns/frees
 clauses

This PR re-enables side effect checking in functions called from assigns
and frees clauses that was mistakenly disabled by PR 7671, and adds
a new test that checks that side effect checking is actually performed.
---
 .../main.c                                    | 54 +++++++++++++++++++
 .../test.desc                                 | 12 +++++
 .../dynamic-frames/dfcc_spec_functions.cpp    | 14 +++++
 3 files changed, 80 insertions(+)
 create mode 100644 regression/contracts-dfcc/assigns-frees-clauses-check-side-effects/main.c
 create mode 100644 regression/contracts-dfcc/assigns-frees-clauses-check-side-effects/test.desc

diff --git a/regression/contracts-dfcc/assigns-frees-clauses-check-side-effects/main.c b/regression/contracts-dfcc/assigns-frees-clauses-check-side-effects/main.c
new file mode 100644
index 00000000000..6d541a45fc2
--- /dev/null
+++ b/regression/contracts-dfcc/assigns-frees-clauses-check-side-effects/main.c
@@ -0,0 +1,54 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+// A function defining an assignable target
+void foo_assigns(char *ptr, const size_t size)
+{
+  __CPROVER_object_upto(ptr, size);
+
+  // an unauthorized side effect that must be detected
+  if(ptr && size > 0)
+    ptr[0] = 0;
+}
+
+// A function defining an freeable target
+void foo_frees(char *ptr, const size_t size)
+{
+  __CPROVER_freeable(ptr);
+
+  // an unauthorized side effect that must be detected
+  if(ptr && size > 0)
+    ptr[0] = 0;
+}
+
+char *foo(char *ptr, const size_t size, const size_t new_size)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(ptr, size))
+__CPROVER_assigns(foo_assigns(ptr, size))
+__CPROVER_frees(foo_frees(ptr, size))
+// clang-format on
+{
+  if(ptr && new_size > size)
+  {
+    free(ptr);
+    ptr = malloc(new_size);
+    return ptr;
+  }
+  else
+  {
+    if(size > 0)
+    {
+      ptr[0] = 0;
+    }
+    return ptr;
+  }
+}
+
+int main()
+{
+  size_t size;
+  size_t new_size;
+  char *ptr;
+  ptr = foo(ptr, size, new_size);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/assigns-frees-clauses-check-side-effects/test.desc b/regression/contracts-dfcc/assigns-frees-clauses-check-side-effects/test.desc
new file mode 100644
index 00000000000..dd2519f56dd
--- /dev/null
+++ b/regression/contracts-dfcc/assigns-frees-clauses-check-side-effects/test.desc
@@ -0,0 +1,12 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo --malloc-may-fail --malloc-fail-null
+^\[foo_assigns.assigns.\d+\] line \d+ Check that ptr\[\(.* int\)0\] is assignable: FAILURE$
+^\[foo_frees.assigns.\d+\] line \d+ Check that ptr\[\(.* int\)0\] is assignable: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test checks that side effects in functions called from the assigns clause
+or the frees clause are detected and make the analysis fail.
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp
index b7d4ac232e0..d9103bc5cfd 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp
@@ -272,6 +272,13 @@ void dfcc_spec_functionst::to_spec_assigns_function(
 
   goto_model.goto_functions.update();
 
+  // instrument for side-effects checking
+  std::set<irep_idt> function_pointer_contracts;
+  instrument.instrument_function(function_id, function_pointer_contracts);
+  INVARIANT(
+    function_pointer_contracts.empty(),
+    "discovered function pointer contracts unexpectedly");
+
   goto_model.goto_functions.function_map.at(function_id).make_hidden();
 }
 
@@ -355,6 +362,13 @@ void dfcc_spec_functionst::to_spec_frees_function(
 
   goto_model.goto_functions.update();
 
+  // instrument for side-effects checking
+  std::set<irep_idt> function_pointer_contracts;
+  instrument.instrument_function(function_id, function_pointer_contracts);
+  INVARIANT(
+    function_pointer_contracts.empty(),
+    "discovered function pointer contracts unexpectedly");
+
   goto_model.goto_functions.function_map.at(function_id).make_hidden();
 }