Optimize Code Mode Patch 1

.gitignore

@@ -166,3 +166,4 @@ config_dev.json
 
 # Proprietary source code samples.
 uav_test.sh
+experiments

Pipfile

@@ -25,6 +25,7 @@ libclang = "*"
 clang = "*"
 text-generation = "*"
 langchain = {extras = ["llms"], version = "*"}
+pydantic = "==1.10.13"
 
 [dev-packages]
 black = "*"

config.json

@@ -35,6 +35,7 @@
       "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'."
     },
     "generate_solution": {
+      "max_attempts": 10,
       "temperature": 1.3,
       "system": [
         {
@@ -50,7 +51,7 @@
       "system": [
         {
           "role": "System",
-          "content": "You are a code optimizer. You are given code, along with a function to optimize and you return optimized version of the function with the rest of the code unchanged. The optimized function should be smaller than the original function if possible and also execute faster than the original. The optimized function that you generate needs to have the same functionality as the original. From this point on, you can only reply in source code. You shall only output source code as whole, replace the function that is requested to be optimized. Reply OK if you understand."
+          "content": "You are a code optimizer. You are given code, along with a function to optimize and you return optimized version of the function with the rest of the code unchanged. The optimized function should be smaller than the original function and also execute faster than the original. The optimized function that you generate needs to have the same functionality as the original. The optimized function that you generate must have the same function name and take the same parameters as the original one, so if the inefficient function name is \"inefficientFunction\", then the optimized function name should also be \"inefficientFunction\". From this point on, you can only reply in source code. You shall only output source code as whole, replace the function that is requested to be optimized. Reply OK if you understand."
         },
         { "role": "AI", "content": "OK" }
       ],
@@ -61,8 +62,11 @@
         "--no-pointer-check",
         "--no-div-by-zero-check",
         "--max-k-step",
-        "10"
-      ]
+        "50"
+      ],
+      "array_expansion": 5,
+      "init_max_depth": 4,
+      "partial_equivalence_check": "deep"
     }
   }
 }

esbmc_ai_lib/__init__.py

@@ -2,4 +2,4 @@
 Software Bounded Model Checker. With the power of LLMs, it adds
 features such as automatic code fixing and more."""
 
-version: str = "0.3.0"
+version: str = "0.3.1"

esbmc_ai_lib/__main__.py

@@ -27,9 +27,10 @@
     HelpCommand,
     ExitCommand,
     OptimizeCodeCommand,
-    # VerifyCodeCommand,
 )
 
+from esbmc_ai_lib import version
+from esbmc_ai_lib.term import get_terminal_width
 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, printvv
@@ -48,11 +49,20 @@
 
 chat: UserChat
 
-HELP_MESSAGE: str = """Tool that passes ESBMC output into ChatGPT and allows for natural language
-explanations. Type /help in order to view available commands."""
+AUTHORS: list[str] = ["Yiannis Charalambous"]
+
+PROLOGUE: str = f"ESBMC-AI\nMade by {', '.join(AUTHORS)}"
+
+HELP_MESSAGE: str = f"""{PROLOGUE}
+
+Tool that passes ESBMC output into an LLM and allows for natural language
+explanations among other things. Type /help in order to view available commands."""
 
 ESBMC_HELP: str = """Additional ESBMC Arguments - The following are useful
 arguments that can be added after the filename to modify ESBMC functionality.
+Use the -a or --append parameter to append the options to the ones defined in the
+config. 
+
 For all the options, run ESBMC with -h as a parameter:
 
   --compact-trace                  add trace information to output
@@ -83,20 +93,6 @@
 """
 
 
-def init_check_health(verbose: bool) -> None:
-    def printv(m) -> None:
-        if verbose:
-            print(m)
-
-    printv("Performing init health check...")
-    # Check that the .env file exists.
-    if os.path.exists(".env"):
-        printv("Environment file has been located")
-    else:
-        print("Error: .env file is not found in project directory")
-        sys.exit(3)
-
-
 def check_health() -> None:
     printv("Performing health check...")
     # Check that ESBMC exists.
@@ -161,7 +157,7 @@ def init_commands() -> None:
 
 def _run_command_mode(
     command: ChatCommand,
-    args: list[str],
+    args: str,
     esbmc_output: str,
     source_code: str,
 ) -> None:
@@ -170,6 +166,7 @@ def _run_command_mode(
             file_name=get_main_source_file_path(),
             source_code=source_code,
             esbmc_output=esbmc_output,
+            max_retries=config.fix_code_max_attempts,
         )
 
         if error:
@@ -178,10 +175,11 @@ def _run_command_mode(
         else:
             print(solution)
     elif command == optimize_code_command:
+        function_names: list[str] = args.split(",")
         error, solution = optimize_code_command.execute(
             file_path=get_main_source_file_path(),
             source_code=source_code,
-            function_names=args,
+            function_names=function_names if len(args) > 0 else [],
         )
 
         print(solution)
@@ -209,12 +207,11 @@ def main() -> None:
     init_commands_list()
 
     parser = argparse.ArgumentParser(
-        prog="ESBMC-ChatGPT",
+        # prog="ESBMC-AI",
         description=HELP_MESSAGE,
-        # argparse.RawDescriptionHelpFormatter allows the ESBMC_HELP to display
-        # properly.
+        # argparse.RawDescriptionHelpFormatter allows the ESBMC_HELP to display properly.
         formatter_class=argparse.RawDescriptionHelpFormatter,
-        epilog=f"Made by Yiannis Charalambous\n\n{ESBMC_HELP}",
+        epilog="GitHub: https://github.com/Yiannis128/esbmc-ai",
     )
 
     parser.add_argument(
@@ -225,7 +222,14 @@ def main() -> None:
     parser.add_argument(
         "remaining",
         nargs=argparse.REMAINDER,
-        help="Any arguments after the filename will be passed to ESBMC as parameters.",
+        help="Any arguments after the filename will be passed to ESBMC as parameters. Any ESBMC-AI parameters will need to be included before the filename.",
+    )
+
+    parser.add_argument(
+        "-e",
+        "--env",
+        default=None,
+        help="Override the default .env file location, which is in the current working directory.",
     )
 
     parser.add_argument(
@@ -254,24 +258,42 @@ def main() -> None:
     )
 
     parser.add_argument(
+        "--version",
+        action="version",
+        version=f"ESBMC-AI v{version}",
+    )
+
+    command_mode_parser = parser.add_argument_group(
+        title="Command Mode",
+        description="Run the program in command mode, this will skip User Chat Mode and automatically run a command. The program will exit after the command ends with an exit code.",
+    )
+
+    command_mode_parser.add_argument(
         "-c",
         "--command",
         choices=command_names,
         metavar="",
-        help="Runs the program in command mode, it will exit after the command ends with an exit code. Options: {"
-        + ", ".join(command_names)
-        + "}",
+        help="Specify the command to run. Options: {" + ", ".join(command_names) + "}",
+    )
+
+    command_mode_parser.add_argument(
+        "-p",
+        "--params",
+        default="",
+        help="Arguments for the current command, supplied using the -c or --command parameter.",
+    )
+
+    parser.add_argument_group(
+        title="ESBMC",
+        description=ESBMC_HELP,
     )
 
     args = parser.parse_args()
 
-    print("ESBMC-AI")
-    print("Made by Yiannis Charalambous")
+    print(PROLOGUE)
     print()
 
-    init_check_health(args.verbose)
-
-    config.load_envs()
+    config.load_envs(args.env)
     config.load_config(config.cfg_path)
     config.load_args(args)
 
@@ -299,10 +321,10 @@ def main() -> None:
     anim.stop()
 
     # Print verbose lvl 2
-    printvv("-" * os.get_terminal_size().columns)
+    printvv("-" * get_terminal_width())
     printvv(esbmc_output)
     printvv(esbmc_err_output)
-    printvv("-" * os.get_terminal_size().columns)
+    printvv("-" * get_terminal_width())
 
     # ESBMC will output 0 for verification success and 1 for verification
     # failed, if anything else gets thrown, it's an ESBMC error.
@@ -325,7 +347,7 @@ def main() -> None:
                 if command == command_name:
                     _run_command_mode(
                         command=commands[idx],
-                        args=[],  # NOTE: Currently not supported...
+                        args=args.params,
                         source_code=get_main_source_file().content,
                         esbmc_output=esbmc_output,
                     )
@@ -391,6 +413,7 @@ def main() -> None:
                     file_name=get_main_source_file_path(),
                     source_code=get_main_source_file().content,
                     esbmc_output=esbmc_output,
+                    max_retries=config.fix_code_max_attempts,
                 )
 
                 if not error:

esbmc_ai_lib/ai_models.py

@@ -5,10 +5,11 @@
 from enum import Enum
 from typing_extensions import override
 
-from langchain import HuggingFaceTextGenInference, PromptTemplate
 from langchain.base_language import BaseLanguageModel
 from langchain.chat_models import ChatOpenAI
+from langchain.llms import HuggingFaceTextGenInference
 
+from langchain.prompts import PromptTemplate
 from langchain.prompts.chat import ChatPromptValue
 from langchain.schema import (
     BaseMessage,

esbmc_ai_lib/commands/fix_code_command.py

@@ -1,6 +1,5 @@
 # Author: Yiannis Charalambous
 
-from os import get_terminal_size
 from time import sleep
 from typing import Tuple
 from typing_extensions import override
@@ -11,6 +10,7 @@
     json_to_base_messages,
 )
 
+from esbmc_ai_lib.term import get_terminal_width
 
 from .chat_command import ChatCommand
 from .. import config
@@ -33,7 +33,11 @@ def __init__(self) -> None:
 
     @override
     def execute(
-        self, file_name: str, source_code: str, esbmc_output: str
+        self,
+        file_name: str,
+        source_code: str,
+        esbmc_output: str,
+        max_retries: int = 10,
     ) -> Tuple[bool, str]:
         wait_time: int = int(config.consecutive_prompt_delay)
         # Create time left animation to show how much time left between API calls
@@ -62,7 +66,6 @@ def execute(
 
         print()
 
-        max_retries: int = 10
         for idx in range(max_retries):
             # Get a response. Use while loop to account for if the message stack
             # gets full, then need to compress and retry.
@@ -81,9 +84,9 @@ def execute(
 
             # Print verbose lvl 2
             printvv("\nGeneration:")
-            printvv("-" * get_terminal_size().columns)
+            printvv("-" * get_terminal_width())
             printvv(response)
-            printvv("-" * get_terminal_size().columns)
+            printvv("-" * get_terminal_width())
             printvv("")
 
             # Pass to ESBMC, a workaround is used where the file is saved
@@ -98,10 +101,10 @@ def execute(
             self.anim.stop()
 
             # Print verbose lvl 2
-            printvv("-" * get_terminal_size().columns)
+            printvv("-" * get_terminal_width())
             printvv(esbmc_output)
             printvv(esbmc_err_output)
-            printvv("-" * get_terminal_size().columns)
+            printvv("-" * get_terminal_width())
 
             if exit_code == 0:
                 self.on_solution_signal.emit(response)