#include <klee/klee.h>

int same(char *a, char *b, size_t size)
{
  size_t i;
  for (i = 0; i < size; i++) {
    if (a[i] != b[i]) {
      return 0;
    }
  }
  return 1;
}

int base64encode(const void* data_buf, size_t dataLength, char* result, size_t* rsultSize);

int main(int argc, char *argv[])
{
  int error;
  size_t src_len = 14;
  char *src = "Hello, world!";
  char dest[30];
  size_t dest_size;
  char new_dest[30];
  size_t new_dest_size;
  char new_src[14]; /* <-- Keep your eye on the ball */

  /* Encode src to dest */  
  base64encode(src, src_len, dest, &dest_size);

  /* Tell KLEE to go wild on the new_src */
  klee_make_symbolic(new_src, src_len, "new_src");

  /* Encode new_src to new_dest */
  error = base64encode(new_src, src_len, new_dest, &new_dest_size);

  /* No way the result would be the same as for src, right? */
  klee_assert(!(!error &&
                new_dest_size == dest_size &&
                same(new_dest, dest, new_dest_size)));
}

/* Base64 encoder from here:
 * https://en.wikibooks.org/wiki/Algorithm_Implementation/Miscellaneous/Base64#C 
 * Minor change to return encoded size in *rsultSize (just for convenience).
 */
int base64encode(const void* data_buf, size_t dataLength, char* result, size_t* rsultSize)
{
   size_t resultSize = *rsultSize;
   const char base64chars[] = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/";
   const uint8_t *data = (const uint8_t *)data_buf;
   size_t resultIndex = 0;
   size_t x;
   uint32_t n = 0;
   int padCount = dataLength % 3;
   uint8_t n0, n1, n2, n3;

   /* increment over the length of the string, three characters at a time */
   for (x = 0; x < dataLength; x += 3) 
   {
      /* these three 8-bit (ASCII) characters become one 24-bit number */
      n = ((uint32_t)data[x]) << 16; //parenthesis needed, compiler depending on flags can do the shifting before conversion to uint32_t, resulting to 0
      
      if((x+1) < dataLength)
         n += ((uint32_t)data[x+1]) << 8;//parenthesis needed, compiler depending on flags can do the shifting before conversion to uint32_t, resulting to 0
      
      if((x+2) < dataLength)
         n += data[x+2];

      /* this 24-bit number gets separated into four 6-bit numbers */
      n0 = (uint8_t)(n >> 18) & 63;
      n1 = (uint8_t)(n >> 12) & 63;
      n2 = (uint8_t)(n >> 6) & 63;
      n3 = (uint8_t)n & 63;
            
      /*
       * if we have one byte available, then its encoding is spread
       * out over two characters
       */
      if(resultIndex >= resultSize) return 1;   /* indicate failure: buffer too small */
      result[resultIndex++] = base64chars[n0];
      if(resultIndex >= resultSize) return 1;   /* indicate failure: buffer too small */
      result[resultIndex++] = base64chars[n1];

      /*
       * if we have only two bytes available, then their encoding is
       * spread out over three chars
       */
      if((x+1) < dataLength)
      {
         if(resultIndex >= resultSize) return 1;   /* indicate failure: buffer too small */
         result[resultIndex++] = base64chars[n2];
      }

      /*
       * if we have all three bytes available, then their encoding is spread
       * out over four characters
       */
      if((x+2) < dataLength)
      {
         if(resultIndex >= resultSize) return 1;   /* indicate failure: buffer too small */
         result[resultIndex++] = base64chars[n3];
      }
   }  

   /*
    * create and add padding that is required if we did not have a multiple of 3
    * number of characters available
    */
   if (padCount > 0) 
   { 
      for (; padCount < 3; padCount++) 
      { 
         if(resultIndex >= resultSize) return 1;   /* indicate failure: buffer too small */
         result[resultIndex++] = '=';
      } 
   }
   if(resultIndex >= resultSize) return 1;   /* indicate failure: buffer too small */
   result[resultIndex] = 0;
   *rsultSize = resultIndex + 1;
   return 0;   /* indicate success */
}