3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00

add prompt to ask for patch, assume directory alignment

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-02-11 16:01:30 -08:00
parent 253e44faf8
commit 1a77622714

View file

@ -8,6 +8,21 @@ import * as fs from 'fs';
import * as path from 'path'; import * as path from 'path';
async function runCodePrompt(role, message, code) {
const answer = await runPrompt(
(_) => {
_.def("ROLE", role);
_.def("REQUEST", message);
_.def("CODE", code);
_.$`Your role is <ROLE>.
The request is given by <REQUEST>
original code snippet:
<CODE>.`
}
)
console.log(answer.text);
return answer.text;
}
async function invokeLLMCompletion(code, prefix) { async function invokeLLMCompletion(code, prefix) {
@ -22,19 +37,7 @@ async function invokeLLMCompletion(code, prefix) {
successful compilation and execution. Avoid unnecessary code additions. successful compilation and execution. Avoid unnecessary code additions.
Ensure the final code is robust, secure, and adheres to best practices.`; Ensure the final code is robust, secure, and adheres to best practices.`;
const answer = await runPrompt( return runCodePrompt(role, userMessage, code);
(_) => {
_.def("ROLE", role);
_.def("REQUEST", userMessage);
_.def("CODE", code);
_.$`Your role is ROLE.
The request is given by REQUEST
original code snippet:
CODE.`
}
)
console.log(answer.text);
return answer.text;
} }
async function invokeLLMAnalyzer(code, inputFilename, funcName) { async function invokeLLMAnalyzer(code, inputFilename, funcName) {
@ -66,50 +69,81 @@ async function invokeLLMAnalyzer(code, inputFilename, funcName) {
- Explanation of optimizations and their expected benefits. - Explanation of optimizations and their expected benefits.
4. **Additional Insights or Best Practices:** 4. **Additional Insights or Best Practices:**
- Suggestions to further enhance the code's quality and maintainability.` - Suggestions to further enhance the code's quality and maintainability.`;
const answer = await runPrompt( return runCodePrompt(role, userMessage, code);
}
async function createGitUpdateRequest(src_directory : string, filename : string, modifiedCode : string) {
// extract relative path from filename after slice_directory, extract function and source file name.
// Relative path: code_slices\ast\sls\orig_sls_smt_solver.cpp_updt_params.cpp file name: orig_sls_smt.cpp
const regex = /code_slices\\(.*)\\([^_]*)_(.*)\.cpp_(.*)\.cpp/;
const match = filename.match(regex);
if (!match) {
console.log(`Filename does not match expected pattern: ${filename}`);
return "";
}
const [_, relative_path, prefix, fileName, funcName] = match;
console.log(`Relative path: ${relative_path} file name: ${fileName}.cpp`);
const srcFilePath = path.join(src_directory, relative_path, fileName + ".cpp");
const srcFileContent = await workspace.readText(srcFilePath);
let role =
`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.`;
const answer = await runPrompt(
(_) => { (_) => {
_.def("ROLE", role); _.def("ROLE", role);
_.def("REQUEST", userMessage); _.def("SOURCE", srcFileContent);
_.def("CODE", code); _.def("REVIEW", modifiedCode);
_.$`Your role is ROLE. _.def("FUNCTION", funcName);
The request is given by REQUEST _.$`Your role is <ROLE>.
original code snippet: Please create a well-formed git patch based on the source code given in
CODE.` <SOURCE>
A code analysis is for the method or function <FUNCTION>.
The analysis is he following:
<REVIEW>`
} }
) )
console.log(answer.text); console.log(answer.text);
return answer.text; return answer.text;
}
}
const input_directory = "code_slices"; const input_directory = "code_slices";
const output_directory = "code_slices_analyzed"; const output_directory = "code_slices_analyzed";
const code_slice_files = fs.readdirSync(input_directory); const src_directory = "src";
const code_slice_files = await workspace.findFiles("code_slices/**/*.cpp");
let count = 0; let count = 0;
for (const file of code_slice_files) { for (const file of code_slice_files) {
if (path.extname(file) === '.cpp') { if (path.extname(file.filename) === '.cpp') {
console.log(`Processing file: ${file}`); console.log(`Processing file: ${file.filename}`);
const regex = /(.*)_(.*)\.cpp_(.*)\.cpp/; const regex = /(.*)_(.*)\.cpp_(.*)\.cpp/;
const match = file.match(regex); const match = file.filename.match(regex);
if (!match) { if (!match) {
console.log(`Filename does not match expected pattern: ${file}`); console.log(`Filename does not match expected pattern: ${file.filename}`);
continue; continue;
} }
const [_, prefix, fileName, funcName] = match; const [_, prefix, fileName, funcName] = match;
const content = file.content;
const filePath = path.join(input_directory, file); const answer1 = await invokeLLMCompletion(content, fileName);
const content = await workspace.readText(filePath);
const answer1 = await invokeLLMCompletion(content.content, fileName);
const answer2 = await invokeLLMAnalyzer(answer1, fileName, funcName); const answer2 = await invokeLLMAnalyzer(answer1, fileName, funcName);
const outputFilePath = path.join(output_directory, fileName + "_" + funcName + ".md"); const outputFilePath = path.join(output_directory, fileName + "_" + funcName + ".md");
await workspace.writeText(outputFilePath, answer2); await workspace.writeText(outputFilePath, answer2);
const answer3 = await createGitUpdateRequest(src_directory, file.filename, answer2);
const outputFilePath2 = path.join(output_directory, fileName + "_" + funcName + "_git.md");
await workspace.writeText(outputFilePath2, answer3);
++count; ++count;
if (count > 3)
break;
} }
} }