Function contracts: improved support for conditional targets in assigns clause checking.

Author: Remi Delmas

src/goto-instrument/contracts/assigns.cpp

@@ -71,86 +71,27 @@ static const slicet normalize_to_slice(const exprt &expr, const namespacet &ns)
   UNREACHABLE;
 }
 
-/// Result type for guarded assigns target pattern matching
-using if_match_resultt = optionalt<std::pair<exprt, exprt>>;
-
-/// \brief Matches an expression with ID_NULL or ID_constant "0".
-/// \param expr The candidate expression.
-/// \returns True iff the match is successful.
-bool match_NULL_or_zero(const exprt &expr)
-{
-  const auto &clean_expr = skip_typecast(expr);
-  // FIXME clean up once #6532 lands.
-  return clean_expr.id() == ID_NULL ||
-         (clean_expr.id() == ID_constant &&
-          id2string(to_constant_expr(clean_expr).get_value()) == "0");
-}
-
-/// \brief Matches an expression of the form `guard ? target : (NULL|0)`
-/// \param expr The candidate expression.
-/// \returns A pair `(guard,target)` iff the match is successful.
-if_match_resultt match_if(const exprt &expr)
-{
-  const auto &clean_expr = skip_typecast(expr);
-  if(clean_expr.id() == ID_if)
-  {
-    const auto &if_expr = to_if_expr(clean_expr);
-    if(!match_NULL_or_zero(if_expr.false_case()))
-      return {};
-
-    return {{if_expr.cond(), if_expr.true_case()}};
-  }
-  else
-    return {};
-}
-
-/// Pattern match the given expression for a guarded pattern
-/// and builds guarded_slice expression as follows:
+/// Normalises a assigns target expression to a guarded slice struct.
 ///
 /// ```
 /// case expr of
-///  | guard ? target : NULL ->
-///          {guard,
+///  | guard ? target ->
+///          {guard
 ///           target,
-///           address_of{target},
-///           size_of_expr{target}}
-///  | __CPROVER_POINTER_OBJECT(guard ? target : NULL) ->
-///          {guard,
-///           __CPROVER_POINTER_OBJECT(target),
-///           address_of{target-offset(target)},
-///           object_size{target}}
-///  | other ->
+///           normalize_to_slice(target)}
+///  | target ->
 ///          {true,
-///           expr,
-///           address_of{expr},
-///           object_size{expr}}
+///           target,
+///           normalize_to_slice(target)}
 /// ```
 static const guarded_slicet
 normalize_to_guarded_slice(const exprt &expr, const namespacet &ns)
 {
-  if(expr.id() == ID_pointer_object)
-  {
-    if_match_resultt match_opt = match_if(expr.operands().at(0));
-    if(match_opt.has_value())
-    {
-      const auto &match = match_opt.value();
-      const auto &new_expr = pointer_object(match.second);
-      const auto slice = normalize_to_slice(new_expr, ns);
-      return {match.first, new_expr, slice.first, slice.second};
-    }
-    else
-    {
-      const auto slice = normalize_to_slice(expr, ns);
-      return {true_exprt{}, expr, slice.first, slice.second};
-    }
-  }
-
-  if_match_resultt match_opt = match_if(expr);
-  if(match_opt.has_value())
+  if(expr.id() == ID_conditional_assigns_target)
   {
-    const auto &match = match_opt.value();
-    const auto slice = normalize_to_slice(match.second, ns);
-    return {match.first, match.second, slice.first, slice.second};
+    const auto &new_expr = expr.operands().at(1);
+    const auto slice = normalize_to_slice(new_expr, ns);
+    return {expr.operands().at(0), new_expr, slice.first, slice.second};
   }
   else
   {

src/goto-instrument/contracts/assigns.h

@@ -30,7 +30,7 @@ typedef struct guarded_slicet
   {
   }
 
-  /// Guard expression (may contain side effects)
+  /// Guard expression (may contain side_effect_exprt expressions)
   const exprt guard;
 
   /// Target expression