Commit d53caa3e authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov Committed by Julien Signoles
Browse files

Refactoring operations on functions into their own module

parent 4f5b36bb
......@@ -62,6 +62,7 @@ PLUGIN_CMO:= local_config \
rte \
error \
builtins \
functions \
misc \
gmpz \
literal_strings \
......@@ -84,7 +85,6 @@ PLUGIN_CMO:= local_config \
PLUGIN_HAS_MLI:=yes
PLUGIN_DISTRIBUTED:=yes
# We "save" this variable so that it can be used once PLUGIN_DIR has been reset
EACSL_PLUGIN_DIR:=$(PLUGIN_DIR)
......
......@@ -124,7 +124,7 @@ let dup_fundec loc spec bhv kf vi new_vi =
(* unamed formal parameter: must generate a fresh name since a fundec
cannot have unnamed formals (see bts #2303). *)
Env.Varname.get ~scope:Env.Function
(Misc.mk_gen_name "unamed_formal")
(Functions.RTL.mk_gen_name "unamed_formal")
else
vi.vname
in
......@@ -269,7 +269,7 @@ class dup_functions_visitor prj = object (self)
(Extlib.the self#current_kf)))
->
self#next ();
let name = Misc.mk_gen_name vi.vname in
let name = Functions.RTL.mk_gen_name vi.vname in
let new_vi =
Project.on prj (Cil.makeGlobalVar name) vi.vtype
in
......
......@@ -181,7 +181,7 @@ let do_new_var ~loc init ?(scope=Local_block) ?(name="") env t ty mk_stmts =
~source:true
false (* is a global? *)
false (* is a formal? *)
(Varname.get ~scope (Misc.mk_gen_name name))
(Varname.get ~scope (Functions.RTL.mk_gen_name name))
ty
in
v.vreferenced <- true;
......
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
open Cil_types
(* ************************************************************************** *)
(* Misc functions {{{ *)
(* ************************************************************************** *)
(* return true if the string s starts with prefix p and false otherwise *)
let startswith p s =
let lp = String.length p in
if lp <= String.length s then
p = String.sub s 0 lp
else
false
(* if string s is prefixed with string p, then return s without p, otherwise
* return s as is *)
let strip_prefix p s =
let lp = String.length p in
if startswith p s then
String.sub s lp (String.length s - lp)
else
s
let get_fname_exp = function
| { enode = Lval(Var(vi), _) } -> vi.vname
| _ -> ""
let is_fn f exp = f (get_fname_exp exp)
(* True if a named function has a definition and false otherwise *)
let has_fundef exp =
let recognize fname =
try let _ = Globals.Functions.find_def_by_name fname in true
with Not_found -> false
in
is_fn recognize exp
(* }}} *)
(* ************************************************************************** *)
(* RTL functions {{{ *)
(* ************************************************************************** *)
module RTL: sig
val mk_api_name: string -> string
val mk_temporal_name: string -> string
val mk_gen_name: string -> string
val is_generated_name: string -> bool
val is_rtl_name: string -> bool
val is_generated_literal_string_name: string -> bool
val is_generated_kf: kernel_function -> bool
val get_original_name: kernel_function -> string
end = struct
(* prefix of all functions/variables from the public E-ACSL API *)
let e_acsl_api_prefix = "__e_acsl_"
(* prefix of temporal analysis functions of the public E-ACSL API *)
let e_acsl_temporal_prefix = e_acsl_api_prefix ^ "temporal_"
(* prefix of functions/variables generated by E-ACSL *)
let e_acsl_gen_prefix = "__gen_e_acsl_"
(* prefix of literal strings generated by E-ACSL *)
let e_acsl_lit_string_prefix = e_acsl_gen_prefix ^ "literal_string"
let mk_api_name fname = e_acsl_api_prefix ^ fname
let mk_temporal_name fname = e_acsl_temporal_prefix ^ fname
let mk_gen_name name = e_acsl_gen_prefix ^ name
let get_original_name kf =
strip_prefix e_acsl_gen_prefix (Kernel_function.get_name kf)
let is_generated_name name = startswith e_acsl_gen_prefix name
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
end
(* }}} *)
(* ************************************************************************** *)
(* Libc functions {{{ *)
(* ************************************************************************** *)
module Libc: sig
val is_memcpy: exp -> bool
val is_memcpy_name: string -> bool
val is_memset: exp -> bool
val is_memset_name: string -> bool
val is_dyn_alloc: exp -> bool
val is_dyn_alloc_name: string -> bool
val is_dyn_free: exp -> bool
val is_dyn_free_name: string -> bool
val is_vla_free: exp -> bool
val is_vla_free_name: string -> bool
val is_vla_alloc: exp -> bool
val is_vla_alloc_name: string -> bool
val is_alloca: exp -> bool
val is_alloca_name: string -> bool
val actual_alloca: string
end = struct
let is_dyn_alloc_name name =
name = "malloc" || name = "realloc" || name = "calloc"
let is_dyn_free_name name = name = "free" || name = "cfree"
let is_vla_alloc_name name = name = "__fc_vla_alloc"
let is_vla_free_name name = name = "__fc_vla_free"
let is_alloca_name name = name = "alloca" || name = "__builtin_alloca"
let actual_alloca = "__builtin_alloca"
let is_memcpy_name name = name = "memcpy"
let is_memset_name name = name = "memset"
let is_dyn_alloc exp = is_fn is_dyn_alloc_name exp
let is_dyn_free exp = is_fn is_dyn_free_name exp
let is_vla_alloc exp = is_fn is_vla_alloc_name exp
let is_vla_free exp = is_fn is_vla_free_name exp
let is_alloca exp = is_fn is_alloca_name exp
let is_memcpy exp = is_fn is_memcpy_name exp
let is_memset exp = is_fn is_memset_name exp
end
(* }}} *)
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
open Cil_types
val get_fname_exp: exp -> string
(** Provided that [exp] captures a function name return that name *)
val has_fundef: exp -> bool
(** @return [true] if a function whose name is given via [exp] is defined and
[false] otherwise *)
(* ************************************************************************** *)
(** {2 RTL} Operations on function belonging to the runtime library of E-ACSL *)
(* ************************************************************************** *)
module RTL: sig
val mk_api_name: string -> string
(** Prefix a name (of a variable or a function) with a string that identifies
it as belonging to the public API of E-ACSL runtime library ([__e_acsl_])
*)
val mk_temporal_name: string -> string
(** Prefix a name (of a variable or a function) with a string that identifies
it as belonging to the public API of E-ACSL runtime library dealing
with temporal analysis ([__e_acsl_temporal_]). *)
val mk_gen_name: string -> string
(** Prefix a name (of a variable or a function) with a string indicating
that this name has been generated during instrumentation phase.
([__gen_e_acsl_]) *)
val is_generated_name: string -> bool
(** @return [true] if the prefix of the given name indicates that it has been
generated by E-ACSL instrumentation (see [mk_gen_name] function). *)
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. *)
val is_generated_kf: kernel_function -> bool
(** Same as [is_generated_name] but for kernel functions *)
val get_original_name: kernel_function -> string
(** Retrieve the name of the kernel function and strip prefix that indicates
that it has been generated by the instrumentation. *)
end
(* ************************************************************************** *)
(** {2 Libc} Operations on functions belonging to standard library *)
(* ************************************************************************** *)
module Libc: sig
val is_memcpy: exp -> bool
(** Return [true] if [exp] captures a function name that matches [memcpy] or
an equivalent function *)
val is_memcpy_name: string -> bool
(** Same as [is_memcpy] but for strings *)
val is_memset: exp -> bool
(** Return [true] if [exp] captures a function name that matches [memset] or
an equivalent function *)
val is_memset_name: string -> bool
(** Same as [is_memset] but for strings *)
val is_dyn_alloc: exp -> bool
(** Return [true] if [exp] captures a function name that matches a function
that dynamically allocates memory such as [malloc] or [calloc] *)
val is_dyn_alloc_name: string -> bool
(** Same as [is_dyn_alloc] but for strings *)
val is_dyn_free: exp -> bool
(** Return [true] if [exp] captures a function name that matches
a function that dynamically deallocates memory (e.g., [free]) *)
val is_dyn_free_name: string -> bool
(** Same as [is_dyn_free] but for strings *)
val is_vla_free: exp -> bool
(** Return [true] if [exp] captures a function name that matches
a function that allocates memory for a variable-size array. *)
val is_vla_free_name: string -> bool
(** Return [true] if [string] captures a function name that matches
a function that deallocates memory for a variable-size array. *)
val is_vla_alloc: exp -> bool
(** Return [true] if [exp] captures a function name that matches
a function that deallocates memory for a variable-size array. *)
val is_vla_alloc_name: string -> bool
(** Same as [is_dyn_alloc] but for strings *)
val is_alloca: exp -> bool
(** Return [true] if [exp] captures a function name that matches
a function that allocates memory on stack. *)
val is_alloca_name: string -> bool
(** Same as [is_alloca] but for strings *)
val actual_alloca: string
(** The name of an actual [alloca] function used at link-time.
In GCC/Clang [alloca] is typically implemented via [__builtin_alloca] *)
end
......@@ -130,7 +130,7 @@ let must_translate kf kind =
(* function contracts have been moved from the original function to its
duplicate by [Dup_function] but they are still associated to the original
function here *)
let name = Misc.get_original_name kf in
let name = Functions.RTL.get_original_name kf in
let info =
try Datatype.String.Hashtbl.find keep_status name
with Not_found ->
......
......@@ -20,6 +20,7 @@
(* *)
(**************************************************************************)
module RTL = Functions.RTL
open Cil_types
open Cil_datatype
......@@ -102,52 +103,6 @@ let kind_to_string loc k =
| Invariant -> "Invariant"
| RTE -> "RTE")
(* prefix of functions belonging to the public API of E-ACSL *)
let e_acsl_api_prefix = "__e_acsl_"
(* prefix of functions generated by E-ACSL *)
let e_acsl_gen_prefix = "__gen_e_acsl_"
(* return true if the string s starts with prefix p and false otherwise *)
let startswith p s =
let lp = String.length p in
if lp <= String.length s then
p = String.sub s 0 lp
else
false
(* if string s is prefixed with string p, then return s without p, otherwise
* return s as is *)
let strip_prefix p s =
let lp = String.length p in
if startswith p s then
String.sub s lp (String.length s - lp)
else
s
let is_generated_varinfo vi =
startswith e_acsl_gen_prefix vi.vname
let is_generated_literal_string_varinfo vi =
startswith (e_acsl_gen_prefix ^ "literal_string") vi.vname
let is_library_name name =
startswith e_acsl_api_prefix name
let is_generated_kf kf =
let name = Kernel_function.get_vi kf in
is_generated_varinfo name
let get_original_name kf =
let name = Kernel_function.get_name kf in
strip_prefix e_acsl_gen_prefix name
let mk_api_name fname =
e_acsl_api_prefix ^ fname
let mk_gen_name name =
e_acsl_gen_prefix ^ name
(* Build a C conditional doing a runtime assertion check. *)
let mk_e_acsl_guard ?(reverse=false) kind kf e p =
let loc = p.pred_loc in
......@@ -161,10 +116,10 @@ let mk_e_acsl_guard ?(reverse=false) kind kf e p =
in
mk_call
~loc
(mk_api_name "assert")
(RTL.mk_api_name "assert")
[ e;
kind_to_string loc kind;
Cil.mkString ~loc (get_original_name kf);
Cil.mkString ~loc (RTL.get_original_name kf);
Cil.mkString ~loc msg;
Cil.integer loc line ]
......@@ -202,25 +157,25 @@ let result_vi kf = match result_lhost kf with
let mk_full_init_stmt ?(addr=true) vi =
let loc = vi.vdecl in
let mk = mk_call ~loc (RTL.mk_api_name "full_init") in
match addr, Cil.unrollType vi.vtype with
| _, TArray(_,Some _, _, _) | false, _ ->
mk_call ~loc (mk_api_name "full_init") [ Cil.evar ~loc vi ]
| _ -> mk_call ~loc (mk_api_name "full_init") [ Cil.mkAddrOfVi vi ]
| _, TArray(_,Some _, _, _) | false, _ -> mk [ Cil.evar ~loc vi ]
| _ -> mk [ Cil.mkAddrOfVi vi ]
let mk_initialize ~loc (host, offset as lv) = match host, offset with
| Var _, NoOffset -> mk_call ~loc
(mk_api_name "full_init")
(RTL.mk_api_name "full_init")
[ Cil.mkAddrOf ~loc lv ]
| _ ->
let typ = Cil.typeOfLval lv in
mk_call ~loc
(mk_api_name "initialize")
(RTL.mk_api_name "initialize")
[ Cil.mkAddrOf ~loc lv; Cil.new_exp loc (SizeOf typ) ]
let mk_named_store_stmt name ?str_size vi =
let ty = Cil.unrollType vi.vtype in
let loc = vi.vdecl in
let store = mk_call ~loc (mk_api_name name) in
let store = mk_call ~loc (RTL.mk_api_name name) in
match ty, str_size with
| TArray(_, Some _,_,_), None ->
store [ Cil.evar ~loc vi ; Cil.sizeOf ~loc ty ]
......@@ -236,14 +191,14 @@ let mk_duplicate_store_stmt ?str_size vi =
let mk_delete_stmt vi =
let loc = vi.vdecl in
let mk = mk_call ~loc (RTL.mk_api_name "delete_block") in
match Cil.unrollType vi.vtype with
| TArray(_, Some _, _, _) ->
mk_call ~loc (mk_api_name "delete_block") [ Cil.evar ~loc vi ]
| _ -> mk_call ~loc (mk_api_name "delete_block") [ Cil.mkAddrOfVi vi ]
| TArray(_, Some _, _, _) -> mk [ Cil.evar ~loc vi ]
| _ -> mk [ Cil.mkAddrOfVi vi ]
let mk_mark_readonly vi =
let loc = vi.vdecl in
mk_call ~loc (mk_api_name "mark_readonly") [ Cil.evar ~loc vi ]
mk_call ~loc (RTL.mk_api_name "mark_readonly") [ Cil.evar ~loc vi ]
(* ************************************************************************** *)
(** {2 Other stuff} *)
......@@ -255,8 +210,9 @@ let term_addr_of ~loc tlv ty =
let reorder_ast () =
let ast = Ast.get() in
let is_from_library = function
| GType(ti, _) when ti.tname = "size_t" || is_library_name ti.tname -> true
| GCompTag (ci, _) when is_library_name ci.cname -> true
| GType(ti, _) when ti.tname = "size_t"
|| RTL.is_rtl_name ti.tname -> true
| GCompTag (ci, _) when RTL.is_rtl_name ci.cname -> true
| GFunDecl(_, _, loc) | GVarDecl(_, loc) when is_library_loc loc -> true
| _ -> false in
let rtl, other = List.partition is_from_library ast.globals in
......
......@@ -97,35 +97,6 @@ val ptr_index: ?loc:location -> ?index:exp -> exp
(** Split pointer-arithmetic expression of the type `p + i` into its
pointer and integer parts. *)
(* ************************************************************************** *)
(** {2 Handling prefixes of generated library functions and variables} *)
(* ************************************************************************** *)
val mk_api_name: string -> string
(** @return given some base name append it with a prefix used
by functions and variables in the public API of E-ACSL runtime library.
([__e_acsl_]) *)
val mk_gen_name: string -> string
(** @return given some base name append it with a prefix used
by functions and variables generated by E-ACSL ([__gen_e_acsl_]). *)
val is_generated_varinfo: varinfo -> bool
(** @return true if the name of the given [varinfo] indicates that it has been
generated by E-ACSL. This is done by checking whether the name of the
varinfo has been generated using [mk_gen_name function]. *)
val is_generated_literal_string_varinfo: varinfo -> bool
(** Same as [is_generated_varinfo] but indicates that varinfo is a local
variable which replaced a literal string. *)
val is_generated_kf: kernel_function -> bool
(** Same as [is_generated_varinfo] but for kernel functions *)
val get_original_name: kernel_function -> string
(** @return the original basename of a function for generated functions, or the
identify for ungenerated ones. *)
(*
Local Variables:
compile-command: "make"
......
......@@ -400,7 +400,7 @@ let register_predicate kf pred state =
(fun state ->
let state = Env.default_varinfos state in
let state =
if (is_first || is_last) && Misc.is_generated_kf kf then
if (is_first || is_last) && Functions.RTL.is_generated_kf kf then
Annotations.fold_behaviors
(fun _ bhv s ->
let handle_annot test f s =
......
......@@ -25,6 +25,8 @@
Temporal Memory Errors" by K. Vorobyov, N. Kosmatov, J Signoles and
A. Jakobsson. *)
module RTL = Functions.RTL
module Libc = Functions.Libc
open Cil_types
open Cil_datatype
......@@ -50,38 +52,6 @@ type flow =
(* Miscellaneous {{{ *)
(* ************************************************************************** *)
(* Generate a function name in the temporal analysis name space, i.e., prefixed
by [__e_acsl_temporal_ + function name].
NOTE: Further on, all analysis function names are used without prefix *)
let mk_api_name name = Misc.mk_api_name ("temporal_" ^ name)
let is_alloc_name fn =
fn = "malloc" || fn = "free" || fn = "realloc" || fn = "calloc"
let is_memcpy_name fn = fn = "memcpy"
let is_memset_name fn = fn = "memset"
let get_fname = function
| { enode = Lval(Var(vi), _) } -> vi.vname
| _ -> ""
let is_fn f fname = f (get_fname fname)
let is_alloc fvi = is_fn is_alloc_name fvi
let is_memcpy fvi = is_fn is_memcpy_name fvi
let is_memset fvi = is_fn is_memset_name fvi
(* True if a named function has a definition and false otherwise *)
let has_fundef fname =
let recognize fn =
try let _ = Globals.Functions.find_def_by_name fn in true
with Not_found -> false
in
is_fn recognize fname
(* Shortcuts for SA in Mmodel_analysis *)
let must_model_exp exp env =
let kf, bhv = Extlib.the (Env.current_kf env), Env.get_behavior env in
......@@ -121,8 +91,8 @@ module Mk: sig
val reset_return_referent: loc:location -> stmt
(* Generate [memcpy(lhs, rhs, size)] function call assuming that [lhs = rhs]
represents an assignment of struct to a struct, that is, both sides are left
values and we need to use addressof for both sides *)
represents an assignment of struct to a struct, that is, both sides are
left values and we need to use addressof for both sides *)
val temporal_memcpy_struct: loc:location -> lval -> exp -> stmt
end = struct
......@@ -132,7 +102,8 @@ end = struct
| Indirect -> "store_nreferent"
| Copy -> Options.fatal "Copy flow type in store_reference"
in
Misc.mk_call ~loc (mk_api_name fname) [ Cil.mkAddrOf ~loc lhs; rhs ]
let fname = RTL.mk_temporal_name fname in
Misc.mk_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs ]
let save_param ~loc flow lhs pos =
let infix = match flow with
......@@ -141,11 +112,12 @@ end = struct
| Copy -> "copy"
in
let fname = "save_" ^ infix ^ "_parameter" in
Misc.mk_call ~loc (mk_api_name fname) [ lhs ; Cil.integer ~loc pos ]
let fname = RTL.mk_temporal_name fname in
Misc.mk_call ~loc fname [ lhs ; Cil.integer ~loc pos ]
let pull_param ~loc vi pos =
let exp = Cil.mkAddrOfVi vi in
let fname = mk_api_name "pull_parameter" in
let fname = RTL.mk_temporal_name "pull_parameter" in
let sz = Cil.kinteger ~loc IULong (Cil.bytesSizeOf vi.vtype) in
Misc.mk_call ~loc fname [ exp ; Cil.integer ~loc pos ; sz ]
......@@ -158,13 +130,13 @@ end = struct
(match (Cil.typeOf lhs) with
| TPtr _ -> ()
| _ -> Error.not_yet "Struct in return");
Misc.mk_call ~loc (mk_api_name fname) [ lhs ]
Misc.mk_call ~loc (RTL.mk_temporal_name fname) [ lhs ]