[sledge][NFC] Minor code simplification

Reviewed By: bennostein

Differential Revision: D17801942

fbshipit-source-id: 45b881877

sledge/src/control.ml

@@ -328,7 +328,8 @@ module Make (Dom : Domain_sig.Dom) = struct
     [%Trace.call fun {pf} -> pf "from: %a" Reg.pp name.reg]
     ;
     let summarize post_state =
-      if opts.function_summaries then (
+      if not opts.function_summaries then post_state
+      else
         let globals = used_globals opts name.reg in
         let function_summary, post_state =
           Dom.create_summary ~locals post_state
@@ -336,8 +337,7 @@ module Make (Dom : Domain_sig.Dom) = struct
         in
         Hashtbl.add_multi summary_table ~key:name.reg ~data:function_summary ;
         pp_st () ;
-        post_state )
-      else post_state
+        post_state
     in
     let exit_state =
       match (freturn, exp) with

sledge/src/domain/domain_sig.ml

@@ -14,6 +14,7 @@ module type Dom = sig
   val init : Global.t vector -> t
   val join : t -> t -> t option
   val is_false : t -> bool
+  val dnf : t -> t list
   val exec_assume : t -> Exp.t -> t option
   val exec_kill : t -> Reg.t -> t
   val exec_move : t -> (Reg.t * Exp.t) vector -> t
@@ -40,14 +41,14 @@ module type Dom = sig
     -> t
     -> t * from_call
 
-  val recursion_beyond_bound : [`skip | `prune]
   val post : Reg.Set.t -> from_call -> t -> t
   val retn : Reg.t list -> Reg.t option -> from_call -> t -> t
-  val dnf : t -> t list
 
   val resolve_callee :
     (string -> Llair.func list) -> Exp.t -> t -> Llair.func list * t
 
+  val recursion_beyond_bound : [`skip | `prune]
+
   type summary
 
   val pp_summary : summary pp

sledge/src/symbheap/sh_domain.ml

@@ -28,6 +28,7 @@ let init globals =
 
 let join l r = Some (Sh.or_ l r)
 let is_false = Sh.is_false
+let dnf = Sh.dnf
 let exec_assume q b = Exec.assume q (Exp.term b)
 let exec_kill q r = Exec.kill q (Reg.var r)
 
@@ -69,8 +70,6 @@ let exec_intrinsic ~skip_throw q r i es =
   Exec.intrinsic ~skip_throw q (Option.map ~f:Reg.var r) (Reg.var i)
     (List.map ~f:Exp.term es)
 
-let dnf = Sh.dnf
-
 let term_eq_class_has_only_vars_in fvs cong term =
   [%Trace.call fun {pf} ->
     pf "@[<v> fvs: @[%a@] @,cong: @[%a@] @,term: @[%a@]@]" Var.Set.pp fvs
@@ -163,8 +162,6 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
     pf "@[<v>subst: %a@ frame: %a@ q': %a@]" Var.Subst.pp subst pp frame pp
       q']
 
-let recursion_beyond_bound = `prune
-
 (** Leave scope of locals: existentially quantify locals. *)
 let post locals _ q =
   [%Trace.call fun {pf} ->
@@ -204,6 +201,8 @@ let resolve_callee lookup ptr q =
   | Some callee -> (lookup (Reg.name callee), q)
   | None -> ([], q)
 
+let recursion_beyond_bound = `prune
+
 type summary = {xs: Var.Set.t; foot: t; post: t}
 
 let pp_summary fs {xs; foot; post} =