Skip to content

Commit

Permalink
Verbose Level 2
Browse files Browse the repository at this point in the history
* LoadingWidget instances use factory constructor
* ESBMC output now is shown for verbose level 2
* Fix code: failed generations are shown on verbose level 2
  • Loading branch information
Yiannis128 committed Jul 7, 2023
1 parent 577d685 commit 6bd2715
Show file tree
Hide file tree
Showing 3 changed files with 30 additions and 12 deletions.
14 changes: 10 additions & 4 deletions esbmc_ai_lib/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -25,9 +25,9 @@
VerifyCodeCommand,
)

from esbmc_ai_lib.loading_widget import LoadingWidget
from esbmc_ai_lib.loading_widget import LoadingWidget, create_loading_widget
from esbmc_ai_lib.user_chat import UserChat
from esbmc_ai_lib.logging import printv
from esbmc_ai_lib.logging import printv, printvv
from esbmc_ai_lib.esbmc_util import esbmc
from esbmc_ai_lib.chat_response import FinishReason, json_to_base_message, ChatResponse
from esbmc_ai_lib.ai_models import _ai_model_names
Expand Down Expand Up @@ -274,20 +274,26 @@ def main() -> None:

check_health()

anim: LoadingWidget = LoadingWidget()
anim: LoadingWidget = create_loading_widget()

# Read the source code and esbmc output.
printv("Reading source code...")
print(f"Running ESBMC with {config.esbmc_params}\n")
source_code: str = get_src(get_main_source_file())

anim.start("ESBMC is processing... Please Wait")
exit_code, esbmc_output = esbmc(
exit_code, esbmc_output, esbmc_err_output = esbmc(
path=get_main_source_file(),
esbmc_params=config.esbmc_params,
)
anim.stop()

# Print verbose lvl 2
printvv("-" * os.get_terminal_size().columns)
printvv(esbmc_output)
printvv(esbmc_err_output)
printvv("-" * os.get_terminal_size().columns)

# ESBMC will output 0 for verification success and 1 for verification
# failed, if anything else gets thrown, it's an ESBMC error.
if exit_code == 0:
Expand Down
23 changes: 19 additions & 4 deletions esbmc_ai_lib/commands/fix_code_command.py
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
# Author: Yiannis Charalambous

from os import get_terminal_size
from time import sleep
from typing_extensions import override
from langchain.schema import AIMessage, HumanMessage
Expand All @@ -13,9 +14,10 @@
from .chat_command import ChatCommand
from .. import config
from ..msg_bus import Signal
from ..loading_widget import LoadingWidget
from ..loading_widget import create_loading_widget
from ..esbmc_util import esbmc_load_source_code
from ..solution_generator import SolutionGenerator
from ..logging import printvv


class FixCodeCommand(ChatCommand):
Expand All @@ -26,15 +28,15 @@ def __init__(self) -> None:
command_name="fix-code",
help_message="Generates a solution for this code, and reevaluates it with ESBMC.",
)
self.anim = LoadingWidget()
self.anim = create_loading_widget()

@override
def execute(self, file_name: str, source_code: str, esbmc_output: str):
wait_time: int = int(config.consecutive_prompt_delay)
# Create time left animation to show how much time left between API calls
# This is done by creating a list of all the numbers to be displayed and
# setting the animation delay to 1 second.
wait_anim = LoadingWidget(
wait_anim = create_loading_widget(
anim_speed=1,
animation=[str(num) for num in range(wait_time, 0, -1)],
)
Expand Down Expand Up @@ -75,17 +77,30 @@ def execute(self, file_name: str, source_code: str, esbmc_output: str):
else:
break

# Print verbose lvl 2
printvv("\nGeneration:")
printvv("-" * get_terminal_size().columns)
printvv(response)
printvv("-" * get_terminal_size().columns)
printvv("")

# Pass to ESBMC, a workaround is used where the file is saved
# to a temporary location since ESBMC needs it in file format.
self.anim.start("Verifying with ESBMC... Please Wait")
exit_code, esbmc_output = esbmc_load_source_code(
exit_code, esbmc_output, esbmc_err_output = esbmc_load_source_code(
file_path=file_name,
source_code=str(response),
esbmc_params=config.esbmc_params,
auto_clean=config.temp_auto_clean,
)
self.anim.stop()

# Print verbose lvl 2
printvv("-" * get_terminal_size().columns)
printvv(esbmc_output)
printvv(esbmc_err_output)
printvv("-" * get_terminal_size().columns)

if exit_code == 0:
self.on_solution_signal.emit(response)

Expand Down
5 changes: 1 addition & 4 deletions esbmc_ai_lib/esbmc_util.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@
from pathlib import Path

from . import config
from .logging import printvv


def esbmc(path: str, esbmc_params: list):
Expand All @@ -23,9 +22,7 @@ def esbmc(path: str, esbmc_params: list):
exit_code = process.wait()
output: str = str(output_bytes).replace("\\n", "\n")
err: str = str(err_bytes).replace("\\n", "\n")
printvv(output)
printvv(err)
return exit_code, output
return exit_code, output, err


def esbmc_load_source_code(
Expand Down

0 comments on commit 6bd2715

Please sign in to comment.