<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! Utils

module L = Logging

module Make
    (C : ProcCfg.Wrapper)
    (Sched : Scheduler.S)
    (A : AbstractDomain.S)
    (T : TransferFunctions.S with type astate = A.astate) = struct

  module S = Sched (C)
  module M = ProcCfg.NodeIdMap (C)

  type state = { pre: A.astate; post: A.astate; visit_count: int; }
  (* invariant map from node id -> abstract state representing postcondition for node id *)
  type inv_map = state M.t

  (** extract the state of node [n] from [inv_map] *)
  let extract_state node_id inv_map =
    try
      Some (M.find node_id inv_map)
    with Not_found ->
      L.err "Warning: No state found for node %a" C.pp_node_id node_id;
      None

  (** 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 proc_data =
    let exec_instrs astate_acc instr =
      if A.is_bottom astate_acc
      then astate_acc
      else T.exec_instr astate_acc proc_data instr in
    let node_id = C.node_id node in
    L.out "Doing analysis of node %a from pre %a@." C.pp_node_id node_id A.pp astate_pre;
    let instrs = C.instrs node in
    let astate_post =
      IList.fold_left exec_instrs astate_pre instrs in
    L.out "Post for node %a is %a@." C.pp_node_id node_id A.pp astate_post;
    if M.mem node_id inv_map then
      let old_state = M.find node_id inv_map in
      let widened_post =
        A.widen ~prev:old_state.post ~next:astate_post ~num_iters:old_state.visit_count in
      if A.(<=) ~lhs:widened_post ~rhs:old_state.post
      then
        begin
          L.out "Old state contains new, not adding succs@.";
          inv_map, work_queue
        end
      else
        begin
          L.out "Widening: %a <widen> %a = %a@."
            A.pp astate_post A.pp old_state.post A.pp widened_post;
          let inv_map' =
            let visit_count = old_state.visit_count + 1 in
            M.add node_id { pre=astate_pre; post=widened_post; visit_count; } inv_map in
          inv_map', S.schedule_succs work_queue node
        end
    else
      (* first time visiting this node *)
      let inv_map' =
        let visit_count = 0 in
        M.add node_id { pre=astate_pre; post=astate_post; visit_count; } inv_map in
      inv_map', S.schedule_succs work_queue node

  let rec exec_worklist cfg work_queue inv_map proc_data =
    let compute_pre node inv_map =
      (* if the [pred] -> [node] transition was normal, use post([pred]) *)
      let extract_post_ pred = extract_post (C.node_id pred) inv_map in
      let normal_posts = IList.map extract_post_ (C.normal_preds cfg node) in
      (* if the [pred] -> [node] transition was exceptional, use pre([pred]) *)
      let extract_pre_f acc pred = extract_pre (C.node_id pred) inv_map :: acc in
      let all_posts = IList.fold_left extract_pre_f normal_posts (C.exceptional_preds cfg node) in
      match IList.flatten_options all_posts with<commit_msg>widen at pre instead of at post<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! Utils

module L = Logging

module Make
    (C : ProcCfg.Wrapper)
    (Sched : Scheduler.S)
    (A : AbstractDomain.S)
    (T : TransferFunctions.S with type astate = A.astate) = struct

  module S = Sched (C)
  module M = ProcCfg.NodeIdMap (C)

  type state = { pre: A.astate; post: A.astate; visit_count: int; }
  (* invariant map from node id -> abstract state representing postcondition for node id *)
  type inv_map = state M.t

  (** extract the state of node [n] from [inv_map] *)
  let extract_state node_id inv_map =
    try
      Some (M.find node_id inv_map)
    with Not_found ->
      L.err "Warning: No state found for node %a" C.pp_node_id node_id;
      None

  (** 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 proc_data =
    let node_id = C.node_id node in
    L.out "Doing analysis of node %a from pre %a@." C.pp_node_id node_id A.pp astate_pre;
    let update_inv_map astate_pre visit_count =
      let astate_post =
        let exec_instrs astate_acc instr =
          if A.is_bottom astate_acc
          then astate_acc
          else T.exec_instr astate_acc proc_data instr in
        IList.fold_left exec_instrs astate_pre (C.instrs node) in
      L.out "Post for node %a is %a@." C.pp_node_id node_id A.pp astate_post;
      let inv_map' = M.add node_id { pre=astate_pre; post=astate_post; visit_count; } inv_map in
      inv_map', S.schedule_succs work_queue node in
    if M.mem node_id inv_map then
      let old_state = M.find node_id inv_map in
      let widened_pre =
        A.widen ~prev:old_state.pre ~next:astate_pre ~num_iters:old_state.visit_count in
      if A.(<=) ~lhs:widened_pre ~rhs:old_state.pre
      then
        begin
          L.out "Old state contains new, not updating invariant or scheduling succs@.";
          inv_map, work_queue
        end
      else
        begin
          L.out "Widening: %a <widen> %a = %a@."
            A.pp astate_pre A.pp old_state.post A.pp widened_pre;
          update_inv_map widened_pre (old_state.visit_count + 1)
        end
    else
      (* first time visiting this node *)
      let visit_count = 1 in
      update_inv_map astate_pre visit_count

  let rec exec_worklist cfg work_queue inv_map proc_data =
    let compute_pre node inv_map =
      (* if the [pred] -> [node] transition was normal, use post([pred]) *)
      let extract_post_ pred = extract_post (C.node_id pred) inv_map in
      let normal_posts = IList.map extract_post_ (C.normal_preds cfg node) in
      (* if the [pred] -> [node] transition was exceptional, use pre([pred]) *)
      let extract_pre_f acc pred = extract_pre (C.node_id pred) inv_map :: acc in
      let all_posts = IList.fold_left extract_pre_f normal_posts (C.exceptional_preds cfg node) in
      match IList.flatten_options all_posts with
{'fraction_non_alphanumeric': 0.08013544018058691, 'fraction_numerical': 0.001693002257336343, 'mean_word_length': 2.8112903225806454, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 21, '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': '7137891', 'n_tokens_mistral': 2356, 'n_tokens_neox': 2310, 'n_words': 798}