[pulse] no need to expose `PulseOperations.TBool`

Summary:
The business of translating `Top/True/False` to `true/false` can be
hidden more.

Reviewed By: skcho

Differential Revision: D18115228

fbshipit-source-id: 071fcbddf

infer/src/pulse/Pulse.ml

@@ -168,15 +168,14 @@ module PulseTransferFunctions = struct
               Ok astate
         in
         [check_error summary result]
-    | Prune (condition, loc, _is_then_branch, _if_kind) -> (
+    | Prune (condition, loc, _is_then_branch, _if_kind) ->
         let post, cond_satisfiable =
           PulseOperations.assert_is_true loc ~condition astate |> check_error summary
         in
-        match (cond_satisfiable : PulseOperations.TBool.t) with
+        if cond_satisfiable then
-        | False ->
+          (* [condition] is true or unknown value: go into the branch *)
-            (* [condition] is known to be unsatisfiable: prune path *) []
+          [post]
-        | True | Top ->
+        else (* [condition] is known to be unsatisfiable: prune path *) []
-            (* [condition] is true or unknown value: go into the branch *) [post] )
     | Call (ret, call_exp, actuals, loc, call_flags) ->
         dispatch_call summary ret call_exp actuals loc call_flags astate |> check_error summary
     | Metadata (ExitScope (vars, location)) ->

infer/src/pulse/PulseOperations.ml

@@ -200,7 +200,12 @@ let rec eval_cond ~negated location exp astate =
       eval_cond ~negated location (Exp.BinOp (Ne, exp, zero)) astate
 
 
-let assert_is_true location ~condition astate = eval_cond ~negated:false location condition astate
+let assert_is_true location ~condition astate =
+  eval_cond ~negated:false location condition astate
+  >>| fun (astate, result) ->
+  let can_go_through = match (result : TBool.t) with Top | True -> true | False -> false in
+  (astate, can_go_through)
+
 
 let eval_deref location exp astate =
   eval location exp astate

infer/src/pulse/PulseOperations.mli

@@ -25,12 +25,7 @@ val eval : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t))
     Return an error state if it traverses some known invalid address or if the end destination is
     known to be invalid. *)
 
-module TBool : sig
+val assert_is_true : Location.t -> condition:Exp.t -> t -> (t * bool) access_result
-  (** booleans with \top *)
-  type t = True | False | Top
-end
-
-val assert_is_true : Location.t -> condition:Exp.t -> t -> (t * TBool.t) access_result
 
 val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result
 (** Like [eval] but evaluates [*exp]. *)