[llvm-dev] Possible soundness issue with available_externally (split from "RFC: Add guard intrinsics")
Sanjoy Das via llvm-dev
llvm-dev at lists.llvm.org
Thu Feb 25 08:33:50 PST 2016
Hal Finkel wrote:
> That summary needs unnecessarily broad. So far we've learned that: a) There are issues with atomics b) there are issues
> with a safe-to-speculate attribute we don't yet have c) there might be issues with folding undefs independent of the
> previous two items, but we thus-far lack a concrete example. We don't yet have enough information.
I don't have a good example for (c), but if you go by the textbook "is
a non-deterministic value" definition for undef then
void foo() available_externally {
%x = create_undef();
if (%x) print("X");
}
is just as problematic as the two atomic loads case. This isn't a
good example though, since we can specify as part of `undef` s
semantics: "if the program has different observable behavior based on
undef's non-determinism, then it is undefined". However, if we do
that, we'll get stuck in cases like
// In C
void foo() {
int c;
if (c) print("X");
escape(&c); // escape is an empty function
}
which I think is not UB in C (is it?), but will boil down to the kind
of IR above.
-- Sanjoy
More information about the llvm-dev
mailing list