From d091e5a201a9394a534b0f902fec0d11e9181eaa Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Tue, 13 Feb 2024 16:07:58 -0800 Subject: [PATCH 1/4] Add Advanced_simd_modified_immediate (MOVI) instruction --- Arm/Decode.lean | 24 +++ Arm/Decode/DPSFP.lean | 26 ++++ Arm/Exec.lean | 2 + .../Advanced_simd_modified_immediate.lean | 142 ++++++++++++++++++ Arm/Insts/DPSFP/Insts.lean | 2 + 5 files changed, 196 insertions(+) create mode 100644 Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean diff --git a/Arm/Decode.lean b/Arm/Decode.lean index a438c360..98963edc 100644 --- a/Arm/Decode.lean +++ b/Arm/Decode.lean @@ -96,6 +96,8 @@ def decode_data_proc_sfp (i : BitVec 32) : Option ArmInst := DPSFP (Advanced_simd_copy {Q, op, imm5, imm4, Rn, Rd}) | [0, Q:1, 101110, op2:2, 0, Rm:5, 0, imm4:4, 0, Rn:5, Rd:5] => DPSFP (Advanced_simd_extract {Q, op2, Rm, imm4, Rn, Rd}) + | [0, Q:1, op:1, 0111100000, a:1, b:1, c:1, cmode:4, o2:1, 1, d:1, e:1, f:1, g:1, h:1, Rd:5] => + DPSFP (Advanced_simd_modified_immediate {Q, op, a, b, c, cmode, o2, d, e, f, g, h, Rd}) | [0, Q:1, U:1, 01110, size:2, 1, Rm:5, opcode:5, 1, Rn:5, Rd:5] => DPSFP (Advanced_simd_three_same {Q, U, size, Rm, opcode, Rn, Rd}) | [0, Q:1, U:1, 01110, size:2, 1, Rm:5, opcode:4, 00, Rn:5, Rd:5] => @@ -397,6 +399,28 @@ example : decode_raw_inst 0xcb0fdf69 = Rd := 0x09#5 })) := by rfl +-- orr v5.8h, #0x77, lsl #8 +example : decode_raw_inst 0x4f03b6e5 = + (ArmInst.DPSFP + (DataProcSFPInst.Advanced_simd_modified_immediate + { _fixed1 := 0x0#1, + Q := 0x1#1, + op := 0x0#1, + _fixed2 := 0x1e0#10, + a := 0x0#1, + b := 0x1#1, + c := 0x1#1, + cmode := 0xb#4, + o2 := 0x0#1, + _fixed3 := 0x1#1, + d := 0x1#1, + e := 0x0#1, + f := 0x1#1, + g := 0x1#1, + h := 0x1#1, + Rd := 0x05#5 })) := by + rfl + -- Unimplemented example : decode_raw_inst 0x00000000#32 = none := by rfl diff --git a/Arm/Decode/DPSFP.lean b/Arm/Decode/DPSFP.lean index 5b12859c..deacf766 100644 --- a/Arm/Decode/DPSFP.lean +++ b/Arm/Decode/DPSFP.lean @@ -105,6 +105,30 @@ instance : ToString Advanced_simd_extract_cls where toString a := toString (repr def Advanced_simd_extract_cls.toBitVec32 (x : Advanced_simd_extract_cls) : BitVec 32 := x._fixed1 ++ x.Q ++ x._fixed2 ++ x.op2 ++ x._fixed3 ++ x.Rm ++ x._fixed4 ++ x.imm4 ++ x._fixed5 ++ x.Rn ++ x.Rd +structure Advanced_simd_modified_immediate_cls where + _fixed1 : BitVec 1 := 0b0#1 -- [31:31] + Q : BitVec 1 -- [30:30] + op : BitVec 1 -- [29:29] + _fixed2 : BitVec 10 := 0b0111100000#10 -- [28:19] + a : BitVec 1 -- [18:18] + b : BitVec 1 -- [17:17] + c : BitVec 1 -- [16:16] + cmode : BitVec 4 -- [15:12] + o2 : BitVec 1 -- [11:11] + _fixed3 : BitVec 1 := 0b1#1 -- [10:10] + d : BitVec 1 -- [9:9] + e : BitVec 1 -- [8:8] + f : BitVec 1 -- [7:7] + g : BitVec 1 -- [6:6] + h : BitVec 1 -- [5:5] + Rd : BitVec 5 -- [4:0] +deriving DecidableEq, Repr + +instance : ToString Advanced_simd_modified_immediate_cls where toString a := toString (repr a) + +def Advanced_simd_modified_immediate_cls.toBitVec32 (x : Advanced_simd_modified_immediate_cls) : BitVec 32 := + x._fixed1 ++ x.Q ++ x.op ++ x._fixed2 ++ x.a ++ x.b ++ x.c ++ x.cmode ++ x.o2 ++ x._fixed3 ++ x.d ++ x.e ++ x.f ++ x.g ++ x.h ++ x.Rd + structure Advanced_simd_three_same_cls where _fixed1 : BitVec 1 := 0b0#1 -- [31:31] Q : BitVec 1 -- [30:30] @@ -156,6 +180,8 @@ inductive DataProcSFPInst where Advanced_simd_copy_cls → DataProcSFPInst | Advanced_simd_extract : Advanced_simd_extract_cls → DataProcSFPInst + | Advanced_simd_modified_immediate : + Advanced_simd_modified_immediate_cls → DataProcSFPInst | Advanced_simd_three_same : Advanced_simd_three_same_cls → DataProcSFPInst | Advanced_simd_three_different : diff --git a/Arm/Exec.lean b/Arm/Exec.lean index bea31af6..4ac94251 100644 --- a/Arm/Exec.lean +++ b/Arm/Exec.lean @@ -44,6 +44,8 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState := DPSFP.exec_advanced_simd_two_reg_misc i s | DPSFP (DataProcSFPInst.Advanced_simd_extract i) => DPSFP.exec_advanced_simd_extract i s + | DPSFP (DataProcSFPInst.Advanced_simd_modified_immediate i) => + DPSFP.exec_advanced_simd_modified_immediate i s | DPSFP (DataProcSFPInst.Advanced_simd_three_same i) => DPSFP.exec_advanced_simd_three_same i s | DPSFP (DataProcSFPInst.Advanced_simd_three_different i) => diff --git a/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean b/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean new file mode 100644 index 00000000..ba60959d --- /dev/null +++ b/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean @@ -0,0 +1,142 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Author(s): Yan Peng +-/ +-- MOVI, MVNI, ORR, BIC (Immediate, vector) + +import Arm.Decode +import Arm.Insts.Common +import Arm.BitVec + +---------------------------------------------------------------------- + +namespace DPSFP + +open Std.BitVec + +inductive ImmediateOp where + | MOVI : ImmediateOp + | MVNI : ImmediateOp + | ORR : ImmediateOp + | BIC : ImmediateOp +deriving DecidableEq, Repr + +instance : ToString ImmediateOp where toString a := toString (repr a) + +def decode_immediate_op (cmode : BitVec 4) (op : BitVec 1) : ImmediateOp := + match_bv cmode ++ op with + | [0, _xx:2, 00] => ImmediateOp.MOVI + | [0, _xx:2, 01] => ImmediateOp.MVNI + | [0, _xx:2, 10] => ImmediateOp.ORR + | [0, _xx:2, 11] => ImmediateOp.BIC + | [10, _x:1, 00] => ImmediateOp.MOVI + | [10, _x:1, 01] => ImmediateOp.MVNI + | [10, _x:1, 10] => ImmediateOp.ORR + | [10, _x:1, 11] => ImmediateOp.BIC + | [110, _x:1, 0] => ImmediateOp.MOVI + | [110, _x:1, 1] => ImmediateOp.MVNI + | [1110, _x:1] => ImmediateOp.MOVI + | [11110] => ImmediateOp.MOVI + -- | [11111] => ImmediateOp.MOVI + | _ => ImmediateOp.MOVI + +def AdvSIMDExpandImm (op : BitVec 1) (cmode : BitVec 4) (imm8 : BitVec 8) : BitVec 64 := + let cmode_high3 := extractLsb 3 1 cmode + let cmode_low1 := extractLsb 0 0 cmode + match cmode_high3 with + | 0b000#3 => replicate 2 $ Std.BitVec.zero 24 ++ imm8 + | 0b001#3 => replicate 2 $ Std.BitVec.zero 16 ++ imm8 ++ Std.BitVec.zero 8 + | 0b010#3 => replicate 2 $ Std.BitVec.zero 8 ++ imm8 ++ Std.BitVec.zero 16 + | 0b011#3 => replicate 2 $ imm8 ++ Std.BitVec.zero 24 + | 0b100#3 => replicate 4 $ Std.BitVec.zero 8 ++ imm8 + | 0b101#3 => replicate 4 $ imm8 ++ Std.BitVec.zero 8 + | 0b110#3 => + if cmode_low1 == 0 then + replicate 2 $ Std.BitVec.zero 16 ++ imm8 ++ allOnes 8 + else + replicate 2 $ Std.BitVec.zero 8 ++ imm8 ++ allOnes 16 + | _ => + if cmode_low1 == 0 && op == 0 then + replicate 8 imm8 + else if cmode_low1 == 0 && op == 1 then + let imm8a := replicate 8 $ extractLsb 7 7 imm8 + let imm8b := replicate 8 $ extractLsb 6 6 imm8 + let imm8c := replicate 8 $ extractLsb 5 5 imm8 + let imm8d := replicate 8 $ extractLsb 4 4 imm8 + let imm8e := replicate 8 $ extractLsb 3 3 imm8 + let imm8f := replicate 8 $ extractLsb 2 2 imm8 + let imm8g := replicate 8 $ extractLsb 1 1 imm8 + let imm8h := replicate 8 $ extractLsb 0 0 imm8 + imm8a ++ imm8b ++ imm8c ++ imm8d ++ imm8e ++ imm8f ++ imm8g ++ imm8h + else if cmode_low1 == 1 && op == 0 then + let imm32 := extractLsb 7 7 imm8 ++ ~~~(extractLsb 6 6 imm8) ++ + (replicate 5 $ extractLsb 6 6 imm8) ++ + extractLsb 5 0 imm8 ++ Std.BitVec.zero 19 + replicate 2 imm32 + else + -- Assume not UsingAArch32() + -- if UsingAArch32() then ReservedEncoding(); + extractLsb 7 7 imm8 ++ ~~~(extractLsb 6 6 imm8) ++ + (replicate 8 $ extractLsb 6 6 imm8) ++ extractLsb 5 0 imm8 ++ Std.BitVec.zero 48 + +@[simp] +-- Assumes CheckFPAdvSIMDEnabled64(); +def exec_advanced_simd_modified_immediate + (inst : Advanced_simd_modified_immediate_cls) (s : ArmState) : ArmState := + if inst.cmode == 0b1111#4 && inst.op == 0b1#1 && inst.Q == 0b0#1 then + -- FMOV Dn,#imm is in main FP instruction set + write_err (StateError.Illegal s!"Illegal {inst} encountered!") s + else + let datasize := 64 <<< inst.Q.toNat + let operation := decode_immediate_op inst.cmode inst.op + let imm8 := inst.a ++ inst.b ++ inst.c ++ inst.d ++ inst.e ++ inst.f ++ inst.g ++ inst.h + let imm64 := AdvSIMDExpandImm inst.op inst.cmode imm8 + let imm := replicate (datasize/64) imm64 + have h : (64 * (datasize / 64)) = datasize := by sorry + let result := match operation with + | ImmediateOp.MOVI => (h ▸ imm) + | ImmediateOp.MVNI => ~~~(h ▸ imm) + | ImmediateOp.ORR => + let operand := read_sfp datasize inst.Rd s + operand ||| (h ▸ imm) + | _ => + let operand := read_sfp datasize inst.Rd s + operand &&& ~~~(h ▸ imm) + -- State Updates + let s' := write_pc ((read_pc s) + 4#64) s + let s' := write_sfp datasize inst.Rd result s + s' + +---------------------------------------------------------------------- + +partial def Advanced_simd_modified_immediate_cls.nonfp.rand : IO (Option (BitVec 32)) := do + let cmode := ← BitVec.rand 4 + let op := ← BitVec.rand 1 + let Q := ← BitVec.rand 1 + if cmode == 0b1111#4 && op == 0b1#1 && Q = 0b0#1 then + Advanced_simd_modified_immediate_cls.nonfp.rand + else + let (inst : Advanced_simd_modified_immediate_cls) := + { Q := Q + , op := op + , a := ← BitVec.rand 1 + , b := ← BitVec.rand 1 + , c := ← BitVec.rand 1 + , cmode := cmode + , o2 := 0b0#1 + , d := ← BitVec.rand 1 + , e := ← BitVec.rand 1 + , f := ← BitVec.rand 1 + , g := ← BitVec.rand 1 + , h := ← BitVec.rand 1 + , Rd := ← BitVec.rand 5 + } + pure (some (inst.toBitVec32)) + +/-- Generate random instructions of Advanced_simd_modified_immediate class. -/ +def Advanced_simd_modified_immediate_cls.rand : List (IO (Option (BitVec 32))) := + [ Advanced_simd_modified_immediate_cls.nonfp.rand ] + +---------------------------------------------------------------------- + +end DPSFP diff --git a/Arm/Insts/DPSFP/Insts.lean b/Arm/Insts/DPSFP/Insts.lean index 0009361a..7cf06547 100644 --- a/Arm/Insts/DPSFP/Insts.lean +++ b/Arm/Insts/DPSFP/Insts.lean @@ -5,6 +5,7 @@ Author(s): Shilpi Goel -/ import Arm.Insts.DPSFP.Advanced_simd_two_reg_misc import Arm.Insts.DPSFP.Advanced_simd_extract +import Arm.Insts.DPSFP.Advanced_simd_modified_immediate import Arm.Insts.DPSFP.Advanced_simd_three_same import Arm.Insts.DPSFP.Advanced_simd_three_different import Arm.Insts.DPSFP.Crypto_aes @@ -15,6 +16,7 @@ import Arm.Insts.DPSFP.Crypto_three_reg_sha512 DPSFP class. -/ def DPSFP.rand : List (IO (Option (BitVec 32))) := DPSFP.Advanced_simd_extract_cls.rand ++ + DPSFP.Advanced_simd_modified_immediate_cls.rand ++ DPSFP.Advanced_simd_three_same_cls.rand ++ DPSFP.Advanced_simd_three_different_cls.rand ++ DPSFP.Advanced_simd_two_reg_misc_cls.rand ++ From 3bf520ed48bc3dc2add4409a8c2dcec0c2b8d220 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 15 Feb 2024 16:12:49 -0800 Subject: [PATCH 2/4] Add advanced simd scalar copy (DUP element scalar class) --- Arm/Decode.lean | 2 + Arm/Decode/DPSFP.lean | 42 ++++++++++--- Arm/Exec.lean | 2 + Arm/Insts/Common.lean | 8 +++ Arm/Insts/DPSFP/Advanced_simd_copy.lean | 29 +++++++++ .../Advanced_simd_modified_immediate.lean | 18 +++--- .../DPSFP/Advanced_simd_scalar_copy.lean | 62 +++++++++++++++++++ Arm/Insts/DPSFP/Insts.lean | 2 + 8 files changed, 147 insertions(+), 18 deletions(-) create mode 100644 Arm/Insts/DPSFP/Advanced_simd_copy.lean create mode 100644 Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean diff --git a/Arm/Decode.lean b/Arm/Decode.lean index 98963edc..8024daa0 100644 --- a/Arm/Decode.lean +++ b/Arm/Decode.lean @@ -98,6 +98,8 @@ def decode_data_proc_sfp (i : BitVec 32) : Option ArmInst := DPSFP (Advanced_simd_extract {Q, op2, Rm, imm4, Rn, Rd}) | [0, Q:1, op:1, 0111100000, a:1, b:1, c:1, cmode:4, o2:1, 1, d:1, e:1, f:1, g:1, h:1, Rd:5] => DPSFP (Advanced_simd_modified_immediate {Q, op, a, b, c, cmode, o2, d, e, f, g, h, Rd}) + | [01, op:1, 11110000, imm5:5, 0, imm4:4, 1, Rn:5, Rd:5] => + DPSFP (Advanced_simd_scalar_copy {op, imm5, imm4, Rn, Rd}) | [0, Q:1, U:1, 01110, size:2, 1, Rm:5, opcode:5, 1, Rn:5, Rd:5] => DPSFP (Advanced_simd_three_same {Q, U, size, Rm, opcode, Rn, Rd}) | [0, Q:1, U:1, 01110, size:2, 1, Rm:5, opcode:4, 00, Rn:5, Rd:5] => diff --git a/Arm/Decode/DPSFP.lean b/Arm/Decode/DPSFP.lean index deacf766..0e16042e 100644 --- a/Arm/Decode/DPSFP.lean +++ b/Arm/Decode/DPSFP.lean @@ -72,20 +72,40 @@ def Advanced_simd_two_reg_misc_cls.toBitVec32 (x : Advanced_simd_two_reg_misc_cl x._fixed1 ++ x.Q ++ x.U ++ x._fixed2 ++ x.size ++ x._fixed3 ++ x.opcode ++ x._fixed4 ++ x.Rn ++ x.Rd structure Advanced_simd_copy_cls where - _fixed1 : BitVec 1 := 0b0#1 -- [31:31] - Q : BitVec 1 -- [30:30] - op : BitVec 1 -- [29:29] - _fixed2 : BitVec 7 := 01110000#7 -- [28:21] - imm5 : BitVec 5 -- [20:16] - _fixed3 : BitVec 1 := 0b0#1 -- [15:15] - imm4 : BitVec 4 -- [14:11] - _fixed4 : BitVec 1 := 0b1#1 -- [10:10] - Rn : BitVec 5 -- [9:5] - Rd : BitVec 5 -- [4:0] + _fixed1 : BitVec 1 := 0b0#1 -- [31:31] + Q : BitVec 1 -- [30:30] + op : BitVec 1 -- [29:29] + _fixed2 : BitVec 8 := 0b01110000#8 -- [28:21] + imm5 : BitVec 5 -- [20:16] + _fixed3 : BitVec 1 := 0b0#1 -- [15:15] + imm4 : BitVec 4 -- [14:11] + _fixed4 : BitVec 1 := 0b1#1 -- [10:10] + Rn : BitVec 5 -- [9:5] + Rd : BitVec 5 -- [4:0] deriving DecidableEq, Repr instance : ToString Advanced_simd_copy_cls where toString a := toString (repr a) +def Advanced_simd_copy_cls.toBitVec32 (x : Advanced_simd_copy_cls) : BitVec 32 := + x._fixed1 ++ x.Q ++ x.op ++ x._fixed2 ++ x.imm5 ++ x._fixed3 ++ x.imm4 ++ x._fixed4 ++ x.Rn ++ x.Rd + +structure Advanced_simd_scalar_copy_cls where + _fixed1 : BitVec 2 := 0b01#2 -- [31:30] + op : BitVec 1 -- [29:29] + _fixed2 : BitVec 8 := 0b11110000#8 -- [28:21] + imm5 : BitVec 5 -- [20:16] + _fixed3 : BitVec 1 := 0b0#1 -- [15:15] + imm4 : BitVec 4 -- [14:11] + _fixed4 : BitVec 1 := 0b1#1 -- [10:10] + Rn : BitVec 5 -- [9:5] + Rd : BitVec 5 -- [4:0] +deriving DecidableEq, Repr + +instance : ToString Advanced_simd_scalar_copy_cls where toString a := toString (repr a) + +def Advanced_simd_scalar_copy_cls.toBitVec32 (x : Advanced_simd_scalar_copy_cls) : BitVec 32 := + x._fixed1 ++ x.op ++ x._fixed2 ++ x.imm5 ++ x._fixed3 ++ x.imm4 ++ x._fixed4 ++ x.Rn ++ x.Rd + structure Advanced_simd_extract_cls where _fixed1 : BitVec 1 := 0b0#1 -- [31:31] Q : BitVec 1 -- [30:30] @@ -182,6 +202,8 @@ inductive DataProcSFPInst where Advanced_simd_extract_cls → DataProcSFPInst | Advanced_simd_modified_immediate : Advanced_simd_modified_immediate_cls → DataProcSFPInst + | Advanced_simd_scalar_copy : + Advanced_simd_scalar_copy_cls → DataProcSFPInst | Advanced_simd_three_same : Advanced_simd_three_same_cls → DataProcSFPInst | Advanced_simd_three_different : diff --git a/Arm/Exec.lean b/Arm/Exec.lean index 4ac94251..24e102af 100644 --- a/Arm/Exec.lean +++ b/Arm/Exec.lean @@ -46,6 +46,8 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState := DPSFP.exec_advanced_simd_extract i s | DPSFP (DataProcSFPInst.Advanced_simd_modified_immediate i) => DPSFP.exec_advanced_simd_modified_immediate i s + | DPSFP (DataProcSFPInst.Advanced_simd_scalar_copy i) => + DPSFP.exec_advanced_simd_scalar_copy i s | DPSFP (DataProcSFPInst.Advanced_simd_three_same i) => DPSFP.exec_advanced_simd_three_same i s | DPSFP (DataProcSFPInst.Advanced_simd_three_different i) => diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean index 0f420393..43068ec3 100644 --- a/Arm/Insts/Common.lean +++ b/Arm/Insts/Common.lean @@ -112,6 +112,14 @@ def highest_set_bit (bv : BitVec n) : Option Nat := Id.run do break return acc +def lowest_set_bit (bv : BitVec n) : Nat := Id.run do + let mut acc := n + for i in List.range n do + if extractLsb i i bv == 1 + then acc := i + break + return acc + def invalid_bit_masks (immN : BitVec 1) (imms : BitVec 6) (immediate : Bool) (M : Nat) : Bool := let len := highest_set_bit $ immN ++ ~~~imms diff --git a/Arm/Insts/DPSFP/Advanced_simd_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_copy.lean new file mode 100644 index 00000000..2cf1fd34 --- /dev/null +++ b/Arm/Insts/DPSFP/Advanced_simd_copy.lean @@ -0,0 +1,29 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Author(s): Yan Peng +-/ +-- DUP, INS, SMOV, UMOV + +import Arm.Decode +import Arm.Insts.Common +import Arm.BitVec + +---------------------------------------------------------------------- + +namespace DPSFP + +open Std.BitVec + +@[simp] +def exec_advanced_simd_copy + (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState := + sorry + + +---------------------------------------------------------------------- + +/-- Generate random instructions of Advanced_simd_copy class. -/ +def Advanced_simd_copy_cls.rand : List (IO (Option (BitVec 32))) := + [] + +end DPSFP diff --git a/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean b/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean index ba60959d..209a85e6 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean @@ -2,7 +2,8 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Author(s): Yan Peng -/ --- MOVI, MVNI, ORR, BIC (Immediate, vector) +-- MOVI, MVNI, ORR, BIC (Immediate, vector), and FMOV (vector, immediate) - Single/double-precision +-- Missing: FMOV (vector, immediate) - Half-precision import Arm.Decode import Arm.Insts.Common @@ -37,7 +38,7 @@ def decode_immediate_op (cmode : BitVec 4) (op : BitVec 1) : ImmediateOp := | [110, _x:1, 1] => ImmediateOp.MVNI | [1110, _x:1] => ImmediateOp.MOVI | [11110] => ImmediateOp.MOVI - -- | [11111] => ImmediateOp.MOVI + -- | case [11111] | _ => ImmediateOp.MOVI def AdvSIMDExpandImm (op : BitVec 1) (cmode : BitVec 4) (imm8 : BitVec 8) : BitVec 64 := @@ -83,8 +84,9 @@ def AdvSIMDExpandImm (op : BitVec 1) (cmode : BitVec 4) (imm8 : BitVec 8) : BitV -- Assumes CheckFPAdvSIMDEnabled64(); def exec_advanced_simd_modified_immediate (inst : Advanced_simd_modified_immediate_cls) (s : ArmState) : ArmState := - if inst.cmode == 0b1111#4 && inst.op == 0b1#1 && inst.Q == 0b0#1 then - -- FMOV Dn,#imm is in main FP instruction set + if inst.cmode == 0b1111#4 && inst.op == 0b0#1 && inst.o2 == 0b1#1 then + write_err (StateError.Unimplemented s!"Unsupported {inst} encountered!") s + else if inst.cmode == 0b1111#4 && inst.op == 0b1#1 && inst.Q == 0b0#1 || inst.o2 == 0b1#1 then write_err (StateError.Illegal s!"Illegal {inst} encountered!") s else let datasize := 64 <<< inst.Q.toNat @@ -103,9 +105,9 @@ def exec_advanced_simd_modified_immediate let operand := read_sfp datasize inst.Rd s operand &&& ~~~(h ▸ imm) -- State Updates - let s' := write_pc ((read_pc s) + 4#64) s - let s' := write_sfp datasize inst.Rd result s - s' + let s := write_pc ((read_pc s) + 4#64) s + let s := write_sfp datasize inst.Rd result s + s ---------------------------------------------------------------------- @@ -131,7 +133,7 @@ partial def Advanced_simd_modified_immediate_cls.nonfp.rand : IO (Option (BitVec , h := ← BitVec.rand 1 , Rd := ← BitVec.rand 5 } - pure (some (inst.toBitVec32)) + pure (some inst.toBitVec32) /-- Generate random instructions of Advanced_simd_modified_immediate class. -/ def Advanced_simd_modified_immediate_cls.rand : List (IO (Option (BitVec 32))) := diff --git a/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean new file mode 100644 index 00000000..39211702 --- /dev/null +++ b/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean @@ -0,0 +1,62 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Author(s): Yan Peng +-/ +-- DUP (element) scalar + +import Arm.Decode +import Arm.Insts.Common +import Arm.BitVec + +---------------------------------------------------------------------- + +namespace DPSFP + +open Std.BitVec + +theorem advanced_simd_scalar_copy_helper_lemma (x y : Nat): + y + 8 <<< x - 1 - y + 1 = 8 <<< x := by sorry + +@[simp] +def exec_advanced_simd_scalar_copy + (inst : Advanced_simd_scalar_copy_cls) (s : ArmState) : ArmState := + let size := lowest_set_bit inst.imm5 + if h₀ : size > 3 || inst.imm4 != 0b0000#4 || inst.op != 0 then + write_err (StateError.Illegal s!"Illegal {inst} encountered!") s + else + let index := extractLsb 4 (size + 1) inst.imm5 + let idxdsize := 64 <<< (extractLsb 4 4 inst.imm5).toNat + let esize := 8 <<< size + let datasize := esize + let operand := read_sfp idxdsize inst.Rn s + let lo := index.toNat * esize + let hi := lo + esize - 1 + let result := extractLsb hi lo operand + have h : hi - lo + 1 = datasize := by + simp; apply advanced_simd_scalar_copy_helper_lemma + -- State Updates + let s := write_pc ((read_pc s) + 4#64) s + let s := write_sfp datasize inst.Rd (h ▸ result) s + s + +---------------------------------------------------------------------- + +partial def Advanced_simd_scalar_copy_cls.dup.rand : IO (Option (BitVec 32)) := do + let imm5 := ← BitVec.rand 5 + if (Option.get! $ lowest_set_bit imm5) > 3 then + Advanced_simd_scalar_copy_cls.dup.rand + else + let (inst : Advanced_simd_scalar_copy_cls) := + { op := 0b0#1 + , imm5 := imm5 + , imm4 := 0b0000#4 + , Rn := ← BitVec.rand 5 + , Rd := ← BitVec.rand 5 + } + pure (some inst.toBitVec32) + +/-- Generate random instructions of Advanced_simd_scalar_copy class. -/ +def Advanced_simd_scalar_copy_cls.rand : List (IO (Option (BitVec 32))) := + [ Advanced_simd_scalar_copy_cls.dup.rand ] + +end DPSFP diff --git a/Arm/Insts/DPSFP/Insts.lean b/Arm/Insts/DPSFP/Insts.lean index 7cf06547..5d023b22 100644 --- a/Arm/Insts/DPSFP/Insts.lean +++ b/Arm/Insts/DPSFP/Insts.lean @@ -6,6 +6,7 @@ Author(s): Shilpi Goel import Arm.Insts.DPSFP.Advanced_simd_two_reg_misc import Arm.Insts.DPSFP.Advanced_simd_extract import Arm.Insts.DPSFP.Advanced_simd_modified_immediate +import Arm.Insts.DPSFP.Advanced_simd_scalar_copy import Arm.Insts.DPSFP.Advanced_simd_three_same import Arm.Insts.DPSFP.Advanced_simd_three_different import Arm.Insts.DPSFP.Crypto_aes @@ -17,6 +18,7 @@ DPSFP class. -/ def DPSFP.rand : List (IO (Option (BitVec 32))) := DPSFP.Advanced_simd_extract_cls.rand ++ DPSFP.Advanced_simd_modified_immediate_cls.rand ++ + DPSFP.Advanced_simd_scalar_copy_cls.rand ++ DPSFP.Advanced_simd_three_same_cls.rand ++ DPSFP.Advanced_simd_three_different_cls.rand ++ DPSFP.Advanced_simd_two_reg_misc_cls.rand ++ From a3ada79df96e381ea058f8a6490c400d21d8b5b5 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 15 Feb 2024 17:41:53 -0800 Subject: [PATCH 3/4] Add advanced simd copy --- Arm/Decode.lean | 16 ++ Arm/Exec.lean | 2 + Arm/Insts/Common.lean | 11 + Arm/Insts/DPSFP/Advanced_simd_copy.lean | 242 +++++++++++++++++- .../Advanced_simd_modified_immediate.lean | 1 + .../DPSFP/Advanced_simd_scalar_copy.lean | 11 +- .../DPSFP/Advanced_simd_three_different.lean | 13 +- Arm/Insts/DPSFP/Advanced_simd_three_same.lean | 11 +- Arm/Insts/DPSFP/Insts.lean | 2 + 9 files changed, 280 insertions(+), 29 deletions(-) diff --git a/Arm/Decode.lean b/Arm/Decode.lean index 8024daa0..3af126c5 100644 --- a/Arm/Decode.lean +++ b/Arm/Decode.lean @@ -423,6 +423,22 @@ example : decode_raw_inst 0x4f03b6e5 = Rd := 0x05#5 })) := by rfl +-- mov v10.h[0] v17.h[6] +example : decode_raw_inst 0x6e026e2a = + (ArmInst.DPSFP + (DataProcSFPInst.Advanced_simd_copy + { _fixed1 := 0x0#1, + Q := 0x1#1, + op := 0x1#1, + _fixed2 := 0x70#8, + imm5 := 0x02#5, + _fixed3 := 0x0#1, + imm4 := 0xd#4, + _fixed4 := 0x1#1, + Rn := 0x11#5, + Rd := 0x0a#5 })) := by + rfl + -- Unimplemented example : decode_raw_inst 0x00000000#32 = none := by rfl diff --git a/Arm/Exec.lean b/Arm/Exec.lean index 24e102af..10fabf66 100644 --- a/Arm/Exec.lean +++ b/Arm/Exec.lean @@ -36,6 +36,8 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState := | DPR (DataProcRegInst.Logical_shifted_reg i) => DPR.exec_logical_shifted_reg i s + | DPSFP (DataProcSFPInst.Advanced_simd_copy i) => + DPSFP.exec_advanced_simd_copy i s | DPSFP (DataProcSFPInst.Crypto_two_reg_sha512 i) => DPSFP.exec_crypto_two_reg_sha512 i s | DPSFP (DataProcSFPInst.Crypto_three_reg_sha512 i) => diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean index 43068ec3..9d351fe1 100644 --- a/Arm/Insts/Common.lean +++ b/Arm/Insts/Common.lean @@ -222,4 +222,15 @@ def ldst_write (SIMD? : Bool) (width : Nat) (idx : BitVec 5) (val : BitVec width : ArmState := if SIMD? then write_sfp width idx val s else write_gpr width idx val s +---------------------------------------------------------------------- + +theorem hi_lo_diff_equal_esize (esize : Nat) (lo : Nat) (hi : Nat) + (h₀ : esize > 0) (h₁ : hi = lo + esize - 1): + hi - lo + 1 = esize := by omega + +theorem esize_gt_zero (size : Nat): + 8 <<< size > 0 := by + simp_all only [ Nat.shiftLeft_eq, gt_iff_lt, Nat.zero_lt_succ + , mul_pos_iff_of_pos_left, zero_lt_two, pow_pos] + end Common diff --git a/Arm/Insts/DPSFP/Advanced_simd_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_copy.lean index 2cf1fd34..2141f288 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_copy.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_copy.lean @@ -1,5 +1,6 @@ /- Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. Author(s): Yan Peng -/ -- DUP, INS, SMOV, UMOV @@ -14,16 +15,251 @@ namespace DPSFP open Std.BitVec +def dup_aux (e : Nat) (elements : Nat) (esize : Nat) + (element : BitVec esize) (result : BitVec datasize) (H : esize > 0) : BitVec datasize := + if h₀ : e ≥ elements then + result + else + let lo := e * esize + let hi := lo + esize -1 + have h₁ : hi - lo + 1 = esize := by simp; omega + let result := BitVec.partInstall hi lo (h₁ ▸ element) result + have h : elements - (e + 1) < elements - e := by omega + dup_aux (e + 1) elements esize element result H + termination_by dup_aux e elements esize element result H => (elements - e) + +def exec_dup_element (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState := + let size := lowest_set_bit inst.imm5 + if size > 3 || (size == 3 && inst.Q == 0) then + write_err (StateError.Illegal s!"Illegal {inst} encountered!") s + else + let index := (extractLsb 4 (size + 1) inst.imm5).toNat + let idxdsize := 64 <<< (extractLsb 4 4 inst.imm5).toNat + let esize := 8 <<< size + let datasize := 64 <<< inst.Q.toNat + let elements := datasize / esize + let operand := read_sfp idxdsize inst.Rn s + let lo := index * esize + let hi := lo + esize - 1 + let element := extractLsb hi lo operand + have h₀ : esize > 0 := by apply esize_gt_zero + have h₁ : hi - lo + 1 = esize := by simp; omega + let result := dup_aux 0 elements esize (h₁ ▸ element) (Std.BitVec.zero datasize) h₀ + -- State Updates + let s := write_pc ((read_pc s) + 4#64) s + let s := write_sfp datasize inst.Rd result s + s + +def exec_dup_general (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState := + let size := lowest_set_bit inst.imm5 + if size > 3 || (size == 3 && inst.Q == 0) then + write_err (StateError.Illegal s!"Illegal {inst} encountered!") s + else + let esize := 8 <<< size + let datasize := 64 <<< inst.Q.toNat + let elements := datasize / esize + let element := read_gpr esize inst.Rn s + have h₀ : esize > 0 := by apply esize_gt_zero + let result := dup_aux 0 elements esize element (Std.BitVec.zero datasize) h₀ + -- State Updates + let s := write_pc ((read_pc s) + 4#64) s + let s := write_sfp datasize inst.Rd result s + s + +def exec_ins_element (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState := + let size := lowest_set_bit inst.imm5 + if size > 3 then + write_err (StateError.Illegal s!"Illegal {inst} encountered!") s + else + let dst_index := (extractLsb 4 (size + 1) inst.imm5).toNat + let src_index := (extractLsb 3 size inst.imm4).toNat + let idxdsize := 64 <<< (extractLsb 3 3 inst.imm4).toNat + let esize := 8 <<< size + let operand := read_sfp idxdsize inst.Rn s + let result := read_sfp 128 inst.Rd s + let lo_src := src_index * esize + let hi_src := lo_src + esize - 1 + let elem := extractLsb hi_src lo_src operand + let lo_dst := dst_index * esize + let hi_dst := lo_dst + esize - 1 + have h₀ : esize > 0 := by apply esize_gt_zero + have h : hi_dst - lo_dst + 1 = hi_src - lo_src + 1 := by + -- rewrite the LHS and RHS to esize + rw [hi_lo_diff_equal_esize _ _ _ h₀ (by simp)] + rw [hi_lo_diff_equal_esize _ _ _ h₀ (by simp)] + let result := BitVec.partInstall hi_dst lo_dst (h ▸ elem) result + -- State Updates + let s := write_pc ((read_pc s) + 4#64) s + let s := write_sfp 128 inst.Rd result s + s + +def exec_ins_general (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState := + let size := lowest_set_bit inst.imm5 + if size > 3 then + write_err (StateError.Illegal s!"Illegal {inst} encountered!") s + else + let index := (extractLsb 4 (size + 1) inst.imm5).toNat + let esize := 8 <<< size + let element := read_gpr esize inst.Rn s + let result := read_sfp 128 inst.Rd s + let lo := index * esize + let hi := lo + esize -1 + have h₀ : esize > 0 := by apply esize_gt_zero + have h : hi - lo + 1 = esize := by simp; omega + let result := BitVec.partInstall hi lo (h ▸ element) result + -- State Updates + let s := write_pc ((read_pc s) + 4#64) s + let s := write_sfp 128 inst.Rd result s + s + +def exec_smov_umov (inst : Advanced_simd_copy_cls) (s : ArmState) (signed : Bool): ArmState := + let size := lowest_set_bit inst.imm5 + let esize := 8 <<< size + let datasize := 32 <<< inst.Q.toNat + if signed && (size > 2 || datasize <= esize) then + write_err (StateError.Illegal s!"Illegal {inst} encountered!") s + else if (not signed) + && (size > 3 || datasize == 64 && esize < 64 || datasize == 32 && esize >= 64) then + write_err (StateError.Illegal s!"Illegal {inst} encountered!") s + else + let index := (extractLsb 4 (size + 1) inst.imm5).toNat + let idxdsize := 64 <<< (extractLsb 4 4 inst.imm5).toNat + -- if index == 0 then CheckFPEnabled64 else CheckFPAdvSIMDEnabled64 + let operand := read_sfp idxdsize inst.Rn s + let lo := index * esize + let hi := lo + esize - 1 + let element := extractLsb hi lo operand + let result := if signed then signExtend datasize element else zeroExtend datasize element + -- State Updates + let s := write_pc ((read_pc s) + 4#64) s + let s := write_gpr datasize inst.Rd result s + s + @[simp] def exec_advanced_simd_copy (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState := - sorry - + match_bv inst.Q ++ inst.op ++ inst.imm5 ++ inst.imm4 with + | [_Q:1, 0, _imm5:5, 0000] => exec_dup_element inst s + | [_Q:1, 0, _imm5:5, 0001] => exec_dup_general inst s + | [_Q:1, 0, _imm5:5, 0101] => exec_smov_umov inst s true + | [_Q:1, 0, _imm5:5, 0111] => exec_smov_umov inst s false + | [1, 0, _imm5:5, 0011] => exec_ins_general inst s + | [1, 1, _imm5:5, _imm4:4] => exec_ins_element inst s + | _ => write_err (StateError.Illegal s!"Illegal {inst} encountered!") s ---------------------------------------------------------------------- +partial def Advanced_simd_copy_cls.dup_element.rand : IO (Option (BitVec 32)) := do + let Q := ← BitVec.rand 1 + let imm5 := ← BitVec.rand 5 + let size := lowest_set_bit imm5 + if size > 3 || (size == 3 && Q == 0) then + Advanced_simd_copy_cls.dup_element.rand + else + let (inst : Advanced_simd_copy_cls) := + { Q := Q + , op := 0b0#1 + , imm5 := imm5 + , imm4 := 0b0000#4 + , Rn := ← BitVec.rand 5 + , Rd := ← BitVec.rand 5 + } + pure (inst.toBitVec32) + +partial def Advanced_simd_copy_cls.dup_general.rand : IO (Option (BitVec 32)) := do + let Q := ← BitVec.rand 1 + let imm5 := ← BitVec.rand 5 + let size := lowest_set_bit imm5 + if size > 3 || (size == 3 && Q == 0) then + Advanced_simd_copy_cls.dup_general.rand + else + let (inst : Advanced_simd_copy_cls) := + { Q := Q + , op := 0b0#1 + , imm5 := imm5 + , imm4 := 0b0001#4 + , Rn := ← BitVec.rand 5 + , Rd := ← BitVec.rand 5 + } + pure (inst.toBitVec32) + +partial def Advanced_simd_copy_cls.ins_element.rand : IO (Option (BitVec 32)) := do + let imm5 := ← BitVec.rand 5 + let size := lowest_set_bit imm5 + if size > 3 then + Advanced_simd_copy_cls.ins_element.rand + else + let (inst : Advanced_simd_copy_cls) := + { Q := 0b1#1 + , op := 0b1#1 + , imm5 := imm5 + , imm4 := ← BitVec.rand 4 + , Rn := ← BitVec.rand 5 + , Rd := ← BitVec.rand 5 + } + pure (inst.toBitVec32) + +partial def Advanced_simd_copy_cls.ins_general.rand : IO (Option (BitVec 32)) := do + let imm5 := ← BitVec.rand 5 + let size := lowest_set_bit imm5 + if size > 3 then + Advanced_simd_copy_cls.ins_general.rand + else + let (inst : Advanced_simd_copy_cls) := + { Q := 0b1#1 + , op := 0b0#1 + , imm5 := imm5 + , imm4 := 0b0011#4 + , Rn := ← BitVec.rand 5 + , Rd := ← BitVec.rand 5 + } + pure (inst.toBitVec32) + +partial def Advanced_simd_copy_cls.smov.rand : IO (Option (BitVec 32)) := do + let Q := ← BitVec.rand 1 + let imm5 := ← BitVec.rand 5 + let size := lowest_set_bit imm5 + let esize := 8 <<< size + let datasize := 32 <<< Q.toNat + if size > 2 || datasize <= esize then + Advanced_simd_copy_cls.smov.rand + else + let (inst : Advanced_simd_copy_cls) := + { Q := Q + , op := 0b0#1 + , imm5 := imm5 + , imm4 := 0b0101#4 + , Rn := ← BitVec.rand 5 + , Rd := ← BitVec.rand 5 + } + pure (inst.toBitVec32) + +partial def Advanced_simd_copy_cls.umov.rand : IO (Option (BitVec 32)) := do + let Q := ← BitVec.rand 1 + let imm5 := ← BitVec.rand 5 + let size := lowest_set_bit imm5 + let esize := 8 <<< size + let datasize := 32 <<< Q.toNat + if size > 3 || datasize == 64 && esize < 64 || datasize == 32 && esize >= 64 then + Advanced_simd_copy_cls.umov.rand + else + let (inst : Advanced_simd_copy_cls) := + { Q := Q + , op := 0b0#1 + , imm5 := imm5 + , imm4 := 0b0111#4 + , Rn := ← BitVec.rand 5 + , Rd := ← BitVec.rand 5 + } + pure (inst.toBitVec32) + /-- Generate random instructions of Advanced_simd_copy class. -/ def Advanced_simd_copy_cls.rand : List (IO (Option (BitVec 32))) := - [] +[ Advanced_simd_copy_cls.dup_element.rand + , Advanced_simd_copy_cls.dup_general.rand + , Advanced_simd_copy_cls.ins_element.rand + , Advanced_simd_copy_cls.ins_general.rand + , Advanced_simd_copy_cls.smov.rand + , Advanced_simd_copy_cls.umov.rand ] end DPSFP diff --git a/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean b/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean index 209a85e6..e7083e3c 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean @@ -1,5 +1,6 @@ /- Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. Author(s): Yan Peng -/ -- MOVI, MVNI, ORR, BIC (Immediate, vector), and FMOV (vector, immediate) - Single/double-precision diff --git a/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean index 39211702..4405f2a8 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean @@ -1,5 +1,6 @@ /- Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. Author(s): Yan Peng -/ -- DUP (element) scalar @@ -14,9 +15,6 @@ namespace DPSFP open Std.BitVec -theorem advanced_simd_scalar_copy_helper_lemma (x y : Nat): - y + 8 <<< x - 1 - y + 1 = 8 <<< x := by sorry - @[simp] def exec_advanced_simd_scalar_copy (inst : Advanced_simd_scalar_copy_cls) (s : ArmState) : ArmState := @@ -27,16 +25,15 @@ def exec_advanced_simd_scalar_copy let index := extractLsb 4 (size + 1) inst.imm5 let idxdsize := 64 <<< (extractLsb 4 4 inst.imm5).toNat let esize := 8 <<< size - let datasize := esize let operand := read_sfp idxdsize inst.Rn s let lo := index.toNat * esize let hi := lo + esize - 1 let result := extractLsb hi lo operand - have h : hi - lo + 1 = datasize := by - simp; apply advanced_simd_scalar_copy_helper_lemma + have h₁ : esize > 0 := by apply esize_gt_zero + have h : hi - lo + 1 = esize := by simp; omega -- State Updates let s := write_pc ((read_pc s) + 4#64) s - let s := write_sfp datasize inst.Rd (h ▸ result) s + let s := write_sfp esize inst.Rd (h ▸ result) s s ---------------------------------------------------------------------- diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_different.lean b/Arm/Insts/DPSFP/Advanced_simd_three_different.lean index d3a1ff41..ae47150a 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_three_different.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_three_different.lean @@ -1,5 +1,6 @@ /- Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. Author(s): Yan Peng -/ -- PMULL and PMULL2 @@ -30,10 +31,6 @@ def polynomial_mult (op1 : BitVec m) (op2 : BitVec n) : BitVec (m+n) := let extended_op2 := zeroExtend (m+n) op2 polynomial_mult_aux 0 result op1 extended_op2 -theorem pmull_op_helper_lemma (x y : Nat) (h : 0 < y): - x + y - 1 - x + 1 + (x + y - 1 - x + 1) = 2 * x + 2 * y - 1 - 2 * x + 1 := by - omega - def pmull_op (e : Nat) (esize : Nat) (elements : Nat) (x : BitVec n) (y : BitVec n) (result : BitVec (n*2)) (H : esize > 0) : BitVec (n*2) := if h₀ : e ≥ elements then @@ -46,8 +43,7 @@ def pmull_op (e : Nat) (esize : Nat) (elements : Nat) (x : BitVec n) let elem_result := polynomial_mult element1 element2 let lo2 := 2 * (e * esize) let hi2 := lo2 + 2 * esize - 1 - have h₁ : hi - lo + 1 + (hi - lo + 1) = hi2 - lo2 + 1 := by - simp; apply pmull_op_helper_lemma; simp [*] at * + have h₁ : hi - lo + 1 + (hi - lo + 1) = hi2 - lo2 + 1 := by simp; omega let result := BitVec.partInstall hi2 lo2 (h₁ ▸ elem_result) result have h₂ : elements - (e + 1) < elements - e := by omega pmull_op (e + 1) esize elements x y result H @@ -60,10 +56,7 @@ def exec_pmull (inst : Advanced_simd_three_different_cls) (s : ArmState) : ArmSt write_err (StateError.Illegal s!"Illegal {inst} encountered!") s else let esize := 8 <<< inst.size.toNat - have h₀ : esize > 0 := by - simp_all only [Nat.shiftLeft_eq, gt_iff_lt, - Nat.zero_lt_succ, mul_pos_iff_of_pos_left, - zero_lt_two, pow_pos] + have h₀ : esize > 0 := by apply esize_gt_zero let datasize := 64 let part := inst.Q.toNat let elements := datasize / esize diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_same.lean b/Arm/Insts/DPSFP/Advanced_simd_three_same.lean index ba9d67f4..2367b7e0 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_three_same.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_three_same.lean @@ -16,9 +16,6 @@ namespace DPSFP open Std.BitVec -theorem binary_vector_op_aux_helper_lemma (x y : Nat) (h : 0 < y) : - x + y - 1 - x + 1 = y := by omega - def binary_vector_op_aux (e : Nat) (elems : Nat) (esize : Nat) (op : BitVec esize → BitVec esize → BitVec esize) (x : BitVec n) (y : BitVec n) (result : BitVec n) @@ -31,8 +28,7 @@ def binary_vector_op_aux (e : Nat) (elems : Nat) (esize : Nat) let hi := lo + esize - 1 let element1 := extractLsb hi lo x let element2 := extractLsb hi lo y - have h : hi - lo + 1 = esize := by - simp; apply binary_vector_op_aux_helper_lemma; simp [*] at * + have h : hi - lo + 1 = esize := by simp; omega let elem_result := op (h ▸ element1) (h ▸ element2) let result := BitVec.partInstall hi lo (h.symm ▸ elem_result) result have ht1 : elems - (e + 1) < elems - e := by omega @@ -54,10 +50,7 @@ def exec_binary_vector (inst : Advanced_simd_three_same_cls) (s : ArmState) : Ar else let datasize := if inst.Q = 1#1 then 128 else 64 let esize := 8 <<< (Std.BitVec.toNat inst.size) - have h_esize : esize > 0 := by - simp_all only [Nat.shiftLeft_eq, gt_iff_lt, - Nat.zero_lt_succ, mul_pos_iff_of_pos_left, - zero_lt_two, pow_pos] + have h_esize : esize > 0 := by apply esize_gt_zero let sub_op := inst.U == 1 let operand1 := read_sfp datasize inst.Rn s let operand2 := read_sfp datasize inst.Rm s diff --git a/Arm/Insts/DPSFP/Insts.lean b/Arm/Insts/DPSFP/Insts.lean index 5d023b22..dce42a52 100644 --- a/Arm/Insts/DPSFP/Insts.lean +++ b/Arm/Insts/DPSFP/Insts.lean @@ -3,6 +3,7 @@ Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Author(s): Shilpi Goel -/ +import Arm.Insts.DPSFP.Advanced_simd_copy import Arm.Insts.DPSFP.Advanced_simd_two_reg_misc import Arm.Insts.DPSFP.Advanced_simd_extract import Arm.Insts.DPSFP.Advanced_simd_modified_immediate @@ -16,6 +17,7 @@ import Arm.Insts.DPSFP.Crypto_three_reg_sha512 /-- List of functions to generate random instructions of the DPSFP class. -/ def DPSFP.rand : List (IO (Option (BitVec 32))) := + DPSFP.Advanced_simd_copy_cls.rand ++ DPSFP.Advanced_simd_extract_cls.rand ++ DPSFP.Advanced_simd_modified_immediate_cls.rand ++ DPSFP.Advanced_simd_scalar_copy_cls.rand ++ From 1225eaccabd839ffc0c5bea3a1bdde1b8526f814 Mon Sep 17 00:00:00 2001 From: Shilpi Goel Date: Thu, 22 Feb 2024 12:10:37 +0530 Subject: [PATCH 4/4] Prove away a 'sorry' --- .../DPSFP/Advanced_simd_modified_immediate.lean | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean b/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean index e7083e3c..2127a597 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean @@ -81,6 +81,12 @@ def AdvSIMDExpandImm (op : BitVec 1) (cmode : BitVec 4) (imm8 : BitVec 8) : BitV extractLsb 7 7 imm8 ++ ~~~(extractLsb 6 6 imm8) ++ (replicate 8 $ extractLsb 6 6 imm8) ++ extractLsb 5 0 imm8 ++ Std.BitVec.zero 48 + +private theorem mul_div_norm_form_lemma (n m : Nat) (_h1 : 0 < m) (h2 : n ∣ m) : + (n * (m / n)) = n * m / n := by + rw [Nat.mul_div_assoc] + simp only [h2] + @[simp] -- Assumes CheckFPAdvSIMDEnabled64(); def exec_advanced_simd_modified_immediate @@ -95,7 +101,16 @@ def exec_advanced_simd_modified_immediate let imm8 := inst.a ++ inst.b ++ inst.c ++ inst.d ++ inst.e ++ inst.f ++ inst.g ++ inst.h let imm64 := AdvSIMDExpandImm inst.op inst.cmode imm8 let imm := replicate (datasize/64) imm64 - have h : (64 * (datasize / 64)) = datasize := by sorry + have h₀ : 0 < datasize := by + simp_all! only [Nat.shiftLeft_eq, Nat.dvd_mul_right] + generalize Std.BitVec.toNat inst.Q = x + have hb : 2 ^ x > 0 := by exact Nat.pow_two_pos x + exact Nat.mul_pos (by decide) hb + have h₁ : 64 ∣ datasize := by + simp_all! only [Nat.shiftLeft_eq, Nat.dvd_mul_right] + have h : (64 * (datasize / 64)) = datasize := by + rw [mul_div_norm_form_lemma 64 datasize h₀ h₁] + refine Nat.mul_div_cancel_left datasize ?H; decide let result := match operation with | ImmediateOp.MOVI => (h ▸ imm) | ImmediateOp.MVNI => ~~~(h ▸ imm)