[Eva] multidim: add annotation to hint the apropriate segmentation

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

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

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 =

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

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