diff --git a/infer/src/checkers/loopInvariant.ml b/infer/src/checkers/loopInvariant.ml index 28ddaa0c5..6f20f5cbf 100644 --- a/infer/src/checkers/loopInvariant.ml +++ b/infer/src/checkers/loopInvariant.ml @@ -8,9 +8,12 @@ open! IStd module L = Logging module InvariantVars = AbstractDomain.FiniteSet (Var) module VarsInLoop = AbstractDomain.FiniteSet (Var) +module InvalidatedVars = AbstractDomain.FiniteSet (Var) module LoopNodes = AbstractDomain.FiniteSet (Procdesc.Node) module Models = InvariantModels +let debug fmt = L.(debug Analysis Medium) fmt + (** Map loop header node -> all nodes in the loop *) module LoopHeadToLoopNodes = Procdesc.NodeMap @@ -20,10 +23,8 @@ let is_defined_outside loop_nodes reaching_defs var = |> Option.value ~default:true -let is_fun_call_invariant tenv ~is_exp_invariant ~is_inv_by_default callee_pname params = - List.for_all ~f:(fun (exp, _) -> is_exp_invariant exp) params - && - (* Take into account invariance behavior of modeled functions *) +let is_fun_pure tenv ~is_inv_by_default callee_pname params = + (* Take into account purity behavior of modeled functions *) match Models.Call.dispatch tenv callee_pname params with | Some inv -> InvariantModels.is_invariant inv @@ -55,17 +56,19 @@ let is_def_unique_and_satisfy tenv var (loop_nodes : LoopNodes.t) ~is_inv_by_def when Exp.equal exp_lhs (Var.to_exp var) && is_exp_invariant exp_rhs -> true | Sil.Call ((id, _), Const (Cfun callee_pname), params, _, _) when equals_var id -> - is_fun_call_invariant tenv ~is_exp_invariant ~is_inv_by_default callee_pname - params + is_fun_pure tenv ~is_inv_by_default callee_pname params + && (* check if all params are invariant *) + List.for_all ~f:(fun (exp, _) -> is_exp_invariant exp) params | _ -> false ) ) loop_nodes -let is_exp_invariant inv_vars loop_nodes reaching_defs exp = +let is_exp_invariant inv_vars invalidated_vars loop_nodes reaching_defs exp = Var.get_all_vars_in_exp exp |> Sequence.for_all ~f:(fun var -> - InvariantVars.mem var inv_vars || is_defined_outside loop_nodes reaching_defs var ) + (not (InvalidatedVars.mem var invalidated_vars)) + && (InvariantVars.mem var inv_vars || is_defined_outside loop_nodes reaching_defs var) ) let get_vars_in_loop loop_nodes = @@ -97,14 +100,55 @@ let get_vars_in_loop loop_nodes = loop_nodes VarsInLoop.empty +let get_loaded_object var node invalidated_vars = + Procdesc.Node.get_instrs node + |> Instrs.fold + ~f:(fun acc instr -> + match instr with + | Sil.Load (id, Lvar pvar, typ, _) when Var.equal var (Var.of_id id) && Typ.is_pointer typ + -> + InvalidatedVars.add (Var.of_pvar pvar) acc + | _ -> + acc ) + ~init:invalidated_vars + + +let get_vars_to_invalidate node params invalidated_vars : InvalidatedVars.t = + List.fold ~init:invalidated_vars + ~f:(fun acc (arg_exp, _) -> + Var.get_all_vars_in_exp arg_exp + |> Sequence.fold ~init:acc ~f:(fun acc var -> + get_loaded_object var node (InvalidatedVars.add var acc) ) ) + params + + +(* If there is a call to an impure function in the loop, invalidate + all its non-primitive arguments. Once invalidated, it should be + never added again. *) +let get_invalidated_vars_in_loop tenv ~is_inv_by_default loop_nodes = + LoopNodes.fold + (fun node acc -> + Procdesc.Node.get_instrs node + |> Instrs.fold ~init:acc ~f:(fun acc instr -> + match instr with + | Sil.Call ((id, _), Const (Cfun callee_pname), params, _, _) + when not (is_fun_pure tenv ~is_inv_by_default callee_pname params) -> + get_vars_to_invalidate node params (InvalidatedVars.add (Var.of_id id) acc) + | _ -> + acc ) ) + loop_nodes InvalidatedVars.empty + + (* A variable is invariant if - its reaching definition is outside of the loop - o.w. its definition is constant or invariant itself *) let get_inv_vars_in_loop tenv reaching_defs_invariant_map ~is_inv_by_default loop_head loop_nodes = - let process_var_once var inv_vars = + let process_var_once var inv_vars invalidated_vars = (* if a variable is marked invariant once, it can't be invalidated (i.e. invariance is monotonic) *) - if InvariantVars.mem var inv_vars || Var.is_none var then (inv_vars, false) + if + InvariantVars.mem var inv_vars || Var.is_none var || InvalidatedVars.mem var invalidated_vars + then (inv_vars, false) else let loop_head_id = Procdesc.Node.get_id loop_head in ReachingDefs.Analyzer.extract_post loop_head_id reaching_defs_invariant_map @@ -117,7 +161,7 @@ let get_inv_vars_in_loop tenv reaching_defs_invariant_map ~is_inv_by_default loo else if (* its definition is unique and invariant *) is_def_unique_and_satisfy tenv var def_nodes ~is_inv_by_default - (is_exp_invariant inv_vars loop_nodes reaching_defs) + (is_exp_invariant inv_vars invalidated_vars loop_nodes reaching_defs) then (InvariantVars.add var inv_vars, true) else (inv_vars, false) ) |> Option.value (* if a var is not declared, it must be invariant *) @@ -127,16 +171,18 @@ let get_inv_vars_in_loop tenv reaching_defs_invariant_map ~is_inv_by_default loo let vars_in_loop = get_vars_in_loop loop_nodes in (* until there are no changes to inv_vars, keep repeatedly processing all the variables that occur in the loop nodes *) + let invalidated_vars = get_invalidated_vars_in_loop tenv ~is_inv_by_default loop_nodes in let rec find_fixpoint inv_vars = let inv_vars', modified = InvariantVars.fold (fun var (inv_vars, is_mod) -> - let inv_vars', is_mod' = process_var_once var inv_vars in + let inv_vars', is_mod' = process_var_once var inv_vars invalidated_vars in (inv_vars', is_mod || is_mod') ) vars_in_loop (inv_vars, false) in if modified then find_fixpoint inv_vars' else inv_vars' in + debug "\n>>> Invalidated vars: %a\n" InvalidatedVars.pp invalidated_vars ; find_fixpoint InvariantVars.empty diff --git a/infer/tests/codetoanalyze/java/hoisting/HoistIndirect.java b/infer/tests/codetoanalyze/java/hoisting/HoistIndirect.java index 7e7be9768..6d30ac727 100644 --- a/infer/tests/codetoanalyze/java/hoisting/HoistIndirect.java +++ b/infer/tests/codetoanalyze/java/hoisting/HoistIndirect.java @@ -7,10 +7,17 @@ class HoistIndirect { + public static int svar = 0; + int[] array; + class Test { int a = 0; + int foo(int x) { + return x + 10; + } + void set_test(Test test) { test.a = 5; } @@ -19,15 +26,132 @@ class HoistIndirect { return test.a; } - int indirect_modification_dont_hoist_FP(int size) { - int d = 0; - Test t = new Test(); + int get_sum_test(Test test, int x) { + return test.a + x; + } + + Test return_only(Test t) { + return t; + } + int indirect_modification_dont_hoist(int size, Test t) { + int d = 0; for (int i = 0; i < size; i++) { set_test(t); d = get_test(t); // don't hoist since t changes } return d; } + + void variant_arg_dont_hoist(int size, Test t) { + for (int i = 0; i < size; i++) { + set_test(t); // t is invalidated + get_sum_test( + return_only(t), + size); // foo' and return_only's arguments are variant, hence don't hoist + } + ; + } + + // t changes deep in the call stack + int deep_modification_dont_hoist(int size) { + int d = 0; + Test t = new Test(); + + for (int i = 0; i < size; i++) { + indirect_modification_dont_hoist(size, t); + } + return d; + } + + // foo(3) is ok to hoist, but can't detect this right now + int indirect_modification_hoist_FN(int size) { + int d = 0; + Test t = new Test(); + for (int i = 0; i < size; i++) { + set_test(t); // this (and t) is invalidated here + d = foo(3); // foo becomes variant due to implicit arg. this being invalidated above + } + return d; + } + } + + void set() { + svar = 5; + } + + int get() { + return svar; + } + + int indirect_this_modification_dont_hoist(int size) { + int d = 0; + + for (int i = 0; i < size; i++) { + d = get(); // don't hoist since this.svar changes in the loop + set(); + } + return d; + } + + int direct_this_modification_dont_hoist_FP(int size) { + int d = 0; + + for (int i = 0; i < size; i++) { + d += get(); // don't hoist since this.svar changes in the loop + svar = i; + } + return d; + } + + int this_modification_outside_hoist(int size) { + int d = 0; + set(); + for (int i = 0; i < size; i++) { + d += get(); // ok to hoist since set is outside + } + return d; + } + + int arg_modification_hoist(int size, Test t) { + int d = 0; + for (int i = 0; i < size; i++) { + d += get(); // ok to hoist since set_test doesn't modify this + t.set_test(t); + } + return d; + } + + void set_ith(int i, int[] array) { + array[i] = 0; + } + + int get_ith(int i, int[] array) { + return array[i]; + } + + int modified_array_dont_hoist(int size, Test t) { + int d = 0; + for (int i = 0; i < size; i++) { + set_ith(i, array); + d += get_ith(size, array); // don't hoist since array changes + } + return d; + } + + static int regionFirst(int[] region) { + return region[0]; + } + + static void incrDest(int[] source, int[] dest) { + dest[0] = source[0] + 1; + } + + void nested_change_dont_hoist_FP(int[][] nextRegionM, int p, int[] tempRegion) { + for (int i = 0; i < 10; i++) { + if (i < regionFirst(nextRegionM[p])) { + incrDest(tempRegion, nextRegionM[p]); + } + } } } diff --git a/infer/tests/codetoanalyze/java/hoisting/issues.exp b/infer/tests/codetoanalyze/java/hoisting/issues.exp index 421a23f62..36c82c3cc 100644 --- a/infer/tests/codetoanalyze/java/hoisting/issues.exp +++ b/infer/tests/codetoanalyze/java/hoisting/issues.exp @@ -21,5 +21,14 @@ codetoanalyze/java/hoisting/Hoist.java, Hoist.used_in_loop_body_before_def_temp_ codetoanalyze/java/hoisting/Hoist.java, Hoist.void_hoist(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Hoist.void_hoist(int)] codetoanalyze/java/hoisting/Hoist.java, Hoist.void_hoist(int):void, 2, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to void Hoist.dumb_foo() at line 183] codetoanalyze/java/hoisting/Hoist.java, Hoist.x_not_invariant_dont_hoist(int,int,int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Hoist.x_not_invariant_dont_hoist(int,int,int)] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.foo(int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect$Test.foo(int)] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.get_sum_test(HoistIndirect$Test,int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect$Test.get_sum_test(HoistIndirect$Test,int)] codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.get_test(HoistIndirect$Test):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect$Test.get_test(HoistIndirect$Test)] -codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.indirect_modification_dont_hoist_FP(int):int, 6, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect$Test.get_test(HoistIndirect$Test) at line 28] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.return_only(HoistIndirect$Test):HoistIndirect$Test, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function HoistIndirect$Test HoistIndirect$Test.return_only(HoistIndirect$Test)] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.arg_modification_hoist(int,HoistIndirect$Test):int, 3, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect.get() at line 119] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.direct_this_modification_dont_hoist_FP(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect.get() at line 101] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.get():int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect.get()] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.get_ith(int,int[]):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect.get_ith(int,int[])] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.nested_change_dont_hoist_FP(int[][],int,int[]):void, 2, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect.regionFirst(int[]) at line 152] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.regionFirst(int[]):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect.regionFirst(int[])] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.this_modification_outside_hoist(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect.get() at line 111]