Trying to build ATS2 with CompCert

[Yannick Duchêne]

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 Duchêne]

Le samedi 31 janvier 2015 11:15:20 UTC+1, Yannick Duchêne a écrit : 

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 Duchêne]

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 http://pubs.opengroup.org/onlinepubs/009695399/basedefs/sys/types.h.html  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 Duchêne]

Le samedi 31 janvier 2015 12:59:05 UTC+1, Yannick Duchêne a écrit :

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

[Yannick Duchêne]

Le samedi 31 janvier 2015 13:01:40 UTC+1, Yannick Duchêne a écrit :

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 http://www.gnu.org/software/gnu-c-manual/gnu-c-manual.html , `__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 Duchêne]

Le samedi 31 janvier 2015 13:34:34 UTC+1, Yannick Duchêne a écrit :

According to http://www.gnu.org/software/gnu-c-manual/gnu-c-manual.html , `__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

[Yannick Duchêne]

Le samedi 31 janvier 2015 14:02:28 UTC+1, Yannick Duchêne a écrit :

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]

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!

[Yannick Duchêne]

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.

 

[Hongwei Xi]

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?

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

[Hongwei Xi]

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

--

[Yannick Duchêne]

Le samedi 31 janvier 2015 20:30:58 UTC+1, gmhwxi a écrit :

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

[Yannick Duchêne]

Le samedi 31 janvier 2015 21:24:26 UTC+1, Yannick Duchêne a écrit :

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.

[Shea Levy]

> On Jan 31, 2015, at 11:59 AM, 'Yannick Duchêne' via ats-lang-users <ats-lan...@googlegroups.com> 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.

[gmhwxi]

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

Will make changes shortly.

[gmhwxi]

Okay, I have got eq_dev_dev (and eq_ino_ino) fixed.