Goto-transcoder action

.github/workflows/goto-transcoder.yml

@@ -0,0 +1,37 @@
+# This workflow executes the supported contracts in goto-transcoder
+
+name: Run GOTO Transcoder (ESBMC)
+on:
+  workflow_dispatch:
+  merge_group:
+  pull_request:
+    branches: [ main ]
+  push:
+    paths:
+      - 'library/**'
+      - '.github/workflows/goto-transcoder.yml'
+      - 'scripts/run-kani.sh'
+      - 'scripts/run-goto-transcoder.sh'
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  verify-rust-std:
+    name: Verify contracts with goto-transcoder
+    runs-on: ubuntu-latest
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      # Step 2: Generate contracts programs
+      - name: Generate contracts
+        run: ./scripts/run-kani.sh --kani-args --keep-temps --only-codegen
+
+      # Step 3: Run goto-transcoder
+      - name: Run goto-transcoder
+        run: ./scripts/run-goto-transcoder.sh

scripts/run-goto-transcoder.sh

@@ -0,0 +1,49 @@
+#!/bin/bash
+
+set -e
+
+##############
+# PARAMETERS #
+##############
+contract_folder=target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps
+supported_regex=checked_unchecked.*.out
+unsupported_regex=neg
+
+goto_transcoder_git=https://github.com/rafaelsamenezes/goto-transcoder
+esbmc_url=https://github.com/esbmc/esbmc/releases/download/nightly-7867f5e5595b9e181cd36eb9155d1905f87ad241/esbmc-linux.zip
+
+##########
+# SCRIPT #
+##########
+
+echo "Checking contracts with goto-transcoder"
+
+if [ ! -d "goto-transcoder" ]; then
+    echo "goto-transcoder not found. Downloading..."
+    git clone $goto_transcoder_git
+    cd goto-transcoder
+    wget $esbmc_url
+    unzip esbmc-linux.zip
+    chmod +x ./linux-release/bin/esbmc
+    cd ..
+fi
+
+ls $contract_folder | grep "$supported_regex" | grep -v .symtab.out > ./goto-transcoder/_contracts.txt
+
+cd goto-transcoder
+while IFS= read -r line; do
+    contract=`echo "$line" | awk '{match($0, /(_RNv.*).out/, arr); print arr[1]}'`
+    echo "Processing: $contract"
+    if [[ -z "$contract" ]]; then
+        continue
+    fi
+    if echo "$contract" | grep -q "$unsupported_regex"; then
+        continue
+    fi
+    echo "Running: goto-transcoder $contract $contract_folder/$line $contract.esbmc.goto"
+    cargo run cbmc2esbmc $contract ../$contract_folder/$line $contract.esbmc.goto
+    ./linux-release/bin/esbmc --binary $contract.esbmc.goto
+done < "_contracts.txt"
+
+rm "_contracts.txt"
+cd ..