Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
75d3f505
Commit
75d3f505
authored
1 year ago
by
Jan Rochel
Browse files
Options
Downloads
Patches
Plain Diff
[alias] correctly expose Abstract_state including graph
parent
a1c78b46
No related branches found
No related tags found
No related merge requests found
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
src/plugins/alias/API.mli
+51
-3
51 additions, 3 deletions
src/plugins/alias/API.mli
src/plugins/alias/abstract_state.ml
+0
-16
0 additions, 16 deletions
src/plugins/alias/abstract_state.ml
src/plugins/alias/abstract_state.mli
+46
-62
46 additions, 62 deletions
src/plugins/alias/abstract_state.mli
with
97 additions
and
81 deletions
src/plugins/alias/API.mli
+
51
−
3
View file @
75d3f505
...
...
@@ -25,6 +25,7 @@
open
Cil_types
module
LSet
=
Cil_datatype
.
LvalStructEq
.
Set
module
G
:
Graph
.
Sig
.
G
with
type
V
.
t
=
int
(** NB : do the analysis BEFORE using any of those functions *)
...
...
@@ -89,17 +90,64 @@ val are_aliased: kernel_function -> stmt -> lval -> lval -> bool
(** [fold_vertex f acc kf s v] folds [f acc i lv] to all [lv] in [i], where [i] is
the vertex that represents the equivalence class of [v] before statement [s] in function [kf]. *)
val
fold_vertex
:
(
'
a
->
in
t
->
lval
->
'
a
)
->
'
a
->
kernel_function
->
stmt
->
lval
->
'
a
(
'
a
->
G
.
V
.
t
->
lval
->
'
a
)
->
'
a
->
kernel_function
->
stmt
->
lval
->
'
a
(** [fold_vertex_closure f acc kf s v] is the transitive closure of function
[fold_vertex]. *)
val
fold_vertex_closure
:
(
'
a
->
in
t
->
lval
->
'
a
)
->
'
a
->
kernel_function
->
stmt
->
lval
->
'
a
(
'
a
->
G
.
V
.
t
->
lval
->
'
a
)
->
'
a
->
kernel_function
->
stmt
->
lval
->
'
a
(** direct access to the abstract state. See Abstract_state.mli *)
module
Abstract_state
:
Abstract_state
.
S
module
Abstract_state
:
sig
(** Type denothing an abstract state of the analysis. It is a graph containing
all aliases and points-to information. *)
type
t
(** access to the points-to graph *)
val
get_graph
:
t
->
G
.
t
(** set of lvals stored in a vertex *)
val
get_lval_set
:
G
.
V
.
t
->
t
->
LSet
.
t
(** pretty printer; debug=true prints the graph, debug = false only
prints aliased variables *)
val
pretty
:
?
debug
:
bool
->
Format
.
formatter
->
t
->
unit
(** dot printer; first argument is a file name *)
val
print_dot
:
string
->
t
->
unit
(** finds the vertex corresponding to a lval.
@raise Not_found if such a vertex does not exist
*)
val
find_vertex
:
lval
->
t
->
G
.
V
.
t
(** same as previous function, but return a set of lval. Cannot
raise an exception but may return an empty set if the lval is not
in the graph *)
val
find_aliases
:
lval
->
t
->
LSet
.
t
(** similar to the previous functions, but does not only give the
equivalence class of lv, but also all lv that are aliases in
other vertex of the graph *)
val
find_all_aliases
:
lval
->
t
->
LSet
.
t
(** the set of all lvars to which the given variable may point. *)
val
points_to_set
:
lval
->
t
->
LSet
.
t
(** find_aliases, then recursively finds other sets of lvals. We
have the property (if lval [lv] is in abstract state [x]) :
List.hd (find_transitive_closure lv x) = (find_vertex lv x,
find_aliases lv x) *)
val
find_transitive_closure
:
lval
->
t
->
(
G
.
V
.
t
*
LSet
.
t
)
list
(** inclusion test; [is_included a1 a2] tests if, for any lvl
present in a1 (associated to a vertex v1), that it is also
present in a2 (associated to a vertex v2) and that
get_lval_set(succ(v1) is included in get_lval_set(succ(v2)) *)
val
is_included
:
t
->
t
->
bool
end
(** [get_state_before_stmt f s] gets the abstract state computed after
statement [s] in function [f]. Returns [None] if
...
...
This diff is collapsed.
Click to expand it.
src/plugins/alias/abstract_state.ml
+
0
−
16
View file @
75d3f505
...
...
@@ -111,22 +111,6 @@ struct
end
module
type
S
=
sig
(* see abstract_state.mli for coments *)
type
t
val
get_graph
:
t
->
G
.
t
val
get_lval_set
:
G
.
V
.
t
->
t
->
LSet
.
t
val
pretty
:
?
debug
:
bool
->
Format
.
formatter
->
t
->
unit
val
print_dot
:
string
->
t
->
unit
val
find_vertex
:
lval
->
t
->
G
.
V
.
t
val
find_aliases
:
lval
->
t
->
LSet
.
t
val
find_all_aliases
:
lval
->
t
->
LSet
.
t
val
points_to_set
:
lval
->
t
->
LSet
.
t
val
find_transitive_closure
:
lval
->
t
->
(
G
.
V
.
t
*
LSet
.
t
)
list
val
is_included
:
t
->
t
->
bool
end
type
t
=
{
graph
:
G
.
t
;
lmap
:
LLMap
.
t
;
(* lmap(lv) is a table [offset->v] where the vertex v corresponding to lval (lv+offset), in other words (lv+offset) is in label(v) *)
...
...
This diff is collapsed.
Click to expand it.
src/plugins/alias/abstract_state.mli
+
46
−
62
View file @
75d3f505
...
...
@@ -30,61 +30,52 @@ module G: Graph.Sig.G with type V.t = int
module
LSet
=
Cil_datatype
.
LvalStructEq
.
Set
module
LMap
=
Cil_datatype
.
LvalStructEq
.
Map
(** external signature *)
module
type
S
=
sig
(** Type denothing an abstract state of the analysis. It is a graph containing
all aliases and points-to information. *)
type
t
(** access to the points-to graph *)
val
get_graph
:
t
->
G
.
t
(** set of lvals stored in a vertex *)
val
get_lval_set
:
G
.
V
.
t
->
t
->
LSet
.
t
(** pretty printer; debug=true prints the graph, debug = false only
prints aliased variables *)
val
pretty
:
?
debug
:
bool
->
Format
.
formatter
->
t
->
unit
(** dot printer; first argument is a file name *)
val
print_dot
:
string
->
t
->
unit
(** finds the vertex corresponding to a lval.
@raise Not_found if such a vertex does not exist
*)
val
find_vertex
:
lval
->
t
->
G
.
V
.
t
(** same as previous function, but return a set of lval. Cannot
raise an exception but may return an empty set if the lval is not
in the graph *)
val
find_aliases
:
lval
->
t
->
LSet
.
t
(** similar to the previous functions, but does not only give the
equivalence class of lv, but also all lv that are aliases in
other vertex of the graph *)
val
find_all_aliases
:
lval
->
t
->
LSet
.
t
(** the set of all lvars to which the given variable may point. *)
val
points_to_set
:
lval
->
t
->
LSet
.
t
(** find_aliases, then recursively finds other sets of lvals. We
have the property (if lval [lv] is in abstract state [x]) :
List.hd (find_transitive_closure lv x) = (find_vertex lv x,
find_aliases lv x) *)
val
find_transitive_closure
:
lval
->
t
->
(
G
.
V
.
t
*
LSet
.
t
)
list
(** inclusion test; [is_included a1 a2] tests if, for any lvl
present in a1 (associated to a vertex v1), that it is also
present in a2 (associated to a vertex v2) and that
get_lval_set(succ(v1) is included in get_lval_set(succ(v2)) *)
val
is_included
:
t
->
t
->
bool
end
include
S
(** Type denothing an abstract state of the analysis. It is a graph containing
all aliases and points-to information. *)
type
t
(** access to the points-to graph *)
val
get_graph
:
t
->
G
.
t
(** set of lvals stored in a vertex *)
val
get_lval_set
:
G
.
V
.
t
->
t
->
LSet
.
t
(** pretty printer; debug=true prints the graph, debug = false only
prints aliased variables *)
val
pretty
:
?
debug
:
bool
->
Format
.
formatter
->
t
->
unit
(** dot printer; first argument is a file name *)
val
print_dot
:
string
->
t
->
unit
(** finds the vertex corresponding to a lval.
@raise Not_found if such a vertex does not exist
*)
val
find_vertex
:
lval
->
t
->
G
.
V
.
t
(** same as previous function, but return a set of lval. Cannot
raise an exception but may return an empty set if the lval is not
in the graph *)
val
find_aliases
:
lval
->
t
->
LSet
.
t
(** similar to the previous functions, but does not only give the
equivalence class of lv, but also all lv that are aliases in
other vertex of the graph *)
val
find_all_aliases
:
lval
->
t
->
LSet
.
t
(** the set of all lvars to which the given variable may point. *)
val
points_to_set
:
lval
->
t
->
LSet
.
t
(** find_aliases, then recursively finds other sets of lvals. We
have the property (if lval [lv] is in abstract state [x]) :
List.hd (find_transitive_closure lv x) = (find_vertex lv x,
find_aliases lv x) *)
val
find_transitive_closure
:
lval
->
t
->
(
G
.
V
.
t
*
LSet
.
t
)
list
(** inclusion test; [is_included a1 a2] tests if, for any lvl
present in a1 (associated to a vertex v1), that it is also
present in a2 (associated to a vertex v2) and that
get_lval_set(succ(v1) is included in get_lval_set(succ(v2)) *)
val
is_included
:
t
->
t
->
bool
(** check all the invariants that must be true on an abstract value
before and after each function call or transformation of the graph) *)
...
...
@@ -99,13 +90,6 @@ val assignment : t -> lval -> exp -> t
(** transfert function for malloc calls *)
val
assignment_x_allocate_y
:
t
->
lval
->
t
(** inclusion test; [is_included a1 a2] tests if, for any lvl present
in a1 (associated to a vertex v1), that it is also present in a2
(associated to a vertex v2) and that set(succ(v1) is included in
set(succ(v2)) *)
val
is_included
:
t
->
t
->
bool
(** union of two abstract values ; ensures that if 2 lval are
aliased in one of the two input graph (or in a points-to
relationship), then they will also be aliased/points-to in the
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment