From f163e72721a0259beb90ce41fbba036d558b5727 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 4 May 2021 17:39:06 +0200
Subject: [PATCH] [Kernel] fix several crashes related to very large integers
---
src/kernel_internals/typing/cabs2cil.ml | 55 ++++++++++++++++++++++---
src/kernel_services/ast_queries/cil.ml | 19 ++++++---
src/kernel_services/ast_queries/cil.mli | 5 ++-
3 files changed, 66 insertions(+), 13 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 0b61835de9d..5f17a26c2b7 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3348,7 +3348,14 @@ let rec setOneInit this o preinit =
let idx, (* Index in the current comp *)
restoff (* Rest offset *) =
match o with
- | Index({enode = Const(CInt64(i,_,_))}, off) -> Integer.to_int i, off
+ | Index({enode = Const(CInt64(i,_,_))}, off) ->
+ begin
+ match Integer.to_int_opt i with
+ | Some i' -> i', off
+ | None -> Kernel.fatal ~current:true
+ "integer too large: %a"
+ (Integer.pretty ~hexa:true) i
+ end
| Field (f, off) ->
(* Find the index of the field *)
let rec loop (idx: int) = function
@@ -3428,7 +3435,14 @@ let rec collectInitializer
| Some len -> begin
match constFoldToInt len with
| Some ni when Integer.ge ni Integer.zero ->
- (Integer.to_int ni), false
+ begin
+ match Integer.to_int_opt ni with
+ | Some ni' -> ni', false
+ | None ->
+ Kernel.fatal ~current:true
+ "Array length %a overflows int, cannot use initializer."
+ Cil_printer.pp_exp len
+ end
| _ ->
Kernel.fatal ~current:true
"Array length %a is not a compile-time constant: \
@@ -5701,7 +5715,14 @@ and isIntegerConstant ghost (aexp) : int option =
match doExp (ghost_local_env ghost) CMayConst aexp (AExp None) with
| (_, c, e, _) when isEmpty c -> begin
match Cil.constFoldToInt e with
- | Some n -> (try Some (Integer.to_int n) with Z.Overflow -> None)
+ | Some n ->
+ begin
+ match Integer.to_int_opt n with
+ | Some n' -> Some n'
+ | None -> Kernel.fatal ~current:true
+ "integer constant too large in expression: %a"
+ Cil_printer.pp_exp e
+ end
| _ -> None
end
| _ -> None
@@ -8467,7 +8488,13 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
let doidx = add_reads ~ghost idxe'.eloc r doidx in
match constFoldToInt idxe', isNotEmpty doidx with
- | Some x, false -> Integer.to_int x, doidx
+ | Some x, false ->
+ begin
+ match Integer.to_int_opt x with
+ | Some x' -> x', doidx
+ | None -> abort_context
+ "INDEX initialization designator overflows"
+ end
| _ ->
abort_context
"INDEX initialization designator is not a constant"
@@ -8505,7 +8532,14 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
Kernel.fatal ~current:true "Range designators are not constants";
let first, last =
match constFoldToInt idxs', constFoldToInt idxe' with
- | Some s, Some e -> Integer.to_int s, Integer.to_int e
+ | Some s, Some e ->
+ begin
+ match Integer.to_int_opt s, Integer.to_int_opt e with
+ | Some s', Some e' -> s', e'
+ | _, _ ->
+ Kernel.fatal ~current:true
+ "INDEX_RANGE initialization designator overflows"
+ end
| _ ->
Kernel.fatal ~current:true
"INDEX_RANGE initialization designator is not a constant"
@@ -10062,7 +10096,16 @@ and doStatement local_env (s : Cabs.statement) : chunk =
"Case statement with a non-constant";
let il, ih =
match constFoldToInt el', constFoldToInt eh' with
- | Some il, Some ih -> Integer.to_int il, Integer.to_int ih
+ | Some il, Some ih ->
+ begin
+ match Integer.to_int_opt il, Integer.to_int_opt ih with
+ | Some il', Some ih' -> il', ih'
+ | _, _ ->
+ Kernel.fatal ~current:true
+ "constant(s) in case range too large: %a ... %a"
+ (Integer.pretty ~hexa:false) il
+ (Integer.pretty ~hexa:false) ih
+ end
| _ ->
Kernel.fatal ~current:true
"Cannot understand the constants in case range"
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index b7b405e03e2..25de3a7c644 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4102,7 +4102,13 @@ and alignOfField (fi: fieldinfo) =
and intOfAttrparam (a:attrparam) : int option =
let rec doit a : int =
match a with
- | AInt(n) -> Integer.to_int n
+ | AInt(n) ->
+ begin
+ match Integer.to_int_opt n with
+ | Some n' -> n'
+ | None ->
+ raise (SizeOfError ("Overflow in integer attribute.", voidType))
+ end
| ABinOp(PlusA, a1, a2) -> doit a1 + doit a2
| ABinOp(MinusA, a1, a2) -> doit a1 - doit a2
| ABinOp(Mult, a1, a2) -> doit a1 * doit a2
@@ -4410,9 +4416,9 @@ and bitsSizeOf t =
Const(CInt64(l,_,_)) ->
let sz = Integer.mul (Integer.of_int (bitsSizeOf bt)) l in
let sz' =
- try
- Integer.to_int sz
- with Z.Overflow ->
+ match Integer.to_int_opt sz with
+ | Some i -> i
+ | None ->
raise
(SizeOfError
("Array is so long that its size can't be "
@@ -5996,7 +6002,10 @@ let lenOfArray64 eo =
ni
| _ -> raise LenOfArray
end
-let lenOfArray eo = Integer.to_int (lenOfArray64 eo)
+let lenOfArray eo =
+ match Integer.to_int_opt (lenOfArray64 eo) with
+ | None -> raise LenOfArray
+ | Some l -> l
(*** Make an initializer for zeroing a data type ***)
let rec makeZeroInit ~loc (t: typ) : init =
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 094edf99428..7e24ee1a47a 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -606,8 +606,9 @@ val isArrayType: typ -> bool
(** True if the argument is a struct of union type *)
val isStructOrUnionType: typ -> bool
-(** Raised when {!Cil.lenOfArray} fails either because the length is [None]
- * or because it is a non-constant expression *)
+(** Raised when {!Cil.lenOfArray} fails either because the length is [None],
+ * because it is a non-constant expression, or because it overflows an int.
+*)
exception LenOfArray
(** Call to compute the array length as present in the array type, to an
--
GitLab