for review: fix bug in unique mode checking

[Fergus Henderson]

Hi,

Could someone please review this one?

--------------------

Estimated hours taken: 4

compiler/unique_modes.m:
	Fix a bug reported by Serge Varennes
	<serge.varennes at detexis.thomson-csf.com>:
	we need to mark variables as `mostly_unique' rather
	than `unique' at all disjunctions, not just at model_non
	disjunctions, because model_semi and even model_det
	disjunctions can still have backtracking from one failing
	disjunct into the next disjunct.

	Also add a couple of comments.

tests/invalid/Mmakefile:
tests/invalid/uniq_modes.m:
tests/invalid/uniq_modes.err_exp:
	Add a regression test for this change.

tests/hard_coded/purity.m:
tests/hard_coded/cc_nondet_disj.m:
	Fix code that the compiler now rejects, due to the above change.
	The compiler is being a bit conservative to reject these cases,
	because the code won't actually violate unique-mode-correctness,
	but the conservatism here with disjunctions is similar to unique
	mode analysis's already existing conservatism with regard to
	if-then-elses, and the work-around for cases like this is easy,
	so I don't consider that to be a significant problem.

	The conservatism in question is that if it sees
	`{ test }, io__write_string("blah")' in a model_det/model_semi
	disjunct or in the condition of an if-then-else, it will report
	a unique mode error, since it doesn't realize that destructive
	update only occurs _after_ we have committed to this branch.

tests/hard_coded/Mmakefile:
	Disable the test case bidirectional.m, since the compiler now
	rejects it, due to the above change to unique_modes.m. 
	The compiler is again being overly conservative in its analysis.
	The problem is similar to that in the two test cases above, 
	unfortunately there is no easy work-around in this case. 
	The compiler really ought to support this style of bidirectional
	code using unique modes, so I do consider this to be a significant
	problem, but the fix is a fair bit of work, so I will deal with
	that as a separate change.

Index: compiler/unique_modes.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/unique_modes.m,v
retrieving revision 1.50
diff -u -r1.50 unique_modes.m
--- unique_modes.m	1998/11/20 04:09:38	1.50
+++ unique_modes.m	1999/04/08 16:42:07
@@ -10,6 +10,10 @@
 % This module checks that variables with a unique mode (as opposed to
 % a mostly-unique mode) really are unique, and not nondet live - i.e.,
 % that they cannot be referenced on backtracking.
+% (Actually the term "nondet live" is a bit of a misnomer, because
+% really we are just interested in whether something can be referenced
+% on backtracking, and this can occur after backtracking in semidet
+% code too, not just in nondet code.)
 
 % Basically we just traverse each goal, keeping track of which variables
 % are nondet live.  At each procedure call, we check that any arguments
@@ -19,7 +23,9 @@
 
 % Variables can become nondet live in several places:
 % in negations, in the conditions of if-then-elses,
-% and in disjunctions, and at nondet calls.
+% in disjunctions, and at nondet calls.
+% These are the only places at which we can resume execution
+% after backtracking.
 
 % XXX we currently make the conservative assumption that
 % any non-local variable in a disjunction or nondet call
@@ -245,10 +251,10 @@
 
 unique_modes__check_goal_2(conj(List0), _GoalInfo0, conj(List)) -->
 	mode_checkpoint(enter, "conj"),
-	mode_info_add_goals_live_vars(List0),
 	( { List0 = [] } ->	% for efficiency, optimize common case
 		{ List = [] }
 	;
+		mode_info_add_goals_live_vars(List0),
 		unique_modes__check_conj(List0, List)
 	),
 	mode_checkpoint(exit, "conj").
@@ -270,21 +276,15 @@
 		{ instmap__init_unreachable(InstMap) },
 		mode_info_set_instmap(InstMap)
 	;
+		%
+		% Mark all the variables which are nondet-live at the
+		% start of the disjunction and whose inst is `unique'
+		% as instead being only `mostly_unique'.
+		%
 		{ goal_info_get_nonlocals(GoalInfo0, NonLocals) },
-		{ goal_info_get_code_model(GoalInfo0, CodeModel) },
-		% does this disjunction create a choice point?
-		( { CodeModel = model_non } ->
-			%
-			% Mark all the variables which are nondet-live at the
-			% start of the disjunction and whose inst is `unique'
-			% as instead being only `mostly_unique'.
-			%
-			mode_info_add_live_vars(NonLocals),
-			make_all_nondet_live_vars_mostly_uniq,
-			mode_info_remove_live_vars(NonLocals)
-		;
-			[]
-		),
+		mode_info_add_live_vars(NonLocals),
+		make_all_nondet_live_vars_mostly_uniq,
+		mode_info_remove_live_vars(NonLocals),
 
 		%
 		% Now just modecheck each disjunct in turn, and then
@@ -314,6 +314,23 @@
 	% safe to leave it as `unique' on entry to the condition.
 	% The only case we need to set it to `mostly_unique' is
 	% if the condition would clobber it.
+	%
+	% XXX actually that is not true; the code below does
+	% the wrong thing for examples such as this one:
+	%
+	% :- mode p(di).
+	% p(Var) :-
+	%	(if 
+	%		(if semidet_succeed then
+	%			clobber(Var), fail
+	%		else
+	%			true
+	%		)
+	%	then
+	%		blah
+	%	else
+	%		use(Var)
+	%	).
 	%
 	mode_info_add_live_vars(C_Vars),
 	=(ModeInfo),
Index: tests/hard_coded/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/Mmakefile,v
retrieving revision 1.54
diff -u -r1.54 Mmakefile
--- Mmakefile	1999/03/26 04:34:14	1.54
+++ Mmakefile	1999/04/08 17:18:29
@@ -9,7 +9,6 @@
 PROGS=	\
 	address_of_builtins \
 	agg \
-	bidirectional \
 	bigtest \
 	boyer \
 	c_write_string \
@@ -94,6 +93,8 @@
 
 # we do no pass the following tests
 #	var_not_found -- "sorry, not implemented" in polymorphism.m.
+#	bidirectional -- unique mode analysis is overly conservative
+#		and thus rejects this test case.
 
 #-----------------------------------------------------------------------------#
 
Index: tests/hard_coded/cc_nondet_disj.m
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/cc_nondet_disj.m,v
retrieving revision 1.4
diff -u -r1.4 cc_nondet_disj.m
--- cc_nondet_disj.m	1997/05/20 02:08:16	1.4
+++ cc_nondet_disj.m	1999/04/08 17:03:01
@@ -9,7 +9,20 @@
 :- import_module list.
 
 main --> io__read_line(Res),
+	( { Res = ok(['y'|_]), Message = "Yes\n" }
+	; { Res = ok(['n'|_]), Message = "No\n" }
+	; { Message = "Huh?\n" }
+	),
+	io__write_string(Message).
+
+/***
+% This test used to be written as follows, but currently
+% the unique mode analysis is not smart enough to realize
+% that the disjuncts which update the I/O state won't
+% backtrack over I/O if the code is written like that.
+main --> io__read_line(Res),
 	( { Res = ok(['y'|_]) }, io__write_string("Yes\n")
 	; { Res = ok(['n'|_]) }, io__write_string("No\n")
 	; io__write_string("Huh?\n")
 	).
+***/
Index: tests/hard_coded/purity.m
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/purity.m,v
retrieving revision 1.3
diff -u -r1.3 purity.m
--- purity.m	1998/01/06 06:31:40	1.3
+++ purity.m	1999/04/08 17:03:58
@@ -80,9 +80,24 @@
 test3 -->
 	(   { impure incr_x },
 	    { fail }
+	;   { semipure get_x(Y) }
+	),
+	io__format("%d\n", [i(Y)]).
+
+/***
+% This test used to be written as follows, but currently
+% the unique mode analysis is not smart enough to realize
+% that the disjuncts which update the I/O state won't
+% backtrack over I/O if the code is written like that.
+
+% tempt compiler to optimize away impure goal in branch that cannot succeed.
+test3 -->
+	(   { impure incr_x },
+	    { fail }
 	;   { semipure get_x(Y) },
 	    io__format("%d\n", [i(Y)])
 	).
+***/
 
 % regression test for problem with calls to implied modes of impure/semipure
 % preds reporting spurious warnings about impurity markers in the wrong place.
@@ -118,9 +133,24 @@
 test3_inline -->
 	(   { impure incr_x_inline },
 	    { fail }
+	;   { semipure get_x_inline(Y) }
+	),
+	io__format("%d\n", [i(Y)]).
+
+/***
+% This test used to be written as follows, but currently
+% the unique mode analysis is not smart enough to realize
+% that the disjuncts which update the I/O state won't
+% backtrack over I/O if the code is written like that.
+
+% tempt compiler to optimize away impure goal in branch that cannot succeed.
+test3_inline -->
+	(   { impure incr_x_inline },
+	    { fail }
 	;   { semipure get_x_inline(Y) },
 	    io__format("%d\n", [i(Y)])
 	).
+***/
 
 % regression test for problem with calls to implied modes of impure/semipure
 % preds reporting spurious warnings about impurity markers in the wrong place.
Index: tests/hard_coded/uniq_modes.m
===================================================================
RCS file: uniq_modes.m
diff -N uniq_modes.m
--- /dev/null	Fri Apr  9 04:28:35 1999
+++ uniq_modes.m	Fri Apr  9 04:03:24 1999
@@ -0,0 +1,18 @@
+:- module uniq_modes.
+:- interface.
+:- import_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+:- implementation.
+:- import_module list,std_util.
+
+main(In, _Out) :-
+	io__write("looking for", In, Int1),
+	io__nl(Int1, _Int2),
+	fail.
+main(In, Out) :-
+	io__write("not found", In, Int),
+	io__nl(Int, Out).
+
Index: tests/hard_coded/uniq_modes.err_exp
===================================================================
RCS file: uniq_modes.err_exp
diff -N uniq_modes.err_exp
--- /dev/null	Fri Apr  9 04:28:37 1999
+++ uniq_modes.err_exp	Fri Apr  9 04:06:46 1999
@@ -0,0 +1,5 @@
+uniq_modes.m:012: In clause for `main(di, uo)':
+uniq_modes.m:012:   in argument 2 of call to predicate `io:write/3':
+uniq_modes.m:012:   mode error: variable `In' has instantiatedness `mostly_unique',
+uniq_modes.m:012:   expected instantiatedness was `unique'.
+For more information, try recompiling with `-E'.
Index: tests/hard_coded/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.37
diff -u -r1.37 Mmakefile
--- Mmakefile	1999/02/12 04:19:30	1.37
+++ Mmakefile	1999/04/08 18:00:44
@@ -61,6 +61,7 @@
 	undef_mode.m \
 	undef_symbol.m \
 	undef_type.m \
+	uniq_modes.m \
 	uu_type.m \
 	vars_in_wrong_places.m
 

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.