From 8a9f4506ff3ec498ebe3def566a594990bfa3c4e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 27 Mar 2024 15:46:04 +0100
Subject: [PATCH] [Eva] Tests the reduction by ACSL predicates valid_string and
valid_read_string.
---
tests/value/oracle/strings_logic.res.oracle | 232 ++++++++++++++++++
.../oracle_multidim/strings_logic.res.oracle | 8 +
tests/value/strings_logic.c | 178 ++++++++++++++
3 files changed, 418 insertions(+)
create mode 100644 tests/value/oracle/strings_logic.res.oracle
create mode 100644 tests/value/oracle_multidim/strings_logic.res.oracle
create mode 100644 tests/value/strings_logic.c
diff --git a/tests/value/oracle/strings_logic.res.oracle b/tests/value/oracle/strings_logic.res.oracle
new file mode 100644
index 00000000000..1b681b00f32
--- /dev/null
+++ b/tests/value/oracle/strings_logic.res.oracle
@@ -0,0 +1,232 @@
+[kernel] Parsing strings_logic.c (with 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 reduce_by_valid_string <- main.
+ Called from strings_logic.c:177.
+[eva:loop-unroll:auto] strings_logic.c:30: Automatic loop unrolling.
+[eva:loop-unroll:auto] strings_logic.c:36: Automatic loop unrolling.
+[eva:loop-unroll:auto] strings_logic.c:41: Automatic loop unrolling.
+[eva:loop-unroll:auto] strings_logic.c:48: Automatic loop unrolling.
+[eva:loop-unroll:auto] strings_logic.c:53: Automatic loop unrolling.
+[eva:alarm] strings_logic.c:84: Warning: assertion got status unknown.
+[eva] strings_logic.c:85:
+ Frama_C_show_each_valid_string_zero_offset:
+ {{ &s1 ; &s2 ; &s_zero ; &s_partially_valid ; &s_imprecise ; &s_unknown ;
+ &anything }}
+[eva:alarm] strings_logic.c:89: Warning: assertion got status unknown.
+[eva] strings_logic.c:90:
+ Frama_C_show_each_valid_read_string_zero_offset:
+ {{ &s1 ; &s2 ; &s_const ; &s_zero ; &s_partially_valid ; &s_imprecise ;
+ &s_unknown ; &anything ; "hello\000 world" ; "hello world" }}
+[eva:alarm] strings_logic.c:94: Warning: assertion got status unknown.
+[eva] strings_logic.c:95:
+ Frama_C_show_each_invalid_string_zero_offset:
+ {{ NULL ; &s_const ; &s_uninit ; &s_partially_initialized ; &s_imprecise ;
+ &s_unknown ; &anything ; "hello\000 world" ; "hello world" }}
+[eva:alarm] strings_logic.c:99: Warning: assertion got status unknown.
+[eva] strings_logic.c:100:
+ Frama_C_show_each_invalid_read_string_zero_offset:
+ {{ NULL ; &s_uninit ; &s_partially_initialized ; &s_imprecise ; &s_unknown ;
+ &anything }}
+[eva:alarm] strings_logic.c:108: Warning: assertion got status unknown.
+[eva] strings_logic.c:109:
+ Frama_C_show_each_valid_string_precise_offset:
+ {{ &s1 + {5; 10} ; &s2 + {5; 10} ; &s_zero + {5; 10; 20} ;
+ &s_partially_initialized + {5; 10; 20} ;
+ &s_partially_valid + {5; 10; 20} ; &s_imprecise + {5; 10; 20} ;
+ &s_unknown + {5; 10; 20} ; &anything + {5; 10} }}
+[eva:alarm] strings_logic.c:113: Warning: assertion got status unknown.
+[eva] strings_logic.c:114:
+ Frama_C_show_each_valid_read_string_precise_offset:
+ {{ &s1 + {5; 10} ; &s2 + {5; 10} ; &s_const + {5; 10} ;
+ &s_zero + {5; 10; 20} ; &s_partially_initialized + {5; 10; 20} ;
+ &s_partially_valid + {5; 10; 20} ; &s_imprecise + {5; 10; 20} ;
+ &s_unknown + {5; 10; 20} ; &anything + {5; 10} ;
+ "hello\000 world" + {5; 10} ; "hello world" + {5; 10} }}
+[eva:alarm] strings_logic.c:118: Warning: assertion got status unknown.
+[eva] strings_logic.c:119:
+ Frama_C_show_each_invalid_string_precise_offset:
+ {{ NULL + {5; 10; 20} ; &s1 + {5; 10; 20} ; &s2 + {5; 10; 20} ;
+ &s_const + {5; 10; 20} ; &s_uninit + {5; 10; 20} ;
+ &s_partially_initialized + {5; 10; 20} ;
+ &s_partially_valid + {5; 10; 20} ; &s_imprecise + {5; 10; 20} ;
+ &s_unknown + {5; 10; 20} ; &anything + {5; 10; 20} ;
+ "hello\000 world" + {5; 10; 20} ; "hello world" + {5; 10; 20} }}
+[eva:alarm] strings_logic.c:123: Warning: assertion got status unknown.
+[eva] strings_logic.c:124:
+ Frama_C_show_each_invalid_read_string_precise_offset:
+ {{ NULL + {5; 10; 20} ; &s1 + {5; 10; 20} ; &s2 + {5; 10; 20} ;
+ &s_const + {5; 10; 20} ; &s_uninit + {5; 10; 20} ;
+ &s_partially_initialized + {5; 10; 20} ;
+ &s_partially_valid + {5; 10; 20} ; &s_imprecise + {5; 10; 20} ;
+ &s_unknown + {5; 10; 20} ; &anything + {5; 10; 20} ;
+ "hello\000 world" + {5; 10; 20} ; "hello world" + {5; 10; 20} }}
+[eva:alarm] strings_logic.c:131: Warning: assertion got status unknown.
+[eva] strings_logic.c:132:
+ Frama_C_show_each_valid_string_imprecise_offset:
+ {{ &s1 + [0..13] ; &s2 + [0..12] ; &s_zero + [0..31] ;
+ &s_partially_initialized + [0..31] ; &s_partially_valid + [0..31] ;
+ &s_imprecise + [0..31] ; &s_unknown + [0..31] ; &anything + [0..15] }}
+[eva:alarm] strings_logic.c:136: Warning: assertion got status unknown.
+[eva] strings_logic.c:137:
+ Frama_C_show_each_valid_read_string_imprecise_offset:
+ {{ &s1 + [0..13] ; &s2 + [0..12] ; &s_const + [0..16] ; &s_zero + [0..31] ;
+ &s_partially_initialized + [0..31] ; &s_partially_valid + [0..31] ;
+ &s_imprecise + [0..31] ; &s_unknown + [0..31] ; &anything + [0..15] ;
+ "hello\000 world" + [0..12] ; "hello world" + [0..11] }}
+[eva:alarm] strings_logic.c:141: Warning: assertion got status unknown.
+[eva] strings_logic.c:142:
+ Frama_C_show_each_invalid_string_imprecise_offset:
+ {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+ &s_const + [-123..147] ; &s_zero + [-123..147] ; &s_uninit + [-123..147] ;
+ &s_partially_initialized + [-123..147] ;
+ &s_partially_valid + [-123..147] ; &s_imprecise + [-123..147] ;
+ &s_unknown + [-123..147] ; &anything + [-123..147] ;
+ "hello\000 world" + [-123..147] ; "hello world" + [-123..147] }}
+[eva:alarm] strings_logic.c:146: Warning: assertion got status unknown.
+[eva] strings_logic.c:147:
+ Frama_C_show_each_invalid_read_string_imprecise_offset:
+ {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+ &s_const + [-123..147] ; &s_zero + [-123..147] ; &s_uninit + [-123..147] ;
+ &s_partially_initialized + [-123..147] ;
+ &s_partially_valid + [-123..147] ; &s_imprecise + [-123..147] ;
+ &s_unknown + [-123..147] ; &anything + [-123..147] ;
+ "hello\000 world" + [-123..147] ; "hello world" + [-123..147] }}
+[eva] computing for function garbled_mix <- reduce_by_valid_string <- main.
+ Called from strings_logic.c:151.
+[eva] using specification for function garbled_mix
+[eva:garbled-mix:assigns] strings_logic.c:151:
+ The specification of function garbled_mix
+ has generated a garbled mix of addresses for assigns clause \result.
+[eva] Done for function garbled_mix
+[eva:alarm] strings_logic.c:154: Warning: assertion got status unknown.
+[eva] strings_logic.c:155:
+ Frama_C_show_each_valid_string_garbled_mix:
+ {{ &s1 + [0..13] ; &s2 + [0..12] ; &s_zero + [0..31] ;
+ &s_partially_initialized + [0..31] ; &s_partially_valid + [0..31] ;
+ &s_imprecise + [0..31] ; &s_unknown + [0..31] ; &anything + [0..15] }}
+[eva:alarm] strings_logic.c:159: Warning: assertion got status unknown.
+[eva] strings_logic.c:160:
+ Frama_C_show_each_valid_read_string_garbled_mix:
+ {{ &s1 + [0..13] ; &s2 + [0..12] ; &s_const + [0..16] ; &s_zero + [0..31] ;
+ &s_partially_initialized + [0..31] ; &s_partially_valid + [0..31] ;
+ &s_imprecise + [0..31] ; &s_unknown + [0..31] ; &anything + [0..15] ;
+ "hello\000 world" + [0..12] ; "hello world" + [0..11] }}
+[eva:alarm] strings_logic.c:164: Warning: assertion got status unknown.
+[eva] strings_logic.c:165:
+ Frama_C_show_each_invalid_string_garbled_mix:
+ {{ garbled mix of &{s1; s2; s_const; s_zero; s_uninit;
+ s_partially_initialized; s_partially_valid; s_imprecise;
+ s_unknown; anything; "hello\000 world"; "hello world"}
+ (origin: Library function {strings_logic.c:151}) }}
+[eva:alarm] strings_logic.c:169: Warning: assertion got status unknown.
+[eva] strings_logic.c:170:
+ Frama_C_show_each_invalid_read_string_garbled_mix:
+ {{ garbled mix of &{s1; s2; s_const; s_zero; s_uninit;
+ s_partially_initialized; s_partially_valid; s_imprecise;
+ s_unknown; anything; "hello\000 world"; "hello world"}
+ (origin: Library function {strings_logic.c:151}) }}
+[eva] Recording results for reduce_by_valid_string
+[eva] Done for function reduce_by_valid_string
+[eva] Recording results for main
+[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ strings_logic.c:151: assigns clause on addresses
+ (read in 2 statements, propagated through 1 statement)
+ garbled mix of &{s1; s2; s_const; s_zero; s_uninit;
+ s_partially_initialized; s_partially_valid; s_imprecise;
+ s_unknown; anything; "hello\000 world"; "hello world"}
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function reduce_by_valid_string:
+ s1[0] ∈ {104}
+ [1] ∈ {101}
+ [2..3] ∈ {108}
+ [4] ∈ {111}
+ [5] ∈ {0}
+ [6] ∈ {32}
+ [7] ∈ {119}
+ [8] ∈ {111}
+ [9] ∈ {114}
+ [10] ∈ {108}
+ [11] ∈ {100}
+ [12] ∈ {33}
+ [13] ∈ {0}
+ s2[0] ∈ {104}
+ [1] ∈ {101}
+ [2..3] ∈ {108}
+ [4] ∈ {111}
+ [5] ∈ {32}
+ [6] ∈ {119}
+ [7] ∈ {111}
+ [8] ∈ {114}
+ [9] ∈ {108}
+ [10] ∈ {100}
+ [11] ∈ {33}
+ [12] ∈ {0}
+ s_const[0] ∈ {99}
+ [1] ∈ {111}
+ [2] ∈ {110}
+ [3] ∈ {115}
+ [4] ∈ {116}
+ [5] ∈ {32}
+ [6] ∈ {99}
+ [7] ∈ {104}
+ [8] ∈ {97}
+ [9] ∈ {114}
+ [10] ∈ {32}
+ [11] ∈ {97}
+ [12..13] ∈ {114}
+ [14] ∈ {97}
+ [15] ∈ {121}
+ [16] ∈ {0}
+ s_zero[0..31] ∈ {0}
+ s_partially_initialized[0..9] ∈ UNINITIALIZED
+ [10..24] ∈ {105}
+ [25] ∈ {0}
+ [26..31] ∈ UNINITIALIZED
+ s_invalid[0..31] ∈ {97}
+ s_partially_valid[0..7] ∈ {111}
+ [8] ∈ {0}
+ [9..15] ∈ {111}
+ [16] ∈ {0}
+ [17..31] ∈ {111}
+ s_imprecise[0..31] ∈ [--..--]
+ s_unknown[0..31] ∈ [--..--] or UNINITIALIZED
+ anything.ptr ∈ {{ &x }}
+ .d ∈ [-128. .. 127.]
+ .c ∈ [--..--]
+ .[bits 104 to 127] ∈ UNINITIALIZED
+ p ∈ {0}
+ offset ∈ {5; 10; 20}
+[eva:final-states] Values at end of function main:
+
+[from] Computing for function reduce_by_valid_string
+[from] Computing for function garbled_mix <-reduce_by_valid_string
+[from] Done for function garbled_mix
+[from] Done for function reduce_by_valid_string
+[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 garbled_mix:
+ \result FROM p
+[from] Function reduce_by_valid_string:
+ NO EFFECTS
+[from] Function main:
+ NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function reduce_by_valid_string:
+ s1[0..13]; s2[0..12]; s_const[0..16]; s_zero[0..31];
+ s_partially_initialized[10..25]; i; s_invalid[0..31]; i_0;
+ s_partially_valid[0..31]; i_1; s_imprecise[0..31]; i_2; s_unknown[0..31];
+ i_3; anything{.ptr; .d; .c}; p; offset; tmp; tmp_0
+[inout] Inputs for function reduce_by_valid_string:
+ nondet
+[inout] Out (internal) for function main:
+ \nothing
+[inout] Inputs for function main:
+ nondet
diff --git a/tests/value/oracle_multidim/strings_logic.res.oracle b/tests/value/oracle_multidim/strings_logic.res.oracle
new file mode 100644
index 00000000000..ed8b014f3c9
--- /dev/null
+++ b/tests/value/oracle_multidim/strings_logic.res.oracle
@@ -0,0 +1,8 @@
+83c83
+< {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+---
+> {{ NULL + [0..147] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+92c92
+< {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+---
+> {{ NULL + [0..147] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
diff --git a/tests/value/strings_logic.c b/tests/value/strings_logic.c
new file mode 100644
index 00000000000..3fe276661fe
--- /dev/null
+++ b/tests/value/strings_logic.c
@@ -0,0 +1,178 @@
+/* run.config*
+ STDOPT: +"-eva-auto-loop-unroll 32"
+*/
+
+/* Tests the evaluation and reduction by ACSL predicate on strings. */
+
+#include "__fc_string_axiomatic.h"
+
+volatile char nondet;
+
+struct anything {
+ int *ptr;
+ double d;
+ char c;
+};
+
+/*@ assigns \result \from p; */
+char* garbled_mix(char *p);
+
+/* Tests the reduction by ACSL predicate "valid_string" and "valid_read_string"
+ from the Frama-C libc. */
+void reduce_by_valid_string (void) {
+ char s1[] = "hello\000 world!";
+ char s2[] = "hello world!";
+ const char s_const[] = "const char array";
+ char s_zero[32] = {0};
+ char s_uninit[32];
+
+ char s_partially_initialized[32]; // valid only between 10 and 25.
+ for (int i = 10; i < 25; i++) {
+ s_partially_initialized[i] = 'i';
+ }
+ s_partially_initialized[25] = '\0';
+
+ char s_invalid[32]; // Invalid as no terminating \0
+ for (int i = 0; i < 32; i++){
+ s_invalid[i] = 'a';
+ }
+
+ char s_partially_valid[32]; // valid up to offset 16.
+ for (int i = 0; i < 32; i++){
+ s_partially_valid[i] = 'o';
+ }
+ s_partially_valid[8] = '\0';
+ s_partially_valid[16] = '\0';
+
+ char s_imprecise[32]; // char array of imprecise values
+ for (int i = 0; i < 32; i++){
+ s_imprecise[i] = nondet;
+ }
+
+ char s_unknown[32]; // char array of imprecise values that may be uninitialized
+ for (int i = 0; i < 32; i++) {
+ if (nondet) s_unknown[i] = nondet;
+ }
+
+ int x;
+ struct anything anything;
+ anything.ptr = &x;
+ anything.d = (double)nondet;
+ anything.c = nondet;
+
+ // Pointer p that can point to any of the strings above.
+ char *p;
+ switch (nondet) {
+ case 0: p = "hello\000 world"; break;
+ case 1: p = "hello world"; break;
+ case 2: p = s1; break;
+ case 3: p = s2; break;
+ case 4: p = s_const; break;
+ case 5: p = s_zero; break;
+ case 6: p = s_uninit; break;
+ case 7: p = s_partially_initialized; break;
+ case 8: p = s_partially_valid; break;
+ case 9: p = s_imprecise; break;
+ case 10: p = s_unknown; break;
+ case 11: p = (char *)&anything; break;
+ default: p = NULL;
+ }
+
+ // Test with a zero offset for all bases.
+
+ if (nondet) {
+ //@ assert valid_string(p);
+ Frama_C_show_each_valid_string_zero_offset(p);
+ }
+
+ if (nondet) {
+ //@ assert valid_read_string(p);
+ Frama_C_show_each_valid_read_string_zero_offset(p);
+ }
+
+ if (nondet) {
+ //@ assert !valid_string(p);
+ Frama_C_show_each_invalid_string_zero_offset(p);
+ }
+
+ if (nondet) {
+ //@ assert !valid_read_string(p);
+ Frama_C_show_each_invalid_read_string_zero_offset(p);
+ }
+
+ // Test with a precise non-zero non-singleton offset.
+ int offset = nondet ? 5 : (nondet ? 10 : 20);
+ p = p + offset;
+
+ if (nondet) {
+ //@ assert valid_string(p);
+ Frama_C_show_each_valid_string_precise_offset(p);
+ }
+
+ if (nondet) {
+ //@ assert valid_read_string(p);
+ Frama_C_show_each_valid_read_string_precise_offset(p);
+ }
+
+ if (nondet) {
+ //@ assert !valid_string(p);
+ Frama_C_show_each_invalid_string_precise_offset(p);
+ }
+
+ if (nondet) {
+ //@ assert !valid_read_string(p);
+ Frama_C_show_each_invalid_read_string_precise_offset(p);
+ }
+
+ // Test with a very imprecise offset.
+ p = p + nondet;
+
+ if (nondet) {
+ //@ assert valid_string(p);
+ Frama_C_show_each_valid_string_imprecise_offset(p);
+ }
+
+ if (nondet) {
+ //@ assert valid_read_string(p);
+ Frama_C_show_each_valid_read_string_imprecise_offset(p);
+ }
+
+ if (nondet) {
+ //@ assert !valid_string(p);
+ Frama_C_show_each_invalid_string_imprecise_offset(p);
+ }
+
+ if (nondet) {
+ //@ assert !valid_read_string(p);
+ Frama_C_show_each_invalid_read_string_imprecise_offset(p);
+ }
+
+ // Test with a garbled mix.
+ p = garbled_mix(p);
+
+ if (nondet) {
+ //@ assert valid_string(p);
+ Frama_C_show_each_valid_string_garbled_mix(p);
+ }
+
+ if (nondet) {
+ //@ assert valid_read_string(p);
+ Frama_C_show_each_valid_read_string_garbled_mix(p);
+ }
+
+ if (nondet) {
+ //@ assert !valid_string(p);
+ Frama_C_show_each_invalid_string_garbled_mix(p);
+ }
+
+ if (nondet) {
+ //@ assert !valid_read_string(p);
+ Frama_C_show_each_invalid_read_string_garbled_mix(p);
+ }
+
+ p = NULL;
+}
+
+void main (void) {
+ reduce_by_valid_string();
+}
--
GitLab