summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Ally Donaldson <unknown>2015-01-16 16:48:31 +0000
committerGravatar Ally Donaldson <unknown>2015-01-16 16:48:31 +0000
commit007a11fe5e8deda771ea4215557ad7143c8d608c (patch)
treee2a85162383b14ba5159f8162b593b2bbda8e44a
parentfe461a22df4cade95f1ff30f8e19ef8a54ce8b41 (diff)
Worked on StagedHoudini
-rw-r--r--Source/Houdini/AnnotationDependenceAnalyser.cs167
1 files changed, 106 insertions, 61 deletions
diff --git a/Source/Houdini/AnnotationDependenceAnalyser.cs b/Source/Houdini/AnnotationDependenceAnalyser.cs
index 7cb43fbd..1d12b6b1 100644
--- a/Source/Houdini/AnnotationDependenceAnalyser.cs
+++ b/Source/Houdini/AnnotationDependenceAnalyser.cs
@@ -206,7 +206,10 @@ namespace Microsoft.Boogie.Houdini {
if(Houdini.MatchCandidate(p.Expr, CandidateIdentifiers, out c)) {
yield return new AnnotationInstance(c, impl.Name, p.Expr);
} else if((p is AssertCmd) && QKeyValue.FindBoolAttribute(p.Attributes, "originated_from_invariant")) {
- yield return new AnnotationInstance(GetTagFromNonCandidateAttributes(p.Attributes), impl.Name, p.Expr);
+ var tag = GetTagFromNonCandidateAttributes(p.Attributes);
+ if (tag != null) {
+ yield return new AnnotationInstance(tag, impl.Name, p.Expr);
+ }
}
}
}
@@ -219,7 +222,10 @@ namespace Microsoft.Boogie.Houdini {
if(Houdini.MatchCandidate(r.Condition, CandidateIdentifiers, out c)) {
yield return new AnnotationInstance(c, proc.Name, r.Condition);
} else {
- //yield return new AnnotationInstance(GetTagFromNonCandidateAttributes(r.Attributes), proc.Name, r.Condition);
+ var tag = GetTagFromNonCandidateAttributes(r.Attributes);
+ if (tag != null) {
+ yield return new AnnotationInstance(tag, proc.Name, r.Condition);
+ }
}
}
foreach (Ensures e in proc.Ensures)
@@ -228,7 +234,10 @@ namespace Microsoft.Boogie.Houdini {
if(Houdini.MatchCandidate(e.Condition, CandidateIdentifiers, out c)) {
yield return new AnnotationInstance(c, proc.Name, e.Condition);
} else {
- //yield return new AnnotationInstance(GetTagFromNonCandidateAttributes(e.Attributes), proc.Name, e.Condition);
+ var tag = GetTagFromNonCandidateAttributes(e.Attributes);
+ if (tag != null) {
+ yield return new AnnotationInstance(tag, proc.Name, e.Condition);
+ }
}
}
}
@@ -237,7 +246,6 @@ namespace Microsoft.Boogie.Houdini {
internal static string GetTagFromNonCandidateAttributes(QKeyValue Attributes)
{
string tag = QKeyValue.FindStringAttribute(Attributes, "staged_houdini_tag");
- Debug.Assert(tag != null);
return tag;
}
@@ -369,6 +377,12 @@ namespace Microsoft.Boogie.Houdini {
Console.Write(" }");
}
+ private bool OnlyRefersToConstants(Expr e) {
+ VariableCollector vc = new VariableCollector();
+ vc.Visit(e);
+ return vc.usedVars.OfType<Constant>().Count() == vc.usedVars.Count();
+ }
+
private IEnumerable<string> GetNonCandidateAnnotations() {
var Result = new HashSet<string>();
int Counter = 0;
@@ -384,14 +398,17 @@ namespace Microsoft.Boogie.Houdini {
continue;
}
+ if (OnlyRefersToConstants(Assertion.Expr)) {
+ continue;
+ }
+
string Tag = "staged_houdini_tag_" + Counter;
Result.Add(Tag);
Assertion.Attributes = new QKeyValue(Token.NoToken, "staged_houdini_tag",
new List<object> { Tag }, Assertion.Attributes);
Counter++;
}
-
- /*
+
foreach(var Req in prog.NonInlinedProcedures().SelectMany(Item => Item.Requires)) {
string unused;
@@ -399,6 +416,10 @@ namespace Microsoft.Boogie.Houdini {
continue;
}
+ if (OnlyRefersToConstants(Req.Condition)) {
+ continue;
+ }
+
string Tag = "staged_houdini_tag_" + Counter;
Result.Add(Tag);
Req.Attributes = new QKeyValue(Token.NoToken, "staged_houdini_tag",
@@ -414,6 +435,10 @@ namespace Microsoft.Boogie.Houdini {
continue;
}
+ if (OnlyRefersToConstants(Ens.Condition)) {
+ continue;
+ }
+
string Tag = "staged_houdini_tag_" + Counter;
Result.Add(Tag);
Ens.Attributes = new QKeyValue(Token.NoToken, "staged_houdini_tag",
@@ -421,7 +446,6 @@ namespace Microsoft.Boogie.Houdini {
Counter++;
}
- */
return Result;
}
@@ -503,12 +527,16 @@ namespace Microsoft.Boogie.Houdini {
Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(c).GetId()]), c), a.Attributes));
} else if (QKeyValue.FindBoolAttribute(a.Attributes, "originated_from_invariant")) {
string tag = GetTagFromNonCandidateAttributes(a.Attributes);
- newCmds.Add(new AssertCmd(a.tok, Expr.Imp(
- Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(tag).GetId()]), a.Expr),
- a.Attributes));
- newCmds.Add(new AssumeCmd(a.tok, Expr.Imp(
- Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(tag).GetId()]), a.Expr),
- a.Attributes));
+ if (tag == null) {
+ newCmds.Add(a);
+ } else {
+ newCmds.Add(new AssertCmd(a.tok, Expr.Imp(
+ Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(tag).GetId()]), a.Expr),
+ a.Attributes));
+ newCmds.Add(new AssumeCmd(a.tok, Expr.Imp(
+ Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(tag).GetId()]), a.Expr),
+ a.Attributes));
+ }
}
}
else
@@ -525,58 +553,68 @@ namespace Microsoft.Boogie.Houdini {
{
#region Handle the preconditions
- List<Requires> newRequires = new List<Requires>();
- foreach(Requires r in p.Requires) {
- string c;
- if (Houdini.MatchCandidate(r.Condition, CandidateIdentifiers, out c)) {
- newRequires.Add(new Requires(r.tok, false,
- Houdini.AddConditionToCandidate(r.Condition,
- Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(c).GetId()]), c),
- r.Comment, r.Attributes));
- newRequires.Add(new Requires(r.tok, true,
- Houdini.AddConditionToCandidate(r.Condition,
- Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(c).GetId()]), c),
- r.Comment, r.Attributes));
- } else {
- newRequires.Add(r);
- /*string tag = GetTagFromNonCandidateAttributes(r.Attributes);
- newRequires.Add(new Requires(r.tok, false,
- Expr.Imp(Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(tag).GetId()]), r.Condition),
- r.Comment, r.Attributes));
- newRequires.Add(new Requires(r.tok, true,
- Expr.Imp(Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(tag).GetId()]), r.Condition),
- r.Comment, r.Attributes));*/
+ {
+ List<Requires> newRequires = new List<Requires>();
+ foreach(Requires r in p.Requires) {
+ string c;
+ if (Houdini.MatchCandidate(r.Condition, CandidateIdentifiers, out c)) {
+ newRequires.Add(new Requires(r.tok, false,
+ Houdini.AddConditionToCandidate(r.Condition,
+ Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(c).GetId()]), c),
+ r.Comment, r.Attributes));
+ newRequires.Add(new Requires(r.tok, true,
+ Houdini.AddConditionToCandidate(r.Condition,
+ Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(c).GetId()]), c),
+ r.Comment, r.Attributes));
+ } else {
+ string tag = GetTagFromNonCandidateAttributes(r.Attributes);
+ if (tag == null) {
+ newRequires.Add(r);
+ } else {
+ newRequires.Add(new Requires(r.tok, false,
+ Expr.Imp(Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(tag).GetId()]), r.Condition),
+ r.Comment, r.Attributes));
+ newRequires.Add(new Requires(r.tok, true,
+ Expr.Imp(Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(tag).GetId()]), r.Condition),
+ r.Comment, r.Attributes));
+ }
+ }
}
+ p.Requires = newRequires;
}
- p.Requires = newRequires;
#endregion
#region Handle the postconditions
- List<Ensures> newEnsures = new List<Ensures>();
- foreach(Ensures e in p.Ensures) {
- string c;
- if (Houdini.MatchCandidate(e.Condition, CandidateIdentifiers, out c)) {
- int stage = Plan.StageForAnnotation(c).GetId();
- newEnsures.Add(new Ensures(e.tok, false,
- Houdini.AddConditionToCandidate(e.Condition,
- Expr.Ident(stageToActiveBoolean[stage]), c),
- e.Comment, e.Attributes));
- newEnsures.Add(new Ensures(e.tok, true,
- Houdini.AddConditionToCandidate(e.Condition,
- Expr.Ident(stageToCompleteBoolean[stage]), c),
- e.Comment, e.Attributes));
- } else {
- newEnsures.Add(e);
- /*string tag = GetTagFromNonCandidateAttributes(e.Attributes);
- newRequires.Add(new Requires(e.tok, false,
- Expr.Imp(Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(tag).GetId()]), e.Condition),
- e.Comment, e.Attributes));
- newRequires.Add(new Requires(e.tok, true,
- Expr.Imp(Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(tag).GetId()]), e.Condition),
- e.Comment, e.Attributes));*/
+ {
+ List<Ensures> newEnsures = new List<Ensures>();
+ foreach(Ensures e in p.Ensures) {
+ string c;
+ if (Houdini.MatchCandidate(e.Condition, CandidateIdentifiers, out c)) {
+ int stage = Plan.StageForAnnotation(c).GetId();
+ newEnsures.Add(new Ensures(e.tok, false,
+ Houdini.AddConditionToCandidate(e.Condition,
+ Expr.Ident(stageToActiveBoolean[stage]), c),
+ e.Comment, e.Attributes));
+ newEnsures.Add(new Ensures(e.tok, true,
+ Houdini.AddConditionToCandidate(e.Condition,
+ Expr.Ident(stageToCompleteBoolean[stage]), c),
+ e.Comment, e.Attributes));
+ } else {
+ string tag = GetTagFromNonCandidateAttributes(e.Attributes);
+ if (tag == null) {
+ newEnsures.Add(e);
+ } else {
+ newEnsures.Add(new Ensures(e.tok, false,
+ Expr.Imp(Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(tag).GetId()]), e.Condition),
+ e.Comment, e.Attributes));
+ newEnsures.Add(new Ensures(e.tok, true,
+ Expr.Imp(Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(tag).GetId()]), e.Condition),
+ e.Comment, e.Attributes));
+ }
+ }
}
+ p.Ensures = newEnsures;
}
- p.Ensures = newEnsures;
#endregion
}
@@ -740,7 +778,10 @@ namespace Microsoft.Boogie.Houdini {
if(Houdini.MatchCandidate(assertCmd.Expr, AnnotationIdentifiers, out c)) {
AddAnnotationOccurrence(c, b);
} else {
- AddAnnotationOccurrence(AnnotationDependenceAnalyser.GetTagFromNonCandidateAttributes(assertCmd.Attributes), b);
+ var tag = AnnotationDependenceAnalyser.GetTagFromNonCandidateAttributes(assertCmd.Attributes);
+ if (tag != null) {
+ AddAnnotationOccurrence(tag, b);
+ }
}
}
}
@@ -753,7 +794,9 @@ namespace Microsoft.Boogie.Houdini {
AddAnnotationOccurrence(c, new Tuple<string, PrePost>(proc.Name, PrePost.PRE));
} else {
string tag = AnnotationDependenceAnalyser.GetTagFromNonCandidateAttributes(r.Attributes);
- AddAnnotationOccurrence(tag, new Tuple<string, PrePost>(proc.Name, PrePost.PRE));
+ if(tag != null) {
+ AddAnnotationOccurrence(tag, new Tuple<string, PrePost>(proc.Name, PrePost.PRE));
+ }
}
}
foreach(Ensures e in proc.Ensures) {
@@ -762,7 +805,9 @@ namespace Microsoft.Boogie.Houdini {
AddAnnotationOccurrence(c, new Tuple<string, PrePost>(proc.Name, PrePost.POST));
} else {
string tag = AnnotationDependenceAnalyser.GetTagFromNonCandidateAttributes(e.Attributes);
- AddAnnotationOccurrence(tag, new Tuple<string, PrePost>(proc.Name, PrePost.PRE));
+ if(tag != null) {
+ AddAnnotationOccurrence(tag, new Tuple<string, PrePost>(proc.Name, PrePost.PRE));
+ }
}
}
}