Merge pull request #7699 from remi-delmas-3000/contracts-check-side-effects-in-assigns-frees-clauses

CONTRACTS: re-enable side effect checking in assigns/frees clauses (HOTFIX)

Author: remi-delmas-3000

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;
+}

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.

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();
 }