Summary: Put hooks into Pulse for a faster Topl: - done: PulseAbductiveDomain now tracks a Topl state - todo: PulseTopl needs some transfer function (now they're dummies) Reviewed By: jvillard Differential Revision: D23815497 fbshipit-source-id: f3f0cf9efmaster
Radu Grigore
4 years ago
committed by
Facebook GitHub Bot
parent
128d13d810
commit
72a5a1e7ec
@ -0,0 +1,38 @@
|
||||
(*
|
||||
* Copyright (c) Facebook, Inc. and its affiliates.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
open PulseBasicInterface
|
||||
|
||||
type value = AbstractValue.t
|
||||
|
||||
type event = Call of {return: value option; arguments: value list}
|
||||
|
||||
type vertex = string
|
||||
|
||||
type register = string
|
||||
|
||||
type configuration = {vertex: vertex; memory: (register * value) list}
|
||||
|
||||
(** Let P be the [path_condition] in the enclosing pulse state, and let Q be the [path_condition] in
|
||||
the [simple_state] below. Then, the facts we know are P∧Q, and it should be that ∃V P∧Q,
|
||||
where V are the abstract values mentioned in the pre/post-configurations of the simple state, is
|
||||
equivalent to P. In other words, the facts in Q should not constrain program variables but may
|
||||
constrain Topl registers. *)
|
||||
type simple_state =
|
||||
{ pre: configuration (** at the start of the procedure *)
|
||||
; post: configuration (** at the current program point *)
|
||||
; path_condition: PathCondition.t }
|
||||
|
||||
(* TODO: include a hash of the automaton in a summary to avoid caching problems. *)
|
||||
type state = simple_state list
|
||||
|
||||
let start () = (* TODO *) []
|
||||
|
||||
let small_step _condition _event state = (* TODO *) state
|
||||
|
||||
let pp_state _formatter _state = (* TODO *) ()
|
||||
@ -0,0 +1,21 @@
|
||||
(*
|
||||
* Copyright (c) Facebook, Inc. and its affiliates.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
|
||||
type value = PulseAbstractValue.t
|
||||
|
||||
type event = Call of {return: value option; arguments: value list}
|
||||
|
||||
type state
|
||||
|
||||
val start : unit -> state
|
||||
(** Return the initial state of [Topl.automaton ()]. *)
|
||||
|
||||
val small_step : PulsePathCondition.t -> event -> state -> state
|
||||
|
||||
val pp_state : Format.formatter -> state -> unit
|
||||
@ -0,0 +1,56 @@
|
||||
(*
|
||||
* Copyright (c) Facebook, Inc. and its affiliates.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
|
||||
let add_errors {InterproceduralAnalysis.proc_desc; err_log} (pulse_summary : PulseSummary.t) =
|
||||
let pulse_summary =
|
||||
let f = function PulseExecutionDomain.ContinueProgram s -> Some s | _ -> None in
|
||||
List.filter_map ~f (pulse_summary :> PulseExecutionDomain.t list)
|
||||
in
|
||||
let proc_name = Procdesc.get_proc_name proc_desc in
|
||||
if not (ToplUtils.is_synthesized proc_name) then
|
||||
let start_to_error =
|
||||
Topl.automaton () |> ToplAutomaton.get_start_error_pairs |> Int.Table.of_alist_exn
|
||||
in
|
||||
let topl_property_var = Var.of_pvar ToplUtils.topl_class_pvar in
|
||||
let topl_state_field = HilExp.Access.FieldAccess (ToplUtils.make_field ToplName.state) in
|
||||
let check_pre_post pre_post =
|
||||
let open IOption.Let_syntax in
|
||||
let path_condition = pre_post.PulseAbductiveDomain.path_condition in
|
||||
let get_topl_state_opt pulse_state =
|
||||
let stack = pulse_state.PulseBaseDomain.stack in
|
||||
let heap = pulse_state.PulseBaseDomain.heap in
|
||||
let* topl_property_addr, _ = PulseBaseStack.find_opt topl_property_var stack in
|
||||
let* state_addr, _ =
|
||||
PulseBaseMemory.find_edge_opt topl_property_addr topl_state_field heap
|
||||
in
|
||||
let* state_val, _ =
|
||||
PulseBaseMemory.find_edge_opt state_addr HilExp.Access.Dereference heap
|
||||
in
|
||||
PulsePathCondition.as_int path_condition state_val
|
||||
in
|
||||
let* pre_topl = get_topl_state_opt (pre_post.PulseAbductiveDomain.pre :> PulseBaseDomain.t) in
|
||||
let* post_topl =
|
||||
get_topl_state_opt (pre_post.PulseAbductiveDomain.post :> PulseBaseDomain.t)
|
||||
in
|
||||
let* error_topl = Int.Table.find start_to_error pre_topl in
|
||||
if Int.equal post_topl error_topl then Some error_topl else None
|
||||
in
|
||||
let errors = List.filter_map ~f:check_pre_post pulse_summary in
|
||||
let errors = Int.Set.to_list (Int.Set.of_list errors) in
|
||||
let loc = Procdesc.get_loc proc_desc in
|
||||
let report error_state =
|
||||
let m =
|
||||
Format.asprintf "%a" ToplAutomaton.pp_message_of_state (Topl.automaton (), error_state)
|
||||
in
|
||||
Reporting.log_issue proc_desc err_log ToplOnPulse IssueType.topl_pulse_error ~loc m
|
||||
in
|
||||
List.iter ~f:report errors
|
||||
|
||||
|
||||
let analyze pulse analysis_data = Topl.analyze_with add_errors pulse analysis_data
|
||||
@ -0,0 +1,12 @@
|
||||
(*
|
||||
* Copyright (c) Facebook, Inc. and its affiliates.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
|
||||
val analyze : PulseSummary.t Topl.analysis_transformer
|
||||
(** Run pulse with Topl instrumentation if active. Inserts calls to the Topl automaton. Mutates the
|
||||
arguments: it is the caller's responsibility to instrument procedures at most once. *)
|
||||
Loading…
Reference in new issue