[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