From 6eb8f07e9f8c98bdcc87b796622b92956b2f51ff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 9 Oct 2024 10:18:39 +0200
Subject: [PATCH] [Eva] In offsetmap, do not use V.bottom in
 [update_imprecise_everywhere].

---
 .../abstract_interp/offsetmap.ml              |  26 +-
 .../oracle_bitwise/allocated.0.res.oracle     |   4 -
 .../oracle_bitwise/allocated.1.res.oracle     | 222 ------------------
 .../malloc-optimistic.res.oracle              |   4 -
 4 files changed, 8 insertions(+), 248 deletions(-)

diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 60d836c7675..2c3099a0fe1 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -1738,11 +1738,11 @@ module Make
       topification of [v]. The parameter [validity] is respected, and so is the
       current size of [offsm]: each interval already present in [offsm] and valid
       is overwritten. Interval already present but not valid are bound to
-      [V.bottom]. *)
-  (* TODO: the convention to write bottom on non-valid locations is strange,
-     and only useful for the NULL base in Lmap.ml. It would be simpler an more
-     elegant to keep the existing value on non-valid ranges instead. This
-     function should also be written as a call to fold_between *)
+      [V.bottom].
+      This function used to write bottom on non-valid locations, but this was
+      unnecessary as values on non-valid locations should never be accessed
+      anyway. *)
+  (* TODO: this function should also be written as a call to fold_between *)
   let update_imprecise_everywhere ~validity o v offsm =
     let v = V.topify_with_origin o v in
     if Base.Validity.equal validity Base.Invalid then
@@ -1750,23 +1750,13 @@ module Make
     else
       let clip = clip_by_validity validity in
       let r = fold
-          (fun (min, max as itv) (bound_v, _, _) acc ->
+          (fun itv (bound_v, _, _) acc ->
              let new_v = V.topify_with_origin o (V.join bound_v v) in
              let new_min, new_max = clip itv in
              if new_min <=~ new_max then (* [min..max] and validity intersect *)
-               let acc =
-                 if min <~ new_min (* Before validity *)
-                 then append_basic_itv ~min ~max:(pred new_min) ~v:V.bottom acc
-                 else acc
-               in
-               let acc = append_basic_itv ~min:new_min ~max:new_max ~v:new_v acc in
-               let acc =
-                 if new_max <~ max (* After validity *)
-                 then append_basic_itv ~min:(succ new_max) ~max ~v:V.bottom acc
-                 else acc
-               in acc
+               append_basic_itv ~min:new_min ~max:new_max ~v:new_v acc
              else
-               append_basic_itv ~min ~max ~v:V.bottom acc
+              acc
           ) offsm m_empty
       in
       `Value r
diff --git a/tests/builtins/oracle_bitwise/allocated.0.res.oracle b/tests/builtins/oracle_bitwise/allocated.0.res.oracle
index 6b235da53df..e69de29bb2d 100644
--- a/tests/builtins/oracle_bitwise/allocated.0.res.oracle
+++ b/tests/builtins/oracle_bitwise/allocated.0.res.oracle
@@ -1,4 +0,0 @@
-200a201,203
-> [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-> [eva:malloc] allocated.c:127: 
->   resizing variable `__malloc_main_l127' (0..31/319) to fit 0..63/319
diff --git a/tests/builtins/oracle_bitwise/allocated.1.res.oracle b/tests/builtins/oracle_bitwise/allocated.1.res.oracle
index 07f6b70bfde..e69de29bb2d 100644
--- a/tests/builtins/oracle_bitwise/allocated.1.res.oracle
+++ b/tests/builtins/oracle_bitwise/allocated.1.res.oracle
@@ -1,222 +0,0 @@
-135a136,137
-> [eva] allocated.c:82: Call to builtin malloc
-> [eva] allocated.c:82: allocating variable __malloc_main_l82_7
-146a149,150
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
-> [eva] allocated.c:87: Call to builtin free
-156a161,162
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
-> [eva] allocated.c:87: Call to builtin free
-166a173,174
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
-> [eva] allocated.c:87: Call to builtin free
-176,177c184,185
-< [eva] allocated.c:82: Call to builtin malloc
-< [eva] allocated.c:82: allocating variable __malloc_main_l82_7
----
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
-223a232,245
-> [eva] allocated.c:82: Call to builtin malloc
-> [eva] allocated.c:82: allocating variable __malloc_main_l82_31
-> [eva] allocated.c:82: Call to builtin malloc
-> [eva] allocated.c:82: allocating variable __malloc_main_l82_32
-> [eva] allocated.c:82: Call to builtin malloc
-> [eva] allocated.c:82: allocating variable __malloc_main_l82_33
-> [eva] allocated.c:82: Call to builtin malloc
-> [eva] allocated.c:82: allocating variable __malloc_main_l82_34
-> [eva] allocated.c:82: Call to builtin malloc
-> [eva] allocated.c:82: allocating variable __malloc_main_l82_35
-> [eva] allocated.c:82: Call to builtin malloc
-> [eva] allocated.c:82: allocating variable __malloc_main_l82_36
-> [eva] allocated.c:82: Call to builtin malloc
-> [eva] allocated.c:82: allocating variable __malloc_main_l82_37
-226d247
-< [eva] allocated.c:84: Trace partitioning superposing up to 300 states
-228a250,263
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_37}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_36}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_35}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_34}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_33}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_32}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_31}
-> [eva] allocated.c:87: Call to builtin free
-275c310,322
-< [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
----
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_37}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_36}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_35}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_34}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_33}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_32}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_31}
-323c370,382
-< [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
----
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_37}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_36}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_35}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_34}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_33}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_32}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_31}
-371c430,442
-< [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
----
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_37}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_36}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_35}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_34}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_33}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_32}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_31}
-419c490,502
-< [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
----
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_37}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_36}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_35}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_34}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_33}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_32}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_31}
-467c550,562
-< [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
----
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_37}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_36}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_35}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_34}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_33}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_32}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_31}
-515c610,622
-< [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
----
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_37}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_36}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_35}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_34}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_33}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_32}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_31}
-563c670,682
-< [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
----
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_37}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_36}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_35}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_34}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_33}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_32}
-> [eva] allocated.c:87: Call to builtin free
-> [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_31}
-610,611c729
-< [eva] allocated.c:87: Call to builtin free
-< [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
----
-> [eva] allocated.c:81: Trace partitioning superposing up to 500 states
-721,723c839,840
-<   __malloc_main_l82_7[0] ∈ {21} or UNINITIALIZED
-<                      [1] ∈ {24} or UNINITIALIZED
-<                      [2] ∈ {27} or UNINITIALIZED
----
->   __malloc_main_l82_7[0] ∈ {14} or UNINITIALIZED
->                      [1] ∈ {17} or UNINITIALIZED
-792a910,930
->   __malloc_main_l82_31[0] ∈ {21} or UNINITIALIZED
->                       [1] ∈ {24} or UNINITIALIZED
->                       [2] ∈ {27} or UNINITIALIZED
->   __malloc_main_l82_32[0] ∈ {21} or UNINITIALIZED
->                       [1] ∈ {24} or UNINITIALIZED
->                       [2] ∈ {27} or UNINITIALIZED
->   __malloc_main_l82_33[0] ∈ {21} or UNINITIALIZED
->                       [1] ∈ {24} or UNINITIALIZED
->                       [2] ∈ {27} or UNINITIALIZED
->   __malloc_main_l82_34[0] ∈ {21} or UNINITIALIZED
->                       [1] ∈ {24} or UNINITIALIZED
->                       [2] ∈ {27} or UNINITIALIZED
->   __malloc_main_l82_35[0] ∈ {21} or UNINITIALIZED
->                       [1] ∈ {24} or UNINITIALIZED
->                       [2] ∈ {27} or UNINITIALIZED
->   __malloc_main_l82_36[0] ∈ {21} or UNINITIALIZED
->                       [1] ∈ {24} or UNINITIALIZED
->                       [2] ∈ {27} or UNINITIALIZED
->   __malloc_main_l82_37[0] ∈ {21} or UNINITIALIZED
->                       [1] ∈ {24} or UNINITIALIZED
->                       [2] ∈ {27} or UNINITIALIZED
-836c974
-<   __malloc_main_l82_7[0..2] FROM __fc_heap_status; nondet (and SELF)
----
->   __malloc_main_l82_7[0..1] FROM __fc_heap_status; nondet (and SELF)
-859a998,1004
->   __malloc_main_l82_31[0..2] FROM __fc_heap_status; nondet (and SELF)
->   __malloc_main_l82_32[0..2] FROM __fc_heap_status; nondet (and SELF)
->   __malloc_main_l82_33[0..2] FROM __fc_heap_status; nondet (and SELF)
->   __malloc_main_l82_34[0..2] FROM __fc_heap_status; nondet (and SELF)
->   __malloc_main_l82_35[0..2] FROM __fc_heap_status; nondet (and SELF)
->   __malloc_main_l82_36[0..2] FROM __fc_heap_status; nondet (and SELF)
->   __malloc_main_l82_37[0..2] FROM __fc_heap_status; nondet (and SELF)
-883c1028
-<     __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..2];
----
->     __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..1];
-895,896c1040,1045
-<     __malloc_main_l82_30[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
-<     __malloc_main_l127; __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
----
->     __malloc_main_l82_30[0..2]; __malloc_main_l82_31[0..2];
->     __malloc_main_l82_32[0..2]; __malloc_main_l82_33[0..2];
->     __malloc_main_l82_34[0..2]; __malloc_main_l82_35[0..2];
->     __malloc_main_l82_36[0..2]; __malloc_main_l82_37[0..2];
->     __malloc_main_l97[0]; __malloc_main_l114[0..3]; __malloc_main_l127;
->     __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
diff --git a/tests/builtins/oracle_bitwise/malloc-optimistic.res.oracle b/tests/builtins/oracle_bitwise/malloc-optimistic.res.oracle
index e9b2cc9aa18..e69de29bb2d 100644
--- a/tests/builtins/oracle_bitwise/malloc-optimistic.res.oracle
+++ b/tests/builtins/oracle_bitwise/malloc-optimistic.res.oracle
@@ -1,4 +0,0 @@
-1872a1873,1875
-> [eva] malloc-optimistic.c:90: Call to builtin malloc
-> [eva:malloc] malloc-optimistic.c:90: 
->   resizing variable `__malloc_main7_l90' (0..31/3231) to fit 0..511/3231
-- 
GitLab