<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.S

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

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

  val compute_post :
    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 ->
    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.S with module CFG = Scheduler.CFG) = struct

  module CFG = Scheduler.CFG
  module InvariantMap = ProcCfg.NodeIdMap (CFG)
  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 =
    try Some (InvariantMap.find node_id inv_map)
    with Not_found -> 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 = CFG.id node in
    let update_inv_map pre visit_count =
      let compute_post (pre, inv_map) (instr, id_opt) =
        let post = TransferFunctions.exec_instr pre proc_data node instr in
        match id_opt with
        | Some id -> post, InvariantMap.add id { pre; post; visit_count; } inv_map
        | None -> post, inv_map in
      (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *)
      let instr_ids = match CFG.instr_ids node with
        | [] -> [Sil.skip_instr, None]
        | l -> l in
      let astate_post, inv_map_post = IList.fold_left compute_post (pre, inv_map) instr_ids in
      let inv_map'' =
        InvariantMap.add node_id { pre; post=astate_post; visit_count; } inv_map_post in
      inv_map'', Scheduler.schedule_succs work_queue node in
    if InvariantMap.mem node_id inv_map<commit_msg>[absint] support HTML debug output<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.S

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

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

  val compute_post :
    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 ->
    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.S with module CFG = Scheduler.CFG) = struct

  module CFG = Scheduler.CFG
  module InvariantMap = ProcCfg.NodeIdMap (CFG)
  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 =
    try Some (InvariantMap.find node_id inv_map)
    with Not_found -> 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 = CFG.id node in
    let update_inv_map pre visit_count =
      let compute_post (pre, inv_map) (instr, id_opt) =
        let post = TransferFunctions.exec_instr pre proc_data node instr in
        match id_opt with
        | Some id -> post, InvariantMap.add id { pre; post; visit_count; } inv_map
        | None -> post, inv_map in
      (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *)
      let instr_ids = match CFG.instr_ids node with
        | [] -> [Sil.skip_instr, None]
        | l -> l in
      let underlying_node = CFG.underlying_node node in
      NodePrinter.start_session underlying_node;
      let astate_post, inv_map_post = IList.fold_left compute_post (pre, inv_map) instr_ids in
      if Config.write_html
      then
        begin
          let str =
            let instrs = IList.map fst instr_ids in
            Format.asprintf "PRE: %a@.INSTRS: %aPOST: %a@."
              Domain.pp pre (Sil.pp_instr_list Pp.text) instrs Domain.pp astate_post in
          L.d_strln str
        end;
      NodePrinter.finish_session underlying_node;
      let inv_map'' =
        InvariantMap.add node_id { pre; post=astate_post; visit_count; } inv_map_post in
      inv_map'', Scheduler.schedule_succs work_queue node in
    if InvariantMap.mem node_id inv_map
{'fraction_non_alphanumeric': 0.07838827838827839, 'fraction_numerical': 0.0011721611721611722, 'mean_word_length': 3.218788627935723, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 47, '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': '5404719', 'n_tokens_mistral': 2106, 'n_tokens_neox': 2047, 'n_words': 684}