diff: simplify.m/determinism bug fix

[Fergus Henderson]

Hi,

Anyone want to review this one?

Fix a bug.  For the example code in the bug report, simplify.m simplified
the code by merging two switches, which happened to lead to one branch
containing `error(...), fail'.  The problem was that determinism
analysis inferred a determinism of `failure' for that branch, rather
than `erroneous'.  This caused the code generator to abort, because
the switch was `det' (= model_det) but the case was `failure' (= model_semi).
The basic problem is that simplify.m assumed that simplifying goals
in this way should never make their determinism worse (less precise),
though it might make it better.  But due to the imprecision of determinism
analysis, this assumption was not correct.  The fix is to change determinism
analysis so that the assumption is correct.

compiler/det_analysis.m:
	Add a new predicate exported predicate det_conjunction_detism/3.
	This is similar to calling det_conjunction_canfail/3
	and det_conjunction_maxsoln/3 and combining the results,
	except that if the first goal cannot ever succeed, the determinism
	of the second goal is ignored.  Also, make det_conjunction_canfail/3
	and det_conjunction_maxsoln/3 local rather than exported, to ensure
	that callers from other modules use the new predicate.

compiler/simplify.m:
	Delete conjuncts which are known to be unreachable based on the
	determinism information, as well as based on mode information.
	(The previous code already deleted conjuncts which were
	unreachable due to mode information, but the determinism
	information may be more precise than the mode information.)

compiler/simplify.m:
compiler/follow_code.m:
	Use det_conjunction_detism/3 rather than det_conjunction_canfail/3
	and det_conjunction_maxsoln/3.

tests/hard_coded/Mmake:
tests/hard_coded/det_in_semidet_cntxt.m:
tests/hard_coded/det_in_semidet_cntxt.exp:
	Regression test.

cvs diff: Diffing .
Index: det_analysis.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/det_analysis.m,v
retrieving revision 1.117
diff -u -r1.117 det_analysis.m
--- det_analysis.m	1997/06/29 23:10:26	1.117
+++ det_analysis.m	1997/07/08 12:25:10
@@ -76,11 +76,8 @@
 	% The tables for computing the determinism of compound goals
 	% from the determinism of their components.
 
-:- pred det_conjunction_maxsoln(soln_count, soln_count, soln_count).
-:- mode det_conjunction_maxsoln(in, in, out) is det.
-
-:- pred det_conjunction_canfail(can_fail, can_fail, can_fail).
-:- mode det_conjunction_canfail(in, in, out) is det.
+:- pred det_conjunction_detism(determinism, determinism, determinism).
+:- mode det_conjunction_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.
@@ -508,8 +505,7 @@
 	% Finally combine the results from the three parts
 	( CondCanFail = cannot_fail ->
 		% A -> B ; C is equivalent to A, B if A cannot fail
-		det_conjunction_maxsoln(CondMaxSoln, ThenMaxSoln, MaxSoln),
-		det_conjunction_canfail(CondCanFail, ThenCanFail, CanFail)
+		det_conjunction_detism(CondDetism, ThenDetism, Detism)
 	; CondMaxSoln = at_most_zero ->
 		% A -> B ; C is equivalent to ~A, C if A cannot succeed
 		det_negation_det(CondDetism, MaybeNegDetism),
@@ -519,16 +515,14 @@
 		;
 			MaybeNegDetism = yes(NegDetism)
 		),
-		determinism_components(NegDetism, NegCanFail, NegMaxSoln),
-		det_conjunction_maxsoln(NegMaxSoln, ElseMaxSoln, MaxSoln),
-		det_conjunction_canfail(NegCanFail, ElseCanFail, CanFail)
+		det_conjunction_detism(NegDetism, ElseDetism, Detism)
 	;
 		det_conjunction_maxsoln(CondMaxSoln, ThenMaxSoln, CTMaxSoln),
 		det_switch_maxsoln(CTMaxSoln, ElseMaxSoln, MaxSoln),
-		det_switch_canfail(ThenCanFail, ElseCanFail, CanFail)
+		det_switch_canfail(ThenCanFail, ElseCanFail, CanFail),
+		determinism_components(Detism, CanFail, MaxSoln)
 	),
 
-	determinism_components(Detism, CanFail, MaxSoln),
 	list__append(ThenMsgs, ElseMsgs, AfterMsgs),
 	list__append(CondMsgs, AfterMsgs, Msgs).
 
@@ -611,7 +605,7 @@
 	update_instmap(Goal0, InstMap0, InstMap1),
 	det_infer_conj(Goals0, InstMap1, SolnContext, DetInfo,
 			Goals, DetismB, MsgsB),
-	determinism_components(DetismB, CanFailB, MaxSolnsB),
+	determinism_components(DetismB, CanFailB, _MaxSolnsB),
 
 	%
 	% Next, work out whether the first conjunct is in a first_soln context
@@ -634,14 +628,11 @@
 	%
 	det_infer_goal(Goal0, InstMap0, SolnContextA, DetInfo,
 			Goal, DetismA, MsgsA),
-	determinism_components(DetismA, CanFailA, MaxSolnsA),
 
 	%
 	% Finally combine the results computed above.
 	%
-	det_conjunction_canfail(CanFailA, CanFailB, CanFail),
-	det_conjunction_maxsoln(MaxSolnsA, MaxSolnsB, MaxSolns),
-	determinism_components(Detism, CanFail, MaxSolns),
+	det_conjunction_detism(DetismA, DetismB, Detism),
 	list__append(MsgsA, MsgsB, Msgs).
 
 :- pred det_infer_disj(list(hlds_goal), instmap, soln_context, det_info,
@@ -709,6 +700,22 @@
 
 %-----------------------------------------------------------------------------%
 
+% When figuring out the determinism of a conjunction,
+% if the second goal is unreachable, then then the
+% determinism of the conjunction is just the determinism
+% of the first goal.
+
+det_conjunction_detism(DetismA, DetismB, Detism) :-
+	determinism_components(DetismA, CanFailA, MaxSolnA),
+	( MaxSolnA = at_most_zero ->
+		Detism = DetismA
+	;
+		determinism_components(DetismB, CanFailB, MaxSolnB),
+		det_conjunction_canfail(CanFailA, CanFailB, CanFail),
+		det_conjunction_maxsoln(MaxSolnA, MaxSolnB, MaxSoln),
+		determinism_components(Detism, CanFail, MaxSoln)
+	).
+
 % For the at_most_zero, at_most_one, at_most_many,
 % we're just doing abstract interpretation to count
 % the number of solutions.  Similarly, for the can_fail
@@ -719,6 +726,9 @@
 % pruning, but that the goal occurs in a single-solution
 % context, so only the first solution will be returned.
 
+:- pred det_conjunction_maxsoln(soln_count, soln_count, soln_count).
+:- mode det_conjunction_maxsoln(in, in, out) is det.
+
 det_conjunction_maxsoln(at_most_zero,    at_most_zero,    at_most_zero).
 det_conjunction_maxsoln(at_most_zero,    at_most_one,     at_most_zero).
 det_conjunction_maxsoln(at_most_zero,    at_most_many_cc, at_most_zero).
@@ -741,6 +751,9 @@
 det_conjunction_maxsoln(at_most_many,    at_most_one,     at_most_many).
 det_conjunction_maxsoln(at_most_many,    at_most_many_cc, at_most_many).
 det_conjunction_maxsoln(at_most_many,    at_most_many,    at_most_many).
+
+:- pred det_conjunction_canfail(can_fail, can_fail, can_fail).
+:- mode det_conjunction_canfail(in, in, out) is det.
 
 det_conjunction_canfail(can_fail,    can_fail,    can_fail).
 det_conjunction_canfail(can_fail,    cannot_fail, can_fail).
Index: follow_code.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/follow_code.m,v
retrieving revision 1.40
diff -u -r1.40 follow_code.m
--- follow_code.m	1997/05/21 02:13:24	1.40
+++ follow_code.m	1997/07/08 11:35:56
@@ -267,11 +267,11 @@
 follow_code__conjoin_goal_and_goal_list(Goal0, FollowGoals, Goal) :-
 	Goal0 = GoalExpr0 - GoalInfo0,
 	goal_info_get_determinism(GoalInfo0, Detism0),
-	determinism_components(Detism0, CanFail0, MaxSolns0),
+	determinism_components(Detism0, _CanFail0, MaxSolns0),
 	( MaxSolns0 = at_most_zero ->	
 		Goal = Goal0
 	;
-		check_follow_code_detism(FollowGoals, CanFail0, MaxSolns0),
+		check_follow_code_detism(FollowGoals, Detism0),
 		( GoalExpr0 = conj(GoalList0) ->
 			list__append(GoalList0, FollowGoals, GoalList),
 			GoalExpr = conj(GoalList)
@@ -284,16 +284,14 @@
 	% This check is necessary to make sure that follow_code
 	% doesn't change the determinism of the goal.
 
-:- pred check_follow_code_detism(list(hlds_goal), can_fail, soln_count).
-:- mode check_follow_code_detism(in, in, in) is semidet.
+:- pred check_follow_code_detism(list(hlds_goal), determinism).
+:- mode check_follow_code_detism(in, in) is semidet.
 
-check_follow_code_detism([], _, _).
-check_follow_code_detism([_ - GoalInfo | Goals], CanFail0, MaxSolns0) :-
+check_follow_code_detism([], _).
+check_follow_code_detism([_ - GoalInfo | Goals], Detism0) :-
 	goal_info_get_determinism(GoalInfo, Detism1),
-	determinism_components(Detism1, CanFail1, MaxSolns1),
-	det_conjunction_maxsoln(MaxSolns0, MaxSolns1, MaxSolns0),
-	det_conjunction_canfail(CanFail0, CanFail1, CanFail0),
-	check_follow_code_detism(Goals, CanFail0, MaxSolns0).
+	det_conjunction_detism(Detism0, Detism1, Detism0),
+	check_follow_code_detism(Goals, Detism0).
 
 %-----------------------------------------------------------------------------%
 
Index: simplify.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/simplify.m,v
retrieving revision 1.34
diff -u -r1.34 simplify.m
--- simplify.m	1997/06/25 08:43:15	1.34
+++ simplify.m	1997/07/08 12:25:32
@@ -698,8 +698,14 @@
 			ConjInfo, Info3, Info)
 	    ;
 		% Delete unreachable goals.
-		simplify_info_get_instmap(Info2, InstMap1),
-		instmap__is_unreachable(InstMap1)
+		(
+		    simplify_info_get_instmap(Info2, InstMap1),
+		    instmap__is_unreachable(InstMap1)
+		;
+		    Goal1 = _ - GoalInfo1,
+		    goal_info_get_determinism(GoalInfo1, Detism1),
+		    determinism_components(Detism1, _, at_most_zero)
+		)
 	    ->
 		Info = Info2,
 		simplify__conjoin_goal_and_rev_goal_list(Goal1,
@@ -900,11 +906,7 @@
 		goal_info_set_nonlocals(GInfo2, NonLocals, GInfo3),
 		goal_info_get_determinism(GInfo3, Detism0),
 		goal_info_get_determinism(GInfo1, Detism1),
-		determinism_components(Detism0, CanFail0, MaxSolns0),
-		determinism_components(Detism1, CanFail1, MaxSolns1),
-		det_conjunction_maxsoln(MaxSolns0, MaxSolns1, MaxSolns),
-		det_conjunction_canfail(CanFail0, CanFail1, CanFail),
-		determinism_components(Detism, CanFail, MaxSolns),
+		det_conjunction_detism(Detism0, Detism1, Detism),
 	    	goal_info_set_determinism(GInfo3, Detism, GInfo)
 	    )),
 	list__foldl(ComputeGoalInfo, NewGoals, GoalInfo0, GoalInfo).
cvs diff: Diffing notes
cvs diff: Diffing .
Index: Mmake
===================================================================
RCS file: /home/staff/zs/imp/tests/hard_coded/Mmake,v
retrieving revision 1.46
diff -u -r1.46 Mmake
--- Mmake	1997/06/10 04:03:58	1.46
+++ Mmake	1997/07/09 05:38:34
@@ -18,6 +18,7 @@
 	curry2 \
 	cycles \
 	deep_copy_bug \
+	det_in_semidet_cntxt \
 	division_test \
 	elim_special_pred \
 	expand \
Index: det_in_semidet_cntxt.exp
===================================================================
RCS file: det_in_semidet_cntxt.exp
diff -N det_in_semidet_cntxt.exp
Index: det_in_semidet_cntxt.m
===================================================================
RCS file: det_in_semidet_cntxt.m
diff -N det_in_semidet_cntxt.m
--- /dev/null	Tue Jan  1 15:00:00 1980
+++ det_in_semidet_cntxt.m	Wed Jul  9 15:37:55 1997
@@ -0,0 +1,97 @@
+% Regression test.
+% The Mercury compiler dated Wed Jul 9th 1997
+% got an internal error for this test case.
+
+:- module det_in_semidet_cntxt.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+
+
+:- implementation.
+
+:- import_module list, require, std_util, string.
+
+:- type	name	== 	string.
+:- type sympton	== 	string.
+:- type vaccine	== 	string.
+
+:- type disease	--->	d(name, list(sympton), list(vaccine)).
+
+main -->
+	read_diseases(_Diseases).
+
+
+%------------------------------------------------------------------------------%
+
+	%
+	% read_diseases(D)
+	%
+	% D is the list of diseases.
+	%
+:- pred read_diseases(list(disease), io__state, io__state).
+:- mode read_diseases(out, di, uo) is det.
+
+read_diseases(D) -->
+	read_disease(MaybeDisease),
+	(
+		{ MaybeDisease = yes(Disease) },
+		read_diseases(Diseases),
+		{ D = [Disease | Diseases] }
+	;
+		{ MaybeDisease = no },
+		{ D = [] }
+	).
+
+
+:- pred read_disease(maybe(disease), io__state, io__state).
+:- mode read_disease(out, di, uo) is det.
+
+read_disease(MaybeDisease) -->
+	read_name(MaybeName),
+	(
+		{ MaybeName = yes(Name) },
+		read_symptons(Symptons),
+		read_vaccines(Vaccines),
+		{ MaybeDisease = yes(d(Name, Symptons, Vaccines)) }
+	;
+		{ MaybeName = no },
+		{ MaybeDisease = no }
+	).
+		
+
+:- pred read_name(maybe(string)::out, io__state::di, io__state::uo) is det.
+
+read_name(MaybeName) --> 
+	io__read_word(Result),
+	(
+		{ Result = ok(Name0) },
+		{ string__from_char_list(Name0, Name) },
+		{ MaybeName = yes(Name) }
+	;
+		{ Result = eof },
+		{ MaybeName = no }
+	;
+		{ Result = error(Err) },
+		{ io__error_message(Err, ErrStr) },
+		{ error(ErrStr) }
+	).
+
+
+:- pred read_symptons(list(string)::out, io__state::di, io__state::uo) is det.
+read_symptons([]) --> [].
+
+:- pred read_vaccines(list(string)::out, io__state::di, io__state::uo) is det.
+read_vaccines([]) --> [].
+
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+
+

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