From 718aa27c8d2f1f882c7e62e45b7ff57c6f206977 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 31 Oct 2018 11:16:21 -0700 Subject: [PATCH] [sledge] Add typ of Add and Mul expressions Reviewed By: mbouaziz Differential Revision: D12854503 fbshipit-source-id: ee4b90fe1 --- sledge/src/llair/exp.ml | 45 ++++++++++++++++--------------- sledge/src/llair/exp.mli | 4 +-- sledge/src/symbheap/congruence.ml | 11 ++++---- sledge/src/symbheap/sh.ml | 2 +- 4 files changed, 31 insertions(+), 31 deletions(-) diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 4393193ab..21375efef 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -90,8 +90,8 @@ module T0 = struct | Ord | Uno (* binary: arithmetic, numeric and pointer *) - | Add - | Mul + | Add of {typ: Typ.t} + | Mul of {typ: Typ.t} | Div | Udiv | Rem @@ -178,8 +178,8 @@ module T = struct | Ule -> pf "u<=" | Ord -> pf "ord" | Uno -> pf "uno" - | Add -> pf "+" - | Mul -> pf "*" + | Add _ -> pf "+" + | Mul _ -> pf "*" | Div -> pf "/" | Udiv -> pf "udiv" | Rem -> pf "rem" @@ -264,8 +264,8 @@ let invariant ?(partial = false) e = | [Integer {typ}] -> assert (Typ.equal src typ) | _ -> assert_arity 1 ) ; assert (Typ.convertible src dst) - | Eq | Dq | Gt | Ge | Lt | Le | Ugt | Uge | Ult | Ule | Add | Mul | Div - |Udiv | Rem | Urem | And | Or | Xor | Shl | Lshr | Ashr -> ( + | Eq | Dq | Gt | Ge | Lt | Le | Ugt | Uge | Ult | Ule | Add _ | Mul _ + |Div | Udiv | Rem | Urem | And | Or | Xor | Shl | Lshr | Ashr -> ( match args with | [Integer {typ= Integer {bits= m}}; Integer {typ= Integer {bits= n}}] -> @@ -555,7 +555,7 @@ and simp_eq x y = | Integer {data= i; typ= Integer {bits}}, Integer {data= j} -> bool (Z.eq ~bits i j) (* e+i = j ==> e = j-i *) - | ( App {op= App {op= Add; arg= e}; arg= Integer {data= i}} + | ( App {op= App {op= Add _; arg= e}; arg= Integer {data= i}} , Integer {data= j; typ= Integer {bits} as typ} ) -> simp_eq e (integer (Z.sub ~bits j i) typ) (* b = false ==> ¬b *) @@ -581,7 +581,7 @@ and simp_dq x y = | Integer {data= i; typ= Integer {bits}}, Integer {data= j} -> bool (not (Z.eq ~bits i j)) (* e+i != j ==> e != j-i *) - | ( App {op= App {op= Add; arg= e}; arg= Integer {data= i}} + | ( App {op= App {op= Add _; arg= e}; arg= Integer {data= i}} , Integer {data= j; typ= Integer {bits} as typ} ) -> simp_dq e (integer (Z.sub ~bits j i) typ) (* b != false ==> b *) @@ -690,31 +690,32 @@ let simp_ashr x y = | e, Integer {data} when Z.equal Z.zero data -> e | _ -> App {op= App {op= Ashr; arg= x}; arg= y} -let rec simp_add x y = +let rec simp_add typ x y = match (x, y) with (* i + j *) | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} -> integer (Z.add ~bits i j) typ (* i + e ==> e + i *) - | Integer _, _ -> simp_add y x + | Integer _, _ -> simp_add typ y x (* e + 0 ==> e *) | e, Integer {data} when Z.equal Z.zero data -> e (* (e+i) + j ==> e+(i+j) *) | ( App - { op= App {op= Add; arg} + { op= App {op= Add _; arg} ; arg= Integer {data= i; typ= Integer {bits} as typ} } , Integer {data= j} ) -> - simp_add arg (integer (Z.add ~bits i j) typ) + simp_add typ arg (integer (Z.add ~bits i j) typ) (* (i+e) + j ==> (i+j)+e *) | ( App { op= - App {op= Add; arg= Integer {data= i; typ= Integer {bits} as typ}} + App + {op= Add _; arg= Integer {data= i; typ= Integer {bits} as typ}} ; arg } , Integer {data= j} ) -> - simp_add (integer (Z.add ~bits i j) typ) arg - | _ -> App {op= App {op= Add; arg= x}; arg= y} + simp_add typ (integer (Z.add ~bits i j) typ) arg + | _ -> App {op= App {op= Add {typ}; arg= x}; arg= y} -let simp_mul x y = +let simp_mul typ x y = match (x, y) with (* i * j *) | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} -> @@ -722,7 +723,7 @@ let simp_mul x y = (* e * 1 ==> e *) | Integer {data}, e when Z.equal Z.one data -> e | e, Integer {data} when Z.equal Z.one data -> e - | _ -> App {op= App {op= Mul; arg= x}; arg= y} + | _ -> App {op= App {op= Mul {typ}; arg= x}; arg= y} let simp_sub typ x y = match (x, y) with @@ -730,7 +731,7 @@ let simp_sub typ x y = | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} -> integer (Z.sub ~bits i j) typ (* x - y ==> x + (-1 * y) *) - | _ -> simp_add x (simp_mul (integer Z.minus_one typ) y) + | _ -> simp_add typ x (simp_mul typ (integer Z.minus_one typ) y) let simp_div x y = match (x, y) with @@ -782,8 +783,8 @@ let app1 ?(partial = false) op arg = | 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= Add; arg= x}, y -> simp_add x y - | App {op= Mul; arg= x}, y -> simp_mul x y + | App {op= Add {typ}; arg= x}, y -> simp_add typ x y + | App {op= Mul {typ}; arg= x}, y -> simp_mul typ 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 @@ -817,8 +818,8 @@ let ult = app2 Ult let ule = app2 Ule let ord = app2 Ord let uno = app2 Uno -let add typ = app2 Add -let mul typ = app2 Mul +let add typ = app2 (Add {typ}) +let mul typ = app2 (Mul {typ}) let sub = simp_sub let div = app2 Div let udiv = app2 Udiv diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index 2b971f6fe..53863eb52 100644 --- a/sledge/src/llair/exp.mli +++ b/sledge/src/llair/exp.mli @@ -49,8 +49,8 @@ type t = private | Ule (** Unsigned less-than-or-equal test *) | Ord (** Ordered test (neither arg is nan) *) | Uno (** Unordered test (some arg is nan) *) - | Add (** Addition *) - | Mul (** Multiplication *) + | Add of {typ: Typ.t} (** Addition *) + | Mul of {typ: Typ.t} (** Multiplication *) | Div (** Division *) | Udiv (** Unsigned division *) | Rem (** Remainder of division *) diff --git a/sledge/src/symbheap/congruence.ml b/sledge/src/symbheap/congruence.ml index 8ab146d24..85da5f167 100644 --- a/sledge/src/symbheap/congruence.ml +++ b/sledge/src/symbheap/congruence.ml @@ -126,25 +126,24 @@ let invariant r = let map_sum e ~f = match e with - | Exp.App {op= App {op= Add; arg= a}; arg= Integer {typ} as i} -> + | Exp.App {op= App {op= Add {typ}; arg= a}; arg= i} -> let a' = f a in if a' == a then e else Exp.add typ a' i | a -> f a let fold_sum e ~init ~f = match e with - | Exp.App {op= App {op= Add; arg= a}; arg= Integer _} -> f init a + | Exp.App {op= App {op= Add _; arg= a}; arg= Integer _} -> f init a | a -> f init a let base_of = function - | Exp.App {op= App {op= Add; arg= a}; arg= Integer _} -> a + | Exp.App {op= App {op= Add _; arg= a}; arg= Integer _} -> a | a -> a (** solve a+i = b for a, yielding a = b-i *) let solve_for_base ai b = match ai with - | Exp.App {op= App {op= Add; arg= a}; arg= Integer {typ} as i} -> - (a, Exp.sub typ b i) + | Exp.App {op= App {op= Add {typ}; arg= a}; arg= i} -> (a, Exp.sub typ b i) | _ -> (ai, b) (** [norm r a+i] = [a'+k] where [r] implies [a+i=a'+k] and [a'] is a rep *) @@ -430,7 +429,7 @@ let difference r a b = (* a - b = (c+i) - (d+j) *) ( match solve_for_base dj ci with (* d = (c+i)-j = c+(i-j) & c = d *) - | d, App {op= App {op= Add; arg= c}; arg= Integer {data= i_j}} + | d, App {op= App {op= Add _; arg= c}; arg= Integer {data= i_j}} when Exp.equal d c -> (* a - b = (c+i) - (d+j) = i-j *) Some i_j diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 0f0f7fa38..4d8df9839 100644 --- a/sledge/src/symbheap/sh.ml +++ b/sledge/src/symbheap/sh.ml @@ -67,7 +67,7 @@ let rec pp_ vs fs {us; xs; cong; pure; heap; djns} = (List.map ~f:(map_seg ~f:(Congruence.normalize cong)) heap) ~compare:(fun s1 s2 -> let b_o = function - | Exp.App {op= App {op= Add; arg}; arg= Integer {data; _}} -> + | Exp.App {op= App {op= Add _; arg}; arg= Integer {data; _}} -> (arg, data) | e -> (e, Z.zero) in