diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 19:09:30 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 19:09:30 +0200 |
commit | 6ec981b26bd3f3d6c379ec48fd6ac6931a86bff5 (patch) | |
tree | cee523d3139c4b94a273a61b9bfbb5bfcb660c6d | |
parent | 731c230f1c583b9e20e86e2b7fc43a1f6c8520ea (diff) | |
parent | aa4dcf296521ebe5be4aee5ee29aa678b8325c46 (diff) | |
download | compcert-kvx-6ec981b26bd3f3d6c379ec48fd6ac6931a86bff5.tar.gz compcert-kvx-6ec981b26bd3f3d6c379ec48fd6ac6931a86bff5.zip |
Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2
-rw-r--r-- | .gitlab-ci.yml | 221 | ||||
-rw-r--r-- | aarch64/Asmgen.v | 9 | ||||
-rw-r--r-- | aarch64/Asmgenproof.v | 141 | ||||
-rw-r--r-- | aarch64/Asmgenproof1.v | 656 | ||||
-rw-r--r-- | aarch64/DuplicateOpcodeHeuristic.ml | 30 | ||||
-rw-r--r-- | arm/DuplicateOpcodeHeuristic.ml | 25 | ||||
-rw-r--r-- | backend/Duplicateaux.ml | 18 | ||||
-rw-r--r-- | backend/Inliningaux.ml | 9 | ||||
-rwxr-xr-x | config_arm.sh | 2 | ||||
-rwxr-xr-x | config_armhf.sh | 1 | ||||
-rwxr-xr-x | config_ppc64.sh | 1 | ||||
-rwxr-xr-x | config_rv32.sh | 2 | ||||
-rwxr-xr-x | config_rv64.sh | 2 | ||||
-rwxr-xr-x | config_simple.sh | 7 | ||||
-rw-r--r-- | cparser/Elab.ml | 4 | ||||
-rw-r--r-- | driver/Clflags.ml | 3 | ||||
-rw-r--r-- | driver/Driver.ml | 8 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 125 | ||||
-rw-r--r-- | powerpc/DuplicateOpcodeHeuristic.ml | 30 | ||||
-rw-r--r-- | riscV/Conventions1.v | 17 | ||||
-rw-r--r-- | riscV/DuplicateOpcodeHeuristic.ml | 30 | ||||
-rw-r--r-- | runtime/include/math.h | 7 | ||||
-rw-r--r-- | test/Makefile | 4 | ||||
-rw-r--r-- | test/c/mandelbrot.c | 2 | ||||
-rw-r--r-- | test/monniaux/yarpgen/Makefile | 130 | ||||
-rw-r--r-- | test/monniaux/yarpgen/Makefile.old | 52 | ||||
-rw-r--r-- | test/regression/Makefile | 8 | ||||
-rw-r--r-- | x86/DuplicateOpcodeHeuristic.ml | 30 |
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 |