Merge branch 'main' into macos-lean-action

Arm/Cosim.lean

@@ -7,6 +7,48 @@ import Arm.Exec
 
 namespace Cosim
 
+/-
+NOTE: Considerations for running cosimulations on Arm-based Apple platforms:
+
+On Arm-based Apple platforms, we completely avoid using the register
+`x18`. It is not allowed to be a source or a destination operand --
+see `GPRIndex.rand`. Even with these restrictions, we cannot expect
+the value of `x18` to be preserved, even though it is callee-saved --
+see Arm/Insts/Cosim/template.S. Here's a quote from "Procedure Call
+Standard for the Arm 64-bit Architecture" (the latest version is
+available at https://github.com/ARM-software/abi-aa/releases) that
+informs this choice:
+
+"The role of register r18 is platform specific. If a platform ABI has
+need of a dedicated general-purpose register to carry inter-procedural
+state (for example, the thread context) then it should use this
+register for that purpose. If the platform ABI has no such
+requirements, then it should use r18 as an additional temporary
+register. The platform ABI specification must document the usage for
+this register...
+
+Software developers creating platform-independent code are advised to
+avoid using r18 if at all possible. Most compilers provide a mechanism
+to prevent specific registers from being used for general allocation;
+portable hand-coded assembler should avoid it entirely...
+
+It should not be assumed that treating the register as callee-saved
+will be sufficient to satisfy the requirements of the platform."
+
+Our conformance testing framework is parallelized -- we spawn a task
+for each random test. This is why we cannot expect the contents of
+`x18` to be preserved -- `x18` is reserved on Apple's Arm machines and
+probably carries thread context (though we haven't actually found a
+reference for the latter). See
+https://developer.apple.com/documentation/xcode/writing-arm64-code-for-apple-platforms#Respect-the-purpose-of-specific-CPU-registers
+for details.
+
+As such, when we check whether our model's state matches the machine
+after every instruction test, we ignore the contents of `x18` only on
+Arm-based Apple machines -- `x18` is still checked on other Arm
+machines. See `gpr_mismatch` and `regStates_match` for details.
+-/
+
 open BitVec
 
 /-- A default concrete state to begin co-simulations. -/
@@ -173,10 +215,16 @@ def model_to_regState (inst : BitVec 32) (s : ArmState) : regState :=
     nzcv := nzcv s,
     sfp  := sfp_list s }
 
-def gpr_mismatch (x1 x2 : List (BitVec 64)) : IO String := do
+/-- Check whether the machine and model GPRs match. We ignore register
+`x18` on Arm-based Apple platforms because `x18` cannot be guaranteed
+to be preserved there. -/
+def gpr_mismatch (isDarwin : Bool) (x1 x2 : List (BitVec 64)) : IO String := do
   let mut acc := ""
   for i in [0:31] do
-    if x1[i]! == x2[i]! then
+    if isDarwin && i == 18 then
+      -- Ignore x18 contents.
+      continue
+    else if x1[i]! == x2[i]! then
       continue
     else
       acc := acc ++ s!"GPR{i} machine {x1[i]!} model {x2[i]!}"
@@ -205,17 +253,34 @@ def nzcv_mismatch (x1 x2 : BitVec 4) : IO String := do
       acc := acc ++ s!"Flag{flag} machine {f1} model {f2}"
   pure acc
 
-def regStates_match (input o1 o2 : regState) : IO Bool := do
+def regStates_match (uniqueBaseName : String) (input o1 o2 : regState) :
+  IO Bool := do
   if o1 == o2 then
-     pure true
+      pure true
   else
-     let gpr_mismatch ← gpr_mismatch o1.gpr o2.gpr
+    let darwin_check ←
+    IO.Process.output
+      { cmd  := "Arm/Insts/Cosim/platform_check.sh",
+        args := #["-d"] }
+    let isDarwin := (darwin_check.exitCode == 1)
+     let gpr_mismatch ← gpr_mismatch isDarwin o1.gpr o2.gpr
      let nzcv_mismatch ← nzcv_mismatch o1.nzcv o2.nzcv
      let sfp_mismatch  ← sfp_mismatch o1.sfp o2.sfp
-     IO.println s!"Instruction: {decode_raw_inst input.inst}"
-     IO.println s!"input: {toString input}"
-     IO.println s!"Mismatch found: {gpr_mismatch} {nzcv_mismatch} {sfp_mismatch}"
-     pure false
+     if gpr_mismatch.isEmpty &&
+        nzcv_mismatch.isEmpty &&
+        sfp_mismatch.isEmpty then
+        -- If we are on an Arm-based Apple platform where only the
+        -- value of `x18` differs between the model and the machine,
+        -- then we don't flag a mismatch. This register is not
+        -- expected to be preserved on this platform.
+        pure true
+     else
+       -- TODO: also print the instruction class and sample.
+       IO.println s!"ID: {uniqueBaseName}"
+       IO.println s!"Instruction: {decode_raw_inst input.inst}"
+       IO.println s!"input: {toString input}"
+       IO.println s!"Mismatch found: {gpr_mismatch} {nzcv_mismatch} {sfp_mismatch}"
+       pure false
 
 /-- Run one random test for the instruction `inst`. -/
 def one_test (inst : BitVec 32) (uniqueBaseName : String) : IO Bool := do
@@ -224,7 +289,7 @@ def one_test (inst : BitVec 32) (uniqueBaseName : String) : IO Bool := do
   let machine_st := machine_to_regState inst machine
   let model      := run 1 (regState_to_armState input)
   let model_st := model_to_regState inst model
-  regStates_match input machine_st model_st
+  regStates_match uniqueBaseName input machine_st model_st
 
 /--
 Make a task for running a single test.

Arm/Insts/Common.lean

@@ -13,18 +13,15 @@ section Common
 open BitVec
 
 ----------------------------------------------------------------------
-/-- `GPRIndex.rand` picks a safe GPR index (i.e., one not reserved on
-Apple platforms). Use this function instead of `BitVec.rand` to pick
-an appropriate random index for a destination GPR during
-cosimulations. We say "destination" because using reserved registers
-as source operands does not violate the Apple ABI.
-
-For details, see
-https://developer.apple.com/documentation/xcode/writing-arm64-code-for-apple-platforms#Respect-the-purpose-of-specific-CPU-registers
-
-Also see "Procedure Call Standard for the Arm 64-bit Architecture";
-the latest version is available at
-https://github.com/ARM-software/abi-aa/releases
+
+/-- 
+`GPRIndex.rand` picks a safe GPR index for Arm-based Apple platforms
+i.e., one not reserved on them. Use this function instead of
+`BitVec.rand` to pick an appropriate random index for a source and
+destination GPR during cosimulations. 
+
+See "NOTE: Considerations for running cosimulations on Arm-based Apple
+platforms" in Arm/Cosim.lean for details.
 -/
 partial def GPRIndex.rand (lo := 0) (hi := 31) :
   IO (BitVec 5) := do

Arm/Insts/DPI/Add_sub_imm.lean

@@ -52,7 +52,7 @@ def Add_sub_imm_cls.inst.rand : IO (Option (BitVec 32)) := do
        -- 31) since our simulation framework doesn't work in such
        -- cases. For now, we do sacrifice a little bit of the state
        -- space.
-      Rn    := ← BitVec.rand 5 (lo := 0) (hi := 30),
+      Rn    := ← GPRIndex.rand (lo := 0) (hi := 30),
       Rd    := ← GPRIndex.rand (lo := 0) (hi := 30) }
   pure (some (inst.toBitVec32))
 

Arm/Insts/DPI/Bitfield.lean

@@ -75,7 +75,7 @@ partial def Bitfield_cls.all.rand : IO (Option (BitVec 32)) := do
       N     := N,
       immr  := immr,
       imms  := imms,
-      Rn    := ← BitVec.rand 5,
+      Rn    := ← GPRIndex.rand,
       Rd    := ← GPRIndex.rand }
   pure (some (inst.toBitVec32))
  where pick_legal_bitfield_opc : IO (BitVec 2) := do
@@ -101,7 +101,7 @@ partial def Bitfield_cls.lsr.rand : IO (Option (BitVec 32)) := do
       N     := N,
       immr  := immr,
       imms  := imms,
-      Rn    := ← BitVec.rand 5,
+      Rn    := ← GPRIndex.rand,
       Rd    := ← GPRIndex.rand }
   pure (some (inst.toBitVec32))
 
@@ -117,7 +117,7 @@ partial def Bitfield_cls.lsl.rand : IO (Option (BitVec 32)) := do
       N     := N,
       immr  := immr,
       imms  := imms,
-      Rn    := ← BitVec.rand 5,
+      Rn    := ← GPRIndex.rand,
       Rd    := ← GPRIndex.rand }
   pure (some (inst.toBitVec32))
   where pick_legal_lsl_low_imms_bits : IO (BitVec 5) := do

Arm/Insts/DPI/Logical_imm.lean

@@ -75,7 +75,7 @@ partial def Logical_imm_cls.inst.rand : IO (Option (BitVec 32)) := do
       N     := ← BitVec.rand 1,
       immr  := ← BitVec.rand 6,
       imms  := ← BitVec.rand 6,
-      Rn    := ← BitVec.rand 5 (lo := 0) (hi := hi),
+      Rn    := ← GPRIndex.rand (lo := 0) (hi := hi),
       Rd    := ← GPRIndex.rand (lo := 0) (hi := hi)
     }
   let datasize := 32 <<< inst.sf.toNat

Arm/Insts/DPR/Add_sub_carry.lean

@@ -38,8 +38,8 @@ def Add_sub_carry_cls.rand : IO (Option (BitVec 32)) := do
     { sf    := ← BitVec.rand 1,
       op    := ← BitVec.rand 1,
       S     := ← BitVec.rand 1,
-      Rm    := ← BitVec.rand 5,
-      Rn    := ← BitVec.rand 5,
+      Rm    := ← GPRIndex.rand,
+      Rn    := ← GPRIndex.rand,
       Rd    := ← GPRIndex.rand }
   pure (some (inst.toBitVec32))
 

Arm/Insts/DPR/Add_sub_shifted_reg.lean

@@ -52,9 +52,9 @@ partial def Add_sub_shifted_reg_cls.rand : IO (Option (BitVec 32)) := do
         op    := ← BitVec.rand 1,
         S     := ← BitVec.rand 1,
         shift := shift,
-        Rm    := ← BitVec.rand 5,
+        Rm    := ← GPRIndex.rand,
         imm6  := imm6,
-        Rn    := ← BitVec.rand 5,
+        Rn    := ← GPRIndex.rand,
         Rd    := ← GPRIndex.rand }
     pure (some (inst.toBitVec32))
 

Arm/Insts/DPR/Conditional_select.lean

@@ -44,10 +44,10 @@ def Conditional_select_cls.rand : IO (Option (BitVec 32)) := do
     { sf    := ← BitVec.rand 1,
       op    := ← pure 0#1,
       S     := ← pure 0#1,
-      Rm    := ← BitVec.rand 5,
+      Rm    := ← GPRIndex.rand,
       cond  := ← BitVec.rand 4,
       op2   := ← pure 0b00#2,
-      Rn    := ← BitVec.rand 5,
+      Rn    := ← GPRIndex.rand,
       Rd    := ← GPRIndex.rand }
   pure (some (inst.toBitVec32))
 

Arm/Insts/DPR/Data_processing_one_source.lean

@@ -111,7 +111,7 @@ partial def Data_processing_one_source_cls.rev_all.rand : IO (Option (BitVec 32)
         S := 0b0#1,
         opcode2 := 0b00000#5,
         opcode := 0b0000#4 ++ opc,
-        Rn := ← BitVec.rand 5,
+        Rn := ← GPRIndex.rand,
         Rd := ← GPRIndex.rand
       }
     pure (some (inst.toBitVec32))

Arm/Insts/DPR/Data_processing_three_source.lean

@@ -79,10 +79,10 @@ def Data_processing_three_source_cls.shift.rand
     { sf := sf,
       op54 := op54,
       op31 := op31,
-      Rm := ← BitVec.rand 5,
+      Rm := ← GPRIndex.rand,
       o0 := o0,
-      Ra := ← BitVec.rand 5,
-      Rn := ← BitVec.rand 5,
+      Ra := ← GPRIndex.rand,
+      Rn := ← GPRIndex.rand,
       Rd := ← GPRIndex.rand
     }
   pure (some inst.toBitVec32)

Arm/Insts/DPR/Data_processing_two_source.lean

@@ -46,9 +46,9 @@ def Data_processing_two_source_cls.shift.rand
   let (inst : Data_processing_two_source_cls) :=
     { sf := ← BitVec.rand 1,
       S := 0b0#1,
-      Rm := ← BitVec.rand 5,
+      Rm := ← GPRIndex.rand,
       opcode := opcode,
-      Rn := ← BitVec.rand 5,
+      Rn := ← GPRIndex.rand,
       Rd := ← GPRIndex.rand
     }
   pure (some inst.toBitVec32)

Arm/Insts/DPR/Logical_shifted_reg.lean

@@ -82,9 +82,9 @@ partial def Logical_shifted_reg_cls.rand : IO (Option (BitVec 32)) := do
         opc   := ← BitVec.rand 2,
         shift := ← BitVec.rand 2,
         N     := ← BitVec.rand 1,
-        Rm    := ← BitVec.rand 5,
+        Rm    := ← GPRIndex.rand,
         imm6  := imm6,
-        Rn    := ← BitVec.rand 5,
+        Rn    := ← GPRIndex.rand,
         Rd    := ← GPRIndex.rand }
     pure (some (inst.toBitVec32))
 

Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean

@@ -91,26 +91,32 @@ partial def Conversion_between_FP_and_Int_cls.fmov_general.rand : IO (Option (Bi
   let sf := ← BitVec.rand 1
   let intsize := 32 <<< sf.toNat
   let decode_fltsize := if ftype == 0b10#2 then 64 else (8 <<< (ftype ^^^ 0b10#2).toNat)
-  if ftype == 0b10#2 && (extractLsb 2 1 opcode) ++ rmode != 0b1101#4
-  || decode_fltsize != 16 && decode_fltsize != intsize
-  || intsize != 64 || ftype != 0b10#2 then
+  if ftype == 0b10#2 && ((extractLsb 2 1 opcode) ++ rmode) != 0b1101#4 ||
+     decode_fltsize != 16 && decode_fltsize != intsize ||
+     intsize != 64 || ftype != 0b10#2 then
     Conversion_between_FP_and_Int_cls.fmov_general.rand
   else
     let (inst : Conversion_between_FP_and_Int_cls) :=
+      let gpr_idx := ←GPRIndex.rand
+      let sfp_idx := ←BitVec.rand 5
+      let (src_idx, dst_idx) :=
+        if (lsb opcode 0) = 1#1 then
+        -- FPConvOp.FPConvOp_MOV_ItoF
+        -- Source operand is a GPR.
+        -- Destination operand is a SIMD&FP register.
+          (gpr_idx, sfp_idx)
+       else
+       -- FPConvOp.FPConvOp_MOV_FtoI
+       -- Source operand is a SIMD&FP register.
+       -- Destination operand is a GPR.
+         (sfp_idx, gpr_idx)
       { sf := sf,
         S := 0b0#1,
         ftype := ftype,
         rmode  := rmode,
         opcode := opcode,
-        Rn := ← BitVec.rand 5,
-        Rd := ← (if (lsb opcode 0) = 1#1 then
-                -- FPConvOp.FPConvOp_MOV_ItoF
-                -- Destination operand is a SIMD&FP register.
-                  BitVec.rand 5
-                else
-                -- FPConvOp.FPConvOp_MOV_FtoI
-                -- Destination operand is a GPR register.
-                  GPRIndex.rand) }
+        Rn := src_idx,
+        Rd := dst_idx }
     pure (inst.toBitVec32)
 
 /-- Generate random instructions of Conversion_between_FP_and_Int class. -/

Arm/Memory/Separate.lean

@@ -582,7 +582,7 @@ theorem read_mem_bytes_write_mem_bytes_eq_extract_LsB_of_mem_subset
           rw [BitVec.le_def] at hstart
           omega
     · simp only [h₁, bitvec_rules, minimal_theory]
-      intros h
+      intros 
       apply BitVec.getLsb_ge
       omega
 

Arm/MinTheory.lean

@@ -94,6 +94,8 @@ attribute [minimal_theory] bne_iff_ne
 attribute [minimal_theory] Bool.false_eq
 attribute [minimal_theory] Bool.and_eq_false_imp
 
+attribute [minimal_theory] Decidable.not_not
+
 attribute [minimal_theory] Nat.le_zero_eq
 attribute [minimal_theory] Nat.zero_add
 attribute [minimal_theory] Nat.zero_eq

Correctness/ArmSpec.lean

@@ -1,3 +1,12 @@
+/-
+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): Shilpi Goel
+
+Specializing the Correctness module for use with our specification of the Arm
+ISA.
+-/
+
 import Arm.Exec
 import Correctness.Correctness
 
@@ -18,4 +27,20 @@ theorem arm_run (n : Nat) (s : ArmState) :
     simp only [Sys.run, Sys.next, run]
     rw [h]
 
+-- (TODO) Move to Arm/BitVec.lean?
+/-- Unexpander to represent bitvector literals in hexadecimal -- this overrides
+  the unexpander in the Lean BitVec library. -/
+@[app_unexpander BitVec.ofNat] def unexpandBitVecOfNatToHex : Lean.PrettyPrinter.Unexpander
+  | `($(_) $n:num $i:num) =>
+      let i' := i.getNat
+      let n' := n.getNat
+      let trimmed_hex := -- Remove leading zeroes...
+        String.dropWhile (BitVec.ofNat n' i').toHex
+                         (fun c => c = '0')
+                         -- ... but keep one if the literal is all zeros.
+      let trimmed_hex := if trimmed_hex.isEmpty then "0" else trimmed_hex
+      let bv := Lean.Syntax.mkNumLit s!"0x{trimmed_hex}#{n'}"
+      `($bv:num)
+  | _ => throw ()
+
 end Correctness

Correctness/Correctness.lean

@@ -142,7 +142,8 @@ theorem partial_correctness_from_verification_conditions [Sys σ] [Spec' σ]
     (v1 : ∀ s0 : σ, pre s0 → assert s0 s0)
     (v2 : ∀ sf : σ, exit sf → cut sf)
     (v3 : ∀ s0 sf : σ, assert s0 sf → exit sf → post s0 sf)
-    (v4 : ∀ s0 si : σ, assert s0 si → ¬ exit si → assert s0 (nextc (next si)))
+    -- We prefer to use `run` instead of `step`.
+    (v4 : ∀ s0 si : σ, assert s0 si → ¬ exit si → assert s0 (nextc (run si 1)))
     : PartialCorrectness σ :=
   fun s0 n hp hexit =>
     let rec find (i : Nat) (h : assert s0 (run s0 i)) (hle : i ≤ n) :