zero alloc: assume that works with inlining

backend/cfg/cfg.ml

@@ -389,7 +389,7 @@ let print_basic' ?print_reg ppf (instruction : basic instruction) =
       next = Linear.end_instr;
       arg = instruction.arg;
       res = instruction.res;
-      dbg = [];
+      dbg = Debuginfo.none;
       fdo = None;
       live = Reg.Set.empty;
       available_before = None;

backend/checkmach.ml

@@ -95,7 +95,7 @@ module Witness = struct
           pp ppf;
           (* Show inlined locations. If dbg has only one item, it will already
              be shown as [loc]. *)
-          if List.length t.dbg > 1
+          if Debuginfo.length t.dbg > 1
           then Format.fprintf ppf " (%a)" Debuginfo.print_compact dbg;
           if not (String.equal "" component)
           then Format.fprintf ppf " on a path to %s" component;
@@ -453,7 +453,7 @@ end = struct
     Format.fprintf ppf "Annotation check for %s%s failed on function %s (%s)"
       (Printcmm.property_to_string property)
       (if t.strict then " strict" else "")
-      (fun_dbg
+      (fun_dbg |> Debuginfo.to_list
       |> List.map (fun dbg ->
              Debuginfo.(Scoped_location.string_of_scopes dbg.dinfo_scopes))
       |> String.concat ",")
@@ -915,19 +915,30 @@ end = struct
     let r = Value.join next exn in
     report t r ~msg:"transform join" ~desc dbg;
     let r = transform_diverge ~effect:effect.div r in
-    report t r ~msg:"transform_call result" ~desc dbg;
+    report t r ~msg:"transform result" ~desc dbg;
     check t r desc dbg
 
+  let transform_top t ~next ~exn w desc dbg =
+    let effect =
+      if Debuginfo.assume_zero_alloc dbg then Value.safe else Value.top w
+    in
+    transform t ~next ~exn ~effect desc dbg
+
   let transform_call t ~next ~exn callee w ~desc dbg =
     report t next ~msg:"transform_call next" ~desc dbg;
     report t exn ~msg:"transform_call exn" ~desc dbg;
-    let callee_value, new_dep = find_callee t callee dbg in
-    update_deps t callee_value new_dep w desc dbg;
-    (* Abstract witnesses of a call to the single witness for the callee name.
-       Summary of tailcall self won't be affected because it is set to Safe not
-       Top by [find_callee]. *)
-    let callee_value = Value.replace_witnesses w callee_value in
-    transform t ~next ~exn ~effect:callee_value desc dbg
+    let effect =
+      if Debuginfo.assume_zero_alloc dbg
+      then Value.safe
+      else
+        let callee_value, new_dep = find_callee t callee dbg in
+        update_deps t callee_value new_dep w desc dbg;
+        (* Abstract witnesses of a call to the single witness for the callee
+           name. Summary of tailcall self won't be affected because it is set to
+           Safe not Top by [find_callee]. *)
+        Value.replace_witnesses w callee_value
+    in
+    transform t ~next ~exn ~effect desc dbg
 
   let transform_operation t (op : Mach.operation) ~next ~exn dbg =
     match op with
@@ -968,22 +979,23 @@ end = struct
       next
     | Ialloc { mode = Alloc_heap; bytes; dbginfo } ->
       assert (not (Mach.operation_can_raise op));
-      let w = create_witnesses t (Alloc { bytes; dbginfo }) dbg in
-      let r = Value.transform w next in
-      check t r "heap allocation" dbg
+      if Debuginfo.assume_zero_alloc dbg
+      then next
+      else
+        let w = create_witnesses t (Alloc { bytes; dbginfo }) dbg in
+        let r = Value.transform w next in
+        check t r "heap allocation" dbg
     | Iprobe { name; handler_code_sym; enabled_at_init = __ } ->
       let desc = Printf.sprintf "probe %s handler %s" name handler_code_sym in
       let w = create_witnesses t (Probe { name; handler_code_sym }) dbg in
       transform_call t ~next ~exn handler_code_sym w ~desc dbg
     | Icall_ind ->
       let w = create_witnesses t Indirect_call dbg in
-      let effect = Value.top w in
-      transform t ~next ~exn ~effect "indirect call" dbg
+      transform_top t ~next ~exn w "indirect call" dbg
     | Itailcall_ind ->
       (* Sound to ignore [next] and [exn] because the call never returns. *)
       let w = create_witnesses t Indirect_tailcall dbg in
-      let effect = Value.top w in
-      transform t ~next:Value.normal_return ~exn:Value.exn_escape ~effect
+      transform_top t ~next:Value.normal_return ~exn:Value.exn_escape w
         "indirect tailcall" dbg
     | Icall_imm { func = { sym_name = func; _ } } ->
       let w = create_witnesses t (Direct_call { callee = func }) dbg in
@@ -1004,12 +1016,22 @@ end = struct
       Value.bot
     | Iextcall { func; alloc = true; _ } ->
       let w = create_witnesses t (Extcall { callee = func }) dbg in
-      let effect = Value.top w in
-      transform t ~next ~exn ~effect ("external call to " ^ func) dbg
+      transform_top t ~next ~exn w ("external call to " ^ func) dbg
     | Ispecific s ->
-      let w = create_witnesses t Arch_specific dbg in
-      transform t ~next ~exn ~effect:(S.transform_specific w s)
-        "Arch.specific_operation" dbg
+      let effect =
+        if Debuginfo.assume_zero_alloc dbg
+        then
+          (* Conservatively assume that operation can return normally. *)
+          let nor = V.Safe in
+          let exn = if Arch.operation_can_raise s then V.Safe else V.Bot in
+          (* Assume that the operation does not diverge. *)
+          let div = V.Bot in
+          { Value.nor; exn; div }
+        else
+          let w = create_witnesses t Arch_specific dbg in
+          S.transform_specific w s
+      in
+      transform t ~next ~exn ~effect "Arch.specific_operation" dbg
 
   module D = Dataflow.Backward ((Value : Dataflow.DOMAIN))
 

backend/debug/dwarf/dwarf_ocaml/dwarf_concrete_instances.ml

@@ -45,7 +45,7 @@ let for_fundecl ~get_file_id state (fundecl : L.fundecl) ~fun_end_label
   let parent = Dwarf_state.compilation_unit_proto_die state in
   let fun_name = fundecl.fun_name in
   let linkage_name =
-    match fundecl.fun_dbg with
+    match Debuginfo.to_list fundecl.fun_dbg with
     | [item] ->
       Debuginfo.Scoped_location.string_of_scopes item.dinfo_scopes
       |> remove_double_underscores

backend/emitaux.ml

@@ -209,8 +209,7 @@ let emit_frames a =
   in
   let debuginfos = Label_table.create 7 in
   let label_debuginfos rs dbg =
-    let rdbg = List.rev dbg in
-    let key = (rs, rdbg) in
+    let key = (rs, dbg) in
     try Label_table.find debuginfos key
     with Not_found ->
       let lbl = Cmm.new_label () in
@@ -287,7 +286,8 @@ let emit_frames a =
                    (add (shift_left (of_int kind) 1)
                       (of_int has_next)))))
   in
-  let emit_debuginfo (rs, rdbg) lbl =
+  let emit_debuginfo (rs, dbg) lbl =
+    let rdbg = dbg |> Debuginfo.to_list |> List.rev in
     (* Due to inlined functions, a single debuginfo may have multiple locations.
        These are represented sequentially in memory (innermost frame first),
        with the low bit of the packed debuginfo being 0 on the last entry. *)
@@ -381,6 +381,7 @@ let get_file_num ~file_emitter file_name =
 (* We only display .file if the file has not been seen before. We
    display .loc for every instruction. *)
 let emit_debug_info_gen ?discriminator dbg file_emitter loc_emitter =
+  let dbg = Debuginfo.to_list dbg in
   if is_cfi_enabled () &&
     (!Clflags.debug || Config.with_frame_pointers) then begin
     match List.rev dbg with