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

Fix unique scalars #12

Closed kuhar closed 6 years ago

kuhar commented 6 years ago

Make m_unique_scalar and m_has_unique_scalar consistent.

agurfinkel commented 6 years ago

it is strange to have both bool flag and a pointer. Your change makes the bool flag redundant.

This could be correct, or there could be a case where unique scalar was set, but to null. If such case is possible, it would mean that scalar is some unknown value, and if it is set again, then the scalar must be reset.

On the other hand, if I am wrong and there is no such use, we should remove bool flag and have both set() and reset() methods instead of set to null

caballa commented 6 years ago

Yes, that's weird. Let me check the code

caballa commented 6 years ago

OK, it's intended that m_unique_scalar and m_has_unique_scalar might not be consistent.

m_unique_scalar can be reset to null. The purpose of m_has_unique_scalar is to remember if the node was ever set to some scalar (different from null).

When we run context-sensitive analysis, in order to claim a node is a unique scalar we need to run a global analysis on the call graph and making sure that all callsites agree on the claim. The way we represent "top" is by set m_unique_scalar to null but remembering that the node was once non-null. I did this so that the join operation is bitwise-or. But I'll try to see if this reasoning can be simplified because it's very confusing.

At the very least, we can rename m_has_unique_scalar to m_has_once_unique_scalar and add a comment.

agurfinkel commented 6 years ago

Renaming and adding a comment like the one above would help avoid this confusion in the future. I'm closing this pull request for now.