Merge pull request #8413 from tautschnig/dfcc-no-unnecessary-check

Dynamic frames: do not add trivial properties

Author: tautschnig

regression/contracts-dfcc/assigns_enforce_malloc_02/test.desc

@@ -2,9 +2,7 @@ CORE dfcc-only
 main.c
 --no-malloc-may-fail --dfcc main --enforce-contract f
 main.c function f
-^\[f.assigns.\d+\] line 7 Check that ptr is assignable: SUCCESS$
 ^\[f.assigns.\d+\] line 12 Check that \*ptr is assignable: SUCCESS$
-^\[f.assigns.\d+\] line 13 Check that n is assignable: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts-dfcc/assigns_enforce_statics/test.desc

@@ -1,7 +1,6 @@
 CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo _ --pointer-primitive-check
-^\[foo.assigns.\d+\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.assigns.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$
 ^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: FAILURE$
 ^VERIFICATION FAILED$

regression/contracts-dfcc/loop-freeness-check/test.desc

@@ -1,7 +1,6 @@
 CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
-^\[foo.assigns.\d+\].*Check that i is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].*Check that arr\[(\(.*\))?i\] is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$

regression/contracts-dfcc/loop_body_with_hole/test.desc

@@ -1,14 +1,11 @@
 CORE dfcc-only
 main.c
 --dfcc main --apply-loop-contracts
-^\[main.assigns.\d+\] line 6 Check that sum_to_k is assignable: SUCCESS$
-^\[main.assigns.\d+\] line 7 Check that flag is assignable: SUCCESS$
 ^\[main.assigns.\d+\] line 9 Check that i is assignable: SUCCESS$
 ^\[main.loop_assigns.\d+\] line 9 Check assigns clause inclusion for loop .*: SUCCESS$
 ^\[main.loop_invariant_base.\d+\] line 9 Check invariant before entry for loop .*: SUCCESS$
 ^\[main.loop_invariant_step.\d+\] line 9 Check invariant after step for loop .*: SUCCESS$
 ^\[main.loop_step_unwinding.\d+\] line 9 Check step was unwound for loop .*: SUCCESS$
-^\[main.assigns.\d+\] line 17 Check that flag is assignable: SUCCESS$
 ^\[main.assigns.\d+\] line 20 Check that sum_to_k is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp

@@ -693,54 +693,38 @@ void dfcc_instrumentt::instrument_lhs(
   check_source_location.set_comment(
     "Check that " + from_expr_using_mode(ns, mode, lhs) + " is assignable");
 
-  if(cfg_info.must_check_lhs(target))
-  {
-    // ```
-    // IF !write_set GOTO skip_target;
-    // DECL check_assign: bool;
-    // CALL check_assign = check_assignment(write_set, &lhs, sizeof(lhs));
-    // ASSERT(check_assign);
-    // DEAD check_assign;
-    // skip_target: SKIP;
-    // ----
-    // ASSIGN lhs := rhs;
-    // ```
+  // ```
+  // IF !write_set GOTO skip_target;
+  // DECL check_assign: bool;
+  // CALL check_assign = check_assignment(write_set, &lhs, sizeof(lhs));
+  // ASSERT(check_assign);
+  // DEAD check_assign;
+  // skip_target: SKIP;
+  // ----
+  // ASSIGN lhs := rhs;
+  // ```
 
-    const auto check_var = dfcc_utilst::create_symbol(
-      goto_model.symbol_table,
-      bool_typet(),
-      function_id,
-      "__check_lhs_assignment",
-      lhs_source_location);
+  const auto check_var = dfcc_utilst::create_symbol(
+    goto_model.symbol_table,
+    bool_typet(),
+    function_id,
+    "__check_lhs_assignment",
+    lhs_source_location);
 
-    payload.add(goto_programt::make_decl(check_var, lhs_source_location));
+  payload.add(goto_programt::make_decl(check_var, lhs_source_location));
 
-    payload.add(goto_programt::make_function_call(
-      library.write_set_check_assignment_call(
-        check_var,
-        write_set,
-        typecast_exprt::conditional_cast(
-          address_of_exprt(lhs), pointer_type(empty_typet{})),
-        dfcc_utilst::make_sizeof_expr(lhs, ns),
-        lhs_source_location),
-      lhs_source_location));
-
-    payload.add(
-      goto_programt::make_assertion(check_var, check_source_location));
-    payload.add(goto_programt::make_dead(check_var, check_source_location));
-  }
-  else
-  {
-    // ```
-    // IF !write_set GOTO skip_target;
-    // ASSERT(true);
-    // skip_target: SKIP;
-    // ----
-    // ASSIGN lhs := rhs;
-    // ```
-    payload.add(
-      goto_programt::make_assertion(true_exprt(), check_source_location));
-  }
+  payload.add(goto_programt::make_function_call(
+    library.write_set_check_assignment_call(
+      check_var,
+      write_set,
+      typecast_exprt::conditional_cast(
+        address_of_exprt(lhs), pointer_type(empty_typet{})),
+      dfcc_utilst::make_sizeof_expr(lhs, ns),
+      lhs_source_location),
+    lhs_source_location));
+
+  payload.add(goto_programt::make_assertion(check_var, check_source_location));
+  payload.add(goto_programt::make_dead(check_var, check_source_location));
 
   auto label_instruction =
     payload.add(goto_programt::make_skip(lhs_source_location));
@@ -786,7 +770,8 @@ void dfcc_instrumentt::instrument_assign(
   auto &write_set = cfg_info.get_write_set(target);
 
   // check the lhs
-  instrument_lhs(function_id, target, lhs, goto_program, cfg_info);
+  if(cfg_info.must_check_lhs(target))
+    instrument_lhs(function_id, target, lhs, goto_program, cfg_info);
 
   // handle dead_object updates (created by __builtin_alloca for instance)
   // Remark: we do not really need to track this deallocation since the default
@@ -1018,7 +1003,7 @@ void dfcc_instrumentt::instrument_function_call(
   auto &write_set = cfg_info.get_write_set(target);
 
   // Instrument the lhs if any.
-  if(target->call_lhs().is_not_nil())
+  if(target->call_lhs().is_not_nil() && cfg_info.must_check_lhs(target))
   {
     instrument_lhs(
       function_id, target, target->call_lhs(), goto_program, cfg_info);