<commit_before>(*
 * Copyright © 1990-2009 The Regents of the University of California. All rights reserved. 
 *
 * Permission is hereby granted, without written agreement and without 
 * license or royalty fees, to use, copy, modify, and distribute this 
 * software and its documentation for any purpose, provided that the 
 * above copyright notice and the following two paragraphs appear in 
 * all copies of this software. 
 * 
 * IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY 
 * FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES 
 * ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN 
 * IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY 
 * OF SUCH DAMAGE. 
 * 
 * THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, 
 * INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY 
 * AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS 
 * ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION 
 * TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
 *
 *)

(* change wfsubst to disjoint locations
   use sorting on eqpair to cut complexity *)

module M   = Misc
module P   = Pretty
module C   = Cil
module Cs  = Constants
module E   = Errormsg
module ST  = Ssa_transform
module RA  = Refanno
module S   = Sloc
module Sb  = S.Subst
module SLM = S.SlocMap
module SS  = S.SlocSet
module CM  = CilMisc
module VM  = CM.VarMap
module SM  = M.StringMap
module FI  = FixInterface
module Sh  = Shape
module FF  = FinalFields

open Ctypes
open ShapeInfra
open M.Ops

module LDesc = I.LDesc
module Store = I.Store
module Ct    = I.CType
module CFun  = I.CFun
module Field = I.Field
module CSpec = I.Spec 

(******************************************************************************)
(******************************** Environments ********************************)
(******************************************************************************)

module IM = M.IntMap

type ctvenv = ctype VM.t

type funenv = (cfun * ctvenv) VM.t

let funenv_entry_of_cfun cf =
  (cf, VM.empty)

let ctenv_of_funenv fe =
  VM.map fst fe

let funenv_of_ctenv env =
  VM.fold (fun f cf fe -> VM.add f (funenv_entry_of_cfun cf) fe) env VM.empty

type env = funenv * ctvenv

type ctvemap = I.ctemap

(******************************************************************************)
(********************************* Constraints ********************************)
(******************************************************************************)

type cstrdesc =
  | CWFSubst of S.Subst.t

let cstrdesc_slocs = function
  | CWFSubst (sub) -> S.Subst.slocs sub

let d_cstrdesc () = function
  | CWFSubst (sub) -> P.dprintf "WF(%a)" S.Subst.d_subst sub

let apply_subst_to_subst appsub sub =
  List.map (fun (sfrom, sto) -> (S.Subst.apply appsub sfrom, S.Subst.apply appsub sto)) sub

let cstrdesc_subst sub = function
  | CWFSubst sub2 -> CWFSubst (apply_subst_to_subst sub sub2)

(* pmr: Inline constraint def? *)
type 'a precstr = {cid: int; cdesc: 'a; cloc: C.location}

type cstr = cstrdesc precstr

let (fresh_cstrid, reset_fresh_cstrids) = M.mk_int_factory ()

let mk_cstr loc cdesc =
  {cid = fresh_cstrid (); cloc = loc; cdesc = cdesc}

let cstr_subst sub c =
  mk_cstr c.cloc (cstrdesc_subst sub c.cdesc)

let d_cstr () {cid = cid; cdesc = cdesc; cloc = loc} =
  P.dprintf "%a: %a" C.d_loc loc d_cstrdesc cdesc

(******************************************************************************)
(***************************** Constraint Solving *****************************)
(******************************************************************************)

exception Unify of ctype * ctype

let store_add_absent loc l i ctv sto =
  SLM.add l (LDesc.add loc i (Field.create Ctypes.Final ctv) (Store.find_or_empty l sto)) sto

let rec unify_ctypes loc ct1 ct2 sub sto = match Ct.subs sub ct1, Ct.subs sub ct2 with
  | _, _                     when ct1 = ct2  -> (sub, sto)
  | Ref (s1, _), Ref (s2, _) when S.eq s1 s2 -> (sub, sto)
  | Int (n1, _), Int (n2, _) when n1 = n2    -> (sub, sto)
  | Ref (s1, _), Ref (s2, _)                 -> unify_locations loc s1 s2 sub sto
  | _                                        -> raise (Unify (ct1, ct2))

and unify_locations loc s1 s2 sub sto =
  let sub = S.Subst.extend s1 s2 sub in
  let ld1 = sto |> Store.find_or_empty s1 |> LDesc.subs sub in
  let sto = Store.remove sto s1 |> SLM.add s2 (Store.find_or_empty s2 sto) |> Store.subs sub in
    LDesc.fold (fun (sub, sto) i f -> store_add loc s2 i (Field.type_of f) sub sto) (sub, sto) ld1

and store_add loc s i ct sub sto =
  let s  = S.Subst.apply sub s in
  let ct = Ct.subs sub ct in
  try match i with
    | Index.IBot   -> (sub, sto)
    | Index.IInt n ->
      begin match Store.find_index s i sto with
        | []    -> (sub, store_add_absent loc s i ct sto)
        | [fld] -> unify_ctypes loc ct (Field.type_of fld) sub sto
        | _     -> assert false
      end
    | Index.ICClass _ ->
      let ld       = Store.find_or_empty s sto in
      let flds     = LDesc.find i ld in
      let cts      = List.map (snd <+> Field.type_of) flds in
      let sub, sto = List.fold_left (fun (sub, sto) ct2 -> unify_ctypes loc ct ct2 sub sto) (sub, sto) cts in
        if List.exists (fun (i2, _) -> Index.is_subindex i i2) flds then
          (* If this sequence is included in an existing one, there's nothing left to do *)
          (sub, sto)
        else
          (* Otherwise, remove overlapping elements and add one at the LUB of all indices. *)
          let ld = List.fold_left (fun ld (i2, _) -> LDesc.remove i2 ld) ld flds in
          let i  = List.fold_left (fun i (i2, _) -> Index.lub i i2) i flds in
          let ld = LDesc.add loc i (Field.create Ctypes.Final ct) ld in
            (sub, SLM.add s ld sto)<commit_msg>simplify store_add<commit_after>(*
 * Copyright © 1990-2009 The Regents of the University of California. All rights reserved. 
 *
 * Permission is hereby granted, without written agreement and without 
 * license or royalty fees, to use, copy, modify, and distribute this 
 * software and its documentation for any purpose, provided that the 
 * above copyright notice and the following two paragraphs appear in 
 * all copies of this software. 
 * 
 * IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY 
 * FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES 
 * ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN 
 * IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY 
 * OF SUCH DAMAGE. 
 * 
 * THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, 
 * INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY 
 * AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS 
 * ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION 
 * TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
 *
 *)

(* change wfsubst to disjoint locations
   use sorting on eqpair to cut complexity *)

module M   = Misc
module P   = Pretty
module C   = Cil
module Cs  = Constants
module E   = Errormsg
module ST  = Ssa_transform
module RA  = Refanno
module S   = Sloc
module Sb  = S.Subst
module SLM = S.SlocMap
module SS  = S.SlocSet
module CM  = CilMisc
module VM  = CM.VarMap
module SM  = M.StringMap
module FI  = FixInterface
module Sh  = Shape
module FF  = FinalFields

open Ctypes
open ShapeInfra
open M.Ops

module LDesc = I.LDesc
module Store = I.Store
module Ct    = I.CType
module CFun  = I.CFun
module Field = I.Field
module CSpec = I.Spec 

(******************************************************************************)
(******************************** Environments ********************************)
(******************************************************************************)

module IM = M.IntMap

type ctvenv = ctype VM.t

type funenv = (cfun * ctvenv) VM.t

let funenv_entry_of_cfun cf =
  (cf, VM.empty)

let ctenv_of_funenv fe =
  VM.map fst fe

let funenv_of_ctenv env =
  VM.fold (fun f cf fe -> VM.add f (funenv_entry_of_cfun cf) fe) env VM.empty

type env = funenv * ctvenv

type ctvemap = I.ctemap

(******************************************************************************)
(********************************* Constraints ********************************)
(******************************************************************************)

type cstrdesc =
  | CWFSubst of S.Subst.t

let cstrdesc_slocs = function
  | CWFSubst (sub) -> S.Subst.slocs sub

let d_cstrdesc () = function
  | CWFSubst (sub) -> P.dprintf "WF(%a)" S.Subst.d_subst sub

let apply_subst_to_subst appsub sub =
  List.map (fun (sfrom, sto) -> (S.Subst.apply appsub sfrom, S.Subst.apply appsub sto)) sub

let cstrdesc_subst sub = function
  | CWFSubst sub2 -> CWFSubst (apply_subst_to_subst sub sub2)

(* pmr: Inline constraint def? *)
type 'a precstr = {cid: int; cdesc: 'a; cloc: C.location}

type cstr = cstrdesc precstr

let (fresh_cstrid, reset_fresh_cstrids) = M.mk_int_factory ()

let mk_cstr loc cdesc =
  {cid = fresh_cstrid (); cloc = loc; cdesc = cdesc}

let cstr_subst sub c =
  mk_cstr c.cloc (cstrdesc_subst sub c.cdesc)

let d_cstr () {cid = cid; cdesc = cdesc; cloc = loc} =
  P.dprintf "%a: %a" C.d_loc loc d_cstrdesc cdesc

(******************************************************************************)
(***************************** Constraint Solving *****************************)
(******************************************************************************)

exception Unify of ctype * ctype

let store_add_absent loc l i ctv sto =
  SLM.add l (LDesc.add loc i (Field.create Ctypes.Final ctv) (Store.find_or_empty l sto)) sto

let rec unify_ctypes loc ct1 ct2 sub sto = match Ct.subs sub ct1, Ct.subs sub ct2 with
  | _, _                     when ct1 = ct2  -> (sub, sto)
  | Ref (s1, _), Ref (s2, _) when S.eq s1 s2 -> (sub, sto)
  | Int (n1, _), Int (n2, _) when n1 = n2    -> (sub, sto)
  | Ref (s1, _), Ref (s2, _)                 -> unify_locations loc s1 s2 sub sto
  | _                                        -> raise (Unify (ct1, ct2))

and unify_locations loc s1 s2 sub sto =
  let sub = S.Subst.extend s1 s2 sub in
  let ld1 = sto |> Store.find_or_empty s1 |> LDesc.subs sub in
  let sto = Store.remove sto s1 |> SLM.add s2 (Store.find_or_empty s2 sto) |> Store.subs sub in
    LDesc.fold (fun (sub, sto) i f -> store_add loc s2 i (Field.type_of f) sub sto) (sub, sto) ld1

and store_add loc s i ct sub sto =
  let s  = S.Subst.apply sub s in
  let ct = Ct.subs sub ct in
  try match i with
    | Index.IBot                     -> (sub, sto)
    | Index.ICClass _ | Index.IInt _ ->
      let ld = Store.find_or_empty s sto in
        match LDesc.find i ld with
          | []   -> (sub, store_add_absent loc s i ct sto)
          | flds ->
            let cts      = List.map (snd <+> Field.type_of) flds in
            let sub, sto = List.fold_left (fun (sub, sto) ct2 -> unify_ctypes loc ct ct2 sub sto) (sub, sto) cts in
              if List.exists (fun (i2, _) -> Index.is_subindex i i2) flds then
                (* If this sequence is included in an existing one, there's nothing left to do *)
                (sub, sto)
              else
                (* Otherwise, remove overlapping elements and add one at the LUB of all indices. *)
                let ld = List.fold_left (fun ld (i2, _) -> LDesc.remove i2 ld) ld flds in
                let i  = List.fold_left (fun i (i2, _) -> Index.lub i i2) i flds in
                let ld = LDesc.add loc i (Field.create Ctypes.Final ct) ld in
                  (sub, SLM.add s ld sto)
{'fraction_non_alphanumeric': 0.1924292916346236, 'fraction_numerical': 0.008373921216782022, 'mean_word_length': 3.188976377952756, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 53, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3349002', 'n_tokens_mistral': 4023, 'n_tokens_neox': 3746, 'n_words': 1367}