From 7883e630310dec9895c65af47c7cccbfaa7bba52 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 22 Feb 2022 01:01:12 +0100
Subject: [PATCH] [Eva] multidim: add an annotation to control which bases are
tracked
---
src/plugins/value/domains/multidim_domain.ml | 166 ++++++++++++-------
src/plugins/value/utils/eva_annotations.ml | 50 +++++-
src/plugins/value/utils/eva_annotations.mli | 8 +-
3 files changed, 162 insertions(+), 62 deletions(-)
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index 2e732ece763..86d3850c471 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -305,6 +305,11 @@ struct
include Base.Hptset (* The set of bases referencing the variable *)
end
+module TrackedBases =
+struct
+ include Base.Hptset
+end
+
module DomainLattice =
struct
(* The domain is essentially a map from bases to individual memory abstractions *)
@@ -317,9 +322,31 @@ struct
let top = Memory.top, References.empty
end
- include Hptmap.Make
- (Base.Base) (V)
- (Hptmap.Comp_unused) (Initial_Values) (Deps)
+ module BaseMap =
+ struct
+ include
+ Hptmap.Make
+ (Base.Base) (V)
+ (Hptmap.Comp_unused) (Initial_Values) (Deps)
+
+ let find_or_top (state : t) (b : Base.t) =
+ try find b state with Not_found -> V.top
+
+ let remove_var (state : t) (v : Cil_types.varinfo) =
+ remove (Base.of_varinfo v) state
+
+ let remove_vars (state : t) (l : Cil_types.varinfo list) =
+ List.fold_left remove_var state l
+
+ let remove_loc (state : t) (loc : Precise_locs.precise_location) =
+ let loc = Precise_locs.imprecise_location loc in
+ Locations.(Location_Bits.fold_bases remove loc.loc state)
+ end
+
+ include Datatype.Pair_with_collections
+ (BaseMap)
+ (Datatype.Option (TrackedBases))
+ (struct let module_name = "DomainLattice" end)
type state = t
type value = Value.t
@@ -338,25 +365,19 @@ struct
(* Bases handling *)
- let covers_base (b : base) =
+ let covers_base (tracked : TrackedBases.t option) (b : base) : bool =
match b with
| Base.Var (vi, _) | Allocated (vi, _, _) ->
- not (Cil.typeHasQualifier "volatile" vi.vtype)
+ not (Cil.typeHasQualifier "volatile" vi.vtype) &&
+ Option.fold ~none:true ~some:(TrackedBases.mem b) tracked
| Null -> true
| CLogic_Var _ | String _ -> false
- let find_or_top (state : state) (b : base) =
- try find b state with Not_found -> V.top
-
- let remove_var (state : state) (v : Cil_types.varinfo) =
- remove (Base.of_varinfo v) state
+ let join_tracked tracked1 tracked2 =
+ match tracked1, tracked2 with
+ | None, tracked | tracked, None -> tracked
+ | Some s1, Some s2 -> Some (TrackedBases.union s1 s2)
- let remove_vars (state : state) (l : Cil_types.varinfo list) =
- List.fold_left remove_var state l
-
- let remove (state : state) (loc : location) =
- let loc = Precise_locs.imprecise_location loc in
- Locations.(Location_Bits.fold_bases remove loc.loc state)
(* Accesses *)
@@ -364,9 +385,9 @@ struct
type a .
(memory -> offset -> a) -> (a -> a -> a) ->
state -> mdlocation -> a or_bottom =
- fun map reduce state loc ->
+ fun map reduce (state,_tracked) loc ->
let f base off acc =
- let v = map (fst (find_or_top state base)) off in
+ let v = map (fst (BaseMap.find_or_top state base)) off in
Bottom.join reduce (`Value v) acc
in
Location.fold f loc `Bottom
@@ -421,11 +442,11 @@ struct
let oracle = mk_oracle state in
read (Memory.extract ~oracle) (Memory.smash ~oracle) state src
- let add_references state vi refs' =
+ let add_references (base_map,tracked) vi refs' =
let base = Base.of_varinfo vi in
- let memory, refs = find_or_top state base in
+ let memory, refs = BaseMap.find_or_top base_map base in
let refs'' = References.union refs (References.of_list refs') in
- add base (memory, refs'') state
+ BaseMap.add base (memory, refs'') base_map, tracked
let add_references_l state l refs =
List.fold_left (fun state vi -> add_references state vi refs) state l
@@ -433,11 +454,11 @@ struct
let write' (update : memory -> offset -> memory or_bottom)
(state : state) (loc : mdlocation) : state or_bottom =
let f base off state' =
- if covers_base base then
- state' >>- fun state ->
- let memory, refs = find_or_top state base in
+ state' >>- fun (base_map,tracked) ->
+ if covers_base tracked base then
+ let memory, refs = BaseMap.find_or_top base_map base in
update memory off >>-: fun memory' ->
- add base (memory', refs) state
+ BaseMap.add base (memory', refs) base_map, tracked
else
state'
in
@@ -475,26 +496,29 @@ struct
(* Lattice *)
- let top = empty
+ let top = BaseMap.empty, None
let is_included =
+ let open BaseMap in
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 _ (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
+ let is_included = binary_predicate cache UniversalPredicate
+ ~decide_fast ~decide_fst ~decide_snd ~decide_both
+ in
+ fun (m1,_) (m2,_) -> is_included m1 m2
let narrow =
+ let open BaseMap in
let cache = cache_name "narrow" in
- let decide _ v1 v2 =
- Memory.narrow v1 v2
- in
+ let decide _ v1 v2 = Memory.narrow v1 v2 in
let narrow = join ~cache ~symmetric:false ~idempotent:true ~decide in
- fun a b -> `Value (narrow a b)
+ fun (m1,t1) (m2,t2) -> `Value (narrow m1 m2, join_tracked t1 t2)
- let join s1 s2 =
+ let join (m1,t1 as s1) (m2,t2 as s2) =
+ let open BaseMap in
let oracle = function
| Abstract_memory.Left -> mk_oracle s1
| Right -> mk_oracle s2
@@ -505,9 +529,12 @@ struct
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
+ inter ~cache ~symmetric:false ~idempotent:true ~decide m1 m2,
+ join_tracked t1 t2
- let widen kf stmt s1 s2 =
+
+ let widen kf stmt (m1,t1 as s1) (m2,t2 as s2) =
+ let open BaseMap in
let oracle = function
| Abstract_memory.Left -> mk_oracle s1
| Right -> mk_oracle s2
@@ -518,7 +545,8 @@ struct
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
+ inter ~cache ~symmetric:false ~idempotent:true ~decide m1 m2,
+ join_tracked t1 t2
end
module Domain =
@@ -589,7 +617,7 @@ struct
let update valuation state =
assume_valuation valuation state
- let update_array_segmentation_bounds vi expr state =
+ let update_array_segmentation_bounds vi expr (base_map,tracked as state) =
(* TODO: more general transfer function *)
let incr = Option.bind expr (fun expr ->
match expr.Cil_types.enode with
@@ -608,23 +636,26 @@ struct
assignement of the bound to allow removing of eventual empty slice
before the bound leaves the segmentation. *)
let oracle = mk_oracle state in
- let references = snd (find_or_top state (Base.of_varinfo vi)) in
- let update_ref base state =
+ let references = snd (BaseMap.find_or_top base_map (Base.of_varinfo vi)) in
+ let update_ref base base_map =
let update (memory, refs) =
Memory.incr_bound ~oracle vi incr memory, refs
in
- replace (Option.map update) base state
+ BaseMap.replace (Option.map update) base base_map
in
- let state = References.fold update_ref references state in
+ let base_map = References.fold update_ref references base_map 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 base_map =
+ if Option.is_none incr then
+ BaseMap.replace
+ (Option.map (fun (memory, _refs) -> memory, References.empty))
+ (Base.of_varinfo vi)
+ base_map
+ else
+ base_map
+ in
+ base_map, tracked
let update_array_segmentation lval expr state =
match lval with
@@ -708,11 +739,12 @@ struct
(fun state vi -> update_array_segmentation_bounds vi None state)
state vars
in
- remove_vars state vars
+ let (base_map,tracked) = state in
+ BaseMap.remove_vars base_map vars, tracked
- let logic_assign assign location state =
+ let logic_assign assign location (base_map,tracked as state) =
match assign with
- | None -> remove state location
+ | None -> BaseMap.remove_loc base_map location, tracked
| Some ((Frees _ | Allocates _), _) -> state
| Some (Assigns (_dest, sources), _pre_state) ->
match sources with
@@ -720,7 +752,7 @@ struct
let dst = Location.of_precise_loc location in
erase state dst Abstract_memory.Bit.numerical
| _ ->
- remove state location
+ BaseMap.remove_loc base_map location, tracked
let reduce_by_papp env li _labels args positive state =
try
@@ -750,7 +782,8 @@ struct
reduce predicate truth state
let interpret_acsl_extension extension _env state =
- if extension.ext_name = "array_partition" then
+ match extension.ext_name with
+ | "array_partition" ->
let annotation = Eva_annotations.read_array_segmentation extension in
let vi,offset,bounds = annotation in
(* Update the segmentation *)
@@ -768,7 +801,16 @@ struct
in
let references = List.fold_left add [] bounds in
add_references_l state references (Location.bases loc)
- else
+ | "eva_domain_scope" ->
+ let domain,vars = Eva_annotations.read_domain_scope extension in
+ if domain = "multidim" then
+ let (base_map,tracked) = state in
+ let set = Option.value ~default:TrackedBases.empty tracked
+ and bases = List.map Base.of_varinfo vars in
+ base_map, Some (List.fold_right TrackedBases.add bases set)
+ else
+ state
+ | _ ->
state
let empty () = top
@@ -788,18 +830,22 @@ struct
let relate _kf _bases _state = Base.SetLattice.empty
- let filter _kf _kind bases state =
- DomainLattice.filter (fun elt -> Base.Hptset.mem elt bases) state
+ let filter _kf _kind bases (base_map,tracked) =
+ BaseMap.filter (fun elt -> Base.Hptset.mem elt bases) base_map,
+ tracked (* TODO: intersection with bases *)
- let reuse _kf bases ~current_input ~previous_output =
+ let reuse _kf bases =
+ let open BaseMap in
let cache = Hptmap_sig.NoCache in
let decide_both _key _v1 v2 = Some v2 in
let decide_left key v1 =
if Base.Hptset.mem key bases then None else Some v1
in
- merge ~cache ~symmetric:false ~idempotent:true
- ~decide_both ~decide_left:(Traversing decide_left) ~decide_right:Neutral
- current_input previous_output
+ let reuse = merge ~cache ~symmetric:false ~idempotent:true
+ ~decide_both ~decide_left:(Traversing decide_left) ~decide_right:Neutral
+ in
+ fun ~current_input:(m1,t1) ~previous_output:(m2,t2) ->
+ reuse m1 m2, join_tracked t1 t2
end
include Domain
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index 2c0ab30aefb..9080f611f27 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -396,6 +396,54 @@ module ArraySegmentation = Register (struct
type array_segmentation = ArraySegmentation.t
-let get_array_segmentation = ArraySegmentation.get
let add_array_segmentation = ArraySegmentation.add
let read_array_segmentation ext = ArraySegmentation.import ext.ext_kind
+
+
+module DomainScope = Register (struct
+ type t = string * Cil_types.varinfo list
+ let name = "eva_domain_scope"
+ let is_loop_annot = false
+
+ let parse ~typing_context:context =
+ let parse_domain = function
+ | {lexpr_node = PLvar v} -> v
+ | _ -> raise Parse_error
+ and parse_var = function
+ | {lexpr_node = PLvar v} ->
+ begin match context.Logic_typing.find_var v with
+ | {lv_origin=Some vi} -> vi
+ | _ -> raise Parse_error
+ end
+ | _ -> raise Parse_error
+ in
+ function
+ | domain :: vars ->
+ parse_domain domain, List.map parse_var vars
+ | _ -> raise Parse_error
+
+ let import = function
+ | Ext_terms ({term_node=TConst (LStr domain)} :: vars) ->
+ let import_var = function
+ | {term_node=TLval (TVar {lv_origin=Some vi}, TNoOffset)} -> vi
+ | _ -> assert false
+ in
+ domain, List.map import_var vars
+ | _ -> assert false
+
+ let export (domain, vars) =
+ let export_var vi =
+ Logic_const.tvar (Cil.cvar_to_lvar vi)
+ in
+ Ext_terms (Logic_const.tstring domain :: List.map export_var vars)
+
+ let print fmt (domain, vars) =
+ Format.fprintf fmt "%s, %a"
+ domain
+ (Pretty_utils.pp_list ~sep:",@ " Cil_printer.pp_varinfo) vars
+ end)
+
+
+type domain_scope = DomainScope.t
+let add_domain_scope = DomainScope.add
+let read_domain_scope ext = DomainScope.import ext.ext_kind
diff --git a/src/plugins/value/utils/eva_annotations.mli b/src/plugins/value/utils/eva_annotations.mli
index 98d914d689a..f5c46349d56 100644
--- a/src/plugins/value/utils/eva_annotations.mli
+++ b/src/plugins/value/utils/eva_annotations.mli
@@ -62,12 +62,15 @@ type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
type array_segmentation =
Cil_types.varinfo * Cil_types.offset * Cil_types.exp list
+type domain_scope =
+ string (* domain *) *
+ Cil_types.varinfo list (* variables that must be tracked by the domain *)
+
val get_slevel_annot : Cil_types.stmt -> slevel_annotation option
val get_unroll_annot : Cil_types.stmt -> unroll_annotation list
val get_flow_annot : Cil_types.stmt -> flow_annotation list
val get_subdivision_annot : Cil_types.stmt -> int list
val get_allocation: Cil_types.stmt -> allocation_kind
-val get_array_segmentation : Cil_types.stmt -> array_segmentation list
val add_slevel_annot : emitter:Emitter.t ->
Cil_types.stmt -> slevel_annotation -> unit
@@ -79,6 +82,9 @@ val add_subdivision_annot : emitter:Emitter.t ->
Cil_types.stmt -> int -> unit
val add_array_segmentation : emitter:Emitter.t ->
Cil_types.stmt -> array_segmentation -> unit
+val add_domain_scope : emitter:Emitter.t ->
+ Cil_types.stmt -> domain_scope -> unit
[@@@ api_end]
val read_array_segmentation : Cil_types.acsl_extension -> array_segmentation
+val read_domain_scope : Cil_types.acsl_extension -> domain_scope
--
GitLab