feat: generic command-oracle verifier with pytest output parsing (#260)

* refactor: extract run_command method from ESBMC into BaseSourceVerifier

* refactor: decouple fix-code command from ESBMC-specific types

* feat: add command-oracle verifier with regex-based output parsing

* test: add tests for CommandOracle pytest output parser

* chore: remove unused Config import from test_config

* fix: improve ESBMC error handling and source file defaults

Author: Yiannis128

esbmc_ai/__main__.py

@@ -16,10 +16,10 @@
 
 from esbmc_ai import Config, ChatCommand, __author__, __version__
 from esbmc_ai.addon_loader import AddonLoader
+from esbmc_ai.base_component import BaseComponent
 from esbmc_ai.command_result import CommandResult
 from esbmc_ai.log_utils import LogCategories, get_log_level, init_logging
-from esbmc_ai.verifiers.base_source_verifier import BaseSourceVerifier
-from esbmc_ai.verifiers.esbmc import ESBMC
+from esbmc_ai.verifiers import BaseSourceVerifier, ESBMC, CommandOracle
 from esbmc_ai.component_manager import ComponentManager
 import esbmc_ai.commands
 
@@ -110,15 +110,19 @@ def _load_config(
 
 def _init_builtin_components() -> None:
     """Initializes the builtin verifiers and commands."""
-    component_manager = ComponentManager()
+    component_manager: ComponentManager = ComponentManager()
 
     # Built-in verifiers
-    esbmc = ESBMC.create()
+    esbmc: BaseComponent = ESBMC.create()
     assert isinstance(esbmc, BaseSourceVerifier)
     component_manager.add_verifier(esbmc)
-    # Load component-specific configuration
     component_manager.load_component_config(esbmc, builtin=True)
 
+    generic_cmd: BaseComponent = CommandOracle.create()
+    assert isinstance(generic_cmd, BaseSourceVerifier)
+    component_manager.add_verifier(generic_cmd)
+    component_manager.load_component_config(generic_cmd, builtin=True)
+
     # Init built-in commands - Loads everything in the esbmc_ai.commands module.
     commands: list[ChatCommand] = []
     for cmd_classname in getattr(esbmc_ai.commands, "__all__"):

esbmc_ai/chats/solution_generator.py

@@ -11,7 +11,7 @@
     OracleTemplateKeyProvider,
     TemplateKeyProvider,
 )
-from esbmc_ai.verifiers.esbmc import ESBMCOutput
+from esbmc_ai.verifier_output import VerifierOutput
 from esbmc_ai.chats import KeyTemplateRenderer
 
 
@@ -68,7 +68,7 @@ def generate_solution(
         self,
         initial_message_prompt: PromptTemplate,
         solution: Solution,
-        verifier_output: ESBMCOutput,
+        verifier_output: VerifierOutput,
     ) -> str:
         """Prompts the LLM to repair the source code using the verifier output.
         Returns the extracted code from the LLM's response."""

esbmc_ai/commands/fix_code_command.py

@@ -1,7 +1,6 @@
 # Author: Yiannis Charalambous
 
 from enum import Enum
-import os
 from pathlib import Path
 from typing import Any
 from pydantic import Field, field_validator
@@ -18,7 +17,8 @@
 from esbmc_ai.verifier_output import VerifierOutput
 from esbmc_ai.chat_command import ChatCommand
 from esbmc_ai.loading_widget import BaseLoadingWidget, LoadingWidget
-from esbmc_ai.verifiers.esbmc import ESBMC, ESBMCOutput
+from esbmc_ai.verifiers.base_source_verifier import BaseSourceVerifier
+from esbmc_ai.verifiers.esbmc import ESBMCOutput
 
 
 class FixCodeCommandResult(CommandResult):
@@ -137,10 +137,8 @@ def execute(self) -> FixCodeCommandResult:
         solution.add_source_file(source_file)
 
 
-        verifier: Any = ComponentManager().get_verifier("esbmc")
-        assert isinstance(verifier, ESBMC)
+        verifier: Any = ComponentManager().verifier
         verifier_output: VerifierOutput = verifier.verify_source(solution=solution)
-        assert isinstance(verifier_output, ESBMCOutput)
 
         if verifier_output.successful:
             self.logger.info("File verified successfully")
@@ -227,8 +225,8 @@ def _attempt_repair(
         solution_generator: SolutionGenerator,
         prompt: PromptTemplate,
         solution: Solution,
-        verifier: ESBMC,
-        verifier_output: ESBMCOutput,
+        verifier: BaseSourceVerifier,
+        verifier_output: VerifierOutput,
     ) -> tuple[FixCodeCommandResult | None, ESBMCOutput]:
         source_file: SourceFile = solution.files[0]
 

esbmc_ai/config.py

@@ -2,6 +2,7 @@
 
 
 from collections import defaultdict
+from enum import Enum
 from importlib.machinery import ModuleSpec
 from importlib.util import find_spec
 import logging
@@ -231,6 +232,49 @@ def on_after_set_output_dir(cls, value: Path | None) -> Path | None:
         return value
 
 
+class _CommandOracleOutputTypes(Enum):
+    PYTEST = "PYTEST"
+
+
+class CommandOracleConfig(BaseModel):
+    """Configures the command-based verifier."""
+
+    cmd: str = Field(
+        default="",
+        description=(
+            "The command to run to verify the files. The following"
+            "variables are supported:\n"
+            "1. {files} - Represents the source files."
+            "2. {includes} - Represents the include directories."
+        ),
+    )
+
+    exit_success: int = Field(
+        default=0,
+        description=("The exit code expected when the command runs successfully."),
+    )
+
+    parser: _CommandOracleOutputTypes | None = Field(
+        default=None,
+        description=(
+            "The type of verifier output to expect. Current options: "
+            f"{", ".join(t.value for t in _CommandOracleOutputTypes)}"
+        ),
+    )
+
+    @field_validator("parser", mode="before")
+    @classmethod
+    def on_set_parser(cls, value: str | None) -> _CommandOracleOutputTypes | None:
+        if not value:
+            return None
+
+        value_upper: str = value.upper()
+        if value_upper in _CommandOracleOutputTypes:
+            return _CommandOracleOutputTypes(value_upper)
+
+        raise ValueError(f"Invalid parser set: {value}")
+
+
 class ESBMCConfig(BaseModel):
     """ESBMC-specific configuration.
 
@@ -287,6 +331,11 @@ class VerifierConfig(BaseModel):
         "This is not supported by all verifiers.",
     )
 
+    command_oracle: CommandOracleConfig = Field(
+        default_factory=CommandOracleConfig,
+        description='Command oracle "command-oracle" specific configuration.',
+    )
+
     esbmc: ESBMCConfig = Field(
         default_factory=ESBMCConfig,
         description="ESBMC-specific configuration.",

esbmc_ai/solution.py

@@ -239,7 +239,7 @@ def formatted(self) -> str:
     def format_as(
         self,
         style: _SourceFileFormatStyles = "markdown",
-        include_line_numbers: bool = False,
+        include_line_numbers: bool = True,
         max_lines: int | None = None,
         working_dir: Path | None = None,
     ) -> str:

esbmc_ai/verifiers/__init__.py

@@ -1,4 +1,5 @@
 from .base_source_verifier import BaseSourceVerifier
 from .esbmc import ESBMC
+from .cmd_oracle import CommandOracle
 
-__all__ = ["BaseSourceVerifier", "ESBMC"]
+__all__ = ["BaseSourceVerifier", "ESBMC", "CommandOracle"]

esbmc_ai/verifiers/base_source_verifier.py

@@ -4,6 +4,8 @@
 
 from abc import abstractmethod
 from pathlib import Path
+from time import perf_counter
+from subprocess import PIPE, STDOUT, run, CompletedProcess
 from typing import Any, override
 from hashlib import sha256
 import pickle
@@ -140,3 +142,30 @@ def verify_source(
         """Verifies source_file."""
         _ = solution
         raise NotImplementedError()
+
+    def run_command(
+        self,
+        cmd: list[str],
+        cwd: Path,
+        process_timeout: float | None,
+    ) -> tuple[CompletedProcess, float]:
+        """Runs the verifier."""
+
+        # Add slack time to process to allow verifier to timeout and end gracefully.
+        process_timeout = process_timeout + 5 if process_timeout else None
+        # Measure execution time
+        start_time = perf_counter()
+
+        # Run ESBMC from solution working_dir and get output
+        process: CompletedProcess = run(
+            cmd,
+            cwd=cwd,
+            timeout=process_timeout,
+            stdout=PIPE,
+            stderr=STDOUT,
+            check=False,
+        )
+
+        duration: float = perf_counter() - start_time
+
+        return process, duration