Merge pull request #7214 from remi-delmas-3000/contracts-assigns-clause-allow-all-void-function-calls

feliperodri · web-flow · commit 057fe4e27b26 · 2022-10-07T12:51:34.000-04:00
CONTRACTS: Allow void function calls in assigns clauses
diff --git a/regression/contracts/assigns_enforce_address_of/test.desc b/regression/contracts/assigns_enforce_address_of/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc b/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$
diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc b/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$
diff --git a/regression/contracts/assigns_enforce_function_calls/main.c b/regression/contracts/assigns_enforce_function_calls/main.c
@@ -13,5 +13,4 @@ int main()
 {
   int x;
   foo(&x);
-  baz(&x);
 }
diff --git a/regression/contracts/assigns_enforce_function_calls/test.desc b/regression/contracts/assigns_enforce_function_calls/test.desc
@@ -3,8 +3,8 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: expecting void return type for function 'bar' called in assigns clause$
 ^CONVERSION ERROR$
 --
 --
-Check that function call expressions are rejected in assigns clauses.
+Check that non-void function call expressions are rejected in assigns clauses.
diff --git a/regression/contracts/assigns_enforce_function_calls_ignored/main.c b/regression/contracts/assigns_enforce_function_calls_ignored/main.c
@@ -0,0 +1,17 @@
+void bar(int *x)
+{
+  if(x)
+    __CPROVER_typed_target(x);
+}
+
+int foo(int *x) __CPROVER_assigns(bar(x))
+{
+  *x = 0;
+  return 0;
+}
+
+int main()
+{
+  int x;
+  foo(&x);
+}
diff --git a/regression/contracts/assigns_enforce_function_calls_ignored/test.desc b/regression/contracts/assigns_enforce_function_calls_ignored/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^call to function 'bar' in assigns clause not supported yet$
+^EXIT=(127|134)$
+^SIGNAL=0$
+--
+--
+Check that void function call expressions in assigns clauses make
+instrumentation fail.
diff --git a/regression/contracts/assigns_enforce_literal/test.desc b/regression/contracts/assigns_enforce_literal/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_side_effects_2/test.desc b/regression/contracts/assigns_enforce_side_effects_2/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_side_effects_3/test.desc b/regression/contracts/assigns_enforce_side_effects_3/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 --
 Checks whether type checking rejects literal constants in assigns clause.
diff --git a/regression/contracts/reject_history_expr_in_assigns_clause/test.desc b/regression/contracts/reject_history_expr_in_assigns_clause/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^main.c.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^main.c.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 ^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
@@ -995,34 +995,34 @@ void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target)
   else if(can_cast_expr<side_effect_expr_function_callt>(target))
   {
     const auto &funcall = to_side_effect_expr_function_call(target);
-    if(can_cast_expr<symbol_exprt>(funcall.function()))
+    if(!can_cast_expr<symbol_exprt>(funcall.function()))
     {
-      const auto &ident = to_symbol_expr(funcall.function()).get_identifier();
-      if(
-        ident == CPROVER_PREFIX "assignable" ||
-        ident == CPROVER_PREFIX "object_whole" ||
-        ident == CPROVER_PREFIX "object_upto" ||
-        ident == CPROVER_PREFIX "object_from")
-      {
-        for(const auto &argument : funcall.arguments())
-          throw_on_side_effects(argument);
-        return;
-      }
+      throw invalid_source_file_exceptiont(
+        "function pointer calls not allowed in assigns clauses",
+        target.source_location());
     }
-    else
+
+    if(target.type().id() != ID_empty)
     {
       throw invalid_source_file_exceptiont(
-        "function pointer calls not allowed in assigns clauses",
+        "expecting void return type for function '" +
+          id2string(to_symbol_expr(funcall.function()).get_identifier()) +
+          "' called in assigns clause",
         target.source_location());
     }
+
+    for(const auto &argument : funcall.arguments())
+      throw_on_side_effects(argument);
+  }
+  else
+  {
+    // if we reach this point the target did not pass the checks
+    throw invalid_source_file_exceptiont(
+      "assigns clause target must be a non-void lvalue, a call "
+      "to " CPROVER_PREFIX
+      "POINTER_OBJECT or a call to a function returning void",
+      target.source_location());
   }
-  // if we reach this point the target did not pass the checks
-  throw invalid_source_file_exceptiont(
-    "assigns clause target must be a non-void lvalue or a call to one "
-    "of " CPROVER_PREFIX "POINTER_OBJECT, " CPROVER_PREFIX
-    "assignable, " CPROVER_PREFIX "object_whole, " CPROVER_PREFIX
-    "object_upto, " CPROVER_PREFIX "object_from",
-    target.source_location());
 }
 
 void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract(
diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp
@@ -487,6 +487,15 @@ car_exprt instrument_spec_assignst::create_car_expr(
     if(can_cast_expr<symbol_exprt>(funcall.function()))
     {
       const auto &ident = to_symbol_expr(funcall.function()).get_identifier();
+
+      PRECONDITION_WITH_DIAGNOSTICS(
+        ident == CPROVER_PREFIX "object_from" ||
+          ident == CPROVER_PREFIX "object_upto" ||
+          ident == CPROVER_PREFIX "object_whole" ||
+          ident == CPROVER_PREFIX "assignable",
+        "call to function '" + id2string(ident) +
+          "' in assigns clause not supported yet");
+
       if(ident == CPROVER_PREFIX "object_from")
       {
         const auto &ptr = funcall.arguments().at(0);
@@ -558,12 +567,6 @@ car_exprt instrument_spec_assignst::create_car_expr(
           is_ptr_to_ptr.is_true() ? car_havoc_methodt::NONDET_ASSIGN
                                   : car_havoc_methodt::HAVOC_SLICE};
       }
-      else
-      {
-        log.error().source_location = target.source_location();
-        log.error() << "call to " << ident
-                    << " in assigns clauses not supported in this version";
-      }
     }
   }
   else if(is_assignable(target))

Original file line number	Diff line number	Diff line change
`@@ -13,5 +13,4 @@ int main()`
`13`	`13`	`{`
`14`	`14`	`int x;`
`15`	`15`	`foo(&x);`
`16`		`- baz(&x);`
`17`	`16`	`}`