From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- .../AIFramework/VariableMap/ConstantExpressions.cs | 1056 ++++++++++---------- 1 file changed, 528 insertions(+), 528 deletions(-) (limited to 'Source/AIFramework/VariableMap/ConstantExpressions.cs') diff --git a/Source/AIFramework/VariableMap/ConstantExpressions.cs b/Source/AIFramework/VariableMap/ConstantExpressions.cs index fcf49b25..185c700e 100644 --- a/Source/AIFramework/VariableMap/ConstantExpressions.cs +++ b/Source/AIFramework/VariableMap/ConstantExpressions.cs @@ -1,538 +1,538 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- - - ///////////////////////////////////////////////////////////////////////////////// - // The Abstract domain for determining "constant" expressions - // i.e. It determines which expression are statically binded - ///////////////////////////////////////////////////////////////////////////////// -/* -using System; - -namespace Microsoft.AbstractInterpretationFramework -{ - using Microsoft.Contracts; - using System.Collections.Generic; - using Microsoft.AbstractInterpretationFramework; - - /// - /// This is an abstract domain for inferring constant expressions - /// - - public class ConstantExpressions : Lattice - { - /// - /// An abstract element is made of two maps: - /// + A map from variables to expressions \cup top ( i.e. for each variable, the expression it is binded ) - /// + A map from variables to set of variabes ( i.e. for each variable, the set of variables that depends on its value ) - /// - private class AbstractElement: Element - { - private Dictionary variableBindings; - private Dictionary> variableDependences; - - static private AbstractElement! bottom; - static public Element! Bottom - { - get - { - if(bottom == null) - { - bottom = new AbstractElement(); - bottom.variableBindings = null; - bottom.variableDependences = null; - } - assert bottom.variableBindings == null && bottom.variableDependences == null; - return bottom; - } - } - - static public Element! Top - { - get - { - return new AbstractElement(); - } - } - - AbstractElement() - { - this.variableBindings = new Dictionary(); - this.variableDependences = new Dictionary>(); - } - - /// - /// Our abstract element is top if and only if it has any constraint on variables - /// - public bool IsTop - { - get - { - return this.variableBindings.Keys.Count == 0 && this.variableDependences.Keys.Count == 0; - } - } - - /// - /// Our abstract element is bottom if and only if the maps are null - /// - public bool IsBottom - { - get - { - assert (this.variableBindings == null) <==> (this.variableDependences == null); +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- + + ///////////////////////////////////////////////////////////////////////////////// + // The Abstract domain for determining "constant" expressions + // i.e. It determines which expression are statically binded + ///////////////////////////////////////////////////////////////////////////////// +/* +using System; + +namespace Microsoft.AbstractInterpretationFramework +{ + using Microsoft.Contracts; + using System.Collections.Generic; + using Microsoft.AbstractInterpretationFramework; + + /// + /// This is an abstract domain for inferring constant expressions + /// + + public class ConstantExpressions : Lattice + { + /// + /// An abstract element is made of two maps: + /// + A map from variables to expressions \cup top ( i.e. for each variable, the expression it is binded ) + /// + A map from variables to set of variabes ( i.e. for each variable, the set of variables that depends on its value ) + /// + private class AbstractElement: Element + { + private Dictionary variableBindings; + private Dictionary> variableDependences; + + static private AbstractElement! bottom; + static public Element! Bottom + { + get + { + if(bottom == null) + { + bottom = new AbstractElement(); + bottom.variableBindings = null; + bottom.variableDependences = null; + } + assert bottom.variableBindings == null && bottom.variableDependences == null; + return bottom; + } + } + + static public Element! Top + { + get + { + return new AbstractElement(); + } + } + + AbstractElement() + { + this.variableBindings = new Dictionary(); + this.variableDependences = new Dictionary>(); + } + + /// + /// Our abstract element is top if and only if it has any constraint on variables + /// + public bool IsTop + { + get + { + return this.variableBindings.Keys.Count == 0 && this.variableDependences.Keys.Count == 0; + } + } + + /// + /// Our abstract element is bottom if and only if the maps are null + /// + public bool IsBottom + { + get + { + assert (this.variableBindings == null) <==> (this.variableDependences == null); return this.variableBindings == null && this.variableDependences == null; - } - } - - /// - /// The pointwise join... - /// - public static AbstractElement! Join(AbstractElement! left, AbstractElement! right) - { + } + } + + /// + /// The pointwise join... + /// + public static AbstractElement! Join(AbstractElement! left, AbstractElement! right) + { AbstractElement! result = new AbstractElement(); - - // Put all the variables in the left - foreach(IVariable! var in left.variableBindings.Keys) - { - BindExpr leftVal = left.variableBindings[var]; - assert leftVal != null; - - BindExpr rightVal = right.variableBindings[var]; - - if(rightVal== null) // the expression is not there - { + + // Put all the variables in the left + foreach(IVariable! var in left.variableBindings.Keys) + { + BindExpr leftVal = left.variableBindings[var]; + assert leftVal != null; + + BindExpr rightVal = right.variableBindings[var]; + + if(rightVal== null) // the expression is not there + { result.variableBindings.Add(var, leftVal); - } - else // both abstract elements have a definition for the variable.... - { - result.variableBindings.Add(var, BindExpr.Join(leftVal, rightVal)); - } - } - - // Put all the variables in the right - foreach(IVariable! var in right.variableBindings.Keys) - { - BindExpr rightVal = right.variableBindings[var]; - assert rightVal != null; - - BindExpr leftVal = left.variableBindings[var]; - - if(rightVal== null) // the expression is not there - { + } + else // both abstract elements have a definition for the variable.... + { + result.variableBindings.Add(var, BindExpr.Join(leftVal, rightVal)); + } + } + + // Put all the variables in the right + foreach(IVariable! var in right.variableBindings.Keys) + { + BindExpr rightVal = right.variableBindings[var]; + assert rightVal != null; + + BindExpr leftVal = left.variableBindings[var]; + + if(rightVal== null) // the expression is not there + { result.variableBindings.Add(var, rightVal); - } - else // both abstract elements have a definition for the variable.... - { - result.variableBindings.Add(var, BindExpr.Join(rightVal, leftVal)); - } - } - - // Join the dependencies... - foreach(IVariable! var in left.variableDependences.Keys) - { - List dependencies = left.variableDependences[var]; - List dup = new List(dependencies); - - result.variableDependences.Add(var, dup); - } - - foreach(IVariable! var in right.variableDependences.Keys) - { - if(result.variableDependences.ContainsKey(var)) - { - List dependencies = result.variableDependences[var]; - dependencies.AddRange(right.variableDependences[var]); - } - else - { - List dependencies = right.variableDependences[var]; - List dup = new List(dependencies); - - result.variableDependences.Add(var, dup); - } - } - - // Normalize... i.e. for the variables such thas they point to an unknown expression (top) we have to update also their values - result.Normalize(); - - return result; - } - - - /// - /// Normalize the current abstract element, in that it propagetes the "dynamic" information throughtout the abstract element - /// - public void Normalize() - { - if(this.IsBottom) - return; - if(this.IsTop) - return; - assert this.variableBindings != null; - - bool atFixpoint = false; - - while(!atFixpoint) - { - atFixpoint = true; // guess that we've got the fixpoint... - - foreach(IVariable x in this.variableBindings.Keys) - { - if(this.variableBindings[x].IsTop) // It means that the variable is tied to a dynamic expression - { - foreach(IVariable y in this.variableDependences[x]) // The all the variables that depend on x are also dynamic... - { - assert x != y; // A variable cannot depend on itself... - if(!this.variableBindings[y].IsTop) - { - this.variableBindings[y] = BindExpr.Top; - atFixpoint = false; // the assumption that we were at the fixpoint was false, we have still to propagate some information... - } - } - } - } - } - } - - /// - /// The pointwise meet... - /// - public static AbstractElement! Meet(AbstractElement! left, AbstractElement! right) - { - AbstractElement! result = new AbstractElement(); - - // Put the variables that are both in left and right - foreach(IVariable var in left.variableBindings.Keys) - { - if(right.variableBindings.ContainsKey(var)) - { - result.variableBindings.Add(var, BindExpr.Meet(left.variableBindings[var], right.variableBindings[var])); - } - } - - // Intersect the dependencies - foreach(IVariable var in result.variableBindings.Keys) - { - List depLeft = left.variableDependences[var]; - List depRight = right.variableDependences[var]; - - // Intersect the two sets + } + else // both abstract elements have a definition for the variable.... + { + result.variableBindings.Add(var, BindExpr.Join(rightVal, leftVal)); + } + } + + // Join the dependencies... + foreach(IVariable! var in left.variableDependences.Keys) + { + List dependencies = left.variableDependences[var]; + List dup = new List(dependencies); + + result.variableDependences.Add(var, dup); + } + + foreach(IVariable! var in right.variableDependences.Keys) + { + if(result.variableDependences.ContainsKey(var)) + { + List dependencies = result.variableDependences[var]; + dependencies.AddRange(right.variableDependences[var]); + } + else + { + List dependencies = right.variableDependences[var]; + List dup = new List(dependencies); + + result.variableDependences.Add(var, dup); + } + } + + // Normalize... i.e. for the variables such thas they point to an unknown expression (top) we have to update also their values + result.Normalize(); + + return result; + } + + + /// + /// Normalize the current abstract element, in that it propagetes the "dynamic" information throughtout the abstract element + /// + public void Normalize() + { + if(this.IsBottom) + return; + if(this.IsTop) + return; + assert this.variableBindings != null; + + bool atFixpoint = false; + + while(!atFixpoint) + { + atFixpoint = true; // guess that we've got the fixpoint... + + foreach(IVariable x in this.variableBindings.Keys) + { + if(this.variableBindings[x].IsTop) // It means that the variable is tied to a dynamic expression + { + foreach(IVariable y in this.variableDependences[x]) // The all the variables that depend on x are also dynamic... + { + assert x != y; // A variable cannot depend on itself... + if(!this.variableBindings[y].IsTop) + { + this.variableBindings[y] = BindExpr.Top; + atFixpoint = false; // the assumption that we were at the fixpoint was false, we have still to propagate some information... + } + } + } + } + } + } + + /// + /// The pointwise meet... + /// + public static AbstractElement! Meet(AbstractElement! left, AbstractElement! right) + { + AbstractElement! result = new AbstractElement(); + + // Put the variables that are both in left and right + foreach(IVariable var in left.variableBindings.Keys) + { + if(right.variableBindings.ContainsKey(var)) + { + result.variableBindings.Add(var, BindExpr.Meet(left.variableBindings[var], right.variableBindings[var])); + } + } + + // Intersect the dependencies + foreach(IVariable var in result.variableBindings.Keys) + { + List depLeft = left.variableDependences[var]; + List depRight = right.variableDependences[var]; + + // Intersect the two sets result.variableDependences.Add(var, depLeft); - foreach(IVariable v in depRight) - { - if(!result.variableDependences.ContainsKey(v)) - { + foreach(IVariable v in depRight) + { + if(!result.variableDependences.ContainsKey(v)) + { result.variableDependences.Remove(v); - } - } - } - - // Now we remove the dependencies with variables not in variableBindings + } + } + } + + // Now we remove the dependencies with variables not in variableBindings List! varsToRemove = new List(); - - foreach(IVariable var in result. - - - } - - /// - /// Clone the current abstract element - /// - public override Element! Clone() - { - AbstractElement cloned = new AbstractElement(); - foreach(IVariable var in this.variableBindings.Keys) - { - cloned.variableBindings.Add(var, this.variableBindings[var]); - } - - foreach(IVariable var in this.variableDependences.Keys) - { - List dependingVars = this.variableDependences[var]; - List clonedDependingVars = new List(dependingVars); + + foreach(IVariable var in result. + + + } + + /// + /// Clone the current abstract element + /// + public override Element! Clone() + { + AbstractElement cloned = new AbstractElement(); + foreach(IVariable var in this.variableBindings.Keys) + { + cloned.variableBindings.Add(var, this.variableBindings[var]); + } + + foreach(IVariable var in this.variableDependences.Keys) + { + List dependingVars = this.variableDependences[var]; + List clonedDependingVars = new List(dependingVars); cloned.variableDependences.Add(var, clonedDependingVars); - } - } - - /// - /// Return the variables that have a binding - /// - public override ICollection! FreeVariables() - { - List vars = new List(this.variableBindings.Keys); - - return vars; - } - - public override string! ToString() - { + } + } + + /// + /// Return the variables that have a binding + /// + public override ICollection! FreeVariables() + { + List vars = new List(this.variableBindings.Keys); + + return vars; + } + + public override string! ToString() + { string! retString = ""; - retString += "Bindings"; - - foreach(IVariable var in this.variableBindings.Keys) - { - string! toAdd = var.ToString() + " -> " + this.variableBindings[var]; - retString += toAdd + ","; - } - - retString += "\nDependencies"; - foreach(IVariable var in this.variableDependences.Keys) - { - string! toAdd = var.ToString() + " -> " + this.variableDependences[var]; - retString += toAdd + ","; - } - - return retString; - } - } - - public override Element! Top - { - get - { - return AbstractElement.Top; - } - } - - public override Element! Bottom - { - get - { - return AbstractElement.Bottom; - } - } - - public override bool IsTop(Element! e) - { - assert e is AbstractElement; - AbstractElement! absElement = (AbstractElement) e; - - return absElement.IsTop; - } - - public override bool IsBottom(Element! e) - { - assert e is AbstractElement; - AbstractElement absElement = (AbstractElement) e; - return absElement.IsBottom; - } - - /// - /// Perform the pointwise join of the two abstract elements - /// - public override Element! NontrivialJoin(Element! a, Element! b) - { - assert a is AbstractElement; - assert b is AbstractElement; - - AbstractElement! left = (AbstractElement!) a; - AbstractElement! right = (AbstractElement!) b; - - return AbstractElement.Join(left, right); - } - - /// - /// Perform the pointwise meet of two abstract elements - /// - public override Element! NontrivialMeet(Element! a, Element!b) - { - assert a is AbstractElement; - assert b is AbstractElement; - - AbstractElement! left = (AbstractElement!) a; - AbstractElement! right = (AbstractElement!) b; - - return AbstractElement.Meet(left, right); - } - - - } - - /// - /// A wrapper in order to have the algebraic datatype BindExpr := IExpr | Top - /// - abstract class BindExpr - { - /// - /// True iff this expression is instance of BindExprTop - /// - public bool IsTop - { - get - { - return this is BindExprTop; - } - } - - static public BindExpr Top - { - get - { - return BindExprTop.UniqueTop; - } - } - - /// - /// True iff this expression is instance of BindExprBottom - /// - public bool IsBottom - { - get - { - return this is BindExprBottom; - } - } - - static public BindExpr Bottom - { - get - { - return BindExprBottom.UniqueBottom; - } - } - - public static BindExpr! Join(BindExpr! left, BindExpr! right) - { - if(left.IsTop || right.IsTop) - { - return BindExpr.Top; - } - else if(left.IsBottom) - { - return right; - } - else if(right.IsBottom) - { - return left; - } - else if(left.EmbeddedExpr != right.EmbeddedExpr) - { - return BindExpr.Top; - } - else // left.EmbeddedExpr == right.EmbeddedExpr - { - return left; - } - } - - public static BindExpr! Meet(BindExpr! left, BindExpr! right) - { - if(left.IsTop) - { - return right; - } - else if(right.IsTop) - { - return right; - } - else if(left.IsBottom || right.IsBottom) - { - return BindExpr.Bottom; - } - else if(left.EmbeddedExpr != right.EmbeddedExpr) - { - return BindExpr.Bottom; - } - else // left.EmbeddedExpr == right.EmbeddedExpr - { - return left; - } - } - - abstract public IExpr! EmbeddedExpr - { - get; - } - - } - - /// - /// A wrapper for an integer - /// - class Expr : BindExpr - { - private IExpr! exp; - - public Expr(IExpr! exp) - { - this.exp = exp; - } - - override public IExpr! EmbeddedExpr - { - get - { - return this.exp; - } - } - - public override string! ToString() - { - return this.exp.ToString(); - } - } - - /// - /// The dynamic expression - /// - class BindExprTop : BindExpr - { - private BindExprTop top = new BindExprTop(); - static public BindExprTop! UniqueTop - { - get - { - return this.top; - } - } - - private BindExprTop() {} - - override public IExpr! EmbeddedExpr - { - get - { - assert false; // If we get there, we have an error - } - } - - public override string! ToString() - { - return ""; - } - } - - /// - /// The unreachable expression - /// - class BindExprBottom : BindExpr - { - private BindExprBottom! bottom = new BindExprBottom(); - static public BindExprBottom! UniqueBottom - { - get - { - return this.bottom; - } - } - - private BindExprBottom() {} - - override public IExpr! EmbeddedExpr - { - get - { - assert false; - } - } - - public override string! ToString() - { - return ""; - } - } - -} // end namespace Microsoft.AbstractInterpretationFramework + retString += "Bindings"; + + foreach(IVariable var in this.variableBindings.Keys) + { + string! toAdd = var.ToString() + " -> " + this.variableBindings[var]; + retString += toAdd + ","; + } + + retString += "\nDependencies"; + foreach(IVariable var in this.variableDependences.Keys) + { + string! toAdd = var.ToString() + " -> " + this.variableDependences[var]; + retString += toAdd + ","; + } + + return retString; + } + } + + public override Element! Top + { + get + { + return AbstractElement.Top; + } + } + + public override Element! Bottom + { + get + { + return AbstractElement.Bottom; + } + } + + public override bool IsTop(Element! e) + { + assert e is AbstractElement; + AbstractElement! absElement = (AbstractElement) e; + + return absElement.IsTop; + } + + public override bool IsBottom(Element! e) + { + assert e is AbstractElement; + AbstractElement absElement = (AbstractElement) e; + return absElement.IsBottom; + } + + /// + /// Perform the pointwise join of the two abstract elements + /// + public override Element! NontrivialJoin(Element! a, Element! b) + { + assert a is AbstractElement; + assert b is AbstractElement; + + AbstractElement! left = (AbstractElement!) a; + AbstractElement! right = (AbstractElement!) b; + + return AbstractElement.Join(left, right); + } + + /// + /// Perform the pointwise meet of two abstract elements + /// + public override Element! NontrivialMeet(Element! a, Element!b) + { + assert a is AbstractElement; + assert b is AbstractElement; + + AbstractElement! left = (AbstractElement!) a; + AbstractElement! right = (AbstractElement!) b; + + return AbstractElement.Meet(left, right); + } + + + } + + /// + /// A wrapper in order to have the algebraic datatype BindExpr := IExpr | Top + /// + abstract class BindExpr + { + /// + /// True iff this expression is instance of BindExprTop + /// + public bool IsTop + { + get + { + return this is BindExprTop; + } + } + + static public BindExpr Top + { + get + { + return BindExprTop.UniqueTop; + } + } + + /// + /// True iff this expression is instance of BindExprBottom + /// + public bool IsBottom + { + get + { + return this is BindExprBottom; + } + } + + static public BindExpr Bottom + { + get + { + return BindExprBottom.UniqueBottom; + } + } + + public static BindExpr! Join(BindExpr! left, BindExpr! right) + { + if(left.IsTop || right.IsTop) + { + return BindExpr.Top; + } + else if(left.IsBottom) + { + return right; + } + else if(right.IsBottom) + { + return left; + } + else if(left.EmbeddedExpr != right.EmbeddedExpr) + { + return BindExpr.Top; + } + else // left.EmbeddedExpr == right.EmbeddedExpr + { + return left; + } + } + + public static BindExpr! Meet(BindExpr! left, BindExpr! right) + { + if(left.IsTop) + { + return right; + } + else if(right.IsTop) + { + return right; + } + else if(left.IsBottom || right.IsBottom) + { + return BindExpr.Bottom; + } + else if(left.EmbeddedExpr != right.EmbeddedExpr) + { + return BindExpr.Bottom; + } + else // left.EmbeddedExpr == right.EmbeddedExpr + { + return left; + } + } + + abstract public IExpr! EmbeddedExpr + { + get; + } + + } + + /// + /// A wrapper for an integer + /// + class Expr : BindExpr + { + private IExpr! exp; + + public Expr(IExpr! exp) + { + this.exp = exp; + } + + override public IExpr! EmbeddedExpr + { + get + { + return this.exp; + } + } + + public override string! ToString() + { + return this.exp.ToString(); + } + } + + /// + /// The dynamic expression + /// + class BindExprTop : BindExpr + { + private BindExprTop top = new BindExprTop(); + static public BindExprTop! UniqueTop + { + get + { + return this.top; + } + } + + private BindExprTop() {} + + override public IExpr! EmbeddedExpr + { + get + { + assert false; // If we get there, we have an error + } + } + + public override string! ToString() + { + return ""; + } + } + + /// + /// The unreachable expression + /// + class BindExprBottom : BindExpr + { + private BindExprBottom! bottom = new BindExprBottom(); + static public BindExprBottom! UniqueBottom + { + get + { + return this.bottom; + } + } + + private BindExprBottom() {} + + override public IExpr! EmbeddedExpr + { + get + { + assert false; + } + } + + public override string! ToString() + { + return ""; + } + } + +} // end namespace Microsoft.AbstractInterpretationFramework */ \ No newline at end of file -- cgit v1.2.3