diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-07-24 11:42:09 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-07-24 11:42:09 +0200 |
| commit | a4570fed198034e535d0d6d99e23cfbb1d40b926 (patch) | |
| tree | e4e5a9dc845fc0972622ae05fd9084234ed9a44d /x86 | |
| parent | 95f918c38b1e59f40ae7af455ec2c6746289375e (diff) | |
| parent | b5c4192c73d7b02e0c90354e26b35a84ee141083 (diff) | |
| download | compcert-kvx-a4570fed198034e535d0d6d99e23cfbb1d40b926.tar.gz compcert-kvx-a4570fed198034e535d0d6d99e23cfbb1d40b926.zip | |
Merge branch 'kvx-work' into rtl-tunneling
Diffstat (limited to 'x86')
| -rw-r--r--[l---------] | x86/ExpansionOracle.ml | 18 | ||||
| -rw-r--r-- | x86/PrepassSchedulingOracle.ml | 3 | ||||
| -rw-r--r-- | x86/TargetPrinter.ml | 14 |
3 files changed, 30 insertions, 5 deletions
diff --git a/x86/ExpansionOracle.ml b/x86/ExpansionOracle.ml index ee2674bf..3b63b80d 120000..100644 --- a/x86/ExpansionOracle.ml +++ b/x86/ExpansionOracle.ml @@ -1 +1,17 @@ -../aarch64/ExpansionOracle.ml
\ No newline at end of file +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Léo Gourdin UGA, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +open RTLpathCommon + +let expanse (sb : superblock) code pm = (code, pm) + +let find_last_node_reg c = () diff --git a/x86/PrepassSchedulingOracle.ml b/x86/PrepassSchedulingOracle.ml index 7b6a1b14..42a3da23 100644 --- a/x86/PrepassSchedulingOracle.ml +++ b/x86/PrepassSchedulingOracle.ml @@ -2,4 +2,5 @@ open RTL open Registers (* Do not do anything *) -let schedule_sequence (seqa : (instruction*Regset.t) array) = None +let schedule_sequence (seqa : (instruction*Regset.t) array) + live_regs_entry typing reference = None diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index 2000f96a..00e70f65 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -95,9 +95,6 @@ let z oc n = output_string oc (Z.to_string n) let data_pointer = if Archi.ptr64 then ".quad" else ".long" -(* The comment deliminiter *) -let comment = "#" - (* Base-2 log of a Caml integer *) let rec log2 n = assert (n > 0); @@ -106,6 +103,7 @@ let rec log2 n = (* System dependent printer functions *) module type SYSTEM = sig + val comment: string val raw_symbol: out_channel -> string -> unit val symbol: out_channel -> P.t -> unit val label: out_channel -> int -> unit @@ -124,6 +122,9 @@ module type SYSTEM = module ELF_System : SYSTEM = struct + (* The comment delimiter *) + let comment = "#" + let raw_symbol oc s = fprintf oc "%s" s @@ -219,6 +220,10 @@ module ELF_System : SYSTEM = module MacOS_System : SYSTEM = struct + (* The comment delimiter. + `##` instead of `#` to please the Clang assembler. *) + let comment = "##" + let raw_symbol oc s = fprintf oc "_%s" s @@ -280,6 +285,9 @@ module MacOS_System : SYSTEM = module Cygwin_System : SYSTEM = struct + (* The comment delimiter *) + let comment = "#" + let symbol_prefix = if Archi.ptr64 then "" else "_" |