Skip to content

Commit 5287bb7

Browse files
thvnxthvnx
committed
Merge branch 'mr/thevenoux/langkit-query-language#584' into 'master'
GNATkp: fix KP-19501 after KP description update Closes #584 See merge request eng/libadalang/langkit-query-language!585
2 parents 1d0b174 + 20a699a commit 5287bb7

File tree

5 files changed

+298
-79
lines changed

5 files changed

+298
-79
lines changed

‎lkql_checker/share/lkql/kp/kp_19501.lkql‎

Lines changed: 60 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -1,66 +1,87 @@
11
import stdlib
22

3-
fun is_static_int_attr(expr) =
3+
fun is_int_attr(expr) =
44
|" Returns whether the given expression is a universal-integer valued
5-
|" attribute reference known at compile time.
5+
|" attribute reference.
66
expr is AttributeRef
7-
when expr.p_expression_type() == expr.p_universal_int_type() and
8-
expr.p_is_static_expr()
7+
when expr.p_expression_type() == expr.p_universal_int_type()
98

10-
fun is_dynamic_subtyped_entity(name) =
11-
|" Returns whether the given name is a DefiningName and has a dynamic
12-
|" subtype.
9+
10+
fun is_subtype_indication_constrained(subtype_indication) =
11+
|" Return whether the provided SubtypeIndication is constrained.
1312
{
14-
val decl = match name
15-
| DefiningName => name.p_basic_decl()
16-
| Name => name.p_referenced_decl();
17-
decl is (ComponentDef | DiscriminantSpec | ObjectDecl | ParamSpec)
18-
when decl.f_type_expr is (SubtypeIndication)(
19-
p_is_statically_constrained(): false
13+
14+
fun is_constrained_subtype(type_decl) =
15+
|" Returns whether the provided BaseTypeDecl declares a constrained
16+
|" subtype.
17+
{
18+
(type_decl.p_has_aspect("Predicate")
19+
and not type_decl.p_is_statically_predicated())
20+
or type_decl.p_has_aspect("Dynamic_Predicate")
21+
or type_decl.p_full_view() is BaseTypeDecl when
22+
match type_decl
23+
| TypeDecl => (
24+
match type_decl.f_type_def
25+
| ArrayTypeDef(f_indices: ConstrainedArrayIndices) => true
26+
| d@DerivedTypeDef =>
27+
is_subtype_indication_constrained(
28+
d.f_subtype_indication
29+
)
30+
| * => false
31+
)
32+
| sd@SubtypeDecl =>
33+
is_subtype_indication_constrained(sd.f_subtype)
34+
};
35+
36+
subtype_indication.f_constraint is not null
37+
or is_constrained_subtype(
38+
subtype_indication.f_name.p_referenced_decl()
2039
)
2140
}
2241

23-
fun array_index_has_kp(expr, array_decl, child_n) =
24-
|" Returns whether the given array indexing expression contains an index
25-
|" being a reference to the ``Length`` attribute, while dimension bounds
26-
|" aren't static. Recurse on all indexing expr params starting from
27-
|" ``child_n``.
28-
match expr.f_suffix[child_n]?.f_r_expr
29-
| e when is_static_int_attr(e) =>
30-
if array_decl.f_type_expr.p_is_statically_constrained()
31-
then array_index_has_kp(expr, array_decl, child_n + 1)
32-
| null => false
33-
| * => array_index_has_kp(expr, array_decl, child_n + 1)
42+
43+
fun is_subject_to_constraint(name) =
44+
|" Returns whether the given name refers to a subtype subject to a
45+
|" constraint.
46+
{
47+
val decl = match name
48+
| DefiningName => name.p_basic_decl()
49+
| Name => name.p_referenced_decl();
50+
51+
match decl
52+
| (ComponentDef | DiscriminantSpec | ObjectDecl | ParamSpec) =>
53+
decl.f_type_expr is SubtypeIndication
54+
and is_subtype_indication_constrained(decl.f_type_expr)
55+
| SubtypeDecl => is_subtype_indication_constrained(decl.f_subtype)
56+
}
57+
3458

3559
@check(help="possible occurrence of KP 19501",
3660
message="possible occurrence of KP 19501")
3761
fun kp_19501(node) =
38-
|" Flag constructions involving an integer valued attribute reference known
39-
|" at compile time, when the attribute reference is:
62+
|" Flag constructions involving an integer valued attribute reference when
63+
|" the attribute reference is:
4064
|" * an actual parameter in a call where the subtype of the corresponding
4165
|" formal parameter is subject to a constraint
4266
|" * the expression of an assignment where the subtype of the target object
4367
|" is subject to a constraint
4468
|" * the operand of a qualified expression where the subtype mark
4569
|" denotes a subtype that is subject to a constraint
4670
|" * an array index value in an indexed component name
47-
|"
48-
|" Additionally, at least one of the bounds of the applicable constraint
49-
|" must be unknown at compile time.
5071
match node
5172
| CallExpr(p_is_call(): true) =>
5273
stdlib.any([
53-
is_static_int_attr(p.actual) and
54-
is_dynamic_subtyped_entity(p.param)
74+
is_int_attr(p.actual) and is_subject_to_constraint(p.param)
5575
for p in node.p_call_params()
5676
])
57-
| CallExpr(p_kind(): "array_index") =>
58-
array_index_has_kp(node, node.f_name.p_referenced_decl(), 1)
5977
| AssignStmt =>
60-
is_static_int_attr(node.f_expr) and
61-
is_dynamic_subtyped_entity(node.f_dest)
78+
is_int_attr(node.f_expr) and is_subject_to_constraint(node.f_dest)
6279
| QualExpr(f_suffix: ParenExpr(f_expr: operand)) =>
63-
is_static_int_attr(operand) and
64-
node.f_prefix is (Name)(
65-
p_name_designated_type(): BaseTypeDecl(p_is_statically_constrained(): false)
66-
)
80+
is_int_attr(operand)
81+
and node.f_prefix is Name
82+
and is_subject_to_constraint(node.f_prefix)
83+
| CallExpr(p_kind(): "array_index") =>
84+
stdlib.any([
85+
is_int_attr(p.f_r_expr)
86+
for p in node.f_suffix.children
87+
])

‎testsuite/tests/checks/KP-19501/main.adb‎

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -54,42 +54,42 @@ procedure Main is
5454
Dyn_Index : Dyn_Arr;
5555
Mult_Index : Multidim_Dyn_Arr;
5656

57-
Qual_Expr_1 : Stat_Int := Stat_Int'(C_S'Length); -- NOFLAG
58-
Qual_Expr_2 : Dyn_Int := Dyn_Int'(S'Length); -- NOFLAG
57+
Qual_Expr_1 : Stat_Int := Stat_Int'(C_S'Length); -- FLAG
58+
Qual_Expr_2 : Dyn_Int := Dyn_Int'(S'Length); -- FLAG
5959
Qual_Expr_3 : Dyn_Int := Dyn_Int'(C_S'Length); -- FLAG
60-
Qual_Expr_4 : Dyn_Int := Dyn_Int'(C_S'Size); -- NOFLAG
60+
Qual_Expr_4 : Dyn_Int := Dyn_Int'(C_S'Size); -- FLAG
6161
begin
6262
Process_Int (S'Length); -- NOFLAG
6363
Process_Int (C_S'Length); -- NOFLAG
64-
Process_Stat_Int (S'Length); -- NOFLAG
65-
Process_Stat_Int (C_S'Length); -- NOFLAG
66-
Process_Dyn_Int (S'Length); -- NOFLAG
64+
Process_Stat_Int (S'Length); -- FLAG
65+
Process_Stat_Int (C_S'Length); -- FLAG
66+
Process_Dyn_Int (S'Length); -- FLAG
6767
Process_Dyn_Int (C_S'Length); -- FLAG
68-
Process_Dyn_Int (C_S'Size); -- NOFLAG
68+
Process_Dyn_Int (C_S'Size); -- FLAG
6969
Process_Stat_Pred_Int (S'Length); -- NOFLAG
7070
Process_Stat_Pred_Int (C_S'Length); -- NOFLAG
71-
Process_Dyn_Pred_Int (S'Length); -- NOFLAG
71+
Process_Dyn_Pred_Int (S'Length); -- FLAG
7272
Process_Dyn_Pred_Int (C_S'Length); -- FLAG
73-
Process_Dyn_Pred_Int (C_S'Size); -- NOFLAG
73+
Process_Dyn_Pred_Int (C_S'Size); -- FLAG
7474

75-
Process_Multiple (S'Length, S'Size); -- NOFLAG
75+
Process_Multiple (S'Length, S'Size); -- FLAG
7676
Process_Multiple (C_S'Length, C_S'Size); -- FLAG
7777

78-
Stat_Assign := S'Length; -- NOFLAG
79-
Stat_Assign := C_S'Length; -- NOFLAG
80-
Dyn_Assign := S'Length; -- NOFLAG
78+
Stat_Assign := S'Length; -- FLAG
79+
Stat_Assign := C_S'Length; -- FLAG
80+
Dyn_Assign := S'Length; -- FLAG
8181
Dyn_Assign := C_S'Length; -- FLAG
82-
Dyn_Assign := C_S'Size; -- NOFLAG
82+
Dyn_Assign := C_S'Size; -- FLAG
8383

84-
Stat_Index (S'Length) := 10; -- NOFLAG
85-
Stat_Index (C_S'Length) := 10; -- NOFLAG
86-
Dyn_Index (S'Length) := 10; -- NOFLAG
84+
Stat_Index (S'Length) := 10; -- FLAG
85+
Stat_Index (C_S'Length) := 10; -- FLAG
86+
Dyn_Index (S'Length) := 10; -- FLAG
8787
Dyn_Index (C_S'Length) := 10; -- FLAG
88-
Dyn_Index (C_S'Size) := 10; -- NOFLAG
88+
Dyn_Index (C_S'Size) := 10; -- FLAG
8989
Dyn_Index (1) := 10; -- NOFLAG
90-
Mult_Index (1, S'Length) := 10; -- NOFLAG
90+
Mult_Index (1, S'Length) := 10; -- FLAG
9191
Mult_Index (1, C_S'Length) := 10; -- FLAG
92-
Mult_Index (1, C_S'Size) := 10; -- NOFLAG
92+
Mult_Index (1, C_S'Size) := 10; -- FLAG
9393
Mult_Index (C_S'Length, 1) := 10; -- FLAG
9494
Mult_Index (1, 1) := 10; -- NOFLAG
9595
end Main;

‎testsuite/tests/checks/KP-19501/main95.adb‎

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -56,42 +56,42 @@ procedure Main95 is
5656
Dyn_Index : Dyn_Arr;
5757
Mult_Index : Multidim_Dyn_Arr;
5858

59-
Qual_Expr_1 : Stat_Int := Stat_Int'(C_S'Length); -- NOFLAG
60-
Qual_Expr_2 : Dyn_Int := Dyn_Int'(S'Length); -- NOFLAG
59+
Qual_Expr_1 : Stat_Int := Stat_Int'(C_S'Length); -- FLAG
60+
Qual_Expr_2 : Dyn_Int := Dyn_Int'(S'Length); -- FLAG
6161
Qual_Expr_3 : Dyn_Int := Dyn_Int'(C_S'Length); -- FLAG
62-
Qual_Expr_4 : Dyn_Int := Dyn_Int'(C_S'Size); -- NOFLAG
62+
Qual_Expr_4 : Dyn_Int := Dyn_Int'(C_S'Size); -- FLAG
6363
begin
6464
Process_Int (S'Length); -- NOFLAG
6565
Process_Int (C_S'Length); -- NOFLAG
66-
Process_Stat_Int (S'Length); -- NOFLAG
67-
Process_Stat_Int (C_S'Length); -- NOFLAG
68-
Process_Dyn_Int (S'Length); -- NOFLAG
66+
Process_Stat_Int (S'Length); -- FLAG
67+
Process_Stat_Int (C_S'Length); -- FLAG
68+
Process_Dyn_Int (S'Length); -- FLAG
6969
Process_Dyn_Int (C_S'Length); -- FLAG
70-
Process_Dyn_Int (C_S'Size); -- NOFLAG
70+
Process_Dyn_Int (C_S'Size); -- FLAG
7171
Process_Stat_Pred_Int (S'Length); -- NOFLAG
7272
Process_Stat_Pred_Int (C_S'Length); -- NOFLAG
73-
Process_Dyn_Pred_Int (S'Length); -- NOFLAG
73+
Process_Dyn_Pred_Int (S'Length); -- FLAG
7474
Process_Dyn_Pred_Int (C_S'Length); -- FLAG
75-
Process_Dyn_Pred_Int (C_S'Size); -- NOFLAG
75+
Process_Dyn_Pred_Int (C_S'Size); -- FLAG
7676

77-
Process_Multiple (S'Length, S'Size); -- NOFLAG
77+
Process_Multiple (S'Length, S'Size); -- FLAG
7878
Process_Multiple (C_S'Length, C_S'Size); -- FLAG
7979

80-
Stat_Assign := S'Length; -- NOFLAG
81-
Stat_Assign := C_S'Length; -- NOFLAG
82-
Dyn_Assign := S'Length; -- NOFLAG
80+
Stat_Assign := S'Length; -- FLAG
81+
Stat_Assign := C_S'Length; -- FLAG
82+
Dyn_Assign := S'Length; -- FLAG
8383
Dyn_Assign := C_S'Length; -- FLAG
84-
Dyn_Assign := C_S'Size; -- NOFLAG
84+
Dyn_Assign := C_S'Size; -- FLAG
8585

86-
Stat_Index (S'Length) := 10; -- NOFLAG
87-
Stat_Index (C_S'Length) := 10; -- NOFLAG
88-
Dyn_Index (S'Length) := 10; -- NOFLAG
86+
Stat_Index (S'Length) := 10; -- FLAG
87+
Stat_Index (C_S'Length) := 10; -- FLAG
88+
Dyn_Index (S'Length) := 10; -- FLAG
8989
Dyn_Index (C_S'Length) := 10; -- FLAG
90-
Dyn_Index (C_S'Size) := 10; -- NOFLAG
90+
Dyn_Index (C_S'Size) := 10; -- FLAG
9191
Dyn_Index (1) := 10; -- NOFLAG
92-
Mult_Index (1, S'Length) := 10; -- NOFLAG
92+
Mult_Index (1, S'Length) := 10; -- FLAG
9393
Mult_Index (1, C_S'Length) := 10; -- FLAG
94-
Mult_Index (1, C_S'Size) := 10; -- NOFLAG
94+
Mult_Index (1, C_S'Size) := 10; -- FLAG
9595
Mult_Index (C_S'Length, 1) := 10; -- FLAG
9696
Mult_Index (1, 1) := 10; -- NOFLAG
9797
end Main95;

‎testsuite/tests/checks/KP-19501/test.adb‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
procedure Test is
2+
type Bit_T is range 0 .. 1;
3+
type Bits_T is array (Integer range <>) of Bit_T;
4+
5+
N_Array_Actual_Size_C : constant := 100;
6+
subtype Message_Length_T is Integer range 0 .. N_Array_Actual_Size_C;
7+
8+
function Get_Buffer return Bits_T is
9+
Buffer : constant Bits_T (0 .. N_Array_Actual_Size_C) := (others => 0);
10+
begin
11+
return Buffer;
12+
end Get_Buffer;
13+
14+
function Check_Length_Mes (Length : in Message_Length_T) return Message_Length_T is
15+
begin
16+
return Length;
17+
end Check_Length_Mes;
18+
19+
function Check_Length_Int (Length : in Integer) return Integer is
20+
begin
21+
return Length;
22+
end Check_Length_Int;
23+
24+
procedure Reproduce_Bug is
25+
Message : constant Bits_T := Get_Buffer;
26+
Length_Mes : Message_Length_T;
27+
Length_Int : Integer;
28+
begin
29+
Length_Mes := Check_Length_Mes (Message'Length); -- FLAG
30+
Length_Int := Check_Length_Int (Message'Length); -- NOFLAG
31+
end Reproduce_Bug;
32+
begin
33+
Reproduce_Bug;
34+
end Test;

0 commit comments

Comments
 (0)