[ivette/eva] output rank of probes

ivette/api/generated/plugins/eva/values/index.ts

@@ -92,12 +92,13 @@ export const getStmtInfo: Server.GetRequest<
 
 const getProbeInfo_internal: Server.GetRequest<
   marker,
-  { code?: string, stmt?: Json.key<'#stmt'> }
+  { rank: number, code?: string, stmt?: Json.key<'#stmt'> }
   > = {
   kind: Server.RqKind.GET,
   name:   'plugins.eva.values.getProbeInfo',
   input:  jMarker,
   output: Json.jObject({
+            rank: Json.jFail(Json.jNumber,'Number expected'),
             code: Json.jString,
             stmt: Json.jKey<'#stmt'>('#stmt'),
           }),
@@ -105,7 +106,7 @@ const getProbeInfo_internal: Server.GetRequest<
 /** Probe informations */
 export const getProbeInfo: Server.GetRequest<
   marker,
-  { code?: string, stmt?: Json.key<'#stmt'> }
+  { rank: number, code?: string, stmt?: Json.key<'#stmt'> }
   >= getProbeInfo_internal;
 
 const getValues_internal: Server.GetRequest<

ivette/src/frama-c/eva/Values.tsx

@@ -33,16 +33,18 @@ interface ProbePanelProps {
   transient?: boolean;
   label?: string;
   code?: string;
+  stmt?: string;
   onPersistent?: callback;
   onTransient?: callback;
 }
 
 function ProbePanel(props: ProbePanelProps) {
-  const { transient = false, label, code } = props;
+  const { transient = false, label, code, stmt } = props;
   return code ? (
     <Hpack className="eva-probe">
       <Label className="eva-probe-label">{label && `${label}:`}</Label>
       <Code className="eva-probe-code">{code}</Code>
+      <Code className="eva-probe-stmt">{stmt}</Code>
       <IconButton
         kind={transient ? 'positive' : 'negative'}
         icon={transient ? 'CIRC.PLUS' : 'CIRC.CLOSE'}
@@ -114,6 +116,8 @@ function ValuesComponent() {
   const makeWindow = (size: Size) => (
     <ValuesPanel vstate={vstate} {...size} />
   );
+  const rank = probe?.rank;
+  const stmt = rank ? `@S${rank}` : undefined;
   return (
     <>
       <TitleBar />
@@ -122,6 +126,7 @@ function ValuesComponent() {
           transient={probe?.transient}
           label={probe?.label}
           code={probe?.code}
+          stmt={stmt}
           onPersistent={probe?.setPersistent}
           onTransient={probe?.setTransient}
         />

ivette/src/frama-c/eva/style.css

@@ -20,3 +20,10 @@
     padding-right: 6px;
     border-radius: 4px;
 }
+
+.eva-probe-stmt {
+    color: grey;
+    margin-left: 0px;
+    margin-right: 2px;
+    margin-top: 3px;
+}

ivette/src/frama-c/eva/vmodel.ts

@@ -80,13 +80,14 @@ function newLabel() {
 export class Probe implements StateCallbacks {
 
   // properties
-  marker: Readonly<string>;
+  readonly marker: string;
   forceUpdate: callback;
   forceLayout: callback;
   transient = true;
   label?: string;
   code?: string;
   stmt?: string;
+  rank?: number;
 
   constructor(marker: string, state: StateCallbacks) {
     this.marker = marker;
@@ -100,9 +101,10 @@ export class Probe implements StateCallbacks {
   requestProbeInfo() {
     Server
       .send(Values.getProbeInfo, this.marker)
-      .then(({ code, stmt }) => {
+      .then(({ code, stmt, rank }) => {
         this.code = code;
         this.stmt = stmt;
+        this.rank = rank;
       })
       .catch(() => {
         this.code = '(error)';

src/plugins/value/api/values_request.ml

@@ -106,7 +106,8 @@ struct
   class ranker =
     object(self)
       inherit Visitor.frama_c_inplace
-
+      (* ranks really starts at 1 *)
+      (* rank < 0 means not computed yet *)
       val mutable rank = (-1)
       val rmap = Smap.create 0
       val fmark = Kmap.create 0
@@ -136,23 +137,26 @@ struct
         ignore (self#newrank s) ;
         Cil.DoChildren
 
+      method flush =
+        while not (Queue.is_empty fqueue) do
+          let kf = Queue.pop fqueue in
+          ignore (Visitor.(visitFramacKf (self :> frama_c_visitor) kf))
+        done
+
       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
+        | kf , _ -> self#call kf ; self#flush
         | 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
+        with Not_found ->
+          let kf = Kernel_function.find_englobing_kf s in
+          self#call kf ;
+          self#flush ;
+          try Smap.find rmap s
+          with Not_found -> self#newrank s
 
     end
 
@@ -358,11 +362,11 @@ let () = Request.register ~package
 
 let pretty fmt cs =
   match cs with
-    | (_, Kstmt _) :: callers ->
-      Value_types.Callstack.pretty_hash fmt cs;
-      Pretty_utils.pp_flowlist ~left:"@[" ~sep:" ←@ " ~right:"@]"
-        (fun fmt (kf, _) -> Kernel_function.pretty fmt kf) fmt callers
-    | _ -> ()
+  | (_, Kstmt _) :: callers ->
+    Value_types.Callstack.pretty_hash fmt cs;
+    Pretty_utils.pp_flowlist ~left:"@[" ~sep:" ←@ " ~right:"@]"
+      (fun fmt (kf, _) -> Kernel_function.pretty fmt kf) fmt callers
+  | _ -> ()
 
 let () =
   let getCallstackInfo = Request.signature
@@ -374,12 +378,12 @@ let () =
       ~descr:(Md.plain "Callers site, from last to first")
       (module Jlist(Jcallsite)) in
   Request.register_sig ~package getCallstackInfo
-      ~kind:`GET ~name:"getCallstackInfo"
-      ~descr:(Md.plain "Callstack Description")
-      begin fun rq cs ->
-        set_calls rq cs ;
-        set_descr rq (Pretty_utils.to_string pretty cs) ;
-      end
+    ~kind:`GET ~name:"getCallstackInfo"
+    ~descr:(Md.plain "Callstack Description")
+    begin fun rq cs ->
+      set_calls rq cs ;
+      set_descr rq (Pretty_utils.to_string pretty cs) ;
+    end
 
 (* -------------------------------------------------------------------------- *)
 (* --- Request getStmtInfo                                                --- *)
@@ -413,6 +417,9 @@ let () =
   let set_code = Request.result_opt getProbeInfo
       ~name:"code" ~descr:(Md.plain "Probe source code")
       (module Jstring) in
+  let set_rank = Request.result getProbeInfo
+      ~name:"rank" ~descr:(Md.plain "Probe statement rank")
+      ~default:0 (module Jint) in
   let pp_code rq pp x = set_code rq (Some (Pretty_utils.to_string pp x)) in
   Request.register_sig ~package ~kind:`GET getProbeInfo
     ~name:"getProbeInfo" ~descr:(Md.plain "Probe informations")
@@ -421,9 +428,11 @@ let () =
       | Plval(l,s) ->
         pp_code rq Printer.pp_lval l ;
         set_stmt rq (Some s) ;
+        set_rank rq (Ranking.stmt s) ;
       | Pexpr(e,s) ->
         pp_code rq Printer.pp_exp e ;
         set_stmt rq (Some s) ;
+        set_rank rq (Ranking.stmt s) ;
       | Pnone -> ()
     end