Merge branch 'master' into SelfReference

.github/workflows/release-brew.yml

@@ -19,43 +19,35 @@ jobs:
  - name: Install dafny
  run: |
  brew install dafny
- - name: Make test program
- run: |
- echo "method Main() { assert true; print 42, ['\n']; }" > a.dfy
- echo "method m() { assert false; }" > b.dfy
- echo "42" > expect.txt
  - name: Versions
  run: |
- dafny -version
  which dafny
- # -version is not supported in old dafny,
- # but this gives the version with an error
+ dafny -version
  dotnet --list-sdks
  go version
  node --version
  java -version
- - name: Check
- run: dafny /compile:0 a.dfy
- - name: Check bad
- run: dafny /compile:0 b.dfy || echo EXPECTED FAILURE
- ## Check that a simple program compiles and runs on each supported platform
- - name: Check C# compile
- run: |
- dafny /compileVerbose:0 /compile:3 /compileTarget:cs /spillTargetCode:3 a.dfy
- - name: Check Go compile
- run: |
- dafny /compile:3 /spillTargetCode:3 /compileTarget:go a.dfy
- env GO111MODULE=auto GOPATH=$PWD/a-go go run a-go/src/a.go > actual.txt
- diff expect.txt actual.txt
- - name: Check Javascript compile
+ python --version
+ - name: Set up Python
+ uses: actions/setup-python@v4
+ with:
+ python-version: '3.11'
+ ## To be consistent, the download should be tested with the quicktest.sh corresponding to
+ ## that release. But earlier releases relied on inline tests. So for up through 4.0,
+ ## we downliad quicktest.sh from the repo -- which will eventually fail if the quicktest
+ ## evolves beyond the capabilities of old versions.
+ ## But post-4.0, the script is part of the release and internally checks its results.
+ - name: Perform smoke tests on each platform
  run: |
  npm install bignumber.js
- dafny /compile:3 /spillTargetCode:3 /compileTarget:js a.dfy
- node a.js dafny/DafnyRuntime.js > actual.txt
- diff expect.txt actual.txt
- - name: Check Java compile
- run: |
- (ls dafny/DafnyRuntime.jar || echo NO DafnyRuntime.jar )
- #dafny /compile:3 /spillTargetCode:3 /compileTarget:java a.dfy
- #java -cp a:dafny/DafnyRuntime.jar a > actual.txt
- #diff expect.txt actual.txt
+ ver=`dafny -version`
+ ver=${ver[1]}
+ if [[ "$ver" < "4.0.0.99999" ]] ; then \
+ echo "4.0 or prior" ;\
+ wget https://github.com/dafny-lang/dafny/raw/master/Scripts/quicktest.sh; \
+ else \
+ echo "Post 4.0" ;\
+ cp /usr/local/Cellar/dafny/*/libexec/quicktest.sh . ;\
+ fi
+ chmod +x quicktest.sh
+ ./quicktest.sh `which dafny`

Scripts/quicktest.out

@@ -1,48 +1,13 @@
 Should succeed
-
-Dafny program verifier finished with 1 verified, 0 errors
 Should fail
-b.dfy(1,24): Error: assertion might not hold
-
-Dafny program verifier finished with 0 verified, 1 error
 Running with C#
-
-Dafny program verifier finished with 0 verified, 0 errors
-(42, 131)
 Running with Javascript
-
-Dafny program verifier finished with 0 verified, 0 errors
-(42, 131)
 Running with Java
-
-Dafny program verifier finished with 0 verified, 0 errors
-(42, 131)
 Running with Go
-
-Dafny program verifier finished with 0 verified, 0 errors
-(42, 131)
 Running with Python
-
-Dafny program verifier finished with 0 verified, 0 errors
-(42, 131)
 Building with C#
-
-Dafny program verifier finished with 0 verified, 0 errors
-(42, 131)
 Building with Javascript
-
-Dafny program verifier finished with 0 verified, 0 errors
-(42, 131)
 Building with Java
-
-Dafny program verifier finished with 0 verified, 0 errors
-(42, 131)
 Building with Go
-
-Dafny program verifier finished with 0 verified, 0 errors
-(42, 131)
-(42, 131)
 Building with Python
-
-Dafny program verifier finished with 0 verified, 0 errors
-(42, 131)
+Quicktest script succeeded

Scripts/quicktest.sh

@@ -4,43 +4,67 @@ echo "method m() { assert 1+1 == 2; }" > a.dfy
 echo "method m() { assert 1+1 == 3; }" > b.dfy
 echo 'method Main() { print (42,131), "\n"; }' > c.dfy
 
+tmp=quicktest.tmp
+tmpx=quicktest.tmpx
+
 DIR="$(dirname ${BASH_SOURCE[0]})"
 if [ -n "$1" ]; then
  DAFNY=$1
 else
  DAFNY=$DIR/dafny
 fi
 
+echo "" > $tmp
+echo "Dafny program verifier finished with 1 verified, 0 errors" >> $tmp
+
 echo Should succeed
-$DAFNY verify a.dfy
+$DAFNY verify a.dfy | diff - $tmp || exit 1
+
+echo "b.dfy(1,24): Error: assertion might not hold" > $tmp
+echo "" >> $tmp
+echo "Dafny program verifier finished with 0 verified, 1 error" >> $tmp
+
 echo Should fail
-$DAFNY verify --use-basename-for-filename b.dfy
+$DAFNY verify --use-basename-for-filename b.dfy | diff - $tmp
+
+echo "" > $tmp
+echo "Dafny program verifier finished with 0 verified, 0 errors" >> $tmp
+echo "(42, 131)" >> $tmp
+
 echo Running with C#
-$DAFNY run -t:cs c.dfy
+$DAFNY run -t:cs c.dfy | diff - $tmp || exit 1
 echo Running with Javascript
-$DAFNY run -t:js c.dfy
+$DAFNY run -t:js c.dfy | diff - $tmp || exit 1
 echo Running with Java
-$DAFNY run -t:java c.dfy
+$DAFNY run -t:java c.dfy | diff - $tmp || exit 1
 echo Running with Go
-$DAFNY run -t:go c.dfy
+$DAFNY run -t:go c.dfy | diff - $tmp || exit 1
 echo Running with Python
-$DAFNY run -t:py c.dfy
-echo Building with C#
+$DAFNY run -t:py c.dfy | diff - $tmp || exit 1
+
 rm -rf c-go c-java c-py c.jar c c.dll c.exe c.js c.runtimeconfig.json
-$DAFNY build -t:cs c.dfy
-dotnet c.dll
+echo "" > $tmp
+echo "Dafny program verifier finished with 0 verified, 0 errors" >> $tmp
+echo "(42, 131)" > $tmpx
+
+echo Building with C#
+$DAFNY build -t:cs c.dfy | diff - $tmp || exit 1
+dotnet c.dll | diff - $tmpx || exit 1
 echo Building with Javascript
-$DAFNY build -t:js c.dfy
-node c.js
+$DAFNY build -t:js c.dfy | diff - $tmp || exit 1
+node c.js | diff - $tmpx || exit 1
 echo Building with Java
-$DAFNY build -t:java c.dfy
-java -jar c.jar
+$DAFNY build -t:java c.dfy | diff - $tmp || exit 1
+java -jar c.jar | diff - $tmpx || exit 1
 echo Building with Go
-$DAFNY build -t:go c.dfy
-./c
-(cd c-go; GO111MODULE=auto GOPATH=`pwd` go run src/c.go)
+$DAFNY build -t:go c.dfy | diff - $tmp || exit 1
+./c | diff - $tmpx || exit 1
+(cd c-go; GO111MODULE=auto GOPATH=`pwd` go run src/c.go) | diff - $tmpx || exit 1
 echo Building with Python
-$DAFNY build -t:py c.dfy
-python c-py/c.py
+$DAFNY build -t:py c.dfy | diff - $tmp || exit 1
+python c-py/c.py | diff - $tmpx || exit 1
+
+echo Quicktest script succeeded
 
 rm -rf a.dfy b.dfy c.dfy c-go c-java c-py c.jar c c.dll c.exe c.js c.runtimeconfig.json
+rm $tmp $tmpx

Source/DafnyCore/Dafny.atg

@@ -188,6 +188,7 @@ public static Parser SetupParser(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module,
  return new Parser(scanner, errors, module, builtIns);
 }
 
+// Unused code
 public static Expression ParseExpression(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module,
  BuiltIns builtIns, Errors/*!*/ errors) {
  Parser parser = SetupParser(s, uri, module, builtIns, errors);
@@ -358,10 +359,10 @@ bool IsGets() {
  return la.kind == _gets;
 }
 
-bool IsVar() {
+bool IsPeekVar() {
  scanner.ResetPeek();
  IToken x = scanner.Peek();
- return la.kind == _var || (x.kind == _var && la.kind == _ghost);
+ return x.kind == _var;
 }
 
 // an existential guard starts with an identifier and is then followed by
@@ -4487,12 +4488,12 @@ ParensExpression<out Expression e>
 TupleArgs<.List<ActualBinding> args.>
 = (. ActualBinding binding; bool isGhost = false; .)
  // The IF is to distinguish between `(ghost var x := 5; x + x)` and (ghost x), both of which begin with `( ghost`.
- [ IF(la.kind == _ghost && !IsVar())
+ [ IF(la.kind == _ghost && !IsPeekVar())
  "ghost" (. isGhost = true; .)
  ]
  ActualBinding<out binding, isGhost> (. args.Add(binding); .)
  { "," (. isGhost = false; .)
- [ IF(la.kind == _ghost && !IsVar())
+ [ IF(la.kind == _ghost && !IsPeekVar())
  "ghost" (. isGhost = true; .)
  ]
  ActualBinding<out binding, isGhost> (. args.Add(binding); .)
@@ -4684,6 +4685,8 @@ LetExprWithLHS<out Expression e, bool allowLemma, bool allowLambda, bool allowBi
  bool isGhost = false;
  var letLHSs = new List<CasePattern<BoundVar>>();
  var letRHSs = new List<Expression>();
+ IToken lastLHS = null;
+ IToken lastRHS = null;
  CasePattern<BoundVar> pat;
  bool exact = true;
  bool isLetOrFail = false;
@@ -4695,6 +4698,7 @@ LetExprWithLHS<out Expression e, bool allowLemma, bool allowLambda, bool allowBi
  "var" (. if (!isGhost) { x = t; } .)
  CasePattern<out pat> (. if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); }
  letLHSs.Add(pat);
+ lastLHS = la;
  .)
  { "," CasePattern<out pat> (. if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); }
  letLHSs.Add(pat);
@@ -4712,7 +4716,7 @@ LetExprWithLHS<out Expression e, bool allowLemma, bool allowLambda, bool allowBi
  | ":-" (. isLetOrFail = true; .)
  | "=" (. SemErr(t, "a variable in a let expression should be initialized using ':=', ':-', or ':|', not '='"); .)
  )
- Expression<out e, false, true> (. letRHSs.Add(e); .)
+ Expression<out e, false, true> (. letRHSs.Add(e); lastRHS = la; .)
  { "," Expression<out e, false, true> (. letRHSs.Add(e); .)
  }
  ";"
@@ -4724,14 +4728,14 @@ LetExprWithLHS<out Expression e, bool allowLemma, bool allowLambda, bool allowBi
  if (letLHSs.Count == 1) {
  lhs = letLHSs[0];
  } else {
- SemErr("':-' can have at most one left-hand side");
+ SemErr(lastLHS, "':-' can have at most one left-hand side");
  }
  Expression rhs = null;
  Contract.Assert(letRHSs.Count > 0);
  if (letRHSs.Count == 1) {
  rhs = letRHSs[0];
  } else {
- SemErr("':-' must have exactly one right-hand side");
+ SemErr(lastRHS, "':-' must have exactly one right-hand side");
  }
  e = new LetOrFailExpr(x, lhs, rhs, e);
  } else {

Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs

@@ -351,7 +351,7 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont
  var e = (NegationExpression)expr;
  ResolveExpression(e.E, resolutionContext);
  e.Type = e.E.Type;
- AddXConstraint(e.E.tok, "NumericOrBitvector", e.E.Type, "type of unary - must be of a numeric or bitvector type (instead got {0})");
+ AddXConstraint(e.E.tok, "NumericOrBitvector", e.E.Type, "the argument of a unary minus must have numeric or bitvector type (instead got {0})");
  // Note, e.ResolvedExpression will be filled in during CheckTypeInference, at which time e.Type has been determined
 
  } else if (expr is LiteralExpr) {
@@ -601,7 +601,7 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont
  "non-function expression (of type {0}) is called with parameters", e.Function.Type);
  } else if (fnType.Arity != e.Args.Count) {
  reporter.Error(MessageSource.Resolver, e.tok,
- "wrong number of arguments to function application (function type '{0}' expects {1}, got {2})", fnType,
+ "wrong number of arguments for function application (function type '{0}' expects {1}, got {2})", fnType,
  fnType.Arity, e.Args.Count);
  } else {
  for (var i = 0; i < fnType.Arity; i++) {

Source/DafnyCore/Resolver/TailRecursion.cs

@@ -362,7 +362,7 @@ public void DetermineTailRecursion(Function f) {
  if (hasTailRecursionPreference && !tail) {
  // the user specifically requested no tail recursion, so do nothing else
  } else if (hasTailRecursionPreference && tail && f.IsGhost) {
- reporter.Error(MessageSource.Resolver, f.tok, "tail recursion can be specified only for function that will be compiled, not for ghost functions");
+ reporter.Error(MessageSource.Resolver, f.tok, "tail recursion can be specified only for functions that will be compiled, not for ghost functions");
  } else {
  var module = f.EnclosingClass.EnclosingModuleDefinition;
  var sccSize = module.CallGraph.GetSCCSize(f);

Test/dafny0/QuantificationNewSyntaxResolution.dfy.expect

@@ -14,7 +14,7 @@ QuantificationNewSyntaxResolution.dfy(35,37): Error: range of quantified variabl
 QuantificationNewSyntaxResolution.dfy(36,25): Error: range of quantified variable must be of type bool (instead got string)
 QuantificationNewSyntaxResolution.dfy(37,18): Error: range restriction in forall statement must be of type bool (instead got string)
 QuantificationNewSyntaxResolution.dfy(44,19): Error: arguments to < must have a common supertype (got set<?> and seq<int>)
-QuantificationNewSyntaxResolution.dfy(44,23): Error: type of unary - must be of a numeric or bitvector type (instead got seq<int>)
+QuantificationNewSyntaxResolution.dfy(44,23): Error: the argument of a unary minus must have numeric or bitvector type (instead got seq<int>)
 QuantificationNewSyntaxResolution.dfy(9,22): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int)
 QuantificationNewSyntaxResolution.dfy(10,32): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int)
 QuantificationNewSyntaxResolution.dfy(15,22): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got int)

Test/dafny0/TailCalls.dfy.expect

@@ -8,7 +8,7 @@ TailCalls.dfy(171,13): Error: to be tail recursive, every use of this function m
 TailCalls.dfy(174,6): Error: to be tail recursive, every use of this function must be part of a tail call or a simple accumulating tail call
 TailCalls.dfy(178,13): Error: to be tail recursive, every use of this function must be part of a tail call or a simple accumulating tail call
 TailCalls.dfy(181,6): Error: to be tail recursive, every use of this function must be part of a tail call or a simple accumulating tail call
-TailCalls.dfy(188,32): Error: tail recursion can be specified only for function that will be compiled, not for ghost functions
+TailCalls.dfy(188,32): Error: tail recursion can be specified only for functions that will be compiled, not for ghost functions
 TailCalls.dfy(195,30): Error: tail recursion can be specified only for methods that will be compiled, not for ghost methods
 TailCalls.dfy(229,7): Error: if-then-else branches have different accumulator needs for tail recursion
 TailCalls.dfy(261,2): Error: if-then-else branches have different accumulator needs for tail recursion

Test/dafny4/parse-errors.dfy

@@ -0,0 +1,24 @@
+// RUN: ! %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype D = B | CCC | E { predicate IsFailure() { E? } function PropagateFailure(): D { E } }
+
+// Careful: some errors will prevent subsequent ones from begin reported
+
+method m2() returns (d: D) {
+ var x := (var y, z :- D.E; 0);
+ var x := (var y :- D.CCC, 0; 0);
+ var x := (var y = D.CCC, 0; 0);
+ var x := (var B() :| D.CCC; 0);
+ var m := map x, y :: x+y;
+ var n := ( z := 0 );
+ var s := seq<int,int>(1, _=>0);
+ var s := seq<int>(1, 2);
+ var s := seq<int>(1);
+ var s := [1,2,3,];
+}
+
+method m3() {
+ var x := (var x := 0; 0);
+}
+

Test/dafny4/parse-errors.dfy.expect

@@ -0,0 +1,10 @@
+parse-errors.dfy(9,17): Error: ':-' can have at most one left-hand side
+parse-errors.dfy(10,26): Error: ':-' must have exactly one right-hand side
+parse-errors.dfy(11,18): Error: a variable in a let expression should be initialized using ':=', ':-', or ':|', not '='
+parse-errors.dfy(12,16): Error: LHS of let-such-that expression must be variables, not general patterns
+parse-errors.dfy(13,25): Error: a map comprehension with more than one bound variable must have a term expression of the form 'Expr := Expr'
+parse-errors.dfy(14,13): Error: binding not allowed in parenthesized expression
+parse-errors.dfy(15,22): Error: seq type expects only one type argument
+parse-errors.dfy(17,21): Error: comma expected
+parse-errors.dfy(18,18): Error: invalid UnaryExpression
+9 parse errors detected in parse-errors.dfy

Test/dafny4/parse-errors2.dfy

@@ -0,0 +1,13 @@
+// RUN: ! %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype D = D(z: int, 2: int)
+method m1(s: seq<int>) {
+ var a := 1 ! ! 1;
+ var a := 1 ! 1;
+}
+
+method m2() {
+ assert true <== true ==> true ==> true <== true;
+ assert 1 !! 1 != 1;
+}

Test/dafny4/parse-errors2.dfy.expect

@@ -0,0 +1,5 @@
+parse-errors2.dfy(6,13): Error: invalid relational operator (perhaps you intended "!!" with no intervening whitespace?)
+parse-errors2.dfy(7,13): Error: invalid relational operator
+parse-errors2.dfy(11,23): Error: Ambiguous use of ==> and <==. Use parentheses to disambiguate.
+parse-errors2.dfy(12,16): Error: this operator cannot continue this chain
+4 parse errors detected in parse-errors2.dfy

Test/git-issues/git-issue-889b.dfy.expect

@@ -5,7 +5,7 @@ git-issue-889b.dfy(24,9): Error: unary minus (-0, type bv8) not allowed in case
 git-issue-889b.dfy(30,11): Error: unary minus (-3, type bv8) not allowed in case pattern
 git-issue-889b.dfy(31,11): Error: unary minus (-0, type bv8) not allowed in case pattern
 git-issue-889b.dfy(39,9): Error: unary minus (-0, type bv0) not allowed in case pattern
-git-issue-889b.dfy(46,10): Error: type of unary - must be of a numeric or bitvector type (instead got ORDINAL)
+git-issue-889b.dfy(46,10): Error: the argument of a unary minus must have numeric or bitvector type (instead got ORDINAL)
 git-issue-889b.dfy(54,9): Error: unary minus (-2, type ORDINAL) not allowed in case pattern
 git-issue-889b.dfy(55,9): Error: unary minus (-0, type ORDINAL) not allowed in case pattern
 10 resolution/type errors detected in git-issue-889b.dfy