Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
58fd9dd4
Commit
58fd9dd4
authored
Feb 20, 2018
by
Julien Signoles
Browse files
[Functions] minor refactoring
parent
73c33a2e
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/plugins/e-acsl/functions.ml
View file @
58fd9dd4
...
...
@@ -23,8 +23,9 @@
open
Cil_types
(* ************************************************************************** *)
(* Misc functions
{{{
*)
(* 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
...
...
@@ -42,23 +43,21 @@ let strip_prefix p s =
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
(* }}} *)
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
(* ************************************************************************** *)
(* RTL functions
{{{
*)
(* RTL functions *)
(* ************************************************************************** *)
module
RTL
:
sig
...
...
@@ -116,10 +115,9 @@ end = struct
|
"strncmp"
|
"memcpy"
|
"memset"
|
"memcmp"
|
"memmove"
->
true
|
_
->
false
end
(* }}} *)
(* ************************************************************************** *)
(* Libc functions
{{{
*)
(* Libc functions *)
(* ************************************************************************** *)
module
Libc
:
sig
...
...
@@ -143,36 +141,33 @@ module Libc: sig
val
get_printf_argument_str
:
loc
:
location
->
string
->
exp
list
->
exp
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_alloca_name
name
=
name
=
"alloca"
||
name
=
actual_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
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_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
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
let
printf_fmt_position
=
function
|
"printf"
->
1
...
...
@@ -181,8 +176,7 @@ end = struct
|
_
->
0
let
is_printf_name
name
=
printf_fmt_position
name
<>
0
let
is_printf
exp
=
is_fn
is_printf_name
exp
let
is_printf
exp
=
apply_fn
is_printf_name
exp
let
get_printf_argument_str
~
loc
fn
args
=
assert
(
is_printf_name
fn
);
...
...
@@ -200,7 +194,8 @@ end = struct
|
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) *)
(* _Bool, char and short (either signed or unsigned are promoted to
int) *)
|
IBool
|
IChar
|
ISChar
|
IUChar
|
IShort
|
IUShort
->
"d"
in
(* get a character representing an floating point type *)
...
...
@@ -241,4 +236,3 @@ end = struct
exps
in
Cil
.
mkString
~
loc
param_str
end
(* }}} *)
src/plugins/e-acsl/functions.mli
View file @
58fd9dd4
...
...
@@ -22,9 +22,6 @@
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 *)
...
...
@@ -34,25 +31,27 @@ val has_fundef: exp -> bool
(* ************************************************************************** *)
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_])
*)
it as belonging to the public API of E-ACSL runtime library *)
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_])
. *)
with temporal analysis. *)
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_]) *)
that this name has been generated during instrumentation phase. *)
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_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 *)
...
...
@@ -61,9 +60,6 @@ module RTL: sig
(** 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. *)
...
...
@@ -75,13 +71,15 @@ module RTL: sig
val
has_rtl_replacement
:
string
->
bool
(** Given the name of C library function return true if there is a drop-in
replacement function for it in the RTL. *)
end
end
(* Rtl *)
(* ************************************************************************** *)
(** {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 *)
...
...
@@ -145,11 +143,11 @@ module Libc: sig
arguments. *)
val
get_printf_argument_str
:
loc
:
location
->
string
->
exp
list
->
exp
(** Given the name of a printf-like function
([string])
and the list
of its variadic arguments [exp list]
return a literal string expression
where each character
describes the type of an argument from a list.
Such characters are also
called abbreviated types. Conversion between
abbreviated and C types
characters is as follows:
(** Given the name of a printf-like function and the list
of its variadic
arguments
return a literal string expression
where each character
describes the type of an argument from a list.
Such characters are also
called abbreviated types. Conversion between
abbreviated and C types
characters is as follows:
- "b" -> [_Bool]
- "c" -> [signed char]
- "C" -> [unsigned char]
...
...
@@ -171,4 +169,5 @@ module Libc: sig
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
end
(* Libc *)
src/plugins/e-acsl/temporal.ml
View file @
58fd9dd4
...
...
@@ -317,15 +317,18 @@ end = struct
(* Update local environment with a statement tracking temporal metadata
associated with memcpy/memset call *)
let
call_memxxx
current_stmt
loc
args
fname
env
=
if
Libc
.
is_memcpy
fname
||
Libc
.
is_memset
fname
then
let
name
=
Functions
.
get_fname_exp
fname
in
let
call_memxxx
current_stmt
loc
args
fexp
env
=
if
Libc
.
is_memcpy
fexp
||
Libc
.
is_memset
fexp
then
let
name
=
match
fexp
.
enode
with
|
Lval
(
Var
vi
,
_
)
->
vi
.
vname
|
_
->
Options
.
fatal
"[Temporal.call_memxxx] not a left-value"
in
let
stmt
=
Misc
.
mk_call
~
loc
(
RTL
.
mk_temporal_name
name
)
args
in
Env
.
add_stmt
~
before
:
current_stmt
~
post
:
false
env
stmt
else
env
let
instr
current_stmt
ret
f
name
args
loc
env
=
let
instr
current_stmt
ret
f
exp
args
loc
env
=
(* Add function calls to reset_parameters and reset_return before each
function call regardless. They are not really required, as if the
instrumentation is correct then the right parameters will be saved
...
...
@@ -340,15 +343,15 @@ end = struct
let
env
=
Env
.
add_stmt
~
before
:
current_stmt
~
post
:
false
env
stmt
in
(* Push parameters with either a call to a function pointer or a function
definition otherwise there is no point. *)
let
has_def
=
Functions
.
has_fundef
f
name
in
let
has_def
=
Functions
.
has_fundef
f
exp
in
let
env
=
if
Cil
.
isFunctionType
(
Cil
.
typeOf
f
name
)
||
has_def
then
if
Cil
.
isFunctionType
(
Cil
.
typeOf
f
exp
)
||
has_def
then
save_params
current_stmt
loc
args
env
else
env
in
(* Handle special cases of memcpy/memset *)
let
env
=
call_memxxx
current_stmt
loc
args
f
name
env
in
let
env
=
call_memxxx
current_stmt
loc
args
f
exp
env
in
(* Memory allocating functions have no definitions so below expression
should capture them *)
let
alloc
=
not
has_def
in
...
...
@@ -386,10 +389,10 @@ end = struct
match
li
with
|
AssignInit
init
->
handle_init
current_stmt
NoOffset
loc
vi
init
env
|
ConsInit
(
f
name
,
args
,
_
)
->
|
ConsInit
(
f
exp
,
args
,
_
)
->
let
ret
=
Some
(
Cil
.
var
vi
)
in
let
f
name
=
Cil
.
evar
~
loc
f
name
in
Function_call
.
instr
current_stmt
ret
f
name
args
loc
env
let
f
exp
=
Cil
.
evar
~
loc
f
exp
in
Function_call
.
instr
current_stmt
ret
f
exp
args
loc
env
else
env
end
(* }}} *)
...
...
@@ -446,8 +449,8 @@ let handle_return_stmt loc ret env =
let
handle_instruction
current_stmt
instr
env
=
match
instr
with
|
Set
(
lv
,
exp
,
loc
)
->
set_instr
current_stmt
loc
lv
exp
env
|
Call
(
ret
,
f
name
,
args
,
loc
)
->
Function_call
.
instr
current_stmt
ret
f
name
args
loc
env
|
Call
(
ret
,
f
exp
,
args
,
loc
)
->
Function_call
.
instr
current_stmt
ret
f
exp
args
loc
env
|
Local_init
(
vi
,
li
,
loc
)
->
Local_init
.
instr
current_stmt
vi
li
loc
env
|
Asm
_
->
Options
.
warning
~
once
:
true
~
current
:
true
"@[Analysis is\
potentially incorrect in presence of assembly code.@]"
;
env
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment