<commit_before>(*
 * Copyright (c) Facebook, Inc. and its affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)

open! IStd
module L = Logging
open PulseBasicInterface
open PulseDomainInterface
open PulseOperations.Import

type t = AbductiveDomain.t

let is_ptr_to_const formal_typ_opt =
  Option.value_map formal_typ_opt ~default:false ~f:(fun (formal_typ : Typ.t) ->
      match formal_typ.desc with Typ.Tptr (t, _) -> Typ.is_const t.quals | _ -> false )


let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate =
  let event = ValueHistory.Call {f= reason; location= call_loc; in_call= []} in
  let havoc_ret (ret, _) astate = PulseOperations.havoc_id ret [event] astate in
  let rec havoc_fields ((_, history) as addr) typ astate =
    match typ.Typ.desc with
    | Tstruct struct_name -> (
      match Tenv.lookup tenv struct_name with
      | Some {fields} ->
          List.fold fields ~init:astate ~f:(fun acc (field, field_typ, _) ->
              let fresh_value = AbstractValue.mk_fresh () in
              Memory.add_edge addr (FieldAccess field) (fresh_value, [event]) call_loc acc
              |> havoc_fields (fresh_value, history) field_typ )
      | None ->
          astate )
    | _ ->
        astate
  in
  let havoc_actual_if_ptr (actual, actual_typ) formal_typ_opt astate =
    (* We should not havoc when the corresponding formal is a
       pointer to const *)
    match actual_typ.Typ.desc with
    | Tptr (typ, _)
      when (not (Language.curr_language_is Java)) && not (is_ptr_to_const formal_typ_opt) ->
        (* HACK: write through the pointer even if it is invalid (except in Java). This is to avoid raising issues when
           havoc'ing pointer parameters (which normally causes a [check_valid] call. *)
        let fresh_value = AbstractValue.mk_fresh () in
        Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate
        |> havoc_fields actual typ
    | _ ->
        astate
  in
  let add_skipped_proc astate =
    match reason with
    | CallEvent.SkippedKnownCall proc_name ->
        AbductiveDomain.add_skipped_call proc_name
          (Trace.Immediate {location= call_loc; history= []})
          astate
    | _ ->
        astate
  in
  L.d_printfln "skipping unknown procedure@." ;
  ( match formals_opt with
  | None ->
      List.fold actuals
        ~f:(fun astate actual_typ -> havoc_actual_if_ptr actual_typ None astate)
        ~init:astate
  | Some formals -> (
    match
      List.fold2 actuals formals
        ~f:(fun astate actual_typ (_, formal_typ) ->
          havoc_actual_if_ptr actual_typ (Some formal_typ) astate )
        ~init:astate
    with
    | Unequal_lengths ->
        L.d_printfln "ERROR: formals have length %d but actuals have length %d"
          (List.length formals) (List.length actuals) ;
        astate<commit_msg>[pulse] Havoc actuals when lengths of actuals and formals mismatch<commit_after>(*
 * Copyright (c) Facebook, Inc. and its affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)

open! IStd
module L = Logging
open PulseBasicInterface
open PulseDomainInterface
open PulseOperations.Import

type t = AbductiveDomain.t

let is_ptr_to_const formal_typ_opt =
  Option.value_map formal_typ_opt ~default:false ~f:(fun (formal_typ : Typ.t) ->
      match formal_typ.desc with Typ.Tptr (t, _) -> Typ.is_const t.quals | _ -> false )


let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate =
  let event = ValueHistory.Call {f= reason; location= call_loc; in_call= []} in
  let havoc_ret (ret, _) astate = PulseOperations.havoc_id ret [event] astate in
  let rec havoc_fields ((_, history) as addr) typ astate =
    match typ.Typ.desc with
    | Tstruct struct_name -> (
      match Tenv.lookup tenv struct_name with
      | Some {fields} ->
          List.fold fields ~init:astate ~f:(fun acc (field, field_typ, _) ->
              let fresh_value = AbstractValue.mk_fresh () in
              Memory.add_edge addr (FieldAccess field) (fresh_value, [event]) call_loc acc
              |> havoc_fields (fresh_value, history) field_typ )
      | None ->
          astate )
    | _ ->
        astate
  in
  let havoc_actual_if_ptr (actual, actual_typ) formal_typ_opt astate =
    (* We should not havoc when the corresponding formal is a
       pointer to const *)
    match actual_typ.Typ.desc with
    | Tptr (typ, _)
      when (not (Language.curr_language_is Java)) && not (is_ptr_to_const formal_typ_opt) ->
        (* HACK: write through the pointer even if it is invalid (except in Java). This is to avoid raising issues when
           havoc'ing pointer parameters (which normally causes a [check_valid] call. *)
        let fresh_value = AbstractValue.mk_fresh () in
        Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate
        |> havoc_fields actual typ
    | _ ->
        astate
  in
  let add_skipped_proc astate =
    match reason with
    | CallEvent.SkippedKnownCall proc_name ->
        AbductiveDomain.add_skipped_call proc_name
          (Trace.Immediate {location= call_loc; history= []})
          astate
    | _ ->
        astate
  in
  let havoc_actuals_without_typ_info astate =
    List.fold actuals
      ~f:(fun astate actual_typ -> havoc_actual_if_ptr actual_typ None astate)
      ~init:astate
  in
  L.d_printfln "skipping unknown procedure@." ;
  ( match formals_opt with
  | None ->
      havoc_actuals_without_typ_info astate
  | Some formals -> (
    match
      List.fold2 actuals formals
        ~f:(fun astate actual_typ (_, formal_typ) ->
          havoc_actual_if_ptr actual_typ (Some formal_typ) astate )
        ~init:astate
    with
    | Unequal_lengths ->
        L.d_printfln "ERROR: formals have length %d but actuals have length %d"
          (List.length formals) (List.length actuals) ;
        havoc_actuals_without_typ_info astate
{'fraction_non_alphanumeric': 0.08337477208685563, 'fraction_numerical': 0.0003315100281783524, 'mean_word_length': 2.8629961587708066, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 41, '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': '4877056', 'n_tokens_mistral': 1910, 'n_tokens_neox': 1878, 'n_words': 575}