From f00d10c71ecc6caedae1e662efbdd73d7649ffe0 Mon Sep 17 00:00:00 2001 From: Hanyuan Li Date: Mon, 17 Aug 2026 12:40:06 +1000 Subject: [PATCH] fix: remove `isCmpBranchFeasible` and `isSwitchBranchFeasible` --- pybind/AE.cpp | 294 +------------------------------------------------- 1 file changed, 1 insertion(+), 293 deletions(-) diff --git a/pybind/AE.cpp b/pybind/AE.cpp index d79d181..aebb850 100644 --- a/pybind/AE.cpp +++ b/pybind/AE.cpp @@ -403,299 +403,7 @@ void bind_abstract_state(py::module& m) { .def("initObjVar", &AbstractState::initObjVar, py::arg("objVar"), "Initialize an object variable in the abstract state") .def("addToFreedAddrs", &AbstractState::addToFreedAddrs, py::arg("addr"), "Add an address to the freed addresses set") .def("isFreedMem", &AbstractState::isFreedMem, py::arg("addr"), "Check if an address is freed memory") - .def("hash", &AbstractState::hash, "Get the hash of this abstract state") - .def_static("isCmpBranchFeasible", [](SVFIR* svfir, const CmpStmt* cmpStmt, s64_t succ, AbstractState& as) { - Map _reverse_predicate = { - {CmpStmt::Predicate::FCMP_OEQ, CmpStmt::Predicate::FCMP_ONE}, // == -> != - {CmpStmt::Predicate::FCMP_UEQ, CmpStmt::Predicate::FCMP_UNE}, // == -> != - {CmpStmt::Predicate::FCMP_OGT, CmpStmt::Predicate::FCMP_OLE}, // > -> <= - {CmpStmt::Predicate::FCMP_OGE, CmpStmt::Predicate::FCMP_OLT}, // >= -> < - {CmpStmt::Predicate::FCMP_OLT, CmpStmt::Predicate::FCMP_OGE}, // < -> >= - {CmpStmt::Predicate::FCMP_OLE, CmpStmt::Predicate::FCMP_OGT}, // <= -> > - {CmpStmt::Predicate::FCMP_ONE, CmpStmt::Predicate::FCMP_OEQ}, // != -> == - {CmpStmt::Predicate::FCMP_UNE, CmpStmt::Predicate::FCMP_UEQ}, // != -> == - {CmpStmt::Predicate::ICMP_EQ, CmpStmt::Predicate::ICMP_NE}, // == -> != - {CmpStmt::Predicate::ICMP_NE, CmpStmt::Predicate::ICMP_EQ}, // != -> == - {CmpStmt::Predicate::ICMP_UGT, CmpStmt::Predicate::ICMP_ULE}, // > -> <= - {CmpStmt::Predicate::ICMP_ULT, CmpStmt::Predicate::ICMP_UGE}, // < -> >= - {CmpStmt::Predicate::ICMP_UGE, CmpStmt::Predicate::ICMP_ULT}, // >= -> < - {CmpStmt::Predicate::ICMP_SGT, CmpStmt::Predicate::ICMP_SLE}, // > -> <= - {CmpStmt::Predicate::ICMP_SLT, CmpStmt::Predicate::ICMP_SGE}, // < -> >= - {CmpStmt::Predicate::ICMP_SGE, CmpStmt::Predicate::ICMP_SLT}, // >= -> < - }; - - Map _switch_lhsrhs_predicate = { - {CmpStmt::Predicate::FCMP_OEQ, CmpStmt::Predicate::FCMP_OEQ}, // == -> == - {CmpStmt::Predicate::FCMP_UEQ, CmpStmt::Predicate::FCMP_UEQ}, // == -> == - {CmpStmt::Predicate::FCMP_OGT, CmpStmt::Predicate::FCMP_OLT}, // > -> < - {CmpStmt::Predicate::FCMP_OGE, CmpStmt::Predicate::FCMP_OLE}, // >= -> <= - {CmpStmt::Predicate::FCMP_OLT, CmpStmt::Predicate::FCMP_OGT}, // < -> > - {CmpStmt::Predicate::FCMP_OLE, CmpStmt::Predicate::FCMP_OGE}, // <= -> >= - {CmpStmt::Predicate::FCMP_ONE, CmpStmt::Predicate::FCMP_ONE}, // != -> != - {CmpStmt::Predicate::FCMP_UNE, CmpStmt::Predicate::FCMP_UNE}, // != -> != - {CmpStmt::Predicate::ICMP_EQ, CmpStmt::Predicate::ICMP_EQ}, // == -> == - {CmpStmt::Predicate::ICMP_NE, CmpStmt::Predicate::ICMP_NE}, // != -> != - {CmpStmt::Predicate::ICMP_UGT, CmpStmt::Predicate::ICMP_ULT}, // > -> < - {CmpStmt::Predicate::ICMP_ULT, CmpStmt::Predicate::ICMP_UGT}, // < -> > - {CmpStmt::Predicate::ICMP_UGE, CmpStmt::Predicate::ICMP_ULE}, // >= -> <= - {CmpStmt::Predicate::ICMP_SGT, CmpStmt::Predicate::ICMP_SLT}, // > -> < - {CmpStmt::Predicate::ICMP_SLT, CmpStmt::Predicate::ICMP_SGT}, // < -> > - {CmpStmt::Predicate::ICMP_SGE, CmpStmt::Predicate::ICMP_SLE}, // >= -> <= - }; - - AbstractState new_es = as; - // get cmp stmt's op0, op1, and predicate - NodeID op0 = cmpStmt->getOpVarID(0); - NodeID op1 = cmpStmt->getOpVarID(1); - NodeID res_id = cmpStmt->getResID(); - s32_t predicate = cmpStmt->getPredicate(); - - // if op0 or op1 is undefined, return; - // skip address compare - if (new_es.inVarToAddrsTable(op0) || new_es.inVarToAddrsTable(op1)) { - as = new_es; - return true; - } - // get '%1 = load i32 s', and load inst may not exist - auto getLoadOp = [](SVFVar* opVar) -> const LoadStmt* { - if (!opVar->getInEdges().empty()) { - SVFStmt* loadVar0InStmt = *opVar->getInEdges().begin(); - if (const LoadStmt* loadStmt = SVFUtil::dyn_cast(loadVar0InStmt)) { - return loadStmt; - } - else if (const CopyStmt* copyStmt = SVFUtil::dyn_cast(loadVar0InStmt)) { - if (!copyStmt->getRHSVar()->getInEdges().empty()) { - SVFStmt* loadVar0InStmt2 = *opVar->getInEdges().begin(); - if (const LoadStmt* loadStmt = SVFUtil::dyn_cast(loadVar0InStmt2)) { - return loadStmt; - } - } - } - } - return nullptr; - }; - const LoadStmt* load_op0 = getLoadOp(svfir->getGNode(op0)); - const LoadStmt* load_op1 = getLoadOp(svfir->getGNode(op1)); - - // for const X const, we may get concrete resVal instantly - // for var X const, we may get [0,1] if the intersection of var and const is not empty set - IntervalValue resVal = new_es[res_id].getInterval(); - resVal.meet_with(IntervalValue((s64_t)succ, succ)); - // If Var X const generates bottom value, it means this branch path is not feasible. - if (resVal.isBottom()) { - return false; - } - - bool b0 = new_es[op0].getInterval().is_numeral(); - bool b1 = new_es[op1].getInterval().is_numeral(); - - // if const X var, we should reverse op0 and op1. - if (b0 && !b1) { - std::swap(op0, op1); - std::swap(load_op0, load_op1); - predicate = _switch_lhsrhs_predicate[predicate]; - } - else { - // if var X var, we cannot preset the branch condition to infer the intervals of var0,var1 - if (!b0 && !b1) { - as = new_es; - return true; - } - // if const X const, we can instantly get the resVal - else if (b0 && b1) { - as = new_es; - return true; - } - } - // if cmp is 'var X const == false', we should reverse predicate 'var X' const == true' - // X' is reverse predicate of X - if (succ == 0) { - predicate = _reverse_predicate[predicate]; - } - else { - } - // change interval range according to the compare predicate - AddressValue addrs; - if (load_op0 && new_es.inVarToAddrsTable(load_op0->getRHSVarID())) - addrs = new_es[load_op0->getRHSVarID()].getAddrs(); - - IntervalValue &lhs = new_es[op0].getInterval(), &rhs = new_es[op1].getInterval(); - switch (predicate) { - case CmpStmt::Predicate::ICMP_EQ: - case CmpStmt::Predicate::FCMP_OEQ: - case CmpStmt::Predicate::FCMP_UEQ: { - // Var == Const, so [var.lb, var.ub].meet_with(const) - lhs.meet_with(rhs); - break; - } - case CmpStmt::Predicate::ICMP_NE: - case CmpStmt::Predicate::FCMP_ONE: - case CmpStmt::Predicate::FCMP_UNE: - // Compliment set - break; - case CmpStmt::Predicate::ICMP_UGT: - case CmpStmt::Predicate::ICMP_SGT: - case CmpStmt::Predicate::FCMP_OGT: - case CmpStmt::Predicate::FCMP_UGT: - // Var > Const, so [var.lb, var.ub].meet_with([Const+1, +INF]) - lhs.meet_with(IntervalValue(rhs.lb() + 1, IntervalValue::plus_infinity())); - break; - case CmpStmt::Predicate::ICMP_UGE: - case CmpStmt::Predicate::ICMP_SGE: - case CmpStmt::Predicate::FCMP_OGE: - case CmpStmt::Predicate::FCMP_UGE: { - // Var >= Const, so [var.lb, var.ub].meet_with([Const, +INF]) - lhs.meet_with(IntervalValue(rhs.lb(), IntervalValue::plus_infinity())); - break; - } - case CmpStmt::Predicate::ICMP_ULT: - case CmpStmt::Predicate::ICMP_SLT: - case CmpStmt::Predicate::FCMP_OLT: - case CmpStmt::Predicate::FCMP_ULT: { - // Var < Const, so [var.lb, var.ub].meet_with([-INF, const.ub-1]) - lhs.meet_with(IntervalValue(IntervalValue::minus_infinity(), rhs.ub() - 1)); - break; - } - case CmpStmt::Predicate::ICMP_ULE: - case CmpStmt::Predicate::ICMP_SLE: - case CmpStmt::Predicate::FCMP_OLE: - case CmpStmt::Predicate::FCMP_ULE: { - // Var <= Const, so [var.lb, var.ub].meet_with([-INF, const.ub]) - lhs.meet_with(IntervalValue(IntervalValue::minus_infinity(), rhs.ub())); - break; - } - case CmpStmt::Predicate::FCMP_FALSE: break; - case CmpStmt::Predicate::FCMP_TRUE: break; - default: assert(false && "implement this part"); abort(); - } - - for (const auto& addr : addrs) { - NodeID objId = as.getIDFromAddr(addr); - if (new_es.inAddrToValTable(objId)) { - switch (predicate) { - case CmpStmt::Predicate::ICMP_EQ: - case CmpStmt::Predicate::FCMP_OEQ: - case CmpStmt::Predicate::FCMP_UEQ: { - new_es.load(addr).meet_with(rhs); - break; - } - case CmpStmt::Predicate::ICMP_NE: - case CmpStmt::Predicate::FCMP_ONE: - case CmpStmt::Predicate::FCMP_UNE: - // Compliment set - break; - case CmpStmt::Predicate::ICMP_UGT: - case CmpStmt::Predicate::ICMP_SGT: - case CmpStmt::Predicate::FCMP_OGT: - case CmpStmt::Predicate::FCMP_UGT: - // Var > Const, so [var.lb, var.ub].meet_with([Const+1, +INF]) - new_es.load(addr).meet_with(IntervalValue(rhs.lb() + 1, IntervalValue::plus_infinity())); - break; - case CmpStmt::Predicate::ICMP_UGE: - case CmpStmt::Predicate::ICMP_SGE: - case CmpStmt::Predicate::FCMP_OGE: - case CmpStmt::Predicate::FCMP_UGE: { - // Var >= Const, so [var.lb, var.ub].meet_with([Const, +INF]) - new_es.load(addr).meet_with(IntervalValue(rhs.lb(), IntervalValue::plus_infinity())); - break; - } - case CmpStmt::Predicate::ICMP_ULT: - case CmpStmt::Predicate::ICMP_SLT: - case CmpStmt::Predicate::FCMP_OLT: - case CmpStmt::Predicate::FCMP_ULT: { - // Var < Const, so [var.lb, var.ub].meet_with([-INF, const.ub-1]) - new_es.load(addr).meet_with(IntervalValue(IntervalValue::minus_infinity(), rhs.ub() - 1)); - break; - } - case CmpStmt::Predicate::ICMP_ULE: - case CmpStmt::Predicate::ICMP_SLE: - case CmpStmt::Predicate::FCMP_OLE: - case CmpStmt::Predicate::FCMP_ULE: { - // Var <= Const, so [var.lb, var.ub].meet_with([-INF, const.ub]) - new_es.load(addr).meet_with(IntervalValue(IntervalValue::minus_infinity(), rhs.ub())); - break; - } - case CmpStmt::Predicate::FCMP_FALSE: break; - case CmpStmt::Predicate::FCMP_TRUE: break; - default: assert(false && "implement this part"); abort(); - } - } - } - - as = new_es; - return true; - }, py::arg("pag"), py::arg("cmpStmt"), py::arg("succ"), py::arg("as")) - .def_static("isSwitchBranchFeasible", [](SVFIR* svfir, const SVFVar* var, s64_t succ, AbstractState& as) { - Map _reverse_predicate = { - {CmpStmt::Predicate::FCMP_OEQ, CmpStmt::Predicate::FCMP_ONE}, // == -> != - {CmpStmt::Predicate::FCMP_UEQ, CmpStmt::Predicate::FCMP_UNE}, // == -> != - {CmpStmt::Predicate::FCMP_OGT, CmpStmt::Predicate::FCMP_OLE}, // > -> <= - {CmpStmt::Predicate::FCMP_OGE, CmpStmt::Predicate::FCMP_OLT}, // >= -> < - {CmpStmt::Predicate::FCMP_OLT, CmpStmt::Predicate::FCMP_OGE}, // < -> >= - {CmpStmt::Predicate::FCMP_OLE, CmpStmt::Predicate::FCMP_OGT}, // <= -> > - {CmpStmt::Predicate::FCMP_ONE, CmpStmt::Predicate::FCMP_OEQ}, // != -> == - {CmpStmt::Predicate::FCMP_UNE, CmpStmt::Predicate::FCMP_UEQ}, // != -> == - {CmpStmt::Predicate::ICMP_EQ, CmpStmt::Predicate::ICMP_NE}, // == -> != - {CmpStmt::Predicate::ICMP_NE, CmpStmt::Predicate::ICMP_EQ}, // != -> == - {CmpStmt::Predicate::ICMP_UGT, CmpStmt::Predicate::ICMP_ULE}, // > -> <= - {CmpStmt::Predicate::ICMP_ULT, CmpStmt::Predicate::ICMP_UGE}, // < -> >= - {CmpStmt::Predicate::ICMP_UGE, CmpStmt::Predicate::ICMP_ULT}, // >= -> < - {CmpStmt::Predicate::ICMP_SGT, CmpStmt::Predicate::ICMP_SLE}, // > -> <= - {CmpStmt::Predicate::ICMP_SLT, CmpStmt::Predicate::ICMP_SGE}, // < -> >= - {CmpStmt::Predicate::ICMP_SGE, CmpStmt::Predicate::ICMP_SLT}, // >= -> < - }; - - Map _switch_lhsrhs_predicate = { - {CmpStmt::Predicate::FCMP_OEQ, CmpStmt::Predicate::FCMP_OEQ}, // == -> == - {CmpStmt::Predicate::FCMP_UEQ, CmpStmt::Predicate::FCMP_UEQ}, // == -> == - {CmpStmt::Predicate::FCMP_OGT, CmpStmt::Predicate::FCMP_OLT}, // > -> < - {CmpStmt::Predicate::FCMP_OGE, CmpStmt::Predicate::FCMP_OLE}, // >= -> <= - {CmpStmt::Predicate::FCMP_OLT, CmpStmt::Predicate::FCMP_OGT}, // < -> > - {CmpStmt::Predicate::FCMP_OLE, CmpStmt::Predicate::FCMP_OGE}, // <= -> >= - {CmpStmt::Predicate::FCMP_ONE, CmpStmt::Predicate::FCMP_ONE}, // != -> != - {CmpStmt::Predicate::FCMP_UNE, CmpStmt::Predicate::FCMP_UNE}, // != -> != - {CmpStmt::Predicate::ICMP_EQ, CmpStmt::Predicate::ICMP_EQ}, // == -> == - {CmpStmt::Predicate::ICMP_NE, CmpStmt::Predicate::ICMP_NE}, // != -> != - {CmpStmt::Predicate::ICMP_UGT, CmpStmt::Predicate::ICMP_ULT}, // > -> < - {CmpStmt::Predicate::ICMP_ULT, CmpStmt::Predicate::ICMP_UGT}, // < -> > - {CmpStmt::Predicate::ICMP_UGE, CmpStmt::Predicate::ICMP_ULE}, // >= -> <= - {CmpStmt::Predicate::ICMP_SGT, CmpStmt::Predicate::ICMP_SLT}, // > -> < - {CmpStmt::Predicate::ICMP_SLT, CmpStmt::Predicate::ICMP_SGT}, // < -> > - {CmpStmt::Predicate::ICMP_SGE, CmpStmt::Predicate::ICMP_SLE}, // >= -> <= - }; - - AbstractState new_es = as; - IntervalValue& switch_cond = new_es[var->getId()].getInterval(); - s64_t value = succ; - FIFOWorkList workList; - for (SVFStmt* cmpVarInStmt : var->getInEdges()) { - workList.push(cmpVarInStmt); - } - switch_cond.meet_with(IntervalValue(value, value)); - if (switch_cond.isBottom()) { - return false; - } - while (!workList.empty()) { - const SVFStmt* stmt = workList.pop(); - if (SVFUtil::isa(stmt)) { - IntervalValue& copy_cond = new_es[var->getId()].getInterval(); - copy_cond.meet_with(IntervalValue(value, value)); - } - else if (const LoadStmt* load = SVFUtil::dyn_cast(stmt)) { - if (new_es.inVarToAddrsTable(load->getRHSVarID())) { - AddressValue& addrs = new_es[load->getRHSVarID()].getAddrs(); - for (const auto& addr : addrs) { - NodeID objId = as.getIDFromAddr(addr); - if (new_es.inAddrToValTable(objId)) { - new_es.load(addr).meet_with(switch_cond); - } - } - } - } - } - as = new_es; - return true; - }, py::arg("svfir"), py::arg("var"), py::arg("succ"), py::arg("as")); + .def("hash", &AbstractState::hash, "Get the hash of this abstract state"); // --------------------------------------------------------------- // AbstractInterpretation — owns the per-ICFGNode AbstractState trace