search

seahorn / sea-dsa

A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
Other
157 stars 29 forks source link

Question: sea-dsa does not produce memory graph when main function has internal linkage type. #109

Closed shaobo-he closed 3 years ago

shaobo-he commented 3 years ago

Hello sea-dsa developers,

I tried to run sea-dsa on a file that is processed with the LLVM internalization pass (opt flag -internalize). No memory graphs are produced. When I removed the internal keyword in the definition of main function, it can generate a correct one. So I was wondering if sea-dsa should reject this type of program since something is probably wrong with main function having internal linkage type. SMACK seems to have a need for the internalization pass so we hope there's a way to let sea-dsa process this type of program.

shaobo-he commented 3 years ago

file.zip This is a test bc file. The command I invoked sea-dsa (dev10 branch) on it is seadsa -sea-dsa=ci -sea-dsa-dot strings-opt.ll.

caballa commented 3 years ago

The problem is that once main has internal linkage then it becomes a dead function. In fact, if you run opt even with -O1 I believe then you should get an empty module. So from sea-dsa perspective, I don't see any problem. You give an empty module to sea-dsa you get empty graphs. Note that technically in your example the module is not empty (but it would be with opt -O1) but we follow the callgraph of the module which detects that there is no incoming edge to main so it will be correctly skipped. When main has no internal linkage there is a special edge from the root of the call graph to main so then main cannot be skipped

caballa commented 3 years ago

Why does SMACK need to internalize main? In SeaHorn, we also have an internalize pass to force aggressive inlining but main is not internalized.

shaobo-he commented 3 years ago

Why does SMACK need to internalize main? In SeaHorn, we also have an internalize pass to force aggressive inlining but main is not internalized.

Thank you for your reply, @caballa. We don't need to internalize the main function. It's just that we used to internalize all the functions but llvm dsa seems to be ok with it. So I'm curious what's going on here. Now it makes perfect sense. Thanks again.