Skip to content

Commit

Permalink
fix: indentation
Browse files Browse the repository at this point in the history
  • Loading branch information
tobiasgrosser committed Mar 26, 2024
1 parent f3819ee commit ef450e4
Showing 1 changed file with 6 additions and 6 deletions.
12 changes: 6 additions & 6 deletions SSA/Projects/InstCombine/LLVM/Semantics.lean
Original file line number Diff line number Diff line change
Expand Up @@ -11,38 +11,38 @@ namespace LLVM
The ‘and’ instruction returns the bitwise logical and of its two operands.
-/
def and? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
some <| x &&& y
some <| x &&& y

/--
The ‘or’ instruction returns the bitwise logical inclusive or of its two
operands.
-/
def or? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
some <| x ||| y
some <| x ||| y

/--
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.
-/
def xor? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
some <| x ^^^ y
some <| x ^^^ y

/--
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.
-/
def add? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
some <| x + y
some <| x + y

/--
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.
-/
def sub? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
some <| x - y
some <| x - y

/--
The value produced is the integer product of the two operands.
Expand All @@ -56,7 +56,7 @@ 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.
-/
def mul? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
some <| x * y
some <| x * y

/--
The value produced is the unsigned integer quotient of the two operands.
Expand Down

0 comments on commit ef450e4

Please sign in to comment.