From 9c61e985665a2829d84868f8ac6f94ecccacb82e Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Sun, 26 Dec 2021 16:10:43 +0100
Subject: [PATCH] [Eva] multidim: Prove initialization alarms
---
.../abstract_interp/abstract_memory.ml | 118 ++++++++++----
.../abstract_interp/abstract_memory.mli | 14 +-
src/plugins/value/domains/multidim_domain.ml | 154 ++++++++++++------
tests/value/oracle/multidim.res.oracle | 8 +-
4 files changed, 204 insertions(+), 90 deletions(-)
diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml
index d2e361038cc..16b4b49c667 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.ml
+++ b/src/kernel_services/abstract_interp/abstract_memory.ml
@@ -84,10 +84,51 @@ let are_typ_compatible t1 t2 =
(* --- Imprecise bits abstraction --- *)
(* ------------------------------------------------------------------------ *)
+type initialization =
+ | SurelyInitialized
+ | MaybeUninitialized
+
type bit =
| Uninitialized
- | Zero
- | Any of Base.SetLattice.t
+ | Zero of initialization
+ | Any of Base.SetLattice.t * initialization
+
+module Initialization =
+struct
+ let pretty fmt = function
+ | SurelyInitialized -> ()
+ | MaybeUninitialized ->
+ Format.fprintf fmt "or UNINITIALIZED"
+
+ let hash = function
+ | SurelyInitialized -> 3
+ | MaybeUninitialized -> 7
+
+ let equal i1 i2 =
+ match i1, i2 with
+ | SurelyInitialized, SurelyInitialized
+ | MaybeUninitialized, MaybeUninitialized -> true
+ | _, _ -> false
+
+ let compare i1 i2 =
+ match i1, i2 with
+ | SurelyInitialized, SurelyInitialized
+ | MaybeUninitialized, MaybeUninitialized -> 0
+ | SurelyInitialized, MaybeUninitialized -> -1
+ | MaybeUninitialized, SurelyInitialized -> 1
+
+ let is_included i1 i2 =
+ match i1, i2 with
+ | SurelyInitialized, _
+ | _, MaybeUninitialized -> true
+ | MaybeUninitialized, SurelyInitialized -> false
+
+ let join i1 i2 =
+ match i1, i2 with
+ | SurelyInitialized, SurelyInitialized -> SurelyInitialized
+ | MaybeUninitialized, _
+ | _, MaybeUninitialized -> MaybeUninitialized
+end
module Bit =
struct
@@ -96,54 +137,72 @@ struct
type t = bit
let uninitialized = Uninitialized
- let zero = Zero
- let numerical = Any Bases.empty
- let top = Any Bases.top
+ let zero = Zero SurelyInitialized
+ let numerical = Any (Bases.empty, SurelyInitialized)
+ let top = Any (Bases.top, MaybeUninitialized)
+
let pretty 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 "[--..--]"
+ | Uninitialized ->
+ Format.fprintf fmt "UNINITIALIZED"
+ | Zero i ->
+ Format.fprintf fmt "0%a" Initialization.pretty i
+ | Any (Set set, i) when Base.SetLattice.O.is_empty set ->
+ Format.fprintf fmt "[--..--]%a" Initialization.pretty i
| Any _ -> Format.fprintf fmt "T"
let is_any = function Any _ -> true | _ -> false
let hash = function
| Uninitialized -> 7
- | Zero -> 3
- | Any set -> Bases.hash set
+ | Zero i -> Hashtbl.hash (3, Initialization.hash i)
+ | Any (set, i)-> Hashtbl.hash (53, Bases.hash set, Initialization.hash i)
let equal d1 d2 =
match d1,d2 with
| Uninitialized, Uninitialized -> true
- | Zero, Zero -> true
- | Any set1, Any set2 -> Bases.equal set1 set2
+ | Zero i1, Zero i2 -> Initialization.equal i1 i2
+ | Any (set1,i1), Any (set2,i2) ->
+ Bases.equal set1 set2 && Initialization.equal i1 i2
| _, _ -> false
let compare d1 d2 =
match d1,d2 with
| Uninitialized, Uninitialized -> 0
- | Zero, Zero -> 0
- | Any set1, Any set2 -> Bases.compare set1 set2
+ | Zero i1, Zero i2 -> Initialization.compare i1 i2
+ | Any (set1,i1), Any (set2,i2) ->
+ Bases.compare set1 set2 <?> (Initialization.compare, i1, i2)
| Uninitialized, _ -> 1
| _, Uninitialized -> -1
- | Zero, _ -> 1
- | _, Zero -> -1
+ | Zero _, _ -> 1
+ | _, Zero _-> -1
+
+ let initialization = function
+ | Uninitialized -> MaybeUninitialized
+ | Zero i -> i
+ | Any (_,i) -> i
let is_included d1 d2 =
+ Initialization.is_included (initialization d1) (initialization d2) &&
match d1, d2 with
| Uninitialized, _ -> true
| _, Uninitialized -> false
- | Zero, _ -> true
- | _, Zero -> false
- | Any set1, Any set2 -> Bases.is_included set1 set2
+ | Zero _, _ -> true
+ | _, Zero _ -> false
+ | Any (set1,_), Any (set2,_) -> Bases.is_included set1 set2
let join d1 d2 =
match d1, d2 with
- | Uninitialized, d | d, Uninitialized -> d
- | Zero, d | d, Zero -> d
- | Any set1, Any set2 -> Any (Bases.join set1 set2)
+ | Uninitialized, Uninitialized -> Uninitialized
+ | Zero i1, Zero i2 ->
+ Zero (Initialization.join i1 i2)
+ | Any (set1,i1), Any (set2,i2) ->
+ Any (Bases.join set1 set2, Initialization.join i1 i2)
+ | Zero _, Uninitialized
+ | Uninitialized, Zero _ -> Zero MaybeUninitialized
+ | Any (set,i), (Zero _ | Uninitialized as b)
+ | (Zero _ | Uninitialized as b), Any (set,i) ->
+ Any (set, Initialization.join i (initialization b))
end
@@ -259,7 +318,7 @@ struct
include Datatype.Serializable_undefined
include M
let name = "Abstract_Memory.Structures.Values"
- let reprs = [ of_raw Zero ]
+ let reprs = [ of_raw Bit.zero ]
end)
let pretty_debug = pretty
end
@@ -416,7 +475,7 @@ struct
include Datatype.Serializable_undefined
include S
let name = "Abstract_Memory.Disjunction.S"
- let reprs = [ of_raw Zero ]
+ let reprs = [ of_raw Bit.zero ]
let eval_key key m = M.to_singleton_int (read m key)
let suitable_key key m = Option.is_some (eval_key key m)
let keys_candidates ci m =
@@ -1470,7 +1529,7 @@ struct
let rec to_singleton_int = function
| Scalar s -> V.to_integer s.scalar_value
- | Raw Zero -> Some Integer.zero
+ | Raw (Zero _) -> Some Integer.zero
| Union u -> to_singleton_int u.union_value
| _ -> None
@@ -1688,7 +1747,7 @@ struct
Array { array_cell_type = elem_type ; array_value }
in aux
- let incr_bound ~oracle vi x = (* TODO: keep subtree when nothing changes *)
+ let incr_bound ~oracle vi x m = (* 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 }
@@ -1697,7 +1756,10 @@ struct
| 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
+ in
+ let r = aux m in
+ (* debug true "bounds updated@.%a@.to%a" pretty m pretty r; *)
+ r
let add_segmentation_bounds ~oracle ~typ bounds =
let convert_bound exp =
diff --git a/src/kernel_services/abstract_interp/abstract_memory.mli b/src/kernel_services/abstract_interp/abstract_memory.mli
index 41f304a05f0..7a9ed21b0d5 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.mli
+++ b/src/kernel_services/abstract_interp/abstract_memory.mli
@@ -22,12 +22,18 @@
type size = Integer.t
+type initialization =
+ | SurelyInitialized
+ | MaybeUninitialized
+
type bit =
| Uninitialized (* Uninitialized everywhere *)
- | Zero (* Zero or uninitialized everywhere *)
- | Any of Base.SetLattice.t (* Undetermined anywhere, and can contain bits
- of pointers. If the base set is empty,
- the bit can only come from numerical values. *)
+ | Zero of initialization (* Zero or uninitialized everywhere *)
+ | Any of Base.SetLattice.t * initialization
+ (* Undetermined anywhere, and can contain bits
+ of pointers. If the base set is empty,
+ the bit can only come from numerical values. *)
+
module Bit :
sig
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index 112b20da720..6f9210091e0 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -37,25 +37,6 @@ struct
include Cvalue.V
include Cvalue_forward (* for fallback oracles *)
- let to_integer cvalue =
- try Some (Ival.project_int (project_ival cvalue))
- with Not_based_on_null | Ival.Not_Singleton_Int -> None
-
- let of_integer = inject_int
-
- let of_bit = function
- | Abstract_memory.Uninitialized -> bottom
- | Zero -> inject_int Integer.zero
- | Any (Set s) -> inject_top_origin Origin.top s
- | Any (Top) -> top_with_origin Origin.top
-
- let to_bit v =
- if is_bottom v
- then Abstract_memory.Uninitialized
- else if is_zero v
- then Abstract_memory.Zero
- else Abstract_memory.Any (get_bases v)
-
let backward_is_finite positive fkind v =
let prec = Fval.kind fkind in
try
@@ -65,10 +46,58 @@ struct
`Value v
end
+module Value_or_Uninitialized =
+struct
+ open Cvalue
+ include V_Or_Uninitialized
+
+ let to_integer cvalue =
+ try Some (Ival.project_int (V.project_ival (get_v cvalue)))
+ with V.Not_based_on_null | Ival.Not_Singleton_Int -> None
+
+ let make i v =
+ let initialized = match i with
+ | Abstract_memory.SurelyInitialized -> true
+ | Abstract_memory.MaybeUninitialized -> false
+ in
+ V_Or_Uninitialized.make ~initialized ~escaping:false v
+
+ let of_value v =
+ V_Or_Uninitialized.make ~initialized:true ~escaping:false v
+
+ let of_bit = function
+ | Abstract_memory.Uninitialized -> uninitialized
+ | Zero i -> make i (V.inject_int Integer.zero)
+ | Any (Set s,i) -> make i (V.inject_top_origin Origin.top s)
+ | Any (Top, i) -> make i (V.top_with_origin Origin.top)
+
+ let to_bit v' =
+ let v = get_v v'
+ and initialization =
+ if is_initialized v'
+ then Abstract_memory.SurelyInitialized
+ else Abstract_memory.MaybeUninitialized
+ in
+ if V.is_bottom v
+ then Abstract_memory.Uninitialized
+ else if V.is_zero v
+ then Abstract_memory.Zero (initialization)
+ else Abstract_memory.Any (V.get_bases v, initialization)
+
+ let from_flagged fv =
+ V_Or_Uninitialized.make
+ ~initialized:fv.initialized
+ ~escaping:false
+ (Bottom.value ~bottom:V.bottom fv.v)
+
+ let map' f v =
+ f (get_v v) >>-: fun new_v -> map (fun _ -> new_v) v
+end
+
let no_oracle exp =
match Cil.isInteger exp with
| None -> raise Abstract_interp.Error_Top
- | Some i -> Value.of_integer i
+ | Some i -> Value.inject_int i
let convert_oracle oracle =
fun exp ->
@@ -200,7 +229,7 @@ struct
let disjunctive_invariants =
Parameters.MultidimDisjunctiveInvariants.get
end
- module Memory = Abstract_memory.TypedMemory (Config) (Value)
+ module Memory = Abstract_memory.TypedMemory (Config) (Value_or_Uninitialized)
module Prototype =
(* Datatype *)
@@ -221,12 +250,14 @@ struct
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 widen h =
+ Memory.widen
+ (fun ~size v1 v2 -> Value_or_Uninitialized.widen (size,h) v1 v2)
let incr_bound = Memory.incr_bound
let get ~oracle m loc =
match loc with
- | `Top -> Value.top
+ | `Top -> Value_or_Uninitialized.top
| `Value loc -> Memory.get ~oracle m loc
let extract ~oracle m loc =
@@ -292,6 +323,7 @@ struct
type state = t
type value = Value.t
+ type value_or_uninitialized = Value_or_Uninitialized.t
type base = Base.t
type offset = Location.offset
type memory = Memory.t
@@ -339,18 +371,18 @@ struct
in
Location.fold f loc `Bottom
- and get (state : state) (src : mdlocation) : value or_bottom =
+ and get (state : state) (src : mdlocation) : value_or_uninitialized or_bottom =
let oracle = mk_oracle state in
- read (Memory.get ~oracle) Value.join state src
+ read (Memory.get ~oracle) Value_or_Uninitialized.join state src
- and mk_oracle' (state : state) : Cil_types.exp -> Value.t =
+ and mk_oracle' (state : state) : Cil_types.exp -> value =
(* Until Eva gives access to good oracles, we use this poor stupid oracle
instead *)
let rec oracle exp =
match exp.enode with
| Lval lval ->
let value = get state (Location.of_lval oracle lval) in
- Bottom.non_bottom value (* TODO: handle exception *)
+ Value_or_Uninitialized.get_v (Bottom.non_bottom value) (* TODO: handle exception *)
| Const (CInt64 (i,_,_)) -> Value.inject_int i
| UnOp (op, e, typ) -> Value.forward_unop typ op (oracle e)
| BinOp (op, e1, e2, TFloat (fkind, _)) ->
@@ -369,13 +401,21 @@ struct
in
fun exp -> oracle (Cil.constFold true exp)
- and mk_oracle (state : state) : Abstract_memory.oracle =
+ and convert_oracle (oracle : Cil_types.exp -> value)
+ : Abstract_memory.oracle =
fun exp ->
try
- Value.project_ival (mk_oracle' state exp)
+ Value.project_ival (oracle exp)
with Value.Not_based_on_null ->
Ival.top (* TODO: should it just not happen ? *)
+ and convert_oracle_or_default state = function (* TODO: use everywhere *)
+ | Some oracle -> convert_oracle oracle
+ | None -> mk_oracle state
+
+ and mk_oracle (state : state) : Abstract_memory.oracle =
+ convert_oracle (mk_oracle' state)
+
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
@@ -407,7 +447,7 @@ struct
(* Result can never be bottom if update never returns bottom *)
Bottom.non_bottom (write' (fun m o -> `Value (update m o)) state loc)
- let set (state : state) (dst : mdlocation) (v : value) : state =
+ let set (state : state) (dst : mdlocation) (v : value_or_uninitialized) : state =
let weak = not (Location.is_singleton dst)
and oracle = mk_oracle state in
write (Memory.set ~oracle ~weak v) state dst
@@ -425,9 +465,11 @@ struct
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)
+ let reinforce
+ ?oracle
+ (f : value_or_uninitialized -> value_or_uninitialized or_bottom)
(state : state) (dst : mdlocation) : state or_bottom =
- let oracle = mk_oracle state in
+ let oracle = convert_oracle_or_default state oracle in
write' (fun m off -> Memory.reinforce ~oracle f m off) state dst
(* Lattice *)
@@ -495,15 +537,19 @@ struct
| `Bottom, _ -> raise Abstract_interp.Error_Bottom
| `Value v, _ -> v
in
- let v =
- try
- let loc = Location.of_lval oracle lv in
- get state loc >>-: fun v -> v, None
- with
- | Abstract_interp.Error_Top -> `Value (Value.top, None)
- | Abstract_interp.Error_Bottom -> `Bottom
- in
- v, Alarmset.all
+ try
+ let loc = Location.of_lval oracle lv in
+ let v = get state loc in
+ (v >>-: fun v -> (Value_or_Uninitialized.get_v v, None)),
+ match v with
+ | `Bottom -> Alarmset.all
+ | `Value v ->
+ if Value_or_Uninitialized.is_initialized v
+ then Alarmset.(set (Alarms.Uninitialized lv) True all)
+ else Alarmset.all
+ with
+ | Abstract_interp.Error_Top -> `Value (Value.top, None), Alarmset.all
+ | Abstract_interp.Error_Bottom -> `Bottom, Alarmset.all
(* Eva Transfer *)
@@ -518,17 +564,19 @@ struct
state' >>- fun state ->
let oracle = make_oracle valuation in
try
- match expr.enode, record.value.v with
- | Lval lv, `Value value when not (Value.is_topint value) ->
- let loc = Location.of_lval oracle lv in
- let update value' =
- let v = Value.narrow value value' in
- if Value.is_bottom v then `Bottom else `Value v
- in
- if Location.is_singleton loc
- then reinforce update state loc
+ match expr.enode with
+ | Lval lv ->
+ let value = Value_or_Uninitialized.from_flagged record.value in
+ if not (Value.is_topint (Value_or_Uninitialized.get_v value)) then
+ let loc = Location.of_lval oracle lv in
+ let update value' =
+ let v = Value_or_Uninitialized.narrow value value' in
+ if Value_or_Uninitialized.is_bottom v then `Bottom else `Value v
+ in
+ if Location.is_singleton loc
+ then reinforce ~oracle update state loc
+ else `Value state
else `Value state
- | _, `Bottom -> `Value state (* Indeterminate value, ignore *)
| _ -> `Value state
with
(* Failed to evaluate the location *)
@@ -592,7 +640,7 @@ struct
let dst = Location.of_lval oracle lval in
match assigned_value with
| Assign value ->
- set state dst value
+ set state dst (Value_or_Uninitialized.of_value value)
| Copy (right, _value) ->
try
let src = Location.of_lval oracle right.lval in
@@ -681,7 +729,7 @@ struct
begin match Cil.unrollType (Logic_utils.logicCType typ) with
| TFloat (fkind,_) ->
let update = Value.backward_is_finite positive fkind in
- reinforce update state loc
+ reinforce (Value_or_Uninitialized.map' update) state loc
| _ | exception (Failure _) -> `Value state
end
| _ -> `Value state
diff --git a/tests/value/oracle/multidim.res.oracle b/tests/value/oracle/multidim.res.oracle
index 9d11b591920..634b46a94bf 100644
--- a/tests/value/oracle/multidim.res.oracle
+++ b/tests/value/oracle/multidim.res.oracle
@@ -42,7 +42,7 @@
}
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.} or UNINITIALIZED } }
z : # cvalue: {0}
# multidim: 0
[eva] multidim.c:45:
@@ -64,8 +64,8 @@
.t2[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[3].i ∈ [--..--]
# multidim: {
- .t1[0 .. 3] = { .f = {{ ANYTHING }} },
- .t2[0 .. 3] = { .f = {{ ANYTHING }} }
+ .t1[0 .. 3] = { .f = {{ ANYTHING }} or UNINITIALIZED },
+ .t2[0 .. 3] = { .f = {{ ANYTHING }} or UNINITIALIZED }
}
[eva] computing for function f <- main1 <- main.
Called from multidim.c:47.
@@ -207,8 +207,6 @@
[eva] multidim.c:147:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva:alarm] multidim.c:148: Warning:
- accessing uninitialized left-value. assert \initialized(&t[j].typ);
[eva] multidim.c:150: Frama_C_show_each_INT: {42}
[eva] multidim.c:153: Frama_C_show_each_FLOAT: {42.}
[eva] Recording results for main7
--
GitLab