From 008ce5ac80cd545de45d9cbf18a23995af341c3e Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 6 Aug 2024 12:50:42 +0200
Subject: [PATCH] [tests] Better tests for nearest functions
---
tests/misc/oracle/test_dominators.res.oracle | 135 +------------------
tests/misc/test_dominators.ml | 99 ++++++++------
2 files changed, 57 insertions(+), 177 deletions(-)
diff --git a/tests/misc/oracle/test_dominators.res.oracle b/tests/misc/oracle/test_dominators.res.oracle
index 83659d4eb8..76bebfc2cd 100644
--- a/tests/misc/oracle/test_dominators.res.oracle
+++ b/tests/misc/oracle/test_dominators.res.oracle
@@ -1,4 +1,5 @@
[kernel] Parsing test_dominators.c (with preprocessing)
+
Computing for function f:
{
int __retres;
@@ -30,28 +31,6 @@ Computing for function f:
Immediate dominators of f (sid, idom, ipostdom):
(1, none, 3), (3, 1, 6), (4, 3, none), (5, 4, none), (6, 3, 53),
(53, 6, 8), (8, 53, 54), (54, 8, 55), (55, 54, none)
-Nearest common ancestors/child of f (sid, sid, ancestor, child):
- (1, 1, none, 3), (1, 3, none, 6), (1, 4, none, none), (1, 5, none, none),
- (1, 6, none, 53), (1, 53, none, 8), (1, 8, none, 54), (1, 54, none, 55),
- (1, 55, none, none), (3, 1, none, 6), (3, 3, 1, 6), (3, 4, 1, none),
- (3, 5, 1, none), (3, 6, 1, 53), (3, 53, 1, 8), (3, 8, 1, 54),
- (3, 54, 1, 55), (3, 55, 1, none), (4, 1, none, none), (4, 3, 1, none),
- (4, 4, 3, none), (4, 5, 3, none), (4, 6, 3, none), (4, 53, 3, none),
- (4, 8, 3, none), (4, 54, 3, none), (4, 55, 3, none), (5, 1, none, none),
- (5, 3, 1, none), (5, 4, 3, none), (5, 5, 4, none), (5, 6, 3, none),
- (5, 53, 3, none), (5, 8, 3, none), (5, 54, 3, none), (5, 55, 3, none),
- (6, 1, none, 53), (6, 3, 1, 53), (6, 4, 3, none), (6, 5, 3, none),
- (6, 6, 3, 53), (6, 53, 3, 8), (6, 8, 3, 54), (6, 54, 3, 55),
- (6, 55, 3, none), (53, 1, none, 8), (53, 3, 1, 8), (53, 4, 3, none),
- (53, 5, 3, none), (53, 6, 3, 8), (53, 53, 6, 8), (53, 8, 6, 54),
- (53, 54, 6, 55), (53, 55, 6, none), (8, 1, none, 54), (8, 3, 1, 54),
- (8, 4, 3, none), (8, 5, 3, none), (8, 6, 3, 54), (8, 53, 6, 54),
- (8, 8, 53, 54), (8, 54, 53, 55), (8, 55, 53, none), (54, 1, none, 55),
- (54, 3, 1, 55), (54, 4, 3, none), (54, 5, 3, none), (54, 6, 3, 55),
- (54, 53, 6, 55), (54, 8, 53, 55), (54, 54, 8, 55), (54, 55, 8, none),
- (55, 1, none, none), (55, 3, 1, none), (55, 4, 3, none), (55, 5, 3, none),
- (55, 6, 3, none), (55, 53, 6, none), (55, 8, 53, none), (55, 54, 8, none),
- (55, 55, 54, none)
Computing for function g:
{
@@ -89,41 +68,6 @@ Immediate dominators of g (sid, idom, ipostdom):
(10, none, 12), (12, 10, 59), (13, 12, 15), (14, none, 15), (15, 13, 20),
(16, 12, 57), (57, 16, 18), (18, 57, 58), (58, 18, 59), (20, 15, 59),
(59, 12, none)
-Nearest common ancestors/child of g (sid, sid, ancestor, child):
- (10, 10, none, 12), (10, 12, none, 59), (10, 13, none, 59),
- (10, 14, none, 59), (10, 15, none, 59), (10, 16, none, 59),
- (10, 57, none, 59), (10, 18, none, 59), (10, 58, none, 59),
- (10, 20, none, 59), (10, 59, none, none), (12, 10, none, 59),
- (12, 12, 10, 59), (12, 13, 10, 59), (12, 14, none, 59), (12, 15, 10, 59),
- (12, 16, 10, 59), (12, 57, 10, 59), (12, 18, 10, 59), (12, 58, 10, 59),
- (12, 20, 10, 59), (12, 59, 10, none), (13, 10, none, 59), (13, 12, 10, 59),
- (13, 13, 12, 15), (13, 14, none, 15), (13, 15, 12, 20), (13, 16, 12, 59),
- (13, 57, 12, 59), (13, 18, 12, 59), (13, 58, 12, 59), (13, 20, 12, 59),
- (13, 59, 12, none), (14, 10, none, 59), (14, 12, none, 59),
- (14, 13, none, 15), (14, 14, none, 15), (14, 15, none, 20),
- (14, 16, none, 59), (14, 57, none, 59), (14, 18, none, 59),
- (14, 58, none, 59), (14, 20, none, 59), (14, 59, none, none),
- (15, 10, none, 59), (15, 12, 10, 59), (15, 13, 12, 20), (15, 14, none, 20),
- (15, 15, 13, 20), (15, 16, 12, 59), (15, 57, 12, 59), (15, 18, 12, 59),
- (15, 58, 12, 59), (15, 20, 13, 59), (15, 59, 12, none), (16, 10, none, 59),
- (16, 12, 10, 59), (16, 13, 12, 59), (16, 14, none, 59), (16, 15, 12, 59),
- (16, 16, 12, 57), (16, 57, 12, 18), (16, 18, 12, 58), (16, 58, 12, 59),
- (16, 20, 12, 59), (16, 59, 12, none), (57, 10, none, 59), (57, 12, 10, 59),
- (57, 13, 12, 59), (57, 14, none, 59), (57, 15, 12, 59), (57, 16, 12, 18),
- (57, 57, 16, 18), (57, 18, 16, 58), (57, 58, 16, 59), (57, 20, 12, 59),
- (57, 59, 12, none), (18, 10, none, 59), (18, 12, 10, 59), (18, 13, 12, 59),
- (18, 14, none, 59), (18, 15, 12, 59), (18, 16, 12, 58), (18, 57, 16, 58),
- (18, 18, 57, 58), (18, 58, 57, 59), (18, 20, 12, 59), (18, 59, 12, none),
- (58, 10, none, 59), (58, 12, 10, 59), (58, 13, 12, 59), (58, 14, none, 59),
- (58, 15, 12, 59), (58, 16, 12, 59), (58, 57, 16, 59), (58, 18, 57, 59),
- (58, 58, 18, 59), (58, 20, 12, 59), (58, 59, 12, none), (20, 10, none, 59),
- (20, 12, 10, 59), (20, 13, 12, 59), (20, 14, none, 59), (20, 15, 13, 59),
- (20, 16, 12, 59), (20, 57, 12, 59), (20, 18, 12, 59), (20, 58, 12, 59),
- (20, 20, 15, 59), (20, 59, 12, none), (59, 10, none, none),
- (59, 12, 10, none), (59, 13, 12, none), (59, 14, none, none),
- (59, 15, 12, none), (59, 16, 12, none), (59, 57, 12, none),
- (59, 18, 12, none), (59, 58, 12, none), (59, 20, 12, none),
- (59, 59, 12, none)
Computing for function h:
{
@@ -167,48 +111,6 @@ Immediate dominators of h (sid, idom, ipostdom):
(22, none, none), (23, 22, none), (24, 23, none), (26, 24, none),
(27, 26, none), (28, 26, none), (30, 28, none), (31, 30, none),
(33, 30, none), (34, 27, none), (36, none, none)
-Nearest common ancestors/child of h (sid, sid, ancestor, child):
- (22, 22, none, none), (22, 23, none, none), (22, 24, none, none),
- (22, 26, none, none), (22, 27, none, none), (22, 28, none, none),
- (22, 30, none, none), (22, 31, none, none), (22, 33, none, none),
- (22, 34, none, none), (22, 36, none, none), (23, 22, none, none),
- (23, 23, 22, none), (23, 24, 22, none), (23, 26, 22, none),
- (23, 27, 22, none), (23, 28, 22, none), (23, 30, 22, none),
- (23, 31, 22, none), (23, 33, 22, none), (23, 34, 22, none),
- (23, 36, none, none), (24, 22, none, none), (24, 23, 22, none),
- (24, 24, 23, none), (24, 26, 23, none), (24, 27, 23, none),
- (24, 28, 23, none), (24, 30, 23, none), (24, 31, 23, none),
- (24, 33, 23, none), (24, 34, 23, none), (24, 36, none, none),
- (26, 22, none, none), (26, 23, 22, none), (26, 24, 23, none),
- (26, 26, 24, none), (26, 27, 24, none), (26, 28, 24, none),
- (26, 30, 24, none), (26, 31, 24, none), (26, 33, 24, none),
- (26, 34, 24, none), (26, 36, none, none), (27, 22, none, none),
- (27, 23, 22, none), (27, 24, 23, none), (27, 26, 24, none),
- (27, 27, 26, none), (27, 28, 26, none), (27, 30, 26, none),
- (27, 31, 26, none), (27, 33, 26, none), (27, 34, 26, none),
- (27, 36, none, none), (28, 22, none, none), (28, 23, 22, none),
- (28, 24, 23, none), (28, 26, 24, none), (28, 27, 26, none),
- (28, 28, 26, none), (28, 30, 26, none), (28, 31, 26, none),
- (28, 33, 26, none), (28, 34, 26, none), (28, 36, none, none),
- (30, 22, none, none), (30, 23, 22, none), (30, 24, 23, none),
- (30, 26, 24, none), (30, 27, 26, none), (30, 28, 26, none),
- (30, 30, 28, none), (30, 31, 28, none), (30, 33, 28, none),
- (30, 34, 26, none), (30, 36, none, none), (31, 22, none, none),
- (31, 23, 22, none), (31, 24, 23, none), (31, 26, 24, none),
- (31, 27, 26, none), (31, 28, 26, none), (31, 30, 28, none),
- (31, 31, 30, none), (31, 33, 30, none), (31, 34, 26, none),
- (31, 36, none, none), (33, 22, none, none), (33, 23, 22, none),
- (33, 24, 23, none), (33, 26, 24, none), (33, 27, 26, none),
- (33, 28, 26, none), (33, 30, 28, none), (33, 31, 30, none),
- (33, 33, 30, none), (33, 34, 26, none), (33, 36, none, none),
- (34, 22, none, none), (34, 23, 22, none), (34, 24, 23, none),
- (34, 26, 24, none), (34, 27, 26, none), (34, 28, 26, none),
- (34, 30, 26, none), (34, 31, 26, none), (34, 33, 26, none),
- (34, 34, 27, none), (34, 36, none, none), (36, 22, none, none),
- (36, 23, none, none), (36, 24, none, none), (36, 26, none, none),
- (36, 27, none, none), (36, 28, none, none), (36, 30, none, none),
- (36, 31, none, none), (36, 33, none, none), (36, 34, none, none),
- (36, 36, none, none)
Computing for function i:
{
@@ -251,40 +153,6 @@ Immediate dominators of i (sid, idom, ipostdom):
(38, none, 40), (40, 38, 44), (41, 40, 50), (43, 40, 44), (44, 40, 46),
(46, 44, 47), (47, 46, 62), (48, 46, 49), (49, 48, 50), (50, 40, 44),
(62, 47, none)
-Nearest common ancestors/child of i (sid, sid, ancestor, child):
- (38, 38, none, 40), (38, 40, none, 44), (38, 41, none, 44),
- (38, 43, none, 44), (38, 44, none, 46), (38, 46, none, 47),
- (38, 47, none, 62), (38, 48, none, 44), (38, 49, none, 44),
- (38, 50, none, 44), (38, 62, none, none), (40, 38, none, 44),
- (40, 40, 38, 44), (40, 41, 38, 44), (40, 43, 38, 44), (40, 44, 38, 46),
- (40, 46, 38, 47), (40, 47, 38, 62), (40, 48, 38, 44), (40, 49, 38, 44),
- (40, 50, 38, 44), (40, 62, 38, none), (41, 38, none, 44), (41, 40, 38, 44),
- (41, 41, 40, 50), (41, 43, 40, 44), (41, 44, 40, 46), (41, 46, 40, 47),
- (41, 47, 40, 62), (41, 48, 40, 50), (41, 49, 40, 50), (41, 50, 40, 44),
- (41, 62, 40, none), (43, 38, none, 44), (43, 40, 38, 44), (43, 41, 40, 44),
- (43, 43, 40, 44), (43, 44, 40, 46), (43, 46, 40, 47), (43, 47, 40, 62),
- (43, 48, 40, 44), (43, 49, 40, 44), (43, 50, 40, 44), (43, 62, 40, none),
- (44, 38, none, 46), (44, 40, 38, 46), (44, 41, 40, 46), (44, 43, 40, 46),
- (44, 44, 40, 46), (44, 46, 40, 47), (44, 47, 40, 62), (44, 48, 40, 46),
- (44, 49, 40, 46), (44, 50, 40, 46), (44, 62, 40, none), (46, 38, none, 47),
- (46, 40, 38, 47), (46, 41, 40, 47), (46, 43, 40, 47), (46, 44, 40, 47),
- (46, 46, 44, 47), (46, 47, 44, 62), (46, 48, 44, 47), (46, 49, 44, 47),
- (46, 50, 40, 47), (46, 62, 44, none), (47, 38, none, 62), (47, 40, 38, 62),
- (47, 41, 40, 62), (47, 43, 40, 62), (47, 44, 40, 62), (47, 46, 44, 62),
- (47, 47, 46, 62), (47, 48, 46, 62), (47, 49, 46, 62), (47, 50, 40, 62),
- (47, 62, 46, none), (48, 38, none, 44), (48, 40, 38, 44), (48, 41, 40, 50),
- (48, 43, 40, 44), (48, 44, 40, 46), (48, 46, 44, 47), (48, 47, 46, 62),
- (48, 48, 46, 49), (48, 49, 46, 50), (48, 50, 40, 44), (48, 62, 46, none),
- (49, 38, none, 44), (49, 40, 38, 44), (49, 41, 40, 50), (49, 43, 40, 44),
- (49, 44, 40, 46), (49, 46, 44, 47), (49, 47, 46, 62), (49, 48, 46, 50),
- (49, 49, 48, 50), (49, 50, 40, 44), (49, 62, 46, none), (50, 38, none, 44),
- (50, 40, 38, 44), (50, 41, 40, 44), (50, 43, 40, 44), (50, 44, 40, 46),
- (50, 46, 40, 47), (50, 47, 40, 62), (50, 48, 40, 44), (50, 49, 40, 44),
- (50, 50, 40, 44), (50, 62, 40, none), (62, 38, none, none),
- (62, 40, 38, none), (62, 41, 40, none), (62, 43, 40, none),
- (62, 44, 40, none), (62, 46, 44, none), (62, 47, 46, none),
- (62, 48, 46, none), (62, 49, 46, none), (62, 50, 40, none),
- (62, 62, 47, none)
Dominators analysis:
Stmt:1 -> {1}
@@ -382,6 +250,7 @@ Dominators analysis:
Postominators analysis:
Empty
+Trigger some errors/warnings :
[kernel] Failure: Statement -1 is not part of a function
[kernel] Warning: No statement in function stop: Dominators analysis cannot be done
[kernel] Warning: No statement in function stop: PostDominators analysis cannot be done
diff --git a/tests/misc/test_dominators.ml b/tests/misc/test_dominators.ml
index c9c03a2b73..eb26706d80 100644
--- a/tests/misc/test_dominators.ml
+++ b/tests/misc/test_dominators.ml
@@ -9,9 +9,6 @@ let get = function
let pp_res =
Pretty_utils.pp_list ~pre:"(" ~sep:", " ~suf:")" Format.pp_print_string
-let first_stmt_f = ref None
-let first_stmt_g = ref None
-
(** For each statement of [f], find its immediate dominator and postdominator
and print the triplets. *)
let print_immediate f =
@@ -26,24 +23,6 @@ let print_immediate f =
f.svar.vname
(Pretty_utils.pp_list ~pre:"@[" ~sep:",@ " ~suf:"@]" pp_res) res
-(** For each couple of statement of [f], find their common ancestor and child
- and print the quadruplets. *)
-let print_nearest f =
- assert (Dominators.nearest_common_ancestor [] = None);
- let res =
- List.map (fun s ->
- List.map (fun s' ->
- let dom = Dominators.nearest_common_ancestor [s; s'] in
- let postdom = Dominators.nearest_common_child [s; s'] in
- [string_of_int s.sid; string_of_int s'.sid; get dom; get postdom]
- ) f.sallstmts
- ) f.sallstmts
- |> List.flatten
- in
- Format.printf "@[<v2>Nearest common ancestors/child of %s (sid, sid, ancestor, child):@;%a@]@;"
- f.svar.vname
- (Pretty_utils.pp_list ~pre:"@[" ~sep:",@ " ~suf:"@]" pp_res) res
-
(* Make sure that the difference between (post)dominators and strict
(post)dominators of a statement [s] is equal to the singleton [s]. *)
let test_strict f =
@@ -63,12 +42,46 @@ let test_strict f =
assert (Dominators.strictly_postdominates s s = false)
) f.sallstmts
+let test_nearest kf f =
+ (* Simple test for empty list coverage of nearest function. *)
+ assert (Dominators.nearest_common_ancestor [] = None);
+ assert (Dominators.nearest_common_child [] = None);
+
+ (* Since first and last statement do not have an ancestor/child,
+ common nearest for all statements should be empty. *)
+ assert (Dominators.nearest_common_ancestor f.sallstmts = None);
+ assert (Dominators.nearest_common_child f.sallstmts = None);
+
+ if List.length f.sallstmts > 1 then begin
+
+ let first = Kernel_function.find_first_stmt kf in
+ let last = Kernel_function.find_return kf in
+ let all_but_first = List.filter (fun s -> s != first) f.sallstmts in
+ let all_but_last = List.filter (fun s -> s != last) f.sallstmts in
+
+ (* Test that all statements (except the first one) have as common ancestor
+ the first statement of f, unless one of them is unreachable. *)
+ begin match Dominators.nearest_common_ancestor all_but_first with
+ | None -> (* At leats one statement is unreachable. *) ()
+ | Some ancestor -> assert (first == ancestor)
+ end;
+
+ (* Test that all statements (except the last one) have as common child
+ the return statement of f, unless one of them is unreachable. This test
+ supposes that frama-c's normalization removed all but one return statement.
+ *)
+ begin match Dominators.nearest_common_child all_but_last with
+ | None -> (* At leats one statement is unreachable. *) ()
+ | Some child -> assert (last == child)
+ end
+ end
+
class visitPostDom = object(self)
inherit Visitor.frama_c_inplace
method! vfunc f =
let kf = Option.get (self#current_kf) in
- Format.printf "@[<v>Computing for function %s:@;%a@?@;@?"
+ Format.printf "@.@[<v>Computing for function %s:@;%a@?@;@?@]"
f.svar.vname Cil_printer.pp_block f.sbody;
Dominators.compute_dominators kf;
@@ -78,37 +91,35 @@ class visitPostDom = object(self)
Dominators.print_dot_postdominators "postdom_graph" kf;
print_immediate f;
- print_nearest f;
test_strict f;
+ test_nearest kf f;
- Format.printf "@]@.";
SkipChildren
end
-let catch f x =
- try ignore (f x)
- with Log.AbortFatal _ -> ()
-
let cover_errors () =
+ Format.printf "Trigger some errors/warnings :@.";
+
+ (* Test when a statement is not in a function. *)
let loc = Cil_datatype.Location.unknown in
- (* Test statement not in a function. *)
let skip = Cil_builder.Pure.(cil_stmt ~loc skip) in
- catch Dominators.get_postdominators skip;
- let trigger kf =
- match kf.fundec with
- | Definition _ -> ()
- | Declaration _ ->
- (* Test Kernel_function.find_first_stmt on decl. *)
- Dominators.compute_dominators kf;
- (* Test Kernel_function.find_return on decl. *)
- Dominators.compute_postdominators kf;
- (* Test print_dot on decl. *)
- Dominators.print_dot_dominators "tmp" kf
- in
- Globals.Functions.iter trigger
+ try ignore (Dominators.get_postdominators skip) with Log.AbortFatal _ -> ();
+
+ let trigger kf =
+ match kf.fundec with
+ | Definition _ -> ()
+ | Declaration _ ->
+ (* Test Kernel_function.find_first_stmt on decl. *)
+ ignore @@ Dominators.compute_dominators kf;
+ (* Test Kernel_function.find_return on decl. *)
+ ignore @@ Dominators.compute_postdominators kf;
+ (* Test print_dot on decl. *)
+ ignore @@ Dominators.print_dot_dominators "tmp" kf
+ in
+ Globals.Functions.iter trigger
let pretty () =
- Format.printf "@[<v2>Dominators analysis:@;%a@]\n@."
+ Format.printf "@.@[<v2>Dominators analysis:@;%a@]\n@."
Dominators.pretty_dominators ();
Format.printf "@[<v2>Postominators analysis:@;%a@]\n@."
Dominators.pretty_postdominators ()
@@ -117,7 +128,7 @@ let startup () =
ignore (Cil.visitCilFileSameGlobals (new visitPostDom:>Cil.cilVisitor) (Ast.get ()));
pretty ();
Ast.mark_as_changed ();
- Format.printf "Invalidate tables, which should now be empty\n@.";
+ Format.printf "Invalidate tables, which should now be empty\n";
pretty ();
cover_errors ()
--
GitLab