diff --git a/ada/ast.py b/ada/ast.py index 8d6f2065c..6c752e220 100644 --- a/ada/ast.py +++ b/ada/ast.py @@ -6231,40 +6231,6 @@ def derefed_base_subtype(): ).base_subtype ) - @langkit_property(return_type=Bool) - def one_non_universal(second=T.BaseTypeDecl.entity): - return Or( - Not(Entity.is_null) & Entity.is_not_universal_type, - Not(second.is_null) & second.is_not_universal_type - ) - - @langkit_property(return_type=T.BaseTypeDecl.entity, - dynamic_vars=[default_origin()]) - def non_universal_base_subtype(second=T.BaseTypeDecl.entity): - first_ok = Var(Not(Entity.is_null) & Entity.is_not_universal_type) - second_ok = Var(Not(second.is_null) & second.is_not_universal_type) - return Cond( - first_ok & second_ok, - Let( - lambda - first_st=Entity.derefed_base_subtype, - second_st=second.derefed_base_subtype: - If( - second_st.matching_formal_type(first_st), - first_st, - second_st - ) - ), - - first_ok, - Entity.derefed_base_subtype, - - second_ok, - second.derefed_base_subtype, - - No(BaseTypeDecl.entity) - ) - @langkit_property(return_type=T.BaseTypeDecl.entity, dynamic_vars=[default_origin()]) def array_concat_result_type(other=T.BaseTypeDecl.entity): @@ -13005,18 +12971,18 @@ def double_dot_equation(): Predicate(AdaNode.is_not_null, Self.expected_type_var), Bind(Self.expected_type_var, Self.type_var), Bind(Self.type_var, Self.left.expected_type_var), - Bind(Self.type_var, Self.right.expected_type_var) - ) & Or( - # Expected type was given explicitly, so we can simply check that - # the type inferred for the operands matches. This is generally - # the case for ranges in component representation clauses or - # in subtype indications' constraints. - Self.left.matches_expected_formal_type - & Self.right.matches_expected_formal_type, - - # Expected was not given explicitly, so we must infer it here. - # This is generally the case for ranges in for loop specs. - Entity.numeric_type_from_operands_equation(Self.type_var) + Bind(Self.type_var, Self.right.expected_type_var), + Self.left.matches_expected_formal_type, + Self.right.matches_expected_formal_type + ) & Self.use_expected_type_or( + # In some cases the expected type is given explicitly, so we can + # simply check that the type inferred for the operands matches. + # This is generally the case for ranges in component representation + # clauses or in subtype indications' constraints. + # However if the expected is not given explicitly, we must infer + # it here from one of the operands. This is generally the case + # for ranges in for-loop specs. + Entity.infer_from_either_operands(Self.type_var) ) @langkit_property(dynamic_vars=[origin]) @@ -13075,107 +13041,122 @@ def no_overload_equation(): to construct the xref equation for this node. """ return Cond( - # For multiplication operators, we must handle the general shape - # `function "op" (X, Y : T) return T`, but also the shape - # `function "op" (X : Integer, Y : T) return T` as well as - # `function "op" (X : T, Y : Integer) return T`. + # For multiplication operators, we must handle three shapes Self.op.is_a(Op.alt_mult, Op.alt_div), Or( + # `function "op" (X, Y : T) return T` Bind(Self.type_var, Self.left.expected_type_var) - & Bind(Self.type_var, Self.right.expected_type_var), + & Bind(Self.type_var, Self.right.expected_type_var) + & Self.use_expected_type_or( + Entity.infer_from_either_operands(Self.type_var) + ), + # `function "op" (X : Integer, Y : T) return T` Bind(Self.left.expected_type_var, Self.int_type) - & Bind(Self.right.expected_type_var, Self.type_var), + & Bind(Self.right.expected_type_var, Self.type_var) + & Self.use_expected_type_or( + Entity.infer_from_right_operand(Self.type_var) + ), + # `function "op" (X : T, Y : Integer) return T` Bind(Self.right.expected_type_var, Self.int_type) - & Bind(Self.left.expected_type_var, Self.type_var), + & Bind(Self.left.expected_type_var, Self.type_var) + & Self.use_expected_type_or( + Entity.infer_from_left_operand(Self.type_var) + ) ), # For power operators, we must only handle the shape # `function "op" (X : T, Y : Integer) return T`. Self.op.is_a(Op.alt_pow), Bind(Self.right.expected_type_var, Self.int_type) - & Bind(Self.left.expected_type_var, Self.type_var), + & Bind(Self.left.expected_type_var, Self.type_var) + & Self.use_expected_type_or( + Entity.infer_from_left_operand(Self.type_var) + ), # For other operators, we only need to handle the shape # `function "op" (X, Y : T) return T`. - And( - Bind(Self.type_var, Self.left.expected_type_var), - Bind(Self.type_var, Self.right.expected_type_var) + Bind(Self.type_var, Self.left.expected_type_var) + & Bind(Self.type_var, Self.right.expected_type_var) + & Self.use_expected_type_or( + Entity.infer_from_either_operands(Self.type_var) ) ) & Or( - # If the expected type is known, use it to infer the type of Self. - # This will allow Self's type to be used in the next disjunction to - # infer the type of the operands if necessary. + # We have an expected type: we can directly infer the actual type + # of the result, and of the operands using the equations above. + # Note that there is a difference between not having an expected + # type at all (as in a type conversion), and having an expected + # type but not inferrable from the context (as in an operand of a + # comparison operator `(A + B) = 2`. The latter simply means + # that the expected type itself will be inferred from the operands + # using one of `Entity.infer_from_*` properties. Predicate(AdaNode.is_not_null, Self.expected_type_var) & Bind(Self.expected_type_var, Self.type_var, conv_prop=BaseTypeDecl.derefed_base_subtype), - # Otherwise, we cannot infer the type of Self from its expected - # type, so we will infer it from one of the operands, since at - # least one of them necessarily has a context-free type (otherwise - # this wouldn't be valid Ada code). + # There is no expected type (e.g. we are in a type conversion). + # In this case, the type of the result will be inferred from the + # type of operands: we know that at least one of them has a + # context-free type (otherwise this wouldn't be valid Ada code). Bind(Self.expected_type_var, No(BaseTypeDecl.entity)) - ) & Or( - # If the expected is known, it was assigned to the type of Self, - # there might be nothing more to do. - Predicate(AdaNode.is_not_null, Self.expected_type_var) - & Self.left.matches_expected_formal_type - & Self.right.matches_expected_formal_type, - - # If we're trying the following option, it means we must infer - # Self's type from one of the operands. We assign it to the first - # one that is *not* a universal type (the result of a binary - # operation cannot be a universal type). - Entity.numeric_type_from_operands_equation(Self.type_var) + ) & And( + Self.left.matches_expected_formal_type, + Self.right.matches_expected_formal_type ) + @langkit_property(return_type=Equation) + def use_expected_type_or(eq=T.Equation): + """ + Construct the xref equation that first attempts to resolve this binary + operation using the expected type given by the context only, and then + by using the additional equation given as argument (typically this + equation will try to infer the type from one of the operands). + """ + return Predicate(AdaNode.is_not_null, Self.expected_type_var) | eq + @langkit_property(return_type=Equation, dynamic_vars=[origin]) - def numeric_type_from_operands_equation(dest_var=T.LogicVar): + def infer_from_left_operand(dest_var=T.LogicVar): """ Construct the xref equation that must bind the given variable to the type of this binary operation's operands, assuming we are dealing with - numeric types and arithmetic operators. + numeric types and arithmetic operators with the following profile: + ``function "op" (X : T, Y : U) return T`` (we want to infer ``T``). """ - left_ctx_free = Var(Self.left.has_context_free_type) - right_ctx_free = Var(Self.right.has_context_free_type) - return If( - # If both operands have a context free type, we can use an - # N-Propagate equation to assign `dest_var` because we know for - # sure that Self.left.type_var and Self.right.type_var will be - # given a value explicitly. - left_ctx_free & right_ctx_free, - - Predicate(BaseTypeDecl.one_non_universal, - Self.left.type_var, Self.right.type_var) - & NPropagate(dest_var, - BaseTypeDecl.non_universal_base_subtype, - Self.left.type_var, Self.right.type_var) - & Self.left.matches_expected_formal_type - & Self.right.matches_expected_formal_type, + return And( + Predicate(BaseTypeDecl.is_not_universal_type, + Self.left.type_var), + Bind(Self.left.type_var, dest_var, + conv_prop=BaseTypeDecl.derefed_base_subtype), + ) - Let( - lambda - infer_left=Predicate(BaseTypeDecl.is_not_universal_type, - Self.left.type_var) - & Bind(Self.left.type_var, dest_var, - conv_prop=BaseTypeDecl.derefed_base_subtype) - & Self.left.matches_expected_formal_type - & Self.right.matches_expected_formal_type, - - infer_right=Predicate(BaseTypeDecl.is_not_universal_type, - Self.right.type_var) - & Bind(Self.right.type_var, dest_var, - conv_prop=BaseTypeDecl.derefed_base_subtype) - & Self.left.matches_expected_formal_type - & Self.right.matches_expected_formal_type: - - If(left_ctx_free, - infer_left | infer_right, - infer_right | infer_left) - ) + @langkit_property(return_type=Equation, dynamic_vars=[origin]) + def infer_from_right_operand(dest_var=T.LogicVar): + """ + Construct the xref equation that must bind the given variable to the + type of this binary operation's operands, assuming we are dealing with + numeric types and arithmetic operators with the following profile: + ``function "op" (X : U, Y : T) return T`` (we want to infer ``T``). + """ + return And( + Predicate(BaseTypeDecl.is_not_universal_type, + Self.right.type_var), + Bind(Self.right.type_var, dest_var, + conv_prop=BaseTypeDecl.derefed_base_subtype), ) + @langkit_property(return_type=Equation, dynamic_vars=[origin]) + def infer_from_either_operands(dest_var=T.LogicVar): + """ + Construct the xref equation that must bind the given variable to the + type of this binary operation's operands, assuming we are dealing with + numeric types and arithmetic operators with the following profile: + ``function "op" (X, Y : T) return T`` (we want to infer ``T``). + """ + infer_left = Var(Entity.infer_from_left_operand(dest_var)) + infer_right = Var(Entity.infer_from_right_operand(dest_var)) + return infer_left | infer_right + @langkit_property() def potential_actuals_for_dispatch(spec=T.BaseSubpSpec.entity): params = Var(spec.unpacked_formal_params) @@ -13508,9 +13489,11 @@ class RelationOp(BinOp): no_overload_equation = Property( Bind(Self.type_var, Self.bool_type) & Bind(Self.left.expected_type_var, Self.right.expected_type_var) - & Entity.numeric_type_from_operands_equation( + & Entity.infer_from_either_operands( Self.left.expected_type_var ) + & Self.left.matches_expected_formal_type + & Self.right.matches_expected_formal_type ) @@ -17923,11 +17906,16 @@ def subprograms_for_symbol(sym=T.Symbol, from_node=T.AdaNode.entity): lambda e: And( e.cast_or_raise(T.BasicDecl).is_subprogram, - # Note: we do not use synthesized operators for BinOp/UnOp - # resolution for now as it introduces a significant performance - # regression. - - # TODO: retry when new solver is available + # Note: here we explicitly filter out synthesized operators + # (which correspond to built-in operators), because using them + # for resolving arithmetic expressions would have a significant + # performance impact. Instead, we use specific equations + # tailored for the resolution of built-in operators. See + # `BinOp.no_overload_equation`. + # TODO: However these custom rules currently do not assign the + # `ref_var` of operator references designating which built-in + # operators have been called, which would be useful for users + # and make this more transparent. Not(e.is_a(SyntheticSubpDecl)) ) )) diff --git a/testsuite/tests/name_resolution/operators_17/test.adb b/testsuite/tests/name_resolution/operators_17/test.adb new file mode 100644 index 000000000..7e7d5abfc --- /dev/null +++ b/testsuite/tests/name_resolution/operators_17/test.adb @@ -0,0 +1,13 @@ +procedure Test is + type T is delta 0.1 range -10.0 .. 10.0; + + X : T := 2.0; + B : Boolean; + I : Integer := Integer (2 * X); + pragma Test_Statement; +begin + B := X * Integer'(2) = 4.0; + pragma Test_Statement; + B := Integer'(2) * X = 4.0; + pragma Test_Statement; +end Test; diff --git a/testsuite/tests/name_resolution/operators_17/test.out b/testsuite/tests/name_resolution/operators_17/test.out new file mode 100644 index 000000000..9f2a6cd40 --- /dev/null +++ b/testsuite/tests/name_resolution/operators_17/test.out @@ -0,0 +1,126 @@ +Analyzing test.adb +################## + +Resolving xrefs for node +************************************************************* + +Expr: + references: + type: None + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: None +Expr: + references: None + 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: + references: + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: None + expected type: None +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + expected type: + +Resolving xrefs for node +********************************************************* + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: None + expected type: None +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: + type: + expected type: +Expr: + expected type: + + +Done. diff --git a/testsuite/tests/name_resolution/operators_17/test.yaml b/testsuite/tests/name_resolution/operators_17/test.yaml new file mode 100644 index 000000000..173e325ff --- /dev/null +++ b/testsuite/tests/name_resolution/operators_17/test.yaml @@ -0,0 +1,2 @@ +driver: name-resolution +input_sources: [test.adb] diff --git a/testsuite/tests/name_resolution/pow_op/test.out b/testsuite/tests/name_resolution/pow_op/test.out index 3c421125f..6abafa7fe 100644 --- a/testsuite/tests/name_resolution/pow_op/test.out +++ b/testsuite/tests/name_resolution/pow_op/test.out @@ -24,5 +24,164 @@ Expr: type: expected type: +Resolving xrefs for node +****************************************************************** + +Expr: + references: + type: None + expected type: None +Expr: + type: + expected type: +Expr: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: None + expected type: None +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: None + expected type: None +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + expected type: + +Resolving xrefs for node +****************************************************************** + +Expr: + references: + type: None + expected type: None +Expr: + type: + expected type: +Expr: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: None + expected type: None +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: None + expected type: None +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: + references: + type: None + expected type: None +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: + type: None + expected type: None +Expr: + references: + type: None + expected type: None +Expr: + references: None + type: None + expected type: None +Expr: + references: None + type: None + expected type: None +Expr: + references: None + type: None + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: + Done. diff --git a/testsuite/tests/name_resolution/pow_op/testexp.adb b/testsuite/tests/name_resolution/pow_op/testexp.adb index 4ff19fb39..6d76e3a57 100644 --- a/testsuite/tests/name_resolution/pow_op/testexp.adb +++ b/testsuite/tests/name_resolution/pow_op/testexp.adb @@ -1,6 +1,21 @@ procedure Testexp is A : Float := 12412335125.99 ** 2; pragma Test_Statement; + + type My_Int is range -1000 .. 1000; + + function Ident_Int (X : Integer) return Integer is (X); + -- Used in expressions below to make them non-static and avoid GNAT + -- from rejected programs that it can prove would raise Constraint_Errors. + + B : Boolean := My_Int'(3) ** Integer'(4) <= 100; + pragma Test_Statement; + + C : Boolean := Float'(2.0) ** Integer'(3) /= 8.0; + pragma Test_Statement; + + D : Float := Float'Base'Last ** Ident_Int (2); + pragma Test_Statement; begin null; end Testexp;