Closed RyanGlScott closed 2 months ago
FWIW, there are some interesting things that handling metadata during symbolic execution can enable, such as checking validity of debug info a la this work: https://convolv.es/talks/testing-debug-info/
I don't think it should weigh too much on our deliberations about this issue, but it could be a gentle point in favor of leaving the door open for processing metadata.
It also occurs to me that actually processing these declarations might help by allowing things like under-constrained symbolic execution to respect/check aliasing requirements.
Sooner or later there'll be a spec you can't prove unless you can reason about (non)aliasing of pointers, so I'd agree with the last part. FWIW
Thinking about this some more, I don't think that encoding metadata
values as Crucible simulator values is a good idea, mainly because it would be annoying to figure out how to mux everything that can appear inside a metadata
value. Moreover, if we do want to reason about the behavior of llvm.experimental.noalias.scope.decl
later, then a better way to do it would be to extend LLVMStmt
with a data constructor that handles llvm.experimental.noalias.scope.decl
. (Perhaps we could call it LLVM_NoAlias
or something similar.) This mirrors the way we handle certain llvm.dbg.*
statements by having a dedicated LLVM_Dbg
data constructor for LLVMStmt
.
That being said, crucible-llvm
doesn't yet do this sort of reasoning, and I don't yet have a pressing need for it—rather, my primary objective is to support recent versions of LLVM. As such, the most expedient fix is to add llvm.experimental.noalias.scope.decl
to the list of LLVM intrinsics to skip here. This means that we can avoid needing to translate metadata
values into Crucible simulator values, which is nice.
I'm going to pursue the aforementioned expedient fix in an upcoming patch. If we want to support no-alias reasoning at a deeper level in the future, we can implement the LLVM_NoAlias
idea.
C has a
restrict
mechanism that lets you indicate whether two pointers cannot alias. Here is an example based off of these slides:Prior to LLVM 12,
restrict
would compile to anoalias
annotation, whichcrucible-llvm
ignores¹:In LLVM 12 or later, however, the
noalias
annotation was replaced with a dedicatedllvm.experimental.noalias.scope.decl
intrinsic. Here is a standalone program that can be used to make Clang emit this intrinsic:Clang 14.0.0 will compile this to:
Unfortunately,
crucible-llvm
cannot handle this intrinsic out of the box:The problem is revealed in the
unsupported LLVM value: ValMd (ValMdNode [Just (ValMdRef 24)]) of type metadata
part of the error: thellvm.experimental.noalias.scope.decl
intrinsic takes ametadata
value as an argument, andcrucible-llvm
currently does not support any intrinsics that acceptmetadata
values as arguments². In fact,crucible-llvm
doesn't even support translatingmetadata
values, which is what leads to the error message above.The most expedient course of action would be to figure out how to make
crucible-llvm
treat calls to this intrinsic as a no-op. The main barrier is figuring out how to translatemetadata
values. Perhaps these can be translated to a trivial Crucible representation (e.g.,UnitRepr
).¹Perhaps
crucible-llvm
shouldn't ignore this, but that's a discussion for another issue. ²Strictly speaking,crucible-llvm
does handle somellvm.dbg.*
intrinsics that acceptmetadata
values as arguments, but these are done in a very ad hoc, special-cased fashion. See this code.