SVF::MTAResultValidator Class Reference

#include <MTAResultValidator.h>

Public Types
typedef int	INTERLEV_FLAG
typedef int	INTERLEV_FLAG

Public Member Functions
	MTAResultValidator (MHP *mh)
	~MTAResultValidator ()
void	analyze ()
SVFModule *	getModule () const
	MTAResultValidator (MHP *mh)
	~MTAResultValidator ()
void	analyze ()
SVFModule *	getModule () const

Protected Member Functions
std::vector< std::string > &	split (const std::string &s, char delim, std::vector< std::string > &elems)
std::vector< std::string >	split (const std::string &s, char delim)
NodeID	getIntArg (const Instruction *inst, unsigned int arg_num)
std::vector< std::string >	getStringArg (const Instruction *inst, unsigned int arg_num)
CallStrCxt	getCxtArg (const Instruction *inst, unsigned int arg_num)
const Instruction *	getPreviousMemoryAccessInst (const Instruction *I)
bool	matchCxt (const CallStrCxt cxt1, const CallStrCxt cxt2) const
void	dumpCxt (const CallStrCxt &cxt) const
void	dumpInterlev (NodeBS &lev)
std::string	getOutput (const char *scenario, bool analysisRes)
std::string	getOutputforInterlevAnalysis (const char *scenario, INTERLEV_FLAG analysisRes)
bool	collectCallsiteTargets ()
bool	collectCxtThreadTargets ()
bool	collectTCTTargets ()
bool	collectInterleavingTargets ()
bool	validateCxtThread ()
bool	validateTCT ()
INTERLEV_FLAG	validateInterleaving ()
std::vector< std::string > &	split (const std::string &s, char delim, std::vector< std::string > &elems)
std::vector< std::string >	split (const std::string &s, char delim)
NodeID	getIntArg (const Instruction *inst, unsigned int arg_num)
std::vector< std::string >	getStringArg (const Instruction *inst, unsigned int arg_num)
CallStrCxt	getCxtArg (const Instruction *inst, unsigned int arg_num)
const Instruction *	getPreviousMemoryAccessInst (const Instruction *I)
bool	matchCxt (const CallStrCxt cxt1, const CallStrCxt cxt2) const
void	dumpCxt (const CallStrCxt &cxt) const
void	dumpInterlev (NodeBS &lev)
std::string	getOutput (const char *scenario, bool analysisRes)
std::string	getOutputforInterlevAnalysis (const char *scenario, INTERLEV_FLAG analysisRes)
bool	collectCallsiteTargets ()
bool	collectCxtThreadTargets ()
bool	collectTCTTargets ()
bool	collectInterleavingTargets ()
bool	validateCxtThread ()
bool	validateTCT ()
INTERLEV_FLAG	validateInterleaving ()

Private Types
typedef Map< NodeID, const SVFInstruction * >	csnumToInst
typedef Map< NodeID, CallStrCxt >	vthdToCxtMap
typedef Map< NodeID, NodeID >	vthdTorthdMap
typedef Map< NodeID, NodeID >	rthdTovthdMap
typedef Map< NodeID, Set< NodeID > >	rthdToChildrenMap
typedef Map< NodeID, const SVFInstruction * >	csnumToInst
typedef Map< NodeID, CallStrCxt >	vthdToCxtMap
typedef Map< NodeID, NodeID >	vthdTorthdMap
typedef Map< NodeID, NodeID >	rthdTovthdMap
typedef Map< NodeID, Set< NodeID > >	rthdToChildrenMap

Private Attributes
MHP::InstToThreadStmtSetMap	instToTSMap
MHP::ThreadStmtToThreadInterleav	threadStmtToInterLeaving
ThreadAPI *	tdAPI
ThreadCallGraph *	tcg
MHP *	mhp
vthdToCxtMap	vthdToCxt
vthdTorthdMap	vthdTorthd
rthdTovthdMap	rthdTovthd
csnumToInst	csnumToInstMap
rthdToChildrenMap	rthdToChildren
SVFModule *	mod

Static Private Attributes
static constexpr char const *	CXT_THREAD = "CXT_THREAD"
	Map a statement to its thread interleavings. More...
static constexpr char const *	INTERLEV_ACCESS = "INTERLEV_ACCESS"
static constexpr char const *	TCT_ACCESS = "TCT_ACCESS"
static const INTERLEV_FLAG	INTERLEV_TRUE = 0x01
	Constant INTERLEV_FLAG values. More...
static const INTERLEV_FLAG	INTERLEV_IMPRECISE = 0x02
static const INTERLEV_FLAG	INTERLEV_UNSOUND = 0x04

Detailed Description

Definition at line 22 of file MTAResultValidator.h.

Member Typedef Documentation

csnumToInst [1/2]

typedef Map<NodeID, const SVFInstruction*> SVF::MTAResultValidator::csnumToInst

private

Definition at line 121 of file MTAResultValidator.h.

csnumToInst [2/2]

typedef Map<NodeID, const SVFInstruction*> SVF::MTAResultValidator::csnumToInst

private

Definition at line 120 of file MTAResultValidator.h.

INTERLEV_FLAG [1/2]

typedef int SVF::MTAResultValidator::INTERLEV_FLAG

Definition at line 26 of file MTAResultValidator.h.

INTERLEV_FLAG [2/2]

typedef int SVF::MTAResultValidator::INTERLEV_FLAG

Definition at line 25 of file MTAResultValidator.h.

rthdToChildrenMap [1/2]

typedef Map<NodeID, Set<NodeID> > SVF::MTAResultValidator::rthdToChildrenMap

private

Definition at line 126 of file MTAResultValidator.h.

rthdToChildrenMap [2/2]

typedef Map<NodeID, Set<NodeID> > SVF::MTAResultValidator::rthdToChildrenMap

private

Definition at line 125 of file MTAResultValidator.h.

rthdTovthdMap [1/2]

typedef Map<NodeID, NodeID> SVF::MTAResultValidator::rthdTovthdMap

private

Definition at line 124 of file MTAResultValidator.h.

rthdTovthdMap [2/2]

typedef Map<NodeID, NodeID> SVF::MTAResultValidator::rthdTovthdMap

private

Definition at line 123 of file MTAResultValidator.h.

vthdToCxtMap [1/2]

typedef Map<NodeID, CallStrCxt> SVF::MTAResultValidator::vthdToCxtMap

private

Definition at line 122 of file MTAResultValidator.h.

vthdToCxtMap [2/2]

typedef Map<NodeID, CallStrCxt> SVF::MTAResultValidator::vthdToCxtMap

private

Definition at line 121 of file MTAResultValidator.h.

vthdTorthdMap [1/2]

typedef Map<NodeID, NodeID> SVF::MTAResultValidator::vthdTorthdMap

private

Definition at line 123 of file MTAResultValidator.h.

vthdTorthdMap [2/2]

typedef Map<NodeID, NodeID> SVF::MTAResultValidator::vthdTorthdMap

private

Definition at line 122 of file MTAResultValidator.h.

Constructor & Destructor Documentation

MTAResultValidator() [1/2]

SVF::MTAResultValidator::MTAResultValidator ( MHP *  mh )

inline

Definition at line 27 of file MTAResultValidator.h.

                                :
        mhp(mh)
    {
        tcg = mhp->getThreadCallGraph();
        tdAPI = tcg->getThreadAPI();
        mod = mhp->getTCT()->getSVFModule();
    }

~MTAResultValidator() [1/2]

SVF::MTAResultValidator::~MTAResultValidator ( )

inline

Definition at line 35 of file MTAResultValidator.h.

    {
    }

MTAResultValidator() [2/2]

SVF::MTAResultValidator::MTAResultValidator ( MHP *  mh )

inline

Definition at line 26 of file MTAResultValidator.h.

                                :
        mhp(mh)
    {
        tcg = mhp->getThreadCallGraph();
        tdAPI = tcg->getThreadAPI();
        mod = mhp->getTCT()->getSVFModule();
    }

~MTAResultValidator() [2/2]

SVF::MTAResultValidator::~MTAResultValidator ( )

inline

Definition at line 34 of file MTAResultValidator.h.

    {
    }

Member Function Documentation

analyze() [1/2]

void MTAResultValidator::analyze

(

)

Definition at line 40 of file MTAResultValidator.cpp.

{
 
    // Initialize the validator and perform validation.
    MHPValidator validator(mhp);
    validator.init(mhp->getTCT()->getSVFModule());
    validator.analyze();
 
 
    std::string errstring;
    if (!collectCallsiteTargets())
        return;
    if (!collectCxtThreadTargets())
        return;
 
    errstring = getOutput("Validate CxtThread:", validateCxtThread());
    outs() << "======" << errstring << "======\n";
 
    if (!collectTCTTargets())
        return;
    errstring = getOutput("Validate TCT:     ", validateTCT());
    outs() << "======" << errstring << "======\n";
 
    if (!collectInterleavingTargets())
        return;
    errstring = getOutputforInterlevAnalysis("Validate Interleaving:", validateInterleaving());
    outs() << "======" << errstring << "======\n";
}

analyze() [2/2]

void SVF::MTAResultValidator::analyze

(

)

collectCallsiteTargets() [1/2]

bool MTAResultValidator::collectCallsiteTargets ( )

protected

Definition at line 215 of file MTAResultValidator.cpp.

{
    for (Module& M : LLVMModuleSet::getLLVMModuleSet()->getLLVMModules())
    {
        for (Module::const_iterator F = M.begin(), E = M.end(); F != E; ++F)
        {
            for (Function::const_iterator bi = (*F).begin(), ebi = (*F).end(); bi != ebi; ++bi)
            {
                const BasicBlock* bb = &*bi;
                if (!bb->getName().str().compare(0, 2, "cs"))
                {
                    NodeID csnum = atoi(bb->getName().str().substr(2).c_str());
                    const Instruction* inst = &bb->front();
                    while (1)
                    {
                        if (SVFUtil::isa<CallInst>(inst))
                        {
                            break;
                        }
                        inst = inst->getNextNode();
                        assert(inst && "Wrong cs label, cannot find callsite");
                    }
                    const SVFInstruction* svfInst = LLVMModuleSet::getLLVMModuleSet()->getSVFInstruction(inst);
                    csnumToInstMap[csnum] = svfInst;
                }
            }
        }
    }
    return !csnumToInstMap.empty();
}

collectCallsiteTargets() [2/2]

bool SVF::MTAResultValidator::collectCallsiteTargets ( )

protected

collectCxtThreadTargets() [1/2]

bool MTAResultValidator::collectCxtThreadTargets ( )

protected

Definition at line 246 of file MTAResultValidator.cpp.

{
    const Function* F = nullptr;
    for (Module &M : LLVMModuleSet::getLLVMModuleSet()->getLLVMModules())
    {
        for(auto it = M.begin(); it != M.end(); it++)
        {
            const std::string fName = (*it).getName().str();
            if(fName.find(CXT_THREAD) != std::string::npos)
            {
                F = &(*it);
                break;
            }
        }
    }
    if (!F)
        return false;
 
    // Push main thread into vthdToCxt;
    CallStrCxt main_cxt;
    vthdToCxt[0] = main_cxt;
 
    // Collect call sites of all CXT_THREAD function calls.
 
    for (Value::const_use_iterator it = F->use_begin(), ie = F->use_end(); it != ie; ++it)
    {
        const Use *u = &*it;
        const Value* user = u->getUser();
        const Instruction* inst = SVFUtil::dyn_cast<Instruction>(user);
 
        NodeID vthdnum = getIntArg(inst, 0);
        CallStrCxt cxt = getCxtArg(inst, 1);
 
        vthdToCxt[vthdnum] = cxt;
    }
    return true;
}

collectCxtThreadTargets() [2/2]

bool SVF::MTAResultValidator::collectCxtThreadTargets ( )

protected

collectInterleavingTargets() [1/2]

bool MTAResultValidator::collectInterleavingTargets ( )

protected

Definition at line 322 of file MTAResultValidator.cpp.

{
 
    // Collect call sites of all INTERLEV_ACCESS function calls.
    const Function* F = nullptr;
    for (Module &M : LLVMModuleSet::getLLVMModuleSet()->getLLVMModules())
    {
        for(auto it = M.begin(); it != M.end(); it++)
        {
            const std::string fName = (*it).getName().str();
            if(fName.find(INTERLEV_ACCESS) != std::string::npos)
            {
                F = &(*it);
                break;
            }
        }
    }
    if (!F)
        return false;
 
    for (Value::const_use_iterator it = F->use_begin(), ie = F->use_end(); it != ie; ++it)
    {
        const Use *u = &*it;
        const Value* user = u->getUser();
        const Instruction* inst = SVFUtil::dyn_cast<Instruction>(user);
 
        NodeID vthdnum = getIntArg(inst, 0);
        NodeID rthdnum = vthdTorthd[vthdnum];
        CallStrCxt x = getCxtArg(inst, 1);
        std::vector<std::string> y = getStringArg(inst, 2);
 
        // Record given interleaving
        NodeBS lev;
        // Push thread itself into interleaving set
        lev.set(rthdnum);
        // Find rthd of given vthd and push it into interleaving set
        for (std::vector<std::string>::iterator i = y.begin(); i != y.end(); i++)
        {
            lev.set(vthdTorthd[atoi((*i).c_str())]);
        }
 
        const Instruction* memInst = getPreviousMemoryAccessInst(inst);
        const SVFInstruction* svfMemInst = LLVMModuleSet::getLLVMModuleSet()->getSVFInstruction(memInst);
        CxtThreadStmt cts(rthdnum, x, svfMemInst);
        instToTSMap[svfMemInst].insert(cts);
        threadStmtToInterLeaving[cts] = lev;
    }
    return true;
}

collectInterleavingTargets() [2/2]

bool SVF::MTAResultValidator::collectInterleavingTargets ( )

protected

collectTCTTargets() [1/2]

bool MTAResultValidator::collectTCTTargets ( )

protected

Definition at line 284 of file MTAResultValidator.cpp.

{
 
    // Collect call sites of all TCT_ACCESS function calls.
    const Function* F = nullptr;
    for (Module &M : LLVMModuleSet::getLLVMModuleSet()->getLLVMModules())
    {
        for(auto it = M.begin(); it != M.end(); it++)
        {
            const std::string fName = (*it).getName().str();
            if(fName.find(TCT_ACCESS) != std::string::npos)
            {
                F = &(*it);
                break;
            }
        }
    }
    if (!F)
        return false;
 
    for (Value::const_use_iterator it = F->use_begin(), ie = F->use_end(); it != ie; ++it)
    {
        const Use *u = &*it;
        const Value* user = u->getUser();
        const Instruction* inst = SVFUtil::dyn_cast<Instruction>(user);
 
        NodeID vthdnum = getIntArg(inst, 0);
        NodeID rthdnum = vthdTorthd[vthdnum];
        std::vector<std::string> x = getStringArg(inst, 1);
 
        for (std::vector<std::string>::iterator i = x.begin(); i != x.end(); i++)
        {
            rthdToChildren[rthdnum].insert(vthdTorthd[atoi((*i).c_str())]);
        }
    }
    return true;
}

collectTCTTargets() [2/2]

bool SVF::MTAResultValidator::collectTCTTargets ( )

protected

dumpCxt() [1/2]

void MTAResultValidator::dumpCxt ( const CallStrCxt &  cxt ) const

protected

Definition at line 189 of file MTAResultValidator.cpp.

{
    std::string str;
    std::stringstream rawstr(str);
    rawstr << "[:";
    for (CallStrCxt::const_iterator it = cxt.begin(), eit = cxt.end(); it != eit; ++it)
    {
        rawstr << " ' " << *it << " ' ";
        rawstr << tcg->getCallSite(*it)->getCallSite()->toString();
        rawstr << "  call  " << tcg->getCallSite(*it)->getCaller()->getName() << "-->" << tcg->getCalleeOfCallSite(*it)->getName() << ", \n";
    }
    rawstr << " ]";
    outs() << "max cxt = " << cxt.size() << rawstr.str() << "\n";
}

dumpCxt() [2/2]

void SVF::MTAResultValidator::dumpCxt ( const CallStrCxt &  cxt ) const

protected

dumpInterlev() [1/2]

void MTAResultValidator::dumpInterlev ( NodeBS &  lev )

protected

Definition at line 204 of file MTAResultValidator.cpp.

{
    outs() << " [ ";
    for (NodeBS::iterator it = lev.begin(), eit = lev.end(); it != eit; it++)
    {
        NodeID id = *it;
        outs() << rthdTovthd[id] << ", ";
    }
    outs() << "]\n";
}

dumpInterlev() [2/2]

void SVF::MTAResultValidator::dumpInterlev ( NodeBS &  lev )

protected

getCxtArg() [1/2]

CallStrCxt MTAResultValidator::getCxtArg ( const Instruction *  inst, unsigned int  arg_num  )

protected

Definition at line 115 of file MTAResultValidator.cpp.

{
    std::vector<std::string> x = getStringArg(inst, arg_num);
    CallStrCxt cxt;
    if (0 == x.size())
        return cxt;
    // Deal with the second argument that records all callsites
    for (std::vector<std::string>::iterator i = x.begin(); i != x.end(); i++)
    {
        std::vector<std::string> y = split((*i), '.');
        y[0].erase(y[0].find("cs"), 2);
 
        const SVFFunction* callee = mod->getSVFFunction(y[1]);
        const SVFInstruction* svfInst = csnumToInstMap[atoi(y[0].c_str())];
        assert(callee && "callee error");
        CallICFGNode* cbn = mhp->getTCT()->getCallICFGNode(svfInst);
        CallSiteID csId = tcg->getCallSiteID(cbn, callee);
        cxt.push_back(csId);
    }
    return cxt;
}

getCxtArg() [2/2]

CallStrCxt SVF::MTAResultValidator::getCxtArg ( const Instruction *  inst, unsigned int  arg_num  )

protected

getIntArg() [1/2]

NodeID SVF::MTAResultValidator::getIntArg ( const Instruction *  inst, unsigned int  arg_num  )

protected

getIntArg() [2/2]

NodeID SVF::MTAResultValidator::getIntArg ( const Instruction *  inst, unsigned int  arg_num  )

protected

getModule() [1/2]

SVFModule* SVF::MTAResultValidator::getModule ( ) const

inline

Definition at line 41 of file MTAResultValidator.h.

    {
        return mod;
    }

getModule() [2/2]

SVFModule* SVF::MTAResultValidator::getModule ( ) const

inline

Definition at line 40 of file MTAResultValidator.h.

    {
        return mod;
    }

getOutput() [1/2]

std::string MTAResultValidator::getOutput ( const char *  scenario, bool  analysisRes  )

inlineprotected

Definition at line 149 of file MTAResultValidator.cpp.

{
    std::string ret(scenario);
    ret += "\t";
 
    if (analysisRes)
        ret += SVFUtil::sucMsg("SUCCESS");
    else
        ret += SVFUtil::errMsg("FAILURE");
    return ret;
}

getOutput() [2/2]

std::string SVF::MTAResultValidator::getOutput ( const char *  scenario, bool  analysisRes  )

inlineprotected

getOutputforInterlevAnalysis() [1/2]

std::string MTAResultValidator::getOutputforInterlevAnalysis ( const char *  scenario, INTERLEV_FLAG  analysisRes  )

inlineprotected

Definition at line 161 of file MTAResultValidator.cpp.

{
    std::string ret(scenario);
    ret += "\t";
    switch (analysisRes)
    {
    case INTERLEV_TRUE:
        ret += SVFUtil::sucMsg("SUCCESS");
        break;
    case INTERLEV_UNSOUND:
        ret += SVFUtil::bugMsg2("UNSOUND");
        break;
    case INTERLEV_IMPRECISE:
        ret += SVFUtil::bugMsg1("IMPRECISE");
        break;
    default:
        ret += SVFUtil::errMsg("FAILURE");
    }
    return ret;
}

getOutputforInterlevAnalysis() [2/2]

std::string SVF::MTAResultValidator::getOutputforInterlevAnalysis ( const char *  scenario, INTERLEV_FLAG  analysisRes  )

inlineprotected

getPreviousMemoryAccessInst() [1/2]

const Instruction * MTAResultValidator::getPreviousMemoryAccessInst ( const Instruction *  I )

protected

Definition at line 137 of file MTAResultValidator.cpp.

{
    I = I->getPrevNode();
    while (I)
    {
        if (SVFUtil::isa<LoadInst>(I) || SVFUtil::isa<StoreInst>(I))
            return I;
        I = I->getPrevNode();
    }
    return nullptr;
}

getPreviousMemoryAccessInst() [2/2]

const Instruction* SVF::MTAResultValidator::getPreviousMemoryAccessInst ( const Instruction *  I )

protected

getStringArg() [1/2]

std::vector< std::string > MTAResultValidator::getStringArg ( const Instruction *  inst, unsigned int  arg_num  )

protected

Definition at line 95 of file MTAResultValidator.cpp.

{
    assert(LLVMUtil::isCallSite(inst) && "getFirstIntArg: inst is not a callinst");
    const CallBase* cs = LLVMUtil::getLLVMCallSite(inst);
    assert((arg_num < cs->arg_size()) && "Does not has this argument");
    const Constant* arrayinst = SVFUtil::dyn_cast<Constant>(cs->getArgOperand(arg_num));
    if(const GetElementPtrInst* gepinst = SVFUtil::dyn_cast<GetElementPtrInst>(cs->getArgOperand(arg_num)))
    {
        arrayinst = SVFUtil::dyn_cast<Constant>(gepinst->getOperand(0));
    }
    const ConstantDataArray* cxtarray = SVFUtil::dyn_cast<ConstantDataArray>(arrayinst->getOperand(0));
    if (!cxtarray)
    {
        std::vector<std::string> strvec;
        return strvec;
    }
    const std::string vthdcxtstring = cxtarray->getAsCString().str();
    return split(vthdcxtstring, ',');
}

getStringArg() [2/2]

std::vector<std::string> SVF::MTAResultValidator::getStringArg ( const Instruction *  inst, unsigned int  arg_num  )

protected

matchCxt() [1/2]

bool MTAResultValidator::matchCxt ( const CallStrCxt  cxt1, const CallStrCxt  cxt2  ) const

protected

Definition at line 182 of file MTAResultValidator.cpp.

{
    if (cxt1.size() != cxt2.size())
        return false;
    return std::equal(cxt1.begin(), cxt1.end(), cxt2.begin());
}

matchCxt() [2/2]

bool SVF::MTAResultValidator::matchCxt ( const CallStrCxt  cxt1, const CallStrCxt  cxt2  ) const

protected

split() [1/4]

std::vector< std::string > MTAResultValidator::split ( const std::string &  s, char  delim  )

protected

Definition at line 80 of file MTAResultValidator.cpp.

{
    std::vector<std::string> elems;
    split(s, delim, elems);
    return elems;
}

split() [2/4]

std::vector<std::string> SVF::MTAResultValidator::split ( const std::string &  s, char  delim  )

protected

split() [3/4]

std::vector< std::string > & MTAResultValidator::split ( const std::string &  s, char  delim, std::vector< std::string > &  elems  )

protected

Definition at line 69 of file MTAResultValidator.cpp.

{
    std::stringstream ss(s);
    std::string item;
    while (std::getline(ss, item, delim))
    {
        elems.push_back(item);
    }
    return elems;
}

split() [4/4]

std::vector<std::string>& SVF::MTAResultValidator::split ( const std::string &  s, char  delim, std::vector< std::string > &  elems  )

protected

validateCxtThread() [1/2]

bool MTAResultValidator::validateCxtThread ( )

protected

Definition at line 372 of file MTAResultValidator.cpp.

{
 
    bool res = true;
    TCT* tct = mhp->getTCT();
    if (tct->getTCTNodeNum() != vthdToCxt.size())
    {
        res = false;
        if (Options::PrintValidRes())
        {
            outs() << errMsg("\nValidate CxtThread: The number of CxtThread is different from given result!!!\n");
            outs() << "Given threads:\t" << vthdToCxt.size() << "\nAnalysis result:\t" << tct->getTCTNodeNum() << "\n";
            assert(false && "test case failed!");
        }
    }
 
    Set<int> visitedvthd;
 
    for (NodeID i = 0; i < tct->getTCTNodeNum(); i++)
    {
        const CxtThread rthd = tct->getTCTNode(i)->getCxtThread();
        bool matched = false;
        for (Map<NodeID, CallStrCxt>::iterator j = vthdToCxt.begin(), ej = vthdToCxt.end(); j != ej; j++)
        {
            NodeID vthdid = (*j).first;
            if (matchCxt(rthd.getContext(), vthdToCxt[vthdid]))
            {
                if (visitedvthd.find(vthdid) != visitedvthd.end())
                {
                    res = false;
                    if (Options::PrintValidRes())
                    {
                        outs() << "\nValidate CxtThread: Repeat real CxtThread !!!\n";
                        rthd.dump();
                        tct->getTCTNode(vthdTorthd[vthdid])->getCxtThread().dump();
                    }
                }
                vthdTorthd[vthdid] = i;
                rthdTovthd[i] = vthdid;
                visitedvthd.insert(vthdid);
                matched = true;
                break;
            }
        }
        if (!matched)
        {
            res = false;
            if (Options::PrintValidRes())
            {
                SVFUtil::errs() << errMsg("\nValidate CxtThread: Cannot match real CxtThread !!!\n");
                rthd.dump();
                assert(false && "test case failed!");
            }
        }
    }
    if (visitedvthd.size() != vthdToCxt.size())
    {
        res = false;
        if (Options::PrintValidRes())
        {
            SVFUtil::errs() << errMsg("\nValidate CxtThread: Some given CxtThreads cannot be found !!!\n");
            assert(false && "test case failed!");
            for (Map<NodeID, CallStrCxt>::iterator j = vthdToCxt.begin(), ej = vthdToCxt.end(); j != ej; j++)
            {
                NodeID vthdid = (*j).first;
                if (visitedvthd.find(vthdid) == visitedvthd.end())
                {
                    dumpCxt(vthdToCxt[vthdid]);
                }
            }
        }
    }
    return res;
}

validateCxtThread() [2/2]

bool SVF::MTAResultValidator::validateCxtThread ( )

protected

validateInterleaving() [1/2]

MTAResultValidator::INTERLEV_FLAG MTAResultValidator::validateInterleaving ( )

protected

Definition at line 498 of file MTAResultValidator.cpp.

{
    MTAResultValidator::INTERLEV_FLAG res = MTAResultValidator::INTERLEV_TRUE;
 
    for (MHP::InstToThreadStmtSetMap::iterator seti = instToTSMap.begin(), eseti = instToTSMap.end(); seti != eseti; ++seti)
    {
        const SVFInstruction* inst = (*seti).first;
 
        const MHP::CxtThreadStmtSet& tsSet = mhp->getThreadStmtSet(inst);
 
        if ((*seti).second.size() != tsSet.size())
        {
            if (Options::PrintValidRes())
            {
                outs() << errMsg("\n Validate Interleaving: Wrong at : ") << inst->getSourceLoc() << "\n";
                outs() << "Reason: The number of thread running on stmt is wrong\n";
                outs() << "\n----Given threads:\n";
                for (MHP::CxtThreadStmtSet::iterator thdlevi = (*seti).second.begin(), ethdlevi = (*seti).second.end(); thdlevi != ethdlevi;
                        ++thdlevi)
                {
                    outs() << "TID " << rthdTovthd[(*thdlevi).getTid()] << ": ";
                    dumpCxt((*thdlevi).getContext());
                }
                outs() << "\n----Analysis threads:\n";
                for (MHP::CxtThreadStmtSet::const_iterator it = tsSet.begin(), eit = tsSet.end(); it != eit; ++it)
                {
                    outs() << "TID " << rthdTovthd[(*it).getTid()] << ": ";
                    dumpCxt((*it).getContext());
                }
                outs() << "\n";
            }
            res = MTAResultValidator::INTERLEV_UNSOUND;
        }
 
        for (MHP::CxtThreadStmtSet::const_iterator it = tsSet.begin(), eit = tsSet.end(); it != eit; ++it)
        {
            const CxtThreadStmt& ts = *it;
            bool matched = false;
            for (MHP::CxtThreadStmtSet::iterator it2 = (*seti).second.begin(), eit2 = (*seti).second.end(); it2 != eit2; ++it2)
            {
                const CxtThreadStmt& ts2 = *it2;
 
                if (ts2.getTid() == ts.getTid() && matchCxt(ts2.getContext(), ts.getContext()))
                {
                    matched = true;
                    NodeBS lev = mhp->getInterleavingThreads(ts);
                    NodeBS lev2 = threadStmtToInterLeaving[ts2];
                    if (lev != lev2)
                    {
                        if (Options::PrintValidRes())
                        {
                            outs() << errMsg("\nValidate Interleaving: Wrong at: ") << inst->getSourceLoc() << "\n";
                            outs() << "Reason: thread interleaving on stmt is wrong\n";
                            dumpCxt(ts.getContext());
                            outs() << "Given result:    \tTID " << rthdTovthd[ts.getTid()];
                            dumpInterlev(lev2);
                            outs() << "Analysis result: \tTID " << rthdTovthd[ts.getTid()];
                            dumpInterlev(lev);
                        }
 
                        if (MTAResultValidator::INTERLEV_IMPRECISE > res)
                            res = MTAResultValidator::INTERLEV_IMPRECISE;
 
                        if (lev.count() >= lev2.count())
                        {
                            bool findeveryelement = true;
                            for (NodeBS::iterator it = lev2.begin(), eit = lev2.end(); it != eit; it++)
                            {
                                if (!lev.test(*it))
                                {
                                    findeveryelement = false;
                                    break;
                                }
                            }
                            if (!findeveryelement)
                                res = MTAResultValidator::INTERLEV_UNSOUND;
                        }
                        else
                            res = MTAResultValidator::INTERLEV_UNSOUND;
                    }
                }
            }
 
            if (!matched)
            {
                if (Options::PrintValidRes())
                {
                    outs() << errMsg("\nValidate Interleaving: Wrong at:") << inst->getSourceLoc() << "\n";
                    outs() << "Reason: analysis thread cxt is not matched by given thread cxt\n";
                    dumpCxt(ts.getContext());
                    NodeBS lev = mhp->getInterleavingThreads(ts);
 
                    outs() << "Analysis result: \tTID " << rthdTovthd[ts.getTid()];
                    dumpInterlev(lev);
                }
                res = MTAResultValidator::INTERLEV_UNSOUND;
            }
        }
    }
    return res;
}

validateInterleaving() [2/2]

INTERLEV_FLAG SVF::MTAResultValidator::validateInterleaving ( )

protected

validateTCT() [1/2]

bool MTAResultValidator::validateTCT ( )

protected

Definition at line 447 of file MTAResultValidator.cpp.

{
    bool res = true;
 
    TCT* tct = mhp->getTCT();
    for (NodeID i = 0; i < tct->getTCTNodeNum(); i++)
    {
        bool res_node = true;
        TCTNode* pnode = tct->getTCTNode(i);
        for (TCT::ThreadCreateEdgeSet::const_iterator ci = tct->getChildrenBegin(pnode), cei = tct->getChildrenEnd(pnode); ci != cei;
                ci++)
        {
            NodeID tid = (*ci)->getDstID();
            if (rthdToChildren[i].find(tid) == rthdToChildren[i].end())
            {
                res = false;
                res_node = false;
            }
        }
 
        for (Set<NodeID>::iterator j = rthdToChildren[i].begin(), ej = rthdToChildren[i].end(); j != ej; j++)
        {
            NodeID gid = *j;
            if (!tct->hasGraphEdge(pnode, tct->getTCTNode(gid), TCTEdge::ThreadCreateEdge))
            {
                res = false;
                res_node = false;
            }
        }
        if ((!res_node) && Options::PrintValidRes())
        {
            outs() << errMsg("\nValidate TCT: Wrong at TID ") << rthdTovthd[i] << "\n";
            outs() << "Given children: \t";
            for (Set<NodeID>::iterator j = rthdToChildren[i].begin(), ej = rthdToChildren[i].end(); j != ej; j++)
            {
                NodeID gid = *j;
                outs() << rthdTovthd[gid] << ", ";
            }
            outs() << "\nAnalysis children:\t";
            for (TCT::ThreadCreateEdgeSet::const_iterator ci = tct->getChildrenBegin(pnode), cei = tct->getChildrenEnd(pnode); ci != cei;
                    ci++)
            {
                NodeID tid = (*ci)->getDstID();
                outs() << rthdTovthd[tid] << ", ";
            }
            outs() << "\n";
        }
    }
    return res;
}

validateTCT() [2/2]

bool SVF::MTAResultValidator::validateTCT ( )

protected

Member Data Documentation

csnumToInstMap

csnumToInst SVF::MTAResultValidator::csnumToInstMap

private

Definition at line 141 of file MTAResultValidator.h.

CXT_THREAD

static constexpr char const * SVF::MTAResultValidator::CXT_THREAD = "CXT_THREAD"

staticconstexprprivate

Map a statement to its thread interleavings.

Definition at line 131 of file MTAResultValidator.h.

instToTSMap

MHP::InstToThreadStmtSetMap SVF::MTAResultValidator::instToTSMap

private

Definition at line 128 of file MTAResultValidator.h.

INTERLEV_ACCESS

static constexpr char const * SVF::MTAResultValidator::INTERLEV_ACCESS = "INTERLEV_ACCESS"

staticconstexprprivate

Definition at line 132 of file MTAResultValidator.h.

INTERLEV_IMPRECISE

static const INTERLEV_FLAG SVF::MTAResultValidator::INTERLEV_IMPRECISE = 0x02

staticprivate

Definition at line 147 of file MTAResultValidator.h.

INTERLEV_TRUE

static const INTERLEV_FLAG SVF::MTAResultValidator::INTERLEV_TRUE = 0x01

staticprivate

Constant INTERLEV_FLAG values.

Definition at line 146 of file MTAResultValidator.h.

INTERLEV_UNSOUND

static const INTERLEV_FLAG SVF::MTAResultValidator::INTERLEV_UNSOUND = 0x04

staticprivate

Definition at line 148 of file MTAResultValidator.h.

mhp

MHP * SVF::MTAResultValidator::mhp

private

Definition at line 137 of file MTAResultValidator.h.

mod

SVFModule * SVF::MTAResultValidator::mod

private

Definition at line 143 of file MTAResultValidator.h.

rthdToChildren

rthdToChildrenMap SVF::MTAResultValidator::rthdToChildren

private

Definition at line 142 of file MTAResultValidator.h.

rthdTovthd

rthdTovthdMap SVF::MTAResultValidator::rthdTovthd

private

Definition at line 140 of file MTAResultValidator.h.

tcg

ThreadCallGraph * SVF::MTAResultValidator::tcg

private

Definition at line 136 of file MTAResultValidator.h.

TCT_ACCESS

static constexpr char const * SVF::MTAResultValidator::TCT_ACCESS = "TCT_ACCESS"

staticconstexprprivate

Definition at line 133 of file MTAResultValidator.h.

tdAPI

ThreadAPI * SVF::MTAResultValidator::tdAPI

private

Definition at line 135 of file MTAResultValidator.h.

threadStmtToInterLeaving

MHP::ThreadStmtToThreadInterleav SVF::MTAResultValidator::threadStmtToInterLeaving

private

Definition at line 129 of file MTAResultValidator.h.

vthdToCxt

vthdToCxtMap SVF::MTAResultValidator::vthdToCxt

private

Definition at line 138 of file MTAResultValidator.h.

vthdTorthd

vthdTorthdMap SVF::MTAResultValidator::vthdTorthd

private

Definition at line 139 of file MTAResultValidator.h.

---

The documentation for this class was generated from the following files:

• /home/runner/work/SVF/SVF/svf-llvm/tools/MTA/MTAResultValidator.h
• /home/runner/work/SVF/SVF/svf-llvm/tools/MTA/MTAResultValidator.cpp