From cc95308361d22131bb2fbb11903c30b9dba68300 Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 10 Aug 2011 23:56:06 +0530 Subject: Added "procedure-copy bounding" for lazy inlining --- Source/Core/CommandLineOptions.cs | 24 +++--- Source/VCGeneration/VC.cs | 162 +++++++++++++++++++++++++++++++++++++- 2 files changed, 170 insertions(+), 16 deletions(-) (limited to 'Source') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index edca934c..c6b8e493 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -353,6 +353,7 @@ namespace Microsoft.Boogie { public bool PrintInlined = false; public bool ExtractLoops = false; public int LazyInlining = 0; + public int ProcedureCopyBound = 1; public int StratifiedInlining = 0; public int StratifiedInliningOption = 0; public bool UseUnsatCoreForInlining = false; @@ -1127,20 +1128,15 @@ namespace Microsoft.Boogie { case "-lazyInline": case "/lazyInline": if (ps.ConfirmArgumentCount(1)) { - switch (args[ps.i]) { - case "0": - LazyInlining = 0; - break; - case "1": - LazyInlining = 1; - break; - case "2": - LazyInlining = 2; - break; - default: - ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); - break; - } + LazyInlining = Int32.Parse(args[ps.i]); + if (LazyInlining > 3) ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + } + break; + case "-procCopyBound": + case "/procCopyBound": + if (ps.ConfirmArgumentCount(1)) + { + ProcedureCopyBound = Int32.Parse(args[ps.i]); } break; case "-stratifiedInline": diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 87ab590d..576ce080 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -36,6 +36,10 @@ namespace VC { if (CommandLineOptions.Clo.LazyInlining > 0) { this.GenerateVCsForLazyInlining(program); + if (CommandLineOptions.Clo.LazyInlining == 3) + { + CreateCopiesForLazyInlining(CommandLineOptions.Clo.ProcedureCopyBound, program); + } } } @@ -83,6 +87,8 @@ namespace VC { public List interfaceVars; public Expr assertExpr; public VCExpr vcexpr; + public VCExpr inside_vc; // (without the quantifiers) + public List privateVars; public Dictionary incarnationOriginMap; public Hashtable /*Variable->Expr*/ exitIncarnationMap; public Hashtable /*GotoCmd->returnCmd*/ gotoCmdOrigins; @@ -220,6 +226,145 @@ namespace VC { } } + // proc name -> k -> interface variables + public static Dictionary>> interfaceVarCopies; + // proc name -> k -> VCExpr + Dictionary> procVcCopies; + + private void CreateCopiesForLazyInlining(int K, Program program) + { + interfaceVarCopies = new Dictionary>>(); + procVcCopies = new Dictionary>(); + + // Duplicate VCs of each procedure K times and remove quantifiers + Checker checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime); + foreach (LazyInliningInfo info in implName2LazyInliningInfo.Values) + { + Contract.Assert(info != null); + CreateCopyForLazyInlining(K, program, info, checker); + } + + // Change the procedure calls in each VC + // Push all to the theorem prover + var bm = new BoundingVCMutator(checker.VCExprGen, interfaceVarCopies); + foreach (var kvp in procVcCopies) + { + for (int i = 0; i < kvp.Value.Count; i++) + { + kvp.Value[i] = bm.Mutate(kvp.Value[i], true); + checker.TheoremProver.PushVCExpression(kvp.Value[i]); + } + } + } + + public class BoundingVCMutator : MutatingVCExprVisitor + { + // proc name -> k -> interface variables + Dictionary>> interfaceVarCopies; + + public BoundingVCMutator(VCExpressionGenerator gen, Dictionary>> interfaceVarCopies) + : base(gen) + { + Contract.Requires(gen != null); + this.interfaceVarCopies = interfaceVarCopies; + } + + protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, + List/*!*/ newSubExprs, + // has any of the subexpressions changed? + bool changed, + bool arg) + { + //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null); + Contract.Ensures(Contract.Result() != null); + + VCExpr node; + if (changed) + node = Gen.Function(originalNode.Op, + newSubExprs, originalNode.TypeArguments); + else + node = originalNode; + + var expr = node as VCExprNAry; + if (expr == null) return node; + var op = expr.Op as VCExprBoogieFunctionOp; + if (op == null) return node; + if (!interfaceVarCopies.ContainsKey(op.Func.Name)) return node; + + // substitute + var K = interfaceVarCopies[op.Func.Name].Count; + + + VCExpr ret = VCExpressionGenerator.False; + for (int k = 0; k < K; k++) + { + var iv = interfaceVarCopies[op.Func.Name][k]; + Contract.Assert(op.Arity == iv.Count); + + VCExpr conj = VCExpressionGenerator.True; + for (int i = 0; i < iv.Count; i++) + { + var c = Gen.Eq(expr[i], iv[i]); + conj = Gen.And(conj, c); + } + ret = Gen.Or(conj, ret); + } + + return ret; + } + + } // end BoundingVCMutator + + private static int newVarCnt = 0; + + private void CreateCopyForLazyInlining(int K, Program program, LazyInliningInfo info, Checker checker) + { + var translator = checker.TheoremProver.Context.BoogieExprTranslator; + interfaceVarCopies.Add(info.impl.Name, new List>()); + procVcCopies.Add(info.impl.Name, new List()); + + for (int k = 0; k < K; k++) + { + var expr = info.inside_vc; + // Instantiate the "forall" variables + Dictionary substForallDict = new Dictionary(); + var ls = new List(); + for (int i = 0; i < info.interfaceVars.Count; i++) + { + var v = translator.LookupVariable(info.interfaceVars[i]); + string newName = v.Name + "_fa_" + k.ToString() + "_" + newVarCnt.ToString(); + newVarCnt++; + //checker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null); + var vp = checker.VCExprGen.Variable(newName, v.Type); + substForallDict.Add(v, vp); + ls.Add(vp); + } + interfaceVarCopies[info.impl.Name].Add(ls); + VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary()); + + SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(checker.VCExprGen); + Contract.Assert(subst != null); + expr = subst.Mutate(expr, substForall); + + // Instantiate and declare the "exists" variables + Dictionary substExistsDict = new Dictionary(); + foreach (VCExprVar v in info.privateVars) + { + Contract.Assert(v != null); + string newName = v.Name + "_te_" + k.ToString() + "_" + newVarCnt.ToString(); + newVarCnt++; + checker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null); + substExistsDict.Add(v, checker.VCExprGen.Variable(newName, v.Type)); + } + VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary()); + + subst = new SubstitutingVCExprVisitor(checker.VCExprGen); + expr = subst.Mutate(expr, substExists); + + procVcCopies[info.impl.Name].Add(expr); + } + } + private void GenerateVCForLazyInlining(Program program, LazyInliningInfo info, Checker checker) { Contract.Requires(program != null); Contract.Requires(info != null); @@ -254,6 +399,10 @@ namespace VC { Contract.Assert(v != null); privateVars.Add(translator.LookupVariable(v)); } + + info.privateVars = privateVars; + info.inside_vc = vcexpr; + if (privateVars.Count > 0) { vcexpr = gen.Exists(new List(), privateVars, new List(), new VCQuantifierInfos(impl.Name, info.uniqueId, false, null), vcexpr); @@ -275,7 +424,7 @@ namespace VC { if (CommandLineOptions.Clo.LazyInlining == 1) { vcexpr = gen.Implies(expr, vcexpr); } else { - Contract.Assert(CommandLineOptions.Clo.LazyInlining == 2); + //Contract.Assert(CommandLineOptions.Clo.LazyInlining == 2); vcexpr = gen.Eq(expr, vcexpr); } @@ -293,7 +442,10 @@ namespace VC { new VCQuantifierInfos(impl.Name, QuantifierExpr.GetNextSkolemId(), false, q), vcexpr); info.vcexpr = vcexpr; - checker.TheoremProver.PushVCExpression(vcexpr); + if (CommandLineOptions.Clo.LazyInlining != 3) + { + checker.TheoremProver.PushVCExpression(vcexpr); + } } protected VCExpr GenerateReachVC(Implementation impl, LazyInliningInfo info, Checker ch) { @@ -1510,6 +1662,12 @@ namespace VC { VCExpr vc = parent.GenerateVCAux(impl, null, label2absy, checker); Contract.Assert(vc != null); + if (CommandLineOptions.Clo.LazyInlining == 3) + { + var bm = new BoundingVCMutator(checker.VCExprGen, interfaceVarCopies); + vc = bm.Mutate(vc, true); + } + if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) { reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, parent.implName2LazyInliningInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program); } else { -- cgit v1.2.3