From e8e272df2e02460d11d1ae55220f5254be715298 Mon Sep 17 00:00:00 2001 From: Romain Beguet Date: Mon, 18 Dec 2023 15:43:41 +0100 Subject: [PATCH] Fix expected type for constructs expecting booleans. --- ada/ast.py | 93 ++--- .../if_implicit_deref/test.adb | 13 + .../if_implicit_deref/test.out | 21 ++ .../if_implicit_deref/test.yaml | 2 + .../use_bool_derived_type/test.out | 345 ++++++++++++++++++ .../use_bool_derived_type/test.yaml | 2 + .../use_bool_derived_type/test_invalid.adb | 32 ++ .../use_bool_derived_type/test_task.adb | 38 ++ .../use_bool_derived_type/test_valid.adb | 25 ++ 9 files changed, 529 insertions(+), 42 deletions(-) create mode 100644 testsuite/tests/name_resolution/if_implicit_deref/test.adb create mode 100644 testsuite/tests/name_resolution/if_implicit_deref/test.out create mode 100644 testsuite/tests/name_resolution/if_implicit_deref/test.yaml create mode 100644 testsuite/tests/name_resolution/use_bool_derived_type/test.out create mode 100644 testsuite/tests/name_resolution/use_bool_derived_type/test.yaml create mode 100644 testsuite/tests/name_resolution/use_bool_derived_type/test_invalid.adb create mode 100644 testsuite/tests/name_resolution/use_bool_derived_type/test_task.adb create mode 100644 testsuite/tests/name_resolution/use_bool_derived_type/test_valid.adb diff --git a/ada/ast.py b/ada/ast.py index 744d5978c..572f54675 100644 --- a/ada/ast.py +++ b/ada/ast.py @@ -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(): @@ -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')) @@ -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() ), @@ -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"), @@ -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( @@ -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'), @@ -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()], @@ -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) ) @@ -16597,7 +16614,7 @@ 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() @@ -16605,7 +16622,7 @@ def contract_cases_assoc_equation(): ), 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]) @@ -17058,9 +17075,8 @@ 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 @@ -17068,9 +17084,8 @@ def xref_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 ) @@ -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( @@ -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) @@ -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() ) @@ -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() ), @@ -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 ) @@ -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 ) @@ -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 ) @@ -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() ) @@ -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 ) diff --git a/testsuite/tests/name_resolution/if_implicit_deref/test.adb b/testsuite/tests/name_resolution/if_implicit_deref/test.adb new file mode 100644 index 000000000..b332fb135 --- /dev/null +++ b/testsuite/tests/name_resolution/if_implicit_deref/test.adb @@ -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; diff --git a/testsuite/tests/name_resolution/if_implicit_deref/test.out b/testsuite/tests/name_resolution/if_implicit_deref/test.out new file mode 100644 index 000000000..5eca50655 --- /dev/null +++ b/testsuite/tests/name_resolution/if_implicit_deref/test.out @@ -0,0 +1,21 @@ +Analyzing test.adb +################## + +Resolving xrefs for node +**************************************************** + +Expr: + references: test().v + type: test().my_vectors.constant_reference_type + expected type: standard.boolean +Expr: + references: test().v + type: test().my_vectors.vector + expected type: None +Expr: + references: None + type: standard.universal_int_type_ + expected type: standard.positive + + +Done. diff --git a/testsuite/tests/name_resolution/if_implicit_deref/test.yaml b/testsuite/tests/name_resolution/if_implicit_deref/test.yaml new file mode 100644 index 000000000..173e325ff --- /dev/null +++ b/testsuite/tests/name_resolution/if_implicit_deref/test.yaml @@ -0,0 +1,2 @@ +driver: name-resolution +input_sources: [test.adb] diff --git a/testsuite/tests/name_resolution/use_bool_derived_type/test.out b/testsuite/tests/name_resolution/use_bool_derived_type/test.out new file mode 100644 index 000000000..f892bbf9b --- /dev/null +++ b/testsuite/tests/name_resolution/use_bool_derived_type/test.out @@ -0,0 +1,345 @@ +Analyzing test_valid.adb +######################## + +Resolving xrefs for node +*********************************************************** + + +Resolving xrefs for node +******************************************************************************* + +Expr: + references: + type: None + expected type: None + +Resolving xrefs for node +************************************************************************ + +Expr: + references: + type: None + expected type: None + +Resolving xrefs for node +******************************************************************* + +Expr: + references: + type: None + expected type: None + +Resolving xrefs for node +********************************************************** + +Expr: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: + type: + expected type: + +Resolving xrefs for node +*********************************************************** + + +Resolving xrefs for node +***************************************************************** + +Expr: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: + type: + expected type: + +Resolving xrefs for node +************************************************************* + + +Resolving xrefs for node +****************************************************************** + +Expr: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: + type: + expected type: + +Resolving xrefs for node +************************************************************* + + +Resolving xrefs for node +*************************************************************** + +Expr: + references: None + type: None + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: + type: + expected type: + +Resolving xrefs for node +*************************************************************** + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + type: + expected type: +Expr: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: + +Resolving xrefs for node +**************************************************************** + + +Resolving xrefs for node +**************************************************************** + +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: None + type: + expected type: + +Resolving xrefs for node +************************************************************* + +Expr: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: + type: + expected type: + +Resolving xrefs for node +************************************************************ + +Expr: + references: + type: None + expected type: None +Expr: + references: + type: None + expected type: None + + +Analyzing test_invalid.adb +########################## + +Resolving xrefs for node +************************************************************* + +Expr: + references: + type: None + expected type: None + +Resolving xrefs for node +************************************************************************** + +Expr: + references: + type: None + expected type: None + +Resolving xrefs for node +***************************************************************** + +Resolution failed for node + +Resolving xrefs for node +***************************************************************** + +Resolution failed for node + +Resolving xrefs for node +***************************************************************** + +Resolution failed for node + +Resolving xrefs for node +***************************************************************** + +Resolution failed for node + +Resolving xrefs for node +****************************************************************** + +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: None + type: + expected type: + +Resolving xrefs for node +************************************************************************* + +Resolution failed for node + +Resolving xrefs for node +*************************************************************** + + +Resolving xrefs for node +***************************************************************** + +Resolution failed for node + + +Analyzing test_task.adb +####################### + +Resolving xrefs for node +************************************************************** + +Expr: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: + type: + expected type: + +Resolving xrefs for node +********************************************************************* + +Resolution failed for node + + +Done. diff --git a/testsuite/tests/name_resolution/use_bool_derived_type/test.yaml b/testsuite/tests/name_resolution/use_bool_derived_type/test.yaml new file mode 100644 index 000000000..e164dadba --- /dev/null +++ b/testsuite/tests/name_resolution/use_bool_derived_type/test.yaml @@ -0,0 +1,2 @@ +driver: name-resolution +input_sources: [test_valid.adb, test_invalid.adb, test_task.adb] diff --git a/testsuite/tests/name_resolution/use_bool_derived_type/test_invalid.adb b/testsuite/tests/name_resolution/use_bool_derived_type/test_invalid.adb new file mode 100644 index 000000000..b5be6e434 --- /dev/null +++ b/testsuite/tests/name_resolution/use_bool_derived_type/test_invalid.adb @@ -0,0 +1,32 @@ +procedure Test_Invalid is + type My_Bool is new Boolean; + + -- Preconditions and contract aspects in general do not accept bool type + -- derivations, so nameres should fail. + function Foo (X, Y : My_Bool) return My_Bool is (X) + with Pre => X and not Y, + Contract_Cases => (X and not Y => X and not Y, + others => X and not Y); + pragma Test_Block; + + pragma Post (Foo, X and not Y); + pragma Test_Statement; + + procedure Bar is null; + + X, Y : My_Bool; + Z : Boolean; +begin + -- Only bool types are expected for the condition of a ``Debug`` pragma + pragma Debug (X or Y, Bar); + pragma Test_Statement; + + -- Iterator filters seem to only accept standard booleans + for K in 1 .. 3 when X and not Y loop + null; + end loop; + pragma Test_Block; + + Z := (for all K in 1 ..3 => X and not Y); + pragma Test_Statement; +end Test_Invalid; diff --git a/testsuite/tests/name_resolution/use_bool_derived_type/test_task.adb b/testsuite/tests/name_resolution/use_bool_derived_type/test_task.adb new file mode 100644 index 000000000..fb6f6ca01 --- /dev/null +++ b/testsuite/tests/name_resolution/use_bool_derived_type/test_task.adb @@ -0,0 +1,38 @@ +procedure Test_Task is + type My_Bool is new Boolean; + + task T is + entry E; + end T; + + task body T is + X, Y : My_Bool; + begin + -- This one is allowed + select when X and not Y => + accept E do + null; + end E; + or + terminate; + end select; + pragma Test_Statement; + end T; + + protected type P is + entry Foo; + private + X, Y : My_Bool; + end P; + + protected body P is + -- But this one is not allowed, only standard booleans are accepted + entry Foo when X and not Y is + begin + null; + end Foo; + pragma Test_Statement; + end P; +begin + null; +end Test_Task; diff --git a/testsuite/tests/name_resolution/use_bool_derived_type/test_valid.adb b/testsuite/tests/name_resolution/use_bool_derived_type/test_valid.adb new file mode 100644 index 000000000..1502c5677 --- /dev/null +++ b/testsuite/tests/name_resolution/use_bool_derived_type/test_valid.adb @@ -0,0 +1,25 @@ +procedure Test_Valid is + type My_Bool is new Boolean; + + X, Y : My_Bool; + Z : Integer; +begin + if X and not Y then + null; + elsif X or Y then + null; + end if; + + while X and Y loop + null; + end loop; + + pragma Assert (X or Y); + + Z := (if X and not Y then 1 else 2); + + for K in 1 .. 3 loop + exit when X and not Y; + end loop; +end Test_Valid; +pragma Test_Block;