#! /usr/bin/env python3

def print_input_parameters (acc, a, b):
    for i in range (0x30):
        print ('uint8 {0}{1:02x}'.format (acc, i),
               end = ',\n' if i%4 == 3 else ', ')
    for i in range (0x30):
        print ('uint8 {0}{1:02x}'.format (a, i),
               end = ',\n' if i%4 == 3 else ', ')
    print ('uint8 {0}'.format (b))

def print_initialization (baseacc, acc, basea, a, b):
    for i in range (0x30):
        print ('mov L0x{0:x} {1}{2:02x};'.format (baseacc+i, acc, i),
               end = '\n' if i % 3 == 2 or i == 0x30-1 else '')
    for i in range (0x30):
        print ('mov L0x{0:x} {1}{2:02x};'.format (basea+i, a, i),
               end = '\n' if i % 3 == 2 or i == 0x30-1 else '')
    print ('mov rdx b;')
    print ('\n\nnondet rax@uint64; nondet rcx@uint64;')
    print ('nondet rdi@uint64; nondet rsi@uint64;')

def print_constants (base, values):
    for i in range (len (values)):
        print ('mov L0x{0:x} 0x{1:02x}@uint8;'.format (base + i, values[i]),
               end = '\n' if i % 2 == 1 or i == len (values) - 1 else '')

def print_outputs (base, r):
    for i in range (0x30):
        print ('mov {0}{1:02x} L0x{2:x};'.format (r, i, base + i),
               end = '\n' if i % 3 == 2 else '')
    print ()

print ('(**************** input parameters ****************)\n')
print_input_parameters ('acc', 'a', 'b')

print ('\n(**************** initialization ****************)\n')
print_initialization (0x7fffffffa460, 'acc', 0x7fffffffa490, 'a', 'b')

print ('\n(**************** constants ****************)\n')
print_constants (0x555555566020,
                 [1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1])
print ()
print_constants (0x555555566030,
                 [15,15,15,15,15,15,15,15, 15,15,15,15,15,15,15,15])
print ()
print_constants (0x555555568080,
                 [0x00,0x01,0x02,0x03,0x04,0x05,0x06,0x07,
                  0x08,0x09,0x0a,0x0b,0x0c,0x0d,0x0e,0x0f,
                  0x00,0x10,0x20,0x30,0x40,0x50,0x60,0x70,
                  0x80,0x90,0xa0,0xb0,0xc0,0xd0,0xe0,0xf0,

                  0x00,0x02,0x04,0x06,0x08,0x0a,0x0c,0x0e,
                  0x10,0x12,0x14,0x16,0x18,0x1a,0x1c,0x1e,
                  0x00,0x20,0x40,0x60,0x80,0xa0,0xc0,0xe0,
                  0x1b,0x3b,0x5b,0x7b,0x9b,0xbb,0xdb,0xfb,

                  0x00,0x04,0x08,0x0c,0x10,0x14,0x18,0x1c,
                  0x20,0x24,0x28,0x2c,0x30,0x34,0x38,0x3c,
                  0x00,0x40,0x80,0xc0,0x1b,0x5b,0x9b,0xdb,
                  0x36,0x76,0xb6,0xf6,0x2d,0x6d,0xad,0xed,

                  0x00,0x08,0x10,0x18,0x20,0x28,0x30,0x38,
                  0x40,0x48,0x50,0x58,0x60,0x68,0x70,0x78,
                  0x00,0x80,0x1b,0x9b,0x36,0xb6,0x2d,0xad,
                  0x6c,0xec,0x77,0xf7,0x5a,0xda,0x41,0xc1,

                  0x00,0x10,0x20,0x30,0x40,0x50,0x60,0x70,
                  0x80,0x90,0xa0,0xb0,0xc0,0xd0,0xe0,0xf0,
                  0x00,0x1b,0x36,0x2d,0x6c,0x77,0x5a,0x41,
                  0xd8,0xc3,0xee,0xf5,0xb4,0xaf,0x82,0x99,

                  0x00,0x20,0x40,0x60,0x80,0xa0,0xc0,0xe0,
                  0x1b,0x3b,0x5b,0x7b,0x9b,0xbb,0xdb,0xfb,
                  0x00,0x36,0x6c,0x5a,0xd8,0xee,0xb4,0x82,
                  0xab,0x9d,0xc7,0xf1,0x73,0x45,0x1f,0x29,

                  0x00,0x40,0x80,0xc0,0x1b,0x5b,0x9b,0xdb,
                  0x36,0x76,0xb6,0xf6,0x2d,0x6d,0xad,0xed,
                  0x00,0x6c,0xd8,0xb4,0xab,0xc7,0x73,0x1f,
                  0x4d,0x21,0x95,0xf9,0xe6,0x8a,0x3e,0x52,

                  0x00,0x80,0x1b,0x9b,0x36,0xb6,0x2d,0xad,
                  0x6c,0xec,0x77,0xf7,0x5a,0xda,0x41,0xc1,
                  0x00,0xd8,0xab,0x73,0x4d,0x95,0xe6,0x3e,
                  0x9a,0x42,0x31,0xe9,0xd7,0x0f,0x7c,0xa4])

print ('\n(**************** outputs ****************)\n')
print_outputs (0x7fffffffa490, 'r')

