how many of those things could be modeled by dependent types so that we’d
still be able to get the optimizations? we’d statically know if we’ve
dereferenced null, or if we’ve not 0’d out a memory allocation, etc.?
All these can certainly be modeled. The real point is whether someone is
willing to
go through the trouble to make sure that ‘undefined behavior’ is not relied
upon.On Friday, March 14, 2014 4:37:13 PM UTC-4, Raoul Duke wrote:
What Every C Programmer Should Know About Undefined Behavior #1/3 - The LLVM Project Blog
how many of those things could be modeled by dependent types so that we’d
still be able to get the optimizations? we’d statically know if we’ve
dereferenced null, or if we’ve not 0’d out a memory allocation, etc.?
I’m pretty sure that all of these are handled in ATS2 by linear or
dependent types, but there is one I’m not sure about.
It is possible I’ve gotten the categorizations wrong but this is my
understanding:
dependent:
*Signed integer overflow *
Dereferencing a NULL Pointer
linear:
Violating Type Rules (e.g. use castfn in ATS2 where appropriate, and use
the correct views)
Use of an uninitialized variable
linear or dependent:
*Dereferences of Wild Pointers and Out of Bounds Array Accesses *
other:
Oversized Shift Amount (I’m not sure about this one, but it seems that it
is possible to do this safely, if not necessarily as efficiently as doing
it unsafely. But I think dependent types could be used to do this safely,
as you just define the shift amount as a size < 32).
Brandon Barker
brandon…@gmail.comOn Fri, Mar 14, 2014 at 4:37 PM, Raoul Duke rao...@gmail.com wrote:
What Every C Programmer Should Know About Undefined Behavior #1/3 - The LLVM Project Blog
how many of those things could be modeled by dependent types so that we’d
still be able to get the optimizations? we’d statically know if we’ve
dereferenced null, or if we’ve not 0’d out a memory allocation, etc.?–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/07233cfe-e517-4e3d-ae2a-07413023b033%40googlegroups.comhttps://groups.google.com/d/msgid/ats-lang-users/07233cfe-e517-4e3d-ae2a-07413023b033%40googlegroups.com?utm_medium=email&utm_source=footer
.