Skip to content

Commit

Permalink
Merge branch 'topic/kp_19501' into 'master'
Browse files Browse the repository at this point in the history 
Update the KP-19501 detector

Closes #333

See merge request eng/libadalang/langkit-query-language!318
  • Loading branch information
@HugoGGuerrier
HugoGGuerrier committed Nov 28, 2024
2 parents 3a4d6ff + 2f50e0b commit 87103b6
Show file tree
Hide file tree
Showing 3 changed files with 114 additions and 40 deletions.
76 changes: 56 additions & 20 deletions lkql_checker/share/lkql/kp/KP-19501.lkql
View file
Original file line number Diff line number Diff line change
@@ -1,31 +1,67 @@
import stdlib

fun is_static_int_attr_ref(expr) =
|" Returns whether the given expression is an attribute reference which
|" value is a static (compilation known) universal integer.
fun is_static_int_attr(expr) =
|" Returns whether the given expression is a universal-integer valued
|" attribute reference known at compile time.
expr is AttributeRef
when expr.p_expression_type() == expr.p_universal_int_type()
and expr.p_is_static_expr()
when expr.p_expression_type() == expr.p_universal_int_type() and
expr.p_is_static_expr()

fun is_dynamic_subtype_formal(formal) =
|" Returns whether the given formal parameter DefiningName has a dynamic
fun is_dynamic_subtyped_entity(name) =
|" Returns whether the given name is a DefiningName and has a dynamic
|" subtype.
formal is DefiningName(p_basic_decl(): decl@BasicDecl)
when decl.f_type_expr is (SubtypeIndication | Name)(
p_is_static_subtype(): false
)
{
val decl = match name
| DefiningName => name.p_basic_decl()
| Name => name.p_referenced_decl();
decl is (ComponentDef | DiscriminantSpec | ObjectDecl | ParamSpec)
when decl.f_type_expr is (SubtypeIndication | Name)(
p_is_static_subtype(): false
)
}

fun array_index_has_kp(expr, array_decl, child_n) =
|" Returns whether the given array indexing expression contains an index
|" being a reference to the ``Length`` attribute, while dimension bounds
|" aren't static. Recurse on all indexing expr params starting from
|" ``child_n``.
match expr.f_suffix[child_n]?.f_r_expr
| e when is_static_int_attr(e) =>
if array_decl.f_type_expr.p_is_static_subtype()
then array_index_has_kp(expr, array_decl, child_n + 1)
| null => false
| * => array_index_has_kp(expr, array_decl, child_n + 1)

@check(help="possible occurrence of KP 19501",
message="possible occurrence of KP 19501",
impact="7.1.*,7.2.*,7.3.*,7.4.*,17.*,18.*,19.*,20.*,21.*,22.*,23.*,24.*")
fun kp_19501(node) =
|" Flag all call expressions which include at least one known problematic
|" formal/actual parameter pair.
node is CallExpr(p_is_call(): true)
when stdlib.any(
[
is_static_int_attr_ref(p.actual) and
is_dynamic_subtype_formal(p.param)
|" Flag constructions involving an integer valued attribute reference known
|" at compile time, when the attribute reference is:
|" * an actual parameter in a call where the subtype of the corresponding
|" formal parameter is subject to a constraint
|" * the expression of an assignment where the subtype of the target object
|" is subject to a constraint
|" * the operand of a qualified expression where the subtype mark
|" denotes a subtype that is subject to a constraint
|" * an array index value in an indexed component name
|"
|" Additionally, at least one of the bounds of the applicable constraint
|" must be unknown at compile time.
match node
| CallExpr(p_is_call(): true) =>
stdlib.any([
is_static_int_attr(p.actual) and
is_dynamic_subtyped_entity(p.param)
for p in node.p_call_params()
]
)
])
| CallExpr(p_kind(): "array_index") =>
array_index_has_kp(node, node.f_name.p_referenced_decl(), 1)
| AssignStmt =>
is_static_int_attr(node.f_expr) and
is_dynamic_subtyped_entity(node.f_dest)
| QualExpr(f_suffix: ParenExpr(f_expr: operand)) =>
is_static_int_attr(operand) and
node.f_prefix is (SubtypeIndication | Name)(
p_is_static_subtype(): false
)
54 changes: 36 additions & 18 deletions testsuite/tests/checks/KP-19501/main.adb
View file
Original file line number Diff line number Diff line change
@@ -1,20 +1,16 @@
procedure Main is
function Id (B : Boolean) return Boolean is (B);
function Id (I : Integer) return Integer is (I);

type Rec (D : Boolean) is null record;
subtype Stat_Const_Rec is Rec (True);
subtype Dyn_Const_Rec is Rec (Id (True));

type Arr is array (Integer range <>) of Integer;
subtype Stat_Const_Arr is Arr (1 .. 3);
subtype Dyn_Const_Arr is Arr (1 .. Id (3));
subtype Stat_Arr is Arr (1 .. 10);
subtype Dyn_Arr is Arr (1 .. Id (10));
type Multidim_Dyn_Arr is array (1 .. 10, 1 .. Id (10)) of Integer;

subtype Stat_Int is Integer range 1 .. 3;
subtype Dyn_Int is Integer range Id (1) .. Id (3);
subtype Stat_Int is Integer range 1 .. 10;
subtype Dyn_Int is Integer range Id (1) .. Id (10);

subtype Stat_Pred_Int is Integer
with Static_Predicate => Stat_Pred_Int in 1 .. 5;
with Static_Predicate => Stat_Pred_Int in 1 .. 10;
subtype Dyn_Pred_Int is Integer
with Dynamic_Predicate => Dyn_Pred_Int < 50;

Expand Down Expand Up @@ -50,28 +46,50 @@ procedure Main is
begin
null;
end Process_Multiple;

Stat_Assign : Stat_Int;
Dyn_Assign : Dyn_Int;

Stat_Index : Stat_Arr;
Dyn_Index : Dyn_Arr;
Mult_Index : Multidim_Dyn_Arr;

Qual_Expr_1 : Stat_Int := Stat_Int'(C_S'Length); -- NOFLAG
Qual_Expr_2 : Dyn_Int := Dyn_Int'(S'Length); -- NOFLAG
Qual_Expr_3 : Dyn_Int := Dyn_Int'(C_S'Length); -- FLAG
Qual_Expr_4 : Dyn_Int := Dyn_Int'(C_S'Size); -- NOFLAG
begin
Process_Int (S'Length); -- NOFLAG
Process_Int (S'Size); -- NOFLAG
Process_Int (C_S'Length); -- NOFLAG
Process_Int (C_S'Size); -- NOFLAG
Process_Stat_Int (S'Length); -- NOFLAG
Process_Stat_Int (S'Size); -- NOFLAG
Process_Stat_Int (C_S'Length); -- NOFLAG
Process_Stat_Int (C_S'Size); -- NOFLAG
Process_Dyn_Int (S'Length); -- NOFLAG
Process_Dyn_Int (S'Size); -- NOFLAG
Process_Dyn_Int (C_S'Length); -- FLAG
Process_Dyn_Int (C_S'Size); -- NOFLAG
Process_Stat_Pred_Int (S'Length); -- NOFLAG
Process_Stat_Pred_Int (S'Size); -- NOFLAG
Process_Stat_Pred_Int (C_S'Length); -- NOFLAG
Process_Stat_Pred_Int (C_S'Size); -- NOFLAG
Process_Dyn_Pred_Int (S'Length); -- NOFLAG
Process_Dyn_Pred_Int (S'Size); -- NOFLAG
Process_Dyn_Pred_Int (C_S'Length); -- FLAG
Process_Dyn_Pred_Int (C_S'Size); -- NOFLAG

Process_Multiple (S'Length, S'Size); -- NOFLAG
Process_Multiple (C_S'Length, C_S'Size); -- FLAG

Stat_Assign := S'Length; -- NOFLAG
Stat_Assign := C_S'Length; -- NOFLAG
Dyn_Assign := S'Length; -- NOFLAG
Dyn_Assign := C_S'Length; -- FLAG
Dyn_Assign := C_S'Size; -- NOFLAG

Stat_Index (S'Length) := 10; -- NOFLAG
Stat_Index (C_S'Length) := 10; -- NOFLAG
Dyn_Index (S'Length) := 10; -- NOFLAG
Dyn_Index (C_S'Length) := 10; -- FLAG
Dyn_Index (C_S'Size) := 10; -- NOFLAG
Dyn_Index (1) := 10; -- NOFLAG
Mult_Index (1, S'Length) := 10; -- NOFLAG
Mult_Index (1, C_S'Length) := 10; -- FLAG
Mult_Index (1, C_S'Size) := 10; -- NOFLAG
Mult_Index (C_S'Length, 1) := 10; -- FLAG
Mult_Index (1, 1) := 10; -- NOFLAG
end Main;
24 changes: 22 additions & 2 deletions testsuite/tests/checks/KP-19501/test.out
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,9 @@
main.adb:64:4: rule violation: possible occurrence of KP 19501
64 | Process_Dyn_Int (C_S'Length); -- FLAG
main.adb:59:29: rule violation: possible occurrence of KP 19501
59 | Qual_Expr_3 : Dyn_Int := Dyn_Int'(C_S'Length); -- FLAG
| ^^^^^^^^^^^^^^^^^^^^

main.adb:67:4: rule violation: possible occurrence of KP 19501
67 | Process_Dyn_Int (C_S'Length); -- FLAG
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

main.adb:72:4: rule violation: possible occurrence of KP 19501
Expand All @@ -10,3 +14,19 @@ main.adb:76:4: rule violation: possible occurrence of KP 19501
76 | Process_Multiple (C_S'Length, C_S'Size); -- FLAG
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

main.adb:81:4: rule violation: possible occurrence of KP 19501
81 | Dyn_Assign := C_S'Length; -- FLAG
| ^^^^^^^^^^^^^^^^^^^^^^^^^^

main.adb:87:4: rule violation: possible occurrence of KP 19501
87 | Dyn_Index (C_S'Length) := 10; -- FLAG
| ^^^^^^^^^^^^^^^^^^^^^^

main.adb:91:4: rule violation: possible occurrence of KP 19501
91 | Mult_Index (1, C_S'Length) := 10; -- FLAG
| ^^^^^^^^^^^^^^^^^^^^^^^^^^

main.adb:93:4: rule violation: possible occurrence of KP 19501
93 | Mult_Index (C_S'Length, 1) := 10; -- FLAG
| ^^^^^^^^^^^^^^^^^^^^^^^^^^

0 comments on commit 87103b6

Please sign in to comment.