@ -10,120 +10,124 @@ module AbstractValue = PulseAbstractValue
open PulseFormula open PulseFormula
open SatUnsatMonad open SatUnsatMonad
let % test_module _ = (* * {2 Utilities for defining formulas easily}
( module struct
(* * {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
This is convoluted , especially as each step may also return [ Unsat ] even during " term "
{ ! PulseFormula } doesn't support building arbitrary formulas or even arbitrary terms .
construction , but as a result the tests themselves should be straightforward to understand . * )
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 ) .
The definitions here make this transparent by passing the formula around . For example ,
(* * a literal integer leaves the formula unchanged and returns a [LiteralOperand] *)
building [ x + y ] takes in a formula [ phi ] and returns [ ( phi ∧ v123 = x + y , v123 ) ] , i . e . a
let i i phi = Sat ( phi , LiteralOperand ( IntLit . of_int i ) )
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 ) ] .
This is convoluted , especially as each step may also return [ Unsat ] even during " term "
(* * similarly as for literals; this is not used directly in tests so the name is a bit more
construction , but as a result the tests themselves should be straightforward to understand . * )
descriptive * )
let op_of_var x phi = Sat ( phi , AbstractValueOperand x )
(* * a literal integer leaves the formula unchanged and returns a [LiteralOperand] *)
let of_binop bop f1 f2 phi =
let i i phi = Sat ( phi , LiteralOperand ( IntLit . of_int i ) )
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 ( + ) f1 f2 phi = of_binop ( PlusA None ) 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 ( 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 ( = ) f1 f2 phi =
let * phi , op1 = f1 phi in let * phi , op1 = f1 phi in
let * phi , op2 = f2 phi in let * phi , op2 = f2 phi in
and_equal op1 op2 phi and_equal op1 op2 phi
let ( < ) f1 f2 phi = let ( < ) f1 f2 phi =
let * phi , op1 = f1 phi in let * phi , op1 = f1 phi in
let * phi , op2 = f2 phi in let * phi , op2 = f2 phi in
and_less_than op1 op2 phi 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 (* 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 ] * ) user - defined variables by their readable names instead of [ v123 ] * )
let var_names = Caml . Hashtbl . create 4 let var_names = Caml . Hashtbl . create 4
let mk_var name = let mk_var name =
let v = AbstractValue . mk_fresh () in let v = AbstractValue . mk_fresh () in
Caml . Hashtbl . add var_names v name ; Caml . Hashtbl . add var_names v name ;
v 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
let v = op_of_var ( mk_var " v " )
added in the future * )
let init_vars_state = AbstractValue . State . get ()
let pp_var fmt v =
(* * reset to this state before each test so that variable id's remain stable when tests are added in
match Caml . Hashtbl . find_opt var_names v with
the future * )
| Some name ->
let init_vars_state = AbstractValue . State . get ()
F . pp_print_string fmt name
| None ->
AbstractValue . pp fmt 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
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 _ =
let % expect_test _ =
normalize ( x < y ) ;
normalize ( x < y ) ;
[ % expect { | true ( no var = var ) && true ( no linear ) && { 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
∧ v8 = x + v6 + 1 ∧ v9 = 0 ∧ v10 = 0
&&
&&
true ( no atoms ) | } ]
true ( no atoms ) | } ]
end )
let % test_module " variable elimination " =
( module struct
let % expect_test _ =
let % expect_test _ =
simplify ~ keep : [ x_var ] ( x = i 0 && y = i 1 && z = i 2 && w = i 3 ) ;
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 ) | } ]
[ % 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 ) ;
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 ) | } ]
[ % expect { | x = w = v6 ∧ y = z && x = y + 4 && true ( no atoms ) | } ]
end )
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 )
Jules Villard
4 years ago
committed by
Facebook GitHub Bot