diff options
| -rw-r--r-- | Source/Predication/SmartBlockPredicator.cs | 37 | ||||
| -rw-r--r-- | Source/Predication/UniformityAnalyser.cs | 80 |
2 files changed, 85 insertions, 32 deletions
diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs index 9478595b..55e73161 100644 --- a/Source/Predication/SmartBlockPredicator.cs +++ b/Source/Predication/SmartBlockPredicator.cs @@ -94,7 +94,9 @@ public class SmartBlockPredicator { cmdSeq.Add(aCmd);
} else if (cmd is AssumeCmd) {
var aCmd = (AssumeCmd)cmd;
- cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
+ Expr newExpr = new EnabledReplacementVisitor(p).VisitExpr(aCmd.Expr);
+ aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(p, newExpr);
+ cmdSeq.Add(aCmd);
} else if (cmd is HavocCmd) {
var hCmd = (HavocCmd)cmd;
foreach (IdentifierExpr v in hCmd.Vars) {
@@ -216,12 +218,22 @@ public class SmartBlockPredicator { while (i.MoveNext()) {
var block = i.Current;
- if (uni != null && uni.IsUniform(impl.Name, block.Item1))
- continue;
+
if (block.Item2) {
- if (block.Item1 == header)
+ if (block.Item1 == header) {
return;
- } else {
+ }
+ }
+
+ if (uni != null && uni.IsUniform(impl.Name, block.Item1)) {
+ if (blockGraph.Headers.Contains(block.Item1)) {
+ parentMap[block.Item1] = header;
+ AssignPredicates(blockGraph, dom, pdom, i, headPredicate, ref predCount);
+ }
+ continue;
+ }
+
+ if (!block.Item2) {
if (blockGraph.Headers.Contains(block.Item1)) {
parentMap[block.Item1] = header;
var loopPred = FreshPredicate(ref predCount);
@@ -494,15 +506,18 @@ public class SmartBlockPredicator { .ToArray());
if (impl == null) {
- var newRequires = new RequiresSeq();
+ var fpIdentifierExpr = new IdentifierExpr(Token.NoToken, fpVar);
foreach (Requires r in proc.Requires) {
- newRequires.Add(new Requires(r.Free,
- new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition)));
+ new EnabledReplacementVisitor(fpIdentifierExpr).VisitExpr(r.Condition);
+ if (!QKeyValue.FindBoolAttribute(r.Attributes, "do_not_predicate")) {
+ r.Condition = Expr.Imp(fpIdentifierExpr, r.Condition);
+ }
}
- var newEnsures = new EnsuresSeq();
foreach (Ensures e in proc.Ensures) {
- newEnsures.Add(new Ensures(e.Free,
- new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition)));
+ new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition);
+ if (!QKeyValue.FindBoolAttribute(e.Attributes, "do_not_predicate")) {
+ e.Condition = Expr.Imp(fpIdentifierExpr, e.Condition);
+ }
}
}
}
diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs index 3408d88b..6365d974 100644 --- a/Source/Predication/UniformityAnalyser.cs +++ b/Source/Predication/UniformityAnalyser.cs @@ -149,6 +149,44 @@ namespace Microsoft.Boogie ProcedureChanged = true;
}
+ var procs = prog.TopLevelDeclarations.OfType<Procedure>();
+
+ foreach (var Proc in procs) {
+
+ if (uniformityInfo.ContainsKey(Proc.Name)) {
+ continue;
+ }
+
+ bool uniformProcedure = doAnalysis;
+
+ uniformityInfo.Add(Proc.Name, new KeyValuePair<bool, Dictionary<string, bool>>
+ (uniformProcedure, new Dictionary<string, bool>()));
+
+ inParameters[Proc.Name] = new List<string>();
+
+ foreach (Variable v in Proc.InParams) {
+ inParameters[Proc.Name].Add(v.Name);
+ if (doAnalysis) {
+ SetUniform(Proc.Name, v.Name);
+ }
+ else {
+ SetNonUniform(Proc.Name, v.Name);
+ }
+ }
+
+ outParameters[Proc.Name] = new List<string>();
+ foreach (Variable v in Proc.OutParams) {
+ outParameters[Proc.Name].Add(v.Name);
+ // We do not have a body for the procedure,
+ // so we must assume it produces non-uniform
+ // results
+ SetNonUniform(Proc.Name, v.Name);
+ }
+
+ ProcedureChanged = true;
+ }
+
+
if (doAnalysis)
{
while (ProcedureChanged)
@@ -163,17 +201,17 @@ namespace Microsoft.Boogie }
}
- foreach (var Impl in impls)
+ foreach (var Proc in procs)
{
- if (!IsUniform (Impl.Name))
+ if (!IsUniform (Proc.Name))
{
List<string> newIns = new List<String>();
newIns.Add("_P");
- foreach (string s in inParameters[Impl.Name])
+ foreach (string s in inParameters[Proc.Name])
{
newIns.Add(s);
}
- inParameters[Impl.Name] = newIns;
+ inParameters[Proc.Name] = newIns;
}
}
}
@@ -265,15 +303,16 @@ namespace Microsoft.Boogie }
}
- private Implementation GetImplementation(string procedureName)
+ private Procedure GetProcedure(string procedureName)
{
foreach (Declaration D in prog.TopLevelDeclarations)
{
- if (D is Implementation && ((D as Implementation).Name == procedureName))
+ if (D is Procedure && ((D as Procedure).Name == procedureName))
{
- return D as Implementation;
+ return D as Procedure;
}
}
+ Debug.Assert(false);
return null;
}
@@ -357,10 +396,8 @@ namespace Microsoft.Boogie else if (c is CallCmd)
{
CallCmd callCmd = c as CallCmd;
- Implementation CalleeImplementation = GetImplementation(callCmd.callee);
-
- if (CalleeImplementation != null)
- {
+ DeclWithFormals Callee = GetProcedure(callCmd.callee);
+ Debug.Assert(Callee != null);
if (!ControlFlowIsUniform)
{
@@ -369,26 +406,25 @@ namespace Microsoft.Boogie SetNonUniform(callCmd.callee);
}
}
- for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
+ for (int i = 0; i < Callee.InParams.Length; i++)
{
- if (IsUniform(callCmd.callee, CalleeImplementation.InParams[i].Name)
+ if (IsUniform(callCmd.callee, Callee.InParams[i].Name)
&& !IsUniform(impl.Name, callCmd.Ins[i]))
{
- SetNonUniform(callCmd.callee, CalleeImplementation.InParams[i].Name);
+ SetNonUniform(callCmd.callee, Callee.InParams[i].Name);
}
}
- for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
+ for (int i = 0; i < Callee.OutParams.Length; i++)
{
if (IsUniform(impl.Name, callCmd.Outs[i].Name)
- && !IsUniform(callCmd.callee, CalleeImplementation.OutParams[i].Name))
+ && !IsUniform(callCmd.callee, Callee.OutParams[i].Name))
{
SetNonUniform(impl.Name, callCmd.Outs[i].Name);
}
}
}
- }
else if (c is AssumeCmd)
{
var ac = (AssumeCmd)c;
@@ -526,20 +562,22 @@ namespace Microsoft.Boogie Console.Write((i == 0 ? "" : ", ") + outParameters[p][i]);
}
Console.WriteLine("]");
+ if (nonUniformLoops.ContainsKey(p)) {
Console.Write("Non-uniform loops:");
- foreach (int l in nonUniformLoops[p])
- {
+ foreach (int l in nonUniformLoops[p]) {
Console.Write(" " + l);
}
Console.WriteLine();
+ }
+ if (nonUniformBlocks.ContainsKey(p)) {
Console.Write("Non-uniform blocks:");
- foreach (Block b in nonUniformBlocks[p])
- {
+ foreach (Block b in nonUniformBlocks[p]) {
Console.Write(" " + b.Label);
}
Console.WriteLine();
}
}
+ }
public string GetInParameter(string procName, int i)
|