hphp/hack/src/ifc/ifc_pretty.ml

   1 (*
   2  * Copyright (c) Facebook, Inc. and its affiliates.
   3  *
   4  * This source code is licensed under the MIT license found in the
   5  * LICENSE file in the "hack" directory of this source tree.
   6  *
   7  *)
   8
   9 open Hh_prelude
  10 open Format
  11 open Ifc_types
  12 module Env = Ifc_env
  13 module Logic = Ifc_logic
  14 module Utils = Ifc_utils
  15 module T = Typing_defs
  16
  17 let comma_sep fmt () = fprintf fmt ",@ "
  18
  19 let blank_sep fmt () = fprintf fmt "@ "
  20
  21 let newline_sep fmt () = fprintf fmt "@,"
  22
  23 let rec list pp_sep pp fmt = function
  24   | [] -> ()
  25   | [x] -> fprintf fmt "%a" pp x
  26   | x :: xs -> fprintf fmt "%a%a%a" pp x pp_sep () (list pp_sep pp) xs
  27
  28 let smap pp_sep pp fmt map =
  29   let prop_pol fmt (prop, pol) = fprintf fmt "%s=%a" prop pp pol in
  30   list pp_sep prop_pol fmt (SMap.bindings map)
  31
  32 let option pp fmt opt =
  33   match opt with
  34   | Some x -> fprintf fmt "%a" pp x
  35   | None -> fprintf fmt "None"
  36
  37 let show_policy = function
  38   | Pbot _ -> "PUBLIC"
  39   | Ptop _ -> "PRIVATE"
  40   | Ppurpose (_, p) -> p
  41   | Pfree_var (v, _s) -> v
  42   | Pbound_var n -> Printf.sprintf "<bound%d>" n
  43
  44 let policy fmt p = fprintf fmt "%s" (show_policy p)
  45
  46 let array_kind fmt = function
  47   | Avec -> fprintf fmt "vec"
  48   | Adict -> fprintf fmt "dict"
  49   | Akeyset -> fprintf fmt "keyset"
  50
  51 let rec ptype fmt ty =
  52   let list' sep l =
  53     let pp_sep fmt () = fprintf fmt "%s@ " sep in
  54     fprintf fmt "(@[<hov2>%a@])" (list pp_sep ptype) l
  55   in
  56   match ty with
  57   | Tprim p
  58   | Tgeneric p ->
  59     fprintf fmt "<%a>" policy p
  60   | Ttuple tl -> list' "," tl
  61   | Tunion [] -> fprintf fmt "nothing"
  62   | Tunion tl -> list' " |" tl
  63   | Tinter tl -> list' " &" tl
  64   | Tclass { c_name; c_self; c_lump } ->
  65     fprintf fmt "%s<@[<hov2>%a,@ %a@]>" c_name policy c_self policy c_lump
  66   | Tfun fn -> fun_ fmt fn
  67   | Tcow_array { a_key; a_value; a_length; a_kind } ->
  68     fprintf fmt "%a" array_kind a_kind;
  69     fprintf fmt "<%a => %a; |%a|>" ptype a_key ptype a_value policy a_length
  70   | Tshape (kind, m) ->
  71     let field fmt f =
  72       if f.sft_optional then fprintf fmt "?";
  73       ptype fmt f.sft_ty
  74     in
  75     fprintf fmt "shape(";
  76     Nast.ShapeMap.pp field fmt m;
  77     (match kind with
  78     | T.Closed_shape -> fprintf fmt ")"
  79     | T.Open_shape -> fprintf fmt ", ...)")
  80
  81 (* Format: <pc, self>(arg1, arg2, ...): ret [exn] *)
  82 and fun_ fmt fn =
  83   fprintf fmt "<%a, %a>" policy fn.f_pc policy fn.f_self;
  84   fprintf fmt "(@[<hov>%a@])" (list comma_sep ptype) fn.f_args;
  85   fprintf fmt ":@ %a [%a]" ptype fn.f_ret ptype fn.f_exn
  86
  87 let fun_proto fmt fp =
  88   Option.iter ~f:(fprintf fmt "(this: %a)->" ptype) fp.fp_this;
  89   fprintf fmt "%s%a" fp.fp_name fun_ fp.fp_type
  90
  91 let prop =
  92   let is_symmetric = function
  93     | (Cflow (_, a, b), Cflow (_, c, d)) -> equal_policy a d && equal_policy b c
  94     | _ -> false
  95   in
  96   let equate a b =
  97     if Policy.compare a b <= 0 then
  98       `q (a, b)
  99     else
 100       `q (b, a)
 101   in
 102   let rec conjuncts = function
 103     | Cconj ((Cflow (_, a, b) as f1), Cconj ((Cflow _ as f2), prop))
 104       when is_symmetric (f1, f2) ->
 105       equate a b :: conjuncts prop
 106     | Cconj ((Cflow (_, a, b) as f1), (Cflow _ as f2)) when is_symmetric (f1, f2)
 107       ->
 108       [equate a b]
 109     | Cconj (cl, cr) -> conjuncts cl @ conjuncts cr
 110     | Ctrue -> []
 111     | c -> [`c c]
 112   in
 113   let bv =
 114     let rec f = function
 115       | [] -> ['a']
 116       | 'z' :: n -> 'a' :: f n
 117       | c :: n -> Char.(of_int_exn (1 + to_int c)) :: n
 118     in
 119     (fun i -> String.of_char_list (Utils.funpow i ~f ~init:[]))
 120   in
 121   let pp_policy b fmt = function
 122     | Pbound_var n -> fprintf fmt "%s" (bv (b - n))
 123     | p -> policy fmt p
 124   in
 125   let rec aux b fmt =
 126     let pol = pp_policy b in
 127     function
 128     | [] -> fprintf fmt "True"
 129     | [`q (p1, p2)] -> fprintf fmt "%a = %a" pol p1 pol p2
 130     | [`c (Cflow (_, p1, p2))] -> fprintf fmt "%a < %a" pol p1 pol p2
 131     | [`c (Cquant (q, n, c))] ->
 132       fprintf
 133         fmt
 134         "@[<hov2>%s @[<h>%a@].@ %a@]"
 135         (match q with
 136         | Qexists -> "exists"
 137         | Qforall -> "forall")
 138         (list blank_sep pp_print_string)
 139         (snd
 140            (Utils.funpow
 141               n
 142               ~f:(fun (i, l) -> (i + 1, l @ [bv i]))
 143               ~init:(b + 1, [])))
 144         (aux (b + n))
 145         (conjuncts c)
 146     | [`c (Ccond ((_, p, x), ct, ce))] ->
 147       fprintf fmt "@[<hov>if %a < %s@" pol p x;
 148       let cct = conjuncts ct in
 149       let cce = conjuncts ce in
 150       fprintf fmt "then %a@ else %a@]" (aux b) cct (aux b) cce
 151     | [`c (Chole (_, fp))] -> fprintf fmt "@[<h>{%a}@]" fun_proto fp
 152     | l ->
 153       let pp = list comma_sep (fun fmt c -> aux b fmt [c]) in
 154       fprintf fmt "@[<hov>%a@]" pp l
 155   in
 156   (fun fmt c -> aux 0 fmt (conjuncts c))
 157
 158 let cont fmt k =
 159   pp_open_vbox fmt 0;
 160   fprintf fmt "@[<hov2>%a@]" (LMap.make_pp Local_id.pp ptype) k.k_vars;
 161   let policy_set fmt s = list comma_sep policy fmt (PSet.elements s) in
 162   if not (PSet.is_empty k.k_pc) then
 163     fprintf fmt "@,@[<hov2>pc: @[<hov>%a@]@]" policy_set k.k_pc;
 164   pp_close_box fmt ()
 165
 166 let renv fmt renv =
 167   pp_open_vbox fmt 0;
 168   fprintf fmt "* @[<hov2>pc: @[<hov>%a@]@]" policy renv.re_gpc;
 169   fprintf fmt "@,* @[<hov2>This:@ @[<hov>%a@]@]" (option ptype) renv.re_this;
 170   fprintf fmt "@,* @[<hov2>Return:@ @[<hov>%a@]@]" ptype renv.re_ret;
 171   fprintf fmt "@,* @[<hov2>Exception: @[<hov>%a@]@]" ptype renv.re_exn;
 172   pp_close_box fmt ()
 173
 174 let env fmt env =
 175   let rec flatten = function
 176     | Cconj (p1, p2) -> flatten p1 @ flatten p2
 177     | prop -> [prop]
 178   in
 179   let rec group_by_line =
 180     let has_same_pos p1 p2 =
 181       Option.equal Pos.equal (unique_pos_of_prop p1) (unique_pos_of_prop p2)
 182     in
 183     function
 184     | [] -> []
 185     | prop :: props ->
 186       let (group, rest) = List.partition_tf ~f:(has_same_pos prop) props in
 187       let pos_opt = unique_pos_of_prop prop in
 188       let prop = Logic.conjoin (prop :: group) in
 189       (pos_opt, prop) :: group_by_line rest
 190   in
 191   let group fmt (pos_opt, p) =
 192     match pos_opt with
 193     | Some pos -> fprintf fmt "@[<hov2>%a@ %a@]" Pos.pp pos prop p
 194     | None -> fprintf fmt "@[<hov2>[no pos]@ %a@]" prop p
 195   in
 196   let groups = list newline_sep group in
 197
 198   pp_open_vbox fmt 0;
 199   fprintf fmt "@[<hov2>Deps:@ %a@]" SSet.pp (Env.get_deps env);
 200   let props = List.concat_map ~f:flatten (Env.get_constraints env) in
 201   let prop_groups =
 202     let compare (pos1, _) (pos2, _) = Option.compare Pos.compare pos1 pos2 in
 203     group_by_line props |> List.sort ~compare
 204   in
 205   fprintf fmt "@,Constraints:@,  @[<v>%a@]" groups prop_groups;
 206   pp_close_box fmt ()
 207
 208 let class_decl fmt { cd_policied_properties = props; _ } =
 209   let policied_property fmt { pp_name; pp_purpose; _ } =
 210     fprintf fmt "%s:%s" pp_name pp_purpose
 211   in
 212   let properties fmt = list comma_sep policied_property fmt in
 213   fprintf fmt "{ policied_props = [@[<hov>%a@]] }" properties props
 214
 215 let fun_decl fmt decl =
 216   let kind =
 217     match decl.fd_kind with
 218     | FDPolicied (Some policy) -> show_policy policy
 219     | FDPolicied None -> "implicit"
 220     | FDInferFlows -> "infer"
 221   in
 222   fprintf fmt "{ kind = %s }" kind
 223
 224 let decl_env fmt de =
 225   let handle_class name decl =
 226     fprintf fmt "class %s: %a@ " name class_decl decl
 227   in
 228   fprintf fmt "Decls:@.  @[<v>";
 229   let handle_fun name decl =
 230     fprintf fmt "function %s: %a@ " name fun_decl decl
 231   in
 232   SMap.iter handle_class de.de_class;
 233   SMap.iter handle_fun de.de_fun;
 234   fprintf fmt "@]"
 235
 236 let implicit_violation fmt (l, r) =
 237   fprintf
 238     fmt
 239     "Data with an implicit policy is leaked by %a in context %a."
 240     policy
 241     l
 242     policy
 243     r
 244
 245 let security_lattice fmt lattice =
 246   let flow fmt (l, r) = fprintf fmt "%a < %a" policy l policy r in
 247   let flows = FlowSet.elements lattice in
 248   fprintf fmt "{%a}" (list comma_sep flow) flows