arrayDomain.ml

open GoblintCil
open Pretty
open GobConfig
open FlagHelper

module M = Messages
module A = Array
module VDQ = ValueDomainQueries

type domain = TrivialDomain | PartitionedDomain | UnrolledDomain

(* determines the domain based on variable, type and flag *)
let get_domain ~varAttr ~typAttr =
  let domain_from_string = function
    | "partitioned" -> PartitionedDomain
    | "trivial" -> TrivialDomain
    | "unroll" ->  UnrolledDomain
    | _ -> failwith "AttributeConfiguredArrayDomain: invalid option for domain"
  in
  (*TODO add options?*)
  (*TODO let attribute determine unrolling factor?*)
  let from_attributes = List.find_map (
      fun (Attr (s,ps) )->
        if s = "goblint_array_domain" then (
          List.find_map (fun p -> match p with
              | AStr x -> Some x
              | _ -> None
            ) ps
        )
        else None
    ) in
  if get_bool "annotation.goblint_array_domain" then
    match from_attributes varAttr, from_attributes typAttr with
    | Some x, _ -> domain_from_string x
    | _, Some x -> domain_from_string x
    | _ -> domain_from_string @@ get_string "ana.base.arrays.domain"
  else domain_from_string @@ get_string "ana.base.arrays.domain"

let can_recover_from_top x = x <> TrivialDomain

module type S0 =
sig
  include Lattice.S
  type idx
  type value

  val set: VDQ.t -> t -> Basetype.CilExp.t option * idx -> value -> t
  val make: ?varAttr:attributes -> ?typAttr:attributes -> idx -> value -> t
  val length: t -> idx option

  val move_if_affected: ?replace_with_const:bool -> VDQ.t -> t -> Cil.varinfo -> (Cil.exp -> int option) -> t
  val get_vars_in_e: t -> Cil.varinfo list
  val map: (value -> value) -> t -> t
  val fold_left: ('a -> value -> 'a) -> 'a -> t -> 'a
  val smart_join: (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t -> t
  val smart_widen: (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t -> t
  val smart_leq: (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t -> bool
  val update_length: idx -> t -> t

  val project: ?varAttr:attributes -> ?typAttr:attributes -> VDQ.t -> t -> t
  val invariant: value_invariant:(offset:Cil.offset -> lval:Cil.lval -> value -> Invariant.t) -> offset:Cil.offset -> lval:Cil.lval -> t -> Invariant.t
end

module type S =
sig
  include S0

  val domain_of_t: t -> domain
  val get: ?checkBounds:bool -> VDQ.t -> t -> Basetype.CilExp.t option * idx -> value
end

module type Str =
sig
  include S0

  type ret = Null | NotNull | Maybe
  type substr = IsNotSubstr | IsSubstrAtIndex0 | IsMaybeSubstr

  val get: VDQ.t -> t -> Basetype.CilExp.t option * idx -> ret

  val to_null_byte_domain: string -> t
  val to_string_length: t -> idx
  val string_copy: t -> t -> int option -> t
  val string_concat: t -> t -> int option -> t
  val substring_extraction: t -> t -> substr
  val string_comparison: t -> t -> int option -> idx
end

module type StrWithDomain =
sig
  include Str
  include S with type t := t and type idx := idx
end

module type LatticeWithInvalidate =
sig
  include Lattice.S
  val invalidate_abstract_value: t -> t
end

module type LatticeWithSmartOps =
sig
  include LatticeWithInvalidate
  val smart_join: (Cil.exp -> Z.t option) -> (Cil.exp -> Z.t option) -> t -> t -> t
  val smart_widen: (Cil.exp -> Z.t option) -> (Cil.exp -> Z.t option) -> t -> t -> t
  val smart_leq: (Cil.exp -> Z.t option) -> (Cil.exp -> Z.t option) -> t -> t -> bool
end

module type Null =
sig
  type t
  type retnull = Null | NotNull | Maybe

  val null: unit -> t
  val is_null: t -> retnull

  val get_ikind: t -> Cil.ikind option
  val zero_of_ikind: Cil.ikind -> t
  val not_zero_of_ikind: Cil.ikind -> t
end

module type LatticeWithNull =
sig
  include LatticeWithSmartOps
  include Null with type t := t
end

module Trivial (Val: LatticeWithInvalidate) (Idx: Lattice.S): S with type value = Val.t and type idx = Idx.t =
struct
  include Val
  let name () = "trivial arrays"
  type idx = Idx.t
  type value = Val.t

  let domain_of_t _ = TrivialDomain

  let show x = "Array: " ^ Val.show x
  let pretty () x = text "Array: " ++ pretty () x
  let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
  let get ?(checkBounds=true) (ask: VDQ.t) a i = a
  let set (ask: VDQ.t) a (ie, i) v =
    match ie with
    | Some ie when Offset.Index.Exp.is_all ie ->
      v
    | _ ->
      join a v
  let make ?(varAttr=[]) ?(typAttr=[])  i v = v
  let length _ = None

  let move_if_affected ?(replace_with_const=false) _ x _ _ = x
  let get_vars_in_e _ = []
  let map f x = f x
  let fold_left f a x = f a x

  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>Any</key>\n%a\n</map>\n</value>\n" Val.printXml x
  let smart_join _ _ = join
  let smart_widen _ _ = widen
  let smart_leq _ _ = leq
  let update_length _ x = x

  let project ?(varAttr=[]) ?(typAttr=[]) _ t = t

  let invariant ~value_invariant ~offset ~lval x =
    match offset with
    (* invariants for all indices *)
    | NoOffset when get_bool "witness.invariant.goblint" ->
      let i_lval = Cil.addOffsetLval (Index (Lazy.force Offset.Index.Exp.all, NoOffset)) lval in
      value_invariant ~offset ~lval:i_lval x
    | NoOffset ->
      Invariant.none
    (* invariant for one index *)
    | Index (i, offset) ->
      value_invariant ~offset ~lval x
    (* invariant for one field *)
    | Field (f, offset) ->
      Invariant.none
end

let factor () =
  match get_int "ana.base.arrays.unrolling-factor" with
  | 0 -> failwith "ArrayDomain: ana.base.arrays.unrolling-factor needs to be set when using the unroll domain"
  | x -> x

module Unroll (Val: LatticeWithInvalidate) (Idx:IntDomain.Z): S with type value = Val.t and type idx = Idx.t =
struct
  module Factor = struct let x () = (get_int "ana.base.arrays.unrolling-factor") end
  module Base = Lattice.ProdList (Val) (Factor)
  include Lattice.ProdSimple(Base) (Val)

  let name () = "unrolled arrays"
  type idx = Idx.t
  type value = Val.t

  let domain_of_t _ = UnrolledDomain

  let join_of_all_parts (xl, xr) = List.fold_left Val.join xr xl
  let show (xl, xr) =
    let rec show_list xlist = match xlist with
      | [] -> " --- "
      | hd::tl -> (Val.show hd ^ " - " ^ (show_list tl)) in
    "Array (unrolled to " ^ (Stdlib.string_of_int (factor ())) ^ "): " ^
    (show_list xl) ^ Val.show xr ^ ")"
  let pretty () x = text "Array: " ++ text (show x)
  let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
  let get ?(checkBounds=true)  (ask: VDQ.t) (xl, xr) (_,i) =
    let search_unrolled_values min_i max_i =
      let rec subjoin l i = match l with
        | [] -> Val.bot ()
        | hd::tl ->
          begin
            match Z.gt i max_i, Z.lt i min_i with
            | false,true -> subjoin tl (Z.succ i)
            | false,false -> Val.join hd (subjoin tl (Z.succ i))
            | _,_ -> Val.bot ()
          end in
      subjoin xl Z.zero in
    let f = Z.of_int (factor ()) in
    let min_i = BatOption.default Z.zero (Idx.minimal i) in
    let max_i = BatOption.default f (Idx.maximal i) in
    if Z.geq min_i f then xr
    else if Z.lt max_i f then search_unrolled_values min_i max_i
    else Val.join xr (search_unrolled_values min_i (Z.of_int ((factor ())-1)))
  let set (ask: VDQ.t) (xl,xr) (_,i) v =
    let update_unrolled_values min_i max_i =
      let rec weak_update l i = match l with
        | [] -> []
        | hd::tl ->
          if Z.lt i min_i then hd::(weak_update tl (Z.succ i))
          else if Z.gt i max_i then (hd::tl)
          else (Val.join hd v)::(weak_update tl (Z.succ i)) in
      let rec full_update l i = match l with
        | [] -> []
        | hd::tl ->
          if Z.lt i min_i then hd::(full_update tl (Z.succ i))
          else v::tl in
      if Z.equal min_i max_i then full_update xl Z.zero
      else weak_update xl Z.zero in
    let f = Z.of_int (factor ()) in
    let min_i = BatOption.default Z.zero (Idx.minimal i) in
    let max_i = BatOption.default f (Idx.maximal i) in
    if Z.geq min_i f then (xl, (Val.join xr v))
    else if Z.lt max_i f then ((update_unrolled_values min_i max_i), xr)
    else ((update_unrolled_values min_i (Z.of_int ((factor ())-1))), (Val.join xr v))
  let set ask (xl, xr) (ie, i) v =
    match ie with
    | Some ie when Offset.Index.Exp.is_all ie ->
      (* TODO: Doesn't seem to work for unassume because unrolled elements are top-initialized, not bot-initialized. *)
      (BatList.make (factor ()) v, v)
    | _ ->
      set ask (xl, xr) (ie, i) v

  let make ?(varAttr=[]) ?(typAttr=[]) _ v =
    let xl = BatList.make (factor ()) v in
    (xl,Val.bot ())
  let length _ = None
  let move_if_affected ?(replace_with_const=false) _ x _ _ = x
  let get_vars_in_e _ = []
  let map f (xl, xr) = ((List.map f xl), f xr)
  let fold_left f a x = f a (join_of_all_parts x)
  let printXml f (xl,xr) = BatPrintf.fprintf f "<value>\n<map>\n
  <key>unrolled array</key>\n
  <key>xl</key>\n%a\n\n
  <key>xm</key>\n%a\n\n
  </map></value>\n" Base.printXml xl Val.printXml xr
  let smart_join _ _ = join
  let smart_widen _ _ = widen
  let smart_leq _ _ = leq
  let update_length _ x = x
  let project ?(varAttr=[]) ?(typAttr=[]) _ t = t

  let invariant ~value_invariant ~offset ~lval ((xl, xr) as x) =
    match offset with
    (* invariants for all indices *)
    | NoOffset ->
      let i_all =
        if Val.is_bot xr then
          Invariant.top ()
        else if get_bool "witness.invariant.goblint" then (
          let i_lval = Cil.addOffsetLval (Index (Lazy.force Offset.Index.Exp.all, NoOffset)) lval in
          value_invariant ~offset ~lval:i_lval (join_of_all_parts x)
        )
        else
          Invariant.top ()
      in
      BatList.fold_lefti (fun acc i x ->
          let i_lval = Cil.addOffsetLval (Index (Cil.integer i, NoOffset)) lval in
          let i = value_invariant ~offset ~lval:i_lval x in
          Invariant.(acc && i)
        ) i_all xl
    (* invariant for one index *)
    | Index (i, offset) ->
      Invariant.none (* TODO: look up *)
    (* invariant for one field *)
    | Field (f, offset) ->
      Invariant.none
end

(** Special signature so that we can use the _with_length functions from PartitionedWithLength but still match the interface *
  * defined for array domains *)
module type SPartitioned =
sig
  include S
  val set_with_length: idx option -> VDQ.t -> t -> Basetype.CilExp.t option * idx -> value -> t
  val smart_join_with_length: idx option -> (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t -> t
  val smart_widen_with_length: idx option -> (exp -> Z.t option) -> (exp -> Z.t option)  -> t -> t-> t
  val smart_leq_with_length: idx option -> (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t -> bool
  val move_if_affected_with_length: ?replace_with_const:bool -> idx option -> VDQ.t -> t -> Cil.varinfo -> (Cil.exp -> int option) -> t
end

module Partitioned (Val: LatticeWithSmartOps) (Idx:IntDomain.Z): SPartitioned with type value = Val.t and type idx = Idx.t =
struct
  include Printable.Std

  type t = Joint of Val.t | Partitioned of (CilType.Exp.t * (Val.t * Val.t * Val.t)) [@@deriving eq, ord, hash]

  type idx = Idx.t
  type value = Val.t

  let domain_of_t _ = PartitionedDomain

  let name () = "partitioned array"

  let relift = function
    | Joint v -> Joint (Val.relift v)
    | Partitioned (e, (l, m, r)) -> Partitioned (CilType.Exp.relift e, (Val.relift l, Val.relift m, Val.relift r))

  let join_of_all_parts = function
    | Joint v -> v
    | Partitioned (e, (xl, xm, xr)) -> Val.join xl (Val.join xm xr)

  (** Ensures an array where all three Val are equal, is represented by an unpartitioned array *)
  let normalize = function
    | Joint v -> Joint v
    | (Partitioned (e, (xl, xm, xr)) as p) ->
      if Val.equal xl xm && Val.equal xm xr then Joint xl
      else p

  let leq (x:t) (y:t) =
    match x, y with
    | Joint x, Joint y -> Val.leq x y
    | Partitioned (e,(xl, xm, xr)), Joint y -> Val.leq xl y && Val.leq xm y && Val.leq xr y
    | Partitioned (e,(xl, xm, xr)), Partitioned (e',(yl, ym, yr)) ->
      CilType.Exp.equal e e' && Val.leq xl yl && Val.leq xm ym && Val.leq xr yr
    | Joint x, Partitioned (e, (xl, xm, xr)) -> Val.leq x xl && Val.leq x xm && Val.leq x xr

  let bot () = Joint (Val.bot ())
  let is_bot (x:t) = Val.is_bot (join_of_all_parts x)
  let top () = Joint (Val.top ())
  let is_top = function
    | Joint x -> Val.is_top x
    | _-> false

  let join (x:t) (y:t) = normalize @@
    match x, y with
    | Joint x, Joint y -> Joint (Val.join x y)
    | Partitioned (e,(xl, xm, xr)), Joint y -> Partitioned (e,(Val.join xl y, Val.join xm y, Val.join xr y))
    | Joint x, Partitioned (e,(yl, ym, yr)) -> Partitioned (e,(Val.join x yl, Val.join x ym, Val.join x yr))
    | Partitioned (e,(xl, xm, xr)), Partitioned (e',(yl, ym, yr)) ->
      if CilType.Exp.equal e e' then Partitioned (e,(Val.join xl yl, Val.join xm ym, Val.join xr yr))
      else Joint (Val.join (join_of_all_parts x) (join_of_all_parts y))

  let widen (x:t) (y:t) = normalize @@ match x,y with
    | Joint x, Joint y -> Joint (Val.widen x y)
    | Partitioned (e,(xl, xm, xr)), Joint y -> Partitioned (e,(Val.widen xl y, Val.widen xm y, Val.widen xr y))
    | Joint x, Partitioned (e,(yl, ym, yr)) -> Partitioned (e,(Val.widen x yl, Val.widen x ym, Val.widen x yr))
    | Partitioned (e,(xl, xm, xr)), Partitioned (e',(yl, ym, yr)) ->
      if CilType.Exp.equal e e' then Partitioned (e,(Val.widen xl yl, Val.widen xm ym, Val.widen xr yr))
      else Joint (Val.widen (join_of_all_parts x) (join_of_all_parts y))

  let show = function
    | Joint x ->  "Array (no part.): " ^ Val.show x
    | Partitioned (e,(xl, xm, xr)) ->
      "Array (part. by " ^ CilType.Exp.show e ^ "): (" ^
      Val.show xl ^ " -- " ^
      Val.show xm ^ " -- " ^
      Val.show xr ^ ")"

  let pretty () x = text "Array: " ++ text (show x)
  let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y

  let printXml f = function
    | Joint x -> BatPrintf.fprintf f "<value>\n<map>\n<key>Any</key>\n%a\n</map>\n</value>\n" Val.printXml x
    | Partitioned (e,(xl, xm, xr)) ->
      BatPrintf.fprintf f "<value>\n<map>\n
          <key>Partitioned By</key>\n%a\n
          <key>l</key>\n%a\n\n
          <key>m</key>\n%a\n\n
          <key>r</key>\n%a\n\n
        </map></value>\n" CilType.Exp.printXml e Val.printXml xl Val.printXml xm Val.printXml xr

  let to_yojson = function
    | Joint x -> `Assoc [ ("any", Val.to_yojson x) ]
    | Partitioned (e,(xl, xm, xr)) ->
      `Assoc [ ("partitioned_by", CilType.Exp.to_yojson e);
               ("l", Val.to_yojson xl);
               ("m", Val.to_yojson xm);
               ("r", Val.to_yojson xr) ]

  let get ?(checkBounds=true) (ask:VDQ.t) (x:t) (i,_) =
    match x, i with
    | Joint v, _ -> v
    | Partitioned (e, (xl, xm, xr)), Some i' ->
      begin
        if VDQ.must_be_equal ask.eval_int e i' then xm
        else
          begin
            let contributionLess = match VDQ.may_be_less ask.eval_int i' e with        (* (may i < e) ? xl : bot *)
              | false -> Val.bot ()
              | _ -> xl in
            let contributionEqual = match VDQ.may_be_equal ask.eval_int i' e with      (* (may i = e) ? xm : bot *)
              | false -> Val.bot ()
              | _ -> xm in
            let contributionGreater =  match VDQ.may_be_less ask.eval_int e i' with    (* (may i > e) ? xr : bot *)
              | false -> Val.bot ()
              | _ -> xr in
            Val.join (Val.join contributionLess contributionEqual) contributionGreater
          end
      end
    | _ -> join_of_all_parts x

  let get_vars_in_e = function
    | Partitioned (e, _) -> Basetype.CilExp.get_vars e
    | _ -> []

  (* expressions containing globals or array accesses are not suitable for partitioning *)
  let not_allowed_for_part e =
    let rec contains_array_access e =
      let rec offset_contains_array_access offs =
        match offs with
        | NoOffset -> false
        | Index _ -> true
        | Field (_, o) -> offset_contains_array_access o
      in
      match e with
      |	Const _
      |	SizeOf _
      |	SizeOfE _
      |	SizeOfStr _
      |	AlignOf _
      |	AlignOfE _ -> false
      | Question(e1, e2, e3, _) ->
        contains_array_access e1 || contains_array_access e2 || contains_array_access e3
      |	CastE(_, _, e)
      |	UnOp(_, e , _)
      | Real e
      | Imag e -> contains_array_access e
      |	BinOp(_, e1, e2, _) -> contains_array_access e1 || contains_array_access e2
      | AddrOf _
      | AddrOfLabel _
      | StartOf _ -> false
      | Lval(Mem e, o) -> offset_contains_array_access o || contains_array_access e
      | Lval(Var _, o) -> offset_contains_array_access o
    in
    let vars = Basetype.CilExp.get_vars e in
    List.exists (fun x -> x.vglob) vars || contains_array_access e


  let map f = function
    | Joint v -> Joint (f v)
    | Partitioned (e,(xl, xm, xr)) -> normalize @@ Partitioned (e,(f xl, f xm, f xr))

  let fold_left f a = function
    | Joint x -> f a x
    | Partitioned (_, (xl,xm,xr)) -> f (f (f a xl) xm) xr

  let move_if_affected_with_length ?(replace_with_const=false) length (ask:VDQ.t) x (v:varinfo) (movement_for_exp: exp -> int option) =
    normalize @@
    let move (i:int option) (e, (xl,xm, xr)) =
      match i with
      | Some 0   ->
        Partitioned (e, (xl, xm, xr))
      | Some 1   ->
        Partitioned (e, (Val.join xl xm, xr, xr)) (* moved one to the right *)
      | Some -1  ->
        Partitioned (e, (xl, xl, Val.join xm xr)) (* moved one to the left  *)
      | Some x when x > 1 ->
        Partitioned (e, (Val.join (Val.join xl xm) xr, xr, xr)) (* moved more than one to the right *)
      | Some x when x < -1 ->
        Partitioned (e, (xl, xl, Val.join (Val.join xl xm) xr)) (* moved more than one to the left *)
      | _ ->
        begin
          let nval = join_of_all_parts x in
          let default = Joint nval in
          if replace_with_const then
            let n = ask.eval_int e in
            match VDQ.ID.to_int n with
            | Some i ->
              Partitioned ((Cil.kintegerCilint (Cilfacade.ptrdiff_ikind ()) i), (xl, xm, xr))
            | _ -> default
          else
            default
        end
    in
    match x with
    | Partitioned (e, (xl,xm, xr)) ->
      let is_affected = Basetype.CilExp.occurs v e in
      if not is_affected then
        x
      else
        (* check if one part covers the entire array, so we can drop partitioning *)
        let e_must_bigger_max_index = GobOption.exists (fun i ->
            let b = VDQ.may_be_less ask.eval_int e (Cil.kintegerCilint (Cilfacade.ptrdiff_ikind ()) i) in
            not b (* !(e <_{may} length) => e >=_{must} length *)
          ) (Option.bind length Idx.to_int)
        in

        if e_must_bigger_max_index then
          (* Entire array is covered by left part, dropping partitioning. *)
          Joint xl
        else
          let e_must_less_zero  =
            VDQ.eval_int_binop (module BoolDomain.MustBool) Lt ask.eval_int e Cil.zero (* TODO: untested *)
          in
          if e_must_less_zero then
            (* Entire array is covered by right value, dropping partitioning. *)
            Joint xr
          else
            (* If we can not drop partitioning, move *)
            move (movement_for_exp e) (e, (xl,xm, xr))

    | _ -> x (* If the array is not partitioned, nothing to do *)

  let move_if_affected ?replace_with_const = move_if_affected_with_length ?replace_with_const None

  let set_with_length length (ask:VDQ.t) x (i,_) a =
    if M.tracing then M.trace "update_offset" "part array set_with_length %a %s %a" pretty x (BatOption.map_default Basetype.CilExp.show "None" i) Val.pretty a;
    match i with
    | Some i when Offset.Index.Exp.is_all i ->
      (* TODO: Doesn't seem to work for unassume. *)
      Joint a
    | Some i when Offset.Index.Exp.is_any i ->
      (assert !AnalysisState.global_initialization; (* just joining with xm here assumes that all values will be set, which is guaranteed during inits *)
       (* the join is needed here! see e.g 30/04 *)
       let o = match x with Partitioned (_, (_, xm, _)) -> xm | Joint v -> v in
       let r =  Val.join o a in
       Joint r)
    | _ ->
      normalize @@
      let use_last = get_string "ana.base.partition-arrays.keep-expr" = "last" in
      let exp_value e =
        let n = ask.eval_int e in
        VDQ.ID.to_int n
      in
      (* TODO: use ID.equal_to here, VDQ.ID doesn't have though *)
      let equals_zero e = GobOption.exists (Z.equal Z.zero) (exp_value e) in
      let equals_maxIndex e =
        GobOption.exists2 (fun l -> Z.equal (Z.pred l)) (Option.bind length Idx.to_int) (exp_value e)
      in
      let lubIfNotBot x = if Val.is_bot x then x else Val.join a x in
      match x with
      | Joint v ->
        (match i with
         | Some i when not @@ not_allowed_for_part i ->
           let l = if equals_zero i then Val.bot () else join_of_all_parts x in
           let r = if equals_maxIndex i then Val.bot () else join_of_all_parts x in
           Partitioned (i, (l, a, r))
         | _ -> Joint (Val.join v a)
        )
      | Partitioned (e, (xl, xm, xr)) ->
        let isEqual = VDQ.must_be_equal ask.eval_int in
        match i with
        | Some i' when not use_last || not_allowed_for_part i' -> begin
            let default =
              let left =
                match VDQ.may_be_less ask.eval_int i' e with     (* (may i < e) ? xl : bot *) (* TODO: untested *)
                | false -> xl
                | _ -> lubIfNotBot xl in
              let middle =
                match VDQ.may_be_equal ask.eval_int i' e with    (* (may i = e) ? xm : bot *)
                | false -> xm
                | _ -> Val.join xm a in
              let right =
                match VDQ.may_be_less ask.eval_int e i' with     (* (may i > e) ? xr : bot *) (* TODO: untested *)
                | false -> xr
                | _ -> lubIfNotBot xr in
              Partitioned (e, (left, middle, right))
            in
            if isEqual e i' then
              (*  e = _{must} i => update strongly *)
              Partitioned (e, (xl, a, xr))
            else if Cil.isConstant e && Cil.isConstant i' then
              match Cil.getInteger e, Cil.getInteger i' with
              | Some (e'': Cilint.cilint), Some i'' ->
                if Z.equal  i'' (Z.succ e'') then
                  (* If both are integer constants and they are directly adjacent, we change partitioning to maintain information *)
                  Partitioned (i', (Val.join xl xm, a, xr))
                else if Z.equal e'' (Z.succ i'') then
                  Partitioned (i', (xl, a, Val.join xm xr))
                else
                  default
              | _ ->
                default
            else
              default
          end
        | Some i' ->
          if isEqual e i' then
            Partitioned (e, (xl, a, xr))
          else
            let left = if equals_zero i' then Val.bot () else Val.join xl @@ Val.join
                  (match VDQ.may_be_equal ask.eval_int e i' with (* TODO: untested *)
                   | false -> Val.bot()
                   | _ -> xm) (* if e' may be equal to i', but e' may not be smaller than i' then we only need xm *)
                  (
                    let t = Cilfacade.typeOf e in
                    let ik = Cilfacade.get_ikind t in
                    match VDQ.must_be_equal ask.eval_int (BinOp(PlusA, e, Cil.kinteger ik 1, t)) i' with
                    | true -> xm
                    | _ ->
                      begin
                        match VDQ.may_be_less ask.eval_int e i' with (* TODO: untested *)
                        | false-> Val.bot()
                        | _ -> Val.join xm xr (* if e' may be less than i' then we also need xm for sure *)
                      end
                  )
            in
            let right = if equals_maxIndex i' then Val.bot () else  Val.join xr @@  Val.join
                  (match VDQ.may_be_equal ask.eval_int e i' with (* TODO: untested *)
                   | false -> Val.bot()
                   | _ -> xm)

                  (
                    let t = Cilfacade.typeOf e in
                    let ik = Cilfacade.get_ikind t in
                    match VDQ.must_be_equal ask.eval_int (BinOp(PlusA, e, Cil.kinteger ik (-1), t)) i' with (* TODO: untested *)
                    | true -> xm
                    | _ ->
                      begin
                        match VDQ.may_be_less ask.eval_int i' e with (* TODO: untested *)
                        | false -> Val.bot()
                        | _ -> Val.join xl xm (* if e' may be less than i' then we also need xm for sure *)
                      end
                  )
            in
            (* The new thing is partitioned according to i so we can strongly update *)
            Partitioned (i',(left, a, right))
        | _ ->
          (* If the expression used to write is not known, all segments except the empty ones will be affected *)
          Partitioned (e, (lubIfNotBot xl, Val.join xm a, lubIfNotBot xr))

  let set = set_with_length None


  let make ?(varAttr=[]) ?(typAttr=[]) i v:t =
    if Idx.to_int i = Some Z.one  then
      Partitioned ((Cil.integer 0), (v, v, v))
    else if Val.is_bot v then
      Joint (Val.bot ())
    else
      Joint v

  let length _ = None

  let must_i_one_smaller l i =
    GobOption.exists2 (fun l i -> Z.equal i (Z.pred l)) (Option.bind l Idx.to_int) i

  let must_be_zero = GobOption.exists (Z.equal Z.zero)

  let smart_op (op: Val.t -> Val.t -> Val.t) length x1 x2 x1_eval_int x2_eval_int =
    normalize @@
    let must_be_length_minus_one = must_i_one_smaller length in
    let op_over_all = op (join_of_all_parts x1) (join_of_all_parts x2) in
    match x1, x2 with
    | Partitioned (e1, (xl1, xm1, xr1)), Partitioned (e2, (xl2, xm2, xr2)) when Basetype.CilExp.equal e1 e2 ->
      Partitioned (e1, (op xl1 xl2, op xm1 xm2, op xr1 xr2))
    | Partitioned (e1, (xl1, xm1, xr1)), Partitioned (e2, (xl2, xm2, xr2)) ->
      if get_string "ana.base.partition-arrays.keep-expr" = "last" || get_bool "ana.base.partition-arrays.smart-join" then
        let op = Val.join in (* widen between different components isn't called validly *)
        let over_all_x1 = op (op xl1 xm1) xr1 in
        let over_all_x2 = op (op xl2 xm2) xr2 in
        let e1_in_state_of_x2 = x2_eval_int e1 in
        let e2_in_state_of_x1 = x1_eval_int e2 in
        (* TODO: why does this depend on exp comparison? probably to use "simpler" expression according to constructor order in compare *)
        (* It is mostly SOME order to ensure commutativity of join *)
        let e1_is_better = (not (Cil.isConstant e1) && Cil.isConstant e2) || Basetype.CilExp.compare e1 e2 < 0 in
        if e1_is_better then (* first try if the result can be partitioned by e1e *)
          if must_be_zero e1_in_state_of_x2  then
            Partitioned (e1, (xl1, op xm1 over_all_x2, op xr1 over_all_x2))
          else if must_be_length_minus_one e1_in_state_of_x2  then
            Partitioned (e1, (op xl1 over_all_x2, op xm1 over_all_x2, xr1))
          else if must_be_zero e2_in_state_of_x1 then
            Partitioned (e2, (xl2, op over_all_x1 xm2, op over_all_x1 xr2))
          else if must_be_length_minus_one e2_in_state_of_x1 then
            Partitioned (e2, (op over_all_x1 xl2, op over_all_x1 xm2, xr2))
          else
            Joint op_over_all
        else  (* first try if the result can be partitioned by e2e *)
        if must_be_zero e2_in_state_of_x1 then
          Partitioned (e2, (xl2, op over_all_x1 xm2, op over_all_x1 xr2))
        else if must_be_length_minus_one e2_in_state_of_x1 then
          Partitioned (e2, (op over_all_x1 xl2, op over_all_x1 xm2, xr2))
        else if must_be_zero e1_in_state_of_x2 then
          Partitioned (e1, (xl1, op xm1 over_all_x2, op xr1 over_all_x2))
        else if must_be_length_minus_one e1_in_state_of_x2 then
          Partitioned (e1, (op xl1 over_all_x2, op xm1 over_all_x2, xr1))
        else
          Joint op_over_all
      else
        Joint op_over_all
    | Joint _, Joint _ ->
      Joint op_over_all
    | Joint x1, Partitioned (e2, (xl2, xm2, xr2)) ->
      if must_be_zero (x1_eval_int e2) then
        Partitioned (e2, (xl2, op x1 xm2, op x1 xr2))
      else if must_be_length_minus_one (x1_eval_int e2) then
        Partitioned (e2, (op x1 xl2, op x1 xm2, xr2))
      else
        Joint op_over_all
    | Partitioned (e1, (xl1, xm1, xr1)), Joint x2 ->
      if must_be_zero (x2_eval_int e1) then
        Partitioned (e1, (xl1, op xm1 x2, op xr1 x2))
      else if must_be_length_minus_one (x2_eval_int e1) then
        Partitioned (e1, (op xl1 x2, op xm1 x2, xr1))
      else
        Joint op_over_all

  let smart_join_with_length length x1_eval_int x2_eval_int x1 x2 =
    smart_op (Val.smart_join x1_eval_int x2_eval_int) length x1 x2 x1_eval_int x2_eval_int

  let smart_widen_with_length length x1_eval_int x2_eval_int x1 x2  =
    smart_op (Val.smart_widen x1_eval_int x2_eval_int) length x1 x2 x1_eval_int x2_eval_int

  let smart_leq_with_length length x1_eval_int x2_eval_int x1 x2 =
    let leq' = Val.smart_leq x1_eval_int x2_eval_int in
    let must_be_length_minus_one = must_i_one_smaller length in
    match x1, x2 with
    | Joint x1, Joint x2 ->
      leq' x1 x2
    | Partitioned (e1, (xl1, xm1, xr1)), Joint x2 ->
      (* leq' (Val.join xl1 (Val.join xm1 xr1)) (Val.join xl2 (Val.join xm2 xr2)) *)
      leq' xl1 x2 && leq' xm1 x2 && leq' xr1 x2
    | Partitioned (e1, (xl1, xm1, xr1)), Partitioned (e2, (xl2, xm2, xr2)) ->
      if Basetype.CilExp.equal e1 e2 then
        leq' xl1 xl2 && leq' xm1 xm2 && leq' xr1 xr2
      else if must_be_zero (x1_eval_int e2) then
        (* A read will never be from xl2 -> we can ignore that here *)
        let l = join_of_all_parts x1 in
        leq' l xm2 && leq' l xr2
      else if must_be_length_minus_one (x1_eval_int e2) then
        (* A read will never be from xr2 -> we can ignore that here *)
        let l = join_of_all_parts x1 in
        leq' l xl2 && leq' l xm2
      else
        false
    | Joint x1, Partitioned (e2, (xl2, xm2, xr2)) ->
      if must_be_zero (x1_eval_int e2) then
        leq' x1 xm2 && leq' x1 xr2
      else if must_be_length_minus_one (x1_eval_int e2) then
        leq' x1 xl2 && leq' x1 xm2
      else
        leq' x1 xl2 && leq' x1 xr2 && leq' x1 xm2 && leq' x1 xr2

  let smart_join = smart_join_with_length None
  let smart_widen = smart_widen_with_length None
  let smart_leq = smart_leq_with_length None

  let meet x y = normalize @@ match x,y with
    | Joint x, Joint y -> Joint (Val.meet x y)
    | Joint x, Partitioned (e, (xl, xm, xr))
    | Partitioned (e, (xl, xm, xr)), Joint x ->
      Partitioned (e, (Val.meet x xl, Val.meet x xm, Val.meet x xr))
    | Partitioned (e1, (xl1, xm1, xr1)), Partitioned (e2, (xl2, xm2, xr2)) ->
      if Basetype.CilExp.equal e1 e2 then
        Partitioned (e1, (Val.meet xl1 xl2, Val.meet xm1 xm2, Val.meet xr1 xr2))
      else
        (* partitioned according to two different expressions -> meet can not be element-wise *)
        (* arrays can not be partitioned according to multiple expressions, arbitrary prefer the first one here *)
        (* TODO: do smart things if the relationship between e1e and e2e is known *)
        x

  let narrow x y = normalize @@ match x,y with
    | Joint x, Joint y -> Joint (Val.narrow x y)
    | Joint x, Partitioned (e, (xl, xm, xr))
    | Partitioned (e, (xl, xm, xr)), Joint x ->
      Partitioned (e, (Val.narrow x xl, Val.narrow x xm, Val.narrow x xr))
    | Partitioned (e1, (xl1, xm1, xr1)), Partitioned (e2, (xl2, xm2, xr2)) ->
      if Basetype.CilExp.equal e1 e2 then
        Partitioned (e1, (Val.narrow xl1 xl2, Val.narrow xm1 xm2, Val.narrow xr1 xr2))
      else
        (* partitioned according to two different expressions -> narrow can not be element-wise *)
        (* arrays can not be partitioned according to multiple expressions, arbitrary prefer the first one here *)
        x

  let update_length _ x = x
  let project ?(varAttr=[]) ?(typAttr=[]) _ t = t

  let invariant ~value_invariant ~offset ~lval x =
    match offset with
    (* invariants for all indices *)
    | NoOffset when get_bool "witness.invariant.goblint" ->
      let i_lval = Cil.addOffsetLval (Index (Lazy.force Offset.Index.Exp.all, NoOffset)) lval in
      value_invariant ~offset ~lval:i_lval (join_of_all_parts x)
    | NoOffset ->
      Invariant.none
    (* invariant for one index *)
    | Index (i, offset) ->
      Invariant.none (* TODO: look up *)
    (* invariant for one field *)
    | Field (f, offset) ->
      Invariant.none
end

(* This is the main array out of bounds check *)
let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l) (e, v) =
  if !AnalysisState.executing_speculative_computations then
    ()
  else if GobConfig.get_bool "ana.arrayoob" then (* The purpose of the following 2 lines is to give the user extra info about the array oob *)
    let idx_before_end = Idx.lt v l in (* check whether index is before the end of the array *)
    let idx_after_start = Idx.ge v (Idx.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero) in (* check whether the index is non-negative *)
    (* For an explanation of the warning types check the Pull Request #255 *)
    match idx_after_start, idx_before_end with
    | Some true, Some true -> (* Certainly in bounds on both sides.*)
      Checks.safe Checks.Category.InvalidMemoryAccess
    | Some true, Some false -> (* The following matching differentiates the must and may cases*)
      AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
      M.error ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.past_end "Must access array past end";
      Checks.error Checks.Category.InvalidMemoryAccess "Invalid array access: Must access past end"
    | Some true, None ->
      AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
      M.warn ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.past_end "May access array past end";
      Checks.warn Checks.Category.InvalidMemoryAccess "Invalid array access: May access past end"
    | Some false, Some true ->
      AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
      M.error ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.before_start "Must access array before start";
      Checks.error Checks.Category.InvalidMemoryAccess "Invalid array access: Must access before start"
    | None, Some true ->
      AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
      M.warn ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.before_start "May access array before start";
      Checks.warn Checks.Category.InvalidMemoryAccess "Invalid array access: May access before start"
    | _ ->
      AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
      M.warn ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.unknown "May access array out of bounds";
      Checks.warn Checks.Category.InvalidMemoryAccess "Invalid array access: May access out of bounds"


module TrivialWithLength (Val: LatticeWithInvalidate) (Idx: IntDomain.Z): S with type value = Val.t and type idx = Idx.t =
struct
  module Base = Trivial (Val) (Idx)
  include Lattice.Prod (Base) (Idx)
  type idx = Idx.t
  type value = Val.t

  let domain_of_t _ = TrivialDomain

  let get ?(checkBounds=true) (ask : VDQ.t) (x, (l : idx)) (e, v) =
    if checkBounds then (array_oob_check (module Idx) (x, l) (e, v));
    Base.get ask x (e, v)
  let set (ask: VDQ.t) (x,l) i v = Base.set ask x i v, l
  let make ?(varAttr=[]) ?(typAttr=[])  l x = Base.make l x, l
  let length (_,l) = Some l
  let move_if_affected ?(replace_with_const=false) _ x _ _ = x
  let map f (x, l):t = (Base.map f x, l)
  let fold_left f a (x, l) = Base.fold_left f a x
  let get_vars_in_e _ = []

  let smart_join _ _ = join
  let smart_widen _ _ = widen
  let smart_leq _ _ = leq

  (* It is not necessary to do a least-upper bound between the old and the new length here.   *)
  (* Any array can only be declared in one location. The value for newl that we get there is  *)
  (* the one obtained by abstractly evaluating the size expression at this location for the   *)
  (* current state. If newl leq l this means that we somehow know more about the expression   *)
  (* determining the size now (e.g. because of narrowing), but this holds for all the times   *)
  (* the declaration is visited. *)
  let update_length newl (x, l) = (x, newl)

  let project ?(varAttr=[]) ?(typAttr=[]) _ t = t

  let invariant ~value_invariant ~offset ~lval (x, _) =
    Base.invariant ~value_invariant ~offset ~lval x

  let printXml f (x,y) =
    BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Base.name ())) Base.printXml x "length" Idx.printXml y

  let to_yojson (x, y) = `Assoc [ (Base.name (), Base.to_yojson x); ("length", Idx.to_yojson y) ]
end


module PartitionedWithLength (Val: LatticeWithSmartOps) (Idx: IntDomain.Z): S with type value = Val.t and type idx = Idx.t =
struct
  module Base = Partitioned (Val) (Idx)
  include Lattice.Prod (Base) (Idx)
  type idx = Idx.t
  type value = Val.t

  let domain_of_t _ = PartitionedDomain

  let get ?(checkBounds=true) (ask : VDQ.t) (x, (l : idx)) (e, v) =
    if checkBounds then (array_oob_check (module Idx) (x, l) (e, v));
    Base.get ask x (e, v)
  let set ask (x,l) i v = Base.set_with_length (Some l) ask x i v, l
  let make ?(varAttr=[]) ?(typAttr=[])  l x = Base.make l x, l
  let length (_,l) = Some l

  let move_if_affected ?replace_with_const ask (x,l) v i =
    (Base.move_if_affected_with_length ?replace_with_const (Some l) ask x v i), l

  let map f (x, l):t = (Base.map f x, l)
  let fold_left f a (x, l) = Base.fold_left f a x
  let get_vars_in_e (x, _) = Base.get_vars_in_e x

  let smart_join x_eval_int y_eval_int (x,xl) (y,yl) =
    let l = Idx.join xl yl in
    (Base.smart_join_with_length (Some l) x_eval_int y_eval_int x y , l)

  let smart_widen x_eval_int y_eval_int (x,xl) (y,yl) =
    let l = Idx.join xl yl in
    (Base.smart_widen_with_length (Some l) x_eval_int y_eval_int x y, l)

  let smart_leq x_eval_int y_eval_int (x,xl) (y,yl)  =
    let l = Idx.join xl yl in
    Idx.leq xl yl && Base.smart_leq_with_length (Some l) x_eval_int y_eval_int x y

  (* It is not necessary to do a least-upper bound between the old and the new length here.   *)
  (* Any array can only be declared in one location. The value for newl that we get there is  *)
  (* the one obtained by abstractly evaluating the size expression at this location for the   *)
  (* current state. If newl leq l this means that we somehow know more about the expression   *)
  (* determining the size now (e.g. because of narrowing), but this holds for all the times   *)
  (* the declaration is visited. *)
  let update_length newl (x, l) = (x, newl)

  let project ?(varAttr=[]) ?(typAttr=[]) _ t = t

  let invariant ~value_invariant ~offset ~lval (x, _) =
    Base.invariant ~value_invariant ~offset ~lval x

  let printXml f (x,y) =
    BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Base.name ())) Base.printXml x "length" Idx.printXml y

  let to_yojson (x, y) = `Assoc [ (Base.name (), Base.to_yojson x); ("length", Idx.to_yojson y) ]
end

module UnrollWithLength (Val: LatticeWithInvalidate) (Idx: IntDomain.Z): S with type value = Val.t and type idx = Idx.t =
struct
  module Base = Unroll (Val) (Idx)
  include Lattice.Prod (Base) (Idx)
  type idx = Idx.t
  type value = Val.t

  let domain_of_t _ = UnrolledDomain

  let get ?(checkBounds=true) (ask : VDQ.t) (x, (l : idx)) (e, v) =
    if checkBounds then (array_oob_check (module Idx) (x, l) (e, v));
    Base.get ask x (e, v)
  let set (ask: VDQ.t) (x,l) i v = Base.set ask x i v, l
  let make ?(varAttr=[]) ?(typAttr=[]) l x = Base.make l x, l
  let length (_,l) = Some l

  let move_if_affected ?(replace_with_const=false) _ x _ _ = x
  let map f (x, l):t = (Base.map f x, l)
  let fold_left f a (x, l) = Base.fold_left f a x
  let get_vars_in_e _ = []

  let smart_join _ _ = join
  let smart_widen _ _ = widen
  let smart_leq _ _ = leq

  (* It is not necessary to do a least-upper bound between the old and the new length here.   *)
  (* Any array can only be declared in one location. The value for newl that we get there is  *)
  (* the one obtained by abstractly evaluating the size expression at this location for the   *)
  (* current state. If newl leq l this means that we somehow know more about the expression   *)
  (* determining the size now (e.g. because of narrowing), but this holds for all the times   *)
  (* the declaration is visited. *)
  let update_length newl (x, l) = (x, newl)

  let project ?(varAttr=[]) ?(typAttr=[]) _ t = t

  let invariant ~value_invariant ~offset ~lval (x, _) =
    Base.invariant ~value_invariant ~offset ~lval x

  let printXml f (x,y) =
    BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Base.name ())) Base.printXml x "length" Idx.printXml y

  let to_yojson (x, y) = `Assoc [ (Base.name (), Base.to_yojson x); ("length", Idx.to_yojson y) ]
end

module NullByte (Val: LatticeWithNull) (Idx: IntDomain.Z): Str with type value = Val.t and type idx = Idx.t =
struct
  module MustSet = NullByteSet.MustSet
  module MaySet = NullByteSet.MaySet
  module Nulls = NullByteSet.MustMaySet

  let (<.) = Z.lt
  let (<=.) = Z.leq
  let (>.) = Z.gt
  let (>=.) = Z.geq
  let (=.) = Z.equal
  let (+.) = Z.add

  (* (Must Null Set, May Null Set, Array Size) *)
  include Lattice.Prod (Nulls) (struct include Idx let name () = "length" end)

  let name () = "ArrayNullBytes"
  type idx = Idx.t
  type value = Val.t

  type ret = Null | NotNull | Maybe

  type substr = IsNotSubstr | IsSubstrAtIndex0 | IsMaybeSubstr

  module ArrayOobMessage = M.Category.Behavior.Undefined.ArrayOutOfBounds
  let warn_past_end ?loc ?tags fmt =
    (* Must do it this way to use same format string for multiple functions and also pass all arguments after.
       Just calling Checks.error and M.error with fmt as last argument will silently not call Checks.error! *)
    Pretty.gprintf (fun doc ->
        Checks.error Checks.Category.InvalidMemoryAccess "%a" Pretty.insert doc;
        M.error ~category:ArrayOobMessage.past_end ?loc ?tags "%a" Pretty.insert doc
      ) fmt

  let min_nat_of_idx i = Z.max Z.zero (BatOption.default Z.zero (Idx.minimal i))

  let get (ask: VDQ.t) (nulls, size) (e, i) =
    let min_i = min_nat_of_idx i in
    let max_i = Idx.maximal i in
    let min_size = min_nat_of_idx size in

    match max_i, Idx.maximal size with
    (* if there is no maximum value in index interval *)
    | None, _ when not (Nulls.exists Possibly ((<=.) min_i) nulls) ->
      (* ... return NotNull if no i >= min_i in may_nulls_set *)
      NotNull
    | None, _ ->
      (* ... else return Top *)
      Maybe
    (* if there is no maximum size *)
    | Some max_i, None when max_i >=. Z.zero ->
      (* ... and maximum value in index interval < minimal size, return Null if all numbers in index interval are in must_nulls_set *)
      if max_i <. min_size && Nulls.interval_mem Definitely (min_i,max_i) nulls then
        Null
        (* ... return NotNull if no number in index interval is in may_nulls_set *)
      else if not (Nulls.exists Possibly (fun x -> x >=. min_i && x <=. max_i) nulls) then
        NotNull
      else
        Maybe
    | Some max_i, Some max_size when max_i >=. Z.zero ->
      (* if maximum value in index interval < minimal size, return Null if all numbers in index interval are in must_nulls_set *)
      if max_i <. min_size && Nulls.interval_mem Definitely (min_i, max_i) nulls then
        Null
        (* if maximum value in index interval < maximal size, return NotNull if no number in index interval is in may_nulls_set *)
      else if max_i <. max_size && not (Nulls.exists Possibly (fun x -> x >=. min_i && x <=. max_i) nulls) then
        NotNull
      else
        Maybe
    (* if maximum number in interval is invalid, i.e. negative, return Top of value *)
    | _ -> Maybe

  let set (ask: VDQ.t) (nulls, size) (e, i) v =
    let min_size = min_nat_of_idx size in
    let min_i = min_nat_of_idx i in
    let max_i = Idx.maximal i in

    let set_exact_nulls i =
      match Idx.maximal size with
      (* if size has no upper limit *)
      | None ->
        (match Val.is_null v with
         | NotNull ->
           Nulls.remove (if Nulls.is_full_set Possibly nulls then Possibly else Definitely) i nulls min_size
         (* ... and value <> null, remove i from must_nulls_set and also from may_nulls_set if not top *)
         | Null ->
           Nulls.add (if i <. min_size then Definitely else Possibly) i nulls
         (* i < minimal size and value = null, add i to must_nulls_set and may_nulls_set *)
         (* i >= minimal size and value = null, add i only to may_nulls_set *)
         | Maybe ->
           let removed = Nulls.remove Possibly i nulls min_size in
           Nulls.add Possibly i removed)
      | Some max_size ->
        (match Val.is_null v with
         | NotNull ->
           Nulls.remove Definitely i nulls min_size
         (* if value <> null, remove i from must_nulls_set and may_nulls_set *)
         | Null when i <. min_size ->
           Nulls.add Definitely i nulls
         | Null when i <. max_size ->
           Nulls.add Possibly i nulls
         | Maybe when i <. max_size ->
           let removed = Nulls.remove Possibly i nulls min_size in
           Nulls.add Possibly i removed
         | _ -> nulls
        )
    in

    let set_interval min_i max_i =
      (* Update max_i so it is capped at the maximum size *)
      let max_i = BatOption.map_default (fun x -> Z.min max_i @@ Z.pred x) max_i (Idx.maximal size) in
      match Val.is_null v with
      | NotNull -> Nulls.remove_interval Possibly (min_i, max_i) min_size nulls
      | Null -> Nulls.add_interval ~maxfull:(Idx.maximal size) Possibly (min_i, max_i) nulls
      | Maybe ->
        let nulls = Nulls.add_interval ~maxfull:(Idx.maximal size) Possibly (min_i, max_i) nulls in
        Nulls.remove_interval Possibly (min_i, max_i) min_size nulls
    in

    (* warn if index is (potentially) out of bounds *)
    array_oob_check (module Idx) (Nulls.get_set Possibly, size) (e, i);
    let nulls = match max_i with
      (* if no maximum number in index interval *)
      | None ->
        (* ..., value = null *)
        (if Val.is_null v = Null && Idx.maximal size = None then
           match Idx.maximal size with
           (* ... and there is no maximal size, modify may_nulls_set to top *)
           | None ->  Nulls.add_all Possibly nulls
           (* ... and there is a maximal size, add all i from minimal index to maximal size to may_nulls_set *)
           | Some max_size -> Nulls.add_interval Possibly (min_i, Z.pred max_size) nulls
           (* ... and value <> null, only keep indexes < minimal index in must_nulls_set *)
         else if Val.is_null v = NotNull then
           Nulls.filter_musts (Z.gt min_i) min_size nulls
           (*..., value unknown *)
         else
           match Idx.minimal size, Idx.maximal size with
           (* ... and size unknown, modify both sets to top *)
           | None, None -> Nulls.top ()
           (* ... and only minimal size known, remove all indexes < minimal size from must_nulls_set and modify may_nulls_set to top *)
           | Some min_size, None ->
             let nulls = Nulls.add_all Possibly nulls in
             Nulls.filter_musts (Z.gt min_size) min_size nulls
           (* ... and only maximal size known, modify must_nulls_set to top and add all i from minimal index to maximal size to may_nulls_set *)
           | None, Some max_size ->
             let nulls = Nulls.remove_all Possibly nulls in
             Nulls.add_interval Possibly (min_i, Z.pred max_size) nulls
           (* ... and size is known, remove all indexes < minimal size from must_nulls_set and add all i from minimal index to maximal size to may_nulls_set *)
           | Some min_size, Some max_size ->
             let nulls = Nulls.filter_musts (Z.gt min_size) min_size nulls in
             Nulls.add_interval Possibly (min_i, Z.pred max_size) nulls
        )
      | Some max_i when max_i >=. Z.zero ->
        if min_i =. max_i then
          set_exact_nulls min_i
        else
          set_interval min_i max_i
      (* if maximum number in interval is invalid, i.e. negative, return tuple unmodified *)
      | _ -> nulls
    in
    (nulls, size)


  let make ?(varAttr=[]) ?(typAttr=[]) i v =
    let min_i, max_i = match Idx.minimal i, Idx.maximal i with
      | Some min_i, Some max_i ->
        if min_i <. Z.zero && max_i <. Z.zero then
          (M.error ~category:ArrayOobMessage.before_start "Tries to create an array of negative size";
           Checks.error Checks.Category.NegativeArraySize "Tries to create an array of negative size";
           Z.zero, Some Z.zero)
        else if min_i <. Z.zero then
          (M.warn ~category:ArrayOobMessage.before_start "May try to create an array of negative size";
           Checks.warn Checks.Category.NegativeArraySize "May try to create an array of negative size";
           Z.zero, Some max_i)
        else (
          Checks.safe Checks.Category.NegativeArraySize;
          min_i, Some max_i)
      | None, Some max_i ->
        if max_i <. Z.zero then
          (M.error ~category:ArrayOobMessage.before_start "Tries to create an array of negative size";
           Checks.error Checks.Category.NegativeArraySize "Tries to create an array of negative size";
           Z.zero, Some Z.zero)
        else (
          Checks.safe Checks.Category.NegativeArraySize;
          Z.zero, Some max_i
        )
      | Some min_i, None ->
        if min_i <. Z.zero then
          (M.warn ~category:ArrayOobMessage.before_start "May try to create an array of negative size";
           Checks.warn Checks.Category.NegativeArraySize "May try to create an array of negative size";
           Z.zero, None)
        else (
          Checks.safe Checks.Category.NegativeArraySize;
          min_i, None)
      | None, None ->
        Checks.safe Checks.Category.NegativeArraySize;
        Z.zero, None
    in
    let size = BatOption.map_default (fun max -> Idx.of_interval ILong (min_i, max)) (Idx.starting ILong min_i) max_i in
    match Val.is_null v with
    | Null -> (Nulls.make_all_must (), size)
    | NotNull -> (Nulls.empty (), size)
    | Maybe -> (Nulls.top (), size)


  let length (_, size) = Some size

  let move_if_affected ?(replace_with_const=false) _ x _ _ = x

  let get_vars_in_e _ = []

  let map f (nulls, size) =
    (* if f(null) = null, all values in must_nulls_set still are surely null;
     * assume top for may_nulls_set as checking effect of f for every possible value is unfeasbile *)
    match Val.is_null (f (Val.null ())) with
    | Null -> (Nulls.add_all Possibly nulls, size)
    | _ -> (Nulls.top (), size) (* else also return top for must_nulls_set *)

  let fold_left f acc _ = f acc (Val.top ())

  let smart_join _ _ = join
  let smart_widen _ _ = widen
  let smart_leq _ _ = leq

  (* string functions *)

  let to_null_byte_domain s =
    let last_null = Z.of_int (String.length s) in
    let rec build_set i set =
      if (Z.of_int i) >=. last_null then
        Nulls.Set.add last_null set
      else
        match String.index_from_opt s i '\x00' with
        | Some i -> build_set (i + 1) (Nulls.Set.add (Z.of_int i) set)
        | None -> Nulls.Set.add last_null set in
    let set = build_set 0 (Nulls.Set.empty ()) in
    (Nulls.precise_set set, Idx.of_int ILong (Z.succ last_null))

  (** Returns an abstract value with at most one null byte marking the end of the string *)
  let to_string ((nulls, size) as x:t):t =
    (* if must_nulls_set and min_nulls_set empty, definitely no null byte in array => warn about certain buffer overflow and return tuple unchanged *)
    if Nulls.is_empty Definitely nulls then
      (warn_past_end "Array access past end: buffer overflow"; x)
      (* if only must_nulls_set empty, no certainty about array containing null byte => warn about potential buffer overflow and return tuple unchanged *)
    else if Nulls.is_empty Possibly nulls then
      (warn_past_end "May access array past end: potential buffer overflow"; x)
    else
      (Checks.safe Checks.Category.InvalidMemoryAccess;
      let min_must_null = Nulls.min_elem Definitely nulls in
      let new_size = Idx.of_int ILong (Z.succ min_must_null) in
      let min_may_null = Nulls.min_elem Possibly nulls in
      (* if smallest index in sets coincides, only this null byte is kept in both sets *)
      let nulls =
        if min_must_null =. min_may_null then
          Nulls.precise_singleton min_must_null
          (* else return empty must_nulls_set and keep every index up to smallest index of must_nulls_set included in may_nulls_set *)
        else
          match Idx.maximal size with
          | Some max_size ->
            let nulls' = Nulls.remove_all Possibly nulls in
            Nulls.filter ~max_size (Z.leq min_must_null) nulls'
          | None when not (Nulls.may_can_benefit_from_filter nulls) ->
            Nulls.add_interval Possibly (Z.zero, min_must_null) (Nulls.empty ())
          | None ->
            let nulls' = Nulls.remove_all Possibly nulls in
            Nulls.filter (Z.leq min_must_null) nulls'
      in
      (nulls, new_size))

  (** [to_n_string index_set n] returns an abstract value with a potential null byte
    * marking the end of the string and if needed followed by further null bytes to obtain
    * an n bytes string. *)
  let to_n_string (nulls, size) n:t =
    if n < 0 then
      (Nulls.top (), Idx.top_of ILong)
    else
      let n = Z.of_int n in
      let warn_no_null min_must_null min_may_null =
        if Z.geq min_may_null n then (
          M.warn "Resulting string might not be null-terminated because src doesn't contain a null byte in the first n bytes";
          Checks.warn Checks.Category.StubCondition "Resulting string might not be null-terminated because src doesn't contain a null byte in the first n bytes")
        else
          (match min_must_null with
           | Some min_must_null when not (min_must_null >=. n || min_must_null >. min_may_null) -> Checks.safe Checks.Category.StubCondition
           | _ ->
             M.warn "Resulting string might not be null-terminated because src might not contain a null byte in the first n bytes";
             Checks.warn Checks.Category.StubCondition "Resulting string might not be null-terminated because src might not contain a null byte in the first n bytes"
          )
      in
      (match Idx.minimal size, Idx.maximal size with
       | Some min_size, Some max_size ->
         if n >. max_size then
           warn_past_end "Array size is smaller than n bytes; can cause a buffer overflow"
         else if n >. min_size then
           warn_past_end "Array size might be smaller than n bytes; can cause a buffer overflow"
         else
           Checks.safe Checks.Category.InvalidMemoryAccess
       | Some min_size, None ->
         if n >. min_size then
           warn_past_end "Array size might be smaller than n bytes; can cause a buffer overflow"
         else
           Checks.safe Checks.Category.InvalidMemoryAccess
       | None, Some max_size ->
         if n >. max_size then
           warn_past_end "Array size is smaller than n bytes; can cause a buffer overflow"
         else
           Checks.safe Checks.Category.InvalidMemoryAccess
       | None, None -> Checks.safe Checks.Category.InvalidMemoryAccess);
      let nulls =
        (* if definitely no null byte in array, i.e. must_nulls_set = may_nulls_set = empty set *)
        if Nulls.is_empty Definitely nulls then
          (warn_past_end
             "Resulting string might not be null-terminated because src doesn't contain a null byte";
           match Idx.maximal size with
           (* ... there *may* be null bytes from maximal size to n - 1 if maximal size < n (i.e. past end) *)
           | Some max_size when Z.geq max_size Z.zero -> Nulls.add_interval Possibly (max_size, Z.pred n) nulls
           | _ -> nulls)
          (* if only must_nulls_set empty, remove indexes >= n from may_nulls_set and add all indexes from minimal may null index to n - 1;
           * warn as in any case, resulting array not guaranteed to contain null byte *)
        else if Nulls.is_empty Possibly nulls then
          (Checks.safe Checks.Category.InvalidMemoryAccess;
          let min_may_null = Nulls.min_elem Possibly nulls in
          warn_no_null None min_may_null;
          if min_may_null =. Z.zero then
            Nulls.add_all Possibly nulls
          else
            let nulls = Nulls.add_interval Possibly (min_may_null, Z.pred n) nulls in
            Nulls.filter (fun x -> x <. n) nulls)
        else
          (Checks.safe Checks.Category.InvalidMemoryAccess;
          let min_must_null = Nulls.min_elem Definitely nulls in
          let min_may_null = Nulls.min_elem Possibly nulls in
          (* warn if resulting array may not contain null byte *)
          warn_no_null (Some min_must_null) min_may_null;
          (* if min_must_null = min_may_null, remove indexes >= n and add all indexes from minimal must/may null to n - 1 in the sets *)
          if min_must_null =. min_may_null then
            if min_must_null =. Z.zero then
              Nulls.full_set ()
            else
              let nulls = Nulls.add_interval Definitely (min_must_null, Z.pred n) nulls in
              let nulls = Nulls.add_interval Possibly (min_may_null, Z.pred n) nulls in
              Nulls.filter (fun x -> x <. n) nulls
          else if min_may_null =. Z.zero then
            Nulls.top ()
          else
            let nulls = Nulls.remove_all Possibly nulls in
            let nulls = Nulls.add_interval Possibly (min_may_null, Z.pred n) nulls in
            Nulls.filter (fun x -> x <. n) nulls)
      in
      (nulls,  Idx.of_int ILong n)

  let to_string_length (nulls, size) =
    (* if must_nulls_set and min_nulls_set empty, definitely no null byte in array => return interval [size, inf) and warn *)
    if Nulls.is_empty Definitely nulls then
      (warn_past_end "Array doesn't contain a null byte: buffer overflow";
       Idx.starting !Cil.kindOfSizeOf (BatOption.default Z.zero (Idx.minimal size))
      )
      (* if only must_nulls_set empty, no guarantee that null ever encountered in array => return interval [minimal may null, inf) and *)
    else if Nulls.is_empty Possibly nulls then
      (warn_past_end "Array might not contain a null byte: potential buffer overflow";
       Idx.starting !Cil.kindOfSizeOf (Nulls.min_elem Possibly nulls))
      (* else return interval [minimal may null, minimal must null] *)
    else (
      Checks.safe Checks.Category.InvalidMemoryAccess;
      Idx.of_interval !Cil.kindOfSizeOf (Nulls.min_elem Possibly nulls, Nulls.min_elem Definitely nulls))

  let string_copy (dstnulls, dstsize) ((srcnulls, srcsize) as src) n =
    let must_nulls_set1, may_nulls_set1 = dstnulls in
    (* filter out indexes before strlen(src) from dest sets and after strlen(src) from src sets and build union, keep size of dest *)
    let update_sets (truncatednulls, truncatedsize) len2 =
      let must_nulls_set2',may_nulls_set2' = truncatednulls in
      match Idx.minimal dstsize, Idx.maximal dstsize, Idx.minimal len2, Idx.maximal len2 with
      | Some min_dstsize, Some max_dstsize, Some min_srclen, Some max_srclen ->
        (if max_dstsize <. min_srclen then
           warn_past_end "The length of string src is greater than the allocated size for dest"
         else if min_dstsize <. max_srclen then
           warn_past_end "The length of string src may be greater than the allocated size for dest"
         else
           Checks.safe Checks.Category.InvalidMemoryAccess);
        let must_nulls_set_result =
          let min_size2 = BatOption.default Z.zero (Idx.minimal truncatedsize) in
          (* get must nulls from src string < minimal size of dest *)
          MustSet.filter ~min_size:min_size2 (Z.gt min_dstsize) must_nulls_set2'
          (* and keep indexes of dest >= maximal strlen of src *)
          |> MustSet.union (MustSet.filter ~min_size:min_dstsize (Z.leq max_srclen) must_nulls_set1) in
        let may_nulls_set_result =
          let max_size2 = BatOption.default max_dstsize (Idx.maximal truncatedsize) in
          (* get may nulls from src string < maximal size of dest *)
          MaySet.filter ~max_size:max_size2 (Z.gt max_dstsize) may_nulls_set2'
          (* and keep indexes of dest >= minimal strlen of src *)
          |> MaySet.union (MaySet.filter ~max_size:max_dstsize (Z.leq min_srclen) may_nulls_set1) in
        ((must_nulls_set_result, may_nulls_set_result), dstsize)


      | Some min_size1, None, Some min_len2, Some max_len2 ->
        (if min_size1 <. max_len2 then
           warn_past_end "The length of string src may be greater than the allocated size for dest"
         else
           Checks.safe Checks.Category.InvalidMemoryAccess);
        let must_nulls_set_result =
          let min_size2 = BatOption.default Z.zero (Idx.minimal truncatedsize) in
          MustSet.filter ~min_size: min_size2 (Z.gt min_size1) must_nulls_set2'
          |> MustSet.union (MustSet.filter ~min_size:min_size1 (Z.leq max_len2) must_nulls_set1) in
        let may_nulls_set_result =
          (* get all may nulls from src string as no maximal size of dest *)
          may_nulls_set2'
          |> MaySet.union (MaySet.filter ~max_size:(Z.succ min_len2) (Z.leq min_len2) may_nulls_set1)  in
        ((must_nulls_set_result, may_nulls_set_result), dstsize)
      | Some min_size1, Some max_size1, Some min_len2, None ->
        (if max_size1 <. min_len2 then
           warn_past_end "The length of string src is greater than the allocated size for dest"
         else if min_size1 <. min_len2 then
           warn_past_end"The length of string src may be greater than the allocated size for dest"
         else
           Checks.safe Checks.Category.InvalidMemoryAccess);
        (* do not keep any index of dest as no maximal strlen of src *)
        let must_nulls_set_result =
          let min_size2 = BatOption.default Z.zero (Idx.minimal truncatedsize) in
          MustSet.filter ~min_size:min_size2 (Z.gt min_size1) must_nulls_set2' in
        let may_nulls_set_result =
          let max_size2 = BatOption.default max_size1 (Idx.maximal truncatedsize) in
          MaySet.filter ~max_size:max_size2 (Z.gt max_size1) may_nulls_set2'
          |> MaySet.union (MaySet.filter ~max_size:max_size1 (Z.leq min_len2) may_nulls_set1) in
        ((must_nulls_set_result, may_nulls_set_result), dstsize)
      | Some min_size1, None, Some min_len2, None ->
        (if min_size1 <. min_len2 then
           warn_past_end "The length of string src may be greater than the allocated size for dest"
         else
           Checks.safe Checks.Category.InvalidMemoryAccess);
        (* do not keep any index of dest as no maximal strlen of src *)
        let min_size2 = BatOption.default Z.zero (Idx.minimal truncatedsize) in
        let truncatednulls = Nulls.remove_interval Possibly (Z.zero, min_size1) min_size2 truncatednulls in
        let filtered_dst = Nulls.filter ~max_size:(Z.succ min_len2) (Z.leq min_len2) dstnulls in
        (* get all may nulls from src string as no maximal size of dest *)
        (Nulls.union_mays truncatednulls filtered_dst, dstsize)
      (* any other case shouldn't happen as minimal index is always >= 0 *)
      | _ -> (Nulls.top (), dstsize) in

    (* warn if size of dest is (potentially) smaller than size of src and the latter (potentially) has no null byte at index < size of dest *)
    let sizes_warning srcsize =
      (match Idx.minimal dstsize, Idx.maximal dstsize, Idx.minimal srcsize, Idx.maximal srcsize with
       | Some min_dstsize, _, Some min_srcsize, _ when min_dstsize <. min_srcsize ->
         if not (Nulls.exists Possibly (Z.gt min_dstsize) srcnulls) then
           warn_past_end "src doesn't contain a null byte at an index smaller than the size of dest"
         else if not (Nulls.exists Definitely (Z.gt min_dstsize) srcnulls) then
           warn_past_end "src may not contain a null byte at an index smaller than the size of dest"
         else
           Checks.safe Checks.Category.InvalidMemoryAccess
       | Some min_dstsize, _, _, Some max_srcsize when min_dstsize <. max_srcsize ->
         if not (Nulls.exists Possibly (Z.gt min_dstsize) srcnulls) then
           warn_past_end "src doesn't contain a null byte at an index smaller than the size of dest"
         else if not (Nulls.exists Definitely (Z.gt min_dstsize) srcnulls) then
           warn_past_end "src may not contain a null byte at an index smaller than the size of dest"
         else
           Checks.safe Checks.Category.InvalidMemoryAccess
       | Some min_dstsize, _, _, None ->
         if not (Nulls.exists Definitely (Z.gt min_dstsize) srcnulls) then
           warn_past_end "src may not contain a null byte at an index smaller than the size of dest"
         else
           Checks.safe Checks.Category.InvalidMemoryAccess
       | _, Some mac_dstsize, _, Some max_srcsize when mac_dstsize <. max_srcsize ->
         if not (Nulls.exists Definitely (Z.gt mac_dstsize) srcnulls) then
           warn_past_end "src may not contain a null byte at an index smaller than the size of dest"
         else
           Checks.safe Checks.Category.InvalidMemoryAccess
       |_, Some max_dstsize, _, None ->
         if not (Nulls.exists Definitely (Z.gt max_dstsize) srcnulls) then
           warn_past_end "src may not contain a null byte at an index smaller than the size of dest"
         else
           Checks.safe Checks.Category.InvalidMemoryAccess
       | _ -> Checks.safe Checks.Category.InvalidMemoryAccess) in

    match n with
    (* strcpy *)
    | None ->
      sizes_warning srcsize;
      let truncated = to_string src in
      update_sets truncated (to_string_length src)
    (* strncpy = exactly n bytes from src are copied to dest *)
    | Some n when n >= 0 ->
      sizes_warning (Idx.of_int ILong (Z.of_int n));
      let truncated = to_n_string src n in
      update_sets truncated (Idx.of_int !Cil.kindOfSizeOf (Z.of_int n))
    | _ -> (Nulls.top (), dstsize)

  let string_concat (nulls1, size1) (nulls2, size2) n =
    let update_sets min_size1 max_size1 minlen1 maxlen1 minlen2 (maxlen2: Z.t option) nulls2' =
      (* track any potential buffer overflow and issue warning if needed *)
      (if GobOption.exists (fun x -> x <=. (minlen1 +. minlen2)) max_size1 then
         warn_past_end
           "The length of the concatenation of the strings in src and dest is greater than the allocated size for dest"
       else
         (match maxlen1, maxlen2 with
          | Some maxlen1, Some maxlen2 when min_size1 >. (maxlen1 +. maxlen2) -> Checks.safe Checks.Category.InvalidMemoryAccess
          | _ -> warn_past_end
                   "The length of the concatenation of the strings in src and dest may be greater than the allocated size for dest")
      );
      (* if any must_nulls_set empty, result must_nulls_set also empty;
       * for all i1, i2 in may_nulls_set1, may_nulls_set2: add i1 + i2 if it is <= strlen(dest) + strlen(src) to new may_nulls_set
       * and keep indexes > minimal strlen(dest) + strlen(src) of may_nulls_set *)
      if Nulls.is_empty Possibly nulls1 || Nulls.is_empty Possibly nulls2 then
        match max_size1 with
        | Some max_size1 ->
          let nulls1_no_must = Nulls.remove_all Possibly nulls1 in
          let pred = match maxlen1, maxlen2 with
            | Some maxlen1, Some maxlen2 -> (fun x -> x <=. (maxlen1 +. maxlen2))
            | _ -> (fun _ -> true)
          in
          let r =
            nulls1_no_must
            (* filter ensures we have the concete representation *)
            |> Nulls.filter ~max_size:max_size1 pred
            |> Nulls.elements ~max_size:max_size1 Possibly
            |> BatList.cartesian_product (Nulls.elements ~max_size:max_size1 Possibly nulls2')
            |> List.map (fun (i1, i2) -> i1 +. i2)
            |> (fun x -> Nulls.add_list Possibly x (Nulls.filter ~max_size:max_size1 (Z.lt (minlen1 +. minlen2)) nulls1_no_must))
            |> Nulls.filter (Z.gt max_size1)
          in
          (r, size1)
        | None when Nulls.may_can_benefit_from_filter nulls1 && Nulls.may_can_benefit_from_filter nulls2 ->
          (match maxlen1, maxlen2 with
           | Some maxlen1, Some maxlen2->
             let nulls1_no_must = Nulls.remove_all Possibly nulls1 in
             let r =
               nulls1_no_must
               (* filter ensures we have the concete representation *)
               |> Nulls.filter (fun x -> x <=. (maxlen1 +. maxlen2))
               |> Nulls.elements Possibly
               |> BatList.cartesian_product (Nulls.elements Possibly nulls2')
               |> List.map (fun (i1, i2) -> i1 +. i2)
               |> (fun x -> Nulls.add_list Possibly x (Nulls.filter (Z.lt (minlen1 +. minlen2)) nulls1_no_must))
             in
             (r, size1)
           | _ -> (Nulls.top (), size1))
        |  _ -> (Nulls.top (), size1)
        (* if minimal must null = minimal may null in ar1 and ar2, add them together and keep indexes > strlen(dest) + strlen(src) of ar1 *)
      else if Nulls.min_elem_precise nulls1 && Nulls.min_elem_precise nulls2' then
        let min_i1 = Nulls.min_elem Definitely nulls1 in
        let min_i2 = Nulls.min_elem Definitely nulls2' in
        let min_i = min_i1 +. min_i2 in
        let (must_nulls_set1, may_nulls_set1) = nulls1 in
        let must_nulls_set_result =
          MustSet.filter ~min_size:min_size1 (Z.lt min_i) must_nulls_set1
          |> MustSet.add min_i
          |> MustSet.M.filter (Z.gt min_size1) in
        let may_nulls_set_result =
          match max_size1 with
          | Some max_size1 ->
            MaySet.filter ~max_size:max_size1 (Z.lt min_i) may_nulls_set1
            |> MaySet.add min_i
            |> MaySet.M.filter (fun x -> max_size1 >. x)
          | _ -> MaySet.top ()
        in
        ((must_nulls_set_result, may_nulls_set_result), size1)
        (* else only add all may nulls together <= strlen(dest) + strlen(src) *)
      else
        let min_i2 = Nulls.min_elem Definitely nulls2' in
        let (must_nulls_set1, may_nulls_set1) = nulls1 in
        let (must_nulls_set2', may_nulls_set2') = nulls2' in
        let may_nulls_set2'_until_min_i2 =
          match Idx.maximal size2 with
          | Some max_size2 -> MaySet.filter ~max_size:max_size2 (Z.geq min_i2) may_nulls_set2'
          | None -> MaySet.filter ~max_size:(Z.succ min_i2) (Z.geq min_i2) may_nulls_set2' in
        let must_nulls_set_result =
          let pred = match maxlen1, maxlen2 with
            | Some maxlen1, Some maxlen2 -> (fun x -> (maxlen1 +. maxlen2) <. x)
            | _ -> (fun _ -> false)
          in
          MustSet.filter ~min_size:min_size1 pred must_nulls_set1
        in
        let may_nulls_set_result =
          let pred = match maxlen1, maxlen2 with
            | Some maxlen1, Some maxlen2 -> (fun x -> x <=. (maxlen1 +. maxlen2))
            | _ -> (fun _ -> true)
          in
          match max_size1 with
          | Some max_size1 ->
            MaySet.filter ~max_size:max_size1 pred may_nulls_set1
            |> MaySet.elements
            |> BatList.cartesian_product (MaySet.elements may_nulls_set2'_until_min_i2)
            |> List.map (fun (i1, i2) -> i1 +. i2)
            |> MaySet.of_list
            |> MaySet.union (MaySet.filter ~max_size:max_size1 (Z.lt (minlen1 +. minlen2)) may_nulls_set1)
            |> MaySet.M.filter (fun x -> max_size1 >. x)
          | None when not (MaySet.is_top may_nulls_set1) ->
            MaySet.M.filter pred may_nulls_set1
            |> MaySet.elements
            |> BatList.cartesian_product (MaySet.elements may_nulls_set2'_until_min_i2)
            |> List.map (fun (i1, i2) -> i1 +. i2)
            |> MaySet.of_list
            |> MaySet.union (MaySet.M.filter (Z.lt (minlen1 +. minlen2)) may_nulls_set1)
          | _ ->
            MaySet.top () in
        ((must_nulls_set_result, may_nulls_set_result), size1) in

    let compute_concat nulls2' =
      let strlen1 = to_string_length (nulls1, size1) in
      let strlen2 = to_string_length (nulls2', size2) in
      match Idx.minimal size1, Idx.minimal strlen1, Idx.minimal strlen2 with
      | Some min_size1, Some minlen1, Some minlen2 ->
        begin
          let f = update_sets min_size1 (Idx.maximal size1) minlen1 in
          match Idx.maximal strlen1, Idx.maximal strlen2 with
          | (Some _ as maxlen1), (Some _ as maxlen2) -> f maxlen1 minlen2 maxlen2 nulls2'
          | _ -> f None minlen2 None nulls2'
        end
      (* any other case shouldn't happen as minimal index is always >= 0 *)
      | _ -> (Nulls.top (), size1) in

    match n with
    (* strcat *)
    | None ->
      let nulls2', _ = to_string (nulls2, size2) in
      compute_concat nulls2'
    (* strncat *)
    | Some n when n >= 0 ->
      let n = Z.of_int n in
      (* take at most n bytes from src; if no null byte among them, add null byte at index n *)
      let nulls2' =
        let (nulls2, size2) = to_string (nulls2, size2) in
        if not (Nulls.exists Possibly (Z.gt n) nulls2) then
          Nulls.precise_singleton n
        else if not (Nulls.exists Definitely (Z.gt n) nulls2) then
          let max_size = BatOption.default (Z.succ n) (Idx.maximal size2) in
          let nulls2 = Nulls.remove_all Possibly nulls2 in
          let nulls2 = Nulls.filter ~max_size (Z.geq n) nulls2 in
          Nulls.add Possibly n nulls2
        else
          let min_size = BatOption.default Z.zero (Idx.minimal size2) in
          let max_size = BatOption.default n (Idx.maximal size2) in
          Nulls.filter ~max_size ~min_size (Z.gt n) nulls2
      in
      compute_concat nulls2'
    | _ -> (Nulls.top (), size1)

  let substring_extraction haystack ((nulls_needle, size_needle) as needle) =
    (* if needle is empty string, i.e. certain null byte at index 0, return value of strstr is pointer to haystack *)
    if Nulls.mem Definitely Z.zero nulls_needle then
      IsSubstrAtIndex0
    else
      let haystack_len = to_string_length haystack in
      let needle_len = to_string_length needle in
      match Idx.maximal haystack_len, Idx.minimal needle_len with
      | Some haystack_max, Some needle_min when haystack_max <. needle_min ->
        (* if strlen(haystack) < strlen(needle), needle can never be substring of haystack => return None *)
        IsNotSubstr
      | _ -> IsMaybeSubstr

  let string_comparison (nulls1, size1) (nulls2, size2) n =
    let cmp n =
      (* if s1 = s2 = empty string, i.e. certain null byte at index 0, or n = 0, return 0 *)
      if (Nulls.mem Definitely Z.zero nulls1 && Nulls.mem Definitely Z.zero nulls2) || (BatOption.map_default (Z.equal Z.zero) false n) then
        Idx.of_int IInt Z.zero
        (* if only s1 = empty string, return negative integer *)
      else if Nulls.mem Definitely Z.zero nulls1 && not (Nulls.mem Possibly Z.zero nulls2) then
        Idx.ending IInt Z.minus_one
        (* if only s2 = empty string, return positive integer *)
      else if Nulls.mem Definitely Z.zero nulls2 then
        Idx.starting IInt Z.one
      else
        try
          let min_must1 = Nulls.min_elem Definitely nulls1 in
          let min_must2 = Nulls.min_elem Definitely nulls2 in
          if not (min_must1 =. min_must2)
          && min_must1 =.(Nulls.min_elem Possibly nulls1)
          && min_must2 =. (Nulls.min_elem Possibly nulls2)
          && (BatOption.map_default (fun x -> min_must1 <. x || min_must2 <. x) true n)
          then
            (* if first null bytes are certain, have different indexes and are before index n if n present, return integer <> 0 *)
            Idx.of_excl_list IInt [Z.zero]
          else
            Idx.top_of IInt
        with Not_found -> Idx.top_of IInt
    in

    match n with
    (* strcmp *)
    | None ->
      (* track any potential buffer overflow and issue warning if needed *)
      let warn_missing_nulls nulls name =
        if Nulls.is_empty Definitely nulls then
          warn_past_end "Array of string %s doesn't contain a null byte: buffer overflow" name
        else if Nulls.is_empty Possibly nulls then
          warn_past_end "Array of string %s might not contain a null byte: potential buffer overflow" name
        else
          Checks.safe Checks.Category.InvalidMemoryAccess
      in
      warn_missing_nulls nulls1 "1";
      warn_missing_nulls nulls2 "2";
      (* compute abstract value for result of strcmp *)
      cmp None
    (* strncmp *)
    | Some n when n >= 0 ->
      let n = Z.of_int n in
      let warn_size size name =
        let min = min_nat_of_idx size in
        match Idx.maximal size with
        | Some max when n >. max ->
          warn_past_end "The size of the array of string %s is smaller than n bytes" name
        | Some max when n >. min ->
          warn_past_end "The size of the array of string %s might be smaller than n bytes" name
        | None when n >. min ->
          warn_past_end "The size of the array of string %s might be smaller than n bytes" name
        | _ -> Checks.safe Checks.Category.InvalidMemoryAccess
      in
      warn_size size1 "1";
      warn_size size2 "2";
      (* compute abstract value for result of strncmp *)
      cmp (Some n)
    | _ -> Idx.top_of IInt

  let update_length new_size (nulls, size) = (nulls, new_size)

  let project ?(varAttr=[]) ?(typAttr=[]) _ t = t

  let invariant ~value_invariant ~offset ~lval x = Invariant.none
end

module AttributeConfiguredArrayDomain(Val: LatticeWithSmartOps) (Idx:IntDomain.Z):S with type value = Val.t and type idx = Idx.t =
struct
  module P = PartitionedWithLength(Val)(Idx)
  module T = TrivialWithLength(Val)(Idx)
  module U = UnrollWithLength(Val)(Idx)

  type idx = Idx.t
  type value = Val.t

  module K = struct
    let msg = "AttributeConfiguredArrayDomain received a value where not exactly one component is set"
    let name = "AttributeConfiguredArrayDomain"
  end

  let to_t = function
    | (Some p, None, None) -> (Some p, None)
    | (None, Some t, None) -> (None, Some (Some t, None))
    | (None, None, Some u) -> (None, Some (None, Some u))
    | _ -> failwith "AttributeConfiguredArrayDomain received a value where not exactly one component is set"

  module I = struct include LatticeFlagHelper (T) (U) (K) let name () = "" end
  include LatticeFlagHelper (P) (I) (K)

  let domain_of_t = function
    | (Some p, None) -> PartitionedDomain
    | (None, Some (Some t, None)) -> TrivialDomain
    | (None, Some (None, Some u)) -> UnrolledDomain
    | _ -> failwith "Array of invalid domain"

  let binop' opp opt opu = binop opp (I.binop opt opu)
  let unop' opp opt opu = unop opp (I.unop opt opu)
  let binop_to_t' opp opt opu = binop_to_t opp (I.binop_to_t opt opu)
  let unop_to_t' opp opt opu = unop_to_t opp (I.unop_to_t opt opu)

  (* Simply call appropriate function for component that is not None *)
  let get ?(checkBounds=true) a x (e,i) = unop' (fun x ->
      if e = None then
        let e' = BatOption.map (fun x -> Cil.kintegerCilint (Cilfacade.ptrdiff_ikind ()) x) (Idx.to_int i) in
        P.get ~checkBounds a x (e', i)
      else
        P.get ~checkBounds a x (e, i)
    ) (fun x -> T.get ~checkBounds a x (e,i)) (fun x -> U.get ~checkBounds a x (e,i)) x
  let set (ask:VDQ.t) x i a = unop_to_t' (fun x -> P.set ask x i a) (fun x -> T.set ask x i a) (fun x -> U.set ask x i a) x
  let length = unop' P.length T.length U.length
  let map f = unop_to_t' (P.map f) (T.map f) (U.map f)
  let fold_left f s = unop' (P.fold_left f s) (T.fold_left f s) (U.fold_left f s)

  let move_if_affected ?(replace_with_const=false) (ask:VDQ.t) x v f = unop_to_t' (fun x -> P.move_if_affected ~replace_with_const:replace_with_const ask x v f) (fun x -> T.move_if_affected ~replace_with_const:replace_with_const ask x v f) (fun x -> U.move_if_affected ~replace_with_const:replace_with_const ask x v f) x
  let get_vars_in_e = unop' P.get_vars_in_e T.get_vars_in_e U.get_vars_in_e
  let smart_join f g = binop_to_t' (P.smart_join f g) (T.smart_join f g) (U.smart_join f g)
  let smart_widen f g =  binop_to_t' (P.smart_widen f g) (T.smart_widen f g) (U.smart_widen f g)
  let smart_leq f g = binop' (P.smart_leq f g) (T.smart_leq f g) (U.smart_leq f g)
  let update_length newl x = unop_to_t' (P.update_length newl) (T.update_length newl) (U.update_length newl) x
  let name () = "FlagHelperAttributeConfiguredArrayDomain"

  let bot () = to_t @@ match get_domain ~varAttr:[] ~typAttr:[] with
    | PartitionedDomain -> (Some (P.bot ()), None, None)
    | TrivialDomain -> (None, Some (T.bot ()), None)
    | UnrolledDomain ->  (None, None, Some (U.bot ()))

  let top () = to_t @@ match get_domain ~varAttr:[] ~typAttr:[] with
    | PartitionedDomain -> (Some (P.top ()), None, None)
    | TrivialDomain -> (None, Some (T.top ()), None)
    | UnrolledDomain -> (None, None, Some (U.top ()))

  let make ?(varAttr=[]) ?(typAttr=[]) i v = to_t @@  match get_domain ~varAttr ~typAttr with
    | PartitionedDomain -> (Some (P.make i v), None, None)
    | TrivialDomain -> (None, Some (T.make i v), None)
    | UnrolledDomain -> (None, None, Some (U.make i v))

  (* convert to another domain *)
  let index_as_expression i = (Some (Cil.integer i), Idx.of_int IInt (Z.of_int i))

  let partitioned_of_trivial ask t = P.make (Option.value (T.length t) ~default:(Idx.top ())) (T.get ~checkBounds:false ask t (index_as_expression 0))

  let partitioned_of_unroll ask u =
    (* We end with a partition at "ana.base.arrays.unrolling-factor", which keeps the most information. Maybe first element is more commonly useful? *)
    let rest = (U.get ~checkBounds:false ask u (index_as_expression (factor ()))) in
    let p = P.make (Option.value (U.length u) ~default:(Idx.top ())) rest in
    let get_i i = (i, P.get ~checkBounds:false ask p (index_as_expression i)) in
    let set_i p (i,v) =  P.set ask p (index_as_expression i) v in
    List.fold_left set_i p @@ List.init (factor ()) get_i

  let trivial_of_partitioned ask p =
    let element = (P.get ~checkBounds:false ask p (None, Idx.top ()))
    in T.make (Option.value (P.length p) ~default:(Idx.top ())) element

  let trivial_of_unroll ask u =
    let get_i i = U.get ~checkBounds:false ask u (index_as_expression i) in
    let element = List.fold_left Val.join (get_i (factor ())) @@ List.init (factor ()) get_i in (*join all single elements and the element at  *)
    T.make (Option.value (U.length u) ~default:(Idx.top ())) element

  let unroll_of_trivial ask t = U.make (Option.value (T.length t) ~default:(Idx.top ())) (T.get ~checkBounds:false ask t (index_as_expression 0))

  let unroll_of_partitioned ask p =
    let unrolledValues = List.init (factor ()) (fun i ->(i, P.get ~checkBounds:false ask p (index_as_expression i))) in
    (* This could be more precise if we were able to compare this with the partition index, but we can not access it here *)
    let rest = (P.get ~checkBounds:false ask p (None, Idx.top ())) in
    let u = U.make (Option.value (P.length p) ~default:(Idx.top ())) (Val.bot ()) in
    let set_i u (i,v) =  U.set ask u (index_as_expression i) v in
    set_i (List.fold_left set_i u unrolledValues) (factor (), rest)

  let project ?(varAttr=[]) ?(typAttr=[]) ask (t:t) =
    match get_domain ~varAttr ~typAttr, t with
    | PartitionedDomain, (Some x, None) -> to_t @@ (Some x, None, None)
    | PartitionedDomain, (None, Some (Some x, None)) -> to_t @@ (Some (partitioned_of_trivial ask x), None, None)
    | PartitionedDomain, (None, Some (None, Some x)) -> to_t @@ (Some (partitioned_of_unroll ask x), None, None)
    | TrivialDomain, (Some x, None) -> to_t @@ (None, Some (trivial_of_partitioned ask x), None)
    | TrivialDomain, (None, Some (Some x, None)) -> to_t @@ (None, Some x, None)
    | TrivialDomain, (None, Some (None, Some x)) -> to_t @@ (None, Some (trivial_of_unroll ask x), None)
    | UnrolledDomain, (Some x, None) -> to_t @@ (None, None, Some (unroll_of_partitioned ask x) )
    | UnrolledDomain, (None, Some (Some x, None)) -> to_t @@ (None, None, Some (unroll_of_trivial ask x) )
    | UnrolledDomain, (None, Some (None, Some x)) -> to_t @@ (None, None, Some x)
    | _ ->  failwith "AttributeConfiguredArrayDomain received a value where not exactly one component is set"

  let invariant ~value_invariant ~offset ~lval =
    unop'
      (P.invariant ~value_invariant ~offset ~lval)
      (T.invariant ~value_invariant ~offset ~lval)
      (U.invariant ~value_invariant ~offset ~lval)
end

module AttributeConfiguredAndNullByteArrayDomain (Val: LatticeWithNull) (Idx: IntDomain.Z): StrWithDomain with type value = Val.t and type idx = Idx.t =
struct
  module A = AttributeConfiguredArrayDomain (Val) (Idx)
  module N = NullByte (Val) (Idx)

  include Lattice.Prod (A) (N)

  let name () = "AttributeConfiguredAndNullByteArrayDomain"
  type idx = Idx.t
  type value = Val.t

  type ret = Null | NotNull | Maybe
  type substr = N.substr = IsNotSubstr | IsSubstrAtIndex0 | IsMaybeSubstr

  let domain_of_t (t_f, _) = A.domain_of_t t_f

  let get ?(checkBounds=true) (ask: VDQ.t) (t_f, t_n) i =
    let f_get = A.get ~checkBounds ask t_f i in
    if get_bool "ana.base.arrays.nullbytes" then
      let n_get = N.get ask t_n i in
      match Val.get_ikind f_get, n_get with
      | Some ik, Null -> Val.meet f_get (Val.zero_of_ikind ik)
      | Some ik, NotNull -> Val.meet f_get (Val.not_zero_of_ikind ik)
      | _ -> f_get
    else
      f_get

  let delegate_if_no_nullbytes (a, n) ffull fa =
    if get_bool "ana.base.arrays.nullbytes" then
      ffull (a, n)
    else
      fa a

  let show x = delegate_if_no_nullbytes x show A.show
  let printXml f x = delegate_if_no_nullbytes x (printXml f) (A.printXml f)
  let to_yojson x = delegate_if_no_nullbytes x to_yojson A.to_yojson
  let pretty () x = delegate_if_no_nullbytes x (pretty ()) (A.pretty ())

  let construct a n =
    if get_bool "ana.base.arrays.nullbytes" then
      (a, n ())
    else
      (a, N.top ())

  let set (ask:VDQ.t) (t_f, t_n) i v = construct (A.set ask t_f i v) (fun () -> N.set ask t_n i v)
  let make ?(varAttr=[]) ?(typAttr=[]) i v = construct (A.make ~varAttr ~typAttr i v) (fun () -> N.make ~varAttr ~typAttr i v)
  let map f (t_f, t_n) = construct (A.map f t_f) (fun () -> N.map f t_n)
  let update_length newl (t_f, t_n) = construct (A.update_length newl t_f) (fun () -> N.update_length newl t_n)

  let smart_binop op_a op_n x y (t_f1, t_n1) (t_f2, t_n2) = construct (op_a x y t_f1 t_f2) (fun () -> op_n x y t_n1 t_n2)

  let smart_join = smart_binop A.smart_join N.smart_join
  let smart_widen = smart_binop A.smart_widen N.smart_widen

  let string_op op (t_f1, t_n1) (_, t_n2) n = construct (A.map Val.invalidate_abstract_value t_f1) (fun () -> op t_n1 t_n2 n)
  let string_copy = string_op N.string_copy
  let string_concat = string_op N.string_concat

  let extract op default (_, t_n1) (_, t_n2) n =
    if get_bool "ana.base.arrays.nullbytes" then
      op t_n1 t_n2 n
    else
      (* Hidden behind unit, as constructing defaults may happen to early otherwise *)
      (* e.g. for Idx.top_of IInt *)
      default ()

  let substring_extraction x y = extract (fun x y _  -> N.substring_extraction x y) (fun () -> IsMaybeSubstr) x y None
  let string_comparison = extract N.string_comparison (fun () -> Idx.top_of IInt)

  let length (t_f, t_n) =
    if get_bool "ana.base.arrays.nullbytes" then
      N.length t_n
    else
      A.length t_f
  let move_if_affected ?(replace_with_const=false) (ask:VDQ.t) (t_f, t_n) v f = (A.move_if_affected ~replace_with_const ask t_f v f, N.move_if_affected ~replace_with_const ask t_n v f)
  let get_vars_in_e (t_f, _) = A.get_vars_in_e t_f
  let fold_left f acc (t_f, _) = A.fold_left f acc t_f

  let smart_leq x y (t_f1, t_n1) (t_f2, t_n2) =
    if get_bool "ana.base.arrays.nullbytes" then
      A.smart_leq x y t_f1 t_f2 && N.smart_leq x y t_n1 t_n2
    else
      A.smart_leq x y t_f1 t_f2

  let to_null_byte_domain s =
    if get_bool "ana.base.arrays.nullbytes" then
      (A.make (Idx.top_of ILong) (Val.meet (Val.not_zero_of_ikind IChar) (Val.zero_of_ikind IChar)), N.to_null_byte_domain s)
    else
      (A.top (), N.top ())
  let to_string_length (_, t_n) =
    if get_bool "ana.base.arrays.nullbytes" then
      N.to_string_length t_n
    else
      Idx.top_of !Cil.kindOfSizeOf

  let project ?(varAttr=[]) ?(typAttr=[]) ask (t_f, t_n) = (A.project ~varAttr ~typAttr ask t_f, N.project ~varAttr ~typAttr ask t_n)
  let invariant ~value_invariant ~offset ~lval (t_f, _) = A.invariant ~value_invariant ~offset ~lval t_f
end