[m-dev.] diff: fix bug with negation and mostly unique modes

[Fergus Henderson]

Estimated hours taken: 1.5

Fix a bug with unique mode analysis of negations
that was reported by Ralph Becket.

compiler/modes.m:
compiler/unique_modes.m:
	When processing negations, set the forward-live variables
	set to empty, because nothing is forward-live after
	the negated goal -- if the negated goal succeeds,
	execution will immediately backtrack.

tests/valid/Mmakefile:
tests/valid/mostly_uniq_neg.m:
	Add a regression test to make sure that the compiler
	now accepts the code that it should, i.e. code
	using backtrackable destructive assignment inside
	a negation.

tests/invalid/Mmakefile:
tests/invalid/uniq_neg.m:
tests/invalid/uniq_neg.err_exp:
	Add a test to make sure that the above change does
	not make the compiler accept code that it shouldn't,
	i.e. code using non-backtrackable destructive assignment
	inside a negation.

Workspace: /home/mercury0/fjh/mercury
Index: compiler/modes.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modes.m,v
retrieving revision 1.236
diff -u -d -r1.236 modes.m
--- modes.m	1999/10/29 07:22:25	1.236
+++ modes.m	1999/11/19 10:46:11
@@ -1040,6 +1040,10 @@
 	{ goal_info_get_nonlocals(GoalInfo0, NonLocals) },
 	{ goal_get_nonlocals(B0, B_Vars) },
 	mode_info_dcg_get_instmap(InstMap0),
+	%
+	% We need to lock the non-local variables, to ensure
+	% that the condition of the if-then-else does not bind them.
+	%
 	mode_info_lock_vars(if_then_else, NonLocals),
 	mode_info_add_live_vars(B_Vars),
 	modecheck_goal(A0, A),
@@ -1068,8 +1072,26 @@
 	mode_checkpoint(enter, "not"),
 	{ goal_info_get_nonlocals(GoalInfo0, NonLocals) },
 	mode_info_dcg_get_instmap(InstMap0),
+	%
+	% when analyzing a negated goal, nothing is forward-live
+	% (live on forward executution after that goal), because
+	% if the goal succeeds then execution will immediately backtrack.
+	% So we need to set the live variables set to empty here.
+	% This allows those variables to be backtrackably
+	% destructively updated.  (If you try to do non-backtrackable
+	% destructive update on such a variable, it will be caught
+	% later on by unique_modes.m.)
+	%
+	=(ModeInfo),
+	{ mode_info_get_live_vars(ModeInfo, LiveVars0) },
+	mode_info_set_live_vars([]),
+	%
+	% We need to lock the non-local variables, to ensure
+	% that the negation does not bind them.
+	%
 	mode_info_lock_vars(negation, NonLocals),
 	modecheck_goal(A0, A),
+	mode_info_set_live_vars(LiveVars0),
 	mode_info_unlock_vars(negation, NonLocals),
 	mode_info_set_instmap(InstMap0),
 	mode_checkpoint(exit, "not").
Index: compiler/unique_modes.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/unique_modes.m,v
retrieving revision 1.59
diff -u -d -r1.59 unique_modes.m
--- unique_modes.m	1999/10/25 03:49:50	1.59
+++ unique_modes.m	1999/11/19 10:58:34
@@ -388,15 +388,34 @@
 
 unique_modes__check_goal_2(not(A0), GoalInfo0, not(A)) -->
 	mode_checkpoint(enter, "not"),
-	{ goal_info_get_nonlocals(GoalInfo0, NonLocals) },
 	mode_info_dcg_get_instmap(InstMap0),
+	%
+	% We need to mark all the variables which are live
+	% after the negation as nondet-live for the negated
+	% goal, since if the negated goal fails, then the
+	% negation will succeed, and so these variables
+	% can be accessed again after backtracking.
+	%
+	{ goal_info_get_nonlocals(GoalInfo0, NonLocals) },
 	{ set__to_sorted_list(NonLocals, NonLocalsList) },
 	=(ModeInfo),
 	{ select_live_vars(NonLocalsList, ModeInfo, LiveNonLocals) },
 	make_var_list_mostly_uniq(LiveNonLocals),
+	%
+	% But nothing is forward-live for the negated goal, since
+	% if the goal succeeds then execution will immediately backtrack.
+	% So we need to set the live variables set to empty here.
+	%
+	{ mode_info_get_live_vars(ModeInfo, LiveVars0) },
+	mode_info_set_live_vars([]),
+	%
+	% We need to lock the non-local variables, to ensure
+	% that the negation does not bind them.
+	%
 	mode_info_lock_vars(negation, NonLocals),
 	unique_modes__check_goal(A0, A),
 	mode_info_unlock_vars(negation, NonLocals),
+	mode_info_set_live_vars(LiveVars0),
 	mode_info_set_instmap(InstMap0),
 	mode_checkpoint(exit, "not").
 
Index: tests/invalid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.52
diff -u -d -r1.52 Mmakefile
--- Mmakefile	1999/11/11 23:17:55	1.52
+++ Mmakefile	1999/11/19 11:10:12
@@ -72,6 +72,7 @@
 	undef_type.m \
 	unify_mode_error.m \
 	uniq_modes.m \
+	uniq_neg.m \
 	uu_type.m \
 	vars_in_wrong_places.m
 
Index: tests/invalid/uniq_neg.err_exp
===================================================================
RCS file: uniq_neg.err_exp
diff -N uniq_neg.err_exp
--- /dev/null	Fri Nov 19 22:05:11 1999
+++ uniq_neg.err_exp	Fri Nov 19 22:10:39 1999
@@ -0,0 +1,5 @@
+uniq_neg.m:025: In clause for `unify(in, in, in, in, di, uo)':
+uniq_neg.m:025:   in argument 3 of call to predicate `uniq_neg:occurs/4':
+uniq_neg.m:025:   mode error: variable `DCG_0' has instantiatedness `mostly_unique',
+uniq_neg.m:025:   expected instantiatedness was `unique'.
+For more information, try recompiling with `-E'.
Index: tests/invalid/uniq_neg.m
===================================================================
RCS file: uniq_neg.m
diff -N uniq_neg.m
--- /dev/null	Fri Nov 19 22:05:11 1999
+++ uniq_neg.m	Fri Nov 19 22:09:49 1999
@@ -0,0 +1,27 @@
+% A regression test, adapted from a bug report by Ralph Becket.
+% Mercury 0.8.1 and earlier reported a spurious mode error
+% for this code.
+
+:- module uniq_neg.
+:- interface.
+:- import_module list, store.
+
+:- type term(S) == mutvar(term_type(S), S).
+:- type var(S) == term(S).
+:- type term_type(S) ---> free ; functor(string, int, list(term(S))).
+
+
+:- pred unify(term(S), term_type(S), term(S), term_type(S), store(S), store(S)).
+:- mode unify(in, in, in, in, di, uo) is semidet.
+
+:- implementation.
+
+:- pred occurs(var(S), list(term(S)), store(S), store(S)).
+:- mode occurs(in, in, di, uo) is semidet.
+
+:- external(occurs/4).
+
+unify(T1, free, _T2, functor(Name2, Arity2, Args2)) -->
+        \+ occurs(T1, Args2),
+        store__set_mutvar(T1, functor(Name2, Arity2, Args2)).
+
Index: tests/valid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.48
diff -u -d -r1.48 Mmakefile
--- Mmakefile	1999/11/14 02:29:19	1.48
+++ Mmakefile	1999/11/19 11:13:38
@@ -88,6 +88,7 @@
 	module_c.m \
 	module_d.m \
 	module_e.m \
+	mostly_uniq_neg.m \
 	mostly_uniq_mode_inf.m \
 	multidet_prune1.m \
 	multidet_test.m \
Index: tests/valid/mostly_uniq_neg.m
===================================================================
RCS file: mostly_uniq_neg.m
diff -N mostly_uniq_neg.m
--- /dev/null	Fri Nov 19 22:05:11 1999
+++ mostly_uniq_neg.m	Fri Nov 19 22:14:49 1999
@@ -0,0 +1,32 @@
+% A regression test, adapted from a bug report by Ralph Becket.
+% Mercury 0.8.1 and earlier reported a spurious mode error
+% for this code.
+
+:- module mostly_uniq_neg.
+:- interface.
+:- import_module list, store.
+
+:- type term(S) == mutvar(term_type(S), S).
+:- type var(S) == term(S).
+:- type term_type(S) ---> free ; functor(string, int, list(term(S))).
+
+
+:- pred unify(term(S), term_type(S), term(S), term_type(S), store(S), store(S)).
+:- mode unify(in, in, in, in, mdi, muo) is semidet.
+
+:- implementation.
+
+:- pred occurs(var(S), list(term(S)), store(S), store(S)).
+:- mode occurs(in, in, mdi, muo) is semidet.
+
+:- external(occurs/4).
+
+:- pred tr_store_set_mutvar(mutvar(T, S), T, store(S), store(S)).
+:- mode tr_store_set_mutvar(in, in, mdi, muo) is det.
+
+:- external(tr_store_set_mutvar/4).
+
+unify(T1, free, _T2, functor(Name2, Arity2, Args2)) -->
+        \+ occurs(T1, Args2),
+        tr_store_set_mutvar(T1, functor(Name2, Arity2, Args2)).
+

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