diff --git a/ir/memory.cpp b/ir/memory.cpp index 879731074..89956329f 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..4eb2ad6d6 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(DisjointExpr(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); + get<0>(return_errno).add(errno_val, domain.path); 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,10 @@ State::addFnCall(const string &name, vector &&inputs, } } + 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), (noret || willret) @@ -1269,7 +1282,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 +1297,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 +1352,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()) @@ -1405,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; @@ -1551,6 +1573,7 @@ void State::cleanup() { domain = {}; analysis = {}; var_args_data = {}; + errno_val = {}; } } diff --git a/ir/state.h b/ir/state.h index bdcfd2c98..f8e067333 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; + std::variant, 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); } + smt::expr getReturnErrno(); + 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 }