💻 computer science

Array-Carrying Symbolic Execution for Function Contract Generation

This paper presents a novel symbolic execution framework implemented within LLVM and integrated with Frama-C that generates function contracts by effectively carrying invariants and modification information over contiguous array segments, thereby overcoming limitations of existing approaches in analyzing array-manipulating functions.

Original authors: Weijie Lu, Jingyu Ke, Hongfei Fu, Zhouyue Sun, Yi Zhou, Guoqiang Li, Haokun Li

Published 2026-03-02

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Weijie Lu, Jingyu Ke, Hongfei Fu, Zhouyue Sun, Yi Zhou, Guoqiang Li, Haokun Li

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are a quality inspector in a massive, automated factory. Your job is to write a "User Manual" (a contract) for every machine (function) that passes through your line. This manual needs to tell you:

What you need to feed the machine (Preconditions).
What the machine will spit out (Postconditions).
What parts of the factory floor the machine is allowed to touch or change (Assigns).

The problem? Many of these machines are array-manipulating monsters. They don't just handle one item at a time; they grab huge, continuous rows of boxes (arrays) and rearrange them, search through them, or add numbers across them.

Existing inspectors (old tools) were like blindfolded workers. They could guess the rules for a single box, but when a machine grabbed a whole row of 1,000 boxes, they got confused. They couldn't tell you exactly which boxes changed or what the relationship was between the first box and the last one. They either gave up or wrote vague, useless manuals.

The New Solution: The "Carrying" Inspector

The authors of this paper built a new kind of inspector called Array-Carrying Symbolic Execution. Here is how it works, using simple analogies:

1. The "Carrying" Backpack

Imagine your inspector has a magical backpack. As the machine runs, the inspector doesn't just watch; they carry a running log of the state of the entire row of boxes.

Old Way: The inspector looked at one box, wrote down a note, looked at the next, and forgot the first.
New Way: The inspector carries a "segment" in their backpack. They know, "Okay, from box 0 to box 50, every single box is now even numbers." They carry this knowledge forward as the machine moves.

2. Handling the "Split Paths" (The Fork in the Road)

Sometimes, a machine has a "If/Else" decision.

Scenario: "If you find a zero, stop. If not, keep going."
Old Way: The inspector would try to merge these two paths into one messy, vague rule, often losing the specific details.
New Way: The inspector splits into two parallel universes. In Universe A (found a zero), they carry the note: "Boxes 0 to 10 are zeros, and we stopped here." In Universe B (didn't find a zero), they carry: "Boxes 0 to 100 are zeros, and we reached the end."
The Magic: At the end, instead of forcing a messy merge, the inspector writes a contract that says: "The result is EITHER Universe A's rule OR Universe B's rule." This keeps the information precise.

3. The "Merging" Puzzle

Imagine a machine that processes a row of boxes in two stages:

First, it processes the first 100 boxes in big batches.
Then, it processes the remaining 50 boxes one by one.

Old Way: The inspector might say, "It touched the first 100" and "It touched the last 50," but fail to realize these are actually one continuous block from 0 to 150.
New Way: The inspector sees the two separate notes in their backpack. They realize, "Hey, these two segments are right next to each other!" They merge them into a single, clean note: "The machine modified the entire row from 0 to 150."

Why This Matters

In the real world, software libraries (like the ones used for encryption or handling certificates) rely heavily on these "rows of boxes" (arrays). If you can't write a precise contract for them, you can't prove the software is safe.

The Result: The authors tested their new inspector on 282 different programs.
The Competition: A top-tier existing tool (AutoDeduct) managed to write a perfect, verifiable manual for only 10 programs.
The New Tool: Their "Carrying" inspector wrote perfect manuals for 68 programs, including complex cryptographic code that the old tools couldn't even touch.

The Catch (Limitations)

The new inspector is great at handling rows of boxes (arrays). However, it's still learning how to handle twisted chains (linked lists) or complex trees (binary trees). If the data structure is a simple, straight line, the inspector is a genius. If the data structure is a tangled knot of pointers, the inspector gets a bit confused.

Summary

Think of this paper as inventing a super-powered magnifying glass that doesn't just look at individual pixels on a screen, but understands the entire picture as a continuous, moving image. It allows computers to automatically write precise, trustworthy manuals for complex software that handles large amounts of data, ensuring that when we use these programs, we know exactly what they did and what they changed.

1. Problem Statement

The paper addresses the challenge of automated function contract generation for programs that manipulate arrays. A function contract typically consists of:

Preconditions: Constraints on input states.
Postconditions: Properties guaranteed upon termination.
Assigns information: Specification of which memory segments (variables or array ranges) are modified during execution.

The Core Challenge: Existing approaches struggle with contiguous array segments.

Abstract Interpretation: While capable of inferring array invariants, it often fails to preserve path-sensitive disjunctive loop-exit information needed to generate precise merged "assigns" clauses.
Model Checking/SMT: Often geared toward proving specific assertions rather than synthesizing reusable, general-purpose contracts ( $\langle Pre, Post, Assign \rangle$ ).
Instrumentation/LLMs: Rely heavily on manual ghost variable specification or suffer from hallucinations and lack rigorous logical guarantees.
Symbolic Execution: Traditional tools (e.g., KLEE, Clang Static Analyzer) often track memory at the level of individual elements or allocations, lacking the ability to summarize iteration effects or infer relational properties over contiguous array regions across loop executions.

2. Methodology

The authors propose a novel Symbolic Execution Framework that explicitly "carries" invariants and contiguous array segments throughout the execution path.

A. Core Architecture

The framework is implemented as a prototype within the LLVM ecosystem (approx. 19,000 lines of C++) and integrates with the ACSL (ANSI/ISO C Specification Language) and Frama-C verification platform.

The workflow involves:

Input: An abstract syntax tree (AST) of a C function.
Symbolic Execution: Simulates execution paths, maintaining a symbolic state $(M, A)$ where $M$ is a memory map and $A$ is an address map.
External Invariant Generation: Instead of inferring all invariants internally, the executor calls external plugins (based on Farkas' Lemma and idiom recognition) to generate loop invariants and summaries.
Carrying Mechanism: The framework propagates these invariants and contiguous array segments along the execution path, handling splits and merges.
Output: Synthesized function contracts in ACSL format, verified by Frama-C's WP plugin.

B. Key Technical Innovations

1. Carrying Contiguous Array Segments
Unlike traditional symbolic execution that treats array elements individually, this framework models array segments as triples: $s = \langle (\beta_b, \beta_o), \beta_{len}, C \rangle$ .

$(\beta_b, \beta_o)$ : Base address and offset.
$\beta_{len}$ : Length of the segment.
$C$ $C$ : Content summary (invariant pattern).
- Direct-Indexed Invariants: $C$ is a function of the index (e.g., $arr[i] = i + 2$).
- Aggregate Abstractions: $C$ represents reduction operations (e.g., sum, max) as first-class arithmetic expressions.
- Quantified Constraints: Complex invariants (e.g., $\forall k \in [0, i), arr[k] = 0$ ) are stored as logical statements in the path condition set.

2. Segment Management (Split, Merge, Disjunction)

Splitting: When a write operation occurs within a segment (e.g., writing to arr[j]), the segment is split into prefix and suffix segments to maintain precision.
Merging: After loops or writes, adjacent segments with syntactically equivalent content summaries are merged to form coarse-grained summaries (crucial for generating the assigns clause).
Disjunction Handling: The framework maintains disjunctive path conditions resulting from different loop exit modes (e.g., loop exits via break vs. natural termination). It carries these disjunctions forward to the post-condition, allowing for precise contracts that capture different execution scenarios.

3. Hybrid Invariant Generation
The framework integrates a plugin-based loop analyzer:

Affine/Linear Generators: Uses Farkas' Lemma reasoning for linear relations.
Idiom-Oriented Generators: Specialized plugins for common patterns like Search (finding an element), Max/Min (reduction), and Linear Search. These generate specific quantified invariants (e.g., "all elements before index $i$ are zero").

3. Key Contributions

Novel Symbolic Execution Framework: A system designed to carry numerical and array invariants from external generators, propagating them alongside program statements.
Refined Segment Treatment: A dedicated mechanism for handling the disjunction, splitting, and merging of contiguous array segments. This allows the system to track information over array ranges precisely, which is essential for deriving accurate assigns clauses and postconditions.
Implementation & Integration: A working prototype in LLVM (19k lines C++) integrated with ACSL and Frama-C, enabling end-to-end verification of generated contracts.
Handling of Disjunctive Exits: The ability to maintain disjunctive loop summaries (e.g., distinguishing between "found" and "not found" states in a search loop) and carry them to the final contract, avoiding the loss of precision common in other methods.

4. Experimental Results

The framework was evaluated against AutoDeduct (a state-of-the-art toolchain using Saida/TriCera) on 282 benchmarks, including:

SyGuS, OOPSLA-13, Frama-C Problems, SV-Comp.
Real-world libraries: X-509 (PKI) and openHiTLS (cryptographic big-number arithmetic).

Performance Metrics:

Precision (Verification Success):
- Ours: Successfully generated verifiable contracts for 68 out of 281 benchmarks.
- AutoDeduct: Successfully verified only 10 benchmarks.
- Reason: AutoDeduct failed to synthesize necessary loop invariants for most programs, rendering contracts unverifiable.
Efficiency:
- Ours: Average runtime 0.160s per file.
- AutoDeduct: Average runtime 2.706s per file (approx. 17.1x slower).
- Reason: The symbolic execution engine avoids loop unrolling and explicit enumeration of array elements by using abstract segment carrying.

Failure Analysis:

The authors' tool failed on 69 cases primarily due to syntax limitations (e.g., bitwise operators, nested loops) in the current prototype.
AutoDeduct failed mostly due to structural inability to handle complex array initializers and lack of loop invariant synthesis.

5. Significance

Bridging the Gap: This work successfully bridges the gap between low-level symbolic execution and high-level contract synthesis for array-manipulating code.
Practical Applicability: By handling real-world cryptographic libraries (openHiTLS), the framework demonstrates utility beyond synthetic academic benchmarks.
Soundness vs. Probabilistic Methods: Unlike LLM-based approaches, this framework provides deterministic, logically derivable guarantees, ensuring that generated contracts are sound consequences of the program semantics.
Foundation for Interprocedural Analysis: The ability to generate precise assigns and postconditions for array functions enables more accurate interprocedural analysis, as these contracts can be used as building blocks for analyzing larger programs.

Limitations:

Currently limited to simple pointer arithmetic (base + offset); cannot handle recursive pointer structures like linked lists or binary trees.
Support for certain operators (bitwise, modulo) and nested loops is not yet fully implemented.