Skip to content

Commit 2225ebf

Browse files
Refactor and correct the "is pure" and "can raise" (port upstream PR#10354 and PR#10387) (#555)
* Refactor Proc.op_is_pure and fix Mach.operation_can_raise These two predicates test properties of Mach operations. For the standard operations, the results are independent of the target platform. For the platform-specific operations, results vary. The "is pure" predicate was implemented in a platform-specific file, $ARCH/proc.ml. The treatment of standard operations was duplicated. The "can raise" predicate was implemented in a platform-independent file, mach.ml. All specific operations were assumed not to raise, which is incorrect for ARM and ARM64 and their "shiftcheckbound" specific operation. (See #10339.) This commit refactors the two predicates as follows: - `Arch.operation_is_pure` and `Arch.operation_can_raise` predicates are added to each platform description file. They deal with specific operations only. - `Mach.operation_is_pure` was added and `Mach.operation_can_raise` was fixed to implement the test for standard operations and delegate to the Arch functions for specific operations. * Fix handling of exception-raising specific operations during spilling The ARM and ARM64 architectures have `Ishiftcheckbound` specific instructions that can raise an Invalid_argument exception. This exception can, in turn, be handled in the same function (see PR#10339 for an example). However, these specific instructions were not taken into account during insertion of spill code in asmcomp/spill.ml. The consequence is a variable that is reloaded from stack in the exception handler, yet has not been spilled to stack before. This commit fixes the issue by using the recently-fixed `Mach.operation_can_raise` predicate to handle operations during spill code insertion, instead of an ad-hoc pattern-matching. Fixes: PR#10339 * Fix handling of exception-raising specific operations during liveness analysis (#10387) This is a follow-up to 15e6354 and #10354. Use the `Mach.operation_can_raise` predicate instead of an ad-hoc pattern matching to spot operations where the variables live at entry to the enclosing exception handler must also be live. The ad-hoc pattern matching was missing the `Ishiftcheckbound` specific operations of ARM and ARM64. * Handle flambda-backend operations * Update cfg * Iprobe_is_enabled is pure * Exhaustive match * Fix after rebase * Fix arm64 after rebase and cleanup Co-authored-by: Xavier Leroy <xavier.leroy@college-de-france.fr> Co-authored-by: Xavier Leroy <xavierleroy@users.noreply.github.com>
1 parent 2d37c10 commit 2225ebf

32 files changed

+227
-194
lines changed

backend/amd64/arch.ml

+21-20
Original file line numberDiff line numberDiff line change
@@ -230,11 +230,32 @@ let print_specific_operation printreg op ppf arg =
230230
is_write (string_of_prefetch_temporal_locality_hint locality)
231231
printreg arg.(0)
232232

233+
(* Are we using the Windows 64-bit ABI? *)
233234
let win64 =
234235
match Config.system with
235236
| "win64" | "mingw64" | "cygwin" -> true
236237
| _ -> false
237238

239+
(* Specific operations that are pure *)
240+
241+
let operation_is_pure = function
242+
| Ilea _ | Ibswap _ | Isqrtf | Isextend32 | Izextend32 -> true
243+
| Ifloatarithmem _ | Ifloatsqrtf _ -> true
244+
| Ifloat_iround | Ifloat_round _ | Ifloat_min | Ifloat_max -> true
245+
| Icrc32q -> true
246+
| Irdtsc | Irdpmc | Ipause | Istore_int (_, _, _) | Ioffset_loc (_, _)
247+
| Iprefetch _ -> false
248+
249+
(* Specific operations that can raise *)
250+
251+
let operation_can_raise = function
252+
| Ilea _ | Ibswap _ | Isqrtf | Isextend32 | Izextend32
253+
| Ifloatarithmem _ | Ifloatsqrtf _
254+
| Ifloat_iround | Ifloat_round _ | Ifloat_min | Ifloat_max
255+
| Icrc32q | Irdtsc | Irdpmc | Ipause
256+
| Istore_int (_, _, _) | Ioffset_loc (_, _)
257+
| Iprefetch _ -> false
258+
238259
open X86_ast
239260

240261
(* Certain float conditions aren't represented directly in the opcode for
@@ -334,23 +355,3 @@ let equal_specific_operation left right =
334355
| Ifloat_iround | Ifloat_round _ | Ifloat_min | Ifloat_max | Ipause
335356
| Icrc32q | Iprefetch _), _ ->
336357
false
337-
338-
let is_pure_specific : specific_operation -> bool = function
339-
| Ilea _ -> true
340-
| Istore_int _ -> false
341-
| Ioffset_loc _ -> false
342-
| Ifloatarithmem _ -> false
343-
| Ibswap _ -> true
344-
| Isqrtf -> true
345-
| Ifloatsqrtf _ -> false
346-
| Ifloat_iround -> true
347-
| Ifloat_round _ -> true
348-
| Ifloat_min -> true
349-
| Ifloat_max -> true
350-
| Isextend32 -> true
351-
| Izextend32 -> true
352-
| Irdtsc -> false
353-
| Irdpmc -> false
354-
| Icrc32q -> true
355-
| Ipause -> false
356-
| Iprefetch _ -> false

backend/amd64/proc.ml

-26
Original file line numberDiff line numberDiff line change
@@ -426,32 +426,6 @@ let max_register_pressure =
426426
| Ibeginregion | Iendregion
427427
-> consumes ~int:0 ~float:0
428428

429-
(* Pure operations (without any side effect besides updating their result
430-
registers). *)
431-
432-
let op_is_pure = function
433-
| Icall_ind | Icall_imm _ | Itailcall_ind | Itailcall_imm _
434-
| Iextcall _ | Istackoffset _ | Istore _ | Ialloc _
435-
| Iintop(Icheckbound) | Iintop_imm(Icheckbound, _) | Iopaque -> false
436-
| Ibeginregion | Iendregion -> false
437-
| Ispecific(Ipause)
438-
| Ispecific(Iprefetch _) -> false
439-
| Ispecific(Ilea _ | Isextend32 | Izextend32 | Ifloat_iround | Ifloat_round _
440-
| Ifloat_min | Ifloat_max) -> true
441-
| Ispecific(Irdtsc | Irdpmc | Icrc32q | Istore_int (_, _, _)
442-
| Ioffset_loc (_, _) | Ifloatarithmem (_, _)
443-
| Ibswap _ | Ifloatsqrtf _ | Isqrtf)-> false
444-
| Iprobe _ | Iprobe_is_enabled _-> false
445-
| Iintop(Iadd | Isub | Imul | Imulh _ | Idiv | Imod | Iand | Ior | Ixor
446-
| Ilsl | Ilsr | Iasr | Ipopcnt | Iclz _|Ictz _|Icomp _)
447-
| Iintop_imm((Iadd | Isub | Imul | Imulh _ | Idiv | Imod | Iand | Ior | Ixor
448-
| Ilsl | Ilsr | Iasr | Ipopcnt | Iclz _|Ictz _|Icomp _), _)
449-
| Imove | Ispill | Ireload | Inegf | Iabsf | Iaddf | Isubf | Imulf | Idivf
450-
| Icompf _
451-
| Ifloatofint | Iintoffloat | Iconst_int _ | Iconst_float _ | Iconst_symbol _
452-
| Iload (_, _, _) | Iname_for_debugger _
453-
-> true
454-
455429
(* Layout of the stack frame *)
456430

457431
let frame_required ~fun_contains_calls ~fun_num_stack_slots =

backend/arm64/arch.ml

+24-1
Original file line numberDiff line numberDiff line change
@@ -301,7 +301,9 @@ let logical_imm_length x =
301301
let is_logical_immediate x =
302302
x <> 0n && x <> -1n && run_automata (logical_imm_length x) 0 x
303303

304-
let is_pure_specific : specific_operation -> bool = function
304+
(* Specific operations that are pure *)
305+
306+
let operation_is_pure : specific_operation -> bool = function
305307
| Ifar_alloc _ -> false
306308
| Ifar_intop_checkbound -> false
307309
| Ifar_intop_imm_checkbound _ -> false
@@ -319,3 +321,24 @@ let is_pure_specific : specific_operation -> bool = function
319321
| Ibswap _ -> true
320322
| Imove32 -> true
321323
| Isignext _ -> true
324+
325+
(* Specific operations that can raise *)
326+
327+
let operation_can_raise = function
328+
| Ifar_alloc _
329+
| Ifar_intop_checkbound
330+
| Ifar_intop_imm_checkbound _
331+
| Ishiftcheckbound _
332+
| Ifar_shiftcheckbound _ -> true
333+
| Imuladd
334+
| Imulsub
335+
| Inegmulf
336+
| Imuladdf
337+
| Inegmuladdf
338+
| Imulsubf
339+
| Inegmulsubf
340+
| Isqrtf
341+
| Imove32
342+
| Ishiftarith (_, _)
343+
| Isignext _
344+
| Ibswap _ -> false

backend/arm64/proc.ml

-11
Original file line numberDiff line numberDiff line change
@@ -293,17 +293,6 @@ let max_register_pressure = function
293293
| Iload(Single, _, _) | Istore(Single, _, _) -> [| 23; 31 |]
294294
| _ -> [| 23; 32 |]
295295

296-
(* Pure operations (without any side effect besides updating their result
297-
registers). *)
298-
299-
let op_is_pure = function
300-
| Icall_ind | Icall_imm _ | Itailcall_ind | Itailcall_imm _
301-
| Iextcall _ | Istackoffset _ | Istore _ | Ialloc _
302-
| Iintop(Icheckbound) | Iintop_imm(Icheckbound, _) | Iopaque
303-
| Ibeginregion | Iendregion
304-
| Ispecific(Ishiftcheckbound _) -> false
305-
| _ -> true
306-
307296
(* Layout of the stack *)
308297
let frame_required ~fun_contains_calls ~fun_num_stack_slots =
309298
fun_contains_calls

backend/cfg/cfg.ml

+3-3
Original file line numberDiff line numberDiff line change
@@ -323,8 +323,8 @@ let can_raise_operation : operation -> bool = function
323323
| Floatofint -> false
324324
| Intoffloat -> false
325325
| Probe _ -> true
326-
| Probe_is_enabled _ -> false (* CR xclerc for xclerc: double check *)
327-
| Specific _ -> false (* CR xclerc for xclerc: double check *)
326+
| Probe_is_enabled _ -> true
327+
| Specific op -> Arch.operation_can_raise op
328328
| Opaque -> false
329329
| Name_for_debugger _ -> false
330330
| Begin_region -> false
@@ -375,7 +375,7 @@ let is_pure_operation : operation -> bool = function
375375
| Opaque -> false
376376
| Begin_region -> false
377377
| End_region -> false
378-
| Specific s -> Arch.is_pure_specific s
378+
| Specific s -> Arch.operation_is_pure s
379379
| Name_for_debugger _ -> true
380380

381381
let is_pure_basic : basic -> bool = function

backend/deadcode.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ let rec deadcode i =
4343
{ i; regs; exits = Int.Set.empty; }
4444
| Iop op ->
4545
let s = deadcode i.next in
46-
if Proc.op_is_pure op (* no side effects *)
46+
if operation_is_pure op (* no side effects *)
4747
&& Reg.disjoint_set_array s.regs i.res (* results are not used after *)
4848
&& not (Proc.regs_are_volatile i.arg) (* no stack-like hard reg *)
4949
&& not (Proc.regs_are_volatile i.res) (* is involved *)

backend/liveness.ml

+9-17
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,7 @@ let rec live env i finally =
101101
Reg.set_of_array i.arg
102102
| Iop op ->
103103
let after = live env i.next finally in
104-
if Proc.op_is_pure op (* no side effects *)
104+
if operation_is_pure op (* no side effects *)
105105
&& Reg.disjoint_set_array after i.res (* results are not used after *)
106106
&& not (Proc.regs_are_volatile i.arg) (* no stack-like hard reg *)
107107
&& not (Proc.regs_are_volatile i.res) (* is involved *)
@@ -112,22 +112,14 @@ let rec live env i finally =
112112
end else begin
113113
let across_after = Reg.diff_set_array after i.res in
114114
let across =
115-
match op with
116-
| Iextcall { returns = false; _ } ->
117-
(* extcalls that never return can raise an exception *)
118-
env.at_raise
119-
| Icall_ind | Icall_imm _ | Iextcall _ | Ialloc _
120-
| Iprobe _
121-
| Iintop (Icheckbound) | Iintop_imm(Icheckbound, _) ->
122-
(* The function call may raise an exception, branching to the
123-
nearest enclosing try ... with. Similarly for bounds checks,
124-
probes and allocation (for the latter: finalizers may throw
125-
exceptions, as may signal handlers).
126-
Hence, everything that must be live at the beginning of
127-
the exception handler must also be live across this instr. *)
128-
Reg.Set.union across_after env.at_raise
129-
| _ ->
130-
across_after in
115+
(* Operations that can raise an exception (function calls,
116+
bounds checks, allocations) can branch to the
117+
nearest enclosing try ... with.
118+
Hence, everything that must be live at the beginning of
119+
the exception handler must also be live across this instr. *)
120+
if operation_can_raise op
121+
then Reg.Set.union across_after env.at_raise
122+
else across_after in
131123
i.live <- across;
132124
Reg.add_set_array across i.arg
133125
end

backend/mach.ml

+32-1
Original file line numberDiff line numberDiff line change
@@ -181,13 +181,44 @@ let rec instr_iter f i =
181181
| Ibeginregion | Iendregion) ->
182182
instr_iter f i.next
183183

184+
let operation_is_pure = function
185+
| Icall_ind | Icall_imm _ | Itailcall_ind | Itailcall_imm _
186+
| Iextcall _ | Istackoffset _ | Istore _ | Ialloc _
187+
| Iintop(Icheckbound) | Iintop_imm(Icheckbound, _) | Iopaque -> false
188+
| Ibeginregion | Iendregion -> false
189+
| Iprobe _ -> false
190+
| Iprobe_is_enabled _-> true
191+
| Ispecific sop -> Arch.operation_is_pure sop
192+
| Iintop_imm((Iadd | Isub | Imul | Imulh _ | Idiv | Imod | Iand | Ior | Ixor
193+
| Ilsl | Ilsr | Iasr | Ipopcnt | Iclz _|Ictz _|Icomp _), _)
194+
| Iintop(Iadd | Isub | Imul | Imulh _ | Idiv | Imod | Iand | Ior | Ixor
195+
| Ilsl | Ilsr | Iasr | Ipopcnt | Iclz _|Ictz _|Icomp _)
196+
| Imove | Ispill | Ireload | Inegf | Iabsf | Iaddf | Isubf | Imulf | Idivf
197+
| Icompf _
198+
| Ifloatofint | Iintoffloat | Iconst_int _ | Iconst_float _ | Iconst_symbol _
199+
| Iload (_, _, _) | Iname_for_debugger _
200+
-> true
201+
202+
184203
let operation_can_raise op =
185204
match op with
186205
| Icall_ind | Icall_imm _ | Iextcall _
187206
| Iintop (Icheckbound) | Iintop_imm (Icheckbound, _)
188207
| Iprobe _
189208
| Ialloc _ -> true
190-
| _ -> false
209+
| Ispecific sop -> Arch.operation_can_raise sop
210+
| Iintop_imm((Iadd | Isub | Imul | Imulh _ | Idiv | Imod | Iand | Ior | Ixor
211+
| Ilsl | Ilsr | Iasr | Ipopcnt | Iclz _|Ictz _|Icomp _), _)
212+
| Iintop(Iadd | Isub | Imul | Imulh _ | Idiv | Imod | Iand | Ior | Ixor
213+
| Ilsl | Ilsr | Iasr | Ipopcnt | Iclz _|Ictz _|Icomp _)
214+
| Imove | Ispill | Ireload | Inegf | Iabsf | Iaddf | Isubf | Imulf | Idivf
215+
| Icompf _
216+
| Ifloatofint | Iintoffloat | Iconst_int _ | Iconst_float _ | Iconst_symbol _
217+
| Istackoffset _ | Istore _ | Iload (_, _, _) | Iname_for_debugger _
218+
| Itailcall_imm _ | Itailcall_ind
219+
| Iopaque | Ibeginregion | Iendregion
220+
| Iprobe_is_enabled _
221+
-> false
191222

192223
let free_conts_for_handlers fundecl =
193224
let module S = Numbers.Int.Set in

backend/mach.mli

+7
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,14 @@ val instr_cons_debug:
130130
instruction -> instruction
131131
val instr_iter: (instruction -> unit) -> instruction -> unit
132132

133+
val operation_is_pure : operation -> bool
134+
(** Returns [true] if the given operation only produces a result
135+
in its destination registers, but has no side effects whatsoever:
136+
it doesn't raise exceptions, it doesn't modify already-allocated
137+
blocks, it doesn't adjust the stack frame, etc. *)
138+
133139
val operation_can_raise : operation -> bool
140+
(** Returns [true] if the given operation can raise an exception. *)
134141

135142
val free_conts_for_handlers : fundecl -> Numbers.Int.Set.t Numbers.Int.Map.t
136143
val equal_trap_stack : trap_stack -> trap_stack -> bool

backend/proc.mli

-3
Original file line numberDiff line numberDiff line change
@@ -58,9 +58,6 @@ val destroyed_at_reloadretaddr : Reg.t array
5858
(* Volatile registers: those that change value when read *)
5959
val regs_are_volatile: Reg.t array -> bool
6060

61-
(* Pure operations *)
62-
val op_is_pure: Mach.operation -> bool
63-
6461
(* Info for laying out the stack frame *)
6562
val frame_required :
6663
fun_contains_calls:bool ->

backend/spill.ml

+4-8
Original file line numberDiff line numberDiff line change
@@ -494,17 +494,13 @@ let rec spill :
494494
let before1 = Reg.diff_set_array after i.res in
495495
k (instr_cons i.desc i.arg i.res new_next)
496496
(Reg.add_set_array before1 i.res))
497-
| Iop _ ->
497+
| Iop op ->
498498
spill env i.next finally (fun new_next after ->
499499
let before1 = Reg.diff_set_array after i.res in
500500
let before =
501-
match i.desc with
502-
Iop Icall_ind | Iop(Icall_imm _) | Iop(Iextcall _) | Iop(Ialloc _)
503-
| Iop(Iintop Icheckbound) | Iop(Iintop_imm(Icheckbound, _))
504-
| Iop (Iprobe _) ->
505-
Reg.Set.union before1 env.at_raise
506-
| _ ->
507-
before1 in
501+
if operation_can_raise op
502+
then Reg.Set.union before1 env.at_raise
503+
else before1 in
508504
k (instr_cons_debug i.desc i.arg i.res i.dbg
509505
(add_spills env (Reg.inter_set_array after i.res) new_next))
510506
before)

ocaml/asmcomp/amd64/arch.ml

+13
Original file line numberDiff line numberDiff line change
@@ -134,7 +134,20 @@ let print_specific_operation printreg op ppf arg =
134134
| Izextend32 ->
135135
fprintf ppf "zextend32 %a" printreg arg.(0)
136136

137+
(* Are we using the Windows 64-bit ABI? *)
138+
137139
let win64 =
138140
match Config.system with
139141
| "win64" | "mingw64" | "cygwin" -> true
140142
| _ -> false
143+
144+
(* Specific operations that are pure *)
145+
146+
let operation_is_pure = function
147+
| Ilea _ | Ibswap _ | Isqrtf | Isextend32 | Izextend32 -> true
148+
| Ifloatarithmem _ | Ifloatsqrtf _ -> true
149+
| _ -> false
150+
151+
(* Specific operations that can raise *)
152+
153+
let operation_can_raise _ = false

ocaml/asmcomp/amd64/proc.ml

-13
Original file line numberDiff line numberDiff line change
@@ -360,19 +360,6 @@ let max_register_pressure = function
360360
if fp then [| 12; 15 |] else [| 13; 15 |]
361361
| _ -> if fp then [| 12; 16 |] else [| 13; 16 |]
362362

363-
(* Pure operations (without any side effect besides updating their result
364-
registers). *)
365-
366-
let op_is_pure = function
367-
| Icall_ind | Icall_imm _ | Itailcall_ind | Itailcall_imm _
368-
| Iextcall _ | Istackoffset _ | Istore _ | Ialloc _
369-
| Iintop(Icheckbound) | Iintop_imm(Icheckbound, _) | Iopaque -> false
370-
| Ispecific(Ilea _|Isextend32|Izextend32) -> true
371-
| Ispecific _ -> false
372-
| Iprobe _ | Iprobe_is_enabled _-> false
373-
| Ibeginregion | Iendregion -> false
374-
| _ -> true
375-
376363
(* Layout of the stack frame *)
377364

378365
let frame_required fd =

ocaml/asmcomp/arm/arch.ml

+12
Original file line numberDiff line numberDiff line change
@@ -262,3 +262,15 @@ let is_immediate n =
262262
s := !s + 2
263263
done;
264264
!s <= m
265+
266+
(* Specific operations that are pure *)
267+
268+
let operation_is_pure = function
269+
| Ishiftcheckbound _ -> false
270+
| _ -> true
271+
272+
(* Specific operations that can raise *)
273+
274+
let operation_can_raise = function
275+
| Ishiftcheckbound _ -> true
276+
| _ -> false

ocaml/asmcomp/arm/proc.ml

-10
Original file line numberDiff line numberDiff line change
@@ -340,16 +340,6 @@ let max_register_pressure = function
340340
| Iintop Imulh when !arch < ARMv6 -> [| 8; 16; 32 |]
341341
| _ -> [| 9; 16; 32 |]
342342

343-
(* Pure operations (without any side effect besides updating their result
344-
registers). *)
345-
346-
let op_is_pure = function
347-
| Icall_ind | Icall_imm _ | Itailcall_ind | Itailcall_imm _
348-
| Iextcall _ | Istackoffset _ | Istore _ | Ialloc _
349-
| Iintop(Icheckbound) | Iintop_imm(Icheckbound, _) | Iopaque
350-
| Ispecific(Ishiftcheckbound _) -> false
351-
| _ -> true
352-
353343
(* Layout of the stack *)
354344

355345
let frame_required fd =

0 commit comments

Comments
 (0)