diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml
index d11f76492427d9cbd278f23d8817bf98fdea28b6..cbe6c0290882f4b68d2036bcce074358e61f93f5 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.ml
+++ b/src/kernel_services/abstract_interp/abstract_memory.ml
@@ -314,10 +314,10 @@ sig
val join : oracle:bioracle -> t -> t -> t
val smash : oracle:oracle -> t -> t -> t
val read : oracle:oracle -> (Cil_types.typ -> t -> 'a) -> ('a -> 'a -> 'a) ->
- Abstract_offset.typed_offset -> t -> 'a
+ Abstract_offset.t -> t -> 'a
val write : oracle:oracle ->
(weak:bool -> Cil_types.typ -> t -> t or_bottom) ->
- weak:bool -> Abstract_offset.typed_offset -> t -> t or_bottom
+ weak:bool -> Abstract_offset.t -> t -> t or_bottom
val incr_bound : oracle:oracle -> Cil_types.varinfo -> Integer.t option ->
t -> t
val add_segmentation_bounds : oracle:oracle -> typ:Cil_types.typ ->
@@ -1873,7 +1873,7 @@ struct
include ProtoMemory
- type location = Abstract_offset.typed_offset
+ type location = Abstract_offset.t
let pretty = pretty_root
diff --git a/src/kernel_services/abstract_interp/abstract_memory.mli b/src/kernel_services/abstract_interp/abstract_memory.mli
index 7a9ed21b0d568cbf05308de00cf430defe1f87d1..3100daa6bbf1ac5faa13b742e5eca5e7d659947a 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.mli
+++ b/src/kernel_services/abstract_interp/abstract_memory.mli
@@ -87,7 +87,7 @@ type strength = Strong | Weak | Reinforce (* update strength *)
module TypedMemory (Config : Config) (Value : Value) :
sig
- type location = Abstract_offset.typed_offset
+ type location = Abstract_offset.t
type value = Value.t
type t
diff --git a/src/kernel_services/abstract_interp/abstract_offset.ml b/src/kernel_services/abstract_interp/abstract_offset.ml
index 4324506eb45abdc043f5983034c59a12f52618d3..25eacbf4e4ab8fbf3ca3c4f177b7c88e302087ce 100644
--- a/src/kernel_services/abstract_interp/abstract_offset.ml
+++ b/src/kernel_services/abstract_interp/abstract_offset.ml
@@ -38,292 +38,245 @@ struct
| `Value t -> `Value (f t)
let (let+) = (>>-:)
- let (let*) = (>>-)
-end
-
-open Top
-
-module type T =
-sig
- type t
+ let (and+) = zip
+let (let*) = (>>-)
- val pretty : Format.formatter -> t -> unit
- val append : t -> t -> 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
- val of_term_offset : Cil_types.typ -> Cil_types.term_offset -> t
- val is_singleton : t -> bool
- val references : t -> Cil_types.varinfo list
+let of_option = function
+ | None -> `Top
+ | Some x -> `Value x
end
-type typed_offset =
- | NoOffset of Cil_types.typ
- | Index of Cil_types.exp option * Int_val.t * Cil_types.typ * typed_offset
- | Field of Cil_types.fieldinfo * typed_offset
-
-
-module TypedOffset =
-struct
- type t = typed_offset
+type 'a or_top = [`Value of 'a | `Top]
- let rec pretty fmt = function
- | NoOffset _t -> ()
- | Field (fi, s) -> Format.fprintf fmt ".%s%a" fi.fname pretty s
- | Index (None, i, _t, s) ->
- Format.fprintf fmt "[%a]%a"
- Int_val.pretty i
- pretty s
- | Index (Some e, i, _t, s) ->
- Format.fprintf fmt "[%a∈%a]%a"
- Cil_printer.pp_exp e
- Int_val.pretty i
- pretty s
-
- let rec append o1 o2 =
- match o1 with
- | NoOffset _t -> o2
- | Field (fi, s) -> Field (fi, append s o2)
- | Index (e, i, t, s) -> Index (e, i, t, append s o2)
-
- let add_index oracle base exp =
- let rec aux = function
- | 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)) ->
- 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
+open Top
- let rec join o1 o2 =
- match o1, o2 with
- | NoOffset t, NoOffset t'
- when Bit_utils.type_compatible t t' ->
- NoOffset t
- | Field (fi, s1), Field (fi', s2)
- when Cil_datatype.Fieldinfo.equal fi fi' ->
- Field (fi, join s1 s2)
- | Index (e1, i1, t, s1), Index (e2, i2, t', s2)
- when Bit_utils.type_compatible t t' ->
- let e = match e1, e2 with
- | Some e1, Some e2 when Cil_datatype.ExpStructEq.equal e1 e2 ->
- Some e1 (* keep expression only when equivalent from both offsets *)
- | _ -> None
+type t =
+ | NoOffset of Cil_types.typ
+ | Index of Cil_types.exp option * Int_val.t * Cil_types.typ * t
+ | Field of Cil_types.fieldinfo * t
+
+let rec pretty fmt = function
+ | NoOffset _t -> ()
+ | Field (fi, s) -> Format.fprintf fmt ".%s%a" fi.fname pretty s
+ | Index (None, i, _t, s) ->
+ Format.fprintf fmt "[%a]%a"
+ Int_val.pretty i
+ pretty s
+ | Index (Some e, i, _t, s) ->
+ Format.fprintf fmt "[%a∈%a]%a"
+ Cil_printer.pp_exp e
+ Int_val.pretty i
+ pretty s
+
+let rec append o1 o2 =
+ match o1 with
+ | NoOffset _t -> o2
+ | Field (fi, s) -> Field (fi, append s o2)
+ | Index (e, i, t, s) -> Index (e, i, t, append s o2)
+
+let add_index oracle base exp =
+ let rec aux = function
+ | 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, sub) ->
+ let+ sub' = aux sub in
+ Field (fi, sub')
+ | Index (e, i, t, (NoOffset _ as sub)) ->
+ 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
- Index (e, Int_val.join i1 i2, t, join s1 s2)
- | _ -> raise Abstract_interp.Error_Top
-
- let array_bounds array_size =
- (* TODO: handle undefined sizes and not const foldable sizes *)
- match array_size with
+ 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, sub))
+ | Index (e, i, t, sub) ->
+ let+ sub' = aux sub in
+ Index (e, i, t, sub')
+ in
+ aux base
+
+let rec join o1 o2 =
+ match o1, o2 with
+ | NoOffset t, NoOffset t'
+ when Bit_utils.type_compatible t t' ->
+ `Value (NoOffset t)
+ | Field (fi, sub1), Field (fi', sub2)
+ when Cil_datatype.Fieldinfo.equal fi fi' ->
+ let+ sub' = join sub1 sub2 in
+ Field (fi, sub')
+ | Index (e1, i1, t, sub1), Index (e2, i2, t', sub2)
+ when Bit_utils.type_compatible t t' ->
+ let e = match e1, e2 with
+ | Some e1, Some e2 when Cil_datatype.ExpStructEq.equal e1 e2 ->
+ Some e1 (* keep expression only when equivalent from both offsets *)
+ | _ -> None
+ in
+ let+ sub' = join sub1 sub2 in
+ Index (e, Int_val.join i1 i2, t, sub')
+ | _ -> `Top
+
+let array_bounds array_size =
+ (* TODO: handle undefined sizes and not const foldable sizes *)
+ match array_size with
+ | None -> None
+ | Some size_exp ->
+ match Cil.constFoldToInt size_exp with
| None -> None
- | Some size_exp ->
- match Cil.constFoldToInt size_exp with
- | None -> None
- | Some size when Integer.(gt size zero) -> Some Integer.(zero, pred size)
- | Some _ -> None
-
- let array_range array_size =
- Option.map
- (fun (l,u) -> Int_val.inject_range (Some l) (Some u))
- (array_bounds array_size)
-
- let assert_valid_index idx size =
- match array_range size with
- | Some range when Int_val.is_included idx range -> ()
- | _ -> raise Abstract_interp.Error_Top
-
- let rec of_cil_offset oracle base_typ = function
- | Cil_types.NoOffset -> NoOffset base_typ
- | Field (fi, sub) ->
- if Cil.typeHasQualifier "volatile" fi.ftype then
- raise Abstract_interp.Error_Top
- else
- Field (fi, of_cil_offset oracle fi.ftype sub)
- | Index (exp, sub) ->
- match Cil.unrollType base_typ with
- | TArray (elem_typ, array_size, _) ->
- let idx = oracle exp in
- assert_valid_index idx array_size;
- Index (Some exp, idx, elem_typ, of_cil_offset oracle elem_typ sub)
- | _ -> assert false
-
- let rec of_int_val ~base_typ ~typ ival =
- if Int_val.is_zero ival && Bit_utils.type_compatible base_typ typ then
- NoOffset typ
+ | Some size when Integer.(gt size zero) -> Some Integer.(zero, pred size)
+ | Some _ -> None
+
+let array_range array_size =
+ Option.map
+ (fun (l,u) -> Int_val.inject_range (Some l) (Some u))
+ (array_bounds array_size)
+
+let assert_valid_index idx size =
+ match array_range size with
+ | Some range when Int_val.is_included idx range -> `Value ()
+ | _ -> `Top
+
+let of_var_address vi =
+ NoOffset vi.Cil_types.vtype
+
+let rec of_cil_offset oracle base_typ = function
+ | Cil_types.NoOffset -> `Value (NoOffset base_typ)
+ | Field (fi, sub) ->
+ if Cil.typeHasQualifier "volatile" fi.ftype then
+ `Top
else
- match Cil.unrollType base_typ with
- | TArray (elem_typ, array_size, _) ->
- let range, rem =
- try
- let elem_size = Integer.of_int (Cil.bitsSizeOf elem_typ) in
- if Integer.is_zero elem_size then (* array of elements of size 0 *)
- if Int_val.is_zero ival then (* the whole range is valid *)
- let range = array_range array_size in
- Extlib.the ~exn:Abstract_interp.Error_Top range, ival
- else (* Non-zero offset cannot represent anything here *)
- raise Abstract_interp.Error_Top
- else
- Int_val.scale_div ~pos:true elem_size ival,
- Int_val.scale_rem ~pos:true elem_size ival
- with Cil.SizeOfError (_,_) ->
- (* Cil.bitsSizeOf can raise an exception when elements are
- themselves array of execution-time size *)
- if Int_val.is_zero ival then
- ival, ival
- else
- raise Abstract_interp.Error_Top
- in
- assert_valid_index range array_size;
- let sub = of_int_val ~base_typ:elem_typ ~typ rem in
- Index (None, range, elem_typ, sub)
-
- | TComp (ci, _) ->
- if not ci.cstruct then
- (* Ignore unions for now *)
- raise Abstract_interp.Error_Top
- else
- let rec find_field = function
- | [] -> raise Abstract_interp.Error_Top
- | fi :: q ->
- let offset, width = Cil.fieldBitsOffset fi in
- let l = Integer.(of_int offset) in
- let u = Integer.(pred (add l (of_int width))) in
- let matches =
- if width = 0 then
- Int_val.(equal ival (inject_singleton l))
- else
- let range = Int_val.inject_range (Some l) (Some u) in
- Int_val.is_included ival range
- in
- if matches then
- if Cil.typeHasQualifier "volatile" fi.ftype then
- raise Abstract_interp.Error_Top
- else
- let sub_ival = Int_val.add_singleton (Integer.neg l) ival in
- Field (fi, of_int_val ~base_typ:fi.ftype ~typ sub_ival)
- else
- find_field q
- in
- find_field (Option.value ~default:[] ci.cfields)
-
- | _ -> raise Abstract_interp.Error_Top
-
- let of_ival ~base_typ ~typ ival =
- match Ival.project_int_val ival with
- | Some ival -> of_int_val ~base_typ ~typ ival
- | None -> raise Abstract_interp.Error_Top (* should not happen *)
-
- let index_of_term array_size t = (* Exact constant ranges *)
- match t.Cil_types.term_node with
- | TConst (Integer (v, _)) -> Int_val.inject_singleton v
- | Trange (l,u) ->
- let eval bound = function
- | None -> Extlib.the ~exn:Abstract_interp.Error_Top bound
- | Some { Cil_types.term_node=TConst (Integer (v, _)) } -> v
- | Some _ -> raise Abstract_interp.Error_Top
+ let+ sub' = of_cil_offset oracle fi.ftype sub in
+ Field (fi, sub')
+ | Index (exp, sub) ->
+ match Cil.unrollType base_typ with
+ | TArray (elem_typ, array_size, _) ->
+ let idx = oracle exp in
+ let+ () = assert_valid_index idx array_size
+ and+ sub' = of_cil_offset oracle elem_typ sub in
+ Index (Some exp, idx, elem_typ, sub')
+ | _ -> assert false
+
+let rec of_int_val ~base_typ ~typ ival =
+ if Int_val.is_zero ival && Bit_utils.type_compatible base_typ typ then
+ `Value (NoOffset typ)
+ else
+ match Cil.unrollType base_typ with
+ | TArray (elem_typ, array_size, _) ->
+ let* range, rem =
+ try
+ let elem_size = Integer.of_int (Cil.bitsSizeOf elem_typ) in
+ if Integer.is_zero elem_size then (* array of elements of size 0 *)
+ if Int_val.is_zero ival then (* the whole range is valid *)
+ let+ range = Top.of_option (array_range array_size) in
+ range, ival
+ else (* Non-zero offset cannot represent anything here *)
+ `Top
+ else
+ let range = Int_val.scale_div ~pos:true elem_size ival
+ and rem = Int_val.scale_rem ~pos:true elem_size ival in
+ `Value (range, rem)
+ with Cil.SizeOfError (_,_) ->
+ (* Cil.bitsSizeOf can raise an exception when elements are
+ themselves array of execution-time size *)
+ if Int_val.is_zero ival then
+ `Value (ival, ival)
+ else
+ `Top
in
- let bounds = array_bounds array_size in
- let lb = Option.map fst bounds and ub = Option.map snd bounds in
- let l' = eval lb l and u' = eval ub u in
- Int_val.inject_range (Some l') (Some u')
- | _ -> raise Abstract_interp.Error_Top
-
- let rec of_term_offset base_typ = function
- | Cil_types.TNoOffset -> NoOffset base_typ
- | TField (fi, sub) ->
- if Cil.typeHasQualifier "volatile" fi.ftype then
- raise Abstract_interp.Error_Top
+ let+ () = assert_valid_index range array_size
+ and+ sub' = of_int_val ~base_typ:elem_typ ~typ rem in
+ Index (None, range, elem_typ, sub')
+
+ | TComp (ci, _) ->
+ if not ci.cstruct then
+ (* Ignore unions for now *)
+ `Top
else
- Field (fi, of_term_offset fi.ftype sub)
- | TIndex (index, sub) ->
- begin match Cil.unrollType base_typ with
- | TArray (elem_typ, array_size, _) ->
- let idx = index_of_term array_size index in
- assert_valid_index idx array_size;
- Index (None, idx, elem_typ, of_term_offset elem_typ sub)
- | _ -> assert false
- end
- | _ -> raise Abstract_interp.Error_Top
-
- let rec is_singleton = function
- | NoOffset _ -> true
- | Field (_fi, sub) -> is_singleton sub
- | Index (e, ival, _elem_typ, sub) ->
- (Option.is_some e || Int_val.is_singleton ival) && is_singleton sub
-
- let references =
- let rec aux acc = function
- | NoOffset _ -> acc
- | Field (_, sub) | Index (None, _, _, sub) -> aux acc sub
- | Index (Some e, _, _, sub) ->
- let r = Cil.extract_varinfos_from_exp e in
- let acc = (Cil_datatype.Varinfo.Set.to_seq r |> List.of_seq) @ acc in
- aux acc sub
+ let rec find_field = function
+ | [] -> `Top
+ | fi :: q ->
+ let offset, width = Cil.fieldBitsOffset fi in
+ let l = Integer.(of_int offset) in
+ let u = Integer.(pred (add l (of_int width))) in
+ let matches =
+ if width = 0 then
+ Int_val.(equal ival (inject_singleton l))
+ else
+ let range = Int_val.inject_range (Some l) (Some u) in
+ Int_val.is_included ival range
+ in
+ if matches then
+ if Cil.typeHasQualifier "volatile" fi.ftype then
+ `Top
+ else
+ let sub_ival = Int_val.add_singleton (Integer.neg l) ival in
+ let+ sub' = of_int_val ~base_typ:fi.ftype ~typ sub_ival in
+ Field (fi, sub')
+ else
+ find_field q
+ in
+ find_field (Option.value ~default:[] ci.cfields)
+
+ | _ -> `Top
+
+let of_ival ~base_typ ~typ ival =
+ match Ival.project_int_val ival with
+ | Some ival -> of_int_val ~base_typ ~typ ival
+ | None -> `Top (* should not happen *)
+
+let index_of_term array_size t = (* Exact constant ranges *)
+ match t.Cil_types.term_node with
+ | TConst (Integer (v, _)) -> `Value (Int_val.inject_singleton v)
+ | Trange (l,u) ->
+ let eval bound = function
+ | None -> Top.of_option bound
+ | Some { Cil_types.term_node=TConst (Integer (v, _)) } -> `Value v
+ | Some _ -> `Top
in
- aux []
-end
-
-module TypedOffsetOrTop =
-struct
- type t = [ `Value of typed_offset | `Top ]
-
- let pretty fmt = function
- | `Top -> Format.pp_print_string fmt "T"
- | `Value o -> TypedOffset.pretty fmt o
-
- let append o1 o2 =
- match o1, o2 with
- | `Top, _ | _, `Top -> `Top
- | `Value o1, `Value o2 -> `Value (TypedOffset.append o1 o2)
-
- let add_index oracle base exp =
- let* base = base in
- TypedOffset.add_index oracle base exp
-
- let join o1 o2 =
- match o1, o2 with
- | `Top, _ | _, `Top -> `Top
- | `Value o1, `Value o2 ->
- try `Value (TypedOffset.join o1 o2)
- with Abstract_interp.Error_Top -> `Top
-
- let of_cil_offset oracle base_typ offset =
- try `Value (TypedOffset.of_cil_offset oracle base_typ offset)
- with Abstract_interp.Error_Top -> `Top
-
- let of_ival ~base_typ ~typ ival =
- try `Value (TypedOffset.of_ival ~base_typ ~typ ival)
- with Abstract_interp.Error_Top -> `Top
-
- let of_term_offset base_typ toffset =
- try `Value (TypedOffset.of_term_offset base_typ toffset)
- with Abstract_interp.Error_Top -> `Top
-
- let is_singleton = function
- | `Top -> false
- | `Value o -> TypedOffset.is_singleton o
-
- let references = function
- | `Top -> []
- | `Value o -> TypedOffset.references o
-end
+ let bounds = array_bounds array_size in
+ let lb = Option.map fst bounds and ub = Option.map snd bounds in
+ let+ l' = eval lb l and+ u' = eval ub u in
+ Int_val.inject_range (Some l') (Some u')
+ | _ -> `Top
+
+let rec of_term_offset base_typ = function
+ | Cil_types.TNoOffset -> `Value (NoOffset base_typ)
+ | TField (fi, sub) ->
+ if Cil.typeHasQualifier "volatile" fi.ftype then
+ `Top
+ else
+ let+ sub' = of_term_offset fi.ftype sub in
+ Field (fi, sub')
+ | TIndex (index, sub) ->
+ begin match Cil.unrollType base_typ with
+ | TArray (elem_typ, array_size, _) ->
+ let* idx = index_of_term array_size index in
+ let+ () = assert_valid_index idx array_size
+ and+ sub' = of_term_offset elem_typ sub in
+ Index (None, idx, elem_typ, sub')
+ | _ -> assert false
+ end
+ | _ -> `Top
+
+let rec is_singleton = function
+ | NoOffset _ -> true
+ | Field (_fi, sub) -> is_singleton sub
+ | Index (e, ival, _elem_typ, sub) ->
+ (Option.is_some e || Int_val.is_singleton ival) && is_singleton sub
+
+let references =
+ let rec aux acc = function
+ | NoOffset _ -> acc
+ | Field (_, sub) | Index (None, _, _, sub) -> aux acc sub
+ | Index (Some e, _, _, sub) ->
+ let r = Cil.extract_varinfos_from_exp e in
+ let acc = (Cil_datatype.Varinfo.Set.to_seq r |> List.of_seq) @ acc in
+ aux acc sub
+ in
+ aux []
diff --git a/src/kernel_services/abstract_interp/abstract_offset.mli b/src/kernel_services/abstract_interp/abstract_offset.mli
index 368cce1d4e3f2bbc901e7229c2535c68c0f2cc86..457393b96da61ec366c9323f73e06874b69dcdb6 100644
--- a/src/kernel_services/abstract_interp/abstract_offset.mli
+++ b/src/kernel_services/abstract_interp/abstract_offset.mli
@@ -20,28 +20,24 @@
(* *)
(**************************************************************************)
-module type T =
-sig
- type t
+type t =
+ | NoOffset of Cil_types.typ
+ | Index of Cil_types.exp option * Int_val.t * Cil_types.typ * t
+ | Field of Cil_types.fieldinfo * t
- val pretty : Format.formatter -> t -> unit
- val append : t -> t -> t (* Does not check that the appened offset fits *)
- 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
- val of_term_offset : Cil_types.typ -> Cil_types.term_offset -> t
- val is_singleton : t -> bool
- val references : t -> Cil_types.varinfo list (* variables referenced in the offset *)
-end
+type 'a or_top = [`Value of 'a | `Top]
-type typed_offset =
- | NoOffset of Cil_types.typ
- | Index of Cil_types.exp option * Int_val.t * Cil_types.typ * typed_offset
- | Field of Cil_types.fieldinfo * typed_offset
+val pretty : Format.formatter -> t -> unit
+
+val of_var_address : Cil_types.varinfo -> t
+val of_cil_offset : (Cil_types.exp -> Int_val.t) ->
+ Cil_types.typ -> Cil_types.offset -> t or_top
+val of_ival : base_typ:Cil_types.typ -> typ:Cil_types.typ -> Ival.t -> t or_top
+val of_term_offset : Cil_types.typ -> Cil_types.term_offset -> t or_top
+
+val is_singleton : t -> bool
+val references : t -> Cil_types.varinfo list (* variables referenced in the offset *)
-module TypedOffset : T with type t = typed_offset
-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
+val append : t -> t -> t (* Does not check that the appened offset fits *)
+val join : t -> t -> t or_top
+val add_index : (Cil_types.exp -> Int_val.t) -> t -> Cil_types.exp -> t or_top
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index 411bc31ff5184bef71af4e99204372764ac9c795..75473ca8fc09bb3fde3946ec72fa96e4ce6705ea 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -25,6 +25,32 @@ open Eval
let dkey = Self.register_category "d-multidim"
+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 (and+) = zip
+let (let*) = (>>-)
+
+let of_option = function
+ | None -> `Top
+ | Some x -> `Value x
+end
+
let map_to_singleton map =
let aux base offset = function
| None -> Some (base, offset)
@@ -121,12 +147,11 @@ let find_builtin =
module Location =
struct
- open Abstract_offset
-
- module Offset = TypedOffsetOrTop
+ module Offset = Abstract_offset
module Map = Base.Base.Map
+ open Top
- type offset = Offset.t
+ type offset = Offset.t or_top
type base = Base.t
type t = offset Map.t
@@ -145,19 +170,22 @@ struct
match map_to_singleton map with
| None -> false
| Some (b,o) ->
- not (Base.is_weak b) && Offset.is_singleton o
+ match o with
+ | `Top -> false
+ | `Value o -> not (Base.is_weak b) && Offset.is_singleton o
- let references map =
+ let references (map : t) =
let module Set = Cil_datatype.Varinfo.Set in
- let add_refs _b o =
- Set.union (Set.of_list (Offset.references o))
+ let add_refs _b o acc =
+ match o with
+ | `Top -> acc
+ | `Value o -> Set.union (Set.of_list (Offset.references o)) acc
in
Map.fold add_refs map Set.empty |> Set.to_seq |> List.of_seq
let of_var (vi : Cil_types.varinfo) : t =
- Map.singleton (Base.of_varinfo vi) (`Value (NoOffset vi.vtype))
+ Map.singleton (Base.of_varinfo vi) (`Value (Offset.of_var_address vi))
- (* Raises Abstract_domain.{Error_top,Error_bottom} *)
let of_lval oracle ((host,offset) as lval : Cil_types.lval) : t =
let oracle' = convert_oracle oracle in
let base_typ = Cil.typeOfLhost host in
@@ -176,16 +204,18 @@ struct
| _ -> exp, None
in
let add base ival map =
- let offset' : Offset.t =
+ let offset' : Offset.t or_top =
match Base.typeof base with
| None -> `Top
| Some base_typ ->
let typ = Cil.typeOf_pointed (Cil.typeOf exp) in
- let base_offset = Offset.of_ival ~base_typ ~typ ival in
- let base_offset = match index with
- | None -> base_offset
- | Some exp -> Offset.add_index oracle' base_offset exp
+ let* base_offset = Offset.of_ival ~base_typ ~typ ival in
+ let* base_offset = match index with
+ | None -> `Value (base_offset)
+ | Some exp ->
+ Offset.add_index oracle' base_offset exp
in
+ let+ offset = offset in
Offset.append base_offset offset
in
Map.add base offset' map
@@ -213,7 +243,7 @@ struct
let add_base base map =
(* Null base doesn't have a type ; use void instead *)
let typ = Option.value ~default:Cil.voidType (Base.typeof base) in
- Map.add base (`Value (NoOffset typ)) map
+ Map.add base (`Value (Offset.NoOffset typ)) map
in
Locations.Location_Bits.(fold_bases add_base loc'.loc empty)
end