From 5e0123996f7a79ea7d3576ef120b4c2cb2417a71 Mon Sep 17 00:00:00 2001 From: qadeer Date: Sat, 28 Apr 2012 16:26:12 -0700 Subject: eliminated LazyInliningInfo --- Source/VCGeneration/StratifiedVC.cs | 143 ++++++++++++++---------------------- 1 file changed, 56 insertions(+), 87 deletions(-) diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 758925fa..3bbe92a1 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -67,19 +67,51 @@ namespace VC return RECORD_TYPES.INT_BOOL; } - public class LazyInliningInfo { - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(impl != null); - Contract.Invariant(function != null); - Contract.Invariant(controlFlowVariable != null); - Contract.Invariant(assertExpr != null); - Contract.Invariant(cce.NonNullElements(interfaceVars)); - Contract.Invariant(incarnationOriginMap == null || cce.NonNullDictionaryAndValues(incarnationOriginMap)); + protected VCExpr GenerateReachVC(Implementation impl, StratifiedInliningInfo info, Checker ch) { + Variable controlFlowVariable = info.controlFlowVariable; + VCExpressionGenerator gen = ch.VCExprGen; + ProverContext proverCtxt = ch.TheoremProver.Context; + Boogie2VCExprTranslator translator = proverCtxt.BoogieExprTranslator; + VCExprVar controlFlowVariableExpr = translator.LookupVariable(controlFlowVariable); + + Block exitBlock = null; + Dictionary reachVars = new Dictionary(); + Dictionary reachExprs = new Dictionary(); + foreach (Block b in impl.Blocks) { + reachVars[b] = gen.Variable(b.Label + "_reachable", Bpl.Type.Bool); + reachExprs[b] = VCExpressionGenerator.False; + if (b.TransferCmd is ReturnCmd) + exitBlock = b; } + info.reachVars = reachVars; + foreach (Block b in impl.Blocks) { + foreach (Block pb in b.Predecessors) { + VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(pb.UniqueId))); + VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(b.UniqueId))); + reachExprs[b] = gen.Or(reachExprs[b], gen.And(reachVars[pb], controlTransferExpr)); + } + } + reachExprs[impl.Blocks[0]] = VCExpressionGenerator.True; + List bindings = new List(); + foreach (Block b in impl.Blocks) { + bindings.Add(gen.LetBinding(reachVars[b], reachExprs[b])); + } + info.reachVarBindings = bindings; + + Debug.Assert(exitBlock != null && exitBlock.Cmds.Length > 0); + AssertCmd assertCmd = (AssertCmd)exitBlock.Cmds[exitBlock.Cmds.Length - 1]; + Debug.Assert(assertCmd != null); + VCExpr exitFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(exitBlock.UniqueId))); + VCExpr exitTransferExpr = gen.Eq(exitFlowFunctionAppl, gen.Integer(BigNum.FromInt(assertCmd.UniqueId))); + VCExpr exitCondition = gen.And(info.reachVars[exitBlock], exitTransferExpr); + VCExpr errorExpr = gen.Eq(translator.LookupVariable(info.outputErrorVariable), gen.And(translator.LookupVariable(info.inputErrorVariable), exitCondition)); + VCExpr reachvcexpr = gen.Let(info.reachVarBindings, errorExpr); + return reachvcexpr; + } + + public class StratifiedInliningInfo { public Implementation impl; - public int uniqueId; public Function function; public Variable controlFlowVariable; public List interfaceVars; @@ -98,13 +130,20 @@ namespace VC public Variable inputErrorVariable; public Variable outputErrorVariable; - public LazyInliningInfo(Implementation impl, Program program, ProverContext ctxt, int uniqueId, GlobalVariable errorVariable) { + public bool initialized; + public int inline_cnt; + public List interfaceExprVars; + public VCExpr funcExpr; + public VCExpr falseExpr; + + public StratifiedInliningInfo(Implementation impl, Program program, ProverContext ctxt) { + Contract.Requires(impl != null); + Contract.Requires(program != null); Contract.Requires(impl != null); Contract.Requires(program != null); Procedure proc = cce.NonNull(impl.Proc); this.impl = impl; - this.uniqueId = uniqueId; this.controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int)); impl.LocVars.Add(controlFlowVariable); @@ -131,9 +170,6 @@ namespace VC Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v)); assertExpr = Expr.And(assertExpr, eqExpr); } - if (errorVariable != null) { - proc.Modifies.Add(new IdentifierExpr(Token.NoToken, errorVariable)); - } foreach (IdentifierExpr e in proc.Modifies) { Contract.Assert(e != null); if (e.Decl == null) @@ -170,81 +206,14 @@ namespace VC foreach (Variable v in interfaceVars) { Constant constant = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, v.Name + temp++, v.TypedIdent.Type)); interfaceVarCopies[i].Add(constant); - //program.TopLevelDeclarations.Add(constant); } } - } - } - protected VCExpr GenerateReachVC(Implementation impl, LazyInliningInfo info, Checker ch) { - Variable controlFlowVariable = info.controlFlowVariable; - VCExpressionGenerator gen = ch.VCExprGen; - ProverContext proverCtxt = ch.TheoremProver.Context; - Boogie2VCExprTranslator translator = proverCtxt.BoogieExprTranslator; - VCExprVar controlFlowVariableExpr = translator.LookupVariable(controlFlowVariable); - - Block exitBlock = null; - Dictionary reachVars = new Dictionary(); - Dictionary reachExprs = new Dictionary(); - foreach (Block b in impl.Blocks) { - reachVars[b] = gen.Variable(b.Label + "_reachable", Bpl.Type.Bool); - reachExprs[b] = VCExpressionGenerator.False; - if (b.TransferCmd is ReturnCmd) - exitBlock = b; - } - info.reachVars = reachVars; - - foreach (Block b in impl.Blocks) { - foreach (Block pb in b.Predecessors) { - VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(pb.UniqueId))); - VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(b.UniqueId))); - reachExprs[b] = gen.Or(reachExprs[b], gen.And(reachVars[pb], controlTransferExpr)); - } - } - reachExprs[impl.Blocks[0]] = VCExpressionGenerator.True; - List bindings = new List(); - foreach (Block b in impl.Blocks) { - bindings.Add(gen.LetBinding(reachVars[b], reachExprs[b])); + inline_cnt = 0; + privateVars = new List(); + interfaceExprVars = new List(); + initialized = false; } - info.reachVarBindings = bindings; - - Debug.Assert(exitBlock != null && exitBlock.Cmds.Length > 0); - AssertCmd assertCmd = (AssertCmd)exitBlock.Cmds[exitBlock.Cmds.Length - 1]; - Debug.Assert(assertCmd != null); - VCExpr exitFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(exitBlock.UniqueId))); - VCExpr exitTransferExpr = gen.Eq(exitFlowFunctionAppl, gen.Integer(BigNum.FromInt(assertCmd.UniqueId))); - VCExpr exitCondition = gen.And(info.reachVars[exitBlock], exitTransferExpr); - VCExpr errorExpr = gen.Eq(translator.LookupVariable(info.outputErrorVariable), gen.And(translator.LookupVariable(info.inputErrorVariable), exitCondition)); - VCExpr reachvcexpr = gen.Let(info.reachVarBindings, errorExpr); - return reachvcexpr; - } - - public class StratifiedInliningInfo : LazyInliningInfo - { - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(cce.NonNullElements(privateVars)); - Contract.Invariant(cce.NonNullElements(interfaceExprVars)); - } - - public bool initialized; - public int inline_cnt; - public List interfaceExprVars; - public VCExpr funcExpr; - public VCExpr falseExpr; - - public StratifiedInliningInfo(Implementation impl, Program program, ProverContext ctxt, int uniqueid) - : base(impl, program, ctxt, uniqueid, null) - { - Contract.Requires(impl != null); - Contract.Requires(program != null); - inline_cnt = 0; - privateVars = new List(); - interfaceExprVars = new List(); - initialized = false; - } - } public void GenerateVCsForStratifiedInlining(Program program) @@ -263,7 +232,7 @@ namespace VC Procedure proc = cce.NonNull(impl.Proc); if (proc.FindExprAttribute("inline") != null) { - StratifiedInliningInfo info = new StratifiedInliningInfo(impl, program, checker.TheoremProver.Context, QuantifierExpr.GetNextSkolemId()); + StratifiedInliningInfo info = new StratifiedInliningInfo(impl, program, checker.TheoremProver.Context); implName2StratifiedInliningInfo[impl.Name] = info; ExprSeq exprs = new ExprSeq(); -- cgit v1.2.3