Skip to content

Commit

Permalink
Merge branch 'topic/1117' into 'master'
Browse files Browse the repository at this point in the history
Avoid more crashes on illegal self references

Closes #1117, #1122, and #1123

See merge request eng/libadalang/libadalang!1447
  • Loading branch information
Roldak committed Oct 30, 2023
2 parents 08e551a + 1dddaf7 commit d6b2017
Show file tree
Hide file tree
Showing 6 changed files with 203 additions and 46 deletions.
127 changes: 83 additions & 44 deletions ada/ast.py
Original file line number Diff line number Diff line change
Expand Up @@ -1183,7 +1183,12 @@ def has_with_visibility(refd_unit=AnalysisUnit,

@langkit_property(return_type=Bool)
def has_visibility(other_entity=T.AdaNode.entity):
return Or(
# We found a synthetic type predicate object decl, check if we are
# allowed to see it.
return other_entity.cast(SyntheticTypePredicateObjectDecl).then(
lambda sod: sod.is_referred_by(Self),
default_val=True
) & Or(
# The node is a generic package instantiation coming from a formal
# package.
other_entity.cast(GenericPackageInstantiation)._.info.from_rebound,
Expand Down Expand Up @@ -3431,15 +3436,18 @@ def most_visible_part_for_name(sym=T.Symbol, only_backwards=(Bool, False)):
Entity,

# This part is visible, now check if the next part is as well
Entity.most_visible_forward_part_for_name(sym),
Entity.most_visible_forward_part_for_name(sym, seq=True),
)

@langkit_property(return_type=T.BasicDecl.entity,
dynamic_vars=[origin, default_imprecise_fallback()])
def most_visible_forward_part_for_name(sym=T.Symbol):
def most_visible_forward_part_for_name(sym=T.Symbol, seq=T.Bool):
"""
Internal method for computing the most visible part (only looking
forward) of a basic decl according to one of its defining names.
If ``seq`` is True, the visibility check is sequential: if a next
part is in the same unit as the origin but defined after it, it will
not be considered visible.
"""
np = Var(Entity.next_part_for_name(sym))
return Cond(
Expand All @@ -3449,7 +3457,11 @@ def most_visible_forward_part_for_name(sym=T.Symbol):

# A null origin means any "find the most complete part"
origin.is_null,
np.most_visible_forward_part_for_name(sym),
np.most_visible_forward_part_for_name(sym, seq),

# The query is sequential and origin can't see the next part
seq & (origin.unit == np.unit) & (origin <= np.node),
Entity,

# If the entity is not a package declaration, we only need to check
# if its lexical env is one of the parents of origin's env.
Expand All @@ -3459,14 +3471,14 @@ def most_visible_forward_part_for_name(sym=T.Symbol):
sym,
categories=no_prims
).contains(Self.as_bare_entity),
np.most_visible_forward_part_for_name(sym),
np.most_visible_forward_part_for_name(sym, seq),
Entity
),

# Otherwise this is a package declaration, so we can use the
# is_visible property.
np.is_visible(origin.as_bare_entity),
np.most_visible_forward_part_for_name(sym),
np.most_visible_forward_part_for_name(sym, seq),

# Otherwise this was the most visible part
Entity
Expand Down Expand Up @@ -7802,14 +7814,6 @@ def predefined_operators():
add_to_env(Self.predefined_operators),
add_env(),
handle_children(),
reference(
Self.cast(AdaNode).singleton,
through=T.TypeDecl.refined_parent_primitives_env,
kind=RefKind.transitive,
dest_env=Self.node_env,
cond=Self.type_def.is_a(T.DerivedTypeDef, T.InterfaceTypeDef),
category="inherited_primitives"
),

# If this `TypeDecl` can have a predicate, add a synthetic object
# declaration into its environement in order to support name resolution
Expand All @@ -7821,7 +7825,21 @@ def predefined_operators():
Self.type_def.is_a(T.DerivedTypeDef, T.TypeAccessDef),
Entity.synthetic_type_predicate_object_decl,
No(T.env_assoc)
))
)),

# Make sure the reference to the primitives env is created *AFTER* the
# synthetic type predicate object has been added to Self's env: since
# this object has the same name as the type, it is indirectly used to
# hide the type and avoid infinite recursions in invalid Ada code such
# as ``type X is new X``. See nameres test `invalid_self_reference`.
reference(
Self.cast(AdaNode).singleton,
through=T.TypeDecl.refined_parent_primitives_env,
kind=RefKind.transitive,
dest_env=Self.node_env,
cond=Self.type_def.is_a(T.DerivedTypeDef, T.InterfaceTypeDef),
category="inherited_primitives"
)
)

record_def = Property(
Expand Down Expand Up @@ -8633,12 +8651,7 @@ class DerivedTypeDef(TypeDef):
default_val=Entity.super()
))

base_type = Property(Entity.subtype_indication.designated_type.then(
# If the designated type is Self, it means there is an illegal
# cycle. Explicitly return an null node here, otherwise this may
# cause infinite recursions in caller properties.
lambda t: If(t.node == Self.parent, No(BaseTypeDecl.entity), t)
))
base_type = Property(Entity.subtype_indication.designated_type)

base_interfaces = Property(
Entity.interfaces.map(lambda i: i.name_designated_type)
Expand Down Expand Up @@ -9160,6 +9173,34 @@ class SyntheticTypePredicateObjectDecl(BasicDecl):
type_expression = Property(Self.type_expr.as_entity)
defining_names = Property(Self.name.as_entity.singleton)

@langkit_property(return_type=T.Bool)
def is_referred_by(origin=T.AdaNode):
"""
Return whether a synthetic type predicate object can be seen from the
given ``origin`` node. If we are outside the type definition, this will
always be the type itself. Otherwise this will always be the synthetic
object, unless we are in an access type definition. In particular, this
allows correctly resolving:

.. code:: ada

type T is record
X : access T := T'Unrestricted_Access;
-- (1) (2)
end record;

Here, the reference (1) points to the type, whereas (2) refers to the
synthetic object.
"""
return And(
Not(origin.parent.parent.is_a(TypeAccessDef)),
Self.is_children_env(
Self.type_expr.cast(SyntheticTypeExpr)
.target_type.children_env,
origin.children_env
)
)


@synthetic
class DiscreteBaseSubtypeDecl(BaseSubtypeDecl):
Expand Down Expand Up @@ -10119,26 +10160,6 @@ def is_ghost_code():
'Assert', 'Assert_And_Cut', 'Assume', 'Loop_Invariant'
)

@langkit_property()
def xref_initial_env():
"""
Contract pragmas such as ``Precondition`` have full visibility on their
associated subprogram's formals although they are not in an internal
scope. We handle that by overriding this ``xref_initial_env`` property
which will make sure that name resolution uses the env returned by this
property when constructing xref_equations.
"""
return If(
Entity.id.name_symbol.any_of(
"Pre", "Post", "Pre'Class", "Post'Class",
"Precondition", "Postcondition",
"Precondition'Class", "Postcondition'Class",
"Test_Case", "Contract_Cases", "Predicate"
),
Entity.associated_entities.at(0).children_env,
Entity.children_env
)

@langkit_property()
def xref_equation():
return Cond(
Expand Down Expand Up @@ -10450,11 +10471,26 @@ def associated_entities():
def initial_env():
"""
Return the initial env name for a pragma clause. We use the
Standard package for top level use clauses.
Standard package for top level use clauses. For contract pragmas such
as ``Precondition`` or ``Predicate``, we use the env of the entity the
pragma is associated with in order to properly resolve references to
formals or to the type's ``SyntheticTypePredicateObjectDecl`` instance.
"""
return If(
return Cond(
Self.parent.parent.is_a(CompilationUnit),
named_env('Standard'),

Self.as_bare_entity.id.name_symbol.any_of(
"Pre", "Post", "Pre'Class", "Post'Class",
"Precondition", "Postcondition",
"Precondition'Class", "Postcondition'Class",
"Test_Case", "Contract_Cases", "Predicate"
),
Self.as_bare_entity.associated_entities.at(0).then(
lambda ent: direct_env(ent.children_env),
default_val=current_env()
),

current_env()
)

Expand Down Expand Up @@ -17715,7 +17751,10 @@ def designated_type_impl():
origin.is_null,
origin.bind(
Self.origin_node,
t.most_visible_forward_part_for_name(t.name_symbol)
t.most_visible_forward_part_for_name(
t.name_symbol,
seq=False
)
),
t.most_visible_part
),
Expand Down
17 changes: 16 additions & 1 deletion testsuite/tests/name_resolution/invalid_self_reference/test.adb
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,26 @@ procedure Test is
--% node.f_type_expr.p_designated_type_decl
-- This is invalid Ada but should not make LAL crash!

-- Likewise, the following invalid self derivations
-- should not make LAL crash:

type X;
type X is new X;
--% node.p_base_type(node)
--% node.f_type_def.f_subtype_indication.p_designated_type_decl
-- Likewise, this should not make LAL crash

type Y;
--% node.p_base_type(node)
type Z is new Y;
--% node.p_base_type(node)
--% node.f_type_def.f_subtype_indication.p_designated_type_decl
type Y is new Z;
--% node.p_base_type(node)
--% node.f_type_def.f_subtype_indication.p_designated_type_decl

type R is new R.T;
--% node.p_base_type(node)
--% node.f_type_def.f_subtype_indication.p_designated_type_decl
begin
null;
end Test;
35 changes: 34 additions & 1 deletion testsuite/tests/name_resolution/invalid_self_reference/test.out
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,40 @@ Working on node <ObjectDecl ["Foo"] test.adb:6:4-6:16>
Eval 'node.f_type_expr.p_designated_type_decl'
Result: None

Working on node <ConcreteTypeDecl ["X"] test.adb:11:4-11:20>
Working on node <ConcreteTypeDecl ["X"] test.adb:14:4-14:20>
============================================================

Eval 'node.p_base_type(node)'
Result: None

Eval 'node.f_type_def.f_subtype_indication.p_designated_type_decl'
Result: None

Working on node <IncompleteTypeDecl ["Y"] test.adb:18:4-18:11>
==============================================================

Eval 'node.p_base_type(node)'
Result: None

Working on node <ConcreteTypeDecl ["Z"] test.adb:20:4-20:20>
============================================================

Eval 'node.p_base_type(node)'
Result: <IncompleteTypeDecl ["Y"] test.adb:18:4-18:11>

Eval 'node.f_type_def.f_subtype_indication.p_designated_type_decl'
Result: <IncompleteTypeDecl ["Y"] test.adb:18:4-18:11>

Working on node <ConcreteTypeDecl ["Y"] test.adb:23:4-23:20>
============================================================

Eval 'node.p_base_type(node)'
Result: <ConcreteTypeDecl ["Z"] test.adb:20:4-20:20>

Eval 'node.f_type_def.f_subtype_indication.p_designated_type_decl'
Result: <ConcreteTypeDecl ["Z"] test.adb:20:4-20:20>

Working on node <ConcreteTypeDecl ["R"] test.adb:27:4-27:22>
============================================================

Eval 'node.p_base_type(node)'
Expand Down
33 changes: 33 additions & 0 deletions testsuite/tests/name_resolution/record_self_access/test.adb
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
procedure Test is
type P is tagged null record;
type T is new P with record
X : access T;
--% access_type = node.f_component_def.f_type_expr.f_type_decl
--% access_type.f_type_def.f_subtype_indication.p_designated_type_decl
--% access_type.f_type_def.f_subtype_indication.f_name.p_referenced_decl()
end record;

type T_2 is new P with record
X : access T_2 := T_2'Unrestricted_Access;
--% access_type = node.f_component_def.f_type_expr.f_type_decl
--% access_type.f_type_def.f_subtype_indication.f_name.p_referenced_decl()
--% access_type.f_type_def.f_subtype_indication.p_designated_type_decl
--% node.f_default_expr.f_prefix.p_referenced_decl()
end record;

type A is record
B : Integer;
end record;

type B is new A;

procedure Assign (X : in out B; Y : B) is
begin
X.B := Y.B;
--% node.f_dest.f_suffix.p_referenced_decl()
--% node.f_expr.f_suffix.p_referenced_decl()
end Assign;
begin
null;
end Test;

35 changes: 35 additions & 0 deletions testsuite/tests/name_resolution/record_self_access/test.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
Working on node <ComponentDecl ["X"] test.adb:4:7-4:20>
=======================================================

Set 'access_type' to 'node.f_component_def.f_type_expr.f_type_decl'
Result: <AnonymousTypeDecl ["None"] test.adb:4:11-4:19>

Eval 'access_type.f_type_def.f_subtype_indication.p_designated_type_decl'
Result: <ConcreteTypeDecl ["T"] test.adb:3:4-8:15>

Eval 'access_type.f_type_def.f_subtype_indication.f_name.p_referenced_decl()'
Result: <ConcreteTypeDecl ["T"] test.adb:3:4-8:15>

Working on node <ComponentDecl ["X"] test.adb:11:7-11:49>
=========================================================

Set 'access_type' to 'node.f_component_def.f_type_expr.f_type_decl'
Result: <AnonymousTypeDecl ["None"] test.adb:11:11-11:21>

Eval 'access_type.f_type_def.f_subtype_indication.f_name.p_referenced_decl()'
Result: <ConcreteTypeDecl ["T_2"] test.adb:10:4-16:15>

Eval 'access_type.f_type_def.f_subtype_indication.p_designated_type_decl'
Result: <ConcreteTypeDecl ["T_2"] test.adb:10:4-16:15>

Eval 'node.f_default_expr.f_prefix.p_referenced_decl()'
Result: <SyntheticTypePredicateObjectDecl ["T_2"] test.adb:10:4-16:15>

Working on node <AssignStmt test.adb:26:7-26:18>
================================================

Eval 'node.f_dest.f_suffix.p_referenced_decl()'
Result: <ComponentDecl ["B"] test.adb:19:7-19:19>

Eval 'node.f_expr.f_suffix.p_referenced_decl()'
Result: <ComponentDecl ["B"] test.adb:19:7-19:19>
2 changes: 2 additions & 0 deletions testsuite/tests/name_resolution/record_self_access/test.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
driver: inline-playground
input_sources: [test.adb]

0 comments on commit d6b2017

Please sign in to comment.