Skip to content

FIX: remove isCmpBranchFeasible and isSwitchBranchFeasible #74

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
bjjwwang merged 1 commit into from
Aug 17, 2026
Merged

FIX: remove isCmpBranchFeasible and isSwitchBranchFeasible #74

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
294 changes: 1 addition & 293 deletions pybind/AE.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<s32_t, s32_t> _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<s32_t, s32_t> _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<LoadStmt>(loadVar0InStmt)) {
return loadStmt;
}
else if (const CopyStmt* copyStmt = SVFUtil::dyn_cast<CopyStmt>(loadVar0InStmt)) {
if (!copyStmt->getRHSVar()->getInEdges().empty()) {
SVFStmt* loadVar0InStmt2 = *opVar->getInEdges().begin();
if (const LoadStmt* loadStmt = SVFUtil::dyn_cast<LoadStmt>(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<s32_t, s32_t> _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<s32_t, s32_t> _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<const SVFStmt*> 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<CopyStmt>(stmt)) {
IntervalValue& copy_cond = new_es[var->getId()].getInterval();
copy_cond.meet_with(IntervalValue(value, value));
}
else if (const LoadStmt* load = SVFUtil::dyn_cast<LoadStmt>(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
Expand Down
Loading