Skip to content

CSE: remember the abstract pointers in Load equations #518

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
xavierleroy merged 3 commits into from
Aug 19, 2024
+264 −149
Merged

CSE: remember the abstract pointers in Load equations #518

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8657787
Update test suite
xavierleroy Aug 12, 2024
08851d2
Stronger result about the nonaliasing test `pdisjoint`
xavierleroy Aug 12, 2024
2458d07
CSE: remember the abstract pointers in Load equations
xavierleroy Aug 12, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
38 changes: 17 additions & 21 deletions backend/CSE.v
View file
Open in desktop
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
Copy link
Copy Markdown
Contributor Author

@xavierleroy xavierleroy Aug 19, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could probably take the glb (intersection) of the abstract pointers in r and r', as it seems that both abstract pointers are valid. But I'm not expecting any significant precision gain from that, so let's keep it for future work.

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
Open in desktop
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