--- layout: fc_discuss_archives title: Message 81 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Small function with Shifting



Claude Marche schrieb:
> You are assuming that every true property is provable.
>
> SMT provers have almost no knowledge of shift operations, so you need 
> to give hints to them under the form of a lemma.
> Here is your example below, slightly modified/simplified.
>
> The lemma itself is not proved of course, you have to convince 
> yourself of its truth by other means: from human review to use of a 
> proof assistant.
>
> - Claude
>
> #pragma JessieIntegerModel(math)
>
> typedef struct s1 { unsigned int mantissa; int exponent; };
>
> /*@ lemma shift_prop: \forall integer x,y;
>      y >= 8 ==>
>      (x << 8) * (1 << (y-8)) == x * (1 << y);
> */
>
> /*@ requires \valid(e);
>  @ requires 0 < e->mantissa < 10;
>  @ requires 10 < e->exponent < 20;
>  @ ensures
>  @   e->mantissa * (1 << e->exponent) == \old(e->mantissa * (1 << 
> e->exponent));
> */
> int sizetype_normalize(struct s1* e) {
>     unsigned int min_mantissa = 1 << 21;
>     if (e->mantissa < min_mantissa) {
>       e->mantissa <<= 8;
>       e->exponent -= 8;
>   }
>
>   return 0;
> }
>

Using the lemma as a "precondition" worked for the example, although I'm 
not yet alltogether content with it,since it is not a totally formal 
prove of course. But thank you for the hint.

I then tried it with the next part myself, with another lemma. It didn't 
work, though i think I used the technique the same way you did:

#pragma JessieIntegerModel(math)

typedef struct s1 { unsigned int mantissa; int exponent; };

/*@ lemma shift_prop: \forall integer x,y;
     y >= 8 ==>
     (x << 8) * (1 << (y-8)) == x * (1 << y);
*/

/*@ lemma shift_prop2: \forall integer x,y;
    ((x >> 3) + 1) * (1 << (y + 3)) >= x * (1 << y);
*/

/*@ requires \valid(e);
@ ensures  e->mantissa * (1 << e->exponent) >= \old(e->mantissa * (1 << 
e->exponent));
*/
int sizetype_normalize(struct s1* e) {
    unsigned int min_mantissa = 1 << 21;
    unsigned int max_mantissa = 1 << 29;
    if (e->mantissa < min_mantissa) {
      e->mantissa <<= 8;
      e->exponent -= 8;
  }
    if (e->mantissa >= max_mantissa) {
        e->mantissa = (e->mantissa >> 3) + 1;
        e->exponent += 3;
    }

  return 0;
}

Could you explain to me what is wrong here? Lemma2 states (in my 
opinion) exactly what is done in the second if-condition.