From a0337b4cad4daac477078e6e885116c21c5555f9 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 19 Sep 2019 16:50:08 +0200
Subject: [PATCH] [Override Std] Initial version
---
src/plugins/override_std/.gitignore | 4 +
src/plugins/override_std/Makefile.in | 64 +++++++++
src/plugins/override_std/OverrideStd.mli | 0
src/plugins/override_std/basic_blocks.ml | 140 +++++++++++++++++++
src/plugins/override_std/basic_blocks.mli | 48 +++++++
src/plugins/override_std/configure.ac | 45 ++++++
src/plugins/override_std/memcpy.ml | 161 ++++++++++++++++++++++
src/plugins/override_std/memcpy.mli | 21 +++
src/plugins/override_std/options.ml | 39 ++++++
src/plugins/override_std/options.mli | 27 ++++
src/plugins/override_std/register.ml | 30 ++++
src/plugins/override_std/transform.ml | 94 +++++++++++++
src/plugins/override_std/transform.mli | 33 +++++
13 files changed, 706 insertions(+)
create mode 100644 src/plugins/override_std/.gitignore
create mode 100644 src/plugins/override_std/Makefile.in
create mode 100644 src/plugins/override_std/OverrideStd.mli
create mode 100644 src/plugins/override_std/basic_blocks.ml
create mode 100644 src/plugins/override_std/basic_blocks.mli
create mode 100644 src/plugins/override_std/configure.ac
create mode 100644 src/plugins/override_std/memcpy.ml
create mode 100644 src/plugins/override_std/memcpy.mli
create mode 100644 src/plugins/override_std/options.ml
create mode 100644 src/plugins/override_std/options.mli
create mode 100644 src/plugins/override_std/register.ml
create mode 100644 src/plugins/override_std/transform.ml
create mode 100644 src/plugins/override_std/transform.mli
diff --git a/src/plugins/override_std/.gitignore b/src/plugins/override_std/.gitignore
new file mode 100644
index 00000000000..0114e3d0f08
--- /dev/null
+++ b/src/plugins/override_std/.gitignore
@@ -0,0 +1,4 @@
+/configure
+/Makefile
+/tests/ptests_config
+/tests/*/result
diff --git a/src/plugins/override_std/Makefile.in b/src/plugins/override_std/Makefile.in
new file mode 100644
index 00000000000..4a3d3652d3c
--- /dev/null
+++ b/src/plugins/override_std/Makefile.in
@@ -0,0 +1,64 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2019 #
+# 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). #
+# #
+##########################################################################
+
+# Do not use ?= to initialize both below variables
+# (fixed efficiency issue, see GNU Make manual, Section 8.11)
+ifndef FRAMAC_SHARE
+FRAMAC_SHARE :=$(shell frama-c-config -print-share-path)
+endif
+ifndef FRAMAC_LIBDIR
+FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
+endif
+
+###################
+# Plug-in Setting #
+###################
+
+PLUGIN_DIR ?= .
+PLUGIN_ENABLE := @ENABLE_OVERRIDE_STD@
+PLUGIN_NAME := OverrideStd
+PLUGIN_CMI :=
+PLUGIN_CMO := options transform basic_blocks memcpy register
+PLUGIN_DISTRIBUTED := $(PLUGIN_ENABLE)
+PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
+#PLUGIN_NO_DEFAULT_TEST := no
+PLUGIN_TESTS_DIRS :=
+
+################
+# Generic part #
+################
+
+include $(FRAMAC_SHARE)/Makefile.dynamic
+
+#####################################
+# Regenerating the Makefile on need #
+#####################################
+
+ifeq ("$(FRAMAC_INTERNAL)","yes")
+CONFIG_STATUS_DIR=$(FRAMAC_SRC)
+else
+CONFIG_STATUS_DIR=.
+endif
+
+$(OverrideStd_DIR)/Makefile: $(OverrideStd_DIR)/Makefile.in \
+ $(CONFIG_STATUS_DIR)/config.status
+ cd $(CONFIG_STATUS_DIR) && ./config.status --file $@
diff --git a/src/plugins/override_std/OverrideStd.mli b/src/plugins/override_std/OverrideStd.mli
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/override_std/basic_blocks.ml b/src/plugins/override_std/basic_blocks.ml
new file mode 100644
index 00000000000..db2fa62e8f9
--- /dev/null
+++ b/src/plugins/override_std/basic_blocks.ml
@@ -0,0 +1,140 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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
+open Cil_types
+open Cil_const
+open Logic_const
+
+let ptr_of t = TPtr(t, [])
+let const_of t = Cil.typeAddAttributes [Attr("const", [])] t
+let restrict_of t = Cil.typeAddAttributes [Attr("restrict", [])] t
+
+let size_t () =
+ Globals.Types.find_type Logic_typing.Typedef "size_t"
+
+let rec string_of_typ_aux = function
+ | TInt(IBool, _) -> "bool"
+ | TInt(IChar, _) -> "char"
+ | TInt(ISChar, _) -> "schar"
+ | TInt(IUChar, _) -> "uchar"
+ | TInt(IInt, _) -> "int"
+ | TInt(IUInt, _) -> "uint"
+ | TInt(IShort, _) -> "short"
+ | TInt(IUShort, _) -> "ushort"
+ | TInt(ILong, _) -> "long"
+ | TInt(IULong, _) -> "ulong"
+ | TInt(ILongLong, _) -> "llong"
+ | TInt(IULongLong, _) -> "ullong"
+ | TFloat(FFloat, _) -> "float"
+ | TFloat(FDouble, _) -> "double"
+ | TFloat(FLongDouble, _) -> "ldouble"
+ | TPtr(t, _) -> "ptr_" ^ string_of_typ t
+ | TEnum (ei, _) -> ei.ename
+ | TComp (ci, _, _) -> ci.cname
+ | TArray (t, _, _, _) -> "arr_" ^ string_of_typ t
+ | _ -> assert false
+and string_of_typ t = string_of_typ_aux (Cil.unrollType t)
+
+
+let size_var t value = {
+ l_var_info = make_logic_var_local "__fc_len" t;
+ l_type = Some t;
+ l_tparams = [];
+ l_labels = [];
+ l_profile = [];
+ l_body = LBterm value;
+}
+
+(** Features related to terms *)
+
+let cvar_to_tvar vi = tvar (cvar_to_lvar vi)
+
+let tminus ?loc t1 t2 =
+ let minus, typ = match t1.term_type, t2.term_type with
+ | Ctype(t1), Ctype(t2) when Cil.isPointerType t1 && Cil.isPointerType t2 ->
+ MinusPP, Linteger
+ | Ctype(t), _ when Cil.isPointerType t ->
+ MinusPI, Ctype(t)
+ | t, _ ->
+ MinusA, t
+ in
+ term ?loc (TBinOp(minus, t1, t2)) typ
+
+let tplus ?loc t1 t2 =
+ let plus = match t1.term_type with
+ | Ctype(t) when Cil.isPointerType t -> PlusPI
+ | _ -> PlusA
+ in
+ term ?loc (TBinOp(plus, t1, t2)) t1.term_type
+
+let tdivide ?loc t1 t2 =
+ term ?loc (TBinOp(Div, t1, t2)) t1.term_type
+
+let ttype_of_pointed = function
+ | Ctype(TPtr(t, _)) | Ctype(TArray(t, _, _, _)) -> Ctype t
+ | _ -> assert false
+
+let tbuffer_range ?loc ptr len =
+ let last = tminus ?loc len (tinteger ?loc 1) in
+ let range = trange ?loc (Some (tinteger ?loc 0), Some last) in
+ tplus ?loc ptr range
+
+let tunref_range ?loc ptr len =
+ let typ = ttype_of_pointed ptr.term_type in
+ let range = tbuffer_range ?loc ptr len in
+ term (TLval ((TMem range), TNoOffset)) typ
+
+let tsizeofpointed ?loc = function
+ | Ctype(TPtr(t, _)) | Ctype(TArray(t, _, _, _)) -> tinteger ?loc (Cil.bytesSizeOf t)
+ | _ -> assert false
+
+let tlen_div_size ?loc t bytes_len =
+ let sizeof = tsizeofpointed ?loc t in
+ tdivide ?loc bytes_len sizeof
+
+(** Features related to predicates *)
+
+let plet_len_div_size ?loc t bytes_len pred =
+ let len = tlen_div_size t bytes_len in
+ let len_var = size_var Linteger len in
+ plet ?loc len_var (pred (tvar len_var.l_var_info))
+
+let pgeneric_valid_buffer ?loc validity lbl ptr len =
+ let buffer = tbuffer_range ?loc ptr len in
+ validity ?loc (lbl, buffer)
+
+let pgeneric_valid_len_bytes ?loc validity lbl ptr bytes_len =
+ plet_len_div_size ?loc ptr.term_type bytes_len (pgeneric_valid_buffer ?loc validity lbl ptr)
+
+let pvalid_len_bytes ?loc = pgeneric_valid_len_bytes ?loc pvalid
+let pvalid_read_len_bytes ?loc = pgeneric_valid_len_bytes ?loc pvalid_read
+
+let pcorrect_len_bytes ?loc t bytes_len =
+ let sizeof = tsizeofpointed ?loc t in
+ let modulo = term ?loc (TBinOp(Mod, bytes_len, sizeof)) Linteger in
+ prel ?loc (Req, modulo, tinteger ?loc 0)
+
+let pseparated_memories ?loc p1 len1 p2 len2 =
+ let b1 = tbuffer_range ?loc p1 len1 in
+ let b2 = tbuffer_range ?loc p2 len2 in
+ pseparated ?loc [ b1 ; b2 ]
\ No newline at end of file
diff --git a/src/plugins/override_std/basic_blocks.mli b/src/plugins/override_std/basic_blocks.mli
new file mode 100644
index 00000000000..95683f01d0b
--- /dev/null
+++ b/src/plugins/override_std/basic_blocks.mli
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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
+
+val ptr_of: typ -> typ
+val const_of: typ -> typ
+val restrict_of: typ -> typ
+
+val size_t: unit -> typ
+
+val string_of_typ: typ -> string
+
+val ttype_of_pointed: logic_type -> logic_type
+
+val cvar_to_tvar: varinfo -> term
+val tunref_range: ?loc:location -> term -> term -> term
+val tplus: ?loc:location -> term -> term -> term
+val tminus: ?loc:location -> term -> term -> term
+val tdivide: ?loc:location -> term -> term -> term
+
+val pvalid_len_bytes: ?loc:location -> logic_label -> term -> term -> predicate
+val pvalid_read_len_bytes: ?loc:location -> logic_label -> term -> term -> predicate
+val pcorrect_len_bytes: ?loc:location -> logic_type -> term -> predicate
+
+val pseparated_memories: ?loc:location -> term -> term -> term -> term -> predicate
+
+val plet_len_div_size:
+ ?loc:location -> logic_type -> term -> (term -> predicate) -> predicate
\ No newline at end of file
diff --git a/src/plugins/override_std/configure.ac b/src/plugins/override_std/configure.ac
new file mode 100644
index 00000000000..d90276f26f2
--- /dev/null
+++ b/src/plugins/override_std/configure.ac
@@ -0,0 +1,45 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2019 #
+# 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). #
+# #
+##########################################################################
+
+##########################################
+# Override stdlib C plugin #
+##########################################
+
+m4_define([plugin_file],Makefile.in)
+
+m4_define([FRAMAC_SHARE_ENV],
+ [m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
+
+m4_define([FRAMAC_SHARE],
+ [m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
+ [m4_esyscmd(frama-c -print-path)])])
+
+m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
+
+check_plugin(overridestd,PLUGIN_RELATIVE_PATH(plugin_file),
+ [support for override-std plug-in],yes)
+
+#######################
+# Generating Makefile #
+#######################
+
+write_plugin_config(Makefile)
diff --git a/src/plugins/override_std/memcpy.ml b/src/plugins/override_std/memcpy.ml
new file mode 100644
index 00000000000..0ca191c8860
--- /dev/null
+++ b/src/plugins/override_std/memcpy.ml
@@ -0,0 +1,161 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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 Logic_const
+open Basic_blocks
+
+let table: (typ, varinfo) Hashtbl.t = Hashtbl.create 5
+
+let function_name = "memcpy"
+
+let pseparated_memcpy_len_bytes ?loc p1 p2 bytes_len =
+ let generate len = pseparated_memories ?loc p1 len p2 len in
+ plet_len_div_size ?loc p1.term_type bytes_len generate
+
+let pcopied_memcpy ?loc p1 p2 len =
+ let j = Cil_const.make_logic_var_quant "j" Linteger in
+ let tj = tvar j in
+ let geq_0 = prel ?loc (Rle, (tinteger 0), tj) in
+ let lt_len = prel ?loc (Rlt, tj, len) in
+ let bounds = pand ?loc (geq_0, lt_len) in
+ let p1_j = tplus ?loc p1 tj in
+ let p1_acc = term ?loc (TLval(TMem(p1_j), TNoOffset)) (ttype_of_pointed p1.term_type) in
+ let p2_j = tplus ?loc p2 tj in
+ let p2_acc = term ?loc (TLval(TMem(p2_j), TNoOffset)) (ttype_of_pointed p2.term_type) in
+ let eq = prel ?loc (Req, p1_acc, p2_acc) in
+ pforall ?loc ([j], (pimplies ?loc (bounds, eq)))
+
+let pcopied_len_bytes ?loc p1 p2 bytes_len =
+ plet_len_div_size ?loc p1.term_type bytes_len (pcopied_memcpy ?loc p1 p2)
+
+let generate_requires loc dest src len =
+ List.map new_predicate [
+ { (pcorrect_len_bytes ~loc dest.term_type len) with pred_name = ["aligned_end"] } ;
+ { (pvalid_len_bytes ~loc here_label dest len) with pred_name = ["valid_dest"] } ;
+ { (pvalid_read_len_bytes ~loc here_label src len) with pred_name = ["valid_read_src"] } ;
+ { (pseparated_memcpy_len_bytes ~loc dest src len) with pred_name = ["separation"] }
+ ]
+
+let generate_assigns loc t dest src len =
+ let dest_range = new_identified_term (tunref_range ~loc dest len) in
+ let src_range = new_identified_term(tunref_range ~loc src len) in
+ let copy = dest_range, From [src_range] in
+ let result = new_identified_term (tresult t) in
+ let dest = new_identified_term dest in
+ let res = result, From [dest] in
+ Writes [ copy ; res ]
+
+let generate_ensures loc dest src len =
+ List.map (fun p -> Normal, new_predicate p) [
+ { (pcopied_len_bytes ~loc dest src len) with pred_name = [ "copied"] }
+ ]
+
+let generate_spec loc kf cdest csrc clen =
+ Kernel.feedback "Spec for: %a" Kernel_function.pretty kf ;
+ let t = cdest.vtype in
+ let dest = cvar_to_tvar cdest in
+ let src = cvar_to_tvar csrc in
+ let len = cvar_to_tvar clen in
+ let requires = generate_requires loc dest src len in
+ let assigns = generate_assigns loc t dest src len in
+ let ensures = generate_ensures loc dest src len in
+ Annotations.add_requires Options.emitter kf requires ;
+ Annotations.add_assigns ~keep_empty:false Options.emitter kf assigns ;
+ Annotations.add_ensures Options.emitter kf ensures ;
+ ()
+
+let finalize_override vi loc =
+ let spec = Cil.empty_funspec () in
+ Globals.Functions.replace_by_declaration spec vi loc ;
+ let kf = Globals.Functions.get vi in
+ let (dest, src, len) = match Cil.getFormalsDecl vi with
+ | [ dest ; src ; len ] -> dest, src, len
+ | _ -> assert false
+ in
+ generate_spec loc kf dest src len ;
+ spec, vi
+
+let generate_prototype t =
+ let name = function_name ^ "_" ^ (string_of_typ t) in
+ let dt = ptr_of (restrict_of t) in
+ let st = ptr_of (restrict_of (const_of t)) in
+ let params = [
+ ("dest", dt, []) ;
+ ("src", st, []) ;
+ ("len", size_t (), [])
+ ] in
+ let fun_t = TFun(dt, Some params, false, []) in
+ let vi = Cil.makeGlobalVar ~referenced:true name fun_t in
+ Cil.setFormalsDecl vi fun_t ;
+ vi
+
+let get_override t = try
+ Hashtbl.find table t
+ with Not_found ->
+ let fct = generate_prototype t in
+ Hashtbl.add table t fct ;
+ fct
+
+let memcpy_type_from_parameter x =
+ let x = Cil.stripCasts x in
+ let xt = Cil.unrollTypeDeep (Cil.typeOf x) in
+ let xt = Cil.type_remove_qualifier_attributes_deep xt in
+ Cil.typeOf_pointed xt
+
+let well_typed_parameters dest src =
+ let dt = memcpy_type_from_parameter dest in
+ let st = memcpy_type_from_parameter src in
+ Cil_datatype.Typ.equal dt st
+
+let create_call fct (dest, src, len) =
+ if well_typed_parameters dest src then
+ let typ = memcpy_type_from_parameter dest in
+ let fct = get_override typ in
+ let dest = Cil.stripCasts dest in
+ let src = Cil.stripCasts src in
+ fct, (dest, src, len)
+ else
+ fct, (dest, src, len)
+
+let replace_call = function
+ | Call(r, ({ enode = Lval((Var fct), NoOffset) } as e), [ dest ; src ; len ], loc) ->
+ let fct, (dest, src, len) = create_call fct (dest, src, len) in
+ Call(r, { e with enode = Lval((Var fct), NoOffset) }, [ dest ; src ; len ], loc)
+ | Local_init(r, ConsInit(fct, [ dest ; src ; len ], Plain_func), loc) ->
+ let fct, (dest, src, len) = create_call fct (dest, src, len) in
+ Local_init(r, ConsInit(fct, [ dest ; src ; len ], Plain_func), loc)
+ | _ -> assert false
+
+let get_globals loc =
+ let add_global _ vi l =
+ let spec, vi = finalize_override vi loc in
+ GFunDecl(spec, vi, loc) :: l
+ in
+ Hashtbl.fold add_global table []
+
+let () = Transform.register (module struct
+ let function_name = function_name
+ let replace_call = replace_call
+ let get_globals = get_globals
+ let reset () = Hashtbl.reset table
+ end)
\ No newline at end of file
diff --git a/src/plugins/override_std/memcpy.mli b/src/plugins/override_std/memcpy.mli
new file mode 100644
index 00000000000..fa8f3783c35
--- /dev/null
+++ b/src/plugins/override_std/memcpy.mli
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
diff --git a/src/plugins/override_std/options.ml b/src/plugins/override_std/options.ml
new file mode 100644
index 00000000000..b52116a613b
--- /dev/null
+++ b/src/plugins/override_std/options.ml
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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 name = "Override Std"
+let shortname = "override-std"
+
+include Plugin.Register
+ (struct
+ let name = name
+ let shortname = shortname
+ let help = "Overrides standard library functions"
+ end)
+
+module Enabled = True
+ (struct
+ let option_name = "-override-std-perform"
+ let help = ""
+ end)
+
+let emitter = Emitter.create shortname [Emitter.Funspec] ~correctness:[] ~tuning:[]
\ No newline at end of file
diff --git a/src/plugins/override_std/options.mli b/src/plugins/override_std/options.mli
new file mode 100644
index 00000000000..0e4d28155f8
--- /dev/null
+++ b/src/plugins/override_std/options.mli
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+include Plugin.General_services
+
+module Enabled : Parameter_sig.Bool
+
+val emitter: Emitter.t
diff --git a/src/plugins/override_std/register.ml b/src/plugins/override_std/register.ml
new file mode 100644
index 00000000000..96a7d82bdb9
--- /dev/null
+++ b/src/plugins/override_std/register.ml
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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 category = File.register_code_transformation_category "override-std"
+
+let () =
+ let perform file =
+ if Options.Enabled.get () then
+ Transform.transform file
+ in
+ File.add_code_transformation_after_cleanup category perform
diff --git a/src/plugins/override_std/transform.ml b/src/plugins/override_std/transform.ml
new file mode 100644
index 00000000000..1fd8c90224d
--- /dev/null
+++ b/src/plugins/override_std/transform.ml
@@ -0,0 +1,94 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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
+
+module type Override = sig
+ val function_name: string
+ val replace_call: instr -> instr
+ val get_globals: location -> global list
+ val reset: unit -> unit
+end
+
+let base : (string, (module Override)) Hashtbl.t = Hashtbl.create 17
+
+let register ((module M: Override) as m) =
+ Hashtbl.add base M.function_name m
+
+let reset_tables () =
+ let reset _ m = let module M = (val m: Override) in M.reset () in
+ Hashtbl.iter reset base
+
+let get_globals loc =
+ let get_globals m =
+ let module M = (val m: Override) in
+ M.get_globals loc
+ in
+ Hashtbl.fold (fun _ v l -> (get_globals v) @ l) base []
+
+let called_function = function
+ | Call(_, { enode = Lval((Var fct), NoOffset) }, _, _)
+ | Local_init(_, ConsInit(fct, _, Plain_func), _) -> fct
+ | _ -> assert false
+
+let called_function_name inst =
+ let fct = called_function inst in fct.vname
+
+let find_stdlib_attr_in_call inst =
+ let fct = called_function inst in
+ if not (Cil.hasAttribute "fc_stdlib" fct.vattr) then raise Not_found
+
+let replace_call inst =
+ try
+ find_stdlib_attr_in_call inst ;
+ let name = called_function_name inst in
+ let m = Hashtbl.find base name in
+ let module M = (val m: Override) in
+ M.replace_call inst
+ with Not_found -> inst
+
+class visitor = object(_)
+ inherit Visitor.frama_c_inplace
+
+ method! vfile _ =
+ let after f =
+ let loc = Cil.CurrentLoc.get() in
+ let globals = get_globals loc in
+ f.globals <- globals @ f.globals ;
+ reset_tables () ;
+ Ast.mark_as_changed () ;
+ f
+ in
+ Cil.DoChildrenPost after
+
+ method! vinst = function
+ | Call(_) | Local_init(_, ConsInit(_, _, Plain_func), _) ->
+ let change = function
+ | [i] -> [ replace_call i ]
+ | _ -> assert false
+ in
+ Cil.DoChildrenPost change
+ | _ -> Cil.DoChildren
+end
+
+let transform file =
+ Visitor.visitFramacFile (new visitor) file
\ No newline at end of file
diff --git a/src/plugins/override_std/transform.mli b/src/plugins/override_std/transform.mli
new file mode 100644
index 00000000000..dcf037b5b1a
--- /dev/null
+++ b/src/plugins/override_std/transform.mli
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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
+
+module type Override = sig
+ val function_name: string
+ val replace_call: instr -> instr
+ val get_globals: location -> global list
+ val reset: unit -> unit
+end
+val register: (module Override) -> unit
+
+val transform: Cil_types.file -> unit
\ No newline at end of file
--
GitLab