[llvm-dev] Possible soundness issue with available_externally (split from "RFC: Add guard intrinsics")

[Hal Finkel via llvm-dev]

----- Original Message -----
> From: "Sanjoy Das" <sanjoy at playingwithpointers.com>
> To: "Hal Finkel" <hfinkel at anl.gov>
> Cc: "Chandler Carruth" <chandlerc at google.com>, "llvm-dev" <llvm-dev at lists.llvm.org>, "Philip Reames"
> <listmail at philipreames.com>, "Duncan P. N. Exon Smith" <dexonsmith at apple.com>
> Sent: Thursday, February 25, 2016 1:47:04 AM
> Subject: Re: [llvm-dev] Possible soundness issue with available_externally (split from "RFC: Add guard intrinsics")
> 
> On Wed, Feb 24, 2016 at 11:44 PM, Hal Finkel <hfinkel at anl.gov> wrote:
> >> The only optimizations I can think of that are okay are algebraic
> >> simplifications that don't exploit no-overflow, inbounds or exact
> >
> > Why? Can you provide an example using nsw, inbounds, etc.?
> 
> I think the same case as the general UB applies:
> 
> void foo(int n) available_externally {
>   if (n s< (n +nsw 1)) abort();
> }
> 
> void bar() {
>   if (< runtine cond always false>)
>     foo(INT_SMAX);
> }
> 
> Now foo() can be simplified to "ret void" using the nsw, and the call
> to foo(INT_SMAX) can be hoisted.  This is a problem if we link to an
> unrefined @foo.

This is another example of why speculation safety is restricted in the presence of differently-optimized comdat functions. But we don't do that anyway (currently). Can we think of an example where this matters for something we currently do (readonly, nocapture, etc.)?

Thanks again,
Hal

> 
> -- Sanjoy
> 

-- 
Hal Finkel
Assistant Computational Scientist
Leadership Computing Facility
Argonne National Laboratory