3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-12 11:54:07 +00:00

update improvers

This commit is contained in:
Don Syme 2025-09-17 13:19:24 +01:00
parent 7268136bb6
commit 2364ea42ba
12 changed files with 295 additions and 228 deletions

83
.github/workflows/ask.lock.yml generated vendored
View file

@ -2,7 +2,7 @@
# To update this file, edit the corresponding .md file and run:
# gh aw compile
#
# Effective stop-time: 2025-09-19 10:32:53
# Effective stop-time: 2025-09-19 12:19:14
name: "Question Answering Researcher"
on:
@ -594,7 +594,7 @@ jobs:
main();
- name: Setup Safe Outputs Collector MCP
env:
GITHUB_AW_SAFE_OUTPUTS_CONFIG: "{\"add-issue-comment\":{\"enabled\":true}}"
GITHUB_AW_SAFE_OUTPUTS_CONFIG: "{\"add-comment\":{\"enabled\":true}}"
run: |
mkdir -p /tmp/safe-outputs
cat > /tmp/safe-outputs/mcp-server.cjs << 'EOF'
@ -747,7 +747,7 @@ jobs:
},
},
{
name: "add-issue-comment",
name: "add-comment",
description: "Add a comment to a GitHub issue or pull request",
inputSchema: {
type: "object",
@ -854,7 +854,7 @@ jobs:
},
},
{
name: "add-issue-labels",
name: "add-labels",
description: "Add labels to a GitHub issue or pull request",
inputSchema: {
type: "object",
@ -1028,7 +1028,7 @@ jobs:
- name: Setup MCPs
env:
GITHUB_AW_SAFE_OUTPUTS: ${{ env.GITHUB_AW_SAFE_OUTPUTS }}
GITHUB_AW_SAFE_OUTPUTS_CONFIG: "{\"add-issue-comment\":{\"enabled\":true}}"
GITHUB_AW_SAFE_OUTPUTS_CONFIG: "{\"add-comment\":{\"enabled\":true}}"
run: |
mkdir -p /tmp/mcp-config
cat > /tmp/mcp-config/mcp-servers.json << 'EOF'
@ -1066,7 +1066,7 @@ jobs:
WORKFLOW_NAME="Question Answering Researcher"
# Check stop-time limit
STOP_TIME="2025-09-19 10:32:53"
STOP_TIME="2025-09-19 12:19:14"
echo "Checking stop-time limit: $STOP_TIME"
# Convert stop time to epoch seconds
@ -1157,7 +1157,7 @@ jobs:
**Adding a Comment to an Issue or Pull Request**
To add a comment to an issue or pull request, use the add-issue-comments tool from the safe-outputs MCP
To add a comment to an issue or pull request, use the add-comments tool from the safe-outputs MCP
EOF
- name: Print prompt to step summary
@ -1327,7 +1327,7 @@ jobs:
uses: actions/github-script@v8
env:
GITHUB_AW_SAFE_OUTPUTS: ${{ env.GITHUB_AW_SAFE_OUTPUTS }}
GITHUB_AW_SAFE_OUTPUTS_CONFIG: "{\"add-issue-comment\":{\"enabled\":true}}"
GITHUB_AW_SAFE_OUTPUTS_CONFIG: "{\"add-comment\":{\"enabled\":true}}"
with:
script: |
async function main() {
@ -1360,15 +1360,12 @@ jobs:
let sanitized = content;
// Neutralize @mentions to prevent unintended notifications
sanitized = neutralizeMentions(sanitized);
// Remove XML comments to prevent content hiding
sanitized = removeXmlComments(sanitized);
// Remove ANSI escape sequences BEFORE removing control characters
sanitized = sanitized.replace(/\x1b\[[0-9;]*[mGKH]/g, "");
// Remove control characters (except newlines and tabs)
sanitized = sanitized.replace(/[\x00-\x08\x0B\x0C\x0E-\x1F\x7F]/g, "");
// XML character escaping
sanitized = sanitized
.replace(/&/g, "&amp;") // Must be first to avoid double-escaping
.replace(/</g, "&lt;")
.replace(/>/g, "&gt;")
.replace(/"/g, "&quot;")
.replace(/'/g, "&apos;");
// URI filtering - replace non-https protocols with "(redacted)"
sanitized = sanitizeUrlProtocols(sanitized);
// Domain filtering for HTTPS URIs
@ -1388,8 +1385,7 @@ jobs:
lines.slice(0, maxLines).join("\n") +
"\n[Content truncated due to line count]";
}
// Remove ANSI escape sequences
sanitized = sanitized.replace(/\x1b\[[0-9;]*[mGKH]/g, "");
// ANSI escape sequences already removed earlier in the function
// Neutralize common bot trigger phrases
sanitized = neutralizeBotTriggers(sanitized);
// Trim excessive whitespace
@ -1401,10 +1397,12 @@ jobs:
*/
function sanitizeUrlDomains(s) {
return s.replace(
/\bhttps:\/\/([^\/\s\])}'"<>&\x00-\x1f]+)/gi,
(match, domain) => {
/\bhttps:\/\/[^\s\])}'"<>&\x00-\x1f,;]+/gi,
(match) => {
// Extract just the URL part after https://
const urlAfterProtocol = match.slice(8); // Remove 'https://'
// Extract the hostname part (before first slash, colon, or other delimiter)
const hostname = domain.split(/[\/:\?#]/)[0].toLowerCase();
const hostname = urlAfterProtocol.split(/[\/:\?#]/)[0].toLowerCase();
// Check if this domain or any parent domain is in the allowlist
const isAllowed = allowedDomains.some(allowedDomain => {
const normalizedAllowed = allowedDomain.toLowerCase();
@ -1423,9 +1421,10 @@ jobs:
* @returns {string} The string with non-https protocols redacted
*/
function sanitizeUrlProtocols(s) {
// Match both protocol:// and protocol: patterns
// Match protocol:// patterns (URLs) and standalone protocol: patterns that look like URLs
// Avoid matching command line flags like -v:10 or z3 -memory:high
return s.replace(
/\b(\w+):(?:\/\/)?[^\s\])}'"<>&\x00-\x1f]+/gi,
/\b(\w+):\/\/[^\s\])}'"<>&\x00-\x1f]+/gi,
(match, protocol) => {
// Allow https (case insensitive), redact everything else
return protocol.toLowerCase() === "https" ? match : "(redacted)";
@ -1444,6 +1443,16 @@ jobs:
(_m, p1, p2) => `${p1}\`@${p2}\``
);
}
/**
* Removes XML comments to prevent content hiding
* @param {string} s - The string to process
* @returns {string} The string with XML comments removed
*/
function removeXmlComments(s) {
// Remove XML/HTML comments including malformed ones that might be used to hide content
// Matches: <!-- ... --> and <!--- ... --> and <!--- ... --!> variations
return s.replace(/<!--[\s\S]*?-->/g, "").replace(/<!--[\s\S]*?--!>/g, "");
}
/**
* Neutralizes bot trigger phrases by wrapping them in backticks
* @param {string} s - The string to process
@ -1477,13 +1486,13 @@ jobs:
switch (itemType) {
case "create-issue":
return 1; // Only one issue allowed
case "add-issue-comment":
case "add-comment":
return 1; // Only one comment allowed
case "create-pull-request":
return 1; // Only one pull request allowed
case "create-pull-request-review-comment":
return 10; // Default to 10 review comments allowed
case "add-issue-labels":
case "add-labels":
return 5; // Only one labels operation allowed
case "update-issue":
return 1; // Only one issue update allowed
@ -1698,10 +1707,10 @@ jobs:
);
}
break;
case "add-issue-comment":
case "add-comment":
if (!item.body || typeof item.body !== "string") {
errors.push(
`Line ${i + 1}: add-issue-comment requires a 'body' string field`
`Line ${i + 1}: add-comment requires a 'body' string field`
);
continue;
}
@ -1736,10 +1745,10 @@ jobs:
);
}
break;
case "add-issue-labels":
case "add-labels":
if (!item.labels || !Array.isArray(item.labels)) {
errors.push(
`Line ${i + 1}: add-issue-labels requires a 'labels' array field`
`Line ${i + 1}: add-labels requires a 'labels' array field`
);
continue;
}
@ -1749,7 +1758,7 @@ jobs:
)
) {
errors.push(
`Line ${i + 1}: add-issue-labels labels array must contain only strings`
`Line ${i + 1}: add-labels labels array must contain only strings`
);
continue;
}
@ -2671,11 +2680,11 @@ jobs:
pull-requests: write
timeout-minutes: 10
outputs:
comment_id: ${{ steps.create_comment.outputs.comment_id }}
comment_url: ${{ steps.create_comment.outputs.comment_url }}
comment_id: ${{ steps.add_comment.outputs.comment_id }}
comment_url: ${{ steps.add_comment.outputs.comment_url }}
steps:
- name: Add Issue Comment
id: create_comment
id: add_comment
uses: actions/github-script@v8
env:
GITHUB_AW_AGENT_OUTPUT: ${{ needs.question-answering-researcher.outputs.output }}
@ -2709,15 +2718,15 @@ jobs:
core.info("No valid items found in agent output");
return;
}
// Find all add-issue-comment items
// Find all add-comment items
const commentItems = validatedOutput.items.filter(
/** @param {any} item */ item => item.type === "add-issue-comment"
/** @param {any} item */ item => item.type === "add-comment"
);
if (commentItems.length === 0) {
core.info("No add-issue-comment items found in agent output");
core.info("No add-comment items found in agent output");
return;
}
core.info(`Found ${commentItems.length} add-issue-comment item(s)`);
core.info(`Found ${commentItems.length} add-comment item(s)`);
// If in staged mode, emit step summary instead of creating comments
if (isStaged) {
let summaryContent = "## 🎭 Staged Mode: Add Comments Preview\n\n";
@ -2761,7 +2770,7 @@ jobs:
for (let i = 0; i < commentItems.length; i++) {
const commentItem = commentItems[i];
core.info(
`Processing add-issue-comment item ${i + 1}/${commentItems.length}: bodyLength=${commentItem.body.length}`
`Processing add-comment item ${i + 1}/${commentItems.length}: bodyLength=${commentItem.body.length}`
);
// Determine the issue/PR number and comment endpoint for this comment
let issueNumber;