/* Sets the location in memory where a frame should be stored.  This value is written into a software register
 * in the vision core and then incremented as bursting takes place.  Because this value is used during a 
 * frame capture, it SHOULD NOT be changed while the core is in operation.
 * @param frame_id int type of frame address to be set.  Currently we only capture one frame, so there is only
                       one choice, VISION_FRAME_RGB565, but more frame types can be added here so multiple images
							  can be saved for each frame
 * @param frameAddr int memory address where this frame type should be saved.  Make sure this memory address
                        has been properly malloc'ed before passing it to the core.
*/
void SetFrameAddress(Xuint32 frame_id, Xuint32 frameAddr)
{
	int offset = 0x0;
	switch(frame_id)
	{
		case VISION_FRAME_RGB565:
			offset = OFFSET_ORG_FRAME_MEM_ADDR;
			break;
		/*case VISION_FRAME_GRAYSCALE8: //this is just an example, this fifo is not built into hardware
			offset = OFFSET_SEG_FRAME_MEM_ADDR;
			break;*/
		default:
			return;
	}
	*PTR(BASEADDR + offset) = frameAddr;
}

/* Optimized naHash_get for looking up local variables (OP_LOCAL is by
 * far the most common opcode and deserves some special case
 * optimization).  Assumes that the key is an interned symbol
 * (i.e. the hash code is precomputed, and we only need to test for
 * pointer identity). */
int naiHash_sym(struct naHash* hash, struct naStr* sym, naRef* out)
{
    HashRec* hr = hash->rec;
    if(hr) {
        int* tab = TAB(hr);
        HashEnt* ents = ENTS(hr);
        unsigned int hc = sym->hashcode;
        int cell, mask = POW2(hr->lgsz+1) - 1, step = (2*hc+1) & mask;
        for(cell=HBITS(hr,hc); tab[cell] != ENT_EMPTY; cell=(cell+step)&mask)
            if(tab[cell]!=ENT_DELETED && sym==PTR(ents[tab[cell]].key).str) {
                *out = ents[tab[cell]].val;
                return 1;
            }
    }
    return 0;
}

/* Create a fake mpz consisting of just a single 1 bit, with totbits being
   the total number of bits, inclusive of that 1 bit.  */
void
mpz_fake_bits (mpz_ptr z, unsigned long totbits)
{
  static mp_limb_t  n;
  unsigned long     zero_bits, zero_limbs;

  zero_bits = totbits - 1;
  zero_limbs = zero_bits / GMP_NUMB_BITS;
  zero_bits %= GMP_NUMB_BITS;

  SIZ(z) = zero_limbs + 1;
  PTR(z) = (&n) - (SIZ(z) - 1);
  n = CNST_LIMB(1) << zero_bits;

  ASSERT_ALWAYS (mpz_sizeinbase (z, 2) == totbits);
}

void
mpz_array_init (mpz_ptr arr, mp_size_t arr_size, mp_size_t nbits)
{
  mp_ptr p;
  mp_size_t i;
  mp_size_t nlimbs;

  nlimbs = nbits / GMP_NUMB_BITS + 1;
  p = __GMP_ALLOCATE_FUNC_LIMBS (arr_size * nlimbs);

  for (i = 0; i < arr_size; i++)
    {
      ALLOC (&arr[i]) = nlimbs + 1; /* Yes, lie a little... */
      SIZ (&arr[i]) = 0;
      PTR (&arr[i]) = p + i * nlimbs;
    }
}

/* this function is useful in debug mode to print residues */
static void
mpres_print (mpres_t x, char* name, mpmod_t n)
{
  mp_size_t m, xn;
  mpres_t t;
  mpres_init(t, n);
  mpz_set_ui(t, 1);
  mpres_mul (t, x, t, n);

  xn = SIZ(t);
  m = ABSIZ(t);
  MPN_NORMALIZE(PTR(t), m);
  SIZ(t) = xn >= 0 ? m : -m;
  gmp_printf ("%s=%Zd\n", name, t);
  SIZ(t) = xn;
  mpres_clear (t, n);
}

/* generate nbits random bits into mp[], assuming mp was allocated to contain
   a sufficient number of limbs */
void
mpfr_rand_raw (mpfr_limb_ptr mp, gmp_randstate_t rstate,
               mpfr_prec_t nbits)
{
  mpz_t z;

  MPFR_ASSERTN (nbits >= 1);
  /* To be sure to avoid the potential allocation of mpz_urandomb */
  ALLOC(z) = SIZ(z) = MPFR_PREC2LIMBS (nbits);
  PTR(z)   = mp;
#if __MPFR_GMP(5,0,0)
  /* Check for integer overflow (unless mp_bitcnt_t is signed,
     but according to the GMP manual, this shouldn't happen).
     Note: mp_bitcnt_t has been introduced in GMP 5.0.0. */
  MPFR_ASSERTN ((mp_bitcnt_t) -1 < 0 || nbits <= (mp_bitcnt_t) -1);
#endif
  mpz_urandomb (z, rstate, nbits);
}

/* Whether the absolute value of z is a power of 2. */
int
mpz_pow2abs_p (mpz_srcptr z)
{
  mp_size_t  size, i;
  mp_srcptr  ptr;

  size = SIZ (z);
  if (size == 0)
    return 0;  /* zero is not a power of 2 */
  size = ABS (size);

  ptr = PTR (z);
  for (i = 0; i < size-1; i++)
    if (ptr[i] != 0)
      return 0;  /* non-zero low limb means not a power of 2 */

  return POW2_P (ptr[i]);  /* high limb power of 2 */
}

int
mpz_invert (mpz_ptr inverse, mpz_srcptr x, mpz_srcptr n)
{
  mpz_t gcd, tmp;
  mp_size_t xsize, nsize, size;
  TMP_DECL;

  xsize = ABSIZ (x);
  nsize = ABSIZ (n);

  /* No inverse exists if the leftside operand is 0.  Likewise, no
     inverse exists if the mod operand is 1.  */
  if (xsize == 0 || (nsize == 1 && (PTR (n))[0] == 1))
    return 0;

  size = MAX (xsize, nsize) + 1;
  TMP_MARK;

  MPZ_TMP_INIT (gcd, size);
  MPZ_TMP_INIT (tmp, size);
  mpz_gcdext (gcd, tmp, (mpz_ptr) 0, x, n);

  /* If no inverse existed, return with an indication of that.  */
  if (!MPZ_EQUAL_1_P (gcd))
    {
      TMP_FREE;
      return 0;
    }

  /* Make sure we return a positive inverse.  */
  if (SIZ (tmp) < 0)
    {
      if (SIZ (n) < 0)
	mpz_sub (inverse, tmp, n);
      else
	mpz_add (inverse, tmp, n);
    }
  else
    mpz_set (inverse, tmp);

  TMP_FREE;
  return 1;
}

/* As above, a special naHash_set for setting local variables.
 * Assumes that the key is interned, and also that it isn't already
 * present in the hash. */
void naiHash_newsym(struct naHash* hash, naRef* sym, naRef* val)
{
    HashRec* hr = hash->rec;
    int mask, step, cell, ent;
    struct naStr *s = PTR(*sym).str;
    if(!hr || hr->next >= POW2(hr->lgsz))
        hr = resize(hash);
    mask = POW2(hr->lgsz+1) - 1;
    step = (2*s->hashcode+1) & mask;
    cell = HBITS(hr, s->hashcode);
    while(TAB(hr)[cell] != ENT_EMPTY)
        cell = (cell + step) & mask;
    ent = hr->next++;
    if(ent >= NCELLS(hr)) return; /* race protection, don't overrun */
    TAB(hr)[cell] = ent;
    hr->size++;
    ENTS(hr)[TAB(hr)[cell]].key = *sym;
    ENTS(hr)[TAB(hr)[cell]].val = *val;
}

void
mpz_ui_sub (mpz_ptr w, unsigned long int uval, mpz_srcptr v)
{
  mp_ptr vp, wp;
  mp_size_t vn, wn;
  mp_limb_t cy;

#if GMP_NAIL_BITS != 0
  if (uval > GMP_NUMB_MAX)
    {
      mpz_t u;
      mp_limb_t ul[2];
      PTR(u) = ul;
      ul[0] = uval & GMP_NUMB_MASK;
      ul[1] = uval >> GMP_NUMB_BITS;
      SIZ(u) = 2;
      mpz_sub (w, u, v);
      return;
    }

unsigned long int
mpz_tdiv_ui (mpz_srcptr dividend, unsigned long int divisor)
{
  mp_size_t ns, nn;
  mp_ptr np;
  mp_limb_t rl;

  if (divisor == 0)
    DIVIDE_BY_ZERO;

  ns = SIZ(dividend);
  if (ns == 0)
    {
      return 0;
    }

  nn = ABS(ns);
  np = PTR(dividend);

#if BITS_PER_ULONG > GMP_NUMB_BITS  /* avoid warnings about shift amount */
  if (divisor > GMP_NUMB_MAX)
    {
      mp_limb_t dp[2], rp[2];
      mp_ptr qp;
      mp_size_t rn;
      TMP_DECL;

      if (nn == 1)		/* tdiv_qr requirements; tested above for 0 */
	{
	  rl = np[0];
	  return rl;
	}

      TMP_MARK;
      dp[0] = divisor & GMP_NUMB_MASK;
      dp[1] = divisor >> GMP_NUMB_BITS;
      qp = TMP_ALLOC_LIMBS (nn - 2 + 1);
      mpn_tdiv_qr (qp, rp, (mp_size_t) 0, np, nn, dp, (mp_size_t) 2);
      TMP_FREE;
      rl = rp[0] + (rp[1] << GMP_NUMB_BITS);
      rn = 2 - (rp[1] == 0);  rn -= (rp[rn - 1] == 0);
    }

int
_mpz_cmp_si (mpz_srcptr u, signed long int v_digit)
{
  mp_size_t usize = u->_mp_size;
  mp_size_t vsize;
  mp_limb_t u_digit;

#if GMP_NAIL_BITS != 0
  /* FIXME.  This isn't very pretty.  */
  mpz_t tmp;
  mp_limb_t tt[2];
  PTR(tmp) = tt;
  ALLOC(tmp) = 2;
  mpz_set_si (tmp, v_digit);
  return mpz_cmp (u, tmp);
#endif

  vsize = 0;
  if (v_digit > 0)
    vsize = 1;
  else if (v_digit < 0)
    {
      vsize = -1;
      v_digit = -v_digit;
    }

  if (usize != vsize)
    return usize - vsize;

  if (usize == 0)
    return 0;

  u_digit = u->_mp_d[0];

  if (u_digit == (mp_limb_t) (unsigned long) v_digit)
    return 0;

  if (u_digit > (mp_limb_t) (unsigned long) v_digit)
    return usize;
  else
    return -usize;
}

// reading and writing through a pointer field
int main(void) {
    struct st *p;
    p = __VERIFIER_nondet_st();

    assume(p > 0);
    BASE_PTR(p);

    if (p->x == 42) {
        if (p->next != 0) {
            PTR(p->next, sizeof(struct st));
            p->next->y = 474;
            if (p->next->x == 526) {
                if (p->next->x + p->next->y == 1000) {
                    __VERIFIER_error();
                }
            }
        }
    }
    return 0;
}

unsigned long int
mpz_gcd_ui (mpz_ptr w, mpz_srcptr u, unsigned long int v)
{
  mp_size_t un;
  mp_limb_t res;

#if BITS_PER_ULONG > GMP_NUMB_BITS  /* avoid warnings about shift amount */
  if (v > GMP_NUMB_MAX)
    {
      mpz_t vz;
      mp_limb_t vlimbs[2];
      vlimbs[0] = v & GMP_NUMB_MASK;
      vlimbs[1] = v >> GMP_NUMB_BITS;
      PTR(vz) = vlimbs;
      SIZ(vz) = 2;
      mpz_gcd (w, u, vz);
      /* because v!=0 we will have w<=v hence fitting a ulong */
      ASSERT (mpz_fits_ulong_p (w));
      return mpz_get_ui (w);
    }

void
mpz_lcm_ui (mpz_ptr r, mpz_srcptr u, mpir_ui v)
{
  mp_size_t      usize;
  mp_srcptr      up;
  mp_ptr         rp;
  mpir_ui         g;
  mp_limb_t      c;

#if BITS_PER_UI > GMP_NUMB_BITS  /* avoid warnings about shift amount */
  if (v > GMP_NUMB_MAX)
    {
      mpz_t vz;
      mp_limb_t vlimbs[2];
      vlimbs[0] = v & GMP_NUMB_MASK;
      vlimbs[1] = v >> GMP_NUMB_BITS;
      PTR(vz) = vlimbs;
      SIZ(vz) = 2;
      mpz_lcm (r, u, vz);
      return;
    }

void
mpf_set_d (mpf_ptr r, double d)
{
  int negative;

  DOUBLE_NAN_INF_ACTION (d,
                         __gmp_invalid_operation (),
                         __gmp_invalid_operation ());

  if (UNLIKELY (d == 0))
    {
      SIZ(r) = 0;
      EXP(r) = 0;
      return;
    }
  negative = d < 0;
  d = ABS (d);

  SIZ(r) = negative ? -LIMBS_PER_DOUBLE : LIMBS_PER_DOUBLE;
  EXP(r) = __gmp_extract_double (PTR(r), d);
}

static void
refmpz_mul (mpz_t w, const mpz_t u, const mpz_t v)
{
  mp_size_t usize = u->_mp_size;
  mp_size_t vsize = v->_mp_size;
  mp_size_t wsize;
  mp_size_t sign_product;
  mp_ptr up, vp;
  mp_ptr wp;
  mp_size_t talloc;

  sign_product = usize ^ vsize;
  usize = ABS (usize);
  vsize = ABS (vsize);

  if (usize == 0 || vsize == 0)
    {
      SIZ (w) = 0;
      return;
    }

  talloc = usize + vsize;

  up = u->_mp_d;
  vp = v->_mp_d;

  wp = __GMP_ALLOCATE_FUNC_LIMBS (talloc);

  if (usize > vsize)
    refmpn_mul (wp, up, usize, vp, vsize);
  else
    refmpn_mul (wp, vp, vsize, up, usize);
  wsize = usize + vsize;
  wsize -= wp[wsize - 1] == 0;
  MPZ_REALLOC (w, wsize);
  MPN_COPY (PTR(w), wp, wsize);

  SIZ(w) = sign_product < 0 ? -wsize : wsize;
  __GMP_FREE_FUNC_LIMBS (wp, talloc);
}

// Recursive print function - updates buf_index as appropriate
// during its traversal of c
static int print(cell c) {
    switch (TYPE(c)) {
    case PAIR:
        if (TYPE(car(c)) == PAIR) {
            catf("(");
            print(car(c));
            catf(")");
        } else
            print(car(c));
        if (!cdr(c)) return 0;

        catf(" ");
        if (TYPE(cdr(c)) != PAIR) catf(". ");
        return print(cdr(c));
    case S64:
    case S32:
        return catf("%ld", INT_VAL(c));
    case SYMBOL:
        return catf("%s", SYM_STR(c));
    case NATIVE_FN:
    case NATIVE_FN_TCO:
    case NATIVE_MACRO:
        return catf("NATIVE_FUNCTION<%p>", PTR(c));
    case FFI_SYM:
        return catf("FFI_SYM<%p>", PTR(c));
    case FFI_FN:
        return catf("FFI_FN<%p>", PTR(c));
    case FFI_LIBRARY:
        return catf("FFI_LIBRARY<%p>", PTR(c));
    case MACRO:
        catf("(macro (");
        goto print_args_body;
    case FN:
        catf("(lambda (");
    print_args_body:
        print(((fn_t*)PTR(c))->args);
        catf(") ");
        print(((fn_t*)PTR(c))->body);
        return catf(")");
    case CONS:
        return catf("CONS");
    case NIL:
        return catf("()");
    default:
        return catf("UNKNOWN<%p>", c);
    }
}

lispobj
alloc_string(const char *str)
{
    int k;
    int len = strlen(str);
    lispobj result = alloc_vector(type_SimpleString, len + 1, 16);
    struct vector *vec = (struct vector *) PTR(result);
    unsigned short int *wide_char_data;

    vec->length = make_fixnum(len);
    wide_char_data = (unsigned short int*) vec->data;
    for (k = 0; k < len; ++k) {
        wide_char_data[k] = str[k] & 0xff;
    }

#if 0
    fprintf(stderr, "alloc-string: 0x%lx %d -> `%s'\n",
            result, len, str);
#endif
    
    return result;
}

void
mpz_neg (mpz_ptr w, mpz_srcptr u)
{
  mp_ptr wp;
  mp_srcptr up;
  mp_size_t usize, size;

  usize = SIZ (u);

  if (u != w)
    {
      size = ABS (usize);

      wp = MPZ_NEWALLOC (w, size);

      up = PTR (u);

      MPN_COPY (wp, up, size);
    }

  SIZ (w) = -usize;
}