-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Tools.WeakestPreconditions
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- A toy imperative language with a proof system based on Dijkstra's weakest
-- preconditions methodology to establish partial/total correctness proofs.
--
-- See @Documentation.SBV.Examples.WeakestPreconditions@ directory for
-- several example proofs.
-----------------------------------------------------------------------------

{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE NamedFieldPuns         #-}
{-# LANGUAGE ScopedTypeVariables    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Tools.WeakestPreconditions (
        -- * Programs and statements
          Program(..), Stmt(..), assert, stable

        -- * Invariants, measures, and stability
        , Invariant, Measure, Stable

        -- * Verification conditions
        , VC(..)

        -- * Result of a proof
        , ProofResult(..)

        -- * Configuring the WP engine
        , WPConfig(..), defaultWPCfg

        -- * Checking WP correctness
        , wpProve, wpProveWith

        -- * Concrete runs of programs
        , traceExecution, Status(..)
        ) where

import Data.List   (intercalate)
import Data.Maybe  (fromJust, isJust, isNothing)

import Control.Monad (when)

import Data.SBV
import Data.SBV.Control

-- | A program over a state is simply a statement, together with
-- a pre-condition capturing environmental assumptions and
-- a post-condition that states its correctness. In the usual
-- Hoare-triple notation, it captures:
--
--   @ {precondition} program {postcondition} @
--
-- We also allow for a stability check, which is ensured at
-- every assignment statement to deal with ghost variables.
-- In general, this is useful for making sure what you consider
-- as "primary inputs" remain unaffected. Of course, you can
-- also put any arbitrary condition you want to check that you
-- want performed for each 'Assign' statement.
--
-- Note that stability is quite a strong condition: It is intended
-- to capture constants that never change during execution. So,
-- if you have a program that changes an input temporarily but
-- always restores it at the end, it would still fail the stability
-- condition.
--
-- The 'setup' field is reserved for any symbolic code you might
-- want to run before the proof takes place, typically for calls
-- to 'Data.SBV.setOption'. If not needed, simply pass @return ()@.
-- For an interesting use case where we use setup to axiomatize
-- the spec, see "Documentation.SBV.Examples.WeakestPreconditions.Fib"
-- and "Documentation.SBV.Examples.WeakestPreconditions.GCD".
data Program st = Program { Program st -> Symbolic ()
setup         :: Symbolic ()  -- ^ Any set-up required
                          , Program st -> st -> SBool
precondition  :: st -> SBool  -- ^ Environmental assumptions
                          , Program st -> Stmt st
program       :: Stmt st      -- ^ Program
                          , Program st -> st -> SBool
postcondition :: st -> SBool  -- ^ Correctness statement
                          , Program st -> Stable st
stability     :: Stable st    -- ^ Each assignment must satisfy stability
                          }

-- | A stability condition captures a primary input that does not change. Use 'stable'
-- to create elements of this type.
type Stable st = [st -> st -> (String, SBool)]

-- | An invariant takes a state and evaluates to a boolean.
type Invariant st = st -> SBool

-- | A measure takes the state and returns a sequence of integers. The ordering
-- will be done lexicographically over the elements.
type Measure st = st -> [SInteger]

-- | A statement in our imperative program, parameterized over the state.
data Stmt st = Skip                                                                     -- ^ Skip, do nothing.
             | Abort String                                                             -- ^ Abort execution. The name is for diagnostic purposes.
             | Assign (st -> st)                                                        -- ^ Assignment: Transform the state by a function.
             | If (st -> SBool) (Stmt st) (Stmt st)                                     -- ^ Conditional: @If condition thenBranch elseBranch@.
             | While String (Invariant st) (Maybe (Measure st)) (st -> SBool) (Stmt st) -- ^ A while loop: @While name invariant measure condition body@.
                                                                                        -- The string @name@ is merely for diagnostic purposes.
                                                                                        -- If the measure is 'Nothing', then only partial correctness
                                                                                        -- of this loop will be proven.
             | Seq [Stmt st]                                                            -- ^ A sequence of statements.

-- | An 'assert' is a quick way of ensuring some condition holds. If it does,
-- then it's equivalent to 'Skip'. Otherwise, it is equivalent to 'Abort'.
assert :: String -> (st -> SBool) -> Stmt st
assert :: String -> (st -> SBool) -> Stmt st
assert String
nm st -> SBool
cond = (st -> SBool) -> Stmt st -> Stmt st -> Stmt st
forall st. (st -> SBool) -> Stmt st -> Stmt st -> Stmt st
If st -> SBool
cond Stmt st
forall st. Stmt st
Skip (String -> Stmt st
forall st. String -> Stmt st
Abort String
nm)

-- | Stability: A call of the form @stable "f" f@ means the value of the field @f@
-- does not change during any assignment. The string argument is for diagnostic
-- purposes only. Note that we use strong-equality here, so if the program
-- is manipulating floats, we don't get a false-positive on @NaN@ and also
-- not miss @+0@ and @-@@ changes.
stable :: EqSymbolic a => String -> (st -> a) -> st -> st -> (String, SBool)
stable :: String -> (st -> a) -> st -> st -> (String, SBool)
stable String
nm st -> a
f st
before st
after = (String
nm, st -> a
f st
before a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.=== st -> a
f st
after)

-- | Are all the termination measures provided?
isTotal :: Stmt st -> Bool
isTotal :: Stmt st -> Bool
isTotal Stmt st
Skip                = Bool
True
isTotal (Abort String
_)           = Bool
True
isTotal (Assign st -> st
_)          = Bool
True
isTotal (If st -> SBool
_ Stmt st
tb Stmt st
fb)        = (Stmt st -> Bool) -> [Stmt st] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Stmt st -> Bool
forall st. Stmt st -> Bool
isTotal [Stmt st
tb, Stmt st
fb]
isTotal (While String
_ st -> SBool
_ Maybe (Measure st)
msr st -> SBool
_ Stmt st
s) = Maybe (Measure st) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (Measure st)
msr Bool -> Bool -> Bool
&& Stmt st -> Bool
forall st. Stmt st -> Bool
isTotal Stmt st
s
isTotal (Seq [Stmt st]
ss)            = (Stmt st -> Bool) -> [Stmt st] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Stmt st -> Bool
forall st. Stmt st -> Bool
isTotal [Stmt st]
ss

-- | A verification condition. Upon failure, each 'VC' carries enough state and diagnostic information
-- to indicate what particular proof obligation failed for further debugging.
data VC st m = BadPrecondition          st                  -- ^ The precondition doesn't hold. This can only happen in 'traceExecution'.
             | BadPostcondition         st st               -- ^ The postcondition doesn't hold
             | Unstable          String st st               -- ^ Stability condition is violated
             | AbortReachable    String st st               -- ^ The named abort condition is reachable
             | InvariantPre      String st                  -- ^ Invariant doesn't hold upon entry to the named loop
             | InvariantMaintain String st st               -- ^ Invariant isn't maintained by the body
             | MeasureBound      String (st, [m])           -- ^ Measure cannot be shown to be non-negative
             | MeasureDecrease   String (st, [m]) (st, [m]) -- ^ Measure cannot be shown to decrease through each iteration

-- | Helper function to display VC's nicely
dispVC :: String -> [(String, String)] -> String
dispVC :: String -> [(String, String)] -> String
dispVC String
tag [(String, String)]
flds = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> String
col String
tag String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> String
showField [(String, String)]
flds
  where col :: String -> String
col String
"" = String
""
        col String
t  = String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":"

        showField :: (String, String) -> String
showField (String
t, String
c) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Int -> String -> String) -> [Int] -> [String] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> String -> String
forall a. (Eq a, Num a) => a -> String -> String
mark [(Int
1::Int)..] (String -> [String]
lines String
c)
           where tt :: String
tt   = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
t then String
"" else String -> String
col String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
                 sp :: String
sp   = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
tt) Char
' '
                 mark :: a -> String -> String
mark a
i String
s = String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
1 then String
tt else String
sp) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s

-- If a measure is a singleton, just show the number. Otherwise as a list:
showMeasure :: Show a => [a] -> String
showMeasure :: [a] -> String
showMeasure [a
x] = a -> String
forall a. Show a => a -> String
show a
x
showMeasure [a]
xs  = [a] -> String
forall a. Show a => a -> String
show [a]
xs

-- | Show instance for VC's
instance (Show st, Show m) => Show (VC st m) where
  show :: VC st m -> String
show (BadPrecondition   st
s)                    = String -> [(String, String)] -> String
dispVC String
"Precondition fails"
                                                         [(String
"", st -> String
forall a. Show a => a -> String
show st
s)]
  show (BadPostcondition  st
s1 st
s2)                = String -> [(String, String)] -> String
dispVC String
"Postcondition fails"
                                                         [ (String
"Start", st -> String
forall a. Show a => a -> String
show st
s1)
                                                         , (String
"End  ", st -> String
forall a. Show a => a -> String
show st
s2)
                                                         ]
  show (Unstable          String
m st
s1 st
s2)              = String -> [(String, String)] -> String
dispVC (String
"Stability fails for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
m)
                                                         [ (String
"Before", st -> String
forall a. Show a => a -> String
show st
s1)
                                                         , (String
"After ", st -> String
forall a. Show a => a -> String
show st
s2)
                                                         ]
  show (AbortReachable    String
nm st
s1 st
s2)             = String -> [(String, String)] -> String
dispVC (String
"Abort " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" condition is satisfiable")
                                                         [ (String
"Before", st -> String
forall a. Show a => a -> String
show st
s1)
                                                         , (String
"After ", st -> String
forall a. Show a => a -> String
show st
s2)
                                                         ]
  show (InvariantPre      String
nm st
s)                 = String -> [(String, String)] -> String
dispVC (String
"Invariant for loop " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" fails upon entry")
                                                         [(String
"", st -> String
forall a. Show a => a -> String
show st
s)]
  show (InvariantMaintain String
nm st
s1 st
s2)             = String -> [(String, String)] -> String
dispVC (String
"Invariant for loop " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not maintained by the body")
                                                         [ (String
"Before", st -> String
forall a. Show a => a -> String
show st
s1)
                                                         , (String
"After ", st -> String
forall a. Show a => a -> String
show st
s2)
                                                         ]
  show (MeasureBound      String
nm (st
s, [m]
m))            = String -> [(String, String)] -> String
dispVC (String
"Measure for loop "   String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is negative")
                                                         [ (String
"State  ", st -> String
forall a. Show a => a -> String
show st
s)
                                                         , (String
"Measure", [m] -> String
forall a. Show a => [a] -> String
showMeasure [m]
m )
                                                         ]
  show (MeasureDecrease   String
nm (st
s1, [m]
m1) (st
s2, [m]
m2)) = String -> [(String, String)] -> String
dispVC (String
"Measure for loop "   String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" does not decrease")
                                                         [ (String
"Before ", st -> String
forall a. Show a => a -> String
show st
s1)
                                                         , (String
"Measure", [m] -> String
forall a. Show a => [a] -> String
showMeasure [m]
m1)
                                                         , (String
"After  ", st -> String
forall a. Show a => a -> String
show st
s2)
                                                         , (String
"Measure", [m] -> String
forall a. Show a => [a] -> String
showMeasure [m]
m2)
                                                         ]

-- | The result of a weakest-precondition proof.
data ProofResult res = Proven Bool                -- ^ The property holds. If 'Bool' is 'True', then total correctness, otherwise partial.
                     | Indeterminate String       -- ^ Failed to establish correctness. Happens when the proof obligations lead to
                                                  -- the SMT solver to return @Unk@. This can happen, for instance, if you have
                                                  -- non-linear constraints, causing the solver to give up.
                     | Failed [VC res Integer]    -- ^ The property fails, failing to establish the conditions listed.

-- | 'Show' instance for proofs, for readability.
instance Show res => Show (ProofResult res) where
  show :: ProofResult res -> String
show (Proven Bool
True)     = String
"Q.E.D."
  show (Proven Bool
False)    = String
"Q.E.D. [Partial: not all termination measures were provided.]"
  show (Indeterminate String
s) = String
"Indeterminate: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
  show (Failed [VC res Integer]
vcs)      = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String
"Proof failure. Failing verification condition" String -> String -> String
forall a. [a] -> [a] -> [a]
++ if [VC res Integer] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VC res Integer]
vcs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 then String
"s:" else String
":")
                                              String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (VC res Integer -> String) -> [VC res Integer] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\VC res Integer
vc -> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l | String
l <- String -> [String]
lines (VC res Integer -> String
forall a. Show a => a -> String
show VC res Integer
vc)]) [VC res Integer]
vcs



-- | Checking WP based correctness
wpProveWith :: forall st res. (Show res, Mergeable st, Queriable IO st res) => WPConfig -> Program st -> IO (ProofResult res)
wpProveWith :: WPConfig -> Program st -> IO (ProofResult res)
wpProveWith cfg :: WPConfig
cfg@WPConfig{Bool
wpVerbose :: WPConfig -> Bool
wpVerbose :: Bool
wpVerbose} Program{Symbolic ()
setup :: Symbolic ()
setup :: forall st. Program st -> Symbolic ()
setup, st -> SBool
precondition :: st -> SBool
precondition :: forall st. Program st -> st -> SBool
precondition, Stmt st
program :: Stmt st
program :: forall st. Program st -> Stmt st
program, st -> SBool
postcondition :: st -> SBool
postcondition :: forall st. Program st -> st -> SBool
postcondition, Stable st
stability :: Stable st
stability :: forall st. Program st -> Stable st
stability} =
   SMTConfig -> Symbolic (ProofResult res) -> IO (ProofResult res)
forall a. SMTConfig -> Symbolic a -> IO a
runSMTWith (WPConfig -> SMTConfig
wpSolver WPConfig
cfg) (Symbolic (ProofResult res) -> IO (ProofResult res))
-> Symbolic (ProofResult res) -> IO (ProofResult res)
forall a b. (a -> b) -> a -> b
$ do Symbolic ()
setup
                                  Query (ProofResult res) -> Symbolic (ProofResult res)
forall a. Query a -> Symbolic a
query Query (ProofResult res)
q
  where q :: Query (ProofResult res)
q = do st
start <- QueryT IO st
forall (m :: * -> *) a b. Queriable m a b => QueryT m a
create

               st -> [(SBool, VC st SInteger)]
weakestPrecondition <- st
-> Stmt st
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
wp st
start Stmt st
program (\st
st -> [(st -> SBool
postcondition st
st, st -> st -> VC st SInteger
forall st m. st -> st -> VC st m
BadPostcondition st
start st
st)])

               let vcs :: [(SBool, VC st SInteger)]
vcs = st -> [(SBool, VC st SInteger)]
weakestPrecondition st
start

               SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ st -> SBool
precondition st
start SBool -> SBool -> SBool
.=> [SBool] -> SBool
sAnd (((SBool, VC st SInteger) -> SBool)
-> [(SBool, VC st SInteger)] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map (SBool, VC st SInteger) -> SBool
forall a b. (a, b) -> a
fst [(SBool, VC st SInteger)]
vcs)

               CheckSatResult
cs <- Query CheckSatResult
checkSat
               case CheckSatResult
cs of
                 CheckSatResult
Unk    -> String -> ProofResult res
forall res. String -> ProofResult res
Indeterminate (String -> ProofResult res)
-> (SMTReasonUnknown -> String)
-> SMTReasonUnknown
-> ProofResult res
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTReasonUnknown -> String
forall a. Show a => a -> String
show (SMTReasonUnknown -> ProofResult res)
-> QueryT IO SMTReasonUnknown -> Query (ProofResult res)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT IO SMTReasonUnknown
getUnknownReason

                 CheckSatResult
Unsat  -> do let t :: Bool
t = Stmt st -> Bool
forall st. Stmt st -> Bool
isTotal Stmt st
program

                              if Bool
t then String -> QueryT IO ()
msg String
"Total correctness is established."
                                   else String -> QueryT IO ()
msg String
"Partial correctness is established."

                              ProofResult res -> Query (ProofResult res)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ProofResult res -> Query (ProofResult res))
-> ProofResult res -> Query (ProofResult res)
forall a b. (a -> b) -> a -> b
$ Bool -> ProofResult res
forall res. Bool -> ProofResult res
Proven Bool
t

                 DSat{} -> ProofResult res -> Query (ProofResult res)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ProofResult res -> Query (ProofResult res))
-> ProofResult res -> Query (ProofResult res)
forall a b. (a -> b) -> a -> b
$ String -> ProofResult res
forall res. String -> ProofResult res
Indeterminate String
"Unsupported: Solver returned a delta-satisfiable answer."

                 CheckSatResult
Sat    -> do let checkVC :: (SBool, VC st SInteger) -> Query [VC res Integer]
                                  checkVC :: (SBool, VC st SInteger) -> Query [VC res Integer]
checkVC (SBool
cond, VC st SInteger
vc) = do Bool
c <- SBool -> Query Bool
forall a. SymVal a => SBV a -> Query a
getValue SBool
cond
                                                          if Bool
c
                                                             then [VC res Integer] -> Query [VC res Integer]
forall (m :: * -> *) a. Monad m => a -> m a
return []   -- The VC was OK
                                                             else do VC res Integer
vc' <- case VC st SInteger
vc of
                                                                              BadPrecondition     st
s                 -> res -> VC res Integer
forall st m. st -> VC st m
BadPrecondition     (res -> VC res Integer)
-> QueryT IO res -> QueryT IO (VC res Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> st -> QueryT IO res
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project st
s
                                                                              BadPostcondition    st
s1 st
s2             -> res -> res -> VC res Integer
forall st m. st -> st -> VC st m
BadPostcondition    (res -> res -> VC res Integer)
-> QueryT IO res -> QueryT IO (res -> VC res Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> st -> QueryT IO res
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project st
s1 QueryT IO (res -> VC res Integer)
-> QueryT IO res -> QueryT IO (VC res Integer)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> st -> QueryT IO res
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project st
s2
                                                                              Unstable          String
l st
s1 st
s2             -> String -> res -> res -> VC res Integer
forall st m. String -> st -> st -> VC st m
Unstable          String
l (res -> res -> VC res Integer)
-> QueryT IO res -> QueryT IO (res -> VC res Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> st -> QueryT IO res
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project st
s1 QueryT IO (res -> VC res Integer)
-> QueryT IO res -> QueryT IO (VC res Integer)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> st -> QueryT IO res
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project st
s2
                                                                              AbortReachable    String
l st
s1 st
s2             -> String -> res -> res -> VC res Integer
forall st m. String -> st -> st -> VC st m
AbortReachable    String
l (res -> res -> VC res Integer)
-> QueryT IO res -> QueryT IO (res -> VC res Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> st -> QueryT IO res
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project st
s1 QueryT IO (res -> VC res Integer)
-> QueryT IO res -> QueryT IO (VC res Integer)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> st -> QueryT IO res
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project st
s2
                                                                              InvariantPre      String
l st
s                 -> String -> res -> VC res Integer
forall st m. String -> st -> VC st m
InvariantPre      String
l (res -> VC res Integer)
-> QueryT IO res -> QueryT IO (VC res Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> st -> QueryT IO res
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project st
s
                                                                              InvariantMaintain String
l st
s1 st
s2             -> String -> res -> res -> VC res Integer
forall st m. String -> st -> st -> VC st m
InvariantMaintain String
l (res -> res -> VC res Integer)
-> QueryT IO res -> QueryT IO (res -> VC res Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> st -> QueryT IO res
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project st
s1 QueryT IO (res -> VC res Integer)
-> QueryT IO res -> QueryT IO (VC res Integer)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> st -> QueryT IO res
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project st
s2
                                                                              MeasureBound      String
l (st
s, [SInteger]
m)            -> do res
r <- st -> QueryT IO res
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project st
s
                                                                                                                          [Integer]
v <- (SInteger -> QueryT IO Integer)
-> [SInteger] -> QueryT IO [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SInteger -> QueryT IO Integer
forall a. SymVal a => SBV a -> Query a
getValue [SInteger]
m
                                                                                                                          VC res Integer -> QueryT IO (VC res Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (VC res Integer -> QueryT IO (VC res Integer))
-> VC res Integer -> QueryT IO (VC res Integer)
forall a b. (a -> b) -> a -> b
$ String -> (res, [Integer]) -> VC res Integer
forall st m. String -> (st, [m]) -> VC st m
MeasureBound String
l (res
r, [Integer]
v)
                                                                              MeasureDecrease   String
l (st
s1, [SInteger]
i1) (st
s2, [SInteger]
i2) -> do res
r1 <- st -> QueryT IO res
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project st
s1
                                                                                                                          [Integer]
v1 <- (SInteger -> QueryT IO Integer)
-> [SInteger] -> QueryT IO [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SInteger -> QueryT IO Integer
forall a. SymVal a => SBV a -> Query a
getValue [SInteger]
i1
                                                                                                                          res
r2 <- st -> QueryT IO res
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project st
s2
                                                                                                                          [Integer]
v2 <- (SInteger -> QueryT IO Integer)
-> [SInteger] -> QueryT IO [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SInteger -> QueryT IO Integer
forall a. SymVal a => SBV a -> Query a
getValue [SInteger]
i2
                                                                                                                          VC res Integer -> QueryT IO (VC res Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (VC res Integer -> QueryT IO (VC res Integer))
-> VC res Integer -> QueryT IO (VC res Integer)
forall a b. (a -> b) -> a -> b
$ String -> (res, [Integer]) -> (res, [Integer]) -> VC res Integer
forall st m. String -> (st, [m]) -> (st, [m]) -> VC st m
MeasureDecrease String
l (res
r1, [Integer]
v1) (res
r2, [Integer]
v2)
                                                                     [VC res Integer] -> Query [VC res Integer]
forall (m :: * -> *) a. Monad m => a -> m a
return [VC res Integer
vc']

                              [VC res Integer]
badVCs <- [[VC res Integer]] -> [VC res Integer]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[VC res Integer]] -> [VC res Integer])
-> QueryT IO [[VC res Integer]] -> Query [VC res Integer]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((SBool, VC st SInteger) -> Query [VC res Integer])
-> [(SBool, VC st SInteger)] -> QueryT IO [[VC res Integer]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SBool, VC st SInteger) -> Query [VC res Integer]
checkVC [(SBool, VC st SInteger)]
vcs

                              Bool -> QueryT IO () -> QueryT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([VC res Integer] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VC res Integer]
badVCs) (QueryT IO () -> QueryT IO ()) -> QueryT IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ String -> QueryT IO ()
forall a. HasCallStack => String -> a
error String
"Data.SBV.proveWP: Impossible happened. Proof failed, but no failing VC found!"

                              let plu :: String -> [a] -> String
plu String
w (a
_:a
_:[a]
_) = String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"s"
                                  plu String
w [a]
_       = String
w

                                  m :: String
m = String
"Following proof " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [VC res Integer] -> String
forall a. String -> [a] -> String
plu String
"obligation" [VC res Integer]
badVCs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" failed:"

                              String -> QueryT IO ()
msg String
m
                              String -> QueryT IO ()
msg (String -> QueryT IO ()) -> String -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
m) Char
'='

                              let disp :: a -> QueryT IO ()
disp a
c = (String -> QueryT IO ()) -> [String] -> QueryT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> QueryT IO ()
msg [String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l | String
l <- String -> [String]
lines (a -> String
forall a. Show a => a -> String
show a
c)]
                              (VC res Integer -> QueryT IO ())
-> [VC res Integer] -> QueryT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VC res Integer -> QueryT IO ()
forall a. Show a => a -> QueryT IO ()
disp [VC res Integer]
badVCs

                              ProofResult res -> Query (ProofResult res)
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofResult res -> Query (ProofResult res))
-> ProofResult res -> Query (ProofResult res)
forall a b. (a -> b) -> a -> b
$ [VC res Integer] -> ProofResult res
forall res. [VC res Integer] -> ProofResult res
Failed [VC res Integer]
badVCs

        msg :: String -> QueryT IO ()
msg = IO () -> QueryT IO ()
forall a. IO a -> Query a
io (IO () -> QueryT IO ())
-> (String -> IO ()) -> String -> QueryT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
wpVerbose (IO () -> IO ()) -> (String -> IO ()) -> String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn

        -- Compute the weakest precondition to establish the property:
        wp :: st -> Stmt st -> (st -> [(SBool, VC st SInteger)]) -> Query (st -> [(SBool, VC st SInteger)])

        -- Skip simply keeps the conditions
        wp :: st
-> Stmt st
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
wp st
_ Stmt st
Skip st -> [(SBool, VC st SInteger)]
post = (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
forall (m :: * -> *) a. Monad m => a -> m a
return st -> [(SBool, VC st SInteger)]
post

        -- Abort is never satisfiable. The only way to have Abort's VC to pass is
        -- to run it in a precondition (either via program or in an if branch) that
        -- evaluates to false, i.e., it must not be reachable.
        wp st
start (Abort String
nm) st -> [(SBool, VC st SInteger)]
_ = (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((st -> [(SBool, VC st SInteger)])
 -> Query (st -> [(SBool, VC st SInteger)]))
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
forall a b. (a -> b) -> a -> b
$ \st
st -> [(SBool
sFalse, String -> st -> st -> VC st SInteger
forall st m. String -> st -> st -> VC st m
AbortReachable String
nm st
start st
st)]

        -- Assign simply transforms the state and passes on. It also checks that the
        -- stability constraints are not violated.
        wp st
_ (Assign st -> st
f) st -> [(SBool, VC st SInteger)]
post = (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((st -> [(SBool, VC st SInteger)])
 -> Query (st -> [(SBool, VC st SInteger)]))
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
forall a b. (a -> b) -> a -> b
$ \st
st -> let st' :: st
st'       = st -> st
f st
st
                                                   vcs :: [(SBool, VC st m)]
vcs       = ((st -> st -> (String, SBool)) -> (SBool, VC st m))
-> Stable st -> [(SBool, VC st m)]
forall a b. (a -> b) -> [a] -> [b]
map (\st -> st -> (String, SBool)
s -> let (String
nm, SBool
b) = st -> st -> (String, SBool)
s st
st st
st' in (SBool
b, String -> st -> st -> VC st m
forall st m. String -> st -> st -> VC st m
Unstable String
nm st
st st
st')) Stable st
stability
                                               in [(SBool, VC st SInteger)]
forall m. [(SBool, VC st m)]
vcs [(SBool, VC st SInteger)]
-> [(SBool, VC st SInteger)] -> [(SBool, VC st SInteger)]
forall a. [a] -> [a] -> [a]
++ st -> [(SBool, VC st SInteger)]
post st
st'

        -- Conditional: We separately collect the VCs, and predicate with the proper branch condition
        wp st
start (If st -> SBool
c Stmt st
tb Stmt st
fb) st -> [(SBool, VC st SInteger)]
post = do st -> [(SBool, VC st SInteger)]
tWP <- st
-> Stmt st
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
wp st
start Stmt st
tb st -> [(SBool, VC st SInteger)]
post
                                        st -> [(SBool, VC st SInteger)]
fWP <- st
-> Stmt st
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
wp st
start Stmt st
fb st -> [(SBool, VC st SInteger)]
post
                                        (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((st -> [(SBool, VC st SInteger)])
 -> Query (st -> [(SBool, VC st SInteger)]))
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
forall a b. (a -> b) -> a -> b
$ \st
st -> let cond :: SBool
cond = st -> SBool
c st
st
                                                        in   [(     SBool
cond SBool -> SBool -> SBool
.=> SBool
b, VC st SInteger
v) | (SBool
b, VC st SInteger
v) <- st -> [(SBool, VC st SInteger)]
tWP st
st]
                                                          [(SBool, VC st SInteger)]
-> [(SBool, VC st SInteger)] -> [(SBool, VC st SInteger)]
forall a. [a] -> [a] -> [a]
++ [(SBool -> SBool
sNot SBool
cond SBool -> SBool -> SBool
.=> SBool
b, VC st SInteger
v) | (SBool
b, VC st SInteger
v) <- st -> [(SBool, VC st SInteger)]
fWP st
st]

        -- Sequencing: Simply run through the statements
        wp st
_     (Seq [])              st -> [(SBool, VC st SInteger)]
post = (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
forall (m :: * -> *) a. Monad m => a -> m a
return st -> [(SBool, VC st SInteger)]
post
        wp st
start (Seq (Stmt st
s:[Stmt st]
ss))          st -> [(SBool, VC st SInteger)]
post = st
-> Stmt st
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
wp st
start Stmt st
s ((st -> [(SBool, VC st SInteger)])
 -> Query (st -> [(SBool, VC st SInteger)]))
-> Query (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< st
-> Stmt st
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
wp st
start ([Stmt st] -> Stmt st
forall st. [Stmt st] -> Stmt st
Seq [Stmt st]
ss) st -> [(SBool, VC st SInteger)]
post

        -- While loop, where all the WP magic happens!
        wp st
start (While String
nm st -> SBool
inv Maybe (Measure st)
mm st -> SBool
cond Stmt st
body) st -> [(SBool, VC st SInteger)]
post = do
                st
st'  <- QueryT IO st
forall (m :: * -> *) a b. Queriable m a b => QueryT m a
create

                let noMeasure :: Bool
noMeasure = Maybe (Measure st) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (Measure st)
mm
                    m :: Measure st
m         = Maybe (Measure st) -> Measure st
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Measure st)
mm
                    curM :: [SInteger]
curM      = Measure st
m st
st'
                    zero :: [SInteger]
zero      = (SInteger -> SInteger) -> [SInteger] -> [SInteger]
forall a b. (a -> b) -> [a] -> [b]
map (SInteger -> SInteger -> SInteger
forall a b. a -> b -> a
const SInteger
0) [SInteger]
curM

                    iterates :: SBool
iterates   = st -> SBool
inv st
st' SBool -> SBool -> SBool
.&&       st -> SBool
cond st
st'
                    terminates :: SBool
terminates = st -> SBool
inv st
st' SBool -> SBool -> SBool
.&& SBool -> SBool
sNot (st -> SBool
cond st
st')


                -- Condition 1: Invariant must hold prior to loop entry
                st -> [(SBool, VC st SInteger)]
invHoldsPrior <- st
-> Stmt st
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
wp st
start Stmt st
forall st. Stmt st
Skip (\st
st -> [(st -> SBool
inv st
st, String -> st -> VC st SInteger
forall st m. String -> st -> VC st m
InvariantPre String
nm st
st)])

                -- Condition 2: If we iterate, invariant must be maitained by the body
                st -> [(SBool, VC st SInteger)]
invMaintained <- st
-> Stmt st
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
wp st
st' Stmt st
body (\st
st -> [(SBool
iterates SBool -> SBool -> SBool
.=> st -> SBool
inv st
st, String -> st -> st -> VC st SInteger
forall st m. String -> st -> st -> VC st m
InvariantMaintain String
nm st
st' st
st)])

                -- Condition 3: If we terminate, invariant must be strong enough to establish the post condition
                st -> [(SBool, VC st SInteger)]
invEstablish <- st
-> Stmt st
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
wp st
st' Stmt st
body ([(SBool, VC st SInteger)] -> st -> [(SBool, VC st SInteger)]
forall a b. a -> b -> a
const [(SBool
terminates SBool -> SBool -> SBool
.=> SBool
b, VC st SInteger
v) | (SBool
b, VC st SInteger
v) <- st -> [(SBool, VC st SInteger)]
post st
st'])

                -- Condition 4: If we iterate, measure must always be non-negative
                st -> [(SBool, VC st SInteger)]
measureNonNegative <- if Bool
noMeasure
                                      then (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
forall (m :: * -> *) a. Monad m => a -> m a
return  ([(SBool, VC st SInteger)] -> st -> [(SBool, VC st SInteger)]
forall a b. a -> b -> a
const [])
                                      else st
-> Stmt st
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
wp st
st' Stmt st
forall st. Stmt st
Skip ([(SBool, VC st SInteger)] -> st -> [(SBool, VC st SInteger)]
forall a b. a -> b -> a
const [(SBool
iterates SBool -> SBool -> SBool
.=> [SInteger]
curM [SInteger] -> [SInteger] -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= [SInteger]
zero, String -> (st, [SInteger]) -> VC st SInteger
forall st m. String -> (st, [m]) -> VC st m
MeasureBound String
nm (st
st', [SInteger]
curM))])

                -- Condition 5: If we iterate, the measure must decrease
                st -> [(SBool, VC st SInteger)]
measureDecreases <- if Bool
noMeasure
                                    then (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
forall (m :: * -> *) a. Monad m => a -> m a
return  ([(SBool, VC st SInteger)] -> st -> [(SBool, VC st SInteger)]
forall a b. a -> b -> a
const [])
                                    else st
-> Stmt st
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
wp st
st' Stmt st
body (\st
st -> let prevM :: [SInteger]
prevM = Measure st
m st
st in [(SBool
iterates SBool -> SBool -> SBool
.=> [SInteger]
prevM [SInteger] -> [SInteger] -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< [SInteger]
curM, String -> (st, [SInteger]) -> (st, [SInteger]) -> VC st SInteger
forall st m. String -> (st, [m]) -> (st, [m]) -> VC st m
MeasureDecrease String
nm (st
st', [SInteger]
curM) (st
st, [SInteger]
prevM))])

                -- Simply concatenate the VCs from all our conditions:
                (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((st -> [(SBool, VC st SInteger)])
 -> Query (st -> [(SBool, VC st SInteger)]))
-> (st -> [(SBool, VC st SInteger)])
-> Query (st -> [(SBool, VC st SInteger)])
forall a b. (a -> b) -> a -> b
$ \st
st ->    st -> [(SBool, VC st SInteger)]
invHoldsPrior      st
st
                                [(SBool, VC st SInteger)]
-> [(SBool, VC st SInteger)] -> [(SBool, VC st SInteger)]
forall a. [a] -> [a] -> [a]
++ st -> [(SBool, VC st SInteger)]
invMaintained      st
st'
                                [(SBool, VC st SInteger)]
-> [(SBool, VC st SInteger)] -> [(SBool, VC st SInteger)]
forall a. [a] -> [a] -> [a]
++ st -> [(SBool, VC st SInteger)]
invEstablish       st
st'
                                [(SBool, VC st SInteger)]
-> [(SBool, VC st SInteger)] -> [(SBool, VC st SInteger)]
forall a. [a] -> [a] -> [a]
++ st -> [(SBool, VC st SInteger)]
measureNonNegative st
st'
                                [(SBool, VC st SInteger)]
-> [(SBool, VC st SInteger)] -> [(SBool, VC st SInteger)]
forall a. [a] -> [a] -> [a]
++ st -> [(SBool, VC st SInteger)]
measureDecreases   st
st'

-- | Check correctness using the default solver. Equivalent to @'wpProveWith' 'defaultWPCfg'@.
wpProve :: (Show res, Mergeable st, Queriable IO st res) => Program st -> IO (ProofResult res)
wpProve :: Program st -> IO (ProofResult res)
wpProve = WPConfig -> Program st -> IO (ProofResult res)
forall st res.
(Show res, Mergeable st, Queriable IO st res) =>
WPConfig -> Program st -> IO (ProofResult res)
wpProveWith WPConfig
defaultWPCfg

-- | Configuration for WP proofs.
data WPConfig = WPConfig { WPConfig -> SMTConfig
wpSolver  :: SMTConfig   -- ^ SMT Solver to use
                         , WPConfig -> Bool
wpVerbose :: Bool        -- ^ Should we be chatty?
                         }

-- | Default WP configuration: Uses the default solver, and is not verbose.
defaultWPCfg :: WPConfig
defaultWPCfg :: WPConfig
defaultWPCfg = WPConfig :: SMTConfig -> Bool -> WPConfig
WPConfig { wpSolver :: SMTConfig
wpSolver  = SMTConfig
defaultSMTCfg
                        , wpVerbose :: Bool
wpVerbose = Bool
False
                        }

-- * Concrete execution of a program

-- | Tracking locations: Either a line (sequence) number, or an iteration count
data Location = Line      Int
              | Iteration Int

-- | A 'Loc' is a nesting of locations. We store this in reverse order.
type Loc = [Location]

-- | Are we in a good state, or in a stuck state?
data Status st = Good st               -- ^ Execution finished in the given state.
               | Stuck (VC st Integer) -- ^ Execution got stuck, with the failing VC

-- | Show instance for 'Status'
instance Show st => Show (Status st) where
  show :: Status st -> String
show (Good st
st)  = String
"Program terminated successfully. Final state:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l | String
l <- String -> [String]
lines (st -> String
forall a. Show a => a -> String
show st
st)]
  show (Stuck VC st Integer
vc) = String
"Program is stuck.\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ VC st Integer -> String
forall a. Show a => a -> String
show VC st Integer
vc

-- | Trace the execution of a program, starting from a sufficiently concrete state. (Sufficiently here means that
-- all parts of the state that is used uninitialized must have concrete values, i.e., essentially the inputs.
-- You can leave the "temporary" variables initialized by the program before use undefined or even symbolic.)
-- The return value will have a 'Good' state to indicate the program ended successfully, if that is the case. The
-- result will be 'Stuck' if the program aborts without completing: This can happen either by executing an 'Abort'
-- statement, or some invariant gets violated, or if a metric fails to go down through a loop body.
traceExecution :: forall st. Show st
               => Program st            -- ^ Program
               -> st                    -- ^ Starting state. It must be fully concrete.
               -> IO (Status st)
traceExecution :: Program st -> st -> IO (Status st)
traceExecution Program{st -> SBool
precondition :: st -> SBool
precondition :: forall st. Program st -> st -> SBool
precondition, Stmt st
program :: Stmt st
program :: forall st. Program st -> Stmt st
program, st -> SBool
postcondition :: st -> SBool
postcondition :: forall st. Program st -> st -> SBool
postcondition, Stable st
stability :: Stable st
stability :: forall st. Program st -> Stable st
stability} st
start = do

                Status st
status <- if Loc -> String -> SBool -> Bool
forall a. SymVal a => Loc -> String -> SBV a -> a
unwrap [] String
"checking precondition" (st -> SBool
precondition st
start)
                          then Loc -> Stmt st -> Status st -> IO (Status st)
go [Int -> Location
Line Int
1] Stmt st
program (Status st -> IO (Status st)) -> IO (Status st) -> IO (Status st)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Loc -> st -> String -> IO (Status st)
step [] st
start String
"*** Precondition holds, starting execution:"
                          else st -> VC st Integer -> String -> IO (Status st)
giveUp st
start (st -> VC st Integer
forall st m. st -> VC st m
BadPrecondition st
start) String
"*** Initial state does not satisfy the precondition:"

                case Status st
status of
                  s :: Status st
s@Stuck{} -> Status st -> IO (Status st)
forall (m :: * -> *) a. Monad m => a -> m a
return Status st
s
                  Good st
end  -> if Loc -> String -> SBool -> Bool
forall a. SymVal a => Loc -> String -> SBV a -> a
unwrap [] String
"checking postcondition" (st -> SBool
postcondition st
end)
                               then Loc -> st -> String -> IO (Status st)
step [] st
end String
"*** Program successfully terminated, post condition holds of the final state:"
                               else st -> VC st Integer -> String -> IO (Status st)
giveUp st
end (st -> st -> VC st Integer
forall st m. st -> st -> VC st m
BadPostcondition st
start st
end) String
"*** Failed, final state does not satisfy the postcondition:"

  where sLoc :: Loc -> String -> String
        sLoc :: Loc -> String -> String
sLoc Loc
l String
m
          | Loc -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Loc
l = String
m
          | Bool
True   = String
"===> [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." ((Location -> String) -> Loc -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Location -> String
sh (Loc -> Loc
forall a. [a] -> [a]
reverse Loc
l)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m
          where sh :: Location -> String
sh (Line  Int
i)     = Int -> String
forall a. Show a => a -> String
show Int
i
                sh (Iteration Int
i) = String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"

        step :: Loc -> st -> String -> IO (Status st)
        step :: Loc -> st -> String -> IO (Status st)
step Loc
l st
st String
m = do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Loc -> String -> String
sLoc Loc
l String
m
                         st -> IO ()
printST st
st
                         Status st -> IO (Status st)
forall (m :: * -> *) a. Monad m => a -> m a
return (Status st -> IO (Status st)) -> Status st -> IO (Status st)
forall a b. (a -> b) -> a -> b
$ st -> Status st
forall st. st -> Status st
Good st
st

        stop :: Loc -> VC st Integer -> String -> IO (Status st)
        stop :: Loc -> VC st Integer -> String -> IO (Status st)
stop Loc
l VC st Integer
vc String
m = do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Loc -> String -> String
sLoc Loc
l String
m
                         Status st -> IO (Status st)
forall (m :: * -> *) a. Monad m => a -> m a
return (Status st -> IO (Status st)) -> Status st -> IO (Status st)
forall a b. (a -> b) -> a -> b
$ VC st Integer -> Status st
forall st. VC st Integer -> Status st
Stuck VC st Integer
vc

        giveUp :: st -> VC st Integer -> String -> IO (Status st)
        giveUp :: st -> VC st Integer -> String -> IO (Status st)
giveUp st
st VC st Integer
vc String
m = do Status st
r <- Loc -> VC st Integer -> String -> IO (Status st)
stop [] VC st Integer
vc String
m
                            st -> IO ()
printST st
st
                            Status st -> IO (Status st)
forall (m :: * -> *) a. Monad m => a -> m a
return Status st
r

        dispST :: st -> String
        dispST :: st -> String
dispST st
st = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l | String
l <- String -> [String]
lines (st -> String
forall a. Show a => a -> String
show st
st)]

        printST :: st -> IO ()
        printST :: st -> IO ()
printST = String -> IO ()
putStrLn (String -> IO ()) -> (st -> String) -> st -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. st -> String
dispST

        unwrap :: SymVal a => Loc -> String -> SBV a -> a
        unwrap :: Loc -> String -> SBV a -> a
unwrap Loc
l String
m SBV a
v = case SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
v of
                         Just a
c  -> a
c
                         Maybe a
Nothing -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                    , String
"*** Data.SBV.WeakestPreconditions.traceExecution:"
                                                    , String
"***"
                                                    , String
"***    Unable to extract concrete value:"
                                                    , String
"***      "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Loc -> String -> String
sLoc Loc
l String
m
                                                    , String
"***"
                                                    , String
"*** Make sure the starting state is fully concrete and"
                                                    , String
"*** there are no uninterpreted functions in play!"
                                                    ]

        go :: Loc -> Stmt st -> Status st -> IO (Status st)
        go :: Loc -> Stmt st -> Status st -> IO (Status st)
go Loc
_   Stmt st
_ s :: Status st
s@Stuck{}  = Status st -> IO (Status st)
forall (m :: * -> *) a. Monad m => a -> m a
return Status st
s
        go Loc
loc Stmt st
p (Good  st
st) = Stmt st -> IO (Status st)
analyze Stmt st
p
          where analyze :: Stmt st -> IO (Status st)
analyze Stmt st
Skip = Loc -> st -> String -> IO (Status st)
step Loc
loc st
st String
"Skip"

                analyze (Abort String
nm) = Loc -> VC st Integer -> String -> IO (Status st)
stop Loc
loc (String -> st -> st -> VC st Integer
forall st m. String -> st -> st -> VC st m
AbortReachable String
nm st
start st
st) (String -> IO (Status st)) -> String -> IO (Status st)
forall a b. (a -> b) -> a -> b
$ String
"Abort command executed, labeled: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm

                analyze (Assign st -> st
f) = case [String
nm | st -> st -> (String, SBool)
s <- Stable st
stability, let (String
nm, SBool
b) = st -> st -> (String, SBool)
s st
st st
st', Bool -> Bool
not (Loc -> String -> SBool -> Bool
forall a. SymVal a => Loc -> String -> SBV a -> a
unwrap Loc
loc (String
"evaluation stability condition " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm) SBool
b)] of
                                       []  -> Loc -> st -> String -> IO (Status st)
step Loc
loc st
st' String
"Assign"
                                       [String]
nms -> let comb :: String
comb = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
nms
                                                  bad :: VC st m
bad  = String -> st -> st -> VC st m
forall st m. String -> st -> st -> VC st m
Unstable String
comb st
st st
st'
                                              in Loc -> VC st Integer -> String -> IO (Status st)
stop Loc
loc VC st Integer
forall m. VC st m
bad (String -> IO (Status st)) -> String -> IO (Status st)
forall a b. (a -> b) -> a -> b
$ String
"Stability condition fails for: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
comb
                    where st' :: st
st' = st -> st
f st
st

                analyze (If st -> SBool
c Stmt st
tb Stmt st
eb)
                  | Bool
branchTrue       = Loc -> Stmt st -> Status st -> IO (Status st)
go (Int -> Location
Line Int
1 Location -> Loc -> Loc
forall a. a -> [a] -> [a]
: Loc
loc) Stmt st
tb (Status st -> IO (Status st)) -> IO (Status st) -> IO (Status st)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Loc -> st -> String -> IO (Status st)
step Loc
loc st
st String
"Conditional, taking the \"then\" branch"
                  | Bool
True             = Loc -> Stmt st -> Status st -> IO (Status st)
go (Int -> Location
Line Int
2 Location -> Loc -> Loc
forall a. a -> [a] -> [a]
: Loc
loc) Stmt st
eb (Status st -> IO (Status st)) -> IO (Status st) -> IO (Status st)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Loc -> st -> String -> IO (Status st)
step Loc
loc st
st String
"Conditional, taking the \"else\" branch"
                  where branchTrue :: Bool
branchTrue = Loc -> String -> SBool -> Bool
forall a. SymVal a => Loc -> String -> SBV a -> a
unwrap Loc
loc String
"evaluating the test condition" (st -> SBool
c st
st)

                analyze (Seq [Stmt st]
stmts)  = [Stmt st] -> Int -> Status st -> IO (Status st)
walk [Stmt st]
stmts Int
1 (st -> Status st
forall st. st -> Status st
Good st
st)
                  where walk :: [Stmt st] -> Int -> Status st -> IO (Status st)
walk []     Int
_ Status st
is = Status st -> IO (Status st)
forall (m :: * -> *) a. Monad m => a -> m a
return Status st
is
                        walk (Stmt st
s:[Stmt st]
ss) Int
c Status st
is = [Stmt st] -> Int -> Status st -> IO (Status st)
walk [Stmt st]
ss (Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Status st -> IO (Status st)) -> IO (Status st) -> IO (Status st)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Loc -> Stmt st -> Status st -> IO (Status st)
go (Int -> Location
Line Int
c Location -> Loc -> Loc
forall a. a -> [a] -> [a]
: Loc
loc) Stmt st
s Status st
is

                analyze (While String
loopName st -> SBool
invariant Maybe (Measure st)
mbMeasure st -> SBool
condition Stmt st
body)
                   | st -> Bool
currentInvariant st
st
                   = Int -> st -> Maybe [Integer] -> Status st -> IO (Status st)
while Int
1 st
st Maybe [Integer]
forall a. Maybe a
Nothing (st -> Status st
forall st. st -> Status st
Good st
st)
                   | Bool
True
                   = Loc -> VC st Integer -> String -> IO (Status st)
stop Loc
loc  (String -> st -> VC st Integer
forall st m. String -> st -> VC st m
InvariantPre String
loopName st
st) (String -> IO (Status st)) -> String -> IO (Status st)
forall a b. (a -> b) -> a -> b
$ String -> String
tag String
"invariant fails to hold prior to loop entry"
                   where tag :: String -> String
tag String
s = String
"Loop " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
loopName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s

                         hasMeasure :: Bool
hasMeasure = Maybe (Measure st) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (Measure st)
mbMeasure
                         measure :: Measure st
measure    = Maybe (Measure st) -> Measure st
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Measure st)
mbMeasure

                         currentCondition :: st -> Bool
currentCondition = Loc -> String -> SBool -> Bool
forall a. SymVal a => Loc -> String -> SBV a -> a
unwrap Loc
loc (String -> String
tag  String
"evaluating the while condition") (SBool -> Bool) -> (st -> SBool) -> st -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. st -> SBool
condition
                         currentMeasure :: st -> [Integer]
currentMeasure   = (SInteger -> Integer) -> [SInteger] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Loc -> String -> SInteger -> Integer
forall a. SymVal a => Loc -> String -> SBV a -> a
unwrap Loc
loc (String -> String
tag  String
"evaluating the measure"))   ([SInteger] -> [Integer]) -> Measure st -> st -> [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Measure st
measure
                         currentInvariant :: st -> Bool
currentInvariant = Loc -> String -> SBool -> Bool
forall a. SymVal a => Loc -> String -> SBV a -> a
unwrap Loc
loc (String -> String
tag  String
"evaluating the invariant")       (SBool -> Bool) -> (st -> SBool) -> st -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. st -> SBool
invariant

                         while :: Int -> st -> Maybe [Integer] -> Status st -> IO (Status st)
while Int
_ st
_      Maybe [Integer]
_      s :: Status st
s@Stuck{}  = Status st -> IO (Status st)
forall (m :: * -> *) a. Monad m => a -> m a
return Status st
s
                         while Int
c st
prevST Maybe [Integer]
mbPrev (Good  st
is)
                           | Bool -> Bool
not (st -> Bool
currentCondition st
is)
                           = Loc -> st -> String -> IO (Status st)
step Loc
loc st
is (String -> IO (Status st)) -> String -> IO (Status st)
forall a b. (a -> b) -> a -> b
$ String -> String
tag String
"condition fails, terminating"
                           | Bool -> Bool
not (st -> Bool
currentInvariant st
is)
                           = Loc -> VC st Integer -> String -> IO (Status st)
stop Loc
loc (String -> st -> st -> VC st Integer
forall st m. String -> st -> st -> VC st m
InvariantMaintain String
loopName st
prevST st
is) (String -> IO (Status st)) -> String -> IO (Status st)
forall a b. (a -> b) -> a -> b
$ String -> String
tag String
"invariant fails to hold in iteration " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
c
                           | Bool
hasMeasure Bool -> Bool -> Bool
&& [Integer]
mCur [Integer] -> [Integer] -> Bool
forall a. Ord a => a -> a -> Bool
< [Integer]
zero
                           = Loc -> VC st Integer -> String -> IO (Status st)
stop Loc
loc (String -> (st, [Integer]) -> VC st Integer
forall st m. String -> (st, [m]) -> VC st m
MeasureBound String
loopName (st
is, [Integer]
mCur)) (String -> IO (Status st)) -> String -> IO (Status st)
forall a b. (a -> b) -> a -> b
$ String -> String
tag String
"measure must be non-negative, evaluated to: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Integer] -> String
forall a. Show a => a -> String
show [Integer]
mCur
                           | Bool
hasMeasure, Just [Integer]
mPrev <- Maybe [Integer]
mbPrev, [Integer]
mCur [Integer] -> [Integer] -> Bool
forall a. Ord a => a -> a -> Bool
>= [Integer]
mPrev
                           = Loc -> VC st Integer -> String -> IO (Status st)
stop Loc
loc (String -> (st, [Integer]) -> (st, [Integer]) -> VC st Integer
forall st m. String -> (st, [m]) -> (st, [m]) -> VC st m
MeasureDecrease String
loopName (st
prevST, [Integer]
mPrev) (st
is, [Integer]
mCur)) (String -> IO (Status st)) -> String -> IO (Status st)
forall a b. (a -> b) -> a -> b
$ String -> String
tag (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"measure failed to decrease, prev = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Integer] -> String
forall a. Show a => a -> String
show [Integer]
mPrev String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", current = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Integer] -> String
forall a. Show a => a -> String
show [Integer]
mCur
                           | Bool
True
                           = do Status st
nextState <- Loc -> Stmt st -> Status st -> IO (Status st)
go (Int -> Location
Iteration Int
c Location -> Loc -> Loc
forall a. a -> [a] -> [a]
: Loc
loc) Stmt st
body (Status st -> IO (Status st)) -> IO (Status st) -> IO (Status st)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Loc -> st -> String -> IO (Status st)
step Loc
loc st
is (String -> String
tag String
"condition holds, executing the body")
                                Int -> st -> Maybe [Integer] -> Status st -> IO (Status st)
while (Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) st
is ([Integer] -> Maybe [Integer]
forall a. a -> Maybe a
Just [Integer]
mCur) Status st
nextState
                           where mCur :: [Integer]
mCur = st -> [Integer]
currentMeasure st
is
                                 zero :: [Integer]
zero = (Integer -> Integer) -> [Integer] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> Integer -> Integer
forall a b. a -> b -> a
const Integer
0) [Integer]
mCur

{-# ANN traceExecution ("HLint: ignore Use fromMaybe" :: String) #-}