llvm dev - Mar 2015 - [LLVMdev] Question: Motivation of the semantics of the undefined value?

Dear LLVMdev,

We have a question regarding the semantics of the undefined value in LLVM
IR.

As far as we understand, in order to give a semantics to the undefined
value, the semantics of LLVM IR is generalized to a rather unusual
set-based semantics. More specifically, the notion of value in LLVM IR is
generalized to a set of values, rather than a single value. Then the
undefined value is simply defined as the set of all values.

Our question is simply why LLVM does not use the notion of trap
representation of C11 standard to represent the undefined value, rather
than using the set-based semantics.

We'd like to understand the motivation of the set-based semantics over the
trap representation.

Thanks.
Chung-Kil Hur, Steve Zdancewic & Viktor Vafeiadis.
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20150317/fa236059/attachment.html>

A trap representation prevents hoisting operations over control flow.
For instance, if we defined reading uninitialized memory to trap, then
we could not transform

  %t = alloca
  call void @escape(%t)
  loop n times {
    %m = load %t
    use(%m)
  }

to

  %t = alloca
  call void @escape(%t)
  %m = load %t
  loop n times {
   use(%m)
  }

since if n was 0 and @escape did not initialize %t, we would have
introduced a trap that was not present in the original program.

On Mon, Mar 16, 2015 at 8:49 AM, Chung-Kil Hur <gil.hur at sf.snu.ac.kr>
wrote:
> Dear LLVMdev,
>
> We have a question regarding the semantics of the undefined value in LLVM
> IR.
>
> As far as we understand, in order to give a semantics to the undefined
> value, the semantics of LLVM IR is generalized to a rather unusual
set-based
> semantics. More specifically, the notion of value in LLVM IR is generalized
> to a set of values, rather than a single value. Then the undefined value is
> simply defined as the set of all values.
>
> Our question is simply why LLVM does not use the notion of trap
> representation of C11 standard to represent the undefined value, rather
than
> using the set-based semantics.
>
> We'd like to understand the motivation of the set-based semantics over
the
> trap representation.
>
> Thanks.
> Chung-Kil Hur, Steve Zdancewic & Viktor Vafeiadis.
>
>
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>

Dear Sanjoy Das,

I can see the point.
Thanks a lot for the instructive example.

Best,
Chung-Kil Hur

On Tue, Mar 17, 2015 at 4:29 AM, Sanjoy Das <sanjoy at
playingwithpointers.com>
wrote:
> A trap representation prevents hoisting operations over control flow.
> For instance, if we defined reading uninitialized memory to trap, then
> we could not transform
>
>   %t = alloca
>   call void @escape(%t)
>   loop n times {
>     %m = load %t
>     use(%m)
>   }
>
> to
>
>   %t = alloca
>   call void @escape(%t)
>   %m = load %t
>   loop n times {
>    use(%m)
>   }
>
> since if n was 0 and @escape did not initialize %t, we would have
> introduced a trap that was not present in the original program.
>
> On Mon, Mar 16, 2015 at 8:49 AM, Chung-Kil Hur <gil.hur at
sf.snu.ac.kr>
> wrote:
> > Dear LLVMdev,
> >
> > We have a question regarding the semantics of the undefined value in
LLVM
> > IR.
> >
> > As far as we understand, in order to give a semantics to the undefined
> > value, the semantics of LLVM IR is generalized to a rather unusual
> set-based
> > semantics. More specifically, the notion of value in LLVM IR is
> generalized
> > to a set of values, rather than a single value. Then the undefined
value
> is
> > simply defined as the set of all values.
> >
> > Our question is simply why LLVM does not use the notion of trap
> > representation of C11 standard to represent the undefined value,
rather
> than
> > using the set-based semantics.
> >
> > We'd like to understand the motivation of the set-based semantics
over
> the
> > trap representation.
> >
> > Thanks.
> > Chung-Kil Hur, Steve Zdancewic & Viktor Vafeiadis.
> >
> >
> > _______________________________________________
> > LLVM Developers mailing list
> > LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> > http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20150317/9afcc492/attachment.html>