[Kernel] JCDB: improve parsing of quoted arguments

src/kernel_services/ast_queries/json_compilation_database.ml

@@ -139,7 +139,9 @@ let split_command_args s =
     never need quotes. *)
 let quote_define_argument arg = Format.sprintf "%S" arg
 
-(* Filters and normalize useful flags: -I, -D, -U, ... *)
+(* Filters and normalize useful flags: -I, -D, -U, ...
+   This includes removing extraneous double quotes
+   (when the first and last characters are both '"') *)
 let filter_useful_flags ~requote option_list =
   let convert_define arg =
     if requote then quote_define_argument arg else arg
@@ -150,11 +152,20 @@ let filter_useful_flags ~requote option_list =
     | Define s -> s ^ convert_define suffix
     | Undefine s -> s ^ suffix
   in
+  let remove_extraneous_quotes arg =
+    let len = String.length arg in
+    if len = 0 then arg
+    else
+    if String.get arg 0 = '"' && String.get arg (len-1) = '"' then
+      String.sub arg 1 (len-2)
+    else arg
+  in
   (* we must process the arguments in-order, since several -D and -U may
      exist on the command line *)
   (* prev is the prefix of the previous argument (if any) *)
   let _, res =
     List.fold_left (fun (prev, acc_res) arg ->
+        let arg = remove_extraneous_quotes arg in
         match prev with
         | None -> begin
             match has_whitelisted_prefix arg with

tests/jcdb/compile_commands.json

@@ -12,7 +12,7 @@
       "file": "jcdb.c"
     },
     { "directory": ".",
-      "command": "/usr/bin/clang -D'MSG=\"a \\\" \\\"b\"'  -D'SINGLE_DOUBLE(a)=\"a \\\"with spaces and	tab \"' -DSOMEDEF=\"With spaces, quotes and \\-es.\" -D\"DOUBLE_SINGLE(a)=a \\\"macro with spaces and non-escaped \\\\'\\\"\"   -DEMPTY=''  -DEMPTY2= -DTEST=42	 -D'MACRO_FOR_INCR(s)=s+1' -DTOUNDEF -UTOUNDEF",
+      "command": "/usr/bin/clang -D'MSG=\"a \\\" \\\"b\"'  -D'SINGLE_DOUBLE(a)=\"a \\\"with spaces and	tab \"' -DSOMEDEF=\"With spaces, quotes and \\-es.\" -D\"DOUBLE_SINGLE(a)=a \\\"macro with spaces and non-escaped \\\\'\\\"\"   -DEMPTY=''  -DEMPTY2= -DTEST=42	 \"-DTEST2=43\" -D'MACRO_FOR_INCR(s)=s+1' -DTOUNDEF -UTOUNDEF",
       "file": "jcdb.c"
     }
 ]

tests/jcdb/jcdb.c

@@ -22,4 +22,4 @@ int main () {
   #ifndef __FRAMAC__
   printf("%s\n", s); // for GCC debugging
   #endif
-  return MACRO_FOR_INCR(TEST); }
+  return MACRO_FOR_INCR(TEST) - TEST2; }

tests/jcdb/oracle/jcdb.0.res.oracle

@@ -13,7 +13,7 @@ int main(void)
 {
   int __retres;
   char *s = (char *)"a macro with spaces and non-escaped \'";
-  __retres = 42 + 1;
+  __retres = (42 + 1) - 43;
   return __retres;
 }
 

tests/jcdb/oracle/jcdb.1.res.oracle

@@ -9,7 +9,7 @@ int main(void)
 {
   int __retres;
   char *s = (char *)"a macro with spaces and non-escaped \'";
-  __retres = 42 + 1;
+  __retres = (42 + 1) - 43;
   return __retres;
 }
 

tests/jcdb/with_arguments.json

@@ -7,6 +7,7 @@
           "-DEMPTY=",
           "-DEMPTY2=",
           "-DTEST=42",
+          "\"-DTEST2=43\"",
           "-DMACRO_FOR_INCR(s)=s+1",
           "-DSINGLE_DOUBLE(a)=\"a \\\"with spaces and\ttab \"",
           "-DMSG=\"a \\\" \\\"b\"",