[Eva] New requests for unreachable and non terminating statements in a function.

src/plugins/value/api/general_requests.ml

@@ -21,6 +21,7 @@
 (**************************************************************************)
 
 open Server
+open Cil_types
 
 let package =
   Package.package
@@ -30,6 +31,13 @@ let package =
     ~readme:"eva.md"
     ()
 
+let is_computed kf =
+  Db.Value.is_computed () &&
+  match kf with
+  | { fundec = Definition (fundec, _) } ->
+    Mark_noresults.should_memorize_function fundec
+  | { fundec = Declaration _ } -> false
+
 module CallSite = Data.Jpair (Kernel_ast.Kf) (Kernel_ast.Stmt)
 
 let callers kf =
@@ -42,4 +50,67 @@ let () = Request.register ~package
     ~input:(module Kernel_ast.Kf) ~output:(module Data.Jlist (CallSite))
     callers
 
+
+(* ----- Dead code: unreachable and non-terminating statements -------------- *)
+
+type dead_code =
+  { kf: Kernel_function.t;
+    unreachable : stmt list;
+    non_terminating : stmt list; }
+
+module DeadCode = struct
+  open Server.Data
+
+  type record
+  let record : record Record.signature = Record.signature ()
+
+  let unreachable = Record.field record ~name:"unreachable"
+      ~descr:(Markdown.plain "List of unreachable statements.")
+      (module Data.Jlist (Kernel_ast.Marker))
+  let non_terminating = Record.field record ~name:"nonTerminating"
+      ~descr:(Markdown.plain "List of reachable but non terminating statements.")
+      (module Data.Jlist (Kernel_ast.Marker))
+
+  let data = Record.publish record ~package ~name:"deadCode"
+      ~descr:(Markdown.plain "Unreachable and non terminating statements.")
+
+  module R : Record.S with type r = record = (val data)
+  type t = dead_code
+  let jtype = R.jtype
+
+  let to_json (dead_code) =
+    let make_unreachable stmt = Printer_tag.PStmt (dead_code.kf, stmt)
+    and make_non_term stmt = Printer_tag.PStmtStart (dead_code.kf, stmt) in
+    R.default |>
+    R.set unreachable (List.map make_unreachable dead_code.unreachable) |>
+    R.set non_terminating (List.map make_non_term dead_code.non_terminating) |>
+    R.to_json
+end
+
+let dead_code kf =
+  let empty = { kf; unreachable = []; non_terminating = [] } in
+  if is_computed kf then
+    let module Results = (val Analysis.current_analyzer ()) in
+    let is_unreachable ~after stmt =
+      Results.get_stmt_state ~after stmt = `Bottom
+    in
+    let classify acc stmt =
+      if is_unreachable ~after:false stmt
+      then { acc with unreachable = stmt :: acc.unreachable }
+      else if is_unreachable ~after:true stmt
+      then { acc with non_terminating = stmt :: acc.non_terminating }
+      else acc
+    in
+    let fundec = Kernel_function.get_definition kf in
+    List.fold_left classify empty fundec.sallstmts
+  else empty
+
+let () = Request.register ~package
+    ~kind:`GET ~name:"getDeadCode"
+    ~descr:(Markdown.plain "Get the lists of unreachable and of non terminating \
+                            statements in a function")
+    ~input:(module Kernel_ast.Kf)
+    ~output:(module DeadCode)
+    dead_code
+
 (**************************************************************************)