## GNATcheck rule configuration proposal This document summarizes a proposal for a new rule configuration endpoint for GNATcheck. Eventually, in a further version of GNATcheck, the goal is also to deprecate/scale back as much as possible the current paradigm for passing rules to GNATcheck: * Support for `-rules` would be scaled back to a minimum (no support for rule parameters, or for turning off rules) * Support for the rules.txt file would be deprecated * We would support using `--rules` instead of `-rules` and deprecate the old one The rationale behind this is that the current paradigm is both hard to use, and a maintenance burden. Parsing rule arguments manually is error prone, and the format is a custom one rather than a general one. Additionally, using the command line for such complex configuration support is a smell in general. Starting from there, we have two alternatives for the new rule passing paradigm ### Option 1: GPR based rule passing support The first option would be to support passing rules via project files. ```ada package Check is for Rules ("SPARK_Mode" | others) use <rules_aggregate>; end Check; ``` Passing of simple rules would be done directly via passing identifiers corresponding to the rule names ```ada package Check is for Rules ("Ada") use (Goto_Statements, Recursive_Subprograms); end Check; ``` Rules with arguments would use aggregate syntax as such: ```ada package Check is for Rules (others) use (Goto_Statements, Identifier_Suffixes => (Type_Suffix => "T_")); end Check; ``` Pros: * Consistent with the way we configure the rest of our tools * Some configurability inherited from GPR, makes it so that you can use scenario variables/some level of conditional configuration Cons: * When users want to share rule files across projects, GPR might not be the ideal mechanism to write rules into * GPR doesn't have support for more complex data structure literals yet ### Option 2: Toml based rule passing support We would use Toml as a format to pass configuration options to GNATcheck, including rules: ``` rules = [ "goto_statements", "recursive_subprograms", {identifier_suffix = "t_"} ] spark_rules = [...] ``` Pros: * We already have a toml parser * It's becoming more and more common as a format for config files, and looks a lot like INI on steroids * Built-in syntax for passing arguments via dicts * Built-in support for basic types like strings/numerals/dicts/lists, that we need for gnatcheck rule arguments Cons: * No configurability * New file format for AdaCore tools (except for Alire) ### Option 3: Hybrid * Basically option 2 with some configurability via project files * Use a default path for rule file ("rules.toml") * Allow some configurability via the project file as shown below ```ada package Check is for Rules (others) use "rules.toml"; end Check; ``` ```ada package Check is case Match (Project'Runtime("Ada"), "tasking") is when "tasking" => for Rules (others) use "rules_tasking.toml" when others => for Rules (others) use "rules.toml" end case; end Check; ``` ### Option 4: LKQL config file ```python # On the fly design: We add a conf dict data structure, with @{} # (for example), where you can have "empty" keys, where the value # is automatically an empty dict. Pretty trivial to add to the # LKQL parser/interpreter. rules = @{ recursive_subprograms, #: {} goto_statements, expression_functions, identifier_suffixes: [ {suffix: "t", alias_name: "pouet"}, {suffix: "p", alias_name: "foo"}, ] } spark_rules = { ... } ``` Pros: * We already have that parser, just need to slightly extend it. Probably the option that requires the least effort * We get some configurability out of the box. We can imagine exposing some outside variables in that config file (for example, access to env vars/scenario vars). We have conditional expressions to allow configurability. * Built-in types * The types are exactly the ones LKQL rules will get in the end Cons: * Users that use GNATcheck and don't write their own rules will have to learn a bit of syntax. * OTOH syntax is almost exactly JSON/JS * and rules.txt is already custom syntax ## Tentative SOW AdaCore will implement a GNATcheck capability that allows the user to configure which rules are ran on its code via an LKQL configuration file. This configuration capability will allow the user to chose which rules are meant to be ran on Ada code, SPARK code, or both. It will also allow passing parameters to rules, and the definition of aliases for rules. Here is an example: ``` rules = @{ recursive_subprograms, goto_statements, expression_functions, identifier_suffixes: [ {suffix: "t", alias_name: "pouet"}, {suffix: "p", alias_name: "foo"}, ] } spark_rules = @{ no_ada_2022 } ``` The delivery schedule will go as follows: Final delivery - T0 + 3 months