[sledge] Support intrinsics which do not return

Summary:
Allow intrinsics to return an inconsistent state, to specify that they
do not return.

Reviewed By: kren1

Differential Revision: D16069453

fbshipit-source-id: deb5d2a22

sledge/src/control.ml

@@ -407,6 +407,7 @@ let exec_term :
             | Some (Error ()) ->
                 Report.invalid_access_term (Domain.project state) block.term ;
                 Work.skip
+            | Some (Ok state) when Domain.is_false state -> Work.skip
             | Some (Ok state) -> exec_goto stk state block return
             | None when Llair.Func.is_undefined callee ->
                 exec_skip_func stk state block return

sledge/src/symbheap/domain.ml

@@ -22,6 +22,8 @@ let join (entry_a, current_a) (entry_b, current_b) =
   assert (State_domain.equal entry_b entry_a) ;
   (entry_a, State_domain.join current_a current_b)
 
+let is_false (_, curr) = State_domain.is_false curr
+
 let exec_assume (entry, current) cnd =
   match State_domain.exec_assume current cnd with
   | Some current -> Some (entry, current)

sledge/src/symbheap/domain.mli

@@ -13,6 +13,7 @@ val project : t -> State_domain.t
 val pp : t pp
 val init : Global.t vector -> t
 val join : t -> t -> t
+val is_false : t -> bool
 val exec_assume : t -> Exp.t -> t option
 val exec_inst : t -> Llair.inst -> (t, unit) result
 val exec_return : t -> Var.t -> Exp.t -> t

sledge/src/symbheap/state_domain.ml

@@ -25,6 +25,7 @@ let init globals =
     | _ -> q )
 
 let join = Sh.or_
+let is_false = Sh.is_false
 let exec_assume = Exec.assume
 let exec_return = Exec.return
 let exec_inst = Exec.inst

sledge/src/symbheap/state_domain.mli

@@ -12,6 +12,7 @@ type t [@@deriving equal, sexp_of]
 val pp : t pp
 val init : Global.t vector -> t
 val join : t -> t -> t
+val is_false : t -> bool
 val exec_assume : t -> Exp.t -> t option
 val exec_inst : t -> Llair.inst -> (t, unit) result
 val exec_return : t -> Var.t -> Exp.t -> t