Skip to content
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.

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

feat: support fixed integers and conditions in meta-simp-set #346

Merged
merged 50 commits into from
May 28, 2024
Merged
Changes from 45 commits
Commits
Show all changes
50 commits
Select commit Hold shift + click to select a range
37f9bf4
feat: support short test case without a need for reduction
tobiasgrosser May 24, 2024
65675ca
feat: add lemmas
tobiasgrosser May 24, 2024
3a2c10d
Make one_inst_macro_proof_noreduce work
tobiasgrosser May 24, 2024
a70f2d7
Make this end deterministically
tobiasgrosser May 24, 2024
efaa153
generalize theorem thanks to Siddharth
tobiasgrosser May 24, 2024
24344e4
Add prefix
tobiasgrosser May 24, 2024
9c8f4c0
clean proof
tobiasgrosser May 24, 2024
a6b727e
Clean up noise
tobiasgrosser May 24, 2024
970f6f2
chore: do not pp proofs
tobiasgrosser May 24, 2024
5b1ff48
chore: use full context in simp_alive_meta
tobiasgrosser May 24, 2024
389bf83
:Merge branch 'chore_simp_alive_meta_full_ctxt' into disable_reduce_o…
tobiasgrosser May 24, 2024
e99012c
Merge remote-tracking branch 'origin/main' into disable_reduce_on_inst
tobiasgrosser May 24, 2024
00394fd
chore: drop unused things
tobiasgrosser May 24, 2024
56b396e
Update SSA/Core/Framework.lean
tobiasgrosser May 24, 2024
6d80b2e
Update SSA/Core/Framework.lean
tobiasgrosser May 24, 2024
140a063
Fix notation
tobiasgrosser May 24, 2024
cc9f587
feat: support equality-based rewriting for equation two operations
tobiasgrosser May 25, 2024
439c130
Merge remote-tracking branch 'origin/main' into disable_reduce_on_inst
tobiasgrosser May 25, 2024
9ad56a4
chore: ensuer that simplification works end-to-end. Now we need to cl…
tobiasgrosser May 25, 2024
9db80f6
cleanup
tobiasgrosser May 25, 2024
7b16657
fix build
tobiasgrosser May 25, 2024
605904d
fix build
tobiasgrosser May 25, 2024
bf48ddf
chore: make two operations work
tobiasgrosser May 25, 2024
7b9fa09
fix typo
tobiasgrosser May 25, 2024
4e0c666
chore: make all work
tobiasgrosser May 25, 2024
f90c5d3
Merge remote-tracking branch 'origin/main' into make_all_work
tobiasgrosser May 25, 2024
8ad4f25
WIP
tobiasgrosser May 25, 2024
fc37768
Drop set_option
tobiasgrosser May 25, 2024
f82125d
chore: try all of AliveAutoGenerated
tobiasgrosser May 26, 2024
3a7b5d9
minimized test case
tobiasgrosser May 26, 2024
0fbaf31
reduce test case
tobiasgrosser May 26, 2024
b97bdaf
WIP
tobiasgrosser May 26, 2024
42b9297
Merge remote-tracking branch 'origin/main' into all_of_alive_autogene…
tobiasgrosser May 26, 2024
4454b71
WIP
tobiasgrosser May 26, 2024
523c1dd
two more reduced test cases
tobiasgrosser May 26, 2024
36c78f0
make it work
tobiasgrosser May 26, 2024
15a08da
Remove diff on AliveAutoGenerated
tobiasgrosser May 26, 2024
c47e763
chore: fix toSnoc_toMap
tobiasgrosser May 26, 2024
b692c7b
remove unnecessary theorem
tobiasgrosser May 26, 2024
e3ef5db
fix typo
tobiasgrosser May 26, 2024
c100fe1
Fix the intro case
tobiasgrosser May 26, 2024
0ccf7d4
Merge remote-tracking branch 'origin/main' into all_of_alive_autogene…
tobiasgrosser May 26, 2024
e1b7bcf
improve formatting
tobiasgrosser May 26, 2024
6692809
chore: canonicalize to ConcreteOrMVar.concrete into OfNat.ofNat
tobiasgrosser May 27, 2024
ffa83ab
remove option
tobiasgrosser May 27, 2024
360d2ff
Merge remote-tracking branch 'origin/main' into all_of_alive_autogene…
tobiasgrosser May 27, 2024
2682651
Improve formatting
tobiasgrosser May 27, 2024
24f47c8
Improve formatting
tobiasgrosser May 27, 2024
ec9ba5d
Flip canonical form
tobiasgrosser May 27, 2024
8a7a6a8
Update SSA/Core/Util/ConcreteOrMVar.lean
tobiasgrosser May 28, 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
2 changes: 1 addition & 1 deletion SSA/Core/ErasedContext.lean
Original file line number Diff line number Diff line change
@@ -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
9 changes: 7 additions & 2 deletions SSA/Core/Util/ConcreteOrMVar.lean
Original file line number Diff line number Diff line change
@@ -48,9 +48,14 @@ def instantiate (as : Vector α φ) : ConcreteOrMVar α φ → α
| .concrete w => w
| .mvar i => as.get i

/-- We choose OfNat.ofNat to be our simp normal form. -/
tobiasgrosser marked this conversation as resolved.
Show resolved Hide resolved
@[simp]
def instantiate_concrete_eq (as : Vector α φ) :
(ConcreteOrMVar.concrete w).instantiate as = w := by rfl
def concrete_eq_ofNat (x : Nat) :
(ConcreteOrMVar.concrete x : ConcreteOrMVar Nat φ) = (OfNat.ofNat x) := 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 < φ} :
4 changes: 3 additions & 1 deletion SSA/Projects/InstCombine/Tactic.lean
Original file line number Diff line number Diff line change
@@ -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.concrete_eq_ofNat]
simp! (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_ofNat_eq]
)
)

165 changes: 165 additions & 0 deletions SSA/Projects/InstCombine/Test.lean
Original file line number Diff line number Diff line change
@@ -383,3 +383,168 @@ 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) :=
tobiasgrosser marked this conversation as resolved.
Show resolved Hide resolved
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
tobiasgrosser marked this conversation as resolved.
Show resolved Hide resolved
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