diff options
| -rw-r--r-- | mppa_k1c/Asmgen.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/Asmgenproof1.v | 26 | ||||
| -rw-r--r-- | test/mppa/mmult/.gitignore | 3 | ||||
| -rw-r--r-- | test/mppa/mmult/Makefile | 74 | ||||
| -rw-r--r-- | test/mppa/mmult/mmult.c | 2 |
6 files changed, 59 insertions, 52 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index d17ba14b..675cb065 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -262,12 +262,12 @@ Definition transl_op OK (if Float32.eq_dec f Float32.zero then Pfcvtsw rd GPR0 :: k else Ploadsi rd f :: k) - | Oaddrsymbol s ofs, nil => +*)| Oaddrsymbol s ofs, nil => do rd <- ireg_of res; OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero) then Ploadsymbol rd s Ptrofs.zero :: addptrofs rd rd ofs k else Ploadsymbol rd s ofs :: k) -*)| Oaddrstack n, nil => + | Oaddrstack n, nil => do rd <- ireg_of res; OK (addptrofs rd SP n k) diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 4150cba8..2003239e 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -317,6 +317,8 @@ Opaque Int.eq. unfold transl_op; intros; destruct op; TailNoLabel. (* Omove *) - destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. +(* Oaddrsymbol *) +- destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)); TailNoLabel. (* Oaddimm32 *) - apply opimm32_label; intros; exact I. (* Oandimm32 *) diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v index 77643b8b..3085072e 100644 --- a/mppa_k1c/Asmgenproof1.v +++ b/mppa_k1c/Asmgenproof1.v @@ -1198,6 +1198,19 @@ Opaque Int.eq. unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl. - (* Omove *) destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl. +- (* Oaddrsymbol *) + destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)). ++ set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))). + exploit (addptrofs_correct x x ofs k rs1 m); eauto with asmgen. + intros (rs2 & A & B & C). + exists rs2; split. + apply exec_straight_step with rs1 m; auto. + split. replace ofs with (Ptrofs.add Ptrofs.zero ofs) by (apply Ptrofs.add_zero_l). + rewrite Genv.shift_symbol_address. + replace (rs1 x) with (Genv.symbol_address ge id Ptrofs.zero) in B by (unfold rs1; Simpl). + exact B. + intros. rewrite C by eauto with asmgen. unfold rs1; Simpl. ++ TranslOpSimpl. - (* Oaddrstack *) exploit addptrofs_correct. instantiate (1 := GPR12); auto with asmgen. intros (rs' & A & B & C). exists rs'; split; eauto. auto with asmgen. @@ -1229,19 +1242,6 @@ Opaque Int.eq. + econstructor; split. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. -- (* addrsymbol *) - destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)). -+ set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))). - exploit (addptrofs_correct x x ofs k rs1 m); eauto with asmgen. - intros (rs2 & A & B & C). - exists rs2; split. - apply exec_straight_step with rs1 m; auto. - split. replace ofs with (Ptrofs.add Ptrofs.zero ofs) by (apply Ptrofs.add_zero_l). - rewrite Genv.shift_symbol_address. - replace (rs1 x) with (Genv.symbol_address ge id Ptrofs.zero) in B by (unfold rs1; Simpl). - exact B. - intros. rewrite C by eauto with asmgen. unfold rs1; Simpl. -+ TranslOpSimpl. - (* stackoffset *) exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C). exists rs'; split; eauto. auto with asmgen. diff --git a/test/mppa/mmult/.gitignore b/test/mppa/mmult/.gitignore new file mode 100644 index 00000000..5883d367 --- /dev/null +++ b/test/mppa/mmult/.gitignore @@ -0,0 +1,3 @@ +mmult-test-k1c +mmult-test-x86 +test-ccomp diff --git a/test/mppa/mmult/Makefile b/test/mppa/mmult/Makefile index 9cb5b9e7..bb4506bf 100644 --- a/test/mppa/mmult/Makefile +++ b/test/mppa/mmult/Makefile @@ -10,47 +10,47 @@ all: $(ALL) %-test-k1c: %.c $(PRNG) k1-gcc -D__UNIT_TEST_$$(echo $(basename $<) | tr a-z A-Z)__ -O2 -std=c99 $^ -o $@ -#test-x86: selection.c merge.c insertion.c test.c $(PRNG) -# gcc -g -O2 -std=c99 $^ -o $@ -# -#test-k1c: selection.c merge.c insertion.c test.c $(PRNG) -# k1-gcc -g -O2 -std=c99 $^ -o $@ -# -#%.s: %.c -# ccomp -O2 -S $< -o $@ -# -#test-ccomp: selection.s merge.s insertion.s test.s $(subst .c,.s,$(PRNG)) -# k1-gcc $^ -o $@ +test-x86: mmult.c $(PRNG) + gcc -g -O2 -std=c99 $^ -o $@ + +test-k1c: mmult.c $(PRNG) + k1-gcc -g -O2 -std=c99 $^ -o $@ + +%.s: %.c + ccomp -O2 -S $< -o $@ + +test-ccomp: mmult.s $(subst .c,.s,$(PRNG)) + k1-gcc $^ -o $@ .PHONY: unittest: unittest-x86 unittest-k1c -#.PHONY: -#check: check-x86 check-k1c - -#.PHONY: -#compc-check: test-ccomp -# @if ! k1-cluster -- ./$<; then\ -# >&2 echo "ERROR k1c: sort $< failed";\ -# else\ -# echo "k1c: Test sort $< succeeded";\ -# fi -# -#.PHONY: -#check-x86: test-x86 -# @if ! ./$<; then\ -# >&2 echo "ERROR x86: $< failed";\ -# else\ -# echo "x86: Test $< succeeded";\ -# fi -# -#.PHONY: -#check-k1c: test-k1c -# @if ! k1-cluster -- ./$<; then\ -# >&2 echo "ERROR k1c: $< failed";\ -# else\ -# echo "k1c: Test $< succeeded";\ -# fi +.PHONY: +check: check-x86 check-k1c + +.PHONY: +compc-check: test-ccomp + @if ! k1-cluster -- ./$<; then\ + >&2 echo "ERROR k1c: sort $< failed";\ + else\ + echo "k1c: Test sort $< succeeded";\ + fi + +.PHONY: +check-x86: test-x86 + @if ! ./$<; then\ + >&2 echo "ERROR x86: $< failed";\ + else\ + echo "x86: Test $< succeeded";\ + fi + +.PHONY: +check-k1c: test-k1c + @if ! k1-cluster -- ./$<; then\ + >&2 echo "ERROR k1c: $< failed";\ + else\ + echo "k1c: Test $< succeeded";\ + fi .PHONY: unittest-x86: mmult-test-x86 diff --git a/test/mppa/mmult/mmult.c b/test/mppa/mmult/mmult.c index 04ac4605..16dcf34c 100644 --- a/test/mppa/mmult/mmult.c +++ b/test/mppa/mmult/mmult.c @@ -1,6 +1,8 @@ #include "../lib/types.h" #include "../lib/prng.h" +#define __UNIT_TEST_MMULT__ + #ifdef __UNIT_TEST_MMULT__ #define SIZE 50 #else |