From 876dcf7c5e1e2be752a395b2e6c5f18ba2df8814 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 29 Nov 2021 17:43:12 +0100
Subject: [PATCH] [Eva] multidim: do not update segmentations that do not
contain assigned variables
---
.../abstract_interp/abstract_offset.ml | 18 ++++-
.../abstract_interp/abstract_offset.mli | 1 +
src/plugins/value/domains/multidim_domain.ml | 81 +++++++++++++++----
3 files changed, 83 insertions(+), 17 deletions(-)
diff --git a/src/kernel_services/abstract_interp/abstract_offset.ml b/src/kernel_services/abstract_interp/abstract_offset.ml
index e315b281272..b4fe5713dd1 100644
--- a/src/kernel_services/abstract_interp/abstract_offset.ml
+++ b/src/kernel_services/abstract_interp/abstract_offset.ml
@@ -31,6 +31,7 @@ sig
val of_ival : base_typ:Cil_types.typ -> typ:Cil_types.typ -> Ival.t -> t
val of_term_offset : Cil_types.typ -> Cil_types.term_offset -> t
val is_singleton : t -> bool
+ val references : t -> Cil_types.varinfo list
end
type typed_offset =
@@ -87,7 +88,7 @@ struct
| Some size_exp ->
match Cil.constFoldToInt size_exp with
| None -> None
- | Some size when Integer.(gt size zero) -> Some (Integer.zero, size)
+ | Some size when Integer.(gt size zero) -> Some Integer.(zero, pred size)
| Some _ -> None
let array_range array_size =
@@ -208,6 +209,17 @@ struct
| Field (_fi, sub) -> is_singleton sub
| Index (e, ival, _elem_typ, sub) ->
(Option.is_some e || Int_val.is_singleton ival) && is_singleton sub
+
+ let references =
+ let rec aux acc = function
+ | NoOffset _ -> acc
+ | Field (_, sub) | Index (None, _, _, sub) -> aux acc sub
+ | Index (Some e, _, _, sub) ->
+ let r = Cil.extract_varinfos_from_exp e in
+ let acc = (Cil_datatype.Varinfo.Set.to_seq r |> List.of_seq) @ acc in
+ aux acc sub
+ in
+ aux []
end
module TypedOffsetOrTop =
@@ -245,4 +257,8 @@ struct
let is_singleton = function
| `Top -> false
| `Value o -> TypedOffset.is_singleton o
+
+ let references = function
+ | `Top -> []
+ | `Value o -> TypedOffset.references o
end
diff --git a/src/kernel_services/abstract_interp/abstract_offset.mli b/src/kernel_services/abstract_interp/abstract_offset.mli
index 96723402c80..5b2dc622609 100644
--- a/src/kernel_services/abstract_interp/abstract_offset.mli
+++ b/src/kernel_services/abstract_interp/abstract_offset.mli
@@ -31,6 +31,7 @@ sig
val of_ival : base_typ:Cil_types.typ -> typ:Cil_types.typ -> Ival.t -> t
val of_term_offset : Cil_types.typ -> Cil_types.term_offset -> t
val is_singleton : t -> bool
+ val references : t -> Cil_types.varinfo list (* variables referenced in the offset *)
end
type typed_offset =
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index deb69557b5e..f7ad735a528 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -108,12 +108,22 @@ struct
let fold : (base-> offset -> 'a -> 'a) -> t -> 'a -> 'a = Map.fold
+ let bases map =
+ Map.fold (fun b _ acc -> b :: acc) map []
+
let is_singleton map =
match map_to_singleton map with
| None -> false
| Some (b,o) ->
not (Base.is_weak b) && Offset.is_singleton o
+ let references map =
+ let module Set = Cil_datatype.Varinfo.Set in
+ let add_refs _b o =
+ Set.union (Set.of_list (Offset.references o))
+ in
+ Map.fold add_refs map Set.empty |> Set.to_seq |> List.of_seq
+
let of_var (vi : Cil_types.varinfo) : t =
Map.singleton (Base.of_varinfo vi) (`Value (NoOffset vi.vtype))
@@ -184,7 +194,7 @@ struct
include Datatype.Make (Prototype)
let pretty = Memory.pretty
- let pretty_debug = Memory.pretty
+ let _pretty_debug = Memory.pretty
let top = Memory.top
let is_top = Memory.is_top
let is_included = Memory.is_included
@@ -233,15 +243,30 @@ struct
Memory.overwrite ~oracle ~weak dst loc src
end
+(* References to variables inside array segmentation.
+ For instance if an array A is described with the segmentation
+ 0..i-1 ; i ; i+1..10
+ then, everytime i is changed, the segmentation must be updated. This requires
+ referencing every base where at least one segmentation references i. *)
+module References =
+struct
+ include Base.Hptset (* The set of bases referencing the variable *)
+end
module DomainLattice =
struct
(* The domain is essentially a map from bases to individual memory abstractions *)
module Initial_Values = struct let v = [[]] end
module Deps = struct let l = [Ast.self] end
+ module V =
+ struct
+ include Datatype.Pair (Memory) (References)
+ let pretty_debug = pretty
+ let top = Memory.top, References.empty
+ end
include Hptmap.Make
- (Base.Base) (Memory)
+ (Base.Base) (V)
(Hptmap.Comp_unused) (Initial_Values) (Deps)
type state = t
@@ -268,7 +293,7 @@ struct
| CLogic_Var _ | String _ -> false
let find_or_top (state : state) (b : base) =
- try find b state with Not_found -> Memory.top
+ try find b state with Not_found -> V.top
let remove_var (state : state) (v : Cil_types.varinfo) =
remove (Base.of_varinfo v) state
@@ -288,7 +313,7 @@ struct
state -> mdlocation -> a or_bottom =
fun map reduce state loc ->
let f base off acc =
- let v = map (find_or_top state base) off in
+ let v = map (fst (find_or_top state base)) off in
Bottom.join reduce (`Value v) acc
in
Location.fold f loc `Bottom
@@ -317,13 +342,20 @@ struct
let write (update : memory -> offset -> memory)
(state : state) (loc : mdlocation) : state =
+ let bases = Location.bases loc in
let f base off state =
if covers_base base then
- add base (update (find_or_top state base) off) state
+ let memory, refs = find_or_top state base in
+ add base (update memory off, refs) state
else
state
+ and add_ref state vi =
+ let base = Base.of_varinfo vi in
+ let memory, refs = find_or_top state base in
+ add base (memory, References.union refs (References.of_list bases)) state
in
- Location.fold f loc state
+ let state = Location.fold f loc state in
+ List.fold_left add_ref state (Location.references loc)
let set (state : state) (dst : mdlocation) (v : value) : state =
let weak = not (Location.is_singleton dst)
@@ -356,7 +388,7 @@ struct
let cache = cache_name "is_included" in
let decide_fst _b _v1 = true (* v2 is top *) in
let decide_snd _b _v2 = false (* v1 is top, v2 is not *) in
- let decide_both _ v1 v2 = Memory.is_included v1 v2 in
+ let decide_both _ (m1,_r1) (m2,_r2) = Memory.is_included m1 m2 in
let decide_fast s t = if s == t then PTrue else PUnknown in
binary_predicate cache UniversalPredicate
~decide_fast ~decide_fst ~decide_snd ~decide_both
@@ -375,9 +407,10 @@ struct
| Right -> mk_oracle s2
in
let cache = Hptmap_sig.NoCache
- and decide _ v1 v2 =
- let r = Memory.join ~oracle v1 v2 in
- if Memory.(is_top r) then None else Some r
+ and decide _ (m1,r1) (m2,r2) =
+ let m = Memory.join ~oracle m1 m2
+ and r = References.union r1 r2 in
+ if Memory.(is_top m) then None else Some (m,r)
in
inter ~cache ~symmetric:false ~idempotent:true ~decide s1 s2
@@ -387,9 +420,10 @@ struct
| Right -> mk_oracle s2
and _,get_hints = Widen.getWidenHints kf stmt in
let cache = Hptmap_sig.NoCache
- and decide base b1 b2 =
- let r = Memory.widen ~oracle (get_hints base) b1 b2 in
- if Memory.(is_top r) then None else Some r
+ and decide base (m1,r1) (m2,r2) =
+ let m = Memory.widen ~oracle (get_hints base) m1 m2
+ and r = References.union r1 r2 in
+ if Memory.(is_top m) then None else Some (m,r)
in
inter ~cache ~symmetric:false ~idempotent:true ~decide s1 s2
end
@@ -456,8 +490,6 @@ struct
let update_array_segmentation_bounds vi expr state =
(* TODO: more general transfer function *)
- (* TODO: only update memory models where the lval is present in the
- segmentation *)
let incr = Option.bind expr (fun expr ->
match expr.Cil_types.enode with
| BinOp ((PlusA|PlusPI), { enode=Lval (Var vi', NoOffset) }, exp, _typ)
@@ -474,7 +506,24 @@ struct
(* Very important : oracle must be the oracle before a non-invertible
assignement of the bound to allow removing of eventual empty slice
before the bound leaves the segmentation. *)
- map (Memory.incr_bound ~oracle:(mk_oracle state) vi incr) state
+ let oracle = mk_oracle state in
+ let references = snd (find_or_top state (Base.of_varinfo vi)) in
+ let update_ref base state =
+ let update (memory, refs) =
+ Memory.incr_bound ~oracle vi incr memory, refs
+ in
+ replace (Option.map update) base state
+ in
+ let state = References.fold update_ref references state in
+ (* If increment is None, every reference to vi should have been removed by
+ Memory.incr_bound *)
+ if Option.is_none incr then
+ replace
+ (Option.map (fun (memory, _refs) -> memory, References.empty))
+ (Base.of_varinfo vi)
+ state
+ else
+ state
let update_array_segmentation lval expr state =
match lval with
--
GitLab