From 1ce73b95e1e2787e9031879922ba1480219113c9 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 1 Dec 2021 16:36:15 +0100
Subject: [PATCH] [Eva] multidim: add annotation to hint the apropriate
segmentation
---
.../abstract_interp/abstract_memory.ml | 31 +++++++++++-
.../abstract_interp/abstract_memory.mli | 5 ++
src/plugins/value/domains/multidim_domain.ml | 47 ++++++++++++++----
src/plugins/value/utils/eva_annotations.ml | 48 +++++++++++++++++++
src/plugins/value/utils/eva_annotations.mli | 8 ++++
5 files changed, 130 insertions(+), 9 deletions(-)
diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml
index ea1ff820b2e..2f3e1be7fa3 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.ml
+++ b/src/kernel_services/abstract_interp/abstract_memory.ml
@@ -211,6 +211,7 @@ sig
weak:bool -> Abstract_offset.typed_offset -> t -> t
val incr_bound : oracle:oracle -> Cil_types.varinfo -> Integer.t option ->
t -> t
+ val add_segmentation_bounds : oracle:oracle -> Cil_types.exp list -> t -> t
end
@@ -661,6 +662,7 @@ sig
val incr_bound :
oracle:oracle -> Bound.Var.t -> Integer.t option -> t -> t
val map : (submemory -> submemory) -> t -> t
+ val add_segmentation_bounds : oracle:oracle -> bound list -> t -> t
end
module Segmentation (Config : Config) (M : ProtoMemory) =
@@ -925,6 +927,7 @@ struct
let write ~oracle f m lindex (* included *) uindex (* excluded *) = (* lindex < uindex *)
let open (val (B.operators oracle)) in
let age = Integer.succ m.age in
+ let same_bounds = lindex == uindex in
let lindex = lindex, age and uindex = uindex, age in
(* (start,head) : segmentation kept identical below the write indexes,
head is a list in reverse order
@@ -967,7 +970,7 @@ struct
and next_is_empty = is_empty_segment ~oracle uindex u in
let tail' =
(if previous_is_empty then [] else [(v,lindex)]) @
- [(f v,uindex)] @
+ (if same_bounds then [] else [(f v,uindex)]) @
(if next_is_empty then [] else [(v,u)]) @
tail
and head',start' = match head with (* change last bound to match lindex *)
@@ -1014,6 +1017,12 @@ struct
let map f m =
{ m with segments = check_segments (List.map (fun (v,u) -> f v, u) m.segments) }
+
+ let add_segmentation_bounds ~oracle bounds m =
+ let add_bound m b =
+ write ~oracle (fun _ -> assert false) m b b
+ in
+ List.fold_left add_bound m bounds
end
@@ -1355,6 +1364,20 @@ struct
let array_value = A.incr_bound ~oracle vi x a.array_value in
Array { a with array_value=A.map aux array_value }
in aux
+
+ let add_segmentation_bounds ~oracle bounds = function
+ | Array a ->
+ let convert_bound exp =
+ try
+ Some (Bound.of_exp exp)
+ with Bound.UnsupportedBoundExpression -> None
+ in
+ let bounds = List.filter_map convert_bound bounds in
+ Array {
+ a with
+ array_value = A.add_segmentation_bounds ~oracle bounds a.array_value
+ }
+ | m -> m (* Ignore segmentation hints on non-array *)
end
and S : Structures with type submemory = ProtoMemory.t =
Structures (Config) (ProtoMemory)
@@ -1425,4 +1448,10 @@ struct
src
in
write ~oracle ~weak f offset dst
+
+ let segmentation_hint ~oracle m offset bounds =
+ let f ~weak:_ _typ m =
+ add_segmentation_bounds ~oracle bounds m
+ in
+ write ~oracle ~weak:false f offset m
end
diff --git a/src/kernel_services/abstract_interp/abstract_memory.mli b/src/kernel_services/abstract_interp/abstract_memory.mli
index 229dfee4bb7..32ac5f50cb6 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.mli
+++ b/src/kernel_services/abstract_interp/abstract_memory.mli
@@ -123,4 +123,9 @@ sig
(* Pretty prints memory *)
val pretty : Format.formatter -> t -> unit
+
+ (* Update the array segmentation at the given offset so the given bound
+ expressions appear in the segmentation *)
+ val segmentation_hint : oracle:oracle ->
+ t -> location -> Cil_types.exp list -> t
end
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index 2908b421633..82ae326f38f 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -246,6 +246,12 @@ struct
| `Top -> Memory.top
| `Value loc ->
Memory.overwrite ~oracle ~weak dst loc src
+
+ let segmentation_hint ~oracle m loc bounds =
+ match loc with
+ | `Top -> Memory.top
+ | `Value loc ->
+ Memory.segmentation_hint ~oracle m loc bounds
end
(* References to variables inside array segmentation.
@@ -335,7 +341,6 @@ struct
| Lval lval ->
let value = get state (Location.of_lval oracle lval) in
Bottom.non_bottom value (* TODO: handle exception *)
- | Info (e, _) -> oracle e
| Const (CInt64 (i,_,_)) -> Value.inject_int i
| UnOp (op, e, typ) -> Value.forward_unop typ op (oracle e)
| BinOp (op, e1, e2, TFloat (fkind, _)) ->
@@ -348,7 +353,7 @@ struct
and dst_type = scalar_type typ in
Value.forward_cast ~src_type ~dst_type (oracle e)
| _ ->
- Value_parameters.fatal
+ Self.fatal
"This type of array index expression is not supported: %a"
Cil_printer.pp_exp exp
in
@@ -365,22 +370,26 @@ struct
let oracle = mk_oracle state in
read (Memory.extract ~oracle) (Memory.smash ~oracle) state src
+ let add_references state vi refs' =
+ let base = Base.of_varinfo vi in
+ let memory, refs = find_or_top state base in
+ let refs'' = References.union refs (References.of_list refs') in
+ add base (memory, refs'') state
+
+ let add_references_l state l refs =
+ List.fold_left (fun state vi -> add_references state vi refs) state l
+
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
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
let state = Location.fold f loc state in
- List.fold_left add_ref state (Location.references loc)
+ add_references_l state (Location.references loc) (Location.bases loc)
let set (state : state) (dst : mdlocation) (v : value) : state =
let weak = not (Location.is_singleton dst)
@@ -673,6 +682,28 @@ struct
in
reduce predicate truth state
+ let interpret_acsl_extension extension _env state =
+ if extension.ext_name = "array_partition" then
+ let annotation = Eva_annotations.read_array_segmentation extension in
+ let vi,offset,bounds = annotation in
+ (* Update the segmentation *)
+ let lval = Cil_types.Var vi, offset in
+ let loc = Location.of_lval (mk_oracle' state) lval in
+ let oracle = mk_oracle state in
+ let update m offset =
+ Memory.segmentation_hint ~oracle m offset bounds
+ in
+ let state = write update state loc in
+ (* Update the references *)
+ let add acc e =
+ let r = Cil.extract_varinfos_from_exp e in
+ (Cil_datatype.Varinfo.Set.to_seq r |> List.of_seq) @ acc
+ in
+ let references = List.fold_left add [] bounds in
+ add_references_l state references (Location.bases loc)
+ else
+ state
+
let empty () = top
let initialize_variable lval _loc ~initialized:_ init_value state =
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index fd9feb85a1e..2c0ab30aefb 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -351,3 +351,51 @@ module Allocation = struct
end
let get_allocation = Allocation.get
+
+
+module ArraySegmentation = Register (struct
+ module Interp = Db.Properties.Interp
+
+ type t = Cil_types.varinfo * Cil_types.offset * Cil_types.exp list
+ let name = "array_partition"
+ let is_loop_annot = false
+
+ let convert = function
+ | {term_node = TLval (TVar {lv_origin=Some vi}, toffset)} :: tbounds ->
+ begin try
+ let offset = !Interp.term_offset_to_offset ~result:None toffset
+ and bounds = List.map (!Interp.term_to_exp ~result:None) tbounds in
+ Some (vi, offset, bounds)
+ with
+ Interp.No_conversion -> None
+ end
+ | _ -> None
+
+ let parse ~typing_context:context lexprs =
+ let open Logic_typing in
+ let l = List.map (context.type_term context context.pre_state) lexprs in
+ Extlib.the ~exn:Parse_error (convert l)
+
+ let import = function
+ | Ext_terms l -> Option.get (convert l)
+ | _ -> assert false
+
+ let export (vi, offset, bounds) =
+ let lv = Cil.cvar_to_lvar vi
+ and toffset = Logic_utils.offset_to_term_offset offset
+ and tbounds = List.map Logic_utils.expr_to_term bounds in
+ let tlval = TVar lv, toffset in
+ let tarray = Logic_const.term (TLval tlval) (Cil.typeOfTermLval tlval) in
+ Ext_terms (tarray :: tbounds)
+
+ let print fmt (vi,offset,bounds) =
+ Format.fprintf fmt "%a, %a"
+ Cil_printer.pp_lval (Var vi, offset)
+ (Pretty_utils.pp_list ~sep:",@ " Cil_printer.pp_exp) bounds
+ end)
+
+
+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
diff --git a/src/plugins/value/utils/eva_annotations.mli b/src/plugins/value/utils/eva_annotations.mli
index 4aaa3084dee..98d914d689a 100644
--- a/src/plugins/value/utils/eva_annotations.mli
+++ b/src/plugins/value/utils/eva_annotations.mli
@@ -59,11 +59,15 @@ type flow_annotation =
type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
+type array_segmentation =
+ Cil_types.varinfo * Cil_types.offset * Cil_types.exp list
+
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
@@ -73,4 +77,8 @@ val add_flow_annot : emitter:Emitter.t ->
Cil_types.stmt -> flow_annotation -> unit
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
[@@@ api_end]
+
+val read_array_segmentation : Cil_types.acsl_extension -> array_segmentation
--
GitLab