From 1bf27ed935da383eb7dcf3975e78179248ad28bb Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 7 Apr 2020 11:22:14 +0200
Subject: [PATCH] [e-acsl] adding the RTL AST
---
src/plugins/e-acsl/Makefile.in | 1 +
.../e-acsl/src/analyses/mmodel_analysis.ml | 2 +-
.../e-acsl/src/code_generator/constructor.ml | 7 +-
.../e-acsl/src/code_generator/constructor.mli | 2 +-
.../e-acsl/src/code_generator/injector.ml | 12 +-
src/plugins/e-acsl/src/libraries/functions.ml | 4 +-
.../e-acsl/src/libraries/functions.mli | 12 +-
src/plugins/e-acsl/src/options.ml | 4 +-
src/plugins/e-acsl/src/options.mli | 1 +
.../e-acsl/src/project_initializer/rtl.ml | 283 ++++++++++++++++++
.../e-acsl/src/project_initializer/rtl.mli | 48 +++
11 files changed, 358 insertions(+), 18 deletions(-)
create mode 100644 src/plugins/e-acsl/src/project_initializer/rtl.ml
create mode 100644 src/plugins/e-acsl/src/project_initializer/rtl.mli
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 936fc6f57fa..2eb4d2d1a7e 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -58,6 +58,7 @@ SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
# project initializer
SRC_PROJECT_INITIALIZER:= \
keep_status \
+ rtl \
prepare_ast
SRC_PROJECT_INITIALIZER:=\
$(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))
diff --git a/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml b/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
index 3b655683995..fb984d7073e 100644
--- a/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
+++ b/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
@@ -27,7 +27,7 @@ module Dataflow = Dataflow2
let must_never_monitor vi =
(* E-ACSL, please do not monitor yourself! *)
- Functions.RTL.is_rtl_name vi.vname
+ Rtl.Symbols.mem_vi vi.vname
||
(* extern ghost variables are usually used (by the Frama-C libc) to
represent some internal invisible states in ACSL specifications. They do
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/constructor.ml
index 4848a1f2e21..a38f36ce70e 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.ml
+++ b/src/plugins/e-acsl/src/code_generator/constructor.ml
@@ -98,7 +98,12 @@ let mk_block stmt b = match b.bstmts with
(* ********************************************************************** *)
let mk_lib_call ~loc ?result fname args =
- let vi = Misc.get_lib_fun_vi fname in
+ let vi =
+ try Rtl.Symbols.find_vi fname
+ with Rtl.Symbols.Unregistered _ as exn ->
+ try Builtins.find fname
+ with Not_found -> raise exn
+ in
let f = Cil.evar ~loc vi in
vi.vreferenced <- true;
let make_args ~variadic args param_ty =
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.mli b/src/plugins/e-acsl/src/code_generator/constructor.mli
index 73173483987..d21c71e53a4 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.mli
+++ b/src/plugins/e-acsl/src/code_generator/constructor.mli
@@ -79,7 +79,7 @@ val mk_break: loc:location -> stmt
val mk_lib_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
(** Construct a call to a library function with the given name.
- @raise Unregistered_library_function if the given string does not represent
+ @raise Rtl.Symbols.Unregistered if the given string does not represent
such a function or if library functions were never registered (only possible
when using E-ACSL through its API). *)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index a0357a168fd..c01f07f6269 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -68,9 +68,9 @@ let inject_in_local_init loc env kf vi = function
when Options.Validate_format_strings.get ()
&& Functions.Libc.is_printf_name fvi.vname
->
- (* rewrite format functions (e.g., [printf]). *)
- let name = Functions.RTL.get_rtl_replacement_name fvi.vname in
- let new_vi = Misc.get_lib_fun_vi name in
+ (* rewrite libc function names (e.g., [printf]). *)
+ let name = Functions.RTL.libc_replacement_name fvi.vname in
+ let new_vi = try Builtins.find name with Not_found -> assert false in
let fmt = Functions.Libc.get_printf_argument_str ~loc fvi.vname args in
ConsInit(new_vi, fmt :: args, kind), env
@@ -80,7 +80,7 @@ let inject_in_local_init loc env kf vi = function
->
(* rewrite names of functions for which we have alternative definitions in
the RTL. *)
- fvi.vname <- Functions.RTL.get_rtl_replacement_name fvi.vname;
+ fvi.vname <- Functions.RTL.libc_replacement_name fvi.vname;
init, env
| AssignInit init ->
@@ -109,7 +109,7 @@ let rename_caller loc args exp = match exp.enode with
when Options.Replace_libc_functions.get ()
&& Functions.RTL.has_rtl_replacement vi.vname
->
- vi.vname <- Functions.RTL.get_rtl_replacement_name vi.vname;
+ vi.vname <- Functions.RTL.libc_replacement_name vi.vname;
exp, args
| Lval(Var vi, _)
@@ -120,7 +120,7 @@ let rename_caller loc args exp = match exp.enode with
from the above because argument list of format functions is extended with
an argument describing actual variadic arguments *)
(* replacement name, e.g., [printf] -> [__e_acsl_builtin_printf] *)
- let name = Functions.RTL.get_rtl_replacement_name vi.vname in
+ let name = Functions.RTL.libc_replacement_name vi.vname in
(* variadic arguments descriptor *)
let fmt = Functions.Libc.get_printf_argument_str ~loc vi.vname args in
(* get the name of the library function we need. Cannot just rewrite the
diff --git a/src/plugins/e-acsl/src/libraries/functions.ml b/src/plugins/e-acsl/src/libraries/functions.ml
index b939bcff401..37cf8f8319f 100644
--- a/src/plugins/e-acsl/src/libraries/functions.ml
+++ b/src/plugins/e-acsl/src/libraries/functions.ml
@@ -92,12 +92,10 @@ module RTL = struct
let is_generated_kf kf =
is_generated_name (Kernel_function.get_name kf)
- let is_rtl_name name = startswith e_acsl_api_prefix name
-
let is_generated_literal_string_name name =
startswith e_acsl_lit_string_prefix name
- let get_rtl_replacement_name fn = e_acsl_builtin_prefix ^ fn
+ let libc_replacement_name fn = e_acsl_builtin_prefix ^ fn
let has_rtl_replacement = function
| "strcpy" | "strncpy" | "strlen" | "strcat" | "strncat" | "strcmp"
diff --git a/src/plugins/e-acsl/src/libraries/functions.mli b/src/plugins/e-acsl/src/libraries/functions.mli
index a99291b585f..4963870c285 100644
--- a/src/plugins/e-acsl/src/libraries/functions.mli
+++ b/src/plugins/e-acsl/src/libraries/functions.mli
@@ -59,10 +59,6 @@ module RTL: sig
val is_generated_kf: kernel_function -> bool
(** Same as [is_generated_name] but for kernel functions *)
- val is_rtl_name: string -> bool
- (** @return [true] if the prefix of the given name indicates that it
- belongs to the public API of the E-ACSL Runtime Library *)
-
val is_generated_literal_string_name: string -> bool
(** Same as [is_generated_name] but indicates that the name represents a local
variable that replaced a literal string. *)
@@ -71,7 +67,7 @@ module RTL: sig
(** Retrieve the name of the kernel function and strip prefix that indicates
that it has been generated by the instrumentation. *)
- val get_rtl_replacement_name: string -> string
+ val libc_replacement_name: string -> string
(** Given the name of C library function return the name of the RTL function
that potentially replaces it. *)
@@ -178,3 +174,9 @@ module Libc: sig
In GCC/Clang [alloca] is typically implemented via [__builtin_alloca] *)
end (* Libc *)
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml
index da218069292..deadac84c81 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/src/plugins/e-acsl/src/options.ml
@@ -163,7 +163,9 @@ let parameter_states =
Functions.self;
Instrument.self ]
-let must_visit () = Run.get () || Check.get ()
+let emitter = Emitter.create "E-ACSL" [ Funspec ] ~correctness:[] ~tuning:[]
+
+let must_visit () = Run.get ()
let dkey_analysis = register_category "analysis"
let dkey_prepare = register_category "preparation"
diff --git a/src/plugins/e-acsl/src/options.mli b/src/plugins/e-acsl/src/options.mli
index 8e8114594f8..a3fc3697cbb 100644
--- a/src/plugins/e-acsl/src/options.mli
+++ b/src/plugins/e-acsl/src/options.mli
@@ -38,6 +38,7 @@ module Functions: Parameter_sig.Kernel_function_set
module Instrument: Parameter_sig.Kernel_function_set
val parameter_states: State.t list
+val emitter: Emitter.t
val must_visit: unit -> bool
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
new file mode 100644
index 00000000000..71e4991ff8b
--- /dev/null
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml
@@ -0,0 +1,283 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Cil_datatype
+
+let rtl_files () =
+ List.map
+ (fun d -> Options.Share.get_file ~mode:`Must_exist d)
+ [ "e_acsl_gmp_api.h";
+ "e_acsl.h" ]
+
+(* create the RTL AST in a fresh project *)
+let create_rtl_ast prj =
+ Project.on
+ prj
+ (fun () ->
+ (* compute the RTL AST in the same settings as the user source code.
+ Modifying these settings purposely kills the current AST (if any) *)
+ if Plugin.is_present "variadic" then
+ Dynamic.Parameter.Bool.off "-variadic-translation" ();
+ Kernel.Keep_unused_specified_functions.off ();
+ Kernel.CppExtraArgs.add
+ (Format.asprintf " -DE_ACSL_MACHDEP=%s" (Kernel.Machdep.get ()));
+ Kernel.Files.set (rtl_files ());
+ Ast.get ())
+ ()
+
+(* Note: vids, sids and eids are shared between projects (see implementation of
+ [Cil_const]). Therefore, no need to set them when inserting the corresponding
+ global into the AST. *)
+
+(* Tables that contain RTL's symbols. Useful to know whether some symbols is
+ part of the RTL. *)
+module Symbols: sig
+ val add_global: global -> unit
+ val mem_global: global -> bool
+ val add_kf: kernel_function -> unit
+ val mem_kf: kernel_function -> bool
+ val add_vi: string -> varinfo -> unit
+ val mem_vi: string -> bool
+ exception Unregistered of string
+ val find_vi: string -> varinfo (* may raise Unregistered *)
+ (* val debug: unit -> unit*)
+end = struct
+
+ let globals: unit Global.Hashtbl.t = Global.Hashtbl.create 17
+ let kfs: unit Kernel_function.Hashtbl.t = Kernel_function.Hashtbl.create 17
+ let vars
+ : varinfo Datatype.String.Hashtbl.t
+ = Datatype.String.Hashtbl.create 17
+
+ let add_global g = Global.Hashtbl.add globals g ()
+ let mem_global g = Global.Hashtbl.mem globals g
+
+ let add_kf g = Kernel_function.Hashtbl.add kfs g ()
+ let mem_kf g = Kernel_function.Hashtbl.mem kfs g
+
+ let add_vi s vi = Datatype.String.Hashtbl.add vars s vi
+ let mem_vi s = Datatype.String.Hashtbl.mem vars s
+ exception Unregistered of string
+ let find_vi s =
+ try Datatype.String.Hashtbl.find vars s
+ with Not_found -> raise (Unregistered s)
+
+(*
+ let debug () =
+ Global.Hashtbl.iter
+ (fun g1 () -> Format.printf "RTL %a@." Printer.pp_global g1)
+ rtl;
+ Varinfo.Hashtbl.iter
+ (fun g1 g2 -> Format.printf "VAR %a -> %a@."
+ Printer.pp_varinfo g1
+ Printer.pp_varinfo g2)
+ vars;
+ Typ.Hashtbl.iter
+ (fun g1 g2 -> Format.printf "TYP %a -> %a@."
+ Printer.pp_typ g1
+ Printer.pp_typ g2)
+ types;
+ Global_annotation.Hashtbl.iter
+ (fun g1 g2 -> Format.printf "ANNOT %a -> %a@."
+ Printer.pp_global_annotation g1
+ Printer.pp_global_annotation g2)
+ annots
+*)
+end
+
+(* NOTE: do not use [Mergecil.merge] since all [ast]'s symbols must be kept
+ unchanged: so do it ourselves. Thanksfully, we merge in a particular
+ setting because we know what the RTL is. Therefore merging is far from being
+ as complicated as [Mergecil]. *)
+
+(* lookup globals from [rtl_ast] in the current [ast] and fill the [Symbols]'
+ tables.
+ @return the list of globals to be inserted into [ast], in reverse order. *)
+let lookup_rtl_globals rtl_ast =
+ (* [do_it ~add mem acc l g] checks whether the global does exist in the user's
+ AST. If not, add it to the corresponding symbol table(s). *)
+ let rec do_it ?(add=fun _g -> ()) mem acc l g =
+ if mem g then do_globals (g :: acc) l
+ else begin
+ add g;
+ Symbols.add_global g;
+ do_globals (g :: acc) l
+ end
+ (* [do_ty] is [do_it] for types *)
+ and do_ty acc l g kind tname =
+ let mem _g =
+ try
+ ignore (Globals.Types.find_type kind tname);
+ true
+ with Not_found ->
+ false
+ in
+ do_it mem acc l g
+ and do_globals acc globs =
+ match globs with
+ | [] ->
+ acc
+ | GType(ti, _loc) as g :: l ->
+ do_ty acc l g Logic_typing.Typedef ti.tname
+ | GCompTag(ci, _loc) | GCompTagDecl(ci, _loc) as g :: l ->
+ let k = if ci.cstruct then Logic_typing.Struct else Logic_typing.Union in
+ do_ty acc l g k ci.cname
+ | GEnumTag(ei, _loc) | GEnumTagDecl(ei, _loc) as g :: l ->
+ do_ty acc l g Logic_typing.Enum ei.ename
+ | GVarDecl(vi, (pos, _)) | GVar(vi, _, (pos, _)) as g :: l ->
+ let tunit = Translation_unit pos.Filepath.pos_path in
+ let mem _g =
+ match Globals.Syntactic_search.find_in_scope vi.vorig_name tunit with
+ | None -> false
+ | Some _ -> true
+ in
+ let add g =
+ Symbols.add_vi vi.vname vi;
+ match g with
+ | GVarDecl _ -> Globals.Vars.add_decl vi
+ | GVar(_, ii, _) -> Globals.Vars.add vi ii
+ | _ -> assert false
+ in
+ do_it ~add mem acc l g
+ | GFunDecl(_, vi, _loc) | GFun({ svar = vi }, _loc) as g :: l ->
+ let mem _g =
+ try ignore (Globals.Functions.find_by_name vi.vname); true
+ with Not_found -> false
+ in
+ let add _g =
+ Symbols.add_vi vi.vname vi;
+ (* functions will be registered in kernel's table after substitution of
+ RTL's symbols inside them *)
+ in
+ do_it ~add mem acc l g
+ | GAnnot _ :: l ->
+ (* ignoring annotations from the AST *)
+ do_globals acc l
+ | GAsm _ | GPragma _ | GText _ as g :: _l ->
+ Kernel.fatal "unexpected global %a" Printer.pp_global g
+ in
+ do_globals [] rtl_ast.globals
+
+(* [substitute_rtl_symbols] registers the correct symbols for RTL's functions *)
+let substitute_rtl_symbols rtl_prj = function
+ | GVarDecl _ | GVar _ as g ->
+ g
+ | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc) as g ->
+ let get_kf vi =
+ try
+ Globals.Functions.get vi
+ with Not_found ->
+ Options.fatal "unknown function %s in project %a"
+ vi.vname
+ Project.pretty (Project.current ())
+ in
+ let selection =
+ State_selection.of_list
+ [ Globals.Functions.self; Annotations.funspec_state ]
+ in
+ (* get the RTL's formals and spec *)
+ let formals, spec =
+ Project.on
+ rtl_prj
+ ~selection
+ (fun vi ->
+ let kf = get_kf vi in
+ Kernel_function.get_formals kf,
+ Annotations.funspec ~populate:false kf)
+ vi
+ in
+ (match g with
+ | GFunDecl _ ->
+ Globals.Functions.replace_by_declaration spec vi loc
+ | GFun(fundec, _) ->
+ Globals.Functions.replace_by_definition spec fundec loc
+ | _ -> assert false);
+ (* [Globals.Functions.replace_by_declaration] assigns new vids to formals:
+ get them back to their original ids in order to have the correct ids in
+ [spec] *)
+ let kf = get_kf vi in
+ List.iter2
+ (fun rtl_vi src_vi -> src_vi.vid <- rtl_vi.vid)
+ formals
+ (Kernel_function.get_formals kf);
+ Cil.unsafeSetFormalsDecl vi formals;
+ Annotations.register_funspec ~emitter:Options.emitter kf;
+ Symbols.add_kf kf;
+ g
+ | GType _ | GCompTag _ | GCompTagDecl _ | GEnumTag _ | GEnumTagDecl _
+ | GAnnot _ | GAsm _ | GPragma _ | GText _ ->
+ assert false
+
+(* [insert_rtl_globals] adds the rtl symbols into the user's AST *)
+let insert_rtl_globals rtl_prj rtl_globals ast =
+ let add_ty acc old_g new_g =
+ let g = if Symbols.mem_global old_g then old_g else new_g in
+ (* keep them in the AST even if already in the user's one to prevent forward
+ references *)
+ g :: acc
+ in
+ let rec add acc = function
+ | [] ->
+ acc
+ | GType _ | GCompTagDecl _ | GEnumTagDecl _ as g :: l ->
+ (* RTL types contain no libc values: no need to substitute inside them *)
+ let acc = add_ty acc g g in
+ add acc l
+ | GCompTag(ci, loc) as g :: l ->
+ (* RTL's structure definitions that are already defined in the AST shall
+ be only declared *)
+ let acc = add_ty acc g (GCompTagDecl(ci, loc)) in
+ add acc l
+ | GEnumTag(ei, loc) as g :: l ->
+ (* RTL's enum definitions that are already defined in the AST shall be
+ only declared *)
+ let acc = add_ty acc g (GEnumTagDecl(ei, loc)) in
+ add acc l
+ | GVarDecl _ | GVar _ | GFunDecl _ | GFun _ as g :: l ->
+ let acc =
+ if Symbols.mem_global g then
+ let g = substitute_rtl_symbols rtl_prj g in
+ g :: acc
+ else
+ acc
+ in
+ add acc l
+ | GAnnot _ | GAsm _ | GPragma _ | GText _ as g :: _l ->
+ Kernel.fatal "unexpected global %a" Printer.pp_global g
+ in
+ ast.globals <- add ast.globals rtl_globals
+
+let link rtl_prj =
+ Options.feedback ~level:2 "link the E-ACSL RTL with the user source code";
+ let rtl_ast = create_rtl_ast rtl_prj in
+ let ast = Ast.get () in
+ let rtl_globals = lookup_rtl_globals rtl_ast in
+ (* Symbols.debug ();*)
+ insert_rtl_globals rtl_prj rtl_globals ast;
+ Ast.mark_as_grown ()
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.mli b/src/plugins/e-acsl/src/project_initializer/rtl.mli
new file mode 100644
index 00000000000..ff7cf96526a
--- /dev/null
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.mli
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** This module links the E-ACSL's RTL to the user source code. *)
+
+val link: Project.t -> unit
+(** [link prj] links the RTL's AST contained in [prj] to the AST of the current
+ project. *)
+
+(** Tables that contain RTL's symbols. Useful to know whether some symbols is
+ part of the RTL. *)
+module Symbols: sig
+ open Cil_types
+
+ val mem_global: global -> bool
+ val mem_kf: kernel_function -> bool
+
+ val mem_vi: string -> bool
+ exception Unregistered of string
+ val find_vi: string -> varinfo
+ (** @raise Unregistered if the given name is not part of the RTL. *)
+
+end
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
--
GitLab