PL II

For this assignment you will write a symbolic interpreter for Fb.

• Your interpreter should closely follow Chapter 3 of the PLII book, which serves as the specification.
• For this assignment you will again write all your code in the file Fb/fbinterp.ml.
• Here is a possible symbolic-expression type. Feel free to use whatever type you want.

  type callsite = int
  type context = callsite list
  type sident = ident * context
  
  type sexpr =
    | SVar of sident | SFunction of ident * sexpr | SAppl of callsite * sexpr * sexpr
    | SLet of ident * sexpr * sexpr | SLetRec of ident * ident * sexpr * sexpr
    | SLetInput of ident * sexpr 
    | SPlus of sexpr * sexpr | SMinus of sexpr * sexpr | SEqual of sexpr * sexpr
    | SAnd of sexpr * sexpr| SOr of sexpr * sexpr | SNot of sexpr
    | SIf of sexpr * sexpr * sexpr | SInt of int | SBool of bool
  
  type phi =
    | VVar of sident | VFunction of ident * sexpr
    | VPlus of phi * phi | VMinus of phi * phi | VEqual of phi * phi
    | VInt of int | VBool of bool
    | VAnd of phi * phi| VOr of phi * phi | VNot of phi | VMap of sident * phi
  

• Recall from the book spec that we are reverting to our old substitution-based method but substituting variables for variables instead of values for variables; these new variables also use the call site stacks (contexts) C to freshen appropriately so we are also borrowing the contexts idea from the context-based interpreter (but, not the closures which make extracting formulae more difficult).
• Recall again from the spec that values may be things like 4 + 3, by default we are relying on the SMT solver to do all our atomic operations. The phi data type above is one possible type of values and formulae.
• The above grammar merges the value (v) and formula (phi) grammars of the spec, this is one possible approach which will have fewer coercions at the expense of some "type correctness". Feel free to do this your own way.
• For inputs my suggested data type uses a separate SLetInput constructor for let-input expressions; the expr_to_sexpr function can convert to those. You just need to follow the (input) rule to implement input.
• Special input variables i^n are created by the input rule, you can just use variables with a special symbol in them, e.g. SVar("i^1"), SVar("i^2"), ....
• The hardest part is running all possible if-then-else branch choices without getting stuck in an infinite regress. We sugest two approaches in the section below.
• Lastly you need to hook up the Z3 SMT solver to answer satisfiability questions. It is not all that hard to use and Shiwei has written a guide below to help you.

Trying all if branches

The "hard part" of a symbolic interpreter is that conditionals are non-deterministic since either branch could hold. If your interpreter just tried the two paths in series it could get stuck in an infinitely deep pit on the first one (for example, infinitely looping on factorial recursion case never to hit the base case) and miss the correct result in the second one. There are many solutions to this problem. We outline here an easy but inefficient one, and a more efficient one which is a bit harder. You get extra credit for implementing the latter.

First method: use an oracle and iterate on it

• Define the basic evaluation function to pick only ONE choice at each conditional, based on an oracle. One simple encoding of an oracle is a list of booleans; for example the list [true; true; false; true] means at the first conditional take the true branch, false at second, etc. If you are still computing when the list ends then some failure result is returned. This evaluator is deterministic, the oracle "solves" the nondeterminism problem.
• This basic evaluator will then be invoked many times; the symbolic evaluator just enumerates through all posssble lists of booleans of length 1,2,3, etc until computation terminates and the final formula phi is satisfiable according to Z3.
• The downside of this approach is if the list is too short we throw away all the (partial) progress we made and start over. The upside is it is a lot simpiler than trying to save that work; see method two for how the work can be saved.
• There is also a subtle corner case that a program could in theory loop without hitting any conditionals (e.g. on our favorite diverging lambda-expression); for this case some max-steps count is also needed. You can leave this issue til the end as it will almost never arise in realistic programs.

• Keep a queue of active evaluations in progress, and only do one step of computation and put any needed sub-computations on the back of the queue (at lower priority). At a conditional there will be two sub-computations queued up, one for each path.
• Since evaluations are pulled off a queue, recursive calls may pull a computation off the queue different than what the caller was waiting for. So, queued tasks should include both the expression to evaluate, and a callback function aka continuation to invoke on the value.
• At the top level the continuation should return the final result value and formula, as well as the queue of any evaluations not yet completed.
• The queue of evaluations should be implementable with a coroutine monad if you would like to try a monadic approach; see Xavier's notes and code.

Using Z3

1. Install z3 via opam pin z3 4.8.1 - you need to use this version due to bugs in the latest one
2. Set the z3 path via

   export LD_LIBRARY_PATH=`opam config var z3:lib`
   export DYLD_LIBRARY_PATH=`opam config var z3:lib`
   

3. To use the Z3 library when compiling change makefiles/interpreters.make line 31 to
   ocamlbuild -use-ocamlfind -use-menhir -I $(srcdir) -Is "$(interpreter_dirs)" -r $(BUILD_FLAGS) -pkg z3 $@
4. Here is an fbinterp.ml written by Shiwei which just does a simple test of Z3, start with this one to test your Z3 install and to get an idea of how the API works.
5. The full API docs are here: Z3 API
6. To run: make fb.byte && ./fb.byte
7. There is an obscure bug on Macs which may rear its ugly head for you. If you get an error like
   Error: Error on dynamically loaded library: /Users/scott/.opam/4.08.1/lib/z3/dllz3ml.so: dlopen(/Users/scott/.opam/4.08.1/lib/z3/dllz3ml.so, 10): Library not loaded: libz3.dylib
   on the make, then you may need to manually copy this library into the _build/ directory:
   cp /Users/scott/.opam/4.08.1/lib/z3/libz3.dylib _build/
   (the above paths are from my computer, replace with yours)
8. One last thing, to test your evaluator in the top loop, put #require "z3";; in the beginning of debugscript/fb.ml to enable Z3, OR use utop -require z3 when launching.

   Submission

   For this assignment submit ONLY the file fbinterp.ml with your symbolic interpreter code, we will test it with the one changed line in the makefile.