diff: Fix bug in modechecking of non-local lambda vars

[Andrew Bromage]

G'day all.

Fergus, could you please review this?  Thanks.

Note: In this diff, the regression test files are included in full
since the diff is a bit confusing.

Cheers,
Andrew Bromage


Estimated hours taken: 6

Fix a semantic hole.  Previously, unique variables could be used
as non-local variables inside a lambda goal and shared within that
lambda.  This fixes the problem by requiring that all non-local
vars to a lambda must be ground-shared.

compiler/modecheck_unify.m:
	Changes detailed above.

compiler/mode_errors.m:
	Add a new kind of mode error, mode_error_non_local_lambda_var.
	One small change to find_important_errors/3 to ensure that this
	error will be reported if the lambda is an implicit call argument
	unification.

compiler/inst_util.m:
	Export make_shared_inst_list/4.

compiler/instmap.m:
	New predicate: instmap__set_vars/4, which sets multiple vars
	in an instmap.

tests/invalid/bind_var_errors.m:
tests/invalid/bind_var_errors.err_exp:
	Regression test.


Index: compiler/inst_util.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/inst_util.m,v
retrieving revision 1.9
diff -u -r1.9 inst_util.m
--- inst_util.m	1998/01/23 12:56:36	1.9
+++ inst_util.m	1998/02/05 05:09:37
@@ -75,6 +75,14 @@
 	% original inst but with all occurrences of `unique' replaced
 	% with `mostly_unique'.
 
+:- pred make_shared_inst_list(list(inst), module_info, list(inst), module_info).
+:- mode make_shared_inst_list(in, in, out, out) is det.
+
+	% Given a list of insts, return a new list of insts which is the
+	% same as the original list of insts, but with all occurrences
+	% of `unique' replaced with `shared'.  It is an error if any part
+	% of the inst list is free.
+
 %-----------------------------------------------------------------------------%
 
 :- pred inst_merge(inst, inst, module_info, inst, module_info).
@@ -970,9 +978,6 @@
 maybe_make_shared_inst_list([_|_], [], _, _, _) :-
 	error("maybe_make_shared_inst_list: length mismatch").
 
-:- pred make_shared_inst_list(list(inst), module_info,
-				list(inst), module_info).
-:- mode make_shared_inst_list(in, in, out, out) is det.
 
 make_shared_inst_list([], ModuleInfo, [], ModuleInfo).
 make_shared_inst_list([Inst0 | Insts0], ModuleInfo0,
Index: compiler/instmap.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/instmap.m,v
retrieving revision 1.18
diff -u -r1.18 instmap.m
--- instmap.m	1998/01/23 12:56:37	1.18
+++ instmap.m	1998/02/03 12:47:18
@@ -133,6 +133,11 @@
 :- pred instmap__set(instmap, var, inst, instmap).
 :- mode instmap__set(in, in, in, out) is det.
 
+	% Set multiple entries in an instmap.
+	%
+:- pred instmap__set_vars(instmap, list(var), list(inst), instmap).
+:- mode instmap__set_vars(in, in, in, out) is det.
+
 :- pred instmap_delta_set(instmap_delta, var, inst, instmap_delta).
 :- mode instmap_delta_set(in, in, in, out) is det.
 
@@ -376,6 +381,15 @@
 instmap__set(reachable(InstMapping0), Var, Inst,
 		reachable(InstMapping)) :-
 	map__set(InstMapping0, Var, Inst, InstMapping).
+
+instmap__set_vars(InstMap, [], [], InstMap).
+instmap__set_vars(InstMap0, [V | Vs], [I | Is], InstMap) :-
+	instmap__set(InstMap0, V, I, InstMap1),
+	instmap__set_vars(InstMap1, Vs, Is, InstMap).
+instmap__set_vars(_, [_ | _], [], _) :-
+	error("instmap__set_vars").
+instmap__set_vars(_, [], [_ | _], _) :-
+	error("instmap__set_vars").
 
 instmap_delta_set(unreachable, _Var, _Inst, unreachable).
 instmap_delta_set(reachable(InstMapping0), Var, Inst, Instmap) :-
Index: compiler/mode_errors.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/mode_errors.m,v
retrieving revision 1.54
diff -u -r1.54 mode_errors.m
--- mode_errors.m	1998/01/30 06:12:50	1.54
+++ mode_errors.m	1998/02/05 07:01:26
@@ -68,6 +68,9 @@
 	;	mode_error_bind_var(var_lock_reason, var, inst, inst)
 			% attempt to bind a non-local variable inside
 			% a negated context
+	;	mode_error_non_local_lambda_var(var, inst)
+			% attempt to pass a live non-ground var as a
+			% non-local variable to a lambda goal
 	;	mode_error_unify_var_var(var, var, inst, inst)
 			% attempt to unify two free variables
 	;	mode_error_unify_var_functor(var, cons_id, list(var),
@@ -190,6 +193,8 @@
 	report_mode_error_no_mode_decl(ModeInfo).
 report_mode_error(mode_error_bind_var(Reason, Var, InstA, InstB), ModeInfo) -->
 	report_mode_error_bind_var(ModeInfo, Reason, Var, InstA, InstB).
+report_mode_error(mode_error_non_local_lambda_var(Var, Inst), ModeInfo) -->
+	report_mode_error_non_local_lambda_var(ModeInfo, Var, Inst).
 report_mode_error(mode_error_unify_var_var(VarA, VarB, InstA, InstB),
 		ModeInfo) -->
 	report_mode_error_unify_var_var(ModeInfo, VarA, VarB, InstA, InstB).
@@ -280,12 +285,17 @@
 
 find_important_errors([], [], []).
 find_important_errors([Error | Errors], ImportantErrors, OtherErrors) :-
-	Error = delayed_goal(_, mode_error_info(_, _, _, ModeContext), _),
+	Error = delayed_goal(_, mode_error_info(_, ModeError, _, ModeContext),
+				_),
 	(
 		% an error is important unless it is a non-explicit unification,
 		% i.e. a head unification or a call argument unification
 		ModeContext = unify(unify_context(UnifyContext, _), _),
-		UnifyContext \= explicit
+		UnifyContext \= explicit,
+		% except that errors in lambda goals are important even
+		% if the unification that creates the lambda goal is
+		% an implicit one
+		ModeError \= mode_error_non_local_lambda_var(_, _)
 	->
 		ImportantErrors1 = ImportantErrors,
 		OtherErrors = [Error | OtherErrors1]
@@ -417,6 +427,28 @@
 	;
 		[]
 	).
+
+%-----------------------------------------------------------------------------%
+
+:- pred report_mode_error_non_local_lambda_var(mode_info, var, inst,
+					io__state, io__state).
+:- mode report_mode_error_non_local_lambda_var(mode_info_ui, in, in,
+					di, uo) is det.
+
+report_mode_error_non_local_lambda_var(ModeInfo, Var, VarInst) -->
+	{ mode_info_get_context(ModeInfo, Context) },
+	{ mode_info_get_varset(ModeInfo, VarSet) },
+	{ mode_info_get_instvarset(ModeInfo, InstVarSet) },
+	mode_info_write_context(ModeInfo),
+	prog_out__write_context(Context),
+	io__write_string("  mode error: variable `"),
+	mercury_output_var(Var, VarSet, no),
+	io__write_string("' has instantiatedness `"),
+	output_inst(VarInst, InstVarSet),
+	io__write_string("',\n"),
+	prog_out__write_context(Context),
+	io__write_string("  expected instantiatedness for non-local variables of  lambda goals\n"),
+	io__write_string("  is `ground'.\n").
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/modecheck_unify.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/modecheck_unify.m,v
retrieving revision 1.27
diff -u -r1.27 modecheck_unify.m
--- modecheck_unify.m	1998/01/30 06:12:52	1.27
+++ modecheck_unify.m	1998/02/06 00:16:48
@@ -334,6 +334,7 @@
 	% First modecheck the lambda goal itself:
 	%
 	% initialize the initial insts of the lambda variables,
+	% check that the non-local vars are ground,
 	% lock the non-local vars,
 	% mark the non-clobbered lambda variables as live,
 	% modecheck the goal,
@@ -384,35 +385,94 @@
 	Goal0 = _ - GoalInfo0,
 	goal_info_get_nonlocals(GoalInfo0, NonLocals0),
 	set__delete_list(NonLocals0, Vars, NonLocals),
-	mode_info_lock_vars(lambda(PredOrFunc), NonLocals,
-		ModeInfo2, ModeInfo3),
- 
-	mode_checkpoint(enter, "lambda goal", ModeInfo3, ModeInfo4),
-	% if we're being called from unique_modes.m, then we need to 
-	% call unique_modes__check_goal rather than modecheck_goal.
-	( HowToCheckGoal = check_unique_modes ->
-		unique_modes__check_goal(Goal0, Goal, ModeInfo4, ModeInfo5)
+	set__to_sorted_list(NonLocals, NonLocalsList),
+	instmap__lookup_vars(NonLocalsList, InstMap1, NonLocalInsts),
+	mode_info_get_module_info(ModeInfo2, ModuleInfo2),
+	(
+		% XXX This test is too conservative.
+		%
+		%     We should allow non-local variables to be non-ground
+		%     if they are dead after this unification.  In addition,
+		%     we should not "share" a unique non-local variable if
+		%     these two conditions hold:
+		%
+		%	- It is dead after this unification.
+		%	- It is not shared within the lambda body.
+		%
+		%     Unfortunately, we can't test the latter condition
+		%     until after we've mode-checked the lambda body.
+
+		inst_list_is_ground(NonLocalInsts, ModuleInfo2)
+	->
+		make_shared_inst_list(NonLocalInsts, ModuleInfo2,
+			SharedNonLocalInsts, ModuleInfo3),
+		instmap__set_vars(InstMap1, NonLocalsList, SharedNonLocalInsts,
+			InstMap2),
+		mode_info_set_module_info(ModeInfo2, ModuleInfo3, ModeInfo3),
+		mode_info_set_instmap(InstMap2, ModeInfo3, ModeInfo4),
+
+		mode_info_lock_vars(lambda(PredOrFunc), NonLocals,
+				ModeInfo4, ModeInfo5),
+
+		mode_checkpoint(enter, "lambda goal", ModeInfo5, ModeInfo6),
+		% if we're being called from unique_modes.m, then we need to 
+		% call unique_modes__check_goal rather than modecheck_goal.
+		(
+			HowToCheckGoal = check_unique_modes
+		->
+			unique_modes__check_goal(Goal0, Goal, ModeInfo6,
+				ModeInfo7)
+		;
+			modecheck_goal(Goal0, Goal, ModeInfo6, ModeInfo7)
+		),
+		mode_list_get_final_insts(Modes, ModuleInfo0, FinalInsts),
+		modecheck_final_insts(Vars, FinalInsts, ModeInfo7, ModeInfo8),
+		mode_checkpoint(exit, "lambda goal", ModeInfo8, ModeInfo9),
+
+		mode_info_remove_live_vars(LiveVars, ModeInfo9, ModeInfo10),
+		mode_info_unlock_vars(lambda(PredOrFunc), NonLocals,
+			ModeInfo10, ModeInfo11),
+
+		%
+		% Ensure that the non-local vars are shared OUTSIDE the
+		% lambda unification as well as inside.
+		%
+
+		instmap__set_vars(InstMap0, NonLocalsList, SharedNonLocalInsts,
+			InstMap11),
+		mode_info_set_instmap(InstMap11, ModeInfo11, ModeInfo12),
+
+		%
+		% Now modecheck the unification of X with the lambda-expression.
+		%
+
+		set__to_sorted_list(NonLocals, ArgVars),
+		modecheck_unify_lambda(X, PredOrFunc, ArgVars, Modes,
+				Det, Unification0, Mode, Unification,
+				ModeInfo12, ModeInfo),
+		RHS = lambda_goal(PredOrFunc, Vars, Modes, Det, Goal)
 	;
-		modecheck_goal(Goal0, Goal, ModeInfo4, ModeInfo5)
-	),
-	mode_list_get_final_insts(Modes, ModuleInfo0, FinalInsts),
-	modecheck_final_insts(Vars, FinalInsts, ModeInfo5, ModeInfo6),
-	mode_checkpoint(exit, "lambda goal", ModeInfo6, ModeInfo7),
- 
-	mode_info_remove_live_vars(LiveVars, ModeInfo7, ModeInfo8),
-	mode_info_unlock_vars(lambda(PredOrFunc), NonLocals,
-		ModeInfo8, ModeInfo9),
-	mode_info_set_instmap(InstMap0, ModeInfo9, ModeInfo10),
- 
-	%
-	% Now modecheck the unification of X with the lambda-expression.
-	%
+		list__filter(lambda([Var :: in] is semidet,
+			( instmap__lookup_var(InstMap1, Var, Inst),
+			  \+ inst_is_ground(ModuleInfo2, Inst)
+			)),
+			NonLocalsList, NonGroundNonLocals),
+		( NonGroundNonLocals = [BadVar | _] ->
+			instmap__lookup_var(InstMap1, BadVar, BadInst),
+			set__singleton_set(WaitingVars, BadVar),
+			mode_info_error(WaitingVars,
+				mode_error_non_local_lambda_var(BadVar,
+						BadInst),
+				ModeInfo2, ModeInfo)
+		;
+			error("modecheck_unification(lambda): very strange var")
+		),
+			% return any old garbage
+		RHS = lambda_goal(PredOrFunc, Vars, Modes0, Det, Goal0),
+		Mode = (free -> free) - (free -> free),
+		Unification = Unification0
+	).
  
-	set__to_sorted_list(NonLocals, ArgVars),
-	modecheck_unify_lambda(X, PredOrFunc, ArgVars, Modes,
-			Det, Unification0, Mode, Unification,
-			ModeInfo10, ModeInfo),
-	RHS = lambda_goal(PredOrFunc, Vars, Modes, Det, Goal).
 
 :- pred modecheck_unify_lambda(var, pred_or_func, list(var),
 			list(mode), determinism, unification,
Index: tests/invalid/bind_var_errors.m
===================================================================
:- module bind_var_errors.
:- interface.

:- import_module int.

:- pred bind_var_in_negation is semidet.

:- pred bind_var_in_ite_cond(int :: in) is semidet.

:- pred bind_var_in_lambda is semidet.

:- pred share_var_in_lambda(T :: di) is det.

:- pred share_dead_var_in_lambda(T :: di) is det.

:- pred clobber_var_in_lambda(T :: di) is det.

:- implementation.

:- pragma no_inline(consume/1).
:- pred consume(T :: in) is det.
consume(_).

:- pragma no_inline(destroy/1).
:- pred destroy(T :: di) is det.
destroy(_).

:- pragma no_inline(share/1).
:- pred share(T :: in) is det.
share(_).

bind_var_in_negation :-
	\+ (X = 42),
	consume(X).

bind_var_in_ite_cond(X) :-
	(
		X = 42,
		Y = 42
	->
		true
	;
		true
	),
	consume(Y).

bind_var_in_lambda :-
	call((pred) is det :- Y = 42),
	consume(Y).

share_var_in_lambda(X) :-
	call((pred) is det :- share(X)),
	destroy(X).

	% This one is OK since X is dead after the lambda.
share_dead_var_in_lambda(X) :-
	call((pred) is det :- share(X)).

clobber_var_in_lambda(X) :-
	call((pred) is det :- destroy(X)),
	destroy(X).

Index: tests/invalid/bind_var_errors.err_exp
===================================================================
bind_var_errors.m:033: In clause for `bind_var_in_negation':
bind_var_errors.m:033:   scope error: attempt to bind a variable inside a negation.
bind_var_errors.m:033:   Variable `X' has instantiatedness `free',
bind_var_errors.m:033:   expected instantiatedness was `unique(42)'.
bind_var_errors.m:039: In clause for `bind_var_in_ite_cond(in)':
bind_var_errors.m:039:   scope error: attempt to bind a non-local variable inside the
bind_var_errors.m:039:   condition of an if-then-else.
bind_var_errors.m:039:   Variable `Y' has instantiatedness `free',
bind_var_errors.m:039:   expected instantiatedness was `unique(42)'.
bind_var_errors.m:048: In clause for `bind_var_in_lambda':
bind_var_errors.m:048:   in argument 1 of call to predicate `call/1':
bind_var_errors.m:048:   mode error: variable `Y' has instantiatedness `free',
bind_var_errors.m:048:   expected instantiatedness for non-local variables of  lambda goals
  is `ground'.
bind_var_errors.m:053: In clause for `share_var_in_lambda(di)':
bind_var_errors.m:053:   in argument 1 of call to predicate `bind_var_errors:destroy/1':
bind_var_errors.m:053:   mode error: variable `X' has instantiatedness `ground',
bind_var_errors.m:053:   expected instantiatedness was `unique'.
bind_var_errors.m:060: In clause for `clobber_var_in_lambda(di)':
bind_var_errors.m:060:   in argument 1 of call to predicate `bind_var_errors:destroy/1':
bind_var_errors.m:060:   unique-mode error: the called procedure would clobber
bind_var_errors.m:060:   its argument, but variable `X' is still live.
For more information, try recompiling with `-E'.