diff options
25 files changed, 205 insertions, 223 deletions
diff --git a/Source/AIFramework/CommonFunctionSymbols.ssc b/Source/AIFramework/CommonFunctionSymbols.ssc index 4e38fbcb..f014e963 100644 --- a/Source/AIFramework/CommonFunctionSymbols.ssc +++ b/Source/AIFramework/CommonFunctionSymbols.ssc @@ -30,11 +30,10 @@ namespace Microsoft.AbstractInterpretationFramework // base();
}
-// public AIType! AIType { [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return typ; } }
- public AIType! AIType { [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return typ; } }
+ public AIType! AIType { get { return typ; } }
[NoDefaultContract]
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return display;
@@ -65,7 +64,7 @@ namespace Microsoft.AbstractInterpretationFramework return isym != null && isym.Value.Equals(this.Value);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override int GetHashCode()
{
return Value.GetHashCode();
@@ -97,7 +96,7 @@ namespace Microsoft.AbstractInterpretationFramework return isym != null && isym.Value == this.Value && isym.Bits == this.Bits;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override int GetHashCode()
{
unchecked {
@@ -126,7 +125,7 @@ namespace Microsoft.AbstractInterpretationFramework return dsym != null && dsym.Value == this.Value;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override int GetHashCode()
{
return Value.GetHashCode();
@@ -155,7 +154,7 @@ namespace Microsoft.AbstractInterpretationFramework }
[NoDefaultContract]
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override int GetHashCode()
{
return Value.GetHashCode();
@@ -898,19 +897,19 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// Returns true iff "t" denotes a type constant.
/// </summary>
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
bool IsTypeConstant(IExpr! t);
/// <summary>
/// Returns true iff t0 and t1 are types such that t0 and t1 are equal.
/// </summary>
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
bool IsTypeEqual(IExpr! t0, IExpr! t1);
/// <summary>
/// Returns true iff t0 and t1 are types such that t0 is a subtype of t1.
/// </summary>
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
bool IsSubType(IExpr! t0, IExpr! t1);
/// <summary>
diff --git a/Source/AIFramework/Expr.ssc b/Source/AIFramework/Expr.ssc index 94dc4dc7..42621239 100644 --- a/Source/AIFramework/Expr.ssc +++ b/Source/AIFramework/Expr.ssc @@ -35,7 +35,7 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
/// <param name="visitor">The expression visitor.</param>
/// <returns>The result of the visit.</returns>
- [Pure][Reads(ReadsAttribute.Reads.Owned)] object DoVisit(ExprVisitor! visitor);
+ [Pure] object DoVisit(ExprVisitor! visitor);
// TODO: Type checking of the expressions.
}
@@ -57,10 +57,10 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
public interface IFunApp : IExpr
{
- IFunctionSymbol! FunctionSymbol { [Pure][Reads(ReadsAttribute.Reads.Owned)] get; }
+ IFunctionSymbol! FunctionSymbol { get; }
IList/*<IExpr!>*/! Arguments
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)][Rep] get
+ [Pure][Rep] get
ensures result.IsReadOnly;
;
}
@@ -82,9 +82,9 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
public interface IFunction : IExpr
{
- IVariable! Param { [Pure][Reads(ReadsAttribute.Reads.Owned)] get; }
- AIType! ParamType { [Pure][Reads(ReadsAttribute.Reads.Owned)] get; }
- IExpr! Body { [Pure][Reads(ReadsAttribute.Reads.Owned)] get; }
+ IVariable! Param { get; }
+ AIType! ParamType { get; }
+ IExpr! Body { get; }
IFunction! CloneWithBody(IExpr! body);
}
@@ -307,7 +307,7 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
public interface IFunctionSymbol
{
- AIType! AIType { [Pure][Reads(ReadsAttribute.Reads.Owned)][Rep][ResultNotNewlyAllocated]
+ AIType! AIType { [Rep][ResultNotNewlyAllocated]
get; }
}
@@ -354,7 +354,7 @@ namespace Microsoft.AbstractInterpretationFramework public IList/*<AIType!>*/! Arguments
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)][Rep]
+ [Pure][Rep]
get
ensures result.IsReadOnly;
{
@@ -364,12 +364,12 @@ namespace Microsoft.AbstractInterpretationFramework public int Arity
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return argTypes.Count; }
+ get { return argTypes.Count; }
}
public AIType! ReturnType
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return retType; }
+ get { return retType; }
}
/* TODO Do we have the invariant that two functions are equal iff they're the same object.
diff --git a/Source/AIFramework/Functional.ssc b/Source/AIFramework/Functional.ssc index 4c4a5791..1413230e 100644 --- a/Source/AIFramework/Functional.ssc +++ b/Source/AIFramework/Functional.ssc @@ -28,7 +28,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections /// <returns>true if the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" /> contains an element with the key; otherwise, false.</returns>
/// <param name="key">The key to locate in the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />. </param>
/// <filterpriority>2</filterpriority>
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
bool Contains(object! key);
/// <summary>Returns an <see cref="T:System.Collections.IDictionaryEnumerator" /> for the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>
@@ -106,7 +106,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections return new FunctionalHashtable(r);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public bool Contains(object! key)
{
return h.Contains(key);
diff --git a/Source/AIFramework/Lattice.ssc b/Source/AIFramework/Lattice.ssc index 2b606492..2ecc49f8 100644 --- a/Source/AIFramework/Lattice.ssc +++ b/Source/AIFramework/Lattice.ssc @@ -576,7 +576,7 @@ namespace Microsoft.AbstractInterpretationFramework return lattice.ToString(e);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return string.Format(
diff --git a/Source/AIFramework/MultiLattice.ssc b/Source/AIFramework/MultiLattice.ssc index b6b6ba5e..761f4c7e 100644 --- a/Source/AIFramework/MultiLattice.ssc +++ b/Source/AIFramework/MultiLattice.ssc @@ -48,7 +48,7 @@ namespace Microsoft.AbstractInterpretationFramework return new Elt(this);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
// string s = "MultiLattice+Elt{";
@@ -83,7 +83,7 @@ namespace Microsoft.AbstractInterpretationFramework }
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override ICollection<IVariable!>! FreeVariables()
{
List<IVariable!>! list = new List<IVariable!>();
@@ -522,7 +522,6 @@ namespace Microsoft.AbstractInterpretationFramework public object Current
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
get
{
return this.Entry;
diff --git a/Source/AIFramework/Mutable.ssc b/Source/AIFramework/Mutable.ssc index 894359ef..36bb3647 100644 --- a/Source/AIFramework/Mutable.ssc +++ b/Source/AIFramework/Mutable.ssc @@ -18,10 +18,9 @@ namespace Microsoft.AbstractInterpretationFramework.Collections // Without it, the contract inheritance rules will complain since it
// has nowhere to attach the out-of-band contract it gets from
// ICollection.Count that it gets from IWorkList.
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
public override int Count { get { return base.Count; } }
- [Pure][Reads(ReadsAttribute.Reads.Owned)] public bool IsEmpty()
+ [Pure] public bool IsEmpty()
{
return Count == 0;
}
diff --git a/Source/AIFramework/Polyhedra/LinearConstraint.ssc b/Source/AIFramework/Polyhedra/LinearConstraint.ssc index 9ce1552b..087c3696 100644 --- a/Source/AIFramework/Polyhedra/LinearConstraint.ssc +++ b/Source/AIFramework/Polyhedra/LinearConstraint.ssc @@ -36,7 +36,7 @@ namespace Microsoft.AbstractInterpretationFramework Relation = rel;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
string s = null;
@@ -501,7 +501,7 @@ namespace Microsoft.AbstractInterpretationFramework terms.Add(dimension, value);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
string s = null;
diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc b/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc index b4e33a28..a99a4ee8 100644 --- a/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc +++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc @@ -172,7 +172,7 @@ namespace Microsoft.AbstractInterpretationFramework return Constraints != null && Constraints.Count == 0;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
if (Constraints == null)
@@ -1055,12 +1055,12 @@ namespace Microsoft.AbstractInterpretationFramework id = count;
count++;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return "lambda" + id;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public object DoVisit(ExprVisitor! visitor)
{
return visitor.VisitVariable(this);
@@ -1697,7 +1697,7 @@ namespace Microsoft.AbstractInterpretationFramework public TestVariable(string! name) {
this.name = name;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public object DoVisit(ExprVisitor! visitor) {
return visitor.VisitVariable(this);
}
diff --git a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc index bcf9c64d..fdb8d86d 100644 --- a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc +++ b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc @@ -43,7 +43,7 @@ namespace Microsoft.AbstractInterpretationFramework }
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return lcs.ToString();
@@ -54,7 +54,7 @@ namespace Microsoft.AbstractInterpretationFramework lcs.Dump();
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override ICollection<IVariable!>! FreeVariables()
{
return lcs.FreeVariables();
@@ -258,14 +258,14 @@ namespace Microsoft.AbstractInterpretationFramework // base();
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)] public object DoVisit(ExprVisitor! visitor) {
+ [Pure] public object DoVisit(ExprVisitor! visitor) {
return visitor.VisitFunApp(this);
}
- public IFunctionSymbol! FunctionSymbol { [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return Prop.Not; } }
+ public IFunctionSymbol! FunctionSymbol { get { return Prop.Not; } }
public IList/*<IExpr!>*/! Arguments {
- [Pure][Reads(ReadsAttribute.Reads.Owned)] get {
+ get {
IExpr[] args = new IExpr[] { arg };
return ArrayList.ReadOnly(args);
}
diff --git a/Source/AIFramework/VariableMap/ConstantAbstraction.ssc b/Source/AIFramework/VariableMap/ConstantAbstraction.ssc index 7b7fd87e..97fb57ce 100644 --- a/Source/AIFramework/VariableMap/ConstantAbstraction.ssc +++ b/Source/AIFramework/VariableMap/ConstantAbstraction.ssc @@ -31,7 +31,7 @@ namespace Microsoft.AbstractInterpretationFramework public BigNum Constant { get { return this.constantValue; } } // only when IsConstant
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
{
return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
diff --git a/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc b/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc index b9d1a7a4..8161cb3e 100644 --- a/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc +++ b/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc @@ -114,7 +114,7 @@ namespace Microsoft.AbstractInterpretationFramework }
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
{
return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
diff --git a/Source/AIFramework/VariableMap/Intervals.ssc b/Source/AIFramework/VariableMap/Intervals.ssc index 721b175d..7f6211ba 100644 --- a/Source/AIFramework/VariableMap/Intervals.ssc +++ b/Source/AIFramework/VariableMap/Intervals.ssc @@ -466,13 +466,13 @@ namespace Microsoft.AbstractInterpretationFramework */
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
{
return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return "[" + this.inf + ", " + this.sup + "]";
@@ -704,7 +704,7 @@ namespace Microsoft.AbstractInterpretationFramework this.val = i;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return this.Value.ToString();
@@ -746,7 +746,7 @@ namespace Microsoft.AbstractInterpretationFramework class PlusInfinity : InfinitaryInt
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return "+oo";
@@ -768,7 +768,7 @@ namespace Microsoft.AbstractInterpretationFramework class MinusInfinity : InfinitaryInt
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return "-oo";
diff --git a/Source/AIFramework/VariableMap/Nullness.ssc b/Source/AIFramework/VariableMap/Nullness.ssc index 63d637ce..bbd1da70 100644 --- a/Source/AIFramework/VariableMap/Nullness.ssc +++ b/Source/AIFramework/VariableMap/Nullness.ssc @@ -27,7 +27,7 @@ namespace Microsoft.AbstractInterpretationFramework public Elt (Value v) { this.value = v; }
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
{
return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.ssc b/Source/AIFramework/VariableMap/VariableMapLattice.ssc index aa15f1e6..34f876f5 100644 --- a/Source/AIFramework/VariableMap/VariableMapLattice.ssc +++ b/Source/AIFramework/VariableMap/VariableMapLattice.ssc @@ -51,6 +51,22 @@ namespace Microsoft.AbstractInterpretationFramework {
return new Elt(this.constraints);
}
+
+ [Pure]
+ public override string! ToString()
+ {
+ if (constraints == null) {
+ return "<bottom>";
+ }
+ string s = "[";
+ string sep = "";
+ foreach (IVariable! v in (!)constraints.Keys) {
+ 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);
@@ -61,7 +77,6 @@ namespace Microsoft.AbstractInterpretationFramework }
public bool IsBottom {
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
get {
return this.constraints == null;
}
@@ -158,7 +173,7 @@ namespace Microsoft.AbstractInterpretationFramework return new Elt(newMap);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override ICollection<IVariable!>! FreeVariables()
{
throw new System.NotImplementedException();
diff --git a/Source/AbsInt/AbstractInterpretation.ssc b/Source/AbsInt/AbstractInterpretation.ssc index eee25a09..ee5a1f06 100644 --- a/Source/AbsInt/AbstractInterpretation.ssc +++ b/Source/AbsInt/AbstractInterpretation.ssc @@ -55,7 +55,6 @@ namespace Microsoft.Boogie.AbstractInterpretation this.lattice = lattice;
this.procWorkItems = new Queue<ProcedureWorkItem!>();
this.callReturnWorkItems = new Queue();
- // base();
}
private Cci.IGraphNavigator ComputeCallGraph (Program! program)
@@ -198,17 +197,17 @@ namespace Microsoft.Boogie.AbstractInterpretation // where the notation i' means a variable with the same (string) name as i,
// but a different identity.
- AI.Lattice.Element! releventToCall = knownAtCallSite;
+ AI.Lattice.Element! relevantToCall = knownAtCallSite;
for (int i=0; i<proc.InParams.Length; i++)
{
// "Assign" the actual expressions to the corresponding formal variables.
assume proc.InParams[i] != null; //PM: this can be fixed once VariableSeq is replaced by List<Variable!>;
assume call.Ins[i] != null; //PM: this can be fixed once VariableSeq is replaced by List<Variable!>;
Expr equality = Expr.Eq(Expr.Ident( (!) proc.InParams[i]), (!) call.Ins[i]);
- releventToCall = lattice.Constrain(releventToCall, equality.IExpr);
+ relevantToCall = lattice.Constrain(relevantToCall, equality.IExpr);
}
foreach (Variable! var in caller.LocVars) {
- releventToCall = this.lattice.Eliminate(releventToCall, var);
+ relevantToCall = this.lattice.Eliminate(relevantToCall, var);
}
ProcedureSummary! summary = proc.Summary;
@@ -218,7 +217,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
ProcedureSummaryEntry! current = (!) summary[i];
- if (lattice.Equivalent(current.OnEntry, releventToCall))
+ if (lattice.Equivalent(current.OnEntry, relevantToCall))
{
applicableEntry = current;
break;
@@ -228,7 +227,7 @@ namespace Microsoft.Boogie.AbstractInterpretation // Not found in current map, so add new entry.
if (applicableEntry == null)
{
- ProcedureWorkItem! newWorkItem = new ProcedureWorkItem(proc, releventToCall, lattice);
+ ProcedureWorkItem! newWorkItem = new ProcedureWorkItem(proc, relevantToCall, lattice);
this.procWorkItems.Enqueue(newWorkItem);
applicableEntry = (!) proc.Summary[newWorkItem.Index];
}
@@ -351,48 +350,8 @@ namespace Microsoft.Boogie.AbstractInterpretation {
// process each procedure implementation by recursively processing the first (entry) block...
((!)impl.Blocks[0]).Lattice = lattice;
- ComputeBlockInvariants(impl, (!) impl.Blocks[0], summaryEntry.OnEntry);
-
- if (!CommandLineOptions.Clo.IntraproceduralInfer)
- {
- // compute the procedure invariant by joining all terminal block invariants...
- AI.Lattice.Element post = lattice.Bottom;
- foreach (Block block in impl.Blocks)
- {
- if (block.TransferCmd is ReturnCmd)
- {
- // note: if program control cannot reach this block, then postValue will be null
- if (block.PostInvariant != null)
- {
- post = (AI.Lattice.Element) lattice.Join(post, block.PostInvariant);
- }
- }
- }
-
- AI.Lattice.Element atReturn = post;
- foreach (Variable! var in impl.LocVars)
- {
- atReturn = this.lattice.Eliminate(atReturn, var);
- }
- foreach (Variable! var in impl.InParams)
- {
- atReturn = this.lattice.Eliminate(atReturn, var);
- }
-
- if ( ! this.lattice.LowerThan(atReturn, summaryEntry.OnExit))
- {
- // If the results of this analysis are strictly worse than
- // what we previous knew for the same input assumptions,
- // update the summary and re-do the call sites.
-
- summaryEntry.OnExit = this.lattice.Join(summaryEntry.OnExit, atReturn);
-
- foreach (CallSite callSite in summaryEntry.ReturnPoints)
- {
- this.callReturnWorkItems.Enqueue(callSite);
- }
- }
- }
+ ComputeBlockInvariants(impl, (!) impl.Blocks[0], summaryEntry.OnEntry, summaryEntry);
+ AdjustProcedureSummary(impl, summaryEntry);
}
}
}
@@ -402,13 +361,58 @@ namespace Microsoft.Boogie.AbstractInterpretation {
CallSite callSite = (CallSite!) this.callReturnWorkItems.Dequeue();
- PropagateStartingAtStatement( callSite.Impl, callSite.Block, callSite.Statement, callSite.KnownBeforeCall);
+ PropagateStartingAtStatement(callSite.Impl, callSite.Block, callSite.Statement, callSite.KnownBeforeCall, callSite.SummaryEntry);
+ AdjustProcedureSummary(callSite.Impl, callSite.SummaryEntry);
}
-
} // both queues
}
+
+ void AdjustProcedureSummary(Implementation! impl, ProcedureSummaryEntry! summaryEntry)
+ {
+ if (CommandLineOptions.Clo.IntraproceduralInfer) {
+ return; // no summary to adjust
+ }
+
+ // compute the procedure invariant by joining all terminal block invariants...
+ AI.Lattice.Element post = lattice.Bottom;
+ foreach (Block block in impl.Blocks)
+ {
+ if (block.TransferCmd is ReturnCmd)
+ {
+ // note: if program control cannot reach this block, then postValue will be null
+ if (block.PostInvariant != null)
+ {
+ post = (AI.Lattice.Element) lattice.Join(post, block.PostInvariant);
+ }
+ }
+ }
+
+ AI.Lattice.Element atReturn = post;
+ foreach (Variable! var in impl.LocVars)
+ {
+ atReturn = this.lattice.Eliminate(atReturn, var);
+ }
+ foreach (Variable! var in impl.InParams)
+ {
+ atReturn = this.lattice.Eliminate(atReturn, var);
+ }
+
+ if ( ! this.lattice.LowerThan(atReturn, summaryEntry.OnExit))
+ {
+ // If the results of this analysis are strictly worse than
+ // what we previous knew for the same input assumptions,
+ // update the summary and re-do the call sites.
+
+ summaryEntry.OnExit = this.lattice.Join(summaryEntry.OnExit, atReturn);
+
+ foreach (CallSite! callSite in summaryEntry.ReturnPoints)
+ {
+ this.callReturnWorkItems.Enqueue(callSite);
+ }
+ }
+ }
private static int freshVarId = 0;
private static Variable! FreshVar(Boogie.Type! ty)
@@ -427,7 +431,8 @@ namespace Microsoft.Boogie.AbstractInterpretation /// <param name="statementIndex"> </param>
/// <param name="currentValue"> The initial value </param>
/// </summary>
- private void PropagateStartingAtStatement (Implementation! impl, Block! block, int statementIndex, AI.Lattice.Element! currentValue)
+ private void PropagateStartingAtStatement (Implementation! impl, Block! block, int statementIndex, AI.Lattice.Element! currentValue,
+ ProcedureSummaryEntry! summaryEntry)
{
assume log.IsPeerConsistent;
log.DbgMsg(string.Format("{0}:", block.Label)); log.DbgMsgIndent();
@@ -439,7 +444,7 @@ namespace Microsoft.Boogie.AbstractInterpretation currentValue = Step(cmd, currentValue, impl, // Apply the transition function
delegate (AI.Lattice.Element! currentValue)
{
- return new CallSite(impl, block, cmdIndex, currentValue);
+ return new CallSite(impl, block, cmdIndex, currentValue, summaryEntry);
}
);
}
@@ -464,7 +469,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
succ.Lattice = block.Lattice; // The lattice is the same
// Propagate the post-abstract state of this block to the successor
- ComputeBlockInvariants(impl, succ, block.PostInvariant);
+ ComputeBlockInvariants(impl, succ, block.PostInvariant, summaryEntry);
}
}
}
@@ -680,8 +685,8 @@ namespace Microsoft.Boogie.AbstractInterpretation /// <param name="block"> The block for which we compute the invariants </param>
/// <param name="incomingValue"> The "init" abstract state for the block </param>
/// </summary>
- private void ComputeBlockInvariants (Implementation! impl, Block! block, AI.Lattice.Element! incomingValue)
- {
+ private void ComputeBlockInvariants (Implementation! impl, Block! block, AI.Lattice.Element! incomingValue, ProcedureSummaryEntry! summaryEntry)
+ {
if (block.PreInvariant == null) // block has not yet been processed
{
assert block.PostInvariant == null;
@@ -709,7 +714,7 @@ namespace Microsoft.Boogie.AbstractInterpretation return;
}
#if DEBUG_PRINT
- // Compute the free variables in incoming and block.PreInvariant
+ // Compute the free variables in incoming and block.PreInvariant
FreeVariablesVisitor freeVarsVisitorForA = new FreeVariablesVisitor();
FreeVariablesVisitor freeVarsVisitorForB = new FreeVariablesVisitor();
@@ -766,47 +771,22 @@ namespace Microsoft.Boogie.AbstractInterpretation #endif
#endregion
#region Propagate the entry abstract state through the method
- PropagateStartingAtStatement(impl, block, 0, (!) block.PreInvariant.Clone());
+ PropagateStartingAtStatement(impl, block, 0, (!) block.PreInvariant.Clone(), summaryEntry);
#endregion
}
#if DEBUG_PRINT
-private string! ToString(List<AI.IVariable!>! vars)
-{
- string s = "";
-
- foreach(AI.IVariable! v in vars)
- {
- s += v.Name +" ";
- }
- return s;
-}
-
-#endif
-
-
- /// <summary>
- /// Analyze the given set of blocks.
- /// <param name="blocks"> The set of blocks to analyze </param>
- /// <param name="entryPoint"> The initial block (from where we start the analysis </param>
- /// <param name="initialState"> The initial abstract state </param>
- /// </summary>
- public void AnalyzeBlocks(ICollection<Block!>! blocks, Block! entryPoint, AI.MathematicalLattice.Element! initialState)
- requires blocks.Contains(entryPoint);
+ private string! ToString(List<AI.IVariable!>! vars)
{
- TypeVariableSeq! dummyVarSeq = new TypeVariableSeq();
- VariableSeq! dummySeq = new VariableSeq();
- List<Block!> blockSequence = new List<Block!>();
-
- foreach(Block! block in blocks) {
- blockSequence.Add(block);
+ string s = "";
+
+ foreach(AI.IVariable! v in vars)
+ {
+ s += v.Name +" ";
}
-
- Implementation dummyImplementation =
- new Implementation(Token.NoToken, "dummyImplementation", dummyVarSeq, dummySeq, dummySeq, dummySeq, blockSequence);
-
- ComputeBlockInvariants(dummyImplementation, entryPoint, initialState);
+ return s;
}
+#endif
} // class
@@ -1004,58 +984,50 @@ private string! ToString(List<AI.IVariable!>! vars) public class AbstractInterpretation
{
/// <summary>
- /// Run the abstract interpretation.
- /// It has two entry points. One is the RunBoogie method. The other is the CCI PlugIn
- /// </summary>
- public static void RunAbstractInterpretation(Program! program)
- {
- Helpers.ExtraTraceInformation("Starting abstract interpretation");
-
- if(CommandLineOptions.Clo.UseAbstractInterpretation)
- {
- DateTime start = new DateTime(); // to please compiler's definite assignment rules
- if (CommandLineOptions.Clo.Trace) {
- Console.WriteLine();
- Console.WriteLine("Running abstract interpretation...");
- start = DateTime.Now;
- }
-
- WidenPoints.Compute(program);
-
- if (CommandLineOptions.Clo.Ai.AnySet) // if there is some user defined domain we override the default (= intervals)
- {
- AI.Lattice! lattice;
-
- lattice = AbstractDomainBuilder.BuildAbstractDomain().Lattice;
-
- ApplyAbstractInterpretation(program, lattice);
+ /// Run the abstract interpretation.
+ /// It has two entry points. One is the RunBoogie method. The other is the CCI PlugIn
+ /// </summary>
+ public static void RunAbstractInterpretation(Program! program)
+ {
+ Helpers.ExtraTraceInformation("Starting abstract interpretation");
- if (CommandLineOptions.Clo.Ai.DebugStatistics)
- {
- Console.Error.WriteLine(lattice);
- }
+ if(CommandLineOptions.Clo.UseAbstractInterpretation)
+ {
+ DateTime start = new DateTime(); // to please compiler's definite assignment rules
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine();
+ Console.WriteLine("Running abstract interpretation...");
+ start = DateTime.Now;
+ }
- if (!CommandLineOptions.Clo.IntraproceduralInfer)
- {
- Procedure.ShowSummaries = true;
- }
- }
- else // Otherwise the default is the use of the abstract domain of intervals (useful for simple for loops)
- {
- AI.Lattice! lattice = AbstractDomainBuilder.BuildIntervalsAbstractDomain().Lattice;
- ApplyAbstractInterpretation(program, lattice);
- }
+ WidenPoints.Compute(program);
- program.InstrumentWithInvariants();
+ if (CommandLineOptions.Clo.Ai.AnySet) // if there is some user defined domain we override the default (= intervals)
+ {
+ AI.Lattice lattice = AbstractDomainBuilder.BuildAbstractDomain().Lattice;
+ ApplyAbstractInterpretation(program, lattice);
- if (CommandLineOptions.Clo.Trace) {
- DateTime end = DateTime.Now;
- TimeSpan elapsed = end - start;
- Console.WriteLine(" [{0} s]", elapsed.TotalSeconds);
- Console.Out.Flush();
+ if (CommandLineOptions.Clo.Ai.DebugStatistics)
+ {
+ Console.Error.WriteLine(lattice);
}
}
+ else // Otherwise the default is the use of the abstract domain of intervals (useful for simple for loops)
+ {
+ AI.Lattice! lattice = AbstractDomainBuilder.BuildIntervalsAbstractDomain().Lattice;
+ ApplyAbstractInterpretation(program, lattice);
+ }
+
+ program.InstrumentWithInvariants();
+
+ if (CommandLineOptions.Clo.Trace) {
+ DateTime end = DateTime.Now;
+ TimeSpan elapsed = end - start;
+ Console.WriteLine(" [{0} s]", elapsed.TotalSeconds);
+ Console.Out.Flush();
+ }
}
+ }
static void ApplyAbstractInterpretation (Program! program, AI.Lattice! lattice)
{
diff --git a/Source/AbsInt/ExprFactories.ssc b/Source/AbsInt/ExprFactories.ssc index 1569c36c..ad090f2b 100644 --- a/Source/AbsInt/ExprFactories.ssc +++ b/Source/AbsInt/ExprFactories.ssc @@ -166,7 +166,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { /// <summary>
/// Returns true iff "t" denotes a type constant.
/// </summary>
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public bool IsTypeConstant(AI.IExpr! t)
ensures result == (t is Constant);
{
@@ -176,7 +176,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { /// <summary>
/// Returns true iff t0 and t1 are types such that t0 and t1 are equal.
/// </summary>
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public bool IsTypeEqual(AI.IExpr! t0, AI.IExpr! t1) {
Constant c0 = t0 as Constant;
Constant c1 = t1 as Constant;
@@ -186,10 +186,9 @@ namespace Microsoft.Boogie.AbstractInterpretation { /// <summary>
/// Returns true iff t0 and t1 are types such that t0 is a subtype of t1.
/// </summary>
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public bool IsSubType(AI.IExpr! t0, AI.IExpr! t1) {
assert false; // BUGBUG: TODO
- return false;
}
/// <summary>
@@ -198,7 +197,6 @@ namespace Microsoft.Boogie.AbstractInterpretation { /// </summary>
public AI.IExpr! JoinTypes(AI.IExpr! t0, AI.IExpr! t1) {
assert false; // BUGBUG: TODO
- throw new System.NotImplementedException();
}
public AI.IFunApp! IsExactlyA(AI.IExpr! e, AI.IExpr! type) {
diff --git a/Source/Basetypes/Set.ssc b/Source/Basetypes/Set.ssc index 221a9ad4..9286d6f5 100644 --- a/Source/Basetypes/Set.ssc +++ b/Source/Basetypes/Set.ssc @@ -189,7 +189,7 @@ namespace Microsoft.Boogie public virtual int Count
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)] get
+ get
{
return ht.Count;
}
@@ -201,7 +201,7 @@ namespace Microsoft.Boogie return ht.Keys.GetEnumerator();
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
string s = null;
diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc index 18d29c73..35175881 100644 --- a/Source/Core/Absy.ssc +++ b/Source/Core/Absy.ssc @@ -15,17 +15,19 @@ namespace Microsoft.Boogie.AbstractInterpretation public class CallSite
{
- public Implementation! Impl;
- public Block! Block;
- public int Statement; // invariant: Block[Statement] is CallCmd
- public AI.Lattice.Element! KnownBeforeCall;
+ public readonly Implementation! Impl;
+ public readonly Block! Block;
+ public readonly int Statement; // invariant: Block[Statement] is CallCmd
+ public readonly AI.Lattice.Element! KnownBeforeCall;
+ public readonly ProcedureSummaryEntry! SummaryEntry;
- public CallSite (Implementation! impl, Block! b, int stmt, AI.Lattice.Element! e)
+ public CallSite (Implementation! impl, Block! b, int stmt, AI.Lattice.Element! e, ProcedureSummaryEntry! summaryEntry)
{
this.Impl = impl;
this.Block = b;
this.Statement = stmt;
this.KnownBeforeCall = e;
+ this.SummaryEntry = summaryEntry;
}
}
@@ -532,7 +534,7 @@ namespace Microsoft.Boogie this.name = name;
// base(tok);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return (!) Name;
@@ -775,7 +777,7 @@ namespace Microsoft.Boogie TypecheckAttributes(tc);
this.TypedIdent.Typecheck(tc);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public object DoVisit(AI.ExprVisitor! visitor)
{
return visitor.VisitVariable(this);
@@ -1496,8 +1498,6 @@ namespace Microsoft.Boogie [Rep]
public readonly ProcedureSummary! Summary;
- public static bool ShowSummaries = false;
-
public Procedure (
IToken! tok,
string! name,
@@ -1559,9 +1559,9 @@ namespace Microsoft.Boogie e.Emit(stream, level);
}
- if (ShowSummaries)
+ if (!CommandLineOptions.Clo.IntraproceduralInfer)
{
- for (int s=0; s<this.Summary.Count; s++)
+ for (int s=0; s < this.Summary.Count; s++)
{
ProcedureSummaryEntry! entry = (!) this.Summary[s];
stream.Write(level + 1, "// ");
diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc index d0c65c96..da4f4247 100644 --- a/Source/Core/AbsyCmd.ssc +++ b/Source/Core/AbsyCmd.ssc @@ -775,7 +775,7 @@ namespace Microsoft.Boogie this.PostInvariant = null;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return this.Label + (this.widenBlock? "[w]" : "");
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index 2dd85a65..bed34c63 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -1842,7 +1842,8 @@ namespace Microsoft.Boogie switch on its left
/checkInfer : instrument inferred invariants as asserts to be checked by
theorem prover
- /interprocInfer : perform interprocedural inference
+ /interprocInfer : perform interprocedural inference (deprecated, not
+ supported)
/contractInfer : perform procedure contract inference
/logInfer : print debug output during inference
/printInstrumented : print Boogie program after it has been
diff --git a/Source/Core/GraphAlgorithms.ssc b/Source/Core/GraphAlgorithms.ssc index 7ce07d6e..aac45d73 100644 --- a/Source/Core/GraphAlgorithms.ssc +++ b/Source/Core/GraphAlgorithms.ssc @@ -33,7 +33,7 @@ namespace Microsoft.Boogie public bool IsReadOnly { get { return nodesMap.IsReadOnly; } }
public void Add(Node item) { nodesMap.Add(item,null); }
public void Clear() { nodesMap.Clear(); }
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public bool Contains(Node item) { return nodesMap.ContainsKey(item); }
public void CopyTo(Node[]! array, int arrayIndex) { nodes.CopyTo(array, arrayIndex); }
public bool Remove(Node item) { return nodesMap.Remove(item); }
@@ -148,7 +148,7 @@ namespace Microsoft.Boogie }
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
string outStr = "";
diff --git a/Source/Core/OOLongUtil.ssc b/Source/Core/OOLongUtil.ssc index 81dadf1b..e87666f3 100644 --- a/Source/Core/OOLongUtil.ssc +++ b/Source/Core/OOLongUtil.ssc @@ -34,7 +34,7 @@ namespace Boogie.Util { b.Flush();
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString() {
return "<TeeWriter: " + a.ToString() + ", " + b.ToString() + ">";
}
diff --git a/Source/Core/PureCollections.ssc b/Source/Core/PureCollections.ssc index d51ebe62..971af388 100644 --- a/Source/Core/PureCollections.ssc +++ b/Source/Core/PureCollections.ssc @@ -80,7 +80,7 @@ namespace PureCollections { [Pure][Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
public static bool operator != (Tuple s, Tuple t) { return ! (t == s); }
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override int GetHashCode (){
int h =0;
assume this.elems != null;
@@ -120,7 +120,7 @@ namespace PureCollections { }
//ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString() {
assert this.elems != null;
if (elems.Length==0)
@@ -165,7 +165,7 @@ namespace PureCollections { } while (index < map.elems.Length && map.elems[index] == null);
return index < map.elems.Length;
}
- public object Current{ [Pure][Reads(ReadsAttribute.Reads.Owned)] get {assert map.elems != null; return new Pair(map.elems[index],map.vals[index]); }}
+ public object Current{ get { assert map.elems != null; return new Pair(map.elems[index],map.vals[index]); }}
public void Reset() {index = -1; }
}
@@ -281,7 +281,7 @@ namespace PureCollections { }
//ToString - - - - - - - - - - - - - - - - - - - - - - - - -
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString() {
if (card ==0)
return "{|->}";
@@ -351,7 +351,7 @@ namespace PureCollections { public static bool operator != (Map s, Map t){
return ! (t == s);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override int GetHashCode (){
int h =0;
assert this.elems != null;
@@ -368,7 +368,7 @@ namespace PureCollections { //Ordinary map operations- - - - - - - - - - - - - - - - - - - - - - - -
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public bool Has(Object x) {
if (x == null)
throw new MissingCase();
@@ -427,7 +427,7 @@ namespace PureCollections { //while (index < seq.elems.Length); // Sequences allow nils ... && seq.elems[index] == null);
return index < seq.Length;
}
- public object Current{ [Pure][Reads(ReadsAttribute.Reads.Owned)] get {assert seq.elems != null; return seq.elems[index]; }}
+ public object Current{ get { assert seq.elems != null; return seq.elems[index]; }}
public void Reset() {index = -1; }
}
@@ -546,7 +546,7 @@ namespace PureCollections { }
//ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString() {
string s ="";
assert this.elems != null;
@@ -596,7 +596,7 @@ namespace PureCollections { public static bool operator != (Sequence s, Sequence t){
return !(s == t);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override int GetHashCode (){
int h = 0;
for(int i = 0; i < card; i++)
@@ -645,7 +645,7 @@ namespace PureCollections { public static bool operator >= (Sequence s, Sequence t){ return t <= s;}
//pure---------------------------------------------------------------
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public bool Has(object x) { // WS translate to tailrecursion
if (x == null)
throw new MissingCase();
@@ -658,7 +658,7 @@ namespace PureCollections { // the index of the first occurrence of x in this sequence,
// or -1 if x does not occur
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public int IndexOf(object x) {
if (x == null)
throw new MissingCase();
@@ -671,7 +671,7 @@ namespace PureCollections { // the index of the last occurrence of x in this sequence,
// or -1 if x does not occur
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public int LastIndexOf(object x) {
if (x == null)
throw new MissingCase();
diff --git a/Source/Graph/Graph.ssc b/Source/Graph/Graph.ssc index c9795f15..dcbd12a3 100644 --- a/Source/Graph/Graph.ssc +++ b/Source/Graph/Graph.ssc @@ -91,7 +91,7 @@ internal class DomRelation<Node>{ return false;
}
private Dictionary<Node,List<Node>>? domMap = null;
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string ToString(){
assume this.doms != null;
int[] localDoms = this.doms;
@@ -269,7 +269,7 @@ public class Graph<Node> { Node! myHeader;
internal PreHeader(Node! h) { myHeader = h; }
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString() { return "#" + myHeader.ToString(); }
}
@@ -295,7 +295,7 @@ public class Graph<Node> { { es = new Set<Pair<Node!,Node!>>(); ns = new Set<Node>(); }
// BUGBUG: Set<T>.ToString() should return a non-null string
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString() { return "" + es.ToString(); }
public void AddSource(Node! x)
diff --git a/Source/VCExpr/VCExprASTVisitors.ssc b/Source/VCExpr/VCExprASTVisitors.ssc index 47865747..2808f6bb 100644 --- a/Source/VCExpr/VCExprASTVisitors.ssc +++ b/Source/VCExpr/VCExprASTVisitors.ssc @@ -163,7 +163,6 @@ namespace Microsoft.Boogie.VCExprAST }
public object Current {
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
get {
return (!)CurrentExpr;
} }
|