From 925e600e9153975d21be8b9c2941e348c7debc74 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 7 Aug 2024 15:18:12 +0200
Subject: [PATCH] [Eva] Adds a test for the \tainted predicate.

---
 tests/value/oracle/taint.res.oracle         | 69 +++++++++++++++------
 tests/value/oracle_apron/taint.res.oracle   | 28 ++++++---
 tests/value/oracle_octagon/taint.res.oracle |  6 +-
 tests/value/taint.c                         | 20 ++++++
 4 files changed, 92 insertions(+), 31 deletions(-)

diff --git a/tests/value/oracle/taint.res.oracle b/tests/value/oracle/taint.res.oracle
index 6d7c072866f..ef918aac811 100644
--- a/tests/value/oracle/taint.res.oracle
+++ b/tests/value/oracle/taint.res.oracle
@@ -7,17 +7,17 @@
   undet ∈ [--..--]
   tainted ∈ {0}
 [eva] computing for function taints <- main.
-  Called from taint.c:175.
+  Called from taint.c:192.
 [eva] computing for function Frama_C_interval <- taints <- main.
-  Called from taint.c:170.
+  Called from taint.c:187.
 [eva] using specification for function Frama_C_interval
-[eva] taint.c:170: 
+[eva] taint.c:187: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] Recording results for taints
 [eva] Done for function taints
 [eva] computing for function taint_basic <- main.
-  Called from taint.c:176.
+  Called from taint.c:193.
 [eva:alarm] taint.c:33: Warning: accessing out of bounds index. assert t < 2;
 [eva] taint.c:35: 
   Frama_C_dump_each:
@@ -30,7 +30,7 @@
 [eva] Recording results for taint_basic
 [eva] Done for function taint_basic
 [eva] computing for function taint_assume_1 <- main.
-  Called from taint.c:179.
+  Called from taint.c:196.
 [eva:loop-unroll:auto] taint.c:49: Automatic loop unrolling.
 [eva] taint.c:50: 
   Frama_C_dump_each:
@@ -91,7 +91,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 taint.c:180.
+  Called from taint.c:197.
 [eva] taint.c:79: 
   Frama_C_dump_each:
   # taint:
@@ -103,7 +103,7 @@
 [eva] Recording results for taint_assume_2
 [eva] Done for function taint_assume_2
 [eva] computing for function taint_undet_locs <- main.
-  Called from taint.c:182.
+  Called from taint.c:199.
 [eva] taint.c:91: 
   Frama_C_dump_each:
   # taint:
@@ -114,16 +114,16 @@
   ==END OF DUMP==
 [eva] Recording results for taint_undet_locs
 [eva] Done for function taint_undet_locs
-[eva] taint.c:185: Reusing old results for call to taints
+[eva] taint.c:202: Reusing old results for call to taints
 [eva] computing for function taint_spec_assigns <- main.
-  Called from taint.c:186.
+  Called from taint.c:203.
 [eva] using specification for function taint_spec_assigns
 [eva] Done for function taint_spec_assigns
-[eva] taint.c:188: 
+[eva] taint.c:205: 
   Frama_C_domain_show_each:
   l : # taint: true
 [eva] computing for function taint_goto_1 <- main.
-  Called from taint.c:191.
+  Called from taint.c:208.
 [eva] taint.c:110: 
   Frama_C_dump_each:
   # taint:
@@ -135,7 +135,7 @@
 [eva] Recording results for taint_goto_1
 [eva] Done for function taint_goto_1
 [eva] computing for function taint_goto_2 <- main.
-  Called from taint.c:192.
+  Called from taint.c:209.
 [eva] taint.c:130: 
   Frama_C_dump_each:
   # taint:
@@ -146,9 +146,9 @@
   ==END OF DUMP==
 [eva] Recording results for taint_goto_2
 [eva] Done for function taint_goto_2
-[eva] taint.c:194: Reusing old results for call to taints
+[eva] taint.c:211: Reusing old results for call to taints
 [eva] computing for function taint_call <- main.
-  Called from taint.c:195.
+  Called from taint.c:212.
 [eva] computing for function taint_basic <- taint_call <- main.
   Called from taint.c:138.
 [eva] taint.c:35: 
@@ -166,9 +166,9 @@
   x : # taint: false
 [eva] Recording results for taint_call
 [eva] Done for function taint_call
-[eva] taint.c:197: Reusing old results for call to taints
+[eva] taint.c:214: Reusing old results for call to taints
 [eva] computing for function taint_infinite_while <- main.
-  Called from taint.c:198.
+  Called from taint.c:215.
 [eva:loop-unroll:auto] taint.c:157: Automatic loop unrolling.
 [eva:loop-unroll:partial] taint.c:157: loop not completely unrolled
 [eva] taint.c:157: starting to merge loop iterations
@@ -183,8 +183,26 @@
   ==END OF DUMP==
 [eva] Recording results for taint_infinite_while
 [eva] Done for function taint_infinite_while
+[eva] taint.c:217: Reusing old results for call to taints
+[eva] computing for function tainted_predicate <- main.
+  Called from taint.c:218.
+[eva] computing for function Frama_C_interval <- tainted_predicate <- main.
+  Called from taint.c:170.
+[eva] taint.c:170: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:alarm] taint.c:176: Warning: check 'true' got status unknown.
+[eva:alarm] taint.c:177: Warning: check 'false' got status unknown.
+[eva:alarm] taint.c:178: Warning: check 'false' got status invalid.
+[eva] taint.c:179: check 'true' got status valid.
+[eva:alarm] taint.c:180: Warning: assertion 'unknown' got status unknown.
+[eva] taint.c:181: check 'true' got status valid.
+[eva:alarm] taint.c:182: Warning: check got status invalid.
+[eva] Recording results for tainted_predicate
+[eva] Done for function tainted_predicate
 [eva] Recording results for main
 [eva] Done for function main
+[scope:rm_asserts] removing 1 assertion(s)
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function taint_assume_1:
   x ∈ {3}
@@ -222,12 +240,17 @@
   y ∈ {0}
   t ∈ {0}
   p ∈ {{ &x ; &y }}
+[eva:final-states] Values at end of function tainted_predicate:
+  Frama_C_entropy_source ∈ [--..--]
+  not_tainted ∈ [0..20]
+  x ∈ [0..20]
+  indirect ∈ {0; 1}
 [eva:final-states] Values at end of function taints:
   Frama_C_entropy_source ∈ [--..--]
   tainted ∈ [0..10]
 [eva:final-states] Values at end of function main:
   Frama_C_entropy_source ∈ [--..--]
-  tainted ∈ {2; 4; 6; 8; 10}
+  tainted ∈ [0..10]
   l ∈ {0}
   __retres ∈ {0}
 [from] Computing for function taint_assume_1
@@ -246,9 +269,11 @@
 [from] Done for function taint_infinite_while
 [from] Computing for function taint_undet_locs
 [from] Done for function taint_undet_locs
-[from] Computing for function taints
-[from] Computing for function Frama_C_interval <-taints
+[from] Computing for function tainted_predicate
+[from] Computing for function Frama_C_interval <-tainted_predicate
 [from] Done for function Frama_C_interval
+[from] Done for function tainted_predicate
+[from] Computing for function taints
 [from] Done for function taints
 [from] Computing for function main
 [from] Computing for function taint_spec_assigns <-main
@@ -277,6 +302,8 @@
   l FROM t
 [from] Function taint_undet_locs:
   NO EFFECTS
+[from] Function tainted_predicate:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
 [from] Function taints:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
   tainted FROM Frama_C_entropy_source
@@ -317,6 +344,10 @@
     x; y; t; p; tmp
 [inout] Inputs for function taint_undet_locs:
     undet
+[inout] Out (internal) for function tainted_predicate:
+    Frama_C_entropy_source; not_tainted; x; tmp_0; indirect
+[inout] Inputs for function tainted_predicate:
+    Frama_C_entropy_source; undet; tainted
 [inout] Out (internal) for function taints:
     Frama_C_entropy_source; tainted
 [inout] Inputs for function taints:
diff --git a/tests/value/oracle_apron/taint.res.oracle b/tests/value/oracle_apron/taint.res.oracle
index 8178e772b18..0349e08a442 100644
--- a/tests/value/oracle_apron/taint.res.oracle
+++ b/tests/value/oracle_apron/taint.res.oracle
@@ -1,35 +1,45 @@
 2d1
 < [eva:experimental] Warning: The taint domain is experimental.
 117c116,122
-< [eva] taint.c:185: Reusing old results for call to taints
+< [eva] taint.c:202: Reusing old results for call to taints
 ---
 > [eva] computing for function taints <- main.
->   Called from taint.c:185.
+>   Called from taint.c:202.
 > [eva] computing for function Frama_C_interval <- taints <- main.
->   Called from taint.c:170.
+>   Called from taint.c:187.
 > [eva] Done for function Frama_C_interval
 > [eva] Recording results for taints
 > [eva] Done for function taints
 149c154,160
-< [eva] taint.c:194: Reusing old results for call to taints
+< [eva] taint.c:211: Reusing old results for call to taints
 ---
 > [eva] computing for function taints <- main.
->   Called from taint.c:194.
+>   Called from taint.c:211.
 > [eva] computing for function Frama_C_interval <- taints <- main.
->   Called from taint.c:170.
+>   Called from taint.c:187.
 > [eva] Done for function Frama_C_interval
 > [eva] Recording results for taints
 > [eva] Done for function taints
 169c180,186
-< [eva] taint.c:197: Reusing old results for call to taints
+< [eva] taint.c:214: Reusing old results for call to taints
 ---
 > [eva] computing for function taints <- main.
->   Called from taint.c:197.
+>   Called from taint.c:214.
 > [eva] computing for function Frama_C_interval <- taints <- main.
->   Called from taint.c:170.
+>   Called from taint.c:187.
 > [eva] Done for function Frama_C_interval
 > [eva] Recording results for taints
 > [eva] Done for function taints
 172,173d188
 < [eva:loop-unroll:auto] taint.c:157: Automatic loop unrolling.
 < [eva:loop-unroll:partial] taint.c:157: loop not completely unrolled
+186c201,207
+< [eva] taint.c:217: Reusing old results for call to taints
+---
+> [eva] computing for function taints <- main.
+>   Called from taint.c:217.
+> [eva] computing for function Frama_C_interval <- taints <- main.
+>   Called from taint.c:187.
+> [eva] Done for function Frama_C_interval
+> [eva] Recording results for taints
+> [eva] Done for function taints
diff --git a/tests/value/oracle_octagon/taint.res.oracle b/tests/value/oracle_octagon/taint.res.oracle
index 0fc62dbb2d3..93a7c9d2062 100644
--- a/tests/value/oracle_octagon/taint.res.oracle
+++ b/tests/value/oracle_octagon/taint.res.oracle
@@ -1,12 +1,12 @@
-197c197
+215c215
 <   u ∈ [0..10]
 ---
 >   u ∈ {0; 1; 2}
-199c199
+217c217
 <   x ∈ [1..11]
 ---
 >   x ∈ {1; 2}
-219c219
+237c237
 <   y ∈ [2..11]
 ---
 >   y ∈ {3; 5; 7; 9; 11}
diff --git a/tests/value/taint.c b/tests/value/taint.c
index c47c43d9b93..92bc5ea68ce 100644
--- a/tests/value/taint.c
+++ b/tests/value/taint.c
@@ -165,6 +165,23 @@ void taint_infinite_while(int t) {
   Frama_C_dump_each();
 }
 
+/* Tests ACSL predicates related to taint. */
+void tainted_predicate (void) {
+  int not_tainted = Frama_C_interval(0, 20);
+  int x = undet ? not_tainted : tainted;
+  int indirect = 0;
+  if (tainted) {
+    indirect = 1;
+  }
+  //@ check true: \tainted(tainted); // unknown as over-approximation of taint
+  //@ check false: !\tainted(tainted); // unknown as over-approximation of taint
+  //@ check false: \tainted(not_tainted);
+  //@ check true: !\tainted(not_tainted);
+  //@ assert unknown: !\tainted(x);
+  //@ check true: !\tainted(x);
+  //@ check \tainted(indirect); // for now, \tainted only considers direct taint.
+}
+
 // Taints global variable 'tainted'.
 void taints (void) {
   tainted = Frama_C_interval(0, 10);
@@ -197,5 +214,8 @@ int main(void) {
   taints();
   taint_infinite_while(tainted);
 
+  taints();
+  tainted_predicate();
+
   return 0;
 }
-- 
GitLab