[m-dev.] for review: fix bug in unique mode checking

[Fergus Henderson]

Since no-one has raised any objections, I will go ahead and commit this one.

On 09-Apr-1999, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> 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.
> --------------------------------------------------------------------------
> mercury-developers mailing list
> Post messages to:       mercury-developers at cs.mu.oz.au
> Administrative Queries: owner-mercury-developers at cs.mu.oz.au
> Subscriptions:          mercury-developers-request at cs.mu.oz.au
> --------------------------------------------------------------------------
> 

-- 
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.