From 753c8a1df080f5487b01a09cd388b68ff88e4c47 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 15 Jun 2021 17:02:02 +0200
Subject: [PATCH] [Logic] avoid crashes due to large integers or invalid digits
in literal
---
.../ast_queries/logic_typing.ml | 6 ++++-
.../ast_queries/logic_utils.ml | 10 +++++++-
.../oracle/very_large_integers.0.res.oracle | 8 +++---
.../oracle/very_large_integers.1.res.oracle | 8 +++---
.../oracle/very_large_integers.10.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 | 12 ++++-----
.../oracle/very_large_integers.5.res.oracle | 6 ++---
.../oracle/very_large_integers.6.res.oracle | 6 ++---
.../oracle/very_large_integers.7.res.oracle | 8 +++---
.../oracle/very_large_integers.8.res.oracle | 25 ++++++-------------
.../oracle/very_large_integers.9.res.oracle | 12 +++++++++
tests/syntax/very_large_integers.c | 12 +++++++++
14 files changed, 93 insertions(+), 48 deletions(-)
create mode 100644 tests/syntax/oracle/very_large_integers.10.res.oracle
create mode 100644 tests/syntax/oracle/very_large_integers.9.res.oracle
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 44868650b2f..9ba74c01385 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -880,7 +880,11 @@ struct
let tokens = explode content in
let value,_= Cil.interpret_character_constant tokens in
term ~loc (TConst (constant_to_lconstant value)) Linteger
- | _ -> Cil.parseIntLogic ~loc s
+ | _ ->
+ try
+ Cil.parseIntLogic ~loc s
+ with Cil.ParseIntError msg ->
+ Kernel.fatal ~source:(fst loc) "%s" msg
let find_logic_label loc env l =
try Lenv.find_logic_label l env
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index e568ddfc6aa..6cc3eae4743 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -275,7 +275,15 @@ let constant_to_lconstant c = match c with
LReal (real_of_float s f)
let lconstant_to_constant c = match c with
- | Integer (i,s) -> CInt64(i,Cil.intKindForValue i false,s)
+ | Integer (i,s) ->
+ begin
+ try
+ CInt64(i,Cil.intKindForValue i false,s)
+ with Cil.Not_representable ->
+ Kernel.fatal
+ "Cannot represent logical integer in C: %a"
+ (Integer.pretty ~hexa:false) i
+ end
| LStr s -> CStr s
| LWStr s -> CWStr s
| LChr s -> CChr s
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index d7175f1e68f..64ae83250fe 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:18: User Error:
+[kernel] tests/syntax/very_large_integers.c:21: User Error:
integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
-[kernel] tests/syntax/very_large_integers.c:19: User Error:
+[kernel] tests/syntax/very_large_integers.c:22: User Error:
bitfield width is not a valid integer constant
-[kernel] tests/syntax/very_large_integers.c:53: Warning:
+[kernel] tests/syntax/very_large_integers.c:57: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:53: Warning:
+[kernel] tests/syntax/very_large_integers.c:57: 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 43f59ecb36a..4c65204b2fa 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:25: User Error:
+[kernel] tests/syntax/very_large_integers.c:28: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:25: User Error:
+[kernel] tests/syntax/very_large_integers.c:28: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:53: Warning:
+[kernel] tests/syntax/very_large_integers.c:57: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:53: Warning:
+[kernel] tests/syntax/very_large_integers.c:57: 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
new file mode 100644
index 00000000000..a1176c2d521
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.10.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:57: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] tests/syntax/very_large_integers.c:57: Warning:
+ ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+ (9223372036854775808) )
+[kernel] tests/syntax/very_large_integers.c:85: 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 c21f3361baa..2c763bf0674 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:31: User Error:
+[kernel] tests/syntax/very_large_integers.c:35: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:31: Failure:
+[kernel] tests/syntax/very_large_integers.c:35: 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 39820b9d4cd..ac927237baf 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 tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:36: Failure:
+[kernel] tests/syntax/very_large_integers.c:40: 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.
diff --git a/tests/syntax/oracle/very_large_integers.4.res.oracle b/tests/syntax/oracle/very_large_integers.4.res.oracle
index d93cd65fdee..403d2a65c2f 100644
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -1,12 +1,12 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:40: User Error:
+[kernel] tests/syntax/very_large_integers.c:44: User Error:
INDEX initialization designator overflows
- 38
- 39 #ifdef INIT_DESIGNATOR2
- 40 int arr3[1] = { [9999999999999999999U] = 42 };
+ 42
+ 43 #ifdef INIT_DESIGNATOR2
+ 44 int arr3[1] = { [9999999999999999999U] = 42 };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 41 #endif
- 42
+ 45 #endif
+ 46
[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 1de406bf2a6..46e43a1bedb 100644
--- a/tests/syntax/oracle/very_large_integers.5.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.5.res.oracle
@@ -1,9 +1,9 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:44: User Error:
+[kernel] tests/syntax/very_large_integers.c:48: User Error:
integer constant too large in expression -9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:44: User Error:
+[kernel] tests/syntax/very_large_integers.c:48: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:44: Failure:
+[kernel] tests/syntax/very_large_integers.c:48: 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.
diff --git a/tests/syntax/oracle/very_large_integers.6.res.oracle b/tests/syntax/oracle/very_large_integers.6.res.oracle
index 2518a170b6f..45af4ca2032 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 tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:48: User Error:
+[kernel] tests/syntax/very_large_integers.c:52: User Error:
Invalid attribute constant: 0x80000000000000000
-[kernel] tests/syntax/very_large_integers.c:53: Warning:
+[kernel] tests/syntax/very_large_integers.c:57: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:53: Warning:
+[kernel] tests/syntax/very_large_integers.c:57: 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.7.res.oracle b/tests/syntax/oracle/very_large_integers.7.res.oracle
index 18a61c34997..e34bb47c39d 100644
--- a/tests/syntax/oracle/very_large_integers.7.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.7.res.oracle
@@ -1,12 +1,10 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:53: Warning:
+[kernel] tests/syntax/very_large_integers.c:57: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:53: Warning:
+[kernel] tests/syntax/very_large_integers.c:57: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel:annot-error] tests/syntax/very_large_integers.c:67: Warning:
- Invalid slevel directive. Ignoring code annotation
-[kernel] User Error: warning annot-error treated as fatal error.
+[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 9d4810ae444..0f63c2ee5d2 100644
--- a/tests/syntax/oracle/very_large_integers.8.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.8.res.oracle
@@ -1,22 +1,11 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:53: Warning:
+[kernel] tests/syntax/very_large_integers.c:57: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:53: Warning:
+[kernel] tests/syntax/very_large_integers.c:57: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:73: 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:70: 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/oracle/very_large_integers.9.res.oracle b/tests/syntax/oracle/very_large_integers.9.res.oracle
new file mode 100644
index 00000000000..95d122b7737
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.9.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:57: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] tests/syntax/very_large_integers.c:57: Warning:
+ ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+ (9223372036854775808) )
+[kernel:annot-error] tests/syntax/very_large_integers.c:79: 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/very_large_integers.c b/tests/syntax/very_large_integers.c
index 4831ada7bc1..48dff8b8376 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -8,10 +8,13 @@
STDOPT: #"-cpp-extra-args=-DINIT_DESIGNATOR2"
STDOPT: #"-cpp-extra-args=-DRANGE_DESIGNATOR"
STDOPT: #"-cpp-extra-args=-DATTRIBUTE_CONSTANT"
+ STDOPT: #"-cpp-extra-args=-DLOGIC_CONSTANT"
+ STDOPT: #"-cpp-extra-args=-DLOGIC_CONSTANT_OCTAL"
STDOPT: #"-cpp-extra-args=-DEVA_UNROLL -eva"
EXIT: 0
STDOPT: #"-cpp-extra-args=-DUNROLL_PRAGMA"
*/
+
volatile int nondet;
#ifdef BITFIELD
@@ -24,6 +27,7 @@ struct st {
int arr[9999999999999999999U+18000000000000000000U];
char arr1[99999999999999999999U];
#endif
+
#ifdef CASE_RANGE
unsigned long nondetul;
void case_range() {
@@ -58,6 +62,14 @@ typedef struct {
//@ logic integer too_large_integer = 9999999999999999999;
+#ifdef LOGIC_CONSTANT
+//@ type too_large_logic_array = int[9999999999999999999U];
+#endif
+
+#ifdef LOGIC_CONSTANT_OCTAL
+//@ type too_large_logic_array_octal = int[09876543210];
+#endif
+
int main() {
#ifdef EVA_UNROLL
//@ loop unroll (-9999999999999999999); // IntLimit
--
GitLab