diff --git a/src/plugins/alias/API.ml b/src/plugins/alias/API.ml
index 1fd3b92ed557f1afacd6b3b6c4c56b026baebd8c..433e902039ae57a204762c9ba97721a0dde92608 100644
--- a/src/plugins/alias/API.ml
+++ b/src/plugins/alias/API.ml
@@ -27,23 +27,22 @@ open Cil_datatype
module LSet = Lval.Set
-let fold_new_aliases_stmt
- (f_fold : 'a -> lval -> 'a) (acc: 'a) (kf: kernel_function) (s:stmt) (lv: lval) : 'a =
+let fold_aliases_stmt (f_fold : 'a -> lval -> 'a) (acc: 'a) (kf: kernel_function) (s:stmt) (lv: lval) : 'a =
match Analysis.get_abstract_state kf s with
None -> acc
| Some state ->
let set_aliases = Abstract_state.find_aliases lv state in
LSet.fold (fun e a -> f_fold a e) set_aliases acc
-let fold_aliases_stmt
- (f_fold: 'a -> lval -> 'a) (acc: 'a) (kf:kernel_function) (s:stmt) (lv:lval) : 'a =
- (* TODO is it correct ? obviously not *)
- match s.preds with
- [] -> acc
- | s::_ -> fold_new_aliases_stmt f_fold acc kf s lv
+let fold_new_aliases_stmt (f_fold: 'a -> lval -> 'a) (acc: 'a) (kf:kernel_function) (s:stmt) (lv:lval) : 'a =
+ match Analysis.get_abstract_state kf s with
+ None -> acc
+ | Some state ->
+ let new_state = Analysis.do_stmt state s in
+ let set_aliases = Abstract_state.find_aliases lv new_state in
+ LSet.fold (fun e a -> f_fold a e) set_aliases 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:kernel_function) (lv:lval) : 'a =
let s = Kernel_function.find_return kf in
fold_new_aliases_stmt f_fold acc kf s lv
@@ -64,17 +63,30 @@ let fold_fundec_stmts (f_fold: 'a -> stmt -> lval -> 'a) (acc: 'a) (kf:kernel_fu
acc
list_stmt
else
- failwith "not implemented"
+ Options.abort "fold_dundec_stmts: function %a has no definition" Kernel_function.pretty kf
-let are_aliased (kf: kernel_function) (s:stmt) (lv1: lval) (lv2:lval) : bool =
+let are_aliased (kf: kernel_function) (s:stmt) (lv1: lval) (lv2:lval) : bool =
match Analysis.get_abstract_state kf s with
None -> false
| Some state ->
let setv1 = Abstract_state.find_aliases lv1 state in
LSet.mem lv2 setv1
-let fold_points_to _ =
- failwith "not implemented"
-let fold_points_to_closure _ =
- failwith "not implemented"
+
+let fold_points_to (f_fold : 'a -> Lval.Set.t -> 'a) (acc: 'a) (kf: kernel_function) (s:stmt) (lv: lval) : 'a =
+ match Analysis.get_abstract_state kf s with
+ None -> acc
+ | Some state ->
+ let set_aliases = Abstract_state.find_aliases lv state in
+ f_fold acc set_aliases
+
+let fold_points_to_closure (f_fold : 'a -> Lval.Set.t -> 'a) (acc: 'a) (kf: kernel_function) (s:stmt) (lv: lval) : 'a =
+ match Analysis.get_abstract_state kf s with
+ None -> acc
+ | Some state ->
+ let list_closure = Abstract_state.find_transitive_closure lv state in
+ List.fold_left
+ f_fold
+ acc
+ list_closure
diff --git a/src/plugins/alias/API.mli b/src/plugins/alias/API.mli
index 8b7ec27d5a46841c10d3c34e4574dd019a67d72d..8583eefc77f30b8e560b45c2ec6a4c85f30b936f 100644
--- a/src/plugins/alias/API.mli
+++ b/src/plugins/alias/API.mli
@@ -44,18 +44,18 @@ val fold_aliases_kf:
('a -> lval -> 'a) -> 'a -> kernel_function -> lval -> 'a
(** [fold_fundec_stmts f acc kf v] folds function [f acc s e] on the list of
- pairs [s, e] where e is the set of lval aliased to [v] after statement [s] in
+ pairs [s, e] where e is the set of lval aliased to [v] before statement [s] in
function [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 right after stmt [s] in function
+ lvals [lv1] and [lv2] are aliased before stmt [s] in function
[kf]. *)
val are_aliased: kernel_function -> stmt -> lval -> lval -> bool
(** [fold_points_to f acc kf s v] folds [f acc setv] where
- [setv] is the set of lvals that are pointed to by [v] right after
+ [setv] is the set of lvals that are pointed to by [v] before
statement [s] in function [kf]. *)
val fold_points_to:
('a -> Lval.Set.t -> 'a) -> 'a -> kernel_function -> stmt -> lval -> 'a
diff --git a/src/plugins/alias/abstract_state.ml b/src/plugins/alias/abstract_state.ml
index a5fbf54b9fe7bc4cc6b3c9438865f12750a6d383..b8ddd1f91ea5489ff3f4ff0d2d0b45a79700a6d8 100644
--- a/src/plugins/alias/abstract_state.ml
+++ b/src/plugins/alias/abstract_state.ml
@@ -155,6 +155,22 @@ let assert_invariants x =
Assert_failure f -> (Format.printf "DEBUG FAILED INVARIANTS@.%a@." (pretty ~debug:true) x; raise (Assert_failure f))
+(* find functions, part 2 *)
+let rec closure_find_lset (v:V.t) (x:t) =
+ match G.succ x.graph v with
+ [] -> [find_lset v x]
+ | [v_next] -> (find_lset v x)::(closure_find_lset v_next x)
+ | _ -> failwith ("this shall not happen (invariant broken)")
+
+let find_transitive_closure (lv:lval) (x:t) =
+ assert_invariants x;
+ try
+ let v = (LMap.find lv x.lmap) in
+ closure_find_lset v x
+ with
+ Not_found -> []
+
+
(* find the vertex of an lval *)
let find_vertex (lv:lval) (x:t) =
LMap.find lv x.lmap
@@ -723,7 +739,7 @@ let union (a1:t) (a2:t) :t =
let new_a =
(* if new_a.cmpt > 2 * (G.nb_vertex new_a.graph)
* then *)
- rename_all_vertex new_a
+ rename_all_vertex new_a
(* else
* new_a *)
in
@@ -766,7 +782,7 @@ let make_summary (s: t option) (kf: kernel_function) =
if Kernel_function.has_definition kf then
let return_stmt = Kernel_function.find_return kf in
match return_stmt.skind with
- Return (e, _) -> e
+ Return (e, _) -> e
| _ -> failwith "this should not happen"
else
None
diff --git a/src/plugins/alias/abstract_state.mli b/src/plugins/alias/abstract_state.mli
index ce97fc9a4edc3bec92ddc3472fe728dd9545dea2..9bd407819d957e313f84cc925fd1c32a33661d0e 100644
--- a/src/plugins/alias/abstract_state.mli
+++ b/src/plugins/alias/abstract_state.mli
@@ -52,6 +52,12 @@ val find_vertex : lval -> t -> G.V.t
val find_aliases : lval -> t -> LSet.t
+(** find_aliases, then recursively finds other sets of lvals. We have
+ the property (if lv is in x) :
+ List.hd (find_transitive_closure lv x) = find_aliases lv x
+*)
+val find_transitive_closure : lval -> t -> LSet.t list
+
(** Functions for Steensgaard's algorithm *)
val join : t -> G.V.t -> G.V.t -> t
diff --git a/src/plugins/alias/analysis.ml b/src/plugins/alias/analysis.ml
index bee409e132ad35bd463560dd701d7c704b731b5d..b3c4f07ffca70bb494afe89430f906dfc837bc08 100644
--- a/src/plugins/alias/analysis.ml
+++ b/src/plugins/alias/analysis.ml
@@ -187,10 +187,10 @@ struct
let rec process_Stmt (s:stmt) (a:t) : t =
(* register a before stmt *)
Stmt_table.add s a;
- match s.skind with
- Instr i -> doInstr s i a
- | Block b -> process_Block b a
- | _ -> a
+ match s.skind with
+ Instr i -> doInstr s i a
+ | Block b -> process_Block b a
+ | _ -> a
and process_Block b a =
List.fold_left
@@ -214,14 +214,14 @@ let do_stmt (a: Abstract_state.t) (s:stmt) : Abstract_state.t =
match do_instr s i (Some a) with
None -> failwith "problem here"
| Some a -> a
- end
+ end
| _ -> a
let doFunction (kf:kernel_function) =
Options.feedback ~level:2 "entering in function %a."
Kernel_function.pretty kf;
if Kernel_function.has_definition kf then
- begin
+ begin
let first_stmts =
try [Kernel_function.find_first_stmt kf]
with Kernel_function.No_Statement -> []
@@ -241,7 +241,7 @@ let doFunction (kf:kernel_function) =
in
Function_table.add kf (Some summary)
end
- else
+ else
begin
(* summary by default *)
Options.warning "Function %a has no definition (summary empty)"
@@ -251,7 +251,7 @@ let doFunction (kf:kernel_function) =
in
Function_table.add kf (Some summary)
end
-
+
let () = function_compute_ref := doFunction
let make_summary (state:Abstract_state.t) (kf:kernel_function) =
diff --git a/src/plugins/alias/utils.mli b/src/plugins/alias/utils.mli
index f483b4ceb199627dbf15ae9b37d8f9f4ee412e3c..c091ad78cfc93f26c71b1e84ef049171471a3bc5 100644
--- a/src/plugins/alias/utils.mli
+++ b/src/plugins/alias/utils.mli
@@ -22,9 +22,9 @@
open Cil_types
-
+
(* type of the return of the following function *)
type basic_lval = BNone | BLval of lval | BAddrOf of lval
-
+
(* finds, in an expression, the "basic" lval (eg a variable, a pointer or an array name). *)
-val find_basic_lval : exp -> basic_lval
+val find_basic_lval : exp -> basic_lval