def LLVM.IntW (w : ℕ) : Type

Equations

• LLVM.IntW w = Option (BitVec w)

def LLVM.and? {w : ℕ} (x : BitVec w) (y : BitVec w) : LLVM.IntW w

The ‘and’ instruction returns the bitwise logical and of its two operands.

Equations

• LLVM.and? x y = pure (x &&& y)

theorem LLVM.and?_eq : ∀ {w : ℕ} {a b : BitVec w}, LLVM.and? a b = some (a.and b)

def LLVM.and {w : ℕ} (x : LLVM.IntW w) (y : LLVM.IntW w) : LLVM.IntW w

Equations

• LLVM.and x y = do let x' ← x let y' ← y LLVM.and? x' y'

def LLVM.or? {w : ℕ} (x : BitVec w) (y : BitVec w) : LLVM.IntW w

The ‘or’ instruction returns the bitwise logical inclusive or of its two operands.

Equations

• LLVM.or? x y = pure (x ||| y)

theorem LLVM.or?_eq : ∀ {w : ℕ} {a b : BitVec w}, LLVM.or? a b = some (a.or b)

structure LLVM.DisjointFlag : Type

• disjoint : Bool

instance LLVM.instReprDisjointFlag : Repr LLVM.DisjointFlag

Equations

• LLVM.instReprDisjointFlag = { reprPrec := LLVM.reprDisjointFlag✝ }

instance LLVM.instDecidableEqDisjointFlag : DecidableEq LLVM.DisjointFlag

Equations

• LLVM.instDecidableEqDisjointFlag = LLVM.decEqDisjointFlag✝

def LLVM.or {w : ℕ} (x : LLVM.IntW w) (y : LLVM.IntW w) (flag : optParam LLVM.DisjointFlag { disjoint := false }) : LLVM.IntW w

Equations

• LLVM.or x y flag = do let x' ← x let y' ← y if flag.disjoint = true ∧ (x' &&& y' != 0) = true then none else LLVM.or? x' y'

def LLVM.xor? {w : ℕ} (x : BitVec w) (y : BitVec w) : LLVM.IntW w

The ‘xor’ instruction returns the bitwise logical exclusive or of its two operands. The xor is used to implement the “one’s complement” operation, which is the “~” operator in C.

Equations

• LLVM.xor? x y = pure (x ^^^ y)

theorem LLVM.xor?_eq : ∀ {w : ℕ} {a b : BitVec w}, LLVM.xor? a b = some (a.xor b)

def LLVM.xor {w : ℕ} (x : LLVM.IntW w) (y : LLVM.IntW w) : LLVM.IntW w

Equations

• LLVM.xor x y = do let x' ← x let y' ← y LLVM.xor? x' y'

def LLVM.add? {w : ℕ} (x : BitVec w) (y : BitVec w) : LLVM.IntW w

The value produced is the integer sum of the two operands. If the sum has unsigned overflow, the result returned is the mathematical result modulo 2n, where n is the bit width of the result. Because LLVM integers use a two’s complement representation, this instruction is appropriate for both signed and unsigned integers.

Equations

• LLVM.add? x y = pure (x + y)

theorem LLVM.add?_eq : ∀ {w : ℕ} {a b : BitVec w}, LLVM.add? a b = some (a.add b)

structure LLVM.NoWrapFlags : Type

• nsw : Bool
• nuw : Bool

instance LLVM.instReprNoWrapFlags : Repr LLVM.NoWrapFlags

Equations

• LLVM.instReprNoWrapFlags = { reprPrec := LLVM.reprNoWrapFlags✝ }

instance LLVM.instDecidableEqNoWrapFlags : DecidableEq LLVM.NoWrapFlags

Equations

• LLVM.instDecidableEqNoWrapFlags = LLVM.decEqNoWrapFlags✝

def LLVM.add {w : ℕ} (x : LLVM.IntW w) (y : LLVM.IntW w) (flags : optParam LLVM.NoWrapFlags { nsw := false, nuw := false }) : LLVM.IntW w

Equations

• One or more equations did not get rendered due to their size.

def LLVM.sub? {w : ℕ} (x : BitVec w) (y : BitVec w) : LLVM.IntW w

The value produced is the integer difference of the two operands. If the difference has unsigned overflow, the result returned is the mathematical result modulo 2n, where n is the bit width of the result. Because LLVM integers use a two’s complement representation, this instruction is appropriate for both signed and unsigned integers.

Equations

• LLVM.sub? x y = pure (x - y)

theorem LLVM.sub?_eq : ∀ {w : ℕ} {a b : BitVec w}, LLVM.sub? a b = some (a.sub b)

def LLVM.sub {w : ℕ} (x : LLVM.IntW w) (y : LLVM.IntW w) (flags : optParam LLVM.NoWrapFlags { nsw := false, nuw := false }) : LLVM.IntW w

Equations

• One or more equations did not get rendered due to their size.

def LLVM.mul? {w : ℕ} (x : BitVec w) (y : BitVec w) : LLVM.IntW w

The value produced is the integer product of the two operands. If the result of the multiplication has unsigned overflow, the result returned is the mathematical result modulo 2n, where n is the bit width of the result. Because LLVM integers use a two’s complement representation, and the result is the same width as the operands, this instruction returns the correct result for both signed and unsigned integers.

If a full product (e.g. i32 * i32 -> i64) is needed, the operands should be sign-extended or zero-extended as appropriate to the width of the full product.

Equations

• LLVM.mul? x y = pure (x * y)

theorem LLVM.mul?_eq : ∀ {w : ℕ} {a b : BitVec w}, LLVM.mul? a b = some (a.mul b)

def LLVM.mul {w : ℕ} (x : LLVM.IntW w) (y : LLVM.IntW w) (flags : optParam LLVM.NoWrapFlags { nsw := false, nuw := false }) : LLVM.IntW w

Equations

• One or more equations did not get rendered due to their size.

def LLVM.udiv? {w : ℕ} (x : BitVec w) (y : BitVec w) : LLVM.IntW w

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.

Equations

• LLVM.udiv? x y = if y = 0 then none else pure (x / y)

structure LLVM.ExactFlag : Type

• exact : Bool

instance LLVM.instReprExactFlag : Repr LLVM.ExactFlag

Equations

• LLVM.instReprExactFlag = { reprPrec := LLVM.reprExactFlag✝ }

instance LLVM.instDecidableEqExactFlag : DecidableEq LLVM.ExactFlag

Equations

• LLVM.instDecidableEqExactFlag = LLVM.decEqExactFlag✝

def LLVM.udiv {w : ℕ} (x : LLVM.IntW w) (y : LLVM.IntW w) (flag : optParam LLVM.ExactFlag { exact := false }) : LLVM.IntW w

Equations

• LLVM.udiv x y flag = do let x' ← x let y' ← y if flag.exact = true ∧ x'.umod y' ≠ 0 then none else LLVM.udiv? x' y'

def LLVM.sdiv? {w : ℕ} (x : BitVec w) (y : BitVec w) : LLVM.IntW w

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.

Notes

The rounding is round to zero, not round to -infty. at width 1, -1 / -1 is considered -1 at width 2, -4 / -1 is considered overflow!

Equations

• LLVM.sdiv? x y = if (y == 0 || w != 1 && x == BitVec.intMin w && y == -1) = true then none else pure (x.sdiv y)

theorem LLVM.sdiv?_denom_zero_eq_none {w : ℕ} (x : BitVec w) : LLVM.sdiv? x 0 = none

theorem LLVM.sdiv?_eq_pure_of_neq_allOnes {w : ℕ} {x : BitVec w} {y : BitVec w} (hy : y ≠ 0) (hx : BitVec.intMin w ≠ x) : LLVM.sdiv? x y = pure (x.sdiv y)

def LLVM.sdiv {w : ℕ} (x : LLVM.IntW w) (y : LLVM.IntW w) (flag : optParam LLVM.ExactFlag { exact := false }) : LLVM.IntW w

Equations

• LLVM.sdiv x y flag = do let x' ← x let y' ← y if flag.exact = true ∧ x'.smod y' ≠ 0 then none else LLVM.sdiv? x' y'

theorem LLVM.sdiv?_eq_div_if {w : ℕ} {x : BitVec w} {y : BitVec w} : LLVM.sdiv? x y = if y = 0 ∨ w ≠ 1 ∧ x = BitVec.intMin w ∧ y = -1 then none else pure (x.sdiv y)

def LLVM.urem? {w : ℕ} (x : BitVec w) (y : BitVec w) : LLVM.IntW w

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.

Equations

• LLVM.urem? x y = if y = 0 then none else pure (x % y)

def LLVM.urem {w : ℕ} (x : LLVM.IntW w) (y : LLVM.IntW w) : LLVM.IntW w

Equations

• LLVM.urem x y = do let x' ← x let y' ← y LLVM.urem? x' y'

def Int.rem (x : ℤ) (y : ℤ) : ℤ

Equations

• x.rem y = if x ≥ 0 then x % y else x % y - ↑y.natAbs

theorem Int.rem_sign_dividend (x : ℤ) (y : ℤ) : x.rem y < 0 ↔ x < 0

def LLVM.srem? {w : ℕ} (x : BitVec w) (y : BitVec w) : LLVM.IntW w

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.)

The fundamental equation of div/rem is: x = (x/y) * y + x%y => x%y = x - (x/y) We use this equation to define srem.

Equations

• LLVM.srem? x y = Option.map (fun (div : BitVec w) => x - div * y) (LLVM.sdiv? x y)

def LLVM.srem {w : ℕ} (x : LLVM.IntW w) (y : LLVM.IntW w) : LLVM.IntW w

Equations

• LLVM.srem x y = do let x' ← x let y' ← y LLVM.srem? x' y'

def LLVM.sshr {n : ℕ} (a : BitVec n) (s : ℕ) : BitVec n

Equations

• LLVM.sshr a s = a.sshiftRight s

def LLVM.shl? {n : ℕ} (op1 : BitVec n) (op2 : BitVec n) : LLVM.IntW n

Shift left instruction. The value produced is op1 * 2^op2 mod 2n, where n is the width of the result. If op2 is (statically or dynamically) equal to or larger than the number of bits in op1, this instruction returns a poison value.

Equations

• LLVM.shl? op1 op2 = if op2 ≥ ↑n then none else pure (op1 <<< op2)

def LLVM.shl {w : ℕ} (x : LLVM.IntW w) (y : LLVM.IntW w) (flags : optParam LLVM.NoWrapFlags { nsw := false, nuw := false }) : LLVM.IntW w

Equations

• One or more equations did not get rendered due to their size.

def LLVM.lshr? {n : ℕ} (op1 : BitVec n) (op2 : BitVec n) : LLVM.IntW n

This instruction always performs a logical shift right operation. The most significant bits of the result will be filled with zero bits after the shift.

If op2 is (statically or dynamically) equal to or larger than the number of bits in op1, this instruction returns a poison value.

Corresponds to Std.BitVec.ushiftRight in the pure case.

Equations

• LLVM.lshr? op1 op2 = if op2 ≥ ↑n then none else pure (op1 >>> op2)

def LLVM.lshr {w : ℕ} (x : LLVM.IntW w) (y : LLVM.IntW w) (flag : optParam LLVM.ExactFlag { exact := false }) : LLVM.IntW w

Equations

• LLVM.lshr x y flag = do let x' ← x let y' ← y if flag.exact = true ∧ x' >>> y' <<< y' ≠ x' then none else LLVM.lshr? x' y'

def LLVM.ashr? {n : ℕ} (op1 : BitVec n) (op2 : BitVec n) : LLVM.IntW n

This instruction always performs an arithmetic shift right operation, The most significant bits of the result will be filled with the sign bit of op1.

If op2 is (statically or dynamically) equal to or larger than the number of bits in op1, this instruction returns a poison value.

Corresponds to Std.BitVec.sshiftRight in the pure case.

Equations

• LLVM.ashr? op1 op2 = if op2 ≥ ↑n then none else pure ((fun (x y : BitVec n) => x.sshiftRight y.toNat) op1 op2)

def LLVM.ashr {w : ℕ} (x : LLVM.IntW w) (y : LLVM.IntW w) (flag : optParam LLVM.ExactFlag { exact := false }) : LLVM.IntW w

Equations

• LLVM.ashr x y flag = do let x' ← x let y' ← y if flag.exact = true ∧ x' >>> y' <<< y' ≠ x' then none else LLVM.ashr? x' y'

def LLVM.select {w : ℕ} (c? : LLVM.IntW 1) (x? : LLVM.IntW w) (y? : LLVM.IntW w) : LLVM.IntW w

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.

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.

Equations

• LLVM.select none x? y? = none
• LLVM.select (some { toFin := ⟨1, ⋯⟩ }) x? y? = x?
• LLVM.select (some { toFin := ⟨0, ⋯⟩ }) x? y? = y?

inductive LLVM.IntPredicate : Type

• eq: LLVM.IntPredicate
• ne: LLVM.IntPredicate
• ugt: LLVM.IntPredicate
• uge: LLVM.IntPredicate
• ult: LLVM.IntPredicate
• ule: LLVM.IntPredicate
• sgt: LLVM.IntPredicate
• sge: LLVM.IntPredicate
• slt: LLVM.IntPredicate
• sle: LLVM.IntPredicate

instance LLVM.instInhabitedIntPredicate : Inhabited LLVM.IntPredicate

Equations

• LLVM.instInhabitedIntPredicate = { default := LLVM.IntPredicate.eq }

instance LLVM.instDecidableEqIntPredicate : DecidableEq LLVM.IntPredicate

Equations

• LLVM.instDecidableEqIntPredicate x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance LLVM.instReprIntPredicate : Repr LLVM.IntPredicate

Equations

• LLVM.instReprIntPredicate = { reprPrec := LLVM.reprIntPredicate✝ }

instance LLVM.instToStringIntPredicate : ToString LLVM.IntPredicate

Equations

• One or more equations did not get rendered due to their size.

def LLVM.icmp' {w : ℕ} (c : LLVM.IntPredicate) (x : BitVec w) (y : BitVec w) : Bool

The ‘icmp’ instruction takes three operands. The first operand is the condition code indicating the kind of comparison to perform. It is not a value, just a keyword. The possible condition codes are:

• eq: equal
• ne: not equal
• ugt: unsigned greater than
• uge: unsigned greater or equal
• ult: unsigned less than
• ule: unsigned less or equal
• sgt: signed greater than
• sge: signed greater or equal
• slt: signed less than
• sle: signed less or equal

The remaining two arguments must be integer. They must also be identical types.

Equations

• LLVM.icmp' LLVM.IntPredicate.eq x y = (x == y)
• LLVM.icmp' LLVM.IntPredicate.ne x y = (x != y)
• LLVM.icmp' LLVM.IntPredicate.sgt x y = (x >ₛ y)
• LLVM.icmp' LLVM.IntPredicate.sge x y = (x ≥ₛ y)
• LLVM.icmp' LLVM.IntPredicate.slt x y = (y >ₛ x)
• LLVM.icmp' LLVM.IntPredicate.sle x y = (y ≥ₛ x)
• LLVM.icmp' LLVM.IntPredicate.ugt x y = (x >ᵤ y)
• LLVM.icmp' LLVM.IntPredicate.uge x y = (x ≥ᵤ y)
• LLVM.icmp' LLVM.IntPredicate.ult x y = (y >ᵤ x)
• LLVM.icmp' LLVM.IntPredicate.ule x y = (y ≥ᵤ x)

def LLVM.icmp? {w : ℕ} (c : LLVM.IntPredicate) (x : BitVec w) (y : BitVec w) : LLVM.IntW 1

Wrapper around icmp (this cannot become none on its own).

The ‘icmp’ instruction takes three operands. The first operand is the condition code indicating the kind of comparison to perform. It is not a value, just a keyword. The possible condition codes are:

• eq: equal
• ne: not equal
• ugt: unsigned greater than
• uge: unsigned greater or equal
• ult: unsigned less than
• ule: unsigned less or equal
• sgt: signed greater than
• sge: signed greater or equal
• slt: signed less than
• sle: signed less or equal

The remaining two arguments must be integer. They must also be identical types.

Equations

• LLVM.icmp? c x y = pure (BitVec.ofBool (LLVM.icmp' c x y))

@[simp]

theorem LLVM.icmp?_ult_eq {w : ℕ} {a : BitVec w} {b : BitVec w} : LLVM.icmp? LLVM.IntPredicate.ult a b = some (BitVec.ofBool (b >ᵤ a))

@[simp]

theorem LLVM.icmp?_slt_eq {w : ℕ} {a : BitVec w} {b : BitVec w} : LLVM.icmp? LLVM.IntPredicate.slt a b = some (BitVec.ofBool (b >ₛ a))

@[simp]

theorem LLVM.icmp?_sgt_eq {w : ℕ} {a : BitVec w} {b : BitVec w} : LLVM.icmp? LLVM.IntPredicate.sgt a b = some (BitVec.ofBool (a >ₛ b))

def LLVM.icmp {w : ℕ} (c : LLVM.IntPredicate) (x : LLVM.IntW w) (y : LLVM.IntW w) : LLVM.IntW 1

Equations

• LLVM.icmp c x y = do let x' ← x let y' ← y LLVM.icmp? c x' y'

def LLVM.const? {w : ℕ} (i : ℤ) : LLVM.IntW w

Unlike LLVM IR, MLIR does not have first-class constant values. Therefore, all constants must be created as SSA values before being used in other operations. llvm.mlir.constant creates such values for scalars and vectors. It has a mandatory value attribute, which must be an integer (currently the only supported type in these semantics).

The type of the attribute is one of the corresponding MLIR builtin types. The operation produces a new SSA value of the specified LLVM IR dialect type. The type of that value must correspond to the attribute type converted to LLVM IR.

This interprets the value as a signed bitvector. If the bitwidth is not enough it will be reduced, returning the value (2^w + (i mod 2^w)) mod 2^w.

TODO: double-check that truncating works the same as MLIR (signedness, overflow, etc)

Equations

• LLVM.const? i = pure (BitVec.ofInt w i)

theorem LLVM.const?_eq {i : ℤ} {w : ℕ} : LLVM.const? i = some (BitVec.ofInt w i)

def LLVM.not? {w : ℕ} (x : BitVec w) : LLVM.IntW w

Equations

• LLVM.not? x = pure (~~~x)

theorem LLVM.not?_eq : ∀ {w : ℕ} {a : BitVec w}, LLVM.not? a = some a.not

def LLVM.not {w : ℕ} (x : LLVM.IntW w) : LLVM.IntW w

Equations

• LLVM.not x = do let x' ← x LLVM.not? x'

def LLVM.neg? {w : ℕ} (x : BitVec w) : LLVM.IntW w

Equations

• LLVM.neg? x = pure ((fun (x : BitVec w) => -x) x)

theorem LLVM.neg?_eq : ∀ {w : ℕ} {a : BitVec w}, LLVM.neg? a = some a.neg

def LLVM.neg {w : ℕ} (x : LLVM.IntW w) : LLVM.IntW w

Equations

• LLVM.neg x = do let x' ← x LLVM.neg? x'