diff options
| author |  qadeer <unknown> | 2014-12-16 22:40:16 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2014-12-16 22:40:16 -0800 |
| commit | fa6b47445e52ef471560deb44e62965982daa63a (patch) | |
| tree | 9a63292f3d9dd75eebe9c620c485bba14d97cdc2 | |
| parent | 9dda7cc805664f4d68b79877663182adc829d315 (diff) | |
patched two occurrences of StackOverflowException on benchmarks from IronClad
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 43 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprASTVisitors.cs | 35 |
2 files changed, 65 insertions, 13 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 7c6a3a9a..5cd40896 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -211,24 +211,53 @@ namespace Microsoft.Boogie.SMTLib public bool Visit(VCExprNAry node, LineariserOptions options)
{
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
VCExprOp op = node.Op;
Contract.Assert(op != null);
+
+ if (op.Equals(VCExpressionGenerator.ImpliesOp))
+ {
+ // handle this operator without recursion
+ VCExprNAry iter = node;
+ List<VCExpr> conjuncts = new List<VCExpr>();
+ VCExpr next = null;
+ do
+ {
+ conjuncts.Add(iter[0]);
+ next = iter[1];
+ iter = next as VCExprNAry;
+ if (iter == null) break;
+ }
+ while (iter.Op.Equals(VCExpressionGenerator.ImpliesOp));
+
+ wr.Write("(=> ");
+ if (conjuncts.Count == 1)
+ {
+ Linearise(conjuncts[0], options);
+ }
+ else {
+ wr.Write("(and");
+ foreach (var e in conjuncts)
+ {
+ wr.Write(" ");
+ Linearise(e, options);
+ }
+ wr.Write(")");
+ }
+ wr.Write(" ");
+ Linearise(next, options);
+ wr.Write(")");
+ return true;
+ }
if (op.Equals(VCExpressionGenerator.AndOp) ||
op.Equals(VCExpressionGenerator.OrOp)) {
// handle these operators without recursion
-
- wr.Write("({0}",
- op.Equals(VCExpressionGenerator.AndOp) ? "and" : "or");
+ wr.Write("({0}", op.Equals(VCExpressionGenerator.AndOp) ? "and" : "or");
foreach (var ch in node.UniformArguments) {
wr.Write("\n");
Linearise(ch, options);
}
wr.Write(")");
-
return true;
}
diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index 02220057..c9d4f1c3 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -288,14 +288,15 @@ namespace Microsoft.Boogie.VCExprAST { node.Op == VCExpressionGenerator.ImpliesOp)) {
Contract.Assert(node.Op != null);
VCExprOp op = node.Op;
-
- IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);
- enumerator.MoveNext(); // skip the node itself
-
+ HashSet<VCExprOp> ops = new HashSet<VCExprOp>();
+ ops.Add(VCExpressionGenerator.AndOp);
+ ops.Add(VCExpressionGenerator.OrOp);
+ ops.Add(VCExpressionGenerator.ImpliesOp);
+ IEnumerator enumerator = new VCExprNAryMultiUniformOpEnumerator(node, ops);
while (enumerator.MoveNext()) {
- VCExpr/*!*/ expr = cce.NonNull((VCExpr/*!*/)enumerator.Current);
+ VCExpr expr = cce.NonNull((VCExpr)enumerator.Current);
VCExprNAry naryExpr = expr as VCExprNAry;
- if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+ if (naryExpr == null || !ops.Contains(naryExpr.Op)) {
expr.Accept(this, arg);
} else {
StandardResult(expr, arg);
@@ -433,6 +434,28 @@ namespace Microsoft.Boogie.VCExprAST { }
}
+ public class VCExprNAryMultiUniformOpEnumerator : VCExprNAryEnumerator
+ {
+ private readonly HashSet<VCExprOp> Ops;
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(Ops != null);
+ }
+
+ public VCExprNAryMultiUniformOpEnumerator(VCExprNAry completeExpr, HashSet<VCExprOp> ops)
+ : base(completeExpr)
+ {
+ Contract.Requires(completeExpr != null);
+
+ this.Ops = ops;
+ }
+ protected override bool Descend(VCExprNAry expr)
+ {
+ return Ops.Contains(expr.Op) && expr.TypeParamArity == 0;
+ }
+ }
+
//////////////////////////////////////////////////////////////////////////////
// Visitor that knows about the variables bound at each location in a VCExpr
|