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
Constructor
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.Sampling temperature passed to the provider. Higher values increase output variance across K candidates, which improves voting coverage. Lower values produce more deterministic scripts.
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
ConstraintProfilemetrics - REDQUEEN-style offset mapping (when
base_offset > 0) - GDB runtime state dump (when available)
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.
| Parameter | Type | Description |
|---|---|---|
original_request | Z3GenerationRequest | The original generation request containing the VulnerabilitySpec and context |
failed_script | Z3Script | The best-failing script selected by AgentLoop._select_best_failure() |
error_result | Z3Result | The sandbox result carrying the error message and verdict |
attempt_number | int | One-indexed repair attempt count, stored in the returned Z3Script.attempt_number |
Providers
Three provider implementations ship with Agentic-AFL. All implement theBaseLLMProvider 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.
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.
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.
Using a Custom Provider
SubclassBaseLLMProvider and implement the single abstract method generate(). Pass your instance to LLMClient(provider=...).
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.