From 9bf4fca19bc6da920f37abd9344fe3226e22a333 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 6 Sep 2023 10:49:29 +0200
Subject: [PATCH] [kernel] avoid crash on ill-typed multiplicative operators +
more tests
---
src/kernel_internals/typing/cabs2cil.ml | 19 ++++++++++-------
tests/syntax/binary_op.c | 24 ++++++++++++++++++++++
tests/syntax/binary_op.i | 6 ------
tests/syntax/oracle/binary_op.0.res.oracle | 10 +++++++++
tests/syntax/oracle/binary_op.1.res.oracle | 10 +++++++++
tests/syntax/oracle/binary_op.2.res.oracle | 3 +++
tests/syntax/oracle/binary_op.3.res.oracle | 1 +
tests/syntax/oracle/binary_op.res.oracle | 8 --------
8 files changed, 60 insertions(+), 21 deletions(-)
create mode 100644 tests/syntax/binary_op.c
delete mode 100644 tests/syntax/binary_op.i
create mode 100644 tests/syntax/oracle/binary_op.0.res.oracle
create mode 100644 tests/syntax/oracle/binary_op.1.res.oracle
create mode 100644 tests/syntax/oracle/binary_op.2.res.oracle
create mode 100644 tests/syntax/oracle/binary_op.3.res.oracle
delete mode 100644 tests/syntax/oracle/binary_op.res.oracle
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 74c9c3317e9..e2fedba13a4 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -7674,13 +7674,18 @@ and normalize_binop binop action local_env asconst le re what =
* version if necessary *)
and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
let doArithmetic () =
- let tres = arithmeticConversion t1 t2 in
- (* Keep the operator since it is arithmetic *)
- tres,
- optConstFoldBinOp loc false bop
- (makeCastT ~e:e1 ~oldt:t1 ~newt:tres)
- (makeCastT ~e:e2 ~oldt:t2 ~newt:tres)
- tres
+ if isArithmeticType t1 && isArithmeticType t2 then begin
+ let tres = arithmeticConversion t1 t2 in
+ (* Keep the operator since it is arithmetic *)
+ tres,
+ optConstFoldBinOp loc false bop
+ (makeCastT ~e:e1 ~oldt:t1 ~newt:tres)
+ (makeCastT ~e:e2 ~oldt:t2 ~newt:tres)
+ tres
+ end else
+ abort_context
+ "%a operator on non-arithmetic type(s) %a and %a"
+ Cil_printer.pp_binop bop Cil_printer.pp_typ t1 Cil_printer.pp_typ t2
in
let doArithmeticComp () =
let tres = arithmeticConversion t1 t2 in
diff --git a/tests/syntax/binary_op.c b/tests/syntax/binary_op.c
new file mode 100644
index 00000000000..da6c970aca0
--- /dev/null
+++ b/tests/syntax/binary_op.c
@@ -0,0 +1,24 @@
+/* run.config
+EXIT: 1
+OPT:-cpp-extra-args="-DBITWISE"
+OPT:-cpp-extra-args="-DMULT"
+EXIT: 0
+OPT:-cpp-extra-args="-DADD"
+OPT:-cpp-extra-args="-DCMP"
+*/
+
+#ifdef BITWISE
+int v(void) { return 0 & v; }
+#endif
+
+#ifdef MULT
+int w(void) { return 0 * w; }
+#endif
+
+#ifdef ADD
+int x(void) { return 0 + x; }
+#endif
+
+#ifdef CMP
+int y(void) { return 0 <= y; }
+#endif
diff --git a/tests/syntax/binary_op.i b/tests/syntax/binary_op.i
deleted file mode 100644
index 768af5955de..00000000000
--- a/tests/syntax/binary_op.i
+++ /dev/null
@@ -1,6 +0,0 @@
-/* run.config
-EXIT: 1
-STDOPT:
-*/
-
-int v(void) { return 0 & v; }
diff --git a/tests/syntax/oracle/binary_op.0.res.oracle b/tests/syntax/oracle/binary_op.0.res.oracle
new file mode 100644
index 00000000000..60dc2afc775
--- /dev/null
+++ b/tests/syntax/oracle/binary_op.0.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing binary_op.c (with preprocessing)
+[kernel] binary_op.c:11: User Error:
+ & operator on non-integer type(s) int and int (*)(void)
+ 9
+ 10 #ifdef BITWISE
+ 11 int v(void) { return 0 & v; }
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 12 #endif
+ 13
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/binary_op.1.res.oracle b/tests/syntax/oracle/binary_op.1.res.oracle
new file mode 100644
index 00000000000..b896f4027b9
--- /dev/null
+++ b/tests/syntax/oracle/binary_op.1.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing binary_op.c (with preprocessing)
+[kernel] binary_op.c:15: User Error:
+ * operator on non-arithmetic type(s) int and int (*)(void)
+ 13
+ 14 #ifdef MULT
+ 15 int w(void) { return 0 * w; }
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 16 #endif
+ 17
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/binary_op.2.res.oracle b/tests/syntax/oracle/binary_op.2.res.oracle
new file mode 100644
index 00000000000..b60a0b2353c
--- /dev/null
+++ b/tests/syntax/oracle/binary_op.2.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing binary_op.c (with preprocessing)
+[kernel:typing:int-conversion] binary_op.c:19: Warning:
+ Conversion from a pointer to an integer without an explicit cast
diff --git a/tests/syntax/oracle/binary_op.3.res.oracle b/tests/syntax/oracle/binary_op.3.res.oracle
new file mode 100644
index 00000000000..651bbbc7815
--- /dev/null
+++ b/tests/syntax/oracle/binary_op.3.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing binary_op.c (with preprocessing)
diff --git a/tests/syntax/oracle/binary_op.res.oracle b/tests/syntax/oracle/binary_op.res.oracle
deleted file mode 100644
index c173a17a488..00000000000
--- a/tests/syntax/oracle/binary_op.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-[kernel] Parsing binary_op.i (no preprocessing)
-[kernel] binary_op.i:6: User Error:
- & operator on non-integer type(s) int and int (*)(void)
- 4 */
- 5
- 6 int v(void) { return 0 & v; }
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-[kernel] Frama-C aborted: invalid user input.
--
GitLab