[Eva] Fixes summary of garbled mix origins at the end of an analysis.

Prints the number of statements at which a garbled mix from a given origin has been read and propagated, instead of the total number of times such a garbled mix has been read/propagated. This is more stable and depends less on states partitioning.

[Eva] Fixes summary of garbled mix origins at the end of an analysis.
Prints the number of statements at which a garbled mix from a given origin has been read and propagated, instead of the total number of times such a garbled mix has been read/propagated. This is more stable and depends less on states partitioning.
711c8fc6 · David Bühler · 8e0b87cf · 711c8fc6 · 711c8fc6 · 711c8fc6
Commit 711c8fc6 authored 1 year ago by David Bühler
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -41,6 +41,10 @@ let kind_label = function
  | Merge -> "Merge"
  | Arith -> "Arithmetic"

+(* Ideally, we would use the current statement sid instead of the current
+   source file location. However, that would require passing the current
+   statement through any datastructures and operations that can create
+   garbled mixes, which would be an invasive change. *)
 type location = Cil_datatype.Location.t

 type tt =
@@ -139,9 +143,10 @@ module History_Info = struct
  let size = 32
 end

-(* Number of writes, number of reads, related bases. *)
-module History_Data =
-  Datatype.Triple (Datatype.Int) (Datatype.Int) (Base.SetLattice)
+module LocSet = Cil_datatype.Location.Set
+
+(* Locations of writes, locations of reads, related bases. *)
+module History_Data = Datatype.Triple (LocSet) (LocSet) (Base.SetLattice)
 module History = State_builder.Hashtbl (Hashtbl) (History_Data) (History_Info)

 let clear () = Id.reset (); History.clear ()
@@ -154,21 +159,35 @@ let is_current = function
   current location. *)
 let register_write bases t =
  if is_unknown t then false else
-    let change (w, r, b) = w+1, r, Base.SetLattice.join b bases in
-    let count, _, _ = History.memo ~change (fun _ -> 1, 0, bases) t in
-    count < 2 && is_current t
+    let current_loc = Cil.CurrentLoc.get () in
+    let is_new = not (History.mem t) in
+    let change (w, r, b) =
+      LocSet.add current_loc w, r, Base.SetLattice.join b bases
+    in
+    let create _ = LocSet.singleton current_loc, LocSet.empty, bases in
+    ignore (History.memo ~change create t);
+    is_new && is_current t

 (* Registers a read only if the current location is not that of the origin. *)
 let register_read bases t =
  if not (is_unknown t || is_current t) then
-    let change (w, r, b) = w, r+1, Base.SetLattice.join b bases in
-    ignore (History.memo ~change (fun _ -> 0, 1, bases) t)
+    let current_loc = Cil.CurrentLoc.get () in
+    let change (w, r, b) =
+      w, LocSet.add current_loc r, Base.SetLattice.join b bases
+    in
+    let create _ = LocSet.empty, LocSet.singleton current_loc, bases in
+    ignore (History.memo ~change create t)

 (* Returns the list of recorded origins, sorted by number of reads.
   Origins with no reads are filtered. *)
 let get_history () =
  let list = List.of_seq (History.to_seq ()) in
-  let list = List.filter (fun (_origin, (_, r, _)) -> r > 0) list in
+  let count (origin, (w, r, bases)) =
+    if LocSet.is_empty r
+    then None
+    else Some (origin, (LocSet.cardinal w, LocSet.cardinal r, bases))
+  in
+  let list = List.filter_map count list in
  let cmp (origin1, (_, r1, _)) (origin2, (_, r2, _)) =
    let r = r2 - r1 in
    if r <> 0 then r else compare origin1 origin2
@@ -185,12 +204,13 @@ let pretty_origin fmt origin =

 let pretty_history fmt =
  let list = get_history () in
+  let plural count = if count = 1 then "" else "s" in
  let pp_origin fmt (origin, (w, r, bases)) =
    let bases = Base.SetLattice.filter (fun b -> not (Base.is_null b)) bases in
    Format.fprintf fmt
-      "@[<hov 2>%a@ (read %i times, propagated %i times)@ \
+      "@[<hov 2>%a@ (read in %i statement%s, propagated through %i statement%s)@ \
       garbled mix of &%a@]"
-      pretty_origin origin r w Base.SetLattice.pretty bases
+      pretty_origin origin r (plural r) w (plural w) Base.SetLattice.pretty bases
  in
  if list <> [] then
    Format.fprintf fmt

--- a/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
+++ b/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
@@ -16,7 +16,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    exceptional.i:5: arithmetic operation on addresses
-      (read 3 times, propagated 3 times) garbled mix of &{i}
+      (read in 2 statements, propagated through 2 statements)
+      garbled mix of &{i}
 [eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  2 functions analyzed (out of 2): 100% coverage.

--- a/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
@@ -25,7 +25,7 @@
                   (tmp from vararg)
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
-    Initial state (read 12 times, propagated 6 times)
+    Initial state (read in 3 statements, propagated through 3 statements)
      garbled mix of &{S_0_S___va_params; S_1_S___va_params}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function sum:

--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -29,7 +29,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    printf_garbled_mix.c:6: arithmetic operation on addresses
-      (read 2 times, propagated 3 times) garbled mix of &{a}
+      (read in 1 statement, propagated through 2 statements)
+      garbled mix of &{a}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
  a[0] ∈ {1}

--- a/tests/builtins/oracle/alloc.0.res.oracle
+++ b/tests/builtins/oracle/alloc.0.res.oracle
@@ -67,7 +67,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    alloc.c:26: arithmetic operation on addresses
-      (read 3 times, propagated 1 times) garbled mix of &{__malloc_main_l25}
+      (read in 1 statement, propagated through 1 statement)
+      garbled mix of &{__malloc_main_l25}
 [eva] alloc.c:18: assertion 'Eva,mem_access' got final status invalid.
 [eva] alloc.c:19: assertion 'Eva,mem_access' got final status invalid.
 [eva] alloc.c:20: assertion 'Eva,mem_access' got final status invalid.

--- a/tests/builtins/oracle/alloc.1.res.oracle
+++ b/tests/builtins/oracle/alloc.1.res.oracle
@@ -33,7 +33,7 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    alloc.c:51: arithmetic operation on addresses
-      (read 2 times, propagated 1 times)
+      (read in 1 statement, propagated through 1 statement)
      garbled mix of &{__malloc_main_abs_l50}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main_abs:

--- a/tests/builtins/oracle/imprecise-malloc-free.res.oracle
+++ b/tests/builtins/oracle/imprecise-malloc-free.res.oracle
@@ -67,7 +67,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    imprecise-malloc-free.c:13: arithmetic operation on addresses
-      (read 1 times, propagated 2 times) garbled mix of &{size2}
+      (read in 1 statement, propagated through 2 statements)
+      garbled mix of &{size2}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
  __fc_heap_status ∈ [--..--]

--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -267,7 +267,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    imprecise.c:19: arithmetic operation on addresses
-      (read 3 times, propagated 1 times) garbled mix of &{j; k}
+      (read in 1 statement, propagated through 1 statement)
+      garbled mix of &{j; k}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function cast_address:
  p ∈ {{ &x }}
@@ -815,7 +816,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    imprecise.c:19: arithmetic operation on addresses
-      (read 3 times, propagated 1 times) garbled mix of &{j; k}
+      (read in 1 statement, propagated through 1 statement)
+      garbled mix of &{j; k}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function cast_address:
  p ∈ {{ &x }}

--- a/tests/builtins/oracle/strchr.res.oracle
+++ b/tests/builtins/oracle/strchr.res.oracle
@@ -675,7 +675,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    strchr.c:541: arithmetic operation on addresses
-      (read 1 times, propagated 3 times) garbled mix of &{x}
+      (read in 1 statement, propagated through 2 statements)
+      garbled mix of &{x}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function init_array_nondet:
  from ∈ {-1}

--- a/tests/float/oracle/nonlin.0.res.oracle
+++ b/tests/float/oracle/nonlin.0.res.oracle
@@ -287,7 +287,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    nonlin.c:98: arithmetic operation on addresses
-      (read 1 times, propagated 2 times) garbled mix of &{x_0}
+      (read in 1 statement, propagated through 2 statements)
+      garbled mix of &{x_0}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function access_bits:
  rbits1 ∈ {0; 1; 2}

--- a/tests/float/oracle/nonlin.1.res.oracle
+++ b/tests/float/oracle/nonlin.1.res.oracle
@@ -314,7 +314,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    nonlin.c:98: arithmetic operation on addresses
-      (read 1 times, propagated 2 times) garbled mix of &{x_0}
+      (read in 1 statement, propagated through 2 statements)
+      garbled mix of &{x_0}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function access_bits:
  rbits1 ∈ {0; 1; 2}

--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -288,7 +288,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    nonlin.c:98: arithmetic operation on addresses
-      (read 1 times, propagated 2 times) garbled mix of &{x_0}
+      (read in 1 statement, propagated through 2 statements)
+      garbled mix of &{x_0}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function access_bits:
  rbits1 ∈ {0; 1; 2}

--- a/tests/float/oracle/nonlin.3.res.oracle
+++ b/tests/float/oracle/nonlin.3.res.oracle
@@ -287,7 +287,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    nonlin.c:98: arithmetic operation on addresses
-      (read 1 times, propagated 2 times) garbled mix of &{x_0}
+      (read in 1 statement, propagated through 2 statements)
+      garbled mix of &{x_0}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function access_bits:
  rbits1 ∈ {0; 1; 2}

--- a/tests/float/oracle/nonlin.4.res.oracle
+++ b/tests/float/oracle/nonlin.4.res.oracle
@@ -314,7 +314,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    nonlin.c:98: arithmetic operation on addresses
-      (read 1 times, propagated 2 times) garbled mix of &{x_0}
+      (read in 1 statement, propagated through 2 statements)
+      garbled mix of &{x_0}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function access_bits:
  rbits1 ∈ {0; 1; 2}

--- a/tests/float/oracle/nonlin.5.res.oracle
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -288,7 +288,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    nonlin.c:98: arithmetic operation on addresses
-      (read 1 times, propagated 2 times) garbled mix of &{x_0}
+      (read in 1 statement, propagated through 2 statements)
+      garbled mix of &{x_0}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function access_bits:
  rbits1 ∈ {0; 1; 2}

--- a/tests/libc/oracle/spawn_h.res.oracle
+++ b/tests/libc/oracle/spawn_h.res.oracle
@@ -255,7 +255,7 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    spawn_h.c:36: assigns clause on addresses
-      (read 20 times, propagated 13 times)
+      (read in 3 statements, propagated through 2 statements)
      garbled mix of &{S_argv; S_0_S_argv; S_1_S_argv}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:

--- a/tests/value/oracle/arith_pointer.res.oracle
+++ b/tests/value/oracle/arith_pointer.res.oracle
@@ -45,7 +45,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    arith_pointer.c:54: arithmetic operation on addresses
-      (read 2 times, propagated 2 times) garbled mix of &{x}
+      (read in 2 statements, propagated through 2 statements)
+      garbled mix of &{x}
 [eva] arith_pointer.c:30: 
  assertion 'Eva,differing_blocks' got final status invalid.
 [eva] ====== VALUES COMPUTED ======
@@ -158,13 +159,17 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    arith_pointer.c:54: arithmetic operation on addresses
-      (read 2 times, propagated 2 times) garbled mix of &{x}
+      (read in 2 statements, propagated through 2 statements)
+      garbled mix of &{x}
    arith_pointer.c:30: arithmetic operation on addresses
-      (read 1 times, propagated 1 times) garbled mix of &{x; y}
+      (read in 1 statement, propagated through 1 statement)
+      garbled mix of &{x; y}
    arith_pointer.c:49: arithmetic operation on addresses
-      (read 1 times, propagated 1 times) garbled mix of &{x; y}
+      (read in 1 statement, propagated through 1 statement)
+      garbled mix of &{x; y}
    arith_pointer.c:51: arithmetic operation on addresses
-      (read 1 times, propagated 1 times) garbled mix of &{x; y}
+      (read in 1 statement, propagated through 1 statement)
+      garbled mix of &{x; y}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main1:
  t[0..1] ∈ {-3}

--- a/tests/value/oracle/backward_add_ptr.res.oracle
+++ b/tests/value/oracle/backward_add_ptr.res.oracle
@@ -151,7 +151,8 @@
 [eva:garbled-mix:summary] Warning: 
  Origins of garbled mix generated during analysis:
    backward_add_ptr.c:68: arithmetic operation on addresses
-      (read 81 times, propagated 20 times) garbled mix of &{a; b; a; b; c}
+      (read in 30 statements, propagated through 11 statements)
+      garbled mix of &{a; b; a; b; c}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function gm:
  __retres ∈

--- a/tests/value/oracle/behaviors1.res.oracle
+++ b/tests/value/oracle/behaviors1.res.oracle
@@ -449,9 +449,11 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    behaviors1.i:473: assigns clause on addresses
-      (read 1 times, propagated 3 times) garbled mix of &{a}
+      (read in 1 statement, propagated through 2 statements)
+      garbled mix of &{a}
    behaviors1.i:474: assigns clause on addresses
-      (read 1 times, propagated 3 times) garbled mix of &{b}
+      (read in 1 statement, propagated through 2 statements)
+      garbled mix of &{b}
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function test_123_comp_2345_comp_disj:
  a ∈ [--..--]

--- a/tests/value/oracle/bitfield.res.oracle
+++ b/tests/value/oracle/bitfield.res.oracle
@@ -210,7 +210,8 @@
 [eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    bitfield.i:70: misaligned read of addresses
-      (read 5 times, propagated 7 times) garbled mix of &{b; ee}
+      (read in 2 statements, propagated through 2 statements)
+      garbled mix of &{b; ee}
 [eva] bitfield.i:102: assertion 'Eva,initialization' got final status invalid.
 [scope:rm_asserts] removing 1 assertion(s)
 [eva] ====== VALUES COMPUTED ======