test whether the instructions are allowed

9 files changed, 28 insertions, 10 deletions

diff --git a/aarch64/Archi.v b/aarch64/Archi.v
index aef4ab77..7d7b6887 100644
--- a/aarch64/Archi.v
+++ b/aarch64/Archi.v
@@ -86,3 +86,5 @@ Global Opaque ptr64 big_endian splitlong
 (** Whether to generate position-independent code or not *)
 
 Parameter pic_code: unit -> bool.
+
+Definition has_notrap_loads := false.
diff --git a/arm/Archi.v b/arm/Archi.v
index 16d6c71d..738341cc 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -97,3 +97,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/backend/LICMaux.ml b/backend/LICMaux.ml
index 314a5cf4..0368b94f 100644
--- a/backend/LICMaux.ml
+++ b/backend/LICMaux.ml
@@ -133,14 +133,15 @@ let rewrite_loop_body (last_alloc : reg ref)
         | Some ii ->
            let mapper' =
              match ii with
-             | Iop(op, args, res, pc') ->
+             | Iop(op, args, res, pc') when not (Op.is_trapping_op op) ->
                 let new_res = P.succ !last_alloc in
                 last_alloc := new_res;
                 add_inj (INJop(op,
                                (List.map (map_reg mapper) args),
                                new_res));
                 PTree.set res new_res mapper
-             | Iload(trap, chunk, addr, args, res, pc') ->
+             | Iload(trap, chunk, addr, args, res, pc')
+               when Archi.has_notrap_loads ->
                 let new_res = P.succ !last_alloc in
                 last_alloc := new_res;
                 add_inj (INJload(chunk, addr,
@@ -245,9 +246,6 @@ let print_loop_headers f =
 
 let gen_injections (f : coq_function) (coq_max_pc : node) (coq_max_reg : reg):
       (Inject.inj_instr list) PTree.t =
-  let _ = pp_injections stdout (compute_injections f) in
-  PTree.empty;;
-(*
-  let max_reg = P.to_int coq_max_reg in
-  PTree.set coq_max_pc [Inject.INJload(AST.Mint32, (Op.Aindexed (Ptrofs.of_int (Z.of_sint 0))), [P.of_int 1], P.of_int (max_reg+1))] PTree.empty;;
- *)
+  let injections = compute_injections f in
+  let () = pp_injections stdout injections in
+  injections;;
diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v
index 69b32c7c..587f768e 100644
--- a/mppa_k1c/Archi.v
+++ b/mppa_k1c/Archi.v
@@ -26,11 +26,11 @@ Definition big_endian := false.
 Definition align_int64 := 8%Z.
 Definition align_float64 := 8%Z.
 
-Definition splitlong := negb ptr64.
+Definition splitlong := false.
 
 Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.
 Proof.
-  unfold splitlong. destruct ptr64; simpl; congruence. 
+  unfold splitlong. congruence. 
 Qed.
 
 (** THIS IS NOT CHECKED ! NONE OF THIS ! *)
@@ -77,3 +77,5 @@ Global Opaque ptr64 big_endian splitlong
 (** Whether to generate position-independent code or not *)
 
 Parameter pic_code: unit -> bool.
+
+Definition has_notrap_loads := true.
diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index 10f38391..8f96dafc 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -71,3 +71,5 @@ Global Opaque ptr64 big_endian splitlong
               default_nan_32 choose_nan_32
               fma_order fma_invalid_mul_is_nan
               float_of_single_preserves_sNaN.
+
+Definition has_notrap_loads := false.
diff --git a/riscV/Archi.v b/riscV/Archi.v
index 61d129d0..9bdaad99 100644
--- a/riscV/Archi.v
+++ b/riscV/Archi.v
@@ -72,3 +72,5 @@ Global Opaque ptr64 big_endian splitlong
 (** Whether to generate position-independent code or not *)
 
 Parameter pic_code: unit -> bool.
+
+Definition has_notrap_loads := false.
diff --git a/test/monniaux/cse2/noloopinvariant.c b/test/monniaux/cse2/noloopinvariant.c
new file mode 100644
index 00000000..5c7789bf
--- /dev/null
+++ b/test/monniaux/cse2/noloopinvariant.c
@@ -0,0 +1,6 @@
+int toto(int *t, int n) {
+  for(int i=1; i<n; i++) {
+    if (t[i] > t[0]) return i;
+  }
+  return 0;
+}
diff --git a/x86_32/Archi.v b/x86_32/Archi.v
index e9d05c14..4681784d 100644
--- a/x86_32/Archi.v
+++ b/x86_32/Archi.v
@@ -64,3 +64,5 @@ Global Opaque ptr64 big_endian splitlong
               default_nan_32 choose_nan_32
               fma_order fma_invalid_mul_is_nan
               float_of_single_preserves_sNaN.
+
+Definition has_notrap_loads := false.
diff --git a/x86_64/Archi.v b/x86_64/Archi.v
index 959d8dc1..0e3c55f8 100644
--- a/x86_64/Archi.v
+++ b/x86_64/Archi.v
@@ -64,3 +64,5 @@ Global Opaque ptr64 big_endian splitlong
               default_nan_32 choose_nan_32
               fma_order fma_invalid_mul_is_nan
               float_of_single_preserves_sNaN.
+
+Definition has_notrap_loads := false.