From 58e790eb2d0ebdd984ca1be586a0aeac634135c1 Mon Sep 17 00:00:00 2001
From: Alfredo Rodrigues <Alfredo.Rodrigues@synopsys.com>
Date: Mon, 19 Aug 2024 16:31:09 +0100
Subject: [PATCH] new files for update the sail output

---
 .../asciidoctor-sail/asciidoctor-sail.rb      |  14 +
 .../asciidoctor-sail/highlighter.rb           | 165 ++++++
 .../asciidoctor-sail/macros.rb                | 472 ++++++++++++++++++
 .../asciidoctor-sail/sources.rb               |  24 +
 themes/riscv-pdf.yml                          |   6 +-
 5 files changed, 678 insertions(+), 3 deletions(-)
 create mode 100644 extensions/asciidoctor-sail/asciidoctor-sail.rb
 create mode 100644 extensions/asciidoctor-sail/asciidoctor-sail/highlighter.rb
 create mode 100644 extensions/asciidoctor-sail/asciidoctor-sail/macros.rb
 create mode 100644 extensions/asciidoctor-sail/asciidoctor-sail/sources.rb

diff --git a/extensions/asciidoctor-sail/asciidoctor-sail.rb b/extensions/asciidoctor-sail/asciidoctor-sail.rb
new file mode 100644
index 0000000..9f80f09
--- /dev/null
+++ b/extensions/asciidoctor-sail/asciidoctor-sail.rb
@@ -0,0 +1,14 @@
+# frozen_string_literal: true
+
+require 'asciidoctor/extensions'
+
+require_relative 'asciidoctor-sail/sources'
+require_relative 'asciidoctor-sail/macros'
+require_relative 'asciidoctor-sail/highlighter'
+
+Asciidoctor::Extensions.register do
+  block_macro Asciidoctor::Sail::SourceBlockMacro
+  include_processor Asciidoctor::Sail::SourceIncludeProcessor
+  include_processor Asciidoctor::Sail::DocCommentIncludeProcessor
+  include_processor Asciidoctor::Sail::WavedromIncludeProcessor
+end
diff --git a/extensions/asciidoctor-sail/asciidoctor-sail/highlighter.rb b/extensions/asciidoctor-sail/asciidoctor-sail/highlighter.rb
new file mode 100644
index 0000000..2e30ae5
--- /dev/null
+++ b/extensions/asciidoctor-sail/asciidoctor-sail/highlighter.rb
@@ -0,0 +1,165 @@
+# frozen_string_literal: true
+
+require 'rouge'
+
+# We define a rouge lexer for Sail source
+class SailLexer < Rouge::RegexLexer
+  title 'Sail'
+  desc 'Sail ISA Description Language (https://github.com/rems-project/sail)'
+  tag 'sail'
+  filenames '*.sail'
+
+  id = /[a-zA-Z_?][a-zA-Z0-9_?#]*/
+
+  # Specially handle inserted cross-references
+  sailref = /sailref:[^\[]*\[[^\]]*\]/
+
+  tyvar = /'[a-zA-Z_?][a-zA-Z0-9_?#]*/
+
+  # We are careful with the definition of operators to ensure openers
+  # like // and /* cannot prefix valid operators
+  op_char = '[!%&*+-./:<=>@^|]'
+  op_char_no_slash = '[!%&*+-.:<=>@^|]'
+  op_char_no_slash_star = '[!%&+-.:<=>@^|]'
+
+  # Sail operators can be suffixed with an underscore followed by a
+  # regular identifier i.e. <=_u for unsigned less that or equal to
+  op_suffix = "#{op_char}*(_#{id.source})"
+
+  # Operators of length 1, 2, and n > 2
+  operator1 = Regexp.new(op_char)
+  operator2 = Regexp.new("(#{op_char}#{op_char_no_slash_star})|(#{op_char_no_slash}#{op_char})")
+  operatorn = Regexp.new("(#{op_char}#{op_char_no_slash_star}#{op_suffix})|(#{op_char_no_slash}#{op_char}#{op_suffix})")
+
+  def self.return_type
+    @return_type ||= Set.new %w[
+      RETIRE_SUCCESS RETIRE_FAIL
+    ]
+  end
+
+  def self.keywords
+    @keywords ||= Set.new %w[
+      and as by match clause operator default end enum else forall foreach function mapping overload throw
+      try catch if in let var ref pure monadic register return scattered struct then type union newtype with
+      val outcome instantiation impl repeat until while do bitfield forwards backwards to from
+    ]
+  end
+
+  # Keywords that appear in types, and builtin special types
+  def self.keywords_type
+    @keywords_type ||= Set.new %w[
+      dec inc Int Order Bool Type bits bool int option unit implicit
+    ]
+  end
+
+  # These keywords appear like special functions rather than regular
+  # keywords, i.e. `assert(cond, "message")`
+  def self.builtins
+    @builtins ||= Set.new %w[
+      bitzero bitone exit false sizeof constraint true undefined
+    ]
+  end
+
+  # Reserved and internal keywords, as well as deprecated keywords
+  def self.reserved
+    @reserved ||= Set.new %w[
+      effect cast constant import module mutual configuration termination_measure internal_plet internal_return
+    ]
+  end
+
+  state :whitespace do
+    rule(/\s+/, Text::Whitespace)
+  end
+
+  state :root do
+    mixin :whitespace
+
+    rule(/\b(RETIRE_SUCCESS|RETIRE_FAIL)\b/, Name::Constant)
+
+    rule(/0x[0-9A-Fa-f_]+/, Num::Hex)
+    rule(/0b[0-1_]+/, Num::Bin)
+    rule(/[0-9]+\.[0-9]+/, Num::Float)
+    rule(/[0-9_]+/, Num::Integer)
+
+    rule(/"/, Str, :string)
+
+    rule tyvar, Name::Variable
+
+    rule(/(val\b)(\s+)(#{id})/) do
+      groups Keyword, Text::Whitespace, Name::Function
+    end
+
+    rule(/(function\b)(\s+)(#{id})/) do
+      groups Keyword, Text::Whitespace, Name::Function
+    end
+
+    rule %r{//}, Comment, :line_comment
+    rule %r{/\*}, Comment, :comment
+    rule(/\$\[/, Comment::Preproc, :attribute)
+    rule(/\$#{id}/, Comment::Preproc, :pragma)
+
+    # Function arrows
+    rule(/->/, Punctuation)
+
+    # Two character brackets
+    rule(/\[\|/, Punctuation)
+    rule(/\|\]/, Punctuation)
+   # rule(/{\|/, Punctuation)
+    rule(/\|}/, Punctuation)
+
+    rule(/[,@=(){}\[\];:]/, Punctuation)
+    rule operatorn, Operator
+    rule operator2, Operator
+    rule operator1, Operator
+
+    rule sailref, Name
+
+    rule id do |m|
+      name = m[0]
+
+      if self.class.keywords.include? name
+        token Keyword
+      elsif self.class.keywords_type.include? name
+        token Keyword::Type
+      elsif self.class.builtins.include? name
+        token Name::Builtin
+      elsif self.class.reserved.include? name
+        token Keyword::Reserved
+      elsif self.class.return_type.include? name
+        token Name::Constant
+      else
+        token Name
+      end
+    end
+  end
+
+  state :string do
+    rule(/"/, Str, :pop!)
+    # Sail escape sequences are a subset of OCaml's https://v2.ocaml.org/manual/lex.html#escape-sequence
+    rule(/\\([\\ntbr"']|x[a-fA-F0-9]{2}|[0-7]{3})/, Str::Escape)
+    rule(/[^\\"\n]+/, Str)
+  end
+
+  state :attribute do
+    rule(/\[/, Comment::Preproc, :attribute)
+    rule(/\]/, Comment::Preproc, :pop!)
+    rule(/[^\[\]]+/, Comment::Preproc)
+  end
+
+  state :pragma do
+    rule(/\n/, Text::Whitespace, :pop!)
+    rule(/[^\n]+/, Comment::Preproc)
+  end
+
+  state :line_comment do
+    rule(/\n/, Text::Whitespace, :pop!)
+    rule(/[^\n]+/, Comment)
+  end
+
+  state :comment do
+    rule %r{/\*}, Comment, :comment
+    rule %r{\*/}, Comment, :pop!
+    rule(/\n/, Text::Whitespace)
+    rule(/./, Comment)
+  end
+end
diff --git a/extensions/asciidoctor-sail/asciidoctor-sail/macros.rb b/extensions/asciidoctor-sail/asciidoctor-sail/macros.rb
new file mode 100644
index 0000000..0ac4bcd
--- /dev/null
+++ b/extensions/asciidoctor-sail/asciidoctor-sail/macros.rb
@@ -0,0 +1,472 @@
+# frozen_string_literal: true
+
+require 'delegate'
+
+module Asciidoctor
+  module Sail
+    @@ids = {}
+
+    def self.seen_id?(id)
+      @@ids.key?(id)
+    end
+
+    def self.get_id(id)
+      return unless @@ids.key?(id)
+
+      @@ids[id]
+    end
+
+    def self.add_id(id)
+      @@ids[id] = id
+    end
+
+    def self.add_id_parent(id, parent)
+      @@ids[id] = parent
+    end
+
+    # A snippet is a small chunk of Sail source with an optional file and location
+    class Snippet
+      attr_accessor :source, :file, :loc
+
+      def initialize(source, file = nil, loc = nil)
+        @source = source
+        @file = file
+        @loc = loc
+      end
+    end
+
+    module SourceMacro
+      include Asciidoctor::Logging
+
+      # Should match Docinfo.docinfo_version in Sail OCaml source
+      VERSION = 1
+      PLUGIN_NAME = 'asciidoctor-sail'
+
+      def get_sourcemap(doc, attrs, loc)
+        from = attrs.delete('from') { 'sail-doc' }
+        source_map = doc.attr(from)
+        if source_map.nil?
+          info = "Document attribute :#{from}: does not exist, so we don't know where to find any sources"
+          logger.error %(#{logger.progname} (#{PLUGIN_NAME})) do
+            message_with_context info, source_location: loc
+          end
+          raise "#{PLUGIN_NAME}: #{info}"
+        end
+        ::Asciidoctor::Sail::Sources.register(from, source_map)
+        json = ::Asciidoctor::Sail::Sources.get(from)
+        if json['version'] != VERSION
+          logger.warn %(#{logger.progname} (#{PLUGIN_NAME})) do
+            message_with_context "Version does not match version in source map #{source_map}", source_location: loc
+          end
+        end
+
+        [json, from]
+      end
+
+      def cross_referencing?(doc)
+        doc.attr?('sail-xref')
+      end
+
+      def get_type(attrs)
+        attrs.delete('type') { 'function' }
+      end
+
+      def get_part(attrs)
+        attrs.delete('part') { 'source' }
+      end
+
+      def get_split(attrs)
+        attrs.delete('split') { '' }
+      end
+
+      def read_snippet(json, part)
+        return ::Asciidoctor::Sail::Snippet.new(json) if json.is_a? String
+
+        json = json.fetch(part, json)
+
+        return ::Asciidoctor::Sail::Snippet.new(json) if json.is_a? String
+
+        source = ''
+        file = json['file']
+        loc = json['loc']
+
+        if json['contents'].nil?
+          raise "#{PLUGIN_NAME}: File #{file} does not exist" unless File.exist?(file)
+
+          contents = File.read(file)
+
+          # Get the source code, adjusting for the indentation of the first line of the span
+          indent = loc[2] - loc[1]
+
+          source = contents.byteslice(loc[2], loc[5] - loc[2])
+          source = (' ' * indent) + source
+        else
+          source = json['contents']
+        end
+
+        ::Asciidoctor::Sail::Snippet.new(source, file, loc)
+      end
+
+      def get_sail_object(json, target, attrs)
+        type = get_type(attrs)
+        json = json["#{type}s"]
+        raise "#{PLUGIN_NAME}: No Sail objects of type #{type}" if json.nil?
+
+        json = json[target]
+        raise "#{PLUGIN_NAME}: No Sail #{type} #{target} could be found" if json.nil?
+
+        links = json['links']
+
+        json = json[type]
+
+        if attrs.key? 'clause'
+          clause = attrs.delete('clause')
+          json.each do |child|
+            if match_clause(clause, child['pattern'])
+              json = child
+              break
+            end
+          end
+        elsif attrs.key? 'left-clause'
+          clause = attrs.delete('left-clause')
+          json.each do |child|
+            if match_clause(clause, child['left'])
+              json = child
+              break
+            end
+          end
+        elsif attrs.key? 'right-clause'
+          clause = attrs.delete('right-clause')
+          json.each do |child|
+            if match_clause(clause, child['right'])
+              json = child
+              break
+            end
+          end
+        elsif attrs.key? 'grep'
+          grep = attrs.delete('grep')
+          json.each do |child|
+            source = read_snippet(child, 'body').source
+            json = child if source =~ Regexp.new(grep)
+          end
+        end
+
+        [json, type, links]
+      end
+
+      # Compute the minimum indentation for any line in a source block
+      def minindent(tabwidth, source)
+        indent = -1
+        source.each_line do |line|
+          line_indent = 0
+          line.chars.each do |c|
+            case c
+            when ' '
+              line_indent += 1
+            when "\t"
+              line_indent += tabwidth
+            else
+              break
+            end
+          end
+          indent = line_indent if indent == -1 || line_indent < indent
+        end
+        indent
+      end
+
+      def insert_links(snippet, links, from, type)
+        return snippet.source if snippet.loc.nil? || snippet.file.nil? || links.nil?
+
+        cursor = snippet.loc[2]
+        link_end = nil
+        final = ''
+
+        snippet.source.each_byte do |b|
+          if !link_end.nil? && cursor == link_end
+            final += ']'
+            link_end = nil
+          else
+            links.each do |link|
+              if link['loc'][0] == cursor && link['file'] == snippet.file && link_end.nil?
+                final += "sailref:#{from}##{type}["
+                link_end = link['loc'][1]
+              end
+            end
+          end
+
+          final += b.chr
+          cursor += 1
+        end
+
+        final
+      end
+
+      def get_source(doc, target, attrs, loc)
+        json, from = get_sourcemap doc, attrs, loc
+        json, type, links = get_sail_object json, target, attrs
+        dedent = attrs.any? { |k, v| (k.is_a? Integer) && %w[dedent unindent].include?(v) }
+        strip = attrs.any? { |k, v| (k.is_a? Integer) && %w[trim strip].include?(v) }
+
+        part = get_part attrs
+        split = get_split attrs
+        snippet = if split == ''
+                    read_snippet(json, part)
+                  else
+                    ::Asciidoctor::Sail::Snippet.new(json['splits'][split])
+                  end
+
+        source = if cross_referencing? doc
+                   insert_links(snippet, links, from, type)
+                 else
+                   snippet.source
+                 end
+
+        source.strip! if strip
+
+        if dedent
+          lines = ''
+          min = minindent 4, source
+
+          source.each_line do |line|
+            lines += line[min..]
+          end
+          source = lines
+        end
+
+        [source, type, from]
+      end
+
+      def match_clause(desc, json)
+        if desc =~ /^([a-zA-Z_?][a-zA-Z0-9_?#]*)(\(.*\))$/
+          return false unless json['type'] == 'app' && json['id'] == ::Regexp.last_match(1)
+
+          patterns = json['patterns']
+          patterns = patterns[0] if patterns.length == 1
+
+          match_clause ::Regexp.last_match(2), patterns
+        elsif desc.length.positive? && desc[0] == '('
+          tuples = nil
+          tuples = if json.is_a? Array
+                     json
+                   elsif json['type'] == 'tuple'
+                     json['patterns']
+                   else
+                     [json]
+                   end
+
+          results = []
+          desc[1...-1].split(',').each_with_index do |desc, i|
+            results.push(match_clause(desc.strip, tuples[i]))
+          end
+          results.all?
+        elsif desc == '_'
+          true
+        elsif desc =~ /^([a-zA-Z_?][a-zA-Z0-9_?#]*)$/
+          json['type'] == 'id' && json['id'] == ::Regexp.last_match(1)
+        elsif desc =~ /^(0[bx][a-fA-F0-9]*)$/
+          json['type'] == 'literal' && json['value'] == ::Regexp.last_match(1)
+        else
+          false
+        end
+      end
+    end
+
+    class SourceBlockMacro < ::Asciidoctor::Extensions::BlockMacroProcessor
+      include SourceMacro
+
+      use_dsl
+
+      named :sail
+
+      def process(parent, target, attrs)
+        logger.info "Including Sail source #{target} #{attrs}"
+        loc = parent.document.reader.cursor_at_mark
+
+        source, type, from = get_source parent.document, target, attrs, loc
+
+        id = if type == 'function'
+               "#{from}-#{target}"
+             else
+               "#{from}-#{type}-#{target}"
+             end
+
+        if ::Asciidoctor::Sail.seen_id?(id)
+          block = create_listing_block parent, source, { 'style' => 'source', 'language' => 'sail' }
+        else
+          ::Asciidoctor::Sail.add_id(id)
+          block = create_listing_block parent, source, { 'id' => id, 'style' => 'source', 'language' => 'sail' }
+        end
+
+        block
+      end
+    end
+
+    class SourceIncludeProcessor < ::Asciidoctor::Extensions::IncludeProcessor
+      include SourceMacro
+
+      def handles?(target)
+        target.start_with? 'sail:'
+      end
+
+      def process(doc, reader, target, attrs)
+        logger.info "Including Sail source #{target} #{attrs}"
+        loc = reader.cursor_at_mark
+
+        target.delete_prefix! 'sail:'
+
+        source, type, from = get_source doc, target, attrs, loc
+
+        hyper_ref = attrs.delete('ref')
+
+        id = if type == 'function'
+               "#{from}-#{target}"
+             else
+               "#{from}-#{type}-#{target}"
+             end
+
+        ::Asciidoctor::Sail.add_id_parent(id, hyper_ref) unless ::Asciidoctor::Sail.seen_id?(id)
+
+        reader.push_include source, target, target, 1, {}
+        reader
+      end
+    end
+
+    class WavedromIncludeProcessor < ::Asciidoctor::Extensions::IncludeProcessor
+      include SourceMacro
+
+      def handles?(target)
+        target.start_with? 'sailwavedrom:'
+      end
+
+      def process(doc, reader, target, attrs)
+        target.delete_prefix! 'sailwavedrom:'
+        json, = get_sourcemap doc, attrs, reader.cursor_at_mark
+        json, = get_sail_object json, target, attrs
+
+        key = 'wavedrom'
+        if attrs.any? { |k, v| (k.is_a? Integer) && v == 'right' }
+          key = 'right_wavedrom'
+        elsif attrs.any? { |k, v| (k.is_a? Integer) && v == 'left' }
+          key = 'left_wavedrom'
+        end
+
+        diagram = if attrs.any? { |k, v| (k.is_a? Integer) && v == 'raw' }
+                    json[key]
+                  else
+                    "[wavedrom, ,]\n....\n#{json[key]}\n...."
+                  end
+
+        reader.push_include diagram, target, target, 1, {}
+        reader
+      end
+    end
+
+    class DocCommentIncludeProcessor < ::Asciidoctor::Extensions::IncludeProcessor
+      include SourceMacro
+
+      def handles?(target)
+        target.start_with? 'sailcomment:'
+      end
+
+      def process(doc, reader, target, attrs)
+        target.delete_prefix! 'sailcomment:'
+        json, = get_sourcemap doc, attrs, reader.cursor_at_mark
+        json, = get_sail_object json, target, attrs
+
+        if json.nil? || json.is_a?(Array)
+          raise "#{PLUGIN_NAME}: Could not find Sail object for #{target} when processing include::sailcomment. You may need to specify a clause."
+        end
+
+        comment = json['comment']
+        raise "#{PLUGIN_NAME}: No documentation comment for Sail object #{target}" if comment.nil?
+
+        reader.push_include comment.strip, nil, nil, 1, {}
+        reader
+      end
+    end
+
+    # We want to swap out the source of a listing block to include
+    # cross-referenced source, but asciidoctor won't let us write to
+    # content directly.
+    class ListingDecorator < SimpleDelegator
+      attr_accessor :source
+
+      def content
+        source
+      end
+    end
+
+    # This class overrides the default asciidoctor html5 converter by
+    # post-processing the listing blocks that contain Sail code to
+    # insert cross referencing information.
+    class ListingLinkInserter < (Asciidoctor::Converter.for 'html5')
+      include SourceMacro
+
+      register_for 'html5'
+
+      SAILREF_REGEX = /sailref:(?<from>[^#]*)#(?<type>[^\[]*)\[(?<sail_id>[^\]]*)\]/
+
+      def match_id(match, override_type = nil)
+        type = override_type.nil? ? match[:type] : override_type
+        if type == 'function'
+          "#{match[:from]}-#{match[:sail_id]}"
+        else
+          "#{match[:from]}-#{type}-#{match[:sail_id]}"
+        end
+      end
+
+      def instantiate_template(match, ext)
+        return match[:sail_id] unless /^[a-zA-Z0-9_#?]*$/ =~ match[:sail_id]
+
+        json = ::Asciidoctor::Sail::Sources.get(match[:from])
+        commit = json['git']['commit']
+        json, = get_sail_object json, match[:sail_id], { 'type' => match[:type] }
+        json = json.fetch('source', json)
+        file = json['file']
+        line = json['loc'][0]
+        ext = ext.gsub('%commit%', commit)
+        ext = ext.gsub('%file%', file)
+        ext = ext.gsub('%filehtml%', file.gsub('.sail', '.html'))
+        ext = ext.gsub('%line%', line.to_s)
+        "<a href=\"#{ext}\">#{match[:sail_id]}</a>"
+      rescue Exception
+        match[:sail_id]
+      end
+
+      def source_with_link(match, ref, ext)
+        if ref.nil? && ext.nil?
+          "#{match.pre_match}#{match[:sail_id]}#{match.post_match}"
+        elsif ref.nil?
+          "#{match.pre_match}#{instantiate_template(match, ext)}#{match.post_match}"
+        else
+          "#{match.pre_match}<a href=\"##{ref}\">#{match[:sail_id]}</a>#{match.post_match}"
+        end
+      end
+
+      def external_template(document)
+        document.attr('sail-xref-external')
+      end
+
+      def convert_listing(node)
+        return super unless node.style == 'source' && (node.attr 'language') == 'sail'
+
+        source = node.content
+        ext = external_template node.document
+
+        loop do
+          match = source.match(SAILREF_REGEX)
+          break if match.nil?
+
+          ref = ::Asciidoctor::Sail.get_id(match_id(match))
+          ref = ::Asciidoctor::Sail.get_id(match_id(match, 'val')) if ref.nil? && match[:type] == 'function'
+          source = source_with_link(match, ref, ext)
+        end
+
+        decorated_node = ListingDecorator.new(node)
+        decorated_node.source = source
+
+        super(decorated_node)
+      end
+    end
+  end
+end
diff --git a/extensions/asciidoctor-sail/asciidoctor-sail/sources.rb b/extensions/asciidoctor-sail/asciidoctor-sail/sources.rb
new file mode 100644
index 0000000..ab30fcb
--- /dev/null
+++ b/extensions/asciidoctor-sail/asciidoctor-sail/sources.rb
@@ -0,0 +1,24 @@
+# frozen_string_literal: true
+
+require 'json'
+
+module Asciidoctor
+  module Sail
+    class Sources
+      @sources = {}
+
+      def self.register(key, sourcemap_path)
+        return if @sources.key?(key)
+
+        raise "Sail Asciidoc plugin: File #{sourcemap_path} does not exist" unless File.exist?(sourcemap_path)
+
+        file = File.read(sourcemap_path)
+        @sources[key] = JSON.parse(file)
+      end
+
+      def self.get(key)
+        @sources[key]
+      end
+    end
+  end
+end
diff --git a/themes/riscv-pdf.yml b/themes/riscv-pdf.yml
index 599556e..c44e00e 100644
--- a/themes/riscv-pdf.yml
+++ b/themes/riscv-pdf.yml
@@ -201,13 +201,13 @@ code:
   font-color: 000000
   font_family: $codespan_font_family
   #font_size: ceil($base_font_size)
-  font-size: 10
+  font-size: 9
   padding: $code_font_size
   line_height: 1.15
   # line_gap is an experimental property to control how a background color is applied to an inline block element
   line_gap: 3.8
-  #background_color: f4f4fb
-  background_color: ffffff
+  background_color: fefcff
+  #background_color: ffffff
   #border_color: cccccc
   #border_radius: $base_border_radius
   #border_width: 0.2