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 --- x86/PrepassSchedulingOracle.ml | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 x86/PrepassSchedulingOracle.ml (limited to 'x86') diff --git a/x86/PrepassSchedulingOracle.ml b/x86/PrepassSchedulingOracle.ml new file mode 100644 index 00000000..7b6a1b14 --- /dev/null +++ b/x86/PrepassSchedulingOracle.ml @@ -0,0 +1,5 @@ +open RTL +open Registers + +(* Do not do anything *) +let schedule_sequence (seqa : (instruction*Regset.t) array) = None -- cgit From 38f808a4b2a26d1ae71d9a0866e49a5207385e23 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 19 Oct 2020 19:08:09 +0200 Subject: op_valid_pointer_eq x86 --- x86/Op.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'x86') diff --git a/x86/Op.v b/x86/Op.v index 28e6dbd8..776f9495 100644 --- a/x86/Op.v +++ b/x86/Op.v @@ -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 := -- cgit From 7c63e3df80deb87a11355ed98e1a78970a7f78fd Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 23 Nov 2020 21:50:00 +0100 Subject: bug #223 fix on x86 / x86-64 --- x86/CSE2deps.v | 2 ++ x86/CSE2depsproof.v | 82 ++++++++++++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 80 insertions(+), 4 deletions(-) (limited to 'x86') 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. -- cgit