Strip external source locations from error traces.

It is possible for a source location to point to code outside of the
source tree (like an inlined function definition in a system header
file).  This patch replaces all such external source locations in
error traces with a special 'missing' source location, inhibiting
linking to external source code.

Author: Mark R. Tuttle

.gitignore

@@ -1,5 +1,8 @@
+__pycache__/
+build/
 cbmc-viewer
 cbmc_viewer.egg-info/
+dist/
 easy_install
 easy_install-*
 make-coverage
@@ -10,5 +13,3 @@ make-result
 make-source
 make-symbol
 make-trace
-build/
-dist/

cbmc_viewer/markup_link.py

@@ -44,7 +44,7 @@ def path_to_file(dst, src):
 def link_text_to_file(text, to_file, from_file=None):
     """Link text to a file in the source tree."""
 
-    if srcloct.is_builtin(to_file):
+    if srcloct.is_builtin(to_file) or srcloct.is_missing(to_file):
         return html.escape(str(text))
 
     from_file = from_file or '.'
@@ -54,7 +54,7 @@ def link_text_to_file(text, to_file, from_file=None):
 def link_text_to_line(text, to_file, line, from_file=None):
     """Link text to a line in a file in the source tree."""
 
-    if srcloct.is_builtin(to_file):
+    if srcloct.is_builtin(to_file) or srcloct.is_missing(to_file):
         return html.escape(str(text))
 
     from_file = from_file or '.'

cbmc_viewer/srcloct.py

@@ -104,12 +104,29 @@ def relpath(path, root):
     required=True
 )
 
+################################################################
+# A "missing source location" for use when the source location really
+# is missing from cbmc output, or when the source location might
+# otherwise point to code outside of the source tree (like an inlined
+# function definition in a system header file).
+
+MISSING = 'MISSING'
+MISSING_SRCLOC = {'file': MISSING, 'function': MISSING, 'line': 0}
+
+def is_missing(name):
+    """The name of a file or function is missing."""
+    return name == MISSING
+
+################################################################
+# Construct a viewer source location from cbmc source locations
+# appearing in cbmc output.
+
 def make_srcloc(path, func, line, wkdir, root):
     """Make a viewer source location from a CBMC source location."""
 
     if path is None or line is None:
         logging.info("Generating a viewer srcloc for a missing CBMC srcloc.")
-        return {'file': 'MISSING', 'function': 'MISSING', 'line': 0}
+        return MISSING_SRCLOC
 
     path = normpath(path)
     if is_builtin(path):

cbmc_viewer/tracet.py

@@ -150,8 +150,11 @@ def handle_duplicate(key, val1, val2):
             logging.warning("Found duplicate traces for property %s", key)
 
         traces = util.merge_dicts(trace_lists, handle_duplicate)
-        return {name: close_function_stack_frames(trace)
-                for name, trace in traces.items()}
+        traces = {name: close_function_stack_frames(trace)
+                  for name, trace in traces.items()}
+        traces = {name: strip_external_srclocs(trace)
+                  for name, trace in traces.items()}
+        return traces
 
 ################################################################
 
@@ -621,6 +624,30 @@ def pop_stack(stack):
 
     return trace
 
+################################################################
+
+def strip_external_srclocs(trace):
+    """Strip source locations pointing to code outside the source tree.
+
+    It is possible for a source location to point to code outside of
+    the source tree (like an inlined function definition in a system
+    header file).  This function replaces all such external source
+    locations in the trace with the special 'missing' source location.
+    """
+
+    for step in trace:
+
+        # The source locations produced by srcloct have paths
+        # relative to the source root for all files under the
+        # root, and have absolute paths for all other files.
+
+        if step['location']['file'].startswith('/'):
+            step['location'] = srcloct.MISSING_SRCLOC
+        if step['detail'].get('location'):
+            if step['detail']['location']['file'].startswith('/'):
+                step['detail']['location'] = srcloct.MISSING_SRCLOC
+    return trace
+
 ################################################################
 # make-trace