Skip to content
Merged
Show file tree
Hide file tree
Changes from 18 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
47 changes: 47 additions & 0 deletions .vscode/debug/config.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
ai_model = "openai:gpt-5-nano"
temp_auto_clean = true
#temp_file_dir = "temp"
allow_successful = false
loading_hints = false
source_code_format = "full"
dev_mode = true

[ai_custom."llama3.2:3b"]
server_type = "ollama"
url = "localhost:11434"
max_tokens = 100000

[ai_custom."llama3.3:latest"]
server_type = "ollama"
url = "localhost:11435"
max_tokens = 100000

[solution]
filenames = ["samples/threading.c"]

[verifier]
name = "esbmc"

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

[llm_requests]
max_tries = 5
timeout = 60
15 changes: 15 additions & 0 deletions .vscode/launch.json
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,21 @@
// For more information, visit: https://go.microsoft.com/fwlink/?linkid=830387
"version": "0.2.0",
"configurations": [
{
"name": "Run on Open File",
"type": "debugpy",
"request": "launch",
"module": "esbmc_ai",
"justMyCode": true,
"cwd": "${workspaceFolder}",
"env": {
"ESBMCAI_CONFIG_FILE": "${workspaceFolder}/.vscode/debug/config.toml"
},
"args": [
"-vvv",
"debug-view-config"
]
},
{
"name": "Fix Code on Open File",
"type": "debugpy",
Expand Down
38 changes: 12 additions & 26 deletions config.toml
Original file line number Diff line number Diff line change
@@ -1,4 +1,15 @@
ai_model = "gpt-3.5-turbo"
# ESBMC-AI Default Config File.
# The ESBMC-AI config is loaded in the following order:
# 1. CLI
# 2. env
# 3. dotenv
# 4. TOML
# 5. file_secret
# This file is provided as an example, however it should be customized to your
# needs as it probably contains values that are wrong for your system.
# To view all the possible config options and their description, run the
# subcommand "list-config".
ai_model = "openai:gpt-5-nano"
temp_auto_clean = true
#temp_file_dir = "temp"
allow_successful = false
Expand Down Expand Up @@ -31,28 +42,3 @@ timeout = 60
[llm_requests]
max_tries = 5
timeout = 60

# FIX CODE

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

[fix_code.prompt_templates.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."

[[fix_code.prompt_templates.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."

[fix_code.prompt_templates."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."

[[fix_code.prompt_templates."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."

[[fix_code.prompt_templates."division by zero".system]]
role = "AI"
content = "OK."
10 changes: 4 additions & 6 deletions esbmc_ai/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -4,21 +4,19 @@

from esbmc_ai.__about__ import __version__, __author__

from esbmc_ai.config_field import ConfigField
from esbmc_ai.config import Config
from esbmc_ai.chat_command import ChatCommand
from esbmc_ai.base_component import BaseComponent
from esbmc_ai.base_component import BaseComponent, BaseComponentConfig
from esbmc_ai.verifiers import BaseSourceVerifier
from esbmc_ai.ai_models import AIModel, AIModels
from esbmc_ai.log_utils import LogCategories
from esbmc_ai.ai_models import AIModel
from esbmc_ai.log_categories import LogCategories

__all__ = [
"ConfigField",
"Config",
"BaseComponent",
"BaseComponentConfig",
"ChatCommand",
"BaseSourceVerifier",
"AIModel",
"AIModels",
"LogCategories",
]
Loading