Fix evaluation of decreases clause

regression/contracts/variant_init_inside_loop/main.c

@@ -0,0 +1,19 @@
+int main()
+{
+  unsigned start, max;
+  unsigned i = start;
+
+  while(i < max)
+    // clang-format off
+    __CPROVER_loop_invariant(
+      (start > max && i == start) ||
+      (start <= i && i <= max)
+    )
+    __CPROVER_decreases(max - i)
+    // clang-format on
+    {
+      i++;
+    }
+
+  return 0;
+}

regression/contracts/variant_init_inside_loop/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--apply-loop-contracts _ --unsigned-overflow-check
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main.overflow.1\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$
+^\[main.overflow.3\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$
+^\[main.overflow.2\] .* arithmetic overflow on unsigned \+ in i \+ 1u: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test checks that the decreases clause is evaluated only within the loop iteration,
+not outside of it (before the loop guard).
+The `main.overflow.1` check would fail if the decreases clause `(max - i)` is evaluated
+before the loop guard is satisfied. This would occur when `start > max` and therefore
+`i > max` after assuming the invariant.

src/goto-instrument/contracts/contracts.cpp

@@ -38,21 +38,62 @@ Date: February 2016
 // This is used in the implementation of multidimensional decreases clauses.
 static exprt create_lexicographic_less_than(
   const std::vector<symbol_exprt> &lhs,
-  const std::vector<symbol_exprt> &rhs);
+  const std::vector<symbol_exprt> &rhs)
+{
+  PRECONDITION(lhs.size() == rhs.size());
+
+  if(lhs.empty())
+  {
+    return false_exprt();
+  }
 
-exprt get_size(const typet &type, const namespacet &ns, messaget &log)
+  // Store conjunctions of equalities.
+  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
+  // l2, l3>.
+  // Then this vector stores <s1 == l1, s1 == l1 && s2 == l2,
+  // s1 == l1 && s2 == l2 && s3 == l3>.
+  // In fact, the last element is unnecessary, so we do not create it.
+  exprt::operandst equality_conjunctions(lhs.size());
+  equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]);
+  for(size_t i = 1; i < equality_conjunctions.size() - 1; i++)
+  {
+    binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]};
+    equality_conjunctions[i] =
+      and_exprt(equality_conjunctions[i - 1], component_i_equality);
+  }
+
+  // Store inequalities between the i-th components of the input vectors
+  // (i.e. lhs and rhs).
+  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
+  // l2, l3>.
+  // Then this vector stores <s1 < l1, s1 == l1 && s2 < l2, s1 == l1 &&
+  // s2 == l2 && s3 < l3>.
+  exprt::operandst lexicographic_individual_comparisons(lhs.size());
+  lexicographic_individual_comparisons[0] =
+    binary_relation_exprt(lhs[0], ID_lt, rhs[0]);
+  for(size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
+  {
+    binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]};
+    lexicographic_individual_comparisons[i] =
+      and_exprt(equality_conjunctions[i - 1], component_i_less_than);
+  }
+  return disjunction(lexicographic_individual_comparisons);
+}
+
+static void insert_before_swap_and_advance(
+  goto_programt &program,
+  goto_programt::targett &target,
+  goto_programt &payload)
 {
-  auto size_of_opt = size_of_expr(type, ns);
-  CHECK_RETURN(size_of_opt.has_value());
-  exprt result = size_of_opt.value();
-  result.add(ID_C_c_sizeof_type) = type;
-  return result;
+  const auto offset = payload.instructions.size();
+  program.insert_before_swap(target, payload);
+  std::advance(target, offset);
 }
 
 void code_contractst::check_apply_loop_contracts(
   goto_functionst::goto_functiont &goto_function,
   const local_may_aliast &local_may_alias,
-  const goto_programt::targett loop_head,
+  goto_programt::targett loop_head,
   const loopt &loop,
   const irep_idt &mode)
 {
@@ -67,10 +108,11 @@ void code_contractst::check_apply_loop_contracts(
       loop_end = t;
 
   // see whether we have an invariant and a decreases clause
-  exprt invariant = static_cast<const exprt &>(
+  auto invariant = static_cast<const exprt &>(
     loop_end->get_condition().find(ID_C_spec_loop_invariant));
-  exprt decreases_clause = static_cast<const exprt &>(
+  auto decreases_clause = static_cast<const exprt &>(
     loop_end->get_condition().find(ID_C_spec_decreases));
+
   if(invariant.is_nil())
   {
     if(decreases_clause.is_nil())
@@ -92,12 +134,12 @@ void code_contractst::check_apply_loop_contracts(
   }
 
   // Vector representing a (possibly multidimensional) decreases clause
-  const auto decreases_clause_vector = decreases_clause.operands();
+  const auto &decreases_clause_exprs = decreases_clause.operands();
 
   // Temporary variables for storing the multidimensional decreases clause
   // at the start of and end of a loop body
-  std::vector<symbol_exprt> old_temporary_variables;
-  std::vector<symbol_exprt> new_temporary_variables;
+  std::vector<symbol_exprt> old_decreases_vars;
+  std::vector<symbol_exprt> new_decreases_vars;
 
   // change
   //   H: loop;
@@ -106,8 +148,8 @@ void code_contractst::check_apply_loop_contracts(
   //   H: assert(invariant);
   //   havoc;
   //   assume(invariant);
-  //   old_decreases_value = decreases_clause(current_environment);
   //   if(guard) goto E:
+  //   old_decreases_value = decreases_clause(current_environment);
   //   loop;
   //   new_decreases_value = decreases_clause(current_environment);
   //   assert(invariant);
@@ -159,34 +201,19 @@ void code_contractst::check_apply_loop_contracts(
   // decreases clause's value before and after the loop
   for(const auto &clause : decreases_clause.operands())
   {
-    old_temporary_variables.push_back(
+    const auto old_decreases_var =
       new_tmp_symbol(clause.type(), loop_head->source_location, mode)
-        .symbol_expr());
-    new_temporary_variables.push_back(
-      new_tmp_symbol(clause.type(), loop_head->source_location, mode)
-        .symbol_expr());
-  }
-
-  if(!decreases_clause.is_nil())
-  {
-    // Generate: declarations of the temporary variables that stores the
-    // multidimensional decreases clause's value before the loop
-    for(const auto &old_temp_var : old_temporary_variables)
-    {
-      havoc_code.add(
-        goto_programt::make_decl(old_temp_var, loop_head->source_location));
-    }
+        .symbol_expr();
+    havoc_code.add(
+      goto_programt::make_decl(old_decreases_var, loop_head->source_location));
+    old_decreases_vars.push_back(old_decreases_var);
 
-    // Generate: assignments to store the multidimensional decreases clause's
-    // value before the loop
-    for(size_t i = 0; i < old_temporary_variables.size(); i++)
-    {
-      code_assignt old_decreases_assignment{old_temporary_variables[i],
-                                            decreases_clause_vector[i]};
-      old_decreases_assignment.add_source_location() =
-        loop_head->source_location;
-      converter.goto_convert(old_decreases_assignment, havoc_code, mode);
-    }
+    const auto new_decreases_var =
+      new_tmp_symbol(clause.type(), loop_head->source_location, mode)
+        .symbol_expr();
+    havoc_code.add(
+      goto_programt::make_decl(new_decreases_var, loop_head->source_location));
+    new_decreases_vars.push_back(new_decreases_var);
   }
 
   // non-deterministically skip the loop if it is a do-while loop
@@ -199,7 +226,23 @@ void code_contractst::check_apply_loop_contracts(
 
   // Now havoc at the loop head.
   // Use insert_before_swap to preserve jumps to loop head.
-  goto_function.body.insert_before_swap(loop_head, havoc_code);
+  insert_before_swap_and_advance(goto_function.body, loop_head, havoc_code);
+
+  // Generate: assignments to store the multidimensional decreases clause's
+  // value before the loop
+  if(!decreases_clause.is_nil())
+  {
+    for(size_t i = 0; i < old_decreases_vars.size(); i++)
+    {
+      code_assignt old_decreases_assignment{old_decreases_vars[i],
+                                            decreases_clause_exprs[i]};
+      old_decreases_assignment.add_source_location() =
+        loop_head->source_location;
+      converter.goto_convert(old_decreases_assignment, havoc_code, mode);
+    }
+
+    goto_function.body.destructive_insert(std::next(loop_head), havoc_code);
+  }
 
   // Generate: assert(invariant) just after the loop exits
   // We use a block scope to create a temporary assertion,
@@ -212,23 +255,14 @@ void code_contractst::check_apply_loop_contracts(
       "Check that loop invariant is preserved");
   }
 
+  // Generate: assignments to store the multidimensional decreases clause's
+  // value after one iteration of the loop
   if(!decreases_clause.is_nil())
   {
-    // Generate: declarations of temporary variables that stores the
-    // multidimensional decreases clause's value after one arbitrary iteration
-    // of the loop
-    for(const auto &new_temp_var : new_temporary_variables)
+    for(size_t i = 0; i < new_decreases_vars.size(); i++)
     {
-      havoc_code.add(
-        goto_programt::make_decl(new_temp_var, loop_head->source_location));
-    }
-
-    // Generate: assignments to store the multidimensional decreases clause's
-    // value after one iteration of the loop
-    for(size_t i = 0; i < new_temporary_variables.size(); i++)
-    {
-      code_assignt new_decreases_assignment{new_temporary_variables[i],
-                                            decreases_clause_vector[i]};
+      code_assignt new_decreases_assignment{new_decreases_vars[i],
+                                            decreases_clause_exprs[i]};
       new_decreases_assignment.add_source_location() =
         loop_head->source_location;
       converter.goto_convert(new_decreases_assignment, havoc_code, mode);
@@ -237,27 +271,25 @@ void code_contractst::check_apply_loop_contracts(
     // Generate: assertion that the multidimensional decreases clause's value
     // after the loop is smaller than the value before the loop.
     // Here, we use the lexicographic order.
-    code_assertt monotonic_decreasing_assertion{create_lexicographic_less_than(
-      new_temporary_variables, old_temporary_variables)};
+    code_assertt monotonic_decreasing_assertion{
+      create_lexicographic_less_than(new_decreases_vars, old_decreases_vars)};
     monotonic_decreasing_assertion.add_source_location() =
       loop_head->source_location;
     converter.goto_convert(monotonic_decreasing_assertion, havoc_code, mode);
     havoc_code.instructions.back().source_location.set_comment(
       "Check decreases clause on loop iteration");
 
     // Discard the temporary variables that store decreases clause's value
-    for(size_t i = 0; i < old_temporary_variables.size(); i++)
+    for(size_t i = 0; i < old_decreases_vars.size(); i++)
     {
       havoc_code.add(goto_programt::make_dead(
-        old_temporary_variables[i], loop_head->source_location));
+        old_decreases_vars[i], loop_head->source_location));
       havoc_code.add(goto_programt::make_dead(
-        new_temporary_variables[i], loop_head->source_location));
+        new_decreases_vars[i], loop_head->source_location));
     }
   }
 
-  auto offset = havoc_code.instructions.size();
-  goto_function.body.insert_before_swap(loop_end, havoc_code);
-  std::advance(loop_end, offset);
+  insert_before_swap_and_advance(goto_function.body, loop_end, havoc_code);
 
   // change the back edge into assume(false) or assume(guard)
   loop_end->targets.clear();
@@ -268,52 +300,6 @@ void code_contractst::check_apply_loop_contracts(
     loop_end->set_condition(boolean_negate(loop_end->get_condition()));
 }
 
-// Create a lexicographic less-than relation between two tuples of variables.
-// This is used in the implementation of multidimensional decreases clauses.
-static exprt create_lexicographic_less_than(
-  const std::vector<symbol_exprt> &lhs,
-  const std::vector<symbol_exprt> &rhs)
-{
-  PRECONDITION(lhs.size() == rhs.size());
-
-  if(lhs.empty())
-  {
-    return false_exprt();
-  }
-
-  // Store conjunctions of equalities.
-  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
-  // l2, l3>.
-  // Then this vector stores <s1 == l1, s1 == l1 && s2 == l2,
-  // s1 == l1 && s2 == l2 && s3 == l3>.
-  // In fact, the last element is unnecessary, so we do not create it.
-  exprt::operandst equality_conjunctions(lhs.size());
-  equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]);
-  for(unsigned int i = 1; i < equality_conjunctions.size() - 1; i++)
-  {
-    binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]};
-    equality_conjunctions[i] =
-      and_exprt(equality_conjunctions[i - 1], component_i_equality);
-  }
-
-  // Store inequalities between the i-th components of the input vectors
-  // (i.e. lhs and rhs).
-  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
-  // l2, l3>.
-  // Then this vector stores <s1 < l1, s1 == l1 && s2 < l2, s1 == l1 &&
-  // s2 == l2 && s3 < l3>.
-  exprt::operandst lexicographic_individual_comparisons(lhs.size());
-  lexicographic_individual_comparisons[0] =
-    binary_relation_exprt(lhs[0], ID_lt, rhs[0]);
-  for(unsigned int i = 1; i < lexicographic_individual_comparisons.size(); i++)
-  {
-    binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]};
-    lexicographic_individual_comparisons[i] =
-      and_exprt(equality_conjunctions[i - 1], component_i_less_than);
-  }
-  return disjunction(lexicographic_individual_comparisons);
-}
-
 bool code_contractst::has_contract(const irep_idt fun_name)
 {
   const symbolt &function_symbol = ns.lookup(fun_name);

src/goto-instrument/contracts/contracts.h

@@ -123,7 +123,7 @@ class code_contractst
   void check_apply_loop_contracts(
     goto_functionst::goto_functiont &goto_function,
     const local_may_aliast &local_may_alias,
-    const goto_programt::targett loop_head,
+    goto_programt::targett loop_head,
     const loopt &loop,
     const irep_idt &mode);