Zero alloc: assume that works with inlining - propagate via Scoped_location

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 Debuginfo.length t.dbg > 1
+          if Debuginfo.Dbg.length (Debuginfo.get_dbg 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 |> Debuginfo.to_list
+      (fun_dbg |> Debuginfo.get_dbg |> Debuginfo.Dbg.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 Debuginfo.to_list fundecl.fun_dbg with
+    match Debuginfo.Dbg.to_list (Debuginfo.get_dbg fundecl.fun_dbg) with
     | [item] ->
       Debuginfo.Scoped_location.string_of_scopes item.dinfo_scopes
       |> remove_double_underscores

backend/emitaux.ml

@@ -127,14 +127,16 @@ type frame_descr =
 
 let frame_descriptors = ref([] : frame_descr list)
 
+let is_none_dbg d = Debuginfo.Dbg.is_none (Debuginfo.get_dbg d)
+
 let get_flags debuginfo =
   match debuginfo with
   | Dbg_other d | Dbg_raise d ->
-    if Debuginfo.is_none d then 0 else 1
+    if is_none_dbg d then 0 else 1
   | Dbg_alloc dbgs ->
     if !Clflags.debug &&
        List.exists (fun d ->
-         not (Debuginfo.is_none d.Debuginfo.alloc_dbg)) dbgs
+         not (is_none_dbg d.Debuginfo.alloc_dbg)) dbgs
     then 3 else 2
 
 let is_long n =
@@ -198,17 +200,18 @@ let emit_frames a =
   in
   let module Label_table =
     Hashtbl.Make (struct
-      type t = bool * Debuginfo.t
+      type t = bool * Debuginfo.Dbg.t
 
       let equal ((rs1 : bool), dbg1) (rs2, dbg2) =
-        rs1 = rs2 && Debuginfo.compare dbg1 dbg2 = 0
+        rs1 = rs2 && Debuginfo.Dbg.compare dbg1 dbg2 = 0
 
       let hash (rs, dbg) =
-        Hashtbl.hash (rs, Debuginfo.hash dbg)
+        Hashtbl.hash (rs, Debuginfo.Dbg.hash dbg)
     end)
   in
   let debuginfos = Label_table.create 7 in
   let label_debuginfos rs dbg =
+    let dbg = Debuginfo.get_dbg dbg in
     let key = (rs, dbg) in
     try Label_table.find debuginfos key
     with Not_found ->
@@ -253,7 +256,7 @@ let emit_frames a =
       if flags = 3 then begin
         a.efa_align 4;
         List.iter (fun Debuginfo.{alloc_dbg; _} ->
-          if Debuginfo.is_none alloc_dbg then
+          if is_none_dbg alloc_dbg then
             a.efa_32 Int32.zero
           else
             a.efa_label_rel (label_debuginfos false alloc_dbg) Int32.zero) dbg
@@ -287,7 +290,7 @@ let emit_frames a =
                       (of_int has_next)))))
   in
   let emit_debuginfo (rs, dbg) lbl =
-    let rdbg = dbg |> Debuginfo.to_list |> List.rev in
+    let rdbg = dbg |> Debuginfo.Dbg.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,7 +384,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
+  let dbg = Debuginfo.Dbg.to_list (Debuginfo.get_dbg dbg) in
   if is_cfi_enabled () &&
     (!Clflags.debug || Config.with_frame_pointers) then begin
     match List.rev dbg with

backend/fdo_info.ml

@@ -28,7 +28,7 @@ let create ~dbg ~discriminator =
     }
 
 let equal_info left right =
-  Debuginfo.compare left.dbg right.dbg = 0
+  Debuginfo.(Dbg.compare (get_dbg left.dbg) (get_dbg right.dbg) = 0)
   && Int.equal left.discriminator right.discriminator
 
 let equal left right =

ocaml/asmcomp/emitaux.ml

@@ -166,17 +166,18 @@ let emit_frames a =
   in
   let module Label_table =
     Hashtbl.Make (struct
-      type t = bool * Debuginfo.t
+      type t = bool * Debuginfo.Dbg.t
 
       let equal ((rs1 : bool), dbg1) (rs2, dbg2) =
-        rs1 = rs2 && Debuginfo.compare dbg1 dbg2 = 0
+        rs1 = rs2 && Debuginfo.Dbg.compare dbg1 dbg2 = 0
 
       let hash (rs, dbg) =
-        Hashtbl.hash (rs, Debuginfo.hash dbg)
+        Hashtbl.hash (rs, Debuginfo.Dbg.hash dbg)
     end)
   in
   let debuginfos = Label_table.create 7 in
   let label_debuginfos rs dbg =
+    let dbg = Debuginfo.get_dbg dbg in
     let key = (rs, dbg) in
     try Label_table.find debuginfos key
     with Not_found ->
@@ -190,16 +191,17 @@ let emit_frames a =
     then a.efa_16 n
     else raise (Error(Stack_frame_too_large n))
   in
+  let is_none_dbg d = Debuginfo.Dbg.is_none (Debuginfo.get_dbg d) in
   let emit_frame fd =
     assert (fd.fd_frame_size land 3 = 0);
     let flags =
       match fd.fd_debuginfo with
       | Dbg_other d | Dbg_raise d ->
-        if Debuginfo.is_none d then 0 else 1
+        if is_none_dbg d then 0 else 1
       | Dbg_alloc dbgs ->
         if !Clflags.debug &&
            List.exists (fun d ->
-             not (Debuginfo.is_none d.Debuginfo.alloc_dbg)) dbgs
+             not (is_none_dbg d.Debuginfo.alloc_dbg)) dbgs
         then 3 else 2
     in
     a.efa_label_rel fd.fd_lbl 0l;
@@ -227,7 +229,7 @@ let emit_frames a =
       if flags = 3 then begin
         a.efa_align 4;
         List.iter (fun Debuginfo.{alloc_dbg; _} ->
-          if Debuginfo.is_none alloc_dbg then
+          if is_none_dbg alloc_dbg then
             a.efa_32 Int32.zero
           else
             a.efa_label_rel (label_debuginfos false alloc_dbg) Int32.zero) dbg
@@ -261,7 +263,7 @@ let emit_frames a =
                       (of_int has_next)))))
   in
   let emit_debuginfo (rs, dbg) lbl =
-    let rdbg = dbg |> Debuginfo.to_list |> List.rev in
+    let rdbg = dbg |> Debuginfo.Dbg.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. *)
@@ -346,7 +348,7 @@ let reset_debug_info () =
 (* We only display .file if the file has not been seen before. We
    display .loc for every instruction. *)
 let emit_debug_info_gen dbg file_emitter loc_emitter =
-  let dbg = Debuginfo.to_list dbg in
+  let dbg = Debuginfo.Dbg.to_list (Debuginfo.get_dbg dbg) in
   if is_cfi_enabled () &&
     (!Clflags.debug || Config.with_frame_pointers) then begin
     match List.rev dbg with