Full implementation of loop variants

Author: Long Pham

regression/contracts/invar_check_multiple_loops/test.desc

@@ -5,8 +5,10 @@ main.c
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.3\] .* Check loop invariant before entry: SUCCESS$
-^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.3\] .* Compare the old and new variant values: SUCCESS$
+^\[main.4\] .* Check loop invariant before entry: SUCCESS$
+^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.6\] .* Compare the old and new variant values: SUCCESS$
 ^\[main.assertion.1\] .* assertion x == y \+ 2 \* n: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --

regression/contracts/invar_check_nested_loops/main.c

@@ -7,7 +7,7 @@ int main()
 
   for(int i = 0; i < n; ++i)
     // clang-format off
-    __CPROVER_loop_invariant(i <= n && s == i)
+    __CPROVER_loop_invariant(0 <= i && i <= n && s == i)
     __CPROVER_decreases(n - i)
     // clang-format on
     {

regression/contracts/invar_check_nested_loops/test.desc

@@ -4,9 +4,11 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.6\] .* Compare the old and new variant values: SUCCESS$
 ^\[main.2\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.3\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.4\] .* Compare the old and new variant values: SUCCESS$
 ^\[main.assertion.1\] .* assertion s == n: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --

regression/contracts/variant_function_call_fail/main.c

@@ -0,0 +1,21 @@
+#define N 10
+
+int foo(int i); 
+
+int main() 
+{
+  int i = 0; 
+  while (i != N)
+    __CPROVER_loop_invariant(0 <= i && i <= N)
+    __CPROVER_decreases(foo(i))
+  {
+    i++;
+  }
+
+  return 0; 
+}
+
+int foo(int i) 
+{
+  return N - i;
+}

regression/contracts/variant_function_call_fail/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--apply-loop-contracts
+^Loop variant is not side-effect free. \(at: file main.c line .* function main\)$
+^EXIT=70$
+^SIGNAL=0$
+--
+--
+This test fails because the loop invariant contains a function call. Loop 
+variants must not contain loops, since we want to ensure that the
+calculation of loop variants themselves will terminate. To enforce this
+requirement, for now, we simply ban loop variants from containing function
+calls. In the future, we may allow function calls (but definitely not loops) to
+appear inside loop variants. 

regression/contracts/variant_not_decreasing_fail/main.c

@@ -0,0 +1,14 @@
+
+int main() 
+{
+  int i = 0; 
+  int N = 10; 
+  while (i != N)
+    __CPROVER_loop_invariant(0 <= i && i <= N)
+    __CPROVER_decreases(i)
+  {
+    i++;
+  }
+
+  return 0; 
+}

regression/contracts/variant_not_decreasing_fail/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--apply-loop-contracts
+^main.c function main$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.3\] .* Compare the old and new variant values: FAILURE$
+^.* 1 of 3 failed \(2 iterations\)$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test fails because the loop invariant contains a function call. Loop 
+variants must not contain loops, since we want to ensure that the
+calculation of loop variants themselves will terminate. To enforce this
+requirement, we simply ban loop variants from containing function calls. 
+In the future, we may allow function calls (but definitely not loops) to appear
+inside loop variants. 

regression/contracts/variant_parsing_statement_fail/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 activate-multi-line-match
 ^main.c.*error: syntax error before 'int'\n.*__CPROVER_decreases\(int x = 0\)$
 ^PARSING ERROR$

regression/contracts/variant_parsing_tuple_fail/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 activate-multi-line-match
 ^main.c.*error: syntax error before ','\n.*__CPROVER_decreases\(N - i, 42\)$
 ^PARSING ERROR$

regression/contracts/variant_side_effects_fail/main.c

@@ -0,0 +1,13 @@
+int main() 
+{
+  int i = 0; 
+  int N = 10;
+  while (i != N)
+    __CPROVER_loop_invariant(0 <= i && i <= N)
+    __CPROVER_decreases((N+=0) - i)
+  {
+    i++;
+  }
+
+  return 0; 
+}

regression/contracts/variant_side_effects_fail/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--apply-loop-contracts
+^Loop variant is not side-effect free. \(at: file main.c line .* function main\)$
+^EXIT=70$
+^SIGNAL=0$
+--
+--
+This test fails because the loop invariant contains a side effect, namely
+incrementing variable N and by zero. In this case, although the value of N
+remains unchanged after the increment operation, we read from and write to N. 
+So this constitues a side effect. Loop variants are banned from containing 
+side effects, since loop variants should not modify program states. 

regression/contracts/variant_weak_invariant_fail/main.c

@@ -0,0 +1,14 @@
+
+int main() 
+{
+  int i = 0; 
+  int N = 10; 
+  while (i != N)
+    __CPROVER_loop_invariant(i <= N)
+    __CPROVER_decreases(N - i)
+  {
+    i++;
+  }
+
+  return 0; 
+}

regression/contracts/variant_weak_invariant_fail/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--apply-loop-contracts
+^main.c function main$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.3\] .* Compare the old and new variant values: FAILURE$
+^.* 1 of 3 failed \(2 iterations\)$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test fails because the loop invariant is not strong enough. We 
+additionally need 0 <= i in the loop invariant. 

regression/contracts/variant_while_true_pass/main.c

@@ -0,0 +1,15 @@
+
+int main() 
+{
+  int i = 0; 
+  int N = 10; 
+  while (1 == 1)
+    __CPROVER_loop_invariant(0 <= i && i <= N)
+    __CPROVER_decreases(N - i)
+  {
+    if (i == 10) {break;}    
+    i++;
+  }
+
+  return 0; 
+}

regression/contracts/variant_while_true_pass/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--apply-loop-contracts
+^main.c function main$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.3\] .* Compare the old and new variant values: SUCCESS$
+^.*0 of 3 failed \(1 iterations\)$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test succeeds. The purpose of this test is to check whether a loop variant
+can successfully prove the termination of a loop (i) whose exit condition
+is 1 == 1 (i.e. true) and (ii) that will eventually exit via a break statement. 

src/goto-instrument/code_contracts.cpp

@@ -112,8 +112,9 @@ exprt get_size(const typet &type, const namespacet &ns, messaget &log)
   return result;
 }
 
-void code_contractst::check_apply_invariants(
+void code_contractst::check_apply_invariants_and_decreases(
   goto_functionst::goto_functiont &goto_function,
+  const irep_idt &function_name, 
   const local_may_aliast &local_may_alias,
   const goto_programt::targett loop_head,
   const loopt &loop,
@@ -129,11 +130,18 @@ void code_contractst::check_apply_invariants(
       t->location_number > loop_end->location_number)
       loop_end = t;
 
-  // see whether we have an invariant
+  // see whether we have an invariant and a variant
   exprt invariant = static_cast<const exprt &>(
     loop_end->get_condition().find(ID_C_spec_loop_invariant));
-  if(invariant.is_nil())
-    return;
+  exprt variant = static_cast<const exprt &>(
+    loop_end->get_condition().find(ID_C_spec_decreases));
+  if(invariant.is_nil()) 
+  {
+    if (variant.is_nil())
+      return;
+    else 
+      invariant = true_exprt(); // The Boolean true expression
+  }
 
   // change
   //   H: loop;
@@ -142,9 +150,12 @@ void code_contractst::check_apply_invariants(
   //   H: assert(invariant);
   //   havoc;
   //   assume(invariant);
+  //   old_variant = variant(current_environment);
   //   if(guard) goto E:
   //   loop;
+  //   new_variant = variant(current_environment);
   //   assert(invariant);
+  //   assert(new_variant < old_variant); 
   //   assume(false);
   //   E: ...
 
@@ -188,6 +199,27 @@ void code_contractst::check_apply_invariants(
     converter.goto_convert(assumption, havoc_code, mode);
   }
 
+  // Temproary variables that store the variant before and after the loop
+  symbol_exprt old_variant_symbol = new_tmp_symbol(variant.type(), loop_head->source_location, function_name, mode).symbol_expr();
+  symbol_exprt new_variant_symbol = new_tmp_symbol(variant.type(), loop_head->source_location, function_name, mode).symbol_expr();
+  
+  if (!variant.is_nil())
+  {
+    // Generate: a declaration of the temporary variable that stores the loop
+    // variant before the loop entry
+    havoc_code.add(goto_programt::make_decl(old_variant_symbol, loop_head->source_location));
+
+    // Generate: an assignment to store the loop variant before the loop entry
+    // We would like to set a comment associated with a source location. 
+    // However, we have already used loop_head->source_location to set a
+    // comment. Furthermore, the third argument of make_assignment is passed by
+    // reference rather than by value. Therefore, it is necessary to clone 
+    // loop_head->source_location. 
+    source_locationt declaration_old_variant_source_location {loop_head->source_location};
+    havoc_code.add(goto_programt::make_assignment(old_variant_symbol, variant, declaration_old_variant_source_location));
+    havoc_code.instructions.back().source_location.set_comment("Evaluate and store the loop variant before the loop");
+  }
+
   // non-deterministically skip the loop if it is a do-while loop
   if(!loop_head->is_goto())
   {
@@ -209,11 +241,35 @@ void code_contractst::check_apply_invariants(
     converter.goto_convert(assertion, havoc_code, mode);
     havoc_code.instructions.back().source_location.set_comment(
       "Check that loop invariant is preserved");
-    auto offset = havoc_code.instructions.size();
-    goto_function.body.insert_before_swap(loop_end, havoc_code);
-    std::advance(loop_end, offset);
   }
 
+  if (!variant.is_nil())
+  {
+    // Generate: a declaration of a temporary variable that stores the variant
+    // after one arbitrary iteration of the loop
+    havoc_code.add(goto_programt::make_decl(new_variant_symbol, loop_head->source_location));
+
+    // Generate: an assignment to store the loop variant after one iteration of
+    // the loop
+    source_locationt declaration_new_variant_source_location {loop_head->source_location}; 
+    havoc_code.add(goto_programt::make_assignment(new_variant_symbol, variant, declaration_new_variant_source_location));
+    havoc_code.instructions.back().source_location.set_comment("Evaluate and store the loop variant after the loop");
+
+    // Generate: assertion that the loop variant after the loop is smaller than
+    // the loop variant before the loop
+    source_locationt assignment_source_location {loop_head->source_location}; 
+    havoc_code.add(goto_programt::make_inequality(new_variant_symbol, old_variant_symbol, assignment_source_location));
+    havoc_code.instructions.back().source_location.set_comment("Compare the old and new variant values");
+
+    // Discartd the temporary variables that store loop variants
+    havoc_code.add(goto_programt::make_dead(old_variant_symbol, loop_head->source_location));
+    havoc_code.add(goto_programt::make_dead(new_variant_symbol, 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);
+
   // change the back edge into assume(false) or assume(guard)
   loop_end->targets.clear();
   loop_end->type=ASSUME;
@@ -558,13 +614,16 @@ void code_contractst::apply_loop_contract(
 
   // Iterate over the (natural) loops in the function,
   // and apply any invariant annotations that we find.
-  for(const auto &loop : natural_loops.loop_map)
-    check_apply_invariants(
+  for(const auto &loop : natural_loops.loop_map) 
+  {
+    check_apply_invariants_and_decreases(
       goto_function,
+      function_name, 
       local_may_alias,
       loop.first,
       loop.second,
       symbol_table.lookup_ref(function_name).mode);
+  }
 }
 
 const symbolt &code_contractst::new_tmp_symbol(

src/goto-instrument/code_contracts.h

@@ -98,12 +98,14 @@ class code_contractst
     const irep_idt &function_id,
     const irep_idt &mode);
 
-  void check_apply_invariants(
+  void check_apply_invariants_and_decreases(
     goto_functionst::goto_functiont &goto_function,
+    const irep_idt &function_name, 
     const local_may_aliast &local_may_alias,
     const goto_programt::targett loop_head,
     const loopt &loop,
     const irep_idt &mode);
+
   const namespacet &get_namespace() const;
 
   // for "helper" classes to update symbol table.

src/goto-instrument/loop_utils.cpp

@@ -116,6 +116,7 @@ void get_modifies_lhs(
     const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
     for(const auto &mod : local_may_alias.get(t, ptr.pointer))
     {
+      if(mod.id() == ID_unknown) continue;
       if(ptr.offset.is_nil())
         modifies.insert(dereference_exprt{mod});
       else