From 47c2f19da719de1ccff7a59e80193f64be4e3cc6 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 12 Oct 2021 22:06:02 +0200
Subject: [PATCH] [Cabs2cil] avoid stack overflow with large switch case ranges
---
src/kernel_internals/typing/cabs2cil.ml | 6 ++++-
.../oracle/very_large_integers.0.res.oracle | 8 +++---
.../oracle/very_large_integers.1.res.oracle | 8 +++---
.../oracle/very_large_integers.10.res.oracle | 15 ++++++-----
.../oracle/very_large_integers.11.res.oracle | 9 ++++---
.../oracle/very_large_integers.12.res.oracle | 25 ++++++-------------
.../oracle/very_large_integers.13.res.oracle | 22 ++++++++++++++++
.../oracle/very_large_integers.2.res.oracle | 4 +--
.../oracle/very_large_integers.3.res.oracle | 3 +--
.../oracle/very_large_integers.4.res.oracle | 10 ++------
.../oracle/very_large_integers.5.res.oracle | 14 ++++++-----
.../oracle/very_large_integers.6.res.oracle | 13 +++++-----
.../oracle/very_large_integers.7.res.oracle | 7 +++---
.../oracle/very_large_integers.8.res.oracle | 7 +++---
.../oracle/very_large_integers.9.res.oracle | 16 +++++-------
tests/syntax/very_large_integers.c | 9 +++++++
16 files changed, 97 insertions(+), 79 deletions(-)
create mode 100644 tests/syntax/oracle/very_large_integers.13.res.oracle
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 75665dec063..b5b1e8e6c8f 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -10104,7 +10104,11 @@ and doStatement local_env (s : Cabs.statement) : chunk =
in
if il > ih then Kernel.error ~once:true ~current:true "Empty case range";
let rec mkAll (i: int) =
- if i > ih then [] else integer ~loc i :: mkAll (i + 1)
+ if i > ih then [] else
+ if ih - i > 100_000 then
+ Kernel.fatal ~current:true "Case range too large"
+ else
+ integer ~loc i :: mkAll (i + 1)
in
(sel @@ (seh,ghost)) @@
(caseRangeChunk ~ghost (mkAll il) loc' (doStatement local_env s),
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index db573af932d..1cba593f0dc 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 tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:22: User Error:
- integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
[kernel] tests/syntax/very_large_integers.c:23: User Error:
+ integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
+[kernel] tests/syntax/very_large_integers.c:24: User Error:
bitfield width is not a valid integer constant
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] User Error: stopping on file "tests/syntax/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 23cfa866c0b..29f4d99b928 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 tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:29: User Error:
+[kernel] tests/syntax/very_large_integers.c:30: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:29: User Error:
+[kernel] tests/syntax/very_large_integers.c:30: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] User Error: stopping on file "tests/syntax/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 b3e0404db43..b9200fafcf7 100644
--- a/tests/syntax/oracle/very_large_integers.10.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.10.res.oracle
@@ -1,12 +1,15 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel:annot-error] tests/syntax/very_large_integers.c:82: 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] tests/syntax/very_large_integers.c:86: Warning:
+ invalid loop unrolling parameter (-9999999999999999999); ignoring
[kernel] User Error: warning annot-error treated as fatal error.
-[kernel] User Error: stopping on file "tests/syntax/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.11.res.oracle b/tests/syntax/oracle/very_large_integers.11.res.oracle
index bb2ebf80688..650607ffad8 100644
--- a/tests/syntax/oracle/very_large_integers.11.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.11.res.oracle
@@ -1,11 +1,12 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:86: User Error:
- Invalid digit 9 in integer literal '09' in base 8.
+[kernel:annot-error] tests/syntax/very_large_integers.c:91: Warning:
+ Invalid slevel directive. Ignoring code annotation
+[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "tests/syntax/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.12.res.oracle b/tests/syntax/oracle/very_large_integers.12.res.oracle
index db0893a7e07..ba0dd7c26f2 100644
--- a/tests/syntax/oracle/very_large_integers.12.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.12.res.oracle
@@ -1,22 +1,11 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:91: 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] tests/syntax/very_large_integers.c:95: User Error:
+ Invalid digit 9 in integer literal '09' in base 8.
+[kernel] User Error: stopping on file "tests/syntax/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.13.res.oracle b/tests/syntax/oracle/very_large_integers.13.res.oracle
new file mode 100644
index 00000000000..29b15f32902
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.13.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
+ ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+ (9223372036854775808) )
+[kernel] tests/syntax/very_large_integers.c:100: 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 bb5f47fe756..25740fed33d 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 tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:36: User Error:
+[kernel] tests/syntax/very_large_integers.c:37: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:36: Failure:
+[kernel] tests/syntax/very_large_integers.c:37: Failure:
Cannot understand the constants in case range
[kernel] User Error: stopping on file "tests/syntax/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 ad9de534b05..f4cbe4f4e6d 100644
--- a/tests/syntax/oracle/very_large_integers.3.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.3.res.oracle
@@ -1,6 +1,5 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:41: Failure:
- Array length 9999999999999999999U is not a compile-time constant: no explicit initializer allowed.
+[kernel] tests/syntax/very_large_integers.c:45: Failure: Case range too large
[kernel] User Error: stopping on file "tests/syntax/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 0d8599e3295..e53651c2f5b 100644
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -1,12 +1,6 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:45: User Error:
- INDEX initialization designator overflows
- 43
- 44 #ifdef INIT_DESIGNATOR2
- 45 int arr3[1] = { [9999999999999999999U] = 42 };
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 46 #endif
- 47
+[kernel] tests/syntax/very_large_integers.c:50: Failure:
+ Array length 9999999999999999999U is not a compile-time constant: no explicit initializer allowed.
[kernel] User Error: stopping on file "tests/syntax/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.5.res.oracle b/tests/syntax/oracle/very_large_integers.5.res.oracle
index 1798bfe46e3..028afa06f27 100644
--- a/tests/syntax/oracle/very_large_integers.5.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.5.res.oracle
@@ -1,10 +1,12 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:49: User Error:
- integer constant too large in expression -9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:49: User Error:
- integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:49: Failure:
- INDEX_RANGE initialization designator is not a valid constant
+[kernel] tests/syntax/very_large_integers.c:54: User Error:
+ INDEX initialization designator overflows
+ 52
+ 53 #ifdef INIT_DESIGNATOR2
+ 54 int arr3[1] = { [9999999999999999999U] = 42 };
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 55 #endif
+ 56
[kernel] User Error: stopping on file "tests/syntax/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 c531dfb15a1..80ea4f9cf53 100644
--- a/tests/syntax/oracle/very_large_integers.6.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.6.res.oracle
@@ -1,11 +1,10 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:53: User Error:
- Invalid attribute constant: 0x80000000000000000
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
- ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
- ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
- (9223372036854775808) )
+[kernel] tests/syntax/very_large_integers.c:58: User Error:
+ integer constant too large in expression -9999999999999999999U
+[kernel] tests/syntax/very_large_integers.c:58: User Error:
+ integer constant too large in expression 9999999999999999999U
+[kernel] tests/syntax/very_large_integers.c:58: Failure:
+ INDEX_RANGE initialization designator is not a valid constant
[kernel] User Error: stopping on file "tests/syntax/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.7.res.oracle b/tests/syntax/oracle/very_large_integers.7.res.oracle
index 75dbebc66e6..c998aaf5b33 100644
--- a/tests/syntax/oracle/very_large_integers.7.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.7.res.oracle
@@ -1,10 +1,11 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:62: User Error:
+ Invalid attribute constant: 0x80000000000000000
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] Failure: Cannot represent logical integer in C: 9999999999999999999
[kernel] User Error: stopping on file "tests/syntax/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 a0898661e14..1028d33119a 100644
--- a/tests/syntax/oracle/very_large_integers.8.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.8.res.oracle
@@ -1,11 +1,10 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:71: Failure:
- Invalid digit 9 in integer literal '09876543210' in base 8.
+[kernel] Failure: Cannot represent logical integer in C: 9999999999999999999
[kernel] User Error: stopping on file "tests/syntax/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.9.res.oracle b/tests/syntax/oracle/very_large_integers.9.res.oracle
index 3c17088f959..bcf3568e2a8 100644
--- a/tests/syntax/oracle/very_large_integers.9.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.9.res.oracle
@@ -1,15 +1,11 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[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] tests/syntax/very_large_integers.c:77: Warning:
- invalid loop unrolling parameter (-9999999999999999999); ignoring
-[kernel] User Error: warning annot-error treated as fatal error.
+[kernel] tests/syntax/very_large_integers.c:80: Failure:
+ Invalid digit 9 in integer literal '09876543210' in base 8.
+[kernel] User Error: stopping on file "tests/syntax/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/very_large_integers.c b/tests/syntax/very_large_integers.c
index 8cb37536c37..47c3629e67c 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -4,6 +4,7 @@
STDOPT: #"-cpp-extra-args=-DBITFIELD"
STDOPT: #"-cpp-extra-args=-DARRAY_DECL"
STDOPT: #"-cpp-extra-args=-DCASE_RANGE"
+ STDOPT: #"-cpp-extra-args=-DCASE_RANGE2"
STDOPT: #"-cpp-extra-args=-DINIT_DESIGNATOR"
STDOPT: #"-cpp-extra-args=-DINIT_DESIGNATOR2"
STDOPT: #"-cpp-extra-args=-DRANGE_DESIGNATOR"
@@ -34,6 +35,14 @@ unsigned long nondetul;
void case_range() {
switch (nondetul)
case 0 ... 9999999999999999999U:;
+ case 0 ... 199999999999999999U:;
+}
+#endif
+
+#ifdef CASE_RANGE2
+void case_range() {
+ switch (nondet)
+ case 0 ... 10000000U:;
}
#endif
--
GitLab