Skip to content

Commit

Permalink
Merge pull request #518 from AbsInt/cse-alias
Browse files Browse the repository at this point in the history 
CSE: remember the abstract pointers in `Load` equations
  • Loading branch information
@xavierleroy
xavierleroy authored Aug 19, 2024
2 parents 62251c7 + 2458d07 commit 9e47293
Show file tree
Hide file tree
Showing 5 changed files with 264 additions and 149 deletions.
38 changes: 17 additions & 21 deletions backend/CSE.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ Fixpoint find_valnum_rhs (r: rhs) (eqs: list equation)
match eqs with
| nil => None
| Eq v str r' :: eqs1 =>
if str && eq_rhs r r' then Some v else find_valnum_rhs r eqs1
if str && compat_rhs r r' then Some v else find_valnum_rhs r eqs1
end.

(** [find_valnum_rhs' rhs eqs] is similar, but also accepts equations
Expand All @@ -88,7 +88,7 @@ Fixpoint find_valnum_rhs' (r: rhs) (eqs: list equation)
match eqs with
| nil => None
| Eq v str r' :: eqs1 =>
if eq_rhs r r' then Some v else find_valnum_rhs' r eqs1
if compat_rhs r r' then Some v else find_valnum_rhs' r eqs1
end.

(** [find_valnum_num vn eqs] searches the list of equations [eqs]
Expand Down Expand Up @@ -203,9 +203,9 @@ Definition add_op (n: numbering) (rd: reg) (op: operation) (rs: list reg) :=

Definition add_load (n: numbering) (rd: reg)
(chunk: memory_chunk) (addr: addressing)
(rs: list reg) :=
(rs: list reg) (p: aptr) :=
let (n1, vs) := valnum_regs n rs in
add_rhs n1 rd (Load chunk addr vs).
add_rhs n1 rd (Load chunk addr vs p).

(** [set_unknown n rd] returns a numbering where [rd] is mapped to
no value number, and no equations are added. This is useful
Expand Down Expand Up @@ -246,7 +246,7 @@ Definition kill_equations (pred: rhs -> bool) (n: numbering) : numbering :=
Definition filter_loads (r: rhs) : bool :=
match r with
| Op op _ => op_depends_on_memory op
| Load _ _ _ => true
| Load _ _ _ _ => true
end.

Definition kill_all_loads (n: numbering) : numbering :=
Expand All @@ -258,23 +258,19 @@ Definition kill_all_loads (n: numbering) : numbering :=
from this store are preserved. Equations involving memory-dependent
operators are also removed. *)

Definition filter_after_store (app: VA.t) (n: numbering) (p: aptr) (sz: Z) (r: rhs) :=
Definition filter_after_store (n: numbering) (p: aptr) (sz: Z) (r: rhs) :=
match r with
| Op op vl =>
op_depends_on_memory op
| Load chunk addr vl =>
match regs_valnums n vl with
| None => true
| Some rl =>
negb (pdisjoint (aaddressing app addr rl) (size_chunk chunk) p sz)
end
| Load chunk addr vl q =>
negb (pdisjoint q (size_chunk chunk) p sz)
end.

Definition kill_loads_after_store
(app: VA.t) (n: numbering)
(chunk: memory_chunk) (addr: addressing) (args: list reg) :=
let p := aaddressing app addr args in
kill_equations (filter_after_store app n p (size_chunk chunk)) n.
kill_equations (filter_after_store n p (size_chunk chunk)) n.

(** [add_store_result n chunk addr rargs rsrc] updates the numbering [n]
to reflect the knowledge gained after executing an instruction
Expand All @@ -298,7 +294,7 @@ Definition add_store_result (app: VA.t) (n: numbering) (chunk: memory_chunk) (ad
let (n1, vsrc) := valnum_reg n rsrc in
let (n2, vargs) := valnum_regs n1 rargs in
{| num_next := n2.(num_next);
num_eqs := Eq vsrc false (Load chunk addr vargs) :: n2.(num_eqs);
num_eqs := Eq vsrc false (Load chunk addr vargs (aaddressing app addr rargs)) :: n2.(num_eqs);
num_reg := n2.(num_reg);
num_val := n2.(num_val) |}
else n.
Expand All @@ -310,8 +306,8 @@ Definition add_store_result (app: VA.t) (n: numbering) (chunk: memory_chunk) (ad
operators are also removed. *)

Definition kill_loads_after_storebytes
(app: VA.t) (n: numbering) (dst: aptr) (sz: Z) :=
kill_equations (filter_after_store app n dst sz) n.
(n: numbering) (dst: aptr) (sz: Z) :=
kill_equations (filter_after_store n dst sz) n.

(** [add_memcpy app n1 n2 rsrc rdst sz] adds equations to [n2] that
represent the effect of a [memcpy] block copy operation of [sz] bytes
Expand All @@ -327,15 +323,15 @@ Definition kill_loads_after_storebytes

Definition shift_memcpy_eq (src sz delta: Z) (e: equation) :=
match e with
| Eq l strict (Load chunk (Ainstack i) _) =>
| Eq l strict (Load chunk (Ainstack i) _ _) =>
let i := Ptrofs.unsigned i in
let j := i + delta in
if zle src i
&& zle (i + size_chunk chunk) (src + sz)
&& zeq (Z.modulo delta (align_chunk chunk)) 0
&& zle 0 j
&& zle j Ptrofs.max_unsigned
then Some(Eq l strict (Load chunk (Ainstack (Ptrofs.repr j)) nil))
then Some(Eq l strict (Load chunk (Ainstack (Ptrofs.repr j)) nil (Stk (Ptrofs.repr j))))
else None
| _ => None
end.
Expand Down Expand Up @@ -461,7 +457,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
| Iop op args res s =>
add_op before res op args
| Iload chunk addr args dst s =>
add_load before dst chunk addr args
add_load before dst chunk addr args (aaddressing approx!!pc addr args)
| Istore chunk addr args src s =>
let app := approx!!pc in
let n := kill_loads_after_store app before chunk addr args in
Expand All @@ -487,7 +483,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
let app := approx!!pc in
let adst := aaddr_arg app dst in
let asrc := aaddr_arg app src in
let n := kill_loads_after_storebytes app before adst sz in
let n := kill_loads_after_storebytes before adst sz in
set_res_unknown (add_memcpy before n asrc adst sz) res
| _ =>
empty_numbering
Expand Down Expand Up @@ -537,7 +533,7 @@ Definition transf_instr (n: numbering) (instr: instruction) :=
end
| Iload chunk addr args dst s =>
let (n1, vl) := valnum_regs n args in
match find_rhs n1 (Load chunk addr vl) with
match find_rhs n1 (Load chunk addr vl Ptop) with
| Some r =>
Iop Omove (r :: nil) dst s
| None =>
Expand Down
63 changes: 58 additions & 5 deletions backend/CSEdomain.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
Require Import Coqlib Maps.
Require Import AST Integers Values Memory.
Require Import Op Registers RTL.
Require Import ValueDomain.

(** Value numbers are represented by positive integers. Equations are
of the form [valnum = rhs] or [valnum >= rhs], where the right-hand
Expand All @@ -27,7 +28,7 @@ Definition valnum := positive.

Inductive rhs : Type :=
| Op: operation -> list valnum -> rhs
| Load: memory_chunk -> addressing -> list valnum -> rhs.
| Load: memory_chunk -> addressing -> list valnum -> aptr -> rhs.

Inductive equation : Type :=
| Eq (v: valnum) (strict: bool) (r: rhs).
Expand All @@ -38,10 +39,39 @@ Definition eq_list_valnum: forall (x y: list valnum), {x=y}+{x<>y} := list_eq_de

Definition eq_rhs (x y: rhs) : {x=y}+{x<>y}.
Proof.
generalize chunk_eq eq_operation eq_addressing eq_valnum eq_list_valnum.
generalize chunk_eq eq_operation eq_addressing eq_valnum eq_list_valnum eq_aptr.
decide equality.
Defined.

(** Equality of [rhs] up to differences in regions attached to [Load] rhs. *)

Inductive rhs_compat: rhs -> rhs -> Prop :=
| rhs_compat_op: forall op vl,
rhs_compat (Op op vl) (Op op vl)
| rhs_compat_load: forall chunk addr vl p1 p2,
rhs_compat (Load chunk addr vl p1) (Load chunk addr vl p2).

Lemma rhs_compat_sym: forall rh1 rh2,
rhs_compat rh1 rh2 -> rhs_compat rh2 rh1.
Proof.
destruct 1; constructor; auto.
Qed.

Definition compat_rhs (r1 r2: rhs) : bool :=
match r1, r2 with
| Op op1 vl1, Op op2 vl2 => eq_operation op1 op2 && eq_list_valnum vl1 vl2
| Load chunk1 addr1 vl1 p1, Load chunk2 addr2 vl2 p2 =>
chunk_eq chunk1 chunk2 && eq_addressing addr1 addr2 && eq_list_valnum vl1 vl2
| _, _ => false
end.

Lemma compat_rhs_sound: forall r1 r2,
compat_rhs r1 r2 = true -> rhs_compat r1 r2.
Proof.
unfold compat_rhs; intros; destruct r1, r2; try discriminate;
InvBooleans; subst; constructor.
Qed.

(** A value numbering is a collection of equations between value numbers
plus a partial map from registers to value numbers. Additionally,
we maintain the next unused value number, so as to easily generate
Expand Down Expand Up @@ -69,7 +99,7 @@ Definition empty_numbering :=
Definition valnums_rhs (r: rhs): list valnum :=
match r with
| Op op vl => vl
| Load chunk addr vl => vl
| Load chunk addr vl ap => vl
end.

Definition wf_rhs (next: valnum) (r: rhs) : Prop :=
Expand Down Expand Up @@ -101,18 +131,41 @@ Inductive rhs_eval_to (valu: valuation) (ge: genv) (sp: val) (m: mem):
| op_eval_to: forall op vl v,
eval_operation ge sp op (map valu vl) m = Some v ->
rhs_eval_to valu ge sp m (Op op vl) v
| load_eval_to: forall chunk addr vl a v,
| load_eval_to: forall chunk addr vl a v p,
eval_addressing ge sp addr (map valu vl) = Some a ->
Mem.loadv chunk m a = Some v ->
rhs_eval_to valu ge sp m (Load chunk addr vl) v.
rhs_eval_to valu ge sp m (Load chunk addr vl p) v.

Lemma rhs_eval_to_compat: forall valu ge sp m rh v rh',
rhs_eval_to valu ge sp m rh v ->
rhs_compat rh rh' ->
rhs_eval_to valu ge sp m rh' v.
Proof.
intros. inv H; inv H0; econstructor; eauto.
Qed.

(** A [Load] equation carries a region (abstract pointer) [p],
characterizing which part of memory is being read.
The following predicate makes sure the actual address
belongs to the given region. *)

Inductive rhs_valid (valu: valuation) (ge: genv): val -> rhs -> Prop :=
| op_valid: forall sp op vl,
rhs_valid valu ge sp (Op op vl)
| load_valid: forall sp chunk addr vl p b ofs bc,
eval_addressing ge (Vptr sp Ptrofs.zero) addr (map valu vl) = Some (Vptr b ofs) ->
pmatch bc b ofs p -> genv_match bc ge -> bc sp = BCstack ->
rhs_valid valu ge (Vptr sp Ptrofs.zero) (Load chunk addr vl p).

Inductive equation_holds (valu: valuation) (ge: genv) (sp: val) (m: mem):
equation -> Prop :=
| eq_holds_strict: forall l r,
rhs_eval_to valu ge sp m r (valu l) ->
rhs_valid valu ge sp r ->
equation_holds valu ge sp m (Eq l true r)
| eq_holds_lessdef: forall l r v,
rhs_eval_to valu ge sp m r v -> Val.lessdef v (valu l) ->
rhs_valid valu ge sp r ->
equation_holds valu ge sp m (Eq l false r).

Record numbering_holds (valu: valuation) (ge: genv) (sp: val)
Expand Down
Loading

0 comments on commit 9e47293

Please sign in to comment.