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 d53cc13b authored by Cyril SIX's avatar Cyril SIX
Browse files

Adding distinction between kvx-cos and kvx-mbr (for trapping loads)

parent 5a846f2a
......@@ -297,6 +297,7 @@ compcert.ini: Makefile.config
echo "linker_options=$(CLINKER_OPTIONS)";\
echo "arch=$(ARCH)"; \
echo "model=$(MODEL)"; \
echo "os=$(OS)"; \
echo "abi=$(ABI)"; \
echo "endianness=$(ENDIANNESS)"; \
echo "system=$(SYSTEM)"; \
......
......@@ -710,6 +710,7 @@ HAS_STANDARD_HEADERS=$has_standard_headers
INSTALL_COQDEV=$install_coqdev
LIBMATH=$libmath
MODEL=$model
OS=${os:-unspecified}
SYSTEM=$system
RESPONSEFILE=$responsefile
LIBRARY_FLOCQ=$library_Flocq
......
......@@ -242,7 +242,7 @@ let rv64 =
struct_passing_style = SP_ref_callee; (* Wrong *)
struct_return_style = SR_ref } (* to check *)
let kvx =
let kvxbase =
{ name = "kvx";
char_signed = true;
wchar_signed = true;
......@@ -275,7 +275,15 @@ let kvx =
supports_unaligned_accesses = true;
struct_passing_style = SP_value32_ref_callee;
struct_return_style = SR_int1to4;
has_non_trapping_loads = true;
has_non_trapping_loads = false;
}
let kvxcos =
{ kvxbase with has_non_trapping_loads = false;
}
let kvxmbr =
{ kvxbase with has_non_trapping_loads = true;
}
let aarch64 =
......
......@@ -88,7 +88,8 @@ val arm_littleendian : t
val arm_bigendian : t
val rv32 : t
val rv64 : t
val kvx : t
val kvxmbr : t
val kvxcos : t
val aarch64 : t
val gcc_extensions : t -> t
......
......@@ -126,6 +126,7 @@ let arch =
| "powerpc"|"arm"|"x86"|"riscV"|"kvx"|"aarch64" as a -> a
| v -> bad_config "arch" [v]
let model = get_config_string "model"
let os = get_config_string "os"
let abi = get_config_string "abi"
let is_big_endian =
match get_config_string "endianness" with
......
......@@ -19,6 +19,9 @@ val model: string
val abi: string
(** ABI to use *)
val os: string
(** ABI to use *)
val is_big_endian: bool
(** Endianness to use *)
......
......@@ -117,7 +117,10 @@ let init () =
| "riscV" -> if Configuration.model = "64"
then Machine.rv64
else Machine.rv32
| "kvx" -> Machine.kvx
| "kvx" -> if Configuration.os = "cos" then Machine.kvxcos
else if Configuration.os = "mbr" then Machine.kvxmbr
else (Printf.eprintf "Configuration OS = %s\n" Configuration.os;
failwith "Wrong OS configuration for KVX")
| "aarch64" -> Machine.aarch64
| _ -> assert false
end;
......
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