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.

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

Feat: add overflow flags to lean semantics #471

Closed
wants to merge 9 commits into from
Closed

Feat: add overflow flags to lean semantics #471

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
d66a7b8
add flags
Jul 16, 2024
ce2e0d9
Make changes
Jul 17, 2024
5730a60
change syntax parser
Jul 17, 2024
3ad683a
add all overflow flags
Jul 17, 2024
7492a71
fix a bug
Jul 18, 2024
18b38fc
fix autogenerated messages
Jul 18, 2024
a203c33
please pass the github actions
Jul 18, 2024
65fd1d5
please work please work
Jul 18, 2024
b37e2f5
Merge remote-tracking branch 'origin/main' into feat/overflow_flags
tobiasgrosser Jul 23, 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
1 change: 1 addition & 0 deletions .gitattributes
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,2 +1,3 @@
SSA/Projects/InstCombine/tests/LLVM/** linguist-generated=true
SSA/Projects/InstCombine/all.lean linguist-generated=true
test/LLVMDialect/InstCombine/** linguist-generated=true
14 changes: 11 additions & 3 deletions SSA/Core/MLIRSyntax/GenericParser.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -548,8 +548,13 @@ syntax "@" ident : mlir_attr_val_symbol
syntax "@" str : mlir_attr_val_symbol
syntax "#" ident : mlir_attr_val -- alias
syntax "#" strLit : mlir_attr_val -- aliass

syntax "#" ident "<" strLit ">" : mlir_attr_val -- opaqueAttr
declare_syntax_cat dialect_attribute_contents
syntax mlir_attr_val : dialect_attribute_contents
syntax "(" dialect_attribute_contents + ")" : dialect_attribute_contents
syntax "[" dialect_attribute_contents + "]": dialect_attribute_contents
syntax "{" dialect_attribute_contents + "}": dialect_attribute_contents
-- syntax [^\[<({\]>)}\0]+ : dialect_attribute_contents
syntax "#" ident "<" dialect_attribute_contents ">" : mlir_attr_val -- opaqueAttr
syntax "#opaque<" ident "," strLit ">" ":" mlir_type : mlir_attr_val -- opaqueElementsAttr
syntax mlir_attr_val_symbol "::" mlir_attr_val_symbol : mlir_attr_val_symbol

Expand Down Expand Up @@ -595,7 +600,10 @@ macro_rules
| `([mlir_attr_val| # $dialect:ident < $opaqueData:str > ]) => do
let dialect := Lean.quote dialect.getId.toString
`(AttrValue.opaque_ $dialect $opaqueData)

| `([mlir_attr_val| # $dialect:ident < $opaqueData:ident > ]) => do
let d := Lean.quote dialect.getId.toString
let g : TSyntax `str := Lean.Syntax.mkStrLit (toString opaqueData.getId)
`(AttrValue.opaque_ $d $g)
macro_rules
| `([mlir_attr_val| #opaque< $dialect:ident, $opaqueData:str> : $t:mlir_type ]) => do
let dialect := Lean.quote dialect.getId.toString
Expand Down
4 changes: 4 additions & 0 deletions SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ import SSA.Projects.InstCombine.LLVM.PrettyEDSL
import SSA.Projects.InstCombine.Tactic
import SSA.Projects.InstCombine.TacticAuto
import SSA.Projects.InstCombine.ComWrappers
import SSA.Projects.InstCombine.LLVM.Semantics
import Mathlib.Tactic

open BitVec
Expand Down Expand Up @@ -134,6 +135,7 @@ def alive_simplifyMulDivRem805 (w : Nat) :
rw [LLVM.sdiv?_denom_zero_eq_none]
apply Refinement.none_left
case neg =>
simp
Copy link
Collaborator

Choose a reason for hiding this comment

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

non-terminal simp (if a simp is not the last element of a proof, it should be simp only to reduce chances of the proof breaking when the global simp-set changes, you can use simp? to "squeeze" the simp)

rw [BitVec.ult_toNat]
rw [BitVec.toNat_ofNat]
cases w'
Expand Down Expand Up @@ -227,6 +229,8 @@ def alive_simplifyMulDivRem805' (w : Nat) :
unfold MulDivRem805_lhs MulDivRem805_rhs
simp only [simp_llvm_wrap]
simp_alive_ssa
simp only [LLVM.add_reduce]
simp only [LLVM.sdiv_reduce]
simp_alive_undef
simp_alive_case_bash
simp only [ofInt_ofNat, add_eq, LLVM.icmp?_ult_eq]
Expand Down
129 changes: 66 additions & 63 deletions SSA/Projects/InstCombine/Base.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,18 +89,18 @@ deriving Repr, DecidableEq, Inhabited
/-- Homogeneous, binary operations -/
inductive MOp.BinaryOp : Type
| and
| or
| or (disjoint : Bool)
| xor
| shl
| lshr
| ashr
| shl (nsw : Bool) (nuw : Bool)
| lshr (exact : Bool)
| ashr (exact : Bool)
| urem
| srem
| add
| mul
| sub
| sdiv
| udiv
| add (nsw : Bool) (nuw : Bool)
| mul (nsw : Bool) (nuw : Bool)
| sub (nsw : Bool) (nuw : Bool)
| sdiv (exact : Bool)
| udiv (exact : Bool)
deriving Repr, DecidableEq, Inhabited

-- See: https://releases.llvm.org/14.0.0/docs/LangRef.html#bitwise-binary-operations
Expand All @@ -120,37 +120,37 @@ namespace MOp
@[match_pattern] def copy (w : Width φ) : MOp φ := .unary w .copy

@[match_pattern] def and (w : Width φ) : MOp φ := .binary w .and
@[match_pattern] def or (w : Width φ) : MOp φ := .binary w .or
@[match_pattern] def or (disjoint : Bool := false) (w : Width φ) : MOp φ := .binary w (.or disjoint)
@[match_pattern] def xor (w : Width φ) : MOp φ := .binary w .xor
@[match_pattern] def shl (w : Width φ) : MOp φ := .binary w .shl
@[match_pattern] def lshr (w : Width φ) : MOp φ := .binary w .lshr
@[match_pattern] def ashr (w : Width φ) : MOp φ := .binary w .ashr
@[match_pattern] def shl (nsw : Bool) (nuw : Bool) (w : Width φ) : MOp φ := .binary w (.shl nsw nuw)
@[match_pattern] def lshr (exact : Bool:= false) (w : Width φ) : MOp φ := .binary w (.lshr exact)
@[match_pattern] def ashr (exact : Bool:= false) (w : Width φ) : MOp φ := .binary w (.ashr exact)
@[match_pattern] def urem (w : Width φ) : MOp φ := .binary w .urem
@[match_pattern] def srem (w : Width φ) : MOp φ := .binary w .srem
@[match_pattern] def add (w : Width φ) : MOp φ := .binary w .add
@[match_pattern] def mul (w : Width φ) : MOp φ := .binary w .mul
@[match_pattern] def sub (w : Width φ) : MOp φ := .binary w .sub
@[match_pattern] def sdiv (w : Width φ) : MOp φ := .binary w .sdiv
@[match_pattern] def udiv (w : Width φ) : MOp φ := .binary w .udiv
@[match_pattern] def add (nsw : Bool:= false) (nuw : Bool:= false) (w : Width φ) : MOp φ := .binary w (.add nsw nuw)
@[match_pattern] def mul (nsw : Bool:= false) (nuw : Bool:= false) (w : Width φ) : MOp φ := .binary w (.mul nsw nuw)
@[match_pattern] def sub (nsw : Bool:= false) (nuw : Bool:= false) (w : Width φ) : MOp φ := .binary w (.sub nsw nuw)
@[match_pattern] def sdiv (exact : Bool:= false) (w : Width φ) : MOp φ := .binary w (.sdiv exact)
@[match_pattern] def udiv (exact : Bool:= false) (w : Width φ) : MOp φ := .binary w (.udiv exact)

/-- Recursion principle in terms of individual operations, rather than `unary` or `binary` -/
def deepCasesOn {motive : ∀ {φ}, MOp φ → Sort*}
(neg : ∀ {φ} {w : Width φ}, motive (neg w))
(not : ∀ {φ} {w : Width φ}, motive (not w))
(copy : ∀ {φ} {w : Width φ}, motive (copy w))
(and : ∀ {φ} {w : Width φ}, motive (and w))
(or : ∀ {φ} {w : Width φ}, motive (or w))
(or : ∀ {φ disjoint} {w : Width φ}, motive (or disjoint w))
(xor : ∀ {φ} {w : Width φ}, motive (xor w))
(shl : ∀ {φ} {w : Width φ}, motive (shl w))
(lshr : ∀ {φ} {w : Width φ}, motive (lshr w))
(ashr : ∀ {φ} {w : Width φ}, motive (ashr w))
(shl : ∀ {φ nsw nuw} {w : Width φ}, motive (shl nsw nuw w))
(lshr : ∀ {φ exact } {w : Width φ}, motive (lshr exact w))
(ashr : ∀ {φ exact } {w : Width φ}, motive (ashr exact w))
(urem : ∀ {φ} {w : Width φ}, motive (urem w))
(srem : ∀ {φ} {w : Width φ}, motive (srem w))
(add : ∀ {φ} {w : Width φ}, motive (add w))
(mul : ∀ {φ} {w : Width φ}, motive (mul w))
(sub : ∀ {φ} {w : Width φ}, motive (sub w))
(sdiv : ∀ {φ} {w : Width φ}, motive (sdiv w))
(udiv : ∀ {φ} {w : Width φ}, motive (udiv w))
(add : ∀ {φ nsw nuw} {w : Width φ}, motive (add nsw nuw w))
(mul : ∀ {φ nsw nuw} {w : Width φ}, motive (mul nsw nuw w))
(sub : ∀ {φ nsw nuw} {w : Width φ}, motive (sub nsw nuw w))
(sdiv : ∀ {φ exact } {w : Width φ}, motive (sdiv exact w))
(udiv : ∀ {φ exact } {w : Width φ}, motive (udiv exact w))
(select : ∀ {φ} {w : Width φ}, motive (select w))
(icmp : ∀ {φ c} {w : Width φ}, motive (icmp c w))
(const : ∀ {φ v} {w : Width φ}, motive (const w v)) :
Expand All @@ -159,18 +159,18 @@ def deepCasesOn {motive : ∀ {φ}, MOp φ → Sort*}
| _, .not _ => not
| _, .copy _ => copy
| _, .and _ => and
| _, .or _ => or
| _, .or _ _ => or
| _, .xor _ => xor
| _, .shl _ => shl
| _, .lshr _ => lshr
| _, .ashr _ => ashr
| _, .shl _ _ _ => shl
| _, .lshr _ _ => lshr
| _, .ashr _ _ => ashr
| _, .urem _ => urem
| _, .srem _ => srem
| _, .add _ => add
| _, .mul _ => mul
| _, .sub _ => sub
| _, .sdiv _ => sdiv
| _, .udiv _ => udiv
| n, .add nsw nuw w => @add n nsw nuw w
| _, .mul _ _ _ => mul
| _, .sub _ _ _ => sub
| _, .sdiv _ _ => sdiv
| _, .udiv _ _ => udiv
| _, .select _ => select
| _, .icmp .. => icmp
| _, .const .. => const
Expand All @@ -180,22 +180,22 @@ end MOp
instance : ToString (MOp φ) where
toString
| .and _ => "and"
| .or _ => "or"
| .or _ _ => "or"
| .not _ => "not"
| .xor _ => "xor"
| .shl _ => "shl"
| .lshr _ => "lshr"
| .ashr _ => "ashr"
| .shl _ _ _ => "shl"
| .lshr _ _ => "lshr"
| .ashr _ _ => "ashr"
| .urem _ => "urem"
| .srem _ => "srem"
| .select _ => "select"
| .add _ => "add"
| .mul _ => "mul"
| .sub _ => "sub"
| .add _ _ _ => "add"
| .mul _ _ _ => "mul"
| .sub _ _ _ => "sub"
| .neg _ => "neg"
| .copy _ => "copy"
| .sdiv _ => "sdiv"
| .udiv _ => "udiv"
| .sdiv _ _ => "sdiv"
| .udiv _ _ => "udiv"
| .icmp ty _ => s!"icmp {ty}"
| .const _ v => s!"const {v}"

Expand All @@ -207,22 +207,22 @@ namespace Op
@[match_pattern] abbrev binary (w : Nat) (op : MOp.BinaryOp) : Op := MOp.binary (.concrete w) op

@[match_pattern] abbrev and : Nat → Op := MOp.and ∘ .concrete
@[match_pattern] abbrev or : Nat → Op := MOp.or ∘ .concrete
@[match_pattern] abbrev or (disjoint : Bool) : Nat → Op := MOp.or disjoint ∘ .concrete
@[match_pattern] abbrev not : Nat → Op := MOp.not ∘ .concrete
@[match_pattern] abbrev xor : Nat → Op := MOp.xor ∘ .concrete
@[match_pattern] abbrev shl : Nat → Op := MOp.shl ∘ .concrete
@[match_pattern] abbrev lshr : Nat → Op := MOp.lshr ∘ .concrete
@[match_pattern] abbrev ashr : Nat → Op := MOp.ashr ∘ .concrete
@[match_pattern] abbrev shl (nsw nuw : Bool) : Nat → Op := MOp.shl nsw nuw ∘ .concrete
@[match_pattern] abbrev lshr (exact : Bool) : Nat → Op := MOp.lshr exact ∘ .concrete
@[match_pattern] abbrev ashr (exact : Bool) : Nat → Op := MOp.ashr exact ∘ .concrete
@[match_pattern] abbrev urem : Nat → Op := MOp.urem ∘ .concrete
@[match_pattern] abbrev srem : Nat → Op := MOp.srem ∘ .concrete
@[match_pattern] abbrev select : Nat → Op := MOp.select ∘ .concrete
@[match_pattern] abbrev add : Nat → Op := MOp.add ∘ .concrete
@[match_pattern] abbrev mul : Nat → Op := MOp.mul ∘ .concrete
@[match_pattern] abbrev sub : Nat → Op := MOp.sub ∘ .concrete
@[match_pattern] abbrev add (nuw : Bool := false) (nsw : Bool := false) : Nat → Op := (MOp.add nsw nuw) ∘ .concrete
@[match_pattern] abbrev mul (nsw nuw : Bool) : Nat → Op := MOp.mul nsw nuw ∘ .concrete
@[match_pattern] abbrev sub (nsw nuw : Bool) : Nat → Op := MOp.sub nsw nuw ∘ .concrete
@[match_pattern] abbrev neg : Nat → Op := MOp.neg ∘ .concrete
@[match_pattern] abbrev copy : Nat → Op := MOp.copy ∘ .concrete
@[match_pattern] abbrev sdiv : Nat → Op := MOp.sdiv ∘ .concrete
@[match_pattern] abbrev udiv : Nat → Op := MOp.udiv ∘ .concrete
@[match_pattern] abbrev sdiv (exact : Bool) : Nat → Op := MOp.sdiv exact ∘ .concrete
@[match_pattern] abbrev udiv (exact : Bool) : Nat → Op := MOp.udiv exact ∘ .concrete

@[match_pattern] abbrev icmp (c : IntPredicate) : Nat → Op := MOp.icmp c ∘ .concrete
@[match_pattern] abbrev const (w : Nat) (val : ℤ) : Op := MOp.const (.concrete w) val
Expand Down Expand Up @@ -269,20 +269,23 @@ def Op.denote (o : LLVM.Op) (op : HVector TyDenote.toType (DialectSignature.sig
| Op.not _ => LLVM.not (op.getN 0)
| Op.neg _ => LLVM.neg (op.getN 0)
| Op.and _ => LLVM.and (op.getN 0) (op.getN 1)
| Op.or _ => LLVM.or (op.getN 0) (op.getN 1)
| Op.or d _ => LLVM.or (op.getN 0) (op.getN 1) d
| Op.xor _ => LLVM.xor (op.getN 0) (op.getN 1)
| Op.shl _ => LLVM.shl (op.getN 0) (op.getN 1)
| Op.lshr _ => LLVM.lshr (op.getN 0) (op.getN 1)
| Op.ashr _ => LLVM.ashr (op.getN 0) (op.getN 1)
| Op.sub _ => LLVM.sub (op.getN 0) (op.getN 1)
| Op.add _ => LLVM.add (op.getN 0) (op.getN 1)
| Op.mul _ => LLVM.mul (op.getN 0) (op.getN 1)
| Op.sdiv _ => LLVM.sdiv (op.getN 0) (op.getN 1)
| Op.udiv _ => LLVM.udiv (op.getN 0) (op.getN 1)
| Op.shl nsw nuw _ => LLVM.shl (op.getN 0) (op.getN 1) { nsw := nsw , nuw := nuw}
| Op.lshr e _ => LLVM.lshr (op.getN 0) (op.getN 1)
| Op.ashr e _ => LLVM.ashr (op.getN 0) (op.getN 1)
| Op.sub nsw nuw _ => LLVM.sub (op.getN 0) (op.getN 1) { nsw := nsw , nuw := nuw}
| Op.add a b _ => LLVM.add (op.getN 0) (op.getN 1) {nsw := a, nuw := b}

-- | (@MOp.binary (ConcreteOrMVar.concrete _) (@MOp.BinaryOp.add true true)), _ => sorry
| Op.mul nsw nuw _ => LLVM.mul (op.getN 0) (op.getN 1) { nsw := nsw , nuw := nuw}
| Op.sdiv e _ => LLVM.sdiv (op.getN 0) (op.getN 1) {exact := e}
| Op.udiv e _ => LLVM.udiv (op.getN 0) (op.getN 1) {exact := e}
| Op.urem _ => LLVM.urem (op.getN 0) (op.getN 1)
| Op.srem _ => LLVM.srem (op.getN 0) (op.getN 1)
| Op.icmp c _ => LLVM.icmp c (op.getN 0) (op.getN 1)
| Op.select _ => LLVM.select (op.getN 0) (op.getN 1) (op.getN 2)
-- | (@MOp.binary (ConcreteOrMVar.concrete _) (@MOp.BinaryOp.add true false)), _ => sorry

instance : DialectDenote LLVM := ⟨
fun o args _ => Op.denote o args
Expand Down
18 changes: 9 additions & 9 deletions SSA/Projects/InstCombine/ComWrappers.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ def or {Γ : Ctxt _} (w : ℕ) (l r : Nat)
:= by get_elem_tactic) :
Expr InstCombine.LLVM Γ .pure (InstCombine.Ty.bitvec w) :=
Expr.mk
(op := InstCombine.MOp.or w)
(op := InstCombine.MOp.or false w)
(eff_le := by constructor)
(ty_eq := rfl)
(args := .cons ⟨l, lp⟩ <| .cons ⟨r, rp⟩ .nil)
Expand Down Expand Up @@ -93,7 +93,7 @@ def shl {Γ : Ctxt _} (w : ℕ) (l r : Nat)
:= by get_elem_tactic) :
Expr InstCombine.LLVM Γ .pure (InstCombine.Ty.bitvec w) :=
Expr.mk
(op := InstCombine.MOp.shl w)
(op := InstCombine.MOp.shl false false w)
(eff_le := by constructor)
(ty_eq := rfl)
(args := .cons ⟨l, lp⟩ <| .cons ⟨r, rp⟩ .nil)
Expand All @@ -107,7 +107,7 @@ def lshr {Γ : Ctxt _} (w : ℕ) (l r : Nat)
:= by get_elem_tactic) :
Expr InstCombine.LLVM Γ .pure (InstCombine.Ty.bitvec w) :=
Expr.mk
(op := InstCombine.MOp.lshr w)
(op := InstCombine.MOp.lshr false w)
(eff_le := by constructor)
(ty_eq := rfl)
(args := .cons ⟨l, lp⟩ <| .cons ⟨r, rp⟩ .nil)
Expand All @@ -121,7 +121,7 @@ def ashr {Γ : Ctxt _} (w : ℕ) (l r : Nat)
:= by get_elem_tactic) :
Expr InstCombine.LLVM Γ .pure (InstCombine.Ty.bitvec w) :=
Expr.mk
(op := InstCombine.MOp.ashr w)
(op := InstCombine.MOp.ashr false w)
(eff_le := by constructor)
(ty_eq := rfl)
(args := .cons ⟨l, lp⟩ <| .cons ⟨r, rp⟩ .nil)
Expand All @@ -135,7 +135,7 @@ def sub {Γ : Ctxt _} (w : ℕ) (l r : Nat)
:= by get_elem_tactic) :
Expr InstCombine.LLVM Γ .pure (InstCombine.Ty.bitvec w) :=
Expr.mk
(op := InstCombine.MOp.sub w)
(op := InstCombine.MOp.sub false false w)
(eff_le := by constructor)
(ty_eq := rfl)
(args := .cons ⟨l, lp⟩ <| .cons ⟨r, rp⟩ .nil)
Expand All @@ -149,7 +149,7 @@ def add {Γ : Ctxt _} (w : ℕ) (l r : Nat)
:= by get_elem_tactic) :
Expr InstCombine.LLVM Γ .pure (InstCombine.Ty.bitvec w) :=
Expr.mk
(op := InstCombine.MOp.add w)
(op := InstCombine.MOp.add false false w)
(eff_le := by constructor)
(ty_eq := rfl)
(args := .cons ⟨l, lp⟩ <| .cons ⟨r, rp⟩ .nil)
Expand All @@ -163,7 +163,7 @@ def mul {Γ : Ctxt _} (w : ℕ) (l r : Nat)
:= by get_elem_tactic) :
Expr InstCombine.LLVM Γ .pure (InstCombine.Ty.bitvec w) :=
Expr.mk
(op := InstCombine.MOp.mul w)
(op := InstCombine.MOp.mul false false w)
(eff_le := by constructor)
(ty_eq := rfl)
(args := .cons ⟨l, lp⟩ <| .cons ⟨r, rp⟩ .nil)
Expand All @@ -177,7 +177,7 @@ def sdiv {Γ : Ctxt _} (w : ℕ) (l r : Nat)
:= by get_elem_tactic) :
Expr InstCombine.LLVM Γ .pure (InstCombine.Ty.bitvec w) :=
Expr.mk
(op := InstCombine.MOp.sdiv w)
(op := InstCombine.MOp.sdiv false w)
(eff_le := by constructor)
(ty_eq := rfl)
(args := .cons ⟨l, lp⟩ <| .cons ⟨r, rp⟩ .nil)
Expand All @@ -191,7 +191,7 @@ def udiv {Γ : Ctxt _} (w : ℕ) (l r : Nat)
:= by get_elem_tactic) :
Expr InstCombine.LLVM Γ .pure (InstCombine.Ty.bitvec w) :=
Expr.mk
(op := InstCombine.MOp.udiv w)
(op := InstCombine.MOp.udiv false w)
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
(op := InstCombine.MOp.udiv false w)
(op := InstCombine.MOp.udiv false w)

(eff_le := by constructor)
(ty_eq := rfl)
(args := .cons ⟨l, lp⟩ <| .cons ⟨r, rp⟩ .nil)
Expand Down
Loading
Loading