Skip to content
Snippets Groups Projects
gnu-asm-aesni.res.oracle 5.35 KiB
Newer Older
[kernel] Parsing tests/syntax/gnu-asm-aesni.c (with preprocessing)
[kernel:asm:clobber] tests/syntax/gnu-asm-aesni.c:93: Warning: 
  Clobber list contains "memory" argument. Assuming no side effects beyond those mentioned in operands.
/* Generated by Frama-C */
#include "__fc_builtin.h"
#include "string.h"
#include "strings.h"
typedef unsigned short byte;
union __anonunion_PROPERLY_ALIGNED_TYPE_1 {
   int a ;
   short b ;
   char c[1] ;
   long d ;
   float f ;
   double g ;
};
typedef union __anonunion_PROPERLY_ALIGNED_TYPE_1 PROPERLY_ALIGNED_TYPE;
union __anonunion_u1_3 {
   PROPERLY_ALIGNED_TYPE dummy ;
   byte keyschedule[14 + 1][4][4] ;
};
union __anonunion_u2_4 {
   PROPERLY_ALIGNED_TYPE dummy ;
   byte keyschedule[14 + 1][4][4] ;
};
struct __anonstruct_RIJNDAEL_context_2 {
   union __anonunion_u1_3 u1 ;
   union __anonunion_u2_4 u2 ;
   int rounds ;
   unsigned int decryption_prepared : 1 ;
   unsigned int use_aesni : 1 ;
};
typedef struct __anonstruct_RIJNDAEL_context_2 RIJNDAEL_context;
__inline static void do_aesni_enc(RIJNDAEL_context const *ctx,
                                  unsigned char *b, unsigned char const *a)
{
  /*@ assigns *b, ctx->u1.keyschedule[0 .. 14];
      assigns *b \from *a, ctx->rounds;
      assigns ctx->u1.keyschedule[0 .. 14] \from *a, ctx->rounds;
  */
  __asm__ volatile (
    "movdqu %[src], %%xmm0\n\t"
    "movdqa (%[key]), %%xmm1\n\t"
    "pxor   %%xmm1, %%xmm0\n\t"
    "movdqa 0x10(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x20(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x30(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x40(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x50(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x60(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x70(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x80(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x90(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0xa0(%[key]), %%xmm1\n\t"
    "cmpl $10, %[rounds]\n\t"
    "jz .Lenclast%=\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0xb0(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0xc0(%[key]), %%xmm1\n\t"
    "cmpl $12, %[rounds]\n\t"
    "jz .Lenclast%=\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0xd0(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0xe0(%[key]), %%xmm1\n"
    ".Lenclast%=:\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdd, 0xc1\n\t"
    "movdqu %%xmm0, %[dst]\n"
    : [dst] "=m" (*b)
    : [src] "m" (*a), [key] "r" (ctx->u1.keyschedule),
      [rounds] "r" (ctx->rounds)
    : "cc", "memory"
    );
  return;
}

extern int ( /* missing proto */ Frama_C_dump_each)();

void encrypt_aesni(void)
{
  RIJNDAEL_context ctx;
  unsigned char b[64];
  unsigned char a[64];
  unsigned char test;
  int i;
  int j;
  int k;
  unsigned char a_init[64] =
    {(unsigned char)0x85,
     (unsigned char)0x50,
     (unsigned char)0x43,
     (unsigned char)0xda,
     (unsigned char)0x06,
     (unsigned char)0x99,
     (unsigned char)0xd8,
     (unsigned char)0x3b,
     (unsigned char)0x65,
     (unsigned char)0xf7,
     (unsigned char)0x1d,
     (unsigned char)0xf7,
     (unsigned char)0x95,
     (unsigned char)0xd4,
     (unsigned char)0x34,
     (unsigned char)0x5d,
     (unsigned char)0x6e,
     (unsigned char)0x21,
     (unsigned char)0x01,
     (unsigned char)0xba,
     (unsigned char)0x2a,
     (unsigned char)0xbd,
     (unsigned char)0x7f,
     (unsigned char)0xab,
     (unsigned char)0xa7,
     (unsigned char)0x6d,
     (unsigned char)0xe7,
     (unsigned char)0xcd,
     (unsigned char)0x72,
     (unsigned char)0xcf,
     (unsigned char)0xce,
     (unsigned char)0xa1,
     (unsigned char)0xa7,
     (unsigned char)0x4a,
     (unsigned char)0xb8,
     (unsigned char)0x12,
     (unsigned char)0xef,
     (unsigned char)0x2d,
     (unsigned char)0x6b,
     (unsigned char)0xd5,
     (unsigned char)0xdc,
     (unsigned char)0x09,
     (unsigned char)0xb9,
     (unsigned char)0xdd,
     (unsigned char)0x09,
     (unsigned char)0x27,
     (unsigned char)0x7c,
     (unsigned char)0x86,
     (unsigned char)0x35,
     (unsigned char)0x60,
     (unsigned char)0x99,
     (unsigned char)0xea,
     (unsigned char)0x72,
     (unsigned char)0xbb,
     (unsigned char)0x93,
     (unsigned char)0x9e,
     (unsigned char)0x9e,
     (unsigned char)0x16,
     (unsigned char)0x7b,
     (unsigned char)0xd4,
     (unsigned char)0x8c,
     (unsigned char)0x81,
     (unsigned char)0x8a,
     (unsigned char)0x53};
  memcpy((void *)(a),(void const *)(a_init),
         (unsigned int)64 * sizeof(unsigned char));
  i = 0;
  while (i < 14 + 1) {
    j = 0;
    while (j < 4) {
      k = 0;
      while (k < 4) {
        Frama_C_make_unknown((char *)(& ctx.u1.keyschedule[i][j][k]),
                             sizeof(byte));
        k ++;
      }
      j ++;
    }
    i ++;
  }
  ctx.rounds = 12;
  ctx.use_aesni = (unsigned int)1;
  do_aesni_enc((RIJNDAEL_context const *)(& ctx),b,
               (unsigned char const *)(a));
  test = (unsigned char)0x00U;
  i = 0;
  while (i < 64) {
    test = (unsigned char)((int)test ^ (int)b[i]);
    i ++;
  }
  Frama_C_dump_each();
  return;
}