aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--aarch64/DuplicateOpcodeHeuristic.ml30
-rw-r--r--arm/DuplicateOpcodeHeuristic.ml25
-rw-r--r--backend/Duplicateaux.ml18
-rwxr-xr-xconfig_rv64.sh2
-rwxr-xr-xconfig_simple.sh7
-rw-r--r--driver/Clflags.ml2
-rw-r--r--driver/Driver.ml6
-rw-r--r--powerpc/DuplicateOpcodeHeuristic.ml30
-rw-r--r--riscV/DuplicateOpcodeHeuristic.ml30
-rw-r--r--x86/DuplicateOpcodeHeuristic.ml30
10 files changed, 154 insertions, 26 deletions
diff --git a/aarch64/DuplicateOpcodeHeuristic.ml b/aarch64/DuplicateOpcodeHeuristic.ml
index 85505245..5fc2156c 100644
--- a/aarch64/DuplicateOpcodeHeuristic.ml
+++ b/aarch64/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,27 @@
-exception HeuristicSucceeded
-
-let opcode_heuristic code cond ifso ifnot preferred = ()
+open Op
+open Integers
+
+let opcode_heuristic code cond ifso ifnot is_loop_header =
+ match cond with
+ | Ccompimm (c, n) | Ccompuimm (c, n) -> if n == Integers.Int.zero then (match c with
+ | Clt | Cle -> Some false
+ | Cgt | Cge -> Some true
+ | _ -> None
+ ) else None
+ | Ccomplimm (c, n) | Ccompluimm (c, n) -> if n == Integers.Int64.zero then (match c with
+ | Clt | Cle -> Some false
+ | Cgt | Cge -> Some true
+ | _ -> None
+ ) else None
+ | Ccompf c | Ccompfs c -> (match c with
+ | Ceq -> Some false
+ | Cne -> Some true
+ | _ -> None
+ )
+ | Cnotcompf c | Cnotcompfs c -> (match c with
+ | Ceq -> Some true
+ | Cne -> Some false
+ | _ -> None
+ )
+ | _ -> None
+
diff --git a/arm/DuplicateOpcodeHeuristic.ml b/arm/DuplicateOpcodeHeuristic.ml
index 85505245..9b6a6409 100644
--- a/arm/DuplicateOpcodeHeuristic.ml
+++ b/arm/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,22 @@
-exception HeuristicSucceeded
-
-let opcode_heuristic code cond ifso ifnot preferred = ()
+open Op
+open Integers
+
+let opcode_heuristic code cond ifso ifnot is_loop_header =
+ match cond with
+ | Ccompimm (c, n) | Ccompuimm (c, n) -> if n == Integers.Int.zero then (match c with
+ | Clt | Cle -> Some false
+ | Cgt | Cge -> Some true
+ | _ -> None
+ ) else None
+ | Ccompf c | Ccompfs c -> (match c with
+ | Ceq -> Some false
+ | Cne -> Some true
+ | _ -> None
+ )
+ | Cnotcompf c | Cnotcompfs c -> (match c with
+ | Ceq -> Some true
+ | Cne -> Some false
+ | _ -> None
+ )
+ | _ -> None
+
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 209527b9..a84f9754 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -502,11 +502,15 @@ let rec invert_iconds code = function
let duplicate_aux f =
let entrypoint = f.fn_entrypoint in
let code = f.fn_code in
- let traces = select_traces (to_ttl_code code entrypoint) entrypoint in
- let icond_code = invert_iconds code traces in
- let preds = get_predecessors_rtl icond_code in
- if !Clflags.option_fduplicate >= 1 then
- let (new_code, pTreeId) = ((* print_traces traces; *) superblockify_traces icond_code preds traces) in
- ((new_code, f.fn_entrypoint), pTreeId)
+ if !Clflags.option_fduplicate < 0 then
+ ((code, entrypoint), make_identity_ptree code)
else
- ((icond_code, entrypoint), make_identity_ptree code)
+ let traces = select_traces (to_ttl_code code entrypoint) entrypoint in
+ let icond_code = invert_iconds code traces in
+ let preds = get_predecessors_rtl icond_code in
+ if !Clflags.option_fduplicate >= 1 then
+ let (new_code, pTreeId) = ((* print_traces traces; *) superblockify_traces icond_code preds traces) in
+ ((new_code, f.fn_entrypoint), pTreeId)
+ else
+ ((icond_code, entrypoint), make_identity_ptree code)
+
diff --git a/config_rv64.sh b/config_rv64.sh
index e95f8a70..0698c2ff 100755
--- a/config_rv64.sh
+++ b/config_rv64.sh
@@ -1 +1 @@
-exec ./config_simple.sh rv64-linux --toolprefix riscv64-unknown-elf- "$@"
+exec ./config_simple.sh rv64-linux --toolprefix riscv64-linux-gnu- "$@"
diff --git a/config_simple.sh b/config_simple.sh
index f02680c4..e2d3844c 100755
--- a/config_simple.sh
+++ b/config_simple.sh
@@ -3,4 +3,9 @@ shift
version=`git rev-parse --short HEAD`
branch=`git rev-parse --abbrev-ref HEAD`
date=`date -I`
-./configure --prefix /opt/CompCert/${branch}/${date}_${version}/$arch "$@" $arch
+
+if test "x$CCOMP_INSTALL_PREFIX" = "x" ;
+then CCOMP_INSTALL_PREFIX=/opt/CompCert ;
+fi
+
+./configure --prefix ${CCOMP_INSTALL_PREFIX}/${branch}/${date}_${version}/$arch "$@" $arch
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 901aaa59..ff2647a7 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -30,7 +30,7 @@ let option_fcse2 = ref false
let option_fcse3 = ref true
let option_fcse3_alias_analysis = ref true
let option_fredundancy = ref true
-let option_fduplicate = ref 0
+let option_fduplicate = ref (-1)
let option_finvertcond = ref true
let option_ftracelinearize = ref false
let option_fpostpass = ref true
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 5ae31a1f..b167dbd1 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -203,7 +203,11 @@ Processing options:
-fpostpass Perform postpass scheduling (only for K1 architecture) [on]
-fpostpass= <optim> Perform postpass scheduling with the specified optimization [list]
(<optim>=list: list scheduling, <optim>=ilp: ILP, <optim>=greedy: just packing bundles)
- -fduplicate Perform tail duplication to form superblocks on predicted traces
+ -fduplicate <nb_nodes> Perform tail duplication to form superblocks on predicted traces
+ nb_nodes control the heuristic deciding to duplicate or not
+ A value of -1 desactivates the entire pass (including branch prediction)
+ A value of 0 desactivates the duplication (but activates the branch prediction)
+ FIXME : this is desactivated by default for now
-finvertcond Invert conditions based on predicted paths (to prefer fallthrough).
Requires -fduplicate to be also activated [on]
-ftracelinearize Linearizes based on the traces identified by duplicate phase
diff --git a/powerpc/DuplicateOpcodeHeuristic.ml b/powerpc/DuplicateOpcodeHeuristic.ml
index 85505245..33be79e8 100644
--- a/powerpc/DuplicateOpcodeHeuristic.ml
+++ b/powerpc/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,27 @@
-exception HeuristicSucceeded
-
-let opcode_heuristic code cond ifso ifnot preferred = ()
+(* open Camlcoq *)
+open Op
+open Integers
+
+let opcode_heuristic code cond ifso ifnot is_loop_header =
+ match cond with
+ | Ccompimm (c, n) | Ccompuimm (c, n) -> if n == Integers.Int.zero then (match c with
+ | Clt | Cle -> Some false
+ | Cgt | Cge -> Some true
+ | _ -> None
+ ) else None
+ | Ccomplimm (c, n) | Ccompluimm (c, n) -> if n == Integers.Int64.zero then (match c with
+ | Clt | Cle -> Some false
+ | Cgt | Cge -> Some true
+ | _ -> None
+ ) else None
+ | Ccompf c -> (match c with
+ | Ceq -> Some false
+ | Cne -> Some true
+ | _ -> None
+ )
+ | Cnotcompf c -> (match c with
+ | Ceq -> Some true
+ | Cne -> Some false
+ | _ -> None
+ )
+ | _ -> None
diff --git a/riscV/DuplicateOpcodeHeuristic.ml b/riscV/DuplicateOpcodeHeuristic.ml
index 85505245..2ec314c1 100644
--- a/riscV/DuplicateOpcodeHeuristic.ml
+++ b/riscV/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,27 @@
-exception HeuristicSucceeded
-
-let opcode_heuristic code cond ifso ifnot preferred = ()
+(* open Camlcoq *)
+open Op
+open Integers
+
+let opcode_heuristic code cond ifso ifnot is_loop_header =
+ match cond with
+ | Ccompimm (c, n) | Ccompuimm (c, n) -> if n == Integers.Int.zero then (match c with
+ | Clt | Cle -> Some false
+ | Cgt | Cge -> Some true
+ | _ -> None
+ ) else None
+ | Ccomplimm (c, n) | Ccompluimm (c, n) -> if n == Integers.Int64.zero then (match c with
+ | Clt | Cle -> Some false
+ | Cgt | Cge -> Some true
+ | _ -> None
+ ) else None
+ | Ccompf c | Ccompfs c -> (match c with
+ | Ceq -> Some false
+ | Cne -> Some true
+ | _ -> None
+ )
+ | Cnotcompf c | Cnotcompfs c -> (match c with
+ | Ceq -> Some true
+ | Cne -> Some false
+ | _ -> None
+ )
+ | _ -> None
diff --git a/x86/DuplicateOpcodeHeuristic.ml b/x86/DuplicateOpcodeHeuristic.ml
index 85505245..2ec314c1 100644
--- a/x86/DuplicateOpcodeHeuristic.ml
+++ b/x86/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,27 @@
-exception HeuristicSucceeded
-
-let opcode_heuristic code cond ifso ifnot preferred = ()
+(* open Camlcoq *)
+open Op
+open Integers
+
+let opcode_heuristic code cond ifso ifnot is_loop_header =
+ match cond with
+ | Ccompimm (c, n) | Ccompuimm (c, n) -> if n == Integers.Int.zero then (match c with
+ | Clt | Cle -> Some false
+ | Cgt | Cge -> Some true
+ | _ -> None
+ ) else None
+ | Ccomplimm (c, n) | Ccompluimm (c, n) -> if n == Integers.Int64.zero then (match c with
+ | Clt | Cle -> Some false
+ | Cgt | Cge -> Some true
+ | _ -> None
+ ) else None
+ | Ccompf c | Ccompfs c -> (match c with
+ | Ceq -> Some false
+ | Cne -> Some true
+ | _ -> None
+ )
+ | Cnotcompf c | Cnotcompfs c -> (match c with
+ | Ceq -> Some true
+ | Cne -> Some false
+ | _ -> None
+ )
+ | _ -> None