From bedd2f3255159dacdc9338fee5640f95bb8d9a67 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Sat, 3 Oct 2026 08:46:48 +0100 Subject: [PATCH 1/3] Check contracts with ESBMC's native CBMC goto reader ESBMC 7.10 segfaults reading goto-transcoder's output for contracts built by Kani main (CBMC 6.11). ESBMC v8.5 reads Kani's .out files directly, so drop the transcoder and library.goto, and find the .out files under either Cargo layout (debug/deps or debug/build/PKG/HASH/out). Fixes #708 --- .gitignore | 4 +-- scripts/run-goto-transcoder.sh | 50 ++++++++++++++++++---------------- 2 files changed, 28 insertions(+), 26 deletions(-) diff --git a/.gitignore b/.gitignore index 82d2291fd22b0..a98335bf7c3e4 100644 --- a/.gitignore +++ b/.gitignore @@ -49,8 +49,8 @@ package-lock.json ## Kani *.out -## GOTO-Transcoder -goto-transcoder +## ESBMC +esbmc # Added by cargo # # already existing elements were commented out diff --git a/scripts/run-goto-transcoder.sh b/scripts/run-goto-transcoder.sh index e11a012ed4556..af847284251df 100755 --- a/scripts/run-goto-transcoder.sh +++ b/scripts/run-goto-transcoder.sh @@ -5,48 +5,50 @@ set -e ############## # PARAMETERS # ############## -contract_folder=$1/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps +target=$1/kani_verify_std/target/x86_64-unknown-linux-gnu/debug supported_regex=$2 unsupported_regex=neg -goto_transcoder_git=https://github.com/esbmc/goto-transcoder -esbmc_url=https://github.com/esbmc/esbmc/releases/download/v7.10/esbmc-linux.zip +# ESBMC reads CBMC goto binaries directly since v8.4, so Kani's output needs no conversion. +esbmc_url=https://github.com/esbmc/esbmc/releases/download/v8.5/esbmc-linux.zip +esbmc=esbmc/release/bin/esbmc + +contract_folder=$target/deps +# Cargo 1.99+ gives each package its own debug/build/PKG/HASH/out/ and no longer creates debug/deps. +if [ ! -d "$contract_folder" ]; then + contract_folder=$(find "$target/build" -path '*/out/*.out' | grep "$supported_regex" | head -n 1 | xargs -r dirname) +fi +if [ -z "$contract_folder" ]; then + echo "No contract programs matching '$supported_regex' under $target" + exit 1 +fi ########## # SCRIPT # ########## -echo "Checking contracts with goto-transcoder" +echo "Checking contracts with ESBMC" -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 ./bin/esbmc - cd .. +if [ ! -x "$esbmc" ]; then + echo "ESBMC not found. Downloading..." + mkdir -p esbmc + wget -q -O esbmc/esbmc-linux.zip $esbmc_url + unzip -q -o esbmc/esbmc-linux.zip -d esbmc + chmod +x $esbmc fi -ls $contract_folder | grep "$supported_regex" | grep -v .symtab.out > ./goto-transcoder/_contracts.txt +ls $contract_folder | grep "$supported_regex" | grep -v .symtab.out > _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 + [[ $line =~ (_RNv.*)\.out$ ]] || continue + contract=${BASH_REMATCH[1]} 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_folder/$line $contract.esbmc.goto - ./bin/esbmc --cprover --function $contract --binary resources/library.goto $contract.esbmc.goto + echo "Processing: $contract" + $esbmc --binary $contract_folder/$line --function $contract done < "_contracts.txt" rm "_contracts.txt" -cd .. From c489d636e9a53cb7c865f04cff0376203700c4e8 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Sat, 3 Oct 2026 08:48:32 +0100 Subject: [PATCH 2/3] Fail the ESBMC contract check when no contract was checked If no listed file has an _RNv entry point, or all of them are excluded, the loop never runs ESBMC and the job used to exit 0. Count the checked contracts and exit 1 when there are none. --- scripts/run-goto-transcoder.sh | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/scripts/run-goto-transcoder.sh b/scripts/run-goto-transcoder.sh index af847284251df..6f32baea3aec6 100755 --- a/scripts/run-goto-transcoder.sh +++ b/scripts/run-goto-transcoder.sh @@ -37,6 +37,7 @@ if [ ! -x "$esbmc" ]; then chmod +x $esbmc fi +checked=0 ls $contract_folder | grep "$supported_regex" | grep -v .symtab.out > _contracts.txt while IFS= read -r line; do @@ -49,6 +50,12 @@ while IFS= read -r line; do fi echo "Processing: $contract" $esbmc --binary $contract_folder/$line --function $contract + checked=$((checked + 1)) done < "_contracts.txt" rm "_contracts.txt" + +if [ "$checked" -eq 0 ]; then + echo "No contract matching '$supported_regex' was checked" + exit 1 +fi From d1c0c686a1bbc7ef29397cf8b3851038cb8aaa28 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Sat, 3 Oct 2026 09:17:52 +0100 Subject: [PATCH 3/3] Keep ESBMC from reading the contract list on stdin ESBMC runs inside a loop that reads the contract list from stdin. A release that read stdin would consume the rest of the list after the first contract, and the job would pass with only one contract checked. --- scripts/run-goto-transcoder.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/run-goto-transcoder.sh b/scripts/run-goto-transcoder.sh index 6f32baea3aec6..f605e5714152e 100755 --- a/scripts/run-goto-transcoder.sh +++ b/scripts/run-goto-transcoder.sh @@ -49,7 +49,7 @@ while IFS= read -r line; do continue fi echo "Processing: $contract" - $esbmc --binary $contract_folder/$line --function $contract + $esbmc --binary $contract_folder/$line --function $contract < /dev/null checked=$((checked + 1)) done < "_contracts.txt"