[absint] separate id map bookkeeping from checker transfer functions in LowerHIL

Summary:
This may help running the id map bookkeeping on its own in the future
and makes the code slightly more readable in my opinion.

Reviewed By: mbouaziz

Differential Revision: D12858066

fbshipit-source-id: fea4aea63

infer/src/absint/LowerHil.ml

@@ -15,6 +15,16 @@ module DefaultConfig : HilConfig = struct
   let include_array_indexes = false
 end
 
+let update_id_map hil_translation id_map =
+  match (hil_translation : HilInstr.translation) with
+  | Bind (id, access_path) ->
+      IdAccessPathMapDomain.add id access_path id_map
+  | Unbind ids ->
+      List.fold ~f:(fun acc id -> IdAccessPathMapDomain.remove id acc) ~init:id_map ids
+  | Instr _ | Ignore ->
+      id_map
+
+
 (** HIL adds a map from temporary variables to access paths to each domain *)
 module MakeHILDomain (Domain : AbstractDomain.S) = struct
   include AbstractDomain.Pair (Domain) (IdAccessPathMapDomain)
@@ -42,20 +52,9 @@ struct
     && match ConcurrencyModels.get_lock pname actuals with Unlock -> true | _ -> false
 
 
-  let exec_instr ((actual_state, id_map) as astate) extras node instr =
-    let f_resolve_id id = IdAccessPathMapDomain.find_opt id id_map in
-    match
-      HilInstr.of_sil ~include_array_indexes:HilConfig.include_array_indexes ~f_resolve_id instr
-    with
-    | Bind (id, access_path) ->
-        let id_map' = IdAccessPathMapDomain.add id access_path id_map in
-        if phys_equal id_map id_map' then astate else (actual_state, id_map')
-    | Unbind ids ->
-        let id_map' =
-          List.fold ~f:(fun acc id -> IdAccessPathMapDomain.remove id acc) ~init:id_map ids
-        in
-        if phys_equal id_map id_map' then astate else (actual_state, id_map')
-    | Instr (Call (_, Direct callee_pname, actuals, _, loc) as hil_instr)
+  let exec_instr_actual extras id_map node hil_instr actual_state =
+    match (hil_instr : HilInstr.t) with
+    | Call (_, Direct callee_pname, actuals, _, loc) as hil_instr
       when is_java_unlock callee_pname actuals ->
         (* need to be careful not to move reads/writes out of a critical section due to odd
            temporaries introduced in our translation of try/synchronized in Java. to ensure this,
@@ -70,13 +69,27 @@ struct
               TransferFunctions.exec_instr astate_acc extras node dummy_assign )
             id_map actual_state
         in
-        let actual_state'' = TransferFunctions.exec_instr actual_state' extras node hil_instr in
-        (actual_state'', IdAccessPathMapDomain.empty)
+        ( TransferFunctions.exec_instr actual_state' extras node hil_instr
+        , IdAccessPathMapDomain.empty )
+    | hil_instr ->
+        (TransferFunctions.exec_instr actual_state extras node hil_instr, id_map)
+
+
+  let exec_instr ((actual_state, id_map) as astate) extras node instr =
+    let f_resolve_id id = IdAccessPathMapDomain.find_opt id id_map in
+    let hil_translation =
+      HilInstr.of_sil ~include_array_indexes:HilConfig.include_array_indexes ~f_resolve_id instr
+    in
+    let id_map' = update_id_map hil_translation id_map in
+    let actual_state', id_map' =
+      match hil_translation with
       | Instr hil_instr ->
-        let actual_state' = TransferFunctions.exec_instr actual_state extras node hil_instr in
-        if phys_equal actual_state actual_state' then astate else (actual_state', id_map)
-    | Ignore ->
-        astate
+          exec_instr_actual extras id_map' node hil_instr actual_state
+      | Bind _ | Unbind _ | Ignore ->
+          (actual_state, id_map')
+    in
+    if phys_equal id_map id_map' && phys_equal actual_state actual_state' then astate
+    else (actual_state', id_map')
 end
 
 module MakeAbstractInterpreterWithConfig