diff options
| author |  tabarbe <unknown> | 2010-08-27 21:15:08 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-27 21:15:08 +0000 |
| commit | c333ecd2f30badea143e79f5f944a8c63398b959 (patch) | |
| tree | 28b04dc9f46d6fa90b4fdf38ffb24898bdc139b0 /Source/AIFramework/VariableMap/VariableMapLattice.cs | |
| parent | dce6bf46952b5dd470ae841cae03706dbc30bc3b (diff) | |
Boogie: Removed some errors with code contracts (commenting out doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
Diffstat (limited to 'Source/AIFramework/VariableMap/VariableMapLattice.cs')
| -rw-r--r-- | Source/AIFramework/VariableMap/VariableMapLattice.cs | 1505 |
1 files changed, 754 insertions, 751 deletions
diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.cs b/Source/AIFramework/VariableMap/VariableMapLattice.cs index e0b9ac04..169156b0 100644 --- a/Source/AIFramework/VariableMap/VariableMapLattice.cs +++ b/Source/AIFramework/VariableMap/VariableMapLattice.cs @@ -3,852 +3,855 @@ // Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
-namespace Microsoft.AbstractInterpretationFramework
-{
- using System.Diagnostics.Contracts;
- using System.Collections;
- using System.Collections.Generic;
- using System.Diagnostics;
-
- using Microsoft.AbstractInterpretationFramework;
- using Microsoft.AbstractInterpretationFramework.Collections;
-
- using Microsoft.Boogie;
- using IMutableSet = Microsoft.Boogie.Set;
- using HashSet = Microsoft.Boogie.Set;
- using ISet = Microsoft.Boogie.Set;
-
- /// <summary>
- /// Creates a lattice that works for several variables given a MicroLattice. Assumes
- /// if one variable is bottom, then all variables are bottom.
- /// </summary>
- public class VariableMapLattice : Lattice
- {
- private class Elt : Element
- {
- /// <summary>
- /// IsBottom(e) iff e.constraints == null
- /// </summary>
- /*MayBeNull*/
- private IFunctionalMap constraints; // of type IVariable -> LATTICE_ELEMENT
- public IFunctionalMap Constraints
- {
- get
- {
- return this.constraints;
- }
- }
+namespace Microsoft.AbstractInterpretationFramework {
+ using System.Diagnostics.Contracts;
+ using System.Collections;
+ using System.Collections.Generic;
+ using System.Diagnostics;
+
+ using Microsoft.AbstractInterpretationFramework;
+ using Microsoft.AbstractInterpretationFramework.Collections;
+
+ using Microsoft.Boogie;
+ using IMutableSet = Microsoft.Boogie.Set;
+ using HashSet = Microsoft.Boogie.Set;
+ using ISet = Microsoft.Boogie.Set;
+
+ /// <summary>
+ /// Creates a lattice that works for several variables given a MicroLattice. Assumes
+ /// if one variable is bottom, then all variables are bottom.
+ /// </summary>
+ public class VariableMapLattice : Lattice {
+ private class Elt : Element {
+ /// <summary>
+ /// IsBottom(e) iff e.constraints == null
+ /// </summary>
+ /*MayBeNull*/
+ private IFunctionalMap constraints; // of type IVariable -> LATTICE_ELEMENT
+ public IFunctionalMap Constraints {
+ get {
+ return this.constraints;
+ }
+ }
- private Elt(bool top) {
- if (top) {
- this.constraints = FunctionalHashtable.Empty;
- } else {
- this.constraints = null;
- }
- }
+ private Elt(bool top) {
+ if (top) {
+ this.constraints = FunctionalHashtable.Empty;
+ } else {
+ this.constraints = null;
+ }
+ }
- public override Element/*!*/ Clone() {
-Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(this.constraints);
- }
-
- [Pure]
- public override string/*!*/ ToString() {
-Contract.Ensures(Contract.Result<string>() != null);
- if (constraints == null) {
- return "<bottom>";
- }
- string s = "[";
- string sep = "";
- foreach(IVariable/*!*/ v in cce.NonNull(constraints.Keys)){
-Contract.Assert(v != null);
- Element m = (Element)constraints[v];
- s += sep + v.Name + " -> " + m;
- sep = ", ";
- }
- return s + "]";
- }
+ public override Element/*!*/ Clone() {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(this.constraints);
+ }
- public static Elt/*!*/ Top = new Elt(true);
- public static Elt/*!*/ Bottom = new Elt(false);
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(Top != null);
- Contract.Invariant(Bottom != null);
-}
+ [Pure]
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ if (constraints == null) {
+ return "<bottom>";
+ }
+ string s = "[";
+ string sep = "";
+ foreach (IVariable/*!*/ v in cce.NonNull(constraints.Keys)) {
+ Contract.Assert(v != null);
+ Element m = (Element)constraints[v];
+ s += sep + v.Name + " -> " + m;
+ sep = ", ";
+ }
+ return s + "]";
+ }
+ public static Elt/*!*/ Top = new Elt(true);
+ public static Elt/*!*/ Bottom = new Elt(false);
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Top != null);
+ Contract.Invariant(Bottom != null);
+ }
- public Elt(IFunctionalMap constraints)
- {
- this.constraints = constraints;
- }
- public bool IsBottom {
- get {
- return this.constraints == null;
- }
- }
+ public Elt(IFunctionalMap constraints) {
+ this.constraints = constraints;
+ }
- public int Count { get { return this.constraints == null ? 0 : this.constraints.Count; } }
+ public bool IsBottom {
+ get {
+ return this.constraints == null;
+ }
+ }
- public IEnumerable/*<IVariable>*//*!*/ Variables {
- get {
- Contract.Requires(!this.IsBottom);
- Contract.Ensures(Contract.Result<IEnumerable>() != null);
- Contract.Assume(this.constraints != null);
- return cce.NonNull(this.constraints.Keys);
- }
- }
+ public int Count {
+ get {
+ return this.constraints == null ? 0 : this.constraints.Count;
+ }
+ }
- public IEnumerable/*<IVariable>*//*!*/ SortedVariables(/*maybe null*/ IComparer variableComparer) {
- Contract.Ensures(Contract.Result<IEnumerable>() != null);
- if (variableComparer == null) {
- return Variables;
- } else {
- ArrayList /*IVariable*/ vars = new ArrayList /*IVariable*/ (Count);
- foreach (IVariable variable in Variables) {
- vars.Add(variable);
- }
- vars.Sort(variableComparer);
- return vars;
- }
- }
-
- public Element Lookup(IVariable v)
- {
- if ((v == null) || (this.constraints == null)) { return null; }
- return (Element)this.constraints[v];
- }
+ public IEnumerable/*<IVariable>*//*!*/ Variables {
+ get {
+ Contract.Requires(!this.IsBottom);
+ Contract.Ensures(Contract.Result<IEnumerable>() != null);
+ Contract.Assume(this.constraints != null);
+ return cce.NonNull(this.constraints.Keys);
+ }
+ }
- public Element this [IVariable/*!*/ key] {
- get{
- Contract.Requires(!this.IsBottom);
- Contract.Requires(key != null);
- Contract.Assume(this.constraints != null);
- return (Element)constraints[key];
- }
- }
+ public IEnumerable/*<IVariable>*//*!*/ SortedVariables(/*maybe null*/ IComparer variableComparer) {
+ Contract.Ensures(Contract.Result<IEnumerable>() != null);
+ if (variableComparer == null) {
+ return Variables;
+ } else {
+ ArrayList /*IVariable*/ vars = new ArrayList /*IVariable*/ (Count);
+ foreach (IVariable variable in Variables) {
+ vars.Add(variable);
+ }
+ vars.Sort(variableComparer);
+ return vars;
+ }
+ }
- /// <summary>
- /// Add a new entry in the functional map: var --> value.
- /// If the variable is already there, throws an exception
- /// </summary>
- public Elt/*!*/ Add(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice){
-Contract.Requires(microLattice != null);
-Contract.Requires(value != null);
-Contract.Requires(var != null);
-Contract.Requires((!this.IsBottom));
-Contract.Ensures(Contract.Result<Elt>() != null);
- Contract.Assume(this.constraints != null);
- Contract.Assert(!this.constraints.Contains(var));
-
- if (microLattice.IsBottom(value)) { return Bottom; }
- if (microLattice.IsTop(value)) { return this.Remove(var, microLattice); }
-
- return new Elt(this.constraints.Add(var, value));
- }
+ public Element Lookup(IVariable v) {
+ if ((v == null) || (this.constraints == null)) {
+ return null;
+ }
+ return (Element)this.constraints[v];
+ }
- /// <summary>
- /// Set the value of the variable in the functional map
- /// If the variable is not already there, throws an exception
- /// </summary>
- public Elt/*!*/ Set(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice){
- Contract.Requires(microLattice != null);
- Contract.Requires(value != null);
- Contract.Requires(var != null);
- Contract.Ensures(Contract.Result<Elt>() != null);
- if(microLattice.IsBottom(value)) { return Bottom; }
- if(microLattice.IsTop(value)) { return this.Remove(var, microLattice); }
-
- Contract.Assume(this.constraints != null);
- Contract.Assert(this.constraints.Contains(var));
-
- // this.constraints[var] = value;
- IFunctionalMap newMap = this.constraints.Set(var, value);
-
- return new Elt(newMap);
- }
+ public Element this[IVariable/*!*/ key] {
+ get {
+ Contract.Requires(!this.IsBottom);
+ Contract.Requires(key != null);
+ Contract.Assume(this.constraints != null);
+ return (Element)constraints[key];
+ }
+ }
- public Elt/*!*/ Remove(IVariable/*!*/ var, MicroLattice microLattice){
-Contract.Requires(var != null);
-Contract.Ensures(Contract.Result<Elt>() != null);
- if (this.IsBottom) { return this; }
- Contract.Assume(this.constraints != null);
- return new Elt(this.constraints.Remove(var));
- }
+ /// <summary>
+ /// Add a new entry in the functional map: var --> value.
+ /// If the variable is already there, throws an exception
+ /// </summary>
+ public Elt/*!*/ Add(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice) {
+ Contract.Requires(microLattice != null);
+ Contract.Requires(value != null);
+ Contract.Requires(var != null);
+ Contract.Requires((!this.IsBottom));
+ Contract.Ensures(Contract.Result<Elt>() != null);
+ Contract.Assume(this.constraints != null);
+ Contract.Assert(!this.constraints.Contains(var));
+
+ if (microLattice.IsBottom(value)) {
+ return Bottom;
+ }
+ if (microLattice.IsTop(value)) {
+ return this.Remove(var, microLattice);
+ }
- public Elt/*!*/ Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName, MicroLattice/*!*/ microLattice){
-Contract.Requires(microLattice != null);
-Contract.Requires(newName != null);
-Contract.Requires(oldName != null);
-Contract.Requires((!this.IsBottom));
-Contract.Ensures(Contract.Result<Elt>() != null);
- Element value = this[oldName];
- if (value == null) { return this; } // 'oldName' isn't in the map, so neither will be 'newName'
- Contract.Assume(this.constraints != null);
- IFunctionalMap newMap = this.constraints.Remove(oldName);
- newMap = newMap.Add(newName, value);
- return new Elt(newMap);
- }
+ return new Elt(this.constraints.Add(var, value));
+ }
- [Pure]
- public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
- throw new System.NotImplementedException();
- }
+ /// <summary>
+ /// Set the value of the variable in the functional map
+ /// If the variable is not already there, throws an exception
+ /// </summary>
+ public Elt/*!*/ Set(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice) {
+ Contract.Requires(microLattice != null);
+ Contract.Requires(value != null);
+ Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<Elt>() != null);
+ if (microLattice.IsBottom(value)) {
+ return Bottom;
+ }
+ if (microLattice.IsTop(value)) {
+ return this.Remove(var, microLattice);
+ }
- } // class
+ Contract.Assume(this.constraints != null);
+ Contract.Assert(this.constraints.Contains(var));
- private readonly MicroLattice/*!*/ microLattice;
+ // this.constraints[var] = value;
+ IFunctionalMap newMap = this.constraints.Set(var, value);
- private readonly IPropExprFactory/*!*/ propExprFactory;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(microLattice != null);
- Contract.Invariant(propExprFactory != null);
-}
+ return new Elt(newMap);
+ }
-
- private readonly /*maybe null*/IComparer variableComparer;
-
- public VariableMapLattice(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valueExprFactory, MicroLattice/*!*/ microLattice, /*maybe null*/IComparer variableComparer)
- : base(valueExprFactory){
-Contract.Requires(microLattice != null);
-Contract.Requires(valueExprFactory != null);
-Contract.Requires(propExprFactory != null);
- this.propExprFactory = propExprFactory;
- this.microLattice = microLattice;
- this.variableComparer = variableComparer;
- // base(valueExprFactory);
+ public Elt/*!*/ Remove(IVariable/*!*/ var, MicroLattice microLattice) {
+ Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<Elt>() != null);
+ if (this.IsBottom) {
+ return this;
}
+ Contract.Assume(this.constraints != null);
+ return new Elt(this.constraints.Remove(var));
+ }
- protected override object/*!*/ UniqueId{
- get{
-Contract.Ensures(Contract.Result<object>() != null);
- return this.microLattice.GetType(); } }
+ public Elt/*!*/ Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName, MicroLattice/*!*/ microLattice) {
+ Contract.Requires(microLattice != null);
+ Contract.Requires(newName != null);
+ Contract.Requires(oldName != null);
+ Contract.Requires((!this.IsBottom));
+ Contract.Ensures(Contract.Result<Elt>() != null);
+ Element value = this[oldName];
+ if (value == null) {
+ return this;
+ } // 'oldName' isn't in the map, so neither will be 'newName'
+ Contract.Assume(this.constraints != null);
+ IFunctionalMap newMap = this.constraints.Remove(oldName);
+ newMap = newMap.Add(newName, value);
+ return new Elt(newMap);
+ }
- public override Element/*!*/ Top{
-get{Contract.Ensures(Contract.Result<Element>() != null);
- return Elt.Top; } }
+ [Pure]
+ public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
+ throw new System.NotImplementedException();
+ }
- public override Element Bottom{get{
-Contract.Ensures(Contract.Result<Element>() != null);
- return Elt.Bottom; } }
+ } // class
- public override bool IsTop(Element/*!*/ element){
-Contract.Requires(element != null);
- Elt e = (Elt)element;
- return !e.IsBottom && e.Count == 0;
- }
+ private readonly MicroLattice/*!*/ microLattice;
- public override bool IsBottom(Element/*!*/ element){
-Contract.Requires(element != null);
- return ((Elt)element).IsBottom;
- }
+ private readonly IPropExprFactory/*!*/ propExprFactory;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(microLattice != null);
+ Contract.Invariant(propExprFactory != null);
+ }
- protected override bool AtMost(Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
-
- // return true iff every constraint in "this" is no weaker than the corresponding
- // constraint in "that" and there are no additional constraints in "that"
- foreach(IVariable/*!*/ var in a.Variables){
-Contract.Assert(var != null);
- Element thisValue = cce.NonNull(a[var]);
-
- Element thatValue = b[var];
- if (thatValue == null) { continue; } // it's okay for "a" to know something "b" doesn't
-
- if (this.microLattice.LowerThan(thisValue, thatValue)) { continue; } // constraint for "var" satisfies AtMost relation
-
- return false;
- }
- foreach(IVariable/*!*/ var in b.Variables){
-Contract.Assert(var != null);
- if (a.Lookup(var) != null) { continue; } // we checked this case in the loop above
-
- Element thatValue = cce.NonNull(b[var]);
- if (this.microLattice.IsTop(thatValue)) { continue; } // this is a trivial constraint
-
- return false;
- }
- return true;
- }
- private Elt/*!*/ AddConstraint(Element/*!*/ element, IVariable/*!*/ var, /*MicroLattice*/Element/*!*/ newValue) {
-Contract.Requires((newValue != null));
-Contract.Requires((var != null));
-Contract.Requires((element != null));
-Contract.Ensures(Contract.Result<Elt>() != null);
- Elt e = (Elt)element;
+ private readonly /*maybe null*/IComparer variableComparer;
+
+ public VariableMapLattice(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valueExprFactory, MicroLattice/*!*/ microLattice, /*maybe null*/IComparer variableComparer)
+ : base(valueExprFactory) {
+ Contract.Requires(microLattice != null);
+ Contract.Requires(valueExprFactory != null);
+ Contract.Requires(propExprFactory != null);
+ this.propExprFactory = propExprFactory;
+ this.microLattice = microLattice;
+ this.variableComparer = variableComparer;
+ // base(valueExprFactory);
+ }
+
+ protected override object/*!*/ UniqueId {
+ get {
+ Contract.Ensures(Contract.Result<object>() != null);
+ return this.microLattice.GetType();
+ }
+ }
+
+ public override Element/*!*/ Top {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return Elt.Top;
+ }
+ }
+
+ public override Element Bottom {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return Elt.Bottom;
+ }
+ }
+
+ public override bool IsTop(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ Elt e = (Elt)element;
+ return !e.IsBottom && e.Count == 0;
+ }
+
+ public override bool IsBottom(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ return ((Elt)element).IsBottom;
+ }
+
+ protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+
+ // return true iff every constraint in "this" is no weaker than the corresponding
+ // constraint in "that" and there are no additional constraints in "that"
+ foreach (IVariable/*!*/ var in a.Variables) {
+ Contract.Assert(var != null);
+ Element thisValue = cce.NonNull(a[var]);
+
+ Element thatValue = b[var];
+ if (thatValue == null) {
+ continue;
+ } // it's okay for "a" to know something "b" doesn't
+
+ if (this.microLattice.LowerThan(thisValue, thatValue)) {
+ continue;
+ } // constraint for "var" satisfies AtMost relation
+
+ return false;
+ }
+ foreach (IVariable/*!*/ var in b.Variables) {
+ Contract.Assert(var != null);
+ if (a.Lookup(var) != null) {
+ continue;
+ } // we checked this case in the loop above
+
+ Element thatValue = cce.NonNull(b[var]);
+ if (this.microLattice.IsTop(thatValue)) {
+ continue;
+ } // this is a trivial constraint
+
+ return false;
+ }
+ return true;
+ }
+
+ private Elt/*!*/ AddConstraint(Element/*!*/ element, IVariable/*!*/ var, /*MicroLattice*/Element/*!*/ newValue) {
+ Contract.Requires((newValue != null));
+ Contract.Requires((var != null));
+ Contract.Requires((element != null));
+ Contract.Ensures(Contract.Result<Elt>() != null);
+ Elt e = (Elt)element;
- if (!e.IsBottom && !this.microLattice.IsBottom(newValue)) // if we're not at bottom
+ if (!e.IsBottom && !this.microLattice.IsBottom(newValue)) // if we're not at bottom
{
- /*MicroLattice*/Element currentValue = e[var];
-
- if (currentValue == null)
- {
- // No information currently, so we just add the new info.
- return e.Add(var, newValue, this.microLattice);
- }
- else
- {
- // Otherwise, take the meet of the new and current info.
- //return e.Add(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
- return e.Set(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
- }
- }
- return e;
+ /*MicroLattice*/
+ Element currentValue = e[var];
+
+ if (currentValue == null) {
+ // No information currently, so we just add the new info.
+ return e.Add(var, newValue, this.microLattice);
+ } else {
+ // Otherwise, take the meet of the new and current info.
+ //return e.Add(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
+ return e.Set(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
}
+ }
+ return e;
+ }
- public override string/*!*/ ToString(Element/*!*/ element){
-Contract.Requires(element != null);
-Contract.Ensures(Contract.Result<string>() != null);
- Elt e = (Elt)element;
+ public override string/*!*/ ToString(Element/*!*/ element) {
+ Contract.Requires(element != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+ Elt e = (Elt)element;
- if (IsTop(e)) { return "<top>"; }
- if (IsBottom(e)) { return "<bottom>"; }
+ if (IsTop(e)) {
+ return "<top>";
+ }
+ if (IsBottom(e)) {
+ return "<bottom>";
+ }
- int k = 0;
- System.Text.StringBuilder buffer = new System.Text.StringBuilder();
- foreach(IVariable/*!*/ key in e.SortedVariables(variableComparer)){
-Contract.Assert(key != null);
- if (k++ > 0) { buffer.Append("; "); }
- buffer.AppendFormat("{0} = {1}", key, e[key]);
- }
- return buffer.ToString();
+ int k = 0;
+ System.Text.StringBuilder buffer = new System.Text.StringBuilder();
+ foreach (IVariable/*!*/ key in e.SortedVariables(variableComparer)) {
+ Contract.Assert(key != null);
+ if (k++ > 0) {
+ buffer.Append("; ");
}
+ buffer.AppendFormat("{0} = {1}", key, e[key]);
+ }
+ return buffer.ToString();
+ }
- public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
-
- IFunctionalMap newMap = FunctionalHashtable.Empty;
- foreach(IVariable/*!*/ key in a.Variables){
-Contract.Assert(key != null);
- Element aValue = a[key];
- Element bValue = b[key];
-
- if (aValue != null && bValue != null)
- {
- // Keep only the variables known to both elements.
- Element newValue = this.microLattice.Join(aValue, bValue);
- newMap = newMap.Add(key, newValue);
- }
- }
- Elt/*!*/ join = new Elt(newMap);
- Contract.Assert(join != null);
-
- // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
-
- return join;
+ public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+
+ IFunctionalMap newMap = FunctionalHashtable.Empty;
+ foreach (IVariable/*!*/ key in a.Variables) {
+ Contract.Assert(key != null);
+ Element aValue = a[key];
+ Element bValue = b[key];
+
+ if (aValue != null && bValue != null) {
+ // Keep only the variables known to both elements.
+ Element newValue = this.microLattice.Join(aValue, bValue);
+ newMap = newMap.Add(key, newValue);
}
+ }
+ Elt/*!*/ join = new Elt(newMap);
+ Contract.Assert(join != null);
+
+ // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
- public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
+ return join;
+ }
- IFunctionalMap newMap = FunctionalHashtable.Empty;
- foreach(IVariable/*!*/ key in a.Variables){
-Contract.Assert(key != null);
-Element/*!*/ aValue = cce.NonNull(a[key]);
- Element bValue = b[key];
+ public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
- Element newValue =
- bValue == null ? aValue :
- this.microLattice.Meet(aValue, bValue);
+ IFunctionalMap newMap = FunctionalHashtable.Empty;
+ foreach (IVariable/*!*/ key in a.Variables) {
+ Contract.Assert(key != null);
+ Element/*!*/ aValue = cce.NonNull(a[key]);
+ Element bValue = b[key];
- newMap = newMap.Add(key, newValue);
- }
- foreach(IVariable/*!*/ key in b.Variables){
-Contract.Assert(key != null);
- Element aValue = a[key];
- Element bValue = b[key]; Debug.Assert(bValue != null);
-
- if (aValue == null)
- {
- // It's a variable we didn't cover in the last loop.
- newMap = newMap.Add(key, bValue);
- }
- }
- return new Elt(newMap);
+ Element newValue =
+ bValue == null ? aValue :
+ this.microLattice.Meet(aValue, bValue);
+
+ newMap = newMap.Add(key, newValue);
+ }
+ foreach (IVariable/*!*/ key in b.Variables) {
+ Contract.Assert(key != null);
+ Element aValue = a[key];
+ Element bValue = b[key];
+ Debug.Assert(bValue != null);
+
+ if (aValue == null) {
+ // It's a variable we didn't cover in the last loop.
+ newMap = newMap.Add(key, bValue);
}
+ }
+ return new Elt(newMap);
+ }
- /// <summary>
- /// Perform the pointwise widening of the elements in the map
- /// </summary>
- public override Element/*!*/ Widen (Element/*!*/ first, Element/*!*/ second) {
-Contract.Requires((second != null));
-Contract.Requires((first != null));
-Contract.Ensures(Contract.Result<Element>() != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
-
- // Note we have to add those cases as we do not have a "NonTrivialWiden" method
- if(a.IsBottom)
- return new Elt(b.Constraints);
- if(b.IsBottom)
- return new Elt(a.Constraints);
-
- IFunctionalMap newMap = FunctionalHashtable.Empty;
- foreach(IVariable/*!*/ key in a.Variables){
-Contract.Assert(key != null);
- Element aValue = a[key];
- Element bValue = b[key];
-
- if (aValue != null && bValue != null)
- {
- // Keep only the variables known to both elements.
- Element newValue = this.microLattice.Widen(aValue, bValue);
- newMap = newMap.Add(key, newValue);
- }
- }
- Element/*!*/ widen= new Elt(newMap);
+ /// <summary>
+ /// Perform the pointwise widening of the elements in the map
+ /// </summary>
+ public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
+ Contract.Requires((second != null));
+ Contract.Requires((first != null));
+ Contract.Ensures(Contract.Result<Element>() != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+
+ // Note we have to add those cases as we do not have a "NonTrivialWiden" method
+ if (a.IsBottom)
+ return new Elt(b.Constraints);
+ if (b.IsBottom)
+ return new Elt(a.Constraints);
+
+ IFunctionalMap newMap = FunctionalHashtable.Empty;
+ foreach (IVariable/*!*/ key in a.Variables) {
+ Contract.Assert(key != null);
+ Element aValue = a[key];
+ Element bValue = b[key];
+
+ if (aValue != null && bValue != null) {
+ // Keep only the variables known to both elements.
+ Element newValue = this.microLattice.Widen(aValue, bValue);
+ newMap = newMap.Add(key, newValue);
+ }
+ }
+ Element/*!*/ widen = new Elt(newMap);
Contract.Assert(widen != null);
- // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
+ // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
- return widen;
- }
+ return widen;
+ }
- internal static ISet/*<IVariable!>*//*!*/ VariablesInExpression(IExpr/*!*/ e, ISet/*<IVariable!>*//*!*/ ignoreVars){
-Contract.Requires(ignoreVars != null);
-Contract.Requires(e != null);
- Contract.Ensures(Contract.Result<ISet>() != null);
- HashSet s = new HashSet();
+ internal static ISet/*<IVariable!>*//*!*/ VariablesInExpression(IExpr/*!*/ e, ISet/*<IVariable!>*//*!*/ ignoreVars) {
+ Contract.Requires(ignoreVars != null);
+ Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<ISet>() != null);
+ HashSet s = new HashSet();
- IFunApp f = e as IFunApp;
- IFunction lambda = e as IFunction;
+ IFunApp f = e as IFunApp;
+ IFunction lambda = e as IFunction;
- if (e is IVariable)
- {
- if (!ignoreVars.Contains(e))
- s.Add(e);
- }
- else if (f != null) // e is IFunApp
- {
- foreach(IExpr/*!*/ arg in f.Arguments){
-Contract.Assert(arg != null);
- s.AddAll(VariablesInExpression(arg, ignoreVars));
- }
- }
- else if (lambda != null)
+ if (e is IVariable) {
+ if (!ignoreVars.Contains(e))
+ s.Add(e);
+ } else if (f != null) // e is IFunApp
{
- IMutableSet x = new HashSet(1);
- x.Add(lambda.Param);
+ foreach (IExpr/*!*/ arg in f.Arguments) {
+ Contract.Assert(arg != null);
+ s.AddAll(VariablesInExpression(arg, ignoreVars));
+ }
+ } else if (lambda != null) {
+ IMutableSet x = new HashSet(1);
+ x.Add(lambda.Param);
+
+ // Ignore the bound variable
+ s.AddAll(VariablesInExpression(lambda.Body, cce.NonNull(Set.Union(ignoreVars, x))));
+ } else if (e is IUnknown) {
+ // skip (actually, it would be appropriate to return the universal set of all variables)
+ } else {
+ Debug.Assert(false, "case not handled: " + e);
+ }
+ return s;
+ }
- // Ignore the bound variable
- s.AddAll(VariablesInExpression(lambda.Body, cce.NonNull(Set.Union(ignoreVars, x))));
- }
- else if (e is IUnknown)
- {
- // skip (actually, it would be appropriate to return the universal set of all variables)
- }
- else
- {
- Debug.Assert(false, "case not handled: " + e);
- }
- return s;
+
+ private static ArrayList/*<IExpr>*//*!*/ FindConjuncts(IExpr e) {
+ Contract.Ensures(Contract.Result<ArrayList>() != null);
+ ArrayList result = new ArrayList();
+
+ IFunApp f = e as IFunApp;
+ if (f != null) {
+ if (f.FunctionSymbol.Equals(Prop.And)) {
+ foreach (IExpr arg in f.Arguments) {
+ result.AddRange(FindConjuncts(arg));
+ }
+ } else if (f.FunctionSymbol.Equals(Prop.Or)
+ || f.FunctionSymbol.Equals(Prop.Implies)) {
+ // Do nothing.
+ } else {
+ result.Add(e);
}
+ } else {
+ result.Add(e);
+ }
+ return result;
+ }
- private static ArrayList/*<IExpr>*//*!*/ FindConjuncts(IExpr e)
- {
- Contract.Ensures(Contract.Result<ArrayList>() != null);
- ArrayList result = new ArrayList();
+ private static bool IsSimpleEquality(IExpr expr, out IVariable left, out IVariable right) {
+ Contract.Ensures(!Contract.Result<bool>() || Contract.ValueAtReturn(out left) != null && Contract.ValueAtReturn(out right) != null);
+ left = null;
+ right = null;
- IFunApp f = e as IFunApp;
- if (f != null)
- {
- if (f.FunctionSymbol.Equals(Prop.And))
- {
- foreach (IExpr arg in f.Arguments)
- {
- result.AddRange(FindConjuncts(arg));
- }
- }
- else if (f.FunctionSymbol.Equals(Prop.Or)
- || f.FunctionSymbol.Equals(Prop.Implies))
- {
- // Do nothing.
- }
- else
- {
- result.Add(e);
- }
- }
- else
- {
- result.Add(e);
- }
+ // See if we have an equality
+ IFunApp nary = expr as IFunApp;
+ if (nary == null || !nary.FunctionSymbol.Equals(Value.Eq)) {
+ return false;
+ }
- return result;
- }
+ // See if it is an equality of two variables
+ IVariable idLeft = nary.Arguments[0] as IVariable;
+ IVariable idRight = nary.Arguments[1] as IVariable;
+ if (idLeft == null || idRight == null) {
+ return false;
+ }
- private static bool IsSimpleEquality(IExpr expr, out IVariable left, out IVariable right)
- {
- Contract.Ensures(!Contract.Result<bool>() || Contract.ValueAtReturn(out left) != null && Contract.ValueAtReturn(out right) != null);
- left = null;
- right = null;
-
- // See if we have an equality
- IFunApp nary = expr as IFunApp;
- if (nary == null || !nary.FunctionSymbol.Equals(Value.Eq)) { return false; }
-
- // See if it is an equality of two variables
- IVariable idLeft = nary.Arguments[0] as IVariable;
- IVariable idRight = nary.Arguments[1] as IVariable;
- if (idLeft == null || idRight == null) { return false; }
-
- left = idLeft;
- right = idRight;
- return true;
- }
+ left = idLeft;
+ right = idRight;
+ return true;
+ }
- /// <summary>
- /// Returns true iff the expression is in the form var == arithmeticExpr
- /// </summary>
- private static bool IsArithmeticExpr(IExpr/*!*/ expr){
-Contract.Requires(expr != null);
- // System.Console.WriteLine("\t\tIsArithmetic called with {0} of type {1}", expr, expr.GetType().ToString());
-
- if(expr is IVariable) // expr is a variable
- return true;
- else if(expr is IFunApp) // may be ==, +, -, /, % or an integer
+ /// <summary>
+ /// Returns true iff the expression is in the form var == arithmeticExpr
+ /// </summary>
+ private static bool IsArithmeticExpr(IExpr/*!*/ expr) {
+ Contract.Requires(expr != null);
+ // System.Console.WriteLine("\t\tIsArithmetic called with {0} of type {1}", expr, expr.GetType().ToString());
+
+ if (expr is IVariable) // expr is a variable
+ return true;
+ else if (expr is IFunApp) // may be ==, +, -, /, % or an integer
{
- IFunApp fun = (IFunApp) expr;
+ IFunApp fun = (IFunApp)expr;
+
+ if (fun.FunctionSymbol is IntSymbol) // it is an integer
+ return true;
+ else if (fun.FunctionSymbol.Equals(Int.Negate)) // it is an unary minus
+ return IsArithmeticExpr((IExpr/*!*/)cce.NonNull(fun.Arguments[0]));
+ else if (fun.Arguments.Count != 2) // A function of two or more operands is not arithmetic
+ return false;
+ else {
+ IExpr/*!*/ left = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+ IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
- if(fun.FunctionSymbol is IntSymbol) // it is an integer
- return true;
- else if(fun.FunctionSymbol.Equals(Int.Negate)) // it is an unary minus
- return IsArithmeticExpr((IExpr/*!*/)cce.NonNull(fun.Arguments[0]));
- else if(fun.Arguments.Count != 2) // A function of two or more operands is not arithmetic
+ if (!(left is IVariable || right is IVariable)) // At least one of the two operands must be a variable
return false;
- else
- {
- IExpr/*!*/ left = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
- IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
-
- if(!(left is IVariable || right is IVariable)) // At least one of the two operands must be a variable
- return false;
-
- if(fun.FunctionSymbol.Equals(Value.Eq)
- || fun.FunctionSymbol.Equals(Int.Add)
- || fun.FunctionSymbol.Equals(Int.Sub)
- || fun.FunctionSymbol.Equals(Int.Mul)
- || fun.FunctionSymbol.Equals(Int.Div)
- || fun.FunctionSymbol.Equals(Int.Mod))
- return IsArithmeticExpr(left) && IsArithmeticExpr(right);
- else
- return false;
- }
- }
+
+ if (fun.FunctionSymbol.Equals(Value.Eq)
+ || fun.FunctionSymbol.Equals(Int.Add)
+ || fun.FunctionSymbol.Equals(Int.Sub)
+ || fun.FunctionSymbol.Equals(Int.Mul)
+ || fun.FunctionSymbol.Equals(Int.Div)
+ || fun.FunctionSymbol.Equals(Int.Mod))
+ return IsArithmeticExpr(left) && IsArithmeticExpr(right);
else
- {
- return false;
- }
+ return false;
+ }
+ } else {
+ return false;
}
+ }
- public override IExpr/*!*/ ToPredicate(Element/*!*/ element){
-Contract.Requires(element != null);
-Contract.Ensures(Contract.Result<IExpr>() != null);
- if (IsTop(element)) { return propExprFactory.True; }
- if (IsBottom(element)) { return propExprFactory.False; }
-
- Elt e = (Elt)element;
- IExpr truth = propExprFactory.True;
- IExpr result = truth;
-
- foreach(IVariable/*!*/ variable in e.SortedVariables(variableComparer)){
-Contract.Assert(variable != null);
- Element value = (Element)e[variable];
+ public override IExpr/*!*/ ToPredicate(Element/*!*/ element) {
+ Contract.Requires(element != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ if (IsTop(element)) {
+ return propExprFactory.True;
+ }
+ if (IsBottom(element)) {
+ return propExprFactory.False;
+ }
- if (value == null || this.microLattice.IsTop(value)) { continue; } // Skip variables about which we know nothing.
- if (this.microLattice.IsBottom(value)) { return propExprFactory.False; }
+ Elt e = (Elt)element;
+ IExpr truth = propExprFactory.True;
+ IExpr result = truth;
- IExpr conjunct = this.microLattice.ToPredicate(variable, value);
+ foreach (IVariable/*!*/ variable in e.SortedVariables(variableComparer)) {
+ Contract.Assert(variable != null);
+ Element value = (Element)e[variable];
- result = (result == truth) ? (IExpr)conjunct : (IExpr)propExprFactory.And(result, conjunct);
- }
- return result;
+ if (value == null || this.microLattice.IsTop(value)) {
+ continue;
+ } // Skip variables about which we know nothing.
+ if (this.microLattice.IsBottom(value)) {
+ return propExprFactory.False;
}
+ IExpr conjunct = this.microLattice.ToPredicate(variable, value);
- public override Element/*!*/ Eliminate(Element/*!*/ element, IVariable/*!*/ variable){
-Contract.Requires(variable != null);
-Contract.Requires(element != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- return cce.NonNull((Elt)element).Remove(variable, this.microLattice);
+ result = (result == truth) ? (IExpr)conjunct : (IExpr)propExprFactory.And(result, conjunct);
+ }
+ return result;
+ }
+
+
+ public override Element/*!*/ Eliminate(Element/*!*/ element, IVariable/*!*/ variable) {
+ //Contract.Requires(variable != null);
+ //Contract.Requires(element != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return cce.NonNull((Elt)element).Remove(variable, this.microLattice);
+ }
+
+ private delegate IExpr/*!*/ OnUnableToInline(IVariable/*!*/ var);
+ private IExpr/*!*/ IdentityVarToExpr(IVariable/*!*/ var) {
+ //Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ return var;
+ }
+
+ /// <summary>
+ /// Return a new expression in which each variable has been
+ /// replaced by an expression representing what is known about
+ /// that variable.
+ /// </summary>
+ private IExpr/*!*/ InlineVariables(Elt/*!*/ element, IExpr/*!*/ expr, ISet/*<IVariable!>*//*!*/ notInlineable,
+ OnUnableToInline/*!*/ unableToInline) {
+ Contract.Requires(unableToInline != null);
+ Contract.Requires(notInlineable != null);
+ Contract.Requires(expr != null);
+ Contract.Requires(element != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ IVariable var = expr as IVariable;
+ if (var != null) {
+ /*MicroLattice*/
+ Element value = element[var];
+ if (notInlineable.Contains(var) || value == null || this.microLattice.IsTop(value)) {
+ return unableToInline(var); // We don't know anything about this variable.
+ } else {
+ // GetFoldExpr returns null when it can yield an expression that
+ // can be substituted for the variable.
+ IExpr valueExpr = this.microLattice.GetFoldExpr(value);
+ return (valueExpr == null) ? var : valueExpr;
}
+ }
+
+ // else
- private delegate IExpr/*!*/ OnUnableToInline(IVariable/*!*/ var);
- private IExpr/*!*/ IdentityVarToExpr(IVariable/*!*/ var){
-Contract.Requires(var != null);
-Contract.Ensures(Contract.Result<IExpr>() != null);
- return var;
+ IFunApp fun = expr as IFunApp;
+ if (fun != null) {
+ IList newargs = new ArrayList();
+ foreach (IExpr/*!*/ arg in fun.Arguments) {
+ Contract.Assert(arg != null);
+ newargs.Add(InlineVariables(element, arg, notInlineable, unableToInline));
}
+ return fun.CloneWithArguments(newargs);
+ }
- /// <summary>
- /// Return a new expression in which each variable has been
- /// replaced by an expression representing what is known about
- /// that variable.
- /// </summary>
- private IExpr/*!*/ InlineVariables(Elt/*!*/ element, IExpr/*!*/ expr, ISet/*<IVariable!>*//*!*/ notInlineable,
- OnUnableToInline/*!*/ unableToInline){
- Contract.Requires(unableToInline != null);
-Contract.Requires(notInlineable != null);
-Contract.Requires(expr != null);
-Contract.Requires(element != null);
- Contract.Ensures(Contract.Result<IExpr>() != null);
- IVariable var = expr as IVariable;
- if (var != null)
- {
- /*MicroLattice*/Element value = element[var];
- if (notInlineable.Contains(var) || value == null || this.microLattice.IsTop(value))
- {
- return unableToInline(var); // We don't know anything about this variable.
- }
- else
- {
- // GetFoldExpr returns null when it can yield an expression that
- // can be substituted for the variable.
- IExpr valueExpr = this.microLattice.GetFoldExpr(value);
- return (valueExpr == null) ? var : valueExpr;
- }
- }
+ // else
- // else
+ IFunction lambda = expr as IFunction;
+ if (lambda != null) {
+ IMutableSet x = new HashSet(1);
+ x.Add(lambda.Param);
- IFunApp fun = expr as IFunApp;
- if (fun != null)
- {
- IList newargs = new ArrayList();
- foreach(IExpr/*!*/ arg in fun.Arguments){
-Contract.Assert(arg != null);
- newargs.Add(InlineVariables(element, arg, notInlineable, unableToInline));
- }
- return fun.CloneWithArguments(newargs);
- }
+ // Don't inline the bound variable
+ return lambda.CloneWithBody(
+ InlineVariables(element, lambda.Body,
+ cce.NonNull(Set.Union(notInlineable, x)), unableToInline)
+ );
+ }
- // else
+ // else
- IFunction lambda = expr as IFunction;
- if (lambda != null)
- {
- IMutableSet x = new HashSet(1);
- x.Add(lambda.Param);
-
- // Don't inline the bound variable
- return lambda.CloneWithBody(
- InlineVariables(element, lambda.Body,
- cce.NonNull(Set.Union(notInlineable, x)), unableToInline)
- );
- }
+ if (expr is IUnknown) {
+ return expr;
+ } else {
+ throw
+ new System.NotImplementedException("cannot inline identifies in expression " + expr);
+ }
+ }
- // else
-
- if (expr is IUnknown) {
- return expr;
- }
- else
- {
- throw
- new System.NotImplementedException("cannot inline identifies in expression " + expr);
- }
- }
+ public override Element/*!*/ Constrain(Element/*!*/ element, IExpr/*!*/ expr) {
+ //Contract.Requires(expr != null);
+ //Contract.Requires(element != null);
+ //Contract.Ensures(Contract.Result<Element>() != null);
+ Elt/*!*/ result = (Elt)element;
+ Contract.Assert(result != null);
+ if (IsBottom(element)) {
+ return result; // == element
+ }
- public override Element/*!*/ Constrain(Element/*!*/ element, IExpr/*!*/ expr){
-Contract.Requires(expr != null);
-Contract.Requires(element != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- Elt/*!*/ result = (Elt)element;
- Contract.Assert(result != null);
+ expr = InlineVariables(result, expr, cce.NonNull(Set.Empty), new OnUnableToInline(IdentityVarToExpr));
- if(IsBottom(element))
- {
- return result; // == element
- }
+ foreach (IExpr/*!*/ conjunct in FindConjuncts(expr)) {
+ Contract.Assert(conjunct != null);
+ IVariable left, right;
- expr = InlineVariables(result, expr, cce.NonNull(Set.Empty), new OnUnableToInline(IdentityVarToExpr));
-
- foreach(IExpr/*!*/ conjunct in FindConjuncts(expr)){
-Contract.Assert(conjunct != null);
- IVariable left, right;
-
- if (IsSimpleEquality(conjunct, out left, out right))
- {
- #region The conjunct is a simple equality
-
-
- Contract.Assert(left != null && right != null);
-
- Element leftValue = result[left], rightValue = result[right];
- if (leftValue == null) { leftValue = this.microLattice.Top; }
- if (rightValue == null) { rightValue = this.microLattice.Top; }
- Element newValue = this.microLattice.Meet(leftValue, rightValue);
- result = AddConstraint(result, left, newValue);
- result = AddConstraint(result, right, newValue);
-
- #endregion
- }
- else
- {
- ISet/*<IVariable>*/ variablesInvolved = VariablesInExpression(conjunct, Set.Empty);
-
- if (variablesInvolved.Count == 1)
- {
- #region We have just one variable
-
- IVariable var = null;
- foreach (IVariable/*!*/ v in variablesInvolved) {Contract.Assert(v != null); var = v; } // why is there no better way to get the elements?
- Contract.Assert(var != null);
- Element/*!*/ value = this.microLattice.EvaluatePredicate(conjunct);
- result = AddConstraint(result, var, value);
-
- #endregion
- }
- else if(IsArithmeticExpr(conjunct) && this.microLattice.UnderstandsBasicArithmetics)
- {
- #region We evalaute an arithmetic expression
-
- IFunApp fun = (IFunApp) conjunct;
- if(fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
- {
- // get the variable to be assigned
- IExpr/*!*/ leftArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
- IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
- IExpr/*!*/ var = (leftArg is IVariable) ? leftArg : rightArg;
-
- Element/*!*/ value = this.microLattice.EvaluatePredicateWithState(conjunct, result.Constraints);
- Contract.Assert(value != null);
- result = AddConstraint(result, (IVariable/*!*/)cce.NonNull(var), value);
- }
- #endregion
- }
- }
- }
- return result;
- }
+ if (IsSimpleEquality(conjunct, out left, out right)) {
+ #region The conjunct is a simple equality
- public override Element/*!*/ Rename(Element/*!*/ element, IVariable/*!*/ oldName, IVariable/*!*/ newName){
-Contract.Requires(newName != null);
-Contract.Requires(oldName != null);
-Contract.Requires(element != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- if(IsBottom(element))
- {
- return element;
- }
- else
- {
- return ((Elt)element).Rename(oldName, newName, this.microLattice);
- }
+ Contract.Assert(left != null && right != null);
+
+ Element leftValue = result[left], rightValue = result[right];
+ if (leftValue == null) {
+ leftValue = this.microLattice.Top;
+ }
+ if (rightValue == null) {
+ rightValue = this.microLattice.Top;
+ }
+ Element newValue = this.microLattice.Meet(leftValue, rightValue);
+ result = AddConstraint(result, left, newValue);
+ result = AddConstraint(result, right, newValue);
+
+ #endregion
+ } else {
+ ISet/*<IVariable>*/ variablesInvolved = VariablesInExpression(conjunct, Set.Empty);
+
+ if (variablesInvolved.Count == 1) {
+ #region We have just one variable
+
+ IVariable var = null;
+ foreach (IVariable/*!*/ v in variablesInvolved) {
+ Contract.Assert(v != null);
+ var = v;
+ } // why is there no better way to get the elements?
+ Contract.Assert(var != null);
+ Element/*!*/ value = this.microLattice.EvaluatePredicate(conjunct);
+ result = AddConstraint(result, var, value);
+
+ #endregion
+ } else if (IsArithmeticExpr(conjunct) && this.microLattice.UnderstandsBasicArithmetics) {
+ #region We evalaute an arithmetic expression
+
+ IFunApp fun = (IFunApp)conjunct;
+ if (fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
+ {
+ // get the variable to be assigned
+ IExpr/*!*/ leftArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+ IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
+ IExpr/*!*/ var = (leftArg is IVariable) ? leftArg : rightArg;
+
+ Element/*!*/ value = this.microLattice.EvaluatePredicateWithState(conjunct, result.Constraints);
+ Contract.Assert(value != null);
+ result = AddConstraint(result, (IVariable/*!*/)cce.NonNull(var), value);
+ }
+ #endregion
+ }
}
+ }
+ return result;
+ }
- public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args){
-Contract.Requires(args != null);
-Contract.Requires(f != null);
- return f.Equals(Prop.And) ||
- f.Equals(Value.Eq) ||
- microLattice.Understands(f, args);
- }
+ public override Element/*!*/ Rename(Element/*!*/ element, IVariable/*!*/ oldName, IVariable/*!*/ newName) {
+ //Contract.Requires(newName != null);
+ //Contract.Requires(oldName != null);
+ //Contract.Requires(element != null);
+ //Contract.Ensures(Contract.Result<Element>() != null);
+ if (IsBottom(element)) {
+ return element;
+ } else {
+ return ((Elt)element).Rename(oldName, newName, this.microLattice);
+ }
+ }
- private sealed class EquivalentExprException :CheckedException { }
- private sealed class EquivalentExprInlineCallback
- {
- private readonly IVariable/*!*/ var;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(var != null);
- }
- public EquivalentExprInlineCallback(IVariable/*!*/ var){
-Contract.Requires(var != null);
- this.var = var;
- // base();
- }
+ public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) {
+ Contract.Requires(args != null);
+ Contract.Requires(f != null);
+ return f.Equals(Prop.And) ||
+ f.Equals(Value.Eq) ||
+ microLattice.Understands(f, args);
+ }
- public IExpr/*!*/ ThrowOnUnableToInline(IVariable/*!*/ othervar)
- //throws EquivalentExprException;
- {Contract.Requires(othervar != null);
- Contract.Ensures(Contract.Result<IExpr>() != null);
- Contract.EnsuresOnThrow<EquivalentExprException>(true);
- if (othervar.Equals(var))
- throw new EquivalentExprException();
- else
- return othervar;
- }
- }
+ private sealed class EquivalentExprException : CheckedException {
+ }
+ private sealed class EquivalentExprInlineCallback {
+ private readonly IVariable/*!*/ var;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(var != null);
+ }
- public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/*<IVariable!>*//*!*/ prohibitedVars){
-Contract.Requires(prohibitedVars != null);
-Contract.Requires(var != null);
-Contract.Requires(expr != null);
-Contract.Requires(q != null);
-Contract.Requires(e != null);
- try
- {
- EquivalentExprInlineCallback closure = new EquivalentExprInlineCallback(var);
- return InlineVariables((Elt)e, expr, cce.NonNull(Set.Empty),
- new OnUnableToInline(closure.ThrowOnUnableToInline));
- }
- catch (EquivalentExprException)
- {
- return null;
- }
- }
+ public EquivalentExprInlineCallback(IVariable/*!*/ var) {
+ Contract.Requires(var != null);
+ this.var = var;
+ // base();
+ }
+
+ public IExpr/*!*/ ThrowOnUnableToInline(IVariable/*!*/ othervar)
+ //throws EquivalentExprException;
+ {
+ Contract.Requires(othervar != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ Contract.EnsuresOnThrow<EquivalentExprException>(true);
+ if (othervar.Equals(var))
+ throw new EquivalentExprException();
+ else
+ return othervar;
+ }
+ }
+ public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/*<IVariable!>*//*!*/ prohibitedVars) {
+ //Contract.Requires(prohibitedVars != null);
+ //Contract.Requires(var != null);
+ //Contract.Requires(expr != null);
+ //Contract.Requires(q != null);
+ //Contract.Requires(e != null);
+ try {
+ EquivalentExprInlineCallback closure = new EquivalentExprInlineCallback(var);
+ return InlineVariables((Elt)e, expr, cce.NonNull(Set.Empty),
+ new OnUnableToInline(closure.ThrowOnUnableToInline));
+ } catch (EquivalentExprException) {
+ return null;
+ }
+ }
- /// <summary>
- /// Check to see if the given predicate holds in the given lattice element.
- ///
- /// TODO: We leave this unimplemented for now and just return maybe.
- /// </summary>
- /// <param name="e">The lattice element.</param>
- /// <param name="pred">The predicate.</param>
- /// <returns>Yes, No, or Maybe</returns>
- public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred){
-Contract.Requires(pred != null);
-Contract.Requires(e != null);
- return Answer.Maybe;
- }
- /// <summary>
- /// Answers a disequality about two variables. The same information could be obtained
- /// by asking CheckPredicate, but a different implementation may be simpler and more
- /// efficient.
- ///
- /// TODO: We leave this unimplemented for now and just return maybe.
- /// </summary>
- /// <param name="e">The lattice element.</param>
- /// <param name="var1">The first variable.</param>
- /// <param name="var2">The second variable.</param>
- /// <returns>Yes, No, or Maybe.</returns>
- public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2){
-Contract.Requires(var2 != null);
-Contract.Requires(var1 != null);
-Contract.Requires(e != null);
- return Answer.Maybe;
- }
+ /// <summary>
+ /// Check to see if the given predicate holds in the given lattice element.
+ ///
+ /// TODO: We leave this unimplemented for now and just return maybe.
+ /// </summary>
+ /// <param name="e">The lattice element.</param>
+ /// <param name="pred">The predicate.</param>
+ /// <returns>Yes, No, or Maybe</returns>
+ public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) {
+ //Contract.Requires(pred != null);
+ //Contract.Requires(e != null);
+ return Answer.Maybe;
+ }
- public override void Validate()
- {
- base.Validate();
- microLattice.Validate();
- }
+ /// <summary>
+ /// Answers a disequality about two variables. The same information could be obtained
+ /// by asking CheckPredicate, but a different implementation may be simpler and more
+ /// efficient.
+ ///
+ /// TODO: We leave this unimplemented for now and just return maybe.
+ /// </summary>
+ /// <param name="e">The lattice element.</param>
+ /// <param name="var1">The first variable.</param>
+ /// <param name="var2">The second variable.</param>
+ /// <returns>Yes, No, or Maybe.</returns>
+ public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) {
+ //Contract.Requires(var2 != null);
+ //Contract.Requires(var1 != null);
+ //Contract.Requires(e != null);
+ return Answer.Maybe;
+ }
+ public override void Validate() {
+ base.Validate();
+ microLattice.Validate();
}
+
+ }
}
|