Merge pull request #20 from riscv-software-src/dhower/config_independ…

…ent_type_check

Perform type checking on config-indpendent IDL code.

Gemfile

@@ -10,6 +10,7 @@ gem "base64"
 gem "bigdecimal"
 gem "json_schemer", "~> 1.0"
 gem "minitest"
+gem "ruby-progressbar", "~> 1.13"
 gem "pygments.rb"
 gem "rake", "~> 13.0"
 gem "rouge"

Gemfile.lock

@@ -153,6 +153,7 @@ DEPENDENCIES
   rouge
   rubocop-minitest
   ruby-prof
+  ruby-progressbar (~> 1.13)
   solargraph
   treetop (= 1.6.12)
   webrick

Rakefile

@@ -3,6 +3,7 @@
 $root = Pathname.new(__FILE__).dirname.realpath
 $lib = $root / "lib"
 
+require "ruby-progressbar"
 require "yard"
 require "minitest/test_task"
 
@@ -64,10 +65,48 @@ end
 desc "Validate the arch docs"
 task validate: "gen:arch" do
   validator = Validator.instance
-  Dir.glob("#{$root}/arch/**/*.yaml") do |f|
+  puts "Checking arch files against schema.."
+  arch_files = Dir.glob("#{$root}/arch/**/*.yaml")
+  progressbar = ProgressBar.create(total: arch_files.size)
+  arch_files.each do |f|
+    progressbar.increment
     validator.validate(f)
   end
   puts "All files validate against their schema"
+
+  puts "Type checking IDL code..."
+  arch_def = arch_def_for("_")
+  progressbar = ProgressBar.create(title: "Instructions", total: arch_def.instructions.size)
+  arch_def.instructions.each do |inst|
+    progressbar.increment
+    inst.type_checked_operation_ast(arch_def.idl_compiler, arch_def.sym_table_32, 32) if inst.rv32?
+    inst.type_checked_operation_ast(arch_def.idl_compiler, arch_def.sym_table_64, 64) if inst.rv64?
+    # also need to check for an RV64 machine running with effective XLEN of 32
+    inst.type_checked_operation_ast(arch_def.idl_compiler, arch_def.sym_table_64, 32) if inst.rv64? && inst.rv32?
+  end
+  progressbar = ProgressBar.create(title: "CSRs", total: arch_def.csrs.size)
+  arch_def.csrs.each do |csr|
+    progressbar.increment
+    if csr.has_custom_sw_read?
+      csr.type_checked_sw_read_ast(arch_def.sym_table_32) if csr.defined_in_base32?
+      csr.type_checked_sw_read_ast(arch_def.sym_table_64) if csr.defined_in_base64?
+    end
+    csr.fields.each do |field|
+      unless field.type_ast(arch_def.idl_compiler).nil?
+        field.type_checked_type_ast(arch_def.sym_table_32) if csr.defined_in_base32? && field.defined_in_base32?
+        field.type_checked_type_ast(arch_def.sym_table_64) if csr.defined_in_base64? && field.defined_in_base64?
+      end
+      unless field.reset_value_ast(arch_def.idl_compiler).nil?
+        field.type_checked_reset_value_ast(arch_def.sym_table_32) if csr.defined_in_base32? && field.defined_in_base32?
+        field.type_checked_reset_value_ast(arch_def.sym_table_64) if csr.defined_in_base64? && field.defined_in_base64?
+      end
+      unless field.sw_write_ast(arch_def.idl_compiler).nil?
+        field.type_checked_sw_write_ast(arch_def.sym_table_32, 32) if csr.defined_in_base32? && field.defined_in_base32?
+        field.type_checked_sw_write_ast(arch_def.sym_table_64, 64) if csr.defined_in_base64? && field.defined_in_base64?
+      end
+    end
+  end
+  puts "All IDL passed type checking"
 end
 
 def insert_warning(str, from)
@@ -76,6 +115,7 @@ def insert_warning(str, from)
   first_line = lines.shift
   lines.unshift(first_line, "\n# WARNING: This file is auto-generated from #{Pathname.new(from).relative_path_from($root)}\n\n").join("")
 end
+private :insert_warning
 
 (3..31).each do |hpm_num|
   file "#{$root}/arch/csr/Zihpm/mhpmcounter#{hpm_num}.yaml" => [

arch/csr/H/hcounteren.yaml

@@ -12,7 +12,7 @@ hcounteren:
     Together with `scounteren`, delegates control of the hardware performance-monitoring counters
     to VS/VU-mode
 
-    See `cycle` for a table of how exceptions occur across all modes.
+    See `cycle` for a table describing how exceptions occur.
   definedBy: H
   fields:
     CY:

arch/csr/H/vsatp.yaml

@@ -0,0 +1,141 @@
+# yaml-language-server: $schema=../../schemas/csr_schema.json
+
+vsatp:
+  address: 0x280
+  virtual_address: 0x180
+  long_name: Virtual Supervisor Address Translation and Protection
+  description: |
+    The `vsatp` register is a VSXLEN-bit read/write register that is VS-mode's version of supervisor
+    register `satp`.
+    When V=1, `vsatp` substitutes for the usual `satp`, so instructions that normally read or modify
+    `satp` actually access `vsatp` instead.
+    `vsatp` controls VS-stage address translation, the first stage of two-stage translation for
+    guest virtual addresses.
+
+    The `vsatp` register is considered active for the purposes of the address-translation algorithm
+    unless the effective privilege mode is U and `hstatus.HU`=0.
+    However, even when `vsatp` is active, VS-stage page-table entries' A bits must not be set as a
+    result of speculative execution, unless the effective privilege mode is VS or VU.
+
+    [NOTE]
+    In particular, virtual-machine load/store (`hlv`, 'hlvx', or 'hsv') instructions that are
+    misspeculatively executed must not cause VS-stage A bits to be set.
+
+    When V=0, a write to `vsatp` with an unsupported MODE value is either ignored as it is for
+    `satp`, or the fields of `vsatp` are treated as WARL in the normal way.
+    However, when V=1, a write to `satp` with an unsupported MODE value is ignored and no write to
+    `vsatp` is effected.
+  priv_mode: VS
+  length: VSXLEN
+  definedBy: H
+  fields:
+    MODE:
+      location_rv64: 63-60
+      location_rv32: 31
+      type: RW-R
+      description: |
+        *Translation Mode*
+
+        Controls the current translation mode in VS-mode according to the table below.
+
+        [separator="!",%autowidth]
+        !===
+        ! Value ! Name ! Description
+
+        ! 0 ! Bare a! No translation -> virtual address == physical address
+        <%- if ext?(:Sv39) -%>
+        ! 8 ! Sv39 ! 39-bit virtual address translation
+        <%- end -%>
+        <%- if ext?(:Sv48) -%>
+        ! 9 ! Sv48 ! 48-bit virtual address translation
+        <%- end -%>
+        <%- if ext?(:Sv57) -%>
+        ! 10 ! Sv57 ! 57-bit virtual address translation
+        <%- end -%>
+        !===
+
+        Any other value shall be ignored on a write.
+      reset_value: UNDEFINED_LEGAL
+      sw_write(csr_value): |
+        if (csr_value.MODE == 0) {
+          if (virtual_mode?() || IGNORE_INVALID_VSATP_MODE_WRITES_WHEN_V_EQ_ZERO) {
+            # In Bare, ASID and PPN must be zero, else the entire write is ignored
+            if (csr_value.ASID == 0 && csr_value.PPN == 0) {
+              return csr_value.MODE;
+            } else {
+              return UNDEFINED_LEGAL_DETERMINISTIC;
+            }
+          } else {
+            return UNDEFINED_LEGAL_DETERMINISTIC;
+          }
+        }
+        else if (implemented?(ExtensionName::Sv39) && csr_value.MODE == 8) { return csr_value.MODE; }
+        else if (implemented?(ExtensionName::Sv48) && csr_value.MODE == 9) { return csr_value.MODE; }
+        else if (implemented?(ExtensionName::Sv57) && csr_value.MODE == 10) { return csr_value.MODE; }
+        else {
+          return UNDEFINED_LEGAL_DETERMINISTIC;
+        }
+    ASID:
+      location_rv32: 30-22
+      location_rv64: 59-44
+      description: |
+        *Address Space ID*
+      type: RW-R
+      sw_write(csr_value): |
+        if (csr_value.MODE == 0) {
+          if (virtual_mode?() || IGNORE_INVALID_VSATP_MODE_WRITES_WHEN_V_EQ_ZERO) {
+            # when MODE == Bare, PPN and ASID must be zero
+            if (csr_value.ASID == 0 && csr_value.PPN == 0) {
+              return csr_value.ASID;
+            } else {
+              return UNDEFINED_LEGAL_DETERMINISTIC;
+            }
+          } else {
+            return UNDEFINED_LEGAL_DETERMINISTIC;
+          }
+        } else {
+          XReg shamt = (CSR[mstatus].SXL == $bits(XRegWidth::XLEN64)) ? 16 : 9;
+          XReg all_ones = ((1 << shamt) - 1);
+          XReg largest_allowed_asid = (1 << shamt) - 1;
+
+          if (csr_value.ASID == all_ones) {
+            # the specification states that if all 1's are written to the ASID field, then
+            # you must return the largest asid
+            return largest_allowed_asid;
+          } else if (csr_value.ASID > largest_allowed_asid) {
+            # ... but is silent on what happens on any other illegal value
+            return UNDEFINED_LEGAL_DETERMINISTIC;
+          } else {
+            # unrestricted
+            return csr_value.ASID;
+          }
+        }
+      reset_value: UNDEFINED_LEGAL
+    PPN:
+      location_rv32: 21-0
+      location_rv64: 43-0
+      description: |
+        *Physical Page Number*
+
+        The physical address of the active root page table is PPN << 12.
+
+        Can only hold values that correspond to a valid page table base, which
+        will be implementation-dependent.
+      type: RW-R
+      reset_value: UNDEFINED_LEGAL
+      sw_write(csr_value): |
+        if (csr_value.MODE == 0) {
+          if (virtual_mode?() || IGNORE_INVALID_VSATP_MODE_WRITES_WHEN_V_EQ_ZERO) {          
+            # when MODE == Bare, PPN and ASID must be zero
+            if (csr_value.ASID == 0 && csr_value.PPN == 0) {
+              return csr_value.PPN;
+            } else {
+              return UNDEFINED_LEGAL_DETERMINISTIC;
+            }
+          } else {
+            return UNDEFINED_LEGAL_DETERMINISTIC;
+          }
+        } else {
+          # unrestricted
+          return csr_value.PPN;
+        }

arch/csr/I/mcounteren.layout

@@ -102,13 +102,13 @@ mcounteren:
         When `hcounteren.CY` && `scounteren.CY` are both set, `cycle` is futher accessible to VU-mode.
         <%%- end -%>
       type(): |
-        if (COUNTENABLE_EN[2]) {
+        if (MCOUNTENABLE_EN[2]) {
           return CsrFieldType::RW;
         } else {
           return CsrFieldType::RO;
         }
       reset_value(): |
-        if (COUNTENABLE_EN[2]) {
+        if (MCOUNTENABLE_EN[2]) {
           return UNDEFINED_LEGAL;
         } else {
           return 0;
@@ -140,13 +140,13 @@ mcounteren:
         When `hcounteren.IR` && `scounteren.IR` are both set, `instret` is futher accessible to VU-mode.
         <%%- end -%>
       type(): |
-        if (COUNTENABLE_EN[2]) {
+        if (MCOUNTENABLE_EN[2]) {
           return CsrFieldType::RW;
         } else {
           return CsrFieldType::RO;
         }
       reset_value(): |
-        if (COUNTENABLE_EN[2]) {
+        if (MCOUNTENABLE_EN[2]) {
           return UNDEFINED_LEGAL;
         } else {
           return 0;
@@ -172,13 +172,13 @@ mcounteren:
         When `hcounteren.HPM<%= hpm_num %>` && `scounteren.HPM<%= hpm_num %>` are both set, `hpmcounter<%= hpm_num %>` is futher accessible to VU-mode.
         <%%- end -%>
       type(): |
-        if (COUNTENABLE_EN[<%= hpm_num %>]) {
+        if (MCOUNTENABLE_EN[<%= hpm_num %>]) {
           return CsrFieldType::RW;
         } else {
           return CsrFieldType::RO;
         }
       reset_value(): |
-        if (COUNTENABLE_EN[<%= hpm_num %>]) {
+        if (MCOUNTENABLE_EN[<%= hpm_num %>]) {
           return UNDEFINED_LEGAL;
         } else {
           return 0;

arch/csr/I/mcounteren.yaml

@@ -1,4 +1,4 @@
-# yaml-language-server: $schema=../../../schemas/csr_schema.json
+# yaml-language-server: $schema=../../schemas/csr_schema.json
 
 # WARNING: This file is auto-generated from arch/csr/I/mcounteren.layout
 
@@ -105,48 +105,24 @@ mcounteren:
         When `hcounteren.CY` && `scounteren.CY` are both set, `cycle` is futher accessible to VU-mode.
         <%- end -%>
       type(): |
-        if (MCOUNTENABLE_EN[0]) {
+        if (MCOUNTENABLE_EN[2]) {
           return CsrFieldType::RW;
         } else {
           return CsrFieldType::RO;
         }
       reset_value(): |
-        if (MCOUNTENABLE_EN[0]) {
+        if (MCOUNTENABLE_EN[2]) {
           return UNDEFINED_LEGAL;
         } else {
           return 0;
         }
     TM:
       location: 1
       description: |
-        When set, the `time` CSR (an alias of the `mtime` memory-mapped CSR) is accessible to
-        <%- if ext?(:S) -%>
-        S-mode.
-        <%- else -%>
-        U-mode.
-        <%- end -%>
-
-        <%- if ext?(:S) -%>
-        When `scounteren.TM` is also set, `time` is futher accessible to U-mode.
-        <%- end -%>
-
-        <%- if ext?(:H) -%>
-        When `hcounteren.TM` is also set, `time` is futher accessible to VS-mode.
-
-        When `hcounteren.TM` && `scounteren.TM` are both set, `time` is futher accessible to VU-mode.
-        <%- end -%>
-      type(): |
-        if (MCOUNTENABLE_EN[1]) {
-          return CsrFieldType::RW;
-        } else {
-          return CsrFieldType::RO;
-        }
-      reset_value(): |
-        if (MCOUNTENABLE_EN[1]) {
-          return UNDEFINED_LEGAL;
-        } else {
-          return 0;
-        }
+        Placeholder for delegating `time` to less-privileged modes; however, since `time`
+        is memory-mapped rather than a CSR, this field is always read-only zero.
+      type: RO
+      reset_value: 0
     IR:
       location: 2
       description: |

arch/csr/Zihpm/mhpmcounter10h.yaml

@@ -19,10 +19,10 @@ mhpmcounter10h:
       alias: mhpmcounter.COUNT10[63:32]
       description: |
         Upper bits of counter.
-      type(): 'return (NUM_HPM_COUNTERS > 7) ? CsrFieldType::RWH : CsrFieldType::RO;'
-      reset_value(): 'return (NUM_HPM_COUNTERS > 7) ? UNDEFINED_LEGAL : 0;'
+      type(): 'return (HPM_COUNTER_EN[10]) ? CsrFieldType::RWH : CsrFieldType::RO;'
+      reset_value(): 'return (HPM_COUNTER_EN[10]) ? UNDEFINED_LEGAL : 0;'
   sw_read(): |
-    if (NUM_HPM_COUNTERS <= 7) {
+    if (HPM_COUNTER_EN[10]) {
       return read_hpm_counter(10)[63:32];
     } else {
       return 0;

arch/csr/Zihpm/mhpmcounter11h.yaml

@@ -19,10 +19,10 @@ mhpmcounter11h:
       alias: mhpmcounter.COUNT11[63:32]
       description: |
         Upper bits of counter.
-      type(): 'return (NUM_HPM_COUNTERS > 8) ? CsrFieldType::RWH : CsrFieldType::RO;'
-      reset_value(): 'return (NUM_HPM_COUNTERS > 8) ? UNDEFINED_LEGAL : 0;'
+      type(): 'return (HPM_COUNTER_EN[11]) ? CsrFieldType::RWH : CsrFieldType::RO;'
+      reset_value(): 'return (HPM_COUNTER_EN[11]) ? UNDEFINED_LEGAL : 0;'
   sw_read(): |
-    if (NUM_HPM_COUNTERS <= 8) {
+    if (HPM_COUNTER_EN[11]) {
       return read_hpm_counter(11)[63:32];
     } else {
       return 0;

arch/csr/Zihpm/mhpmcounter12h.yaml

@@ -19,10 +19,10 @@ mhpmcounter12h:
       alias: mhpmcounter.COUNT12[63:32]
       description: |
         Upper bits of counter.
-      type(): 'return (NUM_HPM_COUNTERS > 9) ? CsrFieldType::RWH : CsrFieldType::RO;'
-      reset_value(): 'return (NUM_HPM_COUNTERS > 9) ? UNDEFINED_LEGAL : 0;'
+      type(): 'return (HPM_COUNTER_EN[12]) ? CsrFieldType::RWH : CsrFieldType::RO;'
+      reset_value(): 'return (HPM_COUNTER_EN[12]) ? UNDEFINED_LEGAL : 0;'
   sw_read(): |
-    if (NUM_HPM_COUNTERS <= 9) {
+    if (HPM_COUNTER_EN[12]) {
       return read_hpm_counter(12)[63:32];
     } else {
       return 0;

arch/csr/Zihpm/mhpmcounter13h.yaml

@@ -19,10 +19,10 @@ mhpmcounter13h:
       alias: mhpmcounter.COUNT13[63:32]
       description: |
         Upper bits of counter.
-      type(): 'return (NUM_HPM_COUNTERS > 10) ? CsrFieldType::RWH : CsrFieldType::RO;'
-      reset_value(): 'return (NUM_HPM_COUNTERS > 10) ? UNDEFINED_LEGAL : 0;'
+      type(): 'return (HPM_COUNTER_EN[13]) ? CsrFieldType::RWH : CsrFieldType::RO;'
+      reset_value(): 'return (HPM_COUNTER_EN[13]) ? UNDEFINED_LEGAL : 0;'
   sw_read(): |
-    if (NUM_HPM_COUNTERS <= 10) {
+    if (HPM_COUNTER_EN[13]) {
       return read_hpm_counter(13)[63:32];
     } else {
       return 0;