CN: Parallelise and caputure output in CN CI (#703)

* CN: Add Python for running CN tests

This allows us to parallelise some of the testing easily, and also use
diff-based tests rather than just relying on return codes.

* CN: Switch to Python script and diffs

The docker CI uses run-cn.sh so keeping it for now.

* CN: Tidy up lemmma CI

Not enabling it just yet because (a) it's not under active development
and (b) I want to sort out caching first so that rebuilding Cerberus
and opam don't eat up any savings from parallelising.

* Generalise test script

The test script now requires a (JSON) config file with documented
attributes, and does not default to a test directory or executable.
It also includes a `--dry-run` flag to see what command is being run.

* CN: Use Python for running CN VIP tests

* Swap order of args in diff-prog

.github/workflows/ci-cn-spec-testing.yml

@@ -80,5 +80,5 @@ jobs:
       run: |
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
-        cd tests; USE_OPAM='' ./run-cn-test-gen.sh
+        cd tests; ./run-cn-test-gen.sh
 

.github/workflows/ci-cn.yml

@@ -71,28 +71,28 @@ jobs:
       run: |
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
-        USE_OPAM='' cd backend/cn && dune build @fmt
+        cd backend/cn && dune build @fmt
 
     - name: Checkout cn-tutorial
       uses: actions/checkout@v4
       with:
         repository: rems-project/cn-tutorial
         path: cn-tutorial
 
-    - name: Run CN CI tests
+    - name: Run CN tests
       run: |
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
-        cd tests; USE_OPAM='' ./run-cn.sh
+        ./tests/diff-prog.py cn tests/cn/verify.json 2> diff.patch || (cat diff.patch; exit 1)
 
-    - name: Run CN Tutorial CI tests
+    - name: Run CN Tutorial tests
       run: |
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
-        USE_OPAM='' tests/run-cn-tutorial-ci.sh cn-tutorial
+        tests/run-cn-tutorial-ci.sh cn-tutorial
 
-    - name: Run CN VIP CI tests
+    - name: Run CN VIP tests
       run: |
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
-        cd tests; USE_OPAM='' ./run-cn-vip.sh
+        tests/run-cn-vip.sh

.github/workflows/ci-pr-bench.yml.disabled

@@ -90,7 +90,7 @@ jobs:
       run: |
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
-        cd tests; USE_OPAM='' ./run-ci-benchmarks.sh
+        cd tests; ./run-ci-benchmarks.sh
         mv benchmark-data.json ${{ env.PR_DATA }}
         cd ..
 
@@ -117,7 +117,7 @@ jobs:
       run: |
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
-        cd tests; USE_OPAM='' ./run-ci-benchmarks.sh; mv benchmark-data.json ${{ env.BASE_DATA }}
+        cd tests; ./run-ci-benchmarks.sh; mv benchmark-data.json ${{ env.BASE_DATA }}
         cd ..
 
     - name: Compare results

tests/cn/alloc_create.c.verify

@@ -0,0 +1,2 @@
+return code: 0
+[1/1]: main -- pass

tests/cn/alloc_token.c.verify

@@ -0,0 +1 @@
+return code: 0

tests/cn/and_or_precedence.error.c.verify

@@ -0,0 +1,9 @@
+return code: 1
+[1/1]: g1 -- fail
+tests/cn/and_or_precedence.error.c:15:13: error: Unprovable constraint
+        /*@ assert (false); @*/
+            ^~~~~~~~~~~~~~~ 
+Constraint from tests/cn/and_or_precedence.error.c:15:13:
+        /*@ assert (false); @*/
+            ^~~~~~~~~~~~~~~ 
+State file: file:///tmp/state__and_or_precedence.error.c__g1.html

tests/cn/append.c.verify

@@ -0,0 +1,3 @@
+return code: 0
+[1/2]: IntList_append -- pass
+[2/2]: split -- pass

tests/cn/arith_type.error.c.verify

@@ -0,0 +1,8 @@
+return code: 1
+tests/cn/arith_type.error.c:8:21: error: Type error
+ let x = negate() + true;
+                    ^
+Expression 'true' has type 'boolean'.
+I expected it to have type 'integer' because of tests/cn/arith_type.error.c:8:10:
+ let x = negate() + true;
+         ~~~~~~^~ 

tests/cn/arrow_access.c.verify

@@ -0,0 +1,3 @@
+return code: 0
+[1/2]: arrow_access_1 -- pass
+[2/2]: arrow_access_2 -- pass

tests/cn/assert_on_toplevel.error.c.verify

@@ -0,0 +1,5 @@
+return code: 2
+tests/cn/assert_on_toplevel.error.c:2:5: error: unexpected token before 'assert'
+parsing "cn_toplevel'": expected "cn_toplevel"
+    assert @*/
+    ^~~~~~ 

tests/cn/b_or.c.verify

@@ -0,0 +1,2 @@
+return code: 0
+[1/1]: f -- pass

tests/cn/b_xor.c.verify

@@ -0,0 +1,2 @@
+return code: 0
+[1/1]: f -- pass

tests/cn/bad_col.error.c.verify

@@ -0,0 +1,5 @@
+return code: 1
+tests/cn/bad_col.error.c:3:32: error: unexpected token after '+' and before 'function'
+parsing "add_expr": seen "add_expr PLUS", expecting "mul_expr"
+              x < 2147483647 + function; @*/
+                               ^~~~~~~~ 

tests/cn/bad_constructor_user.error.c.verify

@@ -0,0 +1,8 @@
+return code: 1
+tests/cn/bad_constructor_user.error.c:9:19: error: Type error
+    Cons { head : 0, tail : Nil {} }
+                  ^
+Expression '0' has type 'integer'.
+I expected it to have type 'i32' because of tests/cn/bad_constructor_user.error.c:9:5:
+    Cons { head : 0, tail : Nil {} }
+    ~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~ 

tests/cn/bad_function_call.error.c.verify

@@ -0,0 +1,8 @@
+return code: 1
+tests/cn/bad_function_call.error.c:7:12: error: Type error
+    id_int(x)
+           ^
+Expression 'x' has type 'i32'.
+I expected it to have type 'integer' because of tests/cn/bad_function_call.error.c:2:1:
+function (integer) id_int(integer x) {
+^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 

tests/cn/bad_record.error.c.verify

@@ -0,0 +1,4 @@
+return code: 2
+tests/cn/bad_record.error.c:3:43: error: field `x' duplicated
+type_synonym wrong = { integer x, integer x }
+                                          ^

tests/cn/bad_record2.error.c.verify

@@ -0,0 +1,4 @@
+return code: 2
+tests/cn/bad_record2.error.c:6:15: error: field `x' duplicated
+    { x: p.x, x: p.y }
+              ^

tests/cn/bad_recursion.error.c.verify

@@ -0,0 +1,6 @@
+return code: 1
+tests/cn/bad_recursion.error.c:3:1: error: Illegal datatype definition.
+Constructor argument 'b' is given type 'map<u8, datatype bad>', which indirectly refers to 'datatype bad'.
+Indirect recursion via map, set, record, or tuple types is not permitted.
+datatype bad { Bad { map<u8, datatype bad> b } }
+^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 

tests/cn/bad_resource_var.error.c.verify

@@ -0,0 +1,9 @@
+return code: 1
+[1/1]: inc -- fail
+tests/cn/bad_resource_var.error.c:1:1: error: Unprovable constraint
+void inc(int* p)
+~~~~~^~~~~~~~~~~ 
+Constraint from tests/cn/bad_resource_var.error.c:5:13:
+            X2 < 2147483647i32; @*/
+            ^~~~~~~~~~~~~~~~~~~ 
+State file: file:///tmp/state__bad_resource_var.error.c__inc.html

tests/cn/before_from_bytes.error.c.verify

@@ -0,0 +1,13 @@
+return code: 1
+tests/cn/before_from_bytes.error.c:6:9: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
+    /*@ to_bytes Owned<int>(p); @*/
+        ^~~~~~~~ 
+tests/cn/before_from_bytes.error.c:7:9: warning: extract: index added, no resources (yet) extracted.
+    /*@ extract Owned<char>, 2u64; @*/
+        ^~~~~~~~~~~~~~~~~~~~~~~~~~ 
+[1/1]: main -- fail
+tests/cn/before_from_bytes.error.c:8:5: error: Missing resource for writing
+    p_char[2] = 0xff;
+    ~~~~~~~~~~^~~~~~ 
+Resource needed: Block<char>(&&x[(u64)2'i32])
+State file: file:///tmp/state__before_from_bytes.error.c__main.html

tests/cn/before_to_bytes.error.c.verify

@@ -0,0 +1,7 @@
+return code: 1
+[1/1]: main -- fail
+tests/cn/before_to_bytes.error.c:6:5: error: Missing resource for writing
+    p_char[2] = 0xff;
+    ~~~~~~~~~~^~~~~~ 
+Resource needed: Block<char>(&&x[(u64)2'i32])
+State file: file:///tmp/state__before_to_bytes.error.c__main.html

tests/cn/bitwise_and.c.verify

@@ -0,0 +1,2 @@
+return code: 0
+[1/1]: main -- pass

tests/cn/bitwise_and_type_left.error.c.verify

@@ -0,0 +1,5 @@
+return code: 1
+tests/cn/bitwise_and_type_left.error.c:3:17: error: Ill-typed application of binary operation '&' .
+    /*@ assert (0 & 1i32 == 0i32); @*/
+                ~~^~~~~~ 
+'0' has type 'integer', '1'i32' has type 'i32'.

tests/cn/bitwise_and_type_right.error.c.verify

@@ -0,0 +1,8 @@
+return code: 1
+tests/cn/bitwise_and_type_right.error.c:3:24: error: Type error
+    /*@ assert (0i32 & 1 == 0i32); @*/
+                       ^
+Expression '1' has type 'integer'.
+I expected it to have type 'i32' because of tests/cn/bitwise_and_type_right.error.c:3:17:
+    /*@ assert (0i32 & 1 == 0i32); @*/
+                ^

tests/cn/bitwise_compl.c.verify

@@ -0,0 +1,2 @@
+return code: 0
+[1/1]: main -- pass

tests/cn/bitwise_compl_precedence.c.verify

@@ -0,0 +1,2 @@
+return code: 0
+[1/1]: main -- pass

tests/cn/bitwise_compl_type.error.c.verify

@@ -0,0 +1,5 @@
+return code: 1
+tests/cn/bitwise_compl_type.error.c:3:18: error: Mismatched types.
+    /*@ assert (~0 == -1); @*/
+                 ^
+Expected value of type 'bitvector' but found value of type 'integer'

tests/cn/block_type.c.verify

@@ -0,0 +1,3 @@
+return code: 0
+[1/2]: block_notype_1 -- pass
+[2/2]: block_notype_2 -- pass

tests/cn/builtin_ctz.c.verify

@@ -0,0 +1,2 @@
+return code: 0
+[1/1]: f -- pass

tests/cn/builtin_ctz_val.c.verify

@@ -0,0 +1,2 @@
+return code: 0
+[1/1]: f -- pass

tests/cn/cn_inline.c.verify

@@ -0,0 +1,6 @@
+return code: 0
+tests/cn/cn_inline.c:13:5: warning: experimental keyword 'cn_function' (use of experimental features is discouraged)
+/*@ cn_function lookup_size_shift_cn; @*/
+    ^~~~~~~~~~~ 
+[1/2]: lookup_size_shift -- pass
+[2/2]: f -- pass

tests/cn/cnfunction_mismatched_args1.error.c.verify

@@ -0,0 +1,7 @@
+return code: 1
+tests/cn/cnfunction_mismatched_args1.error.c:6:5: warning: experimental keyword 'cn_function' (use of experimental features is discouraged)
+/*@ cn_function bw_or; @*/
+    ^~~~~~~~~~~ 
+tests/cn/cnfunction_mismatched_args1.error.c:5:1: error: mismatched argument number for c_bw_or -> bw_or
+int c_bw_or(int x)
+~~~~^~~~~~~~~~~~~~ 

tests/cn/cnfunction_mismatched_args2.error.c.verify

@@ -0,0 +1,7 @@
+return code: 1
+tests/cn/cnfunction_mismatched_args2.error.c:6:5: warning: experimental keyword 'cn_function' (use of experimental features is discouraged)
+/*@ cn_function bw_or; @*/
+    ^~~~~~~~~~~ 
+tests/cn/cnfunction_mismatched_args2.error.c:5:1: error: mismatched argument number for c_bw_or -> bw_or
+int c_bw_or(int x, int y, int z)
+~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~ 

tests/cn/cnfunction_mismatched_args3.error.c.verify

@@ -0,0 +1,7 @@
+return code: 1
+tests/cn/cnfunction_mismatched_args3.error.c:6:5: warning: experimental keyword 'cn_function' (use of experimental features is discouraged)
+/*@ cn_function bw_or; @*/
+    ^~~~~~~~~~~ 
+tests/cn/cnfunction_mismatched_args3.error.c:5:1: error: mismatched arguments: (u32 y) and (i32 y)
+int c_bw_or(int x, int y)
+~~~~^~~~~~~~~~~~~~~~~~~~~ 

tests/cn/cnfunction_mismatched_args4.error.c.verify

@@ -0,0 +1,8 @@
+return code: 1
+tests/cn/cnfunction_mismatched_args4.error.c:6:5: warning: experimental keyword 'cn_function' (use of experimental features is discouraged)
+/*@ cn_function bw_or; @*/
+    ^~~~~~~~~~~ 
+tests/cn/cnfunction_mismatched_args4.error.c:6:5: error: cn_function: return-type mismatch:
+c_bw_or : i32 -> bw_or : u32
+/*@ cn_function bw_or; @*/
+    ^~~~~~~~~~~~~~~~~~ 

tests/cn/copy_alloc_id.c.verify

@@ -0,0 +1,4 @@
+return code: 0
+[1/3]: f1 -- pass
+[2/3]: f2 -- pass
+[3/3]: main -- pass

tests/cn/copy_alloc_id.error.c.verify

@@ -0,0 +1,8 @@
+return code: 1
+[1/2]: f -- fail
+[2/2]: main -- pass
+tests/cn/copy_alloc_id.error.c:4:12: error: Pointer `p` needs allocation ID
+  int* q = __cerbvar_copy_alloc_id(p_int + 0ULL, p);
+           ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+(UB missing short message): UB_CERB004_unspecified__copy_alloc_id
+State file: file:///tmp/state__copy_alloc_id.error.c__f.html

tests/cn/copy_alloc_id2.error.c.verify

@@ -0,0 +1,8 @@
+return code: 1
+[1/2]: f -- fail
+[2/2]: main -- pass
+tests/cn/copy_alloc_id2.error.c:10:12: error: Pointer `p` needs to be live for copy_alloc_id
+  int* q = __cerbvar_copy_alloc_id(p_int + 0ULL, p);
+           ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+Need an Alloc or Owned in context with same allocation id
+State file: file:///tmp/state__copy_alloc_id2.error.c__f.html

tests/cn/create_rdonly.c.verify

@@ -0,0 +1,2 @@
+return code: 0
+[1/1]: main -- pass

tests/cn/disj_nonnull.c.verify

@@ -0,0 +1,3 @@
+return code: 0
+[1/2]: globals -- pass
+[2/2]: main -- pass

tests/cn/division.c.verify

@@ -0,0 +1,2 @@
+return code: 0
+[1/1]: division -- pass

tests/cn/division_by_0.error.c.verify

@@ -0,0 +1,7 @@
+return code: 1
+[1/1]: division -- fail
+tests/cn/division_by_0.error.c:6:12: error: Undefined behaviour
+    return x / y;
+           ~~^~~ 
+the value of the second operand of a '/' operator is zero (§6.5.5#5, sentence 2)
+State file: file:///tmp/state__division_by_0.error.c__division.html

tests/cn/division_casting.c.verify

@@ -0,0 +1,2 @@
+return code: 0
+[1/1]: division -- pass

tests/cn/division_precedence.c.verify

@@ -0,0 +1,4 @@
+return code: 0
+[1/3]: divide_no_parenthesis -- pass
+[2/3]: multiply_then_divide -- pass
+[3/3]: divide_multiply_add_subtract -- pass

tests/cn/division_return_sign.error.c.verify

@@ -0,0 +1,8 @@
+return code: 1
+tests/cn/division_return_sign.error.c:7:25: error: Type error
+    ensures return == x/y; @*/
+                        ^
+Expression 'y' has type 'u32'.
+I expected it to have type 'i32' because of tests/cn/division_return_sign.error.c:7:23:
+    ensures return == x/y; @*/
+                      ^

tests/cn/division_return_size.error.c.verify

@@ -0,0 +1,7 @@
+return code: 1
+[1/1]: different_size -- fail
+tests/cn/division_return_size.error.c:9:5: error: integer value not representable at type signed int
+    return x / y;
+    ^~~~~~~~~~~~~ 
+Value: (i64)x / y
+State file: file:///tmp/state__division_return_size.error.c__different_size.html

tests/cn/division_with_constants.c.verify

@@ -0,0 +1,4 @@
+return code: 0
+[1/3]: divide_by_ten -- pass
+[2/3]: divide_by_neg_ten -- pass
+[3/3]: division_diff_sign -- pass

tests/cn/doubling.c.verify

@@ -0,0 +1,3 @@
+return code: 0
+[1/2]: add_self -- pass
+[2/2]: add_self_twice -- pass

tests/cn/duplicate_datatype_var.error.c.verify

@@ -0,0 +1,4 @@
+return code: 1
+tests/cn/duplicate_datatype_var.error.c:5:22: error: Re-using member name x within datatype definition.
+    Single { integer x }
+                     ^

tests/cn/duplicate_pattern_var.error.c.verify

@@ -0,0 +1,4 @@
+return code: 2
+tests/cn/duplicate_pattern_var.error.c:15:43: error: redeclaration of variable
+        Cons { head : Point { x : a , y : a } , tail : tail } => { a + b + sum(tail) }
+                                          ^

tests/cn/enum_and_and.c.verify

@@ -0,0 +1,2 @@
+return code: 0
+[1/1]: foo -- pass

tests/cn/extract_verbose.c.verify

@@ -0,0 +1,23 @@
+return code: 0
+tests/cn/extract_verbose.c:10:27: warning: 'extract' expects a 'u64', but '1' with type 'integer' was provided. This will become an error in the future.
+  /*@ extract Owned<int>, 1; @*/
+                          ^
+tests/cn/extract_verbose.c:11:27: warning: 'extract' expects a 'u64', but '1' with type 'integer' was provided. This will become an error in the future.
+  /*@ extract Owned<int>, 1; @*/
+                          ^
+tests/cn/extract_verbose.c:14:27: warning: 'extract' expects a 'u64', but '12' with type 'integer' was provided. This will become an error in the future.
+  /*@ extract Owned<int>, 12; @*/
+                          ^
+tests/cn/extract_verbose.c:10:7: warning: extract: index added, no resources (yet) extracted.
+  /*@ extract Owned<int>, 1; @*/
+      ^~~~~~~~~~~~~~~~~~~~~~ 
+tests/cn/extract_verbose.c:11:7: warning: extract: index added, no resources (yet) extracted.
+  /*@ extract Owned<int>, 1; @*/
+      ^~~~~~~~~~~~~~~~~~~~~~ 
+tests/cn/extract_verbose.c:13:7: warning: extract: index added, no resources (yet) extracted.
+  /*@ extract Owned<int>, 1u64; @*/
+      ^~~~~~~~~~~~~~~~~~~~~~~~~ 
+tests/cn/extract_verbose.c:14:7: warning: extract: index added, no resources (yet) extracted.
+  /*@ extract Owned<int>, 12; @*/
+      ^~~~~~~~~~~~~~~~~~~~~~~ 
+[1/1]: f -- pass

tests/cn/failing_postcond.error.c.verify

@@ -0,0 +1,9 @@
+return code: 1
+[1/1]: inc -- fail
+tests/cn/failing_postcond.error.c:5:5: error: Unprovable constraint
+    return x + 1;
+    ^~~~~~~~~~~~~ 
+Constraint from tests/cn/failing_postcond.error.c:3:13:
+/*@ ensures return < 2147483647i32; @*/
+            ^~~~~~~~~~~~~~~~~~~~~~~ 
+State file: file:///tmp/state__failing_postcond.error.c__inc.html

tests/cn/failing_precond.error.c.verify

@@ -0,0 +1,8 @@
+return code: 1
+tests/cn/failing_precond.error.c:2:18: error: Type error
+/*@ requires x < 2147483647; @*/
+                 ^
+Expression '2147483647' has type 'integer'.
+I expected it to have type 'i32' because of tests/cn/failing_precond.error.c:2:14:
+/*@ requires x < 2147483647; @*/
+             ^

tests/cn/forloop_with_decl.c.verify

@@ -0,0 +1,2 @@
+return code: 0
+[1/1]: for_with_decl -- pass