diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index 986e4339faf65d14376ebf79b6294ca1d3274a4a..1a6c222f453e37b83ba79221374ae50fb8c55b6d 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -24,6 +24,11 @@ open Server
open Data
open Cil_types
+module Kmap = Kernel_function.Hashtbl
+module Smap = Cil_datatype.Stmt.Hashtbl
+module CS = Value_types.Callstack
+module CSmap = CS.Hashtbl
+
module Md = Markdown
module Jkf = Kernel_ast.Kf
module Jki = Kernel_ast.Ki
@@ -87,15 +92,119 @@ let probe marker =
| _ -> Pnone
(* -------------------------------------------------------------------------- *)
-(* --- Domain Utilities --- *)
+(* --- Stmt Ranking --- *)
(* -------------------------------------------------------------------------- *)
-module CS = Value_types.Callstack
-module CSmap = CS.Hashtbl
+module Ranking :
+sig
+ val stmt : stmt -> int
+ val kinstr : kinstr -> int
+ val sort : callstack list -> callstack list
+end =
+struct
+
+ class ranker =
+ object(self)
+ inherit Visitor.frama_c_inplace
+
+ val mutable rank = (-1)
+ val rmap = Smap.create 0
+ val fmark = Kmap.create 0
+ val fqueue = Queue.create ()
+
+ method private call kf =
+ if not (Kmap.mem fmark kf) then
+ begin
+ Kmap.add fmark kf () ;
+ Queue.push kf fqueue ;
+ end
+
+ method private newrank s =
+ let r = succ rank in
+ Smap.add rmap s r ;
+ rank <- r ; r
+
+ method! vlval lv =
+ begin
+ try match fst lv with
+ | Var vi -> self#call (Globals.Functions.get vi)
+ | _ -> ()
+ with Not_found -> ()
+ end ; Cil.DoChildren
+
+ method! vstmt_aux s =
+ ignore (self#newrank s) ;
+ Cil.DoChildren
+
+ method compute =
+ match Globals.entry_point () with
+ | kf , _ ->
+ let job kf =
+ ignore (Visitor.(visitFramacKf (self :> frama_c_visitor) kf))
+ in begin
+ job kf ;
+ while not (Queue.is_empty fqueue) do
+ job (Queue.pop fqueue)
+ done
+ end
+ | exception Globals.No_such_entry_point _ -> ()
+
+ method rank s =
+ if rank < 0 then (rank <- 0 ; self#compute) ;
+ try Smap.find rmap s
+ with Not_found -> self#newrank s
+
+ end
+
+ let stmt = let rk = new ranker in rk#rank
+
+ let kinstr = function
+ | Kglobal -> 0
+ | Kstmt s -> stmt s
+
+ let rec ranks (rks : int list) (cs : callstack) : int list =
+ match cs with
+ | [] -> rks
+ | (_,Kglobal)::wcs -> ranks rks wcs
+ | (_,Kstmt s)::wcs -> ranks (stmt s :: rks) wcs
+
+ let order : int list -> int list -> int = Stdlib.compare
+
+ let sort (wcs : callstack list) : callstack list =
+ List.map fst @@
+ List.sort (fun (_,rp) (_,rq) -> order rp rq) @@
+ List.map (fun cs -> cs , ranks [] cs) wcs
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Domain Utilities --- *)
+(* -------------------------------------------------------------------------- *)
module Jcallstack = Data.Index(Value_types.Callstack.Map)
(struct let name = "eva-callstack-id" end)
+module Jcallsite : Data.S with type t = Value_types.call_site =
+struct
+ type t = kernel_function * kinstr
+ let jtype = Package.(Jrecord [
+ "fct" , Jkf.jtype ;
+ "stmt" , Jki.jtype ;
+ "rank" , Jnumber ;
+ ])
+ let to_json (kf,ki) = `Assoc [
+ "fct" , Jkf.to_json kf ;
+ "stmt" , Jki.to_json ki ;
+ "rank" , Jint.to_json (Ranking.kinstr ki) ;
+ ]
+ let of_json = function
+ | `Assoc fds ->
+ let kf = Jkf.of_json (List.assoc "fct" fds) in
+ let ki = Jki.of_json (List.assoc "stmt" fds) in
+ (kf,ki)
+ | _ -> failwith "Not a call-site"
+end
+
module Jtruth : Data.S with type t = truth =
struct
type t = truth
@@ -238,7 +347,10 @@ let () = Request.register ~package
~descr:(Md.plain "Callstacks for markers")
~input:(module Jstmt)
~output:(module Jlist(Jcallstack))
- (fun stmt -> let module A = (val !proxy) in A.callstacks stmt)
+ begin fun stmt ->
+ let module A = (val !proxy) in
+ Ranking.sort (A.callstacks stmt)
+ end
(* -------------------------------------------------------------------------- *)
(* --- Request getCallstackInfo --- *)
@@ -260,7 +372,7 @@ let () =
(module Jstring) in
let set_calls = Request.result getCallstackInfo ~name:"calls"
~descr:(Md.plain "Callers site, from last to first")
- (module Jlist(Jpair(Jkf)(Jki))) in
+ (module Jlist(Jcallsite)) in
Request.register_sig ~package getCallstackInfo
~kind:`GET ~name:"getCallstackInfo"
~descr:(Md.plain "Callstack Description")
@@ -269,6 +381,26 @@ let () =
set_descr rq (Pretty_utils.to_string pretty cs) ;
end
+(* -------------------------------------------------------------------------- *)
+(* --- Request getStmtInfo --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () =
+ let getStmtInfo = Request.signature ~input:(module Jstmt) () in
+ let set_fct = Request.result getStmtInfo ~name:"fct"
+ ~descr:(Md.plain "Englobing function")
+ (module Jkf) in
+ let set_rank = Request.result getStmtInfo ~name:"rank"
+ ~descr:(Md.plain "Global stmt order")
+ (module Jint) in
+ Request.register_sig ~package getStmtInfo
+ ~kind:`GET ~name:"getStmtInfo"
+ ~descr:(Md.plain "Stmt Information")
+ begin fun rq s ->
+ set_fct rq (Kernel_function.find_englobing_kf s) ;
+ set_rank rq (Ranking.stmt s) ;
+ end
+
(* -------------------------------------------------------------------------- *)
(* --- Request getProbeInfo --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/value_types/value_types.mli b/src/plugins/value_types/value_types.mli
index 99589861241eeb1e280acc5f5abee60270ee4f0e..cdd8f86c51b15e072ea718a42cf62740ba5e5143 100644
--- a/src/plugins/value_types/value_types.mli
+++ b/src/plugins/value_types/value_types.mli
@@ -27,8 +27,23 @@ open Cil_types
(* TODO: These types are already defined in Value_util. *)
type call_site = kernel_function * kinstr
+(** Value call-site.
+ A callsite [(f,p)] represents a call at function [f] invoked
+ {i from} program point [p].
+*)
+
type callstack = call_site list
-(** Value callstacks, as used e.g. in Db.Value hooks *)
+(** Value callstacks, as used e.g. in Db.Value hooks.
+
+ The head call site [(f,p)] is the most recent one,
+ where current function [f] has been called from program point [p].
+
+ Therefore, the tail call site is expected to be [(main,Kglobal)]
+ where [main] is the global entry point.
+
+ Moreover, given two consecutive call-sites […(_,p);(g,_)…] in a callstack,
+ program point [p] is then expected to live in function [g].
+ *)
module Callsite: Datatype.S_with_collections with type t = call_site
module Callstack: sig