From 7a69b4c9cbe9ac05738ffb22df48e361c088c7c6 Mon Sep 17 00:00:00 2001 From: qadeer Date: Tue, 12 Jun 2012 10:36:25 -0700 Subject: refactoring in SI --- Source/VCGeneration/StratifiedVC.cs | 111 +++++++++++++++--------------------- 1 file changed, 45 insertions(+), 66 deletions(-) (limited to 'Source') diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 3900499b..414fda1e 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -15,7 +15,7 @@ using Microsoft.Boogie.VCExprAST; namespace VC { using Bpl = Microsoft.Boogie; - + public class StratifiedVC { public StratifiedInliningInfo info; public int id; @@ -23,6 +23,8 @@ namespace VC { public Dictionary> callSites; public Dictionary> recordProcCallSites; public VCExpr vcexpr; + + // the following three fields are not being used at the moment public VCExprVar entryExprVar; public Dictionary reachMacros; public Dictionary reachMacroDefinitions; @@ -75,21 +77,7 @@ namespace VC { foreach (Block b in info.callSites.Keys) { callSites[b] = new List(); foreach (CallSite cs in info.callSites[b]) { - VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(BigNum.FromInt(id)), gen.Integer(BigNum.FromInt(b.UniqueId))); - // VCExpr blockExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.ZERO)); - VCExpr unblockExpr; - GotoCmd gotoCmd = b.TransferCmd as GotoCmd; - if (gotoCmd == null) { - AssertCmd assertCmd = (AssertCmd) b.Cmds[b.Cmds.Length-1]; - unblockExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(-assertCmd.UniqueId))); - } - else { - unblockExpr = VCExpressionGenerator.False; - foreach (Block nextBlock in gotoCmd.labelTargets) { - unblockExpr = gen.Or(unblockExpr, gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(nextBlock.UniqueId)))); - } - } - callSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, gen.Function(reachMacros[cs.block]), gen.Not(unblockExpr))); + callSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst)); } } @@ -97,21 +85,7 @@ namespace VC { foreach (Block b in info.recordProcCallSites.Keys) { recordProcCallSites[b] = new List(); foreach (CallSite cs in info.recordProcCallSites[b]) { - VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(BigNum.FromInt(id)), gen.Integer(BigNum.FromInt(b.UniqueId))); - // VCExpr blockExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.ZERO)); - VCExpr unblockExpr; - GotoCmd gotoCmd = b.TransferCmd as GotoCmd; - if (gotoCmd == null) { - AssertCmd assertCmd = (AssertCmd)b.Cmds[b.Cmds.Length - 1]; - unblockExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(-assertCmd.UniqueId))); - } - else { - unblockExpr = VCExpressionGenerator.False; - foreach (Block nextBlock in gotoCmd.labelTargets) { - unblockExpr = gen.Or(unblockExpr, gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(nextBlock.UniqueId)))); - } - } - recordProcCallSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, gen.Function(reachMacros[cs.block]), gen.Not(unblockExpr))); + recordProcCallSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst)); } } } @@ -146,9 +120,11 @@ namespace VC { public List interfaceExprs; public Block block; public int numInstr; // for TraceLocation - public CallSite(string callee, List interfaceExprs, Block block, int numInstr) { + public VCExprVar callSiteVar; + public CallSite(string callee, List interfaceExprs, VCExprVar callSiteVar, Block block, int numInstr) { this.calleeName = callee; this.interfaceExprs = interfaceExprs; + this.callSiteVar = callSiteVar; this.block = block; this.numInstr = numInstr; } @@ -157,18 +133,16 @@ namespace VC { public class StratifiedCallSite { public CallSite callSite; public List interfaceExprs; - public VCExpr reachExpr; - public VCExpr blockExpr; + public VCExpr callSiteExpr; - public StratifiedCallSite(CallSite cs, SubstitutingVCExprVisitor substVisitor, VCExprSubstitution subst, - VCExpr reachExpression, VCExpr blockExpression) { + public StratifiedCallSite(CallSite cs, SubstitutingVCExprVisitor substVisitor, VCExprSubstitution subst) { callSite = cs; interfaceExprs = new List(); foreach (VCExpr v in cs.interfaceExprs) { interfaceExprs.Add(substVisitor.Mutate(v, subst)); } - reachExpr = reachExpression; - blockExpr = blockExpression; + if (callSite.callSiteVar != null) + callSiteExpr = substVisitor.Mutate(callSite.callSiteVar, subst); } public VCExpr Attach(StratifiedVC svc) { @@ -199,16 +173,7 @@ namespace VC { } scs.interfaceExprs = newInterfaceExprs; } - return gen.Or(blockExpr, svc.vcexpr); - - /* - VCExpr ret = svc.vcexpr; - for (int i = 0; i < interfaceExprs.Count; i++) { - ret = gen.And(ret, gen.Eq(interfaceExprs[i], svc.interfaceExprVars[i])); - } - ret = gen.Or(blockExpr, ret); - return ret; - */ + return gen.Implies(callSiteExpr, svc.vcexpr); } } @@ -225,7 +190,6 @@ namespace VC { public ModelViewInfo mvInfo; public Dictionary> callSites; public Dictionary> recordProcCallSites; - public IEnumerable sortedBlocks; public bool initialized { get; private set; } public StratifiedInliningInfo(Implementation implementation, StratifiedVCGenBase stratifiedVcGen) { @@ -307,26 +271,17 @@ namespace VC { if (!CommandLineOptions.Clo.UseLabels) { controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int)); controlFlowVariableExpr = translator.LookupVariable(controlFlowVariable); + vcgen.InstrumentCallSites(impl); } vcexpr = gen.Not(vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context)); if (controlFlowVariableExpr != null) { VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, exprGen.Integer(BigNum.ZERO)); VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId))); vcexpr = exprGen.And(eqExpr, vcexpr); + callSites = vcgen.CollectCallSites(impl); + recordProcCallSites = vcgen.CollectRecordProcedureCallSites(impl); } - Graph dag = new Graph(); - dag.AddSource(impl.Blocks[0]); - foreach (Block b in impl.Blocks) { - GotoCmd gtc = b.TransferCmd as GotoCmd; - if (gtc != null) { - foreach (Block dest in gtc.labelTargets) { - dag.AddEdge(b, dest); - } - } - } - sortedBlocks = dag.TopologicalSort(); - privateExprVars = new List(); foreach (Variable v in impl.LocVars) { privateExprVars.Add(translator.LookupVariable(v)); @@ -346,8 +301,6 @@ namespace VC { interfaceExprVars.Add(translator.LookupVariable(v)); } - callSites = vcgen.CollectCallSites(impl); - recordProcCallSites = vcgen.CollectRecordProcedureCallSites(impl); initialized = true; } } @@ -443,11 +396,33 @@ namespace VC { base.Close(); } + public void InstrumentCallSites(Implementation implementation) { + var callSiteId = 0; + foreach (Block block in implementation.Blocks) { + CmdSeq newCmds = new CmdSeq(); + for (int i = 0; i < block.Cmds.Length; i++) { + Cmd cmd = block.Cmds[i]; + newCmds.Add(cmd); + AssumeCmd assumeCmd = cmd as AssumeCmd; + if (assumeCmd == null) continue; + NAryExpr naryExpr = assumeCmd.Expr as NAryExpr; + if (naryExpr == null) continue; + if (!implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) continue; + Variable callSiteVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "StratifiedInliningCallSite" + callSiteId, Microsoft.Boogie.Type.Bool)); + implementation.LocVars.Add(callSiteVar); + newCmds.Add(new AssumeCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, callSiteVar))); + callSiteId++; + } + block.Cmds = newCmds; + } + } + public Dictionary> CollectCallSites(Implementation implementation) { var callSites = new Dictionary>(); foreach (Block block in implementation.Blocks) { for (int i = 0; i < block.Cmds.Length; i++) { - AssumeCmd assumeCmd = block.Cmds[i] as AssumeCmd; + Cmd cmd = block.Cmds[i]; + AssumeCmd assumeCmd = cmd as AssumeCmd; if (assumeCmd == null) continue; NAryExpr naryExpr = assumeCmd.Expr as NAryExpr; if (naryExpr == null) continue; @@ -456,7 +431,11 @@ namespace VC { foreach (Expr e in naryExpr.Args) { interfaceExprs.Add(prover.Context.BoogieExprTranslator.Translate(e)); } - CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, block, i); + int instr = i; + i++; + AssumeCmd callSiteAssumeCmd = (AssumeCmd)block.Cmds[i]; + IdentifierExpr iexpr = (IdentifierExpr) callSiteAssumeCmd.Expr; + CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, prover.Context.BoogieExprTranslator.LookupVariable(iexpr.Decl), block, instr); if (!callSites.ContainsKey(block)) callSites[block] = new List(); callSites[block].Add(cs); @@ -478,7 +457,7 @@ namespace VC { foreach (Expr e in naryExpr.Args) { interfaceExprs.Add(prover.Context.BoogieExprTranslator.Translate(e)); } - CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, block, i); + CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, null, block, i); if (!callSites.ContainsKey(block)) callSites[block] = new List(); callSites[block].Add(cs); -- cgit v1.2.3