A5: Program Analysis

For this assignment you will write a program analysis for Fb.

  1. Your analysis should closely follow Chapter 2 of the PLII book, which serves as the specification.
  2. For this assignment you will again write all your code in the file Fb/fbinterp.ml, constructing an aeval function there which will in turn invoke your abstract interpreter.
  3. Here is a possible abstract-expression type. Feel free to use whatever type you want. 
    type callsite = int
type context = callsite list

(* abstract booleans *)
type abool = T | F

(* abstract ints *)
type aint = N | Z | P

type aexpr =
  | AVar of ident | AFunction of ident * aexpr | AAppl of callsite * aexpr * aexpr
  | ALet of ident * aexpr * aexpr | ALetRec of ident * ident * aexpr * aexpr
  | APlus of aexpr * aexpr | AMinus of aexpr * aexpr | AEqual of aexpr * aexpr
  | AAnd of aexpr * aexpr| AOr of aexpr * aexpr | ANot of aexpr
  | AIf of aexpr * aexpr * aexpr | AInt of aint | ABool of abool
  | AClosure of aexpr * context
  4. There are several changes that the analysis must make to the interpreter of the previous assignment:
    1. The context must be made some fixed finite length. Please either include a ref variable k which contains the maximum length of the context stack, or otherwise specifiy some other mechanism in comments.
    2. The integers need to be finitized to just - 0, and + values. As in the previous assignments we suggest a function expr_to_aexpr which can map initial Fb expr expressions to these abstract expressions. The interpreter operations then must work over these abstract values.
    3. The store is now not just a map from contexts to environments, due to non-determinism it must be a mapping from contexts to sets of environments. You can use the OCaml Set module or you can just implement sets as OCaml lists.
    4. Here is the hardest part: there may be more than one value to any computation, including intermediate results. For example (+) = (+) returns both true and false, and if this is the condition on an if then both branches must be taken and the final result the union of those two results (which themselves could be sets of more than one result). Any binary operator also returns a set on either side so the product of possibilities must be evaluated.
    5. Related to this, any lookup of a variable may also return multiple values all of which must be evaluated.
    6. Lastly, all visited states must be checkpointed in a set -- this interpreter can get in a loop, but since the possible states are finite we can cache them and abort any eval which is visiitng a state already visited (just return an empty set of values).
  5. If you had big problems on the previous interpreter assignment we can give you some "answers" to that to help you catch up. Just ask.
  6. Please make sure your aeval output is readable by some mechanism. If you use OCaml lists it will get printed out in the top loop which is good enough, but if you use the Map and Set modules you will need to write a pretty-printer. You will find this handy for debuging as well :-)

For this assignment submit ONLY the file fbinterp.ml with your interpreter code.