[m-rev.] for review: fix bug 311

[Julien Fischer]

On Sun, 27 Jul 2014, Zoltan Somogyi wrote:

> Fix mantis bug 311.
> 
> compiler/simplify_goal_disj.m:
>     Look for the conditions that lead to the bug (a disjunction that
>     further instantiates an already partially instantiated variable).
>     Generate an error message when found, PROVIDED that this happens
>     in a context in which the surrounding procedure can succeed
>     more than once. (If it cannot, then you cannot invoke an all-solutions
>     predicate on it, and the bug cannot happen.)
>
>     This condition (a model_non surrounding procedure) was motivated
>     by mdbcomp/feedback.m, which does not compile without it.
> 
> compiler/simplify_info.m:
>     The simplify_info type used to contain four different kinds of fields:
>
>     1 static fields; set and then never changed, such as the id of the
>       containing procedure
>     2 global information, such as the varset and vartypes, which are updated
>       as new variable are added, and whose updates need to be kept regardless
>       of what part of the procedure is analyzed next
>     3 information about the context surrounding the goal currently being
>       analyzed, such as the number of lambda expressions we are inside
>     4 information about the point in the code before the goal currently being
>       analyzed, such as the set of equivalences that currently hold between
>       variables (part of common_info).
>
>     The code of the simplify_goal*.m modules used to have jump through hoops
>     to handle 3 and 4 properly, given that the simplify_info was being
>     threaded through code in a way that was suitable only for 1 and 2.
>
>     This change takes categories 3 and 4 out of the simplify_info.
>     It creates a new type, simplify_nested_context, for category 3,
>     and adds information about the ability of the procedure surrounding
>     the current point to succeed more than once (needed for the bug311 fix)
>     to this new type.
> 
> compiler/simplify_tasks.m:
>     Rename the do_once task to mark_code_model_changes, since this
>     expresses what the task is much less ambiguously.
> 
> compiler/simplify_goal*.m:
> compiler/simplify_proc.m:
> compiler/common.m:
> compiler/mercury_compile_front_end.m:
> compiler/mercury_compile_llds_back_end.m:
>     Conform to the changes to simplify_info (and simplify_tasks).
>     Pass the current instmap and common_info (the two category 4 fields)
>     separately.
>
>     Mark some places that could be improved.
> 
> compiler/hlds_out_mode.m:
>     Generate easier-to-understand debugging output. I needed this to track
>     down a bug in my initial fix.
> 
> compiler/inst_match.m:
>     Remove a redundant unification that couldn't fail (since it was invoked
>     only if the exact same unification succeeded a few lines earlier).
>     Apply another minor optimizations.
> 
> compiler/instmap.m:
>     Remove references to the alias branch. It won't be coming back.
> 
> compiler/error_util.m:
>     Fix some documentation.
> 
> mdbcomp/feedback.m:
>     Put related stuff together.
> 
> tests/invalid/bug311.{m,err_exp}:
>     New test case for the bug.
> 
> tests/invalid/Mmakefile:
>     Enable the new test case.

Please also add an entry to the NEWS file mentioning the bug-fix.

> diff --git a/compiler/common.m b/compiler/common.m
> index c5ef900..e5fa621 100644
> --- a/compiler/common.m
> +++ b/compiler/common.m

...

> @@ -238,10 +241,10 @@
>      % A struct_map maps a principal type constructor and a cons_id of that
>      % type to information about cells involving that cons_id.
>      %
> -    % The reason why we need the principal type constructors is that two
> -    % syntactically identical structures have compatible representations if and
> -    % only if their principal type constructors are the same.  For example, if
> -    % we have:
> +    % The reason why we need the principal type constructors is that
> +    % two syntactically identical structures are guaranteed to have
> +    % compatible representations if and ONLy if their principal type

s/ONLy/ONLY/

> +    % constructors are the same. For example, if we have:
>      %
>      %   :- type maybe_err(T) ---> ok(T) ; err(string).
>      %

...

> @@ -621,7 +619,9 @@ common_optimise_call_2(SeenCall, InputArgs, OutputArgs, Modes, GoalInfo,
>              simplify_info_get_module_info(!.Info, ModuleInfo),
>              modes_to_uni_modes(ModuleInfo, Modes, Modes, UniModes),
>              create_output_unifications(GoalInfo, OutputArgs, OutputArgs2,
> -                UniModes, Goals, !Info),
> +                UniModes, Goals, Common0, _Common1, !Info),
> +            % XXX should be Common = Common1
> +            Common = Common0,

If that must be left as an XXX, make the comment say why it is not currently
Common1.

...

> index 441908b..7803f36 100644
> --- a/compiler/simplify_goal.m
> +++ b/compiler/simplify_goal.m
> @@ -16,9 +16,11 @@
>  :- module check_hlds.simplify.simplify_goal.
>  :- interface.
> 
> +:- import_module check_hlds.simplify.common.
>  :- import_module check_hlds.simplify.simplify_info.
>  :- import_module hlds.
>  :- import_module hlds.hlds_goal.
> +:- import_module hlds.instmap.
>
>      % Handle simplification of all goals.
>      %
> @@ -26,13 +28,33 @@
>      % and its surrounding goals before invoking the goal-type-specific
>      % simplification code on it.
>      %
> +    % simplify_goal and its goal-type-specific subcontractor predicates
> +    % pass around information about the context surrounding the goal
> +    % currently being analyzed in the simplify_nested_context argument.
> +    % They pass around information about the program point just before
> +    % the current goal in the instmap and common_info arguments.
> +    % They pass around information that is global to the simplification
> +    % process as a whole in the simplify_info arguments..

Doubled-up full stop there.

> +    %
> +    % These predicates return the common_info appropriate to the program
> +    % point after the goal that was just analyzed in the common_info output
> +    % argumen. They do not return the new instmap, because it is not necessary.

s/argumen/argument/

> +    % The two predicates that need to know the instmap after the goal
> +    % that was just analyzed (simplify_goal_conj, after a conjunct, and
> +    % simplify_goal_ite, after the condition) apply the goal's instmap delta
> +    % themselves.
> +    %
>  :- pred simplify_goal(hlds_goal::in, hlds_goal::out,
> +    simplify_nested_context::in, instmap::in,
> +    common_info::in, common_info::out,
>      simplify_info::in, simplify_info::out) is det.

...

> diff --git a/compiler/simplify_goal_conj.m b/compiler/simplify_goal_conj.m
> index 77d9034..4d095cd 100644
> --- a/compiler/simplify_goal_conj.m
> +++ b/compiler/simplify_goal_conj.m

...

> @@ -110,30 +115,58 @@ contains_multisoln_goal(Goals) :-

...

>              % Delete unreachable goals.
>              (
> -                simplify_info_get_instmap(!.Info, InstMap1),
> -                instmap_is_unreachable(InstMap1)
> +                % XXX InstMap1 after
> +                % update_instmap(Goal1, InstMap0, InstMap1),
> +                instmap_is_unreachable(InstMap0)

Is that XXX something you plan to commit or just a note to yourself?
(If the former, then more detail is required).

...

> diff --git a/compiler/simplify_goal_disj.m b/compiler/simplify_goal_disj.m
> index ac3ec0b..7aba6c2 100644
> --- a/compiler/simplify_goal_disj.m
> +++ b/compiler/simplify_goal_disj.m

...

> @@ -78,12 +91,33 @@ simplify_goal_disj(GoalExpr0, GoalExpr, GoalInfo0, GoalInfo, !Info) :-
>              simplify_info_get_module_info(!.Info, ModuleInfo1),
>              NonLocals = goal_info_get_nonlocals(GoalInfo0),
>              simplify_info_get_var_types(!.Info, VarTypes),
> -            merge_instmap_deltas(InstMap0, NonLocals, VarTypes, InstMaps,
> +            merge_instmap_deltas(InstMap0, NonLocals, VarTypes, InstMapDeltas,
>                  NewDelta, ModuleInfo1, ModuleInfo2),
>              simplify_info_set_module_info(ModuleInfo2, !Info),
> -            goal_info_set_instmap_delta(NewDelta, GoalInfo0, GoalInfo)
> +            goal_info_set_instmap_delta(NewDelta, GoalInfo0, GoalInfo),
> +
> +            (
> +                simplify_do_after_front_end(!.Info),
> +                % If the surround procedure cannot have more than one solution,

s/surround/surrounding/

> +                % then any warning about not being able to compute the set of
> +                % all solutions would be meaningless and confusing.
> +                NestedContext0 ^ snc_proc_is_model_non = yes(Innermost)
> +            ->
> +                warn_about_any_problem_partial_vars(Innermost, GoalInfo0,
> +                    InstMap0, NewDelta, !Info)
> +            ;
> +                true
> +            )

...

> @@ -101,18 +135,121 @@ simplify_goal_disj(GoalExpr0, GoalExpr, GoalInfo0, GoalInfo, !Info) :-
>          true
>      ).
> 
> +    % Look for the kind of bug represented by tests/invalid/bug311.m.
> +    % For a detailed description of the problem, see that test case.
> +    %
> +:- pred warn_about_any_problem_partial_vars(innermost_proc::in,
> +    hlds_goal_info::in, instmap::in, instmap_delta::in,
> +    simplify_info::in, simplify_info::out) is det.
> + 
> +warn_about_any_problem_partial_vars(Innermost, GoalInfo, InstMap0,
> +        InstMapDelta, !Info) :-
> +    instmap_delta_to_assoc_list(InstMapDelta, InstMapDeltaChanges),
> +    simplify_info_get_module_info(!.Info, ModuleInfo),
> +    list.filter_map(is_var_a_problem_partial_var(ModuleInfo, InstMap0),
> +        InstMapDeltaChanges, ProblemPartialVars),
> +    (
> +        ProblemPartialVars = []
> +    ;
> +        ProblemPartialVars = [_ | _],
> +        (
> +            Innermost = imp_whole_proc,
> +            ProcStr = "the procedure"
> +        ;
> +            Innermost = imp_lambda(LambdaContext),
> +            % If the lambda expression does not leave the scope of its
> +            % defining procedure and does not have an all-solutions predicate
> +            % invoked on it, the warning we generate could be a bit misleading.
> +            % Unfortunately, without an escape analysis, I (zs) see no way
> +            % to avoid this while still generating the warning in cases
> +            % where the program *does* invoke an all-solutions predicate
> +            % on the closure generated by the ambda expression.

s/ambda/lambda/

...

The rest looks okay.

Cheers,
Julien