[m-rev.] for review: fix termination analysis bug

[Julien Fischer]

Estimated hours taken: 10
Branches: main

Fix a bug that caused the termination analyser to abort when using
the `num-data-elems' norm whilst analysing code that (de)constructs
existentially typed data types.

compiler/term_util.m:
	When building the weight table add any type_infos to the list
	of non-recursive arguments otherwise term_util.functor_norm/9 will
	throw an exception when processing an existentially typed data item.
	When calculating the weight do not add arguments that correspond
	to type_info related variables.

tests/term/existential_error1.m:
tests/term/existential_error2.m:
tests/term/existential_error1.trans_opt_exp:
tests/term/existential_error2.trans_opt_exp:
	Tests cases for above.

tests/term/Mmakefile:
tests/term/Mercury.options:
	Add new test cases.  Specify which norm to use on a case-by-case
	basis.


Index: compiler/term_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_util.m,v
retrieving revision 1.26
diff -u -r1.26 term_util.m
--- compiler/term_util.m	25 Jul 2003 02:27:24 -0000	1.26
+++ compiler/term_util.m	2 Oct 2003 13:39:09 -0000
@@ -297,19 +297,20 @@
 	weight_table::in, weight_table::out) is det.

 find_weights_for_cons(Ctor, TypeCtor, Params, Weights0, Weights) :-
-	% XXX should we do something about ExistQVars here?
- 	Ctor = ctor(_ExistQVars, _Constraints, SymName, Args),
+ 	Ctor = ctor(ExistQVars, _Constraints, SymName, Args),
+	list__length(ExistQVars, NumExistQVars),
 	list__length(Args, Arity),
 	( Arity > 0 ->
 		find_and_count_nonrec_args(Args, TypeCtor, Params,
 			NumNonRec, ArgInfos0),
 		( NumNonRec = 0 ->
 			Weight = 1,
-			list__duplicate(Arity, yes, ArgInfos)
+			list__duplicate(Arity, yes, ArgInfos1)
 		;
 			Weight = NumNonRec,
-			ArgInfos = ArgInfos0
+			ArgInfos1 = ArgInfos0
 		),
+		ArgInfos = list__duplicate(NumExistQVars, no) ++ ArgInfos1,
 		WeightInfo = weight(Weight, ArgInfos)
 	;
 		WeightInfo = weight(0, [])
Index: tests/term/Mercury.options
===================================================================
RCS file: /home/mercury1/repository/tests/term/Mercury.options,v
retrieving revision 1.1
diff -u -r1.1 Mercury.options
--- tests/term/Mercury.options	17 Aug 2002 13:52:29 -0000	1.1
+++ tests/term/Mercury.options	2 Oct 2003 11:39:24 -0000
@@ -0,0 +1,58 @@
+MCFLAGS-ack=--term-norm=simple
+MCFLAGS-append=--term-norm=simple
+MCFLAGS-arit_exp=--term-norm=simple
+MCFLAGS-associative=--term-norm=simple
+MCFLAGS-dds1_2=--term-norm=simple
+MCFLAGS-dds3_13=--term-norm=simple
+MCFLAGS-dds3_14=--term-norm=simple
+MCFLAGS-dds3_15=--term-norm=simple
+MCFLAGS-dds3_17=--term-norm=simple
+MCFLAGS-dds3_8=--term-norm=simple
+MCFLAGS-existential_error1=--term-norm=num-data-elems
+MCFLAGS-existential_error2=--term-norm=num-data-elems
+MCFLAGS-fold=--term-norm=simple
+MCFLAGS-my_list=--term-norm=simple
+MCFLAGS-lte=--term-norm=simple
+MCFLAGS-my_map=--term-norm=simple
+MCFLAGS-member=--term-norm=simple
+MCFLAGS-mergesort=--term-norm=simple
+MCFLAGS-mergesort_ap=--term-norm=simple
+MCFLAGS-mergesort_t=--term-norm=simple
+MCFLAGS-mmatrix=--term-norm=simple
+MCFLAGS-money=--term-norm=simple
+MCFLAGS-naive_rev=--term-norm=simple
+MCFLAGS-occur=--term-norm=simple
+MCFLAGS-ordered=--term-norm=simple
+MCFLAGS-overlap=--term-norm=simple
+MCFLAGS-permutation=--term-norm=simple
+MCFLAGS-pl1_1=--term-norm=simple
+MCFLAGS-pl1_2=--term-norm=simple
+MCFLAGS-pl2_3_1=--term-norm=simple
+MCFLAGS-pl3_1_1=--term-norm=simple
+MCFLAGS-pl3_5_6=--term-norm=simple
+MCFLAGS-pl3_5_6a=--term-norm=simple
+MCFLAGS-pl4_01=--term-norm=simple
+MCFLAGS-pl4_4_3=--term-norm=simple
+MCFLAGS-pl4_4_6a=--term-norm=simple
+MCFLAGS-pl4_5_2=--term-norm=simple
+MCFLAGS-pl4_5_3a=--term-norm=simple
+MCFLAGS-pl5_2_2=--term-norm=simple
+MCFLAGS-pl6_1_1=--term-norm=simple
+MCFLAGS-pl7_2_9=--term-norm=simple
+MCFLAGS-pl7_6_2a=--term-norm=simple
+MCFLAGS-pl7_6_2b=--term-norm=simple
+MCFLAGS-pl7_6_2c=--term-norm=simple
+MCFLAGS-pl8_2_1=--term-norm=simple
+MCFLAGS-pl8_2_1a=--term-norm=simple
+MCFLAGS-pl8_3_1=--term-norm=simple
+MCFLAGS-pl8_3_1a=--term-norm=simple
+MCFLAGS-pl8_4_1=--term-norm=simple
+MCFLAGS-pl8_4_2=--term-norm=simple
+MCFLAGS-pragma_non_term=--term-norm=simple
+MCFLAGS-pragma_term=--term-norm=simple
+MCFLAGS-queens=--term-norm=simple
+MCFLAGS-quicksort=--term-norm=simple
+MCFLAGS-select=--term-norm=simple
+MCFLAGS-subset=--term-norm=simple
+MCFLAGS-sum=--term-norm=simple
+MCFLAGS-vangelder=--term-norm=simple
Index: tests/term/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/term/Mmakefile,v
retrieving revision 1.20
diff -u -r1.20 Mmakefile
--- tests/term/Mmakefile	25 Jun 2003 06:57:34 -0000	1.20
+++ tests/term/Mmakefile	2 Oct 2003 11:39:37 -0000
@@ -19,6 +19,8 @@
 	dds3_15 \
 	dds3_17 \
 	dds3_8 \
+	existential_error1 \
+	existential_error2 \
 	fold \
 	my_list \
 	lte \
@@ -87,7 +89,7 @@

 #-----------------------------------------------------------------------------#

-MCTERMFLAGS = --enable-termination --term-single-arg 5 --term-norm simple
+MCTERMFLAGS = --enable-termination --term-single-arg 5
 MCOPTFLAGS  = --no-inlining --no-optimize-unused-args --no-deforestation \
 	      --no-optimize-higher-order
 MCTRANSOPTFLAGS = $(MCTERMFLAGS) $(MCOPTFLAGS)
Index: tests/term/existential_error1.m
===================================================================
RCS file: tests/term/existential_error1.m
diff -N tests/term/existential_error1.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/term/existential_error1.m	2 Oct 2003 13:59:17 -0000
@@ -0,0 +1,22 @@
+% Regression test for term_util.m
+% Symptom: "Software Error: Unmatched lists in functor_norm_filter_args."
+% This was caused by the list of counted arguments in the weight table differing
+% from the list of arguments the termination analyser provided when it called
+% functor_norm/9.  The code that constructed the weight table was
+% ignoring type_infos when constructing the list of counted arguments.
+
+:- module existential_error1.
+
+:- interface.
+
+:- type univ ---> some [T] univ_cons(T).
+
+:- pred deconstruct_univ(univ::in, T::out) is semidet.
+
+:- implementation.
+
+deconstruct_univ(Univ, T) :-
+	Univ = univ_cons(T0),
+	private_builtin__typed_unify(T0, T).
+
+:- end_module existential_error1.
Index: tests/term/existential_error1.trans_opt_exp
===================================================================
RCS file: tests/term/existential_error1.trans_opt_exp
diff -N tests/term/existential_error1.trans_opt_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/term/existential_error1.trans_opt_exp	2 Oct 2003 07:06:25 -0000
@@ -0,0 +1,2 @@
+:- module existential_error1.
+:- pragma termination_info(existential_error1.deconstruct_univ((builtin.in), (builtin.out)), infinite, can_loop).
Index: tests/term/existential_error2.m
===================================================================
RCS file: tests/term/existential_error2.m
diff -N tests/term/existential_error2.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/term/existential_error2.m	2 Oct 2003 13:59:49 -0000
@@ -0,0 +1,20 @@
+% Regression test for term_util.m
+% Symptom: "Software Error: Unmatched lists in functor_norm_filter_args."
+% (see existential_error1.m for a description of the cause)
+
+:- module existential_error2.
+
+:- interface.
+
+:- type list_of_any
+	--->	nil_any
+	;	some [T] cons_arg(T, list_of_any).
+
+:- pred construct_list_of_any(list_of_any::out) is det.
+
+:- implementation.
+
+construct_list_of_any(X) :-
+	X = 'new cons_arg'(123, nil_any).
+
+:- end_module existential_error2.
Index: tests/term/existential_error2.trans_opt_exp
===================================================================
RCS file: tests/term/existential_error2.trans_opt_exp
diff -N tests/term/existential_error2.trans_opt_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/term/existential_error2.trans_opt_exp	2 Oct 2003 07:06:56 -0000
@@ -0,0 +1,2 @@
+:- module existential_error2.
+:- pragma termination_info(existential_error2.construct_list_of_any((builtin.out)), finite(1, [no]), cannot_loop).
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------