From 0a7b6097eeb0fc6e7835d9fba6f4977962bbfcf3 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 24 Jan 2022 09:20:29 +0100
Subject: [PATCH] [Cabs2cil] avoid more crashes due to large array initializer
Note: trying to compile the initializer with gcc/CompCert likely results in
'no space left on device'. Clang 12 reports an unexpected warning
("initializer overrides prior initialization of this subobject"), and some
tests indicate it actually replaces index 72057594037927936 with 0, which would
explain why it compiles. Removing a digit from the index, for instance, results
in a similar issue as GCC/CompCert (except that Clang starts consuming all RAM
instead of simply disk space).
---
src/kernel_internals/typing/cabs2cil.ml | 10 +++++---
.../oracle/very_large_integers.0.res.oracle | 4 +--
.../oracle/very_large_integers.1.res.oracle | 8 +++---
.../oracle/very_large_integers.10.res.oracle | 6 ++---
.../oracle/very_large_integers.11.res.oracle | 10 ++++----
.../oracle/very_large_integers.12.res.oracle | 6 ++---
.../oracle/very_large_integers.13.res.oracle | 6 ++---
.../oracle/very_large_integers.14.res.oracle | 6 ++---
.../oracle/very_large_integers.15.res.oracle | 25 ++++++-------------
.../oracle/very_large_integers.16.res.oracle | 11 ++++++++
.../oracle/very_large_integers.17.res.oracle | 22 ++++++++++++++++
.../oracle/very_large_integers.2.res.oracle | 4 +--
.../oracle/very_large_integers.3.res.oracle | 2 +-
.../oracle/very_large_integers.4.res.oracle | 2 +-
.../oracle/very_large_integers.5.res.oracle | 12 ++++-----
.../oracle/very_large_integers.6.res.oracle | 6 ++---
.../oracle/very_large_integers.7.res.oracle | 2 +-
.../oracle/very_large_integers.8.res.oracle | 6 ++---
.../oracle/very_large_integers.9.res.oracle | 4 +--
tests/syntax/very_large_integers.c | 18 +++++++++++++
20 files changed, 107 insertions(+), 63 deletions(-)
create mode 100644 tests/syntax/oracle/very_large_integers.16.res.oracle
create mode 100644 tests/syntax/oracle/very_large_integers.17.res.oracle
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index f6aebe306d4..f958082d4b0 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3399,9 +3399,13 @@ let rec setOneInit this o preinit =
let l = Array.length !pArray in
if l <= idx then begin
let growBy = max (max 32 (idx + 1 - l)) (l / 2) in
- let newarray = Array.make (growBy + idx) NoInitPre in
- Array.blit !pArray 0 newarray 0 l;
- pArray := newarray
+ try
+ let newarray = Array.make (growBy + idx) NoInitPre in
+ Array.blit !pArray 0 newarray 0 l;
+ pArray := newarray
+ with Invalid_argument _ | Out_of_memory ->
+ Kernel.abort ~current:true
+ "array length too large for Frama-C: %d" (idx)
end
end;
pMaxIdx, pArray
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index 1236cc7d725..aadc000d33d 100644
--- a/tests/syntax/oracle/very_large_integers.0.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.0.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:25: User Error:
+[kernel] very_large_integers.c:35: User Error:
integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
-[kernel] very_large_integers.c:26: User Error:
+[kernel] very_large_integers.c:36: User Error:
bitfield width is not a valid integer constant
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/very_large_integers.1.res.oracle b/tests/syntax/oracle/very_large_integers.1.res.oracle
index 0ceeff36ccd..4f4479d8509 100644
--- a/tests/syntax/oracle/very_large_integers.1.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.1.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:32: User Error:
+[kernel] very_large_integers.c:42: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] very_large_integers.c:32: User Error:
+[kernel] very_large_integers.c:42: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
diff --git a/tests/syntax/oracle/very_large_integers.10.res.oracle b/tests/syntax/oracle/very_large_integers.10.res.oracle
index 468e5fb2083..b40b28536c4 100644
--- a/tests/syntax/oracle/very_large_integers.10.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.10.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:87: Failure:
+[kernel] very_large_integers.c:97: Failure:
Invalid digit 9 in integer literal '09876543210' in base 8.
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/very_large_integers.11.res.oracle b/tests/syntax/oracle/very_large_integers.11.res.oracle
index c0fab3ffc41..26c3f665eca 100644
--- a/tests/syntax/oracle/very_large_integers.11.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.11.res.oracle
@@ -1,19 +1,19 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel:annot-error] very_large_integers.c:114: Warning:
+[kernel:annot-error] very_large_integers.c:132: Warning:
Invalid slevel directive. Ignoring code annotation
[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 ∈ [--..--]
-[kernel:annot-error] very_large_integers.c:111: Warning:
+[kernel:annot-error] very_large_integers.c:129: Warning:
invalid loop unrolling parameter; ignoring
-[kernel:annot-error] very_large_integers.c:113: Warning:
+[kernel:annot-error] very_large_integers.c:131: Warning:
invalid loop unrolling parameter; ignoring
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/syntax/oracle/very_large_integers.12.res.oracle b/tests/syntax/oracle/very_large_integers.12.res.oracle
index 71f4141e2fe..8b9b72707ec 100644
--- a/tests/syntax/oracle/very_large_integers.12.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.12.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:118: User Error:
+[kernel] very_large_integers.c:136: User Error:
Invalid digit 9 in integer literal '09' in base 8.
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/very_large_integers.13.res.oracle b/tests/syntax/oracle/very_large_integers.13.res.oracle
index 3d0eb837dc4..3a4a0c0b838 100644
--- a/tests/syntax/oracle/very_large_integers.13.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.13.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:92: User Error:
+[kernel] very_large_integers.c:102: User Error:
array length too large: 72057594037927937
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/very_large_integers.14.res.oracle b/tests/syntax/oracle/very_large_integers.14.res.oracle
index d404452dfd8..8d7684b496f 100644
--- a/tests/syntax/oracle/very_large_integers.14.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.14.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:103: User Error:
+[kernel] very_large_integers.c:113: User Error:
array length too large: 7205759403792794
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/very_large_integers.15.res.oracle b/tests/syntax/oracle/very_large_integers.15.res.oracle
index dc363357b8e..adad5046822 100644
--- a/tests/syntax/oracle/very_large_integers.15.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.15.res.oracle
@@ -1,22 +1,11 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:123: Warning:
- ignoring unrolling directive (not an understood constant expression)
-/* Generated by Frama-C */
-int volatile nondet;
-/*@ logic ℤ too_large_integer= 9999999999999999999;
- */
-int main(void)
-{
- int __retres;
- /*@ loop pragma UNROLL 99999999999999999999; */
- while (nondet) ;
- __retres = 0;
- return __retres;
-}
-
-
+[kernel] very_large_integers.c:119: User Error:
+ array length too large for Frama-C: 72057594037927936
+[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.16.res.oracle b/tests/syntax/oracle/very_large_integers.16.res.oracle
new file mode 100644
index 00000000000..1d8fc3c7d7c
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.16.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing very_large_integers.c (with preprocessing)
+[kernel] very_large_integers.c:84: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] very_large_integers.c:84: Warning:
+ ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+ (9223372036854775808) )
+[kernel] very_large_integers.c:123: User Error:
+ array length too large for Frama-C: 7205759403792793
+[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.17.res.oracle b/tests/syntax/oracle/very_large_integers.17.res.oracle
new file mode 100644
index 00000000000..3012ddb57d4
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.17.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing very_large_integers.c (with preprocessing)
+[kernel] very_large_integers.c:84: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] very_large_integers.c:84: Warning:
+ ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+ (9223372036854775808) )
+[kernel] very_large_integers.c:141: Warning:
+ ignoring unrolling directive (not an understood constant expression)
+/* Generated by Frama-C */
+int volatile nondet;
+/*@ logic ℤ too_large_integer= 9999999999999999999;
+ */
+int main(void)
+{
+ int __retres;
+ /*@ loop pragma UNROLL 99999999999999999999; */
+ while (nondet) ;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/very_large_integers.2.res.oracle b/tests/syntax/oracle/very_large_integers.2.res.oracle
index 1b640275031..851e81eb034 100644
--- a/tests/syntax/oracle/very_large_integers.2.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.2.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:39: User Error:
+[kernel] very_large_integers.c:49: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] very_large_integers.c:39: Failure:
+[kernel] very_large_integers.c:49: Failure:
Cannot understand the constants in case range
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/very_large_integers.3.res.oracle b/tests/syntax/oracle/very_large_integers.3.res.oracle
index 09f3e166f6f..b46e1c5c2cd 100644
--- a/tests/syntax/oracle/very_large_integers.3.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.3.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:47: Failure: Case range too large
+[kernel] very_large_integers.c:57: Failure: Case range too large
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.4.res.oracle b/tests/syntax/oracle/very_large_integers.4.res.oracle
index b4a00ef7aed..5e6c8b87f51 100644
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:52: User Error:
+[kernel] very_large_integers.c:62: User Error:
Array length 9999999999999999999U is too big: no explicit initializer allowed.
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/very_large_integers.5.res.oracle b/tests/syntax/oracle/very_large_integers.5.res.oracle
index e38af09ec48..4d011e9d844 100644
--- a/tests/syntax/oracle/very_large_integers.5.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.5.res.oracle
@@ -1,12 +1,12 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:56: User Error:
+[kernel] very_large_integers.c:66: User Error:
INDEX initialization designator overflows
- 54
- 55 #ifdef INIT_DESIGNATOR2
- 56 int arr3[1] = { [9999999999999999999U] = 42 };
+ 64
+ 65 #ifdef INIT_DESIGNATOR2
+ 66 int arr3[1] = { [9999999999999999999U] = 42 };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 57 #endif
- 58
+ 67 #endif
+ 68
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.6.res.oracle b/tests/syntax/oracle/very_large_integers.6.res.oracle
index dd10e931b3a..c603644b586 100644
--- a/tests/syntax/oracle/very_large_integers.6.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.6.res.oracle
@@ -1,9 +1,9 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:60: User Error:
+[kernel] very_large_integers.c:70: User Error:
integer constant too large in expression -9999999999999999999U
-[kernel] very_large_integers.c:60: User Error:
+[kernel] very_large_integers.c:70: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] very_large_integers.c:60: Failure:
+[kernel] very_large_integers.c:70: Failure:
INDEX_RANGE initialization designator is not a valid constant
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/very_large_integers.7.res.oracle b/tests/syntax/oracle/very_large_integers.7.res.oracle
index 406e636f462..5ca8f61644c 100644
--- a/tests/syntax/oracle/very_large_integers.7.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.7.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:64: Failure: INDEX_RANGE too large
+[kernel] very_large_integers.c:74: Failure: INDEX_RANGE too large
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.8.res.oracle b/tests/syntax/oracle/very_large_integers.8.res.oracle
index 8de4f1b1a65..bf9a0960534 100644
--- a/tests/syntax/oracle/very_large_integers.8.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.8.res.oracle
@@ -1,9 +1,9 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:69: User Error:
+[kernel] very_large_integers.c:79: User Error:
Invalid attribute constant: 0x80000000000000000
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
diff --git a/tests/syntax/oracle/very_large_integers.9.res.oracle b/tests/syntax/oracle/very_large_integers.9.res.oracle
index fb843772ce7..2c2a6cbdf3a 100644
--- a/tests/syntax/oracle/very_large_integers.9.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.9.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] Failure: Cannot represent logical integer in C: 9999999999999999999
diff --git a/tests/syntax/very_large_integers.c b/tests/syntax/very_large_integers.c
index 996c0ca0bf0..02f67ae7560 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -16,10 +16,20 @@
STDOPT: #"-cpp-extra-args=-DCABS_DOWHILE"
STDOPT: #"-cpp-extra-args=-DARRAY_INIT1"
STDOPT: #"-cpp-extra-args=-DARRAY_INIT2"
+ STDOPT: #"-cpp-extra-args=-DARRAY_INIT3"
+ STDOPT: #"-cpp-extra-args=-DARRAY_INIT4"
EXIT: 0
STDOPT: #"-cpp-extra-args=-DUNROLL_PRAGMA"
*/
+
+
+
+
+
+
+// Lines intentionally left blank to minimize future oracle changes
+
volatile int nondet;
#ifdef BITFIELD
struct st {
@@ -105,6 +115,14 @@ struct st s = {
};
#endif
+#ifdef ARRAY_INIT3
+int ai3[] = {0xdead, [72057594037927936] = 0xbeef};
+#endif
+#ifdef ARRAY_INIT4
+// Previously caused Out of memory
+int ai4[] = {1, [7205759403792793] = 11};
+#endif
+
int main() {
#ifdef EVA_UNROLL
//@ loop unroll (-9999999999999999999); // IntLimit
--
GitLab