[hil] HIL instructions

Summary: Instruction language for new high-level IR

Reviewed By: jberdine

Differential Revision: D4899367

fbshipit-source-id: 9d4f735

infer/src/IR/HilExp.ml

@@ -56,37 +56,37 @@ let get_access_paths exp0 =
         acc in
   get_access_paths_ exp0 []
 
-(* convert an SIL expression into an HIL expression. the [lookup_id] function should map an SSA
+(* convert an SIL expression into an HIL expression. the [f_resolve_id] function should map an SSA
    temporary variable to the access path it represents. evaluating the HIL expression should
    produce the same result as evaluating the SIL expression and replacing the temporary variables
-   using [lookup_id] *)
-let rec of_sil ~lookup_id (exp : Exp.t) typ = match exp with
+   using [f_resolve_id] *)
+let rec of_sil ~f_resolve_id (exp : Exp.t) typ = match exp with
   | Var id ->
-      let ap = match lookup_id (Var.of_id id) with
+      let ap = match f_resolve_id (Var.of_id id) with
         | Some access_path -> access_path
         | None -> AccessPath.of_id id typ in
       AccessPath ap
   | UnOp (op, e, typ_opt) ->
-      UnaryOperator (op, of_sil ~lookup_id e typ, typ_opt)
+      UnaryOperator (op, of_sil ~f_resolve_id e typ, typ_opt)
   | BinOp (op, e0, e1) ->
-      BinaryOperator (op, of_sil ~lookup_id e0 typ, of_sil ~lookup_id e1 typ)
+      BinaryOperator (op, of_sil ~f_resolve_id e0 typ, of_sil ~f_resolve_id e1 typ)
   | Exn e ->
-      Exception (of_sil ~lookup_id e typ)
+      Exception (of_sil ~f_resolve_id e typ)
   | Const c ->
       Constant c
   | Cast (cast_typ, e) ->
-      Cast (cast_typ, of_sil ~lookup_id e typ)
+      Cast (cast_typ, of_sil ~f_resolve_id e typ)
   | Sizeof (sizeof_typ, dynamic_length, _) ->
-      Sizeof (sizeof_typ, Option.map ~f:(fun e -> of_sil ~lookup_id e typ) dynamic_length)
+      Sizeof (sizeof_typ, Option.map ~f:(fun e -> of_sil ~f_resolve_id e typ) dynamic_length)
   | Closure closure ->
       let environment =
         List.map
           ~f:(fun (value, pvar, typ) ->
-              AccessPath.base_of_pvar pvar typ, of_sil ~lookup_id value typ)
+              AccessPath.base_of_pvar pvar typ, of_sil ~f_resolve_id value typ)
           closure.captured_vars in
       Closure (closure.name, environment)
   | Lvar _ | Lfield _ | Lindex _ ->
-      match AccessPath.of_lhs_exp exp typ ~f_resolve_id:lookup_id with
+      match AccessPath.of_lhs_exp exp typ ~f_resolve_id with
       | Some access_path ->
           AccessPath access_path
       | None ->

infer/src/IR/HilExp.mli

@@ -34,7 +34,7 @@ type t =
 val pp : F.formatter -> t -> unit
 
 (** Convert SIL expression to HIL expression *)
-val of_sil : lookup_id:(Var.t -> AccessPath.Raw.t option) -> Exp.t -> Typ.t -> t
+val of_sil : f_resolve_id:(Var.t -> AccessPath.Raw.t option) -> Exp.t -> Typ.t -> t
 
 (** Get all the access paths used in the given HIL expression, including duplicates if a path is
     used more than once. *)

infer/src/IR/HilInstr.ml

@@ -0,0 +1,90 @@
+(*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+open! IStd
+
+module F = Format
+module L = Logging
+
+type call =
+  | Direct of Typ.Procname.t
+  | Indirect of AccessPath.Raw.t
+[@@deriving compare]
+
+let pp_call fmt = function
+  | Direct pname -> Typ.Procname.pp fmt pname
+  | Indirect access_path -> F.fprintf fmt "*%a" AccessPath.Raw.pp access_path
+
+type t =
+  | Write of AccessPath.Raw.t * HilExp.t * Location.t
+  | Assume of HilExp.t * [`Then | `Else] * Sil.if_kind * Location.t
+  | Call of AccessPath.base option * call * HilExp.t list * CallFlags.t * Location.t
+[@@deriving compare]
+
+let pp fmt = function
+  | Write (access_path, exp, loc) ->
+      F.fprintf fmt "%a := %a [%a]" AccessPath.Raw.pp access_path HilExp.pp exp Location.pp loc
+  | Assume (exp, _, _, loc) ->
+      F.fprintf fmt "assume %a [%a]" HilExp.pp exp Location.pp loc
+  | Call (ret_opt, call, actuals, _, loc) ->
+      let pp_ret fmt = Option.iter ~f:(F.fprintf fmt "%a := " AccessPath.pp_base) in
+      let pp_actuals fmt = PrettyPrintable.pp_collection ~pp_item:HilExp.pp fmt in
+      F.fprintf fmt "%a%a(%a) [%a]" pp_ret ret_opt pp_call call pp_actuals actuals Location.pp loc
+
+type translation =
+  | Instr of t
+  | Update of Var.t * AccessPath.Raw.t
+  | Ignore
+
+(* convert an SIL instruction into an HIL instruction. the [f_resolve_id] function should map an SSA
+   temporary variable to the access path it represents. evaluating the HIL instruction should
+   produce the same result as evaluating the SIL instruction and replacing the temporary variables
+   using [f_resolve_id]. *)
+let of_sil ~f_resolve_id (instr : Sil.instr) =
+  let analyze_id_assignment lhs_id rhs_exp rhs_typ loc =
+    let rhs_hil_exp = HilExp.of_sil ~f_resolve_id rhs_exp rhs_typ in
+    match HilExp.get_access_paths rhs_hil_exp with
+    | [rhs_access_path] ->
+        Update (lhs_id, rhs_access_path)
+    | _ ->
+        Instr (Write (((lhs_id, rhs_typ), []), rhs_hil_exp, loc)) in
+  match instr with
+  | Load (lhs_id, rhs_exp, rhs_typ, loc) ->
+      analyze_id_assignment (Var.of_id lhs_id) rhs_exp rhs_typ loc
+  | Store (Lvar lhs_pvar, lhs_typ, rhs_exp, loc)
+    when Pvar.is_ssa_frontend_tmp lhs_pvar ->
+      analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ loc
+  | Call (Some (ret_id, _), Const (Cfun callee_pname),
+          (target_exp, _) :: (Sizeof (cast_typ, _, _), _) :: _ , loc, _)
+    when Typ.Procname.equal callee_pname BuiltinDecl.__cast ->
+      analyze_id_assignment (Var.of_id ret_id) target_exp cast_typ loc
+  | Store (lhs_exp, typ, rhs_exp, loc) ->
+      let lhs_access_path =
+        match HilExp.of_sil ~f_resolve_id lhs_exp typ with
+        | AccessPath ap -> ap
+        | _ -> invalid_argf "Non-assignable LHS expression %a" Exp.pp lhs_exp in
+      Instr (Write (lhs_access_path, HilExp.of_sil ~f_resolve_id rhs_exp typ, loc))
+  | Call (ret_opt, call_exp, formals, loc, call_flags) ->
+      let hil_ret = Option.map ~f:(fun (ret_id, ret_typ) -> Var.of_id ret_id, ret_typ) ret_opt in
+      let hil_call =
+        match HilExp.of_sil ~f_resolve_id call_exp Typ.Tvoid with
+        | Constant (Cfun procname) -> Direct procname
+        | AccessPath access_path -> Indirect access_path
+        | call_exp -> invalid_argf "Unexpected call expression %a" HilExp.pp call_exp in
+      let formals = List.map ~f:(fun (exp, typ) -> HilExp.of_sil ~f_resolve_id exp typ) formals in
+      Instr (Call (hil_ret, hil_call, formals, call_flags, loc))
+  | Prune (exp, loc, true_branch, if_kind) ->
+      let hil_exp = HilExp.of_sil ~f_resolve_id exp (Typ.Tint Typ.IBool) in
+      let branch = if true_branch then `Then else `Else in
+      Instr (Assume (hil_exp, branch, if_kind, loc))
+  | Nullify _ | Remove_temps _
+  (* ignoring for now; will translate as builtin function call if needed *)
+  | Abstract _ | Declare_locals _ ->
+      (* these don't seem useful for most analyses. can translate them later if we want to *)
+      Ignore

infer/src/IR/HilInstr.mli

@@ -0,0 +1,41 @@
+(*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+open! IStd
+
+module F = Format
+
+(** type of a procedure call; either direct or via function pointer *)
+type call =
+  | Direct of Typ.Procname.t
+  | Indirect of AccessPath.Raw.t
+[@@deriving compare]
+
+val pp_call : F.formatter -> call -> unit
+
+type t =
+  | Write of AccessPath.Raw.t * HilExp.t * Location.t
+  (** LHS access path, RHS expression *)
+  | Assume of HilExp.t * [`Then | `Else] * Sil.if_kind * Location.t
+  (** Assumed expression, true_branch boolean, source of the assume (conditional, ternary, etc.) *)
+  | Call of AccessPath.base option * call * HilExp.t list * CallFlags.t * Location.t
+  (** Var to hold the return if it exists, call expression, formals *)
+[@@deriving compare]
+
+val pp : F.formatter -> t -> unit
+
+(** The result of translating an SIL instruction can either be a new HIL instruction or an update to
+    the identifier map (in the case that the SIL instructions writes to a temporary) *)
+type translation =
+  | Instr of t
+  | Update of Var.t * AccessPath.Raw.t
+  | Ignore
+
+(** Convert an SIL instruction to an HIL instruction *)
+val of_sil : f_resolve_id:(Var.t -> AccessPath.Raw.t option) -> Sil.instr -> translation