From e4ae43c275129a270b5cb467d8316d1d2a56265a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 10 Aug 2023 10:32:32 +0200
Subject: [PATCH] [Eva] Adds test of -eva-show-perf.

---
 tests/value/oracle/show_perf.res.oracle       | 150 ++++++++++++++++++
 tests/value/oracle_apron/show_perf.res.oracle |  81 ++++++++++
 tests/value/show_perf.i                       |  42 +++++
 3 files changed, 273 insertions(+)
 create mode 100644 tests/value/oracle/show_perf.res.oracle
 create mode 100644 tests/value/oracle_apron/show_perf.res.oracle
 create mode 100644 tests/value/show_perf.i

diff --git a/tests/value/oracle/show_perf.res.oracle b/tests/value/oracle/show_perf.res.oracle
new file mode 100644
index 0000000000..7202898ac5
--- /dev/null
+++ b/tests/value/oracle/show_perf.res.oracle
@@ -0,0 +1,150 @@
+[kernel] Parsing show_perf.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  nondet ∈ [--..--]
+[eva] computing for function print_collatz <- main.
+  Called from show_perf.i:41.
+[eva] computing for function collatz <- print_collatz <- main.
+  Called from show_perf.i:35.
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+  Called from show_perf.i:28.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] Recording results for collatz
+[eva] Done for function collatz
+[eva] show_perf.i:36: Reusing old results for call to collatz
+[eva] show_perf.i:37: Frama_C_show_each: {7}, {16}, {52}
+[eva] Recording results for print_collatz
+[eva] Done for function print_collatz
+[eva] Recording results for main
+[eva] Done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function compute_next:
+  __retres ∈ [1..52]
+[eva:final-states] Values at end of function collatz:
+  i ∈ {16}
+  v ∈ {1}
+  max ∈ {52}
+  r.length ∈ {16}
+   .max ∈ {52}
+[eva:final-states] Values at end of function print_collatz:
+  r.length ∈ {16}
+   .max ∈ {52}
+[eva:final-states] Values at end of function main:
+  
+[eva] ######## Eva execution feedback ######## 
+  Long running functions:
+  ================================================================
+  * main: executed: 1x total: ?s
+    | print_collatz 1x ?s (?%) | self: ?s (?%)
+  * print_collatz: executed: 1x total: ?s
+    | collatz 2x ?s (?%) | self: ?s (?%)
+  * collatz: executed: 2x total: ?s
+    | compute_next 16x ?s (?%) | self: ?s (?%)
+  * compute_next: executed: 16x total: ?s
+    | self: ?s (?%)
+  
+  Execution time per callstack:
+  ================================================================
+  * main: executed: 1x total: ?s
+  | * print_collatz: executed: 1x total: ?s
+  | | * collatz: executed: 2x total: ?s
+  | | | * compute_next: executed: 16x total: ?s
+   
+[from] Computing for function compute_next
+[from] Done for function compute_next
+[from] Computing for function collatz
+[from] Done for function collatz
+[from] Computing for function print_collatz
+[from] Done for function print_collatz
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function compute_next:
+  \result FROM x
+[from] Function collatz:
+  \result FROM n
+[from] Function print_collatz:
+  NO EFFECTS
+[from] Function main:
+  NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function compute_next:
+    tmp; __retres
+[inout] Inputs for function compute_next:
+    \nothing
+[inout] Out (internal) for function collatz:
+    i; v; max; tmp; r
+[inout] Inputs for function collatz:
+    \nothing
+[inout] Out (internal) for function print_collatz:
+    r
+[inout] Inputs for function print_collatz:
+    \nothing
+[inout] Out (internal) for function main:
+    \nothing
+[inout] Inputs for function main:
+    \nothing
diff --git a/tests/value/oracle_apron/show_perf.res.oracle b/tests/value/oracle_apron/show_perf.res.oracle
new file mode 100644
index 0000000000..d997f5e393
--- /dev/null
+++ b/tests/value/oracle_apron/show_perf.res.oracle
@@ -0,0 +1,81 @@
+77c77,144
+< [eva] show_perf.i:36: Reusing old results for call to collatz
+---
+> [eva] computing for function collatz <- print_collatz <- main.
+>   Called from show_perf.i:36.
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+>   Called from show_perf.i:28.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] Recording results for collatz
+> [eva] Done for function collatz
+105,106c172,173
+<     | compute_next 16x ?s (?%) | self: ?s (?%)
+<   * compute_next: executed: 16x total: ?s
+---
+>     | compute_next 32x ?s (?%) | self: ?s (?%)
+>   * compute_next: executed: 32x total: ?s
+114c181
+<   | | | * compute_next: executed: 16x total: ?s
+---
+>   | | | * compute_next: executed: 32x total: ?s
diff --git a/tests/value/show_perf.i b/tests/value/show_perf.i
new file mode 100644
index 0000000000..5dc541cc95
--- /dev/null
+++ b/tests/value/show_perf.i
@@ -0,0 +1,42 @@
+/* run.config*
+   FILTER: sed -e 's/\([0-9.]\+\(%\|s\)\)/?\2/g'
+   STDOPT: +"-eva-show-perf"
+*/
+
+/* This example is kept minimal to ensure the stability of the output
+   of -eva-show-perf. */
+
+volatile int nondet;
+
+typedef struct S {
+  unsigned int length;
+  unsigned int max;
+} result;
+
+int compute_next(unsigned int x) {
+  return (x % 2 == 0) ? x / 2 : 3*x + 1;
+}
+
+result collatz(unsigned int n) {
+  unsigned int i = 0;
+  unsigned int v = n;
+  unsigned int max = n;
+  //@ loop unroll 100;
+  for (i = 0; i < 100; i++) {
+    if (v == 1) break;
+    if (v > max) max = v;
+    v = compute_next(v);
+  }
+  result r = { .length = i, .max = max };
+  return r;
+}
+
+void print_collatz(unsigned int n) {
+  result r = collatz(n); // 1 call to collatz
+  r = collatz(n);        // 1 call cached by memexec
+  Frama_C_show_each(n, r.length, r.max);
+}
+
+void main (void) {
+  print_collatz(7); // 16 calls to [compute_next] for n = 7.
+}
-- 
GitLab