From 1b111e3658b3f79a9814fd9799e2dbe0a921c768 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 17 Mar 2020 00:11:42 +0100 Subject: specify prefix with CCOMP_INSTALL_PREFIX --- config_simple.sh | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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 -- cgit From fac63511aaf3fd3c77db69802c24474559365879 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 17 Mar 2020 07:44:45 +0100 Subject: fix for aarch64 DuplicateOpcodeHeuristic.ml --- aarch64/DuplicateOpcodeHeuristic.ml | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 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 + -- cgit From 0ebdbc31c3e992e43d85699a039ebdd23e272df6 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 17 Mar 2020 07:49:46 +0100 Subject: DuplicateOpcodeHeuristic for ARM --- arm/DuplicateOpcodeHeuristic.ml | 25 ++++++++++++++++++++++--- 1 file changed, 22 insertions(+), 3 deletions(-) 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 + -- cgit From 2f19071e865181d9a0c2e61f5e57731fb86e4e5d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 17 Mar 2020 07:57:56 +0100 Subject: riscV/DuplicateOpcodeHeuristic.ml --- config_rv64.sh | 2 +- riscV/DuplicateOpcodeHeuristic.ml | 30 +++++++++++++++++++++++++++--- 2 files changed, 28 insertions(+), 4 deletions(-) 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/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 -- cgit From 0eb778a85b5b76ab6c7fd914ffaff1affcbde7bb Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 17 Mar 2020 08:05:17 +0100 Subject: DuplicateOpcodeHeuristic ppc --- powerpc/DuplicateOpcodeHeuristic.ml | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 deletions(-) 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 -- cgit From aa2e3d776cb82ce01c4afdbacc52951e60ff2104 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 17 Mar 2020 08:10:26 +0100 Subject: DuplicateOpcodeHeuristic x86 --- x86/DuplicateOpcodeHeuristic.ml | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 deletions(-) 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 -- cgit From fb43d1078c0b0824132b30d7dd9bfe6b0ac47122 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 17 Mar 2020 15:12:06 +0100 Subject: Desactivating branch predictions by default --- backend/Duplicateaux.ml | 18 +++++++++++------- driver/Clflags.ml | 2 +- driver/Driver.ml | 6 +++++- 3 files changed, 17 insertions(+), 9 deletions(-) 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/driver/Clflags.ml b/driver/Clflags.ml index 8054eb5b..6986fb96 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -28,7 +28,7 @@ let option_fconstprop = ref true let option_fcse = ref true let option_fcse2 = 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 01451e07..388482a0 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -201,7 +201,11 @@ Processing options: -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] (=list: list scheduling, =ilp: ILP, =greedy: just packing bundles) - -fduplicate Perform tail duplication to form superblocks on predicted traces + -fduplicate 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 -- cgit