diff --git a/src/kernel_services/abstract_interp/function_Froms.ml b/src/kernel_services/abstract_interp/function_Froms.ml
deleted file mode 100644
index f6f2f5e8a931121cbb58b2d66caf6c5fdaa4e3e5..0000000000000000000000000000000000000000
--- a/src/kernel_services/abstract_interp/function_Froms.ml
+++ /dev/null
@@ -1,633 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* 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 Locations
-
-module Deps =
-struct
-
- type deps = {
- data: Zone.t;
- indirect: Zone.t;
- }
-
- let to_zone {data; indirect} = Zone.join data indirect
-
- module DatatypeFromDeps = Datatype.Make(struct
- type t = deps
-
- let name = "Function_Froms.Deps.from_deps"
-
- let hash fd =
- Zone.hash fd.data + 37 * Zone.hash fd.indirect
-
- let compare fd1 fd2 =
- let c = Zone.compare fd1.data fd2.data in
- if c <> 0 then c
- else Zone.compare fd1.indirect fd2.indirect
-
- let equal = Datatype.from_compare
-
- let pretty fmt d = Zone.pretty fmt (to_zone d)
-
- let reprs =
- List.map (fun z -> {data = z; indirect = z}) Zone.reprs
-
- let structural_descr =
- Structural_descr.t_record [| Zone.packed_descr; Zone.packed_descr; |]
- let rehash = Datatype.identity
-
- let mem_project = Datatype.never_any_project
-
- let copy = Datatype.undefined
- end)
-
- include DatatypeFromDeps
-
- let pretty_precise fmt {data; indirect} =
- let bottom_data = Zone.is_bottom data in
- let bottom_indirect = Zone.is_bottom indirect in
- match bottom_indirect, bottom_data with
- | true, true ->
- Format.fprintf fmt "\\nothing"
- | true, false ->
- Format.fprintf fmt "direct: %a"
- Zone.pretty data
- | false, true ->
- Format.fprintf fmt "indirect: %a"
- Zone.pretty indirect
- | false, false ->
- Format.fprintf fmt "indirect: %a; direct: %a"
- Zone.pretty indirect
- Zone.pretty data
-
- let from_data_deps z = { data = z; indirect = Zone.bottom }
- let from_indirect_deps z = { data = Zone.bottom; indirect = z }
-
- let bottom = {
- data = Zone.bottom;
- indirect = Zone.bottom;
- }
-
- let top = {
- data = Zone.top;
- indirect = Zone.top;
- }
-
- let is_included fd1 fd2 =
- Zone.is_included fd1.data fd2.data &&
- Zone.is_included fd1.indirect fd2.indirect
-
- let join fd1 fd2 =
- if fd1 == bottom then fd2
- else if fd2 == bottom then fd1
- else {
- data = Zone.join fd1.data fd2.data;
- indirect = Zone.join fd1.indirect fd2.indirect
- }
-
- let narrow fd1 fd2 = {
- data = Zone.narrow fd1.data fd2.data;
- indirect = Zone.narrow fd1.indirect fd2.indirect
- }
-
- let add_data_dep fd data =
- { fd with data = Zone.join fd.data data }
-
- let add_indirect_dep fd indirect =
- { fd with indirect = Zone.join fd.indirect indirect }
-
- let map f fd = {
- data = f fd.data;
- indirect = f fd.indirect;
- }
-
-end
-
-module DepsOrUnassigned = struct
-
- type deps_or_unassigned =
- | DepsBottom
- | Unassigned
- | AssignedFrom of Deps.t
- | MaybeAssignedFrom of Deps.t
-
- module DatatypeDeps = Datatype.Make(struct
- type t = deps_or_unassigned
-
- let name = "Function_Froms.Deps.deps"
-
- let pretty fmt = function
- | DepsBottom -> Format.pp_print_string fmt "DEPS_BOTTOM"
- | Unassigned -> Format.pp_print_string fmt "UNASSIGNED"
- | AssignedFrom fd -> Deps.pretty_precise fmt fd
- | MaybeAssignedFrom fd ->
- (* '(or UNASSIGNED)' would be a better pretty-printer, we use
- '(and SELF)' only for compatibility reasons *)
- Format.fprintf fmt "%a (and SELF)" Deps.pretty_precise fd
-
- let hash = function
- | DepsBottom -> 3
- | Unassigned -> 17
- | AssignedFrom fd -> 37 + 13 * Deps.hash fd
- | MaybeAssignedFrom fd -> 57 + 123 * Deps.hash fd
-
- let compare d1 d2 = match d1, d2 with
- | DepsBottom, DepsBottom
- | Unassigned, Unassigned -> 0
- | AssignedFrom fd1, AssignedFrom fd2
- | MaybeAssignedFrom fd1, MaybeAssignedFrom fd2 ->
- Deps.compare fd1 fd2
- | DepsBottom, (Unassigned | AssignedFrom _ | MaybeAssignedFrom _)
- | Unassigned, (AssignedFrom _ | MaybeAssignedFrom _)
- | AssignedFrom _, MaybeAssignedFrom _ ->
- -1
- | (Unassigned | AssignedFrom _ | MaybeAssignedFrom _), DepsBottom
- | (AssignedFrom _ | MaybeAssignedFrom _), Unassigned
- | MaybeAssignedFrom _, AssignedFrom _ ->
- 1
-
- let equal = Datatype.from_compare
-
- let reprs = Unassigned :: List.map (fun r -> AssignedFrom r) Deps.reprs
-
- let structural_descr =
- let d = Deps.packed_descr in
- Structural_descr.t_sum [| [| d |]; [| d |] |]
- let rehash = Datatype.identity
-
- let mem_project = Datatype.never_any_project
-
- let copy = Datatype.undefined
-
- end)
-
- let join d1 d2 = match d1, d2 with
- | DepsBottom, d | d, DepsBottom -> d
- | Unassigned, Unassigned -> Unassigned
- | Unassigned, AssignedFrom fd | AssignedFrom fd, Unassigned ->
- MaybeAssignedFrom fd
- | Unassigned, (MaybeAssignedFrom _ as d)
- | (MaybeAssignedFrom _ as d), Unassigned ->
- d
- | AssignedFrom fd1, AssignedFrom fd2 ->
- AssignedFrom (Deps.join fd1 fd2)
- | AssignedFrom fd1, MaybeAssignedFrom fd2
- | MaybeAssignedFrom fd1, AssignedFrom fd2
- | MaybeAssignedFrom fd1, MaybeAssignedFrom fd2 ->
- MaybeAssignedFrom (Deps.join fd1 fd2)
-
- let narrow _ _ = assert false (* not used yet *)
-
- let is_included d1 d2 = match d1, d2 with
- | DepsBottom, (DepsBottom | Unassigned | AssignedFrom _ |
- MaybeAssignedFrom _)
- | Unassigned, (Unassigned | AssignedFrom _ | MaybeAssignedFrom _) ->
- true
- | MaybeAssignedFrom fd1, (AssignedFrom fd2 | MaybeAssignedFrom fd2)
- | AssignedFrom fd1, AssignedFrom fd2 ->
- Deps.is_included fd1 fd2
- | (Unassigned | AssignedFrom _ | MaybeAssignedFrom _), DepsBottom
- | (AssignedFrom _ | MaybeAssignedFrom _), Unassigned
- | AssignedFrom _, MaybeAssignedFrom _ ->
- false
-
- let bottom = DepsBottom
- let top = MaybeAssignedFrom Deps.top
- let default = Unassigned
-
- include DatatypeDeps
-
- let subst f d = match d with
- | DepsBottom -> DepsBottom
- | Unassigned -> Unassigned
- | AssignedFrom fd ->
- let fd' = f fd in
- if fd == fd' then d else AssignedFrom fd'
- | MaybeAssignedFrom fd ->
- let fd' = f fd in
- if fd == fd' then d else MaybeAssignedFrom fd'
-
- let pretty_precise = pretty
-
- let to_zone = function
- | DepsBottom | Unassigned -> Zone.bottom
- | AssignedFrom fd | MaybeAssignedFrom fd -> Deps.to_zone fd
-
- let to_deps = function
- | DepsBottom | Unassigned -> Deps.bottom
- | AssignedFrom fd | MaybeAssignedFrom fd -> fd
-
- let extract_data = function
- | DepsBottom | Unassigned -> Zone.bottom
- | AssignedFrom fd | MaybeAssignedFrom fd -> fd.Deps.data
-
- let extract_indirect = function
- | DepsBottom | Unassigned -> Zone.bottom
- | AssignedFrom fd | MaybeAssignedFrom fd -> fd.Deps.indirect
-
- let may_be_unassigned = function
- | DepsBottom | AssignedFrom _ -> false
- | Unassigned | MaybeAssignedFrom _ -> true
-
- let compose d1 d2 =
- match d1, d2 with
- | DepsBottom, _ | _, DepsBottom ->
- DepsBottom (* could indicate dead code. Not used in practice anyway *)
- | Unassigned, _ -> d2
- | AssignedFrom _, _ -> d1
- | MaybeAssignedFrom _, Unassigned -> d1
- | MaybeAssignedFrom d1, MaybeAssignedFrom d2 ->
- MaybeAssignedFrom (Deps.join d1 d2)
- | MaybeAssignedFrom d1, AssignedFrom d2 ->
- AssignedFrom (Deps.join d1 d2)
-
- (* for backwards compatibility *)
- let pretty fmt fd =
- match fd with
- | DepsBottom -> Format.pp_print_string fmt "DEPS_BOTTOM"
- | Unassigned -> Format.pp_print_string fmt "(SELF)"
- | AssignedFrom d -> Zone.pretty fmt (Deps.to_zone d)
- | MaybeAssignedFrom d ->
- Format.fprintf fmt "%a (and SELF)" Zone.pretty (Deps.to_zone d)
-end
-
-module Memory = struct
- (** A From table is internally represented as a Lmap of [DepsOrUnassigned].
- However, the API mostly hides this fact, and exports access functions
- that take or return [Deps.t] values. This way, the user needs not
- understand the subtleties of DepsBottom/Unassigned/MaybeAssigned. *)
-
- include Lmap_bitwise.Make_bitwise(DepsOrUnassigned)
-
- let () = imprecise_write_msg := "dependencies to update"
-
- let pretty_skip = function
- | DepsOrUnassigned.DepsBottom -> true
- | DepsOrUnassigned.Unassigned -> true
- | DepsOrUnassigned.AssignedFrom _ -> false
- | DepsOrUnassigned.MaybeAssignedFrom _ -> false
-
- let pretty =
- pretty_generic_printer
- ~skip_v:pretty_skip ~pretty_v:DepsOrUnassigned.pretty ~sep:"FROM" ()
-
- let pretty_ind_data =
- pretty_generic_printer
- ~skip_v:pretty_skip ~pretty_v:DepsOrUnassigned.pretty_precise ~sep:"FROM"
- ()
-
-
- (** This is the auxiliary datastructure used to write the function [find].
- When we iterate over a offsetmap of value [DepsOrUnassigned], we obtain
- two things: (1) some dependencies; (2) some intervals that may have not
- been assigned, and that will appear as data dependencies (once we know
- the base we are iterating on). *)
- type find_offsm = {
- fo_itvs: Int_Intervals.t;
- fo_deps: Deps.t;
- }
-
- (** Once the base is known, we can obtain something of type [Deps.t] *)
- let convert_find_offsm base fp =
- let z = Zone.inject base fp.fo_itvs in
- Deps.add_data_dep fp.fo_deps z
-
- let empty_find_offsm = {
- fo_itvs = Int_Intervals.bottom;
- fo_deps = Deps.bottom;
- }
-
- let join_find_offsm fp1 fp2 =
- if fp1 == empty_find_offsm then fp2
- else if fp2 == empty_find_offsm then fp1
- else {
- fo_itvs = Int_Intervals.join fp1.fo_itvs fp2.fo_itvs;
- fo_deps = Deps.join fp1.fo_deps fp2.fo_deps;
- }
-
- (** Auxiliary function that collects the dependencies on some intervals of
- an offsetmap. *)
- let find_precise_offsetmap : Int_Intervals.t -> LOffset.t -> find_offsm =
- let cache = Hptmap_sig.PersistentCache "Function_Froms.find_precise" in
- let aux_find_offsm ib ie v =
- (* If the interval can be unassigned, we collect its bound. We also
- return the dependencies stored at this interval. *)
- let default, v = match v with
- | DepsOrUnassigned.DepsBottom -> false, Deps.bottom
- | DepsOrUnassigned.Unassigned -> true, Deps.bottom
- | DepsOrUnassigned.MaybeAssignedFrom v -> true, v
- | DepsOrUnassigned.AssignedFrom v -> false, v
- in
- { fo_itvs =
- if default
- then Int_Intervals.inject_bounds ib ie
- else Int_Intervals.bottom;
- fo_deps = v }
- in
- (* Partial application is important *)
- LOffset.fold_join_itvs
- ~cache aux_find_offsm join_find_offsm empty_find_offsm
-
- (** Collecting dependencies on a given zone. *)
- let find_precise : t -> Zone.t -> Deps.t =
- let both = find_precise_offsetmap in
- let conv = convert_find_offsm in
- (* We are querying a zone for which no dependency is stored. Hence, every
- base is implicitly bound to [Unassigned]. *)
- let empty_map z = Deps.from_data_deps z in
- let join = Deps.join in
- let empty = Deps.bottom in
- (* Partial application is important *)
- let f = fold_join_zone ~both ~conv ~empty_map ~join ~empty in
- fun m z ->
- match m with
- | Top -> Deps.top
- | Bottom -> Deps.bottom
- | Map m -> try f z m with Abstract_interp.Error_Top -> Deps.top
-
- let find z m =
- Deps.to_zone (find_precise z m)
-
- let add_binding_precise_loc ~exact access m loc v =
- let aux_one_loc loc m =
- let loc = Locations.valid_part access loc in
- add_binding_loc ~exact m loc (DepsOrUnassigned.AssignedFrom v)
- in
- Precise_locs.fold aux_one_loc loc m
-
- let bind_var vi v m =
- let z = Locations.zone_of_varinfo vi in
- add_binding ~exact:true m z (DepsOrUnassigned.AssignedFrom v)
-
- let unbind_var vi m =
- remove_base (Base.of_varinfo vi) m
-
- let add_binding ~exact m z v =
- add_binding ~exact m z (DepsOrUnassigned.AssignedFrom v)
-
- let add_binding_loc ~exact m loc v =
- add_binding_loc ~exact m loc (DepsOrUnassigned.AssignedFrom v)
-
- let is_unassigned m =
- LOffset.is_same_value m DepsOrUnassigned.Unassigned
-
- (* Unassigned is a neutral value for compose, on both sides *)
- let decide_compose m1 m2 =
- if m1 == m2 || is_unassigned m1 then LOffset.ReturnRight
- else if is_unassigned m2 then LOffset.ReturnLeft
- else LOffset.Recurse
-
- let compose_map =
- let cache = Hptmap_sig.PersistentCache "Function_Froms.Memory.compose" in
- (* Partial application is important because of the cache. Idempotent,
- because [compose x x] is always equal to [x]. *)
- map2 ~cache ~symmetric:false ~idempotent:true ~empty_neutral:true
- decide_compose DepsOrUnassigned.compose
-
- let compose m1 m2 = match m1, m2 with
- | Top, _ | _, Top -> Top
- | Map m1, Map m2 -> Map (compose_map m1 m2)
- | Bottom, (Map _ | Bottom) | Map _, Bottom -> Bottom
-
- (** Auxiliary function that substitutes the data right-hand part of a
- dependency by a pre-existing From state. The returned result is a Deps.t:
- the data part will be the data part of the complete result, the indirect
- part will be added to the indirect part of the final result. *)
- (* This function iterates simultaneously on a From memory, and on a zone.
- It is cached. The definitions below are used to call the function that
- does the recursive descent. *)
- let substitute_data_deps =
- (* Nothing left to substitute, return z unchanged *)
- let empty_right z = Deps.from_data_deps z in
- (* Zone to substitute is empty *)
- let empty_left _ = Deps.bottom in
- (* [b] is in the zone and substituted. Rewrite appropriately *)
- let both b itvs offsm =
- let fp = find_precise_offsetmap itvs offsm in
- convert_find_offsm b fp
- in
- let join = Deps.join in
- let empty = Deps.bottom in
- let cache = Hptmap_sig.PersistentCache "From_compute.subst_data" in
- let f_map =
- Zone.fold2_join_heterogeneous
- ~cache ~empty_left ~empty_right ~both ~join ~empty
- in
- fun call_site_froms z ->
- match call_site_froms with
- | Bottom -> Deps.bottom
- | Top -> Deps.top
- | Map m ->
- try f_map z (shape m)
- with Abstract_interp.Error_Top -> Deps.top
-
- (** Auxiliary function that substitutes the indirect right-hand part of a
- dependency by a pre-existing From state. The returned result is a zone,
- which will be added to the indirect part of the final result. *)
- let substitute_indirect_deps =
- (* Nothing left to substitute, z is directly an indirect dependency *)
- let empty_right z = z in
- (* Zone to substitute is empty *)
- let empty_left _ = Zone.bottom in
- let both b itvs offsm =
- (* Both the found data and indirect dependencies are computed for indirect
- dependencies: merge to a single zone *)
- let fp = find_precise_offsetmap itvs offsm in
- Deps.to_zone (convert_find_offsm b fp)
- in
- let join = Zone.join in
- let empty = Zone.bottom in
- let cache = Hptmap_sig.PersistentCache "From_compute.subst_indirect" in
- let f_map =
- Zone.fold2_join_heterogeneous
- ~cache ~empty_left ~empty_right ~both ~join ~empty
- in
- fun call_site_froms z ->
- match call_site_froms with
- | Bottom -> Zone.bottom
- | Top -> Zone.top
- | Map m ->
- try f_map z (shape m)
- with Abstract_interp.Error_Top -> Zone.top
-
- let substitute call_site_froms deps =
- let open Deps in
- let { data; indirect } = deps in
- (* depending directly on an indirect dependency -> indirect,
- depending indirectly on a direct dependency -> indirect *)
- let dirdeps = substitute_data_deps call_site_froms data in
- let inddeps = substitute_indirect_deps call_site_froms indirect in
- let dir = dirdeps.data in
- let ind = Zone.(join dirdeps.indirect inddeps) in
- { data = dir; indirect = ind }
-
-
- type return = Deps.t
-
- let default_return = Deps.bottom
-
- let top_return = Deps.top
-
- let add_to_return ?start:(_start=0) ~size:_size ?(m=default_return) v =
- Deps.join m v
-(*
- let start = Ival.of_int start in
- let itvs = Int_Intervals.from_ival_size start size in
- LOffset.add_iset ~exact:true itvs (DepsOrUnassigned.AssignedFrom v) m
-*)
-
- let top_return_size size =
- add_to_return ~size Deps.top
-
- let join_return = Deps.join
-
- let collapse_return x = x
-
-end
-
-type froms =
- { deps_return : Memory.return;
- deps_table : Memory.t }
-
-let top = {
- deps_return = Memory.top_return;
- deps_table = Memory.top;
-}
-
-let join x y =
- { deps_return = Memory.join_return x.deps_return y.deps_return ;
- deps_table = Memory.join x.deps_table y.deps_table }
-
-let outputs { deps_table = t } =
- match t with
- | Memory.Top -> Locations.Zone.top
- | Memory.Bottom -> Locations.Zone.bottom
- | Memory.Map(m) ->
- Memory.fold
- (fun z v acc ->
- let open DepsOrUnassigned in
- match v with
- | DepsBottom | Unassigned -> acc
- | AssignedFrom _ | MaybeAssignedFrom _ -> Locations.Zone.join z acc)
- m Locations.Zone.bottom
-
-let inputs ?(include_self=false) t =
- let aux b offm acc =
- Memory.LOffset.fold
- (fun itvs deps acc ->
- let z = DepsOrUnassigned.to_zone deps in
- let self = DepsOrUnassigned.may_be_unassigned deps in
- let acc = Zone.join z acc in
- match include_self, self, b with
- | true, true, Some b ->
- Zone.join acc (Zone.inject b itvs)
- | _ -> acc
- )
- offm
- acc
- in
- let return = Deps.to_zone t.deps_return in
- let aux_table b = aux (Some b) in
- match t.deps_table with
- | Memory.Top -> Zone.top
- | Memory.Bottom -> Zone.bottom
- | Memory.Map m -> Memory.fold_base aux_table m return
-
-
-let pretty fmt { deps_return = r ; deps_table = t } =
- Format.fprintf fmt "%a@\n\\result FROM @[%a@]@\n"
- Memory.pretty t
- Deps.pretty r
-
-(** same as pretty, but uses the type of the function to output more
- precise information.
- @raise Error if the given type is not a function type
-*)
-let pretty_with_type ~indirect typ fmt { deps_return = r; deps_table = t } =
- let (rt_typ,_,_,_) = Cil.splitFunctionType typ in
- if Memory.is_bottom t
- then Format.fprintf fmt
- "@[NON TERMINATING - NO EFFECTS@]"
- else
- let map_pretty =
- if indirect
- then Memory.pretty_ind_data
- else Memory.pretty
- in
- if Cil.isVoidType rt_typ
- then begin
- if Memory.is_empty t
- then Format.fprintf fmt "@[NO EFFECTS@]"
- else map_pretty fmt t
- end
- else
- let pp_space fmt =
- if not (Memory.is_empty t) then
- Format.fprintf fmt "@ "
- in
- Format.fprintf fmt "@[<v>%a%t@[\\result FROM @[%a@]@]@]"
- map_pretty t pp_space
- (if indirect then Deps.pretty_precise else Deps.pretty) r
-
-let pretty_with_type_indirect = pretty_with_type ~indirect:true
-let pretty_with_type = pretty_with_type ~indirect:false
-
-let hash { deps_return = dr ; deps_table = dt } =
- Memory.hash dt + 197 * Deps.hash dr
-
-let equal
- { deps_return = dr ; deps_table = dt }
- { deps_return = dr' ; deps_table = dt' } =
- Memory.equal dt dt'&& Deps.equal dr dr'
-
-include Datatype.Make
- (struct
- type t = froms
- let reprs =
- List.fold_left
- (fun acc o ->
- List.fold_left
- (fun acc m -> { deps_return = o; deps_table = m } :: acc)
- acc
- Memory.reprs)
- []
- Deps.reprs
- let structural_descr =
- Structural_descr.t_record
- [| Deps.packed_descr;
- Memory.packed_descr |]
- let name = "Function_Froms"
- let hash = hash
- let compare = Datatype.undefined
- let equal = equal
- let pretty = pretty
- let rehash = Datatype.identity
- let copy = Datatype.undefined
- let mem_project = Datatype.never_any_project
- end)
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/abstract_interp/function_Froms.mli b/src/kernel_services/abstract_interp/function_Froms.mli
deleted file mode 100644
index 141bfc5f9a5266c16d87476242410a5f7f679f83..0000000000000000000000000000000000000000
--- a/src/kernel_services/abstract_interp/function_Froms.mli
+++ /dev/null
@@ -1,186 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(** Datastructures and common operations for the results of the From plugin. *)
-
-module Deps : sig
-
- type deps = {
- data: Locations.Zone.t;
- indirect: Locations.Zone.t;
- }
-
- val bottom: deps
- val top: deps
- val is_included: deps -> deps -> bool
- val join: deps -> deps -> deps
- val narrow: deps -> deps -> deps
- val to_zone: deps -> Locations.Zone.t
-
- val add_data_dep: deps -> Locations.Zone.t -> deps
- val add_indirect_dep: deps -> Locations.Zone.t -> deps
-
-
- val from_data_deps: Locations.Zone.t -> deps
- val from_indirect_deps: Locations.Zone.t -> deps
-
- val map: (Locations.Zone.t -> Locations.Zone.t) -> deps -> deps
-
- include Datatype.S with type t = deps
-
- val pretty_precise : Format.formatter -> t -> unit
-end
-
-
-module DepsOrUnassigned : sig
-
- type deps_or_unassigned =
- | DepsBottom (** Bottom of the lattice, never bound inside a memory state
- at a valid location. (May appear for bases for which the
- validity does not start at 0, currently only NULL.) *)
- | Unassigned (** Location has never been assigned *)
- | AssignedFrom of Deps.t (** Location guaranteed to have been overwritten,
- its contents depend on the [Deps.t] value *)
- | MaybeAssignedFrom of Deps.t (** Location may or may not have been
- overwritten *)
- (** The lattice is [DepsBottom <= Unassigned], [DepsBottom <= AssignedFrom z],
- [Unassigned <= MaybeAssignedFrom] and
- [AssignedFrom z <= MaybeAssignedFrom z]. *)
-
- include Lmap_bitwise.With_default with type t = deps_or_unassigned
-
- val subst: (Deps.t -> Deps.t) -> t -> t
-
- val extract_data: t -> Locations.Zone.t
- val extract_indirect: t -> Locations.Zone.t
-
- val may_be_unassigned: t -> bool
-
- val compose: t -> t -> t
- (** [compose d1 d2] is the sequential composition of [d1] after [d2], ie.
- the dependencies needed to execute [d1] after having executed [d2].
- It is computed as [d1] if [d1 = AssignedFrom _] (as executing [d1]
- completely overwrites what [d2] wrote), and as a partial join between
- [d1] and [d2] in the other cases. *)
-
- val pretty_precise : Format.formatter -> t -> unit
-
- val to_zone: t -> Locations.Zone.t
- val to_deps: t -> Deps.deps
-end
-
-module Memory : sig
- include Lmap_bitwise.Location_map_bitwise with type v = DepsOrUnassigned.t
-
- (** Prints the detail of address and data dependencies, as opposed to [pretty]
- that prints the backwards-compatible union of them *)
- val pretty_ind_data : Format.formatter -> t -> unit
-
- val find: t -> Locations.Zone.t -> Locations.Zone.t
- (** Imprecise version of find, in which data and indirect dependencies are
- not distinguished *)
-
- val find_precise: t -> Locations.Zone.t -> Deps.t
- (** Precise version of find *)
-
- val add_binding: exact:bool -> t -> Locations.Zone.t -> Deps.t -> t
- val add_binding_loc: exact:bool -> t -> Locations.location -> Deps.t -> t
- val add_binding_precise_loc:
- exact:bool -> Locations.access -> t ->
- Precise_locs.precise_location -> Deps.t -> t
- val bind_var: Cil_types.varinfo -> Deps.t -> t -> t
- val unbind_var: Cil_types.varinfo -> t -> t
-
- val map: (DepsOrUnassigned.t -> DepsOrUnassigned.t) -> t -> t
-
- val compose: t -> t -> t
- (** Sequential composition. See {!DepsOrUnassigned.compose}. *)
-
- val substitute: t -> Deps.t -> Deps.t
- (** [substitute m d] applies [m] to [d] so that any dependency in [d] is
- expressed using the dependencies already present in [m]. For example,
- [substitute 'x From y' 'x'] returns ['y']. *)
-
-
- (** Dependencies for [\result]. *)
-
- type return = Deps.t
- (* Currently, this type is equal to [Deps.t]. However, some of the functions
- below are more precise, and will be more useful when 'return' are
- represented by a precise offsetmap. *)
-
- (** Default value to use for storing the dependencies of [\result] *)
- val default_return: return
-
- (** Completely imprecise return *)
- val top_return: return
-
- (** Completely imprecise return of the given size *)
- val top_return_size: Int_Base.t -> return
-
- (** Add some dependencies to [\result], between bits [start] and
- [start+size-1], to the [Deps.t] value; default value for [start] is 0.
- If [m] is specified, the dependencies are added to it. Otherwise,
- {!default_return} is used. *)
- val add_to_return:
- ?start:int -> size:Int_Base.t -> ?m:return -> Deps.t -> return
-
- val collapse_return: return -> Deps.t
-end
-
-
-
-type froms = {
- deps_return : Memory.return
-(** Dependencies for the returned value *);
- deps_table : Memory.t
-(** Dependencies on all the zones modified by the function *);
-}
-
-include Datatype.S with type t = froms
-
-val join: froms -> froms -> froms
-
-val top: froms
-
-(** Display dependencies of a function, using the function's type to improve
- readability *)
-val pretty_with_type: Cil_types.typ -> froms Pretty_utils.formatter
-
-(** Display dependencies of a function, using the function's type to improve
- readability, separating direct and indirect dependencies *)
-val pretty_with_type_indirect: Cil_types.typ -> froms Pretty_utils.formatter
-
-(** Extract the left part of a from result, ie. the zones that are written *)
-val outputs: froms -> Locations.Zone.t
-
-(** Extract the right part of a from result, ie. the zones on which the
- written zones depend. If [include_self] is true, and the from is
- of the form [x FROM y (and SELF)], [x] is added to the result;
- default value is [false]. *)
-val inputs: ?include_self:bool -> froms -> Locations.Zone.t
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 7ee21c551d305b60cadca7ec6460b7d37f67b24b..1a8fe1b2101e763421ef6889a479e982fe6eb818 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -178,6 +178,48 @@ module Callstack: sig
end
+module Deps: sig
+
+ (** Memory dependencies of an expression. *)
+ type t = {
+ data: Locations.Zone.t;
+ (** Memory zone directly required to evaluate the given expression. *)
+ indirect: Locations.Zone.t;
+ (** Memory zone read to compute data addresses. *)
+ }
+
+ include Datatype.S with type t := t
+
+ val pretty_precise: Format.formatter -> t -> unit
+ val pretty_debug: Format.formatter -> t -> unit
+
+ (* Constructors *)
+
+ val top : t
+ val bottom : t
+ val data : Locations.Zone.t -> t
+ val indirect : Locations.Zone.t -> t
+
+ (* Conversion *)
+
+ val to_zone : t -> Locations.Zone.t
+
+ (* Mutators *)
+
+ val add_data : t -> Locations.Zone.t -> t
+ val add_indirect : t -> Locations.Zone.t -> t
+
+ (* Map *)
+
+ val map : (Locations.Zone.t -> Locations.Zone.t) -> t -> t
+
+ (* Lattice operators *)
+
+ val is_included : t -> t -> bool
+ val join : t -> t -> t
+ val narrow : t -> t -> t
+end
+
module Results: sig
(** Eva's result API is a new interface to access the results of an analysis,
@@ -335,14 +377,6 @@ module Results: sig
evaluate the given lvalue, excluding the lvalue zone itself. *)
val address_deps : Cil_types.lval -> request -> Locations.Zone.t
- (** Memory dependencies of an expression. *)
- type deps = Function_Froms.Deps.deps = {
- data: Locations.Zone.t;
- (** Memory zone directly required to evaluate the given expression. *)
- indirect: Locations.Zone.t;
- (** Memory zone read to compute data addresses. *)
- }
-
(** Taint of a memory zone, according to the taint domain. *)
type taint =
| Direct
@@ -361,7 +395,7 @@ module Results: sig
(** Computes (an overapproximation of) the memory dependencies of an
expression. *)
- val expr_dependencies : Cil_types.exp -> request -> deps
+ val expr_dependencies : Cil_types.exp -> request -> Deps.t
(** Evaluation *)
@@ -600,6 +634,63 @@ module Eval: sig
callers, can be cached. *)
end
+module Assigns: sig
+
+ module DepsOrUnassigned : sig
+
+ type t =
+ | DepsBottom (** Bottom of the lattice, never bound inside a memory state
+ at a valid location. (May appear for bases for which the
+ validity does not start at 0, currently only NULL.) *)
+ | Unassigned (** Location has never been assigned *)
+ | AssignedFrom of Deps.t (** Location guaranteed to have been overwritten,
+ its contents depend on the [Deps.t] value *)
+ | MaybeAssignedFrom of Deps.t (** Location may or may not have been
+ overwritten *)
+
+ (** The lattice is [DepsBottom <= Unassigned], [DepsBottom <= AssignedFrom z],
+ [Unassigned <= MaybeAssignedFrom] and
+ [AssignedFrom z <= MaybeAssignedFrom z]. *)
+
+ val top : t
+ val equal : t -> t -> bool
+ val may_be_unassigned : t -> bool
+ val to_zone : t -> Locations.Zone.t
+ end
+
+ module Memory : sig
+ include Lmap_bitwise.Location_map_bitwise with type v = DepsOrUnassigned.t
+
+ val find : t -> Locations.Zone.t -> Locations.Zone.t
+ (** Imprecise version of find, in which data and indirect dependencies are
+ not distinguished *)
+
+ val find_precise : t -> Locations.Zone.t -> Deps.t
+ (** Precise version of find *)
+
+ val find_precise_loffset : LOffset.t -> Base.t -> Int_Intervals.t -> Deps.t
+
+ val add_binding : exact:bool -> t -> Locations.Zone.t -> Deps.t -> t
+ val add_binding_loc : exact:bool -> t -> Locations.location -> Deps.t -> t
+ val add_binding_precise_loc :
+ exact:bool -> Locations.access -> t ->
+ Precise_locs.precise_location -> Deps.t -> t
+ end
+
+ type t = {
+ return : Deps.t
+ (** Dependencies for the returned value *);
+ memory : Memory.t
+ (** Dependencies on all the zones modified by the function *);
+ }
+
+ include Datatype.S with type t := t
+
+ val top : t
+ val join : t -> t -> t
+
+end
+
module Builtins: sig
(** Eva analysis builtins for the cvalue domain, more efficient than their
@@ -624,9 +715,11 @@ module Builtins: sig
c_clobbered: Base.SetLattice.t;
(** An over-approximation of the bases in which addresses of local variables
might have been written *)
- c_from: (Function_Froms.froms * Locations.Zone.t) option;
- (** If not None, the froms of the function, and its sure outputs;
- i.e. the dependencies of the result and of each zone written to. *)
+ c_assigns: (Assigns.t * Locations.Zone.t) option;
+ (** If not None:
+ - the assigns of the function, i.e. the dependencies of the result
+ and of each zone written to.
+ - and its sure outputs, i.e. an under-approximation of written zones. *)
}
(** The result of a builtin can be given in different forms. *)
@@ -672,10 +765,11 @@ module Cvalue_callbacks: sig
type state = Cvalue.Model.t
- (** If not None, the froms of the function, and its sure outputs;
- i.e. the dependencies of the result, and the dependencies
- of each zone written to. *)
- type call_froms = (Function_Froms.froms * Locations.Zone.t) option
+ (** If not None:
+ - the assigns of the function, i.e. the dependencies of the result
+ and the dependencies of each zone written to;
+ - and its sure outputs, i.e. an under-approximation of written zones. *)
+ type call_assigns = (Assigns.t * Locations.Zone.t) option
type analysis_kind =
[ `Builtin (** A cvalue builtin is used to interpret the function. *)
@@ -700,7 +794,7 @@ module Cvalue_callbacks: sig
(** Results of a function call. *)
type call_results =
- [ `Builtin of state list * call_froms
+ [ `Builtin of state list * call_assigns
(** List of cvalue states at the end of the builtin. *)
| `Spec of state list
(** List of cvalue states at the end of the call. *)
@@ -767,10 +861,10 @@ module Logic_inout: sig
Cvalue.Model.t -> Locations.access -> Cil_types.term -> tlval_zones option
(** Evaluate the assigns clauses of the given function in its given pre-state,
- and compare them with the given froms (computed by the from plugin).
+ and compare them with the dependencies computed by the from plugin.
Emits warnings if needed, and sets statuses to the assigns clauses. *)
val verify_assigns:
- Cil_types.kernel_function -> pre:Cvalue.Model.t -> Function_Froms.froms -> unit
+ Cil_types.kernel_function -> pre:Cvalue.Model.t -> Assigns.t -> unit
(** [accept_base ~formals ~locals kf b] returns [true] if and only if [b] is:
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index 3015cbcf1564ee2332cac2973c08abf0289588dd..3666a0c4345da0dbe0554481a50459fd1dd98453 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -327,7 +327,7 @@ module EvaTaints = struct
let evaluate expr request =
let (let+) = Option.bind in
- let { data ; indirect } = expr_dependencies expr request in
+ let Deps.{ data ; indirect } = expr_dependencies expr request in
let+ data = is_tainted data request |> Result.to_option in
let+ indirect = is_tainted indirect request |> Result.to_option in
Some (data, indirect)
diff --git a/src/plugins/eva/domains/cvalue/builtins.ml b/src/plugins/eva/domains/cvalue/builtins.ml
index b128b35eed8387cf041c595f1438392a8f0bc3e9..493a62a052b953e553871f1d6d1dbdf50ca7bd05 100644
--- a/src/plugins/eva/domains/cvalue/builtins.ml
+++ b/src/plugins/eva/domains/cvalue/builtins.ml
@@ -31,7 +31,7 @@ type cacheable = Eval.cacheable = Cacheable | NoCache | NoCacheCallers
type full_result = {
c_values: (Cvalue.V.t option * Cvalue.Model.t) list;
c_clobbered: Base.SetLattice.t;
- c_from: (Function_Froms.froms * Locations.Zone.t) option;
+ c_assigns: (Assigns.t * Locations.Zone.t) option;
}
type call_result =
@@ -276,7 +276,7 @@ let apply_builtin (builtin:builtin) call ~pre ~post =
let states = process_result call post call_result in
let froms =
match call_result with
- | Full result -> result.c_from
+ | Full result -> result.c_assigns
| States _ | Result _ -> None
in
let result = `Builtin (List.map fst states, froms) in
diff --git a/src/plugins/eva/domains/cvalue/builtins.mli b/src/plugins/eva/domains/cvalue/builtins.mli
index 1d25c32aff6cc28b5391b25368b0c3a52dce20dc..bf85aba9659e2bd3cac76f04b6af8814f283dac0 100644
--- a/src/plugins/eva/domains/cvalue/builtins.mli
+++ b/src/plugins/eva/domains/cvalue/builtins.mli
@@ -44,9 +44,11 @@ type full_result = {
c_clobbered: Base.SetLattice.t;
(** An over-approximation of the bases in which addresses of local variables
might have been written *)
- c_from: (Function_Froms.froms * Locations.Zone.t) option;
- (** If not None, the froms of the function, and its sure outputs;
- i.e. the dependencies of the result and of each zone written to. *)
+ c_assigns: (Assigns.t * Locations.Zone.t) option;
+ (** If not None:
+ - the assigns of the function, i.e. the dependencies of the result
+ and of each zone written to.
+ - and its sure outputs, i.e. an under-approximation of written zones. *)
}
(** The result of a builtin can be given in different forms. *)
diff --git a/src/plugins/eva/domains/cvalue/builtins_malloc.ml b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
index 77b26cbe8cc5bcb6e6cd6812c283f612ecb56eed..14364066d2fa108a24be87f005c2e0a6bce40756 100644
--- a/src/plugins/eva/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
@@ -489,7 +489,7 @@ let register_malloc ?replace name ?returns_null prefix region =
let ret = V.inject new_base Ival.zero in
let c_values = wrap_fallible_alloc ?returns_null ret state new_state in
let c_clobbered = Base.SetLattice.bottom in
- Builtins.Full { c_values; c_clobbered; c_from = None; }
+ Builtins.Full { c_values; c_clobbered; c_assigns = None; }
in
let name = "Frama_C_" ^ name in
let typ () = Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf] in
@@ -541,7 +541,7 @@ let calloc_builtin state args =
wrap_fallible_alloc ?returns_null ret state new_state
in
let c_clobbered = Base.SetLattice.bottom in
- Builtins.Full { c_values; c_clobbered; c_from = None; }
+ Builtins.Full { c_values; c_clobbered; c_assigns = None; }
let () =
let name = "Frama_C_calloc" in
@@ -579,9 +579,8 @@ let free ~exact bases state =
Locals_scoping.make_escaping ~exact ~escaping ~on_escaping ~within state
in
let from_changed =
- let open Function_Froms in
- let m = Memory.(add_binding ~exact empty !changed Deps.bottom) in
- { deps_table = m; deps_return = Deps.bottom }
+ let m = Assigns.Memory.(add_binding ~exact empty !changed Deps.bottom) in
+ Assigns.{ memory = m; return = Deps.bottom }
in
state, (from_changed, if exact then !changed else Zone.bottom)
@@ -646,12 +645,12 @@ let frama_c_free state actuals =
let bases_to_remove, card_to_remove, _null = resolve_bases_to_free arg in
let c_clobbered = Base.SetLattice.bottom in
if card_to_remove = 0 then
- Builtins.Full { c_values = []; c_clobbered; c_from = None; }
+ Builtins.Full { c_values = []; c_clobbered; c_assigns = None; }
else
let strong = card_to_remove <= 1 in
let state, changed = free_aux state ~strong bases_to_remove in
let c_values = [None, state] in
- Builtins.Full { c_values; c_clobbered; c_from = Some changed; }
+ Builtins.Full { c_values; c_clobbered; c_assigns = Some changed; }
| _ -> raise (Builtins.Invalid_nb_of_args 1)
let () =
@@ -667,7 +666,7 @@ let frama_c_vla_free state actuals =
let state, changed = free_aux state ~strong:true bases_to_remove in
let c_values = [None, state] in
let c_clobbered = Base.SetLattice.bottom in
- Builtins.Full { c_values; c_clobbered; c_from = Some changed; }
+ Builtins.Full { c_values; c_clobbered; c_assigns = Some changed; }
| _ -> raise (Builtins.Invalid_nb_of_args 1)
let () =
@@ -824,10 +823,10 @@ let realloc_builtin_aux state ptr size =
let new_state, changed = free_aux new_state ~strong bases in
let c_values = wrap_fallible_alloc ret state new_state in
let c_clobbered = Builtins.clobbered_set_from_ret new_state ret in
- Builtins.Full { c_values; c_clobbered; c_from = Some changed; }
+ Builtins.Full { c_values; c_clobbered; c_assigns = Some changed; }
else (* Invalid call. *)
let c_clobbered = Base.SetLattice.bottom in
- Builtins.Full { c_values = []; c_clobbered; c_from = None; }
+ Builtins.Full { c_values = []; c_clobbered; c_assigns = None; }
let realloc_builtin state args =
let ptr, size =
@@ -915,7 +914,7 @@ let check_leaked_malloced_bases state _ =
Base.pretty base)
alloced_bases;
let c_clobbered = Base.SetLattice.bottom in
- Builtins.Full { c_values = [None,state]; c_clobbered; c_from = None; }
+ Builtins.Full { c_values = [None,state]; c_clobbered; c_assigns = None; }
let () =
Builtins.register_builtin "Frama_C_check_leak" NoCacheCallers
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index 073fc79acf09987e1fd82a7623e58bd1257f3e97..f466617f59030c0b0438385e1b94fa5fb7784450 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -74,7 +74,7 @@ let frama_c_offset _state = function
let () = register_builtin "Frama_C_offset" frama_c_offset
-exception Memcpy_result of (Cvalue.Model.t * Function_Froms.froms * Zone.t)
+exception Memcpy_result of (Cvalue.Model.t * Assigns.t * Zone.t)
exception Indeterminate of V_Or_Uninitialized.t
@@ -97,11 +97,10 @@ let memcpy_check_indeterminate_offsetmap offsm =
(* Create a dependency [\from arg_n] where n is the nth argument of the
currently called function. *)
let deps_nth_arg n =
- let open Function_Froms in
let kf = Callstack.top_kf (Eva_utils.current_call_stack ()) in
try
let vi = List.nth (Kernel_function.get_formals kf) n in
- Deps.add_data_dep Deps.bottom (Locations.zone_of_varinfo vi)
+ Deps.add_data Deps.bottom (Locations.zone_of_varinfo vi)
with Failure _ -> Kernel.fatal "%d arguments expected" n
@@ -126,7 +125,7 @@ let frama_c_memcpy name state actuals =
in
let deps_return = deps_nth_arg 0 in
let empty_cfrom =
- Function_Froms.({ deps_table = Memory.empty; deps_return })
+ Assigns.{ memory = Memory.empty; return = deps_return }
in
let precise_copy state =
(* First step: copy the bytes we are sure to copy *)
@@ -148,26 +147,25 @@ let frama_c_memcpy name state actuals =
let (deps_table, sure_zone) =
let zone_dst = enumerate_valid_bits Locations.Write loc_dst in
let zone_src = enumerate_valid_bits Locations.Read loc_src in
- let deps =
- Function_Froms.(Deps.add_data_dep Deps.bottom zone_src)
- in
+ let deps = Deps.data zone_src in
(* Note: actually a part may be written for sure (if the
difference between the offsets in loc_dst is smaller
than size), but keeping it imprecise reflects more the
imprecision of the value analysis here. *)
let exact = Location_Bits.cardinal_zero_or_one dst_bits in
let deps_table =
- Function_Froms.Memory.add_binding ~exact
- Function_Froms.Memory.empty zone_dst deps in
+ Assigns.Memory.add_binding ~exact
+ Assigns.Memory.empty zone_dst deps
+ in
let sure_zone = if exact then zone_dst else Zone.bottom in
(deps_table, sure_zone)
in
new_state, deps_table, sure_zone
end
else (* Nothing certain can be copied *)
- (state, Function_Froms.Memory.empty, Zone.bottom)
+ (state, Assigns.Memory.empty, Zone.bottom)
in
- let imprecise_copy new_state precise_deps_table sure_zone =
+ let imprecise_copy new_state precise_assigns sure_zone =
(* Second step. Size is imprecise, we will now copy some bits
that we are not sure to copy *)
let size_min_ival = Ival.inject_singleton size_min in
@@ -192,14 +190,13 @@ let frama_c_memcpy name state actuals =
let loc_src = make_loc (Location_Bits.shift range src) size_char in
let loc_dst = make_loc (Location_Bits.shift range dst) size_char in
let c_from =
- let open Function_Froms in
let zone_src = enumerate_valid_bits Locations.Read loc_src in
let zone_dst = enumerate_valid_bits Locations.Write loc_dst in
- let deps = Deps.add_data_dep Deps.bottom zone_src in
- let deps_table =
- Memory.add_binding ~exact:false precise_deps_table zone_dst deps
+ let deps = Deps.data zone_src in
+ let memory =
+ Assigns.Memory.add_binding ~exact:false precise_assigns zone_dst deps
in
- { deps_table; deps_return }
+ Assigns.{ memory; return = deps_return }
in
try
(* We try to iter on all the slices inside the value of slice.
@@ -274,26 +271,29 @@ let frama_c_memcpy name state actuals =
try
if Ival.is_zero size then
raise (Memcpy_result (state, empty_cfrom, Zone.bottom));
- let (precise_state,precise_deps_table,sure_zone) = precise_copy state in
+ let (precise_state,precise_assigns,sure_zone) = precise_copy state in
if Option.fold ~none:false ~some:(Int.equal min) max then
- (let open Function_Froms in
- let c_from = { deps_table = precise_deps_table; deps_return } in
- raise (Memcpy_result (precise_state, c_from, sure_zone)));
- imprecise_copy precise_state precise_deps_table sure_zone
+ begin
+ let c_assigns =
+ Assigns.{ memory = precise_assigns; return = deps_return }
+ in
+ raise (Memcpy_result (precise_state, c_assigns, sure_zone))
+ end;
+ imprecise_copy precise_state precise_assigns sure_zone
with
- | Memcpy_result (new_state,c_from,sure_zone) ->
+ | Memcpy_result (new_state,c_assigns,sure_zone) ->
if Model.is_reachable new_state then
(* Copy at least partially succeeded (with perhaps an
alarm for some of the sizes *)
Builtins.Full
{ Builtins.c_values = [Some dst_bytes, new_state];
c_clobbered = Builtins.clobbered_set_from_ret new_state dst_bytes;
- c_from = Some (c_from, sure_zone); }
+ c_assigns = Some (c_assigns, sure_zone); }
else
Builtins.Full
{ Builtins.c_values = [ None, Cvalue.Model.bottom];
c_clobbered = Base.SetLattice.bottom;
- c_from = Some (c_from, sure_zone); }
+ c_assigns = Some (c_assigns, sure_zone); }
in
match actuals with
| [dst; src; size] -> compute dst src size
@@ -362,22 +362,22 @@ let frama_c_memset_imprecise state dst_lval dst v size =
(new_state,Zone.bottom)
with Not_found -> (new_state,Zone.bottom) (* from find_lonely_key + explicit raise *)
in
- let c_from =
- let open Function_Froms in
+ let c_assigns =
let value_dep = deps_nth_arg 1 in
- let deps_table =
- Memory.add_binding ~exact:false Memory.empty over_zone value_dep
+ let memory = Assigns.Memory.empty in
+ let memory =
+ Assigns.Memory.add_binding ~exact:false memory over_zone value_dep
in
- let deps_table =
- Memory.add_binding ~exact:true deps_table sure_zone value_dep
+ let memory =
+ Assigns.Memory.add_binding ~exact:true memory sure_zone value_dep
in
let deps_return = deps_nth_arg 0 in
- { deps_table; deps_return }
+ Assigns.{ memory; return = deps_return }
in
Builtins.Full
{ Builtins.c_values = [Some dst, new_state'];
c_clobbered = Base.SetLattice.bottom;
- c_from = Some (c_from,sure_zone); }
+ c_assigns = Some (c_assigns,sure_zone); }
(* let () = register_builtin "Frama_C_memset" frama_c_memset_imprecise *)
(* Type that describes why the 'precise memset' builtin may fail. *)
@@ -575,15 +575,15 @@ let frama_c_memset_precise state dst_lval dst v (exp_size, size) =
let dst_loc = Locations.loc_bytes_to_loc_bits dst in
let (c_from,dst_zone) =
let input = deps_nth_arg 1 in
- let open Function_Froms in
let size_bits = Integer.mul size (Bit_utils.sizeofchar ())in
let dst_location = Locations.make_loc dst_loc (Int_Base.Value size_bits) in
let dst_zone = Locations.(enumerate_valid_bits Write dst_location) in
- let deps_table =
- Function_Froms.Memory.add_binding ~exact:true
- Function_Froms.Memory.empty dst_zone input in
- let deps_return = deps_nth_arg 0 in
- let c_from = { deps_table; deps_return } in
+ let memory =
+ Assigns.Memory.add_binding ~exact:true
+ Assigns.Memory.empty dst_zone input
+ in
+ let return = deps_nth_arg 0 in
+ let c_from = Assigns.{ memory; return } in
c_from,dst_zone
in
let _ = c_from in
@@ -596,7 +596,7 @@ let frama_c_memset_precise state dst_lval dst v (exp_size, size) =
Builtins.Full
{ Builtins.c_values = [Some dst, state'];
c_clobbered = Base.SetLattice.bottom;
- c_from = Some (c_from,dst_zone); }
+ c_assigns = Some (c_from,dst_zone); }
with
| Bit_utils.NoMatchingOffset -> raise (ImpreciseMemset SizeMismatch)
| Base.Not_a_C_variable -> raise (ImpreciseMemset NoTypeForDest)
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index 6ba460b8da9fe1f45b14226d6403a4f8fad23116..2cbaa286e1443f43629111580cac105071bd3683 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -56,7 +56,7 @@ let typ_kind typ =
| TFloat _ -> Float
| _ -> assert false
-type dependencies = Eva_utils.deps = {
+type dependencies = Deps.t = {
data: Locations.Zone.t;
indirect: Locations.Zone.t;
}
@@ -836,12 +836,6 @@ end
module VariableToDeps =
struct
- module Deps =
- struct
- include Function_Froms.Deps
- let pretty_debug = pretty_precise
- end
-
let cache_prefix = "Eva.Octagons.VariableToDeps"
include Hptmap.Make (Variable) (Deps) (Hptmap.Comp_unused)
@@ -1040,7 +1034,7 @@ module Deps = struct
BaseToVariables.add_deps var deps i
in
match VariableToDeps.find_opt var m with
- | Some previous_deps when Function_Froms.Deps.equal previous_deps deps ->
+ | Some previous_deps when Deps.equal previous_deps deps ->
m, i
| Some previous_deps when not (are_bases_increasing previous_deps deps) ->
(* If [var] already exists in the state and had bigger dependencies (a
@@ -1053,7 +1047,7 @@ module Deps = struct
contain variables that do not appear in [m]. *)
let add var deps (m, i: t): t =
match VariableToDeps.find_opt var m with
- | Some d when Function_Froms.Deps.equal d deps -> m, i
+ | Some d when Deps.equal d deps -> m, i
| _ ->
VariableToDeps.add var deps m,
BaseToVariables.add_deps var deps i
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index 66e75d5fb6c5738a5fac9570a71e8c8c1743dce1..ee102c636e8dba81c0523c333d5ca81ca3984577 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -112,8 +112,9 @@
(mode (promote (only Eva.mli)))
(deps
gen-api.sh Eva.header
- engine/analysis.mli types/callstack.mli utils/results.mli parameters.mli
- utils/eva_annotations.mli eval.mli domains/cvalue/builtins.mli
- utils/cvalue_callbacks.mli legacy/logic_inout.mli utils/eva_results.mli
+ engine/analysis.mli types/callstack.mli types/deps.mli utils/results.mli parameters.mli
+ utils/eva_annotations.mli eval.mli types/assigns.mli
+ domains/cvalue/builtins.mli utils/cvalue_callbacks.mli legacy/logic_inout.mli
+ utils/eva_results.mli
utils/unit_tests.mli)
(action (run bash %{deps})))
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 88b6280b2e75a83b72bf2a90b23921754ba17269..90a70b081ad5d1f6cfe4b9528a9c50647ef4c3f7 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -35,7 +35,7 @@ let clear_caches () =
Cvalue.Model.clear_caches ();
Locations.Location_Bytes.clear_caches ();
Locations.Zone.clear_caches ();
- Function_Froms.Memory.clear_caches ()
+ Assigns.Memory.clear_caches ()
let () = State.add_hook_on_update Self.state clear_caches
diff --git a/src/plugins/eva/gui/gui_eval.ml b/src/plugins/eva/gui/gui_eval.ml
index 3205c66f1626cdcf9cfbafd72be6a11af0af5b2c..1aec39065f79ef1fcdf4165fe164b86098694e2d 100644
--- a/src/plugins/eva/gui/gui_eval.ml
+++ b/src/plugins/eva/gui/gui_eval.ml
@@ -86,7 +86,7 @@ let clear_caches () =
Cvalue.Model.clear_caches ();
Locations.Location_Bytes.clear_caches ();
Locations.Zone.clear_caches ();
- Function_Froms.Memory.clear_caches ()
+ Assigns.Memory.clear_caches ()
module type S = sig
module Analysis : Analysis.S
diff --git a/src/plugins/eva/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index 03c6ee235bad35404a29e23fe25237a7c671e1b3..7f6db6d4f75c48e434e26205b43ee000b084f9e7 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -147,14 +147,13 @@ let eval_assigns_from pre_state it =
(** Compute the validity status for [from] in [pre_state], assuming the
entire clause is [assigns asgn \from from]. The inferred dependencies
are [found_froms], while [asgn] evaluates to [assigns_zone]. *)
-let check_from pre_state asgn assigns_zone from found_froms =
+let check_from pre_state asgn assigns_zone from found_assigns =
let open Locations in
let found_deps =
- let open Function_Froms in
if Logic_utils.is_result asgn.it_content then
- found_froms.deps_return
+ found_assigns.Assigns.return
else
- Memory.find_precise found_froms.deps_table assigns_zone
+ Assigns.Memory.find_precise found_assigns.memory assigns_zone
in
let (indirect_deps,direct_deps) =
let filter x = List.mem "indirect" x.it_content.term_name in
@@ -165,8 +164,8 @@ let check_from pre_state asgn assigns_zone from found_froms =
let eval = eval_assigns_from pre_state in
let stated_indirect_deps = link (List.map eval indirect_deps) in
let stated_direct_deps = link (List.map eval direct_deps) in
- let found_direct_deps = found_deps.Function_Froms.Deps.data in
- let found_indirect_deps = found_deps.Function_Froms.Deps.indirect in
+ let found_direct_deps = found_deps.Deps.data in
+ let found_indirect_deps = found_deps.Deps.indirect in
let res_for_unknown txt =
Self.debug "found_direct deps %a stated_direct_deps %a \
found_indirect_deps %a stated_indirect_deps %a"
@@ -214,7 +213,7 @@ let check_fct_assigns kf ab ~pre_state found_froms =
let behaviors = Annotations.behaviors kf in
(* Under-approximation of the union. *)
let link zones = List.fold_left Zone.link Zone.bottom zones in
- let outputs = Function_Froms.outputs found_froms in
+ let outputs = Assigns.outputs found_froms in
let check_for_behavior b =
let activity = Active_behaviors.is_active ab b in
match activity with
diff --git a/src/plugins/eva/legacy/logic_inout.mli b/src/plugins/eva/legacy/logic_inout.mli
index ddec2c39239451d647383b453d55c3800a534a7c..f5f7aaf82950babc4a850f8e10ab2d7b3d177748 100644
--- a/src/plugins/eva/legacy/logic_inout.mli
+++ b/src/plugins/eva/legacy/logic_inout.mli
@@ -63,10 +63,10 @@ val assigns_tlval_to_zones:
Cvalue.Model.t -> Locations.access -> Cil_types.term -> tlval_zones option
(** Evaluate the assigns clauses of the given function in its given pre-state,
- and compare them with the given froms (computed by the from plugin).
+ and compare them with the dependencies computed by the from plugin.
Emits warnings if needed, and sets statuses to the assigns clauses. *)
val verify_assigns:
- Cil_types.kernel_function -> pre:Cvalue.Model.t -> Function_Froms.froms -> unit
+ Cil_types.kernel_function -> pre:Cvalue.Model.t -> Assigns.t -> unit
(** [accept_base ~formals ~locals kf b] returns [true] if and only if [b] is:
diff --git a/src/plugins/eva/types/assigns.ml b/src/plugins/eva/types/assigns.ml
new file mode 100644
index 0000000000000000000000000000000000000000..cc34f73bdee90be68d279d7b10c517fd0554ab81
--- /dev/null
+++ b/src/plugins/eva/types/assigns.ml
@@ -0,0 +1,241 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module DepsOrUnassigned = struct
+ module Datatype_Input = struct
+ include Datatype.Serializable_undefined
+
+ type t =
+ | DepsBottom
+ | Unassigned
+ | AssignedFrom of Deps.t
+ | MaybeAssignedFrom of Deps.t
+ [@@deriving eq,ord]
+
+ let name = "Eva.Froms.DepsOrUnassigned"
+
+ let pretty fmt = function
+ | DepsBottom -> Format.pp_print_string fmt "DEPS_BOTTOM"
+ | Unassigned -> Format.pp_print_string fmt "UNASSIGNED"
+ | AssignedFrom fd -> Deps.pretty_precise fmt fd
+ | MaybeAssignedFrom fd ->
+ Format.fprintf fmt "%a (or UNASSIGNED)" Deps.pretty_precise fd
+
+ let hash = function
+ | DepsBottom -> 1
+ | Unassigned -> 2
+ | AssignedFrom fd -> Hashtbl.hash (3, Deps.hash fd)
+ | MaybeAssignedFrom fd -> Hashtbl.hash (4, Deps.hash fd)
+
+ let reprs = Unassigned :: List.map (fun r -> AssignedFrom r) Deps.reprs
+ end
+
+ include Datatype.Make (Datatype_Input)
+ include Datatype_Input
+
+ let join d1 d2 = match d1, d2 with
+ | DepsBottom, d | d, DepsBottom -> d
+ | Unassigned, Unassigned -> Unassigned
+ | Unassigned, AssignedFrom fd | AssignedFrom fd, Unassigned ->
+ MaybeAssignedFrom fd
+ | Unassigned, (MaybeAssignedFrom _ as d)
+ | (MaybeAssignedFrom _ as d), Unassigned ->
+ d
+ | AssignedFrom fd1, AssignedFrom fd2 ->
+ AssignedFrom (Deps.join fd1 fd2)
+ | AssignedFrom fd1, MaybeAssignedFrom fd2
+ | MaybeAssignedFrom fd1, AssignedFrom fd2
+ | MaybeAssignedFrom fd1, MaybeAssignedFrom fd2 ->
+ MaybeAssignedFrom (Deps.join fd1 fd2)
+
+ let narrow _ _ = assert false (* not used yet *)
+
+ let is_included d1 d2 = match d1, d2 with
+ | DepsBottom, (DepsBottom | Unassigned | AssignedFrom _ |
+ MaybeAssignedFrom _)
+ | Unassigned, (Unassigned | AssignedFrom _ | MaybeAssignedFrom _) ->
+ true
+ | MaybeAssignedFrom fd1, (AssignedFrom fd2 | MaybeAssignedFrom fd2)
+ | AssignedFrom fd1, AssignedFrom fd2 ->
+ Deps.is_included fd1 fd2
+ | (Unassigned | AssignedFrom _ | MaybeAssignedFrom _), DepsBottom
+ | (AssignedFrom _ | MaybeAssignedFrom _), Unassigned
+ | AssignedFrom _, MaybeAssignedFrom _ ->
+ false
+
+ let bottom = DepsBottom
+ let top = MaybeAssignedFrom Deps.top
+ let default = Unassigned
+
+ let to_zone = function
+ | DepsBottom | Unassigned -> Locations.Zone.bottom
+ | AssignedFrom fd | MaybeAssignedFrom fd -> Deps.to_zone fd
+
+ let may_be_unassigned = function
+ | DepsBottom | AssignedFrom _ -> false
+ | Unassigned | MaybeAssignedFrom _ -> true
+end
+
+module Memory = struct
+ (* A From table is internally represented as a Lmap of [DepsOrUnassigned].
+ However, the API mostly hides this fact, and exports access functions
+ that take or return [Deps.t] values. This way, the user needs not
+ understand the subtleties of DepsBottom/Unassigned/MaybeAssigned. *)
+
+ include Lmap_bitwise.Make_bitwise(DepsOrUnassigned)
+
+ let add_binding_precise_loc ~exact access m loc v =
+ let aux_one_loc loc m =
+ let loc = Locations.valid_part access loc in
+ add_binding_loc ~exact m loc (DepsOrUnassigned.AssignedFrom v)
+ in
+ Precise_locs.fold aux_one_loc loc m
+
+ let add_binding ~exact m z v =
+ add_binding ~exact m z (DepsOrUnassigned.AssignedFrom v)
+
+ let add_binding_loc ~exact m loc v =
+ add_binding_loc ~exact m loc (DepsOrUnassigned.AssignedFrom v)
+
+ (* This is the auxiliary datastructure used to write the function [find].
+ When we iterate over a offsetmap of value [DepsOrUnassigned], we obtain
+ two things: (1) some dependencies; (2) some intervals that may have not
+ been assigned, and that will appear as data dependencies (once we know
+ the base we are iterating on). *)
+ type find_offsm = {
+ fo_itvs: Int_Intervals.t;
+ fo_deps: Deps.t;
+ }
+
+ (* Once the base is known, we can obtain something of type [Deps.t] *)
+ let convert_find_offsm base fp =
+ let z = Locations.Zone.inject base fp.fo_itvs in
+ Deps.add_data fp.fo_deps z
+
+ let empty_find_offsm = {
+ fo_itvs = Int_Intervals.bottom;
+ fo_deps = Deps.bottom;
+ }
+
+ let join_find_offsm fp1 fp2 =
+ if fp1 == empty_find_offsm then fp2
+ else if fp2 == empty_find_offsm then fp1
+ else {
+ fo_itvs = Int_Intervals.join fp1.fo_itvs fp2.fo_itvs;
+ fo_deps = Deps.join fp1.fo_deps fp2.fo_deps;
+ }
+
+ (* Auxiliary function that collects the dependencies on some intervals of
+ an offsetmap. *)
+ let find_precise_offsetmap : Int_Intervals.t -> LOffset.t -> find_offsm =
+ let cache = Hptmap_sig.PersistentCache "Eva.Froms.Memory.find_precise" in
+ let aux_find_offsm ib ie v =
+ (* If the interval can be unassigned, we collect its bound. We also
+ return the dependencies stored at this interval. *)
+ let default, v = match v with
+ | DepsOrUnassigned.DepsBottom -> false, Deps.bottom
+ | DepsOrUnassigned.Unassigned -> true, Deps.bottom
+ | DepsOrUnassigned.MaybeAssignedFrom v -> true, v
+ | DepsOrUnassigned.AssignedFrom v -> false, v
+ in
+ { fo_itvs =
+ if default
+ then Int_Intervals.inject_bounds ib ie
+ else Int_Intervals.bottom;
+ fo_deps = v }
+ in
+ (* Partial application is important *)
+ LOffset.fold_join_itvs
+ ~cache aux_find_offsm join_find_offsm empty_find_offsm
+
+ (* Collecting dependencies on a given zone. *)
+ let find_precise : t -> Locations.Zone.t -> Deps.t =
+ let both = find_precise_offsetmap in
+ let conv = convert_find_offsm in
+ (* We are querying a zone for which no dependency is stored. Hence, every
+ base is implicitly bound to [Unassigned]. *)
+ let empty_map z = Deps.data z in
+ let join = Deps.join in
+ let empty = Deps.bottom in
+ (* Partial application is important *)
+ let f = fold_join_zone ~both ~conv ~empty_map ~join ~empty in
+ fun m z ->
+ match m with
+ | Top -> Deps.top
+ | Bottom -> Deps.bottom
+ | Map m -> try f z m with Abstract_interp.Error_Top -> Deps.top
+
+ let find_precise_loffset loffset base itv =
+ let fo = find_precise_offsetmap itv loffset in
+ convert_find_offsm base fo
+
+ let find z m = Deps.to_zone (find_precise z m)
+end
+
+module Datatype_Input = struct
+ include Datatype.Serializable_undefined
+
+ type t = {
+ return : Deps.t;
+ memory : Memory.t
+ }
+ [@@deriving eq,ord]
+
+ let name = "Eva.Froms"
+
+ let top = {
+ return = Deps.top;
+ memory = Memory.top;
+ }
+
+ let reprs = [ top ]
+
+ let hash assigns =
+ Hashtbl.hash (Memory.hash assigns.memory, Deps.hash assigns.return)
+
+ let pretty fmt assigns =
+ Format.fprintf fmt "%a@\n\\result FROM @[%a@]@\n"
+ Memory.pretty assigns.memory
+ Deps.pretty assigns.return
+end
+
+include Datatype.Make (Datatype_Input)
+include Datatype_Input
+
+let join x y =
+ {
+ return = Deps.join x.return y.return;
+ memory = Memory.join x.memory y.memory;
+ }
+
+let outputs assigns =
+ match assigns.memory with
+ | Memory.Top -> Locations.Zone.top
+ | Memory.Bottom -> Locations.Zone.bottom
+ | Memory.Map m ->
+ Memory.fold
+ (fun z v acc ->
+ let open DepsOrUnassigned in
+ match v with
+ | DepsBottom | Unassigned -> acc
+ | AssignedFrom _ | MaybeAssignedFrom _ -> Locations.Zone.join z acc)
+ m Locations.Zone.bottom
diff --git a/src/plugins/eva/types/assigns.mli b/src/plugins/eva/types/assigns.mli
new file mode 100644
index 0000000000000000000000000000000000000000..2875fbf0dc3a54e01e7feab400950478fa4f82bb
--- /dev/null
+++ b/src/plugins/eva/types/assigns.mli
@@ -0,0 +1,83 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Datastructures and common operations for the results of the From plugin. *)
+
+[@@@ api_start]
+
+module DepsOrUnassigned : sig
+
+ type t =
+ | DepsBottom (** Bottom of the lattice, never bound inside a memory state
+ at a valid location. (May appear for bases for which the
+ validity does not start at 0, currently only NULL.) *)
+ | Unassigned (** Location has never been assigned *)
+ | AssignedFrom of Deps.t (** Location guaranteed to have been overwritten,
+ its contents depend on the [Deps.t] value *)
+ | MaybeAssignedFrom of Deps.t (** Location may or may not have been
+ overwritten *)
+
+ (** The lattice is [DepsBottom <= Unassigned], [DepsBottom <= AssignedFrom z],
+ [Unassigned <= MaybeAssignedFrom] and
+ [AssignedFrom z <= MaybeAssignedFrom z]. *)
+
+ val top : t
+ val equal : t -> t -> bool
+ val may_be_unassigned : t -> bool
+ val to_zone : t -> Locations.Zone.t
+end
+
+module Memory : sig
+ include Lmap_bitwise.Location_map_bitwise with type v = DepsOrUnassigned.t
+
+ val find : t -> Locations.Zone.t -> Locations.Zone.t
+ (** Imprecise version of find, in which data and indirect dependencies are
+ not distinguished *)
+
+ val find_precise : t -> Locations.Zone.t -> Deps.t
+ (** Precise version of find *)
+
+ val find_precise_loffset : LOffset.t -> Base.t -> Int_Intervals.t -> Deps.t
+
+ val add_binding : exact:bool -> t -> Locations.Zone.t -> Deps.t -> t
+ val add_binding_loc : exact:bool -> t -> Locations.location -> Deps.t -> t
+ val add_binding_precise_loc :
+ exact:bool -> Locations.access -> t ->
+ Precise_locs.precise_location -> Deps.t -> t
+end
+
+type t = {
+ return : Deps.t
+(** Dependencies for the returned value *);
+ memory : Memory.t
+(** Dependencies on all the zones modified by the function *);
+}
+
+include Datatype.S with type t := t
+
+val top : t
+val join : t -> t -> t
+
+[@@@ api_end]
+
+(** Extract the left part of a from result, ie. the zones that are written *)
+val outputs : t -> Locations.Zone.t
diff --git a/src/plugins/eva/types/deps.ml b/src/plugins/eva/types/deps.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2f6bad3f7a3fd2b6929de54743354bf3c206498f
--- /dev/null
+++ b/src/plugins/eva/types/deps.ml
@@ -0,0 +1,132 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module Zone = Locations.Zone
+
+type deps = {
+ data: Zone.t;
+ indirect: Zone.t;
+}
+
+(* Pretty printing of detailed internal representation *)
+let pretty_precise fmt {data; indirect} =
+ let bottom_data = Zone.is_bottom data in
+ let bottom_indirect = Zone.is_bottom indirect in
+ match bottom_indirect, bottom_data with
+ | true, true ->
+ Format.fprintf fmt "\\nothing"
+ | true, false ->
+ Format.fprintf fmt "direct: %a"
+ Zone.pretty data
+ | false, true ->
+ Format.fprintf fmt "indirect: %a"
+ Zone.pretty indirect
+ | false, false ->
+ Format.fprintf fmt "indirect: %a; direct: %a"
+ Zone.pretty indirect
+ Zone.pretty data
+
+let pretty_debug = pretty_precise
+
+(* Conversion to zone, used by default pretty printing *)
+let to_zone d = Locations.Zone.join d.data d.indirect
+
+
+(* Datatype *)
+
+module Prototype = struct
+ include Datatype.Serializable_undefined
+
+ type t = deps = {
+ data: Zone.t;
+ indirect: Zone.t;
+ }
+ [@@deriving eq,ord]
+
+ let name = "Deps"
+ let pretty fmt d = Zone.pretty fmt (to_zone d)
+ let hash fd = Hashtbl.hash (Zone.hash fd.data, Zone.hash fd.indirect)
+ let reprs = List.map (fun z -> {data = z; indirect = z}) Zone.reprs
+end
+
+include Datatype.Make (Prototype)
+include Prototype
+
+
+(* Constructors *)
+
+let bottom = {
+ data = Locations.Zone.bottom;
+ indirect = Locations.Zone.bottom;
+}
+
+let top = {
+ data = Zone.top;
+ indirect = Zone.top;
+}
+
+let data z = {
+ data = z;
+ indirect = Zone.bottom;
+}
+
+let indirect z = {
+ data = Zone.bottom;
+ indirect = z;
+}
+
+
+(* Mutators *)
+
+let add_data d data =
+ { d with data = Zone.join d.data data }
+
+let add_indirect d indirect =
+ { d with indirect = Zone.join d.indirect indirect }
+
+
+(* Map *)
+
+let map f d = {
+ data = f d.data;
+ indirect = f d.indirect;
+}
+
+
+(* Lattice *)
+
+let is_included fd1 fd2 =
+ Zone.is_included fd1.data fd2.data &&
+ Zone.is_included fd1.indirect fd2.indirect
+
+let join d1 d2 =
+ if d1 == bottom then d2
+ else if d2 == bottom then d1
+ else {
+ data = Zone.join d1.data d2.data;
+ indirect = Zone.join d1.indirect d2.indirect;
+ }
+
+let narrow d1 d2 = {
+ data = Zone.narrow d1.data d2.data;
+ indirect = Zone.narrow d1.indirect d2.indirect;
+}
diff --git a/src/plugins/eva/types/deps.mli b/src/plugins/eva/types/deps.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a30399e8e540450f5be762e719d3ffd86db01176
--- /dev/null
+++ b/src/plugins/eva/types/deps.mli
@@ -0,0 +1,63 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+[@@@ api_start]
+
+(** Memory dependencies of an expression. *)
+type t = {
+ data: Locations.Zone.t;
+ (** Memory zone directly required to evaluate the given expression. *)
+ indirect: Locations.Zone.t;
+ (** Memory zone read to compute data addresses. *)
+}
+
+include Datatype.S with type t := t
+
+val pretty_precise: Format.formatter -> t -> unit
+val pretty_debug: Format.formatter -> t -> unit
+
+(* Constructors *)
+
+val top : t
+val bottom : t
+val data : Locations.Zone.t -> t
+val indirect : Locations.Zone.t -> t
+
+(* Conversion *)
+
+val to_zone : t -> Locations.Zone.t
+
+(* Mutators *)
+
+val add_data : t -> Locations.Zone.t -> t
+val add_indirect : t -> Locations.Zone.t -> t
+
+(* Map *)
+
+val map : (Locations.Zone.t -> Locations.Zone.t) -> t -> t
+
+(* Lattice operators *)
+
+val is_included : t -> t -> bool
+val join : t -> t -> t
+val narrow : t -> t -> t
+[@@@ api_end]
diff --git a/src/plugins/eva/utils/cvalue_callbacks.ml b/src/plugins/eva/utils/cvalue_callbacks.ml
index d4101a12b9c2de6f3a289deef62458ba3a3ef6c6..99461fbbeb8ba04c86f57163a4a90380d8f25a1b 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.ml
+++ b/src/plugins/eva/utils/cvalue_callbacks.ml
@@ -41,13 +41,13 @@ let register_call_hook f =
let apply_call_hooks callstack kf state kind =
Call.apply (callstack, kf, state, kind)
-type call_froms = (Function_Froms.froms * Locations.Zone.t) option
+type call_assigns = (Assigns.t * Locations.Zone.t) option
type state_by_stmt = (state Cil_datatype.Stmt.Hashtbl.t) Lazy.t
type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
type call_results =
- [ `Builtin of state list * call_froms
+ [ `Builtin of state list * call_assigns
| `Spec of state list
| `Body of results * int
| `Reuse of int
diff --git a/src/plugins/eva/utils/cvalue_callbacks.mli b/src/plugins/eva/utils/cvalue_callbacks.mli
index baa6dc0942ac19de3ec39a0ce11584b893626fe8..203dddeced30b3c8eb3a0604026075e42ca8837d 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.mli
+++ b/src/plugins/eva/utils/cvalue_callbacks.mli
@@ -30,10 +30,11 @@
type state = Cvalue.Model.t
-(** If not None, the froms of the function, and its sure outputs;
- i.e. the dependencies of the result, and the dependencies
- of each zone written to. *)
-type call_froms = (Function_Froms.froms * Locations.Zone.t) option
+(** If not None:
+ - the assigns of the function, i.e. the dependencies of the result
+ and the dependencies of each zone written to;
+ - and its sure outputs, i.e. an under-approximation of written zones. *)
+type call_assigns = (Assigns.t * Locations.Zone.t) option
type analysis_kind =
[ `Builtin (** A cvalue builtin is used to interpret the function. *)
@@ -58,7 +59,7 @@ type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
(** Results of a function call. *)
type call_results =
- [ `Builtin of state list * call_froms
+ [ `Builtin of state list * call_assigns
(** List of cvalue states at the end of the builtin. *)
| `Spec of state list
(** List of cvalue states at the end of the call. *)
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index e1a9d043fec882e18870b54ba124cdf87ce62943..8741fe7ea42754bfae1230ba6ab801d53dbb2c57 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -285,20 +285,6 @@ let lval_to_exp =
MemoLvalToExp.memo
(fun lv -> Cil.new_exp ~loc:Cil_datatype.Location.unknown (Lval lv))
-type deps = Function_Froms.Deps.deps = {
- data: Locations.Zone.t;
- indirect: Locations.Zone.t;
-}
-
-let bottom_deps =
- { data = Locations.Zone.bottom; indirect = Locations.Zone.bottom }
-
-let join_deps a b =
- { data = Locations.Zone.join a.data b.data;
- indirect = Locations.Zone.join a.indirect b.indirect; }
-
-let deps_to_zone deps = Locations.Zone.join deps.data deps.indirect
-
(* Computation of the inputs of an expression. *)
let rec deps_of_expr find_loc expr =
let rec process expr = match expr.enode with
@@ -310,7 +296,7 @@ let rec deps_of_expr find_loc expr =
process e
| BinOp (_, e1, e2, _) ->
(* Binary operators. *)
- join_deps (process e1) (process e2)
+ Deps.join (process e1) (process e2)
| StartOf lv | AddrOf lv ->
(* computation of an address: the inputs of the lvalue whose address
is computed are read to compute said address. *)
@@ -318,11 +304,11 @@ let rec deps_of_expr find_loc expr =
indirect = Locations.Zone.bottom; }
| Const _ | SizeOf _ | AlignOf _ | SizeOfStr _ | SizeOfE _ | AlignOfE _ ->
(* static constructs, nothing is read to evaluate them. *)
- bottom_deps
+ Deps.bottom
in
process expr
-and zone_of_expr find_loc expr = deps_to_zone (deps_of_expr find_loc expr)
+and zone_of_expr find_loc expr = Deps.to_zone (deps_of_expr find_loc expr)
(* dereference of an lvalue: first, its address must be computed,
then its contents themselves are read *)
diff --git a/src/plugins/eva/utils/eva_utils.mli b/src/plugins/eva/utils/eva_utils.mli
index b7c7a84512a3e487546f175d94229b679fcb82b7..2e6380b1ba6aebca694803c7112c684743c46389 100644
--- a/src/plugins/eva/utils/eva_utils.mli
+++ b/src/plugins/eva/utils/eva_utils.mli
@@ -126,18 +126,12 @@ val indirect_zone_of_lval:
on which the offset and the pointer expression (if any) of an lvalue depend.
*)
-
-type deps = Function_Froms.Deps.deps = {
- data: Locations.Zone.t;
- indirect: Locations.Zone.t;
-}
-
val deps_of_expr:
- (lval -> Precise_locs.precise_location) -> exp -> deps
+ (lval -> Precise_locs.precise_location) -> exp -> Deps.t
(** Given a function computing the location of lvalues, computes the memory
dependencies of an expression. *)
-val deps_of_lval: (lval -> Precise_locs.precise_location) -> lval -> deps
+val deps_of_lval: (lval -> Precise_locs.precise_location) -> lval -> Deps.t
(** Given a function computing the location of lvalues, computes the memory
dependencies of an lvalue. *)
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index e4a368655a9c996dcafcb0369e4ba346cfa6549b..2a103740752b240773be661b721e6142729470cc 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -28,6 +28,7 @@ module Abstractions = Abstractions
module Active_behaviors = Active_behaviors
module Alarmset = Alarmset
module Analysis = Analysis
+module Assigns = Assigns
module Callstack = Callstack
module Cvalue_domain = Cvalue_domain
module Cvalue_results = Cvalue_results
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
index f70377152869169e4763bef80aca6d553384f555..eb7491b3c9617d5c9f9e8029b9d5106d13bf2f5c 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -32,6 +32,7 @@ module Abstractions = Abstractions
module Active_behaviors = Active_behaviors
module Alarmset = Alarmset
module Analysis = Analysis
+module Assigns = Assigns
module Callstack = Callstack
module Cvalue_domain = Cvalue_domain
module Cvalue_results = Cvalue_results
diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml
index 297a2b22d2edf20faaac55e7e7c4e5a6443e824d..0df27562e45c83d92c131f8e32b81caa27d8889e 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -733,11 +733,6 @@ let address_deps lval request =
let lval_to_loc lv = eval_address lv request |> as_precise_loc in
Eva_utils.indirect_zone_of_lval lval_to_loc lval
-type deps = Function_Froms.Deps.deps = {
- data: Locations.Zone.t;
- indirect: Locations.Zone.t;
-}
-
let expr_dependencies expr request =
let lval_to_loc lv = eval_address lv request |> as_precise_loc in
Eva_utils.deps_of_expr lval_to_loc expr
diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli
index b091f95830f1e2c6846970a94b84bbafc81e4072..c68373ebcb4157a8312dfefb59b6f0467863d320 100644
--- a/src/plugins/eva/utils/results.mli
+++ b/src/plugins/eva/utils/results.mli
@@ -177,14 +177,6 @@ val lval_deps : Cil_types.lval -> request -> Locations.Zone.t
evaluate the given lvalue, excluding the lvalue zone itself. *)
val address_deps : Cil_types.lval -> request -> Locations.Zone.t
-(** Memory dependencies of an expression. *)
-type deps = Function_Froms.Deps.deps = {
- data: Locations.Zone.t;
- (** Memory zone directly required to evaluate the given expression. *)
- indirect: Locations.Zone.t;
- (** Memory zone read to compute data addresses. *)
-}
-
(** Taint of a memory zone, according to the taint domain. *)
type taint =
| Direct
@@ -203,7 +195,7 @@ val is_tainted : Locations.Zone.t -> request -> (taint, error) Result.t
(** Computes (an overapproximation of) the memory dependencies of an
expression. *)
-val expr_dependencies : Cil_types.exp -> request -> deps
+val expr_dependencies : Cil_types.exp -> request -> Deps.t
(** Evaluation *)
diff --git a/src/plugins/from/From.ml b/src/plugins/from/From.ml
index 03c99df40462fd32d23c0c3d9794b283fc074559..a2bbb575037a34ebd51051c1406eee5d305a44b5 100644
--- a/src/plugins/from/From.ml
+++ b/src/plugins/from/From.ml
@@ -27,7 +27,7 @@ let is_computed = Functionwise.is_computed
let get = Functionwise.get
let pretty = Functionwise.pretty
-let access zone mem = Function_Froms.Memory.find mem zone
+let access zone mem = Eva.Assigns.Memory.find mem zone
let display fmt = From_register.display (Some fmt)
diff --git a/src/plugins/from/From.mli b/src/plugins/from/From.mli
index ac8e62ad0c26771c22e8f1ccf023d03be617a62f..ac0db406d4db28374a7cea5b28c4486c54885a05 100644
--- a/src/plugins/from/From.mli
+++ b/src/plugins/from/From.mli
@@ -28,8 +28,8 @@ val is_computed : kernel_function -> bool
val compute : kernel_function -> unit
val compute_all : unit -> unit
-val get : Cil_types.kernel_function -> Function_Froms.froms
-val access : Locations.Zone.t -> Function_Froms.Memory.t -> Locations.Zone.t
+val get : Cil_types.kernel_function -> Eva.Assigns.t
+val access : Locations.Zone.t -> Eva.Assigns.Memory.t -> Locations.Zone.t
val self : State.t
@@ -42,6 +42,6 @@ val display : Format.formatter -> unit
val compute_all_calldeps : unit -> unit
module Callwise : sig
- val iter : (Cil_types.kinstr -> Function_Froms.froms -> unit) -> unit
- val find : Cil_types.kinstr -> Function_Froms.froms
+ val iter : (Cil_types.kinstr -> Eva.Assigns.t -> unit) -> unit
+ val find : Cil_types.kinstr -> Eva.Assigns.t
end
diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml
index 0e5d37b4d35d0d8aaf6bd1613548ee7cd526d7d2..1d70d24bb671bb6e53819735614723cf564333ac 100644
--- a/src/plugins/from/callwise.ml
+++ b/src/plugins/from/callwise.ml
@@ -25,7 +25,7 @@ open Cil_datatype
module Tbl =
Cil_state_builder.Kinstr_hashtbl
- (Function_Froms)
+ (Eva.Assigns)
(struct
let name = "Callwise dependencies"
let size = 17
@@ -36,7 +36,7 @@ let () = From_parameters.ForceCallDeps.set_output_dependencies [Tbl.self]
let merge_call_froms table callsite froms =
try
let current = Kinstr.Hashtbl.find table callsite in
- let new_froms = Function_Froms.join froms current in
+ let new_froms = Eva.Assigns.join froms current in
Kinstr.Hashtbl.replace table callsite new_froms
with Not_found ->
Kinstr.Hashtbl.add table callsite froms
@@ -44,7 +44,7 @@ let merge_call_froms table callsite froms =
(** State for the analysis of one function call *)
type from_state = {
current_function: Kernel_function.t (** Function being analyzed *);
- table_for_calls: Function_Froms.t Kinstr.Hashtbl.t
+ table_for_calls: Eva.Assigns.t Kinstr.Hashtbl.t
(** State of the From plugin for each statement containing a function call
in the body of [current_function]. Updated incrementally each time
Value analyses such a statement *);
@@ -59,7 +59,7 @@ let call_froms_stack : from_state list ref = ref []
let record_callwise_dependencies_in_db call_site froms =
try
let previous = Tbl.find call_site in
- Tbl.replace call_site (Function_Froms.join previous froms)
+ Tbl.replace call_site (Eva.Assigns.join previous froms)
with Not_found -> Tbl.add call_site froms
let call_for_individual_froms _callstack current_function _state call_type =
@@ -97,7 +97,7 @@ let end_record callstack froms =
module MemExec =
State_builder.Hashtbl
(Datatype.Int.Hashtbl)
- (Function_Froms)
+ (Eva.Assigns)
(struct
let size = 17
let dependencies = [Tbl.self]
@@ -135,7 +135,7 @@ let record_for_individual_froms callstack kf pre_state value_res =
let froms =
if Eva.Analysis.save_results kf
then compute_call_from_value_states kf (Lazy.force before_stmts)
- else Function_Froms.top
+ else Eva.Assigns.top
in
if From_parameters.VerifyAssigns.get () then
Eva.Logic_inout.verify_assigns kf ~pre:pre_state froms;
diff --git a/src/plugins/from/callwise.mli b/src/plugins/from/callwise.mli
index 6fa25e4f741c7f6803d63cdfd1795f81423afdee..ad682a4d569ca6c75efea339479e358348a738aa 100644
--- a/src/plugins/from/callwise.mli
+++ b/src/plugins/from/callwise.mli
@@ -25,5 +25,5 @@
precise than the functionwise results. *)
val compute_all_calldeps : unit -> unit
-val iter : (Cil_types.kinstr -> Function_Froms.froms -> unit) -> unit
-val find : Cil_types.kinstr -> Function_Froms.froms
+val iter : (Cil_types.kinstr -> Eva.Assigns.t -> unit) -> unit
+val find : Cil_types.kinstr -> Eva.Assigns.t
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 4c662872580ba2732f0583f403dda70ffe646c7a..9a063c21cea44ee5b54938be5b28d21a1fcf8f1b 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -33,16 +33,16 @@ module Record_From_Callbacks =
(struct
type t =
(Kernel_function.t Stack.t) *
- Function_Froms.Memory.t Stmt.Hashtbl.t *
- (Kernel_function.t * Function_Froms.Memory.t) list Stmt.Hashtbl.t
+ Eva.Assigns.Memory.t Stmt.Hashtbl.t *
+ (Kernel_function.t * Eva.Assigns.Memory.t) list Stmt.Hashtbl.t
end)
module type To_Use =
sig
- val get_from_call : kernel_function -> stmt -> Function_Froms.t
+ val get_from_call : kernel_function -> stmt -> Eva.Assigns.t
val stmt_request : stmt -> Eva.Results.request
val keep_base : kernel_function -> Base.t -> bool
- val cleanup_and_save : kernel_function -> Function_Froms.t -> Function_Froms.t
+ val cleanup_and_save : kernel_function -> Eva.Assigns.t -> Eva.Assigns.t
end
let compute_using_prototype_for_state state kf assigns =
@@ -53,7 +53,7 @@ let compute_using_prototype_for_state state kf assigns =
From_parameters.warning "@[no assigns clauses@ for function %a.@]@ \
Results will be imprecise."
Kernel_function.pretty kf;
- Function_Froms.Memory.(top_return, top)
+ From_memory.(top_return, top)
| Writes assigns ->
let (rt_typ,_,_,_) = splitFunctionTypeVI varinfo in
let input_zone out ins =
@@ -75,9 +75,9 @@ let compute_using_prototype_for_state state kf assigns =
(* assign clauses do not let us specify address
dependencies for now, so we assume it is all data
dependencies *)
- let input_deps = Function_Froms.Deps.from_data_deps input_zone in
+ let input_deps = Eva.Deps.data input_zone in
(* Weak update of the over-approximation of the zones assigned *)
- let acc = Function_Froms.Memory.add_binding ~exact:false
+ let acc = Eva.Assigns.Memory.add_binding ~exact:false
acc output.over input_deps in
(* Now, perform a strong update on the zones that are guaranteed
to be assigned (under-approximation) AND that do not depend
@@ -90,7 +90,7 @@ let compute_using_prototype_for_state state kf assigns =
Zone.(if equal top input_zone then bottom
else diff output.under input_zone)
in
- let acc = Function_Froms.Memory.add_binding ~exact:true
+ let acc = Eva.Assigns.Memory.add_binding ~exact:true
acc sure_out_zone input_deps in
acc
@@ -99,15 +99,15 @@ let compute_using_prototype_for_state state kf assigns =
let zone_from = input_zone out from in
(* assign clauses do not let us specify address dependencies for
now, so we assume it is all data dependencies *)
- let inputs_deps = Function_Froms.Deps.from_data_deps zone_from in
+ let inputs_deps = Eva.Deps.data zone_from in
try
let coffs = Logic_to_c.loc_to_offset out.it_content in
List.fold_left
(fun acc coff ->
let (base,width) = bitsOffset rt_typ coff in
let size = Int_Base.inject (Int.of_int width) in
- Function_Froms.Memory.(add_to_return
- ~start:base ~size ~m:acc inputs_deps)
+ From_memory.add_to_return
+ ~start:base ~size ~m:acc inputs_deps
)
acc coffs
with Logic_to_c.No_conversion | SizeOfError _ ->
@@ -115,7 +115,7 @@ let compute_using_prototype_for_state state kf assigns =
"Unable to extract a proper offset. \
Using FROM for the whole \\result";
let size = Bit_utils.sizeof rt_typ in
- Function_Froms.(Memory.add_to_return ~size ~m:acc inputs_deps)
+ From_memory.add_to_return ~size ~m:acc inputs_deps
in
let return_assigns, other_assigns =
List.fold_left
@@ -127,19 +127,19 @@ let compute_using_prototype_for_state state kf assigns =
let return_assigns =
match return_assigns with
| [] when Cil.isVoidType rt_typ ->
- Function_Froms.Memory.default_return
+ From_memory.default_return
| [] -> (* \from unspecified. *)
let size = Bit_utils.sizeof rt_typ in
- Function_Froms.Memory.top_return_size size
+ From_memory.top_return_size size
| _ ->
List.fold_left treat_ret_assign
- Function_Froms.Memory.default_return return_assigns
+ From_memory.default_return return_assigns
in
return_assigns,
List.fold_left
- treat_assign Function_Froms.Memory.empty other_assigns
+ treat_assign Eva.Assigns.Memory.empty other_assigns
in
- { deps_return = return_deps; Function_Froms.deps_table = deps }
+ Eva.Assigns.{ return = return_deps; memory = deps }
module ZoneStmtMap = struct
include
@@ -164,7 +164,7 @@ struct
the statement that gave rise to the dependency. *)
additional_deps : Zone.t;
(** Union of the sets in {!additional_deps_table} *)
- deps_table : Function_Froms.Memory.t
+ deps_table : Eva.Assigns.Memory.t
(** dependency table *)
}
@@ -181,7 +181,7 @@ struct
depending directly on an indirect dependency -> indirect,
depending indirectly on a direct dependency -> indirect *)
let merge_deps f deps =
- let open Function_Froms.Deps in
+ let open Eva.Deps in
let ind = f deps.indirect in
let data = f deps.data in
let ind = Zone.join data.indirect (to_zone ind) in
@@ -202,7 +202,7 @@ struct
let aux_local acc vi =
Cil.CurrentLoc.set vi.vdecl;
(* Consider that local are initialized to a constant value *)
- Function_Froms.Memory.bind_var vi Function_Froms.Deps.bottom acc
+ From_memory.bind_var vi Eva.Deps.bottom acc
in
let loc = Cil.CurrentLoc.get () in
@@ -212,7 +212,7 @@ struct
let unbind_locals m b =
let aux_local acc vi =
- Function_Froms.Memory.unbind_var vi acc
+ From_memory.unbind_var vi acc
in
List.fold_left aux_local m b.blocals
@@ -221,7 +221,7 @@ struct
let request = To_Use.stmt_request stmt in
let pre_trans = Eva.Results.expr_dependencies expr request in
merge_deps
- (fun d -> Function_Froms.Memory.find_precise deps_tbl d) pre_trans
+ (fun d -> Eva.Assigns.Memory.find_precise deps_tbl d) pre_trans
let lval_to_zone_with_deps stmt lv =
let request = To_Use.stmt_request stmt in
@@ -238,12 +238,12 @@ struct
let empty_from =
{ additional_deps_table = ZoneStmtMap.empty;
additional_deps = Zone.bottom;
- deps_table = Function_Froms.Memory.empty }
+ deps_table = Eva.Assigns.Memory.empty }
let bottom_from =
{ additional_deps_table = ZoneStmtMap.empty;
additional_deps = Zone.bottom;
- deps_table = Function_Froms.Memory.bottom }
+ deps_table = Eva.Assigns.Memory.bottom }
module Computer = struct
@@ -253,11 +253,11 @@ struct
let callwise_states_with_formals = Stmt.Hashtbl.create 7
let substitute call_site_froms extra_loc deps =
- let subst_deps = Function_Froms.Memory.substitute call_site_froms deps in
- Function_Froms.Deps.add_indirect_dep subst_deps extra_loc
+ let subst_deps = From_memory.substitute call_site_froms deps in
+ Eva.Deps.add_indirect subst_deps extra_loc
let display_one_from fmt v =
- Function_Froms.Memory.pretty fmt v.deps_table;
+ Eva.Assigns.Memory.pretty fmt v.deps_table;
Format.fprintf fmt "Additional Variable Map : %a@\n"
ZoneStmtMap.pretty v.additional_deps_table;
Format.fprintf fmt
@@ -270,7 +270,7 @@ struct
let transfer_conditional_exp s exp state =
let additional = find s state.deps_table exp in
- let additional = Function_Froms.Deps.to_zone additional in
+ let additional = Eva.Deps.to_zone additional in
{state with
additional_deps_table =
ZoneStmtMap.add s additional state.additional_deps_table;
@@ -291,10 +291,10 @@ struct
m, new_z, false
in
let map =
- Function_Froms.Memory.join new_.deps_table old.deps_table
+ Eva.Assigns.Memory.join new_.deps_table old.deps_table
in
let included' =
- Function_Froms.Memory.is_included new_.deps_table old.deps_table
+ Eva.Assigns.Memory.is_included new_.deps_table old.deps_table
in
{ deps_table = map;
additional_deps_table = additional_map;
@@ -314,12 +314,12 @@ struct
let deps, loc, exact =
lval_to_precise_loc_with_deps stmt ~for_writing:(not init) lv
in
- let deps_of_deps = Function_Froms.Memory.find state.deps_table deps in
+ let deps_of_deps = Eva.Assigns.Memory.find state.deps_table deps in
let all_indirect = Zone.join state.additional_deps deps_of_deps in
- let deps = Function_Froms.Deps.add_indirect_dep deps_right all_indirect in
+ let deps = Eva.Deps.add_indirect deps_right all_indirect in
let access = if init then Read else Write in
{ state with deps_table =
- Function_Froms.Memory.add_binding_precise_loc
+ Eva.Assigns.Memory.add_binding_precise_loc
~exact access state.deps_table loc deps }
let transfer_call stmt dest f args _loc state =
@@ -328,9 +328,7 @@ struct
let called_vinfos = Eva.Results.(eval_callee f request |> default []) in
let f_deps = Eva.Results.expr_deps f request in
(* dependencies for the evaluation of [f] *)
- let f_deps =
- Function_Froms.Memory.find state.deps_table f_deps
- in
+ let f_deps = Eva.Assigns.Memory.find state.deps_table f_deps in
let additional_deps =
Zone.join
state.additional_deps
@@ -350,8 +348,8 @@ struct
state
else
let froms_call = To_Use.get_from_call kf stmt in
- let froms_call_table = froms_call.Function_Froms.deps_table in
- if Function_Froms.Memory.is_bottom froms_call_table then
+ let froms_call_table = froms_call.Eva.Assigns.memory in
+ if Eva.Assigns.Memory.is_bottom froms_call_table then
bottom_from
else
let formal_args = Kernel_function.get_formals kf in
@@ -360,7 +358,7 @@ struct
List.iter2
(fun vi from ->
state_with_formals :=
- Function_Froms.Memory.bind_var
+ From_memory.bind_var
vi from !state_with_formals;
) formal_args args_froms;
with Invalid_argument _ ->
@@ -381,10 +379,10 @@ struct
but before the result assignment *)
let deps_after_call =
let before_call = state.deps_table in
- let open Function_Froms in
- let subst d = DepsOrUnassigned.subst subst_before_call d in
- let call_substituted = Memory.map subst froms_call_table in
- Memory.compose call_substituted before_call
+ let call_substituted =
+ From_memory.map subst_before_call froms_call_table
+ in
+ From_memory.compose call_substituted before_call
in
let state = {state with deps_table = deps_after_call } in
(* Treatement for the possible assignment
@@ -392,7 +390,7 @@ struct
match dest with
| None -> state
| Some lv ->
- let return_from = froms_call.Function_Froms.deps_return in
+ let return_from = froms_call.Eva.Assigns.return in
let deps_ret = subst_before_call return_from in
let init = Cil.is_mutable_or_initialized lv in
transfer_assign stmt ~init lv deps_ret state
@@ -404,7 +402,7 @@ struct
| Some acc_memory ->
Some
{state with
- deps_table = Function_Froms.Memory.join
+ deps_table = Eva.Assigns.Memory.join
p.deps_table
acc_memory.deps_table}
in
@@ -452,7 +450,7 @@ struct
(* If implicit zero-initializers have been skipped, also mark
the entire array as initialized from no dependency (nothing
is read by the implicit zero-initializers). *)
- transfer_assign stmt ~init:true lv Function_Froms.Deps.bottom r
+ transfer_assign stmt ~init:true lv Eva.Deps.bottom r
in
aux (Cil.var v) i state
| Call (lvaloption,funcexp,argl,loc) ->
@@ -521,7 +519,7 @@ struct
(* Filter out unreachable values. *)
let transfer_stmt s d =
if Eva.Results.is_reachable s &&
- not (Function_Froms.Memory.is_bottom d.deps_table)
+ not (Eva.Assigns.Memory.is_bottom d.deps_table)
then transfer_stmt s d
else []
@@ -547,30 +545,27 @@ struct
(* Remove all local variables and formals from table *)
- let externalize return kf state =
- let deps_return =
- (match return.skind with
+ let externalize return_stmt kf state =
+ let return =
+ (match return_stmt.skind with
| Return (Some ({enode = Lval v}),_) ->
- let zone = lval_to_zone_with_deps return v in
- let deps = Function_Froms.Memory.find_precise state.deps_table zone in
+ let zone = lval_to_zone_with_deps return_stmt v in
+ let deps = Eva.Assigns.Memory.find_precise state.deps_table zone in
let size = Bit_utils.sizeof (Cil.typeOfLval v) in
- Function_Froms.(Memory.add_to_return ~size deps)
+ From_memory.add_to_return ~size deps
| Return (None,_) ->
- Function_Froms.Memory.default_return
+ From_memory.default_return
| _ -> assert false)
in
let accept = To_Use.keep_base kf in
- let deps_table =
- Function_Froms.Memory.filter_base accept state.deps_table
- in
- { deps_return = deps_return;
- Function_Froms.deps_table = deps_table }
+ let memory = Eva.Assigns.Memory.filter_base accept state.deps_table in
+ Eva.Assigns.{ return; memory }
let compute_using_cfg kf =
match kf.fundec with
| Declaration _ -> assert false
| Definition (f,_) ->
- if not (Eva.Analysis.save_results kf) then Function_Froms.top
+ if not (Eva.Analysis.save_results kf) then Eva.Assigns.top
else
try
Stack.iter (fun g -> if kf == g then raise Exit) call_stack;
@@ -615,16 +610,19 @@ struct
From_parameters.result
"Non-terminating function %a (no dependencies)"
Kernel_function.pretty kf;
- { Function_Froms.deps_return =
- Function_Froms.Memory.default_return;
- deps_table = Function_Froms.Memory.bottom }
+ Eva.Assigns.{
+ return = From_memory.default_return;
+ memory = Eva.Assigns.Memory.bottom
+ }
end
in
last_from
with Exit (* Recursive call *) ->
- { Function_Froms.deps_return = Function_Froms.Memory.default_return;
- deps_table = Function_Froms.Memory.empty }
+ {
+ return = From_memory.default_return;
+ memory = Eva.Assigns.Memory.empty
+ }
let compute_using_prototype kf =
let state = Eva.Results.(at_start_of kf |> get_cvalue_model) in
diff --git a/src/plugins/from/from_compute.mli b/src/plugins/from/from_compute.mli
index 9beabb6c488608a4c1efd485a7b0d775dbff2859..a48e9c38d2675bd00784dc2a7af4a1230328ccf9 100644
--- a/src/plugins/from/from_compute.mli
+++ b/src/plugins/from/from_compute.mli
@@ -30,7 +30,7 @@ open Cil_types
module type To_Use =
sig
(** How to find the Froms for a given call during the analysis. *)
- val get_from_call : kernel_function -> stmt -> Function_Froms.t
+ val get_from_call : kernel_function -> stmt -> Eva.Assigns.t
(** The Eva request that can be used to evaluate expressions at a given
statement through the Eva public API. *)
@@ -43,7 +43,7 @@ sig
(** Clean the given from (that have been computed for the given function),
optionally save them, and return the cleaned result. *)
- val cleanup_and_save : kernel_function -> Function_Froms.t -> Function_Froms.t
+ val cleanup_and_save : kernel_function -> Eva.Assigns.t -> Eva.Assigns.t
end
(** Function that compute the Froms from a given prototype, called
@@ -52,14 +52,14 @@ val compute_using_prototype_for_state :
Cvalue.Model.t ->
Kernel_function.t ->
assigns ->
- Function_Froms.froms
+ Eva.Assigns.t
(** Functor computing the functional dependencies, according to the three
modules above. *)
module Make (_: To_Use) : sig
(** Compute the dependencies of the given function, and return them *)
- val compute_and_return : Kernel_function.t -> Function_Froms.t
+ val compute_and_return : Kernel_function.t -> Eva.Assigns.t
(** Compute the dependencies of the given function *)
val compute : Kernel_function.t -> unit
diff --git a/src/plugins/from/from_memory.ml b/src/plugins/from/from_memory.ml
new file mode 100644
index 0000000000000000000000000000000000000000..57d9fde7a112b070d89182f35e8ac20107f5bc62
--- /dev/null
+++ b/src/plugins/from/from_memory.ml
@@ -0,0 +1,248 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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 Locations
+module Deps = Eva.Deps
+
+module DepsOrUnassigned = struct
+ include Eva.Assigns.DepsOrUnassigned
+
+ let subst f d =
+ match d with
+ | DepsBottom -> DepsBottom
+ | Unassigned -> Unassigned
+ | AssignedFrom fd ->
+ let fd' = f fd in
+ if fd == fd' then d else AssignedFrom fd'
+ | MaybeAssignedFrom fd ->
+ let fd' = f fd in
+ if fd == fd' then d else MaybeAssignedFrom fd'
+
+ let compose d1 d2 =
+ match d1, d2 with
+ | DepsBottom, _ | _, DepsBottom ->
+ DepsBottom (* could indicate dead code. Not used in practice anyway *)
+ | Unassigned, _ -> d2
+ | AssignedFrom _, _ -> d1
+ | MaybeAssignedFrom _, Unassigned -> d1
+ | MaybeAssignedFrom d1, MaybeAssignedFrom d2 ->
+ MaybeAssignedFrom (Deps.join d1 d2)
+ | MaybeAssignedFrom d1, AssignedFrom d2 ->
+ AssignedFrom (Deps.join d1 d2)
+
+ (* for backwards compatibility *)
+ let pretty fmt fd =
+ match fd with
+ | DepsBottom -> Format.pp_print_string fmt "DEPS_BOTTOM"
+ | Unassigned -> Format.pp_print_string fmt "(SELF)"
+ | AssignedFrom d -> Zone.pretty fmt (Deps.to_zone d)
+ | MaybeAssignedFrom d ->
+ Format.fprintf fmt "%a (and SELF)" Zone.pretty (Deps.to_zone d)
+
+ let pretty_precise fmt = function
+ | DepsBottom -> Format.pp_print_string fmt "DEPS_BOTTOM"
+ | Unassigned -> Format.pp_print_string fmt "UNASSIGNED"
+ | AssignedFrom fd -> Deps.pretty_precise fmt fd
+ | MaybeAssignedFrom fd ->
+ (* '(or UNASSIGNED)' would be a better pretty-printer, we use
+ '(and SELF)' only for compatibility reasons *)
+ Format.fprintf fmt "%a (and SELF)" Deps.pretty_precise fd
+end
+
+include Eva.Assigns.Memory
+
+let bind_var vi v m =
+ let z = Locations.zone_of_varinfo vi in
+ add_binding ~exact:true m z v
+
+let unbind_var vi m =
+ remove_base (Base.of_varinfo vi) m
+
+let map f = map (DepsOrUnassigned.subst f)
+
+let is_unassigned m =
+ LOffset.is_same_value m DepsOrUnassigned.Unassigned
+
+(* Unassigned is a neutral value for compose, on both sides *)
+let decide_compose m1 m2 =
+ if m1 == m2 || is_unassigned m1 then LOffset.ReturnRight
+ else if is_unassigned m2 then LOffset.ReturnLeft
+ else LOffset.Recurse
+
+let compose_map =
+ let cache = Hptmap_sig.PersistentCache "From_memory.compose" in
+ (* Partial application is important because of the cache. Idempotent,
+ because [compose x x] is always equal to [x]. *)
+ map2 ~cache ~symmetric:false ~idempotent:true ~empty_neutral:true
+ decide_compose DepsOrUnassigned.compose
+
+let compose m1 m2 = match m1, m2 with
+ | Top, _ | _, Top -> Top
+ | Map m1, Map m2 -> Map (compose_map m1 m2)
+ | Bottom, (Map _ | Bottom) | Map _, Bottom -> Bottom
+
+
+(* ----- Substitute --------------------------------------------------------- *)
+
+(** Auxiliary function that substitutes the data right-hand part of a
+ dependency by a pre-existing From state. The returned result is a Deps.t:
+ the data part will be the data part of the complete result, the indirect
+ part will be added to the indirect part of the final result. *)
+(* This function iterates simultaneously on a From memory, and on a zone.
+ It is cached. The definitions below are used to call the function that
+ does the recursive descent. *)
+let substitute_data_deps =
+ (* Nothing left to substitute, return z unchanged *)
+ let empty_right z = Deps.data z in
+ (* Zone to substitute is empty *)
+ let empty_left _ = Deps.bottom in
+ (* [b] is in the zone and substituted. Rewrite appropriately *)
+ let both b itvs offsm = find_precise_loffset offsm b itvs in
+ let join = Deps.join in
+ let empty = Deps.bottom in
+ let cache = Hptmap_sig.PersistentCache "From_memory.substitute_data" in
+ let f_map =
+ Zone.fold2_join_heterogeneous
+ ~cache ~empty_left ~empty_right ~both ~join ~empty
+ in
+ fun call_site_froms z ->
+ match call_site_froms with
+ | Bottom -> Deps.bottom
+ | Top -> Deps.top
+ | Map m ->
+ try f_map z (shape m)
+ with Abstract_interp.Error_Top -> Deps.top
+
+(** Auxiliary function that substitutes the indirect right-hand part of a
+ dependency by a pre-existing From state. The returned result is a zone,
+ which will be added to the indirect part of the final result. *)
+let substitute_indirect_deps =
+ (* Nothing left to substitute, z is directly an indirect dependency *)
+ let empty_right z = z in
+ (* Zone to substitute is empty *)
+ let empty_left _ = Zone.bottom in
+ let both b itvs offsm =
+ (* Both the found data and indirect dependencies are computed for indirect
+ dependencies: merge to a single zone *)
+ Deps.to_zone (find_precise_loffset offsm b itvs)
+ in
+ let join = Zone.join in
+ let empty = Zone.bottom in
+ let cache = Hptmap_sig.PersistentCache "From_memory.substitute_indirect" in
+ let f_map =
+ Zone.fold2_join_heterogeneous
+ ~cache ~empty_left ~empty_right ~both ~join ~empty
+ in
+ fun call_site_froms z ->
+ match call_site_froms with
+ | Bottom -> Zone.bottom
+ | Top -> Zone.top
+ | Map m ->
+ try f_map z (shape m)
+ with Abstract_interp.Error_Top -> Zone.top
+
+let substitute call_site_froms deps =
+ let open Deps in
+ let { data; indirect } = deps in
+ (* depending directly on an indirect dependency -> indirect,
+ depending indirectly on a direct dependency -> indirect *)
+ let dirdeps = substitute_data_deps call_site_froms data in
+ let inddeps = substitute_indirect_deps call_site_froms indirect in
+ let dir = dirdeps.data in
+ let ind = Zone.(join dirdeps.indirect inddeps) in
+ { data = dir; indirect = ind }
+
+
+(* ----- Dependency of returned values -------------------------------------- *)
+
+type return = Deps.t
+
+let default_return = Deps.bottom
+
+let top_return = Deps.top
+
+let add_to_return ?start:(_start=0) ~size:_size ?(m=default_return) v =
+ Deps.join m v
+(*
+ let start = Ival.of_int start in
+ let itvs = Int_Intervals.from_ival_size start size in
+ LOffset.add_iset ~exact:true itvs (DepsOrUnassigned.AssignedFrom v) m
+*)
+
+let top_return_size size =
+ add_to_return ~size Deps.top
+
+let collapse_return x = x
+
+
+(* ----- Pretty-printing ---------------------------------------------------- *)
+
+let () = imprecise_write_msg := "dependencies to update"
+
+let pretty_skip = function
+ | DepsOrUnassigned.DepsBottom -> true
+ | DepsOrUnassigned.Unassigned -> true
+ | DepsOrUnassigned.AssignedFrom _ -> false
+ | DepsOrUnassigned.MaybeAssignedFrom _ -> false
+
+let pretty =
+ pretty_generic_printer
+ ~skip_v:pretty_skip ~pretty_v:DepsOrUnassigned.pretty ~sep:"FROM" ()
+
+let pretty_ind_data =
+ pretty_generic_printer
+ ~skip_v:pretty_skip ~pretty_v:DepsOrUnassigned.pretty_precise ~sep:"FROM"
+ ()
+
+(** same as pretty, but uses the type of the function to output more
+ precise information.
+ @raise Error if the given type is not a function type
+*)
+let pretty_with_type ~indirect typ fmt assigns =
+ let Eva.Assigns.{ memory; return } = assigns in
+ let (rt_typ,_,_,_) = Cil.splitFunctionType typ in
+ if is_bottom memory
+ then Format.fprintf fmt
+ "@[NON TERMINATING - NO EFFECTS@]"
+ else
+ let map_pretty =
+ if indirect
+ then pretty_ind_data
+ else pretty
+ in
+ if Cil.isVoidType rt_typ
+ then begin
+ if is_empty memory
+ then Format.fprintf fmt "@[NO EFFECTS@]"
+ else map_pretty fmt memory
+ end
+ else
+ let pp_space fmt =
+ if not (is_empty memory) then
+ Format.fprintf fmt "@ "
+ in
+ Format.fprintf fmt "@[<v>%a%t@[\\result FROM @[%a@]@]@]"
+ map_pretty memory pp_space
+ (if indirect then Deps.pretty_precise else Deps.pretty) return
+
+let pretty_with_type_indirect = pretty_with_type ~indirect:true
+let pretty_with_type = pretty_with_type ~indirect:false
diff --git a/src/plugins/from/from_memory.mli b/src/plugins/from/from_memory.mli
new file mode 100644
index 0000000000000000000000000000000000000000..8e6f08e5905a93ea68fc7f20a0c284b27eaa0f02
--- /dev/null
+++ b/src/plugins/from/from_memory.mli
@@ -0,0 +1,78 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Utilitary functions on the {!Eva.Froms.Memory.t} type. *)
+
+type t = Eva.Assigns.Memory.t
+
+val top : t
+
+val bind_var: Cil_types.varinfo -> Eva.Deps.t -> t -> t
+val unbind_var: Cil_types.varinfo -> t -> t
+
+val map : (Eva.Deps.t -> Eva.Deps.t) -> t -> t
+
+val compose : t -> t -> t
+(** Sequential composition. See {!DepsOrUnassigned.compose}. *)
+
+val substitute : t -> Eva.Deps.t -> Eva.Deps.t
+(** [substitute m d] applies [m] to [d] so that any dependency in [d] is
+ expressed using the dependencies already present in [m]. For example,
+ [substitute 'x From y' 'x'] returns ['y']. *)
+
+(** {2 Dependencies for [\result]} *)
+
+type return = Eva.Deps.t
+(* Currently, this type is equal to [Eva.Deps.t]. However, some of the functions
+ below are more precise, and will be more useful when 'return' is
+ represented by a precise offsetmap. This would also require changing
+ the type of the [deps.return] of type Eva.Froms.t. *)
+
+(** Default value to use for storing the dependencies of [\result] *)
+val default_return: return
+
+(** Completely imprecise return *)
+val top_return: return
+
+(** Completely imprecise return of the given size *)
+val top_return_size: Int_Base.t -> return
+
+(** Add some dependencies to [\result], between bits [start] and
+ [start+size-1], to the [Deps.t] value; default value for [start] is 0.
+ If [m] is specified, the dependencies are added to it. Otherwise,
+ {!default_return} is used. *)
+val add_to_return:
+ ?start:int -> size:Int_Base.t -> ?m:return -> Eva.Deps.t -> return
+
+val collapse_return: return -> Eva.Deps.t
+
+(** {2 Pretty-printing} *)
+
+(** Display dependencies of a function, using the function's type to improve
+ readability *)
+val pretty_with_type: Cil_types.typ -> Eva.Assigns.t Pretty_utils.formatter
+
+(** Display dependencies of a function, using the function's type to improve
+ readability, separating direct and indirect dependencies *)
+val pretty_with_type_indirect:
+ Cil_types.typ ->
+ Eva.Assigns.t Pretty_utils.formatter
diff --git a/src/plugins/from/from_register.ml b/src/plugins/from/from_register.ml
index df9beea20f8bd31766c25136d413db7fb06a2b9f..680ad06894204d0f75bc0a4c0a372010ae9776f5 100644
--- a/src/plugins/from/from_register.ml
+++ b/src/plugins/from/from_register.ml
@@ -24,7 +24,7 @@ open Cil_types
let pretty_with_indirect fmt v =
let deps = Functionwise.get v in
- Function_Froms.pretty_with_type_indirect (Kernel_function.get_type v) fmt deps
+ From_memory.pretty_with_type_indirect (Kernel_function.get_type v) fmt deps
let display fmtopt =
Option.iter (fun fmt -> Format.fprintf fmt "@[<v>") fmtopt;
@@ -138,8 +138,8 @@ let print_calldeps () =
From_parameters.printf ~header
"@[ %a@]"
((if From_parameters.ShowIndirectDeps.get ()
- then Function_Froms.pretty_with_type_indirect
- else Function_Froms.pretty_with_type) typ)
+ then From_memory.pretty_with_type_indirect
+ else From_memory.pretty_with_type) typ)
d);
From_parameters.feedback "====== END OF CALLWISE DEPENDENCIES ======"
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index 484fbdba5b54ddcd4643bbba1f7f7e62d396d3e6..972c2749f7f19c2ea85b81ed1339a71acf19e48b 100644
--- a/src/plugins/from/functionwise.ml
+++ b/src/plugins/from/functionwise.ml
@@ -25,7 +25,7 @@ open Locations
module Tbl =
Kernel_function.Make_Table
- (Function_Froms)
+ (Eva.Assigns)
(struct
let name = "Functionwise dependencies"
let size = 17
@@ -53,7 +53,7 @@ module To_Use = struct
Eva.Logic_inout.accept_base ~formals:false ~locals:false kf
let cleanup kf froms =
- if Function_Froms.Memory.is_bottom froms.Function_Froms.deps_table
+ if Eva.Assigns.Memory.is_bottom froms.Eva.Assigns.memory
then froms
else
let accept_base =
@@ -75,11 +75,9 @@ module To_Use = struct
zone_substitution x
with Abstract_interp.Error_Top -> Zone.top
in
- let map_zone = Function_Froms.Deps.map zone_substitution in
- let subst = Function_Froms.DepsOrUnassigned.subst map_zone in
- let open Function_Froms in
- { deps_table = Memory.map subst froms.deps_table;
- deps_return = Deps.map zone_substitution froms.deps_return;
+ let map_zone = Eva.Deps.map zone_substitution in
+ { memory = From_memory.map map_zone froms.memory;
+ return = Eva.Deps.map zone_substitution froms.return;
}
let cleanup_and_save kf froms =
@@ -111,7 +109,7 @@ let is_computed = Tbl.mem
let get = To_Use.memo
let pretty fmt v =
- Function_Froms.pretty_with_type (Kernel_function.get_type v) fmt (get v)
+ From_memory.pretty_with_type (Kernel_function.get_type v) fmt (get v)
(*
Local Variables:
diff --git a/src/plugins/from/functionwise.mli b/src/plugins/from/functionwise.mli
index 2f81e01120c45eb4fb58e1d242dd885c6f760136..5f0ba60bace3c7b9c29a4dfa3c4506482b3b25a7 100644
--- a/src/plugins/from/functionwise.mli
+++ b/src/plugins/from/functionwise.mli
@@ -29,5 +29,5 @@ val self : State.t
val compute : kernel_function -> unit
val compute_all : unit -> unit
val is_computed : kernel_function -> bool
-val get : Cil_types.kernel_function -> Function_Froms.froms
+val get : Cil_types.kernel_function -> Eva.Assigns.t
val pretty : Format.formatter -> kernel_function -> unit
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index d12bc75efab318688cbc438b023c28003b81d836..74d506662ca0d90cfad653097b3140edffa329d9 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -514,26 +514,24 @@ let get_external_aux ?stmt kf =
r
else !ref_get_external kf
-let extract_inout_from_froms froms =
- let open Function_Froms in
- let {deps_return; deps_table } = froms in
- let in_return = Deps.to_zone deps_return in
+let extract_inout_from_froms assigns =
+ let Eva.Assigns.{ return = deps_return; memory = deps_table } = assigns in
+ let in_return = Eva.Deps.to_zone deps_return in
let in_, out_ =
match deps_table with
- | Memory.Top -> Zone.top, Zone.top
- | Memory.Bottom -> Zone.bottom, Zone.bottom
- | Memory.Map m ->
+ | Top -> Zone.top, Zone.top
+ | Bottom -> Zone.bottom, Zone.bottom
+ | Map m ->
let aux_from out in_ (acc_in,acc_out as acc) =
- let open DepsOrUnassigned in
(* Skip zones fully unassigned, they are not really port of the
dependencies, but just present in the offsetmap to avoid "holes" *)
- match in_ with
+ match (in_ : Eva.Assigns.DepsOrUnassigned.t) with
| DepsBottom | Unassigned -> acc
| AssignedFrom in_ | MaybeAssignedFrom in_ ->
- Zone.join acc_in (Deps.to_zone in_),
+ Zone.join acc_in (Eva.Deps.to_zone in_),
Zone.join acc_out out
in
- Memory.fold aux_from m (Zone.bottom, Zone.bottom)
+ Eva.Assigns.Memory.fold aux_from m (Zone.bottom, Zone.bottom)
in
(Zone.join in_return in_), out_
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index 6db271d345e2405a1761dc0f0ea9be74ad26a0d8..c2268d86d6f084325f3b5cf096c294eb2e2749d5 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -566,7 +566,7 @@ let finalize_pdg pdg from_opt =
(* TODO : also add the nodes for the other from ! *)
let state = match last_state with Some s -> s | None -> assert false in
let process_out out deps s =
- let open Function_Froms.DepsOrUnassigned in
+ let open Eva.Assigns.DepsOrUnassigned in
if (equal Unassigned deps)
then s
else
@@ -574,24 +574,23 @@ let finalize_pdg pdg from_opt =
let default = may_be_unassigned deps in
add_from pdg state s out (default, from_out)
in
- let from_table = froms.Function_Froms.deps_table in
+ let from_table = froms.Eva.Assigns.memory in
let new_state =
- if Function_Froms.Memory.is_bottom from_table then
+ if Eva.Assigns.Memory.is_bottom from_table then
Pdg_state.bottom
else
let new_state =
match from_table with
- | Function_Froms.Memory.Top ->
+ | Top ->
process_out
- Locations.Zone.top Function_Froms.DepsOrUnassigned.top state
- | Function_Froms.Memory.Map m ->
- Function_Froms.Memory.fold_fuse_same process_out m state
- | Function_Froms.Memory.Bottom -> assert false (* checked above *)
+ Locations.Zone.top Eva.Assigns.DepsOrUnassigned.top state
+ | Map m ->
+ Eva.Assigns.Memory.fold_fuse_same process_out m state
+ | Bottom -> assert false (* checked above *)
in
if not (Kernel_function.returns_void pdg.fct) then begin
- let from0 = froms.Function_Froms.deps_return in
- let deps_ret = Function_Froms.Memory.collapse_return from0 in
- let deps_ret = Function_Froms.Deps.to_zone deps_ret in
+ let deps_ret = froms.Eva.Assigns.return in
+ let deps_ret = Eva.Deps.to_zone deps_ret in
ignore
(create_fun_output_node pdg (Some new_state) deps_ret)
end;
@@ -648,49 +647,44 @@ let process_args pdg st stmt argl =
and [new_state] the state to modify.
* Process call outputs (including returned value) *)
let call_outputs pdg state_before_call state_with_inputs stmt
- lvaloption froms fct_dpds =
+ lvaloption assigns fct_dpds =
(* obtain inputs from state_with_inputs
to avoid mixing in and out *)
- let froms_deps_return = froms.Function_Froms.deps_return in
- let from_table = froms.Function_Froms.deps_table in
+ let Eva.Assigns.{ return = return_deps; memory = memory_deps } = assigns in
let print_outputs fmt =
Format.fprintf fmt "call outputs : %a"
- Function_Froms.Memory.pretty from_table;
+ Eva.Assigns.Memory.pretty memory_deps;
if not (lvaloption = None) then
Format.fprintf fmt "\t and \\result %a@."
- Function_Froms.Deps.pretty froms_deps_return
+ Eva.Deps.pretty return_deps
in
debug "%t" print_outputs;
let process_out out deps state =
- if Function_Froms.DepsOrUnassigned.(equal Unassigned deps) then
+ if Eva.Assigns.DepsOrUnassigned.(equal Unassigned deps) then
state
else
- let from_out = Function_Froms.DepsOrUnassigned.to_zone deps in
- let default = Function_Froms.DepsOrUnassigned.may_be_unassigned deps in
+ let from_out = Eva.Assigns.DepsOrUnassigned.to_zone deps in
+ let default = Eva.Assigns.DepsOrUnassigned.may_be_unassigned deps in
process_call_output
pdg state_with_inputs state stmt out default from_out fct_dpds
in
- if Function_Froms.Memory.is_bottom from_table then
+ if Eva.Assigns.Memory.is_bottom memory_deps then
Pdg_state.bottom
else
let state_with_outputs =
- let open Function_Froms in
- match from_table with
- | Memory.Top ->
+ match memory_deps with
+ | Top ->
process_out
- Locations.Zone.top DepsOrUnassigned.top state_before_call
- | Memory.Bottom -> assert false (* checked above *)
- | Memory.Map m ->
- Memory.fold_fuse_same process_out m state_before_call
+ Locations.Zone.top Eva.Assigns.DepsOrUnassigned.top state_before_call
+ | Bottom -> assert false (* checked above *)
+ | Map m ->
+ Eva.Assigns.Memory.fold_fuse_same process_out m state_before_call
in
match lvaloption with
| None -> state_with_outputs
| Some lval ->
- let r_dpds =
- Function_Froms.Memory.collapse_return froms_deps_return
- in
- let r_dpds = Function_Froms.Deps.to_zone r_dpds in
+ let r_dpds = Eva.Deps.to_zone return_deps in
let (l_loc, exact, l_dpds, l_decl) = get_lval_infos lval stmt in
process_call_return
pdg
diff --git a/src/plugins/scope/zones.ml b/src/plugins/scope/zones.ml
index 03a5d675411bf205295840b9b9102a57a8931f6f..3c2ecaa401f5672483771b620db63c95b9c8dea9 100644
--- a/src/plugins/scope/zones.ml
+++ b/src/plugins/scope/zones.ml
@@ -79,9 +79,8 @@ let process_call_res data stmt lvaloption froms =
let data = match lvaloption with
| None -> false, data
| Some lval ->
- let ret_dpds = froms.Function_Froms.deps_return in
- let r_dpds = Function_Froms.Memory.collapse_return ret_dpds in
- let r_dpds = Function_Froms.Deps.to_zone r_dpds in
+ let ret_dpds = froms.Eva.Assigns.return in
+ let r_dpds = Eva.Deps.to_zone ret_dpds in
let l_dpds, exact, l_zone =
get_lval_zones ~for_writing:true stmt lval in
compute_new_data data l_zone l_dpds exact r_dpds
@@ -92,10 +91,10 @@ let process_call_res data stmt lvaloption froms =
* Moreover, we need to add the part of [data_after] that has not been
* modified for sure. *)
let process_froms data_after froms =
- let from_table = froms.Function_Froms.deps_table in
+ let from_table = froms.Eva.Assigns.memory in
let process_out_call out deps (to_prop, used, new_data) =
- let out_dpds = Function_Froms.DepsOrUnassigned.to_zone deps in
- let default = Function_Froms.DepsOrUnassigned.may_be_unassigned deps in
+ let out_dpds = Eva.Assigns.DepsOrUnassigned.to_zone deps in
+ let default = Eva.Assigns.DepsOrUnassigned.may_be_unassigned deps in
let exact = not default in
(* be careful to compare out with data_after and not new_data *)
if (Data.intersects data_after out) then
@@ -113,12 +112,12 @@ let process_froms data_after froms =
let used = false in (* is the call needed ? *)
let to_prop, used, new_data =
match from_table with
- | Function_Froms.Memory.Bottom -> to_prop, used, new_data
- | Function_Froms.Memory.Top ->
- let v = Function_Froms.DepsOrUnassigned.top in
+ | Bottom -> to_prop, used, new_data
+ | Top ->
+ let v = Eva.Assigns.DepsOrUnassigned.top in
process_out_call Locations.Zone.top v (to_prop, used, new_data)
- | Function_Froms.Memory.Map m ->
- Function_Froms.Memory.fold process_out_call m (to_prop, used, new_data)
+ | Map m ->
+ Eva.Assigns.Memory.fold process_out_call m (to_prop, used, new_data)
in let data = Data.merge to_prop new_data in
(used, data)