Dafny:

* Big change:  Add type and allocatedness information everywhere in the Boogie translation.  This not only fixes some potential soundness problems (see Test/dafny1/TypeAntecedents.dfy), but it also gives more information about the program.  On the downside, it also requires discharging more antecedents in order to use some axioms.  Another downside is that overall performance has gone down (however, this may be just an indirect consequence of the change, as it was in one investigated case).

* Increase the applicability of function axioms (extending the coarse-grain function/module height mechanism used as an antecedent of function axioms).  (Internally, this uses the new canCall mechanism.)

* Extend language with "allocated( Expr )" expressions, which for any type of expression "Expr" says that "Expr" is allocated and has the expected type.

* More details error messages about ill-defined expressions (internally, by using CheckWellformedness instead of "assert IsTotal")

* Add axioms about idempotence of set union and intersection

* The compiler does not support (the experimental feature) coupling invariants, so generate error if the compiler ever gets one

* In the implementation, combine common behavior of MatchCaseStmt and MatchCaseExpr into a superclass MatchCase

* Fixed error in translation of while(*)

1 files changed, 58 insertions, 5 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 6c9faa29..1ef8aea7 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -51,6 +51,15 @@ function Set#Intersection<T>(Set T, Set T) returns (Set T);
 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] }

   Set#Intersection(a,b)[o] <==> a[o] && b[o]);

 

+axiom (forall<T> a, b: Set T :: { Set#Union(Set#Union(a, b), b) }

+  Set#Union(Set#Union(a, b), b) == Set#Union(a, b));

+axiom (forall<T> a, b: Set T :: { Set#Union(a, Set#Union(a, b)) }

+  Set#Union(a, Set#Union(a, b)) == Set#Union(a, b));

+axiom (forall<T> a, b: Set T :: { Set#Intersection(Set#Intersection(a, b), b) }

+  Set#Intersection(Set#Intersection(a, b), b) == Set#Intersection(a, b));

+axiom (forall<T> a, b: Set T :: { Set#Intersection(a, Set#Intersection(a, b)) }

+  Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b));

+

 function Set#Difference<T>(Set T, Set T) returns (Set T);

 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] }

   Set#Difference(a,b)[o] <==> a[o] && !b[o]);

@@ -205,8 +214,8 @@ const unique class.bool: ClassName;
 const unique class.set: ClassName;

 const unique class.seq: ClassName;

 

-function dtype(ref) returns (ClassName);

-function TypeParams(ref, int) returns (ClassName);

+function /*{:never_pattern true}*/ dtype(ref) returns (ClassName);

+function /*{:never_pattern true}*/ TypeParams(ref, int) returns (ClassName);

 

 function TypeTuple(a: ClassName, b: ClassName) returns (ClassName);

 function TypeTupleCar(ClassName) returns (ClassName);

@@ -222,6 +231,9 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) }
 

 type DatatypeType;

 

+function /*{:never_pattern true}*/ DtType(DatatypeType) returns (ClassName);  // the analog of dtype for datatype values

+function /*{:never_pattern true}*/ DtTypeParams(DatatypeType, int) returns (ClassName);  // the analog of TypeParams

+

 type DtCtorId;

 function DatatypeCtorId(DatatypeType) returns (DtCtorId);

 

@@ -244,9 +256,6 @@ type Field alpha;
 

 function FDim<T>(Field T): int;

 

-const unique alloc: Field bool;

-axiom FDim(alloc) == 0;

-

 function IndexField(int): Field BoxType;

 axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1);

 function IndexField_Inverse<T>(Field T): int;

@@ -264,6 +273,50 @@ axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) }
 function DeclType<T>(Field T) returns (ClassName);

 

 // ---------------------------------------------------------------

+// -- Allocatedness ----------------------------------------------

+// ---------------------------------------------------------------

+

+const unique alloc: Field bool;

+axiom FDim(alloc) == 0;

+

+function DtAlloc(DatatypeType, HeapType): bool;

+axiom (forall h, k: HeapType, d: DatatypeType ::

+  { $HeapSucc(h, k), DtAlloc(d, h) }

+  { $HeapSucc(h, k), DtAlloc(d, k) }

+  $HeapSucc(h, k) ==> DtAlloc(d, h) ==> DtAlloc(d, k));

+

+function GenericAlloc(BoxType, HeapType): bool;

+axiom (forall h: HeapType, k: HeapType, d: BoxType ::

+  { $HeapSucc(h, k), GenericAlloc(d, h) }

+  { $HeapSucc(h, k), GenericAlloc(d, k) }

+  $HeapSucc(h, k) ==> GenericAlloc(d, h) ==> GenericAlloc(d, k));

+// GenericAlloc ==>

+axiom (forall b: BoxType, h: HeapType ::

+  { GenericAlloc(b, h), h[$Unbox(b): ref, alloc] }

+  GenericAlloc(b, h) ==>

+  $Unbox(b): ref == null || h[$Unbox(b): ref, alloc]);

+axiom (forall b: BoxType, h: HeapType, i: int ::

+  { GenericAlloc(b, h), Seq#Index($Unbox(b): Seq BoxType, i) }

+  GenericAlloc(b, h) &&

+  0 <= i && i < Seq#Length($Unbox(b): Seq BoxType) ==>

+  GenericAlloc( Seq#Index($Unbox(b): Seq BoxType, i), h ) );

+axiom (forall b: BoxType, h: HeapType, t: BoxType ::

+  { GenericAlloc(b, h), ($Unbox(b): Set BoxType)[t] }

+  GenericAlloc(b, h) && ($Unbox(b): Set BoxType)[t] ==>

+  GenericAlloc(t, h));

+axiom (forall b: BoxType, h: HeapType ::

+  { GenericAlloc(b, h), DtType($Unbox(b): DatatypeType) }

+  GenericAlloc(b, h) ==> DtAlloc($Unbox(b): DatatypeType, h));

+// ==> GenericAlloc

+axiom (forall b: bool, h: HeapType ::

+  $IsGoodHeap(h) ==> GenericAlloc($Box(b), h));

+axiom (forall x: int, h: HeapType ::

+  $IsGoodHeap(h) ==> GenericAlloc($Box(x), h));

+axiom (forall r: ref, h: HeapType ::

+  { GenericAlloc($Box(r), h) }

+  $IsGoodHeap(h) && (r == null || h[r,alloc]) ==> GenericAlloc($Box(r), h));

+

+// ---------------------------------------------------------------

 // -- Arrays -----------------------------------------------------

 // ---------------------------------------------------------------