Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
008ce5ac
Commit
008ce5ac
authored
8 months ago
by
Thibault Martin
Committed by
David Bühler
8 months ago
Browse files
Options
Downloads
Patches
Plain Diff
[tests] Better tests for nearest functions
parent
4a1be85a
No related branches found
No related tags found
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
tests/misc/oracle/test_dominators.res.oracle
+2
-133
2 additions, 133 deletions
tests/misc/oracle/test_dominators.res.oracle
tests/misc/test_dominators.ml
+55
-44
55 additions, 44 deletions
tests/misc/test_dominators.ml
with
57 additions
and
177 deletions
tests/misc/oracle/test_dominators.res.oracle
+
2
−
133
View file @
008ce5ac
[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
...
...
This diff is collapsed.
Click to expand it.
tests/misc/test_dominators.ml
+
55
−
44
View file @
008ce5ac
...
...
@@ -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
()
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment