| | | 1 | | using Microsoft.Z3; |
| | | 2 | | using System; |
| | | 3 | | |
| | | 4 | | namespace NanoCLang.Entities { |
| | | 5 | | /// <summary> |
| | | 6 | | /// Provides a superclass for all index entities. |
| | | 7 | | /// Also provides methods for analysing index overlaps. |
| | | 8 | | /// </summary> |
| | | 9 | | public abstract class Index : Base, ISubstitutable<Index>, ICloneable { |
| | | 10 | | /// <summary> |
| | | 11 | | /// Gets the zero-index that only contains the single offset zero. |
| | | 12 | | /// </summary> |
| | 101 | 13 | | public static Index Zero { get; } = new SingletonIndex(0); |
| | | 14 | | /// <summary> |
| | | 15 | | /// Checks if the <paramref name="index"/> that contains a type of <paramref name="otherSize"/> in bytes collide |
| | | 16 | | /// I.e. 0 and 2 collide with a 4 bit integer. |
| | | 17 | | /// Default behaviour if not overridden is the worst possible case that a collision always happens. |
| | | 18 | | /// </summary> |
| | | 19 | | /// <param name="index">Index to check against.</param> |
| | | 20 | | /// <param name="size">Size of the the type at the current index.</param> |
| | | 21 | | /// <param name="otherSize">Size of the type to check against.</param> |
| | | 22 | | /// <returns><see langword="true"/> iff the indices collide.</returns> |
| | | 23 | | public virtual bool CollidesWith(int size, Index index, int otherSize) |
| | 22 | 24 | | => NanoCSMT.Default.IndicesCollide(this, size, index, otherSize); |
| | | 25 | | /// <summary> |
| | | 26 | | /// Embeds the index of a type with given size into the SMT expression that allows all possible index values for |
| | | 27 | | /// </summary> |
| | | 28 | | /// <param name="smt">Solver to use for solving the collision.</param> |
| | | 29 | | /// <param name="size">Size of the type at the current index.</param> |
| | | 30 | | /// <param name="prefix">Variable name suffix.</param> |
| | | 31 | | /// <returns>Returns a guard expression and the index expression.</returns> |
| | | 32 | | public abstract (BoolExpr guard, IntExpr value) SMTPossibleValues(NanoCSMT smt, int size, string prefix); |
| | | 33 | | /// <summary> |
| | | 34 | | /// Checks if the <paramref name="offset"/> is included in the index. |
| | | 35 | | /// </summary> |
| | | 36 | | /// <param name="offset">Offset to check for.</param> |
| | | 37 | | /// <returns><see langword="true"/> iff the <paramref name="offset"/> is included in the current index.</returns |
| | | 38 | | public abstract bool IncludesOffset(int offset); |
| | | 39 | | /// <summary> |
| | | 40 | | /// Checks if the current index is a subindex of the <paramref name="other"/> index. |
| | | 41 | | /// </summary> |
| | | 42 | | /// <param name="other">Other index to check against.</param> |
| | | 43 | | /// <returns><see langword="true"/> iff the index values are included in the <paramref name="other"/> index.</re |
| | | 44 | | public abstract bool SubIndex(Index other); |
| | | 45 | | /// <inheritdoc/> |
| | | 46 | | public abstract object Clone(); |
| | | 47 | | /// <inheritdoc/> |
| | 73 | 48 | | public virtual Index Replace(Substitutor sub) => (Index)Clone(); |
| | | 49 | | #region Operators and Helper functions |
| | | 50 | | /// <summary> |
| | | 51 | | /// Checks if the <paramref name="lhs"/> is a subindex of the <paramref name="rhs"/>. |
| | | 52 | | /// </summary> |
| | | 53 | | /// <param name="lhs">Left hand operand.</param> |
| | | 54 | | /// <param name="rhs">Right hand operand.</param> |
| | | 55 | | /// <returns><see langword="true"/> iff <paramref name="lhs"/> is a subindex of <paramref name="rhs"/>.</returns |
| | 121 | 56 | | public static bool operator <=(Index lhs, Index rhs) => lhs == rhs || lhs.SubIndex(rhs); |
| | | 57 | | /// <summary> |
| | | 58 | | /// Checks if the <paramref name="rhs"/> is a subindex of the <paramref name="lhs"/>. |
| | | 59 | | /// </summary> |
| | | 60 | | /// <param name="rhs">Left hand operand.</param> |
| | | 61 | | /// <param name="lhs">Right hand operand.</param> |
| | | 62 | | /// <returns><see langword="true"/> iff <paramref name="rhs"/> is a subindex of <paramref name="lhs"/>.</returns |
| | 14 | 63 | | public static bool operator >=(Index lhs, Index rhs) => lhs == rhs || rhs.SubIndex(lhs); |
| | | 64 | | /// <summary> |
| | | 65 | | /// Creates a new index that is a superset of all values the addition operation of <paramref name="left"/> and < |
| | | 66 | | /// </summary> |
| | | 67 | | /// <param name="left">Index to add.</param> |
| | | 68 | | /// <param name="right">Index to add.</param> |
| | | 69 | | /// <returns>All posible values of the addition.</returns> |
| | 43 | 70 | | public static Index operator +(Index left, Index right) => left.Add(right); |
| | | 71 | | /// <summary> |
| | | 72 | | /// Creates a new index that is a superset of all values the subtraction operation of <paramref name="left"/> an |
| | | 73 | | /// </summary> |
| | | 74 | | /// <param name="left">Index to add.</param> |
| | | 75 | | /// <param name="right">Index to add.</param> |
| | | 76 | | /// <returns>All posible values of the subtraction.</returns> |
| | 17 | 77 | | public static Index operator -(Index left, Index right) => left.Sub(right); |
| | | 78 | | /// <summary> |
| | | 79 | | /// Creates a new index that is a superset of all values the addition operation of <see langword="this"/> and <p |
| | | 80 | | /// </summary> |
| | | 81 | | /// <param name="right">Index to add.</param> |
| | | 82 | | /// <returns>All posible values of the addition.</returns> |
| | | 83 | | protected abstract Index Add(Index right); |
| | | 84 | | /// <summary> |
| | | 85 | | /// Creates a new index that is a superset of all values the subtraction operation of <see langword="this"/> and |
| | | 86 | | /// </summary> |
| | | 87 | | /// <param name="right">Index to add.</param> |
| | | 88 | | /// <returns>All posible values of the subtraction.</returns> |
| | | 89 | | protected abstract Index Sub(Index right); |
| | | 90 | | #endregion |
| | | 91 | | } |
| | | 92 | | } |