diff options
Diffstat (limited to 'Source/VCGeneration/StratifiedVC.cs')
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 227 |
1 files changed, 127 insertions, 100 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 563cbf40..a2ad1bd3 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,44 +23,22 @@ namespace VC { public Dictionary<Block, List<StratifiedCallSite>> callSites;
public Dictionary<Block, List<StratifiedCallSite>> recordProcCallSites;
public VCExpr vcexpr;
- public Dictionary<Block, VCExprVar> reachVars;
+
+ // the following three fields are not being used at the moment
+ public VCExprVar entryExprVar;
+ public Dictionary<Block, Macro> reachMacros;
+ public Dictionary<Block, VCExpr> reachMacroDefinitions;
public StratifiedVC(StratifiedInliningInfo siInfo) {
info = siInfo;
info.GenerateVC();
- vcexpr = info.vcexpr;
var vcgen = info.vcgen;
var prover = vcgen.prover;
VCExpressionGenerator gen = prover.VCExprGen;
- var bet = prover.Context.BoogieExprTranslator;
- VCExpr controlFlowVariableExpr = bet.LookupVariable(info.controlFlowVariable);
+ var bet = prover.Context.BoogieExprTranslator;
+
+ vcexpr = info.vcexpr;
id = vcgen.CreateNewId();
- VCExpr eqExpr = gen.Eq(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));
- vcexpr = gen.And(eqExpr, vcexpr);
-
- var impl = info.impl;
- reachVars = new Dictionary<Block, VCExprVar>();
- Dictionary<Block, VCExpr> reachExprs = new Dictionary<Block, VCExpr>();
- foreach (Block b in impl.Blocks) {
- reachVars[b] = vcgen.CreateNewVar(Bpl.Type.Bool);
- reachExprs[b] = VCExpressionGenerator.False;
- }
- foreach (Block currBlock in impl.Blocks) {
- GotoCmd gotoCmd = currBlock.TransferCmd as GotoCmd;
- if (gotoCmd == null) continue;
- foreach (Block successorBlock in gotoCmd.labelTargets) {
- VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(currBlock.UniqueId)));
- VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(successorBlock.UniqueId)));
- reachExprs[successorBlock] = gen.Or(reachExprs[successorBlock], gen.And(reachVars[currBlock], controlTransferExpr));
- }
- }
- // The binding for entry block should be left defined;
- // it will get filled in when the call tree is constructed
- for (int i = 1; i < impl.Blocks.Count; i++) {
- Block b = impl.Blocks[i];
- vcexpr = gen.And(vcexpr, gen.Eq(reachVars[b], reachExprs[b]));
- }
-
interfaceExprVars = new List<VCExprVar>();
Dictionary<VCExprVar, VCExpr> substDict = new Dictionary<VCExprVar, VCExpr>();
foreach (VCExprVar v in info.interfaceExprVars) {
@@ -71,15 +49,35 @@ namespace VC { foreach (VCExprVar v in info.privateExprVars) {
substDict.Add(v, vcgen.CreateNewVar(v.Type));
}
+ substDict.Add(bet.LookupVariable(info.controlFlowVariable), gen.Integer(BigNum.FromInt(id)));
VCExprSubstitution subst = new VCExprSubstitution(substDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
SubstitutingVCExprVisitor substVisitor = new SubstitutingVCExprVisitor(prover.VCExprGen);
vcexpr = substVisitor.Mutate(vcexpr, subst);
+ var impl = info.impl;
+ reachMacros = new Dictionary<Block, Macro>();
+ reachMacroDefinitions = new Dictionary<Block, VCExpr>();
+ foreach (Block b in impl.Blocks) {
+ reachMacros[b] = vcgen.CreateNewMacro();
+ reachMacroDefinitions[b] = VCExpressionGenerator.False;
+ }
+ entryExprVar = vcgen.CreateNewVar(Microsoft.Boogie.Type.Bool);
+ reachMacroDefinitions[impl.Blocks[0]] = entryExprVar;
+ foreach (Block currBlock in impl.Blocks) {
+ GotoCmd gotoCmd = currBlock.TransferCmd as GotoCmd;
+ if (gotoCmd == null) continue;
+ foreach (Block successorBlock in gotoCmd.labelTargets) {
+ VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(BigNum.FromInt(id)), gen.Integer(BigNum.FromInt(currBlock.UniqueId)));
+ VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(successorBlock.UniqueId)));
+ reachMacroDefinitions[successorBlock] = gen.Or(reachMacroDefinitions[successorBlock], gen.And(gen.Function(reachMacros[currBlock]), controlTransferExpr));
+ }
+ }
+
callSites = new Dictionary<Block, List<StratifiedCallSite>>();
foreach (Block b in info.callSites.Keys) {
callSites[b] = new List<StratifiedCallSite>();
foreach (CallSite cs in info.callSites[b]) {
- callSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));
+ callSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst));
}
}
@@ -87,7 +85,7 @@ namespace VC { foreach (Block b in info.recordProcCallSites.Keys) {
recordProcCallSites[b] = new List<StratifiedCallSite>();
foreach (CallSite cs in info.recordProcCallSites[b]) {
- recordProcCallSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));
+ recordProcCallSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst));
}
}
}
@@ -103,6 +101,18 @@ namespace VC { return ret;
}
}
+
+ public List<StratifiedCallSite> RecordProcCallSites {
+ get {
+ var ret = new List<StratifiedCallSite>();
+ foreach (var b in recordProcCallSites.Keys) {
+ foreach (var cs in recordProcCallSites[b]) {
+ ret.Add(cs);
+ }
+ }
+ return ret;
+ }
+ }
}
public class CallSite {
@@ -110,9 +120,11 @@ namespace VC { public List<VCExpr> interfaceExprs;
public Block block;
public int numInstr; // for TraceLocation
- public CallSite(string callee, List<VCExpr> interfaceExprs, Block block, int numInstr) {
+ public VCExprVar callSiteVar;
+ public CallSite(string callee, List<VCExpr> interfaceExprs, VCExprVar callSiteVar, Block block, int numInstr) {
this.calleeName = callee;
this.interfaceExprs = interfaceExprs;
+ this.callSiteVar = callSiteVar;
this.block = block;
this.numInstr = numInstr;
}
@@ -121,26 +133,47 @@ namespace VC { public class StratifiedCallSite {
public CallSite callSite;
public List<VCExpr> interfaceExprs;
- public VCExprVar reachVar;
+ public VCExpr callSiteExpr;
- public StratifiedCallSite(CallSite cs, SubstitutingVCExprVisitor substVisitor, VCExprSubstitution subst, Dictionary<Block, VCExprVar> reachVars) {
+ public StratifiedCallSite(CallSite cs, SubstitutingVCExprVisitor substVisitor, VCExprSubstitution subst) {
callSite = cs;
interfaceExprs = new List<VCExpr>();
foreach (VCExpr v in cs.interfaceExprs) {
interfaceExprs.Add(substVisitor.Mutate(v, subst));
}
- reachVar = reachVars[cs.block];
+ if (callSite.callSiteVar != null)
+ callSiteExpr = substVisitor.Mutate(callSite.callSiteVar, subst);
}
public VCExpr Attach(StratifiedVC svc) {
Contract.Assert(interfaceExprs.Count == svc.interfaceExprVars.Count);
StratifiedInliningInfo info = svc.info;
- VCExpressionGenerator gen = info.vcgen.prover.VCExprGen;
- VCExpr ret = gen.Eq(reachVar, svc.reachVars[info.impl.Blocks[0]]);
- for (int i = 0; i < interfaceExprs.Count; i++) {
- ret = gen.And(ret, gen.Eq(interfaceExprs[i], svc.interfaceExprVars[i]));
+ ProverInterface prover = info.vcgen.prover;
+ VCExpressionGenerator gen = prover.VCExprGen;
+
+ Dictionary<VCExprVar, VCExpr> substDict = new Dictionary<VCExprVar, VCExpr>();
+ for (int i = 0; i < svc.interfaceExprVars.Count; i++) {
+ VCExprVar v = svc.interfaceExprVars[i];
+ substDict.Add(v, interfaceExprs[i]);
}
- return ret;
+ VCExprSubstitution subst = new VCExprSubstitution(substDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
+ SubstitutingVCExprVisitor substVisitor = new SubstitutingVCExprVisitor(prover.VCExprGen);
+ svc.vcexpr = substVisitor.Mutate(svc.vcexpr, subst);
+ foreach (StratifiedCallSite scs in svc.CallSites) {
+ List<VCExpr> newInterfaceExprs = new List<VCExpr>();
+ foreach (VCExpr expr in scs.interfaceExprs) {
+ newInterfaceExprs.Add(substVisitor.Mutate(expr, subst));
+ }
+ scs.interfaceExprs = newInterfaceExprs;
+ }
+ foreach (StratifiedCallSite scs in svc.RecordProcCallSites) {
+ List<VCExpr> newInterfaceExprs = new List<VCExpr>();
+ foreach (VCExpr expr in scs.interfaceExprs) {
+ newInterfaceExprs.Add(substVisitor.Mutate(expr, subst));
+ }
+ scs.interfaceExprs = newInterfaceExprs;
+ }
+ return gen.Implies(callSiteExpr, svc.vcexpr);
}
}
@@ -149,7 +182,7 @@ namespace VC { public Implementation impl;
public Function function;
public Variable controlFlowVariable;
- public Expr assertExpr;
+ public AssertCmd exitAssertCmd;
public VCExpr vcexpr;
public List<VCExprVar> interfaceExprVars;
public List<VCExprVar> privateExprVars;
@@ -209,7 +242,7 @@ namespace VC { public void GenerateVC() {
if (initialized) return;
List<Variable> outputVariables = new List<Variable>();
- assertExpr = new LiteralExpr(Token.NoToken, true);
+ Expr assertExpr = new LiteralExpr(Token.NoToken, true);
foreach (Variable v in impl.OutParams) {
Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));
outputVariables.Add(c);
@@ -224,26 +257,29 @@ namespace VC { Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
assertExpr = Expr.And(assertExpr, eqExpr);
}
- assertExpr = Expr.Not(assertExpr);
+ exitAssertCmd = new AssertCmd(Token.NoToken, Expr.Not(assertExpr));
Program program = vcgen.program;
ProverInterface proverInterface = vcgen.prover;
vcgen.ConvertCFG2DAG(impl);
- ModelViewInfo mvInfo;
vcgen.PassifyImpl(impl, out mvInfo);
- controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));
- impl.LocVars.Add(controlFlowVariable);
-
VCExpressionGenerator gen = proverInterface.VCExprGen;
var exprGen = proverInterface.Context.ExprGen;
var translator = proverInterface.Context.BoogieExprTranslator;
- VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : translator.LookupVariable(controlFlowVariable);
+ VCExpr controlFlowVariableExpr = null;
+ 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);
}
privateExprVars = new List<VCExprVar>();
@@ -265,51 +301,10 @@ namespace VC { interfaceExprVars.Add(translator.LookupVariable(v));
}
- callSites = vcgen.CollectCallSites(impl);
- recordProcCallSites = vcgen.CollectRecordProcedureCallSites(impl);
initialized = true;
}
}
- public class CallSitesSimplifier : StandardVisitor {
- VariableSeq localVars;
- StratifiedVCGenBase vcgen;
- public static void SimplifyCallSites(Implementation implementation, StratifiedVCGenBase vcgen) {
- CallSitesSimplifier visitor = new CallSitesSimplifier(vcgen);
- visitor.Visit(implementation);
- implementation.LocVars.AddRange(visitor.localVars);
- }
- private CallSitesSimplifier(StratifiedVCGenBase vcgen) {
- this.vcgen = vcgen;
- this.localVars = new VariableSeq();
- }
- public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {
- CmdSeq newCmdSeq = new CmdSeq();
- foreach (Cmd cmd in cmdSeq) {
- AssumeCmd assumeCmd = cmd as AssumeCmd;
- if (assumeCmd == null) {
- newCmdSeq.Add(cmd);
- continue;
- }
- NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
- if (naryExpr == null || !vcgen.implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) {
- newCmdSeq.Add(cmd);
- continue;
- }
-
- ExprSeq exprs = new ExprSeq();
- foreach (Expr e in naryExpr.Args) {
- LocalVariable newVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "CallSiteSimplification@" + localVars.Length, e.Type));
- localVars.Add(newVar);
- newCmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(newVar), e)));
- exprs.Add(Expr.Ident(newVar));
- }
- newCmdSeq.Add(new AssumeCmd(Token.NoToken, new NAryExpr(Token.NoToken, naryExpr.Fun, exprs)));
- }
- return newCmdSeq;
- }
- }
-
public abstract class StratifiedVCGenBase : VCGen {
public readonly static string recordProcName = "boogie_si_record";
public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
@@ -362,11 +357,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<Block, List<CallSite>> CollectCallSites(Implementation implementation) {
var callSites = new Dictionary<Block, List<CallSite>>();
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;
@@ -375,7 +392,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<CallSite>();
callSites[block].Add(cs);
@@ -397,7 +418,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<CallSite>();
callSites[block].Add(cs);
@@ -406,10 +427,16 @@ namespace VC { return callSites;
}
- private int newVarCountForStratifiedInlining = 0;
+ private int macroCountForStratifiedInlining = 0;
+ public Macro CreateNewMacro() {
+ string newName = "StratifiedInliningMacro@" + macroCountForStratifiedInlining.ToString();
+ macroCountForStratifiedInlining++;
+ return new Macro(Token.NoToken, newName, new VariableSeq(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool), false));
+ }
+ private int varCountForStratifiedInlining = 0;
public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {
- string newName = "StratifiedInlining@" + newVarCountForStratifiedInlining.ToString();
- newVarCountForStratifiedInlining++;
+ string newName = "StratifiedInliningVar@" + varCountForStratifiedInlining.ToString();
+ varCountForStratifiedInlining++;
Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));
prover.Context.DeclareConstant(newVar, false, null);
return prover.VCExprGen.Variable(newVar.Name, type);
@@ -422,9 +449,9 @@ namespace VC { // Used inside PassifyImpl
protected override void addExitAssert(string implName, Block exitBlock) {
if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(implName)) {
- Expr assertExpr = implName2StratifiedInliningInfo[implName].assertExpr;
- Contract.Assert(assertExpr != null);
- exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));
+ AssertCmd exitAssertCmd = implName2StratifiedInliningInfo[implName].exitAssertCmd;
+ Contract.Assert(exitAssertCmd != null);
+ exitBlock.Cmds.Add(exitAssertCmd);
}
}
|