| | | 1 | | using Microsoft.Z3; |
| | | 2 | | using NanoCLang.Environemnts; |
| | | 3 | | using System; |
| | | 4 | | using System.Collections.Generic; |
| | | 5 | | |
| | | 6 | | namespace NanoCLang.Entities { |
| | | 7 | | /// <summary> |
| | | 8 | | /// Provides a class for integer literal constants. |
| | | 9 | | /// </summary> |
| | | 10 | | public class IntegerConstant : PureExpression, IEquatable<IntegerConstant?>, ICloneable { |
| | | 11 | | /// <summary> |
| | | 12 | | /// Creates a new integer constant with <paramref name="value"/> and a <paramref name="size"/> in bytes. |
| | | 13 | | /// </summary> |
| | | 14 | | /// <param name="value">Value of the literal.</param> |
| | | 15 | | /// <param name="size">Size of the integer literal in bytes.</param> |
| | 1334 | 16 | | public IntegerConstant(int value, int size) { |
| | 667 | 17 | | Size = size; |
| | 667 | 18 | | Value = value; |
| | 667 | 19 | | } |
| | | 20 | | /// <summary> |
| | | 21 | | /// Size of the integer literal in bytes. |
| | | 22 | | /// </summary> |
| | 1746 | 23 | | public int Size { get; } |
| | | 24 | | /// <summary> |
| | | 25 | | /// Value of the literal. |
| | | 26 | | /// </summary> |
| | 2552 | 27 | | public int Value { get; } |
| | | 28 | | /// <inheritdoc/> |
| | 79 | 29 | | public override void WellFormed(LocalEnvironment gamma) { |
| | 79 | 30 | | if (Size < 0) |
| | 1 | 31 | | throw new IllFormedException(this, $"Integer literal cannot have negative size {Size}!"); |
| | 78 | 32 | | } |
| | | 33 | | /// <inheritdoc/> |
| | 144 | 34 | | protected override Type DoInferType(LocalEnvironment gamma) => new RefinedType(new IntegerType(Size, new Singlet |
| | 288 | 35 | | v => EqualExpression(v, this)); |
| | | 36 | | /// <inheritdoc/> |
| | 608 | 37 | | public override IEnumerable<StringFormatterToken> Tokens(NanoCSourceFormat args) { |
| | 650 | 38 | | if (Value == 0 && Size == 0) { |
| | 42 | 39 | | yield return "return"; |
| | 42 | 40 | | yield break; |
| | | 41 | | } |
| | 566 | 42 | | yield return Value.ToString(); |
| | 566 | 43 | | yield return "_"; |
| | 566 | 44 | | yield return Size.ToString(); |
| | 566 | 45 | | } |
| | | 46 | | /// <inheritdoc/> |
| | 455 | 47 | | public override ArithExpr ToArithmetic(LocalEnvironment gamma, NanoCSMT smt) => smt.Context.MkInt(Value); |
| | | 48 | | /// <inheritdoc/> |
| | 144 | 49 | | public override BoolExpr ToBoolean(LocalEnvironment gamma, NanoCSMT smt) => smt.Context.MkBool(Value != 0); |
| | | 50 | | /// <inheritdoc/> |
| | 244 | 51 | | public override PureExpression Replace(Substitutor sub) => (PureExpression)Clone(); |
| | | 52 | | /// <inheritdoc/> |
| | 244 | 53 | | public virtual object Clone() => new IntegerConstant(Value, Size); |
| | | 54 | | /// <inheritdoc/> |
| | 53 | 55 | | protected override IEnumerable<StringFormatterToken> NoReturnTokens(CSourceFormat args) { |
| | 53 | 56 | | if (args.PureRequiresReturn && Size == 0) yield break; |
| | 53 | 57 | | yield return "("; |
| | 53 | 58 | | yield return IntegerType.GetCType(Size); |
| | 53 | 59 | | yield return ")"; |
| | 53 | 60 | | yield return Value.ToString(); |
| | 53 | 61 | | yield return "LL"; |
| | 53 | 62 | | } |
| | | 63 | | #region Equality checks |
| | | 64 | | /// <inheritdoc/> |
| | 169 | 65 | | public override bool Equals(object? obj) => Equals(obj as IntegerConstant); |
| | | 66 | | /// <inheritdoc/> |
| | 169 | 67 | | public bool Equals(IntegerConstant? other) => !(other is null) && Size == other.Size && Value == other.Value; |
| | | 68 | | /// <inheritdoc/> |
| | 4 | 69 | | public override int GetHashCode() => System.HashCode.Combine(Size, Value); |
| | | 70 | | /// <inheritdoc/> |
| | 0 | 71 | | public static bool operator ==(IntegerConstant? left, IntegerConstant? right) => EqualityComparer<IntegerConstan |
| | | 72 | | /// <inheritdoc/> |
| | 0 | 73 | | public static bool operator !=(IntegerConstant? left, IntegerConstant? right) => !(left == right); |
| | | 74 | | #endregion |
| | | 75 | | } |
| | | 76 | | } |