[m-rev.] for review: fix state var bug

[Fergus Henderson]

For review by Ralph.

Estimated hours taken: 4
Branches: main

compiler/make_hlds.m:
	Fix a bug where the state variable transformation was not
	correctly handling the case where the condition of an if-then-else
	referred to a state variable, but the "then" part didn't.

	(Also, fix some incorrect comments for get_rev_conj and get_rev_disj,
	and rearrange some misleading whitespace in the comments for the
	svar_info type.)

tests/valid/Mmakefile:
tests/valid/state_var_bug.m:
	Add a regression test.

----------

The crucial part of this diff is the following lines,
which fix a bug in `add_then_arm_specific_unifiers':

-		new_dot_state_var(StateVar, Dot, VarSet0, VarSet1,
-			SInfoT0, SInfoT1),
+		new_colon_state_var(StateVar, Dot, !VarSet, !SInfoT),
+		prepare_for_next_conjunct(set__make_singleton_set(StateVar),
+			!VarSet, !SInfoT)

If I understand the code correctly, this fixes two problems:
	- since we are appending a new unification, i.e. a new atomic goal,
	  we need to call prepare_for_next_conjunct after we're done.
	- we should be calling new_colon_state_var to get the new version
	  of the state variable, not new_dot_state_var.  I guess previously
	  we were doing it that odd way since the right way didn't work
	  because of the missing call to prepare_for_next_conjunct.

Workspace: /home/jupiter/fjh/ws-jupiter/mercury
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.450
diff -u -d -r1.450 make_hlds.m
--- compiler/make_hlds.m	5 Nov 2003 03:17:39 -0000	1.450
+++ compiler/make_hlds.m	6 Nov 2003 09:35:30 -0000
@@ -8191,9 +8191,9 @@
 
 %-----------------------------------------------------------------------------%
 
-% get_rev_conj(Goal, Conj0, Subst, Conj) :
+% get_rev_conj(Goal, Subst, RevConj0, RevConj) :
 % 	Goal is a tree of conjuncts.  Flatten it into a list (applying Subst),
-%	append Conj0, and return the result in reverse order in Conj.
+%	reverse it, append RevConj0, and return the result in RevConj.
 
 :- pred get_rev_conj(goal::in, prog_substitution::in, list(hlds_goal)::in,
 	list(hlds_goal)::out, prog_varset::in, prog_varset::out,
@@ -8213,9 +8213,9 @@
 		RevConj = list__reverse(ConjList) ++ RevConj0
 	).
 
-% get_rev_par_conj(Goal, ParConj0, Subst, ParConj) :
+% get_rev_par_conj(Goal, Subst, RevParConj0, RevParConj) :
 % 	Goal is a tree of conjuncts.  Flatten it into a list (applying Subst),
-%	append ParConj0, and return the result in reverse order in ParConj.
+%	reverse it, append RevParConj0, and return the result in RevParConj.
 
 :- pred get_rev_par_conj(goal::in, prog_substitution::in, list(hlds_goal)::in,
 	list(hlds_goal)::out, prog_varset::in, prog_varset::out,
@@ -9016,20 +9016,20 @@
 :- type svar_info
 	--->	svar_info(
 			ctxt		::	svar_ctxt,
+
 			num		::	int,
-				%
 				% This is used to number state variables and
 				% is incremented for each source-level
 				% conjunct.
+
 			external_dot	::	svar_map,
-				%
 				% The "read only" state variables in
 				% scope (e.g. external state variables
 				% visible from within a lambda body or
 				% condition of an if-then-else expression.)
+
 			dot		::	svar_map,
 			colon		::	svar_map
-				%
 				% The "read/write" state variables in scope.
 		).
 
@@ -9430,24 +9430,22 @@
 		Thens, Thens, VarSet, VarSet).
 
 add_then_arm_specific_unifiers(Context, [StateVar | StateVars],
-		SInfo0, SInfoC, SInfoT0, SInfoT,
-		Thens0, Thens, VarSet0, VarSet) :-
-	( if /* the condition refers to !:X, but the then-goal doesn't */
+		SInfo0, SInfoC, !SInfoT, !Thens, !VarSet) :-
+	( if % the condition refers to !:X, but the then-goal doesn't
 	     SInfoC  ^ dot ^ elem(StateVar) \= SInfo0 ^ dot ^ elem(StateVar),
-	     SInfoT0 ^ dot ^ elem(StateVar)  = SInfoC ^ dot ^ elem(StateVar)
+	     !.SInfoT ^ dot ^ elem(StateVar)  = SInfoC ^ dot ^ elem(StateVar)
 	  then
-	  	Dot0    = SInfoT0 ^ dot ^ det_elem(StateVar),
-		new_dot_state_var(StateVar, Dot, VarSet0, VarSet1,
-			SInfoT0, SInfoT1),
-		Thens1  = [svar_unification(Context, Dot, Dot0) | Thens0]
+	  	% add a new unifier !:X = !.X
+	  	Dot0    = !.SInfoT ^ dot ^ det_elem(StateVar),
+		new_colon_state_var(StateVar, Dot, !VarSet, !SInfoT),
+		!:Thens = [svar_unification(Context, Dot, Dot0) | !.Thens],
+		prepare_for_next_conjunct(set__make_singleton_set(StateVar),
+			!VarSet, !SInfoT)
 	  else
-	  	SInfoT1 = SInfoT0,
-		Thens1  = Thens0,
-		VarSet1 = VarSet0
+	  	true
 	),
 	add_then_arm_specific_unifiers(Context, StateVars,
-		SInfo0, SInfoC, SInfoT1, SInfoT,
-		Thens1, Thens, VarSet1, VarSet).
+		SInfo0, SInfoC, !SInfoT, !Thens, !VarSet).
 
 %------------------------------------------------------------------------------%
 
Index: tests/valid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.134
diff -u -d -r1.134 Mmakefile
--- tests/valid/Mmakefile	27 Oct 2003 05:59:48 -0000	1.134
+++ tests/valid/Mmakefile	6 Nov 2003 09:43:54 -0000
@@ -168,6 +168,7 @@
 	spurious_purity_warning \
 	stack_alloc \
 	static \
+	state_var_bug \
 	subtype_switch \
 	switch_detection_bug \
 	switch_detection_bug2 \
Index: tests/valid/state_var_bug.m
===================================================================
RCS file: tests/valid/state_var_bug.m
diff -N tests/valid/state_var_bug.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/valid/state_var_bug.m	6 Nov 2003 09:41:07 -0000
@@ -0,0 +1,23 @@
+% This is a regression test for a bug with the state variable transformation.
+% It was not correctly handling the case where the condition of an if-then-else
+% referred to a state variable, but the "then" part didn't.
+% This lead to a determinism error in the following code.
+
+:- module state_var_bug.
+:- interface.
+
+:- pred foo(int::in, int::out) is det.
+
+:- implementation.
+
+foo(!X) :-
+	( copy(!X) ->
+		true
+	;
+		true
+	),
+	(
+		fail
+	;
+		copy(!X)
+	).

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------