Functions to trace ArmState during concrete simulations

.gitignore

@@ -2,3 +2,4 @@
 /lakefile.olean
 /lake-packages/*
 /.lake/*
+*.log

Arm/Insts/LDST/Advanced_simd_multiple_struct.lean

@@ -27,7 +27,7 @@ deriving DecidableEq, Repr
 @[state_simp_rules]
 def ld1_st1_operation (wback : Bool) (inst : Multiple_struct_inst_fields)
   (inst_str : String) (s : ArmState)
-  (H_opcode : inst.opcode ∈
+  (_H_opcode : inst.opcode ∈
               [0b0000#4, 0b0010#4, 0b0100#4, 0b0110#4, 0b0111#4,
               0b1000#4, 0b1010#4])
   : ArmState :=

Tests/Debug.lean

@@ -0,0 +1,63 @@
+/-
+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
+-/
+
+-- Some utilities for debugging concrete simulations
+
+import Arm.Exec
+
+section Debug
+
+open BitVec
+
+/-- `trace_run`: Print `(debug s)` before simulating each instruction. -/
+def trace_run (debug : ArmState → String) (n : Nat) (s : ArmState) : ArmState :=
+  match n with
+  | 0 => s
+  | n' + 1 =>
+    dbg_trace (debug s)
+    let s' := stepi s
+    trace_run debug n' s'
+
+/-- `log_run`: Log `(debug s)` to a file `filename` before
+     simulating each instruction. Note that we append to file, so
+     any old contents are not overwritten. -/
+def log_run (filename : System.FilePath) (debug : ArmState → String)
+  (n : Nat) (s : ArmState) : IO ArmState := do
+  let h ← IO.FS.Handle.mk filename IO.FS.Mode.append
+  h.putStrLn (debug s)
+  match n with
+  | 0 => pure s
+  | n' + 1 =>
+    let s' := stepi s
+    log_run filename debug n' s'
+
+/-- `run_until`: Run until `cond` is true or `n` instructions are simulated,
+  whichever comes first. -/
+def run_until (cond : ArmState → Bool) (n : Nat) (s : ArmState) : ArmState :=
+  match n with
+  | 0 => s
+  | n' + 1 =>
+    if (cond s) then
+      dbg_trace "Stopping condition reached!"
+      s
+    else
+      let s' := stepi s
+      run_until cond n' s'
+
+-- Examples of debug functions for use in `trace_run` and `log_run`:
+
+/-- `pc_trace`: Unconditionally trace the program counter. -/
+def pc_trace (s : ArmState) : String :=
+  "pc: " ++ (read_pc s).toHex
+
+/-- `non_zero_x2_trace`: Trace the program counter if x2 != 0#64. -/
+def non_zero_x2_trace (s : ArmState) : String :=
+  if (read_gpr 64 2 s) != 0#64 then
+    "pc: " ++ (read_pc s).toHex ++ ": x2 != 0"
+  else
+    ""
+
+end Debug

Tests/SHA512ProgramTest.lean

@@ -6,6 +6,7 @@ Author(s): Shilpi Goel
 import Arm.Exec
 import Arm.Cfg.Cfg
 import Specs.SHA512
+import Tests.Debug
 
 section SHA512ProgramTest
 
@@ -596,6 +597,10 @@ def init_sha512_test : ArmState :=
   let s := write_mem_bytes (80 * 8) ktbl_address SHA512_K s
   s
 
+-- Log the PCs of all the instructions that were simulated in
+-- `Tests/SHA512_PC.log`.
+-- #eval (log_run "Tests/SHA512_PC.log" pc_trace 503 init_sha512_test)
+
 def final_sha512_state : ArmState := run 503 init_sha512_test
 def final_sha512_pc : BitVec 64 := final_sha512_state.pc
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-05-16
+leanprover/lean4:nightly-2024-05-23