diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index a574d3a3c4a82d66b9c5c5844dfada3d02dab530..b8b6ee7d87af66a98e082b94a747271b4aafaf24 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-
module type InputDomain = sig
include Abstract_domain.S
val storage: unit -> bool
@@ -252,3 +251,328 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
include Complete (D)
end
+
+(* -------------------------------------------------------------------------- *)
+
+type permission = { read: bool; write: bool; }
+type mode = { current: permission; calls: permission; }
+
+module Mode = struct
+
+ let all =
+ let p = { read = true; write = true } in
+ { current = p; calls = p; }
+
+
+ include Datatype.Make_with_collections
+ (struct
+ include Datatype.Serializable_undefined
+ type t = mode
+ let name = "Domain_builder.Restrict_State"
+ let reprs = [ all ]
+ let compare _ _ = 0
+ let equal _ _ = true
+ let hash _ = 0
+ end)
+
+ let merge f m1 m2 =
+ let merge_perm p1 p2 =
+ { read = f p1.read p2.read;
+ write = f p1.write p2.write; }
+ in
+ { current = merge_perm m1.current m2.current;
+ calls = merge_perm m1.calls m2.calls; }
+
+ let join = merge (&&)
+ let narrow = merge (||)
+end
+
+module Restrict
+ (Value: Abstract_value.S)
+ (Domain: Abstract.Domain.Internal with type value = Value.t)
+ (Scope: sig val functions: (Kernel_function.t * mode) list end)
+= struct
+
+ let functions_map =
+ List.fold_left
+ (fun map (kf, mode) -> Kernel_function.Map.add kf mode map)
+ Kernel_function.Map.empty Scope.functions
+
+ module Info = struct let module_name = Domain.name ^ " restricted" end
+ module D = Datatype.Pair_with_collections (Domain) (Mode) (Info)
+
+ module I = struct let module_name = Domain.name ^ " option" end
+ include Datatype.Option_with_collections (D) (I)
+
+ let default = Domain.top, Mode.all
+ let structure: t Abstract.Domain.structure =
+ Abstract.Domain.(Option ((Node (Domain.structure, Void)), default))
+
+ type state = t
+ type value = Domain.value
+ type location = Domain.location
+ type origin = Domain.origin
+
+ let get_state = function
+ | None -> Domain.top
+ | Some (state, _mode) -> state
+
+ let compute_starting_state () =
+ let empty = Domain.empty () in
+ let var_kind = Abstract_domain.Global in
+ let init varinfo _init state =
+ let state = Domain.enter_scope var_kind [varinfo] state in
+ Domain.initialize_variable_using_type var_kind varinfo state
+ in
+ Globals.Vars.fold init empty
+
+ let get_starting_state =
+ let starting_state = ref None in
+ fun () ->
+ match !starting_state with
+ | None ->
+ let s = compute_starting_state () in
+ starting_state := Some s;
+ s
+ | Some state -> state
+
+ (* ----- Lattice ---------------------------------------------------------- *)
+
+ let top = None
+
+ let is_included x y =
+ match x, y with
+ | _, None -> true
+ | None, _ -> false
+ | Some (d1, _), Some (d2, _) -> Domain.is_included d1 d2
+
+ let make_join join = fun x y ->
+ match x, y with
+ | None, _ | _, None -> None
+ | Some (d1, m1), Some (d2, m2) -> Some (join d1 d2, Mode.join m1 m2)
+
+ let join = make_join Domain.join
+ let widen kf stmt = make_join (Domain.widen kf stmt)
+
+ let narrow x y =
+ match x, y with
+ | None, s | s, None -> `Value s
+ | Some (d1, s1), Some (d2, s2) ->
+ Domain.narrow d1 d2 >>-: fun s ->
+ Some (s, Mode.narrow s1 s2)
+
+ (* ----- Queries ---------------------------------------------------------- *)
+
+ let default_query = `Value (Value.top, None), Alarmset.all
+
+ let make_query default query = function
+ | None -> default
+ | Some (state, mode) ->
+ if mode.current.read
+ then query state
+ else default
+
+ let extract_expr oracle state expr =
+ make_query default_query (fun s -> Domain.extract_expr oracle s expr) state
+
+ let extract_lval oracle state lval typ location =
+ make_query
+ default_query
+ (fun s -> Domain.extract_lval oracle s lval typ location)
+ state
+
+ let backward_location state lval typ location value =
+ make_query
+ (`Value (location, value))
+ (fun s -> Domain.backward_location s lval typ location value)
+ state
+
+ let reduce_further state expr value =
+ make_query [] (fun s -> Domain.reduce_further s expr value) state
+
+ (* ----- Transfer functions ----------------------------------------------- *)
+
+ let make_transfer f = function
+ | None -> `Value None
+ | Some (state, mode) ->
+ if mode.current.write
+ then f state >>-: fun state -> Some (state, mode)
+ else `Value (Some (state, mode))
+
+ let update valuation = make_transfer (Domain.update valuation)
+ let assume stmt expr positive valuation =
+ make_transfer (Domain.assume stmt expr positive valuation)
+
+ let assign kinstr lvalue expr assigned valuation = function
+ | None -> `Value None
+ | Some (state, mode) ->
+ if mode.current.write
+ then
+ Domain.assign kinstr lvalue expr assigned valuation state >>-: fun s ->
+ Some (s, mode)
+ else
+ let state = Domain.logic_assign None lvalue.lloc state in
+ `Value (Some (state, mode))
+
+ let start_analysis call state =
+ let formals = List.map (fun argument -> argument.formal) call.arguments in
+ let kind = Abstract_domain.Formal call.kf in
+ let state = Domain.enter_scope kind formals state in
+ let initialize acc v = Domain.initialize_variable_using_type kind v acc in
+ let state = List.fold_left initialize state formals in
+ state
+
+ let start_call stmt call valuation state =
+ let start_call_with_mode ?previous_mode ~new_mode state =
+ if new_mode.current.write
+ then
+ match previous_mode with
+ | Some mode when mode.current.write ->
+ Domain.start_call stmt call valuation state >>-: fun state ->
+ Some (state, new_mode)
+ | _ ->
+ `Value (Some (start_analysis call state, new_mode))
+ else `Value (Some (state, new_mode))
+ in
+ let called_mode = Kernel_function.Map.find_opt call.kf functions_map in
+ match state, called_mode with
+ | Some (state, previous_mode), Some new_mode ->
+ start_call_with_mode ~previous_mode ~new_mode state
+ | Some (state, previous_mode), None ->
+ let new_mode = { previous_mode with current = previous_mode.calls } in
+ start_call_with_mode ~previous_mode ~new_mode state
+ | None, Some new_mode ->
+ start_call_with_mode ~new_mode (get_starting_state ())
+ | None, None ->
+ `Value None
+
+ let finalize_call stmt call ~pre ~post =
+ match pre, post with
+ | None, _ | _, None -> `Value None
+ | Some (pre, pre_mode), Some (post, post_mode) ->
+ if post_mode.current.write
+ then
+ Domain.finalize_call stmt call ~pre ~post >>-: fun state ->
+ Some (state, pre_mode)
+ else
+ `Value (Some (post, pre_mode))
+
+ let show_expr valuation state fmt expr =
+ match state with
+ | None -> ()
+ | Some (state, _mode) -> Domain.show_expr valuation state fmt expr
+
+ (* ----- Logic evalutation ------------------------------------------------ *)
+
+ let logic_assign assign location = function
+ | None -> None
+ | Some (state, mode) ->
+ let assign =
+ Extlib.opt_map (fun (assign, state) -> assign, get_state state) assign
+ in
+ Some (Domain.logic_assign assign location state, mode)
+
+ let lift_env env =
+ let states label = get_state (env.Abstract_domain.states label) in
+ Abstract_domain.{ env with states = states }
+
+ let evaluate_predicate env state predicate =
+ make_query
+ Alarmset.Unknown
+ (fun s -> Domain.evaluate_predicate (lift_env env) s predicate)
+ state
+
+ let reduce_by_predicate env state predicate positive =
+ make_transfer
+ (fun s -> Domain.reduce_by_predicate (lift_env env) s predicate positive)
+ state
+
+ (* ----- Scoping, initialization & loops ---------------------------------- *)
+
+ let lift f = function
+ | None -> None
+ | Some (state, mode) as x ->
+ if mode.current.write
+ then Some (f state, mode)
+ else x
+
+ let enter_scope kind varinfos = lift (Domain.enter_scope kind varinfos)
+ let leave_scope kf varinfos = lift (Domain.leave_scope kf varinfos)
+
+ let empty () =
+ let main_kf = fst (Globals.entry_point ()) in
+ match Kernel_function.Map.find_opt main_kf functions_map with
+ | None -> None
+ | Some mode -> Some (Domain.empty (), mode)
+
+ let initialize_variable lval location ~initialized init_value =
+ lift (Domain.initialize_variable lval location ~initialized init_value)
+ let initialize_variable_using_type init_kind varinfo =
+ lift (Domain.initialize_variable_using_type init_kind varinfo)
+
+ let enter_loop stmt = lift (Domain.enter_loop stmt)
+ let incr_loop_counter stmt = lift (Domain.incr_loop_counter stmt)
+ let leave_loop stmt = lift (Domain.leave_loop stmt)
+
+ (* ----- MemExec ---------------------------------------------------------- *)
+
+ let relate kf bases = function
+ | None -> Base.SetLattice.empty
+ | Some (state, _mode) -> Domain.relate kf bases state
+
+ let filter kf kind bases = function
+ | None -> None
+ | Some (state, mode) -> Some (Domain.filter kf kind bases state, mode)
+
+ let reuse kf bases ~current_input ~previous_output =
+ match current_input, previous_output with
+ | None, _ | _, None -> None
+ | Some (current_input, mode), Some (previous_output, _) ->
+ Some (Domain.reuse kf bases ~current_input ~previous_output, mode)
+
+ let log_category = Domain.log_category
+
+ let post_analysis state =
+ let state = state >>-: get_state in
+ Domain.post_analysis state
+
+ (* ----- Storage ---------------------------------------------------------- *)
+
+ module Store = struct
+
+ let register_global_state state =
+ let state = state >>-: get_state in
+ Domain.Store.register_global_state state
+
+ let lift_register f state = f (get_state state)
+
+ let register_initial_state callstack =
+ lift_register (Domain.Store.register_initial_state callstack)
+ let register_state_before_stmt callstack stmt =
+ lift_register (Domain.Store.register_state_before_stmt callstack stmt)
+ let register_state_after_stmt callstack stmt =
+ lift_register (Domain.Store.register_state_after_stmt callstack stmt)
+
+ let inject state = Some (state, Mode.all)
+
+ let get_global_state () = Domain.Store.get_global_state () >>-: inject
+ let get_initial_state kf = Domain.Store.get_initial_state kf >>-: inject
+ let get_stmt_state ~after stmt =
+ Domain.Store.get_stmt_state ~after stmt >>-: inject
+
+ let inject_table = function
+ | `Top -> `Top
+ | `Bottom -> `Bottom
+ | `Value t ->
+ let module Hashtbl = Value_types.Callstack.Hashtbl in
+ let table = Hashtbl.create (Hashtbl.length t) in
+ Hashtbl.iter (fun key s -> Hashtbl.add table key (inject s)) t;
+ `Value table
+
+ let get_initial_state_by_callstack kf =
+ inject_table (Domain.Store.get_initial_state_by_callstack kf)
+ let get_stmt_state_by_callstack ~after stmt =
+ inject_table (Domain.Store.get_stmt_state_by_callstack ~after stmt)
+
+ end
+end
diff --git a/src/plugins/value/domains/domain_builder.mli b/src/plugins/value/domains/domain_builder.mli
index b604579e939f7d63075e53eaf5e1bc80e1748c30..f63aa2e6ded7d83ca69f3557686c92cd2e09ce61 100644
--- a/src/plugins/value/domains/domain_builder.mli
+++ b/src/plugins/value/domains/domain_builder.mli
@@ -55,3 +55,18 @@ module Complete_Simple_Cvalue
: Abstract_domain.Leaf with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
and type state = Domain.t
+
+
+type permission = { read: bool; write: bool; }
+type mode = { current: permission; calls: permission; }
+
+module Mode : sig
+ val all: mode
+end
+
+module Restrict
+ (Value: Abstract_value.S)
+ (Domain: Abstract.Domain.Internal with type value = Value.t)
+ (Scope: sig val functions: (Kernel_function.t * mode) list end)
+ : Abstract.Domain.Internal with type value = Value.t
+ and type location = Domain.location