|
sourcecode:
|
module VerifierState where
import Data.IORef
import Data.List ( find )
import Contract.Names ( isPreCondName, isPostCondName )
import FlatCurry.Annotated.Goodies ( funcName, typeName, progName, progTypes )
import FlatCurry.Typed.Types
import ToolOptions
---------------------------------------------------------------------------
-- Some global information used by the transformation process:
data VerifyInfo = VerifyInfo
{ toolOpts :: Options -- options passed to the tool
, allFuns :: [TAFuncDecl] -- all defined operations
, preConds :: [TAFuncDecl] -- all precondition operations
, postConds :: [TAFuncDecl] -- all postcondition operations
}
makeVerifyInfo :: Options -> [AFuncDecl TypeExpr] -> VerifyInfo
makeVerifyInfo opts fdecls = VerifyInfo opts fdecls preconds postconds
where
-- Precondition operations:
preconds = filter (isPreCondName . snd . funcName) fdecls
-- Postcondition operations:
postconds = filter (isPostCondName . snd . funcName) fdecls
---------------------------------------------------------------------------
-- The global state of the verification process keeps some
-- statistical information and the programs that are already read
-- (to avoid multiple readings).
data VState = VState
{ trInfo :: VerifyInfo -- information used by the transformation process
, uPreCond :: [String] -- unverified preconditions
, vPreCond :: [String] -- verified preconditions
, uPostCond :: [String] -- unverified postconditions
, vPostCond :: [String] -- verified postconditions
, currTAProgs :: [TAProg] -- already read typed FlatCurry programs
}
initVState :: VerifyInfo -> VState
initVState ti = VState ti [] [] [] [] []
--- Reads VerifyInfo from VState IORef.
readVerifyInfoRef :: IORef VState -> IO VerifyInfo
readVerifyInfoRef vstref = readIORef vstref >>= return . trInfo
--- Shows the statistics in human-readable format.
showStats :: VState -> String
showStats vst =
showStat "PRECONDITIONS : VERIFIED " (vPreCond vst) ++
showStat "PRECONDITIONS : UNVERIFIED" (uPreCond vst) ++
showStat "POSTCONDITIONS: VERIFIED " (vPostCond vst) ++
showStat "POSTCONDITIONS: UNVERIFIED" (uPostCond vst) ++
(if null (uPreCond vst ++ uPostCond vst)
then "\nALL CONTRACTS VERIFIED!"
else "")
where
showStat t fs = if null fs then "" else "\n" ++ t ++ ": " ++ unwords fs
--- Is the program transformed so that some contracts are added?
areContractsAdded :: VState -> Bool
areContractsAdded vst =
not (null (preConds (trInfo vst)) && null (uPostCond vst))
--- Increments the number of preconditions. If the first argument is true,
--- a precondition has been verified.
addPreCondToStats :: String -> Bool -> VState -> VState
addPreCondToStats pc verified vst =
if verified then vst { vPreCond = pc : vPreCond vst }
else vst { uPreCond = pc : uPreCond vst }
--- Adds an operation to the already processed operations with postconditions.
--- If the second argument is true, the postcondition of this operation
--- has been verified.
addPostCondToStats :: String -> Bool -> VState -> VState
addPostCondToStats pc verified vst =
if verified then vst { vPostCond = pc : vPostCond vst }
else vst { uPostCond = pc : uPostCond vst }
--- Adds a new typed FlatCurry program to the state.
addProgToState :: AProg TypeExpr -> VState -> VState
addProgToState prog vstate = vstate { currTAProgs = prog : currTAProgs vstate }
---------------------------------------------------------------------------
--- Selects the type declaration of a type constructor from the state.
tdeclOf :: VState -> QName -> Maybe TypeDecl
tdeclOf vst tcons@(mn,_) =
maybe Nothing
(\p -> find (\td -> typeName td == tcons) (progTypes p))
(find (\p -> progName p == mn) (currTAProgs vst))
---------------------------------------------------------------------------
|