22 files changed, 536 insertions, 24 deletions

diff --git a/arm/Archi.v b/arm/Archi.v
index 2ca79710..c334c2a7 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -96,3 +96,5 @@ Parameter abi: abi_kind.
 (** Whether instructions added with Thumb2 are supported. True for ARMv6T2
   and above. *)
 Parameter thumb2_support: bool.
+
+Definition has_notrap_loads := false.
diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index e850fed6..669d8c0c 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -177,6 +177,7 @@ let pp_instructions pp ic =
         | EF_annot_val _
         | EF_builtin _
         | EF_debug _
+        | EF_profiling _
         | EF_external _
         | EF_free
         | EF_malloc
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 15cbebec..83bce915 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -617,7 +617,7 @@ let expand_instruction instr =
 	   | EF_memcpy(sz, al) ->
 	      expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz))
 		(Int32.to_int (camlint_of_coqint al)) args
-	   | EF_annot _ | EF_debug _ | EF_inline_asm _ ->
+	   | EF_annot _ | EF_debug _ | EF_inline_asm _ | EF_profiling _ ->
               emit instr
 	   | _ ->
               assert false
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 1a1e7f2f..f428feea 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -481,6 +481,9 @@ Definition transl_op
       do r <- ireg_of res; do r1 <- ireg_of a1;
       if Int.eq n Int.zero then
         OK (Pmov r (SOreg r1) :: k)
+      else if Int.eq n Int.one then
+        OK (Padd IR14 r1 (SOlsr r1 (Int.repr 31)) ::
+            Pmov r (SOasr IR14 n) :: k)
       else
         OK (Pmov IR14 (SOasr r1 (Int.repr 31)) ::
             Padd IR14 r1 (SOlsr IR14 (Int.sub Int.iwordsize n)) ::
@@ -689,8 +692,12 @@ Definition transl_memory_access_float
     None
     mk_immed addr args k.
 
-Definition transl_load (chunk: memory_chunk) (addr: addressing)
-                       (args: list mreg) (dst: mreg) (k: code) :=
+Definition transl_load (trap : trapping_mode)
+           (chunk: memory_chunk) (addr: addressing)
+           (args: list mreg) (dst: mreg) (k: code) :=
+  match trap with
+  | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on Arm")
+  | TRAP =>
   match chunk with
   | Mint8signed =>
       transl_memory_access_int Pldrsb mk_immed_mem_small dst addr args k
@@ -708,6 +715,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing)
       transl_memory_access_float Pfldd mk_immed_mem_float dst addr args k
   | _ =>
       Error (msg "Asmgen.transl_load")
+  end
   end.
 
 Definition transl_store (chunk: memory_chunk) (addr: addressing)
@@ -747,8 +755,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
           else loadind_int IR13 f.(fn_link_ofs) IR12 c)
   | Mop op args res =>
       transl_op op args res k
-  | Mload chunk addr args dst =>
-      transl_load chunk addr args dst k
+  | Mload trap chunk addr args dst =>
+      transl_load trap chunk addr args dst k
   | Mstore chunk addr args src =>
       transl_store chunk addr args src k
   | Mcall sig (inl arg) =>
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 93e0c6c2..67cfe0ae 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -303,6 +303,7 @@ Proof.
     eapply tail_nolabel_trans. 2: eapply loadind_label; eauto. unfold loadind_int; TailNoLabel.
   eapply transl_op_label; eauto.
   unfold transl_load, transl_memory_access_int, transl_memory_access_float in H.
+  destruct t; try discriminate.
   destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto.
   unfold transl_store, transl_memory_access_int, transl_memory_access_float in H.
   destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto.
@@ -618,6 +619,12 @@ Opaque loadind.
   split. eapply agree_set_undef_mreg; eauto. congruence.
   simpl; congruence.
 
+- (* Mload notrap1 *)
+  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
+
+- (* Mload notrap *)
+  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
+
 - (* Mstore *)
   assert (eval_addressing tge sp addr rs##args = Some a).
     rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index b94964a0..7a707f32 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -1264,15 +1264,32 @@ Local Transparent destroyed_by_op.
   destruct (rs x0) eqn: X0; simpl in H0; try discriminate.
   destruct (Int.ltu i (Int.repr 31)) eqn: LTU; inv H0.
   revert EQ2. predSpec Int.eq Int.eq_spec i Int.zero; intros EQ2.
+  {
   (* i = 0 *)
   inv EQ2. econstructor.
   split. apply exec_straight_one. simpl. reflexivity. auto.
   split. Simpl. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs.
   change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed. auto.
   intros. Simpl.
-  (* i <> 0 *)
-  inv EQ2.
-  assert (LTU': Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize = true).
+  }
+  { (* i <> 0 *)
+    revert EQ2. predSpec Int.eq Int.eq_spec i Int.one; intros EQ2.
+    {
+      inv EQ2.
+      econstructor; split.
+      eapply exec_straight_two; simpl; reflexivity.
+      split.
+      { rewrite X0.
+        rewrite Int.shrx1_shr by reflexivity.
+        Simpl.
+      }
+      { intros.
+        Simpl.
+      }
+    }
+    clear H0.
+    inv EQ2.
+    assert (LTU': Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize = true).
   {
     generalize (Int.ltu_inv _ _ LTU). intros.
     unfold Int.sub, Int.ltu. rewrite Int.unsigned_repr_wordsize.
@@ -1306,6 +1323,7 @@ Local Transparent destroyed_by_op.
   rewrite LTU'; simpl. rewrite LTU''; simpl.
   f_equal. symmetry. apply Int.shrx_shr_2. assumption.
   intros. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl.
+  }
   (* intoffloat *)
   econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
 Transparent destroyed_by_op.
@@ -1540,8 +1558,8 @@ Proof.
 Qed.
 
 Lemma transl_load_correct:
-  forall chunk addr args dst k c (rs: regset) a m v,
-  transl_load chunk addr args dst k = OK c ->
+  forall trap chunk addr args dst k c (rs: regset) a m v,
+  transl_load trap chunk addr args dst k = OK c ->
   eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
   Mem.loadv chunk m a = Some v ->
   exists rs',
@@ -1549,7 +1567,9 @@ Lemma transl_load_correct:
    /\ rs'#(preg_of dst) = v
    /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
-  intros. destruct chunk; simpl in H.
+  intros.
+  destruct trap; try (simpl in *; discriminate).
+  destruct chunk; simpl in H.
   eapply transl_load_int_correct; eauto.
   eapply transl_load_int_correct; eauto.
   eapply transl_load_int_correct; eauto.
diff --git a/arm/CSE2deps.v b/arm/CSE2deps.v
new file mode 100644
index 00000000..4592f408
--- /dev/null
+++ b/arm/CSE2deps.v
@@ -0,0 +1,35 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*                                                             *)
+(*  Copyright VERIMAG. All rights reserved.                    *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+     (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+  && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+  && ((ofsw + size_chunk chunkw <=? ofsr) ||
+      (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+  match addr, addr', args, args' with
+  | (Aindexed ofs), (Aindexed ofs'),
+    (base :: nil), (base' :: nil) =>
+    if peq base base'
+    then negb (can_swap_accesses_ofs (Int.unsigned ofs') chunk' (Int.unsigned ofs) chunk)
+    else true
+  | (Ainstack ofs), (Ainstack ofs'), _, _ =>
+    negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk)
+  | _, _, _, _ => true
+  end.
diff --git a/arm/CSE2depsproof.v b/arm/CSE2depsproof.v
new file mode 100644
index 00000000..7dd0914e
--- /dev/null
+++ b/arm/CSE2depsproof.v
@@ -0,0 +1,211 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*                                                             *)
+(*  Copyright VERIMAG. All rights reserved.                    *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps.
+
+Require Import Globalenvs Values.
+Require Import Linking Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import CSE2 CSE2deps.
+Require Import Lia.
+
+Lemma ptrofs_size :
+  Ptrofs.wordsize = 32%nat.
+Proof.
+  unfold Ptrofs.wordsize.
+  unfold Wordsize_Ptrofs.wordsize.
+  trivial.
+Qed.
+
+Lemma ptrofs_modulus :
+  Ptrofs.modulus = 4294967296.
+Proof.
+  unfold Ptrofs.modulus.
+  rewrite ptrofs_size.
+  destruct Archi.ptr64; reflexivity.
+Qed.
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+Section MEMORY_WRITE.
+  Variable m m2 : mem.
+  Variable chunkw chunkr : memory_chunk.
+  Variable base : val.
+  
+  Variable addrw addrr valw : val.
+  Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
+
+  Section INDEXED_AWAY.
+  Variable ofsw ofsr : int.
+  Hypothesis ADDRW : eval_addressing genv sp
+                       (Aindexed ofsw) (base :: nil) = Some addrw. 
+  Hypothesis ADDRR : eval_addressing genv sp
+                       (Aindexed ofsr) (base :: nil) = Some addrr.
+
+  Lemma load_store_away1 :
+    forall RANGEW : 0 <= Int.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk,
+    forall RANGER : 0 <= Int.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk,
+    forall SWAPPABLE :    Int.unsigned ofsw + size_chunk chunkw <= Int.unsigned ofsr
+                       \/ Int.unsigned ofsr + size_chunk chunkr <= Int.unsigned ofsw,
+    Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+  Proof.
+    intros.
+    
+    pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
+    pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
+    unfold largest_size_chunk in *.
+
+    rewrite ptrofs_modulus in *.
+    simpl in *.
+    inv ADDRR.
+    inv ADDRW.
+    destruct base; try discriminate.
+    eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+    exact STORE.
+    right.
+
+    all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsr)) as [OFSR | OFSR];
+              rewrite OFSR).
+    all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsw)) as [OFSW | OFSW];
+              rewrite OFSW).
+    
+    all: try rewrite ptrofs_modulus in *.
+
+    all: unfold Ptrofs.of_int.
+   
+    all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia).
+    all: intuition lia.
+  Qed.
+  
+  Theorem load_store_away :
+    can_swap_accesses_ofs (Int.unsigned ofsr) chunkr (Int.unsigned ofsw) chunkw = true ->
+    Mem.loadv chunkr m2 addrr =  Mem.loadv chunkr m addrr.
+  Proof.
+    intro SWAP.
+    unfold can_swap_accesses_ofs in SWAP.
+    repeat rewrite andb_true_iff in SWAP.
+    repeat rewrite orb_true_iff in SWAP.
+    repeat rewrite Z.leb_le in SWAP.
+    apply load_store_away1.
+    all: tauto.
+  Qed.
+  End INDEXED_AWAY.
+End MEMORY_WRITE.
+
+Section STACK_WRITE.
+  Variable m m2 : mem.
+  Variable chunkw chunkr : memory_chunk.
+  
+  Variable addrw addrr valw : val.
+  Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
+
+  Section INDEXED_AWAY.
+  Variable ofsw ofsr : ptrofs.
+  Hypothesis ADDRW : eval_addressing genv sp
+                       (Ainstack ofsw) nil = Some addrw.
+  Hypothesis ADDRR : eval_addressing genv sp
+                       (Ainstack ofsr) nil = Some addrr.
+
+  Lemma stack_load_store_away1 :
+    forall RANGEW : 0 <= Ptrofs.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk,
+    forall RANGER : 0 <= Ptrofs.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk,
+    forall SWAPPABLE :    Ptrofs.unsigned ofsw + size_chunk chunkw <= Ptrofs.unsigned ofsr
+                       \/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw,
+    Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+  Proof.
+    intros.
+    
+    pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
+    pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
+    unfold largest_size_chunk in *.
+
+    rewrite ptrofs_modulus in *.
+    simpl in *.
+    inv ADDRR.
+    inv ADDRW.
+
+    destruct sp; try discriminate.
+    eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+    exact STORE.
+    right.
+
+    all: try (destruct (Ptrofs.unsigned_add_either i ofsr) as [OFSR | OFSR];
+              rewrite OFSR).
+    all: try (destruct (Ptrofs.unsigned_add_either i ofsw) as [OFSW | OFSW];
+              rewrite OFSW).
+    
+    all: try rewrite ptrofs_modulus in *.
+
+    all: intuition lia.
+  Qed.
+  
+  Theorem stack_load_store_away :
+    can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true ->
+    Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+  Proof.
+    intro SWAP.
+    unfold can_swap_accesses_ofs in SWAP.
+    repeat rewrite andb_true_iff in SWAP.
+    repeat rewrite orb_true_iff in SWAP.
+    repeat rewrite Z.leb_le in SWAP.
+    apply stack_load_store_away1.
+    all: tauto.
+  Qed.
+  End INDEXED_AWAY.
+End STACK_WRITE.
+End SOUNDNESS.
+
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+Lemma may_overlap_sound:
+  forall m m' : mem,
+  forall chunk addr args chunk' addr' args' v a a' rs,
+    (eval_addressing genv sp addr (rs ## args)) = Some a ->
+    (eval_addressing genv sp addr' (rs ## args')) = Some a' ->
+    (may_overlap chunk addr args chunk' addr' args') = false ->
+    (Mem.storev chunk m a v) = Some m' ->
+    (Mem.loadv chunk' m'  a') = (Mem.loadv chunk' m a').
+Proof.
+  intros until rs.
+  intros ADDR ADDR' OVERLAP STORE.
+  destruct addr; destruct addr'; try discriminate.
+- (* Aindexed / Aindexed *)
+  destruct args as [ | base [ | ]]. 1,3: discriminate.
+  destruct args' as [ | base' [ | ]]. 1,3: discriminate.
+  simpl in OVERLAP.
+  destruct (peq base base'). 2: discriminate.
+  subst base'.
+  destruct (can_swap_accesses_ofs (Int.unsigned i0) chunk' (Int.unsigned i) chunk) eqn:SWAP.
+  2: discriminate.
+  simpl in *.
+  eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
+
+- (* Ainstack / Ainstack *)
+  destruct args. 2: discriminate.
+  destruct args'. 2: discriminate.
+  cbn in OVERLAP.
+  destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP.
+  2: discriminate.
+  cbn in *.
+  eapply stack_load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
+Qed.
+
+End SOUNDNESS.
diff --git a/arm/Constantexpand.ml b/arm/Constantexpand.ml
index 408b291e..8cc32c1f 100644
--- a/arm/Constantexpand.ml
+++ b/arm/Constantexpand.ml
@@ -106,6 +106,7 @@ let estimate_size = function
   | Pbuiltin (ef,_,_) ->
     begin match ef with
     | EF_inline_asm _ -> 256
+    | EF_profiling _ -> 40
     | _ -> 0 end
   | Pcfi_adjust _
   | Pcfi_rel_offset _
diff --git a/arm/DuplicateOpcodeHeuristic.ml b/arm/DuplicateOpcodeHeuristic.ml
new file mode 100644
index 00000000..41996028
--- /dev/null
+++ b/arm/DuplicateOpcodeHeuristic.ml
@@ -0,0 +1,36 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+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
+
diff --git a/arm/ExpansionOracle.ml b/arm/ExpansionOracle.ml
new file mode 120000
index 00000000..ee2674bf
--- /dev/null
+++ b/arm/ExpansionOracle.ml
@@ -0,0 +1 @@
+../aarch64/ExpansionOracle.ml
\ No newline at end of file
diff --git a/arm/Machregs.v b/arm/Machregs.v
index ae0ff6bf..1ec8f0a1 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -153,6 +153,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
   | EF_memcpy sz al => R2 :: R3 :: R12 :: F7 :: nil
   | EF_inline_asm txt sg clob => destroyed_by_clobber clob
+  | EF_profiling _ _ => R2 :: R3 :: R12 :: nil
   | _ => nil
   end.
 
diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml
index a4624a9d..24a33e9e 100644
--- a/arm/Machregsaux.ml
+++ b/arm/Machregsaux.ml
@@ -13,3 +13,8 @@
 (** Auxiliary functions on machine registers *)
 
 let is_scratch_register s =  s = "R14"  || s = "r14"
+                                              
+let class_of_type = function
+  | AST.Tint | AST.Tlong -> 0
+  | AST.Tfloat | AST.Tsingle -> 1
+  | AST.Tany32 | AST.Tany64 -> assert false
diff --git a/arm/Machregsaux.mli b/arm/Machregsaux.mli
index f3d52849..01b0f9fd 100644
--- a/arm/Machregsaux.mli
+++ b/arm/Machregsaux.mli
@@ -13,3 +13,5 @@
 (** Auxiliary functions on machine registers *)
 
 val is_scratch_register: string -> bool
+
+val class_of_type: AST.typ -> int
diff --git a/arm/Op.v b/arm/Op.v
index 4739ef2e..68f6662d 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -518,6 +518,37 @@ Proof with (try exact I; try reflexivity).
   unfold Val.select. destruct (eval_condition c vl m). apply Val.normalize_type. exact I.
 Qed.
 
+
+Definition is_trapping_op (op : operation) :=
+  match op with
+  | Odiv | Odivu
+  | Oshrximm _
+  | Ointoffloat | Ointuoffloat
+  | Ointofsingle | Ointuofsingle
+  | Ofloatofint | Ofloatofintu
+  | Osingleofint | Osingleofintu => true
+  | _ => false
+  end.
+                
+
+Definition args_of_operation op :=
+  if eq_operation op Omove
+  then 1%nat
+  else List.length (fst (type_of_operation op)).
+
+Lemma is_trapping_op_sound:
+  forall op vl sp m,
+    is_trapping_op op = false ->
+    (List.length vl) = args_of_operation op ->
+    eval_operation genv sp op vl m <> None.
+Proof.
+  unfold args_of_operation.
+  destruct op; destruct eq_operation; intros; simpl in *; try congruence.
+  all: try (destruct vl as [ | vh1 vl1]; try discriminate).
+  all: try (destruct vl1 as [ | vh2 vl2]; try discriminate).
+  all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).
+  all: try (destruct vl3 as [ | vh4 vl4]; try discriminate).
+Qed.
 End SOUNDNESS.
 
 (** * Manipulating and transforming operations *)
@@ -687,7 +718,7 @@ Definition is_trivial_op (op: operation) : bool :=
 
 (** Operations that depend on the memory state. *)
 
-Definition condition_depends_on_memory (c: condition) : bool :=
+Definition cond_depends_on_memory (c: condition) : bool :=
   match c with
   | Ccompu _ | Ccompushift _ _| Ccompuimm _ _ => true
   | _ => false
@@ -695,14 +726,14 @@ Definition condition_depends_on_memory (c: condition) : bool :=
 
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
-  | Ocmp c => condition_depends_on_memory c
-  | Osel c ty => condition_depends_on_memory c
+  | Ocmp c => cond_depends_on_memory c
+  | Osel c ty => cond_depends_on_memory c
   | _ => false
   end.
 
-Lemma condition_depends_on_memory_correct:
+Lemma cond_depends_on_memory_correct:
   forall c args m1 m2,
-  condition_depends_on_memory c = false ->
+  cond_depends_on_memory c = false ->
   eval_condition c args m1 = eval_condition c args m2.
 Proof.
   intros. destruct c; simpl; auto; discriminate.
@@ -714,12 +745,36 @@ Lemma op_depends_on_memory_correct:
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
   intros until m2. destruct op; simpl; try congruence; intros C.
-- f_equal; f_equal; apply condition_depends_on_memory_correct; auto.
+- f_equal; f_equal; apply cond_depends_on_memory_correct; auto.
 - destruct args; auto. destruct args; auto.
-  rewrite (condition_depends_on_memory_correct c args m1 m2 C).
+  rewrite (cond_depends_on_memory_correct c args m1 m2 C).
   auto.
 Qed.
 
+Lemma cond_valid_pointer_eq:
+  forall cond args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
+  all: repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+Qed.
+
+Lemma op_valid_pointer_eq:
+  forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
+Proof.
+  intros until m2. destruct op eqn:OP; simpl; try congruence.
+  - intros MEM; destruct c; simpl; try congruence;
+    repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+  - intro MEM; destruct c; simpl; try congruence;
+      repeat (destruct args; simpl; try congruence);
+      erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+Qed.
+
 (** Global variables mentioned in an operation or addressing mode *)
 
 Definition globals_operation (op: operation) : list ident :=
@@ -975,6 +1030,20 @@ Proof.
   apply Val.offset_ptr_inject; auto.
 Qed.
 
+Lemma eval_addressing_inj_none:
+  forall addr sp1 vl1 sp2 vl2,
+  (forall id ofs,
+      In id (globals_addressing addr) ->
+      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
+  Val.inject f sp1 sp2 ->
+  Val.inject_list f vl1 vl2 ->
+  eval_addressing ge1 sp1 addr vl1 = None ->
+  eval_addressing ge2 sp2 addr vl2 = None.
+Proof.
+  intros until vl2. intros Hglobal Hinjsp Hinjvl.
+  destruct addr; simpl in *;
+  inv Hinjvl; trivial; try discriminate; inv H0; trivial; try discriminate; inv H2; trivial; try discriminate.
+Qed.
 End EVAL_COMPAT.
 
 (** Compatibility of the evaluation functions with the ``is less defined'' relation over values. *)
@@ -1080,6 +1149,19 @@ Proof.
   destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto.
 Qed.
 
+Lemma eval_addressing_lessdef_none:
+  forall sp addr vl1 vl2,
+  Val.lessdef_list vl1 vl2 ->
+  eval_addressing genv sp addr vl1 = None ->
+  eval_addressing genv sp addr vl2 = None.
+Proof.
+  intros. rewrite val_inject_list_lessdef in H.
+  eapply eval_addressing_inj_none with (sp1 := sp).
+  intros. rewrite <- val_inject_lessdef; auto.
+  rewrite <- val_inject_lessdef; auto.
+  eauto. auto.
+Qed.
+
 End EVAL_LESSDEF.
 
 (** Compatibility of the evaluation functions with memory injections. *)
@@ -1132,6 +1214,19 @@ Proof.
   econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
+Lemma eval_addressing_inject_none:
+  forall addr vl1 vl2,
+  Val.inject_list f vl1 vl2 ->
+  eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = None ->
+  eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = None.
+Proof.
+  intros.
+  rewrite eval_shift_stack_addressing.
+  eapply eval_addressing_inj_none with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
+  intros. apply symbol_address_inject.
+  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
+Qed.
+
 Lemma eval_operation_inject:
   forall op vl1 vl2 v1 m1 m2,
   Val.inject_list f vl1 vl2 ->
diff --git a/arm/PrepassSchedulingOracle.ml b/arm/PrepassSchedulingOracle.ml
new file mode 120000
index 00000000..9885fd52
--- /dev/null
+++ b/arm/PrepassSchedulingOracle.ml
@@ -0,0 +1 @@
+../x86/PrepassSchedulingOracle.ml
\ No newline at end of file
diff --git a/arm/RTLpathSE_simplify.v b/arm/RTLpathSE_simplify.v
new file mode 120000
index 00000000..55bf0e52
--- /dev/null
+++ b/arm/RTLpathSE_simplify.v
@@ -0,0 +1 @@
+../aarch64/RTLpathSE_simplify.v
\ No newline at end of file
diff --git a/arm/SelectLong.vp b/arm/SelectLong.vp
index cc7a38f6..b4cdd0e3 100644
--- a/arm/SelectLong.vp
+++ b/arm/SelectLong.vp
@@ -16,6 +16,6 @@ Require Import Coqlib.
 Require Import Compopts.
 Require Import AST Integers Floats.
 Require Import Op CminorSel.
-Require Import SelectOp SplitLong.
+Require Import OpHelpers SelectOp SplitLong.
 
 (** This file is empty because we use the default implementation provided in [SplitLong]. *)
diff --git a/arm/SelectLongproof.v b/arm/SelectLongproof.v
index a82c082c..a65a38d4 100644
--- a/arm/SelectLongproof.v
+++ b/arm/SelectLongproof.v
@@ -16,6 +16,7 @@ Require Import String Coqlib Maps Integers Floats Errors.
 Require Archi.
 Require Import AST Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
+Require Import OpHelpers OpHelpersproof.
 Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
 Require Import SelectLong.
 
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 1220abc4..5506157c 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -39,7 +39,7 @@
 Require Import Coqlib.
 Require Import Compopts.
 Require Import AST Integers Floats Builtins.
-Require Import Op CminorSel.
+Require Import Op OpHelpers CminorSel.
 
 Local Open Scope cminorsel_scope.
 
@@ -516,6 +516,13 @@ Nondetfunction builtin_arg (e: expr) :=
   | _ => BA e
   end.
 
+(* floats *)
+Definition divf_base (e1: expr) (e2: expr) :=
+  Eop Odivf (e1 ::: e2 ::: Enil).
+
+Definition divfs_base (e1: expr) (e2: expr) :=
+  Eop Odivfs (e1 ::: e2 ::: Enil).
+
 (** Platform-specific known builtins *)
 
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index bd9f01b1..e4e606bc 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -17,6 +17,7 @@ Require Import AST Integers Floats.
 Require Import Values Memory Builtins Globalenvs.
 Require Import Cminor Op CminorSel.
 Require Import SelectOp.
+Require Import OpHelpers OpHelpersproof.
 
 Local Open Scope cminorsel_scope.
 Local Transparent Archi.ptr64.
@@ -69,8 +70,10 @@ Ltac TrivialExists :=
 (** * Correctness of the smart constructors *)
 
 Section CMCONSTR.
-
-Variable ge: genv.
+Variable prog: program.
+Variable hf: helper_functions.
+Hypothesis HELPERS: helper_functions_declared prog hf.
+Let ge := Genv.globalenv prog.
 Variable sp: val.
 Variable e: env.
 Variable m: mem.
@@ -902,6 +905,27 @@ Proof.
 - constructor; auto.
 Qed.
 
+(* floating-point division without HELPERS *)
+Theorem eval_divf_base:
+  forall le a b x y,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  exists v, eval_expr ge sp e m le (divf_base a b) v /\ Val.lessdef (Val.divf x y) v.
+Proof.
+  intros; unfold divf_base.
+  TrivialExists.
+Qed.
+
+Theorem eval_divfs_base:
+  forall le a b x y,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v.
+Proof.
+  intros; unfold divfs_base.
+  TrivialExists.
+Qed.
+
 (** Platform-specific known builtins *)
 
 Theorem eval_platform_builtin:
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 43dac44a..9269dd29 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -147,7 +147,9 @@ struct
 
   let name_of_section = function
     | Section_text -> ".text"
-    | Section_data i | Section_small_data i ->
+    | Section_data(i, true) ->
+         failwith "_Thread_local unsupported on this platform"
+    | Section_data(i, false) | Section_small_data(i) ->
         variable_section ~sec:".data" ~bss:".bss" i
     | Section_const i | Section_small_const i ->
         variable_section ~sec:".section	.rodata" i
@@ -202,6 +204,38 @@ struct
     | SOasr(r, n) -> fprintf oc "%a, asr #%a" ireg r coqint n
     | SOror(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n
 
+
+    let next_profiling_label =
+      let profiling_label_counter = ref 0 in
+      fun () ->
+      let r = sprintf ".Lprofiling_label%d" !profiling_label_counter in
+      incr profiling_label_counter; r;;
+                   
+    let print_profiling_logger oc id kind =
+      assert (kind >= 0);
+      assert (kind <= 1);
+      let ofs = profiling_offset id kind and olbl = next_profiling_label () in
+      fprintf oc "%s begin profiling %a %d: non-atomic increment\n" comment
+        Profilingaux.pp_id id kind;
+      fprintf oc "	ldr	r2, %s\n" olbl;
+      fprintf oc "	ldr	r3, [r2, #%d]\n"
+        (if Configuration.is_big_endian then 8 else 0);
+      fprintf oc "	ldr	r12, [r2, #%d]\n"
+        (if Configuration.is_big_endian then 0 else 8);
+      fprintf oc "	adds	r3, r3, #1\n";
+      fprintf oc "	adc	r12, r12, #0\n";
+      fprintf oc "	str	r3, [r2, #%d]\n"
+        (if Configuration.is_big_endian then 8 else 0);
+      fprintf oc "	str	r12, [r2, #%d]\n"
+        (if Configuration.is_big_endian then 0 else 8);
+      let jlbl = next_profiling_label () in
+      fprintf oc "	b	%s\n" jlbl;
+      fprintf oc "%s:\n" olbl;
+      fprintf oc "	.word	%s + %d\n" profiling_counter_table_name ofs;
+      fprintf oc "%s:\n" jlbl;
+      fprintf oc "%s end profiling %a %d\n" comment
+        Profilingaux.pp_id id kind;;
+
   let print_instruction oc = function
     (* Core instructions *)
     | Padc (r1,r2,so) ->
@@ -482,6 +516,7 @@ struct
           fprintf oc "%s begin inline assembly\n\t" comment;
           print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res;
           fprintf oc "%s end inline assembly\n" comment
+        | EF_profiling(id, coq_kind) -> print_profiling_logger oc id  (Z.to_int coq_kind)
         | _ ->
           assert false
       end
@@ -549,6 +584,11 @@ struct
     if !Clflags.option_mthumb then
       fprintf oc "	.thumb_func\n"
 
+
+  let text_print_fun_info oc name =
+    fprintf oc "	.type	%s, %%function\n" name;
+    fprintf oc "	.size	%s, . - %s\n" name name
+
   let print_fun_info oc name =
     fprintf oc "	.type	%a, %%function\n" symbol name;
     fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
@@ -596,9 +636,22 @@ struct
     if !Clflags.option_g then begin
       section oc Section_text;
       cfi_section oc
-    end
+      end
+
+  let arm_profiling_stub oc nr_items
+          profiling_id_table_name
+          profiling_counter_table_name =
+        fprintf oc "	ldr	r2, = %s\n" profiling_counter_table_name;
+        fprintf oc "	ldr	r1, = %s\n" profiling_id_table_name;
+	fprintf oc "	mov	r0, #%d\n" nr_items;
+	fprintf oc "	b	%s\n" profiling_write_table_helper;;
+  
+  let print_atexit oc to_be_called =
+      	fprintf oc "	ldr	r0, = %s\n" to_be_called;
+	fprintf oc "	b	atexit\n";;
 
   let print_epilogue oc =
+    print_profiling_epilogue text_print_fun_info (Init_atexit print_atexit) arm_profiling_stub oc;
     if !Clflags.option_g then begin
       Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f));
       section oc Section_text;