diff options
-rw-r--r-- | .gitlab-ci.yml | 2 | ||||
-rw-r--r-- | aarch64/CSE2deps.v | 5 | ||||
-rw-r--r-- | aarch64/CSE2depsproof.v | 75 | ||||
-rw-r--r-- | aarch64/Op.v | 14 | ||||
-rw-r--r-- | arm/CSE2deps.v | 5 | ||||
-rw-r--r-- | arm/CSE2depsproof.v | 74 | ||||
-rw-r--r-- | arm/Op.v | 14 | ||||
-rw-r--r-- | backend/CSE3analysis.v | 22 | ||||
-rw-r--r-- | backend/CSE3analysisaux.ml | 4 | ||||
-rw-r--r-- | backend/CSE3analysisproof.v | 143 | ||||
-rw-r--r-- | backend/Tunnelingaux.ml | 4 | ||||
-rw-r--r-- | common/Values.v | 21 | ||||
-rw-r--r-- | kvx/CSE2deps.v | 5 | ||||
-rw-r--r-- | kvx/CSE2depsproof.v | 29 | ||||
-rw-r--r-- | kvx/Op.v | 20 | ||||
-rw-r--r-- | powerpc/CSE2deps.v | 5 | ||||
-rw-r--r-- | powerpc/CSE2depsproof.v | 71 | ||||
-rw-r--r-- | powerpc/Op.v | 14 | ||||
-rw-r--r-- | riscV/CSE2deps.v | 5 | ||||
-rw-r--r-- | riscV/CSE2depsproof.v | 12 | ||||
-rw-r--r-- | riscV/Op.v | 10 | ||||
-rw-r--r-- | x86/CSE2deps.v | 2 | ||||
-rw-r--r-- | x86/CSE2depsproof.v | 82 | ||||
-rw-r--r-- | x86/Op.v | 14 |
24 files changed, 612 insertions, 40 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 10008017..c503c394 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -227,7 +227,7 @@ build_kvx: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install sshpass openssh-client libzip4 lttng-tools liblttng-ctl-dev liblttng-ust-dev babeltrace - ./.download_from_Kalray.sh - - rm -f download/*dkms*.deb download/*eclipse*.deb download/*llvm*.deb download/*board-mgmt* download/*oce-host* download/*pocl* + - rm -f download/*dkms*.deb download/*eclipse*.deb download/*llvm*.deb download/*board-mgmt* download/*oce-host* download/*pocl* download/*flash-util* download/*barebox* - sudo dpkg -i download/*.deb - rm -rf download - eval `opam config env` diff --git a/aarch64/CSE2deps.v b/aarch64/CSE2deps.v index a23e41a8..d5c7ee0f 100644 --- a/aarch64/CSE2deps.v +++ b/aarch64/CSE2deps.v @@ -28,5 +28,8 @@ Definition may_overlap chunk addr args chunk' addr' args' := (base :: nil), (base' :: nil) => if peq base base' then negb (can_swap_accesses_ofs (Int64.unsigned ofs') chunk' (Int64.unsigned ofs) chunk) - else true | _, _, _, _ => true + else true + | (Ainstack ofs), (Ainstack ofs'), _, _ => + negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) + | _, _, _, _ => true end. diff --git a/aarch64/CSE2depsproof.v b/aarch64/CSE2depsproof.v index dbd46142..653c88f4 100644 --- a/aarch64/CSE2depsproof.v +++ b/aarch64/CSE2depsproof.v @@ -104,9 +104,71 @@ Section MEMORY_WRITE. Qed. End INDEXED_AWAY. End MEMORY_WRITE. -End SOUNDNESS. +Section STACK_WRITE. + Variable m m2 : mem. + Variable chunkw chunkr : memory_chunk. + + Variable addrw addrr valw : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + + Section INDEXED_AWAY. + Variable ofsw ofsr : ptrofs. + Hypothesis ADDRW : eval_addressing genv sp + (Ainstack ofsw) nil = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Ainstack ofsr) nil = Some addrr. + + Lemma stack_load_store_away1 : + forall RANGEW : 0 <= Ptrofs.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= Ptrofs.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : Ptrofs.unsigned ofsw + size_chunk chunkw <= Ptrofs.unsigned ofsr + \/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw, + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intros. + + pose proof (max_size_chunk chunkr) as size_chunkr_bounded. + pose proof (max_size_chunk chunkw) as size_chunkw_bounded. + unfold largest_size_chunk in *. + + rewrite ptrofs_modulus in *. + simpl in *. + inv ADDRR. + inv ADDRW. + + destruct sp; try discriminate. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + + all: try (destruct (Ptrofs.unsigned_add_either i ofsr) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i ofsw) as [OFSW | OFSW]; + rewrite OFSW). + + all: try rewrite ptrofs_modulus in *. + + all: intuition lia. + Qed. + + Theorem stack_load_store_away : + can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true -> + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intro SWAP. + unfold can_swap_accesses_ofs in SWAP. + repeat rewrite andb_true_iff in SWAP. + repeat rewrite orb_true_iff in SWAP. + repeat rewrite Z.leb_le in SWAP. + apply stack_load_store_away1. + all: tauto. + Qed. + End INDEXED_AWAY. +End STACK_WRITE. +End SOUNDNESS. + Section SOUNDNESS. Variable F V : Type. Variable genv: Genv.t F V. @@ -124,7 +186,7 @@ Proof. intros until rs. intros ADDR ADDR' OVERLAP STORE. destruct addr; destruct addr'; try discriminate. - { (* Aindexed / Aindexed *) + - (* Aindexed / Aindexed *) destruct args as [ | base [ | ]]. 1,3: discriminate. destruct args' as [ | base' [ | ]]. 1,3: discriminate. simpl in OVERLAP. @@ -134,7 +196,14 @@ Proof. 2: discriminate. simpl in *. eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. - } +- (* Ainstack / Ainstack *) + destruct args. 2: discriminate. + destruct args'. 2: discriminate. + cbn in OVERLAP. + destruct (can_swap_accesses_ofs (Ptrofs.unsigned ofs0) chunk' (Ptrofs.unsigned ofs) chunk) eqn:SWAP. + 2: discriminate. + cbn in *. + eapply stack_load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. Qed. End SOUNDNESS. diff --git a/aarch64/Op.v b/aarch64/Op.v index afc25aa6..f720e545 100644 --- a/aarch64/Op.v +++ b/aarch64/Op.v @@ -1209,6 +1209,20 @@ Proof. rewrite (cond_depends_on_memory_correct cond args m1 m2 H). auto. Qed. +Lemma op_valid_pointer_eq: + forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, + (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> + eval_operation ge sp op args m1 = eval_operation ge sp op args m2. +Proof. + intros until m2. destruct op eqn:OP; simpl; try congruence. + - intros MEM; destruct cond; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + - intro MEM; destruct cond; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. +Qed. + (** Global variables mentioned in an operation or addressing mode *) Definition globals_addressing (addr: addressing) : list ident := diff --git a/arm/CSE2deps.v b/arm/CSE2deps.v index d48dabf3..4592f408 100644 --- a/arm/CSE2deps.v +++ b/arm/CSE2deps.v @@ -28,5 +28,8 @@ Definition may_overlap chunk addr args chunk' addr' args' := (base :: nil), (base' :: nil) => if peq base base' then negb (can_swap_accesses_ofs (Int.unsigned ofs') chunk' (Int.unsigned ofs) chunk) - else true | _, _, _, _ => true + else true + | (Ainstack ofs), (Ainstack ofs'), _, _ => + negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) + | _, _, _, _ => true end. diff --git a/arm/CSE2depsproof.v b/arm/CSE2depsproof.v index 28ef41ca..7dd0914e 100644 --- a/arm/CSE2depsproof.v +++ b/arm/CSE2depsproof.v @@ -105,6 +105,68 @@ Section MEMORY_WRITE. Qed. End INDEXED_AWAY. End MEMORY_WRITE. + +Section STACK_WRITE. + Variable m m2 : mem. + Variable chunkw chunkr : memory_chunk. + + Variable addrw addrr valw : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + + Section INDEXED_AWAY. + Variable ofsw ofsr : ptrofs. + Hypothesis ADDRW : eval_addressing genv sp + (Ainstack ofsw) nil = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Ainstack ofsr) nil = Some addrr. + + Lemma stack_load_store_away1 : + forall RANGEW : 0 <= Ptrofs.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= Ptrofs.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : Ptrofs.unsigned ofsw + size_chunk chunkw <= Ptrofs.unsigned ofsr + \/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw, + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intros. + + pose proof (max_size_chunk chunkr) as size_chunkr_bounded. + pose proof (max_size_chunk chunkw) as size_chunkw_bounded. + unfold largest_size_chunk in *. + + rewrite ptrofs_modulus in *. + simpl in *. + inv ADDRR. + inv ADDRW. + + destruct sp; try discriminate. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + + all: try (destruct (Ptrofs.unsigned_add_either i ofsr) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i ofsw) as [OFSW | OFSW]; + rewrite OFSW). + + all: try rewrite ptrofs_modulus in *. + + all: intuition lia. + Qed. + + Theorem stack_load_store_away : + can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true -> + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intro SWAP. + unfold can_swap_accesses_ofs in SWAP. + repeat rewrite andb_true_iff in SWAP. + repeat rewrite orb_true_iff in SWAP. + repeat rewrite Z.leb_le in SWAP. + apply stack_load_store_away1. + all: tauto. + Qed. + End INDEXED_AWAY. +End STACK_WRITE. End SOUNDNESS. @@ -125,7 +187,7 @@ Proof. intros until rs. intros ADDR ADDR' OVERLAP STORE. destruct addr; destruct addr'; try discriminate. - { (* Aindexed / Aindexed *) +- (* Aindexed / Aindexed *) destruct args as [ | base [ | ]]. 1,3: discriminate. destruct args' as [ | base' [ | ]]. 1,3: discriminate. simpl in OVERLAP. @@ -135,7 +197,15 @@ Proof. 2: discriminate. simpl in *. eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. - } + +- (* Ainstack / Ainstack *) + destruct args. 2: discriminate. + destruct args'. 2: discriminate. + cbn in OVERLAP. + destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP. + 2: discriminate. + cbn in *. + eapply stack_load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. Qed. End SOUNDNESS. @@ -751,6 +751,20 @@ Proof. auto. Qed. +Lemma op_valid_pointer_eq: + forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, + (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> + eval_operation ge sp op args m1 = eval_operation ge sp op args m2. +Proof. + intros until m2. destruct op eqn:OP; simpl; try congruence. + - intros MEM; destruct c; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + - intro MEM; destruct c; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. +Qed. + (** Global variables mentioned in an operation or addressing mode *) Definition globals_operation (op: operation) : list ident := diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 5ed04bc4..8b7f1190 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -181,12 +181,24 @@ Definition eq_depends_on_mem eq := | SOp op => op_depends_on_memory op end. +Definition eq_depends_on_store eq := + match eq_op eq with + | SLoad _ _ => true + | SOp op => false + end. + Definition get_mem_kills (eqs : PTree.t equation) : PSet.t := PTree.fold (fun already (eqno : eq_id) (eq : equation) => if eq_depends_on_mem eq then PSet.add eqno already else already) eqs PSet.empty. +Definition get_store_kills (eqs : PTree.t equation) : PSet.t := + PTree.fold (fun already (eqno : eq_id) (eq : equation) => + if eq_depends_on_store eq + then PSet.add eqno already + else already) eqs PSet.empty. + Definition is_move (op : operation) : { op = Omove } + { op <> Omove }. Proof. @@ -216,6 +228,7 @@ Record eq_context := mkeqcontext eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t; eq_kill_reg : reg -> PSet.t; eq_kill_mem : unit -> PSet.t; + eq_kill_store : unit -> PSet.t; eq_moves : reg -> PSet.t }. Section OPERATIONS. @@ -342,6 +355,9 @@ Section OPERATIONS. (oper1 dst op args' rel) end. + Definition kill_store (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kill_store ctx tt). + Definition clever_kill_store (chunk : memory_chunk) (addr: addressing) (args : list reg) (src : reg) @@ -358,7 +374,7 @@ Section OPERATIONS. may_overlap chunk addr args chunk' addr' (eq_args eq) end end) - (PSet.inter rel (eq_kill_mem ctx tt))). + (PSet.inter rel (eq_kill_store ctx tt))). Definition store2 (chunk : memory_chunk) (addr: addressing) (args : list reg) @@ -366,7 +382,7 @@ Section OPERATIONS. (rel : RELATION.t) : RELATION.t := if Compopts.optim_CSE3_alias_analysis tt then clever_kill_store chunk addr args src rel - else kill_mem rel. + else kill_store rel. Definition store1 (chunk : memory_chunk) (addr: addressing) (args : list reg) @@ -501,6 +517,7 @@ Definition context_from_hints (hints : analysis_hints) := let eqs := hint_eq_catalog hints in let reg_kills := get_reg_kills eqs in let mem_kills := get_mem_kills eqs in + let store_kills := get_store_kills eqs in let moves := get_moves eqs in {| eq_catalog := fun eq_id => PTree.get eq_id eqs; @@ -508,5 +525,6 @@ Definition context_from_hints (hints : analysis_hints) := eq_rhs_oracle := hint_eq_rhs_oracle hints; eq_kill_reg := fun reg => PMap.get reg reg_kills; eq_kill_mem := fun _ => mem_kills; + eq_kill_store := fun _ => store_kills; eq_moves := fun reg => PMap.get reg moves |}. diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index e37ef61f..e038331c 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -174,6 +174,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = and rhs_table = Hashtbl.create 100 and cur_kill_reg = ref (PMap.init PSet.empty) and cur_kill_mem = ref PSet.empty + and cur_kill_store = ref PSet.empty and cur_moves = ref (PMap.init PSet.empty) in let eq_find_oracle node eq = assert (not (is_trivial eq)); @@ -216,6 +217,8 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = (eq.eq_lhs :: eq.eq_args); (if eq_depends_on_mem eq then cur_kill_mem := PSet.add coq_id !cur_kill_mem); + (if eq_depends_on_store eq + then cur_kill_store := PSet.add coq_id !cur_kill_store); (match eq.eq_op, eq.eq_args with | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves eq.eq_lhs coq_id | _, _ -> ()); @@ -232,6 +235,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = eq_rhs_oracle = rhs_find_oracle ; eq_kill_reg = (fun reg -> PMap.get reg !cur_kill_reg); eq_kill_mem = (fun () -> !cur_kill_mem); + eq_kill_store = (fun () -> !cur_kill_store); eq_moves = (fun reg -> PMap.get reg !cur_moves) } in match internal_analysis ctx tenv f diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 1e5b88c3..b298ea65 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -133,13 +133,18 @@ Definition xlget_kills (eqs : list (eq_id * equation)) (m : Regmap.t PSet.t) : add_i_j (eq_lhs (snd item)) (fst item) (add_ilist_j (eq_args (snd item)) (fst item) already)) eqs m. - Definition xlget_mem_kills (eqs : list (positive * equation)) (m : PSet.t) : PSet.t := (fold_left (fun (a : PSet.t) (p : positive * equation) => if eq_depends_on_mem (snd p) then PSet.add (fst p) a else a) eqs m). +Definition xlget_store_kills (eqs : list (positive * equation)) (m : PSet.t) : PSet.t := +(fold_left + (fun (a : PSet.t) (p : positive * equation) => + if eq_depends_on_store (snd p) then PSet.add (fst p) a else a) + eqs m). + Lemma xlget_kills_monotone : forall eqs m i j, PSet.contains (Regmap.get i m) j = true -> @@ -170,6 +175,24 @@ Qed. Hint Resolve xlget_mem_kills_monotone : cse3. +Lemma xlget_store_kills_monotone : + forall eqs m j, + PSet.contains m j = true -> + PSet.contains (xlget_store_kills eqs m) j = true. +Proof. + induction eqs; simpl; trivial. + intros. + destruct eq_depends_on_store. + - apply IHeqs. + destruct (peq (fst a) j). + + subst j. apply PSet.gadds. + + rewrite PSet.gaddo by congruence. + trivial. + - auto. +Qed. + +Hint Resolve xlget_store_kills_monotone : cse3. + Lemma xlget_kills_has_lhs : forall eqs m lhs sop args j, In (j, {| eq_lhs := lhs; @@ -333,6 +356,60 @@ Qed. Hint Resolve context_from_hints_get_kills_has_eq_depends_on_mem : cse3. +Lemma xlget_kills_has_eq_depends_on_store : + forall eqs eq j m, + In (j, eq) eqs -> + eq_depends_on_store eq = true -> + PSet.contains (xlget_store_kills eqs m) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros. + destruct H. + { subst a. + simpl. + rewrite H0. + apply xlget_store_kills_monotone. + apply PSet.gadds. + } + eauto. +Qed. + +Hint Resolve xlget_kills_has_eq_depends_on_store : cse3. + +Lemma get_kills_has_eq_depends_on_store : + forall eqs eq j, + PTree.get j eqs = Some eq -> + eq_depends_on_store eq = true -> + PSet.contains (get_store_kills eqs) j = true. +Proof. + intros. + unfold get_store_kills. + rewrite PTree.fold_spec. + change (fold_left + (fun (a : PSet.t) (p : positive * equation) => + if eq_depends_on_store (snd p) then PSet.add (fst p) a else a) + (PTree.elements eqs) PSet.empty) + with (xlget_store_kills (PTree.elements eqs) PSet.empty). + eapply xlget_kills_has_eq_depends_on_store. + apply PTree.elements_correct. + eassumption. + trivial. +Qed. + +Lemma context_from_hints_get_kills_has_eq_depends_on_store : + forall hints eq j, + PTree.get j (hint_eq_catalog hints) = Some eq -> + eq_depends_on_store eq = true -> + PSet.contains (eq_kill_store (context_from_hints hints) tt) j = true. +Proof. + intros. + simpl. + eapply get_kills_has_eq_depends_on_store; eassumption. +Qed. + +Hint Resolve context_from_hints_get_kills_has_eq_depends_on_store : cse3. + Definition eq_involves (eq : equation) (i : reg) := i = (eq_lhs eq) \/ In i (eq_args eq). @@ -418,6 +495,12 @@ Section SOUNDNESS. eq_depends_on_mem eq = true -> PSet.contains (eq_kill_mem ctx tt) j = true. + Hypothesis ctx_kill_store_has_depends_on_store : + forall eq j, + eq_catalog ctx j = Some eq -> + eq_depends_on_store eq = true -> + PSet.contains (eq_kill_store ctx tt) j = true. + Theorem kill_reg_sound : forall rel rs m dst v, (sem_rel rel rs m) -> @@ -574,6 +657,55 @@ Section SOUNDNESS. Hint Resolve kill_mem_sound : cse3. + (* TODO: shouldn't this already be proved somewhere else? *) + Lemma store_preserves_validity: + forall m m' wchunk a v + (STORE : Mem.storev wchunk m a v = Some m') + (b : block) (z : Z), + Mem.valid_pointer m' b z = Mem.valid_pointer m b z. + Proof. + unfold Mem.storev. + intros. + destruct a; try discriminate. + Local Transparent Mem.store. + unfold Mem.store in STORE. + destruct Mem.valid_access_dec in STORE. + 2: discriminate. + inv STORE. + reflexivity. + Qed. + + Hint Resolve store_preserves_validity : cse3. + + Theorem kill_store_sound : + forall rel rs m m' wchunk a v, + (sem_rel rel rs m) -> + (Mem.storev wchunk m a v = Some m') -> + (sem_rel (kill_store (ctx:=ctx) rel) rs m'). + Proof. + unfold sem_rel, sem_eq, sem_rhs, kill_store. + intros until v. + intros REL STORE i eq. + specialize REL with (i := i) (eq0 := eq). + intros SUBTRACT CATALOG. + rewrite PSet.gsubtract in SUBTRACT. + rewrite andb_true_iff in SUBTRACT. + intuition. + destruct (eq_op eq) as [op | chunk addr] eqn:OP. + - rewrite op_valid_pointer_eq with (m2 := m). + assumption. + eapply store_preserves_validity; eauto. + - specialize ctx_kill_store_has_depends_on_store with (eq0 := eq) (j := i). + destruct eq as [lhs op args]; simpl in *. + rewrite OP in ctx_kill_store_has_depends_on_store. + rewrite negb_true_iff in H0. + rewrite OP in CATALOG. + intuition. + congruence. + Qed. + + Hint Resolve kill_store_sound : cse3. + Theorem eq_find_sound: forall no eq id, eq_find (ctx := ctx) no eq = Some id -> @@ -895,13 +1027,12 @@ Section SOUNDNESS. unfold sem_eq in *. simpl in *. destruct eq_op as [op' | chunk' addr']; simpl. - - destruct (op_depends_on_memory op') eqn:DEPENDS. - + erewrite ctx_kill_mem_has_depends_on_mem in CONTAINS by eauto. - discriminate. - + rewrite op_depends_on_memory_correct with (m2:=m); trivial. + - rewrite op_valid_pointer_eq with (m2 := m). + + cbn in *. apply REL; auto. + + eapply store_preserves_validity; eauto. - simpl in REL. - erewrite ctx_kill_mem_has_depends_on_mem in CONTAINS by eauto. + erewrite ctx_kill_store_has_depends_on_store in CONTAINS by eauto. simpl in CONTAINS. rewrite negb_true_iff in CONTAINS. destruct (eval_addressing genv sp addr' rs ## eq_args) as [a'|] eqn:ADDR'. diff --git a/backend/Tunnelingaux.ml b/backend/Tunnelingaux.ml index af89adea..87e6d303 100644 --- a/backend/Tunnelingaux.ml +++ b/backend/Tunnelingaux.ml @@ -178,11 +178,11 @@ let final_export f c = ) else ( n.dist <- undef_dist; (* force [dist] to compute the actual [n.dist] *) count := !count+1; - (tn, n)::acc + n::acc ) in let nops = Hashtbl.fold filter_nops_init_dist c.nodes [] in - let res = List.fold_left (fun acc (tn,n) -> PTree.set (lab_p n) (lab_p tn, Z.of_uint (dist n)) acc) PTree.empty nops in + let res = List.fold_left (fun acc n -> PTree.set (lab_p n) (lab_p n.link, Z.of_uint (dist n)) acc) PTree.empty nops in debug "* Tunneling.branch_target: final number of eliminated nops = %d\n" !count; res diff --git a/common/Values.v b/common/Values.v index 6401ba52..41138e8e 100644 --- a/common/Values.v +++ b/common/Values.v @@ -2706,3 +2706,24 @@ Proof. unfold compose_meminj; rewrite H1; rewrite H3; eauto. rewrite Ptrofs.add_assoc. decEq. unfold Ptrofs.add. apply Ptrofs.eqm_samerepr. auto with ints. Qed. + + +(** Particular cases of extensionality lemma *) + +Lemma cmpu_bool_valid_pointer_eq vptr1 vptr2 c v1 v2: + (forall (b : block) (z : Z), vptr1 b z = vptr2 b z) -> + Val.cmpu_bool vptr1 c v1 v2 = Val.cmpu_bool vptr2 c v1 v2. +Proof. + intros EQ; unfold Val.cmpu_bool; destruct v1; try congruence; + destruct v2; try congruence; + rewrite !EQ; auto. +Qed. + +Lemma cmplu_bool_valid_pointer_eq vptr1 vptr2 c v1 v2: + (forall (b : block) (z : Z), vptr1 b z = vptr2 b z) -> + Val.cmplu_bool vptr1 c v1 v2 = Val.cmplu_bool vptr2 c v1 v2. +Proof. + intros EQ; unfold Val.cmplu_bool; destruct v1; try congruence; + destruct v2; try congruence; + rewrite !EQ; auto. +Qed. diff --git a/kvx/CSE2deps.v b/kvx/CSE2deps.v index b4b80e2f..c0deacf0 100644 --- a/kvx/CSE2deps.v +++ b/kvx/CSE2deps.v @@ -28,5 +28,8 @@ Definition may_overlap chunk addr args chunk' addr' args' := (base :: nil), (base' :: nil) => if peq base base' then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) - else true | _, _, _, _ => true + else true + | (Ainstack ofs), (Ainstack ofs'), _, _ => + negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) + | _, _, _, _ => true end. diff --git a/kvx/CSE2depsproof.v b/kvx/CSE2depsproof.v index 6c584450..a5f7b317 100644 --- a/kvx/CSE2depsproof.v +++ b/kvx/CSE2depsproof.v @@ -123,17 +123,24 @@ Proof. intros until rs. intros ADDR ADDR' OVERLAP STORE. destruct addr; destruct addr'; try discriminate. - { (* Aindexed / Aindexed *) - destruct args as [ | base [ | ]]. 1,3: discriminate. - destruct args' as [ | base' [ | ]]. 1,3: discriminate. - cbn in OVERLAP. - destruct (peq base base'). 2: discriminate. - subst base'. - destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP. - 2: discriminate. - cbn in *. - eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. - } + - (* Aindexed / Aindexed *) + destruct args as [ | base [ | ]]. 1,3: discriminate. + destruct args' as [ | base' [ | ]]. 1,3: discriminate. + cbn in OVERLAP. + destruct (peq base base'). 2: discriminate. + subst base'. + destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP. + 2: discriminate. + cbn in *. + eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. + - (* Ainstack / Ainstack *) + destruct args. 2: discriminate. + destruct args'. 2: discriminate. + cbn in OVERLAP. + destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP. + 2: discriminate. + cbn in *. + eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. Qed. End SOUNDNESS. @@ -1238,6 +1238,26 @@ Proof. unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. Qed. +Lemma op_valid_pointer_eq: + forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, + (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> + eval_operation ge sp op args m1 = eval_operation ge sp op args m2. +Proof. + intros until m2. destruct op; simpl; try congruence. + - intros MEM; destruct cond; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + - intros MEM; destruct c0; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + - intros MEM; destruct c0; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + - intros MEM; destruct c0; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. +Qed. + (** Global variables mentioned in an operation or addressing mode *) Definition globals_addressing (addr: addressing) : list ident := diff --git a/powerpc/CSE2deps.v b/powerpc/CSE2deps.v index d48dabf3..4592f408 100644 --- a/powerpc/CSE2deps.v +++ b/powerpc/CSE2deps.v @@ -28,5 +28,8 @@ Definition may_overlap chunk addr args chunk' addr' args' := (base :: nil), (base' :: nil) => if peq base base' then negb (can_swap_accesses_ofs (Int.unsigned ofs') chunk' (Int.unsigned ofs) chunk) - else true | _, _, _, _ => true + else true + | (Ainstack ofs), (Ainstack ofs'), _, _ => + negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) + | _, _, _, _ => true end. diff --git a/powerpc/CSE2depsproof.v b/powerpc/CSE2depsproof.v index 123341da..ede09dd6 100644 --- a/powerpc/CSE2depsproof.v +++ b/powerpc/CSE2depsproof.v @@ -111,6 +111,66 @@ Section MEMORY_WRITE. Qed. End INDEXED_AWAY. End MEMORY_WRITE. + +Section STACK_WRITE. + Variable m m2 : mem. + Variable chunkw chunkr : memory_chunk. + + Variable addrw addrr valw : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + + Section INDEXED_AWAY. + Variable ofsw ofsr : ptrofs. + Hypothesis ADDRW : eval_addressing genv sp + (Ainstack ofsw) nil = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Ainstack ofsr) nil = Some addrr. + + Lemma stack_load_store_away1 : + forall RANGEW : 0 <= Ptrofs.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= Ptrofs.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : Ptrofs.unsigned ofsw + size_chunk chunkw <= Ptrofs.unsigned ofsr + \/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw, + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intros. + + pose proof (max_size_chunk chunkr) as size_chunkr_bounded. + pose proof (max_size_chunk chunkw) as size_chunkw_bounded. + unfold largest_size_chunk in *. + + inv ADDRR. + inv ADDRW. + + destruct sp; try discriminate. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + + all: try (destruct (Ptrofs.unsigned_add_either i ofsr) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i ofsw) as [OFSW | OFSW]; + rewrite OFSW). + all: try rewrite ptrofs_modulus in *. + all: destruct Archi.ptr64. + + all: intuition lia. + Qed. + + Theorem stack_load_store_away : + can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true -> + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intro SWAP. + unfold can_swap_accesses_ofs in SWAP. + repeat rewrite andb_true_iff in SWAP. + repeat rewrite orb_true_iff in SWAP. + repeat rewrite Z.leb_le in SWAP. + apply stack_load_store_away1. + all: tauto. + Qed. + End INDEXED_AWAY. +End STACK_WRITE. End SOUNDNESS. @@ -131,7 +191,7 @@ Proof. intros until rs. intros ADDR ADDR' OVERLAP STORE. destruct addr; destruct addr'; try discriminate. - { (* Aindexed / Aindexed *) +- (* Aindexed / Aindexed *) destruct args as [ | base [ | ]]. 1,3: discriminate. destruct args' as [ | base' [ | ]]. 1,3: discriminate. simpl in OVERLAP. @@ -141,7 +201,14 @@ Proof. 2: discriminate. simpl in *. eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. - } +- (* Ainstack / Ainstack *) + destruct args. 2: discriminate. + destruct args'. 2: discriminate. + cbn in OVERLAP. + destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP. + 2: discriminate. + cbn in *. + eapply stack_load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. Qed. End SOUNDNESS. diff --git a/powerpc/Op.v b/powerpc/Op.v index a0ee5bb8..4f14bfac 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -797,6 +797,20 @@ Proof. auto. Qed. +Lemma op_valid_pointer_eq: + forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, + (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> + eval_operation ge sp op args m1 = eval_operation ge sp op args m2. +Proof. + intros until m2. destruct op eqn:OP; simpl; try congruence. + - intros MEM; destruct c; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + - intro MEM; destruct c; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. +Qed. + (** Global variables mentioned in an operation or addressing mode *) Definition globals_operation (op: operation) : list ident := diff --git a/riscV/CSE2deps.v b/riscV/CSE2deps.v index b4b80e2f..c0deacf0 100644 --- a/riscV/CSE2deps.v +++ b/riscV/CSE2deps.v @@ -28,5 +28,8 @@ Definition may_overlap chunk addr args chunk' addr' args' := (base :: nil), (base' :: nil) => if peq base base' then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) - else true | _, _, _, _ => true + else true + | (Ainstack ofs), (Ainstack ofs'), _, _ => + negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) + | _, _, _, _ => true end. diff --git a/riscV/CSE2depsproof.v b/riscV/CSE2depsproof.v index f283c8ac..cf9e62b1 100644 --- a/riscV/CSE2depsproof.v +++ b/riscV/CSE2depsproof.v @@ -123,7 +123,7 @@ Proof. intros until rs. intros ADDR ADDR' OVERLAP STORE. destruct addr; destruct addr'; try discriminate. - { (* Aindexed / Aindexed *) +- (* Aindexed / Aindexed *) destruct args as [ | base [ | ]]. 1,3: discriminate. destruct args' as [ | base' [ | ]]. 1,3: discriminate. simpl in OVERLAP. @@ -133,7 +133,15 @@ Proof. 2: discriminate. simpl in *. eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. - } + +- (* Ainstack / Ainstack *) + destruct args. 2: discriminate. + destruct args'. 2: discriminate. + cbn in OVERLAP. + destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP. + 2: discriminate. + cbn in *. + eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. Qed. End SOUNDNESS. @@ -872,6 +872,16 @@ Proof. unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. Qed. +Lemma op_valid_pointer_eq: + forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, + (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> + eval_operation ge sp op args m1 = eval_operation ge sp op args m2. +Proof. + intros until m2. destruct op; simpl; try congruence. + intros MEM; destruct cond; repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. +Qed. + (** Global variables mentioned in an operation or addressing mode *) Definition globals_addressing (addr: addressing) : list ident := diff --git a/x86/CSE2deps.v b/x86/CSE2deps.v index a4b47a5c..757966b8 100644 --- a/x86/CSE2deps.v +++ b/x86/CSE2deps.v @@ -32,5 +32,7 @@ Definition may_overlap chunk addr args chunk' addr' args' := if peq symb symb' then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) else false + | (Ainstack ofs), (Ainstack ofs'), _, _ => + negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) | _, _, _, _ => true end. diff --git a/x86/CSE2depsproof.v b/x86/CSE2depsproof.v index fd088962..e181b8f4 100644 --- a/x86/CSE2depsproof.v +++ b/x86/CSE2depsproof.v @@ -20,11 +20,79 @@ Require Import Registers Op RTL. Require Import CSE2 CSE2deps. Require Import Lia. +Lemma ptrofs_modulus : + Ptrofs.modulus = if Archi.ptr64 + then 18446744073709551616 + else 4294967296. +Proof. + reflexivity. +Qed. + Section SOUNDNESS. Variable F V : Type. Variable genv: Genv.t F V. Variable sp : val. +Section STACK_WRITE. + Variable m m2 : mem. + Variable chunkw chunkr : memory_chunk. + + Variable addrw addrr valw : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + + Section INDEXED_AWAY. + Variable ofsw ofsr : ptrofs. + Hypothesis ADDRW : eval_addressing genv sp + (Ainstack ofsw) nil = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Ainstack ofsr) nil = Some addrr. + + Lemma stack_load_store_away1 : + forall RANGEW : 0 <= Ptrofs.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= Ptrofs.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : Ptrofs.unsigned ofsw + size_chunk chunkw <= Ptrofs.unsigned ofsr + \/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw, + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intros. + + pose proof (max_size_chunk chunkr) as size_chunkr_bounded. + pose proof (max_size_chunk chunkw) as size_chunkw_bounded. + unfold largest_size_chunk in *. + + inv ADDRR. + inv ADDRW. + + destruct sp; try discriminate. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + + all: try (destruct (Ptrofs.unsigned_add_either i ofsr) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i ofsw) as [OFSW | OFSW]; + rewrite OFSW). + all: try rewrite ptrofs_modulus in *. + all: destruct Archi.ptr64. + + all: intuition lia. + Qed. + + Theorem stack_load_store_away : + can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true -> + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intro SWAP. + unfold can_swap_accesses_ofs in SWAP. + repeat rewrite andb_true_iff in SWAP. + repeat rewrite orb_true_iff in SWAP. + repeat rewrite Z.leb_le in SWAP. + apply stack_load_store_away1. + all: tauto. + Qed. + End INDEXED_AWAY. +End STACK_WRITE. + Section MEMORY_WRITE. Variable m m2 : mem. Variable chunkw chunkr : memory_chunk. @@ -237,7 +305,7 @@ Proof. intros until rs. intros ADDR ADDR' OVERLAP STORE. destruct addr; destruct addr'; try discriminate. - { (* Aindexed / Aindexed *) +- (* Aindexed / Aindexed *) destruct args as [ | base [ | ]]. 1,3: discriminate. destruct args' as [ | base' [ | ]]. 1,3: discriminate. simpl in OVERLAP. @@ -247,8 +315,7 @@ Proof. 2: discriminate. simpl in *. eapply load_store_away; eassumption. - } - { (* Aglobal / Aglobal *) +- (* Aglobal / Aglobal *) destruct args. 2: discriminate. destruct args'. 2: discriminate. simpl in *. @@ -259,7 +326,14 @@ Proof. eapply load_store_glob_away; eassumption. } eapply load_store_diff_globals; eassumption. - } +- (* Ainstack / Ainstack *) + destruct args. 2: discriminate. + destruct args'. 2: discriminate. + cbn in OVERLAP. + destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP. + 2: discriminate. + cbn in *. + eapply stack_load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. Qed. End SOUNDNESS. @@ -1037,6 +1037,20 @@ Proof. auto. Qed. +Lemma op_valid_pointer_eq: + forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, + (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> + eval_operation ge sp op args m1 = eval_operation ge sp op args m2. +Proof. + intros until m2. destruct op eqn:OP; simpl; try congruence. + - intros MEM; destruct cond; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + - intro MEM; destruct c; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. +Qed. + (** Global variables mentioned in an operation or addressing mode *) Definition globals_addressing (addr: addressing) : list ident := |