From 8a52ac8185e092fd5051f6fa24d97ea5e84dc431 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Thu, 24 Sep 2009 22:20:26 +0000 Subject: Added antecedent to select-of-store axioms to make them sound even when triggers are ignored. --- Source/VCExpr/TypeErasureArguments.ssc | 60 +++++----- Source/VCExpr/TypeErasurePremisses.ssc | 198 ++++++++++++++++++++------------- 2 files changed, 148 insertions(+), 110 deletions(-) diff --git a/Source/VCExpr/TypeErasureArguments.ssc b/Source/VCExpr/TypeErasureArguments.ssc index 434866f8..98baf874 100644 --- a/Source/VCExpr/TypeErasureArguments.ssc +++ b/Source/VCExpr/TypeErasureArguments.ssc @@ -166,36 +166,30 @@ namespace Microsoft.Boogie.TypeErasure // Fill in the index types foreach (Type! type in abstractedType.Arguments) { - if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(type)) - { - selectTypes[i] = type; - storeTypes[i] = type; - } - else - { - selectTypes[i] = AxBuilder.U; - storeTypes[i] = AxBuilder.U; - } - i++; - } - // Fill in the output type for select function which also happens - // to be the type of the last argument to the store function - if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(abstractedType.Result)) - { - selectTypes[i] = abstractedType.Result; - storeTypes[i] = abstractedType.Result; - } - else - { - selectTypes[i] = AxBuilder.U; - storeTypes[i] = AxBuilder.U; - } - i++; - // Fill in the map type which is the output of the store function + if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(type)) { + selectTypes[i] = type; + storeTypes[i] = type; + } else { + selectTypes[i] = AxBuilder.U; + storeTypes[i] = AxBuilder.U; + } + i++; + } + // Fill in the output type for select function which also happens + // to be the type of the last argument to the store function + if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(abstractedType.Result)) { + selectTypes[i] = abstractedType.Result; + storeTypes[i] = abstractedType.Result; + } else { + selectTypes[i] = AxBuilder.U; + storeTypes[i] = AxBuilder.U; + } + i++; + // Fill in the map type which is the output of the store function storeTypes[i] = AxBuilder.U; - NonNullType.AssertInitialized(selectTypes); - NonNullType.AssertInitialized(storeTypes); - + NonNullType.AssertInitialized(selectTypes); + NonNullType.AssertInitialized(storeTypes); + select = HelperFuns.BoogieFunction(baseName + "Select", selectTypes); store = HelperFuns.BoogieFunction(baseName + "Store", storeTypes); @@ -241,8 +235,8 @@ namespace Microsoft.Boogie.TypeErasure List indexTypes = new List(); for (int i = mapTypeParamNum + mapAbstractionVarNum + 1; i < select.InParams.Length; i++) { - indexTypes.Add(((!)select.InParams[i]).TypedIdent.Type); - } + indexTypes.Add(((!)select.InParams[i]).TypedIdent.Type); + } assert arity == indexTypes.Count; List! indexes = HelperFuns.VarVector("x", indexTypes, Gen); @@ -289,8 +283,8 @@ namespace Microsoft.Boogie.TypeErasure List indexTypes = new List(); for (int i = mapTypeParamNum + mapAbstractionVarNum + 1; i < select.InParams.Length; i++) { - indexTypes.Add(((!)select.InParams[i]).TypedIdent.Type); - } + indexTypes.Add(((!)select.InParams[i]).TypedIdent.Type); + } assert arity == indexTypes.Count; List! indexes0 = HelperFuns.VarVector("x", indexTypes, Gen); diff --git a/Source/VCExpr/TypeErasurePremisses.ssc b/Source/VCExpr/TypeErasurePremisses.ssc index 16ec87e6..10fb1247 100644 --- a/Source/VCExpr/TypeErasurePremisses.ssc +++ b/Source/VCExpr/TypeErasurePremisses.ssc @@ -136,28 +136,30 @@ namespace Microsoft.Boogie.TypeErasure List! typeParams, List! oldBoundVars, // VariableBindings to which the translation // TypeVariable -> VCExprVar is added - VariableBindings! bindings) { + VariableBindings! bindings, + bool addTypeVarsToBindings) { // type variables are replaced with ordinary variables that are bound using a // let-expression - foreach (TypeVariable! tvar in typeParams) - bindings.TypeVariableBindings.Add(tvar, Gen.Variable(tvar.Name, T)); + if (addTypeVarsToBindings) { + foreach (TypeVariable! tvar in typeParams) + bindings.TypeVariableBindings.Add(tvar, Gen.Variable(tvar.Name, T)); + } // extract the values of type variables from the term variables List! UtypedVars = new List (oldBoundVars.Count); List! originalTypes = new List (oldBoundVars.Count); - for (int i = 0; i < oldBoundVars.Count; ++i) { - VCExprVar! newVar = bindings.VCExprVarBindings[oldBoundVars[i]]; + foreach (VCExprVar var in oldBoundVars) { + VCExprVar! newVar = bindings.VCExprVarBindings[var]; if (newVar.Type.Equals(U)) { UtypedVars.Add(newVar); - originalTypes.Add(oldBoundVars[i].Type); + originalTypes.Add(var.Type); } } UtypedVars.TrimExcess(); originalTypes.TrimExcess(); - return BestTypeVarExtractors(typeParams, originalTypes, UtypedVars, - bindings); + return BestTypeVarExtractors(typeParams, originalTypes, UtypedVars, bindings); } @@ -335,10 +337,8 @@ namespace Microsoft.Boogie.TypeErasure List! explicitTypeParams, List! originalInTypes, Type! originalResultType) - requires originalInTypes.Count + - explicitTypeParams.Count == - fun.InParams.Length; { - + requires originalInTypes.Count + explicitTypeParams.Count == fun.InParams.Length; + { if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) { return VCExpressionGenerator.True; } @@ -361,7 +361,6 @@ namespace Microsoft.Boogie.TypeErasure bindings.TypeVariableBindings.Add(var, newVar); } - // bound term variables are replaced with bound term variables typed in // a simpler way foreach (VCExprVar! var in typedInputVars) { @@ -371,8 +370,8 @@ namespace Microsoft.Boogie.TypeErasure bindings.VCExprVarBindings.Add(var, newVar); } - List! typeVarBindings = - GenTypeParamBindings(implicitTypeParams, typedInputVars, bindings); + List typeVarBindings = + GenTypeParamBindings(implicitTypeParams, typedInputVars, bindings, true); VCExpr! funApp = Gen.Function(fun, HelperFuns.ToVCExprList(boundVars)); VCExpr! conclusion = Gen.Eq(TypeOf(funApp), @@ -384,15 +383,13 @@ namespace Microsoft.Boogie.TypeErasure Gen.Let(typeVarBindings, conclusion); if (boundVars.Count > 0) { - List! triggers = - HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp))); - return Gen.Forall(boundVars, triggers, - "funType:" + fun.Name, conclusionWithPremisses); + List triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp))); + return Gen.Forall(boundVars, triggers, "funType:" + fun.Name, conclusionWithPremisses); } else { return conclusionWithPremisses; } } - + //////////////////////////////////////////////////////////////////////////// protected override void AddVarTypeAxiom(VCExprVar! var, Type! originalType) { @@ -472,25 +469,26 @@ namespace Microsoft.Boogie.TypeErasure out typeParams, out originalInTypes); // select - List! explicitSelectParams; + List! explicitSelectParams, implicitSelectParams; select = CreateAccessFun(typeParams, originalInTypes, abstractedType.Result, synonym.Name + "Select", - out explicitSelectParams); + out implicitSelectParams, out explicitSelectParams); // store, which gets one further argument: the assigned rhs originalInTypes.Add(abstractedType.Result); - List! explicitStoreParams; + List! explicitStoreParams, implicitStoreParams; store = CreateAccessFun(typeParams, originalInTypes, mapTypeSynonym, synonym.Name + "Store", - out explicitStoreParams); + out implicitStoreParams, out explicitStoreParams); // the store function does not have any explicit type parameters assert explicitStoreParams.Count == 0; AxBuilder.AddTypeAxiom(GenMapAxiom0(select, store, abstractedType.Result, - explicitSelectParams)); + implicitSelectParams, explicitSelectParams, + originalInTypes)); AxBuilder.AddTypeAxiom(GenMapAxiom1(select, store, abstractedType.Result, explicitSelectParams)); @@ -518,14 +516,13 @@ namespace Microsoft.Boogie.TypeErasure List! originalInTypes, Type! originalResult, string! name, - out List! explicitTypeParams) { + out List! implicitTypeParams, out List! explicitTypeParams) { // select and store are basically handled like normal functions: the type // parameters are split into the implicit parameters, and into the parameters // that have to be given explicitly - List! implicitParams; TypeAxiomBuilderPremisses.SeparateTypeParams(originalInTypes, HelperFuns.ToSeq(originalTypeParams), - out implicitParams, + out implicitTypeParams, out explicitTypeParams); Type[]! ioTypes = new Type [explicitTypeParams.Count + originalInTypes.Count + 1]; int i = 0; @@ -534,23 +531,23 @@ namespace Microsoft.Boogie.TypeErasure foreach (Type! type in originalInTypes) { if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(type)) - ioTypes[i] = type; - else - ioTypes[i] = AxBuilder.U; - i++; + ioTypes[i] = type; + else + ioTypes[i] = AxBuilder.U; + i++; } if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(originalResult)) - ioTypes[i] = originalResult; - else - ioTypes[i] = AxBuilder.U; - + ioTypes[i] = originalResult; + else + ioTypes[i] = AxBuilder.U; + Function! res = HelperFuns.BoogieFunction(name, ioTypes); if (AxBuilder.U.Equals(ioTypes[i])) { - AxBuilder.AddTypeAxiom( - AxBuilderPremisses.GenFunctionAxiom(res, - implicitParams, explicitTypeParams, + AxBuilder.AddTypeAxiom( + AxBuilderPremisses.GenFunctionAxiom(res, + implicitTypeParams, explicitTypeParams, originalInTypes, originalResult)); } return res; @@ -585,47 +582,95 @@ namespace Microsoft.Boogie.TypeErasure return Gen.Function(store, storeArgs); } + /// + /// Generate: + /// (forall m, indexes, val :: + /// type(val) == T ==> + /// select(store(m, indexes, val), indexes) == val) + /// where the quantifier body is also enclosed in a let that defines portions of T, if needed. + /// private VCExpr! GenMapAxiom0(Function! select, Function! store, Type! mapResult, - List! explicitSelectParams) { + List! implicitTypeParamsSelect, List! explicitTypeParamsSelect, + List! originalInTypes) + { int arity = store.InParams.Length - 2; - VCExprVar! typedVal = Gen.Variable("val", mapResult); - VCExprVar! val = Gen.Variable("val", ((!)select.OutParams[0]).TypedIdent.Type); + List inParams = new List(); + List quantifiedVars = new List(store.InParams.Length); + VariableBindings bindings = new VariableBindings(); + + // bound variable: m + VCExprVar typedM = Gen.Variable("m", originalInTypes[0]); + VCExprVar m = Gen.Variable("m", AxBuilder.U); + inParams.Add(typedM); + quantifiedVars.Add(m); + bindings.VCExprVarBindings.Add(typedM, m); + + // bound variables: indexes + List origIndexTypes = new List(arity); + List indexTypes = new List(arity); + for (int i = 1; i < store.InParams.Length-1; i++) { + origIndexTypes.Add(originalInTypes[i]); + indexTypes.Add(((!)store.InParams[i]).TypedIdent.Type); + } + assert arity == indexTypes.Count; + List typedArgs = HelperFuns.VarVector("arg", origIndexTypes, Gen); + List indexes = HelperFuns.VarVector("x", indexTypes, Gen); + assert typedArgs.Count == indexes.Count; + inParams.AddRange(typedArgs); + quantifiedVars.AddRange(indexes); + for (int i = 0; i < arity; i++) { + bindings.VCExprVarBindings.Add(typedArgs[i], indexes[i]); + } - VariableBindings! bindings = new VariableBindings (); + // bound variable: val + VCExprVar typedVal = Gen.Variable("val", mapResult); + VCExprVar val = Gen.Variable("val", ((!)select.OutParams[0]).TypedIdent.Type); + quantifiedVars.Add(val); bindings.VCExprVarBindings.Add(typedVal, val); - // explicit type parameters are handled using a let-binder - List! letBindings = - AxBuilderPremisses.GenTypeParamBindings(explicitSelectParams, - HelperFuns.ToList(typedVal), - bindings); - List! typeParams = new List (explicitSelectParams.Count); - foreach (TypeVariable! var in explicitSelectParams) - typeParams.Add(bindings.TypeVariableBindings[var]); - - List indexTypes = new List(); - for (int i = 1; i < store.InParams.Length-1; i++) - { - indexTypes.Add(((!)store.InParams[i]).TypedIdent.Type); - } - assert arity == indexTypes.Count; - - List indexes = HelperFuns.VarVector("x", indexTypes, Gen); - VCExprVar! m = Gen.Variable("m", AxBuilder.U); + // add all type parameters into bindings + foreach (TypeVariable tp in implicitTypeParamsSelect) { + VCExprVar tVar = Gen.Variable(tp.Name, AxBuilderPremisses.T); + bindings.TypeVariableBindings.Add(tp, tVar); + } + List typeParams = new List(explicitTypeParamsSelect.Count); + foreach (TypeVariable tp in explicitTypeParamsSelect) { + VCExprVar tVar = Gen.Variable(tp.Name, AxBuilderPremisses.T); + bindings.TypeVariableBindings.Add(tp, tVar); + // ... and record these explicit type-parameter arguments in typeParams + typeParams.Add(tVar); + } VCExpr! storeExpr = Store(store, m, indexes, val); VCExpr! selectExpr = Select(select, typeParams, storeExpr, indexes); - List! quantifiedVars = new List (indexes.Count + 2); - quantifiedVars.Add(val); - quantifiedVars.Add(m); - quantifiedVars.AddRange(indexes); - + // Create let-binding definitions for all type parameters. + // The implicit ones can be phrased in terms of the types of the ordinary in-parameters, and + // we want to make sure that they don't get phrased in terms of the out-parameter, so we pass + // in inParams here. + List letBindings_Implicit = + AxBuilderPremisses.GenTypeParamBindings(implicitTypeParamsSelect, inParams, bindings, false); + // The explicit ones, by definition, can only be phrased in terms of the result, so we pass + // in List(typedVal) here. + List letBindings_Explicit = + AxBuilderPremisses.GenTypeParamBindings(explicitTypeParamsSelect, HelperFuns.ToList(typedVal), bindings, false); + + // generate: select(store(m, indices, val)) == val VCExpr! eq = Gen.Eq(selectExpr, val); - VCExpr! letEq = Gen.Let(letBindings, eq); - return Gen.Forall(quantifiedVars, new List (), - "mapAx0:" + select.Name, letEq); + // generate: type(val) == T, where T is the type of val + VCExpr! ante = Gen.Eq( + AxBuilderPremisses.TypeOf(val), + AxBuilderPremisses.Type2Term(mapResult, bindings.TypeVariableBindings)); + VCExpr body; + if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None || + !AxBuilder.U.Equals(mapResult)) + { + body = Gen.Let(letBindings_Explicit, eq); + } else { + body = Gen.Let(letBindings_Implicit, Gen.Let(letBindings_Explicit, Gen.ImpliesSimp(ante, eq))); + } + return Gen.Forall(quantifiedVars, new List(), "mapAx0:" + select.Name, body); } private VCExpr! GenMapAxiom1(Function! select, Function! store, @@ -633,13 +678,13 @@ namespace Microsoft.Boogie.TypeErasure List! explicitSelectParams) { int arity = store.InParams.Length - 2; - List indexTypes = new List(); + List indexTypes = new List(); for (int i = 1; i < store.InParams.Length-1; i++) { - indexTypes.Add(((!)store.InParams[i]).TypedIdent.Type); - } - assert indexTypes.Count == arity; - + indexTypes.Add(((!)store.InParams[i]).TypedIdent.Type); + } + assert indexTypes.Count == arity; + List! indexes0 = HelperFuns.VarVector("x", indexTypes, Gen); List! indexes1 = HelperFuns.VarVector("y", indexTypes, Gen); VCExprVar! m = Gen.Variable("m", AxBuilder.U); @@ -653,7 +698,7 @@ namespace Microsoft.Boogie.TypeErasure List! letBindings = AxBuilderPremisses.GenTypeParamBindings(explicitSelectParams, HelperFuns.ToList(typedVal), - bindings); + bindings, true); // ... and quantify the introduced term variables for type // parameters universally @@ -831,8 +876,7 @@ namespace Microsoft.Boogie.TypeErasure List! newBoundVars, VariableBindings! bindings) { List! typeVarBindings = - AxBuilderPremisses.GenTypeParamBindings(node.TypeParameters, - occurringVars, bindings); + AxBuilderPremisses.GenTypeParamBindings(node.TypeParameters, occurringVars, bindings, true); // Check whether some of the type parameters could not be // determined from the bound variable types. In this case, we -- cgit v1.2.3