aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--aarch64/OpWeightsAsm.ml55
-rw-r--r--aarch64/PostpassSchedulingOracle.ml8
-rwxr-xr-xtest/aarch64/asmb_aarch64_gen_test.sh106
-rw-r--r--test/aarch64/c/arith_print.c19
-rwxr-xr-xtest/aarch64/gen_tests/asmb_aarch64_gen_test.sh106
-rwxr-xr-xtest/aarch64/postpass_tests/postpass_exec_c_test.sh36
6 files changed, 193 insertions, 137 deletions
diff --git a/aarch64/OpWeightsAsm.ml b/aarch64/OpWeightsAsm.ml
index 5ba5832b..c1d0583a 100644
--- a/aarch64/OpWeightsAsm.ml
+++ b/aarch64/OpWeightsAsm.ml
@@ -221,10 +221,10 @@ module Cortex_A53 = struct
| Uxtw -> 1
| Uxtx -> 1
| Btbl -> 1
- | Allocframe -> 1
- | Freeframe -> 1
- | Builtin -> 1
- | Cvtx2w -> 1
+ | Allocframe -> 51
+ | Freeframe -> 51
+ | Builtin -> 51
+ | Cvtx2w -> 51
let resources_of_op (i : real_instruction) (nargs : int) =
match i with
@@ -317,30 +317,30 @@ module Cortex_A53 = struct
| Uxtw -> [| 1; 1; 0; 0 |]
| Uxtx -> [| 1; 1; 0; 0 |]
| Btbl -> [| 1; 1; 0; 0 |]
- | Allocframe -> [| 1; 0; 0; 0 |]
- | Freeframe -> [| 1; 0; 0; 0 |]
- | Builtin -> [| 1; 0; 0; 0 |]
- | Cvtx2w -> [| 1; 0; 0; 0 |]
+ | Allocframe -> [| 1; 1; 1; 1 |]
+ | Freeframe -> [| 1; 1; 1; 1 |]
+ | Builtin -> [| 1; 1; 1; 1 |]
+ | Cvtx2w -> [| 1; 1; 1; 1 |]
- (*let non_pipelined_resources_of_op (op : operation) (nargs : int) =
- match op with
- | Odiv | Odivu -> [| 29 |]
- | Odivfs -> [| 20 |]
- | Odivl | Odivlu | Odivf -> [| 50 |]
- | _ -> [| -1 |];;
+ (*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 (cmp : condition) (nargs : int) =
- (match cmp with
- | Ccompf _ (* r FP comparison *)
- | Cnotcompf _ (* r negation of an FP comparison *)
- | Ccompfzero _ (* r comparison with 0.0 *)
- | Cnotcompfzero _ (* r negation of comparison with 0.0 *)
- | Ccompfs _ (* r FP comparison *)
- | Cnotcompfs _ (* r negation of an FP comparison *)
- | Ccompfszero _ (* r equal to 0.0 *)
- | Cnotcompfszero _ (* r not equal to 0.0 *) ->
- [| 1; 1; 1; 0 |]
- | _ -> [| 1; 1; 0; 0 |] )*)
+ let resources_of_cond (cmp : condition) (nargs : int) =
+ (match cmp with
+ | Ccompf _ (* r FP comparison *)
+ | Cnotcompf _ (* r negation of an FP comparison *)
+ | Ccompfzero _ (* r comparison with 0.0 *)
+ | Cnotcompfzero _ (* r negation of comparison with 0.0 *)
+ | Ccompfs _ (* r FP comparison *)
+ | Cnotcompfs _ (* r negation of an FP comparison *)
+ | Ccompfszero _ (* r equal to 0.0 *)
+ | Cnotcompfszero _ (* r not equal to 0.0 *) ->
+ [| 1; 1; 1; 0 |]
+ | _ -> [| 1; 1; 0; 0 |] )*)
let latency_of_load trap chunk _ _ = 3
@@ -362,7 +362,8 @@ let get_opweights () : opweights =
pipelined_resource_bounds = Cortex_A53.resource_bounds;
nr_non_pipelined_units = Cortex_A53.nr_non_pipelined_units;
latency_of_op = Cortex_A53.latency_of_op;
- resources_of_op = Cortex_A53.resources_of_op
+ resources_of_op =
+ Cortex_A53.resources_of_op
(*non_pipelined_resources_of_op = Cortex_A53.non_pipelined_resources_of_op;*)
(*latency_of_load = Cortex_A53.latency_of_load;*)
(*resources_of_load = Cortex_A53.resources_of_load;*)
diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml
index a2e15139..831080d5 100644
--- a/aarch64/PostpassSchedulingOracle.ml
+++ b/aarch64/PostpassSchedulingOracle.ml
@@ -17,7 +17,7 @@ open Asmblock
open OpWeightsAsm
open InstructionScheduler
-let debug = false
+let debug = true
(**
* Extracting infos from Asm instructions
@@ -890,11 +890,11 @@ let smart_schedule bb =
pack_result bb'
let bblock_schedule bb =
- if debug then (
+ let identity_mode = not !Clflags.option_fpostpass in
+ if (debug && not identity_mode) then (
Printf.eprintf "###############################\n";
Printf.eprintf "SCHEDULING\n" );
- (*if Compopts.optim_postpass () then smart_schedule bb else dumb_schedule bb*)
- smart_schedule bb
+ if identity_mode then pack_result bb else smart_schedule bb
(** Called schedule function from Coq *)
diff --git a/test/aarch64/asmb_aarch64_gen_test.sh b/test/aarch64/asmb_aarch64_gen_test.sh
deleted file mode 100755
index f816204e..00000000
--- a/test/aarch64/asmb_aarch64_gen_test.sh
+++ /dev/null
@@ -1,106 +0,0 @@
-#!/bin/bash
-
-CLEAN=0
-WOFF=0
-while getopts ':cw' 'OPTKEY'; do
- case ${OPTKEY} in
- c) CLEAN=1;;
- w) WOFF=1;;
- esac
-done
-
-DIRS=(
- c/*.c # Special simple tests
- ../c/*.c
- ../clightgen/*.c
- ../compression/*.c
- ../cse2/*.c
-
- # Monniaux test directory
- ../monniaux/binary_search/*.c
- ../monniaux/complex/*.c
- #../monniaux/crypto-algorithms/*.c # Warnings
- ../monniaux/cse2/*.c
- #../monniaux/des/*.c # Unsupported feature?
- ../monniaux/expect/*.c
- ../monniaux/fill_buffer/*.c
- ../monniaux/genann/*.c
- #../monniaux/heptagon_radio_transmitter/*.c # Warnings
- ../monniaux/idea/*.c
- ../monniaux/jumptable/*.c
- ../monniaux/licm/*.c
- ../monniaux/longjmp/*.c
- ../monniaux/loop/*.c
- ../monniaux/lustrev4_lustrec_heater_control/*.c
- ../monniaux/lustrev4_lv4_heater_control/*.c
- ../monniaux/lustrev4_lv6-en-2cgc_heater_control/*.c
- #../monniaux/lustrev6-carlightV2/*.c # Warnings
- #../monniaux/lustrev6-convertible-2cgc/*.c # Unsupported feature?
- ../monniaux/lustrev6-convertible-en-2cgc/*.c
- #../monniaux/lustrev6-convertible/*.c # Warnings
- ../monniaux/madd/*.c
- #../monniaux/math/*.c # Unsupported feature?
- ../monniaux/memcpy/*.c
- #../monniaux/micro-bunzip/*.c # Warnings
- ../monniaux/moves/*.c
- ../monniaux/multithreaded_volatile/*.c
- ../monniaux/nand/*.c
- #../monniaux/ncompress/*.c # Warnings
- ../monniaux/number_theoretic_transform/*.c
- ../monniaux/predicated/*.c
- ../monniaux/regalloc/*.c
- ../monniaux/rotate/*.c
- ../monniaux/scheduling/*.c
- ../monniaux/send_through/*.c
- ../monniaux/tiny-AES-c/*.c
- ../monniaux/varargs/*.c
- ../monniaux/xor_and_mat/*.c
- #../monniaux/zlib-1.2.11/*.c # Warnings
-)
-#FILES=../c/*.c
-CCOMP_BBLOCKS="../../ccomp"
-CCOMP_REF="../../../CompCert_master/ccomp"
-COUNT=0
-
-if [ $WOFF -eq 1 ]
-then
- CCOMP_BBLOCKS="${CCOMP_BBLOCKS} -w"
- CCOMP_REF="${CCOMP_REF} -w"
-fi
-
-for files in ${DIRS[@]}
-do
- for f in $files
- do
- BNAME=$(basename -s .c $f)
- SNAME="$BNAME".s
- SREFNAME="$BNAME"_ref.s
- ./$CCOMP_BBLOCKS -S $f -o $SNAME
- ./$CCOMP_REF -dmach -S $f -o $SREFNAME
- #diff -I '^//*' <(cut -c-5 $SNAME) <(cut -c-5 $SREFNAME) > /dev/null 2>&1
- diff -I '^//*' $SNAME $SREFNAME > /dev/null 2>&1
-
- error=$?
- if [ $error -eq 0 ]
- then
- echo "[$BNAME] OK"
- COUNT=$((COUNT + 1))
- elif [ $error -eq 1 ]
- then
- echo "[$BNAME] FAIL"
- diff -I '^//*' -y $SNAME $SREFNAME
- exit 1
- else
- echo "[$BNAME] FAIL"
- echo "[WARNING] There was something wrong with the diff command !"
- exit 1
- fi
- done
-done
-
-echo "[TOTAL] $COUNT tests PASSED"
-
-if [ $CLEAN -eq 1 ]
-then
- rm *.s *.mach
-fi
diff --git a/test/aarch64/c/arith_print.c b/test/aarch64/c/arith_print.c
new file mode 100644
index 00000000..d404a151
--- /dev/null
+++ b/test/aarch64/c/arith_print.c
@@ -0,0 +1,19 @@
+int main()
+{
+ int num1 = 2;
+ int num2 = 4;
+ int sum, sub, mult, mod;
+ float div;
+
+ /*
+ * Perform all arithmetic operations
+ */
+ sum = num1 + num2;
+ sub = num1 - num2;
+ mult = num1 * num2;
+ div = (float)num1 / num2;
+ mod = num1 % num2;
+
+ printf("%d", sum + sub + mult + div + mod);
+ return;
+}
diff --git a/test/aarch64/gen_tests/asmb_aarch64_gen_test.sh b/test/aarch64/gen_tests/asmb_aarch64_gen_test.sh
new file mode 100755
index 00000000..660ff7aa
--- /dev/null
+++ b/test/aarch64/gen_tests/asmb_aarch64_gen_test.sh
@@ -0,0 +1,106 @@
+#!/bin/bash
+
+CLEAN=0
+WOFF=0
+while getopts ':cw' 'OPTKEY'; do
+ case ${OPTKEY} in
+ c) CLEAN=1;;
+ w) WOFF=1;;
+ esac
+done
+
+DIRS=(
+ ../c/*.c # Special simple tests
+ ../../c/*.c
+ ../../clightgen/*.c
+ ../../compression/*.c
+ ../../cse2/*.c
+
+ # Monniaux test directory
+ ../../monniaux/binary_search/*.c
+ ../../monniaux/complex/*.c
+ #../../monniaux/crypto-algorithms/*.c # Warnings
+ ../../monniaux/cse2/*.c
+ #../../monniaux/des/*.c # Unsupported feature?
+ ../../monniaux/expect/*.c
+ ../../monniaux/fill_buffer/*.c
+ ../../monniaux/genann/*.c
+ #../../monniaux/heptagon_radio_transmitter/*.c # Warnings
+ ../../monniaux/idea/*.c
+ ../../monniaux/jumptable/*.c
+ ../../monniaux/licm/*.c
+ ../../monniaux/longjmp/*.c
+ ../../monniaux/loop/*.c
+ ../../monniaux/lustrev4_lustrec_heater_control/*.c
+ ../../monniaux/lustrev4_lv4_heater_control/*.c
+ ../../monniaux/lustrev4_lv6-en-2cgc_heater_control/*.c
+ #../../monniaux/lustrev6-carlightV2/*.c # Warnings
+ #../../monniaux/lustrev6-convertible-2cgc/*.c # Unsupported feature?
+ ../../monniaux/lustrev6-convertible-en-2cgc/*.c
+ #../../monniaux/lustrev6-convertible/*.c # Warnings
+ ../../monniaux/madd/*.c
+ #../../monniaux/math/*.c # Unsupported feature?
+ ../../monniaux/memcpy/*.c
+ #../../monniaux/micro-bunzip/*.c # Warnings
+ ../../monniaux/moves/*.c
+ ../../monniaux/multithreaded_volatile/*.c
+ ../../monniaux/nand/*.c
+ #../../monniaux/ncompress/*.c # Warnings
+ ../../monniaux/number_theoretic_transform/*.c
+ ../../monniaux/predicated/*.c
+ ../../monniaux/regalloc/*.c
+ ../../monniaux/rotate/*.c
+ ../../monniaux/scheduling/*.c
+ ../../monniaux/send_through/*.c
+ ../../monniaux/tiny-AES-c/*.c
+ ../../monniaux/varargs/*.c
+ ../../monniaux/xor_and_mat/*.c
+ #../../monniaux/zlib-1.2.11/*.c # Warnings
+)
+#FILES=../c/*.c
+CCOMP_BBLOCKS="../../../ccomp -fno-postpass"
+CCOMP_REF="../../../../CompCert_aarch64-ref/ccomp"
+COUNT=0
+
+if [ $WOFF -eq 1 ]
+then
+ CCOMP_BBLOCKS="${CCOMP_BBLOCKS} -w"
+ CCOMP_REF="${CCOMP_REF} -w"
+fi
+
+for files in ${DIRS[@]}
+do
+ for f in $files
+ do
+ BNAME=$(basename -s .c $f)
+ SNAME="$BNAME".s
+ SREFNAME="$BNAME"_ref.s
+ ./$CCOMP_BBLOCKS -S $f -o $SNAME
+ ./$CCOMP_REF -dmach -S $f -o $SREFNAME
+ #diff -I '^//*' <(cut -c-5 $SNAME) <(cut -c-5 $SREFNAME) > /dev/null 2>&1
+ diff -I '^//*' $SNAME $SREFNAME > /dev/null 2>&1
+
+ error=$?
+ if [ $error -eq 0 ]
+ then
+ echo "[$BNAME] OK"
+ COUNT=$((COUNT + 1))
+ elif [ $error -eq 1 ]
+ then
+ echo "[$BNAME] FAIL"
+ diff -I '^//*' -y $SNAME $SREFNAME
+ exit 1
+ else
+ echo "[$BNAME] FAIL"
+ echo "[WARNING] There was something wrong with the diff command !"
+ exit 1
+ fi
+ done
+done
+
+echo "[TOTAL] $COUNT tests PASSED"
+
+if [ $CLEAN -eq 1 ]
+then
+ rm *.s *.mach
+fi
diff --git a/test/aarch64/postpass_tests/postpass_exec_c_test.sh b/test/aarch64/postpass_tests/postpass_exec_c_test.sh
new file mode 100755
index 00000000..73422990
--- /dev/null
+++ b/test/aarch64/postpass_tests/postpass_exec_c_test.sh
@@ -0,0 +1,36 @@
+#!/bin/bash
+
+CLEAN=0
+WOFF=0
+SRC=""
+while getopts ':cwi:' 'OPTKEY'; do
+ case ${OPTKEY} in
+ c) CLEAN=1;;
+ w) WOFF=1;;
+ i) SRC=${OPTARG};;
+ esac
+done
+
+CCOMP="../../../ccomp -static"
+
+if [ $WOFF -eq 1 ]
+then
+ CCOMP="${CCOMP} -w"
+fi
+
+BNAME=$(basename -s .c $SRC)
+SNAME="$BNAME".s
+SREFNAME="$BNAME"_ref.s
+ENAME="$BNAME"
+EREFNAME="$BNAME"_ref
+./$CCOMP -S $SRC -o $SNAME
+./$CCOMP -fno-postpass -S $SRC -o $SREFNAME
+./$CCOMP $SRC -o $ENAME
+./$CCOMP -fno-postpass $SRC -o $EREFNAME
+
+#diff -I '^//*' -y $SNAME $SREFNAME
+
+if [ $CLEAN -eq 1 ]
+then
+ rm $SNAME $SREFNAME $ENAME $EREFNAME
+fi
generated by cgit (git 2.34.1) at 2024-06-03 03:04:44 +0000