diff --git a/infer/src/IR/Instrs.ml b/infer/src/IR/Instrs.ml
index 886a6b025..5b37fa4e5 100644
--- a/infer/src/IR/Instrs.ml
+++ b/infer/src/IR/Instrs.ml
@@ -91,6 +91,15 @@ let map_changed =
     if phys_equal instrs instrs' then t else NotReversed instrs'
 
 
+let concat_map_changed ~equal (NotReversed instrs as t) ~f =
+  let instrs' = Array.concat_map ~f instrs in
+  if
+    Int.equal (Array.length instrs) (Array.length instrs')
+    && Array.for_all2_exn ~f:equal instrs instrs'
+  then t
+  else NotReversed instrs'
+
+
 let reverse_order (NotReversed instrs) = Reversed (RevArray.of_rev_array instrs)
 
 (* Functions on both reversed and non-reversed arrays *)
diff --git a/infer/src/IR/Instrs.mli b/infer/src/IR/Instrs.mli
index 80cd12c8f..a973d819a 100644
--- a/infer/src/IR/Instrs.mli
+++ b/infer/src/IR/Instrs.mli
@@ -33,6 +33,12 @@ val map_changed :
   -> f:(Sil.instr -> Sil.instr)
   -> not_reversed_t
 
+val concat_map_changed :
+     equal:(Sil.instr -> Sil.instr -> bool)
+  -> not_reversed_t
+  -> f:(Sil.instr -> Sil.instr array)
+  -> not_reversed_t
+
 val reverse_order : not_reversed_t -> reversed t
 
 val is_empty : _ t -> bool
diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml
index f856acc82..bb0e19d5b 100644
--- a/infer/src/IR/Procdesc.ml
+++ b/infer/src/IR/Procdesc.ml
@@ -228,6 +228,15 @@ module Node = struct
       true )
 
 
+  (** Like [replace_instrs], but 1 instr gets replaced by 0, 1, or more instructions. *)
+  let replace_instrs_by node ~f =
+    let instrs' = Instrs.concat_map_changed ~equal:phys_equal node.instrs ~f:(f node) in
+    if phys_equal instrs' node.instrs then false
+    else (
+      node.instrs <- instrs' ;
+      true )
+
+
   let pp_stmt fmt = function
     | AssertionFailure ->
         F.pp_print_string fmt "Assertion failure"
@@ -508,13 +517,22 @@ let find_map_instrs pdesc ~f =
   find_map_nodes ~f:find_map_node pdesc
 
 
-let replace_instrs pdesc ~f =
-  let f updated node =
-    Node.replace_instrs ~f node || (* do not short-circuit [Node.replace_instrs] *) updated
-  in
+let update_nodes pdesc ~(update : Node.t -> bool) : bool =
+  let f acc node = update node || acc in
+  (* do not shortcut call to [update] *)
   fold_nodes pdesc ~init:false ~f
 
 
+let replace_instrs pdesc ~f =
+  let update node = Node.replace_instrs ~f node in
+  update_nodes pdesc ~update
+
+
+let replace_instrs_by pdesc ~f =
+  let update node = Node.replace_instrs_by ~f node in
+  update_nodes pdesc ~update
+
+
 (** fold between two nodes or until we reach a branching structure *)
 let fold_slope_range =
   let rec aux node visited acc ~f =
diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli
index 309490ff7..1b06d0ee0 100644
--- a/infer/src/IR/Procdesc.mli
+++ b/infer/src/IR/Procdesc.mli
@@ -261,6 +261,10 @@ val replace_instrs : t -> f:(Node.t -> Sil.instr -> Sil.instr) -> bool
 (** Map and replace the instructions to be executed.
     Returns true if at least one substitution occured. *)
 
+val replace_instrs_by : t -> f:(Node.t -> Sil.instr -> Sil.instr array) -> bool
+(** Like [replace_instrs], but slower, and each instruction may be replaced
+by 0, 1, or more instructions. *)
+
 val iter_nodes : (Node.t -> unit) -> t -> unit
 (** iterate over all the nodes of a procedure *)
 
diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli
index 31ff0468e..d0ca41eea 100644
--- a/infer/src/IR/Sil.mli
+++ b/infer/src/IR/Sil.mli
@@ -48,7 +48,7 @@ type instr =
       [*lexp1:typ = exp2] where
         [lexp1] is an expression denoting a heap address
         [typ] is the root type of [lexp1]
-        [exp2] is the expression whose value is store. *)
+        [exp2] is the expression whose value is stored. *)
   | Prune of Exp.t * Location.t * bool * if_kind
       (** prune the state based on [exp=1], the boolean indicates whether true branch *)
   | Call of (Ident.t * Typ.t) * Exp.t * (Exp.t * Typ.t) list * Location.t * CallFlags.t
diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml
index fda61124c..07df413c9 100644
--- a/infer/src/IR/Typ.ml
+++ b/infer/src/IR/Typ.ml
@@ -982,6 +982,7 @@ module Procname = struct
     | Block of Block.t
     | ObjC_Cpp of ObjC_Cpp.t
     | WithBlockParameters of t * Block.block_name list
+    | Topl_method of Java.t
   [@@deriving compare]
 
   let equal = [%compare.equal: t]
@@ -1024,6 +1025,8 @@ module Procname = struct
     match t with
     | Java j ->
         Java {j with class_name= new_class}
+    | Topl_method j ->
+        Topl_method {j with class_name= new_class}
     | ObjC_Cpp osig ->
         ObjC_Cpp {osig with class_name= new_class}
     | WithBlockParameters (base, blocks) ->
@@ -1060,7 +1063,7 @@ module Procname = struct
         ObjC_Cpp {osig with method_name= new_method_name}
     | WithBlockParameters (base, blocks) ->
         WithBlockParameters (objc_cpp_replace_method_name base new_method_name, blocks)
-    | C _ | Block _ | Linters_dummy_method | Java _ ->
+    | C _ | Block _ | Linters_dummy_method | Java _ | Topl_method _ ->
         t
 
 
@@ -1074,7 +1077,7 @@ module Procname = struct
         QualifiedCppName.to_qual_string name
     | Block {name} ->
         name
-    | Java j ->
+    | Java j | Topl_method j ->
         j.method_name
     | Linters_dummy_method ->
         "Linters_dummy_method"
@@ -1097,6 +1100,8 @@ module Procname = struct
         Language.Clang
     | Java _ ->
         Language.Java
+    | Topl_method _ ->
+        Language.Java
 
 
   (** [is_constructor pname] returns true if [pname] is a constructor *)
@@ -1141,7 +1146,7 @@ module Procname = struct
   (** Very verbose representation of an existing Procname.t *)
   let rec to_unique_id pn =
     match pn with
-    | Java j ->
+    | Java j | Topl_method j ->
         Java.to_string j Verbose
     | C osig ->
         C.to_string osig Verbose
@@ -1158,7 +1163,7 @@ module Procname = struct
   (** Convert a proc name to a string for the user to see *)
   let rec to_string p =
     match p with
-    | Java j ->
+    | Java j | Topl_method j ->
         Java.to_string j Non_verbose
     | C osig ->
         C.to_string osig Non_verbose
@@ -1175,7 +1180,7 @@ module Procname = struct
   (** Convenient representation of a procname for external tools (e.g. eclipse plugin) *)
   let rec to_simplified_string ?(withclass = false) p =
     match p with
-    | Java j ->
+    | Java j | Topl_method j ->
         Java.to_string ~withclass j Simple
     | C osig ->
         C.to_string osig Simple
@@ -1213,7 +1218,7 @@ module Procname = struct
       List.map ~f:(fun par -> Parameter.ClangParameter par) clang_params
     in
     match procname with
-    | Java j ->
+    | Java j | Topl_method j ->
         List.map ~f:(fun par -> Parameter.JavaParameter par) (Java.get_parameters j)
     | C osig ->
         clang_param_to_param (C.get_parameters osig)
@@ -1253,6 +1258,8 @@ module Procname = struct
     match procname with
     | Java j ->
         Java (Java.replace_parameters (params_to_java_params new_parameters) j)
+    | Topl_method j ->
+        Topl_method (Java.replace_parameters (params_to_java_params new_parameters) j)
     | C osig ->
         C (C.replace_parameters (params_to_clang_params new_parameters) osig)
     | ObjC_Cpp osig ->
diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli
index f0b084604..b3b960a1c 100644
--- a/infer/src/IR/Typ.mli
+++ b/infer/src/IR/Typ.mli
@@ -503,6 +503,7 @@ being the name of the struct, [None] means the parameter is of some other type.
     | Block of Block.t
     | ObjC_Cpp of ObjC_Cpp.t
     | WithBlockParameters of t * Block.block_name list
+    | Topl_method of Java.t
   [@@deriving compare]
 
   val block_name_of_procname : t -> Block.block_name
diff --git a/infer/src/backend/exe_env.ml b/infer/src/backend/exe_env.ml
index 8f5f117b7..ce1071d89 100644
--- a/infer/src/backend/exe_env.ml
+++ b/infer/src/backend/exe_env.ml
@@ -85,7 +85,7 @@ let java_global_tenv =
 
 let get_column_value ~value_on_java ~file_data_to_value ~column_name exe_env proc_name =
   match proc_name with
-  | Typ.Procname.Java _ ->
+  | Typ.Procname.Java _ | Typ.Procname.Topl_method _ ->
       Lazy.force value_on_java
   | _ -> (
     match get_file_data exe_env proc_name with
diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml
index ec3610792..9b4e0346c 100644
--- a/infer/src/backend/ondemand.ml
+++ b/infer/src/backend/ondemand.ml
@@ -59,8 +59,13 @@ let should_be_analyzed proc_attributes =
   (not (is_active proc_name)) (* avoid infinite loops *) && not (already_analyzed proc_name)
 
 
+let get_proc_attr proc_name =
+  IList.pick_first_some
+    [lazy (Topl.get_proc_attr proc_name); lazy (Summary.proc_resolve_attributes proc_name)]
+
+
 let procedure_should_be_analyzed proc_name =
-  match Summary.proc_resolve_attributes proc_name with
+  match get_proc_attr proc_name with
   | Some proc_attributes when Config.reactive_capture && not proc_attributes.is_defined ->
       (* try to capture procedure first *)
       let defined_proc_attributes = OndemandCapture.try_capture proc_attributes in
@@ -270,11 +275,10 @@ let analyze_proc_desc ~caller_pdesc callee_pdesc =
 
 (** Find a proc desc for the procedure, perhaps loading it from disk. *)
 let get_proc_desc callee_pname =
-  match Procdesc.load callee_pname with
-  | Some _ as pdesc_opt ->
-      pdesc_opt
-  | None ->
-      Option.map ~f:Summary.get_proc_desc (Summary.get callee_pname)
+  IList.pick_first_some
+    [ lazy (Procdesc.load callee_pname)
+    ; lazy (Topl.get_proc_desc callee_pname)
+    ; lazy (Option.map ~f:Summary.get_proc_desc (Summary.get callee_pname)) ]
 
 
 (** analyze_proc_name ?caller_pdesc proc_name performs an on-demand analysis of proc_name triggered
diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml
index fea014c5f..aa66f1174 100644
--- a/infer/src/backend/printer.ml
+++ b/infer/src/backend/printer.ml
@@ -210,9 +210,10 @@ let node_finish_session node =
 let write_proc_html pdesc =
   if Config.write_html then (
     let pname = Procdesc.get_proc_name pdesc in
-    let source = (Procdesc.get_loc pdesc).file in
+    let loc = Procdesc.get_loc pdesc in
+    let source = loc.file in
     let nodes = List.sort ~compare:Procdesc.Node.compare (Procdesc.get_nodes pdesc) in
-    let linenum = (Procdesc.Node.get_loc (List.hd_exn nodes)).Location.line in
+    let linenum = loc.Location.line in
     let fd, fmt = Io_infer.Html.create source [Typ.Procname.to_filename pname] in
     F.fprintf fmt "<center><h1>Procedure %a</h1></center>@\n"
       (Io_infer.Html.pp_line_link source
diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml
index 5fa0bc53d..cedeede57 100644
--- a/infer/src/biabduction/SymExec.ml
+++ b/infer/src/biabduction/SymExec.ml
@@ -1274,7 +1274,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t)
             let skip_loop =
               match ik with
               | Sil.Ik_while | Sil.Ik_for ->
-                  not (IntLit.iszero i) (* skip wile(1) and for (;1;) *)
+                  not (IntLit.iszero i) (* skip while(1) and for (;1;) *)
               | Sil.Ik_dowhile ->
                   true (* skip do..while *)
               | Sil.Ik_land_lor ->
@@ -1333,7 +1333,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t)
                 let ret_annots = proc_attrs.ProcAttributes.method_annotation.return in
                 exec_skip_call ~reason resolved_pname ret_annots proc_attrs.ProcAttributes.ret_type
             ) )
-      | Java callee_pname_java ->
+      | Java callee_pname_java | Topl_method callee_pname_java ->
           let norm_prop, norm_args = normalize_params tenv current_pname prop_ actual_params in
           let url_handled_args = call_constructor_url_update_args callee_pname norm_args in
           let resolved_pnames =
diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml
index 3702192b7..882e4af01 100644
--- a/infer/src/biabduction/interproc.ml
+++ b/infer/src/biabduction/interproc.ml
@@ -1258,7 +1258,7 @@ let analyze_procedure_aux summary exe_env tenv proc_desc : Summary.t =
 let analyze_procedure {Callbacks.summary; proc_desc; tenv; exe_env} : Summary.t =
   (* make sure models have been registered *)
   BuiltinDefn.init () ;
-  if not (List.is_empty Config.topl_properties) then Topl.init () ;
+  if Topl.active () then Topl.instrument tenv proc_desc ;
   try analyze_procedure_aux summary exe_env tenv proc_desc
   with exn ->
     IExn.reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ;
diff --git a/infer/src/istd/IList.ml b/infer/src/istd/IList.ml
index 74ebdb1ff..60aa6722b 100644
--- a/infer/src/istd/IList.ml
+++ b/infer/src/istd/IList.ml
@@ -182,6 +182,8 @@ let remove_first =
   fun list ~f -> aux list ~f []
 
 
+let pick_first_some lazies = List.find_map lazies ~f:Lazy.force
+
 let pp_print_list ~max ?(pp_sep = Format.pp_print_cut) pp_v ppf =
   let rec aux n = function
     | [] ->
diff --git a/infer/src/istd/IList.mli b/infer/src/istd/IList.mli
index 61d519ac1..d740b2b20 100644
--- a/infer/src/istd/IList.mli
+++ b/infer/src/istd/IList.mli
@@ -46,6 +46,10 @@ val opt_cons : 'a option -> 'a list -> 'a list
 
 val remove_first : 'a list -> f:('a -> bool) -> 'a list option
 
+val pick_first_some : 'a option lazy_t list -> 'a option
+(** [pick_first_some xs] forces the computation of each element of [xs] and returns the first
+that matches (Some _); or, if no such element exists, it returns None. *)
+
 val pp_print_list :
      max:int
   -> ?pp_sep:(Format.formatter -> unit -> unit)
diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml
index aaf393b00..31d957b9e 100644
--- a/infer/src/topl/Topl.ml
+++ b/infer/src/topl/Topl.ml
@@ -29,3 +29,128 @@ let init () =
   if not !initialized then (
     properties := List.concat_map ~f:parse Config.topl_properties ;
     initialized := true )
+
+
+let active () =
+  init () ;
+  not (List.is_empty !properties)
+
+
+let cfg = Cfg.create ()
+
+let sourcefile = SourceFile.create "SynthesizedToplProperty.java"
+
+let sourcefile_location = Location.none sourcefile
+
+(** The procedure description and its nodes will have location [sourcefile_location]. *)
+let empty_proc_desc proc_name =
+  let attr =
+    {(ProcAttributes.default sourcefile proc_name) with is_defined= true; loc= sourcefile_location}
+  in
+  let proc_desc = Cfg.create_proc_desc cfg attr in
+  let start_node =
+    Procdesc.create_node proc_desc sourcefile_location Procdesc.Node.Start_node []
+  in
+  let exit_node = Procdesc.create_node proc_desc sourcefile_location Procdesc.Node.Exit_node [] in
+  Procdesc.node_set_succs_exn proc_desc start_node [exit_node] [exit_node] ;
+  Procdesc.set_start_node proc_desc start_node ;
+  Procdesc.set_exit_node proc_desc exit_node ;
+  proc_desc
+
+
+let get_proc_desc = function
+  | Typ.Procname.Topl_method _ as proc_name ->
+      init () ;
+      (* TODO: generate code *)
+      Some (empty_proc_desc proc_name)
+  | _ ->
+      None
+
+
+let get_proc_attr proc_name =
+  (* TODO: optimize -- don't generate body just to get attributes  *)
+  Option.map ~f:Procdesc.get_attributes (get_proc_desc proc_name)
+
+
+(** TODO *)
+let get_transitions_count () = 1
+
+(** TODO: For now, just makes sure that *some* synthetic method gets called, so that the hookup
+mechanism gets tested. Later, it will need to compile TOPL properties into one automaton, number
+its transitions, and use that information to implement this function. *)
+let get_active_transitions _e_fun _arg_ts =
+  let result = [|true|] in
+  if not (Int.equal (Array.length result) (get_transitions_count ())) then
+    L.(die InternalError) "get_active_transitions should compute one bool for each transition" ;
+  result
+
+
+let topl_class_exp =
+  let class_name = Mangled.from_string "topl.Property" in
+  let var_name = Pvar.mk_global class_name in
+  Exp.Lvar var_name
+
+
+let topl_class_name : Typ.Name.t = Typ.Name.Java.from_string "topl.Property"
+
+let topl_class_typ = Typ.mk (Tstruct topl_class_name)
+
+let transition_field_name i = Typ.Fieldname.Java.from_string (Printf.sprintf "transition%d" i)
+
+let transition_var i = Exp.Lfield (topl_class_exp, transition_field_name i, topl_class_typ)
+
+let set_transitions loc active_transitions =
+  let store i b =
+    let value = if b then Exp.one else Exp.zero in
+    Sil.Store (transition_var i, topl_class_typ, value, loc)
+  in
+  Array.mapi ~f:store active_transitions
+
+
+(** TODO *)
+let call_save_args _loc _ret_id _ret_typ _arg_ts = [||]
+
+let call_execute loc =
+  let ret_id = Ident.create_fresh Ident.knormal in
+  let ret_typ = Typ.mk Tvoid in
+  let ret_typ_name = Some (Typ.Name.Java.Split.make JConfig.void) in
+  let e_fun =
+    Exp.Const
+      (Const.Cfun
+         (Typ.Procname.Topl_method
+            (Typ.Procname.Java.make topl_class_name ret_typ_name "execute" []
+               Typ.Procname.Java.Static)))
+  in
+  [|Sil.Call ((ret_id, ret_typ), e_fun, [], loc, CallFlags.default)|]
+
+
+let instrument_instruction = function
+  | Sil.Call ((ret_id, ret_typ), e_fun, arg_ts, loc, _call_flags) as i ->
+      let active_transitions = get_active_transitions e_fun arg_ts in
+      if not (Array.exists ~f:(fun x -> x) active_transitions) then [|i|]
+      else
+        let i1s = set_transitions loc active_transitions in
+        let i2s = call_save_args loc ret_id ret_typ arg_ts in
+        let i3s = call_execute loc in
+        Array.concat [[|i|]; i1s; i2s; i3s]
+  | i ->
+      [|i|]
+
+
+(* PRE: Calling [Tenv.mk_struct tenv <args>] twice is a no-op. *)
+let add_types tenv =
+  let transition_field i = (transition_field_name i, Typ.mk (Tint IBool), []) in
+  let rec transitions n =
+    if Int.equal n 0 then [] else transition_field (n - 1) :: transitions (n - 1)
+  in
+  let statics = transitions (get_transitions_count ()) in
+  let _topl_class = Tenv.mk_struct tenv topl_class_name ~statics in
+  ()
+
+
+let instrument tenv procdesc =
+  init () ;
+  add_types tenv ;
+  let f _node = instrument_instruction in
+  let _updated = Procdesc.replace_instrs_by procdesc ~f in
+  ()
diff --git a/infer/src/topl/Topl.mli b/infer/src/topl/Topl.mli
index 324a04f88..4ccf7b0c0 100644
--- a/infer/src/topl/Topl.mli
+++ b/infer/src/topl/Topl.mli
@@ -7,5 +7,15 @@
 
 open! IStd
 
-val init : unit -> unit
-(** Parse properties, mentioned by [Config.topl_properties]. Does this only once. *)
+val active : unit -> bool
+(** Returns whether the TOPL analysis is active. *)
+
+val get_proc_attr : Typ.Procname.t -> ProcAttributes.t option
+(** [get_proc_attr proc_name] returns the attributes of [get_proc_desc proc_name] *)
+
+val get_proc_desc : Typ.Procname.t -> Procdesc.t option
+(** Returns a synthesized Procdesc.t, when it corresponds to instrumentation for a TOPL property. *)
+
+val instrument : Tenv.t -> Procdesc.t -> unit
+(** Inserts calls to the TOPL automaton. Mutates the arguments: it is the caller's responsibility
+to instrument procedures at most once. *)