[m-rev.] for review: new termination analyser (part 5 of 6)

[Julien Fischer]

On Sat, 2 Apr 2005, Mark Brown wrote:

> On 24-Mar-2005, Julien Fischer <juliensf at cs.mu.OZ.AU> wrote:
> >
> > +%-----------------------------------------------------------------------------%
> > Index: compiler/term_constr_errors.m
> > ===================================================================
> > RCS file: compiler/term_constr_errors.m
> > diff -N compiler/term_constr_errors.m
> > --- /dev/null	1 Jan 1970 00:00:00 -0000
> > +++ compiler/term_constr_errors.m	9 Mar 2005 03:43:17 -0000
> > +%-----------------------------------------------------------------------------%
> > +%
> > +% Termination 2 Errors
> > +%
> > +
> > +% The termination errors are all in reference to possible non-termination.
> > +% While it is possible for pass 1 to go amiss the worst that will happen
> > +% (barring an abnormal abort) is that the size of the arguments will be
> > +% unconstrained.
> > +
> > +:- type termination2_error
> > +	--->		imported_pred
> > +				% Termination could not be proved because
> > +				% it depends upon information from another
> > +				% module and that information is not
> > +				% available.
> > +
> > +	;		can_loop_proc_called(pred_proc_id, pred_proc_id)
> > +				% Termination could not be proved because
> > +				% the procedure called another procedure
> > +				% that may not terminate.
> > +
> > +	;		cond_not_satisfied
> > +				% Termination could not be proved because
> > +				% no set of decreasing argument could e found.
>
> s/could e/could be/
>
Fixed.


> > Index: compiler/term_constr_fixpoint.m
> > ===================================================================
> > RCS file: compiler/term_constr_fixpoint.m
> > diff -N compiler/term_constr_fixpoint.m
> > --- /dev/null	1 Jan 1970 00:00:00 -0000
> > +++ compiler/term_constr_fixpoint.m	24 Mar 2005 04:20:56 -0000
> > +%-----------------------------------------------------------------------------%
> > +
> > +    % Calculate the next approximation to the argument size constraints.
> > +    %
> > +    % ChangeFlag is `yes' if the constraints for any procedure in the SCC
> > +    % have changed since the previous iteration.
> > +    %
> > +:- pred do_fixpoint_calculation(fixpoint_options::in, list(pred_proc_id)::in,
> > +    int::in, term2_errors::out, module_info::in, module_info::out,
> > +    io::di, io::uo) is det.
>
> The comment isn't right, since this predicate does the full calculation
> rather than just one iteration, and also there is no ChangeFlag.
>
That comment was out of date.  I've changed it to:

	% Derive the argument size constraints for the procedures in
	% this SCC.


> > +:- func fixpoint_options_init(widening, int) = fixpoint_options.
>
> The arguments to this function should be documented.
>
Done.


> > +%------------------------------------------------------------------------------%
> > +%
> > +% Perform a fixpoint iteration on the AR.
>
> This does the full calculation, right?  The next section of code does
> an iteration.
>
Yes it does the full calculation.  I've fixed the section heading here.

> > +        %
> > +        % Look up the constraints obtained during the previous
> > +        % iteration.
> > +        %
> > +        ArgSizeInfo = lookup_proc_constr_arg_size_info(ModuleInfo, PPId),
> > +        %
> > +        % NOTE: `!.Polyhedron' is the set of constraints obtained by
> > +        % *this* iteration.  `OldPolyhedron' is the set of constraints
> > +        % obtained by the *previous* iteration -- which may in fact
> > +        % be `empty' (false).
> > +        %
> > +        (
> > +            % If there were no constraints for the procedure then
> > +            % we are at the beginning of the analysis.
> > +            %
> > +            ArgSizeInfo = no,
> > +            OldPolyhedron = polyhedron.empty
> > +        ;
> > +            ArgSizeInfo = yes(SizeInfo),
> > +            SizeInfo = OldPolyhedron
>
> That would be easier to understand if OldPolyhedron was on the left.
>
Done.

> > +                %
> > +                % Set any zero_vars in the constraints
> > +                % to zero (ie. delete the terms).  We need
> > +                % to do this when a polymorphic arguments
>
> s/when a/when/
>
Fixed.


> > +%------------------------------------------------------------------------------%
> > +%
> > +% Predicates for handling disjunctions.
> > +%
> > +
> > +    % This version computes the convex hull linearly.
> > +    % That is, ( A ; B ; C ; D) is processed as:
> > +    %
> > +    %  ((((identity \/ A ) \/ B ) \/ C ) \/ D)
> > +    %
> > +:- pred traverse_abstract_disj_linearly(abstract_goals::in,
> > +    size_vars::in, fixpoint_info::in, polyhedron::in, polyhedron::out)
> > +    is det.
> > +
> > +traverse_abstract_disj_linearly(Goals, Locals, Info, !Polyhedron) :-
> > +    list.foldl(traverse_abstract_disjunct_linearly(Info, Locals),
> > +        Goals, polyhedron.empty, ConvexUnion),
> > +    polyhedron.intersection(ConvexUnion, !Polyhedron).
> > +
> > +:- pred traverse_abstract_disjunct_linearly(fixpoint_info::in,
> > +    size_vars::in, abstract_goal::in, polyhedron::in, polyhedron::out)
> > +    is det.
>
> Why not call this "traverse_abstract_disj_linearly_2"?
>
Done.

> > +    % This assumes that the operation in question is associative and
> > +    % commutative.
> > +    %
> > + :- func pairwise_map(func(T, T) = T, list(T)) = T.
>
> No biggie, but this bears more resemblance to a "fold" than to a "map".
>
I suppose it does - at the time I couldn't think what to call it
so I just left it as pairwise_map.  Some other ideas are
pairwise_condense or pairwise_merge_with_op.  Any suggestions?


> > +:- func test_fixpoint(polyhedron, polyhedron, size_varset) = bool.
> > +
> > +test_fixpoint(NewPoly, OldPoly, Varset) = ChangeFlag :-
> > +    %
> > +    % Constraints from this iteration.
> > +    %
> > +    NewConstraints = polyhedron.non_false_constraints(NewPoly),
> > +    %
> > +    % Constraints from previous iteration.
> > +    %
> > +    OldConstraints = polyhedron.non_false_constraints(OldPoly),
> > +    UnchangedConstraints = list.filter(entailed(Varset, NewConstraints),
> > +         OldConstraints),
> > +    ( if    list.same_length(OldConstraints, UnchangedConstraints)
> > +      then  ChangeFlag = no
> > +      else  ChangeFlag = yes
> > +    ).
>
> How about:
>
> 	(
> 		some [OldConstraint] (
> 			member(OldConstraint, OldConstraints),
> 			\+ entailed(Varset, NewConstraints, OldConstraint)
> 		)
> 	->
> 		ChangeFlag = yes
> 	;
> 		ChangeFlag = no
> 	)
>
> This would perform a (green) cut at the first OldConstraint that was not
> entailed, rather than checking all of them.
>
Thanks, that's a much better way of doing it.


> > Index: compiler/term_constr_initial.m
> > ===================================================================
> > RCS file: compiler/term_constr_initial.m
> > diff -N compiler/term_constr_initial.m
> > --- /dev/null	1 Jan 1970 00:00:00 -0000
> > +++ compiler/term_constr_initial.m	24 Mar 2005 04:19:36 -0000
>
> > +%----------------------------------------------------------------------------%
> > +%
> > +% Process each predicate and set the termination property
> > +%
> > +
> > +% Sets termination to `cannot_loop' if:
> > +%   - there is a `terminates' pragma defined for the predicate.
> > +%   - there is a `check_termination' pragma defined for the predicate
> > +%     *and* the compiler is not currently generating the intermodule
> > +%     optimization file.
> > +%   - the predicate is builtin or compiler generated.  (These are assumed
> > +%     to terminate.
>
> Close parenthesis.
>
Done.

> > +%----------------------------------------------------------------------------%
> > +%
> > +% Set the argument size constraints for imported procedures.
> > +%
> > +
> > +% When interargument size constraints are imported from other modules there
> > +% are two parts.  The first of the these is a list of ints.  Each int
> > +% represents one of a procedures arguments (including typeinfo related ones).
>
> s/procedures/procedure's/
>
Fixed.

> > +:- pred process_imported_proc(proc_id::in, proc_table::in, proc_table::out)
> > +    is det.
> > +
> > +process_imported_proc(ProcId, !ProcTable) :-
> > +    some [!ProcInfo] (
> > +        !:ProcInfo = !.ProcTable ^ det_elem(ProcId),
> > +        proc_info_get_termination2_info(!.ProcInfo, TermInfo0),
>
> It would be better to test for import_headvarids = yes(HeadVarIds) here
> rather than below...
>
> > +        process_imported_term_info(!.ProcInfo, TermInfo0, TermInfo),
> > +        proc_info_set_termination2_info(TermInfo, !ProcInfo),
> > +        svmap.det_update(ProcId, !.ProcInfo, !ProcTable)
>
> ...because that would save updating the proc_info and proc_table
> unnecessarily.
>
Done.

> > +:- pred set_compiler_gen_terminates(pred_info::in, list(proc_id)::in,
> > +    pred_id::in, module_info::in, proc_table::in, proc_table::out)
> > +    is semidet.
> > +
> > +set_compiler_gen_terminates(PredInfo, ProcIds, PredId, ModuleInfo,
> > +        !ProcTable) :-
> > +    ( hlds_pred.pred_info_is_builtin(PredInfo) ->
> > +        set_builtin_terminates(ProcIds, PredId, PredInfo, ModuleInfo,
> > +            !ProcTable)
> > +    ;
> > +        (
> > +            Name  = pred_info_name(PredInfo),
> > +            Arity = pred_info_orig_arity(PredInfo),
> > +            special_pred_name_arity(SpecPredId0, Name, Arity),
> > +            ModuleName = pred_info_module(PredInfo),
> > +            any_mercury_builtin_module(ModuleName)
> > +        ->
> > +            SpecialPredId = SpecPredId0
> > +            ;
> > +            pred_info_get_origin(PredInfo, PredOrigin),
> > +            PredOrigin = special_pred(SpecialPredId - _)
> > +        )
> > +    ->
> > +        set_generated_terminates(ProcIds, SpecialPredId, ModuleInfo,
> > +            !ProcTable)
> > +    ;
> > +        fail
> > +    ).
>
> The above code needs some reformatting.
>
Done.


> > +    % Sets up the arg_size an termination info for those special preds
>
> s/an/and/
>
Done.  I've modified that comment so that it reads:

	% Sets the termination status and argument size information for
	% those special_preds (compare and index) where the arguments
	% are either zero sized or unconstrained in size.A

The existing comment didn't really make a great deal of sense.

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