`memcmp`

function from this Tor diff using Frama-C. The `loop_precondition`

is what I'm stuck on./*@ predicate IsValidRange( unsigned char *a, integer n ) = @ ( 0 <= n ) && \valid_range( a, 0, n - 1 ); @*/ /*@ requires \valid(x) && \valid(y); @ assigns nothing; @ @ behavior zero_length: @ assumes len == 0; @ ensures \result == 0; @ @ behavior equal: @ assumes len > 0; @ assumes x_y_equal : \forall integer n; @ 0 <= n < len ==> x[n] == y[n]; @ requires IsValidRange(x, len); @ requires IsValidRange(y, len); @ ensures \result == 0; @ @ behavior not_equal: @ assumes len > 0; @ assumes x_y_not_equal : \exists integer n; @ 0 <= n < len ==> x[n] != y[n]; @ requires IsValidRange(x, len); @ requires IsValidRange(y, len); @ ensures \result != 0; @ @ complete behaviors zero_length, equal, not_equal; @ disjoint behaviors zero_length, equal, not_equal; @*/ int tor_memcmp(const unsigned char *x, const unsigned char *y, unsigned int len) { unsigned int i = len; int retval = 0, newval; if (len == 0) return 0; while (i--) { //@ assert loop_precondition: (retval == 0) || (\exists integer n; i < n < len && x[i] != y[i]); int v1 = x[i]; int v2 = y[i]; int equal_p = v1 ^ v2; //@ assert (x[i] == y[i] && equal_p == 0) || (x[i] != y[i] && 0 < equal_p <= 255); // relies on two's complement! --equal_p; //@ assert (x[i] == y[i] && equal_p == -1) || (x[i] != y[i] && 0 <= equal_p < 255); // relies on signed right shift! equal_p >>= 8; //@ assert (x[i] == y[i] && equal_p == -1) || (x[i] != y[i] && equal_p =>= 0); newval = retval & equal_p; //@ assert (x[i] == y[i] && retval == newval) || (x[i] != y[i] && newval == 0); retval = newval; newval = retval + (v1 - v2); //@ assert (x[i] == y[i] && newval == retval) || (x[i] != y[i] && newval == (v1 - v2)); retval = newval; } return retval; }

## 0 comments:

## Post a Comment