diff options
-rw-r--r-- | aarch64/CSE2deps.v | 20 | ||||
-rw-r--r-- | aarch64/CSE2depsproof.v | 130 | ||||
-rw-r--r-- | arm/CSE2deps.v | 20 | ||||
-rw-r--r-- | arm/CSE2depsproof.v | 132 | ||||
-rw-r--r-- | backend/CSE2.v | 158 | ||||
-rw-r--r-- | backend/CSE2proof.v | 828 | ||||
-rw-r--r-- | backend/IRC.ml | 1 | ||||
-rw-r--r-- | backend/ValueAnalysis.v | 5 | ||||
-rw-r--r-- | backend/ValueDomain.v | 5 | ||||
-rw-r--r-- | cfrontend/Cexec.v | 73 | ||||
-rw-r--r-- | common/Events.v | 88 | ||||
-rw-r--r-- | common/Memdata.v | 7 | ||||
-rw-r--r-- | common/Memory.v | 17 | ||||
-rw-r--r-- | powerpc/Archi.v | 4 | ||||
-rw-r--r-- | powerpc/CSE2deps.v | 20 | ||||
-rw-r--r-- | powerpc/CSE2depsproof.v | 132 | ||||
-rw-r--r-- | powerpc/Conventions1.v | 17 | ||||
-rw-r--r-- | powerpc/extractionMachdep.v | 3 | ||||
-rw-r--r-- | riscV/CSE2deps.v | 20 | ||||
-rw-r--r-- | riscV/CSE2depsproof.v | 129 | ||||
-rw-r--r-- | test/cse2/globals.c | 8 | ||||
-rw-r--r-- | test/cse2/indexed_addr.c | 6 | ||||
-rw-r--r-- | x86/CSE2deps.v | 24 | ||||
-rw-r--r-- | x86/CSE2depsproof.v | 262 |
24 files changed, 1266 insertions, 843 deletions
diff --git a/aarch64/CSE2deps.v b/aarch64/CSE2deps.v new file mode 100644 index 00000000..90b514a2 --- /dev/null +++ b/aarch64/CSE2deps.v @@ -0,0 +1,20 @@ +Require Import BoolEqual Coqlib. +Require Import AST Integers Floats. +Require Import Values Memory Globalenvs Events. +Require Import Op. + + +Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw := + (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk)) + && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk)) + && ((ofsw + size_chunk chunkw <=? ofsr) || + (ofsr + size_chunk chunkr <=? ofsw)). + +Definition may_overlap chunk addr args chunk' addr' args' := + match addr, addr', args, args' with + | (Aindexed ofs), (Aindexed ofs'), + (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 + end. diff --git a/aarch64/CSE2depsproof.v b/aarch64/CSE2depsproof.v new file mode 100644 index 00000000..e20824e3 --- /dev/null +++ b/aarch64/CSE2depsproof.v @@ -0,0 +1,130 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE2 CSE2deps. +Require Import Lia. + +Lemma ptrofs_size : + Ptrofs.wordsize = 64%nat. +Proof. + unfold Ptrofs.wordsize. + unfold Wordsize_Ptrofs.wordsize. + trivial. +Qed. + +Lemma ptrofs_modulus : + Ptrofs.modulus = 18446744073709551616. +Proof. + reflexivity. +Qed. + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Section MEMORY_WRITE. + Variable m m2 : mem. + Variable chunkw chunkr : memory_chunk. + Variable base : val. + + Variable addrw addrr valw valr : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + Hypothesis READ : Mem.loadv chunkr m addrr = Some valr. + + Section INDEXED_AWAY. + Variable ofsw ofsr : int64. + Hypothesis ADDRW : eval_addressing genv sp + (Aindexed ofsw) (base :: nil) = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Aindexed ofsr) (base :: nil) = Some addrr. + + Lemma load_store_away1 : + forall RANGEW : 0 <= Int64.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= Int64.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : Int64.unsigned ofsw + size_chunk chunkw <= Int64.unsigned ofsr + \/ Int64.unsigned ofsr + size_chunk chunkr <= Int64.unsigned ofsw, + Mem.loadv chunkr m2 addrr = Some valr. + 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. + rewrite <- READ. + destruct base; try discriminate. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + + all: unfold Ptrofs.of_int64. + + all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.repr (Int64.unsigned ofsr))) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.repr (Int64.unsigned ofsw))) as [OFSW | OFSW]; + rewrite OFSW). + all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 18446744073709551615; lia). + + all: try rewrite ptrofs_modulus in *. + + all: intuition lia. + Qed. + + Theorem load_store_away : + can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true -> + Mem.loadv chunkr m2 addrr = Some valr. + 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 load_store_away1. + all: tauto. + Qed. + End INDEXED_AWAY. +End MEMORY_WRITE. +End SOUNDNESS. + + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Lemma may_overlap_sound: + forall m m' : mem, + forall chunk addr args chunk' addr' args' v a a' vl rs, + (eval_addressing genv sp addr (rs ## args)) = Some a -> + (eval_addressing genv sp addr' (rs ## args')) = Some a' -> + (may_overlap chunk addr args chunk' addr' args') = false -> + (Mem.storev chunk m a v) = Some m' -> + (Mem.loadv chunk' m a') = Some vl -> + (Mem.loadv chunk' m' a') = Some vl. +Proof. + intros until rs. + intros ADDR ADDR' OVERLAP STORE LOAD. + destruct addr; destruct addr'; try discriminate. + { (* Aindexed / Aindexed *) + destruct args as [ | base [ | ]]. 1,3: discriminate. + destruct args' as [ | base' [ | ]]. 1,3: discriminate. + simpl 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. + simpl in *. + eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. + } +Qed. + +End SOUNDNESS. diff --git a/arm/CSE2deps.v b/arm/CSE2deps.v new file mode 100644 index 00000000..9db51bbb --- /dev/null +++ b/arm/CSE2deps.v @@ -0,0 +1,20 @@ +Require Import BoolEqual Coqlib. +Require Import AST Integers Floats. +Require Import Values Memory Globalenvs Events. +Require Import Op. + + +Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw := + (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk)) + && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk)) + && ((ofsw + size_chunk chunkw <=? ofsr) || + (ofsr + size_chunk chunkr <=? ofsw)). + +Definition may_overlap chunk addr args chunk' addr' args' := + match addr, addr', args, args' with + | (Aindexed ofs), (Aindexed ofs'), + (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 + end. diff --git a/arm/CSE2depsproof.v b/arm/CSE2depsproof.v new file mode 100644 index 00000000..2112a230 --- /dev/null +++ b/arm/CSE2depsproof.v @@ -0,0 +1,132 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE2 CSE2deps. +Require Import Lia. + +Lemma ptrofs_size : + Ptrofs.wordsize = 32%nat. +Proof. + unfold Ptrofs.wordsize. + unfold Wordsize_Ptrofs.wordsize. + trivial. +Qed. + +Lemma ptrofs_modulus : + Ptrofs.modulus = 4294967296. +Proof. + unfold Ptrofs.modulus. + rewrite ptrofs_size. + destruct Archi.ptr64; reflexivity. +Qed. + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Section MEMORY_WRITE. + Variable m m2 : mem. + Variable chunkw chunkr : memory_chunk. + Variable base : val. + + Variable addrw addrr valw valr : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + Hypothesis READ : Mem.loadv chunkr m addrr = Some valr. + + Section INDEXED_AWAY. + Variable ofsw ofsr : int. + Hypothesis ADDRW : eval_addressing genv sp + (Aindexed ofsw) (base :: nil) = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Aindexed ofsr) (base :: nil) = Some addrr. + + Lemma load_store_away1 : + forall RANGEW : 0 <= Int.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= Int.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : Int.unsigned ofsw + size_chunk chunkw <= Int.unsigned ofsr + \/ Int.unsigned ofsr + size_chunk chunkr <= Int.unsigned ofsw, + Mem.loadv chunkr m2 addrr = Some valr. + 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. + rewrite <- READ. + destruct base; 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 (Ptrofs.of_int ofsr)) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsw)) as [OFSW | OFSW]; + rewrite OFSW). + + all: try rewrite ptrofs_modulus in *. + + all: unfold Ptrofs.of_int. + + all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia). + all: intuition lia. + Qed. + + Theorem load_store_away : + can_swap_accesses_ofs (Int.unsigned ofsr) chunkr (Int.unsigned ofsw) chunkw = true -> + Mem.loadv chunkr m2 addrr = Some valr. + 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 load_store_away1. + all: tauto. + Qed. + End INDEXED_AWAY. +End MEMORY_WRITE. +End SOUNDNESS. + + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Lemma may_overlap_sound: + forall m m' : mem, + forall chunk addr args chunk' addr' args' v a a' vl rs, + (eval_addressing genv sp addr (rs ## args)) = Some a -> + (eval_addressing genv sp addr' (rs ## args')) = Some a' -> + (may_overlap chunk addr args chunk' addr' args') = false -> + (Mem.storev chunk m a v) = Some m' -> + (Mem.loadv chunk' m a') = Some vl -> + (Mem.loadv chunk' m' a') = Some vl. +Proof. + intros until rs. + intros ADDR ADDR' OVERLAP STORE LOAD. + destruct addr; destruct addr'; try discriminate. + { (* Aindexed / Aindexed *) + destruct args as [ | base [ | ]]. 1,3: discriminate. + destruct args' as [ | base' [ | ]]. 1,3: discriminate. + simpl in OVERLAP. + destruct (peq base base'). 2: discriminate. + subst base'. + destruct (can_swap_accesses_ofs (Int.unsigned i0) chunk' (Int.unsigned i) chunk) eqn:SWAP. + 2: discriminate. + simpl in *. + eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. + } +Qed. + +End SOUNDNESS. diff --git a/backend/CSE2.v b/backend/CSE2.v index 41adba7b..be72405b 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -6,7 +6,7 @@ David Monniaux, CNRS, VERIMAG Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. -Require Import Memory Registers Op RTL Maps. +Require Import Memory Registers Op RTL Maps CSE2deps. (* Static analysis *) @@ -29,30 +29,13 @@ Proof. decide equality. Defined. -Definition pset := PTree.t unit. - -Definition pset_inter : pset -> pset -> pset := - PTree.combine_null - (fun ov1 ov2 => Some tt). - -Definition pset_empty : pset := PTree.empty unit. -Definition pset_add (i : positive) (s : pset) := PTree.set i tt s. -Definition pset_remove (i : positive) (s : pset) := PTree.remove i s. - -Record relmap := mkrel { - var_to_sym : PTree.t sym_val ; - mem_used : pset ; - reg_used : PTree.t pset - }. - Module RELATION. - -Definition t := relmap. - + +Definition t := (PTree.t sym_val). Definition eq (r1 r2 : t) := - forall x, (PTree.get x (var_to_sym r1)) = (PTree.get x (var_to_sym r2)). + forall x, (PTree.get x r1) = (PTree.get x r2). -Definition top : t := mkrel (PTree.empty sym_val) pset_empty (PTree.empty pset). +Definition top : t := PTree.empty sym_val. Lemma eq_refl: forall x, eq x x. Proof. @@ -75,27 +58,27 @@ Qed. Definition sym_val_beq (x y : sym_val) := if eq_sym_val x y then true else false. -Definition beq (r1 r2 : t) := PTree.beq sym_val_beq (var_to_sym r1) (var_to_sym r2). +Definition beq (r1 r2 : t) := PTree.beq sym_val_beq r1 r2. Lemma beq_correct: forall r1 r2, beq r1 r2 = true -> eq r1 r2. Proof. unfold beq, eq. intros r1 r2 EQ x. - pose proof (PTree.beq_correct sym_val_beq (var_to_sym r1) (var_to_sym r2)) as CORRECT. + pose proof (PTree.beq_correct sym_val_beq r1 r2) as CORRECT. destruct CORRECT as [CORRECTF CORRECTB]. pose proof (CORRECTF EQ x) as EQx. clear CORRECTF CORRECTB EQ. unfold sym_val_beq in *. - destruct ((var_to_sym r1) ! x) as [R1x | ] in *; - destruct ((var_to_sym r2) ! x) as [R2x | ] in *; + destruct (r1 ! x) as [R1x | ] in *; + destruct (r2 ! x) as [R2x | ] in *; trivial; try contradiction. destruct (eq_sym_val R1x R2x) in *; congruence. Qed. Definition ge (r1 r2 : t) := forall x, - match PTree.get x (var_to_sym r1) with + match PTree.get x r1 with | None => True - | Some v => (PTree.get x (var_to_sym r2)) = Some v + | Some v => (PTree.get x r2) = Some v end. Lemma ge_refl: forall r1 r2, eq r1 r2 -> ge r1 r2. @@ -104,7 +87,7 @@ Proof. intros r1 r2 EQ x. pose proof (EQ x) as EQx. clear EQ. - destruct ((var_to_sym r1) ! x). + destruct (r1 ! x). - congruence. - trivial. Qed. @@ -115,13 +98,12 @@ Proof. intros r1 r2 r3 GE12 GE23 x. pose proof (GE12 x) as GE12x; clear GE12. pose proof (GE23 x) as GE23x; clear GE23. - destruct ((var_to_sym r1) ! x); trivial. - destruct ((var_to_sym r2) ! x); congruence. + destruct (r1 ! x); trivial. + destruct (r2 ! x); congruence. Qed. Definition lub (r1 r2 : t) := - mkrel - (PTree.combine + PTree.combine (fun ov1 ov2 => match ov1, ov2 with | (Some v1), (Some v2) => @@ -131,19 +113,12 @@ Definition lub (r1 r2 : t) := | None, _ | _, None => None end) - (var_to_sym r1) (var_to_sym r2)) - (pset_inter (mem_used r1) (mem_used r2)) - (PTree.combine_null - (fun x y => let r := pset_inter x y in - if PTree.bempty_canon r - then None - else Some r) - (reg_used r1) (reg_used r2)). + r1 r2. Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. unfold ge, lub. - intros r1 r2 x. simpl. + intros r1 r2 x. rewrite PTree.gcombine by reflexivity. destruct (_ ! _); trivial. destruct (_ ! _); trivial. @@ -153,7 +128,7 @@ Qed. Lemma ge_lub_right: forall x y, ge (lub x y) y. Proof. unfold ge, lub. - intros r1 r2 x. simpl. + intros r1 r2 x. rewrite PTree.gcombine by reflexivity. destruct (_ ! _); trivial. destruct (_ ! _); trivial. @@ -275,79 +250,53 @@ Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM). - apply L.ge_refl. apply L.eq_refl. Qed. - - Definition top := Some RELATION.top. End ADD_BOTTOM. Module RB := ADD_BOTTOM(RELATION). Module DS := Dataflow_Solver(RB)(NodeSetForward). -Definition kill_sym_val (dst : reg) (sv : sym_val) : bool := +Definition kill_sym_val (dst : reg) (sv : sym_val) := match sv with | SMove src => if peq dst src then true else false | SOp op args => List.existsb (peq dst) args | SLoad chunk addr args => List.existsb (peq dst) args end. - -Definition referenced_by sv := + +Definition kill_reg (dst : reg) (rel : RELATION.t) := + PTree.filter1 (fun x => negb (kill_sym_val dst x)) + (PTree.remove dst rel). + +Definition kill_sym_val_mem (sv: sym_val) := match sv with - | SMove src => src :: nil - | SOp op args => args - | SLoad chunk addr args => args - end. - -Definition referenced_by' osv := - match osv with - | None => nil - | Some sv => referenced_by sv + | SMove _ => false + | SOp op _ => op_depends_on_memory op + | SLoad _ _ _ => true end. -Definition remove_from_sets - (to_remove : reg) : - list reg -> PTree.t pset -> PTree.t pset := - List.fold_left - (fun sets reg => - match PTree.get reg sets with - | None => sets - | Some xset => - let xset' := PTree.remove to_remove xset in - if PTree.bempty_canon xset' - then PTree.remove reg sets - else PTree.set reg xset' sets - end). - -Definition kill_reg (dst : reg) (rel : RELATION.t) : RELATION.t := - let rel' := PTree.remove dst (var_to_sym rel) in - mkrel (PTree.filter1 (fun x => negb (kill_sym_val dst x)) rel') - (pset_remove dst (mem_used rel)) - (remove_from_sets dst (referenced_by' (PTree.get dst (var_to_sym rel))) - (PTree.remove dst (reg_used rel))). - -Definition kill_sym_val_mem (sv: sym_val) := +Definition kill_sym_val_store chunk addr args (sv: sym_val) := match sv with | SMove _ => false | SOp op _ => op_depends_on_memory op - | SLoad _ _ _ => true + | SLoad chunk' addr' args' => may_overlap chunk addr args chunk' addr' args' end. Definition kill_mem (rel : RELATION.t) := - mkrel - (PTree.remove_t (var_to_sym rel) (mem_used rel)) - pset_empty - (reg_used rel). (* FIXME *) - + PTree.filter1 (fun x => negb (kill_sym_val_mem x)) rel. Definition forward_move (rel : RELATION.t) (x : reg) : reg := - match (var_to_sym rel) ! x with + match rel ! x with | Some (SMove org) => org | _ => x end. +Definition kill_store1 chunk addr args rel := + PTree.filter1 (fun x => negb (kill_sym_val_store chunk addr args x)) rel. + +Definition kill_store chunk addr args rel := + kill_store1 chunk addr (List.map (forward_move rel) args) rel. + Definition move (src dst : reg) (rel : RELATION.t) := - let rel0 := kill_reg dst rel in - mkrel (PTree.set dst (SMove (forward_move rel src)) (var_to_sym rel0)) - (mem_used rel0) - (reg_used rel0). (* FIXME *) + PTree.set dst (SMove (forward_move rel src)) (kill_reg dst rel). Definition find_op_fold op args (already : option reg) x sv := match already with @@ -363,7 +312,7 @@ Definition find_op_fold op args (already : option reg) x sv := end. Definition find_op (rel : RELATION.t) (op : operation) (args : list reg) := - PTree.fold (find_op_fold op args) (var_to_sym rel) None. + PTree.fold (find_op_fold op args) rel None. Definition find_load_fold chunk addr args (already : option reg) x sv := match already with @@ -381,42 +330,37 @@ Definition find_load_fold chunk addr args (already : option reg) x sv := end. Definition find_load (rel : RELATION.t) (chunk : memory_chunk) (addr : addressing) (args : list reg) := - PTree.fold (find_load_fold chunk addr args) (var_to_sym rel) None. + PTree.fold (find_load_fold chunk addr args) rel None. Definition oper2 (op: operation) (dst : reg) (args : list reg) - (rel : RELATION.t) : RELATION.t := + (rel : RELATION.t) := let rel' := kill_reg dst rel in - mkrel (PTree.set dst (SOp op (List.map (forward_move rel') args)) (var_to_sym rel')) - (if op_depends_on_memory op then (pset_add dst (mem_used rel')) - else mem_used rel') - (reg_used rel'). (* FIXME *) + PTree.set dst (SOp op (List.map (forward_move rel') args)) rel'. Definition oper1 (op: operation) (dst : reg) (args : list reg) - (rel : RELATION.t) : RELATION.t := + (rel : RELATION.t) := if List.in_dec peq dst args then kill_reg dst rel else oper2 op dst args rel. Definition oper (op: operation) (dst : reg) (args : list reg) - (rel : RELATION.t) : RELATION.t := + (rel : RELATION.t) := match find_op rel op (List.map (forward_move rel) args) with | Some r => move r dst rel | None => oper1 op dst args rel end. Definition gen_oper (op: operation) (dst : reg) (args : list reg) - (rel : RELATION.t) : RELATION.t := + (rel : RELATION.t) := match op, args with | Omove, src::nil => move src dst rel | _, _ => oper op dst args rel end. Definition load2 (chunk: memory_chunk) (addr : addressing) - (dst : reg) (args : list reg) (rel : RELATION.t) : RELATION.t := + (dst : reg) (args : list reg) (rel : RELATION.t) := let rel' := kill_reg dst rel in - mkrel (PTree.set dst (SLoad chunk addr (List.map (forward_move rel') args)) (var_to_sym rel')) - (pset_add dst (mem_used rel')) - (reg_used rel'). (* FIXME *) + PTree.set dst (SLoad chunk addr (List.map (forward_move rel') args)) rel'. Definition load1 (chunk: memory_chunk) (addr : addressing) (dst : reg) (args : list reg) (rel : RELATION.t) := @@ -463,7 +407,7 @@ Definition apply_instr instr (rel : RELATION.t) : RB.t := | Inop _ | Icond _ _ _ _ | Ijumptable _ _ => Some rel - | Istore _ _ _ _ _ => Some (kill_mem rel) + | Istore chunk addr args _ _ => Some (kill_store chunk addr args rel) | Iop op args dst _ => Some (gen_oper op dst args rel) | Iload trap chunk addr args dst _ => Some (load chunk addr dst args rel) | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel)) @@ -483,7 +427,7 @@ Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t := Definition forward_map (f : RTL.function) := DS.fixpoint (RTL.fn_code f) RTL.successors_instr - (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) RB.top. + (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). Definition forward_move_b (rb : RB.t) (x : reg) := match rb with @@ -525,7 +469,7 @@ Definition transf_instr (fmap : option (PMap.t RB.t)) match instr with | Iop op args dst s => let args' := subst_args fmap pc args in - match (if is_trivial_op op then None else find_op_in_fmap fmap pc op args') with + match find_op_in_fmap fmap pc op args' with | None => Iop op args' dst s | Some src => Iop Omove (src::nil) dst s end diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 577b1e69..7e1dd430 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -13,7 +13,8 @@ Require Import Memory Registers Op RTL Maps. Require Import Globalenvs Values. Require Import Linking Values Memory Globalenvs Events Smallstep. Require Import Registers Op RTL. -Require Import CSE2. +Require Import CSE2 CSE2deps CSE2depsproof. +Require Import Lia. Lemma args_unaffected: forall rs : regset, @@ -37,515 +38,6 @@ Proof. assumption. Qed. -Lemma gpset_inter_none: forall a b i, - (pset_inter a b) ! i = None <-> - (a ! i = None) \/ (b ! i = None). -Proof. - intros. unfold pset_inter. - rewrite PTree.gcombine_null. - destruct (a ! i); destruct (b ! i); intuition discriminate. -Qed. - -Lemma some_some: - forall x : option unit, - x <> None <-> x = Some tt. -Proof. - destruct x as [[] | ]; split; congruence. -Qed. - -Lemma gpset_inter_some: forall a b i, - (pset_inter a b) ! i = Some tt <-> - (a ! i = Some tt) /\ (b ! i = Some tt). -Proof. - intros. unfold pset_inter. - rewrite PTree.gcombine_null. - destruct (a ! i) as [[] | ]; destruct (b ! i) as [[] | ]; intuition congruence. -Qed. - -Definition wellformed_mem (rel : RELATION.t) : Prop := - forall i sv, - (var_to_sym rel) ! i = Some sv -> - kill_sym_val_mem sv = true -> - (mem_used rel) ! i = Some tt. - -Definition wellformed_reg (rel : RELATION.t) : Prop := - forall i j sv, - (var_to_sym rel) ! i = Some sv -> - kill_sym_val j sv = true -> - match (reg_used rel) ! j with - | Some uses => uses ! i = Some tt - | None => False - end. - -Lemma wellformed_mem_top : wellformed_mem RELATION.top. -Proof. - unfold wellformed_mem, RELATION.top, pset_empty. - simpl. - intros. - rewrite PTree.gempty in *. - discriminate. -Qed. -Local Hint Resolve wellformed_mem_top : wellformed. - -Lemma wellformed_reg_top : wellformed_reg RELATION.top. -Proof. - unfold wellformed_reg, RELATION.top, pset_empty. - simpl. - intros. - rewrite PTree.gempty in *. - discriminate. -Qed. -Local Hint Resolve wellformed_reg_top : wellformed. - -Lemma wellformed_mem_lub : forall a b, - (wellformed_mem a) -> (wellformed_mem b) -> (wellformed_mem (RELATION.lub a b)). -Proof. - unfold wellformed_mem, RELATION.lub. - simpl. - intros a b Ha Hb. - intros i sv COMBINE KILLABLE. - rewrite PTree.gcombine in *. - 2: reflexivity. - destruct (var_to_sym a) ! i as [syma | ] eqn:SYMA; - destruct (var_to_sym b) ! i as [symb | ] eqn:SYMB; - try discriminate. - destruct (eq_sym_val syma symb); try discriminate. - subst syma. - inv COMBINE. - apply gpset_inter_some. - split; eauto. -Qed. -Local Hint Resolve wellformed_mem_lub : wellformed. - -Lemma wellformed_reg_lub : forall a b, - (wellformed_reg a) -> (wellformed_reg b) -> (wellformed_reg (RELATION.lub a b)). -Proof. - unfold wellformed_reg, RELATION.lub. - simpl. - intros a b Ha Hb. - intros i j sv COMBINE KILLABLE. - specialize Ha with (i := i) (j := j). - specialize Hb with (i := i) (j := j). - rewrite PTree.gcombine in *. - 2: reflexivity. - destruct (var_to_sym a) ! i as [syma | ] eqn:SYMA; - destruct (var_to_sym b) ! i as [symb | ] eqn:SYMB; - try discriminate. - specialize Ha with (sv := syma). - specialize Hb with (sv := symb). - destruct (eq_sym_val syma symb); try discriminate. - subst syma. - inv COMBINE. - rewrite PTree.gcombine_null. - destruct ((reg_used a) ! j) as [uA| ]; destruct ((reg_used b) ! j) as [uB | ]; auto. - { pose proof (PTree.bempty_canon_correct (pset_inter uA uB) i) as EMPTY. - destruct PTree.bempty_canon. - - rewrite gpset_inter_none in EMPTY. - intuition congruence. - - rewrite gpset_inter_some. - auto. - } -Qed. -Local Hint Resolve wellformed_reg_lub : wellformed. - -Lemma wellformed_mem_kill_reg: - forall dst rel, - (wellformed_mem rel) -> (wellformed_mem (kill_reg dst rel)). -Proof. - unfold wellformed_mem, kill_reg, pset_remove. - simpl. - intros dst rel Hrel. - intros i sv KILLREG KILLABLE. - rewrite PTree.gfilter1 in KILLREG. - destruct (peq dst i). - { subst i. - rewrite PTree.grs in *. - discriminate. - } - rewrite PTree.gro in * by congruence. - specialize Hrel with (i := i). - eapply Hrel. - 2: eassumption. - destruct (_ ! i); try discriminate. - destruct negb; congruence. -Qed. -Local Hint Resolve wellformed_mem_kill_reg : wellformed. - -Lemma kill_sym_val_referenced: - forall dst, - forall sv, - (kill_sym_val dst sv)=true <-> In dst (referenced_by sv). -Proof. - intros. - destruct sv; simpl. - - destruct peq; intuition congruence. - - rewrite existsb_exists. - split. - + intros [x [IN EQ]]. - destruct peq. - * subst x; trivial. - * discriminate. - + intro. - exists dst. - split; trivial. - destruct peq; trivial. - congruence. - - rewrite existsb_exists. - split. - + intros [x [IN EQ]]. - destruct peq. - * subst x; trivial. - * discriminate. - + intro. - exists dst. - split; trivial. - destruct peq; trivial. - congruence. -Qed. -Local Hint Resolve kill_sym_val_referenced : wellformed. - -Lemma remove_from_sets_notin: - forall dst l sets j, - not (In j l) -> - (remove_from_sets dst l sets) ! j = sets ! j. -Proof. - induction l; simpl; trivial. - intros. - rewrite IHl by tauto. - destruct (@PTree.get (PTree.t unit) a sets) eqn:SETSA; trivial. - pose proof (PTree.bempty_canon_correct (PTree.remove dst t)) as CORRECT. - destruct (PTree.bempty_canon (PTree.remove dst t)). - - apply PTree.gro. - intuition. - - rewrite PTree.gso by intuition. - trivial. -Qed. - -Lemma remove_from_sets_pass: - forall dst l sets i j, - i <> dst -> - match sets ! j with - | Some uses => uses ! i = Some tt - | None => False - end -> - match (remove_from_sets dst l sets) ! j with - | Some uses => uses ! i = Some tt - | None => False - end. -Proof. - induction l; simpl; trivial. - intros. - apply IHl; trivial. - destruct (@PTree.get (PTree.t unit) a sets) eqn:SETSA; trivial. - pose proof (PTree.bempty_canon_correct (PTree.remove dst t)) as CORRECT. - specialize CORRECT with (i := i). - destruct (PTree.bempty_canon (PTree.remove dst t)). - - rewrite PTree.gro in CORRECT by congruence. - destruct (peq a j). - + subst a. - rewrite SETSA in *. - intuition congruence. - + rewrite PTree.gro by congruence. - assumption. - - destruct (peq a j). - + subst a. - rewrite SETSA in *. - rewrite PTree.gss. - rewrite PTree.gro by congruence. - assumption. - + rewrite PTree.gso by congruence. - assumption. -Qed. -Local Hint Resolve remove_from_sets_pass : wellformed. - -Lemma rem_comes_from: - forall A x y (tr: PTree.t A) v, - (PTree.remove x tr) ! y = Some v -> tr ! y = Some v. -Proof. - intros. - destruct (peq x y). - - subst y. - rewrite PTree.grs in *. - discriminate. - - rewrite PTree.gro in * by congruence. - assumption. -Qed. -Local Hint Resolve rem_comes_from : wellformed. - -Lemma rem_ineq: - forall A x y (tr: PTree.t A) v, - (PTree.remove x tr) ! y = Some v -> x<>y. -Proof. - intros. - intro. - subst y. - rewrite PTree.grs in *. - discriminate. -Qed. -Local Hint Resolve rem_ineq : wellformed. - -Lemma wellformed_reg_kill_reg: - forall dst rel, - (wellformed_reg rel) -> (wellformed_reg (kill_reg dst rel)). -Proof. - unfold wellformed_reg, kill_reg. - simpl. - intros dst rel Hrel. - intros i j sv KILLREG KILLABLE. - - rewrite PTree.gfilter1 in KILLREG. - destruct PTree.get eqn:REMi in KILLREG. - 2: discriminate. - destruct negb eqn:NEGB in KILLREG. - 2: discriminate. - inv KILLREG. - - assert ((var_to_sym rel) ! i = Some sv) as RELi by eauto with wellformed. - - destruct (peq dst j). - { (* absurd case *) - subst j. - rewrite KILLABLE in NEGB. - simpl in NEGB. - discriminate. - } - specialize Hrel with (i := i) (j := j) (sv := sv). - destruct ((var_to_sym rel) ! dst) eqn:DST; simpl. - { - assert (dst <> i) by eauto with wellformed. - apply remove_from_sets_pass. - congruence. - rewrite PTree.gro by congruence. - apply Hrel; trivial. - } - rewrite PTree.gro by congruence. - apply Hrel; trivial. -Qed. -Local Hint Resolve wellformed_reg_kill_reg : wellformed. - -Lemma wellformed_mem_kill_mem: - forall rel, - (wellformed_mem rel) -> (wellformed_mem (kill_mem rel)). -Proof. - unfold wellformed_mem, kill_mem. - simpl. - intros rel Hrel. - intros i sv KILLMEM KILLABLE. - rewrite PTree.gremove_t in KILLMEM. - exfalso. - specialize Hrel with (i := i). - destruct ((var_to_sym rel) ! i) eqn:RELi. - - specialize Hrel with (sv := s). - destruct ((mem_used rel) ! i) eqn:USEDi. - discriminate. - inv KILLMEM. - intuition congruence. - - destruct ((mem_used rel) ! i); discriminate. -Qed. -Local Hint Resolve wellformed_mem_kill_mem : wellformed. - -Lemma wellformed_reg_kill_mem: - forall rel, - (wellformed_reg rel) -> (wellformed_reg (kill_mem rel)). -Proof. - unfold wellformed_reg, kill_mem. - simpl. - intros rel Hrel. - intros i j sv KILLMEM KILLABLE. - apply Hrel with (sv := sv); trivial. - rewrite PTree.gremove_t in KILLMEM. - destruct ((mem_used rel) ! i) in KILLMEM. - discriminate. - assumption. -Qed. -Local Hint Resolve wellformed_reg_kill_mem : wellformed. - -Lemma wellformed_mem_move: - forall r dst rel, - (wellformed_mem rel) -> (wellformed_mem (move r dst rel)). -Proof. - Local Opaque kill_reg. - intros; unfold move, wellformed_mem; simpl. - intros i sv MOVE KILL. - destruct (peq i dst). - { subst i. - rewrite PTree.gss in MOVE. - inv MOVE. - simpl in KILL. - discriminate. - } - rewrite PTree.gso in MOVE by congruence. - eapply wellformed_mem_kill_reg; eauto. -Qed. -Local Hint Resolve wellformed_mem_move : wellformed. - -Lemma wellformed_mem_oper2: - forall op dst args rel, - (wellformed_mem rel) -> - (wellformed_mem (oper2 op dst args rel)). -Proof. - intros until rel. intro WELLFORMED. - unfold oper2. - intros i sv MOVE OPER. - simpl in *. - destruct (peq i dst). - { subst i. - rewrite PTree.gss in MOVE. - inv MOVE. - simpl in OPER. - rewrite OPER. - apply PTree.gss. - } - unfold pset_add. - rewrite PTree.gso in MOVE by congruence. - destruct op_depends_on_memory. - - rewrite PTree.gso by congruence. - eapply wellformed_mem_kill_reg; eauto. - - eapply wellformed_mem_kill_reg; eauto. -Qed. -Local Hint Resolve wellformed_mem_oper2 : wellformed. - -Lemma wellformed_mem_oper1: - forall op dst args rel, - (wellformed_mem rel) -> - (wellformed_mem (oper1 op dst args rel)). -Proof. - unfold oper1. intros. - destruct in_dec ; auto with wellformed. -Qed. -Local Hint Resolve wellformed_mem_oper1 : wellformed. - -Lemma wellformed_mem_oper: - forall op dst args rel, - (wellformed_mem rel) -> - (wellformed_mem (oper op dst args rel)). -Proof. - unfold oper. intros. - destruct find_op ; auto with wellformed. -Qed. -Local Hint Resolve wellformed_mem_oper : wellformed. - -Lemma wellformed_mem_gen_oper: - forall op dst args rel, - (wellformed_mem rel) -> - (wellformed_mem (gen_oper op dst args rel)). -Proof. - intros. - unfold gen_oper. - destruct op; auto with wellformed. - destruct args; auto with wellformed. - destruct args; auto with wellformed. -Qed. -Local Hint Resolve wellformed_mem_gen_oper : wellformed. - -Lemma wellformed_mem_load2 : - forall chunk addr dst args rel, - (wellformed_mem rel) -> - (wellformed_mem (load2 chunk addr dst args rel)). -Proof. - intros. - unfold load2, wellformed_mem. - simpl. - intros i sv LOAD KILL. - destruct (peq i dst). - { subst i. - apply PTree.gss. - } - unfold pset_add. - rewrite PTree.gso in * by congruence. - eapply wellformed_mem_kill_reg; eauto. -Qed. -Local Hint Resolve wellformed_mem_load2 : wellformed. - -Lemma wellformed_mem_load1 : - forall chunk addr dst args rel, - (wellformed_mem rel) -> - (wellformed_mem (load1 chunk addr dst args rel)). -Proof. - intros. - unfold load1. - destruct in_dec; eauto with wellformed. -Qed. -Local Hint Resolve wellformed_mem_load1 : wellformed. - -Lemma wellformed_mem_load : - forall chunk addr dst args rel, - (wellformed_mem rel) -> - (wellformed_mem (load chunk addr dst args rel)). -Proof. - intros. - unfold load. - destruct find_load; eauto with wellformed. -Qed. -Local Hint Resolve wellformed_mem_load : wellformed. - -Definition wellformed_mem_rb (rb : RB.t) := - match rb with - | None => True - | Some r => wellformed_mem r - end. - -Lemma wellformed_mem_apply_instr: - forall instr rel, - (wellformed_mem rel) -> - (wellformed_mem_rb (apply_instr instr rel)). -Proof. - destruct instr; simpl; auto with wellformed. -Qed. -Local Hint Resolve wellformed_mem_apply_instr : wellformed. - -Lemma wellformed_mem_rb_bot : - wellformed_mem_rb RB.bot. -Proof. - simpl. - trivial. -Qed. -Local Hint Resolve wellformed_mem_rb_bot: wellformed. - -Lemma wellformed_mem_rb_top : - wellformed_mem_rb RB.top. -Proof. - simpl. - auto with wellformed. -Qed. -Local Hint Resolve wellformed_mem_rb_top: wellformed. - -Lemma wellformed_mem_rb_apply_instr': - forall code pc rel, - (wellformed_mem_rb rel) -> - (wellformed_mem_rb (apply_instr' code pc rel)). -Proof. - destruct rel; simpl; trivial. - intro. - destruct (code ! pc); - eauto with wellformed. -Qed. -Local Hint Resolve wellformed_mem_rb_apply_instr' : wellformed. - -Lemma wellformed_mem_rb_lub : forall a b, - (wellformed_mem_rb a) -> (wellformed_mem_rb b) -> (wellformed_mem_rb (RB.lub a b)). -Proof. - destruct a; destruct b; simpl; auto with wellformed. -Qed. -Local Hint Resolve wellformed_mem_rb_lub: wellformed. - -Definition wellformed_mem_fmap fmap := - forall i, wellformed_mem_rb (fmap !! i). - -Theorem wellformed_mem_forward_map : forall f, - forall fmap, (forward_map f) = Some fmap -> - wellformed_mem_fmap fmap. -Proof. - intros. - unfold forward_map in *. - unfold wellformed_mem_fmap. - intro. - eapply DS.fixpoint_invariant with (ev := Some RELATION.top); eauto with wellformed. -Qed. -Local Hint Resolve wellformed_mem_forward_map: wellformed. - -Local Transparent kill_reg. - Section SOUNDNESS. Variable F V : Type. Variable genv: Genv.t F V. @@ -570,7 +62,7 @@ Definition sem_sym_val sym rs (v : option val) : Prop := end. Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) (v : val) : Prop := - match (var_to_sym rel) ! x with + match rel ! x with | None => True | Some sym => sem_sym_val sym rs (Some (rs # x)) end. @@ -610,7 +102,7 @@ Proof. pose proof (SEM arg) as SEMarg. simpl. unfold forward_move. unfold sem_sym_val in *. - destruct (_ ! arg); trivial. + destruct (t ! arg); trivial. destruct s; congruence. Qed. @@ -639,7 +131,7 @@ Lemma kill_reg_sound : Proof. unfold sem_rel, kill_reg, sem_reg, sem_sym_val. intros until v. - intros REL x. simpl. + intros REL x. rewrite PTree.gfilter1. destruct (Pos.eq_dec dst x). { @@ -649,7 +141,7 @@ Proof. } rewrite PTree.gro by congruence. rewrite Regmap.gso by congruence. - destruct (_ ! x) as [relx | ] eqn:RELx; trivial. + destruct (rel ! x) as [relx | ] eqn:RELx; trivial. unfold kill_sym_val. pose proof (REL x) as RELinstx. rewrite RELx in RELinstx. @@ -702,13 +194,12 @@ Proof. { subst x. unfold sem_reg. - simpl. rewrite PTree.gss. rewrite Regmap.gss. unfold sem_reg in *. simpl. unfold forward_move. - destruct (_ ! src) as [ sv |]; simpl. + destruct (rel ! src) as [ sv |]; simpl. destruct sv eqn:SV; simpl in *. { destruct (peq dst src0). @@ -724,7 +215,6 @@ Proof. } rewrite Regmap.gso by congruence. unfold sem_reg. - simpl. rewrite PTree.gso by congruence. rewrite Regmap.gso in KILL by congruence. exact KILL. @@ -737,10 +227,9 @@ Lemma move_cases_neq: Proof. intros until a. intro NEQ. unfold kill_reg, forward_move. - simpl. rewrite PTree.gfilter1. rewrite PTree.gro by congruence. - destruct (_ ! a); simpl. + destruct (rel ! a); simpl. 2: congruence. destruct s. { @@ -774,10 +263,9 @@ Proof. unfold kill_reg. unfold sem_reg in RELa. unfold forward_move. - simpl. rewrite PTree.gfilter1. rewrite PTree.gro by auto. - destruct (_ ! a); simpl; trivial. + destruct (rel ! a); simpl; trivial. destruct s; simpl in *; destruct negb; simpl; congruence. Qed. @@ -801,7 +289,6 @@ Proof. { subst x. unfold sem_reg. - simpl. rewrite PTree.gss. rewrite Regmap.gss. simpl. @@ -811,7 +298,6 @@ Proof. } rewrite Regmap.gso by congruence. unfold sem_reg. - simpl. rewrite PTree.gso by congruence. rewrite Regmap.gso in KILL by congruence. exact KILL. @@ -859,13 +345,13 @@ Proof. | Some src => eval_operation genv sp op rs ## args m = Some rs # src end -> fold_left (fun (a : option reg) (p : positive * sym_val) => - find_op_fold op args a (fst p) (snd p)) (PTree.elements (var_to_sym rel)) start = + find_op_fold op args a (fst p) (snd p)) (PTree.elements rel) start = Some src -> eval_operation genv sp op rs ## args m = Some rs # src) as REC. { unfold sem_rel, sem_reg in REL. - generalize (PTree.elements_complete (var_to_sym rel)). - generalize (PTree.elements (var_to_sym rel)). + generalize (PTree.elements_complete rel). + generalize (PTree.elements rel). induction l; simpl. { intros. @@ -890,7 +376,7 @@ Proof. destruct eq_args; trivial. subst args0. simpl. - assert (((var_to_sym rel) ! r) = Some (SOp op args)) as RELatr. + assert ((rel ! r) = Some (SOp op args)) as RELatr. { apply COMPLETE. left. @@ -905,6 +391,7 @@ Proof. apply REC; auto. Qed. + Lemma find_load_sound : forall rel : RELATION.t, forall chunk : memory_chunk, @@ -941,7 +428,7 @@ Proof. end -> fold_left (fun (a : option reg) (p : positive * sym_val) => - find_load_fold chunk addr args a (fst p) (snd p)) (PTree.elements (var_to_sym rel)) start = + find_load_fold chunk addr args a (fst p) (snd p)) (PTree.elements rel) start = Some src -> match eval_addressing genv sp addr rs##args with | Some a => match Mem.loadv chunk m a with @@ -953,8 +440,8 @@ Proof. { unfold sem_rel, sem_reg in REL. - generalize (PTree.elements_complete (var_to_sym rel)). - generalize (PTree.elements (var_to_sym rel)). + generalize (PTree.elements_complete rel). + generalize (PTree.elements rel). induction l; simpl. { intros. @@ -981,7 +468,7 @@ Proof. destruct eq_args; trivial. subst args0. simpl. - assert (((var_to_sym rel) ! r) = Some (SLoad chunk addr args)) as RELatr. + assert ((rel ! r) = Some (SLoad chunk addr args)) as RELatr. { apply COMPLETE. left. @@ -1077,7 +564,21 @@ Proof. 2: (apply IHargs; assumption). unfold forward_move, sem_rel, sem_reg, sem_sym_val in *. pose proof (REL a) as RELa. - destruct (_ ! a); trivial. + destruct (rel ! a); trivial. + destruct s; congruence. +Qed. + + +Lemma forward_move_rs: + forall rel arg rs, + sem_rel rel rs -> + rs # (forward_move rel arg) = rs # arg. +Proof. + unfold forward_move, sem_rel, sem_reg, sem_sym_val in *. + intros until rs. + intro REL. + pose proof (REL arg) as RELarg. + destruct (rel ! arg); trivial. destruct s; congruence. Qed. @@ -1160,7 +661,6 @@ Proof. { subst x. unfold sem_reg. - simpl. rewrite PTree.gss. rewrite Regmap.gss. simpl. @@ -1173,7 +673,7 @@ Proof. discriminate. } rewrite Regmap.gso by congruence. - unfold sem_reg. simpl. + unfold sem_reg. rewrite PTree.gso by congruence. rewrite Regmap.gso in KILL by congruence. exact KILL. @@ -1198,7 +698,7 @@ Proof. destruct (peq x dst). { subst x. - unfold sem_reg. simpl. + unfold sem_reg. rewrite PTree.gss. rewrite Regmap.gss. simpl. @@ -1208,7 +708,7 @@ Proof. trivial. } rewrite Regmap.gso by congruence. - unfold sem_reg. simpl. + unfold sem_reg. rewrite PTree.gso by congruence. rewrite Regmap.gso in KILL by congruence. exact KILL. @@ -1235,7 +735,7 @@ Proof. destruct (peq x dst). { subst x. - unfold sem_reg. simpl. + unfold sem_reg. rewrite PTree.gss. rewrite Regmap.gss. simpl. @@ -1245,8 +745,7 @@ Proof. right; trivial. } rewrite Regmap.gso by congruence. - unfold sem_reg. simpl. - simpl. + unfold sem_reg. rewrite PTree.gso by congruence. rewrite Regmap.gso in KILL by congruence. exact KILL. @@ -1443,7 +942,6 @@ Proof. intros REL x. pose proof (REL x) as RELx. unfold kill_reg, sem_reg in *. - simpl. rewrite PTree.gfilter1. destruct (peq res x). { subst x. @@ -1451,7 +949,7 @@ Proof. reflexivity. } rewrite PTree.gro by congruence. - destruct (_ ! x) as [sv | ]; trivial. + destruct (mpc ! x) as [sv | ]; trivial. destruct negb; trivial. Qed. @@ -1474,8 +972,8 @@ Proof. pose proof (RE x) as REx. pose proof (GE x) as GEx. unfold sem_reg in *. - destruct ((var_to_sym r1) ! x) as [r1x | ] in *; - destruct ((var_to_sym r2) ! x) as [r2x | ] in *; + destruct (r1 ! x) as [r1x | ] in *; + destruct (r2 ! x) as [r2x | ] in *; congruence. Qed. End SAME_MEMORY. @@ -1484,35 +982,58 @@ Lemma kill_mem_sound : forall m m' : mem, forall rel : RELATION.t, forall rs, - wellformed_mem rel -> sem_rel m rel rs -> sem_rel m' (kill_mem rel) rs. Proof. unfold sem_rel, sem_reg. intros until rs. - intros WELLFORMED SEM x. - unfold wellformed_mem in *. - specialize SEM with (x := x). - specialize WELLFORMED with (i := x). + intros SEM x. + pose proof (SEM x) as SEMx. unfold kill_mem. - simpl. - rewrite PTree.gremove_t. + rewrite PTree.gfilter1. unfold kill_sym_val_mem. - destruct ((var_to_sym rel) ! x) as [ sv | ] eqn:VAR. - - specialize WELLFORMED with (sv0 := sv). - destruct ((mem_used rel) ! x) eqn:USED; trivial. - unfold sem_sym_val in *. - destruct sv; simpl in *; trivial. - + rewrite op_depends_on_memory_correct with (m2 := m). - assumption. - destruct op_depends_on_memory; intuition congruence. - + intuition discriminate. - - replace (match (mem_used rel) ! x with - | Some _ | _ => None - end) with (@None sym_val) by - (destruct ((mem_used rel) ! x); trivial). - trivial. + destruct (rel ! x) as [ sv | ]. + 2: reflexivity. + destruct sv; simpl in *; trivial. + { + destruct op_depends_on_memory eqn:DEPENDS; simpl; trivial. + rewrite SEMx. + apply op_depends_on_memory_correct; auto. + } Qed. - + +Lemma kill_store_sound : + forall m m' : mem, + forall rel : RELATION.t, + forall chunk addr args a v rs, + (eval_addressing genv sp addr (rs ## args)) = Some a -> + (Mem.storev chunk m a v) = Some m' -> + sem_rel m rel rs -> sem_rel m' (kill_store chunk addr args rel) rs. +Proof. + unfold sem_rel, sem_reg. + intros until rs. + intros ADDR STORE SEM x. + pose proof (SEM x) as SEMx. + unfold kill_store, kill_store1. + rewrite PTree.gfilter1. + destruct (rel ! x) as [ sv | ]. + 2: reflexivity. + destruct sv; simpl in *; trivial. + { + destruct op_depends_on_memory eqn:DEPENDS; simpl; trivial. + rewrite SEMx. + apply op_depends_on_memory_correct; auto. + } + destruct may_overlap eqn:OVERLAP; simpl; trivial. + destruct (eval_addressing genv sp addr0 rs ## args0) eqn:ADDR0. + { + erewrite may_overlap_sound with (args := (map (forward_move rel) args)). + all: try eassumption. + + erewrite forward_move_map by eassumption. + assumption. + } + intuition congruence. +Qed. End SOUNDNESS. Definition match_prog (p tp: RTL.program) := @@ -1600,6 +1121,7 @@ Definition fmap_sem' := fmap_sem fundef unit ge. Definition subst_arg_ok' := subst_arg_ok fundef unit ge. Definition subst_args_ok' := subst_args_ok fundef unit ge. Definition kill_mem_sound' := kill_mem_sound fundef unit ge. +Definition kill_store_sound' := kill_store_sound fundef unit ge. Lemma sem_rel_b_ge: forall rb1 rb2 : RB.t, @@ -1651,39 +1173,6 @@ Ltac TR_AT := generalize (transf_function_at _ _ _ A); intros end. -Lemma wellformed_mem_mpc: - forall f map pc mpc, - (forward_map f) = Some map -> - map # pc = Some mpc -> - wellformed_mem mpc. -Proof. - intros. - assert (wellformed_mem_fmap map) by eauto with wellformed. - unfold wellformed_mem_fmap, wellformed_mem_rb in *. - specialize H1 with (i := pc). - rewrite H0 in H1. - assumption. -Qed. -Hint Resolve wellformed_mem_mpc : wellformed. - -Lemma match_same_option : - forall { A B : Type}, - forall x : option A, - forall y : B, - (match x with Some _ => y | None => y end) = y. -Proof. - destruct x; trivial. -Qed. - -Lemma match_same_bool : - forall { B : Type}, - forall x : bool, - forall y : B, - (if x then y else y) = y. -Proof. - destruct x; trivial. -Qed. - Lemma step_simulation: forall S1 t S2, RTL.step ge S1 t S2 -> forall S1', match_states S1 S1' -> @@ -1711,9 +1200,8 @@ Proof. reflexivity. - (* op *) unfold transf_instr in *. - destruct (if is_trivial_op op then None else find_op_in_fmap (forward_map f) pc op (subst_args (forward_map f) pc args)) eqn:FIND_OP. + destruct find_op_in_fmap eqn:FIND_OP. { - destruct is_trivial_op. discriminate. unfold find_op_in_fmap, fmap_sem', fmap_sem in *. destruct (forward_map f) as [map |] eqn:MAP. 2: discriminate. @@ -1803,9 +1291,9 @@ Proof. { f_equal. symmetry. - apply find_load_sound' with (chunk := chunk) (m := m) (a := a) (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs); trivial. rewrite MAP in H0. - assumption. + eapply find_load_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs). + all: eassumption. } unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. } @@ -1830,36 +1318,37 @@ Proof. apply load_sound with (a := a); auto. } { - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. - apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload; eauto. - rewrite (subst_args_ok' sp m); assumption. - constructor; auto. - - simpl in *. - unfold fmap_sem', fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. + apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. + rewrite (subst_args_ok' sp m); assumption. + constructor; auto. + + simpl in *. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + { + replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). { - replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - simpl. - reflexivity. + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. } - apply load_sound with (a := a); assumption. + unfold apply_instr'. + rewrite H. + rewrite MPC. + simpl. + reflexivity. + } + apply load_sound with (a := a); assumption. } -- unfold transf_instr in *. +- (* load notrap1 *) + unfold transf_instr in *. destruct find_load_in_fmap eqn:FIND_LOAD. { unfold find_load_in_fmap, fmap_sem', fmap_sem in *. @@ -1868,16 +1357,16 @@ Proof. change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. destruct (map # pc) as [mpc | ] eqn:MPC. 2: discriminate. - econstructor; split. { eapply exec_Iop with (v := (default_notrap_load_value chunk)); eauto. + simpl. rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0. - { simpl. + { f_equal. - apply find_load_notrap1_sound' with (chunk := chunk) (m := m) (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs); trivial. rewrite MAP in H0. - assumption. + eapply find_load_notrap1_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs). + all: eassumption. } unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. } @@ -1901,37 +1390,38 @@ Proof. unfold sem_rel_b', sem_rel_b. apply load_notrap1_sound; auto. } - { - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = None). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap1; eauto. - rewrite subst_args_ok with (genv := ge) (sp := sp) (m := m) ; assumption. - constructor; auto. + { + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = None). + rewrite <- H0. + apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload_notrap1; eauto. + rewrite (subst_args_ok' sp m); assumption. + constructor; auto. - simpl in *. - unfold fmap_sem', fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + simpl in *. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + { + replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). { - replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - simpl. - reflexivity. + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. } - apply load_notrap1_sound; trivial. + unfold apply_instr'. + rewrite H. + rewrite MPC. + simpl. + reflexivity. + } + apply load_notrap1_sound; assumption. } -- (* load notrap2 *) - unfold transf_instr in *. +(* load notrap2 *) +- unfold transf_instr in *. destruct find_load_in_fmap eqn:FIND_LOAD. { unfold find_load_in_fmap, fmap_sem', fmap_sem in *. @@ -1947,9 +1437,9 @@ Proof. rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0. { f_equal. - apply find_load_notrap2_sound' with (chunk := chunk) (m := m) (a := a) (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs); trivial. rewrite MAP in H0. - assumption. + eapply find_load_notrap2_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs). + all: try eassumption. } unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. } @@ -1973,19 +1463,20 @@ Proof. unfold sem_rel_b', sem_rel_b. apply load_notrap2_sound with (a := a); auto. } - { + { econstructor; split. assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + rewrite <- H0. + apply eval_addressing_preserved. exact symbols_preserved. eapply exec_Iload_notrap2; eauto. - rewrite subst_args_ok with (genv := ge) (sp := sp) (m := m); assumption. + rewrite (subst_args_ok' sp m); assumption. constructor; auto. simpl in *. unfold fmap_sem', fmap_sem in *. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). { replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). { @@ -2016,9 +1507,9 @@ Proof. unfold fmap_sem', fmap_sem in *. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply sem_rel_b_ge with (rb2 := Some (kill_mem mpc)); trivial. + apply sem_rel_b_ge with (rb2 := Some (kill_store chunk addr args mpc)); trivial. { - replace (Some (kill_mem mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + replace (Some (kill_store chunk addr args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). { eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. 2: apply apply_instr'_bot. @@ -2030,7 +1521,7 @@ Proof. rewrite H. reflexivity. } - apply (kill_mem_sound' sp m); eauto with wellformed. + eapply (kill_store_sound' sp m); eassumption. (* call *) - econstructor; split. @@ -2060,7 +1551,8 @@ Proof. reflexivity. } apply kill_reg_sound. - apply (kill_mem_sound' sp m); eauto with wellformed. + apply (kill_mem_sound' sp m). + assumption. } (* tailcall *) diff --git a/backend/IRC.ml b/backend/IRC.ml index 67da47da..785b0a2d 100644 --- a/backend/IRC.ml +++ b/backend/IRC.ml @@ -238,7 +238,6 @@ type graph = { according to their types. A variable can be forced into class 2 by giving it a negative spill cost. *) - let class_of_reg r = if Conventions1.is_float_reg r then 1 else 0 diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 9a33768c..e25d2e5f 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -1044,9 +1044,8 @@ Proof. red; simpl; intros. destruct (plt b (Mem.nextblock m)). exploit RO; eauto. intros (R & P & Q). split; auto. - split. apply bmatch_incr with bc; auto. apply bmatch_inv with m; auto. - intros. eapply Mem.loadbytes_unchanged_on_1. eapply external_call_readonly; eauto. - auto. intros; red. apply Q. + split. apply bmatch_incr with bc; auto. apply bmatch_ext with m; auto. + intros. eapply external_call_readonly with (m2 := m'); eauto. intros; red; intros; elim (Q ofs). eapply external_call_max_perm with (m2 := m'); eauto. destruct (j' b); congruence. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index c132ce7c..779e7bb9 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -3502,11 +3502,6 @@ Proof. - omegaContradiction. Qed. -Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8. -Proof. - destruct chunk; simpl; omega. -Qed. - Remark inval_before_contents: forall i c chunk' av' j, (inval_before i (i - 7) c)##j = Some (ACval chunk' av') -> diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 2942080b..b08c3ad7 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -460,6 +460,14 @@ Definition do_ef_free check (zlt 0 (Ptrofs.unsigned sz)); do m' <- Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz); Some(w, E0, Vundef, m') + | Vint n :: nil => + if Int.eq_dec n Int.zero && negb Archi.ptr64 + then Some(w, E0, Vundef, m) + else None + | Vlong n :: nil => + if Int64.eq_dec n Int64.zero && Archi.ptr64 + then Some(w, E0, Vundef, m) + else None | _ => None end. @@ -544,45 +552,51 @@ Proof with try congruence. - eapply do_external_function_sound; eauto. } destruct ef; simpl. -(* EF_external *) +- (* EF_external *) eapply do_external_function_sound; eauto. -(* EF_builtin *) +- (* EF_builtin *) eapply BF_EX; eauto. -(* EF_runtime *) +- (* EF_runtime *) eapply BF_EX; eauto. -(* EF_vload *) +- (* EF_vload *) unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... mydestr. destruct p as [[w'' t''] v]; mydestr. exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto. - auto. -(* EF_vstore *) +- (* EF_vstore *) unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs... mydestr. destruct p as [[w'' t''] m'']. mydestr. exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto. - auto. -(* EF_malloc *) +- (* EF_malloc *) unfold do_ef_malloc. destruct vargs... destruct vargs... mydestr. destruct (Mem.alloc m (- size_chunk Mptr) (Ptrofs.unsigned i)) as [m1 b] eqn:?. mydestr. split. apply SIZE in Heqo. subst v. econstructor; eauto. constructor. -(* EF_free *) - unfold do_ef_free. destruct vargs... destruct v... destruct vargs... - mydestr. split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega. constructor. -(* EF_memcpy *) +- (* EF_free *) + unfold do_ef_free. destruct vargs... destruct v... ++ destruct vargs... mydestr; InvBooleans; subst i. + replace (Vint Int.zero) with Vnullptr. split; constructor. + apply negb_true_iff in H0. unfold Vnullptr; rewrite H0; auto. ++ destruct vargs... mydestr; InvBooleans; subst i. + replace (Vlong Int64.zero) with Vnullptr. split; constructor. + unfold Vnullptr; rewrite H0; auto. ++ destruct vargs... mydestr. + split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega. + constructor. +- (* EF_memcpy *) unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... destruct v... destruct vargs... mydestr. apply Decidable_sound in Heqb1. red in Heqb1. split. econstructor; eauto; tauto. constructor. -(* EF_annot *) +- (* EF_annot *) unfold do_ef_annot. mydestr. split. constructor. apply list_eventval_of_val_sound; auto. econstructor. constructor; eauto. constructor. -(* EF_annot_val *) +- (* EF_annot_val *) unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr. split. constructor. apply eventval_of_val_sound; auto. econstructor. constructor; eauto. constructor. -(* EF_inline_asm *) +- (* EF_inline_asm *) eapply do_inline_assembly_sound; eauto. -(* EF_debug *) +- (* EF_debug *) unfold do_ef_debug. mydestr. split; constructor. Qed. @@ -605,37 +619,38 @@ Proof. - eapply do_external_function_complete; eauto. } destruct ef; simpl in *. -(* EF_external *) +- (* EF_external *) eapply do_external_function_complete; eauto. -(* EF_builtin *) +- (* EF_builtin *) eapply BF_EX; eauto. -(* EF_runtime *) +- (* EF_runtime *) eapply BF_EX; eauto. -(* EF_vload *) +- (* EF_vload *) inv H; unfold do_ef_volatile_load. exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto. -(* EF_vstore *) +- (* EF_vstore *) inv H; unfold do_ef_volatile_store. exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto. -(* EF_malloc *) +- (* EF_malloc *) inv H; unfold do_ef_malloc. inv H0. erewrite SIZE by eauto. rewrite H1, H2. auto. -(* EF_free *) +- (* EF_free *) inv H; unfold do_ef_free. - inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega. -(* EF_memcpy *) ++ inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega. ++ inv H0. unfold Vnullptr; destruct Archi.ptr64; auto. +- (* EF_memcpy *) inv H; unfold do_ef_memcpy. inv H0. rewrite Decidable_complete. rewrite H7; rewrite H8; auto. red. tauto. -(* EF_annot *) +- (* EF_annot *) inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. rewrite (list_eventval_of_val_complete _ _ _ H1). auto. -(* EF_annot_val *) +- (* EF_annot_val *) inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. rewrite (eventval_of_val_complete _ _ _ H1). auto. -(* EF_inline_asm *) +- (* EF_inline_asm *) eapply do_inline_assembly_complete; eauto. -(* EF_debug *) +- (* EF_debug *) inv H. inv H0. reflexivity. Qed. diff --git a/common/Events.v b/common/Events.v index 10e0c232..28bb992a 100644 --- a/common/Events.v +++ b/common/Events.v @@ -649,9 +649,12 @@ Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop := (** External call cannot modify memory unless they have [Max, Writable] permissions. *) ec_readonly: - forall ge vargs m1 t vres m2, + forall ge vargs m1 t vres m2 b ofs n bytes, sem ge vargs m1 t vres m2 -> - Mem.unchanged_on (loc_not_writable m1) m1 m2; + Mem.valid_block m1 b -> + Mem.loadbytes m2 b ofs n = Some bytes -> + (forall i, ofs <= i < ofs + n -> ~Mem.perm m1 b i Max Writable) -> + Mem.loadbytes m1 b ofs n = Some bytes; (** External calls must commute with memory extensions, in the following sense. *) @@ -784,7 +787,7 @@ Proof. (* max perms *) - inv H; auto. (* readonly *) -- inv H. apply Mem.unchanged_on_refl. +- inv H; auto. (* mem extends *) - inv H. inv H1. inv H6. inv H4. exploit volatile_load_extends; eauto. intros [v' [A B]]. @@ -833,14 +836,27 @@ Proof. rewrite C; auto. Qed. +Lemma unchanged_on_readonly: + forall m1 m2 b ofs n bytes, + Mem.unchanged_on (loc_not_writable m1) m1 m2 -> + Mem.valid_block m1 b -> + Mem.loadbytes m2 b ofs n = Some bytes -> + (forall i, ofs <= i < ofs + n -> ~Mem.perm m1 b i Max Writable) -> + Mem.loadbytes m1 b ofs n = Some bytes. +Proof. + intros. + rewrite <- H1. symmetry. + apply Mem.loadbytes_unchanged_on_1 with (P := loc_not_writable m1); auto. +Qed. + Lemma volatile_store_readonly: forall ge chunk1 m1 b1 ofs1 v t m2, volatile_store ge chunk1 m1 b1 ofs1 v t m2 -> Mem.unchanged_on (loc_not_writable m1) m1 m2. Proof. intros. inv H. - apply Mem.unchanged_on_refl. - eapply Mem.store_unchanged_on; eauto. +- apply Mem.unchanged_on_refl. +- eapply Mem.store_unchanged_on; eauto. exploit Mem.store_valid_access_3; eauto. intros [P Q]. intros. unfold loc_not_writable. red; intros. elim H2. apply Mem.perm_cur_max. apply P. auto. @@ -934,7 +950,7 @@ Proof. (* perms *) - inv H. inv H2. auto. eauto with mem. (* readonly *) -- inv H. eapply volatile_store_readonly; eauto. +- inv H. eapply unchanged_on_readonly; eauto. eapply volatile_store_readonly; eauto. (* mem extends*) - inv H. inv H1. inv H6. inv H7. inv H4. exploit volatile_store_extends; eauto. intros [m2' [A [B C]]]. @@ -994,7 +1010,7 @@ Proof. rewrite dec_eq_false. auto. apply Mem.valid_not_valid_diff with m1; eauto with mem. (* readonly *) -- inv H. eapply UNCHANGED; eauto. +- inv H. eapply unchanged_on_readonly; eauto. (* mem extends *) - inv H. inv H1. inv H7. assert (SZ: v2 = Vptrofs sz). @@ -1045,11 +1061,13 @@ Qed. Inductive extcall_free_sem (ge: Senv.t): list val -> mem -> trace -> val -> mem -> Prop := - | extcall_free_sem_intro: forall b lo sz m m', + | extcall_free_sem_ptr: forall b lo sz m m', Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr) = Some (Vptrofs sz) -> Ptrofs.unsigned sz > 0 -> Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz) = Some m' -> - extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'. + extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m' + | extcall_free_sem_null: forall m, + extcall_free_sem ge (Vnullptr :: nil) m E0 Vundef m. Lemma extcall_free_ok: extcall_properties extcall_free_sem @@ -1057,26 +1075,29 @@ Lemma extcall_free_ok: Proof. constructor; intros. (* well typed *) -- inv H. simpl. auto. +- inv H; simpl; auto. (* symbols preserved *) - inv H0; econstructor; eauto. (* valid block *) -- inv H. eauto with mem. +- inv H; eauto with mem. (* perms *) -- inv H. eapply Mem.perm_free_3; eauto. +- inv H; eauto using Mem.perm_free_3. (* readonly *) -- inv H. eapply Mem.free_unchanged_on; eauto. - intros. red; intros. elim H3. +- eapply unchanged_on_readonly; eauto. inv H. ++ eapply Mem.free_unchanged_on; eauto. + intros. red; intros. elim H6. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.free_range_perm; eauto. ++ apply Mem.unchanged_on_refl. (* mem extends *) -- inv H. inv H1. inv H8. inv H6. +- inv H. ++ inv H1. inv H8. inv H6. exploit Mem.load_extends; eauto. intros [v' [A B]]. assert (v' = Vptrofs sz). { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. } subst v'. exploit Mem.free_parallel_extends; eauto. intros [m2' [C D]]. - exists Vundef; exists m2'; intuition. + exists Vundef; exists m2'; intuition auto. econstructor; eauto. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_bounds; intros. @@ -1084,8 +1105,14 @@ Proof. { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.free_range_perm. eexact H4. eauto. } tauto. ++ inv H1. inv H5. replace v2 with Vnullptr. + exists Vundef; exists m1'; intuition auto. + constructor. + apply Mem.unchanged_on_refl. + unfold Vnullptr in *; destruct Archi.ptr64; inv H3; auto. (* mem inject *) -- inv H0. inv H2. inv H7. inv H9. +- inv H0. ++ inv H2. inv H7. inv H9. exploit Mem.load_inject; eauto. intros [v' [A B]]. assert (v' = Vptrofs sz). { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. } @@ -1099,7 +1126,7 @@ Proof. intro EQ. exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D). exists f, Vundef, m2'; split. - apply extcall_free_sem_intro with (sz := sz) (m' := m2'). + apply extcall_free_sem_ptr with (sz := sz) (m' := m2'). rewrite EQ. rewrite <- A. f_equal. omega. auto. auto. rewrite ! EQ. rewrite <- C. f_equal; omega. @@ -1112,14 +1139,19 @@ Proof. apply P. omega. split. auto. red; intros. congruence. ++ inv H2. inv H6. replace v' with Vnullptr. + exists f, Vundef, m1'; intuition auto using Mem.unchanged_on_refl. + constructor. + red; intros; congruence. + unfold Vnullptr in *; destruct Archi.ptr64; inv H4; auto. (* trace length *) - inv H; simpl; omega. (* receptive *) -- assert (t1 = t2). inv H; inv H0; auto. subst t2. +- assert (t1 = t2) by (inv H; inv H0; auto). subst t2. exists vres1; exists m1; auto. (* determ *) -- inv H; inv H0. - assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence. +- inv H; inv H0; try (unfold Vnullptr in *; destruct Archi.ptr64; discriminate). ++ assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence. assert (EQ2: sz0 = sz). { unfold Vptrofs in EQ1; destruct Archi.ptr64 eqn:SF. rewrite <- (Ptrofs.of_int64_to_int64 SF sz0), <- (Ptrofs.of_int64_to_int64 SF sz). congruence. @@ -1127,6 +1159,7 @@ Proof. } subst sz0. split. constructor. intuition congruence. ++ split. constructor. intuition auto. Qed. (** ** Semantics of [memcpy] operations. *) @@ -1159,8 +1192,9 @@ Proof. - (* perms *) intros. inv H. eapply Mem.perm_storebytes_2; eauto. - (* readonly *) - intros. inv H. eapply Mem.storebytes_unchanged_on; eauto. - intros; red; intros. elim H8. + intros. inv H. eapply unchanged_on_readonly; eauto. + eapply Mem.storebytes_unchanged_on; eauto. + intros; red; intros. elim H11. apply Mem.perm_cur_max. eapply Mem.storebytes_range_perm; eauto. - (* extensions *) intros. inv H. @@ -1271,7 +1305,7 @@ Proof. (* perms *) - inv H; auto. (* readonly *) -- inv H. apply Mem.unchanged_on_refl. +- inv H; auto. (* mem extends *) - inv H. exists Vundef; exists m1'; intuition. @@ -1316,7 +1350,7 @@ Proof. (* perms *) - inv H; auto. (* readonly *) -- inv H. apply Mem.unchanged_on_refl. +- inv H; auto. (* mem extends *) - inv H. inv H1. inv H6. exists v2; exists m1'; intuition. @@ -1359,7 +1393,7 @@ Proof. (* perms *) - inv H; auto. (* readonly *) -- inv H. apply Mem.unchanged_on_refl. +- inv H; auto. (* mem extends *) - inv H. exists Vundef; exists m1'; intuition. @@ -1406,7 +1440,7 @@ Proof. (* perms *) - inv H; auto. (* readonly *) -- inv H. apply Mem.unchanged_on_refl. +- inv H; auto. (* mem extends *) - inv H. fold bsem in H2. apply val_inject_list_lessdef in H1. specialize (bs_inject _ bsem _ _ _ H1). diff --git a/common/Memdata.v b/common/Memdata.v index f3016efe..a09b90f5 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -44,6 +44,13 @@ Definition size_chunk (chunk: memory_chunk) : Z := | Many64 => 8 end. +Definition largest_size_chunk := 8. + +Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8. +Proof. + destruct chunk; simpl; omega. +Qed. + Lemma size_chunk_pos: forall chunk, size_chunk chunk > 0. Proof. diff --git a/common/Memory.v b/common/Memory.v index f21d99af..cd8a2001 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -1307,6 +1307,23 @@ Proof. } Qed. +Section STOREV. +Variable chunk: memory_chunk. +Variable m1: mem. +Variables addr v: val. +Variable m2: mem. +Hypothesis STORE: storev chunk m1 addr v = Some m2. + + +Theorem loadv_storev_same: + loadv chunk m2 addr = Some (Val.load_result chunk v). +Proof. + destruct addr; simpl in *; try discriminate. + eapply load_store_same. + eassumption. +Qed. +End STOREV. + Lemma load_store_overlap: forall chunk m1 b ofs v m2 chunk' ofs' v', store chunk m1 b ofs v = Some m2 -> diff --git a/powerpc/Archi.v b/powerpc/Archi.v index ab348c14..10f38391 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -30,6 +30,10 @@ Definition align_float64 := 8%Z. (** Can we use the 64-bit extensions to the PowerPC architecture? *) Parameter ppc64 : bool. +(** Should single-precision FP arguments passed on stack be passed + as singles or use double FP format. *) +Parameter single_passed_as_single : bool. + Definition splitlong := negb ppc64. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. diff --git a/powerpc/CSE2deps.v b/powerpc/CSE2deps.v new file mode 100644 index 00000000..9db51bbb --- /dev/null +++ b/powerpc/CSE2deps.v @@ -0,0 +1,20 @@ +Require Import BoolEqual Coqlib. +Require Import AST Integers Floats. +Require Import Values Memory Globalenvs Events. +Require Import Op. + + +Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw := + (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk)) + && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk)) + && ((ofsw + size_chunk chunkw <=? ofsr) || + (ofsr + size_chunk chunkr <=? ofsw)). + +Definition may_overlap chunk addr args chunk' addr' args' := + match addr, addr', args, args' with + | (Aindexed ofs), (Aindexed ofs'), + (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 + end. diff --git a/powerpc/CSE2depsproof.v b/powerpc/CSE2depsproof.v new file mode 100644 index 00000000..2112a230 --- /dev/null +++ b/powerpc/CSE2depsproof.v @@ -0,0 +1,132 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE2 CSE2deps. +Require Import Lia. + +Lemma ptrofs_size : + Ptrofs.wordsize = 32%nat. +Proof. + unfold Ptrofs.wordsize. + unfold Wordsize_Ptrofs.wordsize. + trivial. +Qed. + +Lemma ptrofs_modulus : + Ptrofs.modulus = 4294967296. +Proof. + unfold Ptrofs.modulus. + rewrite ptrofs_size. + destruct Archi.ptr64; reflexivity. +Qed. + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Section MEMORY_WRITE. + Variable m m2 : mem. + Variable chunkw chunkr : memory_chunk. + Variable base : val. + + Variable addrw addrr valw valr : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + Hypothesis READ : Mem.loadv chunkr m addrr = Some valr. + + Section INDEXED_AWAY. + Variable ofsw ofsr : int. + Hypothesis ADDRW : eval_addressing genv sp + (Aindexed ofsw) (base :: nil) = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Aindexed ofsr) (base :: nil) = Some addrr. + + Lemma load_store_away1 : + forall RANGEW : 0 <= Int.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= Int.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : Int.unsigned ofsw + size_chunk chunkw <= Int.unsigned ofsr + \/ Int.unsigned ofsr + size_chunk chunkr <= Int.unsigned ofsw, + Mem.loadv chunkr m2 addrr = Some valr. + 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. + rewrite <- READ. + destruct base; 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 (Ptrofs.of_int ofsr)) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsw)) as [OFSW | OFSW]; + rewrite OFSW). + + all: try rewrite ptrofs_modulus in *. + + all: unfold Ptrofs.of_int. + + all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia). + all: intuition lia. + Qed. + + Theorem load_store_away : + can_swap_accesses_ofs (Int.unsigned ofsr) chunkr (Int.unsigned ofsw) chunkw = true -> + Mem.loadv chunkr m2 addrr = Some valr. + 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 load_store_away1. + all: tauto. + Qed. + End INDEXED_AWAY. +End MEMORY_WRITE. +End SOUNDNESS. + + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Lemma may_overlap_sound: + forall m m' : mem, + forall chunk addr args chunk' addr' args' v a a' vl rs, + (eval_addressing genv sp addr (rs ## args)) = Some a -> + (eval_addressing genv sp addr' (rs ## args')) = Some a' -> + (may_overlap chunk addr args chunk' addr' args') = false -> + (Mem.storev chunk m a v) = Some m' -> + (Mem.loadv chunk' m a') = Some vl -> + (Mem.loadv chunk' m' a') = Some vl. +Proof. + intros until rs. + intros ADDR ADDR' OVERLAP STORE LOAD. + destruct addr; destruct addr'; try discriminate. + { (* Aindexed / Aindexed *) + destruct args as [ | base [ | ]]. 1,3: discriminate. + destruct args' as [ | base' [ | ]]. 1,3: discriminate. + simpl in OVERLAP. + destruct (peq base base'). 2: discriminate. + subst base'. + destruct (can_swap_accesses_ofs (Int.unsigned i0) chunk' (Int.unsigned i) chunk) eqn:SWAP. + 2: discriminate. + simpl in *. + eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. + } +Qed. + +End SOUNDNESS. diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 1f048694..5c9cbd4f 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -208,7 +208,16 @@ Fixpoint loc_arguments_rec | Some ireg => One (R ireg) :: loc_arguments_rec tys (ir + 1) fr ofs end - | (Tfloat | Tsingle | Tany64) as ty :: tys => + | Tsingle as ty :: tys => + match list_nth_z float_param_regs fr with + | None => + let ty := if Archi.single_passed_as_single then Tsingle else Tany64 in + let ofs := align ofs (typesize ty) in + One (S Outgoing ofs ty) :: loc_arguments_rec tys ir fr (ofs + (typesize ty)) + | Some freg => + One (R freg) :: loc_arguments_rec tys ir (fr + 1) ofs + end + | (Tfloat | Tany64) as ty :: tys => match list_nth_z float_param_regs fr with | None => let ofs := align ofs 2 in @@ -295,12 +304,14 @@ Opaque list_nth_z. apply align_divides; omega. apply Z.divide_1_l. apply Z.divide_1_l. eapply Y; eauto. omega. - (* single *) + assert (ofs <= align ofs 1) by (apply align_le; omega). assert (ofs <= align ofs 2) by (apply align_le; omega). destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. apply Z.divide_1_l. - eapply Y; eauto. omega. + subst. split. destruct Archi.single_passed_as_single; simpl; omega. + destruct Archi.single_passed_as_single; simpl; apply Z.divide_1_l. + eapply Y; eauto. destruct Archi.single_passed_as_single; simpl; omega. - (* any32 *) destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H. subst. left. eapply list_nth_z_in; eauto. diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v index 7482435f..a3e945bf 100644 --- a/powerpc/extractionMachdep.v +++ b/powerpc/extractionMachdep.v @@ -34,3 +34,6 @@ Extract Constant Archi.ppc64 => | ""e5500"" -> true | _ -> false end". + +(* Choice of passing of single *) +Extract Constant Archi.single_passed_as_single => "Configuration.gnu_toolchain". diff --git a/riscV/CSE2deps.v b/riscV/CSE2deps.v new file mode 100644 index 00000000..8ab9242a --- /dev/null +++ b/riscV/CSE2deps.v @@ -0,0 +1,20 @@ +Require Import BoolEqual Coqlib. +Require Import AST Integers Floats. +Require Import Values Memory Globalenvs Events. +Require Import Op. + + +Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw := + (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk)) + && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk)) + && ((ofsw + size_chunk chunkw <=? ofsr) || + (ofsr + size_chunk chunkr <=? ofsw)). + +Definition may_overlap chunk addr args chunk' addr' args' := + match addr, addr', args, args' with + | (Aindexed ofs), (Aindexed ofs'), + (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 + end. diff --git a/riscV/CSE2depsproof.v b/riscV/CSE2depsproof.v new file mode 100644 index 00000000..ee500965 --- /dev/null +++ b/riscV/CSE2depsproof.v @@ -0,0 +1,129 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE2 CSE2deps. +Require Import Lia. + +Lemma ptrofs_size : + Ptrofs.wordsize = (if Archi.ptr64 then 64 else 32)%nat. +Proof. + unfold Ptrofs.wordsize. + unfold Wordsize_Ptrofs.wordsize. + trivial. +Qed. + +Lemma ptrofs_modulus : + Ptrofs.modulus = if Archi.ptr64 then 18446744073709551616 else 4294967296. +Proof. + unfold Ptrofs.modulus. + rewrite ptrofs_size. + destruct Archi.ptr64; reflexivity. +Qed. + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Section MEMORY_WRITE. + Variable m m2 : mem. + Variable chunkw chunkr : memory_chunk. + Variable base : val. + + Variable addrw addrr valw valr : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + Hypothesis READ : Mem.loadv chunkr m addrr = Some valr. + + Section INDEXED_AWAY. + Variable ofsw ofsr : ptrofs. + Hypothesis ADDRW : eval_addressing genv sp + (Aindexed ofsw) (base :: nil) = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Aindexed ofsr) (base :: nil) = Some addrr. + + Lemma 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 = Some valr. + 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. + rewrite <- READ. + destruct base; 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 load_store_away : + can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true -> + Mem.loadv chunkr m2 addrr = Some valr. + 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 load_store_away1. + all: tauto. + Qed. + End INDEXED_AWAY. +End MEMORY_WRITE. +End SOUNDNESS. + + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Lemma may_overlap_sound: + forall m m' : mem, + forall chunk addr args chunk' addr' args' v a a' vl rs, + (eval_addressing genv sp addr (rs ## args)) = Some a -> + (eval_addressing genv sp addr' (rs ## args')) = Some a' -> + (may_overlap chunk addr args chunk' addr' args') = false -> + (Mem.storev chunk m a v) = Some m' -> + (Mem.loadv chunk' m a') = Some vl -> + (Mem.loadv chunk' m' a') = Some vl. +Proof. + intros until rs. + intros ADDR ADDR' OVERLAP STORE LOAD. + destruct addr; destruct addr'; try discriminate. + { (* Aindexed / Aindexed *) + destruct args as [ | base [ | ]]. 1,3: discriminate. + destruct args' as [ | base' [ | ]]. 1,3: discriminate. + simpl 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. + simpl in *. + eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. + } +Qed. + +End SOUNDNESS. diff --git a/test/cse2/globals.c b/test/cse2/globals.c new file mode 100644 index 00000000..c6dd59cd --- /dev/null +++ b/test/cse2/globals.c @@ -0,0 +1,8 @@ +int glob1, glob2; + +void toto() { + if (glob1 > 4) { + glob2 ++; + glob1 --; + } +} diff --git a/test/cse2/indexed_addr.c b/test/cse2/indexed_addr.c new file mode 100644 index 00000000..30a7c571 --- /dev/null +++ b/test/cse2/indexed_addr.c @@ -0,0 +1,6 @@ +void foo(int *t) { + if (t[0] > 4) { + t[1] ++; + t[0] --; + } +} diff --git a/x86/CSE2deps.v b/x86/CSE2deps.v new file mode 100644 index 00000000..f4d9e254 --- /dev/null +++ b/x86/CSE2deps.v @@ -0,0 +1,24 @@ +Require Import BoolEqual Coqlib. +Require Import AST Integers Floats. +Require Import Values Memory Globalenvs Events. +Require Import Op. + +Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw := + (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk)) + && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk)) + && ((ofsw + size_chunk chunkw <=? ofsr) || + (ofsr + size_chunk chunkr <=? ofsw)). + +Definition may_overlap chunk addr args chunk' addr' args' := + match addr, addr', args, args' with + | (Aindexed ofs), (Aindexed ofs'), + (base :: nil), (base' :: nil) => + if peq base base' + then negb (can_swap_accesses_ofs ofs' chunk' ofs chunk) + else true + | (Aglobal symb ofs), (Aglobal symb' ofs'), nil, nil => + if peq symb symb' + then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) + else false + | _, _, _, _ => true + end. diff --git a/x86/CSE2depsproof.v b/x86/CSE2depsproof.v new file mode 100644 index 00000000..37e16dfe --- /dev/null +++ b/x86/CSE2depsproof.v @@ -0,0 +1,262 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE2 CSE2deps. +Require Import Lia. + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Section MEMORY_WRITE. + Variable m m2 : mem. + Variable chunkw chunkr : memory_chunk. + Variable base : val. + + Variable addrw addrr valw valr : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + Hypothesis READ : Mem.loadv chunkr m addrr = Some valr. + + Section INDEXED_AWAY. + Variable ofsw ofsr : Z. + Hypothesis ADDRW : eval_addressing genv sp + (Aindexed ofsw) (base :: nil) = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Aindexed ofsr) (base :: nil) = Some addrr. + + Lemma load_store_away1 : + forall RANGEW : 0 <= ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= ofsr <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : ofsw + size_chunk chunkw <= ofsr + \/ ofsr + size_chunk chunkr <= ofsw, + Mem.loadv chunkr m2 addrr = Some valr. + Proof. + intros. + + pose proof (max_size_chunk chunkr) as size_chunkr_bounded. + pose proof (max_size_chunk chunkw) as size_chunkw_bounded. + try change (Ptrofs.modulus - largest_size_chunk) with 4294967288 in *. + try change (Ptrofs.modulus - largest_size_chunk) with 18446744073709551608 in *. + destruct addrr ; simpl in * ; try discriminate. + unfold eval_addressing in *. + destruct Archi.ptr64 eqn:PTR64; destruct base; simpl in *; try discriminate. + rewrite PTR64 in *. + + inv ADDRR. + inv ADDRW. + rewrite <- READ. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int (Int.repr ofsr))) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int64 (Int64.repr ofsr))) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int (Int.repr ofsw))) as [OFSW | OFSW]; + rewrite OFSW). + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int64 (Int64.repr ofsw))) as [OFSW | OFSW]; + rewrite OFSW). + + all: unfold Ptrofs.of_int64. + all: unfold Ptrofs.of_int. + + + all: repeat rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia). + all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia). + all: repeat rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; lia). + all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 18446744073709551615; lia). + + all: try change Ptrofs.modulus with 4294967296. + all: try change Ptrofs.modulus with 18446744073709551616. + + all: intuition lia. + Qed. + + Theorem load_store_away : + can_swap_accesses_ofs ofsr chunkr ofsw chunkw = true -> + Mem.loadv chunkr m2 addrr = Some valr. + 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 load_store_away1. + all: tauto. + Qed. + End INDEXED_AWAY. + + Section DIFFERENT_GLOBALS. + Variable ofsw ofsr : ptrofs. + Hypothesis symw symr : ident. + Hypothesis ADDRW : eval_addressing genv sp + (Aglobal symw ofsw) nil = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Aglobal symr ofsr) nil = Some addrr. + + Lemma ptr64_cases: + forall {T : Type}, + forall b : bool, + forall x y : T, + (if b then (if b then x else y) else (if b then y else x)) = x. + Proof. + destruct b; reflexivity. + Qed. + + Lemma load_store_diff_globals : + symw <> symr -> + Mem.loadv chunkr m2 addrr = Some valr. + Proof. + intros. + unfold eval_addressing in *. + simpl in *. + rewrite ptr64_cases in ADDRR. + rewrite ptr64_cases in ADDRW. + unfold Genv.symbol_address in *. + unfold Genv.find_symbol in *. + destruct ((Genv.genv_symb genv) ! symw) as [bw |] eqn:SYMW; inv ADDRW. + 2: simpl in STORE; discriminate. + destruct ((Genv.genv_symb genv) ! symr) as [br |] eqn:SYMR; inv ADDRR. + 2: simpl in READ; discriminate. + assert (br <> bw). + { + intro EQ. + subst br. + assert (symr = symw). + { + eapply Genv.genv_vars_inj; eauto. + } + congruence. + } + rewrite <- READ. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := bw). + - exact STORE. + - left. assumption. + Qed. + End DIFFERENT_GLOBALS. + + Section SAME_GLOBALS. + Variable ofsw ofsr : ptrofs. + Hypothesis sym : ident. + Hypothesis ADDRW : eval_addressing genv sp + (Aglobal sym ofsw) nil = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Aglobal sym ofsr) nil = Some addrr. + + Lemma load_store_glob_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 = Some valr. + 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 size_chunkr_bounded, size_chunkw_bounded. + try change (Ptrofs.modulus - largest_size_chunk) with 4294967288 in *. + try change (Ptrofs.modulus - largest_size_chunk) with 18446744073709551608 in *. + unfold eval_addressing, eval_addressing32, eval_addressing64 in *. + destruct Archi.ptr64 eqn:PTR64. + + { + unfold Genv.symbol_address in *. + inv ADDRR. + inv ADDRW. + destruct (Genv.find_symbol genv sym). + 2: discriminate. + + rewrite <- READ. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + tauto. + } + + { + unfold Genv.symbol_address in *. + inv ADDRR. + inv ADDRW. + destruct (Genv.find_symbol genv sym). + 2: discriminate. + + rewrite <- READ. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + tauto. + } + Qed. + + Lemma load_store_glob_away : + (can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw) = true -> + Mem.loadv chunkr m2 addrr = Some valr. + 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 load_store_glob_away1. + all: tauto. + Qed. + End SAME_GLOBALS. +End MEMORY_WRITE. +End SOUNDNESS. + + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Lemma may_overlap_sound: + forall m m' : mem, + forall chunk addr args chunk' addr' args' v a a' vl rs, + (eval_addressing genv sp addr (rs ## args)) = Some a -> + (eval_addressing genv sp addr' (rs ## args')) = Some a' -> + (may_overlap chunk addr args chunk' addr' args') = false -> + (Mem.storev chunk m a v) = Some m' -> + (Mem.loadv chunk' m a') = Some vl -> + (Mem.loadv chunk' m' a') = Some vl. +Proof. + intros until rs. + intros ADDR ADDR' OVERLAP STORE LOAD. + destruct addr; destruct addr'; try discriminate. + { (* Aindexed / Aindexed *) + destruct args as [ | base [ | ]]. 1,3: discriminate. + destruct args' as [ | base' [ | ]]. 1,3: discriminate. + simpl in OVERLAP. + destruct (peq base base'). 2: discriminate. + subst base'. + destruct (can_swap_accesses_ofs z0 chunk' z chunk) eqn:SWAP. + 2: discriminate. + simpl in *. + eapply load_store_away; eassumption. + } + { (* Aglobal / Aglobal *) + destruct args. 2: discriminate. + destruct args'. 2: discriminate. + simpl in *. + destruct (peq i i1). + { + subst i1. + rewrite negb_false_iff in OVERLAP. + eapply load_store_glob_away; eassumption. + } + eapply load_store_diff_globals; eassumption. + } +Qed. + +End SOUNDNESS. |