Merge pull request #156 from esbmc/addon-verifier

Verifier Addons

.github/workflows/workflow.yml

@@ -1,4 +1,4 @@
-name: Checking
+name: Development
 on: push
 
 jobs:
@@ -20,19 +20,31 @@ jobs:
       - name: Install Hatch
         run: python -m pip install --upgrade hatch
 
+      - name: Get Hatch Dependency Hash
+        run: echo "HATCH_DEP_HASH=$(hatch dep hash)" >> $GITHUB_ENV
+
+      - name: Cache Hatch environment
+        uses: actions/cache@v4.1.2
+        with:
+          path: |
+            ~/.cache/hatch
+            ~/.local/share/hatch
+          key: ${{ runner.os }}-hatch-${{ env.HATCH_DEP_HASH }}
+
       - name: Generate Requirements
         run: python -m hatch dep show requirements > requirements.txt
 
+      # Upload requirements to have them
       - name: Upload Requirements
         uses: actions/upload-artifact@v4.4.3
         with:
           name: requirements
           path: requirements.txt
 
-
   pylint:
     name: PyLint
     runs-on: ubuntu-latest
+    needs: setup-requirements
     timeout-minutes: 10
 
     steps:
@@ -45,17 +57,28 @@ jobs:
         with:
           python-version: "3.12.0"
 
-      - name: Install pipenv
-        run: |
-          python -m pip install --upgrade pipenv wheel
+      - name: Install Hatch
+        if: steps.cache-hatch.outputs.cache-hit != 'true'
+        run: python -m pip install --upgrade hatch
 
-      - name: Install dependencies
-        run: |
-          pipenv install --deploy --dev
+      - name: Cache Hatch environment
+        uses: actions/cache@v4.1.2
+        with:
+          path: |
+            ~/.cache/hatch
+            ~/.local/share/hatch
+          key: ${{ runner.os }}-hatch-${{ env.HATCH_DEP_HASH }}
 
+      # Don't fail just output, since we want the score to be above 9 not 10.0
+      # Don’t let the Perfect be the Enemy of the Good
       - name: Pylint on esbmc_ai
+        run: hatch run pylint esbmc_ai || true
+
+      # Check if pass, the test command only takes integers so truncate decimals
+      - name: Check If Pass (90%)
         run: |
-          pipenv run pylint esbmc_ai
+          SCORE="$(sed -n '$s/[^0-9]*\([0-9.]*\).*/\1/p' <<< "$(hatch run pylint esbmc_ai)")"
+          test "${SCORE%.*}" -ge 9
 
   test:
     name: PyTest
@@ -73,27 +96,109 @@ jobs:
         with:
           python-version: "3.12.0"
 
-      - name: Download Requirements
-        uses: actions/download-artifact@v4.1.8
+      - name: Install Hatch
+        if: steps.cache-hatch.outputs.cache-hit != 'true'
+        run: python -m pip install --upgrade hatch
+
+      - name: Cache Hatch environment
+        uses: actions/cache@v4.1.2
         with:
-          name: requirements
-          path: .
+          path: |
+            ~/.cache/hatch
+            ~/.local/share/hatch
+          key: ${{ runner.os }}-hatch-${{ env.HATCH_DEP_HASH }}
+
+      - name: Run test suite
+        run: hatch run pytest
+
+  # incremenet_version:
+  #   name: Increment Version
+  #   runs-on: ubuntu-latest
+  #   needs: setup-requirements
+  #   timeout-minutes: 10
+  #   # Configure permissions for git push
+  #   permissions:
+  #     contents: write
+
+  #   steps:
+  #     - name: Check out repository code
+  #       uses: actions/checkout@v4.2.2
+  #       with:
+  #         persist-credentials: false # otherwise, the token used is the GITHUB_TOKEN, instead of your personal access token.
+  #         fetch-depth: 0 # otherwise, there would be errors pushing refs to the destination repository.
+
+  #     # Setup Python (faster than using Python container)
+  #     - name: Setup Python
+  #       uses: actions/setup-python@v5.3.0
+  #       with:
+  #         python-version: "3.12.0"
+
+  #     - name: Install Hatch
+  #       if: steps.cache-hatch.outputs.cache-hit != 'true'
+  #       run: python -m pip install --upgrade hatch
+
+  #     - name: Cache Hatch environment
+  #       uses: actions/cache@v4.1.2
+  #       with:
+  #         path: |
+  #           ~/.cache/hatch
+  #           ~/.local/share/hatch
+  #         key: ${{ runner.os }}-hatch-${{ env.HATCH_DEP_HASH }}
+
+  #     - name: Invrement Version
+  #       run: hatch version dev
+
+  #     - name: Configure Git
+  #       run: |
+  #         git config --global user.email "github-actions[bot]@users.noreply.github.com"
+  #         git config --global user.name "github-actions[bot]"
+
+  #     # Add and commit without changing message
+  #     - name: Git Add
+  #       run: |
+  #         git add esbmc_ai/__about__.py
+  #         git commit -m "Increment version"
+
+  #     - name: GitHub Push
+  #       if: github.ref != 'refs/heads/master'
+  #       uses: ad-m/github-push-action@v0.8.0
+  #       with:
+  #         github_token: ${{ secrets.GITHUB_TOKEN }}
+  #         branch: ${{ github.ref }}
+
+  build:
+    name: Build
+    runs-on: ubuntu-latest
+    needs: setup-requirements
+    timeout-minutes: 10
 
-      - name: Install Environment
-        run: python -m pip install --upgrade pipenv wheel
+    steps:
+      - name: Check out repository code
+        uses: actions/checkout@v4.2.2
 
-      - name: Cache Pipenv
-        id: cache-pipenv
-        uses: actions/cache@v4.1.2
+      # Setup Python (faster than using Python container)
+      - name: Setup Python
+        uses: actions/setup-python@v5.3.0
         with:
-          path: ~/.local/share/virtualenvs
-          key: ${{ runner.os }}-pipenv-${{ hashFiles('**/Pipfile.lock') }}
+          python-version: "3.12.0"
 
-      - name: Install dependencies
-        if: steps.cache-pipenv.outputs.cache-hit != 'true'
-        run: |
-          pipenv install -r requirements.txt
-          pipenv lock
+      - name: Install Hatch
+        if: steps.cache-hatch.outputs.cache-hit != 'true'
+        run: python -m pip install --upgrade hatch
 
-      - name: Run test suite
-        run: pipenv run pytest -v
+      - name: Cache Hatch environment
+        uses: actions/cache@v4.1.2
+        with:
+          path: |
+            ~/.cache/hatch
+            ~/.local/share/hatch
+          key: ${{ runner.os }}-hatch-${{ env.HATCH_DEP_HASH }}
+
+      - name: Hatch build
+        run: hatch build
+
+      - name: Upload build files
+        uses: actions/upload-artifact@v4.4.3
+        with:
+          name: build
+          path: dist

.gitignore

@@ -166,3 +166,5 @@ config_dev.toml
 
 # Proprietary source code samples.
 uav_test.sh
+
+addons/

esbmc_ai/__about__.py

@@ -1,4 +1,4 @@
 # Author: Yiannis Charalambous
 
-__version__ = "v0.6.0"
+__version__ = "v0.6.0.dev1"
 __author__: str = "Yiannis Charalambous"

esbmc_ai/__main__.py

@@ -8,6 +8,10 @@
 # Enables arrow key functionality for input(). Do not remove import.
 import readline
 
+from esbmc_ai.config import ConfigField
+from esbmc_ai.verifier_runner import VerifierRunner
+from esbmc_ai.verifiers.base_source_verifier import BaseSourceVerifier, VerifierOutput
+
 _ = readline
 
 from langchain_core.language_models import BaseChatModel
@@ -33,15 +37,17 @@
 from esbmc_ai.loading_widget import BaseLoadingWidget, LoadingWidget
 from esbmc_ai.chats import UserChat
 from esbmc_ai.logging import print_horizontal_line, printv, printvv
-from esbmc_ai.esbmc_util import ESBMCUtil
+from esbmc_ai.verifiers import ESBMCUtil
 from esbmc_ai.chat_response import FinishReason, ChatResponse
 from esbmc_ai.ai_models import _ai_model_names
 
 help_command: HelpCommand = HelpCommand()
 fix_code_command: FixCodeCommand = FixCodeCommand()
 exit_command: ExitCommand = ExitCommand()
-command_runner: CommandRunner = CommandRunner(
-    [
+
+verifier_runner: VerifierRunner = VerifierRunner()
+command_runner: CommandRunner = CommandRunner().init(
+    builtin_commands=[
         help_command,
         exit_command,
         fix_code_command,
@@ -112,11 +118,41 @@ def print_assistant_response(
         )
 
 
-def init_addons() -> None:
+def _load_addons() -> None:
+    """Manages loading addons"""
+    # Load all the addon commands
     command_runner.addon_commands.clear()
-    command_runner.addon_commands.extend(Config.get_value("addon_modules"))
+    command_runner.addon_commands.extend(
+        [m for m in Config.get_value("addon_modules") if isinstance(m, ChatCommand)]
+    )
     if len(command_runner.addon_commands):
-        printv("Addons:\n\t* " + "\t * ".join(command_runner.addon_commands_names))
+        printv(
+            "ChatCommand Addons:\n\t* "
+            + "\t * ".join(command_runner.addon_commands_names)
+        )
+
+    # Load all the addon verifiers
+    verifier_runner.init([ESBMCUtil()])
+    for m in Config.get_value("addon_modules"):
+        if isinstance(m, BaseSourceVerifier):
+            verifier_runner.addon_verifiers[m.verifier_name] = m
+
+    # Init config fields
+    for field in verifier_runner.init_configs():
+        Config.add_config_field(field)
+
+    Config.add_config_field(
+        ConfigField(
+            name="verifier",
+            default_value="esbmc",
+            validate=lambda v: isinstance(v, str) and v in verifier_runner.verifiers,
+            on_load=lambda v: verifier_runner.verifiers[v],
+            error_message="Invalid verifier name specified.",
+        )
+    )
+    printv(
+        "Verifier Addons:\n\t* " + "\t * ".join(verifier_runner.addon_verifier_names)
+    )
 
 
 def update_solution(source_code: str) -> None:
@@ -127,24 +163,24 @@ def _run_esbmc(source_file: SourceFile, anim: BaseLoadingWidget) -> str:
     assert source_file.file_path
 
     with anim("ESBMC is processing... Please Wait"):
-        exit_code, esbmc_output = ESBMCUtil.esbmc(
-            path=source_file.file_path,
+        verifier_result: VerifierOutput = verifier_runner.verifier.verify_source(
+            source_file=source_file,
             esbmc_params=Config.get_value("esbmc.params"),
             timeout=Config.get_value("esbmc.timeout"),
         )
 
     # ESBMC will output 0 for verification success and 1 for verification
     # failed, if anything else gets thrown, it's an ESBMC error.
-    if not Config.get_value("allow_successful") and exit_code == 0:
+    if not Config.get_value("allow_successful") and verifier_result.successful():
         printv("Success!")
-        print(esbmc_output)
+        print(verifier_result.output)
         sys.exit(0)
-    elif exit_code != 0 and exit_code != 1:
-        printv(f"ESBMC exit code: {exit_code}")
-        printv(f"ESBMC Output:\n\n{esbmc_output}")
+    elif verifier_result.return_code != 0 and verifier_result.return_code != 1:
+        printv(f"ESBMC exit code: {verifier_result.return_code}")
+        printv(f"ESBMC Output:\n\n{verifier_result.output}")
         sys.exit(1)
 
-    return esbmc_output
+    return verifier_result.output
 
 
 def init_commands() -> None:
@@ -304,9 +340,8 @@ def main() -> None:
     print()
 
     Config.init(args)
-    ESBMCUtil.init(Config.get_value("esbmc.path"))
     check_health()
-    init_addons()
+    _load_addons()
 
     printv(f"Source code format: {Config.get_value('source_code_format')}")
     printv(f"ESBMC output type: {Config.get_value('esbmc.output_type')}")
@@ -391,6 +426,7 @@ def main() -> None:
     chat = UserChat(
         ai_model=Config.get_ai_model(),
         llm=chat_llm,
+        verifier=verifier_runner.verifier,
         source_code=source_file.latest_content,
         esbmc_output=source_file.latest_verifier_output,
         system_messages=Config.get_user_chat_system_messages(),

esbmc_ai/chat_response.py

@@ -49,6 +49,6 @@ def dict_to_base_message(json_string: dict) -> BaseMessage:
         raise Exception()
 
 
-def list_to_base_messages(json_messages: list[dict]) -> list[BaseMessage]:
+def list_to_base_messages(json_messages: list[dict]) -> tuple[BaseMessage, ...]:
     """Converts a list of messages from JSON format to a list of BaseMessage."""
-    return [dict_to_base_message(msg) for msg in json_messages]
+    return tuple(dict_to_base_message(msg) for msg in json_messages)