Function contracts: preliminary support for guarded assigns clause targets.

- We add a guard expression to the internal representation
  of assigns clause targets, The validity condition expression
  of a target becomes `guard && all_deref_valid(target) && rw_ok(target, size)`.
- We add support for targets of the form `__CPROVER_POINTER_OBJECT(guard ? target : NULL)`
- We take care of removing any side effects still left in the guard.

Author: Remi Delmas

regression/contracts/aaa-assigns_enforce_guarded_assigns_targets/main.c

@@ -0,0 +1,106 @@
+#include <stdbool.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+typedef struct CTX
+{
+  int data[16];
+} CTX;
+
+union low_level_t {
+  CTX md5;
+};
+
+typedef struct HIGH_LEVEL_MD
+{
+  unsigned long flags;
+} HIGH_LEVEL_MD;
+
+typedef struct HIGH_LEVEL_MD_CTX
+{
+  HIGH_LEVEL_MD *digest;
+  unsigned long flags;
+} HIGH_LEVEL_MD_CTX;
+
+struct high_level_digest_t
+{
+  HIGH_LEVEL_MD_CTX *ctx;
+};
+
+struct high_level_t
+{
+  struct high_level_digest_t first;
+  struct high_level_digest_t second;
+};
+
+typedef struct state_t
+{
+  union {
+    union low_level_t low_level;
+    struct high_level_t high_level;
+  } digest;
+} state_t;
+
+bool nondet_bool();
+
+bool is_high_level()
+{
+  static bool latch = false;
+  static bool once = false;
+  if(!once)
+  {
+    latch = nondet_bool();
+    once = true;
+  }
+  return latch;
+}
+
+bool assign_second()
+{
+  static bool latch = false;
+  static bool once = false;
+  if(!once)
+  {
+    latch = nondet_bool();
+    once = true;
+  }
+  return latch;
+}
+
+int update(state_t *state)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(state, sizeof(*state)))
+__CPROVER_requires(
+  is_high_level() ==> 
+  __CPROVER_is_fresh(state->digest.high_level.first.ctx, 
+            sizeof(*(state->digest.high_level.first.ctx))) &&
+  __CPROVER_is_fresh(state->digest.high_level.first.ctx->digest, 
+            sizeof(*(state->digest.high_level.first.ctx->digest))) &&
+  __CPROVER_is_fresh(state->digest.high_level.second.ctx, 
+            sizeof(*(state->digest.high_level.second.ctx))) &&
+  __CPROVER_is_fresh(state->digest.high_level.second.ctx->digest, 
+            sizeof(*(state->digest.high_level.second.ctx->digest)))
+)
+__CPROVER_assigns(
+  __CPROVER_POINTER_OBJECT(is_high_level() ? state->digest.high_level.first.ctx->digest : NULL),
+  state->digest.high_level.first.ctx->flags,
+  state->digest.high_level.second.ctx->flags
+)
+// clang-format on
+{
+  if(is_high_level())
+  {
+    __CPROVER_havoc_object(state->digest.high_level.first.ctx->digest);
+    __CPROVER_havoc_object(state->digest.high_level.second.ctx->digest);
+    state->digest.high_level.first.ctx->flags = 0;
+    state->digest.high_level.second.ctx->flags = 0;
+  }
+  return 0;
+}
+
+int main()
+{
+  state_t *state;
+  update(state);
+  return 0;
+}

regression/contracts/aaa-assigns_enforce_guarded_assigns_targets/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-contract update _ --pointer-check --pointer-overflow-check --signed-overflow-check --unsigned-overflow-check --conversion-check
+^\[update.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: SUCCESS
+^\[update.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Tests that guarded assignments to whole objects are supported 
+using the notation __CPROVER_POINTER_OBJECT(guard ? target : NULL).

src/goto-instrument/contracts/assigns.cpp

@@ -18,11 +18,29 @@ Date: July 2021
 
 #include <langapi/language_util.h>
 
+#include <goto-programs/goto_convert_class.h>
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 
+/// Allows to clean expressions of side effects.
+class cleanert : public goto_convertt
+{
+public:
+  cleanert(
+    symbol_table_baset &_symbol_table,
+    message_handlert &_message_handler)
+    : goto_convertt(_symbol_table, _message_handler)
+  {
+  }
+
+  void clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
+  {
+    goto_convertt::clean_expr(guard, dest, mode, true);
+  }
+};
+
 static const slicet normalize_to_slice(const exprt &expr, const namespacet &ns)
 {
   // FIXME: Refactor these checks out to a common function that can be
@@ -52,6 +70,98 @@ 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>>;
+
+/// Matches an expression with ID_NULL or  ID_constant and value "0",
+/// modulo some intermediate ID_typecasts
+bool match_NULL_or_zero(const exprt &expr)
+{
+  if(expr.id() == ID_typecast)
+    return match_NULL_or_zero(expr.operands().front());
+  else
+    return expr.id() == ID_NULL ||
+           (expr.id() == ID_constant &&
+            id2string(to_constant_expr(expr).get_value()) == "0");
+}
+
+/// Matches an expression of the form `guard ? target : (NULL|0)`
+/// modulo intermediary typecasts.
+/// \param expr the candidate expression
+/// \returns A pair `(guard,target)` if successful.
+if_match_resultt match_if(const exprt &expr)
+{
+  if(expr.id() == ID_typecast)
+  {
+    return match_if(expr.operands().front());
+  }
+  else if(expr.id() == ID_if)
+  {
+    if(!match_NULL_or_zero(expr.operands().at(2)))
+      return {};
+
+    return {{expr.operands().at(0), expr.operands().at(1)}};
+  }
+  else
+    return {};
+}
+
+/// Pattern match the given expression for a guarded pattern
+/// and builds guarded_slice expression as follows:
+///
+/// ```
+/// case expr of
+///  | guard ? target : NULL ->
+///          {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 ->
+///          {true,
+///           expr,
+///           address_of{expr},
+///           object_size{expr}}
+/// ```
+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);
+      goto_programt empty_program;
+      return {true_exprt{}, expr, slice.first, slice.second};
+    }
+  }
+
+  if_match_resultt match_opt = match_if(expr);
+  if(match_opt.has_value())
+  {
+    const auto &match = match_opt.value();
+    const auto &slice = normalize_to_slice(match.second, ns);
+    return {match.first, match.second, slice.first, slice.second};
+  }
+  else
+  {
+    const auto &slice = normalize_to_slice(expr, ns);
+    return {true_exprt{}, expr, slice.first, slice.second};
+  }
+}
+
 const symbolt assigns_clauset::conditional_address_ranget::generate_new_symbol(
   const std::string &prefix,
   const typet &type,
@@ -71,15 +181,19 @@ assigns_clauset::conditional_address_ranget::conditional_address_ranget(
   : source_expr(expr),
     location(expr.source_location()),
     parent(parent),
-    slice(normalize_to_slice(expr, parent.ns)),
+    guarded_slice(normalize_to_guarded_slice(expr, parent.ns)),
     validity_condition_var(
       generate_new_symbol("__car_valid", bool_typet(), location).symbol_expr()),
-    lower_bound_address_var(
-      generate_new_symbol("__car_lb", slice.first.type(), location)
-        .symbol_expr()),
-    upper_bound_address_var(
-      generate_new_symbol("__car_ub", slice.first.type(), location)
-        .symbol_expr())
+    lower_bound_address_var(generate_new_symbol(
+                              "__car_lb",
+                              guarded_slice.start_adress.type(),
+                              location)
+                              .symbol_expr()),
+    upper_bound_address_var(generate_new_symbol(
+                              "__car_ub",
+                              guarded_slice.start_adress.type(),
+                              location)
+                              .symbol_expr())
 {
 }
 
@@ -93,6 +207,17 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
   source_locationt location_no_checks = location;
   disable_pointer_checks(location_no_checks);
 
+  null_message_handlert null_handler;
+
+  // clean up side effects from the guard expression
+  // we want checks on the guard evaluation instructions because it is user code
+  cleanert cleaner(parent.symbol_table, null_handler);
+  exprt clean_guard(guarded_slice.guard);
+  const auto &mode = parent.symbol_table.lookup_ref(parent.function_name).mode;
+  cleaner.clean(clean_guard, instructions, mode);
+  for(auto &inst : instructions.instructions)
+    inst.source_location_nonconst() = location;
+
   instructions.add(
     goto_programt::make_decl(validity_condition_var, location_no_checks));
   instructions.add(
@@ -102,28 +227,30 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
 
   instructions.add(goto_programt::make_assignment(
     lower_bound_address_var,
-    null_pointer_exprt{to_pointer_type(slice.first.type())},
+    null_pointer_exprt{to_pointer_type(guarded_slice.start_adress.type())},
     location_no_checks));
   instructions.add(goto_programt::make_assignment(
     upper_bound_address_var,
-    null_pointer_exprt{to_pointer_type(slice.first.type())},
+    null_pointer_exprt{to_pointer_type(guarded_slice.start_adress.type())},
     location_no_checks));
 
   goto_programt skip_program;
   const auto skip_target =
     skip_program.add(goto_programt::make_skip(location_no_checks));
 
   const auto validity_check_expr =
-    and_exprt{all_dereferences_are_valid(source_expr, parent.ns),
-              w_ok_exprt{slice.first, slice.second}};
+    and_exprt{clean_guard,
+              all_dereferences_are_valid(guarded_slice.expr, parent.ns),
+              w_ok_exprt{guarded_slice.start_adress, guarded_slice.size}};
+
   instructions.add(goto_programt::make_assignment(
     validity_condition_var, validity_check_expr, location_no_checks));
 
   instructions.add(goto_programt::make_goto(
     skip_target, not_exprt{validity_condition_var}, location_no_checks));
 
   instructions.add(goto_programt::make_assignment(
-    lower_bound_address_var, slice.first, location_no_checks));
+    lower_bound_address_var, guarded_slice.start_adress, location_no_checks));
 
   // the computation of the CAR upper bound can overflow into the object ID bits
   // of the pointer with very large allocation sizes.
@@ -133,7 +260,7 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
 
   instructions.add(goto_programt::make_assignment(
     upper_bound_address_var,
-    plus_exprt{slice.first, slice.second},
+    plus_exprt{guarded_slice.start_adress, guarded_slice.size},
     location_overflow_check));
   instructions.destructive_append(skip_program);
 

src/goto-instrument/contracts/assigns.h

@@ -22,6 +22,27 @@ Date: July 2021
 
 typedef std::pair<const exprt, const exprt> slicet;
 
+/// A guarded slice of memory
+typedef struct guarded_slicet
+{
+  guarded_slicet(exprt _guard, exprt _expr, exprt _start_address, exprt _size)
+    : guard(_guard), expr(_expr), start_adress(_start_address), size(_size)
+  {
+  }
+
+  /// Guard expression (may contain side effects)
+  const exprt guard;
+
+  /// Target expression
+  const exprt expr;
+
+  /// Start address of the target
+  const exprt start_adress;
+
+  /// Size of the target
+  const exprt size;
+} guarded_slicet;
+
 /// \brief A class for representing assigns clauses in code contracts
 class assigns_clauset
 {
@@ -56,7 +77,7 @@ class assigns_clauset
     const source_locationt &location;
     const assigns_clauset &parent;
 
-    const slicet slice;
+    const guarded_slicet guarded_slice;
     const symbol_exprt validity_condition_var;
     const symbol_exprt lower_bound_address_var;
     const symbol_exprt upper_bound_address_var;
@@ -78,11 +99,11 @@ class assigns_clauset
       write_sett;
 
   assigns_clauset(
-    const exprt::operandst &,
-    const messaget &,
-    const namespacet &,
-    const irep_idt &,
-    symbol_tablet &);
+    const exprt::operandst &assigns,
+    const messaget &log,
+    const namespacet &ns,
+    const irep_idt &function_name,
+    symbol_tablet &symbol_table);
 
   write_sett::const_iterator add_to_write_set(const exprt &);
   void remove_from_write_set(const exprt &);