Multidimensional decreases clauses

regression/contracts/variant_missing_invariant_warning/test.desc

@@ -1,11 +1,11 @@
 CORE
 main.c
 --apply-loop-contracts
-activate-multi-line-match
 ^The loop at file main.c line 4 function main does not have a loop invariant, but has a decreases clause. Hence, a default loop invariant \('true'\) is being used.$
 ^\[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$
+^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/contracts/variant_multidimensional_ackermann/main.c

@@ -0,0 +1,40 @@
+#include <stdio.h>
+
+int ackermann(int m, int n);
+
+int main()
+{
+  int m = 3;
+  int n = 5;
+  int result = ackermann(m, n);
+
+  printf("Result of the Ackermann function: %d\n", result);
+  return 0;
+}
+
+int ackermann(int m, int n)
+  // clang-format off
+__CPROVER_requires(0 <= m && 0 <= n)
+__CPROVER_ensures(__CPROVER_return_value >= 0)
+// clang-format on
+{
+  while(m > 0)
+    // clang-format off
+    __CPROVER_loop_invariant(0 <= m && 0 <= n)
+    __CPROVER_decreases(m, n)
+    // clang-format on
+    {
+      if(n == 0)
+      {
+        m--;
+        n = 1;
+      }
+      else
+      {
+        n = ackermann(m, n - 1);
+        m--;
+      }
+    }
+
+  return n + 1;
+}

regression/contracts/variant_multidimensional_ackermann/test.desc

@@ -0,0 +1,34 @@
+CORE
+main.c
+--apply-loop-contracts --replace-all-calls-with-contracts
+^\[precondition.1\] .* Check requires clause: SUCCESS$
+^\[precondition.2\] .* Check requires clause: SUCCESS$
+^\[ackermann.1\] .* Check loop invariant before entry: SUCCESS$
+^\[ackermann.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[ackermann.3\] .* Check decreases clause on loop iteration: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+It tests whether we can prove (only partially) the termination of the Ackermann
+function using a multidimensional decreases clause. 
+
+Note that this particular implementation of the Ackermann function contains
+both a while-loop and recursion. Therefore, to fully prove the termination of 
+the Ackermann function, we must prove both 
+(i) the termination of the while-loop and
+(ii) the termination of the recursion. 
+Because CBMC does not support termination proofs of recursions (yet), we cannot
+prove the latter, but the former. Hence, the termination proof in the code is
+only "partial."
+
+Furthermore, the Ackermann function has a function contract that the result
+is always non-negative. This post-condition is necessary for establishing
+the loop invariant. However, in this test, we do not enforce the function
+contract. Instead, we assume that the function contract is correct and use it
+(i.e. replace a recursive call of the Ackermann function with its contract). 
+
+We cannot verify/enforce the function contract of the Ackermann function, since
+CBMC does not support function contracts for recursively defined functions.
+As of now, CBMC only supports function contracts for non-recursive functions. 

regression/contracts/variant_multidimensional_not_decreasing_fail1/main.c

@@ -0,0 +1,22 @@
+int main()
+{
+  int i = 0;
+  int j = 0;
+  int N = 10;
+  while(i < N)
+    // clang-format off
+    __CPROVER_loop_invariant(0 <= i && i <= N && 0 <= j && j <= N)
+    __CPROVER_decreases(N - i, j)
+    // clang-format on
+    {
+      if(j < N)
+      {
+        j++;
+      }
+      else
+      {
+        i++;
+        j = 0;
+      }
+    }
+}

regression/contracts/variant_multidimensional_not_decreasing_fail1/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--apply-loop-contracts
+^\[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: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test fails because the given multidimensional decreases clause does not 
+monotonically decrease. A mistake is in the second component of the
+decreases clause: j. It should instead be N - j. 

regression/contracts/variant_multidimensional_not_decreasing_fail2/main.c

@@ -0,0 +1,22 @@
+int main()
+{
+  int i = 0;
+  int j = 0;
+  int N = 10;
+  while(i < N)
+    // clang-format off
+    __CPROVER_loop_invariant(0 <= i && i <= N && 0 <= j && j <= N)
+    __CPROVER_decreases(i, N - j)
+    // clang-format on
+    {
+      if(j < N)
+      {
+        j++;
+      }
+      else
+      {
+        i++;
+        j = 0;
+      }
+    }
+}

regression/contracts/variant_multidimensional_not_decreasing_fail2/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--apply-loop-contracts
+^\[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: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test fails because the given multidimensional decreases clause does not 
+monotonically decrease. A mistake is in the first component of the
+decreases clause: i. It should instead be N - i. 

regression/contracts/variant_multidimensional_two_index_variables/main.c

@@ -0,0 +1,22 @@
+int main()
+{
+  int i = 0;
+  int j = 0;
+  int N = 10;
+  while(i < N)
+    // clang-format off
+    __CPROVER_loop_invariant(0 <= i && i <= N && 0 <= j && j <= N)
+    __CPROVER_decreases(N - i, N - j)
+    // clang-format on
+    {
+      if(j < N)
+      {
+        j++;
+      }
+      else
+      {
+        i++;
+        j = 0;
+      }
+    }
+}

regression/contracts/variant_multidimensional_two_index_variables/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--apply-loop-contracts
+^\[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$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+It tests whether a multidimensional decreases clause works properly. 

regression/contracts/variant_not_decreasing_fail/test.desc

@@ -1,11 +1,9 @@
 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\] .* Check decreases clause on loop iteration: FAILURE$
-^.* 1 of 3 failed \(2 iterations\)$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts/variant_parsing_tuple_fail/main.c → regression/contracts/variant_parsing_multiple_clauses_fail/main.c

@@ -5,7 +5,8 @@ int main()
   while(i != N)
     // clang-format off
     __CPROVER_loop_invariant(0 <= i && i <= N)
-    __CPROVER_decreases(N - i, 42)
+    __CPROVER_decreases(N - i) 
+    __CPROVER_decreases(42)
     // clang-format on
     {
       i++;

regression/contracts/variant_parsing_multiple_clauses_fail/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--apply-loop-contracts
+activate-multi-line-match
+^main.c.*error: syntax error before '__CPROVER_decreases'\n.*__CPROVER_decreases\(42\)$
+^PARSING ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test fails because we have multiple decreases clauses. CBMC only admits
+one decreases clause for each loop. If one wants to write a multidimensional
+decreases clause, it should be placed inside a single __CPROVER_decreases(...),
+where each component of the multidimensional decreases clause is separated by a
+comma. Hence, in this test, the correct syntax is 
+__CPROVER_decreases(N - i, 42).

regression/contracts/variant_weak_invariant_fail/test.desc

@@ -1,11 +1,9 @@
 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\] .* Check decreases clause on loop iteration: FAILURE$
-^.* 1 of 3 failed \(2 iterations\)$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts/variant_while_true_pass/test.desc

@@ -1,16 +1,14 @@
 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\] .* Check decreases clause on loop iteration: 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 decreases
-clause 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. 
+The purpose of this test is to check whether a decreases clause 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/ansi-c/c_typecheck_code.cpp

@@ -828,9 +828,11 @@ void c_typecheck_baset::typecheck_spec_decreases(codet &code)
 {
   if(code.find(ID_C_spec_decreases).is_not_nil())
   {
-    exprt &variant = static_cast<exprt &>(code.add(ID_C_spec_decreases));
-
-    typecheck_expr(variant);
-    implicit_typecast_arithmetic(variant);
+    for(auto &decreases_clause_component :
+        (static_cast<exprt &>(code.add(ID_C_spec_decreases)).operands()))
+    {
+      typecheck_expr(decreases_clause_component);
+      implicit_typecast_arithmetic(decreases_clause_component);
+    }
   }
 }

src/ansi-c/parser.y

@@ -509,10 +509,17 @@ cprover_contract_loop_invariant_list_opt:
         | cprover_contract_loop_invariant_list
         ;
 
+ACSL_binding_expression_list:
+          ACSL_binding_expression
+        { init($$); mto($$, $1); }
+        | ACSL_binding_expression_list ',' ACSL_binding_expression
+        { $$=$1; mto($$, $3); }
+        ;
+
 cprover_contract_decreases_opt:
         /* nothing */
         { init($$); parser_stack($$).make_nil(); }
-        | TOK_CPROVER_DECREASES '(' ACSL_binding_expression ')'
+        | TOK_CPROVER_DECREASES '(' ACSL_binding_expression_list ')'
         { $$=$3; }
         ;
 
@@ -2449,8 +2456,8 @@ iteration_statement:
           if(!parser_stack($6).operands().empty())
             static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($6).operands());
 
-          if(parser_stack($7).is_not_nil())
-            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($7));
+          if(!parser_stack($7).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($7).operands());
         }
         | TOK_DO statement TOK_WHILE '(' comma_expression ')'
           cprover_contract_assigns_opt
@@ -2464,8 +2471,8 @@ iteration_statement:
           if(!parser_stack($8).operands().empty())
             static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($8).operands());
 
-          if(parser_stack($9).is_not_nil())
-            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($9));
+          if(!parser_stack($9).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($9).operands());
         }
         | TOK_FOR
           {
@@ -2495,8 +2502,8 @@ iteration_statement:
           if(!parser_stack($10).operands().empty())
             static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($10).operands());
 
-          if(parser_stack($11).is_not_nil())
-            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($11));
+          if(!parser_stack($11).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($11).operands());
 
           if(PARSER.for_has_scope)
             PARSER.pop_scope(); // remove the C99 for-scope