Llvm sem

SSA/Core/Util.lean

@@ -10,6 +10,12 @@ def pairBind [Monad m] (f : α → β → m γ) (pair : (m α × m β)) : m γ :
   let snd ← pair.snd
   f fst snd
 
+@[simp]
+def tripleBind [Monad m] (f : α → β → γ → m δ) (triple : (m α × m β × m γ)) : m δ := do
+  let (fstM,sndM,trdM) := triple
+  let (fst,snd,trd) := (← fstM,← sndM,← trdM)
+  f fst snd trd
+
 @[simp]
 def pairMapM [Monad m] (f : α → β → γ) (pair : (m α × m β)) : m γ := do
   let fst ← pair.fst
@@ -84,4 +90,4 @@ end LengthIndexedList
 elab "print_goal_as_error " : tactic => do
   let target ← Lean.Elab.Tactic.getMainTarget
   throwError target
-  pure ()
+  pure ()

SSA/Projects/InstCombine/AliveStatements.lean

@@ -2,9 +2,11 @@ import Std.Data.BitVec
 
 import SSA.Projects.InstCombine.TacticAuto
 import SSA.Projects.InstCombine.ForStd
+import SSA.Projects.InstCombine.LLVM.Semantics
 
 open Std
 open Std.BitVec
+open LLVM
 
 
 theorem bitvec_AddSub_1043 :

SSA/Projects/InstCombine/Base.lean

@@ -3,6 +3,7 @@ import SSA.Core.Framework
 import SSA.Core.Util
 import SSA.Core.Util.ConcreteOrMVar
 import SSA.Projects.InstCombine.ForStd
+import SSA.Projects.InstCombine.LLVM.Semantics
 
 /-!
   # InstCombine Dialect
@@ -24,33 +25,9 @@ namespace InstCombine
 
 open Std (BitVec)
 
-abbrev Width φ := ConcreteOrMVar Nat φ
+open LLVM
 
-inductive IntPredicate where
-  | eq
-  | ne
-  | ugt
-  | uge
-  | ult
-  | ule
-  | sgt
-  | sge
-  | slt
-  | sle
-deriving Inhabited, DecidableEq, Repr
-
-instance : ToString IntPredicate where
-  toString
-  | .eq => "eq"
-  | .ne => "ne"
-  | .ugt => "ugt"
-  | .uge => "uge"
-  | .ult => "ult"
-  | .ule => "ule"
-  | .sgt => "sgt"
-  | .sge => "sge"
-  | .slt => "slt"
-  | .sle => "sle"
+abbrev Width φ := ConcreteOrMVar Nat φ
 
 inductive MTy (φ : Nat)
   | bitvec (w : Width φ) : MTy φ
@@ -112,25 +89,25 @@ deriving Repr, DecidableEq, Inhabited
 
 instance : ToString (MOp φ) where
   toString
-  | .and w => "and"
-  | .or w => "or"
-  | .not w => "not"
-  | .xor w => "xor"
-  | .shl w => "shl"
-  | .lshr w => "lshr"
-  | .ashr w => "ashr"
-  | .urem w => "urem"
-  | .srem w => "srem"
-  | .select w => "select"
-  | .add w => "add"
-  | .mul w => "mul"
-  | .sub w => "sub"
-  | .neg w => "neg"
-  | .copy w => "copy"
-  | .sdiv w => "sdiv"
-  | .udiv w => "udiv"
-  | .icmp ty w => s!"icmp {ty}"
-  | .const w v => s!"const {v}"
+  | .and _ => "and"
+  | .or _ => "or"
+  | .not _ => "not"
+  | .xor _ => "xor"
+  | .shl _ => "shl"
+  | .lshr _ => "lshr"
+  | .ashr _ => "ashr"
+  | .urem _ => "urem"
+  | .srem _ => "srem"
+  | .select _ => "select"
+  | .add _ => "add"
+  | .mul _ => "mul"
+  | .sub _ => "sub"
+  | .neg _ => "neg"
+  | .copy _ => "copy"
+  | .sdiv _ => "sdiv"
+  | .udiv _ => "udiv"
+  | .icmp ty _ => s!"icmp {ty}"
+  | .const _ v => s!"const {v}"
 
 abbrev Op := MOp 0
 
@@ -189,35 +166,25 @@ instance : OpSignature (MOp φ) (MTy φ) where
 def Op.denote (o : Op) (arg : HVector Goedel.toType (OpSignature.sig o)) :
     (Goedel.toType <| OpSignature.outTy o) :=
   match o with
-  | Op.const w val => Option.some (BitVec.ofInt w val)
-  | Op.and _ => pairMapM (.&&&.) arg.toPair
-  | Op.or _ => pairMapM (.|||.) arg.toPair
-  | Op.xor _ => pairMapM (.^^^.) arg.toPair
-  | Op.shl _ => pairMapM (. <<< .) arg.toPair
-  | Op.lshr _ => pairMapM (. >>> .) arg.toPair
-  | Op.ashr _ => pairMapM (. >>>ₛ .) arg.toPair
-  | Op.sub _ => pairMapM (.-.) arg.toPair
-  | Op.add _ => pairMapM (.+.) arg.toPair
-  | Op.mul _ => pairMapM (.*.) arg.toPair
-  | Op.sdiv _ => pairBind BitVec.sdiv? arg.toPair
-  | Op.udiv _ => pairBind BitVec.udiv? arg.toPair
-  | Op.urem _ => pairBind BitVec.urem? arg.toPair
-  | Op.srem _ => pairBind BitVec.srem? arg.toPair
+  | Op.const _ val => const? val
+  | Op.and _ => pairBind and? arg.toPair
+  | Op.or _ => pairBind or? arg.toPair
+  | Op.xor _ => pairBind xor? arg.toPair
+  | Op.shl _ => pairBind shl? arg.toPair
+  | Op.lshr _ => pairBind lshr? arg.toPair
+  | Op.ashr _ => pairBind ashr? arg.toPair
+  | Op.sub _ => pairBind sub?  arg.toPair
+  | Op.add _ => pairBind add? arg.toPair
+  | Op.mul _ => pairBind mul? arg.toPair
+  | Op.sdiv _ => pairBind sdiv? arg.toPair
+  | Op.udiv _ => pairBind udiv? arg.toPair
+  | Op.urem _ => pairBind urem? arg.toPair
+  | Op.srem _ => pairBind srem? arg.toPair
   | Op.not _ => Option.map (~~~.) arg.toSingle
   | Op.copy _ => arg.toSingle
   | Op.neg _ => Option.map (-.) arg.toSingle
-  | Op.select _ => tripleMapM BitVec.select arg.toTriple
-  | Op.icmp c _ => match c with
-    | .eq => pairMapM (fun x y => ↑(x == y)) arg.toPair
-    | .ne => pairMapM (fun x y => ↑(x != y)) arg.toPair
-    | .sgt => pairMapM (. >ₛ .) arg.toPair
-    | .sge => pairMapM (. ≥ₛ .) arg.toPair
-    | .slt => pairMapM (. <ₛ .) arg.toPair
-    | .sle => pairMapM (. ≤ₛ .) arg.toPair
-    | .ugt => pairMapM (. >ᵤ .) arg.toPair
-    | .uge => pairMapM (. ≥ᵤ .) arg.toPair
-    | .ult => pairMapM (. <ᵤ .) arg.toPair
-    | .ule => pairMapM (. ≤ᵤ .) arg.toPair
+  | Op.select _ => tripleBind select? arg.toTriple
+  | Op.icmp c _ => pairBind (icmp? c) arg.toPair
 
 instance : OpDenote Op Ty := ⟨
   fun o args _ => Op.denote o args

SSA/Projects/InstCombine/ForStd.lean

@@ -24,12 +24,6 @@ instance {n} : ShiftRight (BitVec n) := ⟨fun x y => x >>> y.toNat⟩
 
 infixl:75 ">>>ₛ" => fun x y => BitVec.sshiftRight x (BitVec.toNat y)
 
-/--
- If the condition is an i1 and it evaluates to 1, the instruction returns the first value argument; otherwise, it returns the second value argument.
--/
-def select {w : Nat} (c : BitVec 1) (x y : BitVec w) : BitVec w :=
-  cond (c.toNat != 0) x y
-
 -- A lot of this should probably go to a differet file here and not Mathlib
 inductive Refinement {α : Type u} : Option α → Option α → Prop
   | bothSome {x y : α } : x = y → Refinement (some x) (some y)
@@ -73,74 +67,14 @@ instance {α : Type u} [DecidableEq α] : DecidableRel (@Refinement α) := by
 end Refinement
 
 infix:50 (priority:=low) " ⊑ " => Refinement
+instance : Coe Bool (BitVec 1) := ⟨ofBool⟩
 
-/--
-The value produced is the unsigned integer quotient of the two operands.
-Note that unsigned integer division and signed integer division are distinct operations; for signed integer division, use ‘sdiv’.
-Division by zero is undefined behavior.
--/
-def udiv? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
-  match y.toNat with
-    | 0 => none
-    | _ => some $ BitVec.ofNat w (x.toNat / y.toNat)
-
-/--
-The value produced is the signed integer quotient of the two operands rounded towards zero.
-Note that signed integer division and unsigned integer division are distinct operations; for unsigned integer division, use ‘udiv’.
-Division by zero is undefined behavior.
-Overflow also leads to undefined behavior; this is a rare case, but can occur, for example, by doing a 32-bit division of -2147483648 by -1.
--/
-def sdiv? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
-  if y.toInt = 0
-  then none
-  else
-    let div := (x.toInt / y.toInt)
-    if div < Int.ofNat (2^w)
-      then some $ BitVec.ofInt w div
-      else none
-
-/--
-This instruction returns the unsigned integer remainder of a division. This instruction always performs an unsigned division to get the remainder.
-Note that unsigned integer remainder and signed integer remainder are distinct operations; for signed integer remainder, use ‘srem’.
-Taking the remainder of a division by zero is undefined behavior.
--/
-def urem? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
-  if y.toNat = 0
-  then none
-  else some $ BitVec.ofNat w (x.toNat % y.toNat)
-
-def _root_.Int.rem (x y : Int) : Int :=
-  if x ≥ 0 then (x % y) else ((x % y) - y.natAbs)
-
--- TODO: prove this to make sure it's the right implementation!
-theorem _root_.Int.rem_sign_dividend :
-  ∀ x y, Int.rem x y < 0 ↔ x < 0 :=  by sorry
-
-/--
-This instruction returns the remainder of a division (where the result is either zero or has the same sign as the dividend, op1),
-not the modulo operator (where the result is either zero or has the same sign as the divisor, op2) of a value.
-For more information about the difference, see The Math Forum.
-For a table of how this is implemented in various languages, please see Wikipedia: modulo operation.
-Note that signed integer remainder and unsigned integer remainder are distinct operations; for unsigned integer remainder, use ‘urem’.
-Taking the remainder of a division by zero is undefined behavior.
-For vectors, if any element of the divisor is zero, the operation has undefined behavior.
-Overflow also leads to undefined behavior; this is a rare case, but can occur, for example,
-by taking the remainder of a 32-bit division of -2147483648 by -1.
-(The remainder doesn’t actually overflow, but this rule lets srem be implemented using instructions that return both the result
-of the division and the remainder.)
--/
-def srem? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
-  if y.toInt = 0
-  then none
-  else
-    let div := (x.toInt / y.toInt)
-    if div < Int.ofNat (2^w)
-      then some $ BitVec.ofInt w (x.toInt.rem y.toInt)
-      else none
+def coeWidth {m n : Nat} : BitVec m → BitVec n
+  | x => BitVec.ofNat n x.toNat
 
-instance : Coe Bool (BitVec 1) := ⟨ofBool⟩
+-- not sure what the right `Coe`is for this case
+-- See: https://leanprover-community.github.io/mathlib4_docs/Init/Coe.html#Important-typeclasses
+--instance {m n: Nat} : CoeTail (BitVec m) (BitVec n) := ⟨BitVec.coeWidth⟩
 
 instance decPropToBitvec1 (p : Prop) [Decidable p] : CoeDep Prop p (BitVec 1) where
   coe := ofBool $ decide p
-
-def sshr (a : BitVec n) (s : Nat) := BitVec.sshiftRight a s