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 checked_unchecked.*.out

.gitignore

@@ -46,6 +46,9 @@ package-lock.json
 ## Kani
 *.out
 
+## GOTO-Transcoder
+goto-transcoder
+
 
 # Added by cargo
 #

doc/src/tools.md

@@ -12,6 +12,7 @@ please see the [Tool Application](general-rules.md#tool-applications) section.
 | Tool                | CI Status |
 |---------------------|-------|
  | Kani Rust Verifier  | [![Kani](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml)      |
+ | GOTO-Transcoder (ESBMC) | [![GOTO-Transcoder](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml)      |
 
 
 

rust-toolchain.toml

@@ -1,4 +1,4 @@
-# This version should be updated whenever we update the version of the Rust
+f# This version should be updated whenever we update the version of the Rust
 # standard library we currently track.
 
 [toolchain]

scripts/run-goto-transcoder.sh

@@ -0,0 +1,52 @@
+#!/bin/bash
+
+set -e
+
+##############
+# PARAMETERS #
+##############
+contract_folder=target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps
+supported_regex=$1
+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
+    # I expect each line to be similar to 'core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_i8.out'
+    # The entrypoint of the contract would be _RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_i8
+    # So we use awk to extract this name.
+    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 ..