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* --- Source/VCExpr/LetBindingSorter.cs | 322 +++++++++++++++++++------------------- 1 file changed, 161 insertions(+), 161 deletions(-) (limited to 'Source/VCExpr/LetBindingSorter.cs') diff --git a/Source/VCExpr/LetBindingSorter.cs b/Source/VCExpr/LetBindingSorter.cs index 474770d0..2bf28fbb 100644 --- a/Source/VCExpr/LetBindingSorter.cs +++ b/Source/VCExpr/LetBindingSorter.cs @@ -1,161 +1,161 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Text; -using System.IO; -using System.Linq; -using System.Collections; -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using Microsoft.Basetypes; - -// Sort the bindings in a let-expression so that terms bound earlier do -// not contain variables bound later - -namespace Microsoft.Boogie.VCExprAST { - - // (argument is not used) - public class LetBindingSorter : MutatingVCExprVisitor { - - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(FreeVarCollector != null); - } - - private readonly FreeVariableCollector/*!*/ FreeVarCollector = - new FreeVariableCollector(); - - private List/*!*/ FreeVarsIn(VCExpr expr) { - Contract.Requires(expr != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - FreeVarCollector.Collect(expr); - List/*!*/ freeVars = new List(FreeVarCollector.FreeTermVars.Keys); - FreeVarCollector.Reset(); - return freeVars; - } - - public LetBindingSorter(VCExpressionGenerator gen):base(gen) { - Contract.Requires(gen != null); - - } - - public override VCExpr Visit(VCExprLet node, bool arg){ -Contract.Requires(node != null); -Contract.Ensures(Contract.Result() != null); - IDictionary boundVars = - new Dictionary (); - - // recurse and collect the free variables in bound terms and formulae - foreach (VCExprLetBinding/*!*/ binding in node) {Contract.Assert(binding != null); - VCExpr/*!*/ newE = Mutate(binding.E, arg); - Binding/*!*/ b = new Binding (binding.V, newE, FreeVarsIn(newE)); - boundVars.Add(b.V, b); - } - - // generate the occurrence edges - foreach (KeyValuePair pair in boundVars) {Contract.Assert(cce.NonNullElements(pair)); - Binding/*!*/ b = pair.Value; - Contract.Assert(b != null); - foreach (VCExprVar/*!*/ v in b.FreeVars) {Contract.Assert(v != null); - Binding b2; - if (boundVars.TryGetValue(v, out b2)) { - cce.NonNull(b2).Occurrences.Add(b); - b.InvOccurrencesNum = b.InvOccurrencesNum + 1; - } - } - } - - // topological sort - Stack rootBindings = new Stack (); - foreach (KeyValuePair pair in boundVars) - {Contract.Assert(cce.NonNullElements(pair)); - if (pair.Value.InvOccurrencesNum == 0) - rootBindings.Push(pair.Value);} - - List/*!*/ sortedBindings = new List (); - while (rootBindings.Count > 0) { - Binding/*!*/ b = rootBindings.Pop(); - Contract.Assert(b != null); - sortedBindings.Add(b); - foreach (Binding/*!*/ b2 in b.Occurrences) { - Contract.Assert(b2 != null); - b2.InvOccurrencesNum = b2.InvOccurrencesNum - 1; - if (b2.InvOccurrencesNum == 0) - rootBindings.Push(b2); - } - } - - if (boundVars.Any(pair=> pair.Value.InvOccurrencesNum > 0)) - System.Diagnostics.Debug.Fail("Cyclic let-bindings"); - - Contract.Assert(node.Length == sortedBindings.Count); - - // check which of the bindings can be dropped - VCExpr newBody = Mutate(node.Body, arg); - Contract.Assert(newBody != null); - - IDictionary/*!*/ usedVars = - new Dictionary (); - foreach (VCExprVar/*!*/ v in FreeVarsIn(newBody)){Contract.Assert(v != null); - if (!usedVars.ContainsKey(v)) - usedVars.Add(v, v);} - - for (int i = sortedBindings.Count - 1; i >= 0; --i) { - if (usedVars.ContainsKey(sortedBindings[i].V)) { - foreach (VCExprVar/*!*/ v in sortedBindings[i].FreeVars){ - Contract.Assert(v != null); - if (!usedVars.ContainsKey(v)) - usedVars.Add(v, v);} - } else { - sortedBindings.RemoveAt(i); - } - } - - // assemble the resulting let-expression - List/*!*/ newBindings = new List(); - foreach (Binding b in sortedBindings) - newBindings.Add(Gen.LetBinding(b.V, b.E)); - - return Gen.Let(newBindings, newBody); - } - - private class Binding { - public readonly VCExprVar/*!*/ V; - public readonly VCExpr/*!*/ E; - public readonly List/*!*/ FreeVars; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(V != null); - Contract.Invariant(E != null); - Contract.Invariant(cce.NonNullElements(FreeVars)); - Contract.Invariant(Occurrences != null); - } - - - // list of all bound expression in which the variable V occurs - // (outgoing edges) - public readonly List/*!*/ Occurrences; - - // number of variables that are bound in this let-expression - // and that occur in FreeVars - // (incoming edges) - public int InvOccurrencesNum; - - public Binding(VCExprVar v, VCExpr e, List/*!*/ freeVars) { - Contract.Requires(e != null); - Contract.Requires(v != null); - Contract.Requires(cce.NonNullElements(freeVars)); - this.V = v; - this.E = e; - this.FreeVars = freeVars; - this.Occurrences = new List(); - this.InvOccurrencesNum = 0; - } - } - - } - -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Text; +using System.IO; +using System.Linq; +using System.Collections; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using Microsoft.Basetypes; + +// Sort the bindings in a let-expression so that terms bound earlier do +// not contain variables bound later + +namespace Microsoft.Boogie.VCExprAST { + + // (argument is not used) + public class LetBindingSorter : MutatingVCExprVisitor { + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(FreeVarCollector != null); + } + + private readonly FreeVariableCollector/*!*/ FreeVarCollector = + new FreeVariableCollector(); + + private List/*!*/ FreeVarsIn(VCExpr expr) { + Contract.Requires(expr != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + FreeVarCollector.Collect(expr); + List/*!*/ freeVars = new List(FreeVarCollector.FreeTermVars.Keys); + FreeVarCollector.Reset(); + return freeVars; + } + + public LetBindingSorter(VCExpressionGenerator gen):base(gen) { + Contract.Requires(gen != null); + + } + + public override VCExpr Visit(VCExprLet node, bool arg){ +Contract.Requires(node != null); +Contract.Ensures(Contract.Result() != null); + IDictionary boundVars = + new Dictionary (); + + // recurse and collect the free variables in bound terms and formulae + foreach (VCExprLetBinding/*!*/ binding in node) {Contract.Assert(binding != null); + VCExpr/*!*/ newE = Mutate(binding.E, arg); + Binding/*!*/ b = new Binding (binding.V, newE, FreeVarsIn(newE)); + boundVars.Add(b.V, b); + } + + // generate the occurrence edges + foreach (KeyValuePair pair in boundVars) {Contract.Assert(cce.NonNullElements(pair)); + Binding/*!*/ b = pair.Value; + Contract.Assert(b != null); + foreach (VCExprVar/*!*/ v in b.FreeVars) {Contract.Assert(v != null); + Binding b2; + if (boundVars.TryGetValue(v, out b2)) { + cce.NonNull(b2).Occurrences.Add(b); + b.InvOccurrencesNum = b.InvOccurrencesNum + 1; + } + } + } + + // topological sort + Stack rootBindings = new Stack (); + foreach (KeyValuePair pair in boundVars) + {Contract.Assert(cce.NonNullElements(pair)); + if (pair.Value.InvOccurrencesNum == 0) + rootBindings.Push(pair.Value);} + + List/*!*/ sortedBindings = new List (); + while (rootBindings.Count > 0) { + Binding/*!*/ b = rootBindings.Pop(); + Contract.Assert(b != null); + sortedBindings.Add(b); + foreach (Binding/*!*/ b2 in b.Occurrences) { + Contract.Assert(b2 != null); + b2.InvOccurrencesNum = b2.InvOccurrencesNum - 1; + if (b2.InvOccurrencesNum == 0) + rootBindings.Push(b2); + } + } + + if (boundVars.Any(pair=> pair.Value.InvOccurrencesNum > 0)) + System.Diagnostics.Debug.Fail("Cyclic let-bindings"); + + Contract.Assert(node.Length == sortedBindings.Count); + + // check which of the bindings can be dropped + VCExpr newBody = Mutate(node.Body, arg); + Contract.Assert(newBody != null); + + IDictionary/*!*/ usedVars = + new Dictionary (); + foreach (VCExprVar/*!*/ v in FreeVarsIn(newBody)){Contract.Assert(v != null); + if (!usedVars.ContainsKey(v)) + usedVars.Add(v, v);} + + for (int i = sortedBindings.Count - 1; i >= 0; --i) { + if (usedVars.ContainsKey(sortedBindings[i].V)) { + foreach (VCExprVar/*!*/ v in sortedBindings[i].FreeVars){ + Contract.Assert(v != null); + if (!usedVars.ContainsKey(v)) + usedVars.Add(v, v);} + } else { + sortedBindings.RemoveAt(i); + } + } + + // assemble the resulting let-expression + List/*!*/ newBindings = new List(); + foreach (Binding b in sortedBindings) + newBindings.Add(Gen.LetBinding(b.V, b.E)); + + return Gen.Let(newBindings, newBody); + } + + private class Binding { + public readonly VCExprVar/*!*/ V; + public readonly VCExpr/*!*/ E; + public readonly List/*!*/ FreeVars; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(V != null); + Contract.Invariant(E != null); + Contract.Invariant(cce.NonNullElements(FreeVars)); + Contract.Invariant(Occurrences != null); + } + + + // list of all bound expression in which the variable V occurs + // (outgoing edges) + public readonly List/*!*/ Occurrences; + + // number of variables that are bound in this let-expression + // and that occur in FreeVars + // (incoming edges) + public int InvOccurrencesNum; + + public Binding(VCExprVar v, VCExpr e, List/*!*/ freeVars) { + Contract.Requires(e != null); + Contract.Requires(v != null); + Contract.Requires(cce.NonNullElements(freeVars)); + this.V = v; + this.E = e; + this.FreeVars = freeVars; + this.Occurrences = new List(); + this.InvOccurrencesNum = 0; + } + } + + } + +} -- cgit v1.2.3