(*
 * 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 F = Format
module L = Logging


module Summary = Summary.Make (struct
    type summary = ThreadSafetyDomain.summary

    let update_payload summary payload =
      { payload with Specs.threadsafety = Some summary }

    let read_from_payload payload =
      payload.Specs.threadsafety
  end)

module TransferFunctions (CFG : ProcCfg.S) = struct
  module CFG = CFG
  module Domain = ThreadSafetyDomain
  type extras = ProcData.no_extras

  type lock_model =
    | Lock
    | Unlock
    | NoEffect

  let get_lock_model = function
    | Procname.Java java_pname ->
        begin
          match Procname.java_get_class_name java_pname, Procname.java_get_method java_pname with
          | "java.util.concurrent.locks.Lock", "lock" ->
              Lock
          | ("java.util.concurrent.locks.ReentrantLock"
            | "java.util.concurrent.locks.ReentrantReadWriteLock$ReadLock"
            | "java.util.concurrent.locks.ReentrantReadWriteLock$WriteLock"),
            ("lock" | "tryLock" | "lockInterruptibly") ->
              Lock
          | ("java.util.concurrent.locks.Lock"
            |"java.util.concurrent.locks.ReentrantLock"
            | "java.util.concurrent.locks.ReentrantReadWriteLock$ReadLock"
            | "java.util.concurrent.locks.ReentrantReadWriteLock$WriteLock"),
            "unlock" ->
              Unlock
          | _ ->
              NoEffect
        end
    | pname when Procname.equal pname BuiltinDecl.__set_locked_attribute ->
        Lock
    | pname when Procname.equal pname BuiltinDecl.__delete_locked_attribute ->
        Unlock
    | _ ->
        NoEffect

  let resolve_id (id_map : IdAccessPathMapDomain.astate) id =
    try Some (IdAccessPathMapDomain.find id id_map)
    with Not_found -> None

  let add_path_to_state exp typ loc path_state id_map owned tenv =
    (* remove the last field of the access path, if it has any *)
    let truncate = function
      | base, []
      | base, _ :: [] -> base, []
      | base, accesses -> base, IList.rev (IList.tl (IList.rev accesses)) in
    let is_thread_confined (_, accesses) = match IList.rev accesses with
      | AccessPath.FieldAccess (fieldname, Typ.Tstruct typename) :: _ ->
          begin
            match Tenv.lookup tenv typename with
            | Some struct_typ ->
                Annotations.field_has_annot fieldname struct_typ Annotations.ia_is_thread_confined
            | None ->
                false
          end
      | _ ->
          false in
    let f_resolve_id = resolve_id id_map in

    IList.fold_left
      (fun acc rawpath ->
         if not (ThreadSafetyDomain.OwnershipDomain.mem (truncate rawpath) owned) &&
            not (is_thread_confined rawpath)
         then
           ThreadSafetyDomain.PathDomain.add_sink (ThreadSafetyDomain.make_access rawpath loc) acc
         else
           acc)
      path_state
      (AccessPath.of_exp exp typ ~f_resolve_id)

  let analyze_id_assignment lhs_id rhs_exp rhs_typ { ThreadSafetyDomain.id_map; } =
    let f_resolve_id = resolve_id id_map in
    match AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id with
    | Some rhs_access_path -> IdAccessPathMapDomain.add lhs_id rhs_access_path id_map
    | None -> id_map

  let exec_instr (astate : Domain.astate) { ProcData.pdesc; tenv; } _ =
    let is_allocation pn =
      Procname.equal pn BuiltinDecl.__new ||
      Procname.equal pn BuiltinDecl.__new_array in
    let is_container_write pn tenv = match pn with
      | Procname.Java java_pname ->
          let typename = Typename.Java.from_string (Procname.java_get_class_name java_pname) in
          let is_container_write_ typename _ =
            match Typename.name typename, Procname.java_get_method java_pname with
            | "java.util.Map", ("clear" | "put" | "putAll" | "remove") -> true
            | _ -> false in
          let is_threadsafe_collection typename _ = match Typename.name typename with
            | "java.util.concurrent.ConcurrentMap" -> true
            | _ -> false in
          PatternMatch.supertype_exists tenv is_container_write_ typename &&
          not (PatternMatch.supertype_exists tenv is_threadsafe_collection typename)
      | _ -> false in
    let add_container_write pn loc exp typ (astate : ThreadSafetyDomain.astate) =
      let dummy_fieldname =
        Ident.create_fieldname (Mangled.from_string (Procname.get_method pn)) 0 in
      let dummy_access_exp = Exp.Lfield (exp, dummy_fieldname, typ) in
      let unconditional_writes =
        add_path_to_state
          dummy_access_exp typ loc astate.unconditional_writes astate.id_map astate.owned tenv in
      { astate with unconditional_writes; } in
    let is_unprotected is_locked =
      not is_locked && not (Procdesc.is_java_synchronized pdesc) in
    let f_resolve_id = resolve_id astate.id_map in

    function
    | Sil.Call (Some (lhs_id, lhs_typ), Const (Cfun pn), _, _, _) when is_allocation pn ->
        begin
          match AccessPath.of_lhs_exp (Exp.Var lhs_id) lhs_typ ~f_resolve_id with
          | Some lhs_access_path ->
              let owned = ThreadSafetyDomain.OwnershipDomain.add lhs_access_path astate.owned in
              { astate with owned; }
          | None ->
              astate
        end
    | Sil.Call (_, Const (Cfun pn), actuals, loc, _) ->
        begin
          (* assuming that modeled procedures do not have useful summaries *)
          match get_lock_model pn with
          | Lock ->
              { astate with locks = true; }
          | Unlock ->
              { astate with locks = false; }
          | NoEffect ->
              if is_unprotected astate.locks && is_container_write pn tenv
              then
                match actuals with
                | (receiver_exp, receiver_typ) :: _ ->
                    add_container_write pn loc receiver_exp receiver_typ astate
                | [] ->
                    failwithf
                      "Call to %a is marked as a container write, but has no receiver"
                      Procname.pp pn
              else
                begin
                  match Summary.read_summary pdesc pn with
                  | Some (callee_locks, callee_reads, _, callee_unconditional_writes) ->
                      let locks' = callee_locks || astate.locks in
                      let astate' =
                        (* TODO (14842325): report on constructors that aren't threadsafe
                           (e.g., constructors that access static fields) *)
                        if is_unprotected locks'
                        then
                          let call_site = CallSite.make pn loc in
                          let reads =
                            ThreadSafetyDomain.PathDomain.with_callsite callee_reads call_site
                            |> ThreadSafetyDomain.PathDomain.join astate.reads in
                          let unconditional_writes =
                            ThreadSafetyDomain.PathDomain.with_callsite
                              callee_unconditional_writes
                              call_site
                            |> ThreadSafetyDomain.PathDomain.join astate.unconditional_writes in
                          { astate with reads; unconditional_writes; }
                        else
                          astate in
                      { astate' with locks = locks'; }
                  | None ->
                      astate
                end
        end

    | Sil.Store (Exp.Lvar lhs_pvar, lhs_typ, rhs_exp, _) when Pvar.is_frontend_tmp lhs_pvar ->
        let id_map' = analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ astate in
        { astate with id_map = id_map'; }

    | Sil.Store (lhs_exp, lhs_typ, rhs_exp, loc) ->
        let unconditional_writes =
          match lhs_exp with
          | Lfield ( _, _, typ)
            when is_unprotected astate.locks -> (* abstracts no lock being held *)
              add_path_to_state
                lhs_exp typ loc astate.unconditional_writes astate.id_map astate.owned tenv
          | _ ->
              astate.unconditional_writes in
        (* if rhs is owned, propagate ownership to lhs. otherwise, remove lhs from ownerhsip set
           (since it may have previously held an owned memory loc and is now being reassigned *)
        let owned =
          match AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id,
                AccessPath.of_lhs_exp rhs_exp lhs_typ ~f_resolve_id with
          | Some lhs_access_path, Some rhs_access_path ->
              if ThreadSafetyDomain.OwnershipDomain.mem rhs_access_path astate.owned
              then ThreadSafetyDomain.OwnershipDomain.add lhs_access_path astate.owned
              else ThreadSafetyDomain.OwnershipDomain.remove lhs_access_path astate.owned
          | Some lhs_access_path, None ->
              ThreadSafetyDomain.OwnershipDomain.remove lhs_access_path astate.owned
          | _ ->
              astate.owned in
        { astate with unconditional_writes; owned; }

    | Sil.Load (lhs_id, rhs_exp, rhs_typ, loc) ->
        let id_map = analyze_id_assignment (Var.of_id lhs_id) rhs_exp rhs_typ astate in
        let reads =
          match rhs_exp with
          | Lfield ( _, _, typ) when is_unprotected astate.locks ->
              add_path_to_state rhs_exp typ loc astate.reads astate.id_map astate.owned tenv
          | _ ->
              astate.reads in
        (* if rhs is owned, propagate ownership to lhs *)
        let owned =
          match AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id with
          | Some rhs_access_path
            when ThreadSafetyDomain.OwnershipDomain.mem rhs_access_path astate.owned ->
              ThreadSafetyDomain.OwnershipDomain.add (AccessPath.of_id lhs_id rhs_typ) astate.owned
          | _ ->
              astate.owned in
        { astate with Domain.reads; id_map; owned; }

    | Sil.Remove_temps (ids, _) ->
        let id_map =
          IList.fold_left
            (fun acc id -> IdAccessPathMapDomain.remove (Var.of_id id) acc)
            astate.id_map
            ids in
        { astate with id_map; }

    |  _  ->
        astate
end

module Analyzer =
  AbstractInterpreter.Make
    (ProcCfg.Normal)
    (Scheduler.ReversePostorder)
    (TransferFunctions)

module Interprocedural = AbstractInterpreter.Interprocedural (Summary)

(* a results table is a Map where a key is an a procedure environment,
   i.e., something of type Idenv.t * Tenv.t * Procname.t * Procdesc.t
*)
module ResultsTableType = Caml.Map.Make (struct
    type t = Idenv.t * Tenv.t * Procname.t * Procdesc.t
    let compare (_, _, pn1, _) (_,_,pn2,_) =  Procname.compare pn1 pn2
  end)

(* we want to consider Builder classes and other safe immutablility-ensuring patterns as
   thread-safe. we are overly friendly about this for now; any class whose name ends with `Builder`
   is assumed to be thread-safe. in the future, we can ask for builder classes to be annotated with
   @Builder and verify that annotated classes satisfy the expected invariants. *)
let is_builder_class class_name =
  String.is_suffix ~suffix:"Builder" class_name

(* similarly, we assume that immutable classes safely encapsulate their state *)
let is_immutable_collection_class class_name tenv =
  let immutable_collections = [
    "com.google.common.collect.ImmutableCollection";
    "com.google.common.collect.ImmutableMap";
    "com.google.common.collect.ImmutableTable";
  ] in
  PatternMatch.supertype_exists
    tenv (fun typename _ -> IList.mem (=) (Typename.name typename) immutable_collections) class_name

let is_call_to_builder_class_method = function
  | Procname.Java java_pname -> is_builder_class (Procname.java_get_class_name java_pname)
  | _ -> false

let is_call_to_immutable_collection_method tenv = function
  | Procname.Java java_pname ->
      is_immutable_collection_class (Procname.java_get_class_type_name java_pname) tenv
  | _ ->
      false

let is_initializer tenv proc_name =
  Procname.is_constructor proc_name ||
  Procname.is_class_initializer proc_name ||
  FbThreadSafety.is_custom_init tenv proc_name

let is_annotated f_annot pdesc =
  let annotated_signature = Annotations.get_annotated_signature (Procdesc.get_attributes pdesc) in
  let ret_annotation, _ = annotated_signature.Annotations.ret in
  f_annot ret_annotation

(* Methods in @ThreadConfined classes and methods annotated with @ThreadConfied are assumed to all
   run on the same thread. For the moment we won't warn on accesses resulting from use of such
   methods at all. In future we should account for races between these methods and methods from
   completely different classes that don't necessarily run on the same thread as the confined
   object. *)
let is_thread_confined_method tenv pdesc =
  is_annotated Annotations.ia_is_thread_confined pdesc ||
  PatternMatch.check_current_class_attributes
    Annotations.ia_is_thread_confined tenv (Procdesc.get_proc_name pdesc)

(* we don't want to warn on methods that run on the UI thread because they should always be
   single-threaded *)
let runs_on_ui_thread proc_desc =
  (* assume that methods annotated with @UiThread or @OnEvent(SomeEvent.class) always run on the UI
     thread *)
  is_annotated
    (fun annot -> Annotations.ia_is_ui_thread annot || Annotations.ia_is_on_event annot)
    proc_desc

(* return true if we should compute a summary for the procedure. if this returns false, we won't
   analyze the procedure or report any warnings on it *)
(* note: in the future, we will want to analyze the procedures in all of these cases in order to
   find more bugs. this is just a temporary measure to avoid obvious false positives *)
let should_analyze_proc pdesc tenv =
  let pn = Procdesc.get_proc_name pdesc in
  not (is_initializer tenv pn) &&
  not (FbThreadSafety.is_logging_method pn) &&
  not (is_call_to_builder_class_method pn) &&
  not (is_call_to_immutable_collection_method tenv pn) &&
  not (runs_on_ui_thread pdesc) &&
  not (is_thread_confined_method tenv pdesc)

(* return true if we should report on unprotected accesses during the procedure *)
let should_report_on_proc (_, tenv, proc_name, proc_desc) =
  not (is_initializer tenv proc_name) &&
  not (Procname.java_is_autogen_method proc_name) &&
  Procdesc.get_access proc_desc <> PredSymb.Private

(* creates a map from proc_envs to postconditions *)
let make_results_table get_proc_desc file_env =
  (* make a Map sending each element e of list l to (f e) *)
  let map_post_computation_over_procs f l =
    IList.fold_left (fun m p -> ResultsTableType.add p (f p) m
                    ) ResultsTableType.empty l
  in
  let compute_post_for_procedure = (* takes proc_env as arg *)
    fun (idenv, tenv, proc_name, proc_desc) ->
      let empty =
        false,
        ThreadSafetyDomain.PathDomain.empty,
        ThreadSafetyDomain.ConditionalWritesDomain.empty,
        ThreadSafetyDomain.PathDomain.empty in
      (* convert the abstract state to a summary by dropping the id map *)
      let compute_post ({ ProcData.pdesc; tenv; } as proc_data) =
        if should_analyze_proc pdesc tenv
        then
          begin
            if not (Procdesc.did_preanalysis pdesc) then Preanal.do_liveness pdesc tenv;
            match Analyzer.compute_post proc_data ~initial:ThreadSafetyDomain.empty with
            | Some { locks; reads; conditional_writes; unconditional_writes; } ->
                Some (locks, reads, conditional_writes, unconditional_writes)
            | None ->
                None
          end
        else
          Some empty in
      let callback_arg =
        {Callbacks.get_proc_desc; get_procs_in_file = (fun _ -> []);
         idenv; tenv; proc_name; proc_desc} in
      match
        Interprocedural.compute_and_store_post
          ~compute_post
          ~make_extras:ProcData.make_empty_extras
          callback_arg with
      | Some post -> post
      | None -> empty
  in
  map_post_computation_over_procs compute_post_for_procedure file_env

let get_current_class_and_threadsafe_superclasses tenv pname =
  match pname with
  | Procname.Java java_pname ->
      let current_class = Procname.java_get_class_type_name java_pname in
      let thread_safe_annotated_classes = PatternMatch.find_superclasses_with_attributes
          Annotations.ia_is_thread_safe tenv current_class
      in
      Some (current_class,thread_safe_annotated_classes)
  | _ -> None  (*shouldn't happen*)

(** The addendum message says that a superclass is marked @ThreadSafe,
    when the current class is not so marked*)
let calculate_addendum_message tenv pname =
  match get_current_class_and_threadsafe_superclasses tenv pname with
  | Some (current_class,thread_safe_annotated_classes) ->
      if not (IList.mem Typename.equal current_class thread_safe_annotated_classes) then
        match thread_safe_annotated_classes with
        | hd::_ -> F.asprintf "\n Note: Superclass %a is marked @ThreadSafe." Typename.pp hd
        | [] -> ""
      else ""
  | _ -> ""

let report_thread_safety_violations ( _, tenv, pname, pdesc) trace =
  let open ThreadSafetyDomain in
  let trace_of_pname callee_pname =
    match Summary.read_summary pdesc callee_pname with
    | Some (_, _, _, unconditional_writes) -> unconditional_writes
    | _ -> PathDomain.empty in
  let report_one_path ((_, sinks) as path) =
    let pp_accesses fmt sink =
      let _, accesses = PathDomain.Sink.kind sink in
      AccessPath.pp_access_list fmt accesses in
    let initial_sink, _ = IList.hd (IList.rev sinks) in
    let final_sink, _ = IList.hd sinks in
    let initial_sink_site = PathDomain.Sink.call_site initial_sink in
    let final_sink_site = PathDomain.Sink.call_site final_sink in
    let desc_of_sink sink =
      if CallSite.equal (PathDomain.Sink.call_site sink) final_sink_site
      then
        Format.asprintf "access to %a" pp_accesses sink
      else
        Format.asprintf
          "call to %a" Procname.pp (CallSite.pname (PathDomain.Sink.call_site sink)) in
    let loc = CallSite.loc (PathDomain.Sink.call_site initial_sink) in
    let ltr = PathDomain.to_sink_loc_trace ~desc_of_sink path in
    let msg = Localise.to_string Localise.thread_safety_violation in
    let description =
      Format.asprintf "Public method %a%s writes to field %a outside of synchronization.%s"
        Procname.pp pname
        (if CallSite.equal final_sink_site initial_sink_site then "" else " indirectly")
        pp_accesses final_sink
        (calculate_addendum_message tenv pname) in
    let exn = Exceptions.Checkers (msg, Localise.verbatim_desc description) in
    Reporting.log_error pname ~loc ~ltr exn in

  IList.iter
    report_one_path
    (PathDomain.get_reportable_sink_paths trace ~trace_of_pname)

(* Currently we analyze if there is an @ThreadSafe annotation on at least one of
   the classes in a file. This might be tightened in future or even broadened in future
   based on other criteria *)
let should_report_on_file file_env =
  let current_class_or_super_marked_threadsafe =
    fun (_, tenv, pname, _) ->
      match get_current_class_and_threadsafe_superclasses tenv pname with
      | Some (_, thread_safe_annotated_classes) ->
          not (thread_safe_annotated_classes = [])
      | _ -> false
  in
  let current_class_marked_not_threadsafe =
    fun (_, tenv, pname, _) ->
      PatternMatch.check_current_class_attributes Annotations.ia_is_not_thread_safe tenv pname
  in
  not (IList.exists current_class_marked_not_threadsafe file_env) &&
  IList.exists current_class_or_super_marked_threadsafe file_env

(* For now, just checks if there is one active element amongst the posts of the analyzed methods.
   This indicates that the method races with itself. To be refined later. *)
let process_results_table file_env tab =
  let should_report_on_all_procs = should_report_on_file file_env in
  let should_report ((_, _, _, pdesc) as proc_env) =
    (should_report_on_all_procs || is_annotated Annotations.ia_is_thread_safe_method pdesc)
    && should_report_on_proc proc_env in
  ResultsTableType.iter (* report errors for each method *)
    (fun proc_env (_, _, _, unconditional_writes) ->
       if should_report proc_env then report_thread_safety_violations proc_env unconditional_writes)
    tab

(*This is a "cluster checker" *)
(*Gathers results by analyzing all the methods in a file, then post-processes
  the results to check (approximation of) thread safety *)
(* file_env: (Idenv.t * Tenv.t * Procname.t * Procdesc.t) list *)
let file_analysis _ _ get_procdesc file_env =
  process_results_table file_env (make_results_table get_procdesc file_env)