3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00

add retry, rename to optibot

This commit is contained in:
Nikolaj Bjorner 2025-02-14 08:39:21 -08:00
parent 6b9ce8638f
commit 0cf2b5f515
2 changed files with 76 additions and 24 deletions

View file

@ -74,7 +74,11 @@ export async function mergeModifiedFunction(code: string, funs: { code: string,
return code; return code;
} }
async function canCompileCode(inputFile: WorkspaceFile, new_code: string) { class ShellOutputRef {
shellOutput: ShellOutput;
}
async function canCompileCode(inputFile: WorkspaceFile, new_code: string, result: ShellOutputRef) {
// //
// move input file to a temp file // move input file to a temp file
@ -88,15 +92,47 @@ async function canCompileCode(inputFile: WorkspaceFile, new_code: string) {
let old_code = inputFile.content; let old_code = inputFile.content;
await workspace.writeText(tempFile, old_code); await workspace.writeText(tempFile, old_code);
await workspace.writeText(inputFile.filename, new_code); await workspace.writeText(inputFile.filename, new_code);
let result = await host.exec(`cmd /k "C:\Program\ Files/Microsoft\ Visual\ Studio/2022/Enterprise/Common7/Tools/VsDevCmd.bat" -arch=x64 & ninja`, { cwd: "build" }); result.shellOutput = await host.exec(`cmd /k "C:/Program\ Files/Microsoft\ Visual\ Studio/2022/Enterprise/Common7/Tools/VsDevCmd.bat" -arch=x64 & ninja`, { cwd: "build" });
await workspace.writeText(inputFile.filename, old_code); await workspace.writeText(inputFile.filename, old_code);
if (result.exitCode == 0) { console.log(result.shellOutput.stdout);
console.log(result.shellOutput.stderr);
let has_failed = result.shellOutput.stdout.search("failed");
if (has_failed != -1) {
console.log("Failed to compile");
return false;
}
if (result.shellOutput.exitCode == 0) {
await workspace.writeText(tempFile, new_code); await workspace.writeText(tempFile, new_code);
return true; return true;
} }
console.log(result.stderr);
return false; return false;
}
async function llmFixCompilerErrors(inputFile: WorkspaceFile, new_code: string, result: ShellOutput) {
let answer = await runPrompt(
(_) => {
_.def("CODE", new_code);
_.def("OUTPUT", result.stderr + result.stdout);
_.$`You are a highly experienced compiler engineer with over 20 years of expertise,
specializing in C and C++ programming. Your deep knowledge of best coding practices
and software engineering principles enables you to produce robust, efficient, and
maintainable code in any scenario.
Please modify the original code in <CODE> to ensure that it compiles without any errors.
The compiler produced the output <OUTPUT> when building <CODE>.
`
}, {
system: [],
systemSafety: false
}
);
let new_code_input = answer.text;
let match_new_code = new_code_input.match(/```cpp([\s\S]*?)```/);
if (!match_new_code) {
console.log("Invalid new code");
return new_code;
}
return match_new_code[1];
} }
export async function mergeCompileFunction(inputFile: WorkspaceFile, code: string, funs: { code: string, name: string }[], new_code_input: string) { export async function mergeCompileFunction(inputFile: WorkspaceFile, code: string, funs: { code: string, name: string }[], new_code_input: string) {
@ -106,7 +142,9 @@ export async function mergeCompileFunction(inputFile: WorkspaceFile, code: strin
return code; return code;
} }
let new_code = match_new_code[1]; let new_code = match_new_code[1];
let retry_count = 0;
while (retry_count < 2) {
let name = function_name_from_code(new_code); let name = function_name_from_code(new_code);
let fun = funs.find(f => f.name == name); let fun = funs.find(f => f.name == name);
@ -124,10 +162,16 @@ export async function mergeCompileFunction(inputFile: WorkspaceFile, code: strin
console.log("No change in function: " + name); console.log("No change in function: " + name);
return code; return code;
} }
let canCompile = await canCompileCode(inputFile, modified_code); let result = new ShellOutputRef();
let canCompile = await canCompileCode(inputFile, modified_code, result);
console.log("Can compile: " + canCompile); console.log("Can compile: " + canCompile);
if (canCompile) if (canCompile)
return modified_code; return modified_code;
if (retry_count > 0)
break;
retry_count++;
new_code = await llmFixCompilerErrors(inputFile, new_code, result.shellOutput);
}
return code; return code;
} }
@ -153,7 +197,13 @@ export async function invokeLLMOpt(code: string) {
and software engineering principles enables you to produce robust, efficient, and and software engineering principles enables you to produce robust, efficient, and
maintainable code in any scenario. maintainable code in any scenario.
Please modify the original code in <CODE> to ensure that it uses best practices for optimal code execution.' ` Please modify the original code in <CODE> to ensure that it uses best practices for optimal code execution.
- do not use assert. Instead use SASSERT.
- do not change function signatures.
- do not use std::vector.
- do not add new comments.
- do not split functions into multiple functions.`
}, { }, {
system: [], system: [],
systemSafety: false systemSafety: false

View file

@ -10,6 +10,8 @@ const inputFile = env.files[0];
let funs = await splitFunctions(inputFile); let funs = await splitFunctions(inputFile);
let new_code = inputFile.content; let new_code = inputFile.content;
for (const fun of funs) { for (const fun of funs) {
if (fun.code.length < 200) // don't sweat the small stuff
continue;
let answer = await invokeLLMOpt(fun.code); let answer = await invokeLLMOpt(fun.code);
if (answer) if (answer)
new_code = await mergeCompileFunction(inputFile, new_code, funs, answer); new_code = await mergeCompileFunction(inputFile, new_code, funs, answer);