ATS and Clang-3.5

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.

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 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.

If the compiler could insert the malloc’s and free’s that a human does
in C, then that seems to just end up as reference counting? As much as
I like GC in some ways, I don’t utterly dislike e.g. ARC.

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/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

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 <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.

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.

On Friday, I happened across Plaugers book, which I’m now tempted to buy
(didn’t know about it previously). I did find the following relevant quotes
:slight_smile:

<javascript:>

Indeed, the CompCert manual says the same. Additionnaly to the previous
quote, here is another one, on page 40:

The CompCert C compiler has no special knowledge of the setjmp and
longjmp functions, treating
them as ordinary functions that respect control flow.
It is therefore not
advised to use these two func-
tions in CompCert-compiled code. To prevent misoptimisation, it is crucial
that all local variables that
are live across an invocation of setjmp be declared with volatile modifier.

Thanks!

What should happen if x is not on the stack. Say you do

int *p;
p = malloc(sizeof(int));
*p = 42
//
// replace x with *p from this point on
//

I noted that clang does the same after this change. Is this according to
the C standard?On Monday, January 26, 2015 at 7:05:49 PM UTC-5, gmhwxi 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.

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 :)On Mon, Jan 26, 2015 at 7:09 PM, Raoul Duke rao...@gmail.com wrote:

things like this, and the bugs seen in the Tahoe LAFS project, make me
hold the opinion that compiler optimizations are basically kinda
almost purely bad deals with the devil.


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/CAJ7XQb5TLbxu-Att5nP_SYDujm3Zq%3DwF3yLQKqP15jMQ0m9kPw%40mail.gmail.com
.

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.”

?

I so wished that there had been a so-called “reference” implementation for
C.
Just like Scheme.On Tuesday, January 27, 2015 at 9:14:03 PM UTC-5, Barry Schwartz wrote:

Greg Fitzgerald <gar...@gmail.com <javascript:>> skribis:

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.

My worldview is sustained. I keep the C standard nearby because it is
so precise about things.

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.

-GregOn 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.

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/:

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/dabf0a54-add5-4e04-ab1c-6ebcb11e18e4%40googlegroups.com https://groups.google.com/d/msgid/ats-lang-users/dabf0a54-add5-4e04-ab1c-6ebcb11e18e4%40googlegroups.com?utm_medium=email&utm_source=footer.

It is pretty clear to me that Section 7.13.2.1 is written by
compiler-writers.
The main purpose of this section is to not really trying to clarify the use
of
setjmp/longjmp. If I am sarcastic about it, then I would say that its main
purpose
is probably about covering their rear ends :slight_smile:

First, setjmp/longjmp is straightforward to implement if optimization is
not of
the concern. Essentially, you just attach labels to the stack so that you
know how
to roll back the stack when longjmp is called.

However, if we want to optimize away some memory accesses (that is, caching
some memory contents), then there is a challenge here. Because one never
knows
when longjmp is to take place after setjmp is called, being conservative
means that
everything on the stack should be treated as being volatile. Probably this
is too
conservative a stance for the compiler-writer to take, so Section 7.13.2.1
shifts the
burden to the programmer: it is the programmer’s responsibility to clearly
indicate what
should be treated as being volatile.

This is just like the fine prints in the brochure sent by a credit card
company.

It is not the end of the story yet. Section 7.13.2.1 does not say anything
about
inlining a function that calls setjmp. Is it allowed? If it is, then what
about the
stack-allocated variables in the function that calls the inlined function?
Should
they be handled according to Section 7.13.2.1 as well?On Wednesday, January 28, 2015 at 1:26:58 PM UTC-5, Barry Schwartz wrote:

gmhwxi <gmh...@gmail.com <javascript:>> skribis:

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

I’m looking at the 2011 standard. To me Section 7.13.2.1 seems pretty
clear that the value has to be ‘actually changed’ to be considered
indeterminate. So I would think an optimizer ought to be conservative
about it.

On Friday, I happened across Plaugers book, which I’m now tempted to buy
(didn’t know about it previously). I did find the following relevant quotes
… :)On Sat, Jan 31, 2015 at 4:32 AM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Le mardi 27 janvier 2015 19:44:26 UTC+1, gmhwxi a écrit :

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).


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/ee1267f2-985c-429f-8a74-b14da62112dc%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/ee1267f2-985c-429f-8a74-b14da62112dc%40googlegroups.com?utm_medium=email&utm_source=footer
.

Brandon Barker
brandon...@gmail.com

I will start another thread on this. It has been buried too deep!On Friday, January 30, 2015 at 2:36:48 AM UTC-5, Raoul Duke wrote:

If the compiler could insert the malloc’s and free’s that a human does
in C, then that seems to just end up as reference counting? As much as
I like GC in some ways, I don’t utterly dislike e.g. ARC.

http://xkcd.com/1312/On 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 this is all due to C being a REAL programming language :)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. :-}

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

+ReidOn 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.

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/8ff4ed81-65b3-4259-8cf1-0f7cf0b8911f%40googlegroups.com.