contract for sign_extend function

Jun 22, 2011 at 7:33 PM
Edited Jun 23, 2011 at 4:57 PM


I am having some trouble coming up with a suitable contract for a sign_extend function.  The function is:


static i32 sign_extend(u32 value, u32 sign_bit)   
    _(requires sign_bit < 31)   
    _(requires value < (1<<sign_bit+1))
    if(IS_BIT_SET(value, sign_bit))
        value = value | (0xffffffff << sign_bit); 

    return (i32) _(unchecked) value;


And I used this function on elements from a wrapped object that have invariants set on the maximum size.  The preconditions I have set work well if I use a sign bit that is too small (and in fact already found a bug in my code that did exactly that), but I would also like to know that there exists a value that could be equal to (1<<(sign_bit+1))-1 for a particular invocation of this function to catch any uses of this function where I use a sign bit that is too large.



struct control {
    u32 inst;
    u32 K; _(invariant \this->K == (\this->inst & 0xffff))

sign_extend(cont->K, 15); // correct
sign_extend(cont->K, 14); // bug I found
sign_extend(cont->K, 16); // bugs I would like to find