From 825b77fe8b4eb0919564e51cfaae69a6dfae24e3 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 2 Oct 2020 21:54:34 +0200 Subject: so that all architectures compile --- powerpc/PrepassSchedulingOracle.ml | 1 + 1 file changed, 1 insertion(+) create mode 120000 powerpc/PrepassSchedulingOracle.ml (limited to 'powerpc') diff --git a/powerpc/PrepassSchedulingOracle.ml b/powerpc/PrepassSchedulingOracle.ml new file mode 120000 index 00000000..9885fd52 --- /dev/null +++ b/powerpc/PrepassSchedulingOracle.ml @@ -0,0 +1 @@ +../x86/PrepassSchedulingOracle.ml \ No newline at end of file -- cgit From 8595aa32b35ef18c2124c9147173f366e5d14f86 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 19 Oct 2020 18:47:53 +0200 Subject: op_valid_pointer_eq ppc --- powerpc/Op.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'powerpc') 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 := -- cgit From 1fc9e3b1f4cf32e88888c5277894f5ed1e74f7af Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 23 Nov 2020 22:21:23 +0100 Subject: bug #223 fix on PPC --- powerpc/CSE2deps.v | 5 +++- powerpc/CSE2depsproof.v | 71 +++++++++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 73 insertions(+), 3 deletions(-) (limited to 'powerpc') 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. -- cgit