From 686f0aaff7a4c37e13bfbe823b4dd2a879556f0a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 4 Sep 2019 06:55:27 +0200 Subject: begin CSE --- backend/CSE.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'backend/CSE.v') diff --git a/backend/CSE.v b/backend/CSE.v index 9da30f50..1c884cf0 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -202,10 +202,10 @@ Definition add_op (n: numbering) (rd: reg) (op: operation) (rs: list reg) := and added to [n] as described in [add_rhs]. *) Definition add_load (n: numbering) (rd: reg) - (chunk: memory_chunk) (addr: addressing) + (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (rs: list reg) := let (n1, vs) := valnum_regs n rs in - add_rhs n1 rd (Load chunk addr vs). + add_rhs n1 rd (Load trap chunk addr vs). (** [set_unknown n rd] returns a numbering where [rd] is mapped to no value number, and no equations are added. This is useful @@ -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 := @@ -262,7 +262,7 @@ Definition filter_after_store (app: VA.t) (n: numbering) (p: aptr) (sz: Z) (r: r match r with | Op op vl => op_depends_on_memory op - | Load chunk addr vl => + | Load trap chunk addr vl => match regs_valnums n vl with | None => true | Some rl => @@ -297,7 +297,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 TRAP chunk addr vargs) :: n2.(num_eqs); num_reg := n2.(num_reg); num_val := n2.(num_val) |} else n. @@ -326,7 +326,7 @@ 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 trap chunk (Ainstack i) _) => let i := Ptrofs.unsigned i in let j := i + delta in if zle src i @@ -334,7 +334,7 @@ Definition shift_memcpy_eq (src sz delta: Z) (e: equation) := && 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 trap chunk (Ainstack (Ptrofs.repr j)) nil)) else None | _ => None end. @@ -460,7 +460,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 trap chunk addr args dst s => - add_load before dst chunk addr args + add_load before dst trap chunk 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 @@ -536,7 +536,7 @@ Definition transf_instr (n: numbering) (instr: instruction) := end | Iload trap 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 trap chunk addr vl) with | Some r => Iop Omove (r :: nil) dst s | None => -- cgit