[m-rev.] For review: make impure goals with inst any vars in negated contexts
Ralph Becket
rafe at cs.mu.OZ.AU
Fri Oct 28 14:02:25 AEST 2005
Estimated hours taken: 10
Branches: main
Require impurity annotations on goals in negated contexts or lambdas
containing non-local inst any variables. Such goals can violate referential
transparency, even though they might otherwise be considered pure.
NEWS:
Mention the new change.
compiler/inst_util.m:
Add utility preds inst_contains_any/2 and var_inst_contains_any/3.
compiler/mode_errors.m:
Add three new mode errors to cover the new cases.
compiler/mode_info.m:
Add field `in_negated_context' to the mode_info.
compiler/modecheck_call.m:
compiler/modecheck_unify.m:
Perform purity checks for goals in negated contexts containing inst any
non-locals or lambdas containing inst any non-locals.
compiler/modes.m:
Add negated context tracking.
compiler/purity.m:
Defer purity checking on goals in negated contexts because we
don't have inst information at the time purity analysis is run.
compiler/unique_modes.m:
We now have to include the goal_info in calls to modecheck_call_pred.
doc/reference_manual.texi:
Document the new requirement.
tests/invalid/Mmakefile:
tests/invalid/anys_in_negated_contexts.err_exp:
tests/invalid/anys_in_negated_contexts.m:
Add a test case.
Index: NEWS
===================================================================
RCS file: /home/mercury1/repository/mercury/NEWS,v
retrieving revision 1.391
diff -u -r1.391 NEWS
--- NEWS 26 Oct 2005 05:04:12 -0000 1.391
+++ NEWS 28 Oct 2005 03:33:07 -0000
@@ -5,6 +5,8 @@
==========
Changes to the Mercury language:
+* Goals in negated contexts using inst any non-local variables or lambda
+ expressions containing inst any non-locals must now be marked as impure.
* The Mercury typeclass system now supports functional dependencies.
* We now have support for optional module initialisation and finalisation.
* We now have support for impure module-local mutable variables.
Index: compiler/inst_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/inst_util.m,v
retrieving revision 1.42
diff -u -r1.42 inst_util.m
--- compiler/inst_util.m 28 Oct 2005 02:10:10 -0000 1.42
+++ compiler/inst_util.m 28 Oct 2005 03:28:27 -0000
@@ -41,6 +41,7 @@
:- interface.
:- import_module hlds.hlds_module.
+:- import_module hlds.instmap.
:- import_module parse_tree.prog_data.
:- import_module bool.
@@ -108,6 +109,15 @@
:- pred inst_contains_nonstandard_func_mode(module_info::in, mer_inst::in)
is semidet.
+ % Succeed iff the inst is any or contains any.
+ %
+:- pred inst_contains_any(module_info::in, (mer_inst)::in) is semidet.
+
+ % Succeed iff the given var's inst is any or contains any.
+ %
+:- pred var_inst_contains_any(module_info::in, instmap::in, prog_var::in)
+ is semidet.
+
% Succeed iff the first argument is a function pred_inst_info
% whose mode does not match the standard func mode.
%
@@ -1677,6 +1687,38 @@
%-----------------------------------------------------------------------------%
+inst_contains_any(ModuleInfo, Inst) :-
+ set__init(Expansions),
+ inst_contains_any_2(ModuleInfo, Inst, Expansions).
+
+
+:- pred inst_contains_any_2(module_info::in, (mer_inst)::in,
+ set(inst_name)::in) is semidet.
+
+inst_contains_any_2(_ModuleInfo, any(_), _Expansions).
+
+inst_contains_any_2(ModuleInfo, bound(_, BoundInsts), Expansions) :-
+ list__member(functor(_, Insts), BoundInsts),
+ list__member(Inst, Insts),
+ inst_contains_any_2(ModuleInfo, Inst, Expansions).
+
+inst_contains_any_2(_ModuleInfo, inst_var(_), _Expansions) :-
+ error("internal error: uninstantiated inst parameter").
+
+inst_contains_any_2(ModuleInfo, defined_inst(InstName), Expansions0) :-
+ \+ set__member(InstName, Expansions0),
+ Expansions = set__insert(Expansions0, InstName),
+ inst_lookup(ModuleInfo, InstName, Inst),
+ inst_contains_any_2(ModuleInfo, Inst, Expansions).
+
+%-----------------------------------------------------------------------------%
+
+solver_var_inst_contains_any(ModuleInfo, VarTypes, Instmap, Var) :-
+ instmap__lookup_var(Instmap, Var, Inst),
+ inst_contains_any(ModuleInfo, Inst).
+
+%-----------------------------------------------------------------------------%
+
pred_inst_info_is_nonstandard_func_mode(ModuleInfo, PredInstInfo) :-
PredInstInfo = pred_inst_info(function, ArgModes, _),
Arity = list__length(ArgModes),
Index: compiler/mode_errors.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mode_errors.m,v
retrieving revision 1.94
diff -u -r1.94 mode_errors.m
--- compiler/mode_errors.m 28 Oct 2005 02:10:23 -0000 1.94
+++ compiler/mode_errors.m 28 Oct 2005 03:05:28 -0000
@@ -125,10 +125,24 @@
% schedule_culprit gives the reason why they couldn't be scheduled.
; mode_error_final_inst(int, prog_var, mer_inst, mer_inst,
- final_inst_error).
+ final_inst_error)
% One of the head variables did not have the expected final inst
% on exit from the proc.
+ ; purity_error_should_be_impure(list(prog_var))
+ % A goal in a negated context contains vars with inst any was
+ % not marked impure, as it should be.
+
+ ; purity_error_wrongly_impure(purity)
+ % A goal in a negated context was erroneously marked as impure.
+ % The purity argument specifies what purity the goal has.
+
+ ; purity_error_lambda_should_be_impure(list(prog_var)).
+ % A lambda term containing inst any non-locals should have been
+ % declared impure, but hasn't been (executing such a lambda may
+ % further constrain the inst any variables, thereby violating
+ % referential transparency).
+
:- type schedule_culprit
---> goal_itself_was_impure
; goals_followed_by_impure_goal(hlds_goal)
@@ -329,6 +343,15 @@
ModeError = mode_error_final_inst(ArgNum, Var, VarInst, Inst, Reason),
Specs = mode_error_final_inst_to_specs(ModeInfo, ArgNum, Var, VarInst,
Inst, Reason)
+ ;
+ ModeError = purity_error_should_be_impure(Vars),
+ Specs = purity_error_should_be_impure_to_specs(ModeInfo, Vars)
+ ;
+ ModeError = purity_error_wrongly_impure(Purity),
+ Specs = purity_error_wrongly_impure_to_specs(ModeInfo, Purity)
+ ;
+ ModeError = purity_error_lambda_should_be_impure(Vars),
+ Specs = purity_error_lambda_should_be_impure_to_specs(ModeInfo, Vars)
).
:- func mode_warning_to_specs(mode_info::in, mode_warning_info::in)
@@ -1069,6 +1092,62 @@
%-----------------------------------------------------------------------------%
+:- func purity_error_should_be_impure_to_specs(mode_info::in,
+ list(prog_var)::in) = (list(error_msg_spec)::out(error_msg_specs))
+ is det.
+
+purity_error_should_be_impure_to_specs(ModeInfo, Vars) = Specs :-
+ mode_info_get_context(ModeInfo, Context),
+ mode_info_get_varset(ModeInfo, VarSet),
+ Pieces = [
+ words("purity error: goal should be impure because it appears"),
+ words("in a negated context, but involves the following variables"),
+ words("whose insts contain `any':"),
+ words(mercury_vars_to_string(Vars, VarSet, no))
+ ],
+ Specs = [
+ mode_info_context_to_spec(ModeInfo),
+ error_msg_spec(no, Context, 0, Pieces)
+ ].
+
+%-----------------------------------------------------------------------------%
+
+:- func purity_error_wrongly_impure_to_specs(mode_info::in, purity::in) =
+ (list(error_msg_spec)::out(error_msg_specs)) is det.
+
+purity_error_wrongly_impure_to_specs(ModeInfo, Purity) = Specs :-
+ mode_info_get_context(ModeInfo, Context),
+ Pieces = [
+ words("purity error: goal is marked as impure, but is actually"),
+ words(if Purity = purity_pure then "pure" else "semipure")
+ ],
+ Specs = [
+ mode_info_context_to_spec(ModeInfo),
+ error_msg_spec(no, Context, 0, Pieces)
+ ].
+
+%-----------------------------------------------------------------------------%
+
+:- func purity_error_lambda_should_be_impure_to_specs(mode_info::in,
+ list(prog_var)::in) = (list(error_msg_spec)::out(error_msg_specs))
+ is det.
+
+purity_error_lambda_should_be_impure_to_specs(ModeInfo, Vars) = Specs :-
+ mode_info_get_context(ModeInfo, Context),
+ mode_info_get_varset(ModeInfo, VarSet),
+ Pieces = [
+ words("purity error: lambda should be impure because it"),
+ words("contains the following non-local variables"),
+ words("whose insts contain `any':"),
+ words(mercury_vars_to_string(Vars, VarSet, no))
+ ],
+ Specs = [
+ mode_info_context_to_spec(ModeInfo),
+ error_msg_spec(no, Context, 0, Pieces)
+ ].
+
+%-----------------------------------------------------------------------------%
+
maybe_report_error_no_modes(PredId, PredInfo, ModuleInfo, !IO) :-
pred_info_import_status(PredInfo, ImportStatus),
( ImportStatus = local ->
Index: compiler/mode_info.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mode_info.m,v
retrieving revision 1.77
diff -u -r1.77 mode_info.m
--- compiler/mode_info.m 28 Oct 2005 02:10:23 -0000 1.77
+++ compiler/mode_info.m 28 Oct 2005 03:05:28 -0000
@@ -122,6 +122,7 @@
:- pred mode_info_get_warnings(mode_info::in, list(mode_warning_info)::out)
is det.
:- pred mode_info_get_need_to_requantify(mode_info::in, bool::out) is det.
+:- pred mode_info_get_in_negated_context(mode_info::in, bool::out) is det.
:- pred mode_info_get_num_errors(mode_info::in, int::out) is det.
:- pred mode_info_get_liveness(mode_info::in, set(prog_var)::out) is det.
:- pred mode_info_get_varset(mode_info::in, prog_varset::out) is det.
@@ -171,6 +172,8 @@
mode_info::in, mode_info::out) is det.
:- pred mode_info_set_need_to_requantify(bool::in,
mode_info::in, mode_info::out) is det.
+:- pred mode_info_set_in_negated_context(bool::in,
+ mode_info::in, mode_info::out) is det.
:- pred mode_info_add_live_vars(set(prog_var)::in,
mode_info::in, mode_info::out) is det.
:- pred mode_info_remove_live_vars(set(prog_var)::in,
@@ -318,7 +321,10 @@
% Set to `yes' if we need to requantify the procedure body
% after mode analysis finishes.
- need_to_requantify :: bool
+ need_to_requantify :: bool,
+
+ % Set to `yes' if we are in a negated context.
+ in_negated_context :: bool
).
:- type mode_info
@@ -443,9 +449,11 @@
CheckingExtraGoals = no,
MayInitSolverVars = yes,
NeedToRequantify = no,
+ InNegatedContext = no,
ModeSubInfo = mode_sub_info(ProcId, VarSet, Unreachable, Changed,
- CheckingExtraGoals, InstMapping0, WarningList, NeedToRequantify),
+ CheckingExtraGoals, InstMapping0, WarningList, NeedToRequantify,
+ InNegatedContext),
ModeInfo = mode_info(ModuleInfo, PredId, VarTypes, Debug,
Context, ModeContext, InstMapping0, LockedVars, DelayInfo,
@@ -468,6 +476,7 @@
mode_info_get_errors(MI, MI ^ errors).
mode_info_get_warnings(MI, MI ^ mode_sub_info ^ warnings).
mode_info_get_need_to_requantify(MI, MI ^ mode_sub_info ^ need_to_requantify).
+mode_info_get_in_negated_context(MI, MI ^ mode_sub_info ^ in_negated_context).
mode_info_get_delay_info(MI, MI ^ delay_info).
mode_info_get_live_vars(MI, MI ^ live_vars).
mode_info_get_nondet_live_vars(MI, MI ^ nondet_live_vars).
@@ -492,6 +501,8 @@
MI ^ mode_sub_info ^ warnings := Warnings).
mode_info_set_need_to_requantify(NTRQ, MI,
MI ^ mode_sub_info ^ need_to_requantify := NTRQ).
+mode_info_set_in_negated_context(INC, MI,
+ MI ^ mode_sub_info ^ in_negated_context := INC).
mode_info_set_delay_info(DelayInfo, MI, MI ^ delay_info := DelayInfo).
mode_info_set_live_vars(LiveVarsList, MI, MI ^ live_vars := LiveVarsList).
mode_info_set_nondet_live_vars(NondetLiveVars, MI,
Index: compiler/modecheck_call.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modecheck_call.m,v
retrieving revision 1.62
diff -u -r1.62 modecheck_call.m
--- compiler/modecheck_call.m 28 Oct 2005 02:10:24 -0000 1.62
+++ compiler/modecheck_call.m 28 Oct 2005 03:05:28 -0000
@@ -36,7 +36,8 @@
:- pred modecheck_call_pred(pred_id::in, maybe(determinism)::in,
proc_id::in, proc_id::out, list(prog_var)::in, list(prog_var)::out,
- extra_goals::out, mode_info::in, mode_info::out) is det.
+ hlds_goal_info::in, extra_goals::out, mode_info::in, mode_info::out)
+ is det.
:- pred modecheck_higher_order_call(pred_or_func::in, prog_var::in,
list(prog_var)::in, list(prog_var)::out, list(mer_mode)::out,
@@ -100,7 +101,7 @@
:- import_module varset.
modecheck_call_pred(PredId, DeterminismKnown, ProcId0, TheProcId,
- ArgVars0, ArgVars, ExtraGoals, !ModeInfo) :-
+ ArgVars0, ArgVars, GoalInfo, ExtraGoals, !ModeInfo) :-
mode_info_get_may_change_called_proc(!.ModeInfo, MayChangeCalledProc),
mode_info_get_preds(!.ModeInfo, Preds),
mode_info_get_module_info(!.ModeInfo, ModuleInfo),
@@ -121,9 +122,44 @@
compute_arg_offset(PredInfo, ArgOffset),
pred_info_get_markers(PredInfo, Markers),
- % In order to give better diagnostics, we handle the cases where there are
- % zero or one modes for the called predicate specially.
+ mode_info_get_instmap(!.ModeInfo, InstMap),
+ AnyVars =
+ list__filter(var_inst_contains_any(ModuleInfo, InstMap), ArgVars0),
+
(
+ % If we are in a negated context and one or more vars have
+ % inst any then this call is required to be marked impure
+ % since it may violate referential transparency.
+ %
+ mode_info_get_in_negated_context(!.ModeInfo, yes),
+ \+ goal_info_is_impure(GoalInfo),
+ AnyVars \= []
+ ->
+ set__init(WaitingVars),
+ mode_info_error(WaitingVars, purity_error_should_be_impure(AnyVars),
+ !ModeInfo),
+ TheProcId = invalid_proc_id,
+ ArgVars = ArgVars0,
+ ExtraGoals = no_extra_goals
+ ;
+ % Report a purity error if a pred call is erroneously marked as impure
+ % in a negated context.
+ %
+ mode_info_get_in_negated_context(!.ModeInfo, yes),
+ goal_info_is_impure(GoalInfo),
+ AnyVars = [],
+ Purity \= purity_impure
+ ->
+ set__init(WaitingVars),
+ mode_info_error(WaitingVars, purity_error_wrongly_impure(Purity),
+ !ModeInfo),
+ TheProcId = invalid_proc_id,
+ ArgVars = ArgVars0,
+ ExtraGoals = no_extra_goals
+ ;
+ % In order to give better diagnostics, we handle the cases where there
+ % are zero or one modes for the called predicate specially.
+ %
ProcIds = [],
\+ check_marker(Markers, infer_modes)
->
@@ -141,7 +177,6 @@
TheProcId = ProcId,
map__lookup(Procs, ProcId, ProcInfo),
- %
% Check that `ArgsVars0' have livenesses which match the
% expected livenesses.
%
@@ -150,7 +185,6 @@
modecheck_var_list_is_live(ArgVars0, ProcArgLives0,
NeedExactMatch, ArgOffset, !ModeInfo),
- %
% Check that `ArgsVars0' have insts which match the expected
% initial insts, and set their new final insts (introducing
% extra unifications for implied modes, if necessary).
@@ -194,7 +228,6 @@
ArgVars = ArgVars0,
WaitingVars = set__list_to_set(ArgVars),
ExtraGoals = no_extra_goals,
- mode_info_get_instmap(!.ModeInfo, InstMap),
instmap__lookup_vars(ArgVars, InstMap, ArgInsts),
mode_info_set_call_arg_context(0, !ModeInfo),
mode_info_error(WaitingVars,
@@ -213,6 +246,7 @@
mode_info_set_errors(Errors, !ModeInfo)
).
+
modecheck_higher_order_call(PredOrFunc, PredVar, Args0, Args, Modes, Det,
ExtraGoals, !ModeInfo) :-
%
Index: compiler/modecheck_unify.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modecheck_unify.m,v
retrieving revision 1.92
diff -u -r1.92 modecheck_unify.m
--- compiler/modecheck_unify.m 28 Oct 2005 02:10:24 -0000 1.92
+++ compiler/modecheck_unify.m 28 Oct 2005 03:05:28 -0000
@@ -88,7 +88,95 @@
%-----------------------------------------------------------------------------%
-modecheck_unification(X, var(Y), Unification0, UnifyContext, UnifyGoalInfo0,
+ % We first have to check that if a unification occurs in a negated
+ % context with an inst any argument then it has an explicit `impure'
+ % annotation.
+ %
+ % With lambdas, the lambda itself must be marked as impure if it includes
+ % any inst any nonlocals (executing such a lambda may have the side effect
+ % of constraining a nonlocal solver variable).
+ %
+modecheck_unification(X, RHS, Unification0, UnifyContext, UnifyGoalInfo0,
+ Unify, !ModeInfo, !IO) :-
+ (
+ mode_info_get_in_negated_context(!.ModeInfo, yes),
+ (
+ RHS = var(Y),
+ Vars = [Y]
+ ;
+ RHS = functor(_, _, Vars)
+ ),
+ mode_info_get_module_info(!.ModeInfo, ModuleInfo),
+ mode_info_get_instmap(!.ModeInfo, InstMap),
+ AnyVars =
+ list__filter(var_inst_contains_any(ModuleInfo, InstMap), Vars)
+ % If this unification is in a negated context, but doesn't
+ % have an `impure' annotation, then none of the variables
+ % involved are allowed to have inst any.
+ %
+ ->
+ (
+ AnyVars = [_ | _],
+ (
+ goal_info_is_impure(UnifyGoalInfo0)
+ ->
+ modecheck_unification_2(X, RHS, Unification0, UnifyContext,
+ UnifyGoalInfo0, Unify, !ModeInfo, !IO)
+ ;
+ set__init(WaitingVars),
+ mode_info_error(WaitingVars,
+ purity_error_should_be_impure(AnyVars), !ModeInfo),
+ Unify = conj([])
+ )
+ ;
+ AnyVars = [],
+ (
+ goal_info_is_pure(UnifyGoalInfo0)
+ ->
+ modecheck_unification_2(X, RHS, Unification0, UnifyContext,
+ UnifyGoalInfo0, Unify, !ModeInfo, !IO)
+ ;
+ set__init(WaitingVars),
+ mode_info_error(WaitingVars,
+ purity_error_wrongly_impure(purity_pure), !ModeInfo),
+ Unify = conj([])
+ )
+ )
+ ;
+ mode_info_get_in_negated_context(!.ModeInfo, no),
+ \+ goal_info_is_pure(UnifyGoalInfo0)
+ ->
+ set__init(WaitingVars),
+ mode_info_error(WaitingVars,
+ purity_error_wrongly_impure(purity_pure), !ModeInfo),
+ Unify = conj([])
+ ;
+ % If this is a lambda unification containing some inst any
+ % nonlocals, then the lambda should be marked as impure.
+ %
+ RHS = lambda_goal(Purity, _, _, _, NonLocals, _, _, _, _),
+ Purity \= purity_impure,
+ mode_info_get_module_info(!.ModeInfo, ModuleInfo),
+ mode_info_get_instmap(!.ModeInfo, InstMap),
+ AnyVars = list__filter(var_inst_contains_any(ModuleInfo, InstMap),
+ NonLocals),
+ AnyVars = [_ | _]
+ ->
+ set__init(WaitingVars),
+ mode_info_error(WaitingVars,
+ purity_error_lambda_should_be_impure(AnyVars), !ModeInfo),
+ Unify = conj([])
+ ;
+ modecheck_unification_2(X, RHS, Unification0, UnifyContext,
+ UnifyGoalInfo0, Unify, !ModeInfo, !IO)
+ ).
+
+
+:- pred modecheck_unification_2(prog_var::in, unify_rhs::in, unification::in,
+ unify_context::in, hlds_goal_info::in, hlds_goal_expr::out,
+ mode_info::in, mode_info::out, io::di, io::uo) is det.
+
+modecheck_unification_2(X, var(Y), Unification0, UnifyContext, UnifyGoalInfo0,
Unify, !ModeInfo, !IO) :-
mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
mode_info_get_var_types(!.ModeInfo, VarTypes),
@@ -178,7 +266,7 @@
Unify = unify(X, var(Y), Modes, Unification, UnifyContext)
).
-modecheck_unification(X0, functor(ConsId0, IsExistConstruction, ArgVars0),
+modecheck_unification_2(X0, functor(ConsId0, IsExistConstruction, ArgVars0),
Unification0, UnifyContext, GoalInfo0, Goal, !ModeInfo, !IO) :-
mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
mode_info_get_var_types(!.ModeInfo, VarTypes0),
@@ -220,7 +308,7 @@
mode_info_set_var_types(VarTypes, !ModeInfo),
% Modecheck this unification in its new form.
- modecheck_unification(X0, Functor0, Unification0, UnifyContext,
+ modecheck_unification_2(X0, Functor0, Unification0, UnifyContext,
GoalInfo0, Goal, !ModeInfo, !IO)
;
% It's not a higher-order pred unification - just
@@ -230,7 +318,7 @@
UnifyContext, GoalInfo0, Goal, !ModeInfo, !IO)
).
-modecheck_unification(X, LambdaGoal, Unification0, UnifyContext, _GoalInfo,
+modecheck_unification_2(X, LambdaGoal, Unification0, UnifyContext, _GoalInfo,
unify(X, RHS, Mode, Unification, UnifyContext), !ModeInfo, !IO) :-
LambdaGoal = lambda_goal(Purity, PredOrFunc, EvalMethod, _,
ArgVars, Vars, Modes0, Det, Goal0),
@@ -379,7 +467,7 @@
mode_error_non_local_lambda_var(BadVar, BadInst), !ModeInfo)
;
unexpected(this_file,
- "modecheck_unification(lambda): very strange var")
+ "modecheck_unification_2(lambda): very strange var")
),
% Return any old garbage.
RHS = lambda_goal(Purity, PredOrFunc, EvalMethod, modes_are_ok,
Index: compiler/modes.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modes.m,v
retrieving revision 1.320
diff -u -r1.320 modes.m
--- compiler/modes.m 28 Oct 2005 02:10:24 -0000 1.320
+++ compiler/modes.m 28 Oct 2005 04:00:25 -0000
@@ -1358,7 +1358,10 @@
%
mode_info_lock_vars(if_then_else, NonLocals, !ModeInfo),
mode_info_add_live_vars(ThenVars, !ModeInfo),
+ mode_info_get_in_negated_context(!.ModeInfo, InNegatedContext0),
+ mode_info_set_in_negated_context(yes, !ModeInfo),
modecheck_goal(Cond0, Cond, !ModeInfo, !IO),
+ mode_info_set_in_negated_context(InNegatedContext0, !ModeInfo),
mode_info_get_instmap(!.ModeInfo, InstMapCond),
mode_info_remove_live_vars(ThenVars, !ModeInfo),
mode_info_unlock_vars(if_then_else, NonLocals, !ModeInfo),
@@ -1406,7 +1409,10 @@
% that the negation does not bind them.
%
mode_info_lock_vars(negation, NonLocals, !ModeInfo),
+ mode_info_get_in_negated_context(!.ModeInfo, InNegatedContext0),
+ mode_info_set_in_negated_context(yes, !ModeInfo),
modecheck_goal(SubGoal0, SubGoal, !ModeInfo, !IO),
+ mode_info_set_in_negated_context(InNegatedContext0, !ModeInfo),
mode_info_set_live_vars(LiveVars0, !ModeInfo),
mode_info_unlock_vars(negation, NonLocals, !ModeInfo),
mode_info_set_instmap(InstMap0, !ModeInfo),
@@ -1474,7 +1480,7 @@
mode_info_get_instmap(!.ModeInfo, InstMap0),
DeterminismKnown = no,
modecheck_call_pred(PredId, DeterminismKnown, ProcId0, ProcId,
- Args0, Args, ExtraGoals, !ModeInfo),
+ Args0, Args, GoalInfo0, ExtraGoals, !ModeInfo),
mode_info_get_module_info(!.ModeInfo, ModuleInfo),
mode_info_get_predid(!.ModeInfo, CallerPredId),
@@ -1602,7 +1608,7 @@
mode_info_set_call_context(call(call(CallId)), !ModeInfo),
ArgVars0 = list__map(foreign_arg_var, Args0),
modecheck_call_pred(PredId, DeterminismKnown, ProcId0, ProcId,
- ArgVars0, ArgVars, ExtraGoals, !ModeInfo),
+ ArgVars0, ArgVars, GoalInfo, ExtraGoals, !ModeInfo),
% zs: The assignment to Pragma looks wrong: instead of Args0,
% I think we should use Args after the following call:
@@ -2567,7 +2573,7 @@
hlds_goal_from_delayed_goal(delayed_goal(_WaitingVars, _ModeError, Goal)) =
Goal.
- % Check whether there are any delayed goals (other than headvar
+ % Check whether there are any delayed goals (other than
% unifications) at the point where we are about to schedule an impure goal.
% If so, that is an error. Headvar unifications are allowed to be delayed
% because in the case of output arguments, they cannot be scheduled
@@ -2596,7 +2602,7 @@
!ImpurityErrors, !ModeInfo, !IO),
mode_info_get_delay_info(!.ModeInfo, DelayInfo2),
delay_info__enter_conj(DelayInfo2, DelayInfo3),
- redelay_goals(HeadVarUnificationGoals, DelayInfo3, DelayInfo),
+ redelay_goals(UnificationGoals, DelayInfo3, DelayInfo),
mode_info_set_delay_info(DelayInfo, !ModeInfo),
(
NonHeadVarUnificationGoals = []
@@ -2613,7 +2619,6 @@
:- pred filter_headvar_unification_goals(list(prog_var)::in,
list(delayed_goal)::in, list(delayed_goal)::out,
- list(delayed_goal)::out) is det.
filter_headvar_unification_goals(HeadVars, DelayedGoals,
HeadVarUnificationGoals, NonHeadVarUnificationGoals) :-
Index: compiler/purity.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/purity.m,v
retrieving revision 1.81
diff -u -r1.81 purity.m
--- compiler/purity.m 28 Oct 2005 02:10:31 -0000 1.81
+++ compiler/purity.m 28 Oct 2005 04:01:06 -0000
@@ -9,6 +9,7 @@
% File: purity.m
% Authors: scachte (Peter Schachte, main author and designer of purity system)
% trd (modifications for impure functions)
+% rafe (modifications for solver goals in negated contexts)
% Purpose: handle `impure' and `promise_pure' declarations;
% finish off type checking.
%
@@ -18,6 +19,21 @@
% This includes treating procedures with different clauses for
% different modes as impure, unless promised pure.
%
+% There is a special case to do with solver type goals in negated contexts.
+% A pure goal taking solver type arguments with inst any may be used to
+% break referential transparency if it appears in a negated context. The
+% canonical example is `X < Y, not(X >= Y)' vs `not(X >= Y), X < Y' where
+% (<) and (>=) impose inequality constraints on solver variables. If X
+% and Y are initially free then the first goal ordering will succeed, but the
+% second ordering will fail. To get around this problem we require solver
+% goals in negated contexts with inst any arguments to be marked as `impure'.
+% This means that this module should not report purity warnings for calls
+% marked as impure in negated contexts when those calls are to non-impure
+% predicates or functions. Instead this aspect of purity checking must be
+% deferred until mode analysis which is when information about the insts of
+% variables is available. (Note: the above also applies to lambdas containing
+% non-local inst any variables.)
+%
% This module also calls post_typecheck.m to perform the final parts of
% type analysis, including resolution of predicate and function overloading
% (see the comments in that file).
@@ -331,12 +347,13 @@
clauses_info_varset(!.ClausesInfo, VarSet0),
RunPostTypecheck = yes,
PurityInfo0 = purity_info(ModuleInfo, RunPostTypecheck,
- !.PredInfo, VarTypes0, VarSet0, [], dont_make_implicit_promises),
+ !.PredInfo, VarTypes0, VarSet0, [], dont_make_implicit_promises,
+ no),
pred_info_get_goal_type(!.PredInfo, GoalType),
compute_purity(GoalType, Clauses0, Clauses, ProcIds,
purity_pure, Purity, PurityInfo0, PurityInfo),
PurityInfo = purity_info(_, _, !:PredInfo,
- VarTypes, VarSet, RevMessages, _),
+ VarTypes, VarSet, RevMessages, _, _),
clauses_info_set_vartypes(VarTypes, !ClausesInfo),
clauses_info_set_varset(VarSet, !ClausesInfo),
Messages = list__reverse(RevMessages),
@@ -381,9 +398,9 @@
proc_info_varset(ProcInfo0, VarSet0),
RunPostTypeCheck = no,
PurityInfo0 = purity_info(ModuleInfo, RunPostTypeCheck,
- !.PredInfo, VarTypes0, VarSet0, [], dont_make_implicit_promises),
+ !.PredInfo, VarTypes0, VarSet0, [], dont_make_implicit_promises, no),
compute_goal_purity(Goal0, Goal, Bodypurity, PurityInfo0, PurityInfo),
- PurityInfo = purity_info(_, _, !:PredInfo, VarTypes, VarSet, _, _),
+ PurityInfo = purity_info(_, _, !:PredInfo, VarTypes, VarSet, _, _, _),
proc_info_set_goal(Goal, ProcInfo0, ProcInfo1),
proc_info_set_vartypes(VarTypes, ProcInfo1, ProcInfo2),
proc_info_set_varset(VarSet, ProcInfo2, ProcInfo),
@@ -464,9 +481,8 @@
Clausepurity = purity_impure
),
worst_purity(Bodypurity0, Clausepurity) = Bodypurity,
- add_goal_info_purity_feature(Bodypurity, Info0, Info),
!:Purity = worst_purity(!.Purity, Bodypurity),
- Clause = clause(Ids, Body - Info, Lang, Context),
+ Clause = clause(Ids, Body - Info0, Lang, Context),
compute_purity(GoalType, Clauses0, Clauses, ProcIds, !Purity, !Info).
:- pred applies_to_all_modes(clause::in, list(proc_id)::in) is semidet.
@@ -637,7 +653,10 @@
% Eliminate double negation.
negate_goal(Goal0, GoalInfo0, NotGoal0),
( NotGoal0 = not(Goal1) - _GoalInfo1 ->
+ InNegatedContext0 = !.Info ^ in_negated_context,
+ !:Info = !.Info ^ in_negated_context := yes,
compute_goal_purity(Goal1, Goal, Purity, !Info),
+ !:Info = !.Info ^ in_negated_context := InNegatedContext0,
NotGoal = not(Goal)
;
compute_goal_purity(NotGoal0, NotGoal1, Purity, !Info),
@@ -675,7 +694,14 @@
).
compute_expr_purity(if_then_else(Vars, Cond0, Then0, Else0),
if_then_else(Vars, Cond, Then, Else), _, Purity, !Info) :-
+ % The condition is in a negated context.
+ %
+ InNegatedContext0 = !.Info ^ in_negated_context,
+ !:Info = !.Info ^ in_negated_context := yes,
compute_goal_purity(Cond0, Cond, Purity1, !Info),
+ !:Info = !.Info ^ in_negated_context := InNegatedContext0,
+ % The Then and Else goals are not.
+ %
compute_goal_purity(Then0, Then, Purity2, !Info),
compute_goal_purity(Else0, Else, Purity3, !Info),
worst_purity(Purity1, Purity2) = Purity12,
@@ -845,7 +871,11 @@
).
% Peform purity checking of the actual and declared purity,
- % and check that promises are consistent.
+ % and check that promises are consistent. There is one
+ % exception to this rule: an otherwise pure atomic goal must
+ % be marked as `impure' if it has an inst any argument and
+ % occurs in a negated context (see the comments at the top
+ % of this file).
%
% ActualPurity: The inferred purity of the goal
% DeclaredPurity: The declared purity of the goal
@@ -873,6 +903,14 @@
->
true
;
+ % If DeclaredPurity is impure and this is in a negated context
+ % then we have to defer this purity check until mode checking
+ % when we know whether the vars have inst any or not.
+ DeclaredPurity = purity_impure,
+ !.Info ^ in_negated_context = yes
+ ->
+ true
+ ;
% Don't require purity annotations on calls in
% compiler-generated code.
is_unify_or_compare_pred(PredInfo)
@@ -908,7 +946,14 @@
compute_goal_purity(Goal0 - GoalInfo0, Goal - GoalInfo, Purity, !Info) :-
compute_expr_purity(Goal0, Goal, GoalInfo0, Purity, !Info),
- add_goal_info_purity_feature(Purity, GoalInfo0, GoalInfo).
+ (
+ !.Info ^ in_negated_context = yes,
+ infer_goal_info_purity(GoalInfo0, purity_impure)
+ ->
+ GoalInfo = GoalInfo0
+ ;
+ add_goal_info_purity_feature(Purity, GoalInfo0, GoalInfo)
+ ).
% Compute the purity of a list of hlds_goals. Since the purity of a
% disjunction is computed the same way as the purity of a conjunction,
@@ -1240,11 +1285,15 @@
vartypes :: vartypes,
varset :: prog_varset,
messages :: post_typecheck_messages,
- implicit_purity :: implicit_purity_promise
+ implicit_purity :: implicit_purity_promise,
% If this is make_implicit_promises then
% purity annotations are optional in the
% current scope and purity warnings/errors
% should not be generated.
+ in_negated_context :: bool
+ % This is `yes' iff the current goal
+ % is in a negation or the condition
+ % of an if-then-else.
).
:- pred purity_info_add_message(post_typecheck_message::in,
Index: compiler/unique_modes.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/unique_modes.m,v
retrieving revision 1.98
diff -u -r1.98 unique_modes.m
--- compiler/unique_modes.m 28 Oct 2005 02:10:42 -0000 1.98
+++ compiler/unique_modes.m 28 Oct 2005 03:05:30 -0000
@@ -446,13 +446,13 @@
mode_checkpoint(exit, "generic_call", !ModeInfo, !IO).
check_goal_2(call(PredId, ProcId0, Args, Builtin, CallContext,
- PredName), _GoalInfo0, Goal, !ModeInfo, !IO) :-
+ PredName), GoalInfo0, Goal, !ModeInfo, !IO) :-
sym_name_to_string(PredName, PredNameString),
string__append("call ", PredNameString, CallString),
mode_checkpoint(enter, CallString, !ModeInfo, !IO),
mode_info_get_call_id(!.ModeInfo, PredId, CallId),
mode_info_set_call_context(call(call(CallId)), !ModeInfo),
- check_call(PredId, ProcId0, Args, ProcId, !ModeInfo),
+ check_call(PredId, ProcId0, Args, GoalInfo0, ProcId, !ModeInfo),
Goal = call(PredId, ProcId, Args, Builtin, CallContext, PredName),
mode_info_unset_call_context(!ModeInfo),
mode_checkpoint(exit, "call", !ModeInfo, !IO).
@@ -483,14 +483,14 @@
mode_checkpoint(exit, "switch", !ModeInfo, !IO).
check_goal_2(foreign_proc(Attributes, PredId, ProcId0, Args, ExtraArgs,
- PragmaCode), _GoalInfo, Goal, !ModeInfo, !IO) :-
+ PragmaCode), GoalInfo0, Goal, !ModeInfo, !IO) :-
% To modecheck a pragma_c_code, we just modecheck the proc for
% which it is the goal.
mode_checkpoint(enter, "foreign_proc", !ModeInfo, !IO),
mode_info_get_call_id(!.ModeInfo, PredId, CallId),
mode_info_set_call_context(call(call(CallId)), !ModeInfo),
ArgVars = list__map(foreign_arg_var, Args),
- check_call(PredId, ProcId0, ArgVars, ProcId, !ModeInfo),
+ check_call(PredId, ProcId0, ArgVars, GoalInfo0, ProcId, !ModeInfo),
Goal = foreign_proc(Attributes, PredId, ProcId, Args, ExtraArgs,
PragmaCode),
mode_info_unset_call_context(!ModeInfo),
@@ -500,10 +500,10 @@
% These should have been expanded out by now.
unexpected(this_file, "check_goal_2: unexpected shorthand").
-:- pred check_call(pred_id::in, proc_id::in, list(prog_var)::in, proc_id::out,
- mode_info::in, mode_info::out) is det.
+:- pred check_call(pred_id::in, proc_id::in, list(prog_var)::in,
+ hlds_goal_info::in, proc_id::out, mode_info::in, mode_info::out) is det.
-check_call(PredId, ProcId0, ArgVars, ProcId, !ModeInfo) :-
+check_call(PredId, ProcId0, ArgVars, GoalInfo, ProcId, !ModeInfo) :-
% Set the error list to empty for use below
% (saving the old error list and instmap in variables).
mode_info_get_errors(!.ModeInfo, OldErrors),
@@ -561,7 +561,7 @@
mode_info_set_instmap(InstMap0, !ModeInfo),
proc_info_inferred_determinism(ProcInfo, Determinism),
modecheck_call_pred(PredId, yes(Determinism), ProcId0, ProcId,
- ArgVars, NewArgVars, ExtraGoals, !ModeInfo),
+ ArgVars, NewArgVars, GoalInfo, ExtraGoals, !ModeInfo),
(
NewArgVars = ArgVars,
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.334
diff -u -r1.334 reference_manual.texi
--- doc/reference_manual.texi 20 Oct 2005 01:49:08 -0000 1.334
+++ doc/reference_manual.texi 28 Oct 2005 03:26:50 -0000
@@ -2166,7 +2166,7 @@
* Abstract solver type declarations::
* Solver type definitions::
* Implementing solver types::
-* Solver type constraints and negated contexts::
+* Solver types and negated contexts::
* Polymorphic solver types::
@end menu
@@ -2348,18 +2348,16 @@
program).
@end itemize
- at node Solver type constraints and negated contexts
- at subsection Solver type constraints and negated contexts
+ at node Solver types and negated contexts
+ at subsection Solver types and negated contexts
-It is (a currently unchecked) error to place a constraint on a solver
-type variable in a negated context. The reason for this is that the
-compiler does not understand what constraints mean and therefore it
-cannot enforce their negation outside a negated context.
-
-For this reason, soundness of a program is not guaranteed if constraints
-are placed on solver type variables inside negations or the conditions of
-if-then-else goals. Particular care is needed since unification is a primary
-form of constraint.
+Referential transparency can be violated if a non-local solver type variable
+with inst @code{any} is used in a negated context (i.e., the body of a negated
+goal or the condition of an if-then-else) or in a lambda expression. Programs
+are therefore required to place @code{impure} annotations on such goals or
+lambda expressions, even if they would normally be considered pure. This
+impurity propagates through the enclosing goal structure as specified in
+ at ref{Impurity}.
@node Polymorphic solver types
@subsection Polymorphic solver types
Index: tests/invalid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.183
diff -u -r1.183 Mmakefile
--- tests/invalid/Mmakefile 28 Oct 2005 02:11:02 -0000 1.183
+++ tests/invalid/Mmakefile 28 Oct 2005 03:05:38 -0000
@@ -38,6 +38,7 @@
any_passed_as_ground \
any_should_not_match_bound \
any_to_ground_in_ite_cond \
+ anys_in_negated_contexts \
assert_in_interface \
bad_finalise_decl \
bad_initialise_decl \
Index: tests/invalid/anys_in_negated_contexts.err_exp
===================================================================
RCS file: tests/invalid/anys_in_negated_contexts.err_exp
diff -N tests/invalid/anys_in_negated_contexts.err_exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/invalid/anys_in_negated_contexts.err_exp 28 Oct 2005 02:30:29 -0000
@@ -0,0 +1,28 @@
+anys_in_negated_contexts.m:035: In clause for `bad_if_then_else1(ia, out)':
+anys_in_negated_contexts.m:035: in call to predicate
+anys_in_negated_contexts.m:035: `anys_in_negated_contexts.ia/1':
+anys_in_negated_contexts.m:035: purity error: goal should be impure because
+anys_in_negated_contexts.m:035: it appears in a negated context, but involves
+anys_in_negated_contexts.m:035: the following variables whose insts contain
+anys_in_negated_contexts.m:035: `any': X
+anys_in_negated_contexts.m:043: In clause for `bad_if_then_else2(ia, out)':
+anys_in_negated_contexts.m:043: in call to predicate
+anys_in_negated_contexts.m:043: `anys_in_negated_contexts.ig/1':
+anys_in_negated_contexts.m:043: purity error: goal is marked as impure, but
+anys_in_negated_contexts.m:043: is actually pure
+anys_in_negated_contexts.m:056: In clause for `bad_negation1(ia)':
+anys_in_negated_contexts.m:056: in call to predicate
+anys_in_negated_contexts.m:056: `anys_in_negated_contexts.ia/1':
+anys_in_negated_contexts.m:056: purity error: goal should be impure because
+anys_in_negated_contexts.m:056: it appears in a negated context, but involves
+anys_in_negated_contexts.m:056: the following variables whose insts contain
+anys_in_negated_contexts.m:056: `any': X
+anys_in_negated_contexts.m:061: In clause for `bad_negation2(ia)':
+anys_in_negated_contexts.m:061: in call to predicate
+anys_in_negated_contexts.m:061: `anys_in_negated_contexts.ig/1':
+anys_in_negated_contexts.m:061: purity error: goal is marked as impure, but
+anys_in_negated_contexts.m:061: is actually pure
+anys_in_negated_contexts.m:082: In clause for `bad_lambda(in)':
+anys_in_negated_contexts.m:082: purity error: lambda should be impure because
+anys_in_negated_contexts.m:082: it contains the following non-local variables
+anys_in_negated_contexts.m:082: whose insts contain `any': Y
Index: tests/invalid/anys_in_negated_contexts.m
===================================================================
RCS file: tests/invalid/anys_in_negated_contexts.m
diff -N tests/invalid/anys_in_negated_contexts.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/invalid/anys_in_negated_contexts.m 28 Oct 2005 02:29:46 -0000
@@ -0,0 +1,103 @@
+%-----------------------------------------------------------------------------%
+% anys_in_negated_contexts.m
+% Ralph Becket <rafe at cs.mu.OZ.AU>
+% Wed Oct 19 18:29:50 EST 2005
+% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
+%
+%-----------------------------------------------------------------------------%
+
+:- module anys_in_negated_contexts.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module std_util.
+
+:- pred good_if_then_else(T::ia, int::out) is det.
+
+good_if_then_else(X, Y) :-
+ ( if impure ia(X), ig(3)
+ then Y = 1
+ else Y = 2
+ ).
+
+:- pred bad_if_then_else1(T::ia, int::out) is det.
+
+bad_if_then_else1(X, Y) :-
+ ( if ia(X), ig(3)
+ then Y = 1
+ else Y = 2
+ ).
+
+:- pred bad_if_then_else2(T::ia, int::out) is det.
+
+bad_if_then_else2(X, Y) :-
+ ( if impure ia(X), impure ig(3)
+ then Y = 1
+ else Y = 2
+ ).
+
+:- pred good_negation(T::ia) is semidet.
+
+good_negation(X) :-
+ not (impure ia(X), ig(3)).
+
+:- pred bad_negation1(T::ia) is semidet.
+
+bad_negation1(X) :-
+ not (ia(X), ig(3)).
+
+:- pred bad_negation2(T::ia) is semidet.
+
+bad_negation2(X) :-
+ not (impure ia(X), impure ig(3)).
+
+:- pred pure_pred_mode_specific_clauses(int).
+:- mode pure_pred_mode_specific_clauses(in) is semidet.
+:- mode pure_pred_mode_specific_clauses(out) is det.
+:- pragma promise_pure(pure_pred_mode_specific_clauses/1).
+
+pure_pred_mode_specific_clauses(42::in).
+pure_pred_mode_specific_clauses(11::out).
+
+:- impure pred good_lambda(int::in) is semidet.
+
+good_lambda(X) :-
+ oa(Y),
+ P = (impure pred(Z::in) is semidet :- Y = Z),
+ impure P(X).
+
+:- pred bad_lambda(int::in) is semidet.
+
+bad_lambda(X) :-
+ oa(Y),
+ P = (pred(Z::in) is semidet :- Y = Z),
+ P(X).
+
+:- pred ia(T::ia) is semidet.
+
+ia(_) :-
+ semidet_succeed.
+
+:- pred ig(T::in) is semidet.
+
+ig(_) :-
+ semidet_succeed.
+
+:- pred oa(int::oa) is det.
+
+oa(42).
+
+main(!IO) :-
+ io.print("Hello, World!\n", !IO).
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------
More information about the reviews
mailing list