new axioms for subtyping

2 files changed, 45 insertions, 9 deletions

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 17ed8b20..6553efba 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -320,9 +320,6 @@ namespace BytecodeTranslator {
     [RepresentationFor("$Subtype", "function $Subtype(Type, Type): bool;")]

     public Bpl.Function Subtype = null;

 

-    [RepresentationFor("$DirectSubtype", "function $DirectSubtype(Type, Type): bool;")]

-    public Bpl.Function DirectSubtype = null;

-

     [RepresentationFor("$DisjointSubtree", "function $DisjointSubtree(Type, Type): bool;")]

     public Bpl.Function DisjointSubtree = null;

 

@@ -357,6 +354,7 @@ function {:builtin ""MapIff""} mapiff([Delegate]bool, [Delegate]bool) : [Delegat
 function {:builtin ""MapImp""} mapimp([Delegate]bool, [Delegate]bool) : [Delegate]bool;

 axiom MultisetEmpty == mapconstint(0);

 

+/*

 // Subtype is reflexive

 axiom (forall t: Type :: $Subtype(t, t) );

 

@@ -368,15 +366,11 @@ axiom (forall t0 : Type, t1 : Type :: { $Subtype(t0, t1), $Subtype(t1, t0) }
 axiom (forall t0 : Type, t1 : Type, t2 : Type :: { $Subtype(t0, t1), $Subtype(t1, t2) }

         $Subtype(t0, t1) && $Subtype(t1, t2) ==> $Subtype(t0, t2) );

 

-// Direct subtype definition

-axiom (forall C : Type, D : Type :: { $DirectSubtype(D, C) }

-        $DirectSubtype(D, C) <==> $Subtype(D, C) && (forall z : Type :: $Subtype(D, z) && $Subtype(z, C) ==> z == C || z == D )

-      );

-

 // Incomparable subtypes: the subtrees are disjoint for (some) subtypes (those that imply single inheritance)

 function oneDown(t0 : Type, t1 : Type) : Type; // uninterpreted function with no axioms

 axiom (forall C : Type, D : Type :: { $DisjointSubtree(D, C) }

         $DisjointSubtree(D, C) <==> (forall z : Type :: $Subtype(z, D) ==> oneDown(C,z) == D) );

+*/

 

 function $TypeOfInv(Ref): Type;

 axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 612854d9..afecc3d5 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -1034,7 +1034,7 @@ namespace BytecodeTranslator {
 

       this.declaredTypeFunctions.Add(key, f);

       this.TranslatedProgram.TopLevelDeclarations.Add(f);

-      DeclareParents(type, f);

+      DeclareParentsNew(type, f);

 

       bool isExtern = this.assemblyBeingTranslated != null &&

                       !TypeHelper.GetDefiningUnitReference(type).UnitIdentity.Equals(this.assemblyBeingTranslated.UnitIdentity);

@@ -1045,6 +1045,48 @@ namespace BytecodeTranslator {
       return f;

     }

 

+    private void DeclareParentsNew(ITypeDefinition typeDefinition, Bpl.Function typeDefinitionAsBplFunction) {

+      List<Bpl.Expr> superTypeExprs = new List<Bpl.Expr>();

+      foreach (var p in typeDefinition.BaseClasses) {

+        superTypeExprs.Add(FindOrCreateTypeReference(p));

+      }

+      foreach (var j in typeDefinition.Interfaces) {

+        superTypeExprs.Add(FindOrCreateTypeReference(j));

+      }

+

+      var numberOfGenericParameters = typeDefinitionAsBplFunction.InParams.Length;

+

+      var qvars = new Bpl.VariableSeq();

+      var exprs1 = new Bpl.ExprSeq();

+      var exprs2 = new Bpl.ExprSeq();

+      var exprs3 = new Bpl.ExprSeq();

+      for (int i = 0; i < numberOfGenericParameters; i++) {

+        var t = typeDefinitionAsBplFunction.InParams[i];

+        qvars.Add(t);

+        exprs1.Add(Bpl.Expr.Ident(t));

+        exprs2.Add(Bpl.Expr.Ident(t));

+        exprs3.Add(Bpl.Expr.Ident(t));

+      }

+

+      // G(t,u)

+      var callToG1 = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(typeDefinitionAsBplFunction), exprs1);

+      var callToG2 = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(typeDefinitionAsBplFunction), exprs2);

+      var callToG3 = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(typeDefinitionAsBplFunction), exprs3);

+

+      // T

+      Bpl.BoundVariable boundTypeVar = new Bpl.BoundVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$T", this.Heap.TypeType));

+      qvars.Add(boundTypeVar);

+      var lhs = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.Subtype), new Bpl.ExprSeq(callToG1, Bpl.Expr.Ident(boundTypeVar)));

+      var rhs = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, callToG2, Bpl.Expr.Ident(boundTypeVar));

+      foreach (var superTypeExpr in superTypeExprs) {

+        var subtype = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.Subtype), new Bpl.ExprSeq(superTypeExpr, Bpl.Expr.Ident(boundTypeVar)));

+        rhs = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or, rhs, subtype);

+      }

+      var trigger = new Bpl.Trigger(Bpl.Token.NoToken, true, new Bpl.ExprSeq(new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.Subtype), new Bpl.ExprSeq(callToG3, Bpl.Expr.Ident(boundTypeVar)))));

+      var forall = new Bpl.ForallExpr(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), qvars, null, trigger, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Iff, lhs, rhs));

+      this.TranslatedProgram.TopLevelDeclarations.Add(new Bpl.Axiom(Bpl.Token.NoToken, forall));

+    }

+

     private void DeclareParents(ITypeDefinition typeDefinition, Bpl.Function typeDefinitionAsBplFunction) {

       foreach (var p in typeDefinition.BaseClasses) {

         DeclareSuperType(typeDefinitionAsBplFunction, p);