diff options
| author |  akashlal <unknown> | 2010-07-19 10:47:42 +0000 |
|---|---|---|
| committer | akashlal <unknown> | 2010-07-19 10:47:42 +0000 |
| commit | 6ff0ab85e8a9a5516cc175544b0760a9780c01b2 (patch) | |
| tree | b89b33416f4922e0ef387b4e1c14bd9c35971c57 | |
| parent | 9295a538d5628a7384495c97260b0c885bab01f0 (diff) | |
Boogie: Added interprocedural live variable analysis. Flag to turn it on: "/liveVariableAnalysis:2"
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 7 | ||||
| -rw-r--r-- | Source/Core/DeadVarElim.ssc | 883 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.ssc | 174 |
3 files changed, 1040 insertions, 24 deletions
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index 6a0c274a..70de931f 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -236,7 +236,7 @@ namespace Microsoft.Boogie public bool ReflectAdd = false;
- public bool LiveVariableAnalysis = true;
+ public int LiveVariableAnalysis = 1;
// Static constructor
static CommandLineOptions()
@@ -840,8 +840,8 @@ namespace Microsoft.Boogie case "-liveVariableAnalysis":
case "/liveVariableAnalysis": {
int lva = 0;
- if (ps.GetNumericArgument(ref lva, 2)) {
- LiveVariableAnalysis = lva == 1;
+ if (ps.GetNumericArgument(ref lva, 3)) {
+ LiveVariableAnalysis = lva;
}
break;
}
@@ -1945,6 +1945,7 @@ namespace Microsoft.Boogie /liveVariableAnalysis:<c> : 0 = do not perform live variable analysis
1 = perform live variable analysis (default)
+ 2 = perform interprocedural live variable analysis
/noVerify : skip VC generation and invocation of the theorem prover
/removeEmptyBlocks:<c> : 0 - do not remove empty blocks during VC generation
1 - remove empty blocks (default)
diff --git a/Source/Core/DeadVarElim.ssc b/Source/Core/DeadVarElim.ssc index 0686212e..4e3a431f 100644 --- a/Source/Core/DeadVarElim.ssc +++ b/Source/Core/DeadVarElim.ssc @@ -1,6 +1,8 @@ using System;
using System.Collections.Generic;
using Graphing;
+using PureCollections;
+using Microsoft.Contracts;
namespace Microsoft.Boogie
{
@@ -130,13 +132,29 @@ namespace Microsoft.Boogie public class VariableCollector : StandardVisitor {
public System.Collections.Generic.Set<Variable!>! usedVars;
+ public System.Collections.Generic.Set<Variable!>! oldVarsUsed;
+ int insideOldExpr;
+
public VariableCollector() {
usedVars = new System.Collections.Generic.Set<Variable!>();
+ oldVarsUsed = new System.Collections.Generic.Set<Variable!>();
+ insideOldExpr = 0;
}
+ public override Expr! VisitOldExpr(OldExpr! node)
+ {
+ insideOldExpr ++;
+ node.Expr = this.VisitExpr(node.Expr);
+ insideOldExpr --;
+ return node;
+ }
+
public override Expr! VisitIdentifierExpr(IdentifierExpr! node) {
if (node.Decl != null) {
usedVars.Add(node.Decl);
+ if(insideOldExpr > 0) {
+ oldVarsUsed.Add(node.Decl);
+ }
}
return node;
}
@@ -260,20 +278,29 @@ namespace Microsoft.Boogie liveVarsAfter.AddRange(succ.liveVarsBefore);
}
}
- }
+ }
CmdSeq cmds = block.Cmds;
int len = cmds.Length;
for (int i = len - 1; i >= 0; i--) {
+ if(cmds[i] is CallCmd) {
+ Procedure! proc = (!)((CallCmd!)cmds[i]).Proc;
+ if(InterProcGenKill.HasSummary(proc.Name)) {
+ liveVarsAfter =
+ InterProcGenKill.PropagateLiveVarsAcrossCall((CallCmd!)cmds[i], liveVarsAfter);
+ continue;
+ }
+ }
Propagate(cmds[i], liveVarsAfter);
}
block.liveVarsBefore = liveVarsAfter;
+
}
}
// perform in place update of liveSet
- private static void Propagate(Cmd! cmd, Set<Variable!>! liveSet) {
+ public static void Propagate(Cmd! cmd, Set<Variable!>! liveSet) {
if (cmd is AssignCmd) {
AssignCmd! assignCmd = (AssignCmd) cmd;
// I must first iterate over all the targets and remove the live ones.
@@ -352,4 +379,856 @@ namespace Microsoft.Boogie }
}
}
+
+ /*
+ // An idempotent semiring interface
+ abstract public class Weight {
+ abstract public Weight! one();
+ abstract public Weight! zero();
+ abstract public Weight! extend(Weight! w1, Weight! w2);
+ abstract public Weight! combine(Weight! w1, Weight! w2);
+ abstract public Weight! isEqual(Weight! w);
+ abstract public Weight! projectLocals()
+ }
+ */
+
+ // Weight domain for LiveVariableAnalysis (Gen/Kill)
+
+ public class GenKillWeight {
+ // lambda S. (S - kill) union gen
+ Set<Variable!>! gen;
+ Set<Variable!>! kill;
+ bool isZero;
+
+ public static GenKillWeight! oneWeight = new GenKillWeight(new Set<Variable!>(), new Set<Variable!>());
+ public static GenKillWeight! zeroWeight = new GenKillWeight();
+
+ // initializes to zero
+ public GenKillWeight() {
+ this.isZero = true;
+ this.gen = new Set<Variable!>();
+ this.kill = new Set<Variable!>();
+ }
+
+ public GenKillWeight(Set<Variable!> gen, Set<Variable!> kill) {
+ assert gen != null;
+ assert kill != null;
+ this.gen = gen;
+ this.kill = kill;
+ this.isZero = false;
+ }
+
+ public static GenKillWeight! one() {
+ return oneWeight;
+ }
+
+ public static GenKillWeight! zero() {
+ return zeroWeight;
+ }
+
+ public static GenKillWeight! extend(GenKillWeight! w1, GenKillWeight! w2) {
+ if(w1.isZero || w2.isZero) return zero();
+
+ return new GenKillWeight(w1.gen.Union(w2.gen.Difference(w1.kill)), w1.kill.Union(w2.kill));
+ }
+
+ public static GenKillWeight! combine(GenKillWeight! w1, GenKillWeight! w2) {
+ if(w1.isZero) return w2;
+ if(w2.isZero) return w1;
+
+ return new GenKillWeight(w1.gen.Union(w2.gen), w1.kill.Intersection(w2.kill));
+ }
+
+ public static GenKillWeight! projectLocals(GenKillWeight! w) {
+ Set<Variable!> gen = w.gen.FindAll(isGlobal);
+ Set<Variable!> kill = w.kill.FindAll(isGlobal);
+
+ return new GenKillWeight(gen, kill);
+ }
+
+ public static bool isEqual(GenKillWeight! w1, GenKillWeight! w2) {
+ if(w1.isZero) return w2.isZero;
+ if(w2.isZero) return w1.isZero;
+
+ return (w1.gen.Equals(w2.gen) && w1.kill.Equals(w2.kill));
+ }
+
+ private static bool isGlobal(Variable! v)
+ {
+ return (v is GlobalVariable);
+ }
+
+ [Pure]
+ public override string! ToString() {
+ return string.Format("({0},{1})", gen.ToString(), kill.ToString());
+ }
+
+ public Set<Variable!>! getLiveVars() {
+ return gen;
+ }
+
+ public Set<Variable!>! getLiveVars(Set<Variable!>! lv) {
+ Set<Variable!>! temp = (!)lv.Difference(kill);
+ return (!)temp.Union(gen);
+ }
+
+ }
+
+ public class ICFG
+ {
+ public Graph<Block!>! graph;
+ // Map from procedure to the list of blocks that call that procedure
+ public Dictionary<string!, List<Block!>!>! procsCalled;
+ public Set<Block!>! nodes;
+ public Dictionary<Block!, Set<Block!>!>! succEdges;
+ public Dictionary<Block!, Set<Block!>!>! predEdges;
+ private Dictionary<Block!, int>! priority;
+
+ public Set<Block!>! srcNodes;
+ public Set<Block!>! exitNodes;
+
+ public Dictionary<Block!, GenKillWeight!>! weightBefore;
+ public Dictionary<Block!, GenKillWeight!>! weightAfter;
+ public Dictionary<Block!, Set<Variable!>!>! liveVarsAfter;
+ public Dictionary<Block!, Set<Variable!>!>! liveVarsBefore;
+
+ public GenKillWeight! summary;
+ public Implementation! impl;
+
+ [NotDelayed]
+ public ICFG(Implementation! impl) {
+ this.graph = new Graph<Block!>();
+ this.procsCalled = new Dictionary<string!, List<Block!>!>();
+ this.nodes = new Set<Block!>();
+ this.succEdges = new Dictionary<Block!, Set<Block!>!>();
+ this.predEdges = new Dictionary<Block!, Set<Block!>!>();
+
+ this.priority = new Dictionary<Block!, int>();
+
+ this.srcNodes = new Set<Block!>();
+ this.exitNodes = new Set<Block!>();
+
+ this.weightBefore = new Dictionary<Block!, GenKillWeight!>();
+ this.weightAfter = new Dictionary<Block!, GenKillWeight!>();
+ this.liveVarsAfter = new Dictionary<Block!, Set<Variable!>!>();
+ this.liveVarsBefore = new Dictionary<Block!, Set<Variable!>!>();
+
+ summary = GenKillWeight.zero();
+ this.impl = impl;
+
+ base();
+
+ Initialize(impl);
+
+ }
+
+ private void Initialize(Implementation! impl) {
+ addSource(impl.Blocks[0]);
+ graph.AddSource(impl.Blocks[0]);
+
+ foreach(Block! b in impl.Blocks) {
+ if(b.TransferCmd is ReturnCmd) {
+ exitNodes.Add(b);
+ } else {
+ GotoCmd gc = b.TransferCmd as GotoCmd;
+ assert gc != null;
+ assert gc.labelTargets != null;
+ foreach(Block! t in gc.labelTargets) {
+ addEdge(b,t);
+ graph.AddEdge(b,t);
+ }
+ }
+
+ weightBefore[b] = GenKillWeight.zero();
+ weightAfter[b] = GenKillWeight.zero();
+
+ foreach(Cmd! c in b.Cmds) {
+ if(c is CallCmd) {
+ CallCmd! cc = (CallCmd!)c;
+ assert cc.Proc != null;
+ string! procName = cc.Proc.Name;
+ if(!procsCalled.ContainsKey(procName)) {
+ procsCalled.Add(procName, new List<Block!>());
+ }
+ procsCalled[procName].Add(b);
+ }
+ }
+ }
+
+ List<Block>! sortedNodes;
+ bool acyclic;
+
+ graph.TarjanTopSort(out acyclic, out sortedNodes);
+
+ if(!acyclic) {
+ Console.WriteLine("Warning: graph is not a dag");
+ }
+
+ int num = sortedNodes.Count;
+ foreach(Block! b in sortedNodes) {
+ priority.Add(b,num);
+ num--;
+ }
+
+ }
+
+ public int getPriority(Block! b) {
+ if(priority.ContainsKey(b)) return priority[b];
+ return Int32.MaxValue;
+ }
+
+ private void addSource(Block! b) {
+ registerNode(b);
+ this.srcNodes.Add(b);
+ }
+
+ private void addExit(Block! b) {
+ registerNode(b);
+ this.exitNodes.Add(b);
+ }
+
+ private void registerNode(Block! b) {
+ if(!succEdges.ContainsKey(b)) {
+ succEdges.Add(b, new Set<Block!>());
+ }
+
+ if(!predEdges.ContainsKey(b)) {
+ predEdges.Add(b, new Set<Block!>());
+ }
+
+ nodes.Add(b);
+ }
+
+ private void addEdge(Block! src, Block! tgt) {
+ registerNode(src);
+ registerNode(tgt);
+
+ succEdges[src].Add(tgt);
+ predEdges[tgt].Add(src);
+ }
+
+
+ }
+
+ // Interprocedural Gen/Kill Analysis
+ public class InterProcGenKill
+ {
+ Program! program;
+ Dictionary<string!, ICFG!>! procICFG;
+ Dictionary<string!, Procedure!>! name2Proc;
+ Dictionary<string!, List<WorkItem!>!>! callers;
+ Graph<string!>! callGraph;
+ Dictionary<string!, int>! procPriority;
+ int maxBlocksInProc;
+
+ WorkList! workList;
+
+ Implementation! mainImpl;
+
+ static Dictionary<string!, Set<Variable!>!>! varsLiveAtExit = new Dictionary<string!, Set<Variable!>!>();
+ static Dictionary<string!, Set<Variable!>!>! varsLiveAtEntry = new Dictionary<string!, Set<Variable!>!>();
+ static Dictionary<string!, GenKillWeight!>! varsLiveSummary = new Dictionary<string!, GenKillWeight!>();
+
+ [NotDelayed]
+ public InterProcGenKill(Implementation! impl, Program! program) {
+ this.program = program;
+ procICFG = new Dictionary<string!, ICFG!>();
+ name2Proc = new Dictionary<string!, Procedure!>();
+ workList = new WorkList();
+ this.callers = new Dictionary<string!, List<WorkItem!>!>();
+ this.callGraph = new Graph<string!>();
+ this.procPriority = new Dictionary<string!, int>();
+ this.maxBlocksInProc = 0;
+ this.mainImpl = impl;
+
+ Dictionary<string!, Implementation!>! name2Impl = new Dictionary<string!, Implementation!>();
+ varsLiveAtExit.Clear();
+ varsLiveAtEntry.Clear();
+ varsLiveSummary.Clear();
+
+ base();
+
+ foreach(Declaration! decl in program.TopLevelDeclarations) {
+ if(decl is Implementation) {
+ Implementation! imp = (Implementation!)decl;
+ name2Impl[imp.Name] = imp;
+ } else if(decl is Procedure) {
+ Procedure! proc = (!)(decl as Procedure);
+ name2Proc[proc.Name] = proc;
+ }
+ }
+
+ ICFG! mainICFG = new ICFG(mainImpl);
+ procICFG.Add(mainICFG.impl.Name, mainICFG);
+ callGraph.AddSource(mainICFG.impl.Name);
+
+ List<ICFG!>! procsToConsider = new List<ICFG!>();
+ procsToConsider.Add(mainICFG);
+
+ while(procsToConsider.Count != 0) {
+ ICFG! p = procsToConsider[0];
+ procsToConsider.RemoveAt(0);
+
+ foreach(string! callee in p.procsCalled.Keys) {
+ if(!name2Impl.ContainsKey(callee)) continue;
+
+ callGraph.AddEdge(p.impl.Name, callee);
+
+ if(maxBlocksInProc < p.nodes.Count) {
+ maxBlocksInProc = p.nodes.Count;
+ }
+
+ if(!callers.ContainsKey(callee)) {
+ callers.Add(callee, new List<WorkItem!>());
+ }
+ foreach(Block! b in p.procsCalled[callee]) {
+ callers[callee].Add(new WorkItem(p, b));
+ }
+
+ if(procICFG.ContainsKey(callee)) continue;
+ ICFG! ncfg = new ICFG(name2Impl[callee]);
+ procICFG.Add(callee, ncfg);
+ procsToConsider.Add(ncfg);
+ }
+ }
+
+ bool acyclic;
+ List<string>! sortedNodes;
+ callGraph.TarjanTopSort(out acyclic, out sortedNodes);
+
+ assert acyclic;
+
+ int cnt = 0;
+ for(int i = sortedNodes.Count - 1; i >= 0; i--) {
+ string s = sortedNodes[i];
+ if(s == null) continue;
+ procPriority.Add(s, cnt);
+ cnt++;
+ }
+
+ }
+
+ public static Set<Variable!>! GetVarsLiveAtExit(Implementation! impl, Program! prog) {
+ if(varsLiveAtExit.ContainsKey(impl.Name)) {
+ return varsLiveAtExit[impl.Name];
+ }
+ // Return default: all globals and out params
+ Set<Variable!>! lv = new Set<Variable!>();
+ foreach(Variable! v in prog.GlobalVariables()) {
+ lv.Add(v);
+ }
+ foreach(Variable! v in impl.OutParams) {
+ lv.Add(v);
+ }
+ return lv;
+ }
+
+ public static Set<Variable!>! GetVarsLiveAtEntry(Implementation! impl, Program! prog) {
+ if(varsLiveAtEntry.ContainsKey(impl.Name)) {
+ return varsLiveAtEntry[impl.Name];
+ }
+ // Return default: all globals and in params
+ Set<Variable!>! lv = new Set<Variable!>();
+ foreach(Variable! v in prog.GlobalVariables()) {
+ lv.Add(v);
+ }
+ foreach(Variable! v in impl.InParams) {
+ lv.Add(v);
+ }
+ return lv;
+ }
+
+ public static bool HasSummary(string! name) {
+ return varsLiveSummary.ContainsKey(name);
+ }
+
+ public static Set<Variable!>! PropagateLiveVarsAcrossCall(CallCmd! cmd, Set<Variable!>! lvAfter) {
+ Procedure! proc = (!)cmd.Proc;
+ if(varsLiveSummary.ContainsKey(proc.Name)) {
+ GenKillWeight! w1 = getWeightBeforeCall(cmd);
+ GenKillWeight! w2 = varsLiveSummary[proc.Name];
+ GenKillWeight! w3 = getWeightAfterCall(cmd);
+ GenKillWeight! w = GenKillWeight.extend(w1, GenKillWeight.extend(w2, w3));
+ return w.getLiveVars(lvAfter);
+ }
+ Set<Variable!>! ret = new Set<Variable!>();
+ ret.AddRange(lvAfter);
+ LiveVariableAnalysis.Propagate(cmd, ret);
+ return ret;
+ }
+
+ class WorkItem {
+ public ICFG! cfg;
+ public Block! block;
+
+ public WorkItem(ICFG! cfg, Block! block) {
+ this.cfg = cfg;
+ this.block = block;
+ }
+
+ public GenKillWeight! getWeightAfter() {
+ return cfg.weightAfter[block];
+ }
+
+ public bool setWeightBefore(GenKillWeight! w) {
+ GenKillWeight! prev = cfg.weightBefore[block];
+ GenKillWeight! curr = GenKillWeight.combine(w, prev);
+ if(GenKillWeight.isEqual(prev, curr)) return false;
+ cfg.weightBefore[block] = curr;
+ return true;
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object other)
+ {
+ WorkItem! wi = (WorkItem!)(other);
+ return (wi.cfg == cfg && wi.block == block);
+ }
+
+ [Pure]
+ public override int GetHashCode()
+ {
+ return 0;
+ }
+
+ public string! getLabel() {
+ return cfg.impl.Name + "::" + block.Label;
+ }
+
+ }
+
+ private void AddToWorkList(WorkItem! wi) {
+ int i = procPriority[wi.cfg.impl.Name];
+ int j = wi.cfg.getPriority(wi.block);
+ int priority = (i * maxBlocksInProc) + j;
+
+ workList.Add(wi, priority);
+ }
+
+ private void AddToWorkListReverse(WorkItem! wi) {
+ int i = procPriority[wi.cfg.impl.Name];
+ int j = wi.cfg.getPriority(wi.block);
+ int priority = (procPriority.Count - i) * maxBlocksInProc + j;
+ workList.Add(wi, priority);
+ }
+
+ class WorkList {
+ SortedList<int,int>! priorities;
+ Set<string!>! labels;
+
+ Dictionary<int, List<WorkItem!>!>! workList;
+
+ public WorkList() {
+ labels = new Set<string!>();
+ priorities = new SortedList<int,int>();
+ workList = new Dictionary<int, List<WorkItem!>!>();
+ }
+
+ public void Add(WorkItem! wi, int priority) {
+ string! lab = wi.getLabel();
+ if(labels.Contains(lab)) {
+ // Already on worklist
+ return;
+ }
+ labels.Add(lab);
+ if(!workList.ContainsKey(priority)) {
+ workList.Add(priority, new List<WorkItem!>());
+ }
+ workList[priority].Add(wi);
+ if(!priorities.ContainsKey(priority)) {
+ priorities.Add(priority,0);
+ }
+
+ priorities[priority] = priorities[priority] + 1;
+ }
+
+ public WorkItem! Get() {
+ // Get minimum priority
+ int p = ((!)priorities.Keys)[0];
+ priorities[p] = priorities[p] - 1;
+ if(priorities[p] == 0) {
+ priorities.Remove(p);
+ }
+
+ // Get a WI with this priority
+ WorkItem! wi = workList[p][0];
+ workList[p].RemoveAt(0);
+
+ // update labels
+ labels.Remove(wi.getLabel());
+ return wi;
+ }
+
+ public int Count {
+ get {
+ return labels.Count;
+ }
+ }
+ }
+
+ private GenKillWeight! getSummary(CallCmd! cmd) {
+ assert cmd.Proc != null;
+ string! procName = cmd.Proc.Name;
+ if(procICFG.ContainsKey(procName)) {
+ ICFG! cfg = procICFG[procName];
+ return GenKillWeight.projectLocals(cfg.summary);
+ }
+ assert false;
+ }
+
+ public static void ComputeLiveVars(Implementation! impl, Program !prog) {
+ InterProcGenKill! ipgk = new InterProcGenKill(impl, prog);
+ ipgk.Compute();
+ }
+
+ public void Compute() {
+ // Put all exit nodes in the worklist
+ foreach(ICFG! cfg in procICFG.Values) {
+ foreach(Block! eb in cfg.exitNodes) {
+ WorkItem! wi = new WorkItem(cfg, eb);
+ cfg.weightAfter[eb] = GenKillWeight.one();
+ AddToWorkList(wi);
+ }
+ }
+
+ while(workList.Count != 0) {
+ WorkItem! wi = workList.Get();
+ process(wi);
+ }
+
+ // Propagate LV to all procedures
+ foreach(ICFG! cfg in procICFG.Values) {
+ foreach(Block! b in cfg.nodes) {
+ cfg.liveVarsAfter.Add(b, new Set<Variable!>());
+ cfg.liveVarsBefore.Add(b, new Set<Variable!>());
+ }
+ }
+
+ ICFG! mainCfg = procICFG[mainImpl.Name];
+ foreach(Block! eb in mainCfg.exitNodes) {
+ WorkItem! wi = new WorkItem(mainCfg, eb);
+ AddToWorkListReverse(wi);
+ }
+
+ while(workList.Count != 0) {
+ WorkItem! wi = workList.Get();
+ processLV(wi);
+ }
+
+ // Set live variable info
+ foreach(ICFG! cfg in procICFG.Values) {
+ Set<Variable!>! lv = new Set<Variable!>();
+ foreach(Block! eb in cfg.exitNodes) {
+ lv.AddRange(cfg.liveVarsAfter[eb]);
+ }
+ varsLiveAtExit.Add(cfg.impl.Name, lv);
+ lv = new Set<Variable!>();
+ foreach(Block! eb in cfg.srcNodes) {
+ lv.AddRange(cfg.liveVarsBefore[eb]);
+ }
+ varsLiveAtEntry.Add(cfg.impl.Name, lv);
+ varsLiveSummary.Add(cfg.impl.Name, cfg.summary);
+ }
+
+ /*
+ foreach(Block! b in mainImpl.Blocks) {
+ //Set<Variable!> lv = cfg.weightBefore[b].getLiveVars();
+ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
+ //foreach(GlobalVariable! v in program.GlobalVariables()) {
+ // b.liveVarsBefore.Add(v);
+ //}
+ }
+ */
+ }
+
+ // Called when summaries have already been computed
+ private void processLV(WorkItem! wi) {
+ ICFG! cfg = wi.cfg;
+ Block! block = wi.block;
+
+ Set<Variable!>! lv = cfg.liveVarsAfter[block];
+
+ // Propagate backwards in the block
+ Set<Variable!>! prop = new Set<Variable!>();
+ prop.AddRange(lv);
+ for(int i = block.Cmds.Length - 1; i >= 0; i--) {
+ Cmd! cmd = block.Cmds[i];
+ if(cmd is CallCmd) {
+ string! procName = ((!)((CallCmd!)cmd).Proc).Name;
+ if(procICFG.ContainsKey(procName)) {
+ ICFG! callee = procICFG[procName];
+ // Inter propagation
+ // Remove local variables; add return variables
+ Set<Variable!>! elv = new Set<Variable!>();
+ foreach(Variable! v in prop) {
+ if(v is GlobalVariable) elv.Add(v);
+ }
+ foreach(Variable! v in callee.impl.OutParams) {
+ elv.Add(v);
+ }
+
+ foreach(Block! eb in callee.exitNodes) {
+ callee.liveVarsAfter[eb].AddRange(elv);
+ // TODO: check if modified before inserting
+ AddToWorkListReverse(new WorkItem(callee, eb));
+ }
+
+ // Continue with intra propagation
+ GenKillWeight! summary = getWeightCall((CallCmd!)cmd);
+ prop = summary.getLiveVars(prop);
+ } else {
+ LiveVariableAnalysis.Propagate(cmd, prop);
+ }
+ } else {
+ LiveVariableAnalysis.Propagate(cmd, prop);
+ }
+ }
+
+ cfg.liveVarsBefore[block].AddRange(prop);
+
+ foreach(Block! b in cfg.predEdges[block]) {
+ Set<Variable!>! prev = cfg.liveVarsAfter[b];
+ Set<Variable!>! curr = (!)prev.Union(cfg.liveVarsBefore[block]);
+ if(curr.Count != prev.Count) {
+ cfg.liveVarsAfter[b] = curr;
+ AddToWorkListReverse(new WorkItem(cfg, b));
+ }
+ }
+ }
+
+ private void process(WorkItem! wi)
+ {
+ GenKillWeight! w = wi.getWeightAfter();
+
+ for(int i = wi.block.Cmds.Length - 1; i >= 0; i--) {
+ Cmd! c = wi.block.Cmds[i];
+ if(c is CallCmd && procICFG.ContainsKey( ((!)((CallCmd!)c).Proc).Name ) ){
+ w = GenKillWeight.extend(getWeightCall((CallCmd!)c), w);
+ } else {
+ GenKillWeight! cweight = getWeight(c, wi.cfg.impl, program);
+ w = GenKillWeight.extend(cweight, w);
+ }
+ }
+
+ bool change = wi.setWeightBefore(w);
+
+ if(change && wi.cfg.srcNodes.Contains(wi.block)) {
+ GenKillWeight! prev = wi.cfg.summary;
+ GenKillWeight! curr = GenKillWeight.combine(prev, wi.cfg.weightBefore[wi.block]);
+ if(!GenKillWeight.isEqual(prev, curr)) {
+ wi.cfg.summary = curr;
+ // push callers onto the worklist
+ if(callers.ContainsKey(wi.cfg.impl.Name)) {
+ foreach(WorkItem! caller in callers[wi.cfg.impl.Name]) {
+ AddToWorkList(caller);
+ }
+ }
+ }
+ }
+
+ foreach(Block! b in wi.cfg.predEdges[wi.block]) {
+ GenKillWeight! prev = wi.cfg.weightAfter[b];
+ GenKillWeight! curr = GenKillWeight.combine(prev, w);
+ if(!GenKillWeight.isEqual(prev, curr)) {
+ wi.cfg.weightAfter[b] = curr;
+ AddToWorkList(new WorkItem(wi.cfg, b));
+ }
+ }
+
+ }
+
+ static Dictionary<Cmd!, GenKillWeight!>! weightCache = new Dictionary<Cmd!, GenKillWeight!>();
+
+ private static GenKillWeight! getWeight(Cmd! cmd) {
+ return getWeight(cmd, null, null);
+ }
+
+ private GenKillWeight! getWeightCall(CallCmd! cmd) {
+ GenKillWeight! w1 = getWeightBeforeCall(cmd);
+ GenKillWeight! w2 = getSummary(cmd);
+ GenKillWeight! w3 = getWeightAfterCall(cmd);
+ return GenKillWeight.extend(w1, GenKillWeight.extend(w2, w3));
+ }
+
+ private static GenKillWeight! getWeight(Cmd! cmd, Implementation impl, Program prog) {
+
+ if(weightCache.ContainsKey(cmd))
+ return weightCache[cmd];
+
+ Set<Variable!>! gen = new Set<Variable!>();
+ Set<Variable!>! kill = new Set<Variable!>();
+ GenKillWeight! ret;
+
+ if (cmd is AssignCmd) {
+ AssignCmd! assignCmd = (AssignCmd) cmd;
+ // I must first iterate over all the targets and remove the live ones.
+ // After the removals are done, I must add the variables referred on
+ // the right side of the removed targets
+ foreach (AssignLhs! lhs in assignCmd.Lhss) {
+ Variable var = lhs.DeepAssignedVariable;
+ if (var != null) {
+ if (lhs is SimpleAssignLhs) {
+ // we should only remove non-map target variables because there is an implicit
+ // read of a map variable in an assignment to it
+ kill.Add(var);
+ }
+ }
+ }
+ int index = 0;
+ foreach (Expr! expr in assignCmd.Rhss) {
+ VariableCollector! collector = new VariableCollector();
+ collector.Visit(expr);
+ gen.AddRange(collector.usedVars);
+ AssignLhs lhs = assignCmd.Lhss[index];
+ if (lhs is MapAssignLhs) {
+ // If the target is a map, then all indices are also read
+ MapAssignLhs malhs = (MapAssignLhs) lhs;
+ foreach (Expr e in malhs.Indexes) {
+ VariableCollector! c = new VariableCollector();
+ c.Visit(e);
+ gen.AddRange(c.usedVars);
+ }
+ }
+ index++;
+ }
+ ret = new GenKillWeight(gen, kill);
+ } else if (cmd is HavocCmd) {
+ HavocCmd! havocCmd = (HavocCmd) cmd;
+ foreach (IdentifierExpr! expr in havocCmd.Vars) {
+ if (expr.Decl != null) {
+ kill.Add(expr.Decl);
+ }
+ }
+ ret = new GenKillWeight(gen, kill);
+ } else if (cmd is PredicateCmd) {
+ assert (cmd is AssertCmd || cmd is AssumeCmd);
+ PredicateCmd! predicateCmd = (PredicateCmd) cmd;
+ if (predicateCmd.Expr is LiteralExpr && prog != null && impl != null) {
+ LiteralExpr le = (LiteralExpr) predicateCmd.Expr;
+ if (le.IsFalse) {
+ List<GlobalVariable!>! globals = prog.GlobalVariables();
+ foreach(Variable! v in globals) {
+ kill.Add(v);
+ }
+ foreach(Variable! v in impl.LocVars) {
+ kill.Add(v);
+ }
+ foreach(Variable! v in impl.OutParams) {
+ kill.Add(v);
+ }
+ }
+ } else {
+ VariableCollector! collector = new VariableCollector();
+ collector.Visit(predicateCmd.Expr);
+ gen.AddRange(collector.usedVars);
+ }
+ ret = new GenKillWeight(gen, kill);
+ } else if (cmd is CommentCmd) {
+ ret = new GenKillWeight(gen, kill);
+ // comments are just for debugging and don't affect verification
+ } else if (cmd is SugaredCmd) {
+ SugaredCmd! sugCmd = (SugaredCmd) cmd;
+ ret = getWeight(sugCmd.Desugaring, impl, prog);
+ } else if (cmd is StateCmd) {
+ StateCmd! stCmd = (StateCmd) cmd;
+ CmdSeq! cmds = stCmd.Cmds;
+ int len = cmds.Length;
+ ret = GenKillWeight.one();
+ for (int i = len - 1; i >= 0; i--) {
+ GenKillWeight! w = getWeight(cmds[i], impl, prog);
+ ret = GenKillWeight.extend(w, ret);
+ }
+ foreach (Variable! v in stCmd.Locals) {
+ kill.Add(v);
+ }
+ ret = GenKillWeight.extend(new GenKillWeight(gen, kill), ret);
+ } else {
+ assert false;
+ }
+
+ weightCache[cmd] = ret;
+ return ret;
+ }
+
+ static Dictionary<Cmd!, GenKillWeight!>! weightCacheAfterCall = new Dictionary<Cmd!, GenKillWeight!>();
+ static Dictionary<Cmd!, GenKillWeight!>! weightCacheBeforeCall = new Dictionary<Cmd!, GenKillWeight!>();
+
+ private static GenKillWeight! getWeightAfterCall(Cmd! cmd) {
+
+ if(weightCacheAfterCall.ContainsKey(cmd))
+ return weightCacheAfterCall[cmd];
+
+ Set<Variable!>! gen = new Set<Variable!>();
+ Set<Variable!>! kill = new Set<Variable!>();
+
+ assert (cmd is CallCmd);
+ CallCmd! ccmd = (CallCmd!)cmd;
+
+ foreach(IdentifierExpr! ie in ccmd.Outs) {
+ if(ie.Decl != null) kill.Add(ie.Decl);
+ }
+
+ // Variables in ensures are considered as "read"
+ foreach(Ensures! re in ((!)ccmd.Proc).Ensures) {
+ VariableCollector! collector = new VariableCollector();
+ collector.Visit(re.Condition);
+ foreach(Variable! v in collector.usedVars) {
+ if(v is GlobalVariable) {
+ gen.Add(v);
+ }
+ }
+ }
+
+ GenKillWeight! ret = new GenKillWeight(gen, kill);
+ weightCacheAfterCall[cmd] = ret;
+ return ret;
+ }
+
+ private static GenKillWeight! getWeightBeforeCall(Cmd! cmd) {
+ assert (cmd is CallCmd);
+ if(weightCacheBeforeCall.ContainsKey(cmd))
+ return weightCacheBeforeCall[cmd];
+
+ Set<Variable!>! gen = new Set<Variable!>();
+ Set<Variable!>! kill = new Set<Variable!>();
+ CallCmd! ccmd = (CallCmd!)cmd;
+
+ foreach (Expr! expr in ccmd.Ins) {
+ VariableCollector! collector = new VariableCollector();
+ collector.Visit(expr);
+ gen.AddRange(collector.usedVars);
+ }
+
+ assert ccmd.Proc != null;
+
+ // Variables in requires are considered as "read"
+ foreach(Requires! re in ccmd.Proc.Requires) {
+ VariableCollector! collector = new VariableCollector();
+ collector.Visit(re.Condition);
+ foreach(Variable! v in collector.usedVars) {
+ if(v is GlobalVariable) {
+ gen.Add(v);
+ }
+ }
+ }
+
+ // Old variables in ensures are considered as "read"
+ foreach(Ensures! re in ccmd.Proc.Ensures) {
+ VariableCollector! collector = new VariableCollector();
+ collector.Visit(re.Condition);
+ foreach(Variable! v in collector.oldVarsUsed) {
+ if(v is GlobalVariable) {
+ gen.Add(v);
+ }
+ }
+ }
+
+ GenKillWeight! ret = new GenKillWeight(gen, kill);
+ weightCacheAfterCall[cmd] = ret;
+ return ret;
+ }
+
+
+ }
+
}
\ No newline at end of file diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc index b80fc88f..0f42939d 100644 --- a/Source/VCGeneration/VC.ssc +++ b/Source/VCGeneration/VC.ssc @@ -42,7 +42,9 @@ namespace VC }
if (CommandLineOptions.Clo.StratifiedInlining > 0)
{
+
this.GenerateVCsForStratifiedInlining(program);
+
}
// base();
}
@@ -263,7 +265,7 @@ namespace VC public void GenerateVCsForStratifiedInlining(Program! program)
{
- Checker! checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime);
+ //Checker! checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime);
foreach (Declaration! decl in program.TopLevelDeclarations)
{
Implementation impl = decl as Implementation;
@@ -296,11 +298,7 @@ namespace VC proc.Ensures.Add(new Ensures(true, freePostExpr));
}
}
-
- foreach (StratifiedInliningInfo! info in implName2StratifiedInliningInfo.Values)
- {
- GenerateVCForStratifiedInlining(program, info, checker);
- }
+
}
private void GenerateVCForStratifiedInlining(Program! program, StratifiedInliningInfo! info, Checker! checker)
@@ -1660,8 +1658,24 @@ namespace VC public override Outcome StratifiedVerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback)
throws UnexpectedProverOutputException;
{
+ // This flag control the nature of queries made by StratifiedVerifyImplementation
+ // true: incremental search; false: in-place inlining
+ bool incrementalSearch = true;
+
// Get the checker
Checker! checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime);
+
+ // Run live variable analysis
+ if(CommandLineOptions.Clo.LiveVariableAnalysis == 2) {
+ Microsoft.Boogie.InterProcGenKill.ComputeLiveVars(impl, program);
+ }
+
+ // Build VCs for all procedures
+ assert implName2StratifiedInliningInfo != null;
+ foreach(StratifiedInliningInfo! info in implName2StratifiedInliningInfo.Values)
+ {
+ GenerateVCForStratifiedInlining(program, info, checker);
+ }
// Get the VC of the current procedure
VCExpr! vc;
@@ -1688,8 +1702,14 @@ namespace VC toExpand.Add(id);
}
expansionCount += toExpand.Count;
- total_axioms_pushed +=
- DoExpansion(toExpand, calls, checker);
+ if(incrementalSearch)
+ {
+ total_axioms_pushed +=
+ DoExpansion(toExpand, calls, checker);
+ } else
+ {
+ vc = DoExpansionAndInline(vc, toExpand, calls, checker);
+ }
}
int cnt = 0;
@@ -1756,8 +1776,15 @@ namespace VC assert reporter.candidatesToExpand.Count != 0;
expansionCount += reporter.candidatesToExpand.Count;
- total_axioms_pushed +=
- DoExpansion(reporter.candidatesToExpand, calls, checker);
+
+ if(incrementalSearch)
+ {
+ total_axioms_pushed +=
+ DoExpansion(reporter.candidatesToExpand, calls, checker);
+ } else
+ {
+ vc = DoExpansionAndInline(vc, reporter.candidatesToExpand, calls, checker);
+ }
checker.TheoremProver.LogComment(";;;;;;;;;;;; Expansion end ;;;;;;;;;;");
}
@@ -1848,7 +1875,67 @@ namespace VC checker.TheoremProver.FlushAxiomsToTheoremProver();
return axioms_pushed;
}
-
+
+ // Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.
+ // Returns the number of axioms pushed.
+ private VCExpr! DoExpansionAndInline(
+ VCExpr! mainVC, List<int>! candidates,
+ FCallHandler! calls, Checker! checker)
+ throws UnexpectedProverOutputException;
+ {
+ FCallInliner! inliner = new FCallInliner(checker.VCExprGen);
+ foreach(int id in candidates) {
+ VCExprNAry! expr = calls.id2Candidate[id];
+
+ string procName = ((!)(expr.Op as VCExprBoogieFunctionOp)).Func.Name;
+ if(!implName2StratifiedInliningInfo.ContainsKey(procName)) continue;
+
+ StratifiedInliningInfo info = implName2StratifiedInliningInfo[procName];
+ VCExpr! expansion = (!)info.vcexpr;
+
+ // Instantiate the "forall" variables
+ Dictionary<VCExprVar!, VCExpr!>! substForallDict = new Dictionary<VCExprVar!, VCExpr!>();
+ assert info.interfaceExprVars.Count == expr.Length;
+ for(int i = 0; i < info.interfaceExprVars.Count; i++) {
+ substForallDict.Add(info.interfaceExprVars[i], expr[i]);
+ }
+ VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary<TypeVariable!, Microsoft.Boogie.Type!>());
+
+ SubstitutingVCExprVisitor! subst = new SubstitutingVCExprVisitor(checker.VCExprGen);
+ expansion = subst.Mutate(expansion, substForall);
+
+ // Instantiate and declare the "exists" variables
+ Dictionary<VCExprVar!, VCExpr!>! substExistsDict = new Dictionary<VCExprVar!, VCExpr!>();
+ for(int i = 0; i < info.privateVars.Count; i++) {
+ VCExprVar! v = info.privateVars[i];
+ string newName = v.Name + "_si_" + 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<TypeVariable!, Microsoft.Boogie.Type!>());
+
+ subst = new SubstitutingVCExprVisitor(checker.VCExprGen);
+ expansion = subst.Mutate(expansion, substExists);
+
+ if(!calls.currCandidates.Contains(id)) {
+ Console.WriteLine("Don't know what we just expanded");
+ }
+
+ calls.currCandidates.Remove(id);
+
+ // Record the new set of candidates and rename absy labels
+ calls.currInlineCount = id;
+ calls.setCurrProc(procName);
+ expansion = calls.Mutate(expansion, true);
+
+ inliner.subst.Add(id, expansion);
+
+ }
+
+ return inliner.Mutate(mainVC, true);
+ }
+
// Return the VC for the impl (don't pass it to the theorem prover).
// GetVC is a cheap imitation of VerifyImplementatio, except that the VC is not passed to the theorem prover.
private void GetVC(Implementation! impl, Program! program, VerifierCallback! callback, out VCExpr! vc, out Hashtable/*<int, Absy!>*/! label2absy, out StratifiedInliningErrorReporter! reporter)
@@ -2101,7 +2188,51 @@ namespace VC }
} // end FCallHandler
-
+
+
+ public class FCallInliner : MutatingVCExprVisitor<bool> {
+ public Dictionary<int, VCExpr!>! subst;
+
+ public FCallInliner(VCExpressionGenerator! gen)
+ : base(gen)
+ {
+ subst = new Dictionary<int, VCExpr!>();
+ }
+
+ public void Clear()
+ {
+ subst = new Dictionary<int, VCExpr!>();
+ }
+
+ protected override VCExpr! UpdateModifiedNode(VCExprNAry! originalNode,
+ List<VCExpr!>! newSubExprs,
+ // has any of the subexpressions changed?
+ bool changed,
+ bool arg)
+ {
+ VCExpr! ret;
+ if (changed)
+ ret = Gen.Function(originalNode.Op,
+ newSubExprs, originalNode.TypeArguments);
+ else
+ ret = originalNode;
+
+ VCExprLabelOp lop = originalNode.Op as VCExprLabelOp;
+ if(lop == null) return ret;
+ if(!(ret is VCExprNAry!)) return ret;
+
+ string! prefix = "si_fcall_"; // from FCallHandler::GetLabel
+ if(lop.label.Substring(1).StartsWith(prefix)) {
+ int id = Int32.Parse(lop.label.Substring(prefix.Length + 1));
+ if(subst.ContainsKey(id)) {
+ return subst[id];
+ }
+ }
+ return ret;
+ }
+
+ } // end FCallInliner
+
public class ErrorReporter : ProverInterface.ErrorHandler {
Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins;
Hashtable/*<int, Absy!>*/! label2absy;
@@ -2346,8 +2477,9 @@ namespace VC int candidateId, Implementation! procImpl) {
Hashtable traceNodes = new Hashtable();
- foreach (string! s in labels) {
- string! procPrefix = "si_inline_" + candidateId.ToString() + "_";
+ string! procPrefix = "si_inline_" + candidateId.ToString() + "_";
+
+ foreach (string! s in labels) {
if(!s.StartsWith(procPrefix))
continue;
@@ -2711,14 +2843,14 @@ namespace VC }
#endregion
- #region Support for stratified lazy inlining
+ #region Support for lazy inlining
if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(impl.Name))
{
Expr! assertExpr = implName2StratifiedInliningInfo[impl.Name].assertExpr;
exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));
}
#endregion
-
+
#region Debug Tracing
if (CommandLineOptions.Clo.TraceVerify)
{
@@ -2737,7 +2869,7 @@ namespace VC }
#endregion
- if (CommandLineOptions.Clo.LiveVariableAnalysis) {
+ if (CommandLineOptions.Clo.LiveVariableAnalysis > 0) {
Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);
}
@@ -2755,9 +2887,13 @@ namespace VC info.incarnationOriginMap = this.incarnationOriginMap;
}
- if (CommandLineOptions.Clo.LiveVariableAnalysis) {
+ if (CommandLineOptions.Clo.LiveVariableAnalysis == 1) {
Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);
- }
+ }
+ // TODO: fix
+ //else if (CommandLineOptions.Clo.LiveVariableAnalysis == 2) {
+ // Microsoft.Boogie.InterProcGenKill.ClearLiveVariables(impl, program);
+ //}
#region Peep-hole optimizations
if (CommandLineOptions.Clo.RemoveEmptyBlocks){
|