AdaCore / langkit-query-language

query language for Libadalang and Langkit
Other
3 stars 6 forks source link

integer_types_as_enum: missing case #56

Open Heziode opened 1 year ago

Heziode commented 1 year ago

Context

In the following exemple:

https://github.com/AdaCore/langkit-query-language/blob/75cec794bacac95cd20906998872ca484f728346/lkql_checker/share/lkql/integer_types_as_enum.lkql#L41-L45

The line 43 should be a conditional check. In the case of a type that is used by a subtype, and none of them uses operators, that case is not handled.

Solution

If types does not have a reference of the type, the we continue the other condition (this is actually what the code does).

However, if types have reference of the type, then we have to check instantiations and arithmetic_ops for every references.

So that, we can display a integer type may be replaced by an enumeration for type that do not have arithmetic operator, but have reference to this type (subtype, etc.) which also do not use operators.

Example:

procedure Integer_Types_As_Enum is
   type T1 is mod 10;
   type T2 is new T1;
   V1  : T1;
   V2  : T2;

begin
   declare
      type T11 is range 1 .. 10;          -- FLAGGED
      type T12 is new T1;                 -- FLAGGED

      V11 : T11;
      V12 : T12;
   begin
      if V1 > 1 then
         null;
      end if;
      if V12 in 5 .. 7 then
         null;
      end if;
   end;

   V1 := V1 and 1;
   V2 := V2 + 1;

   declare
      type T13 is range 1 .. 10;
      type T14 is new T13;                 -- FLAGGED
      subtype ST13 is T13 range 1 .. 5;
      function "+" (L, R : ST13) return ST13 is
      begin
         return L;
      end "+";

      type Arr_1_13 is array (T1) of Character;
      V13 : array (T14) of T2;

      VST13 : ST13;
   begin
      VST13 := VST13 + 1;
   end;

   declare
      type T15 is range 1 .. 10;           -- FLAGGED
      type T16 is new T15 range 1 .. 5;    -- FLAGGED
      subtype ST15 is T15 range 1 .. 5;
      subtype ST16 is T16 range 1 .. 2;

      VST15 : ST15;
      VST16 : ST16;
   begin
      if VST16 in 1 .. 1 then
         VST16 := 1;
      elsif VST15 < 3 or VST15 = 10 then
         VST15 := 9;
      end if;
   end;
end Integer_Types_As_Enum;
Heziode commented 1 year ago

Furthermore, the control in arithmetic seems wrong. There is missing cases too.

It should be something like:

6,7c6,8
<                 BinOp(f_op is OpDiv or OpMinus or OpMod or OpMult or
<                               OpPlus or OpPow or OpRem or OpXor) or
---
>                 BinOp(f_op is OpAndThen or OpAnd or OpDiv or OpMinus or
>                 OpMod or OpMult or OpOrElse or OpOr or OpPlus or OpPow or
>                 OpRem or OpXor) or
9d9
< 
ArnaudCharlet commented 1 year ago

Thanks for the report. The first part (missing cases involving subtypes) is currently intentional and as documented at the top of the file (and in the gnatcheck documentation: https://docs.adacore.com/live/wave/lkql/html/gnatcheck_rm/gnatcheck_rm/predefined_rules.html#integer-types-as-enum), so we're talking about a possible enhancement to flag more cases.

The second part is also currently as documented ("and/or" are not arithmetic operators, these are bitwise operators in the case of modular types) although extending this rule to modular integers could be interesting indeed.

Finally note that OpAndThen and OpOrElse are not operators and do not apply to integers, so do not need to be taken into account.

Heziode commented 1 year ago

Ok, As I was originally based on the tuto to use this rule, I did not pay attention to the comment.

is currently intentional

Is it a limitation of libadalang? Or LKQL?

ArnaudCharlet commented 1 year ago

"Is it a limitation of libadalang? Or LKQL?"

Neither, it's a decision based made when defining the rule precisely (and can be subject to changes/improvements in the future), to set expectations right and to allow precise testing.

There is no intrinsic limitation in LAL or LKQL here.

Roldak commented 8 months ago

Was accidentally closed