From 07fa63a476ae930a4d68a4ee8a24e8b94e7bf44f Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Tue, 12 Mar 2024 13:27:04 +0100
Subject: [PATCH] [alias] overhaul API
It makes no sense to reproduce all of the fold functions for sets of
variables and lvals, otherwise we should do the same for iter functions
and the like.
An API user should rather use the pre-existing functions from LSet and
VarSet. Therefore let's mark most of these functions as deprecated.
Fixes #2692
---
src/plugins/alias/src/API.ml | 120 ++++++++--------
src/plugins/alias/src/API.mli | 169 ++++++++++++++++++-----
src/plugins/alias/src/abstract_state.ml | 66 ++++++---
src/plugins/alias/src/abstract_state.mli | 70 ++++------
src/plugins/alias/src/analysis.ml | 2 +-
src/plugins/alias/src/analysis.mli | 2 +-
6 files changed, 273 insertions(+), 156 deletions(-)
diff --git a/src/plugins/alias/src/API.ml b/src/plugins/alias/src/API.ml
index 66e9f86bd08..53ae066ea24 100644
--- a/src/plugins/alias/src/API.ml
+++ b/src/plugins/alias/src/API.ml
@@ -22,12 +22,17 @@
open Cil_types
+module EdgeLabel = Abstract_state.EdgeLabel
+
(** Points-to graphs datastructure. *)
module G = Abstract_state.G
+type v = G.V.t
+
let vid = Abstract_state.vid
module LSet = Abstract_state.LSet
+module VarSet = Abstract_state.VarSet
module Abstract_state = Abstract_state
@@ -37,60 +42,67 @@ let check_computed () =
Options.abort "Static analysis must be called before any function of the API can be called"
-let lset
- (get_set : Abstract_state.t -> LSet.t)
- (kf : kernel_function) (s : stmt) =
+let lset ~stmt (get_set : Abstract_state.t -> LSet.t) =
check_computed ();
- match Analysis.get_state_before_stmt kf s with
+ match Analysis.get_state_before_stmt stmt with
| None -> LSet.empty
| Some state -> get_set state
-let points_to_set_stmt kf s lv = lset (Abstract_state.points_to_set lv) kf s
+let vars ~stmt (get_set : Abstract_state.t -> VarSet.t) =
+ check_computed ();
+ match Analysis.get_state_before_stmt stmt with
+ | None -> VarSet.empty
+ | Some state -> get_set state
-let new_points_to_set_stmt kf s lv =
- let get_set state =
- let new_state = Analysis.do_stmt state s in
- Abstract_state.points_to_set lv new_state
- in
- lset get_set kf s
+module Statement = struct
+ let points_to_vars ~stmt lv = vars ~stmt (Abstract_state.points_to_vars lv)
+ let points_to_lvals ~stmt lv = lset ~stmt (Abstract_state.points_to_lvals lv)
+ let alias_vars ~stmt lv = vars ~stmt (Abstract_state.alias_vars lv)
+ let aliases ~stmt lv = lset ~stmt (Abstract_state.find_all_aliases lv)
+
+ let are_aliased ~stmt (lv1: lval) (lv2:lval) : bool =
+ (* TODO: more efficient algorithm: do they share a successor? *)
+ LSet.mem lv2 @@ aliases ~stmt lv1
+end
-let aliases_stmt kf s lv =
- lset (Abstract_state.find_all_aliases lv) kf s
+let points_to_set_stmt _kf stmt = Statement.points_to_lvals ~stmt
-let new_aliases_stmt kf s lv =
+let aliases_stmt _kf stmt = Statement.aliases ~stmt
+
+let new_aliases_stmt s lv =
let get_set state =
let new_state = Analysis.do_stmt state s in
Abstract_state.find_all_aliases lv new_state
in
- lset get_set kf s
+ lset ~stmt:s get_set
-let points_to_set_kf (kf : kernel_function) (lv : lval) =
- check_computed ();
- if Kernel_function.has_definition kf
- then
- let s = Kernel_function.find_return kf in
- new_points_to_set_stmt kf s lv
- else
- Options.abort "points_to_set_kf: function %a has no definition" Kernel_function.pretty kf
+module Function = struct
+ let return_stmt kf =
+ if Kernel_function.has_definition kf
+ then Kernel_function.find_return kf
+ else Options.abort "function %a has no definition" Kernel_function.pretty kf
-let aliases_kf (kf : kernel_function) (lv : lval) =
- check_computed ();
- if Kernel_function.has_definition kf
- then
- let s = Kernel_function.find_return kf in
- new_aliases_stmt kf s lv
- else
- Options.abort "aliases_kf: function %a has no definition" Kernel_function.pretty kf
+ let points_to_vars ~kf = Statement.points_to_vars ~stmt:(return_stmt kf)
+ let points_to_lvals ~kf = Statement.points_to_lvals ~stmt:(return_stmt kf)
+ let alias_vars ~kf = Statement.alias_vars ~stmt:(return_stmt kf)
+ let aliases ~kf = Statement.aliases ~stmt:(return_stmt kf)
+ let are_aliased ~kf = Statement.are_aliased ~stmt:(return_stmt kf)
-let fundec_stmts (kf : kernel_function) (lv : lval) =
- check_computed ();
- if Kernel_function.has_definition kf
- then
- List.map
- (fun s -> s, new_aliases_stmt kf s lv)
- (Kernel_function.get_definition kf).sallstmts
- else
- Options.abort "fundec_stmts: function %a has no definition" Kernel_function.pretty kf
+ let fundec_stmts ~kf lv =
+ if Kernel_function.has_definition kf
+ then
+ List.map
+ (fun s -> s, new_aliases_stmt s lv)
+ (Kernel_function.get_definition kf).sallstmts
+ else
+ Options.abort "fundec_stmts: function %a has no definition" Kernel_function.pretty kf
+end
+
+let points_to_set_kf kf = Function.points_to_lvals ~kf
+
+let aliases_kf kf = Function.aliases ~kf
+
+let fundec_stmts kf = Function.fundec_stmts ~kf
let fold_points_to_set f_fold acc kf s lv =
@@ -99,13 +111,13 @@ let fold_points_to_set f_fold acc kf s lv =
let fold_aliases_stmt f_fold acc kf s lv =
LSet.fold (fun e a -> f_fold a e) (aliases_stmt kf s lv) acc
-let fold_new_aliases_stmt f_fold acc kf s lv =
- LSet.fold (fun e a -> f_fold a e) (new_aliases_stmt kf s lv) acc
+let fold_new_aliases_stmt f_fold acc _kf s lv =
+ LSet.fold (fun e a -> f_fold a e) (new_aliases_stmt s lv) acc
let fold_points_to_set_kf (f_fold: 'a -> lval -> 'a) (acc: 'a) (kf:kernel_function) (lv:lval) : 'a =
LSet.fold (fun e a -> f_fold a e) (points_to_set_kf kf lv) acc
-let fold_aliases_kf (f_fold : 'a -> lval -> 'a) (acc : 'a) (kf : kernel_function) (lv : lval) : 'a =
+let fold_aliases_kf (f_fold : 'a -> lval -> 'a) (acc : 'a) kf lv : 'a =
LSet.fold (fun e a -> f_fold a e) (aliases_kf kf lv) acc
let fold_fundec_stmts (f_fold: 'a -> stmt -> lval -> 'a) (acc: 'a) (kf:kernel_function) (lv:lval) : 'a =
@@ -116,26 +128,20 @@ let fold_fundec_stmts (f_fold: 'a -> stmt -> lval -> 'a) (acc: 'a) (kf:kernel_fu
acc
(fundec_stmts kf lv)
-let are_aliased (kf: kernel_function) (s:stmt) (lv1: lval) (lv2:lval) : bool =
- check_computed ();
- match Analysis.get_state_before_stmt kf s with
- None -> false
- | Some state ->
- let setv1 = Abstract_state.find_all_aliases lv1 state in
- LSet.mem lv2 setv1
+let are_aliased (_kf: kernel_function) stmt = Statement.are_aliased ~stmt
-let fold_vertex (f_fold : 'a -> G.V.t -> lval -> 'a) (acc: 'a) (kf: kernel_function) (s:stmt) (lv: lval) : 'a =
+let fold_vertex (f_fold : 'a -> G.V.t -> lval -> 'a) (acc: 'a) (_kf: kernel_function) (s:stmt) (lv: lval) : 'a =
check_computed ();
- match Analysis.get_state_before_stmt kf s with
+ match Analysis.get_state_before_stmt s with
None -> acc
| Some state ->
let v : G.V.t = Abstract_state.find_vertex lv state in
- let set_aliases = Abstract_state.find_aliases lv state in
- LSet.fold (fun lv a-> f_fold a v lv) set_aliases acc
+ let set_aliases = Abstract_state.find_synonyms lv state in
+ LSet.fold (fun lv a -> f_fold a v lv) set_aliases acc
-let fold_vertex_closure (f_fold : 'a -> G.V.t -> lval -> 'a) (acc: 'a) (kf: kernel_function) (s:stmt) (lv: lval) : 'a =
+let fold_vertex_closure (f_fold : 'a -> G.V.t -> lval -> 'a) (acc: 'a) (_kf: kernel_function) (s:stmt) (lv: lval) : 'a =
check_computed ();
- match Analysis.get_state_before_stmt kf s with
+ match Analysis.get_state_before_stmt s with
None -> acc
| Some state ->
let list_closure : (G.V.t * LSet.t) list = Abstract_state.find_transitive_closure lv state in
@@ -144,7 +150,7 @@ let fold_vertex_closure (f_fold : 'a -> G.V.t -> lval -> 'a) (acc: 'a) (kf: ker
acc
list_closure
-let get_state_before_stmt =
+let get_state_before_stmt _kf =
Analysis.get_state_before_stmt
let call_function a f res args =
diff --git a/src/plugins/alias/src/API.mli b/src/plugins/alias/src/API.mli
index 6af32089c36..d415b1699ac 100644
--- a/src/plugins/alias/src/API.mli
+++ b/src/plugins/alias/src/API.mli
@@ -25,58 +25,102 @@
open Cil_types
module LSet = Cil_datatype.LvalStructEq.Set
-module G : Graph.Sig.G
+module VarSet = Cil_datatype.Varinfo.Set
-val vid : G.V.t -> int
+module EdgeLabel : sig
+ type t = Pointer | Field of fieldinfo
-(** NB : do the analysis BEFORE using any of those functions *)
+ val compare : t -> t -> int
+ val default : t
+ val is_pointer : t -> bool
+ val is_field : t -> bool
+ val pretty : Format.formatter -> t -> unit
+end
+
+module G : Graph.Sig.G with type V.t = int and type E.t = int * EdgeLabel.t * int
+
+type v = G.V.t
+
+val vid : v -> int
+
+(** analyses at the granularity of a statement, i.e. the results are w.r.t. to
+ the state just before the given statement [stmt] *)
+module Statement : sig
+ (** see [Abstract_state.points_to_vars] *)
+ val points_to_vars : stmt:stmt -> lval -> VarSet.t
+
+ (** see [Abstract_state.points_to_lvals] *)
+ val points_to_lvals : stmt:stmt -> lval -> LSet.t
+
+ (** see [Abstract_state.alias_vars] *)
+ val alias_vars : stmt:stmt -> lval -> VarSet.t
+
+ (** see [Abstract_state.find_all_aliases] *)
+ val aliases : stmt:stmt -> lval -> LSet.t
+
+ val are_aliased: stmt:stmt -> lval -> lval -> bool
+end
+
+(** analyses at the level of a [kernel_function], i.e. the results are w.r.t.
+ to the end of the given function *)
+module Function : sig
+ (** see [Abstract_state.points_to_vars] *)
+ val points_to_vars : kf:kernel_function -> lval -> VarSet.t
+
+ (** see [Abstract_state.points_to_lvals] *)
+ val points_to_lvals : kf:kernel_function -> lval -> LSet.t
+
+ (** see [Abstract_state.alias_vars] *)
+ val alias_vars : kf:kernel_function -> lval -> VarSet.t
+
+ (** see [Abstract_state.find_all_aliases] *)
+ val aliases : kf:kernel_function -> lval -> LSet.t
+
+ val are_aliased: kf:kernel_function -> lval -> lval -> bool
+
+ (** list of pairs [s, e] where [e] is the set of lvals aliased to [v] after
+ each statement [s] in function [kf]. *)
+ val fundec_stmts : kf:kernel_function -> lval -> (stmt * LSet.t) list
+end
-(** [points_to_set_stmt kf s lv] returns the points-to set of lval [lv] before
- [stmt] in function [kf]. *)
val points_to_set_stmt : kernel_function -> stmt -> lval -> LSet.t
+[@@alert deprecated "Use Statement.points_to_vars or Statement.points_to_lvals instead!"]
-(** [points_to_set kf s lv] returns the points-to set of lval [lv] at the end
- of function [kf]. *)
val points_to_set_kf : kernel_function -> lval -> LSet.t
+[@@alert deprecated "Use Function.points_to_vars or Function.points_to_lvals instead!"]
-(** [aliases_stmt kf s lv] return the alias set of lval [lv] before [stmt] in
- function [kf]. *)
val aliases_stmt : kernel_function -> stmt -> lval -> LSet.t
+[@@alert deprecated "Use Statement.aliases instead!"]
-(** [aliases_kf kf lv] return the alias set of lval [lv] at the end of function
- [kf]. *)
val aliases_kf : kernel_function -> lval -> LSet.t
+[@@alert deprecated "Use Function.aliases instead!"]
-(** list of pairs [s, e] where [e] is the set of lval aliased to [v] after
- statement [s] in function [kf]. *)
val fundec_stmts : kernel_function -> lval -> (stmt * LSet.t) list
+[@@alert deprecated "Use Function.fundec_stmts instead!"]
-(** [fold_points_to_set f acc kf s lv] folds [f acc] over all the lvals in the
- points-to set of the given lval [lv] right before stmt [s] in function
- [kf]. *)
val fold_points_to_set:
('a -> lval -> 'a) -> 'a -> kernel_function -> stmt -> lval -> 'a
+[@@alert deprecated "Use LSet.fold/Statement.points_to_lvals or VarSet.fold/Statement.points_to_vars instead!"]
-(** [fold_aliases_stmt f acc kf s lv] folds [f acc] over all the aliases of the
- given lval [lv] right before stmt [s] in function [kf]. *)
val fold_aliases_stmt:
('a -> lval -> 'a) -> 'a -> kernel_function -> stmt -> lval -> 'a
+[@@alert deprecated "Use LSet.fold and Statement.aliases instead!"]
(** [fold_new_aliases_stmt f acc kf s lv] folds [f acc] over all the aliases of
the given lval [lv] created by stmt [s] in function [kf]. *)
val fold_new_aliases_stmt:
('a -> lval -> 'a) -> 'a -> kernel_function -> stmt -> lval -> 'a
-(** [fold_points_to_set_kf f acc kf lv] folds [f acc] over the points-to set of lval
- [lv] at the end of function [kf]. *)
val fold_points_to_set_kf :
('a -> lval -> 'a) -> 'a -> kernel_function -> lval -> 'a
+[@@alert deprecated "Use LSet.fold/Function.points_to_lvals VarSet.fold/Function.points_to_vars instead!"]
(** [fold_aliases_kf f acc kf lv] folds [f acc] over all the aliases of lval
[lv] at the end of function [kf]. *)
val fold_aliases_kf:
('a -> lval -> 'a) -> 'a -> kernel_function -> lval -> 'a
+[@@alert deprecated "Use LSet.fold/Function.aliases VarSet.fold/alias_vars instead!"]
(** [fold_fundec_stmts f acc kf v] folds [f acc s e] on the list of
pairs [s, e] where [e] is the set of lval aliased to [v] after statement [s]
@@ -84,20 +128,18 @@ val fold_aliases_kf:
val fold_fundec_stmts:
('a -> stmt -> lval -> 'a) -> 'a -> kernel_function -> lval -> 'a
-(** [are_aliased kf s lv1 lv2] returns true if and only if the two
- lvals [lv1] and [lv2] are aliased before stmt [s] in function
- [kf]. *)
val are_aliased: kernel_function -> stmt -> lval -> lval -> bool
+[@@alert deprecated "Use Statement.are_aliased instead!"]
(** [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 -> G.V.t -> lval -> 'a) -> 'a -> kernel_function -> stmt -> lval -> 'a
+ ('a -> v -> 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 -> G.V.t -> lval -> 'a) -> 'a -> kernel_function -> stmt -> lval -> 'a
+ ('a -> v -> lval -> 'a) -> 'a -> kernel_function -> stmt -> lval -> 'a
(** direct access to the abstract state. See Abstract_state.mli *)
@@ -110,8 +152,19 @@ module Abstract_state : sig
(** 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
+ (** set of variables associated with given vertex *)
+ val get_vars : v -> t -> VarSet.t
+
+ (** set of lvals which can be used to refered to the given vertex
+ Example graph: {a} → {b} -t→ {c}
+ The lvals corresponding to the rightmost vertex are {c, b.t, a->t}:
+ - c: simply refers to a variable associated with the vertex.
+ - b.t: starting from the second vertex one can follow a field-edge
+ labelled "t" to come upon the rightmost vertex.
+ - a->t: Following a pointer edge from the leftmost vertex one obtains
+ "*a". Following the "t" field-edge one arrives at the rightmost
+ vertex, corresponding to "( *a ).t" or "a->t". *)
+ val get_lval_set : v -> t -> LSet.t
(** pretty printer; debug=true prints the graph, debug = false only
prints aliased variables *)
@@ -123,26 +176,68 @@ module Abstract_state : sig
(** 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
+ val find_vertex : lval -> t -> v
+
+ (* Combining [find_vertex] and [get_vars] finds the varset associated with
+ the vertex of the given lval.
+ Does not raise an exception but returns an empty set for inexisting lval. *)
+ val find_vars : lval -> t -> VarSet.t
+
+ (** Note: You probably want to use [find_all_aliases] instead of this function.
+ Combining [find_vertex] with [get_lval_set], this function yields all the
+ different ways the vertex containing the given lval can be referred to.
+ Example: {a} → {b,c}
+ If "a" points to "b", then the vertex containing "b" can be referred to not
+ only by "b" but also by "c" or "*a".
+ Does not raise an exception but returns an empty set if the lval is not in
+ the graph. *)
+ val find_synonyms : lval -> t -> LSet.t
+
+ (** all the variables that are aliases of the given lval:
+ - variables sharing an equivalence class (or: vertex) with [lv]
+ - variables from a neighbouring vertex, i.e. a vertex that shares a
+ successor with the vertex of [lv].
+
+ Example: {a,b} → {c} ↠{d} ↠{e}
+ The aliases of "a" are {a,b,d}:
+ - "b" shares a vertex with "a"
+ - "d" is in a neighbouring vertex, pointing to "c" as does {a,b} *)
+ val alias_vars : lval -> t -> VarSet.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 *)
+ [@@alert deprecated "Use find_synonyms, alias_vars, or find_all_aliases instead!"]
+
+ (** Yields all lvals that are alias of a given lval [lv]. This includes:
+ - variables sharing an equivalence class (or: vertex) with [lv]
+ - variables from a neighbouring vertex, i.e. a vertex that shares a
+ successor with the vertex of [lv].
+ - lvals reconstructed from the variables from the two previous sets.
+
+ Example: {a,b} → {c} ↠{d} ↠{e}
+ The aliases of "a" are {a,b,d,*e}:
+ - "b" shares a vertex with "a"
+ - "d" is in a neighbouring vertex, pointing to "c" as does {a,b}
+ - *e is obtained by following backwards the pointer edge from {d} to {e}. *)
val find_all_aliases : lval -> t -> LSet.t
(** the set of all lvars to which the given variable may point. *)
+ val points_to_vars : lval -> t -> VarSet.t
+
+ (** the set of all lvals to which the given variable may point including
+ reconstructed lvals such as *p, a.t, c->s.
+ For some pointer p it will always include *p. *)
+ val points_to_lvals : lval -> t -> LSet.t
+
val points_to_set : lval -> t -> LSet.t
+ [@@alert deprecated "Use points_to_vars or points_to_lvals instead!"]
(** 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
+ find_aliases lv x).
+ Only follows pointer edges, not field edges.
+ *)
+ val find_transitive_closure : lval -> t -> (v * 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
diff --git a/src/plugins/alias/src/abstract_state.ml b/src/plugins/alias/src/abstract_state.ml
index 997c08eb829..2dbd0b81ec4 100644
--- a/src/plugins/alias/src/abstract_state.ml
+++ b/src/plugins/alias/src/abstract_state.ml
@@ -71,6 +71,8 @@ module G = struct
| _ -> Options.fatal "Invariant violated: more than one successor"
end
+type v = G.V.t
+
module V = G.V
module E = struct
include G.E
@@ -107,7 +109,7 @@ let fresh_node_id () =
node_counter := !node_counter + 1;
id
-let find_varset v s : VarSet.t =
+let get_vars v s : VarSet.t =
try VMap.find v s.vmap with Not_found -> VarSet.empty
(* raises Not_found *)
@@ -139,10 +141,6 @@ let rec find_lval_vertex ((lhost, offset) : lval) s : V.t =
module Readout = struct
- let get_lval_set v s =
- let mk_lval var = Var var, NoOffset in
- LSet.of_seq @@ Seq.map mk_lval @@ VarSet.to_seq @@ find_varset v s
-
(* Reconstruct all lvals that are represented by the given node.
Nodes only carry varinfos. In order to obtain lvals we recursively walk
backwards in the graph inductively constructing lvals from scratch.
@@ -151,7 +149,7 @@ module Readout = struct
modified according to the edge type used:
* Pointer: add a star (x → *x)
* Field f: add an offset (x -> x.f) *)
- let reconstruct_lvals s v : LSet.t =
+ let get_lval_set v s : LSet.t =
assert (G.mem_vertex s.graph v);
(* cycles can occur with unsafe casts such as: x->f = (int* ) x; *)
let rec checking_for_cycles s visited v =
@@ -185,28 +183,51 @@ module Readout = struct
)
(G.pred_e s.graph v)
in
- let lvals_of_v = get_lval_set v s in
+ let lvals_of_v =
+ let mk_lval var = (Var var), NoOffset in
+ LSet.of_seq @@ Seq.map mk_lval @@ VarSet.to_seq @@ get_vars v s
+ in
List.fold_left LSet.union lvals_of_v modified_predecessors
in
checking_for_cycles s VSet.empty v
let lvals_pointing_to_vertex v s : LSet.t =
assert (G.mem_vertex s.graph v);
- let list_pred = List.map (reconstruct_lvals s) @@ G.ppred s.graph v in
+ let list_pred = List.map (fun b -> get_lval_set b s) (G.ppred s.graph v) in
List.fold_left LSet.union LSet.empty list_pred
- let find_aliases lv s =
+ let find_vars lv s =
+ let lv = Lval.simplify lv in
+ try let v = find_lval_vertex lv s in get_vars v s
+ with Not_found -> VarSet.empty
+
+ let find_synonyms lv s =
let lv = Lval.simplify lv in
try let v = find_lval_vertex lv s in get_lval_set v s
with Not_found -> LSet.empty
+ let alias_vars lv s : VarSet.t =
+ try
+ let v = find_lval_vertex lv s in
+ let succs = G.psucc s.graph v in
+ let pred_succs = List.concat_map (G.ppred s.graph) succs in
+ let pred_vars = List.map (fun p -> get_vars p s) pred_succs in
+ List.fold_left VarSet.union VarSet.empty pred_vars
+ with Not_found -> VarSet.empty
+
let find_all_aliases lv s : LSet.t =
let v_opt = try Some (find_lval_vertex lv s) with Not_found -> None in
match Option.bind v_opt @@ G.psucc_opt s.graph with
| None -> LSet.empty
| Some succ -> lvals_pointing_to_vertex succ s
- let points_to_set lv s : LSet.t =
+ let points_to_vars lv s : VarSet.t =
+ let succ = try G.psucc_opt s.graph @@ find_lval_vertex lv s with Not_found -> None in
+ match succ with
+ | None -> VarSet.empty
+ | Some succ_v -> get_vars succ_v s
+
+ let points_to_lvals lv s : LSet.t =
let succ = try G.psucc_opt s.graph @@ find_lval_vertex lv s with Not_found -> None in
match succ with
| None -> LSet.empty
@@ -433,9 +454,9 @@ let merge s v1 v2 =
then s
else
(* update varmap : every lval in v2 must now be associated with v1 *)
- let new_varmap = VarSet.fold (fun lv2 -> VarMap.add lv2 v1) (find_varset v2 s) s.varmap in
+ let new_varmap = VarSet.fold (fun lv2 -> VarMap.add lv2 v1) (get_vars v2 s) s.varmap in
let new_vmap =
- let new_set = VarSet.union (find_varset v1 s) (find_varset v2 s) in
+ let new_set = VarSet.union (get_vars v1 s) (get_vars v2 s) in
VMap.add v1 new_set @@ VMap.remove v2 s.vmap
in
let new_graph = (* update the graph *)
@@ -742,9 +763,9 @@ module Summary = struct
let pp_elem lv =
if !is_first then is_first := false else Format.fprintf fmt "@ ";
Format.fprintf fmt "@[%a" Cil_datatype.Lval.pretty lv;
- let pointees = Readout.points_to_set lv s in
- if not @@ LSet.is_empty pointees then
- Format.fprintf fmt "→%a" LSet.pretty pointees;
+ let pointees = Readout.points_to_vars lv s in
+ if not @@ VarSet.is_empty pointees then
+ Format.fprintf fmt "→%a" VarSet.pretty pointees;
Format.fprintf fmt "@]";
in
List.iter pp_elem l
@@ -856,7 +877,7 @@ let call s (res : lval option) (args : exp list) (summary : Summary.t) : state =
(List.fold_left join_succs s @@ List.map fst vertex_pairs)
module Dot = struct
- let find_varset_ref = Extlib.mk_fun "find_varset"
+ let find_vars_ref = Extlib.mk_fun "find_vars"
include Graph.Graphviz.Dot (struct
include G
@@ -864,7 +885,7 @@ module Dot = struct
let default_edge_attributes _ = []
let get_subgraph _ = None
let vertex_attributes v =
- let lset = !find_varset_ref v in
+ let lset = !find_vars_ref v in
let label =
VarSet.pretty Format.str_formatter lset;
Format.flush_str_formatter ()
@@ -900,15 +921,20 @@ module API = struct
(* TODO : what about offsets ? *)
let get_lval_set = Readout.get_lval_set
- let find_aliases = Readout.find_aliases
+ let find_vars = Readout.find_vars
+ let find_synonyms = Readout.find_synonyms
+ let find_aliases = Readout.find_synonyms
+ let alias_vars = Readout.alias_vars
let find_all_aliases = Readout.find_all_aliases
- let points_to_set = Readout.points_to_set
+ let points_to_vars = Readout.points_to_vars
+ let points_to_set = Readout.points_to_lvals
+ let points_to_lvals = Readout.points_to_lvals
let get_graph s = s.graph
let print_dot filename s =
let file = open_out filename in
- Dot.find_varset_ref := (fun v -> find_varset v s);
+ Dot.find_vars_ref := (fun v -> get_vars v s);
Dot.output_graph file s.graph;
close_out file
end
diff --git a/src/plugins/alias/src/abstract_state.mli b/src/plugins/alias/src/abstract_state.mli
index b979a413b3c..69f194b08d1 100644
--- a/src/plugins/alias/src/abstract_state.mli
+++ b/src/plugins/alias/src/abstract_state.mli
@@ -20,70 +20,60 @@
(* *)
(**************************************************************************)
-(** Module abstract_state *)
+(** Module Abstract_state *)
+
+(** see API.Abstract_state for documentation *)
open Cil_types
-(** Points-to graphs datastructure. *)
-module G: Graph.Sig.G with type V.t = int
+module EdgeLabel : sig
+ type t = Pointer | Field of fieldinfo
+
+ val compare : t -> t -> int
+ val default : t
+ val is_pointer : t -> bool
+ val is_field : t -> bool
+ val pretty : Format.formatter -> t -> unit
+end
+
+module G: Graph.Sig.G with type V.t = int and type E.t = int * EdgeLabel.t * int
module LSet = Cil_datatype.LvalStructEq.Set
+module VarSet = Cil_datatype.Varinfo.Set
-(** Type denothing an abstract state of the analysis. It is a graph containing
- all aliases and points-to information. *)
type t
+type v = G.V.t
-val vid : G.V.t -> int
-
-(** access to the points-to graph *)
+val vid : v -> int
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 get_vars : v -> t -> VarSet.t
+val get_lval_set : v -> t -> LSet.t
val pretty : ?debug:bool -> Format.formatter -> t -> unit
-
-(** dot printer; first argument is a file name *)
val print_dot : string -> t -> unit
+val find_vertex : lval -> t -> v
+val find_vars : lval -> t -> VarSet.t
+val find_synonyms : lval -> t -> LSet.t
-(** 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
+[@@alert deprecated "Use find_synonyms or find_all_aliases instead!"]
-(** 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 alias_vars : lval -> t -> VarSet.t
val find_all_aliases : lval -> t -> LSet.t
+val points_to_vars : lval -> t -> VarSet.t
+val points_to_lvals : lval -> t -> LSet.t
-(** the set of all lvars to which the given variable may point. *)
val points_to_set : lval -> t -> LSet.t
+[@@alert deprecated "Use points_to_vars or points_to_lvals instead!"]
-(** 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 find_transitive_closure : lval -> t -> (v * LSet.t) list
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) *)
+ before and after each function call or transformation of the graph) *)
val assert_invariants : t -> unit
(** Functions for Steensgaard's algorithm, see the paper *)
-val join : t -> G.V.t -> G.V.t -> t
+val join : t -> v -> v -> t
(** transfert functions for different kinds of assignments *)
val assignment : t -> lval -> exp -> t
diff --git a/src/plugins/alias/src/analysis.ml b/src/plugins/alias/src/analysis.ml
index a508829c38b..d573a733406 100644
--- a/src/plugins/alias/src/analysis.ml
+++ b/src/plugins/alias/src/analysis.ml
@@ -296,7 +296,7 @@ let clear () =
computed_flag := false;
Stmt_table.clear ()
-let get_state_before_stmt _kf stmt =
+let get_state_before_stmt stmt =
if is_computed ()
then try Stmt_table.find stmt with Not_found -> None
else None
diff --git a/src/plugins/alias/src/analysis.mli b/src/plugins/alias/src/analysis.mli
index f1bb2652e88..2b8353181ca 100644
--- a/src/plugins/alias/src/analysis.mli
+++ b/src/plugins/alias/src/analysis.mli
@@ -62,7 +62,7 @@ val is_computed : unit -> bool
val clear : unit -> unit
(** see API.mli *)
-val get_state_before_stmt : kernel_function -> stmt -> Abstract_state.t option
+val get_state_before_stmt : stmt -> Abstract_state.t option
(** see API.mli *)
val get_summary : kernel_function -> Abstract_state.summary option
--
GitLab