From 344ef440eec3e49e9407ff08f1d4517f760fbb78 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 20 Apr 2021 19:37:59 +0200
Subject: [PATCH] [kernel] Fixes a crash on __alignof__(void).
Catches the exception [SizeOfError] when using [Cil.bytesAlignOf].
---
src/kernel_services/abstract_interp/base.ml | 16 +++++++++-------
src/kernel_services/ast_queries/cil.ml | 11 +++++++++--
src/kernel_services/ast_queries/cil.mli | 3 ++-
src/plugins/e-acsl/src/analyses/interval.ml | 4 +++-
4 files changed, 23 insertions(+), 11 deletions(-)
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 0bfde596c3a..9f5bc00b9ef 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -349,13 +349,15 @@ let is_aligned_by b alignment =
if Int.is_zero alignment
then false
else
- match b with
- | Var (v,_) | Allocated(v,_,_) ->
- Int.is_zero (Int.e_rem (Int.of_int (Cil.bytesAlignOf v.vtype)) alignment)
- | CLogic_Var (_, ty, _) ->
- Int.is_zero (Int.e_rem (Int.of_int (Cil.bytesAlignOf ty)) alignment)
- | Null -> true
- | String _ -> Int.is_one alignment
+ try
+ match b with
+ | Var (v,_) | Allocated(v,_,_) ->
+ Int.is_zero (Int.e_rem (Int.of_int (Cil.bytesAlignOf v.vtype)) alignment)
+ | CLogic_Var (_, ty, _) ->
+ Int.is_zero (Int.e_rem (Int.of_int (Cil.bytesAlignOf ty)) alignment)
+ | Null -> true
+ | String _ -> Int.is_one alignment
+ with Cil.SizeOfError _ -> false
let is_any_formal_or_local v =
match v with
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 81f75901401..203845899ac 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4545,7 +4545,10 @@ and constFold (machdep: bool) (e: exp) : exp =
| SizeOfStr s when machdep ->
kinteger ~loc theMachine.kindOfSizeOf (1 + String.length s)
| AlignOf t when machdep ->
- kinteger ~loc theMachine.kindOfSizeOf (bytesAlignOf t)
+ begin
+ try kinteger ~loc theMachine.kindOfSizeOf (bytesAlignOf t)
+ with SizeOfError _ -> e
+ end
| AlignOfE e when machdep -> begin
(* The alignment of an expression is not always the alignment of its
* type. I know that for strings this is not true *)
@@ -5223,7 +5226,11 @@ let rec constFoldTermNodeAtTop = function
(try integer_lconstant (bytesSizeOf typ)
with SizeOfError _ -> t)
| TSizeOfStr str -> integer_lconstant (String.length str + 1)
- | TAlignOf typ -> integer_lconstant (bytesAlignOf typ)
+ | TAlignOf typ as t ->
+ begin
+ try integer_lconstant (bytesAlignOf typ)
+ with SizeOfError _ -> t
+ end
| TSizeOfE { term_type= Ctype typ } -> constFoldTermNodeAtTop (TSizeOf typ)
| TAlignOfE { term_type= Ctype typ }
-> constFoldTermNodeAtTop (TAlignOf typ)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 02f54e2f020..2613a70e4cf 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2183,7 +2183,8 @@ val sizeOf: loc:location -> typ -> exp
(** The minimum alignment (in bytes) for a type. This function is
* architecture dependent, so you should only call this after you call
- * {!Cil.initCIL}. *)
+ * {!Cil.initCIL}.
+ * Raises {!SizeOfError} when it cannot compute the alignment. *)
val bytesAlignOf: typ -> int
(** [intOfAttrparam a] tries to const-fold [a] into a numeric value.
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index ab451611348..4668403ccdd 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -406,7 +406,9 @@ let infer_sizeof ty =
try singleton_of_int (Cil.bytesSizeOf ty)
with Cil.SizeOfError _ -> interv_of_typ Cil.theMachine.Cil.typeOfSizeOf
-let infer_alignof ty = singleton_of_int (Cil.bytesAlignOf ty)
+let infer_alignof ty =
+ try singleton_of_int (Cil.bytesAlignOf ty)
+ with Cil.SizeOfError _ -> interv_of_typ Cil.theMachine.Cil.typeOfSizeOf
let rec infer t =
let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
--
GitLab