< Summary

Class:NanoCLang.Entities.Heap
Assembly:NanoCLang
File(s):C:\GitLab-Runner\builds\JxAESPd8\0\chenmichael\nanoc\src\NanoCLang\Entities\Heap\Heap.cs
Covered lines:151
Uncovered lines:33
Coverable lines:184
Total lines:380
Line coverage:82% (151 of 184)
Covered branches:62
Total branches:86
Branch coverage:72% (62 of 86)

Metrics

MethodBranch coverage Cyclomatic complexity Line coverage
.ctor(...)100%1100%
.ctor(...)50%277.77%
Contains(...)100%1100%
Domain()100%1100%
StrongUpdate(...)72.22%1885.71%
Clone()100%1100%
SuperHeap(...)25%4100%
TryGetBinding(...)100%1100%
.ctor()100%1100%
.ctor(...)100%1100%
.ctor(...)100%1100%
.ctor(...)100%10%
get_BoundLocations()100%1100%
GetBindings(...)100%1100%
get_Empty()100%1100%
IsAbstract()100%1100%
Filter(...)100%1100%
op_Division(...)0%40%
TryGetRest(...)100%10%
SubHeap(...)62.5%8100%
SubBlock(...)80%10100%
WellFormed(...)87.5%893.75%
ContainsAbstract(...)100%1100%
ContainsConcrete(...)100%10%
WellFormedAbstract(...)100%4100%
OffsetVar(...)100%1100%
CheckIndexOverlap(...)75%483.33%
WellFormedConcrete(...)100%2100%
Replace(...)100%2100%
Tokens()90%10100%
PrintLocationBinding()100%4100%
op_Multiply(...)50%283.33%
op_Multiply(...)50%280%
Equals(...)100%10%
Equals(...)50%2100%
GetHashCode()100%10%
op_Equality(...)100%1100%
op_Inequality(...)100%1100%

File(s)

C:\GitLab-Runner\builds\JxAESPd8\0\chenmichael\nanoc\src\NanoCLang\Entities\Heap\Heap.cs

#LineLine coverage
 1using NanoCLang.Environemnts;
 2using System;
 3using System.Collections.Generic;
 4using System.Diagnostics;
 5using System.Diagnostics.CodeAnalysis;
 6using System.Linq;
 7
 8namespace NanoCLang.Entities {
 9    /// <summary>
 10    /// Provides a class for heap entities.
 11    /// Also trivially implements the heap element interface.
 12    /// </summary>
 13    [DebuggerDisplay("{" + nameof(ToString) + "(),nq}")]
 14    public class Heap : Base, ISubstitutable<Heap>, IEquatable<Heap?>, IHeapElement, ICloneable {
 15        /// <summary>
 16        /// Creates a new heap instance from the list of location bindings.
 17        /// </summary>
 18        /// <param name="locations">Locations that are bound in the heap.</param>
 19        /// <exception cref="IllFormedException">Locations are not uniquely defined.</exception>
 46520        public Heap(IEnumerable<LocationBinding> locations) : this(locations.ToList()) { }
 21        /// <inheritdoc cref="Heap(IEnumerable{LocationBinding})"/>
 47422        public Heap(IList<LocationBinding> locations) {
 50223            var duplicates = locations.GroupBy(i => i.Location)
 26524              .Where(g => g.Count() > 1)
 23725              .Select(y => y.Key).ToList();
 23726            if (duplicates.Count > 0) {
 027                var firstDuplicate = duplicates.First();
 028                throw new IllFormedException(firstDuplicate, $"Cannot bind to location {firstDuplicate} twice in a heap!
 29            }
 76730            locationBindings = locations.ToDictionary(i => i.Location, i => i.Blocks);
 23731        }
 32        /// <summary>
 33        /// Checks if the heap has a binding for the <paramref name="location"/>.
 34        /// </summary>
 35        /// <param name="location">Location to check for.</param>
 36        /// <returns><see langword="true"/> iff there exists a matching location binding.</returns>
 637        public bool Contains(Location location) => locationBindings.ContainsKey(location);
 38        /// <summary>
 39        /// Gets an iterator for the domain of the heap. I.e. the set of locations bound in the heap.
 40        /// </summary>
 41        /// <returns>Iterator over the locations.</returns>
 6342        public IEnumerable<Location> Domain() => locationBindings.Keys;
 43        /// <summary>
 44        /// Performs a strong update to the location and offset appointed by the reference <paramref name="ptrRef"/>.
 45        /// Writes the <paramref name="value"/> to the location inside the new heap.
 46        /// Additionally performs a typecheck to verify that the written type matches current base type (refinement does
 47        /// </summary>
 48        /// <param name="ptrRef">Reference pointing to location and block offset for strong update.</param>
 49        /// <param name="value">Value expression to be written to the heap.</param>
 50        /// <param name="tau">Base type of the type that was bound at the written location. Can be typechecked against i
 51        /// <returns>New heap that contains the strong update.</returns>
 1752        public Heap StrongUpdate(ReferenceType ptrRef, PureExpression value, out BasicType tau) {
 1753            var heap = (Heap)Clone();
 1754            var bindings = heap.TryGetBinding(ptrRef.Location, out var tmp) ? tmp
 1755                : throw new IllFormedException(ptrRef, $"Cannot access pointer to location {ptrRef.Location} if the loca
 56
 1757            BlockType? bound = null;
 1758            switch (ptrRef.Offsets) {
 59            case SingletonIndex i:
 1060                VerbConsole.WriteLine(VerbosityLevel.Default, "T-Write-Field");
 8961                foreach (var block in bindings) if (i <= block.Index) { bound = block; break; }
 1062                if (bound is null)
 063                    throw new IllFormedException(this, $"Heap location does not have a writable field at index {i}!");
 2064                bound.Type = new RefinedType(bound.Type.BaseType, v => PureExpression.EqualExpression(v, value));
 1065                break;
 66            case SequenceIndex i:
 767                VerbConsole.WriteLine(VerbosityLevel.Default, "T-Write-Array");
 5668                foreach (var block in bindings) if (i <= block.Index) { bound = block; break; }
 769                if (bound is null)
 070                    throw new IllFormedException(this, $"Heap location does not have a writable field at index {i}!");
 771                break;
 072            default: throw new InvalidProgramException($"Expected valid index but got {ptrRef.Offsets}");
 73            }
 1774            tau = bound.Type.BaseType;
 1775            return heap;
 1776        }
 77        /// <summary>
 78        /// Clones the heap and returns the clone.
 79        /// </summary>
 80        /// <returns>Clone of the current heap.</returns>
 1781        public object Clone() => Replace(new Substitutor());
 82        /// <summary>
 83        /// Gets a heap that is a super heap of both input heaps.
 84        /// </summary>
 85        /// <param name="gamma">Environment to compare heaps within.</param>
 86        /// <param name="heap1">First input heap.</param>
 87        /// <param name="heap2">Second input heap.</param>
 88        /// <returns>Superheap of both heaps.</returns>
 89        /// <exception cref="IllFormedException">Heaps are incomatible.</exception>
 90        public static Heap SuperHeap(LocalEnvironment gamma, Heap heap1, Heap heap2)
 691        => heap1.SubHeap(gamma, heap2)
 692                        ? heap2
 693                        : heap2.SubHeap(gamma, heap1)
 694                            ? heap1
 695                            : throw new IllFormedException(heap1, $"Incompatible branch heaps in if expression: {heap2} 
 96        /// <summary>
 97        /// Checks if the heap has a binding for the <paramref name="location"/> and returns the binding at that locatio
 98        /// </summary>
 99        /// <param name="location">Location to check for.</param>
 100        /// <param name="binding">Binding at that location.</param>
 101        /// <returns><see langword="true"/> iff there exists a matching location binding.</returns>
 102        public bool TryGetBinding(Location location, [NotNullWhen(true)] out BlockType[]? binding)
 115103            => locationBindings.TryGetValue(location, out binding);
 104        /// <summary>
 105        /// Creates a new instance of an empty heap.
 106        /// </summary>
 48107        public Heap() : this(new LocationBinding[] { }) { }
 108        /// <summary>
 109        /// Creates a new instance of a heap with a single location <paramref name="binding"/>.
 110        /// </summary>
 111        /// <param name="binding">Single binding on the heap (if not abstract the heap can not be well formed).</param>
 18112        public Heap(LocationBinding binding) : this(new LocationBinding[] { binding }) { }
 113        /// <summary>
 114        /// Create a heap from a location -> blocktype[] enumeration.
 115        /// </summary>
 116        /// <param name="heap">Input to copy from.</param>
 324117        public Heap(IEnumerable<KeyValuePair<Location, BlockType[]>> heap) {
 162118            locationBindings = new Dictionary<Location, BlockType[]>(heap);
 162119        }
 120        /// <summary>
 121        /// Create a heap from an existing heap.
 122        /// </summary>
 123        /// <param name="heap">Input to copy from.</param>
 0124        public Heap(Heap heap) : this(heap.locationBindings) { }
 125        /// <summary>
 126        /// Locations that are bound in the heap.
 127        /// Same as <see cref="GetBindings(GlobalEnvironment, out IEnumerable{KeyValuePair{string, string}})"/> except t
 128        /// </summary>
 51129        public IEnumerable<LocationBinding> BoundLocations => locationBindings.Select(i => new LocationBinding(i.Key, i.
 130        /// <inheritdoc cref="IHeapElement.GetBindings(GlobalEnvironment, out IEnumerable{KeyValuePair{string, string}})
 6131        public IEnumerable<LocationBinding> GetBindings(GlobalEnvironment phi, out IEnumerable<KeyValuePair<string, stri
 6132            links = Enumerable.Empty<KeyValuePair<string, string>>();
 6133            return BoundLocations;
 6134        }
 135        /// <summary>
 136        /// Checks if the heap is empty and returns <see langword="true"/> iff it is.
 137        /// </summary>
 109138        public bool Empty => locationBindings.Count == 0;
 139        private readonly IDictionary<Location, BlockType[]> locationBindings;
 140        /// <summary>
 141        /// Checks if the heap contains purely abstract bindings.
 142        /// </summary>
 17143        public bool IsAbstract() => locationBindings.All(i => i.Key.Abstract);
 144        /// <summary>
 145        /// Create a heap from the current heap with locations that the <paramref name="predicate"/> evaluates to <see l
 146        /// </summary>
 147        /// <param name="predicate">Predicate to apply to the locations.</param>
 244148        public Heap Filter(Func<Location, bool> predicate) => new Heap(locationBindings.Where(i => predicate(i.Key)));
 149        /// <summary>
 150        /// Calculated the heap after subtracting the <paramref name="rhs"/> from the <paramref name="lhs"/>.
 151        /// </summary>
 152        /// <param name="lhs">Heap to subtract from.</param>
 153        /// <param name="rhs">Heap that is subtracted from the <paramref name="lhs"/>.</param>
 154        /// <returns><see langword="true"/> iff the rest was calculated.</returns>
 155        /// <exception cref="ArgumentNullException"><paramref name="lhs"/> or <paramref name="rhs"/> is <see langword="n
 156        /// <exception cref="InvalidOperationException"><paramref name="rhs"/> is not a sub-heap of <paramref name="lhs"
 0157        public static Heap operator /(Heap lhs, Heap rhs) {
 158            // bad core: keys in subheap that are not in the "super"-heap
 0159            var badCore = rhs.locationBindings.Keys.Except(lhs.locationBindings.Keys).ToList();
 0160            if (badCore.Count > 0) {
 0161                var l = badCore.First();
 0162                throw new InvalidOperationException($"Heap is not a subheap: {l} is not bound in left heap!");
 163            }
 164            // union core: keys in both heaps, needed to check for equality of bindings
 0165            var intersectionCore = rhs.locationBindings.Keys.ToHashSet();
 0166            var intersection = lhs.Filter(i => intersectionCore.Contains(i));
 0167            if (intersection != rhs)
 0168                throw new InvalidOperationException($"Heap is not a subheap: Key Intersection is not consistend!");
 169            // good core: keys only in the super-heap
 0170            var goodCore = lhs.locationBindings.Keys.Except(rhs.locationBindings.Keys).ToHashSet();
 0171            return lhs.Filter(i => goodCore.Contains(i));
 0172        }
 173        /// <summary>
 174        /// Try to get the rest of the heap after subtracting the <paramref name="heap"/> from this heap.
 175        /// If the input is a sub-heap of this heap the difference is calculated as <paramref name="rest"/> <see langwor
 176        /// otherwise the function returns <see langword="false"/>.
 177        /// </summary>
 178        /// <param name="heap">Heap that is subtracted from this heap.</param>
 179        /// <param name="rest">Difference between the heaps, or <see langword="null"/></param>
 180        /// <exception cref="ArgumentNullException"><paramref name="heap"/> is <see langword="null"/>.</exception>
 181        /// <returns><see langword="true"/> iff the rest was calculated.</returns>
 0182        public bool TryGetRest(Heap heap, [NotNullWhen(true)] out Heap? rest) {
 0183            try {
 0184                rest = this / heap;
 0185                return true;
 0186            } catch (InvalidOperationException) { rest = null; }
 0187            return false;
 0188        }
 189        /// <summary>
 190        /// Checks if the current heap is a subheap of the <paramref name="other"/> heap in the given environment.
 191        /// </summary>
 192        /// <param name="gamma">Environment to check the subheap in.</param>
 193        /// <param name="other">Other heap to check against.</param>
 194        /// <returns><see langword="true"/> iff the current heap is a subheap of the <paramref name="other"/> heap.</ret
 34195        public bool SubHeap(LocalEnvironment gamma, Heap other) {
 34196            VerbConsole.WriteLine(VerbosityLevel.Default, "<:-Heap");
 34197            if (locationBindings.Count != other.locationBindings.Count) return false;
 34198            var keys = locationBindings.Keys.ToHashSet();
 34199            if (!keys.SetEquals(other.locationBindings.Keys.ToHashSet())) return false;
 202200            foreach (var key in keys)
 50201                if (!SubBlock(gamma, locationBindings[key], other.locationBindings[key])) return false;
 34202            return true;
 34203        }
 204        /// <summary>
 205        /// Checks if the block <paramref name="left"/> is a subtype of the <paramref name="right"/> block in the given 
 206        /// </summary>
 207        /// <param name="gamma">Environment to check the subtype in.</param>
 208        /// <param name="left">Current block to check with.</param>
 209        /// <param name="right">Other block to check against.</param>
 210        /// <returns><see langword="true"/> iff the current block is a subtype of the <paramref name="right"/> type.</re
 65211        public static bool SubBlock(LocalEnvironment gamma, BlockType[] left, BlockType[] right) {
 65212            var gammaOut = new LocalEnvironment(gamma);
 65213            if (left.Length != right.Length) return false;
 350214            for (int i = 0; i < left.Length; i++) {
 74215                var b1 = left[i];
 74216                var b2 = right[i];
 74217                if (b1.Index != b2.Index) return false;
 75218                if (!b1.Type.SubType(gammaOut, b2.Type)) return false;
 91219                if (b1.Index is SingletonIndex idx) {
 18220                    VerbConsole.WriteLine(VerbosityLevel.Default, "<:-Field");
 18221                    gammaOut[OffsetVar(idx.Offset)] = b1.Type;
 73222                } else VerbConsole.WriteLine(VerbosityLevel.Default, "<:-Array");
 73223            }
 64224            VerbConsole.WriteLine(VerbosityLevel.Default, "<:-Block-Empty");
 64225            return true;
 65226        }
 227        /// <summary>
 228        /// Checks if the heap is well-formed and raises an exception if it is ill-formed.
 229        /// </summary>
 230        /// <param name="gamma">Environemt to check the heap with.</param>
 231        /// <exception cref="IllFormedException">Heap is ill-formed.</exception>
 108232        public void WellFormed(LocalEnvironment gamma) {
 141233            if (Empty) VerbConsole.WriteLine(VerbosityLevel.Default, "WF-Empty");
 765234            foreach (var locationBinding in locationBindings) {
 147235                var l = locationBinding.Key;
 147236                var b = locationBinding.Value;
 252237                if (l.Abstract) {
 105238                    VerbConsole.WriteLine(VerbosityLevel.Default, $"WF-Abstract: {l}");
 239                    // Check ~l not already on the heap (currenlty enforced by design)
 105240                    WellFormedAbstract(gamma, b);
 147241                } else {
 42242                    VerbConsole.WriteLine(VerbosityLevel.Default, $"WF-Concrete: {l}");
 243                    // Check l_j not already on the heap (currenlty enforced by design)
 42244                    if (!ContainsAbstract(l.Name))
 0245                        throw new IllFormedException(l, $"Heap must contain binding to abstract location {l.Name}!");
 42246                    WellFormedConcrete(gamma, b);
 42247                }
 147248            }
 108249        }
 250        /// <summary>
 251        /// Checks if the heap contains a binding to the abstract location named <paramref name="name"/>.
 252        /// </summary>
 253        /// <param name="name">Name of the location to check.</param>
 254        /// <returns><see langword="true"/> iff the abstract location exists.</returns>
 93255        public bool ContainsAbstract(string name) => locationBindings.ContainsKey(new Location(name, true));
 256        /// <summary>
 257        /// Checks if the heap contains a binding to the concrete location named <paramref name="name"/>.
 258        /// </summary>
 259        /// <param name="name">Name of the location to check.</param>
 260        /// <returns><see langword="true"/> iff the concrete location exists.</returns>
 0261        public bool ContainsConcrete(string name) => locationBindings.ContainsKey(new Location(name, false));
 262        /// <summary>
 263        /// Check if the abstract block <paramref name="b"/> is well formed in the environment <paramref name="gammaIn"/
 264        /// </summary>
 265        /// <param name="gammaIn">Environment to check the block in.</param>
 266        /// <param name="b">Block to check.</param>
 105267        private void WellFormedAbstract(LocalEnvironment gammaIn, BlockType[] b) {
 105268            var gamma = new LocalEnvironment(gammaIn);
 615269            for (int i = 0; i < b.Length; i++) {
 135270                var binding = b[i];
 135271                binding.Type.WellFormed(gamma, this);
 135272                CheckIndexOverlap(b, i);
 135273                switch (binding.Index) {
 274                case SingletonIndex idx:
 62275                    VerbConsole.WriteLine(VerbosityLevel.Default, $"WF-Field: {binding.Type}");
 62276                    gamma[OffsetVar(idx.Offset)] = binding.Type;
 62277                    break;
 278                default:
 73279                    VerbConsole.WriteLine(VerbosityLevel.Default, $"WF-Array: {binding.Type}");
 73280                    break;
 281                }
 135282            }
 105283        }
 284        /// <summary>
 285        /// Gets a string that represents the variable containing the block offset in the environment.
 286        /// </summary>
 287        /// <param name="offset">Offset to represent.</param>
 288        /// <returns>Variable name</returns>
 177289        public static string OffsetVar(int offset) => $"@{offset}";
 290        /// <summary>
 291        /// Check if the index of the current binding overlaps with previous bindings in the location.
 292        /// </summary>
 293        /// <param name="b">Array of bindings in the location.</param>
 294        /// <param name="i">Index of current binding in the location</param>
 186295        private static void CheckIndexOverlap(BlockType[] b, int i) {
 186296            var binding = b[i];
 186297            var bindingSize = binding.Type.Size;
 489298            for (int j = 0; j < i; j++) {
 39299                var domB = b[j];
 39300                try {
 39301                    if (binding.Index.CollidesWith(bindingSize, domB.Index, domB.Type.Size))
 0302                        throw new IllFormedException(binding.Index, $"Index collides with binding at {domB.Index}!");
 39303                } catch (NotImplementedException e) {
 0304                    throw new IllFormedException(binding.Index, $"Cannot safely reason about the index overlapping. Deta
 305                }
 39306            }
 186307        }
 308        /// <summary>
 309        /// Check if the concrete block <paramref name="b"/> is well formed in the environment <paramref name="gamma"/>.
 310        /// </summary>
 311        /// <param name="gamma">Environment to check the block in.</param>
 312        /// <param name="b">Block to check.</param>
 42313        private void WellFormedConcrete(LocalEnvironment gamma, BlockType[] b) {
 237314            for (int i = 0; i < b.Length; i++) {
 51315                var binding = b[i];
 51316                VerbConsole.WriteLine(VerbosityLevel.Default, $"WF-ConcBlock: {binding.Type}");
 51317                binding.Type.WellFormed(gamma, this);
 51318                CheckIndexOverlap(b, i);
 51319            }
 42320        }
 321        /// <inheritdoc/>
 322        public Heap Replace(Substitutor sub)
 47323            => new Heap(locationBindings.Select(i
 145324                => new KeyValuePair<Location, BlockType[]>(
 145325                    i.Key.Replace(sub),
 267326                    i.Value.Select(i => i.Replace(sub)).ToArray())));
 327        /// <inheritdoc/>
 8328        public override IEnumerable<StringFormatterToken> Tokens(NanoCSourceFormat args) {
 8329            var locations = BoundLocations.GetEnumerator();
 8330            if (!locations.MoveNext()) { yield return "emp"; yield break; }
 642331            foreach (var tk in locations.Current.Tokens(args)) yield return tk;
 16332            while (locations.MoveNext())
 708333                foreach (var tk in StringFormatterToken.Indented(args.IndentHeapListOperator,
 358334                    () => PrintLocationBinding(args, locations.Current))) yield return tk;
 8335        }
 336
 8337        private static IEnumerable<StringFormatterToken> PrintLocationBinding(NanoCSourceFormat args, LocationBinding lo
 40338            for (int i = 0; i < args.NewlinesBeforeBindingListOperator; i++) yield return new NewLineToken();
 8339            yield return args.HeapBindingListSeparator;
 954340            foreach (var tk in location.Tokens(args)) yield return tk;
 8341        }
 342        /// <summary>
 343        /// Concatenates the <paramref name="left"/> and <paramref name="right"/> heap and returns
 344        /// </summary>
 345        /// <param name="left"></param>
 346        /// <param name="right"></param>
 347        /// <returns>Returns the concatenated heap.</returns>
 348        /// <exception cref="ArgumentException">Heap bindings overlap.</exception>
 21349        public static Heap operator *(Heap left, Heap right) {
 21350            var intersection = left.locationBindings.Keys.Intersect(right.locationBindings.Keys).ToList();
 21351            if (intersection.Count > 0)
 0352                throw new ArgumentException($"Heaps overlap in locations {string.Join(", ", intersection)}!");
 21353            return new Heap(left.locationBindings.Concat(right.locationBindings));
 21354        }
 355        /// <summary>
 356        /// Adds the location <paramref name="binding"/> to the <paramref name="heap"/>.
 357        /// </summary>
 358        /// <param name="heap">Heap to add to.</param>
 359        /// <param name="binding">Location binding to add.</param>
 360        /// <returns>Returns the concatenated heap.</returns>
 361        /// <exception cref="ArgumentException">Heap bindings overlap.</exception>
 8362        public static Heap operator *(Heap heap, LocationBinding binding) {
 8363            if (heap.locationBindings.Keys.Contains(binding.Location))
 0364                throw new ArgumentException($"Cannot append binding to {string.Join(", ", binding.Location)}!");
 8365            return new Heap(heap.locationBindings.Append(new KeyValuePair<Location, BlockType[]>(binding.Location, bindi
 8366        }
 367        #region Equality checks
 368        /// <inheritdoc/>
 0369        public override bool Equals(object? obj) => Equals(obj as Heap);
 370        /// <inheritdoc/>
 69371        public bool Equals(Heap? other) => !(other is null) && HeapComparer.Default.Equals(locationBindings, other.locat
 372        /// <inheritdoc/>
 0373        public override int GetHashCode() => HashCode.Combine(locationBindings);
 374        /// <inheritdoc/>
 21375        public static bool operator ==(Heap? left, Heap? right) => EqualityComparer<Heap?>.Default.Equals(left, right);
 376        /// <inheritdoc/>
 21377        public static bool operator !=(Heap? left, Heap? right) => !(left == right);
 378        #endregion
 379    }
 380}