From ad5d5dd89e51c929b12babc4d11d6ad17c796b88 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 9 Oct 2019 08:36:57 -0700
Subject: [PATCH] [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        | 3 +--
 sledge/src/llair/exp.ml      | 2 ++
 sledge/src/llair/exp.mli     | 2 ++
 sledge/src/llair/frontend.ml | 4 ++--
 sledge/src/llair/llair.ml    | 4 ++--
 5 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index a5075bf4e..a24eb7a36 100644
--- a/sledge/src/control.ml
+++ b/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)
-                     ~f:(fun b (case, _) ->
+                  (Vector.fold tbl ~init:Exp.true_ ~f:(fun b (case, _) ->
                        Exp.and_ Typ.bool (Exp.dq (Exp.typ key) key case) b
                    ))
               with
diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 2af9baf6c..45c593f3c 100644
--- a/sledge/src/llair/exp.ml
+++ b/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
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index 3c93ce484..b0d2aa252 100644
--- a/sledge/src/llair/exp.mli
+++ b/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
 
diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml
index e4b8d4b38..abfe97b29 100644
--- a/sledge/src/llair/frontend.ml
+++ b/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
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index 33724ad92..1bb26170f 100644
--- a/sledge/src/llair/llair.ml
+++ b/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