[sledge] Add typ of integer constants

Summary:
Types of integer constants, in particular their bit-width, are
necessary for:

- correctly interpreting bitwise operations (e.g. `-1 xor 1` at type
  `i1` is `0` while without the type the result is `-2`), and;

- distinguishing between integers and booleans, which are one-bit
  integers, since booleans admit stronger algebraic simplification.

Note that code does genuinely treat 1-bit integers interchangeably as
booleans and integers, e.g. with expressions such as `e + (b != 42)`.
Therefore a lighter-weight early syntactic distinction between boolean
and bitwise operations is nontrivial/impossible to make robust.

This patch:

- adds the type to the representation of Exp.Integer;

- adds checks that Integer values fit within their specified bit-width

- factors out code handling 1-bit integers as booleans into `Z`, as it
  is easy to make mistakes when forgetting that `-1`, not `1`, is the
  representation of `true`;

- corrects the treatment of Exp.Convert in some cases involving
  treating negative integers as unsigned;

- corrects and strengthens Exp simplification based on the bit-width
  information;

- removes the `e - e ==> 0` simplification, due to not having the type
  for `0`.

Reviewed By: mbouaziz

Differential Revision: D10488407

fbshipit-source-id: ff4320a29

sledge/TODO.org

@@ -16,12 +16,14 @@ rather than nearest enclosing
 ** revise spec of strlen to account for non-max length strings
 ** convert strlen inst into a primitive to return the end of the block containing a pointer, and model strlen in code
 * llair
-** ? conflate null and 0
 ** NEXT normalize arithmetic exps to polynomials
 and sort terms
+** when Sub exps have types, simplify e - e to 0
+** when Xor exps have types, simplify e xor e to 0
+** ? remove src typ from Convert
 ** ? distribute addition over multiplication
 for e.g. ((%12 + 1) * 8) to ((%12 * 8) + 8)
-** simplify to NNF where (_ ^ -1) is (not _)
+** ? conflate null and 0
 ** add config to pp e.g. Exp.t as sexps
 ** add check for variable non-occurrence to Exp.rename
 ** define version of map that transforms args of Struct_rec
@@ -31,17 +33,12 @@ for e.g. ((%12 + 1) * 8) to ((%12 * 8) + 8)
       let args' = Vector.map_preserving_phys_equal args ~f in
       if op' == op && args' == args then e
       else AppN {op= op'; args= args'; loc}
-** simplify conv exps
-with dst of int 1 type by testing least significant bit of Integer
-constants
 ** define Label module for Exp.Label and Llair.label
 - to unify how functions and blocks are named
 - the Exp.label construction in Control.exec_term Iswitch is unwieldy
 ** check/ensure that generated names do not clash
 - name ^ ".ti" xlate_instr LandingPad
 ** check that Loc.pp follows GNU conventions
-** do not ignore types and signedness of operations
-interpretation of expressions is currently wrong
 ** ? change Var.freshen to choose the first available
 analogous to the following version that is over just ints
 #+BEGIN_SRC ocaml

sledge/src/llair/exp.ml

@@ -7,6 +7,58 @@
 
 (** Expressions *)
 
+(** Z wrapped to treat bounded and unsigned operations *)
+module Z = struct
+  type t = Z.t [@@deriving compare, hash, sexp]
+
+  let equal = Z.equal
+  let pp = Z.pp_print
+  let zero = Z.zero
+  let one = Z.one
+  let to_int = Z.to_int
+  let numbits = Z.numbits
+  let fits_int = Z.fits_int
+
+  (* the signed 1-bit integers are -1 and 0 *)
+  let true_ = Z.minus_one
+  let false_ = Z.zero
+  let of_bool = function true -> true_ | false -> false_
+  let is_true = Z.equal true_
+  let is_false = Z.equal false_
+
+  (** Interpret as a bounded integer with specified signedness and width. *)
+  let clamp ~signed bits z =
+    if signed then Z.signed_extract z 0 bits else Z.extract z 0 bits
+
+  let clamp_binop ~signed bits op x y =
+    op (clamp ~signed bits x) (clamp ~signed bits y)
+
+  let leq ~bits x y = clamp_binop ~signed:true bits Z.leq x y
+  let geq ~bits x y = clamp_binop ~signed:true bits Z.geq x y
+  let lt ~bits x y = clamp_binop ~signed:true bits Z.lt x y
+  let gt ~bits x y = clamp_binop ~signed:true bits Z.gt x y
+  let uleq ~bits x y = clamp_binop ~signed:false bits Z.leq x y
+  let ugeq ~bits x y = clamp_binop ~signed:false bits Z.geq x y
+  let ult ~bits x y = clamp_binop ~signed:false bits Z.lt x y
+  let ugt ~bits x y = clamp_binop ~signed:false bits Z.gt x y
+  let neg ~bits z = Z.neg (clamp bits ~signed:true z)
+  let add ~bits x y = clamp_binop ~signed:true bits Z.add x y
+  let sub ~bits x y = clamp_binop ~signed:true bits Z.sub x y
+  let mul ~bits x y = clamp_binop ~signed:true bits Z.mul x y
+  let div ~bits x y = clamp_binop ~signed:true bits Z.div x y
+  let rem ~bits x y = clamp_binop ~signed:true bits Z.rem x y
+  let udiv ~bits x y = clamp_binop ~signed:false bits Z.div x y
+  let urem ~bits x y = clamp_binop ~signed:false bits Z.rem x y
+  let logand ~bits x y = clamp_binop ~signed:true bits Z.logand x y
+  let logor ~bits x y = clamp_binop ~signed:true bits Z.logor x y
+  let logxor ~bits x y = clamp_binop ~signed:true bits Z.logxor x y
+  let shift_left ~bits z i = Z.shift_left (clamp bits ~signed:true z) i
+  let shift_right ~bits z i = Z.shift_right (clamp bits ~signed:true z) i
+
+  let shift_right_trunc ~bits z i =
+    Z.shift_right_trunc (clamp bits ~signed:true z) i
+end
+
 module T0 = struct
   type t =
     | Var of {id: int; name: string}
@@ -19,7 +71,7 @@ module T0 = struct
     | Memory
     | Concat
     (* numeric constants *)
-    | Integer of {data: Z.t}
+    | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string}
     (* binary: comparison *)
     | Eq
@@ -110,7 +162,7 @@ module T = struct
       | App {op= App {op= Memory; arg= siz}; arg= bytes} ->
           pf "@<1>⟨%a,%a@<1>⟩" pp siz pp bytes
       | Concat -> pf "^"
-      | Integer {data} -> pf "%a" Z.pp_print data
+      | Integer {data} -> pf "%a" Z.pp data
       | Float {data} -> pf "%s" data
       | Eq -> pf "="
       | Dq -> pf "!="
@@ -134,11 +186,15 @@ module T = struct
       | And -> pf "&&"
       | Or -> pf "||"
       | Xor -> pf "xor"
-      | App {op= App {op= Xor; arg}; arg= Integer {data}}
-        when Z.equal Z.minus_one data ->
+      | App
+          { op= App {op= Xor; arg}
+          ; arg= Integer {data; typ= Integer {bits= 1}} }
+        when Z.is_true data ->
           pf "¬%a" pp arg
-      | App {op= App {op= Xor; arg= Integer {data}}; arg}
-        when Z.equal Z.minus_one data ->
+      | App
+          { op= App {op= Xor; arg= Integer {data; typ= Integer {bits= 1}}}
+          ; arg }
+        when Z.is_true data ->
           pf "¬%a" pp arg
       | Shl -> pf "shl"
       | Lshr -> pf "lshr"
@@ -198,15 +254,24 @@ let invariant ?(partial = false) e =
     assert (nargs = arity || (partial && nargs < arity))
   in
   match op with
+  | Integer {data; typ= Integer {bits}} ->
+      assert_arity 0 ;
+      assert (Z.numbits data <= bits)
   | Var _ | Nondet _ | Label _ | Null | Integer _ | Float _ ->
       assert_arity 0
   | Convert {dst; src} ->
-      assert (Typ.convertible src dst) ;
-      assert_arity 1
-  | Splat | Memory | Concat | Eq | Dq | Gt | Ge | Lt | Le | Ugt | Uge
-   |Ult | Ule | Ord | Uno | Add | Sub | Mul | Div | Udiv | Rem | Urem
-   |And | Or | Xor | Shl | Lshr | Ashr | Select ->
-      assert_arity 2
+      ( match args with
+      | [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 | Sub | Mul
+   |Div | Udiv | Rem | Urem | And | Or | Xor | Shl | Lshr | Ashr -> (
+    match args with
+    | [Integer {typ= Integer {bits= m}}; Integer {typ= Integer {bits= n}}]
+      ->
+        assert (m = n)
+    | _ -> assert_arity 2 )
+  | Splat | Memory | Concat | Ord | Uno | Select -> assert_arity 2
   | Conditional | Update -> assert_arity 3
   | Record -> assert (partial || not (List.is_empty args))
   | Struct_rec {elts} ->
@@ -372,165 +437,366 @@ let var x = x
 let nondet msg = Nondet {msg} |> check invariant
 let label ~parent ~name = Label {parent; name} |> check invariant
 let null = Null |> check invariant
-let integer data = Integer {data} |> check invariant
-let bool b = integer (Z.of_int (Bool.to_int b))
+let integer data typ = Integer {data; typ} |> check invariant
+let bool b = integer (Z.of_bool b) Typ.bool
 let float data = Float {data} |> check invariant
 
-let simp_convert signed (dst : Typ.t) (src : Typ.t) arg =
-  match (signed, dst, src, arg) with
-  | _, Integer {bits}, _, Integer {data} when Z.numbits data <= bits ->
-      integer data
-  | false, Integer {bits= m}, Integer {bits= n}, _ when m >= n -> arg
+let simp_convert signed (dst : Typ.t) src arg =
+  match (dst, arg) with
+  | Integer {bits= m}, Integer {data; typ= Integer {bits= n}} ->
+      integer (Z.clamp ~signed (min m n) data) dst
   | _ -> App {op= Convert {signed; dst; src}; arg}
 
-let rec simp_eq x y =
-  match (x, y) with
-  (* i = j ==> i=j *)
-  | Integer {data= i}, Integer {data= j} -> bool (Z.equal i j)
-  (* e+i = j ==> e = j-i *)
-  | ( App {op= App {op= Add; arg= e}; arg= Integer {data= i}}
-    , Integer {data= j} ) ->
-      simp_eq e (integer (Z.sub j i))
-  (* e = e ==> 1 *)
-  | _ when equal x y -> bool true
-  | _ -> App {op= App {op= Eq; arg= x}; arg= y}
-
-let simp_dq x y =
-  match (x, y) with
-  (* i != j ==> i!=j *)
-  | Integer {data= i}, Integer {data= j} -> bool (not (Z.equal i j))
-  (* e = e ==> 0 *)
-  | _ when equal x y -> bool false
-  | _ -> App {op= App {op= Dq; arg= x}; arg= y}
-
 let simp_gt x y =
   match (x, y) with
-  (* i > j ==> i>j *)
-  | Integer {data= i}, Integer {data= j} -> bool (Z.gt i j)
+  | Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
+      bool (Z.gt ~bits 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.ugt ~bits i j)
+  | _ -> App {op= App {op= Ugt; arg= x}; arg= y}
+
 let simp_ge x y =
   match (x, y) with
-  (* i >= j ==> i>=j *)
-  | Integer {data= i}, Integer {data= j} -> bool (Z.geq i j)
+  | Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
+      bool (Z.geq ~bits 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.ugeq ~bits i j)
+  | _ -> App {op= App {op= Uge; arg= x}; arg= y}
+
 let simp_lt x y =
   match (x, y) with
-  (* i < j ==> i<j *)
-  | Integer {data= i}, Integer {data= j} -> bool (Z.lt i j)
+  | Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
+      bool (Z.lt ~bits 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.ult ~bits i j)
+  | _ -> App {op= App {op= Ult; arg= x}; arg= y}
+
 let simp_le x y =
   match (x, y) with
-  (* i <= j ==> i<=j *)
-  | Integer {data= i}, Integer {data= j} -> bool (Z.leq i j)
+  | Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
+      bool (Z.leq ~bits 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.uleq ~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}
+
+let simp_cond cnd thn els =
+  match cnd with
+  (* ¬(true ? t : e) ==> t *)
+  | Integer {data; typ= Integer {bits= 1}} when Z.is_true data -> thn
+  (* ¬(false ? t : e) ==> e *)
+  | Integer {data; typ= Integer {bits= 1}} when Z.is_false data -> els
+  | _ ->
+      App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els}
+
+let rec simp_not (typ : Typ.t) exp =
+  match (exp, typ) with
+  (* ¬(x = y) ==> x != y *)
+  | App {op= App {op= Eq; arg= x}; arg= y}, _ -> simp_dq x y
+  (* ¬(x != y) ==> x = y *)
+  | App {op= App {op= Dq; arg= x}; arg= y}, _ -> simp_eq x y
+  (* ¬(x > y) ==> x <= y *)
+  | App {op= App {op= Gt; arg= x}; arg= y}, _ -> simp_le x y
+  (* ¬(x >= y) ==> x < y *)
+  | App {op= App {op= Ge; arg= x}; arg= y}, _ -> simp_lt x y
+  (* ¬(x < y) ==> x >= y *)
+  | 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 *)
+  | App {op= App {op= Uno; arg= x}; arg= y}, _ -> simp_ord x y
+  (* ¬(a ∧ b) ==> ¬a ∨ ¬b *)
+  | App {op= App {op= And; arg= x}; arg= y}, Integer {bits= 1} ->
+      simp_or (simp_not typ x) (simp_not typ y)
+  (* ¬(a ∨ b) ==> ¬a ∧ ¬b *)
+  | App {op= App {op= Or; arg= x}; arg= y}, Integer {bits= 1} ->
+      simp_and (simp_not typ x) (simp_not typ y)
+  (* ¬(c ? t : e) ==> c ? ¬t : ¬e *)
+  | ( App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els}
+    , Integer {bits= 1} ) ->
+      simp_cond cnd (simp_not typ thn) (simp_not typ els)
+  (* ¬b ==> false = b *)
+  | b, Integer {bits= 1} -> App {op= App {op= Eq; arg= bool false}; arg= b}
+  (* ¬e ==> true xor e *)
+  | e, _ ->
+      App {op= App {op= Xor; arg= integer (Z.of_bool true) typ}; arg= e}
+
+and simp_eq x y =
+  match (x, y) with
+  (* i = j *)
+  | Integer {data= i}, Integer {data= j} -> bool (Z.equal i j)
+  (* e+i = j ==> e = j-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 *)
+  | b, Integer {data; typ= Integer {bits= 1}}
+   |Integer {data; typ= Integer {bits= 1}}, b
+    when Z.is_false data ->
+      simp_not Typ.bool b
+  (* b = true ==> b *)
+  | b, Integer {data; typ= Integer {bits= 1}}
+   |Integer {data; typ= Integer {bits= 1}}, b
+    when Z.is_true data ->
+      b
+  | _ ->
+      let c = compare x y in
+      (* e = e ==> true *)
+      if c = 0 then bool true
+      else if c < 0 then App {op= App {op= Eq; arg= y}; arg= x}
+      else App {op= App {op= Eq; arg= x}; arg= y}
+
+and simp_dq x y =
+  match (x, y) with
+  (* i != j *)
+  | Integer {data= i}, Integer {data= j} -> bool (not (Z.equal i j))
+  (* e+i != j ==> e != j-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 *)
+  | b, Integer {data; typ= Integer {bits= 1}}
+   |Integer {data; typ= Integer {bits= 1}}, b
+    when Z.is_false data ->
+      b
+  (* b != true ==> ¬b *)
+  | b, Integer {data; typ= Integer {bits= 1}}
+   |Integer {data; typ= Integer {bits= 1}}, b
+    when Z.is_true data ->
+      simp_not Typ.bool b
+  | _ ->
+      let c = compare x y in
+      (* e = e ==> false *)
+      if c = 0 then bool false
+      else if c < 0 then App {op= App {op= Dq; arg= x}; arg= y}
+      else App {op= App {op= Dq; arg= y}; arg= x}
+
+and simp_and x y =
+  match (x, y) with
+  (* i && j *)
+  | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} ->
+      integer (Z.logand ~bits i j) typ
+  (* e && true ==> e *)
+  | Integer {data; typ= Integer {bits= 1}}, e
+   |e, Integer {data; typ= Integer {bits= 1}}
+    when Z.is_true data ->
+      e
+  (* e && false ==> 0 *)
+  | (Integer {data; typ= Integer {bits= 1}} as f), _
+   |_, (Integer {data; typ= Integer {bits= 1}} as f)
+    when Z.is_false data ->
+      f
+  | _ ->
+      let c = compare x y in
+      (* e && e ==> e *)
+      if c = 0 then x
+      else if c < 0 then App {op= App {op= And; arg= x}; arg= y}
+      else App {op= App {op= And; arg= y}; arg= x}
+
+and simp_or x y =
+  match (x, y) with
+  (* i || j *)
+  | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} ->
+      integer (Z.logor ~bits i j) typ
+  (* e || true ==> true *)
+  | (Integer {data; typ= Integer {bits= 1}} as t), _
+   |_, (Integer {data; typ= Integer {bits= 1}} as t)
+    when Z.is_true data ->
+      t
+  (* e || false ==> e *)
+  | Integer {data; typ= Integer {bits= 1}}, e
+   |e, Integer {data; typ= Integer {bits= 1}}
+    when Z.is_false data ->
+      e
+  | _ ->
+      let c = compare x y in
+      (* e || e ==> e *)
+      if c = 0 then x
+      else if c < 0 then App {op= App {op= Or; arg= x}; arg= y}
+      else App {op= App {op= Or; arg= y}; arg= x}
+
+let simp_xor x y =
+  match (x, y) with
+  (* i xor j *)
+  | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} ->
+      integer (Z.logxor ~bits i j) typ
+  (* true xor b ==> ¬b *)
+  | Integer {data; typ= Integer {bits= 1}}, b
+   |b, Integer {data; typ= Integer {bits= 1}}
+    when Z.is_true data ->
+      simp_not Typ.bool b
+  | _ ->
+      let c = compare x y in
+      if c <= 0 then App {op= App {op= Xor; arg= x}; arg= y}
+      else App {op= App {op= Xor; arg= y}; arg= x}
+
+let simp_shl x y =
+  match (x, y) with
+  (* i shl j *)
+  | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}}
+    when Z.fits_int j ->
+      integer (Z.shift_left ~bits i (Z.to_int j)) typ
+  (* e shl 0 ==> e *)
+  | e, Integer {data} when Z.equal Z.zero data -> e
+  | _ -> App {op= App {op= Shl; arg= x}; arg= y}
+
+let simp_lshr x y =
+  match (x, y) with
+  (* i lshr j *)
+  | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}}
+    when Z.fits_int j ->
+      integer (Z.shift_right_trunc ~bits i (Z.to_int j)) typ
+  (* e lshr 0 ==> e *)
+  | e, Integer {data} when Z.equal Z.zero data -> e
+  | _ -> App {op= App {op= Lshr; arg= x}; arg= y}
+
+let simp_ashr x y =
+  match (x, y) with
+  (* i ashr j *)
+  | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}}
+    when Z.fits_int j ->
+      integer (Z.shift_right ~bits i (Z.to_int j)) typ
+  (* e ashr 0 ==> e *)
+  | 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 =
   match (x, y) with
-  (* i + j ==> i+j *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.add i j)
+  (* 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
   (* e + 0 ==> e *)
-  | _, Integer {data} when Z.equal Z.zero data -> x
+  | e, Integer {data} when Z.equal Z.zero data -> e
   (* (e+i) + j ==> e+(i+j) *)
-  | App {op= App {op= Add; arg}; arg= Integer {data= i}}, Integer {data= j}
-    ->
-      simp_add arg (integer (Z.add i j))
+  | ( App
+        { 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)
   (* (i-e) + j ==> (i+j)-e *)
-  | App {op= App {op= Sub; arg= Integer {data= i}}; arg}, Integer {data= j}
-    ->
-      simp_sub (integer (Z.add i j)) arg
+  | ( App
+        { op=
+            App {op= Sub; arg= Integer {data= i; typ= Integer {bits} as typ}}
+        ; arg }
+    , Integer {data= j} ) ->
+      simp_sub (integer (Z.add ~bits i j) typ) arg
   | _ -> App {op= App {op= Add; arg= x}; arg= y}
 
 and simp_sub x y =
   match (x, y) with
-  (* i - j ==> i-j *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.sub i j)
+  (* i - j *)
+  | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} ->
+      integer (Z.sub ~bits i j) typ
   (* e - i ==> e + (-i) *)
-  | _, Integer {data} -> simp_add x (integer (Z.neg data))
-  (* e - e ==> 0 *)
-  | _ when equal x y -> integer Z.zero
+  | _, Integer {data; typ= Integer {bits} as typ} ->
+      simp_add x (integer (Z.neg ~bits data) typ)
   | _ -> App {op= App {op= Sub; arg= x}; arg= y}
 
 let simp_mul x y =
   match (x, y) with
-  (* i * j ==> i*j *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.mul i j)
+  (* i * j *)
+  | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} ->
+      integer (Z.mul ~bits i j) typ
   (* e * 1 ==> e *)
-  | (Integer {data}, e | e, Integer {data}) when Z.equal Z.one data -> 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}
 
 let simp_div x y =
   match (x, y) with
-  (* i / j ==> i/j *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.div i j)
+  (* i / j *)
+  | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} ->
+      integer (Z.div ~bits i j) typ
+  (* e / 1 ==> e *)
+  | Integer {data}, e when Z.equal Z.one data -> e
   | _ -> App {op= App {op= Div; arg= x}; arg= y}
 
-let simp_rem x y =
-  match (x, y) with
-  (* i % j ==> i%j *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.( mod ) i j)
-  | _ -> App {op= App {op= Rem; arg= x}; arg= y}
-
-let simp_and x y =
+let simp_udiv x y =
   match (x, y) with
-  (* i && j ==> i logand j *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.logand i j)
-  (* e && 1 ==> e *)
-  | (Integer {data}, e | e, Integer {data}) when Z.equal Z.one data -> e
-  (* e && 0 ==> 0 *)
-  | ((Integer {data} as z), _ | _, (Integer {data} as z))
-    when Z.equal Z.zero data ->
-      z
-  | _ -> App {op= App {op= And; arg= x}; arg= y}
+  (* i u/ j *)
+  | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j} ->
+      integer (Z.udiv ~bits i j) typ
+  (* e u/ 1 ==> e *)
+  | Integer {data}, e when Z.equal Z.one data -> e
+  | _ -> App {op= App {op= Udiv; arg= x}; arg= y}
 
-let simp_or x y =
+let simp_rem x y =
   match (x, y) with
-  (* i || j ==> i logor j *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.logor i j)
-  (* e || 1 ==> e *)
-  | (Integer {data}, _ | _, Integer {data}) when Z.equal Z.one data ->
-      integer Z.one
-  (* e || 0 ==> e *)
-  | (Integer {data}, e | e, Integer {data}) when Z.equal Z.zero data -> e
-  | _ -> App {op= App {op= Or; arg= x}; arg= y}
+  (* i % j *)
+  | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} ->
+      integer (Z.rem ~bits i j) typ
+  (* e % 1 ==> 0 *)
+  | _, Integer {data; typ} when Z.equal Z.one data -> integer Z.zero typ
+  | _ -> App {op= App {op= Rem; arg= x}; arg= y}
 
-let simp_xor x y =
+let simp_urem x y =
   match (x, y) with
-  (* i xor j ==> i logxor j *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.logxor i j)
-  (* ¬(x=y) ==> x!=y *)
-  | App {op= App {op= Eq; arg= x}; arg= y}, Integer {data}
-   |Integer {data}, App {op= App {op= Eq; arg= x}; arg= y}
-    when Z.equal Z.minus_one data ->
-      simp_dq x y
-  (* ¬(x!=y) ==> x=y *)
-  | App {op= App {op= Dq; arg= x}; arg= y}, Integer {data}
-   |Integer {data}, App {op= App {op= Dq; arg= x}; arg= y}
-    when Z.equal Z.minus_one data ->
-      simp_eq x y
-  | _ -> App {op= App {op= Xor; arg= x}; arg= y}
+  (* i u% j *)
+  | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j} ->
+      integer (Z.urem ~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}
 
 let app1 ?(partial = false) op arg =
   ( match (op, arg) with
-  | Convert {signed; dst; src}, x -> simp_convert signed dst src x
   | App {op= Eq; arg= x}, y -> simp_eq x y
   | App {op= Dq; arg= x}, y -> simp_dq x y
   | App {op= Gt; arg= x}, y -> simp_gt x y
   | 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= Add; arg= x}, y -> simp_add x y
   | App {op= Sub; arg= x}, y -> simp_sub x y
   | App {op= Mul; arg= x}, y -> simp_mul 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
+  | App {op= Shl; arg= x}, y -> simp_shl x y
+  | App {op= Lshr; arg= x}, y -> simp_lshr x y
+  | App {op= Ashr; arg= x}, y -> simp_ashr x y
+  | App {op= App {op= Conditional; arg= x}; arg= y}, z -> simp_cond x y z
+  | Convert {signed; dst; src}, x -> simp_convert signed dst src x
   | _ -> App {op; arg} )
   |> check (invariant ~partial)
 
@@ -562,6 +828,7 @@ let urem = app2 Urem
 let and_ = app2 And
 let or_ = app2 Or
 let xor = app2 Xor
+let not_ = simp_not
 let shl = app2 Shl
 let lshr = app2 Lshr
 let ashr = app2 Ashr
@@ -634,8 +901,13 @@ let rename e sub =
 
 (** Query *)
 
-let is_true = function Integer {data} -> Z.equal Z.one data | _ -> false
-let is_false = function Integer {data} -> Z.equal Z.zero data | _ -> false
+let is_true = function
+  | Integer {data; typ= Integer {bits= 1}} -> Z.is_true data
+  | _ -> false
+
+let is_false = function
+  | Integer {data; typ= Integer {bits= 1}} -> Z.is_false data
+  | _ -> false
 
 let rec is_constant = function
   | Var _ | Nondet _ -> false

sledge/src/llair/exp.mli

@@ -34,7 +34,7 @@ type t = private
   | Splat  (** Iterated concatenation of a single byte *)
   | Memory  (** Size-tagged byte-array *)
   | Concat  (** Byte-array concatenation *)
-  | Integer of {data: Z.t}  (** Integer constant *)
+  | Integer of {data: Z.t; typ: Typ.t}  (** Integer constant *)
   | Float of {data: string}  (** Floating-point constant *)
   | Eq  (** Equal test *)
   | Dq  (** Disequal test *)
@@ -55,12 +55,12 @@ type t = private
   | Udiv  (** Unsigned division *)
   | Rem  (** Remainder of division *)
   | Urem  (** Remainder of unsigned division *)
-  | And  (** Conjunction *)
-  | Or  (** Disjunction *)
-  | Xor  (** Exclusive-or / Boolean disequality *)
-  | Shl  (** Shift left *)
-  | Lshr  (** Logical shift right *)
-  | Ashr  (** Arithmetic shift right *)
+  | And  (** Conjunction, boolean or bitwise *)
+  | Or  (** Disjunction, boolean or bitwise *)
+  | Xor  (** Exclusive-or, bitwise *)
+  | Shl  (** Shift left, bitwise *)
+  | Lshr  (** Logical shift right, bitwise *)
+  | Ashr  (** Arithmetic shift right, bitwise *)
   | Conditional  (** If-then-else *)
   | Record  (** Record (array / struct) constant *)
   | Select  (** Select an index from a record *)
@@ -134,7 +134,7 @@ val splat : byt:t -> siz:t -> t
 val memory : siz:t -> arr:t -> t
 val concat : t -> t -> t
 val bool : bool -> t
-val integer : Z.t -> t
+val integer : Z.t -> Typ.t -> t
 val float : string -> t
 val eq : t -> t -> t
 val dq : t -> t -> t
@@ -158,6 +158,7 @@ val urem : t -> t -> t
 val and_ : t -> t -> t
 val or_ : t -> t -> t
 val xor : t -> t -> t
+val not_ : Typ.t -> t -> t
 val shl : t -> t -> t
 val lshr : t -> t -> t
 val ashr : t -> t -> t

sledge/src/llair/frontend.ml

@@ -274,15 +274,17 @@ let i32 x = xlate_type x (Llvm.i32_type x.llcontext)
 let suffix_after_last_space : string -> string =
  fun str -> String.drop_prefix str (String.rindex_exn str ' ' + 1)
 
-let xlate_int : Llvm.llvalue -> Exp.t =
- fun llv ->
+let xlate_int : x -> Llvm.llvalue -> Exp.t =
+ fun x llv ->
+  let llt = Llvm.type_of llv in
+  let typ = xlate_type x llt in
   let data =
     match Llvm.int64_of_const llv with
     | Some n -> Z.of_int64 n
     | None ->
         Z.of_string (suffix_after_last_space (Llvm.string_of_llvalue llv))
   in
-  Exp.integer data
+  Exp.integer data typ
 
 let xlate_float : Llvm.llvalue -> Exp.t =
  fun llv ->
@@ -314,11 +316,11 @@ let ptr_fld x ~ptr ~fld ~lltyp =
   let offset =
     Llvm_target.DataLayout.offset_of_element lltyp fld x.lldatalayout
   in
-  Exp.add ptr (Exp.integer (Z.of_int64 offset))
+  Exp.add ptr (Exp.integer (Z.of_int64 offset) Typ.siz)
 
 let ptr_idx x ~ptr ~idx ~llelt =
   let stride = Llvm_target.DataLayout.abi_size llelt x.lldatalayout in
-  Exp.add ptr (Exp.mul (Exp.integer (Z.of_int64 stride)) idx)
+  Exp.add ptr (Exp.mul (Exp.integer (Z.of_int64 stride) Typ.siz) idx)
 
 let xlate_llvm_eh_typeid_for : x -> Typ.t -> Exp.t -> Exp.t =
  fun x typ arg -> Exp.convert ~dst:(i32 x) ~src:typ arg
@@ -351,7 +353,7 @@ and xlate_value : x -> Llvm.llvalue -> Exp.t =
         Exp.var (xlate_name llv)
     | Function | GlobalVariable -> Exp.var (xlate_global x llv).var
     | GlobalAlias -> xlate_value x (Llvm.operand llv 0)
-    | ConstantInt -> xlate_int llv
+    | ConstantInt -> xlate_int x llv
     | ConstantFP -> xlate_float llv
     | ConstantPointerNull | ConstantAggregateZero -> Exp.null
     | ConstantVector | ConstantArray ->
@@ -498,10 +500,10 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
         let rcd_i, upd =
           match typ with
           | Tuple _ | Struct _ ->
-              let idx = Exp.integer (Z.of_int indices.(i)) in
+              let idx = Exp.integer (Z.of_int indices.(i)) Typ.siz in
               (Exp.select ~rcd ~idx, Exp.update ~rcd ~idx)
           | Array _ ->
-              let idx = Exp.integer (Z.of_int indices.(i)) in
+              let idx = Exp.integer (Z.of_int indices.(i)) Typ.siz in
               (Exp.select ~rcd ~idx, Exp.update ~rcd ~idx)
           | _ -> fail "xlate_value: %a" pp_llvalue llv ()
         in
@@ -639,9 +641,10 @@ let pop_stack_frame_of_function :
 
 (** construct the types involved in landingpads: i32, std::type_info*, and
     __cxa_exception *)
-let landingpad_typs : x -> Llvm.llvalue -> Typ.t * Llvm.lltype =
+let landingpad_typs : x -> Llvm.llvalue -> Typ.t * Typ.t * Llvm.lltype =
  fun x instr ->
   let llt = Llvm.type_of instr in
+  let i32 = i32 x in
   if
     not
       ( Poly.(Llvm.classify_type llt = Struct)
@@ -662,7 +665,7 @@ let landingpad_typs : x -> Llvm.llvalue -> Typ.t * Llvm.lltype =
   let void = Llvm.void_type llcontext in
   let dtor = Llvm.(pointer_type (function_type void [|llpi8|])) in
   let cxa_exception = Llvm.struct_type llcontext [|tip; dtor|] in
-  (xlate_type x tip, cxa_exception)
+  (i32, xlate_type x tip, cxa_exception)
 
 (** construct the argument of a landingpad block, mainly fix the encoding
     scheme for landingpad instruction name to block arg name *)
@@ -869,23 +872,29 @@ let xlate_instr :
   match opcode with
   | Load ->
       let reg = xlate_name instr in
-      let len = Exp.integer (Z.of_int (size_of x (Llvm.type_of instr))) in
+      let len =
+        Exp.integer (Z.of_int (size_of x (Llvm.type_of instr))) Typ.siz
+      in
       let ptr = xlate_value x (Llvm.operand instr 0) in
       continue (fun (insts, term) ->
           (Llair.Inst.load ~reg ~ptr ~len ~loc :: insts, term, []) )
   | Store ->
       let exp = xlate_value x (Llvm.operand instr 0) in
       let llt = Llvm.type_of (Llvm.operand instr 0) in
-      let len = Exp.integer (Z.of_int (size_of x llt)) in
+      let len = Exp.integer (Z.of_int (size_of x llt)) Typ.siz in
       let ptr = xlate_value x (Llvm.operand instr 1) in
       continue (fun (insts, term) ->
           (Llair.Inst.store ~ptr ~exp ~len ~loc :: insts, term, []) )
   | Alloca ->
       let reg = xlate_name instr in
       let rand = Llvm.operand instr 0 in
-      let num = xlate_value x rand in
+      let num =
+        Exp.convert ~dst:Typ.siz
+          ~src:(xlate_type x (Llvm.type_of rand))
+          (xlate_value x rand)
+      in
       let llt = Llvm.element_type (Llvm.type_of instr) in
-      let len = Exp.integer (Z.of_int (size_of x llt)) in
+      let len = Exp.integer (Z.of_int (size_of x llt)) Typ.siz in
       continue (fun (insts, term) ->
           (Llair.Inst.alloc ~reg ~num ~len ~loc :: insts, term, []) )
   | Call -> (
@@ -956,7 +965,7 @@ let xlate_instr :
       | ["_Znwm"] ->
           let num = xlate_value x (Llvm.operand instr 0) in
           let llt = Llvm.type_of instr in
-          let len = Exp.integer (Z.of_int (size_of x llt)) in
+          let len = Exp.integer (Z.of_int (size_of x llt)) Typ.siz in
           continue (fun (insts, term) ->
               ( Llair.Inst.alloc ~reg:(Option.value_exn reg) ~num ~len ~loc
                 :: insts
@@ -1020,7 +1029,7 @@ let xlate_instr :
           let reg = xlate_name_opt x instr in
           let num = xlate_value x (Llvm.operand instr 0) in
           let llt = Llvm.type_of instr in
-          let len = Exp.integer (Z.of_int (size_of x llt)) in
+          let len = Exp.integer (Z.of_int (size_of x llt)) Typ.siz in
           let blk = Llvm.get_normal_dest instr in
           let args = jump_args x instr blk in
           let dst = Llair.Jump.mk (label_of_block blk) args in
@@ -1135,7 +1144,7 @@ let xlate_instr :
          eventually jumping to the handler code following the landingpad,
          passing a value for the selector which the handler code tests to
          e.g. either cleanup or rethrow. *)
-      let tip, cxa_exception = landingpad_typs x instr in
+      let i32, tip, cxa_exception = landingpad_typs x instr in
       let exc = Exp.var (landingpad_arg instr) in
       let ti = Var.program (name ^ ".ti") in
       (* std::type_info* ti = ((__cxa_exception* )exc - 1)->exceptionType *)
@@ -1144,13 +1153,13 @@ let xlate_instr :
         (* field number of the exceptionType member of __cxa_exception *)
         let fld = 0 in
         (* index from exc that points to header *)
-        let idx = Exp.integer Z.minus_one in
+        let idx = Exp.integer Z.minus_one Typ.siz in
         let ptr =
           ptr_fld x
             ~ptr:(ptr_idx x ~ptr:exc ~idx ~llelt:typ)
             ~fld ~lltyp:typ
         in
-        let len = Exp.integer (Z.of_int (size_of x typ)) in
+        let len = Exp.integer (Z.of_int (size_of x typ)) Typ.siz in
         Llair.Inst.load ~reg:ti ~ptr ~len ~loc
       in
       let ti = Exp.var ti in
@@ -1168,7 +1177,8 @@ let xlate_instr :
         Llair.Term.goto ~dst ~loc
       in
       let term_unwind, rev_blocks =
-        if Llvm.is_cleanup instr then (goto_unwind (Exp.integer Z.zero), [])
+        if Llvm.is_cleanup instr then
+          (goto_unwind (Exp.integer Z.zero i32), [])
         else
           let num_clauses = Llvm.num_operands instr in
           let lbl i = name ^ "." ^ Int.to_string i in
@@ -1177,7 +1187,7 @@ let xlate_instr :
             Llair.Block.mk ~lbl:(lbl i) ~params:[] ~cmnd:Vector.empty ~term
           in
           let match_filter =
-            jump_unwind (Exp.sub (Exp.integer Z.zero) typeid)
+            jump_unwind (Exp.sub (Exp.integer Z.zero i32) typeid)
           in
           let xlate_clause i =
             let clause = Llvm.operand instr i in
@@ -1221,7 +1231,7 @@ let xlate_instr :
                   ~term ] ) )
   | Resume ->
       let rcd = xlate_value x (Llvm.operand instr 0) in
-      let exc = Exp.select ~rcd ~idx:(Exp.integer Z.zero) in
+      let exc = Exp.select ~rcd ~idx:(Exp.integer Z.zero Typ.siz) in
       terminal (pop loc) (Llair.Term.throw ~exc ~loc) []
   | Unreachable -> terminal [] Llair.Term.unreachable []
   | Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc

sledge/src/llair/typ.ml

@@ -100,6 +100,11 @@ let struct_ =
         Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elts.(i) <- elt) ;
         typ |> check invariant
 
+(** Constants *)
+
+let bool = integer ~bits:1
+let siz = integer ~bits:64
+
 (** Queries *)
 
 let rec prim_bit_size_of = function

sledge/src/llair/typ.mli

@@ -34,6 +34,8 @@ include Invariant.S with type t := t
 
 (** Constructors *)
 
+val bool : t
+val siz : t
 val function_ : return:t option -> args:t vector -> t
 val integer : bits:int -> t
 val float : bits:int -> enc:[`Extended | `IEEE | `Pair] -> t

sledge/src/symbheap/congruence.ml

@@ -446,7 +446,7 @@ let difference r a b =
 let%test_module _ =
   ( module struct
     let printf pp = Format.printf "@.%a@." pp
-    let ( ! ) i = Exp.integer (Z.of_int i)
+    let ( ! ) i = Exp.integer (Z.of_int i) Typ.siz
 
     let%expect_test _ =
       printf pp {true_ with pnd= [(!0, !1)]} ;

sledge/src/symbheap/congruence_test.ml

@@ -14,7 +14,7 @@ let%test_module _ =
     let mem_eq x y r = entails r (and_eq true_ x y)
     let i8 = Typ.integer ~bits:8
     let i64 = Typ.integer ~bits:64
-    let ( ! ) i = Exp.integer (Z.of_int i)
+    let ( ! ) i = Exp.integer (Z.of_int i) Typ.siz
     let ( + ) = Exp.add
     let ( - ) = Exp.sub
     let f = Exp.convert ~dst:i64 ~src:i8

sledge/src/symbheap/domain.ml

@@ -15,7 +15,7 @@ let init globals =
   Vector.fold globals ~init:Sh.emp ~f:(fun q -> function
     | {Global.var; init= Some arr; siz} ->
         let loc = Exp.var var in
-        let len = Exp.integer (Z.of_int siz) in
+        let len = Exp.integer (Z.of_int siz) Typ.siz in
         Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr})
     | _ -> q )
 

sledge/src/symbheap/exec.ml

@@ -108,7 +108,7 @@ let memcpy_eq_spec us dst src len =
   let dst_heap = Sh.seg seg in
   let foot =
     Sh.and_ (Exp.eq dst src)
-      (Sh.and_ (Exp.eq len (Exp.integer Z.zero)) dst_heap)
+      (Sh.and_ (Exp.eq len (Exp.integer Z.zero Typ.siz)) dst_heap)
   in
   let post = dst_heap in
   {xs; foot; post}
@@ -249,7 +249,7 @@ let strlen_spec us reg ptr =
   let {xs; seg} = fresh_seg ~loc:ptr us in
   let foot = Sh.seg seg in
   let {Sh.loc= p; bas= b; len= m} = seg in
-  let ret = Exp.sub (Exp.add (Exp.sub b p) m) (Exp.integer Z.one) in
+  let ret = Exp.sub (Exp.add (Exp.sub b p) m) (Exp.integer Z.one Typ.siz) in
   let post = Sh.and_ (Exp.eq (Exp.var reg) ret) foot in
   {xs; foot; post}
 

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
@@ -117,7 +117,9 @@ let rec fv_union init q =
 let fv q = fv_union Var.Set.empty q
 
 let invariant_pure = function
-  | Exp.Integer {data} -> assert (not (Z.equal Z.zero data))
+  | Exp.Integer {data; typ} ->
+      assert (Typ.equal Typ.bool typ) ;
+      assert (not (Z.equal Z.zero data))
   | _ -> assert true
 
 let invariant_seg _ = ()
@@ -333,16 +335,15 @@ let rec pure (e : Exp.t) =
   ;
   let us = Exp.fv e in
   ( match e with
-  | Integer {data} -> if Z.equal Z.zero data then false_ us else emp
+  | Integer {data; typ= Integer {bits= 1}} ->
+      if Z.equal Z.zero data then false_ us else emp
   | App {op= App {op= And; arg= e1}; arg= e2} -> star (pure e1) (pure e2)
   | App {op= App {op= Or; arg= e1}; arg= e2} -> or_ (pure e1) (pure e2)
-  | App
-      { op= App {op= Eq; arg= App {op= App {op= Eq; arg= e1}; arg= e2}}
-      ; arg= Integer {data} }
-    when Z.equal Z.one data ->
-      let cong = Congruence.(and_eq true_ e1 e2) in
-      if Congruence.is_false cong then false_ us
-      else {emp with us; cong; pure= [e]}
+  | App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els}
+    ->
+      or_
+        (star (pure cnd) (pure thn))
+        (star (pure (Exp.not_ Typ.bool cnd)) (pure els))
   | App {op= App {op= Eq; arg= e1}; arg= e2} ->
       let cong = Congruence.(and_eq true_ e1 e2) in
       if Congruence.is_false cong then false_ us

sledge/src/symbheap/solver.ml

@@ -106,7 +106,7 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
       ssg pp goal] ;
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let o_n = Exp.integer o_n in
+  let o_n = Exp.integer o_n Typ.siz in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
   let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
   let com = Sh.star (Sh.seg {msg with siz= n; arr= a0}) com in
@@ -148,7 +148,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
       ssg pp goal] ;
   let {Sh.bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let n_o = Exp.integer n_o in
+  let n_o = Exp.integer n_o Typ.siz in
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
   let a1', xs, zs, _ = fresh_var "a1" xs zs ~wrt:(Set.union us xs) in
@@ -188,7 +188,7 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
       ssg pp goal] ;
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let l_k = Exp.integer l_k in
+  let l_k = Exp.integer l_k Typ.siz in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
   let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
   let com =
@@ -232,7 +232,7 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
       pp goal] ;
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let l_k = Exp.integer l_k and ko_ln = Exp.integer ko_ln in
+  let l_k = Exp.integer l_k Typ.siz and ko_ln = Exp.integer ko_ln Typ.siz in
   let ln = Exp.add l n in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
@@ -282,9 +282,9 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
       pp goal] ;
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let l_k = Exp.integer l_k in
-  let ko_l = Exp.integer ko_l in
-  let ln_ko = Exp.integer ln_ko in
+  let l_k = Exp.integer l_k Typ.siz in
+  let ko_l = Exp.integer ko_l Typ.siz in
+  let ln_ko = Exp.integer ln_ko Typ.siz in
   let ko = Exp.add k o in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
@@ -339,7 +339,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
       ssg pp goal] ;
   let {Sh.bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let k_l = Exp.integer k_l in
+  let k_l = Exp.integer k_l Typ.siz in
   let a0', xs, zs, _ = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
@@ -380,8 +380,8 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
       pp goal] ;
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let k_l = Exp.integer k_l in
-  let ln_ko = Exp.integer ln_ko in
+  let k_l = Exp.integer k_l Typ.siz in
+  let ln_ko = Exp.integer ln_ko Typ.siz in
   let ko = Exp.add k o in
   let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in
   let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
@@ -427,9 +427,9 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
       pp goal] ;
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let k_l = Exp.integer k_l in
-  let ln_k = Exp.integer ln_k in
-  let ko_ln = Exp.integer ko_ln in
+  let k_l = Exp.integer k_l Typ.siz in
+  let ln_k = Exp.integer ln_k Typ.siz in
+  let ko_ln = Exp.integer ko_ln Typ.siz in
   let ln = Exp.add l n in
   let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in