diff options
| -rw-r--r-- | .gitignore | 3 | ||||
| -rw-r--r-- | backend/Duplicate.v | 2 | ||||
| -rw-r--r-- | backend/Duplicateproof.v | 2 | ||||
| -rw-r--r-- | backend/Lineartyping.v | 7 | ||||
| -rwxr-xr-x | configure | 6 | ||||
| -rw-r--r-- | cparser/Machine.ml | 5 | ||||
| -rw-r--r-- | cparser/Machine.mli | 1 | ||||
| -rw-r--r-- | driver/Frontend.ml | 1 | ||||
| -rw-r--r-- | mppa_k1c/Op.v | 6 | ||||
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 4 | ||||
| -rw-r--r-- | riscV/Asmgen.v | 2 | ||||
| -rw-r--r-- | test/c/Makefile | 4 | ||||
| -rw-r--r-- | test/regression/Makefile | 2 | ||||
| -rw-r--r-- | test/regression/extasm.c | 2 |
14 files changed, 26 insertions, 21 deletions
@@ -45,15 +45,12 @@ /riscV/ConstpropOp.v /riscV/SelectOp.v /riscV/SelectLong.v -<<<<<<< HEAD /mppa_k1c/ConstpropOp.v /mppa_k1c/SelectOp.v /mppa_k1c/SelectLong.v -======= /aarch64/ConstpropOp.v /aarch64/SelectOp.v /aarch64/SelectLong.v ->>>>>>> e1725209b2b4401adc63ce5238fa5db7c134609c /backend/SelectDiv.v /backend/SplitLong.v /cparser/Parser.v diff --git a/backend/Duplicate.v b/backend/Duplicate.v index d1458bd4..68a7f413 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -157,7 +157,7 @@ Definition verify_match_inst revmap inst tinst := | Icond cond' lr' n1' n2' => do u1 <- verify_is_copy revmap n1 n1'; do u2 <- verify_is_copy revmap n2 n2'; - if (condition_eq cond cond') then + if (eq_condition cond cond') then if (list_eq_dec Pos.eq_dec lr lr') then OK tt else Error (msg "Different lr in Icond") else Error (msg "Different cond in Icond") diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 54dd6196..d16505dd 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -132,7 +132,7 @@ Proof. - destruct i'; try (inversion H; fail). monadInv H. destruct x. eapply verify_is_copy_correct in EQ. destruct x0. eapply verify_is_copy_correct in EQ1. - destruct (condition_eq _ _); try discriminate. + destruct (eq_condition _ _); try discriminate. destruct (list_eq_dec _ _ _); try discriminate. subst. constructor; assumption. (* Ijumptable *) diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 0e3b7c8e..18594be8 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -321,11 +321,12 @@ Local Opaque mreg_type. + (* other ops *) destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans. econstructor; eauto. - apply wt_setreg. eapply Val.has_subtype; eauto. + + apply wt_setreg; auto; try (apply wt_undef_regs; auto). + eapply Val.has_subtype; eauto. change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto. red; intros; subst op. simpl in ISMOVE. - destruct args; try discriminate. destruct args; discriminate. - apply wt_undef_regs; auto. + destruct args; try discriminate. destruct args; discriminate. - (* load *) simpl in *; InvBooleans. econstructor; eauto. @@ -470,6 +470,10 @@ if test "$arch" = "mppa_k1c"; then system="linux" fi +<<<<<<< HEAD +======= +# +>>>>>>> mppa-work # AArch64 (ARMv8 64 bits) Target Configuration # if test "$arch" = "aarch64"; then @@ -910,6 +914,4 @@ cat <<EOF Coq development will not be installed EOF fi - fi - diff --git a/cparser/Machine.ml b/cparser/Machine.ml index 4999f0ac..193d83c4 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -272,6 +272,11 @@ let mppa_k1c = struct_passing_style = SP_value32_ref_callee; struct_return_style = SR_int1to4 } +let aarch64 = + { i32lpll64 with name = "aarch64"; + struct_passing_style = SP_ref_callee; (* Wrong *) + struct_return_style = SR_ref } (* Wrong *) + (* Add GCC extensions re: sizeof and alignof *) let gcc_extensions c = diff --git a/cparser/Machine.mli b/cparser/Machine.mli index 24d36e6c..ea25c4f6 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -88,6 +88,7 @@ val arm_bigendian : t val rv32 : t val rv64 : t val mppa_k1c : t +val aarch64 : t val gcc_extensions : t -> t val compcert_interpreter : t -> t diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 2584db90..b9db0d23 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -117,6 +117,7 @@ let init () = then Machine.rv64 else Machine.rv32 | "mppa_k1c" -> Machine.mppa_k1c + | "aarch64" -> Machine.aarch64 | _ -> assert false end; Env.set_builtins C2C.builtins; diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index ce9a5dcd..f9a774e8 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -51,12 +51,6 @@ Inductive condition : Type := | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) | Cnotcompfs (c: comparison). (**r negation of a floating-point comparison *) -Definition condition_eq: forall (x y: condition), {x = y} + {x <> y}. -Proof. - generalize comparison_eq int_eq int64_eq. - decide equality. -Defined. - Inductive condition0 : Type := | Ccomp0 (c: comparison) (**r signed integer comparison with 0 *) | Ccompu0 (c: comparison) (**r unsigned integer comparison with 0 *) diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index a360aa7c..38280810 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -1204,7 +1204,7 @@ Qed. Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). Proof. red; intros until x. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm. compute. discriminate. + rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. discriminate. Qed. Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16). @@ -1217,7 +1217,7 @@ Qed. Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16). Proof. red; intros until x. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm. compute. discriminate. + rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. discriminate. Qed. Theorem eval_intoffloat: diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index a704ed74..631693b9 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -25,6 +25,8 @@ Require Import Op Locations Mach Asm. Local Open Scope string_scope. Local Open Scope error_monad_scope. +Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. + (** The code generation functions take advantage of several characteristics of the [Mach] code generated by earlier passes of the compiler, mostly that argument and result registers are of the correct diff --git a/test/c/Makefile b/test/c/Makefile index 72814390..a2a80e06 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -8,7 +8,9 @@ EXECUTE:=timeout --signal=SIGTERM 20s $(EXECUTE) LIBS=$(LIBMATH) -TIME=ocaml unix.cma ../../tools/xtime.ml -o /dev/null -mintime 2.0 -minruns 4 +TIME=time >/dev/null +# FIXME - maybe this is better? From v3.6 +# TIME=ocaml unix.cma ../../tools/xtime.ml -o /dev/null -mintime 2.0 -minruns 4 PROGS?=fib integr qsort fft fftsp fftw sha1 sha3 aes almabench \ lists binarytrees fannkuch mandelbrot nbody \ diff --git a/test/regression/Makefile b/test/regression/Makefile index 585ffb1c..3447d6a5 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -10,7 +10,7 @@ LIBS=$(LIBMATH) # Can run, both in compiled mode and in interpreter mode, # and have reference output in Results -TESTS=int32 int64 floats floats-basics floats-lit \ +TESTS?=int32 int64 floats floats-basics floats-lit \ expr1 expr6 funptr2 initializers initializers2 initializers3 \ volatile1 volatile2 volatile3 volatile4 \ funct3 expr5 struct7 struct8 struct11 struct12 casts1 casts2 char1 \ diff --git a/test/regression/extasm.c b/test/regression/extasm.c index 8abeb98f..352b930b 100644 --- a/test/regression/extasm.c +++ b/test/regression/extasm.c @@ -24,7 +24,7 @@ int clobbers(int x, int z) || (defined(ARCH_riscV) && defined(MODEL_64)) \ || (defined(ARCH_powerpc) && defined(MODEL_ppc64)) \ || (defined(ARCH_powerpc) && defined(MODEL_e5500)) \ - || (defined(ARCH_mppa_k1c) && defined(MODEL_64)) + || (defined(ARCH_mppa_k1c) && defined(MODEL_64)) \ || defined(ARCH_aarch64) #define SIXTYFOUR #else |