From b51cdb25e724d1958af97bd62c1a2c2b4f28c486 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Tue, 28 May 2024 10:42:30 +0100 Subject: [PATCH] feat: support fixed integers and conditions in meta-simp-set (#346) - add `ConcreteOrMVar.instantiate_ofNat_eq` to simplify instantiation and canonicalize to ofNat. Unfortunately, this seems to lead to a 'motive not type correct' error. To resolve it we use simp! that just unfolds. This should be debugged further: https://github.com/opencompl/ssa/issues/349. - generalize `toSnoc_toMap` to work on sequences of snoc --------- Co-authored-by: Siddharth --- SSA/Core/ErasedContext.lean | 2 +- SSA/Core/Util/ConcreteOrMVar.lean | 9 +- SSA/Projects/InstCombine/Tactic.lean | 4 +- SSA/Projects/InstCombine/Test.lean | 169 +++++++++++++++++++++++++++ 4 files changed, 180 insertions(+), 4 deletions(-) diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean index c0f088511..2e9aea2f1 100644 --- a/SSA/Core/ErasedContext.lean +++ b/SSA/Core/ErasedContext.lean @@ -143,7 +143,7 @@ def castCtxt {Γ : Ctxt Op} (h_eq : Γ = Δ) : Γ.Var ty → Δ.Var ty theorem toMap_last {Γ : Ctxt Ty} {t : Ty} : (Ctxt.Var.last Γ t).toMap = Ctxt.Var.last (Γ.map f) (f t) := rfl @[simp] -theorem toSnoc_toMap {Γ : Ctxt Ty} {t : Ty} {var : Ctxt.Var Γ t} {f : Ty → Ty₂} : +theorem toSnoc_toMap {Γ : Ctxt Ty} {t : Ty} {var : Ctxt.Var Γ t'} {f : Ty → Ty₂} : var.toSnoc.toMap (Γ := Γ.snoc t) (f := f) = var.toMap.toSnoc := rfl /-- This is an induction principle that case splits on whether or not a variable diff --git a/SSA/Core/Util/ConcreteOrMVar.lean b/SSA/Core/Util/ConcreteOrMVar.lean index 37cd85aaf..93ff0ec9c 100644 --- a/SSA/Core/Util/ConcreteOrMVar.lean +++ b/SSA/Core/Util/ConcreteOrMVar.lean @@ -48,9 +48,14 @@ def instantiate (as : Vector α φ) : ConcreteOrMVar α φ → α | .concrete w => w | .mvar i => as.get i +/-- We choose ConcreteOrMVar.concrete to be our simp normal form. -/ @[simp] -def instantiate_concrete_eq (as : Vector α φ) : - (ConcreteOrMVar.concrete w).instantiate as = w := by rfl +def ofNat_eq_concrete (x : Nat) : + (OfNat.ofNat x) = (ConcreteOrMVar.concrete x : ConcreteOrMVar Nat φ) := rfl + +@[simp] +def instantiate_ofNat_eq (as : Vector Nat φ) (x : Nat) : + ConcreteOrMVar.instantiate as (OfNat.ofNat x) = x := rfl @[simp] lemma instantiate_mvar_zero {hφ : List.length (w :: ws) = φ} {h0 : 0 < φ} : diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index 9985c185f..bdc93176a 100644 --- a/SSA/Projects/InstCombine/Tactic.lean +++ b/SSA/Projects/InstCombine/Tactic.lean @@ -42,10 +42,12 @@ macro "simp_alive_meta" : tactic => dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero] dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero'] dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero''] - dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_concrete_eq] dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate] dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.instantiateMTy] dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero''] + -- How can I avoid this `simp! only` and instead use a plain `simp only`? + dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.ofNat_eq_concrete] + simp! (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_ofNat_eq] ) ) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index cc1657f35..a20400870 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -386,3 +386,172 @@ def three_inst_macro_noreduc_proof (w : Nat) : simp_alive_meta simp_alive_ssa apply three_inst_stmt + +def one_inst_concrete_macro := + [alive_icom ()|{ + ^bb0(%arg0: i1): + %0 = "llvm.not" (%arg0) : (i1) -> (i1) + "llvm.return" (%0) : (i1) -> () + }] + +set_option ssa.alive_icom_reduce false in +def one_inst_concrete_macro_noreduce := + [alive_icom ()|{ + ^bb0(%arg0: i1): + %0 = "llvm.not" (%arg0) : (i1) -> (i1) + "llvm.return" (%0) : (i1) -> () + }] + +def one_inst_concrete_com : + Com InstCombine.LLVM [InstCombine.Ty.bitvec 1] .pure (InstCombine.Ty.bitvec 1) := + Com.lete (not 1 0) <| + Com.ret ⟨0, by simp [Ctxt.snoc]⟩ + +def one_inst_concrete_stmt : + @BitVec.Refinement (BitVec 1) (LLVM.not e) (LLVM.not e) := by + simp + +def one_inst_concrete_com_proof : + one_inst_concrete_com ⊑ one_inst_concrete_com := by + unfold one_inst_concrete_com + simp only [simp_llvm_wrap] + simp_alive_meta + simp_alive_ssa + apply one_inst_concrete_stmt + +def one_inst_concrete_macro_proof : + one_inst_concrete_macro ⊑ one_inst_concrete_macro := by + unfold one_inst_concrete_macro + simp_alive_meta + simp_alive_ssa + apply one_inst_concrete_stmt + +def one_inst_concrete_macro_proof_noreduce : + one_inst_concrete_macro_noreduce ⊑ one_inst_concrete_macro_noreduce := by + unfold one_inst_concrete_macro_noreduce + simp_alive_meta + simp_alive_ssa + apply one_inst_concrete_stmt + +def two_inst_concrete_macro := + [alive_icom ()|{ + ^bb0(%arg0: i1): + %0 = "llvm.not" (%arg0) : (i1) -> (i1) + %1 = "llvm.not" (%arg0) : (i1) -> (i1) + "llvm.return" (%0) : (i1) -> () + }] + +set_option ssa.alive_icom_reduce false in +def two_inst_concrete_macro_noreduce := + [alive_icom ()|{ + ^bb0(%arg0: i1): + %0 = "llvm.not" (%arg0) : (i1) -> (i1) + %1 = "llvm.not" (%arg0) : (i1) -> (i1) + "llvm.return" (%0) : (i1) -> () + }] + +def two_inst_concrete_com (w : ℕ) : + Com InstCombine.LLVM [InstCombine.Ty.bitvec w] .pure (InstCombine.Ty.bitvec w) := + Com.lete (not w 0) <| + Com.lete (not w 1) <| + Com.ret ⟨1, by simp [Ctxt.snoc]⟩ + +def two_inst_concrete_stmt (e : LLVM.IntW w) : + @BitVec.Refinement (BitVec w) (LLVM.not e) (LLVM.not e) := by + simp + +def two_inst_concrete_com_proof : + two_inst_concrete_com w ⊑ two_inst_concrete_com w := by + unfold two_inst_concrete_com + simp only [simp_llvm_wrap] + simp_alive_meta + simp_alive_ssa + apply two_inst_concrete_stmt + +def two_inst_concrete_macro_proof : + two_inst_concrete_macro ⊑ two_inst_concrete_macro := by + unfold two_inst_concrete_macro + simp_alive_meta + simp_alive_ssa + apply two_inst_concrete_stmt + +def two_inst_concrete_macro_noreduc_proof : + two_inst_concrete_macro_noreduce ⊑ two_inst_concrete_macro_noreduce := by + unfold two_inst_concrete_macro_noreduce + simp_alive_meta + simp_alive_ssa + apply two_inst_concrete_stmt + +def three_inst_concrete_macro := + [alive_icom ()|{ + ^bb0(%arg0: i1): + %0 = "llvm.not" (%arg0) : (i1) -> (i1) + %1 = "llvm.not" (%0) : (i1) -> (i1) + %2 = "llvm.not" (%1) : (i1) -> (i1) + "llvm.return" (%2) : (i1) -> () + }] + +set_option ssa.alive_icom_reduce false in +def three_inst_concrete_macro_noreduce := + [alive_icom ()|{ + ^bb0(%arg0: i1): + %0 = "llvm.not" (%arg0) : (i1) -> (i1) + %1 = "llvm.not" (%0) : (i1) -> (i1) + %2 = "llvm.not" (%1) : (i1) -> (i1) + "llvm.return" (%2) : (i1) -> () + }] + +def three_inst_concrete_com : + Com InstCombine.LLVM [InstCombine.Ty.bitvec 1] .pure (InstCombine.Ty.bitvec 1) := + Com.lete (not 1 0) <| + Com.lete (not 1 0) <| + Com.lete (not 1 0) <| + Com.ret ⟨0, by simp [Ctxt.snoc]⟩ + +def three_inst_concrete_stmt (e : LLVM.IntW 1) : + @BitVec.Refinement (BitVec 1) (LLVM.not (LLVM.not (LLVM.not e))) + (LLVM.not (LLVM.not (LLVM.not e))) := by + simp + +def three_inst_concrete_com_proof : + three_inst_concrete_com ⊑ three_inst_concrete_com := by + unfold three_inst_concrete_com + simp only [simp_llvm_wrap] + simp_alive_meta + simp_alive_ssa + apply three_inst_concrete_stmt + +def three_inst_concrete_macro_proof : + three_inst_concrete_macro ⊑ three_inst_concrete_macro := by + unfold three_inst_concrete_macro + simp_alive_meta + simp_alive_ssa + apply three_inst_concrete_stmt + +def three_inst_concrete_macro_noreduc_proof : + three_inst_concrete_macro_noreduce ⊑ three_inst_concrete_macro_noreduce := by + unfold three_inst_concrete_macro_noreduce + simp_alive_meta + simp_alive_ssa + apply three_inst_concrete_stmt + +set_option ssa.alive_icom_reduce false in +def two_ne_macro_noreduce (w : Nat) := + [alive_icom (w)|{ + ^bb0(%arg0: _, %arg1: _): + %0 = "llvm.icmp.ne" (%arg0, %arg1) : (_, _) -> (i1) + %1 = "llvm.icmp.ne" (%arg0, %arg1) : (_, _) -> (i1) + "llvm.return" (%1) : (i1) -> () + }] + +def two_ne_stmt (a b : LLVM.IntW w) : + @BitVec.Refinement (BitVec 1) (LLVM.icmp LLVM.IntPredicate.ne b a) + (LLVM.icmp LLVM.IntPredicate.ne b a) := by + simp + +def two_ne_macro_noreduc_proof (w : Nat) : + two_ne_macro_noreduce w ⊑ two_ne_macro_noreduce w := by + unfold two_ne_macro_noreduce + simp_alive_meta + simp_alive_ssa + apply two_ne_stmt