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

[Mark Brown]

On 04-Apr-2005, Julien Fischer <juliensf at cs.mu.OZ.AU> wrote:
> On Sat, 2 Apr 2005, Mark Brown wrote:
> > On 24-Mar-2005, Julien Fischer <juliensf at cs.mu.OZ.AU> wrote:
> > > +build_abstract_goal_2(Goal - _, AbstractGoal, !Info) :-
> > > +    Goal = if_then_else(_, Cond, Then, Else),
> > > +    %
> > > +    % Reduce the if-then goals to an abstract conjunction.
> > > +    %
> > > +    list.map_foldl(build_abstract_goal, [Cond, Then], AbstractConjuncts,
> > > +        !Info),
> > > +    AbstractSuccessGoal = conj(AbstractConjuncts, [], []),
> > > +    %
> > > +    % Work out a failure constraint for the Cond and then abstract the else
> > > +    % branch.  We won't bother do any other simplifications here as the AR
> > > +    % simplification pass will sort all of this out.
> > > +    %
> > > +    CondFail = find_failure_constraint_for_goal(Cond, !.Info),
> > > +    %
> > > +    % XXX FIXME - the local/non-local variable sets end up
> > > +    % being incorrect here.
> >
> > Is this one you need to fix now?
> >
> 
> No - there is a workaround in place in the only spot affected by
> this (in term_constr_fixpoint.m).  It does need to be fixed, but that's
> a separate change.
> 

Ok.

> > > +    %
> > > +    % Check the termination status of the callee procedure if we are running a
> > > +    % full analysis - ignore it if we are only running the IR analysis.
> > > +    %
> > > +    proc_info_get_termination2_info(CalleeProcInfo, CalleeTerm2Info),
> > > +    ( !.Info ^ arg_analysis_only = no ->
> > > +        TermStatus = CalleeTerm2Info ^ term_status,
> > > +        (
> > > +            TermStatus = yes(can_loop(_))
> > > +        ->
> > > +            Error = Context - can_loop_proc_called(CallerPPId,
> > > +                CalleePPId),
> > > +            info_update_errors(Error, !Info)
> > > +        ;
> > > +            TermStatus = yes(cannot_loop(_))
> > > +        ->
> > > +            true
> > > +        ;
> > > +            unexpected(this_file, "Callee procedure has no " ++
> > > +                "termination status.")
> > > +        )
> > > +    ;
> > > +        true
> > > +    ),
> >
> > The above code would be better written as nested switches.
> >
> Done ... I'm a bit dubious about there being any improvement though.
> 

The advantage, IMHO, is that every branch has an explicit condition.  This
can be useful because it saves you from having to look through all of the
preceding conditions and figuring out what remaining case covers.
In this case, the remaining condition for where unexpected/2 is called is
fairly obviously "TermStatus = no", however you would need to know the
definition of generic_termination_info/2 to verify this.

Also, if any new branches are added to the generic_termination_info/2 type,
then the compiler would notice the missing case in this goal.

> > > +%------------------------------------------------------------------------------%
> > > +%
> > > +% Additional predicates for abstracting unifications.
> > > +%
> >
> > Why do the "additional" predicates come first?  In any case, the predicates
> > in this section don't appear to be used anywhere else, so this section can
> > be removed.
> >
> 
> The predicates below are also additional predicates - the section
> heading there was misleading.  However, I'm not sure why you think they
> are not used anywhere else.  build_abstract_unification is called by
> build_abstract_goal_2.  It switches on the type of unification and calls
> the appropriate predicate to generate the abstraction for that type of
> unification.

I must have missed that.

> 
> I've combined the two sections dealing with abstraction of unifications
> under one heading.

Ok.

> > > +    % Assignment and simple_test unifications of the form X = Y
> > > +    % are abstracted as |X| - |Y| = 0.
> > > +    %
> > > +:- pred build_abstract_simple_or_assign_unify(prog_var::in, prog_var::in,
> > > +    constraints::out, traversal_info::in, traversal_info::out) is det.
> > > +
> > > +build_abstract_simple_or_assign_unify(LeftProgVar, RightProgVar,
> > > +        Constraints, !Info) :-
> > > +    SizeVarMap = !.Info ^ var_map,
> > > +    Zeros  = !.Info ^ zeros,
> > > +    LeftSizeVar = prog_var_to_size_var(SizeVarMap, LeftProgVar),
> > > +    RightSizeVar = prog_var_to_size_var(SizeVarMap, RightProgVar),
> > > +    (
> > > +        set.member(LeftSizeVar, Zeros),
> > > +        set.member(RightSizeVar, Zeros)
> > > +    ->
> > > +        Constraints = []    % `true' constraint.
> > > +    ;
> > > +        (
> > > +            (set.member(LeftSizeVar, Zeros)
> > > +            ; set.member(RightSizeVar, Zeros))
> > > +        ->
> > > +            unexpected(this_file, "zero unified with non-zero.")
> > > +        ;
> > > +            % Create non-negativity constraints.
> > > +            %
> > > +            NonNegConstrs = list.map(make_nonneg_constr,
> > > +                [LeftSizeVar, RightSizeVar]),
> > > +            Terms = [LeftSizeVar - one, RightSizeVar - (-one)],
> > > +            AssignConstr = constraint(Terms, (=), zero),
> > > +            % XXX I don't think this call to simplify helps anymore.
> > > +            Constraints = simplify_constraints([AssignConstr | NonNegConstrs])
> > > +        )
> >
> > This goal doesn't need the parentheses and indentation.
> >
> I don't see any extraneous paretheses or identation here.

If-then-elses that occur as the "else" part of another if-then-else do
not need to be parenthesised (or indented), according to the coding
standard.

Cheers,
Mark.

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