Updated raytracer test. Added SPASS test.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 553 insertions, 0 deletions

diff --git a/test/spass/table.c b/test/spass/table.c
new file mode 100644
index 0000000..639dbfd
--- /dev/null
+++ b/test/spass/table.c
@@ -0,0 +1,553 @@
+/**************************************************************/
+/* ********************************************************** */
+/* *                                                        * */
+/* *             SIGNATURE TABLE                            * */
+/* *                                                        * */
+/* *  $Module:   TABLE                                      * */ 
+/* *                                                        * */
+/* *  Copyright (C) 1999, 2000, 2001 MPI fuer Informatik    * */
+/* *                                                        * */
+/* *  This program is free software; you can redistribute   * */
+/* *  it and/or modify it under the terms of the GNU        * */
+/* *  General Public License as published by the Free       * */
+/* *  Software Foundation; either version 2 of the License, * */
+/* *  or (at your option) any later version.                * */
+/* *                                                        * */
+/* *  This program is distributed in the hope that it will  * */
+/* *  be useful, but WITHOUT ANY WARRANTY; without even     * */
+/* *  the implied warranty of MERCHANTABILITY or FITNESS    * */
+/* *  FOR A PARTICULAR PURPOSE.  See the GNU General Public * */
+/* *  License for more details.                             * */
+/* *                                                        * */
+/* *  You should have received a copy of the GNU General    * */
+/* *  Public License along with this program; if not, write * */
+/* *  to the Free Software Foundation, Inc., 59 Temple      * */
+/* *  Place, Suite 330, Boston, MA  02111-1307  USA         * */
+/* *                                                        * */
+/* *                                                        * */
+/* $Revision: 21527 $                                         * */
+/* $State$                                            * */
+/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $                             * */
+/* $Author: duraid $                                       * */
+/* *                                                        * */
+/* *             Contact:                                   * */
+/* *             Christoph Weidenbach                       * */
+/* *             MPI fuer Informatik                        * */
+/* *             Stuhlsatzenhausweg 85                      * */
+/* *             66123 Saarbruecken                         * */
+/* *             Email: weidenb@mpi-sb.mpg.de               * */
+/* *             Germany                                    * */
+/* *                                                        * */
+/* ********************************************************** */
+/**************************************************************/
+
+
+/**************************************************************/
+/* Includes                                                   */
+/**************************************************************/
+
+#include "table.h"
+
+
+/**************************************************************/
+/* Inline functions                                           */
+/**************************************************************/
+
+static __inline__ int table_Index(SYMBOL symbol)
+{
+  if (symbol_IsVariable(symbol))
+    return -(int) symbol;
+  else
+    return symbol_Index(symbol);
+}
+
+
+static __inline__ TERM table_GetTerm(TERMARRAY ta)
+{
+  return ta->term;
+}
+
+
+static __inline__ TERMARRAY table_SetTerm(TERMARRAY ta, TERM term)
+{
+  ta->term = term;
+  return ta;
+}
+
+
+static __inline__ int table_GetStamp(TERMARRAY ta)
+{
+  return ta->stamp;
+}
+
+
+static __inline__ TERMARRAY table_SetStamp(TERMARRAY ta, int stamp)
+{
+  ta->stamp = stamp;
+  return ta;
+}
+
+
+static __inline__ TERMARRAY table_GetChild(TERMARRAY ta)
+{
+  return ta->child;
+}
+
+
+static __inline__ TERMARRAY table_SetChild(TERMARRAY ta, TERMARRAY child)
+{
+  ta->child = child;
+  return ta;
+}
+
+
+static __inline__ TERMARRAY table_GetTermarray(TABLE table)
+{
+  return table->ta;
+}
+
+
+static __inline__ TABLE table_SetTermarray(TABLE table, TERMARRAY ta)
+{
+  table->ta = ta;
+  return table;
+}
+
+
+static __inline__ TERMARRAY *table_GetPoss(TABLE table)
+{
+  return table->pos;
+}
+
+
+static __inline__ TERMARRAY table_GetPos(TABLE table, int index)
+{
+  return table_GetPoss(table)[index];
+}
+
+
+static __inline__ TABLE table_SetPoss(TABLE table, TERMARRAY *ref)
+{
+  table->pos = ref;
+  return table;
+}
+
+
+static __inline__ TABLE table_SetPos(TABLE table, int index, TERMARRAY ta)
+{
+  table_GetPoss(table)[index] = ta;
+  return table;
+}
+
+
+static __inline__ int *table_GetPosstamps(TABLE table)
+{
+  return table->posstamp;
+}
+
+
+static __inline__ int table_GetPosstamp(TABLE table, int index)
+{
+  return table_GetPosstamps(table)[index];
+}
+
+
+static __inline__ TABLE table_SetPosstamps(TABLE table, int *ref)
+{
+  table->posstamp = ref;
+  return table;
+}
+
+
+static __inline__ TABLE table_SetPosstamp(TABLE table, int index, int stamp)
+{
+  table_GetPosstamps(table)[index] = stamp;
+  return table;
+}
+
+
+static __inline__ int table_GetStampcounter(TABLE table)
+{
+  return table->stampcounter;
+}
+
+
+static __inline__ TABLE table_SetStampcounter(TABLE table, int stampcounter)
+{
+  table->stampcounter = stampcounter;
+  return table;
+}
+
+
+static __inline__ int table_GetOpbound(TABLE table)
+{
+  return table->opbound;
+}
+
+
+static __inline__ TABLE table_SetOpbound(TABLE table, int opbound)
+{
+  table->opbound = opbound;
+  return table;
+}
+
+
+static __inline__ int table_GetVarbound(TABLE table)
+{
+  return table->varbound;
+}
+
+
+static __inline__ TABLE table_SetVarbound(TABLE table, int varbound)
+{
+  table->varbound = varbound;
+  return table;
+}
+
+
+static __inline__ int table_GetTermbound(TABLE table)
+{
+  return table->termbound;
+}
+
+
+static __inline__ TABLE table_SetTermbound(TABLE table, int termbound)
+{
+  table->termbound = termbound;
+  return table;
+}
+
+
+static __inline__ BOOL table_LegalPosIndex(TABLE table, int index)
+{
+  return 0 <= index && index <= table_GetTermbound(table);
+}
+
+
+static __inline__ BOOL table_Stamped(TABLE table, TERMARRAY ta)
+{
+  return table_GetStamp(ta) == table_GetStampcounter(table);
+}
+
+
+static __inline__ TERMARRAY table_DelayedInit(TABLE table, TERMARRAY ta)
+/***************************************************************
+  INPUT:   a table and a termarray
+  RETURNS: the (now stamped) termarray
+  EFFECT:  partially initializes table by setting the
+	   termarray's entry to the empty term
+***************************************************************/
+{
+  if (!table_Stamped(table, ta)) {
+    table_SetTerm(ta, term_Null());
+    table_SetStamp(ta, table_GetStampcounter(table));
+  }
+  return ta;
+}
+
+
+static __inline__ BOOL table_PosStamped(TABLE table, int index)
+{
+  return table_GetPosstamp(table, index) == table_GetStampcounter(table);
+}
+
+
+static __inline__ int table_DelayedPosInit(TABLE table, int index)
+/***************************************************************
+  INPUT:   a table and a position index
+  RETURNS: the (now stamped) position index
+  EFFECT:  partially initializes table by setting the indexed
+	   position to the empty pointer, which means that the
+	   term with this index is not stored in table
+***************************************************************/
+{
+  if (!table_PosStamped(table, index)) {
+    table_SetPos(table, index, (TERMARRAY) NULL);
+    table_SetPosstamp(table, index, table_GetStampcounter(table));
+  }
+  return index;
+}
+
+
+/**************************************************************/
+/* Functions                                                  */
+/**************************************************************/
+
+TABLE table_Null(void)
+{
+  return (TABLE) NULL;
+}
+
+
+TABLE table_Create(int opbound, int varbound, int termbound)
+/***************************************************************
+  INPUT:   bounds for the operator symbol, variable and term
+	   indices of the terms to be stored in the signature
+	   table (i. e. for every such term its top symbol index
+	   has to be in [1, opbound] and the term numbers of its
+	   arguments in [0, termbound] - or its variable index
+	   in [1, varbound] if it is a variable)
+  RETURNS: a new (and empty) signature table 
+***************************************************************/
+{
+  TABLE result;
+
+#ifdef CHECK
+  if (opbound < 0) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In table_Create: negative opbound.");
+    misc_FinishErrorReport();
+  }
+  if (varbound < 0) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In table_Create: negative varbound.");
+    misc_FinishErrorReport();
+  }
+  if (termbound < 0) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In table_Create: negative termbound.");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  result = (TABLE) memory_Malloc(sizeof(struct table));
+  table_SetTermarray(result, (TERMARRAY) memory_Calloc (
+                                           opbound + varbound + 1,
+                                           sizeof(struct termarray)
+                                         ) + varbound);
+    /* move pointer to the middle of the array to allow negative indices */
+  table_SetPoss(
+    result,
+    (TERMARRAY*) memory_Malloc((termbound + 1) * sizeof(TERMARRAY))
+  );
+  table_SetPosstamps(result, (int*) memory_Calloc(termbound + 1, sizeof(int)));
+  table_SetOpbound(result, opbound);
+  table_SetVarbound(result, varbound);
+  table_SetTermbound(result, termbound);
+  table_SetStampcounter(result, 1);
+  return result;
+}
+
+
+static void table_FreeTermarray(TERMARRAY ta, int size)
+/***************************************************************
+  INPUT:  the termarray to free and its size
+  EFFECT: recursively frees the tree structure allocated for the
+	  signature array
+***************************************************************/
+{
+  int i;
+
+  if (ta) {
+    for (i = 0; i < size; i++)
+      table_FreeTermarray(table_GetChild(ta + i), size);
+    memory_Free(ta, size * sizeof(struct termarray));
+  }
+}
+
+
+void table_Free(TABLE table)
+{
+  int i;
+
+  if (table != table_Null()) {
+    for (i = -table_GetVarbound(table); i <= table_GetOpbound(table); i++)
+      table_FreeTermarray(
+        table_GetChild(table_GetTermarray(table) + i),
+        table_GetTermbound(table) + 1
+      );
+    memory_Free(
+      table_GetTermarray(table) - table_GetVarbound(table),
+      (table_GetOpbound(table) + table_GetVarbound(table) + 1) * sizeof(struct
+	termarray)
+    );
+    memory_Free(
+      table_GetPoss(table),
+      (table_GetTermbound(table) + 1) * sizeof(TERMARRAY)
+    );
+    memory_Free(
+      table_GetPosstamps(table),
+      (table_GetTermbound(table) + 1) * sizeof(int)
+    );
+    memory_Free(table, sizeof(struct table));
+  }
+}
+
+
+TABLE table_Init(TABLE table, int opbound, int varbound, int termbound)
+/***************************************************************
+  INPUT:   the table to recycle and bounds for the operator
+	   symbol, variable and term indices of the terms to be
+	   stored in the signature table (i. e. for every such
+	   term its top symbol index has to be in [1, opbound]
+	   and the term numbers of its arguments in
+	   [0, termbound] - or its variable index in
+	   [1, varbound] if it is a variable)
+  RETURNS: a cleaned up signature table 
+  CAUTION: potentially frees the old table, therefore must be
+	   called inside of an assignment like:
+	     table = table_Init(table, ...)
+***************************************************************/
+{
+  int opmax, varmax, termmax, i;
+  TERMARRAY old;
+
+#ifdef CHECK
+  if (opbound < 0) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In table_Init: negative opbound.");
+    misc_FinishErrorReport();
+  }
+  if (varbound < 0) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In table_Init: negative varbound.");
+    misc_FinishErrorReport();
+  }
+  if (termbound < 0) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In table_Init: negative termbound.");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  opmax   = table_GetOpbound(table) > opbound ? table_GetOpbound(table) :
+	      opbound;
+  varmax  = table_GetVarbound(table) > varbound ? table_GetVarbound(table) :
+	      varbound;
+  termmax = table_GetTermbound(table) > termbound ? table_GetTermbound(table) :
+	      termbound;
+  table_SetStampcounter(table, table_GetStampcounter(table) + 1);
+
+  /* in case of stamp overflow or too small termarray nodes get a new table: */
+  if (table_GetStampcounter(table)<=0 || termbound>table_GetTermbound(table)) {
+    table_Free(table);
+    return table_Create(opmax, varmax, termmax);
+  }
+
+  /* if only the top layer of the tree is too small get a larger top layer: */
+  else if (opbound+varbound > table_GetOpbound(table)+table_GetVarbound(table)){
+    old = table_GetTermarray(table);
+    table_SetTermarray(table, (TERMARRAY) memory_Calloc(
+					    opmax + varmax + 1,
+					    sizeof(struct termarray)
+					  ) + varmax);
+    for (i = -table_GetVarbound(table); i <= table_GetOpbound(table); i++)
+      table_SetChild(table_GetTermarray(table) + i, table_GetChild(old + i));
+    memory_Free(
+      old - table_GetVarbound(table),
+      (table_GetOpbound(table) + table_GetVarbound(table) + 1) * sizeof(struct
+	termarray)
+    );
+    table_SetOpbound(table, opmax);
+    table_SetVarbound(table, varmax);
+    return table;
+  }
+
+  else {
+
+    /* move pointer to termarray's new middle: */
+    table_SetTermarray(
+      table,
+      table_GetTermarray(table) + table_GetOpbound(table) - opbound
+    );
+
+    table_SetVarbound(
+      table,
+      table_GetOpbound(table) + table_GetVarbound(table) - opbound
+    );
+    table_SetOpbound(table, opbound);
+    return table;
+  }
+}
+
+
+TERM table_QueryAndEnter(TABLE table, PARTITION p, TERM term)
+/***************************************************************
+  RETURNS: a term with the same p-signature (sigtab_Index(top
+	   symbol), [arg 1] , ..., [arg n] ) as term - or the
+                           p              p
+	   empty term if no such term exists
+  EFFECT:  term enters table in the latter case
+***************************************************************/
+{
+  TERMARRAY ta;
+  LIST terms;
+
+#ifdef CHECK
+  if (part_Size(p) - 1 > table_GetTermbound(table)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In table_QueryAndEnter: partition not suitable.");
+    misc_FinishErrorReport();
+  }
+  if (table_Index(term_TopSymbol(term)) > table_GetOpbound(table)) {
+    misc_StartErrorReport();
+    misc_ErrorReport
+      ("\n In table_QueryAndEnter: term's operation symbol out of bounds.");
+    misc_FinishErrorReport();
+  }
+  if (table_Index(term_TopSymbol(term)) < -table_GetVarbound(table)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In table_QueryAndEnter: variable out of bounds.");
+    misc_FinishErrorReport();
+  }
+  if (!table_LegalPosIndex(table, term_Size(term))) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In table_QueryAndEnter: term out of bounds.");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  ta = table_GetTermarray(table) + table_Index(term_TopSymbol(term));
+  for (terms = term_ArgumentList(term); !list_Empty(terms); terms =
+      list_Cdr(terms)) {
+    if (!table_GetChild(ta))
+      table_SetChild(ta, (TERMARRAY) memory_Calloc (
+                                       table_GetTermbound(table) + 1,
+                                       sizeof(struct termarray)
+                                     ));
+    ta = table_GetChild(ta) + part_Find(p, term_Size(list_Car(terms)));
+  }
+  table_DelayedInit(table, ta);
+  if (table_GetTerm(ta))
+    return table_GetTerm(ta);
+  else {
+    table_SetTerm(ta, term);
+    table_SetPos(table, table_DelayedPosInit(table, term_Size(term)), ta);
+    return term_Null();
+  }
+}
+
+
+TABLE table_Delete(TABLE table, TERM term)
+/***************************************************************
+  EFFECT: if term has entered table before, it is deleted
+***************************************************************/
+{
+  int no;
+
+#ifdef CHECK
+  if (!table_LegalPosIndex(table, term_Size(term))) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In table_Delete: illegal table access.");
+    misc_FinishErrorReport();
+  }
+#endif
+
+  no = term_Size(term);
+  table_DelayedPosInit(table, no);
+  if (table_GetPos(table, no)) {
+
+#ifdef CHECK
+    if (!table_Stamped(table, table_GetPos(table, no))) {
+      misc_StartErrorReport();
+      misc_ErrorReport("\n In table_Delete: table corrupted.");
+      misc_FinishErrorReport();
+    }
+#endif
+
+    table_SetTerm(table_GetPos(table, no), term_Null());
+    table_SetPos(table, no, (TERMARRAY) NULL);
+  }
+  return table;
+}
+