Updated the branch and implemented the suggested changes.

3 files changed, 78 insertions, 44 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index dd434c02..4e8a411a 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -1,3 +1,4 @@
+
 (* *********************************************************************)
 (*                                                                     *)
 (*              The Compcert verified compiler                         *)
@@ -206,23 +207,30 @@ Inductive instruction : Type :=
   | Pbtbl: ireg -> list label -> instruction       (**r N-way branch through a jump table *)
   | Pbuiltin: external_function -> list preg -> list preg -> instruction  (**r built-in function *)
   | Pannot: external_function -> list (annot_arg preg) -> instruction (**r annotation statement *)
-  | Padc: ireg -> ireg -> shift_op -> instruction   (**r add with carry *)
-  | Pcfi_adjust: int -> instruction                 (**r .cfi_adjust debug directive *)
-  | Pclz: preg -> preg -> instruction               (**r count leading zeros. *)
-  | Pfsqrt: freg -> freg -> instruction             (**r floating-point square root. *)
-  | Prev: preg -> preg -> instruction               (**r reverse bytes and reverse bits. *)
-  | Prev16: preg -> preg -> instruction             (**r reverse bytes and reverse bits. *)
-  | Prsc: ireg -> ireg -> shift_op -> instruction (**r reverse subtract without carry. *)
-  | Psbc: ireg -> ireg -> shift_op -> instruction   (**r add with carry *)
+  | Padc: ireg -> ireg -> shift_op -> instruction     (**r add with carry *)
+  | Pcfi_adjust: int -> instruction                   (**r .cfi_adjust debug directive *)
+  | Pclz: preg -> preg -> instruction                 (**r count leading zeros. *)
+  | Pfsqrt: freg -> freg -> instruction               (**r floating-point square root. *)
+  | Prev: preg -> preg -> instruction                 (**r reverse bytes and reverse bits. *)
+  | Prev16: preg -> preg -> instruction               (**r reverse bytes and reverse bits. *)
+  | Prsc: ireg -> ireg -> shift_op -> instruction     (**r reverse subtract without carry. *)
+  | Psbc: ireg -> ireg -> shift_op -> instruction     (**r add with carry *)
   (* Add, sub, rsb versions with s suffix *)
-  | Padds: ireg -> ireg -> shift_op -> instruction  (**r integer addition with update of condition flags *)
-  | Psubs: ireg -> ireg -> shift_op -> instruction  (**r integer subtraction with update of condition flags *)
-  | Prsbs: ireg -> ireg -> shift_op -> instruction  (**r integer reverse subtraction with update of condition flags *)
-  | Pdmb: instruction                               (**r data memory barrier *)
-  | Pdsb: instruction                               (**r data synchronization barrier *)
-  | Pisb: instruction                               (**r instruction synchronization barrier *)
-  | Pbne: label -> instruction.                     (**r branch if negative macro *)
-
+  | Padds: ireg -> ireg -> shift_op -> instruction    (**r integer addition with update of condition flags *)
+  | Psubs: ireg -> ireg -> shift_op -> instruction    (**r integer subtraction with update of condition flags *)
+  | Prsbs: ireg -> ireg -> shift_op -> instruction    (**r integer reverse subtraction with update of condition flags *)
+  | Pdmb: instruction                                 (**r data memory barrier *)
+  | Pdsb: instruction                                 (**r data synchronization barrier *)
+  | Pisb: instruction                                 (**r instruction synchronization barrier *)
+  | Pbne: label -> instruction                        (**r branch if negative macro *)
+  | Pldr_p: ireg -> ireg -> shift_op -> instruction   (**r int32 load with post increment *)
+  | Pldrb_p: ireg -> ireg -> shift_op -> instruction  (**r unsigned int8 load with post increment *)
+  | Pldrh_p: ireg -> ireg -> shift_op -> instruction  (**r unsigned int16 load with post increment *)
+  | Pstr_p: ireg -> ireg -> shift_op -> instruction   (**r int32 store with post increment *)
+  | Pstrb_p: ireg -> ireg -> shift_op -> instruction  (**r unsigned int8 store with post increment *)
+  | Pstrh_p: ireg -> ireg -> shift_op -> instruction. (**r unsigned int16 store with post increment *)
+ 
+ 
 
 (** The pseudo-instructions are the following:
 
@@ -758,7 +766,13 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pdmb
   | Pdsb
   | Pisb
-  | Pbne _ =>
+  | Pbne _
+  | Pldr_p _ _ _
+  | Pldrb_p _ _ _
+  | Pldrh_p _ _ _
+  | Pstr_p _ _ _
+  | Pstrb_p _ _ _
+  | Pstrh_p _ _ _ =>
     Stuck
   end.
 
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 95f35f37..b4508ace 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -91,22 +91,22 @@ let expand_annot_val txt targ args res =
 let expand_builtin_memcpy_small sz al src dst =
   let rec copy ofs sz  =
     if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin
-	emit (Pfldd (FR7,src,ofs));
-	emit (Pfstd (FR7,dst,ofs));
-	copy (Int.add ofs _8) (sz - 8)
-      end else if sz >= 4 && al >= 4 then begin
-	emit (Pldr (IR14,src,SOimm ofs));
-	emit (Pstr (IR14,dst,SOimm ofs));
-	copy (Int.add ofs _4) (sz - 4)
-      end else if sz >= 2 && al >= 2 then begin
-	emit (Pldrh (IR14,src,SOimm ofs));
-	emit (Pstrh (IR14,dst,SOimm ofs));
-	copy (Int.add ofs _2) (sz - 2)
-      end else if sz >= 1 then begin
-	emit (Pldrb (IR14,src,SOimm ofs));
-	emit (Pstrb (IR14,dst,SOimm ofs));
-	copy (Int.add ofs _1) (sz - 1)
-      end else
+      emit (Pfldd (FR7,src,ofs));
+      emit (Pfstd (FR7,dst,ofs));
+      copy (Int.add ofs _8) (sz - 8)
+    end else if sz >= 4 && al >= 4 then begin
+      emit (Pldr (IR14,src,SOimm ofs));
+      emit (Pstr (IR14,dst,SOimm ofs));
+      copy (Int.add ofs _4) (sz - 4)
+    end else if sz >= 2 && al >= 2 then begin
+      emit (Pldrh (IR14,src,SOimm ofs));
+      emit (Pstrh (IR14,dst,SOimm ofs));
+      copy (Int.add ofs _2) (sz - 2)
+    end else if sz >= 1 then begin
+      emit (Pldrb (IR14,src,SOimm ofs));
+      emit (Pstrb (IR14,dst,SOimm ofs));
+      copy (Int.add ofs _1) (sz - 1)
+    end else
       () in
   copy _0 sz
 
@@ -116,9 +116,9 @@ let expand_builtin_memcpy_big sz al src dst =
   assert (src = IR2);
   assert (dst = IR3);
   let (load, store, chunksize) =
-    if al >= 4 then (Pldr (IR12,src,SOimm _4), Pstr (IR12,dst,SOimm _4) , 4)
-    else if al = 2 then (Pldrh (IR12,src,SOimm _2), Pstrh (IR12,dst,SOimm _2), 2)
-    else (Pldrb (IR12,src,SOimm _1), Pstrb (IR12,dst,SOimm _1), 1) in
+    if al >= 4 then (Pldr_p (IR12,src,SOimm _4), Pstr_p (IR12,dst,SOimm _4) , 4)
+    else if al = 2 then (Pldrh_p (IR12,src,SOimm _2), Pstrh_p (IR12,dst,SOimm _2), 2)
+    else (Pldrb_p (IR12,src,SOimm _1), Pstrb_p (IR12,dst,SOimm _1), 1) in
   expand_movimm IR14 (coqint_of_camlint (Int32.of_int (sz / chunksize)));
   let lbl = new_label () in
   emit (Plabel lbl);
@@ -239,14 +239,17 @@ let expand_builtin_inline name args res =
      emit (Pfsqrt (res,a1))
   (* 64-bit integer arithmetic *)
   | "__builtin_negl", [IR ah;IR al], [IR rh; IR rl] ->
-     emit (Prsbs (rl,al,SOimm _0));
-     if !Clflags.option_mthumb then begin
-	 emit (Pmvn (rh,SOreg ah));
-	 emit (Padc (rh,rh,SOimm _0))
-       end else
-       begin
-	 emit (Prsc (rh,ah,SOimm _0))
-       end
+      expand_int64_arith (rl = ah ) rl (fun rl ->
+        emit (Prsbs (rl,al,SOimm _0));
+        (* No "rsc" instruction in Thumb2.  Emulate based on
+           rsc a, b, #0 == a <- AddWithCarry(~b, 0, carry)
+           == mvn a, b; adc a, a, #0 *)
+        if !Clflags.option_mthumb then begin
+	  emit (Pmvn (rh,SOreg ah));
+	  emit (Padc (rh,rh,SOimm _0))
+        end else begin
+	  emit (Prsc (rh,ah,SOimm _0))
+        end)
   | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
      expand_int64_arith (rl = ah || rl = bh) rl
 			(fun rl ->
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 88261940..f8d72836 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -539,6 +539,12 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           fprintf oc "	ldrb	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
       | Pldrh(r1, r2, sa) ->
           fprintf oc "	ldrh	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
+      | Pldr_p(r1, r2, sa)  ->
+          fprintf oc "	ldr	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1
+      | Pldrb_p(r1, r2, sa) ->
+          fprintf oc "	ldrb	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1
+      | Pldrh_p(r1, r2, sa) ->
+          fprintf oc "	ldrh	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1
       | Pldrsb(r1, r2, sa) ->
           fprintf oc "	ldrsb	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
       | Pldrsh(r1, r2, sa) ->
@@ -591,6 +597,17 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           fprintf oc "	strb	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
       | Pstrh(r1, r2, sa) ->
           fprintf oc "	strh	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
+      | Pstr_p(r1, r2, sa) ->
+          fprintf oc "	str	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa;
+          begin match r1, r2, sa with
+          | IR14, IR13, SOimm n -> cfi_rel_offset oc "lr" (camlint_of_coqint n)
+          | _ -> ()
+          end;
+          1
+      | Pstrb_p(r1, r2, sa) ->
+          fprintf oc "	strb	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1
+      | Pstrh_p(r1, r2, sa) ->
+          fprintf oc "	strh	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1
       | Psdiv ->
           if Opt.hardware_idiv then begin
             fprintf oc "	sdiv	r0, r0, r1\n"; 1