diff --git a/Folds.hs b/Folds.hs new file mode 100644 index 0000000000000000000000000000000000000000..d9002bfe0daacd5da8115fa2e475698a3915ca07 --- /dev/null +++ b/Folds.hs @@ -0,0 +1,109 @@ +-- Folds over Java data structures +module Folds where + +import Language.Java.Syntax + +type StmtAlgebra r = (Block -> r, + Exp -> r -> r, + Exp -> r -> r -> r, + Exp -> r -> r, + (Maybe ForInit) -> (Maybe Exp) -> (Maybe [Exp]) -> r -> r, + [Modifier] -> Type -> Ident -> Exp -> r -> r, + r, + Exp -> r, + Exp -> (Maybe Exp) -> r, + Exp -> [SwitchBlock] -> r, + r -> Exp -> r, + Maybe Ident -> r, + Maybe Ident -> r, + Maybe Exp -> r, + Exp -> Block -> r, + Exp -> r, + Block -> [Catch] -> (Maybe Block) -> r, + Ident -> r -> r + ) + +type ExpAlgebra r = (Literal -> r, + Maybe Type -> r, + r, + Name -> r, + [TypeArgument] -> ClassType -> [Argument] -> (Maybe ClassBody) -> r, + r -> [TypeArgument] -> Ident -> [Argument] -> (Maybe ClassBody) -> r, + Type -> [r] -> Int -> r, + Type -> Int -> ArrayInit -> r, + FieldAccess -> r, + MethodInvocation -> r, + ArrayIndex -> r, + Name -> r, + r -> r, + r -> r, + r -> r, + r -> r, + r -> r, + r -> r, + r -> r, + r -> r, + Type -> r -> r, + r -> Op -> r -> r, + r -> RefType -> r, + r -> r -> r -> r, + Lhs -> AssignOp -> r -> r, + LambdaParams -> LambdaExpression -> r, + Ident -> Ident -> r + ) + + +-- | A fold function over a java statement. +foldStmt :: StmtAlgebra r -> Stmt -> r +foldStmt (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhancedFor, fEmpty, fExpStmt, fAssert, fSwitch, fDo, fBreak, fContinue, fReturn, fSynchronized, fThrow, fTry, fLabeled) s = fold s where + fold s = case s of + StmtBlock b -> fStmtBlock b + IfThen e stmt -> fIfThen e (fold stmt) + IfThenElse e stmt1 stmt2 -> fIfThenElse e (fold stmt1) (fold stmt2) + While e stmt -> fWhile e (fold stmt) + BasicFor init e incr stmt -> fBasicFor init e incr (fold stmt) + EnhancedFor mods t i e stmt -> fEnhancedFor mods t i e (fold stmt) + Empty -> fEmpty + ExpStmt e -> fExpStmt e + Assert e me -> fAssert e me + Switch e bs -> fSwitch e bs + Do stmt e -> fDo (fold stmt) e + Break l -> fBreak l + Continue l -> fContinue l + Return me -> fReturn me + Synchronized e b -> fSynchronized e b + Throw e -> fThrow e + Try b cs f -> fTry b cs f + Labeled l stmt -> fLabeled l (fold stmt) + +-- | A fold function over a java expression. +foldExp :: ExpAlgebra r -> Exp -> r +foldExp (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) e = fold e where + fold e = case e of + Lit lit -> fLit lit + ClassLit mt -> fClassLit mt + This -> fThis + ThisClass name -> fThisClass name + InstanceCreation typeArgs classType args mBody -> fInstanceCreation typeArgs classType args mBody + QualInstanceCreation e typeArgs ident args mBody -> fQualInstanceCreation (fold e) typeArgs ident args mBody + ArrayCreate t exps dim -> fArrayCreate t (map fold exps) dim + ArrayCreateInit t dim arrayInit -> fArrayCreateInit t dim arrayInit + FieldAccess fieldAccess -> fFieldAccess fieldAccess + MethodInv invocation -> fMethodInv invocation + ArrayAccess i -> fArrayAccess i + ExpName name -> fExpName name + PostIncrement e -> fPostIncrement (fold e) + PostDecrement e -> fPostDecrement (fold e) + PreIncrement e -> fPreIncrement (fold e) + PreDecrement e -> fPreDecrement (fold e) + PrePlus e -> fPrePlus (fold e) + PreMinus e -> fPreMinus (fold e) + PreBitCompl e -> fPreBitCompl (fold e) + PreNot e -> fPreNot (fold e) + Cast t e -> fCast t (fold e) + BinOp e1 op e2 -> fBinOp (fold e1) op (fold e2) + InstanceOf e refType -> fInstanceOf (fold e) refType + Cond g e1 e2 -> fCond (fold g) (fold e1) (fold e2) + Assign lhs assOp e -> fAssign lhs assOp (fold e) + Lambda lParams lExp -> fLambda lParams lExp + MethodRef className methodName -> fMethodRef className methodName \ No newline at end of file diff --git a/Main.hs b/Main.hs new file mode 100644 index 0000000000000000000000000000000000000000..d2ee17bb8eb8abee4d5e95fa06108db5b503c3ae --- /dev/null +++ b/Main.hs @@ -0,0 +1,39 @@ +module Main where + +import Language.Java.Syntax +import Language.Java.Lexer +import Language.Java.Parser + +import WLP + + + + + +import Language.Java.Pretty + + +main :: IO () +main = do + source <- readFile "A:\\Thesis\\Test1.java" + + + let result = parser compilationUnit source + + + case result of + Left error -> print error + Right compUnit -> putStrLn . prettyPrint $ wlp (getStmt compUnit) postCond + + +-- Gets the statement(-block) defining the main method for simple tests +getStmt :: CompilationUnit -> Stmt +getStmt (CompilationUnit _ _ [ClassTypeDecl (ClassDecl _ _ _ _ _ (ClassBody decls))]) = getInit decls where + getInit [] = error "No main method" + getInit [MemberDecl (MethodDecl _ _ _ (Ident "main") _ _ (MethodBody (Just b)))] = StmtBlock b + getInit (_:decls) = getInit decls + + +-- The post-condition (for testing) +postCond :: Exp +postCond = BinOp (ExpName (Name [Ident "x"])) Equal (Lit (Int 1)) \ No newline at end of file diff --git a/Substitute.hs b/Substitute.hs new file mode 100644 index 0000000000000000000000000000000000000000..c1c157ab8bfbf1611d58a12a0868be49bd9020b8 --- /dev/null +++ b/Substitute.hs @@ -0,0 +1,66 @@ +module Substitute where + +import Language.Java.Syntax + +import Folds + + +substVarExpAlgebra :: ExpAlgebra ((Lhs, Exp) -> Exp) +substVarExpAlgebra = (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 _ = Lit lit + fClassLit mt _ = ClassLit mt + fThis _ = This + fThisClass name _ = ThisClass name + fInstanceCreation typeArgs classType args mBody _ = InstanceCreation typeArgs classType args mBody + fQualInstanceCreation e typeArgs ident args mBody inh = QualInstanceCreation (e inh) typeArgs ident args mBody + fArrayCreate t exps dim inh = ArrayCreate t (map ($ inh) exps) dim + fArrayCreateInit t dim arrayInit _ = ArrayCreateInit t dim arrayInit + fFieldAccess fieldAccess (lhs, rhs) = case lhs of + FieldLhs fieldAccess' -> case fieldAccess of + PrimaryFieldAccess e ident -> error "todo: fieldAccess substitution" + SuperFieldAccess ident -> error "todo: fieldAccess substitution" + ClassFieldAccess name ident -> error "todo: fieldAccess substitution" + fMethodInv invocation _ = MethodInv invocation + fArrayAccess (ArrayIndex a is) (lhs, rhs) = case lhs of + ArrayLhs arrayIndex -> error "todo: array substitution" + fExpName name (lhs, rhs) = case lhs of + NameLhs name' -> if name == name' then rhs else ExpName name + fPostIncrement e inh = PostIncrement (e inh) + fPostDecrement e inh = PostDecrement (e inh) + fPreIncrement e inh = PreIncrement (e inh) + fPreDecrement e inh = PreDecrement (e inh) + fPrePlus e inh = PrePlus (e inh) + fPreMinus e inh = PreMinus (e inh) + fPreBitCompl e inh = PreBitCompl (e inh) + fPreNot e inh = PreNot (e inh) + fCast t e inh = Cast t (e inh) + fBinOp e1 op e2 inh = BinOp (e1 inh) op (e2 inh) + fInstanceOf e refType inh = InstanceOf (e inh) refType + fCond g e1 e2 inh = Cond (g inh) (e1 inh) (e2 inh) + fAssign lhs assOp e inh = Assign lhs assOp (e inh) -- TODO + fLambda lParams lExp _ = Lambda lParams lExp + fMethodRef className methodName _ = MethodRef className methodName + +-- | Desugars to a basic assignment, returning the new righ hand side. For example: desugaring x += 3 returns the new rhs x + 3 +desugarAssign :: Lhs -> AssignOp -> Exp -> Exp +desugarAssign lhs op e = case op of + EqualA -> e + MultA -> BinOp e Mult (lhsToExp lhs) + DivA -> BinOp e Div (lhsToExp lhs) + RemA -> BinOp e Rem (lhsToExp lhs) + AddA -> BinOp e Add (lhsToExp lhs) + SubA -> BinOp e Sub (lhsToExp lhs) + LShiftA -> BinOp e LShift (lhsToExp lhs) + RShiftA -> BinOp e RShift (lhsToExp lhs) + RRShiftA -> BinOp e RRShift (lhsToExp lhs) + AndA -> BinOp e And (lhsToExp lhs) + XorA -> BinOp e Xor (lhsToExp lhs) + OrA -> BinOp e Or (lhsToExp lhs) + where + lhsToExp (NameLhs name) = ExpName name + lhsToExp (FieldLhs fieldAccess) = undefined + lhsToExp (ArrayLhs arrayIndex) = undefined + +-- | Substitutes all occurences of a specific free variable by an expression +substVar :: Lhs -> Exp -> Exp -> Exp +substVar lhs rhs e = foldExp substVarExpAlgebra e (lhs, rhs) \ No newline at end of file