From 82f1a0f6504f3845e38d9a04079b2760b17d18f5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 25 Sep 2020 11:51:29 +0200
Subject: [PATCH] [Eva] Adds a test for string builtins applied on misaligned
offsetmap or pointer.
---
tests/builtins/oracle/wcslen.res.oracle | 82 ++++++++++++++++++++-----
tests/builtins/wcslen.c | 32 ++++++++++
2 files changed, 100 insertions(+), 14 deletions(-)
diff --git a/tests/builtins/oracle/wcslen.res.oracle b/tests/builtins/oracle/wcslen.res.oracle
index 784bf02c5cf..00a752d3a13 100644
--- a/tests/builtins/oracle/wcslen.res.oracle
+++ b/tests/builtins/oracle/wcslen.res.oracle
@@ -31,7 +31,7 @@
[11] ∈ {100}
nondet ∈ [--..--]
[eva] computing for function small_sets <- main.
- Called from tests/builtins/wcslen.c:339.
+ Called from tests/builtins/wcslen.c:370.
[eva] tests/builtins/wcslen.c:60: Call to builtin wcslen
[eva] tests/builtins/wcslen.c:60:
function wcslen: precondition 'valid_string_s' got status valid.
@@ -55,7 +55,7 @@
[eva] Recording results for small_sets
[eva] Done for function small_sets
[eva] computing for function zero_termination <- main.
- Called from tests/builtins/wcslen.c:340.
+ Called from tests/builtins/wcslen.c:371.
[eva] tests/builtins/wcslen.c:89: Call to builtin wcslen
[eva:alarm] tests/builtins/wcslen.c:89: Warning:
function wcslen: precondition 'valid_string_s' got status unknown.
@@ -69,7 +69,7 @@
[eva] Recording results for zero_termination
[eva] Done for function zero_termination
[eva] computing for function wcslen_initialization <- main.
- Called from tests/builtins/wcslen.c:341.
+ Called from tests/builtins/wcslen.c:372.
[eva] tests/builtins/wcslen.c:105: Call to builtin wcslen
[eva:alarm] tests/builtins/wcslen.c:105: Warning:
function wcslen: precondition 'valid_string_s' got status unknown.
@@ -88,7 +88,7 @@
[eva] Recording results for wcslen_initialization
[eva] Done for function wcslen_initialization
[eva] computing for function wcslen_large <- main.
- Called from tests/builtins/wcslen.c:342.
+ Called from tests/builtins/wcslen.c:373.
[eva] computing for function init_array_nondet <- wcslen_large <- main.
Called from tests/builtins/wcslen.c:168.
[eva] tests/builtins/wcslen.c:161: Call to builtin memset
@@ -152,7 +152,7 @@
[eva] Recording results for wcslen_large
[eva] Done for function wcslen_large
[eva] computing for function wcslen_large_uninit <- main.
- Called from tests/builtins/wcslen.c:343.
+ Called from tests/builtins/wcslen.c:374.
[eva] computing for function init_array_nondet <- wcslen_large_uninit <- main.
Called from tests/builtins/wcslen.c:197.
[eva] tests/builtins/wcslen.c:161: Call to builtin memset
@@ -193,7 +193,7 @@
[eva] Recording results for wcslen_large_uninit
[eva] Done for function wcslen_large_uninit
[eva] computing for function misc <- main.
- Called from tests/builtins/wcslen.c:344.
+ Called from tests/builtins/wcslen.c:375.
[eva] tests/builtins/wcslen.c:241: Call to builtin wcslen
[eva:alarm] tests/builtins/wcslen.c:241: Warning:
function wcslen: precondition 'valid_string_s' got status invalid.
@@ -245,14 +245,14 @@
[eva] Recording results for misc
[eva] Done for function misc
[eva] computing for function bitfields <- main.
- Called from tests/builtins/wcslen.c:345.
+ Called from tests/builtins/wcslen.c:376.
[eva] tests/builtins/wcslen.c:140: Call to builtin wcslen
[eva:alarm] tests/builtins/wcslen.c:140: Warning:
function wcslen: precondition 'valid_string_s' got status invalid.
[eva] Recording results for bitfields
[eva] Done for function bitfields
[eva] computing for function bitfields2 <- main.
- Called from tests/builtins/wcslen.c:346.
+ Called from tests/builtins/wcslen.c:377.
[eva] tests/builtins/wcslen.c:155: Call to builtin wcslen
[eva] tests/builtins/wcslen.c:155:
function wcslen: precondition 'valid_string_s' got status valid.
@@ -260,7 +260,7 @@
[eva] Recording results for bitfields2
[eva] Done for function bitfields2
[eva] computing for function escaping <- main.
- Called from tests/builtins/wcslen.c:347.
+ Called from tests/builtins/wcslen.c:378.
[eva:alarm] tests/builtins/wcslen.c:222: Warning:
pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:alarm] tests/builtins/wcslen.c:222: Warning:
@@ -282,7 +282,7 @@
[eva] Recording results for escaping
[eva] Done for function escaping
[eva] computing for function big_array <- main.
- Called from tests/builtins/wcslen.c:348.
+ Called from tests/builtins/wcslen.c:379.
[eva:alarm] tests/builtins/wcslen.c:287: Warning:
out of bounds write. assert \valid(p);
[eva:alarm] tests/builtins/wcslen.c:291: Warning:
@@ -312,7 +312,7 @@
[eva] Recording results for big_array
[eva] Done for function big_array
[eva] computing for function negative_offsets <- main.
- Called from tests/builtins/wcslen.c:349.
+ Called from tests/builtins/wcslen.c:380.
[eva] tests/builtins/wcslen.c:314: starting to merge loop iterations
[eva] computing for function Frama_C_interval <- negative_offsets <- main.
Called from tests/builtins/wcslen.c:318.
@@ -364,6 +364,32 @@
function wcslen: precondition 'valid_string_s' got status unknown.
[eva] Recording results for negative_offsets
[eva] Done for function negative_offsets
+[eva] computing for function misaligned_string <- main.
+ Called from tests/builtins/wcslen.c:381.
+[eva] tests/builtins/wcslen.c:345: assertion got status valid.
+[eva] tests/builtins/wcslen.c:346: Call to builtin wcslen
+[eva] tests/builtins/wcslen.c:346:
+ function wcslen: precondition 'valid_string_s' got status valid.
+[eva] computing for function Frama_C_interval <- misaligned_string <- main.
+ Called from tests/builtins/wcslen.c:350.
+[eva] tests/builtins/wcslen.c:350:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:alarm] tests/builtins/wcslen.c:351: Warning:
+ out of bounds write. assert \valid((char *)((wchar_t *)b) + i);
+[eva:alarm] tests/builtins/wcslen.c:352: Warning: assertion got status unknown.
+[eva] tests/builtins/wcslen.c:353: Call to builtin wcslen
+[eva:alarm] tests/builtins/wcslen.c:353: Warning:
+ function wcslen: precondition 'valid_string_s' got status unknown.
+[eva:alarm] tests/builtins/wcslen.c:361: Warning: assertion got status unknown.
+[eva] tests/builtins/wcslen.c:362: Call to builtin wcslen
+[eva:alarm] tests/builtins/wcslen.c:362: Warning:
+ function wcslen: precondition 'valid_string_s' got status unknown.
+[eva] tests/builtins/wcslen.c:365: Call to builtin wcslen
+[eva:alarm] tests/builtins/wcslen.c:365: Warning:
+ function wcslen: precondition 'valid_string_s' got status invalid.
+[eva] Recording results for misaligned_string
+[eva] Done for function misaligned_string
[eva] Recording results for main
[eva] done for function main
[scope:rm_asserts] removing 3 assertion(s)
@@ -405,6 +431,24 @@
[1..3] ∈ ESCAPINGADDR
z1 ∈ {0}
z2 ∈ {0}
+[eva:final-states] Values at end of function misaligned_string:
+ Frama_C_entropy_source ∈ [--..--]
+ a[0][bits 0 to 7] ∈ {1}
+ [0][bits 8 to 31] ∈ {0}
+ [1] ∈ {1}
+ [2] ∈ {0}
+ a_length ∈ {2}
+ b[0..9999999]# ∈ {0; 17} repeated %8
+ i ∈ [0..39999999]
+ b_length ∈ [0..9999999]
+ c[0][bits 0 to 7] ∈ {0}
+ {[0][bits 8 to 31]#; [1][bits 0 to 7]#} ∈ {1}
+ {[1][bits 8 to 31]#; [2][bits 0 to 7]#} ∈ {2}
+ {[2][bits 8 to 31]; [3][bits 0 to 7]} ∈ {0}
+ {[3][bits 8 to 31]#; [4][bits 0 to 7]#} ∈ {4}
+ [4][bits 8 to 31] ∈ {0}
+ p ∈ {{ &c + {1} }}
+ c_length ∈ {2}
[eva:final-states] Values at end of function misc:
Frama_C_entropy_source ∈ [--..--]
loc_str ∈ {{ L"Bonjour Monde\n" }}
@@ -524,9 +568,11 @@
[from] Done for function bitfields2
[from] Computing for function escaping
[from] Done for function escaping
-[from] Computing for function misc
-[from] Computing for function Frama_C_interval <-misc
+[from] Computing for function misaligned_string
+[from] Computing for function Frama_C_interval <-misaligned_string
[from] Done for function Frama_C_interval
+[from] Done for function misaligned_string
+[from] Computing for function misc
[from] Done for function misc
[from] Computing for function negative_offsets
[from] Done for function negative_offsets
@@ -560,7 +606,8 @@
non_terminated2[2..3]; empty_or_uninitialized[0];
uninitialized[0]; s[0..1]; t[0..3]; s; s; a[3..99]; a[3..99];
s[0..3]; loc_char_array[0..4]; x[0..3]; maybe_init[0..1];
- t[0..999999]; u[0..199]; r[0..200]; buf[0..99];
+ t[0..999999]; u[0..199]; r[0..200]; buf[0..99]; a[0..2];
+ b[0..9999999]; c{[0][bits 8 to 31]; [1..3]; [4][bits 0 to 7]};
L"Hello World\n"[bits 0 to 415];
L"abc\000\000\000abc"[bits 0 to 319]; L""; L"a"[bits 0 to 63];
L"aa"[bits 0 to 95]; L"aaa"[bits 0 to 127];
@@ -582,6 +629,8 @@
NO EFFECTS
[from] Function escaping:
NO EFFECTS
+[from] Function misaligned_string:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function misc:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function negative_offsets:
@@ -620,6 +669,11 @@
s[0..3]; z1; tmp; z2; tmp_0
[inout] Inputs for function escaping:
nondet
+[inout] Out (internal) for function misaligned_string:
+ Frama_C_entropy_source; a[0..2]; a_length; b[0..9999999]; i; b_length;
+ c[0..4]; p; c_length
+[inout] Inputs for function misaligned_string:
+ Frama_C_entropy_source; nondet
[inout] Out (internal) for function misc:
Frama_C_entropy_source; loc_str; loc_char_array[3]; sz1; sz2; sz3;
sz4; sz5; sz6; sz7; sz8; x[0..3]; z[0..3]; i; str; s1; tmp; s2; tmp_0;
diff --git a/tests/builtins/wcslen.c b/tests/builtins/wcslen.c
index dea7cd1aad9..183e2f2a2da 100644
--- a/tests/builtins/wcslen.c
+++ b/tests/builtins/wcslen.c
@@ -335,6 +335,37 @@ void negative_offsets() {
wchar_t dest[100 * 2];
}
+#define MAX 10000000
+
+void misaligned_string () {
+ // Read an offsetmap with a value range smaller than the read characters.
+ wchar_t a[3] = {0};
+ *(char *)a = 1;
+ a[1] = 1;
+ //@ assert valid_read_wstring(&a[0]);
+ unsigned int a_length = wcslen(&a[0]);
+ /* Read an offsetmap with repeated values smaller than the searched
+ characters: test a performance issue. */
+ wchar_t b[MAX] = {0};
+ int i = Frama_C_interval(0, MAX * 4);
+ *((char *)b + i) = (char)17;
+ //@ assert valid_read_wstring(&b[0]);
+ unsigned int b_length = wcslen(&b[0]);
+ /* Read an offsetmap through a misaligned pointer. */
+ wchar_t c[5] = {0};
+ wchar_t *p = (wchar_t *)( (char *)c + 1);
+ *p = 1;
+ *(p+1) = 2;
+ *(p+2) = 0; // If we accept the string pointed by p, its length should be 2.
+ *(p+3) = 4;
+ //@ assert valid_read_wstring(p);
+ unsigned int c_length = wcslen(p);
+ if (nondet) {
+ *(p+2) = 3; // The string pointed by p cannot be valid here.
+ c_length = wcslen(p);
+ }
+}
+
int main (int c) {
small_sets();
zero_termination();
@@ -347,5 +378,6 @@ int main (int c) {
escaping();
big_array();
negative_offsets();
+ misaligned_string();
return 0;
}
--
GitLab