<commit_before>(** An analyzer that takes the CFG from [MyCFG], a solver from [Selector], constraints from [Constraints] (using the specification from [MCP]) *)

open Prelude
open Cil
open MyCFG
open Pretty
open Analyses
open GobConfig
open Constraints

module type S2S = functor (X : Spec) -> Spec
(* gets Spec for current options *)
let get_spec () : (module Spec) =
  let open Batteries in
  (* apply functor F on module X if opt is true *)
  let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
  (module (val
            (module MCP.MCP2 : Spec)
            |> lift (get_bool "exp.widen-context" && get_bool "exp.full-context") (module WidenContextLifter)
            |> lift (get_bool "exp.widen-context" && neg get_bool "exp.full-context") (module WidenContextLifterSide)
            |> lift true (module PathSensitive2)
            |> lift (get_bool "ana.hashcons") (module HashconsLifter)
            |> lift true (module DeadCodeLifter)
            |> lift (get_bool "dbg.slice.on") (module LevelSliceLifter)
            |> lift (get_int "dbg.limit.widen" > 0) (module LimitLifter)
          ))

(** Given a [Cfg], computes the solution to [MCP.Path] *)
module AnalyzeCFG (Cfg:CfgBidir) =
struct

  (** The main function to preform the selected analyses. *)
  let analyze (file: file) (startfuns, exitfuns, otherfuns: Analyses.fundecs)  (module Spec : Spec) =
    (** The Equation system *)
    let module EQSys = FromSpec (Spec) (Cfg) in

    (** Hashtbl for locals *)
    let module LHT   = BatHashtbl.Make (EQSys.LVar) in
    (** Hashtbl for globals *)
    let module GHT   = BatHashtbl.Make (EQSys.GVar) in

    (** The solver *)
    let module Slvr  = Selector.Make (EQSys) (LHT) (GHT) in
    (** The verifyer *)
    let module Vrfyr = Verify2 (EQSys) (LHT) (GHT) in
    (** The comparator *)
    let module Comp = Compare (Spec) (EQSys) (LHT) (GHT) in

    (** Triple of the function, context, and the local value. *)
    let module RT = Analyses.ResultType2 (Spec) in
    (** Set of triples [RT] *)
    let module LT = SetDomain.HeadlessSet (RT) in
    (** Analysis result structure---a hashtable from program points to [LT] *)
    let module Result = Analyses.Result (LT) (struct let result_name = "analysis" end) in

    (** print out information about dead code *)
    let print_dead_code (xs:Result.t) =
      let dead_locations : unit Deadcode.Locmap.t = Deadcode.Locmap.create 10 in
      let module NH = Hashtbl.Make (MyCFG.Node) in
      let live_nodes : unit NH.t = NH.create 10 in
      let count = ref 0 in
      let module StringMap = BatMap.Make (String) in
      let open BatMap in let open BatPrintf in
      let live_lines = ref StringMap.empty in
      let dead_lines = ref StringMap.empty in
      let add_one (l,n,f) v =
        let add_fun  = BatISet.add l.line in
        let add_file = StringMap.modify_def BatISet.empty f.svar.vname add_fun in
        if LT.for_all (fun (_,x,f) -> Spec.D.is_bot x) v then begin
          dead_lines := StringMap.modify_def StringMap.empty l.file add_file !dead_lines;
          Deadcode.Locmap.add dead_locations l ()
        end else begin
          live_lines := StringMap.modify_def StringMap.empty l.file add_file !live_lines;
          NH.add live_nodes n ()
        end;
      in
      Result.iter add_one xs;
      let live file fn =
        try StringMap.find fn (StringMap.find file !live_lines)
        with Not_found -> BatISet.empty
      in
      dead_lines := StringMap.mapi (fun fi -> StringMap.mapi (fun fu ded -> BatISet.diff ded (live fi fu))) !dead_lines;
      dead_lines := StringMap.map (StringMap.filter (fun _ x -> not (BatISet.is_empty x))) !dead_lines;
      dead_lines := StringMap.filter (fun _ x -> not (StringMap.is_empty x)) !dead_lines;
      let print_func f xs =
        let one_range b e first =
          count := !count + (e - b + 1);
          if not first then printf ", ";
          begin if b=e then
              printf "%d" b
            else
              printf "%d..%d" b e
          end; false
        in
        printf "  function '%s' has dead code on lines: " f;
        ignore (BatISet.fold_range one_range xs true);
        printf "\n"
      in
      let print_file f =
        printf "File '%s':\n" f;
        StringMap.iter print_func
      in
      if StringMap.is_empty !dead_lines
      then printf "No dead code found!\n"
      else begin
        StringMap.iter print_file !dead_lines;
        printf "Found dead code on %d line%s!\n" !count (if !count>1 then "s" else "")
      end;
      let str = function true -> "then" | false -> "else" in
      let report tv loc dead =
        if Deadcode.Locmap.mem dead_locations loc then
          match dead, Deadcode.Locmap.find_option Deadcode.dead_branches_cond loc with
          | true, Some exp -> ignore (Pretty.printf "Dead code: the %s branch over expression '%a' is dead! (%a)\n" (str tv) d_exp exp d_loc loc)
          | true, None     -> ignore (Pretty.printf "Dead code: an %s branch is dead! (%a)\n" (str tv) d_loc loc)
          | _ -> ()
      in
      if get_bool "dbg.print_dead_code" then begin
        Deadcode.Locmap.iter (report true)  Deadcode.dead_branches_then;
        Deadcode.Locmap.iter (report false) Deadcode.dead_branches_else;
        Deadcode.Locmap.clear Deadcode.dead_branches_then;
        Deadcode.Locmap.clear Deadcode.dead_branches_else
      end;
      NH.mem live_nodes
    in

    (** convert result that can be out-put *)
    let solver2source_result h : Result.t =
      (* processed result *)
      let res = Result.create 113 in

      (* Adding the state at each system variable to the final result *)
      let add_local_var (n,es) state =
        let loc = MyCFG.getLoc n in
        if loc <> locUnknown then try
            let (_,_, fundec) as p = loc, n, MyCFG.getFun n in
            if Result.mem res p then
              (* If this source location has been added before, we look it up
               * and add another node to it information to it. *)
              let prev = Result.find res p in
              Result.replace res p (LT.add (es,state,fundec) prev)
            else
              Result.add res p (LT.singleton (es,state,fundec))
          (* If the function is not defined, and yet has been included to the
           * analysis result, we generate a warning. *)
          with Not_found -> Messages.warn ("Undefined function has escaped.")
      in
      LHT.iter add_local_var h;
      res
    in

    (** exctract global xml from result *)
    let make_global_xml g =
      let one_glob k v =
        let k = Xml.PCData k.vname in
        let varname = Xml.Element ("td",[],[k]) in
        let varvalue = Xml.Element ("td",[],[Spec.G.toXML v]) in
        Xml.Element ("tr",[],[varname; varvalue])
      in
      let head =
        Xml.Element ("tr",[],[Xml.Element ("th",[],[Xml.PCData "var"])
                             ;Xml.Element ("th",[],[Xml.PCData "value"])])
      in
      let collect_globals k v b = one_glob k v :: b in
      Xml.Element ("table", [], head :: GHT.fold collect_globals g [])
    in
    (** exctract global xml from result *)
    let make_global_fast_xml f g =
      let open Printf in<commit_msg>clearer message when there is state for undefined functions<commit_after>(** An analyzer that takes the CFG from [MyCFG], a solver from [Selector], constraints from [Constraints] (using the specification from [MCP]) *)

open Prelude
open Cil
open MyCFG
open Pretty
open Analyses
open GobConfig
open Constraints

module type S2S = functor (X : Spec) -> Spec
(* gets Spec for current options *)
let get_spec () : (module Spec) =
  let open Batteries in
  (* apply functor F on module X if opt is true *)
  let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
  (module (val
            (module MCP.MCP2 : Spec)
            |> lift (get_bool "exp.widen-context" && get_bool "exp.full-context") (module WidenContextLifter)
            |> lift (get_bool "exp.widen-context" && neg get_bool "exp.full-context") (module WidenContextLifterSide)
            |> lift true (module PathSensitive2)
            |> lift (get_bool "ana.hashcons") (module HashconsLifter)
            |> lift true (module DeadCodeLifter)
            |> lift (get_bool "dbg.slice.on") (module LevelSliceLifter)
            |> lift (get_int "dbg.limit.widen" > 0) (module LimitLifter)
          ))

(** Given a [Cfg], computes the solution to [MCP.Path] *)
module AnalyzeCFG (Cfg:CfgBidir) =
struct

  (** The main function to preform the selected analyses. *)
  let analyze (file: file) (startfuns, exitfuns, otherfuns: Analyses.fundecs)  (module Spec : Spec) =
    (** The Equation system *)
    let module EQSys = FromSpec (Spec) (Cfg) in

    (** Hashtbl for locals *)
    let module LHT   = BatHashtbl.Make (EQSys.LVar) in
    (** Hashtbl for globals *)
    let module GHT   = BatHashtbl.Make (EQSys.GVar) in

    (** The solver *)
    let module Slvr  = Selector.Make (EQSys) (LHT) (GHT) in
    (** The verifyer *)
    let module Vrfyr = Verify2 (EQSys) (LHT) (GHT) in
    (** The comparator *)
    let module Comp = Compare (Spec) (EQSys) (LHT) (GHT) in

    (** Triple of the function, context, and the local value. *)
    let module RT = Analyses.ResultType2 (Spec) in
    (** Set of triples [RT] *)
    let module LT = SetDomain.HeadlessSet (RT) in
    (** Analysis result structure---a hashtable from program points to [LT] *)
    let module Result = Analyses.Result (LT) (struct let result_name = "analysis" end) in

    (** print out information about dead code *)
    let print_dead_code (xs:Result.t) =
      let dead_locations : unit Deadcode.Locmap.t = Deadcode.Locmap.create 10 in
      let module NH = Hashtbl.Make (MyCFG.Node) in
      let live_nodes : unit NH.t = NH.create 10 in
      let count = ref 0 in
      let module StringMap = BatMap.Make (String) in
      let open BatMap in let open BatPrintf in
      let live_lines = ref StringMap.empty in
      let dead_lines = ref StringMap.empty in
      let add_one (l,n,f) v =
        let add_fun  = BatISet.add l.line in
        let add_file = StringMap.modify_def BatISet.empty f.svar.vname add_fun in
        if LT.for_all (fun (_,x,f) -> Spec.D.is_bot x) v then begin
          dead_lines := StringMap.modify_def StringMap.empty l.file add_file !dead_lines;
          Deadcode.Locmap.add dead_locations l ()
        end else begin
          live_lines := StringMap.modify_def StringMap.empty l.file add_file !live_lines;
          NH.add live_nodes n ()
        end;
      in
      Result.iter add_one xs;
      let live file fn =
        try StringMap.find fn (StringMap.find file !live_lines)
        with Not_found -> BatISet.empty
      in
      dead_lines := StringMap.mapi (fun fi -> StringMap.mapi (fun fu ded -> BatISet.diff ded (live fi fu))) !dead_lines;
      dead_lines := StringMap.map (StringMap.filter (fun _ x -> not (BatISet.is_empty x))) !dead_lines;
      dead_lines := StringMap.filter (fun _ x -> not (StringMap.is_empty x)) !dead_lines;
      let print_func f xs =
        let one_range b e first =
          count := !count + (e - b + 1);
          if not first then printf ", ";
          begin if b=e then
              printf "%d" b
            else
              printf "%d..%d" b e
          end; false
        in
        printf "  function '%s' has dead code on lines: " f;
        ignore (BatISet.fold_range one_range xs true);
        printf "\n"
      in
      let print_file f =
        printf "File '%s':\n" f;
        StringMap.iter print_func
      in
      if StringMap.is_empty !dead_lines
      then printf "No dead code found!\n"
      else begin
        StringMap.iter print_file !dead_lines;
        printf "Found dead code on %d line%s!\n" !count (if !count>1 then "s" else "")
      end;
      let str = function true -> "then" | false -> "else" in
      let report tv loc dead =
        if Deadcode.Locmap.mem dead_locations loc then
          match dead, Deadcode.Locmap.find_option Deadcode.dead_branches_cond loc with
          | true, Some exp -> ignore (Pretty.printf "Dead code: the %s branch over expression '%a' is dead! (%a)\n" (str tv) d_exp exp d_loc loc)
          | true, None     -> ignore (Pretty.printf "Dead code: an %s branch is dead! (%a)\n" (str tv) d_loc loc)
          | _ -> ()
      in
      if get_bool "dbg.print_dead_code" then begin
        Deadcode.Locmap.iter (report true)  Deadcode.dead_branches_then;
        Deadcode.Locmap.iter (report false) Deadcode.dead_branches_else;
        Deadcode.Locmap.clear Deadcode.dead_branches_then;
        Deadcode.Locmap.clear Deadcode.dead_branches_else
      end;
      NH.mem live_nodes
    in

    (** convert result that can be out-put *)
    let solver2source_result h : Result.t =
      (* processed result *)
      let res = Result.create 113 in

      (* Adding the state at each system variable to the final result *)
      let add_local_var (n,es) state =
        let loc = MyCFG.getLoc n in
        if loc <> locUnknown then try
            let (_,_, fundec) as p = loc, n, MyCFG.getFun n in
            if Result.mem res p then
              (* If this source location has been added before, we look it up
               * and add another node to it information to it. *)
              let prev = Result.find res p in
              Result.replace res p (LT.add (es,state,fundec) prev)
            else
              Result.add res p (LT.singleton (es,state,fundec))
          (* If the function is not defined, and yet has been included to the
           * analysis result, we generate a warning. *)
          with Not_found ->
            Messages.warn ("Calculated state for undefined function: unexpected node "^Ana.sprint MyCFG.pretty_node n)
      in
      LHT.iter add_local_var h;
      res
    in

    (** exctract global xml from result *)
    let make_global_xml g =
      let one_glob k v =
        let k = Xml.PCData k.vname in
        let varname = Xml.Element ("td",[],[k]) in
        let varvalue = Xml.Element ("td",[],[Spec.G.toXML v]) in
        Xml.Element ("tr",[],[varname; varvalue])
      in
      let head =
        Xml.Element ("tr",[],[Xml.Element ("th",[],[Xml.PCData "var"])
                             ;Xml.Element ("th",[],[Xml.PCData "value"])])
      in
      let collect_globals k v b = one_glob k v :: b in
      Xml.Element ("table", [], head :: GHT.fold collect_globals g [])
    in
    (** exctract global xml from result *)
    let make_global_fast_xml f g =
      let open Printf in
{'fraction_non_alphanumeric': 0.10533159947984395, 'fraction_numerical': 0.002463897063855999, 'mean_word_length': 2.3452380952380953, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 49, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 8}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2193949', 'n_tokens_mistral': 4642, 'n_tokens_neox': 4487, 'n_words': 1599}