From 8383dcebb8ee587308da736ce86ee0e0afb1dcea Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 2 Mar 2020 08:44:03 -0800 Subject: [PATCH] [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 | 3 +++ sledge/src/sledge.ml | 4 ++++ sledge/src/symbheap/sh_domain.ml | 34 ++++++++++++++++++------------- sledge/src/symbheap/sh_domain.mli | 2 ++ 4 files changed, 29 insertions(+), 14 deletions(-) diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt index 0e2d76e39..7a745e09e 100644 --- a/sledge/sledge-help.txt +++ b/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 ] 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 ] enable debug tracing [-help] print this help text and exit @@ -193,6 +195,7 @@ The 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 ] wrap debug tracing at columns + [-no-simplify-states] do not simplify states during symbolic execution [-preanalyze-globals] pre-analyze global variables used by each function [-trace ] enable debug tracing [-help] print this help text and exit diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml index d210557ba..68bb59080 100644 --- a/sledge/src/sledge.ml +++ b/sledge/src/sledge.ml @@ -112,11 +112,15 @@ let analyze = " 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 = diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/src/symbheap/sh_domain.ml index 2cdb9078b..f6a6f57b0 100644 --- a/sledge/src/symbheap/sh_domain.ml +++ b/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 "@[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] diff --git a/sledge/src/symbheap/sh_domain.mli b/sledge/src/symbheap/sh_domain.mli index 9a7260bbf..a7912d12e 100644 --- a/sledge/src/symbheap/sh_domain.mli +++ b/sledge/src/symbheap/sh_domain.mli @@ -17,3 +17,5 @@ val create_summary : -> entry:t -> current:t -> summary * t + +val simplify_states : bool ref