{-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeSynonymInstances #-}

{- |

Module : $Header$

Description : Generation of Verification Conditions

Copyright : (c) Ewaryst Schulz, DFKI Bremen 2011

License : GPLv2 or higher, see LICENSE.txt

Maintainer : ewaryst.schulz@dfki.de

Stability : experimental

Portability : non-portable (via imports)

This module provides functionality for the generation of verification conditions

during program evaluation. The output is in Isabelle Syntax.

-}

module CSL.Verification where

-- import qualified Data.Map as Map

import qualified Data.Set as Set

import CSL.Interpreter

import CSL.Transformation

import CSL.DependencyGraph

import CSL.AS_BASIC_CSL

import CSL.ASUtils

import CSL.Print_AS

import Common.Doc

import Common.DocUtils

import System.IO

import Control.Monad.Reader

import Control.Monad.Error (MonadError (..))

{- import Control.Monad.Trans (MonadIO (..))

import Control.Monad (when) -}

{- ----------------------------------------------------------------------

Verification Conditions

---------------------------------------------------------------------- -}

{- Given an instantiated constant this data structure keeps

* the value of this constant looked up in the assignment store

* for function constants its definition (looked up in the assignment store)

* the for this constant generated verification condition

data VCData = VCData

{ vcValue :: EXPRESSION

, vcDef :: Maybe AssDefinition

, vcCondition :: EXPRESSION

}

type VCMap = Map.Map InstantiatedConstant VCData

-}

-- | Extra functionality of 'AssignmentStore's for VC generation

class AssignmentStore m => VCGenerator m where

addVC :: EvalAtom -> EXPRESSION -> m ()

getVCPremises :: (Ord a) => AssignmentDepGraph a -- ^ 'DepGraph' for lookup

-> EXPRESSION -- ^ generate premise for this term

-> [EXPRESSION]

getVCPremises adg e =

let scl = Set.map SimpleConstant $ setOfUserDefined e

f (sc, depGrAnno) = mkVCPrem sc $ annoDef depGrAnno

in map f $ Set.toList $ upperUntilRefl (const $ const False) adg scl

mkCondition :: AssDefinition -> EXPRESSION -> EXPRESSION -> EXPRESSION

mkCondition def lhs rhs = f args where

args = getArguments def

f (x : l) = g x $ f l

f _ = toExp $ if isInterval rhs then ("in", lhs, rhs)

else ("=", lhs, rhs)

g v b = toExp ("all", mkVar v, b)

mkVCPrem :: ConstantName -> AssDefinition -> EXPRESSION

mkVCPrem n def = mkCondition def (toExp ( "::"

, toExp (n, map mkVar $ getArguments def)

, OP_real)) $ getDefiniens def

mkVC :: ConstantName

-> AssDefinition

-> EXPRESSION -- ^ the evaluated term for the constant

-> [EXPRESSION] -- ^ a list of premises from assignment graph

-> EXPRESSION

mkVC _ def evalE prl =

let prem = foldl f (head prl) $ tail prl

f a b = toExp ("and", a, b)

conc = mkCondition def (getDefiniens def) evalE

in if null prl then conc else toExp ("impl", prem, conc)

mkBoolVC :: EXPRESSION -- ^ the Boolean term

-> Bool -- ^ the evaluated Boolean term

-> [EXPRESSION] -- ^ a list of premises from assignment graph

-> EXPRESSION

mkBoolVC e evalB prl =

let prem = foldl f (head prl) $ tail prl

f a b = toExp ("and", a, b)

conc = if evalB then e else toExp ("not", e)

in if null prl then conc else toExp ("impl", prem, conc)

verifyingStepper ::

(StepDebugger m, VCGenerator m, MonadIO m, MonadError ASError m) =>

m () -> EvalAtom -> m Bool

verifyingStepper prog x = do

{- liftIO $ putStrLn $ "At step " ++ show (prettyEvalAtom x)

liftIO $ putStrLn "" -}

b <- evaluateAndVerify prog x

dm <- getDebugMode

when dm $ do

let breakPred s = s == "q" || s == "c" || null s

s <- readEvalPrintLoop stdin stdout "next>" breakPred

when (s == "q") $ throwError $ ASError UserError "Quit Debugger"

when (s == "c") $ setDebugMode False

return b

evaluateAndVerify :: (VCGenerator m) => m () -> EvalAtom -> m Bool

evaluateAndVerify _ ea@(AssAtom n def) = do

adg <- getDepGraph

let prl = getVCPremises adg $ getDefiniens def

e <- assign n def

addVC ea $ mkVC n def e prl

-- update the depgraph in the assignment store

updateConstant n $ updateDefinition e def

return True

evaluateAndVerify _ ea@(CaseAtom e) = do

adg <- getDepGraph

let prl = getVCPremises adg e

b <- check e

addVC ea $ mkBoolVC e b prl

return b

evaluateAndVerify prog ea@(RepeatAtom _ _ e') = do

prog

adg <- getDepGraph

let prl = getVCPremises adg e'

b <- check e'

addVC ea $ mkBoolVC e' b prl

return b

{- ----------------------------------------------------------------------

Printing Verification Conditions

---------------------------------------------------------------------- -}

showOpnameForVC :: OPNAME -> String

showOpnameForVC x =

case x of

OP_ex -> "enclEX"

OP_all -> "enclAll"

OP_max -> "maxx"

OP_min -> "minn"

OP_or -> "|"

OP_impl -> "-->"

OP_and -> "&"

_ -> showOPNAME x

data VCPrinter = VCPrinter

-- | The VCPrinter can be interpreted as an 'ExpressionPrinter'

instance ExpressionPrinter (Reader VCPrinter) where

getOINM = return operatorInfoNameMap

printOpname = return . text . showOpnameForVC

printInterval l r = return $

text "Interval"

<> parens (sepByCommas $ map (text . show) [l, r])

printRational r = return $ text $ show nn ++ "/" ++ show dn

where (nn, dn) = toFraction r

printExpForVC :: EXPRESSION -> Doc

printExpForVC e = doubleQuotes $ runReader (printExpression e) VCPrinter

printVCForIsabelle :: EvalAtom -> String -> EXPRESSION -> Doc

printVCForIsabelle ea s e =

let cm = text "Verification condition for" <+> pretty ea <> text ":"

in sep [ parens $ hcat [text "*", cm, text "*"], text "lemma"

, doubleQuotes $ text s, text ":", printExpForVC e ]