[Eva] api: Add evaluation of callee directly from call statements

src/plugins/value/Eva.mli

@@ -79,7 +79,15 @@ module Results: sig
   
   val eval_address : Cil_types.lval -> request -> address evaluation
   
-  val eval_callee : Cil_types.exp -> request -> Cil_types.kernel_function list result (* Ignores non-function values; exp must come from Cil Call constructor and are restricted to lvalues with no offset *)
+  (* Returns the kernel functions into which the given expression may evaluate.
+     If the callee expression doesn't always evaluate to a function, those
+     spurious values are ignored. If it always evaluate to a non-function value
+     then the returned list is empty.
+     Raises [Stdlib.Invalid_argument] if the callee expression is not an lvalue
+     without offset.
+     Also see [callee] for a function which applies directly on Call
+     statements *)
+  val eval_callee : Cil_types.exp -> request -> Kernel_function.t list result
   
   (* Value conversion *)
   val as_int : value evaluation -> int result
@@ -103,11 +111,19 @@ module Results: sig
   val is_called : Cil_types.kernel_function -> bool (* called during the analysis, not by the actual program *)
   val is_reachable : Cil_types.stmt -> bool (* reachable by the analysis, not by the actual program *)
   
-  (* Callers / callsites *)
+  (* Callers / Callees / Callsites *)
   val callers : Cil_types.kernel_function -> Cil_types.kernel_function list
   val callsites : Cil_types.kernel_function -> Cil_types.stmt list
   val callsites_per_caller : Cil_types.kernel_function ->
-      (Cil_types.kernel_function * Cil_types.stmt list) list
+    (Cil_types.kernel_function * Cil_types.stmt list) list
+  
+  (* Returns the kernel functions called in the given statement.
+     If the callee expression doesn't always evaluate to a function, those
+     spurious values are ignored. If it always evaluate to a non-function value
+     then the returned list is empty.
+     Raises [Stdlib.Invalid_argument] if the statement is not a [Call]
+     instruction or a [Local_init] with [ConsInit] initializer. *)
+  val callee : Cil_types.stmt -> Kernel_function.t list
 end
 
 module Value_results: sig

src/plugins/value/utils/results.ml

@@ -376,7 +376,9 @@ struct
       let r,_alarms = A.Eval.eval_function_exp exp state in
       r >>>-: List.map fst
     in
-    get req |> Response.map_join' extract join |> convert
+    get req |> Response.map_join' extract join |> convert |>
+    Result.map (List.sort_uniq Kernel_function.compare)
+
 
   (* Conversion *)
 
@@ -429,7 +431,7 @@ struct
     let response_loc, lv = extract_loc res in
     let is_const_lv = Value_util.is_const_write_invalid (Cil.typeOfLval lv) in
     (* No write effect if [lv] is const *)
-    if access=Locations.Write && is_const_lv 
+    if access=Locations.Write && is_const_lv
     then Result.ok Locations.Zone.bottom
     else
       match A.Loc.get Main_locations.PLoc.key with
@@ -620,9 +622,27 @@ let eval_address lval req =
     end : Lvaluation)
 
 let eval_callee exp req =
+  (* Check the validity of exp *)
+  begin match exp with
+    | Cil_types.({ enode = Lval (_, NoOffset) }) -> ()
+    | _ ->
+      invalid_arg "The callee must be an lvalue with no offset"
+  end;
   let module M = Make () in
   M.eval_callee exp req
 
+let callee stmt =
+  let callee_exp =
+    match stmt.Cil_types.skind with
+    | Instr (Call (_lval, callee_exp, _args, _loc)) ->
+      callee_exp
+    | Instr (Local_init (_vi, ConsInit (f, _, _), _loc)) ->
+      Cil.evar f
+    | _ ->
+      invalid_arg "Can only evaluate the callee on a statement which is a Call"
+  in
+  before stmt |> eval_callee callee_exp |> Result.value ~default:[]
+
 (* Value conversion *)
 
 let as_cvalue (Value evaluation) =
@@ -733,7 +753,7 @@ let callsites_per_caller kf =
   let module Map = Kernel_function.Map in
   let f acc = function
     | [] | (_,Cil_types.Kglobal) :: _ -> acc
-    | (kf,Kstmt stmt) :: _-> 
+    | (kf,Kstmt stmt) :: _->
       Map.update kf (fun old -> Some (stmt :: Option.value ~default:[] old)) acc
   in
   at_start_of kf |> callstacks |>

src/plugins/value/utils/results.mli

@@ -82,7 +82,15 @@ val eval_exp : Cil_types.exp -> request -> value evaluation
 
 val eval_address : Cil_types.lval -> request -> address evaluation
 
-val eval_callee : Cil_types.exp -> request -> Cil_types.kernel_function list result (* Ignores non-function values; exp must come from Cil Call constructor and are restricted to lvalues with no offset *)
+(* Returns the kernel functions into which the given expression may evaluate.
+   If the callee expression doesn't always evaluate to a function, those
+   spurious values are ignored. If it always evaluate to a non-function value
+   then the returned list is empty.
+   Raises [Stdlib.Invalid_argument] if the callee expression is not an lvalue
+   without offset.
+   Also see [callee] for a function which applies directly on Call
+   statements *)
+val eval_callee : Cil_types.exp -> request -> Kernel_function.t list result
 
 (* Value conversion *)
 val as_int : value evaluation -> int result
@@ -106,9 +114,17 @@ val is_bottom : 'a evaluation -> bool
 val is_called : Cil_types.kernel_function -> bool (* called during the analysis, not by the actual program *)
 val is_reachable : Cil_types.stmt -> bool (* reachable by the analysis, not by the actual program *)
 
-(* Callers / callsites *)
+(* Callers / Callees / Callsites *)
 val callers : Cil_types.kernel_function -> Cil_types.kernel_function list
 val callsites : Cil_types.kernel_function -> Cil_types.stmt list
 val callsites_per_caller : Cil_types.kernel_function ->
-    (Cil_types.kernel_function * Cil_types.stmt list) list
+  (Cil_types.kernel_function * Cil_types.stmt list) list
+
+(* Returns the kernel functions called in the given statement.
+   If the callee expression doesn't always evaluate to a function, those
+   spurious values are ignored. If it always evaluate to a non-function value
+   then the returned list is empty.
+   Raises [Stdlib.Invalid_argument] if the statement is not a [Call]
+   instruction or a [Local_init] with [ConsInit] initializer. *)
+val callee : Cil_types.stmt -> Kernel_function.t list
 [@@@ api_end]