[topl] Extract summaries from posts

Summary: Prune inconsitent specs, kill unreachable vars.

Reviewed By: jvillard

Differential Revision: D25150011

fbshipit-source-id: 7087504fa

infer/src/pulse/PulseAbductiveDomain.ml

@@ -401,7 +401,8 @@ let filter_for_summary astate =
   let post_heap = deregister_empty (astate.post :> base_domain).heap in
   { astate with
     pre= PreDomain.update astate.pre ~heap:pre_heap
-  ; post= PostDomain.update ~stack:post_stack ~heap:post_heap astate.post }
+  ; post= PostDomain.update ~stack:post_stack ~heap:post_heap astate.post
+  ; topl= PulseTopl.filter_for_summary astate.path_condition astate.topl }
 
 
 let add_out_of_scope_attribute addr pvar location history heap typ =
@@ -478,7 +479,8 @@ let summary_of_post pdesc astate =
     { astate with
       path_condition=
         PathCondition.simplify ~keep:live_addresses astate.path_condition
-        |> incorporate_new_eqs astate }
+        |> incorporate_new_eqs astate
+    ; topl= PulseTopl.simplify ~keep:live_addresses astate.topl }
   in
   invalidate_locals pdesc astate
 

infer/src/pulse/PulseTopl.ml

@@ -49,17 +49,18 @@ let pp_mapping f (x, value) = Format.fprintf f "@[%s↦%a@]@," x AbstractValue.p
 let pp_memory f memory = Format.fprintf f "@[<2>[%a]@]" (pp_comma_seq pp_mapping) memory
 
 let pp_configuration f {vertex; memory} =
-  Format.fprintf f "@[{topl-config@;vertex=%d@;memory=%a}@]" vertex pp_memory memory
+  Format.fprintf f "@[{ topl-config@;vertex=%d@;memory=%a }@]" vertex pp_memory memory
 
 
 let pp_simple_state f {pre; post; pruned} =
-  Format.fprintf f "@[<2>{topl-simple-state@;pre=%a@;post=%a@;pruned=(%a)}@]" pp_configuration pre
+  Format.fprintf f "@[<2>{ topl-simple-state@;pre=%a@;post=%a@;pruned=(%a) }@]" pp_configuration pre
     pp_configuration post (Pp.seq ~sep:"∧" pp_predicate) pruned
 
 
-let pp_state f = Format.fprintf f "@[<2>[ %a]@]" (pp_comma_seq pp_simple_state)
+let pp_state f = Format.fprintf f "@[<2>[ %a ]@]" (pp_comma_seq pp_simple_state)
 
 let start () =
+  let mk_simple_states () =
     let a = Topl.automaton () in
     let starts = ToplAutomaton.starts a in
     let mk_memory =
@@ -68,6 +69,8 @@ let start () =
     in
     let configurations = List.map ~f:(fun vertex -> {vertex; memory= mk_memory ()}) starts in
     List.map ~f:(fun c -> {pre= c; post= c; pruned= []}) configurations
+  in
+  if Topl.is_deep_active () then mk_simple_states () else (* Avoids work later *) []
 
 
 let get env x =
@@ -80,6 +83,14 @@ let get env x =
 
 let set = List.Assoc.add ~equal:String.equal
 
+let is_trivially_true (predicate : predicate) =
+  match predicate with
+  | Eq, AbstractValueOperand l, AbstractValueOperand r when AbstractValue.equal l r ->
+      true
+  | _ ->
+      false
+
+
 let eval_guard memory tcontext guard =
   let operand_of_value (value : ToplAst.value) : PathCondition.operand =
     match value with
@@ -90,17 +101,18 @@ let eval_guard memory tcontext guard =
     | Binding v ->
         AbstractValueOperand (get tcontext v)
   in
+  let add predicate pruned = if is_trivially_true predicate then pruned else predicate :: pruned in
   let conjoin_predicate pruned (predicate : ToplAst.predicate) =
     match predicate with
     | Binop (binop, l, r) ->
         let l = operand_of_value l in
         let r = operand_of_value r in
         let binop = ToplUtils.binop_to binop in
-        (binop, l, r) :: pruned
+        add (binop, l, r) pruned
     | Value v ->
         let v = operand_of_value v in
         let one = PathCondition.LiteralOperand IntLit.one in
-        (Binop.Ne, v, one) :: pruned
+        add (Binop.Ne, v, one) pruned
   in
   List.fold ~init:[] ~f:conjoin_predicate guard
 
@@ -241,3 +253,26 @@ let small_step path_condition event simple_states =
 
 
 let large_step ~substitution:_ ~condition:_ ~callee_prepost:_ _state = (* TODO *) []
+
+let filter_for_summary path_condition state =
+  List.filter ~f:(fun x -> not (is_unsat path_condition x.pruned)) state
+
+
+let simplify ~keep state =
+  let simplify_simple_state {pre; post; pruned} =
+    (* NOTE(rgrigore): registers could be considered live for the program path_condition as well.
+       That should improve precision, but I'm wary of altering what the Pulse program state is just
+       because Topl is enabled. *)
+    let collect memory keep =
+      List.fold ~init:keep ~f:(fun keep (_reg, value) -> AbstractValue.Set.add value keep) memory
+    in
+    let keep = keep |> collect pre.memory |> collect post.memory in
+    let is_live_operand =
+      PathCondition.(
+        function LiteralOperand _ -> true | AbstractValueOperand v -> AbstractValue.Set.mem v keep)
+    in
+    let is_live_predicate (_op, l, r) = is_live_operand l && is_live_operand r in
+    let pruned = List.filter ~f:is_live_predicate pruned in
+    {pre; post; pruned}
+  in
+  List.map ~f:simplify_simple_state state

infer/src/pulse/PulseTopl.mli

@@ -29,4 +29,11 @@ val large_step :
     [callee_prepost] in another scope: the [substitution] maps from the callee scope to the
     condition&state scope. *)
 
+val filter_for_summary : PulsePathCondition.t -> state -> state
+(** Remove from state those parts that are inconsistent with the path condition. (We do a cheap
+    check to not introduce inconsistent Topl states, but they mey become inconsistent because the
+    program path condition is updated later.) *)
+
+val simplify : keep:PulseAbstractValue.Set.t -> state -> state
+
 val pp_state : Format.formatter -> state -> unit