| | | 1 | | using NanoCLang.Environemnts; |
| | | 2 | | using System; |
| | | 3 | | using System.Collections.Generic; |
| | | 4 | | |
| | | 5 | | namespace NanoCLang.Entities { |
| | | 6 | | /// <summary> |
| | | 7 | | /// Provide an abstract base class for all reading expressions. |
| | | 8 | | /// </summary> |
| | | 9 | | public abstract class ReadExpression : Expression { |
| | | 10 | | /// <summary> |
| | | 11 | | /// Equivalent read expression that is fixed during type inference. |
| | | 12 | | /// </summary> |
| | 14 | 13 | | public virtual PointerReadExpression? BaseRead { get; protected set; } |
| | | 14 | | /// <inheritdoc/> |
| | | 15 | | public override IEnumerable<StringFormatterToken> Tokens(CSourceFormat args) |
| | 6 | 16 | | => (BaseRead ?? throw new InvalidOperationException("Read Expression must be fixed when translating!")) |
| | 6 | 17 | | .Tokens(args); |
| | | 18 | | } |
| | | 19 | | /// <summary> |
| | | 20 | | /// Provides a class for pointer read expressions. |
| | | 21 | | /// </summary> |
| | | 22 | | public class PointerReadExpression : ReadExpression, IEquatable<PointerReadExpression?> { |
| | | 23 | | /// <summary> |
| | | 24 | | /// Creates a new instance of a pointer read expression that reads the value of the <paramref name="pointer"/>. |
| | | 25 | | /// </summary> |
| | | 26 | | /// <param name="pointer">Pointer to write to.</param> |
| | | 27 | | public PointerReadExpression(PureExpression pointer) { |
| | | 28 | | Pointer = pointer; |
| | | 29 | | } |
| | | 30 | | /// <summary> |
| | | 31 | | /// Pointer that is read from. |
| | | 32 | | /// </summary> |
| | | 33 | | public PureExpression Pointer { get; } |
| | | 34 | | /// <inheritdoc/> |
| | | 35 | | public override PointerReadExpression? BaseRead { get => this; protected set => throw new InvalidOperationExcept |
| | | 36 | | /// <summary> |
| | | 37 | | /// Gets the type that the pointer points to if it is well-formed. |
| | | 38 | | /// Additionally checks if the type that is bound at the index in the heap is safe within bounds of the allocati |
| | | 39 | | /// </summary> |
| | | 40 | | /// <param name="ptrType">(Refined) type of the pointer expression.</param> |
| | | 41 | | /// <param name="gamma">Local environment to check the pointer with.</param> |
| | | 42 | | /// <param name="heap">Heap that contains (if well-formed) the appointed location.</param> |
| | | 43 | | /// <returns>Type of the value the pointer points to.</returns> |
| | | 44 | | public static Type GetPointerValueType(Type ptrType, LocalEnvironment gamma, Heap heap) { |
| | | 45 | | if (!(ptrType.BaseType is ReferenceType ptrRef)) |
| | | 46 | | throw new IllFormedException(ptrType, $"Cannot read from non-reference of type {ptrType.BaseType}"); |
| | | 47 | | if (ptrRef.Abstract) |
| | | 48 | | throw new IllFormedException(ptrType, "Cannot read from abstract reference!"); |
| | | 49 | | var loc = ptrRef.Location; |
| | | 50 | | var bindings = heap.TryGetBinding(loc, out var tmp) ? tmp |
| | | 51 | | : throw new IllFormedException(ptrType, $"Cannot access pointer to location {loc} if the location is not |
| | | 52 | | |
| | | 53 | | Type? bound = null; |
| | | 54 | | foreach (var block in bindings) if (ptrRef.Offsets <= block.Index) { |
| | | 55 | | bound = block.Type; |
| | | 56 | | break; |
| | | 57 | | } |
| | | 58 | | |
| | | 59 | | if (bound is null) |
| | | 60 | | throw new IllFormedException(ptrRef.Offsets, $"Heap location {loc} does not contain a binding at offset |
| | | 61 | | |
| | | 62 | | if (!ptrType.SubType(gamma, new RefinedType(ptrRef, |
| | | 63 | | v => new UninterpretedApplicationExpression("SafeN", v, new IntegerConstant(bound.Size, 4))))) |
| | | 64 | | throw new IllFormedException(ptrType, $"Pointer is not safe and can not be read from!"); |
| | | 65 | | return bound; |
| | | 66 | | } |
| | | 67 | | /// <inheritdoc/> |
| | | 68 | | protected override World DoInferWorld(GlobalEnvironment phi, LocalEnvironment gamma, Heap heap) { |
| | | 69 | | VerbConsole.WriteLine(VerbosityLevel.Default, "T-Read"); |
| | | 70 | | var ptrType = Pointer.InferType(gamma); |
| | | 71 | | return new World(GetPointerValueType(ptrType, gamma, heap), heap); |
| | | 72 | | } |
| | | 73 | | /// <inheritdoc/> |
| | | 74 | | public override IEnumerable<StringFormatterToken> Tokens(NanoCSourceFormat args) { |
| | | 75 | | yield return "*"; |
| | | 76 | | if (args.SpaceAfterDerefOperator) yield return " "; |
| | | 77 | | foreach (var tk in Pointer.Tokens(args)) yield return tk; |
| | | 78 | | } |
| | | 79 | | /// <inheritdoc/> |
| | | 80 | | public override IEnumerable<StringFormatterToken> Tokens(CSourceFormat args) { |
| | | 81 | | if (FixedWorld is null) throw new InvalidOperationException("Expression must have fixed world when translati |
| | | 82 | | yield return "*"; |
| | | 83 | | if (args.SpaceAfterDerefOperator) yield return " "; |
| | | 84 | | yield return "(("; |
| | | 85 | | foreach (var tk in FixedWorld.Type.Tokens(args)) yield return tk; |
| | | 86 | | yield return "*)"; |
| | | 87 | | foreach (var tk in Pointer.Tokens(args)) yield return tk; |
| | | 88 | | yield return ")"; |
| | | 89 | | } |
| | | 90 | | /// <inheritdoc/> |
| | | 91 | | public override IEnumerable<string> RequiredFunctions() { yield break; } |
| | | 92 | | #region Equality checks |
| | | 93 | | /// <inheritdoc/> |
| | | 94 | | public override bool Equals(object? obj) => Equals(obj as PointerReadExpression); |
| | | 95 | | /// <inheritdoc/> |
| | | 96 | | public bool Equals(PointerReadExpression? other) => !(other is null) && EqualityComparer<PureExpression>.Default |
| | | 97 | | /// <inheritdoc/> |
| | | 98 | | public override int GetHashCode() => HashCode.Combine(Pointer); |
| | | 99 | | /// <inheritdoc/> |
| | | 100 | | public static bool operator ==(PointerReadExpression? left, PointerReadExpression? right) => EqualityComparer<Po |
| | | 101 | | /// <inheritdoc/> |
| | | 102 | | public static bool operator !=(PointerReadExpression? left, PointerReadExpression? right) => !(left == right); |
| | | 103 | | #endregion |
| | | 104 | | } |
| | | 105 | | } |