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, 593 insertions, 0 deletions

diff --git a/test/spass/kbo.c b/test/spass/kbo.c
new file mode 100644
index 0000000..c598cbe
--- /dev/null
+++ b/test/spass/kbo.c
@@ -0,0 +1,593 @@
+/**************************************************************/
+/* ********************************************************** */
+/* *                                                        * */
+/* *         EXTENDED KNUTH BENDIX ORDERING                 * */
+/* *                                                        * */
+/* *  $Module:   KBO                                        * */ 
+/* *                                                        * */
+/* *  Copyright (C) 1996, 1997, 1998, 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                                    * */
+/* *                                                        * */
+/* ********************************************************** */
+/**************************************************************/
+
+
+/* $RCSfile$ */
+
+#include "kbo.h"
+#include "order.h"
+
+const int kbo_MINWEIGHT = 1;
+
+/**************************************************************/
+/*  Functions to implement an order on terms                  */
+/**************************************************************/
+
+static int kbo_ContCompVarCondAndWeightIntern(CONTEXT Context, TERM Term, int Index)
+/**************************************************************
+  INPUT:   
+  EFFECT:  
+***************************************************************/
+{
+  int Weight;
+
+  Weight = 0;
+  Term   = cont_Deref(&Context,Term);
+
+  if (term_IsStandardVariable(Term)) {
+    ord_VARCOUNT[term_TopSymbol(Term)][Index]++;
+    Weight += kbo_MINWEIGHT;
+  }
+  else {
+    LIST Scan;
+    Weight += symbol_Weight(term_TopSymbol(Term));
+    for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan))
+      Weight += kbo_ContCompVarCondAndWeightIntern(Context, list_Car(Scan), Index);
+  }
+
+  return Weight;
+}
+
+static int kbo_ContCompVarCondAndWeight(CONTEXT Context1, TERM Term1, BOOL *VarCond1, 
+					CONTEXT Context2, TERM Term2, BOOL *VarCond2)
+/**************************************************************
+  INPUT:   Two contexts, two terms and two pointers to booleans.
+  EFFECT:  Sets the booleans with respect to the kbo variable condition.
+           Computes the kbo weight difference.
+	   The terms are interpreted with respect to the bindings in the respective
+	   contexts.
+***************************************************************/
+{
+  SYMBOL MaxVar1,MaxVar2;
+  int    i,Weight;
+
+  *VarCond1 = *VarCond2 = TRUE;
+  MaxVar1   = cont_TermMaxVar(Context1,Term1);
+  MaxVar2   = cont_TermMaxVar(Context2,Term2);
+
+  if (MaxVar1 < MaxVar2)
+    MaxVar1 = MaxVar2;
+
+  for (i = 0; i <= MaxVar1; i++) {
+    ord_VARCOUNT[i][0] = 0;
+    ord_VARCOUNT[i][1] = 0;
+  }
+
+  Weight = kbo_ContCompVarCondAndWeightIntern(Context1, Term1, 0);
+  Weight = Weight - kbo_ContCompVarCondAndWeightIntern(Context2, Term2, 1);
+
+  for (i = 0; i <= MaxVar1; i++) {
+    if (ord_VARCOUNT[i][0] < ord_VARCOUNT[i][1]) {
+      *VarCond1 = FALSE;
+      if (!*VarCond2)
+	return Weight;
+    }
+    else if (ord_VARCOUNT[i][0] > ord_VARCOUNT[i][1]) {
+      *VarCond2 = FALSE;
+      if (!*VarCond1)
+	return Weight;
+    }
+  }
+  return Weight;  
+}
+
+
+static int kbo_CompVarCondAndWeight(TERM Term1, BOOL *VarCond1, TERM Term2, BOOL *VarCond2)
+/**************************************************************
+  INPUT:   Two terms and two pointers to booleans.
+  EFFECT:  Sets the booleans with respect to the kbo variable condition.
+           Computes the kbo weight difference.
+***************************************************************/
+{
+  SYMBOL MaxVar1,MaxVar2;
+  TERM   Term;
+  LIST   Scan;
+  int    i,Stack,Weight;
+
+  *VarCond1 = *VarCond2 = TRUE;
+  MaxVar1   = term_MaxVar(Term1);
+  MaxVar2   = term_MaxVar(Term2);
+  Stack     = stack_Bottom();
+  Weight    = 0;
+
+  if (MaxVar1 < MaxVar2)
+    MaxVar1 = MaxVar2;
+
+  for (i = 0; i <= MaxVar1; i++) {
+    ord_VARCOUNT[i][0] = 0;
+    ord_VARCOUNT[i][1] = 0;
+  }
+
+  Term = Term1;
+  if (term_IsStandardVariable(Term)) {
+    ord_VARCOUNT[term_TopSymbol(Term)][0]++;
+    Weight += kbo_MINWEIGHT;
+  }
+  else {
+    Weight += symbol_Weight(term_TopSymbol(Term));
+    if (term_IsComplex(Term))
+      stack_Push(term_ArgumentList(Term));
+  }
+  while (!stack_Empty(Stack)) {
+    Scan = stack_Top();
+    Term = (TERM)list_Car(Scan);
+    stack_RplacTop(list_Cdr(Scan));
+    if (term_IsStandardVariable(Term)) {
+      Weight += kbo_MINWEIGHT;
+      ord_VARCOUNT[term_TopSymbol(Term)][0]++;
+    }
+    else {
+      Weight += symbol_Weight(term_TopSymbol(Term));
+      if (term_IsComplex(Term))
+	stack_Push(term_ArgumentList(Term));
+    }
+    while (!stack_Empty(Stack) && list_Empty(stack_Top()))
+      stack_Pop();
+  }
+
+  Term = Term2;
+  if (term_IsStandardVariable(Term)) {
+    Weight -= kbo_MINWEIGHT;
+    ord_VARCOUNT[term_TopSymbol(Term)][1]++;
+  }
+  else {
+    Weight -= symbol_Weight(term_TopSymbol(Term));
+    if (term_IsComplex(Term))
+      stack_Push(term_ArgumentList(Term));
+  }
+  while (!stack_Empty(Stack)) {
+    Scan = stack_Top();
+    Term = (TERM)list_Car(Scan);
+    stack_RplacTop(list_Cdr(Scan));
+    if (term_IsStandardVariable(Term)) {
+      Weight -= kbo_MINWEIGHT;
+      ord_VARCOUNT[term_TopSymbol(Term)][1]++;
+    }
+    else {
+      Weight -= symbol_Weight(term_TopSymbol(Term));
+      if (term_IsComplex(Term))
+	stack_Push(term_ArgumentList(Term));
+    }
+    while (!stack_Empty(Stack) && list_Empty(stack_Top()))
+      stack_Pop();
+  }
+
+  for (i = 0; i <= MaxVar1; i++) {
+    if (ord_VARCOUNT[i][0] < ord_VARCOUNT[i][1]) {
+      *VarCond1 = FALSE;
+      if (!*VarCond2)
+	return Weight;
+    }
+   if (ord_VARCOUNT[i][0] > ord_VARCOUNT[i][1]) {
+      *VarCond2 = FALSE;
+      if (!*VarCond1)
+	return Weight;
+    }
+  }
+  return Weight;  
+}
+
+
+static ord_RESULT kbo_CompareStruc(TERM Term1, TERM Term2, int WeightDiff)
+/**************************************************************
+  INPUT:   Two terms where the kbo-variable condition for <Term1> and
+           <Term2> is satisfied and <WeightDiff> is the kbo weight difference
+	   between <Term1> and <Term2> 
+  RETURNS: ord_UNCOMPARABLE, if Term1 and Term2 are uncomparable
+	   ord_EQUAL,        if Term1 and Term2 are equal
+	   ord_GREATER_THAN, if Term1 is greater than Term2
+  CAUTION: The precedence from the order module is used to determine
+           the precedence of symbols!
+***************************************************************/
+{
+  LIST   Scan1,Scan2;
+  SYMBOL Top1,Top2;
+
+  Top1       = term_TopSymbol(Term1);
+  Top2       = term_TopSymbol(Term2);
+
+  if (WeightDiff > 0)
+    return ord_GREATER_THAN;
+  else 
+    if (WeightDiff == 0) {
+      if (symbol_IsStandardVariable(Top1)) {
+	if (symbol_IsStandardVariable(Top2))
+	  return ord_EQUAL;
+	else
+	  return ord_UNCOMPARABLE;
+      }
+      else
+	if (symbol_IsStandardVariable(Top2) ||
+	    symbol_PrecedenceGreater(ord_PRECEDENCE, Top1, Top2))
+	  return ord_GREATER_THAN;
+	else
+	  if (Top1 == Top2) {
+	    int    RecWeightDiff;
+	    BOOL   T1VarCond, T2VarCond;
+	    TERM   RecTerm1,RecTerm2;
+	    Scan1 = term_ArgumentList(Term1);
+	    Scan2 = term_ArgumentList(Term2);
+	    if (symbol_HasProperty(Top1,ORDRIGHT)) {
+	      int i;
+	      for (i = symbol_Arity(Top1);
+		   i > 0 && term_Equal(list_NthElement(Scan1,i),list_NthElement(Scan2,i));
+		   i--);
+	      if (i > 0) {
+		RecTerm1 = (TERM)list_NthElement(Scan1,i);
+		RecTerm2 = (TERM)list_NthElement(Scan2,i);
+	      }
+	      else
+		return ord_EQUAL;
+	    }
+	    else {	      
+	      while (!list_Empty(Scan1) && term_Equal(list_Car(Scan1),list_Car(Scan2))) {
+		Scan1 = list_Cdr(Scan1);
+		Scan2 = list_Cdr(Scan2);
+	      }
+	      if (list_Empty(Scan1)) /* Implies that list_Empty(Scan2)  */
+		return ord_EQUAL;
+	      else {
+		RecTerm1 = (TERM)list_Car(Scan1);
+		RecTerm2 = (TERM)list_Car(Scan2);
+	      }
+	    }	      
+	    RecWeightDiff =  kbo_CompVarCondAndWeight(RecTerm1,&T1VarCond,RecTerm2,&T2VarCond);
+	    if (RecWeightDiff >= 0 && T1VarCond)
+	      return kbo_CompareStruc(RecTerm1, RecTerm2, RecWeightDiff);
+	    else
+	      return ord_UNCOMPARABLE;
+	  }
+	  else
+	    return ord_UNCOMPARABLE;
+    }
+    else
+      return ord_UNCOMPARABLE;
+
+  return ord_UNCOMPARABLE;
+}
+  
+
+ord_RESULT kbo_Compare(TERM Term1, TERM Term2)
+/**************************************************************
+  INPUT:   Two terms.
+  RETURNS: ord_UNCOMPARABLE, if Term1 and Term2 are uncomparable because of
+                              different variables,
+	   ord_EQUAL,        if Term1 and Term2 are comparable and have the
+	                      same weight,
+	   ord_GREATER_THAN, if Term1 is greater than Term2 wrt the kbo with
+	                      the actual precedence and the given symbol weights,
+	   ord_SMALLER_THAN, else.
+  CAUTION: The precedence from the order module is used to determine
+           the precedence of symbols!
+***************************************************************/
+{
+  int        WeightDiff;
+  BOOL       T1VarCond, T2VarCond;
+  ord_RESULT Result;
+
+#ifdef CHECK
+  if (!term_IsTerm(Term1) || !term_IsTerm(Term2)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In kbo_Compare:");
+    misc_ErrorReport("\n Illegal input.");
+    misc_FinishErrorReport();
+  }
+#endif
+
+
+  WeightDiff =  kbo_CompVarCondAndWeight(Term1,&T1VarCond,Term2,&T2VarCond);
+
+  if (T1VarCond && !T2VarCond)
+    return kbo_CompareStruc(Term1,Term2,WeightDiff);
+
+  if (!T1VarCond && T2VarCond)
+    return ord_Not(kbo_CompareStruc(Term2,Term1,-WeightDiff));
+
+  if (T1VarCond && T2VarCond) {
+    Result = kbo_CompareStruc(Term1,Term2,WeightDiff);
+    if (Result == ord_UNCOMPARABLE)
+      return ord_Not(kbo_CompareStruc(Term2,Term1,-WeightDiff));
+    else
+      return Result;
+  }
+
+  return ord_UNCOMPARABLE;
+}
+
+static ord_RESULT kbo_ContCompareStruc(CONTEXT Context1, TERM Term1,
+				       CONTEXT Context2, TERM Term2,
+				       int WeightDiff)
+/**************************************************************
+  INPUT:   Two contexts and two terms where the kbo-variable condition
+           for <Term1> and <Term2> is satisfied and <WeightDiff> is the
+	   kbo weight difference between <Term1> and <Term2>.
+  RETURNS: ord_UNCOMPARABLE, if Term1 and Term2 are uncomparable
+	   ord_EQUAL,        if Term1 and Term2 are equal
+	   ord_GREATER_THAN, if Term1 is greater than Term2 
+	   The Terms are interpreted with respect to the contexts.
+  CAUTION: The precedence from the order module is used to determine
+           the precedence of symbols!
+***************************************************************/
+{
+  LIST   Scan1,Scan2;
+  SYMBOL Top1,Top2;
+
+  Term1      = cont_Deref(&Context1,Term1);
+  Term2      = cont_Deref(&Context2,Term2);
+  Top1       = term_TopSymbol(Term1);
+  Top2       = term_TopSymbol(Term2);
+
+  if (WeightDiff > 0)
+    return ord_GREATER_THAN;
+  else 
+    if (WeightDiff == 0) {
+      if (symbol_IsStandardVariable(Top1)) {
+	if (symbol_IsStandardVariable(Top2))
+	  return ord_EQUAL;
+	else
+	  return ord_UNCOMPARABLE;
+      }
+      else
+	if (symbol_IsStandardVariable(Top2) ||
+	    symbol_PrecedenceGreater(ord_PRECEDENCE, Top1,Top2))
+	  return ord_GREATER_THAN;
+	else
+	  if (Top1 == Top2) {
+	    int    RecWeightDiff;
+	    BOOL   T1VarCond, T2VarCond;
+	    TERM   RecTerm1,RecTerm2;
+	    Scan1 = term_ArgumentList(Term1);
+	    Scan2 = term_ArgumentList(Term2);
+	    if (symbol_HasProperty(Top1,ORDRIGHT)) {
+	      int i;
+	      for (i = symbol_Arity(Top1);
+		   i > 0 && cont_TermEqual(Context1,list_NthElement(Scan1,i),
+					   Context2,list_NthElement(Scan2,i));
+		   i--);
+	      if (i > 0) {
+		RecTerm1 = cont_Deref(&Context1,list_NthElement(Scan1,i));
+		RecTerm2 = cont_Deref(&Context2,list_NthElement(Scan2,i));
+	      }
+	      else
+		return ord_EQUAL;
+	    }
+	    else {	      
+	      while (!list_Empty(Scan1) && cont_TermEqual(Context1,list_Car(Scan1),Context2,list_Car(Scan2))) {
+		Scan1 = list_Cdr(Scan1);
+		Scan2 = list_Cdr(Scan2);
+	      }
+	      if (list_Empty(Scan1)) /* Implies that list_Empty(Scan2)  */
+		return ord_EQUAL;
+	      else {
+		RecTerm1 = cont_Deref(&Context1,list_Car(Scan1));
+		RecTerm2 = cont_Deref(&Context2,list_Car(Scan2));
+	      }
+	    }	      
+	    RecWeightDiff =  kbo_ContCompVarCondAndWeight(Context1,RecTerm1,&T1VarCond,
+							  Context2,RecTerm2,&T2VarCond);
+	    if (RecWeightDiff >= 0 && T1VarCond)
+	      return kbo_ContCompareStruc(Context1, RecTerm1, Context2, RecTerm2, RecWeightDiff);
+	    else
+	      return ord_UNCOMPARABLE;
+	  }
+	  else
+	    return ord_UNCOMPARABLE;
+    }
+    else
+      return ord_UNCOMPARABLE;
+
+  return ord_UNCOMPARABLE;
+}
+  
+
+ord_RESULT kbo_ContCompare(CONTEXT Context1, TERM Term1, CONTEXT Context2, TERM Term2)
+/**************************************************************
+  INPUT:   Two contexts and two terms.
+  RETURNS: ord_UNCOMPARABLE, if Term1 and Term2 are uncomparable because of
+                              different variables,
+	   ord_EQUAL,        if Term1 and Term2 are comparable and have the
+	                      same weight,
+	   ord_GREATER_THAN, if Term1 is greater than Term2 wrt the kbo with
+	                      the actual precedence kbo_Prec and the given 
+			      symbol_Weights,
+	   ord_SMALLER_THAN, else.
+	   The Terms are interpreted with respect to the contexts.
+  CAUTION: The precedence from the order module is used to determine
+           the precedence of symbols!
+***************************************************************/
+{
+  int        WeightDiff;
+  BOOL       T1VarCond, T2VarCond;
+  ord_RESULT Result;
+
+#ifdef CHECK
+  if (!term_IsTerm(Term1) || !term_IsTerm(Term2)) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In kbo_Compare:");
+    misc_ErrorReport("\n Illegal input.");
+    misc_FinishErrorReport();
+  }
+#endif
+
+
+  WeightDiff =  kbo_ContCompVarCondAndWeight(Context1, Term1, &T1VarCond, Context2, Term2, &T2VarCond);
+
+  if (T1VarCond && !T2VarCond)
+    return kbo_ContCompareStruc(Context1,Term1,Context2,Term2,WeightDiff);
+
+  if (!T1VarCond && T2VarCond)
+    return ord_Not(kbo_ContCompareStruc(Context2,Term2,Context1,Term1,-WeightDiff));
+
+  if (T1VarCond && T2VarCond) {
+    Result = kbo_ContCompareStruc(Context1,Term1,Context2,Term2,WeightDiff);
+    if (Result == ord_UNCOMPARABLE)
+      return ord_Not(kbo_ContCompareStruc(Context2,Term2,Context1,Term1,-WeightDiff));
+    else
+      return Result;
+  }
+
+  return ord_UNCOMPARABLE;
+}
+
+static BOOL kbo_ContGreaterCompareStruc(CONTEXT Context1, TERM Term1,
+					CONTEXT Context2, TERM Term2)
+/**************************************************************
+  INPUT:   Two contexts and two terms where the kbo-variable condition
+           for <Term1> and <Term2> is satisfied as well as the
+	   weight difference between the terms is zero.
+  RETURNS: TRUE if Term1 is greater than Term2.
+	   The Terms are interpreted with respect to the contexts.
+  CAUTION: The precedence from the order module is used to determine
+           the precedence of symbols!
+***************************************************************/
+{
+  LIST   Scan1,Scan2;
+  SYMBOL Top1,Top2;
+
+  Term1      = cont_Deref(&Context1,Term1);
+  Term2      = cont_Deref(&Context2,Term2);
+  Top1       = term_TopSymbol(Term1);
+  Top2       = term_TopSymbol(Term2);
+
+  if (symbol_IsStandardVariable(Top1)) {
+    if (symbol_IsStandardVariable(Top2))
+      return FALSE;
+    else
+      return FALSE;
+  }
+  else
+    if (symbol_IsStandardVariable(Top2) ||
+	symbol_PrecedenceGreater(ord_PRECEDENCE, Top1, Top2))
+      return TRUE;
+    else
+      if (Top1 == Top2) {
+	int    RecWeightDiff;
+	BOOL   T1VarCond, T2VarCond;
+	TERM   RecTerm1,RecTerm2;
+	Scan1 = term_ArgumentList(Term1);
+	Scan2 = term_ArgumentList(Term2);
+	if (symbol_HasProperty(Top1,ORDRIGHT)) {
+	  int i;
+	  for (i = symbol_Arity(Top1);
+	       i > 0 && cont_TermEqual(Context1,list_NthElement(Scan1,i),
+				       Context2,list_NthElement(Scan2,i));
+	       i--);
+	  if (i > 0) {
+	    RecTerm1 = cont_Deref(&Context1,list_NthElement(Scan1,i));
+	    RecTerm2 = cont_Deref(&Context2,list_NthElement(Scan2,i));
+	  }
+	  else
+	    return FALSE;
+	}
+	else {	      
+	  while (!list_Empty(Scan1) && cont_TermEqual(Context1,list_Car(Scan1),Context2,list_Car(Scan2))) {
+	    Scan1 = list_Cdr(Scan1);
+	    Scan2 = list_Cdr(Scan2);
+	  }
+	  if (list_Empty(Scan1)) /* Implies that list_Empty(Scan2)  */
+	    return FALSE;
+	  else {
+	    RecTerm1 = cont_Deref(&Context1,list_Car(Scan1));
+	    RecTerm2 = cont_Deref(&Context2,list_Car(Scan2));
+	  }
+	}	      
+	RecWeightDiff =  kbo_ContCompVarCondAndWeight(Context1,RecTerm1,&T1VarCond,
+						      Context2,RecTerm2,&T2VarCond);
+
+	if (T1VarCond) {
+	  if (RecWeightDiff > 0)
+	    return TRUE;
+	  else
+	    if (RecWeightDiff == 0)
+	      return kbo_ContGreaterCompareStruc(Context1, RecTerm1, Context2, RecTerm2);
+	}
+      }
+  
+  return FALSE;
+}
+
+
+BOOL kbo_ContGreater(CONTEXT Context1, TERM Term1, CONTEXT Context2, TERM Term2)
+/**************************************************************
+  INPUT:   Two contexts and two terms.
+  RETURNS: TRUE, if Term1 is greater than Term2 wrt the kbo with
+           the actual precedence kbo_Prec and the given symbol_Weights
+  CAUTION: The precedence from the order module is used to determine
+           the precedence of symbols!
+***************************************************************/
+{
+  int        WeightDiff;
+  BOOL       T1VarCond, T2VarCond;
+
+#ifdef CHECK
+  if ((!term_IsTerm(Term1)) || (!term_IsTerm(Term2)) ) {
+    misc_StartErrorReport();
+    misc_ErrorReport("\n In kbo_ContGreater:");
+    misc_ErrorReport("\n Illegal input.");
+    misc_FinishErrorReport();
+  }
+#endif
+
+
+  WeightDiff =  kbo_ContCompVarCondAndWeight(Context1, Term1, &T1VarCond, Context2, Term2, &T2VarCond);
+
+  if (T1VarCond) {
+    if (WeightDiff > 0)
+      return TRUE;
+    else
+      if (WeightDiff == 0) 
+	return kbo_ContGreaterCompareStruc(Context1,Term1,Context2,Term2);
+  }
+  return FALSE;
+}