From 2d83dfdcb0b8698d217dc5db61cb6b8aeb7cb095 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Thu, 1 Apr 2021 10:24:26 -0700
Subject: [PATCH] [pulse] add a term_eqs field to formulas

Summary: Just some scaffolding to save a bit of churn from the next diff.

Reviewed By: skcho

Differential Revision: D27328348

fbshipit-source-id: 4f5bfcc65
---
 infer/src/pulse/PulseFormula.ml          | 64 ++++++++++++++++----
 infer/src/pulse/unit/PulseFormulaTest.ml | 75 +++++++++++++++++-------
 2 files changed, 107 insertions(+), 32 deletions(-)

diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml
index c302237ef..e0dc129f0 100644
--- a/infer/src/pulse/PulseFormula.ml
+++ b/infer/src/pulse/PulseFormula.ml
@@ -267,6 +267,10 @@ type subst_target = LinArith.subst_target =
   | VarSubst of Var.t
   | LinSubst of LinArith.t
 
+let subst_f subst x = match Var.Map.find_opt x subst with Some y -> y | None -> x
+
+let targetted_subst_var subst_var x = VarSubst (subst_f subst_var x)
+
 (** Expressive term structure to be able to express all of SIL, but the main smarts of the formulas
     are for the equality between variables and linear arithmetic subsets. Terms (and atoms, below)
     are kept as a last-resort for when outside that fragment. *)
@@ -798,6 +802,35 @@ module Term = struct
       match LinArith.get_as_const l with Some c -> Const c | None -> Linear l )
     | t ->
         t
+
+
+  module VarMap = struct
+    include Caml.Map.Make (struct
+      type nonrec t = t [@@deriving compare]
+    end)
+
+    type t_ = Var.t t [@@deriving compare, equal]
+
+    let pp_with_pp_var pp_var fmt m =
+      if is_empty m then F.pp_print_string fmt "true (no term_eqs)"
+      else
+        Pp.collection ~sep:"∧"
+          ~fold:(IContainer.fold_of_pervasives_map_fold fold)
+          ~pp_item:(fun fmt (term, var) ->
+            F.fprintf fmt "%a=%a" (pp_no_paren pp_var) term pp_var var )
+          fmt m
+
+
+    let yojson_of_t_ m = `List (List.map (bindings m) ~f:[%yojson_of: t * Var.t])
+
+    let apply_var_subst subst m =
+      fold
+        (fun t v acc ->
+          let t' = subst_variables t ~f:(targetted_subst_var subst) in
+          let v' = subst_f subst v in
+          add t' v' acc )
+        m empty
+  end
 end
 
 (** Basically boolean terms, used to build the part of a formula that is not equalities between
@@ -1108,10 +1141,17 @@ module Formula = struct
     { var_eqs: var_eqs  (** equality relation between variables *)
     ; linear_eqs: linear_eqs
           (** equalities of the form [x = l] where [l] is from linear arithmetic *)
-    ; atoms: Atom.Set.t  (** not always normalized w.r.t. [var_eqs] and [linear_eqs] *) }
+    ; term_eqs: Term.VarMap.t_  (** equalities of the form [t = x] *)
+    ; atoms: Atom.Set.t  (** "everything else"; not always normalized w.r.t. the components above *)
+    }
   [@@deriving compare, equal, yojson_of]
 
-  let ttrue = {var_eqs= VarUF.empty; linear_eqs= Var.Map.empty; atoms= Atom.Set.empty}
+  let ttrue =
+    { var_eqs= VarUF.empty
+    ; linear_eqs= Var.Map.empty
+    ; term_eqs= Term.VarMap.empty
+    ; atoms= Atom.Set.empty }
+
 
   let pp_with_pp_var pp_var fmt phi =
     let pp_linear_eqs fmt m =
@@ -1122,9 +1162,11 @@ module Formula = struct
           ~pp_item:(fun fmt (v, l) -> F.fprintf fmt "%a = %a" pp_var v (LinArith.pp pp_var) l)
           fmt m
     in
-    F.fprintf fmt "@[<hv>%a@ &&@ %a@ &&@ %a@]"
+    F.fprintf fmt "@[<hv>%a@ &&@ %a@ &&@ %a@ &&@ %a@]"
       (VarUF.pp ~pp_empty:(fun fmt -> F.pp_print_string fmt "true (no var=var)") pp_var)
-      phi.var_eqs pp_linear_eqs phi.linear_eqs (Atom.Set.pp_with_pp_var pp_var) phi.atoms
+      phi.var_eqs pp_linear_eqs phi.linear_eqs
+      (Term.VarMap.pp_with_pp_var pp_var)
+      phi.term_eqs (Atom.Set.pp_with_pp_var pp_var) phi.atoms
 
 
   (** module that breaks invariants more often that the rest, with an interface that is safer to use *)
@@ -1577,10 +1619,6 @@ module QuantifierElimination : sig
 end = struct
   exception Contradiction
 
-  let subst_f subst x = match Var.Map.find_opt x subst with Some y -> y | None -> x
-
-  let targetted_subst_var subst_var x = VarSubst (subst_f subst_var x)
-
   let subst_var_linear_eqs subst linear_eqs =
     Var.Map.fold
       (fun x l new_map ->
@@ -1606,9 +1644,10 @@ end = struct
       atoms Atom.Set.empty
 
 
-  let subst_var_formula subst {Formula.var_eqs; linear_eqs; atoms} =
+  let subst_var_formula subst {Formula.var_eqs; linear_eqs; term_eqs; atoms} =
     { Formula.var_eqs= VarUF.apply_subst subst var_eqs
     ; linear_eqs= subst_var_linear_eqs subst linear_eqs
+    ; term_eqs= Term.VarMap.apply_var_subst subst term_eqs
     ; atoms= subst_var_atoms subst atoms }
 
 
@@ -1725,8 +1764,13 @@ module DeadVariables = struct
       let linear_eqs =
         Var.Map.filter (fun v _ -> Var.Set.mem v vars_to_keep) phi.Formula.linear_eqs
       in
+      let term_eqs =
+        Term.VarMap.filter
+          (fun t v -> Var.Set.mem v vars_to_keep && not (Term.has_var_notin vars_to_keep t))
+          phi.Formula.term_eqs
+      in
       let atoms = Atom.Set.filter filter_atom phi.Formula.atoms in
-      {Formula.var_eqs; linear_eqs; atoms}
+      {Formula.var_eqs; linear_eqs; term_eqs; atoms}
     in
     let known = simplify_phi phi.known in
     let both = simplify_phi phi.both in
diff --git a/infer/src/pulse/unit/PulseFormulaTest.ml b/infer/src/pulse/unit/PulseFormulaTest.ml
index 5e58f4303..b4bd92247 100644
--- a/infer/src/pulse/unit/PulseFormulaTest.ml
+++ b/infer/src/pulse/unit/PulseFormulaTest.ml
@@ -142,8 +142,9 @@ let%test_module "normalization" =
       normalize (x < y) ;
       [%expect
         {|
-        known=true (no var=var) && true (no linear) && {[x + -y] < 0}, pruned=true (no atoms),
-        both=true (no var=var) && true (no linear) && {[x + -y] < 0}|}]
+        known=true (no var=var) && true (no linear) && true (no term_eqs) && {[x + -y] < 0},
+        pruned=true (no atoms),
+        both=true (no var=var) && true (no linear) && true (no term_eqs) && {[x + -y] < 0}|}]
 
     let%expect_test _ =
       normalize (x + i 1 - i 1 < x) ;
@@ -175,8 +176,9 @@ let%test_module "normalization" =
       normalize (of_binop Eq x y = i 0 && x = i 0 && y = i 1) ;
       [%expect
         {|
-        known=true (no var=var) && x = 0 ∧ y = 1 ∧ v6 = 0 && true (no atoms), pruned=true (no atoms),
-        both=true (no var=var) && x = 0 ∧ y = 1 ∧ v6 = 0 && true (no atoms)|}]
+        known=true (no var=var) && x = 0 ∧ y = 1 ∧ v6 = 0 && true (no term_eqs) && true (no atoms),
+        pruned=true (no atoms),
+        both=true (no var=var) && x = 0 ∧ y = 1 ∧ v6 = 0 && true (no term_eqs) && true (no atoms)|}]
 
     let%expect_test _ =
       normalize (x = i 0 && x < i 0) ;
@@ -194,12 +196,16 @@ let%test_module "normalization" =
               &&
               x = -v6 + v8 -1 ∧ v7 = v8 -1 ∧ v10 = 0
               &&
+              true (no term_eqs)
+              &&
               {0 = [v9]÷[w]}∧{[v6] = [v]×[y]}∧{[v9] = [z]×[v8]},
         pruned=true (no atoms),
         both=true (no var=var)
              &&
              x = -v6 + v8 -1 ∧ v7 = v8 -1 ∧ v10 = 0
              &&
+             true (no term_eqs)
+             &&
              {0 = [v9]÷[w]}∧{[v6] = [v]×[y]}∧{[v9] = [z]×[v8]} |}]
 
     (* check that this becomes all linear equalities *)
@@ -211,12 +217,16 @@ let%test_module "normalization" =
               &&
               x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0
               &&
+              true (no term_eqs)
+              &&
               true (no atoms),
         pruned=true (no atoms),
         both=true (no var=var)
              &&
              x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0
              &&
+             true (no term_eqs)
+             &&
              true (no atoms)|}]
 
     (* check that this becomes all linear equalities thanks to constant propagation *)
@@ -229,6 +239,8 @@ let%test_module "normalization" =
               x = -v6 -1 ∧ y = 1/3·v6 ∧ z = 12 ∧ w = 7 ∧ v = 3 ∧ v7 = -1
                ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0
               &&
+              true (no term_eqs)
+              &&
               true (no atoms),
         pruned=true (no atoms),
         both=true (no var=var)
@@ -236,6 +248,8 @@ let%test_module "normalization" =
              x = -v6 -1 ∧ y = 1/3·v6 ∧ z = 12 ∧ w = 7 ∧ v = 3 ∧ v7 = -1
               ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0
              &&
+             true (no term_eqs)
+             &&
              true (no atoms)|}]
   end )
 
@@ -245,37 +259,38 @@ let%test_module "variable elimination" =
       simplify ~keep:[x_var; y_var] (x = y) ;
       [%expect
         {|
-        known=x=y && true (no linear) && true (no atoms), pruned=true (no atoms),
-        both=x=y && true (no linear) && true (no atoms)|}]
+        known=x=y && true (no linear) && true (no term_eqs) && true (no atoms), pruned=true (no atoms),
+        both=x=y && true (no linear) && true (no term_eqs) && true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var] (x = i 0 && y = i 1 && z = i 2 && w = i 3) ;
       [%expect
         {|
-        known=true (no var=var) && x = 0 && true (no atoms), pruned=true (no atoms),
-        both=true (no var=var) && x = 0 && true (no atoms)|}]
+        known=true (no var=var) && x = 0 && true (no term_eqs) && true (no atoms), pruned=true (no atoms),
+        both=true (no var=var) && x = 0 && true (no term_eqs) && true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var] (x = y + i 1 && x = i 0) ;
       [%expect
         {|
-          known=true (no var=var) && x = 0 && true (no atoms), pruned=true (no atoms),
-          both=true (no var=var) && x = 0 && true (no atoms)|}]
+          known=true (no var=var) && x = 0 && true (no term_eqs) && true (no atoms), pruned=true (no atoms),
+          both=true (no var=var) && x = 0 && true (no term_eqs) && true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[y_var] (x = y + i 1 && x = i 0) ;
       [%expect
         {|
-        known=true (no var=var) && y = -1 && true (no atoms), pruned=true (no atoms),
-        both=true (no var=var) && y = -1 && true (no atoms)|}]
+        known=true (no var=var) && y = -1 && true (no term_eqs) && true (no atoms), pruned=true (no atoms),
+        both=true (no var=var) && y = -1 && true (no term_eqs) && true (no atoms)|}]
 
     (* should keep most of this or realize that [w = z] hence this boils down to [z+1 = 0] *)
     let%expect_test _ =
       simplify ~keep:[y_var; z_var] (x = y + z && w = x - y && v = w + i 1 && v = i 0) ;
       [%expect
         {|
-        known=true (no var=var) && x = y -1 ∧ z = -1 && true (no atoms), pruned=true (no atoms),
-        both=true (no var=var) && x = y -1 ∧ z = -1 && true (no atoms)|}]
+        known=true (no var=var) && x = y -1 ∧ z = -1 && true (no term_eqs) && true (no atoms),
+        pruned=true (no atoms),
+        both=true (no var=var) && x = y -1 ∧ z = -1 && true (no term_eqs) && true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var; y_var] (x = y + z && w + x + y = i 0 && v = w + i 1) ;
@@ -285,20 +300,24 @@ let%test_module "variable elimination" =
                 &&
                 x = -v + v7 +1 ∧ y = -v7 ∧ z = -v + 2·v7 +1 ∧ w = v -1
                 &&
+                true (no term_eqs)
+                &&
                 true (no atoms),
           pruned=true (no atoms),
           both=true (no var=var)
                &&
                x = -v + v7 +1 ∧ y = -v7 ∧ z = -v + 2·v7 +1 ∧ w = v -1
                &&
+               true (no term_eqs)
+               &&
                true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var; y_var] (x = y + i 4 && x = w && y = z) ;
       [%expect
         {|
-        known=true (no var=var) && x = y +4 && true (no atoms), pruned=true (no atoms),
-        both=true (no var=var) && x = y +4 && true (no atoms)|}]
+        known=true (no var=var) && x = y +4 && true (no term_eqs) && true (no atoms),
+        pruned=true (no atoms), both=true (no var=var) && x = y +4 && true (no term_eqs) && true (no atoms)|}]
   end )
 
 let%test_module "non-linear simplifications" =
@@ -307,21 +326,33 @@ let%test_module "non-linear simplifications" =
       simplify ~keep:[w_var] (((i 0 / (x * z)) & v) * v mod y = w) ;
       [%expect
         {|
-        known=true (no var=var) && w = 0 && true (no atoms), pruned=true (no atoms),
-        both=true (no var=var) && w = 0 && true (no atoms)|}]
+        known=true (no var=var) && w = 0 && true (no term_eqs) && true (no atoms), pruned=true (no atoms),
+        both=true (no var=var) && w = 0 && true (no term_eqs) && true (no atoms)|}]
 
     let%expect_test "constant propagation: bitshift" =
       simplify ~keep:[x_var] (of_binop Shiftlt (of_binop Shiftrt (i 0b111) (i 2)) (i 2) = x) ;
       [%expect
         {|
-        known=true (no var=var) && x = 4 && true (no atoms), pruned=true (no atoms),
-        both=true (no var=var) && x = 4 && true (no atoms)|}]
+        known=true (no var=var) && x = 4 && true (no term_eqs) && true (no atoms), pruned=true (no atoms),
+        both=true (no var=var) && x = 4 && true (no term_eqs) && true (no atoms)|}]
 
     let%expect_test "non-linear becomes linear" =
       normalize (w = (i 2 * z) - i 3 && z = x * y && y = i 2) ;
       [%expect
         {|
-          known=z=v8 ∧ w=v7 && x = 1/4·v6 ∧ y = 2 ∧ z = 1/2·v6 ∧ w = v6 -3 && true (no atoms),
+          known=z=v8 ∧ w=v7
+                &&
+                x = 1/4·v6 ∧ y = 2 ∧ z = 1/2·v6 ∧ w = v6 -3
+                &&
+                true (no term_eqs)
+                &&
+                true (no atoms),
           pruned=true (no atoms),
-          both=z=v8 ∧ w=v7 && x = 1/4·v6 ∧ y = 2 ∧ z = 1/2·v6 ∧ w = v6 -3 && true (no atoms)|}]
+          both=z=v8 ∧ w=v7
+               &&
+               x = 1/4·v6 ∧ y = 2 ∧ z = 1/2·v6 ∧ w = v6 -3
+               &&
+               true (no term_eqs)
+               &&
+               true (no atoms)|}]
   end )