[Eva] Untaint left value only when the corresponding location is a singleton.

src/plugins/value/domains/taint_domain.ml

@@ -204,8 +204,8 @@ module TransferTaint = struct
         state
       | Kstmt stmt ->
         let to_loc = loc_of_lval valuation in
+        let ploc = to_loc lv.Eval.lval in
         let lv_zone =
-          let ploc = to_loc lv.Eval.lval in
           let loc = Precise_locs.imprecise_location ploc in
           Locations.enumerate_valid_bits Write loc
         in
@@ -249,7 +249,9 @@ module TransferTaint = struct
           in
           if intersect_state
           then { state with locs_data = Zone.join state.locs_data lv_zone }
-          else { state with locs_data = Zone.diff state.locs_data lv_zone }
+          else if Precise_locs.cardinal_zero_or_one ploc
+          then { state with locs_data = Zone.diff state.locs_data lv_zone }
+          else state
     in
     `Value state
 

tests/value/oracle/taint.res.oracle

@@ -7,7 +7,7 @@
   undet ∈ [--..--]
   tainted ∈ {0}
 [eva] computing for function taint_basic <- main.
-  Called from tests/value/taint.c:131.
+  Called from tests/value/taint.c:143.
 [eva] tests/value/taint.c:34: 
   Frama_C_dump_each:
   # taint:
@@ -19,7 +19,7 @@
 [eva] Recording results for taint_basic
 [eva] Done for function taint_basic
 [eva] computing for function taint_assume_1 <- main.
-  Called from tests/value/taint.c:134.
+  Called from tests/value/taint.c:146.
 [eva:loop-unroll] tests/value/taint.c:47: Automatic loop unrolling.
 [eva] tests/value/taint.c:48: 
   Frama_C_dump_each:
@@ -80,7 +80,7 @@
 [eva] Recording results for taint_assume_1
 [eva] Done for function taint_assume_1
 [eva] computing for function taint_assume_2 <- main.
-  Called from tests/value/taint.c:135.
+  Called from tests/value/taint.c:147.
 [eva] tests/value/taint.c:76: 
   Frama_C_dump_each:
   # taint:
@@ -91,16 +91,28 @@
   ==END OF DUMP==
 [eva] Recording results for taint_assume_2
 [eva] Done for function taint_assume_2
+[eva] computing for function taint_undet_locs <- main.
+  Called from tests/value/taint.c:149.
+[eva] tests/value/taint.c:88: 
+  Frama_C_dump_each:
+  # taint:
+  Locations (data):
+    x; y; t
+  Locations (control):
+    \nothing
+  ==END OF DUMP==
+[eva] Recording results for taint_undet_locs
+[eva] Done for function taint_undet_locs
 [eva] computing for function taint_spec_assigns <- main.
-  Called from tests/value/taint.c:138.
+  Called from tests/value/taint.c:152.
 [eva] using specification for function taint_spec_assigns
 [eva] Done for function taint_spec_assigns
-[eva] tests/value/taint.c:140: 
+[eva] tests/value/taint.c:154: 
   Frama_C_domain_show_each:
   l : # taint: false
 [eva] computing for function taint_goto_1 <- main.
-  Called from tests/value/taint.c:142.
-[eva] tests/value/taint.c:95: 
+  Called from tests/value/taint.c:156.
+[eva] tests/value/taint.c:107: 
   Frama_C_dump_each:
   # taint:
   Locations (data):
@@ -111,8 +123,8 @@
 [eva] Recording results for taint_goto_1
 [eva] Done for function taint_goto_1
 [eva] computing for function taint_goto_2 <- main.
-  Called from tests/value/taint.c:143.
-[eva] tests/value/taint.c:115: 
+  Called from tests/value/taint.c:157.
+[eva] tests/value/taint.c:127: 
   Frama_C_dump_each:
   # taint:
   Locations (data):
@@ -123,9 +135,9 @@
 [eva] Recording results for taint_goto_2
 [eva] Done for function taint_goto_2
 [eva] computing for function taint_call <- main.
-  Called from tests/value/taint.c:146.
+  Called from tests/value/taint.c:160.
 [eva] computing for function taint_basic <- taint_call <- main.
-  Called from tests/value/taint.c:123.
+  Called from tests/value/taint.c:135.
 [eva] tests/value/taint.c:34: 
   Frama_C_dump_each:
   # taint:
@@ -136,7 +148,7 @@
   ==END OF DUMP==
 [eva] Recording results for taint_basic
 [eva] Done for function taint_basic
-[eva] tests/value/taint.c:126: 
+[eva] tests/value/taint.c:138: 
   Frama_C_domain_show_each:
   x : # taint: false
 [eva] Recording results for taint_call
@@ -170,6 +182,11 @@
   y ∈ {0} or UNINITIALIZED
   z ∈ {1} or UNINITIALIZED
   t ∈ [--..--]
+[eva:final-states] Values at end of function taint_undet_locs:
+  x ∈ {0}
+  y ∈ {0}
+  t ∈ {0}
+  p ∈ {{ &x ; &y }}
 [eva:final-states] Values at end of function main:
   tainted ∈ {0}
   l ∈ [--..--] or UNINITIALIZED
@@ -186,6 +203,8 @@
 [from] Done for function taint_goto_1
 [from] Computing for function taint_goto_2
 [from] Done for function taint_goto_2
+[from] Computing for function taint_undet_locs
+[from] Done for function taint_undet_locs
 [from] Computing for function main
 [from] Computing for function taint_spec_assigns <-main
 [from] Done for function taint_spec_assigns
@@ -206,6 +225,8 @@
   NO EFFECTS
 [from] Function taint_spec_assigns:
   l FROM t
+[from] Function taint_undet_locs:
+  NO EFFECTS
 [from] Function main:
   tainted FROM \nothing
   \result FROM \nothing
@@ -234,6 +255,10 @@
     x; y; z; t
 [inout] Inputs for function taint_goto_2:
     undet
+[inout] Out (internal) for function taint_undet_locs:
+    x; y; t; p; tmp
+[inout] Inputs for function taint_undet_locs:
+    undet
 [inout] Out (internal) for function main:
     tainted; l; __retres
 [inout] Inputs for function main:

tests/value/taint.c

@@ -76,6 +76,18 @@ void taint_assume_2() {
   Frama_C_dump_each();
 }
 
+void taint_undet_locs() {
+  int x, y, t = 0;
+  int *p = undet ? &x : &y;
+  //@ taint t;
+  x = t;
+  y = t;
+  /* Since 'p' may point to either 'x' or 'y', this assignment does not untaint
+     'x' nor 'y' (which must both remain data-tainted). */
+  *p = 0;
+  Frama_C_dump_each();
+}
+
 /*@ assigns *l \from t; */
 void taint_spec_assigns(int* l, int t);
 
@@ -134,6 +146,8 @@ int main(void) {
   taint_assume_1();
   taint_assume_2();
 
+  taint_undet_locs();
+
   int l;
   taint_spec_assigns(&l, tainted);
   /* Here 'l' must be tainted. */