From cdee1177ae3e73eb54373da18451ff3dbca300c9 Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Tue, 27 Sep 2016 21:48:57 +0200
Subject: [PATCH] blocks (sequences of statements) are now handled correctly
w.r.t. dealing with statements that pass control in different ways
---
WLP.hs | 84 ++++++++++++++++++++++++++++++++++++++--------------------
1 file changed, 55 insertions(+), 29 deletions(-)
diff --git a/WLP.hs b/WLP.hs
index c3e4624..c13baaa 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -3,11 +3,11 @@ module WLP where
import Language.Java.Syntax
import Language.Java.Lexer
import Language.Java.Parser
+import Data.Maybe
import Verifier
-
type StmtAlgebra r = (Block -> r,
Exp -> r -> r,
Exp -> r -> r -> r,
@@ -29,6 +29,19 @@ type StmtAlgebra r = (Block -> r,
)
+-- Some constants:
+
+-- Differentiate between different exceptions?
+diffExc :: Bool
+diffExc = False
+
+true :: Exp
+true = Lit (Boolean True)
+
+false :: Exp
+false = Lit (Boolean False)
+
+
-- Logical operators for expressions:
(&*) :: Exp -> Exp -> Exp
e1 &* e2 = BinOp e1 And e2
@@ -58,37 +71,43 @@ foldStmt (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhancedFor, fEm
-- | A type synonym for the inherited attribute
-
-
-type Inh = (Exp -> Exp, -- The accumulated transformer up till the last loop (this is used when handling break statements etc.)
- Exp -> Exp -- The wlp of the current loop statement not including initialization code. It refers to the loop starting from the loop continuation point.
+type Inh = (Exp -> Exp, -- The accumulated transformer of the current block up until the current statement
+ Exp -> Exp, -- The accumulated transformer up until the last loop (this is used when handling break statements etc.)
+ Exp -> Exp, -- The wlp of the current loop statement not including initialization code. It refers to the loop starting from the loop continuation point.
+ Maybe ([Catch], Bool) -- The catches when executing a block in a try statement, and a Bool indicating wether there is a finally-block
)
+
+-- | A type synonym for the synthesized attribute
+type Syn = Exp -> Exp
-- | The algebra that defines the wlp transformer for statements
-- The synthesized attribute is the resulting transformer.
-wlpStmtAlgebra :: StmtAlgebra (Inh -> Exp -> Exp)
+-- Statements that pass control to the next statement have to explicitly combine their wlp function with the accumulated function, as some statements (e.g. break) ignore the accumulated function.
+wlpStmtAlgebra :: StmtAlgebra (Inh -> Syn)
wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhancedFor, fEmpty, fExpStmt, fAssert, fSwitch, fDo, fBreak, fContinue, fReturn, fSynchronized, fThrow, fTry, fLabeled) where
- fStmtBlock (Block bs) inh = foldr ((.) . wlpBlock inh) id bs
- fIfThen e s1 = fIfThenElse e s1 (const id)
- fIfThenElse e s1 s2 inh = (\q -> (e &* s1 inh q) |* (neg e &* s2 inh q))
- fWhile e s (acc, _) = let loop = (\q -> if isTrue (((inv &* neg e) `imp` q) &* ((inv &* e) `imp` s (acc, loop) inv)) then inv else (neg e &* q)) in loop
- fBasicFor init e incr s inh@(acc, _) = wlp' inh (initToStmt init) . let loop = fWhile (fromMaybeGuard e) (\inh' -> s (acc, loop) . wlp' inh' (incrToStmt incr)) inh in loop
- fEnhancedFor = error "TODO: EnhancedFor"
- fEmpty inh = id
- fExpStmt = error "TODO: ExpStmt"
- fAssert e _ inh = (e &*)
- fSwitch e bs inh = let (e', s1, s2) = desugarSwitch e bs in fIfThenElse e' (flip wlp' s1) (flip wlp' s2) inh
- fDo s e (acc, _) = let loop = s (acc, loop) . fWhile e s (acc, loop) in loop -- Do is just a while with the statement block executed one additional time. Break and continue still have to be handled in this additional execution.
- fBreak _ (acc, _) = acc
- fContinue _ (acc, loop) = loop . acc
- fReturn = undefined
- fSynchronized = undefined
- fThrow = undefined
- fTry = undefined
- fLabeled = undefined
+ fStmtBlock (Block bs) (acc, br, loop, catch) = foldr (\b r -> wlpBlock (r, br, loop, catch) b) acc bs -- The result of the last block-statement will be the accumulated transformer for the second-last etc.
+ fIfThen e s1 = fIfThenElse e s1 (const id) -- if-then is just an if-then-else with an empty else-block
+ fIfThenElse e s1 s2 inh@(acc, _, _, _) = (\q -> (e &* s1 inh q) |* (neg e &* s2 inh q)) . acc
+ fWhile e s (acc, br, _, catch) = let loop = (\q -> if isTrue (((inv &* neg e) `imp` q) &* ((inv &* e) `imp` s (id, br, loop, catch) inv)) then inv else (neg e &* q)) in loop . acc
+ fBasicFor init e incr s inh@(acc, br, loop, catch) = let loop' = fWhile (fromMaybeGuard e) (\inh' -> s (wlp' inh' (incrToStmt incr), br, loop', catch)) inh in wlp' (loop', br, loop, catch) (initToStmt init)
+ fEnhancedFor = error "TODO: EnhancedFor"
+ fEmpty (acc, _, _, _) = acc -- Empty does nothing, but still passes control to the next statement
+ fExpStmt = error "TODO: ExpStmt"
+ fAssert e _ inh@(acc, _, _, _) = (e &*) . acc
+ fSwitch e bs inh@(acc, _, _, _) = let (e', s1, s2) = desugarSwitch e bs in fIfThenElse e' (flip wlp' s1) (flip wlp' s2) inh . acc
+ fDo s e (acc, br, _, catch) = let loop = s (fWhile e s (acc, br, loop, catch), br, loop, catch) in loop -- Do is just a while with the statement block executed one additional time. Break and continue still have to be handled in this additional execution.
+ fBreak _ (_, br, _, _) = br -- wlp of the breakpoint
+ fContinue _ (_, _, loop, _) = loop -- wlp of the loop
+ fReturn = error "TODO: Return"
+ fSynchronized _ = fStmtBlock
+ fThrow e inh@(acc, br, loop, catch) = case catch of
+ Nothing -> (\q -> q &* throwException e) -- acc is ignored, as the rest of the block is not executed
+ Just (cs, f) -> maybe (if f then id else (\q -> q &* throwException e)) (flip fStmtBlock (id, br, loop, Nothing)) (getCatch e cs)
+ fTry b cs f inh@(acc, br, loop, catch) = fStmtBlock b (id, br, loop, Just (cs, isJust f)) . maybe acc (flip fStmtBlock inh) f -- The finally-block is always executed
+ fLabeled _ s = s
-- Helper functions
- wlpBlock :: Inh -> BlockStmt -> Exp -> Exp
+ wlpBlock :: Inh -> BlockStmt -> Syn
wlpBlock inh b = case b of
BlockStmt s -> wlp' inh s
LocalClass _ -> id
@@ -121,13 +140,20 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
SwitchCase e' -> (BinOp e Equal e', StmtBlock (Block bs), sbscode)
Default -> (true, StmtBlock (Block bs), sbscode)
where sbscode = let (e, s1, s2) = desugarSwitch e sbs in IfThenElse e s1 s2
-
-true :: Exp
-true = Lit (Boolean True)
+
+ throwException :: Exp -> Exp
+ throwException e = if diffExc then MethodInv (MethodCall (Name [Ident "Exception"]) [e]) else false
+
+ getCatch :: Exp -> [Catch] -> Maybe Block
+ getCatch e [] = Nothing
+ getCatch e (Catch p b:cs) = if p `catches` e then Just b else getCatch e cs
+
+ catches :: FormalParam -> Exp -> Bool
+ catches (FormalParam _ t _ _) e = True -- TODO
-- | Calculates the weakest liberal pre-condition of a statement and a given post-condition
wlp :: Stmt -> Exp -> Exp
-wlp = wlp' (id, id)
+wlp = wlp' (id, id, id, Nothing)
-- wlp' lets you specify the inherited attributes
wlp' :: Inh -> Stmt -> Exp -> Exp
--
GitLab