From 1f174257db5c5540f187e41995bcddb535d9d03c Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 29 Mar 2022 22:53:27 +0200
Subject: [PATCH] [Eva] multidim: fix unhandled exception in offset addition
---
.../abstract_interp/abstract_offset.ml | 67 +++++++++++++------
.../abstract_interp/abstract_offset.mli | 7 +-
2 files changed, 52 insertions(+), 22 deletions(-)
diff --git a/src/kernel_services/abstract_interp/abstract_offset.ml b/src/kernel_services/abstract_interp/abstract_offset.ml
index 84e6056507e..4324506eb45 100644
--- a/src/kernel_services/abstract_interp/abstract_offset.ml
+++ b/src/kernel_services/abstract_interp/abstract_offset.ml
@@ -20,13 +20,35 @@
(* *)
(**************************************************************************)
+module Top =
+struct
+ [@@@warning "-32"]
+
+ let zip x y =
+ match x, y with
+ | `Top, _ | _, `Top -> `Top
+ | `Value x, `Value y -> `Value (x,y)
+
+ let (>>-) t f = match t with
+ | `Top -> `Top
+ | `Value t -> f t
+
+ let (>>-:) t f = match t with
+ | `Top -> `Top
+ | `Value t -> `Value (f t)
+
+ let (let+) = (>>-:)
+ let (let*) = (>>-)
+end
+
+open Top
+
module type T =
sig
type t
val pretty : Format.formatter -> t -> unit
val append : t -> t -> t
- val add_index : (Cil_types.exp -> Int_val.t) -> t -> Cil_types.exp -> t
val join : t -> t -> t
val of_cil_offset : (Cil_types.exp -> Int_val.t) -> Cil_types.typ -> Cil_types.offset -> t
val of_ival : base_typ:Cil_types.typ -> typ:Cil_types.typ -> Ival.t -> t
@@ -66,23 +88,29 @@ struct
let add_index oracle base exp =
let rec aux = function
- | NoOffset _ -> assert false
- | Field (fi, s) -> Field (fi, aux s)
+ | NoOffset _ as o ->
+ let idx = oracle exp in
+ if Int_val.is_zero idx
+ then `Value o
+ else `Top (* Can't add index if not an array *)
+ | Field (fi, s) ->
+ let+ s = aux s in
+ Field (fi, s)
| Index (e, i, t, (NoOffset _ as s)) ->
- begin
- let idx' = Int_val.add i (oracle exp) in
- let loc = Cil_datatype.Location.unknown in
- let e = match e with (* If i is singleton, we can use this as the index expression *)
- | None when Int_val.is_singleton i ->
- let loc = Cil_datatype.Location.unknown in
- Some (Cil.kinteger64 ~loc (Int_val.project_int i))
- | e -> e
- in
- let e' = Option.map (Fun.flip (Cil.mkBinOp ~loc Cil_types.PlusA) exp) e in
- (* TODO: is idx inside bounds ? *)
- Index (e', idx', t, s)
- end
- | Index (e, i, t, s) -> Index (e, i, t, aux s)
+ let idx' = Int_val.add i (oracle exp) in
+ let loc = Cil_datatype.Location.unknown in
+ let e = match e with (* If i is singleton, we can use this as the index expression *)
+ | None when Int_val.is_singleton i ->
+ let loc = Cil_datatype.Location.unknown in
+ Some (Cil.kinteger64 ~loc (Int_val.project_int i))
+ | e -> e
+ in
+ let e' = Option.map (Fun.flip (Cil.mkBinOp ~loc Cil_types.PlusA) exp) e in
+ (* TODO: is idx inside bounds ? *)
+ `Value (Index (e', idx', t, s))
+ | Index (e, i, t, s) ->
+ let+ s = aux s in
+ Index (e, i, t, s)
in
aux base
@@ -269,9 +297,8 @@ struct
| `Value o1, `Value o2 -> `Value (TypedOffset.append o1 o2)
let add_index oracle base exp =
- match base with
- | `Top -> `Top
- | `Value base -> `Value (TypedOffset.add_index oracle base exp)
+ let* base = base in
+ TypedOffset.add_index oracle base exp
let join o1 o2 =
match o1, o2 with
diff --git a/src/kernel_services/abstract_interp/abstract_offset.mli b/src/kernel_services/abstract_interp/abstract_offset.mli
index 64638b2bd04..368cce1d4e3 100644
--- a/src/kernel_services/abstract_interp/abstract_offset.mli
+++ b/src/kernel_services/abstract_interp/abstract_offset.mli
@@ -26,7 +26,6 @@ sig
val pretty : Format.formatter -> t -> unit
val append : t -> t -> t (* Does not check that the appened offset fits *)
- val add_index : (Cil_types.exp -> Int_val.t) -> t -> Cil_types.exp -> t
val join : t -> t -> t
val of_cil_offset : (Cil_types.exp -> Int_val.t) -> Cil_types.typ -> Cil_types.offset -> t
val of_ival : base_typ:Cil_types.typ -> typ:Cil_types.typ -> Ival.t -> t
@@ -41,4 +40,8 @@ type typed_offset =
| Field of Cil_types.fieldinfo * typed_offset
module TypedOffset : T with type t = typed_offset
-module TypedOffsetOrTop : T with type t = [ `Value of typed_offset | `Top ]
+module TypedOffsetOrTop :
+sig
+ include T with type t = [ `Value of typed_offset | `Top ]
+ val add_index : (Cil_types.exp -> Int_val.t) -> t -> Cil_types.exp -> t
+end
--
GitLab