Skip to content

Commit 47197ef

Browse files
thvnxthvnx
committed
Merge branch 'topic/395' into 'master'
Add detector for KP 19626 Closes #395 See merge request eng/libadalang/langkit-query-language!407
2 parents 8a39008 + e3dfd4e commit 47197ef

File tree

10 files changed

+152
-6
lines changed

10 files changed

+152
-6
lines changed

‎lkql_checker/share/lkql/kp/KP-19279.lkql

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ fun contains_dynamic_bounds(agg) =
2323
not tn.p_is_static_subtype()
2424
| n@Name =>
2525
n.p_referenced_decl()?.p_type_expression() is SubtypeIndication(
26-
p_is_static_subtype(): false
26+
p_is_statically_constrained(): false
2727
)
2828
)
2929
| Name(p_name_designated_type(): not null) =>

‎lkql_checker/share/lkql/kp/KP-19501.lkql

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@ fun is_dynamic_subtyped_entity(name) =
1515
| DefiningName => name.p_basic_decl()
1616
| Name => name.p_referenced_decl();
1717
decl is (ComponentDef | DiscriminantSpec | ObjectDecl | ParamSpec)
18-
when decl.f_type_expr is (SubtypeIndication | Name)(
19-
p_is_static_subtype(): false
18+
when decl.f_type_expr is (SubtypeIndication)(
19+
p_is_statically_constrained(): false
2020
)
2121
}
2222

@@ -27,7 +27,7 @@ fun array_index_has_kp(expr, array_decl, child_n) =
2727
|" ``child_n``.
2828
match expr.f_suffix[child_n]?.f_r_expr
2929
| e when is_static_int_attr(e) =>
30-
if array_decl.f_type_expr.p_is_static_subtype()
30+
if array_decl.f_type_expr.p_is_statically_constrained()
3131
then array_index_has_kp(expr, array_decl, child_n + 1)
3232
| null => false
3333
| * => array_index_has_kp(expr, array_decl, child_n + 1)
@@ -61,6 +61,6 @@ fun kp_19501(node) =
6161
is_dynamic_subtyped_entity(node.f_dest)
6262
| QualExpr(f_suffix: ParenExpr(f_expr: operand)) =>
6363
is_static_int_attr(operand) and
64-
node.f_prefix is (SubtypeIndication | Name)(
65-
p_is_static_subtype(): false
64+
node.f_prefix is (Name)(
65+
p_name_designated_type(): BaseTypeDecl(p_is_statically_constrained(): false)
6666
)

‎lkql_checker/share/lkql/kp/KP-19625.lkql

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
fun indexed_function_result_has_nonstatic_size(subprogram) = {
2+
# To determine if a function is indexed, check that its return
3+
# type has the Constant_Indexing user-defined aspect.
4+
val returns = subprogram.f_subp_spec.p_returns();
5+
match returns.p_designated_type_decl()
6+
| t@BaseTypeDecl => t.p_has_aspect("Constant_Indexing")
7+
and not returns.p_is_statically_constrained()
8+
| * => false
9+
}
10+
11+
@check(help="possible occurrence of KP 19625",
12+
message="possible occurrence of KP 19625")
13+
fun kp_19625(node) =
14+
# Look for a generalized indexing directly applied to the result of a
15+
# function call when the indexed function result has a nonstatic size.
16+
node is CallExpr(
17+
f_name: CallExpr(p_is_call(): true),
18+
p_kind(): "array_index"
19+
)
20+
when indexed_function_result_has_nonstatic_size(
21+
node.f_name.p_referenced_decl()
22+
)

‎lkql_checker/share/lkql/kp/kp.json

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@
2020
"kp_19447": "24.*",
2121
"kp_19501": "7.1.*,7.2.*,7.3.*,7.4.*,17.*,18.*,19.*,20.*,21.*,22.*,23.*,24.*",
2222
"kp_19529": "24.*",
23+
"kp_19625": "24.*",
2324
"kp_19696": "24.*,25.1",
2425
"kp_ob03_009": "19.*",
2526
"kp_p226_024": "7.1.*,7.2.*,7.3.*,7.4.1,7.4.2,7.4.3",

‎testsuite/tests/checks/KP-19625/bounded_vector_return_issue.adb

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
with Ada.Exceptions;
2+
with GNAT.Traceback.Symbolic;
3+
with GNAT.Compiler_Version;
4+
with Ada.Text_IO;
5+
6+
with Ada.Containers.Bounded_Vectors;
7+
8+
with Ada.Command_Line;
9+
10+
procedure Bounded_Vector_Return_Issue is
11+
12+
package V is new
13+
Ada.Containers.Bounded_Vectors
14+
(Index_Type => Positive,
15+
Element_Type => Integer);
16+
Size : constant Positive :=
17+
(if Ada.Command_Line.Argument_Count >= 1
18+
then Positive'Value (Ada.Command_Line.Argument (1))
19+
else 10);
20+
21+
subtype Bounded_Vector is V.Vector (Ada.Containers.Count_Type (Size));
22+
use type Bounded_Vector;
23+
24+
package Bounded_Vector_Sort is new V.Generic_Sorting;
25+
26+
function Sort (X : Bounded_Vector) return Bounded_Vector is
27+
R : V.Vector := X;
28+
begin
29+
Bounded_Vector_Sort.Sort (R);
30+
return R;
31+
end Sort;
32+
33+
procedure Process is
34+
35+
V : Bounded_Vector;
36+
37+
begin
38+
39+
V.Append (1);
40+
V.Append (2);
41+
V.Append (3);
42+
V.Append (4);
43+
V.Append (5);
44+
45+
declare
46+
Middle : Positive := (Positive (V.Length) - 1) / 2 + 1;
47+
V_Sorted : Bounded_Vector := Sort (V);
48+
Median : Integer := V_Sorted (Middle); -- NO FLAG
49+
begin
50+
Ada.Text_IO.Put_Line ("Median " & Median'Img);
51+
end;
52+
53+
declare
54+
Middle : Positive := (Positive (V.Length) - 1) / 2 + 1;
55+
Median : Integer := Sort (V) (Middle); -- FLAG
56+
begin
57+
Ada.Text_IO.Put_Line ("Median " & Median'Img);
58+
end;
59+
end Process;
60+
61+
package C_Version is new GNAT.Compiler_Version;
62+
begin
63+
Ada.Text_IO.Put_Line ("Compiler_Version :" & C_Version.Version);
64+
Process;
65+
exception
66+
when Error : others =>
67+
Ada.Text_IO.Put_Line
68+
("Main :exception raised " & Ada.Exceptions.Exception_Message (Error));
69+
Ada.Text_IO.Put_Line (Ada.Exceptions.Exception_Information (Error));
70+
Ada.Text_IO.Put_Line
71+
(GNAT.Traceback.Symbolic.Symbolic_Traceback (Error));
72+
end;

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

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
procedure Main (Arg : Integer) is
2+
3+
package Container is
4+
type Arr is array (Natural range <>) of Float;
5+
6+
type Vector (X : Integer) is tagged record
7+
Content : Arr (1 .. X);
8+
end record
9+
with Constant_Indexing => Constant_Reference;
10+
11+
function Constant_Reference (V : Vector; Pos : Integer) return Float
12+
is (V.Content (Pos));
13+
end Container;
14+
15+
subtype S1 is Container.Vector (Arg);
16+
subtype S2 is Container.Vector (3);
17+
18+
V : S1;
19+
20+
function Ident1 (X : S1) return S1
21+
is (X);
22+
23+
W : S2;
24+
25+
function Ident2 (X : S2) return S2
26+
is (X);
27+
28+
Res : Float;
29+
30+
begin
31+
V := (Arg, (others => 1.0));
32+
Res := Ident1 (V) (4); -- FLAG
33+
34+
W := (3, (1.0, 2.0, 3.0));
35+
Res := Ident2 (W) (4); -- NO FLAG
36+
end Main;

‎testsuite/tests/checks/KP-19625/prj.gpr

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
project Prj is
2+
end Prj;

‎testsuite/tests/checks/KP-19625/test.out

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
bounded_vector_return_issue.adb:55:30: rule violation: possible occurrence of KP 19625
2+
55 | Median : Integer := Sort (V) (Middle); -- FLAG
3+
| ^^^^^^^^^^^^^^^^^
4+
5+
main.adb:32:11: rule violation: possible occurrence of KP 19625
6+
32 | Res := Ident1 (V) (4); -- FLAG
7+
| ^^^^^^^^^^^^^^
8+

‎testsuite/tests/checks/KP-19625/test.yaml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
driver: checker
2+
rule_name: kp_19625
3+
project: prj.gpr

‎testsuite/tests/gnatcheck/xml_help/test.out

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -86,6 +86,7 @@ testsuite_driver: No output file generated by gnatcheck
8686
<check switch="+Rkp_19447" label="possible occurrence of KP 19447"/>
8787
<check switch="+Rkp_19501" label="possible occurrence of KP 19501"/>
8888
<check switch="+Rkp_19529" label="possible occurrence of KP 19529"/>
89+
<check switch="+Rkp_19625" label="possible occurrence of KP 19625"/>
8990
<check switch="+Rkp_19696" label="possible occurrence of KP 19696"/>
9091
<check switch="+Rkp_ob03_009" label="possible occurrence of KP OB03-009"/>
9192
<check switch="+Rkp_p226_024" label="possible occurrence of KP P226-024 - global analysis required"/>
@@ -595,6 +596,7 @@ testsuite_driver: No output file generated by gnatcheck
595596
<check switch="+Rkp_19447" label="possible occurrence of KP 19447"/>
596597
<check switch="+Rkp_19501" label="possible occurrence of KP 19501"/>
597598
<check switch="+Rkp_19529" label="possible occurrence of KP 19529"/>
599+
<check switch="+Rkp_19625" label="possible occurrence of KP 19625"/>
598600
<check switch="+Rkp_19696" label="possible occurrence of KP 19696"/>
599601
<check switch="+Rkp_ob03_009" label="possible occurrence of KP OB03-009"/>
600602
<check switch="+Rkp_p226_024" label="possible occurrence of KP P226-024 - global analysis required"/>

0 commit comments

Comments
 (0)