From 32846974ebfc6fd387cd428c80c8b54823dd6909 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 27 Jan 2021 07:58:40 -0800 Subject: [PATCH] [closure] Subst variables in ClosureSubstSpecializedMethod Summary: In `ClosureSubstSpecializedMethod`, it duplicates a procedure with specialized closure parameters. Since it introduces a new procedure name, its local variables in the procedure body must be replaced to use the new procedure name. (Note that local variable type includes procedure name.) However, in the previous implementation, it missed the translations in some cases: compound expressions and metadata. Reviewed By: ezgicicek Differential Revision: D26075490 fbshipit-source-id: 2a5a30cd8 --- .../backend/ClosureSubstSpecializedMethod.ml | 116 ++++++++++++++++-- 1 file changed, 104 insertions(+), 12 deletions(-) diff --git a/infer/src/backend/ClosureSubstSpecializedMethod.ml b/infer/src/backend/ClosureSubstSpecializedMethod.ml index 003219d3d..14d948ede 100644 --- a/infer/src/backend/ClosureSubstSpecializedMethod.ml +++ b/infer/src/backend/ClosureSubstSpecializedMethod.ml @@ -66,20 +66,108 @@ end module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions) +let try_keep_original ~default orig new_ ~f = if phys_equal orig new_ then default else f new_ + +let try_keep_original2 ~default orig1 new1 orig2 new2 ~f = + if phys_equal orig1 new1 && phys_equal orig2 new2 then default else f new1 new2 + + +let exec_pvar pname pvar = Pvar.swap_proc_in_local_pvar pvar pname + +let exec_var pname var = + let open Var in + match var with + | LogicalVar _ -> + var + | ProgramVar pvar -> + try_keep_original ~default:var pvar (exec_pvar pname pvar) ~f:of_pvar + + +let rec exec_exp pname e = + let open Exp in + match e with + | Var _ | Const _ -> + e + | UnOp (unop, e1, typ) -> + try_keep_original ~default:e e1 (exec_exp pname e1) ~f:(fun e1' -> UnOp (unop, e1', typ)) + | BinOp (binop, e1, e2) -> + try_keep_original2 ~default:e e1 (exec_exp pname e1) e2 (exec_exp pname e2) ~f:(fun e1' e2' -> + BinOp (binop, e1', e2') ) + | Exn e1 -> + try_keep_original ~default:e e1 (exec_exp pname e1) ~f:(fun e1' -> Exn e1') + | Closure {name; captured_vars} -> + let updated = ref false in + let captured_vars = + List.map captured_vars ~f:(fun ((e, pvar, typ, captured_mode) as captured_var) -> + try_keep_original2 ~default:captured_var e (exec_exp pname e) pvar + (exec_pvar pname pvar) ~f:(fun e' pvar' -> + updated := true ; + (e', pvar', typ, captured_mode) ) ) + in + if !updated then Closure {name; captured_vars} else e + | Cast (typ, e1) -> + try_keep_original ~default:e e1 (exec_exp pname e1) ~f:(fun e1' -> Cast (typ, e1')) + | Lvar pvar -> + try_keep_original ~default:e pvar (exec_pvar pname pvar) ~f:(fun pvar' -> Lvar pvar') + | Lfield (e1, fn, typ) -> + try_keep_original ~default:e e1 (exec_exp pname e1) ~f:(fun e1' -> Lfield (e1', fn, typ)) + | Lindex (e1, e2) -> + try_keep_original2 ~default:e e1 (exec_exp pname e1) e2 (exec_exp pname e2) ~f:(fun e1' e2' -> + Lindex (e1', e2') ) + | Sizeof {typ; nbytes; dynamic_length; subtype} -> + Option.value_map dynamic_length ~default:e ~f:(fun dynamic_length -> + try_keep_original ~default:e dynamic_length (exec_exp pname dynamic_length) + ~f:(fun dynamic_length' -> + Sizeof {typ; nbytes; dynamic_length= Some dynamic_length'; subtype} ) ) + + +let exec_metadata pname metadata = + let open Sil in + match metadata with + | Abstract _ | Skip -> + metadata + | ExitScope (vars, loc) -> + let updated = ref false in + let vars' = + List.map vars ~f:(fun var -> + try_keep_original ~default:var var (exec_var pname var) ~f:(fun var' -> + updated := true ; + var' ) ) + in + if !updated then ExitScope (vars', loc) else metadata + | Nullify (pvar, loc) -> + try_keep_original ~default:metadata pvar (exec_pvar pname pvar) ~f:(fun pvar' -> + Nullify (pvar', loc) ) + | VariableLifetimeBegins (pvar, typ, loc) -> + try_keep_original ~default:metadata pvar (exec_pvar pname pvar) ~f:(fun pvar' -> + VariableLifetimeBegins (pvar', typ, loc) ) + + +let exec_args proc_name args = + let updated = ref false in + let args' = + List.map + ~f:(fun ((exp, typ) as exp_typ) -> + try_keep_original ~default:exp_typ exp (exec_exp proc_name exp) ~f:(fun exp' -> + updated := true ; + (exp', typ) ) ) + args + in + if !updated then args' else args + + let exec_instr proc_name (id_to_pvar_map, pvars_to_blocks_map) instr = let open Sil in let res = - let exec_exp exp = - let exec_pvar pvar = Pvar.swap_proc_in_local_pvar pvar proc_name in - match exp with Exp.Lvar origin_pvar -> Exp.Lvar (exec_pvar origin_pvar) | exp -> exp - in match instr with | Load {id; e; root_typ; loc} -> - [Load {id; e= exec_exp e; root_typ; typ= root_typ; loc}] + [ try_keep_original ~default:instr e (exec_exp proc_name e) ~f:(fun e' -> + Load {id; e= e'; root_typ; typ= root_typ; loc} ) ] | Store {e1; root_typ; typ; e2; loc} -> - [Store {e1= exec_exp e1; root_typ; typ; e2= exec_exp e2; loc}] + [ try_keep_original2 ~default:instr e1 (exec_exp proc_name e1) e2 (exec_exp proc_name e2) + ~f:(fun e1' e2' -> Store {e1= e1'; root_typ; typ; e2= e2'; loc}) ] | Call (ret_id_typ, Var id, origin_args, loc, call_flags) -> ( - let converted_args = List.map ~f:(fun (exp, typ) -> (exec_exp exp, typ)) origin_args in + let converted_args = exec_args proc_name origin_args in match Option.bind ~f:VDom.get (BlockIdMap.find_opt id id_to_pvar_map) with | None -> [instr] @@ -107,12 +195,16 @@ let exec_instr proc_name (id_to_pvar_map, pvars_to_blocks_map) instr = | None -> [instr] ) ) | Call (return_ids, origin_call_exp, origin_args, loc, call_flags) -> - let converted_args = List.map ~f:(fun (exp, typ) -> (exec_exp exp, typ)) origin_args in - [Call (return_ids, exec_exp origin_call_exp, converted_args, loc, call_flags)] + [ try_keep_original2 ~default:instr origin_call_exp (exec_exp proc_name origin_call_exp) + origin_args (exec_args proc_name origin_args) + ~f:(fun converted_call_exp converted_args -> + Call (return_ids, converted_call_exp, converted_args, loc, call_flags) ) ] | Prune (origin_exp, loc, is_true_branch, if_kind) -> - [Prune (exec_exp origin_exp, loc, is_true_branch, if_kind)] - | _ -> - [instr] + [ try_keep_original ~default:instr origin_exp (exec_exp proc_name origin_exp) + ~f:(fun converted_exp -> Prune (converted_exp, loc, is_true_branch, if_kind)) ] + | Metadata metadata -> + [ try_keep_original ~default:instr metadata (exec_metadata proc_name metadata) + ~f:(fun metadata' -> Metadata metadata') ] in Array.of_list res