language-boogie-0.2: Language/Boogie/Interpreter.hs
{-# LANGUAGE FlexibleContexts, Rank2Types #-}
-- | Interpreter for Boogie 2
module Language.Boogie.Interpreter (
-- * Executing programs
executeProgramDet,
executeProgram,
executeProgramGeneric,
-- * Run-time failures
FailureSource (..),
-- InternalCode,
StackFrame (..),
StackTrace,
RuntimeFailure (..),
runtimeFailureDoc,
FailureKind (..),
failureKind,
-- * Execution outcomes
TestCase (..),
isPass,
isInvalid,
isNonexecutable,
isFail,
testCaseSummary,
finalStateDoc,
Summary (..),
testSessionSummary,
summaryDoc,
-- * Executing parts of programs
eval,
exec,
execProcedure,
preprocess
) where
import Language.Boogie.Environment
import Language.Boogie.AST
import Language.Boogie.Util
import Language.Boogie.Heap
import Language.Boogie.Generator
import Language.Boogie.Intervals
import Language.Boogie.Position
import Language.Boogie.Tokens (nonIdChar)
import Language.Boogie.PrettyPrinter
import Language.Boogie.TypeChecker
import Language.Boogie.NormalForm
import Language.Boogie.BasicBlocks
import Data.Maybe
import Data.List
import Data.Map (Map, (!))
import qualified Data.Map as M
import Data.Set (Set)
import qualified Data.Set as S
import Control.Monad.Error hiding (join)
import Control.Applicative hiding (empty)
import Control.Monad.State hiding (join)
import Control.Monad.Identity hiding (join)
import Control.Monad.Stream
import Control.Lens hiding (Context, at)
import Text.PrettyPrint
{- Interface -}
-- | 'executeProgram' @p tc entryPoint@ :
-- Execute program @p@ /non-deterministically/ in type context @tc@ starting from procedure @entryPoint@
-- and return an infinite list of possible outcomes (each either runtime failure or the final variable store).
-- Whenever a value is unspecified, all values of the required type are tried exhaustively.
executeProgram :: Program -> Context -> Generator Stream -> Maybe Integer -> Id -> [TestCase]
executeProgram p tc gen qbound entryPoint = toList $ executeProgramGeneric p tc gen qbound entryPoint
-- | 'executeProgramDet' @p tc entryPoint@ :
-- Execute program @p@ /deterministically/ in type context @tc@ starting from procedure @entryPoint@
-- and return a single outcome.
-- Whenever a value is unspecified, a default value of the required type is used.
executeProgramDet :: Program -> Context -> Maybe Integer -> Id -> TestCase
executeProgramDet p tc qbound entryPoint = runIdentity $ executeProgramGeneric p tc defaultGenerator qbound entryPoint
-- | 'executeProgramGeneric' @p tc generator qbound entryPoint@ :
-- Execute program @p@ in type context @tc@ with input generator @generator@, starting from procedure @entryPoint@,
-- and return the outcome(s) embedded into the generator's monad.
executeProgramGeneric :: (Monad m, Functor m) => Program -> Context -> Generator m -> Maybe Integer -> Id -> m (TestCase)
executeProgramGeneric p tc generator qbound entryPoint = result <$> runStateT (runErrorT programExecution) (initEnv tc generator qbound)
where
programExecution = do
execUnsafely $ preprocess p
execRootCall
sig = procSig entryPoint tc
execRootCall = do
let params = psigParams sig
let defaultBinding = M.fromList $ zip (psigTypeVars sig) (repeat defaultType)
let paramTypes = map (typeSubst defaultBinding) (map itwType params)
envTypeContext %= setLocals (M.fromList $ zip (map itwId params) paramTypes)
execCallBySig (assumePreconditions sig) (map itwId (psigRets sig)) (map (gen . Var . itwId) (psigArgs sig)) noPos
defaultType = BoolType
result (Left err, env) = TestCase sig (env^.envMemory) (Just err)
result (_, env) = TestCase sig (env^.envMemory) Nothing
{- Executions -}
-- | Computations with 'Environment' as state, which can result in either @a@ or 'RuntimeFailure'
type Execution m a = ErrorT RuntimeFailure (StateT (Environment m) m) a
-- | Computations with 'Environment' as state, which always result in @a@
type SafeExecution m a = StateT (Environment m) m a
-- | 'execUnsafely' @computation@ : Execute a safe @computation@ in an unsafe environment
execUnsafely :: (Monad m, Functor m) => SafeExecution m a -> Execution m a
execUnsafely computation = ErrorT (Right <$> computation)
-- | 'execSafely' @computation handler@ : Execute an unsafe @computation@ in a safe environment, handling errors that occur in @computation@ with @handler@
execSafely :: (Monad m, Functor m) => Execution m a -> (RuntimeFailure -> SafeExecution m a) -> SafeExecution m a
execSafely computation handler = do
eres <- runErrorT computation
either handler return eres
-- | Computations that perform a cleanup at the end
class Monad s => Finalizer s where
finally :: s a -> s () -> s a
instance Monad m => Finalizer (StateT s m) where
finally main cleanup = do
res <- main
cleanup
return res
instance (Error e, Monad m) => Finalizer (ErrorT e m) where
finally main cleanup = do
res <- main `catchError` (\err -> cleanup >> throwError err)
cleanup
return res
-- | Run execution in the old environment
old :: (Monad m, Functor m) => Execution m a -> Execution m a
old execution = do
oldEnv <- get
envMemory.memGlobals .= oldEnv^.envMemory.memOld
envInOld .= True
res <- execution
env <- get
envMemory.memOld .= env^.envMemory.memGlobals
envMemory.memGlobals .= (oldEnv^.envMemory.memGlobals) `M.union` (env^.envMemory.memGlobals) -- Include freshly initialized globals into both old and new states
envInOld .= oldEnv^.envInOld
return res
-- | Save current values of global variables in memOld, return the previous memory
saveOld :: (Monad m, Functor m) => Execution m Memory
saveOld = do
mem <- use envMemory
let globals = mem^.memGlobals
envMemory.memOld .= globals
mapM_ incRefCountValue (M.elems globals) -- Each value stored in globals is now pointed by an additional (old) variable
return $ mem
-- | 'restoreOld' @oldMem@ : reset 'memOld' to its value from @oldMem@
restoreOld :: (Monad m, Functor m) => Memory -> Execution m ()
restoreOld oldMem = do
mem <- use envMemory
let (oldOlds, newOlds) = M.partitionWithKey (\var _ -> M.member var (oldMem^.memGlobals)) (mem^.memOld)
envMemory.memOld .= (oldMem^.memOld) `M.union` newOlds -- Add old values for freshly initialized globals (they are valid up until the program entry point, so could be accessed until the end of the program)
mapM_ decRefCountValue (M.elems oldOlds) -- Old values for previously initialized varibles go out of scope
-- | Enter local scope (apply localTC to the type context and assign actuals to formals),
-- execute computation,
-- then restore type context and local variables to their initial values
executeLocally :: (MonadState (Environment m) s, Finalizer s) => (Context -> Context) -> [Id] -> [Id] -> [Value] -> AbstractStore -> s a -> s a
executeLocally localTC locals formals actuals localConstraints computation = do
oldEnv <- get
envTypeContext %= localTC
envMemory.memLocals %= deleteAll locals
envConstraints.amLocals .= localConstraints
zipWithM_ (setVar memLocals) formals actuals -- All formals are fresh, can use emptyStore for current values
computation `finally` unwind oldEnv
where
-- | Restore type context and the values of local variables
unwind oldEnv = do
mapM_ (unsetVar memLocals) locals
env <- get
envTypeContext .= oldEnv^.envTypeContext
envMemory.memLocals .= deleteAll locals (env^.envMemory.memLocals) `M.union` (oldEnv^.envMemory.memLocals)
envConstraints.amLocals .= oldEnv^.envConstraints.amLocals -- Constraints cannot be initialized in a nested context, so here we can just restore old locals
{- Runtime failures -}
data FailureSource =
SpecViolation SpecClause | -- ^ Violation of user-defined specification
DivisionByZero | -- ^ Division by zero
UnsupportedConstruct String | -- ^ Language construct is not yet supported (should disappear in later versions)
InfiniteDomain Id Interval | -- ^ Quantification over an infinite set
MapEquality Value Value | -- ^ Equality of two maps cannot be determined
InternalException InternalCode -- ^ Must be cought inside the interpreter and never reach the user
deriving Eq
-- | Information about a procedure or function call
data StackFrame = StackFrame {
callPos :: SourcePos, -- ^ Source code position of the call
callName :: Id -- ^ Name of procedure or function
} deriving Eq
type StackTrace = [StackFrame]
-- | Failures that occur during execution
data RuntimeFailure = RuntimeFailure {
rtfSource :: FailureSource, -- ^ Source of the failure
rtfPos :: SourcePos, -- ^ Location where the failure occurred
rtfMemory :: Memory, -- ^ Memory state at the time of failure
rtfTrace :: StackTrace -- ^ Stack trace from the program entry point to the procedure where the failure occurred
}
-- | Throw a run-time failure
throwRuntimeFailure source pos = do
mem <- use envMemory
throwError (RuntimeFailure source pos mem [])
-- | Push frame on the stack trace of a runtime failure
addStackFrame frame (RuntimeFailure source pos mem trace) = throwError (RuntimeFailure source pos mem (frame : trace))
-- | Kinds of run-time failures
data FailureKind = Error | -- ^ Error state reached (assertion violation)
Unreachable | -- ^ Unreachable state reached (assumption violation)
Nonexecutable -- ^ The state is OK in Boogie semantics, but the execution cannot continue due to the limitations of the interpreter
deriving Eq
-- | Kind of a run-time failure
failureKind :: RuntimeFailure -> FailureKind
failureKind err = case rtfSource err of
SpecViolation (SpecClause _ True _) -> Unreachable
SpecViolation (SpecClause _ False _) -> Error
DivisionByZero -> Error
_ -> Nonexecutable
instance Error RuntimeFailure where
noMsg = RuntimeFailure (UnsupportedConstruct "unknown") noPos emptyMemory []
strMsg s = RuntimeFailure (UnsupportedConstruct s) noPos emptyMemory []
-- | Pretty-printed run-time failure
runtimeFailureDoc debug err =
let store = (if debug then id else userStore ((rtfMemory err)^.memHeap)) (M.filterWithKey (\k _ -> isRelevant k) (visibleVariables (rtfMemory err)))
sDoc = storeDoc store
in failureSourceDoc (rtfSource err) <+> posDoc (rtfPos err) <+>
(if isEmpty sDoc then empty else text "with") $+$ nest 2 sDoc $+$
vsep (map stackFrameDoc (reverse (rtfTrace err)))
where
failureSourceDoc (SpecViolation (SpecClause specType isFree e)) = text (clauseName specType isFree) <+> doubleQuotes (exprDoc e) <+> defPosition specType e <+> text "violated"
failureSourceDoc (DivisionByZero) = text "Division by zero"
failureSourceDoc (InfiniteDomain var int) = text "Variable" <+> text var <+> text "quantified over an infinite domain" <+> text (show int)
failureSourceDoc (MapEquality m1 m2) = text "Cannot determine equality of map values" <+> valueDoc m1 <+> text "and" <+> valueDoc m2
failureSourceDoc (UnsupportedConstruct s) = text "Unsupported construct" <+> text s
clauseName Inline isFree = if isFree then "Assumption" else "Assertion"
clauseName Precondition isFree = if isFree then "Free precondition" else "Precondition"
clauseName Postcondition isFree = if isFree then "Free postcondition" else "Postcondition"
clauseName LoopInvariant isFree = if isFree then "Free loop invariant" else "Loop invariant"
clauseName Where True = "Where clause" -- where clauses cannot be non-free
clauseName Axiom True = "Axiom" -- axioms cannot be non-free
defPosition Inline _ = empty
defPosition LoopInvariant _ = empty
defPosition _ e = text "defined" <+> posDoc (position e)
isRelevant k = case rtfSource err of
SpecViolation (SpecClause _ _ expr) -> k `elem` freeVars expr
_ -> False
stackFrameDoc f = text "in call to" <+> text (callName f) <+> posDoc (callPos f)
posDoc pos
| pos == noPos = text "from the environment"
| otherwise = text "at" <+> text (sourceName pos) <+> text "line" <+> int (sourceLine pos)
instance Show RuntimeFailure where
show err = show (runtimeFailureDoc True err)
-- | Do two runtime failures represent the same fault?
-- Yes if the same property failed at the same program location
-- or, for preconditions, for the same caller
sameFault f f' = rtfSource f == rtfSource f' &&
case rtfSource f of
SpecViolation (SpecClause Precondition False _) -> last (rtfTrace f) == last (rtfTrace f')
_ -> rtfPos f == rtfPos f'
instance Eq RuntimeFailure where
f == f' = sameFault f f'
-- | Internal error codes
data InternalCode = NotLinear | UnderConstruction Int
deriving Eq
throwInternalException code = throwRuntimeFailure (InternalException code) noPos
{- Execution results -}
-- | Description of an execution
data TestCase = TestCase {
tcProcedure :: PSig, -- ^ Root procedure (entry point) of the execution
tcMemory :: Memory, -- ^ Final memory state (at the exit from the root procedure)
tcFailure :: Maybe RuntimeFailure -- ^ Failure the execution eded with, or Nothing if the execution ended in a valid state
}
-- | 'isPass' @tc@: Does @tc@ end in a valid state?
isPass :: TestCase -> Bool
isPass (TestCase _ _ Nothing) = True
isPass _ = False
-- | 'isInvalid' @tc@: Does @tc@ and in an unreachable state?
isInvalid :: TestCase -> Bool
isInvalid (TestCase _ _ (Just err))
| failureKind err == Unreachable = True
isInvalid _ = False
-- | 'isNonexecutable' @tc@: Does @tc@ end in a non-executable state?
isNonexecutable :: TestCase -> Bool
isNonexecutable (TestCase _ _ (Just err))
| failureKind err == Nonexecutable = True
isNonexecutable _ = False
-- | 'isFail' @tc@: Does @tc@ end in an error state?
isFail :: TestCase -> Bool
isFail tc = not (isPass tc || isInvalid tc || isNonexecutable tc)
-- | 'testCaseSummary' @debug tc@ : Summary of @tc@'s inputs and outcome,
-- displayed in user or debug format depending on 'debug'
testCaseSummary :: Bool -> TestCase -> Doc
testCaseSummary debug tc@(TestCase sig mem mErr) = text (psigName sig) <>
parens (commaSep (map (inDoc . itwId) (psigArgs sig))) <>
(if M.null globalInputsRepr then empty else parens (commaSep (map globDoc (M.toList globalInputsRepr)))) <+>
outcomeDoc tc
where
storeRepr store = if debug then store else userStore (mem^.memHeap) store
removeEmptyMaps store = M.filter (\val -> val /= MapValue emptyMap) store
localsRepr = storeRepr $ mem^.memLocals
globalInputsRepr = removeEmptyMaps . storeRepr $ (mem^.memOld) `M.union` (mem^.memConstants)
inDoc name = valueDoc $ localsRepr ! name
globDoc (name, val) = text name <+> text "=" <+> valueDoc val
outcomeDoc tc
| isPass tc = text "passed"
| isInvalid tc = text "invalid"
| isNonexecutable tc = text "non-executable"
| otherwise = text "failed"
-- | 'finalStateDoc' @debug tc@ : outputs of @tc@,
-- displayed in user or debug format depending on 'debug'
finalStateDoc :: Bool -> TestCase -> Doc
finalStateDoc debug tc@(TestCase sig mem mErr) = vsep $
(if M.null outsRepr then [] else [text "Outs:" <+> storeDoc outsRepr]) ++
(if M.null globalsRepr then [] else [text "Globals:" <+> storeDoc globalsRepr]) ++
(if debug then [text "Heap:" <+> heapDoc (mem^.memHeap)] else [])
where
storeRepr store = if debug then store else userStore (mem^.memHeap) store
outNames = map itwId (psigRets sig)
outsRepr = storeRepr $ M.filterWithKey (\k _ -> k `elem` outNames) (mem^.memLocals)
globalsRepr = storeRepr $ mem^.memGlobals
-- | Test cases are considered equivalent from a user perspective
-- | if they are testing the same procedure and result in the same outcome
equivalent tc1 tc2 = tcProcedure tc1 == tcProcedure tc2 && tcFailure tc1 == tcFailure tc2
-- | Test session summary
data Summary = Summary {
sPassCount :: Int, -- ^ Number of passing test cases
sFailCount :: Int, -- ^ Number of failing test cases
sInvalidCount :: Int, -- ^ Number of invalid test cases
sNonExecutableCount :: Int, -- ^ Number of nonexecutable test cases
sUniqueFailures :: [TestCase] -- ^ Unique failing test cases
}
totalCount s = sPassCount s + sFailCount s + sInvalidCount s + sNonExecutableCount s
-- | Pretty-printed test session summary
summaryDoc :: Summary -> Doc
summaryDoc summary =
text "Test cases:" <+> int (totalCount summary) $+$
text "Passed:" <+> int (sPassCount summary) $+$
text "Invalid:" <+> int (sInvalidCount summary) $+$
text "Non executable:" <+> int (sNonExecutableCount summary) $+$
text "Failed:" <+> int (sFailCount summary) <+> parens (int (length (sUniqueFailures summary)) <+> text "unique") <>
(if null (sUniqueFailures summary) then empty else newline)
instance Show Summary where show s = show (summaryDoc s)
-- | Summary of a set of test cases
testSessionSummary :: [TestCase] -> Summary
testSessionSummary tcs = let
passing = filter isPass tcs
failing = filter isFail tcs
invalid = filter isInvalid tcs
nexec = filter isNonexecutable tcs
in Summary {
sPassCount = length passing,
sFailCount = length failing,
sInvalidCount = length invalid,
sNonExecutableCount = length nexec,
sUniqueFailures = nubBy equivalent failing
}
{- Basic executions -}
-- | 'generate' @f@ : computation that extracts @f@ from the generator
generate :: (Monad m, Functor m) => (Generator m -> m a) -> Execution m a
generate f = do
gen <- use envGenerator
lift (lift (f gen))
-- | 'generateValue' @t pos@ : choose a value of type @t@ at source position @pos@;
-- fail if @t@ is a type variable
generateValue :: (Monad m, Functor m) => Type -> SourcePos -> Execution m Value
generateValue t pos = case t of
IdType x [] | isTypeVar [] x -> throwRuntimeFailure (UnsupportedConstruct ("choice of a value from unknown type " ++ show t)) pos
-- Maps are initializaed lazily, allocate an empty map on the heap:
MapType _ _ _ -> allocate $ MapValue emptyMap
BoolType -> BoolValue <$> generate genBool
IntType -> IntValue <$> generate genInteger
IdType id _ -> do
n <- gets $ lookupCustomCount id
i <- generate (`genIndex` (n + 1))
when (i == n) $ modify (setCustomCount id (n + 1))
return $ CustomValue id i
-- | 'generateValueLike' @v@ : choose a value of the same type as @v@
generateValueLike :: (Monad m, Functor m) => Value -> Execution m Value
generateValueLike (BoolValue _) = generateValue BoolType noPos
generateValueLike (IntValue _) = generateValue IntType noPos
generateValueLike (CustomValue t _) = generateValue (IdType t []) noPos
generateValueLike (Reference _) = allocate $ MapValue emptyMap
generateValueLike (MapValue _) = internalError "Attempt to generateValueLike a map value directly"
-- | 'incRefCountValue' @val@ : if @val@ is a reference, increase its count
incRefCountValue val = case val of
Reference r -> envMemory.memHeap %= incRefCount r
_ -> return ()
-- | 'decRefCountValue' @val@ : if @val@ is a reference, decrease its count
decRefCountValue val = case val of
Reference r -> envMemory.memHeap %= decRefCount r
_ -> return ()
-- | 'unsetVar' @getter name@ : if @name@ was associated with a reference in @getter@, decrease its reference count
unsetVar getter name = do
store <- use $ envMemory.getter
case M.lookup name store of
Just (Reference r) -> do
envMemory.memHeap %= decRefCount r
_ -> return ()
-- | 'setVar' @setter name val@ : set value of variable @name@ to @val@ using @setter@
setVar setter name val = do
incRefCountValue val
envMemory.setter %= M.insert name val
-- | 'resetVar' @lens name val@ : set value of variable @name@ to @val@ using @lens@;
-- if @name@ was associated with a reference, decrease its reference count
resetVar :: (Monad m, Functor m) => StoreLens -> Id -> Value -> Execution m ()
resetVar lens name val = do
unsetVar lens name
setVar lens name val
-- | 'resetAnyVar' @name val@ : set value of a constant, global or local variable @name@ to @val@
resetAnyVar name val = do
tc <- use envTypeContext
if M.member name (localScope tc)
then resetVar memLocals name val
else if M.member name (ctxGlobals tc)
then resetVar memGlobals name val
else resetVar memConstants name val
-- | 'forgetVar' @lens name@ : forget value of variable @name@ in @lens@;
-- if @name@ was associated with a reference, decrease its reference count
forgetVar :: (Monad m, Functor m) => StoreLens -> Id -> Execution m ()
forgetVar lens name = do
unsetVar lens name
envMemory.lens %= M.delete name
-- | 'forgetAnyVar' @name@ : forget value of a constant, global or local variable @name@ to @val@
forgetAnyVar name = do
tc <- use envTypeContext
if M.member name (localScope tc)
then forgetVar memLocals name
else if M.member name (ctxGlobals tc)
then forgetVar memGlobals name
else forgetVar memConstants name
-- | 'setMapValue' @r index val@ : map @index@ to @val@ in the map referenced by @r@
-- (@r@ has to be a source map)
setMapValue r index val = do
MapValue (Source baseVals) <- readHeap r
envMemory.memHeap %= update r (MapValue (Source (M.insert index val baseVals)))
incRefCountValue val
-- | 'forgetMapValue' @r index@ : forget value at @index@ in the map referenced by @r@
-- (@r@ has to be a source map)
forgetMapValue r index = do
MapValue (Source baseVals) <- readHeap r
case M.lookup index baseVals of
Nothing -> return ()
Just val -> do
decRefCountValue val
envMemory.memHeap %= update r (MapValue (Source (M.delete index baseVals)))
-- | 'readHeap' @r@: current value of reference @r@ in the heap
readHeap r = flip at r <$> use (envMemory.memHeap)
-- | 'allocate' @v@: store @v@ at a fresh location in the heap and return that location
allocate :: (Monad m, Functor m) => Value -> Execution m Value
allocate v = Reference <$> (state . withHeap . alloc) v
-- | Remove all unused references from the heap
collectGarbage :: (Monad m, Functor m) => Execution m ()
collectGarbage = do
h <- use (envMemory.memHeap)
when (hasGarbage h) (do
r <- state $ withHeap dealloc
let MapValue repr = h `at` r
case repr of
Source _ -> return ()
Derived base _ -> envMemory.memHeap %= decRefCount base
mapM_ decRefCountValue (M.elems $ stored repr)
envConstraints.amHeap %= M.delete r
collectGarbage)
{- Expressions -}
-- | Semantics of unary operators
unOp :: UnOp -> Value -> Value
unOp Neg (IntValue n) = IntValue (-n)
unOp Not (BoolValue b) = BoolValue (not b)
-- | Semi-strict semantics of binary operators:
-- 'binOpLazy' @op lhs@ : returns the value of @lhs op@ if already defined, otherwise Nothing
binOpLazy :: BinOp -> Value -> Maybe Value
binOpLazy And (BoolValue False) = Just $ BoolValue False
binOpLazy Or (BoolValue True) = Just $ BoolValue True
binOpLazy Implies (BoolValue False) = Just $ BoolValue True
binOpLazy Explies (BoolValue True) = Just $ BoolValue True
binOpLazy _ _ = Nothing
-- | Strict semantics of binary operators
binOp :: (Monad m, Functor m) => SourcePos -> BinOp -> Value -> Value -> Execution m Value
binOp pos Plus (IntValue n1) (IntValue n2) = return $ IntValue (n1 + n2)
binOp pos Minus (IntValue n1) (IntValue n2) = return $ IntValue (n1 - n2)
binOp pos Times (IntValue n1) (IntValue n2) = return $ IntValue (n1 * n2)
binOp pos Div (IntValue n1) (IntValue n2) = if n2 == 0
then throwRuntimeFailure DivisionByZero pos
else return $ IntValue (fst (n1 `euclidean` n2))
binOp pos Mod (IntValue n1) (IntValue n2) = if n2 == 0
then throwRuntimeFailure DivisionByZero pos
else return $ IntValue (snd (n1 `euclidean` n2))
binOp pos Leq (IntValue n1) (IntValue n2) = return $ BoolValue (n1 <= n2)
binOp pos Ls (IntValue n1) (IntValue n2) = return $ BoolValue (n1 < n2)
binOp pos Geq (IntValue n1) (IntValue n2) = return $ BoolValue (n1 >= n2)
binOp pos Gt (IntValue n1) (IntValue n2) = return $ BoolValue (n1 > n2)
binOp pos And (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 && b2)
binOp pos Or (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 || b2)
binOp pos Implies (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 <= b2)
binOp pos Explies (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 >= b2)
binOp pos Equiv (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 == b2)
binOp pos Eq v1 v2 = evalEquality v1 v2
binOp pos Neq v1 v2 = vnot <$> evalEquality v1 v2
binOp pos Lc v1 v2 = throwRuntimeFailure (UnsupportedConstruct "orders") pos
-- | Euclidean division used by Boogie for integer division and modulo
euclidean :: Integer -> Integer -> (Integer, Integer)
a `euclidean` b =
case a `quotRem` b of
(q, r) | r >= 0 -> (q, r)
| b > 0 -> (q - 1, r + b)
| otherwise -> (q + 1, r - b)
-- | Evaluate an expression;
-- can have a side-effect of initializing variables that were not previously defined
eval :: (Monad m, Functor m) => Expression -> Execution m Value
eval expr = case node expr of
TT -> return $ BoolValue True
FF -> return $ BoolValue False
Numeral n -> return $ IntValue n
Var name -> evalVar name (position expr)
Application name args -> evalMapSelection (functionExpr name) args (position expr)
MapSelection m args -> evalMapSelection m args (position expr)
MapUpdate m args new -> evalMapUpdate m args new (position expr)
Old e -> old $ eval e
IfExpr cond e1 e2 -> evalIf cond e1 e2
Coercion e t -> eval e
UnaryExpression op e -> unOp op <$> eval e
BinaryExpression op e1 e2 -> evalBinary op e1 e2
Quantified Lambda _ _ _ -> throwRuntimeFailure (UnsupportedConstruct "lambda expressions") (position expr)
Quantified Forall tv vars e -> vnot <$> evalExists tv vars (enot e) (position expr)
Quantified Exists tv vars e -> evalExists tv vars e (position expr)
where
functionExpr name = gen . Var $ functionConst name
evalVar :: (Monad m, Functor m) => Id -> SourcePos -> Execution m Value
evalVar name pos = do
tc <- use envTypeContext
case M.lookup name (localScope tc) of
Just t -> evalVarWith t memLocals False
Nothing -> case M.lookup name (ctxGlobals tc) of
Just t -> do
inOld <- use envInOld
evalVarWith t memGlobals (not inOld) -- Unless we are evaluating and old expression, also initialize the old value of the global
Nothing -> case M.lookup name (ctxConstants tc) of
Just t -> evalVarWith t memConstants False
Nothing -> (internalError . show) (text "Encountered unknown identifier during execution:" <+> text name)
where
evalVarWith :: (Monad m, Functor m) => Type -> StoreLens -> Bool -> Execution m Value
evalVarWith t lens initOld = do
s <- use $ envMemory.lens
case M.lookup name s of -- Lookup a cached value
Just val -> wellDefined val
Nothing -> do -- If not found, look for an applicable definition
definedValue <- checkNameDefinitions name t pos
case definedValue of
Just val -> do
setVar lens name val
checkNameConstraints name pos
forgetVar lens name
return val
Nothing -> do -- If not found, choose a value non-deterministically
chosenValue <- generateValue t pos
setVar lens name chosenValue
when initOld $ setVar memOld name chosenValue
checkNameConstraints name pos
return chosenValue
rejectMapIndex pos idx = case idx of
Reference r -> throwRuntimeFailure (UnsupportedConstruct "map as an index") pos
_ -> return ()
evalMapSelection m args pos = do
argsV <- mapM eval args
Reference r <- eval m
h <- use $ envMemory.memHeap
let (s, vals) = flattenMap h r
case M.lookup argsV vals of -- Lookup a cached value
Just val -> wellDefined val
Nothing -> do -- If not found, look for an applicable definition
tc <- use envTypeContext
let mapType = exprType tc m
definedValue <- checkMapDefinitions s mapType args argsV pos
case definedValue of
Just val -> do
setMapValue s argsV val
checkMapConstraints s mapType args argsV pos
forgetMapValue s argsV
return val
Nothing -> do -- If not found, choose a value non-deterministically
mapM_ (rejectMapIndex pos) argsV
let rangeType = exprType tc (gen $ MapSelection m args)
chosenValue <- generateValue rangeType pos
setMapValue s argsV chosenValue
checkMapConstraints s mapType args argsV pos
return chosenValue
evalMapUpdate m args new pos = do
Reference r <- eval m
argsV <- mapM eval args
mapM_ (rejectMapIndex pos) argsV
newV <- eval new
MapValue repr <- readHeap r
let
(newSource, newRepr) = case repr of
Source _ -> (r, Derived r (M.singleton argsV newV))
Derived base override -> (base, Derived base (M.insert argsV newV override))
mapM_ incRefCountValue (M.elems $ stored newRepr)
envMemory.memHeap %= incRefCount newSource
allocate $ MapValue newRepr
evalIf cond e1 e2 = do
v <- eval cond
case v of
BoolValue True -> eval e1
BoolValue False -> eval e2
evalBinary op e1 e2 = do
left <- eval e1
case binOpLazy op left of
Just result -> return result
Nothing -> do
right <- eval e2
binOp (position e1) op left right
-- | Finite domain
type Domain = [Value]
evalExists :: (Monad m, Functor m) => [Id] -> [IdType] -> Expression -> SourcePos -> Execution m Value
evalExists tv vars e pos = let Quantified Exists tv' vars' e' = node $ normalize (attachPos pos $ Quantified Exists tv vars e)
in evalExists' tv' vars' e'
evalExists' :: (Monad m, Functor m) => [Id] -> [IdType] -> Expression -> Execution m Value
evalExists' tv vars e = do
localConstraints <- use $ envConstraints.amLocals
BoolValue <$> executeLocally (enterQuantified tv vars) (map fst vars) [] [] localConstraints evalWithDomains
where
evalWithDomains = do
doms <- domains e varNames
evalForEach varNames doms
-- | evalForEach vars domains: evaluate e for each combination of possible values of vars, drown from respective domains
evalForEach :: (Monad m, Functor m) => [Id] -> [Domain] -> Execution m Bool
evalForEach [] [] = unValueBool <$> eval e
evalForEach (var : vars) (dom : doms) = anyM (fixOne vars doms var) dom
-- | Fix the value of var to val, then evaluate e for each combination of values for the rest of vars
fixOne :: (Monad m, Functor m) => [Id] -> [Domain] -> Id -> Value -> Execution m Bool
fixOne vars doms var val = do
resetVar memLocals var val
evalForEach vars doms
varNames = map fst vars
{- Statements -}
-- | Execute a basic statement
-- (no jump, if or while statements allowed)
exec :: (Monad m, Functor m) => Statement -> Execution m ()
exec stmt = case node stmt of
Predicate specClause -> execPredicate specClause (position stmt)
Havoc ids -> execHavoc ids (position stmt)
Assign lhss rhss -> execAssign lhss rhss
Call lhss name args -> execCall name lhss args (position stmt)
CallForall name args -> return ()
>> collectGarbage
execPredicate specClause pos = do
b <- eval $ specExpr specClause
case b of
BoolValue True -> return ()
BoolValue False -> throwRuntimeFailure (SpecViolation specClause) pos
execHavoc names pos = do
mapM_ havoc names
where
havoc name = do
tc <- use envTypeContext
let t = exprType tc . gen . Var $ name
definedValue <- checkNameDefinitions name t pos
case definedValue of
Just val -> do
resetAnyVar name val
checkNameConstraints name pos
Nothing -> do
chosenValue <- generateValue t pos
resetAnyVar name chosenValue
checkNameConstraints name pos
execAssign lhss rhss = do
rVals <- mapM eval rhss'
zipWithM_ resetAnyVar lhss' rVals
where
lhss' = map fst (zipWith simplifyLeft lhss rhss)
rhss' = map snd (zipWith simplifyLeft lhss rhss)
simplifyLeft (id, []) rhs = (id, rhs)
simplifyLeft (id, argss) rhs = (id, mapUpdate (gen $ Var id) argss rhs)
mapUpdate e [args] rhs = gen $ MapUpdate e args rhs
mapUpdate e (args1 : argss) rhs = gen $ MapUpdate e args1 (mapUpdate (gen $ MapSelection e args1) argss rhs)
execCall name lhss args pos = do
sig <- procSig name <$> use envTypeContext
execCallBySig sig lhss args pos
execCallBySig sig lhss args pos = do
defs <- gets $ lookupProcedure (psigName sig)
tc <- use envTypeContext
(sig', def) <- selectDef tc defs
let lhssExpr = map (attachPos (ctxPos tc) . Var) lhss
retsV <- execProcedure sig' def args lhssExpr `catchError` addFrame
zipWithM_ resetAnyVar lhss retsV
where
selectDef tc [] = return (assumePostconditions sig, dummyDef tc)
selectDef tc defs = do
i <- generate (`genIndex` length defs)
return (sig, defs !! i)
params = psigParams sig
paramConstraints tc = M.filterWithKey (\k _ -> k `elem` map itwId params) $ foldr asUnion M.empty $ map (extractConstraints tc . itwWhere) params
-- For procedures with no implementation: dummy definition that just havocs all modifiable globals
dummyDef tc = PDef {
pdefIns = map itwId (psigArgs sig),
pdefOuts = map itwId (psigRets sig),
pdefParamsRenamed = False,
pdefBody = ([], (M.fromList . toBasicBlocks . singletonBlock . gen . Havoc . psigModifies) sig),
pdefConstraints = paramConstraints tc,
pdefPos = noPos
}
addFrame err = addStackFrame (StackFrame pos (psigName sig)) err
-- | Execute program consisting of blocks starting from the block labeled label.
-- Return the location of the exit point.
execBlock :: (Monad m, Functor m) => Map Id [Statement] -> Id -> Execution m SourcePos
execBlock blocks label = let
block = blocks ! label
statements = init block
in do
mapM exec statements
case last block of
Pos pos Return -> return pos
Pos _ (Goto lbs) -> tryOneOf blocks lbs
-- | tryOneOf blocks labels: try executing blocks starting with each of labels,
-- until we find one that does not result in an assumption violation
tryOneOf :: (Monad m, Functor m) => Map Id [Statement] -> [Id] -> Execution m SourcePos
tryOneOf blocks (l : lbs) = execBlock blocks l `catchError` retry
where
retry err
| failureKind err == Unreachable && not (null lbs) = tryOneOf blocks lbs
| otherwise = throwError err
-- | 'execProcedure' @sig def args lhss@ :
-- Execute definition @def@ of procedure @sig@ with actual arguments @args@ and call left-hand sides @lhss@
execProcedure :: (Monad m, Functor m) => PSig -> PDef -> [Expression] -> [Expression] -> Execution m [Value]
execProcedure sig def args lhss = let
ins = pdefIns def
outs = pdefOuts def
blocks = snd (pdefBody def)
localConstraints = pdefConstraints def
exitPoint pos = if pos == noPos
then pdefPos def -- Fall off the procedure body: take the procedure definition location
else pos -- A return statement inside the body
execBody = do
checkPreconditions sig def
pos <- exitPoint <$> execBlock blocks startLabel
checkPostonditions sig def pos
mapM (eval . attachPos (pdefPos def) . Var) outs
in do
argsV <- mapM eval args
mem <- saveOld
executeLocally (enterProcedure sig def args lhss) (pdefLocals def) ins argsV localConstraints execBody `finally` restoreOld mem
{- Specs -}
-- | Assert preconditions of definition def of procedure sig
checkPreconditions sig def = mapM_ (exec . attachPos (pdefPos def) . Predicate . subst sig) (psigRequires sig)
where
subst sig (SpecClause t f e) = SpecClause t f (paramSubst sig def e)
-- | Assert postconditions of definition def of procedure sig at exitPoint
checkPostonditions sig def exitPoint = mapM_ (exec . attachPos exitPoint . Predicate . subst sig) (psigEnsures sig)
where
subst sig (SpecClause t f e) = SpecClause t f (paramSubst sig def e)
-- | 'wellDefined' @val@ : throw an exception if @val@ is under construction
wellDefined (CustomValue t n) | t == ucTypeName = throwInternalException $ UnderConstruction n
wellDefined val = return val
-- | 'checkDefinitions' @typeGuard evalLocally myCode defs pos@ : return the result of the first applicable definition from @defs@;
-- if none are applicable return 'Nothing',
-- unless an under construction value different from @myCode@ has been evaluated, in which case rethrow the UnderConstruction exception;
-- use @typeGuard tv formalTypes@ to decide if a definition with type variables @tv@ and types of formals @formalTypes@ is applicable to the current invocation;
-- use @evalLocally formals@ to evaluate expressions inside a definition with arguments @formals@;
-- @pos@ is the position of the definition invocation
checkDefinitions :: (Monad m, Functor m) => ([Id] -> [Type] -> Bool) -> ([Id] -> Expression -> Execution m Value) -> Int -> [FDef] -> SourcePos -> Execution m (Maybe Value)
checkDefinitions typeGuard evalLocally myCode defs pos = checkDefinitions' typeGuard evalLocally myCode Nothing defs pos
checkDefinitions' _ _ _ Nothing [] _ = return Nothing
checkDefinitions' _ _ _ (Just code) [] _ = throwInternalException (UnderConstruction code)
checkDefinitions' typeGuard evalLocally myCode mCode (FDef name tv formals guard body : defs) pos = tryDefinitions `catchError` ucHandler
where
tryDefinitions = do
mVal <- applyDefinition (evalLocally (map fst formals)) guard body
case mVal of
Just val -> return mVal
Nothing -> checkDefinitions' typeGuard evalLocally myCode mCode defs pos
ucHandler err = case rtfSource err of
InternalException (UnderConstruction code) -> if code == myCode
then checkDefinitions' typeGuard evalLocally myCode mCode defs pos
else checkDefinitions' typeGuard evalLocally myCode (Just code) defs pos
_ -> throwError err
applyDefinition evaluation guard body = if typeGuard tv (map snd formals)
then do
applicable <- case guard of
Pos _ TT -> return $ BoolValue True -- optimization for trivial guards
_ -> evaluation guard `catchError` addFrame
case applicable of
BoolValue False -> return Nothing
BoolValue True -> (Just <$> evaluation body) `catchError` addFrame
else return Nothing
addFrame = addStackFrame (StackFrame pos name)
-- | 'checkNameDefinitions' @name t pos@ : return a value for @name@ of type @t@ mentioned at @pos@, if there is an applicable definition
checkNameDefinitions :: (Monad m, Functor m) => Id -> Type -> SourcePos -> Execution m (Maybe Value)
checkNameDefinitions name t pos = do
n <- gets $ lookupCustomCount ucTypeName
resetAnyVar name $ CustomValue ucTypeName n
modify $ setCustomCount ucTypeName (n + 1)
defs <- fst <$> gets (lookupNameConstraints name)
let simpleDefs = [simpleDef | simpleDef <- defs, null $ fdefArgs simpleDef] -- Ignore forall-definition, they will be attached to the map value by checkNameConstraints
checkDefinitions (\_ _ -> True) (\_ -> eval) n simpleDefs pos `finally` cleanup n
where
cleanup n = do
forgetAnyVar name
modify $ setCustomCount ucTypeName n
-- | 'checkMapDefinitions' @r t args actuals pos@ : return a value at index @actuals@
-- in the map of type @t@ referenced by @r@ mentioned at @pos@, if there is an applicable definition
checkMapDefinitions :: (Monad m, Functor m) => Ref -> Type -> [Expression] -> [Value] -> SourcePos -> Execution m (Maybe Value)
checkMapDefinitions r t args actuals pos = do
n <- gets $ lookupCustomCount ucTypeName
setMapValue r actuals $ CustomValue ucTypeName n
modify $ setCustomCount ucTypeName (n + 1)
defs <- fst <$> gets (lookupMapConstraints r)
tc <- use envTypeContext
let argTypes = map (exprType tc) args
checkDefinitions (typeGuard argTypes) evalLocally n defs pos `finally` cleanup n
where
sig = fsigFromType t
typeGuard argTypes tv formalTypes = isJust $ unifier tv formalTypes argTypes
evalLocally formals expr = if null formals
then eval expr
else executeLocally (enterFunction sig formals args) formals formals actuals M.empty (eval expr)
cleanup n = do
forgetMapValue r actuals
modify $ setCustomCount ucTypeName n
-- | 'applyConstraint' @name evaluation guard body pos@ :
-- check for an entity @name@ that @guard@ ==> @body@, using @evaluation@ to evaluate both @guard@ and @body@;
-- (@pos@ is the position of the constraint invocation)
applyConstraint name evaluation guard body pos = do
applicable <- case guard of
Pos _ TT -> return $ BoolValue True -- optimization for trivial guards
_ -> evaluation guard `catchError` addFrame
case applicable of
BoolValue True -> do
satisfied <- evaluation body `catchError` addFrame
case satisfied of
BoolValue True -> return ()
BoolValue False -> throwRuntimeFailure (SpecViolation $ SpecClause Axiom True body) pos
BoolValue False -> return ()
where
addFrame = addStackFrame (StackFrame pos name)
-- | 'checkNameConstraints' @name pos@: assume all constraints of entity @name@ mentioned at @pos@;
-- is @name@ is of map type, attach all its forall-definitions and forall-contraints to the corresponding reference
checkNameConstraints name pos = do
(defs, constraints) <- gets $ lookupNameConstraints name
mapM_ checkConstraint constraints
mapM_ attachDefinition defs
where
checkConstraint (FDef _ [] [] guard body) = applyConstraint name eval guard body pos -- Simple constraint: assume it
checkConstraint constr = do -- Forall-constraint: attach to the map value
Reference r <- evalVar name pos
modify $ addMapConstraint r constr
attachDefinition (FDef _ [] [] _ _) = return () -- Simple definition: ignore
attachDefinition def = do -- Forall definition: attach to the map value
Reference r <- evalVar name pos
modify $ addMapDefinition r def
-- | 'checkMapConstraints' @r t args actuals pos@ : assume all constraints for the value at index @actuals@
-- in the map of type @t@ referenced by @r@ mentioned at @pos@
checkMapConstraints r t args actuals pos = do
constraints <- snd <$> gets (lookupMapConstraints r)
tc <- use envTypeContext
let argTypes = map (exprType tc) args
let typeGuard tv formalTypes = isJust $ unifier tv formalTypes argTypes
mapM_ (checkConstraint typeGuard) constraints
where
checkConstraint typeGuard (FDef name tv formals guard body) = if typeGuard tv (map snd formals)
then applyConstraint name (evalLocally (map fst formals)) guard body pos
else return ()
evalLocally formalNames expr = do
let sig = fsigFromType t
executeLocally (enterFunction sig formalNames args) formalNames formalNames actuals M.empty (eval expr)
{- Preprocessing -}
-- | Collect procedure implementations, and constant/function/global variable constraints
preprocess :: (Monad m, Functor m) => Program -> SafeExecution m ()
preprocess (Program decls) = mapM_ processDecl decls
where
processDecl decl = case node decl of
FunctionDecl name _ args _ mBody -> processFunction name args mBody
ProcedureDecl name _ args rets _ (Just body) -> processProcedureBody name (position decl) (map noWhere args) (map noWhere rets) body
ImplementationDecl name _ args rets bodies -> mapM_ (processProcedureBody name (position decl) args rets) bodies
AxiomDecl expr -> processAxiom expr
VarDecl vars -> mapM_ processAxiom (map itwWhere vars)
_ -> return ()
processFunction name args mBody = do
sig <- funSig name <$> use envTypeContext
envTypeContext %= \tc -> tc { ctxConstants = M.insert (functionConst name) (fsigType sig) (ctxConstants tc) }
case mBody of
Nothing -> return ()
Just body -> modify $ addGlobalDefinition (functionConst name) (FDef name (fsigTypeVars sig) formals (conjunction []) body)
where
formals = over (mapped._1) formalName args
formalName Nothing = dummyFArg
formalName (Just n) = n
processProcedureBody name pos args rets body = do
tc <- use envTypeContext
let params = psigParams $ procSig name tc
let paramsRenamed = map itwId params /= (argNames ++ retNames)
let flatBody = (map (mapItwType (resolve tc)) (concat $ fst body), M.fromList (toBasicBlocks $ snd body))
let allLocals = params ++ fst flatBody
let localConstraints = M.filterWithKey (\k _ -> k `elem` map itwId allLocals) $ foldr asUnion M.empty $ map (extractConstraints tc . itwWhere) allLocals
modify $ addProcedureImpl name (PDef argNames retNames paramsRenamed flatBody localConstraints pos)
where
argNames = map fst args
retNames = map fst rets
processAxiom expr = do
tc <- use envTypeContext
envConstraints.amGlobals %= (`asUnion` extractConstraints tc expr)
{- Constant and function constraints -}
-- | 'extractConstraints' @bExpr@ : extract definitions and constraints from @bExpr@
extractConstraints :: Context -> Expression -> AbstractStore
extractConstraints tc bExpr = extractConstraints' tc [] (negationNF bExpr)
extractConstraints' :: Context -> [Expression] -> Expression -> AbstractStore
extractConstraints' tc guards bExpr = case (node bExpr) of
Quantified Forall tv vars bExpr' -> extractConstraints' (enterQuantified tv vars tc) guards bExpr'
Quantified Exists _ _ _ -> M.empty
BinaryExpression And bExpr1 bExpr2 -> let
constraints1 = extractConstraints' tc guards bExpr1
constraints2 = extractConstraints' tc guards bExpr2
in constraints1 `asUnion` constraints2
BinaryExpression Or bExpr1 bExpr2 -> let
constraints1 = extractConstraints' tc ((negationNF $ enot bExpr1) : guards) bExpr2
constraints2 = extractConstraints' tc ((negationNF $ enot bExpr2) : guards) bExpr1
in constraints1 `asUnion` constraints2
BinaryExpression Eq expr1 expr2 -> let
defs1 = extractDefsAtomic expr1 expr2
defs2 = extractDefsAtomic expr2 expr1
constraints = extractConstraintsAtomic
in foldr1 asUnion [defs1, defs2, constraints]
_ -> extractConstraintsAtomic
where
fvExpr = freeVars bExpr
fvGuards = concatMap freeVars guards
allFV = fvExpr ++ fvGuards
tv = ctxTypeVars tc
vars = M.toList $ ctxIns tc
usedVars = [(v, t) | (v, t) <- vars, v `elem` allFV]
extractDefsAtomic lhs rhs = case node lhs of
Var name -> addDefFor name [] rhs
MapSelection (Pos _ (Var name)) args -> addDefFor name args rhs
Application name args -> addDefFor (functionConst name) args rhs
_ -> M.empty
addDefFor name args rhs = let
argTypes = map (exprType tc) args
(formals, argGuards) = unzip $ extractArgs (map fst usedVars) args
allGuards = concat argGuards ++ guards
extraVars = [(v, t) | (v, t) <- usedVars, v `notElem` formals]
in if length formals == length args && null extraVars -- Only possible if all arguments are simple and there are no extra variables
then M.singleton name ([FDef name tv (zip formals argTypes) (conjunction allGuards) rhs], [])
else M.empty
extractConstraintsAtomic = case usedVars of -- This is a compromise: quantified expressions constrain names they mention of any arity but zero (ToDo: think about it)
[] -> foldr asUnion M.empty $ map addSimpleConstraintFor fvExpr
_ -> foldr asUnion M.empty $ map addForallConstraintFor (freeSelections bExpr ++ over (mapped._1) functionConst (applications bExpr))
addSimpleConstraintFor name = M.singleton name ([], [FDef name [] [] (conjunction guards) bExpr])
addForallConstraintFor (name, args) = let
argTypes = map (exprType tc) args
(formals, argGuards) = unzip $ extractArgs (map fst usedVars) args
allArgGuards = concat argGuards
extraVars = [(v, t) | (v, t) <- usedVars, v `notElem` formals]
constraint = if null extraVars
then conjunction guards |=>| bExpr
else attachPos (position bExpr) $ Quantified Forall tv extraVars (conjunction guards |=>| bExpr) -- outer guards are inserted into the body, because they might contain extraVars
in if length formals == length args -- Only possible if all arguments are simple
then M.singleton name ([], [FDef name tv (zip formals argTypes) (conjunction allArgGuards) constraint])
else M.empty
-- | 'extractArgs' @vars args@: extract simple arguments from @args@;
-- an argument is simple if it is either one of variables in @vars@ or does not contain any of @vars@;
-- in the latter case the argument is represented as a fresh name and a constraint
extractArgs :: [Id] -> [Expression] -> [(Id, [Expression])]
extractArgs vars args = foldl extractArg [] (zip args [0..])
where
extractArg res ((Pos p e), i) = let
x = freshArgName i
xExpr = attachPos p $ Var x
in res ++
case e of
Var arg -> if arg `elem` vars
then if arg `elem` map fst res
then [(x, [xExpr |=| Pos p e])] -- Bound variable that already occurred: use fresh variable as formal, add equality guard
else [(arg, [])] -- New bound variable: use variable name as formal, no additional guards
else [(x, [xExpr |=| Pos p e])] -- Constant: use fresh variable as formal, add equality guard
_ -> if null $ freeVars (Pos p e) `intersect` nonfixedBV
then [(x, [xExpr |=| Pos p e])] -- Expression where all bound variables are already fixed: use fresh variable as formal, add equality guard
else [] -- Expression involving non-fixed bound variables: not a simple argument, omit
freshArgName i = nonIdChar : show i
varArgs = [v | (Pos p (Var v)) <- args]
nonfixedBV = vars \\ varArgs
{- Quantification -}
-- | Sets of interval constraints on integer variables
type IntervalConstraints = Map Id Interval
-- | The set of domains for each variable in vars, outside which boolean expression boolExpr is always false.
-- Fails if any of the domains are infinite or cannot be found.
domains :: (Monad m, Functor m) => Expression -> [Id] -> Execution m [Domain]
domains boolExpr vars = do
initC <- foldM initConstraints M.empty vars
finalC <- inferConstraints boolExpr initC
forM vars (domain finalC)
where
initConstraints c var = do
tc <- use envTypeContext
qbound <- use envQBound
case M.lookup var (allVars tc) of
Just BoolType -> return c
Just (MapType _ _ _) -> throwRuntimeFailure (UnsupportedConstruct "quantification over a map") (position boolExpr)
Just t -> return $ M.insert var (defaultDomain qbound t) c
defaultDomain qbound t = case qbound of
Nothing -> top
Just n -> let
(lower, upper) = case t of
IntType -> intInterval n
IdType _ _ -> natInterval n
in Interval (Finite lower) (Finite upper)
domain c var = do
tc <- use envTypeContext
case M.lookup var (allVars tc) of
Just BoolType -> return $ map BoolValue [True, False]
Just t -> do
case c ! var of
int | isBottom int -> return []
Interval (Finite l) (Finite u) -> return $ map (valueFromInteger t) [l..u]
int -> throwRuntimeFailure (InfiniteDomain var int) (position boolExpr)
-- | Starting from initial constraints, refine them with the information from boolExpr,
-- until fixpoint is reached or the domain for one of the variables is empty.
-- This function terminates because the interval for each variable can only become smaller with each iteration.
inferConstraints :: (Monad m, Functor m) => Expression -> IntervalConstraints -> Execution m IntervalConstraints
inferConstraints boolExpr constraints = do
constraints' <- foldM refineVar constraints (M.keys constraints)
if bot `elem` M.elems constraints'
then return $ M.map (const bot) constraints' -- if boolExpr does not have a satisfying assignment to one variable, then it has none to all variables
else if constraints == constraints'
then return constraints' -- if a fixpoint is reached, return it
else inferConstraints boolExpr constraints' -- otherwise do another iteration
where
refineVar :: (Monad m, Functor m) => IntervalConstraints -> Id -> Execution m IntervalConstraints
refineVar c id = do
int <- inferInterval boolExpr c id
return $ M.insert id (meet (c ! id) int) c
-- | Infer an interval for variable x, outside which boolean expression booExpr is always false,
-- assuming all other quantified variables satisfy constraints;
-- boolExpr has to be in negation-prenex normal form.
inferInterval :: (Monad m, Functor m) => Expression -> IntervalConstraints -> Id -> Execution m Interval
inferInterval boolExpr constraints x = (case node boolExpr of
FF -> return bot
BinaryExpression And be1 be2 -> liftM2 meet (inferInterval be1 constraints x) (inferInterval be2 constraints x)
BinaryExpression Or be1 be2 -> liftM2 join (inferInterval be1 constraints x) (inferInterval be2 constraints x)
BinaryExpression Eq ae1 ae2 -> do
(a, b) <- toLinearForm (ae1 |-| ae2) constraints x
if 0 <: a && 0 <: b
then return top
else return $ -b // a
BinaryExpression Leq ae1 ae2 -> do
(a, b) <- toLinearForm (ae1 |-| ae2) constraints x
if isBottom a || isBottom b
then return bot
else if 0 <: a && not (isBottom (meet b nonPositives))
then return top
else return $ join (lessEqual (-b // meet a positives)) (greaterEqual (-b // meet a negatives))
BinaryExpression Ls ae1 ae2 -> inferInterval (ae1 |<=| (ae2 |-| num 1)) constraints x
BinaryExpression Geq ae1 ae2 -> inferInterval (ae2 |<=| ae1) constraints x
BinaryExpression Gt ae1 ae2 -> inferInterval (ae2 |<=| (ae1 |-| num 1)) constraints x
-- Quantifier can only occur here if it is alternating with the enclosing one, hence no domain can be inferred
_ -> return top
) `catchError` handleNotLinear
where
lessEqual int | isBottom int = bot
| otherwise = Interval NegInf (upper int)
greaterEqual int | isBottom int = bot
| otherwise = Interval (lower int) Inf
handleNotLinear err = case rtfSource err of
InternalException NotLinear -> return top
_ -> throwError err
-- | Linear form (A, B) represents a set of expressions a*x + b, where a in A and b in B
type LinearForm = (Interval, Interval)
-- | If possible, convert arithmetic expression aExpr into a linear form over variable x,
-- assuming all other quantified variables satisfy constraints.
toLinearForm :: (Monad m, Functor m) => Expression -> IntervalConstraints -> Id -> Execution m LinearForm
toLinearForm aExpr constraints x = case node aExpr of
Numeral n -> return (0, fromInteger n)
Var y -> if x == y
then return (1, 0)
else case M.lookup y constraints of
Just int -> return (0, int)
Nothing -> const aExpr
Application name args -> if null $ M.keys constraints `intersect` freeVars aExpr
then const aExpr
else throwInternalException NotLinear
MapSelection m args -> if null $ M.keys constraints `intersect` freeVars aExpr
then const aExpr
else throwInternalException NotLinear
Old e -> old $ toLinearForm e constraints x
UnaryExpression Neg e -> do
(a, b) <- toLinearForm e constraints x
return (-a, -b)
BinaryExpression op e1 e2 -> do
left <- toLinearForm e1 constraints x
right <- toLinearForm e2 constraints x
combineBinOp op left right
where
const e = do
v <- eval e
case v of
IntValue n -> return (0, fromInteger n)
combineBinOp Plus (a1, b1) (a2, b2) = return (a1 + a2, b1 + b2)
combineBinOp Minus (a1, b1) (a2, b2) = return (a1 - a2, b1 - b2)
combineBinOp Times (a, b) (0, k) = return (k * a, k * b)
combineBinOp Times (0, k) (a, b) = return (k * a, k * b)
combineBinOp _ _ _ = throwInternalException NotLinear
{- Map equality -}
-- | 'evalEquality' @v1 v2@ : Evaluate @v1 == v2@
evalEquality :: (Monad m, Functor m) => Value -> Value -> Execution m Value
evalEquality v1 v2 = do
h <- use $ envMemory.memHeap
case objectEq h v1 v2 of
Just b -> return $ BoolValue b
Nothing -> decideEquality v1 v2 -- No evidence yet if two maps are equal or not, make a non-deterministic choice
where
decideEquality (Reference r1) (Reference r2) = do
h <- use $ envMemory.memHeap
let (s1, vals1) = flattenMap h r1
let (s2, vals2) = flattenMap h r2
mustEqual <- generate genBool -- Decide if maps should be considered equal right away
if mustEqual
then do makeEq v1 v2; return $ BoolValue True -- Make the maps equal and return True
else if s1 == s2 -- Otherwise: if the maps come from the same source
then decideOverrideEquality r1 vals1 r2 vals2 -- Then the difference must be in overrides
else if mustAgree h vals1 vals2 -- Otherwise: if the difference cannot be in overrides
then do makeSourceNeq s1 s2; return $ BoolValue False -- Then make the sources incompatible and return False
else do -- Otherwise we can freely choose if the difference is in the source or in the overrides
compareOverrides <- generate genBool -- Make a choice
if compareOverrides
then decideOverrideEquality r1 vals1 r2 vals2 -- decide equality based on overrides
else do makeSourceNeq s1 s2; return $ BoolValue False -- otherwise make the sources incompatible and return False
decideOverrideEquality r1 vals1 r2 vals2 =
let diff = if hasMapValues $ vals1 `M.intersection` vals2 -- If there are maps stored at common indexes
then vals1 `M.union` vals2 -- then even values at a common index might be different
else (vals2 `M.difference` vals1) `M.union` (vals1 `M.difference` vals2) -- otherwise only values at non-shared indexes might be different
in do
(i, val) <- (`M.elemAt` diff) <$> generate (`genIndex` M.size diff) -- Choose an index at which the values might be different
val1 <- lookupStored r1 i val
val2 <- lookupStored r2 i val
BoolValue answer <- evalEquality val1 val2
when answer $ makeEq v1 v2
return $ BoolValue answer
hasMapValues m
| M.null m = False
| otherwise = case M.findMin m of
(_, Reference _) -> True
_ -> False
lookupStored r i template = do
h <- use $ envMemory.memHeap
let (s, vals) = flattenMap h r
case M.lookup i vals of
Just v -> return v
Nothing -> do
v <- generateValueLike template
setMapValue s i v
return v
makeSourceNeq s1 s2 = do
setMapValue s1 [special s1, special s2] (special s1)
setMapValue s2 [special s1, special s2] (special s2)
special r = CustomValue refIdTypeName $ fromIntegral r
-- | Ensure that two compatible values are equal
makeEq :: (Monad m, Functor m) => Value -> Value -> Execution m ()
makeEq (Reference r1) (Reference r2) = do
h <- use $ envMemory.memHeap
let (s1, vals1) = flattenMap h r1
let (s2, vals2) = flattenMap h r2
zipWithM_ makeEq (M.elems $ vals1 `M.intersection` vals2) (M.elems $ vals2 `M.intersection` vals1) -- Enforce that the values at shared indexes are equal
if s1 == s2
then do -- Same source; compatible, but nonequal overrides
mapM_ (uncurry $ setMapValue s1) (M.toList $ vals2 `M.difference` vals1) -- Store values only defined in r2 in the source
mapM_ (uncurry $ setMapValue s1) (M.toList $ vals1 `M.difference` vals2) -- Store values only defined in r1 in the source
else do -- Different sources
Reference newSource <- allocate . MapValue . Source $ vals1 `M.union` vals2
mapM_ decRefCountValue (M.elems (vals2 `M.intersection` vals1)) -- Take care of references from vals2 that are no longer used
derive r1 newSource
derive r2 newSource
mergeConstraints s1 s2 newSource
where
derive r newSource = do
deriveBaseOf r newSource M.empty
envMemory.memHeap %= update r (MapValue (Derived newSource M.empty))
envMemory.memHeap %= incRefCount newSource
deriveBaseOf r newSource diffR = do
MapValue repr <- readHeap r
case repr of
Source _ -> return ()
Derived base override -> do
let diffBase = override `M.union` diffR -- The difference between base and newSource
h <- use $ envMemory.memHeap
let vals = mapValues h base
deriveBaseOf base newSource diffBase
newVals <- foldM addMissing (vals `M.intersection` diffBase) (M.toList $ diffBase `M.difference` vals) -- Choose arbitrary values for all keys in diffBase that are not defined for base
envMemory.memHeap %= update base (MapValue (Derived newSource newVals))
envMemory.memHeap %= incRefCount newSource
envMemory.memHeap %= decRefCount base
addMissing vals (key, oldVal) = do
newVal <- generateValueLike oldVal
incRefCountValue newVal
return $ M.insert key newVal vals
mergeConstraints s1 s2 newSource = do
(defs1, constraints1) <- gets $ lookupMapConstraints s1
(defs2, constraints2) <- gets $ lookupMapConstraints s2
envConstraints.amHeap %= M.insert newSource (defs1 ++ defs2, constraints1 ++ constraints2)
makeEq (MapValue _) (MapValue _) = internalError "Attempt to call makeEq on maps directly"
makeEq _ _ = return ()