CI tweaks

.github/workflows/proof.yml

@@ -55,13 +55,6 @@ jobs:
         path: ~/.opam
         key: ${{ matrix.version }}
 
-    # - name: Install Cerberus-lib
-    #   run: |
-    #     opam switch ${{ matrix.version }}
-    #     eval $(opam env --switch=${{ matrix.version }})
-    #     opam pin --yes --no-action add cerberus-lib .
-    #     opam install --yes cerberus-lib
-
     - name: Download cvc5 release
       uses: robinraju/release-downloader@v1
       with:
@@ -80,13 +73,7 @@ jobs:
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
         opam pin --yes --no-action add cn .
-        opam install --yes cn ocamlformat.0.27.0
-
-    - name: Check CN code formatting
-      run: |
-        opam switch ${{ matrix.version }}
-        eval $(opam env --switch=${{ matrix.version }})
-        dune build @fmt
+        opam install --yes cn
 
     - name: Checkout cn-tutorial
       uses: actions/checkout@v4

.github/workflows/spec-testing.yml

@@ -32,49 +32,29 @@ jobs:
     - name: System dependencies (ubuntu)
       run: |
         sudo apt-get install build-essential libgmp-dev z3 opam cmake lcov
-        wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key|sudo apt-key add -
-        sudo add-apt-repository "deb http://apt.llvm.org/jammy/ llvm-toolchain-jammy-19 main"
-        sudo add-apt-repository "deb-src http://apt.llvm.org/jammy/ llvm-toolchain-jammy-19 main"
-        sudo apt-get update
-        sudo apt-get install clang-19 clang-format-19
-
-    - name: Check LibCN code formatting
-      run: |
-        find runtime/libcn/ -iname '*.h' -o -iname '*.c' | xargs clang-format-19 --dry-run -Werror
-
-    - name: Check Clang warnings
-      run: |
-        find runtime/libcn/ -iname '*.c' | xargs clang-19 -I runtime/libcn/include/ -fsyntax-only -Werror
 
     - name: Restore OPAM cache
       id: cache-opam-restore
       uses: actions/cache/restore@v4
       with:
         path: ~/.opam
         key: ${{ matrix.version }}
-  
+
     - name: Setup OPAM
       if: steps.cache-opam-restore.outputs.cache-hit != 'true'
       run: |
         opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
         opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
         opam install --deps-only --yes ./cn.opam
-  
+
     - name: Save OPAM cache
       uses: actions/cache/save@v4
       if: steps.cache-opam-restore.outputs.cache-hit != 'true'
       with:
         path: ~/.opam
         key: ${{ matrix.version }}
 
-    # - name: Install Cerberus-lib
-    #   run: |
-    #     opam switch ${{ matrix.version }}
-    #     eval $(opam env --switch=${{ matrix.version }})
-    #     opam pin --yes --no-action add cerberus-lib .
-    #     opam install --yes cerberus-lib
-
     - name: Install CN
       run: |
         opam switch ${{ matrix.version }}
@@ -107,7 +87,7 @@ jobs:
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
         cd tests; ./run-cn-test-gen.sh
-    
+
     - name: Run CN-Seq-Test-Gen CI tests
       run: |
         opam switch ${{ matrix.version }}

.github/workflows/style.yml

@@ -0,0 +1,133 @@
+# Check style of codebase
+name: Style
+
+on:
+  pull_request:
+  push:
+    branches:
+      - main
+
+jobs:
+  ocaml-format:
+    strategy:
+      matrix:
+        version: [4.14.1]
+
+    name: OCamlFormat
+
+    runs-on: ubuntu-22.04
+
+    steps:
+      - name: Checkout CN
+        uses: actions/checkout@v4
+
+      - name: Install OPAM
+        run: sudo apt-get install opam
+
+      - name: Restore OPAM cache
+        id: cache-opam-restore
+        uses: actions/cache/restore@v4
+        with:
+          path: ~/.opam
+          key: ${{ matrix.version }}
+
+      - name: Setup OPAM
+        if: steps.cache-opam-restore.outputs.cache-hit != 'true'
+        run: |
+          opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
+          eval $(opam env --switch=${{ matrix.version }})
+          opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
+          opam install --deps-only --yes ./cn.opam
+
+      - name: Save OPAM cache
+        uses: actions/cache/save@v4
+        if: steps.cache-opam-restore.outputs.cache-hit != 'true'
+        with:
+          path: ~/.opam
+          key: ${{ matrix.version }}
+
+      - name: Install OCamlFormat
+        run: |
+          eval $(opam env --switch=${{ matrix.version }})
+          opam install --yes ocamlformat.0.27.0
+
+      - name: Check CN code formatting
+        run: |
+          eval $(opam env --switch=${{ matrix.version }})
+          dune build @fmt
+
+  clang-format:
+    name: ClangFormat
+
+    runs-on: ubuntu-22.04
+
+    steps:
+      - name: Checkout CN
+        uses: actions/checkout@v4
+
+      - name: Install ClangFormat
+        run: |
+          wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key|sudo apt-key add -
+          sudo add-apt-repository "deb http://apt.llvm.org/jammy/ llvm-toolchain-jammy-19 main"
+          sudo add-apt-repository "deb-src http://apt.llvm.org/jammy/ llvm-toolchain-jammy-19 main"
+          sudo apt-get update
+          sudo apt-get install clang-format-19
+
+      - name: Check LibCN code formatting
+        run: |
+          find runtime/libcn/ -iname '*.h' -o -iname '*.c' | xargs clang-format-19 --dry-run -Werror
+
+  clang-warnings:
+    name: Clang warnings
+
+    runs-on: ubuntu-22.04
+
+    steps:
+      - name: Checkout CN
+        uses: actions/checkout@v4
+
+      - name: Install Clang
+        run: |
+          wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key|sudo apt-key add -
+          sudo add-apt-repository "deb http://apt.llvm.org/jammy/ llvm-toolchain-jammy-19 main"
+          sudo add-apt-repository "deb-src http://apt.llvm.org/jammy/ llvm-toolchain-jammy-19 main"
+          sudo apt-get update
+          sudo apt-get install clang-19
+
+      - name: Check Clang warnings
+        run: |
+          find runtime/libcn/ -iname '*.c' -exec clang-19 -c -I runtime/libcn/include/ -Werror -Wall -o /dev/null {} ';'
+
+  gcc-warnings:
+    name: GCC warnings
+
+    runs-on: ubuntu-24.04
+
+    steps:
+      - name: Checkout CN
+        uses: actions/checkout@v4
+
+      - name: Install GCC
+        run: |
+          sudo add-apt-repository ppa:ubuntu-toolchain-r/test
+          sudo apt-get update
+          sudo apt-get install gcc
+
+      - name: Check GCC warnings
+        run: |
+          find runtime/libcn/ -iname '*.c' -exec gcc -c -I runtime/libcn/include/ -Werror -Wall -o /dev/null {} ';'
+
+  shellcheck:
+    name: ShellCheck
+
+    runs-on: ubuntu-22.04
+
+    steps:
+      - name: Checkout CN
+        uses: actions/checkout@v4
+
+      - name: Install ShellCheck
+        run: sudo apt-get install shellcheck
+
+      - name: Check test scripts
+        run: shellcheck -S error tests/**/*.sh

.gitignore

@@ -1,5 +1,6 @@
-# Dune build directory
+# Build directories
 _build
+_opam
 
 # Dune temporary files
 *.install

runtime/libcn/lib/compile.sh

@@ -2,7 +2,7 @@
 
 FLAGS=""
 if [[ -n "${GITHUB_ACTIONS+isset}" ]]; then
-    FLAGS="-Werror"
+    FLAGS="-Werror -Wall"
 fi
 
 cc ${FLAGS} -I ../../include/ -c -g "$@"

runtime/libcn/src/cn-executable/alloc.c

@@ -248,10 +248,6 @@ static inline uint32_t fl_offset(block_header* fl) {
   return (uintptr_t)fl - (uintptr_t)block_list;
 }
 
-static inline free_block_header* fl_by_offset(uint32_t offset) {
-  return (free_block_header*)((uintptr_t)block_list + offset);
-}
-
 static inline free_block_header* fl_next_free_node(free_block_header* fl) {
   if (fl->next > MAX_BLOCK_INDEX) {
     return NULL;

runtime/libcn/src/cn-executable/utils.c

@@ -291,7 +291,7 @@ void dump_ownership_state() {
   hash_table_iterator it = ht_iterator(cn_ownership_global_ghost_state);
   // cn_printf(CN_LOGGING_INFO, "BEGIN ownership state\n");
   while (ht_next(&it)) {
-    int depth = it.value ? *(int*)it.value : -1;
+    // int depth = it.value ? *(int*)it.value : -1;
     // cn_printf(CN_LOGGING_INFO, "[%#lx] => depth: %d\n", *it.key, depth);
   }
   // cn_printf(CN_LOGGING_INFO, "END\n");

runtime/libcn/src/cn-replicate/shape.c

@@ -180,6 +180,7 @@ static void init_decimal_places() {
       count /= 10;
       log++;
     }
+    decimal_places = log;
   }
 }
 

runtime/libcn/src/cn-testing/alloc.c

@@ -186,8 +186,6 @@ int cn_gen_ownership_check(void* p, size_t sz) {
     return 1;
   }
 
-  int bytes = sz;
-
   struct pointer_data* q =
       (struct pointer_data*)((uintptr_t)ownership_curr - sizeof(struct pointer_data));
   for (; (uintptr_t)q >= (uintptr_t)ownership_buf; q--) {

runtime/libcn/src/cn-testing/rand.c

@@ -293,7 +293,6 @@ void cn_gen_shuffle(void* arr, size_t len, size_t size) {
   // byte size is implementation-defined (6.5.3.4, bullet 2)
   // but `sizeof(char) == 1` is guaranteed.
   char tmp[size];
-  char* p = arr;
 
   for (int i = len - 1; i >= 0; i--) {
     uint8_t j = cn_gen_range_u8(0, i + 1);
@@ -303,17 +302,6 @@ void cn_gen_shuffle(void* arr, size_t len, size_t size) {
   }
 }
 
-static int comp_size_t(const void* x, const void* y) {
-  size_t a = *(const size_t*)x;
-  size_t b = *(const size_t*)y;
-
-  if (a < b)
-    return -1;
-  if (b > a)
-    return 1;
-  return 0;
-}
-
 void cn_gen_split(size_t n, size_t* arr[], size_t len) {
   if (len == 1) {
     *(arr[0]) = n;

runtime/libcn/src/cn-testing/test.c

@@ -178,6 +178,9 @@ size_t cn_gen_compute_size(enum cn_gen_sizing_strategy strategy,
       }
 
       return max_size + 1;
+
+    default:
+      assert(false);
   }
 }
 

tests/cn-test-gen/run-single-test.sh

@@ -62,7 +62,7 @@ for ALT_CONFIG in "${ALT_CONFIGS[@]}"; do
     fi
   elif [[ $TEST == *.fail.c ]]; then
     CLEANUP="rm -rf ${DIR} run_tests.sh;separator"
-    $CN test "$TEST" --output-dir="$DIR" $FULL_CONFIG >/dev/null 2>/dev/null
+    $CN test "$TEST" --output-dir="$DIR" "$FULL_CONFIG" >/dev/null 2>/dev/null
     RET=$?
     if [[ "$RET" = 0 ]]; then
       OUTPUT="${OUTPUT}\n$TEST -- Tests passed unexpectedly\n"

tests/run-cn-test-gen.sh

@@ -1,5 +1,5 @@
 #!/bin/bash
 
-cd cn-test-gen
+cd cn-test-gen || exit 1
 
 make -j

tests/run-cn-tutorial-ci.sh

@@ -14,7 +14,7 @@ CN=$OPAM_SWITCH_PREFIX/bin/cn
 
 HERE=$(pwd)
 
-cd "$TUTORIAL_PATH"
+cd "$TUTORIAL_PATH" || exit 1
 
 FAILURE=0
 
@@ -24,7 +24,7 @@ make check CN_PATH="$CN verify --solver-type=cvc5"
 make check CN_PATH="$CN verify --solver-type=z3"
 ((FAILURE+=$?))
 
-cd $HERE
+cd "$HERE" || exit 1
 
 if [ $FAILURE == 0 ]
 then

tests/run-cn-vip.sh

@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -euo pipefail -o noclobber
 
-for file in "$(dirname $0)"/cn_vip_testsuite/*.json
+for file in "$(dirname "$0")"/cn_vip_testsuite/*.json
 do
     ./tests/diff-prog.py cn "$file" 2> "${file%.json}.patch" || (cat "${file%.json}.patch"; exit 1)
 done || exit 1

tests/run-cn.sh

@@ -37,12 +37,12 @@ function exits_with_code() {
   local file=$2
   local -a expected_exit_codes=$3
 
-  printf "[$file]...\n"
-  timeout 60 ${action} "$file"
+  printf "[%s]...\n" "$file"
+  timeout 60 "${action}" "$file"
   local result=$?
 
   for code in "${expected_exit_codes[@]}"; do
-    if [ $result -eq $code ]; then
+    if [ $result -eq "$code" ]; then
       printf "\033[32mPASS\033[0m\n"
       return 0
     fi