Skip to content
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.

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

fix a bug that leads to get many incorrect switch target case value -1 #1191

Merged
merged 2 commits into from
Sep 8, 2023
Merged

fix a bug that leads to get many incorrect switch target case value -1 #1191

merged 2 commits into from
Sep 8, 2023

Conversation

canliture
Copy link
Contributor

@canliture canliture commented Sep 8, 2023

When I use SVF to do some research on static (sparse) symbolic execution, e.g., translate SVFG/VFGNode to Z3 Formula. I think the the following code will lead to some incorrect formulas.

Given the code:

#include <stdio.h>


void test(int a) {
    switch (a)
    {
        case 0: printf("0\n"); break;
        case 1:
        case 2:
        case 3: printf("a >=1 && a <= 3\n"); break;
        case 4:
        case 6:
        case 7:  printf("a >= 4 && a <=7\n"); break;
        default: printf("a < 0 || a > 7"); break;
    }
}

SVF will get many incorrect target case value -1 due to use of API SwitchInst::findCaseDest. Here is comments about SwitchInst::findCaseDest:

/// Finds the unique case value for a given successor. Returns null if the
/// successor is not found, not unique, or is the default case.
ConstantInt *findCaseDest(BasicBlock *BB) {
  // ...
}

Find the unique case value .... .Return null if ... , not unique ...

@canliture canliture changed the title fix a bug that leads to get many incorrect switch target value -1 fix a bug that leads to get many incorrect switch target case value -1 Sep 8, 2023
@codecov
Copy link

codecov bot commented Sep 8, 2023

Codecov Report

Merging #1191 (f691c36) into master (324794b) will increase coverage by 0.01%.
Report is 1 commits behind head on master.
The diff coverage is 100.00%.

Additional details and impacted files

Impacted file tree graph

@@            Coverage Diff             @@
##           master    #1191      +/-   ##
==========================================
+ Coverage   64.64%   64.65%   +0.01%     
==========================================
  Files         222      222              
  Lines       23525    23536      +11     
==========================================
+ Hits        15207    15218      +11     
  Misses       8318     8318              
Files Changed Coverage Δ
svf-llvm/include/SVF-LLVM/LLVMUtil.h 76.25% <ø> (ø)
svf-llvm/lib/LLVMUtil.cpp 73.31% <100.00%> (+0.63%) ⬆️
svf-llvm/lib/SVFIRBuilder.cpp 78.15% <100.00%> (ø)
📢 Have feedback on the report? [Share it here](https://about.codecov.io/codecov-pr-comment-feedback/?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=None).

// Operand[1] = Default basic block destination
// Operand[2n ] = Value to match
// Operand[2n+1] = BasicBlock to go to on match
ConstantInt *condVal = SVFUtil::dyn_cast<ConstantInt>(inst.getOperand(i * 2));
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

what does this mean here, why i * 2? Can we use findCaseDest + something else?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In my mind, 'condVal' is target case value. And in LLVM IR:

Operand 0 is condition of switch,
Operand 1 is default BasicBlock Value , and

Operand 2 is target Value of the first Case
Operand 3 is target succussor BasicBlock Value of the first Case's
...
Operand 2n is target Value of the n-th Case
Operand 2n+1 is target succussor BasicBlock Value of the n-th Case's


Before we use findCaseDest, source code of findCaseDest is below:

  /// Finds the unique case value for a given successor. Returns null if the
  /// successor is not found, not unique, or is the default case.
  ConstantInt *findCaseDest(BasicBlock *BB) {
    if (BB == getDefaultDest())
      return nullptr;

    ConstantInt *CI = nullptr;
    for (auto Case : cases()) {
      if (Case.getCaseSuccessor() != BB)
        continue;

      if (CI)
        return nullptr; // Multiple cases lead to BB.

      CI = Case.getCaseValue();
    }

    return CI;
  }

we will get -1 findCaseDest of default case, and also get -1 when encounter continuous case without break stmt, the LLVM IR related the given code is

// ... 
  switch i32 %0, label %sw.default [
    i32 0, label %sw.bb                                ; get -1 due to default branch
    i32 1, label %sw.bb1                               ; get -1 without break
    i32 2, label %sw.bb1                              ; get -1  without break
    i32 3, label %sw.bb1                             
    i32 4, label %sw.bb3                             ; get -1 without break
    i32 6, label %sw.bb3                             ; get -1 without break
    i32 7, label %sw.bb3
  ], !dbg !18
// ... 

if we use findCaseDest + something else, let me thought a few moments. I can't give the answer at once...

@canliture
Copy link
Contributor Author

I give another answer:

void SVFIRBuilder::visitSwitchInst(SwitchInst &inst)
{
    NodeID brinst = getValueNode(&inst);
    NodeID cond = getValueNode(inst.getCondition());

    BranchStmt::SuccAndCondPairVec successors;

    std::vector<std::pair<ConstantInt*, BasicBlock*>> caseValue2SuccBBVec;
    // default case
    caseValue2SuccBBVec.push_back({nullptr, inst.getDefaultDest()});
    // normal case
    for (const SwitchInst::CaseHandle& cs : inst.cases())
    {
        caseValue2SuccBBVec.push_back({cs.getCaseValue(), cs.getCaseSuccessor()});
    }
    for (const auto& caseValue2SuccBB : caseValue2SuccBBVec)
    {
        ConstantInt *caseValue = caseValue2SuccBB.first;
        BasicBlock *succBB = caseValue2SuccBB.second;
        /// default case is set to -1;
        s64_t val = -1;
        if (caseValue != nullptr && succBB != inst.getDefaultDest())
        {
            if (caseValue->getBitWidth() <= 64)
                val = caseValue->getSExtValue();
        }
        const Instruction* succInst = &succBB->front();
        const SVFInstruction* svfSuccInst = LLVMModuleSet::getLLVMModuleSet()->getSVFInstruction(succInst);
        const ICFGNode* icfgNode = pag->getICFG()->getICFGNode(svfSuccInst);
        SVFUtil::outs() << val << ": " << succBB->getName().str() << std::endl;
        successors.push_back(std::make_pair(icfgNode,val));
    }
    addBranchStmt(brinst, cond,successors);
}

output is:

-1: sw.default
0: sw.bb
1: sw.bb1
2: sw.bb1
3: sw.bb1
4: sw.bb3
6: sw.bb3
7: sw.bb3

@yuleisui
Copy link
Collaborator

yuleisui commented Sep 8, 2023

This look good but code is quite a lot. Could we try to simplify it and any helper functions or make the naming more explicit and easy understandable

…e: get case successor basic block and related case value.
@canliture
Copy link
Contributor Author

This look good but code is quite a lot. Could we try to simplify it and any helper functions or make the naming more explicit and easy understandable

Yeah, I think I have make the code more easily understandable by f691c36

@yuleisui
Copy link
Collaborator

yuleisui commented Sep 8, 2023

Thanks and will merge.

@yuleisui
Copy link
Collaborator

yuleisui commented Sep 8, 2023

Are there any test cases you could provide here to showcase the difference between current buggy implementation and your fix.

@canliture
Copy link
Contributor Author

Are there any test cases you could provide here to showcase the difference between current buggy implementation and your fix.

given the testcase:

#include <stdio.h>

void test(int a) {
    switch (a)
    {
        case 0: printf("0\n"); break;
        case 1:
        case 2:
        case 3: printf("a >=1 && a <= 3\n"); break;
        case 4:
        case 6:
        case 7:  printf("a >= 4 && a <=7\n"); break;
        default: printf("a < 0 || a > 7"); break;
    }
}

generate IR part related switch:

...
  switch i32 %0, label %sw.default [
    i32 0, label %sw.bb
    i32 1, label %sw.bb1
    i32 2, label %sw.bb1
    i32 3, label %sw.bb1
    i32 4, label %sw.bb3
    i32 6, label %sw.bb3
    i32 7, label %sw.bb3
  ], !dbg !18
...

insert a line code into the original codes here:

const ICFGNode* icfgNode = pag->getICFG()->getICFGNode(svfSuccInst);
successors.push_back(std::make_pair(icfgNode,val));

inserted code like this:

const ICFGNode* icfgNode = pag->getICFG()->getICFGNode(svfSuccInst);
SVFUtil::outs() << "case value " << val << ": " << inst.getSuccessor(i)->getName().str() << std::endl;
successors.push_back(std::make_pair(icfgNode,val));

run wpa or other tools that will call into SVFIRBuilder::visitSwitchInst to build SVFIR, output like this:

case value -1: sw.default
case value 0: sw.bb
case value -1: sw.bb1
case value -1: sw.bb1
case value -1: sw.bb1
case value -1: sw.bb3
case value -1: sw.bb3
case value -1: sw.bb3

Apparently, the output is not correct. After applying the patch, and insert code at the same place:

const ICFGNode* icfgNode = pag->getICFG()->getICFGNode(svfSuccInst);
SVFUtil::outs() << "case value " << val << ": " << succBB->getName().str() << std::endl;
successors.push_back(std::make_pair(icfgNode, val));

run wpa or other tools that will call into SVFIRBuilder::visitSwitchInst to build SVFIR, new output like this:

case value -1: sw.default
case value 0: sw.bb
case value 1: sw.bb1
case value 2: sw.bb1
case value 3: sw.bb1
case value 4: sw.bb3
case value 6: sw.bb3
case value 7: sw.bb3

Apparently, the output is correct.

@yuleisui yuleisui merged commit 6a4144d into SVF-tools:master Sep 8, 2023
5 checks passed
JasonZhongZexin pushed a commit to JasonZhongZexin/SVF-1 that referenced this pull request Sep 13, 2023
SVF-tools#1191)

* fix a bug that leads to get many incorrect switch target value -1

* complete SVFIRBuilder about SwitchInst and make it easy understandable: get case successor basic block and related case value.
yuleisui added a commit that referenced this pull request Sep 13, 2023
* fix vfspta read&write

* fix

* fix a nullptr dereference when creating AndersenSCD singleton instance

* Fix the bug of failing to find extapi.bc in npm

* Chang function names in ExtAPI

* SVF code formatter

* Add comments to some APIs in SVFIRExtAPI.cpp

* SVF code formatter

* fix getgepoffset and accumulateconstantOffset
support byte size

* refactor gepoffset api and accumulateOffset api
1. add getBytefromGepTypePair in SvfIR2ItvExeState
2. add getIndexfromGepTypePair in SvfIR2ItvExeState
3. add accumulateConstantByteOffset in AccessPath

* add comment to getGepByteOffset and accumulateConstantByteOffset

* SVF code formatter

* Remove "STATIC" annotation in extapi.bc (#1188)

* Remove "STATIC" annotation in extapi.bc

* Return "STATIC_OBJECT" in an external function which has a static var that its return value points to

* Move the functions with annotations to the front of the functions without annotations in extapi.c

* annotate fdopen() with "ALLOC_RET"

* fix a bug that leads to get many incorrect switch target case value -1 (#1191)

* fix a bug that leads to get many incorrect switch target value -1

* complete SVFIRBuilder about SwitchInst and make it easy understandable: get case successor basic block and related case value.

* add reshapeValue() to getOffsetfromGepPair (#1192)

* add reshapeValue() to getOffsetfromGepPair

* refactor getGepByteOffset and accumulateConstantByteOffset

* fix SVF CI compile err

---------

Co-authored-by: jiawei.wang <jiawei.wang@horizon.ai>

* SVF code formatter

* replace int64 with s64 in IntervalValue/Z3Expr (#1195)

* add reshapeValue() to getOffsetfromGepPair

* refactor getGepByteOffset and accumulateConstantByteOffset

* fix SVF CI compile err

* replace int64 with s64 to IntervalValue

* replace more int64 with s64

* replace more int64 with s64

* replace more int64 with s64

* replace more int64 with s64

* replace more int64 with s64

* replace more int64 with s64

---------

Co-authored-by: jiawei.wang <jiawei.wang@horizon.ai>

* SVF code formatter

update code

update changes

update

upate

---------

Co-authored-by: JasonZhongZexin <jason@PC-20220224QJOH.localdomain>
Co-authored-by: canliture <canliture@outlook.com>
Co-authored-by: shuangxiang kan <18550887212@163.com>
Co-authored-by: GitHub Actions Build <rockysui@gmail.com>
Co-authored-by: jiawei.wang <jiawei.wang@horizon.ai>
Co-authored-by: shuangxiang kan <47422069+shuangxiangkan@users.noreply.github.com>
Co-authored-by: Jiawei Wang <jackwang834@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants