Feat: add overflow flags to lean semantics #471
Conversation
There was a problem hiding this comment.
Overall it seems like going in the right direction! I'm finding the guards with a bunch of negations somewhat confusing. If you feel these are the most idiomatic way because they reflect the document's semantics, maybe you can add a comment (quoting from the language ref) to at least justify these guards?
I think for merging this we also want to be sure that they really correspond to the LLVM behavior. Maybe you can
- add the flags to the LLVM syntax and parse these params
- check them with the flow in
test/bruteforce-correctness/llvm.py
This would give us more confidence your(/our) interpretation of the prose matches the implementation in LLVM
|
Thanks for the feedback. I guess it would be better to use |
|
As for adding the flag to the parser, I think this would be a difficult task. |
|
Alive Statistics: 59 / 93 (34 failed) |
|
Alive Statistics: 59 / 93 (34 failed) |
|
Alive Statistics: 59 / 93 (34 failed) |
|
I've added the overflow flags to the parser. |
|
Alive Statistics: 59 / 93 (34 failed) |
| | (.opaque_ "llvm.overflow" "nsw") => pure <| Sum.inl (MOp.BinaryOp.mul true false) | ||
| | (.opaque_ "llvm.overflow" "nuw") => pure <| Sum.inl (MOp.BinaryOp.mul false true) | ||
| | (.opaque_ "llvm.overflow" s ) =>throw <| .generic s!"flag {s} not allowed" | ||
| | _ => throw <| .generic s!"flag not allowed" |
There was a problem hiding this comment.
It would be helpful to include the flag that was present in the error. Something like unexpected attribute $att``
| let att := opStx.attrs.getAttr "overflowFlags" | ||
| match att with | ||
| | .none => pure <| Sum.inl (MOp.BinaryOp.add false false) | ||
| | .some y => match y with |
There was a problem hiding this comment.
Minor nit: since we use attr as an abbreviation for attribute elsewhere, it's best to be consistent and not use att as an alternative abbreviation as well.
Single letter variables can be fine when the scope is limited like here, but it's better to use a more descriptive name. In this case, we can use ? as a suffix to explicate which variable is the option, and which is the actual attribute
| let att := opStx.attrs.getAttr "overflowFlags" | |
| match att with | |
| | .none => pure <| Sum.inl (MOp.BinaryOp.add false false) | |
| | .some y => match y with | |
| let attr? := opStx.attrs.getAttr "overflowFlags" | |
| match attr? with | |
| | .none => pure <| Sum.inl (MOp.BinaryOp.add false false) | |
| | .some attr => match attr with |
| @@ -134,6 +135,7 @@ def alive_simplifyMulDivRem805 (w : Nat) : | |||
| rw [LLVM.sdiv?_denom_zero_eq_none] | |||
| apply Refinement.none_left | |||
| case neg => | |||
| simp | |||
There was a problem hiding this comment.
non-terminal simp (if a simp is not the last element of a proof, it should be simp only to reduce chances of the proof breaking when the global simp-set changes, you can use simp? to "squeeze" the simp)
| @@ -191,7 +191,7 @@ def udiv {Γ : Ctxt _} (w : ℕ) (l r : Nat) | |||
| := by get_elem_tactic) : | |||
| Expr InstCombine.LLVM Γ .pure (InstCombine.Ty.bitvec w) := | |||
| Expr.mk | |||
| (op := InstCombine.MOp.udiv w) | |||
| (op := InstCombine.MOp.udiv false w) | |||
There was a problem hiding this comment.
| (op := InstCombine.MOp.udiv false w) | |
| (op := InstCombine.MOp.udiv false w) |
| let x' ← x | ||
| let y' ← y | ||
| or? x' y' | ||
| if disjoint ∧ x' &&& y' ≠ 0 then |
There was a problem hiding this comment.
Please be mindful of whitespace
| if disjoint ∧ x' &&& y' ≠ 0 then | |
| if disjoint ∧ x' &&& y' ≠ 0 then |
| def add {w : Nat} (x y : IntW w) (params : AddParams := {}) : IntW w := do | ||
| let x ← x | ||
| let y ← y | ||
| if (params.nsw ∧ (x.toInt + y.toInt) < -(2^(w-1)) ∧ (x.toInt + y.toInt) ≥ 2^w) ∨ ( params.nuw ∧ (x.toNat + y.toNat) ≥ 2^w) then |
There was a problem hiding this comment.
This line you also have some inconsistent whitespace
| structure SubParams where | ||
| nuw : Bool := false | ||
| nsw : Bool := false |
There was a problem hiding this comment.
Given that AddParams is the same as SubParams is the same as MulParams, it makes sense to unify those into a single OverflowFlags structure
| let x' ← x | ||
| let y' ← y | ||
| or? x' y' | ||
| if disjoint ∧ x' &&& y' ≠ 0 then | ||
| .none |
There was a problem hiding this comment.
Since Option.none is brought into scope by the prelude, you don't need the dot here (nor the rest of the file)
| .none | |
| none |
| sdiv? x' y' | ||
| @[simp, reducible] |
There was a problem hiding this comment.
Please leave an empty line between definitions
|
See |
This is a smaller, scaled back version of #471 ``` I am wondering if we can scope it a bit smaller and just add overflow flags for addition. I feel this would allow us to iterate quickly on the right implementation and then expand it to all ops. ``` https://grosser.zulipchat.com/#narrow/stream/446584-Project---Lean4---BitVectors/topic/Overflow.20Flags.20in.20LLVM/near/453334239 --------- Co-authored-by: Atticus Kuhn <[email protected]> Co-authored-by: Tobias Grosser <[email protected]> Co-authored-by: Alex Keizer <[email protected]> Co-authored-by: Atticus Kuhn <[email protected]>
See
#470
and
https://grosser.zulipchat.com/#narrow/stream/248449-Project---Lean4/topic/Overflow.20Flags.20in.20LLVM
for more information