Extend state representation to track `errno` across control-flow by antoniofrighetto · Pull Request #1284 · AliveToolkit/alive2

antoniofrighetto · 2026-02-04T16:43:24Z

An attempt to handle errno in order to prevent Alive2 from treating store-to-load forwarding as valid refinements, if may alias errno. This is achieved by adding a new SMT expression to model errno meant to be used on malloc failure. Also treat malloc et alia as may write errno via LLVM errnomem location kind while translating from LLVM IR.

A thank to Nuno for direction on this!

An attempt to handle `errno` in order to prevent Alive2 from treating store-to-load forwarding as valid refinements, if may alias `errno`. This is achieved by adding a new SMT expression to model `errno` meant to be used on malloc failure. Also treat malloc et alia as may write errno via LLVM `errnomem` location kind while translating from LLVM IR.

antoniofrighetto · 2026-02-04T16:43:51Z

ir/memory.cpp

+
+  // Create a new symbolic variable that represents errno if the allocation
+  // fails.
+  if (blockKind == MALLOC || blockKind == CXX_NEW) {


We don’t seem to model realloc as of now, correct?

we do support realloc!

IIUC, there doesn't appear to exist a separate REALLOC block kind, instead we seem to reuse MALLOC one when encoding realloc calls (AllocKind::Realloc) into SMT expressions:

alive2/ir/instr.cpp

Lines 2774 to 2775 in 2cb1034

auto [p_new, allocated]

= m.alloc(&size, getAlign(), Memory::MALLOC, np_size, nonnull);

antoniofrighetto · 2026-02-04T16:46:17Z

ir/memory.cpp

+    expr errno_on_failure = expr::mkFreshVar("#malloc_errno",
+                                             expr::mkUInt(0, 32));


I’m experiencing the following false positive for test attrs/allocsize.srctgt.ll:

declare ptr @my_malloc(i32) allocsize(0) define ptr @src() { #0: %p = call ptr @my_malloc(i32 23) allocsize(0) ret ptr %p } => declare ptr @my_malloc(i32) allocsize(0) define ptr @tgt() { #0: %p = call ptr @my_malloc(i32 23) dereferenceable_or_null(23) allocsize(0) ret ptr %p }  src_state.getReturnErrno(): (ite (or malloc_never_fails |#alloc_nondet_nonnull!3|) errno_init |#malloc_errno!4|)   tgt_state.getReturnErrno(): (ite (or malloc_never_fails |#alloc_nondet_nonnull!6|) errno_init |#malloc_errno!7|) Transformation doesn't verify! ERROR: Mismatch in errno at return

Possibly we shouldn’t use fresh unique symbolic variables for malloc_errno: I tried switching from using mkFreshVar w/ addNonDetVar to using the dedicated helper getFreshNondetVar instead. This fixes this issue but in doing so we don’t ; ERROR: Mismatch in errno at return anymore for the two new added tests (so we allow the refinement as valid). Any idea on what I'm missing?

regehr · 2026-02-04T18:36:22Z

this is super cool, I never thought about errno being something special we'd need to handle!

nunoplopes · 2026-02-04T18:52:41Z

tests/alive-tv/memory/malloc-errno-fail.srctgt.ll

+
+declare noalias ptr @malloc(i64) memory(inaccessiblemem: readwrite, errnomem: write)
+
+; ERROR: Mismatch in errno at return


this is not the expected behavior. LLVM wants to allow removal of allocation functions.

This is annoying, maybe we need to model alloc functions as written to errno only non-deterministically?

@RalfJung @nikic

We generally consider allocation functions to only be called non-deterministically I think -- see llvm/llvm-project#177592.

nunoplopes · 2026-02-04T18:55:16Z

ir/state.cpp

      }

+      expr errno_on_write = expr::mkFreshVar((name + "#errno").c_str(),
+                                             expr::mkUInt(0, 32));


instead of mkUInt, you can use errno_val.
I would also move this call inside mkIf_fold to avoid creating the expression altogether

nunoplopes · 2026-02-04T18:56:50Z

ir/state.h

  std::variant<smt::DisjointExpr<StateValue>, StateValue> return_val;
  std::variant<smt::DisjointExpr<Memory>, Memory> return_memory;
  std::set<smt::expr> return_undef_vars;
+  smt::expr return_errno;


you can use the std::variant trick above to keep a DisjointExpr during state execution. This can shrink final expr size.

Done, thanks (I originally thought this wasn't necessary for a simple smt::expr).

RalfJung · 2026-02-05T20:38:42Z

An attempt to handle errno in order to prevent Alive2 from treating store-to-load forwarding as valid refinements, if may alias errno.

What makes errno special here?

antoniofrighetto · 2026-03-08T10:35:40Z

An attempt to handle errno in order to prevent Alive2 from treating store-to-load forwarding as valid refinements, if may alias errno.

What makes errno special here?

I think, per se, nothing makes errno semantically special here, it's just observable global state. Currently, Alive2 treats malloc has side-effect-free wrt errno, meaning that folding %v to 0 here:

store i32 0, ptr %p
call ptr @malloc(i64 INT64_MAX) ; may set errno
%v = load i32, ptr %p

would be allowed; except that it should not, as %p may happen to alias errno. On a discussion with Nuno, this may be modelled with varying fidelity. Particularly, it was determined to use a single symbolic variable (malloc_failure), and have every failed allocation set errno to such a variable. This RFC shows how errno, now part of MemoryEffects, is in the process of being modelled in LLVM.

RalfJung · 2026-03-08T11:00:07Z

So the idea is that errno is the only global state observable by the program that malloc is allowed to mutate, and it may also only be mutated on allocation failure (and presumably, malloc is never allowed to itself observe errno, it can only be indiscriminantly overwritten)?

antoniofrighetto · 2026-03-08T11:24:50Z

Yes, this at least is my understanding. malloc will start, hopefully, being declared as memory(inaccessiblemem: readwrite, errnomem: write) some time soon in LLVM: the inaccessiblemem part is memory outside the control of LLVM, and errno should be the only program global-visibile state malloc may mutate (and, indeed, from the new annotation, malloc should only be allowed to write to it).

antoniofrighetto commented Feb 4, 2026

View reviewed changes

nunoplopes reviewed Feb 4, 2026

View reviewed changes

IamYJLee mentioned this pull request Feb 11, 2026

Fix handling of allocation functions without allocsize attribute - #1238 #1252

Open

antoniofrighetto added 2 commits March 8, 2026 11:19

Merge branch 'master' into feature/handle-errno-for-malloc

8f39eb1

!fixup reuse errno_val, use std::variant

4779d23

	auto [p_new, allocated]
	= m.alloc(&size, getAlign(), Memory::MALLOC, np_size, nonnull);

		expr errno_on_failure = expr::mkFreshVar("#malloc_errno",
		expr::mkUInt(0, 32));


		declare noalias ptr @malloc(i64) memory(inaccessiblemem: readwrite, errnomem: write)

		; ERROR: Mismatch in errno at return

Conversation

antoniofrighetto commented Feb 4, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

regehr commented Feb 4, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

RalfJung commented Feb 5, 2026

Uh oh!

antoniofrighetto commented Mar 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

RalfJung commented Mar 8, 2026

Uh oh!

antoniofrighetto commented Mar 8, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

antoniofrighetto commented Mar 8, 2026 •

edited

Loading