From 390feae1e9261a5a37690a5b1480ae59e9988247 Mon Sep 17 00:00:00 2001
From: Duncan Ogilvie <mr.exodia.tpodt@gmail.com>
Date: Sun, 29 Oct 2017 14:58:05 +0100
Subject: [PATCH] refactor LogicIR.Expr to be smaller and to properly support
null arrays
---
src/LogicIR/Backend/Pretty.hs | 66 +++++++++---------
src/LogicIR/Backend/Z3.hs | 124 +++++++++++++++++-----------------
src/LogicIR/Expr.hs | 63 ++++++++---------
src/LogicIR/Fold.hs | 40 +++++------
src/LogicIR/Frontend/Java.hs | 52 +++++++-------
5 files changed, 164 insertions(+), 181 deletions(-)
diff --git a/src/LogicIR/Backend/Pretty.hs b/src/LogicIR/Backend/Pretty.hs
index cf793e9..3f82055 100644
--- a/src/LogicIR/Backend/Pretty.hs
+++ b/src/LogicIR/Backend/Pretty.hs
@@ -15,49 +15,45 @@ prettyType (TPrim PInt32) = "int"
prettyType (TPrim PBool) = "bool"
prettyType (TArray t) = prettyType t ++ "[]"
-prettyCOp :: COp -> String
-prettyCOp CEqual = "=="
-prettyCOp CNEqual = "!="
-prettyCOp CLess = "<"
-prettyCOp CGreater = ">"
-prettyCOp CLeq = "<="
-prettyCOp CGeq = ">="
-
prettyLBinop :: LBinop -> String
+prettyLBinop NAdd = "+"
+prettyLBinop NSub = "-"
+prettyLBinop NMul = "*"
+prettyLBinop NDiv = "/"
+prettyLBinop NRem = "%"
+prettyLBinop NShl = ">>"
+prettyLBinop NShr = "<<"
+prettyLBinop NAnd = "&"
+prettyLBinop NOr = "|"
+prettyLBinop NXor = "^"
prettyLBinop LAnd = "&&"
prettyLBinop LOr = "||"
prettyLBinop LImpl = "->"
-
-prettyNBinop :: NBinop -> String
-prettyNBinop NAdd = "+"
-prettyNBinop NSub = "-"
-prettyNBinop NMul = "*"
-prettyNBinop NDiv = "/"
-prettyNBinop NRem = "%"
-prettyNBinop NShl = ">>"
-prettyNBinop NShr = "<<"
-prettyNBinop NAnd = "&"
-prettyNBinop NOr = "|"
-prettyNBinop NXor = "^"
-
-prettyNUnop :: NUnop -> String
+prettyLBinop CEqual = "=="
+prettyLBinop CNEqual = "!="
+prettyLBinop CLess = "<"
+prettyLBinop CGreater = ">"
+prettyLBinop CLeq = "<="
+prettyLBinop CGeq = ">="
+
+prettyNUnop :: LUnop -> String
prettyNUnop NNeg = "-"
prettyNUnop NNot = "~"
+prettyNUnop LNot = "!"
prettyVar :: Var -> String
prettyVar (Var t n) = prettyType t ++ ":" ++ n
prettyLExprAlgebra :: LExprAlgebra String
-prettyLExprAlgebra = (flConst, prettyVar, flNot, flBinop, flComp, flQuant, flArray, flNil, fnConst, fnUnop, fnBinop, fnIf, fnLen) where
- flConst b = if b then "true" else "false"
- flNot a = '!' : a
- flBinop a o b = a ++ " " ++ prettyLBinop o ++ " " ++ b
- flComp a o b = a ++ " " ++ prettyCOp o ++ " " ++ b
- flQuant o v a = '(' : show o ++ " " ++ prettyVar v ++ " . " ++ a ++ ")"
- flArray v a = prettyVar v ++ "[" ++ a ++ "]"
- flNil = "nil"
- fnConst n = show n
- fnUnop o a = prettyNUnop o ++ a
- fnBinop a o b = a ++ " " ++ prettyNBinop o ++ " " ++ b
- fnIf c a b = "(" ++ c ++ ") ? (" ++ a ++ ") : (" ++ b ++ ")"
- fnLen v = "len(" ++ prettyVar v ++ ")"
\ No newline at end of file
+prettyLExprAlgebra = (fConst, prettyVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull, fLen) where
+ fConst c = case c of
+ CBool b -> if b then "true" else "false"
+ CInt n -> show n
+ CNil -> "nil"
+ fUnop o a = prettyNUnop o ++ a
+ fBinop a o b = a ++ " " ++ prettyLBinop o ++ " " ++ b
+ fIf c a b = "(" ++ c ++ ") ? (" ++ a ++ ") : (" ++ b ++ ")"
+ fQuant o v d a = '(' : show o ++ " " ++ prettyVar v ++ ": " ++ d ++ ": " ++ a ++ ")"
+ fArray v a = prettyVar v ++ "[" ++ a ++ "]"
+ fIsnull v = prettyVar v ++ " == null"
+ fLen v = "len(" ++ prettyVar v ++ ")"
\ No newline at end of file
diff --git a/src/LogicIR/Backend/Z3.hs b/src/LogicIR/Backend/Z3.hs
index e7b76e2..2b91407 100644
--- a/src/LogicIR/Backend/Z3.hs
+++ b/src/LogicIR/Backend/Z3.hs
@@ -10,68 +10,70 @@ lExprToZ3Ast = foldLExpr lExprToZ3AstAlgebra
-- TODO: support more types
lExprToZ3AstAlgebra :: LExprAlgebra (Z3 AST)
-lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, flNil, fnConst, fnUnop, fnBinop, fnIf, fnLen) where
- flConst b = mkBool b
- flVar (Var t n) = do symbol <- mkStringSymbol n
- case t of
- TPrim PInt32 -> mkBvVar symbol 32
- TPrim PBool -> mkBoolVar symbol
- TArray (TPrim PInt32) -> do intSort <- mkBvSort 32
- arraySort <- mkArraySort intSort intSort
- mkVar symbol arraySort
- TArray (TPrim PBool) -> do intSort <- mkBvSort 32
- arraySort <- mkBoolSort >>= mkArraySort intSort
+lExprToZ3AstAlgebra = (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull, fLen) where
+ fConst c = case c of
+ CBool b -> mkBool b
+ CInt n -> mkBitvector 32 (fromIntegral n)
+ CNil -> do intSort <- mkBvSort 32
+ zero <- mkBitvector 32 0x1337 -- (isNull, data, length) TODO: support proper null types
+ mkConstArray intSort zero
+ fVar (Var t n) = do symbol <- mkStringSymbol n
+ case t of
+ TPrim PInt32 -> mkBvVar symbol 32
+ TPrim PBool -> mkBoolVar symbol
+ TArray (TPrim PInt32) -> do intSort <- mkBvSort 32
+ arraySort <- mkArraySort intSort intSort
mkVar symbol arraySort
- _ -> error $ "unsupported type: " ++ show n
- flNot a = a >>= mkNot
- flBinop a' o b' = do a <- a'
- b <- b'
- case o of
- LAnd -> mkAnd [a, b]
- LOr -> mkOr [a, b]
- LImpl -> mkImplies a b
- flComp a' o b' = do a <- a'
+ TArray (TPrim PBool) -> do intSort <- mkBvSort 32
+ arraySort <- mkBoolSort >>= mkArraySort intSort
+ mkVar symbol arraySort
+ _ -> error $ "unsupported type: " ++ show n
+ fUnop o a' = do a <- a'
+ case o of
+ NNeg -> mkBvneg a
+ NNot -> mkBvnot a
+ LNot -> mkNot a
+ fBinop a' o b' = do a <- a'
b <- b'
case o of
- CEqual -> mkEq a b
- CNEqual -> mkEq a b >>= mkNot
- CLess -> mkBvslt a b
- CGreater -> mkBvsgt a b
- CLeq -> mkBvsle a b
- CGeq -> mkBvsge a b
- flQuant o v@(Var t n) a' = do a <- a'
- case t of
- TPrim PInt32 -> do vApp <- flVar v >>= toApp
- case o of
- QAll -> mkForallConst [] [vApp] a
- QAny -> mkExistsConst [] [vApp] a
- _ -> error $ "unsupported quantifier domain type: " ++ show (o, v)
- flArray v a' = do v <- flVar v
+ NAdd -> mkBvadd a b
+ NSub -> mkBvsub a b
+ NMul -> mkBvmul a b
+ NDiv -> mkBvsdiv a b -- NOTE: signed division
+ NRem -> mkBvsrem a b -- TODO: check if the correct remainder is taken
+ NShl -> mkBvshl a b
+ NShr -> mkBvashr a b -- NOTE: signed shift right will keep the sign
+ NAnd -> mkBvand a b
+ NOr -> mkBvor a b
+ NXor -> mkBvxor a b
+
+ LAnd -> mkAnd [a, b]
+ LOr -> mkOr [a, b]
+ LImpl -> mkImplies a b
+
+ CEqual -> mkEq a b
+ CNEqual -> mkEq a b >>= mkNot
+ CLess -> mkBvslt a b
+ CGreater -> mkBvsgt a b
+ CLeq -> mkBvsle a b
+ CGeq -> mkBvsge a b
+ fIf c' a' b' = do c <- c'
a <- a'
- mkSelect v a
- flNil = do intSort <- mkBvSort 32
- zero <- mkBitvector 32 0x1337 -- (isNull, data, length) TODO: support proper null types
- mkConstArray intSort zero
- fnConst n = mkBitvector 32 (fromIntegral n)
- fnUnop o a' = do a <- a'
- case o of
- NNeg -> mkBvneg a
- NNot -> mkBvnot a
- fnBinop a' o b' = do a <- a'
- b <- b'
- case o of
- NAdd -> mkBvadd a b
- NSub -> mkBvsub a b
- NMul -> mkBvmul a b
- NDiv -> mkBvsdiv a b -- NOTE: signed division
- NRem -> mkBvsrem a b -- TODO: check if the correct remainder is taken
- NShl -> mkBvshl a b
- NShr -> mkBvashr a b -- NOTE: signed shift right will keep the sign
- NAnd -> mkBvand a b
- NOr -> mkBvor a b
- NXor -> mkBvxor a b
- fnIf c' a' b' = do c <- c'
- a <- a'
- b <- b'
- mkIte c a b
- fnLen (Var (TArray (TPrim _)) n) = mkStringSymbol (n ++ ".length") >>= flip mkBvVar 32 -- TODO: support proper array lengths
+ b <- b'
+ mkIte c a b
+
+ fQuant o v@(Var t n) d' a' = do a <- a'
+ d <- d'
+ case t of
+ TPrim PInt32 -> do vApp <- fVar v >>= toApp
+ case o of
+ QAll -> do e <- mkImplies d a
+ mkForallConst [] [vApp] e
+ QAny -> do e <- mkAnd [d, a]
+ mkExistsConst [] [vApp] e
+ _ -> error $ "unsupported quantifier domain type: " ++ show (o, v)
+ fArray v a' = do v <- fVar v
+ a <- a'
+ mkSelect v a
+ fIsnull v = undefined
+ fLen (Var (TArray (TPrim _)) n) = mkStringSymbol (n ++ ".length") >>= flip mkBvVar 32 -- TODO: support proper array lengths
diff --git a/src/LogicIR/Expr.hs b/src/LogicIR/Expr.hs
index 0d0f589..9387371 100644
--- a/src/LogicIR/Expr.hs
+++ b/src/LogicIR/Expr.hs
@@ -1,6 +1,7 @@
module LogicIR.Expr where
-- Based on previous work: https://github.com/mrexodia/wp/blob/master/Wp.hs
+-- Reference: https://en.wikipedia.org/wiki/First-order_logic#Logical_symbols
-- The primitive types are bool and int32.
data Primitive = PBool
@@ -16,13 +17,14 @@ data Type = TPrim Primitive
data Var = Var Type String
deriving (Show, Eq, Read)
--- Numeral unary operators
-data NUnop = NNeg -- -n (negation)
+-- Unary operators
+data LUnop = NNeg -- -n (negation)
| NNot -- ~n (binary not)
+ | LNot -- !n (logical not)
deriving (Show, Eq, Read)
--- Numeral binary operators
-data NBinop = NAdd -- a + b
+-- Binary operators
+data LBinop = NAdd -- a + b
| NSub -- a - b
| NMul -- a * b
| NDiv -- a / b
@@ -32,45 +34,36 @@ data NBinop = NAdd -- a + b
| NAnd -- a & b
| NOr -- a | b
| NXor -- a ^ b
- deriving (Show, Eq, Read)
--- Reference: https://en.wikipedia.org/wiki/First-order_logic#Logical_symbols
+ | LAnd -- a && b
+ | LOr -- a || b
+ | LImpl -- a => b
--- Logical operators
-data LBinop = LAnd -- Conjunction
- | LOr -- Disjunction
- | LImpl -- Implication
+ | CEqual -- a == b
+ | CNEqual -- a != b
+ | CLess -- a < b
+ | CGreater -- a > b
+ | CLeq -- a <= b
+ | CGeq -- a >= b
deriving (Show, Eq, Read)
-- Quantifier operators
data QOp = QAll | QAny
deriving (Show, Eq, Read)
--- Comparison operators
-data COp = CEqual -- a == b
- | CNEqual -- a != b
- | CLess -- a < b
- | CGreater -- a > b
- | CLeq -- a <= b
- | CGeq -- a >= b
- deriving (Show, Eq, Read)
-
--- Logical and numeral expressions are the same type, but an alias is added for clarity.
-type NExpr = LExpr
+data LConst = CBool Bool
+ | CInt Int
+ | CNil
+ deriving (Show, Eq, Read)
-- Logical expressions
-data LExpr = LConst Bool -- True/False
- | LVar Var -- Variable
- | LNot LExpr -- Logical negation/not
- | LBinop LExpr LBinop LExpr -- Logical operator
- | LComp NExpr COp NExpr -- Integer comparison
- | LQuant QOp Var LExpr -- Logical quantifier
- | LArray Var NExpr -- Logical array access
- | LNil -- Nil constant
-
- | NConst Int -- Integer constant (TODO: use Integer instead of Int?)
- | NUnop NUnop NExpr -- Unary operator
- | NBinop NExpr NBinop NExpr -- Binary operators
- | NIf LExpr NExpr NExpr -- if c then a else b
- | NLen Var -- len(array)
+data LExpr = LConst LConst -- constant
+ | LVar Var -- variable
+ | LUnop LUnop LExpr -- unary operator
+ | LBinop LExpr LBinop LExpr -- binary operator
+ | LIf LExpr LExpr LExpr -- if c then a else b (ternary operator)
+ | LQuant QOp Var LExpr LExpr -- quantifier (op bound domain expr)
+ | LArray Var LExpr -- array access
+ | LIsnull Var -- var == null
+ | LLen Var -- len(array)
deriving (Show, Eq, Read)
\ No newline at end of file
diff --git a/src/LogicIR/Fold.hs b/src/LogicIR/Fold.hs
index 75ba32c..a9f4b62 100644
--- a/src/LogicIR/Fold.hs
+++ b/src/LogicIR/Fold.hs
@@ -3,35 +3,27 @@ module LogicIR.Fold where
import LogicIR.Expr
-- Fold algebra for logical expressions
-type LExprAlgebra r = (Bool -> r, -- LConst
+type LExprAlgebra r = (LConst -> r, -- LConst
Var -> r, -- LVar
- r -> r, -- LNot
+ LUnop -> r -> r, -- LUnop
r -> LBinop -> r -> r, -- LBinop
- r -> COp -> r -> r, -- LComp
- QOp -> Var -> r -> r, -- LQuant
+ r -> r -> r -> r, -- LIf
+ QOp -> Var -> r -> r -> r, -- LQuant
Var -> r -> r, -- LArray
- r, -- LNil
- Int -> r, -- NConst
- NUnop -> r -> r, -- NUnop
- r -> NBinop -> r -> r, -- NBinop
- r -> r -> r -> r, -- NIf
- Var -> r -- NLen
+ Var -> r, -- LIsnull
+ Var -> r -- LLen
)
-- Fold for logical expressions
foldLExpr :: LExprAlgebra r -> LExpr -> r
-foldLExpr (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, flNil, fnConst, fnUnop, fnBinop, fnIf, fnLen) = fold where
+foldLExpr (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull, fLen) = fold where
fold e = case e of
- LConst c -> flConst c
- LVar v -> flVar v
- LNot e -> flNot (fold e)
- LBinop a o b -> flBinop (fold a) o (fold b)
- LComp a o b -> flComp (fold a) o (fold b)
- LQuant o v e -> flQuant o v (fold e)
- LArray v e -> flArray v (fold e)
- LNil -> flNil
- NConst n -> fnConst n
- NUnop o e -> fnUnop o (fold e)
- NBinop a o b -> fnBinop (fold a) o (fold b)
- NIf c a b -> fnIf (fold c) (fold a) (fold b)
- NLen v -> fnLen v
\ No newline at end of file
+ LConst c -> fConst c
+ LVar v -> fVar v
+ LUnop o a -> fUnop o (fold a)
+ LBinop a o b -> fBinop (fold a) o (fold b)
+ LIf c a b -> fIf (fold c) (fold a) (fold b)
+ LQuant o b d a -> fQuant o b (fold d) (fold a)
+ LArray v a -> fArray v (fold a)
+ LIsnull v -> fIsnull v
+ LLen v -> fLen v
\ No newline at end of file
diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index 7d63f3c..d0bed50 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -26,9 +26,9 @@ nameToVar name env decls = let (arrayType, symbol) = (lookupType decls env name,
javaExpToLExprAlgebra :: ExpAlgebra (TypeEnv -> [TypeDecl] -> LExpr)
javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualInstanceCreation, fArrayCreate, fArrayCreateInit, fFieldAccess, fMethodInv, fArrayAccess, fExpName, fPostIncrement, fPostDecrement, fPreIncrement, fPreDecrement, fPrePlus, fPreMinus, fPreBitCompl, fPreNot, fCast, fBinOp, fInstanceOf, fCond, fAssign, fLambda, fMethodRef) where
fLit lit _ _ = case lit of -- TODO: support more type literals?
- Boolean b -> LConst b
- Int n -> NConst (fromIntegral n)
- Null -> LNil
+ Boolean b -> LConst (CBool b)
+ Int n -> LConst (CInt (fromIntegral n))
+ Null -> LConst CNil
_ -> error $ show $ lit
fClassLit = error "fClassLit not supported..."
fThis = error "fThis not supported..."
@@ -60,52 +60,52 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
-> error $ "Unimplemented fMethodInv: " ++ show inv
where forall name bound expr = let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in
- LQuant QAll i (LBinop (LBinop (LComp (LVar i) CGeq (NConst 0)) LAnd (LComp (LVar i) CLess (NLen arr))) LImpl (foldExp javaExpToLExprAlgebra expr env decls))
+ LQuant QAll i (LBinop (LBinop (LVar i) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar i) CLess (LLen arr))) (foldExp javaExpToLExprAlgebra expr env decls)
exists name bound expr = let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in
- LQuant QAny i (LBinop (LBinop (LComp (LVar i) CGeq (NConst 0)) LAnd (LComp (LVar i) CLess (NLen arr))) LAnd (foldExp javaExpToLExprAlgebra expr env decls))
+ LQuant QAny i (LBinop (LBinop (LVar i) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar i) CLess (LLen arr))) (foldExp javaExpToLExprAlgebra expr env decls)
fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: type checking
ArrayIndex (ExpName name) [expr]
-> LArray (nameToVar name env decls) (javaExpToLExpr expr env decls)
_
-> error $ "Multidimensional arrays are not supported: " ++ show (arrayIndex)
fExpName name env decls = case name of -- TODO: type checking + check implicit `this.name`
- Name [Ident a, Ident "length"] -> NLen $ nameToVar (Name [Ident a]) env decls
+ Name [Ident a, Ident "length"] -> LLen $ nameToVar (Name [Ident a]) env decls
_ -> LVar $ nameToVar name env decls
fPostIncrement = error "fPostIncrement has side effects..."
fPostDecrement = error "fPostDecrement has side effects..."
fPreIncrement = error "fPreIncrement has side effects..."
fPreDecrement = error "fPreDecrement has side effects..."
fPrePlus e env decls = e env decls
- fPreMinus e env decls = NUnop NNeg (e env decls)
- fPreBitCompl e env decls = NUnop NNot (e env decls)
- fPreNot e env decls = LNot (e env decls)
+ fPreMinus e env decls = LUnop NNeg (e env decls)
+ fPreBitCompl e env decls = LUnop NNot (e env decls)
+ fPreNot e env decls = LUnop LNot (e env decls)
fCast = error "fCast is not supported..." -- TODO: perhaps support cast for some types?
fBinOp e1 op e2 env decls = let (a, b) = (e1 env decls, e2 env decls) in -- TODO: type checking?
case op of
-- Integer
- Mult -> NBinop a NMul b
- Div -> NBinop a NDiv b
- Rem -> NBinop a NRem b
- Add -> NBinop a NAdd b
- Sub -> NBinop a NSub b
- LShift -> NBinop a NShl b
- RShift -> NBinop a NShr b
+ Mult -> LBinop a NMul b
+ Div -> LBinop a NDiv b
+ Rem -> LBinop a NRem b
+ Add -> LBinop a NAdd b
+ Sub -> LBinop a NSub b
+ LShift -> LBinop a NShl b
+ RShift -> LBinop a NShr b
RRShift -> undefined
- And -> NBinop a NAnd b
- Or -> NBinop a NOr b
- Xor -> NBinop a NXor b
+ And -> LBinop a NAnd b
+ Or -> LBinop a NOr b
+ Xor -> LBinop a NXor b
-- Logical
CAnd -> LBinop a LAnd b
COr -> LBinop a LOr b
-- Comparisons
- LThan -> LComp a CLess b
- GThan -> LComp a CGreater b
- LThanE -> LComp a CLeq b
- GThanE -> LComp a CGeq b
- Equal -> LComp a CEqual b
- NotEq -> LComp a CNEqual b
+ LThan -> LBinop a CLess b
+ GThan -> LBinop a CGreater b
+ LThanE -> LBinop a CLeq b
+ GThanE -> LBinop a CGeq b
+ Equal -> LBinop a CEqual b
+ NotEq -> LBinop a CNEqual b
fInstanceOf = error "fInstanceOf is not supported..."
- fCond c a b env decls = NIf (c env decls) (a env decls) (b env decls)
+ fCond c a b env decls = LIf (c env decls) (a env decls) (b env decls)
fAssign = error "fAssign has side effects..."
fLambda = error "fLambda should be handled by fMethodInv..."
fMethodRef = undefined
\ No newline at end of file
--
GitLab