diff --git a/Makefile b/Makefile
index 40e7ba2de37519e1f8878a0a4aaf1a44a40c0e4b..715e780673deeb403430217423269c2174cb83c6 100644
--- a/Makefile
+++ b/Makefile
@@ -596,6 +596,8 @@ KERNEL_CMO=\
src/kernel_services/abstract_interp/locations.cmo \
src/kernel_services/abstract_interp/lmap.cmo \
src/kernel_services/abstract_interp/lmap_bitwise.cmo \
+ src/kernel_services/abstract_interp/multidim.cmo \
+ src/kernel_services/abstract_interp/memory_map.cmo \
src/kernel_services/visitors/visitor.cmo \
src/kernel_services/ast_data/statuses_by_call.cmo \
src/kernel_services/ast_printing/printer_tag.cmo \
@@ -874,6 +876,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
domains/hcexprs \
domains/equality/equality domains/equality/equality_domain \
domains/offsm_domain \
+ domains/multidim_domain \
domains/symbolic_locs \
domains/sign_domain \
domains/cvalue/warn domains/cvalue/locals_scoping \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 8d04294f438d5f367ae16f8bf87f2a5784f219f0..409ab53051f5a2c49dd9715a69535b42b28c4219 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -475,6 +475,10 @@ src/kernel_services/abstract_interp/locations.ml: CEA_LGPL
src/kernel_services/abstract_interp/locations.mli: CEA_LGPL
src/kernel_services/abstract_interp/map_lattice.ml: CEA_LGPL
src/kernel_services/abstract_interp/map_lattice.mli: CEA_LGPL
+src/kernel_services/abstract_interp/memory_map.ml: CEA_LGPL
+src/kernel_services/abstract_interp/memory_map.mli: CEA_LGPL
+src/kernel_services/abstract_interp/multidim.ml: CEA_LGPL
+src/kernel_services/abstract_interp/multidim.mli: CEA_LGPL
src/kernel_services/abstract_interp/offsetmap.ml: CEA_LGPL
src/kernel_services/abstract_interp/offsetmap.mli: CEA_LGPL
src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli: CEA_LGPL
@@ -1309,6 +1313,8 @@ src/plugins/value/domains/hcexprs.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/hcexprs.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/inout_domain.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/inout_domain.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim_domain.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim_domain.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/octagons.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/octagons.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/offsm_domain.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/kernel_services/abstract_interp/memory_map.ml b/src/kernel_services/abstract_interp/memory_map.ml
new file mode 100644
index 0000000000000000000000000000000000000000..16e629a679f54f988f80f77f79bb953aa7251eef
--- /dev/null
+++ b/src/kernel_services/abstract_interp/memory_map.ml
@@ -0,0 +1,676 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+[@@@warning "-60"] (* unused module ; to be removed once ocaml is patched *)
+[@@@warning "-37"] (* constructor never used to build values. *)
+[@@@warning "-32"] (* unused value *)
+
+exception Not_implemented
+
+type size = Integer.t
+
+type default =
+ | Top
+ | Numerical
+ | Zero
+
+module Default =
+struct
+ let hash = function
+ | Top -> 3
+ | Numerical -> 7
+ | Zero -> 13
+
+ let equal d1 d2 =
+ match d1,d2 with
+ | Top, Top | Numerical, Numerical | Zero, Zero -> true
+ | Top, (Numerical | Zero) | Numerical, (Top | Zero)
+ | Zero, (Top | Numerical) -> false
+
+ let compare d1 d2 =
+ match d1,d2 with
+ | Top, Top | Numerical, Numerical | Zero, Zero -> 0
+ | Top, (Numerical | Zero) -> 1
+ | (Numerical | Zero), Top -> -1
+ | Numerical, Zero -> 1
+ | Zero, Numerical -> -1
+
+ let is_included d1 d2 =
+ match d1, d2 with
+ | (Top | Numerical | Zero), Top -> true
+ | Top, (Numerical | Zero) -> false
+ | (Numerical | Zero), Numerical -> true
+ | Numerical, Zero -> false
+ | Zero, Zero -> true
+
+ let join d1 d2 =
+ match d1, d2 with
+ | Top, (Top | Numerical | Zero)
+ | (Numerical | Zero), Top -> Top
+ | Numerical, (Numerical | Zero)
+ | Zero, Numerical -> Numerical
+ | Zero, Zero -> Zero
+end
+
+module type Value =
+sig
+ type t
+
+ val name : string
+
+ val hash : t -> int
+ val equal : t -> t -> bool
+ val compare : t -> t -> int
+
+ val pretty : Format.formatter -> t -> unit
+ val zero : t
+ val misaligned : t -> t
+ val top : t
+ val top_numerical : t
+ val is_included : t -> t -> bool
+end
+
+module type Config =
+sig
+ val deps : State.t list
+end
+
+module type T =
+sig
+ type location
+ type value
+ type t
+
+ val hash : t -> int
+ val equal : t -> t -> bool
+ val compare : t -> t -> int
+
+ val top : t
+ val zero : t
+ val is_top : t -> bool
+ val reduce : (value -> value -> value) -> t -> location -> value
+ val extract : (value -> value -> value) -> t -> location -> t
+ val initialize : t -> location -> default -> t
+ val set : t -> location -> value -> t
+ val update : weak:bool -> (weak:bool -> value -> value) -> t -> location -> t
+ val erase : t -> location -> t
+ val overwrite : weak:bool -> (weak:bool -> value -> value -> value) -> t -> location -> t -> t
+ val is_included : t -> t -> bool
+ val join : (size:size -> value -> value -> value) -> t -> t -> t
+ val widen : (size:size -> value -> value -> value) -> t -> t -> t
+ val pretty : Format.formatter -> t -> unit
+end
+
+
+type typed_offset =
+ | NoOffset of Cil_types.typ
+ | Index of Ival.t * Cil_types.typ * typed_offset
+ | Field of Cil_types.fieldinfo * typed_offset
+
+
+module MakeTyped (Config : Config) (Value : Value) =
+struct
+ type location = typed_offset
+ type value = Value.t
+
+ type 'fieldmap memory' =
+ | Default of default
+ | Scalar of memory_scalar
+ | Struct of 'fieldmap memory_struct
+ | Union of 'fieldmap memory_union
+ | Array of 'fieldmap memory_array
+ and memory_scalar = {
+ scalar_value: Value.t;
+ scalar_type: Cil_types.typ;
+ }
+ and 'fieldmap memory_struct = {
+ struct_value: 'fieldmap;
+ struct_info: Cil_types.compinfo;
+ struct_default: default; (* for missing fields *)
+ }
+ (* unions are handled separately from struct to avoid confusion and error *)
+ and 'fieldmap memory_union = {
+ union_value: 'fieldmap memory';
+ union_field: Cil_types.fieldinfo;
+ }
+ and 'fieldmap memory_array = {
+ array_value: 'fieldmap memory';
+ array_cell_type: Cil_types.typ;
+ }
+
+ (* Instanciation of Hptmaps for the tree structure of the memory *)
+
+ module Initial_Values = struct let v = [[]] end
+
+ module Deps = struct let l = Config.deps end
+
+ module Keys =
+ struct
+ include Cil_datatype.Fieldinfo
+ let id f = f.Cil_types.forder (* At each node, all fields come from the same comp *)
+ end
+
+ module rec Memory :
+ Hptmap.V with type t = FieldMap.t memory' =
+ struct
+ include Datatype.Make (
+ struct
+ include Datatype.Undefined
+ include MemorySafe
+ let name = "Memory_map.Typed"
+ let reprs = [ Default Top ]
+ end)
+ let pretty_debug = pretty
+ end
+
+ (* To allow recursive modules to be instanciated, there must be one safe
+ module in the cycle. This is it. It should contain all references
+ to FieldMap and no constants, only functions *)
+ and MemorySafe :
+ sig
+ type t = FieldMap.t memory'
+ val pretty : Format.formatter -> t -> unit
+ val hash : t -> int
+ val equal : t -> t -> bool
+ val compare : t -> t -> int
+ end =
+ struct
+ type t = FieldMap.t memory'
+
+ let rec pretty fmt =
+ let rec leading_indexes acc = function
+ | Array a -> leading_indexes (() :: acc) a.array_value
+ | (Default _ | Scalar _ | Struct _ | Union _) as m -> List.rev acc, m
+ in
+ let pretty_index fmt () =
+ Format.fprintf fmt "[..]"
+ in
+ let pretty_indexes fmt l =
+ Pretty_utils.pp_list pretty_index fmt l
+ in
+ let pretty_field fmt =
+ let first = ref true in
+ fun fi m ->
+ if not !first then Format.fprintf fmt ",@;<1 2>";
+ first := false;
+ let indexes, sub = leading_indexes [] m in
+ Format.fprintf fmt "@[<hv>.%s%a = %a@]"
+ fi.Cil_types.fname
+ pretty_indexes indexes
+ pretty sub
+ in
+ function
+ | Default Top -> Format.fprintf fmt "T"
+ | Default Numerical -> Format.fprintf fmt "[--..--]"
+ | Default Zero -> Format.fprintf fmt "0"
+ | Scalar {scalar_value} -> Value.pretty fmt scalar_value
+ | Struct s ->
+ Format.fprintf fmt "{@;<1 2>";
+ FieldMap.iter (pretty_field fmt) s.struct_value;
+ Format.fprintf fmt "@ }";
+ | Union u ->
+ Format.fprintf fmt "{@;<1 2>%t@ }"
+ (fun fmt -> pretty_field fmt u.union_field u.union_value)
+ | Array a ->
+ let indexes, sub = leading_indexes [()] a.array_value in
+ Format.fprintf fmt "%a = %a"
+ pretty_indexes indexes
+ pretty sub
+
+ let rec hash = function
+ | Default d -> Default.hash d
+ | Scalar s -> Hashtbl.hash (
+ Value.hash s.scalar_value,
+ Cil_datatype.Typ.hash s.scalar_type)
+ | Struct s -> Hashtbl.hash (
+ FieldMap.hash s.struct_value,
+ Cil_datatype.Compinfo.hash s.struct_info,
+ Default.hash s.struct_default)
+ | Union u -> Hashtbl.hash (
+ hash u.union_value,
+ Cil_datatype.Fieldinfo.hash u.union_field
+ )
+ | Array a -> Hashtbl.hash (
+ hash a.array_value,
+ Cil_datatype.Typ.hash a.array_cell_type)
+
+ let rec equal m1 m2 =
+ match m1, m2 with
+ | Default d1, Default d2 -> Default.equal d1 d2
+ | Scalar s1, Scalar s2 ->
+ Value.equal s1.scalar_value s2.scalar_value &&
+ Cil_datatype.Typ.equal s1.scalar_type s2.scalar_type
+ | Struct s1, Struct s2 ->
+ FieldMap.equal s1.struct_value s2.struct_value &&
+ Cil_datatype.Compinfo.equal s1.struct_info s2.struct_info
+ | Union u1, Union u2 ->
+ equal u1.union_value u2.union_value &&
+ Cil_datatype.Fieldinfo.equal u1.union_field u2.union_field
+ | Array a1, Array a2 ->
+ equal a1.array_value a2.array_value &&
+ Cil_datatype.Typ.equal a1.array_cell_type a2.array_cell_type
+ | (Default _ | Scalar _ | Struct _ | Union _ | Array _), _ -> false
+
+ let compare m1 m2 =
+ let (<?>) c (cmp,x,y) =
+ if c = 0 then cmp x y else c
+ in
+ match m1, m2 with
+ | Default d1, Default d2 -> Default.compare d1 d2
+ | Scalar s1, Scalar s2 ->
+ Value.compare s1.scalar_value s2.scalar_value <?>
+ (Cil_datatype.Typ.compare, s1.scalar_type, s2.scalar_type)
+ | Struct s1, Struct s2 ->
+ FieldMap.compare s1.struct_value s2.struct_value <?>
+ (Cil_datatype.Compinfo.compare, s1.struct_info, s2.struct_info)
+ | Union u1, Union u2 ->
+ compare u1.union_value u2.union_value <?>
+ (Cil_datatype.Fieldinfo.compare, u1.union_field, u2.union_field)
+ | Array a1, Array a2 ->
+ compare a1.array_value a2.array_value <?>
+ (Cil_datatype.Typ.compare, a1.array_cell_type, a2.array_cell_type)
+ | Default _, _ -> 1
+ | _, Default _ -> -1
+ | Scalar _, _ -> 1
+ | _, Scalar _ -> -1
+ | Struct _, _ -> 1
+ | _, Struct _ -> -1
+ | Union _, _ -> 1
+ | _, Union _ -> -1
+ end
+
+ (* Maps for structures : field -> node *)
+ and FieldMap :
+ Hptmap_sig.S
+ with type key = Cil_types.fieldinfo
+ and type v = Memory.t =
+ Hptmap.Make (Keys) (Memory) (Hptmap.Comp_unused) (Initial_Values) (Deps)
+
+ (* Caches *)
+
+ let cache_name s =
+ Hptmap_sig.PersistentCache ("Multidim_domain.(" ^ Value.name ^ ")." ^ s)
+
+ (* Datatype *)
+
+ include Memory
+
+ (* Default values *)
+
+ let top = Default Top
+
+ let zero = Default Zero
+
+ let default_to_value = function
+ | Top -> Value.top
+ | Zero -> Value.zero
+ | Numerical -> Value.top_numerical
+
+ let is_top m =
+ m = top
+(*
+ let std_compare =
+
+ let are_typ_compatible t1 2 =
+ match Cil.unrollType t1, Cil.unrollType t2 with
+ | TVoid _a1, TVoid _a2 -> true
+ | TInt (i1, _a1), TInt (i2, _a2) -> i1 = i2
+ | TFloat (f1, _a1), TFloat (f2, _a2) -> f1 = f2
+ | TPtr _, TPtr _ -> true
+ | TArray (t1, _size, _, _a1), TArray (t2, e2, _, _a2) ->
+ are_typ_compatible t1 t2
+ | TFun _, TFun _ -> true
+ | TComp (c1, _, _a1), TComp (c2, _, _a2) ->
+ c1.ckey = c2.ckey
+ in
+ if res <> 0 then res
+ else compare_attributes config _a1 _a2
+ | TEnum (e1, _a1), TEnum (e2, _a2) ->
+ compare_chain
+ (=?=) e1.ename e2.ename
+ (compare_attributes config) _a1 _a2
+ | TBuiltin_va_list _a1, TBuiltin_va_list _a2 ->
+ compare_attributes config _a1 _a2
+ | (TVoid _ | TInt _ | TFloat _ | TPtr _ | TArray _ | TFun _ | TNamed _ |
+ TComp _ | TEnum _ | TBuiltin_va_list _ as a1), a2 ->
+ index_typ a1 - index_typ a2
+
+ let match_array celltyp = function
+ |
+*)
+ let typ_size t =
+ Integer.of_int (Cil.bitsSizeOf t)
+
+ let are_typ_compatible t1 t2 =
+ Integer.equal (typ_size t1) (typ_size t2)
+
+ let are_scalar_compatible s1 s2 =
+ are_typ_compatible s1.scalar_type s2.scalar_type
+
+ let scalar_compatibility s1 s2 =
+ if are_scalar_compatible s1 s2
+ then Some (typ_size s1.scalar_type)
+ else None
+
+ let are_aray_compatible a1 a2 =
+ are_typ_compatible a1.array_cell_type a2.array_cell_type
+
+ let are_structs_compatible s1 s2 =
+ s1.struct_info.ckey = s2.struct_info.ckey
+
+ let are_union_compatible u1 u2 =
+ Cil_datatype.Fieldinfo.equal u1.union_field u2.union_field
+
+ let typ_size t =
+ Integer.of_int (Cil.bitsSizeOf t)
+
+ let type_range t =
+ Ival.inject_range (Some Integer.zero) (Some (typ_size t))
+
+ let is_included =
+ let cache = cache_name "is_included" in
+ let rec is_included m1 m2 = match m1, m2 with
+ | Default d1, Default d2 -> Default.is_included d1 d2
+ | _, Default Top -> true
+ | _, Default (Numerical | Zero) -> false
+ | Default Top, _ -> false
+ | Scalar s1, Scalar s2 ->
+ are_scalar_compatible s1 s2 &&
+ Value.(is_included s1.scalar_value s2.scalar_value)
+ | Default d, Scalar s ->
+ Value.(is_included (default_to_value d) s.scalar_value)
+ | Array a1, Array a2 ->
+ are_aray_compatible a1 a2 &&
+ is_included a1.array_value a2.array_value
+ | Default _, Array a2 ->
+ is_included m1 a2.array_value
+ | Struct s1, Struct s2 ->
+ are_structs_compatible s1 s2 &&
+ let decide_fast s t = if s == t then FieldMap.PTrue else PUnknown in
+ let decide_fst _fi m1 = is_included m1 (Default s2.struct_default) in
+ let decide_snd _fi m2 = is_included (Default s1.struct_default) m2 in
+ let decide_both _fi m1 m2 = is_included m1 m2 in
+ FieldMap.binary_predicate cache UniversalPredicate
+ ~decide_fast ~decide_fst ~decide_snd ~decide_both
+ s1.struct_value s2.struct_value
+ | Union u1, Union u2 ->
+ are_union_compatible u1 u2 &&
+ is_included u1.union_value u2.union_value
+ | Default _, Union u2 ->
+ is_included m1 u2.union_value
+ | Default _, Struct s2 ->
+ FieldMap.for_all (fun _key m2' -> is_included m1 m2') s2.struct_value
+ | Scalar _, (Array _ | Struct _ | Union _)
+ | Array _, (Scalar _ | Struct _ | Union _)
+ | Struct _, (Scalar _ | Array _ | Union _)
+ | Union _, (Scalar _ | Array _ | Struct _) -> false
+ in
+ is_included
+
+ let join f =
+ let cache = cache_name "join" in
+ let rec join m1 m2 =
+ match m1, m2 with
+ | _, Default Top | Default Top, _ -> Default Top
+ | Default d1, Default d2 -> Default (Default.join d1 d2)
+ | Scalar s1, Scalar s2 ->
+ begin match scalar_compatibility s1 s2 with
+ | Some size -> Scalar {
+ scalar_type = s1.scalar_type;
+ scalar_value = f ~size s1.scalar_value s2.scalar_value;
+ }
+ | None -> Default Top
+ end
+ | Scalar s, Default d | Default d, Scalar s ->
+ let size = typ_size s.scalar_type in
+ Scalar { s with
+ scalar_value = f ~size (default_to_value d) s.scalar_value;
+ }
+ | Array a1, Array a2 ->
+ if are_aray_compatible a1 a2
+ then Array { a1 with
+ array_value = join a1.array_value a2.array_value
+ }
+ else Default Top
+ | Array a, (Default d) | (Default d), Array a ->
+ Array { a with
+ array_value = join (Default d) a.array_value
+ }
+ | Struct s1, Struct s2 ->
+ if are_structs_compatible s1 s2 then
+ let empty_action = function
+ | Top -> FieldMap.Absorbing
+ | d ->
+ FieldMap.Traversing (fun _fi m -> Some (join (Default d) m))
+ in
+ let decide_both _fi = fun m1 m2 -> Some (join m1 m2)
+ and decide_left = empty_action s2.struct_default
+ and decide_right = empty_action s1.struct_default
+ in
+ let struct_value = FieldMap.merge ~cache
+ ~symmetric:false ~idempotent:true
+ ~decide_both ~decide_left ~decide_right
+ s1.struct_value s2.struct_value
+ in
+ Struct {
+ s1 with
+ struct_value;
+ struct_default = Default.join s1.struct_default s2.struct_default;
+ }
+ else Default Top
+ | Struct s, (Default d) | (Default d), Struct s ->
+ Struct { s with
+ struct_value = FieldMap.map (join (Default d)) s.struct_value;
+ struct_default = Default.join d s.struct_default ;
+ }
+ | Union u1, Union u2 ->
+ if are_union_compatible u1 u2
+ then Union { u1 with
+ union_value = join u1.union_value u2.union_value
+ }
+ else Default Top
+ | Union u, (Default d) | (Default d), Union u ->
+ Union { u with
+ union_value = join (Default d) u.union_value
+ }
+ | Scalar _, (Array _ | Struct _ | Union _)
+ | Array _, (Scalar _ | Struct _ | Union _)
+ | Struct _, (Scalar _ | Array _ | Union _)
+ | Union _, (Scalar _ | Array _ | Struct _) -> Default Top
+ in
+ join
+
+ let widen f =
+ let cache = cache_name "widen" in
+ let rec widen m1 m2 = match m1, m2 with
+ | _, Default _ | Default _, _ -> join f m1 m2
+ | Scalar s1, Scalar s2 ->
+ begin match scalar_compatibility s1 s2 with
+ | Some size -> Scalar {
+ scalar_type = s1.scalar_type;
+ scalar_value = f ~size s1.scalar_value s2.scalar_value;
+ }
+ | None -> Default Top
+ end
+ | Array a1, Array a2 ->
+ if are_aray_compatible a1 a2
+ then Array { a1 with
+ array_value = widen a1.array_value a2.array_value
+ }
+ else Default Top
+ | Struct s1, Struct s2 ->
+ if are_structs_compatible s1 s2 then
+ let empty_action = function
+ | Top -> FieldMap.Absorbing
+ | d ->
+ FieldMap.Traversing (fun _fi m -> Some (widen (Default d) m))
+ in
+ let decide_both _fi = fun m1 m2 -> Some (widen m1 m2)
+ and decide_left = empty_action s2.struct_default
+ and decide_right = empty_action s1.struct_default
+ in
+ let struct_value = FieldMap.merge ~cache
+ ~symmetric:false ~idempotent:true
+ ~decide_both ~decide_left ~decide_right
+ s1.struct_value s2.struct_value
+ in
+ Struct { s1 with
+ struct_value;
+ struct_default = Default.join s1.struct_default s2.struct_default;
+ }
+ else Default Top
+ | Union u1, Union u2 ->
+ if are_union_compatible u1 u2
+ then Union { u1 with
+ union_value = widen u1.union_value u2.union_value
+ }
+ else Default Top
+ | Scalar _, (Array _ | Struct _ | Union _)
+ | Array _, (Scalar _ | Struct _ | Union _)
+ | Struct _, (Scalar _ | Array _ | Union _)
+ | Union _, (Scalar _ | Array _ | Struct _) -> Default Top
+ in
+ widen
+
+ exception IncompatibleOffset of default
+
+ let rec read m = function
+ | NoOffset t -> m, t
+ | Field (fi, offset') ->
+ begin match m with
+ | Struct s when s.struct_info.ckey = fi.fcomp.ckey ->
+ begin try
+ let m' = FieldMap.find fi s.struct_value in
+ read m' offset'
+ with Not_found ->
+ raise (IncompatibleOffset s.struct_default) (* field undefined *)
+ end
+ | Union u when u.union_field.forder = fi.forder ->
+ read u.union_value offset'
+ | _ -> raise (IncompatibleOffset Top) (* structure mismatch *)
+ end
+ | Index (_index, elem_type, offset') ->
+ begin match m with
+ | Array a ->
+ if not (are_typ_compatible a.array_cell_type elem_type)
+ then raise (IncompatibleOffset Top) (* cell size not compatible *)
+ else read a.array_value offset'
+ | _ -> raise (IncompatibleOffset Top) (* structure mismatch *)
+ end
+
+ let reduce _f m offset =
+ match read m offset with
+ | Scalar s, typ when are_typ_compatible s.scalar_type typ -> s.scalar_value
+ | _ -> default_to_value Top
+ | exception (IncompatibleOffset d) -> default_to_value d
+
+ let extract _join m offset =
+ try
+ fst (read m offset)
+ with IncompatibleOffset d -> Default d
+
+ let rec write ~weak f m = function
+ | NoOffset t ->
+ f ~weak (m,t)
+ | Field (fi, offset') ->
+ if fi.fcomp.cstruct then (* Structures *)
+ let old = match m with
+ | Struct s when s.struct_info.ckey = fi.fcomp.ckey -> s
+ | _ -> {
+ struct_value = FieldMap.empty;
+ struct_info = fi.fcomp;
+ struct_default = match m with
+ | Default d -> d
+ | _ -> Top
+ }
+ in
+ let write' opt =
+ let old = Option.value ~default:(Default old.struct_default) opt in
+ Some (write f ~weak old offset')
+ in
+ Struct {
+ old with struct_value = FieldMap.replace write' fi old.struct_value
+ }
+ else (* Unions *)
+ let old = match m with
+ | Union u when u.union_field.forder = fi.forder -> u.union_value
+ | _ -> Default Top
+ in
+ Union {
+ union_value = write f ~weak old offset';
+ union_field = fi;
+ }
+ | Index (index, elem_type, offset') ->
+ let old = match m with
+ | Array a when are_typ_compatible a.array_cell_type elem_type ->
+ a.array_value
+ | Default _ -> m
+ | _ -> top
+ in
+ let weak = weak || not (Ival.(is_included top index)) in
+ Array {
+ array_value = write f ~weak old offset';
+ array_cell_type = elem_type
+ }
+
+ let initialize m offset d =
+ let f ~weak:_ (_m,_t) =
+ Default d
+ in
+ write ~weak:false f m offset
+
+ let set m offset v =
+ let f ~weak (_old,t) =
+ assert (not weak);
+ Scalar {
+ scalar_value = v;
+ scalar_type = t;
+ }
+ in
+ write ~weak:false f m offset
+
+ let update ~weak f' m offset =
+ let f ~weak (m,t) =
+ let old = match m with
+ | Scalar s when are_typ_compatible s.scalar_type t -> s.scalar_value
+ | Default d -> default_to_value d
+ | _ -> Value.top
+ in
+ Scalar {
+ scalar_value = f' ~weak old;
+ scalar_type = t;
+ }
+ in
+ write ~weak f m offset
+
+ let erase m offset =
+ let f ~weak:_ (_m,_t) =
+ top
+ in
+ write ~weak:false f m offset
+
+ let overwrite ~weak f dst offset src =
+ let f' ~weak:_ (m,_t) =
+ join (fun ~size:_ -> f ~weak) m src
+ in
+ write ~weak f' dst offset
+end
diff --git a/src/kernel_services/abstract_interp/memory_map.mli b/src/kernel_services/abstract_interp/memory_map.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a0371e0961c049e6253bb1a00a2590914b8f2a5c
--- /dev/null
+++ b/src/kernel_services/abstract_interp/memory_map.mli
@@ -0,0 +1,114 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+type size = Integer.t
+
+type default =
+ | Top (* Unknown everywhere *)
+ | Numerical (* Unknown but only numbers, no pointers at all *)
+ | Zero (* Zero everywhere *)
+
+(* Values the memory is mapped to *)
+module type Value =
+sig
+ type t
+
+ val name : string
+
+ val hash : t -> int
+ val equal : t -> t -> bool
+ val compare : t -> t -> int
+
+ val pretty : Format.formatter -> t -> unit
+ val zero : t
+ val misaligned : t -> t
+ val top : t
+ val top_numerical : t
+ val is_included : t -> t -> bool
+end
+
+module type Config =
+sig
+ val deps : State.t list
+end
+
+module type T =
+sig
+ type location
+ type value
+ type t
+
+ (* Datatype *)
+ val hash : t -> int
+ val equal : t -> t -> bool
+ val compare : t -> t -> int
+
+ (* Infinite unknown memory *)
+ val top : t
+
+ (* Infinite zero memory *)
+ val zero : t
+
+ (* Is the memory map completely unknown ? *)
+ val is_top : t -> bool
+
+ (* Get a unique value from a set of locations *)
+ val reduce : (value -> value -> value) -> t -> location -> value
+
+ (* Extract a sub map from a set of locations *)
+ val extract : (value -> value -> value) -> t -> location -> t
+
+ (* Set a default value on a set of locations *)
+ val initialize : t -> location -> default -> t
+
+ (* Set a unique value on a set of locations *)
+ val set : t -> location -> value -> t
+
+ (* Update values on a set of locations *)
+ val update : weak:bool -> (weak:bool -> value -> value) -> t -> location -> t
+
+ (* Set top on a set of locations *)
+ val erase : t -> location -> t
+
+ (* Copy a whole map over another *)
+ val overwrite : weak:bool -> (weak:bool -> value -> value -> value) -> t -> location -> t -> t
+
+ (* Test inclusion of one memory map into another *)
+ val is_included : t -> t -> bool
+
+ (* Finest partition that is coarcer than both *)
+ val join : (size:size -> value -> value -> value) -> t -> t -> t
+
+ (* Partition widening *)
+ val widen : (size:size -> value -> value -> value) -> t -> t -> t
+
+ val pretty : Format.formatter -> t -> unit
+end
+
+type typed_offset =
+ | NoOffset of Cil_types.typ
+ | Index of Ival.t * Cil_types.typ * typed_offset
+ | Field of Cil_types.fieldinfo * typed_offset
+
+module MakeTyped (Config : Config) (Value : Value) : T
+ with type value = Value.t
+ and type location = typed_offset
diff --git a/src/kernel_services/abstract_interp/multidim.ml b/src/kernel_services/abstract_interp/multidim.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2d8eca1853a60a390116faeb4e9654a5210a0799
--- /dev/null
+++ b/src/kernel_services/abstract_interp/multidim.ml
@@ -0,0 +1,203 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+type index = Integer.t * (Integer.t * Integer.t) list (* o, [dáµ¢,báµ¢]áµ¢ *)
+
+let pretty_int fmt i =
+ Integer.pretty ~hexa:false fmt i
+
+module Term =
+struct
+ type t = Integer.t * Integer.t
+
+ let pretty fmt (d,b) =
+ Format.fprintf fmt "%a×[..%a]" pretty_int d pretty_int b
+
+ let order (d1,_b1) (d2,_b2) = (* descending order *)
+ Integer.compare d2 d1
+
+ (* Keep the same interval but change the dimension (leading to
+ over-approximation, hence coarcer abstraction). This might
+ produce two terms instead of one *)
+ let coarsen (d,b) d' =
+ (* d×[0,b] -> (d'q + r)×[0,b] -> d'×[0,qb] + r×[0,b] *)
+ let q,r = Integer.e_div_rem d d' in
+ if Integer.is_zero r
+ then [ (d', Integer.mul q b) ]
+ else [ (d', Integer.mul q b) ; (r,b) ]
+
+ let mul (d1,b1) (d2,b2) =
+ Integer.mul d1 d2, Integer.mul b1 b2
+
+ let mul_integer i (d,b) =
+ Integer.mul d i, b
+end
+
+module Terms =
+struct
+ let hull sum =
+ List.fold_left (fun acc (d,b) -> Integer.(add acc (mul d b))) Integer.zero sum
+
+ (* Normalization *)
+
+ let reorder sum =
+ List.sort Term.order sum
+
+ let merge sum1 sum2 =
+ List.merge Term.order sum1 sum2
+
+ let normalize sum = (* sum must be sorted in descending order *)
+ let rec aux acc = function
+ | [] -> acc
+ | [term] -> term :: acc
+ | (d1,b1) :: (((d2,b2) :: l) as tail) -> (* Descending order : d1 > d2 *)
+ if Integer.equal d1 d2
+ then aux ((d1,Integer.add b1 b2) :: acc) l (* merge terms together *)
+ else if Integer.(lt (hull tail) d1)
+ then aux ((d1,b1) :: acc) tail (* do nothing *)
+ else aux acc (merge (Term.coarsen (d1,b1) d2) tail) (* coarsen d1 -> d2 *)
+ in
+ List.rev (aux [] sum)
+
+ let mul_term (d,b) sum =
+ List.map (Term.mul (d,b)) sum
+end
+
+module Prototype =
+struct
+ include Datatype.Undefined
+
+ type t = index
+
+ let name = "Multidim.SimplerIndex"
+
+ let pretty fmt (o,sum) =
+ Format.fprintf fmt "%a + %a"
+ (Integer.pretty ~hexa:false) o
+ (Pretty_utils.pp_list ~sep:" +@ " Term.pretty) sum
+
+ let reprs = [(Integer.zero,[])]
+end
+
+include Datatype.Make (Prototype)
+
+(* Constructors *)
+
+let zero = (Integer.zero,[])
+
+let of_integer i =
+ (i,[])
+
+let of_int i =
+ (Integer.of_int i,[])
+
+let of_ival ival =
+ try
+ (Ival.project_int ival,[])
+ with Ival.Not_Singleton_Int ->
+ match Ival.min_max_r_mod ival with (* Raises Abstract_interp.Error_Bottom *)
+ | None,_,_,_ | _,None,_,_ -> raise Abstract_interp.Error_Top
+ | Some l, Some u, _r, m ->
+ let u' = Integer.(c_div (sub u l) m) in
+ (l,[m,u'])
+
+(* Properties *)
+
+let is_zero = function
+ | o,[] when Integer.is_zero o -> true
+ | _ -> false
+
+let is_singleton = function
+ | _o,[] -> true
+ | _ -> false
+
+let hull (o,sum) =
+ o, Terms.hull sum
+
+(* Decomposition *)
+
+let first_dimension (o,sum) =
+ match sum with
+ | [] -> None
+ | (d,_b) :: tail ->
+ (* If normalized, no need to look in tail *)
+ Some (d, (Integer.e_rem o d,tail))
+
+(* Arithmetic *)
+
+let add (o1,sum1) (o2,sum2) =
+ Integer.add o1 o2, Terms.(normalize (merge sum1 sum2))
+
+let add_integer (o,sum) i =
+ (Integer.add o i, sum)
+
+let add_int x i =
+ add_integer x (Integer.of_int i)
+
+let sub_integer (o,sum) i =
+ (Integer.sub o i, sum)
+
+let sub_int x i =
+ sub_integer x (Integer.of_int i)
+
+let mul (o1,sum1) (o2,sum2) =
+ let sums =
+ List.map (Term.mul_integer o1) sum2 ::
+ List.map (Term.mul_integer o2) sum1 ::
+ List.map (fun t1 -> Terms.mul_term t1 sum2) sum1
+ in
+ let sum = List.fold_left Terms.merge [] sums in
+ Integer.mul o1 o2, Terms.normalize sum
+
+let mul_integer (o,sum) i =
+ Integer.mul o i, List.map (Term.mul_integer i) sum
+
+let mul_int x i =
+ mul_integer x (Integer.of_int i)
+
+let mod_integer (o,sum) i =
+ (* mod everything *)
+ let o = Integer.e_rem o i in
+ let sum = Extlib.filter_map'
+ (fun (d,b) -> Integer.e_rem d i, b)
+ (fun (d,_b) -> not (Integer.is_zero d))
+ sum
+ in
+ let sum = Terms.(normalize (reorder sum)) in (* order was not preserverd *)
+ (* We must then ensure that the set of represented offset is < i,
+ i.e. that the highest possible value is < i.
+ After normalization, this reduces to check that d*b + o < i.
+ If it is not the case, we coarcen (d,b) to d' = pgcd(d,i) and use the
+ greatest possible b' = i / d' *)
+ match sum with
+ | [] -> (o,[])
+ | (d,b) :: tail ->
+ if Integer.(lt (add (mul d b) o) i)
+ then (o,sum) (* hull is ok, this is our result *)
+ else
+ let d' = Integer.pgcd d i in
+ let b' = Integer.(pred (e_div i d')) in
+ let o' = Integer.e_rem o d' in
+ o', Terms.(normalize (merge [(d',b')] tail))
+
+let mod_int x i =
+ mod_integer x (Integer.of_int i)
diff --git a/src/kernel_services/abstract_interp/multidim.mli b/src/kernel_services/abstract_interp/multidim.mli
new file mode 100644
index 0000000000000000000000000000000000000000..69cb39e01e14d4911509354fecf7ea17a606f7be
--- /dev/null
+++ b/src/kernel_services/abstract_interp/multidim.mli
@@ -0,0 +1,77 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** [offset] is an abstraction for array indexes when these
+ arrays are used as a representation of multidimensional arrays or
+ structures. They have the form :
+
+ o + dâ‚×[0,bâ‚] + ... + dₙ×[0,bâ‚™]
+
+ or, more formally
+
+ { o + Σ dᵢ×xᵢ | ∀i 1≤i≤n ⇒ xᵢ ∊ [0, bᵢ] }
+
+ This is a generalisation of integers intervals with modulo implemented in
+ Ival : o + d×[0, b]
+
+ The list of dáµ¢ is sorted in descending order and we may add the constraint
+
+ dᵢ×báµ¢ < dᵢ₋â‚
+
+ which is verified for normal multidimensional arrays handling.
+*)
+type index = Integer.t * (Integer.t * Integer.t) list (* o, [dáµ¢,báµ¢]áµ¢ *)
+
+include Datatype.S with type t = index
+
+(* Constructors *)
+
+val zero : t
+val of_int : int -> t
+val of_integer : Integer.t -> t
+val of_ival : Ival.t -> t (* Raises Abstract_interp.Error_Bottom and Error_Top *)
+
+(* Properties *)
+
+val is_zero : t -> bool
+val is_singleton : t -> bool
+val hull : t -> Integer.t * Integer.t (* start * size *)
+
+(* Decomposition *)
+
+val first_dimension : t -> (Integer.t * t) option
+
+(* Arithmetic *)
+
+val add : t -> t -> t
+(* slightly faster than add since no normalization takes place *)
+val add_int : t -> int -> t
+val add_integer : t -> Integer.t -> t
+val sub_int : t -> int -> t
+val sub_integer : t -> Integer.t -> t
+
+val mul : t -> t -> t
+val mul_int : t -> int -> t
+val mul_integer : t -> Integer.t -> t
+
+val mod_int : t -> int -> t
+val mod_integer : t -> Integer.t -> t
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
new file mode 100644
index 0000000000000000000000000000000000000000..853471ee3344eb42d1d85292697ec7ee068aff8d
--- /dev/null
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -0,0 +1,804 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Eval
+
+[@@@warning "-60"] (* unused module *)
+[@@@warning "-32"] (* unused value *)
+
+let dkey = Value_parameters.register_category "d-multidim"
+
+let map_to_singleton map =
+ let aux base offset = function
+ | None -> Some (base, offset)
+ | Some _ -> raise Exit
+ in
+ try Base.Base.Map.fold aux map None with Exit -> None
+
+module Value =
+struct
+ include Cvalue.V
+
+ let _to_integer cvalue =
+ try Some (Ival.project_int (project_ival cvalue))
+ with Not_based_on_null | Ival.Not_Singleton_Int -> None
+
+ let of_integer = inject_int
+
+ let zero = inject_int Integer.zero
+
+ let misaligned _v = top
+
+ let backward_is_finite positive fkind v =
+ let prec = Fval.kind fkind in
+ try
+ let v = reinterpret_as_float fkind v in
+ Fval.backward_is_finite ~positive prec (project_float v) >>-: inject_float
+ with Not_based_on_null ->
+ `Value v
+
+ let top = top (* Locations.Location_Bytes.top_with_origin Origin.top *)
+ let top_numerical = top_int
+end
+
+let no_oracle exp =
+ match Cil.isInteger exp with
+ | None -> raise Abstract_interp.Error_Top
+ | Some i -> Value.of_integer i
+
+
+type assigned = (Precise_locs.precise_location,Value.t) Eval.assigned
+type builtin = assigned list -> assigned or_bottom
+
+let builtins : (string * builtin) list = []
+
+let find_builtin =
+ let module Table = Stdlib.Hashtbl in
+ let table = Table.create 17 in
+ List.iter (fun (name, f) -> Table.replace table name f) builtins;
+ fun kf ->
+ try Some (Table.find table (Kernel_function.get_name kf))
+ with Not_found -> None
+
+
+module MultidimOffset =
+struct
+ include Multidim
+
+ let field fi x =
+ let field_offset, field_size = Cil.fieldBitsOffset fi in
+ add_int x field_offset, Integer.of_int field_size
+
+ let index elem_typ index x =
+ let elem_size = Integer.of_int (Cil.bitsSizeOf elem_typ) in
+ add x (mul_integer index elem_size), elem_size
+
+ let rec of_exp oracle = function
+ | { Cil_types.enode=BinOp (PlusA,e1,e2,_typ) } ->
+ add (of_exp oracle e1) (of_exp oracle e2)
+ | { enode=BinOp (Mult,e1,e2,_typ) } ->
+ mul (of_exp oracle e1) (of_exp oracle e2)
+ | { enode=BinOp (Shiftlt,e1,e2,_typ) } as expr ->
+ begin match oracle e2 with
+ | (i,[]) -> mul_integer (of_exp oracle e1) (Integer.two_power i)
+ | _ -> oracle expr (* default to oracle *)
+ end
+ | expr -> oracle expr (* default to oracle *)
+
+ let assert_valid_size idx _array_size =
+ idx
+
+ let of_offset oracle base_typ offset =
+ let rec aux base_typ base_size x = function
+ | Cil_types.NoOffset -> x, base_size
+ | Field (fi, sub) ->
+ let x', size = field fi x in
+ aux fi.ftype size x' sub
+ | Index (exp, sub) ->
+ match base_typ with
+ | TArray (elem_typ, array_size, _, _) ->
+ let idx = of_exp oracle exp in
+ let idx = assert_valid_size idx array_size in
+ let x', elem_size = index elem_typ idx x in
+ aux elem_typ elem_size x' sub
+ | _ -> assert false (* Index is only valid on arrays *)
+ in
+ let base_size = Integer.of_int (Cil.bitsSizeOf base_typ) in
+ aux base_typ base_size zero offset
+end
+
+(* Multidim adresses building from valuation *)
+
+module MultidimLocation =
+struct
+ module Map = Base.Base.Map
+
+ type size = Integer.t
+ type offset = MultidimOffset.t
+ type t = offset Map.t * size
+
+ let size ((_map,size) : t) : size =
+ size
+
+ let fold f ((map,size):t) x =
+ Map.fold (fun base offset -> f base (offset,size)) map x
+
+ (* Raises Abstract_domain.{Error_top,Error_bottom} *)
+ let of_lval oracle ((host,offset) : Cil_types.lval) =
+ let oracle' expr =
+ try MultidimOffset.of_ival (Value.project_ival (oracle expr))
+ with Value.Not_based_on_null -> raise Abstract_interp.Error_Top
+ in
+ let base_typ = Cil.typeOfLhost host in
+ let offset, size = MultidimOffset.of_offset oracle' base_typ offset in
+ let map = match host with
+ | Var vi ->
+ Map.singleton (Base.of_varinfo vi) offset
+ | Mem exp ->
+ let add b o map =
+ Map.add b MultidimOffset.(add (of_ival o) offset) map
+ in
+ Locations.Location_Bytes.fold_topset_ok add (oracle exp) Map.empty
+ in
+ map, size
+
+ let is_singleton (map,_) =
+ match map_to_singleton map with
+ | None -> false
+ | Some (b,o) -> not (Base.is_weak b) && MultidimOffset.is_singleton o
+end
+
+
+module Offset =
+struct
+ open Memory_map
+ type t = [ `Value of typed_offset | `Top ]
+
+ let append o1 o2 =
+ let rec aux o1 o2 =
+ match o1 with
+ | NoOffset _t -> o2
+ | Field (fi, s) -> Field (fi, aux s o2)
+ | Index (i, t, s) -> Index (i, t, aux s o2)
+ in
+ match o1, o2 with
+ | `Top, _ | _, `Top -> `Top
+ | `Value o1, `Value o2 -> `Value (aux o1 o2)
+
+ let join o1 o2 =
+ let rec aux o1 o2 =
+ match o1, o2 with
+ | NoOffset t, NoOffset t' when Cil_datatype.Typ.equal t t' ->
+ NoOffset t
+ | Field (fi, s1), Field (fi', s2) when Cil_datatype.Fieldinfo.equal fi fi' ->
+ Field (fi, aux s1 s2)
+ | Index (i1, t, s1), Index (i2, t', s2) when Cil_datatype.Typ.equal t t' ->
+ Index (Ival.join i1 i2, t, aux s1 s2)
+ | _ -> raise Abstract_interp.Error_Top
+ in
+ match o1, o2 with
+ | `Top, _ | _, `Top -> `Top
+ | `Value o1, `Value o2 ->
+ try `Value (aux o1 o2) with Abstract_interp.Error_Top -> `Top
+
+ let assert_valid_size idx _array_size =
+ idx
+
+ let of_offset oracle base_typ offset =
+ (* Temorary debug *)
+ let rec aux base_typ = function
+ | Cil_types.NoOffset -> NoOffset base_typ
+ | Field (fi, sub) -> Field (fi, aux fi.ftype sub)
+ | Index (exp, sub) ->
+ match Cil.unrollType base_typ with
+ | TArray (elem_typ, array_size, _, _) ->
+ let idx =
+ try Value.project_ival (oracle exp)
+ with Value.Not_based_on_null -> raise Abstract_interp.Error_Top
+ in
+ let idx = assert_valid_size idx array_size in
+ Index (idx, elem_typ, aux elem_typ sub)
+ | _ -> assert false
+ in
+ try `Value (aux base_typ offset) with Abstract_interp.Error_Top -> `Top
+
+ let of_bits_offset base_typ typ i =
+ try
+ let offset, _t = Bit_utils.(find_offset base_typ i (MatchType typ)) in
+ (* typ and _t may be different *)
+ of_offset no_oracle base_typ offset
+ with Bit_utils.NoMatchingOffset ->
+ `Top
+
+ let of_ival base_typ typ ival =
+ match Ival.cardinal ival with
+ | Some c when Integer.(lt c (of_int 100)) ->
+ let f i acc =
+ let offset = of_bits_offset base_typ typ i in
+ match acc with
+ | `Bottom -> offset
+ | #t as prev -> join prev offset
+ in
+ begin match Ival.fold_int f ival `Bottom with
+ | `Bottom -> assert false (* ival should not be bottom *)
+ | #t as o -> o
+ end
+
+ | _ ->
+ Value_parameters.feedback ~dkey ~current:true ~once:true
+ "too many values to convert cvalues to multidim offset";
+ `Top
+
+ let index_of_term t =
+ match t.term_node with
+ | Tempty_set -> Ival.bottom
+ | TConst (Integer (v, _)) -> Ival.inject_singleton v
+ | Trange (l,u) ->
+ let eval_bound = function
+ | { term_node=TConst (Integer (v, _)) } -> v
+ | _ -> raise Abstract_interp.Error_Top
+ in
+ let l' = Option.map eval_bound l
+ and u' = Option.map eval_bound u in
+ Ival.inject_range l' u'
+ | _ -> raise Abstract_interp.Error_Top
+
+ let of_term_offset base_typ offset =
+ let rec aux base_typ = function
+ | Cil_types.TNoOffset -> NoOffset base_typ
+ | TField (fi, sub) ->
+ Field (fi, aux fi.ftype sub)
+ | TIndex (index, sub) ->
+ begin match Cil.unrollType base_typ with
+ | TArray (elem_typ, array_size, _, _) ->
+ let idx = index_of_term index in
+ let idx = assert_valid_size idx array_size in
+ Index (idx, elem_typ, aux elem_typ sub)
+ | _ -> assert false
+ end
+ | _ -> raise Abstract_interp.Error_Top
+ in
+ try `Value (aux base_typ offset) with Abstract_interp.Error_Top -> `Top
+
+ let is_singleton =
+ let rec aux = function
+ | NoOffset _ -> true
+ | Field (_fi, sub) -> aux sub
+ | Index (ival, _elem_typ, sub) ->
+ Ival.is_singleton_int ival && aux sub
+ in function
+ | `Top -> false
+ | `Value o -> aux o
+end
+
+module Location =
+struct
+ module Map = Base.Base.Map
+
+ type offset = Offset.t
+ type t = offset Map.t
+
+ let empty = Map.empty
+
+ let fold = Map.fold
+
+ let is_singleton map =
+ match map_to_singleton map with
+ | None -> false
+ | Some (b,o) ->
+ not (Base.is_weak b) && Offset.is_singleton o
+
+ (* Raises Abstract_domain.{Error_top,Error_bottom} *)
+ let of_lval oracle ((host,offset) as lval : Cil_types.lval) : t =
+ let base_typ = Cil.typeOfLhost host in
+ let offset : Offset.t = Offset.of_offset oracle base_typ offset in
+ match host with
+ | Var vi ->
+ Map.singleton (Base.of_varinfo vi) offset
+ | Mem exp ->
+ let add base ival map =
+ let offset' : Offset.t =
+ match Base.typeof base with
+ | None -> `Top
+ | Some base_typ ->
+ let typ = Cil.typeOfLval lval in
+ Offset.(append (of_ival base_typ typ ival) offset)
+ in
+ Map.add base offset' map
+ in
+ let loc = Locations.loc_bytes_to_loc_bits (oracle exp) in
+ Locations.Location_Bits.fold_i add loc Map.empty
+
+ let of_term_lval env ((lhost, offset) as lval) =
+ let vi = match lhost with
+ | TVar ({lv_origin=Some vi}) -> vi
+ | TResult _ -> Option.get env.Abstract_domain.result
+ | _ -> raise Abstract_interp.Error_Top
+ in
+ let base' = Base.of_varinfo vi in
+ let offset' = Offset.of_term_offset vi.vtype offset in
+ Map.singleton base' offset', Cil.typeOfTermLval lval
+
+ let of_term env t =
+ match t.term_node with
+ | TLval term_lval -> of_term_lval env term_lval
+ | _ -> raise Abstract_interp.Error_Top
+
+ let of_precise_loc loc =
+ let loc' = Precise_locs.imprecise_location loc in
+ 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 Memory_map.(NoOffset typ)) map
+ in
+ Locations.Location_Bits.(fold_bases add_base loc'.loc empty)
+end
+
+
+(* The domain for *one* base *)
+
+module Base_Domain =
+struct
+ module Config = struct let deps = [Ast.self] end
+ module Memory = Memory_map.MakeTyped (Config) (Value)
+
+ module Prototype =
+ (* Datatype *)
+ struct
+ include Datatype.Undefined
+ include Memory
+ let name = "Multidim_domain.Base_Domain"
+ let reprs = [ Memory.top ]
+ end
+
+ include Datatype.Make (Prototype)
+
+ let pretty = Memory.pretty
+ let pretty_debug = Memory.pretty
+ let top = Memory.top
+ let is_top = Memory.is_top
+ let is_included = Memory.is_included
+ let narrow = fun m1 _m2 -> m1
+ let join = Memory.join (fun ~size:_ v1 v2 -> Value.join v1 v2)
+ let widen h = Memory.widen (fun ~size v1 v2 -> Value.widen (size,h) v1 v2)
+
+ let get m loc =
+ match loc with
+ | `Top -> Value.top
+ | `Value loc -> Memory.reduce Value.join m loc
+
+ let extract m loc =
+ match loc with
+ | `Top -> Memory.top
+ | `Value loc -> Memory.extract Value.join m loc
+
+ let initialize m loc init_value =
+ match loc with
+ | `Top -> Memory.top
+ | `Value loc -> Memory.initialize m loc init_value
+
+ let update ~weak new_v m loc =
+ match loc with
+ | `Top -> Memory.top
+ | `Value loc ->
+ let f ~weak old_v =
+ if weak
+ then Value.join old_v new_v
+ else new_v
+ in
+ Memory.update ~weak f m loc
+
+ let reduce f m loc =
+ match loc with
+ | `Top -> m
+ | `Value loc ->
+ let f' ~weak x =
+ if weak
+ then x
+ else
+ match f x with
+ | `Value v -> v
+ | `Bottom -> raise Abstract_interp.Error_Bottom
+ in
+ Memory.update ~weak:false f' m loc
+
+ let erase m loc =
+ match loc with
+ | `Top -> m
+ | `Value loc ->
+ Memory.erase m loc
+
+ let overwrite ~weak dst loc src =
+ match loc with
+ | `Top -> Memory.top
+ | `Value loc ->
+ let f ~weak old_v new_v =
+ if weak
+ then Value.join old_v new_v
+ else new_v
+ in
+ Memory.overwrite ~weak f dst loc src
+end
+
+
+module Prototype =
+struct
+ (* The domain is essentially a map from bases to individual memory abstractions *)
+ module Initial_Values = struct let v = [] end
+ module Deps = struct let l = [Ast.self] end
+
+ include Hptmap.Make
+ (Base.Base) (Base_Domain)
+ (Hptmap.Comp_unused) (Initial_Values) (Deps)
+
+ type state = t
+ type value = Value.t
+ type base = Base.t
+ type location = Precise_locs.precise_location
+ type mdlocation = Location.t (* should be = to location *)
+ type origin
+
+
+ let name = "Multidim domain"
+ let log_category = dkey
+
+ let cache_name s =
+ Hptmap_sig.PersistentCache ("Multidim_domain." ^ s)
+
+
+ (* Lattice *)
+
+ let top = empty
+
+ let is_included =
+ let cache = cache_name "is_included" in
+ let decide_fst _b _v1 = true (* v2 is top *) in
+ let decide_snd _b _v2 = false (* v1 is top, v2 is not *) in
+ let decide_both _ v1 v2 = Base_Domain.is_included v1 v2 in
+ let decide_fast s t = if s == t then PTrue else PUnknown in
+ binary_predicate cache UniversalPredicate
+ ~decide_fast ~decide_fst ~decide_snd ~decide_both
+
+ let narrow =
+ let cache = cache_name "narrow" in
+ let decide _ v1 v2 =
+ Base_Domain.narrow v1 v2
+ in
+ fun a b ->
+ `Value (join ~cache ~symmetric:true ~idempotent:true ~decide a b)
+
+ let join =
+ let cache = cache_name "join" in
+ let decide _ v1 v2 =
+ let r = Base_Domain.join v1 v2 in
+ if Base_Domain.(is_top r) then None else Some r
+ in
+ inter ~cache ~symmetric:true ~idempotent:true ~decide
+
+ let widen =
+ let cache = cache_name "widen" in
+ fun kf stmt ->
+ let _,get_hints = Widen.getWidenHints kf stmt in
+ let decide base b1 b2 =
+ let r = Base_Domain.widen (get_hints base) b1 b2 in
+ if Base_Domain.(is_top r) then None else Some r
+ in
+ inter ~cache ~symmetric:false ~idempotent:true ~decide
+
+
+ (* Bases handling *)
+
+ let covers_base (b : base) =
+ match b with
+ | Base.Var (vi, _) | Allocated (vi, _, _) ->
+ not (Cil.typeHasQualifier "volatile" vi.vtype)
+ | Null -> true
+ | CLogic_Var _ | String _ -> false
+
+ let find_or_top (state : state) (b : base) =
+ try find b state with Not_found -> Base_Domain.top
+
+ let remove_var (state : state) (v : Cil_types.varinfo) =
+ remove (Base.of_varinfo v) state
+
+ let remove_vars (state : state) (l : Cil_types.varinfo list) =
+ List.fold_left remove_var state l
+
+ let remove (state : state) (loc : location) =
+ let loc = Precise_locs.imprecise_location loc in
+ Locations.(Location_Bits.fold_bases remove loc.loc state)
+
+ (* Accesses *)
+
+ let load (state : state) (src : mdlocation) : value =
+ let load_base base loc r =
+ let v = Base_Domain.get (find_or_top state base) loc in
+ Bottom.join Value.join r (`Value v)
+ in
+ match Location.fold load_base src `Bottom with
+ | `Bottom -> Value.top (* does not happen if the location is not empty *)
+ | `Value v -> v
+
+ let extract (state : state) (src : mdlocation) : Base_Domain.t or_bottom =
+ let extract_base base loc acc =
+ let map = find_or_top state base in
+ let value = Base_Domain.extract map loc in
+ Bottom.join Base_Domain.join acc (`Value value)
+ in
+ Location.fold extract_base src `Bottom
+
+ let store (state : state) (dst : mdlocation) (v : value) =
+ let weak = not (Location.is_singleton dst) in
+ let store_base base loc state =
+ if covers_base base then
+ add base (Base_Domain.update ~weak v (find_or_top state base) loc) state
+ else
+ state
+ in
+ Location.fold store_base dst state
+
+ let overwrite (state : state) (dst : mdlocation) (src : mdlocation) =
+ (* assert (Location.size dst = Location.size src); *)
+ let weak = not (Location.is_singleton dst) in
+ match extract state src with
+ | `Bottom -> state (* no source *)
+ | `Value value ->
+ let overwrite_base base loc state =
+ if covers_base base then
+ let map = find_or_top state base in
+ add base (Base_Domain.overwrite ~weak map loc value) state
+ else
+ state (* destination base not covered : do nothing *)
+ in
+ Location.fold overwrite_base dst state
+
+ let erase (state : state) (dst : mdlocation) =
+ let erase_base base loc state =
+ if mem base state
+ then add base (Base_Domain.erase (find_or_top state base) loc) state
+ else state
+ in
+ Location.fold erase_base dst state
+
+ let update_loc (f : value -> value or_bottom) loc state =
+ let update_base base loc state =
+ if covers_base base then
+ let map = find_or_top state base in
+ add base (Base_Domain.reduce f map loc) state
+ else
+ state (* destination base not covered : do nothing *)
+ in
+ Location.fold update_base loc state
+
+ let initialize dst init_value state =
+ (* dst must be exact, otherwise, we may initialize things that shouldn't *)
+ let initialize_base base loc state =
+ if covers_base base then
+ let map = find_or_top state base in
+ add base (Base_Domain.initialize map loc init_value) state
+ else
+ state
+ in
+ Location.fold initialize_base dst state
+
+ (* Eva Queries *)
+
+ (* Nothing interesting to be done on expressions *)
+ let extract_expr ~oracle:_ _context _state _expr =
+ `Value (Value.top, None), Alarmset.all
+
+ let extract_lval ~oracle _context state lv _typ _loc =
+ let oracle = fun exp ->
+ match oracle exp with
+ | `Bottom, _ -> raise Abstract_interp.Error_Bottom
+ | `Value v, _ -> v
+ in
+ let v =
+ try
+ let loc = Location.of_lval oracle lv in
+ load state loc
+ with Abstract_interp.Error_Top | Abstract_interp.Error_Bottom -> Value.top
+ in
+ `Value (v, None), Alarmset.all
+
+ (* do nothing for now *)
+ let backward_location _state _lval _typ loc value =
+ `Value (loc, value)
+
+ (* do nothing for now *)
+ let reduce_further _state _expr _value = []
+
+
+ (* Eva Transfer *)
+
+ let make_oracle valuation : Cil_types.exp -> value = fun exp ->
+ match valuation.Abstract_domain.find exp with
+ | `Top -> raise Abstract_interp.Error_Top
+ | `Value {value={v=`Bottom}} -> raise Abstract_interp.Error_Bottom
+ | `Value {value={v=`Value value}} -> value
+
+ let assume_exp valuation expr record state =
+ let oracle = make_oracle valuation in
+ try
+ match expr.enode, record.value.v with
+ | Lval lv, `Value value ->
+ let loc = Location.of_lval oracle lv in
+ if Location.is_singleton loc
+ then store state loc value
+ else state
+ | _, `Bottom -> state (* Indeterminate value, ignore *)
+ | _ -> state
+ with
+ (* Failed to evaluate the location *)
+ Abstract_interp.Error_Top | Abstract_interp.Error_Bottom -> state
+
+ let assume_valuation valuation state =
+ valuation.Abstract_domain.fold (assume_exp valuation) state
+
+ let update valuation state =
+ `Value (assume_valuation valuation state)
+
+ let assign_lval lval assigned_value oracle state =
+ try
+ let dst = Location.of_lval oracle lval in
+ match assigned_value with
+ | Assign value ->
+ `Value (store state dst value)
+ | Copy (right, _value) ->
+ try
+ let src = Location.of_lval oracle right.lval in
+ `Value (overwrite state dst src)
+ with Abstract_interp.Error_Top | Abstract_interp.Error_Bottom ->
+ `Value (erase state dst)
+ with Abstract_interp.Error_Top | Abstract_interp.Error_Bottom ->
+ (* Failed to evaluate the left location *)
+ `Value top
+
+ let assign _kinstr left _expr assigned_value valuation state =
+ let state = assume_valuation valuation state in
+ let oracle = make_oracle valuation in
+ assign_lval left.lval assigned_value oracle state
+
+ let assume _stmt _expr _pos valuation state =
+ `Value (assume_valuation valuation state)
+
+ let start_call _stmt call valuation state =
+ let oracle = make_oracle valuation in
+ let bind state arg =
+ state >>- assign_lval (Cil.var arg.formal) arg.avalue oracle
+ in
+ List.fold_left bind (`Value state) call.arguments
+
+ let finalize_call _stmt call ~pre:_ ~post =
+ match find_builtin call.kf, call.return with
+ | None, _ | _, None -> `Value post
+ | Some f, Some return ->
+ let args = List.map (fun arg -> arg.avalue) call.arguments in
+ f args >>- fun assigned_result ->
+ assign_lval (Cil.var return) assigned_result no_oracle post
+
+ let show_expr valuation state fmt expr =
+ match expr.enode with
+ | Lval lval | StartOf lval ->
+ begin try
+ let oracle = make_oracle valuation in
+ let loc = Location.of_lval oracle lval in
+ match extract state loc with
+ | `Bottom -> Format.fprintf fmt "⊥"
+ | `Value value -> Base_Domain.pretty fmt value
+ with Abstract_interp.Error_Top | Abstract_interp.Error_Bottom ->
+ (* can't evaluate location : print nothing *)
+ ()
+ end
+ | _ -> ()
+
+ let enter_scope _kind _vars state = state
+ let leave_scope _kf vars state = remove_vars state vars
+
+ let enter_loop _ state = state
+ let incr_loop_counter _ state = state
+ let leave_loop _ state = state
+
+ let logic_assign assign location state =
+ match assign with
+ | None -> remove state location
+ | Some ((Frees _ | Allocates _), _) -> state
+ | Some (Assigns (_it, from), pre_state) ->
+ match from with
+ | FromAny | From (_ :: _) -> remove state location
+ | From [] ->
+ let _env = {
+ Abstract_domain.states = begin function
+ | Cil_types.(BuiltinLabel (Pre | Here)) -> pre_state
+ | _ -> assert false
+ end;
+ Abstract_domain.result = None
+ } in
+ (* let _dst,_typ = Location.of_term env it.it_content in *)
+ let dst = Location.of_precise_loc location in
+ initialize dst Memory_map.Numerical state
+
+ let evaluate_predicate _ _ _ = Alarmset.Unknown
+
+ let reduce_by_papp env li _labels args positive state =
+ try
+ match li.l_var_info.lv_name, args with
+ | "\\are_finite", [arg] ->
+ let loc,typ = Location.of_term env arg in
+ begin match Cil.unrollType (Logic_utils.logicCType typ) with
+ | TFloat (fkind,_) ->
+ let update = Value.backward_is_finite positive fkind in
+ `Value (update_loc update loc state)
+ | _ | exception (Failure _) -> `Value state
+ end
+ | _ -> `Value state
+ with
+ | Abstract_interp.Error_Bottom -> `Bottom
+ | Abstract_interp.Error_Top -> `Value state
+
+ let reduce_by_predicate env state predicate truth =
+ let rec reduce predicate truth state =
+ match truth, predicate.pred_content with
+ | true, Pand (p1,p2) | false, Por (p1,p2) ->
+ state |> reduce p1 truth >>- reduce p2 truth
+ | _,Papp (li, labels, args) ->
+ reduce_by_papp env li labels args truth state
+ | _ -> `Value state
+ in
+ reduce predicate truth state
+
+ let empty () = top
+
+ let initialize_variable lval _loc ~initialized:_ init_value state =
+ let dst = Location.of_lval no_oracle lval in
+ let d = match init_value with
+ | Abstract_domain.Top -> Memory_map.Numerical
+ | Abstract_domain.Zero -> Memory_map.Zero
+ in
+ initialize dst d state
+
+ let initialize_variable_using_type _kind vi state =
+ let lval = Cil.var vi in
+ let dst = Location.of_lval no_oracle lval in
+ initialize dst Memory_map.Top state
+
+ let relate _kf _bases _state = Base.SetLattice.empty
+
+ let filter _kf _kind bases state =
+ filter (fun elt -> Base.Hptset.mem elt bases) state
+
+ let reuse _kf bases ~current_input ~previous_output =
+ let cache = Hptmap_sig.NoCache in
+ let decide_both _key _v1 v2 = Some v2 in
+ let decide_left key v1 =
+ if Base.Hptset.mem key bases then None else Some v1
+ in
+ merge ~cache ~symmetric:false ~idempotent:true
+ ~decide_both ~decide_left:(Traversing decide_left) ~decide_right:Neutral
+ current_input previous_output
+
+ let storage () = true
+end
+
+
+include Domain_builder.Complete (Prototype)
diff --git a/src/plugins/value/domains/multidim_domain.mli b/src/plugins/value/domains/multidim_domain.mli
new file mode 100644
index 0000000000000000000000000000000000000000..de7e2068dc1ea65d6c7b5c88b287ff56301fa629
--- /dev/null
+++ b/src/plugins/value/domains/multidim_domain.mli
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+include Abstract_domain.Leaf
+ with type value = Cvalue.V.t
+ and type location = Precise_locs.precise_location
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 46f01c2f6b4eead6fee75da5a42cfa407953f05e..4497123b4939d86b5fd792333827c942b3db319c 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -172,6 +172,12 @@ module Config = struct
to a statement."
(module Traces_domain.D)
+ let multidim =
+ make 2 "multidim" ~experimental:true
+ "Improve the precision over arrays of structures or multidimensional \
+ arrays."
+ (module Multidim_domain)
+
let printer =
make 2 "printer"
"Debug domain, only useful for developers. Prints the transfer functions \
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index 38364d3fc5b1fb1bbfc52647df1963840922a6fb..28d169c63d173f5b67d370858deaac31b3ef44cf 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -158,6 +158,7 @@ module Config : sig
val taint: flag
val sign: flag
val traces: flag
+ val multidim: flag
val printer: flag
val default: t (** The default configuration of Eva. *)
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index a3d0cb97c5034a4eff502b76729e1d3245bf20a6..b6cf1f8372e87e9f32484e878209d371c6600147 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -137,7 +137,8 @@ module Domains =
let option_name = "-eva-domains"
let arg_name = "d1,...,dn"
let help = "Enable a list of analysis domains."
- let default = Datatype.String.Set.singleton "cvalue"
+ let default = Datatype.String.Set.of_list ["cvalue"]
+ (* let default = Datatype.String.Set.singleton "cvalue" *)
end)
let () = add_precision_dep Domains.parameter