From 5ebc6562eedad4a3e1a2f9b58ddcf6251c47eb95 Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Wed, 14 Feb 2018 02:58:12 -0800 Subject: [PATCH] [HIL] AccessExpression on the left hand side of assignment Summary: More preparation for extending HIL with dereference and address of. We need left hand side of the assignment to also include dereference and address of. Reviewed By: sblackshear Differential Revision: D6976150 fbshipit-source-id: 47d1d76 --- infer/src/IR/HilInstr.ml | 22 ++++++++++++---------- infer/src/IR/HilInstr.mli | 3 ++- infer/src/absint/LowerHil.ml | 2 +- infer/src/checkers/Litho.ml | 6 ++++-- infer/src/checkers/NullabilityCheck.ml | 3 ++- infer/src/checkers/NullabilitySuggest.ml | 3 ++- infer/src/checkers/uninit.ml | 13 +++++++------ infer/src/concurrency/RacerD.ml | 3 ++- infer/src/quandary/TaintAnalysis.ml | 8 +++++--- 9 files changed, 37 insertions(+), 26 deletions(-) diff --git a/infer/src/IR/HilInstr.ml b/infer/src/IR/HilInstr.ml index 2ffe286a5..1165d1235 100644 --- a/infer/src/IR/HilInstr.ml +++ b/infer/src/IR/HilInstr.ml @@ -21,14 +21,16 @@ let pp_call fmt = function type t = - | Assign of AccessPath.t * HilExp.t * Location.t + | Assign of AccessExpression.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 - | Assign (access_path, exp, loc) -> - F.fprintf fmt "%a := %a [%a]" AccessPath.pp access_path HilExp.pp exp Location.pp loc + | Assign (access_expr, exp, loc) -> + F.fprintf fmt "%a := %a [%a]" AccessPath.pp + (AccessExpression.to_access_path access_expr) + 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) -> @@ -51,7 +53,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) = | AccessExpression rhs_access_expr -> Bind (lhs_id, AccessExpression.to_access_path rhs_access_expr) | _ -> - Instr (Assign (((lhs_id, rhs_typ), []), rhs_hil_exp, loc)) + Instr (Assign (AccessExpression.Base (lhs_id, rhs_typ), rhs_hil_exp, loc)) in match instr with | Load (lhs_id, rhs_exp, rhs_typ, loc) -> @@ -67,10 +69,10 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) = 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 = + let lhs_access_expr = match exp_of_sil lhs_exp typ with | AccessExpression access_expr -> - AccessExpression.to_access_path access_expr + access_expr | BinaryOperator (_, exp0, exp1) -> ( match (* pointer arithmetic. somewhere in one of the expressions, there should be at least @@ -80,11 +82,11 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) = HilExp.get_access_paths exp0 with | ap :: _ -> - ap + AccessExpression.of_access_path ap | [] -> match HilExp.get_access_paths exp1 with | ap :: _ -> - ap + AccessExpression.of_access_path ap | [] -> L.(die InternalError) "Invalid pointer arithmetic expression %a used as LHS at %a" Exp.pp lhs_exp @@ -95,12 +97,12 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) = let dummy_base_var = Var.of_id (Ident.create_normal (Ident.string_to_name (IntLit.to_string i)) 0) in - ((dummy_base_var, Typ.void_star), []) + AccessExpression.Base (dummy_base_var, Typ.void_star) | _ -> L.(die InternalError) "Non-assignable LHS expression %a at %a" Exp.pp lhs_exp Location.pp_file_pos loc in - Instr (Assign (lhs_access_path, exp_of_sil rhs_exp typ, loc)) + Instr (Assign (lhs_access_expr, exp_of_sil 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 = diff --git a/infer/src/IR/HilInstr.mli b/infer/src/IR/HilInstr.mli index 38633a74a..47334f391 100644 --- a/infer/src/IR/HilInstr.mli +++ b/infer/src/IR/HilInstr.mli @@ -14,7 +14,8 @@ module F = Format type call = Direct of Typ.Procname.t | Indirect of AccessPath.t [@@deriving compare] type t = - | Assign of AccessPath.t * HilExp.t * Location.t (** LHS access path, RHS expression *) + | Assign of AccessExpression.t * HilExp.t * Location.t + (** LHS access expression, 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 diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 5f1d02125..fa205d45e 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -68,7 +68,7 @@ struct let actual_state' = IdAccessPathMapDomain.fold (fun id access_path astate_acc -> - let lhs_access_path = ((id, Typ.mk Typ.Tvoid), []) in + let lhs_access_path = AccessExpression.Base (id, Typ.mk Typ.Tvoid) in let dummy_assign = HilInstr.Assign ( lhs_access_path diff --git a/infer/src/checkers/Litho.ml b/infer/src/checkers/Litho.ml index 90b7ea63f..45a676089 100644 --- a/infer/src/checkers/Litho.ml +++ b/infer/src/checkers/Litho.ml @@ -260,12 +260,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Call (ret_opt, Direct callee_procname, actuals, _, _) -> let summary = Summary.read_summary proc_data.pdesc callee_procname in apply_callee_summary summary caller_pname ret_opt actuals astate - | Assign (lhs_ap, HilExp.AccessExpression rhs_ae, _) + | Assign (lhs_ae, HilExp.AccessExpression rhs_ae, _) -> ( (* creating an alias for the rhs binding; assume all reads will now occur through the alias. this helps us keep track of chains in cases like tmp = getFoo(); x = tmp; tmp.getBar() *) - let lhs_access_path = Domain.LocalAccessPath.make lhs_ap caller_pname in + let lhs_access_path = + Domain.LocalAccessPath.make (AccessExpression.to_access_path lhs_ae) caller_pname + in let rhs_access_path = Domain.LocalAccessPath.make (AccessExpression.to_access_path rhs_ae) caller_pname in diff --git a/infer/src/checkers/NullabilityCheck.ml b/infer/src/checkers/NullabilityCheck.ml index 4cf3e2561..9de6f022b 100644 --- a/infer/src/checkers/NullabilityCheck.ml +++ b/infer/src/checkers/NullabilityCheck.ml @@ -289,8 +289,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct add_nullable_ap (ret_var, []) call_sites astate ) | Call (Some ret_var, _, _, _, _) -> remove_nullable_ap (ret_var, []) astate - | Assign (lhs, rhs, loc) + | Assign (lhs_access_expr, rhs, loc) -> ( + let lhs = AccessExpression.to_access_path lhs_access_expr in Option.iter ~f:(fun (nullable_ap, call_sites) -> if not (is_pointer_assignment proc_data.ProcData.tenv nullable_ap rhs) then diff --git a/infer/src/checkers/NullabilitySuggest.ml b/infer/src/checkers/NullabilitySuggest.ml index 7403c2057..f9201bac2 100644 --- a/infer/src/checkers/NullabilitySuggest.ml +++ b/infer/src/checkers/NullabilitySuggest.ml @@ -93,7 +93,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Call _ -> (* For now we just assume the callee always return non-null *) astate - | Assign (lhs, rhs, loc) -> + | Assign (lhs_access_expr, rhs, loc) -> + let lhs = AccessExpression.to_access_path lhs_access_expr in if not (is_access_nullable lhs proc_data) then match nullable_usedef_chain_of rhs lhs astate loc with | Some udchain -> diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index c1d5ed980..76ae24367 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -207,11 +207,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else astate.prepost in match instr with - | Assign - ( (((lhs_var, lhs_typ), apl) as lhs_ap) - , (HilExp.AccessExpression access_expr as rhs_expr) - , loc ) -> - let rhs_base, al = AccessExpression.to_access_path access_expr in + | Assign (lhs_access_expr, (HilExp.AccessExpression rhs_access_expr as rhs_expr), loc) -> + let ((lhs_var, lhs_typ), apl) as lhs_ap = + AccessExpression.to_access_path lhs_access_expr + in + let rhs_base, al = AccessExpression.to_access_path rhs_access_expr in let uninit_vars' = D.remove lhs_ap astate.uninit_vars in let uninit_vars = if Int.equal (List.length apl) 0 then @@ -224,7 +224,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct if should_report_var pdesc tenv uninit_vars (rhs_base, al) && not (Typ.is_pointer lhs_typ) then report_intra (rhs_base, al) loc (snd extras) ; {astate with uninit_vars; prepost} - | Assign (((lhs_ap, apl) as lhs), rhs, _) -> + | Assign (lhs_access_expr, rhs, _) -> + let (lhs_ap, apl) as lhs = AccessExpression.to_access_path lhs_access_expr in let uninit_vars = D.remove lhs astate.uninit_vars in let prepost = update_prepost (lhs_ap, apl) rhs in {astate with uninit_vars; prepost} diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index d8989aabb..472b274ef 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -711,7 +711,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {astate_callee with ownership; attribute_map} | _ -> astate_callee ) - | Assign (lhs_access_path, rhs_exp, loc) -> + | Assign (lhs_access_expr, rhs_exp, loc) -> + let lhs_access_path = AccessExpression.to_access_path lhs_access_expr in let rhs_accesses = add_access rhs_exp loc ~is_write_access:false astate.accesses astate.locks astate.threads astate.ownership proc_data diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 2d091165c..ef9f6fca1 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -508,19 +508,21 @@ module Make (TaintSpecification : TaintSpec.S) = struct TaintDomain.add_node (AccessPath.Abs.Exact lhs_access_path) rhs_node astate in match instr with - | Assign (((Var.ProgramVar pvar, _), []), HilExp.Exception _, _) when Pvar.is_return pvar -> + | Assign (AccessExpression.Base (Var.ProgramVar pvar, _), HilExp.Exception _, _) + when Pvar.is_return pvar -> (* the Java frontend translates `throw Exception` as `return Exception`, which is a bit wonky. this translation causes problems for us in computing a summary when an exception is "returned" from a void function. skip code like this for now, fix via t14159157 later *) astate - | Assign (((Var.ProgramVar pvar, _), []), rhs_exp, _) + | Assign (AccessExpression.Base (Var.ProgramVar pvar, _), rhs_exp, _) when Pvar.is_return pvar && HilExp.is_null_literal rhs_exp && Typ.equal_desc Tvoid (Procdesc.get_ret_type proc_data.pdesc).desc -> (* similar to the case above; the Java frontend translates "return no exception" as `return null` in a void function *) astate - | Assign (lhs_access_path, rhs_exp, loc) -> + | Assign (lhs_access_expr, rhs_exp, loc) -> + let lhs_access_path = AccessExpression.to_access_path lhs_access_expr in add_sources_sinks_for_exp rhs_exp loc astate |> add_sinks_for_access_path lhs_access_path loc |> exec_write lhs_access_path rhs_exp | Assume (assume_exp, _, _, loc) ->