diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 1 | ||||
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 158 | ||||
| -rw-r--r-- | Test/AbsHoudini/pred1.bpl | 23 | ||||
| -rw-r--r-- | Test/AbsHoudini/pred2.bpl | 12 | ||||
| -rw-r--r-- | Test/AbsHoudini/pred3.bpl | 24 |
5 files changed, 218 insertions, 0 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index f3194256..afc1a098 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -652,6 +652,7 @@ namespace Microsoft.Boogie { System.Tuple.Create("HoudiniConst", Houdini.HoudiniConst.GetBottom() as Houdini.IAbstractDomain),
System.Tuple.Create("Intervals", new Houdini.Intervals() as Houdini.IAbstractDomain),
System.Tuple.Create("ConstantProp", Houdini.ConstantProp.GetBottom() as Houdini.IAbstractDomain),
+ System.Tuple.Create("PredicateAbs", new Houdini.PredicateAbsElem() as Houdini.IAbstractDomain),
System.Tuple.Create("IA[HoudiniConst]", new Houdini.IndependentAttribute<Houdini.HoudiniConst>() as Houdini.IAbstractDomain),
System.Tuple.Create("IA[ConstantProp]", new Houdini.IndependentAttribute<Houdini.ConstantProp>() as Houdini.IAbstractDomain),
System.Tuple.Create("IA[Intervals]", new Houdini.IndependentAttribute<Houdini.Intervals>() as Houdini.IAbstractDomain)
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index d1e9ba96..a0797308 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -347,6 +347,11 @@ namespace Microsoft.Boogie.Houdini { vcgen.ConvertCFG2DAG(impl);
var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo);
+ //CommandLineOptions.Clo.PrintInstrumented = true;
+ //var tt = new TokenTextWriter(Console.Out);
+ //impl.Emit(tt, 0);
+ //tt.Close();
+
// Intercept the FunctionCalls of the existential functions, and replace them with Boolean constants
var existentialFunctionNames = new HashSet<string>(existentialFunctions.Keys);
var fv = new ReplaceFunctionCalls(existentialFunctionNames);
@@ -672,6 +677,159 @@ namespace Microsoft.Boogie.Houdini { }
+ public class PredicateAbsElem : IAbstractDomain
+ {
+ public static class ExprExt
+ {
+ public static Expr AndSimp(Expr e1, Expr e2)
+ {
+ if (e1 == Expr.True) return e2;
+ if (e2 == Expr.True) return e1;
+ if (e1 == Expr.False || e2 == Expr.False) return Expr.False;
+ return Expr.And(e1, e2);
+ }
+
+ public static Expr OrSimp(Expr e1, Expr e2)
+ {
+ if (e1 == Expr.False) return e2;
+ if (e2 == Expr.False) return e1;
+ if (e1 == Expr.True || e2 == Expr.True) return Expr.True;
+ return Expr.Or(e1, e2);
+ }
+ }
+
+ class Disjunct
+ {
+ public static int DisjunctBound = 3;
+ HashSet<int> pos;
+ HashSet<int> neg;
+ bool isTrue;
+
+ public Disjunct()
+ {
+ isTrue = true;
+ pos = new HashSet<int>();
+ neg = new HashSet<int>();
+ }
+
+ public Disjunct(IEnumerable<int> pos, IEnumerable<int> neg)
+ {
+ this.isTrue = false;
+ this.pos = new HashSet<int>(pos);
+ this.neg = new HashSet<int>(neg);
+ if (this.pos.Overlaps(this.neg))
+ {
+ this.isTrue = true;
+ this.pos = new HashSet<int>();
+ this.neg = new HashSet<int>();
+ }
+ if (this.pos.Count + this.neg.Count > DisjunctBound)
+ {
+ // Set to true
+ this.isTrue = true;
+ this.pos = new HashSet<int>();
+ this.neg = new HashSet<int>();
+ }
+
+ }
+
+ public Disjunct OR(Disjunct that)
+ {
+ if (isTrue)
+ return this;
+ if (that.isTrue)
+ return that;
+
+ return new Disjunct(this.pos.Concat(that.pos), this.neg.Concat(that.neg));
+ }
+
+ public bool Implies(Disjunct that)
+ {
+ if (isTrue) return that.isTrue;
+ if (that.isTrue) return true;
+
+ return pos.IsSubsetOf(that.pos) && neg.IsSubsetOf(that.neg);
+ }
+
+ public Expr Gamma(List<Expr> vars)
+ {
+ if (isTrue) return Expr.True;
+ Expr ret = Expr.False;
+ pos.Iter(i => ret = ExprExt.OrSimp(ret, vars[i]));
+ neg.Iter(i => ret = ExprExt.OrSimp(ret, Expr.Not(vars[i])));
+ return ret;
+ }
+ }
+
+ // Conjunction of Disjuncts
+ List<Disjunct> conjuncts;
+ bool isFalse;
+
+ public PredicateAbsElem()
+ {
+ this.conjuncts = new List<Disjunct>();
+ this.isFalse = true;
+ }
+
+ public IAbstractDomain Bottom()
+ {
+ return new PredicateAbsElem();
+ }
+
+ public IAbstractDomain Join(List<Model.Element> state)
+ {
+ if (state.Any(me => !(me is Model.Boolean)))
+ throw new AbsHoudiniInternalError("Predicate Abstraction requires that each argument be of type bool");
+
+ // quick return if this == true
+ if (!this.isFalse && conjuncts.Count == 0)
+ return this;
+
+ var ret = new PredicateAbsElem();
+ ret.isFalse = false;
+
+ for (int i = 0; i < state.Count; i++)
+ {
+ var b = (state[i] as Model.Boolean).Value;
+ Disjunct d = null;
+ if (b) d = new Disjunct(new int[] { i }, new int[] { });
+ else d = new Disjunct(new int[] { }, new int[] { i });
+
+ if (isFalse)
+ ret.AddDisjunct(d);
+ else
+ {
+ conjuncts.Iter(c => ret.AddDisjunct(c.OR(d)));
+ }
+ }
+
+ return ret;
+
+ }
+
+ public Expr Gamma(List<Expr> vars)
+ {
+ if (isFalse) return Expr.False;
+ Expr ret = Expr.True;
+
+ foreach (var c in conjuncts)
+ {
+ ret = ExprExt.AndSimp(ret, c.Gamma(vars));
+ }
+
+ return ret;
+ }
+
+ private void AddDisjunct(Disjunct d)
+ {
+ if (conjuncts.Any(c => c.Implies(d)))
+ return;
+
+ conjuncts.RemoveAll(c => d.Implies(c));
+ conjuncts.Add(d);
+ }
+ }
+
// [false -- (x == true) -- true]
public class HoudiniConst : IAbstractDomain
{
diff --git a/Test/AbsHoudini/pred1.bpl b/Test/AbsHoudini/pred1.bpl new file mode 100644 index 00000000..fc37a15b --- /dev/null +++ b/Test/AbsHoudini/pred1.bpl @@ -0,0 +1,23 @@ +function {:existential true} b0(x:bool, y:bool): bool;
+function {:existential true} b1(x:bool, y:bool): bool;
+function {:existential true} b2(x:bool, y:bool): bool;
+
+var g: int;
+
+procedure main()
+modifies g;
+ensures b0(g == 0, g == 5);
+{
+ g := 0;
+ if(*) { g := 5; }
+ call foo();
+}
+
+procedure foo()
+ modifies g;
+ requires b1(g == 0, g == 5);
+ ensures b2(g == 0, g == 5);
+{
+ assume g != 5;
+}
+
diff --git a/Test/AbsHoudini/pred2.bpl b/Test/AbsHoudini/pred2.bpl new file mode 100644 index 00000000..3ce948ce --- /dev/null +++ b/Test/AbsHoudini/pred2.bpl @@ -0,0 +1,12 @@ +function {:existential true} b0(x:bool): bool;
+
+var g: int;
+
+procedure main()
+modifies g;
+ensures b0(g == old(g));
+{
+ if(*) { g := 5; }
+ assume g != 5;
+}
+
diff --git a/Test/AbsHoudini/pred3.bpl b/Test/AbsHoudini/pred3.bpl new file mode 100644 index 00000000..450efde4 --- /dev/null +++ b/Test/AbsHoudini/pred3.bpl @@ -0,0 +1,24 @@ +function {:existential true} b0(x:bool, y:bool): bool;
+function {:existential true} b1(x:bool, y:bool): bool;
+function {:existential true} b2(x:bool, y:bool): bool;
+
+var g: int;
+
+procedure main()
+modifies g;
+ensures b0(g == 0, g == 5);
+{
+ assume 0 == old(g) || 1 == old(g);
+ g := 0;
+ if(*) { g := 5; }
+ call foo();
+}
+
+procedure foo()
+ modifies g;
+ requires b1(g == 0, g == 5);
+ ensures b2(old(g) == 0, old(g) == 5);
+{
+ assume g != 5;
+}
+
|