[Eva] Removes a bunch of unused functions from Db.Value.

src/kernel_services/plugin_entry_points/db.ml

@@ -319,20 +319,6 @@ module Value = struct
       ((i land mask_then) <> 0, (i land mask_else) <> 0)
     with Not_found -> false, false
 
-  module RecursiveCallsFound =
-    State_builder.Set_ref
-      (Kernel_function.Set)
-      (struct
-        let name = "Db.Value.RecursiveCallsFound"
-        let dependencies = only_self
-      end)
-
-  let ignored_recursive_call kf =
-    RecursiveCallsFound.mem kf
-
-  let recursive_call_occurred kf =
-    RecursiveCallsFound.add kf
-
   module Called_Functions_By_Callstack =
     State_builder.Hashtbl(Kernel_function.Hashtbl)
       (States_by_callstack)
@@ -433,8 +419,6 @@ module Value = struct
     try Some (Called_Functions_By_Callstack.find kf)
     with Not_found -> None
 
-  let valid_behaviors = mk_fun "Value.get_valid_behaviors"
-
   let get_fundec_from_stmt stmt =
     let kf =
       try
@@ -530,16 +514,6 @@ module Value = struct
   let is_called = mk_fun "Value.is_called"
   let callers = mk_fun "Value.callers"
 
-  let access_location = mk_fun "Value.access_location"
-
-  let find state loc = Cvalue.Model.find state loc
-
-  let access =  mk_fun "Value.access"
-  let access_expr =  mk_fun "Value.access_expr"
-
-  let use_spec_instead_of_definition =
-    mk_fun "Value.use_spec_instead_of_definition"
-
   let eval_lval =
     ref (fun ?with_alarms:_ _ -> mk_labeled_fun "Value.eval_lval")
   let eval_expr =
@@ -552,29 +526,8 @@ module Value = struct
 
   let find_lv_plus = mk_fun "Value.find_lv_plus"
 
-  let pretty_state = Cvalue.Model.pretty
-
-  let pretty = Cvalue.V.pretty
-
   let compute = mk_fun "Value.compute"
 
-  let memoize = mk_fun "Value.memoize"
-  let expr_to_kernel_function = mk_fun "Value.expr_to_kernel_function"
-  let expr_to_kernel_function_state =
-    mk_fun "Value.expr_to_kernel_function_state"
-
-  exception Not_a_call
-
-  let call_to_kernel_function call_stmt = match call_stmt.skind with
-    | Instr (Call (_, fexp, _, _)) ->
-      let _, called_functions =
-        !expr_to_kernel_function ?with_alarms:None ~deps:None
-          (Kstmt call_stmt) fexp
-      in called_functions
-    | Instr(Local_init(_, ConsInit(f,_,_),_)) ->
-      Kernel_function.Hptset.singleton (Globals.Functions.get f)
-    | _ -> raise Not_a_call
-
 
   let lval_to_loc_with_deps = mk_fun "Value.lval_to_loc_with_deps"
   let lval_to_loc_with_deps_state = mk_fun "Value.lval_to_loc_with_deps_state"
@@ -590,31 +543,6 @@ module Value = struct
   let lval_to_precise_loc_with_deps_state =
     mk_fun "Value.lval_to_precise_loc_with_deps_state"
 
-
-  exception Void_Function
-
-  let find_return_loc kf =
-    try
-      let ki = Kernel_function.find_return kf in
-      let lval = match ki with
-        | { skind = Return (Some ({enode = Lval ((_ , offset) as lval)}), _) }
-          ->
-          assert (offset = NoOffset) ;
-          lval
-        | { skind = Return (None, _) } -> raise Void_Function
-        | _ -> assert false
-      in
-      !lval_to_loc (Kstmt ki) ?with_alarms:None lval
-    with Kernel_function.No_Statement ->
-      (* [JS 2011/05/17] should be better to have another name for this
-         exception or another one since it is possible to have no return without
-         returning void (the case when the kf corresponds to a declaration *)
-      raise Void_Function
-
-  let display = mk_fun "Value.display"
-
-  let emitter = ref Emitter.dummy
-
 end
 
 (* ************************************************************************* *)

src/kernel_services/plugin_entry_points/db.mli

@@ -109,9 +109,6 @@ module Value : sig
   type t = Cvalue.V.t
   (** Internal representation of a value. *)
 
-  val emitter: Emitter.t ref
-  (** Emitter used by Value to emit statuses *)
-
   val proxy: State_builder.Proxy.t
 
   val self : State.t
@@ -151,23 +148,11 @@ module Value : sig
       of each reachable and evaluable statement. Filled only if
       [Value_parameters.ResultsAfter] is set. *)
 
-  val ignored_recursive_call: kernel_function -> bool
-  (** This functions returns true if the value analysis found and ignored
-      a recursive call to this function during the analysis. *)
-
   val condition_truth_value: stmt -> bool * bool
   (** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
       (resp. snd) is true if and only if the condition of the 'if' has been
       evaluated to true (resp. false) at least once during the analysis. *)
 
-  (** {3 Parameterization} *)
-
-  val use_spec_instead_of_definition: (kernel_function -> bool) ref
-  (** To be called by derived analyses to determine if they must use
-      the body of the function (if available), or only its spec. Used for
-      value builtins, and option -val-use-spec. *)
-
-
   (** {4 Arguments of the main function} *)
 
   (** The functions below are related to the arguments that are passed to the
@@ -237,8 +222,6 @@ module Value : sig
   val fold_state_callstack :
     (state -> 'a -> 'a) -> 'a -> after:bool -> kinstr -> 'a
 
-  val find : state -> Locations.location ->  t
-
   (** {3 Evaluations} *)
 
   val eval_lval :
@@ -263,28 +246,6 @@ module Value : sig
   (** returns the list of all decompositions of [expr] into the sum an lvalue
       and an interval. *)
 
-  (** {3 Values and kernel functions} *)
-
-  val expr_to_kernel_function :
-    (kinstr
-     -> ?with_alarms:CilE.warn_mode
-     -> deps:Locations.Zone.t option
-     -> exp
-     -> Locations.Zone.t * Kernel_function.Hptset.t) ref
-
-  val expr_to_kernel_function_state :
-    (state
-     -> deps:Locations.Zone.t option
-     -> exp
-     -> Locations.Zone.t * Kernel_function.Hptset.t) ref
-
-  exception Not_a_call
-  val call_to_kernel_function : stmt -> Kernel_function.Hptset.t
-  (** Return the functions that can be called from this call.
-      @raise Not_a_call if the statement is not a call. *)
-
-  val valid_behaviors: (kernel_function -> state -> funbehavior list) ref
-
   (** {3 Reachability} *)
 
   val is_accessible : kinstr -> bool
@@ -295,23 +256,12 @@ module Value : sig
 
   (** {3 About kernel functions} *)
 
-  exception Void_Function
-  val find_return_loc : kernel_function -> Locations.location
-  (** Return the location of the returned lvalue of the given function.
-      @raise Void_Function if the function does not return any value. *)
-
   val is_called: (kernel_function -> bool) ref
 
   val callers: (kernel_function -> (kernel_function*stmt list) list) ref
   (** @return the list of callers with their call sites. Each function is
       present only once in the list. *)
 
-  (** {3 State before a kinstr} *)
-
-  val access : (kinstr -> lval ->  t) ref
-  val access_expr : (kinstr -> exp ->  t) ref
-  val access_location : (kinstr -> Locations.location ->  t) ref
-
 
   (** {3 Locations of left values} *)
 
@@ -380,15 +330,6 @@ module Value : sig
      reference here to avoid a cyclic dependency. *)
   val rm_asserts: (unit -> unit) ref
 
-
-  (** {3 Pretty printing} *)
-
-  val pretty : Format.formatter -> t -> unit
-  val pretty_state : Format.formatter -> state -> unit
-
-
-  val display : (Format.formatter -> kernel_function -> unit) ref
-
   (**/**)
   (** {3 Internal use only} *)
 
@@ -396,8 +337,6 @@ module Value : sig
   (** To be used during the value analysis itself (instead of
       {!get_state}). [after] is false by default. *)
 
-  val recursive_call_occurred: kernel_function -> unit
-
   val merge_conditions: int Cil_datatype.Stmt.Hashtbl.t -> unit
   val mask_then: int
   val mask_else: int
@@ -407,12 +346,6 @@ module Value : sig
   val update_callstack_table: after:bool -> stmt -> callstack -> state -> unit
   (* Merge a new state in the table indexed by callstacks. *)
 
-
-  val memoize : (kernel_function -> unit) ref
-  (*  val compute_call :
-      (kernel_function -> call_kinstr:kinstr -> state ->  (exp*t) list
-         -> Cvalue.V_Offsetmap.t option (** returned value of [kernel_function] *) * state) ref
-  *)
   val merge_initial_state : callstack -> kernel_function -> state -> unit
   (** Store an additional possible initial state for the given callstack as
       well as its values for actuals. *)

src/plugins/eva/domains/cvalue/cvalue_domain.ml

@@ -584,8 +584,6 @@ module State = struct
     then Parameters.ForceValues.output display_results
 end
 
-let () = Db.Value.display := (fun fmt kf -> State.display ~fmt kf)
-
 
 let registered =
   let name = "cvalue"

src/plugins/eva/register.ml

@@ -34,28 +34,9 @@ let main () =
 let () = Db.Main.extend main
 
 
-(* "access" functions before evaluation, registered in Db.Value *)
-let access_value_of_lval kinstr lv =
-  let state = Db.Value.get_state kinstr in
-  snd (!Db.Value.eval_lval None state lv)
-
-let access_value_of_expr kinstr e =
-  let state = Db.Value.get_state kinstr in
-  !Db.Value.eval_expr state e
-
-let access_value_of_location kinstr loc =
-  let state = Db.Value.get_state kinstr in
-  Db.Value.find state loc
-
 let () =
   Db.Value.is_called := Function_calls.is_called;
   Db.Value.callers := Function_calls.callsites;
-  Db.Value.use_spec_instead_of_definition :=
-    Function_calls.use_spec_instead_of_definition;
-  Db.Value.access := access_value_of_lval;
-  Db.Value.access_location := access_value_of_location;
-  Db.Value.access_expr := access_value_of_expr;
-  Db.Value.valid_behaviors := Logic_inout.valid_behaviors;
 
 
   (* -------------------------------------------------------------------------- *)
@@ -342,28 +323,6 @@ module Export (Eval : Eval) = struct
 
   let lval_to_offsetmap_state state lv =
     lval_to_offsetmap_aux state lv
-
-
-  let expr_to_kernel_function_state ?with_alarms state ~deps exp =
-    let r, deps = resolv_func_vinfo ?with_alarms deps state exp in
-    Option.value ~default:Locations.Zone.bottom deps, r
-
-  let expr_to_kernel_function kinstr ?with_alarms ~deps exp =
-    let state_to_joined_kernel_function state (z_acc, kf_acc) =
-      let z, kf =
-        expr_to_kernel_function_state ?with_alarms state ~deps exp
-      in
-      Locations.Zone.join z z_acc,
-      Kernel_function.Hptset.union kf kf_acc
-    in
-    Db.Value.fold_state_callstack
-      state_to_joined_kernel_function
-      ((match deps with None -> Locations.Zone.bottom | Some z -> z),
-       Kernel_function.Hptset.empty)
-      ~after:false kinstr
-
-  let expr_to_kernel_function_state =
-    expr_to_kernel_function_state ?with_alarms:None
 end
 
 
@@ -396,8 +355,6 @@ let register (module Eval: Eval) (module Export: Export) =
     lval_to_precise_loc_with_deps_state;
   Db.Value.lval_to_offsetmap := lval_to_offsetmap;
   Db.Value.lval_to_offsetmap_state := lval_to_offsetmap_state;
-  Db.Value.expr_to_kernel_function := expr_to_kernel_function;
-  Db.Value.expr_to_kernel_function_state := expr_to_kernel_function_state;
   ()
 
 

src/plugins/eva/utils/eva_utils.ml

@@ -79,8 +79,6 @@ let emitter =
     ~correctness:Parameters.parameters_correctness
     ~tuning:Parameters.parameters_tuning
 
-let () = Db.Value.emitter := emitter
-
 let get_slevel kf =
   try Parameters.SlevelFunction.find kf
   with Not_found -> Parameters.SemanticUnrollingLevel.get ()