-
Notifications
You must be signed in to change notification settings - Fork 3
add ValueLattice abstraction and refactor TNum for known bits #553
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: main
Are you sure you want to change the base?
Conversation
this caused problems when bottom was undefined.
i want to be able to pass a value of ValueLattice which defines only a subset of the operations, to ensure that only width-independent functions are called on the provided `top` value. F-bound polymorphism makes it hideously hard to do this because any provided value must conform to `T <: ValueLattice[T]`, effectively forcing it to be a subtype of T (which is TNum here). if we were to make this restricted ValueLattice a subtype of TNum, we also have big problems. first, since TNum already defines all the methods, we would need to override them with implementations that throw. secondly, this overriding needs to happen in TNum and would need to be repeated if we wanted to do the same for other instances of ValueLattice in the future. this is deeply unsatisfying. honestly, idk what to do. i think that the "good" solution would be to make it all type-classes. then, we would be able to split up the "static" ops (width independent) with the non-static ops that need to be called on existing values. it would be very good to avoid the dual-purpose of ValueLattice as both a "dictionary of functions" and as a "lattice value". this is the root of problems here. when we pass around an abitrary (non-sound) value to access the directory of functions, we want to guarantee that the caller does not access the lattice value methods, because it would be unsound to do so.
This reverts commit aed3c9a.
also, seeing scalacheck failure which is concerning.
|
i've added a TypedLattice to abstract the bitwidth-dependence of the lattices BASIL/src/main/scala/analysis/ValueAnalysis.scala Lines 102 to 120 in 34bed33
however, there are still some problems:
|
|
re being able to define both width-deoendent and -independent methods and being able to choose which to use, ig the thing can be the thingy blah blah method parameter dictionary of functions guh |
|
related to #464 |
0571287 to
f400e11
Compare
there is a big problem here with the Top value. the new ValueAnalysis infrastructure expects a unique value
top: Valuebut thetopin TNum requires a bit width parameter. i've arbitrarily set the bv1TNum.top(1)as "the" top value, and this causes the current test failures.(also, the TNum lattice is actually not really valid because values with differing widths are incompatible - meet/join will fail when given different widths.)
maybe we need an abstraction of bit-width which would allow the use of width-dependent lattices and coerce to Top when widths differ.