[m-rev.] for review: fix assertion failure with promise_equivalent_solutions

[Julien Fischer]

Hi, could someone please review this; I would like to commit it today.

On Thu, 17 Jan 2008, Julien Fischer wrote:

> Estimated hours taken: 1.5
> Branches: main
>
> Fix bug #30.  The determinism analysis run as part of partial deduction
> was erroneously reporting that the head of a promise_equivalent_solutions
> scope contained extra variables, i.e. non-locals that were not further bound
> or (potentially) constrained within the scope. This violated an assertion 
> that this run of determinism checking should
> not produce any errors.
>
> The error was caused because some of the variables in the scope head that
> prior to inlining had inst any, had become ground after inlining.
> The fix is to ignore such extra variables in determinism analysis passes
> that are invoked after inlining.
>
> compiler/det_util.m:
> 	Add a field to the det_info structure that indicates whether or not 
> we
> 	should report extra variables occurring in the head of a
> 	promise_equivalent_solutions scope as an error.
>
> 	Define a new type to represent this.
>
> compiler/det_analysis.m:
> 	Check the value of the above field before reporting the
> 	presence of extra variables in a promise_equivalent_solutions scope.
>
> compiler/pd_util.m:
> compiler/det_report.m:
> compiler/simplify.m:
> 	Set the value of the det_info di_pess_extra_vars field as necessary.
>
> tests/valid/Mercury.options:
> tests/valid/Mmakefile:
> tests/valid/equiv_solns_ia.m:
> 	Regression test for the above.
>
> Julien.
>
> Index: compiler/det_analysis.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/compiler/det_analysis.m,v
> retrieving revision 1.210
> diff -u -r1.210 det_analysis.m
> --- compiler/det_analysis.m	30 Dec 2007 08:23:36 -0000	1.210
> +++ compiler/det_analysis.m	17 Jan 2008 05:40:27 -0000
> @@ -284,7 +284,8 @@
>     proc_info_get_goal(Proc0, Goal0),
>     proc_info_get_initial_instmap(Proc0, !.ModuleInfo, InstMap0),
>     proc_info_get_vartypes(Proc0, VarTypes),
> -    det_info_init(!.ModuleInfo, VarTypes, PredId, ProcId, DetInfo0),
> +    det_info_init(!.ModuleInfo, VarTypes, PredId, ProcId,
> +        pess_extra_vars_report, DetInfo0),
>     det_infer_goal(Goal0, Goal, InstMap0, SolnContext, [], no,
>         InferDetism, _,  DetInfo0, DetInfo, [], !:Specs),
>     det_info_get_module_info(DetInfo, !:ModuleInfo),
> @@ -1490,7 +1491,12 @@
>         % Which vars were listed in the promise_equivalent_solutions
>         % but not bound inside the scope?
>         set.difference(set.list_to_set(Vars), BoundVars, ExtraVars),
> -        ( set.empty(ExtraVars) ->
> +        det_info_get_pess_extra_vars(!.DetInfo, IgnoreExtraVars),
> +        ( +            ( set.empty(ExtraVars)
> +            ; IgnoreExtraVars = pess_extra_vars_ignore
> +            )
> +        ->
>             true
>         ;
>             ExtraVarNames = list.map(lookup_var_name_in_varset(VarSet),
> Index: compiler/det_report.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/compiler/det_report.m,v
> retrieving revision 1.141
> diff -u -r1.141 det_report.m
> --- compiler/det_report.m	30 Dec 2007 08:23:36 -0000	1.141
> +++ compiler/det_report.m	17 Jan 2008 05:40:27 -0000
> @@ -255,7 +255,8 @@
>             proc_info_get_goal(ProcInfo0, Goal),
>             proc_info_get_vartypes(ProcInfo0, VarTypes),
>             proc_info_get_initial_instmap(ProcInfo0, !.ModuleInfo, 
> InstMap0),
> -            det_info_init(!.ModuleInfo, VarTypes, PredId, ProcId, DetInfo0),
> +            det_info_init(!.ModuleInfo, VarTypes, PredId, ProcId, + 
> pess_extra_vars_report, DetInfo0),
>             det_diagnose_goal(Goal, InstMap0, DeclaredDetism, [],
>                 DetInfo0, DetInfo, GoalMsgs0),
>             det_info_get_module_info(DetInfo, !:ModuleInfo),
> Index: compiler/det_util.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/compiler/det_util.m,v
> retrieving revision 1.45
> diff -u -r1.45 det_util.m
> --- compiler/det_util.m	30 Dec 2007 08:23:36 -0000	1.45
> +++ compiler/det_util.m	17 Jan 2008 05:40:27 -0000
> @@ -37,6 +37,26 @@
>     --->    changed
>     ;       unchanged.
>
> +    % Should we emit an error message about extra variables in the head
> +    % of a promise_equivalent_solutions scope?  Extra variables are
> +    % those non-locals that are not further bound or (potentially) 
> constrained
> +    % by the goal inside the scope.
> +    %
> +    % We ignore such extra variables when re-running determinism
> +    % analysis after optimisations such as inlining have been performed
> +    % because not doing so results in spurious error messages.
> +    % (Inlining can cause variables that had inst any to become ground.)
> +    %
> +:- type report_pess_extra_vars
> +    --->    pess_extra_vars_report
> +            % Emit an error message if the head of a
> +            % promise_equivalent_solutions scope contains variables that
> +            % are not further bound or (potentially) further constrained
> +            % by the goal inside the scope.
> +
> +    ;       pess_extra_vars_ignore.
> +            % Do not emit an error message if the above occurs.
> +
> :- type det_info.
>
>     % Given a list of cases, and a list of the possible cons_ids
> @@ -66,7 +86,7 @@
>     det_info::in) is semidet.
>
> :- pred det_info_init(module_info::in, vartypes::in, pred_id::in, 
> proc_id::in,
> -    det_info::out) is det.
> +    report_pess_extra_vars::in, det_info::out) is det.
>
> :- pred det_info_get_module_info(det_info::in, module_info::out) is det.
> :- pred det_info_get_pred_id(det_info::in, pred_id::out) is det.
> @@ -75,6 +95,8 @@
> :- pred det_info_get_reorder_disj(det_info::in, bool::out) is det.
> :- pred det_info_get_fully_strict(det_info::in, bool::out) is det.
> :- pred det_info_get_vartypes(det_info::in, vartypes::out) is det.
> +:- pred det_info_get_pess_extra_vars(det_info::in,
> +    report_pess_extra_vars::out) is det.
>
> :- pred det_info_set_module_info(module_info::in, det_info::in, 
> det_info::out)
>     is det.
> @@ -184,16 +206,18 @@
>                 di_proc_id         :: proc_id,     % currently processed
>                 di_reorder_conj    :: bool,        % --reorder-conj
>                 di_reorder_disj    :: bool,        % --reorder-disj
> -                di_fully_strict    :: bool         % --fully-strict
> +                di_fully_strict    :: bool,        % --fully-strict
> +                di_pess_extra_vars :: report_pess_extra_vars
>             ).
>
> -det_info_init(ModuleInfo, VarTypes, PredId, ProcId, DetInfo) :-
> +det_info_init(ModuleInfo, VarTypes, PredId, ProcId, PessExtraVars,
> +        DetInfo) :-
>     module_info_get_globals(ModuleInfo, Globals),
>     globals.lookup_bool_option(Globals, reorder_conj, ReorderConj),
>     globals.lookup_bool_option(Globals, reorder_disj, ReorderDisj),
>     globals.lookup_bool_option(Globals, fully_strict, FullyStrict),
>     DetInfo = det_info(ModuleInfo, VarTypes, PredId, ProcId,
> -        ReorderConj, ReorderDisj, FullyStrict).
> +        ReorderConj, ReorderDisj, FullyStrict, PessExtraVars).
>
> det_info_get_module_info(DI, DI ^ di_module_info).
> det_info_get_pred_id(DI, DI ^ di_pred_id).
> @@ -202,6 +226,7 @@
> det_info_get_reorder_disj(DI, DI ^ di_reorder_disj).
> det_info_get_fully_strict(DI, DI ^ di_fully_strict).
> det_info_get_vartypes(DI, DI ^ di_vartypes).
> +det_info_get_pess_extra_vars(DI, DI ^ di_pess_extra_vars).
>
> det_info_set_module_info(ModuleInfo, DI, DI ^ di_module_info := ModuleInfo).
> det_info_set_vartypes(VarTypes, DI, DI ^ di_vartypes := VarTypes).
> Index: compiler/pd_util.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/compiler/pd_util.m,v
> retrieving revision 1.65
> diff -u -r1.65 pd_util.m
> --- compiler/pd_util.m	30 Dec 2007 08:23:53 -0000	1.65
> +++ compiler/pd_util.m	17 Jan 2008 05:40:27 -0000
> @@ -244,7 +244,8 @@
>     pd_info_get_module_info(!.PDInfo, ModuleInfo0),
>     pd_info_get_pred_proc_id(!.PDInfo, proc(PredId, ProcId)),
>     proc_info_get_vartypes(ProcInfo0, VarTypes0),
> -    det_info_init(ModuleInfo0, VarTypes0, PredId, ProcId, DetInfo0),
> +    det_info_init(ModuleInfo0, VarTypes0, PredId, ProcId, + 
> pess_extra_vars_ignore, DetInfo0),
>     pd_info_get_instmap(!.PDInfo, InstMap0),
>     pd_info_get_proc_info(!.PDInfo, ProcInfo0),
>     simplify_info_init(DetInfo0, Simplifications, InstMap0, ProcInfo0,
> @@ -374,7 +375,8 @@
>         ModuleInfo0, ModuleInfo1),
>
>     proc_info_get_vartypes(ProcInfo, VarTypes),
> -    det_info_init(ModuleInfo1, VarTypes, PredId, ProcId, DetInfo0),
> +    det_info_init(ModuleInfo1, VarTypes, PredId, ProcId,
> +        pess_extra_vars_ignore, DetInfo0),
>     pd_info_get_instmap(!.PDInfo, InstMap),
>     det_infer_goal(Goal0, Goal, InstMap, SolnContext, [], no, _, _,
>         DetInfo0, DetInfo, [], Specs),
> Index: compiler/simplify.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/compiler/simplify.m,v
> retrieving revision 1.222
> diff -u -r1.222 simplify.m
> --- compiler/simplify.m	30 Dec 2007 08:23:56 -0000	1.222
> +++ compiler/simplify.m	17 Jan 2008 05:40:28 -0000
> @@ -380,7 +380,8 @@
>     ;
>         Simplifications = Simplifications0
>     ),
> -    det_info_init(!.ModuleInfo, VarTypes0, PredId, ProcId, DetInfo0),
> +    det_info_init(!.ModuleInfo, VarTypes0, PredId, ProcId,
> +        pess_extra_vars_report, DetInfo0),
>     proc_info_get_initial_instmap(!.ProcInfo, !.ModuleInfo, InstMap0),
>     simplify_info_init(DetInfo0, Simplifications, InstMap0, !.ProcInfo, 
> Info0),
>     proc_info_get_goal(!.ProcInfo, Goal0),
> Index: tests/valid/Mercury.options
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/tests/valid/Mercury.options,v
> retrieving revision 1.42
> diff -u -r1.42 Mercury.options
> --- tests/valid/Mercury.options	3 Dec 2007 09:52:14 -0000	1.42
> +++ tests/valid/Mercury.options	17 Jan 2008 05:40:28 -0000
> @@ -35,6 +35,7 @@
> MCFLAGS-deforest_loop		= -O3 --intermodule-optimization
> MCFLAGS-deforest_rerun_det	= -O3 --check-termination
> MCFLAGS-double_vn		= -O4
> +MCFLAGS-equiv_solns_ia		= --inlining --local-constraint-propagation
> MCFLAGS-exists_cast_bug		= --trace rep -O0 
> --optimize-saved-vars-const
> MCFLAGS-explicit_quant		= --halt-at-warn
> MCFLAGS-func_class		= --no-warn-nothing-exported
> Index: tests/valid/Mmakefile
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/tests/valid/Mmakefile,v
> retrieving revision 1.203
> diff -u -r1.203 Mmakefile
> --- tests/valid/Mmakefile	3 Dec 2007 09:52:14 -0000	1.203
> +++ tests/valid/Mmakefile	17 Jan 2008 05:40:28 -0000
> @@ -85,6 +85,7 @@
> 	empty_switch \
> 	erl_ite_vars \
> 	error \
> +	equiv_solns_ia \
> 	eval \
> 	existential_cons \
> 	explicit_quant \
> Index: tests/valid/equiv_solns_ia.m
> ===================================================================
> RCS file: tests/valid/equiv_solns_ia.m
> diff -N tests/valid/equiv_solns_ia.m
> --- /dev/null	1 Jan 1970 00:00:00 -0000
> +++ tests/valid/equiv_solns_ia.m	17 Jan 2008 05:40:28 -0000
> @@ -0,0 +1,65 @@
> +% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
> +%
> +% rotd-2007-11-27 emits the following error message for this program:
> +%
> +% equiv_solns_ia.m:051: Error: the `promise_equivalent_solutions' goal lists
> +% equiv_solns_ia.m:051:   some extra variables: V_3, V_4 and V_5.
> +% Uncaught Mercury exception:
> +% Software Error: pd_util.m: Unexpected: rerun_det_analysis: determinism 
> errors
> +%
> +% Compile with: -C -O0 --inlining --local-constraint-propagation
> +%
> +% The problem was caused by the fact that inst any non-locals in a promise
> +% equivalent_solutions scope must be listed in the scope head but 
> optimizations
> +% such as inlining can cause the inst of these non-locals to become ground.
> +% Since only variables that become further bound/constrained should be 
> listed
> +% in the scope head this means that determinism analysis reruns after
> +% inlining reported extra variables in the scope head.
> +% +:- module equiv_solns_ia.
> +:- interface.
> +
> +:- import_module list.
> +
> +:- typeclass flatzinc_solver(Solver, Var) <= (Solver -> Var) where [
> +
> +    pred solve_for_vars(Solver::in, solve_spec(Var)::ia,
> +        solver_annotations(Var)::ia, list(Var)::ia) is nondet
> +].
> +
> +:- type solve_spec(Var)
> +    --->    satisfy
> +    ;       minimize(Var)
> +    ;       maximize(Var).
> +
> +:- type solver_annotations(Var) == list(solver_annotation(Var)).
> +
> +:- type solver_annotation(Var)
> +    --->    solver_annotation(list(Var)).
> +
> +:- type env(Var) == list({int, Var}).
> +
> +:- implementation.
> +:- import_module exception.
> +
> +:- pred interpret(Solver::in) is det <= flatzinc_solver(Solver, Var).
> +
> +interpret(Solver) :-
> +    interpret_2(Solver, satisfy, [], []).
> +
> +:- pragma inline(interpret_2/4).
> +:- pred interpret_2(Solver::in, solve_spec(Var)::ia,
> +    solver_annotations(Var)::ia,
> +    list(Var)::ia) is det <= flatzinc_solver(Solver, Var).
> +
> +interpret_2(Solver, SolveSpec, SolverAnns, AllVars) :-
> +    promise_pure
> +    ( if
> +        promise_equivalent_solutions [SolveSpec, SolverAnns, AllVars] (
> +            solve_for_vars(Solver, SolveSpec, SolverAnns, AllVars)
> +        )
> +      then
> +        true
> +      else
> +        throw("")
> +    ).
>
> --------------------------------------------------------------------------
> mercury-reviews mailing list
> Post messages to:       mercury-reviews at csse.unimelb.edu.au
> Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
> Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
> --------------------------------------------------------------------------
>
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------