diff options
| author |  rustanleino <unknown> | 2010-02-18 01:58:27 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-02-18 01:58:27 +0000 |
| commit | 36bda629c0083590c5e4d17f06e769f822617033 (patch) | |
| tree | 1591f3b47a97f4bd3cc0333b0a0dc8eeb40c20de | |
| parent | 0549304b5beaf553ba3e5fa6550a6b8e43e31553 (diff) | |
* Added "deprecated" comment in help message about /interprocInfer switch. The functionality is currently broken.
* Adjust procedure summaries also after processing call returns (used only in interprocedural inference, which is currently not really supported, but this change would be needed if we ever decide to support it)
* Some other code clean-up, like removing unnecessary [Reads(...Owned)] attributes on [Pure] methods
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;
} }
|