< Summary

Class:NanoCLang.Entities.PureExpression
Assembly:NanoCLang
File(s):C:\GitLab-Runner\builds\JxAESPd8\0\chenmichael\nanoc\src\NanoCLang\Entities\Expression\PureExpression\PureExpression.cs
Covered lines:32
Uncovered lines:4
Coverable lines:36
Total lines:177
Line coverage:88.8% (32 of 36)
Covered branches:8
Total branches:8
Branch coverage:100% (8 of 8)

Metrics

MethodBranch coverage Cyclomatic complexity Line coverage
get_FixedType()100%1100%
InferType(...)100%1100%
ToBoolean(...)100%10%
ToArithmetic(...)100%10%
DoInferWorld(...)100%1100%
CheckType(...)100%10%
CheckType(...)100%2100%
RequiredFunctions()100%1100%
Tokens()100%6100%
NoReturnTokens(...)100%1100%
op_Explicit(...)100%10%
op_Explicit(...)100%1100%
EqualExpression(...)100%1100%
UnqualExpression(...)100%1100%
op_LessThanOrEqual(...)100%1100%
op_GreaterThanOrEqual(...)100%1100%
op_LessThan(...)100%1100%
op_GreaterThan(...)100%1100%
op_Addition(...)100%1100%
op_Subtraction(...)100%1100%
op_BitwiseAnd(...)100%1100%
op_BitwiseOr(...)100%1100%

File(s)

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

#LineLine coverage
 1using Microsoft.Z3;
 2using NanoCLang.Environemnts;
 3using System;
 4using System.Collections.Generic;
 5using static NanoCLang.Entities.RelationalExpression;
 6
 7namespace NanoCLang.Entities {
 8    /// <summary>
 9    /// Provides an abstract class for pure expressions.
 10    /// Pure expressions are a subset of all NanoC expressions that do not modify the heap.
 11    /// </summary>
 12    public abstract class PureExpression : Expression, ISubstitutable<PureExpression> {
 13        /// <summary>
 14        /// Gets the type that was fixed to the pure expression during type-checking.
 15        /// </summary>
 99216        public Type? FixedType { get; private set; }
 17        /// <summary>
 18        /// Infer the type of the pure expression based on the environment <paramref name="gamma"/>.
 19        /// Additionally fixes the result of the inference to the expression entity.
 20        /// </summary>
 21        /// <param name="gamma">Environment for type inference.</param>
 22        /// <returns>Inferred type of the expression</returns>
 98023        public Type InferType(LocalEnvironment gamma) => FixedType = DoInferType(gamma);
 24        /// <summary>
 25        /// Infer the type of the pure expression based on the environment <paramref name="gamma"/>.
 26        /// </summary>
 27        /// <param name="gamma">Environment for type inference.</param>
 28        /// <returns>Inferred type of the expression</returns>
 29        protected abstract Type DoInferType(LocalEnvironment gamma);
 30        /// <summary>
 31        /// Converts the expression to a boolean expression that the SMT solver can handle.
 32        /// </summary>
 33        /// <param name="gamma">The local environment to solve with.</param>
 34        /// <param name="smt">SMT solver context.</param>
 35        /// <returns>Boolean expression that makes up the environment.</returns>
 036        public virtual BoolExpr ToBoolean(LocalEnvironment gamma, NanoCSMT smt) => throw new NotImplementedException($"N
 37        /// <summary>
 38        /// Converts the expression to an arithmetic expression that the SMT solver can handle.
 39        /// </summary>
 40        /// <param name="gamma">The local environment to solve with.</param>
 41        /// <param name="smt">SMT solver context.</param>
 42        /// <returns>Arithmetic expression that makes up the environment.</returns>
 043        public virtual ArithExpr ToArithmetic(LocalEnvironment gamma, NanoCSMT smt) => throw new NotImplementedException
 44        /// <inheritdoc/>
 3145        protected override World DoInferWorld(GlobalEnvironment phi, LocalEnvironment gamma, Heap heap) {
 3146            VerbConsole.WriteLine(VerbosityLevel.Default, "T-Pure");
 3147            return new World(InferType(gamma), heap);
 3148        }
 49        /// <inheritdoc/>
 050        public override void CheckType(GlobalEnvironment phi, LocalEnvironment gamma, Heap heap, World world) => CheckTy
 51        /// <summary>
 52        /// Typecheck the pure expression with the <paramref name="type"/> and throw an exception if it is ill-formed.
 53        /// </summary>
 54        /// <param name="gamma">Local Environemt to check the expression with.</param>
 55        /// <param name="type">Type to typecheck with.</param>
 56        /// <exception cref="IllFormedException">Pure expression is ill-formed.</exception>
 6457        public virtual void CheckType(LocalEnvironment gamma, Type type) {
 6458            VerbConsole.WriteLine(VerbosityLevel.Default, "T-PureSub");
 6459            var inferred = InferType(gamma);
 6560            if (!inferred.SubType(gamma, type)) throw new IllFormedException(this, $"{this} : {{{inferred}}} is not of t
 6361        }
 62        /// <summary>
 63        /// Infer the type of the pure expression based on the environment <paramref name="gamma"/>.
 64        /// </summary>
 65        /// <param name="gamma">Environment for well-formedness checking.</param>
 66        public abstract void WellFormed(LocalEnvironment gamma);
 67        /// <inheritdoc/>
 668        public override IEnumerable<string> RequiredFunctions() { yield break; }
 69        /// <inheritdoc/>
 70        public abstract PureExpression Replace(Substitutor sub);
 71        /// <inheritdoc/>
 17772        public override IEnumerable<StringFormatterToken> Tokens(CSourceFormat args) {
 20273            if (args.PureRequiresReturn) yield return "return ";
 17774            var requiresReturn = args.PureRequiresReturn;
 17775            args.PureRequiresReturn = false;
 247276            foreach (var tk in NoReturnTokens(args)) yield return tk;
 17777            args.PureRequiresReturn = requiresReturn;
 20278            if (args.PureRequiresReturn) yield return ";";
 17779        }
 80        /// <inheritdoc cref="Tokens(CSourceFormat)"/>
 9581        protected virtual IEnumerable<StringFormatterToken> NoReturnTokens(CSourceFormat args) => Tokens((NanoCSourceFor
 82        #region Helper functions / Operators
 83        /// <summary>
 84        /// Converts the boolean <paramref name="value"/> to a pure expression in form of a boolean literal.
 85        /// </summary>
 86        /// <param name="value">Value to convert to an expression.</param>
 87        /// <returns><see cref="BooleanConstant"/> with the given <paramref name="value"/>.</returns>
 088        public static explicit operator PureExpression(bool value) => new BooleanConstant(value);
 89        /// <summary>
 90        /// Converts the integer literal <paramref name="value"/> to a pure expression in form of an integer literal.
 91        /// </summary>
 92        /// <param name="value">Value to convert to an expression.</param>
 93        /// <returns><see cref="IntegerConstant"/> with the given <paramref name="value"/>.</returns>
 1194        public static explicit operator PureExpression(int value) => new IntegerConstant(value, sizeof(int));
 95        /// <summary>
 96        /// Generates a new binary expression from the input.
 97        /// </summary>
 98        /// <param name="lhs">Left hand side of the operation.</param>
 99        /// <param name="rhs">Right hand side of the operation.</param>
 100        /// <returns><see cref="BinaryExpression"/> that models the operation.</returns>
 101        public static BinaryExpression EqualExpression(PureExpression lhs, PureExpression rhs)
 971102            => new RelationalExpression(lhs, RelOperator.Equal, rhs);
 103        /// <summary>
 104        /// Generates a new binary expression from the input.
 105        /// </summary>
 106        /// <param name="lhs">Left hand side of the operation.</param>
 107        /// <param name="rhs">Right hand side of the operation.</param>
 108        /// <returns><see cref="BinaryExpression"/> that models the operation.</returns>
 109        public static BinaryExpression UnqualExpression(PureExpression lhs, PureExpression rhs)
 21110            => new RelationalExpression(lhs, RelOperator.Unequal, rhs);
 111        /// <summary>
 112        /// Generates a new binary expression from the input.
 113        /// </summary>
 114        /// <param name="lhs">Left hand side of the operation.</param>
 115        /// <param name="rhs">Right hand side of the operation.</param>
 116        /// <returns><see cref="BinaryExpression"/> that models the operation.</returns>
 117        public static BinaryExpression operator <=(PureExpression lhs, PureExpression rhs)
 1118            => new RelationalExpression(lhs, RelOperator.LessEqual, rhs);
 119        /// <summary>
 120        /// Generates a new binary expression from the input.
 121        /// </summary>
 122        /// <param name="lhs">Left hand side of the operation.</param>
 123        /// <param name="rhs">Right hand side of the operation.</param>
 124        /// <returns><see cref="BinaryExpression"/> that models the operation.</returns>
 125        public static BinaryExpression operator >=(PureExpression lhs, PureExpression rhs)
 6126            => new RelationalExpression(lhs, RelOperator.GreaterEqual, rhs);
 127        /// <summary>
 128        /// Generates a new binary expression from the input.
 129        /// </summary>
 130        /// <param name="lhs">Left hand side of the operation.</param>
 131        /// <param name="rhs">Right hand side of the operation.</param>
 132        /// <returns><see cref="BinaryExpression"/> that models the operation.</returns>
 133        public static BinaryExpression operator <(PureExpression lhs, PureExpression rhs)
 7134            => new RelationalExpression(lhs, RelOperator.Less, rhs);
 135        /// <summary>
 136        /// Generates a new binary expression from the input.
 137        /// </summary>
 138        /// <param name="lhs">Left hand side of the operation.</param>
 139        /// <param name="rhs">Right hand side of the operation.</param>
 140        /// <returns><see cref="BinaryExpression"/> that models the operation.</returns>
 141        public static BinaryExpression operator >(PureExpression lhs, PureExpression rhs)
 14142            => new RelationalExpression(lhs, RelOperator.Greater, rhs);
 143        /// <summary>
 144        /// Generates a new binary expression from the input.
 145        /// </summary>
 146        /// <param name="lhs">Left hand side of the operation.</param>
 147        /// <param name="rhs">Right hand side of the operation.</param>
 148        /// <returns><see cref="BinaryExpression"/> that models the operation.</returns>
 149        public static BinaryExpression operator +(PureExpression lhs, PureExpression rhs)
 22150            => new AdditionExpression(lhs, rhs);
 151        /// <summary>
 152        /// Generates a new binary expression from the input.
 153        /// </summary>
 154        /// <param name="lhs">Left hand side of the operation.</param>
 155        /// <param name="rhs">Right hand side of the operation.</param>
 156        /// <returns><see cref="BinaryExpression"/> that models the operation.</returns>
 157        public static BinaryExpression operator -(PureExpression lhs, PureExpression rhs)
 5158            => new SubtractionExpression(lhs, rhs);
 159        /// <summary>
 160        /// Generates a new binary expression from the input.
 161        /// </summary>
 162        /// <param name="lhs">Left hand side of the operation.</param>
 163        /// <param name="rhs">Right hand side of the operation.</param>
 164        /// <returns><see cref="BinaryExpression"/> that models the operation.</returns>
 165        public static BinaryExpression operator &(PureExpression lhs, PureExpression rhs)
 474166            => new BooleanExpression(lhs, BooleanExpression.BoolOperator.And, rhs);
 167        /// <summary>
 168        /// Generates a new binary expression from the input.
 169        /// </summary>
 170        /// <param name="lhs">Left hand side of the operation.</param>
 171        /// <param name="rhs">Right hand side of the operation.</param>
 172        /// <returns><see cref="BinaryExpression"/> that models the operation.</returns>
 173        public static BinaryExpression operator |(PureExpression lhs, PureExpression rhs)
 6174            => new BooleanExpression(lhs, BooleanExpression.BoolOperator.Or, rhs);
 175        #endregion
 176    }
 177}