Newer
Older
(**************************************************************************)
(* *)
(* 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
(* ************************************************************************** *)
(* ************************************************************************** *)
(* 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
(* True if a named function has a definition and false otherwise *)
let has_fundef exp = match exp.enode with
| Lval(Var vi, _) ->
let kf =
try Globals.Functions.get vi
with Not_found -> Options.fatal "[has_fundef] not a function"
in
Kernel_function.is_definition kf
| Lval _ (* function pointer *) ->
false
| _ ->
Options.fatal "[has_fundef] not a left-value: '%a'" Printer.pp_exp exp
(* ************************************************************************** *)
(* ************************************************************************** *)

Julien Signoles
committed
module RTL = 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_"
Kostyantyn Vorobyov
committed
(* prefix of all builtin functions/variables from the public E-ACSL API,
Builtin functions replace original calls in programs. *)
let e_acsl_builtin_prefix = e_acsl_api_prefix ^ "builtin_"
(* 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
Kostyantyn Vorobyov
committed
let get_rtl_replacement_name fn = e_acsl_builtin_prefix ^ fn
let has_rtl_replacement = function
| "strcpy" | "strncpy" | "strlen" | "strcat" | "strncat" | "strcmp"
| "strncmp" | "memcpy" | "memset" | "memcmp" | "memmove" -> true
| _ -> false

Julien Signoles
committed
end
(* ************************************************************************** *)
(* ************************************************************************** *)

Julien Signoles
committed
module Libc = 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 actual_alloca = "__builtin_alloca"
let is_alloca_name name = name = "alloca" || name = actual_alloca
let is_memcpy_name name = name = "memcpy"
let is_memset_name name = name = "memset"
let apply_fn f exp = match exp.enode with
| Lval(Var vi, _) -> f vi.vname
| Lval _ (* function pointer *) -> false
| _ -> Options.fatal "[Functions.Rtl.apply_fn] not a left-value"
let is_dyn_alloc exp = apply_fn is_dyn_alloc_name exp
let is_dyn_free exp = apply_fn is_dyn_free_name exp
let is_vla_alloc exp = apply_fn is_vla_alloc_name exp
let is_vla_free exp = apply_fn is_vla_free_name exp
let is_alloca exp = apply_fn is_alloca_name exp
let is_memcpy exp = apply_fn is_memcpy_name exp
let is_memset exp = apply_fn is_memset_name exp
Kostyantyn Vorobyov
committed
let printf_fmt_position = function
| "printf" -> 1
| "syslog" | "dprintf" | "fprintf" | "sprintf" -> 2
| "snprintf" -> 3
| _ -> 0
let is_printf_name name = printf_fmt_position name <> 0
let is_printf exp = apply_fn is_printf_name exp
Kostyantyn Vorobyov
committed
let get_printf_argument_str ~loc fn args =
assert (is_printf_name fn);
(* drop first n elements from a list *)
let rec drop n l =
assert (n >= 0);

Julien Signoles
committed
if n > 0 then
let l = match l with _ :: e -> e | [] -> [] in
drop (n-1) l
else
l
Kostyantyn Vorobyov
committed
in
(* get a character representing an integer type *)
let get_ikind_str = function
| IInt -> "d" (* [int] *)
| IUInt -> "D" (* [unsigned int] *)
| ILong -> "l" (* [long] *)
| IULong -> "L" (* [unsigned long] *)
| ILongLong -> "r" (* [long long] *)
| IULongLong -> "R" (* [unsigned long long] *)
(* _Bool, char and short (either signed or unsigned are promoted to
int) *)
Kostyantyn Vorobyov
committed
| IBool | IChar | ISChar | IUChar | IShort | IUShort -> "d"
in

Julien Signoles
committed
(* get a character representing a floating point type *)
Kostyantyn Vorobyov
committed
let get_fkind_str = function
(* Format-based functions expect only double-precision floats.
Single-precision floating points are promoted to doubles so
this case should never happen in fact. *)

Julien Signoles
committed
| FFloat -> assert false (* "f" *) (* [float] *)
Kostyantyn Vorobyov
committed
| FDouble -> "e" (* [float/double] *)
| FLongDouble -> "E" (* [long double] *)
in
(* get a character representing a pointer type *)
let get_pkind_str ty = match ty with
| TInt(IChar,_) | TInt(ISChar,_) -> "s" (* [char*] *)
| TInt(IUChar,_) -> "S" (* [unsigned char*] *)
| TInt(IShort,_) -> "q" (* [short*] *)
| TInt(IUShort,_) -> "Q" (* [unsigned short*] *)
| TInt(IInt,_) -> "i" (* [int*] *)
| TInt(IUInt,_) -> "I" (* [unsigned int*] *)
| TInt(ILong,_) -> "z" (* [long int*] *)
| TInt(IULong,_) -> "Z" (* [unsigned long int*] *)
| TInt(ILongLong,_) -> "w" (* [long int*] *)
| TInt(IULongLong,_) -> "W" (* [unsigned long int*] *)
| TVoid _ -> "p" (* [void*] *)

Julien Signoles
committed
| _ ->
Options.fatal "Unexpected argument type in printf: %a @."
Printer.pp_typ ty
Kostyantyn Vorobyov
committed
in
let exps = drop (printf_fmt_position fn) args in

Julien Signoles
committed
let param_str =
List.fold_right
(fun exp acc -> match Cil.unrollType (Cil.typeOf exp) with
| TInt(k, _) -> get_ikind_str k ^ acc
| TFloat(k, _) -> get_fkind_str k ^ acc
| TPtr(ty, _) -> get_pkind_str (Cil.unrollType ty) ^ acc
Kostyantyn Vorobyov
committed
| TVoid _ | TArray _ | TFun _ | TNamed _ | TComp _ | TEnum _
| TBuiltin_va_list _ -> assert false)

Julien Signoles
committed
exps
""
in
Cil.mkString ~loc param_str