Cleanup Jimpl code

jimple/package.yaml

@@ -15,6 +15,7 @@ dependencies:
   - profunctors
   - mtl
   - random
+  - sturdy-arrows
   - sturdy-lib
   - text
   - vector

jimple/src/ConcreteInterpreter.hs

@@ -14,133 +14,133 @@
 {-# LANGUAGE UndecidableInstances #-}
 module ConcreteInterpreter where
 
-import           Prelude hiding (id,fail,lookup,read)
-
-import           Data.Bits
-import           Data.Fixed
-import           Data.Hashable (Hashable)
-import           Data.List (replicate,repeat,find,splitAt)
-import           Data.Int
-import           Data.Word
-import           Data.Text(Text)
-import qualified Data.Text as T
-import           Data.HashMap.Lazy (HashMap)
-import qualified Data.HashMap.Lazy as Map
-
--- import           Data.Concrete.Error
--- import           Data.Concrete.Exception
-
-import           Control.Monad (return,fmap,replicateM)
-import           Control.Category hiding ((.))
-
-import           Control.Arrow hiding ((<+>))
-import           Control.Arrow.Const
-import           Control.Arrow.Environment
-import           Control.Arrow.Except
-import           Control.Arrow.Fail
-import           Control.Arrow.Fix
-import           Control.Arrow.Reader
-import           Control.Arrow.State
-import           Control.Arrow.Store
-import qualified Control.Arrow.Trans as Trans
-import qualified Control.Arrow.Utils as U
-
-import           Control.Arrow.Transformer.Const
-import           Control.Arrow.Transformer.Reader
-import           Control.Arrow.Transformer.State
-import           Control.Arrow.Transformer.Value
-import           Control.Arrow.Transformer.Concrete.Except
-import           Control.Arrow.Transformer.Concrete.Environment
-import           Control.Arrow.Transformer.Concrete.Failure
-import           Control.Arrow.Transformer.Concrete.Store
-
-import           Syntax
-import           GenericInterpreter (Frame,PC,IsVal)
-import qualified GenericInterpreter as Generic
-
-import           GHC.Generics(Generic)
-import           Data.Profunctor
-
-import           Text.Printf
-
-data Val
-  = IntVal Int32
-  | LongVal Int64
-  | FloatVal Float
-  | DoubleVal Double
-  | StringVal Text
-  -- | ClassVal Text
-  | NullVal
-  | RefVal Addr
-  | ArrayVal [Val]
-  | ObjectVal ClassId Object
-  deriving stock (Eq,Generic)
-  deriving anyclass (Hashable)
-
-type Object = HashMap FieldName Val
-type Exception = Val
-type Env = Frame Val
-type Addr = Word64
-data Store = Store
-  { dynamicStore :: HashMap Addr Val
-  , staticStore :: HashMap ClassId Object
-  , nextAddress :: Addr
-  }
-
-run :: ClassTable -> ClassId -> MethodSignature -> (Store,Exception)
-run classTable mainClass mainMethod = _ $
-  Trans.run
-   (Generic.run ::
-     ValueT Val
-     (ConstT ClassTable
-      (EnvT Env
-       (ExceptT Exception
-        (StoreT Store
-         (FailureT Text
-          (->)))))) PC Val)
-    classTable
-    (emptyStore,(_frame,0))
-
-instance (ArrowChoice c, Profunctor c) => ArrowEnv Variable Val (EnvT Env c) where
-  type Join y (EnvT Env c) = ()
-  lookup = _
-  extend = _
-
-instance IsVal Val (ValueT Val c) where
-  type JoinVal y (ValueT Val c) = ()
-  if_ = _
-  tableswitch = _
-  lookupswitch = _
-  lookupMethod = _
-  matchException = _
-  new = _
-  newArray = _
-  void = _
-  doubleConstant = _
-  floatConstant = _
-  intConstant = _
-  longConstant = _
-  nullConstant = _
-  stringConstant = _
-  and = _
-  or = _
-  xor = _
-  rem = _
-  mod = _
-  cmp = _
-  cmpg = _
-  cmpl = _
-  shl = _
-  shr = _
-  ushr = _
-  plus = _
-  minus = _
-  mult = _
-  lengthOf = _
-  div = _
-  neg = _
-  cast = _
-  instanceOf = _
+-- import           Prelude hiding (id,fail,lookup,read)
+
+-- import           Data.Bits
+-- import           Data.Fixed
+-- import           Data.Hashable (Hashable)
+-- import           Data.List (replicate,repeat,find,splitAt)
+-- import           Data.Int
+-- import           Data.Word
+-- import           Data.Text(Text)
+-- import qualified Data.Text as T
+-- import           Data.HashMap.Lazy (HashMap)
+-- import qualified Data.HashMap.Lazy as Map
+
+-- -- import           Data.Concrete.Error
+-- -- import           Data.Concrete.Exception
+
+-- import           Control.Monad (return,fmap,replicateM)
+-- import           Control.Category hiding ((.))
+
+-- import           Control.Arrow hiding ((<+>))
+-- import           Control.Arrow.Const
+-- import           Control.Arrow.Environment
+-- import           Control.Arrow.Except
+-- import           Control.Arrow.Fail
+-- import           Control.Arrow.Fix
+-- import           Control.Arrow.Reader
+-- import           Control.Arrow.State
+-- import           Control.Arrow.Store
+-- import qualified Control.Arrow.Trans as Trans
+-- import qualified Control.Arrow.Utils as U
+
+-- import           Control.Arrow.Transformer.Const
+-- import           Control.Arrow.Transformer.Reader
+-- import           Control.Arrow.Transformer.State
+-- import           Control.Arrow.Transformer.Value
+-- import           Control.Arrow.Transformer.Concrete.Except
+-- import           Control.Arrow.Transformer.Concrete.Environment
+-- import           Control.Arrow.Transformer.Concrete.Failure
+-- import           Control.Arrow.Transformer.Concrete.Store
+
+-- import           Syntax
+-- import           GenericInterpreter (Frame,PC,IsVal)
+-- import qualified GenericInterpreter as Generic
+
+-- import           GHC.Generics(Generic)
+-- import           Data.Profunctor
+
+-- import           Text.Printf
+
+-- data Val
+--   = IntVal Int32
+--   | LongVal Int64
+--   | FloatVal Float
+--   | DoubleVal Double
+--   | StringVal Text
+--   -- | ClassVal Text
+--   | NullVal
+--   | RefVal Addr
+--   | ArrayVal [Val]
+--   | ObjectVal ClassId Object
+--   deriving stock (Eq,Generic)
+--   deriving anyclass (Hashable)
+
+-- type Object = HashMap FieldName Val
+-- type Exception = Val
+-- type Env = Frame Val
+-- type Addr = Word64
+-- data Store = Store
+--   { dynamicStore :: HashMap Addr Val
+--   , staticStore :: HashMap ClassId Object
+--   , nextAddress :: Addr
+--   }
+
+-- run :: ClassTable -> ClassId -> MethodSignature -> (Store,Exception)
+-- run classTable mainClass mainMethod = _ $
+--   Trans.run
+--    (Generic.run ::
+--      ValueT Val
+--      (ConstT ClassTable
+--       (EnvT Env
+--        (ExceptT Exception
+--         (StoreT Store
+--          (FailureT Text
+--           (->)))))) PC Val)
+--     classTable
+--     (emptyStore,(_frame,0))
+
+-- instance (ArrowChoice c, Profunctor c) => ArrowEnv Variable Val (EnvT Env c) where
+--   type Join y (EnvT Env c) = ()
+--   lookup = _
+--   extend = _
+
+-- instance IsVal Val (ValueT Val c) where
+--   type JoinVal y (ValueT Val c) = ()
+--   if_ = _
+--   tableswitch = _
+--   lookupswitch = _
+--   lookupMethod = _
+--   matchException = _
+--   new = _
+--   newArray = _
+--   void = _
+--   doubleConstant = _
+--   floatConstant = _
+--   intConstant = _
+--   longConstant = _
+--   nullConstant = _
+--   stringConstant = _
+--   and = _
+--   or = _
+--   xor = _
+--   rem = _
+--   mod = _
+--   cmp = _
+--   cmpg = _
+--   cmpl = _
+--   shl = _
+--   shr = _
+--   ushr = _
+--   plus = _
+--   minus = _
+--   mult = _
+--   lengthOf = _
+--   div = _
+--   neg = _
+--   cast = _
+--   instanceOf = _
 
 -- type Constants = ([CompilationUnit],Map FieldSignature Addr)
 
@@ -508,17 +508,17 @@ instance IsVal Val (ValueT Val c) where
 --   DynamicException v -> deepDeref >>^ DynamicException -< v
 --   StaticException _ -> returnA -< e
 
-instance Show Val where
-  show (IntVal n) = show n
-  show (LongVal l) = show l ++ "l"
-  show (FloatVal f) = show f
-  show (DoubleVal d) = show d ++ "d"
-  show (StringVal s) = T.unpack s
-  -- show (ClassVal c) = "<" ++ c ++ ">"
-  show NullVal = "null"
-  show (RefVal a) = "@" ++ show a
-  show (ArrayVal xs) = show xs
-  show (ObjectVal c m) = show c ++ "{" ++ show m ++ "}"
-
-emptyStore :: Store
-emptyStore = Store { dynamicStore = Map.empty, staticStore = Map.empty, nextAddress = 0 }
+-- instance Show Val where
+--   show (IntVal n) = show n
+--   show (LongVal l) = show l ++ "l"
+--   show (FloatVal f) = show f
+--   show (DoubleVal d) = show d ++ "d"
+--   show (StringVal s) = T.unpack s
+--   -- show (ClassVal c) = "<" ++ c ++ ">"
+--   show NullVal = "null"
+--   show (RefVal a) = "@" ++ show a
+--   show (ArrayVal xs) = show xs
+--   show (ObjectVal c m) = show c ++ "{" ++ show m ++ "}"
+
+-- emptyStore :: Store
+-- emptyStore = Store { dynamicStore = Map.empty, staticStore = Map.empty, nextAddress = 0 }

jimple/src/GenericInterpreter.hs

-{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE Arrows #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE OverloadedStrings #-}
 module GenericInterpreter where
 
 import Prelude hiding (rem,mod,div,id,or,and,fail,return,map)
@@ -26,8 +27,8 @@ import Control.Arrow
 import Control.Arrow.Environment as Env
 import Control.Arrow.Frame as Frame
 import Control.Arrow.Except as Except
-import Control.Arrow.Fail
-import Control.Arrow.Fix (ArrowFix(..))
+import Control.Arrow.Fail as Fail
+import Control.Arrow.Fix (ArrowFix(..),FixpointAlgorithm)
 import Control.Arrow.Utils (map)
 
 import GHC.Exts
@@ -52,12 +53,17 @@ type StmtInterpreter val c = c PC val
 type ArrowInterp addr val err c =
   ( IsString err, IsVal val c
   , ArrowChoice c
-  , ArrowFrame (Frame addr) c
+  , ArrowFrame (Frame val) c
   , ArrowEnv Variable val c
   , ArrowExcept val c
   , ArrowFail err c
   , ArrowFix (StmtInterpreter val c)
-  , JoinVal () c, JoinVal val c, Env.Join val c, Except.Join val c
+  , ?fixpointAlgorithm :: FixpointAlgorithm (Fix (c Label val))
+  , JoinVal () c
+  , JoinVal val c
+  , Env.Join val c
+  , Except.Join val c
+  , Fail.Join val c
   )
 
 eval :: ArrowInterp addr val err c => StmtInterpreter val c -> c Expr val
@@ -118,7 +124,7 @@ evalImmediate = proc i -> case i of
   ClassConstant c -> fail -< "Unsupported operation: ClassConstant"
 {-# INLINE evalImmediate #-}
 
-evalInvoke :: ArrowInterp addr val err c => StmtInterpreter val c -> c Invoke val
+evalInvoke :: forall addr val err c. ArrowInterp addr val err c => StmtInterpreter val c -> c Invoke val
 evalInvoke run' = proc e -> case e of
   InvokeVirtual obj klass methodSig args -> do
     receiver <- lookup' -< obj

jimple/src/NullnessSemantics.hs

-{-# LANGUAGE Arrows #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-module NullnessSemantics where
-
-import           Prelude hiding (lookup,read,fail,Bounded(..))
-
-import qualified Data.Boolean as B
-import           Data.Order
-import           Data.String (fromString)
-
-import qualified Data.Abstract.Boolean as Abs
-import           Data.Abstract.Environment (Env)
-import qualified Data.Abstract.Environment as E
-import qualified Data.Abstract.Equality as Abs
-import           Data.Abstract.Exception
-import           Data.Abstract.HandleError
-import qualified Data.Abstract.Store as S
-
-import           Control.Category hiding ((.))
-
-import           Control.Arrow
-import           Control.Arrow.Const
-import           Control.Arrow.Environment
-import           Control.Arrow.Except
-import           Control.Arrow.Fail
-import           Control.Arrow.Fix
-import           Control.Arrow.Reader
-import           Control.Arrow.Store
-import           Control.Arrow.Abstract.Join
-import qualified Control.Arrow.Utils as U
-
-import           Control.Arrow.Transformer.Const
-import           Control.Arrow.Transformer.Reader
-import           Control.Arrow.Transformer.State
-import           Control.Arrow.Transformer.Abstract.HandleExcept
-import           Control.Arrow.Transformer.Abstract.Environment
-import           Control.Arrow.Transformer.Abstract.Store
-
-import           Syntax
-import           SharedSemantics
-
-import           Data.GaloisConnection
-import qualified Data.Concrete.Powerset as Con
-import qualified ConcreteSemantics as Con
-
-import           Text.Printf
-
-data Val
-  = Bottom
-  | Null
-  | NonNull
-  | Top deriving (Eq)
-
-instance Show Val where
-  show Bottom = "⊥"
-  show Null = "Null"
-  show NonNull = "NonNull"
-  show Top = "⊤"
-
-instance Abs.Equality Val where
-  Top == _ = Abs.Top
-  _ == Top = Abs.Top
-  Null == Null = Abs.True
-  NonNull == NonNull = Abs.Top
-  Bottom == Bottom = Abs.True
-  _ == _ = Abs.False
-
-instance PreOrd Val where
-  Bottom ⊑ _ = True
-  _ ⊑ Top = True
-  Null ⊑ Null = True
-  NonNull ⊑ NonNull = True
-  _ ⊑ _ = False
-
-instance Complete Val where
-  Bottom ⊔ v = v
-  v ⊔ Bottom = v
-  Null ⊔ Null = Null
-  NonNull ⊔ NonNull = NonNull
-  _ ⊔ _ = top
-
-instance UpperBounded Val where
-  top = Top
-
-instance LowerBounded Val where
-  bottom = Bottom
-
-instance Galois (Con.Pow Con.Val) Val where
-  alpha = lifted $ \v -> case v of
-    Con.NullVal -> Null
-    _ -> NonNull
-  gamma = error "noncomputable"
-
-type Context = ([Statement],[CatchClause])
-
-newtype Interp x y = Interp
-  (Except (Exception Val)
-    (Reader Context
-      (Environment String Val
-        (StoreArrow FieldSignature Val
-          (Const [CompilationUnit]
-            (->))))) x y)
-  deriving (Category,Arrow,ArrowChoice)
-
-deriving instance ArrowConst [CompilationUnit] Interp
-deriving instance Complete y => ArrowExcept x y (Exception Val) Interp
-deriving instance ArrowFail (Exception Val) Interp
-deriving instance ArrowFix [Statement] (Maybe Val) Interp
-deriving instance ArrowEnv String Val (Env String Val) Interp
-deriving instance ArrowJoin Interp
-deriving instance ArrowReader Context Interp
-deriving instance ArrowRead FieldSignature Val x Val Interp
-deriving instance ArrowWrite FieldSignature Val Interp
-
--- This instance is not in lib because it interferes with an instance in Stratego
-instance (LowerBounded e,LowerBounded a) => LowerBounded (Error e a) where
-  bottom = SuccessOrFail bottom bottom
-
-deriving instance PreOrd y => PreOrd (Interp x y)
-deriving instance (Complete y) => Complete (Interp x y)
-deriving instance LowerBounded y => LowerBounded (Interp x y)
-
-runInterp :: Interp x y ->
-             [CompilationUnit] -> [(String,Val)] -> x ->
-             Error (Exception Val) y
-runInterp (Interp f) compilationUnits mem x =
-  runConst compilationUnits
-    (evalStore
-      (runEnvironment'
-        (runReader
-          (runExcept f))))
-  (fields,(mem,(([],[]),x)))
-  where
-    fields = S.fromList $ zip
-      (concatMap (getFieldSignatures (\m -> Static `elem` m)) compilationUnits)
-      (repeat Bottom)
-
-type Out v = Error (Exception Val) v
-type Mem = [(String,Val)]
-
-runProgram' :: [CompilationUnit] -> (MethodSignature,[Immediate]) -> Out (Maybe Val)
-runProgram' units = runInterp runProgram units []
-
-runStatements' :: [CompilationUnit] -> Mem -> [Statement] -> Out (Maybe Val)
-runStatements' = runInterp (initStatements runStatements)
-
-eval' :: [CompilationUnit] -> Mem -> Expr -> Out Val
-eval' = runInterp eval
-
-evalBool' :: [CompilationUnit] -> Mem -> BoolExpr -> Out Abs.Bool
-evalBool' = runInterp evalBool
-
-evalImmediate' :: [CompilationUnit] -> Mem -> Immediate -> Out Val
-evalImmediate' = runInterp evalImmediate
-
----- Instances -----------------------------------------------------------------
-
-instance UseVal Val Interp where
-  newSimple = proc t -> case t of
-    RefType c -> do
-      readCompilationUnit -< c
-      returnA -< NonNull
-    NullType -> returnA -< Null
-    _ -> returnA -< NonNull
-  newArray = proc _ -> joined returnA failStatic -<
-    (NonNull,"Expected an integer array size")
-  and = binopInteger
-  or = binopInteger
-  xor = binopInteger
-  rem = binopNum
-  cmp = proc _ -> joined returnA failStatic -<
-    (NonNull,"Expected long variables for 'cmp'")
-  cmpg = proc _ -> joined returnA failStatic -<
-    (NonNull,"Expected floating variables for 'cmpg'")
-  cmpl = proc _ -> joined returnA failStatic -<
-    (NonNull,"Expected floating variables for 'cmpl'")
-  shl = binopInteger
-  shr = binopInteger
-  ushr = binopInteger
-  plus = binopNum
-  minus = binopNum
-  mult = binopNum
-  div = proc (v1,v2) -> joined returnA (joined failDynamic failStatic) -< (v1 ⊔ v2,
-    (NonNull,"Expected numeric variables for 'div'"))
-  lengthOf = proc v -> joined returnA failStatic -<
-    (v,"Expected an array variable for 'lengthOf'")
-  neg = proc v -> joined returnA failStatic -<
-    (v,"Expected a number as argument for -")
-  doubleConstant = arr $ const NonNull
-  floatConstant = arr $ const NonNull
-  intConstant = arr $ const NonNull
-  longConstant = arr $ const NonNull
-  nullConstant = arr $ const Null
-  stringConstant = arr $ const NonNull
-  classConstant = arr $ const NonNull
-  defaultValue = arr (\t -> case t of
-    NullType      -> Null
-    (RefType _)   -> Null
-    (ArrayType _) -> Null
-    UnknownType   -> top
-    VoidType      -> bottom
-    _             -> NonNull)
-  instanceOf = arr $ const NonNull
-  cast = proc ((v,_),_) -> joined returnA (joined failDynamic failStatic) -< (v,
-    (NonNull,"Casting of primivites and arrays is not yet supported"))
-  declare f = (\((l,v),x) -> (l,v,x)) ^>> extendEnv' f
-  readVar = lookup_
-  updateVar f = proc ((l,v),x) -> do
-    lookup_ -< l
-    extendEnv' f -< (l,v,x)
-  readIndex = proc (v,_) -> case v of
-    Bottom -> returnA -< bottom
-    Null -> failDynamic -< NonNull
-    NonNull -> returnA -< top
-    Top -> joined returnA failDynamic -< (top,NonNull)
-  updateIndex f = first (first readIndex) >>> U.pi2 >>> f
-  readField = proc (v,FieldSignature _ t _) -> case v of
-    Bottom -> returnA -< bottom
-    Null -> failDynamic -< NonNull
-    NonNull -> defaultValue >>^ (⊔ NonNull) -< t
-    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 "Field %s not bound" (show f))
-  updateStaticField = proc (f,v) -> do
-    readStaticField -< f
-    write -< (f,v)
-  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
-    StaticException _ -> fail -< ex
-    DynamicException v ->
-      joined (lubA f) failDynamic -< (zip (repeat v) clauses