Dafny compiler warnings appear to prevent Dafny program from running in VSCode

[kevinsullivan]

My Dafny program verifies, but when I try to "Compile and Run", I still get an error in VSCode, namely, "Errors compiling program into basic-dafny.exe." I debugged this a little by running the compiler in a terminal window in VSCode. Here's the output. You can see that the program does verify, but the compiler nevertheless reports "Errors compiling program into basic-dafny.exe. The "errors" that it then reports are really only warnings. That said, they're very cryptic warnings that appear to be coming from deep in the bowels of Dafny. I haven't yet figured out what they mean. The main problem here is that the Dafny VSCode plugin is interpreting Dafny's misleading error message as an indication that it's not possible to run the compiled program. But the program does compile, and can be run using "mono Dafny.exe /compile:3" at the command line. Maybe this is an error for the Dafny team. But your plug-in team should at least be aware of the issue. Close this out if it doesn't belong here. Here are the reported compiler errors.

====

OS = OSX High Sierra (10.13) Plugin version = 0.10.10 Dafny version = Hard to tell, no obvious -version compiler option, but current as of January 2018

====

Dafny program verifier finished with 9 verified, 0 errors Errors compiling program into basic-dafny.exe /var/folders/5n/6hml8q9s39300wsyb2kb89b00000gn/T/4bcad2d0/5e25f480.0.cs(1792,19) : warning CS1718: A comparison made to same variable. Did you mean to compare something else? /var/folders/5n/6hml8q9s39300wsyb2kb89b00000gn/T/4bcad2d0/5e25f480.0.cs(1854,7) : warning CS0162: Unreachable code detected

[fmehta]

Thanks for your comment. Could you please provide a source file and exact steps that can be used to reproduce this behaviour?

[kevinsullivan]

I'm running up-to-date plugin and VSCode on an up-to-date OSX machine. The file I'm trying to compile and run is -- in still draft version -- just a quick "getting started" pedagogical program. It's appended below the --- line. To replicate the problem, add this program to a folder and then try to compile and run it. Thanks Kevin

--- the program ---

/*
Dafny support C-style comments
*/

// Like this

/* 
Dafny supports pure functional programming. In functional
programming, we have data and functions that transform data,
but we have no concept of a memory full of data that can be
changed by executing commands, such as assignment commands. 
Here is an example of a function of type int -> int. This type
says that the function consumes a value of type int and returns
a value of type int. By the way, int is the type for integers in Dafny. You will recall from mathematical that the "integers" is
the set of whole numbers: negative, zero, and positive.
*/
function factorial(n: int): int
    requires n >= 0
{
    if (n == 0) then 1  else  n * factorial (n-1) 
}
/*
This function is meant to computs the factorial of the given 
number. You will recall from mathematics that the factorial of 
0 is 1 and the factorial of n, n>0, is n*factorial(n-1). The
factorial of 5 is thus 5 * factorial(4) -- and this of course is
5 * (4 * factorial(3)), which is 5 * (4 * (3 * factorial(2))),
which in turn is 5 * (4 * (3 * 2 * factorial(1))), which is
5 * (4 * (3 * (2 * (1 * factorial(0))))), which is 5*4*3*2*1*1,
which is 120.
*/

// There's something wrong with our definition. What is it?

/*
A pre-condition is a property of the values being manipulated
by a program that must be satisfied in order for a function to 
be guaranteed to work properly. What precondition is necessary for this function to work properly?

A precondition is a part of the specification of a program or a piece thereof. Whereas implementations are written in programming code, specifications are written in the language of mathematical logic. It sounds complicated, but it't really not so bad. Dafny is a software engineering language in which you can include formal specification elements right along with your code, and Dafny will
"do its best" to try to determine whether your code satisfies the specifications you've provided.
*/

/*
Functions in Dafny are defined for use in specifications,
not to be called by ordinary programming code. You can,
however, write pure functions that can be used in regular
code by declaring them as function methods. Here's the 
same function as a function method.
*/

function method fac(n: int): int 
    requires n >= 0
{
    if (n==0) then 1 else n * fac(n-1)
}

/*
Dafny also fully supports imperative programming. This is 
what you've been learning in 111x and maybe in other classes.
Imperative programs are based on variables that store data
in a memory that can be updated using assignment commands.
Imperative programs can also affect the environment outside
the program by doing input and output. Imperative code is
written in Dafny using methods instead of functions. Here's 
a main method that uses the factorial function to compute the
factorial of 5 and then to output the result to the console.
*/

method Main() 
{
    var five_fac := fac(5); // can't use factorial; fac is ok
    // functions are applied to arguments without parentheses
    print("The factorial of 5 is ", five_fac, "\n");
}

// nat is the type of natural numbers (integers >= 0)
// here's a similar function of type nat -> nat
// note that we don't have the same problem as before
// Dafny can prove to itself that the recursion always terminates
function fib(n: nat): nat
{
    if n < 2 then n else fib(n-2) + fib(n-1)
}

// Here's a pure function of type int -> bool
// it tells you whether a given natural number is even or not
function evenb (n: nat): bool
{
    if (n == 0) then true else if (n==1) then false else evenb(n-2)
}

// A pure function that returns bool can be called a predicate
// you don't have to (and can't) given an explicit return type
predicate evenb2 (n: nat)
{
    if (n == 0) then true else if (n==1) then false else evenb(n-2)
}

// pure functions can't do I/O and lots of other stuff
// but they are very useful in writing specifications
// methods on the other hand are used to write imperative code

// Here's a method that illustrates boolean operators in Dafny
method BoolOps() returns (r: bool)
{
    var t: bool := true;
    var f := false;
    var not := !t;
    var conj := t && f;     // short-circuiting
    var disj := t || f;     // short-circuiting
    var impl := t ==> f;    // right associative, s.c. from left
    var foll := t <== f;    // left associative, s.c. from right
    var equv := t <==> t;
    return true;
 }
/* Methods aren't required to return results. Such methods
   do their jobs by having side effects, e.g., doing output
   or writing data into global variables (usually a bad idea).
   Here's a method that doesn't return a value. It illustrates
   numerical types, syntax, and operations.
*/
method NumOps()
{
    var r1: real := 1000000.0;
    var i1: int := 1000000;
    var i2: int := 1_000_000;   // underscores for readiability
    var i3 := 1_000;            // Dafny can often infer types
    var b1 := (10 < 20) && (20 <= 30); // a boolean expression
    var b2 := 10 < 20 <= 30;    // equivalent, with "chaining"
    var i4: int := (5.5).Floor; // 5
    var i5 := (-2.5).Floor;     // -3
    var i6 := -2.5.Floor;        // -2 = -(2.5.Floor); binding!
}

// Characters (char) are handled sort of as they are in C, etc.
method CharFun()
{
    var c1: char := 'a';
    var c2 := 'b';
    // var i1 := c2 - c1;
    var i1 := (c2 as int) - (c1 as int);    // type conversion
    var b1 := c1 < c2;  // ordering operators defined for char
    var c3 := '\n';     // c-style escape for non-printing chars
    var c4 := '\u265B'; // unicode, hex, "chess king" character
}

// To return a value from a method, assign to the return parameter
// Note: functions have colon then return type, whereas methods 
// have return keyword then return parameter list
method ReturnExample() returns (retval: int)
{
    retval := 10;
}

// Methods can return multiple values
method ReturnExample2() returns (x: int, y:int)
{
    x := 10; 
    y := 20;
}

// The return keyword can be used to return immediatey
method ReturnExample3() returns (x: int)
{
    x := 5;     // don't "var" decare return variable
    return;     // return immediately
    x := 6;     // never gets executed
}

// Polymorphic finite and infinite set types.
// set<T> and iset<T>. T must support equality.
method SetPlay()
{
    var empty: set<int> := {};
    var primes := {2, 3, 5, 7, 11};
    var squares := {1, 4, 9, 16, 25};
    var b1 := empty < primes;    // strict subset
    var b2 := primes <= primes;   // subset
    var b3: bool := primes !! squares; // disjoint
    var union := primes + squares;
    var intersection := primes * squares;
    var difference := primes - {3, 5};
    var b4 := primes == squares;    // false
    var i1 := | primes |;   // cardinality (5)
    var b5 := 4 in primes;  // membership (false)
    var b6 := 4 !in primes; // non-membership
    /*
     we'll come back to infinite sets and
     set comprehension notations later on
    */
}

// Polymorphic sequences (often called "lists").
// A function from indices to values. Some of 
// the operations require that T support equality.
method SequencePlay()
{
    var empty_seq: seq<char> := [];
    var hi_seq: seq<char> := ['h', 'i'];
    var b1 := hi_seq == empty_seq; // equality; !=
    var hchar := hi_seq[0];        // indexing 
    var b2 := ['h'] < hi_seq;   // proper prefix
    var b3 := hi_seq < hi_seq;  // this is false
    var b4 := hi_seq <= hi_seq; // prefix, true
    var sum := hi_seq + hi_seq; // concatenation
    var len := | hi_seq |;
    var Hi_seq := hi_seq[0 := 'H']; // update
    var b5 := 'h' in hi_seq; // member, true, !in
    var s := [0,1,2,3,4,5];
    var s1 := s[0..2];  // subseqence
    var s2 := s[1..];   // "drop" prefix of len 1
    var s3 := s[..2];   // "take" prefix of len 2
    // there's a slice operator, too; later
 }

 /*
    Dafny has strings. Strings are literally just
    sequences of characters (of type seq<char>), so
    you can use all the sequence operations on strings.
    Dafny provides additional helpful syntax for strings.
*/
method StringPlay() 
 {
     var s1: string := "Hello CS2102!";
     var s2 := "Hello CS2102!\n";   // return
     var s3 := "\"Hello CS2102!\""; // quotes
 }

/*
  Dafny also supports polymorphic maps, both 
  finite (map<K,V>) and infinite (imap<K,V>).
  The key type, K, must support equality (==).
  In mathematical terms, a map really represents
  a binary relation, i.e., a set of <K,V> pairs,
  which is to say a subset of the product set,
  K * V, where we view the types K and V as
  defining sets of values.
  */
method MapPlay()
{
    // A map literal is keyword map + a list of maplets.
    // A maplet is just a single <K,V> pair (or "tuple").
    // Here's an empty map from strings to ints
    var emptyMap: map<string,int> := map[];

    // Here's non empty map from strings to ints
    // A maplet is "k := v," k and v being of types K and V
    var aMap: map<string,int>  := map["Hi" := 1, "There" := 2];

    // Map domain (key) membership
    var isIn: bool := "There" in aMap; // true
    var isntIn := "Their" !in aMap;    // true

    // Finite map cardinality (number of maplets in a map)
    var card := |aMap|;

    //Map lookup
    var image1 := aMap["There"];
    // var image2 := aMap["Their"]; // error! some kind of magic
    var image2: int;
    if ("Their" in aMap) { image2 := aMap["Their"]; }

    // map update, maplet override and maplet addition
    aMap := aMap["There" := 3];
    aMap := aMap["Their" := 10];  
}

// Dafny supports arrays. Here's we'll see simple 1-d arrays.

method ArrayPlay() 
{
    var a := new int[10]; // in general: a: array<T> := new T[n];
    var a' := new int[10];   // type inference naturally works here
    var i1 := a.Length;      // Immutable "Length" member holds length of array
    a[3] := 3;           // array update
    var i2 := a[3];          // array access
    var seq1 := a[3..8];    // take first 8, drop first 3, return as sequence
    var b := 3 in seq1;     // true! (see sequence operations)
    var seq2 := a[..8];     // take first 8, return rest as sequence
    var seq3 := a[3..];     // drop first 3, return rest as sequence
    var seq4 := a[..];      // return entire array as a sequence
}

/*
Arrays, objects (class instances), and traits (to be discussed) are of
"reference" types, which is to say, values of these types are stored on 
the heap. Values of other types, including sets and sequences, are of 
"value types," which is to say values of these types are stored on the 
stack; and they're thus always treated as "local" variables. They are
passed by value, not reference, when passed as arguments to functions
and methods. Value types include the basic scalar types (bool, char, 
nat, int, real), built-in collection types (set, multiset, seq, string, 
map, imap), tuple, inductive, and co-inductive types (to be discussed).
Reference type values are allocated dynamically on the heap, are passed 
by reference, and therefore can be "side effected" (mofified) by methods
to which they are passed.
*/

[fabianhauser]

I took a look at the error and this is indeed a bug in the upstream dafny compiler.

Would be great if you could open an issue there!