Skip to content

Instantly share code, notes, and snippets.

@katrinafyi

katrinafyi/aarch64_float_arithmetic_max_min.ml

Created September 10, 2025 06:47
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save katrinafyi/17da7ec1e6439634634853bf083b16ef to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save katrinafyi/17da7ec1e6439634634853bf083b16ef to your computer and use it in GitHub Desktop.
Download ZIP
Raw
aarch64_float_arithmetic_max_min.ml
(* AUTO-GENERATED LIFTER FILE *)
open Offline_utils
let f_aarch64_float_arithmetic_max_min v_enc v_pc : unit =
begin
let v_result__1_copyprop = ref (undefined ()) in
let v_Exp13__2 = f_decl_bv ("Exp13__2") (Z.of_string "32") in
let v_Exp15__2 = f_decl_bv ("Exp15__2") (Z.of_string "32") in
let v_Exp17__2 = f_decl_bv ("Exp17__2") (Z.of_string "32") in
let v_Exp19__2 = f_decl_bv ("Exp19__2") (Z.of_string "32") in
let v_result__1_1_copyprop = ref (undefined ()) in
let v_Exp35__2 = f_decl_bv ("Exp35__2") (Z.of_string "64") in
let v_Exp37__2 = f_decl_bv ("Exp37__2") (Z.of_string "64") in
let v_Exp39__2 = f_decl_bv ("Exp39__2") (Z.of_string "64") in
let v_Exp41__2 = f_decl_bv ("Exp41__2") (Z.of_string "64") in
let v_result__1_2_copyprop = ref (undefined ()) in
let v_Exp59__2 = f_decl_bv ("Exp59__2") (Z.of_string "16") in
let v_Exp61__2 = f_decl_bv ("Exp61__2") (Z.of_string "16") in
let v_Exp63__2 = f_decl_bv ("Exp63__2") (Z.of_string "16") in
let v_Exp65__2 = f_decl_bv ("Exp65__2") (Z.of_string "16") in
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000110000000000000000000000")) (from_bitsLit "00000000000000000000000000000000") then
begin
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000000000000000000") then
begin
v_result__1_copyprop := f_gen_load (v_Exp13__2)
end
else
begin
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000001000000000000") then
begin
v_result__1_copyprop := f_gen_load (v_Exp15__2)
end
else
begin
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000010000000000000") then
begin
v_result__1_copyprop := f_gen_load (v_Exp17__2)
end
else
begin
v_result__1_copyprop := f_gen_load (v_Exp19__2)
end
end
end
end
else
begin
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000110000000000000000000000")) (from_bitsLit "00000000010000000000000000000000") then
begin
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000000000000000000") then
begin
v_result__1_1_copyprop := f_gen_load (v_Exp35__2)
end
else
begin
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000001000000000000") then
begin
v_result__1_1_copyprop := f_gen_load (v_Exp37__2)
end
else
begin
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000010000000000000") then
begin
v_result__1_1_copyprop := f_gen_load (v_Exp39__2)
end
else
begin
v_result__1_1_copyprop := f_gen_load (v_Exp41__2)
end
end
end
end
else
begin
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000000000000000000") then
begin
v_result__1_2_copyprop := f_gen_load (v_Exp59__2)
end
else
begin
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000001000000000000") then
begin
v_result__1_2_copyprop := f_gen_load (v_Exp61__2)
end
else
begin
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000010000000000000") then
begin
v_result__1_2_copyprop := f_gen_load (v_Exp63__2)
end
else
begin
v_result__1_2_copyprop := f_gen_load (v_Exp65__2)
end
end
end
end
end;
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000110000000000000000000000")) (from_bitsLit "00000000000000000000000000000000") then
(List.flatten [
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000000000000000000") then
f_gen_store (v_Exp13__2) (f_gen_FPMax (Z.of_string "32") (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "5") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "32")) (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "16") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "32")) (f_gen_load (v_FPCR)))
else
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000001000000000000") then
f_gen_store (v_Exp15__2) (f_gen_FPMin (Z.of_string "32") (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "5") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "32")) (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "16") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "32")) (f_gen_load (v_FPCR)))
else
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000010000000000000") then
f_gen_store (v_Exp17__2) (f_gen_FPMaxNum (Z.of_string "32") (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "5") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "32")) (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "16") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "32")) (f_gen_load (v_FPCR)))
else
f_gen_store (v_Exp19__2) (f_gen_FPMinNum (Z.of_string "32") (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "5") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "32")) (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "16") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "32")) (f_gen_load (v_FPCR)));
f_gen_array_store (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "0") (Z.of_string "5"))) (f_gen_ZeroExtend (Z.of_string "32") (Z.of_string "128") (!v_result__1_copyprop) (f_gen_int_lit (Z.of_string "128")))
])
else
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000110000000000000000000000")) (from_bitsLit "00000000010000000000000000000000") then
(List.flatten [
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000000000000000000") then
f_gen_store (v_Exp35__2) (f_gen_FPMax (Z.of_string "64") (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "5") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "64")) (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "16") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "64")) (f_gen_load (v_FPCR)))
else
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000001000000000000") then
f_gen_store (v_Exp37__2) (f_gen_FPMin (Z.of_string "64") (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "5") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "64")) (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "16") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "64")) (f_gen_load (v_FPCR)))
else
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000010000000000000") then
f_gen_store (v_Exp39__2) (f_gen_FPMaxNum (Z.of_string "64") (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "5") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "64")) (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "16") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "64")) (f_gen_load (v_FPCR)))
else
f_gen_store (v_Exp41__2) (f_gen_FPMinNum (Z.of_string "64") (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "5") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "64")) (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "16") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "64")) (f_gen_load (v_FPCR)));
f_gen_array_store (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "0") (Z.of_string "5"))) (f_gen_ZeroExtend (Z.of_string "64") (Z.of_string "128") (!v_result__1_1_copyprop) (f_gen_int_lit (Z.of_string "128")))
])
else
(List.flatten [
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000000000000000000") then
f_gen_store (v_Exp59__2) (f_gen_FPMax (Z.of_string "16") (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "5") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "16")) (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "16") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "16")) (f_gen_load (v_FPCR)))
else
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000001000000000000") then
f_gen_store (v_Exp61__2) (f_gen_FPMin (Z.of_string "16") (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "5") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "16")) (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "16") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "16")) (f_gen_load (v_FPCR)))
else
if f_eq_bits (Z.of_string "32") (f_and_bits (Z.of_string "32") (v_enc) (from_bitsLit "00000000000000000011000000000000")) (from_bitsLit "00000000000000000010000000000000") then
f_gen_store (v_Exp63__2) (f_gen_FPMaxNum (Z.of_string "16") (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "5") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "16")) (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "16") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "16")) (f_gen_load (v_FPCR)))
else
f_gen_store (v_Exp65__2) (f_gen_FPMinNum (Z.of_string "16") (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "5") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "16")) (f_gen_slice (f_gen_array_load (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "16") (Z.of_string "5")))) (Z.of_string "0") (Z.of_string "16")) (f_gen_load (v_FPCR)));
f_gen_array_store (v__Z) (f_cvt_bits_uint (Z.of_string "5") (extract_bits (v_enc) (Z.of_string "0") (Z.of_string "5"))) (f_gen_ZeroExtend (Z.of_string "16") (Z.of_string "128") (!v_result__1_2_copyprop) (f_gen_int_lit (Z.of_string "128")))
])
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment