assembly_gmp.1.res.oracle

[kernel] Parsing assembly_gmp.c (with preprocessing)
/* Generated by Frama-C */
#include "stddef.h"
typedef long mp_limb_t;
typedef unsigned long UDItype;
typedef long *mp_srcptr;
typedef size_t mp_size_t;
void ADDC_LIMB(mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t);

void udiv_rnnd_preinv(mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t);

mp_limb_t mpn_mod_1_1p(mp_srcptr ap, mp_size_t n, mp_limb_t b,
                       mp_limb_t const bmodb[4])
{
  mp_limb_t __retres;
  int cnt;
  mp_limb_t bi;
  mp_limb_t r0;
  mp_limb_t r1;
  mp_limb_t r;
  r0 = *(ap + (n - (mp_size_t)2));
  r1 = *(ap + (n - (mp_size_t)1));
  if (n > (mp_size_t)2) {
    mp_limb_t B2modb;
    mp_limb_t B2mb;
    mp_limb_t p0;
    mp_limb_t p1;
    mp_limb_t r2;
    mp_size_t j;
    B2modb = *(bmodb + 3);
    B2mb = B2modb - b;
    {
      UDItype __m0 = (UDItype)r1;
      UDItype __m1 = (UDItype)B2modb;
      /*@ assigns p1;
          assigns p1 \from r1, B2modb; */
      __asm__ ("umulh %r1,%2,%0" : "=r" (p1) : "%rJ" (r1), "rI" (B2modb));
      p0 = (mp_limb_t)(__m0 * __m1);
    }
    /*@ assigns r2, r1, r0;
        assigns r2 \from r0, p1, *(ap + (mp_size_t)(n - 3)), p0;
        assigns r1 \from r0, p1, *(ap + (mp_size_t)(n - 3)), p0;
        assigns r0 \from r0, p1, *(ap + (mp_size_t)(n - 3)), p0;
    */
    __asm__ (
      "add\t%6, %q2\n\t"
      "adc\t%4, %q1\n\t"
      "sbb\t%q0, %q0"
      : "=r" (r2), "=r" (r1), "=&r" (r0)
      : "1" ((UDItype)r0), "rme" ((UDItype)p1),
        "%2" ((UDItype)*(ap + (n - (mp_size_t)3))), "rme" ((UDItype)p0)
      );
    j = n - (mp_size_t)4;
    while (j >= (mp_size_t)0) {
      {
        mp_limb_t cy;
        {
          UDItype __m0_0 = (UDItype)r1;
          UDItype __m1_0 = (UDItype)B2modb;
          /*@ assigns p1;
              assigns p1 \from r1, B2modb; */
          __asm__ ("umulh %r1,%2,%0" : "=r" (p1) : "%rJ" (r1), "rI" (B2modb));
          p0 = (mp_limb_t)(__m0_0 * __m1_0);
        }
        ADDC_LIMB(cy,r0,r0,r2 & B2modb);
        r0 -= - cy & b;
        /*@ assigns r2, r1, r0;
            assigns r2 \from r0, p1, *(ap + j), p0;
            assigns r1 \from r0, p1, *(ap + j), p0;
            assigns r0 \from r0, p1, *(ap + j), p0;
        */
        __asm__ (
          "add\t%6, %q2\n\t"
          "adc\t%4, %q1\n\t"
          "sbb\t%q0, %q0"
          : "=r" (r2), "=r" (r1), "=&r" (r0)
          : "1" ((UDItype)r0), "rme" ((UDItype)p1),
            "%2" ((UDItype)*(ap + j)), "rme" ((UDItype)p0)
          );
      }
      j --;
    }
    r1 -= r2 & b;
  }
  cnt = (int)*(bmodb + 1);
  if (cnt != 0) {
    mp_limb_t t;
    mp_limb_t B1modb = *(bmodb + 2);
    {
      UDItype __m0_1 = (UDItype)r1;
      UDItype __m1_1 = (UDItype)B1modb;
      /*@ assigns r1;
          assigns r1 \from r1, B1modb; */
      __asm__ ("umulh %r1,%2,%0" : "=r" (r1) : "%rJ" (r1), "rI" (B1modb));
      t = (mp_limb_t)(__m0_1 * __m1_1);
    }
    r0 += t;
    r1 += (mp_limb_t)(r0 < t);
    r1 = (r1 << cnt) | (r0 >> (64 - cnt));
    r0 <<= cnt;
  }
  else {
    mp_limb_t mask = - ((mp_limb_t)(r1 >= b));
    r1 -= mask & b;
  }
  bi = *(bmodb + 0);
  udiv_rnnd_preinv(r,r1,r0,b,bi);
  __retres = r >> cnt;
  return __retres;
}

int loc[10];
void f(void)
{
  unsigned long ulValue;
  unsigned long *pulValue = & ulValue;
  /*@ assigns loc[0 .. 9];
      assigns loc[0 .. 9] \from loc[0 .. 9]; */
  __asm__ ("sidt %0\n" :  : "m" (loc));
  /*@ assigns *(pulValue + (..));
      assigns *(pulValue + (..))
        \from (indirect: pulValue), *(pulValue + (..));
  */
  __asm__ ("movq $36, (%0)" :  : "r" (pulValue));
  int a = 2;
  int b = 3;
  /*@ assigns a;
      assigns a \from b; */
  __asm__ ("mov %1, %0" : "=r" (a) : "r" (b) : "%eax");
  return;
}