Equations
- LLVM.instReprDisjointFlag = { reprPrec := LLVM.reprDisjointFlag✝ }
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.
Instances For
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.
Instances For
Equations
- LLVM.instReprNoWrapFlags = { reprPrec := LLVM.reprNoWrapFlags✝ }
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.
Instances For
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.
Instances For
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)
Instances For
Equations
- LLVM.instReprExactFlag = { reprPrec := LLVM.reprExactFlag✝ }
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
Instances For
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)
Instances For
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)
Instances For
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.
Instances For
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)
Instances For
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)
Instances For
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?
Instances For
- 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
Instances For
Equations
- LLVM.instInhabitedIntPredicate = { default := LLVM.IntPredicate.eq }
Equations
- LLVM.instDecidableEqIntPredicate x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯
Equations
- LLVM.instReprIntPredicate = { reprPrec := LLVM.reprIntPredicate✝ }
Equations
- One or more equations did not get rendered due to their size.
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)
Instances For
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))
Instances For
Equations
- LLVM.icmp c x y = do let x' ← x let y' ← y LLVM.icmp? c x' y'
Instances For
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)