From 6c196ec8a41d6ed506c133c8b33dba9684f9a7a6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 12:34:43 +0000 Subject: Updated raytracer test. Added SPASS test. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- test/spass/table.c | 553 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 553 insertions(+) create mode 100644 test/spass/table.c (limited to 'test/spass/table.c') diff --git a/test/spass/table.c b/test/spass/table.c new file mode 100644 index 00000000..639dbfd6 --- /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; +} + -- cgit