Add explicit PC metadata for instructions (#1825)

doc/data-templates.adoc

@@ -97,6 +97,9 @@ access:
   vs: always   # VS-mode access
   vu: always   # VU-mode access
 data_independent_timing: true  # For cryptographic extensions
+pc: # program counter
+  references: true # Optional: instruction semantics reference the current PC
+  changes: false   # Optional: instruction semantics update the PC
 operation(): |
   # IDL code implementing the instruction
   X[xd] = X[xs1] + $signed(imm);
@@ -110,6 +113,11 @@ Common variable properties:
 * `sign_extend` - Set to `true` for signed immediates
 * `left_shift` - Shift value left by N bits (common for branch offsets)
 
+Optional instruction metadata:
+
+* `pc.references` - Set to `true` when the instruction semantics explicitly reference the current PC
+* `pc.changes` - Set to `true` when the instruction semantics explicitly update the PC
+
 === Pseudoinstructions
 
 Instructions can define pseudoinstruction mappings:

spec/schemas/inst_schema.json

@@ -395,6 +395,23 @@
       "description": "Whether or not the instruction must execute with data-independent timing when the Zkt extension is supported",
       "default": false
     },
+    "pc": {
+      "type": "object",
+      "description": "Whether the instruction reads and/or writes the program counter",
+      "properties": {
+        "references": {
+          "type": "boolean",
+          "default": false,
+          "description": "Whether the instruction semantics reference the current program counter"
+        },
+        "changes": {
+          "type": "boolean",
+          "default": false,
+          "description": "Whether the instruction semantics update the program counter"
+        }
+      },
+      "additionalProperties": false
+    },
     "pseudoinstructions": {
       "description": "Variations of this instruction that form a pseudoinstruction",
       "type": "array",

spec/std/isa/inst/I/auipc.yaml

@@ -28,4 +28,6 @@ access:
   vs: always
   vu: always
 data_independent_timing: true
+pc:
+  references: true
 operation(): X[xd] = $pc + $signed(imm);

spec/std/isa/inst/I/jalr.yaml

@@ -31,6 +31,9 @@ access:
   u: always
   vs: always
   vu: always
+pc:
+  references: true
+  changes: true
 pseudoinstructions:
   - when: xd == 0
     to: jr imm(xs1)

spec/std/isa/inst/I/mret.yaml

@@ -16,6 +16,8 @@ access:
   u: never
   vs: never
   vu: never
+pc:
+  changes: true
 encoding:
   match: "00110000001000000000000001110011"
 operation(): |

tools/ruby-gems/udb/lib/udb/obj/instruction.rb

@@ -401,6 +401,12 @@ def base
     # @return [Boolean] Whether or not the instruction must have data-independent timing when Zkt is enabled.
     def data_independent_timing? = @data["data_independent_timing"]
 
+    # @return [Boolean] Whether or not the instruction semantics reference the current PC.
+    def pc_references? = @data.dig("pc", "references") || false
+
+    # @return [Boolean] Whether or not the instruction semantics update the PC.
+    def pc_changes? = @data.dig("pc", "changes") || false
+
     # @param xlen [Integer] 32 or 64, the target xlen
     # @return [Boolean] whethen or not instruction is defined in base +xlen+
     def defined_in_base?(xlen)

tools/ruby-gems/udb/test/test_instruction.rb

@@ -12,6 +12,18 @@
 class TestInstruction < Minitest::Test
   include Udb
 
+  private def operation_text(inst)
+    inst.instance_variable_get(:@data)["operation()"]
+  end
+
+  private def idl_references_pc?(operation)
+    operation.include?("$pc")
+  end
+
+  private def idl_changes_pc?(operation)
+    operation.match?(/(?:jump(?:_halfword)?\(|^\s*\$pc\s*=)/)
+  end
+
   def setup
     @resolver = Udb::Resolver.new(Udb.repo_root)
     @cfg_arch = @resolver.cfg_arch_for("_")
@@ -61,4 +73,45 @@ def test_decode_variable_without_sext
     extracted = rs1_var.extract
     refute_match(/sext/, extracted, "non-signed decode variable should not use sext")
   end
+
+  def test_explicit_pc_metadata
+    db = @cfg_arch
+
+    auipc_inst = db.instructions.find { |i| i.name == "auipc" }
+    refute_nil auipc_inst, "AUIPC instruction should be found"
+    assert auipc_inst.pc_references?, "AUIPC should explicitly reference the PC"
+    refute auipc_inst.pc_changes?, "AUIPC should not explicitly change the PC"
+
+    jalr_inst = db.instructions.find { |i| i.name == "jalr" }
+    refute_nil jalr_inst, "JALR instruction should be found"
+    assert jalr_inst.pc_references?, "JALR should explicitly reference the PC"
+    assert jalr_inst.pc_changes?, "JALR should explicitly change the PC"
+
+    mret_inst = db.instructions.find { |i| i.name == "mret" }
+    refute_nil mret_inst, "MRET instruction should be found"
+    refute mret_inst.pc_references?, "MRET should not explicitly reference the current PC"
+    assert mret_inst.pc_changes?, "MRET should explicitly change the PC"
+
+    add_inst = db.instructions.find { |i| i.name == "add" }
+    refute_nil add_inst, "ADD instruction should be found"
+    refute add_inst.pc_references?, "Instructions without pc metadata should default to not referencing the PC"
+    refute add_inst.pc_changes?, "Instructions without pc metadata should default to not changing the PC"
+  end
+
+  def test_explicit_pc_metadata_agrees_with_idl
+    @cfg_arch.instructions.each do |inst|
+      next unless inst.pc_references? || inst.pc_changes?
+
+      operation = operation_text(inst)
+      refute_nil operation, "#{inst.name} should define operation() when explicit pc metadata is present"
+
+      if inst.pc_references?
+        assert idl_references_pc?(operation), "#{inst.name} pc.references should agree with operation()"
+      end
+
+      if inst.pc_changes?
+        assert idl_changes_pc?(operation), "#{inst.name} pc.changes should agree with operation()"
+      end
+    end
+  end
 end