Trying to build ATS2 with CompCert

Yannick_Duchene · January 31, 2015, 10:15am

After some quick and easy tweaks, I’m getting this, and as it’s in C files
probably generated by ATS1, I feel to guess I can’t fix, and it suggest
something would have to be tweaked in the C source generator.

 \
 make -j4 -C src/CBOOT \
 CCOMP=compcert GCFLAG=-D_ATS_NGC \
 CFLAGS= LDFLAGS= patsopt
 make[1]: entrant dans le répertoire «

/home/yannick/Applications/Third_Parties/ATS/ATS2-Postiats-0.1.8/src/CBOOT »
compcert -I. -I./ccomp/runtime -c -o pats_main_dats.o pats_main_dats.c
compcert -I. -I./ccomp/runtime -c -o pats_utils_sats.o
pats_utils_sats.c
compcert -I. -I./ccomp/runtime -c -o pats_location_sats.o
pats_location_sats.c
compcert -I. -I./ccomp/runtime -c -o pats_jsonize_sats.o
pats_jsonize_sats.c
./ccomp/runtime/ats_types.h:68: Warning: empty struct.
./ccomp/runtime/ats_types.h:68: Warning: empty struct.
./ccomp/runtime/ats_types.h:68: Warning: empty struct.
compcert -I. -I./ccomp/runtime -c -o pats_errmsg_sats.o
pats_errmsg_sats.c
./libc/sys/CATS/types.cats:72: Error: illegal comparison between types
dev_t
and dev_t.
Fatal error; compilation aborted.
1 error detected.
make[1]: *** [pats_utils_sats.o] Erreur 2
make[1]: *** Attente des tâches non terminées…
./ccomp/runtime/ats_types.h:68: Warning: empty struct.
./ccomp/runtime/ats_types.h:68: Warning: empty struct.
prelude/CATS/bool.cats:45: Warning:
redefinition of ‘ats_exit_errmsg’ with incompatible type.
libc/sys/CATS/types.cats:72: Error: illegal comparison between types
dev_t
and dev_t.
Fatal error; compilation aborted.
1 error detected.
make[1]: *** [pats_main_dats.o] Erreur 2
make[1]: quittant le répertoire «
/home/yannick/Applications/Third_Parties/ATS/ATS2-Postiats-0.1.8/src/CBOOT »
make: *** [src2_patsopt] Erreur 2

Note the current directory for these messages, seems to be “src/CBOOT”.

The warning “./ccomp/runtime/ats_types.h:68: Warning: empty struct.”, which
appears five times, is about this:

 typedef struct{} ats_empty_type ;

OK, that’s just a warning.

The error “./libc/sys/CATS/types.cats:72: Error: illegal comparison between
types dev_t and dev_t.”, which appears two times, is about this:

typedef dev_t ats_dev_type ; // for device IDs

 ATSinline()
 ats_bool_type
 atslib_eq_dev_dev
   (dev_t x1, dev_t x2) {
   return (x1 == x2 ? ats_true_bool : ats_false_bool) ;
 } // end of [atslib_eq_dev_dev]

Line #72 is the one with “return (x1 == x2 ? ats_true_bool :
ats_false_bool) ;”

I’m surprised with this one: is there a case where C99 disallow a
comparison between two value of the same type? (here, dev_t).

Yannick_Duchene · January 31, 2015, 7:21pm

Hi Yannick,

This is all great!

It does seem quite plausible that we will be able to use compcert to
compile ATS in the
near future.

Could you also try to use compcert to compile some examples of C code
generated by ATS2?

For instance, the examples in the following directory are good ones:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/SHOOTOUT

These examples should give us a rough idea as to how compcert is compared
with gcc/clang in
terms of the efficiency of the generated object code.

Many thanks!

Just had a quick look building with GCC for a prior checkup. Some seems to
require some data as input, but I don’t know where do I have to pick these
data. Some work straight away, but are so fast I’m not sure I have to time
them: are their execution time to be checked too? (must be a few
milliseconds). Some others either crash or don’t compile, and I don’t know
if it’s due to something wrong with my ATS2 (Postiat 0.1.8) or something
else.

Yannick_Duchene · January 31, 2015, 1:16pm

Now it achieves compilation, but fails at link time, and I have so much
link errors I’m afraid. As a side note, during compilation, there is a lot
of warning messages.
The very long list of link error I get (enough for now, I may try to
resume later):

A last note: most of the link errors are about multiple definitions, and
the warnings I get during compilation were about redefinitions with
incompatible types. This seems related… What surprises me, is that there do
not seems to be any issue with multiple definition at link time when ATS2
is compiled with GCC.

Until now, for a summary, I would say compiling ATS2 would need three
things and may be a fourth one:

To know how to tell the GNU C includes files to not use __signed__
To change configure so that it propagates de CC environment variable
it recieves
To use memcmp when nothing in POSIX and the C standard ensure a type
is suitable for direct comparison (i.e. nothing ensure it’s a simple type)
May be to not generate multiple definition, but that’s strange, as it’s
not an issue when compiled with GCC.

gmhwxi · January 31, 2015, 7:30pm

These examples are taken from:

http://benchmarksgame.alioth.debian.org/

For now, let us focus on pidigits. On my machine, I got:

time ./pidigits 10000 > /dev/null

real 0m1.006s
user 0m0.996s
sys 0m0.008s

time ./pidigits_gcc 10000 > /dev/null

real 0m1.004s
user 0m1.000s
sys 0m0.000s

What if we use compcert instead of gcc on pidigits and pidigits_gcc?On Sat, Jan 31, 2015 at 2:21 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Le samedi 31 janvier 2015 19:36:46 UTC+1, gmhwxi a écrit :

Hi Yannick,

This is all great!

It does seem quite plausible that we will be able to use compcert to
compile ATS in the
near future.

Could you also try to use compcert to compile some examples of C code
generated by ATS2?

For instance, the examples in the following directory are good ones:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/SHOOTOUT

These examples should give us a rough idea as to how compcert is compared
with gcc/clang in
terms of the efficiency of the generated object code.

Many thanks!

Just had a quick look building with GCC for a prior checkup. Some seems to
require some data as input, but I don’t know where do I have to pick these
data. Some work straight away, but are so fast I’m not sure I have to time
them: are their execution time to be checked too? (must be a few
milliseconds). Some others either crash or don’t compile, and I don’t know
if it’s due to something wrong with my ATS2 (Postiat 0.1.8) or something
else.

–
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/026704dc-895d-4a0f-843b-9c625f839ab4%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/026704dc-895d-4a0f-843b-9c625f839ab4%40googlegroups.com?utm_medium=email&utm_source=footer
.

gmhwxi · January 31, 2015, 8:05pm

Some others either crash or don’t compile, and I don’t know if it’s due
to something wrong with my ATS2 (Postiats 0.1.8) or something else.

I just tried. All the programs compiled on my machine. Let me know which
ones did not compile on yours.

I also modified several Makefiles so that clang can also be used (except on
those relying on gcc-eccentric features).On Sat, Jan 31, 2015 at 2:21 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Le samedi 31 janvier 2015 19:36:46 UTC+1, gmhwxi a écrit :

Hi Yannick,

This is all great!

It does seem quite plausible that we will be able to use compcert to
compile ATS in the
near future.

Could you also try to use compcert to compile some examples of C code
generated by ATS2?

For instance, the examples in the following directory are good ones:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/SHOOTOUT

These examples should give us a rough idea as to how compcert is compared
with gcc/clang in
terms of the efficiency of the generated object code.

Many thanks!

Just had a quick look building with GCC for a prior checkup. Some seems to
require some data as input, but I don’t know where do I have to pick these
data. Some work straight away, but are so fast I’m not sure I have to time
them: are their execution time to be checked too? (must be a few
milliseconds). Some others either crash or don’t compile, and I don’t know
if it’s due to something wrong with my ATS2 (Postiat 0.1.8) or something
else.

–
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/026704dc-895d-4a0f-843b-9c625f839ab4%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/026704dc-895d-4a0f-843b-9c625f839ab4%40googlegroups.com?utm_medium=email&utm_source=footer
.

Shea_Levy · January 31, 2015, 8:58pm

What about using memcmp for comparison of C types when these C types cannot be ensured to be simple type and so may possibly be compound types?

Any reason not to just use memcmp unconditionally? This is generated code after all.

Yannick_Duchene · January 31, 2015, 11:59am

Here is a short test:
 #include <stdio.h>
 #include <sys/types.h>

 typedef int ats_bool_type;
 #define ats_true_bool 1
 #define ats_false_bool 0

 ats_bool_type atslib_eq_dev_dev (dev_t x1, dev_t x2) {
    return (x1 == x2 ? ats_true_bool : ats_false_bool) ;
 } // end of [atslib_eq_dev_dev]

 int main (void) {
    printf("Hello!\n");
    printf("Size of `dev_t is` %i bytes\n", sizeof(dev_t));
    return 0;
 }
Compilation fails with CompCert, even with this short snippet.

If I change the type of x1 and x2 to int, then it compiles, and says
the size of dev_t is 8 bytes.

May be a track.

First I tested two variations.

 typedef struct {
    int a;
    int b;
 } dev_t2;

 typedef long long dev_t3;

If the type of x1 and x2 is dev_t2, it fails with both GCC and
CompCert, and if it is dev_t3 it compiles with both GCC and CompCert.

I suspect a conditional definition which makes dev_t not be defiend the
same when compiling with one or the other.

dev_t is defined as an alias of __dev_t which is defined to be
__DEV_T_TYPE which is defined to be __UQUAD_TYPE, which for machine
with 32 bits words, is defined to be __u_quad_t and here, things may
start to be wrong.

I have this:

 #if __WORDSIZE == 64
    typedef long int __quad_t;
    typedef unsigned long int __u_quad_t;
 #elif defined __GLIBC_HAVE_LONG_LONG
    __extension__ typedef long long int __quad_t;
    __extension__ typedef unsigned long long int __u_quad_t;
 #else
    typedef struct
    {
       long __val[2];
    } __quad_t;
    typedef struct
    {
       __u_long __val[2];
    } __u_quad_t;
 #endif

I guessed when compiling with CompCert, __GLIBC_HAVE_LONG_LONG is false
and it fall back to the struct definition, which does not allow
comparison.

Indeed, compiling with compcert -D__GLIBC_HAVE_LONG_LONG=1 make the build
succeed.

However, that’s a trick, and may be there is a better way, but which
involves modifying ATS1 which is used to generated C files for ATS2 (and
ATS2 if in the future ATS2 is supposed to generate its own C files).

In <sys/types.h>
nothing is asserted about dev_t. May when nothing assert a type is a
simple type, comparison should be defined using memcmp. This should not
be an issue, as a believe most C compiler will be able to optimize it when
feasible.

What about using memcmp for comparison of C types when these C types
cannot be ensured to be simple type and so may possibly be compound types?

Yannick_Duchene · January 31, 2015, 8:24pm

These examples are taken from:

http://benchmarksgame.alioth.debian.org/

For now, let us focus on pidigits. On my machine, I got:

time ./pidigits 10000 > /dev/null

real 0m1.006s
user 0m0.996s
sys 0m0.008s

time ./pidigits_gcc 10000 > /dev/null

real 0m1.004s
user 0m1.000s
sys 0m0.000s

What if we use compcert instead of gcc on pidigits and pidigits_gcc?

I’m stuck with a “syntax error” in integer_fixed.cats at line 58, the
line “typedef int64_t atstype_int64 ;”

As CompCert seems to complain about syntax error when it encounters an
undefined type, my guess is that it does not see the definition of the
atstype_int64.

Here is the command I used:

 ccomp -v -I${PATSHOME} -I${PATSHOME}/ccomp/runtime

-I/home/yannick/apps/ats/contrib pidigits_dats.c

I can’t figure it out, but I will try again (just wanted to tell why I’m
not posting the expected reply).

gmhwxi · January 31, 2015, 11:12pm

Yes, I should have used memcpy and let the compiler to optimize it
away.

Will make changes shortly.On Saturday, January 31, 2015 at 3:58:39 PM UTC-5, Shea Levy wrote:

On Jan 31, 2015, at 11:59 AM, ‘Yannick Duchêne’ via ats-lang-users < ats-l...@googlegroups.com <javascript:>> wrote:

What about using memcmp for comparison of C types when these C types
cannot be ensured to be simple type and so may possibly be compound types?

Any reason not to just use memcmp unconditionally? This is generated code
after all.

Yannick_Duchene · January 31, 2015, 1:02pm

According to The GNU C Reference Manual ,
__signed__ is a GNU extension to C, so may be the headers must be told to
conform to C99, may be defining another macro on the command line, but I
don’t know which one. Some one who know GCC lib well have an idea?

Tried -D_STDC_VERSION__=199901L and -D__STDC__, and this does not
resolve the error. Tried -D__signed__=, this solve the error, but I don’t
like it, it looks like a hack, and there must be a proper configuration
flag for this.

That said, although it looks like a trick, it proceed further and stop on
errors about an unsupported feature with returning unions.Does not look to
be a bad error, as CompCert suggest to just add the -fstruct-return
option.

It proceed further again, and it stopped on another unsupported feature,
with long double. For this one it does not suggest any option to add to
the command line, but the documentation do. At “5.2.4.2 Numerical limits.”
it says it required the option -flongdouble.

Now it achieves compilation, but fails at link time, and I have so much
link errors I’m afraid. As a side note, during compilation, there is a lot
of warning messages.

The very long list of link error I get (enough for now, I may try to resume
later):

pats_stamp_dats.o: In function aux_31_clofun': (.text+0x520): multiple definition of aux_31_clofun’
pats_intinf_dats.o:(.text+0x8b0): first defined here
pats_stamp_dats.o: In function aux_31_closure_make': (.text+0x560): multiple definition of aux_31_closure_make’
pats_intinf_dats.o:(.text+0x8f0): first defined here
pats_parsing_dats.o: In function __ats_fun_3_clofun': (.text+0x150): multiple definition of __ats_fun_3_clofun’
pats_reader_dats.o:(.text+0xf0): first defined here
pats_parsing_dats.o: In function __ats_fun_3_closure_make': (.text+0x170): multiple definition of __ats_fun_3_closure_make’
pats_reader_dats.o:(.text+0x110): first defined here
pats_trans1_sort_dats.o: In function __ats_fun_5_clofun': (.text+0x190): multiple definition of __ats_fun_5_clofun’
pats_reader_dats.o:(.text+0x1b0): first defined here
pats_trans1_sort_dats.o: In function __ats_fun_5_closure_make': (.text+0x1e0): multiple definition of __ats_fun_5_closure_make’
pats_reader_dats.o:(.text+0x1c0): first defined here
pats_trans1_sort_dats.o: In function __ats_fun_8_clofun': (.text+0x2c0): multiple definition of __ats_fun_8_clofun’
pats_reader_dats.o:(.text+0x300): first defined here
pats_trans1_sort_dats.o: In function __ats_fun_8_closure_make': (.text+0x310): multiple definition of __ats_fun_8_closure_make’
pats_reader_dats.o:(.text+0x320): first defined here
pats_trans1_p0at_dats.o: In function appf_1_clofun': (.text+0x250): multiple definition of appf_1_clofun’
pats_trans1_sort_dats.o:(.text+0x90): first defined here
pats_trans1_p0at_dats.o: In function appf_1_closure_make': (.text+0x290): multiple definition of appf_1_closure_make’
pats_trans1_sort_dats.o:(.text+0xd0): first defined here
pats_trans1_p0at_dats.o: In function __ats_fun_7_clofun': (.text+0x370): multiple definition of __ats_fun_7_clofun’
pats_reader_dats.o:(.text+0x270): first defined here
pats_trans1_p0at_dats.o: In function __ats_fun_7_closure_make': (.text+0x3c0): multiple definition of __ats_fun_7_closure_make’
pats_reader_dats.o:(.text+0x2a0): first defined here
pats_trans1_p0at_dats.o: In function __ats_fun_10_clofun': (.text+0x4c0): multiple definition of __ats_fun_10_clofun’
pats_reader_dats.o:(.text+0x400): first defined here
pats_trans1_p0at_dats.o: In function __ats_fun_10_closure_make': (.text+0x510): multiple definition of __ats_fun_10_closure_make’
pats_reader_dats.o:(.text+0x420): first defined here
pats_trans1_p0at_dats.o: In function f_16_clofun': (.text+0x700): multiple definition of f_16_clofun’
pats_fixity_fxty_dats.o:(.text+0xaa0): first defined here
pats_trans1_p0at_dats.o: In function f_16_closure_make': (.text+0x740): multiple definition of f_16_closure_make’
pats_fixity_fxty_dats.o:(.text+0xaf0): first defined here
pats_trans1_syndef_dats.o: In function __ats_fun_12_clofun': (.text+0x360): multiple definition of __ats_fun_12_clofun’
pats_trans1_e0xp_dats.o:(.text+0x880): first defined here
pats_trans1_syndef_dats.o: In function __ats_fun_12_closure_make': (.text+0x3a0): multiple definition of __ats_fun_12_closure_make’
pats_trans1_e0xp_dats.o:(.text+0x8d0): first defined here
pats_trans1_dynexp_dats.o: In function __ats_fun_8_clofun': (.text+0x3e0): multiple definition of __ats_fun_8_clofun’
pats_reader_dats.o:(.text+0x300): first defined here
pats_trans1_dynexp_dats.o: In function __ats_fun_8_closure_make': (.text+0x430): multiple definition of __ats_fun_8_closure_make’
pats_reader_dats.o:(.text+0x320): first defined here
pats_trans1_dynexp_dats.o: In function __ats_fun_11_clofun': (.text+0x530): multiple definition of __ats_fun_11_clofun’
pats_reader_dats.o:(.text+0x4e0): first defined here
pats_trans1_dynexp_dats.o: In function __ats_fun_11_closure_make': (.text+0x580): multiple definition of __ats_fun_11_closure_make’
pats_reader_dats.o:(.text+0x500): first defined here
pats_staexp2_pprint_dats.o: In function loop_9_clofun': (.text+0x1b50): multiple definition of loop_9_clofun’
pats_symbol_dats.o:(.text+0x180): first defined here
pats_staexp2_pprint_dats.o: In function loop_9_closure_make': (.text+0x1ba0): multiple definition of loop_9_closure_make’
pats_symbol_dats.o:(.text+0x1e0): first defined here
pats_staexp2_pprint_dats.o: In function loop_10_clofun': (.text+0x1cd0): multiple definition of loop_10_clofun’
pats_lexing_token_dats.o:(.text+0x1c0): first defined here
pats_staexp2_pprint_dats.o: In function loop_10_closure_make': (.text+0x1d20): multiple definition of loop_10_closure_make’
pats_lexing_token_dats.o:(.text+0x220): first defined here
pats_staexp2_pprint_dats.o: In function loop_11_clofun': (.text+0x1eb0): multiple definition of loop_11_clofun’
pats_lexing_dats.o:(.text+0x230): first defined here
pats_staexp2_pprint_dats.o: In function loop_11_closure_make': (.text+0x1f00): multiple definition of loop_11_closure_make’
pats_lexing_dats.o:(.text+0x290): first defined here
pats_staexp2_svar_dats.o: In function aux_26_clofun': (.text+0x670): multiple definition of aux_26_clofun’
pats_staexp2_pprint_dats.o:(.text+0x2af0): first defined here
pats_staexp2_svar_dats.o: In function aux_26_closure_make': (.text+0x6c0): multiple definition of aux_26_closure_make’
pats_staexp2_pprint_dats.o:(.text+0x2b40): first defined here
pats_staexp2_svvar_dats.o: In function insert_34_clofun': (.text+0xb10): multiple definition of insert_34_clofun’
pats_staexp2_svar_dats.o:(.text+0xe00): first defined here
pats_staexp2_svvar_dats.o: In function insert_34_closure_make': (.text+0xb60): multiple definition of insert_34_closure_make’
pats_staexp2_svar_dats.o:(.text+0xe50): first defined here
pats_staexp2_skexp_dats.o: In function aux_2_clofun': (.text+0xa0): multiple definition of aux_2_clofun’
pats_dynexp1_print_dats.o:(.text+0x100): first defined here
pats_staexp2_skexp_dats.o: In function aux_2_closure_make': (.text+0xf0): multiple definition of aux_2_closure_make’
pats_dynexp1_print_dats.o:(.text+0x150): first defined here
pats_patcst2_dats.o: In function aux_64_clofun': (.text+0x2280): multiple definition of aux_64_clofun’
pats_staexp2_svvar_dats.o:(.text+0x1740): first defined here
pats_patcst2_dats.o: In function aux_64_closure_make': (.text+0x22b0): multiple definition of aux_64_closure_make’
pats_staexp2_svvar_dats.o:(.text+0x1790): first defined here
pats_dynexp2_print_dats.o: In function aux_5_clofun': (.text+0x4f0): multiple definition of aux_5_clofun’
pats_staexp1_print_dats.o:(.text+0x3f0): first defined here
pats_dynexp2_print_dats.o: In function aux_5_closure_make': (.text+0x540): multiple definition of aux_5_closure_make’
pats_staexp1_print_dats.o:(.text+0x440): first defined here
pats_dynexp2_dcst_dats.o: In function __ats_fun_37_clofun': (.text+0x750): multiple definition of __ats_fun_37_clofun’
pats_patcst2_dats.o:(.text+0x1030): first defined here
pats_dynexp2_dcst_dats.o: In function aux_42_clofun': (.text+0x890): multiple definition of aux_42_clofun’
pats_intinf_dats.o:(.text+0xd40): first defined here
pats_dynexp2_dcst_dats.o: In function aux_42_closure_make': (.text+0x8d0): multiple definition of aux_42_closure_make’
pats_intinf_dats.o:(.text+0xd90): first defined here
pats_dynexp2_dvar_dats.o: In function __ats_fun_50_clofun': (.text+0xde0): multiple definition of __ats_fun_50_clofun’
pats_patcst2_dats.o:(.text+0x17c0): first defined here
pats_dynexp2_dvar_dats.o: In function __ats_fun_50_closure_make': (.text+0xe20): multiple definition of __ats_fun_50_closure_make’
pats_patcst2_dats.o:(.text+0x17f0): first defined here
pats_dynexp2_dvar_dats.o: In function insert_99_clofun': (.text+0x2950): multiple definition of insert_99_clofun’
pats_staexp2_scst_dats.o:(.text+0x2630): first defined here
pats_dynexp2_dvar_dats.o: In function insert_99_closure_make': (.text+0x29a0): multiple definition of insert_99_closure_make’
pats_staexp2_scst_dats.o:(.text+0x2680): first defined here
pats_trans2_env_dats.o: In function f_12_clofun': (.text+0x1d0): multiple definition of f_12_clofun’
pats_fixity_fxty_dats.o:(.text+0x580): first defined here
pats_trans2_env_dats.o: In function f_12_closure_make': (.text+0x200): multiple definition of f_12_closure_make’
pats_fixity_fxty_dats.o:(.text+0x5d0): first defined here
pats_trans2_env_dats.o: In function f_27_clofun': (.text+0x6d0): multiple definition of f_27_clofun’
pats_trans1_staexp_dats.o:(.text+0x980): first defined here
pats_trans2_env_dats.o: In function f_27_closure_make': (.text+0x700): multiple definition of f_27_closure_make’
pats_trans1_staexp_dats.o:(.text+0x9b0): first defined here
pats_trans2_staexp_dats.o: In function aux_62_clofun': (.text+0x2eb0): multiple definition of aux_62_clofun’
pats_trans2_env_dats.o:(.text+0x1390): first defined here
pats_trans2_staexp_dats.o: In function aux_62_closure_make': (.text+0x2ef0): multiple definition of aux_62_closure_make’
pats_trans2_env_dats.o:(.text+0x13d0): first defined here
pats_trans2_dynexp_dats.o: In function __ats_fun_15_clofun': (.text+0xd10): multiple definition of __ats_fun_15_clofun’
pats_trans1_syndef_dats.o:(.text+0x4e0): first defined here
pats_trans2_impdec_dats.o: In function auxerr1_24_clofun': (.text+0x16c0): multiple definition of auxerr1_24_clofun’
pats_trans2_staexp_dats.o:(.text+0x1010): first defined here
pats_trans2_impdec_dats.o: In function auxerr1_24_closure_make': (.text+0x16e0): multiple definition of auxerr1_24_closure_make’
pats_trans2_staexp_dats.o:(.text+0x1060): first defined here
pats_trans2_impdec_dats.o: In function auxerr2_25_clofun': (.text+0x1870): multiple definition of auxerr2_25_clofun’
pats_trans2_staexp_dats.o:(.text+0x11f0): first defined here
pats_trans2_impdec_dats.o: In function auxerr2_25_closure_make': (.text+0x18b0): multiple definition of auxerr2_25_closure_make’
pats_trans2_staexp_dats.o:(.text+0x1240): first defined here
pats_dynexp3_print_dats.o: In function aux_5_clofun': (.text+0xa20): multiple definition of aux_5_clofun’
pats_staexp1_print_dats.o:(.text+0x3f0): first defined here
pats_dynexp3_print_dats.o: In function aux_5_closure_make': (.text+0xa70): multiple definition of aux_5_closure_make’
pats_staexp1_print_dats.o:(.text+0x440): first defined here
pats_trans3_env_lstate_dats.o: In function aux_5_clofun': (.text+0x2d0): multiple definition of aux_5_clofun’
pats_staexp1_print_dats.o:(.text+0x3f0): first defined here
pats_trans3_env_lstate_dats.o: In function aux_5_closure_make': (.text+0x320): multiple definition of aux_5_closure_make’
pats_staexp1_print_dats.o:(.text+0x440): first defined here
pats_dmacro2_print_dats.o: In function aux_2_clofun': (.text+0xa0): multiple definition of aux_2_clofun’
pats_dynexp1_print_dats.o:(.text+0x100): first defined here
pats_dmacro2_print_dats.o: In function aux_2_closure_make': (.text+0xf0): multiple definition of aux_2_closure_make’
pats_dynexp1_print_dats.o:(.text+0x150): first defined here
pats_trans3_p2at_dats.o: In function aux_21_clofun': (.text+0xbb0): multiple definition of aux_21_clofun’
pats_utils_dats.o:(.text+0x900): first defined here
pats_trans3_p2at_dats.o: In function aux_21_closure_make': (.text+0xc10): multiple definition of aux_21_closure_make’
pats_utils_dats.o:(.text+0x940): first defined here
pats_trans3_dynexp_dn_dats.o: In function __ats_fun_7_clofun': (.text+0x3d0): multiple definition of __ats_fun_7_clofun’
pats_reader_dats.o:(.text+0x270): first defined here
pats_trans3_caseof_dats.o: In function auxerr_15_clofun': (.text+0x9b0): multiple definition of auxerr_15_clofun’
pats_trans3_env_effect_dats.o:(.text+0x590): first defined here
pats_trans3_caseof_dats.o: In function auxerr_15_closure_make': (.text+0x9f0): multiple definition of auxerr_15_closure_make’
pats_trans3_env_effect_dats.o:(.text+0x5d0): first defined here
pats_trans3_caseof_dats.o: In function aux_21_clofun': (.text+0xdf0): multiple definition of aux_21_clofun’
pats_utils_dats.o:(.text+0x900): first defined here
pats_trans3_caseof_dats.o: In function aux_21_closure_make': (.text+0xe20): multiple definition of aux_21_closure_make’
pats_utils_dats.o:(.text+0x940): first defined here
pats_trans3_decl_dats.o: In function aux_10_clofun': (.text+0x740): multiple definition of aux_10_clofun’
pats_trans3_env_print_dats.o:(.text+0xc00): first defined here
pats_trans3_decl_dats.o: In function aux_10_closure_make': (.text+0x770): multiple definition of aux_10_closure_make’
pats_trans3_env_print_dats.o:(.text+0xc50): first defined here
pats_constraint3_print_dats.o: In function aux_5_clofun': (.text+0xe60): multiple definition of aux_5_clofun’
pats_staexp1_print_dats.o:(.text+0x3f0): first defined here
pats_constraint3_print_dats.o: In function aux_5_closure_make': (.text+0xeb0): multiple definition of aux_5_closure_make’
pats_staexp1_print_dats.o:(.text+0x440): first defined here
pats_constraint3_simplify_dats.o: In function __ats_fun_22_clofun': (.text+0xa10): multiple definition of __ats_fun_22_clofun’
pats_stamp_dats.o:(.text+0x360): first defined here
pats_constraint3_simplify_dats.o: In function __ats_fun_22_closure_make': (.text+0xa40): multiple definition of __ats_fun_22_closure_make’
pats_stamp_dats.o:(.text+0x3a0): first defined here
pats_histaexp_print_dats.o: In function aux_2_clofun': (.text+0xa0): multiple definition of aux_2_clofun’
pats_dynexp1_print_dats.o:(.text+0x100): first defined here
pats_histaexp_print_dats.o: In function aux_2_closure_make': (.text+0xf0): multiple definition of aux_2_closure_make’
pats_dynexp1_print_dats.o:(.text+0x150): first defined here
pats_hidynexp_print_dats.o: In function aux_5_clofun': (.text+0xaa0): multiple definition of aux_5_clofun’
pats_staexp1_print_dats.o:(.text+0x3f0): first defined here
pats_hidynexp_print_dats.o: In function aux_5_closure_make': (.text+0xaf0): multiple definition of aux_5_closure_make’
pats_staexp1_print_dats.o:(.text+0x440): first defined here
pats_typerase_decl_dats.o: In function __ats_fun_22_clofun': (.text+0x9d0): multiple definition of __ats_fun_22_clofun’
pats_stamp_dats.o:(.text+0x360): first defined here
pats_typerase_decl_dats.o: In function __ats_fun_22_closure_make': (.text+0xa00): multiple definition of __ats_fun_22_closure_make’
pats_stamp_dats.o:(.text+0x3a0): first defined here
pats_ccomp_print_dats.o: In function aux_3_clofun': (.text+0x2a0): multiple definition of aux_3_clofun’
pats_staexp2_szexp_dats.o:(.text+0xa0): first defined here
pats_ccomp_print_dats.o: In function aux_3_closure_make': (.text+0x2f0): multiple definition of aux_3_closure_make’
pats_staexp2_szexp_dats.o:(.text+0xf0): first defined here
pats_ccomp_print_dats.o: In function aux_25_clofun': (.text+0x35b0): multiple definition of aux_25_clofun’
pats_utils_dats.o:(.text+0xc20): first defined here
pats_ccomp_print_dats.o: In function aux_25_closure_make': (.text+0x3600): multiple definition of aux_25_closure_make’
pats_utils_dats.o:(.text+0xc70): first defined here
pats_ccomp_hitype_dats.o: In function aux_3_clofun': (.text+0x820): multiple definition of aux_3_clofun’
pats_staexp2_szexp_dats.o:(.text+0xa0): first defined here
pats_ccomp_hitype_dats.o: In function aux_3_closure_make': (.text+0x870): multiple definition of aux_3_closure_make’
pats_staexp2_szexp_dats.o:(.text+0xf0): first defined here
pats_ccomp_tmpvar_dats.o: In function __ats_fun_21_clofun': (.text+0x5c0): multiple definition of __ats_fun_21_clofun’
pats_symmap_dats.o:(.text+0xae0): first defined here
pats_ccomp_tmpvar_dats.o: In function insert_53_clofun': (.text+0x1590): multiple definition of insert_53_clofun’
pats_dynexp2_dcst_dats.o:(.text+0x1440): first defined here
pats_ccomp_tmpvar_dats.o: In function insert_53_closure_make': (.text+0x15e0): multiple definition of insert_53_closure_make’
pats_dynexp2_dcst_dats.o:(.text+0x1480): first defined here
pats_ccomp_d2env_dats.o: In function __ats_fun_4_clofun': (.text+0x120): multiple definition of __ats_fun_4_clofun’
pats_dynexp2_util_dats.o:(.text+0x140): first defined here
pats_ccomp_d2env_dats.o: In function insert_12_clofun': (.text+0x6c0): multiple definition of insert_12_clofun’
pats_symmap_dats.o:(.text+0x780): first defined here
pats_ccomp_d2env_dats.o: In function insert_12_closure_make': (.text+0x700): multiple definition of insert_12_closure_make’
pats_symmap_dats.o:(.text+0x7d0): first defined here
pats_ccomp_funent_dats.o: In function aux_19_clofun': (.text+0x420): multiple definition of aux_19_clofun’
pats_patcst2_dats.o:(.text+0xac0): first defined here
pats_ccomp_funent_dats.o: In function aux_19_closure_make': (.text+0x470): multiple definition of aux_19_closure_make’
pats_patcst2_dats.o:(.text+0xb10): first defined here
pats_ccomp_claulst_dats.o: In function aux_12_clofun': (.text+0xbb0): multiple definition of aux_12_clofun’
pats_dynexp2_dmac_dats.o:(.text+0x330): first defined here
pats_ccomp_claulst_dats.o: In function aux_12_closure_make': (.text+0xc00): multiple definition of aux_12_closure_make’
pats_dynexp2_dmac_dats.o:(.text+0x380): first defined here
prelude_libats.o: In function __ats_fun_29_clofun': (.text+0x2300): multiple definition of __ats_fun_29_clofun’
pats_staexp2_svar_dats.o:(.text+0x850): first defined here
prelude_libats.o: In function __ats_fun_22_clofun': (.text+0x1f90): multiple definition of __ats_fun_22_clofun’
pats_stamp_dats.o:(.text+0x360): first defined here
prelude_libats.o: In function __ats_fun_5_clofun': (.text+0x2f90): multiple definition of __ats_fun_5_clofun’
pats_reader_dats.o:(.text+0x1b0): first defined here
prelude_libats.o: In function __ats_fun_29_closure_make': (.text+0x2320): multiple definition of __ats_fun_29_closure_make’
pats_staexp2_svar_dats.o:(.text+0x890): first defined here
prelude_libats.o: In function __ats_fun_22_closure_make': (.text+0x1fb0): multiple definition of __ats_fun_22_closure_make’
pats_stamp_dats.o:(.text+0x3a0): first defined here
pats_main_dats.o: In function
_2home_2hwxi_2research_2Postiats_2git_2src_2pats_main_2edats__do_transfinal2': (.text+0x1928): undefined reference to alloca’
pats_staexp2_skexp_dats.o: In function
_2home_2hwxi_2research_2Postiats_2git_2src_2pats_staexp2_util_2esats__s2kexp_ismat': (.text+0x1421): undefined reference to alloca’
pats_staexp2_skexp_dats.o: In function
_2home_2hwxi_2research_2Postiats_2git_2src_2pats_staexp2_util_2esats__s2kexplst_ismat': (.text+0x14e1): undefined reference to alloca’
pats_staexp2_szexp_dats.o: In function
_2home_2hwxi_2research_2Postiats_2git_2src_2pats_staexp2_util_2esats__s2zexp_merge': (.text+0x18a1): undefined reference to alloca’
pats_staexp2_util2_dats.o: In function
_2home_2hwxi_2research_2Postiats_2git_2src_2pats_staexp2_util_2esats__s2hnf_syneq': (.text+0xb91): undefined reference to alloca’
pats_staexp2_util2_dats.o:(.text+0xc51): more undefined references to
`alloca’ follow
collect2: ld a retourné 1 code d’état d’exécution

gmhwxi · January 31, 2015, 11:34pm

Okay, I have got eq_dev_dev (and eq_ino_ino) fixed.On Saturday, January 31, 2015 at 6:59:05 AM UTC-5, Yannick Duchêne wrote:

Le samedi 31 janvier 2015 12:07:48 UTC+1, Yannick Duchêne a écrit :
Here is a short test:
 #include <stdio.h>
 #include <sys/types.h>

 typedef int ats_bool_type;
 #define ats_true_bool 1
 #define ats_false_bool 0

 ats_bool_type atslib_eq_dev_dev (dev_t x1, dev_t x2) {
    return (x1 == x2 ? ats_true_bool : ats_false_bool) ;
 } // end of [atslib_eq_dev_dev]

 int main (void) {
    printf("Hello!\n");
    printf("Size of `dev_t is` %i bytes\n", sizeof(dev_t));
    return 0;
 }
Compilation fails with CompCert, even with this short snippet.

If I change the type of x1 and x2 to int, then it compiles, and
says the size of dev_t is 8 bytes.
May be a track.

First I tested two variations.
 typedef struct {
    int a;
    int b;
 } dev_t2;

 typedef long long dev_t3;
If the type of x1 and x2 is dev_t2, it fails with both GCC and
CompCert, and if it is dev_t3 it compiles with both GCC and CompCert.

I suspect a conditional definition which makes dev_t not be defiend the
same when compiling with one or the other.

dev_t is defined as an alias of __dev_t which is defined to be
__DEV_T_TYPE which is defined to be __UQUAD_TYPE, which for machine
with 32 bits words, is defined to be __u_quad_t and here, things may
start to be wrong.

I have this:
 #if __WORDSIZE == 64
    typedef long int __quad_t;
    typedef unsigned long int __u_quad_t;
 #elif defined __GLIBC_HAVE_LONG_LONG
    __extension__ typedef long long int __quad_t;
    __extension__ typedef unsigned long long int __u_quad_t;
 #else
    typedef struct
    {
       long __val[2];
    } __quad_t;
    typedef struct
    {
       __u_long __val[2];
    } __u_quad_t;
 #endif
I guessed when compiling with CompCert, __GLIBC_HAVE_LONG_LONG is false
and it fall back to the struct definition, which does not allow
comparison.

Indeed, compiling with compcert -D__GLIBC_HAVE_LONG_LONG=1 make the
build succeed.

However, that’s a trick, and may be there is a better way, but which
involves modifying ATS1 which is used to generated C files for ATS2 (and
ATS2 if in the future ATS2 is supposed to generate its own C files).

In
<sys/types.h>
nothing is asserted about dev_t. May when nothing assert a type is a
simple type, comparison should be defined using memcmp. This should not
be an issue, as a believe most C compiler will be able to optimize it when
feasible.

What about using memcmp for comparison of C types when these C types
cannot be ensured to be simple type and so may possibly be compound types?

Yannick_Duchene · January 31, 2015, 11:07am

The error “./libc/sys/CATS/types.cats:72: Error: illegal comparison
between types dev_t and dev_t.”, which appears two times, is about this:

typedef dev_t ats_dev_type ; // for device IDs
 ATSinline()
 ats_bool_type
 atslib_eq_dev_dev
   (dev_t x1, dev_t x2) {
   return (x1 == x2 ? ats_true_bool : ats_false_bool) ;
 } // end of [atslib_eq_dev_dev]
Line #72 is the one with “return (x1 == x2 ? ats_true_bool :
ats_false_bool) ;”

I’m surprised with this one: is there a case where C99 disallow a
comparison between two value of the same type? (here, dev_t).

Here is a short test:

 #include <stdio.h>
 #include <sys/types.h>

 typedef int ats_bool_type;
 #define ats_true_bool 1
 #define ats_false_bool 0

 ats_bool_type atslib_eq_dev_dev (dev_t x1, dev_t x2) {
    return (x1 == x2 ? ats_true_bool : ats_false_bool) ;
 } // end of [atslib_eq_dev_dev]

 int main (void) {
    printf("Hello!\n");
    printf("Size of `dev_t is` %i bytes\n", sizeof(dev_t));
    return 0;
 }

Compilation fails with CompCert, even with this short snippet.

If I change the type of x1 and x2 to int, then it compiles, and says
the size of dev_t is 8 bytes.

Yannick_Duchene · January 31, 2015, 12:01pm

Indeed, compiling with compcert -D__GLIBC_HAVE_LONG_LONG=1 make the
build succeed.

To clarify it, I meant the build of the tiny test file, not the build of
ATS2 (I will test it later).

gmhwxi · January 31, 2015, 6:36pm

Hi Yannick,

This is all great!

It does seem quite plausible that we will be able to use compcert to
compile ATS in the
near future.

Could you also try to use compcert to compile some examples of C code
generated by ATS2?

For instance, the examples in the following directory are good ones:

These examples should give us a rough idea as to how compcert is compared
with gcc/clang in
terms of the efficiency of the generated object code.

Many thanks!On Saturday, January 31, 2015 at 5:15:20 AM UTC-5, Yannick Duchêne wrote:

After some quick and easy tweaks, I’m getting this, and as it’s in C files
probably generated by ATS1, I feel to guess I can’t fix, and it suggest
something would have to be tweaked in the C source generator.
 \
 make -j4 -C src/CBOOT \
 CCOMP=compcert GCFLAG=-D_ATS_NGC \
 CFLAGS= LDFLAGS= patsopt
 make[1]: entrant dans le répertoire « 
/home/yannick/Applications/Third_Parties/ATS/ATS2-Postiats-0.1.8/src/CBOOT »
compcert -I. -I./ccomp/runtime -c -o pats_main_dats.o pats_main_dats.c
compcert -I. -I./ccomp/runtime -c -o pats_utils_sats.o
pats_utils_sats.c
compcert -I. -I./ccomp/runtime -c -o pats_location_sats.o
pats_location_sats.c
compcert -I. -I./ccomp/runtime -c -o pats_jsonize_sats.o
pats_jsonize_sats.c
./ccomp/runtime/ats_types.h:68: Warning: empty struct.
./ccomp/runtime/ats_types.h:68: Warning: empty struct.
./ccomp/runtime/ats_types.h:68: Warning: empty struct.
compcert -I. -I./ccomp/runtime -c -o pats_errmsg_sats.o
pats_errmsg_sats.c
./libc/sys/CATS/types.cats:72: Error: illegal comparison between
types dev_t
and dev_t.
Fatal error; compilation aborted.
1 error detected.
make[1]: *** [pats_utils_sats.o] Erreur 2
make[1]: *** Attente des tâches non terminées…
./ccomp/runtime/ats_types.h:68: Warning: empty struct.
./ccomp/runtime/ats_types.h:68: Warning: empty struct.
prelude/CATS/bool.cats:45: Warning:
redefinition of ‘ats_exit_errmsg’ with incompatible type.
libc/sys/CATS/types.cats:72: Error: illegal comparison between types
dev_t
and dev_t.
Fatal error; compilation aborted.
1 error detected.
make[1]: *** [pats_main_dats.o] Erreur 2
make[1]: quittant le répertoire «
/home/yannick/Applications/Third_Parties/ATS/ATS2-Postiats-0.1.8/src/CBOOT »
make: *** [src2_patsopt] Erreur 2

Note the current directory for these messages, seems to be “src/CBOOT”.

The warning “./ccomp/runtime/ats_types.h:68: Warning: empty struct.”,
which appears five times, is about this:
 typedef struct{} ats_empty_type ;
OK, that’s just a warning.

The error “./libc/sys/CATS/types.cats:72: Error: illegal comparison
between types dev_t and dev_t.”, which appears two times, is about this:

typedef dev_t ats_dev_type ; // for device IDs
 ATSinline()
 ats_bool_type
 atslib_eq_dev_dev
   (dev_t x1, dev_t x2) {
   return (x1 == x2 ? ats_true_bool : ats_false_bool) ;
 } // end of [atslib_eq_dev_dev]
Line #72 is the one with “return (x1 == x2 ? ats_true_bool :
ats_false_bool) ;”

I’m surprised with this one: is there a case where C99 disallow a
comparison between two value of the same type? (here, dev_t).

Yannick_Duchene · January 31, 2015, 12:34pm

To clarify it, I meant the build of the tiny test file, not the build of
ATS2 (I will test it later).

Proceeding does not expose the previous error, but I get another one which
I can’t figure how to solve.

I get this error: “/usr/include/asm-generic/int-ll64.h:19: syntax error.”

At /usr/include/asm-generic/int-ll64.h:19 , I have this:

 typedef __signed__ char __s8;

Side note: I noticed CompCert also returns syntax error on undefined types,
but this does not seems to be the case here.

According to The GNU C Reference Manual ,
__signed__ is a GNU extension to C, so may be the headers must be told to
conform to C99, may be defining another macro on the command line, but I
don’t know which one. Some one who know GCC lib well have an idea?

Yannick_Duchene · January 31, 2015, 8:47pm

I’m stuck with a “syntax error” in integer_fixed.cats at line 58, the
line “typedef int64_t atstype_int64 ;”

As CompCert seems to complain about syntax error when it encounters an
undefined type, my guess is that it does not see the definition of the
atstype_int64.

Sorry, I meant it does not see a definition for int64_t. I wanted to go
on, manually editing the file to change it into long long, but I have
another error in “pointer.cats” at line 112. It complains “illegal pointer
arithmetic in binary ‘-’ ”. The C source at that location is:

 ATSinline()
 atstype_ssize
 atspre_sub_ptr_ptr
   (atstype_ptr p1, atstype_ptr p2) { return (p1 - p2) ; }
 // end of [atspre_sub_ptr_ptr]
 #define atspre_sub_ptr0_ptr0 atspre_sub_ptr_ptr
 #define atspre_sub_ptr1_ptr1 atspre_sub_ptr_ptr

So it sees an issue with “return (p1 - p2) ;”

To be sure, I tried to compile this simple test file:

 #include <sys/types.h>

 typedef ssize_t atstype_ssize;
 typedef void* atstype_ptr;

 atstype_ssize
 atspre_sub_ptr_ptr
   (atstype_ptr p1, atstype_ptr p2) { return (p1 - p2) ; }
 // end of [atspre_sub_ptr_ptr]

And it complains the same, that is “test.c:8: Error: illegal pointer
arithmetic in binary ‘-’.”

GCC does not complain with this test file.

Topic		Replies	Views
CompCert for compiling C generated from ATS Google Group	5	421	February 1, 2015
ATS2-0.1.6 released (fwd) Google Group	0	272	January 6, 2015
ATS2-0.1.9 released Google Group	0	318	February 28, 2015
Ats2-0.2.0 Google Group	7	497	June 13, 2015
ATS2-0.0.7 released Google Group	0	331	March 31, 2014

Trying to build ATS2 with CompCert

Related Topics