diff options
-rw-r--r-- | aarch64/Archi.v | 2 | ||||
-rw-r--r-- | arm/Archi.v | 2 | ||||
-rw-r--r-- | backend/LICMaux.ml | 14 | ||||
-rw-r--r-- | mppa_k1c/Archi.v | 6 | ||||
-rw-r--r-- | powerpc/Archi.v | 2 | ||||
-rw-r--r-- | riscV/Archi.v | 2 | ||||
-rw-r--r-- | test/monniaux/cse2/noloopinvariant.c | 6 | ||||
-rw-r--r-- | x86_32/Archi.v | 2 | ||||
-rw-r--r-- | x86_64/Archi.v | 2 |
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. |