pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[pulse] add a term_eqs field to formulas

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

Reviewed By: skcho

Differential Revision: D27328348

fbshipit-source-id: 4f5bfcc65
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent a5b4992873
commit 2d83dfdcb0
2 changed files with 107 additions and 32 deletions
Show Stats Download Patch File Download Diff File

64
infer/src/pulse/PulseFormula.ml
Unescape View File

@ -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

75
infer/src/pulse/unit/PulseFormulaTest.ml
Unescape View File

@ -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 )

Write Preview
Loading…
Cancel
Save