Function contracts: type checking rules for conditional targets in assigns clauses.

Author: Remi Delmas

src/ansi-c/c_typecheck_base.h

@@ -146,7 +146,16 @@ class c_typecheck_baset:
   virtual void typecheck_start_thread(codet &code);
 
   // contracts
+
+  /// \brief Typechecks a vector of assigns clause targets.
+  ///
+  /// \remark The vector will grow larger in case it contains conditional
+  /// targets of the form `c ? {t1, .. , tn}`, which get expanded to a
+  /// collection `{c ? t1, .. , c ? tn }` by distributing the condition `c`
+  /// on the list of targets.
   virtual void typecheck_spec_assigns(exprt::operandst &targets);
+  virtual void typecheck_spec_assigns_condition(exprt &condition);
+  virtual void typecheck_spec_assigns_target(exprt &target);
   virtual void typecheck_spec_loop_invariant(codet &code);
   virtual void typecheck_spec_decreases(codet &code);
 

src/ansi-c/c_typecheck_code.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_typecheck_base.h"
 
+#include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_util.h>
@@ -842,35 +843,158 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
   }
 }
 
+void c_typecheck_baset::typecheck_spec_assigns_condition(exprt &condition)
+{
+  // compute type
+  typecheck_expr(condition);
+
+  // non-fatal warnings
+  if(has_subexpr(condition, [&](const exprt &subexpr) {
+       return can_cast_expr<side_effect_expr_function_callt>(subexpr);
+     }))
+  {
+    // Remark: we allow function calls without further checks for now because
+    // they are mandatory for some applications.
+    // The next step must be to check that the called functions have a contract
+    // with an empty assigns clause and that they indeed satisfy their contract
+    // using a CI check.
+    warning().source_location = condition.source_location();
+    warning()
+      << "function with possible side-effect called in target's condition"
+      << eom;
+  }
+
+  // fatal errors
+  bool must_throw = false;
+
+  if(condition.type().id() == ID_empty)
+  {
+    must_throw = true;
+    error().source_location = condition.source_location();
+    error() << "void-typed expressions not allowed as assigns clause conditions"
+            << eom;
+  }
+
+  if(has_subexpr(condition, [&](const exprt &subexpr) {
+       return can_cast_expr<side_effect_exprt>(subexpr) &&
+              !can_cast_expr<side_effect_expr_function_callt>(subexpr);
+     }))
+  {
+    must_throw = true;
+    error().source_location = condition.source_location();
+    error() << "side-effects not allowed in assigns clause conditions" << eom;
+  }
+
+  if(has_subexpr(condition, ID_if))
+  {
+    must_throw = true;
+    error().source_location = condition.source_location();
+    error() << "ternary expressions not allowed in assigns "
+               "clause conditions"
+            << eom;
+  }
+
+  if(must_throw)
+    throw 0;
+}
+
+void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target)
+{
+  // compute type
+  typecheck_expr(target);
+
+  // fatal errors
+  bool must_throw = false;
+  if(target.type().id() == ID_empty)
+  {
+    must_throw = true;
+    error().source_location = target.source_location();
+    error() << "void-typed expressions not allowed as assigns clause targets"
+            << eom;
+  }
+
+  if(!target.get_bool(ID_C_lvalue) && target.id() != ID_pointer_object)
+  {
+    must_throw = true;
+    error().source_location = target.source_location();
+    error() << "assigns clause target must be an lvalue or "
+               "__CPROVER_POINTER_OBJECT expression"
+            << eom;
+  }
+
+  // Remark: an expression can be an lvalue and still contain side effects
+  // or ternary expressions. We detect them in a second step.
+  if(has_subexpr(target, ID_side_effect))
+  {
+    must_throw = true;
+    error().source_location = target.source_location();
+    error() << "side-effects not allowed in assigns clause targets" << eom;
+  }
+
+  if(has_subexpr(target, ID_if))
+  {
+    must_throw = true;
+    error().source_location = target.source_location();
+    error() << "ternary expressions not allowed in assigns "
+               "clause targets"
+            << eom;
+  }
+
+  if(must_throw)
+    throw 0;
+}
+
 void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets)
 {
+  exprt::operandst tmp;
   for(auto &target : targets)
   {
-    typecheck_expr(target);
-
-    if(target.type().id() == ID_empty)
+    // conditional target
+    if(target.id() == ID_conditional_assigns_target)
     {
-      error().source_location = target.source_location();
-      error() << "void-typed targets not permitted in assigns clause" << eom;
-      throw 0;
-    }
-    else if(target.id() == ID_pointer_object)
-    {
-      // skip
-    }
-    else if(!target.get_bool(ID_C_lvalue))
-    {
-      error().source_location = target.source_location();
-      error() << "non-lvalue target in assigns clause" << eom;
-      throw 0;
+      // typecheck condition
+      auto &condition = target.operands().at(0);
+      typecheck_spec_assigns_condition(condition);
+
+      // make it boolean if needed
+      if(!can_cast_type<bool_typet>(condition.type()))
+      {
+        if(can_cast_type<pointer_typet>(condition.type()))
+          condition = notequal_exprt{
+            condition, null_pointer_exprt(to_pointer_type(condition.type()))};
+        else
+          condition =
+            notequal_exprt{condition, from_integer(0, condition.type())};
+      }
+
+      // typecheck target(s)
+      auto &conditional_target = target.operands().at(1);
+      if(conditional_target.id() == ID_expression_list)
+      {
+        // distribute condition over all targets
+        for(auto &each : conditional_target.operands())
+        {
+          typecheck_spec_assigns_target(each);
+          exprt new_target{ID_conditional_assigns_target};
+          new_target.add_to_operands(condition, std::move(each));
+          tmp.push_back(std::move(new_target));
+        }
+      }
+      else
+      {
+        typecheck_spec_assigns_target(conditional_target);
+        tmp.push_back(std::move(target));
+      }
     }
-    else if(has_subexpr(target, ID_side_effect))
+    else // unconditional target
     {
-      error().source_location = target.source_location();
-      error() << "assigns clause is not side-effect free" << eom;
-      throw 0;
+      typecheck_spec_assigns_target(target);
+      tmp.push_back(std::move(target));
     }
   }
+  targets.clear();
+  for(auto &each : tmp)
+    targets.push_back(std::move(each));
 }
 
 void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)