Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1

35 files changed, 89 insertions, 157 deletions

diff --git a/test/aarch64/README.md b/test/aarch64/README.md
deleted file mode 100644
index f943489c..00000000
--- a/test/aarch64/README.md
+++ /dev/null
@@ -1,15 +0,0 @@
-# Testing the Machblock --> Asmblock translation
-1. Get the reference version of compcert-aarch in the father's directory if this repo (checkout `aarch64-ref`)
-2. Compile both repo for aarch64
-3. CD in this folder (`test/aarch64`)
-4. Launch `./asmb_aarch64_gen_test.sh`
-
-## Options
-The script takes following options :
-- `-c` to clear generated files at the end
-- `-w` to suppress warnings from Compcert
-
-## Tests files
-The variable `DIRS` in the script takes the list of directories containing c files.
-The tests under `test/aarch64/c` are simpler and useful to debug only one feature at a time.
-Most of them comes from [here](https://cis.temple.edu/~ingargio/cis71/code/).
diff --git a/test/aarch64/gen_tests/asmb_aarch64_gen_test.sh b/test/aarch64/gen_tests/asmb_aarch64_gen_test.sh
deleted file mode 100755
index 38235f14..00000000
--- a/test/aarch64/gen_tests/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 -fno-postpass"
-CCOMP_REF="../../../../CompCert_kvx/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
deleted file mode 100755
index 73422990..00000000
--- a/test/aarch64/postpass_tests/postpass_exec_c_test.sh
+++ /dev/null
@@ -1,36 +0,0 @@
-#!/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
diff --git a/test/aarch64/c/add_return.c b/test/gourdinl/c/add_return.c
index c29aeb16..c29aeb16 100644
--- a/test/aarch64/c/add_return.c
+++ b/test/gourdinl/c/add_return.c
diff --git a/test/aarch64/c/addresses.c b/test/gourdinl/c/addresses.c
index e3cb5201..e3cb5201 100644
--- a/test/aarch64/c/addresses.c
+++ b/test/gourdinl/c/addresses.c
diff --git a/test/aarch64/c/arith.c b/test/gourdinl/c/arith.c
index 02df141b..02df141b 100644
--- a/test/aarch64/c/arith.c
+++ b/test/gourdinl/c/arith.c
diff --git a/test/aarch64/c/arith_print.c b/test/gourdinl/c/arith_print.c
index d404a151..d404a151 100644
--- a/test/aarch64/c/arith_print.c
+++ b/test/gourdinl/c/arith_print.c
diff --git a/test/aarch64/c/armstrong.c b/test/gourdinl/c/armstrong.c
index c5d838f9..c5d838f9 100644
--- a/test/aarch64/c/armstrong.c
+++ b/test/gourdinl/c/armstrong.c
diff --git a/test/aarch64/c/array1.c b/test/gourdinl/c/array1.c
index 5840ca66..5840ca66 100644
--- a/test/aarch64/c/array1.c
+++ b/test/gourdinl/c/array1.c
diff --git a/test/aarch64/c/array2.c b/test/gourdinl/c/array2.c
index 389e1596..389e1596 100644
--- a/test/aarch64/c/array2.c
+++ b/test/gourdinl/c/array2.c
diff --git a/test/aarch64/c/biggest_of_3_int.c b/test/gourdinl/c/biggest_of_3_int.c
index 346908fc..346908fc 100644
--- a/test/aarch64/c/biggest_of_3_int.c
+++ b/test/gourdinl/c/biggest_of_3_int.c
diff --git a/test/aarch64/c/bitwise1.c b/test/gourdinl/c/bitwise1.c
index d20641de..d20641de 100644
--- a/test/aarch64/c/bitwise1.c
+++ b/test/gourdinl/c/bitwise1.c
diff --git a/test/aarch64/c/cpintarray.c b/test/gourdinl/c/cpintarray.c
index 8049fdfb..8049fdfb 100644
--- a/test/aarch64/c/cpintarray.c
+++ b/test/gourdinl/c/cpintarray.c
diff --git a/test/aarch64/c/enum1.c b/test/gourdinl/c/enum1.c
index d1f6b48d..d1f6b48d 100644
--- a/test/aarch64/c/enum1.c
+++ b/test/gourdinl/c/enum1.c
diff --git a/test/aarch64/c/enum2.c b/test/gourdinl/c/enum2.c
index a18acb80..a18acb80 100644
--- a/test/aarch64/c/enum2.c
+++ b/test/gourdinl/c/enum2.c
diff --git a/test/aarch64/c/floop.c b/test/gourdinl/c/floop.c
index 30270892..30270892 100644
--- a/test/aarch64/c/floop.c
+++ b/test/gourdinl/c/floop.c
diff --git a/test/aarch64/c/floor.c b/test/gourdinl/c/floor.c
index 33a57af3..33a57af3 100644
--- a/test/aarch64/c/floor.c
+++ b/test/gourdinl/c/floor.c
diff --git a/test/aarch64/c/funcs.c b/test/gourdinl/c/funcs.c
index 49e610d6..49e610d6 100644
--- a/test/aarch64/c/funcs.c
+++ b/test/gourdinl/c/funcs.c
diff --git a/test/aarch64/c/hello.c b/test/gourdinl/c/hello.c
index 0279269e..0279269e 100644
--- a/test/aarch64/c/hello.c
+++ b/test/gourdinl/c/hello.c
diff --git a/test/aarch64/c/if.c b/test/gourdinl/c/if.c
index 7d2e249a..7d2e249a 100644
--- a/test/aarch64/c/if.c
+++ b/test/gourdinl/c/if.c
diff --git a/test/aarch64/c/msb_pos.c b/test/gourdinl/c/msb_pos.c
index f2e7fe09..f2e7fe09 100644
--- a/test/aarch64/c/msb_pos.c
+++ b/test/gourdinl/c/msb_pos.c
diff --git a/test/aarch64/c/power2.c b/test/gourdinl/c/power2.c
index 64707df9..64707df9 100644
--- a/test/aarch64/c/power2.c
+++ b/test/gourdinl/c/power2.c
diff --git a/test/aarch64/c/prime.c b/test/gourdinl/c/prime.c
index 6c51db32..6c51db32 100644
--- a/test/aarch64/c/prime.c
+++ b/test/gourdinl/c/prime.c
diff --git a/test/aarch64/c/random.c b/test/gourdinl/c/random.c
index 50aa5737..50aa5737 100644
--- a/test/aarch64/c/random.c
+++ b/test/gourdinl/c/random.c
diff --git a/test/aarch64/c/simple_op.c b/test/gourdinl/c/simple_op.c
index 7c43b081..7c43b081 100644
--- a/test/aarch64/c/simple_op.c
+++ b/test/gourdinl/c/simple_op.c
diff --git a/test/aarch64/c/wloop.c b/test/gourdinl/c/wloop.c
index 5ba67419..5ba67419 100644
--- a/test/aarch64/c/wloop.c
+++ b/test/gourdinl/c/wloop.c
diff --git a/test/gourdinl/clause.h b/test/gourdinl/clause.h
new file mode 100644
index 00000000..3eb44402
--- /dev/null
+++ b/test/gourdinl/clause.h
@@ -0,0 +1,12 @@
+typedef struct {
+  int b;
+  int a;
+} * CLAUSE;
+__inline__ int g(CLAUSE c) { return c->b; }
+__inline__ int d(CLAUSE c) { return c->a; }
+__inline__ void clause_SetNumOfConsLits(CLAUSE c, int e) {
+  c->b = e;
+  c->a = e;
+}
+__inline__ int f(CLAUSE c) { return g(c) + d(c); }
+__inline__ int clause_LastLitIndex(c) { return f(c); }
diff --git a/test/gourdinl/clause2.c b/test/gourdinl/clause2.c
new file mode 100644
index 00000000..42cd0fa6
--- /dev/null
+++ b/test/gourdinl/clause2.c
@@ -0,0 +1,23 @@
+#include "clause.h"
+int a, b;
+void c();
+void h() {
+  int f = clause_LastLitIndex(d);
+  a = clause_LastLitIndex(0);
+  if (f)
+    if (a)
+      1;
+}
+void i() {
+  CLAUSE e = 0;
+  int *g[] = {h, c};
+  for (; b;)
+    l(e);
+}
+void m() {
+  int k, j;
+  for (; k <= 0;)
+    ;
+  clause_SetNumOfConsLits(0, j);
+  n(0 - j);
+}
diff --git a/test/gourdinl/cond_exp_mini_cse.c b/test/gourdinl/cond_exp_mini_cse.c
new file mode 100644
index 00000000..3a2ce9c3
--- /dev/null
+++ b/test/gourdinl/cond_exp_mini_cse.c
@@ -0,0 +1,6 @@
+int main(int x, int y, int* t) {
+  if (x + *t < 7)
+    if (y < 7)
+      return 421;
+  return 0;
+}
diff --git a/test/gourdinl/cscript.sh b/test/gourdinl/cscript.sh
new file mode 100755
index 00000000..8bf3a613
--- /dev/null
+++ b/test/gourdinl/cscript.sh
@@ -0,0 +1,20 @@
+#!/bin/bash
+
+/home/yuki/Work/VERIMAG/Compcert_neutral/ccomp -stdlib ../../runtime -dparse -dclight -S -fstruct-return   -c clause2.c > log 2>&1
+
+b1=$(cat log | ack "LDP_CONSEC_PEEP_IMM_DEC_ldr64")
+sb1=$?
+b2=$(cat log | ack "LDP_BACK_SPACED_PEEP_IMM_DEC_ldr32")
+sb2=$?
+b3=$(cat log | ack "STP_FORW_SPACED_PEEP_IMM_INC_str32")
+sb3=$?
+b4=$(cat log | ack "STP_CONSEC_PEEP_IMM_INC_str64")
+sb4=$?
+
+#if [ "$sb1" == 0 ] && [ "$sb2" == 0 ] && [ "$sb3" == 0 ] && [ "$sb4" == 0 ]
+if [ "$sb1" == 0 ] && [ "$sb2" == 0 ] && [ "$sb3" == 0 ] && [ "$sb4" == 0 ]
+then
+  exit 0
+else
+  exit 1
+fi
diff --git a/test/gourdinl/fp_init.c b/test/gourdinl/fp_init.c
new file mode 100644
index 00000000..1d835994
--- /dev/null
+++ b/test/gourdinl/fp_init.c
@@ -0,0 +1,7 @@
+int main (float *x) {
+  double a = 1.0;
+  float b = 1.0f;
+  printf("%f", a);
+  *x = b;
+  return b;
+}
diff --git a/test/gourdinl/gen_asm_files.sh b/test/gourdinl/gen_asm_files.sh
new file mode 100755
index 00000000..08cd4b3d
--- /dev/null
+++ b/test/gourdinl/gen_asm_files.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+../../ccomp -S clause2.c -o clause2.nopostpass.noph.s -fno-coalesce-mem -fno-postpass
+../../ccomp -S clause2.c -o clause2.nopostpass.ph.s -fcoalesce-mem -fno-postpass
+../../ccomp -S clause2.c -o clause2.noph.s -fno-coalesce-mem
+../../ccomp -S clause2.c -o clause2.ph.s -fcoalesce-mem
diff --git a/test/monniaux/profiling/compcert_profiling.dat b/test/monniaux/profiling/compcert_profiling.dat
new file mode 100644
index 00000000..bd2f90da
--- /dev/null
+++ b/test/monniaux/profiling/compcert_profiling.dat
diff --git a/test/monniaux/profiling/test_profiling b/test/monniaux/profiling/test_profiling
new file mode 100755
index 00000000..33e22d11
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling
diff --git a/test/monniaux/profiling/test_profiling.c b/test/monniaux/profiling/test_profiling.c
new file mode 100644
index 00000000..013b1d68
--- /dev/null
+++ b/test/monniaux/profiling/test_profiling.c
@@ -0,0 +1,15 @@
+#include <stdlib.h>
+#include <stdio.h>
+
+int main(int argc, char **argv) {
+  if (argc < 2) return 1;
+  int i = atoi(argv[1]);
+  if (i > 0) {
+    printf("positive\n");
+  } else if (i==0) {
+    printf("zero\n");
+  } else {
+    printf("negative\n");
+  }
+  return 0;
+}