mercurylang/mercury
1
0
Fork 0
mirror of https://github.com/Mercury-Language/mercury.git synced 2025-12-11 03:45:33 +00:00
Code Issues Projects Releases Wiki Activity

Avoid misleading occurs check warnings.

Browse Source 
compiler/superhomogeneous.m:
    Record a unification between X and f(Yi) as possibly leading to
    an occurs check warning only if f is known to be a data constructor,
    either user defined or the builtin tuple constructor.

compiler/hlds_cons.m:
    Add a version of the search_cons_table predicate that does not construct
    the list of hlds_cons_defns that match the given cons_id. The new code
    in superhomogeneous.m needs to know whether a cons_id is a known data
    constructor, but it does not need to know its matching definitions,
    and constructing that list is reasonably expensive when it has to be
    executed for every single function symbol in every clause.

    Add some documentation of the existing predicates, and separate their
    implementations from each other with lines.

tests/warnings/occurs.{m,exp}:
    Extend this test case both with a unifications we should warn about
    (a circular unification whose top level cons_id is a tuple constructor)
    and one we should not warn about (when the cons_is is NOT a data
    constructor of any kind).

compiler/implementation_defined_literals.m:
compiler/prog_data.m:
    Clarify related documentation.
This commit is contained in:
Zoltan Somogyi
2020-04-15 02:57:16 +10:00
parent 520ce39800
commit 9a909ddc7f
6 changed files with 215 additions and 17 deletions
Download Patch File Download Diff File Expand all files Collapse all files

76
compiler/hlds_cons.m
View File

@@ -78,24 +78,58 @@
:- func init_cons_table = cons_table.
% Insert the given hlds_cons_defn into the cons_table as the definition
% for one or more cons_ids. These cons_ids should represent the full range
% of possible qualifications of the *same* cons_id, from unqualified
% through all forms of possible qualification to fully qualified,
% and with both the actual type_ctor and the dummy type_ctor.
% The first argument should be the fully qualified version with
% the actual type_ctor.
%
:- pred insert_into_cons_table(cons_id::in, list(cons_id)::in,
hlds_cons_defn::in, cons_table::in, cons_table::out) is det.
% Does the given cons_id occur in the cons_table? This does the same job
% as search_cons_table, but without constructing and returning the list of
% possible matching hlds_cons_defns.
%
:- pred is_known_data_cons(cons_table::in, cons_id::in) is semidet.
% Does the given cons_id occur in the cons_table? If yes, return
% the list of possible matching hlds_cons_defns, which will be
% for occurrences of the same cons_id in different type definitions.
%
:- pred search_cons_table(cons_table::in, cons_id::in,
list(hlds_cons_defn)::out) is semidet.
% Does the given cons_id occur in the definition of the given type
% constructor in the cons_table? If yes, return its definition in that
% type; otherwise, fail.
%
:- pred search_cons_table_of_type_ctor(cons_table::in, type_ctor::in,
cons_id::in, hlds_cons_defn::out) is semidet.
% Does the given cons_id occur in the definition of the given type
% constructor in the cons_table? If yes, return its definition in that
% type; otherwise, abort.
%
:- pred lookup_cons_table_of_type_ctor(cons_table::in, type_ctor::in,
cons_id::in, hlds_cons_defn::out) is det.
% Return all the constructor definitions in the cons_table.
%
:- pred get_all_cons_defns(cons_table::in,
assoc_list(cons_id, hlds_cons_defn)::out) is det.
% Return the list of arities with which the given sym_name occurs
% in the cons_table.
%
:- pred return_cons_arities(cons_table::in, sym_name::in, list(int)::out)
is det.
% Transform every hlds_cons_defn in the cons_table using the
% given predicate.
%
:- pred replace_cons_defns_in_cons_table(
pred(hlds_cons_defn, hlds_cons_defn)::in(pred(in, out) is det),
cons_table::in, cons_table::out) is det.
@@ -170,8 +204,12 @@
ice_cons_defn :: hlds_cons_defn
).
%---------------------------------------------------------------------------%
init_cons_table = map.init.
%---------------------------------------------------------------------------%
insert_into_cons_table(MainConsId, OtherConsIds, ConsDefn, !ConsTable) :-
( if MainConsId = cons(MainSymName, _, _) then
MainName = unqualify_name(MainSymName),
@@ -187,6 +225,32 @@ insert_into_cons_table(MainConsId, OtherConsIds, ConsDefn, !ConsTable) :-
unexpected($pred, "MainConsId is not cons")
).
%---------------------------------------------------------------------------%
is_known_data_cons(ConsTable, ConsId) :-
ConsId = cons(SymName, _, _),
Name = unqualify_name(SymName),
map.search(ConsTable, Name, InnerConsTable),
is_known_data_cons_inner(InnerConsTable, ConsId).
:- pred is_known_data_cons_inner(list(inner_cons_entry)::in, cons_id::in)
is semidet.
is_known_data_cons_inner([Entry | Entries], ConsId) :-
( if
(
ConsId = Entry ^ ice_fully_qual_cons_id
;
list.member(ConsId, Entry ^ ice_other_cons_ids)
)
then
true
else
is_known_data_cons_inner(Entries, ConsId)
).
%---------------------------------------------------------------------------%
search_cons_table(ConsTable, ConsId, ConsDefns) :-
ConsId = cons(SymName, _, _),
Name = unqualify_name(SymName),
@@ -249,6 +313,8 @@ search_inner_other_cons_ids([Entry | Entries], ConsId, !:ConsDefns) :-
true
).
%---------------------------------------------------------------------------%
search_cons_table_of_type_ctor(ConsTable, TypeCtor, ConsId, ConsDefn) :-
ConsId = cons(SymName, _, _),
Name = unqualify_name(SymName),
@@ -278,6 +344,8 @@ search_inner_cons_ids_type_ctor([Entry | Entries], TypeCtor, ConsId,
search_inner_cons_ids_type_ctor(Entries, TypeCtor, ConsId, ConsDefn)
).
%---------------------------------------------------------------------------%
lookup_cons_table_of_type_ctor(ConsTable, TypeCtor, ConsId, ConsDefn) :-
( if
search_cons_table_of_type_ctor(ConsTable, TypeCtor, ConsId,
@@ -288,6 +356,8 @@ lookup_cons_table_of_type_ctor(ConsTable, TypeCtor, ConsId, ConsDefn) :-
unexpected($pred, "lookup failed")
).
%---------------------------------------------------------------------------%
get_all_cons_defns(ConsTable, AllConsDefns) :-
map.foldl_values(accumulate_all_inner_cons_defns, ConsTable,
[], AllConsDefns).
@@ -307,6 +377,8 @@ project_inner_cons_entry(Entry, Pair) :-
Entry = inner_cons_entry(MainConsId, _OtherConsIds, ConsDefn),
Pair = MainConsId - ConsDefn.
%---------------------------------------------------------------------------%
return_cons_arities(ConsTable, SymName, Arities) :-
Name = unqualify_name(SymName),
( if map.search(ConsTable, Name, InnerConsTable) then
@@ -343,6 +415,8 @@ return_cons_arities_inner_cons_ids([ConsId | ConsIds], SymName, !Arities) :-
),
return_cons_arities_inner_cons_ids(ConsIds, SymName, !Arities).
%---------------------------------------------------------------------------%
replace_cons_defns_in_cons_table(Replace, !ConsTable) :-
map.map_values_only(replace_cons_defns_in_inner_cons_table(Replace),
!ConsTable).
@@ -363,6 +437,8 @@ replace_cons_defns_in_inner_cons_entry(Replace, !Entry) :-
Replace(ConsDefn0, ConsDefn),
!Entry ^ ice_cons_defn := ConsDefn.
%---------------------------------------------------------------------------%
cons_table_optimize(!ConsTable) :-
map.optimize(!ConsTable).

8
compiler/implementation_defined_literals.m
View File

@@ -9,10 +9,10 @@
% File: implementation_defined_literals.m.
% Author: wangp.
%
% This module replaces "implementation-defined literals" such as $file and
% $line by real constants. We transform clauses rather than procedures
% because, currently, clauses are written out to `.opt' files and $file and
% $line need to be substituted beforehand.
% This module replaces implementation-defined literals such as $file and $line
% by real constants. We transform clauses rather than procedures because
% currently, clauses rather than procedures are written out to `.opt' files,
% and $file and $line must be substituted before being written out.
%
%-----------------------------------------------------------------------------%

25
compiler/prog_data.m
View File

@@ -45,10 +45,20 @@
% The representation of cons_ids below is a compromise. The cons_id
% type must be defined here, in a submodule of parse_tree.m, because
% it is a component of insts. However, after the program has been read
% in, the cons_ids cons, int_const, string_const and float_const,
% which can appear in user programs, may also be augmented by the other
% cons_ids, which can only be generated by the compiler.
% it is a component of insts. However, after the program has been read in,
% the cons_ids which can appear in user programs, namely
%
% cons
% tuple_cons
% int*_const
% uint*_const
% float_const
% char_const
% string_const
% impl_defined_const
%
% may also be augmented by the other cons_ids, which can only be
% generated by the compiler.
%
% The problem is that some of these compiler generated cons_ids
% refer to procedures, and the natural method of identifying
@@ -100,6 +110,10 @@
% where Str = term_io.quoted_char(Char).
; tuple_cons(arity)
% Tuples are represented by this cons_id after
% resolve_unify_functor.m has been run as part of the
% post-typecheck pass. Until then, they are represented as
% cons(unqualified("{}"), ...).
; closure_cons(shrouded_pred_proc_id, lambda_eval_method)
% Note that a closure_cons represents a closure, not just
@@ -121,6 +135,9 @@
; string_const(string)
; impl_defined_const(string)
% $file, $line, $module, $pred, or $grade; the string gives
% the part after the dollar sign. (Any string other than
% these five are unrecognized and will yield type errors.)
; type_ctor_info_const(
module_name,

67
compiler/superhomogeneous.m
View File

@@ -135,6 +135,7 @@
:- import_module check_hlds.mode_util.
:- import_module hlds.from_ground_term_util.
:- import_module hlds.goal_util.
:- import_module hlds.hlds_cons.
:- import_module hlds.hlds_out.
:- import_module hlds.hlds_out.hlds_out_goal.
:- import_module hlds.make_goal.
@@ -149,8 +150,8 @@
:- import_module parse_tree.parse_dcg_goal.
:- import_module parse_tree.parse_goal.
:- import_module parse_tree.parse_inst_mode_name.
:- import_module parse_tree.parse_tree_out_term.
:- import_module parse_tree.parse_sym_name.
:- import_module parse_tree.parse_tree_out_term.
:- import_module parse_tree.parse_type_name.
:- import_module parse_tree.prog_mode.
:- import_module parse_tree.prog_out.
@@ -690,7 +691,6 @@ unravel_var_functor_unification(XVar, YFunctor, YArgTerms0, YFunctorContext,
Context, MainContext, SubContext,
Purity, Order, !.AncestorVarMap, Expansion,
!SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
map.search_insert(XVar, Context, _OldContext, !AncestorVarMap),
substitute_state_var_mappings(YArgTerms0, YArgTerms, !VarSet,
!SVarState, !Specs),
( if
@@ -749,6 +749,8 @@ unravel_var_functor_unification(XVar, YFunctor, YArgTerms0, YFunctorContext,
;
MaybeQualifiedYArgTerms = [_ | _],
ArgContext = ac_functor(ConsId, MainContext, SubContext),
maybe_add_to_ancestor_var_map(!.ModuleInfo, XVar, ConsId, Context,
!AncestorVarMap),
(
Purity = purity_pure,
% If we can, we want to add the unifications for the arguments
@@ -793,6 +795,67 @@ unravel_var_functor_unification(XVar, YFunctor, YArgTerms0, YFunctorContext,
)
).
% Add the variable on the left side of the var-functor unification
% XVar = ConsId(...) to the ancestor var map *if* it can be part of
% an occurs check violation we want to report.
%
% - The occurs check cannot be violated if ConsId is a constant.
%
% - If ConsId cannot actually a data constructor, then this unification
% cannot be part of an occurs check violation we want to report.
% There are four possibilities:
%
% 1 ConsId(...) is a full application of a function, which returns
% a piece of data. Even if XVar occurs somewhere inside the
% arguments of ConsId, checking whether XVar is equal to the
% value computed from it is a perfectly legitimate test.
%
% 2 ConsId(...) is a partial application of a function or a predicate,
% and XVar's type is the higher order type matching the type
% of this closure. This case *would* be a perfectly legitimate
% equality test like case 1, were it not for the fact that unification
% of higher order values is not allowed (because it is an undecidable
% problem). This should therefore be detected as a type error.
%
% 3 ConsId(...) is a partial application of a function or a predicate,
% and XVar's type is not the higher order type matching the type
% of this closure. This is a more straightforward type error.
%
% 4 ConsId is not a function or a predicate. This is a straightforward
% "unknown function symbol" error.
%
% In case 1, any warning about occurs check violation would be
% misleading. In cases 2, 3 and 4, it would be redundant, since they
% all involve an error which is not really about the occurs check.
%
:- pred maybe_add_to_ancestor_var_map(module_info::in, prog_var::in,
cons_id::in, prog_context::in,
ancestor_var_map::in, ancestor_var_map::out) is det.
maybe_add_to_ancestor_var_map(ModuleInfo, XVar, ConsId, Context,
!AncestorVarMap) :-
( if
% The only two kinds of cons_ids that may (a) appear in user
% written code, as opposed to compiler-generated code, and
% (b) may have nonzero arities, are cons and tuple_cons.
% However, the cons_ids of tuples are represented by tuple_cons
% only *after* resolve_unify_functor.m has been run as part of
% the post_typecheck pass. Until then, they have the form
% recognized by the second disjunct.
ConsId = cons(SymName, Arity, _TypeCtor),
Arity > 0,
(
module_info_get_cons_table(ModuleInfo, ConsTable),
is_known_data_cons(ConsTable, ConsId)
;
SymName = unqualified("{}")
)
then
map.search_insert(XVar, Context, _OldContext, !AncestorVarMap)
else
true
).
:- pred parse_ordinary_cons_id(term.const::in, list(prog_term)::in,
term.context::in, cons_id::out,
list(error_spec)::in, list(error_spec)::out) is det.

6
tests/warnings/occurs.exp
View File

@@ -1,2 +1,4 @@
occurs.m:019: Warning: the variable `A' is unified with a term containing
occurs.m:019: itself.
occurs.m:026: Warning: the variable `A' is unified with a term containing
occurs.m:026: itself.
occurs.m:037: Warning: the variable `B' is unified with a term containing
occurs.m:037: itself.

50
tests/warnings/occurs.m
View File

@@ -10,24 +10,64 @@
:- interface.
:- import_module list.
:- pred test(list(int)::in, int::out, int::out) is det.
:- type t
---> f({int, t}).
:- pred test(list(int)::in, {int, t}::in,
int::out, int::out, int::out, string::out) is det.
:- implementation.
test(A, X, Y) :-
:- import_module set.
test(A, B, X, Y, Z, MaybeFixpoint) :-
( if
% We should get a warning for this.
A = [_A0, _A1 | A]
then
X = 1
else
X = 2
),
( if
disable_warning [suspected_occurs_check_failure] (
A = [_A2, _A3, _A4 | A]
)
% We should get a warning for this as well.
% Unlike the list example above, this involves a cons_id
% that does not have an entry in the cons_table.
B = {_B0, f(B)}
then
Y = 1
else
Y = 2
),
( if
disable_warning [suspected_occurs_check_failure] (
% We should not get a warning for this occurs check
% violatiom because the warnings has been disabled.
A = [_A2, _A3, _A4 | A]
)
then
Z = 1
else
Z = 2
),
Program = program(0),
Interpretation = set.make_singleton_set("xyzzy"),
% We should not get a warning for this occurs check violatiom
% because the function symbol involved is not a *data* constructor.
( if Interpretation = tp(Program, Interpretation) then
MaybeFixpoint = "have reached fixpoint"
else
MaybeFixpoint = "have not reached fixpoint"
).
:- type program
---> program(int).
:- type interpretation == set(string).
:- func tp(program, interpretation) = interpretation.
tp(_Program, Interpretation) = Interpretation.