afv-0.0.0: src/Verify.hs

module Verify (verify) where

import Control.Monad
import Data.IORef
import Data.List
import Data.Maybe
import Math.SMT.Yices.Pipe
import Math.SMT.Yices.Syntax
import System.IO
import Text.Printf

import Model

-- | Verify a model with k-induction.
verify :: FilePath -> Int -> Model -> IO ()
verify _ maxK _ | maxK < 1 = error "max k can not be less than 1"
verify yices maxK m = do
  y <- createYicesPipe yices []
  mapM_ (verifyModel y maxK) models
  exitY y
  where
  assertions = [ a | a@(Assert _ _ _) <- actions m ]
  models = map (trimModel . trimAssertions m) assertions

-- | Remove all assertions except one.
trimAssertions :: Model -> Action -> Model
trimAssertions m a = m { actions = filter keep $ actions m }
  where
  keep b@(Assert _ _ _) = a == b
  keep _ = True

-- | Trim all unneeded stuff from a model.
trimModel :: Model -> Model
trimModel = id  --XXX

-- | Verify a trimmed model.
verifyModel :: YicesIPC -> Int -> Model -> IO ()
verifyModel y maxK m = do
  printf "verifying assertion %s ...\n" (intercalate "." path) >> hFlush stdout
  withLogic y $ do
    initEnv <- initEnv y m
    check initEnv initEnv [] 1
  where
  [path] = [ path | Assert _ path _ <- actions m ]
  check :: Env -> Env -> [ExpY] -> Int -> IO ()
  check _ _ _ k | k > maxK = printf "inconclusive: unable to proved step up to max k = %d\n" maxK
  check initEnv env asserts k = do
    (env, assert) <- transition y m env
    resultBasis <- checkBasis y m initEnv (assert : asserts)
    case resultBasis of
      Fail -> printf "FAILED: disproved basis in k = %d\n" k
      Pass -> do
        resultStep <- checkStep y assert
        case resultStep of
          Fail -> withLogic y $ check initEnv env (assert : asserts) (k + 1)
          Pass -> printf "passed: proved step in k = %d\n" k
        
data Result = Pass | Fail

-- | Check induction step.
checkStep :: YicesIPC -> ExpY -> IO Result
checkStep y assert = do
  r <- withLogic y $ do
    runCmds y [ASSERT $ NOT assert]
    checkLogic y
  return $ result r

-- | Check induction basis.
checkBasis :: YicesIPC -> Model -> Env -> [ExpY] -> IO Result
checkBasis y m env asserts = do
  r <- withLogic y $ do
    runCmds y [ ASSERT $ VarE (getVar env (State a)) := exprConst t c | a@(VS _ t c _) <- variables m ]
    runCmds y [ASSERT $ NOT $ AND asserts]
    checkLogic y
  return $ result r

result :: ResY -> Result
result a = case a of
  Sat _   -> Fail
  UnSat _ -> Pass
  InCon _ -> Pass

-- | Does operation in a new stack.
withLogic :: YicesIPC -> IO a -> IO a
withLogic y a = do
  runCmds y [PUSH]
  a <- a
  runCmds y [POP]
  return a

-- | Transition relation.  Returns assertion.
transition :: YicesIPC -> Model -> Env -> IO (Env, ExpY)  -- (new env, assertion)
transition y m env = do
  (env', assert) <- foldM (action y) (env, LitB True) (actions m)
  --runCmds y [ ASSERT (VarE (getVar env $ State a) := VarE (getVar env' $ State a)) | a <- variables m ]
  return (env', assert)

action :: YicesIPC -> (Env, ExpY) -> Action -> IO (Env, ExpY)
action y (env, assert) a = case a of
  Assign v e -> do
    e <- expr y env (typeOf v) e
    env <- addVar y env v
    runCmds y [ASSERT $ VarE (getVar env v) := e]
    return (env, assert)
  Assert a _ _ -> do
    a <- expr y env Bool a
    return (env, AND [assert, a])
  Assume a _ _ -> do
    a <- expr y env Bool a
    runCmds y [ASSERT a]
    return (env, assert)

expr :: YicesIPC -> Env -> Type -> E -> IO ExpY
expr y env t a = case a of
  Var a@(Volatile _ _ _) -> do
    env <- addVar y env a
    return $ VarE $ getVar env a
  Var a -> return $ VarE $ getVar env a

  Const a -> return $ exprConst t a

  Not a _ -> do
    a <- expr y env Bool a
    return $ NOT a

  And a b _ -> do
    a <- expr y env Bool a
    b <- expr y env Bool b
    return $ AND [a, b]

  Or  a b _ -> do
    a <- expr y env Bool a
    b <- expr y env Bool b
    return $ OR  [a, b]

  Mul a b _ -> do
    a <- expr y env t a
    b <- expr y env t b
    return $ a :*: b
  
  Div a b _  -> do
    a <- expr y env t a
    b <- expr y env t b
    return $ op a b
    where
    op = case t of
      Integer _ -> DIV
      _         -> (:/:)

  Mod a b _ -> do
    a <- expr y env t a
    b <- expr y env t b
    return $ MOD a b

  Add a b _ -> do
    a <- expr y env t a
    b <- expr y env t b
    return $ a :+: b

  Sub a b _ -> do
    a <- expr y env t a
    b <- expr y env t b
    return $ a :-: b

  Lt  a b n -> do
    let t' = unify n (typeOf a) (typeOf b)
    a <- expr y env t' a
    b <- expr y env t' b
    return $ a :< b

  Eq  a b n -> do
    let t' = unify n (typeOf a) (typeOf b)
    a <- expr y env t' a
    b <- expr y env t' b
    return $ a := b

  Mux a b c n -> do
    let t' = unify n (typeOf b) (typeOf c)
    a <- expr y env Bool a
    b <- expr y env t' b
    c <- expr y env t' c
    return $ IF a b c

exprConst :: Type -> Const -> ExpY
exprConst t a = case a of 
  CBool     a _ -> LitB a
  CInteger  a _ | t == Bool -> LitB $ a /= 0
                | otherwise -> LitI a
  CRational a _ -> LitR a




data Env = Env NextId [(V, String)]  -- Env nextId table

initEnv :: YicesIPC -> Model -> IO Env
initEnv y m = do
  nid <- newNextId
  foldM (addVar y) (Env nid []) $ map State $ variables m

addVar :: YicesIPC -> Env -> V -> IO Env
addVar y (Env nid table) v = do
  i <- nextId nid
  let name = printf "n%d" i
  runCmds y [DEFINE (name, VarT $ typeY v) Nothing]
  return $ Env nid $ replace (v, name) table

getVar :: Env -> V -> String
getVar (Env _ table) v = case lookup v table of
  Just a -> a
  Nothing -> error $ "Verify.getVar: variable not found: " ++ show v  ++ " in " ++ show (fst $ unzip table)

replace :: Eq a => (a, b) -> [(a, b)] -> [(a, b)]
replace a [] = [a]
replace (a, b) ((a', b') : c) | a == a'   = (a, b) : c
                              | otherwise = (a', b') : replace (a, b) c






typeY :: TypeOf a => a -> String
typeY a = case typeOf a of
  Void       -> error "Verify.typeY: void time"
  Bool       -> "bool"
  Integer  _ -> "int"
  Rational _ -> "real"



newtype NextId = NextId (IORef Int)

newNextId :: IO NextId
newNextId = newIORef 0 >>= (return . NextId)

nextId :: NextId -> IO Int
nextId (NextId a) = do
  i <- readIORef a
  writeIORef a $ i + 1
  return i


verbose :: Bool
verbose = False

runCmds :: YicesIPC -> [CmdY] -> IO ()
runCmds y cmds = do
  when verbose $ mapM_ (putStrLn . show) cmds
  runCmdsY' y cmds

checkLogic :: YicesIPC -> IO ResY
checkLogic y = do
  when verbose $ do
    putStrLn "(check)"
    hFlush stdout
  checkY y