From 0217e3d94b4c472f30baa64262a3991d5cb6a36a Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 27 Mar 2020 09:56:10 +0100
Subject: [PATCH] [Instantiate] Fixes Memset for all bits to one
---
src/plugins/instantiate/string/memset.ml | 13 +++++++----
.../tests/string/oracle/memset_FF.res.oracle | 23 +++++++++----------
2 files changed, 19 insertions(+), 17 deletions(-)
diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml
index f681aa0ef13..b62c37aa2ca 100644
--- a/src/plugins/instantiate/string/memset.ml
+++ b/src/plugins/instantiate/string/memset.ml
@@ -89,15 +89,18 @@ let pset_len_bytes_all_bits_to_one ?loc ptr bytes_len =
papp ?loc ((find_nan_for_type t.term_type), [], [t])
| Ctype(TPtr(_)) ->
pnot ?loc (pvalid_read ?loc (here_label, t))
- | Ctype(TInt(kind, _)) | Ctype(TEnum({ ekind = kind }, _)) ->
+ | Ctype((TInt(kind, _) | TEnum({ ekind = kind }, _)) as typ) ->
let is_signed = Cil.isSigned kind in
let bits = Cil.bitsSizeOfInt kind in
- let value = if is_signed then
- Cil.min_signed_number bits
+ let value =
+ if is_signed then
+ let zero = tinteger ?loc 0 in
+ let zero = Logic_utils.mk_cast ?loc typ zero in
+ term (TUnOp(BNot, zero)) t.term_type
else
- Cil.max_unsigned_number bits
+ let value = Cil.max_unsigned_number bits in
+ term ?loc (TConst (Integer (value,None))) Linteger
in
- let value = term ?loc (TConst (Integer (value,None))) Linteger in
prel ?loc (Req, t, value)
| _ ->
unexpected "non atomic type during equality generation"
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
index 7495743e8a2..0054f340577 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
@@ -97,7 +97,7 @@ void nested_chars(char (* /*[10]*/ dest)[10])
ensures
set_content:
\let __fc_len = len / 4;
- ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ -2147483648;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ ~((int)0);
ensures result: \result ≡ ptr;
assigns *(ptr + (0 .. len / 4 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
@@ -176,7 +176,7 @@ void unsigned_integer(unsigned int * /*[10]*/ dest)
ensures
set_content:
\let __fc_len = len / 4;
- ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ -2147483648;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ ~((long)0);
ensures result: \result ≡ ptr;
assigns *(ptr + (0 .. len / 4 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
@@ -229,8 +229,7 @@ void unsigned_long_integer(unsigned long * /*[10]*/ dest)
ensures
set_content:
\let __fc_len = len / 8;
- ∀ ℤ j0;
- 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ -9223372036854775808;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ ~((long long)0);
ensures result: \result ≡ ptr;
assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
@@ -320,7 +319,7 @@ void with_named(named * /*[10]*/ dest)
\let __fc_len = len / 8;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
- (ptr + j0)->x ≡ -2147483648 ∧ (ptr + j0)->y ≡ -2147483648;
+ (ptr + j0)->x ≡ ~((int)0) ∧ (ptr + j0)->y ≡ ~((int)0);
ensures result: \result ≡ ptr;
assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
@@ -374,7 +373,7 @@ void pointers(int ** /*[10]*/ dest)
\let __fc_len = len / 40;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
- (∀ ℤ j1; 0 ≤ j1 < 10 ⇒ (*(ptr + j0))[j1] ≡ -2147483648);
+ (∀ ℤ j1; 0 ≤ j1 < 10 ⇒ (*(ptr + j0))[j1] ≡ ~((int)0));
ensures result: \result ≡ ptr;
assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1], \result;
assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1] \from \nothing;
@@ -505,7 +504,7 @@ void nested_chars(char (*dest)[10])
ensures
set_content:
\let __fc_len = \old(len) / 4;
- ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ -2147483648;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ ~((int)0);
ensures result: \result ≡ \old(ptr);
assigns *(ptr + (0 .. len / 4 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
@@ -584,7 +583,7 @@ void unsigned_integer(unsigned int *dest)
ensures
set_content:
\let __fc_len = \old(len) / 4;
- ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ -2147483648;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ ~((long)0);
ensures result: \result ≡ \old(ptr);
assigns *(ptr + (0 .. len / 4 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
@@ -638,7 +637,7 @@ void unsigned_long_integer(unsigned long *dest)
set_content:
\let __fc_len = \old(len) / 8;
∀ ℤ j0;
- 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ -9223372036854775808;
+ 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ ~((long long)0);
ensures result: \result ≡ \old(ptr);
assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
@@ -728,8 +727,8 @@ void with_named(named *dest)
\let __fc_len = \old(len) / 8;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
- (\old(ptr) + j0)->x ≡ -2147483648 ∧
- (\old(ptr) + j0)->y ≡ -2147483648;
+ (\old(ptr) + j0)->x ≡ ~((int)0) ∧
+ (\old(ptr) + j0)->y ≡ ~((int)0);
ensures result: \result ≡ \old(ptr);
assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
@@ -784,7 +783,7 @@ void pointers(int **dest)
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1;
- 0 ≤ j1 < 10 ⇒ (*(\old(ptr) + j0))[j1] ≡ -2147483648);
+ 0 ≤ j1 < 10 ⇒ (*(\old(ptr) + j0))[j1] ≡ ~((int)0));
ensures result: \result ≡ \old(ptr);
assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1], \result;
assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1] \from \nothing;
--
GitLab