From 28cfb4f2656aede4e6717253217a1ba7c2eee75f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 21 Apr 2022 11:52:43 +0200
Subject: [PATCH] [Eva] Fixes the multidim domain on escaping variables and
empty structs.
---
.../value/domains/multidim/multidim_domain.ml | 9 +-
.../oracle_multidim/empty_struct.0.res.oracle | 20 ----
.../oracle_multidim/empty_struct.1.res.oracle | 10 --
.../oracle_multidim/empty_struct.2.res.oracle | 10 --
.../oracle_multidim/empty_struct.3.res.oracle | 10 --
.../oracle_multidim/empty_struct.5.res.oracle | 23 ----
.../oracle_multidim/empty_struct2.res.oracle | 95 ----------------
.../oracle_multidim/empty_union.res.oracle | 73 +++++-------
tests/value/oracle_multidim/local.res.oracle | 106 ------------------
.../oracle_multidim/split_return.0.res.oracle | 29 -----
.../oracle_multidim/split_return.1.res.oracle | 29 -----
.../oracle_multidim/split_return.3.res.oracle | 29 -----
.../oracle_multidim/split_return.4.res.oracle | 58 ----------
13 files changed, 34 insertions(+), 467 deletions(-)
delete mode 100644 tests/value/oracle_multidim/empty_struct.0.res.oracle
delete mode 100644 tests/value/oracle_multidim/empty_struct.1.res.oracle
delete mode 100644 tests/value/oracle_multidim/empty_struct.2.res.oracle
delete mode 100644 tests/value/oracle_multidim/empty_struct.3.res.oracle
delete mode 100644 tests/value/oracle_multidim/empty_struct.5.res.oracle
delete mode 100644 tests/value/oracle_multidim/empty_struct2.res.oracle
delete mode 100644 tests/value/oracle_multidim/local.res.oracle
delete mode 100644 tests/value/oracle_multidim/split_return.0.res.oracle
delete mode 100644 tests/value/oracle_multidim/split_return.1.res.oracle
delete mode 100644 tests/value/oracle_multidim/split_return.3.res.oracle
delete mode 100644 tests/value/oracle_multidim/split_return.4.res.oracle
diff --git a/src/plugins/value/domains/multidim/multidim_domain.ml b/src/plugins/value/domains/multidim/multidim_domain.ml
index d5cadfc6f06..2207543477b 100644
--- a/src/plugins/value/domains/multidim/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim/multidim_domain.ml
@@ -686,7 +686,14 @@ struct
| `Value loc ->
let update value' =
let v = Value_or_Uninitialized.narrow value value' in
- if Value_or_Uninitialized.is_bottom v then `Bottom else `Value v
+ (* The value can legitimately be bottom on escaping variables (not
+ tracked by the multidim domain), or on empty structs or unions.
+ In these cases, do not reduce the state to bottom. *)
+ if Value_or_Uninitialized.is_bottom v
+ && not record.value.escaping
+ && not (Int_Base.is_zero (Bit_utils.sizeof_lval lv))
+ then `Bottom
+ else `Value v
in
if Location.is_singleton loc
then reinforce ~oracle update state loc
diff --git a/tests/value/oracle_multidim/empty_struct.0.res.oracle b/tests/value/oracle_multidim/empty_struct.0.res.oracle
deleted file mode 100644
index 321b1ceb7e8..00000000000
--- a/tests/value/oracle_multidim/empty_struct.0.res.oracle
+++ /dev/null
@@ -1,20 +0,0 @@
-12c12
-< p ∈ {{ (void *)&s }}
----
-> NON TERMINATING FUNCTION
-13a14
-> [from] Non-terminating function main (no dependencies)
-18c19
-< NO EFFECTS
----
-> NON TERMINATING - NO EFFECTS
-34c35
-< p ∈ {{ (void *)&s }}
----
-> NON TERMINATING FUNCTION
-35a37
-> [from] Non-terminating function main (no dependencies)
-40c42
-< NO EFFECTS
----
-> NON TERMINATING - NO EFFECTS
diff --git a/tests/value/oracle_multidim/empty_struct.1.res.oracle b/tests/value/oracle_multidim/empty_struct.1.res.oracle
deleted file mode 100644
index 00c678fbe5b..00000000000
--- a/tests/value/oracle_multidim/empty_struct.1.res.oracle
+++ /dev/null
@@ -1,10 +0,0 @@
-12c12
-< p ∈ {{ (void *)&s }}
----
-> NON TERMINATING FUNCTION
-13a14
-> [from] Non-terminating function main (no dependencies)
-18c19
-< NO EFFECTS
----
-> NON TERMINATING - NO EFFECTS
diff --git a/tests/value/oracle_multidim/empty_struct.2.res.oracle b/tests/value/oracle_multidim/empty_struct.2.res.oracle
deleted file mode 100644
index 00c678fbe5b..00000000000
--- a/tests/value/oracle_multidim/empty_struct.2.res.oracle
+++ /dev/null
@@ -1,10 +0,0 @@
-12c12
-< p ∈ {{ (void *)&s }}
----
-> NON TERMINATING FUNCTION
-13a14
-> [from] Non-terminating function main (no dependencies)
-18c19
-< NO EFFECTS
----
-> NON TERMINATING - NO EFFECTS
diff --git a/tests/value/oracle_multidim/empty_struct.3.res.oracle b/tests/value/oracle_multidim/empty_struct.3.res.oracle
deleted file mode 100644
index 00c678fbe5b..00000000000
--- a/tests/value/oracle_multidim/empty_struct.3.res.oracle
+++ /dev/null
@@ -1,10 +0,0 @@
-12c12
-< p ∈ {{ (void *)&s }}
----
-> NON TERMINATING FUNCTION
-13a14
-> [from] Non-terminating function main (no dependencies)
-18c19
-< NO EFFECTS
----
-> NON TERMINATING - NO EFFECTS
diff --git a/tests/value/oracle_multidim/empty_struct.5.res.oracle b/tests/value/oracle_multidim/empty_struct.5.res.oracle
deleted file mode 100644
index 75fbe49c4f4..00000000000
--- a/tests/value/oracle_multidim/empty_struct.5.res.oracle
+++ /dev/null
@@ -1,23 +0,0 @@
-17,19d16
-< [eva] empty_struct.c:86: Call to builtin free
-< [eva] empty_struct.c:86:
-< function free: precondition 'freeable' got status valid.
-24,27c21
-< __fc_heap_status ∈ [--..--]
-< q ∈ {{ NULL ; &__malloc_main3_l78[-1] }} or ESCAPINGADDR
-< r ∈ {{ NULL ; &__realloc_main3_l79[-1] }} or ESCAPINGADDR
-< p ∈ {{ &empties[-1] }}
----
-> NON TERMINATING FUNCTION
-33,34c27
-< [from] Computing for function free <-main3
-< [from] Done for function free
----
-> [from] Non-terminating function main3 (no dependencies)
-38,39d30
-< [from] Function free:
-< __fc_heap_status FROM __fc_heap_status (and SELF)
-47c38
-< __fc_heap_status FROM __fc_heap_status (and SELF)
----
-> NON TERMINATING - NO EFFECTS
diff --git a/tests/value/oracle_multidim/empty_struct2.res.oracle b/tests/value/oracle_multidim/empty_struct2.res.oracle
deleted file mode 100644
index 09e8ebd43d5..00000000000
--- a/tests/value/oracle_multidim/empty_struct2.res.oracle
+++ /dev/null
@@ -1,95 +0,0 @@
-9,46d8
-< [eva] empty_struct2.c:50: Frama_C_show_each_global_empty: ∅
-< [eva] empty_struct2.c:51: Frama_C_show_each_e1: ∅
-< [eva] empty_struct2.c:52: Call to builtin memcpy
-< [eva] empty_struct2.c:52:
-< function memcpy: precondition 'valid_dest' got status valid.
-< [eva] empty_struct2.c:52:
-< function memcpy: precondition 'valid_src' got status valid.
-< [eva] empty_struct2.c:52:
-< function memcpy: precondition 'separation' got status valid.
-< [eva] FRAMAC_SHARE/libc/string.h:101:
-< cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
-< [eva] empty_struct2.c:57: Call to builtin memcpy
-< [eva] empty_struct2.c:57:
-< function memcpy: precondition 'valid_dest' got status valid.
-< [eva] empty_struct2.c:57:
-< function memcpy: precondition 'valid_src' got status valid.
-< [eva] empty_struct2.c:57:
-< function memcpy: precondition 'separation' got status valid.
-< [eva] empty_struct2.c:58:
-< Frama_C_show_each_c2: .a ∈ {42}
-< .b ∈ {77}
-< [eva] empty_struct2.c:59: Frama_C_show_each_c2_e: ∅
-< [eva] computing for function f <- main.
-< Called from empty_struct2.c:60.
-< [eva] Recording results for f
-< [eva] Done for function f
-< [eva] empty_struct2.c:62:
-< Frama_C_show_each_res: .a ∈ {87}
-< .b ∈ {39}
-< [eva] empty_struct2.c:66: assertion got status valid.
-< [eva] computing for function ret_empty <- main.
-< Called from empty_struct2.c:68.
-< [eva] using specification for function ret_empty
-< [eva] Done for function ret_empty
-< [eva] computing for function ret_ptr_empty <- main.
-< Called from empty_struct2.c:69.
-< [eva] using specification for function ret_ptr_empty
-< [eva] Done for function ret_ptr_empty
-50,52d11
-< [eva:final-states] Values at end of function f:
-< res.a ∈ {87}
-< .b ∈ {39}
-54,66c13
-< c1.a ∈ {42}
-< .b ∈ {77}
-< c2.a ∈ {42}
-< .b ∈ {77}
-< res.a ∈ {87}
-< .b ∈ {39}
-< cb.i ∈ {91}
-< ce.ch ∈ {90}
-< p ∈ {{ (struct empty *)&cb }}
-< ptr_ret ∈ {{ &global_empty }}
-< __retres ∈ {0}
-< [from] Computing for function f
-< [from] Done for function f
----
-> NON TERMINATING FUNCTION
-68,73c15
-< [from] Computing for function memcpy <-main
-< [from] Done for function memcpy
-< [from] Computing for function ret_empty <-main
-< [from] Done for function ret_empty
-< [from] Computing for function ret_ptr_empty <-main
-< [from] Done for function ret_ptr_empty
----
-> [from] Non-terminating function main (no dependencies)
-77,85d18
-< [from] Function f:
-< \result FROM s
-< [from] Function memcpy:
-< c2 FROM c1 (and SELF)
-< \result FROM dest
-< [from] Function ret_empty:
-< \result FROM \nothing
-< [from] Function ret_ptr_empty:
-< \result FROM pg
-87c20
-< \result FROM \nothing
----
-> NON TERMINATING - NO EFFECTS
-89,92d21
-< [inout] Out (internal) for function f:
-< res
-< [inout] Inputs for function f:
-< nondet
-94c23
-< c1; c2; res; cb; ce; p; ptr_ret; __retres
----
-> \nothing
-96c25
-< nondet; pg
----
-> \nothing
diff --git a/tests/value/oracle_multidim/empty_union.res.oracle b/tests/value/oracle_multidim/empty_union.res.oracle
index 82053116447..23a5ad4e379 100644
--- a/tests/value/oracle_multidim/empty_union.res.oracle
+++ b/tests/value/oracle_multidim/empty_union.res.oracle
@@ -1,28 +1,9 @@
-16,46d15
-< [eva] empty_union.c:70: Frama_C_show_each_global_empty: ∅
-< [eva] empty_union.c:71: Frama_C_show_each_e1: ∅
-< [eva] empty_union.c:72: Call to builtin memcpy
-< [eva] empty_union.c:72:
-< function memcpy: precondition 'valid_dest' got status valid.
-< [eva] empty_union.c:72:
-< function memcpy: precondition 'valid_src' got status valid.
-< [eva] empty_union.c:72:
-< function memcpy: precondition 'separation' got status valid.
-< [eva] FRAMAC_SHARE/libc/string.h:101:
-< cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
-< [eva] empty_union.c:77: Call to builtin memcpy
-< [eva] empty_union.c:77:
-< function memcpy: precondition 'valid_dest' got status valid.
-< [eva] empty_union.c:77:
-< function memcpy: precondition 'valid_src' got status valid.
-< [eva] empty_union.c:77:
-< function memcpy: precondition 'separation' got status valid.
-< [eva] empty_union.c:78: Frama_C_show_each_c2: {77}
-< [eva] empty_union.c:79: Frama_C_show_each_c2_e: ∅
-< [eva] computing for function f <- main.
-< Called from empty_union.c:80.
-< [eva] Recording results for f
-< [eva] Done for function f
+37a38,41
+> [eva] empty_union.c:30:
+> The evaluation of the expression s.b + 10
+> led to bottom without alarms:
+> at this point the product of states has no possible concretization.
+40,46d43
< [eva] computing for function copy_empty <- main.
< Called from empty_union.c:81.
< [eva:alarm] empty_union.c:37: Warning:
@@ -30,12 +11,14 @@
< [eva] Recording results for copy_empty
< [eva] Done for function copy_empty
< [eva] empty_union.c:83: Frama_C_show_each_res: {74}
-50,53d18
+50,51d46
< [eva:final-states] Values at end of function copy_empty:
<
-< [eva:final-states] Values at end of function f:
+53c48
< res{.a; .e{}; .b} ∈ {74}
-55,66c20
+---
+> NON TERMINATING FUNCTION
+55,64c50
< c1{.a; .e{}; .b} ∈ {77}
< c2{.a; .e{}; .b} ∈ {77}
< res{.a; .e{}; .b} ∈ {74}
@@ -46,41 +29,37 @@
< __retres ∈ {0}
< [from] Computing for function copy_empty
< [from] Done for function copy_empty
-< [from] Computing for function f
-< [from] Done for function f
---
> NON TERMINATING FUNCTION
-68,69c22
-< [from] Computing for function memcpy <-main
-< [from] Done for function memcpy
----
+65a52
+> [from] Non-terminating function f (no dependencies)
+69a57
> [from] Non-terminating function main (no dependencies)
-73,79d25
+73,74d60
< [from] Function copy_empty:
< NO EFFECTS
-< [from] Function f:
+76c62
< \result FROM s
-< [from] Function memcpy:
-< c2 FROM c1 (and SELF)
-< \result FROM dest
-81c27
+---
+> NON TERMINATING - NO EFFECTS
+81c67
< \result FROM \nothing
---
> NON TERMINATING - NO EFFECTS
-83,90d28
+83,86d68
< [inout] Out (internal) for function copy_empty:
< \nothing
< [inout] Inputs for function copy_empty:
< \nothing
-< [inout] Out (internal) for function f:
-< res
-< [inout] Inputs for function f:
+90c72
< nondet
-92c30
-< c1; c2; res; cb; ce; p; pc; __retres
---
> \nothing
-94c32
+92c74
+< c1; c2; res; cb; ce; p; pc; __retres
+---
+> c1; c2; res
+94c76
< nondet
---
> \nothing
diff --git a/tests/value/oracle_multidim/local.res.oracle b/tests/value/oracle_multidim/local.res.oracle
deleted file mode 100644
index 399c536a0fe..00000000000
--- a/tests/value/oracle_multidim/local.res.oracle
+++ /dev/null
@@ -1,106 +0,0 @@
-20,54d19
-< [eva] computing for function g <- main.
-< Called from local.i:34.
-< [eva] local.i:13: Reusing old results for call to f
-< [eva:locals-escaping] local.i:13: Warning:
-< locals {a} escaping the scope of f through X
-< [eva:locals-escaping] local.i:13: Warning:
-< locals {b} escaping the scope of f through \result<f>
-< [eva:alarm] local.i:14: Warning:
-< accessing left-value that contains escaping addresses.
-< assert ¬\dangling(&T);
-< [eva] Recording results for g
-< [eva] Done for function g
-< [eva:locals-escaping] local.i:34: Warning:
-< locals {d} escaping the scope of g through U
-< [eva:locals-escaping] local.i:34: Warning:
-< locals {d} escaping the scope of g through \result<g>
-< [eva] local.i:35:
-< Frama_C_dump_each:
-< # cvalue:
-< X ∈ ESCAPINGADDR
-< Y ∈ ESCAPINGADDR
-< Z ∈ ESCAPINGADDR
-< T ∈ ESCAPINGADDR
-< U ∈ ESCAPINGADDR
-< V ∈ {0}
-< e ∈ UNINITIALIZED
-< ==END OF DUMP==
-< [eva] computing for function h <- main.
-< Called from local.i:36.
-< [eva] Recording results for h
-< [eva] Done for function h
-< [eva] computing for function i <- main.
-< Called from local.i:37.
-< [eva] Recording results for i
-< [eva] Done for function i
-57d21
-< [eva] local.i:14: assertion 'Eva,dangling_pointer' got final status invalid.
-62,70d25
-< [eva:final-states] Values at end of function g:
-< X ∈ ESCAPINGADDR
-< T ∈ ESCAPINGADDR
-< U ∈ {{ &d }}
-< d ∈ [--..--]
-< [eva:final-states] Values at end of function h:
-< __retres ∈ {{ &e + {4} }}
-< [eva:final-states] Values at end of function i:
-< x ∈ {{ &local }}
-72,77c27
-< X ∈ ESCAPINGADDR
-< Y ∈ ESCAPINGADDR
-< Z ∈ ESCAPINGADDR
-< T ∈ ESCAPINGADDR
-< U ∈ ESCAPINGADDR
-< V ∈ {{ &e + {4} }}
----
-> NON TERMINATING FUNCTION
-80,85d29
-< [from] Computing for function g
-< [from] Done for function g
-< [from] Computing for function h
-< [from] Done for function h
-< [from] Computing for function i
-< [from] Done for function i
-86a31
-> [from] Non-terminating function main (no dependencies)
-93,101d37
-< [from] Function g:
-< X FROM \nothing
-< T FROM \nothing
-< U FROM \nothing
-< \result FROM \nothing
-< [from] Function h:
-< \result FROM x
-< [from] Function i:
-< NO EFFECTS
-103,108c39
-< X FROM \nothing
-< Y FROM \nothing
-< Z FROM \nothing
-< T FROM \nothing
-< U FROM \nothing
-< V FROM \nothing
----
-> NON TERMINATING - NO EFFECTS
-114,125d44
-< [inout] Out (internal) for function g:
-< X; T; U; d
-< [inout] Inputs for function g:
-< T; U
-< [inout] Out (internal) for function h:
-< __retres
-< [inout] Inputs for function h:
-< \nothing
-< [inout] Out (internal) for function i:
-< x
-< [inout] Inputs for function i:
-< \nothing
-127c46
-< X; Y; Z; T; U; V
----
-> X; Y
-129c48
-< T; U
----
-> \nothing
diff --git a/tests/value/oracle_multidim/split_return.0.res.oracle b/tests/value/oracle_multidim/split_return.0.res.oracle
deleted file mode 100644
index 597bd2c7d55..00000000000
--- a/tests/value/oracle_multidim/split_return.0.res.oracle
+++ /dev/null
@@ -1,29 +0,0 @@
-175,176c175
-< y ∈ {0} or UNINITIALIZED
-< q ∈ ESCAPINGADDR
----
-> NON TERMINATING FUNCTION
-178,182c177
-< i2 ∈ {0; 5}
-< i3 ∈ {0; 5}
-< i4 ∈ {0; 5}
-< i5 ∈ {0; 5}
-< v7 ∈ {0; 1}
----
-> NON TERMINATING FUNCTION
-219a215
-> [from] Non-terminating function main9 (no dependencies)
-221a218
-> [from] Non-terminating function main (no dependencies)
-269c266
-< NO EFFECTS
----
-> NON TERMINATING - NO EFFECTS
-271,275c268
-< i2 FROM i2
-< i3 FROM i3
-< i4 FROM i4
-< i5 FROM i5
-< v7 FROM v
----
-> NON TERMINATING - NO EFFECTS
diff --git a/tests/value/oracle_multidim/split_return.1.res.oracle b/tests/value/oracle_multidim/split_return.1.res.oracle
deleted file mode 100644
index 270ad4b63bd..00000000000
--- a/tests/value/oracle_multidim/split_return.1.res.oracle
+++ /dev/null
@@ -1,29 +0,0 @@
-177,178c177
-< y ∈ {0} or UNINITIALIZED
-< q ∈ ESCAPINGADDR
----
-> NON TERMINATING FUNCTION
-180,184c179
-< i2 ∈ {0; 5}
-< i3 ∈ {0; 5}
-< i4 ∈ {0; 5}
-< i5 ∈ {0; 5}
-< v7 ∈ {0; 1}
----
-> NON TERMINATING FUNCTION
-221a217
-> [from] Non-terminating function main9 (no dependencies)
-223a220
-> [from] Non-terminating function main (no dependencies)
-271c268
-< NO EFFECTS
----
-> NON TERMINATING - NO EFFECTS
-273,277c270
-< i2 FROM i2
-< i3 FROM i3
-< i4 FROM i4
-< i5 FROM i5
-< v7 FROM v
----
-> NON TERMINATING - NO EFFECTS
diff --git a/tests/value/oracle_multidim/split_return.3.res.oracle b/tests/value/oracle_multidim/split_return.3.res.oracle
deleted file mode 100644
index c1fa14d7ea4..00000000000
--- a/tests/value/oracle_multidim/split_return.3.res.oracle
+++ /dev/null
@@ -1,29 +0,0 @@
-262,263c262
-< y ∈ {0} or UNINITIALIZED
-< q ∈ ESCAPINGADDR
----
-> NON TERMINATING FUNCTION
-265,269c264
-< i2 ∈ {0; 5}
-< i3 ∈ {0; 5}
-< i4 ∈ {0; 5}
-< i5 ∈ {0; 5}
-< v7 ∈ {0; 1}
----
-> NON TERMINATING FUNCTION
-306a302
-> [from] Non-terminating function main9 (no dependencies)
-308a305
-> [from] Non-terminating function main (no dependencies)
-356c353
-< NO EFFECTS
----
-> NON TERMINATING - NO EFFECTS
-358,362c355
-< i2 FROM i2
-< i3 FROM i3
-< i4 FROM i4
-< i5 FROM i5
-< v7 FROM v
----
-> NON TERMINATING - NO EFFECTS
diff --git a/tests/value/oracle_multidim/split_return.4.res.oracle b/tests/value/oracle_multidim/split_return.4.res.oracle
deleted file mode 100644
index a918abcbc4f..00000000000
--- a/tests/value/oracle_multidim/split_return.4.res.oracle
+++ /dev/null
@@ -1,58 +0,0 @@
-265,266c265
-< y ∈ {0} or UNINITIALIZED
-< q ∈ ESCAPINGADDR
----
-> NON TERMINATING FUNCTION
-268,272c267
-< i2 ∈ {0; 5}
-< i3 ∈ {0; 5}
-< i4 ∈ {0; 5}
-< i5 ∈ {0; 5}
-< v7 ∈ {0; 1}
----
-> NON TERMINATING FUNCTION
-309a305
-> [from] Non-terminating function main9 (no dependencies)
-311a308
-> [from] Non-terminating function main (no dependencies)
-359c356
-< NO EFFECTS
----
-> NON TERMINATING - NO EFFECTS
-361,365c358
-< i2 FROM i2
-< i3 FROM i3
-< i4 FROM i4
-< i5 FROM i5
-< v7 FROM v
----
-> NON TERMINATING - NO EFFECTS
-694,695c687
-< y ∈ {0} or UNINITIALIZED
-< q ∈ ESCAPINGADDR
----
-> NON TERMINATING FUNCTION
-697,701c689
-< i2 ∈ {0; 5}
-< i3 ∈ {0; 5}
-< i4 ∈ {0; 5}
-< i5 ∈ {0; 5}
-< v7 ∈ {0; 1}
----
-> NON TERMINATING FUNCTION
-738a727
-> [from] Non-terminating function main9 (no dependencies)
-740a730
-> [from] Non-terminating function main (no dependencies)
-788c778
-< NO EFFECTS
----
-> NON TERMINATING - NO EFFECTS
-790,794c780
-< i2 FROM i2
-< i3 FROM i3
-< i4 FROM i4
-< i5 FROM i5
-< v7 FROM v
----
-> NON TERMINATING - NO EFFECTS
--
GitLab