Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Config System Overhaul #146

Merged
merged 17 commits into from
Sep 16, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions .env.example
Original file line number Diff line number Diff line change
@@ -1,3 +1,2 @@
OPENAI_API_KEY=XXXXXXXXXXX
HUGGINGFACE_API_KEY=YYYYYYYYYY
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
44 changes: 0 additions & 44 deletions Pipfile

This file was deleted.

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."
2 changes: 1 addition & 1 deletion esbmc_ai/__about__.py
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# Author: Yiannis Charalambous

__version__ = "v0.5.1"
__version__ = "v0.6.0"
__author__: str = "Yiannis Charalambous"
4 changes: 4 additions & 0 deletions esbmc_ai/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -3,3 +3,7 @@
features such as automatic code fixing and more."""

from esbmc_ai.__about__ import __version__, __author__

from esbmc_ai.config import Config

__all__ = ["Config"]
Loading
Loading