Frontend for bitvectors #879
Conversation
| case TypeRef(_, sym, FrontendBVKind(signed, size) :: Nil) if isBVSym(sym) => | ||
| Some((signed, size)) | ||
| case TypeRef(_, sym, Nil) if isBVSym(sym) => | ||
| val R = """type (UInt|Int)(\d+)""".r |
There was a problem hiding this comment.
You could avoid recreating this regex on every unapply call.
There was a problem hiding this comment.
This will probably be called quite often from extractType, since the vast majority of types will be TypeRefs, I think. Not sure if it actually makes a difference, but for TupleSymbol we have a dedicated cache. That being said, I'm not sure the way we're caching there is ideal either. We also store all the negative results, which means that map is going to be very large with a super low hit rate. Ideally we'd actually enumerate all relevant symbols upfront and put them in the map, then only check for membership during CodeExtraction.
| object FrontendBVKind { | ||
| def unapply(tpe: Type): Option[(Boolean, Int)] = tpe match { | ||
| case SingleType(_, sym) => | ||
| val R = """object ([ui])(\d+)""".r |
|
Thanks, I've moved the regular expressions outside the unapply calls. |
|
I've added |
| case (StrictBVType(_, _), "<<", Seq(rhs)) => xt.BVShiftLeft(extractTree(lhs), extractTree(rhs)) | ||
| case (StrictBVType(_, _), ">>", Seq(rhs)) => xt.BVAShiftRight(extractTree(lhs), extractTree(rhs)) | ||
| case (StrictBVType(_, _), ">>>", Seq(rhs)) => xt.BVLShiftRight(extractTree(lhs), extractTree(rhs)) | ||
| case (StrictBVType(_, _), "unary_-", Seq()) => xt.UMinus(extractTree(lhs)) |
There was a problem hiding this comment.
Not sure this new case is actually reachable. Might be caught here before?
There was a problem hiding this comment.
No it was missed, but perhaps I could adjust the extractor so that it can catch it.
|
👍 apart from the small comment |
|
Merged, thanks! |
@vkuncak @gsps @samarion Any comment in addition to what we discussed?