From d9978bb897c2732d5e46a6955ee41640922f564c Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 3 Jan 2019 06:04:35 -0800 Subject: [PATCH] [pulse] better pretty-printing of stacks Summary: Instead of `x -> 4` print the more accurate `&x=4`. Reviewed By: da319 Differential Revision: D13518669 fbshipit-source-id: 6ca28d0e1 --- infer/src/checkers/PulseDomain.ml | 38 +++++++++++++++++++++++-------- 1 file changed, 29 insertions(+), 9 deletions(-) diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index b8616e4c6..525107979 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -224,19 +224,39 @@ end functor followed by normalization wrt the unification found between abstract locations so it's convenient to define stacks as elements of this domain. *) module Stack = struct - include AbstractDomain.Map - (Var) - (struct - type t = AbstractAddress.t + module VarAddress = struct + include Var + + let pp f var = + let pp_ampersand f = function + | ProgramVar _ -> + F.pp_print_string f "&" + | LogicalVar _ -> + () + in + F.fprintf f "%a%a" pp_ampersand var Var.pp var + end + + module ValueDomain = struct + type t = AbstractAddress.t + + let ( <= ) ~lhs ~rhs = AbstractAddress.equal lhs rhs - let ( <= ) ~lhs ~rhs = AbstractAddress.equal lhs rhs + let join l1 l2 = min l1 l2 - let join l1 l2 = min l1 l2 + let widen ~prev ~next ~num_iters:_ = join prev next - let widen ~prev ~next ~num_iters:_ = join prev next + let pp = AbstractAddress.pp + end + + include AbstractDomain.Map (VarAddress) (ValueDomain) + + let pp fmt m = + let pp_item fmt (var_address, v) = + F.fprintf fmt "%a=%a" VarAddress.pp var_address ValueDomain.pp v + in + PrettyPrintable.pp_collection ~pp_item fmt (bindings m) - let pp = AbstractAddress.pp - end) let compare = compare AbstractAddress.compare end