Some tests and load/store instr

10 files changed, 291 insertions, 33 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index c7170edc..8e095553 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -235,16 +235,6 @@ Definition loadimm64 (rd: ireg) (n: int64) (k: bcode) : bcode :=
 
 (* STUB inspired from kvx/Asmblockgen.v and the reference aarch64/Asmgen.v (see below) *)
 
-(** Translation of addressing modes *)
-
-(*Definition offset_representable (sz: Z) (ofs: int64) : bool :=*)
-  (*let isz := Int64.repr sz in*)
-  (*[>* either unscaled 9-bit signed <]*)
-  (*Int64.eq ofs (Int64.sign_ext 9 ofs) ||*)
-  (*[>* or scaled 12-bit unsigned <]*)
-  (*(Int64.eq (Int64.modu ofs isz) Int64.zero*)
-   (*&& Int64.ltu ofs (Int64.shl isz (Int64.repr 12))).*)
-
 Definition indexed_memory_access (insn: addressing -> basic)
                                  (sz: Z) (base: iregsp) (ofs: ptrofs) (k: bblocks) : bblocks :=
   let ofs := Ptrofs.to_int64 ofs in
@@ -255,6 +245,30 @@ Definition indexed_memory_access_bc (insn: addressing -> basic)
   let ofs := Ptrofs.to_int64 ofs in
   insn (ADimm base ofs) :: k.
 
+Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) :=
+  match ty, preg_of dst with
+  | Tint,    IR' rd => OK (indexed_memory_access_bc (PLoad Pldrw rd) 4 base ofs k)
+  | Tlong,   IR' rd => OK (indexed_memory_access_bc (PLoad Pldrx rd) 8 base ofs k)
+  | Tsingle, FR' rd => OK (indexed_memory_access_bc (PLoad Pldrs rd) 4 base ofs k)
+  | Tfloat,  FR' rd => OK (indexed_memory_access_bc (PLoad Pldrd rd) 8 base ofs k)
+  | Tany32,  IR' rd => OK (indexed_memory_access_bc (PLoad Pldrw_a rd) 4 base ofs k)
+  | Tany64,  IR' rd => OK (indexed_memory_access_bc (PLoad Pldrx_a rd) 8 base ofs k)
+  | Tany64,  FR' rd => OK (indexed_memory_access_bc (PLoad Pldrd_a rd) 8 base ofs k)
+  | _, _           => Error (msg "Asmgen.loadind")
+  end.
+
+Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: bcode) :=
+  match ty, preg_of src with
+  | Tint,    IR' rd => OK (indexed_memory_access_bc (PStore Pstrw rd) 4 base ofs k)
+  | Tlong,   IR' rd => OK (indexed_memory_access_bc (PStore Pstrx rd) 8 base ofs k)
+  | Tsingle, FR' rd => OK (indexed_memory_access_bc (PStore Pstrs rd) 4 base ofs k)
+  | Tfloat,  FR' rd => OK (indexed_memory_access_bc (PStore Pstrd rd) 8 base ofs k)
+  | Tany32,  IR' rd => OK (indexed_memory_access_bc (PStore Pstrw_a rd) 4 base ofs k)
+  | Tany64,  IR' rd => OK (indexed_memory_access_bc (PStore Pstrx_a rd) 8 base ofs k)
+  | Tany64,  FR' rd => OK (indexed_memory_access_bc (PStore Pstrd_a rd) 8 base ofs k)
+  | _, _           => Error (msg "Asmgen.storeind")
+  end.
+
 Definition loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bblocks): bblocks :=
   indexed_memory_access (PLoad Pldrx dst) 8 base ofs k.
 
@@ -594,6 +608,12 @@ Definition transl_cond_branch
 Definition transl_op
               (op: operation) (args: list mreg) (res: mreg) (k: bcode) :=
   match op, args with
+  | Omove, a1 :: nil =>
+      match preg_of res, preg_of a1 with
+      | IR' r, IR' a => OK (Pmov r a ::bi k)
+      | FR' r, FR' a => OK (Pfmov r a ::bi k)
+      |  _  ,  _   => Error(msg "Asmgenblock.Omove")
+      end
   | Ointconst n, nil =>
       do rd <- ireg_of res;
       OK (loadimm32 rd n k)
@@ -990,18 +1010,123 @@ Definition transl_op
   | _, _ => Error(msg "Asmgenblock.transl_op")
   end.
 
+(** Translation of addressing modes *)
+
+Definition offset_representable (sz: Z) (ofs: int64) : bool :=
+  let isz := Int64.repr sz in
+  (** either unscaled 9-bit signed *)
+  Int64.eq ofs (Int64.sign_ext 9 ofs) ||
+  (** or scaled 12-bit unsigned *)
+  (Int64.eq (Int64.modu ofs isz) Int64.zero
+   && Int64.ltu ofs (Int64.shl isz (Int64.repr 12))).
+ 
+Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg)
+                             (insn: Asm.addressing -> basic) (k: bcode) : res bcode :=
+  match addr, args with
+  | Aindexed ofs, a1 :: nil =>
+      do r1 <- ireg_of a1;
+       if offset_representable sz ofs then
+        OK (insn (ADimm r1 ofs) ::bi k)
+      else
+        OK (loadimm64 X16 ofs (insn (ADreg r1 X16) ::bi k))
+  | Aindexed2, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (insn (ADreg r1 r2) ::bi k)
+  | Aindexed2shift a, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      if Int.eq a Int.zero then
+        OK (insn (ADreg r1 r2) ::bi k)
+      else if Int.eq (Int.shl Int.one a) (Int.repr sz) then
+        OK (insn (ADlsl r1 r2 a) ::bi k)
+      else
+        OK (Padd X (SOlsl a) X16 r1 r2 ::bi insn (ADimm X16 Int64.zero) ::bi k)
+  | Aindexed2ext x a, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      if Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz) then
+        OK (insn (match x with Xsgn32 => ADsxt r1 r2 a
+                             | Xuns32 => ADuxt r1 r2 a end) ::bi k)
+      else
+        OK (arith_extended Paddext (Padd X) X16 r1 r2 x a
+                           (insn (ADimm X16 Int64.zero) ::bi k))
+  | Aglobal id ofs, nil =>
+      assertion (negb (Archi.pic_code tt));
+      if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz
+      then OK (Padrp id ofs X16 ::bi insn (ADadr X16 id ofs) ::bi k)
+      else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) ::bi k))
+  | Ainstack ofs, nil =>
+      let ofs := Ptrofs.to_int64 ofs in
+      if offset_representable sz ofs then
+        OK (insn (ADimm XSP ofs) ::bi k)
+      else
+        OK (loadimm64 X16 ofs (insn (ADreg XSP X16) ::bi k))
+  | _, _ =>
+      Error(msg "Asmgen.transl_addressing")
+  end.
+
+(** Translation of loads and stores *)
+
+Definition transl_load (chunk: memory_chunk) (addr: Op.addressing)
+                       (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
+  match chunk with
+  | Mint8unsigned =>
+      do rd <- ireg_of dst; transl_addressing 1 addr args (PLoad (Pldrb W) rd) k
+  | Mint8signed =>
+      do rd <- ireg_of dst; transl_addressing 1 addr args (PLoad (Pldrsb W) rd) k
+  | Mint16unsigned =>
+      do rd <- ireg_of dst; transl_addressing 2 addr args (PLoad (Pldrh W) rd) k
+  | Mint16signed =>
+      do rd <- ireg_of dst; transl_addressing 2 addr args (PLoad (Pldrsh W) rd) k
+  | Mint32 =>
+      do rd <- ireg_of dst; transl_addressing 4 addr args (PLoad Pldrw rd) k
+  | Mint64 =>
+      do rd <- ireg_of dst; transl_addressing 8 addr args (PLoad Pldrx rd) k
+  | Mfloat32 =>
+      do rd <- freg_of dst; transl_addressing 4 addr args (PLoad Pldrs rd) k
+  | Mfloat64 =>
+      do rd <- freg_of dst; transl_addressing 8 addr args (PLoad Pldrd rd) k
+  | Many32 =>
+      do rd <- ireg_of dst; transl_addressing 4 addr args (PLoad Pldrw_a rd) k
+  | Many64 =>
+      do rd <- ireg_of dst; transl_addressing 8 addr args (PLoad Pldrx_a rd) k
+  end.
+
+Definition transl_store (chunk: memory_chunk) (addr: Op.addressing)
+                        (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
+  match chunk with
+  | Mint8unsigned | Mint8signed =>
+      do r1 <- ireg_of src; transl_addressing 1 addr args (PStore Pstrb r1) k
+  | Mint16unsigned | Mint16signed =>
+      do r1 <- ireg_of src; transl_addressing 2 addr args (PStore Pstrh r1) k
+  | Mint32 =>
+      do r1 <- ireg_of src; transl_addressing 4 addr args (PStore Pstrw r1) k
+  | Mint64 =>
+      do r1 <- ireg_of src; transl_addressing 8 addr args (PStore Pstrx r1) k
+  | Mfloat32 =>
+      do r1 <- freg_of src; transl_addressing 4 addr args (PStore Pstrs r1) k
+  | Mfloat64 =>
+      do r1 <- freg_of src; transl_addressing 8 addr args (PStore Pstrd r1) k
+  | Many32 =>
+      do r1 <- ireg_of src; transl_addressing 4 addr args (PStore Pstrw_a r1) k
+  | Many64 =>
+      do r1 <- ireg_of src; transl_addressing 8 addr args (PStore Pstrx_a r1) k
+  end.
+
 (** Translation of a Machblock instruction. *)
 
 Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
                               (ep: bool) (k: bcode) :=
   match i with
+  | MBgetstack ofs ty dst =>
+      loadind XSP ofs ty dst k
+  | MBsetstack src ofs ty =>
+      storeind src XSP ofs ty k
   | MBop op args res =>
       transl_op op args res k
+  | MBload _ chunk addr args dst =>
+      transl_load chunk addr args dst k
+  (*| MBstore chunk addr args src =>*)
+      (*transl_store chunk addr args src k*)
   | _ => Error(msg "Not implemented yet")
-  (*| MBgetstack ofs ty dst =>*)
-      (*loadind SP ofs ty dst k*)
-  (*| MBsetstack src ofs ty =>*)
-      (*storeind src SP ofs ty k*)
   (*| MBgetparam ofs ty dst =>*)
       (*[> load via the frame pointer if it is valid <]*)
       (*do c <- loadind FP ofs ty dst k;*)
@@ -1009,10 +1134,6 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
                 (*else (loadind_ptr SP f.(fn_link_ofs) FP) ::i c)*)
   (*| MBop op args res =>*)
       (*transl_op op args res k*)
-  (*| MBload trap chunk addr args dst =>*)
-      (*transl_load trap chunk addr args dst k*)
-  (*| MBstore chunk addr args src =>*)
-      (*transl_store chunk addr args src k*)
   end.
 
 (** Translation of a code sequence *)
@@ -1030,15 +1151,17 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
 
 Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
   match i with
+  | MBgetstack ofs ty dst => before && negb (mreg_eq dst R29)
   (*| Msetstack src ofs ty => before*)
   (*| Mgetparam ofs ty dst => negb (mreg_eq dst R29)*)
   | MBop op args res => before && negb (mreg_eq res R29)
+  | MBload trapping_mode chunk addr args dst => before && negb (mreg_eq dst R29)
   | _ => false
   end.
 
 Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) (k: bcode):=
   match il with
-  | nil => OK nil
+  | nil => OK (k)
   | i1 :: il' =>
       do k1 <- transl_basic_code f il' (it1_is_parent it1p i1) k;
       transl_instr_basic f i1 it1p k1
@@ -1083,18 +1206,14 @@ Qed.
 
 Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) (ep: bool) : res (bcode*control) :=
   match ctl with
-  | MBcall sig (inl r) => Error (msg "NYI MBcall sig (inl r)")
-  | MBcall sig (inr symb) => Error (msg "NYI MBcall sig (inr symb)")
+  | MBcall sig (inl r) => do r1 <- ireg_of r; OK (nil, PCtlFlow (Pblr r1 sig))
+  | MBcall sig (inr symb) => OK (nil, PCtlFlow (Pbl symb sig))
   | MBtailcall sig (inr symb) => Error (msg "NYI MBtailcall sig (inr symb)")
   | MBtailcall sig (inl r) => Error (msg "NYI MBtailcall sig (inl r)")
   | MBbuiltin ef args res => Error (msg "NYI MBbuiltin ef args res")
   | MBgoto lbl => OK (nil, PCtlFlow (Pb lbl))
   | MBcond cond args lbl => transl_cond_branch cond args lbl nil
   | MBreturn => OK (make_epilogue f, PCtlFlow (Pret RA))
-      (*match make_epilogue f (Pret RA ::c nil) with*)
-      (*| nil => OK(nil,None)*)
-      (*| b :: k  => OK(body b,exit b)*)
-      (*end*)
   | MBjumptable arg tbl => Error (msg "NYI MBjumptable arg tbl")
   end.
 
@@ -1108,7 +1227,7 @@ Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool
   let stub := false in (* TODO: FIXME *) 
   do (bdy, ex) <- transl_exit f fb.(Machblock.exit) stub;
   do bdy' <- transl_basic_code f fb.(Machblock.body) ep bdy;
-  OK (cons_bblocks fb.(Machblock.header) (bdy' ++ bdy) ex k) 
+  OK (cons_bblocks fb.(Machblock.header) bdy' ex k) 
   .
 
 Fixpoint transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): res bblocks :=
diff --git a/test/aarch64/asmb_aarch64_gen_test.sh b/test/aarch64/asmb_aarch64_gen_test.sh
index 5a839539..19149265 100755
--- a/test/aarch64/asmb_aarch64_gen_test.sh
+++ b/test/aarch64/asmb_aarch64_gen_test.sh
@@ -8,26 +8,25 @@ while getopts ':c' 'OPTKEY'; do
 done
 
 FILES=c/*
-CCOMP_BBLOCKS=../../ccomp
-CCOMP_REF=../../../CompCert_master/ccomp
+CCOMP_BBLOCKS="../../ccomp"
+CCOMP_REF="../../../CompCert_master/ccomp"
 for f in $FILES
 do
-  echo "Processing $f file... $(basename $f)"
-
   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 '^//*' <(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 test OK"
+    echo "[$BNAME] OK"
   elif [ $error -eq 1 ]
   then
-    echo "$BNAME test FAIL"
+    echo "[$BNAME] FAIL"
     diff -I '^//*' -y $SNAME $SREFNAME
   else
     echo "[WARNING] There was something wrong with the diff command !"
diff --git a/test/aarch64/c/biggest_of_3_int.c b/test/aarch64/c/biggest_of_3_int.c
new file mode 100644
index 00000000..346908fc
--- /dev/null
+++ b/test/aarch64/c/biggest_of_3_int.c
@@ -0,0 +1,10 @@
+int main(int a, int b, int c) {
+  if ((a > b) && (a > c)) {
+    return a;
+  } else if (b > c) {
+    return b;
+  } else {
+    return c;
+  }
+  return 0;
+}
diff --git a/test/aarch64/c/floop.c b/test/aarch64/c/floop.c
new file mode 100644
index 00000000..30270892
--- /dev/null
+++ b/test/aarch64/c/floop.c
@@ -0,0 +1,8 @@
+int main(int x)
+{
+  int y = 4;
+  int s = 23;
+  for(int i = 0; i <= x; i++)
+    y << s;
+  return y;
+}
diff --git a/test/aarch64/c/floor.c b/test/aarch64/c/floor.c
new file mode 100644
index 00000000..33a57af3
--- /dev/null
+++ b/test/aarch64/c/floor.c
@@ -0,0 +1,29 @@
+int main(int n)
+{
+  int x = 1, i;
+
+  /* for positive values */
+  if (n > 0)
+  {
+    for (; x <= n >> 1;)
+    {
+      x = x << 1;
+    }
+    n = x;
+  }
+  /* for negative values */
+  else
+  {
+    n = ~n;
+    n = n + 1;
+    for (; x <= n >> 1;)
+    {
+      x = x << 1;
+    }
+    x = x << 1;
+    x = ~x;
+    x = x + 1;
+    n = x;
+  }
+  return n;
+}
diff --git a/test/aarch64/c/funcs.c b/test/aarch64/c/funcs.c
new file mode 100644
index 00000000..fba46033
--- /dev/null
+++ b/test/aarch64/c/funcs.c
@@ -0,0 +1,36 @@
+/* funcs.c  -- More examples of functions
+ */
+
+#include <stdio.h>
+
+int getint(void); /*It prompts user to enter an integer, which it returns*/
+
+int getmax(int a, int b, int c); /*It returns value of largest of a, b, c*/
+
+/* Main program: Using the various functions */
+int main (void) {
+  int x, y, z;
+
+  x = getint();
+  y = getint();
+  z = getint();
+  printf("The largest of %d, %d, and %d is %d\n", x, y, z, getmax(x,y,z));
+}
+
+int getint(void) {
+  int a;
+
+  /*printf("Please enter an integer > ");*/
+  scanf("%d", &a);
+  return(a);
+}
+
+int getmax(int a, int b, int c){
+  int m = a;
+
+  if (m<b)
+    m = b;
+  if (m<c)
+    m = c;
+  return(m);
+}
diff --git a/test/aarch64/c/hello.c b/test/aarch64/c/hello.c
new file mode 100644
index 00000000..0279269e
--- /dev/null
+++ b/test/aarch64/c/hello.c
@@ -0,0 +1,6 @@
+#include <stdio.h>
+
+int main(void) {
+  printf("Hello World!\n");
+  return 0; 
+}
diff --git a/test/aarch64/c/msb_pos.c b/test/aarch64/c/msb_pos.c
new file mode 100644
index 00000000..f2e7fe09
--- /dev/null
+++ b/test/aarch64/c/msb_pos.c
@@ -0,0 +1,20 @@
+/* Function to find the MSB bit position */
+int main(int n)
+{
+  int i = 0, bit;
+  while (i < 32)
+  {
+     bit = n & 0x80000000;
+     if (bit == -0x80000000)
+     {
+        bit = 1;
+     }
+
+     if (bit == 1) 
+       break;
+
+      n = n << 1;
+      i++;
+  }
+  return i;
+}
diff --git a/test/aarch64/c/prime.c b/test/aarch64/c/prime.c
new file mode 100644
index 00000000..6c51db32
--- /dev/null
+++ b/test/aarch64/c/prime.c
@@ -0,0 +1,23 @@
+/* prime1.c  It prompts the user to enter an integer N. It prints out
+ *           if it is a prime or not. If not, it prints out a factor of N.
+ */
+
+#include <stdio.h>
+
+int main(int n) {
+  int i;
+  int flag;
+
+  flag = 1;
+  for (i=2; (i<(n/2)) && flag; ) { /* May be we do not need to test
+			values of i greater than the square root of n? */
+    if ((n % i) == 0) /* If true n is divisible by i */
+      flag = 0;
+    else
+      i++;
+  }
+ 
+  if (flag)
+    return 1;
+  return 0;
+}
diff --git a/test/aarch64/c/wloop.c b/test/aarch64/c/wloop.c
new file mode 100644
index 00000000..5ba67419
--- /dev/null
+++ b/test/aarch64/c/wloop.c
@@ -0,0 +1,8 @@
+int main(int x)
+{
+  int y = 4;
+  int s = 23;
+  while(s < x)
+    y << s;
+  return y;
+}