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.
