Commit 42e9f704 authored by Wouter Raateland's avatar Wouter Raateland
Browse files

Create more arbitrary instances and soundly interpret single statements

parent 0daeed4a
......@@ -321,7 +321,7 @@ instance UseVal Val Interp where
case_ f = proc (v,cases) -> case v of
IntVal x -> case find (matchCase x) cases of
Just (_,label) -> f -< label
Nothing -> failStatic -< printf "No cases match value %s" (show v)
Nothing -> failStatic -< "No matching cases"
_ -> failStatic -< "Expected an integer as argument for switch"
where
matchCase x (c,_) = case c of
......
......@@ -18,10 +18,6 @@ instance Show v => Show (Exception v) where
show (StaticException s) = "Static: " ++ show s
show (DynamicException v) = "Dynamic: " ++ show v
-- instance Hashable v => Hashable (Exception v) where
-- hashWithSalt h (StaticException s) = h + hash s
-- hashWithSalt h (DynamicException v) = h + hash v
instance PreOrd v => PreOrd (Exception v) where
StaticException s1 StaticException s2 = s1 s2
DynamicException _ StaticException _ = True
......@@ -38,11 +34,11 @@ instance Complete v => Complete (Exception v) where
DynamicException v1 DynamicException v2 = DynamicException $ v1 v2
instance IsString (Exception v) where
fromString s = StaticException $ singleton s
fromString = StaticException . singleton
instance (Eq v, Hashable v, Complete v', Galois (Con.Pow v) v')
=> Galois (Con.Pow (Con.Exception v)) (Exception v') where
alpha = lifted $ \e -> case e of
Con.StaticException s -> StaticException $ singleton s
Con.StaticException s -> fromString s
Con.DynamicException v -> DynamicException $ alphaSing v
gamma = error "noncomputable"
......@@ -4,7 +4,6 @@
module Data.Concrete.Exception where
import Data.Hashable
import Data.String
data Exception v = StaticException String | DynamicException v deriving (Eq)
......@@ -15,6 +14,3 @@ instance Show v => Show (Exception v) where
instance Hashable v => Hashable (Exception v) where
hashWithSalt h (StaticException s) = h + hash s
hashWithSalt h (DynamicException v) = h + hash v
instance IsString (Exception v) where
fromString = StaticException
......@@ -15,7 +15,7 @@ import Prelude hiding (lookup,read,fail,Bounded(..))
import qualified Data.Boolean as B
import Data.Order
import Data.Set (singleton)
import Data.String (fromString)
import qualified Data.Abstract.Boolean as Abs
import Data.Abstract.Environment (Env)
......@@ -229,11 +229,13 @@ instance UseVal Val Interp where
Top -> joined (defaultValue >>^ ( NonNull)) failDynamic -< (t,NonNull)
updateField f = first ((\(o,(v,_)) -> (o,v)) ^>> readField) >>> U.pi2 >>> f
readStaticField = proc f -> read U.pi1 failStatic -<
(f,printf "FieldReference %s not bound" (show f))
(f,printf "Field %s not bound" (show f))
updateStaticField = proc (f,v) -> do
readStaticField -< f
write -< (f,v)
case_ f = U.pi2 >>> map snd ^>> lubA f
case_ f = proc (_,cases) ->
joined (lubA f) (joined failStatic failStatic) -< (map snd cases,
("No matching cases","Expected an integer as argument for switch"))
instance UseException Exception Val Interp where
catch f = proc (ex,clauses) -> case ex of
......@@ -241,7 +243,7 @@ instance UseException Exception Val Interp where
DynamicException v ->
joined (lubA f) failDynamic -< (zip (repeat v) clauses,v)
failDynamic = DynamicException ^>> fail
failStatic = (\s -> StaticException $ singleton s) ^>> fail
failStatic = fromString ^>> fail
instance UseBool Abs.Bool Val Interp where
eq = arr $ uncurry (Abs.==)
......
......@@ -67,15 +67,15 @@ readCompilationUnit = proc n -> do
evalInvoke :: CanInterp env envval val ex bool c => c EInvoke (Maybe val)
evalInvoke = proc e -> case e of
SpecialInvoke localName m params -> runMethod -< (Just localName,m,params)
VirtualInvoke localName m params -> runMethod -< (Just localName,m,params)
InterfaceInvoke localName m params -> runMethod -< (Just localName,m,params)
SpecialInvoke this m params -> runMethod -< (Just this,m,params)
VirtualInvoke this m params -> runMethod -< (Just this,m,params)
InterfaceInvoke this m params -> runMethod -< (Just this,m,params)
StaticInvoke m params -> runMethod -< (Nothing,m,params)
DynamicInvoke{} -> failStatic -< "DynamicInvoke is not implemented"
evalImmediate :: (ArrowChoice c,UseVal val c) => c Immediate val
evalImmediate = proc i -> case i of
Local localName -> readVar -< localName
Local name -> readVar -< name
DoubleConstant f -> doubleConstant -< f
FloatConstant f -> floatConstant -< f
IntConstant n -> intConstant -< n
......
{-# LANGUAGE DuplicateRecordFields #-}
module Syntax where
import Data.Hashable
......@@ -8,6 +7,8 @@ import Control.Monad
import Test.QuickCheck
---- Data ----------------------------------------------------------------------
data CompilationUnit = CompilationUnit { fileModifiers :: [Modifier]
, fileType :: FileType
, fileName :: String
......@@ -16,25 +17,6 @@ data CompilationUnit = CompilationUnit { fileModifiers :: [Modifier]
, fileBody :: [Member]
}
instance Eq CompilationUnit where
(==) f1 f2 = fileName f1 == fileName f2
instance Show CompilationUnit where
show f = "CompilationUnit {"
++ show (fileModifiers f) ++ " "
++ show (fileType f) ++ " "
++ show (fileName f) ++ " "
++ ex
++ impl
++ "}"
where
ex = case extends f of
Just c -> "extends " ++ show c
Nothing -> ""
impl = case length (implements f) of
0 -> ""
xs -> "implements " ++ show xs
data Modifier
= Abstract
| Final
......@@ -50,49 +32,16 @@ data Modifier
| Enum
| Annotation deriving (Eq)
instance Show Modifier where
show Abstract = "abstract"
show Final = "final"
show Native = "native"
show Public = "public"
show Protected = "protected"
show Private = "private"
show Static = "static"
show Synchronized = "synchronized"
show Transient = "transient"
show Volatile = "volatile"
show Strictfp = "strictfp"
show Enum = "enum"
show Annotation = "annotation"
data FileType
= ClassFile
| InterfaceFile
instance Show FileType where
show ClassFile = "class"
show InterfaceFile = "interface"
data MethodSignature = MethodSignature String Type String [Type] deriving (Show, Eq)
data UnnamedMethodSignature = UnnamedMethodSignature Type [Type] deriving (Show, Eq)
data FieldSignature = FieldSignature String Type String deriving (Eq)
instance Ord FieldSignature where
compare (FieldSignature c1 _ n1) (FieldSignature c2 _ n2) =
case compare c1 c2 of
LT -> LT
EQ -> compare n1 n2
GT -> GT
instance Show FieldSignature where
show (FieldSignature c t n) =
"<" ++ show c ++ ": " ++ show t ++ " " ++ show n ++ ">"
instance Hashable FieldSignature where
hashWithSalt s (FieldSignature c t n) = s + hash c + hash t + hash n
data Member = FieldMember Field | MethodMember Method
data Field = Field { fieldModifiers :: [Modifier]
......@@ -100,10 +49,6 @@ data Field = Field { fieldModifiers :: [Modifier]
, fieldName :: String
}
fieldSignature :: CompilationUnit -> Field -> FieldSignature
fieldSignature CompilationUnit{fileName=c} Field{fieldType=t,fieldName=n}
= FieldSignature c t n
data Method = Method { methodModifiers :: [Modifier]
, returnType :: Type
, methodName :: String
......@@ -112,10 +57,6 @@ data Method = Method { methodModifiers :: [Modifier]
, methodBody :: MethodBody
} deriving (Show, Eq)
methodSignature :: CompilationUnit -> Method -> MethodSignature
methodSignature CompilationUnit{fileName=c} Method{returnType=t,parameters=p,methodName=n}
= MethodSignature c t n p
data Type
= ArrayType Type
| BooleanType
......@@ -131,58 +72,6 @@ data Type
| UnknownType
| VoidType deriving (Eq)
instance Show Type where
show (ArrayType t) = show t ++ "[]"
show BooleanType = "bool"
show ByteType = "byte"
show CharType = "char"
show DoubleType = "double"
show FloatType = "float"
show IntType = "int"
show LongType = "long"
show NullType = "null"
show (RefType s) = show s
show ShortType = "short"
show UnknownType = "<untyped>"
show VoidType = "void"
instance Hashable Type where
hashWithSalt n t = n + hash (show t)
instance Arbitrary Type where
arbitrary = oneof $ refType:map return [
BooleanType,
ByteType,
CharType,
DoubleType,
FloatType,
IntType,
LongType,
NullType,
ShortType]
where
refType = fmap RefType arbitrary
isNonvoidType :: Type -> Bool
isNonvoidType VoidType = False
isNonvoidType UnknownType = False
isNonvoidType _ = True
isBaseType :: Type -> Bool
isBaseType VoidType = False
isBaseType UnknownType = False
isBaseType (ArrayType _) = False
isBaseType _ = True
isIntegerType :: Type -> Bool
isIntegerType BooleanType = True
isIntegerType ByteType = True
isIntegerType CharType = True
isIntegerType IntType = True
isIntegerType LongType = True
isIntegerType ShortType = True
isIntegerType _ = False
data MethodBody
= EmptyBody
| FullBody { declarations :: [Declaration]
......@@ -235,26 +124,9 @@ data Expr
| ImmediateExpr Immediate
| MethodHandle MethodSignature deriving (Show, Eq)
instance Arbitrary Expr where
arbitrary = oneof [
fmap NewExpr arbitrary,
liftM2 NewArrayExpr arbitrary arbitrary,
liftM2 NewMultiArrayExpr arbitrary (replicateM 2 arbitrary),
liftM2 CastExpr arbitrary arbitrary,
liftM2 InstanceOfExpr arbitrary arbitrary,
-- InvokeExpr EInvoke,
-- RefExpr ERef,
liftM3 BinopExpr arbitrary arbitrary arbitrary,
liftM2 UnopExpr arbitrary arbitrary,
fmap ImmediateExpr arbitrary]
-- MethodHandle MethodSignature]
data BoolExpr
= BoolExpr Immediate BoolOp Immediate deriving (Show, Eq)
instance Arbitrary BoolExpr where
arbitrary = liftM3 BoolExpr arbitrary arbitrary arbitrary
data Immediate
= Local String
| DoubleConstant Float
......@@ -265,17 +137,6 @@ data Immediate
| StringConstant String
| ClassConstant String deriving (Show, Eq)
instance Arbitrary Immediate where
arbitrary = oneof [
fmap Local arbitrary,
fmap DoubleConstant arbitrary,
fmap FloatConstant arbitrary,
fmap IntConstant arbitrary,
fmap LongConstant arbitrary,
return NullConstant,
fmap StringConstant arbitrary,
fmap ClassConstant arbitrary]
data AtIdentifier
= ThisRef
| ParameterRef Int
......@@ -300,22 +161,237 @@ data EInvoke
data BoolOp
= Cmpeq | Cmpne | Cmpgt | Cmpge | Cmplt | Cmple deriving (Show, Eq)
instance Arbitrary BoolOp where
arbitrary = oneof $ map return [Cmpeq, Cmpne, Cmpgt, Cmpge, Cmplt, Cmple]
data Binop
= And | Or | Xor | Shl | Shr | Ushr
| Cmp | Cmpg | Cmpl
| Plus | Minus | Mult | Div | Rem deriving (Show, Eq)
data Unop
= Lengthof
| Neg deriving (Show, Eq)
---- Helpers -------------------------------------------------------------------
fieldSignature :: CompilationUnit -> Field -> FieldSignature
fieldSignature CompilationUnit{fileName=c} Field{fieldType=t,fieldName=n}
= FieldSignature c t n
methodSignature :: CompilationUnit -> Method -> MethodSignature
methodSignature CompilationUnit{fileName=c} Method{returnType=t,parameters=p,methodName=n}
= MethodSignature c t n p
isNonvoidType :: Type -> Bool
isNonvoidType VoidType = False
isNonvoidType UnknownType = False
isNonvoidType _ = True
isBaseType :: Type -> Bool
isBaseType VoidType = False
isBaseType UnknownType = False
isBaseType (ArrayType _) = False
isBaseType _ = True
isIntegerType :: Type -> Bool
isIntegerType BooleanType = True
isIntegerType ByteType = True
isIntegerType CharType = True
isIntegerType IntType = True
isIntegerType LongType = True
isIntegerType ShortType = True
isIntegerType _ = False
arbitraryLabel :: Gen String
arbitraryLabel = do
n <- choose (1::Int,10::Int)
return $ "label" ++ show n
arbitraryLocalName :: Gen String
arbitraryLocalName = oneof $ map (return . show) (decreasing 26 ['a'..'z'])
where
decreasing _ [] = []
decreasing n (h:t) = replicate (n*n) h:decreasing (n - 1) t
arbitraryFieldName :: Gen String
arbitraryFieldName = oneof $ arbitrary : map return ["foo","bar","baz"]
arbitraryMethodName :: Gen String
arbitraryMethodName = oneof $ arbitrary : map return ["<clinit>","<init>","main","foo","bar","baz"]
arbitraryClassName :: Gen String
arbitraryClassName = oneof $ arbitrary : map return ["java.lang.Object"]
---- Instances -----------------------------------------------------------------
instance Show Modifier where
show Abstract = "abstract"
show Final = "final"
show Native = "native"
show Public = "public"
show Protected = "protected"
show Private = "private"
show Static = "static"
show Synchronized = "synchronized"
show Transient = "transient"
show Volatile = "volatile"
show Strictfp = "strictfp"
show Enum = "enum"
show Annotation = "annotation"
instance Ord FieldSignature where
compare (FieldSignature c1 _ n1) (FieldSignature c2 _ n2) =
case compare c1 c2 of
LT -> LT
EQ -> compare n1 n2
GT -> GT
instance Show FieldSignature where
show (FieldSignature c t n) =
"<" ++ show c ++ ": " ++ show t ++ " " ++ show n ++ ">"
instance Hashable FieldSignature where
hashWithSalt s (FieldSignature c t n) = s + hash c + hash t + hash n
instance Show Type where
show (ArrayType t) = show t ++ "[]"
show BooleanType = "bool"
show ByteType = "byte"
show CharType = "char"
show DoubleType = "double"
show FloatType = "float"
show IntType = "int"
show LongType = "long"
show NullType = "null"
show (RefType s) = show s
show ShortType = "short"
show UnknownType = "<untyped>"
show VoidType = "void"
instance Hashable Type where
hashWithSalt n t = n + hash (show t)
---- Arbitrary Instances -------------------------------------------------------
-- instance Arbitrary CompilationUnit where
--instance Arbitrary Modifier where
--instance Arbitrary FileType where
instance Arbitrary MethodSignature where
arbitrary = liftM4 MethodSignature arbitraryClassName arbitrary arbitraryMethodName arbitrary
instance Arbitrary UnnamedMethodSignature where
arbitrary = liftM2 UnnamedMethodSignature arbitrary arbitrary
instance Arbitrary FieldSignature where
arbitrary = liftM3 FieldSignature arbitraryClassName arbitrary arbitraryFieldName
--instance Arbitrary Member where
--instance Arbitrary Field where
--instance Arbitrary Method where
instance Arbitrary Type where
arbitrary = oneof $ refType:map return [
BooleanType,
ByteType,
CharType,
DoubleType,
FloatType,
IntType,
LongType,
NullType,
ShortType,
UnknownType,
VoidType]
where
refType = fmap RefType arbitrary
--instance Arbitrary MethodBody where
-- type Declaration
instance Arbitrary Statement where
arbitrary = oneof [
fmap Label arbitraryLabel,
return Breakpoint,
liftM2 Tableswitch arbitrary arbitrary,
liftM2 Lookupswitch arbitrary arbitrary,
liftM3 Identity arbitraryLocalName arbitrary arbitrary,
liftM2 IdentityNoType arbitraryLocalName arbitrary,
liftM2 Assign arbitrary arbitrary,
liftM2 If arbitrary arbitraryLabel,
fmap Goto arbitraryLabel,
return Nop,
fmap Ret arbitrary,
fmap Return arbitrary,
fmap Throw arbitrary,
fmap Invoke arbitrary]
-- type CaseStatement
instance Arbitrary CaseLabel where
arbitrary = oneof $
return DefaultCase :
replicate 5 (fmap ConstantCase arbitrary)
--instance Arbitrary CatchClause where
instance Arbitrary Expr where
arbitrary = oneof [
fmap NewExpr arbitrary,
liftM2 NewArrayExpr arbitrary arbitrary,
liftM2 NewMultiArrayExpr arbitrary (replicateM 2 arbitrary),
liftM2 CastExpr arbitrary arbitrary,
liftM2 InstanceOfExpr arbitrary arbitrary,
fmap InvokeExpr arbitrary,
fmap RefExpr arbitrary,
liftM3 BinopExpr arbitrary arbitrary arbitrary,
liftM2 UnopExpr arbitrary arbitrary,
fmap ImmediateExpr arbitrary,
fmap MethodHandle arbitrary]
instance Arbitrary BoolExpr where
arbitrary = liftM3 BoolExpr arbitrary arbitrary arbitrary
instance Arbitrary Immediate where
arbitrary = oneof [
fmap Local arbitraryLocalName,
fmap DoubleConstant arbitrary,
fmap FloatConstant arbitrary,
fmap IntConstant arbitrary,
fmap LongConstant arbitrary,
return NullConstant,
fmap StringConstant arbitrary,
fmap ClassConstant arbitrary]
instance Arbitrary AtIdentifier where
arbitrary = oneof $ [
return ThisRef,
return CaughtExceptionRef] ++ replicate 4 (fmap ParameterRef arbitrary)
instance Arbitrary Variable where
arbitrary = oneof [
fmap ReferenceVar arbitrary,
fmap LocalVar arbitrary]
instance Arbitrary ERef where
arbitrary = oneof [
liftM2 ArrayRef arbitraryLocalName arbitrary,
liftM2 FieldRef arbitraryLocalName arbitrary,
fmap SignatureRef arbitrary]
instance Arbitrary EInvoke where
arbitrary = oneof [
liftM3 SpecialInvoke arbitraryLocalName arbitrary arbitrary,
liftM3 VirtualInvoke arbitraryLocalName arbitrary arbitrary,
liftM3 InterfaceInvoke arbitraryLocalName arbitrary arbitrary,
liftM2 StaticInvoke arbitrary arbitrary,
liftM5 DynamicInvoke arbitraryLocalName arbitrary arbitrary arbitrary arbitrary]
instance Arbitrary BoolOp where
arbitrary = oneof $ map return [Cmpeq, Cmpne, Cmpgt, Cmpge, Cmplt, Cmple]
instance Arbitrary Binop where
arbitrary = oneof $ map return [And, Or, Xor, Shl, Shr, Ushr,
Cmp, Cmpg, Cmpl,
Plus, Minus, Mult, Div, Rem]
data Unop
= Lengthof
| Neg deriving (Show, Eq)
instance Arbitrary Unop where
arbitrary = oneof $ map return [Lengthof, Neg]
......@@ -37,22 +37,22 @@ jimpleSoundness
evalCon evalAbs
runStatementsCon runStatementsAbs
runProgramCon runProgramAbs = do
soundImmediate "Literals" emptyMem id evalImmediateCon evalImmediateAbs
soundImmediate "Localvar literal"
toMem
(\() -> Local "a")
soundImmediate 50 "Literals" emptyMem id evalImmediateCon evalImmediateAbs
soundImmediate 10 "Localvar literal"
toMem (\() -> Local "a")
evalImmediateCon evalImmediateAbs
soundBoolExpr "Boolean expressions" emptyMem id evalBoolCon evalBoolAbs
soundBoolExpr 100 "Boolean expressions" emptyMem id evalBoolCon evalBoolAbs
soundExpr "Unary operations" emptyMem (uncurry UnopExpr) evalCon evalAbs
soundExpr "Binary operations" emptyMem (\(x,op,y) ->
BinopExpr (IntConstant x) op (IntConstant y)
) evalCon evalAbs
soundExpr 100 "Unary operations" emptyMem (uncurry UnopExpr) evalCon evalAbs
soundExpr 100 "Binary operations" emptyMem (uncurry3 BinopExpr) evalCon evalAbs
soundExpr 1000 "General expressions" emptyMem id evalCon evalAbs
soundExpr "General expressions" emptyMem id evalCon evalAbs
soundStatements 1000 "Single statements" toMem (:[]) runStatementsCon runStatementsAbs
where
uncurry3 :: (a -> b -> c -> d) -> ((a,b,c) -> d)
uncurry3 f = (\(a,b,c) -> f a b c)
emptyMem :: () -> [(String,vc)]
emptyMem = const []
toMem :: [vc] -> [(String,vc)]
......
......@@ -19,9 +19,6 @@ import Test.Hspec
import Test.QuickCheck
import Test.Hspec.Core.QuickCheck (modifyMaxSuccess)
withSize :: Spec -> Spec
withSize = modifyMaxSuccess (const 1000)
shouldBeApproximated :: (HasCallStack,Galois (Con.Pow c) a,Show a,Show c) => c -> a -> Expectation
c `shouldBeApproximated` a = unless (ca a) (expectationFailure msg)
where ca = alpha (singleton c)
......@@ -30,13 +27,13 @@ c `shouldBeApproximated` a = unless (ca ⊑ a) (expectationFailure msg)
soundImmediate :: (Arbitrary a,Show a,
Arbitrary b,Show b,
Galois (Con.Pow vc) va,Complete va,Eq vc,Hashable vc,Show vc,Show va) =>