[pulse] detect when atoms become linear arithmetic

Summary:
Since this is where almost all of the reasoning is concentrated, let's
make sure we use it at every opportunity!

Reviewed By: skcho

Differential Revision: D23194224

fbshipit-source-id: fedb2811e

infer/src/pulse/PulseFormula.ml

@@ -396,12 +396,10 @@ module Atom = struct
     | BitNot (BitNot t) ->
         (* [~~t = t] *)
         t
-    | Not (Const c) when Q.equal c Q.zero ->
-        (* [!0 = 1]  *)
-        one
-    | Not (Const c) when Q.equal c Q.one ->
-        (* [!1 = 0]  *)
-        zero
+    | Not (Const c) ->
+        if Q.equal c Q.zero then (* [!0 = 1]  *)
+          one else (* [!<non-zero> = 0]  *)
+                zero
     | Add (Const c1, Const c2) ->
         (* constants *)
         Const (Q.add c1 c2)
@@ -560,6 +558,10 @@ module LinArith : sig
 
   val of_operand : operand -> t
 
+  val of_term : Term.t -> t option
+  (** more or less syntactic attempt at detecting when an arbitrary term is a linear formula; call
+      {!Atom.eval_term} first for best results *)
+
   val get_as_const : t -> Q.t option
   (** [get_as_const l] is [Some c] if [l=c], else [None] *)
 
@@ -645,10 +647,52 @@ end = struct
 
   let of_var v = (Var.Map.singleton v Q.one, Q.zero)
 
-  let of_intlit i = (Var.Map.empty, IntLit.to_big_int i |> Q.of_bigint)
+  let of_q q = (Var.Map.empty, q)
+
+  let of_intlit i = IntLit.to_big_int i |> Q.of_bigint |> of_q
 
   let of_operand = function AbstractValueOperand v -> of_var v | LiteralOperand i -> of_intlit i
 
+  (* don't duplicate simplifications between here and {!Atom.eval_term} *)
+  let rec of_term (t : Term.t) =
+    let open IOption.Let_syntax in
+    match t with
+    | Var v ->
+        Some (of_var v)
+    | Const c ->
+        Some (of_q c)
+    | Minus t ->
+        let+ l = of_term t in
+        minus l
+    | Add (t1, t2) ->
+        let* l1 = of_term t1 in
+        let+ l2 = of_term t2 in
+        add l1 l2
+    | Mult (Const c, t) | Mult (t, Const c) ->
+        let+ l = of_term t in
+        mult c l
+    | Div (t, Const c) when not (Q.equal c Q.zero) ->
+        let+ l = of_term t in
+        mult (Q.inv c) l
+    | Mult _
+    | Div _
+    | Mod _
+    | BitNot _
+    | BitAnd _
+    | BitOr _
+    | BitShiftLeft _
+    | BitShiftRight _
+    | BitXor _
+    | Not _
+    | And _
+    | Or _
+    | LessThan _
+    | LessEqual _
+    | Equal _
+    | NotEqual _ ->
+        None
+
+
   let get_as_const (vs, c) = if Var.Map.is_empty vs then Some c else None
 
   let get_as_var (vs, c) =
@@ -897,14 +941,26 @@ end = struct
 
 
   let normalize_atoms phi =
-    (* TODO: normalizing an atom may produce a new linear arithmetic or variable equality fact, we
-       should detect that and feed it back to the rest of the formula *)
-    let+ atoms =
-      IContainer.fold_of_pervasives_set_fold Atom.Set.fold phi.atoms ~init:(Sat Atom.Set.empty)
-        ~f:(fun facts atom ->
-          let* facts = facts in
+    let+ phi, atoms =
+      IContainer.fold_of_pervasives_set_fold Atom.Set.fold phi.atoms
+        ~init:(Sat (phi, Atom.Set.empty))
+        ~f:(fun acc atom ->
+          let* phi, facts = acc in
           normalize_atom phi atom
-          >>| function None -> facts | Some atom' -> Atom.Set.add atom' facts )
+          >>= function
+          | None ->
+              acc
+          | Some (Atom.Equal (t1, t2) as atom') -> (
+            match Option.both (LinArith.of_term t1) (LinArith.of_term t2) with
+            | None ->
+                Sat (phi, Atom.Set.add atom' facts)
+            | Some (l1, l2) ->
+                (* an atom has been found to have become a linear equality, move it to the linear
+                   equalities *)
+                let+ phi = solve_eq ~fuel:5 l1 l2 phi in
+                (phi, facts) )
+          | Some atom' ->
+              Sat (phi, Atom.Set.add atom' facts) )
     in
     {phi with atoms}
 

infer/src/pulse/unit/PulseFormulaTest.ml

@@ -50,6 +50,10 @@ let%test_module _ =
 
     let ( - ) f1 f2 phi = of_binop (MinusA None) f1 f2 phi
 
+    let ( * ) f1 f2 phi = of_binop (Mult None) f1 f2 phi
+
+    let ( / ) f1 f2 phi = of_binop Div f1 f2 phi
+
     let ( = ) f1 f2 phi =
       let* phi, op1 = f1 phi in
       let* phi, op2 = f2 phi in
@@ -158,6 +162,39 @@ let%test_module _ =
       normalize (x = i 0 && x < i 0) ;
       [%expect {|unsat|}]
 
+    let%expect_test "nonlinear arithmetic" =
+      normalize (z * (x + (v * y) + i 1) / w = i 0) ;
+      [%expect
+        {|
+        true (no var=var)
+        &&
+        v7 = x + v6 ∧ v8 = x + v6 +1 ∧ v10 = 0
+        &&
+        {0 = v9÷w}∧{v6 = v×y}∧{v9 = z×v8} |}]
+
+    (* check that this becomes all linear equalities *)
+    let%expect_test _ =
+      normalize (i 12 * (x + (i 3 * y) + i 1) / i 7 = i 0) ;
+      [%expect
+        {|
+        true (no var=var)
+        &&
+        x = -v6 + 1/12·v9 -1 ∧ y = 1/3·v6 ∧ v7 = x + v6 ∧ v8 = x + v6 +1 ∧ v9 = 0 ∧ v10 = 0
+        &&
+        true (no atoms)|}]
+
+    (* check that this becomes all linear equalities thanks to constant propagation *)
+    let%expect_test _ =
+      normalize (z * (x + (v * y) + i 1) / w = i 0 && z = i 12 && v = i 3 && w = i 7) ;
+      [%expect
+        {|
+        true (no var=var)
+        &&
+        x = -v6 + 1/12·v9 -1 ∧ y = 1/3·v6 ∧ z = 12 ∧ w = 7 ∧ v = 3 ∧ v7 = x + v6
+         ∧ v8 = x + v6 +1 ∧ v9 = 0 ∧ v10 = 0
+        &&
+        true (no atoms)|}]
+
     let%expect_test _ =
       simplify ~keep:[x_var] (x = i 0 && y = i 1 && z = i 2 && w = i 3) ;
       [%expect {|true (no var=var) && x = 0 && true (no atoms)|}]