Feat: Add Overflow Semantics to Addition in LLVM #480
Conversation
|
Alive Statistics: 59 / 93 (34 failed) |
AtticusKuhn
changed the title
|
Alive Statistics: 59 / 93 (34 failed) |
|
I am surprised to see still a need to print the default false. Is this unavoidable. |
I was also surpised that Lean prints |
|
Maybe someone with more knowledge of the Lean internals can comment as to why this is? |
|
It might be useful to build a minimal example and ask on the official lean zulip. |
|
Alive Statistics: 59 / 93 (34 failed) |
Good idea, I posted this on the Lean Zulip |
|
Alive Statistics: 64 / 93 (29 failed) |
1 similar comment
|
Alive Statistics: 64 / 93 (29 failed) |
The pretty printer only considers omitting the last optional argument. I got around this by writing |
|
Alive Statistics: 64 / 93 (29 failed) |
There was a problem hiding this comment.
This looks great to me. Maybe some comments from a parsing expert such as @bollu .
|
Alive Statistics: 64 / 93 (29 failed) |
|
Alive Statistics: 64 / 93 (29 failed) |
|
Alive Statistics: 64 / 93 (29 failed) |
1 similar comment
|
Alive Statistics: 64 / 93 (29 failed) |
|
I think this PR looks good to me now. |
SSA/Projects/InstCombine/Base.lean
Outdated
| deriving DecidableEq, Inhabited | ||
| /-- Homogeneous, binary operations -/ | ||
| inductive g : Type |
There was a problem hiding this comment.
@AtticusKuhn you've still not added the newline inbetween these two definitions
SSA/Projects/InstCombine/Base.lean
Outdated
| instance : Repr (MOp.BinaryOp) where | ||
| reprPrec op w := ((toString (aux op w)).replace "InstCombine.g" "InstCombine.MOp.BinaryOp").replace "false" "" |
There was a problem hiding this comment.
/-- The reason that I am using the admittedly hacky and ad-hoc method is that I want to preserve the guard_msgs > statements, otherwise the build will fail. But the default Repr instance has some fancy behavior where depending on the indentation it will sometimes wrap in parentheses. I think the only way to replicate this behavior is to have another class and piggy-back off its default Repr class -/
Thanks for writing this comment to explain your rationale! You are right that this solution deserves some comment in the code, but first this would fit better here in the code review --- also, as an aside, code comments are best not written in the first person, since a future reader might not immediately know who actually wrote that comment.
More concretely, the fancy behaviour you refer to is simply behaviour of Std.Format. You can have a look at the derive handler of Repr to see what code it generates; in particular the line: Repr.addAppParen (Format.group (Format.nest (if prec >= max_prec then 1 else 2) ($rhs:term))) prec) is where the parenthesization happens.
We could write similar logic by hand. See for example:
open Std (Format) in
def reprWithoutFlags (op : MOp.BinaryOp) (prec : Nat) : Format :=
let op := match op with
| .and => "and"
| .or => "or"
| .xor => "xor"
| .shl => "shl"
| .lshr => "lshr"
| .ashr => "ashr"
| .urem => "urem"
| .srem => "srem"
| .add _ => "add"
| .mul => "mul"
| .sub => "sub"
| .sdiv => "sdiv"
| .udiv => "udiv"
Repr.addAppParen (Format.group (Format.nest
(if prec >= max_prec then 1 else 2) f!"InstCombine.MOp.BinaryOp.{op}"))
prec
Finally, and the reason I do consider this one a blocker for merging: your current Repr instance completely ignores flags, all four of the following lines print exactly the same (InstCombine.MOp.BinaryOp.add)
#eval repr (MOp.BinaryOp.add ⟨false, false⟩)
#eval repr (MOp.BinaryOp.add ⟨false, true⟩)
#eval repr (MOp.BinaryOp.add ⟨true, true⟩)
#eval repr (MOp.BinaryOp.add ⟨true, false⟩)
|
Alive Statistics: 64 / 93 (29 failed) |
3 similar comments
|
Alive Statistics: 64 / 93 (29 failed) |
|
Alive Statistics: 64 / 93 (29 failed) |
|
Alive Statistics: 64 / 93 (29 failed) |
Avoid writing code comments in the first person
SSA/Projects/InstCombine/Base.lean
Outdated
| | .urem => "urem" | ||
| | .srem => "srem" | ||
| | .add ⟨false, false⟩ => "add" | ||
| | .add ⟨nsw, nuw ⟩ => toString f!"add {nsw} {nuw}" |
There was a problem hiding this comment.
| | .add ⟨nsw, nuw ⟩ => toString f!"add {nsw} {nuw}" | |
| | .add ⟨nsw, nuw⟩ => toString f!"add {nsw} {nuw}" |
Please be more careful with your whitespace!
|
Alive Statistics: 64 / 93 (29 failed) |
There was a problem hiding this comment.
Thanks for addressing my comments @AtticusKuhn, I think this is good to merge now!
Nevertheless, some general remarks: I like your code style generally, but I find you tend to be a bit sloppy when it comes to whitespace (both in terms of putting newlines in between definitions, and where to put spaces inside a line). I appreciate that there is no clear style guide and things are quite vague, but do try to give your diff a thorough read yourself to catch things that are obviously wrong! It might also help to ask @Equilibris to give your code a look for general style, before waiting on me. I've left one suggestion above, please do accept that before merging.
A minor nit: comments with /-- ... -/ are generally intended for so-called docstrings. That is, documentation of a function that will show up when you hover over a call of that function. You have some comments of this form which talk about the position of the function in the file, which is not really interesting outside of the context of that file, and should probably be a -- or /- ... -/ comment instead (neither of which will show up as documentation).
This last point is an exceedingly nitpicky comment, though. Feel free to merge as-is, or to address the points yourself and merge afterwards
|
@bollu I think you also need to "approve these changes" to unblock this PR |
Thank you for your review. I'll be sure to be more attentive in the future. |
|
Great to see this merged. 🎉 |
|
Alive Statistics: 64 / 93 (29 failed) |
This is a smaller, scaled back version of
#471
https://grosser.zulipchat.com/#narrow/stream/446584-Project---Lean4---BitVectors/topic/Overflow.20Flags.20in.20LLVM/near/453334239