Solving text adventure games via symbolic execution

A couple weeks ago, I attended some of the FSCD talks that the time zone difference allowed. One of the satellite workshops of FSCD this year was the Workshop on Rewriting Techniques for Program Transformations and Evaluation, where Martin Lester presented a talk Program Transformations Enable Verification Tools to Solve Interactive Fiction Games.

Because I haven't been able to find slides or the paper itself online, let me summarize it with my own words here quickly. Back in the late seventies and early eighties, Scott Adams (unrelated to the Dilbert comic strip creator) was a prolific text adventure creator; the Digital Antiquarian has written about his games in length, but basically these were simplistic (and in my opinion, creatively quite weak) games published on very limited platforms, where they found a following. Martin Lester's talk was about taking an off-the-shelf open source interpreter for these interactive fiction games (ScottFree) and feeding it (and a given game data file's contents) to a compiler that turns it into an SMT problem, with the free variables corresponding to the user input. Then, if an SMT solver can find an assignment satisfying a winning end condition, that means we have found a possible transcript of user input that wins the given game.

This combination of semi-formal methods and interactive fiction, plus the fact that I wanted to play around with SMT solver-backed interpreters ever since the Rosette talk at last year's ICFP, meant that the pull of this topic was just irresistable nerd catnip for me. So I took a week of afternoon hacking time from working on my Clash book, and started writing a Scott Adams adventure game engine in Haskell, with the aim of doing something similar to Lester's work.

An SBV-based Scott Adams solver

And so now I'm here to tell you about how it went, basically a "poor man's Rosette". When I started this, I have never used SMT solvers and never even looked at SBV, so I am not claiming I became an expert in just a week. But I managed to bumble my way through to something that works well enough on a toy example, so... let's see.

Step one was to implement a bog-standard interpreter for these Scott Adams adventure games. I didn't implement every possible condition and instruction, just barely enough to get a non-trivial example from ScottKit working. My target was the fourth tutorial adventure; see if you can find a solution either by playing the game, or by reading the game script. Why specifically the fourth tutorial example? Well, the short answer is because that is what Lester used as his example in his talk.

Here is the Git commit of this implementation; as you can see, there is really nothing special in there. The game data is parsed using Attoparsec into a simple datatype representation, which is then executed in ReaderT WriterT State, with the Reader containing the static game data, the Writer the output messages, and the State the game state, which is mostly just the current locations of the various items the player can interact with:

data S = S
    { _currentRoom :: Int16
    , _needLook :: Bool
    , _itemLocations :: Array Int16 Int16
    , _endState :: Maybe Bool
    } deriving Show
makeLenses ''S

type Engine = ReaderT Game (WriterT [String] (State S))

The second step was to use SBV so that (mostly) the same interpreter can also be executed symbolically. This is the interesting part. It started with changing the Writer output and the State representation to use SBV's symbolic types, and then following the type errors:

data S = S
    { _currentRoom :: SInt16
    , _needLook :: SBool
    , _itemLocations :: Array Int16 SInt16
    , _endState :: SMaybe Bool
    } deriving (Show, Generic, Mergeable)

Arithmetic works out of the box because of the Num instances; because the Haskell Prelude's Eq and Ord typeclasses hardcode the result type to Bool, and we want symbolic SBool results instead, we have to replace e.g. (==) with (.==).

For the control structures, my idea was to write Mergeable instances for the MTL types. The definitions of these instances are very straightforward, and it allowed me to define symbolic versions of things like when or case with literal matches. The end result of all this is that we can write quite straightforward monadic code, just replacing some combinators with their symbolic counterpart. Here's an example of the code that runs a list of instruction codes in the context of their conditions; even without seeing any other definitions it should be fairly straightforward what it does:

execIf :: [SCondition] -> [SInstr] -> Engine SBool
execIf conds instrs = do
    (bs, args) <- partitionEithers <$> mapM evalCond conds
    let b = sAnd bs
    sWhen b $ exec args instrs
    return b

I decided to use concrete lists and arrays of symbolic values instead of symbolic arrays throughout the code. One interesting example of sticking to this approach is in the implementation of listing all items in the current room. The original concrete code looks like this:

let itemsHere =
        [ desc
        | (Item _ _ desc _, loc) <- zip (A.elems items) (A.elems itemLocs)
        , loc == here
        ]
unless (null itemsHere) $ do
    say "I can also see:"
    mapM_ (\desc -> say $ " * " <> desc) itemsHere

For the symbolic version, I had to get rid of the filtering (since loc .== here returns an SBool now), and instead, I create a concrete list of pairs of symbolic locations and concrete descriptions. By going over the full list, I can push all the symbolic ambiguity down to just the output:

let itemLocsWithDesc =
        [ (loc, desc)
        | (Item _ _ desc _, loc) <- zip (A.elems items) (A.elems itemLocs)
        ]
    anyHere = sAny ((.== here) . fst) itemLocssWithDesc
sWhen anyHere $ do
    say_ "I can also see:"
    forM_ itemLocsWithDesc $ \(loc, desc) ->
        sWhen (loc .== here) $ say $ literal $ " * " <> desc

By the way, as the above code shows, I kept the user-visible text messages in the symbolic version. This is completely superfluous for solving, but it allows using the symbolic interpreter with concrete values: since all input is concrete, we can safely assume that the symbolic output values are all constants. In practice, this means we recover the original interactively playable version from the SBV-based one simply by running inside SBV's Query monad and getValue'ing the concrete String output from the SStrings coming out of the WriterT. I wouldn't be surprised if this turns out to be a major drain on performance, but because my aim was mostly to just get it working, I never bothered checking. Besides, since noone looks at the output in solver mode, maybe Haskell's laziness ensures there's no overhead. I really don't know.

"Turning the crank" on a stateful symbolic computation

So at this point, we have a symbolic interpreter which we can feed user input line by line:

stepPlayer :: SInput -> Engine (SMaybe Bool)
stepPlayer (verb, noun) = do
    perform (verb, noun)
    finished

The question then is, how do we keep running this (and letting the state evolve) for more and more lines of symbolic input, until we get an sJust sTrue result (meaning the player has won the game)? My original idea was to let the user say how many steps to check, and then generate a full list of symbolic inputs up-front. I asked around on Stack Overflow for something better, and it was this very helpful answer that pointed me in the direction of the Query monad in the first place. With this incremental approach, I can feed it one line of symbolic input, check for satisfiability with the newly yielded constraints, and if there's no solution yet, keep this process going, letting the next stepPlayer call create additional constraints.

I've factored out the whole thing into the following nicely reusable function; this is also the reason I am using ReaderT WriterT State instead of RWS so I can peel away naturally into a State.

loopState :: (SymVal i) => (Int -> Query (SBV i)) -> s -> (SBV i -> State s SBool) -> Query ([i], s)
loopState genCmd s0 step = go 1 s0 []
  where
    go i s cmds = do
        io $ putStrLn $ "Searching at depth: " ++ show i

        cmd <- genCmd i
        let cmds' = cmds ++ [cmd]

        push 1
        let (finished, s') = runState (step cmd) s
        constrain finished
        cs <- checkSat

        case cs of
            Unk -> error $ "Solver said Unknown, depth: " ++ show i
            Unsat -> do
                pop 1
                go (i+1) s' cmds'
            Sat -> do
                cmds' <- mapM getValue cmds'      
                return (cmds', s')

SBV bugs discovered on the way

Because I'm a complete SBV noob, I was reluctant to attribute problems to SBV bugs first; I ended up with a ton of Stack Overflow questions. However, it turned out I do still have my Midas touch of finding bugs very quickly in anything I start playing around with; this time, it started with SBV generating invalid SMTLib output from my code. Although my initial report was basically just "this several hundred line project Just Doesn't Work", I managed to cut it down into more reasonable size. The SBV maintainers, especially Levent Erkök, have been very helpful with quick turnaround.

The other bug I found was symbolic arrays misbehaving; although I ended up not using either SFunArray nor SArray in the final version of ScottCheck, it is good to know that my silly project has somehow contributed, if just a little, to making SBV itself better.

The money shot

So, lots of words, but where's the meat? Well first off, my code itself is on GitHub, and could serve as a good introduction to someone wanting to start using SBV with a stateful computation. And second, here is a transcript of ScottCheck verifying that the tutorial game is solvable, with the Z3 backend; the timestamps are in minutes and seconds from the start, to give an idea of how later steps become slower because there's an exponential increase in all possible inputs leading up to it. The words may look truncated, but that's because the actual internal vocabulary of the game only uses three letter words; further letters from the user are discarded (so COIN parses as COI etc.).

00:00 Searching at depth: 1
00:00 Searching at depth: 2
00:00 Searching at depth: 3
00:00 Searching at depth: 4
00:00 Searching at depth: 5
00:01 Searching at depth: 6
00:01 Searching at depth: 7
00:02 Searching at depth: 8
00:05 Searching at depth: 9
00:11 Searching at depth: 10
00:24 Searching at depth: 11
00:45 Searching at depth: 12
01:24 Searching at depth: 13
02:38 Searching at depth: 14
03:35 Solution found:
03:35   1. GO WES
03:35   2. GET CRO
03:35   3. GO EAS
03:35   4. GO NOR
03:35   5. GET KEY
03:35   6. GO SOU
03:35   7. OPE DOO
03:35   8. GO DOO
03:35   9. GET COI
03:35  10. GO NOR
03:35  11. GO WES
03:35  12. GO NOR
03:35  13. DRO COI
03:35  14. SCO ANY