diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 56b16b97f71b400fa7502c214f14319382e12f95..c6f8db8b6f69c634ccfd265263e9bd025c290884 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -24,142 +24,14 @@ open Eval
let dkey_card = Self.register_category "cardinal"
-module Model = struct
+module State = struct
- include Cvalue.Model
+ type state = Cvalue.Model.t * Locals_scoping.clobbered_set
type value = Main_values.CVal.t
type location = Main_locations.PLoc.location
- (* The origin is the value stored in the state for a lvalue, when this value
- has a type incompatible with the type of the lvalue. This may happen on
- union with fields of different types, or on code pattern such as
- int x = v; float f = *(float* )&x
- In this case, the value stored in the state and the value computed for the
- lvalue can be incomparable. The origin is then used to store the value from
- the state, to later choose which value to keep. This is done by the update
- function in cvalue_transfer. *)
- type origin = value
-
- let extract_expr _state _expr = `Value (Cvalue.V.top, None), Alarmset.all
-
- let indeterminate_alarms lval v =
- let open Cvalue.V_Or_Uninitialized in
- let status =
- if Cvalue.V.is_bottom (get_v v) then Alarmset.False else Alarmset.Unknown
- in
- match v with
- | C_uninit_noesc _ -> Alarmset.singleton ~status (Alarms.Uninitialized lval)
- | C_init_esc _ -> Alarmset.singleton ~status (Alarms.Dangling lval)
- | C_uninit_esc _ ->
- (* Unknown alarms: [v] can be either dangling or uninit *)
- Alarmset.(set (Alarms.Dangling lval) Unknown
- (set (Alarms.Uninitialized lval) Unknown none))
- | C_init_noesc _ -> Alarmset.none
-
-
- let eval_one_loc state lval typ =
- let eval_one_loc single_loc =
- let v = Cvalue.Model.find_indeterminate state single_loc in
- Cvalue.V_Or_Uninitialized.get_v v, indeterminate_alarms lval v
- in
- (* We have no good neutral element for "no alarm emitted yet", so we use
- [None] instead. *)
- let join_alarms acc alarms =
- match acc with
- | None -> Some alarms
- | Some acc -> Some (Alarmset.union alarms acc)
- in
- fun loc (acc_result, acc_alarms) ->
- let result, alarms = eval_one_loc loc in
- let result = Cvalue_forward.make_volatile ~typ:typ result in
- Cvalue.V.join result acc_result, join_alarms acc_alarms alarms
-
- (* The zero singleton is shared between float and integer representations in
- ival, and is thus untyped. *)
- let is_float v =
- Cvalue.V.(is_included v top_float) && Cvalue.V.contains_non_zero v
-
- let extract_scalar_lval state lval typ loc =
- let process_one_loc = eval_one_loc state lval typ in
- let acc = Cvalue.V.bottom, None in
- let value, alarms = Precise_locs.fold process_one_loc loc acc in
- let alarms = match alarms with None -> Alarmset.none | Some a -> a in
- (* The origin is set to false when the value stored in the memory has not
- the same type as the read lvalue. In this case, we don't update the state
- with the new value stemming from the evaluation, even if it has been
- reduced, in order to not propagate incompatible type. *)
- let incompatible_type = is_float value <> Cil.isFloatingType typ in
- let origin = if incompatible_type then Some value else None in
- let value = Cvalue_forward.reinterpret typ value in
- if Cvalue.V.is_bottom value
- then `Bottom, alarms
- else `Value (value, origin), alarms
-
- (* Imprecise version for aggregate types that cvalues are unable to precisely
- represent. The initialization alarms must remain sound, though. *)
- let extract_aggregate_lval state lval _typ ploc =
- let loc = Precise_locs.imprecise_location ploc in
- match loc.Locations.size with
- | Int_Base.Top -> `Value (Cvalue.V.top, None), Alarmset.all
- | Int_Base.Value size ->
- let offsm = Cvalue.Model.copy_offsetmap loc.Locations.loc size state in
- match offsm with
- | `Bottom -> `Bottom, Alarmset.none
- | `Value offsm ->
- let value = Cvalue.V_Offsetmap.find_imprecise_everywhere offsm in
- let alarms = indeterminate_alarms lval value in
- let v = Cvalue.V_Or_Uninitialized.get_v value in
- let v = if Cvalue.V.is_bottom v then `Bottom else `Value (v, None) in
- v, alarms
-
- let extract_lval state lval typ loc =
- if Cil.isArithmeticOrPointerType typ
- then extract_scalar_lval state lval typ loc
- else extract_aggregate_lval state lval typ loc
-
- let backward_location state _lval typ precise_loc value =
- let size = Precise_locs.loc_size precise_loc in
- let upto = succ (Int_set.get_small_cardinal()) in
- let loc = Precise_locs.imprecise_location precise_loc in
- let eval_one_loc single_loc =
- let v = Cvalue.Model.find state single_loc in
- let v = Cvalue_forward.make_volatile ~typ v in
- Cvalue_forward.reinterpret typ v
- in
- let process_ival base ival (acc_loc, acc_val as acc) =
- let loc_bits = Locations.Location_Bits.inject base ival in
- let single_loc = Locations.make_loc loc_bits size in
- let v = eval_one_loc single_loc in
- if Cvalue.V.intersects v value
- then Locations.Location_Bits.join loc_bits acc_loc, Cvalue.V.join v acc_val
- else acc
- in
- let fold_ival base ival acc =
- if Ival.cardinal_is_less_than ival upto
- then Ival.fold_enum (process_ival base) ival acc
- else process_ival base ival acc
- in
- let fold_location loc acc =
- try
- let loc = loc.Locations.loc in
- Locations.Location_Bits.fold_i fold_ival loc acc
- with
- Abstract_interp.Error_Top -> loc.Locations.loc, value
- in
- let acc = Locations.Location_Bits.bottom, Cvalue.V.bottom in
- let loc_bits, value = fold_location loc acc in
- if Locations.Location_Bits.is_bottom loc_bits
- then `Bottom
- else
- let loc = Precise_locs.inject_location_bits loc_bits in
- `Value (Precise_locs.make_precise_loc loc ~size, value)
-
-end
-
-
-module State = struct
-
- type state = Model.t * Locals_scoping.clobbered_set
+ let value_dependencies = Main_values.cval
+ let location_dependencies = Main_locations.ploc
let log_category = Self.dkey_cvalue_domain
@@ -167,15 +39,16 @@ module State = struct
struct
include Datatype.Serializable_undefined
type t = state
- let name = Model.name ^ "+clobbered_set"
- let reprs = List.map (fun s -> s, Locals_scoping.bottom ()) Model.reprs
+ let name = Cvalue.Model.name ^ "+clobbered_set"
+ let reprs =
+ List.map (fun s -> s, Locals_scoping.bottom ()) Cvalue.Model.reprs
let structural_descr =
- Structural_descr.(
- t_tuple [| Model.packed_descr; pack Locals_scoping.structural_descr |])
- let pretty fmt (s, _) = Model.pretty fmt s
- let equal (a, _) (b, _) = Model.equal a b
- let compare (a, _) (b, _) = Model.compare a b
- let hash (s, _) = Model.hash s
+ Structural_descr.t_tuple
+ [| Cvalue.Model.packed_descr; Locals_scoping.packed_descr |]
+ let pretty fmt (s, _) = Cvalue.Model.pretty fmt s
+ let equal (a, _) (b, _) = Cvalue.Model.equal a b
+ let compare (a, _) (b, _) = Cvalue.Model.compare a b
+ let hash (s, _) = Cvalue.Model.hash s
let rehash = Datatype.identity
let copy = Datatype.undefined
let mem_project = Datatype.never_any_project
@@ -184,33 +57,31 @@ module State = struct
let name = "cvalue"
let key = Structure.Key_Domain.create_key name
- type value = Model.value
- type location = Model.location
-
- let value_dependencies = Main_values.cval
- let location_dependencies = Main_locations.ploc
-
- let top = Model.top, Locals_scoping.bottom ()
- let is_included (a, _) (b, _) = Model.is_included a b
- let join (a, clob) (b, _) = Model.join a b, clob
+ let top = Cvalue.Model.top, Locals_scoping.bottom ()
+ let is_included (a, _) (b, _) = Cvalue.Model.is_included a b
+ let join (a, clob) (b, _) = Cvalue.Model.join a b, clob
let widen kf stmt (a, clob) (b, _) =
let hint = Widen.getWidenHints kf stmt in
- Model.widen hint a b, clob
+ Cvalue.Model.widen hint a b, clob
let narrow (a, clob) (b, _) =
- let s = Model.narrow a b in
- if Model.(equal bottom s) then `Bottom else `Value (s, clob)
+ let s = Cvalue.Model.narrow a b in
+ if Cvalue.Model.(equal bottom s) then `Bottom else `Value (s, clob)
- type origin = Model.origin
+ type origin = Cvalue_queries.origin
+
+ let extract_expr ~oracle context (state, _) expr =
+ Cvalue_queries.extract_expr ~oracle context state expr
+
+ let extract_lval ~oracle context (state, _) lval typ loc =
+ Cvalue_queries.extract_lval ~oracle context state lval typ loc
- let extract_expr ~oracle:_ _context (s, _) expr =
- Model.extract_expr s expr
- let extract_lval ~oracle:_ _context (s, _) lval typ loc =
- Model.extract_lval s lval typ loc
let backward_location (state, _) lval typ precise_loc value =
- Model.backward_location state lval typ precise_loc value
- let reduce_further _ _ _ = []
+ Cvalue_queries.backward_location state lval typ precise_loc value
+
+ let reduce_further (state, _) expr value =
+ Cvalue_queries.reduce_further state expr value
(* ------------------------------------------------------------------------ *)
(* Transfer Functions *)
@@ -241,11 +112,11 @@ module State = struct
let start_recursive_call stmt call recursion (state, clob) =
let direct = is_direct_recursion stmt call in
- let state = Model.remove_variables recursion.withdrawal state in
+ let state = Cvalue.Model.remove_variables recursion.withdrawal state in
let substitution = recursion.base_substitution in
let clob = if direct then clob else Locals_scoping.top () in
let state = Locals_scoping.substitute substitution clob state in
- Model.replace_base substitution state
+ Cvalue.Model.replace_base substitution state
let start_call stmt call recursion valuation (state, clob) =
(* Uses the [valuation] to update the [state] before the substitution
@@ -263,7 +134,7 @@ module State = struct
let direct = is_direct_recursion stmt call in
let pre, clob = pre in
let substitution = recursion.base_substitution in
- let state = Model.replace_base substitution state in
+ let state = Cvalue.Model.replace_base substitution state in
let clob = if direct then clob else Locals_scoping.top () in
let state = Locals_scoping.substitute substitution clob state in
let inter = Cvalue.Model.filter_by_shape recursion.base_withdrawal pre in
@@ -365,7 +236,7 @@ module State = struct
else Cvalue.V_Or_Uninitialized.C_uninit_noesc value
in
let loc = Precise_locs.imprecise_location loc in
- Model.add_indeterminate_binding ~exact:true state loc cvalue, clob
+ Cvalue.Model.add_indeterminate_binding ~exact:true state loc cvalue, clob
let empty () =
let open Cvalue in
@@ -399,7 +270,7 @@ module State = struct
| Abstract_domain.Result kf ->
let value = Library_functions.returned_value kf in
let loc = Locations.loc_of_varinfo varinfo in
- Model.add_binding ~exact:true state loc value, clob
+ Cvalue.Model.add_binding ~exact:true state loc value, clob
(* ------------------------------------------------------------------------ *)
(* Misc *)
@@ -416,13 +287,13 @@ module State = struct
else
Bottom.non_bottom (Cvalue.Default_offsetmap.default_offsetmap b)
in
- Model.add_base b offsm state
+ Cvalue.Model.add_base b offsm state
let bind_global state varinfo =
let base = Base.of_varinfo varinfo in
let loc = Locations.loc_of_base base in
let value = Cvalue.V_Or_Uninitialized.uninitialized in
- Model.add_indeterminate_binding ~exact:true state loc value
+ Cvalue.Model.add_indeterminate_binding ~exact:true state loc value
let enter_scope kind vars (state, clob) =
let bind =
@@ -433,7 +304,7 @@ module State = struct
List.fold_left bind state vars, clob
let leave_scope kf vars (state, clob) =
- let state = Model.remove_variables vars state in
+ let state = Cvalue.Model.remove_variables vars state in
try
let fdec = Kernel_function.get_definition kf in
Locals_scoping.make_escaping_fundec fdec clob vars state, clob
@@ -595,16 +466,16 @@ let registered =
type prefix = Hptmap.prefix
module Subpart = struct
- type t = Model.subtree
- let hash = Model.hash_subtree
- let equal = Model.equal_subtree
+ type t = Cvalue.Model.subtree
+ let hash = Cvalue.Model.hash_subtree
+ let equal = Cvalue.Model.equal_subtree
end
let distinct_subpart (a, _) (b, _) =
- if Model.equal a b then None
+ if Cvalue.Model.equal a b then None
else
- try Model.comp_prefixes a b; None
- with Model.Found_prefix (p, s1, s2) -> Some (p, s1, s2)
-let find_subpart (s, _) prefix = Model.find_prefix s prefix
+ try Cvalue.Model.comp_prefixes a b; None
+ with Cvalue.Model.Found_prefix (p, s1, s2) -> Some (p, s1, s2)
+let find_subpart (s, _) prefix = Cvalue.Model.find_prefix s prefix
module Getters (Dom : Abstract.Domain.External) = struct
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
new file mode 100644
index 0000000000000000000000000000000000000000..dddb9502ff0994fc0ebad6a0c5a2c5f2a1645249
--- /dev/null
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
@@ -0,0 +1,157 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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 Queries = struct
+
+ type state = Cvalue.Model.t
+ type value = Main_values.CVal.t
+ type location = Main_locations.PLoc.location
+
+ (* The origin is the value stored in the state for a lvalue, when this value
+ has a type incompatible with the type of the lvalue. This may happen on
+ union with fields of different types, or on code pattern such as
+ int x = v; float f = *(float* )&x
+ In this case, the value stored in the state and the value computed for the
+ lvalue can be incomparable. The origin is then used to store the value from
+ the state, to later choose which value to keep. This is done by the update
+ function in cvalue_transfer. *)
+ type origin = value
+
+ let extract_expr ~oracle:_ _context _state _expr =
+ `Value (Cvalue.V.top, None), Alarmset.all
+
+ let indeterminate_alarms lval v =
+ let open Cvalue.V_Or_Uninitialized in
+ let status =
+ if Cvalue.V.is_bottom (get_v v) then Alarmset.False else Alarmset.Unknown
+ in
+ match v with
+ | C_uninit_noesc _ -> Alarmset.singleton ~status (Alarms.Uninitialized lval)
+ | C_init_esc _ -> Alarmset.singleton ~status (Alarms.Dangling lval)
+ | C_uninit_esc _ ->
+ (* Unknown alarms: [v] can be either dangling or uninit *)
+ Alarmset.(set (Alarms.Dangling lval) Unknown
+ (set (Alarms.Uninitialized lval) Unknown none))
+ | C_init_noesc _ -> Alarmset.none
+
+
+ let eval_one_loc state lval typ =
+ let eval_one_loc single_loc =
+ let v = Cvalue.Model.find_indeterminate state single_loc in
+ Cvalue.V_Or_Uninitialized.get_v v, indeterminate_alarms lval v
+ in
+ (* We have no good neutral element for "no alarm emitted yet", so we use
+ [None] instead. *)
+ let join_alarms acc alarms =
+ match acc with
+ | None -> Some alarms
+ | Some acc -> Some (Alarmset.union alarms acc)
+ in
+ fun loc (acc_result, acc_alarms) ->
+ let result, alarms = eval_one_loc loc in
+ let result = Cvalue_forward.make_volatile ~typ:typ result in
+ Cvalue.V.join result acc_result, join_alarms acc_alarms alarms
+
+ (* The zero singleton is shared between float and integer representations in
+ ival, and is thus untyped. *)
+ let is_float v =
+ Cvalue.V.(is_included v top_float) && Cvalue.V.contains_non_zero v
+
+ let extract_scalar_lval state lval typ loc =
+ let process_one_loc = eval_one_loc state lval typ in
+ let acc = Cvalue.V.bottom, None in
+ let value, alarms = Precise_locs.fold process_one_loc loc acc in
+ let alarms = match alarms with None -> Alarmset.none | Some a -> a in
+ (* The origin is set to false when the value stored in the memory has not
+ the same type as the read lvalue. In this case, we don't update the state
+ with the new value stemming from the evaluation, even if it has been
+ reduced, in order to not propagate incompatible type. *)
+ let incompatible_type = is_float value <> Cil.isFloatingType typ in
+ let origin = if incompatible_type then Some value else None in
+ let value = Cvalue_forward.reinterpret typ value in
+ if Cvalue.V.is_bottom value
+ then `Bottom, alarms
+ else `Value (value, origin), alarms
+
+ (* Imprecise version for aggregate types that cvalues are unable to precisely
+ represent. The initialization alarms must remain sound, though. *)
+ let extract_aggregate_lval state lval _typ ploc =
+ let loc = Precise_locs.imprecise_location ploc in
+ match loc.Locations.size with
+ | Int_Base.Top -> `Value (Cvalue.V.top, None), Alarmset.all
+ | Int_Base.Value size ->
+ let offsm = Cvalue.Model.copy_offsetmap loc.Locations.loc size state in
+ match offsm with
+ | `Bottom -> `Bottom, Alarmset.none
+ | `Value offsm ->
+ let value = Cvalue.V_Offsetmap.find_imprecise_everywhere offsm in
+ let alarms = indeterminate_alarms lval value in
+ let v = Cvalue.V_Or_Uninitialized.get_v value in
+ let v = if Cvalue.V.is_bottom v then `Bottom else `Value (v, None) in
+ v, alarms
+
+ let extract_lval ~oracle:_ _context state lval typ loc =
+ if Cil.isArithmeticOrPointerType typ
+ then extract_scalar_lval state lval typ loc
+ else extract_aggregate_lval state lval typ loc
+
+ let backward_location state _lval typ precise_loc value =
+ let size = Precise_locs.loc_size precise_loc in
+ let upto = succ (Int_set.get_small_cardinal()) in
+ let loc = Precise_locs.imprecise_location precise_loc in
+ let eval_one_loc single_loc =
+ let v = Cvalue.Model.find state single_loc in
+ let v = Cvalue_forward.make_volatile ~typ v in
+ Cvalue_forward.reinterpret typ v
+ in
+ let process_ival base ival (acc_loc, acc_val as acc) =
+ let loc_bits = Locations.Location_Bits.inject base ival in
+ let single_loc = Locations.make_loc loc_bits size in
+ let v = eval_one_loc single_loc in
+ if Cvalue.V.intersects v value
+ then Locations.Location_Bits.join loc_bits acc_loc, Cvalue.V.join v acc_val
+ else acc
+ in
+ let fold_ival base ival acc =
+ if Ival.cardinal_is_less_than ival upto
+ then Ival.fold_enum (process_ival base) ival acc
+ else process_ival base ival acc
+ in
+ let fold_location loc acc =
+ try
+ let loc = loc.Locations.loc in
+ Locations.Location_Bits.fold_i fold_ival loc acc
+ with
+ Abstract_interp.Error_Top -> loc.Locations.loc, value
+ in
+ let acc = Locations.Location_Bits.bottom, Cvalue.V.bottom in
+ let loc_bits, value = fold_location loc acc in
+ if Locations.Location_Bits.is_bottom loc_bits
+ then `Bottom
+ else
+ let loc = Precise_locs.inject_location_bits loc_bits in
+ `Value (Precise_locs.make_precise_loc loc ~size, value)
+
+ let reduce_further _state _expr _value = []
+end
+
+include Queries
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.mli b/src/plugins/eva/domains/cvalue/cvalue_queries.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a15f0c6ff5912a11eb5f94c176c0f2ccb85474a6
--- /dev/null
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.mli
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+include Abstract_domain.Queries
+ with type state = Cvalue.Model.t
+ and type value = Main_values.CVal.t
+ and type location = Main_locations.PLoc.location
+ and type origin = Main_values.CVal.t
diff --git a/src/plugins/eva/domains/cvalue/locals_scoping.ml b/src/plugins/eva/domains/cvalue/locals_scoping.ml
index ce41844e798d31a73797da73a637810395c92398..2e263ae8d1f369514c6351153e9628b3e8b0bc62 100644
--- a/src/plugins/eva/domains/cvalue/locals_scoping.ml
+++ b/src/plugins/eva/domains/cvalue/locals_scoping.ml
@@ -27,9 +27,9 @@ type clobbered_set = {
mutable clob: Base.SetLattice.t
}
-let structural_descr =
+let packed_descr =
let open Structural_descr in
- t_record [| Base.SetLattice.packed_descr |]
+ pack (t_record [| Base.SetLattice.packed_descr |])
let bottom () = { clob = Base.SetLattice.bottom }
let top () = { clob = Base.SetLattice.top }
diff --git a/src/plugins/eva/domains/cvalue/locals_scoping.mli b/src/plugins/eva/domains/cvalue/locals_scoping.mli
index 274e3ea64d0991b14b936e847a82cbeaec21750f..abaf168a64d782eb7106b29bde409b2099d48271 100644
--- a/src/plugins/eva/domains/cvalue/locals_scoping.mli
+++ b/src/plugins/eva/domains/cvalue/locals_scoping.mli
@@ -30,7 +30,7 @@ type clobbered_set = {
mutable clob: Base.SetLattice.t
}
-val structural_descr: Structural_descr.t
+val packed_descr: Structural_descr.pack
val bottom: unit -> clobbered_set
val top: unit -> clobbered_set