[m-rev.] for review: fix a bug reportd by Peter Hawkins

[Julien Fischer]

On Tue, 11 Jul 2006, Zoltan Somogyi wrote:

> Fix a bug reported by Peter Hawkins. The bug was that an predicate without
> a declared determinism but whose inferred determinism was invalid for its
> tabling declaration led to a compiler abort.
>
> compiler/det_analysis.m:
> 	Fix the main cause of the bug, which was that the check for the
> 	compatibility of evaluation method and determinism was performed
> 	only for predicates with declared determinisms, not those without.
>
> 	Centralize the printing of determinism error messages, and sort
> 	the messages first.
>
> compiler/hlds_pred.m:
> 	Fix the other half of the bug: the predicate that checked the
> 	compatibility of evaluation method and determinism was too liberal
> 	with minimal model predicates, letting through determinisms that the
> 	tabling transformation cannot (yet) support.
>

...

> Index: compiler/hlds_pred.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/compiler/hlds_pred.m,v
> retrieving revision 1.199
> diff -u -r1.199 hlds_pred.m
> --- compiler/hlds_pred.m	15 Jun 2006 19:36:59 -0000	1.199
> +++ compiler/hlds_pred.m	7 Jul 2006 06:02:17 -0000

...

> @@ -2848,17 +2848,55 @@
>     unexpected(this_file,
>         "valid_determinism_for_eval_method called after tabling phase").
> valid_determinism_for_eval_method(eval_minimal(_), Detism) = Valid :-

I suggest adding sentence here like:

 	The following reasons specify why a particular determinism is
 	incompatible with minimal model tabling.

> +    % Reason 1:
>     % Determinism analysis isn't yet smart enough to know whether
> -    % a cannot_fail execution path is guaranteed not to go through
> -    % a call to a predicate that is mutually recursive with this one,
> -    % which (if this predicate is minimal model) is the only way that
> -    % the predicate can be properly cannot_fail. The problem is that in
> -    % in general, the mutually recursive predicate may be in another
> -    % module.
> -    determinism_components(Detism, CanFail, _),
> -    ( CanFail = can_fail ->
> +    % a cannot_fail execution path is guaranteed not to go through a call
> +    % to a predicate that is mutually recursive with this one, which (if this
> +    % predicate is minimal model) is the only way that the predicate can be
> +    % properly cannot_fail. The problem is that in in general, the mutually
> +    % recursive predicate may be in another module.
> +    %
> +    % Reason 2:
> +    % The transformation, as currently implemented, assumes that it is possible
> +    % to reach the call table tip, and generates HLDS that refers to the
> +    % introduced variable representing this tip. This variable however, will
> +    % be optimized away if the code cannot succeed, causing a code generator
> +    % abort.
> +    %
> +    % Reason 3:
> +    % Minimal model semantics requires computing to a fixpoint, and this is
> +    % incompatible with the notion of Committed choice.
> +    %
> +    % Reason 4:
> +    % Doing the analysis required to ensure that a predicate can't have more
> +    % than one solution is much harder if the predicate concerned is
> +    % minimal_model. In theory, this analysis could be done, but it would
> +    % take a lot of programming, and since there is a simple workaround
> +    % make the predicate nondet, and check the number of solutions at the
> +    % caller), this would not be cost-effective.
> +    (
> +        Detism = detism_det,
> +        Valid = no                  % Reason 1
> +    ;
> +        Detism = detism_semi,
> +        Valid = no                  % Reason 4
> +    ;
> +        Detism = detism_multi,      % Reason 1
> +        Valid = yes
> +    ;
> +        Detism = detism_non,
>         Valid = yes
>     ;
> +        Detism = detism_cc_multi,   % Reason 3
> +        Valid = no
> +    ;
> +        Detism = detism_cc_non,     % Reason 3
> +        Valid = no
> +    ;
> +        Detism = detism_erroneous,  % Reason 2
> +        Valid = no
> +    ;
> +        Detism = detism_failure,    % Reason 2
>         Valid = no
>     ).

...

> Index: tests/invalid/hawkins_mm_fail_reset.err_exp
> ===================================================================
> RCS file: tests/invalid/hawkins_mm_fail_reset.err_exp
> diff -N tests/invalid/hawkins_mm_fail_reset.err_exp
> --- /dev/null	1 Jan 1970 00:00:00 -0000
> +++ tests/invalid/hawkins_mm_fail_reset.err_exp	8 Jul 2006 07:27:05 -0000
> @@ -0,0 +1,13 @@
> +hawkins_mm_fail_reset.m:027: Error: `pragma memo' declaration not allowed for
> +hawkins_mm_fail_reset.m:027:   procedure with determinism `failure'.
> +hawkins_mm_fail_reset.m:036: Error: `pragma memo' declaration not allowed for

The pragmas in the test case are minimal_model not memo pragmas.  The
error message ought to distinguish between the two of them.

> +hawkins_mm_fail_reset.m:036:   procedure with determinism `failure'.
> +hawkins_mm_fail_reset.m:020: In `entry(out)':
> +hawkins_mm_fail_reset.m:020:   warning: determinism declaration could be
> +hawkins_mm_fail_reset.m:020:   tighter.
> +hawkins_mm_fail_reset.m:020:   Declared `nondet', inferred `failure'.
> +hawkins_mm_fail_reset.m:030: Warning: this disjunct will never have any
> +hawkins_mm_fail_reset.m:030:   solutions.
> +hawkins_mm_fail_reset.m:033: Warning: this disjunct will never have any
> +hawkins_mm_fail_reset.m:033:   solutions.
> +For more information, recompile with `-E'.
> Index: tests/invalid/hawkins_mm_fail_reset.m
> ===================================================================
> RCS file: tests/invalid/hawkins_mm_fail_reset.m
> diff -N tests/invalid/hawkins_mm_fail_reset.m
> --- /dev/null	1 Jan 1970 00:00:00 -0000
> +++ tests/invalid/hawkins_mm_fail_reset.m	7 Jul 2006 04:48:05 -0000
> @@ -0,0 +1,40 @@
> +% $ mmc --make foo --grade reg.mmsc.gc --no-warn-singleton-variables
> +% Making Mercury/int3s/foo.int3
> +% Making Mercury/cs/foo.c
> +% Uncaught Mercury exception:
> +% Software Error: map.lookup: key not found
> +%          Key Type: term.var(parse_tree.prog_data.prog_var_type)
> +%          Key Value: var(5)
> +%          Value Type: ll_backend.var_locn.var_state
> +% Stack dump not available in this grade.
> +% foo.m:003: In `entry(out)':
> +% foo.m:003:   warning: determinism declaration could be tighter.
> +% foo.m:003:   Declared `nondet', inferred `failure'.
> +% foo.m:014: Warning: this disjunct will never have any solutions.
> +% foo.m:017: Warning: this disjunct will never have any solutions.
> +% ** Error making `Mercury/cs/foo.c'.
> +
> +:- module hawkins_mm_fail_reset.
> +:- interface.
> +
> +:- pred entry(int::out) is nondet.
> +
> +:- implementation.
> +:- import_module int.
> +
> +entry(0) :- pred1(_).
> +
> +:- pred pred1(int::out).
> +:- pragma minimal_model(pred1/1, [allow_reset]).
> +
> +pred1(2) :-
> +	pred2(_P).
> +
> +pred1(1) :-
> +	pred2(_P).
> +
> +:- pred pred2(int::out).
> +:- pragma minimal_model(pred2/1, [allow_reset]).
> +
> +pred2(_) :-
> +	fail.

> Index: tests/invalid/loopcheck.err_exp
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/tests/invalid/loopcheck.err_exp,v
> retrieving revision 1.3
> diff -u -r1.3 loopcheck.err_exp
> --- tests/invalid/loopcheck.err_exp	14 Jun 2006 08:14:54 -0000	1.3
> +++ tests/invalid/loopcheck.err_exp	8 Jul 2006 09:03:48 -0000
> @@ -4,8 +4,8 @@
> loopcheck.m:016: Error: `pragma loop_check' declaration not allowed for
> loopcheck.m:016:   procedure with determinism `erroneous'.
> loopcheck.m:016:   The pragma requested is only valid for the following
> -loopcheck.m:016:   determinism(s): det, semidet, nondet, multi, cc_nondet and
> -loopcheck.m:016:   cc_multi
> +loopcheck.m:016:   determinism(s): cc_multi, cc_nondet, det, multi, nondet and
> +loopcheck.m:016:   semidet.

s/determinism(s)/determinisms/ there.

The rest of that looks fine.

Julien.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at csse.unimelb.edu.au
administrative address: owner-mercury-reviews at csse.unimelb.edu.au
unsubscribe: Address: mercury-reviews-request at csse.unimelb.edu.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at csse.unimelb.edu.au Message: subscribe
--------------------------------------------------------------------------