[sledge] Factor out common code around calls of Dom.exec_assume

Reviewed By: jvillard

Differential Revision: D25756560

fbshipit-source-id: ace476496

sledge/src/control.ml

@@ -438,6 +438,15 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
     |>
     [%Trace.retn fun {pf} _ -> pf ""]
 
+  let exec_assume cond jump stk state block =
+    match Dom.exec_assume state cond with
+    | Some state -> exec_jump stk state block jump
+    | None ->
+        [%Trace.info
+          "@[<2>infeasible assume %a@\n@[%a@]@]" Llair.Exp.pp cond Dom.pp
+            state] ;
+        Work.skip
+
   let exec_term : Llair.program -> Stack.t -> Dom.t -> Llair.block -> Work.x
       =
    fun pgm stk state block ->
@@ -448,28 +457,22 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
     | Switch {key; tbl; els} ->
         IArray.fold
           ~f:(fun (case, jump) x ->
-            match Dom.exec_assume state (Llair.Exp.eq key case) with
+            exec_assume (Llair.Exp.eq key case) jump stk state block
-            | Some state -> exec_jump stk state block jump |> Work.seq x
+            |> Work.seq x )
-            | None -> x )
           tbl
-          ( match
+          (exec_assume
-              Dom.exec_assume state
+             (IArray.fold tbl Llair.Exp.true_ ~f:(fun (case, _) b ->
-                (IArray.fold tbl Llair.Exp.true_ ~f:(fun (case, _) b ->
+                  Llair.Exp.and_ (Llair.Exp.dq key case) b ))
-                     Llair.Exp.and_ (Llair.Exp.dq key case) b ))
+             els stk state block)
-            with
-          | Some state -> exec_jump stk state block els
-          | None -> Work.skip )
     | Iswitch {ptr; tbl} ->
         IArray.fold tbl Work.skip ~f:(fun (jump : Llair.jump) x ->
-            match
+            exec_assume
-              Dom.exec_assume state
+              (Llair.Exp.eq ptr
-                (Llair.Exp.eq ptr
+                 (Llair.Exp.label
-                   (Llair.Exp.label
+                    ~parent:(Llair.Function.name jump.dst.parent.name)
-                      ~parent:(Llair.Function.name jump.dst.parent.name)
+                    ~name:jump.dst.lbl))
-                      ~name:jump.dst.lbl))
+              jump stk state block
-            with
+            |> Work.seq x )
-            | Some state -> exec_jump stk state block jump |> Work.seq x
-            | None -> x )
     | Call ({callee} as call) ->
         exec_call stk state block call
           (Domain_used_globals.by_function Opts.globals callee.name)