[sledge] Simplify states during symbolic execution

Summary:
`Sh.simplify` formulas after each manipulation during symbolic
execution, unless `-no-simplify-states` is passed.

Reviewed By: ngorogiannis

Differential Revision: D20120265

fbshipit-source-id: 11464cfb2

sledge/sledge-help.txt

@@ -61,6 +61,7 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s
                           points specified in the config file
   [-no-models]            do not add models for C/C++ runtime and standard
                           libraries
+  [-no-simplify-states]   do not simplify states during symbolic execution
   [-preanalyze-globals]   pre-analyze global variables used by each function
   [-trace <spec>]         enable debug tracing
   [-help]                 print this help text and exit
@@ -146,6 +147,7 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo
                           points specified in the config file
   [-no-models]            do not add models for C/C++ runtime and standard
                           libraries
+  [-no-simplify-states]   do not simplify states during symbolic execution
   [-preanalyze-globals]   pre-analyze global variables used by each function
   [-trace <spec>]         enable debug tracing
   [-help]                 print this help text and exit
@@ -193,6 +195,7 @@ The <input> file must be binary LLAIR, such as produced by `sledge translate`.
   [-exceptions]          explore executions that throw and handle exceptions
   [-function-summaries]  use function summaries (in development)
   [-margin <cols>]       wrap debug tracing at <cols> columns
+  [-no-simplify-states]  do not simplify states during symbolic execution
   [-preanalyze-globals]  pre-analyze global variables used by each function
   [-trace <spec>]        enable debug tracing
   [-help]                print this help text and exit

sledge/src/sledge.ml

@@ -112,11 +112,15 @@ let analyze =
         "<string> select abstract domain; must be one of \"sh\" (default, \
          symbolic heap domain), \"globals\" (used-globals domain), or \
          \"unit\" (unit domain)"
+  and no_simplify_states =
+    flag "no-simplify-states" no_arg
+      ~doc:"do not simplify states during symbolic execution"
   in
   fun program () ->
     let pgm = program () in
     let globals = used_globals pgm preanalyze_globals in
     let skip_throw = not exceptions in
+    Sh_domain.simplify_states := not no_simplify_states ;
     exec {bound; skip_throw; function_summaries; globals} pgm
 
 let analyze_cmd =

sledge/src/symbheap/sh_domain.ml

@@ -9,14 +9,13 @@
 
 type t = Sh.t [@@deriving equal, sexp_of]
 
-let pp_simp fs q =
-  let q' = ref q in
-  [%Trace.printf "%a" (fun _ q -> q' := Sh.simplify q) q] ;
-  Sh.pp fs !q'
-
-let pp = pp_simp
+let pp fs q = Format.fprintf fs "@[{ %a@ }@]" Sh.pp q
 let report_fmt_thunk = Fn.flip pp
 
+(* set by cli *)
+let simplify_states = ref true
+let simplify q = if !simplify_states then Sh.simplify q else q
+
 let init globals =
   Vector.fold globals ~init:Sh.emp ~f:(fun q -> function
     | {Global.reg; init= Some arr} ->
@@ -27,22 +26,23 @@ let init globals =
     | _ -> q )
 
 let join p q =
-  [%Trace.call fun {pf} -> pf "{ %a@ }@ { %a@ }" Sh.pp p Sh.pp q]
+  [%Trace.call fun {pf} -> pf "%a@ %a" pp p pp q]
   ;
-  Some (Sh.or_ p q)
+  Some (Sh.or_ p q) |> Option.map ~f:simplify
   |>
-  [%Trace.retn fun {pf} -> pf "%a" (Option.pp "%a" Sh.pp)]
+  [%Trace.retn fun {pf} -> pf "%a" (Option.pp "%a" pp)]
 
 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)
+let exec_assume q b = Exec.assume q (Exp.term b) |> Option.map ~f:simplify
+let exec_kill q r = Exec.kill q (Reg.var r) |> simplify
 
 let exec_move q res =
   Exec.move q (Vector.map res ~f:(fun (r, e) -> (Reg.var r, Exp.term e)))
+  |> simplify
 
 let exec_inst pre inst =
-  match (inst : Llair.inst) with
+  ( match (inst : Llair.inst) with
   | Move {reg_exps; _} ->
       Some
         (Exec.move pre
@@ -67,11 +67,13 @@ let exec_inst pre inst =
         ~len:(Exp.term len)
   | Free {ptr; _} -> Exec.free pre ~ptr:(Exp.term ptr)
   | Nondet {reg; _} -> Some (Exec.nondet pre (Option.map ~f:Reg.var reg))
-  | Abort _ -> Exec.abort pre
+  | Abort _ -> Exec.abort pre )
+  |> Option.map ~f:simplify
 
 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)
+  |> Option.map ~f:(Option.map ~f:simplify)
 
 let term_eq_class_has_only_vars_in fvs cong term =
   [%Trace.call fun {pf} ->
@@ -166,6 +168,8 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
   let entry = and_eqs subst formals actuals q' in
   (* note: locals and formals are in scope *)
   assert (Set.is_subset (Set.add_list formals freturn_locals) ~of_:entry.us) ;
+  (* simplify *)
+  let entry = simplify entry in
   ( if not summaries then (entry, {areturn; subst; frame= Sh.emp})
   else
     let q'', frame =
@@ -182,7 +186,7 @@ let post locals _ q =
   [%Trace.call fun {pf} ->
     pf "@[<hv>locals: {@[%a@]}@ q: %a@]" Reg.Set.pp locals Sh.pp q]
   ;
-  Sh.exists (Reg.Set.vars locals) q
+  Sh.exists (Reg.Set.vars locals) q |> simplify
   |>
   [%Trace.retn fun {pf} -> pf "%a" Sh.pp]
 
@@ -219,6 +223,8 @@ let retn formals freturn {areturn; subst; frame} q =
   let q = Sh.rename inv_subst q in
   (* reconjoin frame *)
   Sh.star frame q
+  (* simplify *)
+  |> simplify
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 

sledge/src/symbheap/sh_domain.mli

@@ -17,3 +17,5 @@ val create_summary :
   -> entry:t
   -> current:t
   -> summary * t
+
+val simplify_states : bool ref