From f43a8b4bb4daa6783e1f3c8b1c34d1a2d956e5c7 Mon Sep 17 00:00:00 2001
From: Tristan Le Gall <tristan.le-gall@cea.fr>
Date: Fri, 6 Oct 2017 14:02:07 +0200
Subject: [PATCH] [kernel] add option -json-compilation-database
---
.gitignore | 1 +
Makefile | 16 ++
configure.in | 16 ++
doc/userman/user-changes.tex | 2 +
doc/userman/user-sources.tex | 9 ++
headers/header_spec.txt | 3 +
man/frama-c.1 | 19 ++-
share/Makefile.config.in | 7 +
src/kernel_services/ast_queries/file.ml | 16 +-
.../json_compilation_database.ko.ml | 29 ++++
.../ast_queries/json_compilation_database.mli | 26 ++++
.../json_compilation_database.ok.ml | 141 ++++++++++++++++++
.../plugin_entry_points/kernel.ml | 15 ++
.../plugin_entry_points/kernel.mli | 3 +
14 files changed, 296 insertions(+), 7 deletions(-)
create mode 100644 src/kernel_services/ast_queries/json_compilation_database.ko.ml
create mode 100644 src/kernel_services/ast_queries/json_compilation_database.mli
create mode 100644 src/kernel_services/ast_queries/json_compilation_database.ok.ml
diff --git a/.gitignore b/.gitignore
index 48665fcf8dd..e04ec9e2d72 100644
--- a/.gitignore
+++ b/.gitignore
@@ -178,6 +178,7 @@ Makefile.plugin.generated
/src/kernel_internals/parsing/cparser.ml
/src/kernel_internals/parsing/cparser.mli
/src/plugins/value/domains/apron/apron_domain.ml
+/src/kernel_services/ast_queries/json_compilation_database.ml
# generated tar.gz files
diff --git a/Makefile b/Makefile
index a8d1211c8fe..12d9f540998 100644
--- a/Makefile
+++ b/Makefile
@@ -530,6 +530,7 @@ KERNEL_CMO=\
src/libraries/utils/command.cmo \
src/libraries/utils/task.cmo \
src/kernel_services/ast_queries/filecheck.cmo \
+ src/kernel_services/ast_queries/json_compilation_database.cmo \
src/kernel_services/ast_queries/file.cmo \
src/kernel_internals/typing/translate_lightweight.cmo \
src/kernel_internals/typing/allocates.cmo \
@@ -581,6 +582,21 @@ GENERATED += $(addprefix src/kernel_internals/parsing/,\
logic_lexer.ml logic_parser.ml \
logic_parser.mli logic_preprocess.ml)
+
+ifeq ($(HAS_YOJSON),yes)
+src/kernel_services/ast_queries/json_compilation_database.ml: \
+ src/kernel_services/ast_queries/json_compilation_database.ok.ml share/Makefile.config
+ $(CP_IF_DIFF) $< $@
+ $(CHMOD_RO) $@
+else
+src/kernel_services/ast_queries/json_compilation_database.ml: \
+ src/kernel_services/ast_queries/json_compilation_database.ko.ml share/Makefile.config
+ $(CP_IF_DIFF) $< $@
+ $(CHMOD_RO) $@
+endif
+GENERATED += src/kernel_services/ast_queries/json_compilation_database.ml
+
+
.PHONY: check-logic-parser-wildcard
check-logic-parser-wildcard:
cd src/kernel_internals/parsing && ocaml check_logic_parser.ml
diff --git a/configure.in b/configure.in
index d3f05f4982a..40f7e2abc41 100644
--- a/configure.in
+++ b/configure.in
@@ -301,6 +301,21 @@ fi
AC_CHECK_PROG(OTAGS,otags,otags,)
+# yojson
+########
+
+AC_MSG_CHECKING(for Yojson)
+
+YOJSON_PATH=$($OCAMLFIND query yojson 2>/dev/null | tr -d '\r\n')
+if test -f "$YOJSON_PATH/yojson.$OBJ_SUFFIX"; then
+ HAS_YOJSON="yes";
+ AC_MSG_RESULT(found)
+else
+ HAS_YOJSON="no";
+ AC_MSG_RESULT(yojson not found. Kernel option -json-compilation-database won't be available.)
+fi;
+
+
# apron
########
@@ -921,6 +936,7 @@ AC_SUBST(VERBOSEMAKE)
AC_SUBST(DEVELOPMENT)
AC_SUBST(DOT)
AC_SUBST(HAS_DOT)
+AC_SUBST(HAS_YOJSON)
AC_SUBST(HAS_APRON)
AC_SUBST(HAS_LANDMARKS)
AC_SUBST(OCAMLBEST)
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 791997648b2..b496c22ab9a 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -9,6 +9,8 @@ release. First we list changes of the last release.
\begin{itemize}
\item \textbf{Customizing Analyzers:} added option \texttt{-warn-special-float}.
+\item \textbf{Preparing the Sources:} added option
+ \texttt{-json-compilation-database}.
\end{itemize}
\section*{Sulfur-20171101}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index c7627ca2306..a0f014ef5d2 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -48,6 +48,15 @@ typically via the inclusion of defines (\texttt{-D} switches) and header
directories (\texttt{-I} switches), as in
\texttt{-cpp-extra-args="-DDEBUG -DARCH=ia32 -I./headers"}.
+If you have a JSON compilation database file\footnote{%
+ \url{http://clang.llvm.org/docs/JSONCompilationDatabase.html}}, you can use
+it to retrieve \texttt{-D} and \texttt{-I} flags for each file in the database,
+via option \optiondef{-}{json-compilation-database} <path>, where <path> is
+the path to the JSON file or to a directory containing a
+\texttt{compile\_commands.json} file. With this option set, \FramaC will parse
+the compilation database and, it will include
+\texttt{-D} and \texttt{-I} flags associated to the file.
+
By default, \acsl annotations are pre-processed (option \optiondef{-}{pp-annot}
is set by default). Unless a custom pre-processor is specified
(via \optionuse{-}{cpp-frama-c-compliant}), \FramaC considers that \gcc is
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 72a19c41d0d..f40ad1dd860 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -485,6 +485,9 @@ src/kernel_services/ast_queries/file.ml: CEA_LGPL
src/kernel_services/ast_queries/file.mli: CEA_LGPL
src/kernel_services/ast_queries/filecheck.ml: CEA_LGPL
src/kernel_services/ast_queries/filecheck.mli: CEA_LGPL
+src/kernel_services/ast_queries/json_compilation_database.ko.ml: CEA_LGPL_OR_PROPRIETARY
+src/kernel_services/ast_queries/json_compilation_database.mli: CEA_LGPL_OR_PROPRIETARY
+src/kernel_services/ast_queries/json_compilation_database.ok.ml: CEA_LGPL_OR_PROPRIETARY
src/kernel_services/ast_queries/logic_const.ml: CEA_INRIA_LGPL
src/kernel_services/ast_queries/logic_const.mli: CEA_INRIA_LGPL
src/kernel_services/ast_queries/logic_env.ml: CEA_INRIA_LGPL
diff --git a/man/frama-c.1 b/man/frama-c.1
index 5afe72dfc40..eb35d7b51df 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -257,9 +257,9 @@ is not false, also adds
to prevent an inconsistent mix of system and Frama-C header files.
Defaults to yes.
.TP
-.BI -implicit-function-declaration\ <action>
+.BI -implicit-function-declaration\ action
warns or aborts when a function is called before it has been declared.
-\fI<action>\fP can be one of \fBignore\fP, \fBwarn\fP, or
+\fIaction\fP can be one of \fBignore\fP, \fBwarn\fP, or
\fBerror\fP. Defaults to \fBwarn\fP.
.TP
.B -initialized-padding-locals
@@ -283,6 +283,19 @@ Set the name of the journal file (without the
.I .ml
extension). Defaults to frama_c_journal.
.TP
+.BI -json-compilation-database\ path
+use \fIpath\fP as a JSON compilation database
+(see
+.RB < https://clang.llvm.org/docs/JSONCompilationDatabase.html >
+for more information)
+: each file preprocessed by
+Frama-C will include corresponding
+.BR -I\ and\ -D
+flags according to the specifications in \fIpath\fP.
+If \fIpath\fP is a directory, use
+.BR <path>/compile_commands.json .
+Disabled by default.
+.TP
.B [-no]-keep-comments
Tries to preserve comments when pretty-printing the source code (defaults to
no).
@@ -301,7 +314,7 @@ copies log messages from the Frama-C's kernel to \fIfile\fP. \fIkind\fP
specifies which kinds of messages to be copied (e.g. \fBw\fP for warnings,
\fBe\fP for errors, etc.). See \fB-kernel-help\fP for more details.
Can also be set on a per-plugin basis, with option
-.BI - plugin \-log \fP.
+.BI - <plugin> \-log \fP.
.TP
.B [-no]-lib-entry
Indicates that the entry point is called during program execution. This
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index baa4ffde083..e932db64f96 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -98,6 +98,9 @@ HAS_GTKSOURCEVIEW ?=@HAS_GTKSOURCEVIEW@
# lablgnomecanvas
HAS_GNOMECANVAS ?=@HAS_GNOMECANVAS@
+# yojson
+HAS_YOJSON ?=@HAS_YOJSON@
+
# apron
HAS_APRON ?=@HAS_APRON@
@@ -158,6 +161,10 @@ ifeq ($(HAS_LANDMARKS),yes)
LIBRARY_NAMES += landmarks landmarks.ppx
endif
+ifeq ($(HAS_YOJSON),yes)
+LIBRARY_NAMES += yojson
+endif
+
ifneq ($(ENABLE_GUI),no)
LIBRARY_NAMES_GUI = lablgtk2 lablgtk2.gnomecanvas lablgtk2.sourceview2
else
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index a745200cb71..fbb39c31641 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -113,9 +113,17 @@ let get_preprocessor_command () =
let from_filename ?cpp f =
let cpp, is_gnu_like =
- match cpp with
- | None -> get_preprocessor_command ()
- | Some s -> s, cpp_opt_kind ()
+ let cmdline = Kernel.CppCommand.get() in
+ if cmdline <> "" then
+ cmdline, cpp_opt_kind ()
+ else
+ let flags = Json_compilation_database.get_flags f in
+ let cpp, gnu =
+ match cpp with
+ | None -> get_preprocessor_command ()
+ | Some cpp -> cpp, cpp_opt_kind ()
+ in
+ (if flags = "" then cpp else cpp ^ " " ^ flags), gnu
in
if Filename.check_suffix f ".i" then begin
NoCPP f
@@ -158,6 +166,7 @@ end = struct
let dependencies =
[ Kernel.CppCommand.self;
Kernel.CppExtraArgs.self;
+ Kernel.JsonCompilationDatabase.self;
Kernel.Files.self ]
let name = "Files for preprocessing"
end)
@@ -648,7 +657,6 @@ let files_to_cabs_cil files =
if Kernel.UnspecifiedAccess.get () then
Undefined_sequence.check_sequences merged_file;
merged_file, cabs_files
-
(* "Implicit" annotations are those added by the kernel with ACSL name
'Frama_C_implicit_init'. Currently, this concerns statements that are
generated to initialize local variables. *)
diff --git a/src/kernel_services/ast_queries/json_compilation_database.ko.ml b/src/kernel_services/ast_queries/json_compilation_database.ko.ml
new file mode 100644
index 00000000000..d9d2df2f841
--- /dev/null
+++ b/src/kernel_services/ast_queries/json_compilation_database.ko.ml
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2017 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+let get_flags _ =
+ if Kernel.JsonCompilationDatabase.get () <> "" then begin
+ Kernel.warning ~once:true "ignoring option %s: Frama-C was not compiled \
+ with the required libraries (yojson)"
+ Kernel.JsonCompilationDatabase.option_name;
+ end;
+ ""
diff --git a/src/kernel_services/ast_queries/json_compilation_database.mli b/src/kernel_services/ast_queries/json_compilation_database.mli
new file mode 100644
index 00000000000..a919aef6fc4
--- /dev/null
+++ b/src/kernel_services/ast_queries/json_compilation_database.mli
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2017 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** [get_flags f] returns the preprocessing flags associated to file [f]
+ in the JSON compilation database (when enabled), or the empty string
+ otherwise. If not empty, the flags always start with a space. *)
+val get_flags : string -> string
diff --git a/src/kernel_services/ast_queries/json_compilation_database.ok.ml b/src/kernel_services/ast_queries/json_compilation_database.ok.ml
new file mode 100644
index 00000000000..1279731b150
--- /dev/null
+++ b/src/kernel_services/ast_queries/json_compilation_database.ok.ml
@@ -0,0 +1,141 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2017 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+let dkey = Kernel.register_category "pp:compilation-db"
+
+module Flags =
+ State_builder.Hashtbl
+ (Datatype.String.Hashtbl)
+ (Datatype.String)
+ (struct
+ let name ="JsonCompilationDatabase.Flags"
+ let dependencies = []
+ let size = 32
+ end)
+
+module Init = State_builder.Bool_ref
+ (struct
+ let name ="JsonCompilationDatabase.Init"
+ let dependencies = []
+ let default () = false
+ end)
+
+let parse_file ?(cwd=Sys.getcwd()) (r : Yojson.Basic.json) =
+ let open Yojson.Basic.Util in
+ let filename = r |> member "file" |> to_string in
+ let dirname = r |> member "directory" |> to_string in
+ let fullname = Filepath.normalize ~base_name:dirname filename in
+
+ (* get the list of arguments *)
+ let string_option_list =
+ try
+ let s = r |> member "command" |> to_string in
+ (* TODO: take into account spaces inside quote blocks *)
+ Str.split (Str.regexp "[ \t]+") s
+ with (* no command args *)
+ _ ->
+ List.map to_string (r |> member "arguments" |> to_list)
+ in
+ (* filtering the list *)
+ let (_, list_includes,list_defines) =
+ List.fold_left
+ (fun (prec,acc_includes,acc_defines) s ->
+ match prec with
+ | "-I" -> ("", s :: acc_includes, acc_defines)
+ | "-D" -> ("", acc_includes, s :: acc_defines)
+ | _ ->
+ let first_two_chars = Str.string_before s 2
+ and other_chars =Str.string_after s 2
+ in
+ begin
+ match first_two_chars with
+ | "-I" when String.length other_chars > 0 ->
+ ("", other_chars :: acc_includes, acc_defines)
+ | "-I" ->
+ ("-I", acc_includes, acc_defines)
+ | "-D" when String.length other_chars > 0 ->
+ ("", acc_includes, other_chars :: acc_defines)
+ | "-D" ->
+ ("-D", acc_includes, acc_defines)
+ | _ ->
+ ("",acc_includes,acc_defines)
+ end
+ )
+ ("", [], [])
+ string_option_list
+ in
+ (* Normalize list_includes path names: first we normalize w.r.t. to the
+ file's directory (following the compilation database logic), then we
+ relativize w.r.t. to Frama-C's PWD if possible (to avoid overly long
+ absolute paths). *)
+ let list_includes =
+ List.map (fun f ->
+ let abs = Filepath.normalize ~base_name:dirname f in
+ Filepath.relativize ~base_name:cwd abs
+ ) list_includes
+ in
+ let arg_includes =
+ if list_includes = [] then ""
+ else " -I" ^ (String.concat " -I" list_includes)
+ in
+ (* The JSON file does not include quotes for macro definitions, so we
+ add them here. It is necessary for function macros, and should not affect
+ constant definitions. *)
+ let arg_defines =
+ String.concat "" (List.map (fun d -> " -D'" ^ d ^ "'") list_defines)
+ in
+ Flags.add fullname (arg_includes ^ arg_defines)
+
+let get_flags f =
+ if Kernel.JsonCompilationDatabase.get () <> "" then begin
+ if not (Init.get ()) then begin
+ let database = Kernel.JsonCompilationDatabase.get () in
+ let path =
+ if Sys.is_directory database then
+ Filename.concat database "compile_commands.json"
+ else database
+ in
+ Kernel.feedback "using compilation database: %s" path;
+ begin
+ try
+ let r_list =
+ Yojson.Basic.from_file path |> Yojson.Basic.Util.to_list
+ in
+ List.iter parse_file r_list;
+ with
+ | Sys_error msg
+ | Yojson.Json_error msg
+ | Yojson.Basic.Util.Type_error (msg, _) ->
+ Kernel.abort "could not parse compilation database@ %s" msg
+ end;
+ Init.set true
+ end;
+ let filepath = Filepath.normalize f in
+ try
+ let flags = Flags.find filepath in
+ Kernel.feedback ~dkey "flags found for '%s': %s" filepath flags;
+ flags
+ with Not_found ->
+ Kernel.feedback ~dkey "no flags found for '%s'" filepath;
+ ""
+ end
+ else ""
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index a9537687505..0c3abff0dd5 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -855,6 +855,21 @@ module C11 =
let module_name = "C11"
end)
+let () = Parameter_customize.set_group parsing
+let () = Parameter_customize.do_not_reset_on_copy ()
+module JsonCompilationDatabase =
+ String
+ (struct
+ let module_name = "JsonCompilationDatabase"
+ let option_name = "-json-compilation-database"
+ let default = ""
+ let arg_name = "path"
+ let help = "when set, preprocessing of each file will include \
+ corresponding -I and -D flags from the JSON compilation \
+ database specified by <path>. If <path> is a directory, \
+ use '<path>/compile_commands.json'. Disabled by default."
+ end)
+
(* ************************************************************************* *)
(** {2 Customizing Normalization} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index ce6e91dbe3b..9441861c9e8 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -260,6 +260,9 @@ module ImplicitFunctionDeclaration: Parameter_sig.String
module C11: Parameter_sig.Bool
(** Behavior of option "-c11" *)
+module JsonCompilationDatabase: Parameter_sig.String
+ (** Behavior of option "-json-compilation-database" *)
+
(* ************************************************************************* *)
(** {3 Customizing cabs2cil options} *)
(* ************************************************************************* *)
--
GitLab