From 39852d090c4107f72eb22bc97d1f8e5411d111d2 Mon Sep 17 00:00:00 2001 From: Antonio Frighetto Date: Wed, 28 Jan 2026 11:10:12 +0100 Subject: [PATCH 1/2] Extend state representation to track `errno` across control-flow 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. --- ir/memory.cpp | 12 +++++++++++ ir/state.cpp | 21 +++++++++++++++++-- ir/state.h | 8 +++++++ llvm_util/known_fns.cpp | 1 + llvm_util/llvm2alive.cpp | 2 +- .../memory/malloc-errno-fail-2.srctgt.ll | 15 +++++++++++++ .../memory/malloc-errno-fail.srctgt.ll | 15 +++++++++++++ tools/transform.cpp | 10 +++++++++ 8 files changed, 81 insertions(+), 3 deletions(-) create mode 100644 tests/alive-tv/memory/malloc-errno-fail-2.srctgt.ll create mode 100644 tests/alive-tv/memory/malloc-errno-fail.srctgt.ll diff --git a/ir/memory.cpp b/ir/memory.cpp index 44a2acfd8..8665d57c9 100644 --- a/ir/memory.cpp +++ b/ir/memory.cpp @@ -2332,6 +2332,18 @@ Memory::alloc(const expr *size, uint64_t align, BlockKind blockKind, state->addQuantVar(nondet_nonnull); allocated = precond && (nonnull || (nooverflow && nondet_nonnull)); } + + // Create a new symbolic variable that represents errno if the allocation + // fails. + if (blockKind == MALLOC || blockKind == CXX_NEW) { + expr errno_on_failure = expr::mkFreshVar("#malloc_errno", + expr::mkUInt(0, 32)); + + expr current_errno = state->getErrno(); + expr new_errno = expr::mkIf(allocated, current_errno, errno_on_failure); + state->setErrno(std::move(new_errno)); + } + return { std::move(p).release(), std::move(allocated) }; } diff --git a/ir/state.cpp b/ir/state.cpp index c2cdf2371..c976205fa 100644 --- a/ir/state.cpp +++ b/ir/state.cpp @@ -302,7 +302,9 @@ State::State(const Function &f, bool source) : f(f), source(source), memory(*this), fp_rounding_mode(expr::mkVar("fp_rounding_mode", 3)), fp_denormal_mode(expr::mkVar("fp_denormal_mode", 2)), - return_val(DisjointExpr(f.getType().getDummyValue(false))) { + errno_val(expr::mkVar("errno_init", expr::mkUInt(0, 32))), + return_val(DisjointExpr(f.getType().getDummyValue(false))), + return_errno(expr::mkUInt(0, 32)) { predecessor_data.reserve(f.getNumBBs()); } @@ -794,6 +796,7 @@ bool State::startBB(const BasicBlock &bb) { DisjointExpr in_memory; DisjointExpr UB; DisjointExpr var_args_in; + DisjointExpr errno_in; OrExpr path; domain.UB = AndExpr(); @@ -807,6 +810,7 @@ bool State::startBB(const BasicBlock &bb) { // This data is never used again, so clean it up to reduce mem consumption in_memory.add_disj(std::move(data.mem), p); var_args_in.add(std::move(data.var_args), std::move(p)); + errno_in.add_disj(std::move(data.errno_val), p); domain.undef_vars.insert(data.undef_vars.begin(), data.undef_vars.end()); data.undef_vars.clear(); @@ -825,6 +829,7 @@ bool State::startBB(const BasicBlock &bb) { domain.path = std::move(path)(); memory = *std::move(in_memory)(); var_args_data = *std::move(var_args_in)(); + errno_val = *std::move(errno_in)(); if (src_state) copyUBFromBB(I->second); @@ -858,6 +863,7 @@ void State::addJump(expr &&cond, const BasicBlock &dst0, bool always_jump) { data.path.add(std::move(cond)); data.undef_vars.insert(undef_vars.begin(), undef_vars.end()); data.undef_vars.insert(domain.undef_vars.begin(), domain.undef_vars.end()); + data.errno_val.add(errno_val, cond); if (always_jump) domain.path = false; @@ -877,6 +883,7 @@ void State::addCondJump(const expr &cond, const BasicBlock &dst_true, void State::addReturn(StateValue &&val) { get<0>(return_val).add(std::move(val), domain.path); get<0>(return_memory).add(std::move(memory), domain.path); + return_errno = expr::mkIf(domain.path, errno_val, return_errno); auto dom = domain(); return_domain.add(expr(dom)); function_domain.add(std::move(dom)); @@ -1057,6 +1064,7 @@ State::FnCallOutput State::FnCallOutput::mkIf(const expr &cond, ret.ub = expr::mkIf(cond, a.ub, b.ub); ret.noreturns = expr::mkIf(cond, a.noreturns, b.noreturns); ret.callstate = Memory::CallState::mkIf(cond, a.callstate, b.callstate); + ret.errno_val = expr::mkIf(cond, a.errno_val, b.errno_val); assert(a.ret_data.size() == b.ret_data.size()); for (unsigned i = 0, e = a.ret_data.size(); i != e; ++i) { @@ -1071,6 +1079,7 @@ expr State::FnCallOutput::refines(const FnCallOutput &rhs, expr ret = ub == rhs.ub; ret &= noreturns == rhs.noreturns; ret &= callstate == rhs.callstate; + ret &= errno_val == rhs.errno_val; function check_out = [&](const StateValue &a, const StateValue &b, const Type &ty) -> void { @@ -1262,6 +1271,11 @@ State::addFnCall(const string &name, vector &&inputs, } } + expr errno_on_write = expr::mkFreshVar((name + "#errno").c_str(), + expr::mkUInt(0, 32)); + expr errno_data = mkIf_fold(memaccess.canWrite(MemoryAccess::Errno), + errno_on_write, errno_val); + I->second = { std::move(output), expr::mkFreshVar((name + "#ub").c_str(), false), (noret || willret) @@ -1269,7 +1283,7 @@ State::addFnCall(const string &name, vector &&inputs, : expr::mkFreshVar((name + "#noreturn").c_str(), false), memory.mkCallState(name, attrs.has(FnAttrs::NoFree), I->first.args_ptr.size(), memaccess), - std::move(ret_data) }; + std::move(ret_data), std::move(errno_data) }; // add equality constraints between source's function calls for (auto II = calls_fn.begin(), E = calls_fn.end(); II != E; ++II) { @@ -1284,6 +1298,7 @@ State::addFnCall(const string &name, vector &&inputs, addUB(I->second.ub); addNoReturn(I->second.noreturns); retval = I->second.retval; + errno_val = I->second.errno_val; memory.setState(I->second.callstate, memaccess, I->first.args_ptr, inaccessible_bid); } @@ -1338,6 +1353,7 @@ State::addFnCall(const string &name, vector &&inputs, retval = std::move(d.retval); memory.setState(d.callstate, memaccess, ptr_inputs, inaccessible_bid); + errno_val = d.errno_val; fn_call_pre &= pre; if (qvar.isValid()) @@ -1551,6 +1567,7 @@ void State::cleanup() { domain = {}; analysis = {}; var_args_data = {}; + errno_val = {}; } } diff --git a/ir/state.h b/ir/state.h index bdcfd2c98..04148f56e 100644 --- a/ir/state.h +++ b/ir/state.h @@ -145,6 +145,7 @@ class State { std::set undef_vars; ValueAnalysis analysis; VarArgsData var_args; + smt::DisjointExpr errno_val; }; const Function &f; @@ -187,6 +188,7 @@ class State { Memory memory; smt::expr fp_rounding_mode; smt::expr fp_denormal_mode; + smt::expr errno_val; std::set undef_vars; ValueAnalysis analysis; std::array tmp_values; @@ -205,6 +207,7 @@ class State { std::variant, StateValue> return_val; std::variant, Memory> return_memory; std::set return_undef_vars; + smt::expr return_errno; struct FnCallInput { std::vector args_nonptr; @@ -232,6 +235,7 @@ class State { smt::expr noreturns; Memory::CallState callstate; std::vector ret_data; + smt::expr errno_val; FnCallOutput replace(const StateValue &retval) const; @@ -353,6 +357,10 @@ class State { const auto& getNondetVars() const { return nondet_vars; } const auto& getFnQuantVars() const { return fn_call_qvars; } + const auto& getErrno() const { return errno_val; } + void setErrno(smt::expr &&val) { errno_val = std::move(val); } + auto& getReturnErrno() const { return return_errno; } + const std::optional& getReturnedInput() const { return returned_input; } diff --git a/llvm_util/known_fns.cpp b/llvm_util/known_fns.cpp index 3fbbc82f0..9685f4c56 100644 --- a/llvm_util/known_fns.cpp +++ b/llvm_util/known_fns.cpp @@ -45,6 +45,7 @@ static bool implict_attrs_(llvm::LibFunc libfn, FnAttrs &attrs, auto alloc_fns = [&](unsigned idx1, unsigned idx2 = -1u) { ret_and_args_no_undef(); attrs.mem.setCanOnlyAccess(MemoryAccess::Inaccessible); + attrs.mem.setCanAlsoWrite(MemoryAccess::Errno); attrs.set(FnAttrs::NoAlias); attrs.set(FnAttrs::WillReturn); attrs.set(FnAttrs::AllocSize); diff --git a/llvm_util/llvm2alive.cpp b/llvm_util/llvm2alive.cpp index 307c6437f..c1867337b 100644 --- a/llvm_util/llvm2alive.cpp +++ b/llvm_util/llvm2alive.cpp @@ -1835,7 +1835,7 @@ class llvm2alive_ : public llvm::InstVisitor> { MemoryAccess::Inaccessible), make_pair(llvm::IRMemLocation::Other, MemoryAccess::Other), make_pair(llvm::IRMemLocation::Other, MemoryAccess::Globals), - make_pair(llvm::IRMemLocation::Other, MemoryAccess::Errno), + make_pair(llvm::IRMemLocation::ErrnoMem, MemoryAccess::Errno), }; for (auto &[ef, ty] : tys) { diff --git a/tests/alive-tv/memory/malloc-errno-fail-2.srctgt.ll b/tests/alive-tv/memory/malloc-errno-fail-2.srctgt.ll new file mode 100644 index 000000000..889b0cc23 --- /dev/null +++ b/tests/alive-tv/memory/malloc-errno-fail-2.srctgt.ll @@ -0,0 +1,15 @@ +define i32 @src(ptr %p) { + store i32 0, ptr %p + call ptr @malloc(i64 -9223372036854775808) + %v = load i32, ptr %p + ret i32 %v +} + +define i32 @tgt(ptr %p) { + store i32 0, ptr %p + ret i32 0 +} + +declare noalias ptr @malloc(i64) memory(inaccessiblemem: readwrite, errnomem: write) + +; ERROR: Mismatch in errno at return diff --git a/tests/alive-tv/memory/malloc-errno-fail.srctgt.ll b/tests/alive-tv/memory/malloc-errno-fail.srctgt.ll new file mode 100644 index 000000000..1865be323 --- /dev/null +++ b/tests/alive-tv/memory/malloc-errno-fail.srctgt.ll @@ -0,0 +1,15 @@ +define i32 @src(ptr %p, i64 %sz) { + store i32 0, ptr %p + call ptr @malloc(i64 %sz) + %v = load i32, ptr %p + ret i32 %v +} + +define i32 @tgt(ptr %p, i64 %sz) { + store i32 0, ptr %p + ret i32 0 +} + +declare noalias ptr @malloc(i64) memory(inaccessiblemem: readwrite, errnomem: write) + +; ERROR: Mismatch in errno at return diff --git a/tools/transform.cpp b/tools/transform.cpp index ee5810678..5c294ee07 100644 --- a/tools/transform.cpp +++ b/tools/transform.cpp @@ -782,6 +782,16 @@ check_refinement(Errors &errs, const Transform &t, State &src_state, : value_cnstr && memory_cnstr0), "memory", print_ptr_load, "Mismatch in memory"); + value_cnstr = expr(); + memory_cnstr0 = expr(); + + // 7. Check errno + auto errno_cnstr = src_state.getReturnErrno() == tgt_state.getReturnErrno(); + CHECK(dom && !errno_cnstr, "errno", + [](ostream &s, const Model &m) { + s << "\nErrno values do not match at return"; + }, "Mismatch in errno at return"); + #undef CHECK } From 4779d236ebf7c164b3f7becdbc4bec66ff55751d Mon Sep 17 00:00:00 2001 From: Antonio Frighetto Date: Sun, 8 Mar 2026 11:30:12 +0100 Subject: [PATCH 2/2] !fixup reuse errno_val, use std::variant --- ir/state.cpp | 18 ++++++++++++------ ir/state.h | 4 ++-- 2 files changed, 14 insertions(+), 8 deletions(-) diff --git a/ir/state.cpp b/ir/state.cpp index c976205fa..4eb2ad6d6 100644 --- a/ir/state.cpp +++ b/ir/state.cpp @@ -304,7 +304,7 @@ State::State(const Function &f, bool source) fp_denormal_mode(expr::mkVar("fp_denormal_mode", 2)), errno_val(expr::mkVar("errno_init", expr::mkUInt(0, 32))), return_val(DisjointExpr(f.getType().getDummyValue(false))), - return_errno(expr::mkUInt(0, 32)) { + return_errno(DisjointExpr(expr::mkUInt(0, 32))) { predecessor_data.reserve(f.getNumBBs()); } @@ -883,7 +883,7 @@ void State::addCondJump(const expr &cond, const BasicBlock &dst_true, void State::addReturn(StateValue &&val) { get<0>(return_val).add(std::move(val), domain.path); get<0>(return_memory).add(std::move(memory), domain.path); - return_errno = expr::mkIf(domain.path, errno_val, return_errno); + get<0>(return_errno).add(errno_val, domain.path); auto dom = domain(); return_domain.add(expr(dom)); function_domain.add(std::move(dom)); @@ -1271,10 +1271,9 @@ State::addFnCall(const string &name, vector &&inputs, } } - expr errno_on_write = expr::mkFreshVar((name + "#errno").c_str(), - expr::mkUInt(0, 32)); - expr errno_data = mkIf_fold(memaccess.canWrite(MemoryAccess::Errno), - errno_on_write, errno_val); + expr errno_data = mkIf_fold( + memaccess.canWrite(MemoryAccess::Errno), + expr::mkFreshVar((name + "#errno").c_str(), errno_val), errno_val); I->second = { std::move(output), expr::mkFreshVar((name + "#ub").c_str(), false), @@ -1421,6 +1420,13 @@ expr State::rewriteUndef(expr &&val, const set &undef_vars) { return rewriteUndef({std::move(val), expr()}, undef_vars).value; } +expr State::getReturnErrno() { + if (auto *e = get_if>(&return_errno)) { + return_errno = *std::move(*e)(); + } + return get(return_errno); +} + void State::finishInitializer() { is_initialization_phase = false; diff --git a/ir/state.h b/ir/state.h index 04148f56e..f8e067333 100644 --- a/ir/state.h +++ b/ir/state.h @@ -207,7 +207,7 @@ class State { std::variant, StateValue> return_val; std::variant, Memory> return_memory; std::set return_undef_vars; - smt::expr return_errno; + std::variant, smt::expr> return_errno; struct FnCallInput { std::vector args_nonptr; @@ -359,7 +359,7 @@ class State { const auto& getErrno() const { return errno_val; } void setErrno(smt::expr &&val) { errno_val = std::move(val); } - auto& getReturnErrno() const { return return_errno; } + smt::expr getReturnErrno(); const std::optional& getReturnedInput() const { return returned_input;