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

[Mark Brown]

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/

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

> +:- func fixpoint_options_init(widening, int) = fixpoint_options.

The arguments to this function should be documented.

> +%------------------------------------------------------------------------------%
> +%
> +% Perform a fixpoint iteration on the AR.

This does the full calculation, right?  The next section of code does
an iteration.

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

> +                %
> +                % 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/

> +%------------------------------------------------------------------------------%
> +%
> +% 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"?

> +    % 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".

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

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

> +%----------------------------------------------------------------------------%
> +%
> +% 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/

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

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

> +    % Sets up the arg_size an termination info for those special preds

s/an/and/

To be continued...

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