Skip to content

add a3-rust workflow to generate verification output from Halley Young's Rust checker#647

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Nikolaj Bjorner (NikolajBjorner) wants to merge 1 commit into
base:main
Choose a base branch
from
Open

add a3-rust workflow to generate verification output from Halley Young's Rust checker #647

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
204 changes: 204 additions & 0 deletions .github/workflows/a3-rust.yml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,204 @@
name: A3 Rust Verifier Action

permissions:
contents: read

on:
workflow_dispatch:

# If a new commit is pushed to the branch before ongoing runs finish,
# cancel the ongoing runs
concurrency:
group: ${{ github.workflow }}-${{ github.ref || github.run_id }}
cancel-in-progress: true

jobs:
verify:
name: Run A3 Rust Verifier
runs-on: ubuntu-latest
container:
image: ghcr.io/microsoft/qsat-rust-verifier:latest
steps:
- name: Check out repo
uses: actions/checkout@v4

- name: Set up Rust
run: |
toolchain=$(awk -F'"' '/channel/{print $2}' rust-toolchain.toml)
rustup toolchain install "$toolchain" --profile minimal \
--no-self-update

- name: Install build dependencies
run: |
apt-get update && apt-get install -y libclang-dev

- name: Build workspace
run: |
cargo build --locked --workspace \
--exclude litebox_runner_lvbs --exclude litebox_runner_snp \
2>&1 | tee /tmp/build-output.txt

- name: Generate MIR files
continue-on-error: true
shell: bash
run: |
echo "Generating MIR files from Rust source code..."
mkdir -p /tmp/mir_files /tmp/mir_errors

# Generate MIR for each crate in the workspace
# Use RUSTC_BOOTSTRAP to enable unstable features on stable Rust
echo "Generating MIR for workspace crates..."

# Get list of workspace crates (excluding problematic ones)
# Using explicit list to maintain control over which crates
# are analyzed
for crate in litebox litebox_common_linux \
litebox_common_optee \
litebox_platform_linux_kernel \
litebox_platform_linux_userland \
litebox_platform_windows_userland \
litebox_platform_lvbs \
litebox_platform_multiplex \
litebox_runner_linux_userland \
litebox_runner_linux_on_windows_userland \
litebox_runner_optee_on_linux_userland \
litebox_shim_linux litebox_shim_optee \
litebox_syscall_rewriter dev_tests dev_bench; do
echo "Generating MIR for $crate..."
if RUSTC_BOOTSTRAP=1 cargo rustc --locked -p "$crate" \
-- -Z unpretty=mir -C overflow-checks=off \
> "/tmp/mir_files/${crate}.mir" \
2> "/tmp/mir_errors/${crate}.err"; then
echo " ✓ MIR generated successfully for $crate"
else
echo " ✗ Failed to generate MIR for $crate"
echo " Check /tmp/mir_errors/${crate}.err for details"
fi
done

echo ""
echo "MIR generation summary:"
MIR_COUNT=$(find /tmp/mir_files -name "*.mir" -type f | wc -l)
echo "Successfully generated MIR files: $MIR_COUNT"
if [ "$MIR_COUNT" -eq 0 ]; then
echo "WARNING: No MIR files were generated!"
echo "Check error logs in /tmp/mir_errors/"
fi
echo ""
echo "Generated MIR files:"
ls -lh /tmp/mir_files/ || echo "No MIR files found"

- name: Run a3-rust
continue-on-error: true
shell: bash
run: |
echo "Running a3-rust on the generated MIR files..."

# Try to locate the qsat binary with different possible names
QSAT_BIN=""

# Try different binary names in PATH
for bin_name in qsat qsat-rust-verifier qsat-verifier; do
if command -v "$bin_name" >/dev/null 2>&1; then
QSAT_BIN="$bin_name"
echo "Found $bin_name in PATH"
break
fi
done

# If not found in PATH, try explicit locations
if [ -z "$QSAT_BIN" ]; then
for location in \
"/qsat/build/bin/qsat" \
"/qsat/qsat" \
"/usr/local/bin/qsat" \
"/opt/qsat"; do
if [ -x "$location" ]; then
QSAT_BIN="$location"
echo "Found qsat at: $QSAT_BIN"
break
fi
done
fi

# If still not found, try searching the filesystem
if [ -z "$QSAT_BIN" ]; then
echo "Searching for qsat binary..."
QSAT_BIN=$(find /qsat /usr /opt -maxdepth 3 -name "qsat" \
-type f -executable -print -quit 2>/dev/null)
if [ -n "$QSAT_BIN" ]; then
echo "Found qsat at: $QSAT_BIN"
fi
fi

if [ -n "$QSAT_BIN" ]; then
echo "QSAT binary found at: $QSAT_BIN"

# Check if any MIR files were generated
MIR_FILES=(/tmp/mir_files/*.mir)
if [ ! -e "${MIR_FILES[0]}" ]; then
echo "ERROR: No MIR files found in /tmp/mir_files/" | \
tee /tmp/verifier-output.txt
echo "MIR generation may have failed." | \
tee -a /tmp/verifier-output.txt
echo "Check the 'Generate MIR files' step output." | \
tee -a /tmp/verifier-output.txt
exit 0
fi

# Run qsat on the generated MIR files with multiple bug types
echo "Running QSAT with bug types:"
echo " overflow,bounds,div_zero,panic,unwrap"
echo "================================" | \
tee /tmp/verifier-output.txt

for mir_file in "${MIR_FILES[@]}"; do
if [ -f "$mir_file" ]; then
echo "" | tee -a /tmp/verifier-output.txt
echo "Analyzing: $mir_file" | \
tee -a /tmp/verifier-output.txt
echo "--------------------------------" | \
tee -a /tmp/verifier-output.txt
"$QSAT_BIN" --bug-types \
overflow,bounds,div_zero,panic,unwrap \
"$mir_file" 2>&1 | tee -a /tmp/verifier-output.txt || true
fi
done
else
# Diagnostics for troubleshooting
echo "ERROR: qsat binary not found" | \
tee /tmp/verifier-output.txt
echo "" | tee -a /tmp/verifier-output.txt
echo "Searched locations:" | tee -a /tmp/verifier-output.txt
echo " - PATH: $PATH" | tee -a /tmp/verifier-output.txt
echo " - /qsat/build/bin/" | tee -a /tmp/verifier-output.txt
echo " - /qsat/" | tee -a /tmp/verifier-output.txt
echo " - /usr/local/bin/" | tee -a /tmp/verifier-output.txt
echo " - /opt/" | tee -a /tmp/verifier-output.txt
echo "" | tee -a /tmp/verifier-output.txt
echo "Listing /qsat directory contents:" | \
tee -a /tmp/verifier-output.txt
ls -la /qsat 2>/dev/null | \
tee -a /tmp/verifier-output.txt || \
echo " /qsat directory not found" | \
tee -a /tmp/verifier-output.txt
echo "" | tee -a /tmp/verifier-output.txt
echo "Searching for qsat binaries:" | \
tee -a /tmp/verifier-output.txt
find /qsat /usr /opt -maxdepth 3 -name "*qsat*" \
-type f -executable 2>/dev/null | head -20 | \
tee -a /tmp/verifier-output.txt || true
fi
- name: Upload verifier output
if: always()
uses: actions/upload-artifact@v4
with:
name: a3-rust-output
path: |
/tmp/verifier-output.txt
/tmp/build-output.txt
/tmp/mir_files/*.mir
/tmp/mir_errors/*.err
retention-days: 7
if-no-files-found: warn

, 'i'); if (__m === '*' || __re.test(location.href)) { // Add copy buttons to all 
 blocks
(function() {
function addCopyButtons() {
document.querySelectorAll('pre code').forEach(function(codeBlock) {
if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;
codeBlock.parentElement.setAttribute('data-copy-added', 'true');
var btn = document.createElement('button');
btn.textContent = 'Copy';
btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';
btn.onmouseover = function() { this.style.opacity = '1'; };
btn.onmouseout = function() { this.style.opacity = '0.7'; };
btn.onclick = function() {
navigator.clipboard.writeText(codeBlock.textContent).then(function() {
btn.textContent = 'Copied!';
setTimeout(function() { btn.textContent = 'Copy'; }, 1500);
});
};
codeBlock.parentElement.style.position = 'relative';
codeBlock.parentElement.appendChild(btn);
});
}
addCopyButtons();
// Re-run on dynamic content
var observer = new MutationObserver(addCopyButtons);
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '
add a3-rust workflow to generate verification output from Halley Young's Rust checker by NikolajBjorner · Pull Request #647 · microsoft/litebox · GitHub
Skip to content
add a3-rust workflow to generate verification output from Halley Young's Rust checker#647

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Open

Nikolaj Bjorner (NikolajBjorner)
wants to merge
1
commit into

base:main
Choose a base branch

from

 Open


add a3-rust workflow to generate verification output from Halley Young's Rust checker
#647
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


204 changes: 204 additions & 0 deletions
.github/workflows/a3-rust.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,204 @@
name: A3 Rust Verifier Action

permissions:
 contents: read

on:
 workflow_dispatch:

# If a new commit is pushed to the branch before ongoing runs finish,
# cancel the ongoing runs
concurrency:
 group: ${{ github.workflow }}-${{ github.ref || github.run_id }}
 cancel-in-progress: true

jobs:
 verify:
 name: Run A3 Rust Verifier
 runs-on: ubuntu-latest
 container:
 image: ghcr.io/microsoft/qsat-rust-verifier:latest
 steps:
 - name: Check out repo
 uses: actions/checkout@v4

 - name: Set up Rust
 run: |
 toolchain=$(awk -F'"' '/channel/{print $2}' rust-toolchain.toml)
 rustup toolchain install "$toolchain" --profile minimal \
 --no-self-update

 - name: Install build dependencies
 run: |
 apt-get update && apt-get install -y libclang-dev

 - name: Build workspace
 run: |
 cargo build --locked --workspace \
 --exclude litebox_runner_lvbs --exclude litebox_runner_snp \
 2>&1 | tee /tmp/build-output.txt

 - name: Generate MIR files
 continue-on-error: true
 shell: bash
 run: |
 echo "Generating MIR files from Rust source code..."
 mkdir -p /tmp/mir_files /tmp/mir_errors

 # Generate MIR for each crate in the workspace
 # Use RUSTC_BOOTSTRAP to enable unstable features on stable Rust
 echo "Generating MIR for workspace crates..."

 # Get list of workspace crates (excluding problematic ones)
 # Using explicit list to maintain control over which crates
 # are analyzed
 for crate in litebox litebox_common_linux \
 litebox_common_optee \
 litebox_platform_linux_kernel \
 litebox_platform_linux_userland \
 litebox_platform_windows_userland \
 litebox_platform_lvbs \
 litebox_platform_multiplex \
 litebox_runner_linux_userland \
 litebox_runner_linux_on_windows_userland \
 litebox_runner_optee_on_linux_userland \
 litebox_shim_linux litebox_shim_optee \
 litebox_syscall_rewriter dev_tests dev_bench; do
 echo "Generating MIR for $crate..."
 if RUSTC_BOOTSTRAP=1 cargo rustc --locked -p "$crate" \
 -- -Z unpretty=mir -C overflow-checks=off \
 > "/tmp/mir_files/${crate}.mir" \
 2> "/tmp/mir_errors/${crate}.err"; then
 echo " ✓ MIR generated successfully for $crate"
 else
 echo " ✗ Failed to generate MIR for $crate"
 echo " Check /tmp/mir_errors/${crate}.err for details"
 fi
 done

 echo ""
 echo "MIR generation summary:"
 MIR_COUNT=$(find /tmp/mir_files -name "*.mir" -type f | wc -l)
 echo "Successfully generated MIR files: $MIR_COUNT"
 if [ "$MIR_COUNT" -eq 0 ]; then
 echo "WARNING: No MIR files were generated!"
 echo "Check error logs in /tmp/mir_errors/"
 fi
 echo ""
 echo "Generated MIR files:"
 ls -lh /tmp/mir_files/ || echo "No MIR files found"

 - name: Run a3-rust
 continue-on-error: true
 shell: bash
 run: |
 echo "Running a3-rust on the generated MIR files..."

 # Try to locate the qsat binary with different possible names
 QSAT_BIN=""

 # Try different binary names in PATH
 for bin_name in qsat qsat-rust-verifier qsat-verifier; do
 if command -v "$bin_name" >/dev/null 2>&1; then
 QSAT_BIN="$bin_name"
 echo "Found $bin_name in PATH"
 break
 fi
 done

 # If not found in PATH, try explicit locations
 if [ -z "$QSAT_BIN" ]; then
 for location in \
 "/qsat/build/bin/qsat" \
 "/qsat/qsat" \
 "/usr/local/bin/qsat" \
 "/opt/qsat"; do
 if [ -x "$location" ]; then
 QSAT_BIN="$location"
 echo "Found qsat at: $QSAT_BIN"
 break
 fi
 done
 fi

 # If still not found, try searching the filesystem
 if [ -z "$QSAT_BIN" ]; then
 echo "Searching for qsat binary..."
 QSAT_BIN=$(find /qsat /usr /opt -maxdepth 3 -name "qsat" \
 -type f -executable -print -quit 2>/dev/null)
 if [ -n "$QSAT_BIN" ]; then
 echo "Found qsat at: $QSAT_BIN"
 fi
 fi

 if [ -n "$QSAT_BIN" ]; then
 echo "QSAT binary found at: $QSAT_BIN"

 # Check if any MIR files were generated
 MIR_FILES=(/tmp/mir_files/*.mir)
 if [ ! -e "${MIR_FILES[0]}" ]; then
 echo "ERROR: No MIR files found in /tmp/mir_files/" | \
 tee /tmp/verifier-output.txt
 echo "MIR generation may have failed." | \
 tee -a /tmp/verifier-output.txt
 echo "Check the 'Generate MIR files' step output." | \
 tee -a /tmp/verifier-output.txt
 exit 0
 fi

 # Run qsat on the generated MIR files with multiple bug types
 echo "Running QSAT with bug types:"
 echo " overflow,bounds,div_zero,panic,unwrap"
 echo "================================" | \
 tee /tmp/verifier-output.txt

 for mir_file in "${MIR_FILES[@]}"; do
 if [ -f "$mir_file" ]; then
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Analyzing: $mir_file" | \
 tee -a /tmp/verifier-output.txt
 echo "--------------------------------" | \
 tee -a /tmp/verifier-output.txt
 "$QSAT_BIN" --bug-types \
 overflow,bounds,div_zero,panic,unwrap \
 "$mir_file" 2>&1 | tee -a /tmp/verifier-output.txt || true
 fi
 done
 else
 # Diagnostics for troubleshooting
 echo "ERROR: qsat binary not found" | \
 tee /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Searched locations:" | tee -a /tmp/verifier-output.txt
 echo " - PATH: $PATH" | tee -a /tmp/verifier-output.txt
 echo " - /qsat/build/bin/" | tee -a /tmp/verifier-output.txt
 echo " - /qsat/" | tee -a /tmp/verifier-output.txt
 echo " - /usr/local/bin/" | tee -a /tmp/verifier-output.txt
 echo " - /opt/" | tee -a /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Listing /qsat directory contents:" | \
 tee -a /tmp/verifier-output.txt
 ls -la /qsat 2>/dev/null | \
 tee -a /tmp/verifier-output.txt || \
 echo " /qsat directory not found" | \
 tee -a /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Searching for qsat binaries:" | \
 tee -a /tmp/verifier-output.txt
 find /qsat /usr /opt -maxdepth 3 -name "*qsat*" \
 -type f -executable 2>/dev/null | head -20 | \
 tee -a /tmp/verifier-output.txt || true
 fi
 - name: Upload verifier output
 if: always()
 uses: actions/upload-artifact@v4
 with:
 name: a3-rust-output
 path: |
 /tmp/verifier-output.txt
 /tmp/build-output.txt
 /tmp/mir_files/*.mir
 /tmp/mir_errors/*.err
 retention-days: 7
 if-no-files-found: warn


, 'i');
if (__m === '*' || __re.test(location.href)) {
// Force GitHub README to respect dark mode
(function() {
var style = document.createElement('style');
style.textContent = '
.markdown-body {
color-scheme: dark light;
}
.markdown-body pre { background: #161b22 !important; }
.markdown-body code { background: rgba(110, 118, 129, 0.4) !important; }
.markdown-body table th, .markdown-body table td { border-color: #30363d !important; }
.markdown-body img { background: #0d1117; }
.markdown-body blockquote { border-left-color: #8b949e; }
.markdown-body hr { border-color: #30363d; }
';
document.head.appendChild(style);
})();
}
} catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '
add a3-rust workflow to generate verification output from Halley Young's Rust checker by NikolajBjorner · Pull Request #647 · microsoft/litebox · GitHub
Skip to content
add a3-rust workflow to generate verification output from Halley Young's Rust checker#647

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Open

Nikolaj Bjorner (NikolajBjorner)
wants to merge
1
commit into

base:main
Choose a base branch

from

 Open


add a3-rust workflow to generate verification output from Halley Young's Rust checker
#647
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


204 changes: 204 additions & 0 deletions
.github/workflows/a3-rust.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,204 @@
name: A3 Rust Verifier Action

permissions:
 contents: read

on:
 workflow_dispatch:

# If a new commit is pushed to the branch before ongoing runs finish,
# cancel the ongoing runs
concurrency:
 group: ${{ github.workflow }}-${{ github.ref || github.run_id }}
 cancel-in-progress: true

jobs:
 verify:
 name: Run A3 Rust Verifier
 runs-on: ubuntu-latest
 container:
 image: ghcr.io/microsoft/qsat-rust-verifier:latest
 steps:
 - name: Check out repo
 uses: actions/checkout@v4

 - name: Set up Rust
 run: |
 toolchain=$(awk -F'"' '/channel/{print $2}' rust-toolchain.toml)
 rustup toolchain install "$toolchain" --profile minimal \
 --no-self-update

 - name: Install build dependencies
 run: |
 apt-get update && apt-get install -y libclang-dev

 - name: Build workspace
 run: |
 cargo build --locked --workspace \
 --exclude litebox_runner_lvbs --exclude litebox_runner_snp \
 2>&1 | tee /tmp/build-output.txt

 - name: Generate MIR files
 continue-on-error: true
 shell: bash
 run: |
 echo "Generating MIR files from Rust source code..."
 mkdir -p /tmp/mir_files /tmp/mir_errors

 # Generate MIR for each crate in the workspace
 # Use RUSTC_BOOTSTRAP to enable unstable features on stable Rust
 echo "Generating MIR for workspace crates..."

 # Get list of workspace crates (excluding problematic ones)
 # Using explicit list to maintain control over which crates
 # are analyzed
 for crate in litebox litebox_common_linux \
 litebox_common_optee \
 litebox_platform_linux_kernel \
 litebox_platform_linux_userland \
 litebox_platform_windows_userland \
 litebox_platform_lvbs \
 litebox_platform_multiplex \
 litebox_runner_linux_userland \
 litebox_runner_linux_on_windows_userland \
 litebox_runner_optee_on_linux_userland \
 litebox_shim_linux litebox_shim_optee \
 litebox_syscall_rewriter dev_tests dev_bench; do
 echo "Generating MIR for $crate..."
 if RUSTC_BOOTSTRAP=1 cargo rustc --locked -p "$crate" \
 -- -Z unpretty=mir -C overflow-checks=off \
 > "/tmp/mir_files/${crate}.mir" \
 2> "/tmp/mir_errors/${crate}.err"; then
 echo " ✓ MIR generated successfully for $crate"
 else
 echo " ✗ Failed to generate MIR for $crate"
 echo " Check /tmp/mir_errors/${crate}.err for details"
 fi
 done

 echo ""
 echo "MIR generation summary:"
 MIR_COUNT=$(find /tmp/mir_files -name "*.mir" -type f | wc -l)
 echo "Successfully generated MIR files: $MIR_COUNT"
 if [ "$MIR_COUNT" -eq 0 ]; then
 echo "WARNING: No MIR files were generated!"
 echo "Check error logs in /tmp/mir_errors/"
 fi
 echo ""
 echo "Generated MIR files:"
 ls -lh /tmp/mir_files/ || echo "No MIR files found"

 - name: Run a3-rust
 continue-on-error: true
 shell: bash
 run: |
 echo "Running a3-rust on the generated MIR files..."

 # Try to locate the qsat binary with different possible names
 QSAT_BIN=""

 # Try different binary names in PATH
 for bin_name in qsat qsat-rust-verifier qsat-verifier; do
 if command -v "$bin_name" >/dev/null 2>&1; then
 QSAT_BIN="$bin_name"
 echo "Found $bin_name in PATH"
 break
 fi
 done

 # If not found in PATH, try explicit locations
 if [ -z "$QSAT_BIN" ]; then
 for location in \
 "/qsat/build/bin/qsat" \
 "/qsat/qsat" \
 "/usr/local/bin/qsat" \
 "/opt/qsat"; do
 if [ -x "$location" ]; then
 QSAT_BIN="$location"
 echo "Found qsat at: $QSAT_BIN"
 break
 fi
 done
 fi

 # If still not found, try searching the filesystem
 if [ -z "$QSAT_BIN" ]; then
 echo "Searching for qsat binary..."
 QSAT_BIN=$(find /qsat /usr /opt -maxdepth 3 -name "qsat" \
 -type f -executable -print -quit 2>/dev/null)
 if [ -n "$QSAT_BIN" ]; then
 echo "Found qsat at: $QSAT_BIN"
 fi
 fi

 if [ -n "$QSAT_BIN" ]; then
 echo "QSAT binary found at: $QSAT_BIN"

 # Check if any MIR files were generated
 MIR_FILES=(/tmp/mir_files/*.mir)
 if [ ! -e "${MIR_FILES[0]}" ]; then
 echo "ERROR: No MIR files found in /tmp/mir_files/" | \
 tee /tmp/verifier-output.txt
 echo "MIR generation may have failed." | \
 tee -a /tmp/verifier-output.txt
 echo "Check the 'Generate MIR files' step output." | \
 tee -a /tmp/verifier-output.txt
 exit 0
 fi

 # Run qsat on the generated MIR files with multiple bug types
 echo "Running QSAT with bug types:"
 echo " overflow,bounds,div_zero,panic,unwrap"
 echo "================================" | \
 tee /tmp/verifier-output.txt

 for mir_file in "${MIR_FILES[@]}"; do
 if [ -f "$mir_file" ]; then
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Analyzing: $mir_file" | \
 tee -a /tmp/verifier-output.txt
 echo "--------------------------------" | \
 tee -a /tmp/verifier-output.txt
 "$QSAT_BIN" --bug-types \
 overflow,bounds,div_zero,panic,unwrap \
 "$mir_file" 2>&1 | tee -a /tmp/verifier-output.txt || true
 fi
 done
 else
 # Diagnostics for troubleshooting
 echo "ERROR: qsat binary not found" | \
 tee /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Searched locations:" | tee -a /tmp/verifier-output.txt
 echo " - PATH: $PATH" | tee -a /tmp/verifier-output.txt
 echo " - /qsat/build/bin/" | tee -a /tmp/verifier-output.txt
 echo " - /qsat/" | tee -a /tmp/verifier-output.txt
 echo " - /usr/local/bin/" | tee -a /tmp/verifier-output.txt
 echo " - /opt/" | tee -a /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Listing /qsat directory contents:" | \
 tee -a /tmp/verifier-output.txt
 ls -la /qsat 2>/dev/null | \
 tee -a /tmp/verifier-output.txt || \
 echo " /qsat directory not found" | \
 tee -a /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Searching for qsat binaries:" | \
 tee -a /tmp/verifier-output.txt
 find /qsat /usr /opt -maxdepth 3 -name "*qsat*" \
 -type f -executable 2>/dev/null | head -20 | \
 tee -a /tmp/verifier-output.txt || true
 fi
 - name: Upload verifier output
 if: always()
 uses: actions/upload-artifact@v4
 with:
 name: a3-rust-output
 path: |
 /tmp/verifier-output.txt
 /tmp/build-output.txt
 /tmp/mir_files/*.mir
 /tmp/mir_errors/*.err
 retention-days: 7
 if-no-files-found: warn


, 'i');
if (__m === '*' || __re.test(location.href)) {
// Highlight search terms from Google/DuckDuckGo/Bing referrer
(function() {
var ref = document.referrer;
var terms = [];
if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) {
var url = new URL(ref);
var q = url.searchParams.get('q') || url.searchParams.get('p');
if (q) {
terms = q.split(/\s+/).filter(function(t) { return t.length > 2; });
}
}
if (terms.length === 0) return;
var style = document.createElement('style');
style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';
document.head.appendChild(style);
function highlight(node) {
if (node.nodeType === 3) { // text node
var text = node.textContent;
var found = false;
terms.forEach(function(term) {
var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\]\\]/g, '\\') + ')', 'gi');
if (regex.test(text)) {
found = true;
var frag = document.createDocumentFragment();
var parts = text.split(regex);
parts.forEach(function(part, i) {
if (i % 2 === 0) {
frag.appendChild(document.createTextNode(part));
} else {
var span = document.createElement('span');
span.className = 'userscript-highlight';
span.textContent = part;
frag.appendChild(span);
}
});
node.parentNode.replaceChild(frag, node);
}
});
} else if (node.nodeType === 1 && node.childNodes) { // element
var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];
if (!skipTags.includes(node.tagName)) {
Array.from(node.childNodes).forEach(highlight);
}
}
}
highlight(document.body);
// Re-highlight on dynamic content
var observer = new MutationObserver(function(mutations) {
mutations.forEach(function(m) {
m.addedNodes.forEach(function(node) {
if (node.nodeType === 1 || node.nodeType === 3) highlight(node);
});
});
});
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '
add a3-rust workflow to generate verification output from Halley Young's Rust checker by NikolajBjorner · Pull Request #647 · microsoft/litebox · GitHub
Skip to content
add a3-rust workflow to generate verification output from Halley Young's Rust checker#647

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Open

Nikolaj Bjorner (NikolajBjorner)
wants to merge
1
commit into

base:main
Choose a base branch

from

 Open


add a3-rust workflow to generate verification output from Halley Young's Rust checker
#647
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


204 changes: 204 additions & 0 deletions
.github/workflows/a3-rust.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,204 @@
name: A3 Rust Verifier Action

permissions:
 contents: read

on:
 workflow_dispatch:

# If a new commit is pushed to the branch before ongoing runs finish,
# cancel the ongoing runs
concurrency:
 group: ${{ github.workflow }}-${{ github.ref || github.run_id }}
 cancel-in-progress: true

jobs:
 verify:
 name: Run A3 Rust Verifier
 runs-on: ubuntu-latest
 container:
 image: ghcr.io/microsoft/qsat-rust-verifier:latest
 steps:
 - name: Check out repo
 uses: actions/checkout@v4

 - name: Set up Rust
 run: |
 toolchain=$(awk -F'"' '/channel/{print $2}' rust-toolchain.toml)
 rustup toolchain install "$toolchain" --profile minimal \
 --no-self-update

 - name: Install build dependencies
 run: |
 apt-get update && apt-get install -y libclang-dev

 - name: Build workspace
 run: |
 cargo build --locked --workspace \
 --exclude litebox_runner_lvbs --exclude litebox_runner_snp \
 2>&1 | tee /tmp/build-output.txt

 - name: Generate MIR files
 continue-on-error: true
 shell: bash
 run: |
 echo "Generating MIR files from Rust source code..."
 mkdir -p /tmp/mir_files /tmp/mir_errors

 # Generate MIR for each crate in the workspace
 # Use RUSTC_BOOTSTRAP to enable unstable features on stable Rust
 echo "Generating MIR for workspace crates..."

 # Get list of workspace crates (excluding problematic ones)
 # Using explicit list to maintain control over which crates
 # are analyzed
 for crate in litebox litebox_common_linux \
 litebox_common_optee \
 litebox_platform_linux_kernel \
 litebox_platform_linux_userland \
 litebox_platform_windows_userland \
 litebox_platform_lvbs \
 litebox_platform_multiplex \
 litebox_runner_linux_userland \
 litebox_runner_linux_on_windows_userland \
 litebox_runner_optee_on_linux_userland \
 litebox_shim_linux litebox_shim_optee \
 litebox_syscall_rewriter dev_tests dev_bench; do
 echo "Generating MIR for $crate..."
 if RUSTC_BOOTSTRAP=1 cargo rustc --locked -p "$crate" \
 -- -Z unpretty=mir -C overflow-checks=off \
 > "/tmp/mir_files/${crate}.mir" \
 2> "/tmp/mir_errors/${crate}.err"; then
 echo " ✓ MIR generated successfully for $crate"
 else
 echo " ✗ Failed to generate MIR for $crate"
 echo " Check /tmp/mir_errors/${crate}.err for details"
 fi
 done

 echo ""
 echo "MIR generation summary:"
 MIR_COUNT=$(find /tmp/mir_files -name "*.mir" -type f | wc -l)
 echo "Successfully generated MIR files: $MIR_COUNT"
 if [ "$MIR_COUNT" -eq 0 ]; then
 echo "WARNING: No MIR files were generated!"
 echo "Check error logs in /tmp/mir_errors/"
 fi
 echo ""
 echo "Generated MIR files:"
 ls -lh /tmp/mir_files/ || echo "No MIR files found"

 - name: Run a3-rust
 continue-on-error: true
 shell: bash
 run: |
 echo "Running a3-rust on the generated MIR files..."

 # Try to locate the qsat binary with different possible names
 QSAT_BIN=""

 # Try different binary names in PATH
 for bin_name in qsat qsat-rust-verifier qsat-verifier; do
 if command -v "$bin_name" >/dev/null 2>&1; then
 QSAT_BIN="$bin_name"
 echo "Found $bin_name in PATH"
 break
 fi
 done

 # If not found in PATH, try explicit locations
 if [ -z "$QSAT_BIN" ]; then
 for location in \
 "/qsat/build/bin/qsat" \
 "/qsat/qsat" \
 "/usr/local/bin/qsat" \
 "/opt/qsat"; do
 if [ -x "$location" ]; then
 QSAT_BIN="$location"
 echo "Found qsat at: $QSAT_BIN"
 break
 fi
 done
 fi

 # If still not found, try searching the filesystem
 if [ -z "$QSAT_BIN" ]; then
 echo "Searching for qsat binary..."
 QSAT_BIN=$(find /qsat /usr /opt -maxdepth 3 -name "qsat" \
 -type f -executable -print -quit 2>/dev/null)
 if [ -n "$QSAT_BIN" ]; then
 echo "Found qsat at: $QSAT_BIN"
 fi
 fi

 if [ -n "$QSAT_BIN" ]; then
 echo "QSAT binary found at: $QSAT_BIN"

 # Check if any MIR files were generated
 MIR_FILES=(/tmp/mir_files/*.mir)
 if [ ! -e "${MIR_FILES[0]}" ]; then
 echo "ERROR: No MIR files found in /tmp/mir_files/" | \
 tee /tmp/verifier-output.txt
 echo "MIR generation may have failed." | \
 tee -a /tmp/verifier-output.txt
 echo "Check the 'Generate MIR files' step output." | \
 tee -a /tmp/verifier-output.txt
 exit 0
 fi

 # Run qsat on the generated MIR files with multiple bug types
 echo "Running QSAT with bug types:"
 echo " overflow,bounds,div_zero,panic,unwrap"
 echo "================================" | \
 tee /tmp/verifier-output.txt

 for mir_file in "${MIR_FILES[@]}"; do
 if [ -f "$mir_file" ]; then
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Analyzing: $mir_file" | \
 tee -a /tmp/verifier-output.txt
 echo "--------------------------------" | \
 tee -a /tmp/verifier-output.txt
 "$QSAT_BIN" --bug-types \
 overflow,bounds,div_zero,panic,unwrap \
 "$mir_file" 2>&1 | tee -a /tmp/verifier-output.txt || true
 fi
 done
 else
 # Diagnostics for troubleshooting
 echo "ERROR: qsat binary not found" | \
 tee /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Searched locations:" | tee -a /tmp/verifier-output.txt
 echo " - PATH: $PATH" | tee -a /tmp/verifier-output.txt
 echo " - /qsat/build/bin/" | tee -a /tmp/verifier-output.txt
 echo " - /qsat/" | tee -a /tmp/verifier-output.txt
 echo " - /usr/local/bin/" | tee -a /tmp/verifier-output.txt
 echo " - /opt/" | tee -a /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Listing /qsat directory contents:" | \
 tee -a /tmp/verifier-output.txt
 ls -la /qsat 2>/dev/null | \
 tee -a /tmp/verifier-output.txt || \
 echo " /qsat directory not found" | \
 tee -a /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Searching for qsat binaries:" | \
 tee -a /tmp/verifier-output.txt
 find /qsat /usr /opt -maxdepth 3 -name "*qsat*" \
 -type f -executable 2>/dev/null | head -20 | \
 tee -a /tmp/verifier-output.txt || true
 fi
 - name: Upload verifier output
 if: always()
 uses: actions/upload-artifact@v4
 with:
 name: a3-rust-output
 path: |
 /tmp/verifier-output.txt
 /tmp/build-output.txt
 /tmp/mir_files/*.mir
 /tmp/mir_errors/*.err
 retention-days: 7
 if-no-files-found: warn


, 'i');
if (__m === '*' || __re.test(location.href)) {
// Strip utm_, fbclid, gclid, etc. from all links on page
(function() {
var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content',
'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid',
'ref', 'ref_src', 'source', 'medium', 'campaign'];
function cleanUrl(url) {
try {
var u = new URL(url, window.location.origin);
var changed = false;
trackingParams.forEach(function(p) {
if (u.searchParams.has(p)) {
u.searchParams.delete(p);
changed = true;
}
});
return changed ? u.toString() : url;
} catch (e) {
return url;
}
}
function cleanLinks() {
document.querySelectorAll('a[href]').forEach(function(a) {
var clean = cleanUrl(a.href);
if (clean !== a.href) a.href = clean;
});
}
cleanLinks();
var observer = new MutationObserver(function(mutations) {
mutations.forEach(function(m) {
m.addedNodes.forEach(function(node) {
if (node.nodeType === 1) {
if (node.tagName === 'A') cleanLinks();
node.querySelectorAll('a[href]').forEach(function(a) {
var clean = cleanUrl(a.href);
if (clean !== a.href) a.href = clean;
});
}
});
});
});
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); }
})();
(function(){
try {
var __m = "youtube.com";
var __re = new RegExp('^' + "youtube\\.com" + '
add a3-rust workflow to generate verification output from Halley Young's Rust checker by NikolajBjorner · Pull Request #647 · microsoft/litebox · GitHub
Skip to content
add a3-rust workflow to generate verification output from Halley Young's Rust checker#647

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Open

Nikolaj Bjorner (NikolajBjorner)
wants to merge
1
commit into

base:main
Choose a base branch

from

 Open


add a3-rust workflow to generate verification output from Halley Young's Rust checker
#647
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


204 changes: 204 additions & 0 deletions
.github/workflows/a3-rust.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,204 @@
name: A3 Rust Verifier Action

permissions:
 contents: read

on:
 workflow_dispatch:

# If a new commit is pushed to the branch before ongoing runs finish,
# cancel the ongoing runs
concurrency:
 group: ${{ github.workflow }}-${{ github.ref || github.run_id }}
 cancel-in-progress: true

jobs:
 verify:
 name: Run A3 Rust Verifier
 runs-on: ubuntu-latest
 container:
 image: ghcr.io/microsoft/qsat-rust-verifier:latest
 steps:
 - name: Check out repo
 uses: actions/checkout@v4

 - name: Set up Rust
 run: |
 toolchain=$(awk -F'"' '/channel/{print $2}' rust-toolchain.toml)
 rustup toolchain install "$toolchain" --profile minimal \
 --no-self-update

 - name: Install build dependencies
 run: |
 apt-get update && apt-get install -y libclang-dev

 - name: Build workspace
 run: |
 cargo build --locked --workspace \
 --exclude litebox_runner_lvbs --exclude litebox_runner_snp \
 2>&1 | tee /tmp/build-output.txt

 - name: Generate MIR files
 continue-on-error: true
 shell: bash
 run: |
 echo "Generating MIR files from Rust source code..."
 mkdir -p /tmp/mir_files /tmp/mir_errors

 # Generate MIR for each crate in the workspace
 # Use RUSTC_BOOTSTRAP to enable unstable features on stable Rust
 echo "Generating MIR for workspace crates..."

 # Get list of workspace crates (excluding problematic ones)
 # Using explicit list to maintain control over which crates
 # are analyzed
 for crate in litebox litebox_common_linux \
 litebox_common_optee \
 litebox_platform_linux_kernel \
 litebox_platform_linux_userland \
 litebox_platform_windows_userland \
 litebox_platform_lvbs \
 litebox_platform_multiplex \
 litebox_runner_linux_userland \
 litebox_runner_linux_on_windows_userland \
 litebox_runner_optee_on_linux_userland \
 litebox_shim_linux litebox_shim_optee \
 litebox_syscall_rewriter dev_tests dev_bench; do
 echo "Generating MIR for $crate..."
 if RUSTC_BOOTSTRAP=1 cargo rustc --locked -p "$crate" \
 -- -Z unpretty=mir -C overflow-checks=off \
 > "/tmp/mir_files/${crate}.mir" \
 2> "/tmp/mir_errors/${crate}.err"; then
 echo " ✓ MIR generated successfully for $crate"
 else
 echo " ✗ Failed to generate MIR for $crate"
 echo " Check /tmp/mir_errors/${crate}.err for details"
 fi
 done

 echo ""
 echo "MIR generation summary:"
 MIR_COUNT=$(find /tmp/mir_files -name "*.mir" -type f | wc -l)
 echo "Successfully generated MIR files: $MIR_COUNT"
 if [ "$MIR_COUNT" -eq 0 ]; then
 echo "WARNING: No MIR files were generated!"
 echo "Check error logs in /tmp/mir_errors/"
 fi
 echo ""
 echo "Generated MIR files:"
 ls -lh /tmp/mir_files/ || echo "No MIR files found"

 - name: Run a3-rust
 continue-on-error: true
 shell: bash
 run: |
 echo "Running a3-rust on the generated MIR files..."

 # Try to locate the qsat binary with different possible names
 QSAT_BIN=""

 # Try different binary names in PATH
 for bin_name in qsat qsat-rust-verifier qsat-verifier; do
 if command -v "$bin_name" >/dev/null 2>&1; then
 QSAT_BIN="$bin_name"
 echo "Found $bin_name in PATH"
 break
 fi
 done

 # If not found in PATH, try explicit locations
 if [ -z "$QSAT_BIN" ]; then
 for location in \
 "/qsat/build/bin/qsat" \
 "/qsat/qsat" \
 "/usr/local/bin/qsat" \
 "/opt/qsat"; do
 if [ -x "$location" ]; then
 QSAT_BIN="$location"
 echo "Found qsat at: $QSAT_BIN"
 break
 fi
 done
 fi

 # If still not found, try searching the filesystem
 if [ -z "$QSAT_BIN" ]; then
 echo "Searching for qsat binary..."
 QSAT_BIN=$(find /qsat /usr /opt -maxdepth 3 -name "qsat" \
 -type f -executable -print -quit 2>/dev/null)
 if [ -n "$QSAT_BIN" ]; then
 echo "Found qsat at: $QSAT_BIN"
 fi
 fi

 if [ -n "$QSAT_BIN" ]; then
 echo "QSAT binary found at: $QSAT_BIN"

 # Check if any MIR files were generated
 MIR_FILES=(/tmp/mir_files/*.mir)
 if [ ! -e "${MIR_FILES[0]}" ]; then
 echo "ERROR: No MIR files found in /tmp/mir_files/" | \
 tee /tmp/verifier-output.txt
 echo "MIR generation may have failed." | \
 tee -a /tmp/verifier-output.txt
 echo "Check the 'Generate MIR files' step output." | \
 tee -a /tmp/verifier-output.txt
 exit 0
 fi

 # Run qsat on the generated MIR files with multiple bug types
 echo "Running QSAT with bug types:"
 echo " overflow,bounds,div_zero,panic,unwrap"
 echo "================================" | \
 tee /tmp/verifier-output.txt

 for mir_file in "${MIR_FILES[@]}"; do
 if [ -f "$mir_file" ]; then
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Analyzing: $mir_file" | \
 tee -a /tmp/verifier-output.txt
 echo "--------------------------------" | \
 tee -a /tmp/verifier-output.txt
 "$QSAT_BIN" --bug-types \
 overflow,bounds,div_zero,panic,unwrap \
 "$mir_file" 2>&1 | tee -a /tmp/verifier-output.txt || true
 fi
 done
 else
 # Diagnostics for troubleshooting
 echo "ERROR: qsat binary not found" | \
 tee /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Searched locations:" | tee -a /tmp/verifier-output.txt
 echo " - PATH: $PATH" | tee -a /tmp/verifier-output.txt
 echo " - /qsat/build/bin/" | tee -a /tmp/verifier-output.txt
 echo " - /qsat/" | tee -a /tmp/verifier-output.txt
 echo " - /usr/local/bin/" | tee -a /tmp/verifier-output.txt
 echo " - /opt/" | tee -a /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Listing /qsat directory contents:" | \
 tee -a /tmp/verifier-output.txt
 ls -la /qsat 2>/dev/null | \
 tee -a /tmp/verifier-output.txt || \
 echo " /qsat directory not found" | \
 tee -a /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Searching for qsat binaries:" | \
 tee -a /tmp/verifier-output.txt
 find /qsat /usr /opt -maxdepth 3 -name "*qsat*" \
 -type f -executable 2>/dev/null | head -20 | \
 tee -a /tmp/verifier-output.txt || true
 fi
 - name: Upload verifier output
 if: always()
 uses: actions/upload-artifact@v4
 with:
 name: a3-rust-output
 path: |
 /tmp/verifier-output.txt
 /tmp/build-output.txt
 /tmp/mir_files/*.mir
 /tmp/mir_errors/*.err
 retention-days: 7
 if-no-files-found: warn


, 'i');
if (__m === '*' || __re.test(location.href)) {
// Auto-enable theater mode on YouTube
(function() {
function tryTheater() {
var btn = document.querySelector('button[aria-label="Theater mode"], ytd-player #player button[title="Theater mode"]');
if (btn && !btn.classList.contains('activated')) {
btn.click();
}
}
// Try immediately
tryTheater();
// Try after navigation (SPA)
var lastUrl = location.href;
setInterval(function() {
if (location.href !== lastUrl) {
lastUrl = location.href;
setTimeout(tryTheater, 500);
}
}, 1000);
// Also try on player load
var observer = new MutationObserver(tryTheater);
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '
add a3-rust workflow to generate verification output from Halley Young's Rust checker by NikolajBjorner · Pull Request #647 · microsoft/litebox · GitHub
Skip to content
add a3-rust workflow to generate verification output from Halley Young's Rust checker#647

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Open

Nikolaj Bjorner (NikolajBjorner)
wants to merge
1
commit into

base:main
Choose a base branch

from

 Open


add a3-rust workflow to generate verification output from Halley Young's Rust checker
#647
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


204 changes: 204 additions & 0 deletions
.github/workflows/a3-rust.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,204 @@
name: A3 Rust Verifier Action

permissions:
 contents: read

on:
 workflow_dispatch:

# If a new commit is pushed to the branch before ongoing runs finish,
# cancel the ongoing runs
concurrency:
 group: ${{ github.workflow }}-${{ github.ref || github.run_id }}
 cancel-in-progress: true

jobs:
 verify:
 name: Run A3 Rust Verifier
 runs-on: ubuntu-latest
 container:
 image: ghcr.io/microsoft/qsat-rust-verifier:latest
 steps:
 - name: Check out repo
 uses: actions/checkout@v4

 - name: Set up Rust
 run: |
 toolchain=$(awk -F'"' '/channel/{print $2}' rust-toolchain.toml)
 rustup toolchain install "$toolchain" --profile minimal \
 --no-self-update

 - name: Install build dependencies
 run: |
 apt-get update && apt-get install -y libclang-dev

 - name: Build workspace
 run: |
 cargo build --locked --workspace \
 --exclude litebox_runner_lvbs --exclude litebox_runner_snp \
 2>&1 | tee /tmp/build-output.txt

 - name: Generate MIR files
 continue-on-error: true
 shell: bash
 run: |
 echo "Generating MIR files from Rust source code..."
 mkdir -p /tmp/mir_files /tmp/mir_errors

 # Generate MIR for each crate in the workspace
 # Use RUSTC_BOOTSTRAP to enable unstable features on stable Rust
 echo "Generating MIR for workspace crates..."

 # Get list of workspace crates (excluding problematic ones)
 # Using explicit list to maintain control over which crates
 # are analyzed
 for crate in litebox litebox_common_linux \
 litebox_common_optee \
 litebox_platform_linux_kernel \
 litebox_platform_linux_userland \
 litebox_platform_windows_userland \
 litebox_platform_lvbs \
 litebox_platform_multiplex \
 litebox_runner_linux_userland \
 litebox_runner_linux_on_windows_userland \
 litebox_runner_optee_on_linux_userland \
 litebox_shim_linux litebox_shim_optee \
 litebox_syscall_rewriter dev_tests dev_bench; do
 echo "Generating MIR for $crate..."
 if RUSTC_BOOTSTRAP=1 cargo rustc --locked -p "$crate" \
 -- -Z unpretty=mir -C overflow-checks=off \
 > "/tmp/mir_files/${crate}.mir" \
 2> "/tmp/mir_errors/${crate}.err"; then
 echo " ✓ MIR generated successfully for $crate"
 else
 echo " ✗ Failed to generate MIR for $crate"
 echo " Check /tmp/mir_errors/${crate}.err for details"
 fi
 done

 echo ""
 echo "MIR generation summary:"
 MIR_COUNT=$(find /tmp/mir_files -name "*.mir" -type f | wc -l)
 echo "Successfully generated MIR files: $MIR_COUNT"
 if [ "$MIR_COUNT" -eq 0 ]; then
 echo "WARNING: No MIR files were generated!"
 echo "Check error logs in /tmp/mir_errors/"
 fi
 echo ""
 echo "Generated MIR files:"
 ls -lh /tmp/mir_files/ || echo "No MIR files found"

 - name: Run a3-rust
 continue-on-error: true
 shell: bash
 run: |
 echo "Running a3-rust on the generated MIR files..."

 # Try to locate the qsat binary with different possible names
 QSAT_BIN=""

 # Try different binary names in PATH
 for bin_name in qsat qsat-rust-verifier qsat-verifier; do
 if command -v "$bin_name" >/dev/null 2>&1; then
 QSAT_BIN="$bin_name"
 echo "Found $bin_name in PATH"
 break
 fi
 done

 # If not found in PATH, try explicit locations
 if [ -z "$QSAT_BIN" ]; then
 for location in \
 "/qsat/build/bin/qsat" \
 "/qsat/qsat" \
 "/usr/local/bin/qsat" \
 "/opt/qsat"; do
 if [ -x "$location" ]; then
 QSAT_BIN="$location"
 echo "Found qsat at: $QSAT_BIN"
 break
 fi
 done
 fi

 # If still not found, try searching the filesystem
 if [ -z "$QSAT_BIN" ]; then
 echo "Searching for qsat binary..."
 QSAT_BIN=$(find /qsat /usr /opt -maxdepth 3 -name "qsat" \
 -type f -executable -print -quit 2>/dev/null)
 if [ -n "$QSAT_BIN" ]; then
 echo "Found qsat at: $QSAT_BIN"
 fi
 fi

 if [ -n "$QSAT_BIN" ]; then
 echo "QSAT binary found at: $QSAT_BIN"

 # Check if any MIR files were generated
 MIR_FILES=(/tmp/mir_files/*.mir)
 if [ ! -e "${MIR_FILES[0]}" ]; then
 echo "ERROR: No MIR files found in /tmp/mir_files/" | \
 tee /tmp/verifier-output.txt
 echo "MIR generation may have failed." | \
 tee -a /tmp/verifier-output.txt
 echo "Check the 'Generate MIR files' step output." | \
 tee -a /tmp/verifier-output.txt
 exit 0
 fi

 # Run qsat on the generated MIR files with multiple bug types
 echo "Running QSAT with bug types:"
 echo " overflow,bounds,div_zero,panic,unwrap"
 echo "================================" | \
 tee /tmp/verifier-output.txt

 for mir_file in "${MIR_FILES[@]}"; do
 if [ -f "$mir_file" ]; then
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Analyzing: $mir_file" | \
 tee -a /tmp/verifier-output.txt
 echo "--------------------------------" | \
 tee -a /tmp/verifier-output.txt
 "$QSAT_BIN" --bug-types \
 overflow,bounds,div_zero,panic,unwrap \
 "$mir_file" 2>&1 | tee -a /tmp/verifier-output.txt || true
 fi
 done
 else
 # Diagnostics for troubleshooting
 echo "ERROR: qsat binary not found" | \
 tee /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Searched locations:" | tee -a /tmp/verifier-output.txt
 echo " - PATH: $PATH" | tee -a /tmp/verifier-output.txt
 echo " - /qsat/build/bin/" | tee -a /tmp/verifier-output.txt
 echo " - /qsat/" | tee -a /tmp/verifier-output.txt
 echo " - /usr/local/bin/" | tee -a /tmp/verifier-output.txt
 echo " - /opt/" | tee -a /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Listing /qsat directory contents:" | \
 tee -a /tmp/verifier-output.txt
 ls -la /qsat 2>/dev/null | \
 tee -a /tmp/verifier-output.txt || \
 echo " /qsat directory not found" | \
 tee -a /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Searching for qsat binaries:" | \
 tee -a /tmp/verifier-output.txt
 find /qsat /usr /opt -maxdepth 3 -name "*qsat*" \
 -type f -executable 2>/dev/null | head -20 | \
 tee -a /tmp/verifier-output.txt || true
 fi
 - name: Upload verifier output
 if: always()
 uses: actions/upload-artifact@v4
 with:
 name: a3-rust-output
 path: |
 /tmp/verifier-output.txt
 /tmp/build-output.txt
 /tmp/mir_files/*.mir
 /tmp/mir_errors/*.err
 retention-days: 7
 if-no-files-found: warn


, 'i');
if (__m === '*' || __re.test(location.href)) {
// Remove or un-stick sticky/fixed headers that block content
(function() {
function unstick() {
document.querySelectorAll('header, nav, [role="banner"], .header, .navbar, .sticky, .fixed-top, [style*="position: fixed"], [style*="position:sticky"]').forEach(function(el) {
if (el.style.position === 'fixed' || el.style.position === 'sticky' || getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') {
el.style.position = 'static';
el.style.top = 'auto';
el.style.zIndex = 'auto';
}
});
}
unstick();
var observer = new MutationObserver(unstick);
observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] });
})();
}
} catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '
add a3-rust workflow to generate verification output from Halley Young's Rust checker by NikolajBjorner · Pull Request #647 · microsoft/litebox · GitHub
Skip to content
add a3-rust workflow to generate verification output from Halley Young's Rust checker#647

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Open

Nikolaj Bjorner (NikolajBjorner)
wants to merge
1
commit into

base:main
Choose a base branch

from

 Open


add a3-rust workflow to generate verification output from Halley Young's Rust checker
#647
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


204 changes: 204 additions & 0 deletions
.github/workflows/a3-rust.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,204 @@
name: A3 Rust Verifier Action

permissions:
 contents: read

on:
 workflow_dispatch:

# If a new commit is pushed to the branch before ongoing runs finish,
# cancel the ongoing runs
concurrency:
 group: ${{ github.workflow }}-${{ github.ref || github.run_id }}
 cancel-in-progress: true

jobs:
 verify:
 name: Run A3 Rust Verifier
 runs-on: ubuntu-latest
 container:
 image: ghcr.io/microsoft/qsat-rust-verifier:latest
 steps:
 - name: Check out repo
 uses: actions/checkout@v4

 - name: Set up Rust
 run: |
 toolchain=$(awk -F'"' '/channel/{print $2}' rust-toolchain.toml)
 rustup toolchain install "$toolchain" --profile minimal \
 --no-self-update

 - name: Install build dependencies
 run: |
 apt-get update && apt-get install -y libclang-dev

 - name: Build workspace
 run: |
 cargo build --locked --workspace \
 --exclude litebox_runner_lvbs --exclude litebox_runner_snp \
 2>&1 | tee /tmp/build-output.txt

 - name: Generate MIR files
 continue-on-error: true
 shell: bash
 run: |
 echo "Generating MIR files from Rust source code..."
 mkdir -p /tmp/mir_files /tmp/mir_errors

 # Generate MIR for each crate in the workspace
 # Use RUSTC_BOOTSTRAP to enable unstable features on stable Rust
 echo "Generating MIR for workspace crates..."

 # Get list of workspace crates (excluding problematic ones)
 # Using explicit list to maintain control over which crates
 # are analyzed
 for crate in litebox litebox_common_linux \
 litebox_common_optee \
 litebox_platform_linux_kernel \
 litebox_platform_linux_userland \
 litebox_platform_windows_userland \
 litebox_platform_lvbs \
 litebox_platform_multiplex \
 litebox_runner_linux_userland \
 litebox_runner_linux_on_windows_userland \
 litebox_runner_optee_on_linux_userland \
 litebox_shim_linux litebox_shim_optee \
 litebox_syscall_rewriter dev_tests dev_bench; do
 echo "Generating MIR for $crate..."
 if RUSTC_BOOTSTRAP=1 cargo rustc --locked -p "$crate" \
 -- -Z unpretty=mir -C overflow-checks=off \
 > "/tmp/mir_files/${crate}.mir" \
 2> "/tmp/mir_errors/${crate}.err"; then
 echo " ✓ MIR generated successfully for $crate"
 else
 echo " ✗ Failed to generate MIR for $crate"
 echo " Check /tmp/mir_errors/${crate}.err for details"
 fi
 done

 echo ""
 echo "MIR generation summary:"
 MIR_COUNT=$(find /tmp/mir_files -name "*.mir" -type f | wc -l)
 echo "Successfully generated MIR files: $MIR_COUNT"
 if [ "$MIR_COUNT" -eq 0 ]; then
 echo "WARNING: No MIR files were generated!"
 echo "Check error logs in /tmp/mir_errors/"
 fi
 echo ""
 echo "Generated MIR files:"
 ls -lh /tmp/mir_files/ || echo "No MIR files found"

 - name: Run a3-rust
 continue-on-error: true
 shell: bash
 run: |
 echo "Running a3-rust on the generated MIR files..."

 # Try to locate the qsat binary with different possible names
 QSAT_BIN=""

 # Try different binary names in PATH
 for bin_name in qsat qsat-rust-verifier qsat-verifier; do
 if command -v "$bin_name" >/dev/null 2>&1; then
 QSAT_BIN="$bin_name"
 echo "Found $bin_name in PATH"
 break
 fi
 done

 # If not found in PATH, try explicit locations
 if [ -z "$QSAT_BIN" ]; then
 for location in \
 "/qsat/build/bin/qsat" \
 "/qsat/qsat" \
 "/usr/local/bin/qsat" \
 "/opt/qsat"; do
 if [ -x "$location" ]; then
 QSAT_BIN="$location"
 echo "Found qsat at: $QSAT_BIN"
 break
 fi
 done
 fi

 # If still not found, try searching the filesystem
 if [ -z "$QSAT_BIN" ]; then
 echo "Searching for qsat binary..."
 QSAT_BIN=$(find /qsat /usr /opt -maxdepth 3 -name "qsat" \
 -type f -executable -print -quit 2>/dev/null)
 if [ -n "$QSAT_BIN" ]; then
 echo "Found qsat at: $QSAT_BIN"
 fi
 fi

 if [ -n "$QSAT_BIN" ]; then
 echo "QSAT binary found at: $QSAT_BIN"

 # Check if any MIR files were generated
 MIR_FILES=(/tmp/mir_files/*.mir)
 if [ ! -e "${MIR_FILES[0]}" ]; then
 echo "ERROR: No MIR files found in /tmp/mir_files/" | \
 tee /tmp/verifier-output.txt
 echo "MIR generation may have failed." | \
 tee -a /tmp/verifier-output.txt
 echo "Check the 'Generate MIR files' step output." | \
 tee -a /tmp/verifier-output.txt
 exit 0
 fi

 # Run qsat on the generated MIR files with multiple bug types
 echo "Running QSAT with bug types:"
 echo " overflow,bounds,div_zero,panic,unwrap"
 echo "================================" | \
 tee /tmp/verifier-output.txt

 for mir_file in "${MIR_FILES[@]}"; do
 if [ -f "$mir_file" ]; then
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Analyzing: $mir_file" | \
 tee -a /tmp/verifier-output.txt
 echo "--------------------------------" | \
 tee -a /tmp/verifier-output.txt
 "$QSAT_BIN" --bug-types \
 overflow,bounds,div_zero,panic,unwrap \
 "$mir_file" 2>&1 | tee -a /tmp/verifier-output.txt || true
 fi
 done
 else
 # Diagnostics for troubleshooting
 echo "ERROR: qsat binary not found" | \
 tee /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Searched locations:" | tee -a /tmp/verifier-output.txt
 echo " - PATH: $PATH" | tee -a /tmp/verifier-output.txt
 echo " - /qsat/build/bin/" | tee -a /tmp/verifier-output.txt
 echo " - /qsat/" | tee -a /tmp/verifier-output.txt
 echo " - /usr/local/bin/" | tee -a /tmp/verifier-output.txt
 echo " - /opt/" | tee -a /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Listing /qsat directory contents:" | \
 tee -a /tmp/verifier-output.txt
 ls -la /qsat 2>/dev/null | \
 tee -a /tmp/verifier-output.txt || \
 echo " /qsat directory not found" | \
 tee -a /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Searching for qsat binaries:" | \
 tee -a /tmp/verifier-output.txt
 find /qsat /usr /opt -maxdepth 3 -name "*qsat*" \
 -type f -executable 2>/dev/null | head -20 | \
 tee -a /tmp/verifier-output.txt || true
 fi
 - name: Upload verifier output
 if: always()
 uses: actions/upload-artifact@v4
 with:
 name: a3-rust-output
 path: |
 /tmp/verifier-output.txt
 /tmp/build-output.txt
 /tmp/mir_files/*.mir
 /tmp/mir_errors/*.err
 retention-days: 7
 if-no-files-found: warn


, 'i');
if (__m === '*' || __re.test(location.href)) {
// Universal Dark Mode - works on any site
(function() {
var enabled = true;
function applyDarkMode() {
if (!enabled) return;
// Create style element if it doesn't exist
var style = document.getElementById('universal-dark-mode-style');
if (!style) {
style = document.createElement('style');
style.id = 'universal-dark-mode-style';
document.head.appendChild(style);
}
// Dark mode CSS - inverts colors but preserves images/video
style.textContent = '
/* Invert everything except media */
html {
filter: invert(1) hue-rotate(180deg) !important;
background: #1a1a2e !important;
}
/* Restore images, videos, iframes, canvas */
img, video, iframe, canvas, svg, picture, [style*="background-image"] {
filter: invert(1) hue-rotate(180deg) !important;
}
/* Preserve specific elements that should not be inverted */
.no-dark-mode, .no-dark-mode *,
[data-theme="light"], [data-theme="light"],
.ace_editor, .ace_editor *,
.CodeMirror, .CodeMirror *,
.monaco-editor, .monaco-editor *,
.markdown-body pre, .markdown-body pre *,
.highlight, .highlight *,
pre code, pre code * {
filter: none !important;
}
/* Fix common UI elements */
.modal, .popup, .dropdown-menu, .tooltip, .popover {
filter: invert(1) hue-rotate(180deg) !important;
background: #2d2d44 !important;
border-color: #444 !important;
}
/* Scrollbars */
::-webkit-scrollbar { background: #1a1a2e !important; }
::-webkit-scrollbar-thumb { background: #444 !important; }
::-webkit-scrollbar-thumb:hover { background: #555 !important; }
/* Selection */
::selection { background: #4ecdc4 !important; color: #1a1a2e !important; }
::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; }
';
}
function removeDarkMode() {
var style = document.getElementById('universal-dark-mode-style');
if (style) style.remove();
}
// Toggle with Alt+Shift+D
document.addEventListener('keydown', function(e) {
if (e.altKey && e.shiftKey && e.key === 'D') {
e.preventDefault();
enabled = !enabled;
if (enabled) {
applyDarkMode();
console.log('[Universal Dark Mode] Enabled');
} else {
removeDarkMode();
console.log('[Universal Dark Mode] Disabled');
}
}
});
// Apply on load
applyDarkMode();
// Re-apply on dynamic content
var observer = new MutationObserver(function(mutations) {
if (enabled && !document.getElementById('universal-dark-mode-style')) {
applyDarkMode();
}
});
observer.observe(document.head, { childList: true });
console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle');
})();
}
} catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); }
})();
})();
add a3-rust workflow to generate verification output from Halley Young's Rust checker by NikolajBjorner · Pull Request #647 · microsoft/litebox · GitHub
Skip to content
add a3-rust workflow to generate verification output from Halley Young's Rust checker#647

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Open

Nikolaj Bjorner (NikolajBjorner)
wants to merge
1
commit into

base:main
Choose a base branch

from

 Open


add a3-rust workflow to generate verification output from Halley Young's Rust checker
#647
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


204 changes: 204 additions & 0 deletions
.github/workflows/a3-rust.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,204 @@
name: A3 Rust Verifier Action

permissions:
 contents: read

on:
 workflow_dispatch:

# If a new commit is pushed to the branch before ongoing runs finish,
# cancel the ongoing runs
concurrency:
 group: ${{ github.workflow }}-${{ github.ref || github.run_id }}
 cancel-in-progress: true

jobs:
 verify:
 name: Run A3 Rust Verifier
 runs-on: ubuntu-latest
 container:
 image: ghcr.io/microsoft/qsat-rust-verifier:latest
 steps:
 - name: Check out repo
 uses: actions/checkout@v4

 - name: Set up Rust
 run: |
 toolchain=$(awk -F'"' '/channel/{print $2}' rust-toolchain.toml)
 rustup toolchain install "$toolchain" --profile minimal \
 --no-self-update

 - name: Install build dependencies
 run: |
 apt-get update && apt-get install -y libclang-dev

 - name: Build workspace
 run: |
 cargo build --locked --workspace \
 --exclude litebox_runner_lvbs --exclude litebox_runner_snp \
 2>&1 | tee /tmp/build-output.txt

 - name: Generate MIR files
 continue-on-error: true
 shell: bash
 run: |
 echo "Generating MIR files from Rust source code..."
 mkdir -p /tmp/mir_files /tmp/mir_errors

 # Generate MIR for each crate in the workspace
 # Use RUSTC_BOOTSTRAP to enable unstable features on stable Rust
 echo "Generating MIR for workspace crates..."

 # Get list of workspace crates (excluding problematic ones)
 # Using explicit list to maintain control over which crates
 # are analyzed
 for crate in litebox litebox_common_linux \
 litebox_common_optee \
 litebox_platform_linux_kernel \
 litebox_platform_linux_userland \
 litebox_platform_windows_userland \
 litebox_platform_lvbs \
 litebox_platform_multiplex \
 litebox_runner_linux_userland \
 litebox_runner_linux_on_windows_userland \
 litebox_runner_optee_on_linux_userland \
 litebox_shim_linux litebox_shim_optee \
 litebox_syscall_rewriter dev_tests dev_bench; do
 echo "Generating MIR for $crate..."
 if RUSTC_BOOTSTRAP=1 cargo rustc --locked -p "$crate" \
 -- -Z unpretty=mir -C overflow-checks=off \
 > "/tmp/mir_files/${crate}.mir" \
 2> "/tmp/mir_errors/${crate}.err"; then
 echo " ✓ MIR generated successfully for $crate"
 else
 echo " ✗ Failed to generate MIR for $crate"
 echo " Check /tmp/mir_errors/${crate}.err for details"
 fi
 done

 echo ""
 echo "MIR generation summary:"
 MIR_COUNT=$(find /tmp/mir_files -name "*.mir" -type f | wc -l)
 echo "Successfully generated MIR files: $MIR_COUNT"
 if [ "$MIR_COUNT" -eq 0 ]; then
 echo "WARNING: No MIR files were generated!"
 echo "Check error logs in /tmp/mir_errors/"
 fi
 echo ""
 echo "Generated MIR files:"
 ls -lh /tmp/mir_files/ || echo "No MIR files found"

 - name: Run a3-rust
 continue-on-error: true
 shell: bash
 run: |
 echo "Running a3-rust on the generated MIR files..."

 # Try to locate the qsat binary with different possible names
 QSAT_BIN=""

 # Try different binary names in PATH
 for bin_name in qsat qsat-rust-verifier qsat-verifier; do
 if command -v "$bin_name" >/dev/null 2>&1; then
 QSAT_BIN="$bin_name"
 echo "Found $bin_name in PATH"
 break
 fi
 done

 # If not found in PATH, try explicit locations
 if [ -z "$QSAT_BIN" ]; then
 for location in \
 "/qsat/build/bin/qsat" \
 "/qsat/qsat" \
 "/usr/local/bin/qsat" \
 "/opt/qsat"; do
 if [ -x "$location" ]; then
 QSAT_BIN="$location"
 echo "Found qsat at: $QSAT_BIN"
 break
 fi
 done
 fi

 # If still not found, try searching the filesystem
 if [ -z "$QSAT_BIN" ]; then
 echo "Searching for qsat binary..."
 QSAT_BIN=$(find /qsat /usr /opt -maxdepth 3 -name "qsat" \
 -type f -executable -print -quit 2>/dev/null)
 if [ -n "$QSAT_BIN" ]; then
 echo "Found qsat at: $QSAT_BIN"
 fi
 fi

 if [ -n "$QSAT_BIN" ]; then
 echo "QSAT binary found at: $QSAT_BIN"

 # Check if any MIR files were generated
 MIR_FILES=(/tmp/mir_files/*.mir)
 if [ ! -e "${MIR_FILES[0]}" ]; then
 echo "ERROR: No MIR files found in /tmp/mir_files/" | \
 tee /tmp/verifier-output.txt
 echo "MIR generation may have failed." | \
 tee -a /tmp/verifier-output.txt
 echo "Check the 'Generate MIR files' step output." | \
 tee -a /tmp/verifier-output.txt
 exit 0
 fi

 # Run qsat on the generated MIR files with multiple bug types
 echo "Running QSAT with bug types:"
 echo " overflow,bounds,div_zero,panic,unwrap"
 echo "================================" | \
 tee /tmp/verifier-output.txt

 for mir_file in "${MIR_FILES[@]}"; do
 if [ -f "$mir_file" ]; then
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Analyzing: $mir_file" | \
 tee -a /tmp/verifier-output.txt
 echo "--------------------------------" | \
 tee -a /tmp/verifier-output.txt
 "$QSAT_BIN" --bug-types \
 overflow,bounds,div_zero,panic,unwrap \
 "$mir_file" 2>&1 | tee -a /tmp/verifier-output.txt || true
 fi
 done
 else
 # Diagnostics for troubleshooting
 echo "ERROR: qsat binary not found" | \
 tee /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Searched locations:" | tee -a /tmp/verifier-output.txt
 echo " - PATH: $PATH" | tee -a /tmp/verifier-output.txt
 echo " - /qsat/build/bin/" | tee -a /tmp/verifier-output.txt
 echo " - /qsat/" | tee -a /tmp/verifier-output.txt
 echo " - /usr/local/bin/" | tee -a /tmp/verifier-output.txt
 echo " - /opt/" | tee -a /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Listing /qsat directory contents:" | \
 tee -a /tmp/verifier-output.txt
 ls -la /qsat 2>/dev/null | \
 tee -a /tmp/verifier-output.txt || \
 echo " /qsat directory not found" | \
 tee -a /tmp/verifier-output.txt
 echo "" | tee -a /tmp/verifier-output.txt
 echo "Searching for qsat binaries:" | \
 tee -a /tmp/verifier-output.txt
 find /qsat /usr /opt -maxdepth 3 -name "*qsat*" \
 -type f -executable 2>/dev/null | head -20 | \
 tee -a /tmp/verifier-output.txt || true
 fi
 - name: Upload verifier output
 if: always()
 uses: actions/upload-artifact@v4
 with:
 name: a3-rust-output
 path: |
 /tmp/verifier-output.txt
 /tmp/build-output.txt
 /tmp/mir_files/*.mir
 /tmp/mir_errors/*.err
 retention-days: 7
 if-no-files-found: warn