ATS and Clang-3.5

Note that works as expected if you change “int” to “volatile int”.

-GregOn Tue, Jan 27, 2015 at 10:43 PM, Greg Fitzgerald gar...@gmail.com wrote:

Yep, still looks like a clang bug to me. I’ll keep digging.

-Greg

On Tue, Jan 27, 2015 at 10:11 PM, gmhwxi gmh...@gmail.com wrote:

Please try (clang -O1) and (clang -O2) on the following code:

#include <stdio.h>
#include <stdlib.h>
#include <setjmp.h>

static jmp_buf buf;

void
second(int *p) {
*p = 1000000;
printf(“second: *p = %i\n”, *p);
longjmp(buf,1); // jumps back to where setjmp was called -
making setjmp now return 1
}

void
first(int *p) {
second(p);
printf(“first\n”); // does not print
}

int main() {
/*
int x = 0;
*/
int p;
p = malloc(sizeof(int));
/

printf(“main: p = %p\n”, p);
*/
if (p == 0)
{
fprintf (stderr, “malloc: failed!\n”); exit(1);
}

*p = 0;

if (!setjmp(buf) ) {
first(p); // when executed, setjmp returns 0
} else { // when longjmp jumps back, setjmp returns 1
printf(“main: *p = %i\n”, *p); // prints
}
return 0;
}

On Wednesday, January 28, 2015 at 12:59:15 AM UTC-5, gmhwxi wrote:

I thought that I had understood the issue; I apparently did not.

“”“”
All accessible objects have values, and all other components of the
abstract
machine have state, as of the time the longjmp function was called, except
that the
values of objects of automatic storage duration that are local to the
function containing
the invocation of the corresponding setjmp macro that do not have
volatile-qualified type
and have been changed between the setjmp invocation and longjmp call are
indeterminate.
“”“”

If you use (clang -O1) to compile the following code and then execute the
generate object code,
you should get:

second
main: x = 1000000

If you use (clang -O2), you should get

second
main: x = 0

I understood this behavior: the value in x is really indeterminate; either
0 or 1000000 is okay.

What I do not understand is that you get the same results even if x is
heap-allocated. This does
not follow from the above description: if x is heap-allocated, it is
considered a state; so its content
should not be indeterminate. Right?

#include <stdio.h>
#include <setjmp.h>

static jmp_buf buf;

void
second(int *p) {
*p = 1000000;
printf(“second\n”); // prints
longjmp(buf,1); // jumps back to where setjmp was called -
making setjmp now return 1
}

void
first(int *p) {
second(p);
printf(“first\n”); // does not print
}

int main() {
int x = 0;
if (!setjmp(buf) ) {
first(&x); // when executed, setjmp returns 0
} else { // when longjmp jumps back, setjmp returns 1
printf(“main: x = %i\n”, x); // prints
}
return 0;
}

On Tuesday, January 27, 2015 at 7:30:59 PM UTC-5, Greg Fitzgerald wrote:

From Reid Kleckner:

So this is almost undoubtedly a setjmp issue. Relevant C standard quote
[7.13.2.1 p5]:

“”"
All accessible objects have values, and all other components of the
abstract
machine249)
have state, as of the time the longjmp function was called, except that
the
values of
objects of automatic storage duration that are local to the function
containing
the
invocation of the corresponding setjmp macro that do not have
volatile-qualified type
and have been changed between the setjmp invocation and longjmp call are
indeterminate.
“”"

As the variable tmp502 is not declared volatile, its value is
indeterminate. I
think this is working as intended with nothing to do in LLVM.

On Tue, Jan 27, 2015 at 2:49 PM, Greg Fitzgerald gar...@gmail.com wrote:

Thanks for doing that work to ensure is in clang and not in
ATS-generated code. I opened a discussion on the llvmdev email list
and added a bug report at llvm.org:

http://llvm.org/bugs/show_bug.cgi?id=22360

I’ll keep you posted on progress. Feel free to jump in on the
discussion.

-Greg

On Tue, Jan 27, 2015 at 12:11 AM, Hongwei Xi gmh...@gmail.com wrote:

I finally found a way to circumvent the problem.

The following code is taken from:

https://github.com/githwxi/ATS-Postiats/blob/master/src/pats_lintprgm.dats

implement{a}
myintvec_cffgcd
{n}(iv, n) = let
//
var res
: myint(a) = myint_make_int (0)
val p_res = &res
//
// HX-2015-01-27:
// fixing a bug in (clang-3.5 -O2)
//
// HX: a dummy to force clang
// not to optimize the value stored in [res]
val ((void)) = ptr_as_volatile(p_res)
//

If the call to ptr_as_volatile is removed, then clang-3.5
may use the (linear) value in [res] repeatedly, causing this
value to be freed more than once.

The C code is attached. Searching for ‘pats_as_volatile’ should lead
you to the spot where the bug occurs.

On Tue, Jan 27, 2015 at 12:36 AM, Greg Fitzgerald gar...@gmail.com wrote:

As I see it, the chance of fixing such a bug is really next to
none.

Fixing clang 3.4 or 3.5? That sounds accurate. But if we move
quickly we might be able to squeeze a fix into 3.6. Can you send me
an isolated C fragment.

Thanks,
Greg

On Mon, Jan 26, 2015 at 5:58 PM, Hongwei Xi gmh...@gmail.com wrote:

I followed your suggestions.

There were 22M bytes of leaks reported (-fsanitize=address)
There were no undefined behaviors reported (-fsanitize=undefined)

Leaks are expected because I turned off GC.

As I see it, the chance of fixing such a bug is really next to
none.

On Mon, Jan 26, 2015 at 8:18 PM, Greg Fitzgerald gar...@gmail.com wrote:

Today, I noted that neither (Clang-3.4 -O2) nor (Clang-3.5 -O2)
can
succeed in
compiling ATS2. The patsopt generated by these compilers crashes
immediately.

It is expected for this class of error to occur if ATS2 depends on
undefined behavior. For example, if you use memcpy() instead of
memset() to copy overlapping regions, then bumping up to -O2 may
pull
in a vectorized version, which could manifest itself as a memory
corruption. To weed out runtime instances of undefined behavior,
compile and link your code with “-fsanitize=undefined”, and then
run
‘patsopt’ from the command-line. If undefined behavior is
detected,
the runtime will report an error message on stderr.

Another useful one is “-fsanitze=address”, which is used the same
way.
Just before segfaulting, it should spit out a stack trace of where
the
memory violation occurred. That might solve your problem as well,
but
for this particular case (upgrading the compiler or enabling more
optimizations) checking for undefined behavior first should be
better
for determining the root cause.

-Greg

On Mon, Jan 26, 2015 at 4:05 PM, gmhwxi gmh...@gmail.com wrote:

FYI.

I once used (Clang-3.2 -O2) to compile ATS2 successfully.

Today, I noted that neither (Clang-3.4 -O2) nor (Clang-3.5 -O2)
can
succeed
in
compiling ATS2. The patsopt generated by these compilers crashes
immediately.
However, (Clang-3.5 -O1) can do it. So it is very suspicious
that new
optimizations
added into Clang-3.4 and Clang-3.5 were the cause of this
failure.
This
is a
very
unfortunate situation!

For now, (Gcc-4.8 -O2) is the only optimizing compiler that can
compile
ATS2.


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...@googlegroups.com.
To post to this group, send email to
ats-l...@googlegroups.com.
Visit this group at
http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/0489dc9f-652e-4a55-aa6e-030ac740561d%40googlegroups.com.


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...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAFLa5WPNvjUJvP_CEnW0Xyytc%2BwHPUjKC_MqT-4JN1YU6VfYXg%40mail.gmail.com.


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...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLpbNS6O%2B8doygqooiuejHnYCQ76CjmZt%3DoWodUX0quaug%40mail.gmail.com.


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...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAFLa5WM-UbGtk%3DVataT-gqzZTfTKrDFB4NxvRvuaYE5x9QNWoQ%40mail.gmail.com.


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...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLph8gEqH-4PHYWMPqg6xpp07s0i6JcCE3_1g9%3DteL69uQ%40mail.gmail.com.


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.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/83e98e70-e320-4d7d-8776-5a6fa2804b94%40googlegroups.com.

Thanks!

I would really like to understand the issue.

As the variable tmp502 is not declared volatile, its value is
indeterminate

When is it indeterminate? During the longjmp phase?

Why does it matter whether it is indeterminate or not? It is not used
during the
longjmp phase.On Tuesday, January 27, 2015 at 7:30:59 PM UTC-5, Greg Fitzgerald wrote:

From Reid Kleckner:

So this is almost undoubtedly a setjmp issue. Relevant C standard quote
[7.13.2.1 p5]:

“”"
All accessible objects have values, and all other components of the
abstract
machine249)
have state, as of the time the longjmp function was called, except that
the
values of
objects of automatic storage duration that are local to the function
containing
the
invocation of the corresponding setjmp macro that do not have
volatile-qualified type
and have been changed between the setjmp invocation and longjmp call are
indeterminate.
“”"

As the variable tmp502 is not declared volatile, its value is
indeterminate. I
think this is working as intended with nothing to do in LLVM.

On Tue, Jan 27, 2015 at 2:49 PM, Greg Fitzgerald <gar...@gmail.com <javascript:>> wrote:

Thanks for doing that work to ensure is in clang and not in
ATS-generated code. I opened a discussion on the llvmdev email list
and added a bug report at llvm.org:

http://llvm.org/bugs/show_bug.cgi?id=22360

I’ll keep you posted on progress. Feel free to jump in on the
discussion.

-Greg

On Tue, Jan 27, 2015 at 12:11 AM, Hongwei Xi <gmh...@gmail.com <javascript:>> wrote:

I finally found a way to circumvent the problem.

The following code is taken from:

https://github.com/githwxi/ATS-Postiats/blob/master/src/pats_lintprgm.dats

implement{a}
myintvec_cffgcd
{n}(iv, n) = let
//
var res
: myint(a) = myint_make_int (0)
val p_res = &res
//
// HX-2015-01-27:
// fixing a bug in (clang-3.5 -O2)
//
// HX: a dummy to force clang
// not to optimize the value stored in [res]
val ((void)) = ptr_as_volatile(p_res)
//

If the call to ptr_as_volatile is removed, then clang-3.5
may use the (linear) value in [res] repeatedly, causing this
value to be freed more than once.

The C code is attached. Searching for ‘pats_as_volatile’ should lead
you to the spot where the bug occurs.

On Tue, Jan 27, 2015 at 12:36 AM, Greg Fitzgerald <gar...@gmail.com <javascript:>> wrote:

As I see it, the chance of fixing such a bug is really next to none.

Fixing clang 3.4 or 3.5? That sounds accurate. But if we move
quickly we might be able to squeeze a fix into 3.6. Can you send me
an isolated C fragment.

Thanks,
Greg

On Mon, Jan 26, 2015 at 5:58 PM, Hongwei Xi <gmh...@gmail.com <javascript:>> wrote:

I followed your suggestions.

There were 22M bytes of leaks reported (-fsanitize=address)
There were no undefined behaviors reported (-fsanitize=undefined)

Leaks are expected because I turned off GC.

As I see it, the chance of fixing such a bug is really next to none.

On Mon, Jan 26, 2015 at 8:18 PM, Greg Fitzgerald <gar...@gmail.com <javascript:>> wrote:

Today, I noted that neither (Clang-3.4 -O2) nor (Clang-3.5 -O2)
can
succeed in
compiling ATS2. The patsopt generated by these compilers crashes
immediately.

It is expected for this class of error to occur if ATS2 depends on
undefined behavior. For example, if you use memcpy() instead of
memset() to copy overlapping regions, then bumping up to -O2 may
pull
in a vectorized version, which could manifest itself as a memory
corruption. To weed out runtime instances of undefined behavior,
compile and link your code with “-fsanitize=undefined”, and then
run
‘patsopt’ from the command-line. If undefined behavior is
detected,
the runtime will report an error message on stderr.

Another useful one is “-fsanitze=address”, which is used the same
way.
Just before segfaulting, it should spit out a stack trace of where
the
memory violation occurred. That might solve your problem as well,
but
for this particular case (upgrading the compiler or enabling more
optimizations) checking for undefined behavior first should be
better
for determining the root cause.

-Greg

On Mon, Jan 26, 2015 at 4:05 PM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

FYI.

I once used (Clang-3.2 -O2) to compile ATS2 successfully.

Today, I noted that neither (Clang-3.4 -O2) nor (Clang-3.5 -O2)
can
succeed
in
compiling ATS2. The patsopt generated by these compilers crashes
immediately.
However, (Clang-3.5 -O1) can do it. So it is very suspicious that
new
optimizations
added into Clang-3.4 and Clang-3.5 were the cause of this
failure.
This
is a
very
unfortunate situation!

For now, (Gcc-4.8 -O2) is the only optimizing compiler that can
compile
ATS2.


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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/0489dc9f-652e-4a55-aa6e-030ac740561d%40googlegroups.com.


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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAFLa5WPNvjUJvP_CEnW0Xyytc%2BwHPUjKC_MqT-4JN1YU6VfYXg%40mail.gmail.com.


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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLpbNS6O%2B8doygqooiuejHnYCQ76CjmZt%3DoWodUX0quaug%40mail.gmail.com.


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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAFLa5WM-UbGtk%3DVataT-gqzZTfTKrDFB4NxvRvuaYE5x9QNWoQ%40mail.gmail.com.


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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLph8gEqH-4PHYWMPqg6xpp07s0i6JcCE3_1g9%3DteL69uQ%40mail.gmail.com.

I finally found a way to circumvent the problem.

The following code is taken from:

implement{a}

myintvec_cffgcd
{n}(iv, n) = let
//
var res
: myint(a) = myint_make_int (0)
val p_res = &res
//
// HX-2015-01-27:
// fixing a bug in (clang-3.5 -O2)
//
// HX: a dummy to force clang
// not to optimize the value stored in [res]
val ((void)) = ptr_as_volatile(p_res)
//

If the call to ptr_as_volatile is removed, then clang-3.5
may use the (linear) value in [res] repeatedly, causing this
value to be freed more than once.

The C code is attached. Searching for ‘pats_as_volatile’ should lead
you to the spot where the bug occurs.On Tue, Jan 27, 2015 at 12:36 AM, Greg Fitzgerald
gar...@gmail.com wrote:

As I see it, the chance of fixing such a bug is really next to none.

Fixing clang 3.4 or 3.5? That sounds accurate. But if we move
quickly we might be able to squeeze a fix into 3.6. Can you send me
an isolated C fragment.

Thanks,
Greg

On Mon, Jan 26, 2015 at 5:58 PM, Hongwei Xi gmh...@gmail.com wrote:

I followed your suggestions.

There were 22M bytes of leaks reported (-fsanitize=address)
There were no undefined behaviors reported (-fsanitize=undefined)

Leaks are expected because I turned off GC.

As I see it, the chance of fixing such a bug is really next to none.

On Mon, Jan 26, 2015 at 8:18 PM, Greg Fitzgerald gar...@gmail.com wrote:

Today, I noted that neither (Clang-3.4 -O2) nor (Clang-3.5 -O2) can
succeed in
compiling ATS2. The patsopt generated by these compilers crashes
immediately.

It is expected for this class of error to occur if ATS2 depends on
undefined behavior. For example, if you use memcpy() instead of
memset() to copy overlapping regions, then bumping up to -O2 may pull
in a vectorized version, which could manifest itself as a memory
corruption. To weed out runtime instances of undefined behavior,
compile and link your code with “-fsanitize=undefined”, and then run
‘patsopt’ from the command-line. If undefined behavior is detected,
the runtime will report an error message on stderr.

Another useful one is “-fsanitze=address”, which is used the same way.
Just before segfaulting, it should spit out a stack trace of where the
memory violation occurred. That might solve your problem as well, but
for this particular case (upgrading the compiler or enabling more
optimizations) checking for undefined behavior first should be better
for determining the root cause.

-Greg

On Mon, Jan 26, 2015 at 4:05 PM, gmhwxi gmh...@gmail.com wrote:

FYI.

I once used (Clang-3.2 -O2) to compile ATS2 successfully.

Today, I noted that neither (Clang-3.4 -O2) nor (Clang-3.5 -O2) can
succeed
in
compiling ATS2. The patsopt generated by these compilers crashes
immediately.
However, (Clang-3.5 -O1) can do it. So it is very suspicious that new
optimizations
added into Clang-3.4 and Clang-3.5 were the cause of this failure.
This
is a
very
unfortunate situation!

For now, (Gcc-4.8 -O2) is the only optimizing compiler that can
compile
ATS2.


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.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/0489dc9f-652e-4a55-aa6e-030ac740561d%40googlegroups.com
.


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.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAFLa5WPNvjUJvP_CEnW0Xyytc%2BwHPUjKC_MqT-4JN1YU6VfYXg%40mail.gmail.com
.


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.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLpbNS6O%2B8doygqooiuejHnYCQ76CjmZt%3DoWodUX0quaug%40mail.gmail.com
.


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.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAFLa5WM-UbGtk%3DVataT-gqzZTfTKrDFB4NxvRvuaYE5x9QNWoQ%40mail.gmail.com
.

pats_constraint3_solve_dats.c (261 KB)

Or, of course, the variable could live in a register that is simply not restored if it’s not volatile.> On Jan 28, 2015, at 5:36 PM, Shea Levy sh...@shealevy.com wrote:

It’s not even const, but either way the standard is clear here that non-volatile stack variables are indeterminate.

I am not at all experienced enough to know how this kind of thing is actually implemented, but I could imagine for example a setjmp/longjmp impl that ran longjmp in an entirely new stack frame, with only the volatile variables copied from before. Or one that filled the stack with garbage first.

On Jan 28, 2015, at 5:31 PM, gmhwxi <gmh...@gmail.com mailto:gmh...@gmail.com> wrote:

But p is unchanged; it is a const; so it should be determinate, I think.

On Wednesday, January 28, 2015 at 12:15:18 PM UTC-5, Shea Levy wrote:
Note that in this case, the printf is undefined behavior: p may point to the heap, but p itself is on the stack and thus indeterminate.

On Jan 28, 2015, at 6:11 AM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

Please try (clang -O1) and (clang -O2) on the following code:

#include <stdio.h>
#include <stdlib.h>
#include <setjmp.h>

static jmp_buf buf;

void
second(int *p) {
*p = 1000000;
printf(“second: *p = %i\n”, *p);
longjmp(buf,1); // jumps back to where setjmp was called - making setjmp now return 1
}

void
first(int *p) {
second(p);
printf(“first\n”); // does not print
}

int main() {
/*
int x = 0;
*/
int p;
p = malloc(sizeof(int));
/

printf(“main: p = %p\n”, p);
*/
if (p == 0)
{
fprintf (stderr, “malloc: failed!\n”); exit(1);
}

*p = 0;

if (!setjmp(buf) ) {
first(p); // when executed, setjmp returns 0
} else { // when longjmp jumps back, setjmp returns 1
printf(“main: *p = %i\n”, *p); // prints
}
return 0;
}

On Wednesday, January 28, 2015 at 12:59:15 AM UTC-5, gmhwxi wrote:
I thought that I had understood the issue; I apparently did not.

“”“”
All accessible objects have values, and all other components of the abstract
machine have state, as of the time the longjmp function was called, except that the
values of objects of automatic storage duration that are local to the function containing
the invocation of the corresponding setjmp macro that do not have volatile-qualified type
and have been changed between the setjmp invocation and longjmp call are
indeterminate.
“”“”

If you use (clang -O1) to compile the following code and then execute the generate object code,
you should get:

second
main: x = 1000000

If you use (clang -O2), you should get

second
main: x = 0

I understood this behavior: the value in x is really indeterminate; either 0 or 1000000 is okay.

What I do not understand is that you get the same results even if x is heap-allocated. This does
not follow from the above description: if x is heap-allocated, it is considered a state; so its content
should not be indeterminate. Right?

#include <stdio.h>
#include <setjmp.h>

static jmp_buf buf;

void
second(int *p) {
*p = 1000000;
printf(“second\n”); // prints
longjmp(buf,1); // jumps back to where setjmp was called - making setjmp now return 1
}

void
first(int *p) {
second(p);
printf(“first\n”); // does not print
}

int main() {
int x = 0;
if (!setjmp(buf) ) {
first(&x); // when executed, setjmp returns 0
} else { // when longjmp jumps back, setjmp returns 1
printf(“main: x = %i\n”, x); // prints
}
return 0;
}

On Tuesday, January 27, 2015 at 7:30:59 PM UTC-5, Greg Fitzgerald wrote:
From Reid Kleckner:

So this is almost undoubtedly a setjmp issue. Relevant C standard quote
[7.13.2.1 p5]:

“”"
All accessible objects have values, and all other components of the abstract
machine249)
have state, as of the time the longjmp function was called, except that the
values of
objects of automatic storage duration that are local to the function containing
the
invocation of the corresponding setjmp macro that do not have
volatile-qualified type
and have been changed between the setjmp invocation and longjmp call are
indeterminate.
“”"

As the variable tmp502 is not declared volatile, its value is indeterminate. I
think this is working as intended with nothing to do in LLVM.

On Tue, Jan 27, 2015 at 2:49 PM, Greg Fitzgerald <gar...@gmail.com <>> wrote:

Thanks for doing that work to ensure is in clang and not in
ATS-generated code. I opened a discussion on the llvmdev email list
and added a bug report at llvm.org http://llvm.org/:

http://llvm.org/bugs/show_bug.cgi?id=22360 http://llvm.org/bugs/show_bug.cgi?id=22360

I’ll keep you posted on progress. Feel free to jump in on the discussion.

-Greg

On Tue, Jan 27, 2015 at 12:11 AM, Hongwei Xi <gmh...@gmail.com <>> wrote:

I finally found a way to circumvent the problem.

The following code is taken from:

https://github.com/githwxi/ATS-Postiats/blob/master/src/pats_lintprgm.dats https://github.com/githwxi/ATS-Postiats/blob/master/src/pats_lintprgm.dats

implement{a}
myintvec_cffgcd
{n}(iv, n) = let
//
var res
: myint(a) = myint_make_int (0)
val p_res = &res
//
// HX-2015-01-27:
// fixing a bug in (clang-3.5 -O2)
//
// HX: a dummy to force clang
// not to optimize the value stored in [res]
val ((void)) = ptr_as_volatile(p_res)
//

If the call to ptr_as_volatile is removed, then clang-3.5
may use the (linear) value in [res] repeatedly, causing this
value to be freed more than once.

The C code is attached. Searching for ‘pats_as_volatile’ should lead
you to the spot where the bug occurs.

On Tue, Jan 27, 2015 at 12:36 AM, Greg Fitzgerald <gar...@gmail.com <>> wrote:

As I see it, the chance of fixing such a bug is really next to none.

Fixing clang 3.4 or 3.5? That sounds accurate. But if we move
quickly we might be able to squeeze a fix into 3.6. Can you send me
an isolated C fragment.

Thanks,
Greg

On Mon, Jan 26, 2015 at 5:58 PM, Hongwei Xi <gmh...@gmail.com <>> wrote:

I followed your suggestions.

There were 22M bytes of leaks reported (-fsanitize=address)
There were no undefined behaviors reported (-fsanitize=undefined)

Leaks are expected because I turned off GC.

As I see it, the chance of fixing such a bug is really next to none.

On Mon, Jan 26, 2015 at 8:18 PM, Greg Fitzgerald <gar...@gmail.com <>> wrote:

Today, I noted that neither (Clang-3.4 -O2) nor (Clang-3.5 -O2) can
succeed in
compiling ATS2. The patsopt generated by these compilers crashes
immediately.

It is expected for this class of error to occur if ATS2 depends on
undefined behavior. For example, if you use memcpy() instead of
memset() to copy overlapping regions, then bumping up to -O2 may pull
in a vectorized version, which could manifest itself as a memory
corruption. To weed out runtime instances of undefined behavior,
compile and link your code with “-fsanitize=undefined”, and then run
‘patsopt’ from the command-line. If undefined behavior is detected,
the runtime will report an error message on stderr.

Another useful one is “-fsanitze=address”, which is used the same way.
Just before segfaulting, it should spit out a stack trace of where the
memory violation occurred. That might solve your problem as well, but
for this particular case (upgrading the compiler or enabling more
optimizations) checking for undefined behavior first should be better
for determining the root cause.

-Greg

On Mon, Jan 26, 2015 at 4:05 PM, gmhwxi <gmh...@gmail.com <>> wrote:

FYI.

I once used (Clang-3.2 -O2) to compile ATS2 successfully.

Today, I noted that neither (Clang-3.4 -O2) nor (Clang-3.5 -O2) can
succeed
in
compiling ATS2. The patsopt generated by these compilers crashes
immediately.
However, (Clang-3.5 -O1) can do it. So it is very suspicious that new
optimizations
added into Clang-3.4 and Clang-3.5 were the cause of this failure.
This
is a
very
unfortunate situation!

For now, (Gcc-4.8 -O2) is the only optimizing compiler that can
compile
ATS2.


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...@googlegroups.com <>.
To post to this group, send email to ats-l...@googlegroups.com <>.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/0489dc9f-652e-4a55-aa6e-030ac740561d%40googlegroups.com https://groups.google.com/d/msgid/ats-lang-users/0489dc9f-652e-4a55-aa6e-030ac740561d%40googlegroups.com.


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...@googlegroups.com <>.
To post to this group, send email to ats-l...@googlegroups.com <>.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAFLa5WPNvjUJvP_CEnW0Xyytc%2BwHPUjKC_MqT-4JN1YU6VfYXg%40mail.gmail.com https://groups.google.com/d/msgid/ats-lang-users/CAFLa5WPNvjUJvP_CEnW0Xyytc%2BwHPUjKC_MqT-4JN1YU6VfYXg%40mail.gmail.com.


You received this message because you are subscribed to the Google
Groups


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 mailto:ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com mailto:ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/b3219e69-000b-4d50-9db8-4e0abe6fdd36%40googlegroups.com https://groups.google.com/d/msgid/ats-lang-users/b3219e69-000b-4d50-9db8-4e0abe6fdd36%40googlegroups.com?utm_medium=email&utm_source=footer.


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 mailto:ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com mailto:ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/713CC297-B9C2-41FA-A172-1C9361A9B437%40shealevy.com https://groups.google.com/d/msgid/ats-lang-users/713CC297-B9C2-41FA-A172-1C9361A9B437%40shealevy.com?utm_medium=email&utm_source=footer.

So I had a quick chat on the llvm irc channel about this. The general
mood is that setjmp/longjmp is a dirty hack for people trying to get C
to do things that it’s not meant for - exception handling. The
‘volatile’ solution is a hack on hack - a convenient escape hatch that
already existed in the language and could be used by those few people
in the world attempting to hack exception handling into C. While it
sounds like we have a solution, have you considered targeting C++ or
LLVM bitcode instead of C?

Regarding your malloc() example. Since that memory is non-volatile
and the C spec gives itself the space to treat setjmp() as a
subroutine, that constant of 42 would still be propagated to “return
*p” and make it “return 42”. The malloc() would probably stick around
even though it appears dead. That’s because someone may override
malloc() and add side-effects. If you did whole-program optimization,
I’d think the malloc() would get the boot and your program would be
reduced to:

#include <setjmp.h>
int main(int argc, char **argv) {
jmp_buf buf;
if (setjmp(buf))
return 42;
longjmp(buf, 1);
}

-GregOn Thu, Jan 29, 2015 at 1:24 PM, gmhwxi gmh...@gmail.com wrote:

But this is all due to C being a REAL programming language :slight_smile:

On Thursday, January 29, 2015 at 3:39:47 PM UTC-5, Raoul Duke wrote:

All I can (re) learn from this is how much C sucks? If it is this hard
to figure out if something is a bug or not… Sheesh. :-}


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.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/2a67eefe-2b84-43cd-b6c5-e6725d58a319%40googlegroups.com.

But asking programmers to write optimized on their own would be a lot
worse!

I think it is time to ask/find someone to use CompCert to compile ATS2 :slight_smile:

Hi! :smiley:

The documentation says

– begin of quote –
1.4.2 The supported C dialect
Chapter 5 specifies the dialect of the C language that CompCert C accepts
as input language. In summary,
CompCert C supports all of ISO C 99 [4], with the following exceptions:
• switch statements must be structured as in MISRA-C [1]; unstructured
switch, as in Duff’s device,
is not supported.
• Variable-length arrays are not supported.
• longjmp and setjmp are not guaranteed to work.
– end of quote –

So unfortunately, this may not solve the setjmp/longjmp issue.

Also, ./configure seems to recognize the CC environment variable passed
to it, but do not propagate it. I had to manually edit Makefile to change
CCOMP=compcert at three places. Note: the CompCert command’s name is
ccomp, but as this name is used everywhere in ATS build’s source
directory, I created a symbolic compcert to ccomp (to avoid ambiguity).

Actually, it complains about unrecognized option -O2, so I guess there
are other files to me manually edited which ./configure don’t.

I’m going on later, and if I succeed to build Postiat 0.1.8 with CompCert,
I will tell in a thread (and will explain how I did).

I don’t feel that it should be interpreted this way:

“”“”
All accessible objects have values, and all other components of the
abstract
machine have state, as of the time the longjmp function was called, except
that the
values of objects of automatic storage duration that are local to the
function containing
the invocation of the corresponding setjmp macro that do not have
volatile-qualified type
and have been changed between the setjmp invocation and longjmp call are
indeterminate.
“”“”

A constant cannot be changed. This paragraph clearly talks about
left-values (objects).
The purpose of this paragraph is very clear: It tries to shift the
responsibility to the programmer
in case of an “over-optimization”. There is really no other way to do it.

By the way, “indeterminate” is not completely indeterminate. Essentially,
it means that
the compiler may use the value available at the point where longjmp starts
(not optimizing)
or the value saved at the point where setjmp happens (optimizing).On Thursday, January 29, 2015 at 5:35:04 PM UTC-5, Greg Fitzgerald wrote:

On Thu, Jan 29, 2015 at 2:08 PM, Barry Schwartz <chem...@chemoelectric.org <javascript:>> wrote:

I could be convinced otherwise, but it looks to me as if LLVM is being
too aggressive to optimize in the presence of pointers.

It’s an interesting case. It’s not the malloc() to look at, but the
code just after:

*p = 42; 
return *p; 

The compiler can still respect memory by changing it to:

*p = 42; 
return 42; 

That is setjmp() won’t begin until 42 is flushed to memory. However,
the value 42 is very much local. I think constants fit comfortably
into the definition “automatic storage duration that are local to the
function”. You get the same bug using:

*p = argc
return *p;

argc is inlined into the return statement.

-Greg

Linear logic as in Concurrent Clean style Uniqueness Types?

All I can (re) learn from this is how much C sucks? If it is this hard
to figure out if something is a bug or not… Sheesh. :-}

My current concern is this one:

#include <stdlib.h>
#include <setjmp.h>
int main(int argc, char **argv) {
int *p;
p = malloc(sizeof(int));
*p = 42;
jmp_buf buf;
if (setjmp(buf))
return *p;
*p = 13;
longjmp(buf, 1);
}

Try

clang abcde.c; ./a.out; echo $? // should see 13
clang -O2 abcde.c; ./a.out; echo $? // should see 42

My current understanding is that this is a BUG.On Thursday, January 29, 2015 at 3:12:20 PM UTC-5, Barry Schwartz wrote:

‘Reid Kleckner’ via ats-lang-users <ats-l...@googlegroups.com
<javascript:>> skribis:

tmp502 is indeterminate after the longjmp. Consider this small
example:

#include <setjmp.h>
int main(int argc, char **argv) {
int x = 42;
jmp_buf buf;
if (setjmp(buf))
return x;
x = 13;
longjmp(buf, 1);
}

This certainly satisfies the criterion that the value of x be changed.

LLVM immediately optimizes it to this:

#include <setjmp.h>
int main(int argc, char **argv) {
jmp_buf buf;
if (setjmp(buf))
return 42; // ‘x = 42’ dominates ‘return x’, x does not escape, so
setjmp cannot modify it, constant propagate
// x = 13; // dead, no one uses x after this.
longjmp(buf, 1); // noreturn, control ends here
}

This looks valid to me, in that if you did not have the ‘x=13’
statement the function would always return the unchanged (and
therefore supposedly determinate) value 42.

I’d have to study tmp502 to see what is going on with that.

http://conal.net/blog/posts/the-c-language-is-purely-functional

While it was an amusing moment, it did force me to think about
how functional programming can be implemented without GC support.

regions? reference counting?

By using gdb, I first guessed that this was due to the compilation of
a file of the name “pats_constraint_solve.dats”. So I did the following:

  1. Compiling pats_constraint_solve.dats using (gcc-4.8 -O2)
  2. Compiling the rest using (clang-3.5 -O2)

It actually worked!

So the good news is that this issue seems to be contained in one single
file.On Mon, Jan 26, 2015 at 7:05 PM, gmhwxi gmh...@gmail.com wrote:

FYI.

I once used (Clang-3.2 -O2) to compile ATS2 successfully.

Today, I noted that neither (Clang-3.4 -O2) nor (Clang-3.5 -O2) can
succeed in
compiling ATS2. The patsopt generated by these compilers crashes
immediately.
However, (Clang-3.5 -O1) can do it. So it is very suspicious that new
optimizations
added into Clang-3.4 and Clang-3.5 were the cause of this failure. This is
a very
unfortunate situation!

For now, (Gcc-4.8 -O2) is the only optimizing compiler that can compile
ATS2.


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.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/0489dc9f-652e-4a55-aa6e-030ac740561d%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/0489dc9f-652e-4a55-aa6e-030ac740561d%40googlegroups.com?utm_medium=email&utm_source=footer
.

Should have added this as well:

While it was an amusing moment, it did force me to think about
how functional programming can be implemented without GC support.On Thursday, January 29, 2015 at 7:40:41 PM UTC-5, gmhwxi wrote:

Conal Elliot :slight_smile:

He and I had the same PhD adviser.

I haven’t met him for at least 12 years. When I met him last time,
he was giving a talk on FRP in Haskell. During the talk, he gave a demo
involving animation. I still remember this vividly: the animation stopped
somewhere in the middle because GC just kicked in :slight_smile:

On Thursday, January 29, 2015 at 6:48:00 PM UTC-5, Raoul Duke wrote:

Conal Elliott » The C language is purely functional

But perhaps this is exactly what the sanitize=undefined is for

Yes, exactly.

so maybe clang could have longjmp somehow put traps in all non-volatile stack variables.
But I don’t know how the sanitization stuff is even implemented so this might be nonsense :slight_smile:

Not nonsense. That’d be a nice contribution to make. If you’re
interested in implementing it:

http://llvm.org/docs/GettingStarted.html#git-mirror

-GregOn Tue, Jan 27, 2015 at 7:54 PM, Shea Levy sh...@shealevy.com wrote:

I would guess that finding a violation of this rule would be very expensive
for the compiler while relying on this rule being followed results in real
optimizations. llvm has put a lot of emphasis on fast compilation times.

But perhaps this is exactly what the sanitize=undefined is for, so maybe
clang could have longjmp somehow put traps in all non-volatile stack
variables. But I don’t know how the sanitization stuff is even implemented
so this might be nonsense :slight_smile:

~Shea

On Jan 28, 2015, at 3:50 AM, gmhwxi gmh...@gmail.com wrote:

Why does it matter whether it is indeterminate or not? It is not used
during the
longjmp phase.

I just noticed that this is not true. It is used as the return value of the
function call.

I strongly suggest that this (reading from a variable holding indeterminate
value)
be reported by clang as an undefined behavior. Having a rule in the standard
is one thing.
Pointing out violations of this rule is another.

–Hongwei

PS: I went ahead to remove the use of exception in my code in this case (and
thus
requiring no setjmp/longjmp). Everything is smooth so far. It is a great
feeling.

On Tuesday, January 27, 2015 at 9:29:03 PM UTC-5, gmhwxi wrote:

Thanks!

I would really like to understand the issue.

As the variable tmp502 is not declared volatile, its value is
indeterminate

When is it indeterminate? During the longjmp phase?

Why does it matter whether it is indeterminate or not? It is not used
during the
longjmp phase.

On Tuesday, January 27, 2015 at 7:30:59 PM UTC-5, Greg Fitzgerald wrote:

From Reid Kleckner:

So this is almost undoubtedly a setjmp issue. Relevant C standard quote
[7.13.2.1 p5]:

“”"
All accessible objects have values, and all other components of the
abstract
machine249)
have state, as of the time the longjmp function was called, except that
the
values of
objects of automatic storage duration that are local to the function
containing
the
invocation of the corresponding setjmp macro that do not have
volatile-qualified type
and have been changed between the setjmp invocation and longjmp call are
indeterminate.
“”"

As the variable tmp502 is not declared volatile, its value is
indeterminate. I
think this is working as intended with nothing to do in LLVM.

On Tue, Jan 27, 2015 at 2:49 PM, Greg Fitzgerald gar...@gmail.com wrote:

Thanks for doing that work to ensure is in clang and not in
ATS-generated code. I opened a discussion on the llvmdev email list
and added a bug report at llvm.org:

http://llvm.org/bugs/show_bug.cgi?id=22360

I’ll keep you posted on progress. Feel free to jump in on the
discussion.

-Greg

On Tue, Jan 27, 2015 at 12:11 AM, Hongwei Xi gmh...@gmail.com wrote:

I finally found a way to circumvent the problem.

The following code is taken from:

https://github.com/githwxi/ATS-Postiats/blob/master/src/pats_lintprgm.dats

implement{a}
myintvec_cffgcd
{n}(iv, n) = let
//
var res
: myint(a) = myint_make_int (0)
val p_res = &res
//
// HX-2015-01-27:
// fixing a bug in (clang-3.5 -O2)
//
// HX: a dummy to force clang
// not to optimize the value stored in [res]
val ((void)) = ptr_as_volatile(p_res)
//

If the call to ptr_as_volatile is removed, then clang-3.5
may use the (linear) value in [res] repeatedly, causing this
value to be freed more than once.

The C code is attached. Searching for ‘pats_as_volatile’ should lead
you to the spot where the bug occurs.

On Tue, Jan 27, 2015 at 12:36 AM, Greg Fitzgerald gar...@gmail.com wrote:

As I see it, the chance of fixing such a bug is really next to
none.

Fixing clang 3.4 or 3.5? That sounds accurate. But if we move
quickly we might be able to squeeze a fix into 3.6. Can you send me
an isolated C fragment.

Thanks,
Greg

On Mon, Jan 26, 2015 at 5:58 PM, Hongwei Xi gmh...@gmail.com wrote:

I followed your suggestions.

There were 22M bytes of leaks reported (-fsanitize=address)
There were no undefined behaviors reported (-fsanitize=undefined)

Leaks are expected because I turned off GC.

As I see it, the chance of fixing such a bug is really next to
none.

On Mon, Jan 26, 2015 at 8:18 PM, Greg Fitzgerald gar...@gmail.com wrote:

Today, I noted that neither (Clang-3.4 -O2) nor (Clang-3.5 -O2)
can
succeed in
compiling ATS2. The patsopt generated by these compilers crashes
immediately.

It is expected for this class of error to occur if ATS2 depends on
undefined behavior. For example, if you use memcpy() instead of
memset() to copy overlapping regions, then bumping up to -O2 may
pull
in a vectorized version, which could manifest itself as a memory
corruption. To weed out runtime instances of undefined behavior,
compile and link your code with “-fsanitize=undefined”, and then
run
‘patsopt’ from the command-line. If undefined behavior is
detected,
the runtime will report an error message on stderr.

Another useful one is “-fsanitze=address”, which is used the same
way.
Just before segfaulting, it should spit out a stack trace of where
the
memory violation occurred. That might solve your problem as well,
but
for this particular case (upgrading the compiler or enabling more
optimizations) checking for undefined behavior first should be
better
for determining the root cause.

-Greg

On Mon, Jan 26, 2015 at 4:05 PM, gmhwxi gmh...@gmail.com wrote:

FYI.

I once used (Clang-3.2 -O2) to compile ATS2 successfully.

Today, I noted that neither (Clang-3.4 -O2) nor (Clang-3.5 -O2)
can
succeed
in
compiling ATS2. The patsopt generated by these compilers crashes
immediately.
However, (Clang-3.5 -O1) can do it. So it is very suspicious
that new
optimizations
added into Clang-3.4 and Clang-3.5 were the cause of this
failure.
This
is a
very
unfortunate situation!

For now, (Gcc-4.8 -O2) is the only optimizing compiler that can
compile
ATS2.


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...@googlegroups.com.
To post to this group, send email to
ats-l...@googlegroups.com.
Visit this group at
http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/0489dc9f-652e-4a55-aa6e-030ac740561d%40googlegroups.com.


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...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAFLa5WPNvjUJvP_CEnW0Xyytc%2BwHPUjKC_MqT-4JN1YU6VfYXg%40mail.gmail.com.


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...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLpbNS6O%2B8doygqooiuejHnYCQ76CjmZt%3DoWodUX0quaug%40mail.gmail.com.


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...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAFLa5WM-UbGtk%3DVataT-gqzZTfTKrDFB4NxvRvuaYE5x9QNWoQ%40mail.gmail.com.


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...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLph8gEqH-4PHYWMPqg6xpp07s0i6JcCE3_1g9%3DteL69uQ%40mail.gmail.com.


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.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/dabf0a54-add5-4e04-ab1c-6ebcb11e18e4%40googlegroups.com.


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.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/F1FA52DD-34D7-446D-9B86-47834C03EA71%40shealevy.com.

https://www.google.com/search?q=linear+abstract+machine+functional+garbage :slight_smile:

I should test ICC… but I am scared.On Jan 26, 2015 7:05 PM, “gmhwxi” gmh...@gmail.com wrote:

FYI.

I once used (Clang-3.2 -O2) to compile ATS2 successfully.

Today, I noted that neither (Clang-3.4 -O2) nor (Clang-3.5 -O2) can
succeed in
compiling ATS2. The patsopt generated by these compilers crashes
immediately.
However, (Clang-3.5 -O1) can do it. So it is very suspicious that new
optimizations
added into Clang-3.4 and Clang-3.5 were the cause of this failure. This is
a very
unfortunate situation!

For now, (Gcc-4.8 -O2) is the only optimizing compiler that can compile
ATS2.


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.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/0489dc9f-652e-4a55-aa6e-030ac740561d%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/0489dc9f-652e-4a55-aa6e-030ac740561d%40googlegroups.com?utm_medium=email&utm_source=footer
.

Resending to get through googlegroups…On Tue, Jan 27, 2015 at 6:37 PM, Greg Fitzgerald gar...@gmail.com wrote:

+Reid

On Tue, Jan 27, 2015 at 6:29 PM, gmhwxi gmh...@gmail.com wrote:

Thanks!

I would really like to understand the issue.

As the variable tmp502 is not declared volatile, its value is
indeterminate

When is it indeterminate? During the longjmp phase?

Why does it matter whether it is indeterminate or not? It is not used
during
the
longjmp phase.

tmp502 is indeterminate after the longjmp. Consider this small example:

#include <setjmp.h>
int main(int argc, char **argv) {
int x = 42;
jmp_buf buf;
if (setjmp(buf))
return x;
x = 13;
longjmp(buf, 1);
}

LLVM immediately optimizes it to this:

#include <setjmp.h>
int main(int argc, char **argv) {
jmp_buf buf;
if (setjmp(buf))
return 42; // ‘x = 42’ dominates ‘return x’, x does not escape, so
setjmp cannot modify it, constant propagate
// x = 13; // dead, no one uses x after this.
longjmp(buf, 1); // noreturn, control ends here
}

setjmp and longjmp allow you to create control flow that the compiler
cannot see. Compilers model them for the most part as simple library
functions that can only modify memory that has previously escaped. Given
that I can write simple setjmp/longjmp wrappers that hide them from the
compiler, it is basically impossible to do otherwise.

Therefore, the C standard suggests that if you want to see updates to ‘x’
after setjmp and before longjmp, you use the ‘volatile’ storage specifier.
This pins it in stack memory and ensures that optimizers will not forward
stores to loads. This program will return 13 instead of 42:

#include <setjmp.h>
int main(int argc, char **argv) {
volatile int x = 42;
jmp_buf buf;
if (setjmp(buf))
return x;
x = 13;
longjmp(buf, 1);
}

Note that in this case, the printf is undefined behavior: p may point to the heap, but p itself is on the stack and thus indeterminate.> On Jan 28, 2015, at 6:11 AM, gmhwxi gmh...@gmail.com wrote:

Please try (clang -O1) and (clang -O2) on the following code:

#include <stdio.h>
#include <stdlib.h>
#include <setjmp.h>

static jmp_buf buf;

void
second(int *p) {
*p = 1000000;
printf(“second: *p = %i\n”, *p);
longjmp(buf,1); // jumps back to where setjmp was called - making setjmp now return 1
}

void
first(int *p) {
second(p);
printf(“first\n”); // does not print
}

int main() {
/*
int x = 0;
*/
int p;
p = malloc(sizeof(int));
/

printf(“main: p = %p\n”, p);
*/
if (p == 0)
{
fprintf (stderr, “malloc: failed!\n”); exit(1);
}

*p = 0;

if (!setjmp(buf) ) {
first(p); // when executed, setjmp returns 0
} else { // when longjmp jumps back, setjmp returns 1
printf(“main: *p = %i\n”, *p); // prints
}
return 0;
}

On Wednesday, January 28, 2015 at 12:59:15 AM UTC-5, gmhwxi wrote:
I thought that I had understood the issue; I apparently did not.

“”“”
All accessible objects have values, and all other components of the abstract
machine have state, as of the time the longjmp function was called, except that the
values of objects of automatic storage duration that are local to the function containing
the invocation of the corresponding setjmp macro that do not have volatile-qualified type
and have been changed between the setjmp invocation and longjmp call are
indeterminate.
“”“”

If you use (clang -O1) to compile the following code and then execute the generate object code,
you should get:

second
main: x = 1000000

If you use (clang -O2), you should get

second
main: x = 0

I understood this behavior: the value in x is really indeterminate; either 0 or 1000000 is okay.

What I do not understand is that you get the same results even if x is heap-allocated. This does
not follow from the above description: if x is heap-allocated, it is considered a state; so its content
should not be indeterminate. Right?

#include <stdio.h>
#include <setjmp.h>

static jmp_buf buf;

void
second(int *p) {
*p = 1000000;
printf(“second\n”); // prints
longjmp(buf,1); // jumps back to where setjmp was called - making setjmp now return 1
}

void
first(int *p) {
second(p);
printf(“first\n”); // does not print
}

int main() {
int x = 0;
if (!setjmp(buf) ) {
first(&x); // when executed, setjmp returns 0
} else { // when longjmp jumps back, setjmp returns 1
printf(“main: x = %i\n”, x); // prints
}
return 0;
}

On Tuesday, January 27, 2015 at 7:30:59 PM UTC-5, Greg Fitzgerald wrote:
From Reid Kleckner:

So this is almost undoubtedly a setjmp issue. Relevant C standard quote
[7.13.2.1 p5]:

“”"
All accessible objects have values, and all other components of the abstract
machine249)
have state, as of the time the longjmp function was called, except that the
values of
objects of automatic storage duration that are local to the function containing
the
invocation of the corresponding setjmp macro that do not have
volatile-qualified type
and have been changed between the setjmp invocation and longjmp call are
indeterminate.
“”"

As the variable tmp502 is not declared volatile, its value is indeterminate. I
think this is working as intended with nothing to do in LLVM.

On Tue, Jan 27, 2015 at 2:49 PM, Greg Fitzgerald <gar...@gmail.com <>> wrote:

Thanks for doing that work to ensure is in clang and not in
ATS-generated code. I opened a discussion on the llvmdev email list
and added a bug report at llvm.org http://llvm.org/:

http://llvm.org/bugs/show_bug.cgi?id=22360 http://llvm.org/bugs/show_bug.cgi?id=22360

I’ll keep you posted on progress. Feel free to jump in on the discussion.

-Greg

On Tue, Jan 27, 2015 at 12:11 AM, Hongwei Xi <gmh...@gmail.com <>> wrote:

I finally found a way to circumvent the problem.

The following code is taken from:

https://github.com/githwxi/ATS-Postiats/blob/master/src/pats_lintprgm.dats https://github.com/githwxi/ATS-Postiats/blob/master/src/pats_lintprgm.dats

implement{a}
myintvec_cffgcd
{n}(iv, n) = let
//
var res
: myint(a) = myint_make_int (0)
val p_res = &res
//
// HX-2015-01-27:
// fixing a bug in (clang-3.5 -O2)
//
// HX: a dummy to force clang
// not to optimize the value stored in [res]
val ((void)) = ptr_as_volatile(p_res)
//

If the call to ptr_as_volatile is removed, then clang-3.5
may use the (linear) value in [res] repeatedly, causing this
value to be freed more than once.

The C code is attached. Searching for ‘pats_as_volatile’ should lead
you to the spot where the bug occurs.

On Tue, Jan 27, 2015 at 12:36 AM, Greg Fitzgerald <gar...@gmail.com <>> wrote:

As I see it, the chance of fixing such a bug is really next to none.

Fixing clang 3.4 or 3.5? That sounds accurate. But if we move
quickly we might be able to squeeze a fix into 3.6. Can you send me
an isolated C fragment.

Thanks,
Greg

On Mon, Jan 26, 2015 at 5:58 PM, Hongwei Xi <gmh...@gmail.com <>> wrote:

I followed your suggestions.

There were 22M bytes of leaks reported (-fsanitize=address)
There were no undefined behaviors reported (-fsanitize=undefined)

Leaks are expected because I turned off GC.

As I see it, the chance of fixing such a bug is really next to none.

On Mon, Jan 26, 2015 at 8:18 PM, Greg Fitzgerald <gar...@gmail.com <>> wrote:

Today, I noted that neither (Clang-3.4 -O2) nor (Clang-3.5 -O2) can
succeed in
compiling ATS2. The patsopt generated by these compilers crashes
immediately.

It is expected for this class of error to occur if ATS2 depends on
undefined behavior. For example, if you use memcpy() instead of
memset() to copy overlapping regions, then bumping up to -O2 may pull
in a vectorized version, which could manifest itself as a memory
corruption. To weed out runtime instances of undefined behavior,
compile and link your code with “-fsanitize=undefined”, and then run
‘patsopt’ from the command-line. If undefined behavior is detected,
the runtime will report an error message on stderr.

Another useful one is “-fsanitze=address”, which is used the same way.
Just before segfaulting, it should spit out a stack trace of where the
memory violation occurred. That might solve your problem as well, but
for this particular case (upgrading the compiler or enabling more
optimizations) checking for undefined behavior first should be better
for determining the root cause.

-Greg

On Mon, Jan 26, 2015 at 4:05 PM, gmhwxi <gmh...@gmail.com <>> wrote:

FYI.

I once used (Clang-3.2 -O2) to compile ATS2 successfully.

Today, I noted that neither (Clang-3.4 -O2) nor (Clang-3.5 -O2) can
succeed
in
compiling ATS2. The patsopt generated by these compilers crashes
immediately.
However, (Clang-3.5 -O1) can do it. So it is very suspicious that new
optimizations
added into Clang-3.4 and Clang-3.5 were the cause of this failure.
This
is a
very
unfortunate situation!

For now, (Gcc-4.8 -O2) is the only optimizing compiler that can
compile
ATS2.


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...@googlegroups.com <>.
To post to this group, send email to ats-l...@googlegroups.com <>.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/0489dc9f-652e-4a55-aa6e-030ac740561d%40googlegroups.com https://groups.google.com/d/msgid/ats-lang-users/0489dc9f-652e-4a55-aa6e-030ac740561d%40googlegroups.com.


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...@googlegroups.com <>.
To post to this group, send email to ats-l...@googlegroups.com <>.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAFLa5WPNvjUJvP_CEnW0Xyytc%2BwHPUjKC_MqT-4JN1YU6VfYXg%40mail.gmail.com https://groups.google.com/d/msgid/ats-lang-users/CAFLa5WPNvjUJvP_CEnW0Xyytc%2BwHPUjKC_MqT-4JN1YU6VfYXg%40mail.gmail.com.


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...@googlegroups.com <>.
To post to this group, send email to ats-l...@googlegroups.com <>.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit

https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLpbNS6O%2B8doygqooiuejHnYCQ76CjmZt%3DoWodUX0quaug%40mail.gmail.com https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLpbNS6O%2B8doygqooiuejHnYCQ76CjmZt%3DoWodUX0quaug%40mail.gmail.com.


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...@googlegroups.com <>.
To post to this group, send email to ats-l...@googlegroups.com <>.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAFLa5WM-UbGtk%3DVataT-gqzZTfTKrDFB4NxvRvuaYE5x9QNWoQ%40mail.gmail.com https://groups.google.com/d/msgid/ats-lang-users/CAFLa5WM-UbGtk%3DVataT-gqzZTfTKrDFB4NxvRvuaYE5x9QNWoQ%40mail.gmail.com.


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...@googlegroups.com <>.
To post to this group, send email to ats-l...@googlegroups.com <>.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLph8gEqH-4PHYWMPqg6xpp07s0i6JcCE3_1g9%3DteL69uQ%40mail.gmail.com https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLph8gEqH-4PHYWMPqg6xpp07s0i6JcCE3_1g9%3DteL69uQ%40mail.gmail.com.


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 mailto:ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com mailto:ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/83e98e70-e320-4d7d-8776-5a6fa2804b94%40googlegroups.com https://groups.google.com/d/msgid/ats-lang-users/83e98e70-e320-4d7d-8776-5a6fa2804b94%40googlegroups.com?utm_medium=email&utm_source=footer.

Clean finds a way to use linear logic.
Essentially, Clean uses linear logic to do reference counting at
compile-time.
IMO, this is a very superficial way to use linear logic.

In physics, if a theory is developed, it should be tested in reality (the
physical
world). To me, a “good” linear type theory should be able to explain how C
works.
I see C as the “reality” testbed for a type theory. In this regard, C is
very special.
Let me give a comparison. Haskell certainly has a sophisticatedly developed
type
theory. But this type theory only explains how things work in the abstract
computational
model of Haskell (Stage 1).On Thu, Jan 29, 2015 at 8:58 PM, Raoul Duke rao...@gmail.com wrote:

Linear logic as in Concurrent Clean style Uniqueness Types?

“If a uniquely typed argument is not returned again in the function
result it has become garbage (the reference has dropped to zero). Due
to the fact that uniqueness typing is static the object can be garbage
collected (see Chapter 2) at compile time.”

?


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.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb6_uTx-EEXh5L_eD637h_E%2BTagutyxxgsiCHzCOEDKPdg%40mail.gmail.com
.