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

[Simon Taylor]

Estimated hours taken: 4
Branches: main

Fix a bug in mode analysis which caused spurious errors
for code containing unifications which always fail.

compiler/inst_util.m:
	Fix the code to abstractly unify bound inst lists.
	The old code was combining determinisms as if they
	were the determinisms of conjuncts when it should
	have been treating them as the determinisms of the
	arms of a switch.

compiler/det_analysis.m:
	Add det_switch_detism for use by inst_util.m.

tests/hard_coded/Mmakefile:
tests/hard_coded/failure_unify.{m,exp}:
	Test case.

Index: compiler/det_analysis.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/det_analysis.m,v
retrieving revision 1.156
diff -u -u -r1.156 det_analysis.m
--- compiler/det_analysis.m	26 Jul 2002 04:18:10 -0000	1.156
+++ compiler/det_analysis.m	29 Jul 2002 09:59:48 -0000
@@ -102,6 +102,9 @@
 :- pred det_par_conjunction_detism(determinism, determinism, determinism).
 :- mode det_par_conjunction_detism(in, in, out) is det.
 
+:- pred det_switch_detism(determinism, determinism, determinism).
+:- mode det_switch_detism(in, in, out) is det.
+
 :- pred det_disjunction_maxsoln(soln_count, soln_count, soln_count).
 :- mode det_disjunction_maxsoln(in, in, out) is det.
 
@@ -1038,6 +1041,13 @@
 	determinism_components(DetismB, CanFailB, MaxSolnB),
 	det_conjunction_canfail(CanFailA, CanFailB, CanFail),
 	det_conjunction_maxsoln(MaxSolnA, MaxSolnB, MaxSoln),
+	determinism_components(Detism, CanFail, MaxSoln).
+
+det_switch_detism(DetismA, DetismB, Detism) :-
+	determinism_components(DetismA, CanFailA, MaxSolnA),
+	determinism_components(DetismB, CanFailB, MaxSolnB),
+	det_switch_canfail(CanFailA, CanFailB, CanFail),
+	det_switch_maxsoln(MaxSolnA, MaxSolnB, MaxSoln),
 	determinism_components(Detism, CanFail, MaxSoln).
 
 % For the at_most_zero, at_most_one, at_most_many,
Index: compiler/inst_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/inst_util.m,v
retrieving revision 1.22
diff -u -u -r1.22 inst_util.m
--- compiler/inst_util.m	4 Jul 2002 23:25:48 -0000	1.22
+++ compiler/inst_util.m	29 Jul 2002 17:07:02 -0000
@@ -569,7 +569,6 @@
 %-----------------------------------------------------------------------------%
 
 	% This code performs abstract unification of two bound(...) insts.
-	% like a sorted merge operation.  If two elements have the
 	% The lists of bound_inst are guaranteed to be sorted.
 	% Abstract unification of two bound(...) insts proceeds
 	% like a sorted merge operation.  If two elements have the
@@ -578,6 +577,10 @@
 	% (If it can't, the whole thing fails).  If a functor name
 	% occurs in only one of the two input lists, it is not inserted
 	% in the output list.
+	%
+	% One way of looking at this code is that it simulates mode
+	% and determinism checking of the goal for the unification
+	% predicate for the type.
 
 :- pred abstractly_unify_bound_inst_list(is_live, list(bound_inst),
 		list(bound_inst), unify_is_real, module_info,
@@ -587,67 +590,70 @@
 
 abstractly_unify_bound_inst_list(Live, Xs, Ys, Real, ModuleInfo0, L, Det,
 		ModuleInfo) :-
-	abstractly_unify_bound_inst_list_2(Live, Xs, Ys, Real,
-		ModuleInfo0, 0, L, Det0, ModuleInfo),
-	( L = [] ->
-		det_par_conjunction_detism(Det0, erroneous, Det)
+	( ( Xs = [] ; Ys = [] ) ->
+		%
+		% This probably shouldn't happen. If we get here,
+		% it means that a previous goal had determinism
+		% `failure' or `erroneous', but we should have optimized
+		% away the rest of the conjunction after that goal.
+		%
+		L = [],
+		Det = erroneous,
+		ModuleInfo = ModuleInfo0
 	;
-		Det = Det0
+		abstractly_unify_bound_inst_list_2(Live, Xs, Ys, Real,
+			ModuleInfo0, L, Det0, ModuleInfo),
+
+		%
+		% If there are multiple alternatives for either of
+		% the inputs, or the constructor of the single
+		% alternative for each input doesn't match, then the
+		% unification can fail, so adjust the determinism.
+		%
+		( Xs = [functor(ConsId, _)], Ys = [functor(ConsId, _)] ->
+			Det = Det0
+		;
+			determinism_components(Det0, _, MaxSoln),
+			determinism_components(Det, can_fail, MaxSoln)
+		)
 	).
 
 :- pred abstractly_unify_bound_inst_list_2(is_live, list(bound_inst),
-		list(bound_inst), unify_is_real, module_info, int,
+		list(bound_inst), unify_is_real, module_info,
 		list(bound_inst), determinism, module_info).
-:- mode abstractly_unify_bound_inst_list_2(in, in, in, in, in, in,
+:- mode abstractly_unify_bound_inst_list_2(in, in, in, in, in,
 		out, out, out) is semidet.
 
-abstractly_unify_bound_inst_list_2(_, [], [], _, ModuleInfo, N, [], Det,
-		ModuleInfo) :-
-	(
-			% The only time an abstract unification should
-			% be det, is when both of the bound_inst lists
-			% are of length one and have the same cons_ids.
-			%
-			% If N=0, we need to make the determinism det
-			% so that determinism is inferred as erroneous
-			% rather then failure in 
-			% abstractly_unify_bound_inst_list
-		N =< 1
-	->
-		Det = det
-	;
-		Det = semidet
-	).
-abstractly_unify_bound_inst_list_2(_, [], [_|_], _, M, _, [], semidet, M).
-abstractly_unify_bound_inst_list_2(_, [_|_], [], _, M, _, [], semidet, M).
+abstractly_unify_bound_inst_list_2(_, [], [], _, M, [], erroneous, M).
+abstractly_unify_bound_inst_list_2(_, [], [_|_], _, M, [], failure, M).
+abstractly_unify_bound_inst_list_2(_, [_|_], [], _, M, [], failure, M).
 abstractly_unify_bound_inst_list_2(Live, [X|Xs], [Y|Ys], Real, ModuleInfo0,
-		N, L, Det, ModuleInfo) :-
+		L, Det, ModuleInfo) :-
 	X = functor(ConsIdX, ArgsX),
 	Y = functor(ConsIdY, ArgsY),
 	( ConsIdX = ConsIdY ->
 		abstractly_unify_inst_list(ArgsX, ArgsY, Live, Real,
 			ModuleInfo0, Args, Det1, ModuleInfo1),
 		abstractly_unify_bound_inst_list_2(Live, Xs, Ys, Real,
-					ModuleInfo1, N+1, L1, Det2, ModuleInfo),
+					ModuleInfo1, L1, Det2, ModuleInfo),
 
 		% If the unification of the two cons_ids is guaranteed
 		% not to succeed, don't include it in the list.
 		( determinism_components(Det1, _, at_most_zero) ->
-			L = L1,
-			Det = Det2
+			L = L1
 		;
-			L = [functor(ConsIdX, Args) | L1],
-			det_par_conjunction_detism(Det1, Det2, Det)
-		)
+			L = [functor(ConsIdX, Args) | L1]
+		),
+		det_switch_detism(Det1, Det2, Det)
 	;
 		( compare(<, ConsIdX, ConsIdY) ->
 			abstractly_unify_bound_inst_list_2(Live, Xs, [Y|Ys],
-				Real, ModuleInfo0, N+1, L, Det1, ModuleInfo)
+				Real, ModuleInfo0, L, Det1, ModuleInfo)
 		;
 			abstractly_unify_bound_inst_list_2(Live, [X|Xs], Ys,
-				Real, ModuleInfo0, N+1, L, Det1, ModuleInfo)
+				Real, ModuleInfo0, L, Det1, ModuleInfo)
 		),
-		det_par_conjunction_detism(Det1, semidet, Det)
+		det_switch_detism(Det1, failure, Det)
 	).
 
 :- pred abstractly_unify_bound_inst_list_lives(list(bound_inst), cons_id,
Index: tests/hard_coded/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/Mmakefile,v
retrieving revision 1.159
diff -u -u -r1.159 Mmakefile
--- tests/hard_coded/Mmakefile	22 Jul 2002 06:30:04 -0000	1.159
+++ tests/hard_coded/Mmakefile	29 Jul 2002 14:52:59 -0000
@@ -52,6 +52,7 @@
 	expand \
 	export_test \
 	factt \
+	failure_unify \
 	float_field \
 	float_map \
 	float_reg \
Index: tests/hard_coded/failure_unify.exp
===================================================================
RCS file: tests/hard_coded/failure_unify.exp
diff -N tests/hard_coded/failure_unify.exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/failure_unify.exp	29 Jul 2002 14:51:48 -0000
@@ -0,0 +1 @@
+test succeeded
Index: tests/hard_coded/failure_unify.m
===================================================================
RCS file: tests/hard_coded/failure_unify.m
diff -N tests/hard_coded/failure_unify.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/failure_unify.m	29 Jul 2002 14:51:21 -0000
@@ -0,0 +1,23 @@
+:- module failure_unify.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io__state::di, io__state::uo) is det.
+
+:- implementation.
+
+:- type f ---> f(int).
+
+main -->
+	(
+		{ X = f(1) },
+		{ Y = f(2) },
+		{ X = Y }
+	->
+		io__write_string("test failed\n")
+	;
+		io__write_string("test succeeded\n")
+	).
+
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------