I've been looking into how to use the z3 theorem prover in Haskell lib. It turns out to be not very well documented, and my particular use case did not have any example programs available.
Specifically, for the abstract value representation for my analysis I want to be able to represent integer values as a unique identifier, along with some constraints that are found by learning about the control flow of the program. For example a binding for within an if statement's then branch where the condition is should add the constraint that the abstract value that flows to that binding has a value greater than 0. This should be combined with finding other constants, such as using an integer to generating a list of a constant size or count down to a specific value. Finally we'd like to use Z3 to be able to prove that a value is within some concrete integer range. Using this information we can optimize the storage and arithmetic of these values statically, and omit a bunch of runtime checks that handle arbitrary precision integers.
I ended up using Ctrl+Click to step into the python api for z3 to see what low level C api calls were being made, which made it simpler to find where my error was. Turned out to be two simple things I was missing: optimizeCheck and modelEval. Changes here
This is the relevant code, that given a var with constraints having been applied via optimizeAssert, will find the appropriate integer class that the value is within.
data IntKind = Int8 | Int16 | Int32 | Int64 | UInt8 | UInt16 | UInt32 | UInt64 | IntOther
deriving Show
checkIntRange :: Z3 AST -> IO IntKind
checkIntRange var = do
b <- evalZ3 $ program optimizeMinimize
t <- evalZ3 $ program optimizeMaximize
-- let b1 = trace ("T " ++ show t ++ " B " ++ show b) b
case (b, t) of
(Just b, Just t) ->
if b >= 0 then
if t < (2^8) then
return UInt8
else if t < (2^16) then
return UInt16
else if t < (2^32) then
return $ trace ("T " ++ show t ++ " B " ++ show b) UInt32
else if t < (2^64) then
return UInt64
else
return IntOther
else
if t < (2^7) && b >= (-2^7) then
return Int8
else if t < (2^15) && b >= (-2^15) then
return Int16
else if t < (2^31) && b >= (-2^31) then
return Int32
else if t < (2^63) && b >= (-2^63) then
return Int64
else
return IntOther
_ -> return IntOther
where
program :: (AST -> Z3 Int) -> Z3 (Maybe Integer)
program optim = do
v <- var
optim v
t <- mkTrue
check <- optimizeCheck [t]
case check of
Sat -> do
m <- optimizeGetModel
x <- fromJust <$> modelEval m v False
xx <- getInt x
return $ Just xx
_ -> return Nothing
There is plenty left to do to integrate demand-cfa into the Koka compiler. However, I need to revisit some other things first.
In our lab meeting today, it was decided that we should investigate how current CFA approaches perform on modern abstractions such as typeclasses, monads, iterators / generators, concurrency, etc.
A few other common modern idioms that we did not talk about in our meeting are metaprogramming and pattern matching. I think it is worth talking about metaprogramming, especially as it pertains to programming languages that allow metaprogramming / reflection at runtime, where it cannot just be expanded statically prior to analysis. Additionally, pattern matching is becoming more pervasive across all modern languages, though most analyzers don't handle them specially - instead opting to desugar to if statements.
There are multiple strategies of implementation for analyzers that work on programs with these modern features,
- Desugar and do a CPS transformation, analyze the program normally
- Analyze the program in CPS style, but handle the modern abstractions specially
- Analyze the program in Direct (big step) style, and handle the modern abstractions specially
- Desugar to effect handlers (some of the abstractions) and do a CPS transformation, analyze the program normally
- Desugar to effect handlers (some of the abstractions) analyze in direct ADI style (potentially with evidence passing style)
While the undergraduates are investigating the question of how current CFA approaches work on modern abstractions, including creating a bunch of benchmark programs to run on, I'll investigate the implementations specific to effect handlers. The advantages of effect handlers I believe will transfer quite well to the abstract domain -- we don't have to have special analysis tools to handle each different feature, and the full generality of CPS is not required. Thus the desugaring step is not necessary. However, it might be worth making a special case for allowing more calls in the context for these particular features if they are implemented in the language instead of the analysis itself.
Additionally, I'm going to need to think about how to add support for the various features that Koka has for demand CFA, which is quite different. I think we'll start with some basics in the demand CFA, since it doesn't need to support the full generality of the language initially.
Tomorrow I plan on working on three things:
- Some basic examples of when the integer specialization analysis would be useful as well as benchmarks for testing whether it is worth the effort
- Looking into how the
linearkeyword for effect handlers alters code size / performance- Prior investigations have shown a good code size improvement, but I have not been able to see performance improvements
- We need to get to the bottom of why it would be slower, such as figuring out good benchmark programs, as well as concretely measuring the impact on code size
- Starting on a full program CFA for algebraic effect handlers
- I'll probably start with just implementing a subset of the concrete semantics of Koka's core lambda calculus with just what is needed for the exception or failure monad, and fully typed without inference. I'll need to figure out what I should do about the syntax.