AbstractInterpretation.cpp

Go to the documentation of this file.

//===- AbstractExecution.cpp -- Abstract Execution---------------------------------//
//
//                     SVF: Static Value-Flow Analysis
//
// Copyright (C) <2013->  <Yulei Sui>
//
 
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU Affero General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
 
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU Affero General Public License for more details.
 
// You should have received a copy of the GNU Affero General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
//
//===----------------------------------------------------------------------===//
 
 
//
//  Created on: Jan 10, 2024
//      Author: Xiao Cheng, Jiawei Wang
//
 
#include "AE/Svfexe/AbstractInterpretation.h"
#include "AE/Svfexe/SparseAbstractInterpretation.h"
#include "AE/Svfexe/AbsExtAPI.h"
#include "SVFIR/SVFIR.h"
#include "Util/Options.h"
#include "Util/WorkList.h"
#include "Graphs/CallGraph.h"
#include "WPA/Andersen.h"
#include <cmath>
#include <memory>
 
using namespace SVF;
using namespace SVFUtil;
 
 
void AbstractInterpretation::runOnModule()
{
    stat->startClk();
    utils = new AbsExtAPI(this);
    utils->collectCheckPoint();
 
    analyse();
    utils->checkPointAllSet();
    stat->endClk();
    stat->finializeStat();
    if (Options::PStat())
        stat->performStat();
    for (auto& detector: detectors)
        detector->reportBug();
}
 
AbstractInterpretation::AbstractInterpretation()
{
    stat = new AEStat(this);
    // Run Andersen's pointer analysis and build WTO
    svfir = PAG::getPAG();
    icfg = svfir->getICFG();
    preAnalysis = new AEWTO(svfir, icfg);
    callGraph = preAnalysis->getCallGraph();
    icfg->updateCallGraph(callGraph);
    preAnalysis->initWTO();
}

AbstractInterpretation& AbstractInterpretation::getAEInstance()
{
    // Leak the singleton on purpose.  AbstractInterpretation owns a
    // Map<std::string, std::function<void(const CallICFGNode*)>> func_map
    // whose lambda closures back-reference state owned by other globals
    // (preAnalysis's WTO, the call graph, ...).  Letting the static
    // unique_ptr's atexit-time destructor run hits a static-destruction-
    // order issue: the func_map hashtable's destructor calls into
    // std::function destroyers whose closures touch already-destroyed
    // state, and ~_Hashtable() segfaults during normal program shutdown.
    //
    // Reliably reproducible from any downstream tool that drives a full
    // AE analysis to completion and then exits normally:
    //   - SSA's ass3 binary (Software-Security-Analysis/Assignment-3)
    //   - pysvf via Python interpreter shutdown
    //
    // A process-lifetime singleton has no observable lifecycle past
    // program exit, so leaking is benign and avoids the use-after-destroy.
    static AbstractInterpretation* instance = []() -> AbstractInterpretation*
    {
        switch (Options::AESparsity())
        {
        case AESparsity::SemiSparse:
            return new SemiSparseAbstractInterpretation();
        case AESparsity::Sparse:
            return new FullSparseAbstractInterpretation();
        case AESparsity::Dense:
        default:
            return new AbstractInterpretation();
        }
    }();
    return *instance;
}
 

AbstractInterpretation::~AbstractInterpretation()
{
    delete utils;
    delete stat;
    delete preAnalysis;
}

FIFOWorkList<const FunObjVar*> AbstractInterpretation::collectProgEntryFuns()
{
    FIFOWorkList<const FunObjVar*> entryFunctions;
    const bool mainEntry = Options::AEFunEntry() == AEFunEntryMode::MAIN;
    Set<NodeID> visitedEntrySCCs;
    auto* callGraphSCC = preAnalysis->getCallGraphSCC();
 
    for (auto it = callGraph->begin(); it != callGraph->end(); ++it)
    {
        const CallGraphNode* cgNode = it->second;
        const FunObjVar* fun = cgNode->getFunction();
 
        // Skip declarations
        if (fun->isDeclaration())
            continue;
 
        if (mainEntry)
        {
            if (SVFUtil::isProgEntryFunction(fun))
            {
                entryFunctions.push(fun);
                break;
            }
        }
        else
        {
            NodeID repNodeId = callGraphSCC->repNode(cgNode->getId());
            if (visitedEntrySCCs.count(repNodeId))
                continue;
 
            const NodeBS& cgSCCNodes = callGraphSCC->subNodes(repNodeId);
            bool hasExternalCaller = false;
            for (NodeID nodeId : cgSCCNodes)
            {
                const CallGraphNode* sccNode = callGraph->getGNode(nodeId);
                for (auto inEdge : sccNode->getInEdges())
                {
                    if (!cgSCCNodes.test(inEdge->getSrcID()))
                    {
                        hasExternalCaller = true;
                        break;
                    }
                }
                if (hasExternalCaller)
                    break;
            }
 
            if (hasExternalCaller)
                continue;
 
            visitedEntrySCCs.insert(repNodeId);
            const FunObjVar* entryFun = fun;
            for (NodeID nodeId : cgSCCNodes)
            {
                const FunObjVar* sccFun = callGraph->getGNode(nodeId)->getFunction();
                if (SVFUtil::isProgEntryFunction(sccFun))
                {
                    entryFun = sccFun;
                    break;
                }
            }
            entryFunctions.push(entryFun);
        }
    }
 
    if (mainEntry && entryFunctions.empty())
    {
        SVFUtil::errs() << SVFUtil::errMsg(
                            "AE -ae-fun-entry=main requires a program entry function, but main/svf.main was not found.\n");
        assert(false && "No program entry function found for -ae-fun-entry=main");
        abort();
    }
 
    return entryFunctions;
}
 

void AbstractInterpretation::analyse()
{
    analyzeFromAllProgEntries();
}

void AbstractInterpretation::analyzeFromAllProgEntries()
{
    // Collect all entry point functions
    FIFOWorkList<const FunObjVar*> entryFunctions = collectProgEntryFuns();
 
    if (entryFunctions.empty())
    {
        assert(false && "No entry functions found for analysis");
        return;
    }
    // handle Global ICFGNode of SVFModule
    handleGlobalNode();
    const ICFGNode* globalNode = icfg->getGlobalICFGNode();
    while (!entryFunctions.empty())
    {
        const FunObjVar* entryFun = entryFunctions.pop();
        const ICFGNode* funEntry = icfg->getFunEntryICFGNode(entryFun);
        updateAbsState(funEntry, getAbsState(globalNode));
        handleFunction(funEntry, nullptr);
    }
}

void AbstractInterpretation::handleGlobalNode()
{
    const ICFGNode* node = icfg->getGlobalICFGNode();
    // Global init is one of the few legitimate direct-mutation sites:
    // updateAbsState filters out ValVars in semi-sparse mode, but NullPtr/
    // BlkPtr have no SVFVar so we cannot route them through updateAbsValue.
    // Use the manager's operator[] (auto-creates the entry if absent).
    AbstractState& init = abstractTrace[node];
    init = AbstractState();
    // NullPtr has no backing SVFVar. Model it directly as the singleton null
    // address; BlkPtr is initialized directly below for the same reason.
    init[IRGraph::NullPtr] = AddressValue(NullMemAddr);
 
    // Global Node, we just need to handle addr, load, store, copy and gep
    for (const SVFStmt *stmt: node->getSVFStmts())
    {
        handleSVFStatement(stmt);
    }
 
    // BlkPtr is the canonical unknown value.  Keep its address-domain meaning
    // for pointer uses, and also give it numeric top so external-input stores
    // can flow through ordinary store/load state as [-inf, +inf].
    AbstractValue blkPtrValue(IntervalValue::top());
    blkPtrValue.getAddrs().insert(BlackHoleObjAddr);
    abstractTrace[node][PAG::getPAG()->getBlkPtr()] = blkPtrValue;
}

bool AbstractInterpretation::mergeStatesFromPredecessors(const ICFGNode* node)
{
    // Collect all feasible predecessor states, then merge at the end.
    AbstractState merged;
    bool hasFeasiblePred = false;
 
    for (auto& edge : node->getInEdges())
    {
        const ICFGNode* pred = edge->getSrcNode();
        if (!hasAbsState(pred))
            continue;
 
        AbstractState predState = getAbsState(pred);
        bool feasible = false;
        if (const IntraCFGEdge* intraCfgEdge = SVFUtil::dyn_cast<IntraCFGEdge>(edge))
        {
            if (intraCfgEdge->getCondition())
            {
                feasible = isBranchEdgeFeasible(intraCfgEdge, predState);
                if (feasible)
                    applyBranchRefinement(intraCfgEdge, predState);
            }
            else
            {
                feasible = true;
            }
        }
        else if (SVFUtil::isa<CallCFGEdge>(edge))
        {
            feasible = true;
        }
        else if (SVFUtil::isa<RetCFGEdge>(edge))
        {
            switch (Options::HandleRecur())
            {
            case TOP:
                feasible = true;
                break;
            case WIDEN_ONLY:
            case WIDEN_NARROW:
            {
                const RetICFGNode* returnSite = SVFUtil::dyn_cast<RetICFGNode>(node);
                const CallICFGNode* callSite = returnSite->getCallICFGNode();
                feasible = hasAbsState(callSite);
                break;
            }
            }
        }
 
        if (feasible)
        {
            if (Options::AESparsity() == AESparsity::Sparse)
            {
                // getAEInstance() selects this class for Sparse mode.
                static_cast<FullSparseAbstractInterpretation*>(this)->mergeFreedAddrs(merged, predState);
            }
            else
                joinStates(merged, predState);
            hasFeasiblePred = true;
        }
    }
 
    if (!hasFeasiblePred)
        return false;
 
    updateAbsState(node, merged);
 
    return true;
}

static const LoadStmt* findBackingLoad(const SVFVar* var)
{
    if (var->getInEdges().empty())
        return nullptr;
    SVFStmt* inStmt = *var->getInEdges().begin();
    if (const LoadStmt* ls = SVFUtil::dyn_cast<LoadStmt>(inStmt))
        return ls;
    if (const CopyStmt* cs = SVFUtil::dyn_cast<CopyStmt>(inStmt))
    {
        const SVFVar* src = cs->getRHSVar();
        if (!src->getInEdges().empty())
            return SVFUtil::dyn_cast<LoadStmt>(*src->getInEdges().begin());
    }
    return nullptr;
}

static IntervalValue computeCmpConstraint(s32_t predicate, s64_t succ,
        bool isLHS, const IntervalValue& self,
        const IntervalValue& other)
{
    // Normalize: always reason from the LHS perspective.
    // If we are the RHS operand, swap the predicate direction.
    if (!isLHS)
    {
        // a > b from b's perspective: b < a
        static const Map<s32_t, s32_t> swapPred =
        {
            {CmpStmt::ICMP_EQ,  CmpStmt::ICMP_EQ},
            {CmpStmt::ICMP_NE,  CmpStmt::ICMP_NE},
            {CmpStmt::ICMP_SGT, CmpStmt::ICMP_SLT},
            {CmpStmt::ICMP_SGE, CmpStmt::ICMP_SLE},
            {CmpStmt::ICMP_SLT, CmpStmt::ICMP_SGT},
            {CmpStmt::ICMP_SLE, CmpStmt::ICMP_SGE},
            {CmpStmt::ICMP_UGT, CmpStmt::ICMP_ULT},
            {CmpStmt::ICMP_UGE, CmpStmt::ICMP_ULE},
            {CmpStmt::ICMP_ULT, CmpStmt::ICMP_UGT},
            {CmpStmt::ICMP_ULE, CmpStmt::ICMP_UGE},
            {CmpStmt::FCMP_OEQ, CmpStmt::FCMP_OEQ},
            {CmpStmt::FCMP_UEQ, CmpStmt::FCMP_UEQ},
            {CmpStmt::FCMP_OGT, CmpStmt::FCMP_OLT},
            {CmpStmt::FCMP_OGE, CmpStmt::FCMP_OLE},
            {CmpStmt::FCMP_OLT, CmpStmt::FCMP_OGT},
            {CmpStmt::FCMP_OLE, CmpStmt::FCMP_OGE},
            {CmpStmt::FCMP_UGT, CmpStmt::FCMP_ULT},
            {CmpStmt::FCMP_UGE, CmpStmt::FCMP_ULE},
            {CmpStmt::FCMP_ULT, CmpStmt::FCMP_UGT},
            {CmpStmt::FCMP_ULE, CmpStmt::FCMP_UGE},
            {CmpStmt::FCMP_ONE, CmpStmt::FCMP_ONE},
            {CmpStmt::FCMP_UNE, CmpStmt::FCMP_UNE},
        };
        auto it = swapPred.find(predicate);
        if (it == swapPred.end()) return IntervalValue::top();
        predicate = it->second;
    }
 
    // If false branch, negate the predicate.
    if (succ == 0)
    {
        static const Map<s32_t, s32_t> negPred =
        {
            {CmpStmt::ICMP_EQ,  CmpStmt::ICMP_NE},
            {CmpStmt::ICMP_NE,  CmpStmt::ICMP_EQ},
            {CmpStmt::ICMP_SGT, CmpStmt::ICMP_SLE},
            {CmpStmt::ICMP_SGE, CmpStmt::ICMP_SLT},
            {CmpStmt::ICMP_SLT, CmpStmt::ICMP_SGE},
            {CmpStmt::ICMP_SLE, CmpStmt::ICMP_SGT},
            {CmpStmt::ICMP_UGT, CmpStmt::ICMP_ULE},
            {CmpStmt::ICMP_UGE, CmpStmt::ICMP_ULT},
            {CmpStmt::ICMP_ULT, CmpStmt::ICMP_UGE},
            {CmpStmt::ICMP_ULE, CmpStmt::ICMP_UGT},
            {CmpStmt::FCMP_OEQ, CmpStmt::FCMP_ONE},
            {CmpStmt::FCMP_UEQ, CmpStmt::FCMP_UNE},
            {CmpStmt::FCMP_OGT, CmpStmt::FCMP_OLE},
            {CmpStmt::FCMP_OGE, CmpStmt::FCMP_OLT},
            {CmpStmt::FCMP_OLT, CmpStmt::FCMP_OGE},
            {CmpStmt::FCMP_OLE, CmpStmt::FCMP_OGT},
            {CmpStmt::FCMP_UGT, CmpStmt::FCMP_ULE},
            {CmpStmt::FCMP_UGE, CmpStmt::FCMP_ULT},
            {CmpStmt::FCMP_ULT, CmpStmt::FCMP_UGE},
            {CmpStmt::FCMP_ULE, CmpStmt::FCMP_UGT},
            {CmpStmt::FCMP_ONE, CmpStmt::FCMP_OEQ},
            {CmpStmt::FCMP_UNE, CmpStmt::FCMP_UEQ},
        };
        auto it = negPred.find(predicate);
        if (it == negPred.end()) return IntervalValue::top();
        predicate = it->second;
    }
 
    // Now compute the constraint on LHS given: LHS <predicate> other
    IntervalValue result = self;
    switch (predicate)
    {
    case CmpStmt::ICMP_EQ:
    case CmpStmt::FCMP_OEQ:
    case CmpStmt::FCMP_UEQ:
        result.meet_with(other);
        break;
    case CmpStmt::ICMP_NE:
    case CmpStmt::FCMP_ONE:
    case CmpStmt::FCMP_UNE:
    case CmpStmt::FCMP_FALSE:
    case CmpStmt::FCMP_TRUE:
        return IntervalValue::top(); // no useful narrowing
    case CmpStmt::ICMP_UGT:
    case CmpStmt::ICMP_SGT:
    case CmpStmt::FCMP_OGT:
    case CmpStmt::FCMP_UGT:
        result.meet_with(IntervalValue(other.lb() + 1, IntervalValue::plus_infinity()));
        break;
    case CmpStmt::ICMP_UGE:
    case CmpStmt::ICMP_SGE:
    case CmpStmt::FCMP_OGE:
    case CmpStmt::FCMP_UGE:
        result.meet_with(IntervalValue(other.lb(), IntervalValue::plus_infinity()));
        break;
    case CmpStmt::ICMP_ULT:
    case CmpStmt::ICMP_SLT:
    case CmpStmt::FCMP_OLT:
    case CmpStmt::FCMP_ULT:
        result.meet_with(IntervalValue(IntervalValue::minus_infinity(), other.ub() - 1));
        break;
    case CmpStmt::ICMP_ULE:
    case CmpStmt::ICMP_SLE:
    case CmpStmt::FCMP_OLE:
    case CmpStmt::FCMP_ULE:
        result.meet_with(IntervalValue(IntervalValue::minus_infinity(), other.ub()));
        break;
    default:
        return IntervalValue::top();
    }
    return result;
}
 
bool AbstractInterpretation::isCmpBranchEdgeFeasible(const IntraCFGEdge* edge,
        AbstractState& as)
{
    const ICFGNode* pred = edge->getSrcNode();
    s64_t succ = edge->getSuccessorCondValue();
    const CmpStmt* cmpStmt = SVFUtil::cast<CmpStmt>(
                                 *edge->getCondition()->getInEdges().begin());
    const AbstractValue& cmpValue = getAbsValue(cmpStmt->getRes(), pred);
    assert(cmpValue.isInterval() &&
           "CmpStmt result must be represented by a Boolean interval");
 
    // Feasibility check: cmp result must be compatible with branch successor
    IntervalValue resVal = cmpValue.getInterval();
    resVal.meet_with(IntervalValue((s64_t)succ, succ));
    return !resVal.isBottom();
}
 
bool AbstractInterpretation::isSwitchDefaultEdge(const IntraCFGEdge* edge) const
{
    // LLVM successor 0 is the default destination, not ICFGNode ID 0.
    // switch(x) { case 1: work(); break; } after(); -> default goes to after().
    // Explicit cases may enter the same block; this checks the destination only.
    enum : u32_t { DefaultSuccessor = 0 };
    const SVFStmt* terminator = edge->getSrcNode()->getSVFStmts().back();
    const auto* branch = SVFUtil::cast<BranchStmt>(terminator);
    return branch->getSuccessor(DefaultSuccessor) == edge->getDstNode();
}
 
bool AbstractInterpretation::isSwitchBranchEdgeFeasible(
    const IntraCFGEdge* edge, const IntervalValue& input) const
{
    if (input.isBottom())
        return false;
    else if (edge->getCondition()->getType()->getByteSize() > sizeof(s64_t))
        return true;
 
    const auto* branch = SVFUtil::cast<BranchStmt>(
                             edge->getSrcNode()->getSVFStmts().back());
    u64_t matchedCases = 0;
    for (u32_t i = 1; i < branch->getNumSuccessors(); ++i)
    {
        const s64_t caseValue = branch->getSuccessorCondValue(i);
        if (input.lb().leq(caseValue) && input.ub().geq(caseValue))
        {
            // case 1:  (input: [0,2])
            //     {block for case 1 }
            // so input can satisfy this case
            if (branch->getSuccessor(i) == edge->getDstNode())
                return true;
            ++matchedCases;
        }
    }
 
    // after last for loop, we test all non-default edge. If we reach here
    // 1)non-default edge, infeasible 2)default edge, it depends.
    if (!isSwitchDefaultEdge(edge))
        return false;
    else if (input.is_infinite())
        // default edge here
        // if input reach infinity, conservatively think it can go default edge
        return true;
    else
    {
        // default edge here
        // if we still have possible value to miss all non-default cases, it can
        // go default now.
        const u64_t span = static_cast<u64_t>(input.ub().getIntNumeral()) -
                           static_cast<u64_t>(input.lb().getIntNumeral());
        return span >= matchedCases;
    }
}
 
bool AbstractInterpretation::applyBranchRefinement(const IntraCFGEdge* edge,
        AbstractState& as)
{
    bool feasible = true;
    std::vector<std::pair<const LoadStmt*, IntervalValue>> constraints;
    // Step 1: collect Load ObjVars related to CmpStmt
    // e.g. cmp = (*p>0), we need to get var p, constant number 0, and predicate > (greater than)
    const SVFVar* cond = edge->getCondition();
    const ICFGNode* pred = edge->getSrcNode();
    s64_t succ = edge->getSuccessorCondValue();
 
    assert(!cond->getInEdges().empty() &&
           "branch condition has no defining edge?");
    const SVFStmt* condDef = *cond->getInEdges().begin();
 
    if (const CmpStmt* cmpStmt = SVFUtil::dyn_cast<CmpStmt>(condDef))
    {
        s32_t predicate = cmpStmt->getPredicate();
 
        if (cmpStmt->getOpVarID(0) == IRGraph::NullPtr ||
                cmpStmt->getOpVarID(1) == IRGraph::NullPtr)
        {
            // p == NULL / p != NULL: no interval obj to refine.
        }
        else
        {
            AbstractValue opVal[2] = {getAbsValue(cmpStmt->getOpVar(0), pred),
                                      getAbsValue(cmpStmt->getOpVar(1), pred)
                                     };
 
            const bool hasIntervalCmp =
                opVal[0].isInterval() && opVal[1].isInterval();
            if (!hasIntervalCmp && (opVal[0].isAddr() || opVal[1].isAddr()))
            {
                // Pointer-valued cmp: branch feasibility only.
            }
            else
            {
                for (int i = 0; i < 2; i++)
                {
                    const int other = 1 - i;
                    const LoadStmt* load =
                        findBackingLoad(cmpStmt->getOpVar(i));
 
                    if (opVal[i].getInterval().is_numeral())
                    {
                        // Example: in x < 5, operand 5 is not refined.
                    }
                    else if (!opVal[other].getInterval().is_numeral())
                    {
                        // Example: x < y, neither side has a fixed bound.
                    }
                    else if (!load)
                    {
                        // Example: cmp uses a computed temporary, not load p.
                    }
                    else
                    {
                        IntervalValue narrowed = computeCmpConstraint(
                                                     predicate, succ, i == 0, opVal[i].getInterval(),
                                                     opVal[other].getInterval());
 
                        if (narrowed.isTop())
                        {
                            // != and unsupported predicates reach here.
                        }
                        else
                        {
                            constraints.emplace_back(load, narrowed);
                        }
                    }
                }
            }
        }
    }
    else
    {
        if (!isSwitchBranchEdgeFeasible(edge, getAbsValue(cond, pred).getInterval()))
            return false;
        else if (isSwitchDefaultEdge(edge))
            return true;
        else
        {
            const auto* branch = SVFUtil::cast<BranchStmt>(pred->getSVFStmts().back());
            u32_t caseCount = 0;
            s64_t caseValue = 0;
            for (u32_t i = 1; i < branch->getNumSuccessors(); ++i)
            {
                if (branch->getSuccessor(i) == edge->getDstNode())
                {
                    ++caseCount;
                    caseValue = branch->getSuccessorCondValue(i);
                }
            }
 
            // case 10: A(); -> entering A requires x == 10.
            // case 10: case 20: A(); -> do not select just one value.
            // Reuse the Obj refinement below; do not modify the defining state.
            if (caseCount == 1)
            {
                if (const LoadStmt* load = findBackingLoad(cond))
                    constraints.emplace_back(load, IntervalValue(caseValue));
            }
        }
    }
 
    // Step 2: refine Obj below.
    // Example: x > 5 supplies [6,+inf]; narrowing [0,10] yields [6,10].
    // Only this temporary input changes, never the backing load's trace.
    for (const auto& [load, narrowed] : constraints)
    {
        const ICFGNode* loadICFG = load->getICFGNode();
        const AbstractValue& pointer = getAbsValue(load->getRHSVar(), loadICFG);
        if (!pointer.isAddr() || pointer.getAddrs().size() != 1)
        {
            // A condition on *p cannot refine every possible target of p.
        }
        else
        {
            const u32_t addr = *pointer.getAddrs().begin();
            const NodeID objId = as.getIDFromAddr(addr);
            if (AbstractState::isNullOrBlackHoleAddr(addr))
            {
                // No backing memory cell to refine.
            }
            else if (!as.inAddrToValTable(objId))
            {
                // Refine only an interval Obj already carried by this state.
            }
            else
            {
                IntervalValue& value = as.load(addr).getInterval();
                value.meet_with(narrowed);
                feasible &= !value.isBottom();
            }
        }
    }
    return feasible;
}
 
bool AbstractInterpretation::isBranchEdgeFeasible(const IntraCFGEdge* edge,
        AbstractState& as)
{
    const SVFVar* cmpVar = edge->getCondition();
    assert(!cmpVar->getInEdges().empty() && "branch condition has no defining edge?");
    if (SVFUtil::isa<CmpStmt>(*cmpVar->getInEdges().begin()))
        return isCmpBranchEdgeFeasible(edge, as);
    return isSwitchBranchEdgeFeasible(edge,
                                      getAbsValue(cmpVar, edge->getSrcNode()).getInterval());
}

bool AbstractInterpretation::handleICFGNode(const ICFGNode* node)
{
    // Check reachability: pre-state must have been propagated by predecessors
    bool isFunEntry = SVFUtil::isa<FunEntryICFGNode>(node);
    if (!hasAbsState(node))
    {
        if (isFunEntry)
        {
            // Entry point with no callers: inherit from global node
            const ICFGNode* globalNode = icfg->getGlobalICFGNode();
            if (hasAbsState(globalNode))
                updateAbsState(node, getAbsState(globalNode));
            else
                updateAbsState(node, AbstractState());
        }
        else
        {
            return false;  // unreachable node
        }
    }
 
    // Store the previous state for fixpoint detection
    AbstractState prevState = getAbsState(node);
 
    stat->getBlockTrace()++;
    stat->getICFGNodeTrace()++;
 
    // Handle SVF statements
    for (const SVFStmt *stmt: node->getSVFStmts())
    {
        handleSVFStatement(stmt);
    }
 
    // Handle call sites
    if (const CallICFGNode* callNode = SVFUtil::dyn_cast<CallICFGNode>(node))
    {
        handleCallSite(callNode);
    }
 
    // Run detectors
    for (auto& detector: detectors)
        detector->detect(node);
    stat->countStateSize();
 
    // Track this node as analyzed (for coverage statistics across all entry points)
    allAnalyzedNodes.insert(node);
 
    if (getAbsState(node) == prevState)
        return false;
 
    return true;
}

void AbstractInterpretation::handleFunction(const ICFGNode* funEntry, const CallICFGNode* caller)
{
    auto it = preAnalysis->getFuncToWTO().find(funEntry->getFun());
    assert(it != preAnalysis->getFuncToWTO().end() && "Missing WTO for function");
 
    // Push all top-level WTO components into the worklist in WTO order
    FIFOWorkList<const ICFGWTOComp*> worklist(it->second->getWTOComponents());
 
    while (!worklist.empty())
    {
        const ICFGWTOComp* comp = worklist.pop();
 
        if (const ICFGSingletonWTO* singleton = SVFUtil::dyn_cast<ICFGSingletonWTO>(comp))
        {
            const ICFGNode* node = singleton->getICFGNode();
            if (mergeStatesFromPredecessors(node))
                handleICFGNode(node);
        }
        else if (const ICFGCycleWTO* cycle = SVFUtil::dyn_cast<ICFGCycleWTO>(comp))
        {
            if (mergeStatesFromPredecessors(cycle->head()->getICFGNode()))
                handleLoopOrRecursion(cycle, caller);
        }
    }
}
 
 
void AbstractInterpretation::handleCallSite(const ICFGNode* node)
{
    if (const CallICFGNode* callNode = SVFUtil::dyn_cast<CallICFGNode>(node))
    {
        if (isExtCall(callNode))
        {
            handleExtCall(callNode);
        }
        else
        {
            // Handle both direct and indirect calls uniformly
            handleFunCall(callNode);
        }
    }
    else
        assert (false && "it is not call node");
}
 
bool AbstractInterpretation::isExtCall(const CallICFGNode *callNode)
{
    return SVFUtil::isExtCall(callNode->getCalledFunction());
}
 
void AbstractInterpretation::handleExtCall(const CallICFGNode *callNode)
{
    utils->handleExtAPI(callNode);
    for (auto& detector : detectors)
    {
        detector->handleStubFunctions(callNode);
    }
}

const FunObjVar* AbstractInterpretation::getCallee(const CallICFGNode* callNode)
{
    // Direct call: get callee directly from call node
    if (const FunObjVar* callee = callNode->getCalledFunction())
        return callee;
 
    // Indirect call: resolve callee through pointer analysis
    const auto callsiteMaps = svfir->getIndirectCallsites();
    auto it = callsiteMaps.find(callNode);
    if (it == callsiteMaps.end())
        return nullptr;
 
    NodeID call_id = it->second;
    if (!hasAbsState(callNode))
        return nullptr;
 
    const AbstractValue& Addrs = getAbsValue(svfir->getSVFVar(call_id), callNode);
    if (!Addrs.isAddr() || Addrs.getAddrs().empty())
        return nullptr;
 
    NodeID addr = *Addrs.getAddrs().begin();
    const SVFVar* func_var = getSVFVar(getAbsState(callNode).getIDFromAddr(addr));
    return SVFUtil::dyn_cast<FunObjVar>(func_var);
}

void AbstractInterpretation::handleFunCall(const CallICFGNode *callNode)
{
    if (skipRecursiveCall(callNode))
        return;
 
    // Direct call: callee is known
    if (const FunObjVar* callee = callNode->getCalledFunction())
    {
        const ICFGNode* calleeEntry = icfg->getFunEntryICFGNode(callee);
        handleFunction(calleeEntry, callNode);
        const RetICFGNode* retNode = callNode->getRetICFGNode();
        updateAbsState(retNode, getAbsState(callNode));
        return;
    }
 
    // Indirect call: use Andersen's call graph to get all resolved callees.
    const RetICFGNode* retNode = callNode->getRetICFGNode();
    if (callGraph->hasIndCSCallees(callNode))
    {
        const auto& callees = callGraph->getIndCSCallees(callNode);
        for (const FunObjVar* callee : callees)
        {
            if (callee->isDeclaration())
                continue;
            const ICFGNode* calleeEntry = icfg->getFunEntryICFGNode(callee);
            handleFunction(calleeEntry, callNode);
        }
    }
    // Resume return node from caller's state (context-insensitive)
    updateAbsState(retNode, getAbsState(callNode));
}
 
// Loop / recursion handling (handleLoopOrRecursion + cycle helpers +
// recursion utilities) lives in AELoopRecursion.cpp.
 
void AbstractInterpretation::handleSVFStatement(const SVFStmt *stmt)
{
    if (const AddrStmt *addr = SVFUtil::dyn_cast<AddrStmt>(stmt))
    {
        updateStateOnAddr(addr);
    }
    else if (const BinaryOPStmt *binary = SVFUtil::dyn_cast<BinaryOPStmt>(stmt))
    {
        updateStateOnBinary(binary);
    }
    else if (const CmpStmt *cmp = SVFUtil::dyn_cast<CmpStmt>(stmt))
    {
        updateStateOnCmp(cmp);
    }
    else if (SVFUtil::isa<UnaryOPStmt>(stmt))
    {
    }
    else if (SVFUtil::isa<BranchStmt>(stmt))
    {
        // branch stmt is handled in hasBranchES
    }
    else if (const LoadStmt *load = SVFUtil::dyn_cast<LoadStmt>(stmt))
    {
        updateStateOnLoad(load);
    }
    else if (const StoreStmt *store = SVFUtil::dyn_cast<StoreStmt>(stmt))
    {
        updateStateOnStore(store);
    }
    else if (const CopyStmt *copy = SVFUtil::dyn_cast<CopyStmt>(stmt))
    {
        updateStateOnCopy(copy);
    }
    else if (const GepStmt *gep = SVFUtil::dyn_cast<GepStmt>(stmt))
    {
        updateStateOnGep(gep);
    }
    else if (const SelectStmt *select = SVFUtil::dyn_cast<SelectStmt>(stmt))
    {
        updateStateOnSelect(select);
    }
    else if (const PhiStmt *phi = SVFUtil::dyn_cast<PhiStmt>(stmt))
    {
        updateStateOnPhi(phi);
    }
    else if (const CallPE *callPE = SVFUtil::dyn_cast<CallPE>(stmt))
    {
        // To handle Call Edge
        updateStateOnCall(callPE);
    }
    else if (const RetPE *retPE = SVFUtil::dyn_cast<RetPE>(stmt))
    {
        updateStateOnRet(retPE);
    }
    else
        assert(false && "implement this part");
    // NullPtr should not be changed by any statement. If the entry is missing
    // (not yet auto-inserted) we treat that as "unchanged" — only check the
    // entry if it actually exists.
    {
        const auto& vmap = getAbsState(stmt->getICFGNode()).getVarToVal();
        auto it = vmap.find(IRGraph::NullPtr);
        (void)it; // Suppress warning of unused variable under release build
        assert(it == vmap.end() ||
               (it->second.isAddr() &&
                it->second.getAddrs().equals(AddressValue(NullMemAddr))));
    }
}
 
void AbstractInterpretation::updateStateOnGep(const GepStmt *gep)
{
    const ICFGNode* node = gep->getICFGNode();
    IntervalValue offsetPair = getGepElementIndex(gep);
    AddressValue gepAddrs = getGepObjAddrs(SVFUtil::cast<ValVar>(gep->getRHSVar()), offsetPair);
    updateAbsValue(gep->getLHSVar(), gepAddrs, node);
}
 
void AbstractInterpretation::updateStateOnSelect(const SelectStmt *select)
{
    const ICFGNode* node = select->getICFGNode();
    const AbstractValue& condVal = getAbsValue(select->getCondition(), node);
    const AbstractValue& tVal = getAbsValue(select->getTrueValue(), node);
    const AbstractValue& fVal = getAbsValue(select->getFalseValue(), node);
    AbstractValue resVal;
    if (condVal.getInterval().is_numeral())
    {
        resVal = condVal.getInterval().is_zero() ? fVal : tVal;
    }
    else
    {
        resVal = tVal;
        resVal.join_with(fVal);
    }
    updateAbsValue(select->getRes(), resVal, node);
}
 
void AbstractInterpretation::updateStateOnPhi(const PhiStmt *phi)
{
    const ICFGNode* icfgNode = phi->getICFGNode();
    AbstractValue rhs;
    for (u32_t i = 0; i < phi->getOpVarNum(); i++)
    {
        const ICFGNode* opICFGNode = phi->getOpICFGNode(i);
        if (hasAbsState(opICFGNode))
        {
            AbstractState tmpState = getAbsState(opICFGNode);
            const AbstractValue& opVal = getAbsValue(phi->getOpVar(i), opICFGNode);
            const ICFGEdge* edge = icfg->getICFGEdge(opICFGNode, icfgNode, ICFGEdge::IntraCF);
            if (edge)
            {
                const IntraCFGEdge* intraEdge = SVFUtil::cast<IntraCFGEdge>(edge);
                if (intraEdge->getCondition())
                {
                    if (isBranchEdgeFeasible(intraEdge, tmpState))
                        rhs.join_with(opVal);
                }
                else
                    rhs.join_with(opVal);
            }
            else
            {
                rhs.join_with(opVal);
            }
        }
    }
    updateAbsValue(phi->getRes(), rhs, icfgNode);
}
 

void AbstractInterpretation::updateStateOnCall(const CallPE *callPE)
{
    const ICFGNode* node = callPE->getICFGNode();
    const SVFVar* res = callPE->getRes();
    AbstractValue rhs;
    for (u32_t i = 0; i < callPE->getOpVarNum(); i++)
    {
        const ICFGNode* opICFGNode = callPE->getOpCallICFGNode(i);
        if (hasAbsState(opICFGNode))
        {
            const AbstractValue& opVal = getAbsValue(callPE->getOpVar(i), opICFGNode);
            rhs.join_with(opVal);
        }
    }
    updateAbsValue(res, rhs, node);
}
 
void AbstractInterpretation::updateStateOnRet(const RetPE *retPE)
{
    const ICFGNode* node = retPE->getICFGNode();
    const AbstractValue& rhsVal = getAbsValue(retPE->getRHSVar(), node);
    updateAbsValue(retPE->getLHSVar(), rhsVal, node);
}
 
 
void AbstractInterpretation::updateStateOnAddr(const AddrStmt *addr)
{
    const ICFGNode* node = addr->getICFGNode();
    // initObjVar mutates _varToAbsVal/_addrToAbsVal directly, so we need
    // mutable access; route via the manager.
    AbstractState& as = getAbsState(node);
    as.initObjVar(SVFUtil::cast<ObjVar>(addr->getRHSVar()));
    // AddrStmt: lhs(ValVar) = &rhs(ObjVar).
    // as[rhsId] stores the ObjVar's virtual address in _varToVal,
    // NOT the object contents. So we must use as[] directly for ObjVar.
    u32_t rhsId = addr->getRHSVarID();
    if (addr->getRHSVar()->getType()->getKind() == SVFType::SVFIntegerTy)
        as[rhsId].getInterval().meet_with(utils->getRangeLimitFromType(addr->getRHSVar()->getType()));
    // LHS is a ValVar (pointer), write through the API
    updateAbsValue(addr->getLHSVar(), as[rhsId], node);
}
 
 
void AbstractInterpretation::updateStateOnBinary(const BinaryOPStmt *binary)
{
    const ICFGNode* node = binary->getICFGNode();
    // Treat bottom (uninitialized) operands as top for soundness
    const AbstractValue& op0Val = getAbsValue(binary->getOpVar(0), node);
    const AbstractValue& op1Val = getAbsValue(binary->getOpVar(1), node);
    IntervalValue lhs = op0Val.getInterval().isBottom() ? IntervalValue::top() : op0Val.getInterval();
    IntervalValue rhs = op1Val.getInterval().isBottom() ? IntervalValue::top() : op1Val.getInterval();
    IntervalValue resVal;
    switch (binary->getOpcode())
    {
    case BinaryOPStmt::Add:
    case BinaryOPStmt::FAdd:
        resVal = (lhs + rhs);
        break;
    case BinaryOPStmt::Sub:
    case BinaryOPStmt::FSub:
        resVal = (lhs - rhs);
        break;
    case BinaryOPStmt::Mul:
    case BinaryOPStmt::FMul:
        resVal = (lhs * rhs);
        break;
    case BinaryOPStmt::SDiv:
    case BinaryOPStmt::FDiv:
    case BinaryOPStmt::UDiv:
        resVal = (lhs / rhs);
        break;
    case BinaryOPStmt::SRem:
    case BinaryOPStmt::FRem:
    case BinaryOPStmt::URem:
        resVal = (lhs % rhs);
        break;
    case BinaryOPStmt::Xor:
        resVal = (lhs ^ rhs);
        break;
    case BinaryOPStmt::And:
        resVal = (lhs & rhs);
        break;
    case BinaryOPStmt::Or:
        resVal = (lhs | rhs);
        break;
    case BinaryOPStmt::AShr:
        resVal = (lhs >> rhs);
        break;
    case BinaryOPStmt::Shl:
        resVal = (lhs << rhs);
        break;
    case BinaryOPStmt::LShr:
        resVal = (lhs >> rhs);
        break;
    default:
        assert(false && "undefined binary: ");
    }
    updateAbsValue(binary->getRes(), resVal, node);
}

IntervalValue AbstractInterpretation::evaluatePointerCmp(
    u32_t predicate, const AddressValue& lhs, const AddressValue& rhs) const
{
    assert(predicate >= CmpStmt::FIRST_ICMP_PREDICATE &&
           predicate <= CmpStmt::LAST_ICMP_PREDICATE &&
           "pointer comparison must use an ICMP predicate");
 
    const bool lhsTargetKnown =
        !lhs.isBottom() && !lhs.contains(BlackHoleObjAddr);
    const bool rhsTargetKnown =
        !rhs.isBottom() && !rhs.contains(BlackHoleObjAddr);
    const bool hasUnknownTarget = !lhsTargetKnown || !rhsTargetKnown;
    const bool targetsMayBeEqual = lhs.hasIntersect(rhs);
    const bool targetsMustBeEqual =
        targetsMayBeEqual && lhs.size() == 1 && rhs.size() == 1;
 
    IntervalValue equality;
    if (hasUnknownTarget)
    {
        // Case 1: an unknown target may equal or differ from the other target.
        equality = IntervalValue((s64_t)0, (s64_t)1);
    }
    else if (!targetsMayBeEqual)
    {
        // Case 2: known disjoint target sets are definitely unequal.
        equality = IntervalValue((s64_t)0);
    }
    else if (targetsMustBeEqual)
    {
        // Case 3: intersecting single-target sets contain the same target.
        equality = IntervalValue((s64_t)1);
    }
    else
    {
        // Case 4: intersecting sets with multiple choices may be equal.
        equality = IntervalValue((s64_t)0, (s64_t)1);
    }
 
    IntervalValue result((s64_t)0, (s64_t)1);
    if (predicate == CmpStmt::ICMP_EQ)
        result = equality;
    else if (predicate == CmpStmt::ICMP_NE)
        result = IntervalValue((s64_t)1) - equality;
    return result;
}
 
IntervalValue AbstractInterpretation::evaluateIntervalCmp(
    u32_t predicate, const IntervalValue& lhs, const IntervalValue& rhs) const
{
    IntervalValue result = IntervalValue::top();
    switch (predicate)
    {
    case CmpStmt::ICMP_EQ:
    case CmpStmt::FCMP_OEQ:
    case CmpStmt::FCMP_UEQ:
        result = (lhs == rhs);
        break;
    case CmpStmt::ICMP_NE:
    case CmpStmt::FCMP_ONE:
    case CmpStmt::FCMP_UNE:
        result = (lhs != rhs);
        break;
    case CmpStmt::ICMP_UGT:
    case CmpStmt::ICMP_SGT:
    case CmpStmt::FCMP_OGT:
    case CmpStmt::FCMP_UGT:
        result = (lhs > rhs);
        break;
    case CmpStmt::ICMP_UGE:
    case CmpStmt::ICMP_SGE:
    case CmpStmt::FCMP_OGE:
    case CmpStmt::FCMP_UGE:
        result = (lhs >= rhs);
        break;
    case CmpStmt::ICMP_ULT:
    case CmpStmt::ICMP_SLT:
    case CmpStmt::FCMP_OLT:
    case CmpStmt::FCMP_ULT:
        result = (lhs < rhs);
        break;
    case CmpStmt::ICMP_ULE:
    case CmpStmt::ICMP_SLE:
    case CmpStmt::FCMP_OLE:
    case CmpStmt::FCMP_ULE:
        result = (lhs <= rhs);
        break;
    case CmpStmt::FCMP_FALSE:
        result = IntervalValue(0, 0);
        break;
    case CmpStmt::FCMP_TRUE:
        result = IntervalValue(1, 1);
        break;
    case CmpStmt::FCMP_ORD:
    case CmpStmt::FCMP_UNO:
        // Keep both outcomes because the interval domain does not track NaN.
        result = IntervalValue(0, 1);
        break;
    default:
        assert(false && "undefined compare: ");
    }
    return result;
}
 
void AbstractInterpretation::updateStateOnCmp(const CmpStmt *cmp)
{
    const ICFGNode* node = cmp->getICFGNode();
    const AbstractValue& lhsValue = getAbsValue(cmp->getOpVar(0), node);
    const AbstractValue& rhsValue = getAbsValue(cmp->getOpVar(1), node);
    const bool pointerCmp = cmp->getOpVar(0)->getType()->isPointerTy();
    assert(pointerCmp == cmp->getOpVar(1)->getType()->isPointerTy() &&
           "CmpStmt operands must belong to the same value domain");
 
    IntervalValue result;
    if (pointerCmp)
    {
        result = evaluatePointerCmp(cmp->getPredicate(), lhsValue.getAddrs(),
                                    rhsValue.getAddrs());
    }
    else
    {
        const IntervalValue lhs = lhsValue.isInterval()
                                  ? lhsValue.getInterval()
                                  : IntervalValue::top();
        const IntervalValue rhs = rhsValue.isInterval()
                                  ? rhsValue.getInterval()
                                  : IntervalValue::top();
        result = evaluateIntervalCmp(cmp->getPredicate(), lhs, rhs);
    }
    updateAbsValue(cmp->getRes(), result, node);
}
 
void AbstractInterpretation::updateStateOnLoad(const LoadStmt *load)
{
    const ICFGNode* node = load->getICFGNode();
    AbstractValue loaded =
        loadValue(SVFUtil::cast<ValVar>(load->getRHSVar()), node);
    updateAbsValue(load->getLHSVar(), loaded, node);
}
 
void AbstractInterpretation::updateStateOnStore(const StoreStmt *store)
{
    const ICFGNode* node = store->getICFGNode();
    AbstractValue val = getAbsValue(store->getRHSVar(), node);
    storeValue(SVFUtil::cast<ValVar>(store->getLHSVar()), val, node);
}
 
void AbstractInterpretation::updateStateOnCopy(const CopyStmt *copy)
{
    const ICFGNode* node = copy->getICFGNode();
    const SVFVar* lhsVar = copy->getLHSVar();
    const SVFVar* rhsVar = copy->getRHSVar();
 
    auto getZExtValue = [&](const SVFVar* var)
    {
        const SVFType* type = var->getType();
        if (SVFUtil::isa<SVFIntegerType>(type))
        {
            u32_t bits = type->getByteSize() * 8;
            const AbstractValue& val = getAbsValue(var, node);
            if (val.getInterval().is_numeral())
            {
                if (bits == 8)
                {
                    int8_t signed_i8_value = val.getInterval().getIntNumeral();
                    u32_t unsigned_value = static_cast<uint8_t>(signed_i8_value);
                    return IntervalValue(unsigned_value, unsigned_value);
                }
                else if (bits == 16)
                {
                    s16_t signed_i16_value = val.getInterval().getIntNumeral();
                    u32_t unsigned_value = static_cast<u16_t>(signed_i16_value);
                    return IntervalValue(unsigned_value, unsigned_value);
                }
                else if (bits == 32)
                {
                    s32_t signed_i32_value = val.getInterval().getIntNumeral();
                    u32_t unsigned_value = static_cast<u32_t>(signed_i32_value);
                    return IntervalValue(unsigned_value, unsigned_value);
                }
                else if (bits == 64)
                {
                    s64_t signed_i64_value = val.getInterval().getIntNumeral();
                    return IntervalValue((s64_t)signed_i64_value, (s64_t)signed_i64_value);
                }
                else
                    assert(false && "cannot support int type other than u8/16/32/64");
            }
            else
            {
                return IntervalValue::top();
            }
        }
        return IntervalValue::top();
    };
 
    auto getTruncValue = [&](const SVFVar* var, const SVFType* dstType)
    {
        const IntervalValue& itv = getAbsValue(var, node).getInterval();
        if(itv.isBottom()) return itv;
        s64_t int_lb = itv.lb().getIntNumeral();
        s64_t int_ub = itv.ub().getIntNumeral();
        u32_t dst_bits = dstType->getByteSize() * 8;
        if (dst_bits == 8)
        {
            int8_t s8_lb = static_cast<int8_t>(int_lb);
            int8_t s8_ub = static_cast<int8_t>(int_ub);
            if (s8_lb > s8_ub)
                return utils->getRangeLimitFromType(dstType);
            return IntervalValue(s8_lb, s8_ub);
        }
        else if (dst_bits == 16)
        {
            s16_t s16_lb = static_cast<s16_t>(int_lb);
            s16_t s16_ub = static_cast<s16_t>(int_ub);
            if (s16_lb > s16_ub)
                return utils->getRangeLimitFromType(dstType);
            return IntervalValue(s16_lb, s16_ub);
        }
        else if (dst_bits == 32)
        {
            s32_t s32_lb = static_cast<s32_t>(int_lb);
            s32_t s32_ub = static_cast<s32_t>(int_ub);
            if (s32_lb > s32_ub)
                return utils->getRangeLimitFromType(dstType);
            return IntervalValue(s32_lb, s32_ub);
        }
        else
        {
            assert(false && "cannot support dst int type other than u8/16/32");
            abort();
        }
    };
 
    const AbstractValue& rhsVal = getAbsValue(rhsVar, node);
 
    if (copy->getCopyKind() == CopyStmt::COPYVAL)
    {
        updateAbsValue(lhsVar, rhsVal, node);
    }
    else if (copy->getCopyKind() == CopyStmt::ZEXT)
    {
        updateAbsValue(lhsVar, getZExtValue(rhsVar), node);
    }
    else if (copy->getCopyKind() == CopyStmt::SEXT)
    {
        updateAbsValue(lhsVar, rhsVal.getInterval(), node);
    }
    else if (copy->getCopyKind() == CopyStmt::FPTOSI)
    {
        updateAbsValue(lhsVar, rhsVal.getInterval(), node);
    }
    else if (copy->getCopyKind() == CopyStmt::FPTOUI)
    {
        updateAbsValue(lhsVar, rhsVal.getInterval(), node);
    }
    else if (copy->getCopyKind() == CopyStmt::SITOFP)
    {
        updateAbsValue(lhsVar, rhsVal.getInterval(), node);
    }
    else if (copy->getCopyKind() == CopyStmt::UITOFP)
    {
        updateAbsValue(lhsVar, rhsVal.getInterval(), node);
    }
    else if (copy->getCopyKind() == CopyStmt::TRUNC)
    {
        updateAbsValue(lhsVar, getTruncValue(rhsVar, lhsVar->getType()), node);
    }
    else if (copy->getCopyKind() == CopyStmt::FPTRUNC)
    {
        updateAbsValue(lhsVar, rhsVal.getInterval(), node);
    }
    else if (copy->getCopyKind() == CopyStmt::INTTOPTR)
    {
        //insert nullptr
    }
    else if (copy->getCopyKind() == CopyStmt::PTRTOINT)
    {
        updateAbsValue(lhsVar, IntervalValue::top(), node);
    }
    else if (copy->getCopyKind() == CopyStmt::BITCAST)
    {
        if (rhsVal.isAddr())
            updateAbsValue(lhsVar, rhsVal, node);
    }
    else
        assert(false && "undefined copy kind");
}