<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.
 *
 *)

module M   = Misc
module P   = Pretty
module E   = Errormsg
module S   = Sloc
module SS  = S.SlocSet
module C   = Cil
module CM  = CilMisc
module SM  = M.StringMap
module SLM = S.SlocMap

module SLMPrinter = P.MakeMapPrinter(SLM)

open M.Ops

(******************************************************************************)
(*********************************** Indices **********************************)
(******************************************************************************)

type seq_polarity =     (* direction in which sequence extends *)
  | Pos                 (* +ve unbounded         *)
  | PosNeg              (* +ve and -ve unbounded *)
  | PosB of int         (* +ve fewer than k > 0 times *)

let is_unbounded = function
  | PosB _ -> false 
  | _      -> true

let seq_polarity_lub (p1: seq_polarity) (p2: seq_polarity): seq_polarity =
  match p1, p2 with
    | PosNeg, _ | _, PosNeg -> PosNeg
    | Pos, _    | _, Pos    -> Pos
    | PosB a, PosB b        -> PosB (max a b)

module Index = struct
  type class_bound = int option (* None = unbounded *)

  let scale_bound x b =
    M.map_opt (( * ) x) b

  let bound_offset x b =
    M.map_opt (( + ) x) b

  let bound_plus b1 b2 = match b1, b2 with
    | Some n, Some m -> Some (m + n)
    | _              -> None

  let lower_bound_le b1 b2 = match b1, b2 with
    | Some n, Some m -> n <= m
    | Some _, None   -> false
    | _              -> true

  let upper_bound_le b1 b2 = match b1, b2 with
    | Some n, Some m -> n <= m
    | None, Some _   -> false
    | _              -> true

  let bound_min le b1 b2 =
    if le b1 b2 then b1 else b2

  let bound_max le b1 b2 =
    if le b1 b2 then b2 else b1

  let lower_bound_min = bound_min lower_bound_le
  let lower_bound_max = bound_max lower_bound_le
  let upper_bound_min = bound_min upper_bound_le
  let upper_bound_max = bound_max upper_bound_le

  (* Describes the integers lb <= n <= ub s.t. n = c (mod m) *)
  type bounded_congruence_class = {
    lb : class_bound; (* Lower bound; lb mod m = c *)
    ub : class_bound; (* Upper bound; ub mod m = c; lb < ub *)
    c  : int;         (* Remainder; 0 <= c < m *)
    m  : int;         (* Modulus; 0 < m <= ub - lb *)
  }

  type t =
    | IBot                                 (* Empty *)
    | IInt    of int                       (* Single integer *)
    | ICClass of bounded_congruence_class  (* Subset of congruence class *)

  let top = ICClass {lb = None; ub = None; c = 0; m = 1}

  let nonneg = ICClass {lb = Some 0; ub = None; c = 0; m = 1}

  let d_index () = function
    | IBot                                         -> P.dprintf "_|_"
    | IInt n                                       -> P.num n
    | ICClass {lb = None; ub = None; c = c; m = m} -> P.dprintf "%d{%d}" c m
    | ICClass {lb = Some n; ub = None; m = m}      -> P.dprintf "%d[%d]" n m
    | ICClass {lb = Some l; ub = Some u; m = m}    -> P.dprintf "[%d][%d < %d]" l m (u + m)
    | _                                            -> assert false

  let of_int i =
    (* pmr: loosen this? *)
    if i >= 0 then IInt i else top

  let mk_sequence start period lbound ubound =
    ICClass {lb = lbound; ub = ubound; m = period; c = start mod period}

  let is_unbounded = function
    | ICClass {lb = None} | ICClass {ub = None} -> true
    | _                                         -> false

  let is_subindex i1 i2 = match i1, i2 with
    | IBot, _                                          -> true
    | _, IBot                                          -> false
    | IInt n, IInt m                                   -> n = m
    | ICClass _, IInt _                                -> false
    | IInt n, ICClass {lb = lb; ub = ub; c = c; m = m} ->
      lower_bound_le lb (Some n) && upper_bound_le (Some n) ub && ((n mod m) = c)
    | ICClass {lb = lb1; ub = ub1; c = c1; m = m1},
      ICClass {lb = lb2; ub = ub2; c = c2; m = m2} ->
      lower_bound_le lb2 lb1 && upper_bound_le ub1 ub2 && (m1 mod m2) = 0 && (c1 mod m2) = c2

  let widen i1 i2 =
    if is_subindex i1 i2 then
      i2
    else if is_subindex i2 i1 then
      i1
    else match i1, i2 with
      | IBot, _ | _, IBot -> assert false
      | IInt n, IInt m    ->
        let d = abs (n - m) in
          ICClass {lb = Some (min n m);
                   ub = None;
                   c  = n mod d;
                   m  = d}
      | IInt n, ICClass {lb = lb; ub = ub; c = c; m = m}
      | ICClass {lb = lb; ub = ub; c = c; m = m}, IInt n ->
        ICClass {lb = lower_bound_min (Some n) lb;
                 ub = upper_bound_max (Some n) ub;
                 c  = 0;
                 m  = M.gcd m (M.gcd c n)}
      | ICClass {lb = lb1; ub = ub1; c = c1; m = m1},
        ICClass {lb = lb2; ub = ub2; c = c2; m = m2} ->
        let m = M.gcd m1 (M.gcd m2 (abs (c1 - c2))) in
          ICClass {lb = if lb1 = lb2 then lb1 else None;
                   ub = if ub1 = ub2 then ub1 else None;
                   c  = c1 mod m;
                   m  = m}

  let plus i1 i2 = match i1, i2 with
    | IBot, _ | _, IBot -> IBot
    | IInt n, IInt m    -> IInt (n + m)<commit_msg>what was really supposed to be in the last commit<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.
 *
 *)

module M   = Misc
module P   = Pretty
module E   = Errormsg
module S   = Sloc
module SS  = S.SlocSet
module C   = Cil
module CM  = CilMisc
module SM  = M.StringMap
module SLM = S.SlocMap

module SLMPrinter = P.MakeMapPrinter(SLM)

open M.Ops

(******************************************************************************)
(*********************************** Indices **********************************)
(******************************************************************************)

type seq_polarity =     (* direction in which sequence extends *)
  | Pos                 (* +ve unbounded         *)
  | PosNeg              (* +ve and -ve unbounded *)
  | PosB of int         (* +ve fewer than k > 0 times *)

let is_unbounded = function
  | PosB _ -> false 
  | _      -> true

let seq_polarity_lub (p1: seq_polarity) (p2: seq_polarity): seq_polarity =
  match p1, p2 with
    | PosNeg, _ | _, PosNeg -> PosNeg
    | Pos, _    | _, Pos    -> Pos
    | PosB a, PosB b        -> PosB (max a b)

module Index = struct
  type class_bound = int option (* None = unbounded *)

  let scale_bound x b =
    M.map_opt (( * ) x) b

  let bound_offset x b =
    M.map_opt (( + ) x) b

  let bound_plus b1 b2 = match b1, b2 with
    | Some n, Some m -> Some (m + n)
    | _              -> None

  let lower_bound_le b1 b2 = match b1, b2 with
    | Some n, Some m -> n <= m
    | Some _, None   -> false
    | _              -> true

  let upper_bound_le b1 b2 = match b1, b2 with
    | Some n, Some m -> n <= m
    | None, Some _   -> false
    | _              -> true

  let bound_min le b1 b2 =
    if le b1 b2 then b1 else b2

  let bound_max le b1 b2 =
    if le b1 b2 then b2 else b1

  let lower_bound_min = bound_min lower_bound_le
  let lower_bound_max = bound_max lower_bound_le
  let upper_bound_min = bound_min upper_bound_le
  let upper_bound_max = bound_max upper_bound_le

  (* Describes the integers lb <= n <= ub s.t. n = c (mod m) *)
  type bounded_congruence_class = {
    lb : class_bound; (* Lower bound; lb mod m = c *)
    ub : class_bound; (* Upper bound; ub mod m = c; lb < ub *)
    c  : int;         (* Remainder; 0 <= c < m *)
    m  : int;         (* Modulus; 0 < m <= ub - lb *)
  }

  type t =
    | IBot                                 (* Empty *)
    | IInt    of int                       (* Single integer *)
    | ICClass of bounded_congruence_class  (* Subset of congruence class *)

  let top = ICClass {lb = None; ub = None; c = 0; m = 1}

  let nonneg = ICClass {lb = Some 0; ub = None; c = 0; m = 1}

  let d_index () = function
    | IBot                                         -> P.dprintf "_|_"
    | IInt n                                       -> P.num n
    | ICClass {lb = None; ub = None; c = c; m = m} -> P.dprintf "%d{%d}" c m
    | ICClass {lb = Some n; ub = None; m = m}      -> P.dprintf "%d[%d]" n m
    | ICClass {lb = Some l; ub = Some u; m = m}    -> P.dprintf "[%d][%d < %d]" l m (u + m)
    | _                                            -> assert false

  let of_int i =
    (* pmr: loosen this? *)
    if i >= 0 then IInt i else top

  let mk_sequence start period lbound ubound =
    ICClass {lb = lbound; ub = ubound; m = period; c = start mod period}

  let is_unbounded = function
    | ICClass {lb = None} | ICClass {ub = None} -> true
    | _                                         -> false

  let is_subindex i1 i2 = match i1, i2 with
    | IBot, _                                          -> true
    | _, IBot                                          -> false
    | IInt n, IInt m                                   -> n = m
    | ICClass _, IInt _                                -> false
    | IInt n, ICClass {lb = lb; ub = ub; c = c; m = m} ->
      lower_bound_le lb (Some n) && upper_bound_le (Some n) ub && ((n mod m) = c)
    | ICClass {lb = lb1; ub = ub1; c = c1; m = m1},
      ICClass {lb = lb2; ub = ub2; c = c2; m = m2} ->
      lower_bound_le lb2 lb1 && upper_bound_le ub1 ub2 && (m1 mod m2) = 0 && (c1 mod m2) = c2

  let lub i1 i2 =
    if is_subindex i1 i2 then
      i2
    else if is_subindex i2 i1 then
      i1
    else match i1, i2 with
      | IBot, _ | _, IBot -> assert false
      | IInt m, IInt n    ->
        let d = abs (m - n) in
          ICClass {lb = Some (min m n); ub = Some (max m n); m = d; c = m mod d}
      | IInt n, ICClass {lb = lb; ub = ub; m = m; c = c}
      | ICClass {lb = lb; ub = ub; m = m; c = c}, IInt n ->
        let m = M.gcd m (abs (c - (n mod m))) in
          ICClass {lb = lower_bound_min lb (Some n);
                   ub = upper_bound_max ub (Some n);
                   m  = m;
                   c  = c mod m}
      | ICClass {lb = lb1; ub = ub1; m = m1; c = c1},
        ICClass {lb = lb2; ub = ub2; m = m2; c = c2} ->
        let m = M.gcd m1 (M.gcd m2 (abs (c1 - c2))) in
          ICClass {lb = lower_bound_min lb1 lb2;
                   ub = upper_bound_max ub1 ub2;
                   m  = m;
                   c  = c1 mod m}

  (* pmr: There is surely a closed form for this, to be sought
     later. *)
  let rec search_congruent c1 m1 c2 m2 n =
    if n < 0 then None else
      if (n mod m1) = c1 && (n mod m2) = c2 then
        Some n
      else
        search_congruent c1 m1 c2 m2 (n - 1)

  let glb i1 i2 =
    if is_subindex i1 i2 then
      i1
    else if is_subindex i2 i1 then
      i2
    else match i1, i2 with
      | IBot, _ | _, IBot         -> assert false
      | IInt m, IInt n when m = n -> IInt m
      | IInt _, IInt _            -> IBot
      | IInt n, ICClass {lb = lb; ub = ub; m = m; c = c}
      | ICClass {lb = lb; ub = ub; m = m; c = c}, IInt n ->
        if lower_bound_le lb (Some n) &&
           upper_bound_le (Some n) ub &&
           (n mod m) = c then
          IInt n
        else IBot
      | ICClass {lb = lb1; ub = ub1; m = m1; c = c1},
        ICClass {lb = lb2; ub = ub2; m = m2; c = c2} ->
        let m = M.lcm m1 m2 in
          match search_congruent c1 m1 c2 m2 (m - 1) with
            | None   -> IBot
            | Some c ->
              let lb = lower_bound_max lb1 lb2 |> M.map_opt (fun l -> m * ((l + m - c - 1) / m) + c) in
              let ub = upper_bound_min ub1 ub2 |> M.map_opt (fun l -> m * ((l - c) / m) + c) in
                match lb, ub with
                  | Some l, Some u when u = l -> IInt u
                  | Some l, Some u when u < l -> IBot
                  | _                         -> ICClass {lb = lb; ub = ub; m = m; c = c}

  let overlaps i1 i2 =
    glb i1 i2 <> IBot

  let widen i1 i2 =
    if is_subindex i1 i2 then
      i2
    else if is_subindex i2 i1 then
      i1
    else match i1, i2 with
      | IBot, _ | _, IBot -> assert false
      | IInt n, IInt m    ->
        let d = abs (n - m) in
          ICClass {lb = Some (min n m);
                   ub = None;
                   c  = n mod d;
                   m  = d}
      | IInt n, ICClass {lb = lb; ub = ub; c = c; m = m}
      | ICClass {lb = lb; ub = ub; c = c; m = m}, IInt n ->
        ICClass {lb = lower_bound_min (Some n) lb;
                 ub = upper_bound_max (Some n) ub;
                 c  = 0;
                 m  = M.gcd m (M.gcd c n)}
      | ICClass {lb = lb1; ub = ub1; c = c1; m = m1},
        ICClass {lb = lb2; ub = ub2; c = c2; m = m2} ->
        let m = M.gcd m1 (M.gcd m2 (abs (c1 - c2))) in
          ICClass {lb = if lb1 = lb2 then lb1 else None;
                   ub = if ub1 = ub2 then ub1 else None;
                   c  = c1 mod m;
                   m  = m}

  let plus i1 i2 = match i1, i2 with
    | IBot, _ | _, IBot -> IBot
    | IInt n, IInt m    -> IInt (n + m)
{'fraction_non_alphanumeric': 0.1303189718319238, 'fraction_numerical': 0.01844576147033362, 'mean_word_length': 1.6674955595026644, 'pattern_counts': {'":': 0, '<': 26, '<?xml version=': 0, '>': 92, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 36, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2702582', 'n_tokens_mistral': 5232, 'n_tokens_neox': 4963, 'n_words': 1931}