docs: update klee verification pipeline

Author: kumarak

docs/KLEEVerification.md

@@ -10,6 +10,10 @@
 4. [Tool Design: `patchir-klee-harness`](#4-tool-design-patchir-klee-harness)
 5. [Generated Harness Structure](#5-generated-harness-structure)
 6. [Predicate-to-IR Translation](#6-predicate-to-ir-translation)
+   - [6.1 Targets](#61-targets)
+   - [6.2 Values and Constants](#62-values-and-constants)
+   - [6.3 Translation by Predicate Kind](#63-translation-by-predicate-kind)
+   - [6.4 Metadata String Format](#64-metadata-string-format)
 7. [YAML Override and Configuration](#7-yaml-override-and-configuration)
 8. [Runtime Contract Support](#8-runtime-contract-support)
 9. [Open Questions and Next Steps](#9-open-questions-and-next-steps)
@@ -46,13 +50,18 @@ When a contract is violated, KLEE produces a **concrete counterexample input** 
 
 Patchestry encodes contracts at two levels:
 
-**Static contracts** — encoded as LLVM metadata strings on call instructions:
+**Static contracts** — encoded as two-operand LLVM MDNode metadata on instructions.
+`patchir-cir2llvm` emits a `!static_contract` MDNode with two operands: a tag
+string (`"static_contract"`) and the serialized contract string:
 
 ```llvm
 !static_contract !56
-!56 = !{!"preconditions=[{...}], postconditions=[{...}]"}
+!56 = !{!"static_contract", !"preconditions=[{...}], postconditions=[{...}]"}
 ```
 
+The harness parser must extract the **second operand** of the MDNode to obtain
+the contract string (see `tools/patchir-cir2llvm/main.cpp` lines 432-440).
+
 **Runtime contracts** — compiled C functions merged into the IR module:
 
 ```llvm
@@ -67,7 +76,7 @@ Both contract types can be present in the patched `.ll` output and must be handl
 
 ```text
 Firmware Binary
-  → [Ghidra 12.0.1]              → P-Code JSON
+  → [Ghidra]                      → P-Code JSON
   → [patchir-decomp]             → .cir
   → [patchir-transform -spec]    → patched.cir
   → [patchir-cir2llvm -S]        → patched.ll  (with !static_contract metadata)
@@ -98,9 +107,27 @@ patchir-klee-harness \
                               #   when omitted
 ```
 
-### 4.2 Contract Source
+### 4.2 Shared Predicate Infrastructure
+
+The SeaHorn integration (`analysis/seahorn/`) and this KLEE harness tool both
+need to parse `!static_contract` metadata and translate predicates into
+verification-tool-specific IR. To avoid duplicating this logic, the following
+should be extracted into a shared library (e.g. `patchestry_contract_ir`):
+
+- **Metadata parsing**: reading `!static_contract` MDNodes and deserializing
+  them into in-memory `Predicate` structures.
+- **Predicate-to-IR translation**: converting `PredicateKind` values (range,
+  non-null, alignment, expr, etc.) into LLVM IR `icmp`/`and`/`or` sequences.
+- **Function-level contract collection**: walking a module to associate
+  contracts with their enclosing functions.
+
+Each verification backend then only needs a thin driver layer: SeaHorn emits
+`__VERIFIER_assert`/`__VERIFIER_assume`, while KLEE emits
+`klee_assume`/`abort()`.
+
+### 4.3 Contract Source
 
-Contracts are always read from the `!static_contract` metadata strings embedded on call instructions by `patchir-cir2llvm`, using a local `parseStaticContractString()` helper that attributes each contract to its enclosing LLVM function.
+Contracts are always read from the `!static_contract` metadata strings embedded on call instructions by `patchir-cir2llvm`, using the shared metadata parsing helpers described above.
 
 If `-spec <yaml>` is provided, the `contracts:` section of the spec is also parsed (reusing `ContractSpec` and `Predicate` types from `include/patchestry/YAML/ContractSpec.hpp`) and merged with the metadata-derived contracts. Spec entries take precedence over metadata for the same function, allowing per-deployment overrides without re-running the full transform pipeline.
 
@@ -127,10 +154,19 @@ For a patched function `int f(int arg0, char* arg1)` with:
 - **Precondition:** `arg0 >= 0`
 - **Postcondition:** `return_value in [0, 32]`
 
+**Note on pointer width:** The harness must derive integer widths from the
+module's `DataLayout` rather than hardcoding `i64`. For 32-bit firmware targets
+(e.g. `ARM:LE:32:Cortex`), the size parameter to `klee_make_symbolic` and the
+argument to `klee_assume` should use the target's native pointer-sized integer
+(e.g. `i32`). The examples below use `i64` for readability; the implementation
+must use `DataLayout::getIntPtrType()` to select the correct width.
+
 The tool generates the following LLVM IR appended to the patched module:
 
 ```llvm
 ; ─── KLEE runtime declarations (added once per module) ───────────────────────
+; NOTE: size_t and assume argument widths are derived from DataLayout;
+; i64 is shown here for a 64-bit target. For 32-bit targets these become i32.
 declare void @klee_make_symbolic(ptr, i64, ptr)
 declare void @klee_assume(i64)
 declare void @abort() noreturn
@@ -184,27 +220,93 @@ done:
 
 ## 6. Predicate-to-IR Translation
 
-The following table defines how each predicate kind in the contract spec is translated into harness IR:
+This section defines how each predicate kind from `Contract.td` is lowered to KLEE harness IR. Preconditions emit `klee_assume` (constraining symbolic inputs); postconditions emit `if (!cond) abort()` (KLEE reports the violation).
+
+### 6.1 Targets
+
+Targets identify what a predicate applies to. The YAML spec and serialized metadata use different spellings; the parser normalizes both:
+
+| YAML | Serialized (in `!static_contract`) | Operand in IR |
+|---|---|---|
+| `arg0` .. `argN` | `Arg(0)` .. `Arg(N)` | Loaded value of the Nth symbolic argument |
+| `return_value` | `ReturnValue` | `%result` from `call @f(...)` |
+| `symbol` + `symbol: "name"` | `Symbol(@name)` | `load @name` from the module |
+
+### 6.2 Values and Constants
+
+String values in `relation.value` and `range.min`/`max` resolve as follows:
+
+- Numeric literals (`"0"`, `"-1"`, `"0x1000"`) — parsed to `ConstantInt` matching the target type.
+- `"NULL"` / `"null"` — `ConstantPointerNull` for pointers; zero for integers.
+- Named constants (`"USB_MAX_PACKET_SIZE"`) — looked up as a module global; diagnostic + skip if absent. C `#define` values are not available as LLVM symbols and must be pre-resolved in the YAML spec.
+
+### 6.3 Translation by Predicate Kind
+
+Each subsection shows the IR pattern per target. `V` denotes the loaded target value; `PRE` = `klee_assume(cond)`, `POST` = `br i1 cond, %done, %fail` where `%fail` calls `abort()`.
+
+#### `nonnull`
+
+| Target | PRE | POST |
+|---|---|---|
+| `Arg(N)` ptr | No-op (harness allocates stack buffer; always non-null) | `icmp eq V, null` → abort (pointer-to-pointer output args) |
+| `ReturnValue` | N/A | `icmp eq %result, null` → abort |
+| `Symbol(@s)` | `klee_assume(load @s != null)` | `icmp eq load @s, null` → abort |
+
+#### `relation`
+
+Maps `relation` field to `icmp` (signed by default; unsigned for pointer-width / unsigned types):
+
+| Relation | `icmp` | | Relation | `icmp` |
+|---|---|---|---|---|
+| `eq` | `eq` | | `gt` | `sgt` / `ugt` |
+| `neq` | `ne` | | `gte` | `sge` / `uge` |
+| `lt` | `slt` / `ult` | | `none` | no IR (existence check) |
+| `lte` | `sle` / `ule` | | | |
+
+For `Arg(N)`: `PRE = klee_assume(icmp <rel> V, const)`. For `ReturnValue` / `Symbol(@s)`: `POST = if (!(icmp <rel> V, const)) abort()`. `relation: none` emits no IR — it is an existence assertion only.
+
+#### `range`
+
+Emits two `icmp` instructions ANDed together:
+
+```
+%lo = icmp sge V, resolved_min
+%hi = icmp sle V, resolved_max
+%ok = and i1 %lo, %hi
+```
+
+`Arg(N)` → PRE (`klee_assume`). `ReturnValue` / `Symbol(@s)` → POST (`abort` on `!%ok`).
+
+#### `alignment`
+
+Checks `(ptr & (align-1)) == 0` using `ptrtoint` + `and` + `icmp eq`:
+
+| Target | PRE | POST |
+|---|---|---|
+| `Arg(N)` ptr | `klee_assume(...)` | N/A |
+| `Symbol(@s)` | `klee_assume(...)` | N/A |
+| `ReturnValue` | N/A | N/A (not meaningful) |
+
+#### `expr`
+
+Free-form C-like expression string (e.g., `"size > 0 && size < MAX_LEN"`). Translation depends on complexity:
+
+- **Simple** (`"arg0 != 0"`) — lowered as a `relation` predicate.
+- **Compound** (`"a > 0 && a < 100"`) — parsed into `icmp` + `and`/`or` tree.
+- **Member access** (`"dev->state == CONFIGURED"`) — emits `getelementptr` + `load`; requires struct type metadata.
+- **Unresolvable** — emits a warning comment in output IR; predicate is skipped.
 
-| Predicate Kind | Target | Precondition IR | Postcondition IR |
-|---|---|---|---|
-| `nonnull` | `Arg(N)` pointer | No assume needed (stack buffer is always non-null) | N/A |
-| `nonnull` | `ReturnValue` | N/A | `if (result == null) abort()` |
-| `relation` | `Arg(N)` | `klee_assume(icmp <rel> arg_N, value)` | N/A |
-| `relation` | `ReturnValue` | N/A | `if (!(icmp <rel> result, value)) abort()` |
-| `range` | `Arg(N)` | `klee_assume(arg_N >= min && arg_N <= max)` | N/A |
-| `range` | `ReturnValue` | N/A | `if (!(result >= min && result <= max)) abort()` |
-| `alignment` | `Arg(N)` pointer | `klee_assume(((uintptr_t)ptr & (align-1)) == 0)` | N/A |
+PRE: `klee_assume(compiled_result)`. POST: `if (!compiled_result) abort()`.
 
-### 6.1 Metadata String Format
+### 6.4 Metadata String Format
 
-`patchir-cir2llvm`'s `serializeStaticContract()` produces the following string format (from `tools/patchir-cir2llvm/main.cpp` lines 136–231):
+`serializeStaticContract()` (`tools/patchir-cir2llvm/main.cpp:136–231`) produces:
 
 ```text
-"preconditions=[{id=\"dest_size_nonzero\", kind=relation, target=Arg(1), relation=neq, value=0}], postconditions=[{id=return_value_range, kind=range, target=ReturnValue, range=[min=0, max=32]}]"
+"preconditions=[{id=\"...\", kind=relation, target=Arg(1), relation=neq, value=0}], postconditions=[{id=..., kind=range, target=ReturnValue, range=[min=0, max=32]}]"
 ```
 
-`parseStaticContractString()` in `MetadataParser.hpp` parses this with a hand-written lexer: splits on `preconditions=[` / `postconditions=[`, extracts `{...}` blocks, then parses `key=value` pairs within each block. Results map to `ParsedPredicate` structs that mirror the existing `::contracts::PredicateAttr` field names.
+Fields per `{...}` block: `id` (always), `kind` (always), `target` (all except `expr`), plus kind-specific fields — `relation`+`value`, `range=[min=..., max=...]`, `align`, `expr`, or `symbol` (when target is `Symbol`). `parseStaticContractString()` in `MetadataParser.hpp` lexes this into `ParsedPredicate` structs.
 
 ---