text: # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
  # SPDX-License-Identifier: Apache-2.0
  
  """Trace annotated with debugging information."""
  
  import html
  import logging
  import os
  import re
  
  import voluptuous
  import voluptuous.humanize
  
  from cbmc_viewer import markup_link
  from cbmc_viewer import srcloct
  from cbmc_viewer import templates
  from cbmc_viewer import util
  
  # Name of directory holding annotated traces
  TRACES = "traces"
  
  ################################################################
  # Data passed to jinja to generate annotated traces from trace.jinja.html
  
  VALID_STEP = voluptuous.Schema({
      'kind': voluptuous.Any(
          'function-call',
          'function-return',
          'variable-assignment',
          'parameter-assignment',
          'assumption',
          'failure'
      ),
      'num': int,
      'srcloc': str,
      'code': voluptuous.Any(str, None),
      'cbmc': str
  }, required=True)
  
  VALID_TRACE = voluptuous.Schema({
      'prop_name': str,
      'prop_desc': str,
      'prop_srcloc': str,
      'steps': [VALID_STEP],
      'outdir': str
  }, required=True)
  
  ################################################################
  # Source code fragments used to annotate traces.
  
  class CodeSnippet:
      """Source code fragments."""
  
      def __init__(self, root):
          self.root = root  # source root
          self.source = {}  # cache mapping file name -> lines of source code
  
      def lookup(self, path, line):
          """A line of source code."""
  
          if line <= 0: # line numbers are 1-based
              logging.info("CodeSnippet lookup: line number not positive: %s", line)
              return None
          line -= 1    # list indices are 0-based
  
          try:
              if path not in self.source:
                  with open(os.path.join(self.root, path), encoding='utf-8') as code:
                      self.source[path] = code.read().splitlines()
          except FileNotFoundError as error:
              if srcloct.is_builtin(path): # <builtin-library-malloc>, etc.
                  return None
              raise UserWarning(f"CodeSnippet lookup: file not found: {path}") from error
  
          # return the whole statement which may be broken over several lines
          snippet = ' '.join(self.source[path][line:line+5])
          snippet = re.sub(r'\s+', ' ', snippet).strip()
          idx = snippet.find(';')     # end of statement
          if idx >= 0:
              return html.escape(snippet[:idx+1])
          idx = snippet.find('}')     # end of block
          if idx >= 0:
              return html.escape(snippet[:idx+1])
          return html.escape(snippet) # statement extends over more that 5 lines
  
  
      def lookup_srcloc(self, srcloc):
          """A line of source code (at a source location)."""
  
          return self.lookup(srcloc['file'], srcloc['line'])
  
  ################################################################
  
  class Trace:
      """Trace annotated with debugging information."""
  
      def __init__(self, name, trace, symbols, properties, loops, snippets,
                   outdir='.'):
          self.prop_name = name
          self.prop_desc = properties.get_description(name)
          self.prop_srcloc = format_srcloc(properties.get_srcloc(name)
                                           or loops.lookup_assertion(name),
                                           symbols)
          self.steps = [{
              'kind': step['kind'],
              'num': num+1, # convert 0-based index to 1-based line number
              'srcloc': format_srcloc(step['location'], symbols),
              'code': snippets.lookup_srcloc(step['location']),
              'cbmc': format_step(step)
          } for num, step in enumerate(trace)]
          self.outdir = outdir
          self.validate()
  
      def __str__(self):
          """Render annotated trace as html."""
  
          return templates.render_trace(self.prop_name,
                                        self.prop_desc,
                                        self.prop_srcloc,
                                        self.steps)
  
      def validate(self):
          """Validate members of an annotated trace object."""
  
          return voluptuous.humanize.validate_with_humanized_errors(
              self.__dict__, VALID_TRACE
          )
  
      def dump(self, filename=None, outdir=None):
          """Write annotated trace to a file rendered as html."""
  
          util.dump(self,
                    filename or self.prop_name + ".html",
                    outdir or self.outdir)
  
  ################################################################
  # Format a source location
  
  def format_srcloc(srcloc, symbols):
      """Format a source location for a trace step."""
  
      if srcloc is None:
          return 'Function none, File none, Line none'
  
      fyle, func, line = srcloc['file'], srcloc['function'], srcloc['line']
      func_srcloc = symbols.lookup(func)
      # Warning: next line assumes trace root is subdirectory of code root
      from_file = os.path.join(TRACES, 'foo.html') # any name foo.html will do
      # pylint: disable=consider-using-f-string
      return 'Function {}, File {}, Line {}'.format(
          markup_link.link_text_to_srcloc(func, func_srcloc, from_file),
          markup_link.link_text_to_file(fyle, fyle, from_file),
          markup_link.link_text_to_line(line, fyle, line, from_file)
      )
  
  ################################################################
  # Format a trace step
  
  def format_step(step):
      """Format a trace step."""
  
      markup = {
          "function-call": format_function_call,
          "function-return": format_function_return,
          "variable-assignment": format_variable_assignment,
          "parameter-assignment": format_parameter_assignment,
          "assumption": format_assumption,
          "failure": format_failure
      }[step['kind']]
      return markup(step)
  
  def format_function_call(step):
      """Format a function call."""
  
      name, srcloc = step['detail']['name'], step['detail']['location']
  
      line = f'-> {markup_link.link_text_to_srcloc(name, srcloc, "./trace/trace.html")}'
      return line
  
  def format_function_return(step):
      """Format a function return."""
  
      name, srcloc = step['detail']['name'], step['detail']['location']
      line = f'<- {markup_link.link_text_to_srcloc(name, srcloc, "./trace/trace.html")}'
      return line
  
  def format_variable_assignment(step):
      """Format an assignment statement."""
  
      asn = step['detail']
      lhs, rhs, binary = asn['lhs'], asn['rhs-value'], asn['rhs-binary']
      binary = f'({binary})' if binary else ''
      return f'{lhs} = {rhs} {binary}'
  
  def format_parameter_assignment(step):
      """Format an assignment of an actual to formal function argument."""
  
      asn = step['detail']
      lhs, rhs, binary = asn['lhs'], asn['rhs-value'], asn['rhs-binary']
      binary = f'({binary})' if binary else ''
      return f'{lhs} = {rhs} {binary}'
  
  def format_assumption(step):
      """Format a proof assumption."""
  
      pred = step['detail']['predicate']
      return f'assumption: {pred}'
  
  def format_failure(step):
      """Format a proof failure."""
  
      prop = step['detail']['property'] or "Unnamed"
      reason = step['detail']['reason'] or "Not given"
      return f'failure: {prop}: {reason}'
  
  ################################################################
  