Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit 320c5559 authored by Xavier Leroy's avatar Xavier Leroy Committed by Xavier Leroy
Browse files

Support __builtin_unreachable

Not yet used for optimizations.
parent 38b0babd
...@@ -355,8 +355,12 @@ let expand_builtin_inline name args res = ...@@ -355,8 +355,12 @@ let expand_builtin_inline name args res =
(* Synchronization *) (* Synchronization *)
| "__builtin_membar", [], _ -> | "__builtin_membar", [], _ ->
() ()
(* No operation *)
| "__builtin_nop", [], _ -> | "__builtin_nop", [], _ ->
emit Pnop emit Pnop
(* Optimization hint *)
| "__builtin_unreachable", [], _ ->
()
(* Byte swap *) (* Byte swap *)
| ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) -> | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
emit (Prev(W, res, a1)) emit (Prev(W, res, a1))
......
...@@ -407,8 +407,12 @@ let expand_builtin_inline name args res = ...@@ -407,8 +407,12 @@ let expand_builtin_inline name args res =
(* Vararg stuff *) (* Vararg stuff *)
| "__builtin_va_start", [BA(IR a)], _ -> | "__builtin_va_start", [BA(IR a)], _ ->
expand_builtin_va_start a expand_builtin_va_start a
(* No operation *)
| "__builtin_nop", [], _ -> | "__builtin_nop", [], _ ->
emit Pnop emit Pnop
(* Optimization hint *)
| "__builtin_unreachable", [], _ ->
()
(* Catch-all *) (* Catch-all *)
| _ -> | _ ->
raise (Error ("unrecognized builtin " ^ name)) raise (Error ("unrecognized builtin " ^ name))
......
...@@ -268,6 +268,9 @@ let builtins_generic = { ...@@ -268,6 +268,9 @@ let builtins_generic = {
(TPtr(TVoid [], []), (TPtr(TVoid [], []),
[TPtr(TVoid [], []); TInt(IULong, [])], [TPtr(TVoid [], []); TInt(IULong, [])],
false); false);
(* Optimization hints *)
"__builtin_unreachable",
(TVoid [], [], false);
(* Helper functions for int64 arithmetic *) (* Helper functions for int64 arithmetic *)
"__compcert_i64_dtos", "__compcert_i64_dtos",
(TInt(ILongLong, []), (TInt(ILongLong, []),
......
...@@ -341,6 +341,7 @@ Inductive standard_builtin : Type := ...@@ -341,6 +341,7 @@ Inductive standard_builtin : Type :=
| BI_i16_bswap | BI_i16_bswap
| BI_i32_bswap | BI_i32_bswap
| BI_i64_bswap | BI_i64_bswap
| BI_unreachable
| BI_i64_umulh | BI_i64_umulh
| BI_i64_smulh | BI_i64_smulh
| BI_i64_sdiv | BI_i64_sdiv
...@@ -376,6 +377,7 @@ Definition standard_builtin_table : list (string * standard_builtin) := ...@@ -376,6 +377,7 @@ Definition standard_builtin_table : list (string * standard_builtin) :=
:: ("__builtin_bswap", BI_i32_bswap) :: ("__builtin_bswap", BI_i32_bswap)
:: ("__builtin_bswap32", BI_i32_bswap) :: ("__builtin_bswap32", BI_i32_bswap)
:: ("__builtin_bswap64", BI_i64_bswap) :: ("__builtin_bswap64", BI_i64_bswap)
:: ("__builtin_unreachable", BI_unreachable)
:: ("__compcert_i64_umulh", BI_i64_umulh) :: ("__compcert_i64_umulh", BI_i64_umulh)
:: ("__compcert_i64_smulh", BI_i64_smulh) :: ("__compcert_i64_smulh", BI_i64_smulh)
:: ("__compcert_i64_sdiv", BI_i64_sdiv) :: ("__compcert_i64_sdiv", BI_i64_sdiv)
...@@ -414,6 +416,8 @@ Definition standard_builtin_sig (b: standard_builtin) : signature := ...@@ -414,6 +416,8 @@ Definition standard_builtin_sig (b: standard_builtin) : signature :=
mksignature (Tlong :: nil) Tlong cc_default mksignature (Tlong :: nil) Tlong cc_default
| BI_i16_bswap => | BI_i16_bswap =>
mksignature (Tint :: nil) Tint cc_default mksignature (Tint :: nil) Tint cc_default
| BI_unreachable =>
mksignature nil Tvoid cc_default
| BI_i64_shl | BI_i64_shr | BI_i64_sar => | BI_i64_shl | BI_i64_shr | BI_i64_sar =>
mksignature (Tlong :: Tint :: nil) Tlong cc_default mksignature (Tlong :: Tint :: nil) Tlong cc_default
| BI_i64_dtos | BI_i64_dtou => | BI_i64_dtos | BI_i64_dtou =>
...@@ -448,6 +452,7 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig ...@@ -448,6 +452,7 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig
| BI_i64_bswap => | BI_i64_bswap =>
mkbuiltin_n1t Tlong Tlong mkbuiltin_n1t Tlong Tlong
(fun n => Int64.repr (decode_int (List.rev (encode_int 8%nat (Int64.unsigned n))))) (fun n => Int64.repr (decode_int (List.rev (encode_int 8%nat (Int64.unsigned n)))))
| BI_unreachable => mkbuiltin Tvoid (fun vargs => None) _ _
| BI_i64_umulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu | BI_i64_umulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu
| BI_i64_smulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs | BI_i64_smulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs
| BI_i64_sdiv => mkbuiltin_v2p Tlong Val.divls _ _ | BI_i64_sdiv => mkbuiltin_v2p Tlong Val.divls _ _
......
...@@ -23,8 +23,12 @@ open Cutil ...@@ -23,8 +23,12 @@ open Cutil
module StringSet = Set.Make(String) module StringSet = Set.Make(String)
(* Functions declared noreturn by the standard *) (* Functions declared noreturn by the standard *)
(* We also add our own "__builtin_unreachable" function because, currently,
it is difficult to attach attributes to a built-in function. *)
let std_noreturn_functions = let std_noreturn_functions =
["longjmp";"exit";"_exit";"abort";"_Exit";"quick_exit";"thrd_exit"] ["longjmp";"exit";"_exit";"abort";"_Exit";"quick_exit";"thrd_exit";
"__builtin_unreachable"]
(* Statements are abstracted as "flow transformers": (* Statements are abstracted as "flow transformers":
functions from possible inputs to possible outcomes. functions from possible inputs to possible outcomes.
......
...@@ -793,6 +793,9 @@ let expand_builtin_inline name args res = ...@@ -793,6 +793,9 @@ let expand_builtin_inline name args res =
(* no operation *) (* no operation *)
| "__builtin_nop", [], _ -> | "__builtin_nop", [], _ ->
emit (Pori (GPR0, GPR0, Cint _0)) emit (Pori (GPR0, GPR0, Cint _0))
(* Optimization hint *)
| "__builtin_unreachable", [], _ ->
()
(* atomic operations *) (* atomic operations *)
| "__builtin_atomic_exchange", [BA (IR a1); BA (IR a2); BA (IR a3)],_ -> | "__builtin_atomic_exchange", [BA (IR a1); BA (IR a2); BA (IR a3)],_ ->
(* Register constraints imposed by Machregs.v *) (* Register constraints imposed by Machregs.v *)
......
...@@ -646,8 +646,12 @@ let expand_builtin_inline name args res = ...@@ -646,8 +646,12 @@ let expand_builtin_inline name args res =
(fun rl -> (fun rl ->
emit (Pmulw (rl, X a, X b)); emit (Pmulw (rl, X a, X b));
emit (Pmulhuw (rh, X a, X b))) emit (Pmulhuw (rh, X a, X b)))
(* No operation *)
| "__builtin_nop", [], _ -> | "__builtin_nop", [], _ ->
emit Pnop emit Pnop
(* Optimization hint *)
| "__builtin_unreachable", [], _ ->
()
(* Catch-all *) (* Catch-all *)
| _ -> | _ ->
raise (Error ("unrecognized builtin " ^ name)) raise (Error ("unrecognized builtin " ^ name))
......
...@@ -487,9 +487,12 @@ let expand_builtin_inline name args res = ...@@ -487,9 +487,12 @@ let expand_builtin_inline name args res =
(* Synchronization *) (* Synchronization *)
| "__builtin_membar", [], _ -> | "__builtin_membar", [], _ ->
() ()
(* no operation *) (* No operation *)
| "__builtin_nop", [], _ -> | "__builtin_nop", [], _ ->
emit Pnop emit Pnop
(* Optimization hint *)
| "__builtin_unreachable", [], _ ->
()
(* Catch-all *) (* Catch-all *)
| _ -> | _ ->
raise (Error ("unrecognized builtin " ^ name)) raise (Error ("unrecognized builtin " ^ name))
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment