From e00dbe46b1c9e97826da506db05caf68ab3af60d Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Wed, 2 Dec 2020 01:14:53 -0800 Subject: [PATCH] [topl] Got rid of quadratic runtime for long methods. Summary: For a long sequence of calls nop();...;nop() the runtime was quadratic because formals and actuals were bound via equalities. Now, substitutions are used, when easy. Reviewed By: jvillard Differential Revision: D25211504 fbshipit-source-id: 696e3dcdf --- infer/src/pulse/PulseTopl.ml | 50 +- .../java/topl/hasnext/ManyNops.java | 2023 +++++++++++++++++ 2 files changed, 2060 insertions(+), 13 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/topl/hasnext/ManyNops.java diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml index 3c2a3dd69..1f349443f 100644 --- a/infer/src/pulse/PulseTopl.ml +++ b/infer/src/pulse/PulseTopl.ml @@ -31,7 +31,6 @@ type vertex = ToplAutomaton.vindex [@@deriving compare] type register = ToplAst.register_name [@@deriving compare] -(* TODO(rgrigore): Change the memory assoc list to a Map. *) type configuration = {vertex: vertex; memory: (register * value) list} [@@deriving compare] type predicate = Binop.t * PathCondition.operand * PathCondition.operand [@@deriving compare] @@ -362,24 +361,48 @@ let sub_simple_state (sub, {pre; post; pruned; last_step}) = (sub, {pre; post; pruned; last_step}) -let sub_state = sub_list sub_simple_state +let normalize_memory memory = List.sort ~compare:[%compare: register * value] memory + +let normalize_configuration {vertex; memory} = {vertex; memory= normalize_memory memory} + +let normalize_pruned pruned = List.sort ~compare:compare_predicate pruned + +let normalize_simple_state {pre; post; pruned; last_step} = + { pre= normalize_configuration pre + ; post= normalize_configuration post + ; pruned= normalize_pruned pruned + ; last_step } + + +let normalize_state state = List.map ~f:normalize_simple_state state let large_step ~call_location ~callee_proc_name ~substitution ~condition ~callee_prepost state = let seq ((p : simple_state), (q : simple_state)) = if not (Int.equal p.post.vertex q.pre.vertex) then None else - let add_eq eqs (register, value_a) = - let value_b = - match List.Assoc.find ~equal:String.equal q.pre.memory register with - | Some x -> - x - | None -> - L.die InternalError "PulseTopl expects all registers in memory" + let substitution, new_eqs = + (* Update the substitution, matching formals with actuals. We work a bit to avoid introducing + equalities, because a growing [pruned] leads to quadratic behaviour. *) + let mk_eq val1 val2 = + let op x = PathCondition.AbstractValueOperand x in + (Binop.Eq, op val1, op val2) + in + let f (sub, eqs) (reg1, val1) (reg2, val2) = + if not (String.equal reg1 reg2) then + L.die InternalError + "PulseTopl: normalized memories are expected to have the same domain" + else + match AbstractValue.Map.find_opt val2 sub with + | Some (old_val1, _history) -> + if AbstractValue.equal old_val1 val1 then (sub, eqs) + else (sub, mk_eq old_val1 val1 :: eqs) + | None -> + (AbstractValue.Map.add val2 (val1, []) sub, eqs) in - let op x = PathCondition.AbstractValueOperand x in - (Binop.Eq, op value_a, op value_b) :: eqs + of_unequal (List.fold2 p.post.memory q.pre.memory ~init:(substitution, []) ~f) in - let pruned = List.fold ~init:(p.pruned @ q.pruned) ~f:add_eq p.post.memory in + let _substitution, q = sub_simple_state (substitution, q) in + let pruned = new_eqs @ q.pruned @ p.pruned in let last_step = Some { step_location= call_location @@ -388,8 +411,9 @@ let large_step ~call_location ~callee_proc_name ~substitution ~condition ~callee in Some {pre= p.pre; post= q.post; pruned; last_step} in - let _updated_substitution, callee_prepost = sub_state (substitution, callee_prepost) in (* TODO(rgrigore): may be worth optimizing the cartesian_product *) + let state = normalize_state state in + let callee_prepost = normalize_state callee_prepost in let new_state = List.filter_map ~f:seq (List.cartesian_product state callee_prepost) in let result = drop_infeasible condition new_state in L.d_printfln "@[<2>PulseTopl.large_step:@;callee_prepost=%a@;%a@ -> %a@]" pp_state callee_prepost diff --git a/infer/tests/codetoanalyze/java/topl/hasnext/ManyNops.java b/infer/tests/codetoanalyze/java/topl/hasnext/ManyNops.java new file mode 100644 index 000000000..3658827c1 --- /dev/null +++ b/infer/tests/codetoanalyze/java/topl/hasnext/ManyNops.java @@ -0,0 +1,2023 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +class ManyNops { + /** Let's check that nothing happens quickly. */ + void fOk() { + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + nop(); + } + + void nop() {} +}