Conversation
tobiasgrosser
force-pushed
the
tobias/add_intbv
branch
from
799c33a to
e7575de
Compare
tobiasgrosser
force-pushed
the
tobias/add_intbv
branch
from
e7575de to
1271bdc
Compare
math-fehr
left a comment
math-fehr
left a comment
There was a problem hiding this comment.
I added some comments but otherwise it's fine!
I think we should probably rename the current folder, Dialects is not really appropriate for all these datatypes, as they are going to be reused in both LLVM, and the MLIR dialects
| @@ -0,0 +1,45 @@ | |||
| module | |||
There was a problem hiding this comment.
Should this file just replace Int/Basic.lean? It seems this is exactly the same structure, just with a different encoding?
There was a problem hiding this comment.
would a Data/ folder be useful? All the data structures used by dialects (which should not anyways be that many) could live there. I find it a little bit confusing to have the data types with the semantics of the operations
There was a problem hiding this comment.
I also don't understand what';s the difference between Int and IntBv?
And a design question: why do we want to have a bool for poison? I find the Option more intuitive, especially because I suppose in a lot of cases we won't be able to specify a priori what the value of poison is (?)
There was a problem hiding this comment.
Another alternative that comes to mind is creating a type that contains all integers (bitvecs) + a special element poison - have we considered this? What are the advantages of this def?
| namespace Veir.Dialects.LLVM.IntBv | ||
|
|
||
| example (w : Nat) (x y : IntBv w) : x + y = y + x := by | ||
| grind |
There was a problem hiding this comment.
Why does this grind works btw? Is it unfolding add by default here?
There was a problem hiding this comment.
no clue, please let me know if you find out!
Veir/Dialects/LLVM/IntBv/Basic.lean
Outdated
| The `IntBv` type can have any bitwidth `w`. It is either a two's complement | ||
| integer value of width `w` or a poison value indicating delayed undefined | ||
| behavior. |
There was a problem hiding this comment.
I would just remove the first sentence here?
Co-authored-by: Fehr Mathieu <mathieu.fehr@gmail.com>
Co-authored-by: Fehr Mathieu <mathieu.fehr@gmail.com>
luisacicolini
left a comment
luisacicolini
left a comment
There was a problem hiding this comment.
Thank you - I left a few questions about the IntBv definition!
This follows Lean's repository layout and implements @luisacicolini's suggestion in #178.
|
Let's close this for now until I have time to look into better bitblastability again. |
3 participants
This type allows us to call
bv_decideright on theIntBvtype.