mirror of
https://github.com/Z3Prover/z3
synced 2026-02-26 18:15:37 +00:00
Update api-coherence-checker to search for Rust traits and trait implementations
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot]
parent
a0a44c5571
commit
bf934398d7
2 changed files with 128 additions and 119 deletions
245
.github/workflows/api-coherence-checker.lock.yml
generated
vendored
245
.github/workflows/api-coherence-checker.lock.yml
generated
vendored
|
|
@ -13,7 +13,7 @@
|
|||
# \ /\ / (_) | | | | ( | | | | (_) \ V V /\__ \
|
||||
# \/ \/ \___/|_| |_|\_\|_| |_|\___/ \_/\_/ |___/
|
||||
#
|
||||
# This file was automatically generated by gh-aw (v0.50.0). DO NOT EDIT.
|
||||
# This file was automatically generated by gh-aw (v0.50.1). DO NOT EDIT.
|
||||
#
|
||||
# To update this file, edit the corresponding .md file and run:
|
||||
# gh aw compile
|
||||
|
|
@ -23,7 +23,7 @@
|
|||
#
|
||||
# Daily API coherence checker across Z3's multi-language bindings including Rust
|
||||
#
|
||||
# gh-aw-metadata: {"schema_version":"v1","frontmatter_hash":"598c1f5c864f7f50ae4874ea58b6a0fb58480c7220cbbd8c9cd2e9386320c5af","compiler_version":"v0.50.0"}
|
||||
# gh-aw-metadata: {"schema_version":"v1","frontmatter_hash":"598c1f5c864f7f50ae4874ea58b6a0fb58480c7220cbbd8c9cd2e9386320c5af","compiler_version":"v0.50.1"}
|
||||
|
||||
name: "API Coherence Checker"
|
||||
"on":
|
||||
|
|
@ -49,7 +49,7 @@ jobs:
|
|||
comment_repo: ""
|
||||
steps:
|
||||
- name: Setup Scripts
|
||||
uses: github/gh-aw/actions/setup@v0.50.0
|
||||
uses: github/gh-aw/actions/setup@v0.50.1
|
||||
with:
|
||||
destination: /opt/gh-aw/actions
|
||||
- name: Validate context variables
|
||||
|
|
@ -229,6 +229,8 @@ jobs:
|
|||
GH_AW_WORKFLOW_ID_SANITIZED: apicoherencechecker
|
||||
outputs:
|
||||
checkout_pr_success: ${{ steps.checkout-pr.outputs.checkout_pr_success || 'true' }}
|
||||
detection_conclusion: ${{ steps.detection_conclusion.outputs.conclusion }}
|
||||
detection_success: ${{ steps.detection_conclusion.outputs.success }}
|
||||
has_patch: ${{ steps.collect_output.outputs.has_patch }}
|
||||
model: ${{ steps.generate_aw_info.outputs.model }}
|
||||
output: ${{ steps.collect_output.outputs.output }}
|
||||
|
|
@ -236,7 +238,7 @@ jobs:
|
|||
secret_verification_result: ${{ steps.validate-secret.outputs.verification_result }}
|
||||
steps:
|
||||
- name: Setup Scripts
|
||||
uses: github/gh-aw/actions/setup@v0.50.0
|
||||
uses: github/gh-aw/actions/setup@v0.50.1
|
||||
with:
|
||||
destination: /opt/gh-aw/actions
|
||||
- name: Create gh-aw temp directory
|
||||
|
|
@ -295,7 +297,7 @@ jobs:
|
|||
model: process.env.GH_AW_MODEL_AGENT_COPILOT || "",
|
||||
version: "",
|
||||
agent_version: "0.0.415",
|
||||
cli_version: "v0.50.0",
|
||||
cli_version: "v0.50.1",
|
||||
workflow_name: "API Coherence Checker",
|
||||
experimental: false,
|
||||
supports_tools_allowlist: true,
|
||||
|
|
@ -821,12 +823,124 @@ jobs:
|
|||
/tmp/gh-aw/agent-stdio.log
|
||||
/tmp/gh-aw/agent/
|
||||
if-no-files-found: ignore
|
||||
# --- Threat Detection (inline) ---
|
||||
- name: Check if detection needed
|
||||
id: detection_guard
|
||||
if: always()
|
||||
env:
|
||||
OUTPUT_TYPES: ${{ steps.collect_output.outputs.output_types }}
|
||||
HAS_PATCH: ${{ steps.collect_output.outputs.has_patch }}
|
||||
run: |
|
||||
if [[ -n "$OUTPUT_TYPES" || "$HAS_PATCH" == "true" ]]; then
|
||||
echo "run_detection=true" >> "$GITHUB_OUTPUT"
|
||||
echo "Detection will run: output_types=$OUTPUT_TYPES, has_patch=$HAS_PATCH"
|
||||
else
|
||||
echo "run_detection=false" >> "$GITHUB_OUTPUT"
|
||||
echo "Detection skipped: no agent outputs or patches to analyze"
|
||||
fi
|
||||
- name: Clear MCP configuration for detection
|
||||
if: always() && steps.detection_guard.outputs.run_detection == 'true'
|
||||
run: |
|
||||
rm -f /tmp/gh-aw/mcp-config/mcp-servers.json
|
||||
rm -f /home/runner/.copilot/mcp-config.json
|
||||
rm -f "$GITHUB_WORKSPACE/.gemini/settings.json"
|
||||
- name: Prepare threat detection files
|
||||
if: always() && steps.detection_guard.outputs.run_detection == 'true'
|
||||
run: |
|
||||
mkdir -p /tmp/gh-aw/threat-detection/aw-prompts
|
||||
cp /tmp/gh-aw/aw-prompts/prompt.txt /tmp/gh-aw/threat-detection/aw-prompts/prompt.txt 2>/dev/null || true
|
||||
cp /tmp/gh-aw/agent_output.json /tmp/gh-aw/threat-detection/agent_output.json 2>/dev/null || true
|
||||
for f in /tmp/gh-aw/aw-*.patch; do
|
||||
[ -f "$f" ] && cp "$f" /tmp/gh-aw/threat-detection/ 2>/dev/null || true
|
||||
done
|
||||
echo "Prepared threat detection files:"
|
||||
ls -la /tmp/gh-aw/threat-detection/ 2>/dev/null || true
|
||||
- name: Setup threat detection
|
||||
if: always() && steps.detection_guard.outputs.run_detection == 'true'
|
||||
uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
|
||||
env:
|
||||
WORKFLOW_NAME: "API Coherence Checker"
|
||||
WORKFLOW_DESCRIPTION: "Daily API coherence checker across Z3's multi-language bindings including Rust"
|
||||
HAS_PATCH: ${{ steps.collect_output.outputs.has_patch }}
|
||||
with:
|
||||
script: |
|
||||
const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
|
||||
setupGlobals(core, github, context, exec, io);
|
||||
const { main } = require('/opt/gh-aw/actions/setup_threat_detection.cjs');
|
||||
await main();
|
||||
- name: Ensure threat-detection directory and log
|
||||
if: always() && steps.detection_guard.outputs.run_detection == 'true'
|
||||
run: |
|
||||
mkdir -p /tmp/gh-aw/threat-detection
|
||||
touch /tmp/gh-aw/threat-detection/detection.log
|
||||
- name: Execute GitHub Copilot CLI
|
||||
if: always() && steps.detection_guard.outputs.run_detection == 'true'
|
||||
id: detection_agentic_execution
|
||||
# Copilot CLI tool arguments (sorted):
|
||||
# --allow-tool shell(cat)
|
||||
# --allow-tool shell(grep)
|
||||
# --allow-tool shell(head)
|
||||
# --allow-tool shell(jq)
|
||||
# --allow-tool shell(ls)
|
||||
# --allow-tool shell(tail)
|
||||
# --allow-tool shell(wc)
|
||||
timeout-minutes: 20
|
||||
run: |
|
||||
set -o pipefail
|
||||
sudo -E awf --env-all --container-workdir "${GITHUB_WORKSPACE}" --allow-domains "api.business.githubcopilot.com,api.enterprise.githubcopilot.com,api.github.com,api.githubcopilot.com,api.individual.githubcopilot.com,github.com,host.docker.internal,raw.githubusercontent.com,registry.npmjs.org,telemetry.enterprise.githubcopilot.com" --log-level info --proxy-logs-dir /tmp/gh-aw/sandbox/firewall/logs --enable-host-access --image-tag 0.20.2 --skip-pull --enable-api-proxy \
|
||||
-- /bin/bash -c '/usr/local/bin/copilot --add-dir /tmp/gh-aw/ --log-level all --log-dir /tmp/gh-aw/sandbox/agent/logs/ --add-dir "${GITHUB_WORKSPACE}" --disable-builtin-mcps --allow-tool '\''shell(cat)'\'' --allow-tool '\''shell(grep)'\'' --allow-tool '\''shell(head)'\'' --allow-tool '\''shell(jq)'\'' --allow-tool '\''shell(ls)'\'' --allow-tool '\''shell(tail)'\'' --allow-tool '\''shell(wc)'\'' --prompt "$(cat /tmp/gh-aw/aw-prompts/prompt.txt)"${GH_AW_MODEL_DETECTION_COPILOT:+ --model "$GH_AW_MODEL_DETECTION_COPILOT"}' 2>&1 | tee -a /tmp/gh-aw/threat-detection/detection.log
|
||||
env:
|
||||
COPILOT_AGENT_RUNNER_TYPE: STANDALONE
|
||||
COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
|
||||
GH_AW_MODEL_DETECTION_COPILOT: ${{ vars.GH_AW_MODEL_DETECTION_COPILOT || '' }}
|
||||
GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt
|
||||
GITHUB_HEAD_REF: ${{ github.head_ref }}
|
||||
GITHUB_REF_NAME: ${{ github.ref_name }}
|
||||
GITHUB_STEP_SUMMARY: ${{ env.GITHUB_STEP_SUMMARY }}
|
||||
GITHUB_WORKSPACE: ${{ github.workspace }}
|
||||
XDG_CONFIG_HOME: /home/runner
|
||||
- name: Parse threat detection results
|
||||
id: parse_detection_results
|
||||
if: always() && steps.detection_guard.outputs.run_detection == 'true'
|
||||
uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
|
||||
with:
|
||||
script: |
|
||||
const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
|
||||
setupGlobals(core, github, context, exec, io);
|
||||
const { main } = require('/opt/gh-aw/actions/parse_threat_detection_results.cjs');
|
||||
await main();
|
||||
- name: Upload threat detection log
|
||||
if: always() && steps.detection_guard.outputs.run_detection == 'true'
|
||||
uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6
|
||||
with:
|
||||
name: threat-detection.log
|
||||
path: /tmp/gh-aw/threat-detection/detection.log
|
||||
if-no-files-found: ignore
|
||||
- name: Set detection conclusion
|
||||
id: detection_conclusion
|
||||
if: always()
|
||||
env:
|
||||
RUN_DETECTION: ${{ steps.detection_guard.outputs.run_detection }}
|
||||
DETECTION_SUCCESS: ${{ steps.parse_detection_results.outputs.success }}
|
||||
run: |
|
||||
if [[ "$RUN_DETECTION" != "true" ]]; then
|
||||
echo "conclusion=skipped" >> "$GITHUB_OUTPUT"
|
||||
echo "success=true" >> "$GITHUB_OUTPUT"
|
||||
echo "Detection was not needed, marking as skipped"
|
||||
elif [[ "$DETECTION_SUCCESS" == "true" ]]; then
|
||||
echo "conclusion=success" >> "$GITHUB_OUTPUT"
|
||||
echo "success=true" >> "$GITHUB_OUTPUT"
|
||||
echo "Detection passed successfully"
|
||||
else
|
||||
echo "conclusion=failure" >> "$GITHUB_OUTPUT"
|
||||
echo "success=false" >> "$GITHUB_OUTPUT"
|
||||
echo "Detection found issues"
|
||||
fi
|
||||
|
||||
conclusion:
|
||||
needs:
|
||||
- activation
|
||||
- agent
|
||||
- detection
|
||||
- safe_outputs
|
||||
- update_cache_memory
|
||||
if: (always()) && (needs.agent.result != 'skipped')
|
||||
|
|
@ -841,7 +955,7 @@ jobs:
|
|||
total_count: ${{ steps.missing_tool.outputs.total_count }}
|
||||
steps:
|
||||
- name: Setup Scripts
|
||||
uses: github/gh-aw/actions/setup@v0.50.0
|
||||
uses: github/gh-aw/actions/setup@v0.50.1
|
||||
with:
|
||||
destination: /opt/gh-aw/actions
|
||||
- name: Download agent output artifact
|
||||
|
|
@ -921,112 +1035,9 @@ jobs:
|
|||
const { main } = require('/opt/gh-aw/actions/handle_noop_message.cjs');
|
||||
await main();
|
||||
|
||||
detection:
|
||||
needs: agent
|
||||
if: needs.agent.outputs.output_types != '' || needs.agent.outputs.has_patch == 'true'
|
||||
runs-on: ubuntu-latest
|
||||
permissions: {}
|
||||
concurrency:
|
||||
group: "gh-aw-copilot-${{ github.workflow }}"
|
||||
timeout-minutes: 10
|
||||
outputs:
|
||||
success: ${{ steps.parse_results.outputs.success }}
|
||||
steps:
|
||||
- name: Setup Scripts
|
||||
uses: github/gh-aw/actions/setup@v0.50.0
|
||||
with:
|
||||
destination: /opt/gh-aw/actions
|
||||
- name: Download agent artifacts
|
||||
continue-on-error: true
|
||||
uses: actions/download-artifact@018cc2cf5baa6db3ef3c5f8a56943fffe632ef53 # v6
|
||||
with:
|
||||
name: agent-artifacts
|
||||
path: /tmp/gh-aw/threat-detection/
|
||||
- name: Download agent output artifact
|
||||
continue-on-error: true
|
||||
uses: actions/download-artifact@018cc2cf5baa6db3ef3c5f8a56943fffe632ef53 # v6
|
||||
with:
|
||||
name: agent-output
|
||||
path: /tmp/gh-aw/threat-detection/
|
||||
- name: Print agent output types
|
||||
env:
|
||||
AGENT_OUTPUT_TYPES: ${{ needs.agent.outputs.output_types }}
|
||||
run: |
|
||||
echo "Agent output-types: $AGENT_OUTPUT_TYPES"
|
||||
- name: Setup threat detection
|
||||
uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
|
||||
env:
|
||||
WORKFLOW_NAME: "API Coherence Checker"
|
||||
WORKFLOW_DESCRIPTION: "Daily API coherence checker across Z3's multi-language bindings including Rust"
|
||||
HAS_PATCH: ${{ needs.agent.outputs.has_patch }}
|
||||
with:
|
||||
script: |
|
||||
const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
|
||||
setupGlobals(core, github, context, exec, io);
|
||||
const { main } = require('/opt/gh-aw/actions/setup_threat_detection.cjs');
|
||||
await main();
|
||||
- name: Ensure threat-detection directory and log
|
||||
run: |
|
||||
mkdir -p /tmp/gh-aw/threat-detection
|
||||
touch /tmp/gh-aw/threat-detection/detection.log
|
||||
- name: Validate COPILOT_GITHUB_TOKEN secret
|
||||
id: validate-secret
|
||||
run: /opt/gh-aw/actions/validate_multi_secret.sh COPILOT_GITHUB_TOKEN 'GitHub Copilot CLI' https://github.github.com/gh-aw/reference/engines/#github-copilot-default
|
||||
env:
|
||||
COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
|
||||
- name: Install GitHub Copilot CLI
|
||||
run: /opt/gh-aw/actions/install_copilot_cli.sh 0.0.415
|
||||
- name: Execute GitHub Copilot CLI
|
||||
id: agentic_execution
|
||||
# Copilot CLI tool arguments (sorted):
|
||||
# --allow-tool shell(cat)
|
||||
# --allow-tool shell(grep)
|
||||
# --allow-tool shell(head)
|
||||
# --allow-tool shell(jq)
|
||||
# --allow-tool shell(ls)
|
||||
# --allow-tool shell(tail)
|
||||
# --allow-tool shell(wc)
|
||||
timeout-minutes: 20
|
||||
run: |
|
||||
set -o pipefail
|
||||
COPILOT_CLI_INSTRUCTION="$(cat /tmp/gh-aw/aw-prompts/prompt.txt)"
|
||||
mkdir -p /tmp/
|
||||
mkdir -p /tmp/gh-aw/
|
||||
mkdir -p /tmp/gh-aw/agent/
|
||||
mkdir -p /tmp/gh-aw/sandbox/agent/logs/
|
||||
copilot --add-dir /tmp/ --add-dir /tmp/gh-aw/ --add-dir /tmp/gh-aw/agent/ --log-level all --log-dir /tmp/gh-aw/sandbox/agent/logs/ --disable-builtin-mcps --allow-tool 'shell(cat)' --allow-tool 'shell(grep)' --allow-tool 'shell(head)' --allow-tool 'shell(jq)' --allow-tool 'shell(ls)' --allow-tool 'shell(tail)' --allow-tool 'shell(wc)' --prompt "$COPILOT_CLI_INSTRUCTION"${GH_AW_MODEL_DETECTION_COPILOT:+ --model "$GH_AW_MODEL_DETECTION_COPILOT"} 2>&1 | tee /tmp/gh-aw/threat-detection/detection.log
|
||||
env:
|
||||
COPILOT_AGENT_RUNNER_TYPE: STANDALONE
|
||||
COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
|
||||
GH_AW_MODEL_DETECTION_COPILOT: ${{ vars.GH_AW_MODEL_DETECTION_COPILOT || '' }}
|
||||
GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt
|
||||
GITHUB_HEAD_REF: ${{ github.head_ref }}
|
||||
GITHUB_REF_NAME: ${{ github.ref_name }}
|
||||
GITHUB_STEP_SUMMARY: ${{ env.GITHUB_STEP_SUMMARY }}
|
||||
GITHUB_WORKSPACE: ${{ github.workspace }}
|
||||
XDG_CONFIG_HOME: /home/runner
|
||||
- name: Parse threat detection results
|
||||
id: parse_results
|
||||
uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
|
||||
with:
|
||||
script: |
|
||||
const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
|
||||
setupGlobals(core, github, context, exec, io);
|
||||
const { main } = require('/opt/gh-aw/actions/parse_threat_detection_results.cjs');
|
||||
await main();
|
||||
- name: Upload threat detection log
|
||||
if: always()
|
||||
uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6
|
||||
with:
|
||||
name: threat-detection.log
|
||||
path: /tmp/gh-aw/threat-detection/detection.log
|
||||
if-no-files-found: ignore
|
||||
|
||||
safe_outputs:
|
||||
needs:
|
||||
- agent
|
||||
- detection
|
||||
if: ((!cancelled()) && (needs.agent.result != 'skipped')) && (needs.detection.outputs.success == 'true')
|
||||
needs: agent
|
||||
if: ((!cancelled()) && (needs.agent.result != 'skipped')) && (needs.agent.outputs.detection_success == 'true')
|
||||
runs-on: ubuntu-slim
|
||||
permissions:
|
||||
contents: read
|
||||
|
|
@ -1046,7 +1057,7 @@ jobs:
|
|||
process_safe_outputs_temporary_id_map: ${{ steps.process_safe_outputs.outputs.temporary_id_map }}
|
||||
steps:
|
||||
- name: Setup Scripts
|
||||
uses: github/gh-aw/actions/setup@v0.50.0
|
||||
uses: github/gh-aw/actions/setup@v0.50.1
|
||||
with:
|
||||
destination: /opt/gh-aw/actions
|
||||
- name: Download agent output artifact
|
||||
|
|
@ -1082,17 +1093,15 @@ jobs:
|
|||
if-no-files-found: warn
|
||||
|
||||
update_cache_memory:
|
||||
needs:
|
||||
- agent
|
||||
- detection
|
||||
if: always() && needs.detection.outputs.success == 'true'
|
||||
needs: agent
|
||||
if: always() && needs.agent.outputs.detection_success == 'true'
|
||||
runs-on: ubuntu-latest
|
||||
permissions: {}
|
||||
env:
|
||||
GH_AW_WORKFLOW_ID_SANITIZED: apicoherencechecker
|
||||
steps:
|
||||
- name: Setup Scripts
|
||||
uses: github/gh-aw/actions/setup@v0.50.0
|
||||
uses: github/gh-aw/actions/setup@v0.50.1
|
||||
with:
|
||||
destination: /opt/gh-aw/actions
|
||||
- name: Download cache-memory artifact (default)
|
||||
|
|
|
|||
2
.github/workflows/api-coherence-checker.md
vendored
2
.github/workflows/api-coherence-checker.md
vendored
|
|
@ -97,7 +97,7 @@ For each selected API family:
|
|||
- **C++**: Use grep/glob to search for function declarations in `z3++.h`
|
||||
- **OCaml**: Use grep/glob to search for function definitions in `.ml` and `.mli` files
|
||||
- **Go**: Use grep/glob to search for function and method definitions in `src/api/go/*.go` files
|
||||
- **Rust**: Clone the external repo (`git clone --depth=1 https://github.com/prove-rs/z3.rs /tmp/z3.rs`) and use grep/glob to search for public types, methods, and functions in `/tmp/z3.rs/z3/src/*.rs`
|
||||
- **Rust**: Clone the external repo (`git clone --depth=1 https://github.com/prove-rs/z3.rs /tmp/z3.rs`) and use grep/glob to search for public types, methods, functions, traits, and trait implementations in `/tmp/z3.rs/z3/src/*.rs`. Note that trait implementations (`impl Trait for Type`) do not use the `pub` keyword in Rust but are as public as the type and trait themselves, so search for `impl ` patterns in addition to `pub ` patterns to find them.
|
||||
|
||||
3. **Compare implementations** across languages:
|
||||
- Is the same functionality available in all languages?
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue