diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-26 12:49:02 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-26 12:49:02 +0100 |
| commit | 95205e72ca536907fa89c7c884f0e22fc605063d (patch) | |
| tree | 4179d9ad8d7abdc7f40e6d35c30836393a07d253 /riscV/NeedOp.v | |
| parent | ca78138a8a81af44a36e339ad1ecf86ca3862e50 (diff) | |
| download | compcert-kvx-95205e72ca536907fa89c7c884f0e22fc605063d.tar.gz compcert-kvx-95205e72ca536907fa89c7c884f0e22fc605063d.zip | |
Adding more expansions, improving miniCSE, and tuning prepass
Diffstat (limited to 'riscV/NeedOp.v')
| -rw-r--r-- | riscV/NeedOp.v | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index 46d6ee73..4ed9868c 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -97,7 +97,10 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OEsltiuw _ => op1 (default nv) | OExoriw _ => op1 (bitwise nv) | OEluiw _ => op1 (default nv) - | OEaddiwr0 _ => op1 (default nv) (* TODO gourdinl modarith impossible? *) + | OEaddiw _ => op1 (default nv) + | OEaddiwr0 _ => op1 (default nv) + | OEandiw n => op1 (andimm nv n) + | OEoriw n => op1 (orimm nv n) | OEseql _ => op2 (default nv) | OEsnel _ => op2 (default nv) | OEsequl _ => op2 (default nv) @@ -108,9 +111,14 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OEsltiul _ => op1 (default nv) | OExoril _ => op1 (default nv) | OEluil _ => op1 (default nv) - | OEaddilr0 _ => op1 (default nv) (* TODO gourdinl modarith impossible? *) + | OEaddil _ => op1 (default nv) + | OEaddilr0 _ => op1 (default nv) + | OEandil _ => op1 (default nv) + | OEoril _ => op1 (default nv) | OEloadli _ => op1 (default nv) | OEmayundef _ => op2 (default nv) + | OEshrxundef _ => op2 (default nv) + | OEshrxlundef _ => op2 (default nv) | OEfeqd => op2 (default nv) | OEfltd => op2 (default nv) | OEfled => op2 (default nv) @@ -189,6 +197,16 @@ Proof. - apply shlimm_sound; auto. - apply shrimm_sound; auto. - apply shruimm_sound; auto. +- fold (Val.and (Vint n) v0); + fold (Val.and (Vint n) v2); + rewrite (Val.and_commut (Vint n) v0); + rewrite (Val.and_commut (Vint n) v2); + apply andimm_sound; auto. +- fold (Val.or (Vint n) v0); + fold (Val.or (Vint n) v2); + rewrite (Val.or_commut (Vint n) v0); + rewrite (Val.or_commut (Vint n) v2); + apply orimm_sound; auto. - apply xor_sound; auto with na. - (* selectl *) unfold ExtValues.select01_long. |