AStat/domains/interval.ml

open Naked
open Abstract_syntax_tree

module Interval : NAKED_VALUE_DOMAIN = struct
  type t = { lower : Z.t; upper : Z.t }

  let const a = { lower = a; upper = a }
  let rand a b = { lower = Z.min a b; upper = Z.max a b }
  let infty = Z.of_int64_unsigned Int64.max_int
  let min_infty = Z.neg infty
  let pos = rand Z.one infty
  let neg = rand min_infty Z.minus_one

  let rand3 a b c =
    let mi = List.fold_left Z.min a [ a; b; c ] in
    let ma = List.fold_left Z.max a [ a; b; c ] in
    rand mi ma

  let rand4 a b c d =
    let mi = List.fold_left Z.min a [ a; b; c; d ] in
    let ma = List.fold_left Z.max a [ a; b; c; d ] in
    rand mi ma

  let minus z = rand (Z.neg z.upper) (Z.neg z.lower)
  let join z1 z2 = rand4 z1.lower z2.lower z1.upper z2.upper

  let meet z1 z2 =
    if Z.lt z1.upper z2.lower || Z.lt z2.upper z1.lower then raise Absurd
    else rand (Z.max z1.lower z2.lower) (Z.min z1.upper z2.upper)

  let widen z1 z2 =
    rand
      (if Z.lt z1.lower z2.lower then z1.lower else min_infty)
      (if Z.gt z1.upper z2.upper then z1.upper else infty)

  let narrow = meet
  let subset z1 z2 = Z.geq z1.lower z2.lower && Z.leq z1.upper z2.upper

  let binary z1 z2 = function
    | AST_PLUS -> rand (Z.add z1.lower z2.lower) (Z.add z1.upper z2.upper)
    | AST_MINUS -> rand (Z.sub z1.lower z2.upper) (Z.sub z1.upper z2.lower)
    | AST_MULTIPLY ->
        rand4 (Z.mul z1.lower z2.lower) (Z.mul z1.upper z2.lower)
          (Z.mul z1.lower z2.upper) (Z.mul z1.upper z2.upper)
    | AST_DIVIDE ->
        if Z.sign z2.lower <> Z.sign z2.upper || Z.sign z2.lower = 0 then
          raise Absurd
        else
          rand4 (Z.div z1.lower z2.lower) (Z.div z1.upper z2.lower)
            (Z.div z1.lower z2.upper) (Z.div z1.upper z2.upper)
    | AST_MODULO ->
        if Z.sign z2.lower <> Z.sign z2.upper || Z.sign z2.lower = 0 then
          raise Absurd
        else
          rand4 (Z.rem z1.lower z2.lower) (Z.rem z1.upper z2.lower)
            (Z.rem z1.lower z2.upper) (Z.rem z1.upper z2.upper)

  let is_only_zero z = Z.equal z.lower Z.zero && Z.equal z.upper Z.zero
  let multiples_of z = if is_only_zero z then const Z.zero else raise NeedTop
  let divisors_of z = if is_only_zero z then const Z.zero else raise NeedTop
  let remainders z = if is_only_zero z then const Z.zero else raise NeedTop
  let convex_sym z = if is_only_zero z then const Z.zero else raise NeedTop

  let compatible z = function
    | AST_EQUAL -> z
    | AST_NOT_EQUAL -> raise NeedTop
    | AST_LESS ->
        if Z.equal z.lower min_infty then raise Absurd
        else rand min_infty z.lower
    | AST_LESS_EQUAL -> rand min_infty z.lower
    | AST_GREATER ->
        if Z.equal z.upper infty then raise Absurd else rand z.upper infty
    | AST_GREATER_EQUAL -> rand z.upper infty

  let rec compare z1 z2 = function
    | AST_EQUAL ->
        let z = meet z1 z2 in
        (z, z)
    | AST_NOT_EQUAL ->
        if
          Z.equal z1.lower z1.upper && Z.equal z1.upper z2.lower
          && Z.equal z2.lower z2.upper
        then raise Absurd
        else (z1, z2)
    | AST_LESS ->
        if Z.leq z2.upper z1.lower then raise Absurd
        else
          let r1 =
            rand z1.lower
              (if Z.geq z1.upper z2.upper then Z.pred z2.upper else z1.upper)
          in
          let r2 =
            rand
              (if Z.geq z1.lower z2.lower then Z.succ z1.lower else z2.lower)
              z2.upper
          in
          (r1, r2)
    | AST_LESS_EQUAL ->
        if Z.lt z2.upper z1.lower then raise Absurd
        else
          let r1 = rand z1.lower (Z.min z1.upper z2.upper) in
          let r2 = rand (Z.max z1.lower z2.lower) z2.upper in
          (r1, r2)
    | AST_GREATER ->
        let r1, r2 = compare z2 z1 AST_LESS in
        (r2, r1)
    | AST_GREATER_EQUAL ->
        let r1, r2 = compare z2 z1 AST_LESS_EQUAL in
        (r2, r1)

  let has_zero z = Z.leq z.lower Z.zero && Z.geq z.upper Z.zero
  let has_one z = Z.leq z.lower Z.one && Z.geq z.upper Z.one
  let has_minus_one z = Z.leq z.lower Z.minus_one && Z.geq z.upper Z.minus_one

  let three_part z1 z2 op =
    if has_one z2 then
      if has_minus_one z2 then
        let a = meet pos z2 in
        let b = meet neg z2 in
        join (binary z1 a op) (binary z1 b op)
      else
        let a = meet pos z2 in
        binary z1 a op
    else
      let a = meet neg z2 in
      binary z1 a op

  let bwd_binary z1 z2 op r =
    match op with
    | AST_PLUS ->
        (meet z1 (binary r z2 AST_MINUS), meet z2 (binary r z1 AST_MINUS))
    | AST_MINUS ->
        (meet z1 (binary r z2 AST_PLUS), meet z2 (binary z1 r AST_MINUS))
    | AST_MULTIPLY ->
        if is_only_zero z1 || is_only_zero z2 then
                if has_zero r then
                        z1, z2
                else raise Absurd
        else
          let z2' = meet z2 (three_part r z1 AST_DIVIDE) in
          let z1' = meet z1 (three_part r z2 AST_DIVIDE) in
          if has_zero r then
            ( (if has_zero z1' then join z1' (const Z.zero) else z1'),
              if has_zero z2' then join z2' (const Z.zero) else z2' )
          else (z1', z2')
    | AST_DIVIDE ->
        (meet z1 (binary r z2 AST_MULTIPLY), meet z2 (binary z1 r AST_DIVIDE))
    | AST_MODULO -> (z1, z2)

  let print fmt z =
    Format.pp_print_string fmt "[";
    Z.pp_print fmt z.lower;
    Format.pp_print_string fmt "; ";
    Z.pp_print fmt z.upper;
    Format.pp_print_string fmt "]"
end