CSE230 Fa16 - Interpreter



Part 3: An Interpreter for WHILE

> {-@ LIQUID "--no-termination" @-}
> 
> module Interpreter (interpret) where
> 
> import           Prelude hiding (lookup)
> import qualified Data.Set as S

HINT: To do this problem, first go through this case study also included in your tarball as case-study-eval.lhs.

Next, you will revisit your interpreter for the WHILE language to ensure that execution never fails due to a use-before-definition error.

Programs in the language are simply values of the type

> data Statement =
>     Assign Variable Expression            -- x = e
>   | IfZ    Expression Statement Statement -- if (e) {s1} else {s2}
>   | WhileZ Expression Statement           -- while (e) {s}
>   | Sequence Statement Statement          -- s1; s2
>   | Skip                                  -- no-op

to simplify matters, we assume the branch statement IfZ e s1 s2 evaluates e and then executes s1 if the value of e equals 0 and otherwise evaluates s2.

Thus, the expressions are variables, constants or binary operators applied to sub-expressions

> data Expression =
>     Var Variable                        -- x
>   | Val Value                           -- v
>   | Op  Bop Expression Expression

and binary operators are simply two-ary functions

> data Bop =
>     Plus     -- (+)  :: Int  -> Int  -> Int
>   | Minus    -- (-)  :: Int  -> Int  -> Int

and variables and values are just:

> type Variable = String
> type Value    = Int

Store

We will represent the store i.e. the machine’s memory, as a list of Variable - Value pairs:

> type Store = [(Variable, Value)]
> 
> update :: Store -> Variable -> Value -> Store 
> update st x v = (x, v) : st
> 
> lookup :: Variable -> Store -> Value 
> lookup x ((y, v) : st)
>   | x == y         = v 
>   | otherwise      = lookup x st
> lookup x []        = impossible "variable not found"

Evaluation

We can now write a function that evaluates Statement in a Store to yield a new updated Store:

> evalS :: Store -> Statement -> Store
> 
> evalS st Skip             = st
> 
> evalS st (Assign x e )    = update st x v
>                             where
>                               v = evalE st e
> 
> evalS st (IfZ e s1 s2)    = if v == 0
>                               then evalS st s1
>                               else evalS st s2
>                             where
>                               v = evalE st e
> evalS st w@(WhileZ e s)   = if v == 0
>                               then evalS st (Sequence s w)
>                               else st
>                             where
>                               v = evalE st e
> 
> evalS st (Sequence s1 s2) = evalS (evalS st s1) s2

The above uses a helper that evaluates an Expression in a Store to get a Value:

> evalE :: Store -> Expression -> Value
> evalE st (Var x)      = lookup x st
> evalE _  (Val v)      = v
> evalE st (Op o e1 e2) = evalOp o (evalE st e1) (evalE st e2)
> 
> evalOp :: Bop -> Value -> Value -> Value
> evalOp Plus  i j = i + j
> evalOp Minus i j = i - j

GOAL: A Safe Evaluator

Our goal is to write an evaluator that never fails due to an undefined variable. This means, we must ensure that the evaluator is never called with malformed programs in which some variable is used-before-being-defined.

In particular, this corresponds to establishing that the call to impossible never happens at run time, by verifying that the below typechecks:

> {-@ impossible :: {v:String | false} -> a @-}
> impossible msg = error msg

Obviously it is possible to throw an exception if you run evalS with a bad statement. Your task is to complete the implementation of isSafe and add suitable refinement type specifications, such that you can prove that the following interpret function is safe:

> interpret :: Statement -> Maybe Store
> interpret s 
>   | isSafe s  = Just (evalS [] s)  -- `s` does not use any vars before definition 
>   | otherwise = Nothing            -- `s` may use some var before definition
> 
> {-@ inline isSafe @-}
> isSafe :: Statement -> Bool
> isSafe s = True -- TODO: replace with correct implementation

To implement isSafe you probably need to write a function that computes the Set of variables that are `read-before-definition" in aStatement(andExpression`):

> {-@ measure readS @-}
> readS :: Statement -> S.Set Variable
> readS (Assign x e)     = S.empty    -- TODO: replace with proper definition 
> readS (IfZ e s1 s2)    = S.empty    -- TODO: replace with proper definition
> readS (WhileZ e s)     = S.empty    -- TODO: replace with proper definition
> readS (Sequence s1 s2) = S.empty    -- TODO: replace with proper definition
> readS Skip             = S.empty    -- TODO: replace with proper definition
> 
> {-@ measure readE @-}
> readE :: Expression -> S.Set Variable   
> readE (Var x)          = S.empty    -- TODO: replace with proper definition
> readE (Val v)          = S.empty    -- TODO: replace with proper definition
> readE (Op o e1 e2)     = S.empty    -- TODO: replace with proper definition

Here are some example programs:

> 
> safeStatement1 = 
>     (Assign "X" (Val 5)) 
>     `Sequence` 
>     (Assign "Y" (Var "X"))
> 
> safeStatement2 = 
>      (IfZ (Val 0) 
>       (Assign "Z" (Val 1)) 
>       (Assign "Z" (Val 2)))
>      `Sequence`
>      (Assign "Y" (Var "Z"))
> 
> unsafeStatement1 = 
>     (Assign "X" (Val 5)) 
>     `Sequence` 
>     (Assign "Y" (Var "Z"))
> 
> unsafeStatement2 = 
>      (WhileZ (Val 0) (Assign "Z" (Val 1)))
>      `Sequence`
>      (Assign "Y" (Var "Z"))

When you are done

  1. liquid Interpreter.lhs should return SAFE.

  2. You should get the following behavior in ghci.

*Interpreter> interpret safeStatement1 
Just [("Y",5),("X",5)]
*Interpreter> interpret safeStatement2 
Just [("Y",1),("Z",1)]
*Interpreter> interpret unsafeStatement1 
Nothing
*Interpreter> interpret unsafeStatement2 
Nothing

Note that the second step is important, you could implement isSafe _ = False which just rejects every program, but that is not a very useful interpreter.