From df1b4a4100db4436377f71a6f6e43222884a0ff3 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Sun, 31 Oct 2021 19:17:21 +0100
Subject: [PATCH] [Eva] multidim: implements array segmentation
---
.../abstract_interp/abstract_memory.ml | 1454 +++++++++++------
.../abstract_interp/abstract_memory.mli | 39 +-
.../abstract_interp/abstract_offset.ml | 40 +-
.../abstract_interp/abstract_offset.mli | 2 +-
src/libraries/stdlib/transitioning.ml.in | 9 +
src/libraries/stdlib/transitioning.mli | 3 +
src/plugins/value/domains/multidim_domain.ml | 223 ++-
tests/value/oracle/multidim.res.oracle | 24 +-
8 files changed, 1197 insertions(+), 597 deletions(-)
diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml
index 15059153744..687d64d5f8f 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.ml
+++ b/src/kernel_services/abstract_interp/abstract_memory.ml
@@ -24,10 +24,53 @@
emits a warning *)
[@@@warning "-60"]
+exception Not_implemented
+
open Abstract_offset
type size = Integer.t
+(* Composition operator for compare function *)
+
+let (<?>) c (cmp,x,y) =
+ if c = 0 then cmp x y else c
+
+(* Pretty printing for iterators - inspired by Pretty_utils.pp_iter *)
+
+let pp_iter
+ ?(pre=format_of_string "{@;<1 2>")
+ ?(sep=format_of_string ",@;<1 2>")
+ ?(suf=format_of_string "@ }")
+ ?(format=format_of_string"@[<hv>%a@]")
+ iter pp fmt v =
+ let need_sep = ref false in
+ Format.fprintf fmt pre;
+ iter (fun v ->
+ if !need_sep then Format.fprintf fmt sep else need_sep := true;
+ Format.fprintf fmt format pp v;
+ ) v;
+ Format.fprintf fmt suf;
+;;
+
+let pp_iter2 ?pre ?sep ?suf ?(format=format_of_string "%a%a")
+ iter2 pp_key pp_val fmt v =
+ let iter f = iter2 (fun k v -> f (k,v)) in
+ let pp fmt (k,v) = Format.fprintf fmt format pp_key k pp_val v in
+ pp_iter ?pre ?sep ?suf ~format:"%a" iter pp fmt v
+
+(* Types compatibility *)
+
+let typ_size t =
+ Integer.of_int (Cil.bitsSizeOf t)
+
+let are_typ_compatible t1 t2 =
+ Integer.equal (typ_size t1) (typ_size t2)
+
+
+(* ------------------------------------------------------------------------ *)
+(* --- Imprecise bits abstraction --- *)
+(* ------------------------------------------------------------------------ *)
+
type bit =
| Uninitialized
| Zero
@@ -44,6 +87,8 @@ struct
let numerical = Any Bases.empty
let top = Any Bases.top
+ let is_any = function Any _ -> true | _ -> false
+
let hash = function
| Uninitialized -> 7
| Zero -> 3
@@ -81,6 +126,11 @@ struct
| Any set1, Any set2 -> Any (Bases.join set1 set2)
end
+
+(* ------------------------------------------------------------------------ *)
+(* --- Inputs parameters for Memory abstraction --- *)
+(* ------------------------------------------------------------------------ *)
+
module type Value =
sig
type t
@@ -95,7 +145,7 @@ sig
val of_bit : bit -> t
val to_bit : t -> bit
val is_included : t -> t -> bool
- val join: t -> t -> t
+ val join : t -> t -> t
end
module type Config =
@@ -103,165 +153,798 @@ sig
val deps : State.t list
end
-module type T =
+
+(* ------------------------------------------------------------------------ *)
+(* --- Proto memory abstraction --- *)
+(* ------------------------------------------------------------------------ *)
+
+type side = Left | Right
+type oracle = Cil_types.exp -> Ival.t
+type bioracle = side -> oracle
+type strength = Strong | Weak | Reinforce (* update strength *)
+
+module type ProtoMemory =
sig
- type location
- type value
type t
+ type value
+ val pretty : Format.formatter -> t -> unit
+ val pretty_root : Format.formatter -> t -> unit
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
- val top : t
- val zero : t
- val is_top : t -> bool
- val get : t -> location -> value
- val extract :t -> location -> t
- val erase : weak:bool -> t -> location -> bit -> t
- val set : weak:bool -> t -> location -> value -> t
- val overwrite : weak:bool -> t -> location -> t -> t
- val reinforce : (value -> value) -> t -> location -> t
+ val of_raw : bit -> t
+ val raw : t -> bit
+ val of_value : Cil_types.typ -> value -> t
+ val to_value : Cil_types.typ -> t -> value
+ val weak_erase : bit -> t -> t
val is_included : t -> t -> bool
- val join : t -> t -> t
- val widen : (size:size -> value -> value -> value) -> t -> t -> t
- val pretty : Format.formatter -> t -> unit
+ val unify : oracle:bioracle ->
+ (size:size -> value -> value -> value) -> t -> t -> t
+ val join : oracle:bioracle -> t -> t -> t
+ val smash : oracle:oracle -> t -> t -> t
+ val read : oracle:oracle -> (Cil_types.typ -> t -> 'a) -> ('a -> 'a -> 'a) ->
+ Abstract_offset.typed_offset -> t -> 'a
+ val write : oracle:oracle -> (weak:bool -> Cil_types.typ -> t -> t) ->
+ weak:bool -> Abstract_offset.typed_offset -> t -> t
+ val incr_bound : oracle:oracle -> Cil_types.varinfo -> Integer.t option ->
+ t -> t
end
-module Make (Config : Config) (Value : Value) =
+(* ------------------------------------------------------------------------ *)
+(* --- C struct abstraction --- *)
+(* ------------------------------------------------------------------------ *)
+
+module type Structures =
+sig
+ type t
+ type submemory
+ val pretty : Format.formatter -> t -> unit
+ val hash : t -> int
+ val equal : t -> t -> bool
+ val compare : t -> t -> int
+ val raw : t -> Bit.t
+ val of_raw : Bit.t -> t
+ val weak_erase : Bit.t -> t -> t
+ val is_included : t -> t -> bool
+ val unify : (submemory -> submemory -> submemory) -> t -> t -> t
+ val read : t -> Cil_types.fieldinfo -> submemory
+ val write : t -> Cil_types.fieldinfo -> (submemory -> submemory) -> t
+ val map : (submemory -> submemory) -> t -> t
+end
+
+module Structures (Config : Config) (M : ProtoMemory) =
struct
- type location = Abstract_offset.typed_offset
- type value = Value.t
-
- type 'fieldmap memory =
- | Raw of bit
- | Scalar of memory_scalar
- | Struct of 'fieldmap memory_struct
- | Union of 'fieldmap memory_union
- | Array of 'fieldmap memory_array
- and memory_scalar = {
- scalar_value: Value.t;
- scalar_type: Cil_types.typ;
- }
- and 'fieldmap memory_struct = {
- struct_value: 'fieldmap;
- struct_info: Cil_types.compinfo;
- struct_padding: bit; (* for missing fields and padding *)
- }
- (* unions are handled separately from struct to avoid confusion and error *)
- and 'fieldmap memory_union = {
- union_value: 'fieldmap memory;
- union_field: Cil_types.fieldinfo;
- union_padding: bit;
+ module Field =
+ struct
+ include Cil_datatype.Fieldinfo
+ let id f = f.Cil_types.forder (* At each node, all fields come from the same comp *)
+ end
+ module Values =
+ struct
+ include Datatype.Make (
+ struct
+ include Datatype.Serializable_undefined
+ include M
+ let name = "Abstract_Memort.Structures.Values"
+ let reprs = [ of_raw Zero ]
+ end)
+ let pretty_debug = pretty
+ end
+ module Initial_Values = struct let v = [[]] end
+ module Deps = struct let l = Config.deps end
+
+ module FieldMap =
+ Hptmap.Make (Field) (Values) (Hptmap.Comp_unused) (Initial_Values) (Deps)
+
+ type t = {
+ padding: Bit.t;
+ fields: FieldMap.t;
}
- and 'fieldmap memory_array = {
- array_value: 'fieldmap memory;
- array_cell_type: Cil_types.typ;
- array_range: Int_val.t; (* range of known cells *)
- array_padding: bit; (* unknown cells outside the previous range *)
+
+ type submemory = M.t
+
+ let pretty fmt m =
+ pp_iter2 ~format:".%a%a" FieldMap.iter Field.pretty M.pretty fmt m.fields
+
+ let hash m =
+ Hashtbl.hash (m.padding, FieldMap.hash m.fields)
+
+ let equal m1 m2 =
+ FieldMap.equal m1.fields m2.fields &&
+ Bit.equal m1.padding m2.padding
+
+ let compare m1 m2 =
+ FieldMap.compare m1.fields m2.fields <?>
+ (Bit.compare, m1.padding, m2.padding)
+
+ let raw m =
+ FieldMap.fold (fun _ x acc -> Bit.join acc (M.raw x)) m.fields m.padding
+
+ let of_raw m =
+ { padding = m ; fields = FieldMap.empty }
+
+ let weak_erase b m =
+ {
+ padding = Bit.join b m.padding ;
+ fields = FieldMap.map (M.weak_erase b) m.fields ;
+ }
+
+ let is_included m1 m2 =
+ Bit.is_included m1.padding m2.padding &&
+ let decide_fast s t = if s == t then FieldMap.PTrue else PUnknown in
+ let decide_fst _fi m1 = M.is_included m1 (M.of_raw m2.padding) in
+ let decide_snd _fi m2 = M.is_included (M.of_raw m1.padding) m2 in
+ let decide_both _fi m1 m2 = M.is_included m1 m2 in
+ FieldMap.binary_predicate Hptmap_sig.NoCache UniversalPredicate
+ ~decide_fast ~decide_fst ~decide_snd ~decide_both
+ m1.fields m2.fields
+
+ let unify f m1 m2 =
+ let decide b =
+ FieldMap.Traversing (fun _fi m -> Some (f (M.of_raw b) m))
+ in
+ let decide_both _fi = fun m1 m2 -> Some (f m1 m2)
+ and decide_left = decide m2.padding
+ and decide_right = decide m1.padding
+ in
+ let fields = FieldMap.merge
+ ~cache:Hptmap_sig.NoCache ~symmetric:false ~idempotent:true
+ ~decide_both ~decide_left ~decide_right
+ m1.fields m2.fields
+ in { padding = Bit.join m1.padding m2.padding ; fields }
+
+ let read m fi =
+ try
+ FieldMap.find fi m.fields
+ with Not_found -> (* field undefined *)
+ M.of_raw m.padding
+
+ let write m fi f =
+ let write' opt =
+ Some (f (Option.value ~default:(M.of_raw m.padding) opt))
+ in
+ { m with fields = FieldMap.replace write' fi m.fields }
+
+ let map f m =
+ { m with fields = FieldMap.map f m.fields }
+end
+
+
+(* ------------------------------------------------------------------------ *)
+(* --- Arrays abstraction --- *)
+(* ------------------------------------------------------------------------ *)
+
+type comparison = Equal | Lower | Greater | Uncomparable
+
+module Bound =
+struct
+ module Var = Cil_datatype.Varinfo
+ module Exp = Cil_datatype.ExpStructEq
+
+ type t =
+ | Const of Integer.t
+ | Exp of Cil_types.exp * Integer.t (* x + c *)
+ | Ptroffset of Cil_types.exp * Cil_types.offset * Integer.t (* (x - &b.offset) + c *)
+
+ let pretty fmt : t -> unit = function
+ | Const i -> Integer.pretty fmt i
+ | Exp (e,i) when Integer.is_zero i -> Exp.pretty fmt e
+ | Exp (e,i) ->
+ Format.fprintf fmt "%a + %a" Exp.pretty e Integer.pretty i
+ | _ -> raise Not_implemented
+
+ let hash : t -> int = function
+ | Const i -> Hashtbl.hash (1, Integer.hash i)
+ | Exp (e, i) -> Hashtbl.hash (2, Exp.hash e, Integer.hash i)
+ | Ptroffset _ -> raise Not_implemented
+
+ let compare (b1 : t) (b2 : t) : int =
+ match b1, b2 with
+ | Const i1, Const i2 -> Integer.compare i1 i2
+ | Exp (e1, i1), Exp (e2, i2) ->
+ Exp.compare e1 e2 <?> (Integer.compare, i1, i2)
+ | Ptroffset _, Ptroffset _ -> raise Not_implemented
+ | Const _, _ -> 1
+ | _, Const _-> -1
+ | Exp _, _ -> 1
+ | _, Exp _ -> -1
+
+ let equal (b1 : t) (b2 : t) : bool =
+ match b1, b2 with
+ | Const i1, Const i2 -> Integer.equal i1 i2
+ | Exp (e1, i1), Exp (e2, i2) ->
+ Exp.equal e1 e2 && Integer.equal i1 i2
+ | Ptroffset _, Ptroffset _ -> raise Not_implemented
+ | _, _ -> false
+
+ let of_integer (i : Integer.t) : t =
+ Const i
+
+ let succ = function
+ | Const i -> Const (Integer.succ i)
+ | Exp (e, i) -> Exp (e, Integer.succ i)
+ | Ptroffset _ -> raise Not_implemented
+
+ let pred = function
+ | Const i -> Const (Integer.pred i)
+ | Exp (e, i) -> Exp (e, Integer.pred i)
+ | Ptroffset _ -> raise Not_implemented
+
+ exception UnsupportedBoundExpression
+ exception NonLinear
+
+ (* Find a coefficient before vi in exp *)
+ let rec linearity vi exp =
+ match exp.Cil_types.enode with
+ | Const _
+ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
+ | AddrOf _ | StartOf _ -> Integer.zero
+ | Lval (Var vi', NoOffset) ->
+ if Var.equal vi' vi
+ then Integer.one
+ else Integer.zero
+ | Lval _ -> raise UnsupportedBoundExpression
+ | UnOp (Neg, e, _typ) ->
+ Integer.neg (linearity vi e)
+ | UnOp (_, e, _typ) | CastE (_typ, e) ->
+ if Integer.is_zero (linearity vi e)
+ then Integer.zero
+ else raise NonLinear
+ | BinOp (op, e1, e2, _typ) ->
+ let l1 = linearity vi e1 and l2 = linearity vi e2 in
+ match op with
+ | PlusA|PlusPI -> Integer.add l1 l2
+ | MinusA|MinusPI -> Integer.sub l1 l2
+ | _ ->
+ if Integer.(is_zero l1 && is_zero l2)
+ then Integer.zero
+ else raise NonLinear
+
+ let check_support exp =
+ (* Check that the linearity of any variable is not hidden into a mem access *)
+ ignore (linearity Var.dummy exp)
+
+ let of_exp exp =
+ check_support exp;
+ (* Normalizes x + c, c + x and x - c *)
+ match Cil.constFoldToInt exp with
+ | Some i -> Const i
+ | None ->
+ match exp.Cil_types.enode with
+ | BinOp ((PlusA|PlusPI), e1, e2, _typ) ->
+ begin match Cil.constFoldToInt e1, Cil.constFoldToInt e2 with
+ | None, Some i -> Exp (e1, i)
+ | Some i, None -> Exp (e2, i)
+ | _ -> Exp (exp, Integer.zero)
+ end
+ | BinOp ((MinusA|MinusPI), e1, e2, _typ) ->
+ begin match Cil.constFoldToInt e2 with
+ | Some i -> Exp (e1, Integer.neg i)
+ | None -> Exp (exp, Integer.zero)
+ end
+ | _ -> Exp (exp, Integer.zero)
+
+ let _of_ptr ~base_offset e =
+ (* TODO: verify type compatibility between e and base_offset *)
+ match of_exp e with
+ | Exp (e, c) -> Ptroffset (e, base_offset, c)
+ | Const _ -> assert false (* should not happen ? even with absolute adresses ? *)
+ | Ptroffset _ -> assert false (* Not produced by of_exp *)
+
+ let incr vi i b =
+ try
+ match b with
+ | Const _ -> Some b
+ | Exp (e, j) ->
+ let l = linearity vi e in
+ Some (Exp (e, Integer.(sub j (mul l i))))
+ | Ptroffset (e, b, j) ->
+ let l = linearity vi e in
+ Some (Ptroffset (e, b, Integer.(sub j (mul l i))))
+ with NonLinear -> None
+
+ (* Stupid oracle built from an Ival oracle *)
+ let to_ival ~oracle = function
+ | Const i -> Ival.inject_singleton i
+ | Exp (e, i) -> Ival.add_singleton_int i (oracle e)
+ | Ptroffset _ -> raise Not_implemented
+
+ let cmp ~oracle b1 b2 =
+ if b1 == b2
+ then Equal
+ else
+ match b1, b2 with
+ | Const i1, Const i2 ->
+ let r = Integer.sub i1 i2 in
+ if Integer.is_zero r
+ then Equal
+ else if Integer.(lt r zero) then Lower else Greater
+ | _, _ ->
+ let r = Ival.sub_int (to_ival ~oracle b1) (to_ival ~oracle b2) in
+ match Ival.min_and_max r with
+ | Some min, Some max when Integer.is_zero min && Integer.is_zero max ->
+ Equal
+ | Some l, _ when Integer.(gt l zero) -> Greater
+ | _, Some u when Integer.(lt u zero) -> Lower
+ | _ -> Uncomparable
+
+ let lower_bound ~oracle b1 b2 =
+ let i1 = to_ival ~oracle:(oracle Left) b1
+ and i2 = to_ival ~oracle:(oracle Right) b2 in
+ let l1 = Option.get (Ival.min_int i1) (* TODO: handle Nones *)
+ and l2 = Option.get (Ival.min_int i2) in
+ Const (Integer.min l1 l2)
+
+ let upper_bound ~oracle b1 b2 =
+ let i1 = to_ival ~oracle:(oracle Left) b1
+ and i2 = to_ival ~oracle:(oracle Right) b2 in
+ let u1 = Option.get (Ival.max_int i1) (* TODO: handle Nones *)
+ and u2 = Option.get (Ival.max_int i2) in
+ Const (Integer.max u1 u2)
+
+ let upper_const ~oracle b =
+ Const (Option.get (Ival.min_int (to_ival ~oracle b))) (* TODO: handle exception *)
+
+ let lower_const ~oracle b =
+ Const (Option.get (Ival.min_int (to_ival ~oracle b))) (* TODO: handle exception *)
+end
+
+module type Segmentation =
+sig
+ type bound = Bound.t
+ type submemory
+ type t
+ val pretty : Format.formatter -> t -> unit
+ val hash : t -> int
+ val equal : t -> t -> bool
+ val compare : t -> t -> int
+ val raw : t -> Bit.t
+ val weak_erase : Bit.t -> t -> t
+ val is_included : t -> t -> bool
+ val unify : oracle:bioracle -> (submemory -> submemory -> submemory) ->
+ t -> t -> t
+ val singleton : bit -> bound -> bound -> submemory -> t
+ val read :
+ oracle:(Cil_types.exp -> Ival.t) ->
+ (submemory -> 'a) -> ('a -> 'a -> 'a) -> t -> bound -> 'a
+ val write : oracle:oracle -> (submemory -> submemory) ->
+ t -> bound -> bound -> t
+ val incr_bound :
+ oracle:oracle -> Bound.Var.t -> Integer.t option -> t -> t
+ val map : (submemory -> submemory) -> t -> t
+end
+
+module Segmentation (Config : Config) (M : ProtoMemory) =
+struct
+ type bound = Bound.t
+ type submemory = M.t
+
+ type t = {
+ start: bound;
+ segments: (M.t * bound) list; (* should not be empty *)
+ padding: bit (* padding at the left and right of the segmentation *)
}
- (* Datatype prototype *)
-
- module Prototype (
- FieldMap :
- sig
- type 'a map
- type v = t memory
- and t = v map
- include Hptmap_sig.S
- with type 'a map := 'a map
- and type key = Cil_types.fieldinfo
- and type v := v
- and type t := v map
- end) =
- struct
- type t = FieldMap.t memory
+ let _pretty_debug fmt (l,s) : unit =
+ Format.fprintf fmt " {%a} " Bound.pretty l;
+ let pp fmt (v,u) =
+ Format.fprintf fmt "%a {%a} " M.pretty v Bound.pretty u
+ in
+ List.iter (pp fmt) s
+
+ let pretty_segments fmt (l,s) : unit =
+ let pp fmt (l,v,u) =
+ let u = Bound.pred u in (* Upper bound is not included *)
+ if Bound.(equal l u) then
+ Format.fprintf fmt "[%a]%a" Bound.pretty l M.pretty v
+ else
+ Format.fprintf fmt "[%a..%a]%a" Bound.pretty l Bound.pretty u M.pretty v
+ in
+ match s with
+ | [] -> Format.fprintf fmt "[]" (* should not happen *)
+ | [(v,u)] -> pp fmt (l,v,u)
+ | _ :: _ ->
+ let iter l f segments =
+ (* fold the previous upper bound = the current lower bound *)
+ ignore (List.fold_left (fun l (v,u) -> f (l,v,u) ; u) l segments)
+ in
+ pp_iter (iter l) pp fmt s
+
+ let pretty fmt (m : t) : unit =
+ pretty_segments fmt (m.start,m.segments)
+
+ let hash (m : t) : int =
+ Hashtbl.hash (
+ Bound.hash m.start,
+ List.map (fun (v,u) -> Hashtbl.hash (M.hash v, Bound.hash u)) m.segments,
+ Bit.hash m.padding)
- let rec pretty fmt : t -> 'a =
- let rec leading_indexes acc = function
- | Array a -> leading_indexes (a.array_range :: acc) a.array_value
- | (Raw _ | Scalar _ | Struct _ | Union _) as m -> List.rev acc, m
+ let compare (m1 : t) (m2 : t) : int =
+ let compare_segments (v1,u1) (v2,u2) =
+ M.compare v1 v2 <?> (Bound.compare, u1, u2)
+ in
+ Bound.compare m1.start m2.start <?>
+ (Transitioning.List.compare compare_segments, m1.segments, m2.segments) <?>
+ (Bit.compare, m1.padding, m2.padding)
+
+ let equal (m1 : t) (m2 : t) : bool =
+ let equal_segments (v1,u1) (v2,u2) =
+ M.equal v1 v2 && Bound.equal u1 u2
+ in
+ Bound.equal m1.start m2.start &&
+ Transitioning.List.equal equal_segments m1.segments m2.segments &&
+ Bit.equal m1.padding m2.padding
+
+ let raw (m : t) : bit =
+ (* Perhaps some segments are empty, but we are not going to test it for now *)
+ List.fold_left
+ (fun acc (v,_u) -> Bit.join acc (M.raw v))
+ m.padding m.segments
+
+ let weak_erase (b : bit) (m : t) : t =
+ {
+ m with
+ segments = List.map (fun (v,u) -> M.weak_erase b v, u) m.segments ;
+ padding = Bit.join b m.padding ;
+ }
+
+ let is_included (m1 : t) (m2 : t) : bool =
+ let included_segments (v1,u1) (v2,u2) =
+ M.is_included v1 v2 &&
+ Bound.equal u1 u2
+ in
+ Bound.equal m1.start m2.start &&
+ Bit.is_included m1.padding m2.padding &&
+ try
+ List.for_all2 included_segments m1.segments m2.segments
+ with Invalid_argument _ -> false (* Segmentations have different sizes *)
+
+ let is_empty_segment ~oracle l u =
+ match Bound.cmp ~oracle l u with
+ | Equal | Greater -> true
+ | Lower | Uncomparable -> false
+
+ let check_segments s = (* TODO: remove *)
+ match s with
+ | [] -> assert false
+ | s -> s
+
+ (* Merge the two first slices of a segmentation *)
+ exception NothingToMerge
+ let merge_first ~oracle l = function
+ | [] | [_] -> raise NothingToMerge
+ | (v1,m) :: (v2,u) :: tail ->
+ let v1' = if is_empty_segment ~oracle l m then `Bottom else `Value v1
+ and v2' = if is_empty_segment ~oracle m u then `Bottom else `Value v2
in
- let pretty_index fmt range =
- Format.fprintf fmt "[%a]" Int_val.pretty range
+ match Bottom.join (M.smash ~oracle) v1' v2' with
+ | `Bottom -> tail
+ | `Value v -> (v,u) :: tail
+
+ let unify ~oracle f (m1 (*Left*): t) (m2 (*Right*) : t) : t =
+ (* Shortcuts *)
+ let compare side = Bound.cmp ~oracle:(oracle side) in
+ let equals side b1 b2 =
+ compare side b1 b2 = Equal
+ in
+ let join side =
+ let oracle = fun _ -> oracle side in
+ Bottom.join (M.join ~oracle)
+ in
+
+ let {start=l1 ; segments=s1 ; padding=p1 } = m1
+ and {start=l2 ; segments=s2 ; padding=p2 } = m2 in
+ (* Unify the segmentation start *)
+ let l = Bound.lower_bound ~oracle l1 l2 in
+ let s1 = if equals Left l l1 then s1 else (M.of_raw p1, l1) :: s1
+ and s2 = if equals Right l l2 then s2 else (M.of_raw p2, l2) :: s2
+ in
+ (* Unify the segmentation end *)
+ let merge_first side = merge_first ~oracle:(oracle side) in
+ let rec smash_end side l = function
+ | [] -> `Bottom, l
+ | [(v,u)] -> `Value v, u
+ | t -> smash_end side l (merge_first side l t)
+ in
+ let unify_end l s1 s2 =
+ let v1, u1 = smash_end Left l s1
+ and v2, u2 = smash_end Right l s2 in
+ let u = Bound.upper_bound ~oracle u1 u2 in
+ let w1 =
+ if equals Left u u1 then v1 else join Left (`Value (M.of_raw p1)) v1
+ and w2 =
+ if equals Right u u2 then v2 else join Right (`Value (M.of_raw p2)) v2
+ in
+ match Bottom.join f w1 w2 with
+ | `Bottom -> [] (* should not happen, but [] is still correct *)
+ | `Value w -> [(w,u)]
+ in
+ (* +----+-------+-----
+ | v1 | v1' |
+ +----+-------+-----
+ l u1
+ +------+-------+---
+ | v2 | v2' |
+ +------+-------+---
+ l u2 *)
+ let rec aux l s1 s2 acc =
+ (* Look for emerging slices *)
+ let left_slice_emerges = match s1 with
+ | (v1,u1) :: t1 when equals Right l u1 -> Some (v1,u1,t1)
+ | _ -> None
+ and right_slice_emerges = match s2 with
+ | (v2,u2) :: t2 when equals Left l u2 -> Some (v2,u2,t2)
+ | _ -> None
+ in
+ match left_slice_emerges, right_slice_emerges with
+ | Some (v1,u1,t1), None -> (* left slice emerges *)
+ aux u1 t1 s2 ((v1,u1) :: acc)
+ | None, Some (v2,u2,t2) -> (* right slice emerges *)
+ aux u2 s1 t2 ((v2,u2) :: acc)
+ | Some _, Some _ (* both emerges, can't choose *)
+ | None, None -> (* none emerges *)
+ match s1, s2 with (* Are we done yet ? *)
+ | [], [] -> acc
+ | _ :: _, [] | [], _ :: _-> unify_end l s1 s2 @ acc
+ | (v1,u1) :: t1, (v2,u2) :: t2 ->
+ try
+ match compare Left u1 u2, compare Right u1 u2 with (* Compare bounds *)
+ | _, Equal ->
+ (* u1 and u2 can be indeferently used right side
+ -> use u1 as next bound
+ Note: Asymetric choice, u2 may also be a good choice *)
+ aux u1 t1 t2 ((f v1 v2, u1) :: acc)
+ | Equal, _ ->
+ (* u1 and u2 can be indeferently used left side
+ -> use u2 as next bound *)
+ aux u2 t1 t2 ((f v1 v2, u2) :: acc)
+ | Greater, (Greater | Uncomparable) ->
+ (* u1 > u2 on the left side, we are sure u2 doesn't appear left
+ -> remove u2, merge slices *)
+ aux l s1 (merge_first Right l s2) acc
+ | (Lower | Uncomparable), Lower ->
+ (* u1 < u2 on the right side, we are sure u1 doesn't appear right
+ -> remove u1, merge slices *)
+ aux l (merge_first Left l s1) s2 acc
+ | Greater, Lower (* Can't choose which bound to remove first *)
+ | (Lower | Uncomparable), (Greater | Uncomparable) ->
+ aux l (merge_first Left l s1) (merge_first Right l s2) acc
+ with NothingToMerge -> (* There is nothing left to merge *)
+ unify_end l s1 s2 @ acc
+ in
+ (* Iterate through segmentations *)
+ {
+ start = l ;
+ segments = check_segments (aux l s1 s2 []) ;
+ padding = Bit.join p1 p2 ;
+ }
+
+ let singleton padding lindex uindex value =
+ {
+ padding ;
+ start = lindex ;
+ segments = check_segments [(value,uindex)] ;
+ }
+
+ let read ~oracle map reduce m index =
+ let is_below = function
+ | Lower-> true
+ | Equal | Greater | Uncomparable -> false
+ and is_above = function
+ | Greater | Equal -> true
+ | Lower | Uncomparable -> false
+ and fold acc x =
+ Bottom.join reduce acc (`Value (map x))
+ in
+ let aux (prev,acc) (v,u) =
+ let next = Bound.cmp ~oracle index u in
+ next,
+ if is_below prev || is_above next then acc else fold acc v
+ in
+ let first = Bound.cmp ~oracle index m.start in
+ let acc = `Bottom in
+ let acc = if is_above first then acc else fold acc (M.of_raw m.padding) in
+ let last,acc = List.fold_left aux (first,acc) m.segments in
+ let acc = if is_below last then acc else fold acc (M.of_raw m.padding) in
+ match acc with
+ | `Bottom -> assert false (* TODO: ensure that with typing *)
+ | `Value v -> v
+
+ (* TODO: partitioning strategies
+ 1. reinforcement without loss
+ 2. weak update without singularization
+ 3. update reduces the number of segments to 3 *)
+ let write ~oracle f m lindex uindex =
+ let (<=) b1 b2 = match Bound.cmp ~oracle b1 b2 with
+ | Lower | Equal -> true
+ | Greater | Uncomparable -> false
+ and (>=) b1 b2 = match Bound.cmp ~oracle b1 b2 with
+ | Greater | Equal -> true
+ | Lower | Uncomparable -> false
+ in
+ let rec aux_before l s =
+ if lindex >= l
+ then aux_below l [] l s
+ else aux_over lindex [] lindex (M.of_raw m.padding) l s
+ and aux_below start head l = function (* l < index *)
+ | [] ->
+ aux_end start head l (M.of_raw m.padding) uindex []
+ | (v,u) :: t ->
+ if lindex >= u
+ then aux_below start ((v,u) :: head) u t
+ else aux_over start head l v u t
+ and aux_over start head l v u = function (* l >= index *)
+ | [] ->
+ aux_end start head l (M.smash ~oracle v (M.of_raw m.padding)) uindex []
+ | ((v',u') :: t) as s ->
+ if uindex <= u'
+ then aux_end start head l v u s
+ (* TODO: do not smash if the slices are covered by the write *)
+ else aux_over start head l (M.smash ~oracle v v') u' t
+ and aux_end start head l v u tail =
+ let tail' =
+ (if is_empty_segment ~oracle l lindex then [] else [(v,lindex)]) @
+ [(f v,uindex)] @
+ (if is_empty_segment ~oracle uindex u then [] else [(v,u)]) @
+ tail
in
- let pretty_indexes fmt l =
- Pretty_utils.pp_list pretty_index fmt l
+ {
+ m with
+ segments = check_segments (List.rev_append head tail');
+ start ;
+ }
+ in
+ aux_before m.start m.segments
+
+ let incr_bound ~oracle vi x m =
+ let rec aux acc = function
+ | [] -> acc
+ | (v,u) :: t ->
+ match Option.bind x (fun x -> Bound.incr vi x u) with
+ | Some u -> aux ((v,u) :: acc) t
+ | None ->
+ match t with
+ | [] ->
+ let u = Bound.upper_const ~oracle u
+ and v = M.smash ~oracle (M.of_raw m.padding) v in
+ (v,u) :: acc
+ | (v',u') :: t -> aux ((M.smash ~oracle v v',u') :: acc) t
+ in
+ let start, segments =
+ match Option.bind x (fun x -> Bound.incr vi x m.start) with
+ | Some start -> start, m.segments
+ | None ->
+ match m.segments with
+ | [] -> assert false
+ | (v,u) :: t ->
+ let l = Bound.lower_const ~oracle m.start
+ and v = M.smash ~oracle (M.of_raw m.padding) v in
+ l, (v,u) :: t
+ in
+ { m with start ; segments = check_segments (List.rev (aux [] segments)) }
+
+ let map f m =
+ { m with segments = check_segments (List.map (fun (v,u) -> f v, u) m.segments) }
+end
+
+
+(* ------------------------------------------------------------------------ *)
+(* --- Typed memory abstraction --- *)
+(* ------------------------------------------------------------------------ *)
+
+module TypedMemory (Config : Config) (V : Value) =
+struct
+ (* Recursively instanciate the typed memory *)
+ module rec ProtoMemory : ProtoMemory with type value = V.t =
+ struct
+ type value = V.t
+
+ type t =
+ | Raw of bit
+ | Scalar of memory_scalar
+ | Struct of memory_struct
+ | Union of memory_union
+ | Array of memory_array
+ and memory_scalar = {
+ scalar_value: V.t;
+ scalar_type: Cil_types.typ;
+ }
+ and memory_struct = {
+ struct_value: S.t;
+ struct_type: Cil_types.compinfo;
+ }
+ (* unions are handled separately from struct to avoid confusion and error *)
+ and memory_union = {
+ union_value: t;
+ union_field: Cil_types.fieldinfo;
+ union_padding: bit;
+ }
+ and memory_array = {
+ array_value: A.t;
+ array_cell_type: Cil_types.typ;
+ }
+
+ let are_scalar_compatible s1 s2 =
+ are_typ_compatible s1.scalar_type s2.scalar_type
+
+ let are_aray_compatible a1 a2 =
+ are_typ_compatible a1.array_cell_type a2.array_cell_type
+
+ let are_structs_compatible s1 s2 =
+ s1.struct_type.ckey = s2.struct_type.ckey
+
+ let are_union_compatible u1 u2 =
+ Cil_datatype.Fieldinfo.equal u1.union_field u2.union_field
+
+ let rec pp ~root fmt =
+ let prefix fmt =
+ if not root then Format.fprintf fmt " = "
in
- let pretty_field fmt =
- let first = ref true in
- fun fi m ->
- if not !first then Format.fprintf fmt ",@;<1 2>";
- first := false;
- let indexes, sub = leading_indexes [] m in
- Format.fprintf fmt "@[<hv>.%s%a = %a@]"
- fi.Cil_types.fname
- pretty_indexes indexes
- pretty sub
+ let pretty_bit fmt = function
+ | Uninitialized -> Format.fprintf fmt "UNINITIALIZED"
+ | Zero -> Format.fprintf fmt "0"
+ | Any (Set set) when Base.SetLattice.O.is_empty set ->
+ Format.fprintf fmt "[--..--]"
+ | Any _ -> Format.fprintf fmt "T"
in
function
| Raw b ->
- begin match b with
- | Uninitialized -> Format.fprintf fmt "UNINITIALIZED"
- | Zero -> Format.fprintf fmt "0"
- | Any (Set set) when Base.SetLattice.O.is_empty set ->
- Format.fprintf fmt "[--..--]"
- | Any _ -> Format.fprintf fmt "T"
- end
- | Scalar {scalar_value} -> Value.pretty fmt scalar_value
+ Format.fprintf fmt "%t%a" prefix pretty_bit b
+ | Scalar { scalar_value } ->
+ Format.fprintf fmt "%t%a" prefix V.pretty scalar_value
| Struct s ->
- Format.fprintf fmt "{@;<1 2>";
- FieldMap.iter (pretty_field fmt) s.struct_value;
- Format.fprintf fmt "@ }";
+ Format.fprintf fmt "%t%a" prefix S.pretty s.struct_value
| Union u ->
- Format.fprintf fmt "{@;<1 2>%t@ }"
- (fun fmt -> pretty_field fmt u.union_field u.union_value)
+ Format.fprintf fmt ".%s%a"
+ u.union_field.Cil_types.fname
+ (pp ~root:false) u.union_value
| Array a ->
- let indexes, sub = leading_indexes [a.array_range] a.array_value in
- Format.fprintf fmt "%a = %a"
- pretty_indexes indexes
- pretty sub
+ Format.fprintf fmt "%a" A.pretty a.array_value
+
+ let pretty fmt m = pp ~root:false fmt m
+ let pretty_root fmt m = pp ~root:true fmt m
- let rec hash = function
- | Raw b -> Bit.hash b
+ let rec hash m = match m with
+ | Raw b -> Hashtbl.hash (
+ 1,
+ Bit.hash b)
| Scalar s -> Hashtbl.hash (
- Value.hash s.scalar_value,
+ 2,
+ V.hash s.scalar_value,
Cil_datatype.Typ.hash s.scalar_type)
| Struct s -> Hashtbl.hash (
- FieldMap.hash s.struct_value,
- Cil_datatype.Compinfo.hash s.struct_info,
- Bit.hash s.struct_padding)
+ 3,
+ S.hash s.struct_value,
+ Cil_datatype.Compinfo.hash s.struct_type)
| Union u -> Hashtbl.hash (
+ 4,
hash u.union_value,
Cil_datatype.Fieldinfo.hash u.union_field,
Bit.hash u.union_padding)
| Array a -> Hashtbl.hash (
- hash a.array_value,
- Cil_datatype.Typ.hash a.array_cell_type,
- Int_val.hash a.array_range,
- Bit.hash a.array_padding)
+ 5,
+ A.hash a.array_value,
+ Cil_datatype.Typ.hash a.array_cell_type)
let rec equal m1 m2 =
match m1, m2 with
| Raw b1, Raw b2 -> Bit.equal b1 b2
| Scalar s1, Scalar s2 ->
- Value.equal s1.scalar_value s2.scalar_value &&
+ V.equal s1.scalar_value s2.scalar_value &&
Cil_datatype.Typ.equal s1.scalar_type s2.scalar_type
| Struct s1, Struct s2 ->
- FieldMap.equal s1.struct_value s2.struct_value &&
- Bit.equal s1.struct_padding s2.struct_padding &&
- Cil_datatype.Compinfo.equal s1.struct_info s2.struct_info
+ S.equal s1.struct_value s2.struct_value &&
+ Cil_datatype.Compinfo.equal s1.struct_type s2.struct_type
| Union u1, Union u2 ->
equal u1.union_value u2.union_value &&
Bit.equal u1.union_padding u2.union_padding &&
Cil_datatype.Fieldinfo.equal u1.union_field u2.union_field
| Array a1, Array a2 ->
- equal a1.array_value a2.array_value &&
- Cil_datatype.Typ.equal a1.array_cell_type a2.array_cell_type &&
- Int_val.equal a1.array_range a2.array_range &&
- Bit.equal a1.array_padding a2.array_padding
+ A.equal a1.array_value a2.array_value &&
+ Cil_datatype.Typ.equal a1.array_cell_type a2.array_cell_type
| (Raw _ | Scalar _ | Struct _ | Union _ | Array _), _ -> false
let rec compare m1 m2 =
@@ -271,21 +954,18 @@ struct
match m1, m2 with
| Raw b1, Raw b2 -> Bit.compare b1 b2
| Scalar s1, Scalar s2 ->
- Value.compare s1.scalar_value s2.scalar_value <?>
+ V.compare s1.scalar_value s2.scalar_value <?>
(Cil_datatype.Typ.compare, s1.scalar_type, s2.scalar_type)
| Struct s1, Struct s2 ->
- FieldMap.compare s1.struct_value s2.struct_value <?>
- (Bit.compare, s1.struct_padding, s2.struct_padding) <?>
- (Cil_datatype.Compinfo.compare, s1.struct_info, s2.struct_info)
+ S.compare s1.struct_value s2.struct_value <?>
+ (Cil_datatype.Compinfo.compare, s1.struct_type, s2.struct_type)
| Union u1, Union u2 ->
compare u1.union_value u2.union_value <?>
(Bit.compare, u1.union_padding, u2.union_padding) <?>
(Cil_datatype.Fieldinfo.compare, u1.union_field, u2.union_field)
| Array a1, Array a2 ->
- compare a1.array_value a2.array_value <?>
- (Cil_datatype.Typ.compare, a1.array_cell_type, a2.array_cell_type) <?>
- (Int_val.compare, a1.array_range, a2.array_range) <?>
- (Bit.compare, a1.array_padding, a2.array_padding)
+ A.compare a1.array_value a2.array_value <?>
+ (Cil_datatype.Typ.compare, a1.array_cell_type, a2.array_cell_type)
| Raw _, _ -> 1
| _, Raw _ -> -1
| Scalar _, _ -> 1
@@ -294,135 +974,51 @@ struct
| _, Struct _ -> -1
| Union _, _ -> 1
| _, Union _ -> -1
- end
-
-
- (* Instanciation of Hptmaps for the tree structure of the memory *)
-
- module Initial_Values = struct let v = [[]] end
-
- module Deps = struct let l = Config.deps end
-
- module Field =
- struct
- include Cil_datatype.Fieldinfo
- let id f = f.Cil_types.forder (* At each node, all fields come from the same comp *)
- end
-
- module rec Memory :
- Hptmap.V with type t = FieldMap.t memory =
- struct
- include Datatype.Make (
- struct
- include Datatype.Undefined
- include MemorySafe
- let name = "Memory_map.Typed"
- let reprs = [ Raw Bit.top ]
- end)
- let pretty_debug = pretty
- end
-
- (* To allow recursive modules to be instanciated, there must be one safe
- module in the cycle. This is it. It should contain all references
- to FieldMap and no constants, only functions *)
- and MemorySafe :
- sig
- type t = FieldMap.t memory
- val pretty : Format.formatter -> t -> unit
- val hash : t -> int
- val equal : t -> t -> bool
- val compare : t -> t -> int
- end =
- struct
- include Prototype (FieldMap)
- end
-
- (* Maps for structures : field -> node *)
- and FieldMap :
- Hptmap_sig.S
- with type key = Cil_types.fieldinfo
- and type v = Memory.t =
- Hptmap.Make (Field) (Memory) (Hptmap.Comp_unused) (Initial_Values) (Deps)
-
- (* Caches *)
-
- let _cache_name s =
- Hptmap_sig.PersistentCache ("Multidim_domain.(" ^ Value.name ^ ")." ^ s)
-
- (* Datatype *)
-
- include Memory
-
- (* Constuctors *)
-
- let top = Raw Bit.top
-
- let zero = Raw Bit.zero
-
- let is_top m =
- m = top
-
- (* Types compatibility *)
-
- let typ_size t =
- Integer.of_int (Cil.bitsSizeOf t)
-
- let are_typ_compatible t1 t2 =
- Integer.equal (typ_size t1) (typ_size t2)
- let are_scalar_compatible s1 s2 =
- are_typ_compatible s1.scalar_type s2.scalar_type
-
- let are_aray_compatible a1 a2 =
- are_typ_compatible a1.array_cell_type a2.array_cell_type
-
- let are_structs_compatible s1 s2 =
- s1.struct_info.ckey = s2.struct_info.ckey
-
- let are_union_compatible u1 u2 =
- Field.equal u1.union_field u2.union_field
-
- (* Conversion *)
-
- let raw m =
- let rec aux acc = function
- | Raw b -> Bit.join acc b
- | Scalar s -> Bit.join acc (Value.to_bit s.scalar_value)
+ let of_raw b = Raw b
+
+ let rec raw m = match m with
+ | Raw b -> b
+ | Scalar s -> V.to_bit s.scalar_value
+ | Struct s -> S.raw s.struct_value
+ | Union u -> raw u.union_value
+ | Array a -> A.raw a.array_value
+
+ let of_value scalar_type scalar_value =
+ Scalar { scalar_type ; scalar_value }
+
+ let to_value typ = function
+ | Scalar s when are_typ_compatible s.scalar_type typ -> s.scalar_value
+ | m -> V.of_bit (raw m)
+
+ let rec weak_erase b = function
+ | Raw b' ->
+ Raw (Bit.join b' b)
+ | Scalar s when Bit.is_any b ->
+ Raw (Bit.join (V.to_bit s.scalar_value) b)
+ | Scalar s ->
+ Scalar { s with scalar_value = V.(join (of_bit b) s.scalar_value) }
| Array a ->
- let acc = Bit.join acc a.array_padding in
- aux acc a.array_value
+ Array { a with array_value = A.weak_erase b a.array_value }
| Struct s ->
- let acc = Bit.join acc s.struct_padding in
- FieldMap.fold (fun _ x acc -> aux acc x) s.struct_value acc
- | Union u ->
- let acc = Bit.join acc u.union_padding in
- aux acc u.union_value
- in
- aux Zero m
-
- (* Lattice operations *)
+ Struct { s with struct_value = S.weak_erase b s.struct_value }
+ | Union u -> Union {
+ u with
+ union_padding = Bit.join u.union_padding b;
+ union_value = weak_erase b u.union_value;
+ }
- let is_included =
let rec is_included m1 m2 = match m1, m2 with
| _, Raw r -> Bit.is_included (raw m1) r
| Scalar s1, Scalar s2 ->
are_scalar_compatible s1 s2 &&
- Value.(is_included s1.scalar_value s2.scalar_value)
+ V.is_included s1.scalar_value s2.scalar_value
| Array a1, Array a2 ->
are_aray_compatible a1 a2 &&
- Int_val.equal a1.array_range a2.array_range &&
- Bit.is_included a1.array_padding a2.array_padding &&
- is_included a1.array_value a2.array_value
+ A.is_included a1.array_value a2.array_value
| Struct s1, Struct s2 ->
are_structs_compatible s1 s2 &&
- Bit.is_included s1.struct_padding s2.struct_padding &&
- let decide_fast s t = if s == t then FieldMap.PTrue else PUnknown in
- let decide_fst _fi m1 = is_included m1 (Raw s2.struct_padding) in
- let decide_snd _fi m2 = is_included (Raw s1.struct_padding) m2 in
- let decide_both _fi m1 m2 = is_included m1 m2 in
- FieldMap.binary_predicate Hptmap_sig.NoCache UniversalPredicate
- ~decide_fast ~decide_fst ~decide_snd ~decide_both
- s1.struct_value s2.struct_value
+ S.is_included s1.struct_value s2.struct_value
| Union u1, Union u2 ->
are_union_compatible u1 u2 &&
Bit.is_included u1.union_padding u2.union_padding &&
@@ -432,254 +1028,176 @@ struct
| Array _, (Scalar _ | Struct _ | Union _)
| Struct _, (Scalar _ | Array _ | Union _)
| Union _, (Scalar _ | Array _ | Struct _) -> false
- in
- is_included
- let join f =
- let rec join m1 m2 =
- match m1, m2 with
- | Raw b1, Raw b2 -> Raw (Bit.join b1 b2)
- | Scalar s1, Scalar s2 when are_scalar_compatible s1 s2 ->
- let size = typ_size s1.scalar_type in
- Scalar {
- scalar_type = s1.scalar_type;
- scalar_value = f ~size s1.scalar_value s2.scalar_value;
- }
- | Scalar s, Raw b | Raw b, Scalar s ->
- let size = typ_size s.scalar_type in
- Scalar {
- s with
- scalar_value = f ~size (Value.of_bit b) s.scalar_value;
- }
- | Array a1, Array a2 when are_aray_compatible a1 a2 ->
- let array_range = Int_val.join a1.array_range a2.array_range in
- let array_value =
- let v1 =
- if not (Int_val.is_included array_range a1.array_range)
- then join a1.array_value (Raw a1.array_padding) (* Increase the range of a1 *)
- else a1.array_value
- and v2 =
- if not (Int_val.is_included array_range a2.array_range)
- then join a2.array_value (Raw a2.array_padding) (* Increase the range of a2 *)
- else a2.array_value
+ let unify ~oracle f =
+ let rec aux m1 m2 =
+ match m1, m2 with
+ | Raw b1, Raw b2 -> Raw (Bit.join b1 b2)
+ | m, Raw b | Raw b, m -> weak_erase b m
+ | Scalar s1, Scalar s2
+ when are_typ_compatible s1.scalar_type s2.scalar_type ->
+ let size = typ_size s1.scalar_type in
+ let scalar_value = f ~size s1.scalar_value s2.scalar_value in
+ Scalar { s1 with scalar_value }
+ | Array a1, Array a2 when are_aray_compatible a1 a2 ->
+ let array_value = A.unify ~oracle aux a1.array_value a2.array_value in
+ Array { a1 with array_value }
+ | Struct s1, Struct s2 when are_structs_compatible s1 s2 ->
+ let struct_value = S.unify aux s1.struct_value s2.struct_value in
+ Struct { s1 with struct_value }
+ | Union u1, Union u2 when are_union_compatible u1 u2 ->
+ Union {
+ u1 with
+ union_value = aux u1.union_value u2.union_value;
+ union_padding = Bit.join u1.union_padding u2.union_padding;
+ }
+ | _,_ ->
+ Raw (Bit.join (raw m1) (raw m2))
+ in
+ aux
+
+ let join ~oracle = unify ~oracle (fun ~size:_ -> V.join)
+
+ let smash ~oracle = join ~oracle:(fun _ -> oracle)
+
+ let read ~oracle (map : Cil_types.typ -> t -> 'a) (reduce : 'a -> 'a -> 'a) =
+ let rec aux offset m =
+ match offset, m with
+ | NoOffset t, m ->
+ map t m
+ | Field (fi, offset'), Struct s
+ when s.struct_type.ckey = fi.fcomp.ckey ->
+ aux offset' (S.read s.struct_value fi)
+ | Field (fi, offset'), Union u
+ when Cil_datatype.Fieldinfo.equal u.union_field fi ->
+ aux offset' u.union_value
+ | Index (exp, _index, elem_type, offset'), Array a
+ when are_typ_compatible a.array_cell_type elem_type ->
+ A.read ~oracle (aux offset') reduce a.array_value (Bound.of_exp (Option.get exp)) (* TODO: handle None *)
+ | _, m -> (* structure mismatch *)
+ let r = Raw (raw m) in
+ match offset with
+ | NoOffset t -> map t r
+ | Field (_, offset') | Index (_, _, _, offset') -> aux offset' r
+ in
+ aux
+
+ let write ~oracle (f : weak:bool -> Cil_types.typ -> t -> t) =
+ let rec aux ~weak offset m =
+ match offset with
+ | NoOffset t ->
+ f ~weak t m
+ | Field (fi, offset') ->
+ if fi.fcomp.cstruct then (* Structures *)
+ let old = match m with
+ | Struct s when s.struct_type.ckey = fi.fcomp.ckey -> s
+ | _ -> { struct_type = fi.fcomp ; struct_value = S.of_raw (raw m) }
+ in
+ Struct {
+ old with
+ struct_value = S.write old.struct_value fi (aux ~weak offset')
+ }
+ else (* Unions *)
+ let old = match m with
+ | Union u when Cil_datatype.Fieldinfo.equal u.union_field fi -> u
+ | _ ->
+ let b = raw m in
+ { union_value = Raw b ; union_field = fi ; union_padding = b }
+ in
+ Union {
+ old with
+ union_value = aux ~weak offset' old.union_value
+ }
+ | Index (exp, index, elem_type, offset') ->
+ let lindex, uindex, weak = match exp with
+ | None ->
+ let l, u = Int_val.min_and_max index in
+ let l = Option.get l and u = Option.get u in (* TODO: handle exceptions *)
+ Bound.of_integer l, Bound.of_integer u,
+ weak || Integer.(equal (succ l) u)
+ | Some e ->
+ let b = Bound.of_exp e in
+ b, Bound.succ b, weak
in
- join v1 v2;
- and array_padding = Bit.join a1.array_padding a2.array_padding in
- Array { a1 with array_value; array_range; array_padding }
- | Array a, (Raw b) | (Raw b), Array a ->
- Array {
- a with
- array_value = join (Raw b) a.array_value;
- array_padding = Bit.join b a.array_padding;
- }
- | Struct s1, Struct s2 when are_structs_compatible s1 s2 ->
- let decide b =
- FieldMap.Traversing (fun _fi m -> Some (join (Raw b) m))
- in
- let decide_both _fi = fun m1 m2 -> Some (join m1 m2)
- and decide_left = decide s2.struct_padding
- and decide_right = decide s1.struct_padding
- in
- let struct_value = FieldMap.merge
- ~cache:Hptmap_sig.NoCache
- ~symmetric:false ~idempotent:true
- ~decide_both ~decide_left ~decide_right
- s1.struct_value s2.struct_value
- in
- Struct {
- s1 with
- struct_value;
- struct_padding = Bit.join s1.struct_padding s2.struct_padding;
- }
- | Struct s, Raw b | Raw b, Struct s ->
- Struct {
- s with
- struct_value = FieldMap.map (join (Raw b)) s.struct_value;
- struct_padding = Bit.join b s.struct_padding ;
- }
- | Union u1, Union u2 when are_union_compatible u1 u2 ->
- Union {
- u1 with
- union_value = join u1.union_value u2.union_value;
- union_padding = Bit.join u1.union_padding u2.union_padding;
- }
- | Union u, Raw b | Raw b, Union u ->
- Union {
- u with
- union_value = join (Raw b) u.union_value;
- union_padding = Bit.join b u.union_padding;
- }
- | _,_ ->
- Raw (Bit.join (raw m1) (raw m2))
- in
- join
+ match m with
+ | Array a when are_typ_compatible a.array_cell_type elem_type ->
+ let array_value =
+ A.write ~oracle (aux ~weak offset') a.array_value lindex uindex
+ in
+ Array { a with array_value }
+ | _ ->
+ let b = raw m in
+ let new_value = aux ~weak offset' (Raw b) in
+ let array_value = A.singleton b lindex uindex new_value in
+ Array { array_cell_type = elem_type ; array_value }
+ in aux
+
+ let incr_bound ~oracle vi x = (* TODO: keep subtree when nothing changes *)
+ let rec aux = function
+ | (Raw _ | Scalar _) as m -> m
+ | Struct s -> Struct { s with struct_value = S.map aux s.struct_value }
+ | Union u -> Union { u with union_value = aux u.union_value }
+ | Array a ->
+ 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
+ end
+ and S : Structures with type submemory = ProtoMemory.t =
+ Structures (Config) (ProtoMemory)
+ and A : Segmentation with type submemory = ProtoMemory.t =
+ Segmentation (Config) (ProtoMemory)
- let widen = join
+ include ProtoMemory
+
+ type location = Abstract_offset.typed_offset
+
+ let pretty = pretty_root
+
+ (* Constuctors *)
- let join = join (fun ~size:_ -> Value.join)
+ let top = of_raw Bit.top
+ let zero = of_raw Bit.zero
+ let is_top m = m = top
+
+ (* Widening *)
+
+ let widen = unify
(* Read/Write accesses *)
- let read (map : t -> 'a) (reduce : 'a -> 'a -> 'a) m offset : 'a =
- let rec aux m offset =
- match offset, m with
- | NoOffset t, Scalar s when are_typ_compatible s.scalar_type t ->
- map m
- | NoOffset _, m ->
- map m (* TODO check type compatibility *)
- | Field (fi, offset'), Struct s when s.struct_info.ckey = fi.fcomp.ckey ->
- begin try
- let m' = FieldMap.find fi s.struct_value in
- aux m' offset'
- with Not_found ->
- map (Raw s.struct_padding) (* field undefined *)
- end
- | Field (fi, offset'), Union u when Field.equal u.union_field fi ->
- aux u.union_value offset'
- | Index (index, elem_type, offset'), Array a
- when are_typ_compatible a.array_cell_type elem_type ->
- if Int_val.intersects index a.array_range then
- let r = aux a.array_value offset' in (* Read inside range *)
- if Int_val.is_included index a.array_range
- then r
- else reduce r (map (Raw a.array_padding)) (* Also read outside of range *)
- else
- map (Raw a.array_padding) (* Only read outside of range *)
- | _, _ -> map (Raw (raw m)) (* structure mismatch *)
- in
- aux m offset
+ let get ~oracle (m : t) (loc : location) : value =
+ read ~oracle to_value V.join loc m
- let get : t -> location -> value =
- let f = function
- | Scalar s -> s.scalar_value
- | m -> Value.of_bit (raw m)
- in
- read f Value.join
-
- let extract : t -> location -> t =
- read (fun x -> x) join
-
- let rec write (f : weak:bool -> t -> Cil_types.typ -> t) ~weak m = function
- | NoOffset t ->
- f ~weak m t
- | Field (fi, offset') ->
- if fi.fcomp.cstruct then (* Structures *)
- let old = match m with
- | Struct s when s.struct_info.ckey = fi.fcomp.ckey -> s
- | _ -> {
- struct_value = FieldMap.empty;
- struct_info = fi.fcomp;
- struct_padding = raw m
- }
- in
- let write' opt =
- let old = Option.value ~default:(Raw old.struct_padding) opt in
- Some (write f ~weak old offset')
- in
- Struct {
- old with struct_value = FieldMap.replace write' fi old.struct_value
- }
- else (* Unions *)
- let old = match m with
- | Union u when Field.equal u.union_field fi -> u
- | _ ->
- let b = raw m in {
- union_value = Raw b;
- union_field = fi;
- union_padding = b;
- }
- in
- Union {
- old with union_value = write f ~weak old.union_value offset'
- }
- | Index (index, elem_type, offset') ->
- match m with
- | Array a when are_typ_compatible a.array_cell_type elem_type ->
- (* The implementation of write-into-array is imprecise for now as it
- can be improved when the write is completely out of the current
- range. However, the implementation would be more complicated and
- we have other plans to increase the precision. *)
- let array_range = Int_val.join index a.array_range in
- let weak = weak || not (Int_val.is_included array_range index) in
- let old =
- if Int_val.is_included array_range a.array_range
- then a.array_value (* Range does not increase *)
- else join a.array_value (Raw a.array_padding)
- in
- Array {
- array_cell_type = a.array_cell_type;
- array_value = write f ~weak old offset';
- array_range;
- array_padding = a.array_padding;
- }
- | _ ->
- let b = raw m in
- Array {
- array_cell_type = elem_type;
- array_value = write f ~weak (Raw b) offset';
- array_range = index;
- array_padding = b;
- }
+ let extract ~oracle (m : t) (loc : location) : t =
+ read ~oracle (fun _typ x -> x) (smash ~oracle) loc m
- let set ~weak m offset new_v =
- let f ~weak m t =
- let scalar_value =
- if weak then
- let old_v = get m (NoOffset t) in
- Value.join old_v new_v
- else
- new_v
- in
- Scalar { scalar_value ; scalar_type=t }
+ let set ~oracle ~weak m offset new_v =
+ let f ~weak typ m =
+ of_value typ (if weak then V.join (to_value typ m) new_v else new_v)
in
- write ~weak f m offset
-
- let reinforce f' m offset =
- let f ~weak m scalar_type =
- match m with
- | m when weak -> m
- | Scalar s when are_typ_compatible s.scalar_type scalar_type ->
- Scalar { s with scalar_value = f' s.scalar_value }
- | Raw b ->
- Scalar { scalar_type; scalar_value = f' (Value.of_bit b) }
- | m -> m
+ write ~oracle ~weak f offset m
+
+ let reinforce ~oracle f m offset =
+ let f' ~weak typ m =
+ if weak then m else of_value typ (f (to_value typ m))
in
- write ~weak:false f m offset
-
- let rec weak_erase b = function
- | Raw b' -> Raw (Bit.join b' b)
- | Scalar s -> Raw (Bit.join (Value.to_bit s.scalar_value) b)
- | Array a -> Array {
- a with
- array_value = weak_erase b a.array_value;
- array_padding = Bit.join a.array_padding b;
- }
- | Struct s -> Struct {
- s with
- struct_padding = Bit.join s.struct_padding b;
- struct_value = FieldMap.map (weak_erase b) s.struct_value;
- }
- | Union u -> Union {
- u with
- union_padding = Bit.join u.union_padding b;
- union_value = weak_erase b u.union_value;
- }
+ write ~oracle ~weak:false f' offset m
- let erase ~weak m offset b =
- let f ~weak m _t =
+ let erase ~oracle ~weak m offset b =
+ let f ~weak _typ m =
if weak then
weak_erase b m
else
- Raw b
+ of_raw b
in
- write ~weak f m offset
+ write ~oracle ~weak f offset m
- let overwrite ~weak dst offset src =
- let f' ~weak m _t =
+ let overwrite ~oracle ~weak dst offset src =
+ let f ~weak _typ m =
if weak then
- join m src
+ smash ~oracle m src
else
src
in
- write ~weak f' dst offset
+ write ~oracle ~weak f offset dst
end
diff --git a/src/kernel_services/abstract_interp/abstract_memory.mli b/src/kernel_services/abstract_interp/abstract_memory.mli
index db5a1b8edf7..229dfee4bb7 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.mli
+++ b/src/kernel_services/abstract_interp/abstract_memory.mli
@@ -62,10 +62,16 @@ sig
val deps : State.t list
end
-module type T =
+
+type side = Left | Right
+type oracle = Cil_types.exp -> Ival.t
+type bioracle = side -> oracle
+type strength = Strong | Weak | Reinforce (* update strength *)
+
+module TypedMemory (Config : Config) (Value : Value) :
sig
- type location
- type value
+ type location = Abstract_offset.typed_offset
+ type value = Value.t
type t
(* Datatype *)
@@ -83,37 +89,38 @@ sig
val is_top : t -> bool
(* Get a value from a set of locations *)
- val get : t -> location -> value
+ val get : oracle:oracle -> t -> location -> value
(* Extract a sub map from a set of locations *)
- val extract : t -> location -> t
+ val extract : oracle:oracle -> t -> location -> t
(* Erase / initialize the memory on a set of locations. *)
- val erase : weak:bool -> t -> location -> bit -> t
+ val erase : oracle:oracle -> weak:bool -> t -> location -> bit -> t
(* Set a value on a set of locations *)
- val set : weak:bool -> t -> location -> value -> t
+ val set : oracle:oracle -> weak:bool -> t -> location -> value -> t
(* Copy a whole map over another *)
- val overwrite : weak:bool -> t -> location -> t -> t
+ val overwrite : oracle:oracle -> weak:bool -> t -> location -> t -> t
(* Reinforce values on a set of locations when the locations match the
memory structure ; does nothing on locations that cannot be matched *)
- val reinforce : (value -> value) -> t -> location -> t
-
+ val reinforce : oracle:oracle -> (value -> value) -> t -> location -> t
(* Test inclusion of one memory map into another *)
val is_included : t -> t -> bool
(* Finest partition that is coarcer than both *)
- val join : t -> t -> t
+ val join : oracle:bioracle -> t -> t -> t
(* Partition widening *)
- val widen : (size:size -> value -> value -> value) -> t -> t -> t
+ val widen : oracle:bioracle -> (size:size -> value -> value -> value) ->
+ t -> t -> t
+
+ (* Bounds update for array segmentations *)
+ val incr_bound : oracle:oracle -> Cil_types.varinfo -> Integer.t option ->
+ t -> t
+ (* Pretty prints memory *)
val pretty : Format.formatter -> t -> unit
end
-
-module Make (Config : Config) (Value : Value) : T
- with type value = Value.t
- and type location = Abstract_offset.typed_offset
diff --git a/src/kernel_services/abstract_interp/abstract_offset.ml b/src/kernel_services/abstract_interp/abstract_offset.ml
index 8556cc156da..f33429517c1 100644
--- a/src/kernel_services/abstract_interp/abstract_offset.ml
+++ b/src/kernel_services/abstract_interp/abstract_offset.ml
@@ -35,7 +35,7 @@ end
type typed_offset =
| NoOffset of Cil_types.typ
- | Index of Int_val.t * Cil_types.typ * typed_offset
+ | Index of Cil_types.exp option * Int_val.t * Cil_types.typ * typed_offset
| Field of Cil_types.fieldinfo * typed_offset
@@ -46,22 +46,38 @@ struct
let rec pretty fmt = function
| NoOffset _t -> ()
| Field (fi, s) -> Format.fprintf fmt ".%s%a" fi.fname pretty s
- | Index (i, _t, s) -> Format.fprintf fmt "[%a]%a" Int_val.pretty i pretty s
+ | Index (None, i, _t, s) ->
+ Format.fprintf fmt "[%a]%a"
+ Int_val.pretty i
+ pretty s
+ | Index (Some e, i, _t, s) ->
+ Format.fprintf fmt "[%a∈%a]%a"
+ Cil_printer.pp_exp e
+ Int_val.pretty i
+ pretty s
let rec append o1 o2 =
match o1 with
| NoOffset _t -> o2
| Field (fi, s) -> Field (fi, append s o2)
- | Index (i, t, s) -> Index (i, t, append s o2)
+ | Index (e, i, t, s) -> Index (e, i, t, append s o2)
let rec join o1 o2 =
match o1, o2 with
- | NoOffset t, NoOffset t' when Bit_utils.type_compatible t t' ->
+ | NoOffset t, NoOffset t'
+ when Bit_utils.type_compatible t t' ->
NoOffset t
- | Field (fi, s1), Field (fi', s2) when Cil_datatype.Fieldinfo.equal fi fi' ->
+ | Field (fi, s1), Field (fi', s2)
+ when Cil_datatype.Fieldinfo.equal fi fi' ->
Field (fi, join s1 s2)
- | Index (i1, t, s1), Index (i2, t', s2) when Bit_utils.type_compatible t t' ->
- Index (Int_val.join i1 i2, t, join s1 s2)
+ | Index (e1, i1, t, s1), Index (e2, i2, t', s2)
+ when Bit_utils.type_compatible t t' ->
+ let e = match e1, e2 with
+ | Some e1, Some e2 when Cil_datatype.ExpStructEq.equal e1 e2 ->
+ Some e1 (* keep expression only when equivalent from both offsets *)
+ | _ -> None
+ in
+ Index (e, Int_val.join i1 i2, t, join s1 s2)
| _ -> raise Abstract_interp.Error_Top
let array_bounds array_size =
@@ -89,7 +105,7 @@ struct
| TArray (elem_typ, array_size, _) ->
let idx = oracle exp in
assert_valid_index idx array_size;
- Index (idx, elem_typ, of_cil_offset oracle elem_typ sub)
+ Index (Some exp, idx, elem_typ, of_cil_offset oracle elem_typ sub)
| _ -> assert false
let rec of_int_val ~base_typ ~typ ival =
@@ -119,7 +135,7 @@ struct
in
assert_valid_index range array_size;
let sub = of_int_val ~base_typ:elem_typ ~typ rem in
- Index (range, elem_typ, sub)
+ Index (None, range, elem_typ, sub)
| TComp (ci, _) ->
if not ci.cstruct then
@@ -171,7 +187,7 @@ struct
| TArray (elem_typ, array_size, _) ->
let idx = index_of_term array_size index in
assert_valid_index idx array_size;
- Index (idx, elem_typ, of_term_offset elem_typ sub)
+ Index (None, idx, elem_typ, of_term_offset elem_typ sub)
| _ -> assert false
end
| _ -> raise Abstract_interp.Error_Top
@@ -179,8 +195,8 @@ struct
let rec is_singleton = function
| NoOffset _ -> true
| Field (_fi, sub) -> is_singleton sub
- | Index (ival, _elem_typ, sub) ->
- Int_val.is_singleton ival && is_singleton sub
+ | Index (e, ival, _elem_typ, sub) ->
+ (Option.is_some e || Int_val.is_singleton ival) && is_singleton sub
end
module TypedOffsetOrTop =
diff --git a/src/kernel_services/abstract_interp/abstract_offset.mli b/src/kernel_services/abstract_interp/abstract_offset.mli
index c877599164a..96723402c80 100644
--- a/src/kernel_services/abstract_interp/abstract_offset.mli
+++ b/src/kernel_services/abstract_interp/abstract_offset.mli
@@ -35,7 +35,7 @@ end
type typed_offset =
| NoOffset of Cil_types.typ
- | Index of Int_val.t * Cil_types.typ * typed_offset
+ | Index of Cil_types.exp option * Int_val.t * Cil_types.typ * typed_offset
| Field of Cil_types.fieldinfo * typed_offset
module TypedOffset : T with type t = typed_offset
diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in
index fcf96184910..0ca1ea3afa5 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -35,4 +35,13 @@ module List = struct
let equal f l1 l2 =
l1 == l2 || try List.for_all2 f l1 l2 with Invalid_argument _ -> false
+ let rec compare f l1 l2 =
+ if l1 == l2 then 0
+ else match l1, l2 with
+ | [], [] -> assert false
+ | [], _ :: _ -> -1
+ | _ :: _, [] -> 1
+ | x1 :: q1, x2 :: q2 ->
+ let n = f x1 x2 in
+ if n = 0 then compare f q1 q2 else n
end
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index d9b263c3022..cb378f0cd9c 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -38,4 +38,7 @@ module List: sig
(** since 4.12.0 *)
val equal: ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
+
+ (** since 4.12.0 *)
+ val compare: ('a -> 'a -> int) -> 'a list -> 'a list -> int
end
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index 5e986cb05cc..1b4d74a046d 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -69,6 +69,11 @@ let no_oracle exp =
| None -> raise Abstract_interp.Error_Top
| Some i -> Value.of_integer i
+let convert_oracle oracle =
+ fun exp ->
+ match Ival.project_int_val (Value.project_ival (oracle exp)) with
+ | Some int_val -> int_val
+ | None | exception Value.Not_based_on_null -> Int_val.top
type assigned = (Precise_locs.precise_location,Value.t) Eval.assigned
type builtin = assigned list -> assigned or_bottom
@@ -114,11 +119,7 @@ struct
(* Raises Abstract_domain.{Error_top,Error_bottom} *)
let of_lval oracle ((host,offset) : Cil_types.lval) : t =
- let oracle' exp =
- match Ival.project_int_val (Value.project_ival (oracle exp)) with
- | Some int_val -> int_val
- | None | exception Value.Not_based_on_null -> Int_val.top
- in
+ let oracle' = convert_oracle oracle in
let base_typ = Cil.typeOfLhost host in
let offset = Offset.of_cil_offset oracle' base_typ offset in
match host with
@@ -169,7 +170,7 @@ end
module Memory =
struct
module Config = struct let deps = [Ast.self] end
- module Memory = Abstract_memory.Make (Config) (Value)
+ module Memory = Abstract_memory.TypedMemory (Config) (Value)
module Prototype =
(* Datatype *)
@@ -189,30 +190,32 @@ struct
let is_included = Memory.is_included
let narrow = fun m1 _m2 -> m1
let join = Memory.join
+ let smash ~oracle = Memory.join ~oracle:(fun _ -> oracle)
let widen h = Memory.widen (fun ~size v1 v2 -> Value.widen (size,h) v1 v2)
+ let incr_bound = Memory.incr_bound
- let get m loc =
+ let get ~oracle m loc =
match loc with
| `Top -> Value.top
- | `Value loc -> Memory.get m loc
+ | `Value loc -> Memory.get ~oracle m loc
- let extract m loc =
+ let extract ~oracle m loc =
match loc with
| `Top -> Memory.top
- | `Value loc -> Memory.extract m loc
+ | `Value loc -> Memory.extract ~oracle m loc
- let erase ~weak m loc bit_value =
+ let erase ~oracle ~weak m loc bit_value =
match loc with
| `Top -> Memory.top
- | `Value loc -> Memory.erase ~weak m loc bit_value
+ | `Value loc -> Memory.erase ~oracle ~weak m loc bit_value
- let set ~weak new_v m loc =
+ let set ~oracle ~weak new_v m loc =
match loc with
| `Top -> Memory.top
| `Value loc ->
- Memory.set ~weak m loc new_v
+ Memory.set ~oracle ~weak m loc new_v
- let reinforce f m loc =
+ let reinforce ~oracle f m loc =
match loc with
| `Top -> m
| `Value loc ->
@@ -221,13 +224,13 @@ struct
| `Value v -> v
| `Bottom -> raise Abstract_interp.Error_Bottom
in
- Memory.reinforce f' m loc
+ Memory.reinforce ~oracle f' m loc
- let overwrite ~weak dst loc src =
+ let overwrite ~oracle ~weak dst loc src =
match loc with
| `Top -> Memory.top
| `Value loc ->
- Memory.overwrite ~weak dst loc src
+ Memory.overwrite ~oracle ~weak dst loc src
end
@@ -241,57 +244,6 @@ struct
(Base.Base) (Memory)
(Hptmap.Comp_unused) (Initial_Values) (Deps)
- let log_category = dkey
-
- let cache_name s =
- Hptmap_sig.PersistentCache ("Multidim_domain." ^ s)
-
-
- (* Lattice *)
-
- let top = empty
-
- let is_included =
- 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_fast s t = if s == t then PTrue else PUnknown in
- binary_predicate cache UniversalPredicate
- ~decide_fast ~decide_fst ~decide_snd ~decide_both
-
- let narrow =
- let cache = cache_name "narrow" 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)
-
- let join =
- let cache = cache_name "join" in
- let decide _ v1 v2 =
- let r = Memory.join v1 v2 in
- if Memory.(is_top r) then None else Some r
- in
- inter ~cache ~symmetric:true ~idempotent:true ~decide
-
- let widen kf stmt =
- let _,get_hints = Widen.getWidenHints kf stmt in
- let decide base b1 b2 =
- let r = Memory.widen (get_hints base) b1 b2 in
- if Memory.(is_top r) then None else Some r
- in
- inter ~cache:Hptmap_sig.NoCache ~symmetric:false ~idempotent:true ~decide
-
-end
-
-module Domain =
-struct
-
- include DomainLattice
- include Domain_builder.Complete (DomainLattice)
-
type state = t
type value = Value.t
type base = Base.t
@@ -301,6 +253,10 @@ struct
type mdlocation = Location.t (* should be = to location *)
type origin
+ let log_category = dkey
+
+ let cache_name s =
+ Hptmap_sig.PersistentCache ("Multidim_domain." ^ s)
(* Bases handling *)
@@ -326,14 +282,35 @@ struct
(* Accesses *)
- let read (map : memory -> offset -> 'a) (reduce : 'a -> 'a -> 'a)
- (state : state) (loc : mdlocation) : 'a or_bottom =
+ let rec read :
+ type a .
+ (memory -> offset -> a) -> (a -> a -> a) ->
+ 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
Bottom.join reduce (`Value v) acc
in
Location.fold f loc `Bottom
+ and get (state : state) (src : mdlocation) : value or_bottom =
+ let oracle = mk_oracle state in
+ read (Memory.get ~oracle) Value.join state src
+
+ and mk_oracle (state : state) : Abstract_memory.oracle =
+ let rec oracle exp =
+ match exp.enode with
+ | Lval lval ->
+ let ival = get state (Location.of_lval oracle lval) in
+ Bottom.non_bottom ival (* TODO: handle exception *)
+ | _ -> Value.top
+ in
+ fun exp -> Value.project_ival (oracle exp) (* TODO: handle exception *)
+
+ let extract (state : state) (src : mdlocation) : Memory.t or_bottom =
+ let oracle = mk_oracle state in
+ read (Memory.extract ~oracle) (Memory.smash ~oracle) state src
+
let write (update : memory -> offset -> memory)
(state : state) (loc : mdlocation) : state =
let f base off state =
@@ -344,30 +321,79 @@ struct
in
Location.fold f loc state
- let get (state : state) (src : mdlocation) : value or_bottom =
- read Memory.get Value.join state src
-
- let extract (state : state) (src : mdlocation) : Memory.t or_bottom =
- read Memory.extract Memory.join state src
-
let set (state : state) (dst : mdlocation) (v : value) : state =
- let weak = not (Location.is_singleton dst) in
- write (Memory.set ~weak v) state dst
+ let weak = not (Location.is_singleton dst)
+ and oracle = mk_oracle state in
+ write (Memory.set ~oracle ~weak v) state dst
let overwrite (state : state) (dst : mdlocation) (src : mdlocation) : state =
- let weak = not (Location.is_singleton dst) in
+ let weak = not (Location.is_singleton dst)
+ and oracle = mk_oracle state in
match extract state src with
| `Bottom -> state (* no source *)
| `Value value ->
- write (fun m off -> Memory.overwrite ~weak m off value) state dst
+ write (fun m off -> Memory.overwrite ~oracle ~weak m off value) state dst
let erase (state : state) (dst : mdlocation) (b : Abstract_memory.bit): state =
- let weak = not (Location.is_singleton dst) in
- write (fun m off -> Memory.erase ~weak m off b) state dst
+ let weak = not (Location.is_singleton dst)
+ and oracle = mk_oracle state in
+ write (fun m off -> Memory.erase ~oracle ~weak m off b) state dst
let reinforce (f : value -> value or_bottom)
(state : state) (dst : mdlocation) : state =
- write (fun m off -> Memory.reinforce f m off) state dst
+ let oracle = mk_oracle state in
+ write (fun m off -> Memory.reinforce ~oracle f m off) state dst
+
+ (* Lattice *)
+
+ let top = empty
+
+ let is_included =
+ 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_fast s t = if s == t then PTrue else PUnknown in
+ binary_predicate cache UniversalPredicate
+ ~decide_fast ~decide_fst ~decide_snd ~decide_both
+
+ let narrow =
+ let cache = cache_name "narrow" 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)
+
+ let join s1 s2 =
+ let oracle = function
+ | Abstract_memory.Left -> mk_oracle s1
+ | 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
+ in
+ inter ~cache ~symmetric:true ~idempotent:true ~decide s1 s2
+
+ let widen kf stmt s1 s2 =
+ let oracle = function
+ | Abstract_memory.Left -> mk_oracle s1
+ | 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
+ in
+ inter ~cache ~symmetric:false ~idempotent:true ~decide s1 s2
+end
+
+module Domain =
+struct
+ include DomainLattice
+ include Domain_builder.Complete (DomainLattice)
(* Eva Queries *)
@@ -424,6 +450,32 @@ struct
let update valuation state =
`Value (assume_valuation valuation state)
+ let update_array_segmentation lval expr state =
+ (* TODO: more general transfer function *)
+ (* TODO: only update memory models where the lval is present in the
+ segmentation *)
+ let increment expr =
+ match expr.Cil_types.enode with
+ | BinOp ((PlusA|PlusPI), { enode=Lval lval' }, exp, _typ)
+ when Cil_datatype.LvalStructEq.equal lval lval' ->
+ Cil.constFoldToInt exp
+ | BinOp ((PlusA|PlusPI), exp, { enode=Lval lval'}, _typ)
+ when Cil_datatype.LvalStructEq.equal lval lval' ->
+ Cil.constFoldToInt exp
+ | BinOp ((MinusA|MinusPI), { enode=Lval lval' }, exp, _typ)
+ when Cil_datatype.LvalStructEq.equal lval lval' ->
+ Option.map Integer.neg (Cil.constFoldToInt exp)
+ | _ -> None
+ in
+ match lval with
+ | Mem _, _ -> state (* Do nothing *)
+ | Var vi, offset ->
+ let incr = match offset with
+ | NoOffset -> increment expr
+ | _ -> None
+ in
+ map (Memory.incr_bound ~oracle:(mk_oracle state) vi incr) state
+
let assign_lval lval assigned_value oracle state =
try
let dst = Location.of_lval oracle lval in
@@ -440,7 +492,8 @@ struct
(* Failed to evaluate the left location *)
`Value top
- let assign _kinstr left _expr assigned_value valuation state =
+ let assign _kinstr left expr assigned_value valuation state =
+ let state = update_array_segmentation left.lval expr state in
let state = assume_valuation valuation state in
let oracle = make_oracle valuation in
assign_lval left.lval assigned_value oracle state
diff --git a/tests/value/oracle/multidim.res.oracle b/tests/value/oracle/multidim.res.oracle
index 8c162b23ce1..fb1fde102da 100644
--- a/tests/value/oracle/multidim.res.oracle
+++ b/tests/value/oracle/multidim.res.oracle
@@ -26,11 +26,11 @@
# multidim: T
y1 : # cvalue: .t1[0].f ∈ {3.}
{.t1{[0].i; [1..3]}; .t2[0..3]} ∈ {0}
- # multidim: { .t1[{0}] = { .f = {3.}, .i = {0} },
- .t2[{0; 1; 2; 3}] = { .f = {0}, .i = {0} } }
+ # multidim: { .t1[0] = { .f = [0. .. 3.], .i = {0} }, .t2[0..3] = {
+ .f = {0}, .i = {0} } }
y2 : # cvalue: .t1[0].f ∈ {4.} or UNINITIALIZED
{.t1{[0].i; [1..3]}; .t2[0..3]} ∈ UNINITIALIZED
- # multidim: { .t1[{0}] = { .f = {4.} } }
+ # multidim: { .t1[0] = { .f = {4.} } }
z : # cvalue: {0}
# multidim: 0
w : # cvalue: {0}
@@ -48,8 +48,8 @@
.t2[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[1].i ∈ [--..--]
.t2[2..3]{.f#; .i#} ∈ [0..18446744073701163007] repeated %64
- # multidim: { .t1[{0; 1; 2; 3}] = { .f = {{ ANYTHING }} },
- .t2[{0; 1; 2; 3}] = { .f = {{ ANYTHING }} } }
+ # multidim: { .t1[0..2] = { .f = {{ ANYTHING }} }, .t2[0..2] = {
+ .f = {{ ANYTHING }} } }
[eva] computing for function f <- main.
Called from multidim.c:48.
[eva] using specification for function f
@@ -57,13 +57,8 @@
[eva] multidim.c:49:
Frama_C_domain_show_each:
z : # cvalue: [--..--]
- # multidim: [{0; 1; 2; 3}] = {
- .t1[{0; 1; 2; 3}] = {
- .f = [-3.40282346639e+38 .. 3.40282346639e+38]
- },
- .t2[{0; 1; 2; 3}] = {
- .f = [-3.40282346639e+38 .. 3.40282346639e+38]
- } }
+ # multidim: [0..2] = { .t1[0..2] = { .f = T }, .t2[0..2] = {
+ .f = [-3.40282346639e+38 .. 3.40282346639e+38] } }
[eva:alarm] multidim.c:52: Warning: assertion got status unknown.
[eva] multidim.c:55: starting to merge loop iterations
[eva] multidim.c:54: starting to merge loop iterations
@@ -82,8 +77,7 @@
[--..--]
[3].t1[3].i ∈ {0; 2}
[3].t2[0..3] ∈ {0}
- # multidim: [{0; 1; 2; 3}] = {
- .t1[{0; 1; 2; 3}] = { .f = [0. .. 2.], .i = {0; 2} } }
+ # multidim: [0..3] = { .t1[0..3] = { .f = [0. .. 2.], .i = {0; 2} } }
[eva] computing for function Frama_C_interval <- main.
Called from multidim.c:63.
[eva] using specification for function Frama_C_interval
@@ -98,7 +92,7 @@
[eva] multidim.c:65:
Frama_C_domain_show_each:
t1 : # cvalue: [--..--]
- # multidim: { .f = [0. .. 2.], .i = {0; 2} }
+ # multidim: [--..--]
[eva] Recording results for main
[kernel] multidim.c:56: more than 0(28) elements to enumerate. Approximating.
[kernel] multidim.c:57: more than 0(28) elements to enumerate. Approximating.
--
GitLab