Re: Hack in gcc/c-decl.c?

[Mike Stump <mrs at apple dot com>]

On Dec 29, 2005, at 2:20 PM, Domagoj D wrote:
> In the case anybody cares about code verifiability... It's  
> exteremely hard
> to automatically prove the correctness of the code that uses pointer
> arithmetic and casts as in the example above.

It is but a couple of trivial rules that one should have anyway...

> Proving more interesting properties like
>
> enum ftype tx;
> float fx;
> ... (assign to tx and fx)
> assert(get_coef(set_coef(tx, fx)) == fx);
>
> would be even harder.

Trivial enough for the compiler.  The only stumbling block might be  
caused by the failure to inline the indirect call to offset.   Seems  
trivial enough to fix up:

static inline int zero() { return 0; }

int bar() {
  int (*func)() = zero;
  return func();
}

currently gives:

_zero:
        li r3,0
        blr
_bar:
        b _zero

which, as I read it,  is trivial.  Notice that in:

enum ftype {T1, T2, T3};

static struct coefs {
  float c[3];
  int (*offset_callback)(enum ftype t);
} filter_s;

static inline int offset(enum ftype t) __attribute__((pure,const));
inline int offset(enum ftype t) {
  int off = 0;
  switch (t) {
  case T1: return off;
  case T2: return off + sizeof(float);
  case T3: return off + 2*sizeof(float);
  }
}

static inline void init(void) {
  filter_s.offset_callback = offset;
}

static inline float get_coef(enum ftype t) {
  return *(float *)((char *)&filter_s + filter_s.offset_callback(t));
}

static inline enum ftype set_coef(enum ftype t, float val) {
  *(float *)((char *)&filter_s + filter_s.offset_callback(t)) = val;
  return t;
}

void foo();
void boo() {
  enum ftype tx;
  float fx;
  fx = 1.0;
  tx = T1;
  init();
  if (filter_s.offset_callback != offset)
    if (get_coef(set_coef(tx, fx)) != fx)
      foo();
}

there is no call to foo.  If one removes the != offset conditional  
and works around the lack of the inlining I pointed out by calling  
offset directly, there still is no call to foo.  If the compiler can  
prove something, I'd expect and hope that a system built to prove  
things would not be worse.  What the compiler doesn't do, is prove  
the general property, rather, given a specific value for tx, it can  
prove equality, but it doesn't need a specific value of fx to do this.