| 
  • If you are citizen of an European Union member nation, you may not use this service unless you are at least 16 years old.

  • You already know Dokkio is an AI-powered assistant to organize & manage your digital files & messages. Very soon, Dokkio will support Outlook as well as One Drive. Check it out today!

View
 

HW8

Page history last edited by Ras Bodik 13 years, 4 months ago

 

Homework 8: Static Types and Analysis

 

Due Monday Nov 29, 10pm.

 


Submission

Using your instructional account, submit three plain text files

  • variance.txt for the first question.
  • inference.txt for the second question.
  • andersen.txt for the last question.

 

Lecture 18: Nominal Type Systems

 

Question on Co/Contra Variance

 

New languages like C# (version >= 4.0) and Scala let the programmer choose the variance of generics. At the end of this homework, you will be able to impress your future co-workers by mastering the subtleties of research type systems that have just gone mainstream.

 

Read Lecture and Section notes for Lecture 18.  

 

Recommended further reading:

 

Here you can learn how to choose between co-variance and contra-variance in C# and Scala.

 

 

Subtyping

 

Let's recall the fundamental principle of subtyping: It is safe to declare a type T as a subtype of type U if you can substitute a value of type T wherever a value of type U is required. This is know as the Liskov Substitution Principle.

 

We give below definition of co/contra variance for a class parameterized by one generic type.

 

Co-variance

A is co-variant if A[T] is a subtype of A[U] when T is a subtype of U

 

Contra-variance

A is contra-variant if A[T] is a subtype of A[U] when U is a subtype of T

 

Invariance

A is invariant if A[T] is a subtype of A[U] when U = T

 

The Question

 

Consider the following two Java classes. They are parameterized by a type T (i.e., they use the generics construct) and provide a read and a write channel to the mysterious Outer-space cloud.

 

/* Provide a read-only access to the Outer-space cloud */
class InputChannel[T] {
    T read() = {...}
}

 

 

/* Provide a write-only access to the Outer-space cloud */
class OutputChannel[T] {
    void write(T x) = {...}
}

 

 

Which of Co/Contra-Variance makes subtypes of InputChannel[T] safe? 

  • Co-variant in T
  • Contra-variant in T
  • Both
  • None (i.e. Invariant in T)

 

Which of the following makes subtypes of  OutputChannel[T] safe?  

  • Co-variant in T
  • Contra-variant in T
  • Both
  • None (i.e. Invariant in T)

 

To justify your answer, your are required to submit a small program demonstrating why co/contra-variance is unsafe for InputChannel, and another example for OutputChannel. If you answered None, you must submit two examples. No -example is required if your answer Both.

 

 

Lecture 19: Unification-based Type Systems

 

Question on Type Inference

 

Part A

 

The goal of this question is to help you understand the reliability (how many bugs are caught) and usability (redability) of static unification-based and dynamic type systems). Please read carefully the following introduction to Haskell type inference (you only need to read from slide 26 on). Then answer the following questions:

 

Questions:

  1. When would the bug in the sort function be detected in a dynamically typed language (e.g., Python)?  Plausible answers include: compile time, run time on some inputs, run time on all inputs.  To answer the question, you may want to rewrite the Haskell sort function to Python and run it on a sample input.
  2. Compare the readability of the diagnostics message obtained from the Haskell type checker with that obtained on the Python program.  In your opinion, which of the two messages message makes it easier for the programmer to locate and fix the bug?  Justify your answer.

 

Part B

 

Consider the following 164 implementation of map:

def map (f, l) {
    if (l == {}) {
        l
    } else {
        x = head(l)
        xs = tail(l)
        cons(f(x), map(f,xs))
    }
}

 

 

Assume that you know the type of the following functions

cons[A](a,b) :  A -> List[A] -> List[A]
head[A](l)   :  List[A] -> A
tail[A](l)   :  List[A] -> List[A]

 

 

Questions:

  1. Write the type of map[A](f,l).
  2. Write a Prolog program, similar to the one in the lecture slides, capable of inferring  the type of map[A](f, l).  

    The program may need to include the facts obtained from the program (i.e., the map function) as well as rules that describe the language semantics (e.g., the semantics of assignment and equality, as they pertains to checking the legality of comparing, say, l with {} and the type inference caused by this comparison).

 

Hint: Why is the type of cons A -> List[A] -> List[A]? This means that cons is a function of two arguments (A and List[A]) and returns a List[A].  The type A -> List[A] -> List[A] actually says that cons is a function of one argument (A) that returns a function of the type List[A] -> List[A].  Why is this so?  If you care to know, have a look at currying: http://en.wikipedia.org/wiki/Currying.

 

Lecture 20  Static Flow Analysis (Andersen's Analysis)

 

Consider this Java program from Lecture 20 notes.  Our goal is to use Andersens analysis to prove that the dynamic check for the cast to Foo in the last line will never fail.  This check will indeed never fail but the analysis, as presented in the lecture, will fail to prove it.

 

class SimpleContainer { Object a;

   void put (Object o) { a=o; }    

   Object get() { return a; }     

SimpleContainer c1 = new SimpleContainer();

SimpleContainer c2 = new SimpleContainer();

c1.put(new Foo()); 

c2.put(“Hello”);

Foo myFoo = (Foo) c1.get();  // verify that cast does not fail

 

 

Here is a Prolog program that (i) translates the above Java program to Prolog facts and (ii) contains inference rules for Andersen's analysis.  We also added rules that show how one can extend Andersen's analysis to answer other facts.  Specifically, we added rules that check whether it is safe to eliminate a cast (rules type, typeFlowingTo, and (un)safeToEliminateCast.

 

% These are the inference rules of Andersen's analysis.  

% They are the same for each program.

 

flowsTo(O,X) :- new(O,X).

flowsTo(O,X) :- assign(Y,X), flowsTo(O,Y).

flowsTo(O,X) :- pf(Y,P,F), gf(R,X,F), alias(P,R), flowsTo(O,Y).

 

alias(X,Y)   :- flowsTo(O,X), flowsTo(O,Y).

 

% We'll rewrite the above program to allow translation to the 

% four canonical statements used in Andersen's analysis.

 

% class SimpleContainer { Object a;

%   void put (Object o) { a=o; }  is rewritten to ...

% void put (put_this, o) { put_this.a=o; }   is rewritten to ...

%   put_this.a = o 

 

pf(put_o,put_this,a).      

 

%   Object get() { return a; }    is rewritten to ...

%   get(get_this) { return get_this.a; }   is rewritten to ...

%   get_retval = get_this.a 

 

gf(get_this,get_retval,a).  

 

new(o1,c1).      % SimpleContainer c1 = new SimpleContainer();

new(o2,c2).      % SimpleContainer c2 = new SimpleContainer();

 

new(o3,t1).           % t1 = new Foo();

new(o4,t2).           % t2 = “Hello”;

 

assign(c1,put_this).  % put(c1,t1); % c1.put(t1); 

assign(t1,put_o).     % ... now copy the second argument

 

assign(c2,put_this).  % put(c2,t2); % c2.put(t2); 

assign(t2,put_o).     % ... now copy the second argument

 

assign(c1,get_this).    % t3 = get(c1); % t3 = c1.get();  

assign(get_retval,t3).  % get the return value

 

% Now we want to prove that this cast does not fail.

%    Foo myFoo = (Foo) t3;

% We want to prove that only values of type Foo flow 

% to variable t3.

 

 

Run this program on your favorite Prolog interpreter.  Here are a few interesting queries.  This query tells us that method put might be invoked on both containers (one is allocated in o1, the other in o2).  More precisely, it cannot be proven that put is not called on either c1 or c2.  Examining the program manually, we see that this result of the analysis is precise, i.e., put is indeed called on both containers.

 

     ?- flowsTo(O,put_this).

     O = o1

     O = o2

 

This query tells us t3, which is cast to Foo, might reference both a Foo object (allocated in o3) and a String object (allocated in o4).  Examining the program tells us that this result is imprecise (t3 can only point to Foo).  Our goal is to make the analysis more precise.

 

     ?-flowsTo(O,t3).

     O = o3

     O = o4

 

Question 1: Extend the Andersen's analyzer above with the rule safeToEliminateCast(X,T).  If the rule answer Yes, then it is safe to eliminate the dynamic check associated with the Java cast (T)X because the dynamic type of the value stored in the variable X is guaranteed by the analyzer to be compatible with the type T.  For example, on our program, the rule must answer:

 

    ?- safeToEliminateCast(c1,simpleContainer).

    Yes

    ?- safeToEliminateCast(t3,foo).

     No

 

Hint: define auxiliary rules type(O,T), typeFlowingTo(X,T), and unsafeToEliminateCast(X,T).

 

Question 2: Explain why the analyzer concluded that flowsTo(o4,t3) holds.

 

  • You must give a sequence s of statements (i.e., a program trace) which the analyzer assumed might be executed by the program and which has such a property that o4 indeed flows to t3 along s (i.e., if s were executed).  This sequence should consist of the four kinds of statements that can appear in Andersen's programs.
  • Explain why s cannot actually be executed by the program.
  • Explain which approximation of program semantics made the analyzer conclude that s might be executed by the program.

 

Question 3: Modify the program so that the imprecision identified in Question 1 is removed.  That is, rewrite the program so that safeToEliminateCast(t3,foo)answers Yes.  Modify the program at the Java level, not at the level of the four Andersen's statements.  You modification must be mechanizable, that is, a compiler, not just a human, should be able to perform it.

 

 

Comments (0)

You don't have permission to comment on this page.