< Summary

Class:NanoCLang.Environemnts.LocalEnvironment
Assembly:NanoCLang
File(s):C:\GitLab-Runner\builds\JxAESPd8\0\chenmichael\nanoc\src\NanoCLang\Environemnts\LocalEnvironment.cs
Covered lines:66
Uncovered lines:12
Coverable lines:78
Total lines:179
Line coverage:84.6% (66 of 78)
Covered branches:20
Total branches:32
Branch coverage:62.5% (20 of 32)

Metrics

MethodBranch coverage Cyclomatic complexity Line coverage
.ctor()100%1100%
.ctor(...)100%1100%
.ctor(...)100%1100%
AddStructLocs(...)100%2100%
TryGetStructLoc(...)100%1100%
PushGuard(...)100%1100%
PopGuard()100%1100%
ToString()100%4100%
Guarded(...)50%2100%
With(...)50%4100%
With(...)87.5%8100%
WithStructLoc(...)0%80%
With(...)100%1100%
ToBoolean(...)100%1100%
EmbedEUFA()100%4100%

File(s)

C:\GitLab-Runner\builds\JxAESPd8\0\chenmichael\nanoc\src\NanoCLang\Environemnts\LocalEnvironment.cs

#LineLine coverage
 1using Microsoft.Z3;
 2using NanoCLang.Entities;
 3using System;
 4using System.Collections.Generic;
 5using System.Diagnostics;
 6using System.Diagnostics.CodeAnalysis;
 7using System.Linq;
 8using System.Text;
 9using Type = NanoCLang.Entities.Type;
 10
 11namespace NanoCLang.Environemnts {
 12    /// <summary>
 13    /// Provides a class for local environments.
 14    /// A local environment maps names in a specific scope to their respective types.
 15    /// Additionally local environments can contain guard expressions for code flow analysis.
 16    /// </summary>
 17    [DebuggerDisplay("{" + nameof(ToString) + "(),nq}")]
 18    public class LocalEnvironment : Dictionary<string, Type> {
 19        /// <summary>
 20        /// Creates a new instance of an empty local environment.
 21        /// </summary>
 16822        public LocalEnvironment() : base() {
 8423            guards = new Stack<PureExpression>();
 8424            structureLocations = new Dictionary<string, string>();
 8425        }
 26        /// <summary>
 27        /// Creates a new instance of a local environment that contains all elements copied from the input environment <
 28        /// </summary>
 29        /// <param name="gamma">Environment to copy from.</param>
 34230        public LocalEnvironment(LocalEnvironment gamma) : base(gamma) {
 17131            guards = new Stack<PureExpression>(gamma.guards.Reverse());
 17132            structureLocations = new Dictionary<string, string>(gamma.structureLocations);
 17133        }
 34        /// <summary>
 35        /// Creates a new instance of a local environment from a list of type assignments.
 36        /// </summary>
 37        /// <param name="types">Type assignments to copy from.</param>
 6438        public LocalEnvironment(IEnumerable<KeyValuePair<string, Type>> types) : base(types) {
 3239            guards = new Stack<PureExpression>();
 3240            structureLocations = new Dictionary<string, string>();
 3241        }
 42        /// <summary>
 43        /// Adds links to the local environment.
 44        /// </summary>
 45        /// <param name="links">Structure links to add.</param>
 3246        public void AddStructLocs(IEnumerable<KeyValuePair<string, string>> links) {
 14247            foreach (var (key, val) in links)
 2348                structureLocations.Add(key, val);
 3249        }
 50
 51        /// <summary>
 52        /// Guard expressions in the current environment.
 53        /// </summary>
 54        private readonly Stack<PureExpression> guards;
 55        /// <summary>
 56        /// Attempts to get a struct location binding from the environment.
 57        /// </summary>
 58        /// <param name="loc">Location that is linked to a struct.</param>
 59        /// <param name="structName">Name of the struct the <paramref name="loc"/> is linked to.</param>
 60        /// <returns><see langword="true"/> iff the location link was found.</returns>
 1161        public bool TryGetStructLoc(string loc, [NotNullWhen(true)] out string structName) => structureLocations.TryGetV
 62        private readonly Dictionary<string, string> structureLocations;
 63        /// <summary>
 64        /// Add a guard expression to the environment.
 65        /// </summary>
 66        /// <param name="guard">Guard expression that restricts the environment.</param>
 2767        public void PushGuard(PureExpression guard) => guards.Push(guard);
 68        /// <summary>
 69        /// Removes and returns the topmost guard expression of the environment.
 70        /// </summary>
 71        /// <returns>The guard expression that was removed from the top of the environment.</returns>
 72        /// <exception cref="InvalidOperationException">No guard expression is on the environment.</exception>
 3173        public PureExpression PopGuard() => guards.Pop();
 74        /// <inheritdoc/>
 475        public override string ToString() {
 576            var sb = new StringBuilder(string.Join(',', this.Select(i => $"{i.Key}:{i.Value}")));
 777            if (guards.Count > 0) {
 2478                foreach (var guard in guards) sb.Append('|').Append(guard.ToString());
 379            }
 480            return sb.ToString();
 481        }
 82        /// <summary>
 83        /// Evaluates a function with a guarded localenvironment.
 84        /// </summary>
 85        /// <typeparam name="T">Function output to evaluate</typeparam>
 86        /// <param name="guard">Guard expression.</param>
 87        /// <param name="p">Function that evaluates the body.</param>
 88        /// <returns>Evaluated function result.</returns>
 2489        public T Guarded<T>(PureExpression guard, Func<LocalEnvironment, T> p) {
 2490            PushGuard(guard);
 2491            try {
 2492                return p(this);
 2493            } finally {
 2494                if (guard != PopGuard()) throw new InvalidProgramException("Guard stack was changed out of scope!");
 2495            }
 2496        }
 97        /// <summary>
 98        /// Evaluates a function with additional bindings on the environment.
 99        /// This function allows for evaluating judgements with additional bindings on an environment without the need t
 100        /// </summary>
 101        /// <typeparam name="T">Function output to evaluate.</typeparam>
 102        /// <param name="name">Name of the binding.</param>
 103        /// <param name="type">Type that the name is bound to.</param>
 104        /// <param name="p">Function that evaluates the body.</param>
 105        /// <returns>Evaluated function result.</returns>
 275106        public T With<T>(string name, Type type, Func<LocalEnvironment, T> p) {
 107            // Get the value that was overridden by the name (can be null)
 275108            var overridden = TryGetValue(name, out var t) ? t : null;
 275109            this[name] = type;
 275110            try {
 275111                return p(this);
 275112            } finally {
 275113                if (overridden is Type) this[name] = overridden;
 275114                else Remove(name);
 275115            }
 273116        }
 117        /// <summary>
 118        /// Evaluates a function with additional bindings on the environment.
 119        /// </summary>
 120        /// <typeparam name="T">Function output to evaluate.</typeparam>
 121        /// <param name="bindings">Additional bindings on the envionment.</param>
 122        /// <param name="p">Function that evaluates the body.</param>
 123        /// <returns>Evaluated function result.</returns>
 6124        public T With<T>(IEnumerable<KeyValuePair<string, Type>> bindings, Func<LocalEnvironment, T> p) {
 18125            var below = new Dictionary<string, Type?>(bindings.Select(i => i.Key).Select(i => new KeyValuePair<string, T
 6126            try {
 30127                foreach (var (name, type) in bindings)
 6128                    this[name] = type;
 6129                return p(this);
 6130            } finally {
 30131                foreach (var (name, type) in below)
 6132                    if (type is Type) this[name] = type;
 6133                    else Remove(name);
 6134            }
 6135        }
 136        /// <summary>
 137        /// Evaluates a function with additional bindings on the environment.
 138        /// </summary>
 139        /// <typeparam name="T">Function output to evaluate.</typeparam>
 140        /// <param name="bindings">Additional bindings on the envionment.</param>
 141        /// <param name="p">Function that evaluates the body.</param>
 142        /// <returns>Evaluated function result.</returns>
 0143        public T WithStructLoc<T>(IEnumerable<KeyValuePair<string, string>> bindings, Func<LocalEnvironment, T> p) {
 0144            var below = new Dictionary<string, string?>(bindings.Select(i => i.Key).Select(i => new KeyValuePair<string,
 0145            try {
 0146                foreach (var (location, @struct) in bindings)
 0147                    structureLocations[location] = @struct;
 0148                return p(this);
 0149            } finally {
 0150                foreach (var (location, @struct) in below)
 0151                    if (@struct is string) structureLocations[location] = @struct;
 0152                    else structureLocations.Remove(location);
 0153            }
 0154        }
 155        /// <summary>
 156        /// Executes an action with additional bindings on the environment.
 157        /// </summary>
 158        /// <param name="name">Name of the binding.</param>
 159        /// <param name="type">Type that the name is bound to.</param>
 160        /// <param name="p">Action to execute with the additional binding.</param>
 161        public void With(string name, Type type, Action<LocalEnvironment> p) =>
 595162            _ = With(name, type, gamma => { p(this); return true; });
 163        /// <summary>
 164        /// Converts the expression to an boolean expression that the SMT solver can handle.
 165        /// </summary>
 166        /// <param name="smt">SMT solver context.</param>
 167        /// <returns>Boolean expression that makes up the environment.</returns>
 168        public BoolExpr ToBoolean(NanoCSMT smt)
 238169        => smt.Context.MkAnd(guards.Select(i => i.ToBoolean(this, smt))
 138170            .Concat(EmbedEUFA(smt).ToList()));
 138171        private IEnumerable<BoolExpr> EmbedEUFA(NanoCSMT smt) {
 1911172            foreach (var entry in this) {
 666173                if (!(entry.Value is RefinedType r)) continue;
 332174                var refinement = r.Refinement.Replace(new Substitutor() { Variables = new Dictionary<string, PureExpress
 332175                yield return refinement.ToBoolean(this, smt);
 332176            }
 138177        }
 178    }
 179}
Generated by: ReportGenerator 4.8.8.0
28/07/2021 - 23:15:07
GitHub | www.palmmedia.de

Methods/Properties

.ctor()
.ctor(...)
.ctor(...)
AddStructLocs(...)
TryGetStructLoc(...)
PushGuard(...)
PopGuard()
ToString()
Guarded(...)
With(...)
With(...)
WithStructLoc(...)
With(...)
ToBoolean(...)
EmbedEUFA()