From bea3890fd24426cba8fb0fe38d5e7b4614de7137 Mon Sep 17 00:00:00 2001 From: Romain Beguet Date: Tue, 14 May 2024 17:13:58 +0200 Subject: [PATCH] Communicate rules to worker using the LKQL config format. --- lkql_checker/src/gnatcheck-rules.adb | 50 ++++++++--------- lkql_checker/src/gnatcheck-rules.ads | 11 +--- lkql_checker/src/gnatcheck_main.adb | 55 +++++++++++++------ .../lkql_jit/drivers/GNATCheckWorker.java | 41 +------------- 4 files changed, 64 insertions(+), 93 deletions(-) diff --git a/lkql_checker/src/gnatcheck-rules.adb b/lkql_checker/src/gnatcheck-rules.adb index 6067024cf..805209812 100644 --- a/lkql_checker/src/gnatcheck-rules.adb +++ b/lkql_checker/src/gnatcheck-rules.adb @@ -306,19 +306,6 @@ package body Gnatcheck.Rules is return Rule.Rule_State = Enabled; end Is_Enabled; - ------------------------ - -- Source_Mode_String -- - ------------------------ - - function Source_Mode_String (Rule : Rule_Template) return String is - begin - case Rule.Source_Mode is - when General => return "GENERAL"; - when Ada_Only => return "ADA"; - when Spark_Only => return "SPARK"; - end case; - end Source_Mode_String; - --------------------- -- Load_Dictionary -- --------------------- @@ -374,27 +361,36 @@ package body Gnatcheck.Rules is Bad_Rule_Detected := True; end Load_Dictionary; - ---------------------------------- - -- Print_Rule_To_Universal_File -- - ---------------------------------- + ----------------------------- + -- Print_Rule_To_LKQL_File -- + ----------------------------- - procedure Print_Rule_To_Universal_File + procedure Print_Rule_To_LKQL_File (Rule : in out Rule_Template'Class; Rule_File : File_Type) is - Args : Rule_Argument_Vectors.Vector; + Args : Rule_Argument_Vectors.Vector; + First : Boolean := True; begin Map_Parameters (Rule, Args); - Put (Rule_File, Rule_Name (Rule) & "|" & Rule.Source_Mode_String); - for Param of Args loop - New_Line (Rule_File); - Put (Rule_File, "-"); - Put (Rule_File, - To_String (To_Wide_Wide_String (Param.Name)) & "=" & - To_String (To_Wide_Wide_String (Param.Value))); - end loop; - end Print_Rule_To_Universal_File; + Put (Rule_File, Rule_Name (Rule)); + + if not Args.Is_Empty then + Put (Rule_File, ": [{"); + for Param of Args loop + if First then + First := False; + else + Put (Rule_File, ", "); + end if; + Put (Rule_File, + To_String (To_Wide_Wide_String (Param.Name)) & ": " & + To_String (To_Wide_Wide_String (Param.Value))); + end loop; + Put (Rule_File, "}]"); + end if; + end Print_Rule_To_LKQL_File; ------------------------ -- Print_Rule_To_File -- diff --git a/lkql_checker/src/gnatcheck-rules.ads b/lkql_checker/src/gnatcheck-rules.ads index 1763c69ae..e6a8928bf 100644 --- a/lkql_checker/src/gnatcheck-rules.ads +++ b/lkql_checker/src/gnatcheck-rules.ads @@ -242,18 +242,11 @@ package Gnatcheck.Rules is function Is_Enabled (Rule : Rule_Template) return Boolean; -- Checks if the rule should be checked - function Source_Mode_String (Rule : Rule_Template) return String; - -- Get the string representing the rule source mode - - procedure Print_Rule_To_Universal_File + procedure Print_Rule_To_LKQL_File (Rule : in out Rule_Template'Class; Rule_File : File_Type); -- Prints information about the (active) rule into the specified file with - -- the following universal format: - -- "{rule_name}[:{param1}={value1}[,{param2}={value2},...]]". - -- Unlike the `Print_Rule_To_File` subprogram, this always prints the rule - -- in the above format without special cases for specific rules names or - -- rules with specific parameter types. + -- the LKQL rule options file syntax. procedure Print_Rule_To_File (Rule : Rule_Template; diff --git a/lkql_checker/src/gnatcheck_main.adb b/lkql_checker/src/gnatcheck_main.adb index b667b9761..1d60b41cd 100644 --- a/lkql_checker/src/gnatcheck_main.adb +++ b/lkql_checker/src/gnatcheck_main.adb @@ -116,6 +116,41 @@ procedure Gnatcheck_Main is procedure Schedule_Files; -- Schedule jobs per set of files + procedure Print_LKQL_Rules (File : File_Type; Mode : Source_Modes); + -- Print the rule configuration of the given source mode into the given + -- file using the LKQL rule config file format. + + ---------------------- + -- Print_LKQL_Rules -- + ---------------------- + + procedure Print_LKQL_Rules (File : File_Type; Mode : Source_Modes) is + Mode_String : constant String := + (case Mode is + when General => "rules", + when Ada_Only => "ada_rules", + when Spark_Only => "spark_rules"); + + First : Boolean := True; + begin + Put_Line (File, "val " & Mode_String & " = @{"); + for Rule in All_Rules.First .. All_Rules.Last loop + if Is_Enabled (All_Rules.Table (Rule).all) then + if All_Rules.Table (Rule).all.Source_Mode = Mode then + if First then + First := False; + else + Put_Line (File, ","); + end if; + Put (File, " "); + All_Rules.Table (Rule).Print_Rule_To_LKQL_File (File); + end if; + end if; + end loop; + New_Line (File); + Put_Line (File, "}"); + end Print_LKQL_Rules; + -------------------- -- Schedule_Files -- -------------------- @@ -129,7 +164,6 @@ procedure Gnatcheck_Main is File : Ada.Text_IO.File_Type; Status : Boolean; Total_Jobs : Natural; - begin -- Compute number of files @@ -158,22 +192,9 @@ procedure Gnatcheck_Main is Create (File, Out_File, File_Name ("rules", 0)); - for Rule in All_Rules.First .. All_Rules.Last loop - if Is_Enabled (All_Rules.Table (Rule).all) then - -- When the worker process to use is the GNATcheck executable - -- itself, the set of rules and their options are transfered in - -- the standard legacy GNATcheck rule format (the same format used - -- by users to specify rules). Otherwise, they are transfered in a - -- more universal format that can be easily parsed by custom - -- worker implementations. - if Use_External_Worker then - All_Rules.Table (Rule).Print_Rule_To_Universal_File (File); - else - All_Rules.Table (Rule).Print_Rule_To_File (File); - end if; - New_Line (File); - end if; - end loop; + Print_LKQL_Rules (File, General); + Print_LKQL_Rules (File, Ada_Only); + Print_LKQL_Rules (File, Spark_Only); Close (File); diff --git a/lkql_jit/cli/src/main/java/com/adacore/lkql_jit/drivers/GNATCheckWorker.java b/lkql_jit/cli/src/main/java/com/adacore/lkql_jit/drivers/GNATCheckWorker.java index b45a473aa..7c0ed6041 100644 --- a/lkql_jit/cli/src/main/java/com/adacore/lkql_jit/drivers/GNATCheckWorker.java +++ b/lkql_jit/cli/src/main/java/com/adacore/lkql_jit/drivers/GNATCheckWorker.java @@ -252,11 +252,7 @@ protected int executeScript(Context.Builder contextBuilder) { final Map instances = new HashMap<>(); for (var rulesFrom : this.args.rulesFroms) { if (!rulesFrom.isEmpty()) { - if (rulesFrom.endsWith(".lkql")) { - instances.putAll(parseLKQLRuleFile(rulesFrom)); - } else { - instances.putAll(parseGNATcheckRuleFile(rulesFrom)); - } + instances.putAll(parseLKQLRuleFile(rulesFrom)); } } contextBuilder.option("lkql.ruleInstances", JsonUtils.serializeInstances(instances)); @@ -284,41 +280,6 @@ protected List preprocessArguments( // ----- Option parsing helpers ----- - /** - * Open the given GNATcheck rule file and parse it to extract all user defined rule instances. - */ - private static Map parseGNATcheckRuleFile( - final String gnatcheckRuleFile) { - String currentInstanceId = null; - final Map res = new HashMap<>(); - try { - for (String ruleSpec : - Files.readAllLines(Paths.get(gnatcheckRuleFile)).stream() - .filter(s -> !s.isBlank()) - .toList()) { - if (ruleSpec.startsWith("-")) { - final String[] argSplit = ruleSpec.substring(1).split("="); - res.get(currentInstanceId).arguments().put(argSplit[0], argSplit[1]); - } else { - final String[] ruleSplit = ruleSpec.split("\\|"); - final RuleInstance.SourceMode sourceMode = - RuleInstance.SourceMode.valueOf(ruleSplit[1]); - currentInstanceId = ruleSplit[0].toLowerCase(); - res.put( - currentInstanceId, - new RuleInstance( - currentInstanceId, - Optional.empty(), - sourceMode, - new HashMap<>())); - } - } - } catch (IOException e) { - System.err.println("WORKER_FATAL_ERROR: Could not read file: " + gnatcheckRuleFile); - } - return res; - } - /** * Read the given LKQL file and parse it as a rule configuration file to return the extracted * instances.