Skip to content

Commit

Permalink
Merge branch 'topic/1172' into 'master'
Browse files Browse the repository at this point in the history
Fix expected type for constructs expecting booleans.

Closes #1172, #1154, and #1141

See merge request eng/libadalang/libadalang!1495
  • Loading branch information
Roldak committed Dec 19, 2023
2 parents 37e8f99 + e8e272d commit 42d783b
Show file tree
Hide file tree
Showing 9 changed files with 529 additions and 42 deletions.
93 changes: 51 additions & 42 deletions ada/ast.py
Original file line number Diff line number Diff line change
Expand Up @@ -7538,6 +7538,17 @@ def matching_allocator_type(allocated_type=T.BaseTypeDecl.entity):
allocated_type.matching_formal_type(Entity.accessed_type)
)

@langkit_property(return_type=Bool, dynamic_vars=[origin])
def derives_from_std_bool_type():
"""
Return whether this type (after implicit dereference) is or derives
from the standard Boolean type. If this type is null, return False.
"""
return And(
Not(Self.is_null),
Entity.derefed_base_subtype.is_derived_type(Self.bool_type)
)

@langkit_property(return_type=T.BaseTypeDecl.entity,
dynamic_vars=[default_origin()], public=True)
def canonical_type():
Expand Down Expand Up @@ -10532,9 +10543,8 @@ def xref_equation():
),
Let(
lambda expr=Entity.args.at(0).assoc_expr:
Bind(expr.expected_type_var, Self.bool_type)
& expr.sub_equation
& expr.matches_expected_formal_prim_type
expr.sub_equation
& expr.expect_bool_derived_type
) & Entity.args.at(1)._.assoc_expr.then(
lambda msg:
Bind(msg.expected_type_var, Self.std_entity('String'))
Expand Down Expand Up @@ -10599,7 +10609,7 @@ def xref_equation():
lambda expr:
Bind(expr.expected_type_var, Self.bool_type)
& expr.sub_equation
& expr.matches_expected_formal_prim_type,
& expr.matches_expected_formal_type,
default_val=LogicFalse()
),

Expand All @@ -10614,7 +10624,7 @@ def xref_equation():
lambda arg:
Bind(arg.assoc_expr.expected_type_var, Self.bool_type)
& arg.assoc_expr.sub_equation
& arg.assoc_expr.matches_expected_formal_prim_type
& arg.assoc_expr.matches_expected_formal_type
),

Entity.id.name_is("Contract_Cases"),
Expand All @@ -10632,7 +10642,7 @@ def xref_equation():
lambda expr=Entity.args.at(0).assoc_expr:
Bind(expr.expected_type_var, Self.bool_type)
& expr.sub_equation
& expr.matches_expected_formal_prim_type
& expr.matches_expected_formal_type
),
LogicTrue()
) & Let(
Expand Down Expand Up @@ -11128,7 +11138,7 @@ def xref_equation():
Bind(Self.expr.expected_type_var, Self.bool_type)
& env.bind(expr_equation_env,
Entity.expr.sub_equation)
& Self.expr.matches_expected_formal_prim_type
& Self.expr.matches_expected_formal_type
),

Entity.id.name_is('Contract_Cases'),
Expand Down Expand Up @@ -12938,19 +12948,26 @@ def matches_expected_membership_type():
)

@langkit_property(return_type=T.Equation, dynamic_vars=[origin])
def matches_expected_formal_prim_type():
def matches_expected_prefix_type():
return Predicate(
BaseTypeDecl.matching_formal_prim_type,
BaseTypeDecl.matching_prefix_type,
Self.type_var,
Self.expected_type_var
)

@langkit_property(return_type=T.Equation, dynamic_vars=[origin])
def matches_expected_prefix_type():
return Predicate(
BaseTypeDecl.matching_prefix_type,
Self.type_var,
Self.expected_type_var
def expect_bool_derived_type():
"""
Construct an equation which asserts that the expected type of this
expression is the standard boolean type or any type that derives from
it.
"""
return And(
Bind(Self.expected_type_var, Self.bool_type)
| Bind(Self.type_var, Self.expected_type_var,
conv_prop=BaseTypeDecl.derefed_base_subtype),

Predicate(BaseTypeDecl.derives_from_std_bool_type, Self.type_var)
)

@langkit_property(public=True, dynamic_vars=[default_imprecise_fallback()],
Expand Down Expand Up @@ -13573,8 +13590,8 @@ def test_eq():
Bind(Self.left.expected_type_var, Self.bool_type),
Bind(Self.right.expected_type_var, Self.bool_type),

Self.left.matches_expected_formal_prim_type,
Self.right.matches_expected_formal_prim_type,
Self.left.expect_bool_derived_type,
Self.right.expect_bool_derived_type,

Bind(Self.type_var, Self.left.type_var)
)
Expand Down Expand Up @@ -16597,15 +16614,15 @@ def contract_cases_assoc_equation():
lambda e:
Bind(e.expected_type_var, Self.bool_type)
& e.sub_equation
& e.matches_expected_formal_prim_type,
& e.matches_expected_formal_type,

# Nothing to do for `others =>`
default_val=LogicTrue()
)
),
Bind(Entity.expr.expected_type_var, Self.bool_type),
Entity.expr.sub_equation,
Entity.expr.matches_expected_formal_prim_type
Entity.expr.matches_expected_formal_type
)

@langkit_property(return_type=Equation, dynamic_vars=[env, origin])
Expand Down Expand Up @@ -17058,19 +17075,17 @@ def dependent_exprs():
def xref_equation():
return (
# Construct sub equations for common sub exprs
Bind(Self.cond_expr.expected_type_var, Self.bool_type)
& Entity.cond_expr.sub_equation
& Entity.cond_expr.matches_expected_formal_prim_type
Entity.cond_expr.sub_equation
& Entity.cond_expr.expect_bool_derived_type

# Construct the equation for the then branch
& Entity.then_expr.sub_equation

& Entity.alternatives.logic_all(
lambda elsif:
# Build the sub equations for cond and then exprs
Bind(elsif.cond_expr.expected_type_var, Self.bool_type)
& elsif.cond_expr.sub_equation
& elsif.cond_expr.matches_expected_formal_prim_type
elsif.cond_expr.sub_equation
& elsif.cond_expr.expect_bool_derived_type
& elsif.then_expr.sub_equation
)

Expand All @@ -17081,8 +17096,7 @@ def xref_equation():
Entity.else_expr.sub_equation,

# If no else, then the then_expression has type bool
Bind(Self.then_expr.expected_type_var, Self.bool_type)
& Entity.then_expr.matches_expected_formal_prim_type
Entity.then_expr.expect_bool_derived_type
)

& Or(
Expand Down Expand Up @@ -19811,7 +19825,7 @@ def xref_equation():
return And(
Bind(Self.expr.expected_type_var, Self.bool_type),
Entity.expr.sub_equation,
Entity.expr.matches_expected_formal_prim_type
Entity.expr.matches_expected_formal_type
)

xref_entry_point = Property(True)
Expand All @@ -19835,7 +19849,7 @@ def xref_equation():
spec_success,
Bind(Self.expr.expected_type_var, Self.bool_type)
& Entity.expr.sub_equation
& Entity.expr.matches_expected_formal_prim_type
& Entity.expr.matches_expected_formal_type
& Bind(Self.type_var, Self.expr.type_var),
LogicFalse()
)
Expand Down Expand Up @@ -21915,9 +21929,8 @@ def xref_equation():
return And(
Entity.cond_expr.then(
lambda cond:
Bind(cond.expected_type_var, Self.bool_type)
& cond.sub_equation
& cond.matches_expected_formal_prim_type,
cond.sub_equation
& cond.expect_bool_derived_type,
default_val=LogicTrue()
),

Expand Down Expand Up @@ -22106,9 +22119,8 @@ class IfStmt(CompositeStmt):
@langkit_property()
def xref_equation():
return (
Bind(Self.cond_expr.expected_type_var, Self.bool_type)
& Entity.cond_expr.sub_equation
& Self.cond_expr.matches_expected_formal_prim_type
Entity.cond_expr.sub_equation
& Self.cond_expr.expect_bool_derived_type
)


Expand All @@ -22125,9 +22137,8 @@ class ElsifStmtPart(AdaNode):
@langkit_property()
def xref_equation():
return (
Bind(Self.cond_expr.expected_type_var, Self.bool_type)
& Entity.cond_expr.sub_equation
& Self.cond_expr.matches_expected_formal_prim_type
Entity.cond_expr.sub_equation
& Self.cond_expr.expect_bool_derived_type
)


Expand Down Expand Up @@ -22166,9 +22177,8 @@ class WhileLoopSpec(LoopSpec):
@langkit_property(return_type=Equation)
def xref_equation():
return And(
Bind(Self.expr.expected_type_var, Self.bool_type),
Entity.expr.sub_equation,
Entity.expr.matches_expected_formal_prim_type
Entity.expr.expect_bool_derived_type
)


Expand Down Expand Up @@ -22477,9 +22487,8 @@ class SelectWhenPart(AdaNode):
def xref_equation():
return Entity.cond_expr.then(
lambda c: And(
Bind(c.expected_type_var, Self.bool_type),
c.sub_equation,
c.matches_expected_formal_prim_type
c.expect_bool_derived_type
),
default_val=LogicTrue()
)
Expand Down Expand Up @@ -22801,7 +22810,7 @@ def xref_equation():
return And(
Bind(Self.barrier.expected_type_var, Self.bool_type),
Entity.barrier.sub_equation,
Entity.barrier.matches_expected_formal_prim_type
Entity.barrier.matches_expected_formal_type
)


Expand Down
13 changes: 13 additions & 0 deletions testsuite/tests/name_resolution/if_implicit_deref/test.adb
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
with Ada.Containers.Vectors;

procedure Test is
package My_Vectors is new Ada.Containers.Vectors (Positive, Boolean);
use My_Vectors;

V : My_Vectors.Vector;
begin
if V (1) then
null;
end if;
pragma Test_Statement_UID;
end Test;
21 changes: 21 additions & 0 deletions testsuite/tests/name_resolution/if_implicit_deref/test.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
Analyzing test.adb
##################

Resolving xrefs for node <IfStmt test.adb:9:4-11:11>
****************************************************

Expr: <CallExpr test.adb:9:7-9:12>
references: test().v
type: test().my_vectors.constant_reference_type
expected type: standard.boolean
Expr: <Id "V" test.adb:9:7-9:8>
references: test().v
type: test().my_vectors.vector
expected type: None
Expr: <Int test.adb:9:10-9:11>
references: None
type: standard.universal_int_type_
expected type: standard.positive


Done.
2 changes: 2 additions & 0 deletions testsuite/tests/name_resolution/if_implicit_deref/test.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
driver: name-resolution
input_sources: [test.adb]
Loading

0 comments on commit 42d783b

Please sign in to comment.