Motivation
While working on formal verification with Alive2, we observed a mismatch between LLVM optimizations and the assumptions made by verification tools when reasoning about calls to custom allocator functions. In particular, the presence or absence of control-flow attributes such as willreturn changed whether a call was considered as potentially non-returning, which in turn affected both optimization results and verification outcomes.
This revealed a broader issue: LLVM IR relies on implicit semantic assumptions about allocator calls that are not clearly specified in LangRef. As a result, optimizations may rely on undocumented properties, verification tools must guess missing semantics, and users cannot know which guarantees their custom allocators must provide.
This RFC aims to clarify what semantic guarantees (if any) LLVM assumes for custom allocator calls, especially along the following three axes:
- Termination: Does the call return, or may it diverge?
- Exceptions: Can the call unwind or throw?
- Side Effects: Does the call have observable effects beyond memory allocation?
Definitions
In this RFC, the term custom allocator refers to any function call that LLVM treats as an allocator due to the presence of allocator-related attributes, such as:
allockind,allocptr,alloc-family,allocsize, or similar
This definition does not assume any specific control-flow or effect behavior beyond what is explicitly stated by attributes.
Scope
This RFC focuses on one question:
What semantic guarantees does LLVM assume for custom allocator calls, and where should these be specified?
It does not attempt to:
- Redefine all allocator-related attributes
- Specify malloc/free families
- Redesign effect or control-flow attributes (e.g.,
willreturn,nounwind)
Problem Statement
In verification experiments, a custom allocator function without control-flow attributes such as willreturn was conservatively modeled as potentially non-returning.
As a result, transformations that removed or simplified such calls failed to verify, because the call was considered unable to return.
This behavior was observed in Alive2 (see PR #1252). When willreturn was added to the custom allocator declaration, the verification succeeded.
This concrete case shows that the behavior of allocator calls depends critically on whether control-flow attributes are present, and that different tools may make different assumptions in their absence.
define i64 @src() {
#0:
%stack = call ptr @myalloc() allockind(alloc)
%sz = objectsize ptr %stack, i1 0, i1 0
ret i64 %sz
}
=>
define i64 @tgt() {
#0:
ret i64 -1
}
Transformation doesn't verify!
ERROR: Source and target don't have the same return domain
Example:
Source:
ptr %stack = function did not return!
Otherwise, when we used a custom allocator with a control-flow attribute such as willreturn, the verification succeeded.
declare ptr @myalloc() willreturn allockind(alloc)
define i64 @src() {
#0:
%stack = call ptr @myalloc() willreturn allockind(alloc)
%sz = objectsize ptr %stack, i1 0, i1 0
ret i64 %sz
}
=>
define i64 @tgt() {
#0:
ret i64 -1
}
Transformation seems to be correct!
Proposed Specification Options
This section proposes two possible directions for LangRef clarification.
Option A: Conservative Semantics
Allocator-related attributes do not imply any control-flow or effect guarantees.
- Termination: May diverge unless explicitly marked
willreturn. - Exceptions: May unwind unless explicitly marked
nounwind. - Side Effects: May have side effects beyond allocation unless restricted by effect attributes.
Option B: Implicit Allocator Guarantees
Calls treated as allocators are assumed to satisfy certain default guarantees, such as:
- Termination: Assumed to return unless explicitly marked otherwise.
- Exceptions: Assumed not to unwind unless explicitly marked.
- Side Effects: Assumed to have no observable effects beyond allocation and possible failure.
Questions for the Community
- Should allocator-related attributes imply any termination guarantees by default?
- Should they imply absence of unwinding or side effects beyond allocation?
- Are current optimizations relying on undocumented assumptions?
CC : @nlopes – Thanks for your time and feedback!
