From 3dab330ae13a294fc2d0eebdad6c8ec9c5e3f537 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 5 Aug 2024 19:36:52 +0200
Subject: [PATCH] [kernel] Dominators: removes module StmtSetOpt and simply
uses the empty set.
---
src/kernel_services/analysis/dominators.ml | 86 ++++++--------------
src/kernel_services/analysis/dominators.mli | 16 ++--
tests/misc/oracle/test_dominators.res.oracle | 28 +++----
tests/misc/test_dominators.ml | 8 +-
4 files changed, 49 insertions(+), 89 deletions(-)
diff --git a/src/kernel_services/analysis/dominators.ml b/src/kernel_services/analysis/dominators.ml
index edee9f7b39..92b0b3f9c7 100644
--- a/src/kernel_services/analysis/dominators.ml
+++ b/src/kernel_services/analysis/dominators.ml
@@ -45,34 +45,9 @@ module StmtSet = struct
List.find_opt f' (elements set)
end
-(* Used to store the result of the analysis. [None] means the statement is
- unreachable while [Some set] means the statement was reached with this set
- of statements. *)
-module StmtSetOpt = struct
- include Datatype.Option (StmtSet)
-
- let remove s setopt =
- Option.map (StmtSet.remove s) setopt
-
- let mem s setopt =
- Option.fold ~none:false ~some:(StmtSet.mem s) setopt
-
- let inter s s' =
- match s, s' with
- | None, None -> None
- | Some s, None | None, Some s -> Some s
- | Some s, Some s' -> Some (StmtSet.inter s s')
-
- let find_opt_for_all f setopt =
- Option.bind setopt (StmtSet.find_opt_for_all f)
-
- let pretty fmt setopt =
- Pretty_utils.pp_opt ~none:"Top" StmtSet.pretty fmt setopt
-end
-
module DotGraph = Graph.Graphviz.Dot (
struct
- type t = string * (StmtSetOpt.t StmtTbl.t)
+ type t = string * (StmtSet.t StmtTbl.t)
module V = struct
type t = stmt
let pretty fmt v = Cil_printer.pp_stmt fmt v
@@ -87,11 +62,7 @@ module DotGraph = Graph.Graphviz.Dot (
StmtTbl.iter (fun stmt _ -> f stmt) graph
let iter_edges_e f (_, graph) =
- let do_edges stmt set_opt =
- let do_edge p = f (p, stmt) in
- Option.iter (fun set -> StmtSet.iter do_edge set) set_opt
- in
- StmtTbl.iter do_edges graph
+ StmtTbl.iter (fun stmt -> StmtSet.iter (fun p -> f (p, stmt))) graph
let graph_attributes (title, _) = [`Label title]
@@ -145,7 +116,7 @@ module Compute (Analysis : Analysis) = struct
module Table =
Cil_state_builder.Stmt_hashtbl
- (StmtSetOpt)
+ (StmtSet)
(struct
let name = Analysis.name ^ "_table"
let dependencies = [Ast.self]
@@ -166,11 +137,11 @@ module Compute (Analysis : Analysis) = struct
(* Compute the analysis, initial state is empty. *)
let result = Analysis.fixpoint kf StmtSet.empty in
(* Fill table with all statements. *)
- List.iter (fun stmt -> Table.add stmt None) f.sallstmts;
+ List.iter (fun stmt -> Table.add stmt StmtSet.empty) f.sallstmts;
(* Update the table with analysis results. *)
Analysis.Result.iter_stmt (fun s set ->
(* A statement always (post)dominates itself, so we add it here. *)
- Table.replace s (Some (StmtSet.add s set))
+ Table.replace s (StmtSet.add s set)
) result;
Kernel.feedback ~level:2 "done for function %a"
Kernel_function.pretty kf
@@ -190,53 +161,46 @@ module Compute (Analysis : Analysis) = struct
| Some v -> v
(* Generic function to get the set of strict (post)dominators of [stmt]. *)
- let get_strict stmt = get stmt |> StmtSetOpt.remove stmt
+ let get_strict stmt = get stmt |> StmtSet.remove stmt
(* Generic function to test the (post)domination of 2 statements. *)
- let mem a b = get b |> StmtSetOpt.mem a
+ let mem a b = get b |> StmtSet.mem a
(* Generic function to test the strict (post)domination of 2 statements. *)
- let mem_strict a b = get_strict b |> StmtSetOpt.mem a
+ let mem_strict a b = get_strict b |> StmtSet.mem a
(* The nearest common ancestor (resp. children) is the ancestor which is
dominated (resp. postdominated) by all common ancestors, ie. the lowest
(resp. highest) ancestor in the domination tree. *)
let nearest stmtl =
- let exception Unreachable in
(* Get the set of strict (post)doms for each statement and intersect them to
- keep the common ones. If one of them is None (unreachable), they do not
+ keep the common ones. If one of them is unreachable, they do not
share a common ancestor/children. *)
let common_set =
- try
- List.fold_left (fun acc s ->
- match get_strict s with
- | None -> raise Unreachable
- | set -> StmtSetOpt.inter acc set
- ) None stmtl
- with Unreachable -> None
+ match stmtl with
+ | [] -> StmtSet.empty
+ | stmt :: tail ->
+ List.fold_left
+ (fun acc s -> StmtSet.inter acc (get_strict s))
+ (get_strict stmt) tail
in
(* Try to find a statement [s] in [common_set] which is (post)dominated by
all statements of the [common_set]. *)
- StmtSetOpt.find_opt_for_all (Fun.flip mem) common_set
+ StmtSet.find_opt_for_all (Fun.flip mem) common_set
let pretty fmt () =
let l = Table.to_seq () |> List.of_seq in
Pretty_utils.pp_list ~pre:"@[<v>" ~sep:"@;" ~empty:"Empty"
(fun fmt (k,v) ->
- Format.fprintf fmt "Stmt:%d -> @[%a@]" k.sid StmtSetOpt.pretty v
+ Format.fprintf fmt "Stmt:%d -> @[%a@]" k.sid StmtSet.pretty v
) fmt l
let get_set graph stmt =
match StmtTbl.find_opt graph stmt with
- | Some None -> assert false
- | Some (Some l) -> l
+ | Some l -> l
| None ->
- match get_strict stmt with
- | Some set ->
- StmtTbl.add graph stmt (Some set); set
- | None ->
- StmtTbl.add graph stmt None;
- raise Not_found
+ let set = get_strict stmt in
+ StmtTbl.add graph stmt set; set
(* [s_set] are [s] (post)dominators, including [s]. We don't have to represent
the relation between [s] and [s], so [get_set] removes it. And because the
@@ -246,12 +210,10 @@ module Compute (Analysis : Analysis) = struct
let reduce graph s =
(* Union of all (post)dominators of [s] (post)dominators [s_set]. *)
let unions p acc = get_set graph p |> StmtSet.union acc in
- try
- let s_set = get_set graph s in
- let p_sets = StmtSet.fold unions s_set StmtSet.empty in
- let res = StmtSet.diff s_set p_sets in
- StmtTbl.replace graph s (Some res)
- with Not_found -> ()
+ let s_set = get_set graph s in
+ let p_sets = StmtSet.fold unions s_set StmtSet.empty in
+ let res = StmtSet.diff s_set p_sets in
+ StmtTbl.replace graph s res
let build_dot filename kf =
match kf.fundec with
diff --git a/src/kernel_services/analysis/dominators.mli b/src/kernel_services/analysis/dominators.mli
index ec9a842881..b61cb35b9f 100644
--- a/src/kernel_services/analysis/dominators.mli
+++ b/src/kernel_services/analysis/dominators.mli
@@ -56,24 +56,24 @@ val compute_postdominators : kernel_function -> unit
@since Frama-C+dev
*)
-val get_dominators : stmt -> Cil_datatype.Stmt.Hptset.t option
-(** Return the [set] of dominators of the given statement. [None] means the
- statement is unreachable.
+val get_dominators : stmt -> Cil_datatype.Stmt.Hptset.t
+(** Return the [set] of dominators of the given statement.
+ The empty set means the statement is unreachable.
@since Frama-C+dev
*)
-val get_postdominators : stmt -> Cil_datatype.Stmt.Hptset.t option
-(** Return the [set] of postdominators of the given statement. [None] means the
- statement is unreachable.
+val get_postdominators : stmt -> Cil_datatype.Stmt.Hptset.t
+(** Return the [set] of postdominators of the given statement.
+ The empty set means the statement is unreachable.
@since Frama-C+dev
*)
-val get_strict_dominators : stmt -> Cil_datatype.Stmt.Hptset.t option
+val get_strict_dominators : stmt -> Cil_datatype.Stmt.Hptset.t
(** Same as [get_dominators] but exclude the statement itself.
@since Frama-C+dev
*)
-val get_strict_postdominators : stmt -> Cil_datatype.Stmt.Hptset.t option
+val get_strict_postdominators : stmt -> Cil_datatype.Stmt.Hptset.t
(** Same as [get_postdominators] but exclude the statement itself.
@since Frama-C+dev
*)
diff --git a/tests/misc/oracle/test_dominators.res.oracle b/tests/misc/oracle/test_dominators.res.oracle
index 0d6e7207b5..cb34f6fee4 100644
--- a/tests/misc/oracle/test_dominators.res.oracle
+++ b/tests/misc/oracle/test_dominators.res.oracle
@@ -296,7 +296,7 @@ Dominators analysis:
Stmt:10 -> {10}
Stmt:12 -> {10,12}
Stmt:13 -> {10,12,13}
- Stmt:14 -> Top
+ Stmt:14 -> {}
Stmt:15 -> {10,12,13,15}
Stmt:16 -> {10,12,16}
Stmt:18 -> {10,12,16,18,57}
@@ -311,7 +311,7 @@ Dominators analysis:
Stmt:31 -> {22,23,24,26,28,30,31}
Stmt:33 -> {22,23,24,26,28,30,33}
Stmt:34 -> {22,23,24,26,27,34}
- Stmt:36 -> Top
+ Stmt:36 -> {}
Stmt:38 -> {38}
Stmt:40 -> {38,40}
Stmt:41 -> {38,40,41}
@@ -333,8 +333,8 @@ Dominators analysis:
Postominators analysis:
Stmt:1 -> {1,3,6,8,53,54,55}
Stmt:3 -> {3,6,8,53,54,55}
- Stmt:4 -> Top
- Stmt:5 -> Top
+ Stmt:4 -> {}
+ Stmt:5 -> {}
Stmt:6 -> {6,8,53,54,55}
Stmt:8 -> {8,54,55}
Stmt:10 -> {10,12,59}
@@ -345,16 +345,16 @@ Postominators analysis:
Stmt:16 -> {16,18,57,58,59}
Stmt:18 -> {18,58,59}
Stmt:20 -> {20,59}
- Stmt:22 -> Top
- Stmt:23 -> Top
- Stmt:24 -> Top
- Stmt:26 -> Top
- Stmt:27 -> Top
- Stmt:28 -> Top
- Stmt:30 -> Top
- Stmt:31 -> Top
- Stmt:33 -> Top
- Stmt:34 -> Top
+ Stmt:22 -> {}
+ Stmt:23 -> {}
+ Stmt:24 -> {}
+ Stmt:26 -> {}
+ Stmt:27 -> {}
+ Stmt:28 -> {}
+ Stmt:30 -> {}
+ Stmt:31 -> {}
+ Stmt:33 -> {}
+ Stmt:34 -> {}
Stmt:36 -> {36}
Stmt:38 -> {38,40,44,46,47,62}
Stmt:40 -> {40,44,46,47,62}
diff --git a/tests/misc/test_dominators.ml b/tests/misc/test_dominators.ml
index 8fad610175..d033442ac2 100644
--- a/tests/misc/test_dominators.ml
+++ b/tests/misc/test_dominators.ml
@@ -48,11 +48,9 @@ let print_nearest f =
(post)dominators of a statement [s] is equal to the singleton [s]. *)
let test_strict f =
let test s dom strict_dom =
- match dom, strict_dom with
- | Some dom, Some strict_dom ->
- assert (StmtSet.diff dom strict_dom == StmtSet.singleton s)
- | None, None -> ()
- | _ -> assert false
+ if StmtSet.is_empty dom
+ then assert (StmtSet.is_empty strict_dom)
+ else assert (StmtSet.diff dom strict_dom == StmtSet.singleton s)
in
List.iter (fun s ->
let dom = Dominators.get_dominators s in
--
GitLab