SVF-tools / SVF

Static Value-Flow Analysis Framework for Source Code
http://svf-tools.github.io/SVF/
Other
1.41k stars 437 forks source link

const: Assertion `it!=LLVMInst2SVFInst.end() && "SVF Instruction not found!"' failed #1574

Open xiaobaozidi opened 5 days ago

xiaobaozidi commented 5 days ago

Hi,

I followed the SVF-example (https://github.com/SVF-tools/SVF-example) to traverse the nodes on the SVFG. I called the void traverseOnVFG() function, but I encountered an assertion failure:


svf-example: /home/SVF-tools/SVF/svf-llvm/include/SVF-LLVM/LLVMModule.h:245: SVF::SVFInstruction* SVF::LLVMModuleSet::getSVFInstruction(const SVF::Instruction*) const: Assertion `it!=LLVMInst2SVFInst.end() && "SVF Instruction not found!"' failed.
Aborted (core dumped)

I identified the issue occurs where the LLVM value is being transferred to the SVF value. It seems that the corresponding SVF value does not exist in the LLVMInst2SVFInst map.

In my toy example, I am attempting to traverse the node starting from line 18. I first convert the value at line 18 to an LLVM value and then call: SVFValue* svfval = LLVMModuleSet::getLLVMModuleSet()->getSVFValue(val);

However, this assertion fails, suggesting that the corresponding LLVM value is not found in the LLVMInst2SVFInst map. Interestingly, I printed out the values in the LLVMInst2SVFInst map, and it seems like the LLVM value does exist in the map.

Could this issue be related to the environment setup (since I am using LLVM-16 with the provided docker), or might there be something else causing the map lookup to fail despite the value being present?

  1 #include <stdio.h>
  2 
  3 int compute(int a, int b) {
  4     int x = a * 2;    // Step 1: Multiply 'a' by 2
  5     int y = b + 3;    // Step 2: Add 3 to 'b'
  6 
  7     int z;
  8 
  9     // Branch: Depending on the value of 'x', perform different operations
 10     if (x > 10) {
 11         z = y * 2;    // Step 3: If 'x' > 10, multiply 'y' by 2
 12     } else {
 13         z = y - 1;    // Step 4: If 'x' <= 10, subtract 1 from 'y'
 14     }
 15 
 16     int result = z + a;    // Step 5: Add 'a' to 'z'
 17 
 18     return result;    // This is our slicing criterion
 19 }
 20 
 21 int main() {
 22     int a = 4;
 23     int b = 5;
 24 
 25     int result = compute(a, b);    // Step 6: Call compute with inputs a and b
 26 
 27     printf("Result: %d\n", result);
 28 
 29     return 0;
 30 }
 31 

I would appreciate any insights you might have regarding this issue.

yuleisui commented 5 days ago

@jumormt could you take a look at this?

jumormt commented 5 days ago

@xiaobaozidi Which version of SVF are you using? Could you also upload the bitcode and running options? thx

jumormt commented 5 days ago

You can try svf-ex. It works fine on my side with the latest version of SVF.

xiaobaozidi commented 4 days ago

Hi Jumormt,

Thank you for your response. I believe the issue arises when converting line 18 into an LLVM value and passing it to the following function: SVFValue* svfval = LLVMModuleSet::getLLVMModuleSet()->getSVFValue(val);

I implemented a function to perform the conversion from line number to an LLVM value. However, it seems that the LLVM contexts between SVF and my function are different, which appears to be causing the problem.

Is there any API available in SVF that can help retrieve the corresponding LLVM value based on a given filename and line number? This would ensure that the LLVM contexts remain consistent between my function and SVF.

jumormt commented 4 days ago

LLVMModuleSet::getLLVMModuleSet()->getLLVMValue(svfvalue) returns the llvm value of svfvalue. If you want to designate specific lines to start the analysis, I suggest you can first build a map from line number to value based on the built LLVMModule in SVF to avoid any inconsistency between different contexts.

jumormt commented 4 days ago

@xiaobaozidi The filename and line number cannot be directly obtained through any APIs but can be retrived through parsing its sourceloc.

xiaobaozidi commented 3 days ago

Thank you, this has been incredibly helpful. I have one more question regarding the svf-ex example (https://github.com/SVF-tools/SVF/blob/master/svf-llvm/tools/Example/svf-ex.cpp). I would like to traverse the SVFG graph to extract the data dependency graph specifically related to line 18. From what I understand, the traverseOnVFG() function already implements this functionality.

Based on my understanding, the Sparse Value Flow Graph (SVFG) contains all the necessary information to construct the data dependency graph, including both top-level and address-taken variables (refined through context-sensitive, flow-sensitive, and field-sensitive pointer analysis). Thus, I just need to call traverseOnVFG() from line 18 to get the data dependency graph.

Is my understanding is correct? Are there any additional steps I should take to accurately obtain the data dependency graph for line 18?

jumormt commented 3 days ago

Yes, the SVFG encodes whole-program data dependencies for both top-level and address-taken variables.