Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/AdithyaaSivamal/Agentic-AFL/llms.txt

Use this file to discover all available pages before exploring further.

LLMClient is the translation engine. It converts P-Code slices into Z3Py scripts via the configured LLM provider. It is not a solver — it is a translator that maps P-Code syntax to Z3 syntax. The actual satisfiability check is handled downstream by Z3Sandbox. LLMClient generates K candidate scripts per request (K-way voting), feeds correction history into repair prompts, and injects strategy hints derived from the ConstraintProfile to guide the LLM toward structurally correct solutions.

Import

from agentic_afl.orchestrator.llm_client import LLMClient

Constructor

provider
BaseLLMProvider | None
default:"None"
LLM provider instance. If None, the default provider is constructed from settings.llm_api_provider (one of "openai", "gemini", or "local"), using the corresponding API key and model name from settings.
temperature
float
default:"settings.llm_temperature (0.7)"
Sampling temperature passed to the provider. Higher values increase output variance across K candidates, which improves voting coverage. Lower values produce more deterministic scripts.
max_tokens
int
default:"settings.llm_max_output_tokens (16384)"
Maximum number of output tokens per completion. Scripts that exceed this limit are truncated, which typically produces SYNTAX_ERROR in the sandbox. Increase this for targets with complex multi-function decompiled C.

Methods

async generate_z3_scripts(request: Z3GenerationRequest) -> list[Z3Script]

Generate K candidate Z3 scripts for a stall site. This is the primary interface called by AgentLoop. The method builds a system prompt with architecture-specific BitVec width constraints and a user prompt containing:
  • The P-Code slice text
  • Ghidra decompiled C pseudocode
  • Constraint profile tags
  • Seed input hex (first 64 bytes)
  • Retrieved CARM templates as positive examples
  • Past correction history as negative examples
  • Strategy hints derived from ConstraintProfile metrics
  • REDQUEEN-style offset mapping (when base_offset > 0)
  • GDB runtime state dump (when available)
Returns a list of exactly K Z3Script objects, one per voting candidate. Each is a complete standalone Z3Py program ready for Z3Sandbox.execute().

async repair_z3_script(original_request, failed_script, error_result, attempt_number) -> Z3Script

Generate a corrected Z3 script by feeding the solver error back to the LLM. Uses a targeted repair prompt that includes the original P-Code, the failing script, the exact error string from the sandbox, and verdict-specific repair guidance. Returns a single Z3Script (one repair candidate). The AgentLoop calls this within the ReAct loop when all K initial candidates fail.
ParameterTypeDescription
original_requestZ3GenerationRequestThe original generation request containing the VulnerabilitySpec and context
failed_scriptZ3ScriptThe best-failing script selected by AgentLoop._select_best_failure()
error_resultZ3ResultThe sandbox result carrying the error message and verdict
attempt_numberintOne-indexed repair attempt count, stored in the returned Z3Script.attempt_number

Providers

Three provider implementations ship with Agentic-AFL. All implement the BaseLLMProvider abstract interface.

OpenAIProvider(api_key, model_name)

Uses AsyncOpenAI.chat.completions.create with n=K to generate all K candidates in a single API call. This is the most token-efficient approach for K-way voting.
from agentic_afl.orchestrator.llm_client import OpenAIProvider, LLMClient

client = LLMClient(
    provider=OpenAIProvider(
        api_key="sk-...",
        model_name="gpt-4.1",
    )
)

GeminiProvider(api_key, model_name)

Uses asyncio.gather to fire K independent client.aio.models.generate_content calls concurrently. Concurrent independent calls maximize variance between candidates (a requirement of the LINC K-way voting design), and avoid any candidate_count API restrictions.
from agentic_afl.orchestrator.llm_client import GeminiProvider, LLMClient

client = LLMClient(
    provider=GeminiProvider(
        api_key="AIza...",
        model_name="gemini-2.0-flash",
    )
)
The GeminiProvider logs a warning if the response finish_reason is not STOP, which typically indicates output truncation. Truncated scripts almost always produce SYNTAX_ERROR in the sandbox.

LocalProvider(endpoint, model_name)

Stub for future vLLM/Ollama integration. Interface-compatible with the other providers but raises NotImplementedError on every generate() call. Intended for offline testing and long-running campaigns without API costs.
from agentic_afl.orchestrator.llm_client import LocalProvider

# Raises NotImplementedError — not yet implemented
provider = LocalProvider(endpoint="http://localhost:8000", model_name="llama3")

Using a Custom Provider

Subclass BaseLLMProvider and implement the single abstract method generate(). Pass your instance to LLMClient(provider=...).
from agentic_afl.orchestrator.llm_client import BaseLLMProvider, LLMClient

class MyProvider(BaseLLMProvider):
    async def generate(
        self, system_prompt, user_prompt, temperature, max_tokens, n
    ) -> list[str]:
        # Call your LLM API here
        ...
        return [completion_text_1, completion_text_2, ...]

client = LLMClient(provider=MyProvider())
The generate() method must return exactly n completion strings. Each string should contain the Z3Py code wrapped in a ```python ... ``` Markdown code block. LLMClient._extract_z3_code() applies three extraction strategies (standard regex, relaxed regex, and fence-stripping fallback) to handle imperfectly formatted responses.
The LLM is given the P-Code slice and Ghidra decompiled C, and asked to produce Z3Py code with BitVec variables named byte_0, byte_1, etc. (one variable per input byte position). When the sandbox returns SAT, AgentLoop._model_to_payload() maps the byte_N model dict back to concrete input bytes and overlays them onto the original seed input.

Build docs developers (and LLMs) love