From 738ceae6639030a17d79bc35baf4b0a51f2cf290 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 24 Oct 2023 16:57:40 +0200
Subject: [PATCH] Check if array length is too large in cabs2cil
---
src/kernel_internals/typing/cabs2cil.ml | 25 ++++++++++++++++++++++---
1 file changed, 22 insertions(+), 3 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 734680610c0..34aac497ba5 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4794,9 +4794,28 @@ and doType (ghost:bool) isFuncArg
let cst = constFold true len' in
(match cst.enode with
| Const(CInt64(i, _, _)) ->
- if Integer.lt i Integer.zero then
- Kernel.error ~once:true ~current:true
- "Array length is negative."
+ begin
+ if Integer.lt i Integer.zero then
+ Kernel.error ~once:true ~current:true
+ "Array length is negative."
+ else
+ try
+ (* Check if array length is > SIZE_MAX / sizeof(bt) *)
+ let elem_size = Integer.of_int @@ bytesSizeOf bt in
+ let size_t = bitsSizeOfInt theMachine.kindOfSizeOf in
+ let size_max = Cil.max_unsigned_number size_t in
+ let limit = Integer.c_div size_max elem_size in
+ if Integer.gt i limit then
+ Kernel.error ~once:true ~current:true
+ "Array length is too large.";
+ with
+ | SizeOfError (msg,_) ->
+ Kernel.abort ~current:true "%s" msg
+ | Invalid_argument msg ->
+ Kernel.fatal ~current:true "%s" msg
+ | Division_by_zero ->
+ Kernel.fatal ~current:true "Array element size cannot be zero"
+ end
| _ when not allowVarSizeArrays ->
if isConstant cst then
(* e.g., there may be a float constant involved.
--
GitLab