From c440c4fc286c55f594675ea53dd7537ca06c6319 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 9 Oct 2019 02:56:19 -0700 Subject: [PATCH] [sledge] Remove unsigned Term operations except Extract Summary: Instead of having separate signed and unsigned operations, use the signed operations applied to explicit conversion of the arguments using an unsigned integer interpretation. Reviewed By: bennostein Differential Revision: D17665267 fbshipit-source-id: 0b3271e71 --- sledge/src/symbheap/term.ml | 137 ++++--------------------------- sledge/src/symbheap/term.mli | 12 --- sledge/src/symbheap/term_test.ml | 7 +- 3 files changed, 22 insertions(+), 134 deletions(-) diff --git a/sledge/src/symbheap/term.ml b/sledge/src/symbheap/term.ml index df131d888..c05aa5a44 100644 --- a/sledge/src/symbheap/term.ml +++ b/sledge/src/symbheap/term.ml @@ -7,27 +7,12 @@ (** Terms *) -(** Z wrapped to treat bounded and unsigned operations *) module Z = struct include Z (** Interpret as a bounded integer with specified signedness and width. *) let extract ?(unsigned = false) bits z = if unsigned then Z.extract z 0 bits else Z.signed_extract z 0 bits - - let extract_cmp ~unsigned bits op x y = - op (extract ~unsigned bits x) (extract ~unsigned bits y) - - let extract_bop ~unsigned bits op x y = - extract ~unsigned bits - (op (extract ~unsigned bits x) (extract ~unsigned bits y)) - - let buleq ~bits x y = extract_cmp ~unsigned:true bits Z.leq x y - let bugeq ~bits x y = extract_cmp ~unsigned:true bits Z.geq x y - let bult ~bits x y = extract_cmp ~unsigned:true bits Z.lt x y - let bugt ~bits x y = extract_cmp ~unsigned:true bits Z.gt x y - let budiv ~bits x y = extract_bop ~unsigned:true bits Z.div x y - let burem ~bits x y = extract_bop ~unsigned:true bits Z.rem x y end module rec T : sig @@ -54,17 +39,11 @@ module rec T : sig | Ge | Lt | Le - | Ugt - | Uge - | Ult - | Ule | Ord | Uno (* binary: arithmetic, numeric and pointer *) | Div - | Udiv | Rem - | Urem (* binary: boolean / bitwise *) | And | Or @@ -118,16 +97,10 @@ and T0 : sig | Ge | Lt | Le - | Ugt - | Uge - | Ult - | Ule | Ord | Uno | Div - | Udiv | Rem - | Urem | And | Or | Xor @@ -163,16 +136,10 @@ end = struct | Ge | Lt | Le - | Ugt - | Uge - | Ult - | Ule | Ord | Uno | Div - | Udiv | Rem - | Urem | And | Or | Xor @@ -252,10 +219,6 @@ let rec pp ?is_x fs term = | Ge -> pf "@<1>≥" | Lt -> pf "<" | Le -> pf "@<1>≤" - | Ugt -> pf "u>" - | Uge -> pf "@<2>u≥" - | Ult -> pf "u<" - | Ule -> pf "@<2>u≤" | Ord -> pf "ord" | Uno -> pf "uno" | Add {args} -> @@ -274,9 +237,7 @@ let rec pp ?is_x fs term = in pf "(%a)" (Qset.pp "@ @<2>× " pp_mono_term) args | Div -> pf "/" - | Udiv -> pf "udiv" | Rem -> pf "rem" - | Urem -> pf "urem" | And -> pf "&&" | Or -> pf "||" | Xor -> pf "xor" @@ -350,15 +311,9 @@ let pp = pp_t let rec typ_of = function | Add {typ} | Mul {typ} | Integer {typ} | App {op= Convert {dst= typ}} -> Some typ - | App {op= App {op= Eq | Dq | Gt | Ge | Lt | Le | Ugt | Uge | Ult | Ule}} - -> - Some Typ.bool + | App {op= App {op= Eq | Dq | Gt | Ge | Lt | Le}} -> Some Typ.bool | App - { op= - App - { op= - Div | Udiv | Rem | Urem | And | Or | Xor | Shl | Lshr | Ashr - ; arg= x } + { op= App {op= Div | Rem | And | Or | Xor | Shl | Lshr | Ashr; arg= x} ; arg= y } -> ( match typ_of x with Some _ as t -> t | None -> typ_of y ) | App {op= App {op= App {op= Conditional}; arg= thn}; arg= els} -> ( @@ -456,8 +411,8 @@ let invariant ?(partial = false) e = assert (Typ.convertible src dst) | Add _ -> assert_polynomial e |> Fn.id | Mul {typ} -> assert_monomial typ e |> Fn.id - | Eq | Dq | Gt | Ge | Lt | Le | Ugt | Uge | Ult | Ule | Div | Udiv | Rem - |Urem | And | Or | Xor | Shl | Lshr | Ashr -> ( + | Eq | Dq | Gt | Ge | Lt | Le | Div | Rem | And | Or | Xor | Shl | Lshr + |Ashr -> ( match args with | [x; y] -> ( match (typ_of x, typ_of y) with @@ -659,45 +614,21 @@ let simp_gt x y = | Integer {data= i}, Integer {data= j} -> bool (Z.gt i j) | _ -> App {op= App {op= Gt; arg= x}; arg= y} -let simp_ugt x y = - match (x, y) with - | Integer {data= i}, Integer {data= j; typ= Integer {bits}} -> - bool (Z.bugt ~bits i j) - | _ -> App {op= App {op= Ugt; arg= x}; arg= y} - let simp_ge x y = match (x, y) with | Integer {data= i}, Integer {data= j} -> bool (Z.geq i j) | _ -> App {op= App {op= Ge; arg= x}; arg= y} -let simp_uge x y = - match (x, y) with - | Integer {data= i}, Integer {data= j; typ= Integer {bits}} -> - bool (Z.bugeq ~bits i j) - | _ -> App {op= App {op= Uge; arg= x}; arg= y} - let simp_lt x y = match (x, y) with | Integer {data= i}, Integer {data= j} -> bool (Z.lt i j) | _ -> App {op= App {op= Lt; arg= x}; arg= y} -let simp_ult x y = - match (x, y) with - | Integer {data= i}, Integer {data= j; typ= Integer {bits}} -> - bool (Z.bult ~bits i j) - | _ -> App {op= App {op= Ult; arg= x}; arg= y} - let simp_le x y = match (x, y) with | Integer {data= i}, Integer {data= j} -> bool (Z.leq i j) | _ -> App {op= App {op= Le; arg= x}; arg= y} -let simp_ule x y = - match (x, y) with - | Integer {data= i}, Integer {data= j; typ= Integer {bits}} -> - bool (Z.buleq ~bits i j) - | _ -> App {op= App {op= Ule; arg= x}; arg= y} - let simp_ord x y = App {op= App {op= Ord; arg= x}; arg= y} let simp_uno x y = App {op= App {op= Uno; arg= x}; arg= y} @@ -730,16 +661,6 @@ and simp_div x y = sum_to_term typ (sum_mul_const Q.(inv (of_z data)) args) | _ -> App {op= App {op= Div; arg= x}; arg= y} -let simp_udiv x y = - match (x, y) with - (* i u/ j *) - | Integer {data= i; typ}, Integer {data= j} when not (Z.equal Z.zero j) -> - let bits = Option.value_exn (Typ.prim_bit_size_of typ) in - integer (Z.budiv ~bits i j) typ - (* e u/ 1 ==> e *) - | e, Integer {data} when Z.equal Z.one data -> e - | _ -> App {op= App {op= Udiv; arg= x}; arg= y} - let simp_rem x y = match (x, y) with (* i % j *) @@ -749,16 +670,6 @@ let simp_rem x y = | _, Integer {data; typ} when Z.equal Z.one data -> integer Z.zero typ | _ -> App {op= App {op= Rem; arg= x}; arg= y} -let simp_urem x y = - match (x, y) with - (* i u% j *) - | Integer {data= i; typ}, Integer {data= j} when not (Z.equal Z.zero j) -> - let bits = Option.value_exn (Typ.prim_bit_size_of typ) in - integer (Z.burem ~bits i j) typ - (* e u% 1 ==> 0 *) - | _, Integer {data; typ} when Z.equal Z.one data -> integer Z.zero typ - | _ -> App {op= App {op= Urem; arg= x}; arg= y} - (* Sums of polynomial terms represented by multisets. A sum ∑ᵢ cᵢ × Xᵢ of monomials Xᵢ with coefficients cᵢ is represented by a multiset where the elements are Xᵢ with multiplicities cᵢ. A constant is treated as the @@ -932,14 +843,6 @@ let rec simp_not (typ : Typ.t) term = | App {op= App {op= Lt; arg= x}; arg= y} -> simp_ge x y (* ¬(x <= y) ==> x > y *) | App {op= App {op= Le; arg= x}; arg= y} -> simp_gt x y - (* ¬(x u> y) ==> x u<= y *) - | App {op= App {op= Ugt; arg= x}; arg= y} -> simp_ule x y - (* ¬(x u>= y) ==> x u< y *) - | App {op= App {op= Uge; arg= x}; arg= y} -> simp_ult x y - (* ¬(x u< y) ==> x u>= y *) - | App {op= App {op= Ult; arg= x}; arg= y} -> simp_uge x y - (* ¬(x u<= y) ==> x u> y *) - | App {op= App {op= Ule; arg= x}; arg= y} -> simp_ugt x y (* ¬(x ≠ nan ∧ y ≠ nan) ==> x = nan ∨ y = nan *) | App {op= App {op= Ord; arg= x}; arg= y} -> simp_uno x y (* ¬(x = nan ∨ y = nan) ==> x ≠ nan ∧ y ≠ nan *) @@ -1065,16 +968,10 @@ let app1 ?(partial = false) op arg = | App {op= Ge; arg= x}, y -> simp_ge x y | App {op= Lt; arg= x}, y -> simp_lt x y | App {op= Le; arg= x}, y -> simp_le x y - | App {op= Ugt; arg= x}, y -> simp_ugt x y - | App {op= Uge; arg= x}, y -> simp_uge x y - | App {op= Ult; arg= x}, y -> simp_ult x y - | App {op= Ule; arg= x}, y -> simp_ule x y | App {op= Ord; arg= x}, y -> simp_ord x y | App {op= Uno; arg= x}, y -> simp_uno x y | App {op= Div; arg= x}, y -> simp_div x y - | App {op= Udiv; arg= x}, y -> simp_udiv x y | App {op= Rem; arg= x}, y -> simp_rem x y - | App {op= Urem; arg= x}, y -> simp_urem x y | App {op= And; arg= x}, y -> simp_and x y | App {op= Or; arg= x}, y -> simp_or x y | App {op= Xor; arg= x}, y -> simp_xor x y @@ -1158,10 +1055,6 @@ let gt = app2 Gt let ge = app2 Ge let lt = app2 Lt let le = app2 Le -let ugt = app2 Ugt -let uge = app2 Uge -let ult = app2 Ult -let ule = app2 Ule let ord = app2 Ord let uno = app2 Uno let neg = check1 simp_negate @@ -1169,9 +1062,7 @@ let add = check2 simp_add2 let sub = check2 simp_sub let mul = check2 simp_mul2 let div = app2 Div -let udiv = app2 Udiv let rem = app2 Rem -let urem = app2 Urem let and_ = app2 And let or_ = app2 Or let xor = app2 Xor @@ -1213,6 +1104,14 @@ let convert ?(unsigned = false) ~dst ~src term = app1 (Convert {unsigned; dst; src}) term let rec of_exp (e : Exp.t) = + let unsigned op typ x y = + match Typ.prim_bit_size_of typ with + | Some bits -> + op + (extract ~unsigned:true ~bits (of_exp x)) + (extract ~unsigned:true ~bits (of_exp y)) + | None -> violates Exp.invariant e + in match e with | Reg {name} -> var (Var {id= 0; name}) | Nondet {msg} -> nondet msg @@ -1231,10 +1130,10 @@ let rec of_exp (e : Exp.t) = | Ap2 (Ge, _, x, y) -> ge (of_exp x) (of_exp y) | Ap2 (Lt, _, x, y) -> lt (of_exp x) (of_exp y) | Ap2 (Le, _, x, y) -> le (of_exp x) (of_exp y) - | Ap2 (Ugt, _, x, y) -> ugt (of_exp x) (of_exp y) - | Ap2 (Uge, _, x, y) -> uge (of_exp x) (of_exp y) - | Ap2 (Ult, _, x, y) -> ult (of_exp x) (of_exp y) - | Ap2 (Ule, _, x, y) -> ule (of_exp x) (of_exp y) + | Ap2 (Ugt, typ, x, y) -> unsigned gt typ x y + | Ap2 (Uge, typ, x, y) -> unsigned ge typ x y + | Ap2 (Ult, typ, x, y) -> unsigned lt typ x y + | Ap2 (Ule, typ, x, y) -> unsigned le typ x y | Ap2 (Ord, _, x, y) -> ord (of_exp x) (of_exp y) | Ap2 (Uno, _, x, y) -> uno (of_exp x) (of_exp y) | Ap2 (Add, typ, x, y) -> add typ (of_exp x) (of_exp y) @@ -1242,8 +1141,8 @@ let rec of_exp (e : Exp.t) = | Ap2 (Mul, typ, x, y) -> mul typ (of_exp x) (of_exp y) | Ap2 (Div, _, x, y) -> div (of_exp x) (of_exp y) | Ap2 (Rem, _, x, y) -> rem (of_exp x) (of_exp y) - | Ap2 (Udiv, _, x, y) -> udiv (of_exp x) (of_exp y) - | Ap2 (Urem, _, x, y) -> urem (of_exp x) (of_exp y) + | Ap2 (Udiv, typ, x, y) -> unsigned div typ x y + | Ap2 (Urem, typ, x, y) -> unsigned rem typ x y | Ap2 (And, _, x, y) -> and_ (of_exp x) (of_exp y) | Ap2 (Or, _, x, y) -> or_ (of_exp x) (of_exp y) | Ap2 (Xor, _, x, y) -> xor (of_exp x) (of_exp y) diff --git a/sledge/src/symbheap/term.mli b/sledge/src/symbheap/term.mli index a63f8fa10..23bb4958f 100644 --- a/sledge/src/symbheap/term.mli +++ b/sledge/src/symbheap/term.mli @@ -41,16 +41,10 @@ and t = private | Ge (** Greater-than-or-equal test *) | Lt (** Less-than test *) | Le (** Less-than-or-equal test *) - | Ugt (** Unsigned greater-than test *) - | Uge (** Unsigned greater-than-or-equal test *) - | Ult (** Unsigned less-than test *) - | Ule (** Unsigned less-than-or-equal test *) | Ord (** Ordered test (neither arg is nan) *) | Uno (** Unordered test (some arg is nan) *) | Div (** Division *) - | Udiv (** Unsigned division *) | Rem (** Remainder of division *) - | Urem (** Remainder of unsigned division *) | And (** Conjunction, boolean or bitwise *) | Or (** Disjunction, boolean or bitwise *) | Xor (** Exclusive-or, bitwise *) @@ -151,10 +145,6 @@ val gt : t -> t -> t val ge : t -> t -> t val lt : t -> t -> t val le : t -> t -> t -val ugt : t -> t -> t -val uge : t -> t -> t -val ult : t -> t -> t -val ule : t -> t -> t val ord : t -> t -> t val uno : t -> t -> t val neg : Typ.t -> t -> t @@ -162,9 +152,7 @@ val add : Typ.t -> t -> t -> t val sub : Typ.t -> t -> t -> t val mul : Typ.t -> t -> t -> t val div : t -> t -> t -val udiv : t -> t -> t val rem : t -> t -> t -val urem : t -> t -> t val and_ : t -> t -> t val or_ : t -> t -> t val xor : t -> t -> t diff --git a/sledge/src/symbheap/term_test.ml b/sledge/src/symbheap/term_test.ml index 54bb43499..c1616931b 100644 --- a/sledge/src/symbheap/term_test.ml +++ b/sledge/src/symbheap/term_test.ml @@ -51,9 +51,10 @@ let%test_module _ = let%test "unsigned boolean overflow" = Term.is_true - (Term.uge - (Term.integer Z.minus_one Typ.bool) - (Term.integer Z.one Typ.bool)) + (Term.of_exp + (Exp.uge Typ.bool + (Exp.integer Typ.bool Z.minus_one) + (Exp.integer Typ.bool Z.one))) let%expect_test _ = pp (!42 + !13) ;