<commit_before>(*
 * Copyright (c) 2016 - present Facebook, Inc.
 * All rights reserved.
 *
 * This source code is licensed under the BSD style license found in the
 * LICENSE file in the root directory of this source tree. An additional grant
 * of patent rights can be found in the PATENTS file in the same directory.
 *)

open! IStd
module L = Logging

type 'a state = {pre: 'a; post: 'a; visit_count: int}

module type S = sig
  module TransferFunctions : TransferFunctions.SIL

  module InvariantMap : Caml.Map.S with type key = TransferFunctions.CFG.id

  type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t

  val compute_post :
    ?debug:bool -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate
    -> TransferFunctions.Domain.astate option

  val exec_cfg :
    TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t
    -> initial:TransferFunctions.Domain.astate -> debug:bool -> invariant_map

  val exec_pdesc :
    TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map

  val extract_post : InvariantMap.key -> 'a state InvariantMap.t -> 'a option

  val extract_pre : InvariantMap.key -> 'a state InvariantMap.t -> 'a option

  val extract_state : InvariantMap.key -> 'a InvariantMap.t -> 'a option
end

module MakeNoCFG
    (Scheduler : Scheduler.S)
    (TransferFunctions : TransferFunctions.SIL with module CFG = Scheduler.CFG) =
struct
  module CFG = Scheduler.CFG
  module InvariantMap = CFG.IdMap
  module TransferFunctions = TransferFunctions
  module Domain = TransferFunctions.Domain

  type invariant_map = Domain.astate state InvariantMap.t

  (** extract the state of node [n] from [inv_map] *)
  let extract_state node_id inv_map = InvariantMap.find_opt node_id inv_map

  (** extract the postcondition of node [n] from [inv_map] *)
  let extract_post node_id inv_map =
    match extract_state node_id inv_map with Some state -> Some state.post | None -> None


  (** extract the precondition of node [n] from [inv_map] *)
  let extract_pre node_id inv_map =
    match extract_state node_id inv_map with Some state -> Some state.pre | None -> None


  let exec_node node astate_pre work_queue inv_map ({ProcData.pdesc} as proc_data) ~debug =
    let node_id = CFG.id node in
    let update_inv_map pre ~visit_count =
      let compute_post pre instr = TransferFunctions.exec_instr pre proc_data node instr in
      (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *)
      let instrs = match CFG.instrs node with [] -> [Sil.skip_instr] | l -> l in
      if debug then
        NodePrinter.start_session
          ~pp_name:(TransferFunctions.pp_session_name node)
          (CFG.underlying_node node) ;
      let astate_post = List.fold ~f:compute_post ~init:pre instrs in
      if debug then (
        L.d_strln
          (Format.asprintf "PRE: %a@.INSTRS: %aPOST: %a@." Domain.pp pre
             (Sil.pp_instr_list Pp.(html Green))
             instrs Domain.pp astate_post) ;
        NodePrinter.finish_session (CFG.underlying_node node) ) ;
      let inv_map' = InvariantMap.add node_id {pre; post= astate_post; visit_count} inv_map in
      (inv_map', Scheduler.schedule_succs work_queue node)
    in
    if InvariantMap.mem node_id inv_map then (
      let old_state = InvariantMap.find node_id inv_map in
      let widened_pre =
        if CFG.is_loop_head pdesc node then
          Domain.widen ~prev:old_state.pre ~next:astate_pre ~num_iters:old_state.visit_count
        else astate_pre
      in
      if Domain.( <= ) ~lhs:widened_pre ~rhs:old_state.pre then (inv_map, work_queue)
      else
        let visit_count' = old_state.visit_count + 1 in
        if visit_count' > Config.max_widens then
          L.(die InternalError)
            "Exceeded max widening threshold %d while analyzing %a. Please check your widening \
             operator or increase the threshold"
            Config.max_widens Typ.Procname.pp (Procdesc.get_proc_name pdesc) ;
        update_inv_map widened_pre ~visit_count:visit_count' )
    else (* first time visiting this node *)
      update_inv_map astate_pre ~visit_count:1


  let rec exec_worklist cfg work_queue inv_map proc_data ~debug =
    let compute_pre node inv_map =
      let extract_post_ pred = extract_post (CFG.id pred) inv_map in
      let all_posts = List.map ~f:extract_post_ (CFG.preds cfg node) in
      match List.filter_opt all_posts with
      | post :: posts ->
          Some (List.fold ~f:Domain.join ~init:post posts)
      | [] ->
          None
    in
    match Scheduler.pop work_queue with
    | Some (_, [], work_queue') ->
        exec_worklist cfg work_queue' inv_map proc_data ~debug
    | Some (node, _, work_queue') ->
        let inv_map_post, work_queue_post =
          match compute_pre node inv_map with
          | Some astate_pre ->
              exec_node node astate_pre work_queue' inv_map proc_data ~debug
          | None ->
              (inv_map, work_queue')
        in
        exec_worklist cfg work_queue_post inv_map_post proc_data ~debug
    | None ->
        inv_map<commit_msg>AbstractInterpreter: less garbage<commit_after>(*
 * Copyright (c) 2016 - present Facebook, Inc.
 * All rights reserved.
 *
 * This source code is licensed under the BSD style license found in the
 * LICENSE file in the root directory of this source tree. An additional grant
 * of patent rights can be found in the PATENTS file in the same directory.
 *)

open! IStd
module L = Logging

type 'a state = {pre: 'a; post: 'a; visit_count: int}

module type S = sig
  module TransferFunctions : TransferFunctions.SIL

  module InvariantMap : Caml.Map.S with type key = TransferFunctions.CFG.id

  type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t

  val compute_post :
    ?debug:bool -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate
    -> TransferFunctions.Domain.astate option

  val exec_cfg :
    TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t
    -> initial:TransferFunctions.Domain.astate -> debug:bool -> invariant_map

  val exec_pdesc :
    TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map

  val extract_post : InvariantMap.key -> 'a state InvariantMap.t -> 'a option

  val extract_pre : InvariantMap.key -> 'a state InvariantMap.t -> 'a option

  val extract_state : InvariantMap.key -> 'a InvariantMap.t -> 'a option
end

module MakeNoCFG
    (Scheduler : Scheduler.S)
    (TransferFunctions : TransferFunctions.SIL with module CFG = Scheduler.CFG) =
struct
  module CFG = Scheduler.CFG
  module InvariantMap = CFG.IdMap
  module TransferFunctions = TransferFunctions
  module Domain = TransferFunctions.Domain

  type invariant_map = Domain.astate state InvariantMap.t

  (** extract the state of node [n] from [inv_map] *)
  let extract_state node_id inv_map = InvariantMap.find_opt node_id inv_map

  (** extract the postcondition of node [n] from [inv_map] *)
  let extract_post node_id inv_map =
    match extract_state node_id inv_map with Some state -> Some state.post | None -> None


  (** extract the precondition of node [n] from [inv_map] *)
  let extract_pre node_id inv_map =
    match extract_state node_id inv_map with Some state -> Some state.pre | None -> None


  let exec_node node astate_pre work_queue inv_map ({ProcData.pdesc} as proc_data) ~debug =
    let node_id = CFG.id node in
    let update_inv_map pre ~visit_count =
      let compute_post pre instr = TransferFunctions.exec_instr pre proc_data node instr in
      (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *)
      let instrs = match CFG.instrs node with [] -> [Sil.skip_instr] | l -> l in
      if debug then
        NodePrinter.start_session
          ~pp_name:(TransferFunctions.pp_session_name node)
          (CFG.underlying_node node) ;
      let astate_post = List.fold ~f:compute_post ~init:pre instrs in
      if debug then (
        L.d_strln
          (Format.asprintf "PRE: %a@.INSTRS: %aPOST: %a@." Domain.pp pre
             (Sil.pp_instr_list Pp.(html Green))
             instrs Domain.pp astate_post) ;
        NodePrinter.finish_session (CFG.underlying_node node) ) ;
      let inv_map' = InvariantMap.add node_id {pre; post= astate_post; visit_count} inv_map in
      (inv_map', Scheduler.schedule_succs work_queue node)
    in
    if InvariantMap.mem node_id inv_map then (
      let old_state = InvariantMap.find node_id inv_map in
      let widened_pre =
        if CFG.is_loop_head pdesc node then
          Domain.widen ~prev:old_state.pre ~next:astate_pre ~num_iters:old_state.visit_count
        else astate_pre
      in
      if Domain.( <= ) ~lhs:widened_pre ~rhs:old_state.pre then (inv_map, work_queue)
      else
        let visit_count' = old_state.visit_count + 1 in
        if visit_count' > Config.max_widens then
          L.(die InternalError)
            "Exceeded max widening threshold %d while analyzing %a. Please check your widening \
             operator or increase the threshold"
            Config.max_widens Typ.Procname.pp (Procdesc.get_proc_name pdesc) ;
        update_inv_map widened_pre ~visit_count:visit_count' )
    else (* first time visiting this node *)
      update_inv_map astate_pre ~visit_count:1


  let rec exec_worklist cfg work_queue inv_map proc_data ~debug =
    let compute_pre node inv_map =
      let extract_post_ pred = extract_post (CFG.id pred) inv_map in
      CFG.preds cfg node
      |> List.fold ~init:None ~f:(fun joined_post_opt pred ->
             match extract_post_ pred with
             | None ->
                 joined_post_opt
             | Some post as some_post ->
               match joined_post_opt with
               | None ->
                   some_post
               | Some joined_post ->
                   Some (Domain.join joined_post post) )
    in
    match Scheduler.pop work_queue with
    | Some (_, [], work_queue') ->
        exec_worklist cfg work_queue' inv_map proc_data ~debug
    | Some (node, _, work_queue') ->
        let inv_map_post, work_queue_post =
          match compute_pre node inv_map with
          | Some astate_pre ->
              exec_node node astate_pre work_queue' inv_map proc_data ~debug
          | None ->
              (inv_map, work_queue')
        in
        exec_worklist cfg work_queue_post inv_map_post proc_data ~debug
    | None ->
        inv_map
{'fraction_non_alphanumeric': 0.07751642700695172, 'fraction_numerical': 0.001142748309684792, 'mean_word_length': 2.9157345264727814, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 65, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2964226', 'n_tokens_mistral': 3221, 'n_tokens_neox': 3137, 'n_words': 980}