From 0ee707c812f1d8e0c37f782273e91aeb15bdf817 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 28 Jan 2021 18:12:34 +0100
Subject: [PATCH] [Eva] Multidim domain: extract code about typed offset
- also improve conversion from ival
---
Makefile | 1 +
headers/header_spec.txt | 2 +
.../abstract_interp/abstract_offset.ml | 231 +++++++++++++++++
.../abstract_interp/abstract_offset.mli | 41 +++
.../abstract_interp/memory_map.ml | 52 +---
.../abstract_interp/memory_map.mli | 9 +-
.../abstract_interp/multidim.ml | 42 ++-
.../abstract_interp/multidim.mli | 5 +
src/plugins/value/domains/multidim_domain.ml | 240 ++----------------
9 files changed, 344 insertions(+), 279 deletions(-)
create mode 100644 src/kernel_services/abstract_interp/abstract_offset.ml
create mode 100644 src/kernel_services/abstract_interp/abstract_offset.mli
diff --git a/Makefile b/Makefile
index 715e780673d..9598162d13d 100644
--- a/Makefile
+++ b/Makefile
@@ -597,6 +597,7 @@ KERNEL_CMO=\
src/kernel_services/abstract_interp/lmap.cmo \
src/kernel_services/abstract_interp/lmap_bitwise.cmo \
src/kernel_services/abstract_interp/multidim.cmo \
+ src/kernel_services/abstract_interp/abstract_offset.cmo \
src/kernel_services/abstract_interp/memory_map.cmo \
src/kernel_services/visitors/visitor.cmo \
src/kernel_services/ast_data/statuses_by_call.cmo \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 409ab53051f..8c1613bca1f 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -437,6 +437,8 @@ src/kernel_services/README.md: .ignore
src/kernel_services/abstract_interp/README.md: .ignore
src/kernel_services/abstract_interp/abstract_interp.ml: CEA_LGPL
src/kernel_services/abstract_interp/abstract_interp.mli: CEA_LGPL
+src/kernel_services/abstract_interp/abstract_offset.ml: CEA_LGPL
+src/kernel_services/abstract_interp/abstract_offset.mli: CEA_LGPL
src/kernel_services/abstract_interp/base.ml: CEA_LGPL
src/kernel_services/abstract_interp/base.mli: CEA_LGPL
src/kernel_services/abstract_interp/bottom.ml: CEA_LGPL
diff --git a/src/kernel_services/abstract_interp/abstract_offset.ml b/src/kernel_services/abstract_interp/abstract_offset.ml
new file mode 100644
index 00000000000..12f1fbedd58
--- /dev/null
+++ b/src/kernel_services/abstract_interp/abstract_offset.ml
@@ -0,0 +1,231 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* Implementation from Bit_utils *)
+let rec type_compatible t1 t2 =
+ match Cil.unrollType t1, Cil.unrollType t2 with
+ | TVoid _, TVoid _ -> true
+ | TInt (i1, _), TInt (i2, _) -> i1 = i2
+ | TFloat (f1, _), TFloat (f2, _) -> f1 = f2
+ | TPtr (t1, _), TPtr (t2, _) -> type_compatible t1 t2
+ | TArray (t1', s1, _, _), TArray (t2', s2, _, _) ->
+ type_compatible t1' t2' &&
+ (s1 == s2 || try Integer.equal (Cil.lenOfArray64 s1) (Cil.lenOfArray64 s2)
+ with Cil.LenOfArray -> false)
+ | TFun (r1, a1, v1, _), TFun (r2, a2, v2, _) ->
+ v1 = v2 && type_compatible r1 r2 &&
+ (match a1, a2 with
+ | None, _ | _, None -> true
+ | Some l1, Some l2 ->
+ try
+ List.for_all2
+ (fun (_, t1, _) (_, t2, _) -> type_compatible t1 t2) l1 l2
+ with Invalid_argument _ -> false)
+ | TNamed _, TNamed _ -> assert false
+ | TComp (c1, _, _), TComp (c2, _, _) -> c1.ckey = c2.ckey
+ | TEnum (e1, _), TEnum (e2, _) -> e1.ename = e2.ename
+ | TBuiltin_va_list _, TBuiltin_va_list _ -> true
+ | (TVoid _ | TInt _ | TFloat _ | TPtr _ | TArray _ | TFun _ | TNamed _ |
+ TComp _ | TEnum _ | TBuiltin_va_list _), _ ->
+ false
+
+module type T =
+sig
+ type t
+
+ val append : t -> t -> t (* Does not check that the appened offset fits *)
+ val join : t -> t -> t
+ val of_cil_offset : (Cil_types.exp -> Ival.t) -> Cil_types.typ -> Cil_types.offset -> t
+ val of_ival : Cil_types.typ -> Cil_types.typ -> Ival.t -> t
+ val of_term_offset : Cil_types.typ -> Cil_types.term_offset -> t
+ val is_singleton : t -> bool
+end
+
+type typed_offset =
+ | NoOffset of Cil_types.typ
+ | Index of Ival.t * Cil_types.typ * typed_offset
+ | Field of Cil_types.fieldinfo * typed_offset
+
+
+module TypedOffset =
+struct
+ type t = typed_offset
+
+ 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)
+
+ let rec join o1 o2 =
+ match o1, o2 with
+ | NoOffset t, NoOffset t' when type_compatible t t' ->
+ NoOffset t
+ | 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 type_compatible t t' ->
+ Index (Ival.join i1 i2, t, join s1 s2)
+ | _ -> raise Abstract_interp.Error_Top
+
+ let array_range array_size =
+ (* TODO: handle undefined sizes and not const foldable sizes *)
+ match array_size with
+ | None -> Ival.top
+ | Some size_exp ->
+ let u = Cil.constFoldToInt size_exp in
+ Ival.inject_range (Some Integer.zero) u
+
+ let assert_valid_index idx size =
+ let range = array_range size in
+ if not (Ival.is_included idx range) then
+ raise Abstract_interp.Error_Top
+
+ let rec of_cil_offset oracle base_typ = function
+ | Cil_types.NoOffset -> NoOffset base_typ
+ | Field (fi, sub) -> Field (fi, of_cil_offset oracle fi.ftype sub)
+ | Index (exp, sub) ->
+ match Cil.unrollType base_typ with
+ | 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)
+ | _ -> assert false
+
+ let rec of_ival base_typ typ ival =
+ if Ival.is_zero ival && type_compatible base_typ typ then
+ NoOffset typ
+ else
+ match Cil.unrollType base_typ with
+ | TArray (elem_typ, array_size, _, _) ->
+ (* TODO: Cil.bitsSizeOf doesn't work when elements are themselves array
+ of execution-time size *)
+ let elem_size = Integer.of_int (Cil.bitsSizeOf elem_typ) in
+ if Integer.is_zero elem_size then (* array of elements of size 0 *)
+ if Ival.is_zero ival then (* the whole range is valid *)
+ let sub = of_ival elem_typ typ ival in
+ Index (array_range array_size, elem_typ, sub)
+ else (* Non-zero offset cannot represent anything here *)
+ raise Abstract_interp.Error_Top
+ else
+ let range = Ival.scale_div ~pos:true elem_size ival
+ and range_rem = Ival.scale_rem ~pos:true elem_size ival in
+ let sub = of_ival elem_typ typ range_rem in
+ Index (range, elem_typ, sub)
+
+ | TComp (ci, _, _) ->
+ if not ci.cstruct then
+ (* Ignore unions for now *)
+ raise Abstract_interp.Error_Top
+ else
+ let rec find_field = function
+ | [] -> raise Abstract_interp.Error_Top
+ | fi :: q ->
+ let offset, width = Cil.fieldBitsOffset fi in
+ let l = Integer.(of_int offset) in
+ let u = Integer.(add l (of_int width)) in
+ let range = Ival.inject_range (Some l) (Some u) in
+ if Ival.is_included ival range then
+ let sub_ival = Ival.add_singleton_int (Integer.neg l) ival in
+ Field (fi, of_ival fi.ftype typ sub_ival)
+ else
+ find_field q
+ in
+ find_field (Option.value ~default:[] ci.cfields)
+
+ | _ -> raise Abstract_interp.Error_Top
+
+ let of_ival base_typ typ ival =
+ if Ival.is_small_set ival then
+ let f i acc =
+ Bottom.join join acc (`Value (of_ival base_typ typ i))
+ in
+ Bottom.non_bottom (Ival.fold_enum f ival `Bottom)
+ else
+ of_ival base_typ typ ival
+
+ let index_of_term t = (* Exact constant ranges *)
+ match t.Cil_types.term_node with
+ | Tempty_set -> Ival.bottom
+ | TConst (Integer (v, _)) -> Ival.inject_singleton v
+ | Trange (l,u) ->
+ let eval_bound = function
+ | { Cil_types.term_node=TConst (Integer (v, _)) } -> v
+ | _ -> raise Abstract_interp.Error_Top
+ in
+ let l' = Option.map eval_bound l
+ and u' = Option.map eval_bound u in
+ Ival.inject_range l' u'
+ | _ -> raise Abstract_interp.Error_Top
+
+ let rec of_term_offset base_typ = function
+ | Cil_types.TNoOffset -> NoOffset base_typ
+ | TField (fi, sub) ->
+ Field (fi, of_term_offset fi.ftype sub)
+ | TIndex (index, sub) ->
+ begin match Cil.unrollType base_typ with
+ | TArray (elem_typ, array_size, _, _) ->
+ let idx = index_of_term index in
+ assert_valid_index idx array_size;
+ Index (idx, elem_typ, of_term_offset elem_typ sub)
+ | _ -> assert false
+ end
+ | _ -> raise Abstract_interp.Error_Top
+
+ let rec is_singleton = function
+ | NoOffset _ -> true
+ | Field (_fi, sub) -> is_singleton sub
+ | Index (ival, _elem_typ, sub) ->
+ Ival.is_singleton_int ival && is_singleton sub
+end
+
+module TypedOffsetOrTop =
+struct
+ type t = [ `Value of typed_offset | `Top ]
+
+ let append o1 o2 =
+ match o1, o2 with
+ | `Top, _ | _, `Top -> `Top
+ | `Value o1, `Value o2 -> `Value (TypedOffset.append o1 o2)
+
+ let join o1 o2 =
+ match o1, o2 with
+ | `Top, _ | _, `Top -> `Top
+ | `Value o1, `Value o2 ->
+ try `Value (TypedOffset.join o1 o2)
+ with Abstract_interp.Error_Top -> `Top
+
+ let of_cil_offset oracle base_typ offset =
+ try `Value (TypedOffset.of_cil_offset oracle base_typ offset)
+ with Abstract_interp.Error_Top -> `Top
+
+ let of_ival base_typ typ ival =
+ try `Value (TypedOffset.of_ival base_typ typ ival)
+ with Abstract_interp.Error_Top -> `Top
+
+ let of_term_offset base_typ toffset =
+ try `Value (TypedOffset.of_term_offset base_typ toffset)
+ with Abstract_interp.Error_Top -> `Top
+
+ let is_singleton = function
+ | `Top -> false
+ | `Value o -> TypedOffset.is_singleton o
+end
diff --git a/src/kernel_services/abstract_interp/abstract_offset.mli b/src/kernel_services/abstract_interp/abstract_offset.mli
new file mode 100644
index 00000000000..b8ce523125d
--- /dev/null
+++ b/src/kernel_services/abstract_interp/abstract_offset.mli
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module type T =
+sig
+ type t
+
+ val append : t -> t -> t (* Does not check that the appened offset fits *)
+ val join : t -> t -> t
+ val of_cil_offset : (Cil_types.exp -> Ival.t) -> Cil_types.typ -> Cil_types.offset -> t
+ val of_ival : Cil_types.typ -> Cil_types.typ -> Ival.t -> t
+ val of_term_offset : Cil_types.typ -> Cil_types.term_offset -> t
+ val is_singleton : t -> bool
+end
+
+type typed_offset =
+ | NoOffset of Cil_types.typ
+ | Index of Ival.t * Cil_types.typ * typed_offset
+ | Field of Cil_types.fieldinfo * typed_offset
+
+module TypedOffset : T with type t = typed_offset
+module TypedOffsetOrTop : T with type t = [ `Value of typed_offset | `Top ]
diff --git a/src/kernel_services/abstract_interp/memory_map.ml b/src/kernel_services/abstract_interp/memory_map.ml
index 5e9d0e6986d..56af0309002 100644
--- a/src/kernel_services/abstract_interp/memory_map.ml
+++ b/src/kernel_services/abstract_interp/memory_map.ml
@@ -20,11 +20,11 @@
(* *)
(**************************************************************************)
-[@@@warning "-60"] (* unused module ; to be removed once ocaml is patched *)
-[@@@warning "-37"] (* constructor never used to build values. *)
-[@@@warning "-32"] (* unused value *)
+(* Ocaml compiler incorrectly considers that module MemorySafe is unused and
+ emits a warning *)
+[@@@warning "-60"]
-exception Not_implemented
+open Abstract_offset
type size = Integer.t
@@ -121,15 +121,9 @@ sig
end
-type typed_offset =
- | NoOffset of Cil_types.typ
- | Index of Ival.t * Cil_types.typ * typed_offset
- | Field of Cil_types.fieldinfo * typed_offset
-
-
-module MakeTyped (Config : Config) (Value : Value) =
+module Make (Config : Config) (Value : Value) =
struct
- type location = typed_offset
+ type location = Abstract_offset.typed_offset
type value = Value.t
type 'fieldmap memory' =
@@ -327,36 +321,7 @@ struct
let is_top m =
m = top
-(*
- let std_compare =
-
- let are_typ_compatible t1 2 =
- match Cil.unrollType t1, Cil.unrollType t2 with
- | TVoid _a1, TVoid _a2 -> true
- | TInt (i1, _a1), TInt (i2, _a2) -> i1 = i2
- | TFloat (f1, _a1), TFloat (f2, _a2) -> f1 = f2
- | TPtr _, TPtr _ -> true
- | TArray (t1, _size, _, _a1), TArray (t2, e2, _, _a2) ->
- are_typ_compatible t1 t2
- | TFun _, TFun _ -> true
- | TComp (c1, _, _a1), TComp (c2, _, _a2) ->
- c1.ckey = c2.ckey
- in
- if res <> 0 then res
- else compare_attributes config _a1 _a2
- | TEnum (e1, _a1), TEnum (e2, _a2) ->
- compare_chain
- (=?=) e1.ename e2.ename
- (compare_attributes config) _a1 _a2
- | TBuiltin_va_list _a1, TBuiltin_va_list _a2 ->
- compare_attributes config _a1 _a2
- | (TVoid _ | TInt _ | TFloat _ | TPtr _ | TArray _ | TFun _ | TNamed _ |
- TComp _ | TEnum _ | TBuiltin_va_list _ as a1), a2 ->
- index_typ a1 - index_typ a2
-
- let match_array celltyp = function
- |
-*)
+
let typ_size t =
Integer.of_int (Cil.bitsSizeOf t)
@@ -383,9 +348,6 @@ struct
let typ_size t =
Integer.of_int (Cil.bitsSizeOf t)
- let type_range t =
- Ival.inject_range (Some Integer.zero) (Some (typ_size t))
-
let is_included =
let rec is_included m1 m2 = match m1, m2 with
| Default d1, Default d2 -> Default.is_included d1 d2
diff --git a/src/kernel_services/abstract_interp/memory_map.mli b/src/kernel_services/abstract_interp/memory_map.mli
index a0371e0961c..57a7fd6f334 100644
--- a/src/kernel_services/abstract_interp/memory_map.mli
+++ b/src/kernel_services/abstract_interp/memory_map.mli
@@ -104,11 +104,6 @@ sig
val pretty : Format.formatter -> t -> unit
end
-type typed_offset =
- | NoOffset of Cil_types.typ
- | Index of Ival.t * Cil_types.typ * typed_offset
- | Field of Cil_types.fieldinfo * typed_offset
-
-module MakeTyped (Config : Config) (Value : Value) : T
+module Make (Config : Config) (Value : Value) : T
with type value = Value.t
- and type location = typed_offset
+ and type location = Abstract_offset.typed_offset
diff --git a/src/kernel_services/abstract_interp/multidim.ml b/src/kernel_services/abstract_interp/multidim.ml
index 2d8eca1853a..ea42409d070 100644
--- a/src/kernel_services/abstract_interp/multidim.ml
+++ b/src/kernel_services/abstract_interp/multidim.ml
@@ -29,26 +29,26 @@ module Term =
struct
type t = Integer.t * Integer.t
- let pretty fmt (d,b) =
+ let pretty fmt (d,b : t) =
Format.fprintf fmt "%a×[..%a]" pretty_int d pretty_int b
- let order (d1,_b1) (d2,_b2) = (* descending order *)
+ let order (d1,_b1 : t) (d2,_b2 : t) = (* descending order *)
Integer.compare d2 d1
(* Keep the same interval but change the dimension (leading to
over-approximation, hence coarcer abstraction). This might
produce two terms instead of one *)
- let coarsen (d,b) d' =
+ let coarsen (d,b : t) (d' : Integer.t) =
(* d×[0,b] -> (d'q + r)×[0,b] -> d'×[0,qb] + r×[0,b] *)
let q,r = Integer.e_div_rem d d' in
if Integer.is_zero r
then [ (d', Integer.mul q b) ]
else [ (d', Integer.mul q b) ; (r,b) ]
- let mul (d1,b1) (d2,b2) =
+ let mul (d1,b1 : t) (d2,b2 : t) =
Integer.mul d1 d2, Integer.mul b1 b2
- let mul_integer i (d,b) =
+ let mul_integer (i : Integer.t) (d,b : t) =
Integer.mul d i, b
end
@@ -201,3 +201,35 @@ let mod_integer (o,sum) i =
let mod_int x i =
mod_integer x (Integer.of_int i)
+
+(* Conversion from Cil *)
+
+let rec of_exp oracle = function
+ | { Cil_types.enode=BinOp (PlusA,e1,e2,_typ) } ->
+ add (of_exp oracle e1) (of_exp oracle e2)
+ | { enode=BinOp (Mult,e1,e2,_typ) } ->
+ mul (of_exp oracle e1) (of_exp oracle e2)
+ | { enode=BinOp (Shiftlt,e1,e2,_typ) } as expr ->
+ begin match oracle e2 with
+ | (i,[]) -> mul_integer (of_exp oracle e1) (Integer.two_power i)
+ | _ -> oracle expr (* default to oracle *)
+ end
+ | expr -> oracle expr (* default to oracle *)
+
+let of_offset oracle base_typ offset =
+ let rec aux base_typ base_size x = function
+ | Cil_types.NoOffset -> x, base_size
+ | Field (fi, sub) ->
+ let field_offset, field_size = Cil.fieldBitsOffset fi in
+ aux fi.ftype (Integer.of_int field_size) (add_int x field_offset) sub
+ | Index (exp, sub) ->
+ match base_typ with
+ | TArray (elem_typ, _array_size, _, _) ->
+ let idx = of_exp oracle exp in
+ let elem_size = Integer.of_int (Cil.bitsSizeOf elem_typ) in
+ let x' = add x (mul_integer idx elem_size) in
+ aux elem_typ elem_size x' sub
+ | _ -> assert false (* Index is only valid on arrays *)
+ in
+ let base_size = Integer.of_int (Cil.bitsSizeOf base_typ) in
+ fst (aux base_typ base_size zero offset)
diff --git a/src/kernel_services/abstract_interp/multidim.mli b/src/kernel_services/abstract_interp/multidim.mli
index 69cb39e01e1..26ff49c7a54 100644
--- a/src/kernel_services/abstract_interp/multidim.mli
+++ b/src/kernel_services/abstract_interp/multidim.mli
@@ -75,3 +75,8 @@ val mul_integer : t -> Integer.t -> t
val mod_int : t -> int -> t
val mod_integer : t -> Integer.t -> t
+
+(* Conversion from Cil *)
+
+val of_exp : (Cil_types.exp -> t) -> Cil_types.exp -> t (* improves over an oracle *)
+val of_offset : (Cil_types.exp -> t) -> Cil_types.typ -> Cil_types.offset -> t
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index e86ebcb5311..484549904b1 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -23,9 +23,6 @@
open Cil_types
open Eval
-[@@@warning "-60"] (* unused module *)
-[@@@warning "-32"] (* unused value *)
-
let dkey = Value_parameters.register_category "d-multidim"
let map_to_singleton map =
@@ -81,226 +78,20 @@ let find_builtin =
with Not_found -> None
-module MultidimOffset =
-struct
- include Multidim
-
- let field fi x =
- let field_offset, field_size = Cil.fieldBitsOffset fi in
- add_int x field_offset, Integer.of_int field_size
-
- let index elem_typ index x =
- let elem_size = Integer.of_int (Cil.bitsSizeOf elem_typ) in
- add x (mul_integer index elem_size), elem_size
-
- let rec of_exp oracle = function
- | { Cil_types.enode=BinOp (PlusA,e1,e2,_typ) } ->
- add (of_exp oracle e1) (of_exp oracle e2)
- | { enode=BinOp (Mult,e1,e2,_typ) } ->
- mul (of_exp oracle e1) (of_exp oracle e2)
- | { enode=BinOp (Shiftlt,e1,e2,_typ) } as expr ->
- begin match oracle e2 with
- | (i,[]) -> mul_integer (of_exp oracle e1) (Integer.two_power i)
- | _ -> oracle expr (* default to oracle *)
- end
- | expr -> oracle expr (* default to oracle *)
-
- let assert_valid_size idx _array_size =
- idx
-
- let of_offset oracle base_typ offset =
- let rec aux base_typ base_size x = function
- | Cil_types.NoOffset -> x, base_size
- | Field (fi, sub) ->
- let x', size = field fi x in
- aux fi.ftype size x' sub
- | Index (exp, sub) ->
- match base_typ with
- | TArray (elem_typ, array_size, _, _) ->
- let idx = of_exp oracle exp in
- let idx = assert_valid_size idx array_size in
- let x', elem_size = index elem_typ idx x in
- aux elem_typ elem_size x' sub
- | _ -> assert false (* Index is only valid on arrays *)
- in
- let base_size = Integer.of_int (Cil.bitsSizeOf base_typ) in
- aux base_typ base_size zero offset
-end
-
-(* Multidim adresses building from valuation *)
-
-module MultidimLocation =
-struct
- module Map = Base.Base.Map
-
- type size = Integer.t
- type offset = MultidimOffset.t
- type t = offset Map.t * size
-
- let size ((_map,size) : t) : size =
- size
-
- let fold f ((map,size):t) x =
- Map.fold (fun base offset -> f base (offset,size)) map x
-
- (* Raises Abstract_domain.{Error_top,Error_bottom} *)
- let of_lval oracle ((host,offset) : Cil_types.lval) =
- let oracle' expr =
- try MultidimOffset.of_ival (Value.project_ival (oracle expr))
- with Value.Not_based_on_null -> raise Abstract_interp.Error_Top
- in
- let base_typ = Cil.typeOfLhost host in
- let offset, size = MultidimOffset.of_offset oracle' base_typ offset in
- let map = match host with
- | Var vi ->
- Map.singleton (Base.of_varinfo vi) offset
- | Mem exp ->
- let add b o map =
- Map.add b MultidimOffset.(add (of_ival o) offset) map
- in
- Locations.Location_Bytes.fold_topset_ok add (oracle exp) Map.empty
- in
- map, size
-
- let is_singleton (map,_) =
- match map_to_singleton map with
- | None -> false
- | Some (b,o) -> not (Base.is_weak b) && MultidimOffset.is_singleton o
-end
-
-
-module Offset =
-struct
- open Memory_map
- type t = [ `Value of typed_offset | `Top ]
-
- let append o1 o2 =
- let rec aux o1 o2 =
- match o1 with
- | NoOffset _t -> o2
- | Field (fi, s) -> Field (fi, aux s o2)
- | Index (i, t, s) -> Index (i, t, aux s o2)
- in
- match o1, o2 with
- | `Top, _ | _, `Top -> `Top
- | `Value o1, `Value o2 -> `Value (aux o1 o2)
-
- let join o1 o2 =
- let rec aux o1 o2 =
- match o1, o2 with
- | NoOffset t, NoOffset t' when Cil_datatype.Typ.equal t t' ->
- NoOffset t
- | Field (fi, s1), Field (fi', s2) when Cil_datatype.Fieldinfo.equal fi fi' ->
- Field (fi, aux s1 s2)
- | Index (i1, t, s1), Index (i2, t', s2) when Cil_datatype.Typ.equal t t' ->
- Index (Ival.join i1 i2, t, aux s1 s2)
- | _ -> raise Abstract_interp.Error_Top
- in
- match o1, o2 with
- | `Top, _ | _, `Top -> `Top
- | `Value o1, `Value o2 ->
- try `Value (aux o1 o2) with Abstract_interp.Error_Top -> `Top
-
- let assert_valid_size idx _array_size =
- idx
-
- let of_offset oracle base_typ offset =
- (* Temorary debug *)
- let rec aux base_typ = function
- | Cil_types.NoOffset -> NoOffset base_typ
- | Field (fi, sub) -> Field (fi, aux fi.ftype sub)
- | Index (exp, sub) ->
- match Cil.unrollType base_typ with
- | TArray (elem_typ, array_size, _, _) ->
- let idx =
- try Value.project_ival (oracle exp)
- with Value.Not_based_on_null -> raise Abstract_interp.Error_Top
- in
- let idx = assert_valid_size idx array_size in
- Index (idx, elem_typ, aux elem_typ sub)
- | _ -> assert false
- in
- try `Value (aux base_typ offset) with Abstract_interp.Error_Top -> `Top
-
- let of_bits_offset base_typ typ i =
- try
- let offset, _t = Bit_utils.(find_offset base_typ i (MatchType typ)) in
- (* typ and _t may be different *)
- of_offset no_oracle base_typ offset
- with Bit_utils.NoMatchingOffset ->
- `Top
-
- let of_ival base_typ typ ival =
- match Ival.cardinal ival with
- | Some c when Integer.(lt c (of_int 100)) ->
- let f i acc =
- let offset = of_bits_offset base_typ typ i in
- match acc with
- | `Bottom -> offset
- | #t as prev -> join prev offset
- in
- begin match Ival.fold_int f ival `Bottom with
- | `Bottom -> assert false (* ival should not be bottom *)
- | #t as o -> o
- end
-
- | _ ->
- Value_parameters.feedback ~dkey ~current:true ~once:true
- "too many values to convert cvalues to multidim offset";
- `Top
-
- let index_of_term t =
- match t.term_node with
- | Tempty_set -> Ival.bottom
- | TConst (Integer (v, _)) -> Ival.inject_singleton v
- | Trange (l,u) ->
- let eval_bound = function
- | { term_node=TConst (Integer (v, _)) } -> v
- | _ -> raise Abstract_interp.Error_Top
- in
- let l' = Option.map eval_bound l
- and u' = Option.map eval_bound u in
- Ival.inject_range l' u'
- | _ -> raise Abstract_interp.Error_Top
-
- let of_term_offset base_typ offset =
- let rec aux base_typ = function
- | Cil_types.TNoOffset -> NoOffset base_typ
- | TField (fi, sub) ->
- Field (fi, aux fi.ftype sub)
- | TIndex (index, sub) ->
- begin match Cil.unrollType base_typ with
- | TArray (elem_typ, array_size, _, _) ->
- let idx = index_of_term index in
- let idx = assert_valid_size idx array_size in
- Index (idx, elem_typ, aux elem_typ sub)
- | _ -> assert false
- end
- | _ -> raise Abstract_interp.Error_Top
- in
- try `Value (aux base_typ offset) with Abstract_interp.Error_Top -> `Top
-
- let is_singleton =
- let rec aux = function
- | NoOffset _ -> true
- | Field (_fi, sub) -> aux sub
- | Index (ival, _elem_typ, sub) ->
- Ival.is_singleton_int ival && aux sub
- in function
- | `Top -> false
- | `Value o -> aux o
-end
-
module Location =
struct
+ open Abstract_offset
+
+ module Offset = TypedOffsetOrTop
module Map = Base.Base.Map
type offset = Offset.t
+ type base = Base.t
type t = offset Map.t
let empty = Map.empty
- let fold = Map.fold
+ let fold : (base-> offset -> 'a -> 'a) -> t -> 'a -> 'a = Map.fold
let is_singleton map =
match map_to_singleton map with
@@ -310,8 +101,12 @@ struct
(* Raises Abstract_domain.{Error_top,Error_bottom} *)
let of_lval oracle ((host,offset) as lval : Cil_types.lval) : t =
+ let oracle' exp =
+ try Value.project_ival (oracle exp)
+ with Value.Not_based_on_null -> Ival.top
+ in
let base_typ = Cil.typeOfLhost host in
- let offset : Offset.t = Offset.of_offset oracle base_typ offset in
+ let offset = Offset.of_cil_offset oracle' base_typ offset in
match host with
| Var vi ->
Map.singleton (Base.of_varinfo vi) offset
@@ -349,7 +144,7 @@ struct
let add_base base map =
(* Null base doesn't have a type ; use void instead *)
let typ = Option.value ~default:Cil.voidType (Base.typeof base) in
- Map.add base (`Value Memory_map.(NoOffset typ)) map
+ Map.add base (`Value (NoOffset typ)) map
in
Locations.Location_Bits.(fold_bases add_base loc'.loc empty)
end
@@ -360,7 +155,7 @@ end
module Base_Domain =
struct
module Config = struct let deps = [Ast.self] end
- module Memory = Memory_map.MakeTyped (Config) (Value)
+ module Memory = Memory_map.Make (Config) (Value)
module Prototype =
(* Datatype *)
@@ -441,7 +236,7 @@ struct
end
-module Prototype =
+module DomainPrototype =
struct
(* The domain is essentially a map from bases to individual memory abstractions *)
module Initial_Values = struct let v = [] end
@@ -635,20 +430,21 @@ struct
| `Value {value={v=`Bottom}} -> raise Abstract_interp.Error_Bottom
| `Value {value={v=`Value value}} -> value
- let assume_exp valuation expr record state =
+ let assume_exp _valuation _expr _record state = (*
let oracle = make_oracle valuation in
try
match expr.enode, record.value.v with
| Lval lv, `Value value ->
let loc = Location.of_lval oracle lv in
+ let update value' = `Value (Value.narrow value value') in
if Location.is_singleton loc
- then store state loc value
+ then update_loc update loc state
else state
| _, `Bottom -> state (* Indeterminate value, ignore *)
| _ -> state
with
(* Failed to evaluate the location *)
- Abstract_interp.Error_Top | Abstract_interp.Error_Bottom -> state
+ Abstract_interp.Error_Top | Abstract_interp.Error_Bottom -> *) state
let assume_valuation valuation state =
valuation.Abstract_domain.fold (assume_exp valuation) state
@@ -799,4 +595,4 @@ struct
end
-include Domain_builder.Complete (Prototype)
+include Domain_builder.Complete (DomainPrototype)
--
GitLab