From 83d5e25f8d05ad6c44d039dce318a6a301f6049e Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 10 Jan 2022 16:15:13 +0100
Subject: [PATCH] [Cabs2cil] avoid crash with overly large array initializers
---
src/kernel_internals/typing/cabs2cil.ml | 8 +++++-
.../oracle/very_large_integers.0.res.oracle | 8 +++---
.../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 | 25 ++++++-------------
.../oracle/very_large_integers.14.res.oracle | 11 ++++++++
.../oracle/very_large_integers.15.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 | 20 +++++++++++++++
18 files changed, 105 insertions(+), 57 deletions(-)
create mode 100644 tests/syntax/oracle/very_large_integers.14.res.oracle
create mode 100644 tests/syntax/oracle/very_large_integers.15.res.oracle
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 06d74aa1d67..5debe483a4b 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3384,7 +3384,13 @@ let rec setOneInit this o preinit =
let pMaxIdx, pArray =
match this with
| NoInitPre -> (* No initializer so far here *)
- ref idx, ref (Array.make (max 32 (idx + 1)) NoInitPre)
+ begin
+ try
+ ref idx, ref (Array.make (max 32 (idx + 1)) NoInitPre)
+ with Invalid_argument _ | Out_of_memory ->
+ Kernel.abort ~current:true
+ "array length too large: %d" ((max 32 (idx + 1)))
+ end
| CompoundPre (pMaxIdx, pArray) ->
if !pMaxIdx < idx then begin
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index db47193a76d..070b0b0891f 100644
--- a/tests/syntax/oracle/very_large_integers.0.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.0.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:23: User Error:
+[kernel] very_large_integers.c:25: User Error:
integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
-[kernel] very_large_integers.c:24: User Error:
+[kernel] very_large_integers.c:26: User Error:
bitfield width is not a valid integer constant
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: 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.1.res.oracle b/tests/syntax/oracle/very_large_integers.1.res.oracle
index 307887ca5d2..0ceeff36ccd 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:30: User Error:
+[kernel] very_large_integers.c:32: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] very_large_integers.c:30: User Error:
+[kernel] very_large_integers.c:32: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: 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 12b104249f7..468e5fb2083 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:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:85: Failure:
+[kernel] very_large_integers.c:87: 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 47557942111..c0fab3ffc41 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:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel:annot-error] very_large_integers.c:94: Warning:
+[kernel:annot-error] very_large_integers.c:114: 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:91: Warning:
+[kernel:annot-error] very_large_integers.c:111: Warning:
invalid loop unrolling parameter; ignoring
-[kernel:annot-error] very_large_integers.c:93: Warning:
+[kernel:annot-error] very_large_integers.c:113: 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 bfe4d557fd5..71f4141e2fe 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:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:98: User Error:
+[kernel] very_large_integers.c:118: 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 2ae16ad88a3..3d0eb837dc4 100644
--- a/tests/syntax/oracle/very_large_integers.13.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.13.res.oracle
@@ -1,22 +1,11 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:103: 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:92: 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.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.14.res.oracle b/tests/syntax/oracle/very_large_integers.14.res.oracle
new file mode 100644
index 00000000000..d404452dfd8
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.14.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing very_large_integers.c (with preprocessing)
+[kernel] very_large_integers.c:74: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] very_large_integers.c:74: Warning:
+ ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+ (9223372036854775808) )
+[kernel] very_large_integers.c:103: 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.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.15.res.oracle b/tests/syntax/oracle/very_large_integers.15.res.oracle
new file mode 100644
index 00000000000..dc363357b8e
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.15.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing very_large_integers.c (with preprocessing)
+[kernel] very_large_integers.c:74: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] very_large_integers.c:74: 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;
+}
+
+
diff --git a/tests/syntax/oracle/very_large_integers.2.res.oracle b/tests/syntax/oracle/very_large_integers.2.res.oracle
index e66ed159168..1b640275031 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:37: User Error:
+[kernel] very_large_integers.c:39: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] very_large_integers.c:37: Failure:
+[kernel] very_large_integers.c:39: 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 e98fe85d7ff..09f3e166f6f 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:45: Failure: Case range too large
+[kernel] very_large_integers.c:47: 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 5af290bef31..817f524174f 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:50: Failure:
+[kernel] very_large_integers.c:52: Failure:
Array length 9999999999999999999U is not a compile-time constant: 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 5dbd30727bd..e38af09ec48 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:54: User Error:
+[kernel] very_large_integers.c:56: User Error:
INDEX initialization designator overflows
- 52
- 53 #ifdef INIT_DESIGNATOR2
- 54 int arr3[1] = { [9999999999999999999U] = 42 };
+ 54
+ 55 #ifdef INIT_DESIGNATOR2
+ 56 int arr3[1] = { [9999999999999999999U] = 42 };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 55 #endif
- 56
+ 57 #endif
+ 58
[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 8b2be7f122e..dd10e931b3a 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:58: User Error:
+[kernel] very_large_integers.c:60: User Error:
integer constant too large in expression -9999999999999999999U
-[kernel] very_large_integers.c:58: User Error:
+[kernel] very_large_integers.c:60: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] very_large_integers.c:58: Failure:
+[kernel] very_large_integers.c:60: 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 90e6c755d45..406e636f462 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:62: Failure: INDEX_RANGE too large
+[kernel] very_large_integers.c:64: 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 5eae6db9af1..8de4f1b1a65 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:67: User Error:
+[kernel] very_large_integers.c:69: User Error:
Invalid attribute constant: 0x80000000000000000
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: 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 e1237274ec9..fb843772ce7 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:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: 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 5e31b993a90..996c0ca0bf0 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -14,6 +14,8 @@
STDOPT: #"-cpp-extra-args=-DLOGIC_CONSTANT_OCTAL"
STDOPT: #"-cpp-extra-args=-DEVA_UNROLL -eva -kernel-warn-key annot-error=error"
STDOPT: #"-cpp-extra-args=-DCABS_DOWHILE"
+ STDOPT: #"-cpp-extra-args=-DARRAY_INIT1"
+ STDOPT: #"-cpp-extra-args=-DARRAY_INIT2"
EXIT: 0
STDOPT: #"-cpp-extra-args=-DUNROLL_PRAGMA"
*/
@@ -85,6 +87,24 @@ typedef struct {
//@ type too_large_logic_array_octal = int[09876543210];
#endif
+#ifdef ARRAY_INIT1
+// Previously caused Invalid_argument(Array.make)
+int a1[] = {[72057594037927936] = 0};
+#endif
+
+#ifdef ARRAY_INIT2
+struct arri2 {
+ int a[7205759403792795];
+};
+struct st {
+ struct arri2 a;
+};
+// Previously caused Out of memory
+struct st s = {
+ {{[7205759403792793 ... 7205759403792793] = 0}}
+};
+#endif
+
int main() {
#ifdef EVA_UNROLL
//@ loop unroll (-9999999999999999999); // IntLimit
--
GitLab