aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-31 19:09:30 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-31 19:09:30 +0200
commit6ec981b26bd3f3d6c379ec48fd6ac6931a86bff5 (patch)
treecee523d3139c4b94a273a61b9bfbb5bfcb660c6d
parent731c230f1c583b9e20e86e2b7fc43a1f6c8520ea (diff)
parentaa4dcf296521ebe5be4aee5ee29aa678b8325c46 (diff)
downloadcompcert-kvx-6ec981b26bd3f3d6c379ec48fd6ac6931a86bff5.tar.gz
compcert-kvx-6ec981b26bd3f3d6c379ec48fd6ac6931a86bff5.zip
Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2
-rw-r--r--.gitlab-ci.yml221
-rw-r--r--aarch64/Asmgen.v9
-rw-r--r--aarch64/Asmgenproof.v141
-rw-r--r--aarch64/Asmgenproof1.v656
-rw-r--r--aarch64/DuplicateOpcodeHeuristic.ml30
-rw-r--r--arm/DuplicateOpcodeHeuristic.ml25
-rw-r--r--backend/Duplicateaux.ml18
-rw-r--r--backend/Inliningaux.ml9
-rwxr-xr-xconfig_arm.sh2
-rwxr-xr-xconfig_armhf.sh1
-rwxr-xr-xconfig_ppc64.sh1
-rwxr-xr-xconfig_rv32.sh2
-rwxr-xr-xconfig_rv64.sh2
-rwxr-xr-xconfig_simple.sh7
-rw-r--r--cparser/Elab.ml4
-rw-r--r--driver/Clflags.ml3
-rw-r--r--driver/Driver.ml8
-rw-r--r--mppa_k1c/Asmblockgenproof1.v125
-rw-r--r--powerpc/DuplicateOpcodeHeuristic.ml30
-rw-r--r--riscV/Conventions1.v17
-rw-r--r--riscV/DuplicateOpcodeHeuristic.ml30
-rw-r--r--runtime/include/math.h7
-rw-r--r--test/Makefile4
-rw-r--r--test/c/mandelbrot.c2
-rw-r--r--test/monniaux/yarpgen/Makefile130
-rw-r--r--test/monniaux/yarpgen/Makefile.old52
-rw-r--r--test/regression/Makefile8
-rw-r--r--x86/DuplicateOpcodeHeuristic.ml30
28 files changed, 1194 insertions, 380 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
new file mode 100644
index 00000000..79a32b25
--- /dev/null
+++ b/.gitlab-ci.yml
@@ -0,0 +1,221 @@
+stages:
+ - build
+
+build_x86_64:
+ stage: build
+ image: "coqorg/coq"
+ before_script:
+ - opam switch 4.07.1+flambda
+ - eval `opam config env`
+ - opam install -y menhir
+ script:
+ - ./config_x86_64.sh
+ - make -j "$NJOBS"
+ - make -C test all test
+ - ulimit -s65536 && make -C test/monniaux/yarpgen
+ rules:
+ - if: '$CI_COMMIT_BRANCH == "mppa-work"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "master"'
+ when: always
+ - when: manual
+
+build_ia32:
+ stage: build
+ image: "coqorg/coq"
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-multilib
+ - opam switch 4.07.1+flambda
+ - eval `opam config env`
+ - opam install -y menhir
+ script:
+ - ./config_ia32.sh
+ - make -j "$NJOBS"
+ - make -C test all test
+ - ulimit -s65536 && make -C test/monniaux/yarpgen BITS=32 TARGET_CC='gcc -m32'
+ rules:
+ - if: '$CI_COMMIT_BRANCH == "mppa-work"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "master"'
+ when: always
+ - when: manual
+
+build_aarch64:
+ stage: build
+ image: "coqorg/coq"
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-aarch64-linux-gnu qemu-user
+ - opam switch 4.07.1+flambda
+ - eval `opam config env`
+ - opam install -y menhir
+ script:
+ - ./config_aarch64.sh
+ - make -j "$NJOBS"
+ - make -C test CCOMPOPTS='-static' SIMU='qemu-aarch64' EXECUTE='qemu-aarch64' all test
+ - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='aarch64-linux-gnu-gcc' EXECUTE='qemu-aarch64' CCOMPOPTS='-static' TARGET_CFLAGS='-static'
+ rules:
+ - if: '$CI_COMMIT_BRANCH == "mppa-work"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "master"'
+ when: always
+ - when: manual
+
+build_arm:
+ stage: build
+ image: "coqorg/coq"
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-arm-linux-gnueabi qemu-user
+ - opam switch 4.07.1+flambda
+ - eval `opam config env`
+ - opam install -y menhir
+ script:
+ - ./config_arm.sh
+ - make -j "$NJOBS"
+ - make -C test CCOMPOPTS=-static SIMU='qemu-arm' EXECUTE='qemu-arm' all test
+ - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='arm-linux-gnueabi-gcc' EXECUTE='qemu-arm' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32
+ rules:
+ - if: '$CI_COMMIT_BRANCH == "mppa-work"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "master"'
+ when: always
+ - when: manual
+
+
+build_armhf:
+ stage: build
+ image: "coqorg/coq"
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-arm-linux-gnueabihf qemu-user
+ - opam switch 4.07.1+flambda
+ - eval `opam config env`
+ - opam install -y menhir
+ script:
+ - ./config_armhf.sh
+ - make -j "$NJOBS"
+ - make -C test CCOMPOPTS=-static SIMU='qemu-arm' EXECUTE='qemu-arm' all test
+ - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='arm-linux-gnueabihf-gcc' EXECUTE='qemu-arm' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32
+ rules:
+ - if: '$CI_COMMIT_BRANCH == "mppa-work"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "master"'
+ when: always
+ - when: manual
+
+build_ppc:
+ stage: build
+ image: "coqorg/coq"
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-powerpc-linux-gnu qemu-user
+ - opam switch 4.07.1+flambda
+ - eval `opam config env`
+ - opam install -y menhir
+ script:
+ - ./config_ppc.sh
+ - make -j "$NJOBS"
+ rules:
+ - if: '$CI_COMMIT_BRANCH == "mppa-work"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "master"'
+ when: always
+ - when: manual
+
+build_ppc64:
+ stage: build
+ image: "coqorg/coq"
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-powerpc64-linux-gnu
+ - opam switch 4.07.1+flambda
+ - eval `opam config env`
+ - opam install -y menhir
+ script:
+ - ./config_ppc64.sh
+ - make -j "$NJOBS"
+ rules:
+ - if: '$CI_COMMIT_BRANCH == "mppa-work"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "master"'
+ when: always
+ - when: manual
+
+build_rv64:
+ stage: build
+ image: "coqorg/coq"
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-riscv64-linux-gnu qemu-user
+ - opam switch 4.07.1+flambda
+ - eval `opam config env`
+ - opam install -y menhir
+ script:
+ - ./config_rv64.sh
+ - make -j "$NJOBS"
+ - make -C test CCOMPOPTS=-static SIMU='qemu-riscv64' EXECUTE='qemu-riscv64' all test
+ - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='riscv64-linux-gnu-gcc' EXECUTE='qemu-riscv64' CCOMPOPTS='-static' TARGET_CFLAGS='-static'
+ rules:
+ - if: '$CI_COMMIT_BRANCH == "mppa-work"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "master"'
+ when: always
+ - when: manual
+
+build_rv32:
+ stage: build
+ image: "coqorg/coq"
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-riscv64-linux-gnu qemu-user
+ - opam switch 4.07.1+flambda
+ - eval `opam config env`
+ - opam install -y menhir
+ script:
+ - ./config_rv32.sh -no-runtime-lib
+ - make -j "$NJOBS"
+ rules:
+ - if: '$CI_COMMIT_BRANCH == "mppa-work"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "master"'
+ when: always
+ - when: manual
+
+build_k1c:
+ stage: build
+ image: "coqorg/coq"
+ before_script:
+ - opam switch 4.07.1+flambda
+ - eval `opam config env`
+ - opam install -y menhir
+ script:
+ - ./config_k1c.sh -no-runtime-lib
+ - make -j "$NJOBS"
+ rules:
+ - if: '$CI_COMMIT_BRANCH == "mppa-work"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "master"'
+ when: always
+ - when: manual
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index 46dd875d..024c9a17 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -1061,8 +1061,13 @@ Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: code) :=
(** Function epilogue *)
Definition make_epilogue (f: Mach.function) (k: code) :=
- loadptr XSP f.(fn_retaddr_ofs) RA
- (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k).
+ (* FIXME
+ Cannot be used because memcpy destroys X30;
+ issue being discussed with X. Leroy *)
+ (* if is_leaf_function f
+ then Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k
+ else*) loadptr XSP f.(fn_retaddr_ofs) RA
+ (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k).
(** Translation of a Mach instruction. *)
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 88258cd6..6831509f 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -337,7 +337,12 @@ Qed.
Remark make_epilogue_label:
forall f k, tail_nolabel k (make_epilogue f k).
Proof.
- unfold make_epilogue; intros. eapply tail_nolabel_trans. apply loadptr_label. TailNoLabel.
+ unfold make_epilogue; intros.
+ (* FIXME destruct is_leaf_function.
+ { TailNoLabel. } *)
+ eapply tail_nolabel_trans.
+ apply loadptr_label.
+ TailNoLabel.
Qed.
Lemma transl_instr_label:
@@ -472,7 +477,8 @@ Inductive match_states: Mach.state -> Asm.state -> Prop :=
(MEXT: Mem.extends m m')
(AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc)
(AG: agree ms sp rs)
- (DXP: ep = true -> rs#X29 = parent_sp s),
+ (DXP: ep = true -> rs#X29 = parent_sp s)
+ (LEAF: is_leaf_function f = true -> rs#RA = parent_ra s),
match_states (Mach.State s fb sp c ms m)
(Asm.State rs m')
| match_states_call:
@@ -503,16 +509,17 @@ Lemma exec_straight_steps:
exists rs2,
exec_straight tge tf c rs1 m1' k rs2 m2'
/\ agree ms2 sp rs2
- /\ (it1_is_parent ep i = true -> rs2#X29 = parent_sp s)) ->
+ /\ (it1_is_parent ep i = true -> rs2#X29 = parent_sp s)
+ /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
exists st',
plus step tge (State rs1 m1') E0 st' /\
match_states (Mach.State s fb sp c ms2 m2) st'.
Proof.
intros. inversion H2. subst. monadInv H7.
- exploit H3; eauto. intros [rs2 [A [B C]]].
+ exploit H3; eauto. intros [rs2 [A [B [C D]]]].
exists (State rs2 m2'); split.
- eapply exec_straight_exec; eauto.
- econstructor; eauto. eapply exec_straight_at; eauto.
+ - eapply exec_straight_exec; eauto.
+ - econstructor; eauto. eapply exec_straight_at; eauto.
Qed.
Lemma exec_straight_steps_goto:
@@ -527,13 +534,14 @@ Lemma exec_straight_steps_goto:
exists jmp, exists k', exists rs2,
exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2'
/\ agree ms2 sp rs2
- /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') ->
+ /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2'
+ /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
exists st',
plus step tge (State rs1 m1') E0 st' /\
match_states (Mach.State s fb sp c' ms2 m2) st'.
Proof.
intros. inversion H3. subst. monadInv H9.
- exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]].
+ exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]].
generalize (functions_transl _ _ _ H7 H8); intro FN.
generalize (transf_function_no_overflow _ _ H8); intro NOOV.
exploit exec_straight_steps_2; eauto.
@@ -550,6 +558,7 @@ Proof.
econstructor; eauto.
apply agree_exten with rs2; auto with asmgen.
congruence.
+ rewrite OTH by congruence; auto.
Qed.
Lemma exec_straight_opt_steps_goto:
@@ -564,13 +573,14 @@ Lemma exec_straight_opt_steps_goto:
exists jmp, exists k', exists rs2,
exec_straight_opt tge tf c rs1 m1' (jmp :: k') rs2 m2'
/\ agree ms2 sp rs2
- /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') ->
+ /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2'
+ /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
exists st',
plus step tge (State rs1 m1') E0 st' /\
match_states (Mach.State s fb sp c' ms2 m2) st'.
Proof.
intros. inversion H3. subst. monadInv H9.
- exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]].
+ exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]].
generalize (functions_transl _ _ _ H7 H8); intro FN.
generalize (transf_function_no_overflow _ _ H8); intro NOOV.
inv A.
@@ -583,6 +593,7 @@ Proof.
econstructor; eauto.
apply agree_exten with rs2; auto with asmgen.
congruence.
+ rewrite OTH by congruence; auto.
- exploit exec_straight_steps_2; eauto.
intros [ofs' [PC2 CT2]].
exploit find_label_goto_label; eauto.
@@ -597,6 +608,7 @@ Proof.
econstructor; eauto.
apply agree_exten with rs2; auto with asmgen.
congruence.
+ rewrite OTH by congruence; auto.
Qed.
(** We need to show that, in the simulation diagram, we cannot
@@ -629,7 +641,7 @@ Qed.
Theorem step_simulation:
forall S1 t S2, Mach.step return_address_offset ge S1 t S2 ->
- forall S1' (MS: match_states S1 S1'),
+ forall S1' (MS: match_states S1 S1') (WF: wf_state ge S1),
(exists S2', plus step tge S1' t S2' /\ match_states S2 S2')
\/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
Proof.
@@ -638,17 +650,20 @@ Proof.
- (* Mlabel *)
left; eapply exec_straight_steps; eauto; intros.
monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split. apply agree_nextinstr; auto. simpl; congruence.
+ split. { apply agree_nextinstr; auto. }
+ split. { simpl; congruence. }
+ rewrite nextinstr_inv by congruence; assumption.
- (* Mgetstack *)
unfold load_stack in H.
exploit Mem.loadv_extends; eauto. intros [v' [A B]].
rewrite (sp_val _ _ _ AG) in A.
left; eapply exec_straight_steps; eauto. intros. simpl in TR.
- exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q R]]].
+ exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q [R S]]]].
exists rs'; split. eauto.
- split. eapply agree_set_mreg; eauto with asmgen. congruence.
- simpl; congruence.
+ split. { eapply agree_set_mreg; eauto with asmgen. congruence. }
+ split. { simpl; congruence. }
+ rewrite S. assumption.
- (* Msetstack *)
unfold store_stack in H.
@@ -656,10 +671,12 @@ Proof.
exploit Mem.storev_extends; eauto. intros [m2' [A B]].
left; eapply exec_straight_steps; eauto.
rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
- exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]].
+ exploit storeind_correct; eauto with asmgen. intros [rs' [P [Q R]]].
exists rs'; split. eauto.
split. eapply agree_undef_regs; eauto with asmgen.
- simpl; intros. rewrite Q; auto with asmgen.
+ simpl; intros.
+ split. rewrite Q; auto with asmgen.
+ rewrite R. assumption.
- (* Mgetparam *)
assert (f0 = f) by congruence; subst f0.
@@ -675,39 +692,45 @@ Opaque loadind.
(* X30 contains parent *)
exploit loadind_correct. eexact EQ.
instantiate (2 := rs0). simpl; rewrite DXP; eauto. simpl; congruence.
- intros [rs1 [P [Q R]]].
+ intros [rs1 [P [Q [R S]]]].
exists rs1; split. eauto.
split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
- simpl; intros. rewrite R; auto with asmgen.
- apply preg_of_not_X29; auto.
+ simpl; split; intros.
+ { rewrite R; auto with asmgen.
+ apply preg_of_not_X29; auto.
+ }
+ { rewrite S; auto. }
+
(* X30 does not contain parent *)
exploit loadptr_correct. eexact A. simpl; congruence. intros [rs1 [P [Q R]]].
exploit loadind_correct. eexact EQ. instantiate (2 := rs1). simpl; rewrite Q. eauto. simpl; congruence.
- intros [rs2 [S [T U]]].
+ intros [rs2 [S [T [U V]]]].
exists rs2; split. eapply exec_straight_trans; eauto.
split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto.
instantiate (1 := rs1#X29 <- (rs2#X29)). intros.
rewrite Pregmap.gso; auto with asmgen.
congruence.
intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen.
- simpl; intros. rewrite U; auto with asmgen.
+ split; simpl; intros. rewrite U; auto with asmgen.
apply preg_of_not_X29; auto.
-
+ rewrite V. rewrite R by congruence. auto.
+
- (* Mop *)
assert (eval_operation tge sp op (map rs args) m = Some v).
{ rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. }
exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0.
intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A.
left; eapply exec_straight_steps; eauto; intros. simpl in TR.
- exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]].
+ exploit transl_op_correct; eauto. intros [rs2 [P [Q [R S]]]].
exists rs2; split. eauto. split.
apply agree_set_undef_mreg with rs0; auto.
apply Val.lessdef_trans with v'; auto.
- simpl; intros. InvBooleans.
+ split; simpl; intros. InvBooleans.
rewrite R; auto. apply preg_of_not_X29; auto.
Local Transparent destroyed_by_op.
destruct op; try exact I; simpl; congruence.
-
+ rewrite S.
+ auto.
- (* Mload *)
destruct trap.
{
@@ -717,10 +740,11 @@ Local Transparent destroyed_by_op.
intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
exploit Mem.loadv_extends; eauto. intros [v' [C D]].
left; eapply exec_straight_steps; eauto; intros. simpl in TR.
- exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]].
+ exploit transl_load_correct; eauto. intros [rs2 [P [Q [R S]]]].
exists rs2; split. eauto.
split. eapply agree_set_undef_mreg; eauto. congruence.
- simpl; congruence.
+ split. simpl; congruence.
+ rewrite S. assumption.
}
(* Mload notrap1 *)
@@ -740,10 +764,11 @@ Local Transparent destroyed_by_op.
assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto).
exploit Mem.storev_extends; eauto. intros [m2' [C D]].
left; eapply exec_straight_steps; eauto.
- intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]].
+ intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P [Q R]]].
exists rs2; split. eauto.
split. eapply agree_undef_regs; eauto with asmgen.
- simpl; congruence.
+ split. simpl; congruence.
+ rewrite R. assumption.
- (* Mcall *)
assert (f0 = f) by congruence. subst f0.
@@ -852,6 +877,18 @@ Local Transparent destroyed_by_op.
eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
congruence.
+ Simpl.
+ rewrite set_res_other by trivial.
+ rewrite undef_regs_other.
+ assumption.
+ intro.
+ rewrite in_map_iff.
+ intros (x0 & PREG & IN).
+ subst r'.
+ intro.
+ apply (preg_of_not_RA x0).
+ congruence.
+
- (* Mgoto *)
assert (f0 = f) by congruence. subst f0.
inv AT. monadInv H4.
@@ -865,25 +902,33 @@ Local Transparent destroyed_by_op.
eapply agree_exten; eauto with asmgen.
congruence.
+ rewrite INV by congruence.
+ assumption.
+
- (* Mcond true *)
assert (f0 = f) by congruence. subst f0.
exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
left; eapply exec_straight_opt_steps_goto; eauto.
intros. simpl in TR.
- exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C).
+ exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D).
exists jmp; exists k; exists rs'.
split. eexact A.
split. apply agree_exten with rs0; auto with asmgen.
- exact B.
+ split.
+ exact B.
+ rewrite D. exact LEAF.
- (* Mcond false *)
exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
left; eapply exec_straight_steps; eauto. intros. simpl in TR.
- exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C).
+ exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D).
econstructor; split.
eapply exec_straight_opt_right. eexact A. apply exec_straight_one. eexact B. auto.
split. apply agree_exten with rs0; auto. intros. Simpl.
+ split.
simpl; congruence.
+ Simpl. rewrite D.
+ exact LEAF.
- (* Mjumptable *)
assert (f0 = f) by congruence. subst f0.
@@ -905,6 +950,10 @@ Local Transparent destroyed_by_op.
simpl. intros. rewrite C; auto with asmgen. Simpl.
congruence.
+ rewrite C by congruence.
+ repeat rewrite Pregmap.gso by congruence.
+ assumption.
+
- (* Mreturn *)
assert (f0 = f) by congruence. subst f0.
inversion AT; subst. simpl in H6; monadInv H6.
@@ -947,7 +996,7 @@ Local Transparent destroyed_by_op.
simpl preg_of_iregsp. change (rs2 X30) with (rs0 X30). rewrite ATLR.
change (rs2 X2) with sp. eexact P.
simpl; congruence. congruence.
- intros (rs3 & U & V).
+ intros (rs3 & U & V & W).
assert (EXEC_PROLOGUE:
exec_straight tge tf
tf.(fn_code) rs0 m'
@@ -974,6 +1023,10 @@ Local Transparent destroyed_at_function_entry. simpl.
unfold sp; congruence.
intros. rewrite V by auto with asmgen. reflexivity.
+ rewrite W.
+ unfold rs2.
+ Simpl.
+
- (* external function *)
exploit functions_translated; eauto.
intros [tf [A B]]. simpl in B. inv B.
@@ -993,6 +1046,10 @@ Local Transparent destroyed_at_function_entry. simpl.
right. split. omega. split. auto.
rewrite <- ATPC in H5.
econstructor; eauto. congruence.
+ inv WF.
+ inv STACK.
+ inv H1.
+ congruence.
Qed.
Lemma transf_initial_states:
@@ -1028,11 +1085,17 @@ Qed.
Theorem transf_program_correct:
forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
Proof.
- eapply forward_simulation_star with (measure := measure).
- apply senv_preserved.
- eexact transf_initial_states.
- eexact transf_final_states.
- exact step_simulation.
+ eapply forward_simulation_star with (measure := measure)
+ (match_states := fun S1 S2 => match_states S1 S2 /\ wf_state ge S1).
+ - apply senv_preserved.
+ - simpl; intros. exploit transf_initial_states; eauto.
+ intros (s2 & A & B).
+ exists s2; intuition auto. apply wf_initial; auto.
+ - simpl; intros. destruct H as [MS WF]. eapply transf_final_states; eauto.
+ - simpl; intros. destruct H0 as [MS WF].
+ exploit step_simulation; eauto. intros [ (s2' & A & B) | (A & B & C) ].
+ + left; exists s2'; intuition auto. eapply wf_step; eauto.
+ + right; intuition auto. eapply wf_step; eauto.
Qed.
End PRESERVATION.
diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v
index 6f296f56..0e36bd05 100644
--- a/aarch64/Asmgenproof1.v
+++ b/aarch64/Asmgenproof1.v
@@ -22,6 +22,51 @@ Local Transparent Archi.ptr64.
(** Properties of registers *)
+Lemma preg_of_not_RA:
+ forall r, (preg_of r) <> RA.
+Proof.
+ destruct r; discriminate.
+Qed.
+
+Lemma RA_not_written:
+ forall (rs : regset) dst v,
+ rs # (preg_of dst) <- v RA = rs RA.
+Proof.
+ intros.
+ apply Pregmap.gso.
+ intro.
+ symmetry in H.
+ exact (preg_of_not_RA dst H).
+Qed.
+
+Hint Resolve RA_not_written : asmgen.
+
+Lemma RA_not_written2:
+ forall (rs : regset) dst v i,
+ preg_of dst = i ->
+ rs # i <- v RA = rs RA.
+Proof.
+ intros.
+ subst i.
+ apply RA_not_written.
+Qed.
+
+Hint Resolve RA_not_written2 : asmgen.
+
+Lemma RA_not_written3:
+ forall (rs : regset) dst v i,
+ ireg_of dst = OK i ->
+ rs # i <- v RA = rs RA.
+Proof.
+ intros.
+ unfold ireg_of in H.
+ destruct preg_of eqn:PREG; try discriminate.
+ replace i0 with i in * by congruence.
+ eapply RA_not_written2; eassumption.
+Qed.
+
+Hint Resolve RA_not_written3 : asmgen.
+
Lemma preg_of_iregsp_not_PC: forall r, preg_of_iregsp r <> PC.
Proof.
destruct r; simpl; congruence.
@@ -39,6 +84,26 @@ Proof.
red; intros; subst x. elim (preg_of_not_X16 r); auto.
Qed.
+Lemma ireg_of_not_RA: forall r x, ireg_of r = OK x -> x <> RA.
+Proof.
+ unfold ireg_of; intros. destruct (preg_of r) eqn:E; inv H.
+ red; intros; subst x. elim (preg_of_not_RA r); auto.
+Qed.
+
+Lemma ireg_of_not_RA': forall r x, ireg_of r = OK x -> RA <> x.
+Proof.
+ intros. intro.
+ apply (ireg_of_not_RA r x); auto.
+Qed.
+
+Lemma ireg_of_not_RA'': forall r x, ireg_of r = OK x -> IR RA <> IR x.
+Proof.
+ intros. intro.
+ apply (ireg_of_not_RA' r x); auto. congruence.
+Qed.
+
+Hint Resolve ireg_of_not_RA ireg_of_not_RA' ireg_of_not_RA'' : asmgen.
+
Lemma ireg_of_not_X16': forall r x, ireg_of r = OK x -> IR x <> IR X16.
Proof.
intros. apply ireg_of_not_X16 in H. congruence.
@@ -205,42 +270,49 @@ Qed.
Lemma exec_loadimm_k_w:
forall (rd: ireg) k m l,
wf_decomposition l ->
+ rd <> RA ->
forall (rs: regset) accu,
rs#rd = Vint (Int.repr accu) ->
exists rs',
exec_straight_opt ge fn (loadimm_k W rd l k) rs m k rs' m
/\ rs'#rd = Vint (Int.repr (recompose_int accu l))
- /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+ /\ (forall r, r <> PC -> r <> rd -> rs'#r = rs#r)
+ /\ rs' # RA = rs # RA.
Proof.
- induction 1; intros rs accu ACCU; simpl.
+ induction 1; intros RD_NOT_RA rs accu ACCU; simpl.
- exists rs; split. apply exec_straight_opt_refl. auto.
-- destruct (IHwf_decomposition
+- destruct (IHwf_decomposition RD_NOT_RA
(nextinstr (rs#rd <- (insert_in_int rs#rd n p 16)))
(Zinsert accu n p 16))
- as (rs' & P & Q & R).
+ as (rs' & P & Q & R & S).
Simpl. rewrite ACCU. simpl. f_equal. apply Int.eqm_samerepr.
apply Zinsert_eqmod. auto. omega. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
exists rs'; split.
eapply exec_straight_opt_step_opt. simpl; eauto. auto. exact P.
- split. exact Q. intros; Simpl. rewrite R by auto. Simpl.
+ split. exact Q.
+ split.
+ { intros; Simpl.
+ rewrite R by auto. Simpl. }
+ { rewrite S. Simpl. }
Qed.
Lemma exec_loadimm_z_w:
forall rd l k rs m,
wf_decomposition l ->
+ rd <> RA ->
exists rs',
exec_straight ge fn (loadimm_z W rd l k) rs m k rs' m
/\ rs'#rd = Vint (Int.repr (recompose_int 0 l))
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
- unfold loadimm_z; destruct 1.
+ unfold loadimm_z; destruct 1; intro RD_NOT_RA.
- econstructor; split.
apply exec_straight_one. simpl; eauto. auto.
split. Simpl.
intros; Simpl.
- set (accu0 := Zinsert 0 n p 16).
set (rs1 := nextinstr (rs#rd <- (Vint (Int.repr accu0)))).
- destruct (exec_loadimm_k_w rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto.
+ destruct (exec_loadimm_k_w rd k m l H1 RD_NOT_RA rs1 accu0) as (rs2 & P & Q & R & S); auto.
unfold rs1; Simpl.
exists rs2; split.
eapply exec_straight_opt_step; eauto.
@@ -253,12 +325,13 @@ Qed.
Lemma exec_loadimm_n_w:
forall rd l k rs m,
wf_decomposition l ->
+ rd <> RA ->
exists rs',
exec_straight ge fn (loadimm_n W rd l k) rs m k rs' m
/\ rs'#rd = Vint (Int.repr (Z.lnot (recompose_int 0 l)))
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
- unfold loadimm_n; destruct 1.
+ unfold loadimm_n; destruct 1; intro RD_NOT_RA.
- econstructor; split.
apply exec_straight_one. simpl; eauto. auto.
split. Simpl.
@@ -267,7 +340,8 @@ Proof.
set (rs1 := nextinstr (rs#rd <- (Vint (Int.repr accu0)))).
destruct (exec_loadimm_k_w rd k m (negate_decomposition l)
(negate_decomposition_wf l H1)
- rs1 accu0) as (rs2 & P & Q & R).
+ RD_NOT_RA rs1 accu0)
+ as (rs2 & P & Q & R & S).
unfold rs1; Simpl.
exists rs2; split.
eapply exec_straight_opt_step; eauto.
@@ -279,7 +353,8 @@ Proof.
Qed.
Lemma exec_loadimm32:
- forall rd n k rs m,
+ forall rd n k rs m
+ (RD_NOT_RA : rd <> RA),
exists rs',
exec_straight ge fn (loadimm32 rd n k) rs m k rs' m
/\ rs'#rd = Vint n
@@ -302,13 +377,14 @@ Proof.
apply Int.eqm_samerepr. apply decompose_notint_eqmod.
apply Int.repr_unsigned. }
destruct Nat.leb.
-+ rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega.
-+ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega.
++ rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega. trivial.
++ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega. trivial.
Qed.
Lemma exec_loadimm_k_x:
forall (rd: ireg) k m l,
- wf_decomposition l ->
+ wf_decomposition l ->
+ rd <> RA ->
forall (rs: regset) accu,
rs#rd = Vlong (Int64.repr accu) ->
exists rs',
@@ -316,9 +392,9 @@ Lemma exec_loadimm_k_x:
/\ rs'#rd = Vlong (Int64.repr (recompose_int accu l))
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
- induction 1; intros rs accu ACCU; simpl.
+ induction 1; intros RD_NOT_RA rs accu ACCU; simpl.
- exists rs; split. apply exec_straight_opt_refl. auto.
-- destruct (IHwf_decomposition
+- destruct (IHwf_decomposition RD_NOT_RA
(nextinstr (rs#rd <- (insert_in_long rs#rd n p 16)))
(Zinsert accu n p 16))
as (rs' & P & Q & R).
@@ -332,19 +408,20 @@ Qed.
Lemma exec_loadimm_z_x:
forall rd l k rs m,
wf_decomposition l ->
+ rd <> RA ->
exists rs',
exec_straight ge fn (loadimm_z X rd l k) rs m k rs' m
/\ rs'#rd = Vlong (Int64.repr (recompose_int 0 l))
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
- unfold loadimm_z; destruct 1.
+ unfold loadimm_z; destruct 1; intro RD_NOT_RA.
- econstructor; split.
apply exec_straight_one. simpl; eauto. auto.
split. Simpl.
intros; Simpl.
- set (accu0 := Zinsert 0 n p 16).
set (rs1 := nextinstr (rs#rd <- (Vlong (Int64.repr accu0)))).
- destruct (exec_loadimm_k_x rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto.
+ destruct (exec_loadimm_k_x rd k m l H1 RD_NOT_RA rs1 accu0) as (rs2 & P & Q & R); auto.
unfold rs1; Simpl.
exists rs2; split.
eapply exec_straight_opt_step; eauto.
@@ -357,12 +434,13 @@ Qed.
Lemma exec_loadimm_n_x:
forall rd l k rs m,
wf_decomposition l ->
+ rd <> RA ->
exists rs',
exec_straight ge fn (loadimm_n X rd l k) rs m k rs' m
/\ rs'#rd = Vlong (Int64.repr (Z.lnot (recompose_int 0 l)))
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
- unfold loadimm_n; destruct 1.
+ unfold loadimm_n; destruct 1; intro RD_NOT_RA.
- econstructor; split.
apply exec_straight_one. simpl; eauto. auto.
split. Simpl.
@@ -371,7 +449,7 @@ Proof.
set (rs1 := nextinstr (rs#rd <- (Vlong (Int64.repr accu0)))).
destruct (exec_loadimm_k_x rd k m (negate_decomposition l)
(negate_decomposition_wf l H1)
- rs1 accu0) as (rs2 & P & Q & R).
+ RD_NOT_RA rs1 accu0) as (rs2 & P & Q & R).
unfold rs1; Simpl.
exists rs2; split.
eapply exec_straight_opt_step; eauto.
@@ -384,12 +462,13 @@ Qed.
Lemma exec_loadimm64:
forall rd n k rs m,
+ rd <> RA ->
exists rs',
exec_straight ge fn (loadimm64 rd n k) rs m k rs' m
/\ rs'#rd = Vlong n
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
- unfold loadimm64, loadimm; intros.
+ unfold loadimm64, loadimm; intros until m; intro RD_NOT_RA.
destruct (is_logical_imm64 n).
- econstructor; split.
apply exec_straight_one. simpl; eauto. auto.
@@ -406,8 +485,8 @@ Proof.
apply Int64.eqm_samerepr. apply decompose_notint_eqmod.
apply Int64.repr_unsigned. }
destruct Nat.leb.
-+ rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega.
-+ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega.
++ rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega. trivial.
++ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega. trivial.
Qed.
(** Add immediate *)
@@ -419,55 +498,59 @@ Lemma exec_addimm_aux_32:
Next (nextinstr (rs#rd <- (sem rs#r1 (Vint (Int.repr n))))) m) ->
(forall v n1 n2, sem (sem v (Vint n1)) (Vint n2) = sem v (Vint (Int.add n1 n2))) ->
forall rd r1 n k rs m,
+ (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
exists rs',
exec_straight ge fn (addimm_aux insn rd r1 (Int.unsigned n) k) rs m k rs' m
/\ rs'#rd = sem rs#r1 (Vint n)
- /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+ /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
+ /\ rs' # RA = rs # RA.
Proof.
- intros insn sem SEM ASSOC; intros. unfold addimm_aux.
+ intros insn sem SEM ASSOC; intros until m; intro RD_NOT_RA. unfold addimm_aux.
set (nlo := Zzero_ext 12 (Int.unsigned n)). set (nhi := Int.unsigned n - nlo).
assert (E: Int.unsigned n = nhi + nlo) by (unfold nhi; omega).
rewrite <- (Int.repr_unsigned n).
destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)].
- econstructor; split. apply exec_straight_one. apply SEM. Simpl.
split. Simpl. do 3 f_equal; omega.
- intros; Simpl.
+ split; intros; Simpl.
- econstructor; split. apply exec_straight_one. apply SEM. Simpl.
split. Simpl. do 3 f_equal; omega.
- intros; Simpl.
+ split; intros; Simpl.
- econstructor; split. eapply exec_straight_two.
apply SEM. apply SEM. Simpl. Simpl.
split. Simpl. rewrite ASSOC. do 2 f_equal. apply Int.eqm_samerepr.
rewrite E. auto with ints.
- intros; Simpl.
+ split; intros; Simpl.
Qed.
Lemma exec_addimm32:
forall rd r1 n k rs m,
r1 <> X16 ->
+ (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
exists rs',
exec_straight ge fn (addimm32 rd r1 n k) rs m k rs' m
/\ rs'#rd = Val.add rs#r1 (Vint n)
- /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+ /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
+ /\ rs' # RA = rs # RA.
Proof.
intros. unfold addimm32. set (nn := Int.neg n).
destruct (Int.eq n (Int.zero_ext 24 n)); [| destruct (Int.eq nn (Int.zero_ext 24 nn))].
-- apply exec_addimm_aux_32 with (sem := Val.add). auto. intros; apply Val.add_assoc.
+- apply exec_addimm_aux_32 with (sem := Val.add); auto. intros; apply Val.add_assoc.
- rewrite <- Val.sub_opp_add.
- apply exec_addimm_aux_32 with (sem := Val.sub). auto.
+ apply exec_addimm_aux_32 with (sem := Val.sub); auto.
intros. rewrite ! Val.sub_add_opp, Val.add_assoc. rewrite Int.neg_add_distr. auto.
- destruct (Int.lt n Int.zero).
+ rewrite <- Val.sub_opp_add; fold nn.
- edestruct (exec_loadimm32 X16 nn) as (rs1 & A & B & C).
+ edestruct (exec_loadimm32 X16 nn) as (rs1 & A & B & C). congruence.
econstructor; split.
eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto.
split. Simpl. rewrite B, C; eauto with asmgen.
- intros; Simpl.
-+ edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C).
+ split; intros; Simpl.
++ edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). congruence.
econstructor; split.
eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto.
split. Simpl. rewrite B, C; eauto with asmgen.
- intros; Simpl.
+ split; intros; Simpl.
Qed.
Lemma exec_addimm_aux_64:
@@ -477,10 +560,12 @@ Lemma exec_addimm_aux_64:
Next (nextinstr (rs#rd <- (sem rs#r1 (Vlong (Int64.repr n))))) m) ->
(forall v n1 n2, sem (sem v (Vlong n1)) (Vlong n2) = sem v (Vlong (Int64.add n1 n2))) ->
forall rd r1 n k rs m,
+ (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
exists rs',
exec_straight ge fn (addimm_aux insn rd r1 (Int64.unsigned n) k) rs m k rs' m
/\ rs'#rd = sem rs#r1 (Vlong n)
- /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+ /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
+ /\ rs' # RA = rs # RA.
Proof.
intros insn sem SEM ASSOC; intros. unfold addimm_aux.
set (nlo := Zzero_ext 12 (Int64.unsigned n)). set (nhi := Int64.unsigned n - nlo).
@@ -489,44 +574,46 @@ Proof.
destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)].
- econstructor; split. apply exec_straight_one. apply SEM. Simpl.
split. Simpl. do 3 f_equal; omega.
- intros; Simpl.
+ split; intros; Simpl.
- econstructor; split. apply exec_straight_one. apply SEM. Simpl.
split. Simpl. do 3 f_equal; omega.
- intros; Simpl.
+ split; intros; Simpl.
- econstructor; split. eapply exec_straight_two.
apply SEM. apply SEM. Simpl. Simpl.
split. Simpl. rewrite ASSOC. do 2 f_equal. apply Int64.eqm_samerepr.
rewrite E. auto with ints.
- intros; Simpl.
+ split; intros; Simpl.
Qed.
Lemma exec_addimm64:
forall rd r1 n k rs m,
preg_of_iregsp r1 <> X16 ->
+ (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
exists rs',
exec_straight ge fn (addimm64 rd r1 n k) rs m k rs' m
/\ rs'#rd = Val.addl rs#r1 (Vlong n)
- /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+ /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
+ /\ rs' # RA = rs # RA.
Proof.
intros.
unfold addimm64. set (nn := Int64.neg n).
destruct (Int64.eq n (Int64.zero_ext 24 n)); [| destruct (Int64.eq nn (Int64.zero_ext 24 nn))].
-- apply exec_addimm_aux_64 with (sem := Val.addl). auto. intros; apply Val.addl_assoc.
+- apply exec_addimm_aux_64 with (sem := Val.addl); auto. intros; apply Val.addl_assoc.
- rewrite <- Val.subl_opp_addl.
- apply exec_addimm_aux_64 with (sem := Val.subl). auto.
+ apply exec_addimm_aux_64 with (sem := Val.subl); auto.
intros. rewrite ! Val.subl_addl_opp, Val.addl_assoc. rewrite Int64.neg_add_distr. auto.
- destruct (Int64.lt n Int64.zero).
+ rewrite <- Val.subl_opp_addl; fold nn.
- edestruct (exec_loadimm64 X16 nn) as (rs1 & A & B & C).
+ edestruct (exec_loadimm64 X16 nn) as (rs1 & A & B & C). congruence.
econstructor; split.
eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl.
split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto.
- intros; Simpl.
-+ edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C).
+ split; intros; Simpl.
++ edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). congruence.
econstructor; split.
eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl.
split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto.
- intros; Simpl.
+ split; intros; Simpl.
Qed.
(** Logical immediate *)
@@ -543,22 +630,25 @@ Lemma exec_logicalimm32:
Next (nextinstr (rs#rd <- (sem rs##r1 (eval_shift_op_int rs#r2 s)))) m) ->
forall rd r1 n k rs m,
r1 <> X16 ->
+ (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
exists rs',
exec_straight ge fn (logicalimm32 insn1 insn2 rd r1 n k) rs m k rs' m
/\ rs'#rd = sem rs#r1 (Vint n)
- /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+ /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
+ /\ rs' # RA = rs # RA.
Proof.
intros until sem; intros SEM1 SEM2; intros. unfold logicalimm32.
destruct (is_logical_imm32 n).
- econstructor; split.
apply exec_straight_one. apply SEM1. reflexivity.
- split. Simpl. rewrite Int.repr_unsigned; auto. intros; Simpl.
-- edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C).
+ split. Simpl. rewrite Int.repr_unsigned; auto.
+ split; intros; Simpl.
+- edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). congruence.
econstructor; split.
eapply exec_straight_trans. eexact A.
apply exec_straight_one. apply SEM2. reflexivity.
split. Simpl. f_equal; auto. apply C; auto with asmgen.
- intros; Simpl.
+ split; intros; Simpl.
Qed.
Lemma exec_logicalimm64:
@@ -573,50 +663,58 @@ Lemma exec_logicalimm64:
Next (nextinstr (rs#rd <- (sem rs###r1 (eval_shift_op_long rs#r2 s)))) m) ->
forall rd r1 n k rs m,
r1 <> X16 ->
+ (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
exists rs',
exec_straight ge fn (logicalimm64 insn1 insn2 rd r1 n k) rs m k rs' m
/\ rs'#rd = sem rs#r1 (Vlong n)
- /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+ /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
+ /\ rs' # RA = rs # RA.
Proof.
intros until sem; intros SEM1 SEM2; intros. unfold logicalimm64.
destruct (is_logical_imm64 n).
- econstructor; split.
apply exec_straight_one. apply SEM1. reflexivity.
- split. Simpl. rewrite Int64.repr_unsigned. auto. intros; Simpl.
-- edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C).
+ split. Simpl. rewrite Int64.repr_unsigned. auto.
+ split; intros; Simpl.
+- edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). congruence.
econstructor; split.
eapply exec_straight_trans. eexact A.
apply exec_straight_one. apply SEM2. reflexivity.
split. Simpl. f_equal; auto. apply C; auto with asmgen.
- intros; Simpl.
+ split; intros; Simpl.
Qed.
(** Load address of symbol *)
Lemma exec_loadsymbol: forall rd s ofs k rs m,
- rd <> X16 \/ Archi.pic_code tt = false ->
+ rd <> X16 \/ Archi.pic_code tt = false ->
+ (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
exists rs',
exec_straight ge fn (loadsymbol rd s ofs k) rs m k rs' m
/\ rs'#rd = Genv.symbol_address ge s ofs
- /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+ /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
+ /\ rs'#RA = rs#RA.
Proof.
unfold loadsymbol; intros. destruct (Archi.pic_code tt).
- predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero.
+ subst ofs. econstructor; split.
apply exec_straight_one; [simpl; eauto | reflexivity].
- split. Simpl. intros; Simpl.
+ split. Simpl. split; intros; Simpl.
+
+ exploit exec_addimm64. instantiate (1 := rd). simpl. destruct H; congruence.
- intros (rs1 & A & B & C).
+ instantiate (1 := rd). assumption.
+ intros (rs1 & A & B & C & D).
econstructor; split.
econstructor. simpl; eauto. auto. eexact A.
split. simpl in B; rewrite B. Simpl.
rewrite <- Genv.shift_symbol_address_64 by auto.
rewrite Ptrofs.add_zero_l, Ptrofs.of_int64_to_int64 by auto. auto.
- intros. rewrite C by auto. Simpl.
+ split; intros. rewrite C by auto; Simpl.
+ rewrite D. Simpl.
- econstructor; split.
eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
split. Simpl. rewrite symbol_high_low; auto.
- intros; Simpl.
+ split; intros; Simpl.
Qed.
(** Shifted operands *)
@@ -725,23 +823,25 @@ Lemma exec_arith_extended:
Next (nextinstr (rs#rd <- (sem rs###r1 (eval_shift_op_long rs#r2 s)))) m) ->
forall (rd r1 r2: ireg) (ex: extension) (a: amount64) (k: code) rs m,
r1 <> X16 ->
+ (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
exists rs',
exec_straight ge fn (arith_extended insnX insnS rd r1 r2 ex a k) rs m k rs' m
/\ rs'#rd = sem rs#r1 (Op.eval_extend ex rs#r2 a)
- /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+ /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
+ /\ rs' # RA = rs # RA.
Proof.
intros sem insnX insnS EX ES; intros. unfold arith_extended. destruct (Int.ltu a (Int.repr 5)).
- econstructor; split.
apply exec_straight_one. rewrite EX; eauto. auto.
split. Simpl. f_equal. destruct ex; auto.
- intros; Simpl.
+ split; intros; Simpl.
- exploit (exec_move_extended_base X16 r2 ex). intros (rs' & A & B & C).
econstructor; split.
eapply exec_straight_trans. eexact A. apply exec_straight_one.
rewrite ES. eauto. auto.
split. Simpl. unfold ir0x. rewrite C by eauto with asmgen. f_equal.
rewrite B. destruct ex; auto.
- intros; Simpl.
+ split; intros; Simpl.
Qed.
(** Extended right shift *)
@@ -749,15 +849,18 @@ Qed.
Lemma exec_shrx32: forall (rd r1: ireg) (n: int) k v (rs: regset) m,
Val.shrx rs#r1 (Vint n) = Some v ->
r1 <> X16 ->
+ (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
exists rs',
exec_straight ge fn (shrx32 rd r1 n k) rs m k rs' m
/\ rs'#rd = v
- /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+ /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
+ /\ rs' # RA = rs # RA.
Proof.
unfold shrx32; intros. apply Val.shrx_shr_3 in H.
destruct (Int.eq n Int.zero) eqn:E.
- econstructor; split. apply exec_straight_one; [simpl;eauto|auto].
- split. Simpl. subst v; auto. intros; Simpl.
+ split. Simpl. subst v; auto.
+ split; intros; Simpl.
- generalize (Int.eq_spec n Int.one).
destruct (Int.eq n Int.one); intro ONE.
* subst n.
@@ -769,27 +872,31 @@ Proof.
change (Int.ltu Int.one Int.iwordsize) with true; simpl.
rewrite Int.or_zero_l.
reflexivity.
- ** intros; Simpl.
+ ** split; intros; Simpl.
* econstructor; split. eapply exec_straight_three.
unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto.
simpl; eauto.
unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto.
auto. auto. auto.
- split. subst v; Simpl. intros; Simpl.
+ split. subst v; Simpl.
+ split; intros; Simpl.
Qed.
Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m,
Val.shrxl rs#r1 (Vint n) = Some v ->
r1 <> X16 ->
+ (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
exists rs',
exec_straight ge fn (shrx64 rd r1 n k) rs m k rs' m
/\ rs'#rd = v
- /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+ /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
+ /\ rs' # RA = rs # RA.
Proof.
unfold shrx64; intros. apply Val.shrxl_shrl_3 in H.
destruct (Int.eq n Int.zero) eqn:E.
- econstructor; split. apply exec_straight_one; [simpl;eauto|auto].
- split. Simpl. subst v; auto. intros; Simpl.
+ split. Simpl. subst v; auto.
+ split; intros; Simpl.
- generalize (Int.eq_spec n Int.one).
destruct (Int.eq n Int.one); intro ONE.
* subst n.
@@ -801,13 +908,14 @@ Proof.
change (Int.ltu Int.one Int64.iwordsize') with true; simpl.
rewrite Int64.or_zero_l.
reflexivity.
- ** intros; Simpl.
+ ** split; intros; Simpl.
* econstructor; split. eapply exec_straight_three.
unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto.
simpl; eauto.
unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto.
auto. auto. auto.
- split. subst v; Simpl. intros; Simpl.
+ split. subst v; Simpl.
+ split; intros; Simpl.
Qed.
(** Condition bits *)
@@ -1063,6 +1171,56 @@ Ltac ArgsInv :=
| [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in *
end).
+Lemma compare_int_RA:
+ forall rs a b m,
+ compare_int rs a b m X30 = rs X30.
+Proof.
+ unfold compare_int.
+ intros.
+ repeat rewrite Pregmap.gso by congruence.
+ trivial.
+Qed.
+
+Hint Resolve compare_int_RA : asmgen.
+
+Lemma compare_long_RA:
+ forall rs a b m,
+ compare_long rs a b m X30 = rs X30.
+Proof.
+ unfold compare_long.
+ intros.
+ repeat rewrite Pregmap.gso by congruence.
+ trivial.
+Qed.
+
+Hint Resolve compare_long_RA : asmgen.
+
+Lemma compare_float_RA:
+ forall rs a b,
+ compare_float rs a b X30 = rs X30.
+Proof.
+ unfold compare_float.
+ intros.
+ destruct a; destruct b.
+ all: repeat rewrite Pregmap.gso by congruence; trivial.
+Qed.
+
+Hint Resolve compare_float_RA : asmgen.
+
+
+Lemma compare_single_RA:
+ forall rs a b,
+ compare_single rs a b X30 = rs X30.
+Proof.
+ unfold compare_single.
+ intros.
+ destruct a; destruct b.
+ all: repeat rewrite Pregmap.gso by congruence; trivial.
+Qed.
+
+Hint Resolve compare_single_RA : asmgen.
+
+
Lemma transl_cond_correct:
forall cond args k c rs m,
transl_cond cond args k = OK c ->
@@ -1071,185 +1229,218 @@ Lemma transl_cond_correct:
/\ (forall b,
eval_condition cond (map rs (map preg_of args)) m = Some b ->
eval_testcond (cond_for_cond cond) rs' = Some b)
- /\ forall r, data_preg r = true -> rs'#r = rs#r.
+ /\ (forall r, data_preg r = true -> rs'#r = rs#r)
+ /\ rs' # RA = rs # RA.
Proof.
intros until m; intros TR. destruct cond; simpl in TR; ArgsInv.
- (* Ccomp *)
econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. apply eval_testcond_compare_sint; auto.
+ repeat split; intros. apply eval_testcond_compare_sint; auto.
destruct r; reflexivity || discriminate.
- (* Ccompu *)
econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. apply eval_testcond_compare_uint; auto.
+ repeat split; intros. apply eval_testcond_compare_uint; auto.
destruct r; reflexivity || discriminate.
- (* Ccompimm *)
destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))].
+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto.
+ repeat split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto.
destruct r; reflexivity || discriminate.
+ econstructor; split.
apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto.
- split; intros. apply eval_testcond_compare_sint; auto.
+ repeat split; intros. apply eval_testcond_compare_sint; auto.
destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
++ exploit (exec_loadimm32 X16 n). congruence. intros (rs' & A & B & C).
econstructor; split.
eapply exec_straight_trans. eexact A. apply exec_straight_one.
simpl. rewrite B, C by eauto with asmgen. eauto. auto.
- split; intros. apply eval_testcond_compare_sint; auto.
- transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+ repeat split; intros. apply eval_testcond_compare_sint; auto.
+ transitivity (rs' r). destruct r; reflexivity || discriminate.
+ auto with asmgen.
+ Simpl. rewrite compare_int_RA.
+ apply C; congruence.
- (* Ccompuimm *)
destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))].
+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_uint; auto.
+ repeat split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_uint; auto.
destruct r; reflexivity || discriminate.
+ econstructor; split.
apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto.
- split; intros. apply eval_testcond_compare_uint; auto.
+ repeat split; intros. apply eval_testcond_compare_uint; auto.
destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
++ exploit (exec_loadimm32 X16 n). congruence. intros (rs' & A & B & C).
econstructor; split.
eapply exec_straight_trans. eexact A. apply exec_straight_one.
simpl. rewrite B, C by eauto with asmgen. eauto. auto.
- split; intros. apply eval_testcond_compare_uint; auto.
+ repeat split; intros. apply eval_testcond_compare_uint; auto.
transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+ Simpl. rewrite compare_int_RA.
+ apply C; congruence.
- (* Ccompshift *)
econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_sint; auto.
+ repeat split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_sint; auto.
destruct r; reflexivity || discriminate.
- (* Ccompushift *)
econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_uint; auto.
+ repeat split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_uint; auto.
destruct r; reflexivity || discriminate.
- (* Cmaskzero *)
destruct (is_logical_imm32 n).
+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); auto.
+ repeat split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); auto.
destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
++ exploit (exec_loadimm32 X16 n). congruence. intros (rs' & A & B & C).
econstructor; split.
eapply exec_straight_trans. eexact A.
apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto.
- split; intros. apply (eval_testcond_compare_sint Ceq); auto.
+ repeat split; intros. apply (eval_testcond_compare_sint Ceq); auto.
transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+ Simpl. rewrite compare_int_RA.
+ apply C; congruence.
+
- (* Cmasknotzero *)
destruct (is_logical_imm32 n).
+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); auto.
+ repeat split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); auto.
destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
+
++ exploit (exec_loadimm32 X16 n). congruence. intros (rs' & A & B & C).
econstructor; split.
eapply exec_straight_trans. eexact A.
apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto.
- split; intros. apply (eval_testcond_compare_sint Cne); auto.
+ repeat split; intros. apply (eval_testcond_compare_sint Cne); auto.
transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+ Simpl. rewrite compare_int_RA.
+ apply C; congruence.
+
- (* Ccompl *)
econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. apply eval_testcond_compare_slong; auto.
+ repeat split; intros. apply eval_testcond_compare_slong; auto.
destruct r; reflexivity || discriminate.
- (* Ccomplu *)
econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. apply eval_testcond_compare_ulong; auto.
+ repeat split; intros. apply eval_testcond_compare_ulong; auto.
destruct r; reflexivity || discriminate.
- (* Ccomplimm *)
destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_slong; auto.
+ repeat split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_slong; auto.
destruct r; reflexivity || discriminate.
+ econstructor; split.
apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. auto.
- split; intros. apply eval_testcond_compare_slong; auto.
+ repeat split; intros. apply eval_testcond_compare_slong; auto.
destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
++ exploit (exec_loadimm64 X16 n). congruence. intros (rs' & A & B & C).
econstructor; split.
eapply exec_straight_trans. eexact A. apply exec_straight_one.
simpl. rewrite B, C by eauto with asmgen. eauto. auto.
- split; intros. apply eval_testcond_compare_slong; auto.
+ repeat split; intros. apply eval_testcond_compare_slong; auto.
transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+ Simpl. rewrite compare_long_RA.
+ apply C; congruence.
+
- (* Ccompluimm *)
destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto.
+ repeat split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto.
destruct r; reflexivity || discriminate.
+ econstructor; split.
apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. auto.
- split; intros. apply eval_testcond_compare_ulong; auto.
+ repeat split; intros. apply eval_testcond_compare_ulong; auto.
destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
++ exploit (exec_loadimm64 X16 n). congruence. intros (rs' & A & B & C).
econstructor; split.
eapply exec_straight_trans. eexact A. apply exec_straight_one.
simpl. rewrite B, C by eauto with asmgen. eauto. auto.
- split; intros. apply eval_testcond_compare_ulong; auto.
+ repeat split; intros. apply eval_testcond_compare_ulong; auto.
transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+ Simpl. rewrite compare_long_RA.
+ apply C; congruence.
+
- (* Ccomplshift *)
econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_slong; auto.
+ repeat split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_slong; auto.
destruct r; reflexivity || discriminate.
- (* Ccomplushift *)
econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto.
+ repeat split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto.
destruct r; reflexivity || discriminate.
- (* Cmasklzero *)
destruct (is_logical_imm64 n).
+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto.
+ repeat split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto.
destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
++ exploit (exec_loadimm64 X16 n). congruence. intros (rs' & A & B & C).
econstructor; split.
eapply exec_straight_trans. eexact A.
apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto.
- split; intros. apply (eval_testcond_compare_slong Ceq); auto.
+ repeat split; intros. apply (eval_testcond_compare_slong Ceq); auto.
transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+ Simpl. rewrite compare_long_RA.
+ apply C; congruence.
+
- (* Cmasknotzero *)
destruct (is_logical_imm64 n).
+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
- split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto.
+ repeat split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto.
destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
++ exploit (exec_loadimm64 X16 n). congruence. intros (rs' & A & B & C).
econstructor; split.
eapply exec_straight_trans. eexact A.
apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto.
- split; intros. apply (eval_testcond_compare_slong Cne); auto.
+ repeat split; intros. apply (eval_testcond_compare_slong Cne); auto.
transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+ Simpl. rewrite compare_long_RA.
+ apply C; congruence.
+
- (* Ccompf *)
econstructor; split. apply exec_straight_one. simpl; eauto.
rewrite compare_float_inv; auto.
- split; intros. apply eval_testcond_compare_float; auto.
+ repeat split; intros. apply eval_testcond_compare_float; auto.
destruct r; discriminate || rewrite compare_float_inv; auto.
+ Simpl.
- (* Cnotcompf *)
econstructor; split. apply exec_straight_one. simpl; eauto.
rewrite compare_float_inv; auto.
- split; intros. apply eval_testcond_compare_not_float; auto.
+ repeat split; intros. apply eval_testcond_compare_not_float; auto.
destruct r; discriminate || rewrite compare_float_inv; auto.
+ Simpl.
- (* Ccompfzero *)
econstructor; split. apply exec_straight_one. simpl; eauto.
rewrite compare_float_inv; auto.
- split; intros. apply eval_testcond_compare_float; auto.
+ repeat split; intros. apply eval_testcond_compare_float; auto.
destruct r; discriminate || rewrite compare_float_inv; auto.
+ Simpl.
- (* Cnotcompfzero *)
econstructor; split. apply exec_straight_one. simpl; eauto.
rewrite compare_float_inv; auto.
- split; intros. apply eval_testcond_compare_not_float; auto.
+ repeat split; intros. apply eval_testcond_compare_not_float; auto.
destruct r; discriminate || rewrite compare_float_inv; auto.
+ Simpl.
- (* Ccompfs *)
econstructor; split. apply exec_straight_one. simpl; eauto.
rewrite compare_single_inv; auto.
- split; intros. apply eval_testcond_compare_single; auto.
+ repeat split; intros. apply eval_testcond_compare_single; auto.
destruct r; discriminate || rewrite compare_single_inv; auto.
+ Simpl.
- (* Cnotcompfs *)
econstructor; split. apply exec_straight_one. simpl; eauto.
rewrite compare_single_inv; auto.
- split; intros. apply eval_testcond_compare_not_single; auto.
+ repeat split; intros. apply eval_testcond_compare_not_single; auto.
destruct r; discriminate || rewrite compare_single_inv; auto.
+ Simpl.
- (* Ccompfszero *)
econstructor; split. apply exec_straight_one. simpl; eauto.
rewrite compare_single_inv; auto.
- split; intros. apply eval_testcond_compare_single; auto.
+ repeat split; intros. apply eval_testcond_compare_single; auto.
destruct r; discriminate || rewrite compare_single_inv; auto.
+ Simpl.
- (* Cnotcompfszero *)
econstructor; split. apply exec_straight_one. simpl; eauto.
rewrite compare_single_inv; auto.
- split; intros. apply eval_testcond_compare_not_single; auto.
+ repeat split; intros. apply eval_testcond_compare_not_single; auto.
destruct r; discriminate || rewrite compare_single_inv; auto.
+ Simpl.
Qed.
(** Translation of conditional branches *)
@@ -1262,7 +1453,8 @@ Lemma transl_cond_branch_correct:
exec_straight_opt ge fn c rs m (insn :: k) rs' m
/\ exec_instr ge fn insn rs' m =
(if b then goto_label fn lbl rs' m else Next (nextinstr rs') m)
- /\ forall r, data_preg r = true -> rs'#r = rs#r.
+ /\ (forall r, data_preg r = true -> rs'#r = rs#r)
+ /\ rs' # RA = rs # RA.
Proof.
intros until b; intros TR EV.
assert (DFL:
@@ -1271,13 +1463,14 @@ Proof.
exec_straight_opt ge fn c rs m (insn :: k) rs' m
/\ exec_instr ge fn insn rs' m =
(if b then goto_label fn lbl rs' m else Next (nextinstr rs') m)
- /\ forall r, data_preg r = true -> rs'#r = rs#r).
+ /\ (forall r, data_preg r = true -> rs'#r = rs#r)
+ /\ rs' # RA = rs # RA ).
{
unfold transl_cond_branch_default; intros.
- exploit transl_cond_correct; eauto. intros (rs' & A & B & C).
+ exploit transl_cond_correct; eauto. intros (rs' & A & B & C & D).
exists rs', (Pbc (cond_for_cond cond) lbl); split.
apply exec_straight_opt_intro. eexact A.
- split; auto. simpl. rewrite (B b) by auto. auto.
+ repeat split; auto. simpl. rewrite (B b) by auto. auto.
}
Local Opaque transl_cond transl_cond_branch_default.
destruct args as [ | a1 args]; simpl in TR; auto.
@@ -1371,13 +1564,15 @@ Ltac TranslOpSimpl :=
[ apply exec_straight_one; [simpl; eauto | reflexivity]
| split; [ rewrite ? transl_eval_shift, ? transl_eval_shiftl;
apply Val.lessdef_same; Simpl; fail
- | intros; Simpl; fail ] ].
+ | split; [ intros; Simpl; fail
+ | intros; Simpl; eauto with asmgen; fail] ]].
Ltac TranslOpBase :=
econstructor; split;
[ apply exec_straight_one; [simpl; eauto | reflexivity]
| split; [ rewrite ? transl_eval_shift, ? transl_eval_shiftl; Simpl
- | intros; Simpl; fail ] ].
+ | split; [ intros; Simpl; fail
+ | intros; Simpl; eapply RA_not_written2; eauto] ]].
Lemma transl_op_correct:
forall op args res k (rs: regset) m v c,
@@ -1386,21 +1581,29 @@ Lemma transl_op_correct:
exists rs',
exec_straight ge fn c rs m k rs' m
/\ Val.lessdef v rs'#(preg_of res)
- /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r.
+ /\ (forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r)
+ /\ rs' RA = rs RA.
Proof.
Local Opaque Int.eq Int64.eq Val.add Val.addl Int.zwordsize Int64.zwordsize.
intros until c; intros TR EV.
unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl.
- (* move *)
destruct (preg_of res) eqn:RR; try discriminate; destruct (preg_of m0) eqn:R1; inv TR.
-+ TranslOpSimpl.
-+ TranslOpSimpl.
+ all: TranslOpSimpl.
- (* intconst *)
- exploit exec_loadimm32. intros (rs' & A & B & C).
- exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen.
+ exploit exec_loadimm32. apply (ireg_of_not_RA res); eassumption.
+ intros (rs' & A & B & C).
+ exists rs'; split. eexact A. split. rewrite B; auto.
+ split. intros; auto with asmgen.
+ apply C. congruence.
+ eapply ireg_of_not_RA''; eauto.
- (* longconst *)
- exploit exec_loadimm64. intros (rs' & A & B & C).
- exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen.
+ exploit exec_loadimm64. apply (ireg_of_not_RA res); eassumption.
+ intros (rs' & A & B & C).
+ exists rs'; split. eexact A. split. rewrite B; auto.
+ split. intros; auto with asmgen.
+ apply C. congruence.
+ eapply ireg_of_not_RA''; eauto.
- (* floatconst *)
destruct (Float.eq_dec n Float.zero).
+ subst n. TranslOpSimpl.
@@ -1410,11 +1613,15 @@ Local Opaque Int.eq Int64.eq Val.add Val.addl Int.zwordsize Int64.zwordsize.
+ subst n. TranslOpSimpl.
+ TranslOpSimpl.
- (* loadsymbol *)
- exploit (exec_loadsymbol x id ofs). eauto with asmgen. intros (rs' & A & B & C).
- exists rs'; split. eexact A. split. rewrite B; auto. auto.
+ exploit (exec_loadsymbol x id ofs). eauto with asmgen.
+ apply (ireg_of_not_RA'' res); eassumption.
+ intros (rs' & A & B & C & D).
+ exists rs'; split. eexact A. split. rewrite B; auto.
+ split; auto.
- (* addrstack *)
exploit (exec_addimm64 x XSP (Ptrofs.to_int64 ofs)). simpl; eauto with asmgen.
- intros (rs' & A & B & C).
+ apply (ireg_of_not_RA'' res); eassumption.
+ intros (rs' & A & B & C & D).
exists rs'; split. eexact A. split. simpl in B; rewrite B.
Local Transparent Val.addl.
destruct (rs SP); simpl; auto. rewrite Ptrofs.of_int64_to_int64 by auto. auto.
@@ -1422,7 +1629,8 @@ Local Transparent Val.addl.
- (* shift *)
rewrite <- transl_eval_shift'. TranslOpSimpl.
- (* addimm *)
- exploit (exec_addimm32 x x0 n). eauto with asmgen. intros (rs' & A & B & C).
+ exploit (exec_addimm32 x x0 n). eauto with asmgen. eapply ireg_of_not_RA''; eassumption.
+ intros (rs' & A & B & C & D).
exists rs'; split. eexact A. split. rewrite B; auto. auto.
- (* mul *)
TranslOpBase.
@@ -1430,18 +1638,20 @@ Local Transparent Val.add.
destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int.add_zero_l; auto.
- (* andimm *)
exploit (exec_logicalimm32 (Pandimm W) (Pand W)).
- intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
- intros (rs' & A & B & C).
- exists rs'; split. eexact A. split. rewrite B; auto. auto.
+ intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. apply (ireg_of_not_RA'' res); eassumption.
+ intros (rs' & A & B & C & D).
+ exists rs'; split. eexact A. split. rewrite B; auto.
+ split; auto.
- (* orimm *)
exploit (exec_logicalimm32 (Porrimm W) (Porr W)).
- intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
- intros (rs' & A & B & C).
- exists rs'; split. eexact A. split. rewrite B; auto. auto.
+ intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. apply (ireg_of_not_RA'' res); eassumption.
+ intros (rs' & A & B & C & D).
+ exists rs'; split. eexact A. split. rewrite B; auto.
+ split; auto.
- (* xorimm *)
exploit (exec_logicalimm32 (Peorimm W) (Peor W)).
- intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
- intros (rs' & A & B & C).
+ intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. apply (ireg_of_not_RA'' res); eassumption.
+ intros (rs' & A & B & C & D).
exists rs'; split. eexact A. split. rewrite B; auto. auto.
- (* not *)
TranslOpBase.
@@ -1450,8 +1660,10 @@ Local Transparent Val.add.
TranslOpBase.
destruct (eval_shift s (rs x0) a); auto. simpl. rewrite Int.or_zero_l; auto.
- (* shrx *)
- exploit (exec_shrx32 x x0 n); eauto with asmgen. intros (rs' & A & B & C).
- econstructor; split. eexact A. split. rewrite B; auto. auto.
+ exploit (exec_shrx32 x x0 n); eauto with asmgen. apply (ireg_of_not_RA'' res); eassumption.
+ intros (rs' & A & B & C & D).
+ econstructor; split. eexact A. split. rewrite B; auto.
+ split; auto.
- (* zero-ext *)
TranslOpBase.
destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto.
@@ -1475,36 +1687,47 @@ Local Transparent Val.add.
- (* extend *)
exploit (exec_move_extended x0 x1 x a k). intros (rs' & A & B & C).
econstructor; split. eexact A.
- split. rewrite B; auto. eauto with asmgen.
+ split. rewrite B; auto.
+ split; eauto with asmgen.
- (* addext *)
exploit (exec_arith_extended Val.addl Paddext (Padd X)).
- auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C).
- econstructor; split. eexact A. split. rewrite B; auto. auto.
+ auto. auto. instantiate (1 := x1). eauto with asmgen.
+ apply (ireg_of_not_RA'' res); eassumption.
+ intros (rs' & A & B & C & D).
+ econstructor; split. eexact A. split. rewrite B; auto.
+ split; auto.
- (* addlimm *)
exploit (exec_addimm64 x x0 n). simpl. generalize (ireg_of_not_X16 _ _ EQ1). congruence.
- intros (rs' & A & B & C).
+ apply (ireg_of_not_RA'' res); eassumption.
+ intros (rs' & A & B & C & D).
exists rs'; split. eexact A. split. simpl in B; rewrite B; auto. auto.
- (* subext *)
exploit (exec_arith_extended Val.subl Psubext (Psub X)).
- auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C).
- econstructor; split. eexact A. split. rewrite B; auto. auto.
+ auto. auto. instantiate (1 := x1). eauto with asmgen.
+ apply (ireg_of_not_RA'' res); eassumption.
+ intros (rs' & A & B & C & D).
+ econstructor; split. eexact A. split. rewrite B; auto.
+ split; auto.
- (* mull *)
TranslOpBase.
destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int64.add_zero_l; auto.
- (* andlimm *)
exploit (exec_logicalimm64 (Pandimm X) (Pand X)).
intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
- intros (rs' & A & B & C).
+ apply (ireg_of_not_RA'' res); eassumption.
+ intros (rs' & A & B & C & D).
exists rs'; split. eexact A. split. rewrite B; auto. auto.
- (* orlimm *)
exploit (exec_logicalimm64 (Porrimm X) (Porr X)).
intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
- intros (rs' & A & B & C).
+ apply (ireg_of_not_RA'' res); eassumption.
+ intros (rs' & A & B & C & D).
exists rs'; split. eexact A. split. rewrite B; auto. auto.
- (* xorlimm *)
exploit (exec_logicalimm64 (Peorimm X) (Peor X)).
intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
- intros (rs' & A & B & C).
+ apply (ireg_of_not_RA'' res); eassumption.
+ intros (rs' & A & B & C & D).
exists rs'; split. eexact A. split. rewrite B; auto. auto.
- (* notl *)
TranslOpBase.
@@ -1513,7 +1736,8 @@ Local Transparent Val.add.
TranslOpBase.
destruct (eval_shiftl s (rs x0) a); auto. simpl. rewrite Int64.or_zero_l; auto.
- (* shrx *)
- exploit (exec_shrx64 x x0 n); eauto with asmgen. intros (rs' & A & B & C).
+ exploit (exec_shrx64 x x0 n); eauto with asmgen.
+ apply (ireg_of_not_RA'' res); eassumption. intros (rs' & A & B & C & D ).
econstructor; split. eexact A. split. rewrite B; auto. auto.
- (* zero-ext-l *)
TranslOpBase.
@@ -1534,35 +1758,37 @@ Local Transparent Val.add.
TranslOpBase.
destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.sign_ext_shr'_min; auto using a64_range.
- (* condition *)
- exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C).
+ exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C & D).
econstructor; split.
eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto.
split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *.
rewrite (B b) by auto. auto.
auto.
- intros; Simpl.
+ split; intros; Simpl.
- (* select *)
destruct (preg_of res) eqn:RES; monadInv TR.
+ (* integer *)
generalize (ireg_of_eq _ _ EQ) (ireg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2.
- exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C).
+ exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C & D).
econstructor; split.
eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto.
split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *.
rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize.
rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen.
auto.
- intros; Simpl.
+ split; intros; Simpl.
+ rewrite <- D.
+ eapply RA_not_written2; eassumption.
+ (* FP *)
generalize (freg_of_eq _ _ EQ) (freg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2.
- exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C).
+ exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C & D).
econstructor; split.
eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto.
split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *.
rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize.
rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen.
auto.
- intros; Simpl.
+ split; intros; Simpl.
Qed.
(** Translation of addressing modes, loads, stores *)
@@ -1574,7 +1800,8 @@ Lemma transl_addressing_correct:
exists ad rs',
exec_straight_opt ge fn c rs m (insn ad :: k) rs' m
/\ Asm.eval_addressing ge ad rs' = Vptr b o
- /\ forall r, data_preg r = true -> rs' r = rs r.
+ /\ (forall r, data_preg r = true -> rs' r = rs r)
+ /\ rs' # RA = rs # RA.
Proof.
intros until o; intros TR EV.
unfold transl_addressing in TR; destruct addr; ArgsInv; SimplEval EV.
@@ -1582,10 +1809,10 @@ Proof.
destruct (offset_representable sz ofs); inv EQ0.
+ econstructor; econstructor; split. apply exec_straight_opt_refl.
auto.
-+ exploit (exec_loadimm64 X16 ofs). intros (rs' & A & B & C).
++ exploit (exec_loadimm64 X16 ofs). congruence. intros (rs' & A & B & C).
econstructor; exists rs'; split. apply exec_straight_opt_intro; eexact A.
split. simpl. rewrite B, C by eauto with asmgen. auto.
- eauto with asmgen.
+ split; eauto with asmgen.
- (* Aindexed2 *)
econstructor; econstructor; split. apply exec_straight_opt_refl.
auto.
@@ -1601,33 +1828,38 @@ Proof.
+ econstructor; econstructor; split.
apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. auto.
split. simpl. Simpl. rewrite H0. simpl. rewrite Ptrofs.add_zero. auto.
- intros; Simpl.
+ split; intros; Simpl.
- (* Aindexed2ext *)
destruct (Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz)); inv EQ2.
+ econstructor; econstructor; split. apply exec_straight_opt_refl.
split; auto. destruct x; auto.
+ exploit (exec_arith_extended Val.addl Paddext (Padd X)); auto.
instantiate (1 := x0). eauto with asmgen.
- intros (rs' & A & B & C).
+ instantiate (1 := X16). simpl. congruence.
+ intros (rs' & A & B & C & D).
econstructor; exists rs'; split.
apply exec_straight_opt_intro. eexact A.
split. simpl. rewrite B. rewrite Val.addl_assoc. f_equal.
unfold Op.eval_extend; destruct x, (rs x1); simpl; auto; rewrite ! a64_range;
simpl; rewrite Int64.add_zero; auto.
- intros. apply C; eauto with asmgen.
+ split; intros.
+ apply C; eauto with asmgen.
+ trivial.
- (* Aglobal *)
destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz); inv TR.
+ econstructor; econstructor; split.
apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. auto.
split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence.
- intros; Simpl.
-+ exploit (exec_loadsymbol X16 id ofs). auto. intros (rs' & A & B & C).
+ split; intros; Simpl.
++ exploit (exec_loadsymbol X16 id ofs). auto.
+ simpl. congruence.
+ intros (rs' & A & B & C & D).
econstructor; exists rs'; split.
apply exec_straight_opt_intro. eexact A.
split. simpl.
rewrite B. rewrite <- Genv.shift_symbol_address_64, Ptrofs.add_zero by auto.
simpl in EV. congruence.
- auto with asmgen.
+ split; auto with asmgen.
- (* Ainstrack *)
assert (E: Val.addl (rs SP) (Vlong (Ptrofs.to_int64 ofs)) = Vptr b o).
{ simpl in EV. inv EV. destruct (rs SP); simpl in H1; inv H1. simpl.
@@ -1635,7 +1867,9 @@ Proof.
destruct (offset_representable sz (Ptrofs.to_int64 ofs)); inv TR.
+ econstructor; econstructor; split. apply exec_straight_opt_refl.
auto.
-+ exploit (exec_loadimm64 X16 (Ptrofs.to_int64 ofs)). intros (rs' & A & B & C).
++ exploit (exec_loadimm64 X16 (Ptrofs.to_int64 ofs)).
+ simpl. congruence.
+ intros (rs' & A & B & C).
econstructor; exists rs'; split.
apply exec_straight_opt_intro. eexact A.
split. simpl. rewrite B, C by eauto with asmgen. auto.
@@ -1650,7 +1884,8 @@ Lemma transl_load_correct:
exists rs',
exec_straight ge fn c rs m k rs' m
/\ rs'#(preg_of dst) = v
- /\ forall r, data_preg r = true -> r <> preg_of dst -> rs' r = rs r.
+ /\ (forall r, data_preg r = true -> r <> preg_of dst -> rs' r = rs r)
+ /\ rs' # RA = rs # RA.
Proof.
intros. destruct vaddr; try discriminate.
assert (A: exists sz insn,
@@ -1663,14 +1898,17 @@ Proof.
do 2 econstructor; (split; [eassumption|auto]).
}
destruct A as (sz & insn & B & C).
- exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R).
+ exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R & S).
assert (X: exec_load ge chunk (fun v => v) ad (preg_of dst) rs' m =
Next (nextinstr (rs'#(preg_of dst) <- v)) m).
{ unfold exec_load. rewrite Q, H1. auto. }
econstructor; split.
eapply exec_straight_opt_right. eexact P.
apply exec_straight_one. rewrite C, X; eauto. Simpl.
- split. Simpl. intros; Simpl.
+ split. Simpl.
+ split; intros; Simpl.
+ rewrite <- S.
+ apply RA_not_written.
Qed.
Lemma transl_store_correct:
@@ -1680,7 +1918,8 @@ Lemma transl_store_correct:
Mem.storev chunk m vaddr rs#(preg_of src) = Some m' ->
exists rs',
exec_straight ge fn c rs m k rs' m'
- /\ forall r, data_preg r = true -> rs' r = rs r.
+ /\ (forall r, data_preg r = true -> rs' r = rs r)
+ /\ rs' # RA = rs # RA.
Proof.
intros. destruct vaddr; try discriminate.
set (chunk' := match chunk with Mint8signed => Mint8unsigned
@@ -1696,7 +1935,7 @@ Proof.
do 2 econstructor; (split; [eassumption|auto]).
}
destruct A as (sz & insn & B & C).
- exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R).
+ exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R & S).
assert (X: Mem.storev chunk' m (Vptr b i) rs#(preg_of src) = Some m').
{ rewrite <- H1. unfold chunk'. destruct chunk; auto; simpl; symmetry.
apply Mem.store_signed_unsigned_8.
@@ -1707,7 +1946,7 @@ Proof.
econstructor; split.
eapply exec_straight_opt_right. eexact P.
apply exec_straight_one. rewrite C, Y; eauto. Simpl.
- intros; Simpl.
+ split; intros; Simpl.
Qed.
(** Translation of indexed memory accesses *)
@@ -1725,7 +1964,9 @@ Proof.
{ destruct (rs base); try discriminate. simpl in *. rewrite Ptrofs.of_int64_to_int64 by auto. auto. }
destruct offset_representable.
- econstructor; econstructor; split. apply exec_straight_opt_refl. auto.
-- exploit (exec_loadimm64 X16); eauto. intros (rs' & A & B & C).
+- exploit (exec_loadimm64 X16); eauto.
+ simpl. congruence.
+ intros (rs' & A & B & C).
econstructor; econstructor; split. apply exec_straight_opt_intro; eexact A.
split. simpl. rewrite B, C by eauto with asmgen. auto. auto.
Qed.
@@ -1736,7 +1977,7 @@ Lemma loadptr_correct: forall (base: iregsp) ofs dst k m v (rs: regset),
exists rs',
exec_straight ge fn (loadptr base ofs dst k) rs m k rs' m
/\ rs'#dst = v
- /\ forall r, r <> PC -> r <> X16 -> r <> dst -> rs' r = rs r.
+ /\ (forall r, r <> PC -> r <> X16 -> r <> dst -> rs' r = rs r).
Proof.
intros.
destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate.
@@ -1744,7 +1985,8 @@ Proof.
econstructor; split.
eapply exec_straight_opt_right. eexact A.
apply exec_straight_one. simpl. unfold exec_load. rewrite B, H. eauto. auto.
- split. Simpl. intros; Simpl.
+ split. Simpl.
+ intros; Simpl.
Qed.
Lemma storeptr_correct: forall (base: iregsp) ofs (src: ireg) k m m' (rs: regset),
@@ -1753,7 +1995,8 @@ Lemma storeptr_correct: forall (base: iregsp) ofs (src: ireg) k m m' (rs: regset
src <> X16 ->
exists rs',
exec_straight ge fn (storeptr src base ofs k) rs m k rs' m'
- /\ forall r, r <> PC -> r <> X16 -> rs' r = rs r.
+ /\ (forall r, r <> PC -> r <> X16 -> rs' r = rs r)
+ /\ rs' RA = rs RA.
Proof.
intros.
destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate.
@@ -1761,7 +2004,7 @@ Proof.
econstructor; split.
eapply exec_straight_opt_right. eexact A.
apply exec_straight_one. simpl. unfold exec_store. rewrite B, C, H by eauto with asmgen. eauto. auto.
- intros; Simpl.
+ split; intros; Simpl.
Qed.
Lemma loadind_correct: forall (base: iregsp) ofs ty dst k c (rs: regset) m v,
@@ -1771,7 +2014,8 @@ Lemma loadind_correct: forall (base: iregsp) ofs ty dst k c (rs: regset) m v,
exists rs',
exec_straight ge fn c rs m k rs' m
/\ rs'#(preg_of dst) = v
- /\ forall r, data_preg r = true -> r <> preg_of dst -> rs' r = rs r.
+ /\ (forall r, data_preg r = true -> r <> preg_of dst -> rs' r = rs r)
+ /\ rs' RA = rs RA.
Proof.
intros.
destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate.
@@ -1787,7 +2031,10 @@ Proof.
econstructor; split.
eapply exec_straight_opt_right. eexact A.
apply exec_straight_one. rewrite SEM. unfold exec_load. rewrite B, H0. eauto. Simpl.
- split. Simpl. intros; Simpl.
+ split. Simpl.
+ split. intros; Simpl.
+ Simpl. rewrite RA_not_written.
+ apply C; congruence.
Qed.
Lemma storeind_correct: forall (base: iregsp) ofs ty src k c (rs: regset) m m',
@@ -1796,7 +2043,8 @@ Lemma storeind_correct: forall (base: iregsp) ofs ty src k c (rs: regset) m m',
preg_of_iregsp base <> IR X16 ->
exists rs',
exec_straight ge fn c rs m k rs' m'
- /\ forall r, data_preg r = true -> rs' r = rs r.
+ /\ (forall r, data_preg r = true -> rs' r = rs r)
+ /\ rs' RA = rs RA.
Proof.
intros.
destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate.
@@ -1814,13 +2062,15 @@ Proof.
apply exec_straight_one. rewrite SEM.
unfold exec_store. rewrite B, C, H0 by eauto with asmgen. eauto.
Simpl.
- intros; Simpl.
+ split. intros; Simpl.
+ Simpl.
Qed.
Lemma make_epilogue_correct:
forall ge0 f m stk soff cs m' ms rs k tm,
+ (is_leaf_function f = true -> rs # (IR RA) = parent_ra cs) ->
load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) ->
- load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs) ->
+ ((* FIXME is_leaf_function f = false -> *) load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs)) ->
Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
agree ms (Vptr stk soff) rs ->
Mem.extends m tm ->
@@ -1831,18 +2081,46 @@ Lemma make_epilogue_correct:
/\ Mem.extends m' tm'
/\ rs'#RA = parent_ra cs
/\ rs'#SP = parent_sp cs
- /\ (forall r, r <> PC -> r <> SP -> r <> X30 -> r <> X16 -> rs'#r = rs#r).
+ /\ (forall r, r <> PC -> r <> SP -> r <> RA -> r <> X16 -> rs'#r = rs#r).
Proof.
- intros until tm; intros LP LRA FREE AG MEXT MCS.
+ intros until tm; intros LEAF_RA LP LRA FREE AG MEXT MCS.
+
+ (* FIXME
+ Cannot be used at this point
+ destruct (is_leaf_function f) eqn:IS_LEAF.
+ {
+ exploit Mem.loadv_extends. eauto. eexact LP. auto. simpl. intros (parent' & LP' & LDP').
+ exploit lessdef_parent_sp; eauto. intros EQ; subst parent'; clear LDP'.
+ exploit Mem.free_parallel_extends; eauto. intros (tm' & FREE' & MEXT').
+ unfold make_epilogue.
+ rewrite IS_LEAF.
+
+ econstructor; econstructor; split.
+ apply exec_straight_one. simpl.
+ rewrite <- (sp_val _ _ _ AG). simpl; rewrite LP'.
+ rewrite FREE'. eauto. auto.
+ split. apply agree_nextinstr. apply agree_set_other; auto.
+ apply agree_change_sp with (Vptr stk soff).
+ apply agree_exten with rs; auto.
+ eapply parent_sp_def; eauto.
+ split. auto.
+ split. Simpl.
+ split. Simpl.
+ intros. Simpl.
+ }
+ lapply LRA. 2: reflexivity.
+ clear LRA. intro LRA. *)
exploit Mem.loadv_extends. eauto. eexact LP. auto. simpl. intros (parent' & LP' & LDP').
exploit Mem.loadv_extends. eauto. eexact LRA. auto. simpl. intros (ra' & LRA' & LDRA').
exploit lessdef_parent_sp; eauto. intros EQ; subst parent'; clear LDP'.
exploit lessdef_parent_ra; eauto. intros EQ; subst ra'; clear LDRA'.
exploit Mem.free_parallel_extends; eauto. intros (tm' & FREE' & MEXT').
- unfold make_epilogue.
+ unfold make_epilogue.
+ (* FIXME rewrite IS_LEAF. *)
exploit (loadptr_correct XSP (fn_retaddr_ofs f)).
instantiate (2 := rs). simpl. rewrite <- (sp_val _ _ _ AG). simpl. eexact LRA'. simpl; congruence.
intros (rs1 & A1 & B1 & C1).
+
econstructor; econstructor; split.
eapply exec_straight_trans. eexact A1. apply exec_straight_one. simpl.
simpl; rewrite (C1 SP) by auto with asmgen. rewrite <- (sp_val _ _ _ AG). simpl; rewrite LP'.
@@ -1857,4 +2135,4 @@ Proof.
intros. Simpl.
Qed.
-End CONSTRUCTORS. \ No newline at end of file
+End CONSTRUCTORS.
diff --git a/aarch64/DuplicateOpcodeHeuristic.ml b/aarch64/DuplicateOpcodeHeuristic.ml
index 85505245..5fc2156c 100644
--- a/aarch64/DuplicateOpcodeHeuristic.ml
+++ b/aarch64/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,27 @@
-exception HeuristicSucceeded
-
-let opcode_heuristic code cond ifso ifnot preferred = ()
+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
+ | Ccomplimm (c, n) | Ccompluimm (c, n) -> if n == Integers.Int64.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/DuplicateOpcodeHeuristic.ml b/arm/DuplicateOpcodeHeuristic.ml
index 85505245..9b6a6409 100644
--- a/arm/DuplicateOpcodeHeuristic.ml
+++ b/arm/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,22 @@
-exception HeuristicSucceeded
-
-let opcode_heuristic code cond ifso ifnot preferred = ()
+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/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 209527b9..a84f9754 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -502,11 +502,15 @@ let rec invert_iconds code = function
let duplicate_aux f =
let entrypoint = f.fn_entrypoint in
let code = f.fn_code in
- let traces = select_traces (to_ttl_code code entrypoint) entrypoint in
- let icond_code = invert_iconds code traces in
- let preds = get_predecessors_rtl icond_code in
- if !Clflags.option_fduplicate >= 1 then
- let (new_code, pTreeId) = ((* print_traces traces; *) superblockify_traces icond_code preds traces) in
- ((new_code, f.fn_entrypoint), pTreeId)
+ if !Clflags.option_fduplicate < 0 then
+ ((code, entrypoint), make_identity_ptree code)
else
- ((icond_code, entrypoint), make_identity_ptree code)
+ let traces = select_traces (to_ttl_code code entrypoint) entrypoint in
+ let icond_code = invert_iconds code traces in
+ let preds = get_predecessors_rtl icond_code in
+ if !Clflags.option_fduplicate >= 1 then
+ let (new_code, pTreeId) = ((* print_traces traces; *) superblockify_traces icond_code preds traces) in
+ ((new_code, f.fn_entrypoint), pTreeId)
+ else
+ ((icond_code, entrypoint), make_identity_ptree code)
+
diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml
index d58704ca..cf308962 100644
--- a/backend/Inliningaux.ml
+++ b/backend/Inliningaux.ml
@@ -17,7 +17,8 @@ open Maps
open Op
open Ordered
open! RTL
-
+open Camlcoq
+
module PSet = Make(OrderedPositive)
type inlining_info = {
@@ -83,13 +84,15 @@ let static_called_once id io =
else
false
-(* To be considered: heuristics based on size of function? *)
+(* D. Monniaux: attempt at heuristic based on size *)
+let small_enough (f : coq_function) =
+ P.to_int (RTL.max_pc_function f) <= !Clflags.option_inline_auto_threshold
let should_inline (io: inlining_info) (id: ident) (f: coq_function) =
if !Clflags.option_finline then begin
match C2C.atom_inline id with
| C2C.Inline -> true
| C2C.Noinline -> false
- | C2C.No_specifier -> static_called_once id io
+ | C2C.No_specifier -> static_called_once id io || small_enough f
end else
false
diff --git a/config_arm.sh b/config_arm.sh
index eed55fab..1861e029 100755
--- a/config_arm.sh
+++ b/config_arm.sh
@@ -1 +1 @@
-exec ./config_simple.sh arm-linux --toolprefix arm-linux-gnueabihf- "$@"
+exec ./config_simple.sh arm-linux --toolprefix arm-linux-gnueabi- "$@"
diff --git a/config_armhf.sh b/config_armhf.sh
new file mode 100755
index 00000000..8a1302bd
--- /dev/null
+++ b/config_armhf.sh
@@ -0,0 +1 @@
+exec ./config_simple.sh arm-eabihf --toolprefix arm-linux-gnueabihf- "$@"
diff --git a/config_ppc64.sh b/config_ppc64.sh
new file mode 100755
index 00000000..df31c18f
--- /dev/null
+++ b/config_ppc64.sh
@@ -0,0 +1 @@
+exec ./config_simple.sh ppc64-linux --toolprefix powerpc64-linux-gnu- "$@"
diff --git a/config_rv32.sh b/config_rv32.sh
index 654cacfa..a5a5cf1c 100755
--- a/config_rv32.sh
+++ b/config_rv32.sh
@@ -1 +1 @@
-exec ./config_simple.sh rv32-linux --toolprefix riscv64-unknown-elf- "$@"
+exec ./config_simple.sh rv32-linux --toolprefix riscv64-linux-gnu- "$@"
diff --git a/config_rv64.sh b/config_rv64.sh
index e95f8a70..0698c2ff 100755
--- a/config_rv64.sh
+++ b/config_rv64.sh
@@ -1 +1 @@
-exec ./config_simple.sh rv64-linux --toolprefix riscv64-unknown-elf- "$@"
+exec ./config_simple.sh rv64-linux --toolprefix riscv64-linux-gnu- "$@"
diff --git a/config_simple.sh b/config_simple.sh
index f02680c4..e2d3844c 100755
--- a/config_simple.sh
+++ b/config_simple.sh
@@ -3,4 +3,9 @@ shift
version=`git rev-parse --short HEAD`
branch=`git rev-parse --abbrev-ref HEAD`
date=`date -I`
-./configure --prefix /opt/CompCert/${branch}/${date}_${version}/$arch "$@" $arch
+
+if test "x$CCOMP_INSTALL_PREFIX" = "x" ;
+then CCOMP_INSTALL_PREFIX=/opt/CompCert ;
+fi
+
+./configure --prefix ${CCOMP_INSTALL_PREFIX}/${branch}/${date}_${version}/$arch "$@" $arch
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index f60e15a3..9e17cb7e 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -2428,8 +2428,8 @@ let enter_typedef loc env sto (s, ty, init) =
env
end
else begin
- error loc "typedef redefinition with different types (%a vs %a)"
- (print_typ env) ty (print_typ env) ty';
+ error loc "redefinition of typedef '%s' with different type (%a vs %a)"
+ s (print_typ env) ty (print_typ env) ty';
env
end
| _ ->
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 79c0bce0..6986fb96 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -28,7 +28,7 @@ let option_fconstprop = ref true
let option_fcse = ref true
let option_fcse2 = ref true
let option_fredundancy = ref true
-let option_fduplicate = ref 0
+let option_fduplicate = ref (-1)
let option_finvertcond = ref true
let option_ftracelinearize = ref false
let option_fpostpass = ref true
@@ -81,3 +81,4 @@ let option_faddx = ref false
let option_fcoalesce_mem = ref true
let option_fforward_moves = ref true
let option_all_loads_nontrap = ref false
+let option_inline_auto_threshold = ref 0
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 43aedf50..388482a0 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -190,6 +190,7 @@ Processing options:
-Os Optimize for code size in preference to code speed
-Obranchless Optimize to generate fewer conditional branches; try to produce
branch-free instruction sequences as much as possible
+ -finline-auto-threshold n Inline functions under size n
-ftailcalls Optimize function calls in tail position [on]
-fconst-prop Perform global constant propagation [on]
-ffloat-const-prop <n> Control constant propagation of floats
@@ -200,7 +201,11 @@ Processing options:
-fpostpass Perform postpass scheduling (only for K1 architecture) [on]
-fpostpass= <optim> Perform postpass scheduling with the specified optimization [list]
(<optim>=list: list scheduling, <optim>=ilp: ILP, <optim>=greedy: just packing bundles)
- -fduplicate Perform tail duplication to form superblocks on predicted traces
+ -fduplicate <nb_nodes> Perform tail duplication to form superblocks on predicted traces
+ nb_nodes control the heuristic deciding to duplicate or not
+ A value of -1 desactivates the entire pass (including branch prediction)
+ A value of 0 desactivates the duplication (but activates the branch prediction)
+ FIXME : this is desactivated by default for now
-finvertcond Invert conditions based on predicted paths (to prefer fallthrough).
Requires -fduplicate to be also activated [on]
-ftracelinearize Linearizes based on the traces identified by duplicate phase
@@ -322,6 +327,7 @@ let cmdline_actions =
_Regexp "-O[123]$", Unit (set_all optimization_options);
Exact "-Os", Set option_Osize;
Exact "-Obranchless", Set option_Obranchless;
+ Exact "-finline-auto-threshold", Integer (fun n -> option_inline_auto_threshold := n);
Exact "-fsmall-data", Integer(fun n -> option_small_data := n);
Exact "-fsmall-const", Integer(fun n -> option_small_const := n);
Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n);
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 5b44ddaa..00df01e3 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1483,6 +1483,8 @@ Proof.
destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; omega.
Qed.
+Ltac splitall := repeat match goal with |- _ /\ _ => split end.
+
Lemma transl_op_correct:
forall op args res k (rs: regset) m v c,
transl_op op args res k = OK c ->
@@ -1517,21 +1519,21 @@ Opaque Int.eq.
- (* Ocast8signed *)
econstructor; split.
eapply exec_straight_two. simpl;eauto. simpl;eauto.
- split; intros; simpl; Simpl.
+ repeat split; intros; simpl; Simpl.
assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto.
destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. rewrite A.
apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity.
- (* Ocast16signed *)
econstructor; split.
eapply exec_straight_two. simpl;eauto. simpl;eauto.
- split; intros; Simpl.
+ repeat split; intros; Simpl.
assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto.
destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. rewrite A.
apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity.
- (* Oshrximm *)
econstructor; split.
+ apply exec_straight_one. simpl. eauto.
- + split.
+ + repeat split.
* rewrite Pregmap.gss.
subst v.
destruct (rs x0); simpl; trivial.
@@ -1542,7 +1544,7 @@ Opaque Int.eq.
- (* Oshrxlimm *)
econstructor; split.
+ apply exec_straight_one. simpl. eauto.
- + split.
+ + repeat split.
* rewrite Pregmap.gss.
subst v.
destruct (rs x0); simpl; trivial.
@@ -1553,7 +1555,7 @@ Opaque Int.eq.
- (* Ocmp *)
exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
- exists rs'; split. eexact A. eauto with asmgen.
+ exists rs'; repeat split; eauto with asmgen.
- (* Osel *)
unfold conditional_move in *.
@@ -1572,72 +1574,73 @@ Opaque Int.eq.
destruct c0; simpl in *.
- all:
- destruct c; simpl in *; inv EQ2;
- econstructor; split; try (apply exec_straight_one; constructor);
- split; try (simpl; intros; rewrite Pregmap.gso; trivial; assumption);
- unfold Val.select; simpl;
- unfold cmove, cmoveu;
- rewrite Pregmap.gss;
- destruct (rs x1); simpl; trivial;
- try rewrite int_ltu_to_neq;
- try rewrite int64_ltu_to_neq;
- try change (Int64.eq Int64.zero Int64.zero) with true;
- try destruct Archi.ptr64;
- repeat rewrite if_neg;
- simpl;
- trivial;
- try destruct (_ || _);
- trivial;
- try apply Val.lessdef_normalize.
+ all: destruct c.
+ all: simpl in *.
+ all: inv EQ2.
+ all: econstructor; splitall.
+ all: try apply exec_straight_one.
+ all: intros; simpl; trivial.
+ all: unfold Val.select, cmove, cmoveu; simpl.
+ all: destruct (rs x1); simpl; trivial.
+ all: try rewrite int_ltu_to_neq.
+ all: try rewrite int64_ltu_to_neq.
+ all: try change (Int64.eq Int64.zero Int64.zero) with true.
+ all: try destruct Archi.ptr64.
+ all: try rewrite Pregmap.gss.
+ all: repeat rewrite if_neg.
+ all: simpl.
+ all: try destruct (_ || _).
+ all: try apply Val.lessdef_normalize.
+ all: trivial. (* no more lessdef *)
+ all: apply Pregmap.gso; congruence.
- (* Oselimm *)
unfold conditional_move_imm32 in *.
destruct c0; simpl in *.
- all:
- destruct c; simpl in *; inv EQ0;
- econstructor; split; try (apply exec_straight_one; constructor);
- split; try (simpl; intros; rewrite Pregmap.gso; trivial; assumption);
- unfold Val.select; simpl;
- unfold cmove, cmoveu;
- rewrite Pregmap.gss;
- destruct (rs x0); simpl; trivial;
- try rewrite int_ltu_to_neq;
- try rewrite int64_ltu_to_neq;
- try change (Int64.eq Int64.zero Int64.zero) with true;
- try destruct Archi.ptr64;
- repeat rewrite if_neg;
- simpl;
- trivial;
- try destruct (_ || _);
- trivial;
- try apply Val.lessdef_normalize.
-
+ all: destruct c.
+ all: simpl in *.
+ all: inv EQ0.
+ all: econstructor; splitall.
+ all: try apply exec_straight_one.
+ all: intros; simpl; trivial.
+ all: unfold Val.select, cmove, cmoveu; simpl.
+ all: destruct (rs x0); simpl; trivial.
+ all: try rewrite int_ltu_to_neq.
+ all: try rewrite int64_ltu_to_neq.
+ all: try change (Int64.eq Int64.zero Int64.zero) with true.
+ all: try destruct Archi.ptr64.
+ all: try rewrite Pregmap.gss.
+ all: repeat rewrite if_neg.
+ all: simpl.
+ all: try destruct (_ || _).
+ all: try apply Val.lessdef_normalize.
+ all: trivial. (* no more lessdef *)
+ all: apply Pregmap.gso; congruence.
- (* Osellimm *)
unfold conditional_move_imm64 in *.
destruct c0; simpl in *.
- all:
- destruct c; simpl in *; inv EQ0;
- econstructor; split; try (apply exec_straight_one; constructor);
- split; try (simpl; intros; rewrite Pregmap.gso; trivial; assumption);
- unfold Val.select; simpl;
- unfold cmove, cmoveu;
- rewrite Pregmap.gss;
- destruct (rs x0); simpl; trivial;
- try rewrite int_ltu_to_neq;
- try rewrite int64_ltu_to_neq;
- try change (Int64.eq Int64.zero Int64.zero) with true;
- try destruct Archi.ptr64;
- repeat rewrite if_neg;
- simpl;
- trivial;
- try destruct (_ || _);
- trivial;
- try apply Val.lessdef_normalize.
-
+ all: destruct c.
+ all: simpl in *.
+ all: inv EQ0.
+ all: econstructor; splitall.
+ all: try apply exec_straight_one.
+ all: intros; simpl; trivial.
+ all: unfold Val.select, cmove, cmoveu; simpl.
+ all: destruct (rs x0); simpl; trivial.
+ all: try rewrite int_ltu_to_neq.
+ all: try rewrite int64_ltu_to_neq.
+ all: try change (Int64.eq Int64.zero Int64.zero) with true.
+ all: try destruct Archi.ptr64.
+ all: try rewrite Pregmap.gss.
+ all: repeat rewrite if_neg.
+ all: simpl.
+ all: try destruct (_ || _).
+ all: try apply Val.lessdef_normalize.
+ all: trivial. (* no more lessdef *)
+ all: apply Pregmap.gso; congruence.
Qed.
(** Memory accesses *)
diff --git a/powerpc/DuplicateOpcodeHeuristic.ml b/powerpc/DuplicateOpcodeHeuristic.ml
index 85505245..33be79e8 100644
--- a/powerpc/DuplicateOpcodeHeuristic.ml
+++ b/powerpc/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,27 @@
-exception HeuristicSucceeded
-
-let opcode_heuristic code cond ifso ifnot preferred = ()
+(* open Camlcoq *)
+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
+ | Ccomplimm (c, n) | Ccompluimm (c, n) -> if n == Integers.Int64.zero then (match c with
+ | Clt | Cle -> Some false
+ | Cgt | Cge -> Some true
+ | _ -> None
+ ) else None
+ | Ccompf c -> (match c with
+ | Ceq -> Some false
+ | Cne -> Some true
+ | _ -> None
+ )
+ | Cnotcompf c -> (match c with
+ | Ceq -> Some true
+ | Cne -> Some false
+ | _ -> None
+ )
+ | _ -> None
diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index 7f8048f6..17326139 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -210,7 +210,7 @@ Definition int_arg (ri rf ofs: Z) (ty: typ)
| Some r =>
One(R r) :: rec (ri + 1) rf ofs
| None =>
- let ofs := align ofs (typealign ty) in
+ let ofs := align ofs (typesize ty) in
One(S Outgoing ofs ty)
:: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty))
end.
@@ -228,13 +228,13 @@ Definition float_arg (va: bool) (ri rf ofs: Z) (ty: typ)
One (R r) :: rec ri' (rf + 1) ofs
else
(* we are out of integer registers, pass argument on stack *)
- let ofs := align ofs (typealign ty) in
+ let ofs := align ofs (typesize ty) in
One(S Outgoing ofs ty)
:: rec ri' rf (ofs + (if Archi.ptr64 then 2 else typesize ty)))
else
One (R r) :: rec ri (rf + 1) ofs
| None =>
- let ofs := align ofs (typealign ty) in
+ let ofs := align ofs (typesize ty) in
One(S Outgoing ofs ty)
:: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty))
end.
@@ -306,10 +306,13 @@ Proof.
{ decide_goal. }
assert (CSF: forall r, In r float_param_regs -> is_callee_save r = false).
{ decide_goal. }
- assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typealign ty) >= 0).
+ assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typesize ty) >= 0).
{ intros.
- assert (ofs <= align ofs (typealign ty)) by (apply align_le; apply typealign_pos).
+ assert (ofs <= align ofs (typesize ty)) by (apply align_le; apply typesize_pos).
omega. }
+ assert (ALD: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs (typesize ty))).
+ { intros. eapply Z.divide_trans. apply typealign_typesize.
+ apply align_divides. apply typesize_pos. }
assert (SK: (if Archi.ptr64 then 2 else 1) > 0).
{ destruct Archi.ptr64; omega. }
assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0).
@@ -332,12 +335,12 @@ Proof.
destruct va; [destruct (zle ri' 8)|idtac]; destruct H.
+ subst p; simpl. apply CSF. eapply list_nth_z_in; eauto.
+ eapply OF; eauto.
- + subst p; repeat split; auto using align_divides, typealign_pos.
+ + subst p; repeat split; auto.
+ eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega.
+ subst p; simpl. apply CSF. eapply list_nth_z_in; eauto.
+ eapply OF; eauto.
- destruct H.
- + subst p; repeat split; auto using align_divides, typealign_pos.
+ + subst p; repeat split; auto.
+ eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega.
}
assert (C: forall va ri rf ofs f,
diff --git a/riscV/DuplicateOpcodeHeuristic.ml b/riscV/DuplicateOpcodeHeuristic.ml
index 85505245..2ec314c1 100644
--- a/riscV/DuplicateOpcodeHeuristic.ml
+++ b/riscV/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,27 @@
-exception HeuristicSucceeded
-
-let opcode_heuristic code cond ifso ifnot preferred = ()
+(* open Camlcoq *)
+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
+ | Ccomplimm (c, n) | Ccompluimm (c, n) -> if n == Integers.Int64.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/runtime/include/math.h b/runtime/include/math.h
index d6475df1..01b8d8d8 100644
--- a/runtime/include/math.h
+++ b/runtime/include/math.h
@@ -1,6 +1,8 @@
#ifndef _COMPCERT_MATH_H
#define _COMPCERT_MATH_H
+#ifdef __K1C__
+
#define isfinite(__y) (fpclassify((__y)) >= FP_ZERO)
#include_next <math.h>
@@ -16,4 +18,9 @@
#define fmaf(x, y, z) __builtin_fmaf((x),(y),(z))
#endif
+#else
+
+#include_next <math.h>
+
+#endif
#endif
diff --git a/test/Makefile b/test/Makefile
index 7efcd8f1..e9c5d6a1 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -4,7 +4,9 @@ include ../Makefile.config
# Kalray note - removing compression, raytracer and spass that cannot be executed by the simulator in reasonable time
ifeq ($(ARCH),mppa_k1c)
- DIRS:=c regression
+ DIRS=c regression
+else
+ DIRS=c compression raytracer spass regression
endif
ifeq ($(CLIGHTGEN),true)
diff --git a/test/c/mandelbrot.c b/test/c/mandelbrot.c
index fb8b929c..548c3ffa 100644
--- a/test/c/mandelbrot.c
+++ b/test/c/mandelbrot.c
@@ -59,7 +59,6 @@ int main (int argc, char **argv)
if(bit_num == 8)
{
- printf("%c", byte_acc);
putc(byte_acc,stdout);
#ifdef __K1C__ // stdout isn't flushed enough when --syscall=libstd_scalls.so is passed to the simulator k1-cluster
fflush(stdout);
@@ -70,7 +69,6 @@ int main (int argc, char **argv)
else if(x == w-1)
{
byte_acc <<= (8-w%8);
- printf("%c", byte_acc);
putc(byte_acc,stdout);
#ifdef __K1C__ // stdout isn't flushed enough when --syscall=libstd_scalls.so is passed to the simulator k1-cluster
fflush(stdout);
diff --git a/test/monniaux/yarpgen/Makefile b/test/monniaux/yarpgen/Makefile
index 9da82deb..28bd5ae0 100644
--- a/test/monniaux/yarpgen/Makefile
+++ b/test/monniaux/yarpgen/Makefile
@@ -1,52 +1,98 @@
-YARPGEN=yarpgen
-MAX=300
+TARGET_CCOMP=../../../ccomp
+TARGET_CC=gcc
+
+all:
+
+.SECONDARY:
+
+ifndef YARPGEN
+YARPGEN=./yarpgen
+GENERATOR=yarpgen
+endif
+
+ifdef BITS
+YARPGEN+=-m $(BITS)
+CFLAGS+=-m$(BITS)
+endif
+
+MAX=129
PREFIX=ran%06.f
-include ../rules.mk
-
-K1C_CCOMPFLAGS += -funprototyped -fbitfields
-CCOMPFLAGS += -funprototyped -fbitfields
-
-TARGETS_C=$(shell seq --format $(PREFIX)/func.c 0 $(MAX)) \
- $(shell seq --format $(PREFIX)/driver.c 0 $(MAX)) \
- $(shell seq --format $(PREFIX)/init.h 0 $(MAX))
-TARGETS_CCOMP_K1C_S=$(shell seq --format $(PREFIX)/func.ccomp.k1c.s 0 $(MAX)) \
- $(shell seq --format $(PREFIX)/driver.ccomp.k1c.s 0 $(MAX))
-TARGETS_GCC_K1C_S=$(shell seq --format $(PREFIX)/func.gcc.k1c.s 0 $(MAX)) \
- $(shell seq --format $(PREFIX)/driver.gcc.k1c.s 0 $(MAX))
-TARGETS_CCOMP_HOST_S=$(shell seq --format $(PREFIX)/func.ccomp.host.s 0 $(MAX)) \
- $(shell seq --format $(PREFIX)/driver.ccomp.host.s 0 $(MAX))
-TARGETS_GCC_HOST_S=$(shell seq --format $(PREFIX)/func.gcc.host.s 0 $(MAX)) \
- $(shell seq --format $(PREFIX)/driver.gcc.host.s 0 $(MAX))
-TARGETS_CCOMP_K1C_OUT=$(shell seq --format $(PREFIX)/example.ccomp.k1c.out 0 $(MAX))
-TARGETS_GCC_K1C_OUT=$(shell seq --format $(PREFIX)/example.gcc.k1c.out 0 $(MAX))
-TARGETS_GCC_HOST_OUT=$(shell seq --format $(PREFIX)/example.gcc.host.out 0 $(MAX))
-TARGETS_CCOMP_HOST_OUT=$(shell seq --format $(PREFIX)/example.ccomp.host.out 0 $(MAX))
-TARGETS_CMP=$(shell seq --format $(PREFIX)/example.k1c.cmp 0 $(MAX))
-
-all: $(TARGETS_CCOMP_K1C_OUT) $(TARGETS_GCC_K1C_OUT) $(TARGETS_GCC_HOST_OUT) $(TARGETS_CCOMP_HOST_OUT) $(TARGETS_CCOMP_K1C_S) $(TARGETS_GCC_K1C_S) $(TARGETS_GCC_HOST_S) $(TARGETS_CCOMP_HOST_S) $(TARGETS_CMP) $(TARGETS_C)
-
-ran%/func.ccomp.k1c.s ran%/func.gcc.k1c.s ran%/func.ccomp.host.s ran%/func.gcc.host.s : ran%/init.h
-
-ran%/example.ccomp.k1c: ran%/func.ccomp.k1c.o ran%/driver.ccomp.k1c.o
- $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
-
-ran%/example.gcc.k1c: ran%/func.gcc.k1c.o ran%/driver.gcc.k1c.o
- $(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-ran%/example.gcc.host: ran%/func.gcc.host.o ran%/driver.gcc.host.o
- $(CC) $(CFLAGS) $+ -o $@
-ran%/example.ccomp.host: ran%/func.ccomp.host.o ran%/driver.ccomp.host.o
- $(CCOMP) $(CCOMPFLAGS) $+ -o $@
+CCOMPOPTS=-static
+CCOMPFLAGS+=-funprototyped -fbitfields -fno-cse2 -stdlib ../../../runtime # FIXME
+
+TESTS_C=$(shell seq --format $(PREFIX)/func.c 1 $(MAX)) \
+ $(shell seq --format $(PREFIX)/driver.c 1 $(MAX)) \
+ $(shell seq --format $(PREFIX)/init.c 1 $(MAX)) \
+ $(shell seq --format $(PREFIX)/hash.c 1 $(MAX)) \
+ $(shell seq --format $(PREFIX)/check.c 1 $(MAX)) \
+ $(shell seq --format $(PREFIX)/init.h 1 $(MAX))
+
+$(TESTS_C): $(GENERATOR)
+
+TESTS_CCOMP_TARGET_S=$(TEST_C:.c=.ccomp.target.s)
+TESTS_GCC_TARGET_S=$(TEST_C:.c=.gcc.target.s)
+TESTS_GCC_HOST_S=$(TEST_C:.c=.gcc.host.s)
+TESTS_CCOMP_TARGET_OUT=$(shell seq --format $(PREFIX)/example.ccomp.target.out 1 $(MAX))
+TESTS_GCC_TARGET_OUT=$(shell seq --format $(PREFIX)/example.gcc.target.out 1 $(MAX))
+TESTS_GCC_HOST_OUT=$(shell seq --format $(PREFIX)/example.gcc.host.out 1 $(MAX))
+TESTS_CMP=$(shell seq --format $(PREFIX)/example.target.cmp 1 $(MAX)) # $(shell seq --format $(PREFIX)/example.host_target.cmp 1 $(MAX))
+
+all: $(TESTS_CCOMP_TARGET_OUT) $(TESTS_GCC_TARGET_OUT) $(TESTS_CCOMP_TARGET_S) $(TESTS_GCC_TARGET_S) $(TESTS_CMP) $(TESTS_C)
+
+tests_c: $(TESTS_C)
+
+tests_s: $(TESTS_CCOMP_TARGET_S)
+
+%.ccomp.target.s : %.c
+ $(TARGET_CCOMP) $(CCOMPOPTS) $(CCOMPFLAGS) -S -o $@ $<
+
+%.gcc.target.s : %.c
+ $(TARGET_CC) $(CCOMPOPTS) -S -o $@ $<
-ran%/driver.c ran%/func.c ran%/init.h:
- -mkdir ran$*
+%.gcc.host.s : %.c
+ $(CC) $(CFLAGS) -S -o $@ $<
+
+%.target.o : %.target.s
+ $(TARGET_CC) -c -o $@ $<
+
+%.host.o : %.host.s
+ $(CC) $(CFLAGS) -c -o $@ $<
+
+%.target.out : %.target
+ $(EXECUTE) $< | tee $@
+
+%.host.out : %.host
+ ./$< | tee $@
+
+ran%/func.ccomp.target.s ran%/func.gcc.target.s ran%/func.ccomp.host.s ran%/func.gcc.host.s ran%/init.gcc.host.s : ran%/init.h
+
+ran%/example.ccomp.target: ran%/func.ccomp.target.o ran%/driver.ccomp.target.o ran%/init.ccomp.target.o ran%/check.ccomp.target.o ran%/hash.ccomp.target.o
+ $(TARGET_CCOMP) $(CCOMPOPTS) $(CCOMPFLAGS) $+ -o $@
+
+ran%/example.gcc.target: ran%/func.gcc.target.o ran%/driver.gcc.target.o ran%/init.gcc.target.o ran%/check.gcc.target.o ran%/hash.gcc.target.o
+ $(TARGET_CC) $(TARGET_CFLAGS) $+ -o $@
+
+ran%/example.gcc.host: ran%/func.gcc.host.o ran%/driver.gcc.host.o ran%/init.gcc.host.o ran%/check.gcc.host.o ran%/hash.gcc.host.o
+ $(CC) $(CFLAGS) $+ -o $@
+
+ran%/driver.c ran%/func.c ran%/init.c ran%/check.c ran%/hash.c ran%/init.h:
+ mkdir -p ran$*
$(YARPGEN) --seed=$* --out-dir=ran$*/ --std=c99
-ran%/example.k1c.cmp : ran%/example.gcc.k1c.out ran%/example.ccomp.k1c.out
+ran%/example.target.cmp : ran%/example.gcc.target.out ran%/example.ccomp.target.out
cmp $+ > $@
-.PHONY: all clean
+ran%/example.host_target.cmp : ran%/example.gcc.host.out ran%/example.ccomp.target.out
+ cmp $+ > $@
+
+yarpgen:
+ curl -L -o yarpgen_v1.1.tar.gz https://github.com/intel/yarpgen/archive/v1.1.tar.gz
+ tar xfz yarpgen_v1.1.tar.gz
+ $(MAKE) CXX=g++ -C yarpgen-1.1
+ cp yarpgen-1.1/yarpgen $@
+
+.PHONY: all clean tests_c tests_c
clean:
-rm -rf ran*
diff --git a/test/monniaux/yarpgen/Makefile.old b/test/monniaux/yarpgen/Makefile.old
new file mode 100644
index 00000000..9da82deb
--- /dev/null
+++ b/test/monniaux/yarpgen/Makefile.old
@@ -0,0 +1,52 @@
+YARPGEN=yarpgen
+MAX=300
+PREFIX=ran%06.f
+include ../rules.mk
+
+K1C_CCOMPFLAGS += -funprototyped -fbitfields
+CCOMPFLAGS += -funprototyped -fbitfields
+
+TARGETS_C=$(shell seq --format $(PREFIX)/func.c 0 $(MAX)) \
+ $(shell seq --format $(PREFIX)/driver.c 0 $(MAX)) \
+ $(shell seq --format $(PREFIX)/init.h 0 $(MAX))
+TARGETS_CCOMP_K1C_S=$(shell seq --format $(PREFIX)/func.ccomp.k1c.s 0 $(MAX)) \
+ $(shell seq --format $(PREFIX)/driver.ccomp.k1c.s 0 $(MAX))
+TARGETS_GCC_K1C_S=$(shell seq --format $(PREFIX)/func.gcc.k1c.s 0 $(MAX)) \
+ $(shell seq --format $(PREFIX)/driver.gcc.k1c.s 0 $(MAX))
+TARGETS_CCOMP_HOST_S=$(shell seq --format $(PREFIX)/func.ccomp.host.s 0 $(MAX)) \
+ $(shell seq --format $(PREFIX)/driver.ccomp.host.s 0 $(MAX))
+TARGETS_GCC_HOST_S=$(shell seq --format $(PREFIX)/func.gcc.host.s 0 $(MAX)) \
+ $(shell seq --format $(PREFIX)/driver.gcc.host.s 0 $(MAX))
+TARGETS_CCOMP_K1C_OUT=$(shell seq --format $(PREFIX)/example.ccomp.k1c.out 0 $(MAX))
+TARGETS_GCC_K1C_OUT=$(shell seq --format $(PREFIX)/example.gcc.k1c.out 0 $(MAX))
+TARGETS_GCC_HOST_OUT=$(shell seq --format $(PREFIX)/example.gcc.host.out 0 $(MAX))
+TARGETS_CCOMP_HOST_OUT=$(shell seq --format $(PREFIX)/example.ccomp.host.out 0 $(MAX))
+TARGETS_CMP=$(shell seq --format $(PREFIX)/example.k1c.cmp 0 $(MAX))
+
+all: $(TARGETS_CCOMP_K1C_OUT) $(TARGETS_GCC_K1C_OUT) $(TARGETS_GCC_HOST_OUT) $(TARGETS_CCOMP_HOST_OUT) $(TARGETS_CCOMP_K1C_S) $(TARGETS_GCC_K1C_S) $(TARGETS_GCC_HOST_S) $(TARGETS_CCOMP_HOST_S) $(TARGETS_CMP) $(TARGETS_C)
+
+ran%/func.ccomp.k1c.s ran%/func.gcc.k1c.s ran%/func.ccomp.host.s ran%/func.gcc.host.s : ran%/init.h
+
+ran%/example.ccomp.k1c: ran%/func.ccomp.k1c.o ran%/driver.ccomp.k1c.o
+ $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
+
+ran%/example.gcc.k1c: ran%/func.gcc.k1c.o ran%/driver.gcc.k1c.o
+ $(K1C_CC) $(K1C_CFLAGS) $+ -o $@
+
+ran%/example.gcc.host: ran%/func.gcc.host.o ran%/driver.gcc.host.o
+ $(CC) $(CFLAGS) $+ -o $@
+
+ran%/example.ccomp.host: ran%/func.ccomp.host.o ran%/driver.ccomp.host.o
+ $(CCOMP) $(CCOMPFLAGS) $+ -o $@
+
+ran%/driver.c ran%/func.c ran%/init.h:
+ -mkdir ran$*
+ $(YARPGEN) --seed=$* --out-dir=ran$*/ --std=c99
+
+ran%/example.k1c.cmp : ran%/example.gcc.k1c.out ran%/example.ccomp.k1c.out
+ cmp $+ > $@
+
+.PHONY: all clean
+
+clean:
+ -rm -rf ran*
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 3447d6a5..ad3ffd99 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -26,18 +26,18 @@ TESTS_COMP?=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \
varargs1 varargs2 varargs3 sections alias aligned\
packedstruct1 packedstruct2
-ifeq ($(ARCH),mppa_k1c)
+# FIXME ifeq ($(ARCH),mppa_k1c)
TESTS_COMP:=$(filter-out packedstruct1,$(TESTS_COMP))
TESTS_COMP:=$(filter-out packedstruct2,$(TESTS_COMP))
-endif
+# endif
# Can run, both in compiled mode and in interpreter mode,
# but produce processor-dependent results, so no reference output in Results
TESTS_DIFF=NaNs
-ifeq ($(ARCH),mppa_k1c)
+# FIXME ifeq ($(ARCH),mppa_k1c)
TESTS_DIFF:=$(filter-out NaNs,$(TESTS_DIFF))
-endif
+# endif endif
# Other tests: should compile to .s without errors (but expect warnings)
diff --git a/x86/DuplicateOpcodeHeuristic.ml b/x86/DuplicateOpcodeHeuristic.ml
index 85505245..2ec314c1 100644
--- a/x86/DuplicateOpcodeHeuristic.ml
+++ b/x86/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,27 @@
-exception HeuristicSucceeded
-
-let opcode_heuristic code cond ifso ifnot preferred = ()
+(* open Camlcoq *)
+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
+ | Ccomplimm (c, n) | Ccompluimm (c, n) -> if n == Integers.Int64.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