diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 8c0a29c73..2e14051c0 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -12,6 +12,20 @@ module Var = PulseAbstractValue type operand = LiteralOperand of IntLit.t | AbstractValueOperand of Var.t +module Q = struct + include Q + + let not_equal q1 q2 = not (Q.equal q1 q2) + + let is_one q = Q.equal q Q.one + + let is_minus_one q = Q.equal q Q.minus_one + + let is_zero q = Q.equal q Q.zero + + let is_not_zero q = not (is_zero q) +end + (** 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. *) @@ -173,9 +187,9 @@ module Term = struct Or (t1, t2) - let is_zero = function Const c -> Q.equal c Q.zero | _ -> false + let is_zero = function Const c -> Q.is_zero c | _ -> false - let is_non_zero_const = function Const c -> not (Q.equal c Q.zero) | _ -> false + let is_non_zero_const = function Const c -> Q.is_not_zero c | _ -> false (** Fold [f] on the strict sub-terms of [t], if any. Preserve physical equality if [f] does. *) let fold_map_direct_subterms t ~init ~f = @@ -397,46 +411,46 @@ module Atom = struct (* [~~t = t] *) t | Not (Const c) -> - if Q.equal c Q.zero then (* [!0 = 1] *) + if Q.is_zero c then (* [!0 = 1] *) one else (* [! = 0] *) zero | Add (Const c1, Const c2) -> (* constants *) Const (Q.add c1 c2) - | Add (Const c, t) when Q.equal c Q.zero -> + | Add (Const c, t) when Q.is_zero c -> (* [0 + t = t] *) t - | Add (t, Const c) when Q.equal c Q.zero -> + | Add (t, Const c) when Q.is_zero c -> (* [t + 0 = t] *) t - | Mult (Const c, t) when Q.equal c Q.one -> + | Mult (Const c, t) when Q.is_one c -> (* [1 × t = t] *) t - | Mult (t, Const c) when Q.equal c Q.one -> + | Mult (t, Const c) when Q.is_one c -> (* [t × 1 = t] *) t - | Mult (Const c, _) when Q.equal c Q.zero -> + | Mult (Const c, _) when Q.is_zero c -> (* [0 × t = 0] *) zero - | Mult (_, Const c) when Q.equal c Q.zero -> + | Mult (_, Const c) when Q.is_zero c -> (* [t × 0 = 0] *) zero - | Div (Const c, _) when Q.equal c Q.zero -> + | Div (Const c, _) when Q.is_zero c -> (* [0 / t = 0] *) zero - | Div (t, Const c) when Q.equal c Q.one -> + | Div (t, Const c) when Q.is_one c -> (* [t / 1 = t] *) t - | Div (t, Const c) when Q.equal c Q.minus_one -> + | Div (t, Const c) when Q.is_minus_one c -> (* [t / (-1) = -t] *) eval_term (Minus t) | Div (Minus t1, Minus t2) -> (* [(-t1) / (-t2) = t1 / t2] *) eval_term (Div (t1, t2)) - | Mod (Const c, _) when Q.equal c Q.zero -> + | Mod (Const c, _) when Q.is_zero c -> (* [0 % t = 0] *) zero - | Mod (_, Const q) when Q.equal q Q.one -> + | Mod (_, Const q) when Q.is_one q -> (* [t % 1 = 0] *) zero | Mod (t1, t2) when equal_syntax t1 t2 -> @@ -480,7 +494,7 @@ module Atom = struct | Equal _ -> eval_result_of_bool (Q.equal c1 c2) | NotEqual _ -> - eval_result_of_bool (not (Q.equal c1 c2)) + eval_result_of_bool (Q.not_equal c1 c2) | LessEqual _ -> eval_result_of_bool (Q.leq c1 c2) | LessThan _ -> @@ -585,14 +599,14 @@ end = struct if Var.Map.is_empty vs then Q.pp_print fmt c else let pp_c fmt c = - if Q.equal c Q.zero then () + if Q.is_zero c then () else let plusminus, c_pos = if Q.geq c Q.zero then ('+', c) else ('-', Q.neg c) in F.fprintf fmt " %c%a" plusminus Q.pp_print c_pos in let pp_coeff fmt q = - if Q.equal q Q.one then () - else if Q.equal q Q.minus_one then F.pp_print_string fmt "-" + if Q.is_one q then () + else if Q.is_minus_one q then F.pp_print_string fmt "-" else F.fprintf fmt "%a·" Q.pp_print q in let pp_vs fmt vs = @@ -608,7 +622,7 @@ end = struct ( Var.Map.union (fun _v c1 c2 -> let c = Q.add c1 c2 in - if Q.equal c Q.zero then None else Some c ) + if Q.is_zero c then None else Some c ) vs1 vs2 , Q.add c1 c2 ) @@ -619,18 +633,18 @@ end = struct let zero = (Var.Map.empty, Q.zero) - let is_zero (vs, c) = Q.equal c Q.zero && Var.Map.is_empty vs + let is_zero (vs, c) = Q.is_zero c && Var.Map.is_empty vs let mult q ((vs, c) as l) = - if Q.equal q Q.zero then (* needed for correction: coeffs cannot be zero *) zero - else if Q.equal q Q.one then (* purely an optimisation *) l + if Q.is_zero q then (* needed for correction: coeffs cannot be zero *) zero + else if Q.is_one q then (* purely an optimisation *) l else (Var.Map.map (fun c -> Q.mul q c) vs, Q.mul q c) let solve_eq_zero (vs, c) = match Var.Map.min_binding_opt vs with | None -> - if Q.equal c Q.zero then Sat None else Unsat + if Q.is_zero c then Sat None else Unsat | Some (x, coeff) -> let d = Q.neg coeff in let vs' = @@ -671,7 +685,7 @@ end = struct | 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) -> + | Div (t, Const c) when Q.is_not_zero c -> let+ l = of_term t in mult (Q.inv c) l | Mult _ @@ -696,9 +710,9 @@ end = struct let get_as_const (vs, c) = if Var.Map.is_empty vs then Some c else None let get_as_var (vs, c) = - if Q.equal c Q.zero then + if Q.is_zero c then match Var.Map.is_singleton_or_more vs with - | Singleton (x, cx) when Q.equal cx Q.one -> + | Singleton (x, cx) when Q.is_one cx -> Some x | _ -> None @@ -729,7 +743,7 @@ end = struct Var.Map.add v q0 vs | Some q -> let q' = Q.add q q0 in - if Q.equal q' Q.zero then Var.Map.remove v vs else Var.Map.add v q vs + if Q.is_zero q' then Var.Map.remove v vs else Var.Map.add v q vs in (acc_f, vs) ) vs_foreign (init, Var.Map.empty) diff --git a/infer/src/pulse/unit/PulseFormulaTest.ml b/infer/src/pulse/unit/PulseFormulaTest.ml index 2c3993551..79889b365 100644 --- a/infer/src/pulse/unit/PulseFormulaTest.ml +++ b/infer/src/pulse/unit/PulseFormulaTest.ml @@ -10,120 +10,124 @@ module AbstractValue = PulseAbstractValue open PulseFormula open SatUnsatMonad -let%test_module _ = - ( module struct - (** {2 Utilities for defining formulas easily} +(** {2 Utilities for defining formulas easily} + + We want to be able to write something close to [x + y - 42 < z], but the API of {!PulseFormula} + doesn't support building arbitrary formulas or even arbitrary terms. Instead, we have to + introduce intermediate variables for each sub-expression (this corresponds to how the rest of + Pulse interacts with the arithmetic layer, so it's good that we follow this convention here + too). + + The definitions here make this transparent by passing the formula around. For example, building + [x+y] takes in a formula [phi] and returns [(phi ∧ v123 = x+y, v123)], i.e. a pair of the + formula with a new intermediate equality and the resulting intermediate variable. This allows us + to chain operations: [x+y-42] is a function that takes a formula, passes it to [x+y] returning + [(phi',v123)] as we saw with [phi' = phi ∧ v123 = x+y], passes it to "42", which here is also + a function returning [(phi',42)] (note the unchanged [phi']), then finally returns + [(phi ∧ v123 = x+y ∧ v234 = v123-42, v234)]. - We want to be able to write something close to [x + y - 42 < z], but the API of - {!PulseFormula} doesn't support building arbitrary formulas or even arbitrary terms. - Instead, we have to introduce intermediate variables for each sub-expression (this - corresponds to how the reste of Pulse interacts with the arithmetic layer too, so it's good - that we follow this constraint here too). + This is convoluted, especially as each step may also return [Unsat] even during "term" + construction, but as a result the tests themselves should be straightforward to understand. *) - The definitions here make this transparent by passing the formula around. For example, - building [x+y] takes in a formula [phi] and returns [(phi ∧ v123 = x+y, v123)], i.e. a - pair of the formula with a new intermediate equality and the resulting intermediate - variable. This allows us to chain operations: [x+y-42] is a function that takes a formula, - passes it to [x+y] returning [(phi',v123)] as we saw with [phi' = phi ∧ v123 = x+y], - passes it to "42", which here is also a function returning [(phi',42)] (note the unchanged - [phi']), then finally returns [(phi ∧ v123 = x+y ∧ v234 = v123-42, v234)]. +(** a literal integer leaves the formula unchanged and returns a [LiteralOperand] *) +let i i phi = Sat (phi, LiteralOperand (IntLit.of_int i)) - This is convoluted, especially as each step may also return [Unsat] even during "term" - construction, but as a result the tests themselves should be straightforward to understand. *) +(** similarly as for literals; this is not used directly in tests so the name is a bit more + descriptive *) +let op_of_var x phi = Sat (phi, AbstractValueOperand x) - (** a literal integer leaves the formula unchanged and returns a [LiteralOperand] *) - let i i phi = Sat (phi, LiteralOperand (IntLit.of_int i)) +let of_binop bop f1 f2 phi = + let* phi, op1 = f1 phi in + let* phi, op2 = f2 phi in + let v = Var.mk_fresh () in + let+ phi = and_equal_binop v bop op1 op2 phi in + (phi, AbstractValueOperand v) - (** similarly as for literals; this is not used directly in tests so the name is a bit more - descriptive *) - let op_of_var x phi = Sat (phi, AbstractValueOperand x) - let of_binop bop f1 f2 phi = - let* phi, op1 = f1 phi in - let* phi, op2 = f2 phi in - let v = Var.mk_fresh () in - let+ phi = and_equal_binop v bop op1 op2 phi in - (phi, AbstractValueOperand v) +let ( + ) f1 f2 phi = of_binop (PlusA None) f1 f2 phi +let ( - ) f1 f2 phi = of_binop (MinusA None) f1 f2 phi - let ( + ) f1 f2 phi = of_binop (PlusA None) f1 f2 phi +let ( * ) f1 f2 phi = of_binop (Mult None) f1 f2 phi - let ( - ) f1 f2 phi = of_binop (MinusA None) f1 f2 phi +let ( / ) f1 f2 phi = of_binop Div f1 f2 phi - let ( * ) f1 f2 phi = of_binop (Mult None) f1 f2 phi +let ( & ) f1 f2 phi = of_binop BAnd f1 f2 phi - let ( / ) f1 f2 phi = of_binop Div f1 f2 phi +let ( mod ) f1 f2 phi = of_binop Mod f1 f2 phi - let ( = ) f1 f2 phi = - let* phi, op1 = f1 phi in - let* phi, op2 = f2 phi in - and_equal op1 op2 phi +let ( = ) f1 f2 phi = + let* phi, op1 = f1 phi in + let* phi, op2 = f2 phi in + and_equal op1 op2 phi - let ( < ) f1 f2 phi = - let* phi, op1 = f1 phi in - let* phi, op2 = f2 phi in - and_less_than op1 op2 phi +let ( < ) f1 f2 phi = + let* phi, op1 = f1 phi in + let* phi, op2 = f2 phi in + and_less_than op1 op2 phi - let ( && ) f1 f2 phi = f1 phi >>= f2 +let ( && ) f1 f2 phi = f1 phi >>= f2 - (* we remember a mapping [Var.t -> string] to print more readable results that mention the - user-defined variables by their readable names instead of [v123] *) - let var_names = Caml.Hashtbl.create 4 +(* we remember a mapping [Var.t -> string] to print more readable results that mention the + user-defined variables by their readable names instead of [v123] *) +let var_names = Caml.Hashtbl.create 4 - let mk_var name = - let v = AbstractValue.mk_fresh () in - Caml.Hashtbl.add var_names v name ; - v +let mk_var name = + let v = AbstractValue.mk_fresh () in + Caml.Hashtbl.add var_names v name ; + v - let x_var = mk_var "x" +let x_var = mk_var "x" - let x = op_of_var x_var +let x = op_of_var x_var - let y_var = mk_var "y" +let y_var = mk_var "y" - let y = op_of_var y_var +let y = op_of_var y_var - let z_var = mk_var "z" +let z_var = mk_var "z" - let z = op_of_var z_var +let z = op_of_var z_var - let w = op_of_var (mk_var "w") +let w_var = mk_var "w" - let v = op_of_var (mk_var "v") +let w = op_of_var w_var - (** reset to this state before each test so that variable id's remain stable when tests are - added in the future *) - let init_vars_state = AbstractValue.State.get () +let v = op_of_var (mk_var "v") - let pp_var fmt v = - match Caml.Hashtbl.find_opt var_names v with - | Some name -> - F.pp_print_string fmt name - | None -> - AbstractValue.pp fmt v +(** reset to this state before each test so that variable id's remain stable when tests are added in + the future *) +let init_vars_state = AbstractValue.State.get () +let pp_var fmt v = + match Caml.Hashtbl.find_opt var_names v with + | Some name -> + F.pp_print_string fmt name + | None -> + AbstractValue.pp fmt v - let normalized_pp fmt = function - | Unsat -> - F.pp_print_string fmt "unsat" - | Sat phi -> - pp_with_pp_var pp_var fmt phi +let normalized_pp fmt = function + | Unsat -> + F.pp_print_string fmt "unsat" + | Sat phi -> + pp_with_pp_var pp_var fmt phi - let test ~f phi = - AbstractValue.State.set init_vars_state ; - phi ttrue >>= f |> F.printf "%a" normalized_pp +let test ~f phi = + AbstractValue.State.set init_vars_state ; + phi ttrue >>= f |> F.printf "%a" normalized_pp - let normalize phi = test ~f:normalize phi - let simplify ~keep phi = test ~f:(simplify ~keep:(AbstractValue.Set.of_list keep)) phi +let normalize phi = test ~f:normalize phi - (** the actual tests *) +let simplify ~keep phi = test ~f:(simplify ~keep:(AbstractValue.Set.of_list keep)) phi +let%test_module "normalization" = + ( module struct let%expect_test _ = normalize (x < y) ; [%expect {|true (no var=var) && true (no linear) && {x < y}|}] @@ -194,7 +198,10 @@ let%test_module _ = ∧ v8 = x + v6 +1 ∧ v9 = 0 ∧ v10 = 0 && true (no atoms)|}] + end ) +let%test_module "variable elimination" = + ( module struct 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)|}] @@ -226,3 +233,14 @@ let%test_module _ = simplify ~keep:[x_var; y_var] (x = y + i 4 && x = w && y = z) ; [%expect {|x=w=v6 ∧ y=z && x = y +4 && true (no atoms)|}] end ) + +let%test_module "non-linear simplifications" = + ( module struct + let%expect_test "zero propagation" = + simplify ~keep:[w_var] (((i 0 / (x * z)) & v) * v mod y = w) ; + [%expect {|w=v10 && true (no linear) && {w = v9 mod y}∧{v8 = 0&v}∧{v9 = v8×v}|}] + + let%expect_test "constant propagation: bitshift" = + simplify ~keep:[x_var] (of_binop Shiftlt (of_binop Shiftrt (i 0b111) (i 2)) (i 2) = x) ; + [%expect {|x=v7 && true (no linear) && {x = v6<<2}∧{v6 = 7>>2}|}] + end )