Skip to content

Commit

Permalink
Updated to use new Config
Browse files Browse the repository at this point in the history
  • Loading branch information
Yiannis128 committed Sep 15, 2024
1 parent 1884be4 commit bcc8022
Show file tree
Hide file tree
Showing 14 changed files with 347 additions and 247 deletions.
2 changes: 1 addition & 1 deletion .env.example
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
OPENAI_API_KEY=XXXXXXXXXXX
ESBMC_AI_CFG_PATH=./config.json
ESBMC_AI_CFG_PATH=./config.toml
2 changes: 1 addition & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -162,7 +162,7 @@ cython_debug/

esbmc
temp/
config_dev.json
config_dev.toml

# Proprietary source code samples.
uav_test.sh
99 changes: 0 additions & 99 deletions config.json

This file was deleted.

95 changes: 95 additions & 0 deletions config.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
ai_model = "gpt-3.5-turbo"
temp_auto_clean = true
#temp_file_dir = "temp"
allow_successful = false
loading_hints = true
source_code_format = "full"

[esbmc]
path = "~/.local/bin/esbmc"
params = [
"--interval-analysis",
"--goto-unwind",
"--unlimited-goto-unwind",
"--k-induction",
"--state-hashing",
"--add-symex-value-sets",
"--k-step",
"2",
"--floatbv",
"--unlimited-k-steps",
"--compact-trace",
"--context-bound",
"2",
]
output_type = "full"
timeout = 60

[llm_requests]
max_tries = 5
timeout = 60

[user_chat]
temperature = 1.0

[fix_code]
temperature = 0.7
max_attempts = 5
message_history = "normal"

# PROMPT TEMPLATES - USER CHAT

[prompt_templates.user_chat]
initial = "Walk me through the source code, while also explaining the output of ESBMC at the relevant parts. You shall not start the reply with an acknowledgement message such as 'Certainly'."

[[prompt_templates.user_chat.system]]
role = "System"
content = "You are a security focused assistant that parses output from a program called ESBMC and explains the output to the user. ESBMC (the Efficient SMT-based Context-Bounded Model Checker) is a context-bounded model checker for verifying single and multithreaded C/C++, Kotlin, and Solidity programs. It can automatically verify both predefined safety properties (e.g., bounds check, pointer safety, overflow) and user-defined program assertions. You don't need to explain how ESBMC works, you only need to parse and explain the vulnerabilities that the output shows. For each line of code explained, say what the line number is as well. Do not answer any questions outside of these explicit parameters. If you understand, reply OK."

[[prompt_templates.user_chat.system]]
role = "AI"
content = "OK"

[[prompt_templates.user_chat.system]]
role = "System"
content = "Reply OK if you understand that the following text is the program source code:\n\n```c{source_code}```"

[[prompt_templates.user_chat.system]]
role = "AI"
content = "OK"

[[prompt_templates.user_chat.system]]
role = "System"
content = "Reply OK if you understand that the following text is the output from ESBMC:\n\n```\n{esbmc_output}\n```"

[[prompt_templates.user_chat.system]]
role = "AI"
content = "OK"

[[prompt_templates.user_chat.set_solution]]
role = "System"
content = "Here is the corrected code:\n\n```c\n{source_code_solution}```"

[[prompt_templates.user_chat.set_solution]]
role = "AI"
content = "OK"

# PROMPT TEMPLATES - FIX CODE

[prompt_templates.fix_code.base]
initial = "The ESBMC output is:\n\n```\n{esbmc_output}\n```\n\nThe source code is:\n\n```c\n{source_code}\n```\n Using the ESBMC output, show the fixed text."

[[prompt_templates.fix_code.base.system]]
role = "System"
content = "From now on, act as an Automated Code Repair Tool that repairs AI C code. You will be shown AI C code, along with ESBMC output. Pay close attention to the ESBMC output, which contains a stack trace along with the type of error that occurred and its location that you need to fix. Provide the repaired C code as output, as would an Automated Code Repair Tool. Aside from the corrected source code, do not output any other text."

[prompt_templates.fix_code."division by zero"]
initial = "The ESBMC output is:\n\n```\n{esbmc_output}\n```\n\nThe source code is:\n\n```c\n{source_code}\n```\n Using the ESBMC output, show the fixed text."

[[prompt_templates.fix_code."division by zero".system]]
role = "System"
content = "Here's a C program with a vulnerability:\n```c\n{source_code}\n```\nA Formal Verification tool identified a division by zero issue:\n{esbmc_output}\nTask: Modify the C code to safely handle scenarios where division by zero might occur. The solution should prevent undefined behavior or crashes due to division by zero. \nGuidelines: Focus on making essential changes only. Avoid adding or modifying comments, and ensure the changes are precise and minimal.\nGuidelines: Ensure the revised code avoids undefined behavior and handles division by zero cases effectively.\nGuidelines: Implement safeguards (like comparison) to prevent division by zero instead of using literal divisions like 1.0/0.0.Output: Provide the corrected, complete C code. The solution should compile and run error-free, addressing the division by zero vulnerability.\nStart the code snippet with ```c and end with ```. Reply OK if you understand."

[[prompt_templates.fix_code."division by zero".system]]
role = "AI"
content = "OK."
Loading

0 comments on commit bcc8022

Please sign in to comment.