#include <yafl_rnt.h>
#include <assert.h>
#include <stdlib.h>

#define PARAM_STACK_SIZE   64
#define OLD_STACK_SIZE     4096
#define OLD_STACK_LEVELS   1024
#define PARAM_STACK_LEVELS 8

                
#define HASPRE_FIELD 1
#define HASPOST_FIELD 2
#define SET_HASPRE(x)  {x ->has_precond = x ->has_precond | HASPRE_FIELD;}
#define SET_HASPOST(x) {x ->has_precond = x ->has_precond | HASPOST_FIELD;}
#define HASPRE(x)  (x ->has_precond & HASPRE_FIELD)
#define HASPOST(x) (x ->has_precond & HASPOST_FIELD)

#define MAX_ASSERT_ERRORS 64
static uint  assert_errors[MAX_ASSERT_ERRORS];
static char* assert_module[MAX_ASSERT_ERRORS];
static char* assert_class[MAX_ASSERT_ERRORS];
static int nb_assert_errors;

stack_elem  old_elems[OLD_STACK_SIZE];
int         old_levels[OLD_STACK_LEVELS];
stack_elem  param_elems[PARAM_STACK_SIZE];                
int         param_levels[PARAM_STACK_LEVELS];
assert_stack  old_stack,
              param_stack;

static AssertStackInit = FALSE;
static AssertBusy = FALSE;

void dump_XRMEs YPARAMS2(minimal_dual *, dual)
{
  METHOD_INFO *tmp, **ptr;
  int i;

  assert(dual != NULL);
  assert(dual->class_name != NULL);
  printf("DUMP: XRME (%s)\n", dual->class_name); 
  printf("DUMP: dual size (%d) minimal (%d)\n", dual->dual_size, sizeof(minimal_dual)); 
  if (dual->XRMEs) {
    printf("DUMP:\n");
	ptr = (METHOD_INFO **)dual->XRMEs;
	printf ("DUMP: ptr (%d)\n", ptr);
	ptr = (METHOD_INFO **)((char*)ptr + sizeof(minimal_dual));
	printf ("DUMP: ptr+sizeof(minimal_dual) = (%d)\n", ptr);
    for (; ptr < (METHOD_INFO**)((char*)dual->XRMEs + dual->dual_size);
         ptr++) {
      printf("XRME: (%d) = (%d) \n", ptr, *ptr);
      }
    }
  else {
    printf("DUMP: problem\n");
    }
}

void init_XRMEs YPARAMS2(minimal_dual *, dual)
{
  minimal_dual *xrmes, *d;
  METHOD_INFO *tmp, **ptr;

  assert (dual != NULL);
  assert (dual->class_name != NULL);
/*   printf("TRACE: init_XRME for (%s)\n", dual->class_name); */
  dual->XRMEs = malloc(dual->dual_size);
  if (!dual->XRMEs) {
    garbage_collect();
	/* retry the malloc*/
    dual->XRMEs = malloc(dual->dual_size);
	assert (dual->XRMEs != NULL);
    }
  xrmes = dual->XRMEs;
  y_memset(xrmes,0,dual->dual_size);
  d = dual;
  while (d != NULL) {
    tmp = d->first_method;
    while (tmp != NULL) {
      if (tmp->offset != 0) {
	    ptr = (METHOD_INFO **)xrmes;
		ptr = (METHOD_INFO**)((char*)ptr + tmp->offset);
        if (*ptr == NULL) {
		  *ptr = tmp;
          }
        }
      tmp = tmp->next;
      }
	d = d->inherited;
    }
}


METHOD_INFO *find_XRME YPARAMS4(obj_ptr, Y_THIS, METHOD_INFO*, meth)
{
  minimal_dual *dual_ptr;
  METHOD_INFO *result; 

  assert(Y_THIS != NULL);
  assert(meth != NULL);

  result = NULL;
/*   printf("TRACE: find_XRME (%s.%s)\n", meth->class->class_name, meth->name); */
  /* For predefined method, we do not need to use the dynamic type of the object.
     We just use the static type (this intend to solve problems with call to BASE
     when the call to pre- and post- conditions is inlined in the method,
     not in the anchor). */
  if ((meth->offset != 0) && (meth->offset >= sizeof(minimal_dual)) ) {
    dual_ptr = (minimal_dual *)((((header*)(Y_THIS))-1)->dual);
    if (dual_ptr) {
      if (!dual_ptr->XRMEs) {
	    init_XRMEs(dual_ptr);
        }
	  assert(dual_ptr->XRMEs != NULL);

/*	  dump_XRMEs(dual_ptr); */

	  result = *((METHOD_INFO**)((char*)dual_ptr->XRMEs + meth->offset));
      }
    else {
      printf("WARNING: no dual pointer\n");
	  result = NULL;
      }
	}
  else {
	result = meth;
    }
  return result;
}


void assert_stack_init()
{
/*   printf("TRACE: assert_stack_init \n"); */

   AssertStackInit      = TRUE;
   old_stack.elems      = old_elems;
   old_stack.max_size   = OLD_STACK_SIZE;
   old_stack.size       = 0;
   old_stack.max_level  = OLD_STACK_LEVELS;
   old_stack.nb_level   = 0;
   old_stack.levels     = old_levels;

/*   printf("TRACE: old_stack = %d\n",  &old_stack);  */

   param_stack.elems     = param_elems;
   param_stack.max_size  = PARAM_STACK_SIZE;
   param_stack.size      = 0;
   param_stack.max_level = PARAM_STACK_LEVELS;
   param_stack.nb_level  = 0;
   param_stack.levels    = param_levels;

/*   printf("TRACE: param_stack = %d\n",  &param_stack); */

}


void assert_stack_push_int YPARAMS4(assert_stack*, the_stack, yint, val)
{
/*   printf("TRACE: assert_stack_push_int \n"); */

  if (!AssertStackInit) {
    assert_stack_init();
    }
  the_stack->elems[the_stack->size].the_int = val;
  the_stack->size++;
  assert (the_stack->size < the_stack->max_size);
}


void assert_stack_push_obj YPARAMS4(assert_stack*, the_stack, obj_ptr, val)
{
/*   printf("TRACE: assert_stack_push_obj \n"); */

/*   printf("TRACE: assert_stack_push_obj (stack= %d , size= %d) \n", the_stack, the_stack->size); */

  if (!AssertStackInit) {
    assert_stack_init();
    }
  the_stack->elems[the_stack->size].the_obj = val;
  the_stack->size++;
  assert (the_stack->size < the_stack->max_size);
}


void assert_stack_push_char YPARAMS4(assert_stack*, the_stack, ychar, val)
{
/*   printf("TRACE: assert_stack_push_char \n"); */

  if (!AssertStackInit) {
    assert_stack_init();
    }
  the_stack->elems[the_stack->size].the_char = val;
  the_stack->size++;
  assert (the_stack->size < the_stack->max_size);
}


void assert_stack_push_double YPARAMS4(assert_stack*, the_stack, double, val)
{
/*   printf("TRACE: assert_stack_push_double \n"); */

  if (!AssertStackInit) {
    assert_stack_init();
    }
  the_stack->elems[the_stack->size].the_double = val;
  the_stack->size++;
  assert (the_stack->size < the_stack->max_size);
}


obj_ptr assert_stack_pop_obj YPARAMS2(assert_stack*, the_stack)
{
/*   printf("TRACE: assert_stack_pop_obj \n"); */

  the_stack->size--;
  assert (the_stack->size >= 0);
  return the_stack->elems[the_stack->size].the_obj;
}


yint assert_stack_pop_int YPARAMS2(assert_stack*, the_stack)
{
/*   printf("TRACE: assert_stack_pop_int \n"); */

  the_stack->size--;
  assert (the_stack->size >= 0);
  return the_stack->elems[the_stack->size].the_int;
}


ychar assert_stack_pop_char YPARAMS2(assert_stack*, the_stack)
{
/*   printf("TRACE: assert_stack_pop_char \n"); */

  the_stack->size--;
  assert (the_stack->size >= 0);
  return the_stack->elems[the_stack->size].the_char;
}


double assert_stack_pop_double YPARAMS2(assert_stack*, the_stack)
{
/*   printf("TRACE: assert_stack_pop_double \n"); */

  the_stack->size--;
  assert (the_stack->size >= 0);
  return the_stack->elems[the_stack->size].the_double;
}


obj_ptr assert_stack_top_obj YPARAMS2(assert_stack*, the_stack)
{
/*   printf("TRACE: assert_stack_top_obj \n"); */

  assert (the_stack->size > 0);
  return the_stack->elems[the_stack->size-1].the_obj;
}


yint assert_stack_top_int YPARAMS2(assert_stack*, the_stack)
{
/*   printf("TRACE: assert_stack_top_int \n"); */

  assert (the_stack->size > 0);
  return the_stack->elems[the_stack->size-1].the_int;
}


ychar assert_stack_top_char YPARAMS2(assert_stack*, the_stack)
{
/*   printf("TRACE: assert_stack_top_char \n"); */

  assert (the_stack->size > 0);
  return the_stack->elems[the_stack->size-1].the_char;
}


double assert_stack_top_double YPARAMS2(assert_stack*, the_stack)
{
/*   printf("TRACE: assert_stack_top_double \n"); */

  assert (the_stack->size > 0);
  return the_stack->elems[the_stack->size-1].the_double;
}


obj_ptr assert_stack_get_obj YPARAMS4(assert_stack*, the_stack, int, offset)
{
/*   printf("TRACE: assert_stack_get_obj (stack= %d, size= %d, offset= %d) \n", the_stack, the_stack->size, offset); */

  assert (the_stack->size >= offset);
  return the_stack->elems[the_stack->size-offset].the_obj;
}


yint assert_stack_get_int YPARAMS4(assert_stack*, the_stack, int, offset)
{
/*   printf("TRACE: assert_stack_get_int \n"); */

  assert (the_stack->size >= offset);
  return the_stack->elems[the_stack->size-offset].the_int;
}


ychar assert_stack_get_char YPARAMS4(assert_stack*, the_stack, int, offset)
{
/*   printf("TRACE: assert_stack_get_char \n"); */

  assert (the_stack->size >= offset);
  return the_stack->elems[the_stack->size-offset].the_char;
}


double assert_stack_get_double YPARAMS4(assert_stack*, the_stack, int, offset)
{
/*   printf("TRACE: assert_stack_get_double \n"); */

  assert (the_stack->size >= offset);
  return the_stack->elems[the_stack->size-offset].the_double;
}


void assert_stack_push_level YPARAMS2(assert_stack*, the_stack)
{
/*   printf("TRACE: assert_stack_push_level (%d = %d)\n", the_stack, the_stack->nb_level ); */

  if (!AssertStackInit) {
    assert_stack_init();
    }
  assert(the_stack != NULL);
  assert (the_stack->levels != NULL);
  the_stack->levels[the_stack->nb_level] = the_stack->size;
  the_stack->nb_level++;
  assert (the_stack->nb_level <= the_stack->max_level);
}


void assert_stack_pop_level YPARAMS2(assert_stack*, the_stack)
{
/*  printf("TRACE: assert_stack_pop_level (%d = %d)\n",  the_stack, the_stack->nb_level ); */

  assert (the_stack->nb_level > 0);
  assert (the_stack->levels[the_stack->nb_level-1] <= the_stack->size);
  the_stack->nb_level--;
  the_stack->size = the_stack->levels[the_stack->nb_level];
}




void decode_errors YPARAMS4(char *, mes_header, char *, methname)
{
  int i, j;

/*   printf("TRACE: decode_errors \n"); */


  assert(sizeof(uint) == 4);
  assert(methname != NULL);
  printf("%s\n", mes_header);
  for (i=0; i < nb_assert_errors; i++){
    if (assert_errors[i]) {
      printf("%s.%s.%s: (Imp) ", assert_module[i], assert_class[i], methname);
      for (j=0; j<16; j++) {
        if (TEST_BIT(assert_errors[i], j)) {
          printf("%d ", j+1);
          }
        }
      printf(" (Def) ");
      for (j=16; j<32; j++) {
        if (TEST_BIT(assert_errors[i], j)) {
          printf("%d ", j-15);
          }
        }
      printf("\n");
      }
    }
}


void check_pre_cond  YPARAMS4(obj_ptr, Y_THIS, METHOD_INFO*, meth)
{
  YINT         (*cf_meth_ptr)();
  YINT         (*cd_meth_ptr)();
  METHOD_INFO   *m;
  unsigned     cf_res, cd_res;
  int          the_end, prec_ok;
  int          level_has_one, has_one;

/*  printf("TRACE: check_pre_cond (%d)\n", meth); */
  if (((meth != NULL) && (!AssertBusy)) && (HASPRE(meth))) {
/*     printf("TRACE: check_pre_cond (%s.%s)\n", meth->class->class_name, meth->name); */

    AssertBusy = TRUE;
    nb_assert_errors = 0;

    m = find_XRME (Y_THIS, meth);
    the_end = FALSE;
    prec_ok = FALSE;
    has_one = FALSE;
    while ((m != NULL) && !the_end) {
      cf_meth_ptr = m->pre_context_free;
      cd_meth_ptr = m->pre_context_dep;
      if (cf_meth_ptr) {
        level_has_one = TRUE;
        cf_res = (*cf_meth_ptr)(Y_THIS);
        }
      else {
        level_has_one = FALSE;
		  cf_res = 0;
        }
      if (cd_meth_ptr) {
        level_has_one = TRUE;
        cd_res = (*cd_meth_ptr)(Y_THIS);
        }
		else {
		  cd_res = 0;
		  }
      assert_errors[nb_assert_errors] = cd_res | cf_res;
	  assert(m->class != NULL);
	  assert(m->class->class_name != NULL);
      assert_class[nb_assert_errors] = m->class->class_name;
	  assert(m->class->module_name != NULL);
      assert_module[nb_assert_errors] = m->class->module_name;
      nb_assert_errors++;
      assert(nb_assert_errors < MAX_ASSERT_ERRORS);
      the_end = level_has_one && !(cd_res | cf_res);
      if (!the_end){
        if (m->base == m) {
          m = NULL;
          }
        else {
          m = m->base;
          }
        }
      else {
	    prec_ok = TRUE;
	    }
	  has_one = has_one || level_has_one;
      }
    if ((!prec_ok) && (has_one)) {
      decode_errors("PreCondition Failed", meth->name);
      fail_prec();
      }
    AssertBusy = FALSE;
    }
}


void check_post_conditions YPARAMS4(obj_ptr, Y_THIS, METHOD_INFO*, meth)
{
  YINT         (*meth_ptr)();
  METHOD_INFO   *m;
  YINT         res;
  int          failed;

/*   printf("TRACE: check_post_cond \n"); */

  if (((meth != NULL) && (!AssertBusy)) && (HASPOST(meth))) {
/*    printf("TRACE: check_post_cond (%s.%s) ", meth->class->class_name, meth->name); 
	if (meth->has_precond) {
	  printf(" has precond\n");
	  }
	else {
	  printf(" has no precond\n");
	  }*/
/*    printf("TRACE: check_post_cond (%s.%s)\n", meth->class->class_name, meth->name); */
    AssertBusy = TRUE;
    nb_assert_errors = 0;
    m = find_XRME (Y_THIS, meth);
    failed = FALSE;
    while (m != NULL) {
      meth_ptr = m->post_func;
      if (meth_ptr) {
        res = (*meth_ptr)(Y_THIS);
        }
		else {
		  res = 0;
		  }
      assert_errors[nb_assert_errors] = res;
	  assert(m->class != NULL);
	  assert(m->class->class_name != NULL);
      assert_class[nb_assert_errors] = m->class->class_name;
	  assert(m->class->module_name != NULL);
      assert_module[nb_assert_errors] = m->class->module_name;
      nb_assert_errors++;
      failed = failed || res;
		if (m->base == m) {
		  m = NULL;
		  }
		else {
          m = m->base;
		  }
      }
    if (failed) {
      decode_errors("PostCondition Failed", meth->name);
      fail_post();
      }
    /* we pop the level here, it has been pushed by the compute_old_expression function */
    assert_stack_pop_level(&old_stack);
    AssertBusy = FALSE;
    }
}


void rec_compute_old YPARAMS4(obj_ptr, Y_THIS, METHOD_INFO*, meth)
{
  void (*meth_ptr)();

/*   printf("TRACE: rec_compute_old \n"); */

  if (meth != NULL) {
    if ((meth->base != NULL) && (meth->base != meth)) {
        /* recursive call to compute old expressions for all methods
           defined for this entry. */
        rec_compute_old (Y_THIS, meth->base);
        }
    meth_ptr = meth->compute_old;
    if (meth_ptr) {
      (*meth_ptr)(Y_THIS);
      }
	}
}


void compute_old_expressions YPARAMS4(obj_ptr, Y_THIS, METHOD_INFO*, meth)
{
  void (*meth_ptr)();
  METHOD_INFO   *m;

/*   printf("TRACE: compute_old_expressions \n"); */

  if (((meth != NULL) && (!AssertBusy)) && (HASPOST(meth))) {
    /* we push the level here, and we pop it after the evaluation of the postcondition */
    assert_stack_push_level(&old_stack);
    AssertBusy = TRUE;
    m = find_XRME(Y_THIS, meth);
	rec_compute_old(Y_THIS, m);
    AssertBusy = FALSE;
	}
}


METHOD_INFO *find_method_on_offset YPARAMS4(minimal_dual*, d,
                                           unsigned, offset)
{
  METHOD_INFO *result, *tmp;

/*   printf("TRACE: find_method_on_offset \n"); */

  result = NULL;
  if ((d != NULL) && (offset)) {
    tmp = d->first_method;
    while (tmp != NULL) {
      if (tmp->offset == offset) {
        result = tmp;
        tmp = NULL;
        }
      else {
        tmp = tmp->next;
        }
      }
    }
  return result;
}

void set_has_precond YPARAMS8(minimal_dual*, class,
                              unsigned, offset,
                              unsigned, has_pre,
                              unsigned, has_post)
{
  minimal_dual *d;
  METHOD_INFO  *p;

  assert (class != NULL);
  d = class;
  while(d != NULL) {
    p = find_method_on_offset(d, offset);
    if (p != NULL) {
	  if (has_pre) {
	    SET_HASPRE(p);
	    }
	  if (has_post) {
	    SET_HASPOST(p);
	    }
	  /*p->has_precond = TRUE;*/
      }
	if (d->first_son != NULL) {
  	  set_has_precond(d->first_son, offset, has_pre, has_post);
	  }
    d = d->brother;
    }
}

void attach_derived_method YPARAMS8(METHOD_INFO*, meth,
                                    unsigned, offset,
                                    METHOD_INFO*, base,
                                    minimal_dual*, class)
{
  minimal_dual *d;
  METHOD_INFO  *p;

/*   printf("TRACE: attach_derived_method \n"); */

  assert (class != NULL);
  assert (meth != NULL);
  d = class;
  while(d != NULL) {
    if (offset == 0) {
	  printf("%s . %s : offset is NULL\n", meth->class->class_name, meth->name);
      }
    p = find_method_on_offset(d, offset);
    if (p != NULL) {
      assert(p->base == base);
      p->base = meth;
	  if (meth->has_precond) {
	    if (!(p->has_precond)) {
		  /* p and all his sons will no have at least one precond */
		  set_has_precond(d, offset, HASPRE(meth), HASPOST(meth));
	      }
	    }
      }
    else {
      if (d->first_son != NULL) {
        attach_derived_method (meth, offset, base, d->first_son);
        }
      }
    d = d->brother;
    }
}


void attach_redefined_method YPARAMS2(METHOD_INFO*, meth)
{
  METHOD_INFO *p, *q;
  minimal_dual *dual_ptr, *d;
  unsigned offset;
	  
/*   printf("TRACE: attach_redefined_method \n"); */

  /* first attach to method that meth redefine (in base classes) */
  if (meth != NULL) {
/*   printf("TRACE: attach_redefined_method (%s.%s)\n", meth->class->class_name, meth->name); */
    dual_ptr = meth->class;
    assert(dual_ptr != NULL);
	if (meth->post_func != NULL) {
	  SET_HASPOST(meth);
	  }
	if ((meth->pre_context_free != NULL) || (meth->pre_context_dep != NULL)) {
	  SET_HASPRE(meth);
	  }
/*	meth->has_precond = (meth->post_func != NULL) 
	                    || (meth->pre_context_free != NULL)
	                    || (meth->pre_context_dep != NULL); */
    p = NULL;
    if (meth->offset) {
      offset = meth->offset;
      d = dual_ptr->inherited;
      if (d != NULL) {
        while ((p == NULL) && (d != NULL)) {
          p = find_method_on_offset(d, offset);
          d = d->inherited;
          }
        if (p != NULL) {
          assert (p->offset == offset);
          meth->base = p;
		  /* handle the has_precond field */
		  if (p->has_precond) {
		    /*meth->has_precond = TRUE;*/
	        if (HASPRE(p)) {
	          SET_HASPRE(meth);
	          }
	        if (HASPOST(p)) {
	          SET_HASPOST(meth);
	          }
		    }
          }
        else {
          /* no base method */
          meth->base = NULL;
          }
        }
      else {
        /* no base class, then no base method */
        meth->base = NULL;
        }
      }
    else {
      offset = 0;
      meth->base = NULL;
      }

    /* then attach redefined versions of meth */
    if (offset) {
      d = dual_ptr->first_son;
      if (d != NULL) {
        attach_derived_method (meth, offset, p, d);
        }
      }
    }
}











