clightgen -fbitfields -dclight may generate incorrect code

[codyroux]

The following code:

struct foo { int bar : 2; int baz : 2;};

/*
  PRE: r not NULL
  POST: r->baz == l && r->bar == r_old->bar
 */
void set_baz(struct foo * r, int l) {
  r->baz = l;
  return;
}

int main(void){

  struct foo my_record;

  my_record.bar = 0;
  my_record.baz = 0;

  set_baz(&my_record, 42);

  return 0;
}

After running clightgen -v -fbitfields -dclight foo.c, gives:

struct foo;
struct foo {
  unsigned char __bf1;
};

extern unsigned int __compcert_va_int32(void *);
extern unsigned long long __compcert_va_int64(void *);
extern double __compcert_va_float64(void *);
extern void *__compcert_va_composite(void *, unsigned int);
extern long long __compcert_i64_dtos(double);
extern unsigned long long __compcert_i64_dtou(double);
extern double __compcert_i64_stod(long long);
extern double __compcert_i64_utod(unsigned long long);
extern float __compcert_i64_stof(long long);
extern float __compcert_i64_utof(unsigned long long);
extern long long __compcert_i64_sdiv(long long, long long);
extern unsigned long long __compcert_i64_udiv(unsigned long long, unsigned long long);
extern long long __compcert_i64_smod(long long, long long);
extern unsigned long long __compcert_i64_umod(unsigned long long, unsigned long long);
extern long long __compcert_i64_shl(long long, int);
extern unsigned long long __compcert_i64_shr(unsigned long long, int);
extern long long __compcert_i64_sar(long long, int);
extern long long __compcert_i64_smulh(long long, long long);
extern unsigned long long __compcert_i64_umulh(unsigned long long, unsigned long long);
extern void __builtin_debug(int, ...);
void set_baz(struct foo *, int);
int main(void);
void set_baz(struct foo *r, int l)
{
  register struct foo *$58;
  $58 = $56;
  (*$58).__bf1 = (*$58).__bf1 & ~12U | (unsigned int) $57 << 2U & 12U;
  return;
}

int main(void)
{
  struct foo my_record;
  my_record.__bf1 = my_record.__bf1 & ~3U | (unsigned int) 0 << 0U & 3U;
  my_record.__bf1 = my_record.__bf1 & ~12U | (unsigned int) 0 << 2U & 12U;
  set_baz(&my_record, 42);
  return 0;
  return 0;
}

Which has some undeclared variables $56 and $57 (presumably refering to the set_baz function arguments).

The version of clightgen is 3.5, built off of current master.

[bschommer]

The output of clightgen is fine and works for me. You are referring to the debugging output of Clight which uses a C like syntax.

[codyroux]

Correct, I am referring to the contents of foo.light.c, which should probably be valid C code?

[xavierleroy]

CompCert's -dclight output is a best effort: it tries to look like valid C code, but it's not always possible, because a few constructs of Clight are actually more general than the corresponding C constructs. The main purpose of the -d outputs is to understand what the compiler is doing, and in the case of clightgen what Clight code was generated in the output .v file.

This being said, there was a mistake in the way clightgen -dclight prints function parameters. This should now be fixed.

[codyroux]

Fantastic! I see why having C light and C differ would be useful, and I greatly appreciate the bug fix, unfortunately embedded code tends to make intensive use of bitfields and it's nice to have the pretty-printed syntax for sanity checking.