diff options
| -rw-r--r-- | aarch64/mono/demo/aarch64_no_vector/decode.sail (renamed from aarch64/mono/demo/aarch64_no_vector/aarch64_no_vector_decode.sail) | 212 | ||||
| -rw-r--r-- | aarch64/mono/demo/aarch64_no_vector/spec.sail (renamed from aarch64/mono/demo/aarch64_no_vector/aarch64_no_vector.sail) | 447 | ||||
| -rwxr-xr-x | aarch64/mono/demo/mk | 4 | ||||
| -rw-r--r-- | src/monomorphise.ml | 10 |
4 files changed, 328 insertions, 345 deletions
diff --git a/aarch64/mono/demo/aarch64_no_vector/aarch64_no_vector_decode.sail b/aarch64/mono/demo/aarch64_no_vector/decode.sail index a37b064a..e881207a 100644 --- a/aarch64/mono/demo/aarch64_no_vector/aarch64_no_vector_decode.sail +++ b/aarch64/mono/demo/aarch64_no_vector/decode.sail @@ -1,4 +1,4 @@ -function clause decode 0b10011011 @ _ : bits(1) @ 0b10 @ _ : bits(5) @ 0b0 @ _ : bits(15) as op_code = { +function clause decode (0b10011011 @ _ : bits(1) @ 0b10 @ _ : bits(5) @ 0b0 @ _ : bits(15) as op_code) = { sf : bits(1) = [op_code[31]]; op54 : bits(2) = op_code[30 .. 29]; U : bits(1) = [op_code[23]]; @@ -10,7 +10,7 @@ function clause decode 0b10011011 @ _ : bits(1) @ 0b10 @ _ : bits(5) @ 0b0 @ _ : integer_arithmetic_mul_widening_64128hi_decode(sf, op54, U, Rm, o0, Ra, Rn, Rd) } -function clause decode _ : bits(2) @ 0b1010001 @ _ : bits(23) as op_code = { +function clause decode (_ : bits(2) @ 0b1010001 @ _ : bits(23) as op_code) = { opc : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; L : bits(1) = [op_code[22]]; @@ -21,7 +21,7 @@ function clause decode _ : bits(2) @ 0b1010001 @ _ : bits(23) as op_code = { memory_pair_general_postidx_aarch64_memory_pair_general_postidx__decode(opc, V, L, imm7, Rt2, Rn, Rt) } -function clause decode _ : bits(2) @ 0b1010011 @ _ : bits(23) as op_code = { +function clause decode (_ : bits(2) @ 0b1010011 @ _ : bits(23) as op_code) = { opc : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; L : bits(1) = [op_code[22]]; @@ -32,7 +32,7 @@ function clause decode _ : bits(2) @ 0b1010011 @ _ : bits(23) as op_code = { memory_pair_general_preidx_aarch64_memory_pair_general_postidx__decode(opc, V, L, imm7, Rt2, Rn, Rt) } -function clause decode _ : bits(2) @ 0b1010010 @ _ : bits(23) as op_code = { +function clause decode (_ : bits(2) @ 0b1010010 @ _ : bits(23) as op_code) = { opc : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; L : bits(1) = [op_code[22]]; @@ -43,7 +43,7 @@ function clause decode _ : bits(2) @ 0b1010010 @ _ : bits(23) as op_code = { memory_pair_general_offset_aarch64_memory_pair_general_postidx__decode(opc, V, L, imm7, Rt2, Rn, Rt) } -function clause decode _ : bits(2) @ 0b111100 @ _ : bits(2) @ 0b1 @ _ : bits(9) @ 0b10 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(2) @ 0b111100 @ _ : bits(2) @ 0b1 @ _ : bits(9) @ 0b10 @ _ : bits(10) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; opc : bits(2) = op_code[23 .. 22]; @@ -55,7 +55,7 @@ function clause decode _ : bits(2) @ 0b111100 @ _ : bits(2) @ 0b1 @ _ : bits(9) memory_single_simdfp_register_aarch64_memory_single_simdfp_register__decode(size, V, opc, Rm, option_name, S, Rn, Rt) } -function clause decode 0b00011111 @ _ : bits(24) as op_code = { +function clause decode (0b00011111 @ _ : bits(24) as op_code) = { M : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; typ : bits(2) = op_code[23 .. 22]; @@ -68,7 +68,7 @@ function clause decode 0b00011111 @ _ : bits(24) as op_code = { float_arithmetic_mul_addsub_decode(M, S, typ, o1, Rm, o0, Ra, Rn, Rd) } -function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b0 @ _ : bits(3) @ 0b00 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b0 @ _ : bits(3) @ 0b00 @ _ : bits(10) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; A : bits(1) = [op_code[23]]; @@ -81,7 +81,7 @@ function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b1 @ _ : bits(5) memory_atomicops_ld_decode(size, V, A, R, Rs, o3, opc, Rn, Rt) } -function clause decode 0b110110101100000101000 @ _ : bits(11) as op_code = { +function clause decode (0b110110101100000101000 @ _ : bits(11) as op_code) = { sf : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; opcode2 : bits(5) = op_code[20 .. 16]; @@ -91,7 +91,7 @@ function clause decode 0b110110101100000101000 @ _ : bits(11) as op_code = { integer_pac_strip_dp_1src_decode(sf, S, opcode2, D, Rn, Rd) } -function clause decode 0b11010101000000110010000011111111 as op_code = { +function clause decode (0b11010101000000110010000011111111 as op_code) = { L : bits(1) = [op_code[21]]; op0 : bits(2) = op_code[20 .. 19]; op1 : bits(3) = op_code[18 .. 16]; @@ -102,7 +102,7 @@ function clause decode 0b11010101000000110010000011111111 as op_code = { integer_pac_strip_hint_decode(L, op0, op1, CRn, CRm, op2, Rt) } -function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b010 @ _ : bits(10) as op_code = { +function clause decode (0b110110101100000100 @ _ : bits(1) @ 0b010 @ _ : bits(10) as op_code) = { sf : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; opcode2 : bits(5) = op_code[20 .. 16]; @@ -112,7 +112,7 @@ function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b010 @ _ : bits(10) integer_pac_pacda_dp_1src_decode(sf, S, opcode2, Z, Rn, Rd) } -function clause decode 0b11010101000000110011 @ _ : bits(4) @ 0b01011111 as op_code = { +function clause decode (0b11010101000000110011 @ _ : bits(4) @ 0b01011111 as op_code) = { L : bits(1) = [op_code[21]]; op0 : bits(2) = op_code[20 .. 19]; op1 : bits(3) = op_code[18 .. 16]; @@ -123,7 +123,7 @@ function clause decode 0b11010101000000110011 @ _ : bits(4) @ 0b01011111 as op_c system_monitors_decode(L, op0, op1, CRn, CRm, op2, Rt) } -function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b0 @ _ : bits(9) @ 0b00 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b0 @ _ : bits(9) @ 0b00 @ _ : bits(10) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; opc : bits(2) = op_code[23 .. 22]; @@ -133,7 +133,7 @@ function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b0 @ _ : bits(9) memory_single_general_immediate_signed_offset_normal_aarch64_memory_single_general_immediate_signed_offset_normal__decode(size, V, opc, imm9, Rn, Rt) } -function clause decode _ : bits(2) @ 0b1010000 @ _ : bits(23) as op_code = { +function clause decode (_ : bits(2) @ 0b1010000 @ _ : bits(23) as op_code) = { opc : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; L : bits(1) = [op_code[22]]; @@ -144,7 +144,7 @@ function clause decode _ : bits(2) @ 0b1010000 @ _ : bits(23) as op_code = { memory_pair_general_noalloc_aarch64_memory_pair_general_noalloc__decode(opc, V, L, imm7, Rt2, Rn, Rt) } -function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(6) @ 0b00010 @ _ : bits(10) as op_code = { +function clause decode (0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(6) @ 0b00010 @ _ : bits(10) as op_code) = { M : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; typ : bits(2) = op_code[23 .. 22]; @@ -155,7 +155,7 @@ function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(6) @ 0b00010 @ float_arithmetic_mul_product_decode(M, S, typ, Rm, op, Rn, Rd) } -function clause decode 0b10011010110 @ _ : bits(5) @ 0b001100 @ _ : bits(10) as op_code = { +function clause decode (0b10011010110 @ _ : bits(5) @ 0b001100 @ _ : bits(10) as op_code) = { sf : bits(1) = [op_code[31]]; op : bits(1) = [op_code[30]]; S : bits(1) = [op_code[29]]; @@ -166,7 +166,7 @@ function clause decode 0b10011010110 @ _ : bits(5) @ 0b001100 @ _ : bits(10) as integer_pac_pacga_dp_2src_decode(sf, op, S, Rm, opcode2, Rn, Rd) } -function clause decode _ : bits(2) @ 0b0010001 @ _ : bits(1) @ 0b1 @ _ : bits(6) @ 0b11111 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(2) @ 0b0010001 @ _ : bits(1) @ 0b1 @ _ : bits(6) @ 0b11111 @ _ : bits(10) as op_code) = { size : bits(2) = op_code[31 .. 30]; o2 : bits(1) = [op_code[23]]; L : bits(1) = [op_code[22]]; @@ -179,7 +179,7 @@ function clause decode _ : bits(2) @ 0b0010001 @ _ : bits(1) @ 0b1 @ _ : bits(6) memory_atomicops_cas_single_decode(size, o2, L, o1, Rs, o0, Rt2, Rn, Rt) } -function clause decode 0b1101010100000 @ _ : bits(3) @ 0b0100 @ _ : bits(7) @ 0b11111 as op_code = { +function clause decode (0b1101010100000 @ _ : bits(3) @ 0b0100 @ _ : bits(7) @ 0b11111 as op_code) = { L : bits(1) = [op_code[21]]; op0 : bits(2) = op_code[20 .. 19]; op1 : bits(3) = op_code[18 .. 16]; @@ -190,7 +190,7 @@ function clause decode 0b1101010100000 @ _ : bits(3) @ 0b0100 @ _ : bits(7) @ 0b system_register_cpsr_decode(L, op0, op1, CRn, CRm, op2, Rt) } -function clause decode 0b01010100 @ _ : bits(19) @ 0b0 @ _ : bits(4) as op_code = { +function clause decode (0b01010100 @ _ : bits(19) @ 0b0 @ _ : bits(4) as op_code) = { o1 : bits(1) = [op_code[24]]; imm19 : bits(19) = op_code[23 .. 5]; o0 : bits(1) = [op_code[4]]; @@ -198,7 +198,7 @@ function clause decode 0b01010100 @ _ : bits(19) @ 0b0 @ _ : bits(4) as op_code branch_conditional_cond_decode(o1, imm19, o0, cond) } -function clause decode 0b11010100000 @ _ : bits(16) @ 0b00010 as op_code = { +function clause decode (0b11010100000 @ _ : bits(16) @ 0b00010 as op_code) = { opc : bits(3) = op_code[23 .. 21]; imm16 : bits(16) = op_code[20 .. 5]; op2 : bits(3) = op_code[4 .. 2]; @@ -206,7 +206,7 @@ function clause decode 0b11010100000 @ _ : bits(16) @ 0b00010 as op_code = { system_exceptions_runtime_hvc_decode(opc, imm16, op2, LL) } -function clause decode 0b1 @ _ : bits(1) @ 0b0010000 @ _ : bits(1) @ 0b1 @ _ : bits(21) as op_code = { +function clause decode (0b1 @ _ : bits(1) @ 0b0010000 @ _ : bits(1) @ 0b1 @ _ : bits(21) as op_code) = { sz : bits(1) = [op_code[30]]; o2 : bits(1) = [op_code[23]]; L : bits(1) = [op_code[22]]; @@ -219,7 +219,7 @@ function clause decode 0b1 @ _ : bits(1) @ 0b0010000 @ _ : bits(1) @ 0b1 @ _ : b memory_exclusive_pair_decode(sz, o2, L, o1, Rs, o0, Rt2, Rn, Rt) } -function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b111 @ _ : bits(10) as op_code = { +function clause decode (0b110110101100000100 @ _ : bits(1) @ 0b111 @ _ : bits(10) as op_code) = { sf : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; opcode2 : bits(5) = op_code[20 .. 16]; @@ -229,7 +229,7 @@ function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b111 @ _ : bits(10) integer_pac_autdb_dp_1src_decode(sf, S, opcode2, Z, Rn, Rd) } -function clause decode _ : bits(1) @ 0b101101011000000000000 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(1) @ 0b101101011000000000000 @ _ : bits(10) as op_code) = { sf : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; opcode2 : bits(5) = op_code[20 .. 16]; @@ -238,7 +238,7 @@ function clause decode _ : bits(1) @ 0b101101011000000000000 @ _ : bits(10) as o integer_arithmetic_rbit_decode(sf, S, opcode2, Rn, Rd) } -function clause decode _ : bits(2) @ 0b111001 @ _ : bits(24) as op_code = { +function clause decode (_ : bits(2) @ 0b111001 @ _ : bits(24) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; opc : bits(2) = op_code[23 .. 22]; @@ -248,7 +248,7 @@ function clause decode _ : bits(2) @ 0b111001 @ _ : bits(24) as op_code = { memory_single_general_immediate_unsigned_aarch64_memory_single_general_immediate_unsigned__decode(size, V, opc, imm12, Rn, Rt) } -function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b100 @ _ : bits(10) as op_code = { +function clause decode (0b110110101100000100 @ _ : bits(1) @ 0b100 @ _ : bits(10) as op_code) = { sf : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; opcode2 : bits(5) = op_code[20 .. 16]; @@ -258,7 +258,7 @@ function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b100 @ _ : bits(10) integer_pac_autia_dp_1src_decode(sf, S, opcode2, Z, Rn, Rd) } -function clause decode 0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code = { +function clause decode (0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code) = { L : bits(1) = [op_code[21]]; op0 : bits(2) = op_code[20 .. 19]; op1 : bits(3) = op_code[18 .. 16]; @@ -269,7 +269,7 @@ function clause decode 0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code integer_pac_autia_hint_decode(L, op0, op1, CRn, CRm, op2, Rt) } -function clause decode 0b11010100000 @ _ : bits(16) @ 0b00001 as op_code = { +function clause decode (0b11010100000 @ _ : bits(16) @ 0b00001 as op_code) = { opc : bits(3) = op_code[23 .. 21]; imm16 : bits(16) = op_code[20 .. 5]; op2 : bits(3) = op_code[4 .. 2]; @@ -277,7 +277,7 @@ function clause decode 0b11010100000 @ _ : bits(16) @ 0b00001 as op_code = { system_exceptions_runtime_svc_decode(opc, imm16, op2, LL) } -function clause decode 0b1101011 @ _ : bits(1) @ 0b0 @ _ : bits(2) @ 0b111110000 @ _ : bits(12) as op_code = { +function clause decode (0b1101011 @ _ : bits(1) @ 0b0 @ _ : bits(2) @ 0b111110000 @ _ : bits(12) as op_code) = { Z : bits(1) = [op_code[24]]; opc : bits(1) = [op_code[23]]; op : bits(2) = op_code[22 .. 21]; @@ -290,7 +290,7 @@ function clause decode 0b1101011 @ _ : bits(1) @ 0b0 @ _ : bits(2) @ 0b111110000 branch_unconditional_register_decode(Z, opc, op, op2, op3, A, M, Rn, Rm) } -function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(8) @ 0b10000000 @ _ : bits(5) as op_code = { +function clause decode (0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(8) @ 0b10000000 @ _ : bits(5) as op_code) = { M : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; typ : bits(2) = op_code[23 .. 22]; @@ -300,7 +300,7 @@ function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(8) @ 0b10000000 float_move_fp_imm_decode(M, S, typ, imm8, imm5, Rd) } -function clause decode _ : bits(1) @ 0b011011 @ _ : bits(25) as op_code = { +function clause decode (_ : bits(1) @ 0b011011 @ _ : bits(25) as op_code) = { b5 : bits(1) = [op_code[31]]; op : bits(1) = [op_code[24]]; b40 : bits(5) = op_code[23 .. 19]; @@ -309,7 +309,7 @@ function clause decode _ : bits(1) @ 0b011011 @ _ : bits(25) as op_code = { branch_conditional_test_decode(b5, op, b40, imm14, Rt) } -function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b0 @ _ : bits(9) @ 0b01 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b0 @ _ : bits(9) @ 0b01 @ _ : bits(10) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; opc : bits(2) = op_code[23 .. 22]; @@ -319,7 +319,7 @@ function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b0 @ _ : bits(9) memory_single_general_immediate_signed_postidx_aarch64_memory_single_general_immediate_signed_postidx__decode(size, V, opc, imm9, Rn, Rt) } -function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b0 @ _ : bits(9) @ 0b11 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b0 @ _ : bits(9) @ 0b11 @ _ : bits(10) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; opc : bits(2) = op_code[23 .. 22]; @@ -329,7 +329,7 @@ function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b0 @ _ : bits(9) memory_single_general_immediate_signed_preidx_aarch64_memory_single_general_immediate_signed_postidx__decode(size, V, opc, imm9, Rn, Rt) } -function clause decode _ : bits(2) @ 0b111001 @ _ : bits(24) as op_code = { +function clause decode (_ : bits(2) @ 0b111001 @ _ : bits(24) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; opc : bits(2) = op_code[23 .. 22]; @@ -339,7 +339,7 @@ function clause decode _ : bits(2) @ 0b111001 @ _ : bits(24) as op_code = { memory_single_general_immediate_unsigned_aarch64_memory_single_general_immediate_signed_postidx__decode(size, V, opc, imm12, Rn, Rt) } -function clause decode _ : bits(2) @ 0b011000 @ _ : bits(24) as op_code = { +function clause decode (_ : bits(2) @ 0b011000 @ _ : bits(24) as op_code) = { opc : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; imm19 : bits(19) = op_code[23 .. 5]; @@ -347,7 +347,7 @@ function clause decode _ : bits(2) @ 0b011000 @ _ : bits(24) as op_code = { memory_literal_general_decode(opc, V, imm19, Rt) } -function clause decode _ : bits(2) @ 0b1011001 @ _ : bits(23) as op_code = { +function clause decode (_ : bits(2) @ 0b1011001 @ _ : bits(23) as op_code) = { opc : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; L : bits(1) = [op_code[22]]; @@ -358,7 +358,7 @@ function clause decode _ : bits(2) @ 0b1011001 @ _ : bits(23) as op_code = { memory_pair_simdfp_postidx_aarch64_memory_pair_simdfp_postidx__decode(opc, V, L, imm7, Rt2, Rn, Rt) } -function clause decode _ : bits(2) @ 0b1011011 @ _ : bits(23) as op_code = { +function clause decode (_ : bits(2) @ 0b1011011 @ _ : bits(23) as op_code) = { opc : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; L : bits(1) = [op_code[22]]; @@ -369,7 +369,7 @@ function clause decode _ : bits(2) @ 0b1011011 @ _ : bits(23) as op_code = { memory_pair_simdfp_preidx_aarch64_memory_pair_simdfp_postidx__decode(opc, V, L, imm7, Rt2, Rn, Rt) } -function clause decode _ : bits(2) @ 0b1011010 @ _ : bits(23) as op_code = { +function clause decode (_ : bits(2) @ 0b1011010 @ _ : bits(23) as op_code) = { opc : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; L : bits(1) = [op_code[22]]; @@ -380,7 +380,7 @@ function clause decode _ : bits(2) @ 0b1011010 @ _ : bits(23) as op_code = { memory_pair_simdfp_offset_aarch64_memory_pair_simdfp_postidx__decode(opc, V, L, imm7, Rt2, Rn, Rt) } -function clause decode _ : bits(1) @ 0b011010 @ _ : bits(25) as op_code = { +function clause decode (_ : bits(1) @ 0b011010 @ _ : bits(25) as op_code) = { sf : bits(1) = [op_code[31]]; op : bits(1) = [op_code[24]]; imm19 : bits(19) = op_code[23 .. 5]; @@ -388,7 +388,7 @@ function clause decode _ : bits(1) @ 0b011010 @ _ : bits(25) as op_code = { branch_conditional_compare_decode(sf, op, imm19, Rt) } -function clause decode _ : bits(2) @ 0b111100 @ _ : bits(2) @ 0b0 @ _ : bits(9) @ 0b00 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(2) @ 0b111100 @ _ : bits(2) @ 0b0 @ _ : bits(9) @ 0b00 @ _ : bits(10) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; opc : bits(2) = op_code[23 .. 22]; @@ -398,7 +398,7 @@ function clause decode _ : bits(2) @ 0b111100 @ _ : bits(2) @ 0b0 @ _ : bits(9) memory_single_simdfp_immediate_signed_offset_normal_aarch64_memory_single_simdfp_immediate_signed_offset_normal__decode(size, V, opc, imm9, Rn, Rt) } -function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b001 @ _ : bits(10) as op_code = { +function clause decode (0b110110101100000100 @ _ : bits(1) @ 0b001 @ _ : bits(10) as op_code) = { sf : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; opcode2 : bits(5) = op_code[20 .. 16]; @@ -408,7 +408,7 @@ function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b001 @ _ : bits(10) integer_pac_pacib_dp_1src_decode(sf, S, opcode2, Z, Rn, Rd) } -function clause decode 0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code = { +function clause decode (0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code) = { L : bits(1) = [op_code[21]]; op0 : bits(2) = op_code[20 .. 19]; op1 : bits(3) = op_code[18 .. 16]; @@ -419,7 +419,7 @@ function clause decode 0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code integer_pac_pacib_hint_decode(L, op0, op1, CRn, CRm, op2, Rt) } -function clause decode _ : bits(2) @ 0b111100 @ _ : bits(2) @ 0b0 @ _ : bits(9) @ 0b01 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(2) @ 0b111100 @ _ : bits(2) @ 0b0 @ _ : bits(9) @ 0b01 @ _ : bits(10) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; opc : bits(2) = op_code[23 .. 22]; @@ -429,7 +429,7 @@ function clause decode _ : bits(2) @ 0b111100 @ _ : bits(2) @ 0b0 @ _ : bits(9) memory_single_simdfp_immediate_signed_postidx_aarch64_memory_single_simdfp_immediate_signed_postidx__decode(size, V, opc, imm9, Rn, Rt) } -function clause decode _ : bits(2) @ 0b111100 @ _ : bits(2) @ 0b0 @ _ : bits(9) @ 0b11 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(2) @ 0b111100 @ _ : bits(2) @ 0b0 @ _ : bits(9) @ 0b11 @ _ : bits(10) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; opc : bits(2) = op_code[23 .. 22]; @@ -439,7 +439,7 @@ function clause decode _ : bits(2) @ 0b111100 @ _ : bits(2) @ 0b0 @ _ : bits(9) memory_single_simdfp_immediate_signed_preidx_aarch64_memory_single_simdfp_immediate_signed_postidx__decode(size, V, opc, imm9, Rn, Rt) } -function clause decode _ : bits(2) @ 0b111101 @ _ : bits(24) as op_code = { +function clause decode (_ : bits(2) @ 0b111101 @ _ : bits(24) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; opc : bits(2) = op_code[23 .. 22]; @@ -449,7 +449,7 @@ function clause decode _ : bits(2) @ 0b111101 @ _ : bits(24) as op_code = { memory_single_simdfp_immediate_unsigned_aarch64_memory_single_simdfp_immediate_signed_postidx__decode(size, V, opc, imm12, Rn, Rt) } -function clause decode 0b0 @ _ : bits(1) @ 0b0011000 @ _ : bits(1) @ 0b000000 @ _ : bits(16) as op_code = { +function clause decode (0b0 @ _ : bits(1) @ 0b0011000 @ _ : bits(1) @ 0b000000 @ _ : bits(16) as op_code) = { Q : bits(1) = [op_code[30]]; L : bits(1) = [op_code[22]]; opcode : bits(4) = op_code[15 .. 12]; @@ -459,7 +459,7 @@ function clause decode 0b0 @ _ : bits(1) @ 0b0011000 @ _ : bits(1) @ 0b000000 @ memory_vector_multiple_nowb_aarch64_memory_vector_multiple_nowb__decode(Q, L, opcode, size, Rn, Rt) } -function clause decode 0b0 @ _ : bits(1) @ 0b0011001 @ _ : bits(1) @ 0b0 @ _ : bits(21) as op_code = { +function clause decode (0b0 @ _ : bits(1) @ 0b0011001 @ _ : bits(1) @ 0b0 @ _ : bits(21) as op_code) = { Q : bits(1) = [op_code[30]]; L : bits(1) = [op_code[22]]; Rm : bits(5) = op_code[20 .. 16]; @@ -470,7 +470,7 @@ function clause decode 0b0 @ _ : bits(1) @ 0b0011001 @ _ : bits(1) @ 0b0 @ _ : b memory_vector_multiple_postinc_aarch64_memory_vector_multiple_nowb__decode(Q, L, Rm, opcode, size, Rn, Rt) } -function clause decode 0b11010110100111110000 @ _ : bits(12) as op_code = { +function clause decode (0b11010110100111110000 @ _ : bits(12) as op_code) = { opc : bits(4) = op_code[24 .. 21]; op2 : bits(5) = op_code[20 .. 16]; op3 : bits(4) = op_code[15 .. 12]; @@ -481,7 +481,7 @@ function clause decode 0b11010110100111110000 @ _ : bits(12) as op_code = { branch_unconditional_eret_decode(opc, op2, op3, A, M, Rn, op4) } -function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b01 @ _ : bits(2) @ 0b10 @ _ : bits(10) as op_code = { +function clause decode (0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b01 @ _ : bits(2) @ 0b10 @ _ : bits(10) as op_code) = { M : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; typ : bits(2) = op_code[23 .. 22]; @@ -492,7 +492,7 @@ function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b01 @ _ : float_arithmetic_maxmin_decode(M, S, typ, Rm, op, Rn, Rd) } -function clause decode 0b00011110 @ _ : bits(2) @ 0b10000 @ _ : bits(2) @ 0b10000 @ _ : bits(10) as op_code = { +function clause decode (0b00011110 @ _ : bits(2) @ 0b10000 @ _ : bits(2) @ 0b10000 @ _ : bits(10) as op_code) = { M : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; typ : bits(2) = op_code[23 .. 22]; @@ -502,7 +502,7 @@ function clause decode 0b00011110 @ _ : bits(2) @ 0b10000 @ _ : bits(2) @ 0b1000 float_arithmetic_unary_decode(M, S, typ, opc, Rn, Rd) } -function clause decode 0b11010100000 @ _ : bits(16) @ 0b00011 as op_code = { +function clause decode (0b11010100000 @ _ : bits(16) @ 0b00011 as op_code) = { opc : bits(3) = op_code[23 .. 21]; imm16 : bits(16) = op_code[20 .. 5]; op2 : bits(3) = op_code[4 .. 2]; @@ -510,7 +510,7 @@ function clause decode 0b11010100000 @ _ : bits(16) @ 0b00011 as op_code = { system_exceptions_runtime_smc_decode(opc, imm16, op2, LL) } -function clause decode _ : bits(2) @ 0b0010001 @ _ : bits(1) @ 0b0 @ _ : bits(21) as op_code = { +function clause decode (_ : bits(2) @ 0b0010001 @ _ : bits(1) @ 0b0 @ _ : bits(21) as op_code) = { size : bits(2) = op_code[31 .. 30]; o2 : bits(1) = [op_code[23]]; L : bits(1) = [op_code[22]]; @@ -523,7 +523,7 @@ function clause decode _ : bits(2) @ 0b0010001 @ _ : bits(1) @ 0b0 @ _ : bits(21 memory_ordered_decode(size, o2, L, o1, Rs, o0, Rt2, Rn, Rt) } -function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b1 @ _ : bits(9) @ 0b10 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b1 @ _ : bits(9) @ 0b10 @ _ : bits(10) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; opc : bits(2) = op_code[23 .. 22]; @@ -535,7 +535,7 @@ function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b1 @ _ : bits(9) memory_single_general_register_aarch64_memory_single_general_register__decode(size, V, opc, Rm, option_name, S, Rn, Rt) } -function clause decode _ : bits(2) @ 0b1011000 @ _ : bits(23) as op_code = { +function clause decode (_ : bits(2) @ 0b1011000 @ _ : bits(23) as op_code) = { opc : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; L : bits(1) = [op_code[22]]; @@ -546,7 +546,7 @@ function clause decode _ : bits(2) @ 0b1011000 @ _ : bits(23) as op_code = { memory_pair_simdfp_noalloc_aarch64_memory_pair_simdfp_noalloc__decode(opc, V, L, imm7, Rt2, Rn, Rt) } -function clause decode 0b11010100001 @ _ : bits(16) @ 0b00000 as op_code = { +function clause decode (0b11010100001 @ _ : bits(16) @ 0b00000 as op_code) = { opc : bits(3) = op_code[23 .. 21]; imm16 : bits(16) = op_code[20 .. 5]; op2 : bits(3) = op_code[4 .. 2]; @@ -554,7 +554,7 @@ function clause decode 0b11010100001 @ _ : bits(16) @ 0b00000 as op_code = { system_exceptions_debug_breakpoint_decode(opc, imm16, op2, LL) } -function clause decode _ : bits(1) @ 0b0011011000 @ _ : bits(21) as op_code = { +function clause decode (_ : bits(1) @ 0b0011011000 @ _ : bits(21) as op_code) = { sf : bits(1) = [op_code[31]]; op54 : bits(2) = op_code[30 .. 29]; op31 : bits(3) = op_code[23 .. 21]; @@ -566,7 +566,7 @@ function clause decode _ : bits(1) @ 0b0011011000 @ _ : bits(21) as op_code = { integer_arithmetic_mul_uniform_addsub_decode(sf, op54, op31, Rm, o0, Ra, Rn, Rd) } -function clause decode _ : bits(2) @ 0b011100 @ _ : bits(24) as op_code = { +function clause decode (_ : bits(2) @ 0b011100 @ _ : bits(24) as op_code) = { opc : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; imm19 : bits(19) = op_code[23 .. 5]; @@ -574,7 +574,7 @@ function clause decode _ : bits(2) @ 0b011100 @ _ : bits(24) as op_code = { memory_literal_simdfp_decode(opc, V, imm19, Rt) } -function clause decode 0b1101010100 @ _ : bits(1) @ 0b01 @ _ : bits(19) as op_code = { +function clause decode (0b1101010100 @ _ : bits(1) @ 0b01 @ _ : bits(19) as op_code) = { L : bits(1) = [op_code[21]]; op0 : bits(2) = op_code[20 .. 19]; op1 : bits(3) = op_code[18 .. 16]; @@ -585,7 +585,7 @@ function clause decode 0b1101010100 @ _ : bits(1) @ 0b01 @ _ : bits(19) as op_co system_sysops_decode(L, op0, op1, CRn, CRm, op2, Rt) } -function clause decode _ : bits(3) @ 0b01011 @ _ : bits(2) @ 0b0 @ _ : bits(21) as op_code = { +function clause decode (_ : bits(3) @ 0b01011 @ _ : bits(2) @ 0b0 @ _ : bits(21) as op_code) = { sf : bits(1) = [op_code[31]]; op : bits(1) = [op_code[30]]; S : bits(1) = [op_code[29]]; @@ -597,7 +597,7 @@ function clause decode _ : bits(3) @ 0b01011 @ _ : bits(2) @ 0b0 @ _ : bits(21) integer_arithmetic_addsub_shiftedreg_decode(sf, op, S, shift, Rm, imm6, Rn, Rd) } -function clause decode _ : bits(3) @ 0b100100 @ _ : bits(23) as op_code = { +function clause decode (_ : bits(3) @ 0b100100 @ _ : bits(23) as op_code) = { sf : bits(1) = [op_code[31]]; opc : bits(2) = op_code[30 .. 29]; N : bits(1) = [op_code[22]]; @@ -608,7 +608,7 @@ function clause decode _ : bits(3) @ 0b100100 @ _ : bits(23) as op_code = { integer_logical_immediate_decode(sf, opc, N, immr, imms, Rn, Rd) } -function clause decode _ : bits(2) @ 0b111010010 @ _ : bits(9) @ 0b00 @ _ : bits(5) @ 0b0 @ _ : bits(4) as op_code = { +function clause decode (_ : bits(2) @ 0b111010010 @ _ : bits(9) @ 0b00 @ _ : bits(5) @ 0b0 @ _ : bits(4) as op_code) = { sf : bits(1) = [op_code[31]]; op : bits(1) = [op_code[30]]; S : bits(1) = [op_code[29]]; @@ -621,7 +621,7 @@ function clause decode _ : bits(2) @ 0b111010010 @ _ : bits(9) @ 0b00 @ _ : bits integer_conditional_compare_register_decode(sf, op, S, Rm, cond, o2, Rn, o3, nzcv) } -function clause decode _ : bits(3) @ 0b100110 @ _ : bits(23) as op_code = { +function clause decode (_ : bits(3) @ 0b100110 @ _ : bits(23) as op_code) = { sf : bits(1) = [op_code[31]]; opc : bits(2) = op_code[30 .. 29]; N : bits(1) = [op_code[22]]; @@ -632,7 +632,7 @@ function clause decode _ : bits(3) @ 0b100110 @ _ : bits(23) as op_code = { integer_bitfield_decode(sf, opc, N, immr, imms, Rn, Rd) } -function clause decode 0b1101010100 @ _ : bits(1) @ 0b1 @ _ : bits(20) as op_code = { +function clause decode (0b1101010100 @ _ : bits(1) @ 0b1 @ _ : bits(20) as op_code) = { L : bits(1) = [op_code[21]]; o0 : bits(1) = [op_code[19]]; op1 : bits(3) = op_code[18 .. 16]; @@ -643,7 +643,7 @@ function clause decode 0b1101010100 @ _ : bits(1) @ 0b1 @ _ : bits(20) as op_cod system_register_system_decode(L, o0, op1, CRn, CRm, op2, Rt) } -function clause decode _ : bits(2) @ 0b111010010 @ _ : bits(9) @ 0b10 @ _ : bits(5) @ 0b0 @ _ : bits(4) as op_code = { +function clause decode (_ : bits(2) @ 0b111010010 @ _ : bits(9) @ 0b10 @ _ : bits(5) @ 0b0 @ _ : bits(4) as op_code) = { sf : bits(1) = [op_code[31]]; op : bits(1) = [op_code[30]]; S : bits(1) = [op_code[29]]; @@ -656,7 +656,7 @@ function clause decode _ : bits(2) @ 0b111010010 @ _ : bits(9) @ 0b10 @ _ : bits integer_conditional_compare_immediate_decode(sf, op, S, imm5, cond, o2, Rn, o3, nzcv) } -function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b000110 @ _ : bits(10) as op_code = { +function clause decode (0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b000110 @ _ : bits(10) as op_code) = { M : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; typ : bits(2) = op_code[23 .. 22]; @@ -666,7 +666,7 @@ function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b000110 @ float_arithmetic_div_decode(M, S, typ, Rm, Rn, Rd) } -function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b100000 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b100000 @ _ : bits(10) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; A : bits(1) = [op_code[23]]; @@ -679,7 +679,7 @@ function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b1 @ _ : bits(5) memory_atomicops_swp_decode(size, V, A, R, Rs, o3, opc, Rn, Rt) } -function clause decode _ : bits(3) @ 0b10001 @ _ : bits(24) as op_code = { +function clause decode (_ : bits(3) @ 0b10001 @ _ : bits(24) as op_code) = { sf : bits(1) = [op_code[31]]; op : bits(1) = [op_code[30]]; S : bits(1) = [op_code[29]]; @@ -690,13 +690,13 @@ function clause decode _ : bits(3) @ 0b10001 @ _ : bits(24) as op_code = { integer_arithmetic_addsub_immediate_decode(sf, op, S, shift, imm12, Rn, Rd) } -function clause decode _ : bits(1) @ 0b00101 @ _ : bits(26) as op_code = { +function clause decode (_ : bits(1) @ 0b00101 @ _ : bits(26) as op_code) = { op : bits(1) = [op_code[31]]; imm26 : bits(26) = op_code[25 .. 0]; branch_unconditional_immediate_decode(op, imm26) } -function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b110 @ _ : bits(10) as op_code = { +function clause decode (0b110110101100000100 @ _ : bits(1) @ 0b110 @ _ : bits(10) as op_code) = { sf : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; opcode2 : bits(5) = op_code[20 .. 16]; @@ -706,7 +706,7 @@ function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b110 @ _ : bits(10) integer_pac_autda_dp_1src_decode(sf, S, opcode2, Z, Rn, Rd) } -function clause decode _ : bits(1) @ 0b10110101100000000010 @ _ : bits(11) as op_code = { +function clause decode (_ : bits(1) @ 0b10110101100000000010 @ _ : bits(11) as op_code) = { sf : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; opcode2 : bits(5) = op_code[20 .. 16]; @@ -716,7 +716,7 @@ function clause decode _ : bits(1) @ 0b10110101100000000010 @ _ : bits(11) as op integer_arithmetic_cnt_decode(sf, S, opcode2, op, Rn, Rd) } -function clause decode _ : bits(2) @ 0b111 @ _ : bits(1) @ 0b00 @ _ : bits(2) @ 0b1 @ _ : bits(9) @ 0b00 @ _ : bits(5) @ 0b11111 as op_code = { +function clause decode (_ : bits(2) @ 0b111 @ _ : bits(1) @ 0b00 @ _ : bits(2) @ 0b1 @ _ : bits(9) @ 0b00 @ _ : bits(5) @ 0b11111 as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; A : bits(1) = [op_code[23]]; @@ -729,7 +729,7 @@ function clause decode _ : bits(2) @ 0b111 @ _ : bits(1) @ 0b00 @ _ : bits(2) @ memory_atomicops_st_decode(size, V, A, R, Rs, o3, opc, Rn, Rt) } -function clause decode 0b11010101000000110011 @ _ : bits(4) @ 0b1 @ _ : bits(2) @ 0b11111 as op_code = { +function clause decode (0b11010101000000110011 @ _ : bits(4) @ 0b1 @ _ : bits(2) @ 0b11111 as op_code) = { L : bits(1) = [op_code[21]]; op0 : bits(2) = op_code[20 .. 19]; op1 : bits(3) = op_code[18 .. 16]; @@ -740,7 +740,7 @@ function clause decode 0b11010101000000110011 @ _ : bits(4) @ 0b1 @ _ : bits(2) system_barriers_decode(L, op0, op1, CRn, CRm, opc, Rt) } -function clause decode 0b0 @ _ : bits(1) @ 0b0010000 @ _ : bits(1) @ 0b1 @ _ : bits(21) as op_code = { +function clause decode (0b0 @ _ : bits(1) @ 0b0010000 @ _ : bits(1) @ 0b1 @ _ : bits(21) as op_code) = { sz : bits(1) = [op_code[30]]; o2 : bits(1) = [op_code[23]]; L : bits(1) = [op_code[22]]; @@ -753,7 +753,7 @@ function clause decode 0b0 @ _ : bits(1) @ 0b0010000 @ _ : bits(1) @ 0b1 @ _ : b memory_atomicops_cas_pair_decode(sz, o2, L, o1, Rs, o0, Rt2, Rn, Rt) } -function clause decode _ : bits(3) @ 0b100101 @ _ : bits(23) as op_code = { +function clause decode (_ : bits(3) @ 0b100101 @ _ : bits(23) as op_code) = { sf : bits(1) = [op_code[31]]; opc : bits(2) = op_code[30 .. 29]; hw : bits(2) = op_code[22 .. 21]; @@ -762,7 +762,7 @@ function clause decode _ : bits(3) @ 0b100101 @ _ : bits(23) as op_code = { integer_insext_insert_movewide_decode(sf, opc, hw, imm16, Rd) } -function clause decode 0b11010110101111110000001111100000 as op_code = { +function clause decode (0b11010110101111110000001111100000 as op_code) = { opc : bits(4) = op_code[24 .. 21]; op2 : bits(5) = op_code[20 .. 16]; op3 : bits(6) = op_code[15 .. 10]; @@ -771,7 +771,7 @@ function clause decode 0b11010110101111110000001111100000 as op_code = { branch_unconditional_dret_decode(opc, op2, op3, Rt, op4) } -function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(9) @ 0b11 @ _ : bits(10) as op_code = { +function clause decode (0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(9) @ 0b11 @ _ : bits(10) as op_code) = { M : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; typ : bits(2) = op_code[23 .. 22]; @@ -782,7 +782,7 @@ function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(9) @ 0b11 @ _ : float_move_fp_select_decode(M, S, typ, Rm, cond, Rn, Rd) } -function clause decode 0b11010100101 @ _ : bits(16) @ 0b000 @ _ : bits(2) as op_code = { +function clause decode (0b11010100101 @ _ : bits(16) @ 0b000 @ _ : bits(2) as op_code) = { opc : bits(3) = op_code[23 .. 21]; imm16 : bits(16) = op_code[20 .. 5]; op2 : bits(3) = op_code[4 .. 2]; @@ -790,7 +790,7 @@ function clause decode 0b11010100101 @ _ : bits(16) @ 0b000 @ _ : bits(2) as op_ system_exceptions_debug_exception_decode(opc, imm16, op2, LL) } -function clause decode _ : bits(1) @ 0b1011010110000000000 @ _ : bits(12) as op_code = { +function clause decode (_ : bits(1) @ 0b1011010110000000000 @ _ : bits(12) as op_code) = { sf : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; opcode2 : bits(5) = op_code[20 .. 16]; @@ -800,7 +800,7 @@ function clause decode _ : bits(1) @ 0b1011010110000000000 @ _ : bits(12) as op_ integer_arithmetic_rev_decode(sf, S, opcode2, opc, Rn, Rd) } -function clause decode 0b00011110 @ _ : bits(2) @ 0b10001 @ _ : bits(2) @ 0b10000 @ _ : bits(10) as op_code = { +function clause decode (0b00011110 @ _ : bits(2) @ 0b10001 @ _ : bits(2) @ 0b10000 @ _ : bits(10) as op_code) = { M : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; typ : bits(2) = op_code[23 .. 22]; @@ -810,7 +810,7 @@ function clause decode 0b00011110 @ _ : bits(2) @ 0b10001 @ _ : bits(2) @ 0b1000 float_convert_fp_decode(M, S, typ, opc, Rn, Rd) } -function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b000 @ _ : bits(10) as op_code = { +function clause decode (0b110110101100000100 @ _ : bits(1) @ 0b000 @ _ : bits(10) as op_code) = { sf : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; opcode2 : bits(5) = op_code[20 .. 16]; @@ -820,7 +820,7 @@ function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b000 @ _ : bits(10) integer_pac_pacia_dp_1src_decode(sf, S, opcode2, Z, Rn, Rd) } -function clause decode 0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code = { +function clause decode (0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code) = { L : bits(1) = [op_code[21]]; op0 : bits(2) = op_code[20 .. 19]; op1 : bits(3) = op_code[18 .. 16]; @@ -831,7 +831,7 @@ function clause decode 0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code integer_pac_pacia_hint_decode(L, op0, op1, CRn, CRm, op2, Rt) } -function clause decode _ : bits(1) @ 0b0011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b000000 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(1) @ 0b0011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b000000 @ _ : bits(10) as op_code) = { sf : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; typ : bits(2) = op_code[23 .. 22]; @@ -842,7 +842,7 @@ function clause decode _ : bits(1) @ 0b0011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) float_convert_int_decode(sf, S, typ, rmode, opcode, Rn, Rd) } -function clause decode _ : bits(2) @ 0b011010100 @ _ : bits(9) @ 0b0 @ _ : bits(11) as op_code = { +function clause decode (_ : bits(2) @ 0b011010100 @ _ : bits(9) @ 0b0 @ _ : bits(11) as op_code) = { sf : bits(1) = [op_code[31]]; op : bits(1) = [op_code[30]]; S : bits(1) = [op_code[29]]; @@ -854,7 +854,7 @@ function clause decode _ : bits(2) @ 0b011010100 @ _ : bits(9) @ 0b0 @ _ : bits( integer_conditional_select_decode(sf, op, S, Rm, cond, o2, Rn, Rd) } -function clause decode _ : bits(2) @ 0b111000101 @ _ : bits(5) @ 0b110000 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(2) @ 0b111000101 @ _ : bits(5) @ 0b110000 @ _ : bits(10) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; A : bits(1) = [op_code[23]]; @@ -867,7 +867,7 @@ function clause decode _ : bits(2) @ 0b111000101 @ _ : bits(5) @ 0b110000 @ _ : memory_orderedrcpc_decode(size, V, A, R, Rs, o3, opc, Rn, Rt) } -function clause decode _ : bits(3) @ 0b01011001 @ _ : bits(21) as op_code = { +function clause decode (_ : bits(3) @ 0b01011001 @ _ : bits(21) as op_code) = { sf : bits(1) = [op_code[31]]; op : bits(1) = [op_code[30]]; S : bits(1) = [op_code[29]]; @@ -880,7 +880,7 @@ function clause decode _ : bits(3) @ 0b01011001 @ _ : bits(21) as op_code = { integer_arithmetic_addsub_extendedreg_decode(sf, op, S, opt, Rm, option_name, imm3, Rn, Rd) } -function clause decode _ : bits(3) @ 0b10000 @ _ : bits(24) as op_code = { +function clause decode (_ : bits(3) @ 0b10000 @ _ : bits(24) as op_code) = { op : bits(1) = [op_code[31]]; immlo : bits(2) = op_code[30 .. 29]; immhi : bits(19) = op_code[23 .. 5]; @@ -888,7 +888,7 @@ function clause decode _ : bits(3) @ 0b10000 @ _ : bits(24) as op_code = { integer_arithmetic_address_pcrel_decode(op, immlo, immhi, Rd) } -function clause decode 0b0 @ _ : bits(1) @ 0b0011010 @ _ : bits(2) @ 0b00000 @ _ : bits(16) as op_code = { +function clause decode (0b0 @ _ : bits(1) @ 0b0011010 @ _ : bits(2) @ 0b00000 @ _ : bits(16) as op_code) = { Q : bits(1) = [op_code[30]]; L : bits(1) = [op_code[22]]; R : bits(1) = [op_code[21]]; @@ -900,7 +900,7 @@ function clause decode 0b0 @ _ : bits(1) @ 0b0011010 @ _ : bits(2) @ 0b00000 @ _ memory_vector_single_nowb_aarch64_memory_vector_single_nowb__decode(Q, L, R, opcode, S, size, Rn, Rt) } -function clause decode 0b0 @ _ : bits(1) @ 0b0011011 @ _ : bits(23) as op_code = { +function clause decode (0b0 @ _ : bits(1) @ 0b0011011 @ _ : bits(23) as op_code) = { Q : bits(1) = [op_code[30]]; L : bits(1) = [op_code[22]]; R : bits(1) = [op_code[21]]; @@ -913,7 +913,7 @@ function clause decode 0b0 @ _ : bits(1) @ 0b0011011 @ _ : bits(23) as op_code = memory_vector_single_postinc_aarch64_memory_vector_single_nowb__decode(Q, L, R, Rm, opcode, S, size, Rn, Rt) } -function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b1 @ _ : bits(10) @ 0b1 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b1 @ _ : bits(10) @ 0b1 @ _ : bits(10) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; M : bits(1) = [op_code[23]]; @@ -925,7 +925,7 @@ function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b1 @ _ : bits(10) memory_single_general_immediate_signed_pac_decode(size, V, M, S, imm9, W, Rn, Rt) } -function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b101 @ _ : bits(10) as op_code = { +function clause decode (0b110110101100000100 @ _ : bits(1) @ 0b101 @ _ : bits(10) as op_code) = { sf : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; opcode2 : bits(5) = op_code[20 .. 16]; @@ -935,7 +935,7 @@ function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b101 @ _ : bits(10) integer_pac_autib_dp_1src_decode(sf, S, opcode2, Z, Rn, Rd) } -function clause decode 0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code = { +function clause decode (0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code) = { L : bits(1) = [op_code[21]]; op0 : bits(2) = op_code[20 .. 19]; op1 : bits(3) = op_code[18 .. 16]; @@ -946,7 +946,7 @@ function clause decode 0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code integer_pac_autib_hint_decode(L, op0, op1, CRn, CRm, op2, Rt) } -function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(9) @ 0b01 @ _ : bits(10) as op_code = { +function clause decode (0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(9) @ 0b01 @ _ : bits(10) as op_code) = { M : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; typ : bits(2) = op_code[23 .. 22]; @@ -958,7 +958,7 @@ function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(9) @ 0b01 @ _ : float_compare_cond_decode(M, S, typ, Rm, cond, Rn, op, nzcv) } -function clause decode _ : bits(2) @ 0b0010000 @ _ : bits(1) @ 0b0 @ _ : bits(21) as op_code = { +function clause decode (_ : bits(2) @ 0b0010000 @ _ : bits(1) @ 0b0 @ _ : bits(21) as op_code) = { size : bits(2) = op_code[31 .. 30]; o2 : bits(1) = [op_code[23]]; L : bits(1) = [op_code[22]]; @@ -971,7 +971,7 @@ function clause decode _ : bits(2) @ 0b0010000 @ _ : bits(1) @ 0b0 @ _ : bits(21 memory_exclusive_single_decode(size, o2, L, o1, Rs, o0, Rt2, Rn, Rt) } -function clause decode _ : bits(1) @ 0b0011110 @ _ : bits(2) @ 0b0 @ _ : bits(21) as op_code = { +function clause decode (_ : bits(1) @ 0b0011110 @ _ : bits(2) @ 0b0 @ _ : bits(21) as op_code) = { sf : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; typ : bits(2) = op_code[23 .. 22]; @@ -983,7 +983,7 @@ function clause decode _ : bits(1) @ 0b0011110 @ _ : bits(2) @ 0b0 @ _ : bits(21 float_convert_fix_decode(sf, S, typ, rmode, opcode, scale, Rn, Rd) } -function clause decode 0b00011110 @ _ : bits(2) @ 0b1001 @ _ : bits(3) @ 0b10000 @ _ : bits(10) as op_code = { +function clause decode (0b00011110 @ _ : bits(2) @ 0b1001 @ _ : bits(3) @ 0b10000 @ _ : bits(10) as op_code) = { M : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; typ : bits(2) = op_code[23 .. 22]; @@ -993,7 +993,7 @@ function clause decode 0b00011110 @ _ : bits(2) @ 0b1001 @ _ : bits(3) @ 0b10000 float_arithmetic_round_decode(M, S, typ, rmode, Rn, Rd) } -function clause decode _ : bits(3) @ 0b01010 @ _ : bits(24) as op_code = { +function clause decode (_ : bits(3) @ 0b01010 @ _ : bits(24) as op_code) = { sf : bits(1) = [op_code[31]]; opc : bits(2) = op_code[30 .. 29]; shift : bits(2) = op_code[23 .. 22]; @@ -1005,7 +1005,7 @@ function clause decode _ : bits(3) @ 0b01010 @ _ : bits(24) as op_code = { integer_logical_shiftedreg_decode(sf, opc, shift, N, Rm, imm6, Rn, Rd) } -function clause decode _ : bits(1) @ 0b0011010110 @ _ : bits(5) @ 0b010 @ _ : bits(13) as op_code = { +function clause decode (_ : bits(1) @ 0b0011010110 @ _ : bits(5) @ 0b010 @ _ : bits(13) as op_code) = { sf : bits(1) = [op_code[31]]; op : bits(1) = [op_code[30]]; S : bits(1) = [op_code[29]]; @@ -1018,7 +1018,7 @@ function clause decode _ : bits(1) @ 0b0011010110 @ _ : bits(5) @ 0b010 @ _ : bi integer_crc_decode(sf, op, S, Rm, opcode2, C, sz, Rn, Rd) } -function clause decode _ : bits(3) @ 0b11010000 @ _ : bits(5) @ 0b000000 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(3) @ 0b11010000 @ _ : bits(5) @ 0b000000 @ _ : bits(10) as op_code) = { sf : bits(1) = [op_code[31]]; op : bits(1) = [op_code[30]]; S : bits(1) = [op_code[29]]; @@ -1029,7 +1029,7 @@ function clause decode _ : bits(3) @ 0b11010000 @ _ : bits(5) @ 0b000000 @ _ : b integer_arithmetic_addsub_carry_decode(sf, op, S, Rm, opcode2, Rn, Rd) } -function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b001000 @ _ : bits(7) @ 0b000 as op_code = { +function clause decode (0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b001000 @ _ : bits(7) @ 0b000 as op_code) = { M : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; typ : bits(2) = op_code[23 .. 22]; @@ -1040,7 +1040,7 @@ function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b001000 @ float_compare_uncond_decode(M, S, typ, Rm, op, Rn, opc) } -function clause decode 0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code = { +function clause decode (0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code) = { L : bits(1) = [op_code[21]]; op0 : bits(2) = op_code[20 .. 19]; op1 : bits(3) = op_code[18 .. 16]; @@ -1051,7 +1051,7 @@ function clause decode 0b11010101000000110010 @ _ : bits(7) @ 0b11111 as op_code system_hints_decode(L, op0, op1, CRn, CRm, op2, Rt) } -function clause decode _ : bits(1) @ 0b0011010110 @ _ : bits(5) @ 0b0010 @ _ : bits(12) as op_code = { +function clause decode (_ : bits(1) @ 0b0011010110 @ _ : bits(5) @ 0b0010 @ _ : bits(12) as op_code) = { sf : bits(1) = [op_code[31]]; op : bits(1) = [op_code[30]]; S : bits(1) = [op_code[29]]; @@ -1063,7 +1063,7 @@ function clause decode _ : bits(1) @ 0b0011010110 @ _ : bits(5) @ 0b0010 @ _ : b integer_shift_variable_decode(sf, op, S, Rm, opcode2, op2, Rn, Rd) } -function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b011 @ _ : bits(10) as op_code = { +function clause decode (0b110110101100000100 @ _ : bits(1) @ 0b011 @ _ : bits(10) as op_code) = { sf : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; opcode2 : bits(5) = op_code[20 .. 16]; @@ -1073,7 +1073,7 @@ function clause decode 0b110110101100000100 @ _ : bits(1) @ 0b011 @ _ : bits(10) integer_pac_pacdb_dp_1src_decode(sf, S, opcode2, Z, Rn, Rd) } -function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b0 @ _ : bits(9) @ 0b10 @ _ : bits(10) as op_code = { +function clause decode (_ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b0 @ _ : bits(9) @ 0b10 @ _ : bits(10) as op_code) = { size : bits(2) = op_code[31 .. 30]; V : bits(1) = [op_code[26]]; opc : bits(2) = op_code[23 .. 22]; @@ -1083,7 +1083,7 @@ function clause decode _ : bits(2) @ 0b111000 @ _ : bits(2) @ 0b0 @ _ : bits(9) memory_single_general_immediate_signed_offset_unpriv_aarch64_memory_single_general_immediate_signed_offset_unpriv__decode(size, V, opc, imm9, Rn, Rt) } -function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b001 @ _ : bits(1) @ 0b10 @ _ : bits(10) as op_code = { +function clause decode (0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b001 @ _ : bits(1) @ 0b10 @ _ : bits(10) as op_code) = { M : bits(1) = [op_code[31]]; S : bits(1) = [op_code[29]]; typ : bits(2) = op_code[23 .. 22]; @@ -1094,7 +1094,7 @@ function clause decode 0b00011110 @ _ : bits(2) @ 0b1 @ _ : bits(5) @ 0b001 @ _ float_arithmetic_addsub_decode(M, S, typ, Rm, op, Rn, Rd) } -function clause decode _ : bits(1) @ 0b00100111 @ _ : bits(1) @ 0b0 @ _ : bits(21) as op_code = { +function clause decode (_ : bits(1) @ 0b00100111 @ _ : bits(1) @ 0b0 @ _ : bits(21) as op_code) = { sf : bits(1) = [op_code[31]]; op21 : bits(2) = op_code[30 .. 29]; N : bits(1) = [op_code[22]]; @@ -1106,7 +1106,7 @@ function clause decode _ : bits(1) @ 0b00100111 @ _ : bits(1) @ 0b0 @ _ : bits(2 integer_insext_extract_immediate_decode(sf, op21, N, o0, Rm, imms, Rn, Rd) } -function clause decode 0b11010100010 @ _ : bits(16) @ 0b00000 as op_code = { +function clause decode (0b11010100010 @ _ : bits(16) @ 0b00000 as op_code) = { opc : bits(3) = op_code[23 .. 21]; imm16 : bits(16) = op_code[20 .. 5]; op2 : bits(3) = op_code[4 .. 2]; @@ -1114,7 +1114,7 @@ function clause decode 0b11010100010 @ _ : bits(16) @ 0b00000 as op_code = { system_exceptions_debug_halt_decode(opc, imm16, op2, LL) } -function clause decode 0b10011011 @ _ : bits(1) @ 0b01 @ _ : bits(21) as op_code = { +function clause decode (0b10011011 @ _ : bits(1) @ 0b01 @ _ : bits(21) as op_code) = { sf : bits(1) = [op_code[31]]; op54 : bits(2) = op_code[30 .. 29]; U : bits(1) = [op_code[23]]; @@ -1126,7 +1126,7 @@ function clause decode 0b10011011 @ _ : bits(1) @ 0b01 @ _ : bits(21) as op_code integer_arithmetic_mul_widening_3264_decode(sf, op54, U, Rm, o0, Ra, Rn, Rd) } -function clause decode _ : bits(1) @ 0b0011010110 @ _ : bits(5) @ 0b00001 @ _ : bits(11) as op_code = { +function clause decode (_ : bits(1) @ 0b0011010110 @ _ : bits(5) @ 0b00001 @ _ : bits(11) as op_code) = { sf : bits(1) = [op_code[31]]; op : bits(1) = [op_code[30]]; S : bits(1) = [op_code[29]]; diff --git a/aarch64/mono/demo/aarch64_no_vector/aarch64_no_vector.sail b/aarch64/mono/demo/aarch64_no_vector/spec.sail index 22b1e3a1..0bdd8f68 100644 --- a/aarch64/mono/demo/aarch64_no_vector/aarch64_no_vector.sail +++ b/aarch64/mono/demo/aarch64_no_vector/spec.sail @@ -1027,9 +1027,9 @@ function WaitForInterrupt () = { () } -val EndOfInstruction : unit -> unit +val EndOfInstruction : unit -> unit effect {escape} -function EndOfInstruction () = () +function EndOfInstruction () = throw(Error_ExceptionTaken()) register ESR_EL3 : bits(32) @@ -1702,9 +1702,9 @@ function ExternalInvasiveDebugEnabled () = return(DBGEN == HIGH) val ConstrainUnpredictableInteger : (int, int, Unpredictable) -> (Constraint, int) effect {undef} -function ConstrainUnpredictableInteger (low, high, which) = { +function ConstrainUnpredictableInteger ('low, 'high, which) = { c : Constraint = ConstrainUnpredictable(which); - if c == Constraint_UNKNOWN then return((c, low)) else return((c, undefined : int)) + if c == Constraint_UNKNOWN then return((c, low)) else return((c, undefined)) } val ConstrainUnpredictableBool : Unpredictable -> bool effect {escape} @@ -1803,7 +1803,7 @@ function LookUpRIndex ('n, mode) = { return(result) } -val HighestSetBit : forall ('N : Int), 'N >= 2. bits('N) -> int +val HighestSetBit : forall ('N : Int), 'N >= 0. bits('N) -> int function HighestSetBit x = { foreach (i from ('N - 1) to 0 by 1 in dec) @@ -1813,18 +1813,19 @@ function HighestSetBit x = { val CountLeadingZeroBits : forall ('N : Int), 'N >= 2. bits('N) -> int -function CountLeadingZeroBits x = return('N - 1 - HighestSetBit(x)) +function CountLeadingZeroBits x = return(('N - 1) - HighestSetBit(x)) val CountLeadingSignBits : forall ('N : Int), 'N >= 3. bits('N) -> int function CountLeadingSignBits x = return(CountLeadingZeroBits((x >> 1) ^ (x & slice_mask(0,'N)))) -val BitReverse : forall ('N : Int), 'N >= 2. bits('N) -> bits('N) effect {undef} +val BitReverse : forall ('N : Int), 'N >= 0 & 'N >= 0. + bits('N) -> bits('N) effect {undef} function BitReverse data = { result : bits('N) = undefined; foreach (i from 0 to ('N - 1) by 1 in inc) - result['N - i - 1 .. 'N - i - 1] = [data[i]]; + result = __SetSlice_bits('N, 1, result, ('N - i) - 1, [data[i]]); return(result) } @@ -1946,7 +1947,7 @@ val BigEndianReverse : forall ('width : Int), 'width >= 0 & 'width >= 0. bits('width) -> bits('width) effect {escape} function BigEndianReverse value_name = { - assert(('width == 8) | (('width == 16) | (('width == 32) | (('width == 64) | ('width == 128))))); + assert('width == 8 | 'width == 16 | 'width == 32 | 'width == 64 | 'width == 128); result : bits('width) = replicate_bits(0b0,'width); foreach (i from 0 to ('width - 1) by 8) result[i+7 .. i] = (value_name['width-i - 1 .. 'width-i - 8] : bits(8)); @@ -2062,10 +2063,8 @@ val Replicate : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0. bits('M) -> bits('N) effect {escape} function Replicate x = { - assert(('N % 'M) == 0, "((N MOD M) == 0)"); - let 'p = ex_int('N / 'M); - assert(constraint('N = 'p * 'M)); - return(replicate_bits(x, p)) + assert('N % 'M == 0, "((N MOD M) == 0)"); + return(replicate_bits(x, 'N / 'M)) } val Zeros__0 : forall ('N : Int), 'N >= 0. atom('N) -> bits('N) @@ -2094,7 +2093,7 @@ val ZeroExtend__1 : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0. overload ZeroExtend = {ZeroExtend__0, ZeroExtend__1} function ZeroExtend__0 (x, N) = { - assert(true); + assert('N >= 'M); extzv(x) } @@ -2151,7 +2150,7 @@ function aset_SP value_name = { val LSR_C : forall ('N : Int), 'N >= 0 & 'N >= 0 & 1 >= 0. (bits('N), int) -> (bits('N), bits(1)) effect {escape} -function LSR_C (x, shift) = { +function LSR_C (x, 'shift) = { assert(shift > 0, "(shift > 0)"); result : bits('N) = x >> shift; carry_out : bits(1) = if shift > 'N then 0b0 else [x[shift - 1]]; @@ -2184,7 +2183,7 @@ function Poly32Mod2 (data__arg, poly) = { val LSL_C : forall ('N : Int), 'N >= 0 & 'N >= 0 & 1 >= 0. (bits('N), int) -> (bits('N), bits(1)) effect {escape} -function LSL_C (x, shift) = { +function LSL_C (x, 'shift) = { assert(shift > 0, "(shift > 0)"); result : bits('N) = x << shift; carry_out : bits(1) = if shift > 'N then 0b0 else [x['N - shift]]; @@ -2232,8 +2231,8 @@ val AddWithCarry : forall ('N : Int), 'N >= 0 & 'N >= 0 & 1 >= 0 & 'N >= 0 & 4 > (bits('N), bits('N), bits(1)) -> (bits('N), bits(4)) function AddWithCarry (x, y, carry_in) = { - unsigned_sum : int = UInt(x) + UInt(y) + UInt(carry_in); - signed_sum : int = SInt(x) + SInt(y) + UInt(carry_in); + unsigned_sum : int = (UInt(x) + UInt(y)) + UInt(carry_in); + signed_sum : int = (SInt(x) + SInt(y)) + UInt(carry_in); result : bits('N) = __GetSlice_int('N, unsigned_sum, 0); n : bits(1) = [result['N - 1]]; z : bits(1) = if IsZero(result) then 0b1 else 0b0; @@ -2282,7 +2281,7 @@ val FPZero : forall ('N : Int), 1 >= 0 & 'N >= 0. function FPZero sign = { assert('N == 16 | 'N == 32 | 'N == 64, "((N == 16) || ((N == 32) || (N == 64)))"); let 'E = (if 'N == 16 then 5 else if 'N == 32 then 8 else 11) : {|5, 8, 11|}; - F : atom('N - 'E - 1) = 'N - E - 1; + F : atom('N - 'E - 1) = ('N - E) - 1; exp : bits('E) = Zeros(E); frac : bits('N - 1 - 'E) = Zeros(F); return(append(append(sign, exp), frac)) @@ -2305,7 +2304,7 @@ val ConstrainUnpredictableBits : forall ('width : Int), 'width >= 0. function ConstrainUnpredictableBits which = { c : Constraint = ConstrainUnpredictable(which); - if c == Constraint_UNKNOWN then return((c, Zeros('width))) else return((c, undefined : bits('width))) + if c == Constraint_UNKNOWN then return((c, Zeros('width))) else return((c, undefined)) } val AArch64_SysInstrWithResult : (int, int, int, int, int) -> bits(64) effect {escape} @@ -2338,7 +2337,7 @@ val VFPExpandImm : forall ('N : Int), 8 >= 0 & 'N >= 0. function VFPExpandImm imm8 = { assert('N == 16 | 'N == 32 | 'N == 64, "((N == 16) || ((N == 32) || (N == 64)))"); let 'E = (if 'N == 16 then 5 else if 'N == 32 then 8 else 11) : {|5, 8, 11|}; - F : atom('N - 'E - 1) = 'N - E - 1; + F : atom('N - 'E - 1) = ('N - E) - 1; sign : bits(1) = [imm8[7]]; exp : bits('E) = append(append(~([imm8[6]]), replicate_bits([imm8[6]], E - 3)), imm8[5 .. 4]); frac : bits('N - 1 - 'E) = append(imm8[3 .. 0], Zeros(F - 4)); @@ -2375,7 +2374,7 @@ function Extend__1 (x, unsigned) = return(Extend(x, 'N, unsigned)) val ASR_C : forall ('N : Int), 'N >= 0 & 'N >= 0 & 1 >= 0. (bits('N), int) -> (bits('N), bits(1)) effect {escape} -function ASR_C (x, shift) = { +function ASR_C (x, 'shift) = { assert(shift > 0, "(shift > 0)"); result : bits('N) = arith_shiftright(x, shift); carry_out : bits(1) = if shift > 'N then [x['N - 1]] else [x[shift - 1]]; @@ -2413,7 +2412,7 @@ val FPMaxNormal : forall ('N : Int), 1 >= 0 & 'N >= 0. function FPMaxNormal sign = { assert('N == 16 | 'N == 32 | 'N == 64, "((N == 16) || ((N == 32) || (N == 64)))"); let 'E = (if 'N == 16 then 5 else if 'N == 32 then 8 else 11) : {|5, 8, 11|}; - F : atom('N - 'E - 1) = 'N - E - 1; + F : atom('N - 'E - 1) = ('N - E) - 1; exp : bits('E) = append(Ones(E - 1), 0b0); frac : bits('N - 1 - 'E) = Ones(F); return(append(append(sign, exp), frac)) @@ -2425,7 +2424,7 @@ val FPInfinity : forall ('N : Int), 1 >= 0 & 'N >= 0. function FPInfinity sign = { assert('N == 16 | 'N == 32 | 'N == 64, "((N == 16) || ((N == 32) || (N == 64)))"); let 'E = (if 'N == 16 then 5 else if 'N == 32 then 8 else 11) : {|5, 8, 11|}; - F : atom('N - 'E - 1) = 'N - E - 1; + F : atom('N - 'E - 1) = ('N - E) - 1; exp : bits('E) = Ones(E); frac : bits('N - 1 - 'E) = Zeros(F); return(append(append(sign, exp), frac)) @@ -2436,7 +2435,7 @@ val FPDefaultNaN : forall ('N : Int), 'N >= 0. unit -> bits('N) effect {escape} function FPDefaultNaN () = { assert('N == 16 | 'N == 32 | 'N == 64, "((N == 16) || ((N == 32) || (N == 64)))"); let 'E = (if 'N == 16 then 5 else if 'N == 32 then 8 else 11) : {|5, 8, 11|}; - F : atom('N - 'E - 1) = 'N - E - 1; + F : atom('N - 'E - 1) = ('N - E) - 1; sign : bits(1) = 0b0; exp : bits('E) = Ones(E); frac : bits('N - 1 - 'E) = append(0b1, Zeros(F - 1)); @@ -2546,7 +2545,7 @@ function PACInvSub Tinput = { return(Toutput) } -val ComputePAC : (bits(64), bits(64), bits(64), bits(64)) -> bits(64) effect {rreg, undef, wreg, escape} +val ComputePAC : (bits(64), bits(64), bits(64), bits(64)) -> bits(64) effect {escape, rreg, undef, wreg} function ComputePAC (data, modifier, key0, key1) = { workingval : bits(64) = undefined; @@ -2609,7 +2608,7 @@ val Align__1 : forall ('N : Int), 'N >= 0 & 'N >= 0. (bits('N), int) -> bits('N) overload Align = {Align__0, Align__1} -function Align__0 ('x, 'y) = return(y * x / y) +function Align__0 ('x, 'y) = return(y * (x / y)) function Align__1 (x, 'y) = return(__GetSlice_int('N, Align(UInt(x), y), 0)) @@ -2739,17 +2738,15 @@ function aarch64_integer_insext_extract_immediate ('d, 'datasize, 'lsb, 'm, 'n) aset_X(d, result) } -val aarch64_integer_arithmetic_rev : (int, int, int, int) -> unit effect {escape, wreg, undef, rreg} +val aarch64_integer_arithmetic_rev : (int, int, int, int) -> unit effect {escape, rreg, undef, wreg} -function aarch64_integer_arithmetic_rev ('container_size, 'd, 'datasize, 'n) = { +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('container_size >= 0 + 1)); + assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); operand : bits('datasize) = aget_X(n); result : bits('datasize) = undefined; - let 'containers : int = datasize / container_size; - assert(constraint('containers * 'container_size = 'datasize)); - let 'elements_per_container : int = container_size / 8; - assert(constraint('elements_per_container * 8 = 'container_size)); + containers : int = datasize / container_size; + elements_per_container : int = container_size / 8; index : int = 0; rev_index : int = undefined; foreach (c from 0 to (containers - 1) by 1 in inc) { @@ -2771,7 +2768,7 @@ function aarch64_integer_arithmetic_rbit ('d, 'datasize, 'n) = let 'dbytes = ex_ operand : bits('datasize) = aget_X(n); result : bits('datasize) = undefined; foreach (i from 0 to (datasize - 1) by 1 in inc) - result = __SetSlice_bits(datasize, 1, result, datasize - 1 - i, [operand[i]]); + result = __SetSlice_bits(datasize, 1, result, (datasize - 1) - i, [operand[i]]); aset_X(d, result) } @@ -2926,7 +2923,7 @@ function aarch64_integer_arithmetic_addsub_carry ('d, 'datasize, 'm, 'n, setflag nzcv : bits(4) = undefined; if sub_op then operand2 = ~(operand2) else (); (result, nzcv) = AddWithCarry(operand1, operand2, PSTATE.C); - if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = nzcv else (); + if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = nzcv else (); aset_X(d, result) } @@ -3100,7 +3097,7 @@ function aarch64_integer_logical_shiftedreg ('d, 'datasize, invert, 'm, 'n, op, LogicalOp_ORR => result = operand1 | operand2, LogicalOp_EOR => result = operand1 ^ operand2 }; - if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = ([result[datasize - 1]] @ IsZeroBit(result)) @ 0b00 else (); + if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = ([result[datasize - 1]] @ IsZeroBit(result)) @ 0b00 else (); aset_X(d, result) } @@ -3119,7 +3116,7 @@ function aarch64_integer_arithmetic_addsub_shiftedreg ('d, 'datasize, 'm, 'n, se carry_in = 0b1 } else carry_in = 0b0; (result, nzcv) = AddWithCarry(operand1, operand2, carry_in); - if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = nzcv else (); + if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = nzcv else (); aset_X(d, result) } @@ -3252,7 +3249,7 @@ function aarch64_integer_logical_immediate ('d, datasize, imm, 'n, op, setflags) LogicalOp_ORR => result = operand1 | operand2, LogicalOp_EOR => result = operand1 ^ operand2 }; - if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = ([result[datasize - 1]] @ IsZeroBit(result)) @ 0b00 else (); + if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = ([result[datasize - 1]] @ IsZeroBit(result)) @ 0b00 else (); if d == 31 & ~(setflags) then aset_SP(result) else aset_X(d, result) } @@ -3272,7 +3269,7 @@ function aarch64_integer_arithmetic_addsub_immediate ('d, datasize, imm, 'n, set carry_in = 0b1 } else carry_in = 0b0; (result, nzcv) = AddWithCarry(operand1, operand2, carry_in); - if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = nzcv else (); + if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = nzcv else (); if d == 31 & ~(setflags) then aset_SP(result) else aset_X(d, result) } @@ -3291,7 +3288,7 @@ function aarch64_integer_arithmetic_addsub_extendedreg ('d, 'datasize, extend_ty carry_in = 0b1 } else carry_in = 0b0; (result, nzcv) = AddWithCarry(operand1, operand2, carry_in); - if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = nzcv else (); + if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = nzcv else (); if d == 31 & ~(setflags) then aset_SP(result) else aset_X(d, result) } @@ -3364,18 +3361,18 @@ function Auth (ptr, modifier, K, data, keynumber) = { assert(constraint('bottom_PAC_bit >= 0)); extfield = replicate_bits([ptr[55]], 64); if tbi then - original_ptr = (ptr[63 .. 56] @ extfield[negate(bottom_PAC_bit) + 56 - 1 .. 0]) @ ptr[bottom_PAC_bit - 1 .. 0] + original_ptr = (ptr[63 .. 56] @ extfield[(negate(bottom_PAC_bit) + 56) - 1 .. 0]) @ ptr[bottom_PAC_bit - 1 .. 0] else - original_ptr = extfield[negate(bottom_PAC_bit) + 64 - 1 .. 0] @ ptr[bottom_PAC_bit - 1 .. 0]; + original_ptr = extfield[(negate(bottom_PAC_bit) + 64) - 1 .. 0] @ ptr[bottom_PAC_bit - 1 .. 0]; PAC = ComputePAC(original_ptr, modifier, K[127 .. 64], K[63 .. 0]); if tbi then - if PAC[negate(bottom_PAC_bit) + 55 - 1 + bottom_PAC_bit .. bottom_PAC_bit] == ptr[negate(bottom_PAC_bit) + 55 - 1 + bottom_PAC_bit .. bottom_PAC_bit] then + if PAC[((negate(bottom_PAC_bit) + 55) - 1) + bottom_PAC_bit .. bottom_PAC_bit] == ptr[((negate(bottom_PAC_bit) + 55) - 1) + bottom_PAC_bit .. bottom_PAC_bit] then result = original_ptr else { error_code = keynumber @ ~(keynumber); result = (original_ptr[63 .. 55] @ error_code) @ original_ptr[52 .. 0] } - else if PAC[negate(bottom_PAC_bit) + 55 - 1 + bottom_PAC_bit .. bottom_PAC_bit] == ptr[negate(bottom_PAC_bit) + 55 - 1 + bottom_PAC_bit .. bottom_PAC_bit] & PAC[63 .. 56] == ptr[63 .. 56] then + else if PAC[((negate(bottom_PAC_bit) + 55) - 1) + bottom_PAC_bit .. bottom_PAC_bit] == ptr[((negate(bottom_PAC_bit) + 55) - 1) + bottom_PAC_bit .. bottom_PAC_bit] & PAC[63 .. 56] == ptr[63 .. 56] then result = original_ptr else { error_code = keynumber @ ~(keynumber); @@ -3530,8 +3527,8 @@ function FPRoundBase (op, fpcr, rounding) = { else FPSR = __SetSlice_bits(32, 1, FPSR, 3, 0b1); return(FPZero(sign)) } else (); - biased_exp : int = max(exponent - minimum_exp + 1, 0); - if biased_exp == 0 then mantissa = mantissa / (2.0 ^ (minimum_exp - exponent)) + biased_exp : int = max((exponent - minimum_exp) + 1, 0); + if biased_exp == 0 then mantissa = mantissa / 2.0 ^ (minimum_exp - exponent) else (); int_mant : int = RoundDown(mantissa * 2.0 ^ F); error : real = mantissa * 2.0 ^ F - Real(int_mant); @@ -3578,13 +3575,13 @@ function FPRoundBase (op, fpcr, rounding) = { FPProcessException(FPExc_Overflow, fpcr); error = 1.0 } else - result = (sign @ __GetSlice_int('N - F - 1, biased_exp, 0)) @ __GetSlice_int(F, int_mant, 0) + result = (sign @ __GetSlice_int(('N - F) - 1, biased_exp, 0)) @ __GetSlice_int(F, int_mant, 0) else if biased_exp >= pow2(E) then { result = sign @ Ones('N - 1); FPProcessException(FPExc_InvalidOp, fpcr); error = 0.0 } else - result = (sign @ __GetSlice_int('N - F - 1, biased_exp, 0)) @ __GetSlice_int(F, int_mant, 0); + result = (sign @ __GetSlice_int(('N - F) - 1, biased_exp, 0)) @ __GetSlice_int(F, int_mant, 0); if error != 0.0 then FPProcessException(FPExc_Inexact, fpcr) else (); return(result) } @@ -3624,7 +3621,7 @@ function FixedToFP (op, 'fbits, unsigned, fpcr, rounding) = { assert(fbits >= 0); assert(rounding != FPRounding_ODD); int_operand : int = asl_Int(op, unsigned); - real_operand : real = Real(int_operand) / (2.0 ^ fbits); + real_operand : real = Real(int_operand) / 2.0 ^ fbits; if real_operand == 0.0 then result = FPZero(0b0) else result = FPRound(real_operand, fpcr, rounding); return(result) @@ -3970,7 +3967,7 @@ function FPToFixedJS (op, fpcr, Is64) = { } else (); if sign == 0b1 & value_name == 0.0 then Z = 0b0 else (); if typ == FPType_Infinity then result = 0 else (); - if Is64 then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = (0b0 @ Z) @ 0b00 else FPSCR = __SetSlice_bits(32, 4, FPSCR, 28, (0b0 @ Z) @ 0b00); + if Is64 then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = (0b0 @ Z) @ 0b00 else FPSCR = __SetSlice_bits(32, 4, FPSCR, 28, (0b0 @ Z) @ 0b00); return(__GetSlice_int(32, result, 0)) } @@ -4477,11 +4474,11 @@ function Halt reason = { else assert([EDSCR[16]] == 0b1, "((EDSCR).SDD == '1')"); EDSCR[20 .. 20] = 0b0; if UsingAArch32() then { - (PSTATE.SS, PSTATE.A, PSTATE.I, PSTATE.F) = undefined : bits(4); + (PSTATE.SS @ PSTATE.A @ PSTATE.I @ PSTATE.F) = undefined : bits(4); PSTATE.IT = 0x00; PSTATE.T = 0b1 } else - (PSTATE.SS, PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = undefined : bits(5); + (PSTATE.SS @ PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = undefined : bits(5); PSTATE.IL = 0b0; StopInstructionPrefetchAndEnableITR(); EDSCR[5 .. 0] = reason; @@ -4913,7 +4910,7 @@ function aarch64_integer_conditional_compare_register (condition, 'datasize, fla } else (); (__anon1, flags) = AddWithCarry(operand1, operand2, carry_in) } else (); - (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = flags + (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = flags } val integer_conditional_compare_register_decode : (bits(1), bits(1), bits(1), bits(5), bits(4), bits(1), bits(5), bits(1), bits(4)) -> unit effect {escape, rreg, undef, wreg} @@ -4947,7 +4944,7 @@ function aarch64_integer_conditional_compare_immediate (condition, datasize, fla } else (); (__anon1, flags) = AddWithCarry(operand1, operand2, carry_in) } else (); - (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = flags + (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = flags } val integer_conditional_compare_immediate_decode : (bits(1), bits(1), bits(1), bits(5), bits(4), bits(1), bits(5), bits(1), bits(4)) -> unit effect {escape, wreg, undef, rreg} @@ -5183,17 +5180,17 @@ function AddPAC (ptr, modifier, K, data) = { assert(constraint('bottom_PAC_bit <= 55)); extfield = replicate_bits(selbit, 64); if tbi then - ext_ptr = (ptr[63 .. 56] @ extfield[negate(bottom_PAC_bit) + 56 - 1 .. 0]) @ ptr[bottom_PAC_bit - 1 .. 0] + ext_ptr = (ptr[63 .. 56] @ extfield[(negate(bottom_PAC_bit) + 56) - 1 .. 0]) @ ptr[bottom_PAC_bit - 1 .. 0] else - ext_ptr = extfield[negate(bottom_PAC_bit) + 64 - 1 .. 0] @ ptr[bottom_PAC_bit - 1 .. 0]; + ext_ptr = extfield[(negate(bottom_PAC_bit) + 64) - 1 .. 0] @ ptr[bottom_PAC_bit - 1 .. 0]; PAC = ComputePAC(ext_ptr, modifier, K[127 .. 64], K[63 .. 0]); - if ~(IsZero(ptr[top_bit - bottom_PAC_bit + 1 - 1 + bottom_PAC_bit .. bottom_PAC_bit])) & ~(IsOnes(ptr[top_bit - bottom_PAC_bit + 1 - 1 + bottom_PAC_bit .. bottom_PAC_bit])) then + if ~(IsZero(ptr[(((top_bit - bottom_PAC_bit) + 1) - 1) + bottom_PAC_bit .. bottom_PAC_bit])) & ~(IsOnes(ptr[(((top_bit - bottom_PAC_bit) + 1) - 1) + bottom_PAC_bit .. bottom_PAC_bit])) then PAC[top_bit - 1 .. top_bit - 1] = ~([PAC[top_bit - 1]]) else (); if tbi then - result = ((ptr[63 .. 56] @ selbit) @ PAC[negate(bottom_PAC_bit) + 55 - 1 + bottom_PAC_bit .. bottom_PAC_bit]) @ ptr[bottom_PAC_bit - 1 .. 0] + result = ((ptr[63 .. 56] @ selbit) @ PAC[((negate(bottom_PAC_bit) + 55) - 1) + bottom_PAC_bit .. bottom_PAC_bit]) @ ptr[bottom_PAC_bit - 1 .. 0] else - result = ((PAC[63 .. 56] @ selbit) @ PAC[negate(bottom_PAC_bit) + 55 - 1 + bottom_PAC_bit .. bottom_PAC_bit]) @ ptr[bottom_PAC_bit - 1 .. 0]; + result = ((PAC[63 .. 56] @ selbit) @ PAC[((negate(bottom_PAC_bit) + 55) - 1) + bottom_PAC_bit .. bottom_PAC_bit]) @ ptr[bottom_PAC_bit - 1 .. 0]; return(result) } @@ -5246,12 +5243,12 @@ function AArch64_WatchpointByteMatch (n, vaddress) = let 'top : {'n, true. atom( let 'bottom2 : {'n, true. atom('n)} = ex_int(bottom); if mask > bottom then { assert(constraint('mask2 >= 'bottom2 + 1)); - WVR_match = vaddress[top - mask2 + 1 - 1 + mask2 .. mask2] == DBGWVR_EL1[n][top - mask2 + 1 - 1 + mask2 .. mask2]; - if WVR_match & ~(IsZero(DBGWVR_EL1[n][mask2 - bottom2 - 1 + bottom2 .. bottom2])) then + WVR_match = vaddress[(((top - mask2) + 1) - 1) + mask2 .. mask2] == DBGWVR_EL1[n][(((top - mask2) + 1) - 1) + mask2 .. mask2]; + if WVR_match & ~(IsZero(DBGWVR_EL1[n][((mask2 - bottom2) - 1) + bottom2 .. bottom2])) then WVR_match = ConstrainUnpredictableBool(Unpredictable_WPMASKEDBITS) else () } else - WVR_match = vaddress[top - bottom2 + 1 - 1 + bottom2 .. bottom2] == DBGWVR_EL1[n][top - bottom2 + 1 - 1 + bottom2 .. bottom2]; + WVR_match = vaddress[(((top - bottom2) + 1) - 1) + bottom2 .. bottom2] == DBGWVR_EL1[n][(((top - bottom2) + 1) - 1) + bottom2 .. bottom2]; return(WVR_match & byte_select_match) } @@ -5339,7 +5336,7 @@ function AArch64_TranslationTableWalk (ipaddress, vaddress, acctype, iswrite, se else () } else (); ps = slice(TCR_EL3, 16, 3); - basefound = (inputsize >= inputsize_min & inputsize <= inputsize_max) & IsZero_slice(inputaddr, inputsize, top - inputsize + 1); + basefound = (inputsize >= inputsize_min & inputsize <= inputsize_max) & IsZero_slice(inputaddr, inputsize, (top - inputsize) + 1); disabled = false; baseregister = TTBR0_EL3; descaddr.memattrs = WalkAttrDecode(slice(TCR_EL3, 12, 2), slice(TCR_EL3, 10, 2), slice(TCR_EL3, 8, 2), secondstage); @@ -5368,7 +5365,7 @@ function AArch64_TranslationTableWalk (ipaddress, vaddress, acctype, iswrite, se if c == Constraint_FORCE then inputsize = inputsize_min else () } else (); - basefound = (inputsize >= inputsize_min & inputsize <= inputsize_max) & IsZero_slice(inputaddr, inputsize, top - inputsize + 1); + basefound = (inputsize >= inputsize_min & inputsize <= inputsize_max) & IsZero_slice(inputaddr, inputsize, (top - inputsize) + 1); disabled = [TCR_EL2[7]] == 0b1; baseregister = TTBR0_EL2; descaddr.memattrs = WalkAttrDecode(slice(TCR_EL2, 12, 2), slice(TCR_EL2, 10, 2), slice(TCR_EL2, 8, 2), secondstage); @@ -5391,7 +5388,7 @@ function AArch64_TranslationTableWalk (ipaddress, vaddress, acctype, iswrite, se if c == Constraint_FORCE then inputsize = inputsize_min else () } else (); - basefound = (inputsize >= inputsize_min & inputsize <= inputsize_max) & IsOnes_slice(inputaddr, inputsize, top - inputsize + 1); + basefound = (inputsize >= inputsize_min & inputsize <= inputsize_max) & IsOnes_slice(inputaddr, inputsize, (top - inputsize) + 1); disabled = [TCR_EL2[23]] == 0b1; baseregister = TTBR1_EL2; descaddr.memattrs = WalkAttrDecode(slice(TCR_EL2, 28, 2), slice(TCR_EL2, 26, 2), slice(TCR_EL2, 24, 2), secondstage); @@ -5422,7 +5419,7 @@ function AArch64_TranslationTableWalk (ipaddress, vaddress, acctype, iswrite, se else () } else (); ps = slice(TCR_EL2, 16, 3); - basefound = (inputsize >= inputsize_min & inputsize <= inputsize_max) & IsZero_slice(inputaddr, inputsize, top - inputsize + 1); + basefound = (inputsize >= inputsize_min & inputsize <= inputsize_max) & IsZero_slice(inputaddr, inputsize, (top - inputsize) + 1); disabled = false; baseregister = TTBR0_EL2; descaddr.memattrs = WalkAttrDecode(slice(TCR_EL2, 12, 2), slice(TCR_EL2, 10, 2), slice(TCR_EL2, 8, 2), secondstage); @@ -5451,7 +5448,7 @@ function AArch64_TranslationTableWalk (ipaddress, vaddress, acctype, iswrite, se if c == Constraint_FORCE then inputsize = inputsize_min else () } else (); - basefound = (inputsize >= inputsize_min & inputsize <= inputsize_max) & IsZero_slice(inputaddr, inputsize, top - inputsize + 1); + basefound = (inputsize >= inputsize_min & inputsize <= inputsize_max) & IsZero_slice(inputaddr, inputsize, (top - inputsize) + 1); disabled = [TCR_EL1[7]] == 0b1; baseregister = TTBR0_EL1; descaddr.memattrs = WalkAttrDecode(slice(TCR_EL1, 12, 2), slice(TCR_EL1, 10, 2), slice(TCR_EL1, 8, 2), secondstage); @@ -5474,7 +5471,7 @@ function AArch64_TranslationTableWalk (ipaddress, vaddress, acctype, iswrite, se if c == Constraint_FORCE then inputsize = inputsize_min else () } else (); - basefound = (inputsize >= inputsize_min & inputsize <= inputsize_max) & IsOnes_slice(inputaddr, inputsize, top - inputsize + 1); + basefound = (inputsize >= inputsize_min & inputsize <= inputsize_max) & IsOnes_slice(inputaddr, inputsize, (top - inputsize) + 1); disabled = [TCR_EL1[23]] == 0b1; baseregister = TTBR1_EL1; descaddr.memattrs = WalkAttrDecode(slice(TCR_EL1, 28, 2), slice(TCR_EL1, 26, 2), slice(TCR_EL1, 24, 2), secondstage); @@ -5592,7 +5589,7 @@ function AArch64_TranslationTableWalk (ipaddress, vaddress, acctype, iswrite, se result.addrdesc = __tmp_20; return(result) } else (); - let 'baselowerbound = (3 + inputsize - ((3 - level) * stride + grainsize)) : int; + let 'baselowerbound = ((3 + inputsize) - ((3 - level) * stride + grainsize)) : int; assert(constraint(0 <= 'baselowerbound & 'baselowerbound <= 48)); baseaddress : bits(52) = undefined; if outputsize == 52 then let 'z = (if baselowerbound < 6 then 6 else baselowerbound) : int in { @@ -5614,7 +5611,7 @@ function AArch64_TranslationTableWalk (ipaddress, vaddress, acctype, iswrite, se addrselectbottom : int = undefined; repeat { addrselectbottom = (3 - level) * stride + grainsize; - index : bits(52) = ZeroExtend_slice_append(inputaddr, addrselectbottom, addrselecttop - addrselectbottom + 1, 0b000); + index : bits(52) = ZeroExtend_slice_append(inputaddr, addrselectbottom, (addrselecttop - addrselectbottom) + 1, 0b000); __tmp_21 : FullAddress = descaddr.paddress; __tmp_21.physicaladdress = baseaddress | index; descaddr.paddress = __tmp_21; @@ -5861,7 +5858,7 @@ function AArch64_TranslateAddressS1Off (vaddress, acctype, iswrite) = { secondstage : bool = undefined; ipaddress : bits(52) = undefined; level : int = undefined; - if ~(IsZero_slice2(vaddress, PAMax(), Top + 1 - PAMax())) then { + if ~(IsZero_slice2(vaddress, PAMax(), (Top + 1) - PAMax())) then { level = 0; ipaddress = undefined; secondstage = false; @@ -6006,13 +6003,13 @@ function AArch64_TranslateAddressS1Off (vaddress, acctype, iswrite) = { return(result) } -val AArch64_MaybeZeroRegisterUppers : unit -> unit effect {wreg, undef, rreg, escape} +val AArch64_MaybeZeroRegisterUppers : unit -> unit effect {escape, rreg, undef, wreg} function AArch64_MaybeZeroRegisterUppers () = { assert(UsingAArch32(), "UsingAArch32()"); include_R15_name : bool = undefined; - last : range(14, 30) = undefined; - first : atom(0) = 0; + last : int = undefined; + first : int = undefined; if PSTATE.EL == EL0 & ~(ELUsingAArch32(EL1)) then { first = 0; last = 14; @@ -6027,9 +6024,9 @@ function AArch64_MaybeZeroRegisterUppers () = { include_R15_name = true }; foreach (n from first to last by 1 in inc) - if (n : int != 15 : int | include_R15_name) & ConstrainUnpredictableBool(Unpredictable_ZEROUPPER) then { + if (n != 15 | include_R15_name) & ConstrainUnpredictableBool(Unpredictable_ZEROUPPER) then { __tmp_3 : bits(64) = _R[n]; - __tmp_3[63 .. 32] = Zeros(32); + __tmp_3 = __SetSlice_bits(64, 32, __tmp_3, 32, Zeros()); _R[n] = __tmp_3 } else (); () @@ -6492,7 +6489,7 @@ function AArch64_TranslationTableWalk_SecondStage (ipaddress, vaddress, acctype, result.addrdesc = __tmp_20; return(result) } else (); - let 'baselowerbound = (3 + inputsize - ((3 - level) * stride + grainsize)) : int; + let 'baselowerbound = ((3 + inputsize) - ((3 - level) * stride + grainsize)) : int; assert(constraint(0 <= 'baselowerbound & 'baselowerbound <= 48)); baseaddress : bits(52) = undefined; if outputsize == 52 then let 'z = (if baselowerbound < 6 then 6 else baselowerbound) : int in { @@ -6514,7 +6511,7 @@ function AArch64_TranslationTableWalk_SecondStage (ipaddress, vaddress, acctype, addrselectbottom : int = undefined; repeat { addrselectbottom = (3 - level) * stride + grainsize; - index : bits(52) = ZeroExtend_slice_append(inputaddr, addrselectbottom, addrselecttop - addrselectbottom + 1, 0b000); + index : bits(52) = ZeroExtend_slice_append(inputaddr, addrselectbottom, (addrselecttop - addrselectbottom) + 1, 0b000); __tmp_21 : FullAddress = descaddr.paddress; __tmp_21.physicaladdress = baseaddress | index; descaddr.paddress = __tmp_21; @@ -6802,9 +6799,21 @@ function AArch64_StateMatch (SSC__arg, HMC__arg, PxC__arg, linked__arg, LBN, isb return((priv_match & security_state_match) & (~(linked) | linked_match)) } -val AArch64_WatchpointMatch : (int, bits(64), int, bool, bool) -> bool +val AArch64_WatchpointMatch : (int, bits(64), int, bool, bool) -> bool effect {escape, rreg, undef} -function AArch64_WatchpointMatch (n, vaddress, size, ispriv, iswrite) = false +function AArch64_WatchpointMatch ('n, vaddress, 'size, ispriv, iswrite) = { + assert(~(ELUsingAArch32(S1TranslationRegime())), "!(ELUsingAArch32(S1TranslationRegime()))"); + assert(n <= UInt(slice(ID_AA64DFR0_EL1, 20, 4)), "(n <= UInt((ID_AA64DFR0_EL1).WRPs))"); + enabled : bool = [DBGWCR_EL1[n][0]] == 0b1; + linked : bool = [DBGWCR_EL1[n][20]] == 0b1; + isbreakpnt : bool = false; + state_match : bool = AArch64_StateMatch(slice(DBGWCR_EL1[n], 14, 2), [DBGWCR_EL1[n][13]], slice(DBGWCR_EL1[n], 1, 2), linked, slice(DBGWCR_EL1[n], 16, 4), isbreakpnt, ispriv); + ls_match : bool = [slice(DBGWCR_EL1[n], 3, 2)[if iswrite then 1 else 0]] == 0b1; + value_match_name : bool = false; + foreach (byte from 0 to (size - 1) by 1 in inc) + value_match_name = value_match_name | AArch64_WatchpointByteMatch(n, vaddress + byte); + return(((value_match_name & state_match) & ls_match) & enabled) +} val AArch64_BreakpointMatch : (int, bits(64), int) -> bool effect {escape, rreg, undef} @@ -6957,7 +6966,7 @@ function AArch64_TakeReset cold_reset = { else PSTATE.EL = EL1; AArch64_ResetControlRegisters(cold_reset); PSTATE.SP = 0b1; - (PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = 0xF; + (PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = 0xF; PSTATE.SS = 0b0; PSTATE.IL = 0b0; AArch64_ResetGeneralRegisters(); @@ -6993,11 +7002,18 @@ function AArch64_TakeException (target_el, exception, preferred_exception_return if from_32 then AArch64_MaybeZeroRegisterUppers() else (); if UInt(target_el) > UInt(PSTATE.EL) then { lower_32 : bool = undefined; - if target_el == EL3 then if ~(IsSecure()) & HaveEL(EL2) then lower_32 = ELUsingAArch32(EL2) else lower_32 = ELUsingAArch32(EL1) else if (IsInHost() & PSTATE.EL == EL0) & target_el == EL2 then lower_32 = ELUsingAArch32(EL0) else lower_32 = ELUsingAArch32(target_el - 1); + if target_el == EL3 then + if ~(IsSecure()) & HaveEL(EL2) then lower_32 = ELUsingAArch32(EL2) + else lower_32 = ELUsingAArch32(EL1) + else if (IsInHost() & PSTATE.EL == EL0) & target_el == EL2 then + lower_32 = ELUsingAArch32(EL0) + else lower_32 = ELUsingAArch32(target_el - 1); vect_offset = vect_offset + (if lower_32 then 1536 else 1024) - } else if PSTATE.SP == 0b1 then vect_offset = vect_offset + 512 else (); + } else if PSTATE.SP == 0b1 then vect_offset = vect_offset + 512 + else (); spsr : bits(32) = GetPSRFromPSTATE(); - if HaveUAOExt() then PSTATE.UAO = 0b0 else (); + if HaveUAOExt() then PSTATE.UAO = 0b0 + else (); if ~(exception.typ == Exception_IRQ | exception.typ == Exception_FIQ) then AArch64_ReportException(exception, target_el) else (); PSTATE.EL = target_el; PSTATE.nRW = 0b0; @@ -7005,13 +7021,15 @@ function AArch64_TakeException (target_el, exception, preferred_exception_return aset_SPSR(spsr); aset_ELR(preferred_exception_return); PSTATE.SS = 0b0; - (PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = 0xF; + (PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = 0xF; PSTATE.IL = 0b0; if from_32 then { PSTATE.IT = 0x00; PSTATE.T = 0b0 } else (); - if (HavePANExt() & (PSTATE.EL == EL1 | PSTATE.EL == EL2 & ELIsInHost(EL0))) & [aget_SCTLR()[23]] == 0b0 then PSTATE.PAN = 0b1 else (); + if (HavePANExt() & (PSTATE.EL == EL1 | PSTATE.EL == EL2 & ELIsInHost(EL0))) & [aget_SCTLR()[23]] == 0b0 then + PSTATE.PAN = 0b1 + else (); BranchTo(slice(aget_VBAR(), 11, 53) @ __GetSlice_int(11, vect_offset, 0), BranchType_EXCEPTION); iesb_req : bool = undefined; if HaveRASExt() & [aget_SCTLR()[21]] == 0b1 then { @@ -7962,7 +7980,7 @@ function AArch32_EnterMode (target_mode, preferred_exception_return, 'lr_offset, aset_R(14, preferred_exception_return + lr_offset); PSTATE.T = [SCTLR[30]]; PSTATE.SS = 0b0; - if target_mode == M32_FIQ then (PSTATE.A, PSTATE.I, PSTATE.F) = 0b111 else if target_mode == M32_Abort | target_mode == M32_IRQ then (PSTATE.A, PSTATE.I) = 0b11 else PSTATE.I = 0b1; + if target_mode == M32_FIQ then (PSTATE.A @ PSTATE.I @ PSTATE.F) = 0b111 else if target_mode == M32_Abort | target_mode == M32_IRQ then (PSTATE.A @ PSTATE.I) = 0b11 else PSTATE.I = 0b1; PSTATE.E = [SCTLR[25]]; PSTATE.IL = 0b0; PSTATE.IT = 0x00; @@ -8122,7 +8140,7 @@ function aarch64_float_compare_uncond (cmp_with_zero, 'datasize, 'm, 'n, signal_ CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = if cmp_with_zero then FPZero(0b0) else aget_V(m); - (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = FPCompare(operand1, operand2, signal_all_nans, FPCR) + (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = FPCompare(operand1, operand2, signal_all_nans, FPCR) } val aarch64_float_compare_cond : (bits(4), int, bits(4), int, int, bool) -> unit effect {escape, rreg, undef, wreg} @@ -8135,7 +8153,7 @@ function aarch64_float_compare_cond (condition, 'datasize, flags__arg, 'm, 'n, s operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); if ConditionHolds(condition) then flags = FPCompare(operand1, operand2, signal_all_nans, FPCR) else (); - (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = flags + (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = flags } val aarch64_float_arithmetic_unary : (int, int, FPUnaryOp, int) -> unit effect {escape, rreg, undef, wreg} @@ -8527,7 +8545,7 @@ function aarch64_memory_vector_single_nowb (datasize, esize, index, m, memop, n, element = aget_Mem(address + offs, ebytes, AccType_VEC); let 'v : {'n, true. atom('n)} = ex_int(datasize / esize) in { assert(constraint('esize * 'v = 'datasize)); - aset_V(t, replicate_bits(element, 'v)) + aset_V(t, replicate_bits(element, v)) }; offs = offs + ebytes; t = (t + 1) % 32 @@ -8587,11 +8605,11 @@ function aarch64_memory_vector_multiple_nowb (datasize, elements, esize, m, memo } else () } -val aarch64_memory_single_simdfp_register : forall ('datasize : Int). - (AccType, atom('datasize), ExtendType, int, MemOp, int, bool, int, int, bool) -> unit effect {escape, rmem, wmem, undef, wreg, rreg} +val aarch64_memory_single_simdfp_register : (AccType, int, ExtendType, int, MemOp, int, bool, int, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_simdfp_register (acctype, datasize, extend_type, m, memop, n, postindex, shift, t, wback) = { +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"); offset : bits(64) = ExtendReg(m, extend_type, shift); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; @@ -8600,32 +8618,28 @@ function aarch64_memory_single_simdfp_register (acctype, datasize, extend_type, CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); - let 'dq8 = ex_int(datasize / 8); - assert(constraint(8 * 'dq8 = 'datasize)); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { data = aget_V(t); - aset_Mem(address, dq8, acctype, data) + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dq8, acctype); + data = aget_Mem(address, datasize / 8, acctype); aset_V(t, data) } }; if wback then { - if postindex then address = address + offset - else (); + if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } -val aarch64_memory_single_simdfp_immediate_signed_postidx : forall ('datasize : Int). - (AccType, atom('datasize), MemOp, int, bits(64), bool, int, bool) -> unit effect {escape, rmem, wmem, undef, wreg, rreg} +val aarch64_memory_single_simdfp_immediate_signed_postidx : (AccType, int, MemOp, int, bits(64), bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_simdfp_immediate_signed_postidx (acctype, datasize, memop, n, offset, postindex, t, wback) = { +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"); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -8633,32 +8647,28 @@ function aarch64_memory_single_simdfp_immediate_signed_postidx (acctype, datasiz CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); - let 'dq8 = ex_int(datasize / 8); - assert(constraint('dq8 * 8 = 'datasize)); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { data = aget_V(t); - aset_Mem(address, dq8, acctype, data) + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dq8, acctype); + data = aget_Mem(address, datasize / 8, acctype); aset_V(t, data) } }; if wback then { - if postindex then address = address + offset - else (); + if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } -val aarch64_memory_single_simdfp_immediate_signed_offset_normal : forall ('datasize : Int). - (AccType, atom('datasize), MemOp, int, bits(64), bool, int, bool) -> unit effect {escape, undef, wreg, rreg, rmem, wmem} +val aarch64_memory_single_simdfp_immediate_signed_offset_normal : (AccType, int, MemOp, int, bits(64), bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_simdfp_immediate_signed_offset_normal (acctype, datasize, memop, n, offset, postindex, t, wback) = { +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"); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -8666,23 +8676,19 @@ function aarch64_memory_single_simdfp_immediate_signed_offset_normal (acctype, d CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); - let 'dq8 = ex_int(datasize / 8); - assert(constraint(8 * 'dq8 = 'datasize)); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { data = aget_V(t); - aset_Mem(address, dq8, acctype, data) + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dq8, acctype); + data = aget_Mem(address, datasize / 8, acctype); aset_V(t, data) } }; if wback then { - if postindex then address = address + offset - else (); + if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } @@ -8812,41 +8818,39 @@ function memory_literal_general_decode (opc, V, imm19, Rt) = { aarch64_memory_literal_general(memop, offset, signed, 8 * size, t) } -val aarch64_memory_atomicops_swp : forall ('datasize : Int) ('regsize : Int). - (atom('datasize), AccType, int, atom('regsize), int, AccType, int) -> unit effect {escape, undef, wreg, rreg, rmem, wmem} +val aarch64_memory_atomicops_swp : (int, AccType, int, int, int, AccType, int) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_atomicops_swp (datasize, ldacctype, n, regsize, s, stacctype, t) = { - assert(constraint('datasize in {8, 16, 32, 64, 128} & 'regsize >= 0), "datasize constraint"); +function aarch64_memory_atomicops_swp ('datasize, ldacctype, 'n, 'regsize, 's, stacctype, 't) = { + 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"); address : bits(64) = undefined; data : bits('datasize) = undefined; - let 'dbytes = ex_int(datasize / 8); - assert(constraint(8 * 'dbytes = 'datasize)); if n == 31 then { CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - data = aget_Mem(address, dbytes, ldacctype); - aset_Mem(address, dbytes, stacctype, aget_X(s)); + data = aget_Mem(address, datasize / 8, ldacctype); + aset_Mem(address, datasize / 8, stacctype, aget_X(s)); aset_X(t, ZeroExtend(data, regsize)) } -val aarch64_memory_atomicops_st : forall ('datasize : Int). - (atom('datasize), AccType, int, MemAtomicOp, int, AccType) -> unit effect {escape, undef, wreg, rreg, rmem, wmem} +val aarch64_memory_atomicops_st : (int, AccType, int, MemAtomicOp, int, AccType) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_atomicops_st (datasize, ldacctype, n, op, s, stacctype) = { +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"); address : bits(64) = undefined; value_name : bits('datasize) = undefined; data : bits('datasize) = undefined; result : bits('datasize) = undefined; value_name = aget_X(s); - let 'dbytes = ex_int(datasize / 8); - assert(constraint(8 * 'dbytes = 'datasize)); if n == 31 then { CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - data = aget_Mem(address, dbytes, ldacctype); + data = aget_Mem(address, datasize / 8, ldacctype); match op { MemAtomicOp_ADD => result = data + value_name, MemAtomicOp_BIC => result = data & ~(value_name), @@ -8857,26 +8861,26 @@ function aarch64_memory_atomicops_st (datasize, ldacctype, n, op, s, stacctype) MemAtomicOp_UMAX => result = if UInt(data) > UInt(value_name) then data else value_name, MemAtomicOp_UMIN => result = if UInt(data) > UInt(value_name) then value_name else data }; - aset_Mem(address, dbytes, stacctype, result) + aset_Mem(address, datasize / 8, stacctype, result) } -val aarch64_memory_atomicops_ld : forall ('datasize : Int) ('regsize : Int). - (atom('datasize), AccType, int, MemAtomicOp, atom('regsize), int, AccType, int) -> unit effect {escape, undef, wreg, rreg, rmem, wmem} +val aarch64_memory_atomicops_ld : (int, AccType, int, MemAtomicOp, int, int, AccType, int) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_atomicops_ld (datasize, ldacctype, n, op, regsize, s, stacctype, t) = { - assert(constraint('datasize in {8, 16, 32, 64, 128} & 'regsize >= 0), "datasize constraint"); +function aarch64_memory_atomicops_ld ('datasize, ldacctype, 'n, op, 'regsize, 's, stacctype, 't) = { + 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"); address : bits(64) = undefined; value_name : bits('datasize) = undefined; data : bits('datasize) = undefined; result : bits('datasize) = undefined; value_name = aget_X(s); - let 'dbytes = ex_int(datasize / 8); - assert(constraint(8 * 'dbytes = 'datasize)); if n == 31 then { CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - data = aget_Mem(address, dbytes, ldacctype); + data = aget_Mem(address, datasize / 8, ldacctype); match op { MemAtomicOp_ADD => result = data + value_name, MemAtomicOp_BIC => result = data & ~(value_name), @@ -8887,15 +8891,14 @@ function aarch64_memory_atomicops_ld (datasize, ldacctype, n, op, regsize, s, st MemAtomicOp_UMAX => result = if UInt(data) > UInt(value_name) then data else value_name, MemAtomicOp_UMIN => result = if UInt(data) > UInt(value_name) then value_name else data }; - aset_Mem(address, dbytes, stacctype, result); + aset_Mem(address, datasize / 8, stacctype, result); aset_X(t, ZeroExtend(data, regsize)) } -val aarch64_memory_atomicops_cas_single : forall ('datasize : Int) ('regsize : Int). - (atom('datasize), AccType, int, atom('regsize), int, AccType, int) -> unit effect {escape, undef, wreg, rreg, rmem, wmem} +val aarch64_memory_atomicops_cas_single : (int, AccType, int, int, int, AccType, int) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_atomicops_cas_single (datasize, ldacctype, n, regsize, s, stacctype, t) = { - assert(constraint('regsize >= 0), "destsize constraint"); +function aarch64_memory_atomicops_cas_single ('datasize, ldacctype, 'n, 'regsize, 's, stacctype, 't) = { + 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"); @@ -8909,19 +8912,18 @@ function aarch64_memory_atomicops_cas_single (datasize, ldacctype, n, regsize, s CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - data = aget_Mem(address, dbytes, ldacctype); - if data == comparevalue then aset_Mem(address, dbytes, stacctype, newvalue) else (); + data = aget_Mem(address, datasize / 8, ldacctype); + if data == comparevalue then aset_Mem(address, datasize / 8, stacctype, newvalue) else (); aset_X(s, ZeroExtend(data, regsize)) } -val aarch64_memory_atomicops_cas_pair : forall ('datasize : Int) ('regsize : Int). - (atom('datasize), AccType, int, atom('regsize), int, AccType, int) -> unit effect {escape, undef, wreg, rreg, rmem, wmem} +val aarch64_memory_atomicops_cas_pair : (int, AccType, int, int, int, AccType, int) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_atomicops_cas_pair (datasize, ldacctype, n, regsize, s, stacctype, t) = { - assert(constraint('regsize >= 0), "destsize constraint"); - let 'dbytes = ex_int((2 * datasize) / 8); +function aarch64_memory_atomicops_cas_pair ('datasize, ldacctype, 'n, 'regsize, 's, stacctype, 't) = { + 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(4 * '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; @@ -8936,8 +8938,8 @@ function aarch64_memory_atomicops_cas_pair (datasize, ldacctype, n, regsize, s, CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - data = aget_Mem(address, dbytes, ldacctype); - if data == comparevalue then aset_Mem(address, dbytes, stacctype, newvalue) else (); + data = aget_Mem(address, (2 * datasize) / 8, ldacctype); + if data == comparevalue then aset_Mem(address, (2 * datasize) / 8, stacctype, newvalue) else (); if BigEndian() then { aset_X(s, ZeroExtend(slice(data, datasize, datasize), regsize)); aset_X(s + 1, ZeroExtend(slice(data, 0, datasize), regsize)) @@ -9056,15 +9058,15 @@ function SetPSTATEFromPSR spsr__arg = { } }; if PSTATE.IL == 0b1 & PSTATE.nRW == 0b1 then if ConstrainUnpredictableBool(Unpredictable_ILZEROT) then spsr = __SetSlice_bits(32, 1, spsr, 5, 0b0) else () else (); - (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = slice(spsr, 28, 4); + (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = slice(spsr, 28, 4); if PSTATE.nRW == 0b1 then { PSTATE.Q = [spsr[27]]; PSTATE.IT = RestoredITBits(spsr); PSTATE.GE = slice(spsr, 16, 4); PSTATE.E = [spsr[9]]; - (PSTATE.A, PSTATE.I, PSTATE.F) = slice(spsr, 6, 3); + (PSTATE.A @ PSTATE.I @ PSTATE.F) = slice(spsr, 6, 3); PSTATE.T = [spsr[5]] - } else (PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = slice(spsr, 6, 4); + } else (PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = slice(spsr, 6, 4); if HavePANExt() then PSTATE.PAN = [spsr[22]] else (); if HaveUAOExt() then PSTATE.UAO = [spsr[23]] else (); () @@ -9077,13 +9079,13 @@ function DRPSInstruction () = { if (HaveRASExt() & [aget_SCTLR()[21]] == 0b1) & ConstrainUnpredictableBool(Unpredictable_IESBinDebug) then ErrorSynchronizationBarrier(MBReqDomain_FullSystem, MBReqTypes_All) else (); SetPSTATEFromPSR(aget_SPSR()); if UsingAArch32() then { - (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V, PSTATE.Q, PSTATE.GE, PSTATE.SS, PSTATE.A, PSTATE.I, PSTATE.F) = undefined : bits(13); + (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V @ PSTATE.Q @ PSTATE.GE @ PSTATE.SS @ PSTATE.A @ PSTATE.I @ PSTATE.F) = undefined : bits(13); PSTATE.IT = 0x00; PSTATE.T = 0b1; DLR = undefined : bits(32); DSPSR = undefined : bits(32) } else { - (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V, PSTATE.SS, PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = undefined : bits(9); + (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V @ PSTATE.SS @ PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = undefined : bits(9); DLR_EL0 = undefined : bits(64); DSPSR_EL0 = undefined : bits(32) }; @@ -9196,11 +9198,10 @@ function system_exceptions_runtime_hvc_decode (opc, imm16, op2, LL) = { aarch64_system_exceptions_runtime_hvc(imm) } -val aarch64_memory_single_general_register : forall ('datasize : Int) ('regsize : Int). - (AccType, atom('datasize), ExtendType, int, MemOp, int, bool, atom('regsize), int, bool, int, bool) -> unit effect {escape, undef, rreg, wreg, rmem, wmem} +val aarch64_memory_single_general_register : (AccType, int, ExtendType, int, MemOp, int, bool, int, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_general_register (acctype, datasize, extend_type, m, memop, n, postindex, regsize, shift, signed, t, wback__arg) = { - assert(constraint('regsize >= 0), "destsize constraint"); +function aarch64_memory_single_general_register (acctype, 'datasize, extend_type, 'm, memop, 'n, postindex, 'regsize, 'shift, signed, 't, wback__arg) = { + 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"); @@ -9235,33 +9236,28 @@ function aarch64_memory_single_general_register (acctype, datasize, extend_type, if memop != MemOp_PREFETCH then CheckSPAlignment() else (); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { - if rt_unknown then data = undefined - else data = aget_X(t); - aset_Mem(address, dbytes, acctype, data) + if rt_unknown then data = undefined else data = aget_X(t); + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dbytes, acctype); + data = aget_Mem(address, datasize / 8, acctype); if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize)) }, MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0)) }; if wback then { - if wb_unknown then address = undefined - else if postindex then address = address + offset - else (); + if wb_unknown then address = undefined else if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } -val aarch64_memory_single_general_immediate_unsigned : forall ('datasize : Int) ('regsize : Int). - (AccType, atom('datasize), MemOp, int, bits(64), bool, atom('regsize), bool, int, bool) -> unit effect {escape, undef, rreg, wreg, wmem, rmem} +val aarch64_memory_single_general_immediate_unsigned : (AccType, int, MemOp, int, bits(64), bool, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_general_immediate_unsigned (acctype, datasize, memop, n, offset, postindex, regsize, signed, t, wback__arg) = { - assert(constraint('regsize >= 0), "destsize constraint"); +function aarch64_memory_single_general_immediate_unsigned (acctype, 'datasize, memop, 'n, offset, postindex, 'regsize, signed, 't, wback__arg) = { + 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"); @@ -9295,33 +9291,28 @@ function aarch64_memory_single_general_immediate_unsigned (acctype, datasize, me if memop != MemOp_PREFETCH then CheckSPAlignment() else (); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { - if rt_unknown then data = undefined - else data = aget_X(t); - aset_Mem(address, dbytes, acctype, data) + if rt_unknown then data = undefined else data = aget_X(t); + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dbytes, acctype); + data = aget_Mem(address, datasize / 8, acctype); if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize)) }, MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0)) }; if wback then { - if wb_unknown then address = undefined - else if postindex then address = address + offset - else (); + if wb_unknown then address = undefined else if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } -val aarch64_memory_single_general_immediate_signed_postidx : forall ('datasize : Int) ('regsize : Int). - (AccType, atom('datasize), MemOp, int, bits(64), bool, atom('regsize), bool, int, bool) -> unit effect {escape, undef, rreg, wreg, wmem, rmem} +val aarch64_memory_single_general_immediate_signed_postidx : (AccType, int, MemOp, int, bits(64), bool, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_general_immediate_signed_postidx (acctype, datasize, memop, n, offset, postindex, regsize, signed, t, wback__arg) = { - assert(constraint('regsize >= 0), "destsize constraint"); +function aarch64_memory_single_general_immediate_signed_postidx (acctype, 'datasize, memop, 'n, offset, postindex, 'regsize, signed, 't, wback__arg) = { + 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"); @@ -9355,24 +9346,20 @@ function aarch64_memory_single_general_immediate_signed_postidx (acctype, datasi if memop != MemOp_PREFETCH then CheckSPAlignment() else (); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { - if rt_unknown then data = undefined - else data = aget_X(t); - aset_Mem(address, dbytes, acctype, data) + if rt_unknown then data = undefined else data = aget_X(t); + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dbytes, acctype); + data = aget_Mem(address, datasize / 8, acctype); if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize)) }, MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0)) }; if wback then { - if wb_unknown then address = undefined - else if postindex then address = address + offset - else (); + if wb_unknown then address = undefined else if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } @@ -9409,11 +9396,10 @@ function aarch64_memory_single_general_immediate_signed_pac ('n, offset, 't, use } else () } -val aarch64_memory_single_general_immediate_signed_offset_unpriv : forall ('datasize : Int) ('regsize : Int). - (AccType, atom('datasize), MemOp, int, bits(64), bool, atom('regsize), bool, int, bool) -> unit effect {escape, undef, rreg, wreg, rmem, wmem} +val aarch64_memory_single_general_immediate_signed_offset_unpriv : (AccType, int, MemOp, int, bits(64), bool, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype, datasize, memop, n, offset, postindex, regsize, signed, t, wback__arg) = { - assert(constraint('regsize >= 0), "destsize constraint"); +function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype, 'datasize, memop, 'n, offset, postindex, 'regsize, signed, 't, wback__arg) = { + 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"); @@ -9447,33 +9433,28 @@ function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype, if memop != MemOp_PREFETCH then CheckSPAlignment() else (); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { - if rt_unknown then data = undefined - else data = aget_X(t); - aset_Mem(address, dbytes, acctype, data) + if rt_unknown then data = undefined else data = aget_X(t); + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dbytes, acctype); + data = aget_Mem(address, datasize / 8, acctype); if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize)) }, MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0)) }; if wback then { - if wb_unknown then address = undefined - else if postindex then address = address + offset - else (); + if wb_unknown then address = undefined else if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } -val aarch64_memory_single_general_immediate_signed_offset_normal : forall ('datasize : Int) ('regsize : Int). - (AccType, atom('datasize), MemOp, int, bits(64), bool, atom('regsize), bool, int, bool) -> unit effect {escape, undef, rreg, wreg, rmem, wmem} +val aarch64_memory_single_general_immediate_signed_offset_normal : (AccType, int, MemOp, int, bits(64), bool, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_general_immediate_signed_offset_normal (acctype, datasize, memop, n, offset, postindex, regsize, signed, t, wback__arg) = { - assert(constraint('regsize >= 0), "destsize constraint"); +function aarch64_memory_single_general_immediate_signed_offset_normal (acctype, 'datasize, memop, 'n, offset, postindex, 'regsize, signed, 't, wback__arg) = { + 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"); @@ -9507,24 +9488,20 @@ function aarch64_memory_single_general_immediate_signed_offset_normal (acctype, if memop != MemOp_PREFETCH then CheckSPAlignment() else (); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { - if rt_unknown then data = undefined - else data = aget_X(t); - aset_Mem(address, dbytes, acctype, data) + if rt_unknown then data = undefined else data = aget_X(t); + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dbytes, acctype); + data = aget_Mem(address, datasize / 8, acctype); if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize)) }, MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0)) }; if wback then { - if wb_unknown then address = undefined - else if postindex then address = address + offset - else (); + if wb_unknown then address = undefined else if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } @@ -9944,10 +9921,10 @@ function aarch64_memory_exclusive_pair (acctype, datasize, elsize, memop, n, pai }, MemOp_LOAD => { AArch64_SetExclusiveMonitors(address, dbytes); - if pair then { - assert(constraint(- 'elsize + 'datasize > 0 & 'elsize >= 0), "datasize constraint"); + if pair then if rt_unknown then aset_X(t, undefined : bits(32)) else if elsize == 32 then { - data = aget_Mem(address, dbytes, acctype); + assert(constraint(- 'elsize + 'datasize > 0 & 'elsize >= 0), "datasize constraint"); + data = aget_Mem(address, dbytes, acctype); if BigEndian() then { aset_X(t, slice(data, elsize, negate(elsize) + datasize)); aset_X(t2, slice(data, 0, elsize)) @@ -9964,7 +9941,7 @@ function aarch64_memory_exclusive_pair (acctype, datasize, elsize, memop, n, pai aset_X(t, aget_Mem(address + 0, 8, acctype)); aset_X(t2, aget_Mem(address + 8, 8, acctype)) } - } else { + else { data = aget_Mem(address, dbytes, acctype); aset_X(t, ZeroExtend(data, regsize)) } diff --git a/aarch64/mono/demo/mk b/aarch64/mono/demo/mk index d8ee4a9e..64abea6f 100755 --- a/aarch64/mono/demo/mk +++ b/aarch64/mono/demo/mk @@ -1,8 +1,8 @@ #!/bin/bash set -ex ../../../sail ../../prelude.sail ../mono_rewrites.sail \ - aarch64_no_vector/aarch64_no_vector.sail aarch64_no_vector/decode_start.sail aarch64_no_vector/aarch64_no_vector_decode.sail aarch64_no_vector/decode_end.sail \ - -memo_z3 -undefined_gen \ + aarch64_no_vector/spec.sail aarch64_no_vector/decode_start.sail aarch64_no_vector/decode.sail aarch64_no_vector/decode_end.sail \ + -no_lexp_bounds_check -memo_z3 -undefined_gen \ -auto_mono -mono_rewrites -dall_split_errors -dmono_continue \ -lem -lem_mwords -lem_sequential -lem_lib Aarch64_extras -o aarch64_mono lem -isa -lib ../../../src/gen_lib/ -lib ../../../src/lem_interp ../aarch64_extras.lem aarch64_mono_types.lem aarch64_mono.lem diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 75b82da2..c743ac61 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -636,6 +636,7 @@ let nexp_subst_fns substs = | LEXP_tup les -> re (LEXP_tup (List.map s_lexp les)) | LEXP_vector (le,e) -> re (LEXP_vector (s_lexp le, s_exp e)) | LEXP_vector_range (le,e1,e2) -> re (LEXP_vector_range (s_lexp le, s_exp e1, s_exp e2)) + | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map s_lexp les)) | LEXP_field (le,id) -> re (LEXP_field (s_lexp le, id)) | LEXP_deref e -> re (LEXP_deref (s_exp e)) in (s_pat,s_exp) @@ -955,7 +956,9 @@ let rec assigned_vars_in_lexp (LEXP_aux (le,_)) = match le with | LEXP_id id | LEXP_cast (_,id) -> IdSet.singleton id - | LEXP_tup lexps -> List.fold_left (fun vs le -> IdSet.union vs (assigned_vars_in_lexp le)) IdSet.empty lexps + | LEXP_tup lexps + | LEXP_vector_concat lexps -> + List.fold_left (fun vs le -> IdSet.union vs (assigned_vars_in_lexp le)) IdSet.empty lexps | LEXP_memory (_,es) -> List.fold_left (fun vs e -> IdSet.union vs (assigned_vars e)) IdSet.empty es | LEXP_vector (le,e) -> IdSet.union (assigned_vars_in_lexp le) (assigned_vars e) | LEXP_vector_range (le,e1,e2) -> @@ -1468,6 +1471,7 @@ let split_defs all_errors splits defs = re (LEXP_vector_range (fst (const_prop_lexp ref_vars substs assigns le), fst (const_prop_exp ref_vars substs assigns e1), fst (const_prop_exp ref_vars substs assigns e2))) + | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map (fun le -> fst (const_prop_lexp ref_vars substs assigns le)) les)) | LEXP_field (le,id) -> re (LEXP_field (fst (const_prop_lexp ref_vars substs assigns le), id)) | LEXP_deref e -> re (LEXP_deref (fst (const_prop_exp ref_vars substs assigns e))) @@ -2014,6 +2018,7 @@ let split_defs all_errors splits defs = | LEXP_tup les -> re (LEXP_tup (List.map map_lexp les)) | LEXP_vector (le,e) -> re (LEXP_vector (map_lexp le, map_exp e)) | LEXP_vector_range (le,e1,e2) -> re (LEXP_vector_range (map_lexp le, map_exp e1, map_exp e2)) + | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map map_lexp les)) | LEXP_field (le,id) -> re (LEXP_field (map_lexp le, id)) | LEXP_deref e -> re (LEXP_deref (map_exp e)) in map_pexp, map_letbind @@ -3120,7 +3125,8 @@ and analyse_lexp fn_id env assigns deps (LEXP_aux (lexp,(l,_))) = | LEXP_memory (id,es) -> let _, assigns, r = analyse_exp fn_id env assigns (E_aux (E_tuple es,(Unknown,None))) in assigns, r - | LEXP_tup lexps -> + | LEXP_tup lexps + | LEXP_vector_concat lexps -> List.fold_left (fun (assigns,r) lexp -> let assigns,r' = analyse_lexp fn_id env assigns deps lexp in assigns,merge r r') (assigns,empty) lexps |