Remove typeEncoding:n (#194)

The typeEncoding:n option is unsound, as indicated in its documentation. It also does not appear to be used. This commit eliminates the /typeEncoding:n option.

Source/Core/CommandLineOptions.cs

@@ -792,7 +792,6 @@ public enum FixedPointInferenceMode {
     public bool ExtractLoopsUnrollIrreducible = true; // unroll irreducible loops? (set programmatically)
 
     public enum TypeEncoding {
-      None,
       Predicates,
       Arguments,
       Monomorphic
@@ -1388,10 +1387,6 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
         case "typeEncoding":
           if (ps.ConfirmArgumentCount(1)) {
             switch (args[ps.i]) {
-              case "n":
-              case "none":
-                TypeEncodingMethod = TypeEncoding.None;
-                break;
               case "p":
               case "predicates":
                 TypeEncodingMethod = TypeEncoding.Predicates;
@@ -2098,7 +2093,6 @@ on stratified inlining.
                 Translate Boogie's A ==> B into prover's A ==> A && B.
   /typeEncoding:<m>
                 how to encode types when sending VC to theorem prover
-                   n = none (unsound)
                    p = predicates (default)
                    a = arguments
                    m = monomorphic

Source/VCExpr/TypeErasure.cs

@@ -197,10 +197,7 @@ public VCExpr GetNewAxioms() {
     private VCExpr GenCtorAssignment(VCExpr typeRepr) {
       Contract.Requires(typeRepr != null);
       Contract.Ensures(Contract.Result<VCExpr>() != null);
-      if (CommandLineOptions.Clo.TypeEncodingMethod
-                == CommandLineOptions.TypeEncoding.None)
-        return VCExpressionGenerator.True;
-
+
       VCExpr res = Gen.Eq(Gen.Function(Ctor, typeRepr),
                            Gen.Integer(CurrentCtorNum));
       CurrentCtorNum = CurrentCtorNum + BigNum.ONE;
@@ -210,9 +207,6 @@ private VCExpr GenCtorAssignment(VCExpr typeRepr) {
     private VCExpr GenCtorAssignment(Function typeRepr) {
       Contract.Requires(typeRepr != null);
       Contract.Ensures(Contract.Result<VCExpr>() != null);
-      if (CommandLineOptions.Clo.TypeEncodingMethod
-                == CommandLineOptions.TypeEncoding.None)
-        return VCExpressionGenerator.True;
 
       List<VCExprVar/*!*/>/*!*/ quantifiedVars = HelperFuns.GenVarsForInParams(typeRepr, Gen);
       VCExpr/*!*/ eq =

Source/VCExpr/TypeErasurePremisses.cs

@@ -111,11 +111,7 @@ protected override VCExpr GenReverseCastAxiom(Function castToU, Function castFro
       Contract.Assert(var != null);
       Contract.Assert(eq != null);
       VCExpr/*!*/ premiss;
-      if (CommandLineOptions.Clo.TypeEncodingMethod
-              == CommandLineOptions.TypeEncoding.None)
-        premiss = VCExpressionGenerator.True;
-      else
-        premiss = GenVarTypeAxiom(var, cce.NonNull(castFromU.OutParams[0]).TypedIdent.Type,
+      premiss = GenVarTypeAxiom(var, cce.NonNull(castFromU.OutParams[0]).TypedIdent.Type,
           // we don't have any bindings available
                                   new Dictionary<TypeVariable/*!*/, VCExpr/*!*/>());
       VCExpr/*!*/ matrix = Gen.ImpliesSimp(premiss, eq);
@@ -436,10 +432,6 @@ private VCExpr GenFunctionAxiom(UntypedFunction fun, Function originalFun) {
       Contract.Requires(originalInTypes.Count + explicitTypeParams.Count == fun.InParams.Count);
       Contract.Ensures(Contract.Result<VCExpr>() != null);
 
-      if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) {
-        return VCExpressionGenerator.True;
-      }
-
       List<VCExprVar/*!*/>/*!*/ typedInputVars = new List<VCExprVar/*!*/>(originalInTypes.Count);
       int i = 0;
       foreach (Type/*!*/ t in originalInTypes) {
@@ -501,7 +493,6 @@ private VCExpr GenFunctionAxiom(UntypedFunction fun, Function originalFun) {
     protected override void AddVarTypeAxiom(VCExprVar var, Type originalType) {
       //Contract.Requires(originalType != null);
       //Contract.Requires(var != null);
-      if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) return;
       AddTypeAxiom(GenVarTypeAxiom(var, originalType,
         // we don't have any bindings available
                                    new Dictionary<TypeVariable/*!*/, VCExpr/*!*/>()));
@@ -841,8 +832,7 @@ private VCExpr GenMapAxiom0(Function select, Function store, Type mapResult, Lis
         AxBuilderPremisses.Type2Term(mapResult, bindings.TypeVariableBindings));
       Contract.Assert(ante != null);
       VCExpr body;
-      if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None ||
-          !AxBuilder.U.Equals(cce.NonNull(select.OutParams[0]).TypedIdent.Type)) {
+      if (!AxBuilder.U.Equals(cce.NonNull(select.OutParams[0]).TypedIdent.Type)) {
         body = Gen.Let(letBindings_Explicit, eq);
       } else {
         body = Gen.Let(letBindings_Implicit, Gen.Let(letBindings_Explicit, Gen.ImpliesSimp(ante, eq)));
@@ -1152,11 +1142,6 @@ private VCExpr HandleQuantifier(VCExprQuantifier node, List<VCExprVar/*!*/>/*!*/
 
       // assemble the new quantified formula
 
-      if (CommandLineOptions.Clo.TypeEncodingMethod
-                == CommandLineOptions.TypeEncoding.None) {
-        typePremisses = VCExpressionGenerator.True;
-      }
-
       VCExpr/*!*/ bodyWithPremisses =
         AxBuilderPremisses.AddTypePremisses(typeVarBindings, typePremisses,
                                             node.Quan == Quantifier.ALL,

Test/test21/BooleanQuantification.bpl

@@ -1,5 +1,3 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
-// RUN: %diff "%s.n.expect" "%t"
 // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
 // RUN: %diff "%s.p.expect" "%t"
 // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
@@ -35,4 +33,4 @@ procedure S() returns () {
   assert (forall x:bool :: g(x) >= 0);
   assert g((forall x:bool :: g(x) >= 0)) >= 17;
   assert (forall x:bool :: f(x) == g(x));   // should not be provable
-}
+}

Test/test21/BooleanQuantification.bpl.a.expect

@@ -1,8 +1,8 @@
-BooleanQuantification.bpl(25,3): Error BP5001: This assertion might not hold.
+BooleanQuantification.bpl(23,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    BooleanQuantification.bpl(24,3): anon0
-BooleanQuantification.bpl(37,3): Error BP5001: This assertion might not hold.
+    BooleanQuantification.bpl(22,3): anon0
+BooleanQuantification.bpl(35,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    BooleanQuantification.bpl(35,3): anon0
+    BooleanQuantification.bpl(33,3): anon0
 
 Boogie program verifier finished with 2 verified, 2 errors

Test/test21/BooleanQuantification.bpl.p.expect

@@ -1,8 +1,8 @@
-BooleanQuantification.bpl(25,3): Error BP5001: This assertion might not hold.
+BooleanQuantification.bpl(23,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    BooleanQuantification.bpl(24,3): anon0
-BooleanQuantification.bpl(37,3): Error BP5001: This assertion might not hold.
+    BooleanQuantification.bpl(22,3): anon0
+BooleanQuantification.bpl(35,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    BooleanQuantification.bpl(35,3): anon0
+    BooleanQuantification.bpl(33,3): anon0
 
 Boogie program verifier finished with 2 verified, 2 errors

Test/test21/BooleanQuantification2.bpl

@@ -1,5 +1,3 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
-// RUN: %diff "%s.n.expect" "%t"
 // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
 // RUN: %diff "%s.p.expect" "%t"
 // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
@@ -17,4 +15,4 @@ procedure P() returns () {
   assert j || !j;
 
   assert false;
-}
+}

Test/test21/BooleanQuantification2.bpl.a.expect

@@ -1,5 +1,5 @@
-BooleanQuantification2.bpl(19,3): Error BP5001: This assertion might not hold.
+BooleanQuantification2.bpl(17,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    BooleanQuantification2.bpl(16,3): anon0
+    BooleanQuantification2.bpl(14,3): anon0
 
 Boogie program verifier finished with 0 verified, 1 error

Test/test21/BooleanQuantification2.bpl.p.expect

@@ -1,5 +1,5 @@
-BooleanQuantification2.bpl(19,3): Error BP5001: This assertion might not hold.
+BooleanQuantification2.bpl(17,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    BooleanQuantification2.bpl(16,3): anon0
+    BooleanQuantification2.bpl(14,3): anon0
 
 Boogie program verifier finished with 0 verified, 1 error

Test/test21/Boxing.bpl

@@ -1,5 +1,3 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
-// RUN: %diff "%s.n.expect" "%t"
 // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
 // RUN: %diff "%s.p.expect" "%t"
 // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
@@ -24,4 +22,4 @@ procedure P() returns ()
 
   assert unbox(b1) == 13 && unbox(b2) == true && unbox(unbox(b3)) == 13;
   assert unbox(b1) == true;    // error
-}
+}

Test/test21/Boxing.bpl.a.expect

@@ -1,5 +1,5 @@
-Boxing.bpl(26,3): Error BP5001: This assertion might not hold.
+Boxing.bpl(24,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Boxing.bpl(21,6): anon0
+    Boxing.bpl(19,6): anon0
 
 Boogie program verifier finished with 0 verified, 1 error

Test/test21/Boxing.bpl.p.expect

@@ -1,5 +1,5 @@
-Boxing.bpl(26,3): Error BP5001: This assertion might not hold.
+Boxing.bpl(24,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Boxing.bpl(21,6): anon0
+    Boxing.bpl(19,6): anon0
 
 Boogie program verifier finished with 0 verified, 1 error

Test/test21/Casts.bpl

@@ -1,5 +1,3 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
-// RUN: %diff "%s.n.expect" "%t"
 // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
 // RUN: %diff "%s.p.expect" "%t"
 // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
@@ -14,4 +12,4 @@ procedure P() returns () {
 
   assert n[m[x]] == 1;
   assert m[n[x]] == 1;    // should not be provable
-}
+}

Test/test21/Casts.bpl.a.expect

@@ -1,5 +1,5 @@
-Casts.bpl(16,3): Error BP5001: This assertion might not hold.
+Casts.bpl(14,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Casts.bpl(12,3): anon0
+    Casts.bpl(10,3): anon0
 
 Boogie program verifier finished with 0 verified, 1 error

Test/test21/Casts.bpl.p.expect

@@ -1,5 +1,5 @@
-Casts.bpl(16,3): Error BP5001: This assertion might not hold.
+Casts.bpl(14,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Casts.bpl(12,3): anon0
+    Casts.bpl(10,3): anon0
 
 Boogie program verifier finished with 0 verified, 1 error

Test/test21/Coercions2.bpl

@@ -1,5 +1,3 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
-// RUN: %diff "%s.n.expect" "%t"
 // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
 // RUN: %diff "%s.p.expect" "%t"
 // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
@@ -27,4 +25,4 @@ procedure P() {
   assert b == box(i);
 
   assert false;
-}
+}

Test/test21/Coercions2.bpl.a.expect

@@ -1,6 +1,6 @@
-Coercions2.bpl(18,23): Warning: type parameter a is ambiguous, instantiating to int
-Coercions2.bpl(29,3): Error BP5001: This assertion might not hold.
+Coercions2.bpl(16,23): Warning: type parameter a is ambiguous, instantiating to int
+Coercions2.bpl(27,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Coercions2.bpl(24,3): anon0
+    Coercions2.bpl(22,3): anon0
 
 Boogie program verifier finished with 0 verified, 1 error

Test/test21/Coercions2.bpl.p.expect

@@ -1,6 +1,6 @@
-Coercions2.bpl(18,23): Warning: type parameter a is ambiguous, instantiating to int
-Coercions2.bpl(29,3): Error BP5001: This assertion might not hold.
+Coercions2.bpl(16,23): Warning: type parameter a is ambiguous, instantiating to int
+Coercions2.bpl(27,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Coercions2.bpl(24,3): anon0
+    Coercions2.bpl(22,3): anon0
 
 Boogie program verifier finished with 0 verified, 1 error

Test/test21/Colors.bpl

@@ -1,5 +1,3 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
-// RUN: %diff "%s.n.expect" "%t"
 // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
 // RUN: %diff "%s.p.expect" "%t"
 // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
@@ -24,4 +22,4 @@ procedure Q() returns () {
 
   assume x != Blue && x != Green;
   assert x == Red;
-}
+}

Test/test21/Colors.bpl.a.expect

@@ -1,8 +1,8 @@
-Colors.bpl(19,3): Error BP5001: This assertion might not hold.
+Colors.bpl(17,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Colors.bpl(18,3): anon0
-Colors.bpl(26,3): Error BP5001: This assertion might not hold.
+    Colors.bpl(16,3): anon0
+Colors.bpl(24,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Colors.bpl(25,3): anon0
+    Colors.bpl(23,3): anon0
 
 Boogie program verifier finished with 0 verified, 2 errors

Test/test21/Colors.bpl.p.expect

@@ -1,8 +1,8 @@
-Colors.bpl(19,3): Error BP5001: This assertion might not hold.
+Colors.bpl(17,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Colors.bpl(18,3): anon0
-Colors.bpl(26,3): Error BP5001: This assertion might not hold.
+    Colors.bpl(16,3): anon0
+Colors.bpl(24,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Colors.bpl(25,3): anon0
+    Colors.bpl(23,3): anon0
 
 Boogie program verifier finished with 0 verified, 2 errors

Test/test21/DisjointDomains.bpl

@@ -1,5 +1,3 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
-// RUN: %diff "%s.n.expect" "%t"
 // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
 // RUN: %diff "%s.p.expect" "%t"
 // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

Test/test21/DisjointDomains.bpl.a.expect

@@ -1,11 +1,11 @@
-DisjointDomains.bpl(20,5): Error BP5001: This assertion might not hold.
+DisjointDomains.bpl(18,5): Error BP5001: This assertion might not hold.
 Execution trace:
-    DisjointDomains.bpl(17,3): start
-DisjointDomains.bpl(27,5): Error BP5001: This assertion might not hold.
+    DisjointDomains.bpl(15,3): start
+DisjointDomains.bpl(25,5): Error BP5001: This assertion might not hold.
 Execution trace:
-    DisjointDomains.bpl(26,3): start
-DisjointDomains.bpl(33,5): Error BP5001: This assertion might not hold.
+    DisjointDomains.bpl(24,3): start
+DisjointDomains.bpl(31,5): Error BP5001: This assertion might not hold.
 Execution trace:
-    DisjointDomains.bpl(32,3): start
+    DisjointDomains.bpl(30,3): start
 
 Boogie program verifier finished with 0 verified, 3 errors

Test/test21/DisjointDomains.bpl.p.expect

@@ -1,11 +1,11 @@
-DisjointDomains.bpl(20,5): Error BP5001: This assertion might not hold.
+DisjointDomains.bpl(18,5): Error BP5001: This assertion might not hold.
 Execution trace:
-    DisjointDomains.bpl(17,3): start
-DisjointDomains.bpl(27,5): Error BP5001: This assertion might not hold.
+    DisjointDomains.bpl(15,3): start
+DisjointDomains.bpl(25,5): Error BP5001: This assertion might not hold.
 Execution trace:
-    DisjointDomains.bpl(26,3): start
-DisjointDomains.bpl(33,5): Error BP5001: This assertion might not hold.
+    DisjointDomains.bpl(24,3): start
+DisjointDomains.bpl(31,5): Error BP5001: This assertion might not hold.
 Execution trace:
-    DisjointDomains.bpl(32,3): start
+    DisjointDomains.bpl(30,3): start
 
 Boogie program verifier finished with 0 verified, 3 errors