diff options
| -rw-r--r-- | Source/AIFramework/Polyhedra/LinearConstraintSystem.cs | 3 | ||||
| -rw-r--r-- | Source/AIFramework/Polyhedra/SimplexTableau.cs | 1 | ||||
| -rw-r--r-- | Source/Basetypes/BigNum.cs | 1 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 7 | ||||
| -rw-r--r-- | Source/Provers/Simplify/ProverInterface.cs | 4 | ||||
| -rw-r--r-- | Source/Provers/Z3/Prover.cs | 7 | ||||
| -rw-r--r-- | Source/Provers/Z3/ProverInterface.cs | 4 | ||||
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 22 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasure.cs | 21 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasurePremisses.cs | 382 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprAST.cs | 9 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 118 | ||||
| -rw-r--r-- | Source/VCGeneration/Context.cs | 7 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 27 | ||||
| -rw-r--r-- | Test/test15/Answer | 21 |
15 files changed, 379 insertions, 255 deletions
diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs index c259febe..b6ce193a 100644 --- a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs +++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs @@ -156,7 +156,6 @@ namespace Microsoft.AbstractInterpretationFramework { FrameVertices = null;
FrameRays = null;
FrameLines = null;
- IMutableSet ss;
FrameDimensions.Clear(); // no implicit lines
}
@@ -672,7 +671,7 @@ namespace Microsoft.AbstractInterpretationFramework { CHECK_NEXT_CONSTRAINT: {
}
#if DEBUG_PRINT
- Console.WriteLine("Widen checking: done with that constraint"); + Console.WriteLine("Widen checking: done with that constraint");
#endif
}
diff --git a/Source/AIFramework/Polyhedra/SimplexTableau.cs b/Source/AIFramework/Polyhedra/SimplexTableau.cs index 4b5eaf43..4c37e980 100644 --- a/Source/AIFramework/Polyhedra/SimplexTableau.cs +++ b/Source/AIFramework/Polyhedra/SimplexTableau.cs @@ -364,7 +364,6 @@ namespace Microsoft.AbstractInterpretationFramework { START_ANEW:
;
}
- return false; // make compiler shut up
}
}
diff --git a/Source/Basetypes/BigNum.cs b/Source/Basetypes/BigNum.cs index f5299f47..2e56fd1a 100644 --- a/Source/Basetypes/BigNum.cs +++ b/Source/Basetypes/BigNum.cs @@ -277,7 +277,6 @@ namespace Microsoft.Basetypes { }
}
}
- return ZERO; // make compiler shut up
}
////////////////////////////////////////////////////////////////////////////
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 398382a8..39f69ccc 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -3611,11 +3611,8 @@ namespace Microsoft.Boogie { return new Sequential(new AtomicRE(b), second);
}
} else {
- {
- Contract.Assume(false);
- throw new cce.UnreachableException();
- }
- return new AtomicRE(b);
+ Contract.Assume(false);
+ throw new cce.UnreachableException();
}
}
}
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs index 1f563c0f..1d7bdbb3 100644 --- a/Source/Provers/Simplify/ProverInterface.cs +++ b/Source/Provers/Simplify/ProverInterface.cs @@ -757,6 +757,10 @@ namespace Microsoft.Boogie.Simplify { //Contract.Requires(var != null);
Contract.Ensures(Contract.Result<string>() != null);
+ VCExprVar v = AxBuilder.TryTyped2Untyped(var);
+ if (v != null) {
+ var = v;
+ }
return Namer.Lookup(var);
}
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs index 4a16e6b6..33e622ba 100644 --- a/Source/Provers/Z3/Prover.cs +++ b/Source/Provers/Z3/Prover.cs @@ -597,13 +597,6 @@ namespace Microsoft.Boogie.Z3 int k = s.IndexOfAny(new char[] { ' ', '}' }, j);
Contract.Assume(j <= k);
string id = s.Substring(j, k - j);
-#if IS_THIS_A_GOOD_IDEA
- // remove any @@-suffix
- int doubleAt = id.IndexOf("@@");
- if (doubleAt != -1) {
- id = id.Substring(0, doubleAt);
- }
-#endif
j = k + 1;
Contract.Assume(!identifierToPartition.ContainsKey(id)); // an ID is listed only once in this list, and an ID can only belong to one ZID equivalence class
identifierToPartition.Add(id, zID);
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs index 9289b5b7..af9668d4 100644 --- a/Source/Provers/Z3/ProverInterface.cs +++ b/Source/Provers/Z3/ProverInterface.cs @@ -295,6 +295,10 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P. //Contract.Requires(var != null);
Contract.Ensures(Contract.Result<string>() != null);
+ VCExprVar v = AxBuilder.TryTyped2Untyped(var);
+ if (v != null) {
+ var = v;
+ }
return Namer.Lookup(var);
}
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index b90196e2..64239e42 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -277,6 +277,28 @@ namespace Microsoft.Boogie.VCExprAST { return cce.NonNull(res);
}
+ /// <summary>
+ /// Unlike LookupVariable, this method does not create a new variable mapping if none is
+ /// found. Instead, this method returns null in such cases. Also, this method does not
+ /// look for bound variables.
+ /// </summary>
+ /// <param name="boogieVar"></param>
+ /// <returns></returns>
+ public VCExprVar TryLookupVariable(Variable boogieVar) {
+ Contract.Requires(boogieVar != null);
+
+ VCExprVar res;
+ Formal fml = boogieVar as Formal;
+ if (fml != null && Formals.TryGetValue(fml, out res))
+ return cce.NonNull(res);
+
+ if (UnboundVariables.TryGetValue(boogieVar, out res)) {
+ return cce.NonNull(res);
+ }
+
+ return null; // not present
+ }
+
///////////////////////////////////////////////////////////////////////////////////
internal readonly VCGenerationOptions/*!*/ GenerationOptions;
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index a33ea631..20c946e5 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -424,8 +424,8 @@ namespace Microsoft.Boogie.TypeErasure { public VCExprVar Typed2Untyped(VCExprVar var) {
Contract.Requires(var != null);
Contract.Ensures(Contract.Result<VCExprVar>() != null);
- VCExprVar res;
- if (!Typed2UntypedVariables.TryGetValue(var, out res)) {
+ VCExprVar res = TryTyped2Untyped(var);
+ if (res == null) {
res = Gen.Variable(var.Name, TypeAfterErasure(var.Type));
Typed2UntypedVariables.Add(var, res);
AddVarTypeAxiom(res, var.Type);
@@ -433,6 +433,23 @@ namespace Microsoft.Boogie.TypeErasure { return cce.NonNull(res);
}
+ /// <summary>
+ /// This method is like Typed2Untyped, except in the case where the given variables
+ /// doesn't exist in the mapping. For that case, this method returns null whereas
+ /// Typed2Untyped creates a new variable that it adds to the mapping.
+ /// </summary>
+ /// <param name="var"></param>
+ /// <returns></returns>
+ public VCExprVar TryTyped2Untyped(VCExprVar var) {
+ Contract.Requires(var != null);
+ VCExprVar res;
+ if (Typed2UntypedVariables.TryGetValue(var, out res)) {
+ return res;
+ } else {
+ return null;
+ }
+ }
+
protected abstract void AddVarTypeAxiom(VCExprVar/*!*/ var, Type/*!*/ originalType);
///////////////////////////////////////////////////////////////////////////
diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs index 09794803..25aa8074 100644 --- a/Source/VCExpr/TypeErasurePremisses.cs +++ b/Source/VCExpr/TypeErasurePremisses.cs @@ -31,19 +31,19 @@ namespace Microsoft.Boogie.TypeErasure // type parameters (in the same order as they occur in the signature
// of the original function).
- internal struct UntypedFunction {
+ internal struct UntypedFunction
+ {
public readonly Function/*!*/ Fun;
// type parameters that can be extracted from the value parameters
public readonly List<TypeVariable/*!*/>/*!*/ ImplicitTypeParams;
// type parameters that have to be given explicitly
public readonly List<TypeVariable/*!*/>/*!*/ ExplicitTypeParams;
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(Fun != null);
+ void ObjectInvariant() {
+ Contract.Invariant(Fun != null);
Contract.Invariant(cce.NonNullElements(ImplicitTypeParams));
Contract.Invariant(cce.NonNullElements(ExplicitTypeParams));
-}
+ }
public UntypedFunction(Function/*!*/ fun,
@@ -58,7 +58,8 @@ void ObjectInvariant() }
}
- public class TypeAxiomBuilderPremisses : TypeAxiomBuilderIntBoolU {
+ public class TypeAxiomBuilderPremisses : TypeAxiomBuilderIntBoolU
+ {
public TypeAxiomBuilderPremisses(VCExpressionGenerator gen)
: base(gen) {
@@ -132,17 +133,23 @@ void ObjectInvariant() private MapTypeAbstractionBuilderPremisses MapTypeAbstracterAttr;
- internal override MapTypeAbstractionBuilder/*!*/ MapTypeAbstracter { get {Contract.Ensures(Contract.Result<MapTypeAbstractionBuilder>() != null);
+ internal override MapTypeAbstractionBuilder/*!*/ MapTypeAbstracter {
+ get {
+ Contract.Ensures(Contract.Result<MapTypeAbstractionBuilder>() != null);
- if (MapTypeAbstracterAttr == null)
- MapTypeAbstracterAttr = new MapTypeAbstractionBuilderPremisses (this, Gen);
- return MapTypeAbstracterAttr;
- } }
+ if (MapTypeAbstracterAttr == null)
+ MapTypeAbstracterAttr = new MapTypeAbstractionBuilderPremisses(this, Gen);
+ return MapTypeAbstracterAttr;
+ }
+ }
- internal MapTypeAbstractionBuilderPremisses/*!*/ MapTypeAbstracterPremisses { get {Contract.Ensures(Contract.Result<MapTypeAbstractionBuilderPremisses>() != null);
+ internal MapTypeAbstractionBuilderPremisses/*!*/ MapTypeAbstracterPremisses {
+ get {
+ Contract.Ensures(Contract.Result<MapTypeAbstractionBuilderPremisses>() != null);
- return (MapTypeAbstractionBuilderPremisses)MapTypeAbstracter;
- } }
+ return (MapTypeAbstractionBuilderPremisses)MapTypeAbstracter;
+ }
+ }
////////////////////////////////////////////////////////////////////////////
@@ -150,15 +157,14 @@ void ObjectInvariant() // the field is overwritten with its actual value in "Setup"
private Function/*!*/ TypeFunction;
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(TypeFunction != null);
-}
+ void ObjectInvariant() {
+ Contract.Invariant(TypeFunction != null);
+ }
- public VCExpr TypeOf(VCExpr expr){
-Contract.Requires(expr != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ public VCExpr TypeOf(VCExpr expr) {
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Gen.Function(TypeFunction, expr);
}
@@ -169,26 +175,28 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); public List<VCExprLetBinding/*!*/>/*!*/
GenTypeParamBindings(// the original bound variables and (implicit) type parameters
List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ oldBoundVars,
- // VariableBindings to which the translation
- // TypeVariable -> VCExprVar is added
+ // VariableBindings to which the translation
+ // TypeVariable -> VCExprVar is added
VariableBindings/*!*/ bindings,
bool addTypeVarsToBindings) {
Contract.Requires(typeParams != null);
Contract.Requires(cce.NonNullElements(oldBoundVars));
Contract.Requires(bindings != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprLetBinding>>()));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprLetBinding>>()));
// type variables are replaced with ordinary variables that are bound using a
// let-expression
if (addTypeVarsToBindings) {
- foreach (TypeVariable/*!*/ tvar in typeParams){Contract.Assert(tvar != null);
- bindings.TypeVariableBindings.Add(tvar, Gen.Variable(tvar.Name, T));}
+ foreach (TypeVariable/*!*/ tvar in typeParams) {
+ Contract.Assert(tvar != null);
+ bindings.TypeVariableBindings.Add(tvar, Gen.Variable(tvar.Name, T));
+ }
}
// extract the values of type variables from the term variables
- List<VCExprVar/*!*/>/*!*/ UtypedVars = new List<VCExprVar/*!*/> (oldBoundVars.Count);
- List<Type/*!*/>/*!*/ originalTypes = new List<Type/*!*/> (oldBoundVars.Count);
+ List<VCExprVar/*!*/>/*!*/ UtypedVars = new List<VCExprVar/*!*/>(oldBoundVars.Count);
+ List<Type/*!*/>/*!*/ originalTypes = new List<Type/*!*/>(oldBoundVars.Count);
foreach (VCExprVar var in oldBoundVars) {
VCExprVar/*!*/ newVar = bindings.VCExprVarBindings[var];
if (newVar.Type.Equals(U)) {
@@ -196,7 +204,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); originalTypes.Add(var.Type);
}
}
-
+
UtypedVars.TrimExcess();
originalTypes.TrimExcess();
@@ -206,7 +214,8 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); public VCExpr/*!*/ AddTypePremisses(List<VCExprLetBinding/*!*/>/*!*/ typeVarBindings,
VCExpr/*!*/ typePremisses, bool universal,
- VCExpr/*!*/ body) {Contract.Requires(cce.NonNullElements(typeVarBindings));
+ VCExpr/*!*/ body) {
+ Contract.Requires(cce.NonNullElements(typeVarBindings));
Contract.Requires(typePremisses != null);
Contract.Requires(body != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -217,7 +226,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); else
bodyWithPremisses = Gen.AndSimp(typePremisses, body);
- return Gen.Let(typeVarBindings, bodyWithPremisses);
+ return Gen.Let(typeVarBindings, bodyWithPremisses);
}
@@ -236,7 +245,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); Contract.Requires(bindings != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprLetBinding>>()));
- List<VCExprLetBinding/*!*/>/*!*/ typeParamBindings = new List<VCExprLetBinding/*!*/> ();
+ List<VCExprLetBinding/*!*/>/*!*/ typeParamBindings = new List<VCExprLetBinding/*!*/>();
foreach (TypeVariable/*!*/ var in vars) {
Contract.Assert(var != null);
VCExpr extractor = BestTypeVarExtractor(var, types, concreteTypeSources);
@@ -249,7 +258,8 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); }
private VCExpr BestTypeVarExtractor(TypeVariable/*!*/ var, List<Type/*!*/>/*!*/ types,
- List<VCExprVar/*!*/>/*!*/ concreteTypeSources) {Contract.Requires(var != null);
+ List<VCExprVar/*!*/>/*!*/ concreteTypeSources) {
+ Contract.Requires(var != null);
Contract.Requires(cce.NonNullElements(types));
Contract.Requires(cce.NonNullElements(concreteTypeSources));
List<VCExpr/*!*/> allExtractors = TypeVarExtractors(var, types, concreteTypeSources);
@@ -271,13 +281,12 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); }
private List<VCExpr/*!*/>/*!*/ TypeVarExtractors(TypeVariable/*!*/ var, List<Type/*!*/>/*!*/ types,
- List<VCExprVar/*!*/>/*!*/ concreteTypeSources)
- {
+ List<VCExprVar/*!*/>/*!*/ concreteTypeSources) {
Contract.Requires(var != null);
Contract.Requires(cce.NonNullElements(types));
Contract.Requires(cce.NonNullElements(concreteTypeSources));
Contract.Requires((types.Count == concreteTypeSources.Count));
-Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/>();
for (int i = 0; i < types.Count; ++i)
TypeVarExtractors(var, types[i], TypeOf(concreteTypeSources[i]), res);
@@ -285,11 +294,11 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>())); return res;
}
- private void TypeVarExtractors(TypeVariable var, Type completeType, VCExpr innerTerm, List<VCExpr/*!*/>/*!*/ extractors){
-Contract.Requires(innerTerm != null);
-Contract.Requires(completeType != null);
-Contract.Requires(var != null);
-Contract.Requires(cce.NonNullElements(extractors));
+ private void TypeVarExtractors(TypeVariable var, Type completeType, VCExpr innerTerm, List<VCExpr/*!*/>/*!*/ extractors) {
+ Contract.Requires(innerTerm != null);
+ Contract.Requires(completeType != null);
+ Contract.Requires(var != null);
+ Contract.Requires(cce.NonNullElements(extractors));
if (completeType.IsVariable) {
if (var.Equals(completeType)) {
extractors.Add(innerTerm);
@@ -320,37 +329,40 @@ Contract.Requires(cce.NonNullElements(extractors)); // Symbols for representing functions
// Globally defined functions
- private readonly IDictionary<Function/*!*/, UntypedFunction/*!*/>/*!*/ Typed2UntypedFunctions;
+ private readonly IDictionary<Function/*!*/, UntypedFunction/*!*/>/*!*/ Typed2UntypedFunctions;
[ContractInvariantMethod]
-void Typed2UntypedFunctionsInvariantMethod(){
-Contract.Invariant(cce.NonNullElements(Typed2UntypedFunctions));}
+ void Typed2UntypedFunctionsInvariantMethod() {
+ Contract.Invariant(cce.NonNullElements(Typed2UntypedFunctions));
+ }
// distinguish between implicit and explicit type parameters
internal static void SeparateTypeParams(List<Type/*!*/>/*!*/ valueArgumentTypes,
TypeVariableSeq/*!*/ allTypeParams,
out List<TypeVariable/*!*/>/*!*/ implicitParams,
out List<TypeVariable/*!*/>/*!*/ explicitParams) {
- Contract.Requires(cce.NonNullElements(valueArgumentTypes));
-Contract.Requires(allTypeParams != null);
-Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out implicitParams)));
-Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out explicitParams)));
- TypeVariableSeq/*!*/ varsInInParamTypes = new TypeVariableSeq ();
- foreach (Type/*!*/ t in valueArgumentTypes){Contract.Assert(t != null);
- varsInInParamTypes.AppendWithoutDups(t.FreeVariables);}
-
- implicitParams = new List<TypeVariable/*!*/> (allTypeParams.Length);
- explicitParams = new List<TypeVariable/*!*/> (allTypeParams.Length);
-
- foreach (TypeVariable/*!*/ var in allTypeParams) {
- Contract.Assert(var != null);
- if (varsInInParamTypes.Has(var))
- implicitParams.Add(var);
- else
- explicitParams.Add(var);
- }
-
- implicitParams.TrimExcess();
- explicitParams.TrimExcess();
+ Contract.Requires(cce.NonNullElements(valueArgumentTypes));
+ Contract.Requires(allTypeParams != null);
+ Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out implicitParams)));
+ Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out explicitParams)));
+ TypeVariableSeq/*!*/ varsInInParamTypes = new TypeVariableSeq();
+ foreach (Type/*!*/ t in valueArgumentTypes) {
+ Contract.Assert(t != null);
+ varsInInParamTypes.AppendWithoutDups(t.FreeVariables);
+ }
+
+ implicitParams = new List<TypeVariable/*!*/>(allTypeParams.Length);
+ explicitParams = new List<TypeVariable/*!*/>(allTypeParams.Length);
+
+ foreach (TypeVariable/*!*/ var in allTypeParams) {
+ Contract.Assert(var != null);
+ if (varsInInParamTypes.Has(var))
+ implicitParams.Add(var);
+ else
+ explicitParams.Add(var);
+ }
+
+ implicitParams.TrimExcess();
+ explicitParams.TrimExcess();
}
internal UntypedFunction Typed2Untyped(Function fun) {
@@ -361,7 +373,7 @@ Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out explicitParams)) // if all of the parameters are int or bool, the function does
// not have to be changed
- if (Contract.ForAll(0,fun.InParams.Length, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&
+ if (Contract.ForAll(0, fun.InParams.Length, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&
UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type) &&
fun.TypeParameters.Length == 0) {
res = new UntypedFunction(fun, new List<TypeVariable/*!*/>(), new List<TypeVariable/*!*/>());
@@ -398,10 +410,10 @@ Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out explicitParams)) return res;
}
- private VCExpr GenFunctionAxiom(UntypedFunction fun, Function originalFun){
-Contract.Requires(originalFun != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
- List<Type/*!*/>/*!*/ originalInTypes = new List<Type/*!*/> (originalFun.InParams.Length);
+ private VCExpr GenFunctionAxiom(UntypedFunction fun, Function originalFun) {
+ Contract.Requires(originalFun != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ List<Type/*!*/>/*!*/ originalInTypes = new List<Type/*!*/>(originalFun.InParams.Length);
foreach (Formal/*!*/ f in originalFun.InParams)
originalInTypes.Add(f.TypedIdent.Type);
@@ -414,8 +426,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); List<TypeVariable/*!*/>/*!*/ implicitTypeParams,
List<TypeVariable/*!*/>/*!*/ explicitTypeParams,
List<Type/*!*/>/*!*/ originalInTypes,
- Type/*!*/ originalResultType)
- {
+ Type/*!*/ originalResultType) {
Contract.Requires(cce.NonNullElements(implicitTypeParams));
Contract.Requires(fun != null);
Contract.Requires(cce.NonNullElements(explicitTypeParams));
@@ -426,21 +437,23 @@ 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) {Contract.Assert(t != null);
+ foreach (Type/*!*/ t in originalInTypes) {
+ Contract.Assert(t != null);
typedInputVars.Add(Gen.Variable("arg" + i, t));
i = i + 1;
}
- VariableBindings/*!*/ bindings = new VariableBindings ();
+ VariableBindings/*!*/ bindings = new VariableBindings();
// type parameters that have to be given explicitly are replaced
// with universally quantified type variables
- List<VCExprVar/*!*/>/*!*/ boundVars = new List<VCExprVar/*!*/> (explicitTypeParams.Count + typedInputVars.Count);
- foreach (TypeVariable/*!*/ var in explicitTypeParams) {Contract.Assert(var != null);
+ List<VCExprVar/*!*/>/*!*/ boundVars = new List<VCExprVar/*!*/>(explicitTypeParams.Count + typedInputVars.Count);
+ foreach (TypeVariable/*!*/ var in explicitTypeParams) {
+ Contract.Assert(var != null);
VCExprVar/*!*/ newVar = Gen.Variable(var.Name, T);
boundVars.Add(newVar);
bindings.TypeVariableBindings.Add(var, newVar);
@@ -448,9 +461,9 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); // bound term variables are replaced with bound term variables typed in
// a simpler way
- foreach(VCExprVar/*!*/ var in typedInputVars){
+ foreach (VCExprVar/*!*/ var in typedInputVars) {
Contract.Assert(var != null);
- Type/*!*/ newType = TypeAfterErasure(var.Type);
+ Type/*!*/ newType = TypeAfterErasure(var.Type);
Contract.Assert(newType != null);
VCExprVar/*!*/ newVar = Gen.Variable(var.Name, newType);
Contract.Assert(newVar != null);
@@ -470,7 +483,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); VCExpr conclusionWithPremisses =
// leave out antecedents of function type axioms ... they don't appear necessary,
// because a function can always be extended to all U-values (right?)
-// AddTypePremisses(typeVarBindings, typePremisses, true, conclusion);
+ // AddTypePremisses(typeVarBindings, typePremisses, true, conclusion);
Gen.Let(typeVarBindings, conclusion);
if (boundVars.Count > 0) {
@@ -481,16 +494,16 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); return conclusionWithPremisses;
}
}
-
+
////////////////////////////////////////////////////////////////////////////
- protected override void AddVarTypeAxiom(VCExprVar var, Type originalType){
-//Contract.Requires(originalType != null);
-//Contract.Requires(var != null);
+ 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/*!*/>()));
+ // we don't have any bindings available
+ new Dictionary<TypeVariable/*!*/, VCExpr/*!*/>()));
}
public VCExpr GenVarTypeAxiom(VCExprVar var, Type originalType, IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ varMapping) {
@@ -509,7 +522,8 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); /////////////////////////////////////////////////////////////////////////////
- internal class MapTypeAbstractionBuilderPremisses : MapTypeAbstractionBuilder {
+ internal class MapTypeAbstractionBuilderPremisses : MapTypeAbstractionBuilder
+ {
private readonly TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
[ContractInvariantMethod]
@@ -518,19 +532,21 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); }
- internal MapTypeAbstractionBuilderPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen) :base(axBuilder, gen){
+ internal MapTypeAbstractionBuilderPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen)
+ : base(axBuilder, gen) {
Contract.Requires(gen != null);
Contract.Requires(axBuilder != null);
-
+
this.AxBuilderPremisses = axBuilder;
}
// constructor for cloning
- internal MapTypeAbstractionBuilderPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen, MapTypeAbstractionBuilderPremisses builder):base(axBuilder, gen, builder) {
+ internal MapTypeAbstractionBuilderPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen, MapTypeAbstractionBuilderPremisses builder)
+ : base(axBuilder, gen, builder) {
Contract.Requires(builder != null);
Contract.Requires(gen != null);
Contract.Requires(axBuilder != null);
-
+
this.AxBuilderPremisses = axBuilder;
}
@@ -935,54 +951,59 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); /////////////////////////////////////////////////////////////////////////////
- public class TypeEraserPremisses : TypeEraser {
+ public class TypeEraserPremisses : TypeEraser
+ {
private readonly TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(AxBuilderPremisses != null);
-}
+ void ObjectInvariant() {
+ Contract.Invariant(AxBuilderPremisses != null);
+ }
private OpTypeEraser OpEraserAttr = null;
- protected override OpTypeEraser/*!*/ OpEraser { get {Contract.Ensures(Contract.Result<OpTypeEraser>() != null);
+ protected override OpTypeEraser/*!*/ OpEraser {
+ get {
+ Contract.Ensures(Contract.Result<OpTypeEraser>() != null);
- if (OpEraserAttr == null)
- OpEraserAttr = new OpTypeEraserPremisses(this, AxBuilderPremisses, Gen);
- return OpEraserAttr;
- } }
+ if (OpEraserAttr == null)
+ OpEraserAttr = new OpTypeEraserPremisses(this, AxBuilderPremisses, Gen);
+ return OpEraserAttr;
+ }
+ }
+
+ public TypeEraserPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen)
+ : base(axBuilder, gen) {
+ Contract.Requires(gen != null);
+ Contract.Requires(axBuilder != null);
- public TypeEraserPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen):base(axBuilder, gen){
-Contract.Requires(gen != null);
-Contract.Requires(axBuilder != null);
-
this.AxBuilderPremisses = axBuilder;
}
////////////////////////////////////////////////////////////////////////////
- public override VCExpr Visit(VCExprQuantifier node, VariableBindings oldBindings){
-Contract.Requires(oldBindings != null);
-Contract.Requires(node != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ public override VCExpr Visit(VCExprQuantifier node, VariableBindings oldBindings) {
+ Contract.Requires(oldBindings != null);
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
VariableBindings bindings = oldBindings.Clone();
// determine the bound vars that actually occur in the body or
// in any of the triggers (if some variables do not occur, we
// need to take special care of type parameters that only occur
// in the types of such variables)
- FreeVariableCollector coll = new FreeVariableCollector ();
+ FreeVariableCollector coll = new FreeVariableCollector();
coll.Collect(node.Body);
foreach (VCTrigger trigger in node.Triggers) {
if (trigger.Pos)
- foreach(VCExpr/*!*/ e in trigger.Exprs){
-Contract.Assert(e != null);
+ foreach (VCExpr/*!*/ e in trigger.Exprs) {
+ Contract.Assert(e != null);
- coll.Collect(e);}
+ coll.Collect(e);
+ }
}
- List<VCExprVar/*!*/> occurringVars = new List<VCExprVar/*!*/> (node.BoundVars.Count);
+ List<VCExprVar/*!*/> occurringVars = new List<VCExprVar/*!*/>(node.BoundVars.Count);
foreach (VCExprVar var in node.BoundVars)
if (coll.FreeTermVars.ContainsKey(var))
occurringVars.Add(var);
@@ -1025,15 +1046,16 @@ Contract.Assert(e != null); // build a substitution of the type variables that it can be checked
// whether type premisses are trivial
- VCExprSubstitution/*!*/ typeParamSubstitution = new VCExprSubstitution ();
- foreach(VCExprLetBinding/*!*/ binding in typeVarBindings){
-Contract.Assert(binding != null);
- typeParamSubstitution[binding.V] = binding.E;}
- SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor (Gen);
+ VCExprSubstitution/*!*/ typeParamSubstitution = new VCExprSubstitution();
+ foreach (VCExprLetBinding/*!*/ binding in typeVarBindings) {
+ Contract.Assert(binding != null);
+ typeParamSubstitution[binding.V] = binding.E;
+ }
+ SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor(Gen);
Contract.Assert(substituter != null);
- List<VCExpr/*!*/>/*!*/ typePremisses = new List<VCExpr/*!*/> (newBoundVars.Count);
- triggers = new List<VCTrigger/*!*/> (newBoundVars.Count);
+ List<VCExpr/*!*/>/*!*/ typePremisses = new List<VCExpr/*!*/>(newBoundVars.Count);
+ triggers = new List<VCTrigger/*!*/>(newBoundVars.Count);
for (int i = 0; i < newBoundVars.Count; ++i) {
VCExprVar/*!*/ oldVar = oldBoundVars[i];
@@ -1057,14 +1079,14 @@ Contract.Assert(binding != null); typePremisses.TrimExcess();
triggers.TrimExcess();
-
+
return Gen.NAry(VCExpressionGenerator.AndOp, typePremisses);
}
// these optimisations should maybe be moved into a separate
// visitor (peep-hole optimisations)
- private bool IsTriviallyTrue(VCExpr expr){
-Contract.Requires(expr != null);
+ private bool IsTriviallyTrue(VCExpr expr) {
+ Contract.Requires(expr != null);
if (expr.Equals(VCExpressionGenerator.True))
return true;
@@ -1155,40 +1177,40 @@ Contract.Requires(expr != null); return Gen.Quantify(node.Quan, new List<TypeVariable/*!*/>(), newBoundVars,
newTriggers, node.Infos, bodyWithPremisses);
}
-
+
// check whether we need to add let-binders for any of the type
// parameters to the triggers (otherwise, the triggers will
// contain unbound/dangling variables for such parameters)
- private List<VCTrigger/*!*/>/*!*/ AddLets2Triggers( List<VCTrigger/*!*/>/*!*/ triggers/*!*/, List<VCExprLetBinding/*!*/>/*!*/ typeVarBindings){
-Contract.Requires(cce.NonNullElements(triggers/*!*/));
-Contract.Requires(cce.NonNullElements(typeVarBindings));
-Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCTrigger>>()));
- List<VCTrigger/*!*/>/*!*/ triggersWithLets = new List<VCTrigger/*!*/> (triggers.Count);
+ private List<VCTrigger/*!*/>/*!*/ AddLets2Triggers(List<VCTrigger/*!*/>/*!*/ triggers/*!*/, List<VCExprLetBinding/*!*/>/*!*/ typeVarBindings) {
+ Contract.Requires(cce.NonNullElements(triggers/*!*/));
+ Contract.Requires(cce.NonNullElements(typeVarBindings));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCTrigger>>()));
+ List<VCTrigger/*!*/>/*!*/ triggersWithLets = new List<VCTrigger/*!*/>(triggers.Count);
- foreach(VCTrigger/*!*/ t in triggers){
-Contract.Assert(t != null);
- List<VCExpr/*!*/>/*!*/ exprsWithLets = new List<VCExpr/*!*/> (t.Exprs.Count);
+ foreach (VCTrigger/*!*/ t in triggers) {
+ Contract.Assert(t != null);
+ List<VCExpr/*!*/>/*!*/ exprsWithLets = new List<VCExpr/*!*/>(t.Exprs.Count);
bool changed = false;
- foreach(VCExpr/*!*/ e in t.Exprs){
-Contract.Assert(e != null);
-Dictionary<VCExprVar/*!*/, object>/*!*/ freeVars =
- FreeVariableCollector.FreeTermVariables(e);
-Contract.Assert(freeVars!=null&&cce.NonNullElements(freeVars.Keys));
- if (Contract.Exists(typeVarBindings, b=> freeVars.ContainsKey(b.V))) {
+ foreach (VCExpr/*!*/ e in t.Exprs) {
+ Contract.Assert(e != null);
+ Dictionary<VCExprVar/*!*/, object>/*!*/ freeVars =
+ FreeVariableCollector.FreeTermVariables(e);
+ Contract.Assert(freeVars != null && cce.NonNullElements(freeVars.Keys));
+ if (Contract.Exists(typeVarBindings, b => freeVars.ContainsKey(b.V))) {
exprsWithLets.Add(Gen.Let(typeVarBindings, e));
changed = true;
} else {
exprsWithLets.Add(e);
}
}
-
+
if (changed)
triggersWithLets.Add(Gen.Trigger(t.Pos, exprsWithLets));
else
triggersWithLets.Add(t);
}
-
+
return triggersWithLets;
}
@@ -1196,7 +1218,8 @@ Contract.Assert(freeVars!=null&&cce.NonNullElements(freeVars.Keys)); //////////////////////////////////////////////////////////////////////////////
- public class OpTypeEraserPremisses : OpTypeEraser {
+ public class OpTypeEraserPremisses : OpTypeEraser
+ {
private TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
[ContractInvariantMethod]
@@ -1205,34 +1228,36 @@ Contract.Assert(freeVars!=null&&cce.NonNullElements(freeVars.Keys)); }
- public OpTypeEraserPremisses(TypeEraserPremisses eraser, TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen):base(eraser, axBuilder, gen){
-Contract.Requires(gen != null);
-Contract.Requires(axBuilder != null);
-Contract.Requires(eraser != null);
+ public OpTypeEraserPremisses(TypeEraserPremisses eraser, TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen)
+ : base(eraser, axBuilder, gen) {
+ Contract.Requires(gen != null);
+ Contract.Requires(axBuilder != null);
+ Contract.Requires(eraser != null);
this.AxBuilderPremisses = axBuilder;
}
- private VCExpr HandleFunctionOp(Function newFun, List<Type/*!*/>/*!*/ typeArgs/*!*/, IEnumerable<VCExpr/*!*/>/*!*/ oldArgs, VariableBindings bindings){
-Contract.Requires(bindings != null);
-Contract.Requires(newFun != null);
-Contract.Requires(cce.NonNullElements(typeArgs/*!*/));
-Contract.Requires(cce.NonNullElements(oldArgs));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ private VCExpr HandleFunctionOp(Function newFun, List<Type/*!*/>/*!*/ typeArgs/*!*/, IEnumerable<VCExpr/*!*/>/*!*/ oldArgs, VariableBindings bindings) {
+ Contract.Requires(bindings != null);
+ Contract.Requires(newFun != null);
+ Contract.Requires(cce.NonNullElements(typeArgs/*!*/));
+ Contract.Requires(cce.NonNullElements(oldArgs));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
// UGLY: the code for tracking polarities should be factored out
int oldPolarity = Eraser.Polarity;
Eraser.Polarity = 0;
- List<VCExpr/*!*/>/*!*/ newArgs = new List<VCExpr/*!*/> (typeArgs.Count);
+ List<VCExpr/*!*/>/*!*/ newArgs = new List<VCExpr/*!*/>(typeArgs.Count);
// translate the explicit type arguments
- foreach(Type/*!*/ t in typeArgs){
-Contract.Assert(t != null);
- newArgs.Add(AxBuilder.Type2Term(t, bindings.TypeVariableBindings));}
+ foreach (Type/*!*/ t in typeArgs) {
+ Contract.Assert(t != null);
+ newArgs.Add(AxBuilder.Type2Term(t, bindings.TypeVariableBindings));
+ }
// recursively translate the value arguments
- foreach(VCExpr/*!*/ arg in oldArgs){
-Contract.Assert(arg != null);
-Type/*!*/ newType = cce.NonNull(newFun.InParams[newArgs.Count]).TypedIdent.Type;
+ foreach (VCExpr/*!*/ arg in oldArgs) {
+ Contract.Assert(arg != null);
+ Type/*!*/ newType = cce.NonNull(newFun.InParams[newArgs.Count]).TypedIdent.Type;
newArgs.Add(AxBuilder.Cast(Eraser.Mutate(arg, bindings), newType));
}
@@ -1240,8 +1265,9 @@ Type/*!*/ newType = cce.NonNull(newFun.InParams[newArgs.Count]).TypedIdent.Type; return Gen.Function(newFun, newArgs);
}
- public override VCExpr/*!*/ VisitSelectOp (VCExprNAry/*!*/ node,
- VariableBindings/*!*/ bindings) {Contract.Requires(node != null);Contract.Requires(bindings != null);
+ public override VCExpr/*!*/ VisitSelectOp(VCExprNAry/*!*/ node,
+ VariableBindings/*!*/ bindings) {
+ Contract.Requires(node != null); Contract.Requires(bindings != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
MapType/*!*/ mapType = node[0].Type.AsMap;
@@ -1262,29 +1288,29 @@ Type/*!*/ newType = cce.NonNull(newFun.InParams[newArgs.Count]).TypedIdent.Type; return HandleFunctionOp(select, typeArgs, node, bindings);
}
- public override VCExpr VisitStoreOp (VCExprNAry node, VariableBindings bindings){
-Contract.Requires(bindings != null);
-Contract.Requires(node != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ public override VCExpr VisitStoreOp(VCExprNAry node, VariableBindings bindings) {
+ Contract.Requires(bindings != null);
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
TypeSeq/*!*/ instantiations; // not used
Function/*!*/ store =
AxBuilder.MapTypeAbstracter.Store(node[0].Type.AsMap, out instantiations);
Contract.Assert(store != null);
return HandleFunctionOp(store,
- // the store function never has explicit
- // type parameters
+ // the store function never has explicit
+ // type parameters
new List<Type/*!*/>(),
node, bindings);
}
- public override VCExpr VisitBoogieFunctionOp (VCExprNAry node, VariableBindings bindings){
-Contract.Requires(bindings != null);
-Contract.Requires(node != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ public override VCExpr VisitBoogieFunctionOp(VCExprNAry node, VariableBindings bindings) {
+ Contract.Requires(bindings != null);
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
Function/*!*/ oriFun = ((VCExprBoogieFunctionOp)node.Op).Func;
Contract.Assert(oriFun != null);
UntypedFunction untypedFun = AxBuilderPremisses.Typed2Untyped(oriFun);
- Contract.Assert( untypedFun.Fun.InParams.Length ==
+ Contract.Assert(untypedFun.Fun.InParams.Length ==
untypedFun.ExplicitTypeParams.Count + node.Arity);
List<Type/*!*/>/*!*/ typeArgs =
@@ -1293,12 +1319,12 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); return HandleFunctionOp(untypedFun.Fun, typeArgs, node, bindings);
}
- private List<Type/*!*/>/*!*/ ExtractTypeArgs(VCExprNAry node, TypeVariableSeq allTypeParams, List<TypeVariable/*!*/>/*!*/ explicitTypeParams){
-Contract.Requires(allTypeParams != null);
-Contract.Requires(node != null);
-Contract.Requires(cce.NonNullElements(explicitTypeParams));
-Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
- List<Type/*!*/>/*!*/ res = new List<Type/*!*/> (explicitTypeParams.Count);
+ private List<Type/*!*/>/*!*/ ExtractTypeArgs(VCExprNAry node, TypeVariableSeq allTypeParams, List<TypeVariable/*!*/>/*!*/ explicitTypeParams) {
+ Contract.Requires(allTypeParams != null);
+ Contract.Requires(node != null);
+ Contract.Requires(cce.NonNullElements(explicitTypeParams));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
+ List<Type/*!*/>/*!*/ res = new List<Type/*!*/>(explicitTypeParams.Count);
foreach (TypeVariable/*!*/ var in explicitTypeParams) {
Contract.Assert(var != null);
// this lookup could be optimised
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 89c615ad..74505150 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -664,7 +664,6 @@ namespace Microsoft.Boogie.VCExprAST { return !ib.MoveNext();
}
}
- return true;
}
public static int PolyHash(int init, int factor, IEnumerable a) {
@@ -1505,6 +1504,14 @@ namespace Microsoft.Boogie.VCExprAST { return false;
return this.Name == t.Name && this.arity == t.arity && this.Type == t.Type;
}
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override int GetHashCode() {
+ int h = Name.GetHashCode();
+ h = 7823 * h + arity;
+ h = 7823 * h + Type.GetHashCode();
+ return h;
+ }
public override int Arity {
get {
return arity;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 9e68dc58..55cfa650 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -69,6 +69,7 @@ namespace Microsoft.Boogie { [ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Trace != null);
+ Contract.Invariant(Context != null);
Contract.Invariant(cce.NonNullElements(relatedInformation));
Contract.Invariant(cce.NonNullElements(calleeCounterexamples));
}
@@ -77,16 +78,19 @@ namespace Microsoft.Boogie { public BlockSeq Trace;
public ErrorModel Model;
public VC.ModelViewInfo MvInfo;
+ public ProverContext Context;
[Peer]
public List<string>/*!>!*/ relatedInformation;
public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;
- internal Counterexample(BlockSeq trace, ErrorModel model, VC.ModelViewInfo mvInfo) {
+ internal Counterexample(BlockSeq trace, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context) {
Contract.Requires(trace != null);
+ Contract.Requires(context != null);
this.Trace = trace;
this.Model = model;
this.MvInfo = mvInfo;
+ this.Context = context;
this.relatedInformation = new List<string>();
this.calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();
}
@@ -195,11 +199,70 @@ namespace Microsoft.Boogie { }
// we now have the list of states in 'states'
states.Sort();
+#if DEBUG_PRINT
+ Console.WriteLine("DEBUG: ---------- start ----------");
+ foreach (Variable v in MvInfo.AllVariables) {
+ List<string> names = new List<string>();
+
+ {
+ string ss = v.Name;
+ VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(v);
+ if (vvar != null) {
+ string uniqueName = Context.Lookup(vvar);
+ ss += " -> " + uniqueName;
+ }
+ names.Add(ss);
+ }
+
+ foreach (int s in states) {
+ if (0 <= s && s < MvInfo.CapturePoints.Count) {
+ VC.ModelViewInfo.Mapping m = MvInfo.CapturePoints[s];
+ var map = m.IncarnationMap;
+ if (map.ContainsKey(v)) {
+ Expr e = (Expr)map[v];
+ var ss = string.Format("[{0}: {1}", m.Description, e.ToString());
+ IdentifierExpr ide = e as IdentifierExpr;
+ if (ide != null) {
+ VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(ide.Decl);
+ if (vvar != null) {
+ string uniqueName = Context.Lookup(vvar);
+ ss += " -> " + uniqueName;
+ }
+ }
+ ss += "]";
+ names.Add(ss);
+ }
+ }
+ }
+
+ foreach (var nm in names) {
+ Console.Write("{0} ", nm);
+ }
+ Console.WriteLine();
+ }
+ Console.WriteLine("DEBUG: ---------- end ----------");
+#endif
+ List<Variable> changedVariables;
+ if (states.Count <= 1) {
+ changedVariables = MvInfo.AllVariables;
+ } else {
+ VC.ModelViewInfo.Mapping last = MvInfo.CapturePoints[MvInfo.CapturePoints.Count-1];
+ changedVariables = new List<Variable>();
+ List<Variable> unchangedVariables = new List<Variable>();
+ foreach (Variable v in MvInfo.AllVariables) {
+ if (last.IncarnationMap.ContainsKey(v)) {
+ changedVariables.Add(v);
+ } else {
+ unchangedVariables.Add(v);
+ }
+ }
+ PrintCapturedState(8, unchangedVariables, new Hashtable());
+ }
foreach (int s in states) {
if (0 <= s && s < MvInfo.CapturePoints.Count) {
VC.ModelViewInfo.Mapping m = MvInfo.CapturePoints[s];
Console.WriteLine(" {0}", m.Description);
- PrintCapturedState(8, m.IncarnationMap);
+ PrintCapturedState(8, changedVariables, m.IncarnationMap);
} else {
Console.WriteLine(" undefined captured-state ID {0}", s);
}
@@ -263,20 +326,21 @@ namespace Microsoft.Boogie { return m;
}
- void PrintCapturedState(int indent, Hashtable/*Variable -> Expr*/ incarnations) {
+ void PrintCapturedState(int indent, List<Variable> varSet, Hashtable/*Variable -> Expr*/ incarnations) {
Contract.Requires(0 <= indent);
+ Contract.Requires(varSet != null);
Contract.Requires(Model != null && MvInfo != null);
string ind = new string(' ', indent);
- foreach (Variable v in MvInfo.AllVariables) {
+ foreach (Variable v in varSet) {
string varName = v.Name;
- string incarnationName = varName;
+ Variable incarnation = v;
string val = null;
if (incarnations.ContainsKey(v)) {
Expr e = (Expr)incarnations[v];
if (e is IdentifierExpr) {
IdentifierExpr ide = (IdentifierExpr)e;
- incarnationName = ide.Decl.Name;
+ incarnation = ide.Decl;
} else if (e is LiteralExpr) {
LiteralExpr lit = (LiteralExpr)e;
val = lit.Val.ToString();
@@ -285,17 +349,25 @@ namespace Microsoft.Boogie { }
}
if (val == null) {
+ // first, get the unique name
+ string uniqueName;
+ VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(incarnation);
+ if (vvar == null) {
+ uniqueName = incarnation.Name;
+ } else {
+ uniqueName = Context.Lookup(vvar);
+ }
// look up the value in the model
- int partition;
- if (Model.identifierToPartition.TryGetValue(incarnationName, out partition)) {
- object pvalue = Model.partitionToValue[partition];
+ int zid;
+ if (Model.identifierToPartition.TryGetValue(uniqueName, out zid)) {
+ object pvalue = Model.partitionToValue[zid];
if (pvalue != null) {
val = pvalue.ToString();
} else {
- val = "*" + partition; // temporary hack to have something to do in this case
+ val = "*" + zid; // temporary hack to have something to do in this case
}
} else {
- val = incarnationName; // temporary hack to have something to do in this case
+ val = uniqueName; // temporary hack to have something to do in this case
}
}
Console.WriteLine("{0}{1} = {2}", ind, varName, val);
@@ -326,12 +398,12 @@ namespace Microsoft.Boogie { }
- public AssertCounterexample(BlockSeq trace, AssertCmd failingAssert, ErrorModel model, VC.ModelViewInfo mvInfo)
- : base(trace, model, mvInfo) {
+ public AssertCounterexample(BlockSeq trace, AssertCmd failingAssert, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context)
+ : base(trace, model, mvInfo, context) {
Contract.Requires(trace != null);
Contract.Requires(failingAssert != null);
+ Contract.Requires(context != null);
this.FailingAssert = failingAssert;
- // base(trace);
}
public override int GetLocation() {
@@ -340,7 +412,7 @@ namespace Microsoft.Boogie { public override Counterexample Clone()
{
- var ret = new AssertCounterexample(Trace, FailingAssert, Model, MvInfo);
+ var ret = new AssertCounterexample(Trace, FailingAssert, Model, MvInfo, Context);
ret.calleeCounterexamples = calleeCounterexamples;
return ret;
}
@@ -356,15 +428,15 @@ namespace Microsoft.Boogie { }
- public CallCounterexample(BlockSeq trace, CallCmd failingCall, Requires failingRequires, ErrorModel model, VC.ModelViewInfo mvInfo)
- : base(trace, model, mvInfo) {
+ public CallCounterexample(BlockSeq trace, CallCmd failingCall, Requires failingRequires, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context)
+ : base(trace, model, mvInfo, context) {
Contract.Requires(!failingRequires.Free);
Contract.Requires(trace != null);
+ Contract.Requires(context != null);
Contract.Requires(failingCall != null);
Contract.Requires(failingRequires != null);
this.FailingCall = failingCall;
this.FailingRequires = failingRequires;
- // base(trace);
}
public override int GetLocation() {
@@ -373,7 +445,7 @@ namespace Microsoft.Boogie { public override Counterexample Clone()
{
- var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo);
+ var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo, Context);
ret.calleeCounterexamples = calleeCounterexamples;
return ret;
}
@@ -389,15 +461,15 @@ namespace Microsoft.Boogie { }
- public ReturnCounterexample(BlockSeq trace, TransferCmd failingReturn, Ensures failingEnsures, ErrorModel model, VC.ModelViewInfo mvInfo)
- : base(trace, model, mvInfo) {
+ public ReturnCounterexample(BlockSeq trace, TransferCmd failingReturn, Ensures failingEnsures, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context)
+ : base(trace, model, mvInfo, context) {
Contract.Requires(trace != null);
+ Contract.Requires(context != null);
Contract.Requires(failingReturn != null);
Contract.Requires(failingEnsures != null);
Contract.Requires(!failingEnsures.Free);
this.FailingReturn = failingReturn;
this.FailingEnsures = failingEnsures;
- // base(trace);
}
public override int GetLocation() {
@@ -406,7 +478,7 @@ namespace Microsoft.Boogie { public override Counterexample Clone()
{
- var ret = new ReturnCounterexample(Trace, FailingReturn, FailingEnsures, Model, MvInfo);
+ var ret = new ReturnCounterexample(Trace, FailingReturn, FailingEnsures, Model, MvInfo, Context);
ret.calleeCounterexamples = calleeCounterexamples;
return ret;
}
diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs index 40e454fb..ac52111e 100644 --- a/Source/VCGeneration/Context.cs +++ b/Source/VCGeneration/Context.cs @@ -87,9 +87,8 @@ public abstract class ProverContextContracts:ProverContext{ protected List<VCExpr> axiomConjuncts;
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(gen!=null);
+ void ObjectInvariant() {
+ Contract.Invariant(gen != null);
Contract.Invariant(genOptions != null);
Contract.Invariant(translator != null);
Contract.Invariant(orderingAxiomBuilder != null);
@@ -97,7 +96,7 @@ void ObjectInvariant() Contract.Invariant(incrementalProverCommands != null);
Contract.Invariant(cce.NonNullElements(distincts));
Contract.Invariant(cce.NonNullElements(axiomConjuncts));
-}
+ }
public VCExprTranslator/*?*/ exprTranslator;
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 13206c75..304130ef 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1362,7 +1362,8 @@ namespace VC { impl.Blocks = tmp;
}
- public Counterexample ToCounterexample() {
+ public Counterexample ToCounterexample(ProverContext context) {
+ Contract.Requires(context != null);
Contract.Ensures(Contract.Result<Counterexample>() != null);
BlockSeq trace = new BlockSeq();
@@ -1375,7 +1376,7 @@ namespace VC { foreach (Cmd c in b.Cmds) {
Contract.Assert(c != null);
if (c is AssertCmd) {
- return AssertCmdToCounterexample((AssertCmd)c, cce.NonNull(b.TransferCmd), trace, null, null, new Dictionary<Incarnation, Absy>());
+ return AssertCmdToCounterexample((AssertCmd)c, cce.NonNull(b.TransferCmd), trace, null, null, context, new Dictionary<Incarnation, Absy>());
}
}
}
@@ -1836,7 +1837,7 @@ namespace VC { if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
msg = s.reporter.resourceExceededMessage;
}
- callback.OnCounterexample(s.ToCounterexample(), msg);
+ callback.OnCounterexample(s.ToCounterexample(s.Checker.TheoremProver.Context), msg);
outcome = Outcome.Errors;
break;
}
@@ -2977,7 +2978,7 @@ namespace VC { }
Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo;
- ProverContext/*!*/ context;
+ protected ProverContext/*!*/ context;
Program/*!*/ program;
public ErrorReporter(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,
@@ -3097,7 +3098,6 @@ namespace VC { Contract.Requires(cce.NonNullElements(implName2LazyInliningInfo));
Contract.Requires(context != null);
Contract.Requires(program != null);
-
}
public override void OnModel(IList<string/*!*/>/*!*/ labels, ErrorModel errModel) {
@@ -3132,7 +3132,7 @@ namespace VC { if (b.Cmds.Has(a)) {
BlockSeq trace = new BlockSeq();
trace.Add(b);
- Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, errModel, MvInfo, incarnationOriginMap);
+ Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, errModel, MvInfo, context, incarnationOriginMap);
callback.OnCounterexample(newCounterexample, null);
goto NEXT_ASSERT;
}
@@ -3321,7 +3321,7 @@ namespace VC { // Skip if 'cmd' not contained in the trace or not an assert
if (cmd is AssertCmd && traceNodes.Contains(cmd))
{
- Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, new Dictionary<Incarnation, Absy/*!*/>());
+ Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, context, new Dictionary<Incarnation, Absy/*!*/>());
newCounterexample.AddCalleeCounterexample(calleeCounterexamples);
return newCounterexample;
}
@@ -3979,7 +3979,7 @@ namespace VC { if (assertCmd != null && errModel.LookupControlFlowFunctionAt(cfcValue, assertCmd.UniqueId) == 0)
{
Counterexample newCounterexample;
- newCounterexample = AssertCmdToCounterexample(assertCmd, transferCmd, trace, errModel, mvInfo, cce.NonNull(info.incarnationOriginMap));
+ newCounterexample = AssertCmdToCounterexample(assertCmd, transferCmd, trace, errModel, mvInfo, context, cce.NonNull(info.incarnationOriginMap));
newCounterexample.AddCalleeCounterexample(calleeCounterexamples);
return newCounterexample;
}
@@ -4110,7 +4110,7 @@ namespace VC { // Skip if 'cmd' not contained in the trace or not an assert
if (cmd is AssertCmd && traceNodes.Contains(cmd))
{
- Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, incarnationOriginMap);
+ Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, context, incarnationOriginMap);
Contract.Assert(newCounterexample != null);
newCounterexample.AddCalleeCounterexample(calleeCounterexamples);
return newCounterexample;
@@ -4878,12 +4878,13 @@ namespace VC { }
}
- static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, ErrorModel errModel, ModelViewInfo mvInfo,
+ static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, ErrorModel errModel, ModelViewInfo mvInfo, ProverContext context,
Dictionary<Incarnation, Absy> incarnationOriginMap)
{
Contract.Requires(cmd != null);
Contract.Requires(transferCmd != null);
Contract.Requires(trace != null);
+ Contract.Requires(context != null);
Contract.Requires(cce.NonNullElements(incarnationOriginMap));
Contract.Ensures(Contract.Result<Counterexample>() != null);
@@ -4904,7 +4905,7 @@ namespace VC { {
AssertRequiresCmd assertCmd = (AssertRequiresCmd)cmd;
Contract.Assert(assertCmd != null);
- CallCounterexample cc = new CallCounterexample(trace, assertCmd.Call, assertCmd.Requires, errModel, mvInfo);
+ CallCounterexample cc = new CallCounterexample(trace, assertCmd.Call, assertCmd.Requires, errModel, mvInfo, context);
cc.relatedInformation = relatedInformation;
return cc;
}
@@ -4912,13 +4913,13 @@ namespace VC { {
AssertEnsuresCmd assertCmd = (AssertEnsuresCmd)cmd;
Contract.Assert(assertCmd != null);
- ReturnCounterexample rc = new ReturnCounterexample(trace, transferCmd, assertCmd.Ensures, errModel, mvInfo);
+ ReturnCounterexample rc = new ReturnCounterexample(trace, transferCmd, assertCmd.Ensures, errModel, mvInfo, context);
rc.relatedInformation = relatedInformation;
return rc;
}
else
{
- AssertCounterexample ac = new AssertCounterexample(trace, (AssertCmd)cmd, errModel, mvInfo);
+ AssertCounterexample ac = new AssertCounterexample(trace, (AssertCmd)cmd, errModel, mvInfo, context);
ac.relatedInformation = relatedInformation;
return ac;
}
diff --git a/Test/test15/Answer b/Test/test15/Answer index 825df64f..974f24fc 100644 --- a/Test/test15/Answer +++ b/Test/test15/Answer @@ -199,36 +199,21 @@ Execution trace: CaptureState.bpl(16,5): anon4_Then
CaptureState.bpl(24,5): anon3
Captured states:
- top
Heap = *8
F = *10
this = *9
- x = x
- y = y
+ x = 797
+ y = y@@1
+ top
r = r
m = -2
then
- Heap = *8
- F = *10
- this = *9
- x = x
- y = y
r = r
m = -1
postUpdate0
- Heap = *8
- F = *10
- this = *9
- x = x
- y = y
r = r
m = -1
end
- Heap = *8
- F = *10
- this = *9
- x = x
- y = y
r = -2
m = -1
|