aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-10-02 21:54:34 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-10-02 21:54:34 +0200
commit825b77fe8b4eb0919564e51cfaae69a6dfae24e3 (patch)
treedf8293a59f51b137f2654f8adbe4e6ca7b7cdbc1
parentb5101e0d9c21810bd40253e3676838f87558e879 (diff)
downloadcompcert-kvx-825b77fe8b4eb0919564e51cfaae69a6dfae24e3.tar.gz
compcert-kvx-825b77fe8b4eb0919564e51cfaae69a6dfae24e3.zip
so that all architectures compile
-rw-r--r--aarch64/PrepassSchedulingOracle.ml (renamed from scheduling/PrepassSchedulingOracle.ml)0
l---------arm/PrepassSchedulingOracle.ml1
l---------kvx/PrepassSchedulingOracle.ml1
l---------powerpc/PrepassSchedulingOracle.ml1
-rw-r--r--riscV/OpWeights.ml23
l---------riscV/PrepassSchedulingOracle.ml1
-rw-r--r--x86/PrepassSchedulingOracle.ml5
7 files changed, 24 insertions, 8 deletions
diff --git a/scheduling/PrepassSchedulingOracle.ml b/aarch64/PrepassSchedulingOracle.ml
index 25083bcd..25083bcd 100644
--- a/scheduling/PrepassSchedulingOracle.ml
+++ b/aarch64/PrepassSchedulingOracle.ml
diff --git a/arm/PrepassSchedulingOracle.ml b/arm/PrepassSchedulingOracle.ml
new file mode 120000
index 00000000..9885fd52
--- /dev/null
+++ b/arm/PrepassSchedulingOracle.ml
@@ -0,0 +1 @@
+../x86/PrepassSchedulingOracle.ml \ No newline at end of file
diff --git a/kvx/PrepassSchedulingOracle.ml b/kvx/PrepassSchedulingOracle.ml
new file mode 120000
index 00000000..912e9ffa
--- /dev/null
+++ b/kvx/PrepassSchedulingOracle.ml
@@ -0,0 +1 @@
+../aarch64/PrepassSchedulingOracle.ml \ No newline at end of file
diff --git a/powerpc/PrepassSchedulingOracle.ml b/powerpc/PrepassSchedulingOracle.ml
new file mode 120000
index 00000000..9885fd52
--- /dev/null
+++ b/powerpc/PrepassSchedulingOracle.ml
@@ -0,0 +1 @@
+../x86/PrepassSchedulingOracle.ml \ No newline at end of file
diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml
index 88ef5216..143435c1 100644
--- a/riscV/OpWeights.ml
+++ b/riscV/OpWeights.ml
@@ -1,9 +1,9 @@
open Op;;
(* Attempt at modeling SweRV EH1
-[| issues ; LSU ; multiplier ; divider |] *)
-let resource_bounds = [| 2 ; 1; 1; 2 |];;
-
+[| issues ; LSU ; multiplier |] *)
+let resource_bounds = [| 2 ; 1; 1 |];;
+let nr_non_pipelined_units = 1;; (* divider *)
let latency_of_op (op : operation) (nargs : int) =
match op with
@@ -15,18 +15,25 @@ let latency_of_op (op : operation) (nargs : int) =
let resources_of_op (op : operation) (nargs : int) =
match op with
| Omul | Omulhs | Omulhu
- | Omull | Omullhs | Omullhu -> [| 1 ; 0 ; 1; 0 |]
- | Odiv | Odivu | Odivl | Odivlu -> [| 0 ; 0; 0; 1 |]
+ | Omull | Omullhs | Omullhu -> [| 1 ; 0 ; 1 |]
+ | Odiv | Odivu | Odivl | Odivlu -> [| 0 ; 0; 0 |]
| _ -> [| 1; 0; 0; 0 |];;
+
+let non_pipelined_resources_of_op (op : operation) (nargs : int) =
+ match op with
+ | Odiv | Odivu -> [| 29 |]
+ | Odivfs -> [| 20 |]
+ | Odivl | Odivlu | Odivf -> [| 50 |]
+ | _ -> [| -1 |];;
-let resources_of_cond (cond : condition) (nargs : int) = [| 1; 0; 0; 0 |];;
+let resources_of_cond (cond : condition) (nargs : int) = [| 1; 0; 0 |];;
let latency_of_load trap chunk (addr : addressing) (nargs : int) = 3;;
let latency_of_call _ _ = 6;;
-let resources_of_load trap chunk addressing nargs = [| 1; 1; 0; 0 |];;
+let resources_of_load trap chunk addressing nargs = [| 1; 1; 0 |];;
-let resources_of_store chunk addressing nargs = [| 1; 1; 0; 0 |];;
+let resources_of_store chunk addressing nargs = [| 1; 1; 0 |];;
let resources_of_call _ _ = resource_bounds;;
let resources_of_builtin _ = resource_bounds;;
diff --git a/riscV/PrepassSchedulingOracle.ml b/riscV/PrepassSchedulingOracle.ml
new file mode 120000
index 00000000..912e9ffa
--- /dev/null
+++ b/riscV/PrepassSchedulingOracle.ml
@@ -0,0 +1 @@
+../aarch64/PrepassSchedulingOracle.ml \ No newline at end of file
diff --git a/x86/PrepassSchedulingOracle.ml b/x86/PrepassSchedulingOracle.ml
new file mode 100644
index 00000000..7b6a1b14
--- /dev/null
+++ b/x86/PrepassSchedulingOracle.ml
@@ -0,0 +1,5 @@
+open RTL
+open Registers
+
+(* Do not do anything *)
+let schedule_sequence (seqa : (instruction*Regset.t) array) = None