Skip to content

Commit 124d1ce

Browse files
shazqadeershazqadeer
authored
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.
1 parent 5dc369b commit 124d1ce

File tree

145 files changed

+250
-615
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

145 files changed

+250
-615
lines changed

‎Source/Core/CommandLineOptions.cs

-6
Original file line numberDiff line numberDiff line change
@@ -792,7 +792,6 @@ public enum FixedPointInferenceMode {
792792
public bool ExtractLoopsUnrollIrreducible = true; // unroll irreducible loops? (set programmatically)
793793

794794
public enum TypeEncoding {
795-
None,
796795
Predicates,
797796
Arguments,
798797
Monomorphic
@@ -1388,10 +1387,6 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
13881387
case "typeEncoding":
13891388
if (ps.ConfirmArgumentCount(1)) {
13901389
switch (args[ps.i]) {
1391-
case "n":
1392-
case "none":
1393-
TypeEncodingMethod = TypeEncoding.None;
1394-
break;
13951390
case "p":
13961391
case "predicates":
13971392
TypeEncodingMethod = TypeEncoding.Predicates;
@@ -2098,7 +2093,6 @@ on stratified inlining.
20982093
Translate Boogie's A ==> B into prover's A ==> A && B.
20992094
/typeEncoding:<m>
21002095
how to encode types when sending VC to theorem prover
2101-
n = none (unsound)
21022096
p = predicates (default)
21032097
a = arguments
21042098
m = monomorphic

‎Source/VCExpr/TypeErasure.cs

+1-7
Original file line numberDiff line numberDiff line change
@@ -197,10 +197,7 @@ public VCExpr GetNewAxioms() {
197197
private VCExpr GenCtorAssignment(VCExpr typeRepr) {
198198
Contract.Requires(typeRepr != null);
199199
Contract.Ensures(Contract.Result<VCExpr>() != null);
200-
if (CommandLineOptions.Clo.TypeEncodingMethod
201-
== CommandLineOptions.TypeEncoding.None)
202-
return VCExpressionGenerator.True;
203-
200+
204201
VCExpr res = Gen.Eq(Gen.Function(Ctor, typeRepr),
205202
Gen.Integer(CurrentCtorNum));
206203
CurrentCtorNum = CurrentCtorNum + BigNum.ONE;
@@ -210,9 +207,6 @@ private VCExpr GenCtorAssignment(VCExpr typeRepr) {
210207
private VCExpr GenCtorAssignment(Function typeRepr) {
211208
Contract.Requires(typeRepr != null);
212209
Contract.Ensures(Contract.Result<VCExpr>() != null);
213-
if (CommandLineOptions.Clo.TypeEncodingMethod
214-
== CommandLineOptions.TypeEncoding.None)
215-
return VCExpressionGenerator.True;
216210

217211
List<VCExprVar/*!*/>/*!*/ quantifiedVars = HelperFuns.GenVarsForInParams(typeRepr, Gen);
218212
VCExpr/*!*/ eq =

‎Source/VCExpr/TypeErasurePremisses.cs

+2-17
Original file line numberDiff line numberDiff line change
@@ -111,11 +111,7 @@ protected override VCExpr GenReverseCastAxiom(Function castToU, Function castFro
111111
Contract.Assert(var != null);
112112
Contract.Assert(eq != null);
113113
VCExpr/*!*/ premiss;
114-
if (CommandLineOptions.Clo.TypeEncodingMethod
115-
== CommandLineOptions.TypeEncoding.None)
116-
premiss = VCExpressionGenerator.True;
117-
else
118-
premiss = GenVarTypeAxiom(var, cce.NonNull(castFromU.OutParams[0]).TypedIdent.Type,
114+
premiss = GenVarTypeAxiom(var, cce.NonNull(castFromU.OutParams[0]).TypedIdent.Type,
119115
// we don't have any bindings available
120116
new Dictionary<TypeVariable/*!*/, VCExpr/*!*/>());
121117
VCExpr/*!*/ matrix = Gen.ImpliesSimp(premiss, eq);
@@ -436,10 +432,6 @@ private VCExpr GenFunctionAxiom(UntypedFunction fun, Function originalFun) {
436432
Contract.Requires(originalInTypes.Count + explicitTypeParams.Count == fun.InParams.Count);
437433
Contract.Ensures(Contract.Result<VCExpr>() != null);
438434

439-
if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) {
440-
return VCExpressionGenerator.True;
441-
}
442-
443435
List<VCExprVar/*!*/>/*!*/ typedInputVars = new List<VCExprVar/*!*/>(originalInTypes.Count);
444436
int i = 0;
445437
foreach (Type/*!*/ t in originalInTypes) {
@@ -501,7 +493,6 @@ private VCExpr GenFunctionAxiom(UntypedFunction fun, Function originalFun) {
501493
protected override void AddVarTypeAxiom(VCExprVar var, Type originalType) {
502494
//Contract.Requires(originalType != null);
503495
//Contract.Requires(var != null);
504-
if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) return;
505496
AddTypeAxiom(GenVarTypeAxiom(var, originalType,
506497
// we don't have any bindings available
507498
new Dictionary<TypeVariable/*!*/, VCExpr/*!*/>()));
@@ -841,8 +832,7 @@ private VCExpr GenMapAxiom0(Function select, Function store, Type mapResult, Lis
841832
AxBuilderPremisses.Type2Term(mapResult, bindings.TypeVariableBindings));
842833
Contract.Assert(ante != null);
843834
VCExpr body;
844-
if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None ||
845-
!AxBuilder.U.Equals(cce.NonNull(select.OutParams[0]).TypedIdent.Type)) {
835+
if (!AxBuilder.U.Equals(cce.NonNull(select.OutParams[0]).TypedIdent.Type)) {
846836
body = Gen.Let(letBindings_Explicit, eq);
847837
} else {
848838
body = Gen.Let(letBindings_Implicit, Gen.Let(letBindings_Explicit, Gen.ImpliesSimp(ante, eq)));
@@ -1152,11 +1142,6 @@ private VCExpr HandleQuantifier(VCExprQuantifier node, List<VCExprVar/*!*/>/*!*/
11521142

11531143
// assemble the new quantified formula
11541144

1155-
if (CommandLineOptions.Clo.TypeEncodingMethod
1156-
== CommandLineOptions.TypeEncoding.None) {
1157-
typePremisses = VCExpressionGenerator.True;
1158-
}
1159-
11601145
VCExpr/*!*/ bodyWithPremisses =
11611146
AxBuilderPremisses.AddTypePremisses(typeVarBindings, typePremisses,
11621147
node.Quan == Quantifier.ALL,

‎Test/test21/BooleanQuantification.bpl

+1-3
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
2-
// RUN: %diff "%s.n.expect" "%t"
31
// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
42
// RUN: %diff "%s.p.expect" "%t"
53
// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
@@ -35,4 +33,4 @@ procedure S() returns () {
3533
assert (forall x:bool :: g(x) >= 0);
3634
assert g((forall x:bool :: g(x) >= 0)) >= 17;
3735
assert (forall x:bool :: f(x) == g(x)); // should not be provable
38-
}
36+
}

‎Test/test21/BooleanQuantification.bpl.a.expect

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
BooleanQuantification.bpl(25,3): Error BP5001: This assertion might not hold.
1+
BooleanQuantification.bpl(23,3): Error BP5001: This assertion might not hold.
22
Execution trace:
3-
BooleanQuantification.bpl(24,3): anon0
4-
BooleanQuantification.bpl(37,3): Error BP5001: This assertion might not hold.
3+
BooleanQuantification.bpl(22,3): anon0
4+
BooleanQuantification.bpl(35,3): Error BP5001: This assertion might not hold.
55
Execution trace:
6-
BooleanQuantification.bpl(35,3): anon0
6+
BooleanQuantification.bpl(33,3): anon0
77

88
Boogie program verifier finished with 2 verified, 2 errors

‎Test/test21/BooleanQuantification.bpl.n.expect

-8
This file was deleted.

‎Test/test21/BooleanQuantification.bpl.p.expect

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
BooleanQuantification.bpl(25,3): Error BP5001: This assertion might not hold.
1+
BooleanQuantification.bpl(23,3): Error BP5001: This assertion might not hold.
22
Execution trace:
3-
BooleanQuantification.bpl(24,3): anon0
4-
BooleanQuantification.bpl(37,3): Error BP5001: This assertion might not hold.
3+
BooleanQuantification.bpl(22,3): anon0
4+
BooleanQuantification.bpl(35,3): Error BP5001: This assertion might not hold.
55
Execution trace:
6-
BooleanQuantification.bpl(35,3): anon0
6+
BooleanQuantification.bpl(33,3): anon0
77

88
Boogie program verifier finished with 2 verified, 2 errors

‎Test/test21/BooleanQuantification2.bpl

+1-3
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
2-
// RUN: %diff "%s.n.expect" "%t"
31
// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
42
// RUN: %diff "%s.p.expect" "%t"
53
// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
@@ -17,4 +15,4 @@ procedure P() returns () {
1715
assert j || !j;
1816

1917
assert false;
20-
}
18+
}

‎Test/test21/BooleanQuantification2.bpl.a.expect

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
BooleanQuantification2.bpl(19,3): Error BP5001: This assertion might not hold.
1+
BooleanQuantification2.bpl(17,3): Error BP5001: This assertion might not hold.
22
Execution trace:
3-
BooleanQuantification2.bpl(16,3): anon0
3+
BooleanQuantification2.bpl(14,3): anon0
44

55
Boogie program verifier finished with 0 verified, 1 error

‎Test/test21/BooleanQuantification2.bpl.n.expect

-5
This file was deleted.

‎Test/test21/BooleanQuantification2.bpl.p.expect

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
BooleanQuantification2.bpl(19,3): Error BP5001: This assertion might not hold.
1+
BooleanQuantification2.bpl(17,3): Error BP5001: This assertion might not hold.
22
Execution trace:
3-
BooleanQuantification2.bpl(16,3): anon0
3+
BooleanQuantification2.bpl(14,3): anon0
44

55
Boogie program verifier finished with 0 verified, 1 error

‎Test/test21/Boxing.bpl

+1-3
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
2-
// RUN: %diff "%s.n.expect" "%t"
31
// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
42
// RUN: %diff "%s.p.expect" "%t"
53
// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
@@ -24,4 +22,4 @@ procedure P() returns ()
2422

2523
assert unbox(b1) == 13 && unbox(b2) == true && unbox(unbox(b3)) == 13;
2624
assert unbox(b1) == true; // error
27-
}
25+
}

‎Test/test21/Boxing.bpl.a.expect

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
Boxing.bpl(26,3): Error BP5001: This assertion might not hold.
1+
Boxing.bpl(24,3): Error BP5001: This assertion might not hold.
22
Execution trace:
3-
Boxing.bpl(21,6): anon0
3+
Boxing.bpl(19,6): anon0
44

55
Boogie program verifier finished with 0 verified, 1 error

‎Test/test21/Boxing.bpl.n.expect

-8
This file was deleted.

‎Test/test21/Boxing.bpl.p.expect

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
Boxing.bpl(26,3): Error BP5001: This assertion might not hold.
1+
Boxing.bpl(24,3): Error BP5001: This assertion might not hold.
22
Execution trace:
3-
Boxing.bpl(21,6): anon0
3+
Boxing.bpl(19,6): anon0
44

55
Boogie program verifier finished with 0 verified, 1 error

‎Test/test21/Casts.bpl

+1-3
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
2-
// RUN: %diff "%s.n.expect" "%t"
31
// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
42
// RUN: %diff "%s.p.expect" "%t"
53
// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
@@ -14,4 +12,4 @@ procedure P() returns () {
1412

1513
assert n[m[x]] == 1;
1614
assert m[n[x]] == 1; // should not be provable
17-
}
15+
}

‎Test/test21/Casts.bpl.a.expect

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
Casts.bpl(16,3): Error BP5001: This assertion might not hold.
1+
Casts.bpl(14,3): Error BP5001: This assertion might not hold.
22
Execution trace:
3-
Casts.bpl(12,3): anon0
3+
Casts.bpl(10,3): anon0
44

55
Boogie program verifier finished with 0 verified, 1 error

‎Test/test21/Casts.bpl.n.expect

-5
This file was deleted.

‎Test/test21/Casts.bpl.p.expect

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
Casts.bpl(16,3): Error BP5001: This assertion might not hold.
1+
Casts.bpl(14,3): Error BP5001: This assertion might not hold.
22
Execution trace:
3-
Casts.bpl(12,3): anon0
3+
Casts.bpl(10,3): anon0
44

55
Boogie program verifier finished with 0 verified, 1 error

‎Test/test21/Coercions2.bpl

+1-3
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
2-
// RUN: %diff "%s.n.expect" "%t"
31
// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
42
// RUN: %diff "%s.p.expect" "%t"
53
// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
@@ -27,4 +25,4 @@ procedure P() {
2725
assert b == box(i);
2826

2927
assert false;
30-
}
28+
}

‎Test/test21/Coercions2.bpl.a.expect

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
Coercions2.bpl(18,23): Warning: type parameter a is ambiguous, instantiating to int
2-
Coercions2.bpl(29,3): Error BP5001: This assertion might not hold.
1+
Coercions2.bpl(16,23): Warning: type parameter a is ambiguous, instantiating to int
2+
Coercions2.bpl(27,3): Error BP5001: This assertion might not hold.
33
Execution trace:
4-
Coercions2.bpl(24,3): anon0
4+
Coercions2.bpl(22,3): anon0
55

66
Boogie program verifier finished with 0 verified, 1 error

‎Test/test21/Coercions2.bpl.n.expect

-9
This file was deleted.

‎Test/test21/Coercions2.bpl.p.expect

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
Coercions2.bpl(18,23): Warning: type parameter a is ambiguous, instantiating to int
2-
Coercions2.bpl(29,3): Error BP5001: This assertion might not hold.
1+
Coercions2.bpl(16,23): Warning: type parameter a is ambiguous, instantiating to int
2+
Coercions2.bpl(27,3): Error BP5001: This assertion might not hold.
33
Execution trace:
4-
Coercions2.bpl(24,3): anon0
4+
Coercions2.bpl(22,3): anon0
55

66
Boogie program verifier finished with 0 verified, 1 error

‎Test/test21/Colors.bpl

+1-3
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
2-
// RUN: %diff "%s.n.expect" "%t"
31
// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
42
// RUN: %diff "%s.p.expect" "%t"
53
// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
@@ -24,4 +22,4 @@ procedure Q() returns () {
2422

2523
assume x != Blue && x != Green;
2624
assert x == Red;
27-
}
25+
}

‎Test/test21/Colors.bpl.a.expect

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
Colors.bpl(19,3): Error BP5001: This assertion might not hold.
1+
Colors.bpl(17,3): Error BP5001: This assertion might not hold.
22
Execution trace:
3-
Colors.bpl(18,3): anon0
4-
Colors.bpl(26,3): Error BP5001: This assertion might not hold.
3+
Colors.bpl(16,3): anon0
4+
Colors.bpl(24,3): Error BP5001: This assertion might not hold.
55
Execution trace:
6-
Colors.bpl(25,3): anon0
6+
Colors.bpl(23,3): anon0
77

88
Boogie program verifier finished with 0 verified, 2 errors

‎Test/test21/Colors.bpl.n.expect

-8
This file was deleted.

‎Test/test21/Colors.bpl.p.expect

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
Colors.bpl(19,3): Error BP5001: This assertion might not hold.
1+
Colors.bpl(17,3): Error BP5001: This assertion might not hold.
22
Execution trace:
3-
Colors.bpl(18,3): anon0
4-
Colors.bpl(26,3): Error BP5001: This assertion might not hold.
3+
Colors.bpl(16,3): anon0
4+
Colors.bpl(24,3): Error BP5001: This assertion might not hold.
55
Execution trace:
6-
Colors.bpl(25,3): anon0
6+
Colors.bpl(23,3): anon0
77

88
Boogie program verifier finished with 0 verified, 2 errors

‎Test/test21/DisjointDomains.bpl

-2
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
2-
// RUN: %diff "%s.n.expect" "%t"
31
// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
42
// RUN: %diff "%s.p.expect" "%t"
53
// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

‎Test/test21/DisjointDomains.bpl.a.expect

+6-6
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
1-
DisjointDomains.bpl(20,5): Error BP5001: This assertion might not hold.
1+
DisjointDomains.bpl(18,5): Error BP5001: This assertion might not hold.
22
Execution trace:
3-
DisjointDomains.bpl(17,3): start
4-
DisjointDomains.bpl(27,5): Error BP5001: This assertion might not hold.
3+
DisjointDomains.bpl(15,3): start
4+
DisjointDomains.bpl(25,5): Error BP5001: This assertion might not hold.
55
Execution trace:
6-
DisjointDomains.bpl(26,3): start
7-
DisjointDomains.bpl(33,5): Error BP5001: This assertion might not hold.
6+
DisjointDomains.bpl(24,3): start
7+
DisjointDomains.bpl(31,5): Error BP5001: This assertion might not hold.
88
Execution trace:
9-
DisjointDomains.bpl(32,3): start
9+
DisjointDomains.bpl(30,3): start
1010

1111
Boogie program verifier finished with 0 verified, 3 errors

‎Test/test21/DisjointDomains.bpl.n.expect

-2
This file was deleted.

‎Test/test21/DisjointDomains.bpl.p.expect

+6-6
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
1-
DisjointDomains.bpl(20,5): Error BP5001: This assertion might not hold.
1+
DisjointDomains.bpl(18,5): Error BP5001: This assertion might not hold.
22
Execution trace:
3-
DisjointDomains.bpl(17,3): start
4-
DisjointDomains.bpl(27,5): Error BP5001: This assertion might not hold.
3+
DisjointDomains.bpl(15,3): start
4+
DisjointDomains.bpl(25,5): Error BP5001: This assertion might not hold.
55
Execution trace:
6-
DisjointDomains.bpl(26,3): start
7-
DisjointDomains.bpl(33,5): Error BP5001: This assertion might not hold.
6+
DisjointDomains.bpl(24,3): start
7+
DisjointDomains.bpl(31,5): Error BP5001: This assertion might not hold.
88
Execution trace:
9-
DisjointDomains.bpl(32,3): start
9+
DisjointDomains.bpl(30,3): start
1010

1111
Boogie program verifier finished with 0 verified, 3 errors

0 commit comments

Comments
 (0)