From 62e7a4947f182b34545d7f1b3004d9858e955478 Mon Sep 17 00:00:00 2001
From: Tristan Le Gall <tristan.le-gall@cea.fr>
Date: Fri, 23 Dec 2022 20:16:11 +0100
Subject: [PATCH] [alias] comments and linter
---
src/plugins/alias/abstract_state.ml | 2 +-
src/plugins/alias/abstract_state.mli | 16 ++++++++++++----
src/plugins/alias/analysis.ml | 10 +++++-----
.../alias/tests/basic/oracle/test.res.oracle | 2 +-
.../tests/real_world/oracle/example1.res.oracle | 2 +-
5 files changed, 20 insertions(+), 12 deletions(-)
diff --git a/src/plugins/alias/abstract_state.ml b/src/plugins/alias/abstract_state.ml
index 2c82946b314..9af3dced6b0 100644
--- a/src/plugins/alias/abstract_state.ml
+++ b/src/plugins/alias/abstract_state.ml
@@ -112,7 +112,7 @@ let pretty ?(debug=false) =
(** invariants of type t must be true before and after each functon call *)
let assert_invariants (x:t) : unit =
- Format.printf "Checking invariants@.%a@." (pretty ~debug:true) x;
+ (* Format.printf "Checking invariants@.%a@." (pretty ~debug:true) x; *)
(* check that all vertex of the graph have entries in pending and vmap, and are integer between 0 and cmpt *)
let assert_vertex (v:V.t) =
assert (v >= 0);
diff --git a/src/plugins/alias/abstract_state.mli b/src/plugins/alias/abstract_state.mli
index 35f2a6f0633..2ad7d6c10f4 100644
--- a/src/plugins/alias/abstract_state.mli
+++ b/src/plugins/alias/abstract_state.mli
@@ -36,10 +36,11 @@ module LMap = Lval.Map
type t
(** check all the invariants that must be true on an abstract value
- before and after each function call *)
+ before and after each function call or transformation of the graph) *)
val assert_invariants : t -> unit
-(** pretty printer *)
+(** pretty printer; debug=true prints the graph, debug = false only
+ prints aliased variables *)
val pretty : ?debug:bool -> Format.formatter -> t -> unit
(** dot printer *)
@@ -48,13 +49,19 @@ val print_dot : string -> t -> unit
(** finds the vertex corresponding to a lval *)
val find_vertex : lval -> t -> G.V.t
-(** Functions for the analysis *)
+(** finds the vertex corresponding to a lval; if not present creates
+ the corresponding node in the graph; the (maybe modifed) graph is
+ returned as well *)
+val find_or_create_vertex : lval -> t -> G.V.t * G.t
+
+(** Functions for Steensgaard's algorithm *)
val join : t -> G.V.t -> G.V.t -> t
val cjoin : t -> G.V.t -> G.V.t -> t
val set_type : t -> G.V.t -> G.V.t -> t
+(** transfert functions for different kinds of assignments *)
val assignment_x_y : t -> lval -> lval -> t
val assignment_x_addr_y : t -> lval -> lval -> t
@@ -67,6 +74,7 @@ val assignment_ptr_x_y : t -> lval -> lval -> t
val assignment_ptr_x_cst : t -> lval -> t
+(** equality test *)
val equal : t -> t -> bool
(** union of two abstract values ; ensures that if 2 lval are aliased
@@ -74,7 +82,7 @@ val equal : t -> t -> bool
then they will also be aliased/points-to in the result *)
val union : t -> t -> t
-(* empty graph *)
+(** empty graph *)
val initial_value : t
(** Type denoting summaries of functions *)
diff --git a/src/plugins/alias/analysis.ml b/src/plugins/alias/analysis.ml
index 8126810ccd6..28a681c7dac 100644
--- a/src/plugins/alias/analysis.ml
+++ b/src/plugins/alias/analysis.ml
@@ -79,10 +79,10 @@ struct
| None -> Format.fprintf fmt "None"
| Some s -> Format.fprintf fmt "%a" (Abstract_state.pretty ~debug:false) s
- let pretty_debug fmt state =
- match state with
- | None -> Format.fprintf fmt "None"
- | Some s -> Format.fprintf fmt "%a" (Abstract_state.pretty ~debug:true) s
+ (* let pretty_debug fmt state =
+ * match state with
+ * | None -> Format.fprintf fmt "None"
+ * | Some s -> Format.fprintf fmt "%a" (Abstract_state.pretty ~debug:true) s *)
let computeFirstPredecessor _ a = a
@@ -97,7 +97,7 @@ struct
Some (Some (Abstract_state.union old new_))
let do_assignment (a:t) (lv:lval) (exp:exp) : t =
- Format.printf "State before do_assignment %a = %a : @[%a@]@." Lval.pretty lv Exp.pretty exp pretty_debug a;
+ (* Format.printf "State before do_assignment %a = %a : @[%a@]@." Lval.pretty lv Exp.pretty exp pretty_debug a; *)
match (a,lv,exp.enode) with
(Some a, (Var v1, NoOffset), Lval (Var v2,NoOffset)) ->
(* case x = y *)
diff --git a/src/plugins/alias/tests/basic/oracle/test.res.oracle b/src/plugins/alias/tests/basic/oracle/test.res.oracle
index eff48a5c96a..a1861b053e4 100644
--- a/src/plugins/alias/tests/basic/oracle/test.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/test.res.oracle
@@ -2,4 +2,4 @@
[alias] Parsing done
[alias] Functions done
[alias] Analysis complete
-[]
\ No newline at end of file
+[]
diff --git a/src/plugins/alias/tests/real_world/oracle/example1.res.oracle b/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
index 11a6a2ae06d..ef70b78f374 100644
--- a/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
+++ b/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
@@ -1597,4 +1597,4 @@ VMap:
<end of list>
)
[alias] Analysis complete
-]
\ No newline at end of file
+]
--
GitLab