[sledge] Add Exp.true_ and Exp.false_

Summary: Convenience wrappers for Exp.integer.

Reviewed By: bennostein

Differential Revision: D17665234

fbshipit-source-id: 0cf440861

sledge/src/control.ml

@@ -412,8 +412,7 @@ module Make (Dom : Domain_sig.Dom) = struct
           ~init:
             ( match
                 Dom.exec_assume state
-                  (Vector.fold tbl ~init:(Exp.bool true)
+                  (Vector.fold tbl ~init:Exp.true_ ~f:(fun b (case, _) ->
-                     ~f:(fun b (case, _) ->
                        Exp.and_ Typ.bool (Exp.dq (Exp.typ key) key case) b
                    ))
               with

sledge/src/llair/exp.ml

@@ -389,6 +389,8 @@ let integer typ data =
 
 let null = integer Typ.ptr Z.zero
 let bool b = integer Typ.bool (Z.of_bool b)
+let true_ = bool true
+let false_ = bool false
 
 let float typ data =
   {desc= Float {data; typ}; term= Term.float data} |> check invariant

sledge/src/llair/exp.mli

@@ -132,6 +132,8 @@ val nondet : Typ.t -> string -> t
 val label : parent:string -> name:string -> t
 val null : t
 val bool : bool -> t
+val true_ : t
+val false_ : t
 val integer : Typ.t -> Z.t -> t
 val float : Typ.t -> string -> t
 

sledge/src/llair/frontend.ml

@@ -484,7 +484,7 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
     | Ule -> binary Exp.ule )
   | FCmp -> (
     match Llvm.fcmp_predicate llv with
-    | None | Some False -> binary (fun _ _ _ -> Exp.bool false)
+    | None | Some False -> binary (fun _ _ _ -> Exp.false_)
     | Some Oeq -> binary Exp.eq
     | Some Ogt -> binary Exp.gt
     | Some Oge -> binary Exp.ge
@@ -499,7 +499,7 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
     | Some Ult -> unordered_or Exp.lt
     | Some Ule -> unordered_or Exp.le
     | Some Une -> unordered_or Exp.dq
-    | Some True -> binary (fun _ _ _ -> Exp.bool true) )
+    | Some True -> binary (fun _ _ _ -> Exp.true_) )
   | Add | FAdd -> binary Exp.add
   | Sub | FSub -> binary Exp.sub
   | Mul | FMul -> binary Exp.mul

sledge/src/llair/llair.ml

@@ -324,11 +324,11 @@ module Term = struct
     | Throw _ | Unreachable -> assert true
 
   let goto ~dst ~loc =
-    Switch {key= Exp.bool false; tbl= Vector.empty; els= dst; loc}
+    Switch {key= Exp.false_; tbl= Vector.empty; els= dst; loc}
     |> check invariant
 
   let branch ~key ~nzero ~zero ~loc =
-    let tbl = Vector.of_array [|(Exp.bool false, zero)|] in
+    let tbl = Vector.of_array [|(Exp.false_, zero)|] in
     let els = nzero in
     Switch {key; tbl; els; loc} |> check invariant