for review: make HLDS mostly well-moded

[Fergus Henderson]

On 11-Feb-1998, Simon Taylor <stayl at cs.mu.OZ.AU> wrote:
> Hi Fergus,
> 
> > On 09-Feb-1998, Simon Taylor <stayl at cs.mu.OZ.AU> wrote:
> > > compiler/unique_modes.m
> > > compiler/hlds_pred.m
> > > 	Added proc_info_inferred_never_succeeds, which checks whether
> > > 	the procedure never succeeds according to the inferred determinism.
> > > 	Use it during unique_mode analysis instead of proc_info_never_succeeds,
> > > 	which uses the declared determinism.
> > 
> > Why?
> > 
> > This changes which programs are considered legal programs.
> > Some programs that would previously have been mode-incorrect will become
> > mode-correct.  At very least some rationale is needed.
> 
> tests/valid/same_length_2 is the test case which prompted this change.
> proc_info_never_succeeds only uses the declared determinism, since the
> inferred determinism may not be available. 
> 
> The code that causes the problem is 
> p2(X) :-
> 	r(X::my_output_list_skel),
> 	q(X::my_list_skel_output)	
> 	;
> 	r(X::my_output_list_skel),
> 	q(X::my_list_skel_output).
> 
> Both r/1 and q/1 do not have determinism declarations. r/1
> is inferred to be erroneous. proc_info_never_succeeds looks at
> the declared determinism. Since there is none, it assumes that 
> r/1 can succeed. Since determinism analysis fills in the correct
> determinism, simplify.m prunes away the call to q/1 since it
> will be never reached. This means that the elements of the list X
> are never bound, and unique modes reports an error.

>From a language design perspective, it is arguably inconsistent
for unique mode checking to take inferred cannot_succeed information
into account but for ordinary mode checking to not do so.
The fact that the compiler fails on the above example indicates
a bug in the compiler, but not necessarily a flaw in the language design.

If we assume that the current language design should remain unchanged,
then the bug in the compiler is that simplify.m does not preserve
mode-correctness; that, in combination with your change to rerun
mode analysis, causes the bug.

A possible fix to this bug would be to have simplify.m insert `fail'
(i.e. the empty disjunction `disj([])') to replace the code it
prunes away.  This would ensure that the code remains mode-correct.
It would also still be determinism-correct, because determinism
correctness takes cannot_succeed information from inferred determinisms
into account.  I think the generated code would still be the same,
because code generation won't generate anything for unreachable code.

I'm still open to debate about changing the definition of mode-correctness,
but we shouldn't do so simply because of a compiler bug.

> > > compiler/special_pred.m
> > > library/mercury_builtin.m
> > > 	Make the uniqueness of the comparison_result argument
> > > 	of builtin_compare_* and the automatically generated
> > > 	comparison procedures match that of compare/3. Unique mode 
> > > 	errors will still be introduced if any of the unique modes
> > > 	of compare/3 are used.
> > 
> > Could you explain this in a bit more detail?
> 
> compare/3 has four modes: compare(uo, in, in), compare(uo, in, ui),
> 	compare(uo, ui, in), compare(uo, ui, ui).	
> 
> The automatically generated unification procedures implement
> only the first of these modes. If one of the other modes of
> compare/3 is used and an input argument is required to be
> unique after the call, a unique mode error will result if
> the code is modechecked after the call to compare/3 is replaced 
> by a call to the compiler-generated procedure.

OK, now I understand what you're talking about.  Thanks.

I think you should include a complete fix for this before
checking in any code that would cause mode checking to be
rerun (i.e. which could cause the compiler to report spurious
errors).

A possible fix would be to change polymorphism.m to only perform the
specialization for calls to compare/3 in the `uo, in, in' mode.

But the change you have done so far is fine for now.
I have suggested a small modification to the log message below.

> > > tests/valid/unreachable_code.m
> > > 	Add a test case for a bogus higher-order unification
> > > 	mode error in unreachable code.
> > 
> > Hmm, there were several things described as "bug fixes" in the log message --
> > does this test case test for all of them?  I'd like to see a regression
> > test for each bug you fixed, if possible.
> 
> The bugs fixed were found by compiling existing test cases with 
> --deforestation. Test cases for these bugs are a little hard to 
> generate, since most unreachable code is removed before the unique 
> modes - something like deforestation producing unreachable code
> is required. The bug in the ordering of the modes of introduced
> lambda predicates can only be detected by running mode analysis
> after simplification. Do you want me to add an option to do that?

Well, eventually I'd like you to commit the `--deforestation' option,
although it would be best to make that a separate change.
For this change, it would be helpful to say for each bug fix
"this bug caused tests/foo/bar.m to fail when compiled with the
(not-yet-committed) `--deforestation' option".

The reason for describing the test case is so that if your fix turns
out to be buggy or for any other reason needs to be changed,
then whoever changes your fix can ensure that their change
doesn't reintroduce the bug that you fixed.

> > Oh, you will have a problem with the following optimization
> > in modecheck_unify.m:
> 
> > 		% This optimisation is safe because the only way that
> > 		% we can analyse a unification as having no solutions
> > 		% is that the unification always fails.
> > 		%
> > 		% Unifying two preds is not erroneous as far as the
> > 		% mode checker is concerned, but a mode _error_.
> > 		map__init(Empty),
> > 		Goal = disj([], Empty)
> > 	;
> > 
> > The problem is that by rerunning mode analysis after inlining
> > you have violated the assumption documented there (the one starting
> > with "This optimisation is safe because ...").
> > This optimization might do the wrong thing in the case
> > of user-defined equality predicates, e.g. optimizing away
> > a call to error/1.
> 
> Won't unifications involving user-defined equality predicates have
> been transformed into calls by polymorphism.m?

Hmm...

Actually this code is in modecheck_unify_functor, so the unification
can never be one that involves a call to a user-defined equality predicate.
Only var-var unifications can call user-defined equality predicates.

So there won't be any problem.

> compiler/modecheck_unify.m
> 	Avoid some aborts and mode errors when rerunning mode analysis,
> 	especially those resulting from not_reached insts being treated
> 	as bound.

Please add

	These errors caused tests/FOO/BAR.m to fail when compiled with
	the (not-yet-committed) `--deforestation' option.

for some appropriate value of FOO/BAR.

> compiler/unique_modes.m
> compiler/hlds_pred.m
> 	Added proc_info_inferred_never_succeeds, which checks whether
> 	the procedure never succeeds according to the inferred determinism.
> 	Use it during unique_mode analysis instead of proc_info_never_succeeds,
> 	which uses the declared determinism. This is necessary if an 
> 	optimization removes code after a call to a procedure which is 
> 	declared to succeed but which is inferred to never succeed.

As I said above, I think it might be better to fix simplify.m
rather than changing unique_modes.m.

The log message should include

	...
	The old code caused tests/FOO/BAR.m to fail when compiled with
	the (not-yet-committed) `--deforestation' option.

for some appropriate value of FOO/BAR.

> compiler/mode_util.m
> 	Fix a bug in recompute_instmap_delta_call to do with unreachable
> 	instmaps.

	...
	This bug caused tests/FOO/BAR.m to fail when compiled with
	the (not-yet-committed) `--deforestation' option.

> compiler/special_pred.m
> library/mercury_builtin.m
> 	Make the uniqueness of the comparison_result argument
> 	of builtin_compare_* and the automatically generated
> 	comparison procedures match that of compare/3. Unique mode 
> 	errors will still be introduced if any of the unique modes
> 	of compare/3 are used, since the compiler-generated comparison
> 	procedures only implement the (uo, in, in) mode.

I suggest you change that log message to

 	... Unique mode 
 	errors will still be introduced if polymorphism.m specializes
	calls to any of the unique modes of compare/3 are used,
	and then mode analysis is rerun, since the compiler-generated
	comparison procedures only implement the (uo, in, in) mode.
	(This is not yet a problem because currently we don't rerun
	mode analysis.)

> --- mercury_ho_call.c	1998/02/10 12:02:15	1.1
> +++ mercury_ho_call.c	1998/02/10 12:18:45
...
> -	if (num_in_args < 3) {
> +	if (num_in_args < MR_HO_CALL_INPUTS) {
>  		for (i = 1; i <= num_extra_args; i++) {
> -			virtual_reg(i+num_in_args) = virtual_reg(i+3);
> +			virtual_reg(i+num_in_args) =
> +				virtual_reg(i+MR_HO_CALL_INPUTS);
>  		}
> -	} else if (num_in_args > 3) {
> +	} else if (num_in_args > MR_HO_CALL_INPUTS) {
>  		for (i = num_extra_args; i>0; i--) {
> -			virtual_reg(i+num_in_args) = virtual_reg(i+3);
> +			virtual_reg(i+num_in_args) =
> +				virtual_reg(i+MR_HO_CALL_INPUTS);
>  		}
> -	} /* else do nothing because i == 3 */
> +	} /* else do nothing because i == MR_HO_CALL_INPUTS */

Thanks for those stylistic improvements -- while you're at it,
I suggest s/+/ + /

Apart from the changes to compiler/unique_modes.m and
compiler/hlds_pred.m, and the log message, it looks fine.  If you just
add those bits I suggested to the log message, then I would be quite
happy for you to commit all the parts of your changes except the
addition of proc_info_inferred_never_succeeds to hlds_pred.m and a call
to it in unique_modes.m.

Cheers,
	Fergus.

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