From 75269a9c40e7593525c0f2b666c43e3c5395ec08 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 3 Apr 2024 15:35:17 +0100 Subject: [PATCH 01/11] Increment version and new sample --- esbmc_ai/__about__.py | 2 +- samples/threading_broken.c | 25 +++++++++++++++++++++++++ 2 files changed, 26 insertions(+), 1 deletion(-) create mode 100644 samples/threading_broken.c diff --git a/esbmc_ai/__about__.py b/esbmc_ai/__about__.py index 0f1356e..721ba30 100644 --- a/esbmc_ai/__about__.py +++ b/esbmc_ai/__about__.py @@ -1,4 +1,4 @@ # Author: Yiannis Charalambous -__version__ = "v0.5.0.dev6" +__version__ = "v0.5.0.dev10" __author__: str = "Yiannis Charalambous" diff --git a/samples/threading_broken.c b/samples/threading_broken.c new file mode 100644 index 0000000..5f17856 --- /dev/null +++ b/samples/threading_broken.c @@ -0,0 +1,25 @@ +#include +#include + +int a, b; +void __VERIFIER_atomic_acquire(void) +{{ + __VERIFIER_assume(a == 0); + a = 1; +} +void *c(void *arg) +{ + ; + __VERIFIER_atomic_acquire(); + b = 1; + return NULL; +} +pthread_t d; +int main() +{ + pthread_create(&d, 0, c, 0); + __VERIFIER_atomic_acquire(); + if (!b) + assert(0); + return 0; +} \ No newline at end of file From 5a5cd2c91d84bc0e04c4bf989dff921eedd8d13e Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 3 Apr 2024 15:35:39 +0100 Subject: [PATCH 02/11] Increased esbmc_util cooldown buffer to 10 --- esbmc_ai/esbmc_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/esbmc_ai/esbmc_util.py b/esbmc_ai/esbmc_util.py index 3083bd3..abc1eee 100644 --- a/esbmc_ai/esbmc_util.py +++ b/esbmc_ai/esbmc_util.py @@ -84,7 +84,7 @@ def esbmc(path: str, esbmc_params: list, timeout: Optional[float] = None): esbmc_cmd.extend(["--timeout", str(timeout)]) # Add slack time to process to allow verifier to timeout and end gracefully. - process_timeout: Optional[float] = timeout + 1 if timeout else None + process_timeout: Optional[float] = timeout + 10 if timeout else None # Run ESBMC and get output process: CompletedProcess = run( From 7ebc8809577116650150f8d0b6f5ba6629037e10 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 3 Apr 2024 15:38:10 +0100 Subject: [PATCH 03/11] SolutionGenerator * Added custom error types and error handling code. * Fixed initial_prompt not undergoing template substitution --- esbmc_ai/commands/fix_code_command.py | 48 +++++++++++-------- esbmc_ai/solution_generator.py | 66 +++++++++++++++++++-------- 2 files changed, 78 insertions(+), 36 deletions(-) diff --git a/esbmc_ai/commands/fix_code_command.py b/esbmc_ai/commands/fix_code_command.py index 3091fe2..fb103a4 100644 --- a/esbmc_ai/commands/fix_code_command.py +++ b/esbmc_ai/commands/fix_code_command.py @@ -1,6 +1,7 @@ # Author: Yiannis Charalambous from os import get_terminal_size +import sys from typing import Any, Tuple from typing_extensions import override from langchain.schema import AIMessage, HumanMessage @@ -15,7 +16,12 @@ esbmc_get_error_type, esbmc_load_source_code, ) -from ..solution_generator import SolutionGenerator, get_esbmc_output_formatted +from ..solution_generator import ( + ESBMCTimedOutException, + SolutionGenerator, + SourceCodeParseError, + get_esbmc_output_formatted, +) from ..logging import print_horizontal_line, printv, printvv # TODO Remove built in messages and move them to config. @@ -55,21 +61,25 @@ def print_raw_conversation() -> None: else "Using generic prompt..." ) - solution_generator = SolutionGenerator( - ai_model_agent=config.chat_prompt_generator_mode, - source_code=source_code, - esbmc_output=esbmc_output, - ai_model=config.ai_model, - llm=config.ai_model.create_llm( - api_keys=config.api_keys, - temperature=config.chat_prompt_generator_mode.temperature, - requests_max_tries=config.requests_max_tries, - requests_timeout=config.requests_timeout, - ), - scenario=scenario, - source_code_format=config.source_code_format, - esbmc_output_type=config.esbmc_output_type, - ) + try: + solution_generator = SolutionGenerator( + ai_model_agent=config.chat_prompt_generator_mode, + source_code=source_code, + esbmc_output=esbmc_output, + ai_model=config.ai_model, + llm=config.ai_model.create_llm( + api_keys=config.api_keys, + temperature=config.chat_prompt_generator_mode.temperature, + requests_max_tries=config.requests_max_tries, + requests_timeout=config.requests_timeout, + ), + scenario=scenario, + source_code_format=config.source_code_format, + esbmc_output_type=config.esbmc_output_type, + ) + except ESBMCTimedOutException: + print("error: ESBMC has timed out...") + sys.exit(1) print() @@ -116,9 +126,11 @@ def print_raw_conversation() -> None: esbmc_output_type=config.esbmc_output_type, esbmc_output=esbmc_output, ) - except ValueError: - # Probably did not compile and so ESBMC source code is clang output. + except SourceCodeParseError: pass + except ESBMCTimedOutException: + print("error: ESBMC has timed out...") + sys.exit(1) # Print verbose lvl 2 print_horizontal_line(2) diff --git a/esbmc_ai/solution_generator.py b/esbmc_ai/solution_generator.py index 639eb70..43b763e 100644 --- a/esbmc_ai/solution_generator.py +++ b/esbmc_ai/solution_generator.py @@ -19,13 +19,21 @@ ) +class ESBMCTimedOutException(Exception): + pass + + +class SourceCodeParseError(Exception): + pass + + def get_source_code_formatted( source_code_format: str, source_code: str, esbmc_output: str ) -> str: match source_code_format: case "single": line: Optional[int] = get_source_code_err_line_idx(esbmc_output) - assert line, "error line not found in esbmc output" + assert line, f"error line not found in esbmc output:\n{esbmc_output}" # ESBMC reports errors starting from 1. To get the correct line, we need to use 0 based # indexing. return source_code.splitlines(True)[line] @@ -38,11 +46,18 @@ def get_source_code_formatted( def get_esbmc_output_formatted(esbmc_output_type: str, esbmc_output: str) -> str: + # Check for parsing error + if "ERROR: PARSING ERROR" in esbmc_output: + # Parsing errors are usually small in nature. + raise SourceCodeParseError() + elif "ERROR: Timed out" in esbmc_output: + raise ESBMCTimedOutException() + match esbmc_output_type: case "vp": value: Optional[str] = esbmc_get_violated_property(esbmc_output) if not value: - raise ValueError("Not found violated property.") + raise ValueError("Not found violated property." + esbmc_output) return value case "ce": value: Optional[str] = esbmc_get_counter_example(esbmc_output) @@ -77,32 +92,29 @@ def __init__( ai_model=ai_model, llm=llm, ) + self.initial_prompt = ai_model_agent.initial_prompt self.esbmc_output_type: str = esbmc_output_type - self.esbmc_output = get_esbmc_output_formatted( - esbmc_output_type=self.esbmc_output_type, - esbmc_output=esbmc_output, - ) - self.source_code_format: str = source_code_format self.source_code_raw: str = source_code + # Used for resetting state. + self._original_source_code: str = source_code - source_code_formatted: str = get_source_code_formatted( - source_code_format=self.source_code_format, - source_code=self.source_code_raw, - esbmc_output=self.esbmc_output, - ) - - self.apply_template_value( - source_code=source_code_formatted, - esbmc_output=self.esbmc_output, - ) + # Format ESBMC output + try: + self.esbmc_output = get_esbmc_output_formatted( + esbmc_output_type=self.esbmc_output_type, + esbmc_output=esbmc_output, + ) + except SourceCodeParseError: + self.esbmc_output = esbmc_output @override def compress_message_stack(self) -> None: # Resets the conversation - cannot summarize code self.messages: list[BaseMessage] = [] + self.source_code_raw = self._original_source_code @classmethod def get_code_from_solution(cls, solution: str) -> str: @@ -130,7 +142,23 @@ def get_code_from_solution(cls, solution: str) -> str: return solution def generate_solution(self) -> tuple[str, FinishReason]: - response: ChatResponse = self.send_message(self.initial_prompt) + self.push_to_message_stack(HumanMessage(content=self.initial_prompt)) + + # Format source code + source_code_formatted: str = get_source_code_formatted( + source_code_format=self.source_code_format, + source_code=self.source_code_raw, + esbmc_output=self.esbmc_output, + ) + + # Apply template substitution to message stack + self.apply_template_value( + source_code=source_code_formatted, + esbmc_output=self.esbmc_output, + ) + + # Generate the solution + response: ChatResponse = self.send_message() solution: str = str(response.message.content) solution = SolutionGenerator.get_code_from_solution(solution) @@ -149,4 +177,6 @@ def generate_solution(self) -> tuple[str, FinishReason]: self.source_code_raw, solution, err_line, err_line ) + # Remember it for next cycle + self.source_code_raw = solution return solution, response.finish_reason From 5d8924d31d5230d9caf385f7168d536eed661460 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 3 Apr 2024 18:53:26 +0100 Subject: [PATCH 04/11] Changed build script to use hatch --- build.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/build.sh b/build.sh index 8ba0dee..ef7e728 100755 --- a/build.sh +++ b/build.sh @@ -1,5 +1,6 @@ #!/usr/bin/env sh echo "Building ESBMC-AI" -python3 -m build +# python3 -m build +hatch build From c0cdccf994f0208c03bee445d5e3d7d6a30b6006 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 3 Apr 2024 18:53:43 +0100 Subject: [PATCH 05/11] Added exclusion list to build pyproject.toml --- pyproject.toml | 28 ++++++++++------------------ 1 file changed, 10 insertions(+), 18 deletions(-) diff --git a/pyproject.toml b/pyproject.toml index edd126e..418549d 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -65,22 +65,14 @@ Issues = "https://github.com/Yiannis128/esbmc-ai/issues" [tool.hatch.version] path = "esbmc_ai/__about__.py" -# [tool.hatch.build.targets.esbmc_ai] -# ignore-vcs = true -# include = [ -# "/esbmc_ai/**/*.py", -# "/esbmc_ai_config/**/*.py", -# ] -# exclude = [ -# "/.github/*", -# "/.vscode", -# "/notebooks", -# "/samples", -# "/scripts", -# "/tests", -# "/env.example", -# "/.gitignore" -# ] +[tool.hatch.build.targets.sdist] +ignore-vcs = false +# include = ["esbmc-ai/**/*", "pyproject.toml", "README.md"] +# exclude = ["**/*"] +packages = ["esbmc_ai"] -# [tool.hatch.build.targets.esbmc_ai.force-include] -# "config.json" = "esbmc_ai_config/data/config.template.json" +[tool.hatch.build.targets.wheel] +ignore-vcs = false +# include = ["esbmc-ai/**/*", "pyproject.toml", "README.md"] +# exclude = ["**/*"] +packages = ["esbmc_ai"] From ead8a7ed8518c8cc8a5a5831e62cfeba6be0ad89 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 3 Apr 2024 18:54:28 +0100 Subject: [PATCH 06/11] Added get_clang_err_line to esbmc_util --- esbmc_ai/esbmc_util.py | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/esbmc_ai/esbmc_util.py b/esbmc_ai/esbmc_util.py index abc1eee..d54d769 100644 --- a/esbmc_ai/esbmc_util.py +++ b/esbmc_ai/esbmc_util.py @@ -67,6 +67,25 @@ def get_source_code_err_line_idx(esbmc_output: str) -> Optional[int]: return None +def get_clang_err_line(clang_output: str) -> Optional[int]: + """For when the code does not compile, gets the error line reported in the clang + output. This is useful for `esbmc_output_type single`""" + # TODO Test me + lines: list[str] = clang_output.splitlines() + for line in lines: + # Find the first line containing a filename along with error. + line_split: list[str] = line.split(":") + # Check for the filename + if line_split[0].endswith(".c") and " error" in line_split[3]: + return int(line_split[1]) + + return None + + +def get_clang_err_line_index(clang_output: str) -> Optional[int]: + return get_clang_err_line(clang_output) + + def esbmc(path: str, esbmc_params: list, timeout: Optional[float] = None): """Exit code will be 0 if verification successful, 1 if verification failed. And any other number for compilation error/general errors.""" From 1047f5085bdfda4ba5d64e6f14c2ae47fe6c3624 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 3 Apr 2024 18:54:38 +0100 Subject: [PATCH 07/11] Increment version --- esbmc_ai/__about__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/esbmc_ai/__about__.py b/esbmc_ai/__about__.py index 721ba30..c97fd16 100644 --- a/esbmc_ai/__about__.py +++ b/esbmc_ai/__about__.py @@ -1,4 +1,4 @@ # Author: Yiannis Charalambous -__version__ = "v0.5.0.dev10" +__version__ = "v0.5.0.dev14" __author__: str = "Yiannis Charalambous" From 6aa467d9b1b11d5c2fe693bd1353a6c44cf714e4 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 3 Apr 2024 18:54:50 +0100 Subject: [PATCH 08/11] Fixed print_horizontal_line --- esbmc_ai/logging.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/esbmc_ai/logging.py b/esbmc_ai/logging.py index 0408498..3ca1a3a 100644 --- a/esbmc_ai/logging.py +++ b/esbmc_ai/logging.py @@ -36,8 +36,8 @@ def printvvv(m) -> None: def print_horizontal_line(verbosity: int) -> None: - if verbosity >= _verbose: + if _verbose >= verbosity: try: - printvv("-" * get_terminal_size().columns) + print("-" * get_terminal_size().columns) except OSError: pass From a709fb4c464fc3ebb63c73493e6388a7ce2aabaa Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 3 Apr 2024 18:56:10 +0100 Subject: [PATCH 09/11] SolutionGenerator: Bug fix get_source_code_formatted will get the clang line for source_code_type single --- esbmc_ai/solution_generator.py | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/esbmc_ai/solution_generator.py b/esbmc_ai/solution_generator.py index 43b763e..fd7e664 100644 --- a/esbmc_ai/solution_generator.py +++ b/esbmc_ai/solution_generator.py @@ -16,6 +16,7 @@ esbmc_get_counter_example, esbmc_get_violated_property, get_source_code_err_line_idx, + get_clang_err_line_index, ) @@ -32,11 +33,19 @@ def get_source_code_formatted( ) -> str: match source_code_format: case "single": + # Get source code error line from esbmc output line: Optional[int] = get_source_code_err_line_idx(esbmc_output) - assert line, f"error line not found in esbmc output:\n{esbmc_output}" - # ESBMC reports errors starting from 1. To get the correct line, we need to use 0 based - # indexing. - return source_code.splitlines(True)[line] + if line: + return source_code.splitlines(True)[line] + + # Check if it parses + line = get_clang_err_line_index(esbmc_output) + if line: + return source_code.splitlines(True)[line] + + raise AssertionError( + f"error line not found in esbmc output:\n{esbmc_output}" + ) case "full": return source_code case _: @@ -108,6 +117,8 @@ def __init__( esbmc_output=esbmc_output, ) except SourceCodeParseError: + # When clang output is displayed, show it entirely as it doesn't get very + # big. self.esbmc_output = esbmc_output @override From 1c82514a8c4549f27b3c84974850d05e2f25a6cc Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 3 Apr 2024 18:57:52 +0100 Subject: [PATCH 10/11] FixCodeCommand: Updated notice messages and bug fix Fixed bug where if verification is successful then the get_esbmc_output_formatted would return a stack trace. --- esbmc_ai/commands/fix_code_command.py | 41 +++++++++++++++------------ 1 file changed, 23 insertions(+), 18 deletions(-) diff --git a/esbmc_ai/commands/fix_code_command.py b/esbmc_ai/commands/fix_code_command.py index fb103a4..9ed2edc 100644 --- a/esbmc_ai/commands/fix_code_command.py +++ b/esbmc_ai/commands/fix_code_command.py @@ -1,6 +1,5 @@ # Author: Yiannis Charalambous -from os import get_terminal_size import sys from typing import Any, Tuple from typing_extensions import override @@ -40,12 +39,13 @@ def __init__(self) -> None: @override def execute(self, **kwargs: Any) -> Tuple[bool, str]: def print_raw_conversation() -> None: - print("Notice: Printing raw conversation...") + print_horizontal_line(0) + print("ESBMC-AI Notice: Printing raw conversation...") all_messages = solution_generator._system_messages.copy() all_messages.extend(solution_generator.messages.copy()) messages: list[str] = [f"{msg.type}: {msg.content}" for msg in all_messages] print("\n" + "\n\n".join(messages)) - print("Notice: End of conversation") + print("ESBMC-AI Notice: End of raw conversation") file_name: str = kwargs["file_name"] source_code: str = kwargs["source_code"] @@ -119,34 +119,38 @@ def print_raw_conversation() -> None: ) self.anim.stop() - # TODO Move this process into Solution Generator since have (beginning) is done - # inside, and the other half is done here. - try: - esbmc_output = get_esbmc_output_formatted( - esbmc_output_type=config.esbmc_output_type, - esbmc_output=esbmc_output, - ) - except SourceCodeParseError: - pass - except ESBMCTimedOutException: - print("error: ESBMC has timed out...") - sys.exit(1) - # Print verbose lvl 2 print_horizontal_line(2) printvv(esbmc_output) print_horizontal_line(2) + # Solution found if exit_code == 0: self.on_solution_signal.emit(llm_solution) if config.raw_conversation: print_raw_conversation() + printv("ESBMC-AI Notice: Succesfully verified code") + return False, llm_solution + # TODO Move this process into Solution Generator since have (beginning) is done + # inside, and the other half is done here. + # Get formatted ESBMC output + try: + esbmc_output = get_esbmc_output_formatted( + esbmc_output_type=config.esbmc_output_type, + esbmc_output=esbmc_output, + ) + except SourceCodeParseError: + pass + except ESBMCTimedOutException: + print("error: ESBMC has timed out...") + sys.exit(1) + # Failure case - print(f"Failure {idx+1}/{max_retries}: Retrying...") + print(f"ESBMC-AI Notice: Failure {idx+1}/{max_retries}: Retrying...") # If final iteration no need to sleep. if idx < max_retries - 1: @@ -172,4 +176,5 @@ def print_raw_conversation() -> None: if config.raw_conversation: print_raw_conversation() - return True, "Failed all attempts..." + + return True, "ESBMC-AI Notice: Failed all attempts..." From 992e049f9fe26889e528156dcc0e79011681d595 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Thu, 4 Apr 2024 13:10:15 +0100 Subject: [PATCH 11/11] Fix Code Command: Fix spelling mistake --- esbmc_ai/__about__.py | 2 +- esbmc_ai/commands/fix_code_command.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/esbmc_ai/__about__.py b/esbmc_ai/__about__.py index c97fd16..7415113 100644 --- a/esbmc_ai/__about__.py +++ b/esbmc_ai/__about__.py @@ -1,4 +1,4 @@ # Author: Yiannis Charalambous -__version__ = "v0.5.0.dev14" +__version__ = "v0.5.0rc0" __author__: str = "Yiannis Charalambous" diff --git a/esbmc_ai/commands/fix_code_command.py b/esbmc_ai/commands/fix_code_command.py index 9ed2edc..b2db77d 100644 --- a/esbmc_ai/commands/fix_code_command.py +++ b/esbmc_ai/commands/fix_code_command.py @@ -131,7 +131,7 @@ def print_raw_conversation() -> None: if config.raw_conversation: print_raw_conversation() - printv("ESBMC-AI Notice: Succesfully verified code") + printv("ESBMC-AI Notice: Successfully verified code") return False, llm_solution