[itv] Prettier print

Summary:
- Moving/factorizing/simplifying things
- Prettier output for negative coefficients

Reviewed By: jvillard

Differential Revision: D7925348

fbshipit-source-id: 1e4d046

infer/src/bufferoverrun/itv.ml

@@ -65,7 +65,26 @@ module Symbol = struct
   let is_unsigned : t -> bool = fun x -> x.unsigned
 end
 
-module SymbolMap = PrettyPrintable.MakePPMap (Symbol)
+module SymbolMap = struct
+  include PrettyPrintable.MakePPMap (Symbol)
+
+  let for_all2 : f:(key -> 'a option -> 'b option -> bool) -> 'a t -> 'b t -> bool =
+   fun ~f x y ->
+    match merge (fun k x y -> if f k x y then None else raise Exit) x y with
+    | _ ->
+        true
+    | exception Exit ->
+        false
+
+
+  let is_singleton : 'a t -> (key * 'a) option =
+   fun m ->
+    if is_empty m then None
+    else
+      let (kmin, _) as binding = min_binding m in
+      let kmax, _ = max_binding m in
+      if Symbol.equal kmin kmax then Some binding else None
+end
 
 module NonZeroInt : sig
   type t = private int [@@deriving compare]
@@ -78,6 +97,8 @@ module NonZeroInt : sig
 
   val of_int : int -> t option
 
+  val opt_to_int : t option -> int
+
   val is_one : t -> bool
 
   val is_minus_one : t -> bool
@@ -92,6 +113,8 @@ module NonZeroInt : sig
 
   val ( * ) : t -> t -> t
 
+  val plus : t -> t -> t option
+
   val exact_div_exn : t -> t -> t
 end = struct
   type t = int [@@deriving compare]
@@ -104,6 +127,8 @@ end = struct
 
   let of_int = function 0 -> None | i -> Some i
 
+  let opt_to_int = function None -> 0 | Some i -> i
+
   let is_one = Int.equal 1
 
   let is_minus_one = Int.equal (-1)
@@ -118,29 +143,15 @@ end = struct
 
   let ( * ) = Int.( * )
 
+  let plus x y = of_int (x + y)
+
   let exact_div_exn num den =
     if not (is_multiple num den) then raise DivisionNotExact ;
     num / den
 end
 
 module SymLinear = struct
-  module M = struct
+  module M = SymbolMap
-    include Caml.Map.Make (Symbol)
-
-    let for_all2 : (key -> 'a option -> 'b option -> bool) -> 'a t -> 'b t -> bool =
-     fun cond x y ->
-      let merge_function k x y = if cond k x y then None else raise Exit in
-      match merge merge_function x y with _ -> true | exception Exit -> false
-
-
-    let is_singleton : 'a t -> (key * 'a) option =
-     fun m ->
-      if is_empty m then None
-      else
-        let (kmin, _) as binding = min_binding m in
-        let kmax, _ = max_binding m in
-        if Symbol.equal kmin kmax then Some binding else None
-  end
 
   (**
      Map from symbols to integer coefficients.
@@ -172,12 +183,12 @@ module SymLinear = struct
 
   let le : t -> t -> bool =
    fun x y ->
-    let le_one_pair s (v1_opt: NonZeroInt.t option) (v2_opt: NonZeroInt.t option) =
+    let le_one_pair s v1_opt v2_opt =
-      let v1 = Option.value (v1_opt :> int option) ~default:0 in
+      let v1 = NonZeroInt.opt_to_int v1_opt in
-      let v2 = Option.value (v2_opt :> int option) ~default:0 in
+      let v2 = NonZeroInt.opt_to_int v2_opt in
       Int.equal v1 v2 || (Symbol.is_unsigned s && v1 <= v2)
     in
-    M.for_all2 le_one_pair x y
+    M.for_all2 ~f:le_one_pair x y
 
 
   let make : unsigned:bool -> Typ.Procname.t -> int -> t =
@@ -189,14 +200,14 @@ module SymLinear = struct
     let eq_pair _ (coeff1: NonZeroInt.t option) (coeff2: NonZeroInt.t option) =
       [%compare.equal : int option] (coeff1 :> int option) (coeff2 :> int option)
     in
-    M.for_all2 eq_pair x y
+    M.for_all2 ~f:eq_pair x y
 
 
   let pp1 : F.formatter -> Symbol.t * NonZeroInt.t -> unit =
    fun fmt (s, c) ->
     let c = (c :> int) in
-    if Int.equal c 1 then F.fprintf fmt "%a" Symbol.pp s
+    if Int.equal c 1 then Symbol.pp fmt s
-    else if c < 0 then F.fprintf fmt "(%d)x%a" c Symbol.pp s
+    else if Int.equal c (-1) then F.fprintf fmt "-%a" Symbol.pp s
     else F.fprintf fmt "%dx%a" c Symbol.pp s
 
 
@@ -213,16 +224,8 @@ module SymLinear = struct
 
   let plus : t -> t -> t =
    fun x y ->
-    let plus' _ (n_opt: NonZeroInt.t option) (m_opt: NonZeroInt.t option) =
+    let plus_coeff _ c1 c2 = NonZeroInt.plus c1 c2 in
-      match (n_opt, m_opt) with
+    M.union plus_coeff x y
-      | None, None ->
-          None
-      | (Some _ as some_v), None | None, (Some _ as some_v) ->
-          some_v
-      | Some n, Some m ->
-          NonZeroInt.of_int ((n :> int) + (m :> int))
-    in
-    M.merge plus' x y
 
 
   (** [se1] * [c] + [se2] *)
@@ -235,9 +238,9 @@ module SymLinear = struct
       | None, (Some _ as some_v) ->
           some_v
       | Some v, None ->
-          Some (NonZeroInt.( * ) v c)
+          Some NonZeroInt.(v * c)
       | Some v1, Some v2 ->
-          NonZeroInt.of_int (((v1 :> int) * (c :> int)) + (v2 :> int))
+          NonZeroInt.(v1 * c |> plus v2)
     in
     M.merge f se1 se2
 

infer/tests/codetoanalyze/c/performance/issues.exp

@@ -7,10 +7,10 @@ codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_
 codetoanalyze/c/performance/cost_test.c, loop2_bad, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []
 codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 11xs$1 + 3]
 codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 11xs$1 + 3]
-codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost (-1)xs$0 + s$1 + 16]
+codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost -s$0 + s$1 + 16]
-codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost (-13)xs$0 + 13xs$1 + 199]
+codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost -13xs$0 + 13xs$1 + 199]
-codetoanalyze/c/performance/cost_test.c, loop3_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost (-13)xs$0 + 13xs$1 + 199]
+codetoanalyze/c/performance/cost_test.c, loop3_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost -13xs$0 + 13xs$1 + 199]
-codetoanalyze/c/performance/cost_test.c, loop3_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost (-15)xs$0 + 15xs$1 + 231]
+codetoanalyze/c/performance/cost_test.c, loop3_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost -15xs$0 + 15xs$1 + 231]
 codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 211]
 codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 12, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 201]
 codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1204]