diff options
26 files changed, 353 insertions, 320 deletions
diff --git a/aarch64/Makefile b/aarch64/Makefile index 38900d5f..aa4d5301 100644 --- a/aarch64/Makefile +++ b/aarch64/Makefile @@ -13,6 +13,9 @@ aarch64_c: aarch64.c aarch64: no_vector.sail $(SAIL) $^ -o aarch64 -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3 +aarch64_full: full.sail + $(SAIL) $^ -o aarch64_full -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3 + aarch64.lem: no_vector.sail $(SAIL) $^ -o aarch64 -lem -lem_lib Aarch64_extras -memo_z3 -undefined_gen -no_lexp_bounds_check aarch64_types.lem: aarch64.lem diff --git a/aarch64/full/spec.sail b/aarch64/full/spec.sail index 897fa56e..d98322fd 100644 --- a/aarch64/full/spec.sail +++ b/aarch64/full/spec.sail @@ -2006,7 +2006,7 @@ val BigEndianReverse : forall ('width : Int), 'width >= 0 & 'width >= 0. function BigEndianReverse value_name = { assert('width == 8 | 'width == 16 | 'width == 32 | 'width == 64 | 'width == 128); let 'half = 'width / 2; - assert(constraint('half * 2 = 'width)); + assert(constraint('half * 2 == 'width)); if 'width == 8 then return(value_name) else (); return(BigEndianReverse(slice(value_name, 0, half)) @ BigEndianReverse(slice(value_name, half, 'width - half))) } @@ -2131,7 +2131,7 @@ val Replicate : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0. function Replicate x = { assert('N % 'M == 0, "((N MOD M) == 0)"); let 'O = 'N / 'M; - assert(constraint('O * 'M = 'N)); + assert(constraint('O * 'M == 'N)); return(replicate_bits(x, 'N / 'M)) } @@ -2945,7 +2945,7 @@ val aarch64_integer_insext_insert_movewide : (int, int, bits(16), MoveWideOp, in function aarch64_integer_insext_insert_movewide ('d, 'datasize, imm, opcode, 'pos) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; if opcode == MoveWideOp_K then result = aget_X(d) else result = Zeros(); result = __SetSlice_bits(datasize, 16, result, pos, imm); @@ -2957,7 +2957,7 @@ val aarch64_integer_insext_extract_immediate : (int, int, int, int, int) -> unit function aarch64_integer_insext_extract_immediate ('d, 'datasize, 'lsb, 'm, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); @@ -2970,7 +2970,7 @@ val aarch64_integer_arithmetic_rev : (int, int, int, int) -> unit effect {escape function aarch64_integer_arithmetic_rev ('container_size, 'd, 'datasize, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand : bits('datasize) = aget_X(n); result : bits('datasize) = undefined; containers : int = datasize / container_size; @@ -2992,7 +2992,7 @@ val aarch64_integer_arithmetic_rbit : (int, int, int) -> unit effect {escape, rr function aarch64_integer_arithmetic_rbit ('d, 'datasize, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand : bits('datasize) = aget_X(n); result : bits('datasize) = undefined; foreach (i from 0 to (datasize - 1) by 1 in inc) @@ -3014,7 +3014,7 @@ val aarch64_integer_arithmetic_mul_widening_64128hi : (int, int, int, int, bool) function aarch64_integer_arithmetic_mul_widening_64128hi ('d, 'datasize, 'm, 'n, unsigned) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); result : int = asl_Int(operand1, unsigned) * asl_Int(operand2, unsigned); @@ -3041,7 +3041,7 @@ function aarch64_integer_arithmetic_mul_widening_3264 ('a, 'd, 'datasize, 'dests assert(constraint('destsize in {32, 64}), "destsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); operand3 : bits('destsize) = aget_X(a); @@ -3071,7 +3071,7 @@ function aarch64_integer_arithmetic_mul_uniform_addsub ('a, 'd, 'datasize, 'dest assert(constraint('destsize in {32, 64}), "destsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); operand3 : bits('destsize) = aget_X(a); @@ -3098,7 +3098,7 @@ val aarch64_integer_arithmetic_div : (int, int, int, int, bool) -> unit effect { function aarch64_integer_arithmetic_div ('d, 'datasize, 'm, 'n, unsigned) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); result : int = undefined; @@ -3122,7 +3122,7 @@ val aarch64_integer_arithmetic_cnt : (int, int, int, CountOp) -> unit effect {es function aarch64_integer_arithmetic_cnt ('d, 'datasize, 'n, opcode) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : int = undefined; operand1 : bits('datasize) = aget_X(n); if opcode == CountOp_CLZ then result = CountLeadingZeroBits(operand1) else result = CountLeadingSignBits(operand1); @@ -3144,7 +3144,7 @@ val aarch64_integer_arithmetic_addsub_carry : (int, int, int, int, bool, bool) - function aarch64_integer_arithmetic_addsub_carry ('d, 'datasize, 'm, 'n, setflags, sub_op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); @@ -3341,7 +3341,7 @@ val aarch64_integer_bitfield : forall ('datasize : Int). function aarch64_integer_bitfield ('R, 'S, 'd, datasize, extend, inzero, 'n, tmask, wmask) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); dst : bits('datasize) = if inzero then Zeros() else aget_X(d); src : bits('datasize) = aget_X(n); bot : bits('datasize) = dst & ~(wmask) | ROR(src, R) & wmask; @@ -3367,7 +3367,7 @@ val aarch64_integer_shift_variable : (int, int, int, int, ShiftType) -> unit eff function aarch64_integer_shift_variable ('d, 'datasize, 'm, 'n, shift_type) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand2 : bits('datasize) = aget_X(m); result = ShiftReg(n, shift_type, UInt(operand2) % datasize); @@ -3390,7 +3390,7 @@ val aarch64_integer_logical_shiftedreg : (int, int, bool, int, int, LogicalOp, b function aarch64_integer_logical_shiftedreg ('d, 'datasize, invert, 'm, 'n, op, setflags, 'shift_amount, shift_type) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = ShiftReg(m, shift_type, shift_amount); if invert then operand2 = ~(operand2) else (); @@ -3408,7 +3408,7 @@ val aarch64_integer_arithmetic_addsub_shiftedreg : (int, int, int, int, bool, in function aarch64_integer_arithmetic_addsub_shiftedreg ('d, 'datasize, 'm, 'n, setflags, 'shift_amount, shift_type, sub_op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = ShiftReg(m, shift_type, shift_amount); @@ -3764,7 +3764,7 @@ val aarch64_integer_logical_immediate : forall ('datasize : Int). function aarch64_integer_logical_immediate ('d, datasize, imm, 'n, op, setflags) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = imm; @@ -3782,7 +3782,7 @@ val aarch64_integer_arithmetic_addsub_immediate : forall ('datasize : Int). function aarch64_integer_arithmetic_addsub_immediate ('d, datasize, imm, 'n, setflags, sub_op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand1 : bits('datasize) = if n == 31 then aget_SP() else aget_X(n); operand2 : bits('datasize) = imm; @@ -3801,7 +3801,7 @@ val aarch64_integer_arithmetic_addsub_extendedreg : (int, int, ExtendType, int, function aarch64_integer_arithmetic_addsub_extendedreg ('d, 'datasize, extend_type, 'm, 'n, setflags, 'shift, sub_op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand1 : bits('datasize) = if n == 31 then aget_SP() else aget_X(n); operand2 : bits('datasize) = ExtendReg(m, extend_type, shift); @@ -5319,7 +5319,7 @@ function Reduce (op, input, esize) = { result : bits('esize) = undefined; if 'N == 'esize then return(input) else (); let 'half = 'N / 2; - assert(constraint('half * 2 = 'N)); + assert(constraint('half * 2 == 'N)); hi = Reduce(op, slice(input, half, negate(half) + 'N), 'esize); lo = Reduce(op, slice(input, 0, half), 'esize); match op { @@ -5821,7 +5821,7 @@ val aarch64_integer_conditional_select : (bits(4), int, int, bool, bool, int, in function aarch64_integer_conditional_select (condition, 'd, 'datasize, else_inc, else_inv, 'm, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); @@ -5851,7 +5851,7 @@ val aarch64_integer_conditional_compare_register : (bits(4), int, bits(4), int, function aarch64_integer_conditional_compare_register (condition, 'datasize, flags__arg, 'm, 'n, sub_op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); flags = flags__arg; operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); @@ -5885,7 +5885,7 @@ val aarch64_integer_conditional_compare_immediate : forall ('datasize : Int). function aarch64_integer_conditional_compare_immediate (condition, datasize, flags__arg, imm, 'n, sub_op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); flags = flags__arg; operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = imm; @@ -7856,7 +7856,7 @@ val aarch64_branch_conditional_test : (int, bits(1), int, bits(64), int) -> unit function aarch64_branch_conditional_test ('bit_pos, bit_val, 'datasize, offset, 't) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand : bits('datasize) = aget_X(t); if [operand[bit_pos]] == bit_val then BranchTo(aget_PC() + offset, BranchType_JMP) else () } @@ -7890,7 +7890,7 @@ val aarch64_branch_conditional_compare : (int, bool, bits(64), int) -> unit effe function aarch64_branch_conditional_compare ('datasize, iszero, offset, 't) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand1 : bits('datasize) = aget_X(t); if IsZero(operand1) == iszero then BranchTo(aget_PC() + offset, BranchType_JMP) else () } @@ -8998,7 +8998,7 @@ val aarch64_vector_transfer_vector_table : (int, int, int, bool, int, int, int) function aarch64_vector_transfer_vector_table ('d, 'datasize, 'elements, is_tbl, 'm, n__arg, 'regs) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); assert(constraint('regs >= 1 & 'elements >= 1)); n : int = n__arg; CheckFPAdvSIMDEnabled64(); @@ -9041,7 +9041,7 @@ function aarch64_vector_transfer_vector_permute_zip ('d, 'datasize, 'esize, 'm, assert(constraint('esize >= 0), "esize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -9062,7 +9062,7 @@ function aarch64_vector_transfer_vector_permute_unzip ('d, 'datasize, 'elements, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operandl : bits('datasize) = aget_V(n); operandh : bits('datasize) = aget_V(m); @@ -9080,7 +9080,7 @@ function aarch64_vector_transfer_vector_permute_transpose ('d, 'datasize, 'esize assert(constraint('esize >= 0), "esize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -9109,7 +9109,7 @@ val aarch64_vector_transfer_vector_extract : (int, int, int, int, int) -> unit e function aarch64_vector_transfer_vector_extract ('d, 'datasize, 'm, 'n, 'position) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); hi : bits('datasize) = aget_V(m); lo : bits('datasize) = aget_V(n); @@ -9125,7 +9125,7 @@ function aarch64_vector_transfer_vector_cpydup_sisd ('d, 'datasize, 'elements, ' assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('idxdsize) = aget_V(n); result : bits('datasize) = undefined; @@ -9142,7 +9142,7 @@ function aarch64_vector_transfer_integer_move_unsigned ('d, 'datasize, 'esize, ' assert(constraint('esize >= 0), "esize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('idxdsize) = aget_V(n); aset_X(d, ZeroExtend(aget_Elem(operand, index, esize), datasize)) @@ -9155,7 +9155,7 @@ function aarch64_vector_transfer_integer_move_signed ('d, 'datasize, 'esize, 'id assert(constraint('esize >= 0), "esize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('idxdsize) = aget_V(n); aset_X(d, SignExtend(aget_Elem(operand, index, esize), datasize)) @@ -9167,7 +9167,7 @@ function aarch64_vector_transfer_integer_insert ('d, 'datasize, 'esize, 'index, assert(constraint('esize >= 0), "esize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); element : bits('esize) = aget_X(n); result : bits('datasize) = aget_V(d); @@ -9182,7 +9182,7 @@ function aarch64_vector_transfer_integer_dup ('d, 'datasize, 'elements, 'esize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); element : bits('esize) = aget_X(n); result : bits('datasize) = undefined; @@ -9198,7 +9198,7 @@ function aarch64_vector_shift_right_sisd (accumulate, 'd, 'datasize, 'elements, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); operand2 : bits('datasize) = undefined; @@ -9220,7 +9220,7 @@ function aarch64_vector_shift_rightnarrow_uniform_sisd ('d, 'datasize, 'elements assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits(2 * 'datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9244,7 +9244,7 @@ function aarch64_vector_shift_rightnarrow_nonuniform_sisd ('d, 'datasize, 'eleme assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits(2 * 'datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9268,7 +9268,7 @@ function aarch64_vector_shift_rightnarrow_logical ('d, 'datasize, 'elements, 'es assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits(2 * 'datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9288,7 +9288,7 @@ function aarch64_vector_shift_rightinsert_sisd ('d, 'datasize, 'elements, 'esize assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(d); @@ -9309,7 +9309,7 @@ function aarch64_vector_shift_left_sisd ('d, 'datasize, 'elements, 'esize, 'n, ' assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9325,7 +9325,7 @@ function aarch64_vector_shift_leftsat_sisd ('d, 'datasize, dst_unsigned, 'elemen assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9348,7 +9348,7 @@ function aarch64_vector_shift_leftlong ('d, 'datasize, 'elements, 'esize, 'n, 'p assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_Vpart(n, part); result : bits(2 * 'datasize) = undefined; @@ -9367,7 +9367,7 @@ function aarch64_vector_shift_leftinsert_sisd ('d, 'datasize, 'elements, 'esize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(d); @@ -9388,7 +9388,7 @@ function aarch64_vector_shift_conv_int_sisd ('d, 'datasize, 'elements, 'esize, ' assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9407,7 +9407,7 @@ function aarch64_vector_shift_conv_float_sisd ('d, 'datasize, 'elements, 'esize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9426,7 +9426,7 @@ function aarch64_vector_reduce_intmax ('d, 'datasize, 'elements, 'esize, min, 'n assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); maxmin : int = undefined; @@ -9445,7 +9445,7 @@ function aarch64_vector_reduce_fp16maxnm_sisd ('d, 'datasize, 'esize, 'n, op) = assert(constraint('esize >= 0), "esize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); aset_V(d, Reduce(op, operand, esize)) @@ -9470,7 +9470,7 @@ function aarch64_vector_reduce_fp16maxnm_simd ('d, 'datasize, 'esize, 'n, op) = assert(constraint('esize >= 0), "esize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); aset_V(d, Reduce(op, operand, esize)) @@ -9482,7 +9482,7 @@ function aarch64_vector_reduce_fp16max_sisd ('d, 'datasize, 'esize, 'n, op) = { assert(constraint('esize >= 0), "esize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); aset_V(d, Reduce(op, operand, esize)) @@ -9507,7 +9507,7 @@ function aarch64_vector_reduce_fp16max_simd ('d, 'datasize, 'esize, 'n, op) = { assert(constraint('esize >= 0), "esize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); aset_V(d, Reduce(op, operand, esize)) @@ -9519,7 +9519,7 @@ function aarch64_vector_reduce_fp16add_sisd ('d, 'datasize, 'esize, 'n, op) = { assert(constraint('esize >= 0), "esize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); aset_V(d, Reduce(op, operand, esize)) @@ -9544,7 +9544,7 @@ function aarch64_vector_reduce_add_sisd ('d, 'datasize, 'esize, 'n, op) = { assert(constraint('esize >= 0), "esize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); aset_V(d, Reduce(op, operand, esize)) @@ -9556,7 +9556,7 @@ function aarch64_vector_reduce_add_simd ('d, 'datasize, 'esize, 'n, op) = { assert(constraint('esize >= 0), "esize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); aset_V(d, Reduce(op, operand, esize)) @@ -9569,7 +9569,7 @@ function aarch64_vector_reduce_addlong ('d, 'datasize, 'elements, 'esize, 'n, un assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); sum : int = asl_Int(aget_Elem(operand, 0, esize), unsigned); @@ -9583,7 +9583,7 @@ val aarch64_vector_logical : forall ('datasize : Int). function aarch64_vector_logical (datasize, imm, operation, 'rd) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = undefined; result : bits('datasize) = undefined; @@ -9607,7 +9607,7 @@ val aarch64_vector_fp16_movi : forall ('datasize : Int). function aarch64_vector_fp16_movi (datasize, imm, 'rd) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); aset_V(rd, imm) } @@ -9619,7 +9619,7 @@ function aarch64_vector_arithmetic_unary_special_sqrtfp16 ('d, 'datasize, 'eleme assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9637,7 +9637,7 @@ function aarch64_vector_arithmetic_unary_special_sqrtest_int ('d, 'datasize, 'el assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9656,7 +9656,7 @@ function aarch64_vector_arithmetic_unary_special_sqrtest_fp16_sisd ('d, 'datasiz assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9686,7 +9686,7 @@ function aarch64_vector_arithmetic_unary_special_recip_int ('d, 'datasize, 'elem assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9705,7 +9705,7 @@ function aarch64_vector_arithmetic_unary_special_recip_fp16_sisd ('d, 'datasize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9736,7 +9736,7 @@ function aarch64_vector_arithmetic_unary_special_frecpxfp16 ('d, 'datasize, 'ele assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9767,7 +9767,7 @@ function aarch64_vector_arithmetic_unary_shift ('d, 'datasize, 'elements, 'esize assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_Vpart(n, part); result : bits(2 * 'datasize) = undefined; @@ -9785,7 +9785,7 @@ function aarch64_vector_arithmetic_unary_rev ('containers, 'd, 'datasize, 'eleme assert(constraint('esize >= 0), "esize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9809,7 +9809,7 @@ function aarch64_vector_arithmetic_unary_rbit ('d, 'datasize, 'elements, 'esize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9843,7 +9843,7 @@ function aarch64_vector_arithmetic_unary_not ('d, 'datasize, 'elements, 'esize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9874,7 +9874,7 @@ function aarch64_vector_arithmetic_unary_fp16_round ('d, 'datasize, 'elements, ' assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9893,7 +9893,7 @@ function aarch64_vector_arithmetic_unary_fp16_conv_int_sisd ('d, 'datasize, 'ele assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9926,7 +9926,7 @@ function aarch64_vector_arithmetic_unary_fp16_conv_float_tieaway_sisd ('d, 'data assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9959,7 +9959,7 @@ function aarch64_vector_arithmetic_unary_fp16_conv_float_bulk_sisd ('d, 'datasiz assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -9992,7 +9992,7 @@ function aarch64_vector_arithmetic_unary_float_xtn_sisd ('d, 'datasize, 'element assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits(2 * 'datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -10008,7 +10008,7 @@ function aarch64_vector_arithmetic_unary_float_widen ('d, 'datasize, 'elements, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_Vpart(n, part); result : bits(2 * 'datasize) = undefined; @@ -10037,7 +10037,7 @@ function aarch64_vector_arithmetic_unary_float_narrow ('d, 'datasize, 'elements, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits(2 * 'datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -10066,7 +10066,7 @@ function aarch64_vector_arithmetic_unary_extract_sqxtun_sisd ('d, 'datasize, 'el assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits(2 * 'datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -10089,7 +10089,7 @@ function aarch64_vector_arithmetic_unary_extract_sat_sisd ('d, 'datasize, 'eleme assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits(2 * 'datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -10112,7 +10112,7 @@ function aarch64_vector_arithmetic_unary_extract_nosat ('d, 'datasize, 'elements assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits(2 * 'datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -10131,7 +10131,7 @@ function aarch64_vector_arithmetic_unary_diffneg_sat_sisd ('d, 'datasize, 'eleme assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -10168,7 +10168,7 @@ function aarch64_vector_arithmetic_unary_diffneg_int_sisd ('d, 'datasize, 'eleme assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -10188,7 +10188,7 @@ function aarch64_vector_arithmetic_unary_diffneg_fp16 ('d, 'datasize, 'elements, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -10205,7 +10205,7 @@ val aarch64_vector_arithmetic_unary_cnt : (int, int, int, int, int) -> unit effe function aarch64_vector_arithmetic_unary_cnt ('d, 'datasize, 'elements, 'esize, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); assert('elements >= 1 & 'esize >= 1); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); @@ -10225,7 +10225,7 @@ function aarch64_vector_arithmetic_unary_cmp_int_lessthan_sisd (comparison, 'd, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -10252,7 +10252,7 @@ function aarch64_vector_arithmetic_unary_cmp_int_bulk_sisd (comparison, 'd, 'dat assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -10279,7 +10279,7 @@ function aarch64_vector_arithmetic_unary_cmp_fp16_lessthan_sisd (comparison, 'd, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -10320,7 +10320,7 @@ function aarch64_vector_arithmetic_unary_cmp_fp16_bulk_sisd (comparison, 'd, 'da assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -10364,7 +10364,7 @@ val aarch64_vector_arithmetic_unary_clsz : (CountOp, int, int, int, int, int) -> function aarch64_vector_arithmetic_unary_clsz (countop, 'd, 'datasize, 'elements, 'esize, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); assert('elements >= 1 & 'esize >= 3); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); @@ -10386,7 +10386,7 @@ function aarch64_vector_arithmetic_unary_add_saturating_sisd ('d, 'datasize, 'el assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -10425,7 +10425,7 @@ function aarch64_vector_arithmetic_unary_add_pairwise (acc, 'd, 'datasize, 'elem assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand : bits('datasize) = aget_V(n); result : bits('datasize) = undefined; @@ -10449,7 +10449,7 @@ function aarch64_vector_arithmetic_binary_uniform_sub_saturating_sisd ('d, 'data assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10491,7 +10491,7 @@ function aarch64_vector_arithmetic_binary_uniform_sub_int ('d, 'datasize, 'eleme assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10515,7 +10515,7 @@ function aarch64_vector_arithmetic_binary_uniform_sub_fp16_sisd (abs, 'd, 'datas assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10553,7 +10553,7 @@ function aarch64_vector_arithmetic_binary_uniform_sub_fp16_simd (abs, 'd, 'datas assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10577,7 +10577,7 @@ function aarch64_vector_arithmetic_binary_uniform_shift_sisd ('d, 'datasize, 'el assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10607,7 +10607,7 @@ function aarch64_vector_arithmetic_binary_uniform_rsqrtsfp16_sisd ('d, 'datasize assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10642,7 +10642,7 @@ function aarch64_vector_arithmetic_binary_uniform_recpsfp16_sisd ('d, 'datasize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10674,7 +10674,7 @@ val aarch64_vector_arithmetic_binary_uniform_mul_int_product : (int, int, int, i function aarch64_vector_arithmetic_binary_uniform_mul_int_product ('d, 'datasize, 'elements, 'esize, 'm, 'n, poly) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); assert('elements >= 1 & 'esize >= 1); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); @@ -10700,7 +10700,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_int_doubling_sisd ('d, 'da assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10729,7 +10729,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_int_doubling_accum_sisd (' assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10762,7 +10762,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_int_dotp ('d, 'datasize, ' assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10793,7 +10793,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_int_accum ('d, 'datasize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10818,7 +10818,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_fp16_product ('d, 'datasiz assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10840,7 +10840,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_fp16_fused ('d, 'datasize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10864,7 +10864,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_fp16_extended_sisd ('d, 'd assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10899,7 +10899,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_fp_complex ('d, 'datasize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10949,7 +10949,7 @@ function aarch64_vector_arithmetic_binary_uniform_maxmin_single ('d, 'datasize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10973,7 +10973,7 @@ function aarch64_vector_arithmetic_binary_uniform_maxmin_pair ('d, 'datasize, 'e assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -10998,7 +10998,7 @@ function aarch64_vector_arithmetic_binary_uniform_maxmin_fp16_2008 ('d, 'datasiz assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11026,7 +11026,7 @@ function aarch64_vector_arithmetic_binary_uniform_maxmin_fp16_1985 ('d, 'datasiz assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11051,7 +11051,7 @@ val aarch64_vector_arithmetic_binary_uniform_logical_bsleor : (int, int, int, in function aarch64_vector_arithmetic_binary_uniform_logical_bsleor ('d, 'datasize, 'm, 'n, op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = undefined; operand2 : bits('datasize) = undefined; @@ -11106,7 +11106,7 @@ val aarch64_vector_arithmetic_binary_uniform_logical_andorr : (int, int, bool, i function aarch64_vector_arithmetic_binary_uniform_logical_andorr ('d, 'datasize, invert, 'm, 'n, op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11141,7 +11141,7 @@ function aarch64_vector_arithmetic_binary_uniform_divfp16 ('d, 'datasize, 'eleme assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11163,7 +11163,7 @@ function aarch64_vector_arithmetic_binary_uniform_diff (accumulate, 'd, 'datasiz assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11188,7 +11188,7 @@ function aarch64_vector_arithmetic_binary_uniform_cmp_int_sisd (cmp_eq, 'd, 'dat assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11212,7 +11212,7 @@ function aarch64_vector_arithmetic_binary_uniform_cmp_fp16_sisd (abs, cmp, 'd, ' assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11244,7 +11244,7 @@ function aarch64_vector_arithmetic_binary_uniform_cmp_bitwise_sisd (and_test, 'd assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11268,7 +11268,7 @@ function aarch64_vector_arithmetic_binary_uniform_add_wrapping_single_sisd ('d, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11290,7 +11290,7 @@ function aarch64_vector_arithmetic_binary_uniform_add_wrapping_pair ('d, 'datasi assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11313,7 +11313,7 @@ function aarch64_vector_arithmetic_binary_uniform_add_saturating_sisd ('d, 'data assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11355,7 +11355,7 @@ function aarch64_vector_arithmetic_binary_uniform_add_halving_truncating ('d, 'd assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11379,7 +11379,7 @@ function aarch64_vector_arithmetic_binary_uniform_add_halving_rounding ('d, 'dat assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11401,7 +11401,7 @@ function aarch64_vector_arithmetic_binary_uniform_add_fp16 ('d, 'datasize, 'elem assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11429,7 +11429,7 @@ function aarch64_vector_arithmetic_binary_uniform_add_fp_complex ('d, 'datasize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); @@ -11462,7 +11462,7 @@ function aarch64_vector_arithmetic_binary_element_mul_long ('d, 'datasize, 'elem assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_Vpart(n, part); operand2 : bits('idxdsize) = aget_V(m); @@ -11487,7 +11487,7 @@ function aarch64_vector_arithmetic_binary_element_mul_int ('d, 'datasize, 'eleme assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('idxdsize) = aget_V(m); @@ -11512,7 +11512,7 @@ function aarch64_vector_arithmetic_binary_element_mul_high_sisd ('d, 'datasize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('idxdsize) = aget_V(m); @@ -11542,7 +11542,7 @@ function aarch64_vector_arithmetic_binary_element_mul_fp16_sisd ('d, 'datasize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('idxdsize) = aget_V(m); @@ -11564,7 +11564,7 @@ function aarch64_vector_arithmetic_binary_element_mul_double_sisd ('d, 'datasize assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_Vpart(n, part); operand2 : bits('idxdsize) = aget_V(m); @@ -11591,7 +11591,7 @@ function aarch64_vector_arithmetic_binary_element_mulacc_long ('d, 'datasize, 'e assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_Vpart(n, part); operand2 : bits('idxdsize) = aget_V(m); @@ -11617,7 +11617,7 @@ function aarch64_vector_arithmetic_binary_element_mulacc_int ('d, 'datasize, 'el assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('idxdsize) = aget_V(m); @@ -11643,7 +11643,7 @@ function aarch64_vector_arithmetic_binary_element_mulacc_high_sisd ('d, 'datasiz assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('idxdsize) = aget_V(m); @@ -11677,7 +11677,7 @@ function aarch64_vector_arithmetic_binary_element_mulacc_fp16_sisd ('d, 'datasiz assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('idxdsize) = aget_V(m); @@ -11701,7 +11701,7 @@ function aarch64_vector_arithmetic_binary_element_mulacc_double_sisd ('d, 'datas assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_Vpart(n, part); operand2 : bits('idxdsize) = aget_V(m); @@ -11733,7 +11733,7 @@ function aarch64_vector_arithmetic_binary_element_mulacc_complex ('d, 'datasize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(m); operand2 : bits('datasize) = aget_V(n); @@ -11783,7 +11783,7 @@ function aarch64_vector_arithmetic_binary_element_dotp ('d, 'datasize, 'elements assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits(128) = aget_V(m); @@ -11814,7 +11814,7 @@ function aarch64_vector_arithmetic_binary_disparate_mul_product ('d, 'datasize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_Vpart(n, part); operand2 : bits('datasize) = aget_Vpart(m, part); @@ -11836,7 +11836,7 @@ function aarch64_vector_arithmetic_binary_disparate_mul_poly ('d, 'datasize, 'el assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_Vpart(n, part); operand2 : bits('datasize) = aget_Vpart(m, part); @@ -11858,7 +11858,7 @@ function aarch64_vector_arithmetic_binary_disparate_mul_double_sisd ('d, 'datasi assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_Vpart(n, part); operand2 : bits('datasize) = aget_Vpart(m, part); @@ -11884,7 +11884,7 @@ function aarch64_vector_arithmetic_binary_disparate_mul_dmacc_sisd ('d, 'datasiz assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_Vpart(n, part); operand2 : bits('datasize) = aget_Vpart(m, part); @@ -11916,7 +11916,7 @@ function aarch64_vector_arithmetic_binary_disparate_mul_accum ('d, 'datasize, 'e assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_Vpart(n, part); operand2 : bits('datasize) = aget_Vpart(m, part); @@ -11943,7 +11943,7 @@ function aarch64_vector_arithmetic_binary_disparate_diff (accumulate, 'd, 'datas assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_Vpart(n, part); operand2 : bits('datasize) = aget_Vpart(m, part); @@ -11968,7 +11968,7 @@ function aarch64_vector_arithmetic_binary_disparate_addsub_wide ('d, 'datasize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits(2 * 'datasize) = aget_V(n); operand2 : bits('datasize) = aget_Vpart(m, part); @@ -11992,7 +11992,7 @@ function aarch64_vector_arithmetic_binary_disparate_addsub_narrow ('d, 'datasize assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits(2 * 'datasize) = aget_V(n); operand2 : bits(2 * 'datasize) = aget_V(m); @@ -12018,7 +12018,7 @@ function aarch64_vector_arithmetic_binary_disparate_addsub_long ('d, 'datasize, assert(constraint('elements >= 1), "elements constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_Vpart(n, part); operand2 : bits('datasize) = aget_Vpart(m, part); @@ -12039,7 +12039,7 @@ val aarch64_float_move_fp_select : (bits(4), int, int, int, int) -> unit effect function aarch64_float_move_fp_select (condition, 'd, 'datasize, 'm, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = if ConditionHolds(condition) then aget_V(n) else aget_V(m); aset_V(d, result) @@ -12050,7 +12050,7 @@ val aarch64_float_move_fp_imm : forall ('datasize : Int). function aarch64_float_move_fp_imm ('d, datasize, imm) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); aset_V(d, imm) } @@ -12127,7 +12127,7 @@ val aarch64_float_compare_uncond : (bool, int, int, int, bool) -> unit effect {e function aarch64_float_compare_uncond (cmp_with_zero, 'datasize, 'm, 'n, signal_all_nans) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = if cmp_with_zero then FPZero(0b0) else aget_V(m); @@ -12138,7 +12138,7 @@ val aarch64_float_compare_cond : (bits(4), int, bits(4), int, int, bool) -> unit function aarch64_float_compare_cond (condition, 'datasize, flags__arg, 'm, 'n, signal_all_nans) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); flags = flags__arg; CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); @@ -12151,7 +12151,7 @@ val aarch64_float_arithmetic_unary : (int, int, FPUnaryOp, int) -> unit effect { function aarch64_float_arithmetic_unary ('d, 'datasize, fpop, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = undefined; operand : bits('datasize) = aget_V(n); @@ -12168,7 +12168,7 @@ val aarch64_float_arithmetic_round : (int, int, bool, int, FPRounding) -> unit e function aarch64_float_arithmetic_round ('d, 'datasize, exact, 'n, rounding) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = undefined; operand : bits('datasize) = aget_V(n); @@ -12180,7 +12180,7 @@ val aarch64_float_arithmetic_mul_product : (int, int, int, int, bool) -> unit ef function aarch64_float_arithmetic_mul_product ('d, 'datasize, 'm, 'n, negated) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_V(n); @@ -12194,7 +12194,7 @@ val aarch64_float_arithmetic_mul_addsub : (int, int, int, int, int, bool, bool) function aarch64_float_arithmetic_mul_addsub ('a, 'd, 'datasize, 'm, 'n, op1_neg, opa_neg) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = undefined; operanda : bits('datasize) = aget_V(a); @@ -12210,7 +12210,7 @@ val aarch64_float_arithmetic_maxmin : (int, int, int, int, FPMaxMinOp) -> unit e function aarch64_float_arithmetic_maxmin ('d, 'datasize, 'm, 'n, operation) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_V(n); @@ -12228,7 +12228,7 @@ val aarch64_float_arithmetic_div : (int, int, int, int) -> unit effect {escape, function aarch64_float_arithmetic_div ('d, 'datasize, 'm, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_V(n); @@ -12241,7 +12241,7 @@ val aarch64_float_arithmetic_addsub : (int, int, int, int, bool) -> unit effect function aarch64_float_arithmetic_addsub ('d, 'datasize, 'm, 'n, sub_op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_V(n); @@ -12700,7 +12700,7 @@ function aarch64_memory_vector_single_nowb (datasize, esize, index, m, memop, n, element : bits('esize) = undefined; s : int = undefined; let 'ebytes : {'n, true. atom('n)} = ex_int(esize / 8); - assert(constraint(8 * 'ebytes = 'esize)); + assert(constraint(8 * 'ebytes == 'esize)); if n == 31 then { CheckSPAlignment(); address = aget_SP() @@ -12744,7 +12744,7 @@ function aarch64_memory_vector_multiple_nowb (datasize, elements, esize, m, memo s : int = undefined; tt : int = undefined; let 'ebytes = ex_int(esize / 8); - assert(constraint(8 * 'ebytes = 'esize)); + assert(constraint(8 * 'ebytes == 'esize)); if n == 31 then { CheckSPAlignment(); address = aget_SP() @@ -12774,7 +12774,7 @@ val aarch64_memory_single_simdfp_register : (AccType, int, ExtendType, int, MemO function aarch64_memory_single_simdfp_register (acctype, 'datasize, extend_type, 'm, memop, 'n, postindex, 'shift, 't, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); offset : bits(64) = ExtendReg(m, extend_type, shift); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; @@ -12804,7 +12804,7 @@ val aarch64_memory_single_simdfp_immediate_signed_postidx : (AccType, int, MemOp function aarch64_memory_single_simdfp_immediate_signed_postidx (acctype, 'datasize, memop, 'n, offset, postindex, 't, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -12833,7 +12833,7 @@ val aarch64_memory_single_simdfp_immediate_signed_offset_normal : (AccType, int, function aarch64_memory_single_simdfp_immediate_signed_offset_normal (acctype, 'datasize, memop, 'n, offset, postindex, 't, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -12866,7 +12866,7 @@ function aarch64_memory_ordered (acctype, datasize, memop, n, regsize, t) = { address : bits(64) = undefined; data : bits('datasize) = undefined; let 'dbytes = ex_int(datasize / 8); - assert(constraint(8 * 'dbytes = 'datasize)); + assert(constraint(8 * 'dbytes == 'datasize)); if n == 31 then { CheckSPAlignment(); address = aget_SP() @@ -12907,7 +12907,7 @@ function aarch64_memory_orderedrcpc (acctype, datasize, n, regsize, t) = { address : bits(64) = undefined; data : bits('datasize) = undefined; let 'dbytes = ex_int(datasize / 8); - assert(constraint(8 * 'dbytes = 'datasize)); + assert(constraint(8 * 'dbytes == 'datasize)); if n == 31 then { CheckSPAlignment(); address = aget_SP() @@ -12986,7 +12986,7 @@ function aarch64_memory_atomicops_swp ('datasize, ldacctype, 'n, 'regsize, 's, s assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; data : bits('datasize) = undefined; if n == 31 then { @@ -13002,7 +13002,7 @@ val aarch64_memory_atomicops_st : (int, AccType, int, MemAtomicOp, int, AccType) function aarch64_memory_atomicops_st ('datasize, ldacctype, 'n, op, 's, stacctype) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; value_name : bits('datasize) = undefined; data : bits('datasize) = undefined; @@ -13032,7 +13032,7 @@ function aarch64_memory_atomicops_ld ('datasize, ldacctype, 'n, op, 'regsize, 's assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; value_name : bits('datasize) = undefined; data : bits('datasize) = undefined; @@ -13063,7 +13063,7 @@ function aarch64_memory_atomicops_cas_single ('datasize, ldacctype, 'n, 'regsize assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; comparevalue : bits('datasize) = undefined; newvalue : bits('datasize) = undefined; @@ -13085,7 +13085,7 @@ function aarch64_memory_atomicops_cas_pair ('datasize, ldacctype, 'n, 'regsize, assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; comparevalue : bits(2 * 'datasize) = undefined; newvalue : bits(2 * 'datasize) = undefined; @@ -13366,7 +13366,7 @@ function aarch64_memory_single_general_register (acctype, 'datasize, extend_type assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); wback = wback__arg; offset : bits(64) = ExtendReg(m, extend_type, shift); address : bits(64) = undefined; @@ -13422,7 +13422,7 @@ function aarch64_memory_single_general_immediate_unsigned (acctype, 'datasize, m assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); wback = wback__arg; address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -13477,7 +13477,7 @@ function aarch64_memory_single_general_immediate_signed_postidx (acctype, 'datas assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); wback = wback__arg; address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -13564,7 +13564,7 @@ function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype, assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); wback = wback__arg; address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -13619,7 +13619,7 @@ function aarch64_memory_single_general_immediate_signed_offset_normal (acctype, assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); wback = wback__arg; address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -13673,7 +13673,7 @@ val aarch64_memory_pair_simdfp_postidx : forall ('datasize : Int). function aarch64_memory_pair_simdfp_postidx (acctype, datasize, memop, n, offset, postindex, t, t2, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; data1 : bits('datasize) = undefined; @@ -13724,7 +13724,7 @@ val aarch64_memory_pair_simdfp_noalloc : forall ('datasize : Int). function aarch64_memory_pair_simdfp_noalloc (acctype, datasize, memop, n, offset, postindex, t, t2, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; data1 : bits('datasize) = undefined; @@ -13775,7 +13775,7 @@ val aarch64_memory_pair_general_postidx : forall ('datasize : Int). function aarch64_memory_pair_general_postidx (acctype, datasize, memop, n, offset, postindex, signed, t, t2, wback__arg) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); wback = wback__arg; address : bits(64) = undefined; data1 : bits('datasize) = undefined; @@ -13855,7 +13855,7 @@ val aarch64_memory_pair_general_noalloc : forall ('datasize : Int). function aarch64_memory_pair_general_noalloc (acctype, datasize, memop, n, offset, postindex, t, t2, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; data1 : bits('datasize) = undefined; data2 : bits('datasize) = undefined; @@ -13910,7 +13910,7 @@ function aarch64_memory_exclusive_single (acctype, datasize, elsize, memop, n, p let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); assert(constraint(- 'elsize + 'datasize >= 0 & 'elsize >= 0)); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; data : bits('datasize) = undefined; rt_unknown : bool = false; @@ -13957,7 +13957,7 @@ function aarch64_memory_exclusive_single (acctype, datasize, elsize, memop, n, p MemOp_STORE => { if rt_unknown then data = undefined else if pair then let 'v = ex_int(datasize / 2) in { - assert(constraint(2 * 'v = 'datasize)); + assert(constraint(2 * 'v == 'datasize)); el1 : bits('v) = aget_X(t); el2 : bits('v) = aget_X(t2); data = if BigEndian() then el1 @ el2 else el2 @ el1 @@ -14023,7 +14023,7 @@ function aarch64_memory_exclusive_pair (acctype, datasize, elsize, memop, n, pai let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); assert(constraint(- 'elsize + 'datasize >= 0 & 'elsize >= 0), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; data : bits('datasize) = undefined; rt_unknown : bool = false; @@ -14070,7 +14070,7 @@ function aarch64_memory_exclusive_pair (acctype, datasize, elsize, memop, n, pai MemOp_STORE => { if rt_unknown then data = undefined else if pair then let 'v = ex_int(datasize / 2) in { - assert(constraint(2 * 'v = 'datasize)); + assert(constraint(2 * 'v == 'datasize)); el1 : bits('v) = aget_X(t); el2 : bits('v) = aget_X(t2); data = if BigEndian() then el1 @ el2 else el2 @ el1 @@ -14305,7 +14305,7 @@ function vector_logical_decode (Q, op, a, b, c, cmode, o2, d, e, f, g, h, Rd) = }; imm64 = AdvSIMDExpandImm(op, cmode, ((((((a @ b) @ c) @ d) @ e) @ f) @ g) @ h); let 'immsize = datasize / 64; - assert(constraint('immsize * 64 = 'datasize)); + assert(constraint('immsize * 64 == 'datasize)); imm = replicate_bits(imm64, 'immsize); aarch64_vector_logical(datasize, imm, operation, rd) } @@ -14321,7 +14321,7 @@ function vector_fp16_movi_decode (Q, op, a, b, c, cmode, o2, d, e, f, g, h, Rd) imm8 : bits(8) = ((((((a @ b) @ c) @ d) @ e) @ f) @ g) @ h; imm16 : bits(16) = ((([imm8[7]] @ ~([imm8[6]])) @ replicate_bits([imm8[6]], 2)) @ slice(imm8, 0, 6)) @ Zeros(6); let 'immsize = datasize / 16; - assert(constraint('immsize * 16 = 'datasize)); + assert(constraint('immsize * 16 == 'datasize)); imm = replicate_bits(imm16, immsize); aarch64_vector_fp16_movi(datasize, imm, rd) } diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail index 8710e66b..610884a4 100644 --- a/aarch64/no_vector/spec.sail +++ b/aarch64/no_vector/spec.sail @@ -1949,7 +1949,7 @@ val BigEndianReverse : forall ('width : Int), 'width >= 0 & 'width >= 0. function BigEndianReverse value_name = { assert('width == 8 | 'width == 16 | 'width == 32 | 'width == 64 | 'width == 128); let 'half = 'width / 2; - assert(constraint('half * 2 = 'width)); + assert(constraint('half * 2 == 'width)); if 'width == 8 then return(value_name) else (); return(BigEndianReverse(slice(value_name, 0, half)) @ BigEndianReverse(slice(value_name, half, 'width - half))) } @@ -2065,7 +2065,7 @@ val Replicate : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0. function Replicate x = { assert('N % 'M == 0, "((N MOD M) == 0)"); let 'O = 'N / 'M; - assert(constraint('O * 'M = 'N)); + assert(constraint('O * 'M == 'N)); return(replicate_bits(x, 'N / 'M)) } @@ -2721,7 +2721,7 @@ val aarch64_integer_insext_insert_movewide : (int, int, bits(16), MoveWideOp, in function aarch64_integer_insext_insert_movewide ('d, 'datasize, imm, opcode, 'pos) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; if opcode == MoveWideOp_K then result = aget_X(d) else result = Zeros(); result = __SetSlice_bits(datasize, 16, result, pos, imm); @@ -2733,7 +2733,7 @@ val aarch64_integer_insext_extract_immediate : (int, int, int, int, int) -> unit function aarch64_integer_insext_extract_immediate ('d, 'datasize, 'lsb, 'm, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); @@ -2746,7 +2746,7 @@ val aarch64_integer_arithmetic_rev : (int, int, int, int) -> unit effect {escape function aarch64_integer_arithmetic_rev ('container_size, 'd, 'datasize, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand : bits('datasize) = aget_X(n); result : bits('datasize) = undefined; containers : int = datasize / container_size; @@ -2768,7 +2768,7 @@ val aarch64_integer_arithmetic_rbit : (int, int, int) -> unit effect {escape, rr function aarch64_integer_arithmetic_rbit ('d, 'datasize, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand : bits('datasize) = aget_X(n); result : bits('datasize) = undefined; foreach (i from 0 to (datasize - 1) by 1 in inc) @@ -2790,7 +2790,7 @@ val aarch64_integer_arithmetic_mul_widening_64128hi : (int, int, int, int, bool) function aarch64_integer_arithmetic_mul_widening_64128hi ('d, 'datasize, 'm, 'n, unsigned) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); result : int = asl_Int(operand1, unsigned) * asl_Int(operand2, unsigned); @@ -2817,7 +2817,7 @@ function aarch64_integer_arithmetic_mul_widening_3264 ('a, 'd, 'datasize, 'dests assert(constraint('destsize in {32, 64}), "destsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); operand3 : bits('destsize) = aget_X(a); @@ -2847,7 +2847,7 @@ function aarch64_integer_arithmetic_mul_uniform_addsub ('a, 'd, 'datasize, 'dest assert(constraint('destsize in {32, 64}), "destsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); operand3 : bits('destsize) = aget_X(a); @@ -2874,7 +2874,7 @@ val aarch64_integer_arithmetic_div : (int, int, int, int, bool) -> unit effect { function aarch64_integer_arithmetic_div ('d, 'datasize, 'm, 'n, unsigned) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); result : int = undefined; @@ -2898,7 +2898,7 @@ val aarch64_integer_arithmetic_cnt : (int, int, int, CountOp) -> unit effect {es function aarch64_integer_arithmetic_cnt ('d, 'datasize, 'n, opcode) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : int = undefined; operand1 : bits('datasize) = aget_X(n); if opcode == CountOp_CLZ then result = CountLeadingZeroBits(operand1) else result = CountLeadingSignBits(operand1); @@ -2920,7 +2920,7 @@ val aarch64_integer_arithmetic_addsub_carry : (int, int, int, int, bool, bool) - function aarch64_integer_arithmetic_addsub_carry ('d, 'datasize, 'm, 'n, setflags, sub_op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); @@ -3042,7 +3042,7 @@ val aarch64_integer_bitfield : forall ('datasize : Int). function aarch64_integer_bitfield ('R, 'S, 'd, datasize, extend, inzero, 'n, tmask, wmask) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); dst : bits('datasize) = if inzero then Zeros() else aget_X(d); src : bits('datasize) = aget_X(n); bot : bits('datasize) = dst & ~(wmask) | ROR(src, R) & wmask; @@ -3068,7 +3068,7 @@ val aarch64_integer_shift_variable : (int, int, int, int, ShiftType) -> unit eff function aarch64_integer_shift_variable ('d, 'datasize, 'm, 'n, shift_type) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand2 : bits('datasize) = aget_X(m); result = ShiftReg(n, shift_type, UInt(operand2) % datasize); @@ -3091,7 +3091,7 @@ val aarch64_integer_logical_shiftedreg : (int, int, bool, int, int, LogicalOp, b function aarch64_integer_logical_shiftedreg ('d, 'datasize, invert, 'm, 'n, op, setflags, 'shift_amount, shift_type) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = ShiftReg(m, shift_type, shift_amount); if invert then operand2 = ~(operand2) else (); @@ -3109,7 +3109,7 @@ val aarch64_integer_arithmetic_addsub_shiftedreg : (int, int, int, int, bool, in function aarch64_integer_arithmetic_addsub_shiftedreg ('d, 'datasize, 'm, 'n, setflags, 'shift_amount, shift_type, sub_op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = ShiftReg(m, shift_type, shift_amount); @@ -3244,7 +3244,7 @@ val aarch64_integer_logical_immediate : forall ('datasize : Int). function aarch64_integer_logical_immediate ('d, datasize, imm, 'n, op, setflags) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = imm; @@ -3262,7 +3262,7 @@ val aarch64_integer_arithmetic_addsub_immediate : forall ('datasize : Int). function aarch64_integer_arithmetic_addsub_immediate ('d, datasize, imm, 'n, setflags, sub_op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand1 : bits('datasize) = if n == 31 then aget_SP() else aget_X(n); operand2 : bits('datasize) = imm; @@ -3281,7 +3281,7 @@ val aarch64_integer_arithmetic_addsub_extendedreg : (int, int, ExtendType, int, function aarch64_integer_arithmetic_addsub_extendedreg ('d, 'datasize, extend_type, 'm, 'n, setflags, 'shift, sub_op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand1 : bits('datasize) = if n == 31 then aget_SP() else aget_X(n); operand2 : bits('datasize) = ExtendReg(m, extend_type, shift); @@ -4871,7 +4871,7 @@ val aarch64_integer_conditional_select : (bits(4), int, int, bool, bool, int, in function aarch64_integer_conditional_select (condition, 'd, 'datasize, else_inc, else_inv, 'm, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); @@ -4901,7 +4901,7 @@ val aarch64_integer_conditional_compare_register : (bits(4), int, bits(4), int, function aarch64_integer_conditional_compare_register (condition, 'datasize, flags__arg, 'm, 'n, sub_op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); flags = flags__arg; operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = aget_X(m); @@ -4935,7 +4935,7 @@ val aarch64_integer_conditional_compare_immediate : forall ('datasize : Int). function aarch64_integer_conditional_compare_immediate (condition, datasize, flags__arg, imm, 'n, sub_op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); flags = flags__arg; operand1 : bits('datasize) = aget_X(n); operand2 : bits('datasize) = imm; @@ -6906,7 +6906,7 @@ val aarch64_branch_conditional_test : (int, bits(1), int, bits(64), int) -> unit function aarch64_branch_conditional_test ('bit_pos, bit_val, 'datasize, offset, 't) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand : bits('datasize) = aget_X(t); if [operand[bit_pos]] == bit_val then BranchTo(aget_PC() + offset, BranchType_JMP) else () } @@ -6940,7 +6940,7 @@ val aarch64_branch_conditional_compare : (int, bool, bits(64), int) -> unit effe function aarch64_branch_conditional_compare ('datasize, iszero, offset, 't) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); operand1 : bits('datasize) = aget_X(t); if IsZero(operand1) == iszero then BranchTo(aget_PC() + offset, BranchType_JMP) else () } @@ -8048,7 +8048,7 @@ val aarch64_float_move_fp_select : (bits(4), int, int, int, int) -> unit effect function aarch64_float_move_fp_select (condition, 'd, 'datasize, 'm, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = if ConditionHolds(condition) then aget_V(n) else aget_V(m); aset_V(d, result) @@ -8059,7 +8059,7 @@ val aarch64_float_move_fp_imm : forall ('datasize : Int). function aarch64_float_move_fp_imm ('d, datasize, imm) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); aset_V(d, imm) } @@ -8136,7 +8136,7 @@ val aarch64_float_compare_uncond : (bool, int, int, int, bool) -> unit effect {e function aarch64_float_compare_uncond (cmp_with_zero, 'datasize, 'm, 'n, signal_all_nans) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = if cmp_with_zero then FPZero(0b0) else aget_V(m); @@ -8147,7 +8147,7 @@ val aarch64_float_compare_cond : (bits(4), int, bits(4), int, int, bool) -> unit function aarch64_float_compare_cond (condition, 'datasize, flags__arg, 'm, 'n, signal_all_nans) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); flags = flags__arg; CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); @@ -8160,7 +8160,7 @@ val aarch64_float_arithmetic_unary : (int, int, FPUnaryOp, int) -> unit effect { function aarch64_float_arithmetic_unary ('d, 'datasize, fpop, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = undefined; operand : bits('datasize) = aget_V(n); @@ -8177,7 +8177,7 @@ val aarch64_float_arithmetic_round : (int, int, bool, int, FPRounding) -> unit e function aarch64_float_arithmetic_round ('d, 'datasize, exact, 'n, rounding) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = undefined; operand : bits('datasize) = aget_V(n); @@ -8189,7 +8189,7 @@ val aarch64_float_arithmetic_mul_product : (int, int, int, int, bool) -> unit ef function aarch64_float_arithmetic_mul_product ('d, 'datasize, 'm, 'n, negated) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_V(n); @@ -8203,7 +8203,7 @@ val aarch64_float_arithmetic_mul_addsub : (int, int, int, int, int, bool, bool) function aarch64_float_arithmetic_mul_addsub ('a, 'd, 'datasize, 'm, 'n, op1_neg, opa_neg) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = undefined; operanda : bits('datasize) = aget_V(a); @@ -8219,7 +8219,7 @@ val aarch64_float_arithmetic_maxmin : (int, int, int, int, FPMaxMinOp) -> unit e function aarch64_float_arithmetic_maxmin ('d, 'datasize, 'm, 'n, operation) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_V(n); @@ -8237,7 +8237,7 @@ val aarch64_float_arithmetic_div : (int, int, int, int) -> unit effect {escape, function aarch64_float_arithmetic_div ('d, 'datasize, 'm, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_V(n); @@ -8250,7 +8250,7 @@ val aarch64_float_arithmetic_addsub : (int, int, int, int, bool) -> unit effect function aarch64_float_arithmetic_addsub ('d, 'datasize, 'm, 'n, sub_op) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); result : bits('datasize) = undefined; operand1 : bits('datasize) = aget_V(n); @@ -8535,7 +8535,7 @@ function aarch64_memory_vector_single_nowb (datasize, esize, index, m, memop, n, element : bits('esize) = undefined; s : int = undefined; let 'ebytes : {'n, true. atom('n)} = ex_int(esize / 8); - assert(constraint(8 * 'ebytes = 'esize)); + assert(constraint(8 * 'ebytes == 'esize)); if n == 31 then { CheckSPAlignment(); address = aget_SP() @@ -8579,7 +8579,7 @@ function aarch64_memory_vector_multiple_nowb (datasize, elements, esize, m, memo s : int = undefined; tt : int = undefined; let 'ebytes = ex_int(esize / 8); - assert(constraint(8 * 'ebytes = 'esize)); + assert(constraint(8 * 'ebytes == 'esize)); if n == 31 then { CheckSPAlignment(); address = aget_SP() @@ -8609,7 +8609,7 @@ val aarch64_memory_single_simdfp_register : (AccType, int, ExtendType, int, MemO function aarch64_memory_single_simdfp_register (acctype, 'datasize, extend_type, 'm, memop, 'n, postindex, 'shift, 't, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); offset : bits(64) = ExtendReg(m, extend_type, shift); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; @@ -8639,7 +8639,7 @@ val aarch64_memory_single_simdfp_immediate_signed_postidx : (AccType, int, MemOp function aarch64_memory_single_simdfp_immediate_signed_postidx (acctype, 'datasize, memop, 'n, offset, postindex, 't, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -8668,7 +8668,7 @@ val aarch64_memory_single_simdfp_immediate_signed_offset_normal : (AccType, int, function aarch64_memory_single_simdfp_immediate_signed_offset_normal (acctype, 'datasize, memop, 'n, offset, postindex, 't, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -8701,7 +8701,7 @@ function aarch64_memory_ordered (acctype, datasize, memop, n, regsize, t) = { address : bits(64) = undefined; data : bits('datasize) = undefined; let 'dbytes = ex_int(datasize / 8); - assert(constraint(8 * 'dbytes = 'datasize)); + assert(constraint(8 * 'dbytes == 'datasize)); if n == 31 then { CheckSPAlignment(); address = aget_SP() @@ -8742,7 +8742,7 @@ function aarch64_memory_orderedrcpc (acctype, datasize, n, regsize, t) = { address : bits(64) = undefined; data : bits('datasize) = undefined; let 'dbytes = ex_int(datasize / 8); - assert(constraint(8 * 'dbytes = 'datasize)); + assert(constraint(8 * 'dbytes == 'datasize)); if n == 31 then { CheckSPAlignment(); address = aget_SP() @@ -8821,7 +8821,7 @@ function aarch64_memory_atomicops_swp ('datasize, ldacctype, 'n, 'regsize, 's, s assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; data : bits('datasize) = undefined; if n == 31 then { @@ -8837,7 +8837,7 @@ val aarch64_memory_atomicops_st : (int, AccType, int, MemAtomicOp, int, AccType) function aarch64_memory_atomicops_st ('datasize, ldacctype, 'n, op, 's, stacctype) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; value_name : bits('datasize) = undefined; data : bits('datasize) = undefined; @@ -8867,7 +8867,7 @@ function aarch64_memory_atomicops_ld ('datasize, ldacctype, 'n, op, 'regsize, 's assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; value_name : bits('datasize) = undefined; data : bits('datasize) = undefined; @@ -8898,7 +8898,7 @@ function aarch64_memory_atomicops_cas_single ('datasize, ldacctype, 'n, 'regsize assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; comparevalue : bits('datasize) = undefined; newvalue : bits('datasize) = undefined; @@ -8920,7 +8920,7 @@ function aarch64_memory_atomicops_cas_pair ('datasize, ldacctype, 'n, 'regsize, assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; comparevalue : bits(2 * 'datasize) = undefined; newvalue : bits(2 * 'datasize) = undefined; @@ -9201,7 +9201,7 @@ function aarch64_memory_single_general_register (acctype, 'datasize, extend_type assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); wback = wback__arg; offset : bits(64) = ExtendReg(m, extend_type, shift); address : bits(64) = undefined; @@ -9257,7 +9257,7 @@ function aarch64_memory_single_general_immediate_unsigned (acctype, 'datasize, m assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); wback = wback__arg; address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -9312,7 +9312,7 @@ function aarch64_memory_single_general_immediate_signed_postidx (acctype, 'datas assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); wback = wback__arg; address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -9399,7 +9399,7 @@ function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype, assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); wback = wback__arg; address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -9454,7 +9454,7 @@ function aarch64_memory_single_general_immediate_signed_offset_normal (acctype, assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); wback = wback__arg; address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -9508,7 +9508,7 @@ val aarch64_memory_pair_simdfp_postidx : forall ('datasize : Int). function aarch64_memory_pair_simdfp_postidx (acctype, datasize, memop, n, offset, postindex, t, t2, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; data1 : bits('datasize) = undefined; @@ -9559,7 +9559,7 @@ val aarch64_memory_pair_simdfp_noalloc : forall ('datasize : Int). function aarch64_memory_pair_simdfp_noalloc (acctype, datasize, memop, n, offset, postindex, t, t2, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; data1 : bits('datasize) = undefined; @@ -9610,7 +9610,7 @@ val aarch64_memory_pair_general_postidx : forall ('datasize : Int). function aarch64_memory_pair_general_postidx (acctype, datasize, memop, n, offset, postindex, signed, t, t2, wback__arg) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); wback = wback__arg; address : bits(64) = undefined; data1 : bits('datasize) = undefined; @@ -9690,7 +9690,7 @@ val aarch64_memory_pair_general_noalloc : forall ('datasize : Int). function aarch64_memory_pair_general_noalloc (acctype, datasize, memop, n, offset, postindex, t, t2, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; data1 : bits('datasize) = undefined; data2 : bits('datasize) = undefined; @@ -9745,7 +9745,7 @@ function aarch64_memory_exclusive_single (acctype, datasize, elsize, memop, n, p let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); assert(constraint(- 'elsize + 'datasize >= 0 & 'elsize >= 0)); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; data : bits('datasize) = undefined; rt_unknown : bool = false; @@ -9792,7 +9792,7 @@ function aarch64_memory_exclusive_single (acctype, datasize, elsize, memop, n, p MemOp_STORE => { if rt_unknown then data = undefined else if pair then let 'v = ex_int(datasize / 2) in { - assert(constraint(2 * 'v = 'datasize)); + assert(constraint(2 * 'v == 'datasize)); el1 : bits('v) = aget_X(t); el2 : bits('v) = aget_X(t2); data = if BigEndian() then el1 @ el2 else el2 @ el1 @@ -9858,7 +9858,7 @@ function aarch64_memory_exclusive_pair (acctype, datasize, elsize, memop, n, pai let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); assert(constraint(- 'elsize + 'datasize >= 0 & 'elsize >= 0), "datasize constraint"); - assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint"); address : bits(64) = undefined; data : bits('datasize) = undefined; rt_unknown : bool = false; @@ -9905,7 +9905,7 @@ function aarch64_memory_exclusive_pair (acctype, datasize, elsize, memop, n, pai MemOp_STORE => { if rt_unknown then data = undefined else if pair then let 'v = ex_int(datasize / 2) in { - assert(constraint(2 * 'v = 'datasize)); + assert(constraint(2 * 'v == 'datasize)); el1 : bits('v) = aget_X(t); el2 : bits('v) = aget_X(t2); data = if BigEndian() then el1 @ el2 else el2 @ el1 diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el index eee0986f..e0081fb6 100644 --- a/editors/sail2-mode.el +++ b/editors/sail2-mode.el @@ -30,6 +30,7 @@ (,(regexp-opt sail2-types 'symbols) . font-lock-type-face) (,(regexp-opt sail2-special 'symbols) . font-lock-preprocessor-face) ("~" . font-lock-negation-char-face) + ("\\(::\\)<" 1 font-lock-keyword-face) ("@" . font-lock-preprocessor-face) ("<->" . font-lock-negation-char-face) ("\'[a-zA-Z0-9_]+" . font-lock-variable-name-face) diff --git a/lib/arith.sail b/lib/arith.sail index db011f14..a3a80fc5 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -58,13 +58,13 @@ let elsize = shl_int(8, UInt(size)) THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}` */ val _shl8 = {c: "shl_mach_int", _: "shl_int"} : - forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> int('m) with 'm in {8, 16, 32, 64} + forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> {'m, 'm in {8, 16, 32, 64}. int('m)} /*! Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}` */ val _shl32 = {c: "shl_mach_int", _: "shl_int"} : - forall 'n, 'n in {0, 1}. (int(32), int('n)) -> int('m) with 'm in {32, 64} + forall 'n, 'n in {0, 1}. (int(32), int('n)) -> {'m, 'm in {32, 64}. int('m)} val _shl_int = "shl_int" : (int, int) -> int diff --git a/lib/option.sail b/lib/option.sail index 3869167b..514cf7ba 100644 --- a/lib/option.sail +++ b/lib/option.sail @@ -6,7 +6,7 @@ $define _OPTION // this won't work - also no other type should be created with // constructors named Some or None. -union option ('a : Type) = { +union option('a: Type) = { Some : 'a, None : unit } diff --git a/src/c_backend.ml b/src/c_backend.ml index 326f742a..2f57a802 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -496,6 +496,9 @@ let analyze_primop' ctx id args typ = (* Optimized routines for all combinations of fixed and small bits appends, where the result is guaranteed to be smaller than 64. *) + | "append", [AV_C_fragment (vec1, _, CT_fbits (0, ord1)); AV_C_fragment (vec2, _, CT_fbits (n2, ord2)) as v2] + when ord1 = ord2 -> + AE_val v2 | "append", [AV_C_fragment (vec1, _, CT_fbits (n1, ord1)); AV_C_fragment (vec2, _, CT_fbits (n2, ord2))] when ord1 = ord2 && n1 + n2 <= 64 -> AE_val (AV_C_fragment (F_op (F_op (vec1, "<<", v_int n2), "|", vec2), typ, CT_fbits (n1 + n2, ord1))) diff --git a/src/lexer.mll b/src/lexer.mll index f5a982eb..a1f3ace2 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -217,6 +217,7 @@ rule token = parse | "@" { (At "@") } | "2" ws "^" { TwoCaret } | "^" { (Caret(r"^")) } + | "::<" { ColonColonLt } | "::" { ColonColon(r "::") } (* | "^^" { CaretCaret(r "^^") } *) | "~~" { TildeTilde(r "~~") } diff --git a/src/parser.mly b/src/parser.mly index fec38669..8287060c 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -133,6 +133,8 @@ let mk_tannot typq typ n m = Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ), l let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown) let mk_namesectn = Name_sect_aux(Name_sect_none,Unknown) +let mk_typq kopts nc n m = TypQ_aux (TypQ_tq (List.map qi_id_of_kopt kopts @ nc), loc n m) + type lchain = LC_lt | LC_lteq @@ -171,6 +173,8 @@ let rec desugar_rchain chain s e = mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e | _ -> assert false +let future_syntax l = Util.warn (Reporting.loc_to_string l ^ "\n\nThis syntax is currently experimental") + %} /*Terminals with no content*/ @@ -185,7 +189,7 @@ let rec desugar_rchain chain s e = %nonassoc Then %nonassoc Else -%token Bar Comma Dot Eof Minus Semi Under DotDot +%token Bar Comma Dot Eof Minus Semi Under DotDot ColonColonLt %token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar LsquareBar RsquareBar %token MinusGt Bidir LtMinus @@ -196,7 +200,7 @@ let rec desugar_rchain chain s e = %token <string> String Bin Hex Real %token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit -%token <string> Colon ColonColon (* CaretCaret *) TildeTilde ExclEq +%token <string> Colon ColonColon TildeTilde ExclEq %token <string> EqEq %token <string> GtEq %token <string> LtEq @@ -339,9 +343,6 @@ atomic_nc: { mk_nc NC_true $startpos $endpos } | False { mk_nc NC_false $startpos $endpos } - | typ0 Eq typ0 - { Util.warn ("Deprecated syntax, use == instead at " ^ Reporting.loc_to_string (loc $startpos($2) $endpos($2)) ^ "\n"); - mk_nc (NC_equal ($1, $3)) $startpos $endpos } | typ0 EqEq typ0 { mk_nc (NC_equal ($1, $3)) $startpos $endpos } | typ0 ExclEq typ0 @@ -355,38 +356,6 @@ atomic_nc: | kid In Lcurly num_list Rcurly { mk_nc (NC_set ($1, $4)) $startpos $endpos } -new_nc: - | new_nc Bar new_nc_and - { mk_nc (NC_or ($1, $3)) $startpos $endpos } - | nc_and - { $1 } - -new_nc_and: - | new_nc_and Amp new_atomic_nc - { mk_nc (NC_and ($1, $3)) $startpos $endpos } - | new_atomic_nc - { $1 } - -new_atomic_nc: - | Where id Lparen typ_list Rparen - { mk_nc (NC_app ($2, $4)) $startpos $endpos } - | True - { mk_nc NC_true $startpos $endpos } - | False - { mk_nc NC_false $startpos $endpos } - | typ0 EqEq typ0 - { mk_nc (NC_equal ($1, $3)) $startpos $endpos } - | typ0 ExclEq typ0 - { mk_nc (NC_not_equal ($1, $3)) $startpos $endpos } - | nc_lchain - { desugar_lchain $1 $startpos $endpos } - | nc_rchain - { desugar_rchain $1 $startpos $endpos } - | Lparen new_nc Rparen - { $2 } - | kid In Lcurly num_list Rcurly - { mk_nc (NC_set ($1, $4)) $startpos $endpos } - num_list: | Num { [$1] } @@ -413,11 +382,17 @@ nc_rchain: | typ0 Gt nc_rchain { RC_nexp $1 :: RC_gt :: $3 } +tyarg: + | ColonColonLt typ_list Gt + { future_syntax (loc $startpos($1) $endpos($3)); $2, [] } + | Lparen typ_list Rparen + { [], $2 } + | ColonColonLt typ_list Gt Lparen typ_list Rparen + { future_syntax (loc $startpos($1) $endpos($3)); $2, $5 } + typ: | typ0 { $1 } - | typ0 With new_nc - { mk_typ (ATyp_with ($1, $3)) $startpos $endpos } /* The following implements all nine levels of user-defined precedence for operators in types, with both left, right and non-associative operators */ @@ -587,8 +562,8 @@ atomic_typ: { mk_typ ATyp_dec $startpos $endpos } | Inc { mk_typ ATyp_inc $startpos $endpos } - | id Lparen typ_list Rparen - { mk_typ (ATyp_app ($1, $3)) $startpos $endpos } + | id tyarg + { mk_typ (ATyp_app ($1, snd $2 @ fst $2)) $startpos $endpos } | Register Lparen typ Rparen { let register_id = mk_id (Id "register") $startpos($1) $endpos($1) in mk_typ (ATyp_app (register_id, [$3])) $startpos $endpos } @@ -1193,14 +1168,43 @@ r_def_body: | r_id_def Comma r_def_body { $1 :: $3 } +param_kopt: + | kid Colon kind + { KOpt_aux (KOpt_kind ($3, $1), loc $startpos $endpos) } + | kid + { KOpt_aux (KOpt_none $1, loc $startpos $endpos) } + +param_kopt_list: + | param_kopt + { [$1] } + | param_kopt Comma param_kopt_list + { $1 :: $3 } + +typaram: + | ColonColonLt param_kopt_list Gt Lparen param_kopt_list Rparen Comma nc + { future_syntax (loc $startpos($1) $endpos($3)); + let qi_nc = QI_aux (QI_const $8, loc $startpos($8) $endpos($8)) in + mk_typq ($5 @ $2) [qi_nc] $startpos $endpos } + | ColonColonLt param_kopt_list Gt Lparen param_kopt_list Rparen + { future_syntax (loc $startpos($1) $endpos($3)); + mk_typq ($5 @ $2) [] $startpos $endpos } + | ColonColonLt param_kopt_list Gt + { future_syntax (loc $startpos($1) $endpos($3)); + mk_typq $2 [] $startpos $endpos } + | Lparen param_kopt_list Rparen Comma nc + { let qi_nc = QI_aux (QI_const $5, loc $startpos($5) $endpos($5)) in + mk_typq $2 [qi_nc] $startpos $endpos } + | Lparen param_kopt_list Rparen + { mk_typq $2 [] $startpos $endpos } + type_def: - | Typedef id typquant Eq typ + | Typedef id typaram Eq typ { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm $3 $5 $startpos($3) $endpos)) $startpos $endpos } | Typedef id Eq typ { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm mk_typqn $4 $startpos($4) $endpos)) $startpos $endpos } | Struct id Eq Lcurly struct_fields Rcurly { mk_td (TD_record ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos } - | Struct id typquant Eq Lcurly struct_fields Rcurly + | Struct id typaram Eq Lcurly struct_fields Rcurly { mk_td (TD_record ($2, mk_namesectn, $3, $6, false)) $startpos $endpos } | Enum id Eq enum_bar { mk_td (TD_enum ($2, mk_namesectn, $4, false)) $startpos $endpos } @@ -1208,11 +1212,11 @@ type_def: { mk_td (TD_enum ($2, mk_namesectn, $5, false)) $startpos $endpos } | Newtype id Eq type_union { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), [$4], false)) $startpos $endpos } - | Newtype id typquant Eq type_union + | Newtype id typaram Eq type_union { mk_td (TD_variant ($2, mk_namesectn, $3, [$5], false)) $startpos $endpos } | Union id Eq Lcurly type_unions Rcurly { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos } - | Union id typquant Eq Lcurly type_unions Rcurly + | Union id typaram Eq Lcurly type_unions Rcurly { mk_td (TD_variant ($2, mk_namesectn, $3, $6, false)) $startpos $endpos } | Bitfield id Colon typ Eq Lcurly r_def_body Rcurly { mk_td (TD_bitfield ($2, $4, $7)) $startpos $endpos } diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index a2771ae1..53e77df2 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -151,7 +151,7 @@ let doc_nc nc = | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2] | _ -> atomic_nc nc in - nc0 ~parenthesize:true (constraint_simp nc) + atomic_nc (constraint_simp nc) let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) = match typ_aux with @@ -219,6 +219,27 @@ let doc_quants quants = | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs) +let doc_param_quants quants = + let doc_qi_kopt (QI_aux (qi_aux, _)) = + match qi_aux with + | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid] + | QI_id kopt when is_nat_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Int"] + | QI_id kopt when is_typ_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Type"] + | QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Order"] + | QI_const nc -> [] + in + let qi_nc (QI_aux (qi_aux, _)) = + match qi_aux with + | QI_const nc -> [nc] + | _ -> [] + in + let kdoc = separate (comma ^^ space) (List.concat (List.map doc_qi_kopt quants)) in + let ncs = List.concat (List.map qi_nc quants) in + match ncs with + | [] -> parens kdoc + | [nc] -> parens kdoc ^^ comma ^^ space ^^ doc_nc nc + | nc :: ncs -> parens kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs) + let doc_binding ?(simple=false) ((TypQ_aux (tq_aux, _) as typq), typ) = match tq_aux with | TypQ_no_forall -> doc_typ ~simple:simple typ @@ -244,7 +265,7 @@ let doc_typschm_quants (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) match tq_aux with | TypQ_no_forall -> None | TypQ_tq [] -> None - | TypQ_tq qs -> Some (doc_quants qs) + | TypQ_tq qs -> Some (doc_param_quants qs) let doc_lit (L_aux(l,_)) = utf8string (match l with @@ -547,7 +568,7 @@ let doc_typdef (TD_aux(td,_)) = match td with begin match doc_typschm_quants typschm with | Some qdoc -> - doc_op equals (concat [string "type"; space; doc_id id; space; qdoc]) (doc_typschm_typ typschm) + doc_op equals (concat [string "type"; space; doc_id id; qdoc]) (doc_typschm_typ typschm) | None -> doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm) end @@ -556,12 +577,12 @@ let doc_typdef (TD_aux(td,_)) = match td with | TD_record (id, _, TypQ_aux (TypQ_no_forall, _), fields, _) | TD_record (id, _, TypQ_aux (TypQ_tq [], _), fields, _) -> separate space [string "struct"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace] | TD_record (id, _, TypQ_aux (TypQ_tq qs, _), fields, _) -> - separate space [string "struct"; doc_id id; doc_quants qs; equals; + separate space [string "struct"; doc_id id; doc_param_quants qs; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace] | TD_variant (id, _, TypQ_aux (TypQ_no_forall, _), unions, _) | TD_variant (id, _, TypQ_aux (TypQ_tq [], _), unions, _) -> separate space [string "union"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace] | TD_variant (id, _, TypQ_aux (TypQ_tq qs, _), unions, _) -> - separate space [string "union"; doc_id id; doc_quants qs; equals; + separate space [string "union"; doc_id id; doc_param_quants qs; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace] | _ -> string "TYPEDEF" diff --git a/test/c/cheri128_hsb.sail b/test/c/cheri128_hsb.sail index a06a2ad2..d8501d88 100644 --- a/test/c/cheri128_hsb.sail +++ b/test/c/cheri128_hsb.sail @@ -14,7 +14,7 @@ val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range", c: "add_ val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) -val min = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)} +val min = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c == 'a | 'c == 'b) & 'c <= 'a & 'c <= 'b . atom('c)} overload operator + = {add_range} overload operator - = {sub_range} diff --git a/test/c/poly_pair.sail b/test/c/poly_pair.sail index 6d0bdaad..c4989829 100644 --- a/test/c/poly_pair.sail +++ b/test/c/poly_pair.sail @@ -4,7 +4,7 @@ val print = "print_endline" : string -> unit val "eq_int" : (int, int) -> bool -union test ('a : Type) ('b : Type) = { +union test('a : Type, 'b : Type) = { Ctor1 : ('a, 'b), Ctor2 : int } diff --git a/test/ocaml/reg_ref/rr.sail b/test/ocaml/reg_ref/rr.sail index d0a14586..f162d3a2 100644 --- a/test/ocaml/reg_ref/rr.sail +++ b/test/ocaml/reg_ref/rr.sail @@ -33,7 +33,7 @@ overload _mod_GPR = { rGPR, wGPR } /* Create a new type which is a pair of a bitvector and a start index slice('n, 'm) is equivalent to old-sail vector('n, 'm, dec, bit) */ -newtype slice ('n : Int) ('m : Int) = MkSlice : (atom('n), bits('m)) +newtype slice ('n : Int, 'm : Int) = MkSlice : (atom('n), bits('m)) /* Extract the bitvector from a slice */ val slice_bits : forall 'n 'm. slice('n, 'm) -> bits('m) @@ -76,7 +76,7 @@ overload _mod_slice = {_set_slice, _set_slice2, vector_slice, slice_slice} /* Set up a struct with an aliased LT bit in CR0, mimicing old-style syntax */ infix 1 ... -type operator ... ('n : Int) ('m : Int) = slice('m, 'n - ('m - 1)) +type operator ...('n : Int, 'm : Int) = slice('m, 'n - ('m - 1)) struct cr = { CR0 : 7 ... 4, diff --git a/test/ocaml/void/void.sail b/test/ocaml/void/void.sail index 485ac019..4e8815f5 100644 --- a/test/ocaml/void/void.sail +++ b/test/ocaml/void/void.sail @@ -1,5 +1,5 @@ -val void : forall 'n, 'n = 'n + 1. atom('n) -> unit +val void : forall 'n, 'n == 'n + 1. atom('n) -> unit function void _ = () diff --git a/test/typecheck/pass/bind_typ_var.sail b/test/typecheck/pass/bind_typ_var.sail index c442d6a8..ae340941 100644 --- a/test/typecheck/pass/bind_typ_var.sail +++ b/test/typecheck/pass/bind_typ_var.sail @@ -1,7 +1,7 @@ val mk_vector : unit -> {'n, 'n in {32, 64}. vector('n, dec, bit)} -val mk_square : unit -> {'n 'm, 'n = 'm. vector('n, dec, vector('m, dec, bit))} +val mk_square : unit -> {'n 'm, 'n == 'm. vector('n, dec, vector('m, dec, bit))} val test : unit -> unit @@ -10,8 +10,8 @@ function test () = { // could still be let v2 as 'len2 = mk_vector (); let matrix as vector('width, _, 'height) = mk_square (); - _prove(constraint('width = 'height)); - _prove(constraint('len = 32 | 'len = 64)); - _prove(constraint('len2 = 32 | 'len2 = 64)); + _prove(constraint('width == 'height)); + _prove(constraint('len == 32 | 'len == 64)); + _prove(constraint('len2 == 32 | 'len2 == 64)); () }
\ No newline at end of file diff --git a/test/typecheck/pass/constrained_struct.sail b/test/typecheck/pass/constrained_struct.sail index 64b2287f..87d55b65 100644 --- a/test/typecheck/pass/constrained_struct.sail +++ b/test/typecheck/pass/constrained_struct.sail @@ -2,7 +2,7 @@ default Order dec $include <prelude.sail> -struct MyStruct 'n, 'n in {32, 64} = { +struct MyStruct('n), 'n in {32, 64} = { field: bits('n) } diff --git a/test/typecheck/pass/constrained_struct/v1.sail b/test/typecheck/pass/constrained_struct/v1.sail index 62fc1c01..98daf59e 100644 --- a/test/typecheck/pass/constrained_struct/v1.sail +++ b/test/typecheck/pass/constrained_struct/v1.sail @@ -2,7 +2,7 @@ default Order dec $include <prelude.sail> -struct MyStruct 'n, 'n in {32, 64} = { +struct MyStruct('n), 'n in {32, 64} = { field: bits('n) } diff --git a/test/typecheck/pass/exint.sail b/test/typecheck/pass/exint.sail index ffa6d033..3e2acf28 100644 --- a/test/typecheck/pass/exint.sail +++ b/test/typecheck/pass/exint.sail @@ -1,8 +1,8 @@ type MyInt = {'n, true. atom('n)} -val add : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = 'n + 'm. atom('o)} +val add : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == 'n + 'm. atom('o)} -val mult : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = 'n * 'm. atom('o)} +val mult : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == 'n * 'm. atom('o)} overload operator + = {add} @@ -14,7 +14,7 @@ let y = x + x * x let z : atom(7 * 8) = y -type Range ('n : Int) ('m : Int), 'n <= 'm = {'o, 'n <= 'o & 'o <= 'm. atom('o)} +type Range('n: Int, 'm: Int), 'n <= 'm = {'o, 'n <= 'o & 'o <= 'm. atom('o)} let a : Range(3, 4) = 3 diff --git a/test/typecheck/pass/exist1.sail b/test/typecheck/pass/exist1.sail index f6c0c073..6db518e8 100644 --- a/test/typecheck/pass/exist1.sail +++ b/test/typecheck/pass/exist1.sail @@ -22,6 +22,6 @@ function unit_fn x : atom(4) = () val s_add : forall 'a. (atom('a), atom('a)) -> atom('a + 'a) -let v7 : {'k, 'k = 4. atom('k)} = 4 +let v7 : {'k, 'k == 4. atom('k)} = 4 let v8 = s_add(v7, 4) diff --git a/test/typecheck/pass/exist2.sail b/test/typecheck/pass/exist2.sail index 42ec8cb1..102a1084 100644 --- a/test/typecheck/pass/exist2.sail +++ b/test/typecheck/pass/exist2.sail @@ -22,13 +22,13 @@ function unit_fn x : atom(4) = () val s_add : forall 'a. (atom('a), atom('a)) -> atom('a + 'a) -let v7 : {'k, 'k = 4. atom('k)} = 4 +let v7 : {'k, 'k == 4. atom('k)} = 4 -let v9 : {'n, 0 = 0. atom('n)} = 100 +let v9 : {'n, 0 == 0. atom('n)} = 100 let v10 : int = v9 -type MyInt = {'n, 0 = 0. atom('n)} +type MyInt = {'n, 0 == 0. atom('n)} val existential_int : int -> MyInt @@ -37,7 +37,7 @@ val existential_range : forall 'n 'm. overload existential = {existential_int, existential_range} -let v11 : {'n, 0 = 0. atom('n)} = existential(v10) +let v11 : {'n, 0 == 0. atom('n)} = existential(v10) let v12 : {'e, 0 <= 'e & 'e <= 3. atom('e)} = existential(2 : range(0, 3)) diff --git a/test/typecheck/pass/exist_synonym.sail b/test/typecheck/pass/exist_synonym.sail index 44382213..b251cbf8 100644 --- a/test/typecheck/pass/exist_synonym.sail +++ b/test/typecheck/pass/exist_synonym.sail @@ -1,6 +1,6 @@ // Type synonym with a constraint. -type regno ('n : Int), 0 <= 'n < 32 = atom('n) +type regno('n: Int), 0 <= 'n < 32 = atom('n) // Existential with constrained type synonym. let x : {'n, 0 <= 'n <= 8. regno('n)} = 4 diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect index 3169f619..583c4485 100644 --- a/test/typecheck/pass/exist_synonym/v1.expect +++ b/test/typecheck/pass/exist_synonym/v1.expect @@ -2,6 +2,6 @@ Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, char let x : {'n, 0 <= 'n <= 33. regno('n)} = [41m4[0m -Tried performing type coercion from int(4) to {'n, 0 <= 'n & 'n <= 33. regno('n)} on 4 +Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 33). regno('n)} on 4 Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33) diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect index 02b1c17a..baddbcb0 100644 --- a/test/typecheck/pass/exist_synonym/v2.expect +++ b/test/typecheck/pass/exist_synonym/v2.expect @@ -2,6 +2,6 @@ Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, char let x : {'n, 0 <= 'n <= 8. regno('n)} = [41m4[0m -Tried performing type coercion from int(4) to {'n, 0 <= 'n & 'n <= 8. regno('n)} on 4 +Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 8). regno('n)} on 4 Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8) diff --git a/test/typecheck/pass/option_either.sail b/test/typecheck/pass/option_either.sail index 24e50259..ec4e72db 100644 --- a/test/typecheck/pass/option_either.sail +++ b/test/typecheck/pass/option_either.sail @@ -1,6 +1,6 @@ default Order inc -union option ('a : Type) = {None : unit, Some : 'a} +union option('a: Type) = {None : unit, Some : 'a} function none forall ('a : Type). () -> option('a) = None() @@ -11,7 +11,7 @@ function test forall ('a : Type). x : option('a) -> range(0, 1) = match x { Some(y) => 1 } -union either ('a : Type) ('b : Type) = {Left : 'a, Right : 'b} +union either('a: Type, 'b: Type) = {Left : 'a, Right : 'b} val signed : forall ('n : Int), 'n >= 0. vector('n, inc, bit) -> int diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail index cbdb2c9d..588fd324 100644 --- a/test/typecheck/pass/pure_record2.sail +++ b/test/typecheck/pass/pure_record2.sail @@ -1,6 +1,6 @@ default Order dec -struct State ('a : Type) ('n : Int) = { +struct State('a: Type, 'n: Int) = { N : vector('n, dec, 'a), Z : vector(1, dec, bit) } diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail index cd3e849a..de388c3e 100644 --- a/test/typecheck/pass/pure_record3.sail +++ b/test/typecheck/pass/pure_record3.sail @@ -1,6 +1,6 @@ default Order dec -struct State ('a : Type) ('n : Int) = { +struct State('a: Type, 'n: Int) = { N : vector('n, dec, 'a), Z : vector(1, dec, bit) } |